Theorem: Mt.Utils.Nat.max_of_eq (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:
rw [max_of_eq' h]
State after:
a b : Nat
h : a = b
⊢ b = a

State before:
a b : Nat
h : a = b
⊢ b = a
Tactic:
exact h.symm
State after:
no goals