-- Mathlib/LinearAlgebra/Matrix/FixedDetMatrices.lean
lemma reduce_mem_reps {m : ℤ} (hm : m ≠ 0) (A : Δ m) : reduce A ∈ reps m

Proof state:
case base
m : ℤ
hm : m ≠ 0
A : FixedDetMatrix (Fin 2) ℤ m
h : ↑A 1 0 = 0
hd : ↑A 1 1 ≠ 0
⊢ reduce A ∈ reps m

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

Result:
case pos
m : ℤ
hm : m ≠ 0
A : FixedDetMatrix (Fin 2) ℤ m
h : ↑A 1 0 = 0
hd : ↑A 1 1 ≠ 0
h1 : 0 < ↑A 0 0
⊢ reduce A ∈ reps m

case neg
m : ℤ
hm : m ≠ 0
A : FixedDetMatrix (Fin 2) ℤ m
h : ↑A 1 0 = 0
hd : ↑A 1 1 ≠ 0
h1 : ¬0 < ↑A 0 0
⊢ reduce A ∈ reps m

Proof state:
case pos
m : ℤ
hm : m ≠ 0
A : FixedDetMatrix (Fin 2) ℤ m
h : ↑A 1 0 = 0
hd : ↑A 1 1 ≠ 0
h1 : 0 < ↑A 0 0
⊢ T ^ (-(↑A 0 1 / ↑A 1 1)) • A ∈ reps m

Tactic:
have h2 := Int.emod_def (A.1 0 1) (A.1 1 1)

Result:
case pos
m : ℤ
hm : m ≠ 0
A : FixedDetMatrix (Fin 2) ℤ m
h : ↑A 1 0 = 0
hd : ↑A 1 1 ≠ 0
h1 : 0 < ↑A 0 0
h2 : ↑A 0 1 % ↑A 1 1 = ↑A 0 1 - ↑A 1 1 * (↑A 0 1 / ↑A 1 1)
⊢ T ^ (-(↑A 0 1 / ↑A 1 1)) • A ∈ reps m

Proof state:
case neg.refine_1
m : ℤ
hm : m ≠ 0
A : FixedDetMatrix (Fin 2) ℤ m
h : ↑A 1 0 = 0
hd : ↑A 1 1 ≠ 0
h1 : ¬0 < ↑A 0 0
⊢ ↑A 0 0 < 0

Tactic:
simp only [Int.lt_iff_le_and_ne]

Result:
case neg.refine_1
m : ℤ
hm : m ≠ 0
A : FixedDetMatrix (Fin 2) ℤ m
h : ↑A 1 0 = 0
hd : ↑A 1 1 ≠ 0
h1 : ¬0 < ↑A 0 0
⊢ ↑A 0 0 ≤ 0 ∧ ↑A 0 0 ≠ 0

Proof state:
case neg
m : ℤ
hm : m ≠ 0
A : FixedDetMatrix (Fin 2) ℤ m
h : ↑A 1 0 = 0
hd : ↑A 1 1 ≠ 0
h1 : ¬0 < ↑A 0 0
⊢ ↑A 0 0 < 0 ∧ -↑A 0 1 / ↑A 1 1 * ↑A 1 1 ≤ -↑A 0 1 ∧ |-(-↑A 0 1 / ↑A 1 1 * ↑A 1 1) + -↑A 0 1| < |↑A 1 1|

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

Result:
case neg.refine_1
m : ℤ
hm : m ≠ 0
A : FixedDetMatrix (Fin 2) ℤ m
h : ↑A 1 0 = 0
hd : ↑A 1 1 ≠ 0
h1 : ¬0 < ↑A 0 0
⊢ ↑A 0 0 < 0

case neg.refine_2
m : ℤ
hm : m ≠ 0
A : FixedDetMatrix (Fin 2) ℤ m
h : ↑A 1 0 = 0
hd : ↑A 1 1 ≠ 0
h1 : ¬0 < ↑A 0 0
⊢ |-(-↑A 0 1 / ↑A 1 1 * ↑A 1 1) + -↑A 0 1| < |↑A 1 1|

Proof state:
case pos
m : ℤ
hm : m ≠ 0
A : FixedDetMatrix (Fin 2) ℤ m
h : ↑A 1 0 = 0
hd : ↑A 1 1 ≠ 0
h1 : 0 < ↑A 0 0
n : ℤ := ↑A 0 1 / ↑A 1 1
h2 : ↑A 0 1 % ↑A 1 1 = ↑A 0 1 - ↑A 1 1 * n
h4 : n * ↑A 1 1 ≤ ↑A 0 1
h3 : |↑A 0 1 % ↑A 1 1| < |↑A 1 1|
⊢ T ^ (-n) • A ∈ reps m

Tactic:
simp only [smul_def, Fin.isValue, coe_T_zpow]

Result:
case pos
m : ℤ
hm : m ≠ 0
A : FixedDetMatrix (Fin 2) ℤ m
h : ↑A 1 0 = 0
hd : ↑A 1 1 ≠ 0
h1 : 0 < ↑A 0 0
n : ℤ := ↑A 0 1 / ↑A 1 1
h2 : ↑A 0 1 % ↑A 1 1 = ↑A 0 1 - ↑A 1 1 * n
h4 : n * ↑A 1 1 ≤ ↑A 0 1
h3 : |↑A 0 1 % ↑A 1 1| < |↑A 1 1|
⊢ ⟨!![1, -n; 0, 1] * ↑A, ⋯⟩ ∈ reps m

Proof state:
case pos
m : ℤ
hm : m ≠ 0
A : FixedDetMatrix (Fin 2) ℤ m
h : ↑A 1 0 = 0
hd : ↑A 1 1 ≠ 0
h1 : 0 < ↑A 0 0
n : ℤ := ↑A 0 1 / ↑A 1 1
h2 : ↑A 0 1 % ↑A 1 1 = ↑A 0 1 - ↑A 1 1 * n
h4 : n * ↑A 1 1 ≤ ↑A 0 1
⊢ T ^ (-n) • A ∈ reps m

Tactic:
have h3 := Int.emod_lt (A.1 0 1) hd

Result:
case pos
m : ℤ
hm : m ≠ 0
A : FixedDetMatrix (Fin 2) ℤ m
h : ↑A 1 0 = 0
hd : ↑A 1 1 ≠ 0
h1 : 0 < ↑A 0 0
n : ℤ := ↑A 0 1 / ↑A 1 1
h2 : ↑A 0 1 % ↑A 1 1 = ↑A 0 1 - ↑A 1 1 * n
h4 : n * ↑A 1 1 ≤ ↑A 0 1
h3 : ↑A 0 1 % ↑A 1 1 < |↑A 1 1|
⊢ T ^ (-n) • A ∈ reps m

Proof state:
case pos
m : ℤ
hm : m ≠ 0
A : FixedDetMatrix (Fin 2) ℤ m
h : ↑A 1 0 = 0
hd : ↑A 1 1 ≠ 0
h1 : 0 < ↑A 0 0
n : ℤ := ↑A 0 1 / ↑A 1 1
h2 : ↑A 0 1 % ↑A 1 1 = ↑A 0 1 - ↑A 1 1 * n
h4 : n * ↑A 1 1 ≤ ↑A 0 1
h3 : ↑A 0 1 % ↑A 1 1 < |↑A 1 1|
⊢ T ^ (-n) • A ∈ reps m

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

Result:
case pos
m : ℤ
hm : m ≠ 0
A : FixedDetMatrix (Fin 2) ℤ m
h : ↑A 1 0 = 0
hd : ↑A 1 1 ≠ 0
h1 : 0 < ↑A 0 0
n : ℤ := ↑A 0 1 / ↑A 1 1
h2 : ↑A 0 1 % ↑A 1 1 = ↑A 0 1 - ↑A 1 1 * n
h4 : n * ↑A 1 1 ≤ ↑A 0 1
h3 : |↑A 0 1 % ↑A 1 1| < |↑A 1 1|
⊢ T ^ (-n) • A ∈ reps m

Proof state:
case neg.refine_1
m : ℤ
hm : m ≠ 0
A : FixedDetMatrix (Fin 2) ℤ m
h : ↑A 1 0 = 0
hd : ↑A 1 1 ≠ 0
h1 : ¬0 < ↑A 0 0
⊢ ↑A 0 0 ≤ 0 ∧ ↑A 0 0 ≠ 0

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

Result:
no goals

Proof state:
case neg
m : ℤ
hm : m ≠ 0
A : FixedDetMatrix (Fin 2) ℤ m
h : ↑A 1 0 = 0
hd : ↑A 1 1 ≠ 0
h1 : ¬0 < ↑A 0 0
⊢ 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_empty, 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]

Result:
case neg
m : ℤ
hm : m ≠ 0
A : FixedDetMatrix (Fin 2) ℤ m
h : ↑A 1 0 = 0
hd : ↑A 1 1 ≠ 0
h1 : ¬0 < ↑A 0 0
⊢ ↑A 0 0 < 0 ∧ -↑A 0 1 / ↑A 1 1 * ↑A 1 1 ≤ -↑A 0 1 ∧ |-(-↑A 0 1 / ↑A 1 1 * ↑A 1 1) + -↑A 0 1| < |↑A 1 1|

Proof state:
case step
m : ℤ
hm : m ≠ 0
A : FixedDetMatrix (Fin 2) ℤ m
h1 : ↑A 1 0 ≠ 0
h2 : reduce (reduceStep A) ∈ reps m
⊢ reduce A ∈ reps m

Tactic:
simpa only [reduce_reduceStep h1] using h2

Result:
no goals

Proof state:
case pos
m : ℤ
hm : m ≠ 0
A : FixedDetMatrix (Fin 2) ℤ m
h : ↑A 1 0 = 0
hd : ↑A 1 1 ≠ 0
h1 : 0 < ↑A 0 0
h2 : ↑A 0 1 % ↑A 1 1 = ↑A 0 1 - ↑A 1 1 * (↑A 0 1 / ↑A 1 1)
⊢ T ^ (-(↑A 0 1 / ↑A 1 1)) • A ∈ reps m

Tactic:
have h4 := Int.ediv_mul_le (A.1 0 1) hd

Result:
case pos
m : ℤ
hm : m ≠ 0
A : FixedDetMatrix (Fin 2) ℤ m
h : ↑A 1 0 = 0
hd : ↑A 1 1 ≠ 0
h1 : 0 < ↑A 0 0
h2 : ↑A 0 1 % ↑A 1 1 = ↑A 0 1 - ↑A 1 1 * (↑A 0 1 / ↑A 1 1)
h4 : ↑A 0 1 / ↑A 1 1 * ↑A 1 1 ≤ ↑A 0 1
⊢ T ^ (-(↑A 0 1 / ↑A 1 1)) • A ∈ reps m

Proof state:
case neg.refine_2
m : ℤ
hm : m ≠ 0
A : FixedDetMatrix (Fin 2) ℤ m
h : ↑A 1 0 = 0
hd : ↑A 1 1 ≠ 0
h1 : ¬0 < ↑A 0 0
⊢ |-(-↑A 0 1 / ↑A 1 1 * ↑A 1 1) + -↑A 0 1| < |↑A 1 1|

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

Result:
case neg.refine_2
m : ℤ
hm : m ≠ 0
A : FixedDetMatrix (Fin 2) ℤ m
h : ↑A 1 0 = 0
hd : ↑A 1 1 ≠ 0
h1 : ¬0 < ↑A 0 0
⊢ -↑A 0 1 % ↑A 1 1 < |↑A 1 1|

Proof state:
case neg.refine_2
m : ℤ
hm : m ≠ 0
A : FixedDetMatrix (Fin 2) ℤ m
h : ↑A 1 0 = 0
hd : ↑A 1 1 ≠ 0
h1 : ¬0 < ↑A 0 0
⊢ -↑A 0 1 % ↑A 1 1 < |↑A 1 1|

Tactic:
exact Int.emod_lt _ hd

Result:
no goals

Proof state:
case pos
m : ℤ
hm : m ≠ 0
A : FixedDetMatrix (Fin 2) ℤ m
h : ↑A 1 0 = 0
hd : ↑A 1 1 ≠ 0
h1 : 0 < ↑A 0 0
h2 : ↑A 0 1 % ↑A 1 1 = ↑A 0 1 - ↑A 1 1 * (↑A 0 1 / ↑A 1 1)
h4 : ↑A 0 1 / ↑A 1 1 * ↑A 1 1 ≤ ↑A 0 1
⊢ T ^ (-(↑A 0 1 / ↑A 1 1)) • A ∈ reps m

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

Result:
case pos
m : ℤ
hm : m ≠ 0
A : FixedDetMatrix (Fin 2) ℤ m
h : ↑A 1 0 = 0
hd : ↑A 1 1 ≠ 0
h1 : 0 < ↑A 0 0
n : ℤ := ↑A 0 1 / ↑A 1 1
h2 : ↑A 0 1 % ↑A 1 1 = ↑A 0 1 - ↑A 1 1 * n
h4 : n * ↑A 1 1 ≤ ↑A 0 1
⊢ T ^ (-n) • A ∈ reps m

Proof state:
case pos
m : ℤ
hm : m ≠ 0
A : FixedDetMatrix (Fin 2) ℤ m
h : ↑A 1 0 = 0
hd : ↑A 1 1 ≠ 0
h1 : 0 < ↑A 0 0
n : ℤ := ↑A 0 1 / ↑A 1 1
h2 : ↑A 0 1 % ↑A 1 1 = ↑A 0 1 - ↑A 1 1 * n
h4 : n * ↑A 1 1 ≤ ↑A 0 1
h3 : |↑A 0 1 % ↑A 1 1| < |↑A 1 1|
⊢ ⟨!![1, -n; 0, 1] * ↑A, ⋯⟩ ∈ 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_empty, 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]

Result:
case pos
m : ℤ
hm : m ≠ 0
A : FixedDetMatrix (Fin 2) ℤ m
h : ↑A 1 0 = 0
hd : ↑A 1 1 ≠ 0
h1 : 0 < ↑A 0 0
n : ℤ := ↑A 0 1 / ↑A 1 1
h2 : ↑A 0 1 % ↑A 1 1 = ↑A 0 1 - ↑A 1 1 * n
h4 : n * ↑A 1 1 ≤ ↑A 0 1
h3 : |↑A 0 1 % ↑A 1 1| < |↑A 1 1|
⊢ ↑A 1 0 = 0 ∧ n * ↑A 1 0 < ↑A 0 0 ∧ n * ↑A 1 1 ≤ ↑A 0 1 ∧ |↑A 0 1 + -(n * ↑A 1 1)| < |↑A 1 1|