-- Mathlib/RingTheory/Norm/Transitivity.lean
theorem Matrix.det_det [Fintype m] [Fintype n] (f : S →+* Matrix n n R) :
    (f M.det).det = ((M.map f).comp m m n n R).det

Proof state:
R : Type u_1
S : Type u_2
n : Type u_4
m : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
M : Matrix m m S
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : Fintype n
f : S →+* Matrix n n R
⊢ (f M.det).det = ((comp m m n n R) (M.map ⇑f)).det

Tactic:
set l := Fintype.card m with hl

Result:
R : Type u_1
S : Type u_2
n : Type u_4
m : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
M : Matrix m m S
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : Fintype n
f : S →+* Matrix n n R
l : ℕ := Fintype.card m
hl : l = Fintype.card m
⊢ (f M.det).det = ((comp m m n n R) (M.map ⇑f)).det

Proof state:
case succ
n : Type u_4
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
l : ℕ
ih :
  ∀ {R : Type u_1} {S : Type u_2} {m : Type u_5} [inst : CommRing R] [inst_1 : CommRing S] (M : Matrix m m S)
    [inst_2 : DecidableEq m] [inst_3 : Fintype m] (f : S →+* Matrix n n R),
    l = Fintype.card m → (f M.det).det = ((comp m m n n R) (M.map ⇑f)).det
R : Type u_1
S : Type u_2
m : Type u_5
inst✝³ : CommRing R
inst✝² : CommRing S
M : Matrix m m S
inst✝¹ : DecidableEq m
inst✝ : Fintype m
f : S →+* Matrix n n R
card : l + 1 = Fintype.card m
k : m
f' : S[X] →+* Matrix n n R[X] := f.polyToMatrix
⊢ (f M.det).det = ((comp m m n n R) (M.map ⇑f)).det

Tactic:
let M' := cornerAddX M k

Result:
case succ
n : Type u_4
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
l : ℕ
ih :
  ∀ {R : Type u_1} {S : Type u_2} {m : Type u_5} [inst : CommRing R] [inst_1 : CommRing S] (M : Matrix m m S)
    [inst_2 : DecidableEq m] [inst_3 : Fintype m] (f : S →+* Matrix n n R),
    l = Fintype.card m → (f M.det).det = ((comp m m n n R) (M.map ⇑f)).det
R : Type u_1
S : Type u_2
m : Type u_5
inst✝³ : CommRing R
inst✝² : CommRing S
M : Matrix m m S
inst✝¹ : DecidableEq m
inst✝ : Fintype m
f : S →+* Matrix n n R
card : l + 1 = Fintype.card m
k : m
f' : S[X] →+* Matrix n n R[X] := f.polyToMatrix
M' : Matrix m m S[X] := cornerAddX M k
⊢ (f M.det).det = ((comp m m n n R) (M.map ⇑f)).det

Proof state:
n : Type u_4
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
l : ℕ
ih :
  ∀ {R : Type u_1} {S : Type u_2} {m : Type u_5} [inst : CommRing R] [inst_1 : CommRing S] (M : Matrix m m S)
    [inst_2 : DecidableEq m] [inst_3 : Fintype m] (f : S →+* Matrix n n R),
    l = Fintype.card m → (f M.det).det = ((comp m m n n R) (M.map ⇑f)).det
R : Type u_1
S : Type u_2
m : Type u_5
inst✝³ : CommRing R
inst✝² : CommRing S
M✝ : Matrix m m S
inst✝¹ : DecidableEq m
inst✝ : Fintype m
f : S →+* Matrix n n R
card : l + 1 = Fintype.card m
k : m
f' : S[X] →+* Matrix n n R[X] := f.polyToMatrix
M' : Matrix m m S[X] := cornerAddX M✝ k
M : Matrix { a // (a = k) = False } { a // (a = k) = False } S[X]
⊢ l = Fintype.card { a // (a = k) = False }

Tactic:
simp [← card]

Result:
no goals

Proof state:
n : Type u_4
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
l : ℕ
ih :
  ∀ {R : Type u_1} {S : Type u_2} {m : Type u_5} [inst : CommRing R] [inst_1 : CommRing S] (M : Matrix m m S)
    [inst_2 : DecidableEq m] [inst_3 : Fintype m] (f : S →+* Matrix n n R),
    l = Fintype.card m → (f M.det).det = ((comp m m n n R) (M.map ⇑f)).det
R : Type u_1
S : Type u_2
m : Type u_5
inst✝³ : CommRing R
inst✝² : CommRing S
M : Matrix m m S
inst✝¹ : DecidableEq m
inst✝ : Fintype m
f : S →+* Matrix n n R
card : l + 1 = Fintype.card m
k : m
f' : S[X] →+* Matrix n n R[X] := f.polyToMatrix
M' : Matrix m m S[X] := cornerAddX M k
⊢ (f' (M' k k)).det ∈ nonZeroDivisors R[X]

Tactic:
rw [polyToMatrix_cornerAddX, ← charpoly]

Result:
n : Type u_4
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
l : ℕ
ih :
  ∀ {R : Type u_1} {S : Type u_2} {m : Type u_5} [inst : CommRing R] [inst_1 : CommRing S] (M : Matrix m m S)
    [inst_2 : DecidableEq m] [inst_3 : Fintype m] (f : S →+* Matrix n n R),
    l = Fintype.card m → (f M.det).det = ((comp m m n n R) (M.map ⇑f)).det
R : Type u_1
S : Type u_2
m : Type u_5
inst✝³ : CommRing R
inst✝² : CommRing S
M : Matrix m m S
inst✝¹ : DecidableEq m
inst✝ : Fintype m
f : S →+* Matrix n n R
card : l + 1 = Fintype.card m
k : m
f' : S[X] →+* Matrix n n R[X] := f.polyToMatrix
M' : Matrix m m S[X] := cornerAddX M k
⊢ (-f (M k k)).charpoly ∈ nonZeroDivisors R[X]

Proof state:
R : Type u_1
S : Type u_2
n : Type u_4
m : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
M : Matrix m m S
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : Fintype n
f : S →+* Matrix n n R
l : ℕ := Fintype.card m
hl : l = Fintype.card m
⊢ (f M.det).det = ((comp m m n n R) (M.map ⇑f)).det

Tactic:
clear_value l

Result:
R : Type u_1
S : Type u_2
n : Type u_4
m : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
M : Matrix m m S
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : Fintype n
f : S →+* Matrix n n R
l : ℕ
hl : l = Fintype.card m
⊢ (f M.det).det = ((comp m m n n R) (M.map ⇑f)).det

Proof state:
n : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Fintype n
l : ℕ
⊢ ∀ {R : Type u_1} {S : Type u_2} {m : Type u_5} [inst : CommRing R] [inst_1 : CommRing S] (M : Matrix m m S)
    [inst_2 : DecidableEq m] [inst_3 : Fintype m] (f : S →+* Matrix n n R),
    l = Fintype.card m → (f M.det).det = ((comp m m n n R) (M.map ⇑f)).det

Tactic:
induction' l with l ih <;> intro R S m _ _ M _ _ f card

Result:
case zero
n : Type u_4
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
R : Type u_1
S : Type u_2
m : Type u_5
inst✝³ : CommRing R
inst✝² : CommRing S
M : Matrix m m S
inst✝¹ : DecidableEq m
inst✝ : Fintype m
f : S →+* Matrix n n R
card : 0 = Fintype.card m
⊢ (f M.det).det = ((comp m m n n R) (M.map ⇑f)).det

case succ
n : Type u_4
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
l : ℕ
ih :
  ∀ {R : Type u_1} {S : Type u_2} {m : Type u_5} [inst : CommRing R] [inst_1 : CommRing S] (M : Matrix m m S)
    [inst_2 : DecidableEq m] [inst_3 : Fintype m] (f : S →+* Matrix n n R),
    l = Fintype.card m → (f M.det).det = ((comp m m n n R) (M.map ⇑f)).det
R : Type u_1
S : Type u_2
m : Type u_5
inst✝³ : CommRing R
inst✝² : CommRing S
M : Matrix m m S
inst✝¹ : DecidableEq m
inst✝ : Fintype m
f : S →+* Matrix n n R
card : l + 1 = Fintype.card m
⊢ (f M.det).det = ((comp m m n n R) (M.map ⇑f)).det

Proof state:
case succ
n : Type u_4
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
l : ℕ
ih :
  ∀ {R : Type u_1} {S : Type u_2} {m : Type u_5} [inst : CommRing R] [inst_1 : CommRing S] (M : Matrix m m S)
    [inst_2 : DecidableEq m] [inst_3 : Fintype m] (f : S →+* Matrix n n R),
    l = Fintype.card m → (f M.det).det = ((comp m m n n R) (M.map ⇑f)).det
R : Type u_1
S : Type u_2
m : Type u_5
inst✝³ : CommRing R
inst✝² : CommRing S
M : Matrix m m S
inst✝¹ : DecidableEq m
inst✝ : Fintype m
f : S →+* Matrix n n R
card : l + 1 = Fintype.card m
k : m
f' : S[X] →+* Matrix n n R[X] := f.polyToMatrix
M' : Matrix m m S[X] := cornerAddX M k
this : (f' M'.det).det = ((comp m m n n R[X]) (M'.map ⇑f')).det
⊢ (f M.det).det = ((comp m m n n R) (M.map ⇑f)).det

Tactic:
rw [← eval_zero_det_det, congr_arg (eval 0) this, eval_zero_comp_det]

Result:
no goals