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

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

State before:
a b c : Nat
⊢ Nat.max (Nat.max a b) c = Nat.max a (Nat.max b c)
Tactic:
cases Nat.lt_or_ge a b
<;> cases Nat.lt_or_ge b c
<;> rename_i ab bc
State after:
case inl.inl
a b c : Nat
ab : a < b
bc : b < c
⊢ Nat.max (Nat.max a b) c = Nat.max a (Nat.max b c)

case inl.inr
a b c : Nat
ab : a < b
bc : b ≥ c
⊢ Nat.max (Nat.max a b) c = Nat.max a (Nat.max b c)

case inr.inl
a b c : Nat
ab : a ≥ b
bc : b < c
⊢ Nat.max (Nat.max a b) c = Nat.max a (Nat.max b c)

case inr.inr
a b c : Nat
ab : a ≥ b
bc : b ≥ c
⊢ Nat.max (Nat.max a b) c = Nat.max a (Nat.max b c)

State before:
case inl.inl
a b c : Nat
ab : a < b
bc : b < c
⊢ Nat.max (Nat.max a b) c = Nat.max a (Nat.max b c)

case inl.inr
a b c : Nat
ab : a < b
bc : b ≥ c
⊢ Nat.max (Nat.max a b) c = Nat.max a (Nat.max b c)

case inr.inl
a b c : Nat
ab : a ≥ b
bc : b < c
⊢ Nat.max (Nat.max a b) c = Nat.max a (Nat.max b c)

case inr.inr
a b c : Nat
ab : a ≥ b
bc : b ≥ c
⊢ Nat.max (Nat.max a b) c = Nat.max a (Nat.max b c)
Tactic:
. rw [max_of_lt ab, max_of_lt bc, max_of_lt (trans ab bc)]
State after:
case inl.inr
a b c : Nat
ab : a < b
bc : b ≥ c
⊢ Nat.max (Nat.max a b) c = Nat.max a (Nat.max b c)

case inr.inl
a b c : Nat
ab : a ≥ b
bc : b < c
⊢ Nat.max (Nat.max a b) c = Nat.max a (Nat.max b c)

case inr.inr
a b c : Nat
ab : a ≥ b
bc : b ≥ c
⊢ Nat.max (Nat.max a b) c = Nat.max a (Nat.max b c)

State before:
case inl.inr
a b c : Nat
ab : a < b
bc : b ≥ c
⊢ Nat.max (Nat.max a b) c = Nat.max a (Nat.max b c)

case inr.inl
a b c : Nat
ab : a ≥ b
bc : b < c
⊢ Nat.max (Nat.max a b) c = Nat.max a (Nat.max b c)

case inr.inr
a b c : Nat
ab : a ≥ b
bc : b ≥ c
⊢ Nat.max (Nat.max a b) c = Nat.max a (Nat.max b c)
Tactic:
. rw [max_of_lt ab, max_of_ge bc, max_of_lt ab]
State after:
case inr.inl
a b c : Nat
ab : a ≥ b
bc : b < c
⊢ Nat.max (Nat.max a b) c = Nat.max a (Nat.max b c)

case inr.inr
a b c : Nat
ab : a ≥ b
bc : b ≥ c
⊢ Nat.max (Nat.max a b) c = Nat.max a (Nat.max b c)

State before:
case inr.inl
a b c : Nat
ab : a ≥ b
bc : b < c
⊢ Nat.max (Nat.max a b) c = Nat.max a (Nat.max b c)

case inr.inr
a b c : Nat
ab : a ≥ b
bc : b ≥ c
⊢ Nat.max (Nat.max a b) c = Nat.max a (Nat.max b c)
Tactic:
. rw [max_of_ge ab, max_of_lt bc]
State after:
case inr.inr
a b c : Nat
ab : a ≥ b
bc : b ≥ c
⊢ Nat.max (Nat.max a b) c = Nat.max a (Nat.max b c)

State before:
case inr.inr
a b c : Nat
ab : a ≥ b
bc : b ≥ c
⊢ Nat.max (Nat.max a b) c = Nat.max a (Nat.max b c)
Tactic:
. rw [max_of_ge ab, max_of_ge bc, max_of_ge ab]
  exact max_of_ge (trans bc ab : c ≤ a)
State after:
no goals

State before:
case inl.inl
a b c : Nat
ab : a < b
bc : b < c
⊢ Nat.max (Nat.max a b) c = Nat.max a (Nat.max b c)
Tactic:
rw [max_of_lt ab, max_of_lt bc, max_of_lt (trans ab bc)]
State after:
no goals

State before:
case inl.inr
a b c : Nat
ab : a < b
bc : b ≥ c
⊢ Nat.max (Nat.max a b) c = Nat.max a (Nat.max b c)
Tactic:
rw [max_of_lt ab, max_of_ge bc, max_of_lt ab]
State after:
no goals

State before:
case inr.inl
a b c : Nat
ab : a ≥ b
bc : b < c
⊢ Nat.max (Nat.max a b) c = Nat.max a (Nat.max b c)
Tactic:
rw [max_of_ge ab, max_of_lt bc]
State after:
no goals

State before:
case inr.inr
a b c : Nat
ab : a ≥ b
bc : b ≥ c
⊢ Nat.max (Nat.max a b) c = Nat.max a (Nat.max b c)
Tactic:
rw [max_of_ge ab, max_of_ge bc, max_of_ge ab]
State after:
case inr.inr
a b c : Nat
ab : a ≥ b
bc : b ≥ c
⊢ Nat.max a c = a

State before:
case inr.inr
a b c : Nat
ab : a ≥ b
bc : b ≥ c
⊢ Nat.max a c = a
Tactic:
exact max_of_ge (trans bc ab : c ≤ a)
State after:
no goals