case intro
α : Type ?u.326127
β : Type ?u.326130
b c d : ℝ≥0∞
r p q a : ℝ≥0
hz : ↑a ≠ 0
⊢ ↑a / 2 < ↑a
α : Type ?u.326127
β : Type ?u.326130
a b c d : ℝ≥0∞
r p q : ℝ≥0
hz : a ≠ 0
ht : a ≠ ⊤
⊢ a / 2 < a
lift a to ℝ≥0 using ht
case intro
α : Type ?u.326127
β : Type ?u.326130
b c d : ℝ≥0∞
r p q a : ℝ≥0
hz : a ≠ 0
⊢ ↑a / 2 < ↑a
case intro
α : Type ?u.326127
β : Type ?u.326130
b c d : ℝ≥0∞
r p q a : ℝ≥0
hz : ↑a ≠ 0
⊢ ↑a / 2 < ↑a
rw [coe_ne_zero] at hz
case intro
α : Type ?u.326127
β : Type ?u.326130
b c d : ℝ≥0∞
r p q a : ℝ≥0
hz : a ≠ 0
⊢ a / 2 < a

case intro
α : Type ?u.326127
β : Type ?u.326130
b c d : ℝ≥0∞
r p q a : ℝ≥0
hz : a ≠ 0
⊢ 2 ≠ 0
case intro
α : Type ?u.326127
β : Type ?u.326130
b c d : ℝ≥0∞
r p q a : ℝ≥0
hz : a ≠ 0
⊢ ↑a / 2 < ↑a
rw [← coe_two, ← coe_div, coe_lt_coe]
no goals
case intro
α : Type ?u.326127
β : Type ?u.326130
b c d : ℝ≥0∞
r p q a : ℝ≥0
hz : a ≠ 0
⊢ a / 2 < a

case intro
α : Type ?u.326127
β : Type ?u.326130
b c d : ℝ≥0∞
r p q a : ℝ≥0
hz : a ≠ 0
⊢ 2 ≠ 0
exacts [NNReal.half_lt_self hz, two_ne_zero' _]