awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
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] ⋯)
g : SL(2, R)
obtain :
  ∀ (m : Matrix (Fin 2) (Fin 2) R) (hm : m.det = 1),
    P (Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) R) ↦ A.det = 1) m hm)
⊢ P g

Tactic:
obtain ⟨m, hm⟩ := g
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
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
rwa rwa₁ rwa₂ rwa₃ : ∀ (hm : m 0 0 * m 1 1 - m 0 1 * m 1 0 = 1), m 0 0 * m 1 1 - m 0 1 * m 1 0 = 1
⊢ m 0 0 * m 1 1 - m 0 1 * m 1 0 = 1

Tactic:
rwa [det_fin_two] at hm

Premises used: Matrix.det_fin_two
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
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
h₁ :
  Eq (α := SL(2, R)) (Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) R) ↦ A.det = 1) m hm)
    (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] ⋯)
⊢ P (Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) R) ↦ A.det = 1) m hm)

Tactic:
convert! h (m 0 0) (m 0 1) (m 1 0) (m 1 1) (by rwa [det_fin_two] at hm)

Premises used: OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
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
h₁ :
  ∀ (i 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) 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
⊢ Eq (α := SL(2, R)) (Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) R) ↦ A.det = 1) m hm)
    (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] ⋯)

Tactic:
ext i j
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
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
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)) 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
⊢ (↑(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

Tactic:
fin_cases i
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
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, ⋯⟩)
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) (⟨1, ⋯⟩ : 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) ⟨1, ⋯⟩)
⊢ (↑(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

Tactic:
fin_cases j
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
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, ⋯⟩)
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) (⟨1, ⋯⟩ : 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) ⟨1, ⋯⟩)
⊢ (↑(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

Tactic:
fin_cases j
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
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
⊢ (↑(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, ⋯⟩)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
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
⊢ (↑(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) (⟨1, ⋯⟩ : 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) ⟨1, ⋯⟩)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
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
⊢ (↑(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, ⋯⟩)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
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
⊢ (↑(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) (⟨1, ⋯⟩ : 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) ⟨1, ⋯⟩)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R_1 : Type v
inst_2 : CommRing R_1
S : Type u_1
inst_3 : CommRing S
R : Type u_2
inst_4 : Field R
g : SL(2, R)
hg : (↑g : Matrix (Fin 2) (Fin 2) R) 1 0 = 0
a b : R
h : a ≠ 0
⊢ Eq.{u_2 + 1} (α := R) (det (n := Fin 2) !![a, b; 0, a⁻¹]) 1

Tactic:
simp [h]
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
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)
⊢ c = 0

Tactic:
simpa using hg
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
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)
⊢ c = 0

Tactic:
replace hg : c = 0 := by simpa using hg
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
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
rwa₂ rwa₃ rwa₄ rwa₅ : ∀ (h_det : a * d = 1) (hg : c = 0), a * d = 1
⊢ a * d = 1

Tactic:
rwa [hg, mul_zero, sub_zero] at h_det

Premises used: sub_zero, MulZeroClass.mul_zero
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
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

Tactic:
have had : a * d = 1 := by rwa [hg, mul_zero, sub_zero] at h_det
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
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 })

Tactic:
⟨a, b, left_ne_zero_of_mul_eq_one had, ?_⟩

Premises used: Exists.intro, left_ne_zero_of_mul_eq_one
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
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
h :
  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 })
⊢ ∃ (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 })

Tactic:
refine ⟨a, b, left_ne_zero_of_mul_eq_one had, ?_⟩
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
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
h :
  Eq (α := SL(2, R))
    (Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) R) ↦ A.det = 1) !![a, b; c, a⁻¹] ⋯ :
      { 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 })
⊢ 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 })

Tactic:
simp_rw [eq_inv_of_mul_eq_one_right had, hg]

Premises used: eq_inv_of_mul_eq_one_right
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Goal:
R : Type u_2
inst : Field R
g : SL(2, R)
hg : (↑g : Matrix (Fin 2) (Fin 2) R) 1 0 = 0
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] ⋯) :
              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 })
⊢ ∃ (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⁻¹] ⋯

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]

Premises used: Matrix.SpecialLinearGroup.fin_two_induction
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
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)

Tactic:
match i with
  | 0 => ⟨A 1 1, -(A 1 0), ?_⟩
  | 1 => ⟨-(A 0 1), A 0 0, ?_⟩

Premises used: _private.0.Matrix.SpecialLinearGroup.isCoprime_row.match_1, Exists.intro, OfNat.ofNat, Subtype.val, Neg.neg, IsCoprime
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
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
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
⊢ IsCoprime ((↑A : Matrix (Fin 2) (Fin 2) R) i 0) ((↑A : Matrix (Fin 2) (Fin 2) R) i 1)

Tactic:
refine match i with
  | 0 => ⟨A 1 1, -(A 1 0), ?_⟩
  | 1 => ⟨-(A 0 1), A 0 0, ?_⟩
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
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 =
    (↑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
⊢ (↑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:
simp_rw [det_coe A ▸ det_fin_two A.1]
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
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 =
    (↑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:
ring
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Goal:
R : Type v
inst : CommRing R
A : SL(2, R)
i : Fin 2
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
⊢ -(↑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:
simp_rw [det_coe A ▸ det_fin_two A.1]
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
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 =
    (↑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:
ring
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
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)

Tactic:
match j with
  | 0 => ⟨A 1 1, -(A 0 1), ?_⟩
  | 1 => ⟨-(A 1 0), A 0 0, ?_⟩

Premises used: _private.0.Matrix.SpecialLinearGroup.isCoprime_row.match_1, Exists.intro, OfNat.ofNat, Subtype.val, Neg.neg, IsCoprime
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
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
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
⊢ IsCoprime ((↑A : Matrix (Fin 2) (Fin 2) R) 0 j) ((↑A : Matrix (Fin 2) (Fin 2) R) 1 j)

Tactic:
refine match j with
  | 0 => ⟨A 1 1, -(A 0 1), ?_⟩
  | 1 => ⟨-(A 1 0), A 0 0, ?_⟩
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
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 =
    (↑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
⊢ (↑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:
simp_rw [det_coe A ▸ det_fin_two A.1]
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
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 =
    (↑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:
ring
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Goal:
R : Type v
inst : CommRing R
A : SL(2, R)
j : Fin 2
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
⊢ -(↑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:
simp_rw [det_coe A ▸ det_fin_two A.1]
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
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 =
    (↑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:
ring
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Goal:
R : Type u_1
inst : CommRing R
a b : R
hab : IsCoprime a b
j : Fin 2
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
⊢ ∃ (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
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
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

Tactic:
match j with
  | 0 => ⟨⟨!![a, -v; b, u], ?_⟩, rfl, rfl⟩
  | 1 => ⟨⟨!![v, a; -u, b], ?_⟩, rfl, rfl⟩

Premises used: Matrix.of, Exists, Subtype.mk, And, _private.0.Matrix.SpecialLinearGroup.isCoprime_row.match_1, And.intro, Exists.intro, Matrix.vecEmpty, OfNat.ofNat, Subtype.val, Eq, DFunLike.coe, Matrix.vecCons, Neg.neg, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
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
refine_2 : Eq.{u_1 + 1} (α := R) (det (n := Fin 2) !![v, a; -u, 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:
refine match j with
  | 0 => ⟨⟨!![a, -v; b, u], ?_⟩, rfl, rfl⟩
  | 1 => ⟨⟨!![v, a; -u, b], ?_⟩, rfl, rfl⟩
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
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 : a * u - -v * b = u * a + v * b
⊢ Eq.{u_1 + 1} (α := R) (det (n := Fin 2) !![a, -v; b, u]) 1

Tactic:
rw [Matrix.det_fin_two_of, ← h]

Premises used: Matrix.det_fin_two_of
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Goal:
R : Type u_1
inst : CommRing R
a b : R
j : Fin 2
u v : R
h : u * a + v * b = 1
⊢ a * u - -v * b = u * a + v * b

Tactic:
ring
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Goal:
R : Type u_1
inst : CommRing R
a b : R
j : Fin 2
u v : R
h : u * a + v * b = 1
refine_2 : v * b - a * -u = u * a + v * b
⊢ Eq.{u_1 + 1} (α := R) (det (n := Fin 2) !![v, a; -u, b]) 1

Tactic:
rw [Matrix.det_fin_two_of, ← h]

Premises used: Matrix.det_fin_two_of
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Goal:
R : Type u_1
inst : CommRing R
a b : R
j : Fin 2
u v : R
h : u * a + v * b = 1
⊢ v * b - a * -u = u * a + v * b

Tactic:
ring