α : Type ?u.265925
β : Type ?u.265928
a✝ b✝ c d : ℝ≥0∞
r p q : ℝ≥0
a b : ℝ≥0∞
h : a < b
⊢ b⁻¹ < a⁻¹
α : Type ?u.265925
β : Type ?u.265928
a b c d : ℝ≥0∞
r p q : ℝ≥0
⊢ StrictAnti Inv.inv
intro a b h
case intro
α : Type ?u.265925
β : Type ?u.265928
a✝ b✝ c d : ℝ≥0∞
r p q : ℝ≥0
b : ℝ≥0∞
a : ℝ≥0
h : ↑a < b
⊢ b⁻¹ < (↑a)⁻¹
α : Type ?u.265925
β : Type ?u.265928
a✝ b✝ c d : ℝ≥0∞
r p q : ℝ≥0
a b : ℝ≥0∞
h : a < b
⊢ b⁻¹ < a⁻¹
lift a to ℝ≥0 using h.ne_top
case intro.top
α : Type ?u.265925
β : Type ?u.265928
a✝ b c d : ℝ≥0∞
r p q a : ℝ≥0
h : ↑a < ⊤
⊢ ⊤⁻¹ < (↑a)⁻¹

case intro.coe
α : Type ?u.265925
β : Type ?u.265928
a✝ b c d : ℝ≥0∞
r p q a x✝ : ℝ≥0
h : ↑a < ↑x✝
⊢ (↑x✝)⁻¹ < (↑a)⁻¹
case intro
α : Type ?u.265925
β : Type ?u.265928
a✝ b✝ c d : ℝ≥0∞
r p q : ℝ≥0
b : ℝ≥0∞
a : ℝ≥0
h : ↑a < b
⊢ b⁻¹ < (↑a)⁻¹
induction b using recTopCoe
case intro.coe
α : Type ?u.265925
β : Type ?u.265928
a✝ b c d : ℝ≥0∞
r p q a x✝ : ℝ≥0
h : a < x✝
⊢ (↑x✝)⁻¹ < (↑a)⁻¹
case intro.coe
α : Type ?u.265925
β : Type ?u.265928
a✝ b c d : ℝ≥0∞
r p q a x✝ : ℝ≥0
h : ↑a < ↑x✝
⊢ (↑x✝)⁻¹ < (↑a)⁻¹
rw [coe_lt_coe] at h
case intro.coe.inl
α : Type ?u.265925
β : Type ?u.265928
a b c d : ℝ≥0∞
r p q x✝ : ℝ≥0
h : 0 < x✝
⊢ (↑x✝)⁻¹ < (↑0)⁻¹

case intro.coe.inr
α : Type ?u.265925
β : Type ?u.265928
a✝ b c d : ℝ≥0∞
r p q a x✝ : ℝ≥0
h : a < x✝
ha : a ≠ 0
⊢ (↑x✝)⁻¹ < (↑a)⁻¹
case intro.coe
α : Type ?u.265925
β : Type ?u.265928
a✝ b c d : ℝ≥0∞
r p q a x✝ : ℝ≥0
h : a < x✝
⊢ (↑x✝)⁻¹ < (↑a)⁻¹
rcases eq_or_ne a 0 with (rfl | ha)
case intro.coe.inr
α : Type ?u.265925
β : Type ?u.265928
a✝ b c d : ℝ≥0∞
r p q a x✝ : ℝ≥0
h : a < x✝
ha : a ≠ 0
⊢ x✝⁻¹ < a⁻¹
case intro.coe.inr
α : Type ?u.265925
β : Type ?u.265928
a✝ b c d : ℝ≥0∞
r p q a x✝ : ℝ≥0
h : a < x✝
ha : a ≠ 0
⊢ (↑x✝)⁻¹ < (↑a)⁻¹
rw [← coe_inv h.ne_bot, ← coe_inv ha, coe_lt_coe]
no goals
case intro.coe.inr
α : Type ?u.265925
β : Type ?u.265928
a✝ b c d : ℝ≥0∞
r p q a x✝ : ℝ≥0
h : a < x✝
ha : a ≠ 0
⊢ x✝⁻¹ < a⁻¹
exact NNReal.inv_lt_inv ha h
no goals
case intro.top
α : Type ?u.265925
β : Type ?u.265928
a✝ b c d : ℝ≥0∞
r p q a : ℝ≥0
h : ↑a < ⊤
⊢ ⊤⁻¹ < (↑a)⁻¹
simp
no goals
case intro.coe.inl
α : Type ?u.265925
β : Type ?u.265928
a b c d : ℝ≥0∞
r p q x✝ : ℝ≥0
h : 0 < x✝
⊢ (↑x✝)⁻¹ < (↑0)⁻¹
simp [h]