awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (goal)
Goal:
R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst : Ring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : AddCommMonoid M'
inst_3 : AddCommMonoid M₂
inst_4 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_5 : Module R M'
inst_6 : Module R M₂
inst_7 : Nonempty ι
f : MultilinearMap R M₁ M₂
p : (i : ι) → Submodule R (M₁ i)
c : R
x_1 : M₂
h :
  Membership.mem (γ := Set M₂)
    (Set.image (α := (i : ι) → M₁ i) (⇑f : (a : (i : ι) → M₁ i) → M₂) {v : (i : ι) → M₁ i | ∀ (i : ι), v i ∈ p i}) x_1
x : (i : ι) → M₁ i
hx : Membership.mem (γ := Set ((i : ι) → M₁ i)) {v : (i : ι) → M₁ i | ∀ (i : ι), v i ∈ p i} x
hf : (f : (a : (i : ι) → M₁ i) → M₂) x = x_1
i : ι
this : DecidableEq ι := Classical.decEq ι
j : ι
hij : ¬j = i
⊢ update (β := M₁) x i (c • x i) j ∈ p j
have refine_2 : x j ∈ p j
Tactic: rw [update_of_ne hij]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (goal)
Goal:
R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst : Ring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : AddCommMonoid M'
inst_3 : AddCommMonoid M₂
inst_4 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_5 : Module R M'
inst_6 : Module R M₂
inst_7 : Nonempty ι
f : MultilinearMap R M₁ M₂
p : (i : ι) → Submodule R (M₁ i)
c : R
x_1 : M₂
h :
  Membership.mem (γ := Set M₂)
    (Set.image (α := (i : ι) → M₁ i) (⇑f : (a : (i : ι) → M₁ i) → M₂) {v : (i : ι) → M₁ i | ∀ (i : ι), v i ∈ p i}) x_1
x : (i : ι) → M₁ i
hx : Membership.mem (γ := Set ((i : ι) → M₁ i)) {v : (i : ι) → M₁ i | ∀ (i : ι), v i ∈ p i} x
hf : (f : (a : (i : ι) → M₁ i) → M₂) x = x_1
i : ι
this : DecidableEq ι := Classical.decEq ι
⊢ (f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) x i (c • x i)) =
    HSMul.hSMul (β := M₂) c ((f : (a : (i : ι) → M₁ i) → M₂) x : M₂)
have refine_3 : HSMul.hSMul (β := M₂) c ((f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) x i (x i)) : M₂) =
  HSMul.hSMul (β := M₂) c ((f : (a : (i : ι) → M₁ i) → M₂) x : M₂)
Tactic: rw [f.map_update_smul, update_eq_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (goal)
Goal:
R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst : Ring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : AddCommMonoid M'
inst_3 : AddCommMonoid M₂
inst_4 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_5 : Module R M'
inst_6 : Module R M₂
inst_7 : Nonempty ι
f : MultilinearMap R M₁ M₂
p : (i : ι) → Submodule R (M₁ i)
c : R
x_1 : M₂
h :
  Membership.mem (γ := Set M₂)
    (Set.image (α := (i : ι) → M₁ i) (⇑f : (a : (i : ι) → M₁ i) → M₂) {v : (i : ι) → M₁ i | ∀ (i : ι), v i ∈ p i}) x_1
x : (i : ι) → M₁ i
hx : Membership.mem (γ := Set ((i : ι) → M₁ i)) {v : (i : ι) → M₁ i | ∀ (i : ι), v i ∈ p i} x
hf : (f : (a : (i : ι) → M₁ i) → M₂) x = x_1
i : ι
this : DecidableEq ι := Classical.decEq ι
refine_3 :
  HSMul.hSMul (β := M₂) c ((f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) x i (x i)) : M₂) =
    HSMul.hSMul (β := M₂) c ((f : (a : (i : ι) → M₁ i) → M₂) x : M₂)
⊢ (f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) x i (c • x i)) =
    HSMul.hSMul (β := M₂) c ((f : (a : (i : ι) → M₁ i) → M₂) x : M₂)
have refine_3₁ : HSMul.hSMul (β := M₂) c ((f : (a : (i : ι) → M₁ i) → M₂) x : M₂) =
  HSMul.hSMul (β := M₂) c ((f : (a : (i : ι) → M₁ i) → M₂) x : M₂)
Tactic: rw [f.map_update_smul, update_eq_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basis (goal)
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
M : ι → Type u_3
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u_2, u_3} R (M i)
N : Type u_4
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Finite ι
f g : MultilinearMap R M N
ιM : ι → Type u_5
e : (i : ι) → Basis.{u_5, u_2, u_3} (ιM i) R (M i)
h :
  ∀ (v : (i : ι) → ιM i),
    Eq.{u_4 + 1} (α := N) ((f : (a : (i : ι) → M i) → N) fun (i : ι) ↦ (e i : (a : ιM i) → M i) (v i) : N)
      ((g : (a : (i : ι) → M i) → N) fun (i : ι) ↦ (e i : (a : ιM i) → M i) (v i) : N)
⊢ f = g
have intro : ∀ (val : Fintype ι), f = g
Tactic: cases nonempty_fintype ι
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basis (goal)
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
M : ι → Type u_3
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u_2, u_3} R (M i)
N : Type u_4
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Finite ι
f g : MultilinearMap R M N
ιM : ι → Type u_5
e : (i : ι) → Basis.{u_5, u_2, u_3} (ιM i) R (M i)
h :
  ∀ (v : (i : ι) → ιM i),
    Eq.{u_4 + 1} (α := N) ((f : (a : (i : ι) → M i) → N) fun (i : ι) ↦ (e i : (a : ιM i) → M i) (v i) : N)
      ((g : (a : (i : ι) → M i) → N) fun (i : ι) ↦ (e i : (a : ιM i) → M i) (v i) : N)
val : Fintype ι
⊢ f = g
have intro : ∀ (m : (i : ι) → M i), Eq.{u_4 + 1} (α := N) ((f : (a : (i : ι) → M i) → N) m : N) ((g : (a : (i : ι) → M i) → N) m : N)
Tactic: ext m
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basis (goal)
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
M : ι → Type u_3
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u_2, u_3} R (M i)
N : Type u_4
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Finite ι
f g : MultilinearMap R M N
ιM : ι → Type u_5
e : (i : ι) → Basis.{u_5, u_2, u_3} (ιM i) R (M i)
h :
  ∀ (v : (i : ι) → ιM i),
    Eq.{u_4 + 1} (α := N) ((f : (a : (i : ι) → M i) → N) fun (i : ι) ↦ (e i : (a : ιM i) → M i) (v i) : N)
      ((g : (a : (i : ι) → M i) → N) fun (i : ι) ↦ (e i : (a : ιM i) → M i) (v i) : N)
val : Fintype ι
m : (i : ι) → M i
⊢ Eq.{u_4 + 1} (α := N) ((f : (a : (i : ι) → M i) → N) m : N) ((g : (a : (i : ι) → M i) → N) m : N)
have intro : ∀ (x : (i : ι) → Finsupp.{u_5, u_2} (ιM i) R),
  Eq.{u_4 + 1} (α := N)
    ((f : (a : (i : ι) → M i) → N)
        (Pi.map (α := fun (i : ι) ↦ Finsupp.{u_5, u_2} (ιM i) R) (β := M)
          (fun (i : ι) ↦ (⇑(e i).repr.symm : (a : ιM i →₀ R) → M i)) x) :
      N)
    ((g : (a : (i : ι) → M i) → N)
        (Pi.map (α := fun (i : ι) ↦ Finsupp.{u_5, u_2} (ιM i) R) (β := M)
          (fun (i : ι) ↦ (⇑(e i).repr.symm : (a : ιM i →₀ R) → M i)) x) :
      N)
Tactic: rcases Function.Surjective.piMap (fun i ↦ (e i).repr.symm.surjective) m with ⟨x, rfl⟩
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basis (goal)
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
M : ι → Type u_3
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u_2, u_3} R (M i)
N : Type u_4
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Finite ι
f g : MultilinearMap R M N
ιM : ι → Type u_5
e : (i : ι) → Basis.{u_5, u_2, u_3} (ιM i) R (M i)
h :
  ∀ (v : (i : ι) → ιM i),
    Eq.{u_4 + 1} (α := N) ((f : (a : (i : ι) → M i) → N) fun (i : ι) ↦ (e i : (a : ιM i) → M i) (v i) : N)
      ((g : (a : (i : ι) → M i) → N) fun (i : ι) ↦ (e i : (a : ιM i) → M i) (v i) : N)
val : Fintype ι
x : (i : ι) → Finsupp.{u_5, u_2} (ιM i) R
⊢ Eq.{u_4 + 1} (α := N)
    ((f : (a : (i : ι) → M i) → N)
        (Pi.map (α := fun (i : ι) ↦ Finsupp.{u_5, u_2} (ιM i) R) (β := M)
          (fun (i : ι) ↦ (⇑(e i).repr.symm : (a : ιM i →₀ R) → M i)) x) :
      N)
    ((g : (a : (i : ι) → M i) → N)
        (Pi.map (α := fun (i : ι) ↦ Finsupp.{u_5, u_2} (ιM i) R) (β := M)
          (fun (i : ι) ↦ (⇑(e i).repr.symm : (a : ιM i →₀ R) → M i)) x) :
      N)
have intro : Eq.{u_4 + 1} (α := N)
  ((f : (a : (i : ι) → M i) → N) fun (i : ι) ↦
      (fun (i : ι) ↦
          ((⇑(e i).repr.symm : (a : Finsupp.{u_5, u_2} (ιM i) R) → M i) : (a : Finsupp.{u_5, u_2} (ιM i) R) → M i))
        i (x i) :
    N)
  ((g : (a : (i : ι) → M i) → N) fun (i : ι) ↦
      (fun (i : ι) ↦
          ((⇑(e i).repr.symm : (a : Finsupp.{u_5, u_2} (ιM i) R) → M i) : (a : Finsupp.{u_5, u_2} (ιM i) R) → M i))
        i (x i) :
    N)
Tactic: unfold Pi.map
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basis (goal)
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
M : ι → Type u_3
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u_2, u_3} R (M i)
N : Type u_4
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Finite ι
f g : MultilinearMap R M N
ιM : ι → Type u_5
e : (i : ι) → Basis.{u_5, u_2, u_3} (ιM i) R (M i)
h :
  ∀ (v : (i : ι) → ιM i),
    Eq.{u_4 + 1} (α := N) ((f : (a : (i : ι) → M i) → N) fun (i : ι) ↦ (e i : (a : ιM i) → M i) (v i) : N)
      ((g : (a : (i : ι) → M i) → N) fun (i : ι) ↦ (e i : (a : ιM i) → M i) (v i) : N)
val : Fintype ι
x : (i : ι) → Finsupp.{u_5, u_2} (ιM i) R
intro intro₁ :
  Eq.{u_4 + 1} (α := N)
    ((f : (a : (i : ι) → M i) → N) fun (i : ι) ↦ ((e i).repr.symm : (a : ιM i →₀ R) → M i) (x i) : N)
    ((g : (a : (i : ι) → M i) → N) fun (i : ι) ↦ ((e i).repr.symm : (a : ιM i →₀ R) → M i) (x i) : N)
⊢ Eq.{u_4 + 1} (α := N)
    ((f : (a : (i : ι) → M i) → N) fun (i : ι) ↦
        (fun (i : ι) ↦
            ((⇑(e i).repr.symm : (a : Finsupp.{u_5, u_2} (ιM i) R) → M i) : (a : Finsupp.{u_5, u_2} (ιM i) R) → M i))
          i (x i) :
      N)
    ((g : (a : (i : ι) → M i) → N) fun (i : ι) ↦
        (fun (i : ι) ↦
            ((⇑(e i).repr.symm : (a : Finsupp.{u_5, u_2} (ιM i) R) → M i) : (a : Finsupp.{u_5, u_2} (ιM i) R) → M i))
          i (x i) :
      N)
have intro₂ : Eq.{u_4 + 1} (α := N)
  ((f : (a : (i : ι) → M i) → N) fun (i : ι) ↦
      (Finsupp.linearCombination R (⇑(e i) : (a : ιM i) → M i) : (a : ιM i →₀ R) → M i) (x i) :
    N)
  ((g : (a : (i : ι) → M i) → N) fun (i : ι) ↦
      (Finsupp.linearCombination R (⇑(e i) : (a : ιM i) → M i) : (a : ιM i →₀ R) → M i) (x i) :
    N)
Tactic: simp_rw [(e _).repr_symm_apply, Finsupp.linearCombination_apply, Finsupp.sum,
    map_sum_finset, map_smul_univ, h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basis (goal)
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
M : ι → Type u_3
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u_2, u_3} R (M i)
N : Type u_4
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Finite ι
f g : MultilinearMap R M N
ιM : ι → Type u_5
e : (i : ι) → Basis.{u_5, u_2, u_3} (ιM i) R (M i)
h :
  ∀ (v : (i : ι) → ιM i),
    Eq.{u_4 + 1} (α := N) ((f : (a : (i : ι) → M i) → N) fun (i : ι) ↦ (e i : (a : ιM i) → M i) (v i) : N)
      ((g : (a : (i : ι) → M i) → N) fun (i : ι) ↦ (e i : (a : ιM i) → M i) (v i) : N)
val : Fintype ι
x : (i : ι) → Finsupp.{u_5, u_2} (ιM i) R
intro intro₁ :
  Eq.{u_4 + 1} (α := N)
    ((f : (a : (i : ι) → M i) → N) fun (i : ι) ↦ ((e i).repr.symm : (a : ιM i →₀ R) → M i) (x i) : N)
    ((g : (a : (i : ι) → M i) → N) fun (i : ι) ↦ ((e i).repr.symm : (a : ιM i →₀ R) → M i) (x i) : N)
intro₂ :
  Eq.{u_4 + 1} (α := N)
    ((f : (a : (i : ι) → M i) → N) fun (i : ι) ↦
        (Finsupp.linearCombination R (⇑(e i) : (a : ιM i) → M i) : (a : ιM i →₀ R) → M i) (x i) :
      N)
    ((g : (a : (i : ι) → M i) → N) fun (i : ι) ↦
        (Finsupp.linearCombination R (⇑(e i) : (a : ιM i) → M i) : (a : ιM i →₀ R) → M i) (x i) :
      N)
⊢ Eq.{u_4 + 1} (α := N)
    ((f : (a : (i : ι) → M i) → N) fun (i : ι) ↦
        (fun (i : ι) ↦
            ((⇑(e i).repr.symm : (a : Finsupp.{u_5, u_2} (ιM i) R) → M i) : (a : Finsupp.{u_5, u_2} (ιM i) R) → M i))
          i (x i) :
      N)
    ((g : (a : (i : ι) → M i) → N) fun (i : ι) ↦
        (fun (i : ι) ↦
            ((⇑(e i).repr.symm : (a : Finsupp.{u_5, u_2} (ιM i) R) → M i) : (a : Finsupp.{u_5, u_2} (ιM i) R) → M i))
          i (x i) :
      N)
have intro₃ : Eq.{u_4 + 1} (α := N)
  ((f : (a : (i : ι) → M i) → N) fun (i : ι) ↦
      (x i).sum fun (i_1 : ιM i) (a : R) ↦ HSMul.hSMul (β := M i) a ((e i : (a : ιM i) → M i) i_1 : M i) :
    N)
  ((g : (a : (i : ι) → M i) → N) fun (i : ι) ↦
      (x i).sum fun (i_1 : ιM i) (a : R) ↦ HSMul.hSMul (β := M i) a ((e i : (a : ιM i) → M i) i_1 : M i) :
    N)
Tactic: simp_rw [(e _).repr_symm_apply, Finsupp.linearCombination_apply, Finsupp.sum,
    map_sum_finset, map_smul_univ, h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basis (goal)
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
M : ι → Type u_3
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u_2, u_3} R (M i)
N : Type u_4
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Finite ι
f g : MultilinearMap R M N
ιM : ι → Type u_5
e : (i : ι) → Basis.{u_5, u_2, u_3} (ιM i) R (M i)
h :
  ∀ (v : (i : ι) → ιM i),
    Eq.{u_4 + 1} (α := N) ((f : (a : (i : ι) → M i) → N) fun (i : ι) ↦ (e i : (a : ιM i) → M i) (v i) : N)
      ((g : (a : (i : ι) → M i) → N) fun (i : ι) ↦ (e i : (a : ιM i) → M i) (v i) : N)
val : Fintype ι
x : (i : ι) → Finsupp.{u_5, u_2} (ιM i) R
intro intro₁ :
  Eq.{u_4 + 1} (α := N)
    ((f : (a : (i : ι) → M i) → N) fun (i : ι) ↦ ((e i).repr.symm : (a : ιM i →₀ R) → M i) (x i) : N)
    ((g : (a : (i : ι) → M i) → N) fun (i : ι) ↦ ((e i).repr.symm : (a : ιM i →₀ R) → M i) (x i) : N)
intro₂ :
  Eq.{u_4 + 1} (α := N)
    ((f : (a : (i : ι) → M i) → N) fun (i : ι) ↦
        (Finsupp.linearCombination R (⇑(e i) : (a : ιM i) → M i) : (a : ιM i →₀ R) → M i) (x i) :
      N)
    ((g : (a : (i : ι) → M i) → N) fun (i : ι) ↦
        (Finsupp.linearCombination R (⇑(e i) : (a : ιM i) → M i) : (a : ιM i →₀ R) → M i) (x i) :
      N)
intro₃ :
  Eq.{u_4 + 1} (α := N)
    ((f : (a : (i : ι) → M i) → N) fun (i : ι) ↦
        (x i).sum fun (i_1 : ιM i) (a : R) ↦ HSMul.hSMul (β := M i) a ((e i : (a : ιM i) → M i) i_1 : M i) :
      N)
    ((g : (a : (i : ι) → M i) → N) fun (i : ι) ↦
        (x i).sum fun (i_1 : ιM i) (a : R) ↦ HSMul.hSMul (β := M i) a ((e i : (a : ιM i) → M i) i_1 : M i) :
      N)
⊢ Eq.{u_4 + 1} (α := N)
    ((f : (a : (i : ι) → M i) → N) fun (i : ι) ↦
        (fun (i : ι) ↦
            ((⇑(e i).repr.symm : (a : Finsupp.{u_5, u_2} (ιM i) R) → M i) : (a : Finsupp.{u_5, u_2} (ιM i) R) → M i))
          i (x i) :
      N)
    ((g : (a : (i : ι) → M i) → N) fun (i : ι) ↦
        (fun (i : ι) ↦
            ((⇑(e i).repr.symm : (a : Finsupp.{u_5, u_2} (ιM i) R) → M i) : (a : Finsupp.{u_5, u_2} (ιM i) R) → M i))
          i (x i) :
      N)
have intro₄ : Eq.{u_4 + 1} (α := N)
  ((f : (a : (i : ι) → M i) → N) fun (i : ι) ↦
      ∑ x_1 ∈ (x i).support,
        HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M i) ((x i : (a : ιM i) → R) x_1 : R)
          ((e i : (a : ιM i) → M i) x_1 : M i) :
    N)
  ((g : (a : (i : ι) → M i) → N) fun (i : ι) ↦
      ∑ x_1 ∈ (x i).support,
        HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M i) ((x i : (a : ιM i) → R) x_1 : R)
          ((e i : (a : ιM i) → M i) x_1 : M i) :
    N)
Tactic: simp_rw [(e _).repr_symm_apply, Finsupp.linearCombination_apply, Finsupp.sum,
    map_sum_finset, map_smul_univ, h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basis (goal)
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
M : ι → Type u_3
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u_2, u_3} R (M i)
N : Type u_4
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Finite ι
f g : MultilinearMap R M N
ιM : ι → Type u_5
e : (i : ι) → Basis.{u_5, u_2, u_3} (ιM i) R (M i)
h :
  ∀ (v : (i : ι) → ιM i),
    Eq.{u_4 + 1} (α := N) ((f : (a : (i : ι) → M i) → N) fun (i : ι) ↦ (e i : (a : ιM i) → M i) (v i) : N)
      ((g : (a : (i : ι) → M i) → N) fun (i : ι) ↦ (e i : (a : ιM i) → M i) (v i) : N)
val : Fintype ι
⊢ f = g
have intro : ∀ (m : (i : ι) → M i), Eq.{u_4 + 1} (α := N) ((f : (a : (i : ι) → M i) → N) m : N) ((g : (a : (i : ι) → M i) → N) m : N)
Tactic: classical
  ext m
  rcases Function.Surjective.piMap (fun i ↦ (e i).repr.symm.surjective) m with ⟨x, rfl⟩
  unfold Pi.map
  simp_rw [(e _).repr_symm_apply, Finsupp.linearCombination_apply, Finsupp.sum,
    map_sum_finset, map_smul_univ, h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basis (goal)
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
M : ι → Type u_3
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u_2, u_3} R (M i)
N : Type u_4
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Finite ι
f g : MultilinearMap R M N
ιM : ι → Type u_5
e : (i : ι) → Basis.{u_5, u_2, u_3} (ιM i) R (M i)
h :
  ∀ (v : (i : ι) → ιM i),
    Eq.{u_4 + 1} (α := N) ((f : (a : (i : ι) → M i) → N) fun (i : ι) ↦ (e i : (a : ιM i) → M i) (v i) : N)
      ((g : (a : (i : ι) → M i) → N) fun (i : ι) ↦ (e i : (a : ιM i) → M i) (v i) : N)
val : Fintype ι
intro :
  ∀ (m : (i : ι) → M i),
    Eq.{u_4 + 1} (α := N) ((f : (a : (i : ι) → M i) → N) m : N) ((g : (a : (i : ι) → M i) → N) m : N)
⊢ f = g
have intro₁ : ∀ (x : (i : ι) → Finsupp.{u_5, u_2} (ιM i) R),
  Eq.{u_4 + 1} (α := N)
    ((f : (a : (i : ι) → M i) → N)
        (Pi.map (α := fun (i : ι) ↦ Finsupp.{u_5, u_2} (ιM i) R) (β := M)
          (fun (i : ι) ↦ (⇑(e i).repr.symm : (a : ιM i →₀ R) → M i)) x) :
      N)
    ((g : (a : (i : ι) → M i) → N)
        (Pi.map (α := fun (i : ι) ↦ Finsupp.{u_5, u_2} (ιM i) R) (β := M)
          (fun (i : ι) ↦ (⇑(e i).repr.symm : (a : ιM i →₀ R) → M i)) x) :
      N)
Tactic: classical
  ext m
  rcases Function.Surjective.piMap (fun i ↦ (e i).repr.symm.surjective) m with ⟨x, rfl⟩
  unfold Pi.map
  simp_rw [(e _).repr_symm_apply, Finsupp.linearCombination_apply, Finsupp.sum,
    map_sum_finset, map_smul_univ, h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basis (goal)
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
M : ι → Type u_3
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u_2, u_3} R (M i)
N : Type u_4
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Finite ι
f g : MultilinearMap R M N
ιM : ι → Type u_5
e : (i : ι) → Basis.{u_5, u_2, u_3} (ιM i) R (M i)
h :
  ∀ (v : (i : ι) → ιM i),
    Eq.{u_4 + 1} (α := N) ((f : (a : (i : ι) → M i) → N) fun (i : ι) ↦ (e i : (a : ιM i) → M i) (v i) : N)
      ((g : (a : (i : ι) → M i) → N) fun (i : ι) ↦ (e i : (a : ιM i) → M i) (v i) : N)
val : Fintype ι
intro :
  ∀ (m : (i : ι) → M i),
    Eq.{u_4 + 1} (α := N) ((f : (a : (i : ι) → M i) → N) m : N) ((g : (a : (i : ι) → M i) → N) m : N)
intro₁ :
  ∀ (x : (i : ι) → Finsupp.{u_5, u_2} (ιM i) R),
    Eq.{u_4 + 1} (α := N)
      ((f : (a : (i : ι) → M i) → N)
          (Pi.map (α := fun (i : ι) ↦ Finsupp.{u_5, u_2} (ιM i) R) (β := M)
            (fun (i : ι) ↦ (⇑(e i).repr.symm : (a : ιM i →₀ R) → M i)) x) :
        N)
      ((g : (a : (i : ι) → M i) → N)
          (Pi.map (α := fun (i : ι) ↦ Finsupp.{u_5, u_2} (ιM i) R) (β := M)
            (fun (i : ι) ↦ (⇑(e i).repr.symm : (a : ιM i →₀ R) → M i)) x) :
        N)
⊢ f = g
have intro₂ : ∀ (x : (i : ι) → Finsupp.{u_5, u_2} (ιM i) R),
  Eq.{u_4 + 1} (α := N)
    ((f : (a : (i : ι) → M i) → N) fun (i : ι) ↦
        (fun (i : ι) ↦
            ((⇑(e i).repr.symm : (a : Finsupp.{u_5, u_2} (ιM i) R) → M i) : (a : Finsupp.{u_5, u_2} (ιM i) R) → M i))
          i (x i) :
      N)
    ((g : (a : (i : ι) → M i) → N) fun (i : ι) ↦
        (fun (i : ι) ↦
            ((⇑(e i).repr.symm : (a : Finsupp.{u_5, u_2} (ιM i) R) → M i) : (a : Finsupp.{u_5, u_2} (ιM i) R) → M i))
          i (x i) :
      N)
Tactic: classical
  ext m
  rcases Function.Surjective.piMap (fun i ↦ (e i).repr.symm.surjective) m with ⟨x, rfl⟩
  unfold Pi.map
  simp_rw [(e _).repr_symm_apply, Finsupp.linearCombination_apply, Finsupp.sum,
    map_sum_finset, map_smul_univ, h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basis (goal)
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
M : ι → Type u_3
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u_2, u_3} R (M i)
κ : ι → Type u_5
b : (i : ι) → Basis.{u_5, u_2, u_3} (κ i) R (M i)
ι' : Type u_6
N : Type u_7
inst_3 : AddCommMonoid N
inst_4 : Module R N
b' : Basis ι' R N
inst_5 : Fintype ι
inst_6 : ∀ (i : ι), Finite.{u_5 + 1} (κ i)
i : ((i : ι) → κ i) × ι'
⊢ Eq (α := MultilinearMap R M N)
    ((multilinearMap (M := M) (κ := κ) b b' : (a : ((i : ι) → κ i) × ι') → MultilinearMap R M N) i :
      MultilinearMap R M N)
    (LinearMap.compMultilinearMap (M₁ := M) (M₂ := R) (LinearMap.smulRight LinearMap.id ((b' : (a : ι') → N) i.2))
        (compLinearMap (M₁ := M) (M₁' := fun (x : ι) ↦ R) (MultilinearMap.mkPiRing R ι 1) fun (i' : ι) ↦
          (b i').coord (i.1 i')) :
      MultilinearMap R M N)
have H : ∀ (x : (i : ι) → M i),
  Eq.{u_7 + 1} (α := N)
    ((((multilinearMap (M := M) (κ := κ) b b' : (a : ((i : ι) → κ i) × ι') → MultilinearMap R M N) i :
            MultilinearMap R M N) :
          (a : (i : ι) → M i) → N)
        x :
      N)
    (((LinearMap.compMultilinearMap (M₁ := M) (M₂ := R) (LinearMap.smulRight LinearMap.id ((b' : (a : ι') → N) i.2))
              (compLinearMap (M₁ := M) (M₁' := fun (x : ι) ↦ R) (MultilinearMap.mkPiRing R ι 1) fun (i' : ι) ↦
                (b i').coord (i.1 i')) :
            MultilinearMap R M N) :
          (a : (i : ι) → M i) → N)
        x :
      N)
Tactic: ext x
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Curry (goal)
Goal:
R : Type uR
S : Type uS
ι : Type uι
ι' : Type uι'
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₂ : Type v₂
M₃ : Type v₃
M' : Type v'
inst : CommSemiring R
inst_1 : (i : Fin n.succ) → AddCommMonoid (M i)
inst_2 : AddCommMonoid M'
inst_3 : AddCommMonoid M₂
inst_4 : (i : Fin n.succ) → Module.{uR, v} R (M i)
inst_5 : Module R M'
inst_6 : Module R M₂
f : M 0 →ₗ[R] MultilinearMap.{uR, 0, v, v₂} R (fun (i : Fin n) ↦ M i.succ) M₂
m : (i : Fin n.succ) → M i
i : Fin n.succ
x y : M i
⊢ (fun (m : (i : Fin n.succ) → M i) ↦
        ((((f : (a : M 0) → MultilinearMap R (fun (i : Fin n) ↦ M i.succ) M₂) (m 0) :
                MultilinearMap.{uR, 0, v, v₂} R (fun (i : Fin n) ↦ M i.succ) M₂) :
              (a : (i : Fin n) → M i.succ) → M₂)
            (tail (α := M) m) :
          M₂))
      (update (β := M) m i (x + y)) =
    HAdd.hAdd (α := M₂)
      ((fun (m : (i : Fin n.succ) → M i) ↦
          ((((f : (a : M 0) → MultilinearMap R (fun (i : Fin n) ↦ M i.succ) M₂) (m 0) :
                  MultilinearMap.{uR, 0, v, v₂} R (fun (i : Fin n) ↦ M i.succ) M₂) :
                (a : (i : Fin n) → M i.succ) → M₂)
              (tail (α := M) m) :
            M₂))
        (update (β := M) m i x))
      ((fun (m : (i : Fin n.succ) → M i) ↦
          ((((f : (a : M 0) → MultilinearMap R (fun (i : Fin n) ↦ M i.succ) M₂) (m 0) :
                  MultilinearMap.{uR, 0, v, v₂} R (fun (i : Fin n) ↦ M i.succ) M₂) :
                (a : (i : Fin n) → M i.succ) → M₂)
              (tail (α := M) m) :
            M₂))
        (update (β := M) m i y))
have zero : ∀ (x y : M 0),
  (fun (m : (i : Fin n.succ) → M i) ↦
        ((((f : (a : M 0) → MultilinearMap R (fun (i : Fin n) ↦ M i.succ) M₂) (m 0) :
                MultilinearMap.{uR, 0, v, v₂} R (fun (i : Fin n) ↦ M i.succ) M₂) :
              (a : (i : Fin n) → M i.succ) → M₂)
            (tail (α := M) m) :
          M₂))
      (update (β := M) m 0 (x + y)) =
    HAdd.hAdd (α := M₂)
      ((fun (m : (i : Fin n.succ) → M i) ↦
          ((((f : (a : M 0) → MultilinearMap R (fun (i : Fin n) ↦ M i.succ) M₂) (m 0) :
                  MultilinearMap.{uR, 0, v, v₂} R (fun (i : Fin n) ↦ M i.succ) M₂) :
                (a : (i : Fin n) → M i.succ) → M₂)
              (tail (α := M) m) :
            M₂))
        (update (β := M) m 0 x))
      ((fun (m : (i : Fin n.succ) → M i) ↦
          ((((f : (a : M 0) → MultilinearMap R (fun (i : Fin n) ↦ M i.succ) M₂) (m 0) :
                  MultilinearMap.{uR, 0, v, v₂} R (fun (i : Fin n) ↦ M i.succ) M₂) :
                (a : (i : Fin n) → M i.succ) → M₂)
              (tail (α := M) m) :
            M₂))
        (update (β := M) m 0 y))
Tactic: cases i using Fin.cases
Cleared hypotheses: i, x, y