awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Matrix.Basis (goal)
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_7
inst : DecidableEq l
inst_1 : DecidableEq m
inst_2 : DecidableEq n
inst_3 : DecidableEq o
inst_4 : Zero α
f : l ≃ n
g : m ≃ o
i : n
j : o
r : α
j' : m
hj : (g.symm : (a : o) → m) j ≠ j'
⊢ single i j r ((f : (a : l) → n) ((f.symm : (a : n) → l) i : l)) ((g : (a : m) → o) j') =
    single.{u_1, u_2, u_7} (m := l) ((f.symm : (a : n) → l) i : l) ((g.symm : (a : o) → m) j) r
      ((f.symm : (a : n) → l) i : l) j'
have a : j ≠ (g : (a : m) → o) j'
Tactic: rw [single_apply_of_col_ne _ _ hj, single_apply_of_col_ne]
-- Lean 4 proof step from Mathlib.Data.Matrix.Basis (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type u_7
inst : DecidableEq m
inst_1 : DecidableEq n
inst_2 : AddZeroClass α
i : m
j : n
a b : α
⊢ single i j (a + b) = single i j a + single i j b
have a₁ : ∀ (i_1 : m) (j_1 : n), single i j (a + b) i_1 j_1 = (single i j a + single i j b) i_1 j_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Matrix.Basis (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type u_7
inst : DecidableEq m
inst_1 : DecidableEq n
inst_2 : AddZeroClass α
i : m
j : n
a b : α
i_1 : m
j_1 : n
⊢ single i j (a + b) i_1 j_1 = (single i j a + single i j b) i_1 j_1
have a₁ : (if i = i_1 ∧ j = j_1 then a + b else 0) =
  HAdd.hAdd (α := Matrix m n α) (β := Matrix m n α)
    ((of : (a : m → n → α) → Matrix m n α) fun (i' : m) (j' : n) ↦ if i = i' ∧ j = j' then a else 0)
    ((of : (a : m → n → α) → Matrix m n α) fun (i' : m) (j' : n) ↦ if i = i' ∧ j = j' then b else 0) i_1 j_1
Tactic: simp only [single, of_apply]
-- Lean 4 proof step from Mathlib.Data.Matrix.Basis (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type u_7
inst : DecidableEq m
inst_1 : DecidableEq n
inst_2 : AddZeroClass α
i : m
j : n
a b : α
i_1 : m
j_1 : n
⊢ (if i = i_1 ∧ j = j_1 then a + b else 0) =
    HAdd.hAdd (α := Matrix m n α) (β := Matrix m n α)
      ((of : (a : m → n → α) → Matrix m n α) fun (i' : m) (j' : n) ↦ if i = i' ∧ j = j' then a else 0)
      ((of : (a : m → n → α) → Matrix m n α) fun (i' : m) (j' : n) ↦ if i = i' ∧ j = j' then b else 0) i_1 j_1
have pos : ∀ (h : i = i_1 ∧ j = j_1),
  a + b =
    HAdd.hAdd (α := Matrix m n α) (β := Matrix m n α)
      ((of : (a : m → n → α) → Matrix m n α) fun (i' : m) (j' : n) ↦ if i = i' ∧ j = j' then a else 0)
      ((of : (a : m → n → α) → Matrix m n α) fun (i' : m) (j' : n) ↦ if i = i' ∧ j = j' then b else 0) i_1 j_1
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.Matrix.Basis (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type u_7
inst : DecidableEq m
inst_1 : DecidableEq n
inst_2 : AddZeroClass α
i : m
j : n
a b : α
i_1 : m
j_1 : n
pos :
  ∀ (h : i = i_1 ∧ j = j_1),
    a + b =
      HAdd.hAdd (α := Matrix m n α) (β := Matrix m n α)
        ((of : (a : m → n → α) → Matrix m n α) fun (i' : m) (j' : n) ↦ if i = i' ∧ j = j' then a else 0)
        ((of : (a : m → n → α) → Matrix m n α) fun (i' : m) (j' : n) ↦ if i = i' ∧ j = j' then b else 0) i_1 j_1
⊢ (if i = i_1 ∧ j = j_1 then a + b else 0) =
    HAdd.hAdd (α := Matrix m n α) (β := Matrix m n α)
      ((of : (a : m → n → α) → Matrix m n α) fun (i' : m) (j' : n) ↦ if i = i' ∧ j = j' then a else 0)
      ((of : (a : m → n → α) → Matrix m n α) fun (i' : m) (j' : n) ↦ if i = i' ∧ j = j' then b else 0) i_1 j_1
have neg : ∀ (h : ¬(i = i_1 ∧ j = j_1)),
  0 =
    HAdd.hAdd (α := Matrix m n α) (β := Matrix m n α)
      ((of : (a : m → n → α) → Matrix m n α) fun (i' : m) (j' : n) ↦ if i = i' ∧ j = j' then a else 0)
      ((of : (a : m → n → α) → Matrix m n α) fun (i' : m) (j' : n) ↦ if i = i' ∧ j = j' then b else 0) i_1 j_1
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.Matrix.Basis (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type u_7
inst : DecidableEq m
inst_1 : DecidableEq n
inst_2 : NonUnitalNonAssocSemiring α
inst_3 : Fintype m
i : n
j : m
c : α
x : m → α
⊢ single i j c *ᵥ x = Function.update (β := fun (a : n) ↦ α) 0 i (c * x j)
have h : ∀ (i' : n), (single i j c *ᵥ x) i' = Function.update (β := fun (a : n) ↦ α) 0 i (c * x j) i'
Tactic: ext i'
-- Lean 4 proof step from Mathlib.Data.Matrix.Basis (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type u_7
inst : DecidableEq m
inst_1 : DecidableEq n
inst_2 : NonUnitalNonAssocSemiring α
inst_3 : Fintype m
i : n
j : m
c : α
x : m → α
i' : n
⊢ (single i j c *ᵥ x) i' = Function.update (β := fun (a : n) ↦ α) 0 i (c * x j) i'
have h : Eq.{u_7 + 1} (α := α) (∑ x_1 : m, if i = i' ∧ j = x_1 then c * x x_1 else 0 : α)
  (Function.update (β := fun (a : n) ↦ α) 0 i (c * x j) i' : α)
Tactic: simp only [mulVec, dotProduct, single, of_apply, ite_mul, zero_mul]
-- Lean 4 proof step from Mathlib.Data.Matrix.Basis (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type u_7
inst : DecidableEq m
inst_1 : DecidableEq n
inst_2 : NonUnitalNonAssocSemiring α
inst_3 : Fintype m
i : n
j : m
c : α
x : m → α
i' : n
⊢ Eq.{u_7 + 1} (α := α) (∑ x_1 : m, if i = i' ∧ j = x_1 then c * x x_1 else 0 : α)
    (Function.update (β := fun (a : n) ↦ α) 0 i (c * x j) i' : α)
have h : Eq.{u_7 + 1} (α := α) (∑ x_1 : m, if i = i ∧ j = x_1 then c * x x_1 else 0 : α)
  (Function.update (β := fun (a : n) ↦ α) 0 i (c * x j) i : α)
Tactic: rcases eq_or_ne i i' with rfl | h
Cleared hypotheses: i'
-- Lean 4 proof step from Mathlib.Data.Matrix.Basis (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type u_7
inst : DecidableEq m
inst_1 : DecidableEq n
inst_2 : NonUnitalNonAssocSemiring α
inst_3 : Fintype m
i : n
j : m
c : α
x : m → α
i' : n
h :
  Eq.{u_7 + 1} (α := α) (∑ x_1 : m, if i = i ∧ j = x_1 then c * x x_1 else 0 : α)
    (Function.update (β := fun (a : n) ↦ α) 0 i (c * x j) i : α)
⊢ Eq.{u_7 + 1} (α := α) (∑ x_1 : m, if i = i' ∧ j = x_1 then c * x x_1 else 0 : α)
    (Function.update (β := fun (a : n) ↦ α) 0 i (c * x j) i' : α)
have h₁ : ∀ (h : i ≠ i'),
  Eq.{u_7 + 1} (α := α) (∑ x_1 : m, if i = i' ∧ j = x_1 then c * x x_1 else 0 : α)
    (Function.update (β := fun (a : n) ↦ α) 0 i (c * x j) i' : α)
Tactic: rcases eq_or_ne i i' with rfl | h
-- Lean 4 proof step from Mathlib.Data.Matrix.Basis (goal)
Goal:
m : Type u_2
α : Type u_7
inst : DecidableEq m
inst_1 : AddCommMonoid α
inst_2 : Fintype m
f : m → α
⊢ ∑ i : m, single i i (f i) = diagonal f
have a : ∀ (j k : m), (∑ i : m, single i i (f i)) j k = diagonal f j k
Tactic: ext j k
-- Lean 4 proof step from Mathlib.Data.Matrix.Basis (goal)
Goal:
m : Type u_2
α : Type u_7
inst : DecidableEq m
inst_1 : AddCommMonoid α
inst_2 : Fintype m
f : m → α
j k : m
⊢ (∑ i : m, single i i (f i)) j k = diagonal f j k
have a : single j j (f j) j k = if j = k then f j else 0
Tactic: rw [sum_apply, diagonal_apply, Finset.sum_eq_single j]
-- Lean 4 proof step from Mathlib.Data.Matrix.Basis (goal)
Goal:
m : Type u_2
α : Type u_7
inst : DecidableEq m
inst_1 : AddCommMonoid α
inst_2 : Fintype m
f : m → α
j k : m
a : single j j (f j) j k = if j = k then f j else 0
⊢ (∑ i : m, single i i (f i)) j k = diagonal f j k
have a₁ : ∀ (b : m), Membership.mem (γ := Finset m) Finset.univ b → b ≠ j → single b b (f b) j k = 0
Tactic: rw [sum_apply, diagonal_apply, Finset.sum_eq_single j]
-- Lean 4 proof step from Mathlib.Data.Matrix.Basis (goal)
Goal:
m : Type u_2
α : Type u_7
inst : DecidableEq m
inst_1 : AddCommMonoid α
inst_2 : Fintype m
f : m → α
j k : m
a : single j j (f j) j k = if j = k then f j else 0
a₁ : ∀ (b : m), Membership.mem (γ := Finset m) Finset.univ b → b ≠ j → single b b (f b) j k = 0
⊢ (∑ i : m, single i i (f i)) j k = diagonal f j k
have a₂ : j ∉ Finset.univ → single j j (f j) j k = 0
Tactic: rw [sum_apply, diagonal_apply, Finset.sum_eq_single j]
-- Lean 4 proof step from Mathlib.Data.Matrix.Basis (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type u_7
inst : DecidableEq m
inst_1 : DecidableEq n
inst_2 : AddCommMonoid α
inst_3 : Fintype m
inst_4 : Fintype n
x : m → n → α
⊢ Eq (α := Matrix m n α) (∑ i : m, ∑ j : n, single i j (x i j) : Matrix m n α)
    ((of : (a : m → n → α) → Matrix m n α) x : Matrix m n α)
have a : ∀ (i : m) (j : n),
  Eq.{u_7 + 1} (α := α) ((∑ i : m, ∑ j : n, single i j (x i j)) i j : α)
    ((of : (a : m → n → α) → Matrix m n α) x i j : α)
Tactic: ext i j
-- Lean 4 proof step from Mathlib.Data.Matrix.Basis (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type u_7
inst : DecidableEq m
inst_1 : DecidableEq n
inst_2 : AddCommMonoid α
inst_3 : Fintype m
inst_4 : Fintype n
x : m → n → α
i : m
j : n
⊢ Eq.{u_7 + 1} (α := α) ((∑ i : m, ∑ j : n, single i j (x i j)) i j : α)
    ((of : (a : m → n → α) → Matrix m n α) x i j : α)
have a : Eq.{u_7 + 1} (α := α) ((∑ x_1 : m × n, single x_1.1 x_1.2 (x x_1.1 x_1.2)) i j : α)
  ((of : (a : m → n → α) → Matrix m n α) x i j : α)
Tactic: rw [← Fintype.sum_prod_type']
-- Lean 4 proof step from Mathlib.Data.Matrix.Basis (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type u_7
inst : DecidableEq m
inst_1 : DecidableEq n
inst_2 : AddCommMonoid α
inst_3 : Finite m
inst_4 : Finite n
P : Matrix m n α → Prop
M : Matrix m n α
h_zero : P 0
h_add : ∀ (p q : Matrix m n α), P p → P q → P (p + q)
h_std_basis : ∀ (i : m) (j : n) (x : α), P (single i j x)
⊢ P M
have intro : ∀ (val : Fintype m), P M
Tactic: cases nonempty_fintype m
-- Lean 4 proof step from Mathlib.Data.Matrix.Basis (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type u_7
inst : DecidableEq m
inst_1 : DecidableEq n
inst_2 : AddCommMonoid α
inst_3 : Finite m
inst_4 : Finite n
P : Matrix m n α → Prop
M : Matrix m n α
h_zero : P 0
h_add : ∀ (p q : Matrix m n α), P p → P q → P (p + q)
h_std_basis : ∀ (i : m) (j : n) (x : α), P (single i j x)
val : Fintype m
⊢ P M
have intro : ∀ (val : Fintype n), P M
Tactic: cases nonempty_fintype n
-- Lean 4 proof step from Mathlib.Data.Matrix.Basis (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type u_7
inst : DecidableEq m
inst_1 : DecidableEq n
inst_2 : AddCommMonoid α
inst_3 : Finite m
inst_4 : Finite n
P : Matrix m n α → Prop
M : Matrix m n α
h_zero : P 0
h_add : ∀ (p q : Matrix m n α), P p → P q → P (p + q)
h_std_basis : ∀ (i : m) (j : n) (x : α), P (single i j x)
val : Fintype m
val_1 : Fintype n
⊢ P M
have intro : P (∑ x ∈ SProd.sprod (α := Finset m) (β := Finset n) Finset.univ Finset.univ, single x.1 x.2 (M x.1 x.2))
Tactic: rw [matrix_eq_sum_single M, ← Finset.sum_product']
-- Lean 4 proof step from Mathlib.Data.Matrix.Basis (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type u_7
inst : DecidableEq m
inst_1 : DecidableEq n
inst_2 : AddCommMonoid α
inst_3 : Finite m
inst_4 : Finite n
P : Matrix m n α → Prop
M : Matrix m n α
h_zero : P 0
h_add : ∀ (p q : Matrix m n α), P p → P q → P (p + q)
h_std_basis : ∀ (i : m) (j : n) (x : α), P (single i j x)
val : Fintype m
val_1 : Fintype n
⊢ P (∑ x ∈ SProd.sprod (α := Finset m) (β := Finset n) Finset.univ Finset.univ, single x.1 x.2 (M x.1 x.2))
have intro : ∀ x ∈ SProd.sprod (α := Finset m) (β := Finset n) Finset.univ Finset.univ, P (single x.1 x.2 (M x.1 x.2))
Tactic: apply Finset.sum_induction _ _ h_add h_zero
-- Lean 4 proof step from Mathlib.Data.Matrix.Basis (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type u_7
inst : DecidableEq m
inst_1 : DecidableEq n
inst_2 : AddCommMonoid α
inst_3 : Finite m
inst_4 : Finite n
inst_5 : Nonempty m
inst_6 : Nonempty n
P : Matrix m n α → Prop
M : Matrix m n α
h_add : ∀ (p q : Matrix m n α), P p → P q → P (p + q)
h_std_basis : ∀ (i : m) (j : n) (x : α), P (single i j x)
⊢ P 0
have inhabit : ∀ (inhabited_h : Inhabited m), P 0
Tactic: inhabit m
-- Lean 4 proof step from Mathlib.Data.Matrix.Basis (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type u_7
inst : DecidableEq m
inst_1 : DecidableEq n
inst_2 : AddCommMonoid α
inst_3 : Finite m
inst_4 : Finite n
inst_5 : Nonempty m
inst_6 : Nonempty n
P : Matrix m n α → Prop
M : Matrix m n α
h_add : ∀ (p q : Matrix m n α), P p → P q → P (p + q)
h_std_basis : ∀ (i : m) (j : n) (x : α), P (single i j x)
inhabited_h : Inhabited m
⊢ P 0
have inhabit : ∀ (inhabited_h : Inhabited n), P 0
Tactic: inhabit n
-- Lean 4 proof step from Mathlib.Data.Matrix.Basis (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type u_7
β : Type u_8
inst : DecidableEq m
inst_1 : DecidableEq n
inst_2 : Finite m
inst_3 : Finite n
inst_4 : AddCommMonoid α
inst_5 : AddCommMonoid β
f g : Matrix m n α →+ β
h : ∀ (i : m) (j : n), f.comp (singleAddMonoidHom i j) = g.comp (singleAddMonoidHom i j)
⊢ f = g
have intro : ∀ (val : Fintype m), f = g
Tactic: cases nonempty_fintype m
-- Lean 4 proof step from Mathlib.Data.Matrix.Basis (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type u_7
β : Type u_8
inst : DecidableEq m
inst_1 : DecidableEq n
inst_2 : Finite m
inst_3 : Finite n
inst_4 : AddCommMonoid α
inst_5 : AddCommMonoid β
f g : Matrix m n α →+ β
h : ∀ (i : m) (j : n), f.comp (singleAddMonoidHom i j) = g.comp (singleAddMonoidHom i j)
val : Fintype m
⊢ f = g
have intro : ∀ (val : Fintype n), f = g
Tactic: cases nonempty_fintype n
-- Lean 4 proof step from Mathlib.Data.Matrix.Basis (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type u_7
β : Type u_8
inst : DecidableEq m
inst_1 : DecidableEq n
inst_2 : Finite m
inst_3 : Finite n
inst_4 : AddCommMonoid α
inst_5 : AddCommMonoid β
f g : Matrix m n α →+ β
h : ∀ (i : m) (j : n), f.comp (singleAddMonoidHom i j) = g.comp (singleAddMonoidHom i j)
val : Fintype m
val_1 : Fintype n
⊢ f = g
have intro : ∀ (x : Matrix m n α), Eq.{u_8 + 1} (α := β) ((f : (a : Matrix m n α) → β) x : β) ((g : (a : Matrix m n α) → β) x : β)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Data.Matrix.Basis (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type u_7
β : Type u_8
inst : DecidableEq m
inst_1 : DecidableEq n
inst_2 : Finite m
inst_3 : Finite n
inst_4 : AddCommMonoid α
inst_5 : AddCommMonoid β
f g : Matrix m n α →+ β
h : ∀ (i : m) (j : n), f.comp (singleAddMonoidHom i j) = g.comp (singleAddMonoidHom i j)
val : Fintype m
val_1 : Fintype n
x : Matrix m n α
⊢ Eq.{u_8 + 1} (α := β) ((f : (a : Matrix m n α) → β) x : β) ((g : (a : Matrix m n α) → β) x : β)
have intro : Eq.{u_8 + 1} (α := β) ((f : (a : Matrix m n α) → β) (∑ i : m, ∑ j : n, single i j (x i j)) : β)
  ((g : (a : Matrix m n α) → β) (∑ i : m, ∑ j : n, single i j (x i j)) : β)
Tactic: rw [matrix_eq_sum_single x]
-- Lean 4 proof step from Mathlib.Data.Matrix.Basis (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type u_7
β : Type u_8
inst : DecidableEq m
inst_1 : DecidableEq n
inst_2 : Finite m
inst_3 : Finite n
inst_4 : AddCommMonoid α
inst_5 : AddCommMonoid β
f g : Matrix m n α →+ β
h : ∀ (i : m) (j : n), f.comp (singleAddMonoidHom i j) = g.comp (singleAddMonoidHom i j)
val : Fintype m
val_1 : Fintype n
x : Matrix m n α
⊢ Eq.{u_8 + 1} (α := β) ((f : (a : Matrix m n α) → β) (∑ i : m, ∑ j : n, single i j (x i j)) : β)
    ((g : (a : Matrix m n α) → β) (∑ i : m, ∑ j : n, single i j (x i j)) : β)
have intro : Eq.{u_8 + 1} (α := β) (∑ x_1 : m, ∑ x_2 : n, (f : (a : Matrix m n α) → β) (single x_1 x_2 (x x_1 x_2)))
  (∑ x_1 : m, ∑ x_2 : n, (g : (a : Matrix m n α) → β) (single x_1 x_2 (x x_1 x_2)))
Tactic: simp_rw [map_sum]
-- Lean 4 proof step from Mathlib.Data.Matrix.Basis (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type u_7
β : Type u_8
inst : DecidableEq m
inst_1 : DecidableEq n
inst_2 : Finite m
inst_3 : Finite n
inst_4 : AddCommMonoid α
inst_5 : AddCommMonoid β
f g : Matrix m n α →+ β
h : ∀ (i : m) (j : n), f.comp (singleAddMonoidHom i j) = g.comp (singleAddMonoidHom i j)
val : Fintype m
val_1 : Fintype n
x : Matrix m n α
⊢ Eq.{u_8 + 1} (α := β) (∑ x_1 : m, ∑ x_2 : n, (f : (a : Matrix m n α) → β) (single x_1 x_2 (x x_1 x_2)))
    (∑ x_1 : m, ∑ x_2 : n, (g : (a : Matrix m n α) → β) (single x_1 x_2 (x x_1 x_2)))
have intro : ∀ (x_1 : m),
  Membership.mem (γ := Finset m) Finset.univ x_1 →
    ∀ (x_2 : n),
      Membership.mem (γ := Finset n) Finset.univ x_2 →
        Eq.{u_8 + 1} (α := β) ((f : (a : Matrix m n α) → β) (single x_1 x_2 (x x_1 x_2)) : β)
          ((g : (a : Matrix m n α) → β) (single x_1 x_2 (x x_1 x_2)) : β)
Tactic: congr! 2
-- Lean 4 proof step from Mathlib.Data.Matrix.Basis (goal)
Goal:
m : Type u_2
n : Type u_3
R : Type u_5
S : Type u_6
α : Type u_7
β : Type u_8
inst : DecidableEq m
inst_1 : DecidableEq n
inst_2 : Fintype m
inst_3 : Fintype n
inst_4 : Semiring R
inst_5 : Semiring S
inst_6 : AddCommMonoid α
inst_7 : AddCommMonoid β
inst_8 : Module R α
inst_9 : Module R β
inst_10 : Module S β
inst_11 : SMulCommClass R S β
f : m → n → α →ₗ[R] β
i : m
j : n
a : α
⊢ Eq.{u_8 + 1} (α := β)
    ((((liftLinear S : (a : m → n → α →ₗ[R] β) → Matrix m n α →ₗ[R] β) f : Matrix m n α →ₗ[R] β) :
          (a : Matrix m n α) → β)
        (single i j a) :
      β)
    ((f i j : (a : α) → β) a : β)
have dsimp : Eq.{u_8 + 1} (α := β)
  (((LinearMap.lsum R (fun (i : m) ↦ (i : n) → α) S :
            (a : (i : m) → ((i : n) → α) →ₗ[R] β) → ((i : m) → (i : n) → α) →ₗ[R] β)
          fun (i : m) ↦ (LinearMap.lsum R (fun (a : n) ↦ α) S : (a : n → α →ₗ[R] β) → ((i : n) → α) →ₗ[R] β) (f i) :
        (a : (i : m) → (i : n) → α) → β)
      ((Equiv.symm of : (a : Matrix m n α) → m → n → α) (single i j a) : m → n → α) :
    β)
  ((f i j : (a : α) → β) a : β)
Tactic: dsimp [liftLinear, -LinearMap.lsum_apply, LinearEquiv.congrLeft, LinearEquiv.piCongrRight]
-- Lean 4 proof step from Mathlib.Data.Matrix.Basis (goal)
Goal:
m : Type u_2
n : Type u_3
R : Type u_5
S : Type u_6
α : Type u_7
β : Type u_8
inst : DecidableEq m
inst_1 : DecidableEq n
inst_2 : Fintype m
inst_3 : Fintype n
inst_4 : Semiring R
inst_5 : Semiring S
inst_6 : AddCommMonoid α
inst_7 : AddCommMonoid β
inst_8 : Module R α
inst_9 : Module R β
inst_10 : Module S β
inst_11 : SMulCommClass R S β
f : m → n → α →ₗ[R] β
i : m
j : n
a : α
⊢ Eq.{u_8 + 1} (α := β)
    (((LinearMap.lsum R (fun (i : m) ↦ (i : n) → α) S :
              (a : (i : m) → ((i : n) → α) →ₗ[R] β) → ((i : m) → (i : n) → α) →ₗ[R] β)
            fun (i : m) ↦ (LinearMap.lsum R (fun (a : n) ↦ α) S : (a : n → α →ₗ[R] β) → ((i : n) → α) →ₗ[R] β) (f i) :
          (a : (i : m) → (i : n) → α) → β)
        ((Equiv.symm of : (a : Matrix m n α) → m → n → α) (single i j a) : m → n → α) :
      β)
    ((f i j : (a : α) → β) a : β)
have simp_rw : Eq.{u_8 + 1} (α := β)
  (((LinearMap.lsum R (fun (i : m) ↦ (i : n) → α) S :
            (a : (i : m) → ((i : n) → α) →ₗ[R] β) → ((i : m) → (i : n) → α) →ₗ[R] β)
          fun (i : m) ↦ (LinearMap.lsum R (fun (a : n) ↦ α) S : (a : n → α →ₗ[R] β) → ((i : n) → α) →ₗ[R] β) (f i) :
        (a : (i : m) → (i : n) → α) → β)
      (Pi.single (M := fun (j : m) ↦ n → α) i (Pi.single (M := fun (j : n) ↦ α) j a)) :
    β)
  ((f i j : (a : α) → β) a : β)
Tactic: simp_rw [of_symm_single, LinearMap.lsum_piSingle]
-- Lean 4 proof step from Mathlib.Data.Matrix.Basis (goal)
Goal:
n : Type u_3
α : Type u_7
inst : DecidableEq n
inst_1 : Zero α
i : n
c : α
⊢ (single i i c).diag = Pi.single (M := fun (j : n) ↦ α) i c
have h : ∀ (j : n), (single i i c).diag j = Pi.single (M := fun (j : n) ↦ α) i c j
Tactic: ext j
-- Lean 4 proof step from Mathlib.Data.Matrix.Basis (goal)
Goal:
n : Type u_3
α : Type u_7
inst : DecidableEq n
inst_1 : Zero α
i : n
c : α
j : n
⊢ (single i i c).diag j = Pi.single (M := fun (j : n) ↦ α) i c j
have pos : ∀ (hij : i = j), (single i i c).diag j = Pi.single (M := fun (j : n) ↦ α) i c j
Tactic: by_cases hij : i = j
-- Lean 4 proof step from Mathlib.Data.Matrix.Basis (goal)
Goal:
n : Type u_3
α : Type u_7
inst : DecidableEq n
inst_1 : Zero α
i : n
c : α
j : n
pos : ∀ (hij : i = j), (single i i c).diag j = Pi.single (M := fun (j : n) ↦ α) i c j
⊢ (single i i c).diag j = Pi.single (M := fun (j : n) ↦ α) i c j
have neg : ∀ (hij : ¬i = j), (single i i c).diag j = Pi.single (M := fun (j : n) ↦ α) i c j
Tactic: by_cases hij : i = j
-- Lean 4 proof step from Mathlib.Data.Matrix.Basis (goal)
Goal:
n : Type u_3
α : Type u_7
inst : DecidableEq n
inst_1 : Zero α
i : n
c : α
j : n
hij : i = j
⊢ (single i i c).diag j = Pi.single (M := fun (j : n) ↦ α) i c j
have pos : (single j j c).diag j = Pi.single (M := fun (j : n) ↦ α) j c j
Tactic: rw [hij]
-- Lean 4 proof step from Mathlib.Data.Matrix.Basis (goal)
Goal:
n : Type u_3
α : Type u_7
inst : DecidableEq n
inst_1 : Zero α
i : n
c : α
j : n
hij : i = j
⊢ (single i i c).diag j = Pi.single (M := fun (j : n) ↦ α) i c j
have pos : (single j j c).diag j = Pi.single (M := fun (j : n) ↦ α) j c j
Tactic: try rw [hij]
-- Lean 4 proof step from Mathlib.Data.Matrix.Basis (goal)
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_7
inst : DecidableEq l
inst_1 : DecidableEq m
inst_2 : DecidableEq n
inst_3 : Fintype m
inst_4 : NonUnitalNonAssocSemiring α
c : α
i : l
j : m
k : n
d : α
⊢ single i j c * single j k d = single i k (c * d)
have a : ∀ (a : l) (b : n), (single i j c * single j k d) a b = single i k (c * d) a b
Tactic: ext a b
-- Lean 4 proof step from Mathlib.Data.Matrix.Basis (goal)
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_7
inst : DecidableEq l
inst_1 : DecidableEq m
inst_2 : DecidableEq n
inst_3 : Fintype m
inst_4 : NonUnitalNonAssocSemiring α
c : α
i : l
j : m
k : n
d : α
a : l
b : n
⊢ (single i j c * single j k d) a b = single i k (c * d) a b
have a₁ : Eq.{u_7 + 1} (α := α)
  (∑ j_1 : m,
      HMul.hMul (α := α) (β := α)
        ((of : (a : l → m → α) → Matrix l m α) (fun (i' : l) (j' : m) ↦ if i = i' ∧ j = j' then c else 0) a j_1 : α)
        ((of : (a : m → n → α) → Matrix m n α) (fun (i' : m) (j' : n) ↦ if j = i' ∧ k = j' then d else 0) j_1 b : α) :
    α)
  ((of : (a : l → n → α) → Matrix l n α) (fun (i' : l) (j' : n) ↦ if i = i' ∧ k = j' then c * d else 0) a b : α)
Tactic: simp only [mul_apply, single]
-- Lean 4 proof step from Mathlib.Data.Matrix.Basis (goal)
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_7
inst : DecidableEq l
inst_1 : DecidableEq m
inst_2 : DecidableEq n
inst_3 : Fintype m
inst_4 : NonUnitalNonAssocSemiring α
c : α
i : l
j : m
k : n
d : α
a : l
b : n
⊢ Eq.{u_7 + 1} (α := α)
    (∑ j_1 : m,
        HMul.hMul (α := α) (β := α)
          ((of : (a : l → m → α) → Matrix l m α) (fun (i' : l) (j' : m) ↦ if i = i' ∧ j = j' then c else 0) a j_1 : α)
          ((of : (a : m → n → α) → Matrix m n α) (fun (i' : m) (j' : n) ↦ if j = i' ∧ k = j' then d else 0) j_1 b : α) :
      α)
    ((of : (a : l → n → α) → Matrix l n α) (fun (i' : l) (j' : n) ↦ if i = i' ∧ k = j' then c * d else 0) a b : α)
have pos : ∀ (h₁ : i = a),
  Eq.{u_7 + 1} (α := α)
    (∑ j_1 : m,
        HMul.hMul (α := α) (β := α)
          ((of : (a : l → m → α) → Matrix l m α) (fun (i' : l) (j' : m) ↦ if i = i' ∧ j = j' then c else 0) a j_1 : α)
          ((of : (a : m → n → α) → Matrix m n α) (fun (i' : m) (j' : n) ↦ if j = i' ∧ k = j' then d else 0) j_1 b : α) :
      α)
    ((of : (a : l → n → α) → Matrix l n α) (fun (i' : l) (j' : n) ↦ if i = i' ∧ k = j' then c * d else 0) a b : α)
Tactic: by_cases h₁ : i = a
-- Lean 4 proof step from Mathlib.Data.Matrix.Basis (goal)
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_7
inst : DecidableEq l
inst_1 : DecidableEq m
inst_2 : DecidableEq n
inst_3 : Fintype m
inst_4 : NonUnitalNonAssocSemiring α
c : α
i : l
j : m
k : n
d : α
a : l
b : n
pos :
  ∀ (h₁ : i = a),
    Eq.{u_7 + 1} (α := α)
      (∑ j_1 : m,
          HMul.hMul (α := α) (β := α)
            ((of : (a : l → m → α) → Matrix l m α) (fun (i' : l) (j' : m) ↦ if i = i' ∧ j = j' then c else 0) a j_1 : α)
            ((of : (a : m → n → α) → Matrix m n α) (fun (i' : m) (j' : n) ↦ if j = i' ∧ k = j' then d else 0) j_1 b :
              α) :
        α)
      ((of : (a : l → n → α) → Matrix l n α) (fun (i' : l) (j' : n) ↦ if i = i' ∧ k = j' then c * d else 0) a b : α)
⊢ Eq.{u_7 + 1} (α := α)
    (∑ j_1 : m,
        HMul.hMul (α := α) (β := α)
          ((of : (a : l → m → α) → Matrix l m α) (fun (i' : l) (j' : m) ↦ if i = i' ∧ j = j' then c else 0) a j_1 : α)
          ((of : (a : m → n → α) → Matrix m n α) (fun (i' : m) (j' : n) ↦ if j = i' ∧ k = j' then d else 0) j_1 b : α) :
      α)
    ((of : (a : l → n → α) → Matrix l n α) (fun (i' : l) (j' : n) ↦ if i = i' ∧ k = j' then c * d else 0) a b : α)
have neg : ∀ (h₁ : ¬i = a),
  Eq.{u_7 + 1} (α := α)
    (∑ j_1 : m,
        HMul.hMul (α := α) (β := α)
          ((of : (a : l → m → α) → Matrix l m α) (fun (i' : l) (j' : m) ↦ if i = i' ∧ j = j' then c else 0) a j_1 : α)
          ((of : (a : m → n → α) → Matrix m n α) (fun (i' : m) (j' : n) ↦ if j = i' ∧ k = j' then d else 0) j_1 b : α) :
      α)
    ((of : (a : l → n → α) → Matrix l n α) (fun (i' : l) (j' : n) ↦ if i = i' ∧ k = j' then c * d else 0) a b : α)
Tactic: by_cases h₁ : i = a