case inl
α : Type ?u.179238
β : Type ?u.179241
a c d : ℝ≥0∞
r p q : ℝ≥0
h : a ≠ ⊤ ∨ ⊤ ≠ ⊤
⊢ a - ⊤ < c → a < ⊤ + c

case inr
α : Type ?u.179238
β : Type ?u.179241
a b c d : ℝ≥0∞
r p q : ℝ≥0
h : a ≠ ⊤ ∨ b ≠ ⊤
hb : b ≠ ⊤
⊢ a - b < c → a < b + c
α : Type ?u.179238
β : Type ?u.179241
a b c d : ℝ≥0∞
r p q : ℝ≥0
h : a ≠ ⊤ ∨ b ≠ ⊤
⊢ a - b < c → a < b + c
obtain rfl | hb := eq_or_ne b ∞
case inl
α : Type ?u.179238
β : Type ?u.179241
a c d : ℝ≥0∞
r p q : ℝ≥0
h : a ≠ ⊤ ∨ ⊤ ≠ ⊤
⊢ a - ⊤ < c → a ≠ ⊤
case inl
α : Type ?u.179238
β : Type ?u.179241
a c d : ℝ≥0∞
r p q : ℝ≥0
h : a ≠ ⊤ ∨ ⊤ ≠ ⊤
⊢ a - ⊤ < c → a < ⊤ + c
rw [top_add, lt_top_iff_ne_top]
no goals
case inl
α : Type ?u.179238
β : Type ?u.179241
a c d : ℝ≥0∞
r p q : ℝ≥0
h : a ≠ ⊤ ∨ ⊤ ≠ ⊤
⊢ a - ⊤ < c → a ≠ ⊤
exact fun _ => h.resolve_right (Classical.not_not.2 rfl)
no goals
case inr
α : Type ?u.179238
β : Type ?u.179241
a b c d : ℝ≥0∞
r p q : ℝ≥0
h : a ≠ ⊤ ∨ b ≠ ⊤
hb : b ≠ ⊤
⊢ a - b < c → a < b + c
exact (cancel_of_ne hb).lt_add_of_tsub_lt_left