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
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
⊢ ((↑g : Matrix (Fin 2) (Fin 2) R) * m * (↑g : Matrix (Fin 2) (Fin 2) R)⁻¹).IsParabolic ↔ m.IsParabolic
have 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
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]
-- 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
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
⊢ ((↑g : Matrix (Fin 2) (Fin 2) R) * m * (↑g : Matrix (Fin 2) (Fin 2) R)⁻¹).IsParabolic ↔ m.IsParabolic
have 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
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]
-- 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
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
⊢ ((↑g : Matrix (Fin 2) (Fin 2) R) * m * (↑g : Matrix (Fin 2) (Fin 2) R)⁻¹).IsParabolic ↔ m.IsParabolic
have 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
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]
-- 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
h : m.IsParabolic
⊢ (-m).IsParabolic
have left : -m ∉ Set.range (ι := R) (⇑(scalar (Fin 2)) : (a : R) → Matrix (Fin 2) (Fin 2) R)
Tactic: constructor
-- 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
h : m.IsParabolic
left : -m ∉ Set.range (ι := R) (⇑(scalar (Fin 2)) : (a : R) → Matrix (Fin 2) (Fin 2) R)
⊢ (-m).IsParabolic
have right : (-m).discr = 0
Tactic: constructor
-- 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
h : m.IsParabolic
⊢ -m ∉ Set.range (ι := R) (⇑(scalar (Fin 2)) : (a : R) → Matrix (Fin 2) (Fin 2) R)
have left : m ∉ RingHom.range (R := R) (scalar (Fin 2))
Tactic: rw [← RingHom.coe_range, SetLike.mem_coe, neg_mem_iff]
-- 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
this : m.discr = HPow.hPow (β := ℕ) (m 0 0 - m 1 1) 2
⊢ m.discr = 0 ↔ m 0 0 = m 1 1
have rw : HPow.hPow (β := ℕ) (m 0 0 - m 1 1) 2 = 0 ↔ m 0 0 = m 1 1
Tactic: rw [this, pow_eq_zero_iff two_ne_zero, sub_eq_zero]
-- 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
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
⊢ m.discr = 0 ↔ m 0 0 = m 1 1
have rw₁ : m 0 0 - m 1 1 = 0 ↔ m 0 0 = m 1 1
Tactic: rw [this, pow_eq_zero_iff two_ne_zero, sub_eq_zero]
-- 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
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
⊢ m.discr = 0 ↔ m 0 0 = m 1 1
have rw₂ : m 0 0 = m 1 1 ↔ m 0 0 = m 1 1
Tactic: rw [this, pow_eq_zero_iff two_ne_zero, sub_eq_zero]
-- 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
⊢ m.discr = 0 ↔ m 0 0 = m 1 1
have suffices : m.discr = HPow.hPow (β := ℕ) (m 0 0 - m 1 1) 2
Tactic: suffices m.discr = (m 0 0 - m 1 1) ^ 2 by
      rw [this, pow_eq_zero_iff two_ne_zero, sub_eq_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo (hypothesis)
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 ∉ 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 aux : 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]
-- 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
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
have 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
Tactic: constructor
-- 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
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
⊢ 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
have 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
Tactic: constructor
-- 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
h : m 0 0 = m 1 1
h' : 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
have h₁ : (scalar (Fin 2) : (a : R) → Matrix (Fin 2) (Fin 2) R) (m 1 1) = m
Tactic: use m 1 1
-- 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
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) = m
have h₁ : ∀ (i j : Fin 2), (scalar (Fin 2) : (a : R) → Matrix (Fin 2) (Fin 2) R) (m 1 1) i j = m i j
Tactic: ext i j
-- 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
h : m 0 0 = m 1 1
h' : m 0 1 = 0
i j : Fin 2
⊢ (scalar (Fin 2) : (a : R) → Matrix (Fin 2) (Fin 2) R) (m 1 1) i j = m i j
have h₁ : (scalar (Fin 2) : (a : R) → Matrix (Fin 2) (Fin 2) R) (m 1 1) ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩) j =
  m ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2)) j
Tactic: fin_cases i
Cleared hypotheses: i
-- 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
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
⊢ (scalar (Fin 2) : (a : R) → Matrix (Fin 2) (Fin 2) R) (m 1 1) i j = m i j
have h₂ : (scalar (Fin 2) : (a : R) → Matrix (Fin 2) (Fin 2) R) (m 1 1) ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩) j =
  m ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2)) j
Tactic: fin_cases i
Cleared hypotheses: i
-- 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
h : m 0 0 = m 1 1
h' : m 0 1 = 0
j : 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
have h₁ : (scalar (Fin 2) : (a : R) → Matrix (Fin 2) (Fin 2) R) (m 1 1) ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩)
    ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩) =
  m ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2))
Tactic: fin_cases j
Cleared hypotheses: j
-- 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
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))
⊢ (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
have h₂ : (scalar (Fin 2) : (a : R) → Matrix (Fin 2) (Fin 2) R) (m 1 1) ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩)
    ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩) =
  m ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2))
Tactic: fin_cases j
Cleared hypotheses: j
-- 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
h : m 0 0 = m 1 1
h' : m 0 1 = 0
j : 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
have h₁ : (scalar (Fin 2) : (a : R) → Matrix (Fin 2) (Fin 2) R) (m 1 1) ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩)
    ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩) =
  m ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2))
Tactic: fin_cases j
Cleared hypotheses: j
-- 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
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))
⊢ (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
have h₂ : (scalar (Fin 2) : (a : R) → Matrix (Fin 2) (Fin 2) R) (m 1 1) ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩)
    ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩) =
  m ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2))
Tactic: fin_cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo (hypothesis)
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
⊢ 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 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
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]
-- 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
⊢ 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 : ¬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)
Tactic: tauto
Cleared hypotheses: aux, this
-- 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)
⊢ 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:
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)
⊢ 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 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)
Tactic: tauto
Cleared hypotheses: aux, this
-- 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)
⊢ 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 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)
Tactic: tauto
Cleared hypotheses: aux, this