Theorem: Nat.max'_ge (Test/Nat/Max.lean)

State before:
⊢ ∀ (x y : ℕ), x ≤ x.max' y ∧ y ≤ x.max' y
Tactic:
intro x y
State after:
x y : ℕ
⊢ x ≤ x.max' y ∧ y ≤ x.max' y

State before:
x y : ℕ
⊢ x ≤ x.max' y ∧ y ≤ x.max' y
Tactic:
by_cases h : x ≤ y <;> simp [max', h]
State after:
case neg
x y : ℕ
h : ¬x ≤ y
⊢ y ≤ x

State before:
case neg
x y : ℕ
h : ¬x ≤ y
⊢ y ≤ x
Tactic:
apply not_le_of_reverse_le h
State after:
no goals