awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
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 :
  ((↑(↑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
⊢ (↑(↑(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)

Tactic:
simp only [rootsOfUnity.val_mkOfPowEq_coe, Subgroup.coe_mul, Units.val_mul]

Premises used: rootsOfUnity.val_mkOfPowEq_coe, Subgroup.coe_mul, Units.val_mul
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
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 :
  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)
⊢ ((↑(↑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:
rw [← scalar_eq_coe_self_center A i, ← scalar_eq_coe_self_center B i]

Premises used: Matrix.SpecialLinearGroup.scalar_eq_coe_self_center
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
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))
⊢ 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:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
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
rw : ↥⊥ ≃* ↥⊥
⊢ ↥(center (SpecialLinearGroup n R)) ≃* ↥(rootsOfUnity (max (Fintype.card n) 1) R)

Tactic:
rw [center_eq_bot_of_subsingleton, Fintype.card_eq_zero, max_eq_right_of_lt zero_lt_one,
      rootsOfUnity_one]

Premises used: max_eq_right_of_lt, Matrix.SpecialLinearGroup.center_eq_bot_of_subsingleton, rootsOfUnity_one, Fintype.card_eq_zero, zero_lt_one
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
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
⊢ ↥⊥ ≃* ↥⊥

Tactic:
exact MulEquiv.ofUnique

Premises used: MulEquiv.ofUnique
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
A : ↥(center (SpecialLinearGroup n R))
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 ⋯ (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)
⊢ (↑(↑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)

Tactic:
unfold center_equiv_rootsOfUnity Or.by_cases

Premises used: Matrix.SpecialLinearGroup.center_equiv_rootsOfUnity, Or.by_cases
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
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)
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)) ⋯ :
                          ↥(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)
⊢ (↑(↑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)

Tactic:
split_ifs with h
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
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)
      (↑(↑(((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)

Tactic:
subsingleton
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
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
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)) ⋯ :
                    ↥(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)
⊢ (↑(↑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)) ⋯ :
                        ↥(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:
dsimp only
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
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
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)
⊢ (↑(↑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)

Tactic:
generalize_proofs _ eq
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
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
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)
⊢ (↑(↑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 max (Fintype.card n) 1 = c at eq

Premises used: Fintype.card, Max.max, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
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
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)) ⋯ :
                    ↥(center (SpecialLinearGroup n R)) ≃* ↥(rootsOfUnity (Fintype.card n) R)) :
                  (a : ↥(center (SpecialLinearGroup n R))) → ↥(rootsOfUnity (Fintype.card n) R))
                A) :
            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)) eq :
                    ↥(center (SpecialLinearGroup n R)) ≃* ↥(rootsOfUnity c R)) :
                  (a : ↥(center (SpecialLinearGroup n R))) → ↥(rootsOfUnity c R))
                A) :
            Rˣ) :
        R)

Tactic:
subst eq
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
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))
neg₂ neg₃ : (↑(↑A : SpecialLinearGroup n R) : Matrix n n R) = (↑(↑A : SpecialLinearGroup n R) : Matrix n n 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)

Tactic:
rw [center_equiv_rootsOfUnity'_apply, rootsOfUnity.val_mkOfPowEq_coe,
    scalar_eq_coe_self_center]

Premises used: Matrix.SpecialLinearGroup.center_equiv_rootsOfUnity'_apply, rootsOfUnity.val_mkOfPowEq_coe, Matrix.SpecialLinearGroup.scalar_eq_coe_self_center
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
g : SpecialLinearGroup n ℤ
⊢ Eq (α := Matrix n n R)
    (↑((map (Int.castRingHom R) : (a : SpecialLinearGroup n ℤ) → SpecialLinearGroup n R) g) : Matrix n n R)
    ((↑g : Matrix n n ℤ).map (⇑(Int.castRingHom R) : (a : ℤ) → R))

Tactic:
map_apply_coe (Int.castRingHom R) g

Premises used: Matrix.SpecialLinearGroup.map_apply_coe, Int.castRingHom, Matrix.map
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
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 ℤ
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
⊢ 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

Tactic:
simp_rw [ext_iff, map_apply_coe, RingHom.mapMatrix_apply, Int.coe_castRingHom,
    Matrix.map_apply, Int.cast_inj]

Premises used: RingHom.mapMatrix_apply, Int.cast_inj, Int.coe_castRingHom, Matrix.SpecialLinearGroup.map_apply_coe, Matrix.map_apply, Matrix.SpecialLinearGroup.ext_iff
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
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 ℤ
tauto tauto₁ tauto₂ tauto₃ tauto₄ tauto₅ tauto₆ tauto₇ tauto₈ tauto₉ tauto₁₀ :
  (∀ (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
⊢ (∀ (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:
tauto
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
inst_3 : CharZero R
x y : SpecialLinearGroup n ℤ
⊢ Eq (α := SpecialLinearGroup n R)
      ((map (Int.castRingHom R) : (a : SpecialLinearGroup n ℤ) → SpecialLinearGroup n R) x : SpecialLinearGroup n R)
      ((map (Int.castRingHom R) : (a : SpecialLinearGroup n ℤ) → SpecialLinearGroup n R) y : SpecialLinearGroup n R) ↔
    x = y

Tactic:
map_intCast_injective.eq_iff

Premises used: Matrix.SpecialLinearGroup.map_intCast_injective, Function.Injective.eq_iff
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
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
inst_4 : Fact (Even (Fintype.card n))
g : SpecialLinearGroup n R
⊢ (-(↑g : Matrix n n R)).det = 1

Tactic:
simpa [(@Fact.out <| Even <| Fintype.card n).neg_one_pow, g.det_coe]
      using det_smul (↑ₘg) (-1)

Premises used: Matrix.SpecialLinearGroup.det_coe, Even.neg_one_pow, Fact.out
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
inst_3 : Fact (Even (Fintype.card n))
g : SpecialLinearGroup n R
⊢ (↑(-g) : Matrix n n R) = -(↑g : Matrix n n R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
inst_3 : Fact (Even (Fintype.card n))
g : 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) g : SpecialLinearGroup n R)

Tactic:
Subtype.ext <| (@RingHom.mapMatrix n _ _ _ _ _ _ (Int.castRingHom R)).map_neg ↑g

Premises used: RingHom.map_neg, Matrix.SpecialLinearGroup, RingHom.mapMatrix, Int.castRingHom, Subtype.val, Subtype.ext
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Goal:
R : Type v
inst : CommRing R
A : SL(2, R)
⊢ det
      ![![(↑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]] =
    1

Tactic:
simpa [-det_coe, Matrix.det_fin_two, mul_comm] using A.2

Premises used: Matrix.SpecialLinearGroup.det_coe, mul_comm, Matrix.det_fin_two, Subtype.property
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Goal:
R : Type v
inst : CommRing R
A : SL(2, R)
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]]
              ⋯) :
          Matrix (Fin 2) (Fin 2) R)
        i j
⊢ 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]]
      ⋯

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Goal:
R : Type v
inst : CommRing R
A : SL(2, R)
i j : Fin 2
⊢ (↑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
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
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 :
  !![(↑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]]
            ⋯) :
        Matrix (Fin 2) (Fin 2) R)
      i j
⊢ (↑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

Tactic:
rw [coe_inv, this]

Premises used: Matrix.SpecialLinearGroup.coe_inv
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
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) 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]]
            ⋯) :
        Matrix (Fin 2) (Fin 2) R)
      i j

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
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
P : SL(2, R) → Prop
a b c d : R
hdet rwa rwa₁ rwa₂ rwa₃ : a * d - b * c = 1
⊢ Eq.{v + 1} (α := R) (det (n := Fin 2) !![a, b; c, d]) 1

Tactic:
rwa [det_fin_two_of]

Premises used: Matrix.det_fin_two_of