-- 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)
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
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 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 ∉ 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