awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Finsupp (goal)
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
κ : ι → Type u_4
inst : DecidableEq ι
inst_1 : Fintype ι
inst_2 : CommSemiring R
inst_3 : DecidableEq R
inst_4 : DecidableEq ι'
inst_5 : (i : ι) → Fintype (κ i)
inst_6 : (i : ι) → DecidableEq (κ i)
inst_7 : Fintype ι'
f : ((i : ι) → κ i) × ι' →₀ R
x : (i : ι) → Finsupp.{u_4, u_3} (κ i) R
⊢ Eq (α := ι' →₀ R)
    ((((freeFinsuppEquiv (κ := κ) :
                (a : ((i : ι) → κ i) × ι' →₀ R) → MultilinearMap R (fun (i : ι) ↦ κ i →₀ R) (ι' →₀ R))
              f :
            MultilinearMap R (fun (i : ι) ↦ Finsupp.{u_4, u_3} (κ i) R) (ι' →₀ R)) :
          (a : (i : ι) → κ i →₀ R) → ι' →₀ R)
        x :
      ι' →₀ R)
    (∑ p : ((i : ι) → κ i) × ι',
        HSMul.hSMul (α := R) (β := ι' →₀ R) ((f : (a : ((i : ι) → κ i) × ι') → R) p : R)
          (Finsupp.single p.2 (∏ i : ι, (x i : (a : κ i) → R) (p.1 i))) :
      ι' →₀ R)
have zero : Eq (α := ι' →₀ R)
  (((freeFinsuppEquiv (κ := κ) : (a : ((i : ι) → κ i) × ι' →₀ R) → MultilinearMap R (fun (i : ι) ↦ κ i →₀ R) (ι' →₀ R))
          0 :
        (a : (i : ι) → κ i →₀ R) → ι' →₀ R)
      x :
    ι' →₀ R)
  (∑ p : ((i : ι) → κ i) × ι',
      HSMul.hSMul (α := R) (β := ι' →₀ R) ((0 : (a : ((i : ι) → κ i) × ι') → R) p : R)
        (Finsupp.single p.2 (∏ i : ι, (x i : (a : κ i) → R) (p.1 i))) :
    ι' →₀ R)
Tactic: induction f using Finsupp.induction_linear with
  | zero => simp
  | add f g hf hg => simp [hf, hg, add_mul, Finset.sum_add_distrib]
  | single p r => simp [Finsupp.single_apply]
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Pi (goal)
Goal:
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : Type uN
inst : Semiring R
inst_1 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst_2 : AddCommMonoid N
inst_3 : (i : ι) → (k : κ i) → Module.{uR, uM} R (M i k)
inst_4 : Module R N
inst_5 : Finite ι
inst_6 : ∀ (i : ι), Finite.{uκ + 1} (κ i)
inst_7 : (i : ι) → DecidableEq (κ i)
f g : MultilinearMap R (fun (i : ι) ↦ (j : κ i) → M i j) N
h :
  ∀ (p : (i : ι) → κ i),
    Eq (α := MultilinearMap.{uR, uι, uM, uN} R (fun (i : ι) ↦ M i (p i)) N)
      (f.compLinearMap (M₁ := fun (i : ι) ↦ M i (p i)) (M₁' := fun (i : ι) ↦ (j : κ i) → M i j) fun (i : ι) ↦
        LinearMap.single R (M i) (p i))
      (g.compLinearMap (M₁ := fun (i : ι) ↦ M i (p i)) (M₁' := fun (i : ι) ↦ (j : κ i) → M i j) fun (i : ι) ↦
        LinearMap.single R (M i) (p i))
⊢ f = g
have H : ∀ (x : (i : ι) → (j : κ i) → M i j),
  Eq.{uN + 1} (α := N) ((f : (a : (i : ι) → (j : κ i) → M i j) → N) x : N)
    ((g : (a : (i : ι) → (j : κ i) → M i j) → N) x : N)
Tactic: ext x
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Pi (goal)
Goal:
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : Type uN
inst : Semiring R
inst_1 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst_2 : AddCommMonoid N
inst_3 : (i : ι) → (k : κ i) → Module.{uR, uM} R (M i k)
inst_4 : Module R N
inst_5 : Finite ι
inst_6 : ∀ (i : ι), Finite.{uκ + 1} (κ i)
inst_7 : (i : ι) → DecidableEq (κ i)
f g : MultilinearMap R (fun (i : ι) ↦ (j : κ i) → M i j) N
h :
  ∀ (p : (i : ι) → κ i),
    Eq (α := MultilinearMap.{uR, uι, uM, uN} R (fun (i : ι) ↦ M i (p i)) N)
      (f.compLinearMap (M₁ := fun (i : ι) ↦ M i (p i)) (M₁' := fun (i : ι) ↦ (j : κ i) → M i j) fun (i : ι) ↦
        LinearMap.single R (M i) (p i))
      (g.compLinearMap (M₁ := fun (i : ι) ↦ M i (p i)) (M₁' := fun (i : ι) ↦ (j : κ i) → M i j) fun (i : ι) ↦
        LinearMap.single R (M i) (p i))
x : (i : ι) → (j : κ i) → M i j
⊢ Eq.{uN + 1} (α := N) ((f : (a : (i : ι) → (j : κ i) → M i j) → N) fun (i : ι) ↦ x i : N)
    ((g : (a : (i : ι) → (j : κ i) → M i j) → N) fun (i : ι) ↦ x i : N)
have H : ∀ (i : Fintype ι),
  Eq.{uN + 1} (α := N) ((f : (a : (i : ι) → (j : κ i) → M i j) → N) fun (i : ι) ↦ x i : N)
    ((g : (a : (i : ι) → (j : κ i) → M i j) → N) fun (i : ι) ↦ x i : N)
Tactic: obtain ⟨i⟩ := nonempty_fintype ι
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Pi (goal)
Goal:
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : Type uN
inst : Semiring R
inst_1 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst_2 : AddCommMonoid N
inst_3 : (i : ι) → (k : κ i) → Module.{uR, uM} R (M i k)
inst_4 : Module R N
inst_5 : Finite ι
inst_6 : ∀ (i : ι), Finite.{uκ + 1} (κ i)
inst_7 : (i : ι) → DecidableEq (κ i)
f g : MultilinearMap R (fun (i : ι) ↦ (j : κ i) → M i j) N
h :
  ∀ (p : (i : ι) → κ i),
    Eq (α := MultilinearMap.{uR, uι, uM, uN} R (fun (i : ι) ↦ M i (p i)) N)
      (f.compLinearMap (M₁ := fun (i : ι) ↦ M i (p i)) (M₁' := fun (i : ι) ↦ (j : κ i) → M i j) fun (i : ι) ↦
        LinearMap.single R (M i) (p i))
      (g.compLinearMap (M₁ := fun (i : ι) ↦ M i (p i)) (M₁' := fun (i : ι) ↦ (j : κ i) → M i j) fun (i : ι) ↦
        LinearMap.single R (M i) (p i))
x : (i : ι) → (j : κ i) → M i j
i : Fintype ι
⊢ Eq.{uN + 1} (α := N) ((f : (a : (i : ι) → (j : κ i) → M i j) → N) fun (i : ι) ↦ x i : N)
    ((g : (a : (i : ι) → (j : κ i) → M i j) → N) fun (i : ι) ↦ x i : N)
have H : ∀ (this : (i : ι) → Fintype (κ i)),
  Eq.{uN + 1} (α := N) ((f : (a : (i : ι) → (j : κ i) → M i j) → N) fun (i : ι) ↦ x i : N)
    ((g : (a : (i : ι) → (j : κ i) → M i j) → N) fun (i : ι) ↦ x i : N)
Tactic: have (i : _) := (nonempty_fintype (κ i)).some
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Pi (goal)
Goal:
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : Type uN
inst : Semiring R
inst_1 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst_2 : AddCommMonoid N
inst_3 : (i : ι) → (k : κ i) → Module.{uR, uM} R (M i k)
inst_4 : Module R N
inst_5 : Finite ι
inst_6 : ∀ (i : ι), Finite.{uκ + 1} (κ i)
inst_7 : (i : ι) → DecidableEq (κ i)
f g : MultilinearMap R (fun (i : ι) ↦ (j : κ i) → M i j) N
h :
  ∀ (p : (i : ι) → κ i),
    Eq (α := MultilinearMap.{uR, uι, uM, uN} R (fun (i : ι) ↦ M i (p i)) N)
      (f.compLinearMap (M₁ := fun (i : ι) ↦ M i (p i)) (M₁' := fun (i : ι) ↦ (j : κ i) → M i j) fun (i : ι) ↦
        LinearMap.single R (M i) (p i))
      (g.compLinearMap (M₁ := fun (i : ι) ↦ M i (p i)) (M₁' := fun (i : ι) ↦ (j : κ i) → M i j) fun (i : ι) ↦
        LinearMap.single R (M i) (p i))
x : (i : ι) → (j : κ i) → M i j
i : Fintype ι
this : (i : ι) → Fintype (κ i)
⊢ Eq.{uN + 1} (α := N) ((f : (a : (i : ι) → (j : κ i) → M i j) → N) fun (i : ι) ↦ x i : N)
    ((g : (a : (i : ι) → (j : κ i) → M i j) → N) fun (i : ι) ↦ x i : N)
have H : ∀ (this : DecidableEq ι),
  Eq.{uN + 1} (α := N) ((f : (a : (i : ι) → (j : κ i) → M i j) → N) fun (i : ι) ↦ x i : N)
    ((g : (a : (i : ι) → (j : κ i) → M i j) → N) fun (i : ι) ↦ x i : N)
Tactic: have := Classical.decEq ι
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Pi (goal)
Goal:
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : Type uN
inst : Semiring R
inst_1 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst_2 : AddCommMonoid N
inst_3 : (i : ι) → (k : κ i) → Module.{uR, uM} R (M i k)
inst_4 : Module R N
inst_5 : Finite ι
inst_6 : ∀ (i : ι), Finite.{uκ + 1} (κ i)
inst_7 : (i : ι) → DecidableEq (κ i)
f g : MultilinearMap R (fun (i : ι) ↦ (j : κ i) → M i j) N
h :
  ∀ (p : (i : ι) → κ i),
    Eq (α := MultilinearMap.{uR, uι, uM, uN} R (fun (i : ι) ↦ M i (p i)) N)
      (f.compLinearMap (M₁ := fun (i : ι) ↦ M i (p i)) (M₁' := fun (i : ι) ↦ (j : κ i) → M i j) fun (i : ι) ↦
        LinearMap.single R (M i) (p i))
      (g.compLinearMap (M₁ := fun (i : ι) ↦ M i (p i)) (M₁' := fun (i : ι) ↦ (j : κ i) → M i j) fun (i : ι) ↦
        LinearMap.single R (M i) (p i))
x : (i : ι) → (j : κ i) → M i j
i : Fintype ι
this_1 : (i : ι) → Fintype (κ i)
this : DecidableEq ι
⊢ Eq.{uN + 1} (α := N) ((f : (a : (i : ι) → (j : κ i) → M i j) → N) fun (i : ι) ↦ x i : N)
    ((g : (a : (i : ι) → (j : κ i) → M i j) → N) fun (i : ι) ↦ x i : N)
have H : Eq.{uN + 1} (α := N)
  ((f : (a : (i : ι) → (j : κ i) → M i j) → N) fun (i : ι) ↦
      (fun (i : ι) ↦ (∑ i_1 : κ i, Pi.single (M := M i) i_1 (x i i_1) : (j : κ i) → M i j)) i :
    N)
  ((g : (a : (i : ι) → (j : κ i) → M i j) → N) fun (i : ι) ↦
      (fun (i : ι) ↦ (∑ i_1 : κ i, Pi.single (M := M i) i_1 (x i i_1) : (j : κ i) → M i j)) i :
    N)
Tactic: rw [funext (fun i ↦ Eq.symm (Finset.univ_sum_single (x i)))]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Pi (goal)
Goal:
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : Type uN
inst : Semiring R
inst_1 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst_2 : AddCommMonoid N
inst_3 : (i : ι) → (k : κ i) → Module.{uR, uM} R (M i k)
inst_4 : Module R N
inst_5 : Finite ι
inst_6 : ∀ (i : ι), Finite.{uκ + 1} (κ i)
inst_7 : (i : ι) → DecidableEq (κ i)
f g : MultilinearMap R (fun (i : ι) ↦ (j : κ i) → M i j) N
h :
  ∀ (p : (i : ι) → κ i),
    Eq (α := MultilinearMap.{uR, uι, uM, uN} R (fun (i : ι) ↦ M i (p i)) N)
      (f.compLinearMap (M₁ := fun (i : ι) ↦ M i (p i)) (M₁' := fun (i : ι) ↦ (j : κ i) → M i j) fun (i : ι) ↦
        LinearMap.single R (M i) (p i))
      (g.compLinearMap (M₁ := fun (i : ι) ↦ M i (p i)) (M₁' := fun (i : ι) ↦ (j : κ i) → M i j) fun (i : ι) ↦
        LinearMap.single R (M i) (p i))
x : (i : ι) → (j : κ i) → M i j
i : Fintype ι
this_1 : (i : ι) → Fintype (κ i)
this : DecidableEq ι
⊢ Eq.{uN + 1} (α := N)
    ((f : (a : (i : ι) → (j : κ i) → M i j) → N) fun (i : ι) ↦
        (fun (i : ι) ↦ (∑ i_1 : κ i, Pi.single (M := M i) i_1 (x i i_1) : (j : κ i) → M i j)) i :
      N)
    ((g : (a : (i : ι) → (j : κ i) → M i j) → N) fun (i : ι) ↦
        (fun (i : ι) ↦ (∑ i_1 : κ i, Pi.single (M := M i) i_1 (x i i_1) : (j : κ i) → M i j)) i :
      N)
have H : Eq.{uN + 1} (α := N)
  (∑ r ∈ Fintype.piFinset (δ := κ) fun (i : ι) ↦ Finset.univ,
    (f : (a : (i : ι) → (j : κ i) → M i j) → N) fun (i : ι) ↦ Pi.single (M := M i) (r i) (x i (r i)))
  (∑ r ∈ Fintype.piFinset (δ := κ) fun (i : ι) ↦ Finset.univ,
    (g : (a : (i : ι) → (j : κ i) → M i j) → N) fun (i : ι) ↦ Pi.single (M := M i) (r i) (x i (r i)))
Tactic: simp_rw [MultilinearMap.map_sum_finset]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Pi (goal)
Goal:
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : Type uN
inst : Semiring R
inst_1 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst_2 : AddCommMonoid N
inst_3 : (i : ι) → (k : κ i) → Module.{uR, uM} R (M i k)
inst_4 : Module R N
inst_5 : Finite ι
inst_6 : ∀ (i : ι), Finite.{uκ + 1} (κ i)
inst_7 : (i : ι) → DecidableEq (κ i)
f g : MultilinearMap R (fun (i : ι) ↦ (j : κ i) → M i j) N
h :
  ∀ (p : (i : ι) → κ i),
    Eq (α := MultilinearMap.{uR, uι, uM, uN} R (fun (i : ι) ↦ M i (p i)) N)
      (f.compLinearMap (M₁ := fun (i : ι) ↦ M i (p i)) (M₁' := fun (i : ι) ↦ (j : κ i) → M i j) fun (i : ι) ↦
        LinearMap.single R (M i) (p i))
      (g.compLinearMap (M₁ := fun (i : ι) ↦ M i (p i)) (M₁' := fun (i : ι) ↦ (j : κ i) → M i j) fun (i : ι) ↦
        LinearMap.single R (M i) (p i))
x : (i : ι) → (j : κ i) → M i j
i : Fintype ι
this_1 : (i : ι) → Fintype (κ i)
this : DecidableEq ι
⊢ Eq.{uN + 1} (α := N)
    (∑ r ∈ Fintype.piFinset (δ := κ) fun (i : ι) ↦ Finset.univ,
      (f : (a : (i : ι) → (j : κ i) → M i j) → N) fun (i : ι) ↦ Pi.single (M := M i) (r i) (x i (r i)))
    (∑ r ∈ Fintype.piFinset (δ := κ) fun (i : ι) ↦ Finset.univ,
      (g : (a : (i : ι) → (j : κ i) → M i j) → N) fun (i : ι) ↦ Pi.single (M := M i) (r i) (x i (r i)))
have H : ∀ (p : (a : ι) → κ a),
  Membership.mem (γ := Finset ((a : ι) → κ a)) (Fintype.piFinset (δ := κ) fun (i : ι) ↦ Finset.univ) p →
    Eq.{uN + 1} (α := N)
      ((f : (a : (i : ι) → (j : κ i) → M i j) → N) fun (i : ι) ↦ Pi.single (M := M i) (p i) (x i (p i)) : N)
      ((g : (a : (i : ι) → (j : κ i) → M i j) → N) fun (i : ι) ↦ Pi.single (M := M i) (p i) (x i (p i)) : N)
Tactic: congr! 1 with p
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Pi (hypothesis)
Goal:
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : Type uN
inst : Semiring R
inst_1 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst_2 : AddCommMonoid N
inst_3 : (i : ι) → (k : κ i) → Module.{uR, uM} R (M i k)
inst_4 : Module R N
inst_5 : Finite ι
inst_6 : ∀ (i : ι), Finite.{uκ + 1} (κ i)
inst_7 : (i : ι) → DecidableEq (κ i)
f g : MultilinearMap R (fun (i : ι) ↦ (j : κ i) → M i j) N
h :
  ∀ (p : (i : ι) → κ i),
    Eq (α := MultilinearMap.{uR, uι, uM, uN} R (fun (i : ι) ↦ M i (p i)) N)
      (f.compLinearMap (M₁ := fun (i : ι) ↦ M i (p i)) (M₁' := fun (i : ι) ↦ (j : κ i) → M i j) fun (i : ι) ↦
        LinearMap.single R (M i) (p i))
      (g.compLinearMap (M₁ := fun (i : ι) ↦ M i (p i)) (M₁' := fun (i : ι) ↦ (j : κ i) → M i j) fun (i : ι) ↦
        LinearMap.single R (M i) (p i))
x : (i : ι) → (j : κ i) → M i j
i : Fintype ι
this_1 : (i : ι) → Fintype (κ i)
this : DecidableEq ι
p : (a : ι) → κ a
h_1 : Membership.mem (γ := Finset ((a : ι) → κ a)) (Fintype.piFinset (δ := κ) fun (i : ι) ↦ Finset.univ) p
⊢ Eq.{uN + 1} (α := N)
    ((f : (a : (i : ι) → (j : κ i) → M i j) → N) fun (i : ι) ↦ Pi.single (M := M i) (p i) (x i (p i)) : N)
    ((g : (a : (i : ι) → (j : κ i) → M i j) → N) fun (i : ι) ↦ Pi.single (M := M i) (p i) (x i (p i)) : N)
have h₁ : ∀ (p : (i : ι) → κ i) (x : (i : ι) → M i (p i)),
  Eq.{uN + 1} (α := N)
    ((f.compLinearMap (M₁ := fun (i : ι) ↦ M i (p i)) (M₁' := fun (i : ι) ↦ (j : κ i) → M i j) fun (i : ι) ↦
            LinearMap.single R (M i) (p i) :
          (a : (i : ι) → M i (p i)) → N)
        x :
      N)
    ((g.compLinearMap (M₁ := fun (i : ι) ↦ M i (p i)) (M₁' := fun (i : ι) ↦ (j : κ i) → M i j) fun (i : ι) ↦
            LinearMap.single R (M i) (p i) :
          (a : (i : ι) → M i (p i)) → N)
        x :
      N)
Tactic: simp_rw [MultilinearMap.ext_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Pi (goal)
Goal:
ι : Type uι
κ : ι → Type uκ
S : Type uS
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst : Semiring R
inst_1 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst_2 : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst_3 : (i : ι) → (k : κ i) → Module.{uR, uM} R (M i k)
inst_4 : (p : (i : ι) → κ i) → Module.{uR, uN} R (N p)
f : (p : (i : ι) → κ i) → MultilinearMap.{uR, uι, uM, uN} R (fun (i : ι) ↦ M i (p i)) (N p)
dec : DecidableEq ι
m : (i : ι) → (j : κ i) → M i j
i : ι
x y : (j : κ i) → M i j
p : (i : ι) → κ i
⊢ ((f p : (a : (i : ι) → M i (p i)) → N p) fun (i_1 : ι) ↦
      Function.update (β := fun (i : ι) ↦ (j : κ i) → M i j) m i (x + y) i_1 (p i_1)) =
    HAdd.hAdd (α := (t : (i : ι) → κ i) → N t) (β := (t : (i : ι) → κ i) → N t)
      (fun (p : (i : ι) → κ i) ↦
        (f p : (a : (i : ι) → M i (p i)) → N p) fun (i_1 : ι) ↦
          Function.update (β := fun (i : ι) ↦ (j : κ i) → M i j) m i x i_1 (p i_1))
      (fun (p : (i : ι) → κ i) ↦
        (f p : (a : (i : ι) → M i (p i)) → N p) fun (i_1 : ι) ↦
          Function.update (β := fun (i : ι) ↦ (j : κ i) → M i j) m i y i_1 (p i_1))
      p
have dsimp : ((f p : (a : (i : ι) → M i (p i)) → N p) fun (i_1 : ι) ↦
    Function.update (β := fun (i : ι) ↦ (j : κ i) → M i j) m i (x + y) i_1 (p i_1)) =
  HAdd.hAdd (α := N p)
    ((f p : (a : (i : ι) → M i (p i)) → N p) fun (i_1 : ι) ↦
      Function.update (β := fun (i : ι) ↦ (j : κ i) → M i j) m i x i_1 (p i_1))
    ((f p : (a : (i : ι) → M i (p i)) → N p) fun (i_1 : ι) ↦
      Function.update (β := fun (i : ι) ↦ (j : κ i) → M i j) m i y i_1 (p i_1))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Pi (goal)
Goal:
ι : Type uι
κ : ι → Type uκ
S : Type uS
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst : Semiring R
inst_1 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst_2 : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst_3 : (i : ι) → (k : κ i) → Module.{uR, uM} R (M i k)
inst_4 : (p : (i : ι) → κ i) → Module.{uR, uN} R (N p)
f : (p : (i : ι) → κ i) → MultilinearMap.{uR, uι, uM, uN} R (fun (i : ι) ↦ M i (p i)) (N p)
dec : DecidableEq ι
m : (i : ι) → (j : κ i) → M i j
i : ι
x y : (j : κ i) → M i j
p : (i : ι) → κ i
⊢ ((f p : (a : (i : ι) → M i (p i)) → N p) fun (i_1 : ι) ↦
      Function.update (β := fun (i : ι) ↦ (j : κ i) → M i j) m i (x + y) i_1 (p i_1)) =
    HAdd.hAdd (α := N p)
      ((f p : (a : (i : ι) → M i (p i)) → N p) fun (i_1 : ι) ↦
        Function.update (β := fun (i : ι) ↦ (j : κ i) → M i j) m i x i_1 (p i_1))
      ((f p : (a : (i : ι) → M i (p i)) → N p) fun (i_1 : ι) ↦
        Function.update (β := fun (i : ι) ↦ (j : κ i) → M i j) m i y i_1 (p i_1))
have simp_rw : ((f p : (a : (i : ι) → M i (p i)) → N p) fun (i_1 : ι) ↦
    Function.update (β := fun (i : ι) ↦ M i (p i)) (fun (k : ι) ↦ m k (p k)) i ((x + y) (p i)) i_1) =
  HAdd.hAdd (α := N p)
    ((f p : (a : (i : ι) → M i (p i)) → N p) fun (i_1 : ι) ↦
      Function.update (β := fun (i : ι) ↦ M i (p i)) (fun (k : ι) ↦ m k (p k)) i (x (p i) : M i (p i)) i_1)
    ((f p : (a : (i : ι) → M i (p i)) → N p) fun (i_1 : ι) ↦
      Function.update (β := fun (i : ι) ↦ M i (p i)) (fun (k : ι) ↦ m k (p k)) i (y (p i) : M i (p i)) i_1)
Tactic: simp_rw [Function.apply_update (fun i m => m (p i)) m, Pi.add_apply, (f p).map_update_add]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Pi (goal)
Goal:
ι : Type uι
κ : ι → Type uκ
S : Type uS
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst : Semiring R
inst_1 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst_2 : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst_3 : (i : ι) → (k : κ i) → Module.{uR, uM} R (M i k)
inst_4 : (p : (i : ι) → κ i) → Module.{uR, uN} R (N p)
f : (p : (i : ι) → κ i) → MultilinearMap.{uR, uι, uM, uN} R (fun (i : ι) ↦ M i (p i)) (N p)
dec : DecidableEq ι
m : (i : ι) → (j : κ i) → M i j
i : ι
x y : (j : κ i) → M i j
p : (i : ι) → κ i
simp_rw :
  ((f p : (a : (i : ι) → M i (p i)) → N p) fun (i_1 : ι) ↦
      Function.update (β := fun (i : ι) ↦ M i (p i)) (fun (k : ι) ↦ m k (p k)) i ((x + y) (p i)) i_1) =
    HAdd.hAdd (α := N p)
      ((f p : (a : (i : ι) → M i (p i)) → N p) fun (i_1 : ι) ↦
        Function.update (β := fun (i : ι) ↦ M i (p i)) (fun (k : ι) ↦ m k (p k)) i (x (p i) : M i (p i)) i_1)
      ((f p : (a : (i : ι) → M i (p i)) → N p) fun (i_1 : ι) ↦
        Function.update (β := fun (i : ι) ↦ M i (p i)) (fun (k : ι) ↦ m k (p k)) i (y (p i) : M i (p i)) i_1)
⊢ ((f p : (a : (i : ι) → M i (p i)) → N p) fun (i_1 : ι) ↦
      Function.update (β := fun (i : ι) ↦ (j : κ i) → M i j) m i (x + y) i_1 (p i_1)) =
    HAdd.hAdd (α := N p)
      ((f p : (a : (i : ι) → M i (p i)) → N p) fun (i_1 : ι) ↦
        Function.update (β := fun (i : ι) ↦ (j : κ i) → M i j) m i x i_1 (p i_1))
      ((f p : (a : (i : ι) → M i (p i)) → N p) fun (i_1 : ι) ↦
        Function.update (β := fun (i : ι) ↦ (j : κ i) → M i j) m i y i_1 (p i_1))
have simp_rw₁ : ((f p : (a : (i : ι) → M i (p i)) → N p) fun (i_1 : ι) ↦
    Function.update (β := fun (i : ι) ↦ M i (p i)) (fun (k : ι) ↦ m k (p k)) i
      (HAdd.hAdd (α := M i (p i)) (x (p i)) (y (p i))) i_1) =
  HAdd.hAdd (α := N p)
    ((f p : (a : (i : ι) → M i (p i)) → N p) fun (i_1 : ι) ↦
      Function.update (β := fun (i : ι) ↦ M i (p i)) (fun (k : ι) ↦ m k (p k)) i (x (p i) : M i (p i)) i_1)
    ((f p : (a : (i : ι) → M i (p i)) → N p) fun (i_1 : ι) ↦
      Function.update (β := fun (i : ι) ↦ M i (p i)) (fun (k : ι) ↦ m k (p k)) i (y (p i) : M i (p i)) i_1)
Tactic: simp_rw [Function.apply_update (fun i m => m (p i)) m, Pi.add_apply, (f p).map_update_add]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Pi (goal)
Goal:
ι : Type uι
κ : ι → Type uκ
S : Type uS
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst : Semiring R
inst_1 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst_2 : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst_3 : (i : ι) → (k : κ i) → Module.{uR, uM} R (M i k)
inst_4 : (p : (i : ι) → κ i) → Module.{uR, uN} R (N p)
f : (p : (i : ι) → κ i) → MultilinearMap.{uR, uι, uM, uN} R (fun (i : ι) ↦ M i (p i)) (N p)
dec : DecidableEq ι
m : (i : ι) → (j : κ i) → M i j
i : ι
c : R
x : (j : κ i) → M i j
p : (i : ι) → κ i
⊢ ((f p : (a : (i : ι) → M i (p i)) → N p) fun (i_1 : ι) ↦
      Function.update (β := fun (i : ι) ↦ (j : κ i) → M i j) m i (c • x) i_1 (p i_1)) =
    HSMul.hSMul (β := (t : (i : ι) → κ i) → N t) c
      (fun (p : (i : ι) → κ i) ↦
        (f p : (a : (i : ι) → M i (p i)) → N p) fun (i_1 : ι) ↦
          Function.update (β := fun (i : ι) ↦ (j : κ i) → M i j) m i x i_1 (p i_1))
      p
have dsimp : ((f p : (a : (i : ι) → M i (p i)) → N p) fun (i_1 : ι) ↦
    Function.update (β := fun (i : ι) ↦ (j : κ i) → M i j) m i (c • x) i_1 (p i_1)) =
  HSMul.hSMul (β := N p) c
    ((f p : (a : (i : ι) → M i (p i)) → N p) fun (i_1 : ι) ↦
      Function.update (β := fun (i : ι) ↦ (j : κ i) → M i j) m i x i_1 (p i_1))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Pi (goal)
Goal:
ι : Type uι
κ : ι → Type uκ
S : Type uS
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst : Semiring R
inst_1 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst_2 : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst_3 : (i : ι) → (k : κ i) → Module.{uR, uM} R (M i k)
inst_4 : (p : (i : ι) → κ i) → Module.{uR, uN} R (N p)
f : (p : (i : ι) → κ i) → MultilinearMap.{uR, uι, uM, uN} R (fun (i : ι) ↦ M i (p i)) (N p)
dec : DecidableEq ι
m : (i : ι) → (j : κ i) → M i j
i : ι
c : R
x : (j : κ i) → M i j
p : (i : ι) → κ i
⊢ ((f p : (a : (i : ι) → M i (p i)) → N p) fun (i_1 : ι) ↦
      Function.update (β := fun (i : ι) ↦ (j : κ i) → M i j) m i (c • x) i_1 (p i_1)) =
    HSMul.hSMul (β := N p) c
      ((f p : (a : (i : ι) → M i (p i)) → N p) fun (i_1 : ι) ↦
        Function.update (β := fun (i : ι) ↦ (j : κ i) → M i j) m i x i_1 (p i_1))
have simp_rw : ((f p : (a : (i : ι) → M i (p i)) → N p) fun (i_1 : ι) ↦
    Function.update (β := fun (i : ι) ↦ M i (p i)) (fun (k : ι) ↦ m k (p k)) i ((c • x) (p i)) i_1) =
  HSMul.hSMul (β := N p) c
    ((f p : (a : (i : ι) → M i (p i)) → N p) fun (i_1 : ι) ↦
      Function.update (β := fun (i : ι) ↦ M i (p i)) (fun (k : ι) ↦ m k (p k)) i (x (p i) : M i (p i)) i_1)
Tactic: simp_rw [Function.apply_update (fun i m => m (p i)) m, Pi.smul_apply, (f p).map_update_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Pi (goal)
Goal:
ι : Type uι
κ : ι → Type uκ
S : Type uS
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst : Semiring R
inst_1 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst_2 : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst_3 : (i : ι) → (k : κ i) → Module.{uR, uM} R (M i k)
inst_4 : (p : (i : ι) → κ i) → Module.{uR, uN} R (N p)
f : (p : (i : ι) → κ i) → MultilinearMap.{uR, uι, uM, uN} R (fun (i : ι) ↦ M i (p i)) (N p)
dec : DecidableEq ι
m : (i : ι) → (j : κ i) → M i j
i : ι
c : R
x : (j : κ i) → M i j
p : (i : ι) → κ i
simp_rw :
  ((f p : (a : (i : ι) → M i (p i)) → N p) fun (i_1 : ι) ↦
      Function.update (β := fun (i : ι) ↦ M i (p i)) (fun (k : ι) ↦ m k (p k)) i ((c • x) (p i)) i_1) =
    HSMul.hSMul (β := N p) c
      ((f p : (a : (i : ι) → M i (p i)) → N p) fun (i_1 : ι) ↦
        Function.update (β := fun (i : ι) ↦ M i (p i)) (fun (k : ι) ↦ m k (p k)) i (x (p i) : M i (p i)) i_1)
⊢ ((f p : (a : (i : ι) → M i (p i)) → N p) fun (i_1 : ι) ↦
      Function.update (β := fun (i : ι) ↦ (j : κ i) → M i j) m i (c • x) i_1 (p i_1)) =
    HSMul.hSMul (β := N p) c
      ((f p : (a : (i : ι) → M i (p i)) → N p) fun (i_1 : ι) ↦
        Function.update (β := fun (i : ι) ↦ (j : κ i) → M i j) m i x i_1 (p i_1))
have simp_rw₁ : ((f p : (a : (i : ι) → M i (p i)) → N p) fun (i_1 : ι) ↦
    Function.update (β := fun (i : ι) ↦ M i (p i)) (fun (k : ι) ↦ m k (p k)) i
      (HSMul.hSMul (β := M i (p i)) c (x (p i))) i_1) =
  HSMul.hSMul (β := N p) c
    ((f p : (a : (i : ι) → M i (p i)) → N p) fun (i_1 : ι) ↦
      Function.update (β := fun (i : ι) ↦ M i (p i)) (fun (k : ι) ↦ m k (p k)) i (x (p i) : M i (p i)) i_1)
Tactic: simp_rw [Function.apply_update (fun i m => m (p i)) m, Pi.smul_apply, (f p).map_update_smul]