awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
K : Type u_2
inst : Field K
g : GL (Fin 2) K
inst_1 : CharZero K
n : ℕ
hn : n ≠ 0
a : K
m : Matrix (Fin 2) (Fin 2) K
hg : (↑g : Matrix (Fin 2) (Fin 2) K) = m
hm0 : m ≠ 0
hmsq : HPow.hPow (β := ℕ) m 2 = 0
ha : a = 0
⊢ HPow.hPow (β := ℕ) (↑g : Matrix (Fin 2) (Fin 2) K) 2 = 0

Tactic:
rw [← hg] at hmsq
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
K : Type u_2
inst : Field K
g : GL (Fin 2) K
inst_1 : CharZero K
n : ℕ
hn : n ≠ 0
a : K
m : Matrix (Fin 2) (Fin 2) K
hg : (↑g : Matrix (Fin 2) (Fin 2) K) = m
hm0 : m ≠ 0
hmsq : HPow.hPow (β := ℕ) m 2 = 0
ha : a = 0
hmsq₁ : HPow.hPow (β := ℕ) (↑g : Matrix (Fin 2) (Fin 2) K) 2 = 0
⊢ a = 0

Tactic:
rw [← hg] at hmsq
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
K : Type u_2
inst : Field K
g : GL (Fin 2) K
inst_1 : CharZero K
n : ℕ
hn : n ≠ 0
a : K
m : Matrix (Fin 2) (Fin 2) K
hg : (↑g : Matrix (Fin 2) (Fin 2) K) = m
hm0 : m ≠ 0
hmsq : HPow.hPow (β := ℕ) (↑g : Matrix (Fin 2) (Fin 2) K) 2 = 0
ha : a = 0
refine_2 : (HPow.hPow (β := ℕ) (↑g : Matrix (Fin 2) (Fin 2) K) 2).det = 0
refine_2₁ : Eq.{u_2 + 1} (α := K) (Matrix.det (n := Fin 2) 0) 0
refine_2₂ refine_2₃ : Eq.{u_2 + 1} (α := K) 0 0
⊢ (↑(HPow.hPow (β := ℕ) g 2) : Matrix (Fin 2) (Fin 2) K).det = 0

Tactic:
rw [Units.val_pow_eq_pow_val, hmsq, det_zero ⟨0⟩]

Premises used: Matrix.det_zero, Nonempty.intro, Units.val_pow_eq_pow_val, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
K : Type u_2
inst : Field K
g : GL (Fin 2) K
hg : (↑g : Matrix (Fin 2) (Fin 2) K) 1 0 = 0
⊢ g.IsParabolic ↔
    (↑g : Matrix (Fin 2) (Fin 2) K) 0 0 = (↑g : Matrix (Fin 2) (Fin 2) K) 1 1 ∧ (↑g : Matrix (Fin 2) (Fin 2) K) 0 1 ≠ 0

Tactic:
Matrix.isParabolic_iff_of_upperTriangular hg

Premises used: Matrix.isParabolic_iff_of_upperTriangular
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
K : Type u_2
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
g : GL (Fin 2) K
h_det :
  Eq (α := Kˣ) ((det : (a : GL (Fin 2) K) → Kˣ) g : Kˣ) (1 : Kˣ) ∨
    Eq (α := Kˣ) ((det : (a : GL (Fin 2) K) → Kˣ) g : Kˣ) (-1 : Kˣ)
hg10 : (↑g : Matrix (Fin 2) (Fin 2) K) 1 0 = 0
rw :
  (↑g : Matrix (Fin 2) (Fin 2) K) 0 0 = (↑g : Matrix (Fin 2) (Fin 2) K) 1 1 ∧ (↑g : Matrix (Fin 2) (Fin 2) K) 0 1 ≠ 0 ↔
    (∃ (x : K), x ≠ 0 ∧ g = (upperRightHom : (a : K) → GL (Fin 2) K) x) ∨
      ∃ (x : K), x ≠ 0 ∧ g = -(upperRightHom : (a : K) → GL (Fin 2) K) x
⊢ g.IsParabolic ↔
    (∃ (x : K), x ≠ 0 ∧ g = (upperRightHom : (a : K) → GL (Fin 2) K) x) ∨
      ∃ (x : K), x ≠ 0 ∧ g = -(upperRightHom : (a : K) → GL (Fin 2) K) x

Tactic:
rw [isParabolic_iff_of_upperTriangular hg10]

Premises used: Matrix.GeneralLinearGroup.isParabolic_iff_of_upperTriangular
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
K : Type u_2
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
g : GL (Fin 2) K
h_det :
  Eq (α := Kˣ) ((det : (a : GL (Fin 2) K) → Kˣ) g : Kˣ) (1 : Kˣ) ∨
    Eq (α := Kˣ) ((det : (a : GL (Fin 2) K) → Kˣ) g : Kˣ) (-1 : Kˣ)
hg10 : (↑g : Matrix (Fin 2) (Fin 2) K) 1 0 = 0
mp :
  (↑g : Matrix (Fin 2) (Fin 2) K) 0 0 = (↑g : Matrix (Fin 2) (Fin 2) K) 1 1 ∧ (↑g : Matrix (Fin 2) (Fin 2) K) 0 1 ≠ 0 →
    (∃ (x : K), x ≠ 0 ∧ g = (upperRightHom : (a : K) → GL (Fin 2) K) x) ∨
      ∃ (x : K), x ≠ 0 ∧ g = -(upperRightHom : (a : K) → GL (Fin 2) K) x
mpr :
  ((∃ (x : K), x ≠ 0 ∧ g = (upperRightHom : (a : K) → GL (Fin 2) K) x) ∨
      ∃ (x : K), x ≠ 0 ∧ g = -(upperRightHom : (a : K) → GL (Fin 2) K) x) →
    (↑g : Matrix (Fin 2) (Fin 2) K) 0 0 = (↑g : Matrix (Fin 2) (Fin 2) K) 1 1 ∧ (↑g : Matrix (Fin 2) (Fin 2) K) 0 1 ≠ 0
⊢ (↑g : Matrix (Fin 2) (Fin 2) K) 0 0 = (↑g : Matrix (Fin 2) (Fin 2) K) 1 1 ∧ (↑g : Matrix (Fin 2) (Fin 2) K) 0 1 ≠ 0 ↔
    (∃ (x : K), x ≠ 0 ∧ g = (upperRightHom : (a : K) → GL (Fin 2) K) x) ∨
      ∃ (x : K), x ≠ 0 ∧ g = -(upperRightHom : (a : K) → GL (Fin 2) K) x

Tactic:
constructor
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
K : Type u_2
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
g : GL (Fin 2) K
h_det :
  Eq (α := Kˣ) ((det : (a : GL (Fin 2) K) → Kˣ) g : Kˣ) (1 : Kˣ) ∨
    Eq (α := Kˣ) ((det : (a : GL (Fin 2) K) → Kˣ) g : Kˣ) (-1 : Kˣ)
hg10 : (↑g : Matrix (Fin 2) (Fin 2) K) 1 0 = 0
hg00 : (↑g : Matrix (Fin 2) (Fin 2) K) 0 0 = (↑g : Matrix (Fin 2) (Fin 2) K) 1 1
hg01 : (↑g : Matrix (Fin 2) (Fin 2) K) 0 1 ≠ 0
rw :
  (↑g : Matrix (Fin 2) (Fin 2) K) 1 1 * (↑g : Matrix (Fin 2) (Fin 2) K) 1 1 - (↑g : Matrix (Fin 2) (Fin 2) K) 0 1 * 0 =
    HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) K) 1 1) 2
⊢ (↑((det : (a : GL (Fin 2) K) → Kˣ) g) : K) = HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) K) 1 1) 2

Tactic:
rw [val_det_apply, det_fin_two, hg10, hg00]

Premises used: Matrix.det_fin_two, Matrix.GeneralLinearGroup.val_det_apply
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
K : Type u_2
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
g : GL (Fin 2) K
h_det :
  Eq (α := Kˣ) ((det : (a : GL (Fin 2) K) → Kˣ) g : Kˣ) (1 : Kˣ) ∨
    Eq (α := Kˣ) ((det : (a : GL (Fin 2) K) → Kˣ) g : Kˣ) (-1 : Kˣ)
hg10 : (↑g : Matrix (Fin 2) (Fin 2) K) 1 0 = 0
hg00 : (↑g : Matrix (Fin 2) (Fin 2) K) 0 0 = (↑g : Matrix (Fin 2) (Fin 2) K) 1 1
hg01 : (↑g : Matrix (Fin 2) (Fin 2) K) 0 1 ≠ 0
⊢ (↑g : Matrix (Fin 2) (Fin 2) K) 1 1 * (↑g : Matrix (Fin 2) (Fin 2) K) 1 1 - (↑g : Matrix (Fin 2) (Fin 2) K) 0 1 * 0 =
    HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) K) 1 1) 2

Tactic:
ring
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
K : Type u_2
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
g : GL (Fin 2) K
h_det :
  Eq (α := Kˣ) ((det : (a : GL (Fin 2) K) → Kˣ) g : Kˣ) (1 : Kˣ) ∨
    Eq (α := Kˣ) ((det : (a : GL (Fin 2) K) → Kˣ) g : Kˣ) (-1 : Kˣ)
hg10 : (↑g : Matrix (Fin 2) (Fin 2) K) 1 0 = 0
hg00 : (↑g : Matrix (Fin 2) (Fin 2) K) 0 0 = (↑g : Matrix (Fin 2) (Fin 2) K) 1 1
hg01 : (↑g : Matrix (Fin 2) (Fin 2) K) 0 1 ≠ 0
⊢ (↑((det : (a : GL (Fin 2) K) → Kˣ) g) : K) = HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) K) 1 1) 2

Tactic:
have : g.det = g 1 1 ^ 2 := by rw [val_det_apply, det_fin_two, hg10, hg00]; ring
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
K : Type u_2
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
g : GL (Fin 2) K
h_det :
  Eq (α := Kˣ) ((det : (a : GL (Fin 2) K) → Kˣ) g : Kˣ) (1 : Kˣ) ∨
    Eq (α := Kˣ) ((det : (a : GL (Fin 2) K) → Kˣ) g : Kˣ) (-1 : Kˣ)
hg10 : (↑g : Matrix (Fin 2) (Fin 2) K) 1 0 = 0
hg00 : (↑g : Matrix (Fin 2) (Fin 2) K) 0 0 = (↑g : Matrix (Fin 2) (Fin 2) K) 1 1
hg01 : (↑g : Matrix (Fin 2) (Fin 2) K) 0 1 ≠ 0
this : (↑((det : (a : GL (Fin 2) K) → Kˣ) g) : K) = HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) K) 1 1) 2
⊢ HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) K) 1 1) 2 = 1 ∨
    HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) K) 1 1) 2 = -1

Tactic:
simp only [Units.ext_iff, Units.val_one, Units.val_neg, this] at h_det

Premises used: Units.ext_iff, Units.val_neg, Units.val_one
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
K : Type u_2
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
g : GL (Fin 2) K
hg10 : (↑g : Matrix (Fin 2) (Fin 2) K) 1 0 = 0
hg00 : (↑g : Matrix (Fin 2) (Fin 2) K) 0 0 = (↑g : Matrix (Fin 2) (Fin 2) K) 1 1
hg01 : (↑g : Matrix (Fin 2) (Fin 2) K) 0 1 ≠ 0
this : (↑((det : (a : GL (Fin 2) K) → Kˣ) g) : K) = HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) K) 1 1) 2
h_det :
  HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) K) 1 1) 2 = 1 ∨
    HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) K) 1 1) 2 = -1
⊢ HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) K) 1 1) 2 = 1

Tactic:
h_det.resolve_right (neg_one_lt_zero.trans_le <| sq_nonneg _).ne'

Premises used: LT.lt.ne', LT.lt.trans_le, sq_nonneg, neg_one_lt_zero, Or.resolve_right
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
K : Type u_2
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
g : GL (Fin 2) K
hg10 : (↑g : Matrix (Fin 2) (Fin 2) K) 1 0 = 0
hg00 : (↑g : Matrix (Fin 2) (Fin 2) K) 0 0 = (↑g : Matrix (Fin 2) (Fin 2) K) 1 1
hg01 : (↑g : Matrix (Fin 2) (Fin 2) K) 0 1 ≠ 0
this : (↑((det : (a : GL (Fin 2) K) → Kˣ) g) : K) = HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) K) 1 1) 2
h_det :
  HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) K) 1 1) 2 = 1 ∨
    HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) K) 1 1) 2 = -1
⊢ HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) K) 1 1) 2 = 1

Tactic:
exact h_det.resolve_right (neg_one_lt_zero.trans_le <| sq_nonneg _).ne'

Premises used: LT.lt.ne', LT.lt.trans_le, sq_nonneg, neg_one_lt_zero, Or.resolve_right
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
K : Type u_2
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
g : GL (Fin 2) K
h_det :
  Eq (α := Kˣ) ((det : (a : GL (Fin 2) K) → Kˣ) g : Kˣ) (1 : Kˣ) ∨
    Eq (α := Kˣ) ((det : (a : GL (Fin 2) K) → Kˣ) g : Kˣ) (-1 : Kˣ)
hg10 : (↑g : Matrix (Fin 2) (Fin 2) K) 1 0 = 0
hg00 : (↑g : Matrix (Fin 2) (Fin 2) K) 0 0 = (↑g : Matrix (Fin 2) (Fin 2) K) 1 1
hg01 : (↑g : Matrix (Fin 2) (Fin 2) K) 0 1 ≠ 0
⊢ HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) K) 1 1) 2 = 1

Tactic:
have : g 1 1 ^ 2 = 1 := by
      have : g.det = g 1 1 ^ 2 := by rw [val_det_apply, det_fin_two, hg10, hg00]; ring
      simp only [Units.ext_iff, Units.val_one, Units.val_neg, this] at h_det
      exact h_det.resolve_right (neg_one_lt_zero.trans_le <| sq_nonneg _).ne'
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
K : Type u_2
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
g : GL (Fin 2) K
h_det :
  Eq (α := Kˣ) ((det : (a : GL (Fin 2) K) → Kˣ) g : Kˣ) (1 : Kˣ) ∨
    Eq (α := Kˣ) ((det : (a : GL (Fin 2) K) → Kˣ) g : Kˣ) (-1 : Kˣ)
hg10 : (↑g : Matrix (Fin 2) (Fin 2) K) 1 0 = 0
hg00 : (↑g : Matrix (Fin 2) (Fin 2) K) 0 0 = (↑g : Matrix (Fin 2) (Fin 2) K) 1 1
hg01 : (↑g : Matrix (Fin 2) (Fin 2) K) 0 1 ≠ 0
this : HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) K) 1 1) 2 = 1
mp : (↑g : Matrix (Fin 2) (Fin 2) K) 1 1 = 1 → ∃ (x : K), x ≠ 0 ∧ g = (upperRightHom : (a : K) → GL (Fin 2) K) x
mp₁ : (↑g : Matrix (Fin 2) (Fin 2) K) 1 1 = -1 → ∃ (x : K), x ≠ 0 ∧ g = -(upperRightHom : (a : K) → GL (Fin 2) K) x
⊢ (∃ (x : K), x ≠ 0 ∧ g = (upperRightHom : (a : K) → GL (Fin 2) K) x) ∨
    ∃ (x : K), x ≠ 0 ∧ g = -(upperRightHom : (a : K) → GL (Fin 2) K) x

Tactic:
apply (sq_eq_one_iff.mp this).imp

Premises used: sq_eq_one_iff, Iff.mp, Or.imp
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
K : Type u_2
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
g : GL (Fin 2) K
h_det :
  Eq (α := Kˣ) ((det : (a : GL (Fin 2) K) → Kˣ) g : Kˣ) (1 : Kˣ) ∨
    Eq (α := Kˣ) ((det : (a : GL (Fin 2) K) → Kˣ) g : Kˣ) (-1 : Kˣ)
hg10 : (↑g : Matrix (Fin 2) (Fin 2) K) 1 0 = 0
hg00 : (↑g : Matrix (Fin 2) (Fin 2) K) 0 0 = (↑g : Matrix (Fin 2) (Fin 2) K) 1 1
hg01 : (↑g : Matrix (Fin 2) (Fin 2) K) 0 1 ≠ 0
this : HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) K) 1 1) 2 = 1
hg11 : (↑g : Matrix (Fin 2) (Fin 2) K) 1 1 = 1
mp :
  ∃ (x : K),
    x ≠ 0 ∧ (↑g : Matrix (Fin 2) (Fin 2) K) = (↑((upperRightHom : (a : K) → GL (Fin 2) K) x) : Matrix (Fin 2) (Fin 2) K)
⊢ ∃ (x : K), x ≠ 0 ∧ g = (upperRightHom : (a : K) → GL (Fin 2) K) x

Tactic:
simp only [Units.ext_iff]

Premises used: Units.ext_iff
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
K : Type u_2
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
g : GL (Fin 2) K
h_det :
  Eq (α := Kˣ) ((det : (a : GL (Fin 2) K) → Kˣ) g : Kˣ) (1 : Kˣ) ∨
    Eq (α := Kˣ) ((det : (a : GL (Fin 2) K) → Kˣ) g : Kˣ) (-1 : Kˣ)
hg10 : (↑g : Matrix (Fin 2) (Fin 2) K) 1 0 = 0
hg00 : (↑g : Matrix (Fin 2) (Fin 2) K) 0 0 = (↑g : Matrix (Fin 2) (Fin 2) K) 1 1
hg01 : (↑g : Matrix (Fin 2) (Fin 2) K) 0 1 ≠ 0
this : HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) K) 1 1) 2 = 1
hg11 : (↑g : Matrix (Fin 2) (Fin 2) K) 1 1 = -1
mp :
  ∃ (x : K),
    x ≠ 0 ∧
      (↑g : Matrix (Fin 2) (Fin 2) K) = (↑(-(upperRightHom : (a : K) → GL (Fin 2) K) x) : Matrix (Fin 2) (Fin 2) K)
⊢ ∃ (x : K), x ≠ 0 ∧ g = -(upperRightHom : (a : K) → GL (Fin 2) K) x

Tactic:
simp only [Units.ext_iff]

Premises used: Units.ext_iff
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
K : Type u_2
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
g : GL (Fin 2) K
h_det :
  Eq (α := Kˣ) ((det : (a : GL (Fin 2) K) → Kˣ) g : Kˣ) (1 : Kˣ) ∨
    Eq (α := Kˣ) ((det : (a : GL (Fin 2) K) → Kˣ) g : Kˣ) (-1 : Kˣ)
hg10 : (↑g : Matrix (Fin 2) (Fin 2) K) 1 0 = 0
hg00 : (↑g : Matrix (Fin 2) (Fin 2) K) 0 0 = (↑g : Matrix (Fin 2) (Fin 2) K) 1 1
hg01 : (↑g : Matrix (Fin 2) (Fin 2) K) 0 1 ≠ 0
this : HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) K) 1 1) 2 = 1
hg11 : (↑g : Matrix (Fin 2) (Fin 2) K) 1 1 = 1
⊢ ∃ (x : K),
    x ≠ 0 ∧ (↑g : Matrix (Fin 2) (Fin 2) K) = (↑((upperRightHom : (a : K) → GL (Fin 2) K) x) : Matrix (Fin 2) (Fin 2) K)

Tactic:
⟨g 0 1, hg01, ?_⟩

Premises used: Units.val, And.intro, Exists.intro, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
K : Type u_2
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
g : GL (Fin 2) K
h_det :
  Eq (α := Kˣ) ((det : (a : GL (Fin 2) K) → Kˣ) g : Kˣ) (1 : Kˣ) ∨
    Eq (α := Kˣ) ((det : (a : GL (Fin 2) K) → Kˣ) g : Kˣ) (-1 : Kˣ)
hg10 : (↑g : Matrix (Fin 2) (Fin 2) K) 1 0 = 0
hg00 : (↑g : Matrix (Fin 2) (Fin 2) K) 0 0 = (↑g : Matrix (Fin 2) (Fin 2) K) 1 1
hg01 : (↑g : Matrix (Fin 2) (Fin 2) K) 0 1 ≠ 0
this : HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) K) 1 1) 2 = 1
hg11 : (↑g : Matrix (Fin 2) (Fin 2) K) 1 1 = 1
mp :
  (↑g : Matrix (Fin 2) (Fin 2) K) =
    (↑((upperRightHom : (a : K) → GL (Fin 2) K) ((↑g : Matrix (Fin 2) (Fin 2) K) 0 1)) : Matrix (Fin 2) (Fin 2) K)
⊢ ∃ (x : K),
    x ≠ 0 ∧ (↑g : Matrix (Fin 2) (Fin 2) K) = (↑((upperRightHom : (a : K) → GL (Fin 2) K) x) : Matrix (Fin 2) (Fin 2) K)

Tactic:
refine ⟨g 0 1, hg01, ?_⟩
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
K : Type u_2
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
g : GL (Fin 2) K
h_det :
  Eq (α := Kˣ) ((det : (a : GL (Fin 2) K) → Kˣ) g : Kˣ) (1 : Kˣ) ∨
    Eq (α := Kˣ) ((det : (a : GL (Fin 2) K) → Kˣ) g : Kˣ) (-1 : Kˣ)
hg10 : (↑g : Matrix (Fin 2) (Fin 2) K) 1 0 = 0
hg00 : (↑g : Matrix (Fin 2) (Fin 2) K) 0 0 = (↑g : Matrix (Fin 2) (Fin 2) K) 1 1
hg01 : (↑g : Matrix (Fin 2) (Fin 2) K) 0 1 ≠ 0
this : HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) K) 1 1) 2 = 1
hg11 : (↑g : Matrix (Fin 2) (Fin 2) K) 1 1 = 1
mp :
  Eq (α := Matrix (Fin 2) (Fin 2) K)
    (!![(↑g : Matrix (Fin 2) (Fin 2) K) 0 0, (↑g : Matrix (Fin 2) (Fin 2) K) 0 1;
        (↑g : Matrix (Fin 2) (Fin 2) K) 1 0, (↑g : Matrix (Fin 2) (Fin 2) K) 1 1] :
      Matrix (Fin 2) (Fin 2) K)
    ((↑((upperRightHom : (a : K) → GL (Fin 2) K)
            (!![(↑g : Matrix (Fin 2) (Fin 2) K) 0 0, (↑g : Matrix (Fin 2) (Fin 2) K) 0 1;
                (↑g : Matrix (Fin 2) (Fin 2) K) 1 0, (↑g : Matrix (Fin 2) (Fin 2) K) 1 1]
              0 1)) :
        Matrix (Fin 2) (Fin 2) K) :
      Matrix (Fin 2) (Fin 2) K)
⊢ (↑g : Matrix (Fin 2) (Fin 2) K) =
    (↑((upperRightHom : (a : K) → GL (Fin 2) K) ((↑g : Matrix (Fin 2) (Fin 2) K) 0 1)) : Matrix (Fin 2) (Fin 2) K)

Tactic:
rw [g.val.eta_fin_two]

Premises used: Units.val, Matrix.eta_fin_two
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
K : Type u_2
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
g : GL (Fin 2) K
h_det :
  Eq (α := Kˣ) ((det : (a : GL (Fin 2) K) → Kˣ) g : Kˣ) (1 : Kˣ) ∨
    Eq (α := Kˣ) ((det : (a : GL (Fin 2) K) → Kˣ) g : Kˣ) (-1 : Kˣ)
hg10 : (↑g : Matrix (Fin 2) (Fin 2) K) 1 0 = 0
hg00 : (↑g : Matrix (Fin 2) (Fin 2) K) 0 0 = (↑g : Matrix (Fin 2) (Fin 2) K) 1 1
hg01 : (↑g : Matrix (Fin 2) (Fin 2) K) 0 1 ≠ 0
this : HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) K) 1 1) 2 = 1
hg11 : (↑g : Matrix (Fin 2) (Fin 2) K) 1 1 = 1
⊢ Eq (α := Matrix (Fin 2) (Fin 2) K)
    (!![(↑g : Matrix (Fin 2) (Fin 2) K) 0 0, (↑g : Matrix (Fin 2) (Fin 2) K) 0 1;
        (↑g : Matrix (Fin 2) (Fin 2) K) 1 0, (↑g : Matrix (Fin 2) (Fin 2) K) 1 1] :
      Matrix (Fin 2) (Fin 2) K)
    ((↑((upperRightHom : (a : K) → GL (Fin 2) K)
            (!![(↑g : Matrix (Fin 2) (Fin 2) K) 0 0, (↑g : Matrix (Fin 2) (Fin 2) K) 0 1;
                (↑g : Matrix (Fin 2) (Fin 2) K) 1 0, (↑g : Matrix (Fin 2) (Fin 2) K) 1 1]
              0 1)) :
        Matrix (Fin 2) (Fin 2) K) :
      Matrix (Fin 2) (Fin 2) K)

Tactic:
simp_all
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
K : Type u_2
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
g : GL (Fin 2) K
h_det :
  Eq (α := Kˣ) ((det : (a : GL (Fin 2) K) → Kˣ) g : Kˣ) (1 : Kˣ) ∨
    Eq (α := Kˣ) ((det : (a : GL (Fin 2) K) → Kˣ) g : Kˣ) (-1 : Kˣ)
hg10 : (↑g : Matrix (Fin 2) (Fin 2) K) 1 0 = 0
hg00 : (↑g : Matrix (Fin 2) (Fin 2) K) 0 0 = (↑g : Matrix (Fin 2) (Fin 2) K) 1 1
hg01 : (↑g : Matrix (Fin 2) (Fin 2) K) 0 1 ≠ 0
this : HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) K) 1 1) 2 = 1
hg11 : (↑g : Matrix (Fin 2) (Fin 2) K) 1 1 = -1
⊢ ∃ (x : K),
    x ≠ 0 ∧
      (↑g : Matrix (Fin 2) (Fin 2) K) = (↑(-(upperRightHom : (a : K) → GL (Fin 2) K) x) : Matrix (Fin 2) (Fin 2) K)

Tactic:
⟨-g 0 1, neg_eq_zero.not.mpr hg01, ?_⟩

Premises used: Iff.mpr, Units.val, neg_eq_zero, Iff.not, And.intro, Exists.intro, OfNat.ofNat, Neg.neg
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
K : Type u_2
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
g : GL (Fin 2) K
h_det :
  Eq (α := Kˣ) ((det : (a : GL (Fin 2) K) → Kˣ) g : Kˣ) (1 : Kˣ) ∨
    Eq (α := Kˣ) ((det : (a : GL (Fin 2) K) → Kˣ) g : Kˣ) (-1 : Kˣ)
hg10 : (↑g : Matrix (Fin 2) (Fin 2) K) 1 0 = 0
hg00 : (↑g : Matrix (Fin 2) (Fin 2) K) 0 0 = (↑g : Matrix (Fin 2) (Fin 2) K) 1 1
hg01 : (↑g : Matrix (Fin 2) (Fin 2) K) 0 1 ≠ 0
this : HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) K) 1 1) 2 = 1
hg11 : (↑g : Matrix (Fin 2) (Fin 2) K) 1 1 = -1
mp :
  (↑g : Matrix (Fin 2) (Fin 2) K) =
    (↑(-(upperRightHom : (a : K) → GL (Fin 2) K) (-(↑g : Matrix (Fin 2) (Fin 2) K) 0 1)) : Matrix (Fin 2) (Fin 2) K)
⊢ ∃ (x : K),
    x ≠ 0 ∧
      (↑g : Matrix (Fin 2) (Fin 2) K) = (↑(-(upperRightHom : (a : K) → GL (Fin 2) K) x) : Matrix (Fin 2) (Fin 2) K)

Tactic:
refine ⟨-g 0 1, neg_eq_zero.not.mpr hg01, ?_⟩
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
K : Type u_2
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
g : GL (Fin 2) K
h_det :
  Eq (α := Kˣ) ((det : (a : GL (Fin 2) K) → Kˣ) g : Kˣ) (1 : Kˣ) ∨
    Eq (α := Kˣ) ((det : (a : GL (Fin 2) K) → Kˣ) g : Kˣ) (-1 : Kˣ)
hg10 : (↑g : Matrix (Fin 2) (Fin 2) K) 1 0 = 0
hg00 : (↑g : Matrix (Fin 2) (Fin 2) K) 0 0 = (↑g : Matrix (Fin 2) (Fin 2) K) 1 1
hg01 : (↑g : Matrix (Fin 2) (Fin 2) K) 0 1 ≠ 0
this : HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) K) 1 1) 2 = 1
hg11 : (↑g : Matrix (Fin 2) (Fin 2) K) 1 1 = -1
mp :
  Eq (α := Matrix (Fin 2) (Fin 2) K)
    (!![(↑g : Matrix (Fin 2) (Fin 2) K) 0 0, (↑g : Matrix (Fin 2) (Fin 2) K) 0 1;
        (↑g : Matrix (Fin 2) (Fin 2) K) 1 0, (↑g : Matrix (Fin 2) (Fin 2) K) 1 1] :
      Matrix (Fin 2) (Fin 2) K)
    ((↑(-(upperRightHom : (a : K) → GL (Fin 2) K)
              (-!![(↑g : Matrix (Fin 2) (Fin 2) K) 0 0, (↑g : Matrix (Fin 2) (Fin 2) K) 0 1;
                    (↑g : Matrix (Fin 2) (Fin 2) K) 1 0, (↑g : Matrix (Fin 2) (Fin 2) K) 1 1]
                  0 1)) :
        Matrix (Fin 2) (Fin 2) K) :
      Matrix (Fin 2) (Fin 2) K)
⊢ (↑g : Matrix (Fin 2) (Fin 2) K) =
    (↑(-(upperRightHom : (a : K) → GL (Fin 2) K) (-(↑g : Matrix (Fin 2) (Fin 2) K) 0 1)) : Matrix (Fin 2) (Fin 2) K)

Tactic:
rw [g.val.eta_fin_two]

Premises used: Units.val, Matrix.eta_fin_two
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
K : Type u_2
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
g : GL (Fin 2) K
h_det :
  Eq (α := Kˣ) ((det : (a : GL (Fin 2) K) → Kˣ) g : Kˣ) (1 : Kˣ) ∨
    Eq (α := Kˣ) ((det : (a : GL (Fin 2) K) → Kˣ) g : Kˣ) (-1 : Kˣ)
hg10 : (↑g : Matrix (Fin 2) (Fin 2) K) 1 0 = 0
hg00 : (↑g : Matrix (Fin 2) (Fin 2) K) 0 0 = (↑g : Matrix (Fin 2) (Fin 2) K) 1 1
hg01 : (↑g : Matrix (Fin 2) (Fin 2) K) 0 1 ≠ 0
this : HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) K) 1 1) 2 = 1
hg11 : (↑g : Matrix (Fin 2) (Fin 2) K) 1 1 = -1
⊢ Eq (α := Matrix (Fin 2) (Fin 2) K)
    (!![(↑g : Matrix (Fin 2) (Fin 2) K) 0 0, (↑g : Matrix (Fin 2) (Fin 2) K) 0 1;
        (↑g : Matrix (Fin 2) (Fin 2) K) 1 0, (↑g : Matrix (Fin 2) (Fin 2) K) 1 1] :
      Matrix (Fin 2) (Fin 2) K)
    ((↑(-(upperRightHom : (a : K) → GL (Fin 2) K)
              (-!![(↑g : Matrix (Fin 2) (Fin 2) K) 0 0, (↑g : Matrix (Fin 2) (Fin 2) K) 0 1;
                    (↑g : Matrix (Fin 2) (Fin 2) K) 1 0, (↑g : Matrix (Fin 2) (Fin 2) K) 1 1]
                  0 1)) :
        Matrix (Fin 2) (Fin 2) K) :
      Matrix (Fin 2) (Fin 2) K)

Tactic:
simp_all
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
K : Type u_2
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
x : K
hx : x ≠ 0
h_det :
  Eq (α := Kˣ) ((det : (a : GL (Fin 2) K) → Kˣ) ((upperRightHom : (a : K) → GL (Fin 2) K) x) : Kˣ) (1 : Kˣ) ∨
    Eq (α := Kˣ) ((det : (a : GL (Fin 2) K) → Kˣ) ((upperRightHom : (a : K) → GL (Fin 2) K) x) : Kˣ) (-1 : Kˣ)
hg10 : Eq.{u_2 + 1} (α := K) ((↑((upperRightHom : (a : K) → GL (Fin 2) K) x) : Matrix (Fin 2) (Fin 2) K) 1 0) 0
⊢ Eq.{u_2 + 1} (α := K) ((↑((upperRightHom : (a : K) → GL (Fin 2) K) x) : Matrix (Fin 2) (Fin 2) K) 0 0)
      ((↑((upperRightHom : (a : K) → GL (Fin 2) K) x) : Matrix (Fin 2) (Fin 2) K) 1 1) ∧
    Ne.{u_2 + 1} (α := K) ((↑((upperRightHom : (a : K) → GL (Fin 2) K) x) : Matrix (Fin 2) (Fin 2) K) 0 1) 0

Tactic:
simpa using hx
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
K : Type u_2
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
x : K
hx : x ≠ 0
h_det :
  Eq (α := Kˣ) ((det : (a : GL (Fin 2) K) → Kˣ) (-(upperRightHom : (a : K) → GL (Fin 2) K) x) : Kˣ) (1 : Kˣ) ∨
    Eq (α := Kˣ) ((det : (a : GL (Fin 2) K) → Kˣ) (-(upperRightHom : (a : K) → GL (Fin 2) K) x) : Kˣ) (-1 : Kˣ)
hg10 : Eq.{u_2 + 1} (α := K) ((↑(-(upperRightHom : (a : K) → GL (Fin 2) K) x) : Matrix (Fin 2) (Fin 2) K) 1 0) 0
⊢ Eq.{u_2 + 1} (α := K) ((↑(-(upperRightHom : (a : K) → GL (Fin 2) K) x) : Matrix (Fin 2) (Fin 2) K) 0 0)
      ((↑(-(upperRightHom : (a : K) → GL (Fin 2) K) x) : Matrix (Fin 2) (Fin 2) K) 1 1) ∧
    Ne.{u_2 + 1} (α := K) ((↑(-(upperRightHom : (a : K) → GL (Fin 2) K) x) : Matrix (Fin 2) (Fin 2) K) 0 1) 0

Tactic:
simpa using hx
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Projective
Goal:
n : Type u_1
R : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing R
⊢ Function.Surjective (α := GL n R) (β := PGL(n, R)) (⇑mk : (a : GL n R) → PGL(n, R))

Tactic:
Quotient.mk_surjective

Premises used: Matrix.ProjGenLinGroup, Quotient.mk_surjective
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Projective
Goal:
n : Type u_1
R : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing R
⊢ Eq (α := Subgroup (GL n R)) (MonoidHom.ker mk) (Subgroup.center (GL n R))

Tactic:
QuotientGroup.ker_mk' _

Premises used: Matrix.ProjGenLinGroup, Matrix.ProjGenLinGroup.mk, QuotientGroup.ker_mk'
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Projective
Goal:
n : Type u_1
R : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing R
g : GL n R
rw :
  Membership.mem (γ := Subgroup (GL n R)) (MonoidHom.ker mk) g ↔
    Membership.mem (γ := Subgroup (GL n R)) (Subgroup.center (GL n R)) g
rw₁ rw₂ :
  Membership.mem (γ := Subgroup (GL n R)) (Subgroup.center (GL n R)) g ↔
    Membership.mem (γ := Subgroup (GL n R)) (Subgroup.center (GL n R)) g
⊢ Eq (α := PGL(n, R)) ((mk : (a : GL n R) → PGL(n, R)) g : PGL(n, R)) (1 : PGL(n, R)) ↔
    Membership.mem (γ := Subgroup (GL n R)) (Subgroup.center (GL n R)) g

Tactic:
rw [← MonoidHom.mem_ker, ker_mk]

Premises used: Matrix.ProjGenLinGroup.ker_mk, MonoidHom.mem_ker