awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Submodule (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
x : S
a : Set R
y : R
hy : Membership.mem (γ := Ideal R) (Ideal.span a) y
z : ↥M
hz : x = mk' S y z
mpr : mk' S y z = HSMul.hSMul (β := S) (mk' S 1 z) ((algebraMap R S : (a : R) → S) y : S)
mpr₁ : mk' S y z = HMul.hMul (β := S) (mk' S 1 z) ((algebraMap R S : (a : R) → S) y : S)
mpr₂ : mk' S y z = HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) y : S) (mk' S 1 z)
mpr₃ : mk' S y z = mk' S (y * 1) z
⊢ x = HSMul.hSMul (β := S) (mk' S 1 z) ((algebraMap R S : (a : R) → S) y : S)
have mpr₄ : mk' S y z = mk' S y z
Tactic: rw [hz, smul_eq_mul, mul_comm, mul_mk'_eq_mk'_of_mul, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Transitivity (hypothesis)
Goal:
S : Type u_2
m : Type u_5
inst : CommRing S
M : Matrix m m S
inst_1 : DecidableEq m
k i j : m
lt : LT.lt (α := Prop) ((fun (x : m) ↦ x ≠ k) j) ((fun (x : m) ↦ x ≠ k) i)
⊢ auxMat M k i j = 0
have lt₁ : i ≠ k ∧ j = k
Tactic: simp_rw [lt_iff_not_ge, le_Prop_eq, Classical.not_imp, not_not] at lt
Cleared hypotheses: lt
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Transitivity (goal)
Goal:
S : Type u_2
m : Type u_5
inst : CommRing S
M : Matrix m m S
inst_1 : DecidableEq m
k i j : m
lt : i ≠ k ∧ j = k
⊢ auxMat M k i j = 0
have rw : Eq.{u_2 + 1} (α := S)
  ((of : (a : m → m → S) → Matrix m m S)
      (fun (i j : m) ↦ if j = k then if i = k then 1 else 0 else if i = k then -M k j else if i = j then M k k else 0) i
      j :
    S)
  (0 : S)
Tactic: rw [auxMat, of_apply, if_pos lt.2, if_neg lt.1]
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Transitivity (goal)
Goal:
S : Type u_2
m : Type u_5
inst : CommRing S
M : Matrix m m S
inst_1 : DecidableEq m
k i j : m
lt : i ≠ k ∧ j = k
rw :
  Eq.{u_2 + 1} (α := S)
    ((of : (a : m → m → S) → Matrix m m S)
        (fun (i j : m) ↦ if j = k then if i = k then 1 else 0 else if i = k then -M k j else if i = j then M k k else 0)
        i j :
      S)
    (0 : S)
⊢ auxMat M k i j = 0
have rw₁ : (if j = k then if i = k then 1 else 0 else if i = k then -M k j else if i = j then M k k else 0) = 0
Tactic: rw [auxMat, of_apply, if_pos lt.2, if_neg lt.1]
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Transitivity (goal)
Goal:
S : Type u_2
m : Type u_5
inst : CommRing S
M : Matrix m m S
inst_1 : DecidableEq m
k i j : m
lt : i ≠ k ∧ j = k
rw :
  Eq.{u_2 + 1} (α := S)
    ((of : (a : m → m → S) → Matrix m m S)
        (fun (i j : m) ↦ if j = k then if i = k then 1 else 0 else if i = k then -M k j else if i = j then M k k else 0)
        i j :
      S)
    (0 : S)
rw₁ : (if j = k then if i = k then 1 else 0 else if i = k then -M k j else if i = j then M k k else 0) = 0
⊢ auxMat M k i j = 0
have rw₂ : Eq.{u_2 + 1} (α := S) (if i = k then 1 else 0) 0
Tactic: rw [auxMat, of_apply, if_pos lt.2, if_neg lt.1]
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Transitivity (goal)
Goal:
S : Type u_2
m : Type u_5
inst : CommRing S
M : Matrix m m S
inst_1 : DecidableEq m
k i j : m
lt : i ≠ k ∧ j = k
rw :
  Eq.{u_2 + 1} (α := S)
    ((of : (a : m → m → S) → Matrix m m S)
        (fun (i j : m) ↦ if j = k then if i = k then 1 else 0 else if i = k then -M k j else if i = j then M k k else 0)
        i j :
      S)
    (0 : S)
rw₁ : (if j = k then if i = k then 1 else 0 else if i = k then -M k j else if i = j then M k k else 0) = 0
rw₂ : Eq.{u_2 + 1} (α := S) (if i = k then 1 else 0) 0
⊢ auxMat M k i j = 0
have rw₃ : Eq.{u_2 + 1} (α := S) 0 0
Tactic: rw [auxMat, of_apply, if_pos lt.2, if_neg lt.1]
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Transitivity (goal)
Goal:
S : Type u_2
m : Type u_5
inst : CommRing S
M : Matrix m m S
inst_1 : DecidableEq m
k : 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
have a : ∀ (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: ext i j
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Transitivity (goal)
Goal:
S : Type u_2
m : Type u_5
inst : CommRing S
M : Matrix m m S
inst_1 : DecidableEq m
k : m
⊢ 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
have 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)
Tactic: ext ⟨i, hi⟩ ⟨j, hj⟩
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Transitivity (goal)
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
⊢ (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)
have 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)
Tactic: rw [eq_iff_iff, iff_false, not_not] at hi hj
Cleared hypotheses: j, hj
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Transitivity (hypothesis)
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)
⊢ (M * auxMat M k) i j = 0
have lt₁ : i = k ∧ ¬j = k
Tactic: simp_rw [lt_iff_not_ge, le_Prop_eq, Classical.not_imp] at lt
Cleared hypotheses: lt
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Transitivity (goal)
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
⊢ (M * auxMat M k) i j = 0
have 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
Tactic: simp_rw [Matrix.mul_apply, auxMat, of_apply, if_neg lt.2, mul_ite, mul_neg, mul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Transitivity (goal)
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
⊢ 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
have hc : Membership.mem (γ := Finset m) {x : m | ¬x = k} j
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]
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Transitivity (goal)
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).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
have 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)
Tactic: ext ⟨i, hi⟩ ⟨j, hj⟩
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Transitivity (goal)
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
⊢ (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)
have 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)
Tactic: rw [eq_iff_iff, iff_true] at hi hj
Cleared hypotheses: j, hj
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Transitivity (goal)
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 k k * det (n := { a : m // (a = k) = False }) ((M * auxMat M k).toSquareBlock (fun (x : m) ↦ x = k) False)
have trans : M.det * M k k ^ (Fintype.card m - 1) = (M * auxMat M k).det
Tactic: trans (M * auxMat M k).det
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Transitivity (goal)
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
⊢ 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)
have 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)
Tactic: trans (M * auxMat M k).det
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Transitivity (goal)
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).det =
    M k k * det (n := { a : m // (a = k) = False }) ((M * auxMat M k).toSquareBlock (fun (x : m) ↦ x = k) False)
have 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)
Tactic: rw [(mul_auxMat_blockTriangular M k).det_fintype, Fintype.prod_Prop, mul_auxMat_toSquareBlock_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Transitivity (goal)
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
⊢ (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)
have 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)
Tactic: simp_rw [det_smul_of_tower, eq_iff_iff, iff_true, Fintype.card_unique,
    pow_one, det_one, smul_eq_mul, mul_one]
-- 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
⊢ 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))
have 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))
Tactic: rw [← coe_evalRingHom, RingHom.map_det, ← RingHom.comp_apply,
    evalRingHom_mapMatrix_comp_polyToMatrix, f.comp_apply, RingHom.map_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
k : m
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)
        (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))
have e_M : (RingHom.mapMatrix (evalRingHom 0) : (a : Matrix m m S[X]) → Matrix m m S) (cornerAddX M k) = M
Tactic: congr
-- 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
⊢ (RingHom.mapMatrix (evalRingHom 0) : (a : Matrix m m S[X]) → Matrix m m S) (cornerAddX M k) = M
have 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
Tactic: ext
-- 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
⊢ 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))))
have 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)))
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]
-- 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
⊢ 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)))
have 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
Tactic: congr with i j
-- 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.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))))
have 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)))
Tactic: trans (((M * auxMat M k).map f).comp m m n n R).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
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)))
⊢ 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))))
have 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))))
Tactic: trans (((M * auxMat M k).map f).comp m m n n R).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
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 * auxMat M k).map (⇑f : (a : S) → Matrix n n R)))
have 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))
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]