awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (goal)
Goal:
R : Type v
inst : CommRing R
P : SL(2, R) → Prop
h :
  ∀ (a b c d : R) (hdet : a * d - b * c = 1),
    P (Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) R) ↦ A.det = 1) !![a, b; c, d] ⋯)
m : Matrix (Fin 2) (Fin 2) R
hm : m.det = 1
i j : Fin 2
h₁ :
  (↑(Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) R) ↦ A.det = 1) m hm) : Matrix (Fin 2) (Fin 2) R)
      ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) j =
    (↑(Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) R) ↦ A.det = 1) !![m 0 0, m 0 1; m 1 0, m 1 1] ⋯) :
        Matrix (Fin 2) (Fin 2) R)
      ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) j
⊢ (↑(Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) R) ↦ A.det = 1) m hm) : Matrix (Fin 2) (Fin 2) R) i j =
    (↑(Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) R) ↦ A.det = 1) !![m 0 0, m 0 1; m 1 0, m 1 1] ⋯) :
        Matrix (Fin 2) (Fin 2) R)
      i j
have h₂ : (↑(Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) R) ↦ A.det = 1) m hm) : Matrix (Fin 2) (Fin 2) R)
    ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2)) j =
  (↑(Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) R) ↦ A.det = 1) !![m 0 0, m 0 1; m 1 0, m 1 1] sorry) :
      Matrix (Fin 2) (Fin 2) R)
    ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩) j
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (goal)
Goal:
R : Type v
inst : CommRing R
P : SL(2, R) → Prop
h :
  ∀ (a b c d : R) (hdet : a * d - b * c = 1),
    P (Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) R) ↦ A.det = 1) !![a, b; c, d] ⋯)
m : Matrix (Fin 2) (Fin 2) R
hm : m.det = 1
j : Fin 2
⊢ (↑(Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) R) ↦ A.det = 1) m hm) : Matrix (Fin 2) (Fin 2) R)
      ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) j =
    (↑(Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) R) ↦ A.det = 1) !![m 0 0, m 0 1; m 1 0, m 1 1] ⋯) :
        Matrix (Fin 2) (Fin 2) R)
      ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) j
have h₁ : (↑(Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) R) ↦ A.det = 1) m hm) : Matrix (Fin 2) (Fin 2) R)
    ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2)) =
  (↑(Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) R) ↦ A.det = 1) !![m 0 0, m 0 1; m 1 0, m 1 1] sorry) :
      Matrix (Fin 2) (Fin 2) R)
    ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩) ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩)
Tactic: fin_cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (goal)
Goal:
R : Type v
inst : CommRing R
P : SL(2, R) → Prop
h :
  ∀ (a b c d : R) (hdet : a * d - b * c = 1),
    P (Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) R) ↦ A.det = 1) !![a, b; c, d] ⋯)
m : Matrix (Fin 2) (Fin 2) R
hm : m.det = 1
j : Fin 2
h₁ :
  (↑(Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) R) ↦ A.det = 1) m hm) : Matrix (Fin 2) (Fin 2) R)
      ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) =
    (↑(Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) R) ↦ A.det = 1) !![m 0 0, m 0 1; m 1 0, m 1 1] ⋯) :
        Matrix (Fin 2) (Fin 2) R)
      ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)
⊢ (↑(Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) R) ↦ A.det = 1) m hm) : Matrix (Fin 2) (Fin 2) R)
      ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) j =
    (↑(Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) R) ↦ A.det = 1) !![m 0 0, m 0 1; m 1 0, m 1 1] ⋯) :
        Matrix (Fin 2) (Fin 2) R)
      ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) j
have h₂ : (↑(Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) R) ↦ A.det = 1) m hm) : Matrix (Fin 2) (Fin 2) R)
    ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2)) =
  (↑(Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) R) ↦ A.det = 1) !![m 0 0, m 0 1; m 1 0, m 1 1] sorry) :
      Matrix (Fin 2) (Fin 2) R)
    ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩) ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩)
Tactic: fin_cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (goal)
Goal:
R : Type v
inst : CommRing R
P : SL(2, R) → Prop
h :
  ∀ (a b c d : R) (hdet : a * d - b * c = 1),
    P (Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) R) ↦ A.det = 1) !![a, b; c, d] ⋯)
m : Matrix (Fin 2) (Fin 2) R
hm : m.det = 1
j : Fin 2
⊢ (↑(Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) R) ↦ A.det = 1) m hm) : Matrix (Fin 2) (Fin 2) R)
      ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) j =
    (↑(Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) R) ↦ A.det = 1) !![m 0 0, m 0 1; m 1 0, m 1 1] ⋯) :
        Matrix (Fin 2) (Fin 2) R)
      ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) j
have h₁ : (↑(Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) R) ↦ A.det = 1) m hm) : Matrix (Fin 2) (Fin 2) R)
    ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2)) =
  (↑(Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) R) ↦ A.det = 1) !![m 0 0, m 0 1; m 1 0, m 1 1] sorry) :
      Matrix (Fin 2) (Fin 2) R)
    ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩) ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩)
Tactic: fin_cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (goal)
Goal:
R : Type v
inst : CommRing R
P : SL(2, R) → Prop
h :
  ∀ (a b c d : R) (hdet : a * d - b * c = 1),
    P (Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) R) ↦ A.det = 1) !![a, b; c, d] ⋯)
m : Matrix (Fin 2) (Fin 2) R
hm : m.det = 1
j : Fin 2
h₁ :
  (↑(Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) R) ↦ A.det = 1) m hm) : Matrix (Fin 2) (Fin 2) R)
      ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) =
    (↑(Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) R) ↦ A.det = 1) !![m 0 0, m 0 1; m 1 0, m 1 1] ⋯) :
        Matrix (Fin 2) (Fin 2) R)
      ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)
⊢ (↑(Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) R) ↦ A.det = 1) m hm) : Matrix (Fin 2) (Fin 2) R)
      ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) j =
    (↑(Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) R) ↦ A.det = 1) !![m 0 0, m 0 1; m 1 0, m 1 1] ⋯) :
        Matrix (Fin 2) (Fin 2) R)
      ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) j
have h₂ : (↑(Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) R) ↦ A.det = 1) m hm) : Matrix (Fin 2) (Fin 2) R)
    ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2)) =
  (↑(Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) R) ↦ A.det = 1) !![m 0 0, m 0 1; m 1 0, m 1 1] sorry) :
      Matrix (Fin 2) (Fin 2) R)
    ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩) ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩)
Tactic: fin_cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (hypothesis)
Goal:
R : Type u_2
inst : Field R
a b c d : R
h_det : a * d - b * c = 1
hg :
  Eq (α := R)
    ((↑(Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) R) ↦ A.det = 1) !![a, b; c, d] ⋯) : Matrix (Fin 2) (Fin 2) R) 1
        0 :
      R)
    (0 : R)
⊢ ∃ (a_1 : R) (b_1 : R) (h : a_1 ≠ 0),
    Eq (α := SL(2, R))
      (Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) R) ↦ A.det = 1) !![a, b; c, d] ⋯ :
        { A : Matrix (Fin 2) (Fin 2) R // A.det = 1 })
      (Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) R) ↦ A.det = 1) !![a_1, b_1; 0, a_1⁻¹] ⋯ :
        { A : Matrix (Fin 2) (Fin 2) R // A.det = 1 })
have hg₁ : c = 0
Tactic: replace hg : c = 0 := by simpa using hg
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (goal)
Goal:
R : Type u_2
inst : Field R
a b c d : R
h_det : a * d - b * c = 1
hg : c = 0
⊢ a * d = 1
have rwa : ∀ (h_det : a * d - b * 0 = 1) (hg : c = 0), a * d = 1
Tactic: rwa [hg, mul_zero, sub_zero] at h_det
Cleared hypotheses: h_det, hg
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (goal)
Goal:
R : Type u_2
inst : Field R
a b c d : R
h_det : a * d - b * c = 1
hg : c = 0
rwa : ∀ (h_det : a * d - b * 0 = 1) (hg : c = 0), a * d = 1
⊢ a * d = 1
have rwa₁ : ∀ (h_det : a * d - 0 = 1) (hg : c = 0), a * d = 1
Tactic: rwa [hg, mul_zero, sub_zero] at h_det
Cleared hypotheses: h_det, hg
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (goal)
Goal:
R : Type u_2
inst : Field R
a b c d : R
h_det : a * d - b * c = 1
hg : c = 0
rwa : ∀ (h_det : a * d - b * 0 = 1) (hg : c = 0), a * d = 1
rwa₁ : ∀ (h_det : a * d - 0 = 1) (hg : c = 0), a * d = 1
⊢ a * d = 1
have rwa₂ : ∀ (h_det : a * d = 1) (hg : c = 0), a * d = 1
Tactic: rwa [hg, mul_zero, sub_zero] at h_det
Cleared hypotheses: h_det, hg
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (hypothesis)
Goal:
R : Type u_2
inst : Field R
a b c d : R
h_det : a * d - b * c = 1
hg : c = 0
⊢ ∃ (a_1 : R) (b_1 : R) (h : a_1 ≠ 0),
    Eq (α := SL(2, R))
      (Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) R) ↦ A.det = 1) !![a, b; c, d] ⋯ :
        { A : Matrix (Fin 2) (Fin 2) R // A.det = 1 })
      (Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) R) ↦ A.det = 1) !![a_1, b_1; 0, a_1⁻¹] ⋯ :
        { A : Matrix (Fin 2) (Fin 2) R // A.det = 1 })
have had : a * d = 1
Tactic: have had : a * d = 1 := by rwa [hg, mul_zero, sub_zero] at h_det
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (goal)
Goal:
R : Type u_2
inst : Field R
a b c d : R
h_det : a * d - b * c = 1
hg : c = 0
had : a * d = 1
⊢ ∃ (a_1 : R) (b_1 : R) (h : a_1 ≠ 0),
    Eq (α := SL(2, R))
      (Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) R) ↦ A.det = 1) !![a, b; c, d] ⋯ :
        { A : Matrix (Fin 2) (Fin 2) R // A.det = 1 })
      (Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) R) ↦ A.det = 1) !![a_1, b_1; 0, a_1⁻¹] ⋯ :
        { A : Matrix (Fin 2) (Fin 2) R // A.det = 1 })
have h : Eq (α := SL(2, R))
  (Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) R) ↦ A.det = 1) !![a, b; c, d] sorry :
    { A : Matrix (Fin 2) (Fin 2) R // A.det = 1 })
  (Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) R) ↦ A.det = 1) !![a, b; 0, a⁻¹] sorry :
    { A : Matrix (Fin 2) (Fin 2) R // A.det = 1 })
Tactic: refine ⟨a, b, left_ne_zero_of_mul_eq_one had, ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (goal)
Goal:
R : Type u_2
inst : Field R
a b c d : R
h_det : a * d - b * c = 1
hg : c = 0
had : a * d = 1
⊢ Eq (α := SL(2, R))
    (Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) R) ↦ A.det = 1) !![a, b; c, d] ⋯ :
      { A : Matrix (Fin 2) (Fin 2) R // A.det = 1 })
    (Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) R) ↦ A.det = 1) !![a, b; 0, a⁻¹] ⋯ :
      { A : Matrix (Fin 2) (Fin 2) R // A.det = 1 })
have h : Eq (α := SL(2, R))
  (Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) R) ↦ A.det = 1) !![a, b; c, a⁻¹] sorry :
    { A : Matrix (Fin 2) (Fin 2) R // A.det = 1 })
  (Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) R) ↦ A.det = 1) !![a, b; 0, a⁻¹] sorry :
    { A : Matrix (Fin 2) (Fin 2) R // A.det = 1 })
Tactic: simp_rw [eq_inv_of_mul_eq_one_right had, hg]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (goal)
Goal:
R : Type u_2
inst : Field R
g : SL(2, R)
hg : (↑g : Matrix (Fin 2) (Fin 2) R) 1 0 = 0
⊢ ∃ (a : R) (b : R) (h : a ≠ 0), g = Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) R) ↦ A.det = 1) !![a, b; 0, a⁻¹] ⋯
have h : ∀ (a b c d : R) (h_det : a * d - b * c = 1)
  (hg :
    Eq (α := R)
      ((↑(Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) R) ↦ A.det = 1) !![a, b; c, d] sorry) : Matrix (Fin 2) (Fin 2) R)
          1 0 :
        R)
      (0 : R)),
  ∃ (a_1 : R) (b_1 : R) (h : a_1 ≠ 0),
    Eq (α := SL(2, R))
      (Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) R) ↦ A.det = 1) !![a, b; c, d] sorry :
        { A : Matrix (Fin 2) (Fin 2) R // A.det = 1 })
      (Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) R) ↦ A.det = 1) !![a_1, b_1; 0, a_1⁻¹] sorry :
        { A : Matrix (Fin 2) (Fin 2) R // A.det = 1 })
Tactic: induction g using Matrix.SpecialLinearGroup.fin_two_induction with | h a b c d h_det =>
  replace hg : c = 0 := by simpa using hg
  have had : a * d = 1 := by rwa [hg, mul_zero, sub_zero] at h_det
  refine ⟨a, b, left_ne_zero_of_mul_eq_one had, ?_⟩
  simp_rw [eq_inv_of_mul_eq_one_right had, hg]
Cleared hypotheses: g, hg
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (goal)
Goal:
R : Type v
inst : CommRing R
A : SL(2, R)
i : Fin 2
⊢ IsCoprime ((↑A : Matrix (Fin 2) (Fin 2) R) i 0) ((↑A : Matrix (Fin 2) (Fin 2) R) i 1)
have refine_1 : (↑A : Matrix (Fin 2) (Fin 2) R) 1 1 * (↑A : Matrix (Fin 2) (Fin 2) R) 0 0 +
    -(↑A : Matrix (Fin 2) (Fin 2) R) 1 0 * (↑A : Matrix (Fin 2) (Fin 2) R) 0 1 =
  1
Tactic: refine match i with
  | 0 => ⟨A 1 1, -(A 1 0), ?_⟩
  | 1 => ⟨-(A 0 1), A 0 0, ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (goal)
Goal:
R : Type v
inst : CommRing R
A : SL(2, R)
i : Fin 2
refine_1 :
  (↑A : Matrix (Fin 2) (Fin 2) R) 1 1 * (↑A : Matrix (Fin 2) (Fin 2) R) 0 0 +
      -(↑A : Matrix (Fin 2) (Fin 2) R) 1 0 * (↑A : Matrix (Fin 2) (Fin 2) R) 0 1 =
    1
⊢ IsCoprime ((↑A : Matrix (Fin 2) (Fin 2) R) i 0) ((↑A : Matrix (Fin 2) (Fin 2) R) i 1)
have refine_2 : -(↑A : Matrix (Fin 2) (Fin 2) R) 0 1 * (↑A : Matrix (Fin 2) (Fin 2) R) 1 0 +
    (↑A : Matrix (Fin 2) (Fin 2) R) 0 0 * (↑A : Matrix (Fin 2) (Fin 2) R) 1 1 =
  1
Tactic: refine match i with
  | 0 => ⟨A 1 1, -(A 1 0), ?_⟩
  | 1 => ⟨-(A 0 1), A 0 0, ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (goal)
Goal:
R : Type v
inst : CommRing R
A : SL(2, R)
i : Fin 2
⊢ (↑A : Matrix (Fin 2) (Fin 2) R) 1 1 * (↑A : Matrix (Fin 2) (Fin 2) R) 0 0 +
      -(↑A : Matrix (Fin 2) (Fin 2) R) 1 0 * (↑A : Matrix (Fin 2) (Fin 2) R) 0 1 =
    1
have refine_1 : (↑A : Matrix (Fin 2) (Fin 2) R) 1 1 * (↑A : Matrix (Fin 2) (Fin 2) R) 0 0 +
    -(↑A : Matrix (Fin 2) (Fin 2) R) 1 0 * (↑A : Matrix (Fin 2) (Fin 2) R) 0 1 =
  (↑A : Matrix (Fin 2) (Fin 2) R) 0 0 * (↑A : Matrix (Fin 2) (Fin 2) R) 1 1 -
    (↑A : Matrix (Fin 2) (Fin 2) R) 0 1 * (↑A : Matrix (Fin 2) (Fin 2) R) 1 0
Tactic: simp_rw [det_coe A ▸ det_fin_two A.1]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (goal)
Goal:
R : Type v
inst : CommRing R
A : SL(2, R)
i : Fin 2
⊢ -(↑A : Matrix (Fin 2) (Fin 2) R) 0 1 * (↑A : Matrix (Fin 2) (Fin 2) R) 1 0 +
      (↑A : Matrix (Fin 2) (Fin 2) R) 0 0 * (↑A : Matrix (Fin 2) (Fin 2) R) 1 1 =
    1
have refine_2 : -(↑A : Matrix (Fin 2) (Fin 2) R) 0 1 * (↑A : Matrix (Fin 2) (Fin 2) R) 1 0 +
    (↑A : Matrix (Fin 2) (Fin 2) R) 0 0 * (↑A : Matrix (Fin 2) (Fin 2) R) 1 1 =
  (↑A : Matrix (Fin 2) (Fin 2) R) 0 0 * (↑A : Matrix (Fin 2) (Fin 2) R) 1 1 -
    (↑A : Matrix (Fin 2) (Fin 2) R) 0 1 * (↑A : Matrix (Fin 2) (Fin 2) R) 1 0
Tactic: simp_rw [det_coe A ▸ det_fin_two A.1]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (goal)
Goal:
R : Type v
inst : CommRing R
A : SL(2, R)
j : Fin 2
⊢ IsCoprime ((↑A : Matrix (Fin 2) (Fin 2) R) 0 j) ((↑A : Matrix (Fin 2) (Fin 2) R) 1 j)
have refine_1 : (↑A : Matrix (Fin 2) (Fin 2) R) 1 1 * (↑A : Matrix (Fin 2) (Fin 2) R) 0 0 +
    -(↑A : Matrix (Fin 2) (Fin 2) R) 0 1 * (↑A : Matrix (Fin 2) (Fin 2) R) 1 0 =
  1
Tactic: refine match j with
  | 0 => ⟨A 1 1, -(A 0 1), ?_⟩
  | 1 => ⟨-(A 1 0), A 0 0, ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (goal)
Goal:
R : Type v
inst : CommRing R
A : SL(2, R)
j : Fin 2
refine_1 :
  (↑A : Matrix (Fin 2) (Fin 2) R) 1 1 * (↑A : Matrix (Fin 2) (Fin 2) R) 0 0 +
      -(↑A : Matrix (Fin 2) (Fin 2) R) 0 1 * (↑A : Matrix (Fin 2) (Fin 2) R) 1 0 =
    1
⊢ IsCoprime ((↑A : Matrix (Fin 2) (Fin 2) R) 0 j) ((↑A : Matrix (Fin 2) (Fin 2) R) 1 j)
have refine_2 : -(↑A : Matrix (Fin 2) (Fin 2) R) 1 0 * (↑A : Matrix (Fin 2) (Fin 2) R) 0 1 +
    (↑A : Matrix (Fin 2) (Fin 2) R) 0 0 * (↑A : Matrix (Fin 2) (Fin 2) R) 1 1 =
  1
Tactic: refine match j with
  | 0 => ⟨A 1 1, -(A 0 1), ?_⟩
  | 1 => ⟨-(A 1 0), A 0 0, ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (goal)
Goal:
R : Type v
inst : CommRing R
A : SL(2, R)
j : Fin 2
⊢ (↑A : Matrix (Fin 2) (Fin 2) R) 1 1 * (↑A : Matrix (Fin 2) (Fin 2) R) 0 0 +
      -(↑A : Matrix (Fin 2) (Fin 2) R) 0 1 * (↑A : Matrix (Fin 2) (Fin 2) R) 1 0 =
    1
have refine_1 : (↑A : Matrix (Fin 2) (Fin 2) R) 1 1 * (↑A : Matrix (Fin 2) (Fin 2) R) 0 0 +
    -(↑A : Matrix (Fin 2) (Fin 2) R) 0 1 * (↑A : Matrix (Fin 2) (Fin 2) R) 1 0 =
  (↑A : Matrix (Fin 2) (Fin 2) R) 0 0 * (↑A : Matrix (Fin 2) (Fin 2) R) 1 1 -
    (↑A : Matrix (Fin 2) (Fin 2) R) 0 1 * (↑A : Matrix (Fin 2) (Fin 2) R) 1 0
Tactic: simp_rw [det_coe A ▸ det_fin_two A.1]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (goal)
Goal:
R : Type v
inst : CommRing R
A : SL(2, R)
j : Fin 2
⊢ -(↑A : Matrix (Fin 2) (Fin 2) R) 1 0 * (↑A : Matrix (Fin 2) (Fin 2) R) 0 1 +
      (↑A : Matrix (Fin 2) (Fin 2) R) 0 0 * (↑A : Matrix (Fin 2) (Fin 2) R) 1 1 =
    1
have refine_2 : -(↑A : Matrix (Fin 2) (Fin 2) R) 1 0 * (↑A : Matrix (Fin 2) (Fin 2) R) 0 1 +
    (↑A : Matrix (Fin 2) (Fin 2) R) 0 0 * (↑A : Matrix (Fin 2) (Fin 2) R) 1 1 =
  (↑A : Matrix (Fin 2) (Fin 2) R) 0 0 * (↑A : Matrix (Fin 2) (Fin 2) R) 1 1 -
    (↑A : Matrix (Fin 2) (Fin 2) R) 0 1 * (↑A : Matrix (Fin 2) (Fin 2) R) 1 0
Tactic: simp_rw [det_coe A ▸ det_fin_two A.1]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (goal)
Goal:
R : Type u_1
inst : CommRing R
a b : R
hab : IsCoprime a b
j : Fin 2
⊢ ∃ (g : SL(2, R)), (↑g : Matrix (Fin 2) (Fin 2) R) 0 j = a ∧ (↑g : Matrix (Fin 2) (Fin 2) R) 1 j = b
have obtain : ∀ (u v : R) (h : u * a + v * b = 1),
  ∃ (g : SL(2, R)), (↑g : Matrix (Fin 2) (Fin 2) R) 0 j = a ∧ (↑g : Matrix (Fin 2) (Fin 2) R) 1 j = b
Tactic: obtain ⟨u, v, h⟩ := hab
Cleared hypotheses: hab
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (goal)
Goal:
R : Type u_1
inst : CommRing R
a b : R
j : Fin 2
u v : R
h : u * a + v * b = 1
⊢ ∃ (g : SL(2, R)), (↑g : Matrix (Fin 2) (Fin 2) R) 0 j = a ∧ (↑g : Matrix (Fin 2) (Fin 2) R) 1 j = b
have refine_1 : Eq.{u_1 + 1} (α := R) (det (n := Fin 2) !![a, -v; b, u]) 1
Tactic: refine match j with
  | 0 => ⟨⟨!![a, -v; b, u], ?_⟩, rfl, rfl⟩
  | 1 => ⟨⟨!![v, a; -u, b], ?_⟩, rfl, rfl⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (goal)
Goal:
R : Type u_1
inst : CommRing R
a b : R
j : Fin 2
u v : R
h : u * a + v * b = 1
refine_1 : Eq.{u_1 + 1} (α := R) (det (n := Fin 2) !![a, -v; b, u]) 1
⊢ ∃ (g : SL(2, R)), (↑g : Matrix (Fin 2) (Fin 2) R) 0 j = a ∧ (↑g : Matrix (Fin 2) (Fin 2) R) 1 j = b
have refine_2 : Eq.{u_1 + 1} (α := R) (det (n := Fin 2) !![v, a; -u, b]) 1
Tactic: refine match j with
  | 0 => ⟨⟨!![a, -v; b, u], ?_⟩, rfl, rfl⟩
  | 1 => ⟨⟨!![v, a; -u, b], ?_⟩, rfl, rfl⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (goal)
Goal:
R : Type u_1
inst : CommRing R
a b : R
j : Fin 2
u v : R
h : u * a + v * b = 1
⊢ Eq.{u_1 + 1} (α := R) (det (n := Fin 2) !![a, -v; b, u]) 1
have refine_1 : a * u - -v * b = u * a + v * b
Tactic: rw [Matrix.det_fin_two_of, ← h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (goal)
Goal:
R : Type u_1
inst : CommRing R
a b : R
j : Fin 2
u v : R
h : u * a + v * b = 1
⊢ Eq.{u_1 + 1} (α := R) (det (n := Fin 2) !![v, a; -u, b]) 1
have refine_2 : v * b - a * -u = u * a + v * b
Tactic: rw [Matrix.det_fin_two_of, ← h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (goal)
Goal:
R : Type u_1
inst : CommRing R
a b : R
hab : IsCoprime a b
i : Fin 2
⊢ ∃ (g : SL(2, R)), (↑g : Matrix (Fin 2) (Fin 2) R) i 0 = a ∧ (↑g : Matrix (Fin 2) (Fin 2) R) i 1 = b
have obtain : ∀ (u v : R) (h : u * a + v * b = 1),
  ∃ (g : SL(2, R)), (↑g : Matrix (Fin 2) (Fin 2) R) i 0 = a ∧ (↑g : Matrix (Fin 2) (Fin 2) R) i 1 = b
Tactic: obtain ⟨u, v, h⟩ := hab
Cleared hypotheses: hab
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (goal)
Goal:
R : Type u_1
inst : CommRing R
a b : R
i : Fin 2
u v : R
h : u * a + v * b = 1
⊢ ∃ (g : SL(2, R)), (↑g : Matrix (Fin 2) (Fin 2) R) i 0 = a ∧ (↑g : Matrix (Fin 2) (Fin 2) R) i 1 = b
have refine_1 : Eq.{u_1 + 1} (α := R) (det (n := Fin 2) !![a, b; -v, u]) 1
Tactic: refine match i with
  | 0 => ⟨⟨!![a, b; -v, u], ?_⟩, rfl, rfl⟩
  | 1 => ⟨⟨!![v, -u; a, b], ?_⟩, rfl, rfl⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (goal)
Goal:
R : Type u_1
inst : CommRing R
a b : R
i : Fin 2
u v : R
h : u * a + v * b = 1
refine_1 : Eq.{u_1 + 1} (α := R) (det (n := Fin 2) !![a, b; -v, u]) 1
⊢ ∃ (g : SL(2, R)), (↑g : Matrix (Fin 2) (Fin 2) R) i 0 = a ∧ (↑g : Matrix (Fin 2) (Fin 2) R) i 1 = b
have refine_2 : Eq.{u_1 + 1} (α := R) (det (n := Fin 2) !![v, -u; a, b]) 1
Tactic: refine match i with
  | 0 => ⟨⟨!![a, b; -v, u], ?_⟩, rfl, rfl⟩
  | 1 => ⟨⟨!![v, -u; a, b], ?_⟩, rfl, rfl⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (goal)
Goal:
R : Type u_1
inst : CommRing R
a b : R
i : Fin 2
u v : R
h : u * a + v * b = 1
⊢ Eq.{u_1 + 1} (α := R) (det (n := Fin 2) !![a, b; -v, u]) 1
have refine_1 : a * u - b * -v = u * a + v * b
Tactic: rw [Matrix.det_fin_two_of, ← h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (goal)
Goal:
R : Type u_1
inst : CommRing R
a b : R
i : Fin 2
u v : R
h : u * a + v * b = 1
⊢ Eq.{u_1 + 1} (α := R) (det (n := Fin 2) !![v, -u; a, b]) 1
have refine_2 : v * b - -u * a = u * a + v * b
Tactic: rw [Matrix.det_fin_two_of, ← h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (goal)
Goal:
R : Type u_1
inst : CommRing R
v : Fin 2 → R
hab : IsCoprime (v 0) (v 1)
A : SL(2, R)
⊢ IsCoprime ((v ᵥ* (↑A : Matrix (Fin 2) (Fin 2) R)) 0) ((v ᵥ* (↑A : Matrix (Fin 2) (Fin 2) R)) 1)
have obtain : ∀ (g : SL(2, R)) (hg : (↑g : Matrix (Fin 2) (Fin 2) R) 0 0 = v 0 ∧ (↑g : Matrix (Fin 2) (Fin 2) R) 0 1 = v 1),
  IsCoprime ((v ᵥ* (↑A : Matrix (Fin 2) (Fin 2) R)) 0) ((v ᵥ* (↑A : Matrix (Fin 2) (Fin 2) R)) 1)
Tactic: obtain ⟨g, hg⟩ := hab.exists_SL2_row 0
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (goal)
Goal:
R : Type u_1
inst : CommRing R
v : Fin 2 → R
hab : IsCoprime (v 0) (v 1)
A g : SL(2, R)
hg : (↑g : Matrix (Fin 2) (Fin 2) R) 0 0 = v 0 ∧ (↑g : Matrix (Fin 2) (Fin 2) R) 0 1 = v 1
t : Fin 2
⊢ v t = (↑g : Matrix (Fin 2) (Fin 2) R) 0 t
have 0 : v ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2)) = (↑g : Matrix (Fin 2) (Fin 2) R) 0 ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩)
Tactic: fin_cases t
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (goal)
Goal:
R : Type u_1
inst : CommRing R
v : Fin 2 → R
hab : IsCoprime (v 0) (v 1)
A g : SL(2, R)
hg : (↑g : Matrix (Fin 2) (Fin 2) R) 0 0 = v 0 ∧ (↑g : Matrix (Fin 2) (Fin 2) R) 0 1 = v 1
t : Fin 2
0 : v ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) = (↑g : Matrix (Fin 2) (Fin 2) R) 0 ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)
⊢ v t = (↑g : Matrix (Fin 2) (Fin 2) R) 0 t
have 1 : v ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2)) = (↑g : Matrix (Fin 2) (Fin 2) R) 0 ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩)
Tactic: fin_cases t
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (goal)
Goal:
R : Type u_1
inst : CommRing R
v : Fin 2 → R
hab : IsCoprime (v 0) (v 1)
A g : SL(2, R)
hg : (↑g : Matrix (Fin 2) (Fin 2) R) 0 0 = v 0 ∧ (↑g : Matrix (Fin 2) (Fin 2) R) 0 1 = v 1
⊢ v ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) = (↑g : Matrix (Fin 2) (Fin 2) R) 0 ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)
have 0 : (↑g : Matrix (Fin 2) (Fin 2) R) 0 0 = v 0 →
  (↑g : Matrix (Fin 2) (Fin 2) R) 0 1 = v 1 →
    v ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2)) = (↑g : Matrix (Fin 2) (Fin 2) R) 0 ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩)
Tactic: tauto
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (goal)
Goal:
R : Type u_1
inst : CommRing R
v : Fin 2 → R
hab : IsCoprime (v 0) (v 1)
A g : SL(2, R)
hg : (↑g : Matrix (Fin 2) (Fin 2) R) 0 0 = v 0 ∧ (↑g : Matrix (Fin 2) (Fin 2) R) 0 1 = v 1
⊢ v ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) = (↑g : Matrix (Fin 2) (Fin 2) R) 0 ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)
have 1 : (↑g : Matrix (Fin 2) (Fin 2) R) 0 0 = v 0 →
  (↑g : Matrix (Fin 2) (Fin 2) R) 0 1 = v 1 →
    v ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2)) = (↑g : Matrix (Fin 2) (Fin 2) R) 0 ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩)
Tactic: tauto
Cleared hypotheses: hg