case mp
α : Type ?u.165330
β : Type ?u.165333
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
a : ℝ≥0∞
⊢ AddLECancellable a → a ≠ ⊤

case mpr
α : Type ?u.165330
β : Type ?u.165333
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
a : ℝ≥0∞
⊢ a ≠ ⊤ → AddLECancellable a
α : Type ?u.165330
β : Type ?u.165333
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
a : ℝ≥0∞
⊢ AddLECancellable a ↔ a ≠ ⊤
constructor
case mp
α : Type ?u.165330
β : Type ?u.165333
a b c d : ℝ≥0∞
r p q : ℝ≥0
h : AddLECancellable ⊤
⊢ False
case mp
α : Type ?u.165330
β : Type ?u.165333
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
a : ℝ≥0∞
⊢ AddLECancellable a → a ≠ ⊤
rintro h rfl
case mp
α : Type ?u.165330
β : Type ?u.165333
a b c d : ℝ≥0∞
r p q : ℝ≥0
h : AddLECancellable ⊤
⊢ ⊤ + 1 ≤ ⊤ + 0
case mp
α : Type ?u.165330
β : Type ?u.165333
a b c d : ℝ≥0∞
r p q : ℝ≥0
h : AddLECancellable ⊤
⊢ False
refine' zero_lt_one.not_le (h _)
no goals
case mp
α : Type ?u.165330
β : Type ?u.165333
a b c d : ℝ≥0∞
r p q : ℝ≥0
h : AddLECancellable ⊤
⊢ ⊤ + 1 ≤ ⊤ + 0
simp
case mpr
α : Type ?u.165330
β : Type ?u.165333
a✝ b✝ c✝ d : ℝ≥0∞
r p q : ℝ≥0
a : ℝ≥0∞
h : a ≠ ⊤
b c : ℝ≥0∞
hbc : a + b ≤ a + c
⊢ b ≤ c
case mpr
α : Type ?u.165330
β : Type ?u.165333
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
a : ℝ≥0∞
⊢ a ≠ ⊤ → AddLECancellable a
rintro h b c hbc
no goals
case mpr
α : Type ?u.165330
β : Type ?u.165333
a✝ b✝ c✝ d : ℝ≥0∞
r p q : ℝ≥0
a : ℝ≥0∞
h : a ≠ ⊤
b c : ℝ≥0∞
hbc : a + b ≤ a + c
⊢ b ≤ c
apply ENNReal.le_of_add_le_add_left h hbc