awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.CrossProduct
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, ⋯⟩)
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, ⋯⟩ : 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, ⋯⟩)
⊢ ![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

Tactic:
fin_cases i
-- Module: Mathlib.LinearAlgebra.CrossProduct
Goal:
R : Type u_1
inst : CommRing R
u v w : Fin 3 → R
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
⊢ ![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, ⋯⟩)

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]

Premises used: Nat.succ_eq_add_one, Matrix.cons_val_one, Matrix.cons_val_zero, Nat.reduceAdd, Fin.reduceFinMk, Fin.isValue, Matrix.cons_val, smul_eq_mul, Pi.sub_apply, Pi.smul_apply
-- Module: Mathlib.LinearAlgebra.CrossProduct
Goal:
R : Type u_1
inst : CommRing R
u v w : Fin 3 → R
⊢ 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:
ring
-- Module: Mathlib.LinearAlgebra.CrossProduct
Goal:
R : Type u_1
inst : CommRing R
u v w : Fin 3 → R
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
⊢ ![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, ⋯⟩)

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]

Premises used: Nat.succ_eq_add_one, Matrix.cons_val_one, Matrix.cons_val_zero, Nat.reduceAdd, Fin.reduceFinMk, Fin.isValue, Matrix.cons_val, smul_eq_mul, Pi.sub_apply, Pi.smul_apply
-- Module: Mathlib.LinearAlgebra.CrossProduct
Goal:
R : Type u_1
inst : CommRing R
u v w : Fin 3 → R
⊢ 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:
ring
-- Module: Mathlib.LinearAlgebra.CrossProduct
Goal:
R : Type u_1
inst : CommRing R
u v w : Fin 3 → R
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
⊢ ![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, ⋯⟩)

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]

Premises used: Nat.succ_eq_add_one, Matrix.cons_val_one, Matrix.cons_val_zero, Nat.reduceAdd, Fin.reduceFinMk, Fin.isValue, Matrix.cons_val, smul_eq_mul, Pi.sub_apply, Pi.smul_apply
-- Module: Mathlib.LinearAlgebra.CrossProduct
Goal:
R : Type u_1
inst : CommRing R
u v w : Fin 3 → R
⊢ 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:
ring
-- Module: Mathlib.LinearAlgebra.DFinsupp
Goal:
ι : Type u_1
R : Type u_3
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 ι
φ ψ : (Π₀ (i : ι), M i) →ₗ[R] N
h :
  ∀ (i : ι) (x : M i),
    Eq.{u_6 + 1} (α := N) ((φ : (a : Π₀ (i : ι), M i) → N) (single (β := M) i x) : N)
      ((ψ : (a : Π₀ (i : ι), M i) → N) (single (β := M) i x) : N)
⊢ φ = ψ

Tactic:
LinearMap.toAddMonoidHom_injective <| addHom_ext h

Premises used: LinearMap.toAddMonoidHom_injective, DFinsupp.addHom_ext
-- Module: Mathlib.LinearAlgebra.DFinsupp
Goal:
ι : Type u_1
R : Type u_3
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 ι
φ ψ : (Π₀ (i : ι), M i) →ₗ[R] N
h : ∀ (i : ι), φ ∘ₗ lsingle (M := M) i = ψ ∘ₗ lsingle (M := M) i
⊢ φ = ψ

Tactic:
lhom_ext fun i => LinearMap.congr_fun (h i)

Premises used: LinearMap.congr_fun, DFinsupp.lhom_ext
-- Module: Mathlib.LinearAlgebra.DFinsupp
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 ι
s : Finset ι
x : (i : (↑(↑s : Set ι) : Type u_1)) → M (↑i : ι)
⊢ Eq (α := Π₀ (i : ι), M i)
    ((lmk (M := M) s : (a : (i : (↑(↑s : Set ι) : Type u_1)) → M (↑i : ι)) → Π₀ (i : ι), M i) x : Π₀ (i : ι), M i)
    (mk (β := M) s x : Π₀ (i : ι), M i)

Tactic:
rfl

Premises used: DFinsupp.mk, rfl
-- Module: Mathlib.LinearAlgebra.DFinsupp
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 : ι
x : M i
⊢ Eq (α := Π₀ (i : ι), M i) ((lsingle (M := M) i : (a : M i) → Π₀ (i : ι), M i) x : Π₀ (i : ι), M i)
    (single (β := M) i x : Π₀ (i : ι), M i)

Tactic:
rfl

Premises used: DFinsupp.single, rfl
-- Module: Mathlib.LinearAlgebra.DFinsupp
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)
i : ι
f : Π₀ (i : ι), M i
⊢ (lapply (M := M) i : (a : Π₀ (i : ι), M i) → M i) f = (f : (a : ι) → M a) i

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.DFinsupp
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)
⊢ Function.Injective (α := Π₀ (i : ι), M i) (β := (i : ι) → M i)
    (⇑(LinearMap.pi (φ := M) (lapply (M := M))) : (a : Π₀ (i : ι), M i) → (i : ι) → M i)

Tactic:
fun _ _ h ↦ ext fun _ ↦ congr_fun h _

Premises used: DFinsupp.ext, Function.Injective, congr_fun
-- Module: Mathlib.LinearAlgebra.DFinsupp
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 : ι
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)
⊢ Eq.{u_5 + 1} (α := M i →ₗ[R] M i) (lapply (M := M) i ∘ₗ lsingle (M := M) i) LinearMap.id

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.DFinsupp
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 : ι
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:
simp
-- Module: Mathlib.LinearAlgebra.DFinsupp
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'
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)
⊢ Eq.{u_5 + 1} (α := M i' →ₗ[R] M i) (lapply (M := M) i ∘ₗ lsingle (M := M) i') 0

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.DFinsupp
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'
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:
simp [h.symm]

Premises used: Ne.symm
-- Module: Mathlib.LinearAlgebra.DFinsupp
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
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
⊢ Equiv.toFun (equivCongrLeft (β := M) e) (x + x_1) =
    Equiv.toFun (equivCongrLeft (β := M) e) x + Equiv.toFun (equivCongrLeft (β := M) e) x_1

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.DFinsupp
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
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:
rfl
-- Module: Mathlib.LinearAlgebra.DFinsupp
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
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
⊢ 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)

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.DFinsupp
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
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:
rfl
-- Module: Mathlib.LinearAlgebra.DFinsupp
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))
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
⊢ __spread.0.toFun (x + x_1) = __spread.0.toFun x + __spread.0.toFun x_1

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.DFinsupp
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))
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:
rfl
-- Module: Mathlib.LinearAlgebra.DFinsupp
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))
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
⊢ __spread.0.toFun (x • x_1) = HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) x : R) (__spread.0.toFun x_1)

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.DFinsupp
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))
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:
rfl
-- Module: Mathlib.LinearAlgebra.DFinsupp
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
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
⊢ Equiv.toFun (equivFunOnFintype (β := M)) (x + x_1) =
    Equiv.toFun (equivFunOnFintype (β := M)) x + Equiv.toFun (equivFunOnFintype (β := M)) x_1

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.DFinsupp
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
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:
rfl
-- Module: Mathlib.LinearAlgebra.DFinsupp
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
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
⊢ Equiv.toFun (equivFunOnFintype (β := M)) (x • x_1) =
    HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) x : R) (Equiv.toFun (equivFunOnFintype (β := M)) x_1)

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.DFinsupp
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
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:
rfl
-- Module: Mathlib.LinearAlgebra.DFinsupp
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
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)
⊢ (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)

Tactic:
dsimp
-- Module: Mathlib.LinearAlgebra.DFinsupp
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)
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)
⊢ (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:
apply DFinsupp.induction f

Premises used: DFinsupp.induction