feat: port Algebra.Module.Pi (#1283)

One earlier failure was extensively discussed:
- https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Performance.20issue.20with.20.60CompleteBooleanAlgebra.60/near/319019205
- https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/type.20class.20inference.20looping

and is fixed as of leanprover/lean4@70a6c06, in mathlib as of the bump #1335.

Another failure posted to Zulip and the Lean 4 repo
- https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/type.20class.20inference.20failure.20in.20pi.20type
- leanprover/lean4#2011

and is fixed as of leanprover/lean4@fedf235, in mathlib as of the bump #1397.

There is one more mysterious `apply` failure, now worked around; we should track this down someday.

- [x] depends on: #1397

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Mathlib.lean

@@ -62,6 +62,7 @@ import Mathlib.Algebra.Hom.Units
 import Mathlib.Algebra.Homology.ComplexShape
 import Mathlib.Algebra.Invertible
 import Mathlib.Algebra.Module.Basic
+import Mathlib.Algebra.Module.Pi
 import Mathlib.Algebra.Module.Prod
 import Mathlib.Algebra.NeZero
 import Mathlib.Algebra.Opposites

Mathlib/Algebra/Module/Pi.lean

@@ -0,0 +1,118 @@
+/-
+Copyright (c) 2018 Simon Hudon. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Simon Hudon, Patrick Massot
+
+! This file was ported from Lean 3 source module algebra.module.pi
+! leanprover-community/mathlib commit a437a2499163d85d670479f69f625f461cc5fef9
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+import Mathlib.Algebra.Module.Basic
+import Mathlib.Algebra.Regular.SMul
+import Mathlib.Algebra.Ring.Pi
+import Mathlib.GroupTheory.GroupAction.Pi
+
+/-!
+# Pi instances for modules
+
+This file defines instances for module and related structures on Pi Types
+-/
+
+
+universe u v w
+
+variable {I : Type u}
+
+-- The indexing type
+variable {f : I → Type v}
+
+-- The family of types already equipped with instances
+variable (x y : ∀ i, f i) (i : I)
+
+namespace Pi
+
+theorem IsSMulRegular.pi {α : Type _} [∀ i, SMul α <| f i] {k : α}
+    (hk : ∀ i, IsSMulRegular (f i) k) : IsSMulRegular (∀ i, f i) k := fun _ _ h =>
+  funext fun i => hk i (congr_fun h i : _)
+#align pi.is_smul_regular.pi Pi.IsSMulRegular.pi
+
+instance smulWithZero (α) [Zero α] [∀ i, Zero (f i)] [∀ i, SMulWithZero α (f i)] :
+    SMulWithZero α (∀ i, f i) :=
+  { Pi.instSMul with
+    smul_zero := fun _ => funext fun _ => smul_zero _
+    zero_smul := fun _ => funext fun _ => zero_smul _ _ }
+#align pi.smul_with_zero Pi.smulWithZero
+
+instance smulWithZero' {g : I → Type _} [∀ i, Zero (g i)] [∀ i, Zero (f i)]
+    [∀ i, SMulWithZero (g i) (f i)] : SMulWithZero (∀ i, g i) (∀ i, f i) :=
+  { Pi.smul' with
+    smul_zero := fun _ => funext fun _ => smul_zero _
+    zero_smul := fun _ => funext fun _ => zero_smul _ _ }
+#align pi.smul_with_zero' Pi.smulWithZero'
+
+instance mulActionWithZero (α) [MonoidWithZero α] [∀ i, Zero (f i)]
+    [∀ i, MulActionWithZero α (f i)] : MulActionWithZero α (∀ i, f i) :=
+  { Pi.mulAction _, Pi.smulWithZero _ with }
+#align pi.mul_action_with_zero Pi.mulActionWithZero
+
+instance mulActionWithZero' {g : I → Type _} [∀ i, MonoidWithZero (g i)] [∀ i, Zero (f i)]
+    [∀ i, MulActionWithZero (g i) (f i)] : MulActionWithZero (∀ i, g i) (∀ i, f i) :=
+  { Pi.mulAction', Pi.smulWithZero' with }
+#align pi.mul_action_with_zero' Pi.mulActionWithZero'
+
+variable (I f)
+
+instance module (α) {r : Semiring α} {m : ∀ i, AddCommMonoid <| f i} [∀ i, Module α <| f i] :
+    @Module α (∀ i : I, f i) r (@Pi.addCommMonoid I f m) :=
+  { Pi.distribMulAction _ with
+    add_smul := fun _ _ _ => funext fun _ => add_smul _ _ _
+    zero_smul := fun _ => funext fun _ => zero_smul α _ }
+#align pi.module Pi.module
+
+/- Extra instance to short-circuit type class resolution.
+For unknown reasons, this is necessary for certain inference problems. E.g., for this to succeed:
+```lean
+example (β X : Type _) [NormedAddCommGroup β] [NormedSpace ℝ β] : Module ℝ (X → β) :=
+inferInstance
+```
+See: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Typeclass.20resolution.20under.20binders/near/281296989
+-/
+/-- A special case of `Pi.module` for non-dependent types. Lean struggles to elaborate
+definitions elsewhere in the library without this. -/
+instance Function.module (α β : Type _) [Semiring α] [AddCommMonoid β] [Module α β] :
+    Module α (I → β) :=
+  Pi.module _ _ _
+#align pi.function.module Pi.Function.module
+
+variable {I f}
+
+instance module' {g : I → Type _} {r : ∀ i, Semiring (f i)} {m : ∀ i, AddCommMonoid (g i)}
+    [∀ i, Module (f i) (g i)] : Module (∀ i, f i) (∀ i, g i)
+    where
+  add_smul := by
+    intros
+    ext1
+    apply add_smul
+  zero_smul := by
+    intros
+    ext1
+    -- Porting note: not sure why `apply zero_smul` fails here.
+    rw [zero_smul]
+#align pi.module' Pi.module'
+
+instance noZeroSMulDivisors (α) {_ : Semiring α} {_ : ∀ i, AddCommMonoid <| f i}
+    [∀ i, Module α <| f i] [∀ i, NoZeroSMulDivisors α <| f i] :
+    NoZeroSMulDivisors α (∀ i : I, f i) :=
+  ⟨fun {_ _} h =>
+    or_iff_not_imp_left.mpr fun hc =>
+      funext fun i => (smul_eq_zero.mp (congr_fun h i)).resolve_left hc⟩
+
+/-- A special case of `Pi.noZeroSMulDivisors` for non-dependent types. Lean struggles to
+synthesize this instance by itself elsewhere in the library. -/
+instance _root_.Function.noZeroSMulDivisors {ι α β : Type _} {_ : Semiring α} {_ : AddCommMonoid β}
+    [Module α β] [NoZeroSMulDivisors α β] : NoZeroSMulDivisors α (ι → β) :=
+  Pi.noZeroSMulDivisors _
+#align function.no_zero_smul_divisors Function.noZeroSMulDivisors
+
+end Pi