awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
x : ℝ
f y : CauSeq ℚ abs
h : ∃ (i : ℕ), ∀ j ≥ i, mk y ≤ (↑((↑f : ℕ → ℚ) j) : ℝ)
K : ℚ
K0 : K > 0
hK : ∃ (i : ℕ), ∀ j ≥ i, K ≤ (↑(y - f) : ℕ → ℚ) j
⊢ False
have h₁ : ∀ (i : ℕ)
  (H :
    ∀ j ≥ i,
      mk y ≤ (↑((↑f : ℕ → ℚ) j) : ℝ) ∧ K ≤ (↑(y - f) : ℕ → ℚ) j ∧ ∀ k ≥ j, |(↑f : ℕ → ℚ) k - (↑f : ℕ → ℚ) j| < K / 2),
  False
Tactic: obtain ⟨i, H⟩ := exists_forall_ge_and h (exists_forall_ge_and hK (f.cauchy₃ <| half_pos K0))
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
x : ℝ
f y : CauSeq ℚ abs
h : ∃ (i : ℕ), ∀ j ≥ i, mk y ≤ (↑((↑f : ℕ → ℚ) j) : ℝ)
K : ℚ
K0 : K > 0
hK : ∃ (i : ℕ), ∀ j ≥ i, K ≤ (↑(y - f) : ℕ → ℚ) j
i : ℕ
H :
  ∀ j ≥ i,
    mk y ≤ (↑((↑f : ℕ → ℚ) j) : ℝ) ∧ K ≤ (↑(y - f) : ℕ → ℚ) j ∧ ∀ k ≥ j, |(↑f : ℕ → ℚ) k - (↑f : ℕ → ℚ) j| < K / 2
⊢ False
have h₁ : (↑((↑f : ℕ → ℚ) i) : ℝ) < mk y
Tactic: apply not_lt_of_ge (H _ le_rfl).1
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
x : ℝ
f y : CauSeq ℚ abs
h : ∃ (i : ℕ), ∀ j ≥ i, mk y ≤ (↑((↑f : ℕ → ℚ) j) : ℝ)
K : ℚ
K0 : K > 0
hK : ∃ (i : ℕ), ∀ j ≥ i, K ≤ (↑(y - f) : ℕ → ℚ) j
i : ℕ
H :
  ∀ j ≥ i,
    mk y ≤ (↑((↑f : ℕ → ℚ) j) : ℝ) ∧ K ≤ (↑(y - f) : ℕ → ℚ) j ∧ ∀ k ≥ j, |(↑f : ℕ → ℚ) k - (↑f : ℕ → ℚ) j| < K / 2
⊢ (↑((↑f : ℕ → ℚ) i) : ℝ) < mk y
have h₁ : const abs ((↑f : ℕ → ℚ) i) < y
Tactic: rw [← mk_const, mk_lt]
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
x : ℝ
f y : CauSeq ℚ abs
h : ∃ (i : ℕ), ∀ j ≥ i, mk y ≤ (↑((↑f : ℕ → ℚ) j) : ℝ)
K : ℚ
K0 : K > 0
hK : ∃ (i : ℕ), ∀ j ≥ i, K ≤ (↑(y - f) : ℕ → ℚ) j
i : ℕ
H :
  ∀ j ≥ i,
    mk y ≤ (↑((↑f : ℕ → ℚ) j) : ℝ) ∧ K ≤ (↑(y - f) : ℕ → ℚ) j ∧ ∀ k ≥ j, |(↑f : ℕ → ℚ) k - (↑f : ℕ → ℚ) j| < K / 2
⊢ const abs ((↑f : ℕ → ℚ) i) < y
have h₁ : ∀ (j : ℕ) (ij : j ≥ i),
  K / 2 ≤ (↑(HSub.hSub (β := CauSeq ℚ abs) y (const abs ((↑f : ℕ → ℚ) i) : CauSeq ℚ abs)) : ℕ → ℚ) j
Tactic: refine ⟨_, half_pos K0, i, fun j ij => ?_⟩
-- Lean 4 proof step from Mathlib.Data.Real.Basic (hypothesis)
Goal:
x : ℝ
f y : CauSeq ℚ abs
h : ∃ (i : ℕ), ∀ j ≥ i, mk y ≤ (↑((↑f : ℕ → ℚ) j) : ℝ)
K : ℚ
K0 : K > 0
hK : ∃ (i : ℕ), ∀ j ≥ i, K ≤ (↑(y - f) : ℕ → ℚ) j
i : ℕ
H :
  ∀ j ≥ i,
    mk y ≤ (↑((↑f : ℕ → ℚ) j) : ℝ) ∧ K ≤ (↑(y - f) : ℕ → ℚ) j ∧ ∀ k ≥ j, |(↑f : ℕ → ℚ) k - (↑f : ℕ → ℚ) j| < K / 2
j : ℕ
ij : j ≥ i
⊢ K / 2 ≤ (↑(HSub.hSub (β := CauSeq ℚ abs) y (const abs ((↑f : ℕ → ℚ) i) : CauSeq ℚ abs)) : ℕ → ℚ) j
have this : K + -(K / 2) ≤ (↑(y - f) : ℕ → ℚ) j + ((↑f : ℕ → ℚ) j - (↑f : ℕ → ℚ) i)
Tactic: have := add_le_add (H _ ij).2.1 (le_of_lt (abs_lt.1 <| (H _ le_rfl).2.2 _ ij).1)
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
x : ℝ
f y : CauSeq ℚ abs
h : ∃ (i : ℕ), ∀ j ≥ i, mk y ≤ (↑((↑f : ℕ → ℚ) j) : ℝ)
K : ℚ
K0 : K > 0
hK : ∃ (i : ℕ), ∀ j ≥ i, K ≤ (↑(y - f) : ℕ → ℚ) j
i : ℕ
H :
  ∀ j ≥ i,
    mk y ≤ (↑((↑f : ℕ → ℚ) j) : ℝ) ∧ K ≤ (↑(y - f) : ℕ → ℚ) j ∧ ∀ k ≥ j, |(↑f : ℕ → ℚ) k - (↑f : ℕ → ℚ) j| < K / 2
j : ℕ
ij : j ≥ i
this : K + -(K / 2) ≤ (↑(y - f) : ℕ → ℚ) j + ((↑f : ℕ → ℚ) j - (↑f : ℕ → ℚ) i)
⊢ K / 2 ≤ (↑(HSub.hSub (β := CauSeq ℚ abs) y (const abs ((↑f : ℕ → ℚ) i) : CauSeq ℚ abs)) : ℕ → ℚ) j
have h₁ : ∀ (this : K - K / 2 ≤ (↑(y - f) : ℕ → ℚ) j + ((↑f : ℕ → ℚ) j - (↑f : ℕ → ℚ) i)),
  K / 2 ≤ (↑(HSub.hSub (β := CauSeq ℚ abs) y (const abs ((↑f : ℕ → ℚ) i) : CauSeq ℚ abs)) : ℕ → ℚ) j
Tactic: rwa [← sub_eq_add_neg, sub_self_div_two, sub_apply, sub_add_sub_cancel] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
x : ℝ
f y : CauSeq ℚ abs
h : ∃ (i : ℕ), ∀ j ≥ i, mk y ≤ (↑((↑f : ℕ → ℚ) j) : ℝ)
K : ℚ
K0 : K > 0
hK : ∃ (i : ℕ), ∀ j ≥ i, K ≤ (↑(y - f) : ℕ → ℚ) j
i : ℕ
H :
  ∀ j ≥ i,
    mk y ≤ (↑((↑f : ℕ → ℚ) j) : ℝ) ∧ K ≤ (↑(y - f) : ℕ → ℚ) j ∧ ∀ k ≥ j, |(↑f : ℕ → ℚ) k - (↑f : ℕ → ℚ) j| < K / 2
j : ℕ
ij : j ≥ i
this : K + -(K / 2) ≤ (↑(y - f) : ℕ → ℚ) j + ((↑f : ℕ → ℚ) j - (↑f : ℕ → ℚ) i)
h₁ :
  ∀ (this : K - K / 2 ≤ (↑(y - f) : ℕ → ℚ) j + ((↑f : ℕ → ℚ) j - (↑f : ℕ → ℚ) i)),
    K / 2 ≤ (↑(HSub.hSub (β := CauSeq ℚ abs) y (const abs ((↑f : ℕ → ℚ) i) : CauSeq ℚ abs)) : ℕ → ℚ) j
⊢ K / 2 ≤ (↑(HSub.hSub (β := CauSeq ℚ abs) y (const abs ((↑f : ℕ → ℚ) i) : CauSeq ℚ abs)) : ℕ → ℚ) j
have h₂ : ∀ (this : K / 2 ≤ (↑(y - f) : ℕ → ℚ) j + ((↑f : ℕ → ℚ) j - (↑f : ℕ → ℚ) i)),
  K / 2 ≤ (↑(HSub.hSub (β := CauSeq ℚ abs) y (const abs ((↑f : ℕ → ℚ) i) : CauSeq ℚ abs)) : ℕ → ℚ) j
Tactic: rwa [← sub_eq_add_neg, sub_self_div_two, sub_apply, sub_add_sub_cancel] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
x : ℝ
f y : CauSeq ℚ abs
h : ∃ (i : ℕ), ∀ j ≥ i, mk y ≤ (↑((↑f : ℕ → ℚ) j) : ℝ)
K : ℚ
K0 : K > 0
hK : ∃ (i : ℕ), ∀ j ≥ i, K ≤ (↑(y - f) : ℕ → ℚ) j
i : ℕ
H :
  ∀ j ≥ i,
    mk y ≤ (↑((↑f : ℕ → ℚ) j) : ℝ) ∧ K ≤ (↑(y - f) : ℕ → ℚ) j ∧ ∀ k ≥ j, |(↑f : ℕ → ℚ) k - (↑f : ℕ → ℚ) j| < K / 2
j : ℕ
ij : j ≥ i
this : K + -(K / 2) ≤ (↑(y - f) : ℕ → ℚ) j + ((↑f : ℕ → ℚ) j - (↑f : ℕ → ℚ) i)
h₁ :
  ∀ (this : K - K / 2 ≤ (↑(y - f) : ℕ → ℚ) j + ((↑f : ℕ → ℚ) j - (↑f : ℕ → ℚ) i)),
    K / 2 ≤ (↑(HSub.hSub (β := CauSeq ℚ abs) y (const abs ((↑f : ℕ → ℚ) i) : CauSeq ℚ abs)) : ℕ → ℚ) j
h₂ :
  ∀ (this : K / 2 ≤ (↑(y - f) : ℕ → ℚ) j + ((↑f : ℕ → ℚ) j - (↑f : ℕ → ℚ) i)),
    K / 2 ≤ (↑(HSub.hSub (β := CauSeq ℚ abs) y (const abs ((↑f : ℕ → ℚ) i) : CauSeq ℚ abs)) : ℕ → ℚ) j
⊢ K / 2 ≤ (↑(HSub.hSub (β := CauSeq ℚ abs) y (const abs ((↑f : ℕ → ℚ) i) : CauSeq ℚ abs)) : ℕ → ℚ) j
have h₃ : ∀ (this : K / 2 ≤ (↑y : ℕ → ℚ) j - (↑f : ℕ → ℚ) j + ((↑f : ℕ → ℚ) j - (↑f : ℕ → ℚ) i)),
  K / 2 ≤ (↑(HSub.hSub (β := CauSeq ℚ abs) y (const abs ((↑f : ℕ → ℚ) i) : CauSeq ℚ abs)) : ℕ → ℚ) j
Tactic: rwa [← sub_eq_add_neg, sub_self_div_two, sub_apply, sub_add_sub_cancel] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
x : ℝ
f y : CauSeq ℚ abs
h : ∃ (i : ℕ), ∀ j ≥ i, mk y ≤ (↑((↑f : ℕ → ℚ) j) : ℝ)
K : ℚ
K0 : K > 0
hK : ∃ (i : ℕ), ∀ j ≥ i, K ≤ (↑(y - f) : ℕ → ℚ) j
i : ℕ
H :
  ∀ j ≥ i,
    mk y ≤ (↑((↑f : ℕ → ℚ) j) : ℝ) ∧ K ≤ (↑(y - f) : ℕ → ℚ) j ∧ ∀ k ≥ j, |(↑f : ℕ → ℚ) k - (↑f : ℕ → ℚ) j| < K / 2
j : ℕ
ij : j ≥ i
this : K + -(K / 2) ≤ (↑(y - f) : ℕ → ℚ) j + ((↑f : ℕ → ℚ) j - (↑f : ℕ → ℚ) i)
h₁ :
  ∀ (this : K - K / 2 ≤ (↑(y - f) : ℕ → ℚ) j + ((↑f : ℕ → ℚ) j - (↑f : ℕ → ℚ) i)),
    K / 2 ≤ (↑(HSub.hSub (β := CauSeq ℚ abs) y (const abs ((↑f : ℕ → ℚ) i) : CauSeq ℚ abs)) : ℕ → ℚ) j
h₂ :
  ∀ (this : K / 2 ≤ (↑(y - f) : ℕ → ℚ) j + ((↑f : ℕ → ℚ) j - (↑f : ℕ → ℚ) i)),
    K / 2 ≤ (↑(HSub.hSub (β := CauSeq ℚ abs) y (const abs ((↑f : ℕ → ℚ) i) : CauSeq ℚ abs)) : ℕ → ℚ) j
h₃ :
  ∀ (this : K / 2 ≤ (↑y : ℕ → ℚ) j - (↑f : ℕ → ℚ) j + ((↑f : ℕ → ℚ) j - (↑f : ℕ → ℚ) i)),
    K / 2 ≤ (↑(HSub.hSub (β := CauSeq ℚ abs) y (const abs ((↑f : ℕ → ℚ) i) : CauSeq ℚ abs)) : ℕ → ℚ) j
⊢ K / 2 ≤ (↑(HSub.hSub (β := CauSeq ℚ abs) y (const abs ((↑f : ℕ → ℚ) i) : CauSeq ℚ abs)) : ℕ → ℚ) j
have h₄ : ∀ (this : K / 2 ≤ (↑y : ℕ → ℚ) j - (↑f : ℕ → ℚ) i),
  K / 2 ≤ (↑(HSub.hSub (β := CauSeq ℚ abs) y (const abs ((↑f : ℕ → ℚ) i) : CauSeq ℚ abs)) : ℕ → ℚ) j
Tactic: rwa [← sub_eq_add_neg, sub_self_div_two, sub_apply, sub_add_sub_cancel] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
f : CauSeq ℚ abs
x : ℝ
h : ∃ (i : ℕ), ∀ j ≥ i, (↑((↑f : ℕ → ℚ) j) : ℝ) ≤ x
⊢ mk f ≤ x
have obtain : ∀ (i : ℕ) (H : ∀ j ≥ i, (↑((↑f : ℕ → ℚ) j) : ℝ) ≤ x), mk f ≤ x
Tactic: obtain ⟨i, H⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
f : CauSeq ℚ abs
x : ℝ
i : ℕ
H : ∀ j ≥ i, (↑((↑f : ℕ → ℚ) j) : ℝ) ≤ x
⊢ mk f ≤ x
have rw : -x ≤ mk (-f)
Tactic: rw [← neg_le_neg_iff, ← mk_neg]
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
a : ℝ
ha : 0 ≤ a
b : ℕ
⊢ a * (↑b : ℝ) + 1 ≤ (a + 1) ^ b
have inl : ∀ (ha : LE.le (α := ℝ) 0 0), HMul.hMul (α := ℝ) 0 (↑b : ℝ) + 1 ≤ HAdd.hAdd (α := ℝ) 0 1 ^ b
Tactic: rcases ha.eq_or_lt with rfl | ha'
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
a : ℝ
ha : 0 ≤ a
b : ℕ
inl : ∀ (ha : LE.le (α := ℝ) 0 0), HMul.hMul (α := ℝ) 0 (↑b : ℝ) + 1 ≤ HAdd.hAdd (α := ℝ) 0 1 ^ b
⊢ a * (↑b : ℝ) + 1 ≤ (a + 1) ^ b
have inr : ∀ (ha' : 0 < a), a * (↑b : ℝ) + 1 ≤ (a + 1) ^ b
Tactic: rcases ha.eq_or_lt with rfl | ha'
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
b : ℕ
hb : ∀ {a : ℝ} (ha' : 0 < a), a * (↑b : ℝ) + 1 ≤ (a + 1) ^ b
a : ℝ
ha' : 0 < a
⊢ HAdd.hAdd (α := ℝ) 0 1 ^ b * a + (a * (↑b : ℝ) + 1) ≤ (a + 1) ^ b * a + (a + 1) ^ b
have h₁ : 0 ≤ HAdd.hAdd (α := ℝ) 0 1
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
b : ℕ
hb : ∀ {a : ℝ} (ha' : 0 < a), a * (↑b : ℝ) + 1 ≤ (a + 1) ^ b
a : ℝ
ha' : 0 < a
h₁ : 0 ≤ HAdd.hAdd (α := ℝ) 0 1
⊢ HAdd.hAdd (α := ℝ) 0 1 ^ b * a + (a * (↑b : ℝ) + 1) ≤ (a + 1) ^ b * a + (a + 1) ^ b
have h₂ : a * (↑b : ℝ) + 1 ≤ (a + 1) ^ b
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
b : ℕ
hb : ∀ {a : ℝ} (ha' : 0 < a), a * (↑b : ℝ) + 1 ≤ (a + 1) ^ b
a : ℝ
ha' : 0 < a
⊢ a * (↑(b + 1) : ℝ) + 1 ≤ (a + 1) ^ (b + 1)
have a₁ : a * (↑(b + 1) : ℝ) + 1 = HAdd.hAdd (α := ℝ) 0 1 ^ b * a + (a * (↑b : ℝ) + 1)
Tactic: calc
      a * ↑(b + 1) + 1 = (0 + 1) ^ b * a + (a * b + 1) := by
        simp [mul_add, add_assoc, add_left_comm]
      _ ≤ (a + 1) ^ b * a + (a + 1) ^ b := by
        gcongr
        · norm_num
        · exact hb ha'
      _ = (a + 1) ^ (b + 1) := by simp [pow_succ, mul_add]
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
b : ℕ
hb : ∀ {a : ℝ} (ha' : 0 < a), a * (↑b : ℝ) + 1 ≤ (a + 1) ^ b
a : ℝ
ha' : 0 < a
a₁ : a * (↑(b + 1) : ℝ) + 1 = HAdd.hAdd (α := ℝ) 0 1 ^ b * a + (a * (↑b : ℝ) + 1)
⊢ a * (↑(b + 1) : ℝ) + 1 ≤ (a + 1) ^ (b + 1)
have a₂ : HAdd.hAdd (α := ℝ) 0 1 ^ b * a + (a * (↑b : ℝ) + 1) ≤ (a + 1) ^ b * a + (a + 1) ^ b
Tactic: calc
      a * ↑(b + 1) + 1 = (0 + 1) ^ b * a + (a * b + 1) := by
        simp [mul_add, add_assoc, add_left_comm]
      _ ≤ (a + 1) ^ b * a + (a + 1) ^ b := by
        gcongr
        · norm_num
        · exact hb ha'
      _ = (a + 1) ^ (b + 1) := by simp [pow_succ, mul_add]
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
b : ℕ
hb : ∀ {a : ℝ} (ha' : 0 < a), a * (↑b : ℝ) + 1 ≤ (a + 1) ^ b
a : ℝ
ha' : 0 < a
a₁ : a * (↑(b + 1) : ℝ) + 1 = HAdd.hAdd (α := ℝ) 0 1 ^ b * a + (a * (↑b : ℝ) + 1)
a₂ : HAdd.hAdd (α := ℝ) 0 1 ^ b * a + (a * (↑b : ℝ) + 1) ≤ (a + 1) ^ b * a + (a + 1) ^ b
⊢ a * (↑(b + 1) : ℝ) + 1 ≤ (a + 1) ^ (b + 1)
have a₃ : (a + 1) ^ b * a + (a + 1) ^ b = (a + 1) ^ (b + 1)
Tactic: calc
      a * ↑(b + 1) + 1 = (0 + 1) ^ b * a + (a * b + 1) := by
        simp [mul_add, add_assoc, add_left_comm]
      _ ≤ (a + 1) ^ b * a + (a + 1) ^ b := by
        gcongr
        · norm_num
        · exact hb ha'
      _ = (a + 1) ^ (b + 1) := by simp [pow_succ, mul_add]
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
a : ℝ
b : ℕ
ha' : 0 < a
⊢ a * (↑b : ℝ) + 1 ≤ (a + 1) ^ b
have inr : ∀ {a : ℝ} (ha' : 0 < a), a * (↑0 : ℝ) + 1 ≤ HPow.hPow (β := ℕ) (a + 1) 0
Tactic: induction b generalizing a with
  | zero => simp
  | succ b hb =>
    calc
      a * ↑(b + 1) + 1 = (0 + 1) ^ b * a + (a * b + 1) := by
        simp [mul_add, add_assoc, add_left_comm]
      _ ≤ (a + 1) ^ b * a + (a + 1) ^ b := by
        gcongr
        · norm_num
        · exact hb ha'
      _ = (a + 1) ^ (b + 1) := by simp [pow_succ, mul_add]
Cleared hypotheses: a, b, ha'
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
a : ℝ
b : ℕ
ha' : 0 < a
inr : ∀ {a : ℝ} (ha' : 0 < a), a * (↑0 : ℝ) + 1 ≤ HPow.hPow (β := ℕ) (a + 1) 0
⊢ a * (↑b : ℝ) + 1 ≤ (a + 1) ^ b
have inr₁ : ∀ (b : ℕ) (hb : ∀ {a : ℝ} (ha' : 0 < a), a * (↑b : ℝ) + 1 ≤ (a + 1) ^ b) {a : ℝ} (ha' : 0 < a),
  a * (↑(b + 1) : ℝ) + 1 ≤ (a + 1) ^ (b + 1)
Tactic: induction b generalizing a with
  | zero => simp
  | succ b hb =>
    calc
      a * ↑(b + 1) + 1 = (0 + 1) ^ b * a + (a * b + 1) := by
        simp [mul_add, add_assoc, add_left_comm]
      _ ≤ (a + 1) ^ b * a + (a + 1) ^ b := by
        gcongr
        · norm_num
        · exact hb ha'
      _ = (a + 1) ^ (b + 1) := by simp [pow_succ, mul_add]
Cleared hypotheses: a, b, ha'
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
R : Type u_1
inst : Monoid R
f : R → ℝ
hf : IsPowMul f
| f 1
have rw : HPow.hPow (β := ℕ) (f 1) 2
Tactic: rw [← one_pow 2, hf _ one_le_two]
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
R : Type u_1
inst : Monoid R
f : R → ℝ
hf : IsPowMul f
⊢ HPow.hPow (β := ℕ) (f 1) 2 = f 1
have conv_rhs : HPow.hPow (β := ℕ) (f 1) 2 = f 1
Tactic: conv_rhs => rw [← one_pow 2, hf _ one_le_two]
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
R : Type u_1
inst : Monoid R
f : R → ℝ
hf : IsPowMul f
conv_rhs : HPow.hPow (β := ℕ) (f 1) 2 = f 1
⊢ HPow.hPow (β := ℕ) (f 1) 2 = f 1
have conv_rhs₁ : HPow.hPow (β := ℕ) (f 1) 2 = HPow.hPow (β := ℕ) (f 1) 2
Tactic: conv_rhs => rw [← one_pow 2, hf _ one_le_two]
-- Lean 4 proof step from Mathlib.Data.Real.Basic (hypothesis)
Goal:
R : Type u_1
inst : Monoid R
f : R → ℝ
hf : IsPowMul f
⊢ f 1 ≤ 1
have hf1 : HPow.hPow (β := ℕ) (f 1) 2 = f 1
Tactic: have hf1 : (f 1) ^ 2 = f 1 := by conv_rhs => rw [← one_pow 2, hf _ one_le_two]
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
R : Type u_1
inst : Monoid R
f : R → ℝ
hf : IsPowMul f
hf1 : HPow.hPow (β := ℕ) (f 1) 2 = f 1
⊢ f 1 ≤ 1
have inl : ∀ (h : f 1 = 0), f 1 ≤ 1
Tactic: rcases eq_zero_or_one_of_sq_eq_self hf1 with h | h
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
R : Type u_1
inst : Monoid R
f : R → ℝ
hf : IsPowMul f
hf1 : HPow.hPow (β := ℕ) (f 1) 2 = f 1
inl : ∀ (h : f 1 = 0), f 1 ≤ 1
⊢ f 1 ≤ 1
have inr : ∀ (h : f 1 = 1), f 1 ≤ 1
Tactic: rcases eq_zero_or_one_of_sq_eq_self hf1 with h | h
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
R : Type u_1
inst : Monoid R
f : R → ℝ
hf : IsPowMul f
hf1 : HPow.hPow (β := ℕ) (f 1) 2 = f 1
h : f 1 = 0
⊢ f 1 ≤ 1
have inl : LE.le (α := ℝ) 0 1
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Data.Real.Basic (goal)
Goal:
R : Type u_1
inst : Monoid R
f : R → ℝ
hf : IsPowMul f
hf1 : HPow.hPow (β := ℕ) (f 1) 2 = f 1
h : f 1 = 1
⊢ f 1 ≤ 1
have inr : LE.le (α := ℝ) 1 1
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Data.Real.ConjExponents (goal)
Goal:
p q r : ℝ
h : p.HolderTriple q r
⊢ p⁻¹ + 0 < p⁻¹ + q⁻¹
have bc : 0 < q⁻¹
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Data.Real.ConjExponents (hypothesis)
Goal:
p q r : ℝ
h : p.HolderTriple q r
⊢ 0 < p / r
have this : 0 < p
Tactic: have := h.left_pos
-- Lean 4 proof step from Mathlib.Data.Real.ConjExponents (hypothesis)
Goal:
p q r : ℝ
h : p.HolderTriple q r
this : 0 < p
⊢ 0 < p / r
have this₁ : 0 < r
Tactic: have := h.pos'
-- Lean 4 proof step from Mathlib.Data.Real.ConjExponents (hypothesis)
Goal:
p q r : ℝ
h : p.HolderTriple q r
⊢ 0 < q / r
have this : 0 < q
Tactic: have := h.right_pos
-- Lean 4 proof step from Mathlib.Data.Real.ConjExponents (hypothesis)
Goal:
p q r : ℝ
h : p.HolderTriple q r
this : 0 < q
⊢ 0 < q / r
have this₁ : 0 < r
Tactic: have := h.pos'
-- Lean 4 proof step from Mathlib.Data.Real.ConjExponents (goal)
Goal:
p q : ℝ
h : p.HolderConjugate q
⊢ q = p / (p - 1)
have h₁ : p / (p - 1) = (1⁻¹ - p⁻¹)⁻¹
Tactic: convert! inv_inv q ▸ congr($(h.symm.inv_sub_inv_eq_inv.symm)⁻¹) using 1
-- Lean 4 proof step from Mathlib.Data.Real.ConjExponents (goal)
Goal:
p q : ℝ
h : p.HolderConjugate q
⊢ p / q = p - 1
have field_simp : p = q * (p - 1)
Tactic: field_simp [h.symm.ne_zero]
-- Lean 4 proof step from Mathlib.Data.Real.ConjExponents (goal)
Goal:
p q : ℝ
h : p.HolderConjugate q
⊢ (ENNReal.ofReal p)⁻¹ + (ENNReal.ofReal q)⁻¹ = 1
have rw : (ENNReal.ofReal p)⁻¹ + (ENNReal.ofReal q)⁻¹ = ENNReal.ofReal 1
Tactic: rw [← ENNReal.ofReal_one, ← ENNReal.ofReal_inv_of_pos h.pos,
    ← ENNReal.ofReal_inv_of_pos h.symm.pos, ← ENNReal.ofReal_add h.inv_nonneg h.symm.inv_nonneg,
    h.inv_add_inv_eq_one]
-- Lean 4 proof step from Mathlib.Data.Real.ConjExponents (goal)
Goal:
p q : ℝ
h : p.HolderConjugate q
rw : (ENNReal.ofReal p)⁻¹ + (ENNReal.ofReal q)⁻¹ = ENNReal.ofReal 1
⊢ (ENNReal.ofReal p)⁻¹ + (ENNReal.ofReal q)⁻¹ = 1
have rw₁ : ENNReal.ofReal p⁻¹ + (ENNReal.ofReal q)⁻¹ = ENNReal.ofReal 1
Tactic: rw [← ENNReal.ofReal_one, ← ENNReal.ofReal_inv_of_pos h.pos,
    ← ENNReal.ofReal_inv_of_pos h.symm.pos, ← ENNReal.ofReal_add h.inv_nonneg h.symm.inv_nonneg,
    h.inv_add_inv_eq_one]
-- Lean 4 proof step from Mathlib.Data.Real.ConjExponents (goal)
Goal:
p q : ℝ
h : p.HolderConjugate q
rw : (ENNReal.ofReal p)⁻¹ + (ENNReal.ofReal q)⁻¹ = ENNReal.ofReal 1
rw₁ : ENNReal.ofReal p⁻¹ + (ENNReal.ofReal q)⁻¹ = ENNReal.ofReal 1
⊢ (ENNReal.ofReal p)⁻¹ + (ENNReal.ofReal q)⁻¹ = 1
have rw₂ : ENNReal.ofReal p⁻¹ + ENNReal.ofReal q⁻¹ = ENNReal.ofReal 1
Tactic: rw [← ENNReal.ofReal_one, ← ENNReal.ofReal_inv_of_pos h.pos,
    ← ENNReal.ofReal_inv_of_pos h.symm.pos, ← ENNReal.ofReal_add h.inv_nonneg h.symm.inv_nonneg,
    h.inv_add_inv_eq_one]
-- Lean 4 proof step from Mathlib.Data.Real.ConjExponents (goal)
Goal:
p q : ℝ
h : p.HolderConjugate q
rw : (ENNReal.ofReal p)⁻¹ + (ENNReal.ofReal q)⁻¹ = ENNReal.ofReal 1
rw₁ : ENNReal.ofReal p⁻¹ + (ENNReal.ofReal q)⁻¹ = ENNReal.ofReal 1
rw₂ : ENNReal.ofReal p⁻¹ + ENNReal.ofReal q⁻¹ = ENNReal.ofReal 1
⊢ (ENNReal.ofReal p)⁻¹ + (ENNReal.ofReal q)⁻¹ = 1
have rw₃ : ENNReal.ofReal (p⁻¹ + q⁻¹) = ENNReal.ofReal 1
Tactic: rw [← ENNReal.ofReal_one, ← ENNReal.ofReal_inv_of_pos h.pos,
    ← ENNReal.ofReal_inv_of_pos h.symm.pos, ← ENNReal.ofReal_add h.inv_nonneg h.symm.inv_nonneg,
    h.inv_add_inv_eq_one]
-- Lean 4 proof step from Mathlib.Data.Real.ConjExponents (goal)
Goal:
p q : ℝ
h : p.HolderConjugate q
rw : (ENNReal.ofReal p)⁻¹ + (ENNReal.ofReal q)⁻¹ = ENNReal.ofReal 1
rw₁ : ENNReal.ofReal p⁻¹ + (ENNReal.ofReal q)⁻¹ = ENNReal.ofReal 1
rw₂ : ENNReal.ofReal p⁻¹ + ENNReal.ofReal q⁻¹ = ENNReal.ofReal 1
rw₃ : ENNReal.ofReal (p⁻¹ + q⁻¹) = ENNReal.ofReal 1
⊢ (ENNReal.ofReal p)⁻¹ + (ENNReal.ofReal q)⁻¹ = 1
have rw₄ : ENNReal.ofReal 1 = ENNReal.ofReal 1
Tactic: rw [← ENNReal.ofReal_one, ← ENNReal.ofReal_inv_of_pos h.pos,
    ← ENNReal.ofReal_inv_of_pos h.symm.pos, ← ENNReal.ofReal_add h.inv_nonneg h.symm.inv_nonneg,
    h.inv_add_inv_eq_one]
-- Lean 4 proof step from Mathlib.Data.Real.ConjExponents (goal)
Goal:
p q : ℝ
⊢ p.HolderConjugate q ↔ 1 < p ∧ p⁻¹ + q⁻¹ = 1
have refine : 1 < p ∧ p⁻¹ + q⁻¹ = 1 → p.HolderConjugate q
Tactic: refine ⟨fun h ↦ ⟨h.lt, h.inv_add_inv_eq_one⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Real.ConjExponents (hypothesis)
Goal:
p q : ℝ
hp : 1 < p
h : p⁻¹ + q⁻¹ = 1
⊢ p.HolderConjugate q
have hp' : 0 < p
Tactic: have hp' := zero_lt_one.trans hp
-- Lean 4 proof step from Mathlib.Data.Real.ConjExponents (goal)
Goal:
p q : ℝ
hp : 1 < p
h : p⁻¹ + q⁻¹ = 1
hp' : 0 < p
⊢ p.HolderConjugate q
have refine : 0 < q
Tactic: refine ⟨inv_one (G := ℝ) |>.symm ▸ h, hp', ?_⟩
-- Lean 4 proof step from Mathlib.Data.Real.ConjExponents (hypothesis)
Goal:
p q : ℝ
hp : 1 < p
h : p⁻¹ + q⁻¹ = 1
hp' : 0 < p
⊢ 0 < q
have hp₁ : 0 < 1 - p⁻¹
Tactic: rw [← inv_lt_one₀ hp', ← sub_pos] at hp
Cleared hypotheses: hp, h, hp'
-- Lean 4 proof step from Mathlib.Data.Real.ConjExponents (goal)
Goal:
p q r : ℝ≥0
⊢ (↑p : ℝ).HolderTriple (↑q : ℝ) (↑r : ℝ) ↔ p.HolderTriple q r
have rw_mod_cast : (↑p : ℝ)⁻¹ + (↑q : ℝ)⁻¹ = (↑r : ℝ)⁻¹ ∧ 0 < (↑p : ℝ) ∧ 0 < (↑q : ℝ) ↔ p.HolderTriple q r
Tactic: rw_mod_cast [Real.holderTriple_iff, holderTriple_iff]
-- Lean 4 proof step from Mathlib.Data.Real.ConjExponents (hypothesis)
Goal:
p q r : ℝ≥0
h : p.HolderTriple q r
⊢ r⁻¹ - q⁻¹ = p⁻¹
have this : q⁻¹ ≤ r⁻¹
Tactic: have := h.symm.inv_lt_inv.le
-- Lean 4 proof step from Mathlib.Data.Real.ConjExponents (hypothesis)
Goal:
p q r : ℝ≥0
h : p.HolderTriple q r
⊢ 0 < p / r
have this : 0 < p
Tactic: have := h.left_pos
-- Lean 4 proof step from Mathlib.Data.Real.ConjExponents (hypothesis)
Goal:
p q r : ℝ≥0
h : p.HolderTriple q r
this : 0 < p
⊢ 0 < p / r
have this₁ : 0 < r
Tactic: have := h.pos'
-- Lean 4 proof step from Mathlib.Data.Real.ConjExponents (hypothesis)
Goal:
p q r : ℝ≥0
h : p.HolderTriple q r
⊢ 0 < q / r
have this : 0 < q
Tactic: have := h.right_pos
-- Lean 4 proof step from Mathlib.Data.Real.ConjExponents (hypothesis)
Goal:
p q r : ℝ≥0
h : p.HolderTriple q r
this : 0 < q
⊢ 0 < q / r
have this₁ : 0 < r
Tactic: have := h.pos'
-- Lean 4 proof step from Mathlib.Data.Real.ConjExponents (hypothesis)
Goal:
p q : ℝ≥0
h : p.HolderConjugate q
⊢ q = p / (p - 1)
have this : (↑1 : ℝ) ≤ (↑p : ℝ)
Tactic: have : ((1 : ℝ≥0) : ℝ) ≤ p := h.coe.lt.le
-- Lean 4 proof step from Mathlib.Data.Real.ConjExponents (goal)
Goal:
p q : ℝ≥0
h : p.HolderConjugate q
⊢ p / q = p - 1
have field_simp : p = q * (p - 1)
Tactic: field_simp [h.symm.ne_zero]
-- Lean 4 proof step from Mathlib.Data.Real.ConjExponents (goal)
Goal:
p q : ℝ≥0
h : p.HolderConjugate q
⊢ (↑p⁻¹ : ℝ≥0∞) + (↑q⁻¹ : ℝ≥0∞) = 1
have norm_cast : p⁻¹ + q⁻¹ = 1
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Data.Real.ConjExponents (goal)
Goal:
p q : ℝ≥0
⊢ p.HolderConjugate q ↔ 1 < p ∧ p⁻¹ + q⁻¹ = 1
have rw : (↑1 : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ)⁻¹ + (↑q : ℝ)⁻¹ = (↑1 : ℝ) ↔ 1 < p ∧ p⁻¹ + q⁻¹ = 1
Tactic: rw [← holderConjugate_coe_iff, Real.holderConjugate_iff, ← coe_one]
-- Lean 4 proof step from Mathlib.Data.Real.ConjExponents (goal)
Goal:
p q : ℝ≥0
hp : 1 < p
⊢ p.HolderConjugate q ↔ q = p / (p - 1)
have rw : (↑q : ℝ) = (↑p : ℝ) / (↑(p - 1) : ℝ) ↔ q = p / (p - 1)
Tactic: rw [← holderConjugate_coe_iff, Real.holderConjugate_iff_eq_conjExponent (by exact_mod_cast hp),
    ← coe_one, ← NNReal.coe_sub hp.le]
-- Lean 4 proof step from Mathlib.Data.Real.ConjExponents (goal)
Goal:
p : ℝ≥0
hp : 1 < p
⊢ (↑(p / (p - 1)) : ℝ≥0∞) = 1 + (↑(p - 1) : ℝ≥0∞)⁻¹
have rw : (↑(p / (p - 1)) : ℝ≥0∞) = 1 + (↑(p - 1)⁻¹ : ℝ≥0∞)
Tactic: rw [← coe_inv (tsub_pos_of_lt hp).ne']
-- Lean 4 proof step from Mathlib.Data.Real.ConjExponents (goal)
Goal:
p : ℝ≥0
hp : 1 < p
⊢ (↑(p / (p - 1)) : ℝ≥0∞) = 1 + (↑(p - 1)⁻¹ : ℝ≥0∞)
have norm_cast : p / (p - 1) = 1 + (p - 1)⁻¹
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Data.Real.ConjExponents (goal)
Goal:
p : ℝ≥0
hp : 1 < p
⊢ p / (p - 1) = 1 + (p - 1)⁻¹
have field_simp : p = p - 1 + 1
Tactic: field_simp [(tsub_pos_of_lt hp).ne']
-- Lean 4 proof step from Mathlib.Data.Real.ConjExponents (goal)
Goal:
p : ℝ≥0
hp : 1 < p
⊢ p = p - 1 + 1
have rw : p = p
Tactic: rw [tsub_add_cancel_of_le hp.le]
-- Lean 4 proof step from Mathlib.Data.Real.ConjExponents (goal)
Goal:
p q r : ℝ≥0
hr : r ≠ 0
⊢ (↑p : ℝ≥0∞).HolderTriple (↑q : ℝ≥0∞) (↑r : ℝ≥0∞) ↔ p.HolderTriple q r
have refine_1 : ∀ (h : (↑p : ℝ≥0∞).HolderTriple (↑q : ℝ≥0∞) (↑r : ℝ≥0∞)), p.HolderTriple q r
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Data.Real.ConjExponents (goal)
Goal:
p q r : ℝ≥0
hr : r ≠ 0
refine_1 : ∀ (h : (↑p : ℝ≥0∞).HolderTriple (↑q : ℝ≥0∞) (↑r : ℝ≥0∞)), p.HolderTriple q r
⊢ (↑p : ℝ≥0∞).HolderTriple (↑q : ℝ≥0∞) (↑r : ℝ≥0∞) ↔ p.HolderTriple q r
have refine_2 : ∀ (h : p.HolderTriple q r), (↑p : ℝ≥0∞).HolderTriple (↑q : ℝ≥0∞) (↑r : ℝ≥0∞)
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Data.Real.ConjExponents (goal)
Goal:
p q r : ℝ≥0
hr : r ≠ 0
h : (↑p : ℝ≥0∞).HolderTriple (↑q : ℝ≥0∞) (↑r : ℝ≥0∞)
⊢ p.HolderTriple q r
have refine_1 : p⁻¹ + q⁻¹ = r⁻¹ ∧ 0 < p ∧ 0 < q
Tactic: rw [NNReal.holderTriple_iff]
-- Lean 4 proof step from Mathlib.Data.Real.ConjExponents (goal)
Goal:
p q r : ℝ≥0
hr : r ≠ 0
h : (↑p : ℝ≥0∞).HolderTriple (↑q : ℝ≥0∞) (↑r : ℝ≥0∞)
⊢ p ≠ 0 ∧ q ≠ 0
have left : p ≠ 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Real.ConjExponents (goal)
Goal:
p q r : ℝ≥0
hr : r ≠ 0
h : (↑p : ℝ≥0∞).HolderTriple (↑q : ℝ≥0∞) (↑r : ℝ≥0∞)
left : p ≠ 0
⊢ p ≠ 0 ∧ q ≠ 0
have right : q ≠ 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Real.ConjExponents (goal)
Goal:
q r : ℝ≥0
hr : r ≠ 0
h : (↑0 : ℝ≥0∞).HolderTriple (↑q : ℝ≥0∞) (↑r : ℝ≥0∞)
⊢ False
have left : r = 0
Tactic: apply hr
-- Lean 4 proof step from Mathlib.Data.Real.ConjExponents (goal)
Goal:
p r : ℝ≥0
hr : r ≠ 0
h : (↑p : ℝ≥0∞).HolderTriple (↑0 : ℝ≥0∞) (↑r : ℝ≥0∞)
⊢ False
have right : r = 0
Tactic: apply hr
-- 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∞)
⊢ p⁻¹ + q⁻¹ = r⁻¹ ∧ 0 < p ∧ 0 < q
have hp : p ≠ 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