-- Mathlib/LinearAlgebra/Matrix/FixedDetMatrices.lean
/-- An auxiliary result bounding the size of the entries of the representatives in `reps` -/
lemma reps_entries_le_m' {A : Δ m} (h : A ∈ reps m) (i j : Fin 2) :
    A.1 i j ∈ Finset.Icc (-|m|) |m|

Proof state:
case intro.intro.intro
m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
i j : Fin 2
h10 : ↑A 1 0 = 0
h00 : 0 < ↑A 0 0
h01 : 0 ≤ ↑A 0 1
h11 : |↑A 0 1| < |↑A 1 1|
⊢ |↑A i j| ≤ |m|

Tactic:
have h1 : 0 < |A.1 1 1| := (abs_nonneg _).trans_lt h11

Result:
case intro.intro.intro
m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
i j : Fin 2
h10 : ↑A 1 0 = 0
h00 : 0 < ↑A 0 0
h01 : 0 ≤ ↑A 0 1
h11 : |↑A 0 1| < |↑A 1 1|
h1 : 0 < |↑A 1 1|
⊢ |↑A i j| ≤ |m|

Proof state:
m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
h : A ∈ reps m
i j : Fin 2
⊢ |↑A i j| ≤ |m|

Tactic:
obtain ⟨h10, h00, h01, h11⟩ := h

Result:
case intro.intro.intro
m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
i j : Fin 2
h10 : ↑A 1 0 = 0
h00 : 0 < ↑A 0 0
h01 : 0 ≤ ↑A 0 1
h11 : |↑A 0 1| < |↑A 1 1|
⊢ |↑A i j| ≤ |m|

Proof state:
case intro.intro.intro.«0».«0»
m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
h10 : ↑A 1 0 = 0
h00 : 0 < ↑A 0 0
h01 : 0 ≤ ↑A 0 1
h11 : |↑A 0 1| < |↑A 1 1|
h1 : 0 < |↑A 1 1|
h2 : 0 < |↑A 0 0|
⊢ |↑A ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩)| ≤ |m|

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

Result:
no goals

Proof state:
case intro.intro.intro
m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
i j : Fin 2
h10 : ↑A 1 0 = 0
h00 : 0 < ↑A 0 0
h01 : 0 ≤ ↑A 0 1
h11 : |↑A 0 1| < |↑A 1 1|
h1 : 0 < |↑A 1 1|
⊢ |↑A i j| ≤ |m|

Tactic:
have h2 : 0 < |A.1 0 0| := abs_pos.mpr h00.ne'

Result:
case intro.intro.intro
m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
i j : Fin 2
h10 : ↑A 1 0 = 0
h00 : 0 < ↑A 0 0
h01 : 0 ≤ ↑A 0 1
h11 : |↑A 0 1| < |↑A 1 1|
h1 : 0 < |↑A 1 1|
h2 : 0 < |↑A 0 0|
⊢ |↑A i j| ≤ |m|

Proof state:
m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
h : A ∈ reps m
i j : Fin 2
⊢ ↑A i j ∈ Finset.Icc (-|m|) |m|

Tactic:
suffices |A.1 i j| ≤ |m| from Finset.mem_Icc.mpr <| abs_le.mp this

Result:
m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
h : A ∈ reps m
i j : Fin 2
⊢ |↑A i j| ≤ |m|

Proof state:
case intro.intro.intro.«0».«1»
m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
h10 : ↑A 1 0 = 0
h00 : 0 < ↑A 0 0
h01 : 0 ≤ ↑A 0 1
h11 : |↑A 0 1| < |↑A 1 1|
h1 : 0 < |↑A 1 1|
h2 : 0 < |↑A 0 0|
⊢ |↑A ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩)| ≤ |m|

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

Result:
no goals

Proof state:
case intro.intro.intro.«1».«1»
m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
h10 : ↑A 1 0 = 0
h00 : 0 < ↑A 0 0
h01 : 0 ≤ ↑A 0 1
h11 : |↑A 0 1| < |↑A 1 1|
h1 : 0 < |↑A 1 1|
h2 : 0 < |↑A 0 0|
⊢ |↑A ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩)| ≤ |m|

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

Result:
no goals

Proof state:
case intro.intro.intro.«1».«0»
m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
h10 : ↑A 1 0 = 0
h00 : 0 < ↑A 0 0
h01 : 0 ≤ ↑A 0 1
h11 : |↑A 0 1| < |↑A 1 1|
h1 : 0 < |↑A 1 1|
h2 : 0 < |↑A 0 0|
⊢ |↑A ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩)| ≤ |m|

Tactic:
simp_all

Result:
no goals

Proof state:
case intro.intro.intro
m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
i j : Fin 2
h10 : ↑A 1 0 = 0
h00 : 0 < ↑A 0 0
h01 : 0 ≤ ↑A 0 1
h11 : |↑A 0 1| < |↑A 1 1|
h1 : 0 < |↑A 1 1|
h2 : 0 < |↑A 0 0|
⊢ |↑A i j| ≤ |m|

Tactic:
fin_cases i <;> fin_cases j

Result:
case intro.intro.intro.«0».«0»
m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
h10 : ↑A 1 0 = 0
h00 : 0 < ↑A 0 0
h01 : 0 ≤ ↑A 0 1
h11 : |↑A 0 1| < |↑A 1 1|
h1 : 0 < |↑A 1 1|
h2 : 0 < |↑A 0 0|
⊢ |↑A ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩)| ≤ |m|

case intro.intro.intro.«0».«1»
m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
h10 : ↑A 1 0 = 0
h00 : 0 < ↑A 0 0
h01 : 0 ≤ ↑A 0 1
h11 : |↑A 0 1| < |↑A 1 1|
h1 : 0 < |↑A 1 1|
h2 : 0 < |↑A 0 0|
⊢ |↑A ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩)| ≤ |m|

case intro.intro.intro.«1».«0»
m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
h10 : ↑A 1 0 = 0
h00 : 0 < ↑A 0 0
h01 : 0 ≤ ↑A 0 1
h11 : |↑A 0 1| < |↑A 1 1|
h1 : 0 < |↑A 1 1|
h2 : 0 < |↑A 0 0|
⊢ |↑A ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩)| ≤ |m|

case intro.intro.intro.«1».«1»
m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
h10 : ↑A 1 0 = 0
h00 : 0 < ↑A 0 0
h01 : 0 ≤ ↑A 0 1
h11 : |↑A 0 1| < |↑A 1 1|
h1 : 0 < |↑A 1 1|
h2 : 0 < |↑A 0 0|
⊢ |↑A ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩)| ≤ |m|