Would someone please tell me how I'd simplify this proof?

Stream: new members

[Ethan Barry]

Hello! I'm following this tutorial series and solved the 19th lesson's exercise. The demonstration and my solution are below. It's a proof by contradiction, and in the Exercise block, I need to set up two contradictory hypotheses.

I used the iff hypothesis to obtain a > 5, which means a != 5, but it feels like there was a simpler way to do that. Does anyone have a better solution?

import Mathlib.Tactic

-- Demonstration
example {a b : ℕ} (hab : a = 5 → b = 6) (hb : b = 7) : ¬ a = 5 := by
  by_contra g
  apply hab at g
  have hbx : ¬ b = 7 := by linarith
  contradiction

-- Exercise
example {a b : ℕ} (hab : a > 5 ↔ b = 6) (hb : b = 6) : ¬ a = 5 := by
  by_contra g
  have ha : a > 5 := by
    apply hab.mpr
    · calc
        b = 6 := by rw [hb]
        _ = 6 := by norm_num
  have hax : ¬ a = 5 := by
    apply ne_of_gt at ha
    exact ha
  contradiction

[Daniel James]

You don't need the contradiction part at all.

example {a b : ℕ} (hab : a > 5 ↔ b = 6) (hb : b = 6) : ¬ a = 5 := by
  have ha : a > 5 := hab.mpr hb
  exact ne_of_gt ha

[Ethan Barry]

Daniel James said:

You don't need the contradiction part at all.

Ooh, much nicer! I assumed I was supposed to use contradiction, since that's what that tutorial was about, but it wasn't actually specified. Thank you very much!