awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Real.ConjExponents (hypothesis)
Goal:
p q r : ℝ≥0
hr : r ≠ 0
h : (↑p : ℝ≥0∞).HolderTriple (↑q : ℝ≥0∞) (↑r : ℝ≥0∞)
hp : p ≠ 0
⊢ p⁻¹ + q⁻¹ = r⁻¹ ∧ 0 < p ∧ 0 < q
have hq : q ≠ 0
Tactic: obtain ⟨hp, hq⟩ : p ≠ 0 ∧ q ≠ 0 := by
      constructor
      all_goals
        rintro rfl
        apply hr
        exact_mod_cast (coe_zero ▸ h).unique _ _ r 0
-- Lean 4 proof step from Mathlib.Data.Real.ConjExponents (goal)
Goal:
p q r : ℝ≥0
hr : r ≠ 0
h : p.HolderTriple q r
⊢ (↑p : ℝ≥0∞).HolderTriple (↑q : ℝ≥0∞) (↑r : ℝ≥0∞)
have refine_2 : (↑p : ℝ≥0∞)⁻¹ + (↑q : ℝ≥0∞)⁻¹ = (↑r : ℝ≥0∞)⁻¹
Tactic: rw [holderTriple_iff]
-- Lean 4 proof step from Mathlib.Data.Real.ConjExponents (hypothesis)
Goal:
p q r : ℝ≥0
hr : r ≠ 0
h : p.HolderTriple q r
⊢ (↑p : ℝ≥0∞)⁻¹ + (↑q : ℝ≥0∞)⁻¹ = (↑r : ℝ≥0∞)⁻¹
have hp : p ≠ 0
Tactic: have hp := h.ne_zero
-- Lean 4 proof step from Mathlib.Data.Real.ConjExponents (hypothesis)
Goal:
p q r : ℝ≥0
hr : r ≠ 0
h : p.HolderTriple q r
hp : p ≠ 0
⊢ (↑p : ℝ≥0∞)⁻¹ + (↑q : ℝ≥0∞)⁻¹ = (↑r : ℝ≥0∞)⁻¹
have hq : q ≠ 0
Tactic: have hq := h.symm.ne_zero
-- Lean 4 proof step from Mathlib.Data.Real.ConjExponents (hypothesis)
Goal:
p q r : ℝ≥0∞
h : p.toReal.HolderTriple q.toReal r.toReal
⊢ p.HolderTriple q r
have hp : 0 < p.toReal
Tactic: have hp := h.pos
-- Lean 4 proof step from Mathlib.Data.Real.ConjExponents (hypothesis)
Goal:
p q r : ℝ≥0∞
h : p.toReal.HolderTriple q.toReal r.toReal
hp : 0 < p.toReal
⊢ p.HolderTriple q r
have hq : 0 < q.toReal
Tactic: have hq := h.symm.pos
-- Lean 4 proof step from Mathlib.Data.Real.ConjExponents (hypothesis)
Goal:
p q r : ℝ≥0∞
h : p.toReal.HolderTriple q.toReal r.toReal
hp : 0 < p.toReal
hq : 0 < q.toReal
⊢ p.HolderTriple q r
have hr : 0 < r.toReal
Tactic: have hr := h.pos'
-- Lean 4 proof step from Mathlib.Data.Real.ConjExponents (hypothesis)
Goal:
p q r : ℝ≥0∞
h : p.toReal.HolderTriple q.toReal r.toReal
hp : 0 < p.toReal
hq : 0 < q.toReal
hr : 0 < r.toReal
⊢ p.HolderTriple q r
have hp₁ : 0 < p ∧ p < ∞
Tactic: rw [toReal_pos_iff] at hp hq hr
Cleared hypotheses: hp, hq, hr
-- Lean 4 proof step from Mathlib.Data.Real.ConjExponents (hypothesis)
Goal:
p q r : ℝ≥0∞
h : p.toReal.HolderTriple q.toReal r.toReal
hp : 0 < p.toReal
hq : 0 < q.toReal
hr : 0 < r.toReal
hp₁ : 0 < p ∧ p < ∞
⊢ p.HolderTriple q r
have hq₁ : 0 < q ∧ q < ∞
Tactic: rw [toReal_pos_iff] at hp hq hr
Cleared hypotheses: hp, hq, hr
-- Lean 4 proof step from Mathlib.Data.Real.ConjExponents (hypothesis)
Goal:
p q r : ℝ≥0∞
h : p.toReal.HolderTriple q.toReal r.toReal
hp : 0 < p.toReal
hq : 0 < q.toReal
hr : 0 < r.toReal
hp₁ : 0 < p ∧ p < ∞
hq₁ : 0 < q ∧ q < ∞
⊢ p.HolderTriple q r
have hr₁ : 0 < r ∧ r < ∞
Tactic: rw [toReal_pos_iff] at hp hq hr
Cleared hypotheses: hp, hq, hr
-- Lean 4 proof step from Mathlib.Data.Real.ConjExponents (goal)
Goal:
p q r : ℝ≥0∞
hp : 0 < p.toReal
hq : 0 < q.toReal
⊢ p.toReal.HolderTriple q.toReal r.toReal ↔ p.HolderTriple q r
have refine : ∀ (h : p.HolderTriple q r), p.toReal⁻¹ + q.toReal⁻¹ = r.toReal⁻¹
Tactic: refine ⟨of_toReal, fun h ↦ ⟨?_, hp, hq⟩⟩
-- Lean 4 proof step from Mathlib.Data.Real.ConjExponents (hypothesis)
Goal:
p q r : ℝ≥0∞
hp : 0 < p.toReal
hq : 0 < q.toReal
h : p.HolderTriple q r
⊢ p.toReal⁻¹ + q.toReal⁻¹ = r.toReal⁻¹
have hp₁ : 0 < p ∧ p < ∞
Tactic: rw [toReal_pos_iff] at hp hq
Cleared hypotheses: hp, hq, h
-- Lean 4 proof step from Mathlib.Data.Real.ConjExponents (hypothesis)
Goal:
p q r : ℝ≥0∞
hp : 0 < p.toReal
hq : 0 < q.toReal
h : p.HolderTriple q r
hp₁ : 0 < p ∧ p < ∞
⊢ p.toReal⁻¹ + q.toReal⁻¹ = r.toReal⁻¹
have hq₁ : 0 < q ∧ q < ∞
Tactic: rw [toReal_pos_iff] at hp hq
Cleared hypotheses: hp, hq, h
-- Lean 4 proof step from Mathlib.Data.Real.ConjExponents (goal)
Goal:
p q r : ℝ≥0∞
hp : 0 < p.toNNReal
hq : 0 < q.toNNReal
⊢ p.toNNReal.HolderTriple q.toNNReal r.toNNReal ↔ p.HolderTriple q r
have simp_rw : p.toReal.HolderTriple q.toReal r.toReal ↔ p.HolderTriple q r
Tactic: simp_rw [← NNReal.holderTriple_coe_iff, coe_toNNReal_eq_toReal]
-- Lean 4 proof step from Mathlib.Data.Real.ConjExponents (goal)
Goal:
p q r : ℝ≥0∞
hp : 0 < p.toNNReal
hq : 0 < q.toNNReal
⊢ p.toReal.HolderTriple q.toReal r.toReal ↔ p.HolderTriple q r
have apply : 0 < p.toReal
Tactic: apply toReal_iff r ?_ ?_
-- Lean 4 proof step from Mathlib.Data.Real.ConjExponents (goal)
Goal:
p q r : ℝ≥0∞
hp : 0 < p.toNNReal
hq : 0 < q.toNNReal
apply : 0 < p.toReal
⊢ p.toReal.HolderTriple q.toReal r.toReal ↔ p.HolderTriple q r
have apply₁ : 0 < q.toReal
Tactic: apply toReal_iff r ?_ ?_
-- Lean 4 proof step from Mathlib.Data.Real.ConjExponents (hypothesis)
Goal:
p q : ℝ≥0∞
h : p.toReal.HolderConjugate q.toReal
⊢ p.HolderConjugate q
have h₁ : p.toReal.HolderTriple q.toReal 1
Tactic: rw [Real.HolderConjugate] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Real.ConjExponents (goal)
Goal:
p q : ℝ≥0∞
hp : 1 < p.toReal
⊢ p.toReal.HolderConjugate q.toReal ↔ p.HolderConjugate q
have refine : ∀ (h : p.HolderConjugate q), p.toReal.HolderConjugate q.toReal
Tactic: refine ⟨of_toReal, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Data.Real.ConjExponents (goal)
Goal:
p q : ℝ≥0∞
hp : 1 < p.toReal
h : p.HolderConjugate q
⊢ 0 < q.toReal
have rw : 0 < q ∧ q < ∞
Tactic: rw [toReal_pos_iff]
-- Lean 4 proof step from Mathlib.Data.Real.ConjExponents (goal)
Goal:
p q : ℝ≥0∞
hp : 1 < p.toReal
h : p.HolderConjugate q
⊢ 0 < q ∧ q < ∞
have refine : 1 < p
Tactic: refine ⟨pos q p, lt_top_iff_one_lt q p |>.mpr ?_⟩
-- Lean 4 proof step from Mathlib.Data.Real.ConjExponents (goal)
Goal:
p q : ℝ≥0∞
hp : 1 < p.toReal
h : p.HolderConjugate q
⊢ 1 < p
have contrapose! : ∀ (hp : p ≤ 1), p.toReal ≤ 1
Tactic: contrapose! hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Data.Real.ConjExponents (hypothesis)
Goal:
p q : ℝ≥0∞
hp : 1 < p.toReal
h : p.HolderConjugate q
⊢ p.toReal.HolderConjugate q.toReal
have hq : 0 < q.toReal
Tactic: have hq : 0 < q.toReal := by
    rw [toReal_pos_iff]
    refine ⟨pos q p, lt_top_iff_one_lt q p |>.mpr ?_⟩
    contrapose! hp
    exact toReal_mono one_ne_top hp
-- Lean 4 proof step from Mathlib.Data.Real.ConjExponents (goal)
Goal:
p q : ℝ≥0∞
hp : 1 < p.toNNReal
⊢ p.toNNReal.HolderConjugate q.toNNReal ↔ p.HolderConjugate q
have simp_rw : p.toReal.HolderTriple q.toReal (↑1 : ℝ) ↔ p.HolderConjugate q
Tactic: simp_rw [← NNReal.holderTriple_coe_iff, coe_toNNReal_eq_toReal]
-- Lean 4 proof step from Mathlib.Data.Real.ConjExponents (goal)
Goal:
p q : ℝ≥0∞
hp : 1 < p.toNNReal
⊢ p.toReal.HolderTriple q.toReal (↑1 : ℝ) ↔ p.HolderConjugate q
have apply : 1 < p.toReal
Tactic: apply toReal_iff ?_
-- Lean 4 proof step from Mathlib.Data.Real.ConjExponents (hypothesis)
Goal:
p : ℝ≥0∞
hp : 1 ≤ p
⊢ p.HolderConjugate p.conjExponent
have this : p ≠ 0
Tactic: have : p ≠ 0 := (zero_lt_one.trans_le hp).ne'
-- Lean 4 proof step from Mathlib.Data.Real.ConjExponents (goal)
Goal:
p : ℝ≥0∞
hp : 1 ≤ p
this : p ≠ 0
⊢ p.HolderConjugate p.conjExponent
have rw : (1 + (p - 1)⁻¹)⁻¹ + p⁻¹ = 1⁻¹
Tactic: rw [HolderConjugate, holderTriple_iff, conjExponent, add_comm]
-- Lean 4 proof step from Mathlib.Data.Real.ConjExponents (goal)
Goal:
p : ℝ≥0∞
hp : 1 ≤ p
this : p ≠ 0
⊢ (1 + (p - 1)⁻¹)⁻¹ + p⁻¹ = 1⁻¹
have refine : (1 + (p - 1)⁻¹)⁻¹ = 1⁻¹ - p⁻¹
Tactic: refine (AddLECancellable.eq_tsub_iff_add_eq_of_le (α := ℝ≥0∞) (by simpa) (by simpa)).1 ?_
-- Lean 4 proof step from Mathlib.Data.Real.ConjExponents (goal)
Goal:
p : ℝ≥0∞
hp : 1 ≤ p
this : p ≠ 0
⊢ (1 + (p - 1)⁻¹)⁻¹ = 1⁻¹ - p⁻¹
have rw : 1 + (p - 1)⁻¹ = (1⁻¹ - p⁻¹)⁻¹
Tactic: rw [inv_eq_iff_eq_inv]
-- Lean 4 proof step from Mathlib.Data.Real.ConjExponents (goal)
Goal:
p : ℝ≥0∞
hp : 1 ≤ p
this : p ≠ 0
⊢ 1 + (p - 1)⁻¹ = (1⁻¹ - p⁻¹)⁻¹
have inl : ∀ (hp : LE.le (α := ℝ≥0∞) 1 1) (this : Ne (α := ℝ≥0∞) 1 0),
  1 + (HSub.hSub (α := ℝ≥0∞) 1 1)⁻¹ = (HSub.hSub (α := ℝ≥0∞) 1⁻¹ 1⁻¹)⁻¹
Tactic: obtain rfl | hp₁ := hp.eq_or_lt
Cleared hypotheses: p, hp, this
-- Lean 4 proof step from Mathlib.Data.Real.ConjExponents (goal)
Goal:
p : ℝ≥0∞
hp : 1 ≤ p
this : p ≠ 0
inl :
  ∀ (hp : LE.le (α := ℝ≥0∞) 1 1) (this : Ne (α := ℝ≥0∞) 1 0),
    1 + (HSub.hSub (α := ℝ≥0∞) 1 1)⁻¹ = (HSub.hSub (α := ℝ≥0∞) 1⁻¹ 1⁻¹)⁻¹
⊢ 1 + (p - 1)⁻¹ = (1⁻¹ - p⁻¹)⁻¹
have inr : ∀ (hp₁ : 1 < p), 1 + (p - 1)⁻¹ = (1⁻¹ - p⁻¹)⁻¹
Tactic: obtain rfl | hp₁ := hp.eq_or_lt
-- Lean 4 proof step from Mathlib.Data.Real.ConjExponents (goal)
Goal:
p : ℝ≥0∞
hp : 1 ≤ p
this : p ≠ 0
hp₁ : 1 < p
⊢ 1 + (p - 1)⁻¹ = (1⁻¹ - p⁻¹)⁻¹
have inr : ∀ (hp : LE.le (α := ℝ≥0∞) 1 ∞) (this : Ne (α := ℝ≥0∞) ∞ 0) (hp₁ : LT.lt (α := ℝ≥0∞) 1 ∞),
  1 + (HSub.hSub (α := ℝ≥0∞) ∞ 1)⁻¹ = (HSub.hSub (α := ℝ≥0∞) 1⁻¹ ∞⁻¹)⁻¹
Tactic: obtain rfl | hp := eq_or_ne p ∞
Cleared hypotheses: p, hp, this, hp₁
-- Lean 4 proof step from Mathlib.Data.Real.ConjExponents (goal)
Goal:
p : ℝ≥0∞
hp : 1 ≤ p
this : p ≠ 0
hp₁ : 1 < p
inr :
  ∀ (hp : LE.le (α := ℝ≥0∞) 1 ∞) (this : Ne (α := ℝ≥0∞) ∞ 0) (hp₁ : LT.lt (α := ℝ≥0∞) 1 ∞),
    1 + (HSub.hSub (α := ℝ≥0∞) ∞ 1)⁻¹ = (HSub.hSub (α := ℝ≥0∞) 1⁻¹ ∞⁻¹)⁻¹
⊢ 1 + (p - 1)⁻¹ = (1⁻¹ - p⁻¹)⁻¹
have inr₁ : ∀ (hp : p ≠ ∞), 1 + (p - 1)⁻¹ = (1⁻¹ - p⁻¹)⁻¹
Tactic: obtain rfl | hp := eq_or_ne p ∞
-- Lean 4 proof step from Mathlib.Data.Real.ConjExponents (goal)
Goal:
p : ℝ≥0∞
hp_1 : 1 ≤ p
this : p ≠ 0
hp₁ : 1 < p
hp : p ≠ ∞
⊢ 1 + (p - 1)⁻¹ = (p - 1 + 1) / (p - 1)
have rw : 1 + (p - 1)⁻¹ = (p - 1) / (p - 1) + 1 / (p - 1)
Tactic: rw [ENNReal.add_div, ENNReal.div_self ((tsub_pos_of_lt hp₁).ne') (sub_ne_top hp), one_div]
-- Lean 4 proof step from Mathlib.Data.Real.ConjExponents (goal)
Goal:
p : ℝ≥0∞
hp_1 : 1 ≤ p
this : p ≠ 0
hp₁ : 1 < p
hp : p ≠ ∞
rw : 1 + (p - 1)⁻¹ = (p - 1) / (p - 1) + 1 / (p - 1)
⊢ 1 + (p - 1)⁻¹ = (p - 1 + 1) / (p - 1)
have rw₁ : 1 + (p - 1)⁻¹ = 1 + 1 / (p - 1)
Tactic: rw [ENNReal.add_div, ENNReal.div_self ((tsub_pos_of_lt hp₁).ne') (sub_ne_top hp), one_div]
-- Lean 4 proof step from Mathlib.Data.Real.ConjExponents (goal)
Goal:
p : ℝ≥0∞
hp_1 : 1 ≤ p
this : p ≠ 0
hp₁ : 1 < p
hp : p ≠ ∞
rw : 1 + (p - 1)⁻¹ = (p - 1) / (p - 1) + 1 / (p - 1)
rw₁ : 1 + (p - 1)⁻¹ = 1 + 1 / (p - 1)
⊢ 1 + (p - 1)⁻¹ = (p - 1 + 1) / (p - 1)
have rw₂ : 1 + (p - 1)⁻¹ = 1 + (p - 1)⁻¹
Tactic: rw [ENNReal.add_div, ENNReal.div_self ((tsub_pos_of_lt hp₁).ne') (sub_ne_top hp), one_div]
-- Lean 4 proof step from Mathlib.Data.Real.ConjExponents (goal)
Goal:
p : ℝ≥0∞
hp_1 : 1 ≤ p
this : p ≠ 0
hp₁ : 1 < p
hp : p ≠ ∞
⊢ (p - 1 + 1) / (p - 1) = (1⁻¹ - p⁻¹)⁻¹
have rw : 1 - p⁻¹ = 1⁻¹ - p⁻¹
Tactic: rw [tsub_add_cancel_of_le, ← inv_eq_iff_eq_inv, div_eq_mul_inv, ENNReal.mul_inv, inv_inv,
        ENNReal.mul_sub, ENNReal.inv_mul_cancel, mul_one]
-- Lean 4 proof step from Mathlib.Data.Real.ConjExponents (goal)
Goal:
p : ℝ≥0∞
hp_1 : 1 ≤ p
this : p ≠ 0
hp₁ : 1 < p
hp : p ≠ ∞
rw : 1 - p⁻¹ = 1⁻¹ - p⁻¹
h0 : p ≠ 0
ht : p ≠ ∞
⊢ (p - 1 + 1) / (p - 1) = (1⁻¹ - p⁻¹)⁻¹
have rw₁ : LT.lt (α := ℝ≥0∞) 0 1 → 1 < p → p⁻¹ ≠ ∞
Tactic: rw [tsub_add_cancel_of_le, ← inv_eq_iff_eq_inv, div_eq_mul_inv, ENNReal.mul_inv, inv_inv,
        ENNReal.mul_sub, ENNReal.inv_mul_cancel, mul_one]
-- Lean 4 proof step from Mathlib.Data.Real.ConjExponents (goal)
Goal:
p : ℝ≥0∞
hp_1 : 1 ≤ p
this : p ≠ 0
hp₁ : 1 < p
hp : p ≠ ∞
rw : 1 - p⁻¹ = 1⁻¹ - p⁻¹
h0 : p ≠ 0
ht : p ≠ ∞
rw₁ : LT.lt (α := ℝ≥0∞) 0 1 → 1 < p → p⁻¹ ≠ ∞
⊢ (p - 1 + 1) / (p - 1) = (1⁻¹ - p⁻¹)⁻¹
have ha : p ≠ 0 ∨ (p - 1)⁻¹ ≠ ∞
Tactic: rw [tsub_add_cancel_of_le, ← inv_eq_iff_eq_inv, div_eq_mul_inv, ENNReal.mul_inv, inv_inv,
        ENNReal.mul_sub, ENNReal.inv_mul_cancel, mul_one]
-- Lean 4 proof step from Mathlib.Data.Real.ConjExponents (goal)
Goal:
p : ℝ≥0∞
hp_1 : 1 ≤ p
this : p ≠ 0
hp₁ : 1 < p
hp : p ≠ ∞
rw : 1 - p⁻¹ = 1⁻¹ - p⁻¹
h0 : p ≠ 0
ht : p ≠ ∞
rw₁ : LT.lt (α := ℝ≥0∞) 0 1 → 1 < p → p⁻¹ ≠ ∞
ha : p ≠ 0 ∨ (p - 1)⁻¹ ≠ ∞
⊢ (p - 1 + 1) / (p - 1) = (1⁻¹ - p⁻¹)⁻¹
have hb : p ≠ ∞ ∨ (p - 1)⁻¹ ≠ 0
Tactic: rw [tsub_add_cancel_of_le, ← inv_eq_iff_eq_inv, div_eq_mul_inv, ENNReal.mul_inv, inv_inv,
        ENNReal.mul_sub, ENNReal.inv_mul_cancel, mul_one]
-- Lean 4 proof step from Mathlib.Data.Real.ConjExponents (goal)
Goal:
p : ℝ≥0∞
hp_1 : 1 ≤ p
this : p ≠ 0
hp₁ : 1 < p
hp : p ≠ ∞
⊢ 1 + (p - 1)⁻¹ = (1⁻¹ - p⁻¹)⁻¹
have rw : 1 + (p - 1)⁻¹ = (p - 1 + 1) / (p - 1)
Tactic: calc
    1 + (p - 1)⁻¹ = (p - 1 + 1) / (p - 1) := by
      rw [ENNReal.add_div, ENNReal.div_self ((tsub_pos_of_lt hp₁).ne') (sub_ne_top hp), one_div]
    _ = (1⁻¹ - p⁻¹)⁻¹ := by
      rw [tsub_add_cancel_of_le, ← inv_eq_iff_eq_inv, div_eq_mul_inv, ENNReal.mul_inv, inv_inv,
        ENNReal.mul_sub, ENNReal.inv_mul_cancel, mul_one] <;> simp [*]
-- Lean 4 proof step from Mathlib.Data.Real.ConjExponents (goal)
Goal:
p : ℝ≥0∞
hp_1 : 1 ≤ p
this : p ≠ 0
hp₁ : 1 < p
hp : p ≠ ∞
rw : 1 + (p - 1)⁻¹ = (p - 1 + 1) / (p - 1)
⊢ 1 + (p - 1)⁻¹ = (1⁻¹ - p⁻¹)⁻¹
have rw₁ : (p - 1 + 1) / (p - 1) = (1⁻¹ - p⁻¹)⁻¹
Tactic: calc
    1 + (p - 1)⁻¹ = (p - 1 + 1) / (p - 1) := by
      rw [ENNReal.add_div, ENNReal.div_self ((tsub_pos_of_lt hp₁).ne') (sub_ne_top hp), one_div]
    _ = (1⁻¹ - p⁻¹)⁻¹ := by
      rw [tsub_add_cancel_of_le, ← inv_eq_iff_eq_inv, div_eq_mul_inv, ENNReal.mul_inv, inv_inv,
        ENNReal.mul_sub, ENNReal.inv_mul_cancel, mul_one] <;> simp [*]
-- Lean 4 proof step from Mathlib.Data.Real.ConjExponents (goal)
Goal:
p q : ℝ≥0∞
h : p.HolderConjugate q
⊢ p * q = p + q
have inl : ∀ [h : HolderConjugate ∞ q], ∞ * q = ∞ + q
Tactic: obtain rfl | hp := eq_or_ne p ∞
Cleared hypotheses: p, h
-- Lean 4 proof step from Mathlib.Data.Real.ConjExponents (goal)
Goal:
p q : ℝ≥0∞
h : p.HolderConjugate q
inl : ∀ [h : HolderConjugate ∞ q], ∞ * q = ∞ + q
⊢ p * q = p + q
have inr : ∀ (hp : p ≠ ∞), p * q = p + q
Tactic: obtain rfl | hp := eq_or_ne p ∞
-- Lean 4 proof step from Mathlib.Data.Real.ConjExponents (goal)
Goal:
p q : ℝ≥0∞
h : p.HolderConjugate q
hp : p ≠ ∞
⊢ p * q = p + q
have inr : ∀ [h : p.HolderConjugate ∞], p * ∞ = p + ∞
Tactic: obtain rfl | hq := eq_or_ne q ∞
Cleared hypotheses: q, h
-- Lean 4 proof step from Mathlib.Data.Real.ConjExponents (goal)
Goal:
p q : ℝ≥0∞
h : p.HolderConjugate q
hp : p ≠ ∞
inr : ∀ [h : p.HolderConjugate ∞], p * ∞ = p + ∞
⊢ p * q = p + q
have inr₁ : ∀ (hq : q ≠ ∞), p * q = p + q
Tactic: obtain rfl | hq := eq_or_ne q ∞
-- Lean 4 proof step from Mathlib.Data.Real.ConjExponents (goal)
Goal:
p q : ℝ≥0∞
h : p.HolderConjugate q
⊢ p / q = p - 1
have inl : ∀ [h : p.HolderConjugate ∞], p / ∞ = p - 1
Tactic: obtain rfl | hq := eq_or_ne q ∞
Cleared hypotheses: q, h
-- Lean 4 proof step from Mathlib.Data.Real.ConjExponents (goal)
Goal:
p q : ℝ≥0∞
h : p.HolderConjugate q
inl : ∀ [h : p.HolderConjugate ∞], p / ∞ = p - 1
⊢ p / q = p - 1
have inr : ∀ (hq : q ≠ ∞), p / q = p - 1
Tactic: obtain rfl | hq := eq_or_ne q ∞
-- Lean 4 proof step from Mathlib.Data.Real.ConjExponents (goal)
Goal:
p : ℝ≥0∞
h : p.HolderConjugate ∞
⊢ p / ∞ = p - 1
have inl : ∀ [h : HolderConjugate 1 ∞], HDiv.hDiv (α := ℝ≥0∞) 1 ∞ = HSub.hSub (α := ℝ≥0∞) 1 1
Tactic: obtain rfl := unique ∞ p 1
Cleared hypotheses: p, h
-- Lean 4 proof step from Mathlib.Data.Real.ConjExponents (goal)
Goal:
p q : ℝ≥0∞
h : p.HolderConjugate q
hq : q ≠ ∞
⊢ p / q = p - 1
have inr : p / q + 1 = p
Tactic: refine ENNReal.eq_sub_of_add_eq one_ne_top ?_
-- Lean 4 proof step from Mathlib.Data.Real.ConjExponents (goal)
Goal:
p q : ℝ≥0∞
h : p.HolderConjugate q
hq : q ≠ ∞
⊢ p / q + 1 = p
have inr : p / q + q / q = p
Tactic: rw [← ENNReal.div_self (ne_zero q p) hq, ← ENNReal.add_div, ← h.mul_eq_add, mul_div_assoc,
    ENNReal.div_self (ne_zero q p) hq, mul_one]
-- Lean 4 proof step from Mathlib.Data.Real.ConjExponents (goal)
Goal:
p q : ℝ≥0∞
h : p.HolderConjugate q
hq : q ≠ ∞
inr : p / q + q / q = p
⊢ p / q + 1 = p
have inr₁ : (p + q) / q = p
Tactic: rw [← ENNReal.div_self (ne_zero q p) hq, ← ENNReal.add_div, ← h.mul_eq_add, mul_div_assoc,
    ENNReal.div_self (ne_zero q p) hq, mul_one]
-- Lean 4 proof step from Mathlib.Data.Real.ConjExponents (goal)
Goal:
p q : ℝ≥0∞
h : p.HolderConjugate q
hq : q ≠ ∞
inr : p / q + q / q = p
inr₁ : (p + q) / q = p
⊢ p / q + 1 = p
have inr₂ : p * q / q = p
Tactic: rw [← ENNReal.div_self (ne_zero q p) hq, ← ENNReal.add_div, ← h.mul_eq_add, mul_div_assoc,
    ENNReal.div_self (ne_zero q p) hq, mul_one]
-- Lean 4 proof step from Mathlib.Data.Real.ConjExponents (goal)
Goal:
p q : ℝ≥0∞
h : p.HolderConjugate q
hq : q ≠ ∞
inr : p / q + q / q = p
inr₁ : (p + q) / q = p
inr₂ : p * q / q = p
⊢ p / q + 1 = p
have inr₃ : p * (q / q) = p
Tactic: rw [← ENNReal.div_self (ne_zero q p) hq, ← ENNReal.add_div, ← h.mul_eq_add, mul_div_assoc,
    ENNReal.div_self (ne_zero q p) hq, mul_one]
-- Lean 4 proof step from Mathlib.Data.Real.ConjExponents (goal)
Goal:
p q : ℝ≥0∞
h : p.HolderConjugate q
hq : q ≠ ∞
inr : p / q + q / q = p
inr₁ : (p + q) / q = p
inr₂ : p * q / q = p
inr₃ : p * (q / q) = p
⊢ p / q + 1 = p
have inr₄ : p * 1 = p
Tactic: rw [← ENNReal.div_self (ne_zero q p) hq, ← ENNReal.add_div, ← h.mul_eq_add, mul_div_assoc,
    ENNReal.div_self (ne_zero q p) hq, mul_one]
-- Lean 4 proof step from Mathlib.Data.Real.ConjExponents (goal)
Goal:
p q : ℝ≥0∞
h : p.HolderConjugate q
hq : q ≠ ∞
inr : p / q + q / q = p
inr₁ : (p + q) / q = p
inr₂ : p * q / q = p
inr₃ : p * (q / q) = p
inr₄ : p * 1 = p
⊢ p / q + 1 = p
have inr₅ : p = p
Tactic: rw [← ENNReal.div_self (ne_zero q p) hq, ← ENNReal.add_div, ← h.mul_eq_add, mul_div_assoc,
    ENNReal.div_self (ne_zero q p) hq, mul_one]
-- Lean 4 proof step from Mathlib.Data.Real.Embedding (goal)
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
inst_3 : One M
num : ℤ
n den : ℕ
hn : 0 < n
x : M
⊢ HSMul.hSMul (β := M) (num * (↑n : ℤ)) 1 < HMul.hMul (α := ℤ) (↑n : ℤ) (↑den : ℤ) • x ↔
    HSMul.hSMul (β := M) num 1 < den • x
have rw : HSMul.hSMul (α := ℤ) (↑n : ℤ) (HSMul.hSMul (β := M) num 1) < HSMul.hSMul (α := ℤ) (↑n : ℤ) (den • x) ↔
  HSMul.hSMul (β := M) num 1 < den • x
Tactic: rw [mul_comm num, mul_smul, mul_smul, natCast_zsmul x den]
-- Lean 4 proof step from Mathlib.Data.Real.Embedding (hypothesis)
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
inst_3 : One M
u v : ℚ
x y : M
hu : HSMul.hSMul (β := M) u.num 1 < u.den • x
hv : HSMul.hSMul (β := M) v.num 1 < v.den • y
⊢ HSMul.hSMul (β := M) (u + v).num 1 < (u + v).den • (x + y)
have hu' : HSMul.hSMul (β := M) (u.num * (↑v.den : ℤ)) 1 < HMul.hMul (α := ℤ) (↑u.den : ℤ) (↑v.den : ℤ) • x
Tactic: have hu' : (u.num * v.den) • 1 < (u.den * v.den : ℤ) • x := by
    simpa [mul_comm] using (mul_smul_one_lt_iff v.den_pos).mpr hu
-- Lean 4 proof step from Mathlib.Data.Real.Embedding (goal)
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
inst_3 : One M
u v : ℚ
x y : M
hu : HSMul.hSMul (β := M) u.num 1 < u.den • x
hv : HSMul.hSMul (β := M) v.num 1 < v.den • y
hu' : HSMul.hSMul (β := M) (u.num * (↑v.den : ℤ)) 1 < HMul.hMul (α := ℤ) (↑u.den : ℤ) (↑v.den : ℤ) • x
this :
  HSMul.hSMul (β := M) ((u + v).num * (↑u.den : ℤ) * (↑v.den : ℤ)) 1 <
    HSMul.hSMul (α := ℤ) (↑(u + v).den : ℤ) (HMul.hMul (α := ℤ) (↑u.den : ℤ) (↑v.den : ℤ) • (x + y))
⊢ HSMul.hSMul (β := M) (u + v).num 1 < (u + v).den • (x + y)
have refine : HSMul.hSMul (β := M) ((u + v).num * (↑(u.den * v.den) : ℤ)) 1 <
  HMul.hMul (α := ℤ) (↑(u.den * v.den) : ℤ) (↑(u + v).den : ℤ) • (x + y)
Tactic: refine (mul_smul_one_lt_iff (mul_pos u.den_pos v.den_pos)).mp ?_
-- Lean 4 proof step from Mathlib.Data.Real.Embedding (goal)
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
inst_3 : One M
u v : ℚ
x y : M
hu : HSMul.hSMul (β := M) u.num 1 < u.den • x
hv : HSMul.hSMul (β := M) v.num 1 < v.den • y
hu' : HSMul.hSMul (β := M) (u.num * (↑v.den : ℤ)) 1 < HMul.hMul (α := ℤ) (↑u.den : ℤ) (↑v.den : ℤ) • x
this :
  HSMul.hSMul (β := M) ((u + v).num * (↑u.den : ℤ) * (↑v.den : ℤ)) 1 <
    HSMul.hSMul (α := ℤ) (↑(u + v).den : ℤ) (HMul.hMul (α := ℤ) (↑u.den : ℤ) (↑v.den : ℤ) • (x + y))
⊢ HSMul.hSMul (β := M) ((u + v).num * (↑(u.den * v.den) : ℤ)) 1 <
    HMul.hMul (α := ℤ) (↑(u.den * v.den) : ℤ) (↑(u + v).den : ℤ) • (x + y)
have rwa : HSMul.hSMul (β := M) ((u + v).num * HMul.hMul (α := ℤ) (↑u.den : ℤ) (↑v.den : ℤ)) 1 <
  (HMul.hMul (α := ℤ) (↑u.den : ℤ) (↑v.den : ℤ) * (↑(u + v).den : ℤ)) • (x + y)
Tactic: rwa [Nat.cast_mul, ← mul_assoc, mul_comm _ ((u + v).den : ℤ), ← smul_eq_mul ((u + v).den : ℤ),
      smul_assoc]
-- Lean 4 proof step from Mathlib.Data.Real.Embedding (goal)
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
inst_3 : One M
u v : ℚ
x y : M
hu : HSMul.hSMul (β := M) u.num 1 < u.den • x
hv : HSMul.hSMul (β := M) v.num 1 < v.den • y
hu' : HSMul.hSMul (β := M) (u.num * (↑v.den : ℤ)) 1 < HMul.hMul (α := ℤ) (↑u.den : ℤ) (↑v.den : ℤ) • x
this :
  HSMul.hSMul (β := M) ((u + v).num * (↑u.den : ℤ) * (↑v.den : ℤ)) 1 <
    HSMul.hSMul (α := ℤ) (↑(u + v).den : ℤ) (HMul.hMul (α := ℤ) (↑u.den : ℤ) (↑v.den : ℤ) • (x + y))
rwa :
  HSMul.hSMul (β := M) ((u + v).num * HMul.hMul (α := ℤ) (↑u.den : ℤ) (↑v.den : ℤ)) 1 <
    (HMul.hMul (α := ℤ) (↑u.den : ℤ) (↑v.den : ℤ) * (↑(u + v).den : ℤ)) • (x + y)
⊢ HSMul.hSMul (β := M) ((u + v).num * (↑(u.den * v.den) : ℤ)) 1 <
    HMul.hMul (α := ℤ) (↑(u.den * v.den) : ℤ) (↑(u + v).den : ℤ) • (x + y)
have rwa₁ : HSMul.hSMul (β := M) ((u + v).num * (↑u.den : ℤ) * (↑v.den : ℤ)) 1 <
  (HMul.hMul (α := ℤ) (↑u.den : ℤ) (↑v.den : ℤ) * (↑(u + v).den : ℤ)) • (x + y)
Tactic: rwa [Nat.cast_mul, ← mul_assoc, mul_comm _ ((u + v).den : ℤ), ← smul_eq_mul ((u + v).den : ℤ),
      smul_assoc]
-- Lean 4 proof step from Mathlib.Data.Real.Embedding (goal)
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
inst_3 : One M
u v : ℚ
x y : M
hu : HSMul.hSMul (β := M) u.num 1 < u.den • x
hv : HSMul.hSMul (β := M) v.num 1 < v.den • y
hu' : HSMul.hSMul (β := M) (u.num * (↑v.den : ℤ)) 1 < HMul.hMul (α := ℤ) (↑u.den : ℤ) (↑v.den : ℤ) • x
this :
  HSMul.hSMul (β := M) ((u + v).num * (↑u.den : ℤ) * (↑v.den : ℤ)) 1 <
    HSMul.hSMul (α := ℤ) (↑(u + v).den : ℤ) (HMul.hMul (α := ℤ) (↑u.den : ℤ) (↑v.den : ℤ) • (x + y))
rwa :
  HSMul.hSMul (β := M) ((u + v).num * HMul.hMul (α := ℤ) (↑u.den : ℤ) (↑v.den : ℤ)) 1 <
    (HMul.hMul (α := ℤ) (↑u.den : ℤ) (↑v.den : ℤ) * (↑(u + v).den : ℤ)) • (x + y)
rwa₁ :
  HSMul.hSMul (β := M) ((u + v).num * (↑u.den : ℤ) * (↑v.den : ℤ)) 1 <
    (HMul.hMul (α := ℤ) (↑u.den : ℤ) (↑v.den : ℤ) * (↑(u + v).den : ℤ)) • (x + y)
⊢ HSMul.hSMul (β := M) ((u + v).num * (↑(u.den * v.den) : ℤ)) 1 <
    HMul.hMul (α := ℤ) (↑(u.den * v.den) : ℤ) (↑(u + v).den : ℤ) • (x + y)
have rwa₂ : HSMul.hSMul (β := M) ((u + v).num * (↑u.den : ℤ) * (↑v.den : ℤ)) 1 <
  ((↑(u + v).den : ℤ) * HMul.hMul (α := ℤ) (↑u.den : ℤ) (↑v.den : ℤ)) • (x + y)
Tactic: rwa [Nat.cast_mul, ← mul_assoc, mul_comm _ ((u + v).den : ℤ), ← smul_eq_mul ((u + v).den : ℤ),
      smul_assoc]
-- Lean 4 proof step from Mathlib.Data.Real.Embedding (goal)
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
inst_3 : One M
u v : ℚ
x y : M
hu : HSMul.hSMul (β := M) u.num 1 < u.den • x
hv : HSMul.hSMul (β := M) v.num 1 < v.den • y
hu' : HSMul.hSMul (β := M) (u.num * (↑v.den : ℤ)) 1 < HMul.hMul (α := ℤ) (↑u.den : ℤ) (↑v.den : ℤ) • x
this :
  HSMul.hSMul (β := M) ((u + v).num * (↑u.den : ℤ) * (↑v.den : ℤ)) 1 <
    HSMul.hSMul (α := ℤ) (↑(u + v).den : ℤ) (HMul.hMul (α := ℤ) (↑u.den : ℤ) (↑v.den : ℤ) • (x + y))
rwa :
  HSMul.hSMul (β := M) ((u + v).num * HMul.hMul (α := ℤ) (↑u.den : ℤ) (↑v.den : ℤ)) 1 <
    (HMul.hMul (α := ℤ) (↑u.den : ℤ) (↑v.den : ℤ) * (↑(u + v).den : ℤ)) • (x + y)
rwa₁ :
  HSMul.hSMul (β := M) ((u + v).num * (↑u.den : ℤ) * (↑v.den : ℤ)) 1 <
    (HMul.hMul (α := ℤ) (↑u.den : ℤ) (↑v.den : ℤ) * (↑(u + v).den : ℤ)) • (x + y)
rwa₂ :
  HSMul.hSMul (β := M) ((u + v).num * (↑u.den : ℤ) * (↑v.den : ℤ)) 1 <
    ((↑(u + v).den : ℤ) * HMul.hMul (α := ℤ) (↑u.den : ℤ) (↑v.den : ℤ)) • (x + y)
⊢ HSMul.hSMul (β := M) ((u + v).num * (↑(u.den * v.den) : ℤ)) 1 <
    HMul.hMul (α := ℤ) (↑(u.den * v.den) : ℤ) (↑(u + v).den : ℤ) • (x + y)
have rwa₃ : HSMul.hSMul (β := M) ((u + v).num * (↑u.den : ℤ) * (↑v.den : ℤ)) 1 <
  HSMul.hSMul (α := ℤ) (↑(u + v).den : ℤ) (HMul.hMul (α := ℤ) (↑u.den : ℤ) (↑v.den : ℤ)) • (x + y)
Tactic: rwa [Nat.cast_mul, ← mul_assoc, mul_comm _ ((u + v).den : ℤ), ← smul_eq_mul ((u + v).den : ℤ),
      smul_assoc]