awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (goal)
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
S : Type u_1
inst_3 : CommRing S
i : n
A B : ↥(center (SpecialLinearGroup n R))
⊢ (↑(↑(rootsOfUnity.mkOfPowEq
              (((↑(↑A : SpecialLinearGroup n R) : Matrix n n R) * (↑(↑B : SpecialLinearGroup n R) : Matrix n n R)) i i)
              ⋯) :
          Rˣ) :
      R) =
    (↑(↑(HMul.hMul (α := ↥(rootsOfUnity (Fintype.card n) R))
              (rootsOfUnity.mkOfPowEq ((↑(↑A : SpecialLinearGroup n R) : Matrix n n R) i i) ⋯)
              (rootsOfUnity.mkOfPowEq ((↑(↑B : SpecialLinearGroup n R) : Matrix n n R) i i) ⋯)) :
          Rˣ) :
      R)
have a : ((↑(↑A : SpecialLinearGroup n R) : Matrix n n R) * (↑(↑B : SpecialLinearGroup n R) : Matrix n n R)) i i =
  (↑(↑A : SpecialLinearGroup n R) : Matrix n n R) i i * (↑(↑B : SpecialLinearGroup n R) : Matrix n n R) i i
Tactic: simp only [rootsOfUnity.val_mkOfPowEq_coe, Subgroup.coe_mul, Units.val_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (goal)
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
S : Type u_1
inst_3 : CommRing S
i : n
A B : ↥(center (SpecialLinearGroup n R))
⊢ ((↑(↑A : SpecialLinearGroup n R) : Matrix n n R) * (↑(↑B : SpecialLinearGroup n R) : Matrix n n R)) i i =
    (↑(↑A : SpecialLinearGroup n R) : Matrix n n R) i i * (↑(↑B : SpecialLinearGroup n R) : Matrix n n R) i i
have a : HMul.hMul (α := Matrix n n R) (β := Matrix n n R)
    ((scalar n : (a : R) → Matrix n n R) ((↑(↑A : SpecialLinearGroup n R) : Matrix n n R) i i) : Matrix n n R)
    ((scalar n : (a : R) → Matrix n n R) ((↑(↑B : SpecialLinearGroup n R) : Matrix n n R) i i) : Matrix n n R) i i =
  HMul.hMul (α := R) (β := R)
    ((scalar n : (a : R) → Matrix n n R) ((↑(↑A : SpecialLinearGroup n R) : Matrix n n R) i i) i i : R)
    ((scalar n : (a : R) → Matrix n n R) ((↑(↑B : SpecialLinearGroup n R) : Matrix n n R) i i) i i : R)
Tactic: rw [← scalar_eq_coe_self_center A i, ← scalar_eq_coe_self_center B i]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (goal)
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
S : Type u_1
inst_3 : CommRing S
hn : IsEmpty n
⊢ ↥(center (SpecialLinearGroup n R)) ≃* ↥(rootsOfUnity (max (Fintype.card n) 1) R)
have rw : ↥⊥ ≃* ↥⊥
Tactic: rw [center_eq_bot_of_subsingleton, Fintype.card_eq_zero, max_eq_right_of_lt zero_lt_one,
      rootsOfUnity_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (goal)
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
A : ↥(center (SpecialLinearGroup n R))
⊢ (↑(↑A : SpecialLinearGroup n R) : Matrix n n R) =
    (scalar n : (a : R) → Matrix n n R)
      (↑(↑((center_equiv_rootsOfUnity :
                  (a : ↥(center (SpecialLinearGroup n R))) → ↥(rootsOfUnity (max (Fintype.card n) 1) R))
                A) :
            Rˣ) :
        R)
have unfold : (↑(↑A : SpecialLinearGroup n R) : Matrix n n R) =
  (scalar n : (a : R) → Matrix n n R)
    (↑(↑((if hp : IsEmpty n then
                  (fun (hn : IsEmpty n) ↦
                      (Eq.mpr sorry (Eq.mpr sorry (Eq.mpr sorry (Eq.mpr sorry MulEquiv.ofUnique))) :
                        ↥(center (SpecialLinearGroup n R)) ≃* ↥(rootsOfUnity (max (Fintype.card n) 1) R)))
                    hp
                else
                  (fun (x : Nonempty n) ↦
                      (Eq.rec (motive := fun (x : ℕ) (h : Fintype.card n = x) ↦
                          ↥(center (SpecialLinearGroup n R)) ≃* ↥(rootsOfUnity x R))
                          (center_equiv_rootsOfUnity' (Classical.arbitrary n)) sorry :
                        ↥(center (SpecialLinearGroup n R)) ≃* ↥(rootsOfUnity (max (Fintype.card n) 1) R)))
                    sorry :
                (a : ↥(center (SpecialLinearGroup n R))) → ↥(rootsOfUnity (max (Fintype.card n) 1) R))
              A) :
          Rˣ) :
      R)
Tactic: unfold center_equiv_rootsOfUnity Or.by_cases
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (goal)
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
A : ↥(center (SpecialLinearGroup n R))
⊢ (↑(↑A : SpecialLinearGroup n R) : Matrix n n R) =
    (scalar n : (a : R) → Matrix n n R)
      (↑(↑((if hp : IsEmpty n then
                    (fun (hn : IsEmpty n) ↦
                        (Eq.mpr ⋯ (Eq.mpr ⋯ (Eq.mpr ⋯ (Eq.mpr ⋯ MulEquiv.ofUnique))) :
                          ↥(center (SpecialLinearGroup n R)) ≃* ↥(rootsOfUnity (max (Fintype.card n) 1) R)))
                      hp
                  else
                    (fun (x : Nonempty n) ↦
                        (Eq.rec (motive := fun (x : ℕ) (h : Fintype.card n = x) ↦
                            ↥(center (SpecialLinearGroup n R)) ≃* ↥(rootsOfUnity x R))
                            (center_equiv_rootsOfUnity' (Classical.arbitrary n)) ⋯ :
                          ↥(center (SpecialLinearGroup n R)) ≃* ↥(rootsOfUnity (max (Fintype.card n) 1) R)))
                      ⋯ :
                  (a : ↥(center (SpecialLinearGroup n R))) → ↥(rootsOfUnity (max (Fintype.card n) 1) R))
                A) :
            Rˣ) :
        R)
have pos : ∀ (h : IsEmpty n),
  (↑(↑A : SpecialLinearGroup n R) : Matrix n n R) =
    (scalar n : (a : R) → Matrix n n R)
      (↑(↑(((fun (hn : IsEmpty n) ↦
                      (Eq.mpr sorry (Eq.mpr sorry (Eq.mpr sorry (Eq.mpr sorry MulEquiv.ofUnique))) :
                        ↥(center (SpecialLinearGroup n R)) ≃* ↥(rootsOfUnity (max (Fintype.card n) 1) R)))
                    h :
                  (a : ↥(center (SpecialLinearGroup n R))) → ↥(rootsOfUnity (max (Fintype.card n) 1) R))
                A) :
            Rˣ) :
        R)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (goal)
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
A : ↥(center (SpecialLinearGroup n R))
pos :
  ∀ (h : IsEmpty n),
    (↑(↑A : SpecialLinearGroup n R) : Matrix n n R) =
      (scalar n : (a : R) → Matrix n n R)
        (↑(↑(((fun (hn : IsEmpty n) ↦
                        (Eq.mpr ⋯ (Eq.mpr ⋯ (Eq.mpr ⋯ (Eq.mpr ⋯ MulEquiv.ofUnique))) :
                          ↥(center (SpecialLinearGroup n R)) ≃* ↥(rootsOfUnity (max (Fintype.card n) 1) R)))
                      h :
                    (a : ↥(center (SpecialLinearGroup n R))) → ↥(rootsOfUnity (max (Fintype.card n) 1) R))
                  A) :
              Rˣ) :
          R)
⊢ (↑(↑A : SpecialLinearGroup n R) : Matrix n n R) =
    (scalar n : (a : R) → Matrix n n R)
      (↑(↑((if hp : IsEmpty n then
                    (fun (hn : IsEmpty n) ↦
                        (Eq.mpr ⋯ (Eq.mpr ⋯ (Eq.mpr ⋯ (Eq.mpr ⋯ MulEquiv.ofUnique))) :
                          ↥(center (SpecialLinearGroup n R)) ≃* ↥(rootsOfUnity (max (Fintype.card n) 1) R)))
                      hp
                  else
                    (fun (x : Nonempty n) ↦
                        (Eq.rec (motive := fun (x : ℕ) (h : Fintype.card n = x) ↦
                            ↥(center (SpecialLinearGroup n R)) ≃* ↥(rootsOfUnity x R))
                            (center_equiv_rootsOfUnity' (Classical.arbitrary n)) ⋯ :
                          ↥(center (SpecialLinearGroup n R)) ≃* ↥(rootsOfUnity (max (Fintype.card n) 1) R)))
                      ⋯ :
                  (a : ↥(center (SpecialLinearGroup n R))) → ↥(rootsOfUnity (max (Fintype.card n) 1) R))
                A) :
            Rˣ) :
        R)
have neg : ∀ (h : ¬IsEmpty n),
  (↑(↑A : SpecialLinearGroup n R) : Matrix n n R) =
    (scalar n : (a : R) → Matrix n n R)
      (↑(↑(((fun (x : Nonempty n) ↦
                      (Eq.rec (motive := fun (x : ℕ) (h : Fintype.card n = x) ↦
                          ↥(center (SpecialLinearGroup n R)) ≃* ↥(rootsOfUnity x R))
                          (center_equiv_rootsOfUnity' (Classical.arbitrary n)) sorry :
                        ↥(center (SpecialLinearGroup n R)) ≃* ↥(rootsOfUnity (max (Fintype.card n) 1) R)))
                    sorry :
                  (a : ↥(center (SpecialLinearGroup n R))) → ↥(rootsOfUnity (max (Fintype.card n) 1) R))
                A) :
            Rˣ) :
        R)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (goal)
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
A : ↥(center (SpecialLinearGroup n R))
h : ¬IsEmpty n
⊢ (↑(↑A : SpecialLinearGroup n R) : Matrix n n R) =
    (scalar n : (a : R) → Matrix n n R)
      (↑(↑(((Eq.rec (motive := fun (x : ℕ) (h : Fintype.card n = x) ↦
                      ↥(center (SpecialLinearGroup n R)) ≃* ↥(rootsOfUnity x R))
                      (center_equiv_rootsOfUnity' (Classical.arbitrary n)) ⋯ :
                    ↥(center (SpecialLinearGroup n R)) ≃* ↥(rootsOfUnity (max (Fintype.card n) 1) R)) :
                  (a : ↥(center (SpecialLinearGroup n R))) → ↥(rootsOfUnity (max (Fintype.card n) 1) R))
                A) :
            Rˣ) :
        R)
have neg : ∀ (pf : Nonempty n) (eq : Fintype.card n = max (Fintype.card n) 1),
  (↑(↑A : SpecialLinearGroup n R) : Matrix n n R) =
    (scalar n : (a : R) → Matrix n n R)
      (↑(↑(((Eq.rec (motive := fun (x : ℕ) (h : Fintype.card n = x) ↦
                      ↥(center (SpecialLinearGroup n R)) ≃* ↥(rootsOfUnity x R))
                      (center_equiv_rootsOfUnity' (Classical.arbitrary n)) eq :
                    ↥(center (SpecialLinearGroup n R)) ≃* ↥(rootsOfUnity (max (Fintype.card n) 1) R)) :
                  (a : ↥(center (SpecialLinearGroup n R))) → ↥(rootsOfUnity (max (Fintype.card n) 1) R))
                A) :
            Rˣ) :
        R)
Tactic: generalize_proofs _ eq
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (goal)
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
A : ↥(center (SpecialLinearGroup n R))
h : ¬IsEmpty n
pf : Nonempty n
eq : Fintype.card n = max (Fintype.card n) 1
⊢ (↑(↑A : SpecialLinearGroup n R) : Matrix n n R) =
    (scalar n : (a : R) → Matrix n n R)
      (↑(↑(((Eq.rec (motive := fun (x : ℕ) (h : Fintype.card n = x) ↦
                      ↥(center (SpecialLinearGroup n R)) ≃* ↥(rootsOfUnity x R))
                      (center_equiv_rootsOfUnity' (Classical.arbitrary n)) eq :
                    ↥(center (SpecialLinearGroup n R)) ≃* ↥(rootsOfUnity (max (Fintype.card n) 1) R)) :
                  (a : ↥(center (SpecialLinearGroup n R))) → ↥(rootsOfUnity (max (Fintype.card n) 1) R))
                A) :
            Rˣ) :
        R)
have neg : ∀ (c : ℕ) (eq : Fintype.card n = c),
  (↑(↑A : SpecialLinearGroup n R) : Matrix n n R) =
    (scalar n : (a : R) → Matrix n n R)
      (↑(↑(((Eq.rec (motive := fun (x : ℕ) (h : Fintype.card n = x) ↦
                      ↥(center (SpecialLinearGroup n R)) ≃* ↥(rootsOfUnity x R))
                      (center_equiv_rootsOfUnity' (Classical.arbitrary n)) eq :
                    ↥(center (SpecialLinearGroup n R)) ≃* ↥(rootsOfUnity c R)) :
                  (a : ↥(center (SpecialLinearGroup n R))) → ↥(rootsOfUnity c R))
                A) :
            Rˣ) :
        R)
Tactic: generalize max (Fintype.card n) 1 = c at eq
Cleared hypotheses: eq
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (goal)
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
A : ↥(center (SpecialLinearGroup n R))
h : ¬IsEmpty n
pf : Nonempty n
c : ℕ
eq : Fintype.card n = c
⊢ (↑(↑A : SpecialLinearGroup n R) : Matrix n n R) =
    (scalar n : (a : R) → Matrix n n R)
      (↑(↑(((Eq.rec (motive := fun (x : ℕ) (h : Fintype.card n = x) ↦
                      ↥(center (SpecialLinearGroup n R)) ≃* ↥(rootsOfUnity x R))
                      (center_equiv_rootsOfUnity' (Classical.arbitrary n)) eq :
                    ↥(center (SpecialLinearGroup n R)) ≃* ↥(rootsOfUnity c R)) :
                  (a : ↥(center (SpecialLinearGroup n R))) → ↥(rootsOfUnity c R))
                A) :
            Rˣ) :
        R)
have neg : (↑(↑A : SpecialLinearGroup n R) : Matrix n n R) =
  (scalar n : (a : R) → Matrix n n R)
    (↑(↑(((Eq.rec (motive := fun (x : ℕ) (h : Fintype.card n = x) ↦
                    ↥(center (SpecialLinearGroup n R)) ≃* ↥(rootsOfUnity x R))
                    (center_equiv_rootsOfUnity' (Classical.arbitrary n)) sorry :
                  ↥(center (SpecialLinearGroup n R)) ≃* ↥(rootsOfUnity (Fintype.card n) R)) :
                (a : ↥(center (SpecialLinearGroup n R))) → ↥(rootsOfUnity (Fintype.card n) R))
              A) :
          Rˣ) :
      R)
Tactic: subst eq
Cleared hypotheses: c, eq
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (goal)
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
A : ↥(center (SpecialLinearGroup n R))
h : ¬IsEmpty n
pf : Nonempty n
⊢ (↑(↑A : SpecialLinearGroup n R) : Matrix n n R) =
    (scalar n : (a : R) → Matrix n n R)
      (↑(↑(((Eq.rec (motive := fun (x : ℕ) (h : Fintype.card n = x) ↦
                      ↥(center (SpecialLinearGroup n R)) ≃* ↥(rootsOfUnity x R))
                      (center_equiv_rootsOfUnity' (Classical.arbitrary n)) ⋯ :
                    ↥(center (SpecialLinearGroup n R)) ≃* ↥(rootsOfUnity (Fintype.card n) R)) :
                  (a : ↥(center (SpecialLinearGroup n R))) → ↥(rootsOfUnity (Fintype.card n) R))
                A) :
            Rˣ) :
        R)
have neg : (↑(↑A : SpecialLinearGroup n R) : Matrix n n R) =
  (scalar n : (a : R) → Matrix n n R)
    (↑(↑(rootsOfUnity.mkOfPowEq
              ((↑(↑A : SpecialLinearGroup n R) : Matrix n n R) (Classical.arbitrary n) (Classical.arbitrary n)) sorry) :
          Rˣ) :
      R)
Tactic: rw [center_equiv_rootsOfUnity'_apply, rootsOfUnity.val_mkOfPowEq_coe,
    scalar_eq_coe_self_center]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (goal)
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
A : ↥(center (SpecialLinearGroup n R))
h : ¬IsEmpty n
pf : Nonempty n
neg :
  (↑(↑A : SpecialLinearGroup n R) : Matrix n n R) =
    (scalar n : (a : R) → Matrix n n R)
      (↑(↑(rootsOfUnity.mkOfPowEq
                ((↑(↑A : SpecialLinearGroup n R) : Matrix n n R) (Classical.arbitrary n) (Classical.arbitrary n)) ⋯) :
            Rˣ) :
        R)
⊢ (↑(↑A : SpecialLinearGroup n R) : Matrix n n R) =
    (scalar n : (a : R) → Matrix n n R)
      (↑(↑(((Eq.rec (motive := fun (x : ℕ) (h : Fintype.card n = x) ↦
                      ↥(center (SpecialLinearGroup n R)) ≃* ↥(rootsOfUnity x R))
                      (center_equiv_rootsOfUnity' (Classical.arbitrary n)) ⋯ :
                    ↥(center (SpecialLinearGroup n R)) ≃* ↥(rootsOfUnity (Fintype.card n) R)) :
                  (a : ↥(center (SpecialLinearGroup n R))) → ↥(rootsOfUnity (Fintype.card n) R))
                A) :
            Rˣ) :
        R)
have neg₁ : (↑(↑A : SpecialLinearGroup n R) : Matrix n n R) =
  (scalar n : (a : R) → Matrix n n R)
    ((↑(↑A : SpecialLinearGroup n R) : Matrix n n R) (Classical.arbitrary n) (Classical.arbitrary n))
Tactic: rw [center_equiv_rootsOfUnity'_apply, rootsOfUnity.val_mkOfPowEq_coe,
    scalar_eq_coe_self_center]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (goal)
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
A : ↥(center (SpecialLinearGroup n R))
h : ¬IsEmpty n
pf : Nonempty n
neg :
  (↑(↑A : SpecialLinearGroup n R) : Matrix n n R) =
    (scalar n : (a : R) → Matrix n n R)
      (↑(↑(rootsOfUnity.mkOfPowEq
                ((↑(↑A : SpecialLinearGroup n R) : Matrix n n R) (Classical.arbitrary n) (Classical.arbitrary n)) ⋯) :
            Rˣ) :
        R)
neg₁ :
  (↑(↑A : SpecialLinearGroup n R) : Matrix n n R) =
    (scalar n : (a : R) → Matrix n n R)
      ((↑(↑A : SpecialLinearGroup n R) : Matrix n n R) (Classical.arbitrary n) (Classical.arbitrary n))
⊢ (↑(↑A : SpecialLinearGroup n R) : Matrix n n R) =
    (scalar n : (a : R) → Matrix n n R)
      (↑(↑(((Eq.rec (motive := fun (x : ℕ) (h : Fintype.card n = x) ↦
                      ↥(center (SpecialLinearGroup n R)) ≃* ↥(rootsOfUnity x R))
                      (center_equiv_rootsOfUnity' (Classical.arbitrary n)) ⋯ :
                    ↥(center (SpecialLinearGroup n R)) ≃* ↥(rootsOfUnity (Fintype.card n) R)) :
                  (a : ↥(center (SpecialLinearGroup n R))) → ↥(rootsOfUnity (Fintype.card n) R))
                A) :
            Rˣ) :
        R)
have neg₂ : (↑(↑A : SpecialLinearGroup n R) : Matrix n n R) = (↑(↑A : SpecialLinearGroup n R) : Matrix n n R)
Tactic: rw [center_equiv_rootsOfUnity'_apply, rootsOfUnity.val_mkOfPowEq_coe,
    scalar_eq_coe_self_center]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (goal)
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
inst_3 : CharZero R
g h : SpecialLinearGroup n ℤ
⊢ Eq (α := SpecialLinearGroup n R)
      ((map (Int.castRingHom R) : (a : SpecialLinearGroup n ℤ) → SpecialLinearGroup n R) g : SpecialLinearGroup n R)
      ((map (Int.castRingHom R) : (a : SpecialLinearGroup n ℤ) → SpecialLinearGroup n R) h : SpecialLinearGroup n R) →
    g = h
have simp_rw : (∀ (i j : n), (↑g : Matrix n n ℤ) i j = (↑h : Matrix n n ℤ) i j) →
  ∀ (i j : n), (↑g : Matrix n n ℤ) i j = (↑h : Matrix n n ℤ) i j
Tactic: simp_rw [ext_iff, map_apply_coe, RingHom.mapMatrix_apply, Int.coe_castRingHom,
    Matrix.map_apply, Int.cast_inj]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (goal)
Goal:
R : Type v
inst : CommRing R
A : SL(2, R)
⊢ A⁻¹ =
    Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) R) ↦ A.det = 1)
      ![![(↑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 0]]
      ⋯
have a : ∀ (i j : Fin 2),
  (↑A⁻¹ : Matrix (Fin 2) (Fin 2) R) i j =
    (↑(Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) R) ↦ A.det = 1)
            ![![(↑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 0]]
            sorry) :
        Matrix (Fin 2) (Fin 2) R)
      i j
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (hypothesis)
Goal:
R : Type v
inst : CommRing R
A : SL(2, R)
i j : Fin 2
⊢ (↑A⁻¹ : Matrix (Fin 2) (Fin 2) R) i j =
    (↑(Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) R) ↦ A.det = 1)
            ![![(↑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 0]]
            ⋯) :
        Matrix (Fin 2) (Fin 2) R)
      i j
have this : (↑A : Matrix (Fin 2) (Fin 2) R).adjugate =
  !![(↑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 0]
Tactic: have := Matrix.adjugate_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 j : Fin 2
this :
  (↑A : Matrix (Fin 2) (Fin 2) R).adjugate =
    !![(↑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 0]
⊢ (↑A⁻¹ : Matrix (Fin 2) (Fin 2) R) i j =
    (↑(Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) R) ↦ A.det = 1)
            ![![(↑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 0]]
            ⋯) :
        Matrix (Fin 2) (Fin 2) R)
      i j
have a : !![(↑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 0]
    i j =
  (↑(Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) R) ↦ A.det = 1)
          ![![(↑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 0]]
          sorry) :
      Matrix (Fin 2) (Fin 2) R)
    i j
Tactic: rw [coe_inv, this]
-- 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] ⋯)
g : SL(2, R)
⊢ P g
have 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)
Tactic: obtain ⟨m, hm⟩ := g
Cleared hypotheses: g
-- 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
⊢ m 0 0 * m 1 1 - m 0 1 * m 1 0 = 1
have 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
Tactic: rwa [det_fin_two] at hm
Cleared hypotheses: hm
-- 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
⊢ P (Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) R) ↦ A.det = 1) m hm)
have 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] sorry)
Tactic: convert! h (m 0 0) (m 0 1) (m 1 0) (m 1 1) (by rwa [det_fin_two] at hm)
-- 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
⊢ 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] ⋯)
have 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] sorry) :
        Matrix (Fin 2) (Fin 2) R)
      i j
Tactic: ext i 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
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
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)) 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) ⟨0, sorry⟩) j
Tactic: fin_cases i
Cleared hypotheses: i