awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.FixedDetMatrices (goal)
Goal:
m : ℤ
hm : m ≠ 0
A : FixedDetMatrix (Fin 2) ℤ m
⊢ reduce A ∈ reps m
have step : ∀ (A : FixedDetMatrix (Fin 2) ℤ m) (h1 : (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 ≠ 0) (h2 : reduce (reduceStep A) ∈ reps m),
  reduce A ∈ reps m
Tactic: induction A using reduce_rec with
  | step A h1 h2 => simpa only [reduce_reduceStep h1] using h2
  | base A h =>
    have hd := A_d_ne_zero h hm
    by_cases h1 : 0 < A.1 0 0
    · simp only [reduce_of_pos h h1]
      have h2 := Int.emod_def (A.1 0 1) (A.1 1 1)
      have h4 := Int.ediv_mul_le (A.1 0 1) hd
      set n : ℤ := A.1 0 1 / A.1 1 1
      have h3 := Int.emod_lt_abs (A.1 0 1) hd
      rw [← abs_eq_self.mpr <| Int.emod_nonneg _ hd] at h3
      simp only [smul_def, coe_T_zpow]
      suffices A.1 1 0 = 0 ∧ n * A.1 1 0 < A.1 0 0 ∧
          n * A.1 1 1 ≤ A.1 0 1 ∧ |A.1 0 1 + -(n * A.1 1 1)| < |A.1 1 1| by
        simpa only [reps, Fin.isValue, cons_mul, Nat.succ_eq_add_one, Nat.reduceAdd, empty_mul,
          Equiv.symm_apply_apply, Set.mem_setOf_eq, of_apply, cons_val', vecMul, cons_dotProduct,
          vecHead, one_mul, vecTail, Function.comp_apply, Fin.succ_zero_eq_one, neg_mul,
          dotProduct_of_isEmpty, add_zero, zero_mul, zero_add, empty_val', cons_val_fin_one,
          cons_val_one, cons_val_zero, lt_add_neg_iff_add_lt, le_add_neg_iff_add_le]
      simp_all only [mul_comm n, zero_mul, ← sub_eq_add_neg, ← h2,
        Fin.isValue, and_true]
    · simp only [reps, Fin.isValue, reduce_of_not_pos h h1, Int.ediv_neg, neg_neg, smul_def, ←
        mul_assoc, S_mul_S_eq, neg_mul, one_mul, coe_T_zpow, mul_neg, cons_mul, Nat.succ_eq_add_one,
        Nat.reduceAdd, empty_mul, Equiv.symm_apply_apply, neg_of, neg_cons, neg_empty,
        Set.mem_setOf_eq, of_apply, cons_val', Pi.neg_apply, vecMul, cons_dotProduct, vecHead,
        vecTail, Function.comp_apply, Fin.succ_zero_eq_one, h, mul_zero, dotProduct_of_isEmpty,
        add_zero, zero_mul, neg_zero, empty_val', cons_val_fin_one, cons_val_one, cons_val_zero,
        lt_neg, neg_add_rev, zero_add, le_add_neg_iff_add_le, ← le_neg, abs_neg, true_and]
      refine ⟨?_, Int.ediv_mul_le _ hd, ?_⟩
      · simp only [Int.lt_iff_le_and_ne]
        exact ⟨not_lt.mp h1, A_a_ne_zero h hm⟩
      · rw [mul_comm, add_comm, ← Int.sub_eq_add_neg, ← Int.emod_def,
         abs_eq_self.mpr <| Int.emod_nonneg _ hd]
        exact Int.emod_lt_abs _ hd
Cleared hypotheses: A
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.FixedDetMatrices (goal)
Goal:
m : ℤ
hm : m ≠ 0
A : FixedDetMatrix (Fin 2) ℤ m
step :
  ∀ (A : FixedDetMatrix (Fin 2) ℤ m) (h1 : (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 ≠ 0)
    (h2 : reduce (reduceStep A) ∈ reps m), reduce A ∈ reps m
⊢ reduce A ∈ reps m
have base : ∀ (A : FixedDetMatrix (Fin 2) ℤ m) (h : (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0), reduce A ∈ reps m
Tactic: induction A using reduce_rec with
  | step A h1 h2 => simpa only [reduce_reduceStep h1] using h2
  | base A h =>
    have hd := A_d_ne_zero h hm
    by_cases h1 : 0 < A.1 0 0
    · simp only [reduce_of_pos h h1]
      have h2 := Int.emod_def (A.1 0 1) (A.1 1 1)
      have h4 := Int.ediv_mul_le (A.1 0 1) hd
      set n : ℤ := A.1 0 1 / A.1 1 1
      have h3 := Int.emod_lt_abs (A.1 0 1) hd
      rw [← abs_eq_self.mpr <| Int.emod_nonneg _ hd] at h3
      simp only [smul_def, coe_T_zpow]
      suffices A.1 1 0 = 0 ∧ n * A.1 1 0 < A.1 0 0 ∧
          n * A.1 1 1 ≤ A.1 0 1 ∧ |A.1 0 1 + -(n * A.1 1 1)| < |A.1 1 1| by
        simpa only [reps, Fin.isValue, cons_mul, Nat.succ_eq_add_one, Nat.reduceAdd, empty_mul,
          Equiv.symm_apply_apply, Set.mem_setOf_eq, of_apply, cons_val', vecMul, cons_dotProduct,
          vecHead, one_mul, vecTail, Function.comp_apply, Fin.succ_zero_eq_one, neg_mul,
          dotProduct_of_isEmpty, add_zero, zero_mul, zero_add, empty_val', cons_val_fin_one,
          cons_val_one, cons_val_zero, lt_add_neg_iff_add_lt, le_add_neg_iff_add_le]
      simp_all only [mul_comm n, zero_mul, ← sub_eq_add_neg, ← h2,
        Fin.isValue, and_true]
    · simp only [reps, Fin.isValue, reduce_of_not_pos h h1, Int.ediv_neg, neg_neg, smul_def, ←
        mul_assoc, S_mul_S_eq, neg_mul, one_mul, coe_T_zpow, mul_neg, cons_mul, Nat.succ_eq_add_one,
        Nat.reduceAdd, empty_mul, Equiv.symm_apply_apply, neg_of, neg_cons, neg_empty,
        Set.mem_setOf_eq, of_apply, cons_val', Pi.neg_apply, vecMul, cons_dotProduct, vecHead,
        vecTail, Function.comp_apply, Fin.succ_zero_eq_one, h, mul_zero, dotProduct_of_isEmpty,
        add_zero, zero_mul, neg_zero, empty_val', cons_val_fin_one, cons_val_one, cons_val_zero,
        lt_neg, neg_add_rev, zero_add, le_add_neg_iff_add_le, ← le_neg, abs_neg, true_and]
      refine ⟨?_, Int.ediv_mul_le _ hd, ?_⟩
      · simp only [Int.lt_iff_le_and_ne]
        exact ⟨not_lt.mp h1, A_a_ne_zero h hm⟩
      · rw [mul_comm, add_comm, ← Int.sub_eq_add_neg, ← Int.emod_def,
         abs_eq_self.mpr <| Int.emod_nonneg _ hd]
        exact Int.emod_lt_abs _ hd
Cleared hypotheses: A
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.FixedDetMatrices (goal)
Goal:
m : ℤ
C : FixedDetMatrix (Fin 2) ℤ m → Prop
hS : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (S • B)
B : FixedDetMatrix (Fin 2) ℤ m
⊢ C (S • B) ↔ C B
have refine : C (S • B) → C B
Tactic: refine ⟨?_, hS _⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.FixedDetMatrices (goal)
Goal:
m : ℤ
C : FixedDetMatrix (Fin 2) ℤ m → Prop
hS : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (S • B)
B : FixedDetMatrix (Fin 2) ℤ m
ih : C (S • B)
⊢ C B
have rw : C (S • S • S • S • B)
Tactic: rw [← (S_smul_four B)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.FixedDetMatrices (goal)
Goal:
m : ℤ
C : FixedDetMatrix (Fin 2) ℤ m → Prop
hS : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (S • B)
hT : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (T • B)
B : FixedDetMatrix (Fin 2) ℤ m
⊢ C (T • B) ↔ C B
have refine : C (T • B) → C B
Tactic: refine ⟨?_, hT _⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.FixedDetMatrices (goal)
Goal:
m : ℤ
C : FixedDetMatrix (Fin 2) ℤ m → Prop
hS : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (S • B)
hT : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (T • B)
B : FixedDetMatrix (Fin 2) ℤ m
ih : C (T • B)
⊢ C B
have rw : C (S • S • S • T • S • T • S • T • B)
Tactic: rw [show B = T⁻¹ • T • B by simp, ← T_S_rel_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.FixedDetMatrices (goal)
Goal:
m_1 : ℤ
C : FixedDetMatrix (Fin 2) ℤ m_1 → Prop
hS : ∀ (B : FixedDetMatrix (Fin 2) ℤ m_1), C B → C (S • B)
hT : ∀ (B : FixedDetMatrix (Fin 2) ℤ m_1), C B → C (T • B)
B : FixedDetMatrix (Fin 2) ℤ m_1
m : ℕ
hm : C (HPow.hPow (β := ℤ) T (-(↑m : ℤ)) • B) ↔ C B
⊢ C (T ^ HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1 • B) ↔ C B
have pred : C (T ^ HAdd.hAdd (α := ℤ) (-1) (-(↑m : ℤ)) • B) ↔ C B
Tactic: rwa [sub_eq_neg_add, zpow_add, zpow_neg_one, ← prop_red_T hS hT, mul_smul, smul_inv_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.FixedDetMatrices (goal)
Goal:
m_1 : ℤ
C : FixedDetMatrix (Fin 2) ℤ m_1 → Prop
hS : ∀ (B : FixedDetMatrix (Fin 2) ℤ m_1), C B → C (S • B)
hT : ∀ (B : FixedDetMatrix (Fin 2) ℤ m_1), C B → C (T • B)
B : FixedDetMatrix (Fin 2) ℤ m_1
m : ℕ
hm : C (HPow.hPow (β := ℤ) T (-(↑m : ℤ)) • B) ↔ C B
pred : C (T ^ HAdd.hAdd (α := ℤ) (-1) (-(↑m : ℤ)) • B) ↔ C B
⊢ C (T ^ HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1 • B) ↔ C B
have pred₁ : C ((HPow.hPow (β := ℤ) T (-1) * HPow.hPow (β := ℤ) T (-(↑m : ℤ))) • B) ↔ C B
Tactic: rwa [sub_eq_neg_add, zpow_add, zpow_neg_one, ← prop_red_T hS hT, mul_smul, smul_inv_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.FixedDetMatrices (goal)
Goal:
m_1 : ℤ
C : FixedDetMatrix (Fin 2) ℤ m_1 → Prop
hS : ∀ (B : FixedDetMatrix (Fin 2) ℤ m_1), C B → C (S • B)
hT : ∀ (B : FixedDetMatrix (Fin 2) ℤ m_1), C B → C (T • B)
B : FixedDetMatrix (Fin 2) ℤ m_1
m : ℕ
hm : C (HPow.hPow (β := ℤ) T (-(↑m : ℤ)) • B) ↔ C B
pred : C (T ^ HAdd.hAdd (α := ℤ) (-1) (-(↑m : ℤ)) • B) ↔ C B
pred₁ : C ((HPow.hPow (β := ℤ) T (-1) * HPow.hPow (β := ℤ) T (-(↑m : ℤ))) • B) ↔ C B
⊢ C (T ^ HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1 • B) ↔ C B
have pred₂ : C ((T⁻¹ * HPow.hPow (β := ℤ) T (-(↑m : ℤ))) • B) ↔ C B
Tactic: rwa [sub_eq_neg_add, zpow_add, zpow_neg_one, ← prop_red_T hS hT, mul_smul, smul_inv_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.FixedDetMatrices (goal)
Goal:
m_1 : ℤ
C : FixedDetMatrix (Fin 2) ℤ m_1 → Prop
hS : ∀ (B : FixedDetMatrix (Fin 2) ℤ m_1), C B → C (S • B)
hT : ∀ (B : FixedDetMatrix (Fin 2) ℤ m_1), C B → C (T • B)
B : FixedDetMatrix (Fin 2) ℤ m_1
m : ℕ
hm : C (HPow.hPow (β := ℤ) T (-(↑m : ℤ)) • B) ↔ C B
pred : C (T ^ HAdd.hAdd (α := ℤ) (-1) (-(↑m : ℤ)) • B) ↔ C B
pred₁ : C ((HPow.hPow (β := ℤ) T (-1) * HPow.hPow (β := ℤ) T (-(↑m : ℤ))) • B) ↔ C B
pred₂ : C ((T⁻¹ * HPow.hPow (β := ℤ) T (-(↑m : ℤ))) • B) ↔ C B
⊢ C (T ^ HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1 • B) ↔ C B
have pred₃ : C (T • (T⁻¹ * HPow.hPow (β := ℤ) T (-(↑m : ℤ))) • B) ↔ C B
Tactic: rwa [sub_eq_neg_add, zpow_add, zpow_neg_one, ← prop_red_T hS hT, mul_smul, smul_inv_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.FixedDetMatrices (goal)
Goal:
m_1 : ℤ
C : FixedDetMatrix (Fin 2) ℤ m_1 → Prop
hS : ∀ (B : FixedDetMatrix (Fin 2) ℤ m_1), C B → C (S • B)
hT : ∀ (B : FixedDetMatrix (Fin 2) ℤ m_1), C B → C (T • B)
B : FixedDetMatrix (Fin 2) ℤ m_1
m : ℕ
hm : C (HPow.hPow (β := ℤ) T (-(↑m : ℤ)) • B) ↔ C B
pred : C (T ^ HAdd.hAdd (α := ℤ) (-1) (-(↑m : ℤ)) • B) ↔ C B
pred₁ : C ((HPow.hPow (β := ℤ) T (-1) * HPow.hPow (β := ℤ) T (-(↑m : ℤ))) • B) ↔ C B
pred₂ : C ((T⁻¹ * HPow.hPow (β := ℤ) T (-(↑m : ℤ))) • B) ↔ C B
pred₃ : C (T • (T⁻¹ * HPow.hPow (β := ℤ) T (-(↑m : ℤ))) • B) ↔ C B
⊢ C (T ^ HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1 • B) ↔ C B
have pred₄ : C (T • T⁻¹ • HPow.hPow (β := ℤ) T (-(↑m : ℤ)) • B) ↔ C B
Tactic: rwa [sub_eq_neg_add, zpow_add, zpow_neg_one, ← prop_red_T hS hT, mul_smul, smul_inv_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.FixedDetMatrices (goal)
Goal:
m : ℤ
C : FixedDetMatrix (Fin 2) ℤ m → Prop
hS : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (S • B)
hT : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (T • B)
B : FixedDetMatrix (Fin 2) ℤ m
n : ℤ
⊢ C (T ^ n • B) ↔ C B
have zero : C (HPow.hPow (β := ℤ) T 0 • B) ↔ C B
Tactic: induction n with
  | zero => simp only [zpow_zero, one_smul]
  | succ n hn =>
    simpa only [add_comm (n : ℤ), zpow_add _ 1, ← smul_eq_mul, zpow_one, smul_assoc,
      prop_red_T hS hT]
  | pred m hm =>
    rwa [sub_eq_neg_add, zpow_add, zpow_neg_one, ← prop_red_T hS hT, mul_smul, smul_inv_smul]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.FixedDetMatrices (goal)
Goal:
m : ℤ
C : FixedDetMatrix (Fin 2) ℤ m → Prop
hS : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (S • B)
hT : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (T • B)
B : FixedDetMatrix (Fin 2) ℤ m
n : ℤ
zero : C (HPow.hPow (β := ℤ) T 0 • B) ↔ C B
⊢ C (T ^ n • B) ↔ C B
have succ : ∀ (n : ℕ) (hn : C (HPow.hPow (β := ℤ) T (↑n : ℤ) • B) ↔ C B), C (T ^ HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 • B) ↔ C B
Tactic: induction n with
  | zero => simp only [zpow_zero, one_smul]
  | succ n hn =>
    simpa only [add_comm (n : ℤ), zpow_add _ 1, ← smul_eq_mul, zpow_one, smul_assoc,
      prop_red_T hS hT]
  | pred m hm =>
    rwa [sub_eq_neg_add, zpow_add, zpow_neg_one, ← prop_red_T hS hT, mul_smul, smul_inv_smul]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.FixedDetMatrices (goal)
Goal:
m : ℤ
C : FixedDetMatrix (Fin 2) ℤ m → Prop
hS : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (S • B)
hT : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (T • B)
B : FixedDetMatrix (Fin 2) ℤ m
n : ℤ
zero : C (HPow.hPow (β := ℤ) T 0 • B) ↔ C B
succ : ∀ (n : ℕ) (hn : C (HPow.hPow (β := ℤ) T (↑n : ℤ) • B) ↔ C B), C (T ^ HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 • B) ↔ C B
⊢ C (T ^ n • B) ↔ C B
have pred : ∀ (m_1 : ℕ) (hm : C (HPow.hPow (β := ℤ) T (-(↑m_1 : ℤ)) • B) ↔ C B),
  C (T ^ HSub.hSub (α := ℤ) (-(↑m_1 : ℤ)) 1 • B) ↔ C B
Tactic: induction n with
  | zero => simp only [zpow_zero, one_smul]
  | succ n hn =>
    simpa only [add_comm (n : ℤ), zpow_add _ 1, ← smul_eq_mul, zpow_one, smul_assoc,
      prop_red_T hS hT]
  | pred m hm =>
    rwa [sub_eq_neg_add, zpow_add, zpow_neg_one, ← prop_red_T hS hT, mul_smul, smul_inv_smul]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.FixedDetMatrices (goal)
Goal:
m : ℤ
C : FixedDetMatrix (Fin 2) ℤ m → Prop
A : FixedDetMatrix (Fin 2) ℤ m
hm : m ≠ 0
h0 :
  ∀ (A : FixedDetMatrix (Fin 2) ℤ m),
    (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0 →
      0 < (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0 →
        0 ≤ (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 →
          |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1| < |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1| → C A
hS : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (S • B)
hT : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (T • B)
⊢ C (reduce A)
have rcases : ∀ (H1 : (↑(reduce A) : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0) (H2 : 0 < (↑(reduce A) : Matrix (Fin 2) (Fin 2) ℤ) 0 0)
  (H3 : 0 ≤ (↑(reduce A) : Matrix (Fin 2) (Fin 2) ℤ) 0 1)
  (H4 : |(↑(reduce A) : Matrix (Fin 2) (Fin 2) ℤ) 0 1| < |(↑(reduce A) : Matrix (Fin 2) (Fin 2) ℤ) 1 1|), C (reduce A)
Tactic: rcases reduce_mem_reps hm A with ⟨H1, H2, H3, H4⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.FixedDetMatrices (goal)
Goal:
m : ℤ
C : FixedDetMatrix (Fin 2) ℤ m → Prop
A : FixedDetMatrix (Fin 2) ℤ m
hm : m ≠ 0
h0 :
  ∀ (A : FixedDetMatrix (Fin 2) ℤ m),
    (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0 →
      0 < (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0 →
        0 ≤ (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 →
          |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1| < |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1| → C A
hS : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (S • B)
hT : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (T • B)
⊢ C A
have have : ∀ (h_reduce : C (reduce A)), C A
Tactic: have h_reduce : C (reduce A) := by
    rcases reduce_mem_reps hm A with ⟨H1, H2, H3, H4⟩
    exact h0 _ H1 H2 H3 H4
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.FixedDetMatrices (goal)
Goal:
m : ℤ
C : FixedDetMatrix (Fin 2) ℤ m → Prop
A : FixedDetMatrix (Fin 2) ℤ m
hm : m ≠ 0
h0 :
  ∀ (A : FixedDetMatrix (Fin 2) ℤ m),
    (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0 →
      0 < (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0 →
        0 ≤ (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 →
          |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1| < |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1| → C A
hS : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (S • B)
hT : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (T • B)
h_reduce : C (reduce A)
⊢ C A
have suffices : ∀ (A : FixedDetMatrix (Fin 2) ℤ m), C (reduce A) → C A
Tactic: suffices ∀ A : Δ m, C (reduce A) → C A from this _ h_reduce
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.FixedDetMatrices (goal)
Goal:
m : ℤ
C : FixedDetMatrix (Fin 2) ℤ m → Prop
A : FixedDetMatrix (Fin 2) ℤ m
hm : m ≠ 0
h0 :
  ∀ (A : FixedDetMatrix (Fin 2) ℤ m),
    (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0 →
      0 < (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0 →
        0 ≤ (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 →
          |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1| < |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1| → C A
hS : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (S • B)
hT : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (T • B)
h_reduce : C (reduce A)
⊢ ∀ (A : FixedDetMatrix (Fin 2) ℤ m), C (reduce A) → C A
have base : ∀ (A : FixedDetMatrix (Fin 2) ℤ m), (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0 → C (reduce A) → C A
Tactic: apply reduce_rec
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.FixedDetMatrices (goal)
Goal:
m : ℤ
C : FixedDetMatrix (Fin 2) ℤ m → Prop
A : FixedDetMatrix (Fin 2) ℤ m
hm : m ≠ 0
h0 :
  ∀ (A : FixedDetMatrix (Fin 2) ℤ m),
    (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0 →
      0 < (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0 →
        0 ≤ (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 →
          |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1| < |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1| → C A
hS : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (S • B)
hT : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (T • B)
h_reduce : C (reduce A)
base : ∀ (A : FixedDetMatrix (Fin 2) ℤ m), (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0 → C (reduce A) → C A
⊢ ∀ (A : FixedDetMatrix (Fin 2) ℤ m), C (reduce A) → C A
have step : ∀ (A : FixedDetMatrix (Fin 2) ℤ m),
  (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 ≠ 0 → (C (reduce (reduceStep A)) → C (reduceStep A)) → C (reduce A) → C A
Tactic: apply reduce_rec
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.FixedDetMatrices (goal)
Goal:
m : ℤ
C : FixedDetMatrix (Fin 2) ℤ m → Prop
A_1 : FixedDetMatrix (Fin 2) ℤ m
hm : m ≠ 0
h0 :
  ∀ (A : FixedDetMatrix (Fin 2) ℤ m),
    (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0 →
      0 < (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0 →
        0 ≤ (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 →
          |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1| < |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1| → C A
hS : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (S • B)
hT : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (T • B)
h_reduce : C (reduce A_1)
A : FixedDetMatrix (Fin 2) ℤ m
h : (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
⊢ C (reduce A) → C A
have pos : ∀ (h1 : 0 < (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0), C (reduce A) → C A
Tactic: by_cases h1 : 0 < A.1 0 0
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.FixedDetMatrices (goal)
Goal:
m : ℤ
C : FixedDetMatrix (Fin 2) ℤ m → Prop
A_1 : FixedDetMatrix (Fin 2) ℤ m
hm : m ≠ 0
h0 :
  ∀ (A : FixedDetMatrix (Fin 2) ℤ m),
    (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0 →
      0 < (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0 →
        0 ≤ (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 →
          |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1| < |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1| → C A
hS : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (S • B)
hT : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (T • B)
h_reduce : C (reduce A_1)
A : FixedDetMatrix (Fin 2) ℤ m
h : (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
pos : ∀ (h1 : 0 < (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0), C (reduce A) → C A
⊢ C (reduce A) → C A
have neg : ∀ (h1 : ¬0 < (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0), C (reduce A) → C A
Tactic: by_cases h1 : 0 < A.1 0 0
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.FixedDetMatrices (hypothesis)
Goal:
m : ℤ
C : FixedDetMatrix (Fin 2) ℤ m → Prop
A_1 : FixedDetMatrix (Fin 2) ℤ m
hm : m ≠ 0
h0 :
  ∀ (A : FixedDetMatrix (Fin 2) ℤ m),
    (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0 →
      0 < (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0 →
        0 ≤ (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 →
          |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1| < |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1| → C A
hS : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (S • B)
hT : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (T • B)
h_reduce : C (reduce A_1)
A : FixedDetMatrix (Fin 2) ℤ m
hc : (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 ≠ 0
ih : C (reduce (reduceStep A)) → C (reduceStep A)
hA : C (reduce A)
⊢ C A
have hA₁ : C (reduce (reduceStep A))
Tactic: rw [← reduce_reduceStep hc] at hA
Cleared hypotheses: hA
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.FixedDetMatrices (hypothesis)
Goal:
A : FixedDetMatrix (Fin 2) ℤ 1
a1 : (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
a4 : 0 < (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0
a6 : |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1| < |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1|
⊢ A = 1
have this : (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 1 ∧ (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 1 ∨
  (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = -1 ∧ (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = -1
Tactic: have := Int.mul_eq_one_iff_eq_one_or_neg_one.mp (A_c_eq_zero a1)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.FixedDetMatrices (goal)
Goal:
A : FixedDetMatrix (Fin 2) ℤ 1
a1 : (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
a4 : 0 < (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0
a6 : |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1| < |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1|
this :
  (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 1 ∧ (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 1 ∨
    (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = -1 ∧ (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = -1
⊢ A = 1
have h : ∀ (i j : Fin 2), (↑A : Matrix (Fin 2) (Fin 2) ℤ) i j = (↑1 : Matrix (Fin 2) (Fin 2) ℤ) i j
Tactic: ext i j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.FixedDetMatrices (goal)
Goal:
A : FixedDetMatrix (Fin 2) ℤ 1
a1 : (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
a4 : 0 < (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0
a6 : |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1| < |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1|
this :
  (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 1 ∧ (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 1 ∨
    (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = -1 ∧ (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = -1
i j : Fin 2
⊢ (↑A : Matrix (Fin 2) (Fin 2) ℤ) i j = (↑1 : Matrix (Fin 2) (Fin 2) ℤ) i j
have h : (↑A : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2)) j =
  (↑1 : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩) j
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.FixedDetMatrices (goal)
Goal:
A : FixedDetMatrix (Fin 2) ℤ 1
a1 : (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
a4 : 0 < (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0
a6 : |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1| < |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1|
this :
  (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 1 ∧ (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 1 ∨
    (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = -1 ∧ (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = -1
i j : Fin 2
h :
  (↑A : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) j =
    (↑1 : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) j
⊢ (↑A : Matrix (Fin 2) (Fin 2) ℤ) i j = (↑1 : Matrix (Fin 2) (Fin 2) ℤ) i j
have h₁ : (↑A : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2)) j =
  (↑1 : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩) j
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.FixedDetMatrices (goal)
Goal:
A : FixedDetMatrix (Fin 2) ℤ 1
a1 : (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
a4 : 0 < (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0
a6 : |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1| < |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1|
this :
  (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 1 ∧ (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 1 ∨
    (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = -1 ∧ (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = -1
j : Fin 2
⊢ (↑A : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) j =
    (↑1 : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) j
have h : (↑A : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2)) =
  (↑1 : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩) ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩)
Tactic: fin_cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.FixedDetMatrices (goal)
Goal:
A : FixedDetMatrix (Fin 2) ℤ 1
a1 : (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
a4 : 0 < (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0
a6 : |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1| < |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1|
this :
  (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 1 ∧ (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 1 ∨
    (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = -1 ∧ (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = -1
j : Fin 2
h :
  (↑A : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) =
    (↑1 : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)
⊢ (↑A : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) j =
    (↑1 : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) j
have h₁ : (↑A : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2)) =
  (↑1 : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩) ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩)
Tactic: fin_cases j
Cleared hypotheses: j