-- Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
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
base : ∀ (A : FixedDetMatrix (Fin 2) ℤ m) (h : (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0), reduce 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

Premises used: neg_add_rev, Iff.mpr, lt_neg, abs_neg, Matrix.neg_cons, Nat.succ_eq_add_one, and_true, Equiv.symm_apply_apply, MulZeroClass.zero_mul, Matrix.cons_val_one, mul_assoc, Matrix.vecMul, Matrix.neg_of, sub_eq_add_neg, Matrix.cons_val_zero, Int.ediv_neg, le_neg, Matrix.cons_dotProduct, Matrix.empty_val', neg_neg, Nat.reduceAdd, Matrix.cons_val_fin_one, Int.sub_eq_add_neg, Set.mem_setOf_eq, Matrix.dotProduct_of_isEmpty, le_add_neg_iff_add_le, Fin.succ_zero_eq_one, Matrix.of_apply, Int.lt_iff_le_and_ne, Matrix.cons_mul, zero_add, FixedDetMatrices.reps, add_comm, MulZeroClass.mul_zero, Fin.isValue, Matrix.vecHead, mul_comm, Matrix.empty_mul, FixedDetMatrices.smul_def, Function.comp_apply, neg_mul, add_zero, ModularGroup.coe_T_zpow, OfNat.ofNat, Matrix.neg_empty, neg_zero, Subtype.val, Int.emod_def, Matrix.vecTail, abs_eq_self, Pi.neg_apply, ModularGroup.S_mul_S_eq, one_mul, true_and, mul_neg, Matrix.cons_val'