Theorem: Mt.Utils.Nat.max_of_eq' (Mt/Utils/Nat.lean)

State before:
a b : Nat
h : a = b
⊢ a ≤ b
Tactic:
rw [h]
State after:
a b : Nat
h : a = b
⊢ b ≤ b

State before:
a b : Nat
h : a = b
⊢ b ≤ b
Tactic:
constructor
State after:
no goals