Theorem: ENNReal.conjugate_conjExponent (ForML/LpHoelder.lean)

State before:
p q : ℝ≥0∞
hp : 1 ≤ p
⊢ p⁻¹ + (conjExponent p)⁻¹ = 1
Tactic:
simp [conjExponent]
State after:
p q : ℝ≥0∞
hp : 1 ≤ p
⊢ p⁻¹ + (1 - p⁻¹) = 1

State before:
p q : ℝ≥0∞
hp : 1 ≤ p
⊢ p⁻¹ + (1 - p⁻¹) = 1
Tactic:
simp [add_tsub_cancel_iff_le]
State after:
p q : ℝ≥0∞
hp : 1 ≤ p
⊢ 1 ≤ p

State before:
p q : ℝ≥0∞
hp : 1 ≤ p
⊢ 1 ≤ p
Tactic:
exact hp
State after:
no goals