awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
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 : Algebra R S
T : Type u_2
inst_5 : CommRing T
inst_6 : Algebra R T
inst_7 : Algebra S T
inst_8 : IsScalarTower R S T
g : SpecialLinearGroup n R
i j : n
⊢ Eq.{u_2 + 1} (α := T)
    ((↑((GeneralLinearGroup.map (algebraMap S T) : (a : GL n S) → GL n T)
            ((mapGL S : (a : SpecialLinearGroup n R) → GL n S) g)) :
        Matrix n n T)
      i j)
    ((↑((mapGL T : (a : SpecialLinearGroup n R) → GL n T) g) : Matrix n n T) i j)

Tactic:
simp [IsScalarTower.algebraMap_apply R S T]

Premises used: IsScalarTower.algebraMap_apply
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
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 : Algebra R S
g : SpecialLinearGroup n R
⊢ Eq.{u_1 + 1} (α := Sˣ)
    ((GeneralLinearGroup.det : (a : GL n S) → Sˣ) ((mapGL S : (a : SpecialLinearGroup n R) → GL n S) g) : Sˣ) (1 : Sˣ)

Tactic:
simp [mapGL]

Premises used: Matrix.SpecialLinearGroup.mapGL
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
Goal:
n : Type u
R : Type v
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing R
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
A : GL n R
⊢ Membership.mem (γ := Subgroup (GL n R)) (GLPos n R) A ↔
    LT.lt.{v} (α := R) 0 (↑((GeneralLinearGroup.det : (a : GL n R) → Rˣ) A) : R)

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.preimage
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
Goal:
n : Type u
R : Type v
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing R
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
A : ↥(GLPos n R)
⊢ (↑(↑A : GL n R) : Matrix n n R).det ≠ 0

Tactic:
ne_of_gt A.prop

Premises used: ne_of_gt, Subtype.prop
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
Goal:
n : Type u
R : Type v
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing R
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
inst_5 : Fact (Even (Fintype.card n))
g : ↥(GLPos n R)
rw : 0 < (↑(↑g : GL n R) : Matrix n n R).det
⊢ Membership.mem (γ := Subgroup (GL n R)) (GLPos n R) (-(↑g : GL n R))

Tactic:
rw [mem_glpos, GeneralLinearGroup.val_det_apply, Units.val_neg, det_neg,
        (Fact.out (p := Even <| Fintype.card n)).neg_one_pow, one_mul]

Premises used: Even.neg_one_pow, Units.val_neg, Matrix.det_neg, Matrix.mem_glpos, one_mul, Fact.out, Matrix.GeneralLinearGroup.val_det_apply
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
Goal:
n : Type u
R : Type v
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing R
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
inst_5 : Fact (Even (Fintype.card n))
g : ↥(GLPos n R)
⊢ 0 < (↑(↑g : GL n R) : Matrix n n R).det

Tactic:
g.prop

Premises used: Set.Mem, setOf, Set.preimage, Subtype.prop, Matrix.det
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
Goal:
n : Type u
R : Type v
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing R
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
inst_5 : Fact (Even (Fintype.card n))
g : ↥(GLPos n R)
⊢ 0 < (↑(↑g : GL n R) : Matrix n n R).det

Tactic:
exact g.prop

Premises used: Subtype.prop
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
Goal:
n : Type u
R : Type v
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing R
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
inst_5 : Fact (Even (Fintype.card n))
g : ↥(GLPos n R)
⊢ (↑(-g) : GL n R) = -(↑g : GL n R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
Goal:
n : Type u
R : Type v
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing R
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
inst_5 : Fact (Even (Fintype.card n))
g : ↥(GLPos n R)
⊢ (↑(↑(-g) : GL n R) : Matrix n n R) = -(↑(↑g : GL n R) : Matrix n n R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
Goal:
n : Type u
R : Type v
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing R
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
inst_5 : Fact (Even (Fintype.card n))
g : ↥(GLPos n R)
i j : n
⊢ (↑(↑(-g) : GL n R) : Matrix n n R) i j = -(↑(↑g : GL n R) : Matrix n n R) i j

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
⊢ Function.Injective (α := SpecialLinearGroup n R) (β := ↥(GLPos n R))
    (⇑toGLPos : (a : SpecialLinearGroup n R) → ↥(GLPos n R))

Tactic:
Function.Injective.of_comp
    (f := fun (A : GLPos n R) ↦ ((A : GL n R) : Matrix n n R))
    Subtype.coe_injective

Premises used: Subtype.coe_injective, Function.Injective.of_comp
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
g : SpecialLinearGroup n R
⊢ (↑(↑((toGLPos : (a : SpecialLinearGroup n R) → ↥(GLPos n R)) g) : GL n R) : Matrix n n R) = (↑g : Matrix n n R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
g : SpecialLinearGroup n R
⊢ Eq.{v + 1} (α := Rˣ)
    ((GeneralLinearGroup.det : (a : GL n R) → Rˣ)
      (↑((toGLPos : (a : SpecialLinearGroup n R) → ↥(GLPos n R)) g) : GL n R))
    1

Tactic:
Units.ext g.prop

Premises used: Units.ext, Subtype.prop
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
inst_5 : Fact (Even (Fintype.card n))
g : SpecialLinearGroup n R
⊢ Eq (α := ↥(GLPos n R)) ((toGLPos : (a : SpecialLinearGroup n R) → ↥(GLPos n R)) (-g) : ↥(GLPos n R))
    (-(toGLPos : (a : SpecialLinearGroup n R) → ↥(GLPos n R)) g : ↥(GLPos n R))

Tactic:
Subtype.ext <| Units.ext rfl

Premises used: Units.ext, rfl, Subtype.ext
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
R : Type u_1
inst : CommRing R
m : Matrix (Fin 2) (Fin 2) R
g : GL (Fin 2) R
simp_rw :
  (↑g : Matrix (Fin 2) (Fin 2) R) * m * (↑g : Matrix (Fin 2) (Fin 2) R)⁻¹ ∉
        Set.range (ι := R) (⇑(scalar (Fin 2)) : (a : R) → Matrix (Fin 2) (Fin 2) R) ∧
      ((↑g : Matrix (Fin 2) (Fin 2) R) * m * (↑g : Matrix (Fin 2) (Fin 2) R)⁻¹).discr = 0 ↔
    m ∉ Set.range (ι := R) (⇑(scalar (Fin 2)) : (a : R) → Matrix (Fin 2) (Fin 2) R) ∧ m.discr = 0
simp_rw₁ :
  (↑g : Matrix (Fin 2) (Fin 2) R) * m * (↑g : Matrix (Fin 2) (Fin 2) R)⁻¹ ∉
        Set.range (ι := R) (⇑(scalar (Fin 2)) : (a : R) → Matrix (Fin 2) (Fin 2) R) ∧
      m.discr = 0 ↔
    m ∉ Set.range (ι := R) (⇑(scalar (Fin 2)) : (a : R) → Matrix (Fin 2) (Fin 2) R) ∧ m.discr = 0
simp_rw₂ :
  (¬∃ (y : R),
          (scalar (Fin 2) : (a : R) → Matrix (Fin 2) (Fin 2) R) y =
            (↑g : Matrix (Fin 2) (Fin 2) R) * m * (↑g : Matrix (Fin 2) (Fin 2) R)⁻¹) ∧
      m.discr = 0 ↔
    (¬∃ (y : R), (scalar (Fin 2) : (a : R) → Matrix (Fin 2) (Fin 2) R) y = m) ∧ m.discr = 0
simp_rw₃ :
  (¬∃ (y : R),
          (scalar (Fin 2) : (a : R) → Matrix (Fin 2) (Fin 2) R) y =
            (↑g : Matrix (Fin 2) (Fin 2) R) * m * (↑g⁻¹ : Matrix (Fin 2) (Fin 2) R)) ∧
      m.discr = 0 ↔
    (¬∃ (y : R), (scalar (Fin 2) : (a : R) → Matrix (Fin 2) (Fin 2) R) y = m) ∧ m.discr = 0
simp_rw₄ :
  (¬∃ (y : R),
          HMul.hMul (α := Matrix (Fin 2) (Fin 2) R)
              ((scalar (Fin 2) : (a : R) → Matrix (Fin 2) (Fin 2) R) y : Matrix (Fin 2) (Fin 2) R)
              (↑g : Matrix (Fin 2) (Fin 2) R) =
            (↑g : Matrix (Fin 2) (Fin 2) R) * m) ∧
      m.discr = 0 ↔
    (¬∃ (y : R), (scalar (Fin 2) : (a : R) → Matrix (Fin 2) (Fin 2) R) y = m) ∧ m.discr = 0
simp_rw₅ :
  (¬∃ (y : R), (diagonal fun (x : Fin 2) ↦ y) * (↑g : Matrix (Fin 2) (Fin 2) R) = (↑g : Matrix (Fin 2) (Fin 2) R) * m) ∧
      m.discr = 0 ↔
    (¬∃ (y : R), (diagonal fun (x : Fin 2) ↦ y) = m) ∧ m.discr = 0
simp_rw₆ :
  (¬∃ (y : R), y • (↑g : Matrix (Fin 2) (Fin 2) R) = (↑g : Matrix (Fin 2) (Fin 2) R) * m) ∧ m.discr = 0 ↔
    (¬∃ (y : R), (diagonal fun (x : Fin 2) ↦ y) = m) ∧ m.discr = 0
simp_rw₇ :
  (¬∃ (y : R), ((↑g : Matrix (Fin 2) (Fin 2) R) * diagonal fun (x : Fin 2) ↦ y) = (↑g : Matrix (Fin 2) (Fin 2) R) * m) ∧
      m.discr = 0 ↔
    (¬∃ (y : R), (diagonal fun (x : Fin 2) ↦ y) = m) ∧ m.discr = 0
⊢ ((↑g : Matrix (Fin 2) (Fin 2) R) * m * (↑g : Matrix (Fin 2) (Fin 2) R)⁻¹).IsParabolic ↔ m.IsParabolic

Tactic:
simp_rw [IsParabolic, discr_conj, Set.mem_range, ← Matrix.coe_units_inv,
    Units.eq_mul_inv_iff_mul_eq, scalar_apply, ← smul_eq_diagonal_mul, smul_eq_mul_diagonal,
    Units.mul_right_inj]

Premises used: Matrix.discr_conj, Set.mem_range, Matrix.coe_units_inv, Matrix.IsParabolic, Matrix.smul_eq_mul_diagonal, Units.eq_mul_inv_iff_mul_eq, Units.mul_right_inj, Matrix.scalar_apply, Matrix.smul_eq_diagonal_mul
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
R : Type u_1
inst : CommRing R
m : Matrix (Fin 2) (Fin 2) R
g : GL (Fin 2) R
⊢ ((↑g : Matrix (Fin 2) (Fin 2) R)⁻¹ * m * (↑g : Matrix (Fin 2) (Fin 2) R)).IsParabolic ↔ m.IsParabolic

Tactic:
simpa using isParabolic_conj_iff g⁻¹

Premises used: Matrix.isParabolic_conj_iff, Inv.inv
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
R : Type u_1
inst : CommRing R
m : Matrix (Fin 2) (Fin 2) R
h : m.IsParabolic
left : -m ∉ Set.range (ι := R) (⇑(scalar (Fin 2)) : (a : R) → Matrix (Fin 2) (Fin 2) R)
right : (-m).discr = 0
⊢ (-m).IsParabolic

Tactic:
constructor
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
R : Type u_1
inst : CommRing R
m : Matrix (Fin 2) (Fin 2) R
h : m.IsParabolic
left : m ∉ RingHom.range (R := R) (scalar (Fin 2))
⊢ -m ∉ Set.range (ι := R) (⇑(scalar (Fin 2)) : (a : R) → Matrix (Fin 2) (Fin 2) R)

Tactic:
rw [← RingHom.coe_range, SetLike.mem_coe, neg_mem_iff]

Premises used: neg_mem_iff, SetLike.mem_coe, RingHom.coe_range
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
R : Type u_1
inst : CommRing R
m : Matrix (Fin 2) (Fin 2) R
h : m.IsParabolic
⊢ m ∉ RingHom.range (R := R) (scalar (Fin 2))

Tactic:
h.1

Premises used: Set.Mem, setOf, And.left, Set.range
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
R : Type u_1
inst : CommRing R
m : Matrix (Fin 2) (Fin 2) R
h : m.IsParabolic
⊢ m ∉ RingHom.range (R := R) (scalar (Fin 2))

Tactic:
exact h.1

Premises used: And.left
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
R : Type u_1
inst : CommRing R
m : Matrix (Fin 2) (Fin 2) R
h : m.IsParabolic
⊢ (-m).discr = 0

Tactic:
simpa [discr_fin_two, det_neg] using h.2

Premises used: Matrix.det_neg, And.right, Matrix.discr_fin_two
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
R : Type u_1
inst : CommRing R
m : Matrix (Fin 2) (Fin 2) R
h : (-m).IsParabolic
⊢ m.IsParabolic

Tactic:
simpa using h.neg

Premises used: Matrix.IsParabolic.neg
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
R : Type u_1
inst : CommRing R
m : Matrix (Fin 2) (Fin 2) R
⊢ (-m).IsParabolic ↔ m.IsParabolic

Tactic:
⟨.of_neg, .neg⟩

Premises used: Matrix.IsParabolic.neg, Matrix.IsParabolic.of_neg, Iff.intro
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
R : Type u_1
inst : CommRing R
m : Matrix (Fin 2) (Fin 2) R
inst_1 : IsReduced R
hm : m 1 0 = 0
this : m.discr = HPow.hPow (β := ℕ) (m 0 0 - m 1 1) 2
rw : HPow.hPow (β := ℕ) (m 0 0 - m 1 1) 2 = 0 ↔ m 0 0 = m 1 1
rw₁ : m 0 0 - m 1 1 = 0 ↔ m 0 0 = m 1 1
rw₂ rw₃ : m 0 0 = m 1 1 ↔ m 0 0 = m 1 1
⊢ m.discr = 0 ↔ m 0 0 = m 1 1

Tactic:
rw [this, pow_eq_zero_iff two_ne_zero, sub_eq_zero]

Premises used: pow_eq_zero_iff, sub_eq_zero, two_ne_zero
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
R : Type u_1
inst : CommRing R
m : Matrix (Fin 2) (Fin 2) R
inst_1 : IsReduced R
hm : m 1 0 = 0
suffices : m.discr = HPow.hPow (β := ℕ) (m 0 0 - m 1 1) 2
⊢ m.discr = 0 ↔ m 0 0 = m 1 1

Tactic:
suffices m.discr = (m 0 0 - m 1 1) ^ 2 by
      rw [this, pow_eq_zero_iff two_ne_zero, sub_eq_zero]
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
R : Type u_1
inst : CommRing R
m : Matrix (Fin 2) (Fin 2) R
inst_1 : IsReduced R
hm : m 1 0 = 0
⊢ m.discr = HPow.hPow (β := ℕ) (m 0 0 - m 1 1) 2

Tactic:
grind [discr_fin_two, trace_fin_two, det_fin_two]

Premises used: Matrix.trace_fin_two, Matrix.det_fin_two, Matrix.discr_fin_two
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
R : Type u_1
inst : CommRing R
m : Matrix (Fin 2) (Fin 2) R
inst_1 : IsReduced R
hm : m 1 0 = 0
⊢ m.discr = 0 ↔ m 0 0 = m 1 1

Tactic:
have aux : m.discr = 0 ↔ m 0 0 = m 1 1 := by
    suffices m.discr = (m 0 0 - m 1 1) ^ 2 by
      rw [this, pow_eq_zero_iff two_ne_zero, sub_eq_zero]
    grind [discr_fin_two, trace_fin_two, det_fin_two]
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
R : Type u_1
inst : CommRing R
m : Matrix (Fin 2) (Fin 2) R
inst_1 : IsReduced R
hm : m 1 0 = 0
aux : m.discr = 0 ↔ m 0 0 = m 1 1
h : m 0 0 = m 1 1
mp :
  Membership.mem (γ := Set (Matrix (Fin 2) (Fin 2) R))
      (Set.range (ι := R) (⇑(scalar (Fin 2)) : (a : R) → Matrix (Fin 2) (Fin 2) R)) m →
    m 0 1 = 0
mpr :
  m 0 1 = 0 →
    Membership.mem (γ := Set (Matrix (Fin 2) (Fin 2) R))
      (Set.range (ι := R) (⇑(scalar (Fin 2)) : (a : R) → Matrix (Fin 2) (Fin 2) R)) m
⊢ Membership.mem (γ := Set (Matrix (Fin 2) (Fin 2) R))
      (Set.range (ι := R) (⇑(scalar (Fin 2)) : (a : R) → Matrix (Fin 2) (Fin 2) R)) m ↔
    m 0 1 = 0

Tactic:
constructor
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsReduced R
a : R
hm : Eq (α := R) ((scalar (Fin 2) : (a : R) → Matrix (Fin 2) (Fin 2) R) a 1 0 : R) (0 : R)
aux :
  Eq.{u_1 + 1} (α := R) (discr (n := Fin 2) ((scalar (Fin 2) : (a : R) → Matrix (Fin 2) (Fin 2) R) a)) 0 ↔
    Eq (α := R) ((scalar (Fin 2) : (a : R) → Matrix (Fin 2) (Fin 2) R) a 0 0 : R)
      ((scalar (Fin 2) : (a : R) → Matrix (Fin 2) (Fin 2) R) a 1 1 : R)
h :
  Eq (α := R) ((scalar (Fin 2) : (a : R) → Matrix (Fin 2) (Fin 2) R) a 0 0 : R)
    ((scalar (Fin 2) : (a : R) → Matrix (Fin 2) (Fin 2) R) a 1 1 : R)
⊢ Eq (α := R) ((scalar (Fin 2) : (a : R) → Matrix (Fin 2) (Fin 2) R) a 0 1 : R) (0 : R)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
R : Type u_1
inst : CommRing R
m : Matrix (Fin 2) (Fin 2) R
inst_1 : IsReduced R
hm : m 1 0 = 0
aux : m.discr = 0 ↔ m 0 0 = m 1 1
h : m 0 0 = m 1 1
h' : m 0 1 = 0
h₁ : (scalar (Fin 2) : (a : R) → Matrix (Fin 2) (Fin 2) R) (m 1 1) = m
⊢ Membership.mem (γ := Set (Matrix (Fin 2) (Fin 2) R))
    (Set.range (ι := R) (⇑(scalar (Fin 2)) : (a : R) → Matrix (Fin 2) (Fin 2) R)) m

Tactic:
use m 1 1

Premises used: OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
R : Type u_1
inst : CommRing R
m : Matrix (Fin 2) (Fin 2) R
inst_1 : IsReduced R
hm : m 1 0 = 0
aux : m.discr = 0 ↔ m 0 0 = m 1 1
h : m 0 0 = m 1 1
h' : m 0 1 = 0
h₁ : ∀ (i j : Fin 2), (scalar (Fin 2) : (a : R) → Matrix (Fin 2) (Fin 2) R) (m 1 1) i j = m i j
⊢ (scalar (Fin 2) : (a : R) → Matrix (Fin 2) (Fin 2) R) (m 1 1) = m

Tactic:
ext i j
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
R : Type u_1
inst : CommRing R
m : Matrix (Fin 2) (Fin 2) R
inst_1 : IsReduced R
hm : m 1 0 = 0
aux : m.discr = 0 ↔ m 0 0 = m 1 1
h : m 0 0 = m 1 1
h' : m 0 1 = 0
i j : Fin 2
h₁ :
  (scalar (Fin 2) : (a : R) → Matrix (Fin 2) (Fin 2) R) (m 1 1) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) j =
    m ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) j
h₂ :
  (scalar (Fin 2) : (a : R) → Matrix (Fin 2) (Fin 2) R) (m 1 1) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) j =
    m ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) j
⊢ (scalar (Fin 2) : (a : R) → Matrix (Fin 2) (Fin 2) R) (m 1 1) i j = m i j

Tactic:
fin_cases i
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
R : Type u_1
inst : CommRing R
m : Matrix (Fin 2) (Fin 2) R
inst_1 : IsReduced R
hm : m 1 0 = 0
aux : m.discr = 0 ↔ m 0 0 = m 1 1
h : m 0 0 = m 1 1
h' : m 0 1 = 0
j : Fin 2
h₁ :
  (scalar (Fin 2) : (a : R) → Matrix (Fin 2) (Fin 2) R) (m 1 1) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)
      ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) =
    m ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2))
h₂ :
  (scalar (Fin 2) : (a : R) → Matrix (Fin 2) (Fin 2) R) (m 1 1) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)
      ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) =
    m ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2))
⊢ (scalar (Fin 2) : (a : R) → Matrix (Fin 2) (Fin 2) R) (m 1 1) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) j =
    m ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) j

Tactic:
fin_cases j
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
R : Type u_1
inst : CommRing R
m : Matrix (Fin 2) (Fin 2) R
inst_1 : IsReduced R
hm : m 1 0 = 0
aux : m.discr = 0 ↔ m 0 0 = m 1 1
h : m 0 0 = m 1 1
h' : m 0 1 = 0
j : Fin 2
h₁ :
  (scalar (Fin 2) : (a : R) → Matrix (Fin 2) (Fin 2) R) (m 1 1) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)
      ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) =
    m ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2))
h₂ :
  (scalar (Fin 2) : (a : R) → Matrix (Fin 2) (Fin 2) R) (m 1 1) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)
      ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) =
    m ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2))
⊢ (scalar (Fin 2) : (a : R) → Matrix (Fin 2) (Fin 2) R) (m 1 1) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) j =
    m ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) j

Tactic:
fin_cases j
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
R : Type u_1
inst : CommRing R
m : Matrix (Fin 2) (Fin 2) R
inst_1 : IsReduced R
hm : m 1 0 = 0
aux : m.discr = 0 ↔ m 0 0 = m 1 1
h : m 0 0 = m 1 1
h' : m 0 1 = 0
⊢ (scalar (Fin 2) : (a : R) → Matrix (Fin 2) (Fin 2) R) (m 1 1) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)
      ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) =
    m ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2))

Tactic:
simp [h, h', hm]
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
R : Type u_1
inst : CommRing R
m : Matrix (Fin 2) (Fin 2) R
inst_1 : IsReduced R
hm : m 1 0 = 0
aux : m.discr = 0 ↔ m 0 0 = m 1 1
h : m 0 0 = m 1 1
h' : m 0 1 = 0
⊢ (scalar (Fin 2) : (a : R) → Matrix (Fin 2) (Fin 2) R) (m 1 1) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)
      ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) =
    m ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2))

Tactic:
simp [h, h', hm]
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
R : Type u_1
inst : CommRing R
m : Matrix (Fin 2) (Fin 2) R
inst_1 : IsReduced R
hm : m 1 0 = 0
aux : m.discr = 0 ↔ m 0 0 = m 1 1
h : m 0 0 = m 1 1
h' : m 0 1 = 0
⊢ (scalar (Fin 2) : (a : R) → Matrix (Fin 2) (Fin 2) R) (m 1 1) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)
      ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) =
    m ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2))

Tactic:
simp [h, h', hm]
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
R : Type u_1
inst : CommRing R
m : Matrix (Fin 2) (Fin 2) R
inst_1 : IsReduced R
hm : m 1 0 = 0
aux : m.discr = 0 ↔ m 0 0 = m 1 1
h : m 0 0 = m 1 1
h' : m 0 1 = 0
⊢ (scalar (Fin 2) : (a : R) → Matrix (Fin 2) (Fin 2) R) (m 1 1) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)
      ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) =
    m ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2))

Tactic:
simp [h, h', hm]
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
R : Type u_1
inst : CommRing R
m : Matrix (Fin 2) (Fin 2) R
inst_1 : IsReduced R
hm : m 1 0 = 0
aux : m.discr = 0 ↔ m 0 0 = m 1 1
⊢ ∀ (h : m 0 0 = m 1 1),
    Membership.mem (γ := Set (Matrix (Fin 2) (Fin 2) R))
        (Set.range (ι := R) (⇑(scalar (Fin 2)) : (a : R) → Matrix (Fin 2) (Fin 2) R)) m ↔
      m 0 1 = 0

Tactic:
have (h : m 0 0 = m 1 1) : m ∈ Set.range (scalar _) ↔ m 0 1 = 0 := by
    constructor
    · rintro ⟨a, rfl⟩
      simp
    · intro h'
      use m 1 1
      ext i j
      fin_cases i <;> fin_cases j <;> simp [h, h', hm]
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
K : Type u_1
inst : Field K
m : Matrix (Fin 2) (Fin 2) K
inst_1 : NeZero.{u_1} (R := K) 2
⊢ 4 = HMul.hMul (α := K) 2 2

Tactic:
norm_num
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
K : Type u_1
inst : Field K
m : Matrix (Fin 2) (Fin 2) K
inst_1 : NeZero.{u_1} (R := K) 2
simp :
  (m - diagonal fun (x : Fin 2) ↦ (m 0 0 + m 1 1) / 2) * (m - diagonal fun (x : Fin 2) ↦ (m 0 0 + m 1 1) / 2) =
    diagonal fun (x : Fin 2) ↦
      ((m 0 0 + m 1 1) * (m 0 0 + m 1 1) - HMul.hMul (α := K) 2 2 * (m 0 0 * m 1 1 - m 0 1 * m 1 0)) /
        HMul.hMul (α := K) 2 2
⊢ HPow.hPow (β := ℕ)
      (HSub.hSub (β := Matrix (Fin 2) (Fin 2) K) m
        ((scalar (Fin 2) : (a : K) → Matrix (Fin 2) (Fin 2) K) (m.trace / 2) : Matrix (Fin 2) (Fin 2) K))
      2 =
    (scalar (Fin 2) : (a : K) → Matrix (Fin 2) (Fin 2) K) (m.discr / 4)

Tactic:
simp only [scalar_apply, trace_fin_two, discr_fin_two, trace_fin_two,
    det_fin_two, sq, (by norm_num : (4 : K) = 2 * 2)]

Premises used: Matrix.trace_fin_two, sq, Matrix.scalar_apply, Matrix.det_fin_two, Matrix.discr_fin_two
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
K : Type u_1
inst : Field K
m : Matrix (Fin 2) (Fin 2) K
inst_1 : NeZero.{u_1} (R := K) 2
a :
  ∀ (i j : Fin 2),
    ((m - diagonal fun (x : Fin 2) ↦ (m 0 0 + m 1 1) / 2) * (m - diagonal fun (x : Fin 2) ↦ (m 0 0 + m 1 1) / 2)) i j =
      diagonal
        (fun (x : Fin 2) ↦
          ((m 0 0 + m 1 1) * (m 0 0 + m 1 1) - HMul.hMul (α := K) 2 2 * (m 0 0 * m 1 1 - m 0 1 * m 1 0)) /
            HMul.hMul (α := K) 2 2)
        i j
⊢ (m - diagonal fun (x : Fin 2) ↦ (m 0 0 + m 1 1) / 2) * (m - diagonal fun (x : Fin 2) ↦ (m 0 0 + m 1 1) / 2) =
    diagonal fun (x : Fin 2) ↦
      ((m 0 0 + m 1 1) * (m 0 0 + m 1 1) - HMul.hMul (α := K) 2 2 * (m 0 0 * m 1 1 - m 0 1 * m 1 0)) /
        HMul.hMul (α := K) 2 2

Tactic:
ext i j
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
K : Type u_1
inst : Field K
m : Matrix (Fin 2) (Fin 2) K
inst_1 : NeZero.{u_1} (R := K) 2
i j : Fin 2
a :
  ((m - diagonal fun (x : Fin 2) ↦ (m 0 0 + m 1 1) / 2) * (m - diagonal fun (x : Fin 2) ↦ (m 0 0 + m 1 1) / 2))
      ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) j =
    diagonal
      (fun (x : Fin 2) ↦
        ((m 0 0 + m 1 1) * (m 0 0 + m 1 1) - HMul.hMul (α := K) 2 2 * (m 0 0 * m 1 1 - m 0 1 * m 1 0)) /
          HMul.hMul (α := K) 2 2)
      ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) j
a₁ :
  ((m - diagonal fun (x : Fin 2) ↦ (m 0 0 + m 1 1) / 2) * (m - diagonal fun (x : Fin 2) ↦ (m 0 0 + m 1 1) / 2))
      ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) j =
    diagonal
      (fun (x : Fin 2) ↦
        ((m 0 0 + m 1 1) * (m 0 0 + m 1 1) - HMul.hMul (α := K) 2 2 * (m 0 0 * m 1 1 - m 0 1 * m 1 0)) /
          HMul.hMul (α := K) 2 2)
      ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) j
⊢ ((m - diagonal fun (x : Fin 2) ↦ (m 0 0 + m 1 1) / 2) * (m - diagonal fun (x : Fin 2) ↦ (m 0 0 + m 1 1) / 2)) i j =
    diagonal
      (fun (x : Fin 2) ↦
        ((m 0 0 + m 1 1) * (m 0 0 + m 1 1) - HMul.hMul (α := K) 2 2 * (m 0 0 * m 1 1 - m 0 1 * m 1 0)) /
          HMul.hMul (α := K) 2 2)
      i j

Tactic:
fin_cases i