awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
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
refine : C (T • B) → C B
⊢ C (T • B) ↔ C B

Tactic:
refine ⟨?_, hT _⟩
-- Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
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)
⊢ B = T⁻¹ • T • B

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
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)
rw : C (S • S • S • T • S • T • S • T • B)
⊢ C B

Tactic:
rw [show B = T⁻¹ • T • B by simp, ← T_S_rel_smul]

Premises used: FixedDetMatrices.T_S_rel_smul
-- Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
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 (S • S • S • T • S • T • S • T • B)

Tactic:
solve_by_elim (maxDepth := 10)
-- Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
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 (HPow.hPow (β := ℤ) T 0 • B) ↔ C B

Tactic:
simp only [zpow_zero, one_smul]

Premises used: zpow_zero, one_smul
-- Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
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 : ℕ
hn : C (HPow.hPow (β := ℤ) T (↑n : ℤ) • B) ↔ C B
⊢ C (T ^ HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 • B) ↔ C B

Tactic:
simpa only [add_comm (n : ℤ), zpow_add _ 1, ← smul_eq_mul, zpow_one, smul_assoc,
      prop_red_T hS hT]

Premises used: zpow_add, smul_assoc, _private.0.FixedDetMatrices.prop_red_T, zpow_one, Nat.cast, add_comm, smul_eq_mul, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
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
pred₄ : C (T • T⁻¹ • HPow.hPow (β := ℤ) T (-(↑m : ℤ)) • B) ↔ C B
pred₅ pred₆ pred₇ pred₈ : C (HPow.hPow (β := ℤ) T (-(↑m : ℤ)) • B) ↔ C B
⊢ C (T ^ HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1 • B) ↔ C B

Tactic:
rwa [sub_eq_neg_add, zpow_add, zpow_neg_one, ← prop_red_T hS hT, mul_smul, smul_inv_smul]

Premises used: zpow_add, zpow_neg_one, _private.0.FixedDetMatrices.prop_red_T, sub_eq_neg_add, smul_inv_smul, SemigroupAction.mul_smul
-- Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
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
pred :
  ∀ (m_1 : ℕ) (hm : C (HPow.hPow (β := ℤ) T (-(↑m_1 : ℤ)) • B) ↔ C B),
    C (T ^ HSub.hSub (α := ℤ) (-(↑m_1 : ℤ)) 1 • B) ↔ C B
⊢ C (T ^ n • 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]

Premises used: zpow_add, smul_assoc, zpow_neg_one, _private.0.FixedDetMatrices.prop_red_T, sub_eq_neg_add, zpow_zero, zpow_one, smul_inv_smul, add_comm, one_smul, smul_eq_mul, OfNat.ofNat, Matrix.zero, SemigroupAction.mul_smul
-- Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
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)
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)
⊢ C (reduce A)

Tactic:
rcases reduce_mem_reps hm A with ⟨H1, H2, H3, H4⟩

Premises used: FixedDetMatrices.reduce_mem_reps
-- Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
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)
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:
h0 _ H1 H2 H3 H4
-- Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
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)
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:
exact h0 _ H1 H2 H3 H4
-- Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
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)
have : ∀ (h_reduce : C (reduce A)), C 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
-- Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
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)
suffices : ∀ (A : FixedDetMatrix (Fin 2) ℤ m), C (reduce A) → C A
⊢ C A

Tactic:
suffices ∀ A : Δ m, C (reduce A) → C A from this _ h_reduce
-- Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
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
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
⊢ ∀ (A : FixedDetMatrix (Fin 2) ℤ m), C (reduce A) → C A

Tactic:
apply reduce_rec
-- Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
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
neg : ∀ (h1 : ¬0 < (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0), C (reduce A) → C A
⊢ C (reduce A) → C A

Tactic:
by_cases h1 : 0 < A.1 0 0

Premises used: OfNat.ofNat, Subtype.val
-- Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
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
h1 : 0 < (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0
⊢ C (reduce A) → C A

Tactic:
simp only [reduce_of_pos h h1, prop_red_T_pow hS hT, imp_self]

Premises used: FixedDetMatrices.reduce_of_pos, imp_self, _private.0.FixedDetMatrices.prop_red_T_pow
-- Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
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
h1 : ¬0 < (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0
⊢ C (reduce A) → C A

Tactic:
simp only [reduce_of_not_pos h h1, prop_red_T_pow hS hT, prop_red_S hS, imp_self]

Premises used: _private.0.FixedDetMatrices.prop_red_S, imp_self, FixedDetMatrices.reduce_of_not_pos, _private.0.FixedDetMatrices.prop_red_T_pow
-- Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
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 (reduce (reduceStep A))

Tactic:
rw [← reduce_reduceStep hc] at hA

Premises used: FixedDetMatrices.reduce_reduceStep
-- Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
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 (reduceStep A))
⊢ C A

Tactic:
simpa only [reduceStep, prop_red_S hS, prop_red_T_pow hS hT] using ih hA

Premises used: _private.0.FixedDetMatrices.prop_red_S, FixedDetMatrices.reduceStep, _private.0.FixedDetMatrices.prop_red_T_pow
-- Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
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 : 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)
-- Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
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
h : ∀ (i j : Fin 2), (↑A : Matrix (Fin 2) (Fin 2) ℤ) i j = (↑1 : Matrix (Fin 2) (Fin 2) ℤ) i j
⊢ A = 1

Tactic:
ext i j
-- Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
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
h₁ :
  (↑A : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) j =
    (↑1 : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) j
⊢ (↑A : Matrix (Fin 2) (Fin 2) ℤ) i j = (↑1 : Matrix (Fin 2) (Fin 2) ℤ) i j

Tactic:
fin_cases i
-- Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
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, ⋯⟩)
h₁ :
  (↑A : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) =
    (↑1 : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)
⊢ (↑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

Tactic:
fin_cases j
-- Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
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) (⟨1, ⋯⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) =
    (↑1 : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)
h₁ :
  (↑A : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) =
    (↑1 : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)
⊢ (↑A : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) j =
    (↑1 : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) j

Tactic:
fin_cases j
-- Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
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 : 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, ⋯⟩)

Tactic:
aesop
-- Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
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 : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) =
    (↑1 : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)

Tactic:
aesop
-- Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
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 : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) =
    (↑1 : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)

Tactic:
aesop
-- Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
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 : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) =
    (↑1 : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)

Tactic:
aesop
-- Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
Goal:
rw : ∀ (x : SL(2, ℤ)), Membership.mem (γ := Subgroup SL(2, ℤ)) (closure {S, T}) x
⊢ Eq (α := Subgroup SL(2, ℤ)) (closure {S, T}) ⊤

Tactic:
rw [eq_top_iff']

Premises used: Subgroup.eq_top_iff'
-- Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
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
h : 0 ≤ (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1
a6 : |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1| < |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1|
h0 : Membership.mem (γ := Subgroup SL(2, ℤ)) (closure {S, T}) 1
⊢ Membership.mem (γ := Subgroup SL(2, ℤ)) (closure {S, T}) A

Tactic:
rw [reps_one_id A a1 a4 a6]

Premises used: FixedDetMatrices.reps_one_id
-- Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
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
h : 0 ≤ (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1
a6 : |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1| < |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1|
⊢ Membership.mem (γ := Subgroup SL(2, ℤ)) (closure {S, T}) 1

Tactic:
one_mem _

Premises used: OneMemClass.one_mem
-- Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
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
h : 0 ≤ (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1
a6 : |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1| < |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1|
⊢ Membership.mem (γ := Subgroup SL(2, ℤ)) (closure {S, T}) 1

Tactic:
exact one_mem _

Premises used: OneMemClass.one_mem
-- Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
Goal:
B : FixedDetMatrix (Fin 2) ℤ 1
hb : Membership.mem (γ := Subgroup SL(2, ℤ)) (closure {S, T}) B
⊢ Membership.mem (γ := Subgroup SL(2, ℤ)) (closure {S, T}) (S • B)

Tactic:
mul_mem (subset_closure (Set.mem_insert S {T})) hb

Premises used: Set.Mem, ModularGroup.T, ModularGroup.S, Subgroup.subset_closure, Set.mem_insert, Singleton.singleton, MulMemClass.mul_mem
-- Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
Goal:
B : FixedDetMatrix (Fin 2) ℤ 1
hb : Membership.mem (γ := Subgroup SL(2, ℤ)) (closure {S, T}) B
⊢ Membership.mem (γ := Subgroup SL(2, ℤ)) (closure {S, T}) (S • B)

Tactic:
exact mul_mem (subset_closure (Set.mem_insert S {T})) hb

Premises used: ModularGroup.T, ModularGroup.S, Subgroup.subset_closure, Set.mem_insert, Singleton.singleton, MulMemClass.mul_mem
-- Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
Goal:
B : FixedDetMatrix (Fin 2) ℤ 1
hb : Membership.mem (γ := Subgroup SL(2, ℤ)) (closure {S, T}) B
⊢ Membership.mem (γ := Subgroup SL(2, ℤ)) (closure {S, T}) (T • B)

Tactic:
mul_mem (subset_closure (Set.mem_insert_of_mem S rfl)) hb

Premises used: Set.Mem, Set.mem_insert_of_mem, ModularGroup.S, Subgroup.subset_closure, rfl, MulMemClass.mul_mem