awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
Goal:
n : Type u_1
p : Type u_2
R : Type u₂
inst : DecidableEq n
inst_1 : DecidableEq p
inst_2 : CommRing R
i j : n
hij : i ≠ j
c : R
⊢ (sumInl p { i := i, j := j, hij := hij, c := c : TransvectionStruct n R }).toMatrix =
    fromBlocks { i := i, j := j, hij := hij, c := c }.toMatrix 0 0 1
have mk : ∀ (a b : n ⊕ p),
  (sumInl p { i := i, j := j, hij := hij, c := c : TransvectionStruct n R }).toMatrix a b =
    fromBlocks { i := i, j := j, hij := hij, c := c : TransvectionStruct n R }.toMatrix 0 0 1 a b
Tactic: ext a b
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
Goal:
n : Type u_1
p : Type u_2
R : Type u₂
inst : DecidableEq n
inst_1 : DecidableEq p
inst_2 : CommRing R
i j : n
hij : i ≠ j
c : R
a b : n ⊕ p
⊢ (sumInl p { i := i, j := j, hij := hij, c := c : TransvectionStruct n R }).toMatrix a b =
    fromBlocks { i := i, j := j, hij := hij, c := c : TransvectionStruct n R }.toMatrix 0 0 1 a b
have mk : ∀ (a : n),
  (sumInl p { i := i, j := j, hij := hij, c := c : TransvectionStruct n R }).toMatrix (inl a) b =
    fromBlocks (o := p) { i := i, j := j, hij := hij, c := c : TransvectionStruct n R }.toMatrix 0 0 1 (inl a) b
Tactic: rcases a with a | a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
Goal:
n : Type u_1
p : Type u_2
R : Type u₂
inst : DecidableEq n
inst_1 : DecidableEq p
inst_2 : CommRing R
i j : n
hij : i ≠ j
c : R
a b : n ⊕ p
mk :
  ∀ (a : n),
    (sumInl p { i := i, j := j, hij := hij, c := c : TransvectionStruct n R }).toMatrix (inl a) b =
      fromBlocks (o := p) { i := i, j := j, hij := hij, c := c : TransvectionStruct n R }.toMatrix 0 0 1 (inl a) b
⊢ (sumInl p { i := i, j := j, hij := hij, c := c : TransvectionStruct n R }).toMatrix a b =
    fromBlocks { i := i, j := j, hij := hij, c := c : TransvectionStruct n R }.toMatrix 0 0 1 a b
have mk₁ : ∀ (a : p),
  (sumInl p { i := i, j := j, hij := hij, c := c : TransvectionStruct n R }).toMatrix (inr a) b =
    fromBlocks { i := i, j := j, hij := hij, c := c : TransvectionStruct n R }.toMatrix 0 0 1 (inr a) b
Tactic: rcases a with a | a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
Goal:
n : Type u_1
p : Type u_2
R : Type u₂
inst : DecidableEq n
inst_1 : DecidableEq p
inst_2 : CommRing R
i j : n
hij : i ≠ j
c : R
b : n ⊕ p
a : n
⊢ (sumInl p { i := i, j := j, hij := hij, c := c : TransvectionStruct n R }).toMatrix (inl a) b =
    fromBlocks (o := p) { i := i, j := j, hij := hij, c := c : TransvectionStruct n R }.toMatrix 0 0 1 (inl a) b
have mk : ∀ (b : n),
  (sumInl p { i := i, j := j, hij := hij, c := c : TransvectionStruct n R }).toMatrix (inl a) (inl b) =
    fromBlocks.{u_1, u_2, u_1, u_2, u₂} (m := p) (o := p)
      { i := i, j := j, hij := hij, c := c : TransvectionStruct n R }.toMatrix 0 0 1 (inl a) (inl b)
Tactic: rcases b with b | b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
Goal:
n : Type u_1
p : Type u_2
R : Type u₂
inst : DecidableEq n
inst_1 : DecidableEq p
inst_2 : CommRing R
i j : n
hij : i ≠ j
c : R
b : n ⊕ p
a : n
mk :
  ∀ (b : n),
    (sumInl p { i := i, j := j, hij := hij, c := c : TransvectionStruct n R }).toMatrix (inl a) (inl b) =
      fromBlocks.{u_1, u_2, u_1, u_2, u₂} (m := p) (o := p)
        { i := i, j := j, hij := hij, c := c : TransvectionStruct n R }.toMatrix 0 0 1 (inl a) (inl b)
⊢ (sumInl p { i := i, j := j, hij := hij, c := c : TransvectionStruct n R }).toMatrix (inl a) b =
    fromBlocks (o := p) { i := i, j := j, hij := hij, c := c : TransvectionStruct n R }.toMatrix 0 0 1 (inl a) b
have mk₁ : ∀ (b : p),
  (sumInl p { i := i, j := j, hij := hij, c := c : TransvectionStruct n R }).toMatrix (inl a) (inr b) =
    fromBlocks (o := p) { i := i, j := j, hij := hij, c := c : TransvectionStruct n R }.toMatrix 0 0 1 (inl a) (inr b)
Tactic: rcases b with b | b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
Goal:
n : Type u_1
p : Type u_2
R : Type u₂
inst : DecidableEq n
inst_1 : DecidableEq p
inst_2 : CommRing R
i j : n
hij : i ≠ j
c : R
b : n ⊕ p
a : p
⊢ (sumInl p { i := i, j := j, hij := hij, c := c : TransvectionStruct n R }).toMatrix (inr a) b =
    fromBlocks { i := i, j := j, hij := hij, c := c : TransvectionStruct n R }.toMatrix 0 0 1 (inr a) b
have mk : ∀ (b : n),
  (sumInl p { i := i, j := j, hij := hij, c := c : TransvectionStruct n R }).toMatrix (inr a) (inl b) =
    fromBlocks (m := p) { i := i, j := j, hij := hij, c := c : TransvectionStruct n R }.toMatrix 0 0 1 (inr a) (inl b)
Tactic: rcases b with b | b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
Goal:
n : Type u_1
p : Type u_2
R : Type u₂
inst : DecidableEq n
inst_1 : DecidableEq p
inst_2 : CommRing R
i j : n
hij : i ≠ j
c : R
b : n ⊕ p
a : p
mk :
  ∀ (b : n),
    (sumInl p { i := i, j := j, hij := hij, c := c : TransvectionStruct n R }).toMatrix (inr a) (inl b) =
      fromBlocks (m := p) { i := i, j := j, hij := hij, c := c : TransvectionStruct n R }.toMatrix 0 0 1 (inr a) (inl b)
⊢ (sumInl p { i := i, j := j, hij := hij, c := c : TransvectionStruct n R }).toMatrix (inr a) b =
    fromBlocks { i := i, j := j, hij := hij, c := c : TransvectionStruct n R }.toMatrix 0 0 1 (inr a) b
have mk₁ : ∀ (b : p),
  (sumInl p { i := i, j := j, hij := hij, c := c : TransvectionStruct n R }).toMatrix (inr a) (inr b) =
    fromBlocks { i := i, j := j, hij := hij, c := c : TransvectionStruct n R }.toMatrix 0 0 1 (inr a) (inr b)
Tactic: rcases b with b | b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
Goal:
n : Type u_1
p : Type u_2
R : Type u₂
inst : DecidableEq n
inst_1 : DecidableEq p
inst_2 : CommRing R
i j : n
hij : i ≠ j
c : R
a b : n
⊢ (sumInl p { i := i, j := j, hij := hij, c := c : TransvectionStruct n R }).toMatrix (inl a) (inl b) =
    fromBlocks.{u_1, u_2, u_1, u_2, u₂} (m := p) (o := p)
      { i := i, j := j, hij := hij, c := c : TransvectionStruct n R }.toMatrix 0 0 1 (inl a) (inl b)
have pos : ∀ (h : a = b),
  (sumInl p { i := i, j := j, hij := hij, c := c : TransvectionStruct n R }).toMatrix (inl a) (inl b) =
    fromBlocks.{u_1, u_2, u_1, u_2, u₂} (m := p) (o := p)
      { i := i, j := j, hij := hij, c := c : TransvectionStruct n R }.toMatrix 0 0 1 (inl a) (inl b)
Tactic: by_cases h : a = b
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
Goal:
n : Type u_1
p : Type u_2
R : Type u₂
inst : DecidableEq n
inst_1 : DecidableEq p
inst_2 : CommRing R
i j : n
hij : i ≠ j
c : R
a b : n
pos :
  ∀ (h : a = b),
    (sumInl p { i := i, j := j, hij := hij, c := c : TransvectionStruct n R }).toMatrix (inl a) (inl b) =
      fromBlocks.{u_1, u_2, u_1, u_2, u₂} (m := p) (o := p)
        { i := i, j := j, hij := hij, c := c : TransvectionStruct n R }.toMatrix 0 0 1 (inl a) (inl b)
⊢ (sumInl p { i := i, j := j, hij := hij, c := c : TransvectionStruct n R }).toMatrix (inl a) (inl b) =
    fromBlocks.{u_1, u_2, u_1, u_2, u₂} (m := p) (o := p)
      { i := i, j := j, hij := hij, c := c : TransvectionStruct n R }.toMatrix 0 0 1 (inl a) (inl b)
have neg : ∀ (h : ¬a = b),
  (sumInl p { i := i, j := j, hij := hij, c := c : TransvectionStruct n R }).toMatrix (inl a) (inl b) =
    fromBlocks.{u_1, u_2, u_1, u_2, u₂} (m := p) (o := p)
      { i := i, j := j, hij := hij, c := c : TransvectionStruct n R }.toMatrix 0 0 1 (inl a) (inl b)
Tactic: by_cases h : a = b
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
Goal:
n : Type u_1
p : Type u_2
R : Type u₂
inst : DecidableEq n
inst_1 : DecidableEq p
inst_2 : CommRing R
i j : n
hij : i ≠ j
c : R
a b : p
⊢ (sumInl p { i := i, j := j, hij := hij, c := c : TransvectionStruct n R }).toMatrix (inr a) (inr b) =
    fromBlocks { i := i, j := j, hij := hij, c := c : TransvectionStruct n R }.toMatrix 0 0 1 (inr a) (inr b)
have pos : ∀ (h : a = b),
  (sumInl p { i := i, j := j, hij := hij, c := c : TransvectionStruct n R }).toMatrix (inr a) (inr b) =
    fromBlocks { i := i, j := j, hij := hij, c := c : TransvectionStruct n R }.toMatrix 0 0 1 (inr a) (inr b)
Tactic: by_cases h : a = b
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
Goal:
n : Type u_1
p : Type u_2
R : Type u₂
inst : DecidableEq n
inst_1 : DecidableEq p
inst_2 : CommRing R
i j : n
hij : i ≠ j
c : R
a b : p
pos :
  ∀ (h : a = b),
    (sumInl p { i := i, j := j, hij := hij, c := c : TransvectionStruct n R }).toMatrix (inr a) (inr b) =
      fromBlocks { i := i, j := j, hij := hij, c := c : TransvectionStruct n R }.toMatrix 0 0 1 (inr a) (inr b)
⊢ (sumInl p { i := i, j := j, hij := hij, c := c : TransvectionStruct n R }).toMatrix (inr a) (inr b) =
    fromBlocks { i := i, j := j, hij := hij, c := c : TransvectionStruct n R }.toMatrix 0 0 1 (inr a) (inr b)
have neg : ∀ (h : ¬a = b),
  (sumInl p { i := i, j := j, hij := hij, c := c : TransvectionStruct n R }).toMatrix (inr a) (inr b) =
    fromBlocks { i := i, j := j, hij := hij, c := c : TransvectionStruct n R }.toMatrix 0 0 1 (inr a) (inr b)
Tactic: by_cases h : a = b
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
Goal:
n : Type u_1
p : Type u_2
R : Type u₂
inst : DecidableEq n
inst_1 : DecidableEq p
inst_2 : CommRing R
inst_3 : Fintype n
inst_4 : Fintype p
M : Matrix n n R
L : List (TransvectionStruct n R)
N : Matrix p p R
⊢ (List.map (toMatrix ∘ sumInl p) L).prod * fromBlocks M 0 0 N = fromBlocks ((List.map toMatrix L).prod * M) 0 0 N
have nil : List.prod (List.map (toMatrix ∘ sumInl p) []) * fromBlocks M 0 0 N =
  fromBlocks (List.prod (List.map toMatrix []) * M) 0 0 N
Tactic: induction L with
  | nil => simp
  | cons t L IH => simp [Matrix.mul_assoc, IH, toMatrix_sumInl, fromBlocks_multiply]
Cleared hypotheses: L
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
Goal:
n : Type u_1
p : Type u_2
R : Type u₂
inst : DecidableEq n
inst_1 : DecidableEq p
inst_2 : CommRing R
inst_3 : Fintype n
inst_4 : Fintype p
M : Matrix n n R
L : List (TransvectionStruct n R)
N : Matrix p p R
nil :
  List.prod (List.map (toMatrix ∘ sumInl p) []) * fromBlocks M 0 0 N =
    fromBlocks (List.prod (List.map toMatrix []) * M) 0 0 N
⊢ (List.map (toMatrix ∘ sumInl p) L).prod * fromBlocks M 0 0 N = fromBlocks ((List.map toMatrix L).prod * M) 0 0 N
have cons : ∀ (t : TransvectionStruct n R) (L : List (TransvectionStruct n R))
  (IH :
    (List.map (toMatrix ∘ sumInl p) L).prod * fromBlocks M 0 0 N = fromBlocks ((List.map toMatrix L).prod * M) 0 0 N),
  (List.map (toMatrix ∘ sumInl p) (t :: L)).prod * fromBlocks M 0 0 N =
    fromBlocks ((List.map toMatrix (t :: L)).prod * M) 0 0 N
Tactic: induction L with
  | nil => simp
  | cons t L IH => simp [Matrix.mul_assoc, IH, toMatrix_sumInl, fromBlocks_multiply]
Cleared hypotheses: L
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
Goal:
n : Type u_1
p : Type u_2
R : Type u₂
inst : DecidableEq n
inst_1 : DecidableEq p
inst_2 : CommRing R
inst_3 : Fintype n
inst_4 : Fintype p
M : Matrix n n R
L : List (TransvectionStruct n R)
N : Matrix p p R
⊢ fromBlocks M 0 0 N * (List.map (toMatrix ∘ sumInl p) L).prod = fromBlocks (M * (List.map toMatrix L).prod) 0 0 N
have nil : ∀ (M : Matrix n n R) (N : Matrix p p R),
  fromBlocks M 0 0 N * List.prod (List.map (toMatrix ∘ sumInl p) []) =
    fromBlocks (M * List.prod (List.map toMatrix [])) 0 0 N
Tactic: induction L generalizing M N with
  | nil => simp
  | cons t L IH => simp [IH, toMatrix_sumInl, fromBlocks_multiply]
Cleared hypotheses: M, L, N
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
Goal:
n : Type u_1
p : Type u_2
R : Type u₂
inst : DecidableEq n
inst_1 : DecidableEq p
inst_2 : CommRing R
inst_3 : Fintype n
inst_4 : Fintype p
M : Matrix n n R
L : List (TransvectionStruct n R)
N : Matrix p p R
nil :
  ∀ (M : Matrix n n R) (N : Matrix p p R),
    fromBlocks M 0 0 N * List.prod (List.map (toMatrix ∘ sumInl p) []) =
      fromBlocks (M * List.prod (List.map toMatrix [])) 0 0 N
⊢ fromBlocks M 0 0 N * (List.map (toMatrix ∘ sumInl p) L).prod = fromBlocks (M * (List.map toMatrix L).prod) 0 0 N
have cons : ∀ (t : TransvectionStruct n R) (L : List (TransvectionStruct n R))
  (IH :
    ∀ (M : Matrix n n R) (N : Matrix p p R),
      fromBlocks M 0 0 N * (List.map (toMatrix ∘ sumInl p) L).prod = fromBlocks (M * (List.map toMatrix L).prod) 0 0 N)
  (M : Matrix n n R) (N : Matrix p p R),
  fromBlocks M 0 0 N * (List.map (toMatrix ∘ sumInl p) (t :: L)).prod =
    fromBlocks (M * (List.map toMatrix (t :: L)).prod) 0 0 N
Tactic: induction L generalizing M N with
  | nil => simp
  | cons t L IH => simp [IH, toMatrix_sumInl, fromBlocks_multiply]
Cleared hypotheses: M, L, N
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
Goal:
n : Type u_1
p : Type u_2
R : Type u₂
inst : DecidableEq n
inst_1 : DecidableEq p
inst_2 : CommRing R
inst_3 : Fintype n
inst_4 : Fintype p
e : n ≃ p
t : TransvectionStruct n R
⊢ (reindexEquiv e t).toMatrix = (reindexAlgEquiv R R e : (a : Matrix n n R) → Matrix p p R) t.toMatrix
have rcases : ∀ (t_i t_j : n) (hij : t_i ≠ t_j) (c : R),
  (reindexEquiv e { i := t_i, j := t_j, hij := hij, c := c : TransvectionStruct n R }).toMatrix =
    (reindexAlgEquiv R R e : (a : Matrix n n R) → Matrix p p R) { i := t_i, j := t_j, hij := hij, c := c }.toMatrix
Tactic: rcases t with ⟨t_i, t_j, _⟩
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
Goal:
n : Type u_1
p : Type u_2
R : Type u₂
inst : DecidableEq n
inst_1 : DecidableEq p
inst_2 : CommRing R
inst_3 : Fintype n
inst_4 : Fintype p
e : n ≃ p
t_i t_j : n
hij : t_i ≠ t_j
c : R
⊢ (reindexEquiv e { i := t_i, j := t_j, hij := hij, c := c : TransvectionStruct n R }).toMatrix =
    (reindexAlgEquiv R R e : (a : Matrix n n R) → Matrix p p R) { i := t_i, j := t_j, hij := hij, c := c }.toMatrix
have a : ∀ (a b : p),
  (reindexEquiv e { i := t_i, j := t_j, hij := hij, c := c : TransvectionStruct n R }).toMatrix a b =
    (reindexAlgEquiv R R e : (a : Matrix n n R) → Matrix p p R) { i := t_i, j := t_j, hij := hij, c := c }.toMatrix a b
Tactic: ext a b
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
Goal:
n : Type u_1
p : Type u_2
R : Type u₂
inst : DecidableEq n
inst_1 : DecidableEq p
inst_2 : CommRing R
inst_3 : Fintype n
inst_4 : Fintype p
e : n ≃ p
t_i t_j : n
hij : t_i ≠ t_j
c : R
a b : p
⊢ (reindexEquiv e { i := t_i, j := t_j, hij := hij, c := c : TransvectionStruct n R }).toMatrix a b =
    (reindexAlgEquiv R R e : (a : Matrix n n R) → Matrix p p R) { i := t_i, j := t_j, hij := hij, c := c }.toMatrix a b
have a₁ : HAdd.hAdd (α := Matrix p p R) (β := Matrix p p R) 1
    (single ((e : (a : n) → p) t_i) ((e : (a : n) → p) t_j) c : Matrix p p R) a b =
  HAdd.hAdd (α := Matrix n n R) 1 (single t_i t_j c) ((e.symm : (a : p) → n) a) ((e.symm : (a : p) → n) b)
Tactic: simp only [reindexEquiv, transvection, toMatrix_mk,
    submatrix_apply, reindex_apply, reindexAlgEquiv_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
Goal:
n : Type u_1
p : Type u_2
R : Type u₂
inst : DecidableEq n
inst_1 : DecidableEq p
inst_2 : CommRing R
inst_3 : Fintype n
inst_4 : Fintype p
e : n ≃ p
t_i t_j : n
hij : t_i ≠ t_j
c : R
a b : p
⊢ HAdd.hAdd (α := Matrix p p R) (β := Matrix p p R) 1
      (single ((e : (a : n) → p) t_i) ((e : (a : n) → p) t_j) c : Matrix p p R) a b =
    HAdd.hAdd (α := Matrix n n R) 1 (single t_i t_j c) ((e.symm : (a : p) → n) a) ((e.symm : (a : p) → n) b)
have pos : ∀ (ha : (e : (a : n) → p) t_i = a),
  HAdd.hAdd (α := Matrix p p R) (β := Matrix p p R) 1
      (single ((e : (a : n) → p) t_i) ((e : (a : n) → p) t_j) c : Matrix p p R) a b =
    HAdd.hAdd (α := Matrix n n R) 1 (single t_i t_j c) ((e.symm : (a : p) → n) a) ((e.symm : (a : p) → n) b)
Tactic: by_cases ha : e t_i = a
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
Goal:
n : Type u_1
p : Type u_2
R : Type u₂
inst : DecidableEq n
inst_1 : DecidableEq p
inst_2 : CommRing R
inst_3 : Fintype n
inst_4 : Fintype p
e : n ≃ p
t_i t_j : n
hij : t_i ≠ t_j
c : R
a b : p
pos :
  ∀ (ha : (e : (a : n) → p) t_i = a),
    HAdd.hAdd (α := Matrix p p R) (β := Matrix p p R) 1
        (single ((e : (a : n) → p) t_i) ((e : (a : n) → p) t_j) c : Matrix p p R) a b =
      HAdd.hAdd (α := Matrix n n R) 1 (single t_i t_j c) ((e.symm : (a : p) → n) a) ((e.symm : (a : p) → n) b)
⊢ HAdd.hAdd (α := Matrix p p R) (β := Matrix p p R) 1
      (single ((e : (a : n) → p) t_i) ((e : (a : n) → p) t_j) c : Matrix p p R) a b =
    HAdd.hAdd (α := Matrix n n R) 1 (single t_i t_j c) ((e.symm : (a : p) → n) a) ((e.symm : (a : p) → n) b)
have neg : ∀ (ha : ¬(e : (a : n) → p) t_i = a),
  HAdd.hAdd (α := Matrix p p R) (β := Matrix p p R) 1
      (single ((e : (a : n) → p) t_i) ((e : (a : n) → p) t_j) c : Matrix p p R) a b =
    HAdd.hAdd (α := Matrix n n R) 1 (single t_i t_j c) ((e.symm : (a : p) → n) a) ((e.symm : (a : p) → n) b)
Tactic: by_cases ha : e t_i = a
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
Goal:
n : Type u_1
p : Type u_2
R : Type u₂
inst : DecidableEq n
inst_1 : DecidableEq p
inst_2 : CommRing R
inst_3 : Fintype n
inst_4 : Fintype p
e : n ≃ p
t_i t_j : n
hij : t_i ≠ t_j
c : R
a b : p
ha : (e : (a : n) → p) t_i = a
⊢ HAdd.hAdd (α := Matrix p p R) (β := Matrix p p R) 1
      (single ((e : (a : n) → p) t_i) ((e : (a : n) → p) t_j) c : Matrix p p R) a b =
    HAdd.hAdd (α := Matrix n n R) 1 (single t_i t_j c) ((e.symm : (a : p) → n) a) ((e.symm : (a : p) → n) b)
have pos : ∀ (hb : (e : (a : n) → p) t_j = b),
  HAdd.hAdd (α := Matrix p p R) (β := Matrix p p R) 1
      (single ((e : (a : n) → p) t_i) ((e : (a : n) → p) t_j) c : Matrix p p R) a b =
    HAdd.hAdd (α := Matrix n n R) 1 (single t_i t_j c) ((e.symm : (a : p) → n) a) ((e.symm : (a : p) → n) b)
Tactic: by_cases hb : e t_j = b
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
Goal:
n : Type u_1
p : Type u_2
R : Type u₂
inst : DecidableEq n
inst_1 : DecidableEq p
inst_2 : CommRing R
inst_3 : Fintype n
inst_4 : Fintype p
e : n ≃ p
t_i t_j : n
hij : t_i ≠ t_j
c : R
a b : p
ha : (e : (a : n) → p) t_i = a
pos :
  ∀ (hb : (e : (a : n) → p) t_j = b),
    HAdd.hAdd (α := Matrix p p R) (β := Matrix p p R) 1
        (single ((e : (a : n) → p) t_i) ((e : (a : n) → p) t_j) c : Matrix p p R) a b =
      HAdd.hAdd (α := Matrix n n R) 1 (single t_i t_j c) ((e.symm : (a : p) → n) a) ((e.symm : (a : p) → n) b)
⊢ HAdd.hAdd (α := Matrix p p R) (β := Matrix p p R) 1
      (single ((e : (a : n) → p) t_i) ((e : (a : n) → p) t_j) c : Matrix p p R) a b =
    HAdd.hAdd (α := Matrix n n R) 1 (single t_i t_j c) ((e.symm : (a : p) → n) a) ((e.symm : (a : p) → n) b)
have neg : ∀ (hb : ¬(e : (a : n) → p) t_j = b),
  HAdd.hAdd (α := Matrix p p R) (β := Matrix p p R) 1
      (single ((e : (a : n) → p) t_i) ((e : (a : n) → p) t_j) c : Matrix p p R) a b =
    HAdd.hAdd (α := Matrix n n R) 1 (single t_i t_j c) ((e.symm : (a : p) → n) a) ((e.symm : (a : p) → n) b)
Tactic: by_cases hb : e t_j = b
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
Goal:
n : Type u_1
p : Type u_2
R : Type u₂
inst : DecidableEq n
inst_1 : DecidableEq p
inst_2 : CommRing R
inst_3 : Fintype n
inst_4 : Fintype p
e : n ≃ p
t_i t_j : n
hij : t_i ≠ t_j
c : R
a b : p
ha : ¬(e : (a : n) → p) t_i = a
⊢ HAdd.hAdd (α := Matrix p p R) (β := Matrix p p R) 1
      (single ((e : (a : n) → p) t_i) ((e : (a : n) → p) t_j) c : Matrix p p R) a b =
    HAdd.hAdd (α := Matrix n n R) 1 (single t_i t_j c) ((e.symm : (a : p) → n) a) ((e.symm : (a : p) → n) b)
have pos : ∀ (hb : (e : (a : n) → p) t_j = b),
  HAdd.hAdd (α := Matrix p p R) (β := Matrix p p R) 1
      (single ((e : (a : n) → p) t_i) ((e : (a : n) → p) t_j) c : Matrix p p R) a b =
    HAdd.hAdd (α := Matrix n n R) 1 (single t_i t_j c) ((e.symm : (a : p) → n) a) ((e.symm : (a : p) → n) b)
Tactic: by_cases hb : e t_j = b
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
Goal:
n : Type u_1
p : Type u_2
R : Type u₂
inst : DecidableEq n
inst_1 : DecidableEq p
inst_2 : CommRing R
inst_3 : Fintype n
inst_4 : Fintype p
e : n ≃ p
t_i t_j : n
hij : t_i ≠ t_j
c : R
a b : p
ha : ¬(e : (a : n) → p) t_i = a
pos :
  ∀ (hb : (e : (a : n) → p) t_j = b),
    HAdd.hAdd (α := Matrix p p R) (β := Matrix p p R) 1
        (single ((e : (a : n) → p) t_i) ((e : (a : n) → p) t_j) c : Matrix p p R) a b =
      HAdd.hAdd (α := Matrix n n R) 1 (single t_i t_j c) ((e.symm : (a : p) → n) a) ((e.symm : (a : p) → n) b)
⊢ HAdd.hAdd (α := Matrix p p R) (β := Matrix p p R) 1
      (single ((e : (a : n) → p) t_i) ((e : (a : n) → p) t_j) c : Matrix p p R) a b =
    HAdd.hAdd (α := Matrix n n R) 1 (single t_i t_j c) ((e.symm : (a : p) → n) a) ((e.symm : (a : p) → n) b)
have neg : ∀ (hb : ¬(e : (a : n) → p) t_j = b),
  HAdd.hAdd (α := Matrix p p R) (β := Matrix p p R) 1
      (single ((e : (a : n) → p) t_i) ((e : (a : n) → p) t_j) c : Matrix p p R) a b =
    HAdd.hAdd (α := Matrix n n R) 1 (single t_i t_j c) ((e.symm : (a : p) → n) a) ((e.symm : (a : p) → n) b)
Tactic: by_cases hb : e t_j = b
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
Goal:
n : Type u_1
p : Type u_2
R : Type u₂
inst : DecidableEq n
inst_1 : DecidableEq p
inst_2 : CommRing R
inst_3 : Fintype n
inst_4 : Fintype p
e : n ≃ p
t_i t_j : n
hij : t_i ≠ t_j
c : R
a b : p
ha : (e : (a : n) → p) t_i = a
hb : (e : (a : n) → p) t_j = b
⊢ HAdd.hAdd (α := Matrix p p R) (β := Matrix p p R) 1
      (single ((e : (a : n) → p) t_i) ((e : (a : n) → p) t_j) c : Matrix p p R) a b =
    HAdd.hAdd (α := Matrix n n R) 1 (single t_i t_j c) ((e.symm : (a : p) → n) a) ((e.symm : (a : p) → n) b)
have pos : ∀ (hab : a = b),
  HAdd.hAdd (α := Matrix p p R) (β := Matrix p p R) 1
      (single ((e : (a : n) → p) t_i) ((e : (a : n) → p) t_j) c : Matrix p p R) a b =
    HAdd.hAdd (α := Matrix n n R) 1 (single t_i t_j c) ((e.symm : (a : p) → n) a) ((e.symm : (a : p) → n) b)
Tactic: by_cases hab : a = b
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
Goal:
n : Type u_1
p : Type u_2
R : Type u₂
inst : DecidableEq n
inst_1 : DecidableEq p
inst_2 : CommRing R
inst_3 : Fintype n
inst_4 : Fintype p
e : n ≃ p
t_i t_j : n
hij : t_i ≠ t_j
c : R
a b : p
ha : (e : (a : n) → p) t_i = a
hb : (e : (a : n) → p) t_j = b
pos :
  ∀ (hab : a = b),
    HAdd.hAdd (α := Matrix p p R) (β := Matrix p p R) 1
        (single ((e : (a : n) → p) t_i) ((e : (a : n) → p) t_j) c : Matrix p p R) a b =
      HAdd.hAdd (α := Matrix n n R) 1 (single t_i t_j c) ((e.symm : (a : p) → n) a) ((e.symm : (a : p) → n) b)
⊢ HAdd.hAdd (α := Matrix p p R) (β := Matrix p p R) 1
      (single ((e : (a : n) → p) t_i) ((e : (a : n) → p) t_j) c : Matrix p p R) a b =
    HAdd.hAdd (α := Matrix n n R) 1 (single t_i t_j c) ((e.symm : (a : p) → n) a) ((e.symm : (a : p) → n) b)
have neg : ∀ (hab : ¬a = b),
  HAdd.hAdd (α := Matrix p p R) (β := Matrix p p R) 1
      (single ((e : (a : n) → p) t_i) ((e : (a : n) → p) t_j) c : Matrix p p R) a b =
    HAdd.hAdd (α := Matrix n n R) 1 (single t_i t_j c) ((e.symm : (a : p) → n) a) ((e.symm : (a : p) → n) b)
Tactic: by_cases hab : a = b
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
Goal:
n : Type u_1
p : Type u_2
R : Type u₂
inst : DecidableEq n
inst_1 : DecidableEq p
inst_2 : CommRing R
inst_3 : Fintype n
inst_4 : Fintype p
e : n ≃ p
t_i t_j : n
hij : t_i ≠ t_j
c : R
a b : p
ha : (e : (a : n) → p) t_i = a
hb : ¬(e : (a : n) → p) t_j = b
⊢ HAdd.hAdd (α := Matrix p p R) (β := Matrix p p R) 1
      (single ((e : (a : n) → p) t_i) ((e : (a : n) → p) t_j) c : Matrix p p R) a b =
    HAdd.hAdd (α := Matrix n n R) 1 (single t_i t_j c) ((e.symm : (a : p) → n) a) ((e.symm : (a : p) → n) b)
have pos : ∀ (hab : a = b),
  HAdd.hAdd (α := Matrix p p R) (β := Matrix p p R) 1
      (single ((e : (a : n) → p) t_i) ((e : (a : n) → p) t_j) c : Matrix p p R) a b =
    HAdd.hAdd (α := Matrix n n R) 1 (single t_i t_j c) ((e.symm : (a : p) → n) a) ((e.symm : (a : p) → n) b)
Tactic: by_cases hab : a = b