-- 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
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 : ¬m 0 0 = m 1 1),
    ¬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
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
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 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
inl₅ :
  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 →
          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 0 0 = m 1 1 ∧ m 0 1 ≠ 0
inl₆ inl₇ :
  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 ∉ Set.range (ι := R) (⇑(scalar (Fin 2)) : (a : R) → Matrix (Fin 2) (Fin 2) R) →
            ¬m 0 1 = 0 → m 0 0 = m 1 1 ∧ m 0 1 ≠ 0
inl₈ :
  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 ∉ Set.range (ι := R) (⇑(scalar (Fin 2)) : (a : R) → Matrix (Fin 2) (Fin 2) R) → ¬m 0 1 = 0 → m 0 0 = m 1 1
inl₉ :
  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 ∉ Set.range (ι := R) (⇑(scalar (Fin 2)) : (a : R) → Matrix (Fin 2) (Fin 2) R) → ¬m 0 1 = 0 → m 0 1 ≠ 0
inl₁₀ :
  m.discr = 0 →
    m 0 0 = m 1 1 →
      m 0 0 = m 1 1 →
        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 → m ∉ Set.range (ι := R) (⇑(scalar (Fin 2)) : (a : R) → Matrix (Fin 2) (Fin 2) R) ∧ m.discr = 0
inl₁₁ inl₁₂ :
  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 0 1 = 0 → m ∉ Set.range (ι := R) (⇑(scalar (Fin 2)) : (a : R) → Matrix (Fin 2) (Fin 2) R) ∧ m.discr = 0
inl₁₃ :
  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 0 1 = 0 → m ∉ Set.range (ι := R) (⇑(scalar (Fin 2)) : (a : R) → Matrix (Fin 2) (Fin 2) R)
inl₁₄ :
  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 0 1 = 0 → m.discr = 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 : ¬m 0 0 = m 1 1),
    ¬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₁₀ : ¬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 →
        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 0 0 = m 1 1 ∧ m 0 1 ≠ 0
Tactic: tauto
Cleared hypotheses: aux, this