Theorem: ENNReal.conjugate_cases' (ForML/LpHoelder.lean)

State before:
p q : ℝ≥0∞
h : p⁻¹ + q⁻¹ = 1
⊢ p ≠ ⊤ ∧ q ≠ ⊤ ∨ p = 1 ∧ q = ⊤ ∨ p = ⊤ ∧ q = 1
Tactic:
cases p with
| none =>
  simpa [inv_eq_iff_eq_inv] using h
| some p =>
  cases q with
  | none =>
    simpa [inv_eq_iff_eq_inv] using h
  | some q =>
    simp
State after:
no goals

State before:
case none
q : ℝ≥0∞
h : none⁻¹ + q⁻¹ = 1
⊢ none ≠ ⊤ ∧ q ≠ ⊤ ∨ none = 1 ∧ q = ⊤ ∨ none = ⊤ ∧ q = 1
Tactic:
simpa [inv_eq_iff_eq_inv] using h
State after:
no goals

State before:
case some
q : ℝ≥0∞
p : ℝ≥0
h : (some p)⁻¹ + q⁻¹ = 1
⊢ some p ≠ ⊤ ∧ q ≠ ⊤ ∨ some p = 1 ∧ q = ⊤ ∨ some p = ⊤ ∧ q = 1
Tactic:
cases q with
| none =>
  simpa [inv_eq_iff_eq_inv] using h
| some q =>
  simp
State after:
no goals

State before:
case some.none
p : ℝ≥0
h : (some p)⁻¹ + none⁻¹ = 1
⊢ some p ≠ ⊤ ∧ none ≠ ⊤ ∨ some p = 1 ∧ none = ⊤ ∨ some p = ⊤ ∧ none = 1
Tactic:
simpa [inv_eq_iff_eq_inv] using h
State after:
no goals

State before:
case some.some
p q : ℝ≥0
h : (some p)⁻¹ + (some q)⁻¹ = 1
⊢ some p ≠ ⊤ ∧ some q ≠ ⊤ ∨ some p = 1 ∧ some q = ⊤ ∨ some p = ⊤ ∧ some q = 1
Tactic:
simp
State after:
no goals