awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Norm.Transitivity
Goal:
S : Type u_2
m : Type u_5
inst : CommRing S
M : Matrix m m S
inst_1 : DecidableEq m
k : m
i j : { a : m // (a ≠ k) = True }
⊢ (auxMat M k).toSquareBlock (fun (x : m) ↦ x ≠ k) True i j =
    HSMul.hSMul (β := Matrix.{u_5, u_5, u_2} { a : m // (a ≠ k) = True } { a : m // (a ≠ k) = True } S) (M k k) 1 i j

Tactic:
simp [auxMat, toSquareBlock_def, if_neg (of_eq_true i.2), if_neg (of_eq_true j.2),
    Matrix.one_apply, Subtype.ext_iff]

Premises used: Matrix.toSquareBlock_def, Matrix.one_apply, Subtype.ext_iff, of_eq_true, if_neg, Algebra.Norm.Transitivity.auxMat, Subtype.property
-- Module: Mathlib.RingTheory.Norm.Transitivity
Goal:
S : Type u_2
m : Type u_5
inst : CommRing S
M : Matrix m m S
inst_1 : DecidableEq m
k : m
a :
  ∀ (i : m) (hi : (i ≠ k) = False) (j : m) (hj : (j ≠ k) = False),
    (auxMat M k).toSquareBlock (fun (x : m) ↦ x ≠ k) False (Subtype.mk (p := fun (a : m) ↦ (a ≠ k) = False) i hi)
        (Subtype.mk (p := fun (a : m) ↦ (a ≠ k) = False) j hj) =
      1 (Subtype.mk (p := fun (a : m) ↦ (a ≠ k) = False) i hi) (Subtype.mk (p := fun (a : m) ↦ (a ≠ k) = False) j hj)
⊢ Eq (α := Matrix.{u_5, u_5, u_2} { a : m // (a ≠ k) = False } { a : m // (a ≠ k) = False } S)
    ((auxMat M k).toSquareBlock (fun (x : m) ↦ x ≠ k) False) 1

Tactic:
ext ⟨i, hi⟩ ⟨j, hj⟩
-- Module: Mathlib.RingTheory.Norm.Transitivity
Goal:
S : Type u_2
m : Type u_5
inst : CommRing S
M : Matrix m m S
inst_1 : DecidableEq m
k i : m
hi : (i ≠ k) = False
j : m
hj : (j ≠ k) = False
a :
  ∀ (hi_1 : i = k) (j : m) (hj : (j ≠ k) = False) (hj_1 : j = k),
    (auxMat M k).toSquareBlock (fun (x : m) ↦ x ≠ k) False (Subtype.mk (p := fun (a : m) ↦ (a ≠ k) = False) i hi)
        (Subtype.mk (p := fun (a : m) ↦ (a ≠ k) = False) j hj) =
      1 (Subtype.mk (p := fun (a : m) ↦ (a ≠ k) = False) i hi) (Subtype.mk (p := fun (a : m) ↦ (a ≠ k) = False) j hj)
⊢ (auxMat M k).toSquareBlock (fun (x : m) ↦ x ≠ k) False (Subtype.mk (p := fun (a : m) ↦ (a ≠ k) = False) i hi)
      (Subtype.mk (p := fun (a : m) ↦ (a ≠ k) = False) j hj) =
    1 (Subtype.mk (p := fun (a : m) ↦ (a ≠ k) = False) i hi) (Subtype.mk (p := fun (a : m) ↦ (a ≠ k) = False) j hj)

Tactic:
rw [eq_iff_iff, iff_false, not_not] at hi hj

Premises used: iff_false, Classical.not_not, eq_iff_iff
-- Module: Mathlib.RingTheory.Norm.Transitivity
Goal:
S : Type u_2
m : Type u_5
inst : CommRing S
M : Matrix m m S
inst_1 : DecidableEq m
k i : m
hi_1 : (i ≠ k) = False
hi : i = k
j : m
hj_1 : (j ≠ k) = False
hj : j = k
⊢ (auxMat M k).toSquareBlock (fun (x : m) ↦ x ≠ k) False (Subtype.mk (p := fun (a : m) ↦ (a ≠ k) = False) i hi_1)
      (Subtype.mk (p := fun (a : m) ↦ (a ≠ k) = False) j hj_1) =
    1 (Subtype.mk (p := fun (a : m) ↦ (a ≠ k) = False) i hi_1) (Subtype.mk (p := fun (a : m) ↦ (a ≠ k) = False) j hj_1)

Tactic:
simp [auxMat, toSquareBlock_def, if_pos hi, if_pos hj, Matrix.one_apply, if_pos (hj ▸ hi)]

Premises used: Matrix.toSquareBlock_def, Matrix.one_apply, if_pos, Algebra.Norm.Transitivity.auxMat
-- Module: Mathlib.RingTheory.Norm.Transitivity
Goal:
S : Type u_2
m : Type u_5
inst : CommRing S
M : Matrix m m S
inst_1 : DecidableEq m
k : m
inst_2 : Fintype m
i j : m
lt : LT.lt (α := Prop) ((fun (x : m) ↦ x = k) j) ((fun (x : m) ↦ x = k) i)
⊢ i = k ∧ ¬j = k

Tactic:
simp_rw [lt_iff_not_ge, le_Prop_eq, Classical.not_imp] at lt

Premises used: lt_iff_not_ge, Classical.not_imp, le_Prop_eq
-- Module: Mathlib.RingTheory.Norm.Transitivity
Goal:
S : Type u_2
m : Type u_5
inst : CommRing S
M : Matrix m m S
inst_1 : DecidableEq m
k : m
inst_2 : Fintype m
i j : m
lt : i = k ∧ ¬j = k
simp_rw : Eq.{u_2 + 1} (α := S) (∑ x : m, if x = k then -(M i x * M k j) else if x = j then M i x * M k k else 0) 0
⊢ (M * auxMat M k) i j = 0

Tactic:
simp_rw [Matrix.mul_apply, auxMat, of_apply, if_neg lt.2, mul_ite, mul_neg, mul_zero]

Premises used: mul_ite, Matrix.mul_apply, Matrix.of_apply, MulZeroClass.mul_zero, And.right, if_neg, Algebra.Norm.Transitivity.auxMat, mul_neg
-- Module: Mathlib.RingTheory.Norm.Transitivity
Goal:
S : Type u_2
m : Type u_5
inst : CommRing S
M : Matrix m m S
inst_1 : DecidableEq m
k : m
inst_2 : Fintype m
i j : m
lt : i = k ∧ ¬j = k
hc : Membership.mem (γ := Finset m) {x : m | ¬x = k} j
⊢ Eq.{u_2 + 1} (α := S) (∑ x : m, if x = k then -(M i x * M k j) else if x = j then M i x * M k k else 0) 0

Tactic:
rw [Finset.sum_ite, Finset.filter_eq', if_pos (Finset.mem_univ _), Finset.sum_singleton,
      Finset.sum_ite_eq', if_pos, lt.1, mul_comm, neg_add_cancel]

Premises used: Finset.mem_univ, Finset.sum_ite_eq', Finset.filter_eq', if_pos, Finset.sum_singleton, neg_add_cancel, And.left, mul_comm, Finset.sum_ite
-- Module: Mathlib.RingTheory.Norm.Transitivity
Goal:
S : Type u_2
m : Type u_5
inst : CommRing S
M : Matrix m m S
inst_1 : DecidableEq m
k : m
inst_2 : Fintype m
i j : m
lt : i = k ∧ ¬j = k
⊢ Membership.mem (γ := Finset m) {x : m | ¬x = k} j

Tactic:
Finset.mem_filter.mpr ⟨Finset.mem_univ _, lt.2⟩

Premises used: Iff.mpr, Finset.mem_univ, And.right, And.intro, Finset.mem_filter
-- Module: Mathlib.RingTheory.Norm.Transitivity
Goal:
S : Type u_2
m : Type u_5
inst : CommRing S
M : Matrix m m S
inst_1 : DecidableEq m
k : m
inst_2 : Fintype m
i j : m
lt : i = k ∧ ¬j = k
⊢ Membership.mem (γ := Finset m) {x : m | ¬x = k} j

Tactic:
exact Finset.mem_filter.mpr ⟨Finset.mem_univ _, lt.2⟩

Premises used: Iff.mpr, Finset.mem_univ, And.right, And.intro, Finset.mem_filter
-- Module: Mathlib.RingTheory.Norm.Transitivity
Goal:
S : Type u_2
m : Type u_5
inst : CommRing S
M : Matrix m m S
inst_1 : DecidableEq m
k : m
inst_2 : Fintype m
⊢ (M * auxMat M k) k k = M k k

Tactic:
simp [Matrix.mul_apply, auxMat]

Premises used: Matrix.mul_apply, Algebra.Norm.Transitivity.auxMat
-- Module: Mathlib.RingTheory.Norm.Transitivity
Goal:
S : Type u_2
m : Type u_5
inst : CommRing S
M : Matrix m m S
inst_1 : DecidableEq m
k : m
inst_2 : Fintype m
a :
  ∀ (i : m) (hi : (i = k) = True) (j : m) (hj : (j = k) = True),
    (M * auxMat M k).toSquareBlock (fun (x : m) ↦ x = k) True (Subtype.mk (p := fun (a : m) ↦ (a = k) = True) i hi)
        (Subtype.mk (p := fun (a : m) ↦ (a = k) = True) j hj) =
      HSMul.hSMul (β := Matrix.{u_5, u_5, u_2} { a : m // (a = k) = True } { a : m // (a = k) = True } S) (M k k) 1
        (Subtype.mk (p := fun (a : m) ↦ (a = k) = True) i hi) (Subtype.mk (p := fun (a : m) ↦ (a = k) = True) j hj)
⊢ (M * auxMat M k).toSquareBlock (fun (x : m) ↦ x = k) True =
    HSMul.hSMul (β := Matrix.{u_5, u_5, u_2} { a : m // (a = k) = True } { a : m // (a = k) = True } S) (M k k) 1

Tactic:
ext ⟨i, hi⟩ ⟨j, hj⟩
-- Module: Mathlib.RingTheory.Norm.Transitivity
Goal:
S : Type u_2
m : Type u_5
inst : CommRing S
M : Matrix m m S
inst_1 : DecidableEq m
k : m
inst_2 : Fintype m
i : m
hi : (i = k) = True
j : m
hj : (j = k) = True
a :
  ∀ (hi_1 : i = k) (j : m) (hj : (j = k) = True) (hj_1 : j = k),
    (M * auxMat M k).toSquareBlock (fun (x : m) ↦ x = k) True (Subtype.mk (p := fun (a : m) ↦ (a = k) = True) i hi)
        (Subtype.mk (p := fun (a : m) ↦ (a = k) = True) j hj) =
      HSMul.hSMul (β := Matrix.{u_5, u_5, u_2} { a : m // (a = k) = True } { a : m // (a = k) = True } S) (M k k) 1
        (Subtype.mk (p := fun (a : m) ↦ (a = k) = True) i hi) (Subtype.mk (p := fun (a : m) ↦ (a = k) = True) j hj)
⊢ (M * auxMat M k).toSquareBlock (fun (x : m) ↦ x = k) True (Subtype.mk (p := fun (a : m) ↦ (a = k) = True) i hi)
      (Subtype.mk (p := fun (a : m) ↦ (a = k) = True) j hj) =
    HSMul.hSMul (β := Matrix.{u_5, u_5, u_2} { a : m // (a = k) = True } { a : m // (a = k) = True } S) (M k k) 1
      (Subtype.mk (p := fun (a : m) ↦ (a = k) = True) i hi) (Subtype.mk (p := fun (a : m) ↦ (a = k) = True) j hj)

Tactic:
rw [eq_iff_iff, iff_true] at hi hj

Premises used: iff_true, eq_iff_iff
-- Module: Mathlib.RingTheory.Norm.Transitivity
Goal:
S : Type u_2
m : Type u_5
inst : CommRing S
M : Matrix m m S
inst_1 : DecidableEq m
k : m
inst_2 : Fintype m
i : m
hi_1 : (i = k) = True
hi : i = k
j : m
hj_1 : (j = k) = True
hj : j = k
⊢ (M * auxMat M k).toSquareBlock (fun (x : m) ↦ x = k) True (Subtype.mk (p := fun (a : m) ↦ (a = k) = True) i hi_1)
      (Subtype.mk (p := fun (a : m) ↦ (a = k) = True) j hj_1) =
    HSMul.hSMul (β := Matrix.{u_5, u_5, u_2} { a : m // (a = k) = True } { a : m // (a = k) = True } S) (M k k) 1
      (Subtype.mk (p := fun (a : m) ↦ (a = k) = True) i hi_1) (Subtype.mk (p := fun (a : m) ↦ (a = k) = True) j hj_1)

Tactic:
simp [toSquareBlock_def, hi, hj, mul_auxMat_corner]

Premises used: Matrix.toSquareBlock_def, Algebra.Norm.Transitivity.mul_auxMat_corner
-- Module: Mathlib.RingTheory.Norm.Transitivity
Goal:
S : Type u_2
m : Type u_5
inst : CommRing S
M : Matrix m m S
inst_1 : DecidableEq m
k : m
inst_2 : Fintype m
trans : M.det * M k k ^ (Fintype.card m - 1) = (M * auxMat M k).det
trans₁ :
  (M * auxMat M k).det =
    M k k * det (n := { a : m // (a = k) = False }) ((M * auxMat M k).toSquareBlock (fun (x : m) ↦ x = k) False)
⊢ M.det * M k k ^ (Fintype.card m - 1) =
    M k k * det (n := { a : m // (a = k) = False }) ((M * auxMat M k).toSquareBlock (fun (x : m) ↦ x = k) False)

Tactic:
trans (M * auxMat M k).det

Premises used: HMul.hMul, Matrix.det, Algebra.Norm.Transitivity.auxMat
-- Module: Mathlib.RingTheory.Norm.Transitivity
Goal:
S : Type u_2
m : Type u_5
inst : CommRing S
M : Matrix m m S
inst_1 : DecidableEq m
k : m
inst_2 : Fintype m
⊢ M.det * M k k ^ (Fintype.card m - 1) = (M * auxMat M k).det

Tactic:
simp [det_mul, (auxMat_blockTriangular M k).det_fintype,
      auxMat_toSquareBlock_ne, auxMat_toSquareBlock_eq]

Premises used: Matrix.det_mul, Algebra.Norm.Transitivity.auxMat_toSquareBlock_ne, Matrix.BlockTriangular.det_fintype, Algebra.Norm.Transitivity.auxMat_toSquareBlock_eq, Algebra.Norm.Transitivity.auxMat_blockTriangular
-- Module: Mathlib.RingTheory.Norm.Transitivity
Goal:
S : Type u_2
m : Type u_5
inst : CommRing S
M : Matrix m m S
inst_1 : DecidableEq m
k : m
inst_2 : Fintype m
rw :
  (HSMul.hSMul (β := Matrix.{u_5, u_5, u_2} { a : m // (a = k) = True } { a : m // (a = k) = True } S) (M k k) 1).det *
      det (n := { a : m // (a = k) = False }) ((M * auxMat M k).toSquareBlock (fun (x : m) ↦ x = k) False) =
    M k k * det (n := { a : m // (a = k) = False }) ((M * auxMat M k).toSquareBlock (fun (x : m) ↦ x = k) False)
⊢ (M * auxMat M k).det =
    M k k * det (n := { a : m // (a = k) = False }) ((M * auxMat M k).toSquareBlock (fun (x : m) ↦ x = k) False)

Tactic:
rw [(mul_auxMat_blockTriangular M k).det_fintype, Fintype.prod_Prop, mul_auxMat_toSquareBlock_eq]

Premises used: Algebra.Norm.Transitivity.mul_auxMat_blockTriangular, Algebra.Norm.Transitivity.mul_auxMat_toSquareBlock_eq, Fintype.prod_Prop, Matrix.BlockTriangular.det_fintype
-- Module: Mathlib.RingTheory.Norm.Transitivity
Goal:
S : Type u_2
m : Type u_5
inst : CommRing S
M : Matrix m m S
inst_1 : DecidableEq m
k : m
inst_2 : Fintype m
simp_rw :
  M k k * det (n := { a : m // (a = k) = False }) ((M * auxMat M k).toSquareBlock (fun (x : m) ↦ x = k) False) =
    M k k * det (n := { a : m // (a = k) = False }) ((M * auxMat M k).toSquareBlock (fun (x : m) ↦ x = k) False)
⊢ (HSMul.hSMul (β := Matrix.{u_5, u_5, u_2} { a : m // (a = k) = True } { a : m // (a = k) = True } S) (M k k) 1).det *
      det (n := { a : m // (a = k) = False }) ((M * auxMat M k).toSquareBlock (fun (x : m) ↦ x = k) False) =
    M k k * det (n := { a : m // (a = k) = False }) ((M * auxMat M k).toSquareBlock (fun (x : m) ↦ x = k) False)

Tactic:
simp_rw [det_smul_of_tower, eq_iff_iff, iff_true, Fintype.card_unique,
    pow_one, det_one, smul_eq_mul, mul_one]

Premises used: Matrix.det_smul_of_tower, iff_true, pow_one, Fintype.card_unique, Matrix.det_one, smul_eq_mul, mul_one, eq_iff_iff
-- Module: Mathlib.RingTheory.Norm.Transitivity
Goal:
S : Type u_2
m : Type u_5
inst : CommRing S
M : Matrix m m S
inst_1 : DecidableEq m
k : m
inst_2 : Fintype m
⊢ M k k * det (n := { a : m // (a = k) = False }) ((M * auxMat M k).toSquareBlock (fun (x : m) ↦ x = k) False) =
    M k k * det (n := { a : m // (a = k) = False }) ((M * auxMat M k).toSquareBlock (fun (x : m) ↦ x = k) False)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Norm.Transitivity
Goal:
S : Type u_2
m : Type u_5
inst : CommRing S
M : Matrix m m S
inst_1 : DecidableEq m
k : m
inst_2 : Fintype m
⊢ M k k * det (n := { a : m // (a = k) = False }) ((M * auxMat M k).toSquareBlock (fun (x : m) ↦ x = k) False) =
    M k k * det (n := { a : m // (a = k) = False }) ((M * auxMat M k).toSquareBlock (fun (x : m) ↦ x = k) False)

Tactic:
convert! rfl

Premises used: rfl
-- 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 n
f : S →+* Matrix n n R
⊢ Eq (α := Matrix.{u_4, u_4, u_1} n n R[X])
    ((f.polyToMatrix : (a : S[X]) → Matrix n n R[X]) (cornerAddX M k k k) : Matrix.{u_4, u_4, u_1} n n R[X])
    (charmatrix (-(f : (a : S) → Matrix n n R) (M k k)) : Matrix.{u_4, u_4, u_1} n n R[X])

Tactic:
simp [cornerAddX, Matrix.add_apply, charmatrix,
    RingHom.polyToMatrix, -AlgEquiv.symm_toRingEquiv, map_neg]

Premises used: Matrix.add_apply, Matrix.charmatrix, map_neg, Algebra.Norm.Transitivity.cornerAddX, RingHom.polyToMatrix, AlgEquiv.symm_toRingEquiv
-- 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
rw :
  Eq.{u_1 + 1} (α := R)
    (det.{u_1, u_4} (n := n)
      ((f : (a : S) → Matrix n n R)
        (det.{u_2, u_5} (n := m)
          ((RingHom.mapMatrix (evalRingHom 0) : (a : Matrix m m S[X]) → Matrix m m S) (cornerAddX M k)))))
    (det.{u_1, u_4} (n := n) ((f : (a : S) → Matrix n n R) M.det))
⊢ 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.{u_1, u_4} (n := n) ((f : (a : S) → Matrix n n R) M.det))

Tactic:
rw [← coe_evalRingHom, RingHom.map_det, ← RingHom.comp_apply,
    evalRingHom_mapMatrix_comp_polyToMatrix, f.comp_apply, RingHom.map_det]

Premises used: evalRingHom_mapMatrix_comp_polyToMatrix, RingHom.map_det, RingHom.comp_apply, Polynomial.coe_evalRingHom
-- 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
e_M : (RingHom.mapMatrix (evalRingHom 0) : (a : Matrix m m S[X]) → Matrix m m S) (cornerAddX M k) = M
⊢ Eq.{u_1 + 1} (α := R)
    (det.{u_1, u_4} (n := n)
      ((f : (a : S) → Matrix n n R)
        (det.{u_2, u_5} (n := m)
          ((RingHom.mapMatrix (evalRingHom 0) : (a : Matrix m m S[X]) → Matrix m m S) (cornerAddX M k)))))
    (det.{u_1, u_4} (n := n) ((f : (a : S) → Matrix n n R) M.det))

Tactic:
congr
-- 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
e_M :
  ∀ (i j : m), (RingHom.mapMatrix (evalRingHom 0) : (a : Matrix m m S[X]) → Matrix m m S) (cornerAddX M k) i j = M i j
⊢ (RingHom.mapMatrix (evalRingHom 0) : (a : Matrix m m S[X]) → Matrix m m S) (cornerAddX M k) = M

Tactic:
ext
-- 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
i j : m
⊢ (RingHom.mapMatrix (evalRingHom 0) : (a : Matrix m m S[X]) → Matrix m m S) (cornerAddX M k) i j = M i j

Tactic:
simp [cornerAddX, diagonal, apply_ite]

Premises used: apply_ite, Algebra.Norm.Transitivity.cornerAddX, Matrix.diagonal
-- 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 :
  Eq.{u_1 + 1} (α := R)
    (det (n := m × n)
      ((RingEquiv.toRingHom (compRingEquiv m n R) : (a : Matrix m m (Matrix n n R)) → Matrix (m × n) (m × n) R)
        ((f.mapMatrix : (a : Matrix m m S) → Matrix m m (Matrix n n R))
          ((RingHom.mapMatrix (evalRingHom 0) : (a : Matrix m m S[X]) → Matrix m m S) (cornerAddX M k)))))
    (det (n := m × n)
      (((↑(compRingEquiv m n R) : Matrix m m (Matrix n n R) →+* Matrix (m × n) (m × n) R) :
          (a : Matrix m m (Matrix n n R)) → Matrix (m × n) (m × n) R)
        ((f.mapMatrix : (a : Matrix m m S) → Matrix m m (Matrix n n R)) M)))
⊢ Eq.{u_1 + 1} (α := R)
    (eval 0
      (det (n := m × n)
        ((Matrix.comp m m n n R[X] : (a : Matrix m m (Matrix n n R[X])) → Matrix (m × n) (m × n) R[X])
          (Matrix.map (α := S[X]) (cornerAddX M k) (⇑f.polyToMatrix : (a : S[X]) → Matrix n n R[X])))))
    (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))))

Tactic:
simp_rw [← coe_evalRingHom, RingHom.map_det, ← compRingEquiv_apply, ← RingEquiv.coe_toRingHom,
    ← RingHom.mapMatrix_apply, ← RingHom.comp_apply, ← RingHom.comp_assoc,
    evalRingHom_mapMatrix_comp_compRingEquiv, RingHom.comp_assoc, RingHom.mapMatrix_comp,
    evalRingHom_mapMatrix_comp_polyToMatrix, ← RingHom.mapMatrix_comp, RingHom.comp_apply]

Premises used: RingHom.mapMatrix_apply, evalRingHom_mapMatrix_comp_polyToMatrix, RingHom.comp_assoc, evalRingHom_mapMatrix_comp_compRingEquiv, RingHom.map_det, RingHom.comp_apply, RingHom.mapMatrix_comp, Matrix.compRingEquiv_apply, RingEquiv.coe_toRingHom, Polynomial.coe_evalRingHom
-- 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
e_M :
  ∀ (i j : m), (RingHom.mapMatrix (evalRingHom 0) : (a : Matrix m m S[X]) → Matrix m m S) (cornerAddX M k) i j = M i j
⊢ Eq.{u_1 + 1} (α := R)
    (det (n := m × n)
      ((RingEquiv.toRingHom (compRingEquiv m n R) : (a : Matrix m m (Matrix n n R)) → Matrix (m × n) (m × n) R)
        ((f.mapMatrix : (a : Matrix m m S) → Matrix m m (Matrix n n R))
          ((RingHom.mapMatrix (evalRingHom 0) : (a : Matrix m m S[X]) → Matrix m m S) (cornerAddX M k)))))
    (det (n := m × n)
      (((↑(compRingEquiv m n R) : Matrix m m (Matrix n n R) →+* Matrix (m × n) (m × n) R) :
          (a : Matrix m m (Matrix n n R)) → Matrix (m × n) (m × n) R)
        ((f.mapMatrix : (a : Matrix m m S) → Matrix m m (Matrix n n R)) M)))

Tactic:
congr with i j
-- 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
trans :
  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 * auxMat M k).map (⇑f : (a : S) → Matrix n n R)))
trans₁ :
  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))))
⊢ 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) =
    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:
trans (((M * auxMat M k).map f).comp m m n n R).det

Premises used: Matrix.comp, HMul.hMul, Matrix.map, DFunLike.coe, Matrix.det, Algebra.Norm.Transitivity.auxMat
-- 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 :
  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))
⊢ 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 * auxMat M k).map (⇑f : (a : S) → Matrix n n R)))

Tactic:
simp_rw [← f.mapMatrix_apply, ← compRingEquiv_apply, map_mul, det_mul, f.mapMatrix_apply,
      compRingEquiv_apply, ((auxMat_blockTriangular M k).map f).comp.det_fintype, Fintype.prod_Prop,
      comp_toSquareBlock (b := (· ≠ k)), det_reindex_self, map_toSquareBlock,
      auxMat_toSquareBlock_eq, auxMat_toSquareBlock_ne, smul_one_eq_diagonal, ← diagonal_one,
      diagonal_map (map_zero _), comp_diagonal, det_reindex_self]

Premises used: Matrix.BlockTriangular.map, RingHom.mapMatrix_apply, Matrix.smul_one_eq_diagonal, Matrix.map_toSquareBlock, map_zero, Matrix.comp_toSquareBlock, Matrix.BlockTriangular.comp, Matrix.det_mul, map_mul, Matrix.diagonal_one, Matrix.det_reindex_self, Fintype.prod_Prop, Algebra.Norm.Transitivity.auxMat_toSquareBlock_ne, Matrix.comp_diagonal, Matrix.compRingEquiv_apply, Matrix.diagonal_map, Matrix.BlockTriangular.det_fintype, Algebra.Norm.Transitivity.auxMat_toSquareBlock_eq, Algebra.Norm.Transitivity.auxMat_blockTriangular