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

State before:
p q : ℝ≥0∞
h : p⁻¹ + q⁻¹ = 1
⊢ (1 < p ∧ p ≠ ⊤) ∧ 1 < q ∧ q ≠ ⊤ ∨ p = 1 ∧ q = ⊤ ∨ p = ⊤ ∧ q = 1
Tactic:
cases eq_or_lt_of_le (le_top : p ≤ ⊤) with
| inl hp =>
  simp [hp] at h ⊢
  simpa [inv_eq_iff_eq_inv] using h
| inr hp =>
  cases eq_or_lt_of_le (le_top : q ≤ ⊤) with
  | inl hq =>
    simp [hq] at h ⊢
    simpa [inv_eq_iff_eq_inv] using h
  | inr hq =>
    refine Or.inl ?_
    simp [← lt_top_iff_ne_top, hp, hq]
    simp_rw [← ENNReal.inv_lt_one]
    rw [← h]
    rw [lt_top_iff_ne_top] at hp hq
    refine And.intro ?_ ?_
    . refine ENNReal.lt_add_right ?_ ?_
      . rw [← lt_top_iff_ne_top]
        simp
        exact lt_of_lt_of_le zero_lt_one (one_le_of_conjugate h)
      . rwa [ENNReal.inv_ne_zero]
    . rw [add_comm]
      refine ENNReal.lt_add_right ?_ ?_
      . rw [← lt_top_iff_ne_top]
        simp
        exact lt_of_lt_of_le zero_lt_one (one_le_of_conjugate' h)
      . rwa [ENNReal.inv_ne_zero]
State after:
no goals

State before:
case inl
p q : ℝ≥0∞
h : p⁻¹ + q⁻¹ = 1
hp : p = ⊤
⊢ (1 < p ∧ p ≠ ⊤) ∧ 1 < q ∧ q ≠ ⊤ ∨ p = 1 ∧ q = ⊤ ∨ p = ⊤ ∧ q = 1
Tactic:
simp [hp] at h ⊢
State after:
case inl
p q : ℝ≥0∞
hp : p = ⊤
h : q = 1
⊢ q = 1

State before:
case inl
p q : ℝ≥0∞
hp : p = ⊤
h : q = 1
⊢ q = 1
Tactic:
simpa [inv_eq_iff_eq_inv] using h
State after:
no goals

State before:
case inr
p q : ℝ≥0∞
h : p⁻¹ + q⁻¹ = 1
hp : p < ⊤
⊢ (1 < p ∧ p ≠ ⊤) ∧ 1 < q ∧ q ≠ ⊤ ∨ p = 1 ∧ q = ⊤ ∨ p = ⊤ ∧ q = 1
Tactic:
cases eq_or_lt_of_le (le_top : q ≤ ⊤) with
| inl hq =>
  simp [hq] at h ⊢
  simpa [inv_eq_iff_eq_inv] using h
| inr hq =>
  refine Or.inl ?_
  simp [← lt_top_iff_ne_top, hp, hq]
  simp_rw [← ENNReal.inv_lt_one]
  rw [← h]
  rw [lt_top_iff_ne_top] at hp hq
  refine And.intro ?_ ?_
  . refine ENNReal.lt_add_right ?_ ?_
    . rw [← lt_top_iff_ne_top]
      simp
      exact lt_of_lt_of_le zero_lt_one (one_le_of_conjugate h)
    . rwa [ENNReal.inv_ne_zero]
  . rw [add_comm]
    refine ENNReal.lt_add_right ?_ ?_
    . rw [← lt_top_iff_ne_top]
      simp
      exact lt_of_lt_of_le zero_lt_one (one_le_of_conjugate' h)
    . rwa [ENNReal.inv_ne_zero]
State after:
no goals

State before:
case inr.inl
p q : ℝ≥0∞
h : p⁻¹ + q⁻¹ = 1
hp : p < ⊤
hq : q = ⊤
⊢ (1 < p ∧ p ≠ ⊤) ∧ 1 < q ∧ q ≠ ⊤ ∨ p = 1 ∧ q = ⊤ ∨ p = ⊤ ∧ q = 1
Tactic:
simp [hq] at h ⊢
State after:
case inr.inl
p q : ℝ≥0∞
hp : p < ⊤
hq : q = ⊤
h : p = 1
⊢ p = 1

State before:
case inr.inl
p q : ℝ≥0∞
hp : p < ⊤
hq : q = ⊤
h : p = 1
⊢ p = 1
Tactic:
simpa [inv_eq_iff_eq_inv] using h
State after:
no goals

State before:
case inr.inr
p q : ℝ≥0∞
h : p⁻¹ + q⁻¹ = 1
hp : p < ⊤
hq : q < ⊤
⊢ (1 < p ∧ p ≠ ⊤) ∧ 1 < q ∧ q ≠ ⊤ ∨ p = 1 ∧ q = ⊤ ∨ p = ⊤ ∧ q = 1
Tactic:
refine Or.inl ?_
State after:
case inr.inr
p q : ℝ≥0∞
h : p⁻¹ + q⁻¹ = 1
hp : p < ⊤
hq : q < ⊤
⊢ (1 < p ∧ p ≠ ⊤) ∧ 1 < q ∧ q ≠ ⊤

State before:
case inr.inr
p q : ℝ≥0∞
h : p⁻¹ + q⁻¹ = 1
hp : p < ⊤
hq : q < ⊤
⊢ (1 < p ∧ p ≠ ⊤) ∧ 1 < q ∧ q ≠ ⊤
Tactic:
simp [← lt_top_iff_ne_top, hp, hq]
State after:
case inr.inr
p q : ℝ≥0∞
h : p⁻¹ + q⁻¹ = 1
hp : p < ⊤
hq : q < ⊤
⊢ 1 < p ∧ 1 < q

State before:
case inr.inr
p q : ℝ≥0∞
h : p⁻¹ + q⁻¹ = 1
hp : p < ⊤
hq : q < ⊤
⊢ 1 < p ∧ 1 < q
Tactic:
simp_rw [← ENNReal.inv_lt_one]
State after:
case inr.inr
p q : ℝ≥0∞
h : p⁻¹ + q⁻¹ = 1
hp : p < ⊤
hq : q < ⊤
⊢ p⁻¹ < 1 ∧ q⁻¹ < 1

State before:
case inr.inr
p q : ℝ≥0∞
h : p⁻¹ + q⁻¹ = 1
hp : p < ⊤
hq : q < ⊤
⊢ p⁻¹ < 1 ∧ q⁻¹ < 1
Tactic:
rw [← h]
State after:
case inr.inr
p q : ℝ≥0∞
h : p⁻¹ + q⁻¹ = 1
hp : p < ⊤
hq : q < ⊤
⊢ p⁻¹ < p⁻¹ + q⁻¹ ∧ q⁻¹ < p⁻¹ + q⁻¹

State before:
case inr.inr
p q : ℝ≥0∞
h : p⁻¹ + q⁻¹ = 1
hp : p < ⊤
hq : q < ⊤
⊢ p⁻¹ < p⁻¹ + q⁻¹ ∧ q⁻¹ < p⁻¹ + q⁻¹
Tactic:
rw [lt_top_iff_ne_top] at hp hq
State after:
case inr.inr
p q : ℝ≥0∞
h : p⁻¹ + q⁻¹ = 1
hp : p ≠ ⊤
hq : q ≠ ⊤
⊢ p⁻¹ < p⁻¹ + q⁻¹ ∧ q⁻¹ < p⁻¹ + q⁻¹

State before:
case inr.inr
p q : ℝ≥0∞
h : p⁻¹ + q⁻¹ = 1
hp : p ≠ ⊤
hq : q ≠ ⊤
⊢ p⁻¹ < p⁻¹ + q⁻¹ ∧ q⁻¹ < p⁻¹ + q⁻¹
Tactic:
refine And.intro ?_ ?_
State after:
case inr.inr.refine_1
p q : ℝ≥0∞
h : p⁻¹ + q⁻¹ = 1
hp : p ≠ ⊤
hq : q ≠ ⊤
⊢ p⁻¹ < p⁻¹ + q⁻¹

case inr.inr.refine_2
p q : ℝ≥0∞
h : p⁻¹ + q⁻¹ = 1
hp : p ≠ ⊤
hq : q ≠ ⊤
⊢ q⁻¹ < p⁻¹ + q⁻¹

State before:
case inr.inr.refine_1
p q : ℝ≥0∞
h : p⁻¹ + q⁻¹ = 1
hp : p ≠ ⊤
hq : q ≠ ⊤
⊢ p⁻¹ < p⁻¹ + q⁻¹

case inr.inr.refine_2
p q : ℝ≥0∞
h : p⁻¹ + q⁻¹ = 1
hp : p ≠ ⊤
hq : q ≠ ⊤
⊢ q⁻¹ < p⁻¹ + q⁻¹
Tactic:
. refine ENNReal.lt_add_right ?_ ?_
  . rw [← lt_top_iff_ne_top]
    simp
    exact lt_of_lt_of_le zero_lt_one (one_le_of_conjugate h)
  . rwa [ENNReal.inv_ne_zero]
State after:
case inr.inr.refine_2
p q : ℝ≥0∞
h : p⁻¹ + q⁻¹ = 1
hp : p ≠ ⊤
hq : q ≠ ⊤
⊢ q⁻¹ < p⁻¹ + q⁻¹

State before:
case inr.inr.refine_2
p q : ℝ≥0∞
h : p⁻¹ + q⁻¹ = 1
hp : p ≠ ⊤
hq : q ≠ ⊤
⊢ q⁻¹ < p⁻¹ + q⁻¹
Tactic:
. rw [add_comm]
  refine ENNReal.lt_add_right ?_ ?_
  . rw [← lt_top_iff_ne_top]
    simp
    exact lt_of_lt_of_le zero_lt_one (one_le_of_conjugate' h)
  . rwa [ENNReal.inv_ne_zero]
State after:
no goals

State before:
case inr.inr.refine_1
p q : ℝ≥0∞
h : p⁻¹ + q⁻¹ = 1
hp : p ≠ ⊤
hq : q ≠ ⊤
⊢ p⁻¹ < p⁻¹ + q⁻¹
Tactic:
refine ENNReal.lt_add_right ?_ ?_
State after:
case inr.inr.refine_1.refine_1
p q : ℝ≥0∞
h : p⁻¹ + q⁻¹ = 1
hp : p ≠ ⊤
hq : q ≠ ⊤
⊢ p⁻¹ ≠ ⊤

case inr.inr.refine_1.refine_2
p q : ℝ≥0∞
h : p⁻¹ + q⁻¹ = 1
hp : p ≠ ⊤
hq : q ≠ ⊤
⊢ q⁻¹ ≠ 0

State before:
case inr.inr.refine_1.refine_1
p q : ℝ≥0∞
h : p⁻¹ + q⁻¹ = 1
hp : p ≠ ⊤
hq : q ≠ ⊤
⊢ p⁻¹ ≠ ⊤

case inr.inr.refine_1.refine_2
p q : ℝ≥0∞
h : p⁻¹ + q⁻¹ = 1
hp : p ≠ ⊤
hq : q ≠ ⊤
⊢ q⁻¹ ≠ 0
Tactic:
. rw [← lt_top_iff_ne_top]
  simp
  exact lt_of_lt_of_le zero_lt_one (one_le_of_conjugate h)
State after:
case inr.inr.refine_1.refine_2
p q : ℝ≥0∞
h : p⁻¹ + q⁻¹ = 1
hp : p ≠ ⊤
hq : q ≠ ⊤
⊢ q⁻¹ ≠ 0

State before:
case inr.inr.refine_1.refine_2
p q : ℝ≥0∞
h : p⁻¹ + q⁻¹ = 1
hp : p ≠ ⊤
hq : q ≠ ⊤
⊢ q⁻¹ ≠ 0
Tactic:
. rwa [ENNReal.inv_ne_zero]
State after:
no goals

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

State before:
case inr.inr.refine_1.refine_1
p q : ℝ≥0∞
h : p⁻¹ + q⁻¹ = 1
hp : p ≠ ⊤
hq : q ≠ ⊤
⊢ p⁻¹ < ⊤
Tactic:
simp
State after:
case inr.inr.refine_1.refine_1
p q : ℝ≥0∞
h : p⁻¹ + q⁻¹ = 1
hp : p ≠ ⊤
hq : q ≠ ⊤
⊢ 0 < p

State before:
case inr.inr.refine_1.refine_1
p q : ℝ≥0∞
h : p⁻¹ + q⁻¹ = 1
hp : p ≠ ⊤
hq : q ≠ ⊤
⊢ 0 < p
Tactic:
exact lt_of_lt_of_le zero_lt_one (one_le_of_conjugate h)
State after:
no goals

State before:
case inr.inr.refine_1.refine_2
p q : ℝ≥0∞
h : p⁻¹ + q⁻¹ = 1
hp : p ≠ ⊤
hq : q ≠ ⊤
⊢ q⁻¹ ≠ 0
Tactic:
rwa [ENNReal.inv_ne_zero]
State after:
no goals

State before:
case inr.inr.refine_2
p q : ℝ≥0∞
h : p⁻¹ + q⁻¹ = 1
hp : p ≠ ⊤
hq : q ≠ ⊤
⊢ q⁻¹ < p⁻¹ + q⁻¹
Tactic:
rw [add_comm]
State after:
case inr.inr.refine_2
p q : ℝ≥0∞
h : p⁻¹ + q⁻¹ = 1
hp : p ≠ ⊤
hq : q ≠ ⊤
⊢ q⁻¹ < q⁻¹ + p⁻¹

State before:
case inr.inr.refine_2
p q : ℝ≥0∞
h : p⁻¹ + q⁻¹ = 1
hp : p ≠ ⊤
hq : q ≠ ⊤
⊢ q⁻¹ < q⁻¹ + p⁻¹
Tactic:
refine ENNReal.lt_add_right ?_ ?_
State after:
case inr.inr.refine_2.refine_1
p q : ℝ≥0∞
h : p⁻¹ + q⁻¹ = 1
hp : p ≠ ⊤
hq : q ≠ ⊤
⊢ q⁻¹ ≠ ⊤

case inr.inr.refine_2.refine_2
p q : ℝ≥0∞
h : p⁻¹ + q⁻¹ = 1
hp : p ≠ ⊤
hq : q ≠ ⊤
⊢ p⁻¹ ≠ 0

State before:
case inr.inr.refine_2.refine_1
p q : ℝ≥0∞
h : p⁻¹ + q⁻¹ = 1
hp : p ≠ ⊤
hq : q ≠ ⊤
⊢ q⁻¹ ≠ ⊤

case inr.inr.refine_2.refine_2
p q : ℝ≥0∞
h : p⁻¹ + q⁻¹ = 1
hp : p ≠ ⊤
hq : q ≠ ⊤
⊢ p⁻¹ ≠ 0
Tactic:
. rw [← lt_top_iff_ne_top]
  simp
  exact lt_of_lt_of_le zero_lt_one (one_le_of_conjugate' h)
State after:
case inr.inr.refine_2.refine_2
p q : ℝ≥0∞
h : p⁻¹ + q⁻¹ = 1
hp : p ≠ ⊤
hq : q ≠ ⊤
⊢ p⁻¹ ≠ 0

State before:
case inr.inr.refine_2.refine_2
p q : ℝ≥0∞
h : p⁻¹ + q⁻¹ = 1
hp : p ≠ ⊤
hq : q ≠ ⊤
⊢ p⁻¹ ≠ 0
Tactic:
. rwa [ENNReal.inv_ne_zero]
State after:
no goals

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

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

State before:
case inr.inr.refine_2.refine_1
p q : ℝ≥0∞
h : p⁻¹ + q⁻¹ = 1
hp : p ≠ ⊤
hq : q ≠ ⊤
⊢ 0 < q
Tactic:
exact lt_of_lt_of_le zero_lt_one (one_le_of_conjugate' h)
State after:
no goals

State before:
case inr.inr.refine_2.refine_2
p q : ℝ≥0∞
h : p⁻¹ + q⁻¹ = 1
hp : p ≠ ⊤
hq : q ≠ ⊤
⊢ p⁻¹ ≠ 0
Tactic:
rwa [ENNReal.inv_ne_zero]
State after:
no goals