case intro.intro
α : Type ?u.152394
β : Type ?u.152397
a b c d : ℝ≥0∞
r p q : ℝ≥0
ac : a < c
bd : b < d
a' : ℝ≥0
aa' : a < ↑a'
a'c : ↑a' < c
⊢ a * b < c * d
α : Type ?u.152394
β : Type ?u.152397
a b c d : ℝ≥0∞
r p q : ℝ≥0
ac : a < c
bd : b < d
⊢ a * b < c * d
rcases lt_iff_exists_nnreal_btwn.1 ac with ⟨a', aa', a'c⟩
case intro.intro.intro
α : Type ?u.152394
β : Type ?u.152397
b c d : ℝ≥0∞
r p q : ℝ≥0
bd : b < d
a' : ℝ≥0
a'c : ↑a' < c
a : ℝ≥0
ac : ↑a < c
aa' : ↑a < ↑a'
⊢ ↑a * b < c * d
case intro.intro
α : Type ?u.152394
β : Type ?u.152397
a b c d : ℝ≥0∞
r p q : ℝ≥0
ac : a < c
bd : b < d
a' : ℝ≥0
aa' : a < ↑a'
a'c : ↑a' < c
⊢ a * b < c * d
lift a to ℝ≥0 using ne_top_of_lt aa'
case intro.intro.intro.intro.intro
α : Type ?u.152394
β : Type ?u.152397
b c d : ℝ≥0∞
r p q : ℝ≥0
bd : b < d
a' : ℝ≥0
a'c : ↑a' < c
a : ℝ≥0
ac : ↑a < c
aa' : ↑a < ↑a'
b' : ℝ≥0
bb' : b < ↑b'
b'd : ↑b' < d
⊢ ↑a * b < c * d
case intro.intro.intro
α : Type ?u.152394
β : Type ?u.152397
b c d : ℝ≥0∞
r p q : ℝ≥0
bd : b < d
a' : ℝ≥0
a'c : ↑a' < c
a : ℝ≥0
ac : ↑a < c
aa' : ↑a < ↑a'
⊢ ↑a * b < c * d
rcases lt_iff_exists_nnreal_btwn.1 bd with ⟨b', bb', b'd⟩
case intro.intro.intro.intro.intro.intro
α : Type ?u.152394
β : Type ?u.152397
c d : ℝ≥0∞
r p q a' : ℝ≥0
a'c : ↑a' < c
a : ℝ≥0
ac : ↑a < c
aa' : ↑a < ↑a'
b' : ℝ≥0
b'd : ↑b' < d
b : ℝ≥0
bd : ↑b < d
bb' : ↑b < ↑b'
⊢ ↑a * ↑b < c * d
case intro.intro.intro.intro.intro
α : Type ?u.152394
β : Type ?u.152397
b c d : ℝ≥0∞
r p q : ℝ≥0
bd : b < d
a' : ℝ≥0
a'c : ↑a' < c
a : ℝ≥0
ac : ↑a < c
aa' : ↑a < ↑a'
b' : ℝ≥0
bb' : b < ↑b'
b'd : ↑b' < d
⊢ ↑a * b < c * d
lift b to ℝ≥0 using ne_top_of_lt bb'
case intro.intro.intro.intro.intro.intro
α : Type ?u.152394
β : Type ?u.152397
c d : ℝ≥0∞
r p q a' : ℝ≥0
a'c : ↑a' < c
a : ℝ≥0
ac : ↑a < c
b' : ℝ≥0
b'd : ↑b' < d
b : ℝ≥0
bd : ↑b < d
aa' : a < a'
bb' : b < b'
⊢ ↑(a * b) < c * d
case intro.intro.intro.intro.intro.intro
α : Type ?u.152394
β : Type ?u.152397
c d : ℝ≥0∞
r p q a' : ℝ≥0
a'c : ↑a' < c
a : ℝ≥0
ac : ↑a < c
aa' : ↑a < ↑a'
b' : ℝ≥0
b'd : ↑b' < d
b : ℝ≥0
bd : ↑b < d
bb' : ↑b < ↑b'
⊢ ↑a * ↑b < c * d
norm_cast at *
no goals
case intro.intro.intro.intro.intro.intro
α : Type ?u.152394
β : Type ?u.152397
c d : ℝ≥0∞
r p q a' : ℝ≥0
a'c : ↑a' < c
a : ℝ≥0
ac : ↑a < c
b' : ℝ≥0
b'd : ↑b' < d
b : ℝ≥0
bd : ↑b < d
aa' : a < a'
bb' : b < b'
⊢ ↑(a * b) < c * d
calc
  ↑(a * b) < ↑(a' * b') := coe_lt_coe.2 (mul_lt_mul₀ aa' bb')
  _ = ↑a' * ↑b' := coe_mul
  _ ≤ c * d := mul_le_mul' a'c.le b'd.le