Theorem: Mt.Utils.Nat.max_of_ge (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:
cases Nat.eq_or_lt_of_le h <;> rename_i h
State after:
case inl
a b : Nat
h✝ : a ≥ b
h : b = a
⊢ Nat.max a b = a

case inr
a b : Nat
h✝ : a ≥ b
h : b < a
⊢ Nat.max a b = a

State before:
case inl
a b : Nat
h✝ : a ≥ b
h : b = a
⊢ Nat.max a b = a

case inr
a b : Nat
h✝ : a ≥ b
h : b < a
⊢ Nat.max a b = a
Tactic:
. exact max_of_eq h.symm
State after:
case inr
a b : Nat
h✝ : a ≥ b
h : b < a
⊢ Nat.max a b = a

State before:
case inr
a b : Nat
h✝ : a ≥ b
h : b < a
⊢ Nat.max a b = a
Tactic:
. exact max_of_gt h
State after:
no goals

State before:
case inl
a b : Nat
h✝ : a ≥ b
h : b = a
⊢ Nat.max a b = a
Tactic:
exact max_of_eq h.symm
State after:
no goals

State before:
case inr
a b : Nat
h✝ : a ≥ b
h : b < a
⊢ Nat.max a b = a
Tactic:
exact max_of_gt h
State after:
no goals