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

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

State before:
p q : ℝ≥0∞
⊢ 1 ≤ p ∧ q = (1 - p⁻¹)⁻¹ ↔ p⁻¹ + q⁻¹ = 1
Tactic:
rw [← inv_eq_iff_eq_inv]
State after:
p q : ℝ≥0∞
⊢ 1 ≤ p ∧ q⁻¹ = 1 - p⁻¹ ↔ p⁻¹ + q⁻¹ = 1

State before:
p q : ℝ≥0∞
⊢ 1 ≤ p ∧ q⁻¹ = 1 - p⁻¹ ↔ p⁻¹ + q⁻¹ = 1
Tactic:
refine Iff.intro ?_ ?_
State after:
case refine_1
p q : ℝ≥0∞
⊢ 1 ≤ p ∧ q⁻¹ = 1 - p⁻¹ → p⁻¹ + q⁻¹ = 1

case refine_2
p q : ℝ≥0∞
⊢ p⁻¹ + q⁻¹ = 1 → 1 ≤ p ∧ q⁻¹ = 1 - p⁻¹

State before:
case refine_1
p q : ℝ≥0∞
⊢ 1 ≤ p ∧ q⁻¹ = 1 - p⁻¹ → p⁻¹ + q⁻¹ = 1

case refine_2
p q : ℝ≥0∞
⊢ p⁻¹ + q⁻¹ = 1 → 1 ≤ p ∧ q⁻¹ = 1 - p⁻¹
Tactic:
. simp
  intro hp h
  rw [h]
  rw [add_tsub_cancel_iff_le]
  simp
  exact hp
State after:
case refine_2
p q : ℝ≥0∞
⊢ p⁻¹ + q⁻¹ = 1 → 1 ≤ p ∧ q⁻¹ = 1 - p⁻¹

State before:
case refine_2
p q : ℝ≥0∞
⊢ p⁻¹ + q⁻¹ = 1 → 1 ≤ p ∧ q⁻¹ = 1 - p⁻¹
Tactic:
. intro h
  have hp : 1 ≤ p := one_le_of_conjugate h
  refine And.intro hp ?_
  rw [← h]
  rw [ENNReal.add_sub_cancel_left]
  rw [← lt_top_iff_ne_top]
  simp
  exact lt_of_lt_of_le zero_lt_one hp
State after:
no goals

State before:
case refine_1
p q : ℝ≥0∞
⊢ 1 ≤ p ∧ q⁻¹ = 1 - p⁻¹ → p⁻¹ + q⁻¹ = 1
Tactic:
simp
State after:
case refine_1
p q : ℝ≥0∞
⊢ 1 ≤ p → q⁻¹ = 1 - p⁻¹ → p⁻¹ + q⁻¹ = 1

State before:
case refine_1
p q : ℝ≥0∞
⊢ 1 ≤ p → q⁻¹ = 1 - p⁻¹ → p⁻¹ + q⁻¹ = 1
Tactic:
intro hp h
State after:
case refine_1
p q : ℝ≥0∞
hp : 1 ≤ p
h : q⁻¹ = 1 - p⁻¹
⊢ p⁻¹ + q⁻¹ = 1

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

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

State before:
case refine_1
p q : ℝ≥0∞
hp : 1 ≤ p
h : q⁻¹ = 1 - p⁻¹
⊢ p⁻¹ ≤ 1
Tactic:
simp
State after:
case refine_1
p q : ℝ≥0∞
hp : 1 ≤ p
h : q⁻¹ = 1 - p⁻¹
⊢ 1 ≤ p

State before:
case refine_1
p q : ℝ≥0∞
hp : 1 ≤ p
h : q⁻¹ = 1 - p⁻¹
⊢ 1 ≤ p
Tactic:
exact hp
State after:
no goals

State before:
case refine_2
p q : ℝ≥0∞
⊢ p⁻¹ + q⁻¹ = 1 → 1 ≤ p ∧ q⁻¹ = 1 - p⁻¹
Tactic:
intro h
State after:
case refine_2
p q : ℝ≥0∞
h : p⁻¹ + q⁻¹ = 1
⊢ 1 ≤ p ∧ q⁻¹ = 1 - p⁻¹

State before:
case refine_2
p q : ℝ≥0∞
h : p⁻¹ + q⁻¹ = 1
⊢ 1 ≤ p ∧ q⁻¹ = 1 - p⁻¹
Tactic:
have hp : 1 ≤ p := one_le_of_conjugate h
State after:
case refine_2
p q : ℝ≥0∞
h : p⁻¹ + q⁻¹ = 1
hp : 1 ≤ p
⊢ 1 ≤ p ∧ q⁻¹ = 1 - p⁻¹

State before:
case refine_2
p q : ℝ≥0∞
h : p⁻¹ + q⁻¹ = 1
hp : 1 ≤ p
⊢ 1 ≤ p ∧ q⁻¹ = 1 - p⁻¹
Tactic:
refine And.intro hp ?_
State after:
case refine_2
p q : ℝ≥0∞
h : p⁻¹ + q⁻¹ = 1
hp : 1 ≤ p
⊢ q⁻¹ = 1 - p⁻¹

State before:
case refine_2
p q : ℝ≥0∞
h : p⁻¹ + q⁻¹ = 1
hp : 1 ≤ p
⊢ q⁻¹ = 1 - p⁻¹
Tactic:
rw [← h]
State after:
case refine_2
p q : ℝ≥0∞
h : p⁻¹ + q⁻¹ = 1
hp : 1 ≤ p
⊢ q⁻¹ = p⁻¹ + q⁻¹ - p⁻¹

State before:
case refine_2
p q : ℝ≥0∞
h : p⁻¹ + q⁻¹ = 1
hp : 1 ≤ p
⊢ q⁻¹ = p⁻¹ + q⁻¹ - p⁻¹
Tactic:
rw [ENNReal.add_sub_cancel_left]
State after:
case refine_2
p q : ℝ≥0∞
h : p⁻¹ + q⁻¹ = 1
hp : 1 ≤ p
⊢ p⁻¹ ≠ ⊤

State before:
case refine_2
p q : ℝ≥0∞
h : p⁻¹ + q⁻¹ = 1
hp : 1 ≤ p
⊢ p⁻¹ ≠ ⊤
Tactic:
rw [← lt_top_iff_ne_top]
State after:
case refine_2
p q : ℝ≥0∞
h : p⁻¹ + q⁻¹ = 1
hp : 1 ≤ p
⊢ p⁻¹ < ⊤

State before:
case refine_2
p q : ℝ≥0∞
h : p⁻¹ + q⁻¹ = 1
hp : 1 ≤ p
⊢ p⁻¹ < ⊤
Tactic:
simp
State after:
case refine_2
p q : ℝ≥0∞
h : p⁻¹ + q⁻¹ = 1
hp : 1 ≤ p
⊢ 0 < p

State before:
case refine_2
p q : ℝ≥0∞
h : p⁻¹ + q⁻¹ = 1
hp : 1 ≤ p
⊢ 0 < p
Tactic:
exact lt_of_lt_of_le zero_lt_one hp
State after:
no goals