awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Matrix.Basic (goal)
Goal:
α : Type u_14
inst : MulOne α
inst_1 : AddCommMonoid α
h : IsStablyFiniteRing.{u_14} αᵐᵒᵖ
n : ℕ
x x_1 : Matrix (Fin n) (Fin n) α
⊢ OneHom.toFun { toFun := fun (M : Matrix (Fin n) (Fin n) α) ↦ M.map (op ∘ op), map_one' := ⋯ } (x * x_1) =
    HMul.hMul (α := Matrix (Fin n) (Fin n) αᵐᵒᵖᵐᵒᵖ)
      (OneHom.toFun
        { toFun := fun (M : Matrix (Fin n) (Fin n) α) ↦ M.map (op ∘ op), map_one' := ⋯ :
          OneHom (Matrix (Fin n) (Fin n) α) (Matrix (Fin n) (Fin n) αᵐᵒᵖᵐᵒᵖ) }
        x)
      (OneHom.toFun
        { toFun := fun (M : Matrix (Fin n) (Fin n) α) ↦ M.map (op ∘ op), map_one' := ⋯ :
          OneHom (Matrix (Fin n) (Fin n) α) (Matrix (Fin n) (Fin n) αᵐᵒᵖᵐᵒᵖ) }
        x_1)
have a : ∀ (i j : Fin n),
  OneHom.toFun { toFun := fun (M : Matrix (Fin n) (Fin n) α) ↦ M.map (op ∘ op), map_one' := sorry } (x * x_1) i j =
    HMul.hMul (α := Matrix (Fin n) (Fin n) αᵐᵒᵖᵐᵒᵖ) (β := Matrix (Fin n) (Fin n) αᵐᵒᵖᵐᵒᵖ)
      (OneHom.toFun
        { toFun := fun (M : Matrix (Fin n) (Fin n) α) ↦ M.map (op ∘ op), map_one' := sorry :
          OneHom (Matrix (Fin n) (Fin n) α) (Matrix (Fin n) (Fin n) αᵐᵒᵖᵐᵒᵖ) }
        x)
      (OneHom.toFun
        { toFun := fun (M : Matrix (Fin n) (Fin n) α) ↦ M.map (op ∘ op), map_one' := sorry :
          OneHom (Matrix (Fin n) (Fin n) α) (Matrix (Fin n) (Fin n) αᵐᵒᵖᵐᵒᵖ) }
        x_1)
      i j
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Matrix.Basic (goal)
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
T : Type u_9
A : Type u_10
α : Type u_11
β : Type u_12
γ : Type u_13
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : CommSemiring R
inst_3 : Semiring α
inst_4 : Semiring β
inst_5 : Semiring γ
inst_6 : Algebra R α
inst_7 : Algebra R β
inst_8 : Algebra R γ
x : R
⊢ Eq (α := Matrix m m α)
    (MulOpposite.unop
      (Equiv.toFun (RingEquiv.toEquiv RingEquiv.mopMatrix)
        ((algebraMap R (Matrix.{u_2, u_2, u_11} m m αᵐᵒᵖ) : (a : R) → Matrix m m αᵐᵒᵖ) x)))
    (MulOpposite.unop ((algebraMap R (Matrix m m α)ᵐᵒᵖ : (a : R) → (Matrix m m α)ᵐᵒᵖ) x))
have a : ∀ (i j : m),
  Eq.{u_11 + 1} (α := α)
    (MulOpposite.unop
        (Equiv.toFun (RingEquiv.toEquiv RingEquiv.mopMatrix)
          ((algebraMap R (Matrix.{u_2, u_2, u_11} m m αᵐᵒᵖ) : (a : R) → Matrix m m αᵐᵒᵖ) x))
        i j :
      α)
    (MulOpposite.unop ((algebraMap R (Matrix m m α)ᵐᵒᵖ : (a : R) → (Matrix m m α)ᵐᵒᵖ) x) i j : α)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Matrix.Basic (goal)
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
T : Type u_9
A : Type u_10
α : Type u_11
β_1 : Type u_12
γ : Type u_13
ι : Type u_14
β : ι → Type u_15
inst : (i : ι) → AddCommMonoid (β i)
inst_1 : (i : ι) → Mul (β i)
inst_2 : Fintype n
x x_1 : Matrix n n ((i : ι) → β i)
⊢ Equiv.toFun (AddEquiv.toEquiv (piAddEquiv (β := β))) (x * x_1) =
    Equiv.toFun (AddEquiv.toEquiv (piAddEquiv (β := β))) x * Equiv.toFun (AddEquiv.toEquiv (piAddEquiv (β := β))) x_1
have h : ∀ (x_2 : ι) (i j : n),
  Equiv.toFun (AddEquiv.toEquiv (piAddEquiv (β := β))) (x * x_1) x_2 i j =
    (Equiv.toFun (AddEquiv.toEquiv (piAddEquiv (β := β))) x * Equiv.toFun (AddEquiv.toEquiv (piAddEquiv (β := β))) x_1)
      x_2 i j
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Matrix.Basic (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type u_11
ι : Type u_14
inst : NonUnitalNonAssocSemiring α
inst_1 : Fintype n
s : Finset ι
x : ι → Matrix m n α
y : n → α
⊢ Eq (α := m → α) ((∑ i ∈ s, x i) *ᵥ y) (∑ i ∈ s, x i *ᵥ y)
have h : ∀ (x_1 : m), ((∑ i ∈ s, x i) *ᵥ y) x_1 = (∑ i ∈ s, x i *ᵥ y) x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Matrix.Basic (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type u_11
ι : Type u_14
inst : NonUnitalNonAssocSemiring α
inst_1 : Fintype n
s : Finset ι
x : ι → Matrix m n α
y : n → α
x_1 : m
⊢ ((∑ i ∈ s, x i) *ᵥ y) x_1 = (∑ i ∈ s, x i *ᵥ y) x_1
have h : Eq.{u_11 + 1} (α := α) (∑ x_2 : n, ∑ i ∈ s, x i x_1 x_2 * y x_2) (∑ x_2 ∈ s, ∑ x_3 : n, x x_2 x_1 x_3 * y x_3)
Tactic: simp only [mulVec, dotProduct, sum_apply, Finset.sum_mul, Finset.sum_apply]
-- Lean 4 proof step from Mathlib.Data.Matrix.Basic (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type u_11
ι : Type u_14
inst : NonUnitalNonAssocSemiring α
inst_1 : Fintype n
s : Finset ι
x : ι → Matrix m n α
y : n → α
x_1 : m
⊢ Eq.{u_11 + 1} (α := α) (∑ x_2 : n, ∑ i ∈ s, x i x_1 x_2 * y x_2) (∑ x_2 ∈ s, ∑ x_3 : n, x x_2 x_1 x_3 * y x_3)
have h : Eq.{u_11 + 1} (α := α) (∑ y_1 ∈ s, ∑ x_2 : n, x y_1 x_1 x_2 * y x_2) (∑ x_2 ∈ s, ∑ x_3 : n, x x_2 x_1 x_3 * y x_3)
Tactic: rw [Finset.sum_comm]
-- Lean 4 proof step from Mathlib.Data.Matrix.Basic (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type u_11
ι : Type u_14
inst : NonUnitalNonAssocSemiring α
inst_1 : Fintype n
x : Matrix m n α
s : Finset ι
y : ι → n → α
⊢ x *ᵥ ∑ i ∈ s, y i = ∑ i ∈ s, x *ᵥ y i
have h : ∀ (x_1 : m), (x *ᵥ ∑ i ∈ s, y i) x_1 = (∑ i ∈ s, x *ᵥ y i) x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Matrix.Basic (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type u_11
ι : Type u_14
inst : NonUnitalNonAssocSemiring α
inst_1 : Fintype n
s : Finset ι
x : ι → n → α
y : Matrix n m α
⊢ (∑ i ∈ s, x i) ᵥ* y = ∑ i ∈ s, x i ᵥ* y
have h : ∀ (x_1 : m), ((∑ i ∈ s, x i) ᵥ* y) x_1 = (∑ i ∈ s, x i ᵥ* y) x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Matrix.Basic (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type u_11
ι : Type u_14
inst : NonUnitalNonAssocSemiring α
inst_1 : Fintype n
x : n → α
s : Finset ι
y : ι → Matrix n m α
⊢ Eq (α := m → α) (x ᵥ* ∑ i ∈ s, y i) (∑ i ∈ s, x ᵥ* y i)
have h : ∀ (x_1 : m), (x ᵥ* ∑ i ∈ s, y i) x_1 = (∑ i ∈ s, x ᵥ* y i) x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Matrix.Basic (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type u_11
ι : Type u_14
inst : NonUnitalNonAssocSemiring α
inst_1 : Fintype n
x : n → α
s : Finset ι
y : ι → Matrix n m α
x_1 : m
⊢ (x ᵥ* ∑ i ∈ s, y i) x_1 = (∑ i ∈ s, x ᵥ* y i) x_1
have h : Eq.{u_11 + 1} (α := α) (∑ x_2 : n, ∑ i ∈ s, x x_2 * y i x_2 x_1) (∑ x_2 ∈ s, ∑ x_3 : n, x x_3 * y x_2 x_3 x_1)
Tactic: simp only [vecMul, dotProduct, sum_apply, Finset.mul_sum, Finset.sum_apply]
-- Lean 4 proof step from Mathlib.Data.Matrix.Basic (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type u_11
ι : Type u_14
inst : NonUnitalNonAssocSemiring α
inst_1 : Fintype n
x : n → α
s : Finset ι
y : ι → Matrix n m α
x_1 : m
⊢ Eq.{u_11 + 1} (α := α) (∑ x_2 : n, ∑ i ∈ s, x x_2 * y i x_2 x_1) (∑ x_2 ∈ s, ∑ x_3 : n, x x_3 * y x_2 x_3 x_1)
have h : Eq.{u_11 + 1} (α := α) (∑ y_1 ∈ s, ∑ x_2 : n, x x_2 * y y_1 x_2 x_1) (∑ x_2 ∈ s, ∑ x_3 : n, x x_3 * y x_2 x_3 x_1)
Tactic: rw [Finset.sum_comm]
-- 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 : Zero α
i : m
j : n
c : α
i' : m
j' : n
h : ¬(i = i' ∧ j = j')
⊢ single i j c i' j' = 0
have simp : i = i' → j = j' → c = 0
Tactic: simp only [single, and_imp, ite_eq_right_iff, 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 : Zero α
i : m
j : n
c : α
i' : m
j' : n
h : ¬(i = i' ∧ j = j')
⊢ i = i' → j = j' → c = 0
have inl : i = i' → ∀ (h : ¬i = i'), j = j' → c = 0
Tactic: tauto
Cleared hypotheses: 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 : Zero α
i : m
j : n
c : α
i' : m
j' : n
h : ¬(i = i' ∧ j = j')
inl : i = i' → ∀ (h : ¬i = i'), j = j' → c = 0
⊢ i = i' → j = j' → c = 0
have inr : i = i' → ∀ (h : ¬j = j'), j = j' → c = 0
Tactic: tauto
Cleared hypotheses: 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 : Zero α
i : m
j : n
a : α
⊢ single i j a =
    (of : (a : m → n → α) → Matrix m n α)
      (Pi.single (M := fun (a : m) ↦ n → α) i (Pi.single (M := fun (a : n) ↦ α) j a))
have a₁ : ∀ (a_1 : m) (b : n),
  single i j a a_1 b =
    (of : (a : m → n → α) → Matrix m n α)
      (Pi.single (M := fun (a : m) ↦ n → α) i (Pi.single (M := fun (a : n) ↦ α) j a)) a_1 b
Tactic: ext a b
-- 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 : Zero α
i : m
j : n
a_1 : α
a : m
b : n
⊢ single i j a_1 a b =
    (of : (a : m → n → α) → Matrix m n α)
      (Pi.single (M := fun (a : m) ↦ n → α) i (Pi.single (M := fun (a : n) ↦ α) j a_1)) a b
have a₁ : Eq.{u_7 + 1} (α := α)
  ((of : (a : m → n → α) → Matrix m n α) (fun (i' : m) (j' : n) ↦ if i = i' ∧ j = j' then a_1 else 0) a b : α)
  ((of : (a : m → n → α) → Matrix m n α)
      (Pi.single (M := fun (a : m) ↦ n → α) i (Pi.single (M := fun (a : n) ↦ α) j a_1)) a b :
    α)
Tactic: unfold single
-- 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 : Zero α
i : m
j : n
a_1 : α
a : m
b : n
⊢ Eq.{u_7 + 1} (α := α)
    ((of : (a : m → n → α) → Matrix m n α) (fun (i' : m) (j' : n) ↦ if i = i' ∧ j = j' then a_1 else 0) a b : α)
    ((of : (a : m → n → α) → Matrix m n α)
        (Pi.single (M := fun (a : m) ↦ n → α) i (Pi.single (M := fun (a : n) ↦ α) j a_1)) a b :
      α)
have pos : ∀ (hi : i = a),
  Eq.{u_7 + 1} (α := α)
    ((of : (a : m → n → α) → Matrix m n α) (fun (i' : m) (j' : n) ↦ if i = i' ∧ j = j' then a_1 else 0) a b : α)
    ((of : (a : m → n → α) → Matrix m n α)
        (Pi.single (M := fun (a : m) ↦ n → α) i (Pi.single (M := fun (a : n) ↦ α) j a_1)) a b :
      α)
Tactic: by_cases hi : i = a
-- 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 : Zero α
i : m
j : n
a_1 : α
a : m
b : n
pos :
  ∀ (hi : i = a),
    Eq.{u_7 + 1} (α := α)
      ((of : (a : m → n → α) → Matrix m n α) (fun (i' : m) (j' : n) ↦ if i = i' ∧ j = j' then a_1 else 0) a b : α)
      ((of : (a : m → n → α) → Matrix m n α)
          (Pi.single (M := fun (a : m) ↦ n → α) i (Pi.single (M := fun (a : n) ↦ α) j a_1)) a b :
        α)
⊢ Eq.{u_7 + 1} (α := α)
    ((of : (a : m → n → α) → Matrix m n α) (fun (i' : m) (j' : n) ↦ if i = i' ∧ j = j' then a_1 else 0) a b : α)
    ((of : (a : m → n → α) → Matrix m n α)
        (Pi.single (M := fun (a : m) ↦ n → α) i (Pi.single (M := fun (a : n) ↦ α) j a_1)) a b :
      α)
have neg : ∀ (hi : ¬i = a),
  Eq.{u_7 + 1} (α := α)
    ((of : (a : m → n → α) → Matrix m n α) (fun (i' : m) (j' : n) ↦ if i = i' ∧ j = j' then a_1 else 0) a b : α)
    ((of : (a : m → n → α) → Matrix m n α)
        (Pi.single (M := fun (a : m) ↦ n → α) i (Pi.single (M := fun (a : n) ↦ α) j a_1)) a b :
      α)
Tactic: by_cases hi : i = a
-- 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 : Zero α
i : m
j : n
a_1 : α
a : m
b : n
hi : i = a
⊢ Eq.{u_7 + 1} (α := α)
    ((of : (a : m → n → α) → Matrix m n α) (fun (i' : m) (j' : n) ↦ if i = i' ∧ j = j' then a_1 else 0) a b : α)
    ((of : (a : m → n → α) → Matrix m n α)
        (Pi.single (M := fun (a : m) ↦ n → α) i (Pi.single (M := fun (a : n) ↦ α) j a_1)) a b :
      α)
have pos : ∀ (hj : j = b),
  Eq.{u_7 + 1} (α := α)
    ((of : (a : m → n → α) → Matrix m n α) (fun (i' : m) (j' : n) ↦ if i = i' ∧ j = j' then a_1 else 0) a b : α)
    ((of : (a : m → n → α) → Matrix m n α)
        (Pi.single (M := fun (a : m) ↦ n → α) i (Pi.single (M := fun (a : n) ↦ α) j a_1)) a b :
      α)
Tactic: by_cases hj : j = b
-- 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 : Zero α
i : m
j : n
a_1 : α
a : m
b : n
hi : i = a
pos :
  ∀ (hj : j = b),
    Eq.{u_7 + 1} (α := α)
      ((of : (a : m → n → α) → Matrix m n α) (fun (i' : m) (j' : n) ↦ if i = i' ∧ j = j' then a_1 else 0) a b : α)
      ((of : (a : m → n → α) → Matrix m n α)
          (Pi.single (M := fun (a : m) ↦ n → α) i (Pi.single (M := fun (a : n) ↦ α) j a_1)) a b :
        α)
⊢ Eq.{u_7 + 1} (α := α)
    ((of : (a : m → n → α) → Matrix m n α) (fun (i' : m) (j' : n) ↦ if i = i' ∧ j = j' then a_1 else 0) a b : α)
    ((of : (a : m → n → α) → Matrix m n α)
        (Pi.single (M := fun (a : m) ↦ n → α) i (Pi.single (M := fun (a : n) ↦ α) j a_1)) a b :
      α)
have neg : ∀ (hj : ¬j = b),
  Eq.{u_7 + 1} (α := α)
    ((of : (a : m → n → α) → Matrix m n α) (fun (i' : m) (j' : n) ↦ if i = i' ∧ j = j' then a_1 else 0) a b : α)
    ((of : (a : m → n → α) → Matrix m n α)
        (Pi.single (M := fun (a : m) ↦ n → α) i (Pi.single (M := fun (a : n) ↦ α) j a_1)) a b :
      α)
Tactic: by_cases hj : j = b
-- 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 : Zero α
i : m
j : n
a_1 : α
a : m
b : n
hi : ¬i = a
⊢ Eq.{u_7 + 1} (α := α)
    ((of : (a : m → n → α) → Matrix m n α) (fun (i' : m) (j' : n) ↦ if i = i' ∧ j = j' then a_1 else 0) a b : α)
    ((of : (a : m → n → α) → Matrix m n α)
        (Pi.single (M := fun (a : m) ↦ n → α) i (Pi.single (M := fun (a : n) ↦ α) j a_1)) a b :
      α)
have pos : ∀ (hj : j = b),
  Eq.{u_7 + 1} (α := α)
    ((of : (a : m → n → α) → Matrix m n α) (fun (i' : m) (j' : n) ↦ if i = i' ∧ j = j' then a_1 else 0) a b : α)
    ((of : (a : m → n → α) → Matrix m n α)
        (Pi.single (M := fun (a : m) ↦ n → α) i (Pi.single (M := fun (a : n) ↦ α) j a_1)) a b :
      α)
Tactic: by_cases hj : j = b
-- 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 : Zero α
i : m
j : n
a_1 : α
a : m
b : n
hi : ¬i = a
pos :
  ∀ (hj : j = b),
    Eq.{u_7 + 1} (α := α)
      ((of : (a : m → n → α) → Matrix m n α) (fun (i' : m) (j' : n) ↦ if i = i' ∧ j = j' then a_1 else 0) a b : α)
      ((of : (a : m → n → α) → Matrix m n α)
          (Pi.single (M := fun (a : m) ↦ n → α) i (Pi.single (M := fun (a : n) ↦ α) j a_1)) a b :
        α)
⊢ Eq.{u_7 + 1} (α := α)
    ((of : (a : m → n → α) → Matrix m n α) (fun (i' : m) (j' : n) ↦ if i = i' ∧ j = j' then a_1 else 0) a b : α)
    ((of : (a : m → n → α) → Matrix m n α)
        (Pi.single (M := fun (a : m) ↦ n → α) i (Pi.single (M := fun (a : n) ↦ α) j a_1)) a b :
      α)
have neg : ∀ (hj : ¬j = b),
  Eq.{u_7 + 1} (α := α)
    ((of : (a : m → n → α) → Matrix m n α) (fun (i' : m) (j' : n) ↦ if i = i' ∧ j = j' then a_1 else 0) a b : α)
    ((of : (a : m → n → α) → Matrix m n α)
        (Pi.single (M := fun (a : m) ↦ n → α) i (Pi.single (M := fun (a : n) ↦ α) j a_1)) a b :
      α)
Tactic: by_cases hj : j = b
-- Lean 4 proof step from Mathlib.Data.Matrix.Basis (goal)
Goal:
m : Type u_2
n : Type u_3
R : Type u_5
α : Type u_7
inst : DecidableEq m
inst_1 : DecidableEq n
inst_2 : Zero α
inst_3 : SMulZeroClass R α
r : R
i : m
j : n
a : α
⊢ r • single i j a = single i j (r • a)
have unfold : HSMul.hSMul (β := Matrix m n α) r
    ((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 r • a else 0
Tactic: unfold single
-- Lean 4 proof step from Mathlib.Data.Matrix.Basis (goal)
Goal:
m : Type u_2
n : Type u_3
R : Type u_5
α : Type u_7
inst : DecidableEq m
inst_1 : DecidableEq n
inst_2 : Zero α
inst_3 : SMulZeroClass R α
r : R
i : m
j : n
a : α
⊢ HSMul.hSMul (β := Matrix m n α) r
      ((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 r • a else 0
have a₁ : ∀ (i_1 : m) (j_1 : n),
  HSMul.hSMul (β := Matrix m n α) r
      ((of : (a : m → n → α) → Matrix m n α) fun (i' : m) (j' : n) ↦ if i = i' ∧ j = j' then a else 0) i_1 j_1 =
    (of : (a : m → n → α) → Matrix m n α) (fun (i' : m) (j' : n) ↦ if i = i' ∧ j = j' then r • a else 0) 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 : Zero α
i : m
j : n
⊢ Eq (α := Matrix m n α)
    ((of : (a : m → n → α) → Matrix m n α) fun (i' : m) (j' : n) ↦ if i = i' ∧ j = j' then 0 else 0) 0
have a : ∀ (i_1 : m) (j_1 : n),
  Eq.{u_7 + 1} (α := α)
    ((of : (a : m → n → α) → Matrix m n α) (fun (i' : m) (j' : n) ↦ if i = i' ∧ j = j' then 0 else 0) i_1 j_1 : α)
    (0 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 : Zero α
S : Set α
hS : 0 ∈ S
i : m
j : n
a : α
⊢ Membership.mem (γ := Set (Matrix m n α)) S.matrix (single i j a) ↔ a ∈ S
have simp : (∀ (i_1 : m) (j_1 : n), (if i = i_1 ∧ j = j_1 then a else 0) ∈ S) ↔ a ∈ S
Tactic: simp only [Set.mem_matrix, 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 : Zero α
S : Set α
hS : 0 ∈ S
i : m
j : n
a : α
i_1 : m
j_1 : n
| (if i = i_1 ∧ j = j_1 then a else 0) ∈ S
have rw : (i = i_1 ∧ j = j_1 → a ∈ S) ∧ (¬(i = i_1 ∧ j = j_1) → 0 ∈ S)
Tactic: rw [ite_mem]
-- 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 : Zero α
S : Set α
hS : 0 ∈ S
i : m
j : n
a : α
⊢ (∀ (i_1 : m) (j_1 : n), (if i = i_1 ∧ j = j_1 then a else 0) ∈ S) ↔ a ∈ S
have conv_lhs : (∀ (i_1 : m) (j_1 : n), (i = i_1 ∧ j = j_1 → a ∈ S) ∧ (¬(i = i_1 ∧ j = j_1) → 0 ∈ S)) ↔ a ∈ S
Tactic: conv_lhs => intro _ _; rw [ite_mem]
-- Lean 4 proof step from Mathlib.Data.Matrix.Basis (goal)
Goal:
m : Type u_2
α : Type u_7
inst : DecidableEq m
inst_1 : Zero α
i : m
r : α
⊢ diagonal (Pi.single (M := fun (a : m) ↦ α) i r) = single i i r
have a : ∀ (j k : m), diagonal (Pi.single (M := fun (a : m) ↦ α) i r) j k = single i i r 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 : Zero α
i : m
r : α
j k : m
⊢ diagonal (Pi.single (M := fun (a : m) ↦ α) i r) j k = single i i r j k
have a : (if j = k then Pi.single (M := fun (a : m) ↦ α) i r j else 0) = if i = j ∧ i = k then r else 0
Tactic: dsimp [diagonal, single]
-- 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 : α
⊢ Eq (α := Matrix l m α) ((single i j r).submatrix (⇑f : (a : l) → n) (⇑g : (a : m) → o) : Matrix l m α)
    (single ((f.symm : (a : n) → l) i) ((g.symm : (a : o) → m) j) r : Matrix l m α)
have a : ∀ (i' : l) (j' : m),
  (single i j r).submatrix (⇑f : (a : l) → n) (⇑g : (a : m) → o) i' j' =
    single ((f.symm : (a : n) → l) i) ((g.symm : (a : o) → m) j) r i' j'
Tactic: ext i' j'
-- 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 : α
i' : l
j' : m
⊢ (single i j r).submatrix (⇑f : (a : l) → n) (⇑g : (a : m) → o) i' j' =
    single ((f.symm : (a : n) → l) i) ((g.symm : (a : o) → m) j) r i' j'
have a : single i j r ((f : (a : l) → n) i') ((g : (a : m) → o) j') =
  single ((f.symm : (a : n) → l) i) ((g.symm : (a : o) → m) j) r i' j'
Tactic: dsimp
-- 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 : α
i' : l
j' : m
⊢ single i j r ((f : (a : l) → n) i') ((g : (a : m) → o) j') =
    single ((f.symm : (a : n) → l) i) ((g.symm : (a : o) → m) j) r i' j'
have a : ∀ (hi : (f.symm : (a : n) → l) i ≠ i'),
  single i j r ((f : (a : l) → n) i') ((g : (a : m) → o) j') =
    single ((f.symm : (a : n) → l) i) ((g.symm : (a : o) → m) j) r i' j'
Tactic: obtain hi | rfl := ne_or_eq (f.symm i) i'
-- 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 : α
i' : l
j' : m
a :
  ∀ (hi : (f.symm : (a : n) → l) i ≠ i'),
    single i j r ((f : (a : l) → n) i') ((g : (a : m) → o) j') =
      single ((f.symm : (a : n) → l) i) ((g.symm : (a : o) → m) j) r i' j'
⊢ single i j r ((f : (a : l) → n) i') ((g : (a : m) → o) j') =
    single ((f.symm : (a : n) → l) i) ((g.symm : (a : o) → m) j) r i' j'
have a₁ : 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'
Tactic: obtain hi | rfl := ne_or_eq (f.symm i) i'
Cleared hypotheses: i'
-- 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 : α
i' : l
j' : m
hi : (f.symm : (a : n) → l) i ≠ i'
⊢ single i j r ((f : (a : l) → n) i') ((g : (a : m) → o) j') =
    single ((f.symm : (a : n) → l) i) ((g.symm : (a : o) → m) j) r i' j'
have a : i ≠ (f : (a : l) → n) i'
Tactic: rw [single_apply_of_row_ne hi, single_apply_of_row_ne]
-- 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
⊢ 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 : ∀ (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'
Tactic: obtain hj | rfl := ne_or_eq (g.symm j) j'
-- 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
a :
  ∀ (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'
⊢ 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₁ : single i j r ((f : (a : l) → n) ((f.symm : (a : n) → l) i : l)) ((g : (a : m) → o) ((g.symm : (a : o) → m) j : m)) =
  single.{u_1, u_2, u_7} (m := l) (n := m) ((f.symm : (a : n) → l) i : l) ((g.symm : (a : o) → m) j : m) r
    ((f.symm : (a : n) → l) i : l) ((g.symm : (a : o) → m) j : m)
Tactic: obtain hj | rfl := ne_or_eq (g.symm j) j'
Cleared hypotheses: j'