case ht.h
α : Type ?u.294981
β : Type ?u.294984
a b c d : ℝ≥0∞
r p q : ℝ≥0
⊢ 1 ≠ ⊤
case ht
α : Type ?u.294981
β : Type ?u.294984
a b c d : ℝ≥0∞
r p q : ℝ≥0
⊢ b ≠ ⊤ ∨ 1 ≠ ⊤
right
no goals
case ht.h
α : Type ?u.294981
β : Type ?u.294984
a b c d : ℝ≥0∞
r p q : ℝ≥0
⊢ 1 ≠ ⊤
simp