awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
Goal:
m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
h : (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 ≠ 0
this :
  (↑(reduceStep A) : Matrix (Fin 2) (Fin 2) ℤ) 1 0 =
    (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0 % (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0
⊢ (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0 % (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 < |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0|

Tactic:
Int.emod_lt_abs (A.1 0 0) h

Premises used: Int.emod_lt_abs, OfNat.ofNat, Subtype.val
-- Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
Goal:
m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
h : (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 ≠ 0
this :
  (↑(reduceStep A) : Matrix (Fin 2) (Fin 2) ℤ) 1 0 =
    (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0 % (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0
⊢ (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0 % (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 < |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0|

Tactic:
exact Int.emod_lt_abs (A.1 0 0) h

Premises used: Int.emod_lt_abs, OfNat.ofNat, Subtype.val
-- Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
Goal:
m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
h : (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 ≠ 0
suffices :
  (↑(reduceStep A) : Matrix (Fin 2) (Fin 2) ℤ) 1 0 =
    (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0 % (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0
⊢ |(↑(reduceStep A) : Matrix (Fin 2) (Fin 2) ℤ) 1 0| < |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0|

Tactic:
suffices ((reduceStep A).1 1 0) = A.1 0 0 % A.1 1 0 by
    rw [this, abs_eq_self.mpr (Int.emod_nonneg (A.1 0 0) h)]
    exact Int.emod_lt_abs (A.1 0 0) h
-- Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
Goal:
m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
h : (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 ≠ 0
simp_rw :
  HMul.hMul (α := Matrix (Fin 2) (Fin 2) ℤ) (!![0, -1; 1, 0] : Matrix (Fin 2) (Fin 2) ℤ)
      (HMul.hMul (α := Matrix (Fin 2) (Fin 2) ℤ)
        (!![1, -((↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0 / (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0); 0, 1] :
          Matrix (Fin 2) (Fin 2) ℤ)
        (↑A : Matrix (Fin 2) (Fin 2) ℤ))
      1 0 =
    (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0 +
      -((↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 *
          ((↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0 / (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0))
⊢ (↑(reduceStep A) : Matrix (Fin 2) (Fin 2) ℤ) 1 0 =
    (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0 % (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0

Tactic:
simp_rw [Int.emod_def, sub_eq_add_neg, reduceStep, smul_coe, coe_T_zpow, S]

Premises used: sub_eq_add_neg, ModularGroup.S, FixedDetMatrices.reduceStep, FixedDetMatrices.smul_coe, ModularGroup.coe_T_zpow, Int.emod_def
-- Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
Goal:
m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
h : (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 ≠ 0
⊢ HMul.hMul (α := Matrix (Fin 2) (Fin 2) ℤ) (!![0, -1; 1, 0] : Matrix (Fin 2) (Fin 2) ℤ)
      (HMul.hMul (α := Matrix (Fin 2) (Fin 2) ℤ)
        (!![1, -((↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0 / (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0); 0, 1] :
          Matrix (Fin 2) (Fin 2) ℤ)
        (↑A : Matrix (Fin 2) (Fin 2) ℤ))
      1 0 =
    (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0 +
      -((↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 *
          ((↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0 / (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0))

Tactic:
norm_num [vecMul, vecHead, vecTail, mul_comm]

Premises used: Matrix.vecMul, Matrix.vecHead, mul_comm, Matrix.vecTail
-- 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 : ℤ
C : FixedDetMatrix (Fin 2) ℤ m → Sort u_3
base : (A : FixedDetMatrix (Fin 2) ℤ m) → (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0 → C A
step : (A : FixedDetMatrix (Fin 2) ℤ m) → (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 ≠ 0 → C (reduceStep A) → C A
A : FixedDetMatrix (Fin 2) ℤ m
pos : (h : (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0) → C A
neg : (h : ¬(↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0) → C A
⊢ C A

Tactic:
by_cases h : (A.1 1 0) = 0

Premises used: OfNat.ofNat, Subtype.val
-- 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 : ℤ
C : FixedDetMatrix (Fin 2) ℤ m → Sort u_3
base : (A : FixedDetMatrix (Fin 2) ℤ m) → (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0 → C A
step : (A : FixedDetMatrix (Fin 2) ℤ m) → (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 ≠ 0 → C (reduceStep A) → C A
A : FixedDetMatrix (Fin 2) ℤ m
h : (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
⊢ C A

Tactic:
exact base _ h
-- 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 : ℤ
C : FixedDetMatrix (Fin 2) ℤ m → Sort u_3
base : (A : FixedDetMatrix (Fin 2) ℤ m) → (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0 → C A
step : (A : FixedDetMatrix (Fin 2) ℤ m) → (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 ≠ 0 → C (reduceStep A) → C A
A : FixedDetMatrix (Fin 2) ℤ m
h : ¬(↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
⊢ C A

Tactic:
exact step A h (reduce_rec base step (reduceStep A))

Premises used: FixedDetMatrices.reduceStep
-- Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
Goal:
m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
h : ¬(↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
zify : |(↑(reduceStep A) : Matrix (Fin 2) (Fin 2) ℤ) 1 0| < |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0|
⊢ ((↑(reduceStep A) : Matrix (Fin 2) (Fin 2) ℤ) 1 0).natAbs < ((↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0).natAbs

Tactic:
zify
-- Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
Goal:
m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
h : ¬(↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
⊢ |(↑(reduceStep A) : Matrix (Fin 2) (Fin 2) ℤ) 1 0| < |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0|

Tactic:
reduce_aux h

Premises used: _private.0.FixedDetMatrices.reduce_aux
-- Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
Goal:
m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
h : ¬(↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
⊢ |(↑(reduceStep A) : Matrix (Fin 2) (Fin 2) ℤ) 1 0| < |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0|

Tactic:
exact reduce_aux h

Premises used: _private.0.FixedDetMatrices.reduce_aux
-- Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
Goal:
m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
h : ¬(↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
exact : |(↑(reduceStep A) : Matrix (Fin 2) (Fin 2) ℤ) 1 0| < |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0|
⊢ ((↑(reduceStep A) : Matrix (Fin 2) (Fin 2) ℤ) 1 0).natAbs < ((↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0).natAbs

Tactic:
decreasing_by
    zify
    exact reduce_aux h

Premises used: _private.0.FixedDetMatrices.reduce_aux
-- Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
Goal:
m : ℤ
a : FixedDetMatrix (Fin 2) ℤ m
h : ¬(↑a : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
zify : |(↑(reduceStep a) : Matrix (Fin 2) (Fin 2) ℤ) 1 0| < |(↑a : Matrix (Fin 2) (Fin 2) ℤ) 1 0|
⊢ ((↑(reduceStep a) : Matrix (Fin 2) (Fin 2) ℤ) 1 0).natAbs < ((↑a : Matrix (Fin 2) (Fin 2) ℤ) 1 0).natAbs

Tactic:
zify
-- Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
Goal:
m : ℤ
a : FixedDetMatrix (Fin 2) ℤ m
h : ¬(↑a : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
⊢ |(↑(reduceStep a) : Matrix (Fin 2) (Fin 2) ℤ) 1 0| < |(↑a : Matrix (Fin 2) (Fin 2) ℤ) 1 0|

Tactic:
reduce_aux h

Premises used: _private.0.FixedDetMatrices.reduce_aux
-- Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
Goal:
m : ℤ
a : FixedDetMatrix (Fin 2) ℤ m
h : ¬(↑a : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
⊢ |(↑(reduceStep a) : Matrix (Fin 2) (Fin 2) ℤ) 1 0| < |(↑a : Matrix (Fin 2) (Fin 2) ℤ) 1 0|

Tactic:
exact reduce_aux h

Premises used: _private.0.FixedDetMatrices.reduce_aux
-- Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
Goal:
m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
hc : (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
ha : 0 < (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0
rw :
  (if (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0 then
      if 0 < (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0 then
        T ^ (-((↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 / (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1)) • A
      else T ^ (-(-(↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 / -(↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1)) • S • S • A
    else reduce (reduceStep A)) =
    T ^ (-((↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 / (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1)) • A
⊢ reduce A = T ^ (-((↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 / (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1)) • A

Tactic:
rw [reduce]

Premises used: FixedDetMatrices.reduce
-- Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
Goal:
m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
hc : (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
ha : 0 < (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0
simp :
  (if (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0 then
      if 0 < (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0 then
        (T ^ ((↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 / (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1))⁻¹ • A
      else T ^ (-(↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 / (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1) • S • S • A
    else reduce (reduceStep A)) =
    (T ^ ((↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 / (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1))⁻¹ • A
⊢ (if (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0 then
      if 0 < (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0 then
        T ^ (-((↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 / (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1)) • A
      else T ^ (-(-(↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 / -(↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1)) • S • S • A
    else reduce (reduceStep A)) =
    T ^ (-((↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 / (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1)) • A

Tactic:
simp only [zpow_neg, Int.ediv_neg, neg_neg] at *

Premises used: Int.ediv_neg, neg_neg, zpow_neg
-- Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
Goal:
m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
hc : (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
ha : 0 < (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0
simp_rw :
  (if 0 < (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0 then
      (T ^ ((↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 / (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1))⁻¹ • A
    else T ^ (-(↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 / (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1) • S • S • A) =
    (T ^ ((↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 / (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1))⁻¹ • A
⊢ (if (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0 then
      if 0 < (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0 then
        (T ^ ((↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 / (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1))⁻¹ • A
      else T ^ (-(↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 / (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1) • S • S • A
    else reduce (reduceStep A)) =
    (T ^ ((↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 / (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1))⁻¹ • A

Tactic:
simp_rw [if_pos hc, if_pos ha]

Premises used: if_pos
-- Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
Goal:
m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
hc : (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
ha : ¬0 < (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0
rw :
  (if (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0 then
      if 0 < (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0 then
        T ^ (-((↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 / (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1)) • A
      else T ^ (-(-(↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 / -(↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1)) • S • S • A
    else reduce (reduceStep A)) =
    T ^ (-(-(↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 / -(↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1)) • S • S • A
⊢ reduce A = T ^ (-(-(↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 / -(↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1)) • S • S • A

Tactic:
rw [reduce]

Premises used: FixedDetMatrices.reduce
-- Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
Goal:
m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
hc : (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
ha : ¬0 < (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0
simp :
  (if (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0 then
      if 0 < (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0 then
        (T ^ ((↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 / (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1))⁻¹ • A
      else T ^ (-(↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 / (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1) • S • S • A
    else reduce (reduceStep A)) =
    T ^ (-(↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 / (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1) • S • S • A
⊢ (if (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0 then
      if 0 < (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0 then
        T ^ (-((↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 / (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1)) • A
      else T ^ (-(-(↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 / -(↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1)) • S • S • A
    else reduce (reduceStep A)) =
    T ^ (-(-(↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 / -(↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1)) • S • S • A

Tactic:
simp only [zpow_neg, Int.ediv_neg, neg_neg] at *

Premises used: Int.ediv_neg, neg_neg, zpow_neg
-- Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
Goal:
m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
hc : (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
ha : ¬0 < (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0
simp_rw :
  (if 0 < (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0 then
      (T ^ ((↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 / (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1))⁻¹ • A
    else T ^ (-(↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 / (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1) • S • S • A) =
    T ^ (-(↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 / (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1) • S • S • A
⊢ (if (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0 then
      if 0 < (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0 then
        (T ^ ((↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 / (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1))⁻¹ • A
      else T ^ (-(↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 / (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1) • S • S • A
    else reduce (reduceStep A)) =
    T ^ (-(↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 / (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1) • S • S • A

Tactic:
simp_rw [if_pos hc, if_neg ha]

Premises used: if_pos, if_neg
-- Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
Goal:
m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
hc : (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 ≠ 0
symm : reduce A = reduce (reduceStep A)
⊢ reduce (reduceStep A) = reduce A

Tactic:
symm
-- Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
Goal:
m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
hc : (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 ≠ 0
rw :
  (if (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0 then
      if 0 < (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0 then
        T ^ (-((↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 / (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1)) • A
      else T ^ (-(-(↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 / -(↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1)) • S • S • A
    else reduce (reduceStep A)) =
    reduce (reduceStep A)
rw₁ rw₂ : reduce (reduceStep A) = reduce (reduceStep A)
⊢ reduce A = reduce (reduceStep A)

Tactic:
rw [reduce, if_neg hc]

Premises used: FixedDetMatrices.reduce, if_neg
-- Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
Goal:
m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
ha : (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
⊢ (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = m

Tactic:
simpa only [det_fin_two, ha, mul_zero, sub_zero] using A.2

Premises used: sub_zero, MulZeroClass.mul_zero, Matrix.det_fin_two, Subtype.property
-- Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
Goal:
m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
ha : (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
hm : m ≠ 0
⊢ (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1 ≠ 0

Tactic:
right_ne_zero_of_mul (A_c_eq_zero (ha) ▸ hm)

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

Tactic:
left_ne_zero_of_mul (A_c_eq_zero ha ▸ hm)

Premises used: left_ne_zero_of_mul
-- Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
Goal:
m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
h : A ∈ reps m
i j : Fin 2
suffices : |(↑A : Matrix (Fin 2) (Fin 2) ℤ) i j| ≤ |m|
⊢ (↑A : Matrix (Fin 2) (Fin 2) ℤ) i j ∈ Finset.Icc (-|m|) |m|

Tactic:
suffices |A.1 i j| ≤ |m| from Finset.mem_Icc.mpr <| abs_le.mp this
-- Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
Goal:
m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
h : A ∈ reps m
i j : Fin 2
⊢ (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0

Tactic:
obtain ⟨h10, h00, h01, h11⟩ := h
-- Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
Goal:
m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
h : A ∈ reps m
i j : Fin 2
h10 : (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
⊢ 0 < (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0

Tactic:
obtain ⟨h10, h00, h01, h11⟩ := h
-- Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
Goal:
m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
h : A ∈ reps m
i j : Fin 2
h10 : (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
h00 : 0 < (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0
⊢ 0 ≤ (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1

Tactic:
obtain ⟨h10, h00, h01, h11⟩ := h
-- Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
Goal:
m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
h : A ∈ reps m
i j : Fin 2
h10 : (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
h00 : 0 < (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0
h01 : 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|

Tactic:
obtain ⟨h10, h00, h01, h11⟩ := h
-- Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
Goal:
m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
i j : Fin 2
h10 : (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
h00 : 0 < (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0
h01 : 0 ≤ (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1
h11 : |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1| < |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1|
⊢ 0 < |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1|

Tactic:
have h1 : 0 < |A.1 1 1| := (abs_nonneg _).trans_lt h11
-- Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
Goal:
m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
i j : Fin 2
h10 : (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
h00 : 0 < (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0
h01 : 0 ≤ (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1
h11 : |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1| < |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1|
h1 : 0 < |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1|
⊢ 0 < |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0|

Tactic:
have h2 : 0 < |A.1 0 0| := abs_pos.mpr h00.ne'
-- Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
Goal:
m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
i j : Fin 2
h10 : (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
h00 : 0 < (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0
h01 : 0 ≤ (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1
h11 : |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1| < |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1|
h1 : 0 < |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1|
h2 : 0 < |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0|
0 : |(↑A : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) j| ≤ |m|
1 : |(↑A : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) j| ≤ |m|
⊢ |(↑A : Matrix (Fin 2) (Fin 2) ℤ) i j| ≤ |m|

Tactic:
fin_cases i
-- Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
Goal:
m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
j : Fin 2
h10 : (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
h00 : 0 < (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0
h01 : 0 ≤ (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1
h11 : |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1| < |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1|
h1 : 0 < |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1|
h2 : 0 < |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0|
0 :
  |(↑A : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2))| ≤
    |m|
h :
  |(↑A : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2))| ≤
    |m|
⊢ |(↑A : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) j| ≤ |m|

Tactic:
fin_cases j
-- Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
Goal:
m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
j : Fin 2
h10 : (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
h00 : 0 < (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0
h01 : 0 ≤ (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1
h11 : |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1| < |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1|
h1 : 0 < |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1|
h2 : 0 < |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0|
1 :
  |(↑A : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2))| ≤
    |m|
h :
  |(↑A : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2))| ≤
    |m|
⊢ |(↑A : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) j| ≤ |m|

Tactic:
fin_cases j
-- Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
Goal:
m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
h10 : (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
h00 : 0 < (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0
h01 : 0 ≤ (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1
h11 : |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1| < |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1|
h1 : 0 < |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1|
h2 : 0 < |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0|
⊢ |(↑A : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2))| ≤
    |m|

Tactic:
simpa only [← abs_mul, A_c_eq_zero h10] using (le_mul_iff_one_le_right h2).mpr h1

Premises used: Iff.mpr, le_mul_iff_one_le_right, abs_mul, _private.0.FixedDetMatrices.A_c_eq_zero
-- Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
Goal:
m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
h10 : (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
h00 : 0 < (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0
h01 : 0 ≤ (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1
h11 : |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1| < |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1|
h1 : 0 < |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1|
h2 : 0 < |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0|
⊢ |(↑A : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2))| ≤
    |m|

Tactic:
simpa only [← abs_mul, A_c_eq_zero h10] using h11.le.trans (le_mul_of_one_le_left h1.le h2)

Premises used: le_mul_of_one_le_left, abs_mul, LT.lt.le, _private.0.FixedDetMatrices.A_c_eq_zero, LE.le.trans
-- Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
Goal:
m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
h10 : (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
h00 : 0 < (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0
h01 : 0 ≤ (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1
h11 : |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1| < |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1|
h1 : 0 < |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1|
h2 : 0 < |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0|
⊢ |(↑A : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2))| ≤
    |m|

Tactic:
simp_all
-- Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
Goal:
m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
h10 : (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
h00 : 0 < (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0
h01 : 0 ≤ (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1
h11 : |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1| < |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1|
h1 : 0 < |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1|
h2 : 0 < |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0|
⊢ |(↑A : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2))| ≤
    |m|

Tactic:
simpa only [← abs_mul, A_c_eq_zero h10] using (le_mul_iff_one_le_left h1).mpr h2

Premises used: Iff.mpr, abs_mul, le_mul_iff_one_le_left, _private.0.FixedDetMatrices.A_c_eq_zero
-- Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
Goal:
rw :
  ∀ (x : FixedDetMatrix (Fin 2) ℤ 0),
    x ∉
      {A : FixedDetMatrix (Fin 2) ℤ 0 |
        (↑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|}
⊢ Eq (α := Set (FixedDetMatrix (Fin 2) ℤ 0)) (reps 0) ∅

Tactic:
rw [reps, Set.eq_empty_iff_forall_notMem]

Premises used: FixedDetMatrices.reps, Set.eq_empty_iff_forall_notMem
-- 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 1| < 0
linarith : -1 + (|(↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1| + 1 - 0) + (0 - |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1|) = 0
⊢ False

Tactic:
linarith [abs_nonneg (A.1 0 1)]

Premises used: OfNat.ofNat, Subtype.val, abs_nonneg
-- 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|
suffices : |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1| < 0
⊢ False

Tactic:
suffices |A.1 0 1| < 0 by linarith [abs_nonneg (A.1 0 1)]