awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo (goal)
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
this :
  ∀ (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
inl :
  ∀ (this : ¬m 0 0 = m 1 1),
    m.discr = 0 →
      m 0 0 = m 1 1 →
        (m ∉ Set.range (ι := R) (⇑(scalar (Fin 2)) : (a : R) → Matrix (Fin 2) (Fin 2) R) ∧ m.discr = 0 ↔
          m 0 0 = m 1 1 ∧ m 0 1 ≠ 0)
inl₁ :
  ∀
    (this :
      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),
    m.discr = 0 →
      m 0 0 = m 1 1 →
        (m ∉ Set.range (ι := R) (⇑(scalar (Fin 2)) : (a : R) → Matrix (Fin 2) (Fin 2) R) ∧ m.discr = 0 ↔
          m 0 0 = m 1 1 ∧ m 0 1 ≠ 0)
inr :
  ∀ (this : ¬m 0 0 = m 1 1),
    ¬m.discr = 0 →
      ¬m 0 0 = m 1 1 →
        (m ∉ Set.range (ι := R) (⇑(scalar (Fin 2)) : (a : R) → Matrix (Fin 2) (Fin 2) R) ∧ m.discr = 0 ↔
          m 0 0 = m 1 1 ∧ m 0 1 ≠ 0)
inr₁ :
  ∀
    (this :
      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),
    ¬m.discr = 0 →
      ¬m 0 0 = m 1 1 →
        (m ∉ Set.range (ι := R) (⇑(scalar (Fin 2)) : (a : R) → Matrix (Fin 2) (Fin 2) R) ∧ m.discr = 0 ↔
          m 0 0 = m 1 1 ∧ m 0 1 ≠ 0)
inl₂ :
  ∀
    (this :
      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),
    m.discr = 0 →
      m 0 0 = m 1 1 →
        (m ∉ Set.range (ι := R) (⇑(scalar (Fin 2)) : (a : R) → Matrix (Fin 2) (Fin 2) R) ∧ m.discr = 0 ↔
          m 0 0 = m 1 1 ∧ m 0 1 ≠ 0)
inr₂ :
  ∀ (this : ¬m 0 0 = m 1 1),
    ¬m.discr = 0 →
      ¬m 0 0 = m 1 1 →
        (m ∉ Set.range (ι := R) (⇑(scalar (Fin 2)) : (a : R) → Matrix (Fin 2) (Fin 2) R) ∧ m.discr = 0 ↔
          m 0 0 = m 1 1 ∧ m 0 1 ≠ 0)
inr₃ :
  ∀
    (this :
      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),
    ¬m.discr = 0 →
      ¬m 0 0 = m 1 1 →
        (m ∉ Set.range (ι := R) (⇑(scalar (Fin 2)) : (a : R) → Matrix (Fin 2) (Fin 2) R) ∧ m.discr = 0 ↔
          m 0 0 = m 1 1 ∧ m 0 1 ≠ 0)
⊢ m ∉ Set.range (ι := R) (⇑(scalar (Fin 2)) : (a : R) → Matrix (Fin 2) (Fin 2) R) ∧ m.discr = 0 ↔
    m 0 0 = m 1 1 ∧ m 0 1 ≠ 0
have inl₃ : ∀
  (this :
    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),
  m.discr = 0 →
    m 0 0 = m 1 1 →
      m ∉ Set.range (ι := R) (⇑(scalar (Fin 2)) : (a : R) → Matrix (Fin 2) (Fin 2) R) ∧ m.discr = 0 →
        m 0 0 = m 1 1 ∧ m 0 1 ≠ 0
Tactic: tauto
Cleared hypotheses: aux, this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo (goal)
Goal:
K : Type u_1
inst : Field K
m : Matrix (Fin 2) (Fin 2) K
inst_1 : NeZero.{u_1} (R := K) 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)
have 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
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)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo (goal)
Goal:
K : Type u_1
inst : Field K
m : Matrix (Fin 2) (Fin 2) K
inst_1 : NeZero.{u_1} (R := K) 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) =
    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
have 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
Tactic: ext i j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo (goal)
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
⊢ ((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
have 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, sorry⟩ : 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, sorry⟩) j
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo (goal)
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
⊢ ((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
have 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, sorry⟩ : 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, sorry⟩) j
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo (goal)
Goal:
K : Type u_1
inst : Field K
m : Matrix (Fin 2) (Fin 2) K
inst_1 : NeZero.{u_1} (R := K) 2
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))
      ((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
have 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, sorry⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 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)
    ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩) ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩)
Tactic: fin_cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo (goal)
Goal:
K : Type u_1
inst : Field K
m : Matrix (Fin 2) (Fin 2) K
inst_1 : NeZero.{u_1} (R := K) 2
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)) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 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)
      ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)
⊢ ((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
have 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, sorry⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 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)
    ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩) ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩)
Tactic: fin_cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo (goal)
Goal:
K : Type u_1
inst : Field K
m : Matrix (Fin 2) (Fin 2) K
inst_1 : NeZero.{u_1} (R := K) 2
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))
      ((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
have 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, sorry⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 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)
    ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩) ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩)
Tactic: fin_cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo (goal)
Goal:
K : Type u_1
inst : Field K
m : Matrix (Fin 2) (Fin 2) K
inst_1 : NeZero.{u_1} (R := K) 2
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) (⟨1, ⋯⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 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)
      ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)
⊢ ((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
have 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, sorry⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 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)
    ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩) ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩)
Tactic: fin_cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo (goal)
Goal:
K : Type u_1
inst : Field K
m : Matrix (Fin 2) (Fin 2) K
inst_1 : NeZero.{u_1} (R := K) 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))
      ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 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)
      ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)
have a : (m 0 0 - (m 0 0 + m 1 1) / 2) * (m 0 0 - (m 0 0 + m 1 1) / 2) + m 0 1 * m 1 0 =
  ((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: simp [Matrix.mul_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo (goal)
Goal:
K : Type u_1
inst : Field K
m : Matrix (Fin 2) (Fin 2) K
inst_1 : NeZero.{u_1} (R := K) 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))
      ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 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)
      ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)
have a : (m 0 0 - (m 0 0 + m 1 1) / 2) * m 0 1 + m 0 1 * (m 1 1 - (m 0 0 + m 1 1) / 2) = 0
Tactic: simp [Matrix.mul_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo (goal)
Goal:
K : Type u_1
inst : Field K
m : Matrix (Fin 2) (Fin 2) K
inst_1 : NeZero.{u_1} (R := K) 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))
      ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 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)
      ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)
have a : m 1 0 * (m 0 0 - (m 0 0 + m 1 1) / 2) + (m 1 1 - (m 0 0 + m 1 1) / 2) * m 1 0 = 0
Tactic: simp [Matrix.mul_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo (goal)
Goal:
K : Type u_1
inst : Field K
m : Matrix (Fin 2) (Fin 2) K
inst_1 : NeZero.{u_1} (R := K) 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))
      ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 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)
      ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)
have a : m 1 0 * m 0 1 + (m 1 1 - (m 0 0 + m 1 1) / 2) * (m 1 1 - (m 0 0 + m 1 1) / 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: simp [Matrix.mul_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo (goal)
Goal:
K : Type u_1
inst : Field K
m : Matrix (Fin 2) (Fin 2) K
inst_1 : NeZero.{u_1} (R := K) 2
⊢ m.IsParabolic ↔
    ∃ (a : K) (n : Matrix (Fin 2) (Fin 2) K),
      m =
          HAdd.hAdd (α := Matrix (Fin 2) (Fin 2) K)
            ((scalar (Fin 2) : (a : K) → Matrix (Fin 2) (Fin 2) K) a : Matrix (Fin 2) (Fin 2) K) n ∧
        n ≠ 0 ∧ HPow.hPow (β := ℕ) n 2 = 0
have mp : m.IsParabolic →
  ∃ (a : K) (n : Matrix (Fin 2) (Fin 2) K),
    m =
        HAdd.hAdd (α := Matrix (Fin 2) (Fin 2) K)
          ((scalar (Fin 2) : (a : K) → Matrix (Fin 2) (Fin 2) K) a : Matrix (Fin 2) (Fin 2) K) n ∧
      n ≠ 0 ∧ HPow.hPow (β := ℕ) n 2 = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo (goal)
Goal:
K : Type u_1
inst : Field K
m : Matrix (Fin 2) (Fin 2) K
inst_1 : NeZero.{u_1} (R := K) 2
mp :
  m.IsParabolic →
    ∃ (a : K) (n : Matrix (Fin 2) (Fin 2) K),
      m =
          HAdd.hAdd (α := Matrix (Fin 2) (Fin 2) K)
            ((scalar (Fin 2) : (a : K) → Matrix (Fin 2) (Fin 2) K) a : Matrix (Fin 2) (Fin 2) K) n ∧
        n ≠ 0 ∧ HPow.hPow (β := ℕ) n 2 = 0
⊢ m.IsParabolic ↔
    ∃ (a : K) (n : Matrix (Fin 2) (Fin 2) K),
      m =
          HAdd.hAdd (α := Matrix (Fin 2) (Fin 2) K)
            ((scalar (Fin 2) : (a : K) → Matrix (Fin 2) (Fin 2) K) a : Matrix (Fin 2) (Fin 2) K) n ∧
        n ≠ 0 ∧ HPow.hPow (β := ℕ) n 2 = 0
have mpr : (∃ (a : K) (n : Matrix (Fin 2) (Fin 2) K),
    m =
        HAdd.hAdd (α := Matrix (Fin 2) (Fin 2) K)
          ((scalar (Fin 2) : (a : K) → Matrix (Fin 2) (Fin 2) K) a : Matrix (Fin 2) (Fin 2) K) n ∧
      n ≠ 0 ∧ HPow.hPow (β := ℕ) n 2 = 0) →
  m.IsParabolic
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo (goal)
Goal:
K : Type u_1
inst : Field K
m : Matrix (Fin 2) (Fin 2) K
inst_1 : NeZero.{u_1} (R := K) 2
a : K
n : Matrix (Fin 2) (Fin 2) K
hm :
  m =
    HAdd.hAdd (α := Matrix (Fin 2) (Fin 2) K)
      ((scalar (Fin 2) : (a : K) → Matrix (Fin 2) (Fin 2) K) a : Matrix (Fin 2) (Fin 2) K) n
hn0 : n ≠ 0
hnsq : HPow.hPow (β := ℕ) n 2 = 0
⊢ m.IsParabolic
have mpr : m ∉ Set.range (ι := K) (⇑(scalar (Fin 2)) : (a : K) → Matrix (Fin 2) (Fin 2) K)
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo (goal)
Goal:
K : Type u_1
inst : Field K
m : Matrix (Fin 2) (Fin 2) K
inst_1 : NeZero.{u_1} (R := K) 2
a : K
n : Matrix (Fin 2) (Fin 2) K
hm :
  m =
    HAdd.hAdd (α := Matrix (Fin 2) (Fin 2) K)
      ((scalar (Fin 2) : (a : K) → Matrix (Fin 2) (Fin 2) K) a : Matrix (Fin 2) (Fin 2) K) n
hn0 : n ≠ 0
hnsq : HPow.hPow (β := ℕ) n 2 = 0
mpr : m ∉ Set.range (ι := K) (⇑(scalar (Fin 2)) : (a : K) → Matrix (Fin 2) (Fin 2) K)
⊢ m.IsParabolic
have mpr₁ : m.discr = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo (goal)
Goal:
K : Type u_1
inst : Field K
m : Matrix (Fin 2) (Fin 2) K
inst_1 : NeZero.{u_1} (R := K) 2
a : K
n : Matrix (Fin 2) (Fin 2) K
hm :
  m =
    HAdd.hAdd (α := Matrix (Fin 2) (Fin 2) K)
      ((scalar (Fin 2) : (a : K) → Matrix (Fin 2) (Fin 2) K) a : Matrix (Fin 2) (Fin 2) K) n
hn0 : n ≠ 0
hnsq : HPow.hPow (β := ℕ) n 2 = 0
⊢ m ∉ Set.range (ι := K) (⇑(scalar (Fin 2)) : (a : K) → Matrix (Fin 2) (Fin 2) K)
have mpr : Membership.mem (γ := Set (Matrix (Fin 2) (Fin 2) K))
    (Set.range (ι := K) (⇑(scalar (Fin 2)) : (a : K) → Matrix (Fin 2) (Fin 2) K)) m →
  ∀ (b : K) (hb : (scalar (Fin 2) : (a : K) → Matrix (Fin 2) (Fin 2) K) b = m), n = 0
Tactic: refine fun ⟨b, hb⟩ ↦ hn0 ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo (goal)
Goal:
K : Type u_1
inst : Field K
m : Matrix (Fin 2) (Fin 2) K
inst_1 : NeZero.{u_1} (R := K) 2
a : K
n : Matrix (Fin 2) (Fin 2) K
hm :
  m =
    HAdd.hAdd (α := Matrix (Fin 2) (Fin 2) K)
      ((scalar (Fin 2) : (a : K) → Matrix (Fin 2) (Fin 2) K) a : Matrix (Fin 2) (Fin 2) K) n
hn0 : n ≠ 0
hnsq : HPow.hPow (β := ℕ) n 2 = 0
h :
  Membership.mem (γ := Set (Matrix (Fin 2) (Fin 2) K))
    (Set.range (ι := K) (⇑(scalar (Fin 2)) : (a : K) → Matrix (Fin 2) (Fin 2) K)) m
b : K
hb : (scalar (Fin 2) : (a : K) → Matrix (Fin 2) (Fin 2) K) b = m
⊢ n = 0
have mpr : ∀
  (hm :
    HSub.hSub (β := Matrix (Fin 2) (Fin 2) K) m
        ((scalar (Fin 2) : (a : K) → Matrix (Fin 2) (Fin 2) K) a : Matrix (Fin 2) (Fin 2) K) =
      n)
  (hn0 : n ≠ 0) (hnsq : HPow.hPow (β := ℕ) n 2 = 0),
  Membership.mem (γ := Set (Matrix (Fin 2) (Fin 2) K))
      (Set.range (ι := K) (⇑(scalar (Fin 2)) : (a : K) → Matrix (Fin 2) (Fin 2) K)) m →
    ∀ (b : K) (hb : (scalar (Fin 2) : (a : K) → Matrix (Fin 2) (Fin 2) K) b = m), n = 0
Tactic: rw [← sub_eq_iff_eq_add'] at hm
Cleared hypotheses: hm, hn0, hnsq, h, b, hb
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo (hypothesis)
Goal:
K : Type u_1
inst : Field K
m : Matrix (Fin 2) (Fin 2) K
inst_1 : NeZero.{u_1} (R := K) 2
a : K
n : Matrix (Fin 2) (Fin 2) K
hm :
  m =
    HAdd.hAdd (α := Matrix (Fin 2) (Fin 2) K)
      ((scalar (Fin 2) : (a : K) → Matrix (Fin 2) (Fin 2) K) a : Matrix (Fin 2) (Fin 2) K) n
hn0 : n ≠ 0
hnsq : HPow.hPow (β := ℕ) n 2 = 0
this :
  Eq (α := Matrix (Fin 2) (Fin 2) K)
    ((scalar (Fin 2) : (a : K) → Matrix (Fin 2) (Fin 2) K) (m.discr / 4) : Matrix (Fin 2) (Fin 2) K)
    (0 : Matrix (Fin 2) (Fin 2) K)
⊢ m.discr = 0
have this₁ : m.discr = 0 ∨ Eq.{u_1 + 1} (α := K) 4 0
Tactic: rw [← map_zero (scalar (Fin 2)), scalar_inj, div_eq_zero_iff] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo (hypothesis)
Goal:
K : Type u_1
inst : Field K
m : Matrix (Fin 2) (Fin 2) K
inst_1 : NeZero.{u_1} (R := K) 2
a : K
n : Matrix (Fin 2) (Fin 2) K
hm :
  m =
    HAdd.hAdd (α := Matrix (Fin 2) (Fin 2) K)
      ((scalar (Fin 2) : (a : K) → Matrix (Fin 2) (Fin 2) K) a : Matrix (Fin 2) (Fin 2) K) n
hn0 : n ≠ 0
hnsq : HPow.hPow (β := ℕ) n 2 = 0
this : m.discr = 0 ∨ Eq.{u_1 + 1} (α := K) 4 0
⊢ m.discr = 0
have this₁ : Ne.{u_1 + 1} (α := K) 4 0
Tactic: have : (4 : K) ≠ 0 := by simpa [show (4 : K) = 2 ^ 2 by norm_num] using NeZero.ne _
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo (goal)
Goal:
K : Type u_1
inst : Field K
m : Matrix (Fin 2) (Fin 2) K
inst_1 : NeZero.{u_1} (R := K) 2
a : K
n : Matrix (Fin 2) (Fin 2) K
hm :
  m =
    HAdd.hAdd (α := Matrix (Fin 2) (Fin 2) K)
      ((scalar (Fin 2) : (a : K) → Matrix (Fin 2) (Fin 2) K) a : Matrix (Fin 2) (Fin 2) K) n
hn0 : n ≠ 0
hnsq : HPow.hPow (β := ℕ) n 2 = 0
this_1 : m.discr = 0 ∨ Eq.{u_1 + 1} (α := K) 4 0
this : Ne.{u_1 + 1} (α := K) 4 0
⊢ m.discr = 0
have inl : ∀ (this : m.discr = 0), m.discr = 0
Tactic: tauto
Cleared hypotheses: this_1
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo (goal)
Goal:
K : Type u_1
inst : Field K
m : Matrix (Fin 2) (Fin 2) K
inst_1 : NeZero.{u_1} (R := K) 2
a : K
n : Matrix (Fin 2) (Fin 2) K
hm :
  m =
    HAdd.hAdd (α := Matrix (Fin 2) (Fin 2) K)
      ((scalar (Fin 2) : (a : K) → Matrix (Fin 2) (Fin 2) K) a : Matrix (Fin 2) (Fin 2) K) n
hn0 : n ≠ 0
hnsq : HPow.hPow (β := ℕ) n 2 = 0
this_1 : m.discr = 0 ∨ Eq.{u_1 + 1} (α := K) 4 0
this : Ne.{u_1 + 1} (α := K) 4 0
inl : ∀ (this : m.discr = 0), m.discr = 0
⊢ m.discr = 0
have inr : ∀ (this : Eq.{u_1 + 1} (α := K) 4 0), m.discr = 0
Tactic: tauto
Cleared hypotheses: this_1
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo (goal)
Goal:
K : Type u_1
inst : Field K
m : Matrix (Fin 2) (Fin 2) K
inst_1 : NeZero.{u_1} (R := K) 2
a : K
n : Matrix (Fin 2) (Fin 2) K
hm :
  m =
    HAdd.hAdd (α := Matrix (Fin 2) (Fin 2) K)
      ((scalar (Fin 2) : (a : K) → Matrix (Fin 2) (Fin 2) K) a : Matrix (Fin 2) (Fin 2) K) n
hn0 : n ≠ 0
hnsq : HPow.hPow (β := ℕ) n 2 = 0
⊢ m.discr = 0
have mpr : Eq (α := Matrix (Fin 2) (Fin 2) K)
  ((scalar (Fin 2) : (a : K) → Matrix (Fin 2) (Fin 2) K) (m.discr / 4) : Matrix (Fin 2) (Fin 2) K)
  (0 : Matrix (Fin 2) (Fin 2) K)
Tactic: suffices scalar (Fin 2) (m.discr / 4) = 0 by
        rw [← map_zero (scalar (Fin 2)), scalar_inj, div_eq_zero_iff] at this
        have : (4 : K) ≠ 0 := by simpa [show (4 : K) = 2 ^ 2 by norm_num] using NeZero.ne _
        tauto