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

State before:
a b c : Nat
⊢ Nat.max a b ≤ c ↔ a ≤ c ∧ b ≤ c
Tactic:
constructor <;> intro h
<;> (cases Nat.lt_or_ge a b) <;> rename_i ab
State after:
case mp.inl
a b c : Nat
h : Nat.max a b ≤ c
ab : a < b
⊢ a ≤ c ∧ b ≤ c

case mp.inr
a b c : Nat
h : Nat.max a b ≤ c
ab : a ≥ b
⊢ a ≤ c ∧ b ≤ c

case mpr.inl
a b c : Nat
h : a ≤ c ∧ b ≤ c
ab : a < b
⊢ Nat.max a b ≤ c

case mpr.inr
a b c : Nat
h : a ≤ c ∧ b ≤ c
ab : a ≥ b
⊢ Nat.max a b ≤ c

State before:
case mp.inl
a b c : Nat
h : Nat.max a b ≤ c
ab : a < b
⊢ a ≤ c ∧ b ≤ c

case mp.inr
a b c : Nat
h : Nat.max a b ≤ c
ab : a ≥ b
⊢ a ≤ c ∧ b ≤ c

case mpr.inl
a b c : Nat
h : a ≤ c ∧ b ≤ c
ab : a < b
⊢ Nat.max a b ≤ c

case mpr.inr
a b c : Nat
h : a ≤ c ∧ b ≤ c
ab : a ≥ b
⊢ Nat.max a b ≤ c
Tactic:
. rw [max_of_lt ab] at h
  exact ⟨Nat.le_of_lt (trans ab h), h⟩
State after:
case mp.inr
a b c : Nat
h : Nat.max a b ≤ c
ab : a ≥ b
⊢ a ≤ c ∧ b ≤ c

case mpr.inl
a b c : Nat
h : a ≤ c ∧ b ≤ c
ab : a < b
⊢ Nat.max a b ≤ c

case mpr.inr
a b c : Nat
h : a ≤ c ∧ b ≤ c
ab : a ≥ b
⊢ Nat.max a b ≤ c

State before:
case mp.inr
a b c : Nat
h : Nat.max a b ≤ c
ab : a ≥ b
⊢ a ≤ c ∧ b ≤ c

case mpr.inl
a b c : Nat
h : a ≤ c ∧ b ≤ c
ab : a < b
⊢ Nat.max a b ≤ c

case mpr.inr
a b c : Nat
h : a ≤ c ∧ b ≤ c
ab : a ≥ b
⊢ Nat.max a b ≤ c
Tactic:
. rw [max_of_ge ab] at h
  exact ⟨h, trans ab h⟩
State after:
case mpr.inl
a b c : Nat
h : a ≤ c ∧ b ≤ c
ab : a < b
⊢ Nat.max a b ≤ c

case mpr.inr
a b c : Nat
h : a ≤ c ∧ b ≤ c
ab : a ≥ b
⊢ Nat.max a b ≤ c

State before:
case mpr.inl
a b c : Nat
h : a ≤ c ∧ b ≤ c
ab : a < b
⊢ Nat.max a b ≤ c

case mpr.inr
a b c : Nat
h : a ≤ c ∧ b ≤ c
ab : a ≥ b
⊢ Nat.max a b ≤ c
Tactic:
. rw [max_of_lt ab]
  exact h.right
State after:
case mpr.inr
a b c : Nat
h : a ≤ c ∧ b ≤ c
ab : a ≥ b
⊢ Nat.max a b ≤ c

State before:
case mpr.inr
a b c : Nat
h : a ≤ c ∧ b ≤ c
ab : a ≥ b
⊢ Nat.max a b ≤ c
Tactic:
. rw [max_of_ge ab]
  exact h.left
State after:
no goals

State before:
case mpr
a b c : Nat
h : a ≤ c ∧ b ≤ c
⊢ Nat.max a b ≤ c
Tactic:
cases Nat.lt_or_ge a b
State after:
case mpr.inl
a b c : Nat
h : a ≤ c ∧ b ≤ c
h✝ : a < b
⊢ Nat.max a b ≤ c

case mpr.inr
a b c : Nat
h : a ≤ c ∧ b ≤ c
h✝ : a ≥ b
⊢ Nat.max a b ≤ c

State before:
case mp.inl
a b c : Nat
h : Nat.max a b ≤ c
ab : a < b
⊢ a ≤ c ∧ b ≤ c
Tactic:
rw [max_of_lt ab] at h
State after:
case mp.inl
a b c : Nat
h : b ≤ c
ab : a < b
⊢ a ≤ c ∧ b ≤ c

State before:
case mp.inl
a b c : Nat
h : b ≤ c
ab : a < b
⊢ a ≤ c ∧ b ≤ c
Tactic:
exact ⟨Nat.le_of_lt (trans ab h), h⟩
State after:
no goals

State before:
case mp.inr
a b c : Nat
h : Nat.max a b ≤ c
ab : a ≥ b
⊢ a ≤ c ∧ b ≤ c
Tactic:
rw [max_of_ge ab] at h
State after:
case mp.inr
a b c : Nat
h : a ≤ c
ab : a ≥ b
⊢ a ≤ c ∧ b ≤ c

State before:
case mp.inr
a b c : Nat
h : a ≤ c
ab : a ≥ b
⊢ a ≤ c ∧ b ≤ c
Tactic:
exact ⟨h, trans ab h⟩
State after:
no goals

State before:
case mpr.inl
a b c : Nat
h : a ≤ c ∧ b ≤ c
ab : a < b
⊢ Nat.max a b ≤ c
Tactic:
rw [max_of_lt ab]
State after:
case mpr.inl
a b c : Nat
h : a ≤ c ∧ b ≤ c
ab : a < b
⊢ b ≤ c

State before:
case mpr.inl
a b c : Nat
h : a ≤ c ∧ b ≤ c
ab : a < b
⊢ b ≤ c
Tactic:
exact h.right
State after:
no goals

State before:
case mpr.inr
a b c : Nat
h : a ≤ c ∧ b ≤ c
ab : a ≥ b
⊢ Nat.max a b ≤ c
Tactic:
rw [max_of_ge ab]
State after:
case mpr.inr
a b c : Nat
h : a ≤ c ∧ b ≤ c
ab : a ≥ b
⊢ a ≤ c

State before:
case mpr.inr
a b c : Nat
h : a ≤ c ∧ b ≤ c
ab : a ≥ b
⊢ a ≤ c
Tactic:
exact h.left
State after:
no goals