case intro
α : Type ?u.138661
β : Type ?u.138664
b c d : ℝ≥0∞
r p q : ℝ≥0
bd : b < d
a : ℝ≥0
ac : ↑a < c
⊢ ↑a + b < c + d
α : Type ?u.138661
β : Type ?u.138664
a b c d : ℝ≥0∞
r p q : ℝ≥0
ac : a < c
bd : b < d
⊢ a + b < c + d
lift a to ℝ≥0 using ac.ne_top
case intro.intro
α : Type ?u.138661
β : Type ?u.138664
c d : ℝ≥0∞
r p q a : ℝ≥0
ac : ↑a < c
b : ℝ≥0
bd : ↑b < d
⊢ ↑a + ↑b < c + d
case intro
α : Type ?u.138661
β : Type ?u.138664
b c d : ℝ≥0∞
r p q : ℝ≥0
bd : b < d
a : ℝ≥0
ac : ↑a < c
⊢ ↑a + b < c + d
lift b to ℝ≥0 using bd.ne_top
case intro.intro.none
α : Type ?u.138661
β : Type ?u.138664
d : ℝ≥0∞
r p q a b : ℝ≥0
bd : ↑b < d
ac : ↑a < none
⊢ ↑a + ↑b < none + d

case intro.intro.some
α : Type ?u.138661
β : Type ?u.138664
d : ℝ≥0∞
r p q a b : ℝ≥0
bd : ↑b < d
val✝ : ℝ≥0
ac : ↑a < Option.some val✝
⊢ ↑a + ↑b < Option.some val✝ + d
case intro.intro
α : Type ?u.138661
β : Type ?u.138664
c d : ℝ≥0∞
r p q a : ℝ≥0
ac : ↑a < c
b : ℝ≥0
bd : ↑b < d
⊢ ↑a + ↑b < c + d
cases c
case intro.intro.some.none
α : Type ?u.138661
β : Type ?u.138664
r p q a b val✝ : ℝ≥0
ac : ↑a < Option.some val✝
bd : ↑b < none
⊢ ↑a + ↑b < Option.some val✝ + none

case intro.intro.some.some
α : Type ?u.138661
β : Type ?u.138664
r p q a b val✝¹ : ℝ≥0
ac : ↑a < Option.some val✝¹
val✝ : ℝ≥0
bd : ↑b < Option.some val✝
⊢ ↑a + ↑b < Option.some val✝¹ + Option.some val✝
case intro.intro.some
α : Type ?u.138661
β : Type ?u.138664
d : ℝ≥0∞
r p q a b : ℝ≥0
bd : ↑b < d
val✝ : ℝ≥0
ac : ↑a < Option.some val✝
⊢ ↑a + ↑b < Option.some val✝ + d
cases d
case intro.intro.some.some
α : Type ?u.138661
β : Type ?u.138664
r p q a b val✝¹ val✝ : ℝ≥0
ac : a < val✝¹
bd : b < val✝
⊢ a + b < val✝¹ + val✝
case intro.intro.some.some
α : Type ?u.138661
β : Type ?u.138664
r p q a b val✝¹ : ℝ≥0
ac : ↑a < Option.some val✝¹
val✝ : ℝ≥0
bd : ↑b < Option.some val✝
⊢ ↑a + ↑b < Option.some val✝¹ + Option.some val✝
simp only [← coe_add, some_eq_coe, coe_lt_coe] at *
no goals
case intro.intro.some.some
α : Type ?u.138661
β : Type ?u.138664
r p q a b val✝¹ val✝ : ℝ≥0
ac : a < val✝¹
bd : b < val✝
⊢ a + b < val✝¹ + val✝
exact add_lt_add ac bd
no goals
case intro.intro.none
α : Type ?u.138661
β : Type ?u.138664
d : ℝ≥0∞
r p q a b : ℝ≥0
bd : ↑b < d
ac : ↑a < none
⊢ ↑a + ↑b < none + d
simp
no goals
case intro.intro.some.none
α : Type ?u.138661
β : Type ?u.138664
r p q a b val✝ : ℝ≥0
ac : ↑a < Option.some val✝
bd : ↑b < none
⊢ ↑a + ↑b < Option.some val✝ + none
simp