awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
Goal:
A : FixedDetMatrix (Fin 2) ℤ 0
h₁ : (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
h₂ : 0 < (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0
h₄ : |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1| < |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1|
⊢ (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 0

Tactic:
have := A_c_eq_zero h₁
-- Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
Goal:
A : FixedDetMatrix (Fin 2) ℤ 0
h₁ : (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
h₂ : 0 < (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0
h₄ : |(↑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 * (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 0
⊢ |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1| < 0

Tactic:
simp_all [h₂.ne']

Premises used: LT.lt.ne'
-- Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
Goal:
n : Type u_1
inst : DecidableEq n
inst_1 : Fintype n
R : Type u_2
inst_2 : CommRing R
m k : ℤ
H : Finset ℤ := Finset.Icc (-|k|) |k|
H4 : Type := Fin 2 → Fin 2 → ↥H
apply :
  Function.Injective (β := H4) fun (M : (↑(reps k) : Type)) (i j : Fin 2) ↦
    Subtype.mk (p := fun (x : ℤ) ↦ x ∈ H) ((↑(↑M : FixedDetMatrix (Fin 2) ℤ k) : Matrix (Fin 2) (Fin 2) ℤ) i j) ⋯
⊢ Fintype (↑(reps k) : Type)

Tactic:
apply Fintype.ofInjective (β := H4) (f := fun M i j ↦ ⟨M.1.1 i j, reps_entries_le_m' M.2 i j⟩)

Premises used: Subtype.mk, Fintype.ofInjective
-- Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
Goal:
n : Type u_1
inst : DecidableEq n
inst_1 : Fintype n
R : Type u_2
inst_2 : CommRing R
m k : ℤ
H : Finset ℤ := Finset.Icc (-|k|) |k|
H4 : Type := Fin 2 → Fin 2 → ↥H
M N : (↑(reps k) : Type)
h :
  Eq (α := H4)
    ((fun (M : (↑(reps k) : Type)) (i j : Fin 2) ↦
        (Subtype.mk (p := fun (x : ℤ) ↦ x ∈ H) ((↑(↑M : FixedDetMatrix (Fin 2) ℤ k) : Matrix (Fin 2) (Fin 2) ℤ) i j) ⋯ :
          ↥H))
      M)
    ((fun (M : (↑(reps k) : Type)) (i j : Fin 2) ↦
        (Subtype.mk (p := fun (x : ℤ) ↦ x ∈ H) ((↑(↑M : FixedDetMatrix (Fin 2) ℤ k) : Matrix (Fin 2) (Fin 2) ℤ) i j) ⋯ :
          ↥H))
      N)
a :
  ∀ (i j : Fin 2),
    (↑(↑M : FixedDetMatrix (Fin 2) ℤ k) : Matrix (Fin 2) (Fin 2) ℤ) i j =
      (↑(↑N : FixedDetMatrix (Fin 2) ℤ k) : Matrix (Fin 2) (Fin 2) ℤ) i j
⊢ M = N

Tactic:
ext i j
-- Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
Goal:
n : Type u_1
inst : DecidableEq n
inst_1 : Fintype n
R : Type u_2
inst_2 : CommRing R
m k : ℤ
H : Finset ℤ := Finset.Icc (-|k|) |k|
H4 : Type := Fin 2 → Fin 2 → ↥H
M N : (↑(reps k) : Type)
h :
  Eq (α := H4)
    ((fun (M : (↑(reps k) : Type)) (i j : Fin 2) ↦
        (Subtype.mk (p := fun (x : ℤ) ↦ x ∈ H) ((↑(↑M : FixedDetMatrix (Fin 2) ℤ k) : Matrix (Fin 2) (Fin 2) ℤ) i j) ⋯ :
          ↥H))
      M)
    ((fun (M : (↑(reps k) : Type)) (i j : Fin 2) ↦
        (Subtype.mk (p := fun (x : ℤ) ↦ x ∈ H) ((↑(↑M : FixedDetMatrix (Fin 2) ℤ k) : Matrix (Fin 2) (Fin 2) ℤ) i j) ⋯ :
          ↥H))
      N)
i j : Fin 2
⊢ (↑(↑M : FixedDetMatrix (Fin 2) ℤ k) : Matrix (Fin 2) (Fin 2) ℤ) i j =
    (↑(↑N : FixedDetMatrix (Fin 2) ℤ k) : Matrix (Fin 2) (Fin 2) ℤ) i j

Tactic:
simpa only [Subtype.mk.injEq] using congrFun₂ h i j

Premises used: congrFun₂, Subtype.mk.injEq
-- Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
Goal:
m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
⊢ S • S • S • S • A = A

Tactic:
simp only [smul_def, ← mul_assoc, S_mul_S_eq, neg_mul, one_mul, mul_neg, neg_neg, Subtype.coe_eta]

Premises used: mul_assoc, neg_neg, Subtype.coe_eta, FixedDetMatrices.smul_def, neg_mul, ModularGroup.S_mul_S_eq, one_mul, mul_neg
-- Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
Goal:
m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
simp_rw : S • S • S • T • S • T • S • A = (S • S • S • T • S • T • S) • A
⊢ S • S • S • T • S • T • S • A = T⁻¹ • A

Tactic:
simp_rw [← T_S_rel, ← smul_assoc]

Premises used: smul_assoc, ModularGroup.T_S_rel
-- Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
Goal:
m : ℤ
hm : m ≠ 0
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:
simpa only [reduce_reduceStep h1] using h2

Premises used: FixedDetMatrices.reduce_reduceStep
-- Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
Goal:
m : ℤ
hm : m ≠ 0
A : FixedDetMatrix (Fin 2) ℤ m
h : (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
⊢ (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1 ≠ 0

Tactic:
have hd := A_d_ne_zero h hm
-- Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
Goal:
m : ℤ
hm : m ≠ 0
A : FixedDetMatrix (Fin 2) ℤ m
h : (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
hd : (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1 ≠ 0
pos : ∀ (h1 : 0 < (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0), reduce A ∈ reps m
neg : ∀ (h1 : ¬0 < (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0), reduce A ∈ reps m
⊢ reduce A ∈ reps m

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

Premises used: OfNat.ofNat, Subtype.val
-- Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
Goal:
m : ℤ
hm : m ≠ 0
A : FixedDetMatrix (Fin 2) ℤ m
h : (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
hd : (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1 ≠ 0
h1 : 0 < (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0
pos : T ^ (-((↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 / (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1)) • A ∈ reps m
⊢ reduce A ∈ reps m

Tactic:
simp only [reduce_of_pos h h1]

Premises used: FixedDetMatrices.reduce_of_pos
-- Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
Goal:
m : ℤ
hm : m ≠ 0
A : FixedDetMatrix (Fin 2) ℤ m
h : (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
hd : (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1 ≠ 0
h1 : 0 < (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0
⊢ (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 % (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1 =
    (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 -
      (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1 * ((↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 / (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1)

Tactic:
have h2 := Int.emod_def (A.1 0 1) (A.1 1 1)
-- Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
Goal:
m : ℤ
hm : m ≠ 0
A : FixedDetMatrix (Fin 2) ℤ m
h : (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
hd : (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1 ≠ 0
h1 : 0 < (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0
h2 :
  (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 % (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1 =
    (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 -
      (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1 * ((↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 / (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1)
⊢ (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 / (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1 * (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1 ≤
    (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1

Tactic:
have h4 := Int.ediv_mul_le (A.1 0 1) hd
-- Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
Goal:
m : ℤ
hm : m ≠ 0
A : FixedDetMatrix (Fin 2) ℤ m
h : (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
hd : (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1 ≠ 0
h1 : 0 < (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0
h2 :
  (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 % (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1 =
    (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 -
      (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1 * ((↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 / (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1)
h4 :
  (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 / (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1 * (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1 ≤
    (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1
pos :
  let n := (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 / (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1;
  ∀
    (h2 :
      (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 % (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1 =
        (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 - (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1 * n)
    (h4 : n * (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1 ≤ (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1), T ^ (-n) • A ∈ reps m
⊢ T ^ (-((↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 / (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1)) • A ∈ reps m

Tactic:
set n : ℤ := A.1 0 1 / A.1 1 1

Premises used: OfNat.ofNat, Subtype.val
-- Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
Goal:
m : ℤ
hm : m ≠ 0
A : FixedDetMatrix (Fin 2) ℤ m
h : (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
hd : (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1 ≠ 0
h1 : 0 < (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0
n : ℤ := (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 / (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1
h2 :
  (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 % (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1 =
    (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 - (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1 * n
h4 : n * (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1 ≤ (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1
⊢ (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 % (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1 < |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1|

Tactic:
have h3 := Int.emod_lt_abs (A.1 0 1) hd
-- Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
Goal:
m : ℤ
hm : m ≠ 0
A : FixedDetMatrix (Fin 2) ℤ m
h : (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
hd : (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1 ≠ 0
h1 : 0 < (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0
n : ℤ := (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 / (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1
h2 :
  (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 % (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1 =
    (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 - (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1 * n
h4 : n * (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1 ≤ (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1
h3 : (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 % (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1 < |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1|
⊢ |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 % (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1| < |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1|

Tactic:
rw [← abs_eq_self.mpr <| Int.emod_nonneg _ hd] at h3

Premises used: Iff.mpr, abs_eq_self, Int.emod_nonneg
-- Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
Goal:
m : ℤ
hm : m ≠ 0
A : FixedDetMatrix (Fin 2) ℤ m
h : (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
hd : (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1 ≠ 0
h1 : 0 < (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0
n : ℤ := (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 / (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1
h2 :
  (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 % (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1 =
    (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 - (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1 * n
h4 : n * (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1 ≤ (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1
h3 : |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 % (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1| < |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1|
pos :
  Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) ℤ) ↦ A.det = m)
      (HMul.hMul (α := Matrix (Fin 2) (Fin 2) ℤ) (!![1, -n; 0, 1] : Matrix (Fin 2) (Fin 2) ℤ)
        (↑A : Matrix (Fin 2) (Fin 2) ℤ))
      ⋯ ∈
    reps m
⊢ T ^ (-n) • A ∈ reps m

Tactic:
simp only [smul_def, coe_T_zpow]

Premises used: FixedDetMatrices.smul_def, ModularGroup.coe_T_zpow
-- Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
Goal:
m : ℤ
hm : m ≠ 0
A : FixedDetMatrix (Fin 2) ℤ m
h : (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
hd : (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1 ≠ 0
h1 : 0 < (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0
n : ℤ := (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 / (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1
h2 :
  (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 % (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1 =
    (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 - (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1 * n
h4 : n * (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1 ≤ (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1
h3 : |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 % (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1| < |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1|
this :
  (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0 ∧
    n * (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 < (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0 ∧
      n * (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1 ≤ (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 ∧
        |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 + -(n * (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1)| <
          |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1|
⊢ Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) ℤ) ↦ A.det = m)
      (HMul.hMul (α := Matrix (Fin 2) (Fin 2) ℤ) (!![1, -n; 0, 1] : Matrix (Fin 2) (Fin 2) ℤ)
        (↑A : Matrix (Fin 2) (Fin 2) ℤ))
      ⋯ ∈
    reps m

Tactic:
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]

Premises used: lt_add_neg_iff_add_lt, Nat.succ_eq_add_one, Equiv.symm_apply_apply, MulZeroClass.zero_mul, Matrix.cons_val_one, Matrix.vecMul, Matrix.cons_val_zero, Matrix.cons_dotProduct, Matrix.empty_val', Nat.reduceAdd, Matrix.cons_val_fin_one, Set.mem_setOf_eq, Matrix.dotProduct_of_isEmpty, le_add_neg_iff_add_le, Fin.succ_zero_eq_one, Matrix.of_apply, Matrix.cons_mul, zero_add, FixedDetMatrices.reps, Fin.isValue, Matrix.vecHead, Matrix.empty_mul, Function.comp_apply, neg_mul, add_zero, Matrix.vecTail, one_mul, Matrix.cons_val'
-- Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
Goal:
m : ℤ
hm : m ≠ 0
A : FixedDetMatrix (Fin 2) ℤ m
h : (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
hd : (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1 ≠ 0
h1 : 0 < (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0
n : ℤ := (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 / (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1
h2 :
  (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 % (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1 =
    (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 - (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1 * n
h4 : n * (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1 ≤ (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1
h3 : |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 % (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1| < |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1|
pos :
  (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0 ∧
    n * (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 < (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0 ∧
      n * (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1 ≤ (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 ∧
        |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 + -(n * (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1)| <
          |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1|
⊢ Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) ℤ) ↦ A.det = m)
      (HMul.hMul (α := Matrix (Fin 2) (Fin 2) ℤ) (!![1, -n; 0, 1] : Matrix (Fin 2) (Fin 2) ℤ)
        (↑A : Matrix (Fin 2) (Fin 2) ℤ))
      ⋯ ∈
    reps m

Tactic:
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]
-- Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
Goal:
m : ℤ
hm : m ≠ 0
A : FixedDetMatrix (Fin 2) ℤ m
h : (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
hd : (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1 ≠ 0
h1 : 0 < (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0
n : ℤ := (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 / (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1
h2 :
  (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 % (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1 =
    (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 - (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1 * n
h4 : n * (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1 ≤ (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1
h3 : |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 % (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1| < |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1|
⊢ (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0 ∧
    n * (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 < (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0 ∧
      n * (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1 ≤ (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 ∧
        |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 + -(n * (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1)| <
          |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1|

Tactic:
simp_all only [mul_comm n, zero_mul, ← sub_eq_add_neg, ← h2,
        Fin.isValue, and_true]

Premises used: and_true, MulZeroClass.zero_mul, sub_eq_add_neg, Fin.isValue, mul_comm
-- Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
Goal:
m : ℤ
hm : m ≠ 0
A : FixedDetMatrix (Fin 2) ℤ m
h : (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
hd : (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1 ≠ 0
h1 : ¬0 < (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0
neg :
  (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0 < 0 ∧
    -(↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 / (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1 * (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1 ≤
        -(↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 ∧
      |-(-(↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 / (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1 *
                (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1) +
            -(↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1| <
        |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1|
⊢ reduce A ∈ reps m

Tactic:
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]

Premises used: neg_add_rev, lt_neg, abs_neg, Matrix.neg_cons, Nat.succ_eq_add_one, Equiv.symm_apply_apply, MulZeroClass.zero_mul, Matrix.cons_val_one, mul_assoc, Matrix.vecMul, Matrix.neg_of, Matrix.cons_val_zero, Int.ediv_neg, le_neg, Matrix.cons_dotProduct, Matrix.empty_val', neg_neg, Nat.reduceAdd, Matrix.cons_val_fin_one, Set.mem_setOf_eq, Matrix.dotProduct_of_isEmpty, le_add_neg_iff_add_le, Fin.succ_zero_eq_one, Matrix.of_apply, Matrix.cons_mul, zero_add, FixedDetMatrices.reps, MulZeroClass.mul_zero, Fin.isValue, Matrix.vecHead, Matrix.empty_mul, FixedDetMatrices.smul_def, FixedDetMatrices.reduce_of_not_pos, Function.comp_apply, neg_mul, add_zero, ModularGroup.coe_T_zpow, Matrix.neg_empty, neg_zero, Matrix.vecTail, Pi.neg_apply, ModularGroup.S_mul_S_eq, one_mul, true_and, mul_neg, Matrix.cons_val'
-- Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
Goal:
m : ℤ
hm : m ≠ 0
A : FixedDetMatrix (Fin 2) ℤ m
h : (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
hd : (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1 ≠ 0
h1 : ¬0 < (↑A : Matrix (Fin 2) (Fin 2) ℤ) 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) ℤ) 1 1 * (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1 ≤
        -(↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 ∧
      |-(-(↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 / (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1 *
                (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1) +
            -(↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1| <
        |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1|

Tactic:
⟨?_, Int.ediv_mul_le _ hd, ?_⟩

Premises used: Int.ediv_mul_le, And.intro
-- Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
Goal:
m : ℤ
hm : m ≠ 0
A : FixedDetMatrix (Fin 2) ℤ m
h : (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
hd : (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1 ≠ 0
h1 : ¬0 < (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0
neg : (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0 < 0
neg₁ :
  |-(-(↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 / (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1 * (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1) +
        -(↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1| <
    |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1|
⊢ (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0 < 0 ∧
    -(↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 / (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1 * (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1 ≤
        -(↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 ∧
      |-(-(↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 / (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1 *
                (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1) +
            -(↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1| <
        |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1|

Tactic:
refine ⟨?_, Int.ediv_mul_le _ hd, ?_⟩
-- Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
Goal:
m : ℤ
hm : m ≠ 0
A : FixedDetMatrix (Fin 2) ℤ m
h : (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
hd : (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1 ≠ 0
h1 : ¬0 < (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0
neg : (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0 ≤ 0 ∧ (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0 ≠ 0
⊢ (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0 < 0

Tactic:
simp only [Int.lt_iff_le_and_ne]

Premises used: Int.lt_iff_le_and_ne
-- Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
Goal:
m : ℤ
hm : m ≠ 0
A : FixedDetMatrix (Fin 2) ℤ m
h : (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
hd : (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1 ≠ 0
h1 : ¬0 < (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0
⊢ (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0 ≤ 0 ∧ (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0 ≠ 0

Tactic:
⟨not_lt.mp h1, A_a_ne_zero h hm⟩

Premises used: not_lt, And.intro, Iff.mp, _private.0.FixedDetMatrices.A_a_ne_zero
-- Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
Goal:
m : ℤ
hm : m ≠ 0
A : FixedDetMatrix (Fin 2) ℤ m
h : (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
hd : (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1 ≠ 0
h1 : ¬0 < (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0
⊢ (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0 ≤ 0 ∧ (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0 ≠ 0

Tactic:
exact ⟨not_lt.mp h1, A_a_ne_zero h hm⟩
-- Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
Goal:
m : ℤ
hm : m ≠ 0
A : FixedDetMatrix (Fin 2) ℤ m
h : (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
hd : (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1 ≠ 0
h1 : ¬0 < (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0
neg : -(↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 % (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1 < |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1|
⊢ |-(-(↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 / (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1 * (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1) +
        -(↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1| <
    |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1|

Tactic:
rw [mul_comm, add_comm, ← Int.sub_eq_add_neg, ← Int.emod_def,
         abs_eq_self.mpr <| Int.emod_nonneg _ hd]

Premises used: Iff.mpr, Int.sub_eq_add_neg, add_comm, mul_comm, Int.emod_def, abs_eq_self, Int.emod_nonneg
-- Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
Goal:
m : ℤ
hm : m ≠ 0
A : FixedDetMatrix (Fin 2) ℤ m
h : (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
hd : (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1 ≠ 0
h1 : ¬0 < (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0
⊢ -(↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 % (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1 < |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1|

Tactic:
Int.emod_lt_abs _ hd

Premises used: Int.emod_lt_abs
-- Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
Goal:
m : ℤ
hm : m ≠ 0
A : FixedDetMatrix (Fin 2) ℤ m
h : (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
hd : (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1 ≠ 0
h1 : ¬0 < (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0
⊢ -(↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 % (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1 < |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1|

Tactic:
exact Int.emod_lt_abs _ hd

Premises used: Int.emod_lt_abs
-- Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
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

Tactic:
⟨?_, hS _⟩

Premises used: Iff.intro
-- Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
Goal:
m : ℤ
C : FixedDetMatrix (Fin 2) ℤ m → Prop
hS : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (S • B)
B : FixedDetMatrix (Fin 2) ℤ m
refine : C (S • B) → C B
⊢ C (S • B) ↔ C B

Tactic:
refine ⟨?_, hS _⟩
-- Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
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)
rw : C (S • S • S • S • B)
⊢ C B

Tactic:
rw [← (S_smul_four B)]

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

Tactic:
solve_by_elim
-- 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 (T • B) ↔ C B

Tactic:
⟨?_, hT _⟩

Premises used: Iff.intro