-- Mathlib/LinearAlgebra/Matrix/Transvection.lean
theorem updateRow_eq_transvection [Finite n] (c : R) :
    updateRow (1 : Matrix n n R) i ((1 : Matrix n n R) i + c • (1 : Matrix n n R) j) =
      transvection i j c

Proof state:
case intro
n : Type u_1
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : CommRing R
i j : n
inst✝ : Finite n
c : R
val✝ : Fintype n
⊢ updateRow 1 i (1 i + c • 1 j) = transvection i j c

Tactic:
ext a b

Result:
case intro.a
n : Type u_1
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : CommRing R
i j : n
inst✝ : Finite n
c : R
val✝ : Fintype n
a b : n
⊢ updateRow 1 i (1 i + c • 1 j) a b = transvection i j c a b

Proof state:
case pos
n : Type u_1
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : CommRing R
i j : n
inst✝ : Finite n
c : R
val✝ : Fintype n
a b : n
ha : i = a
⊢ updateRow 1 i (1 i + c • 1 j) a b = transvection i j c a b

Tactic:
by_cases hb : j = b

Result:
case pos
n : Type u_1
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : CommRing R
i j : n
inst✝ : Finite n
c : R
val✝ : Fintype n
a b : n
ha : i = a
hb : j = b
⊢ updateRow 1 i (1 i + c • 1 j) a b = transvection i j c a b

case neg
n : Type u_1
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : CommRing R
i j : n
inst✝ : Finite n
c : R
val✝ : Fintype n
a b : n
ha : i = a
hb : ¬j = b
⊢ updateRow 1 i (1 i + c • 1 j) a b = transvection i j c a b

Proof state:
case neg
n : Type u_1
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : CommRing R
i j : n
inst✝ : Finite n
c : R
val✝ : Fintype n
a b : n
ha : i = a
hb : ¬j = b
⊢ updateRow 1 i (1 i + c • 1 j) a b = transvection i j c a b

Tactic:
simp only [ha, updateRow_self, Pi.add_apply, one_apply, Pi.smul_apply, hb, ↓reduceIte,
  smul_eq_mul, mul_zero, add_zero, transvection, add_apply, and_false, not_false_eq_true,
  StdBasisMatrix.apply_of_ne]

Result:
no goals

Proof state:
n : Type u_1
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : CommRing R
i j : n
inst✝ : Finite n
c : R
⊢ updateRow 1 i (1 i + c • 1 j) = transvection i j c

Tactic:
cases nonempty_fintype n

Result:
case intro
n : Type u_1
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : CommRing R
i j : n
inst✝ : Finite n
c : R
val✝ : Fintype n
⊢ updateRow 1 i (1 i + c • 1 j) = transvection i j c

Proof state:
case pos
n : Type u_1
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : CommRing R
i j : n
inst✝ : Finite n
c : R
val✝ : Fintype n
a b : n
ha : i = a
hb : j = b
⊢ updateRow 1 i (1 i + c • 1 j) a b = transvection i j c a b

Tactic:
simp only [ha, updateRow_self, Pi.add_apply, one_apply, Pi.smul_apply, hb, ↓reduceIte,
  smul_eq_mul, mul_one, transvection, add_apply, StdBasisMatrix.apply_same]

Result:
no goals

Proof state:
case intro.a
n : Type u_1
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : CommRing R
i j : n
inst✝ : Finite n
c : R
val✝ : Fintype n
a b : n
⊢ updateRow 1 i (1 i + c • 1 j) a b = transvection i j c a b

Tactic:
by_cases ha : i = a

Result:
case pos
n : Type u_1
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : CommRing R
i j : n
inst✝ : Finite n
c : R
val✝ : Fintype n
a b : n
ha : i = a
⊢ updateRow 1 i (1 i + c • 1 j) a b = transvection i j c a b

case neg
n : Type u_1
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : CommRing R
i j : n
inst✝ : Finite n
c : R
val✝ : Fintype n
a b : n
ha : ¬i = a
⊢ updateRow 1 i (1 i + c • 1 j) a b = transvection i j c a b

Proof state:
case neg
n : Type u_1
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : CommRing R
i j : n
inst✝ : Finite n
c : R
val✝ : Fintype n
a b : n
ha : ¬i = a
⊢ updateRow 1 i (1 i + c • 1 j) a b = transvection i j c a b

Tactic:
simp only [updateRow_ne, transvection, ha, Ne.symm ha, StdBasisMatrix.apply_of_ne, add_zero,
  Algebra.id.smul_eq_mul, Ne, not_false_iff, DMatrix.add_apply, Pi.smul_apply,
  mul_zero, false_and, add_apply]

Result:
no goals