Theorem: Mt.Utils.Nat.max_of_gt (Mt/Utils/Nat.lean)

State before:
a b : Nat
⊢ a > b → Nat.max a b = a
Tactic:
intro h
State after:
a b : Nat
h : a > b
⊢ Nat.max a b = a

State before:
a b : Nat
h : a > b
⊢ Nat.max a b = a
Tactic:
simp only [Nat.max, Nat.not_le_of_gt h, ite_false]
State after:
a b : Nat
h : a > b
⊢ max a b = a