awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.FixedDetMatrices (hypothesis)
Goal:
m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
h : A ∈ reps m
i j : Fin 2
⊢ |(↑A : Matrix (Fin 2) (Fin 2) ℤ) i j| ≤ |m|
have h10 : (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
Tactic: obtain ⟨h10, h00, h01, h11⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.FixedDetMatrices (hypothesis)
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
⊢ |(↑A : Matrix (Fin 2) (Fin 2) ℤ) i j| ≤ |m|
have h00 : 0 < (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0
Tactic: obtain ⟨h10, h00, h01, h11⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.FixedDetMatrices (hypothesis)
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
⊢ |(↑A : Matrix (Fin 2) (Fin 2) ℤ) i j| ≤ |m|
have h01 : 0 ≤ (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1
Tactic: obtain ⟨h10, h00, h01, h11⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.FixedDetMatrices (hypothesis)
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) ℤ) i j| ≤ |m|
have h11 : |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1| < |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1|
Tactic: obtain ⟨h10, h00, h01, h11⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.FixedDetMatrices (hypothesis)
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|
⊢ |(↑A : Matrix (Fin 2) (Fin 2) ℤ) i j| ≤ |m|
have h1 : 0 < |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1|
Tactic: have h1 : 0 < |A.1 1 1| := (abs_nonneg _).trans_lt h11
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.FixedDetMatrices (hypothesis)
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|
⊢ |(↑A : Matrix (Fin 2) (Fin 2) ℤ) i j| ≤ |m|
have h2 : 0 < |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0|
Tactic: have h2 : 0 < |A.1 0 0| := abs_pos.mpr h00.ne'
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.FixedDetMatrices (goal)
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|
⊢ |(↑A : Matrix (Fin 2) (Fin 2) ℤ) i j| ≤ |m|
have 0 : |(↑A : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2)) j| ≤ |m|
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.FixedDetMatrices (goal)
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|
⊢ |(↑A : Matrix (Fin 2) (Fin 2) ℤ) i j| ≤ |m|
have 1 : |(↑A : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2)) j| ≤ |m|
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.FixedDetMatrices (goal)
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|
⊢ |(↑A : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) j| ≤ |m|
have 0 : |(↑A : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2))| ≤
  |m|
Tactic: fin_cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.FixedDetMatrices (goal)
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|
⊢ |(↑A : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) j| ≤ |m|
have 0₁ : |(↑A : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2))| ≤
  |m|
Tactic: fin_cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.FixedDetMatrices (goal)
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|
⊢ |(↑A : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) j| ≤ |m|
have 1 : |(↑A : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2))| ≤
  |m|
Tactic: fin_cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.FixedDetMatrices (goal)
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|
⊢ |(↑A : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) j| ≤ |m|
have 1₁ : |(↑A : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2))| ≤
  |m|
Tactic: fin_cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.FixedDetMatrices (goal)
Goal:
⊢ Eq (α := Set (FixedDetMatrix (Fin 2) ℤ 0)) (reps 0) ∅
have 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|}
Tactic: rw [reps, Set.eq_empty_iff_forall_notMem]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.FixedDetMatrices (goal)
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
⊢ False
have linarith : -1 + (|(↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1| + 1 - 0) + (0 - |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1|) = 0
Tactic: linarith [abs_nonneg (A.1 0 1)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.FixedDetMatrices (goal)
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|
⊢ False
have suffices : |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1| < 0
Tactic: suffices |A.1 0 1| < 0 by linarith [abs_nonneg (A.1 0 1)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.FixedDetMatrices (hypothesis)
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 1| < 0
have this : (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0 * (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 0
Tactic: have := A_c_eq_zero h₁
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.FixedDetMatrices (goal)
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
⊢ Fintype (↑(reps k) : Type)
have 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) sorry
Tactic: apply Fintype.ofInjective (β := H4) (f := fun M i j ↦ ⟨M.1.1 i j, reps_entries_le_m' M.2 i j⟩)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.FixedDetMatrices (goal)
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)
⊢ M = N
have 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
Tactic: ext i j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.FixedDetMatrices (goal)
Goal:
m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
⊢ S • S • S • T • S • T • S • A = T⁻¹ • A
have simp_rw : S • S • S • T • S • T • S • A = (S • S • S • T • S • T • S) • A
Tactic: simp_rw [← T_S_rel, ← smul_assoc]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.FixedDetMatrices (hypothesis)
Goal:
m : ℤ
hm : m ≠ 0
A : FixedDetMatrix (Fin 2) ℤ m
h : (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
⊢ reduce A ∈ reps m
have hd : (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1 ≠ 0
Tactic: have hd := A_d_ne_zero h hm
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.FixedDetMatrices (goal)
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
⊢ reduce A ∈ reps m
have pos : ∀ (h1 : 0 < (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0), reduce A ∈ reps m
Tactic: by_cases h1 : 0 < A.1 0 0
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.FixedDetMatrices (goal)
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
⊢ reduce A ∈ reps m
have neg : ∀ (h1 : ¬0 < (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0), reduce A ∈ reps m
Tactic: by_cases h1 : 0 < A.1 0 0
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.FixedDetMatrices (goal)
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
⊢ reduce A ∈ reps m
have pos : T ^ (-((↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 / (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1)) • A ∈ reps m
Tactic: simp only [reduce_of_pos h h1]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.FixedDetMatrices (hypothesis)
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
⊢ T ^ (-((↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 / (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1)) • A ∈ reps m
have 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)
Tactic: have h2 := Int.emod_def (A.1 0 1) (A.1 1 1)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.FixedDetMatrices (hypothesis)
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)
⊢ T ^ (-((↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 / (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1)) • A ∈ reps m
have 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
Tactic: have h4 := Int.ediv_mul_le (A.1 0 1) hd
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.FixedDetMatrices (goal)
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
⊢ T ^ (-((↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 / (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1)) • A ∈ reps m
have 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
Tactic: set n : ℤ := A.1 0 1 / A.1 1 1
Cleared hypotheses: h2, h4
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.FixedDetMatrices (hypothesis)
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
⊢ T ^ (-n) • A ∈ reps m
have 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|
Tactic: have h3 := Int.emod_lt_abs (A.1 0 1) hd
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.FixedDetMatrices (hypothesis)
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|
⊢ T ^ (-n) • A ∈ reps m
have 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|
Tactic: rw [← abs_eq_self.mpr <| Int.emod_nonneg _ hd] at h3
Cleared hypotheses: h3
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.FixedDetMatrices (goal)
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|
⊢ T ^ (-n) • A ∈ reps m
have 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) ℤ))
    sorry ∈
  reps m
Tactic: simp only [smul_def, coe_T_zpow]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.FixedDetMatrices (goal)
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|
⊢ 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
have 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|
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.FixedDetMatrices (goal)
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
⊢ reduce A ∈ reps m
have 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|
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.FixedDetMatrices (goal)
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|
have neg : (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0 < 0
Tactic: refine ⟨?_, Int.ediv_mul_le _ hd, ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.FixedDetMatrices (goal)
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 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|
have 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|
Tactic: refine ⟨?_, Int.ediv_mul_le _ hd, ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.FixedDetMatrices (goal)
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
have neg : (↑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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.FixedDetMatrices (goal)
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) +
        -(↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1| <
    |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1|
have 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|
Tactic: rw [mul_comm, add_comm, ← Int.sub_eq_add_neg, ← Int.emod_def,
         abs_eq_self.mpr <| Int.emod_nonneg _ hd]