awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ZPow (goal)
Goal:
n' : Type u_1
inst : DecidableEq n'
inst_1 : Fintype n'
R : Type u_2
inst_2 : CommRing R
inst_3 : StarRing R
A : M
n : ℕ
⊢ (A ^ -[n+1])ᴴ = Aᴴ ^ -[n+1]
have rw : (A ^ (n + 1))⁻¹ᴴ = Aᴴ ^ -[n+1]
Tactic: rw [zpow_negSucc, zpow_negSucc, conjTranspose_nonsing_inv, conjTranspose_pow]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ZPow (goal)
Goal:
n' : Type u_1
inst : DecidableEq n'
inst_1 : Fintype n'
R : Type u_2
inst_2 : CommRing R
inst_3 : StarRing R
A : M
n : ℕ
rw : (A ^ (n + 1))⁻¹ᴴ = Aᴴ ^ -[n+1]
⊢ (A ^ -[n+1])ᴴ = Aᴴ ^ -[n+1]
have rw₁ : (A ^ (n + 1))⁻¹ᴴ = (Aᴴ ^ (n + 1))⁻¹
Tactic: rw [zpow_negSucc, zpow_negSucc, conjTranspose_nonsing_inv, conjTranspose_pow]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ZPow (goal)
Goal:
n' : Type u_1
inst : DecidableEq n'
inst_1 : Fintype n'
R : Type u_2
inst_2 : CommRing R
inst_3 : StarRing R
A : M
n : ℕ
rw : (A ^ (n + 1))⁻¹ᴴ = Aᴴ ^ -[n+1]
rw₁ : (A ^ (n + 1))⁻¹ᴴ = (Aᴴ ^ (n + 1))⁻¹
⊢ (A ^ -[n+1])ᴴ = Aᴴ ^ -[n+1]
have rw₂ : (A ^ (n + 1))ᴴ⁻¹ = (Aᴴ ^ (n + 1))⁻¹
Tactic: rw [zpow_negSucc, zpow_negSucc, conjTranspose_nonsing_inv, conjTranspose_pow]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ZPow (goal)
Goal:
n' : Type u_1
inst : DecidableEq n'
inst_1 : Fintype n'
R : Type u_2
inst_2 : CommRing R
inst_3 : StarRing R
A : M
n : ℕ
rw : (A ^ (n + 1))⁻¹ᴴ = Aᴴ ^ -[n+1]
rw₁ : (A ^ (n + 1))⁻¹ᴴ = (Aᴴ ^ (n + 1))⁻¹
rw₂ : (A ^ (n + 1))ᴴ⁻¹ = (Aᴴ ^ (n + 1))⁻¹
⊢ (A ^ -[n+1])ᴴ = Aᴴ ^ -[n+1]
have rw₃ : (Aᴴ ^ (n + 1))⁻¹ = (Aᴴ ^ (n + 1))⁻¹
Tactic: rw [zpow_negSucc, zpow_negSucc, conjTranspose_nonsing_inv, conjTranspose_pow]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ZPow (goal)
Goal:
n' : Type u_1
inst : DecidableEq n'
inst_1 : Fintype n'
R : Type u_2
inst_2 : CommRing R
A : M
h : A.IsSymm
k : ℤ
⊢ (A ^ k).IsSymm
have rw : (A ^ k)ᵀ = A ^ k
Tactic: rw [IsSymm, transpose_zpow, h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ZPow (goal)
Goal:
n' : Type u_1
inst : DecidableEq n'
inst_1 : Fintype n'
R : Type u_2
inst_2 : CommRing R
A : M
h : A.IsSymm
k : ℤ
rw : (A ^ k)ᵀ = A ^ k
⊢ (A ^ k).IsSymm
have rw₁ : Aᵀ ^ k = A ^ k
Tactic: rw [IsSymm, transpose_zpow, h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ZPow (goal)
Goal:
n' : Type u_1
inst : DecidableEq n'
inst_1 : Fintype n'
R : Type u_2
inst_2 : CommRing R
A : M
h : A.IsSymm
k : ℤ
rw : (A ^ k)ᵀ = A ^ k
rw₁ : Aᵀ ^ k = A ^ k
⊢ (A ^ k).IsSymm
have rw₂ : A ^ k = A ^ k
Tactic: rw [IsSymm, transpose_zpow, h]
-- 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 : Semiring R
inst_1 : (i : Fin n.succ) → AddCommMonoid (M i)
inst_2 : (i : ι) → AddCommMonoid (M₁ i)
inst_3 : AddCommMonoid M₂
inst_4 : AddCommMonoid M₃
inst_5 : AddCommMonoid M'
inst_6 : (i : Fin n.succ) → Module.{uR, v} R (M i)
inst_7 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_8 : Module R M₂
inst_9 : Module R M₃
inst_10 : Module R M'
f_1 f' f g : MultilinearMap R M₁ M₂
h :
  Eq (α := (a : (i : ι) → M₁ i) → M₂) ((fun (f : MultilinearMap R M₁ M₂) ↦ f.toFun (M₁ := M₁)) f)
    ((fun (f : MultilinearMap R M₁ M₂) ↦ f.toFun (M₁ := M₁)) g)
⊢ f = g
have mk : ∀ (toFun : ((i : ι) → M₁ i) → M₂)
  (map_update_add' :
    ∀ [inst : DecidableEq ι] (m : (i : ι) → M₁ i) (i : ι) (x y : M₁ i),
      toFun (update (β := M₁) m i (x + y)) = toFun (update (β := M₁) m i x) + toFun (update (β := M₁) m i y))
  (map_update_smul' :
    ∀ [inst_11 : DecidableEq ι] (m : (i : ι) → M₁ i) (i : ι) (c : R) (x : M₁ i),
      toFun (update (β := M₁) m i (c • x)) = c • toFun (update (β := M₁) m i x))
  (h :
    Eq (α := (a : (i : ι) → M₁ i) → M₂)
      ((fun (f : MultilinearMap R M₁ M₂) ↦ f.toFun (M₁ := M₁)) (mk (M₁ := M₁) toFun map_update_add' map_update_smul'))
      ((fun (f : MultilinearMap R M₁ M₂) ↦ f.toFun (M₁ := M₁)) g)),
  mk (M₁ := M₁) toFun map_update_add' map_update_smul' = g
Tactic: cases f
Cleared hypotheses: f, h
-- 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 : Semiring R
inst_1 : (i : Fin n.succ) → AddCommMonoid (M i)
inst_2 : (i : ι) → AddCommMonoid (M₁ i)
inst_3 : AddCommMonoid M₂
inst_4 : AddCommMonoid M₃
inst_5 : AddCommMonoid M'
inst_6 : (i : Fin n.succ) → Module.{uR, v} R (M i)
inst_7 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_8 : Module R M₂
inst_9 : Module R M₃
inst_10 : Module R M'
f f' g : MultilinearMap R M₁ M₂
toFun : ((i : ι) → M₁ i) → M₂
map_update_add' :
  ∀ [inst : DecidableEq ι] (m : (i : ι) → M₁ i) (i : ι) (x y : M₁ i),
    toFun (update (β := M₁) m i (x + y)) = toFun (update (β := M₁) m i x) + toFun (update (β := M₁) m i y)
map_update_smul' :
  ∀ [inst_11 : DecidableEq ι] (m : (i : ι) → M₁ i) (i : ι) (c : R) (x : M₁ i),
    toFun (update (β := M₁) m i (c • x)) = c • toFun (update (β := M₁) m i x)
h :
  Eq (α := (a : (i : ι) → M₁ i) → M₂)
    ((fun (f : MultilinearMap R M₁ M₂) ↦ f.toFun (M₁ := M₁)) (mk (M₁ := M₁) toFun map_update_add' map_update_smul'))
    ((fun (f : MultilinearMap R M₁ M₂) ↦ f.toFun (M₁ := M₁)) g)
⊢ mk (M₁ := M₁) toFun map_update_add' map_update_smul' = g
have mk : ∀ (toFun_1 : ((i : ι) → M₁ i) → M₂)
  (map_update_add'_1 :
    ∀ [inst : DecidableEq ι] (m : (i : ι) → M₁ i) (i : ι) (x y : M₁ i),
      toFun_1 (update (β := M₁) m i (x + y)) = toFun_1 (update (β := M₁) m i x) + toFun_1 (update (β := M₁) m i y))
  (map_update_smul'_1 :
    ∀ [inst_11 : DecidableEq ι] (m : (i : ι) → M₁ i) (i : ι) (c : R) (x : M₁ i),
      toFun_1 (update (β := M₁) m i (c • x)) = c • toFun_1 (update (β := M₁) m i x))
  (h :
    Eq (α := (a : (i : ι) → M₁ i) → M₂)
      ((fun (f : MultilinearMap R M₁ M₂) ↦ f.toFun (M₁ := M₁)) (mk (M₁ := M₁) toFun map_update_add' map_update_smul'))
      ((fun (f : MultilinearMap R M₁ M₂) ↦ f.toFun (M₁ := M₁))
        (mk (M₁ := M₁) toFun_1 map_update_add'_1 map_update_smul'_1))),
  mk (M₁ := M₁) toFun map_update_add' map_update_smul' = mk (M₁ := M₁) toFun_1 map_update_add'_1 map_update_smul'_1
Tactic: cases g
Cleared hypotheses: g, h
-- 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 : Semiring R
inst_1 : (i : Fin n.succ) → AddCommMonoid (M i)
inst_2 : (i : ι) → AddCommMonoid (M₁ i)
inst_3 : AddCommMonoid M₂
inst_4 : AddCommMonoid M₃
inst_5 : AddCommMonoid M'
inst_6 : (i : Fin n.succ) → Module.{uR, v} R (M i)
inst_7 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_8 : Module R M₂
inst_9 : Module R M₃
inst_10 : Module R M'
f f' : MultilinearMap R M₁ M₂
toFun : ((i : ι) → M₁ i) → M₂
map_update_add' :
  ∀ [inst : DecidableEq ι] (m : (i : ι) → M₁ i) (i : ι) (x y : M₁ i),
    toFun (update (β := M₁) m i (x + y)) = toFun (update (β := M₁) m i x) + toFun (update (β := M₁) m i y)
map_update_smul' :
  ∀ [inst_11 : DecidableEq ι] (m : (i : ι) → M₁ i) (i : ι) (c : R) (x : M₁ i),
    toFun (update (β := M₁) m i (c • x)) = c • toFun (update (β := M₁) m i x)
toFun_1 : ((i : ι) → M₁ i) → M₂
map_update_add'_1 :
  ∀ [inst : DecidableEq ι] (m : (i : ι) → M₁ i) (i : ι) (x y : M₁ i),
    toFun_1 (update (β := M₁) m i (x + y)) = toFun_1 (update (β := M₁) m i x) + toFun_1 (update (β := M₁) m i y)
map_update_smul'_1 :
  ∀ [inst_11 : DecidableEq ι] (m : (i : ι) → M₁ i) (i : ι) (c : R) (x : M₁ i),
    toFun_1 (update (β := M₁) m i (c • x)) = c • toFun_1 (update (β := M₁) m i x)
h :
  Eq (α := (a : (i : ι) → M₁ i) → M₂)
    ((fun (f : MultilinearMap R M₁ M₂) ↦ f.toFun (M₁ := M₁)) (mk (M₁ := M₁) toFun map_update_add' map_update_smul'))
    ((fun (f : MultilinearMap R M₁ M₂) ↦ f.toFun (M₁ := M₁))
      (mk (M₁ := M₁) toFun_1 map_update_add'_1 map_update_smul'_1))
⊢ mk (M₁ := M₁) toFun map_update_add' map_update_smul' = mk (M₁ := M₁) toFun_1 map_update_add'_1 map_update_smul'_1
have mk : ∀
  (map_update_add'_2 :
    ∀ [inst : DecidableEq ι] (m : (i : ι) → M₁ i) (i : ι) (x y : M₁ i),
      toFun (update (β := M₁) m i (x + y)) = toFun (update (β := M₁) m i x) + toFun (update (β := M₁) m i y))
  (map_update_smul'_2 :
    ∀ [inst_11 : DecidableEq ι] (m : (i : ι) → M₁ i) (i : ι) (c : R) (x : M₁ i),
      toFun (update (β := M₁) m i (c • x)) = c • toFun (update (β := M₁) m i x)),
  mk (M₁ := M₁) toFun map_update_add' map_update_smul' = mk (M₁ := M₁) toFun map_update_add'_2 map_update_smul'_2
Tactic: cases h
Cleared hypotheses: toFun_1, map_update_add'_1, map_update_smul'_1, h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (hypothesis)
Goal:
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : AddCommMonoid M₂
inst_3 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_4 : Module R M₂
f : MultilinearMap R M₁ M₂
m : (i : ι) → M₁ i
i : ι
h : m i = 0
⊢ Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) m : M₂) (0 : M₂)
have this : HSMul.hSMul.{uR, v₁, v₁} (α := R) (β := M₁ i) 0 0 = 0
Tactic: have : (0 : R) • (0 : M₁ i) = 0 := by simp
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (goal)
Goal:
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : AddCommMonoid M₂
inst_3 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_4 : Module R M₂
f : MultilinearMap R M₁ M₂
m : (i : ι) → M₁ i
i : ι
h : m i = 0
this : HSMul.hSMul.{uR, v₁, v₁} (α := R) (β := M₁ i) 0 0 = 0
⊢ Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) m : M₂) (0 : M₂)
have rw : Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i (m i)) : M₂) (0 : M₂)
Tactic: rw [← update_eq_self i m, h, ← this, f.map_update_smul, zero_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (goal)
Goal:
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : AddCommMonoid M₂
inst_3 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_4 : Module R M₂
f : MultilinearMap R M₁ M₂
m : (i : ι) → M₁ i
i : ι
h : m i = 0
this : HSMul.hSMul.{uR, v₁, v₁} (α := R) (β := M₁ i) 0 0 = 0
rw : Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i (m i)) : M₂) (0 : M₂)
⊢ Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) m : M₂) (0 : M₂)
have rw₁ : Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i 0) : M₂) (0 : M₂)
Tactic: rw [← update_eq_self i m, h, ← this, f.map_update_smul, zero_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (goal)
Goal:
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : AddCommMonoid M₂
inst_3 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_4 : Module R M₂
f : MultilinearMap R M₁ M₂
m : (i : ι) → M₁ i
i : ι
h : m i = 0
this : HSMul.hSMul.{uR, v₁, v₁} (α := R) (β := M₁ i) 0 0 = 0
rw : Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i (m i)) : M₂) (0 : M₂)
rw₁ : Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i 0) : M₂) (0 : M₂)
⊢ Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) m : M₂) (0 : M₂)
have rw₂ : Eq.{v₂ + 1} (α := M₂)
  ((f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i (HSMul.hSMul.{uR, v₁, v₁} (α := R) (β := M₁ i) 0 0)) : M₂)
  (0 : M₂)
Tactic: rw [← update_eq_self i m, h, ← this, f.map_update_smul, zero_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (goal)
Goal:
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : AddCommMonoid M₂
inst_3 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_4 : Module R M₂
f : MultilinearMap R M₁ M₂
m : (i : ι) → M₁ i
i : ι
h : m i = 0
this : HSMul.hSMul.{uR, v₁, v₁} (α := R) (β := M₁ i) 0 0 = 0
rw : Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i (m i)) : M₂) (0 : M₂)
rw₁ : Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i 0) : M₂) (0 : M₂)
rw₂ :
  Eq.{v₂ + 1} (α := M₂)
    ((f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i (HSMul.hSMul.{uR, v₁, v₁} (α := R) (β := M₁ i) 0 0)) : M₂)
    (0 : M₂)
⊢ Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) m : M₂) (0 : M₂)
have rw₃ : HSMul.hSMul.{uR, v₂, v₂} (α := R) (β := M₂) 0 ((f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i 0) : M₂) = 0
Tactic: rw [← update_eq_self i m, h, ← this, f.map_update_smul, zero_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (goal)
Goal:
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : AddCommMonoid M₂
inst_3 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_4 : Module R M₂
f : MultilinearMap R M₁ M₂
m : (i : ι) → M₁ i
i : ι
h : m i = 0
this : HSMul.hSMul.{uR, v₁, v₁} (α := R) (β := M₁ i) 0 0 = 0
rw : Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i (m i)) : M₂) (0 : M₂)
rw₁ : Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i 0) : M₂) (0 : M₂)
rw₂ :
  Eq.{v₂ + 1} (α := M₂)
    ((f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i (HSMul.hSMul.{uR, v₁, v₁} (α := R) (β := M₁ i) 0 0)) : M₂)
    (0 : M₂)
rw₃ : HSMul.hSMul.{uR, v₂, v₂} (α := R) (β := M₂) 0 ((f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i 0) : M₂) = 0
⊢ Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) m : M₂) (0 : M₂)
have rw₄ : Eq.{v₂ + 1} (α := M₂) 0 0
Tactic: rw [← update_eq_self i m, h, ← this, f.map_update_smul, zero_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (goal)
Goal:
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : AddCommMonoid M₂
inst_3 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_4 : Module R M₂
f : MultilinearMap R M₁ M₂
m : (i : ι) → M₁ i
i : ι
h : m i = 0
⊢ Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) m : M₂) (0 : M₂)
have have : HSMul.hSMul.{uR, v₁, v₁} (α := R) (β := M₁ i) 0 0 = 0
Tactic: classical
    have : (0 : R) • (0 : M₁ i) = 0 := by simp
    rw [← update_eq_self i m, h, ← this, f.map_update_smul, zero_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (goal)
Goal:
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : AddCommMonoid M₂
inst_3 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_4 : Module R M₂
f : MultilinearMap R M₁ M₂
m : (i : ι) → M₁ i
i : ι
h : m i = 0
have : HSMul.hSMul.{uR, v₁, v₁} (α := R) (β := M₁ i) 0 0 = 0
⊢ Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) m : M₂) (0 : M₂)
have have₁ : ∀ (this : HSMul.hSMul.{uR, v₁, v₁} (α := R) (β := M₁ i) 0 0 = 0),
  Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) m : M₂) (0 : M₂)
Tactic: classical
    have : (0 : R) • (0 : M₁ i) = 0 := by simp
    rw [← update_eq_self i m, h, ← this, f.map_update_smul, zero_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (goal)
Goal:
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : AddCommMonoid M₂
inst_3 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_4 : Module R M₂
f : MultilinearMap R M₁ M₂
inst_5 : Nonempty ι
⊢ Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) 0 : M₂) (0 : M₂)
have obtain : ∀ (i : ι),
  Membership.mem (γ := Set ι) Set.univ i → Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) 0 : M₂) (0 : M₂)
Tactic: obtain ⟨i, _⟩ : ∃ i : ι, i ∈ Set.univ := Set.exists_mem_of_nonempty ι
-- 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 : Semiring R
inst_1 : (i : Fin n.succ) → AddCommMonoid (M i)
inst_2 : (i : ι) → AddCommMonoid (M₁ i)
inst_3 : AddCommMonoid M₂
inst_4 : AddCommMonoid M₃
inst_5 : AddCommMonoid M'
inst_6 : (i : Fin n.succ) → Module.{uR, v} R (M i)
inst_7 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_8 : Module R M₂
inst_9 : Module R M₃
inst_10 : Module R M'
f_1 f' : MultilinearMap R M₁ M₂
inst_11 : Subsingleton ι
i : ι
f : MultilinearMap.{uR, uι, v₂, v₃} R (fun (x : ι) ↦ M₂) M₃
⊢ (fun (f : M₂ →ₗ[R] M₃) ↦
        (mk (M₁ := fun (x : ι) ↦ M₂) (fun (x : (i : ι) → M₂) ↦ (f : (a : M₂) → M₃) (x i)) ⋯ ⋯ :
          MultilinearMap.{uR, uι, v₂, v₃} R (fun (x : ι) ↦ M₂) M₃))
      ((fun (f : MultilinearMap.{uR, uι, v₂, v₃} R (fun (x : ι) ↦ M₂) M₃) ↦
          ({ toFun := fun (x : M₂) ↦ (f : (a : (i : ι) → M₂) → M₃) fun (x_1 : ι) ↦ x, map_add' := ⋯, map_smul' := ⋯ } :
            M₂ →ₗ[R] M₃))
        f) =
    f
have H : ∀ (x : (i : ι) → M₂),
  Eq.{v₃ + 1} (α := M₃)
    (((fun (f : M₂ →ₗ[R] M₃) ↦
              (mk (M₁ := fun (x : ι) ↦ M₂) (fun (x : (i : ι) → M₂) ↦ (f : (a : M₂) → M₃) (x i)) sorry sorry :
                MultilinearMap.{uR, uι, v₂, v₃} R (fun (x : ι) ↦ M₂) M₃))
            ((fun (f : MultilinearMap.{uR, uι, v₂, v₃} R (fun (x : ι) ↦ M₂) M₃) ↦
                ({ toFun := fun (x : M₂) ↦ (f : (a : (i : ι) → M₂) → M₃) fun (x_1 : ι) ↦ x, map_add' := sorry,
                    map_smul' := sorry } :
                  M₂ →ₗ[R] M₃))
              f) :
          (a : (i : ι) → M₂) → M₃)
        x :
      M₃)
    ((f : (a : (i : ι) → M₂) → M₃) x : M₃)
Tactic: ext x
-- 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 : Semiring R
inst_1 : (i : Fin n.succ) → AddCommMonoid (M i)
inst_2 : (i : ι) → AddCommMonoid (M₁ i)
inst_3 : AddCommMonoid M₂
inst_4 : AddCommMonoid M₃
inst_5 : AddCommMonoid M'
inst_6 : (i : Fin n.succ) → Module.{uR, v} R (M i)
inst_7 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_8 : Module R M₂
inst_9 : Module R M₃
inst_10 : Module R M'
f_1 f' : MultilinearMap R M₁ M₂
inst_11 : Subsingleton ι
i : ι
f : MultilinearMap.{uR, uι, v₂, v₃} R (fun (x : ι) ↦ M₂) M₃
x : (i : ι) → M₂
⊢ Eq.{v₃ + 1} (α := M₃)
    (((fun (f : M₂ →ₗ[R] M₃) ↦
              (mk (M₁ := fun (x : ι) ↦ M₂) (fun (x : (i : ι) → M₂) ↦ (f : (a : M₂) → M₃) (x i)) ⋯ ⋯ :
                MultilinearMap.{uR, uι, v₂, v₃} R (fun (x : ι) ↦ M₂) M₃))
            ((fun (f : MultilinearMap.{uR, uι, v₂, v₃} R (fun (x : ι) ↦ M₂) M₃) ↦
                ({ toFun := fun (x : M₂) ↦ (f : (a : (i : ι) → M₂) → M₃) fun (x_1 : ι) ↦ x, map_add' := ⋯,
                    map_smul' := ⋯ } :
                  M₂ →ₗ[R] M₃))
              f) :
          (a : (i : ι) → M₂) → M₃)
        x :
      M₃)
    ((f : (a : (i : ι) → M₂) → M₃) x : M₃)
have H : (fun (x_1 : ι) ↦ x i) = x
Tactic: refine congr_arg f ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (goal)
Goal:
R : Type uR
n : ℕ
M : Fin n.succ → Type v
M₂ : Type v₂
inst : Semiring R
inst_1 : (i : Fin n.succ) → AddCommMonoid (M i)
inst_2 : AddCommMonoid M₂
inst_3 : (i : Fin n.succ) → Module.{uR, v} R (M i)
inst_4 : Module R M₂
f : MultilinearMap R M M₂
m : (i : Fin n) → M i.succ
x y : M 0
⊢ (f : (a : (i : Fin n.succ) → M i) → M₂) (Fin.cons (α := M) (x + y) m) =
    HAdd.hAdd (α := M₂) (β := M₂) ((f : (a : (i : Fin n.succ) → M i) → M₂) (Fin.cons (α := M) x m) : M₂)
      ((f : (a : (i : Fin n.succ) → M i) → M₂) (Fin.cons (α := M) y m) : M₂)
have simp_rw : (f : (a : (i : Fin n.succ) → M i) → M₂) (update (β := M) (Fin.cons (α := M) x m) 0 (x + y)) =
  HAdd.hAdd (α := M₂) (β := M₂) ((f : (a : (i : Fin n.succ) → M i) → M₂) (Fin.cons (α := M) x m) : M₂)
    ((f : (a : (i : Fin n.succ) → M i) → M₂) (Fin.cons (α := M) y m) : M₂)
Tactic: simp_rw [← update_cons_zero x m (x + y), f.map_update_add, update_cons_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (goal)
Goal:
R : Type uR
n : ℕ
M : Fin n.succ → Type v
M₂ : Type v₂
inst : Semiring R
inst_1 : (i : Fin n.succ) → AddCommMonoid (M i)
inst_2 : AddCommMonoid M₂
inst_3 : (i : Fin n.succ) → Module.{uR, v} R (M i)
inst_4 : Module R M₂
f : MultilinearMap R M M₂
m : (i : Fin n) → M i.succ
x y : M 0
simp_rw :
  (f : (a : (i : Fin n.succ) → M i) → M₂) (update (β := M) (Fin.cons (α := M) x m) 0 (x + y)) =
    HAdd.hAdd (α := M₂) (β := M₂) ((f : (a : (i : Fin n.succ) → M i) → M₂) (Fin.cons (α := M) x m) : M₂)
      ((f : (a : (i : Fin n.succ) → M i) → M₂) (Fin.cons (α := M) y m) : M₂)
⊢ (f : (a : (i : Fin n.succ) → M i) → M₂) (Fin.cons (α := M) (x + y) m) =
    HAdd.hAdd (α := M₂) (β := M₂) ((f : (a : (i : Fin n.succ) → M i) → M₂) (Fin.cons (α := M) x m) : M₂)
      ((f : (a : (i : Fin n.succ) → M i) → M₂) (Fin.cons (α := M) y m) : M₂)
have simp_rw₁ : HAdd.hAdd (α := M₂) (β := M₂)
    ((f : (a : (i : Fin n.succ) → M i) → M₂) (update (β := M) (Fin.cons (α := M) x m) 0 x) : M₂)
    ((f : (a : (i : Fin n.succ) → M i) → M₂) (update (β := M) (Fin.cons (α := M) x m) 0 y) : M₂) =
  HAdd.hAdd (α := M₂) (β := M₂) ((f : (a : (i : Fin n.succ) → M i) → M₂) (Fin.cons (α := M) x m) : M₂)
    ((f : (a : (i : Fin n.succ) → M i) → M₂) (Fin.cons (α := M) y m) : M₂)
Tactic: simp_rw [← update_cons_zero x m (x + y), f.map_update_add, update_cons_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (goal)
Goal:
R : Type uR
n : ℕ
M : Fin n.succ → Type v
M₂ : Type v₂
inst : Semiring R
inst_1 : (i : Fin n.succ) → AddCommMonoid (M i)
inst_2 : AddCommMonoid M₂
inst_3 : (i : Fin n.succ) → Module.{uR, v} R (M i)
inst_4 : Module R M₂
f : MultilinearMap R M M₂
m : (i : Fin n) → M i.succ
c : R
x : M 0
⊢ (f : (a : (i : Fin n.succ) → M i) → M₂) (Fin.cons (α := M) (c • x) m) =
    HSMul.hSMul (β := M₂) c ((f : (a : (i : Fin n.succ) → M i) → M₂) (Fin.cons (α := M) x m) : M₂)
have simp_rw : (f : (a : (i : Fin n.succ) → M i) → M₂) (update (β := M) (Fin.cons (α := M) x m) 0 (c • x)) =
  HSMul.hSMul (β := M₂) c ((f : (a : (i : Fin n.succ) → M i) → M₂) (Fin.cons (α := M) x m) : M₂)
Tactic: simp_rw [← update_cons_zero x m (c • x), f.map_update_smul, update_cons_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (goal)
Goal:
R : Type uR
n : ℕ
M : Fin n.succ → Type v
M₂ : Type v₂
inst : Semiring R
inst_1 : (i : Fin n.succ) → AddCommMonoid (M i)
inst_2 : AddCommMonoid M₂
inst_3 : (i : Fin n.succ) → Module.{uR, v} R (M i)
inst_4 : Module R M₂
f : MultilinearMap R M M₂
m : (i : Fin n) → M i.succ
c : R
x : M 0
simp_rw :
  (f : (a : (i : Fin n.succ) → M i) → M₂) (update (β := M) (Fin.cons (α := M) x m) 0 (c • x)) =
    HSMul.hSMul (β := M₂) c ((f : (a : (i : Fin n.succ) → M i) → M₂) (Fin.cons (α := M) x m) : M₂)
⊢ (f : (a : (i : Fin n.succ) → M i) → M₂) (Fin.cons (α := M) (c • x) m) =
    HSMul.hSMul (β := M₂) c ((f : (a : (i : Fin n.succ) → M i) → M₂) (Fin.cons (α := M) x m) : M₂)
have simp_rw₁ : HSMul.hSMul (β := M₂) c ((f : (a : (i : Fin n.succ) → M i) → M₂) (update (β := M) (Fin.cons (α := M) x m) 0 x) : M₂) =
  HSMul.hSMul (β := M₂) c ((f : (a : (i : Fin n.succ) → M i) → M₂) (Fin.cons (α := M) x m) : M₂)
Tactic: simp_rw [← update_cons_zero x m (c • x), f.map_update_smul, update_cons_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (goal)
Goal:
R : Type uR
n : ℕ
M : Fin n.succ → Type v
M₂ : Type v₂
inst : Semiring R
inst_1 : (i : Fin n.succ) → AddCommMonoid (M i)
inst_2 : AddCommMonoid M₂
inst_3 : (i : Fin n.succ) → Module.{uR, v} R (M i)
inst_4 : Module R M₂
f : MultilinearMap R M M₂
m : (i : Fin n) → M i.castSucc
x y : M (last n)
⊢ (f : (a : (i : Fin n.succ) → M i) → M₂) (snoc (α := M) m (x + y)) =
    HAdd.hAdd (α := M₂) (β := M₂) ((f : (a : (i : Fin n.succ) → M i) → M₂) (snoc (α := M) m x) : M₂)
      ((f : (a : (i : Fin n.succ) → M i) → M₂) (snoc (α := M) m y) : M₂)
have simp_rw : (f : (a : (i : Fin n.succ) → M i) → M₂) (update (β := M) (snoc (α := M) m x) (last n) (x + y)) =
  HAdd.hAdd (α := M₂) (β := M₂) ((f : (a : (i : Fin n.succ) → M i) → M₂) (snoc (α := M) m x) : M₂)
    ((f : (a : (i : Fin n.succ) → M i) → M₂) (snoc (α := M) m y) : M₂)
Tactic: simp_rw [← update_snoc_last x m (x + y), f.map_update_add, update_snoc_last]