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

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

State before:
a b : Nat
h : a ≤ b
⊢ Nat.max a b = b
Tactic:
simp only [Nat.max, h, ite_true]
State after:
a b : Nat
h : a ≤ b
⊢ max a b = b