awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Norm.Transitivity
Goal:
R : Type u_1
S : Type u_2
n : Type u_4
m : Type u_5
inst : CommRing R
inst_1 : CommRing S
M : Matrix m m S
inst_2 : DecidableEq m
inst_3 : DecidableEq n
k : m
inst_4 : Fintype m
inst_5 : Fintype n
f : S →+* Matrix n n R
⊢ det (n := m × n)
        ((Matrix.comp m m n n R : (a : Matrix m m (Matrix n n R)) → Matrix (m × n) (m × n) R)
          (M.map (⇑f : (a : S) → Matrix n n R))) *
      HPow.hPow (α := R) (det.{u_1, u_4} (n := n) ((f : (a : S) → Matrix n n R) (M k k))) (Fintype.card m - 1) =
    det (n := m × n)
        ((Matrix.comp m m n n R : (a : Matrix m m (Matrix n n R)) → Matrix (m × n) (m × n) R)
          (M.map (⇑f : (a : S) → Matrix n n R))) *
      HMul.hMul (α := R)
        (det (n := Prod.{u_4, u_5} n { a : m // (a ≠ k) = True })
          (blockDiagonal fun (m : { a : m // (a ≠ k) = True }) ↦ (f : (a : S) → Matrix n n R) (M k k)))
        (det (n := Prod.{u_4, u_5} n { a : m // (a ≠ k) = False })
          (blockDiagonal fun (m : { a : m // (a ≠ k) = False }) ↦ (f : (a : S) → Matrix n n R) 1))

Tactic:
simp
-- Module: Mathlib.RingTheory.Norm.Transitivity
Goal:
R : Type u_1
S : Type u_2
n : Type u_4
m : Type u_5
inst : CommRing R
inst_1 : CommRing S
M : Matrix m m S
inst_2 : DecidableEq m
inst_3 : DecidableEq n
k : m
inst_4 : Fintype m
inst_5 : Fintype n
f : S →+* Matrix n n R
simp_rw :
  HMul.hMul (α := R)
      (det (n := Prod.{u_4, u_5} n { a : m // (a = k) = True })
        (blockDiagonal fun (m : { a : m // (a = k) = True }) ↦ (f : (a : S) → Matrix n n R) (M k k)))
      (det (n := Prod.{u_5, u_4} { a : m // (a = k) = False } n)
        ((Matrix.comp { a : m // (a = k) = False } { a : m // (a = k) = False } n n R :
            (a : Matrix { a : m // (a = k) = False } { a : m // (a = k) = False } (Matrix n n R)) →
              Matrix ({ a : m // (a = k) = False } × n) ({ a : m // (a = k) = False } × n) R)
          (Matrix.map ((M * auxMat M k).toSquareBlock (fun (x : m) ↦ x = k) False) (⇑f : (a : S) → Matrix n n R)))) =
    HMul.hMul (α := R) (det.{u_1, u_4} (n := n) ((f : (a : S) → Matrix n n R) (M k k)))
      (det (n := Prod.{u_5, u_4} { a : m // (a = k) = False } n)
        ((Matrix.comp { a : m // (a = k) = False } { a : m // (a = k) = False } n n R :
            (a : Matrix { a : m // (a = k) = False } { a : m // (a = k) = False } (Matrix n n R)) →
              Matrix ({ a : m // (a = k) = False } × n) ({ a : m // (a = k) = False } × n) R)
          (Matrix.map ((M * auxMat M k).toSquareBlock (fun (x : m) ↦ x = k) False) (⇑f : (a : S) → Matrix n n R))))
⊢ det (n := m × n)
      ((Matrix.comp m m n n R : (a : Matrix m m (Matrix n n R)) → Matrix (m × n) (m × n) R)
        ((M * auxMat M k).map (⇑f : (a : S) → Matrix n n R))) =
    HMul.hMul (α := R) (det.{u_1, u_4} (n := n) ((f : (a : S) → Matrix n n R) (M k k)))
      (det (n := Prod.{u_5, u_4} { a : m // (a = k) = False } n)
        ((Matrix.comp { a : m // (a = k) = False } { a : m // (a = k) = False } n n R :
            (a : Matrix { a : m // (a = k) = False } { a : m // (a = k) = False } (Matrix n n R)) →
              Matrix ({ a : m // (a = k) = False } × n) ({ a : m // (a = k) = False } × n) R)
          (Matrix.map ((M * auxMat M k).toSquareBlock (fun (x : m) ↦ x = k) False) (⇑f : (a : S) → Matrix n n R))))

Tactic:
simp_rw [((mul_auxMat_blockTriangular M k).map f).comp.det_fintype, Fintype.prod_Prop,
      comp_toSquareBlock (b := (· = k)), det_reindex_self, map_toSquareBlock,
      mul_auxMat_toSquareBlock_eq, smul_one_eq_diagonal,
      diagonal_map (map_zero _), comp_diagonal, det_reindex_self]

Premises used: Matrix.BlockTriangular.map, Matrix.smul_one_eq_diagonal, Matrix.map_toSquareBlock, map_zero, Matrix.comp_toSquareBlock, Matrix.BlockTriangular.comp, Algebra.Norm.Transitivity.mul_auxMat_blockTriangular, Matrix.det_reindex_self, Algebra.Norm.Transitivity.mul_auxMat_toSquareBlock_eq, Fintype.prod_Prop, Matrix.comp_diagonal, Matrix.diagonal_map, Matrix.BlockTriangular.det_fintype
-- Module: Mathlib.RingTheory.Norm.Transitivity
Goal:
R : Type u_1
S : Type u_2
n : Type u_4
m : Type u_5
inst : CommRing R
inst_1 : CommRing S
M : Matrix m m S
inst_2 : DecidableEq m
inst_3 : DecidableEq n
k : m
inst_4 : Fintype m
inst_5 : Fintype n
f : S →+* Matrix n n R
⊢ HMul.hMul (α := R)
      (det (n := Prod.{u_4, u_5} n { a : m // (a = k) = True })
        (blockDiagonal fun (m : { a : m // (a = k) = True }) ↦ (f : (a : S) → Matrix n n R) (M k k)))
      (det (n := Prod.{u_5, u_4} { a : m // (a = k) = False } n)
        ((Matrix.comp { a : m // (a = k) = False } { a : m // (a = k) = False } n n R :
            (a : Matrix { a : m // (a = k) = False } { a : m // (a = k) = False } (Matrix n n R)) →
              Matrix ({ a : m // (a = k) = False } × n) ({ a : m // (a = k) = False } × n) R)
          (Matrix.map ((M * auxMat M k).toSquareBlock (fun (x : m) ↦ x = k) False) (⇑f : (a : S) → Matrix n n R)))) =
    HMul.hMul (α := R) (det.{u_1, u_4} (n := n) ((f : (a : S) → Matrix n n R) (M k k)))
      (det (n := Prod.{u_5, u_4} { a : m // (a = k) = False } n)
        ((Matrix.comp { a : m // (a = k) = False } { a : m // (a = k) = False } n n R :
            (a : Matrix { a : m // (a = k) = False } { a : m // (a = k) = False } (Matrix n n R)) →
              Matrix ({ a : m // (a = k) = False } × n) ({ a : m // (a = k) = False } × n) R)
          (Matrix.map ((M * auxMat M k).toSquareBlock (fun (x : m) ↦ x = k) False) (⇑f : (a : S) → Matrix n n R))))

Tactic:
simp
-- Module: Mathlib.RingTheory.Norm.Transitivity
Goal:
n : Type u_4
inst : DecidableEq n
inst_1 : Fintype n
R : Type u_1
S : Type u_2
m : Type u_5
inst_2 : CommRing R
inst_3 : CommRing S
M : Matrix m m S
inst_4 : DecidableEq m
inst_5 : Fintype m
f : S →+* Matrix n n R
l : Fintype.card m = 0
⊢ IsEmpty m

Tactic:
rw [Fintype.card_eq_zero_iff] at l

Premises used: Fintype.card_eq_zero_iff
-- Module: Mathlib.RingTheory.Norm.Transitivity
Goal:
n : Type u_4
inst : DecidableEq n
inst_1 : Fintype n
R : Type u_1
S : Type u_2
m : Type u_5
inst_2 : CommRing R
inst_3 : CommRing S
M : Matrix m m S
inst_4 : DecidableEq m
inst_5 : Fintype m
f : S →+* Matrix n n R
l : IsEmpty m
zero : Eq.{u_1 + 1} (α := R) (det.{u_1, u_4} (n := n) ((f : (a : S) → Matrix n n R) 1)) 1
zero₁ : Eq.{u_1 + 1} (α := R) (det.{u_1, u_4} (n := n) 1) 1
⊢ Eq.{u_1 + 1} (α := R) (det.{u_1, u_4} (n := n) ((f : (a : S) → Matrix n n R) M.det))
    (det (n := m × n)
      ((comp m m n n R : (a : Matrix m m (Matrix n n R)) → Matrix (m × n) (m × n) R)
        (M.map (⇑f : (a : S) → Matrix n n R))))

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

Premises used: map_one, Matrix.det_one, Matrix.det_isEmpty
-- Module: Mathlib.RingTheory.Norm.Transitivity
Goal:
n : Type u_4
inst : DecidableEq n
inst_1 : Fintype n
l_1 : ℕ
ih :
  ∀ {R : Type u_1} {S : Type u_2} {m : Type u_5} [inst_6 : CommRing R] [inst_7 : CommRing S] (M : Matrix m m S)
    [inst_8 : DecidableEq m] [inst_9 : Fintype m] (f : S →+* Matrix n n R) (l : Fintype.card m = l_1),
    Eq.{u_1 + 1} (α := R) (det.{u_1, u_4} (n := n) ((f : (a : S) → Matrix n n R) M.det))
      (det (n := m × n)
        ((comp m m n n R : (a : Matrix m m (Matrix n n R)) → Matrix (m × n) (m × n) R)
          (M.map (⇑f : (a : S) → Matrix n n R))))
R : Type u_1
S : Type u_2
m : Type u_5
inst_2 : CommRing R
inst_3 : CommRing S
M : Matrix m m S
inst_4 : DecidableEq m
inst_5 : Fintype m
f : S →+* Matrix n n R
l : Fintype.card m = l_1 + 1
succ :
  ∀ (k : m),
    Eq.{u_1 + 1} (α := R) (det.{u_1, u_4} (n := n) ((f : (a : S) → Matrix n n R) M.det))
      (det (n := m × n)
        ((comp m m n n R : (a : Matrix m m (Matrix n n R)) → Matrix (m × n) (m × n) R)
          (M.map (⇑f : (a : S) → Matrix n n R))))
⊢ Eq.{u_1 + 1} (α := R) (det.{u_1, u_4} (n := n) ((f : (a : S) → Matrix n n R) M.det))
    (det (n := m × n)
      ((comp m m n n R : (a : Matrix m m (Matrix n n R)) → Matrix (m × n) (m × n) R)
        (M.map (⇑f : (a : S) → Matrix n n R))))

Tactic:
have ⟨k⟩ := Fintype.card_pos_iff.mp (Nat.lt_of_sub_eq_succ l)
-- Module: Mathlib.RingTheory.Norm.Transitivity
Goal:
n : Type u_4
inst : DecidableEq n
inst_1 : Fintype n
l_1 : ℕ
ih :
  ∀ {R : Type u_1} {S : Type u_2} {m : Type u_5} [inst_6 : CommRing R] [inst_7 : CommRing S] (M : Matrix m m S)
    [inst_8 : DecidableEq m] [inst_9 : Fintype m] (f : S →+* Matrix n n R) (l : Fintype.card m = l_1),
    Eq.{u_1 + 1} (α := R) (det.{u_1, u_4} (n := n) ((f : (a : S) → Matrix n n R) M.det))
      (det (n := m × n)
        ((comp m m n n R : (a : Matrix m m (Matrix n n R)) → Matrix (m × n) (m × n) R)
          (M.map (⇑f : (a : S) → Matrix n n R))))
R : Type u_1
S : Type u_2
m : Type u_5
inst_2 : CommRing R
inst_3 : CommRing S
M_1 : Matrix m m S
inst_4 : DecidableEq m
inst_5 : Fintype m
f : S →+* Matrix n n R
l : Fintype.card m = l_1 + 1
k : m
f' : S[X] →+* Matrix.{u_4, u_4, u_1} n n R[X] := f.polyToMatrix
M' : Matrix.{u_5, u_5, u_2} m m S[X] := cornerAddX M_1 k
M : Matrix.{u_5, u_5, u_2} { a : m // (a = k) = False } { a : m // (a = k) = False } S[X]
⊢ Fintype.card.{u_5} { a : m // (a = k) = False } = l_1

Tactic:
grind [Fintype.card_subtype_compl, Fintype.card_unique]

Premises used: Fintype.card_unique, Fintype.card_subtype_compl
-- Module: Mathlib.RingTheory.Norm.Transitivity
Goal:
n : Type u_4
inst : DecidableEq n
inst_1 : Fintype n
l_1 : ℕ
ih :
  ∀ {R : Type u_1} {S : Type u_2} {m : Type u_5} [inst_6 : CommRing R] [inst_7 : CommRing S] (M : Matrix m m S)
    [inst_8 : DecidableEq m] [inst_9 : Fintype m] (f : S →+* Matrix n n R) (l : Fintype.card m = l_1),
    Eq.{u_1 + 1} (α := R) (det.{u_1, u_4} (n := n) ((f : (a : S) → Matrix n n R) M.det))
      (det (n := m × n)
        ((comp m m n n R : (a : Matrix m m (Matrix n n R)) → Matrix (m × n) (m × n) R)
          (M.map (⇑f : (a : S) → Matrix n n R))))
R : Type u_1
S : Type u_2
m : Type u_5
inst_2 : CommRing R
inst_3 : CommRing S
M : Matrix m m S
inst_4 : DecidableEq m
inst_5 : Fintype m
f : S →+* Matrix n n R
l : Fintype.card m = l_1 + 1
k : m
f' : S[X] →+* Matrix.{u_4, u_4, u_1} n n R[X] := f.polyToMatrix
M' : Matrix.{u_5, u_5, u_2} m m S[X] := cornerAddX M k
refine :
  Membership.mem (γ := Submonoid R[X]) (nonZeroDivisors R[X])
    (det.{u_1, u_4} (n := n) ((f' : (a : S[X]) → Matrix n n R[X]) (M' k k)))
⊢ Eq.{u_1 + 1} (α := R[X]) (det.{u_1, u_4} (n := n) ((f' : (a : S[X]) → Matrix n n R[X]) M'.det))
    (det (n := m × n)
      ((comp m m n n R[X] : (a : Matrix m m (Matrix n n R[X])) → Matrix (m × n) (m × n) R[X])
        (M'.map (⇑f' : (a : S[X]) → Matrix n n R[X]))))

Tactic:
refine sub_eq_zero.mp <| mem_nonZeroDivisors_iff_right.mp
        (pow_mem ?_ _) _ (det_det_aux k fun M ↦ ih _ _ <| by
          grind [Fintype.card_subtype_compl, Fintype.card_unique])

Premises used: sub_eq_zero, mem_nonZeroDivisors_iff_right, pow_mem, Iff.mp
-- Module: Mathlib.RingTheory.Norm.Transitivity
Goal:
n : Type u_4
inst : DecidableEq n
inst_1 : Fintype n
l_1 : ℕ
ih :
  ∀ {R : Type u_1} {S : Type u_2} {m : Type u_5} [inst_6 : CommRing R] [inst_7 : CommRing S] (M : Matrix m m S)
    [inst_8 : DecidableEq m] [inst_9 : Fintype m] (f : S →+* Matrix n n R) (l : Fintype.card m = l_1),
    Eq.{u_1 + 1} (α := R) (det.{u_1, u_4} (n := n) ((f : (a : S) → Matrix n n R) M.det))
      (det (n := m × n)
        ((comp m m n n R : (a : Matrix m m (Matrix n n R)) → Matrix (m × n) (m × n) R)
          (M.map (⇑f : (a : S) → Matrix n n R))))
R : Type u_1
S : Type u_2
m : Type u_5
inst_2 : CommRing R
inst_3 : CommRing S
M : Matrix m m S
inst_4 : DecidableEq m
inst_5 : Fintype m
f : S →+* Matrix n n R
l : Fintype.card m = l_1 + 1
k : m
f' : S[X] →+* Matrix.{u_4, u_4, u_1} n n R[X] := f.polyToMatrix
M' : Matrix.{u_5, u_5, u_2} m m S[X] := cornerAddX M k
rw :
  Membership.mem (γ := Submonoid R[X]) (nonZeroDivisors R[X])
    (charpoly.{u_1, u_4} (n := n) (-(f : (a : S) → Matrix n n R) (M k k)))
⊢ Membership.mem (γ := Submonoid R[X]) (nonZeroDivisors R[X])
    (det.{u_1, u_4} (n := n) ((f' : (a : S[X]) → Matrix n n R[X]) (M' k k)))

Tactic:
rw [polyToMatrix_cornerAddX, ← charpoly]

Premises used: Algebra.Norm.Transitivity.polyToMatrix_cornerAddX, Matrix.charpoly
-- Module: Mathlib.RingTheory.Norm.Transitivity
Goal:
n : Type u_4
inst : DecidableEq n
inst_1 : Fintype n
l_1 : ℕ
ih :
  ∀ {R : Type u_1} {S : Type u_2} {m : Type u_5} [inst_6 : CommRing R] [inst_7 : CommRing S] (M : Matrix m m S)
    [inst_8 : DecidableEq m] [inst_9 : Fintype m] (f : S →+* Matrix n n R) (l : Fintype.card m = l_1),
    Eq.{u_1 + 1} (α := R) (det.{u_1, u_4} (n := n) ((f : (a : S) → Matrix n n R) M.det))
      (det (n := m × n)
        ((comp m m n n R : (a : Matrix m m (Matrix n n R)) → Matrix (m × n) (m × n) R)
          (M.map (⇑f : (a : S) → Matrix n n R))))
R : Type u_1
S : Type u_2
m : Type u_5
inst_2 : CommRing R
inst_3 : CommRing S
M : Matrix m m S
inst_4 : DecidableEq m
inst_5 : Fintype m
f : S →+* Matrix n n R
l : Fintype.card m = l_1 + 1
k : m
f' : S[X] →+* Matrix.{u_4, u_4, u_1} n n R[X] := f.polyToMatrix
M' : Matrix.{u_5, u_5, u_2} m m S[X] := cornerAddX M k
⊢ Membership.mem (γ := Submonoid R[X]) (nonZeroDivisors R[X])
    (charpoly.{u_1, u_4} (n := n) (-(f : (a : S) → Matrix n n R) (M k k)))

Tactic:
(Matrix.charpoly_monic _).mem_nonZeroDivisors

Premises used: Set.Mem, setOf, Polynomial.Monic.mem_nonZeroDivisors, Matrix.charpoly_monic
-- Module: Mathlib.RingTheory.Norm.Transitivity
Goal:
n : Type u_4
inst : DecidableEq n
inst_1 : Fintype n
l_1 : ℕ
ih :
  ∀ {R : Type u_1} {S : Type u_2} {m : Type u_5} [inst_6 : CommRing R] [inst_7 : CommRing S] (M : Matrix m m S)
    [inst_8 : DecidableEq m] [inst_9 : Fintype m] (f : S →+* Matrix n n R) (l : Fintype.card m = l_1),
    Eq.{u_1 + 1} (α := R) (det.{u_1, u_4} (n := n) ((f : (a : S) → Matrix n n R) M.det))
      (det (n := m × n)
        ((comp m m n n R : (a : Matrix m m (Matrix n n R)) → Matrix (m × n) (m × n) R)
          (M.map (⇑f : (a : S) → Matrix n n R))))
R : Type u_1
S : Type u_2
m : Type u_5
inst_2 : CommRing R
inst_3 : CommRing S
M : Matrix m m S
inst_4 : DecidableEq m
inst_5 : Fintype m
f : S →+* Matrix n n R
l : Fintype.card m = l_1 + 1
k : m
f' : S[X] →+* Matrix.{u_4, u_4, u_1} n n R[X] := f.polyToMatrix
M' : Matrix.{u_5, u_5, u_2} m m S[X] := cornerAddX M k
⊢ Membership.mem (γ := Submonoid R[X]) (nonZeroDivisors R[X])
    (charpoly.{u_1, u_4} (n := n) (-(f : (a : S) → Matrix n n R) (M k k)))

Tactic:
exact (Matrix.charpoly_monic _).mem_nonZeroDivisors

Premises used: Polynomial.Monic.mem_nonZeroDivisors, Matrix.charpoly_monic
-- Module: Mathlib.RingTheory.Norm.Transitivity
Goal:
n : Type u_4
inst : DecidableEq n
inst_1 : Fintype n
l_1 : ℕ
ih :
  ∀ {R : Type u_1} {S : Type u_2} {m : Type u_5} [inst_6 : CommRing R] [inst_7 : CommRing S] (M : Matrix m m S)
    [inst_8 : DecidableEq m] [inst_9 : Fintype m] (f : S →+* Matrix n n R) (l : Fintype.card m = l_1),
    Eq.{u_1 + 1} (α := R) (det.{u_1, u_4} (n := n) ((f : (a : S) → Matrix n n R) M.det))
      (det (n := m × n)
        ((comp m m n n R : (a : Matrix m m (Matrix n n R)) → Matrix (m × n) (m × n) R)
          (M.map (⇑f : (a : S) → Matrix n n R))))
R : Type u_1
S : Type u_2
m : Type u_5
inst_2 : CommRing R
inst_3 : CommRing S
M : Matrix m m S
inst_4 : DecidableEq m
inst_5 : Fintype m
f : S →+* Matrix n n R
l : Fintype.card m = l_1 + 1
k : m
f' : S[X] →+* Matrix.{u_4, u_4, u_1} n n R[X] := f.polyToMatrix
M' : Matrix.{u_5, u_5, u_2} m m S[X] := cornerAddX M k
⊢ Eq.{u_1 + 1} (α := R[X]) (det.{u_1, u_4} (n := n) ((f' : (a : S[X]) → Matrix n n R[X]) M'.det))
    (det (n := m × n)
      ((comp m m n n R[X] : (a : Matrix m m (Matrix n n R[X])) → Matrix (m × n) (m × n) R[X])
        (M'.map (⇑f' : (a : S[X]) → Matrix n n R[X]))))

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_right.mp
        (pow_mem ?_ _) _ (det_det_aux k fun M ↦ ih _ _ <| by
          grind [Fintype.card_subtype_compl, Fintype.card_unique])
      rw [polyToMatrix_cornerAddX, ← charpoly]
      exact (Matrix.charpoly_monic _).mem_nonZeroDivisors
-- Module: Mathlib.RingTheory.Norm.Transitivity
Goal:
n : Type u_4
inst : DecidableEq n
inst_1 : Fintype n
l_1 : ℕ
ih :
  ∀ {R : Type u_1} {S : Type u_2} {m : Type u_5} [inst_6 : CommRing R] [inst_7 : CommRing S] (M : Matrix m m S)
    [inst_8 : DecidableEq m] [inst_9 : Fintype m] (f : S →+* Matrix n n R) (l : Fintype.card m = l_1),
    Eq.{u_1 + 1} (α := R) (det.{u_1, u_4} (n := n) ((f : (a : S) → Matrix n n R) M.det))
      (det (n := m × n)
        ((comp m m n n R : (a : Matrix m m (Matrix n n R)) → Matrix (m × n) (m × n) R)
          (M.map (⇑f : (a : S) → Matrix n n R))))
R : Type u_1
S : Type u_2
m : Type u_5
inst_2 : CommRing R
inst_3 : CommRing S
M : Matrix m m S
inst_4 : DecidableEq m
inst_5 : Fintype m
f : S →+* Matrix n n R
l : Fintype.card m = l_1 + 1
k : m
f' : S[X] →+* Matrix.{u_4, u_4, u_1} n n R[X] := f.polyToMatrix
M' : Matrix.{u_5, u_5, u_2} m m S[X] := cornerAddX M k
this :
  Eq.{u_1 + 1} (α := R[X]) (det.{u_1, u_4} (n := n) ((f' : (a : S[X]) → Matrix n n R[X]) M'.det))
    (det (n := m × n)
      ((comp m m n n R[X] : (a : Matrix m m (Matrix n n R[X])) → Matrix (m × n) (m × n) R[X])
        (M'.map (⇑f' : (a : S[X]) → Matrix n n R[X]))))
succ :
  Eq.{u_1 + 1} (α := R)
    (eval 0 (det.{u_1, u_4} (n := n) ((f.polyToMatrix : (a : S[X]) → Matrix n n R[X]) (det (cornerAddX M k)))))
    (det (n := m × n)
      ((comp m m n n R : (a : Matrix m m (Matrix n n R)) → Matrix (m × n) (m × n) R)
        (M.map (⇑f : (a : S) → Matrix n n R))))
succ₁ : m
succ₂ :
  Eq.{u_1 + 1} (α := R)
    (eval 0
      (det (n := m × n)
        ((comp m m n n R[X] : (a : Matrix m m (Matrix n n R[X])) → Matrix (m × n) (m × n) R[X])
          (M'.map (⇑f' : (a : S[X]) → Matrix n n R[X])))))
    (det (n := m × n)
      ((comp m m n n R : (a : Matrix m m (Matrix n n R)) → Matrix (m × n) (m × n) R)
        (M.map (⇑f : (a : S) → Matrix n n R))))
succ₃ succ₄ :
  Eq.{u_1 + 1} (α := R)
    (det (n := m × n)
      ((comp m m n n R : (a : Matrix m m (Matrix n n R)) → Matrix (m × n) (m × n) R)
        (M.map (⇑f : (a : S) → Matrix n n R))))
    (det (n := m × n)
      ((comp m m n n R : (a : Matrix m m (Matrix n n R)) → Matrix (m × n) (m × n) R)
        (M.map (⇑f : (a : S) → Matrix n n R))))
⊢ Eq.{u_1 + 1} (α := R) (det.{u_1, u_4} (n := n) ((f : (a : S) → Matrix n n R) M.det))
    (det (n := m × n)
      ((comp m m n n R : (a : Matrix m m (Matrix n n R)) → Matrix (m × n) (m × n) R)
        (M.map (⇑f : (a : S) → Matrix n n R))))

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

Premises used: Polynomial.eval, congr_arg, Algebra.Norm.Transitivity.eval_zero_comp_det, Algebra.Norm.Transitivity.eval_zero_det_det, OfNat.ofNat
-- Module: Mathlib.RingTheory.Norm.Transitivity
Goal:
R : Type u_1
S : Type u_2
n : Type u_4
m : Type u_5
inst : CommRing R
inst_1 : CommRing S
M : Matrix m m S
inst_2 : DecidableEq m
inst_3 : DecidableEq n
inst_4 : Fintype m
inst_5 : Fintype n
f : S →+* Matrix n n R
induction :
  ∀ (x : ℕ) (l : Fintype.card m = x),
    Eq.{u_1 + 1} (α := R) (det.{u_1, u_4} (n := n) ((f : (a : S) → Matrix n n R) M.det))
      (det (n := m × n)
        ((comp m m n n R : (a : Matrix m m (Matrix n n R)) → Matrix (m × n) (m × n) R)
          (M.map (⇑f : (a : S) → Matrix n n R))))
⊢ Eq.{u_1 + 1} (α := R) (det.{u_1, u_4} (n := n) ((f : (a : S) → Matrix n n R) M.det))
    (det (n := m × n)
      ((comp m m n n R : (a : Matrix m m (Matrix n n R)) → Matrix (m × n) (m × n) R)
        (M.map (⇑f : (a : S) → Matrix n n R))))

Tactic:
induction l : Fintype.card m generalizing R S m with
  | zero =>
    rw [Fintype.card_eq_zero_iff] at l
    simp_rw [Matrix.det_isEmpty, map_one, det_one]
  | succ l ih =>
    have ⟨k⟩ := Fintype.card_pos_iff.mp (Nat.lt_of_sub_eq_succ l)
    let f' := f.polyToMatrix
    let M' := cornerAddX M k
    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_right.mp
        (pow_mem ?_ _) _ (det_det_aux k fun M ↦ ih _ _ <| by
          grind [Fintype.card_subtype_compl, Fintype.card_unique])
      rw [polyToMatrix_cornerAddX, ← charpoly]
      exact (Matrix.charpoly_monic _).mem_nonZeroDivisors
    rw [← eval_zero_det_det, congr_arg (eval 0) this, eval_zero_comp_det]

Premises used: Fintype.card, Algebra.Norm.Transitivity.eval_zero_comp_det, map_one, Fintype.card_eq_zero_iff, Matrix.det_one, Matrix.det_isEmpty, Algebra.Norm.Transitivity.eval_zero_det_det, Matrix.zero
-- Module: Mathlib.RingTheory.Norm.Transitivity
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Module.Free R S
inst_4 : AddCommGroup A
inst_5 : Module R A
inst_6 : Module S A
inst_7 : IsScalarTower R S A
inst_8 : Module.Free S A
f : A →ₗ[S] A
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.RingTheory.Norm.Transitivity
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Module.Free R S
inst_4 : AddCommGroup A
inst_5 : Module R A
inst_6 : Module S A
inst_7 : IsScalarTower R S A
inst_8 : Module.Free S A
f : A →ₗ[S] A
h : Nontrivial R
⊢ Nontrivial A

Tactic:
nontriviality A
-- Module: Mathlib.RingTheory.Norm.Transitivity
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Module.Free R S
inst_4 : AddCommGroup A
inst_5 : Module R A
inst_6 : Module S A
inst_7 : IsScalarTower R S A
inst_8 : Module.Free S A
f : A →ₗ[S] A
h : Nontrivial R
h_1 : Nontrivial A
⊢ Nontrivial S

Tactic:
have := Module.nontrivial S A
-- Module: Mathlib.RingTheory.Norm.Transitivity
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Module.Free R S
inst_4 : AddCommGroup A
inst_5 : Module R A
inst_6 : Module S A
inst_7 : IsScalarTower R S A
inst_8 : Module.Free S A
f : A →ₗ[S] A
h : Nontrivial R
h_1 : Nontrivial A
this : Nontrivial S
let :
  ∀ (ιS : Type u_2) (bS : Module.Basis ιS R S),
    Eq.{u_1 + 1} (α := R)
      ((LinearMap.det : (a : A →ₗ[R] A) → R)
          ((↑R :
              {S : Type u_2} →
                {M M₂ : Type u_3} →
                  [inst : Semiring R] →
                    [inst_9 : Semiring S] →
                      [inst_10 : AddCommMonoid M] →
                        [inst_11 : AddCommMonoid M₂] →
                          [inst_12 : Module R M] →
                            [inst_13 : Module R M₂] →
                              [inst_14 : Module S M] →
                                [inst_15 : Module S M₂] → [CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
            f) :
        R)
      ((Algebra.norm R : (a : S) → R) ((LinearMap.det : (a : A →ₗ[S] A) → S) f : S) : R)
⊢ Eq.{u_1 + 1} (α := R)
    ((LinearMap.det : (a : A →ₗ[R] A) → R)
        ((↑R :
            {S : Type u_2} →
              {M M₂ : Type u_3} →
                [inst : Semiring R] →
                  [inst_9 : Semiring S] →
                    [inst_10 : AddCommMonoid M] →
                      [inst_11 : AddCommMonoid M₂] →
                        [inst_12 : Module R M] →
                          [inst_13 : Module R M₂] →
                            [inst_14 : Module S M] →
                              [inst_15 : Module S M₂] → [CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
          f) :
      R)
    ((Algebra.norm R : (a : S) → R) ((LinearMap.det : (a : A →ₗ[S] A) → S) f : S) : R)

Tactic:
let ⟨ιS, bS⟩ := Module.Free.exists_basis (R := R) (M := S)