internlm/Lean-Github huggingface dataset:
Theorem: exists_mul_eq_intervalIntegral
Proof state before:
case refine_2
a b : ℝ
hab : a ≤ b
f g : ℝ → ℝ
μ : Measure ℝ
inst✝¹ : NoAtoms μ
inst✝ : IsLocallyFiniteMeasure μ
hf_cont : ContinuousOn f (Set.Icc a b)
hg_int : IntervalIntegrable g μ a b
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ (Set.Icc a b)] g
h_int : IntervalIntegrable (fun x => f x * g x) μ a b
⊢ IntegrableOn (fun x => f x * g x) (Set.Ioc a b)
Tactic:
exact h_int.left
Proof state after:
no goals
Theorem: exists_mul_eq_intervalIntegral_of_continuousOn
Proof state before:
a b : ℝ
hab : a ≤ b
f g : ℝ → ℝ
μ : Measure ℝ
inst✝¹ : NoAtoms μ
inst✝ : IsLocallyFiniteMeasure μ
hf_cont : ContinuousOn f (Set.Icc a b)
hg_cont : ContinuousOn g (Set.Icc a b)
hg_nonneg : ∀ x ∈ Set.Icc a b, 0 ≤ g x
⊢ ∃ c ∈ Set.Icc a b, ∫ (x : ℝ) in a..b, f x * g x ∂μ = f c * ∫ (x : ℝ) in a..b, g x ∂μ
Tactic:
simp only [intervalIntegral.integral_of_le hab]
Proof state after:
a b : ℝ
hab : a ≤ b
f g : ℝ → ℝ
μ : Measure ℝ
inst✝¹ : NoAtoms μ
inst✝ : IsLocallyFiniteMeasure μ
hf_cont : ContinuousOn f (Set.Icc a b)
hg_cont : ContinuousOn g (Set.Icc a b)
hg_nonneg : ∀ x ∈ Set.Icc a b, 0 ≤ g x
⊢ ∃ c ∈ Set.Icc a b, ∫ (x : ℝ) in Set.Ioc a b, f x * g x ∂μ = f c * ∫ (x : ℝ) in Set.Ioc a b, g x ∂μ
Theorem: exists_mul_eq_intervalIntegral_of_continuousOn
Proof state before:
a b : ℝ
hab : a ≤ b
f g : ℝ → ℝ
μ : Measure ℝ
inst✝¹ : NoAtoms μ
inst✝ : IsLocallyFiniteMeasure μ
hf_cont : ContinuousOn f (Set.Icc a b)
hg_cont : ContinuousOn g (Set.Icc a b)
hg_nonneg : ∀ x ∈ Set.Icc a b, 0 ≤ g x
⊢ ∃ c ∈ Set.Icc a b, ∫ (x : ℝ) in Set.Ioc a b, f x * g x ∂μ = f c * ∫ (x : ℝ) in Set.Ioc a b, g x ∂μ
Tactic:
simp only [← integral_Icc_eq_integral_Ioc]
Proof state after:
a b : ℝ
hab : a ≤ b
f g : ℝ → ℝ
μ : Measure ℝ
inst✝¹ : NoAtoms μ
inst✝ : IsLocallyFiniteMeasure μ
hf_cont : ContinuousOn f (Set.Icc a b)
hg_cont : ContinuousOn g (Set.Icc a b)
hg_nonneg : ∀ x ∈ Set.Icc a b, 0 ≤ g x
⊢ ∃ c ∈ Set.Icc a b, ∫ (x : ℝ) in Set.Icc a b, f x * g x ∂μ = f c * ∫ (x : ℝ) in Set.Icc a b, g x ∂μ
Theorem: exists_mul_eq_intervalIntegral_of_continuousOn
Proof state before:
a b : ℝ
hab : a ≤ b
f g : ℝ → ℝ
μ : Measure ℝ
inst✝¹ : NoAtoms μ
inst✝ : IsLocallyFiniteMeasure μ
hf_cont : ContinuousOn f (Set.Icc a b)
hg_cont : ContinuousOn g (Set.Icc a b)
hg_nonneg : ∀ x ∈ Set.Icc a b, 0 ≤ g x
⊢ ∃ c ∈ Set.Icc a b, ∫ (x : ℝ) in Set.Icc a b, f x * g x ∂μ = f c * ∫ (x : ℝ) in Set.Icc a b, g x ∂μ
Tactic:
exact exists_mul_eq_setInterval_Icc_of_continuousOn hab hf_cont hg_cont hg_nonneg
Proof state after:
no goals
Theorem: ENNReal.one_le_conjExponent
Proof state before:
p q : ℝ≥0∞
⊢ 1 ≤ conjExponent p
Tactic:
simp [conjExponent]
Proof state after:
no goals
Theorem: ENNReal.sub_right_eq_self
Proof state before:
p q a b : ℝ≥0∞
ha : a ≠ 0
ha' : a ≠ ⊤
⊢ a - b = a ↔ b = 0
Tactic:
refine Iff.intro ?_ ?_
Proof state after:
case refine_1
p q a b : ℝ≥0∞
ha : a ≠ 0
ha' : a ≠ ⊤
⊢ a - b = a → b = 0

case refine_2
p q a b : ℝ≥0∞
ha : a ≠ 0
ha' : a ≠ ⊤
⊢ b = 0 → a - b = a
Theorem: ENNReal.sub_right_eq_self
Proof state before:
case refine_1
p q a b : ℝ≥0∞
ha : a ≠ 0
ha' : a ≠ ⊤
⊢ a - b = a → b = 0

case refine_2
p q a b : ℝ≥0∞
ha : a ≠ 0
ha' : a ≠ ⊤
⊢ b = 0 → a - b = a
Tactic:
. intro h
  suffices hba : b ≤ a
  . simpa [← ENNReal.sub_right_inj ha' hba]
  have hba : 0 < a - b
  . simpa [h, zero_lt_iff]
  simp at hba
  exact hba.le
Proof state after:
case refine_2
p q a b : ℝ≥0∞
ha : a ≠ 0
ha' : a ≠ ⊤
⊢ b = 0 → a - b = a
Theorem: ENNReal.sub_right_eq_self
Proof state before:
case refine_2
p q a b : ℝ≥0∞
ha : a ≠ 0
ha' : a ≠ ⊤
⊢ b = 0 → a - b = a
Tactic:
. intro h
  simp [h]
Proof state after:
no goals
Theorem: ENNReal.sub_right_eq_self
Proof state before:
case refine_1
p q a b : ℝ≥0∞
ha : a ≠ 0
ha' : a ≠ ⊤
⊢ a - b = a → b = 0
Tactic:
intro h
Proof state after:
case refine_1
p q a b : ℝ≥0∞
ha : a ≠ 0
ha' : a ≠ ⊤
h : a - b = a
⊢ b = 0
Theorem: ENNReal.sub_right_eq_self
Proof state before:
case refine_1
p q a b : ℝ≥0∞
ha : a ≠ 0
ha' : a ≠ ⊤
h : a - b = a
⊢ b = 0
Tactic:
suffices hba : b ≤ a
Proof state after:
case refine_1
p q a b : ℝ≥0∞
ha : a ≠ 0
ha' : a ≠ ⊤
h : a - b = a
hba : b ≤ a
⊢ b = 0

case hba
p q a b : ℝ≥0∞
ha : a ≠ 0
ha' : a ≠ ⊤
h : a - b = a
⊢ b ≤ a
Theorem: ENNReal.sub_right_eq_self
Proof state before:
case refine_1
p q a b : ℝ≥0∞
ha : a ≠ 0
ha' : a ≠ ⊤
h : a - b = a
hba : b ≤ a
⊢ b = 0

case hba
p q a b : ℝ≥0∞
ha : a ≠ 0
ha' : a ≠ ⊤
h : a - b = a
⊢ b ≤ a
Tactic:
. simpa [← ENNReal.sub_right_inj ha' hba]
Proof state after:
case hba
p q a b : ℝ≥0∞
ha : a ≠ 0
ha' : a ≠ ⊤
h : a - b = a
⊢ b ≤ a
Theorem: ENNReal.sub_right_eq_self
Proof state before:
case hba
p q a b : ℝ≥0∞
ha : a ≠ 0
ha' : a ≠ ⊤
h : a - b = a
⊢ b ≤ a
Tactic:
have hba : 0 < a - b
Proof state after:
case hba
p q a b : ℝ≥0∞
ha : a ≠ 0
ha' : a ≠ ⊤
h : a - b = a
⊢ 0 < a - b

case hba
p q a b : ℝ≥0∞
ha : a ≠ 0
ha' : a ≠ ⊤
h : a - b = a
hba : 0 < a - b
⊢ b ≤ a
Theorem: ENNReal.sub_right_eq_self
Proof state before:
case hba
p q a b : ℝ≥0∞
ha : a ≠ 0
ha' : a ≠ ⊤
h : a - b = a
⊢ 0 < a - b

case hba
p q a b : ℝ≥0∞
ha : a ≠ 0
ha' : a ≠ ⊤
h : a - b = a
hba : 0 < a - b
⊢ b ≤ a
Tactic:
. simpa [h, zero_lt_iff]
Proof state after:
case hba
p q a b : ℝ≥0∞
ha : a ≠ 0
ha' : a ≠ ⊤
h : a - b = a
hba : 0 < a - b
⊢ b ≤ a
Theorem: ENNReal.sub_right_eq_self
Proof state before:
case hba
p q a b : ℝ≥0∞
ha : a ≠ 0
ha' : a ≠ ⊤
h : a - b = a
hba : 0 < a - b
⊢ b ≤ a
Tactic:
simp at hba
Proof state after:
case hba
p q a b : ℝ≥0∞
ha : a ≠ 0
ha' : a ≠ ⊤
h : a - b = a
hba : b < a
⊢ b ≤ a
Theorem: ENNReal.sub_right_eq_self
Proof state before:
case hba
p q a b : ℝ≥0∞
ha : a ≠ 0
ha' : a ≠ ⊤
h : a - b = a
hba : b < a
⊢ b ≤ a
Tactic:
exact hba.le
Proof state after:
no goals
Theorem: ENNReal.sub_right_eq_self
Proof state before:
case refine_1
p q a b : ℝ≥0∞
ha : a ≠ 0
ha' : a ≠ ⊤
h : a - b = a
hba : b ≤ a
⊢ b = 0
Tactic:
simpa [← ENNReal.sub_right_inj ha' hba]
Proof state after:
no goals
Theorem: ENNReal.sub_right_eq_self
Proof state before:
case hba
p q a b : ℝ≥0∞
ha : a ≠ 0
ha' : a ≠ ⊤
h : a - b = a
⊢ 0 < a - b
Tactic:
simpa [h, zero_lt_iff]
Proof state after:
no goals
Theorem: ENNReal.sub_right_eq_self
Proof state before:
case refine_2
p q a b : ℝ≥0∞
ha : a ≠ 0
ha' : a ≠ ⊤
⊢ b = 0 → a - b = a
Tactic:
intro h
Proof state after:
case refine_2
p q a b : ℝ≥0∞
ha : a ≠ 0
ha' : a ≠ ⊤
h : b = 0
⊢ a - b = a
Theorem: ENNReal.sub_right_eq_self
Proof state before:
case refine_2
p q a b : ℝ≥0∞
ha : a ≠ 0
ha' : a ≠ ⊤
h : b = 0
⊢ a - b = a
Tactic:
simp [h]
Proof state after:
no goals
Theorem: ENNReal.conjExponent_eq_one
Proof state before:
p q : ℝ≥0∞
⊢ conjExponent p = 1 ↔ p = ⊤
Tactic:
simp [conjExponent, inv_eq_iff_eq_inv]
Proof state after:
no goals
Theorem: ENNReal.conjExponent_eq_top
Proof state before:
p q : ℝ≥0∞
hp : 1 ≤ p
⊢ conjExponent p = ⊤ ↔ p = 1
Tactic:
rw [conjExponent, inv_eq_top, tsub_eq_zero_iff_le, ENNReal.one_le_inv]
Proof state after:
p q : ℝ≥0∞
hp : 1 ≤ p
⊢ p ≤ 1 ↔ p = 1
Theorem: ENNReal.conjExponent_eq_top
Proof state before:
p q : ℝ≥0∞
hp : 1 ≤ p
⊢ p ≤ 1 ↔ p = 1
Tactic:
exact LE.le.le_iff_eq hp
Proof state after:
no goals
Theorem: ENNReal.one_le_of_conjugate
Proof state before:
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
⊢ 1 ≤ p
Tactic:
rw [← ENNReal.inv_le_inv, inv_one]
Proof state after:
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
⊢ p⁻¹ ≤ 1
Theorem: ENNReal.one_le_of_conjugate
Proof state before:
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
⊢ p⁻¹ ≤ 1
Tactic:
simp [← hpq]
Proof state after:
no goals
Theorem: ENNReal.one_le_of_conjugate'
Proof state before:
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
⊢ 1 ≤ q
Tactic:
rw [add_comm] at hpq
Proof state after:
p q : ℝ≥0∞
hpq : q⁻¹ + p⁻¹ = 1
⊢ 1 ≤ q
Theorem: ENNReal.one_le_of_conjugate'
Proof state before:
p q : ℝ≥0∞
hpq : q⁻¹ + p⁻¹ = 1
⊢ 1 ≤ q
Tactic:
exact one_le_of_conjugate hpq
Proof state after:
no goals
Theorem: ENNReal.conjugate_iff
Proof state before:
p q : ℝ≥0∞
⊢ 1 ≤ p ∧ q = conjExponent p ↔ p⁻¹ + q⁻¹ = 1
Tactic:
rw [conjExponent]
Proof state after:
p q : ℝ≥0∞
⊢ 1 ≤ p ∧ q = (1 - p⁻¹)⁻¹ ↔ p⁻¹ + q⁻¹ = 1
Theorem: ENNReal.conjugate_iff
Proof state before:
p q : ℝ≥0∞
⊢ 1 ≤ p ∧ q = (1 - p⁻¹)⁻¹ ↔ p⁻¹ + q⁻¹ = 1
Tactic:
rw [← inv_eq_iff_eq_inv]
Proof state after:
p q : ℝ≥0∞
⊢ 1 ≤ p ∧ q⁻¹ = 1 - p⁻¹ ↔ p⁻¹ + q⁻¹ = 1
Theorem: ENNReal.conjugate_iff
Proof state before:
p q : ℝ≥0∞
⊢ 1 ≤ p ∧ q⁻¹ = 1 - p⁻¹ ↔ p⁻¹ + q⁻¹ = 1
Tactic:
refine Iff.intro ?_ ?_
Proof 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⁻¹
Theorem: ENNReal.conjugate_iff
Proof 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
Proof state after:
case refine_2
p q : ℝ≥0∞
⊢ p⁻¹ + q⁻¹ = 1 → 1 ≤ p ∧ q⁻¹ = 1 - p⁻¹
Theorem: ENNReal.conjugate_iff
Proof 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
Proof state after:
no goals
Theorem: ENNReal.conjugate_iff
Proof state before:
case refine_1
p q : ℝ≥0∞
⊢ 1 ≤ p ∧ q⁻¹ = 1 - p⁻¹ → p⁻¹ + q⁻¹ = 1
Tactic:
simp
Proof state after:
case refine_1
p q : ℝ≥0∞
⊢ 1 ≤ p → q⁻¹ = 1 - p⁻¹ → p⁻¹ + q⁻¹ = 1
Theorem: ENNReal.conjugate_iff
Proof state before:
case refine_1
p q : ℝ≥0∞
⊢ 1 ≤ p → q⁻¹ = 1 - p⁻¹ → p⁻¹ + q⁻¹ = 1
Tactic:
intro hp h
Proof state after:
case refine_1
p q : ℝ≥0∞
hp : 1 ≤ p
h : q⁻¹ = 1 - p⁻¹
⊢ p⁻¹ + q⁻¹ = 1
Theorem: ENNReal.conjugate_iff
Proof state before:
case refine_1
p q : ℝ≥0∞
hp : 1 ≤ p
h : q⁻¹ = 1 - p⁻¹
⊢ p⁻¹ + q⁻¹ = 1
Tactic:
rw [h]
Proof state after:
case refine_1
p q : ℝ≥0∞
hp : 1 ≤ p
h : q⁻¹ = 1 - p⁻¹
⊢ p⁻¹ + (1 - p⁻¹) = 1
Theorem: ENNReal.conjugate_iff
Proof 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]
Proof state after:
case refine_1
p q : ℝ≥0∞
hp : 1 ≤ p
h : q⁻¹ = 1 - p⁻¹
⊢ p⁻¹ ≤ 1
Theorem: ENNReal.conjugate_iff
Proof state before:
case refine_1
p q : ℝ≥0∞
hp : 1 ≤ p
h : q⁻¹ = 1 - p⁻¹
⊢ p⁻¹ ≤ 1
Tactic:
simp
Proof state after:
case refine_1
p q : ℝ≥0∞
hp : 1 ≤ p
h : q⁻¹ = 1 - p⁻¹
⊢ 1 ≤ p
Theorem: ENNReal.conjugate_iff
Proof state before:
case refine_1
p q : ℝ≥0∞
hp : 1 ≤ p
h : q⁻¹ = 1 - p⁻¹
⊢ 1 ≤ p
Tactic:
exact hp
Proof state after:
no goals
Theorem: ENNReal.conjugate_iff
Proof state before:
case refine_2
p q : ℝ≥0∞
⊢ p⁻¹ + q⁻¹ = 1 → 1 ≤ p ∧ q⁻¹ = 1 - p⁻¹
Tactic:
intro h
Proof state after:
case refine_2
p q : ℝ≥0∞
h : p⁻¹ + q⁻¹ = 1
⊢ 1 ≤ p ∧ q⁻¹ = 1 - p⁻¹
Theorem: ENNReal.conjugate_iff
Proof 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
Proof state after:
case refine_2
p q : ℝ≥0∞
h : p⁻¹ + q⁻¹ = 1
hp : 1 ≤ p
⊢ 1 ≤ p ∧ q⁻¹ = 1 - p⁻¹
Theorem: ENNReal.conjugate_iff
Proof 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 ?_
Proof state after:
case refine_2
p q : ℝ≥0∞
h : p⁻¹ + q⁻¹ = 1
hp : 1 ≤ p
⊢ q⁻¹ = 1 - p⁻¹
Theorem: ENNReal.conjugate_iff
Proof state before:
case refine_2
p q : ℝ≥0∞
h : p⁻¹ + q⁻¹ = 1
hp : 1 ≤ p
⊢ q⁻¹ = 1 - p⁻¹
Tactic:
rw [← h]
Proof state after:
case refine_2
p q : ℝ≥0∞
h : p⁻¹ + q⁻¹ = 1
hp : 1 ≤ p
⊢ q⁻¹ = p⁻¹ + q⁻¹ - p⁻¹
Theorem: ENNReal.conjugate_iff
Proof 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]
Proof state after:
case refine_2
p q : ℝ≥0∞
h : p⁻¹ + q⁻¹ = 1
hp : 1 ≤ p
⊢ p⁻¹ ≠ ⊤
Theorem: ENNReal.conjugate_iff
Proof state before:
case refine_2
p q : ℝ≥0∞
h : p⁻¹ + q⁻¹ = 1
hp : 1 ≤ p
⊢ p⁻¹ ≠ ⊤
Tactic:
rw [← lt_top_iff_ne_top]
Proof state after:
case refine_2
p q : ℝ≥0∞
h : p⁻¹ + q⁻¹ = 1
hp : 1 ≤ p
⊢ p⁻¹ < ⊤
Theorem: ENNReal.conjugate_iff
Proof state before:
case refine_2
p q : ℝ≥0∞
h : p⁻¹ + q⁻¹ = 1
hp : 1 ≤ p
⊢ p⁻¹ < ⊤
Tactic:
simp
Proof state after:
case refine_2
p q : ℝ≥0∞
h : p⁻¹ + q⁻¹ = 1
hp : 1 ≤ p
⊢ 0 < p
Theorem: ENNReal.conjugate_iff
Proof 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
Proof state after:
no goals
Theorem: ENNReal.conjugate_conjExponent
Proof state before:
p q : ℝ≥0∞
hp : 1 ≤ p
⊢ p⁻¹ + (conjExponent p)⁻¹ = 1
Tactic:
simp [conjExponent]
Proof state after:
p q : ℝ≥0∞
hp : 1 ≤ p
⊢ p⁻¹ + (1 - p⁻¹) = 1
Theorem: ENNReal.conjugate_conjExponent
Proof state before:
p q : ℝ≥0∞
hp : 1 ≤ p
⊢ p⁻¹ + (1 - p⁻¹) = 1
Tactic:
simp [add_tsub_cancel_iff_le]
Proof state after:
p q : ℝ≥0∞
hp : 1 ≤ p
⊢ 1 ≤ p
Theorem: ENNReal.conjugate_conjExponent
Proof state before:
p q : ℝ≥0∞
hp : 1 ≤ p
⊢ 1 ≤ p
Tactic:
exact hp
Proof state after:
no goals
Theorem: ENNReal.conjugate_cases'
Proof 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
Proof state after:
no goals
Theorem: ENNReal.conjugate_cases'
Proof 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
Proof state after:
no goals
Theorem: ENNReal.conjugate_cases'
Proof 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
Proof state after:
no goals
Theorem: ENNReal.conjugate_cases'
Proof 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
Proof state after:
no goals
Theorem: ENNReal.conjugate_cases'
Proof 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
Proof state after:
no goals
Theorem: ENNReal.conjugate_cases
Proof 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]
Proof state after:
no goals
Theorem: ENNReal.conjugate_cases
Proof 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 ⊢
Proof state after:
case inl
p q : ℝ≥0∞
hp : p = ⊤
h : q = 1
⊢ q = 1
Theorem: ENNReal.conjugate_cases
Proof state before:
case inl
p q : ℝ≥0∞
hp : p = ⊤
h : q = 1
⊢ q = 1
Tactic:
simpa [inv_eq_iff_eq_inv] using h
Proof state after:
no goals
Theorem: ENNReal.conjugate_cases
Proof 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]
Proof state after:
no goals
Theorem: ENNReal.conjugate_cases
Proof 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 ⊢
Proof state after:
case inr.inl
p q : ℝ≥0∞
hp : p < ⊤
hq : q = ⊤
h : p = 1
⊢ p = 1
Theorem: ENNReal.conjugate_cases
Proof 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
Proof state after:
no goals
Theorem: ENNReal.conjugate_cases
Proof 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 ?_
Proof state after:
case inr.inr
p q : ℝ≥0∞
h : p⁻¹ + q⁻¹ = 1
hp : p < ⊤
hq : q < ⊤
⊢ (1 < p ∧ p ≠ ⊤) ∧ 1 < q ∧ q ≠ ⊤
Theorem: ENNReal.conjugate_cases
Proof 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]
Proof state after:
case inr.inr
p q : ℝ≥0∞
h : p⁻¹ + q⁻¹ = 1
hp : p < ⊤
hq : q < ⊤
⊢ 1 < p ∧ 1 < q
Theorem: ENNReal.conjugate_cases
Proof 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]
Proof state after:
case inr.inr
p q : ℝ≥0∞
h : p⁻¹ + q⁻¹ = 1
hp : p < ⊤
hq : q < ⊤
⊢ p⁻¹ < 1 ∧ q⁻¹ < 1
Theorem: ENNReal.conjugate_cases
Proof state before:
case inr.inr
p q : ℝ≥0∞
h : p⁻¹ + q⁻¹ = 1
hp : p < ⊤
hq : q < ⊤
⊢ p⁻¹ < 1 ∧ q⁻¹ < 1
Tactic:
rw [← h]
Proof state after:
case inr.inr
p q : ℝ≥0∞
h : p⁻¹ + q⁻¹ = 1
hp : p < ⊤
hq : q < ⊤
⊢ p⁻¹ < p⁻¹ + q⁻¹ ∧ q⁻¹ < p⁻¹ + q⁻¹
Theorem: ENNReal.conjugate_cases
Proof 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
Proof state after:
case inr.inr
p q : ℝ≥0∞
h : p⁻¹ + q⁻¹ = 1
hp : p ≠ ⊤
hq : q ≠ ⊤
⊢ p⁻¹ < p⁻¹ + q⁻¹ ∧ q⁻¹ < p⁻¹ + q⁻¹
Theorem: ENNReal.conjugate_cases
Proof 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 ?_ ?_
Proof 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⁻¹
Theorem: ENNReal.conjugate_cases
Proof 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]
Proof state after:
case inr.inr.refine_2
p q : ℝ≥0∞
h : p⁻¹ + q⁻¹ = 1
hp : p ≠ ⊤
hq : q ≠ ⊤
⊢ q⁻¹ < p⁻¹ + q⁻¹
Theorem: ENNReal.conjugate_cases
Proof 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]
Proof state after:
no goals
Theorem: ENNReal.conjugate_cases
Proof 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 ?_ ?_
Proof 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
Theorem: ENNReal.conjugate_cases
Proof 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)
Proof state after:
case inr.inr.refine_1.refine_2
p q : ℝ≥0∞
h : p⁻¹ + q⁻¹ = 1
hp : p ≠ ⊤
hq : q ≠ ⊤
⊢ q⁻¹ ≠ 0
Theorem: ENNReal.conjugate_cases
Proof 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]
Proof state after:
no goals
Theorem: ENNReal.conjugate_cases
Proof 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]
Proof state after:
case inr.inr.refine_1.refine_1
p q : ℝ≥0∞
h : p⁻¹ + q⁻¹ = 1
hp : p ≠ ⊤
hq : q ≠ ⊤
⊢ p⁻¹ < ⊤
Theorem: ENNReal.conjugate_cases
Proof state before:
case inr.inr.refine_1.refine_1
p q : ℝ≥0∞
h : p⁻¹ + q⁻¹ = 1
hp : p ≠ ⊤
hq : q ≠ ⊤
⊢ p⁻¹ < ⊤
Tactic:
simp
Proof state after:
case inr.inr.refine_1.refine_1
p q : ℝ≥0∞
h : p⁻¹ + q⁻¹ = 1
hp : p ≠ ⊤
hq : q ≠ ⊤
⊢ 0 < p
Theorem: ENNReal.conjugate_cases
Proof 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)
Proof state after:
no goals
Theorem: ENNReal.conjugate_cases
Proof 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]
Proof state after:
no goals
Theorem: ENNReal.conjugate_cases
Proof 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]
Proof state after:
case inr.inr.refine_2
p q : ℝ≥0∞
h : p⁻¹ + q⁻¹ = 1
hp : p ≠ ⊤
hq : q ≠ ⊤
⊢ q⁻¹ < q⁻¹ + p⁻¹
Theorem: ENNReal.conjugate_cases
Proof 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 ?_ ?_
Proof 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
Theorem: ENNReal.conjugate_cases
Proof 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)
Proof state after:
case inr.inr.refine_2.refine_2
p q : ℝ≥0∞
h : p⁻¹ + q⁻¹ = 1
hp : p ≠ ⊤
hq : q ≠ ⊤
⊢ p⁻¹ ≠ 0
Theorem: ENNReal.conjugate_cases
Proof 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]
Proof state after:
no goals
Theorem: ENNReal.conjugate_cases
Proof 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]
Proof state after:
case inr.inr.refine_2.refine_1
p q : ℝ≥0∞
h : p⁻¹ + q⁻¹ = 1
hp : p ≠ ⊤
hq : q ≠ ⊤
⊢ q⁻¹ < ⊤
Theorem: ENNReal.conjugate_cases
Proof state before:
case inr.inr.refine_2.refine_1
p q : ℝ≥0∞
h : p⁻¹ + q⁻¹ = 1
hp : p ≠ ⊤
hq : q ≠ ⊤
⊢ q⁻¹ < ⊤
Tactic:
simp
Proof state after:
case inr.inr.refine_2.refine_1
p q : ℝ≥0∞
h : p⁻¹ + q⁻¹ = 1
hp : p ≠ ⊤
hq : q ≠ ⊤
⊢ 0 < q
Theorem: ENNReal.conjugate_cases
Proof 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)
Proof state after:
no goals
Theorem: ENNReal.conjugate_cases
Proof 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]
Proof state after:
no goals