awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.CrossProduct (goal)
Goal:
R : Type u_1
inst : CommRing R
u v w : Fin 3 → R
i : Fin (Nat.succ 0).succ.succ
⊢ ![u 1 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 2 -
          u 2 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 1,
        u 2 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 0 -
          u 0 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 2,
        u 0 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 1 -
          u 1 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 0]
      i =
    ((u 0 * w 0 + u 1 * w 1 + u 2 * w 2) • v - (v 0 * u 0 + v 1 * u 1 + v 2 * u 2) • w) i
have h : ![u 1 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 2 -
        u 2 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 1,
      u 2 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 0 -
        u 0 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 2,
      u 0 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 1 -
        u 1 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 0]
    ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨0, sorry⟩ : Fin (Nat.succ 0).succ.succ)) =
  ((u 0 * w 0 + u 1 * w 1 + u 2 * w 2) • v - (v 0 * u 0 + v 1 * u 1 + v 2 * u 2) • w)
    ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨0, sorry⟩)
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.LinearAlgebra.CrossProduct (goal)
Goal:
R : Type u_1
inst : CommRing R
u v w : Fin 3 → R
i : Fin (Nat.succ 0).succ.succ
h :
  ![u 1 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 2 -
          u 2 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 1,
        u 2 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 0 -
          u 0 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 2,
        u 0 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 1 -
          u 1 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 0]
      ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 0).succ.succ)) =
    ((u 0 * w 0 + u 1 * w 1 + u 2 * w 2) • v - (v 0 * u 0 + v 1 * u 1 + v 2 * u 2) • w)
      ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨0, ⋯⟩)
⊢ ![u 1 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 2 -
          u 2 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 1,
        u 2 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 0 -
          u 0 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 2,
        u 0 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 1 -
          u 1 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 0]
      i =
    ((u 0 * w 0 + u 1 * w 1 + u 2 * w 2) • v - (v 0 * u 0 + v 1 * u 1 + v 2 * u 2) • w) i
have h₁ : ![u 1 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 2 -
        u 2 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 1,
      u 2 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 0 -
        u 0 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 2,
      u 0 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 1 -
        u 1 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 0]
    ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨1, sorry⟩ : Fin (Nat.succ 0).succ.succ)) =
  ((u 0 * w 0 + u 1 * w 1 + u 2 * w 2) • v - (v 0 * u 0 + v 1 * u 1 + v 2 * u 2) • w)
    ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨1, sorry⟩)
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.LinearAlgebra.CrossProduct (goal)
Goal:
R : Type u_1
inst : CommRing R
u v w : Fin 3 → R
i : Fin (Nat.succ 0).succ.succ
h :
  ![u 1 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 2 -
          u 2 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 1,
        u 2 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 0 -
          u 0 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 2,
        u 0 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 1 -
          u 1 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 0]
      ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 0).succ.succ)) =
    ((u 0 * w 0 + u 1 * w 1 + u 2 * w 2) • v - (v 0 * u 0 + v 1 * u 1 + v 2 * u 2) • w)
      ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨0, ⋯⟩)
h₁ :
  ![u 1 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 2 -
          u 2 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 1,
        u 2 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 0 -
          u 0 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 2,
        u 0 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 1 -
          u 1 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 0]
      ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨1, ⋯⟩ : Fin (Nat.succ 0).succ.succ)) =
    ((u 0 * w 0 + u 1 * w 1 + u 2 * w 2) • v - (v 0 * u 0 + v 1 * u 1 + v 2 * u 2) • w)
      ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨1, ⋯⟩)
⊢ ![u 1 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 2 -
          u 2 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 1,
        u 2 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 0 -
          u 0 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 2,
        u 0 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 1 -
          u 1 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 0]
      i =
    ((u 0 * w 0 + u 1 * w 1 + u 2 * w 2) • v - (v 0 * u 0 + v 1 * u 1 + v 2 * u 2) • w) i
have h₂ : ![u 1 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 2 -
        u 2 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 1,
      u 2 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 0 -
        u 0 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 2,
      u 0 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 1 -
        u 1 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 0]
    ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨2, sorry⟩ : Fin (Nat.succ 0).succ.succ)) =
  ((u 0 * w 0 + u 1 * w 1 + u 2 * w 2) • v - (v 0 * u 0 + v 1 * u 1 + v 2 * u 2) • w)
    ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨2, sorry⟩)
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.LinearAlgebra.CrossProduct (goal)
Goal:
R : Type u_1
inst : CommRing R
u v w : Fin 3 → R
⊢ ![u 1 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 2 -
          u 2 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 1,
        u 2 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 0 -
          u 0 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 2,
        u 0 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 1 -
          u 1 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 0]
      ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 0).succ.succ)) =
    ((u 0 * w 0 + u 1 * w 1 + u 2 * w 2) • v - (v 0 * u 0 + v 1 * u 1 + v 2 * u 2) • w)
      ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨0, ⋯⟩)
have h : u 1 * (v 0 * w 1 - v 1 * w 0) - u 2 * (v 2 * w 0 - v 0 * w 2) =
  (u 0 * w 0 + u 1 * w 1 + u 2 * w 2) * v 0 - (v 0 * u 0 + v 1 * u 1 + v 2 * u 2) * w 0
Tactic: simp only [Nat.succ_eq_add_one, Nat.reduceAdd, Fin.isValue, cons_val, cons_val_one,
      cons_val_zero, Fin.reduceFinMk, Pi.sub_apply, Pi.smul_apply, smul_eq_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CrossProduct (goal)
Goal:
R : Type u_1
inst : CommRing R
u v w : Fin 3 → R
⊢ ![u 1 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 2 -
          u 2 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 1,
        u 2 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 0 -
          u 0 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 2,
        u 0 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 1 -
          u 1 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 0]
      ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨1, ⋯⟩ : Fin (Nat.succ 0).succ.succ)) =
    ((u 0 * w 0 + u 1 * w 1 + u 2 * w 2) • v - (v 0 * u 0 + v 1 * u 1 + v 2 * u 2) • w)
      ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨1, ⋯⟩)
have h : u 2 * (v 1 * w 2 - v 2 * w 1) - u 0 * (v 0 * w 1 - v 1 * w 0) =
  (u 0 * w 0 + u 1 * w 1 + u 2 * w 2) * v 1 - (v 0 * u 0 + v 1 * u 1 + v 2 * u 2) * w 1
Tactic: simp only [Nat.succ_eq_add_one, Nat.reduceAdd, Fin.isValue, cons_val, cons_val_one,
      cons_val_zero, Fin.reduceFinMk, Pi.sub_apply, Pi.smul_apply, smul_eq_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CrossProduct (goal)
Goal:
R : Type u_1
inst : CommRing R
u v w : Fin 3 → R
⊢ ![u 1 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 2 -
          u 2 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 1,
        u 2 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 0 -
          u 0 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 2,
        u 0 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 1 -
          u 1 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 0]
      ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨2, ⋯⟩ : Fin (Nat.succ 0).succ.succ)) =
    ((u 0 * w 0 + u 1 * w 1 + u 2 * w 2) • v - (v 0 * u 0 + v 1 * u 1 + v 2 * u 2) • w)
      ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨2, ⋯⟩)
have h : u 0 * (v 2 * w 0 - v 0 * w 2) - u 1 * (v 1 * w 2 - v 2 * w 1) =
  (u 0 * w 0 + u 1 * w 1 + u 2 * w 2) * v 2 - (v 0 * u 0 + v 1 * u 1 + v 2 * u 2) * w 2
Tactic: simp only [Nat.succ_eq_add_one, Nat.reduceAdd, Fin.isValue, cons_val, cons_val_one,
      cons_val_zero, Fin.reduceFinMk, Pi.sub_apply, Pi.smul_apply, smul_eq_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
Goal:
ι : Type u_1
R : Type u_3
M : ι → Type u_5
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u_3, u_5} R (M i)
inst_3 : DecidableEq ι
i : ι
⊢ Eq.{u_5 + 1} (α := M i →ₗ[R] M i) (lapply (M := M) i ∘ₗ lsingle (M := M) i) LinearMap.id
have h : ∀ (x : M i),
  Eq (α := M i) ((lapply (M := M) i ∘ₗ lsingle (M := M) i : (a : M i) → M i) x : M i)
    ((LinearMap.id : (a : M i) → M i) x : M i)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
Goal:
ι : Type u_1
R : Type u_3
M : ι → Type u_5
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u_3, u_5} R (M i)
inst_3 : DecidableEq ι
i i' : ι
h : i ≠ i'
⊢ Eq.{u_5 + 1} (α := M i' →ₗ[R] M i) (lapply (M := M) i ∘ₗ lsingle (M := M) i') 0
have h₁ : ∀ (x : M i'),
  Eq (α := M i) ((lapply (M := M) i ∘ₗ lsingle (M := M) i' : (a : M i') → M i) x : M i) ((0 : (a : M i') → M i) x : M i)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
M : ι → Type u_5
N : Type u_6
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u_3, u_5} R (M i)
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : DecidableEq ι
e : ι ≃ ι'
x x_1 : Π₀ (i : ι), M i
⊢ Equiv.toFun (equivCongrLeft (β := M) e) (x + x_1) =
    Equiv.toFun (equivCongrLeft (β := M) e) x + Equiv.toFun (equivCongrLeft (β := M) e) x_1
have h : ∀ (i : ι'),
  (Equiv.toFun (equivCongrLeft (β := M) e) (x + x_1) : (a : ι') → M ((e.symm : (a : ι') → ι) a)) i =
    (Equiv.toFun (equivCongrLeft (β := M) e) x + Equiv.toFun (equivCongrLeft (β := M) e) x_1 :
        (a : ι') → M ((e.symm : (a : ι') → ι) a))
      i
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
M : ι → Type u_5
N : Type u_6
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u_3, u_5} R (M i)
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : DecidableEq ι
e : ι ≃ ι'
x : R
x_1 : Π₀ (i : ι), M i
⊢ Equiv.toFun (equivCongrLeft (β := M) e) (x • x_1) =
    HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) x : R) (Equiv.toFun (equivCongrLeft (β := M) e) x_1)
have h : ∀ (i : ι'),
  (Equiv.toFun (equivCongrLeft (β := M) e) (x • x_1) : (a : ι') → M ((e.symm : (a : ι') → ι) a)) i =
    (HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) x : R) (Equiv.toFun (equivCongrLeft (β := M) e) x_1) :
        (a : ι') → M ((e.symm : (a : ι') → ι) a))
      i
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
M_1 : ι → Type u_5
N : Type u_6
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M_1 i)
inst_2 : (i : ι) → Module.{u_3, u_5} R (M_1 i)
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : DecidableEq ι
α : ι → Type u_7
M : (i : ι) → α i → Type u_8
inst_6 : (i : ι) → (j : α i) → AddCommMonoid (M i j)
inst_7 : (i : ι) → (j : α i) → Module.{u_3, u_8} R (M i j)
x x_1 : Π₀ (i : (x : ι) × α x), M (i.fst (β := fun (x : ι) ↦ α x)) (i.snd (β := fun (x : ι) ↦ α x))
⊢ __spread.0.toFun (x + x_1) = __spread.0.toFun x + __spread.0.toFun x_1
have h : ∀ (i : ι) (i_1 : α i),
  ((__spread.0.toFun (x + x_1) : (a : ι) → Π₀ (j : α a), M a j) i : (a : α i) → M i a) i_1 =
    ((__spread.0.toFun x + __spread.0.toFun x_1 : (a : ι) → Π₀ (j : α a), M a j) i : (a : α i) → M i a) i_1
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
M_1 : ι → Type u_5
N : Type u_6
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M_1 i)
inst_2 : (i : ι) → Module.{u_3, u_5} R (M_1 i)
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : DecidableEq ι
α : ι → Type u_7
M : (i : ι) → α i → Type u_8
inst_6 : (i : ι) → (j : α i) → AddCommMonoid (M i j)
inst_7 : (i : ι) → (j : α i) → Module.{u_3, u_8} R (M i j)
x : R
x_1 : Π₀ (i : (x : ι) × α x), M (i.fst (β := fun (x : ι) ↦ α x)) (i.snd (β := fun (x : ι) ↦ α x))
⊢ __spread.0.toFun (x • x_1) = HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) x : R) (__spread.0.toFun x_1)
have h : ∀ (i : ι) (i_1 : α i),
  ((__spread.0.toFun (x • x_1) : (a : ι) → Π₀ (j : α a), M a j) i : (a : α i) → M i a) i_1 =
    ((HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) x : R) (__spread.0.toFun x_1) : (a : ι) → Π₀ (j : α a), M a j)
          i :
        (a : α i) → M i a)
      i_1
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
M : ι → Type u_5
N : Type u_6
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u_3, u_5} R (M i)
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : DecidableEq ι
inst_6 : Fintype ι
x x_1 : Π₀ (i : ι), M i
⊢ Equiv.toFun (equivFunOnFintype (β := M)) (x + x_1) =
    Equiv.toFun (equivFunOnFintype (β := M)) x + Equiv.toFun (equivFunOnFintype (β := M)) x_1
have h : ∀ (x_2 : ι),
  Equiv.toFun (equivFunOnFintype (β := M)) (x + x_1) x_2 =
    (Equiv.toFun (equivFunOnFintype (β := M)) x + Equiv.toFun (equivFunOnFintype (β := M)) x_1) x_2
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
M : ι → Type u_5
N : Type u_6
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u_3, u_5} R (M i)
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : DecidableEq ι
inst_6 : Fintype ι
x : R
x_1 : Π₀ (i : ι), M i
⊢ Equiv.toFun (equivFunOnFintype (β := M)) (x • x_1) =
    HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) x : R) (Equiv.toFun (equivFunOnFintype (β := M)) x_1)
have h : ∀ (x_2 : ι),
  Equiv.toFun (equivFunOnFintype (β := M)) (x • x_1) x_2 =
    HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) x : R) (Equiv.toFun (equivFunOnFintype (β := M)) x_1) x_2
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
M : ι → Type u_5
N : Type u_6
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u_3, u_5} R (M i)
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : DecidableEq ι
inst_6 : Semiring S
inst_7 : Module S N
inst_8 : SMulCommClass R S N
F : (i : ι) → LinearMap.{u_3, u_3, u_5, u_6} (RingHom.id R) (M i) N
c : R
f : Π₀ (i : ι), M i
⊢ (sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom : (a : Π₀ (i : ι), M i) → N) (c • f) =
    HSMul.hSMul (α := R) (β := N) ((RingHom.id R : (a : R) → R) c : R)
      ((sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom : (a : Π₀ (i : ι), M i) → N) f : N)
have dsimp : (sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom : (a : Π₀ (i : ι), M i) → N) (c • f) =
  HSMul.hSMul (β := N) c ((sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom : (a : Π₀ (i : ι), M i) → N) f : N)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
M : ι → Type u_5
N : Type u_6
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u_3, u_5} R (M i)
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : DecidableEq ι
inst_6 : Semiring S
inst_7 : Module S N
inst_8 : SMulCommClass R S N
F : (i : ι) → LinearMap.{u_3, u_3, u_5, u_6} (RingHom.id R) (M i) N
c : R
f : Π₀ (i : ι), M i
⊢ (sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom : (a : Π₀ (i : ι), M i) → N) (c • f) =
    HSMul.hSMul (β := N) c ((sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom : (a : Π₀ (i : ι), M i) → N) f : N)
have h0 : (sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom : (a : Π₀ (i : ι), M i) → N)
    (HSMul.hSMul (β := Π₀ (i : ι), M i) c 0) =
  HSMul.hSMul (β := N) c ((sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom : (a : Π₀ (i : ι), M i) → N) 0 : N)
Tactic: apply DFinsupp.induction f
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
M : ι → Type u_5
N : Type u_6
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u_3, u_5} R (M i)
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : DecidableEq ι
inst_6 : Semiring S
inst_7 : Module S N
inst_8 : SMulCommClass R S N
F : (i : ι) → LinearMap.{u_3, u_3, u_5, u_6} (RingHom.id R) (M i) N
c : R
f : Π₀ (i : ι), M i
h0 :
  (sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom : (a : Π₀ (i : ι), M i) → N)
      (HSMul.hSMul (β := Π₀ (i : ι), M i) c 0) =
    HSMul.hSMul (β := N) c ((sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom : (a : Π₀ (i : ι), M i) → N) 0 : N)
⊢ (sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom : (a : Π₀ (i : ι), M i) → N) (c • f) =
    HSMul.hSMul (β := N) c ((sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom : (a : Π₀ (i : ι), M i) → N) f : N)
have ha : ∀ (i : ι) (b : M i) (f : Π₀ (i : ι), M i),
  (f : (a : ι) → M a) i = 0 →
    b ≠ 0 →
      (sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom : (a : Π₀ (i : ι), M i) → N) (c • f) =
          HSMul.hSMul (β := N) c
            ((sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom : (a : Π₀ (i : ι), M i) → N) f : N) →
        (sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom : (a : Π₀ (i : ι), M i) → N)
            (c • (single (β := M) i b + f)) =
          HSMul.hSMul (β := N) c
            ((sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom : (a : Π₀ (i : ι), M i) → N)
                (single (β := M) i b + f) :
              N)
Tactic: apply DFinsupp.induction f
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
M : ι → Type u_5
N : Type u_6
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u_3, u_5} R (M i)
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : DecidableEq ι
inst_6 : Semiring S
inst_7 : Module S N
inst_8 : SMulCommClass R S N
F : (i : ι) → LinearMap.{u_3, u_3, u_5, u_6} (RingHom.id R) (M i) N
c : R
f : Π₀ (i : ι), M i
⊢ (sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom : (a : Π₀ (i : ι), M i) → N)
      (HSMul.hSMul (β := Π₀ (i : ι), M i) c 0) =
    HSMul.hSMul (β := N) c ((sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom : (a : Π₀ (i : ι), M i) → N) 0 : N)
have h0 : (sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom : (a : Π₀ (i : ι), M i) → N) 0 =
  HSMul.hSMul (β := N) c ((sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom : (a : Π₀ (i : ι), M i) → N) 0 : N)
Tactic: rw [smul_zero, map_zero, smul_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
M : ι → Type u_5
N : Type u_6
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u_3, u_5} R (M i)
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : DecidableEq ι
inst_6 : Semiring S
inst_7 : Module S N
inst_8 : SMulCommClass R S N
F : (i : ι) → LinearMap.{u_3, u_3, u_5, u_6} (RingHom.id R) (M i) N
c : R
f : Π₀ (i : ι), M i
h0 :
  (sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom : (a : Π₀ (i : ι), M i) → N) 0 =
    HSMul.hSMul (β := N) c ((sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom : (a : Π₀ (i : ι), M i) → N) 0 : N)
⊢ (sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom : (a : Π₀ (i : ι), M i) → N)
      (HSMul.hSMul (β := Π₀ (i : ι), M i) c 0) =
    HSMul.hSMul (β := N) c ((sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom : (a : Π₀ (i : ι), M i) → N) 0 : N)
have h0₁ : 0 = HSMul.hSMul (β := N) c 0
Tactic: rw [smul_zero, map_zero, smul_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
M : ι → Type u_5
N : Type u_6
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u_3, u_5} R (M i)
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : DecidableEq ι
inst_6 : Semiring S
inst_7 : Module S N
inst_8 : SMulCommClass R S N
F : (i : ι) → LinearMap.{u_3, u_3, u_5, u_6} (RingHom.id R) (M i) N
c : R
f : Π₀ (i : ι), M i
h0 :
  (sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom : (a : Π₀ (i : ι), M i) → N) 0 =
    HSMul.hSMul (β := N) c ((sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom : (a : Π₀ (i : ι), M i) → N) 0 : N)
h0₁ : 0 = HSMul.hSMul (β := N) c 0
⊢ (sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom : (a : Π₀ (i : ι), M i) → N)
      (HSMul.hSMul (β := Π₀ (i : ι), M i) c 0) =
    HSMul.hSMul (β := N) c ((sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom : (a : Π₀ (i : ι), M i) → N) 0 : N)
have h0₂ : Eq.{u_6 + 1} (α := N) 0 0
Tactic: rw [smul_zero, map_zero, smul_zero]