awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Transitivity (goal)
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 * 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))))
have 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))))
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]
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Transitivity (goal)
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
ih :
  ∀ (M : Matrix.{u_5, u_5, u_2} { a : m // (a = k) = False } { a : m // (a = k) = False } S),
    Eq.{u_1 + 1} (α := R) (det.{u_1, u_4} (n := n) ((f : (a : S) → Matrix n n R) M.det))
      (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)
          (M.map (⇑f : (a : S) → Matrix n n R))))
⊢ HSub.hSub (α := R) (det.{u_1, u_4} (n := n) ((f : (a : S) → Matrix n n R) M.det))
        (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) =
    0
have rw : det.{u_1, u_4} (n := n) ((f : (a : S) → Matrix n n R) M.det) *
      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))) *
      HPow.hPow (α := R) (det.{u_1, u_4} (n := n) ((f : (a : S) → Matrix n n R) (M k k))) (Fintype.card m - 1) =
  0
Tactic: rw [sub_mul, comp_det_mul_pow, ← det_pow, ← map_pow, ← det_mul, ← map_mul,
    det_mul_corner_pow, map_mul, det_mul, ih, sub_self]
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Transitivity (goal)
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
ih :
  ∀ (M : Matrix.{u_5, u_5, u_2} { a : m // (a = k) = False } { a : m // (a = k) = False } S),
    Eq.{u_1 + 1} (α := R) (det.{u_1, u_4} (n := n) ((f : (a : S) → Matrix n n R) M.det))
      (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)
          (M.map (⇑f : (a : S) → Matrix n n R))))
rw :
  det.{u_1, u_4} (n := n) ((f : (a : S) → Matrix n n R) M.det) *
        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))) *
        HPow.hPow (α := R) (det.{u_1, u_4} (n := n) ((f : (a : S) → Matrix n n R) (M k k))) (Fintype.card m - 1) =
    0
⊢ HSub.hSub (α := R) (det.{u_1, u_4} (n := n) ((f : (a : S) → Matrix n n R) M.det))
        (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) =
    0
have rw₁ : det.{u_1, u_4} (n := n) ((f : (a : S) → Matrix n n R) M.det) *
      HPow.hPow (α := R) (det.{u_1, u_4} (n := n) ((f : (a : S) → Matrix n n R) (M k k))) (Fintype.card m - 1) -
    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)))) =
  0
Tactic: rw [sub_mul, comp_det_mul_pow, ← det_pow, ← map_pow, ← det_mul, ← map_mul,
    det_mul_corner_pow, map_mul, det_mul, ih, sub_self]
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Transitivity (hypothesis)
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
⊢ 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))))
have l₁ : IsEmpty m
Tactic: rw [Fintype.card_eq_zero_iff] at l
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Transitivity (goal)
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
⊢ 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))))
have zero : Eq.{u_1 + 1} (α := R) (det.{u_1, u_4} (n := n) ((f : (a : S) → Matrix n n R) 1)) 1
Tactic: simp_rw [Matrix.det_isEmpty, map_one, det_one]
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Transitivity (goal)
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
⊢ 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))))
have zero₁ : Eq.{u_1 + 1} (α := R) (det.{u_1, u_4} (n := n) 1) 1
Tactic: simp_rw [Matrix.det_isEmpty, map_one, det_one]
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Transitivity (goal)
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
⊢ 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))))
have 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))))
Tactic: have ⟨k⟩ := Fintype.card_pos_iff.mp (Nat.lt_of_sub_eq_succ l)
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Transitivity (goal)
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]))))
have 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)))
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])
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Transitivity (goal)
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])
    (det.{u_1, u_4} (n := n) ((f' : (a : S[X]) → Matrix n n R[X]) (M' k k)))
have 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)))
Tactic: rw [polyToMatrix_cornerAddX, ← charpoly]
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Transitivity (hypothesis)
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) (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))))
have 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]))))
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
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Transitivity (goal)
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]))))
⊢ 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))))
have 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))))
Tactic: rw [← eval_zero_det_det, congr_arg (eval 0) this, eval_zero_comp_det]
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Transitivity (goal)
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
⊢ 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))))
have 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))))
Tactic: rw [← eval_zero_det_det, congr_arg (eval 0) this, eval_zero_comp_det]
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Transitivity (goal)
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))))
⊢ 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))))
have 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))))
Tactic: rw [← eval_zero_det_det, congr_arg (eval 0) this, eval_zero_comp_det]
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Transitivity (goal)
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
⊢ 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))))
have 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))))
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]
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Transitivity (hypothesis)
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
⊢ 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)
have a : Nontrivial R
Tactic: nontriviality R