-- 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:
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[X]) (M'.map ⇑f')).det

Tactic:
refine sub_eq_zero.mp <| mem_nonZeroDivisors_iff.mp
  (pow_mem ?_ _) _ (det_det_aux k fun M ↦ ih _ _ <| by simp [← card])

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)).det ∈ 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 : ℕ
hl : l = Fintype.card m
⊢ (f M.det).det = ((comp m m n n R) (M.map ⇑f)).det

Tactic:
revert R S m

Result:
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

Proof state:
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

Tactic:
rw [eq_comm, Fintype.card_eq_zero_iff] at 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 : IsEmpty 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
⊢ (f M.det).det = ((comp m m n n R) (M.map ⇑f)).det

Tactic:
have : (f' M'.det).det = ((M'.map f').comp m m n n R[X]).det := by
  refine sub_eq_zero.mp <| mem_nonZeroDivisors_iff.mp
    (pow_mem ?_ _) _ (det_det_aux k fun M ↦ ih _ _ <| by simp [← card])
  rw [polyToMatrix_cornerAddX, ← charpoly]
  exact (Matrix.charpoly_monic _).mem_nonZeroDivisors

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
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

Proof state:
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 : IsEmpty m
⊢ (f M.det).det = ((comp m m n n R) (M.map ⇑f)).det

Tactic:
simp_rw [Matrix.det_isEmpty, _root_.map_one, det_one]

Result:
no goals

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
⊢ (f M.det).det = ((comp m m n n R) (M.map ⇑f)).det

Tactic:
have ⟨k⟩ := Fintype.card_pos_iff.mp (l.succ_pos.trans_eq card)

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 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
⊢ (-f (M k k)).charpoly ∈ nonZeroDivisors R[X]

Tactic:
exact (Matrix.charpoly_monic _).mem_nonZeroDivisors

Result:
no goals