-- Mathlib/Algebra/Order/AddGroupWithTop.lean
lemma sub_pos (a b : α) : 0 < a - b ↔ b < a ∨ b = ⊤ where
  mp h

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroupWithTop α
a b : α
h : b < a
⊢ -b ≠ ⊤

Tactic:
simp [h.ne_top]

Result:
no goals

Proof state:
case inr
α : Type u_1
inst✝ : LinearOrderedAddCommGroupWithTop α
a b : α
h : b = ⊤
⊢ 0 < a - ⊤

Tactic:
simp only [sub_eq_add_neg, LinearOrderedAddCommGroupWithTop.neg_top, add_top]

Result:
case inr
α : Type u_1
inst✝ : LinearOrderedAddCommGroupWithTop α
a b : α
h : b = ⊤
⊢ 0 < ⊤

Proof state:
case h.e'_3
α : Type u_1
inst✝ : LinearOrderedAddCommGroupWithTop α
a b : α
h : b < a
⊢ 0 = (fun x => x + -b) b

Tactic:
simp [add_neg_cancel_of_ne_top h.ne_top]

Result:
no goals

Proof state:
case inr
α : Type u_1
inst✝ : LinearOrderedAddCommGroupWithTop α
a b : α
h : b = ⊤
⊢ 0 ≠ ⊤

Tactic:
exact Ne.symm top_ne_zero

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroupWithTop α
a b : α
h2 : ¬b = ⊤
h : b < a - b + b
⊢ b < a

Tactic:
rw [sub_eq_add_neg, add_assoc, add_comm (-b),
  add_neg_cancel_of_ne_top h2, add_zero] at h

Result:
α : Type u_1
inst✝ : LinearOrderedAddCommGroupWithTop α
a b : α
h2 : ¬b = ⊤
h : b < a
⊢ b < a

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroupWithTop α
a b : α
h : 0 < a - b
h2 : ¬b = ⊤
⊢ b < a

Tactic:
replace h := strictMono_add_left_of_ne_top _ h2 h

Result:
α : Type u_1
inst✝ : LinearOrderedAddCommGroupWithTop α
a b : α
h2 : ¬b = ⊤
h : (fun x => x + b) 0 < (fun x => x + b) (a - b)
⊢ b < a

Proof state:
case inr
α : Type u_1
inst✝ : LinearOrderedAddCommGroupWithTop α
a b : α
h : b = ⊤
⊢ 0 < ⊤

Tactic:
apply lt_of_le_of_ne le_top

Result:
case inr
α : Type u_1
inst✝ : LinearOrderedAddCommGroupWithTop α
a b : α
h : b = ⊤
⊢ 0 ≠ ⊤

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroupWithTop α
a b : α
h2 : ¬b = ⊤
h : b < a
⊢ b < a

Tactic:
exact h

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroupWithTop α
a b : α
h2 : ¬b = ⊤
h : (fun x => x + b) 0 < (fun x => x + b) (a - b)
⊢ b < a

Tactic:
simp only [zero_add] at h

Result:
α : Type u_1
inst✝ : LinearOrderedAddCommGroupWithTop α
a b : α
h2 : ¬b = ⊤
h : b < a - b + b
⊢ b < a

Proof state:
case inl
α : Type u_1
inst✝ : LinearOrderedAddCommGroupWithTop α
a b : α
h : b < a
⊢ 0 < a - b

Tactic:
convert strictMono_add_left_of_ne_top (-b) (by simp [h.ne_top]) h using 1

Result:
case h.e'_3
α : Type u_1
inst✝ : LinearOrderedAddCommGroupWithTop α
a b : α
h : b < a
⊢ 0 = (fun x => x + -b) b

case h.e'_4
α : Type u_1
inst✝ : LinearOrderedAddCommGroupWithTop α
a b : α
h : b < a
⊢ a - b = (fun x => x + -b) a

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroupWithTop α
a b : α
h : 0 < a - b
⊢ b < a ∨ b = ⊤

Tactic:
refine or_iff_not_imp_right.mpr fun h2 ↦ ?_

Result:
α : Type u_1
inst✝ : LinearOrderedAddCommGroupWithTop α
a b : α
h : 0 < a - b
h2 : ¬b = ⊤
⊢ b < a

Proof state:
case inr
α : Type u_1
inst✝ : LinearOrderedAddCommGroupWithTop α
a b : α
h : b = ⊤
⊢ 0 < a - b

Tactic:
rw [h]

Result:
case inr
α : Type u_1
inst✝ : LinearOrderedAddCommGroupWithTop α
a b : α
h : b = ⊤
⊢ 0 < a - ⊤

Proof state:
case h.e'_4
α : Type u_1
inst✝ : LinearOrderedAddCommGroupWithTop α
a b : α
h : b < a
⊢ a - b = (fun x => x + -b) a

Tactic:
simp [sub_eq_add_neg]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroupWithTop α
a b : α
h : b < a ∨ b = ⊤
⊢ 0 < a - b

Tactic:
rcases h with h | h

Result:
case inl
α : Type u_1
inst✝ : LinearOrderedAddCommGroupWithTop α
a b : α
h : b < a
⊢ 0 < a - b

case inr
α : Type u_1
inst✝ : LinearOrderedAddCommGroupWithTop α
a b : α
h : b = ⊤
⊢ 0 < a - b