Theorem: WithTop.coe_lt_iff_succ_le (Jordan/Mathlib/Set.lean)

State before:
α : Type u_1
n : ℕ
c : ℕ∞
⊢ ↑n < c ↔ ↑(Nat.succ n) ≤ c
Tactic:
induction c using WithTop.recTopCoe with
| top =>
  simp only [Nat.cast_succ, le_top, iff_true]
  apply WithTop.coe_lt_top
| coe m =>
  simp only [ENat.some_eq_coe, Nat.cast_lt, Nat.cast_le]
  exact Nat.lt_iff_add_one_le
State after:
no goals

State before:
case top
α : Type u_1
n : ℕ
⊢ ↑n < ⊤ ↔ ↑(Nat.succ n) ≤ ⊤
Tactic:
simp only [Nat.cast_succ, le_top, iff_true]
State after:
case top
α : Type u_1
n : ℕ
⊢ ↑n < ⊤

State before:
case top
α : Type u_1
n : ℕ
⊢ ↑n < ⊤
Tactic:
apply WithTop.coe_lt_top
State after:
no goals

State before:
case coe
α : Type u_1
n m : ℕ
⊢ ↑n < ↑m ↔ ↑(Nat.succ n) ≤ ↑m
Tactic:
simp only [ENat.some_eq_coe, Nat.cast_lt, Nat.cast_le]
State after:
case coe
α : Type u_1
n m : ℕ
⊢ n < m ↔ Nat.succ n ≤ m

State before:
case coe
α : Type u_1
n m : ℕ
⊢ n < m ↔ Nat.succ n ≤ m
Tactic:
exact Nat.lt_iff_add_one_le
State after:
no goals