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

State before:
⊢ ∀ (a b : Nat), Nat.max a b = Nat.max b a
Tactic:
intro a b
State after:
a b : Nat
⊢ Nat.max a b = Nat.max b a

State before:
a b : Nat
⊢ Nat.max a b = Nat.max b a
Tactic:
cases Nat.lt_or_ge a b <;> rename_i h
State after:
case inl
a b : Nat
h : a < b
⊢ Nat.max a b = Nat.max b a

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

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

case inr
a b : Nat
h : a ≥ b
⊢ Nat.max a b = Nat.max b a
Tactic:
. rw [max_of_lt h, max_of_gt h]
State after:
case inr
a b : Nat
h : a ≥ b
⊢ Nat.max a b = Nat.max b a

State before:
case inr
a b : Nat
h : a ≥ b
⊢ Nat.max a b = Nat.max b a
Tactic:
cases Nat.eq_or_lt_of_le h <;> (clear h ; rename_i h)
State after:
case inr.inl
a b : Nat
h : b = a
⊢ Nat.max a b = Nat.max b a

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

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

case inr.inr
a b : Nat
h : b < a
⊢ Nat.max a b = Nat.max b a
Tactic:
. rw [max_of_eq h, max_of_eq' h.symm]
State after:
case inr.inr
a b : Nat
h : b < a
⊢ Nat.max a b = Nat.max b a

State before:
case inr.inr
a b : Nat
h : b < a
⊢ Nat.max a b = Nat.max b a
Tactic:
. rw [max_of_lt h, max_of_gt h]
State after:
no goals

State before:
case inl
a b : Nat
h : a < b
⊢ Nat.max a b = Nat.max b a
Tactic:
rw [max_of_lt h, max_of_gt h]
State after:
no goals

State before:
case inr.inr
a b : Nat
h : a ≥ b
h✝ : b < a
⊢ Nat.max a b = Nat.max b a
Tactic:
clear h
State after:
case inr.inr
a b : Nat
h✝ : b < a
⊢ Nat.max a b = Nat.max b a

State before:
case inr.inr
a b : Nat
h✝ : b < a
⊢ Nat.max a b = Nat.max b a
Tactic:
rename_i h
State after:
case inr.inr
a b : Nat
h : b < a
⊢ Nat.max a b = Nat.max b a

State before:
case inr.inl
a b : Nat
h : b = a
⊢ Nat.max a b = Nat.max b a
Tactic:
rw [max_of_eq h, max_of_eq' h.symm]
State after:
no goals

State before:
case inr.inr
a b : Nat
h : b < a
⊢ Nat.max a b = Nat.max b a
Tactic:
rw [max_of_lt h, max_of_gt h]
State after:
no goals