Theorem: PartENat.lt_coe_succ_iff_le' (Jordan/MultipleTransitivity.lean)

State before:
M : Type ?u.226745
α : Type ?u.226748
inst✝¹ : Group M
inst✝ : MulAction M α
x : PartENat
n : ℕ
⊢ x < ↑(succ n) ↔ x ≤ ↑n
Tactic:
by_cases hx : x = ⊤
State after:
case pos
M : Type ?u.226745
α : Type ?u.226748
inst✝¹ : Group M
inst✝ : MulAction M α
x : PartENat
n : ℕ
hx : x = ⊤
⊢ x < ↑(succ n) ↔ x ≤ ↑n

case neg
M : Type ?u.226745
α : Type ?u.226748
inst✝¹ : Group M
inst✝ : MulAction M α
x : PartENat
n : ℕ
hx : ¬x = ⊤
⊢ x < ↑(succ n) ↔ x ≤ ↑n

State before:
case pos
M : Type ?u.226745
α : Type ?u.226748
inst✝¹ : Group M
inst✝ : MulAction M α
x : PartENat
n : ℕ
hx : x = ⊤
⊢ x < ↑(succ n) ↔ x ≤ ↑n
Tactic:
rw [hx]
State after:
case pos
M : Type ?u.226745
α : Type ?u.226748
inst✝¹ : Group M
inst✝ : MulAction M α
x : PartENat
n : ℕ
hx : x = ⊤
⊢ ⊤ < ↑(succ n) ↔ ⊤ ≤ ↑n

State before:
case pos
M : Type ?u.226745
α : Type ?u.226748
inst✝¹ : Group M
inst✝ : MulAction M α
x : PartENat
n : ℕ
hx : x = ⊤
⊢ ⊤ < ↑(succ n) ↔ ⊤ ≤ ↑n
Tactic:
simp only [cast_succ, not_top_lt, top_le_iff, PartENat.natCast_ne_top]
State after:
no goals

State before:
case neg
M : Type ?u.226745
α : Type ?u.226748
inst✝¹ : Group M
inst✝ : MulAction M α
x : PartENat
n : ℕ
hx : ¬x = ⊤
⊢ x < ↑(succ n) ↔ x ≤ ↑n
Tactic:
rw [Nat.succ_eq_add_one n, Nat.cast_add, Nat.cast_one, PartENat.lt_add_one_iff_lt hx]
State after:
no goals