awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Real.Basic
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
h₁ : const abs ((↑f : ℕ → ℚ) i) < y
⊢ (↑((↑f : ℕ → ℚ) i) : ℝ) < mk y

Tactic:
rw [← mk_const, mk_lt]

Premises used: Real.mk_lt, Real.mk_const
-- Module: Mathlib.Data.Real.Basic
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

Tactic:
⟨_, half_pos K0, i, fun j ij => ?_⟩

Premises used: CauSeq.Pos, half_pos, And.intro, Exists.intro
-- Module: Mathlib.Data.Real.Basic
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
h₁ :
  ∀ (j : ℕ) (ij : j ≥ i),
    K / 2 ≤ (↑(HSub.hSub (β := CauSeq ℚ abs) y (const abs ((↑f : ℕ → ℚ) i) : CauSeq ℚ abs)) : ℕ → ℚ) j
⊢ const abs ((↑f : ℕ → ℚ) i) < y

Tactic:
refine ⟨_, half_pos K0, i, fun j ij => ?_⟩
-- Module: Mathlib.Data.Real.Basic
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 + -(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)
-- Module: Mathlib.Data.Real.Basic
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
h₄ h₅ h₆ h₇ :
  ∀ (this : K / 2 ≤ (↑y : ℕ → ℚ) 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

Tactic:
rwa [← sub_eq_add_neg, sub_self_div_two, sub_apply, sub_add_sub_cancel] at this

Premises used: sub_add_sub_cancel, sub_eq_add_neg, CauSeq.sub_apply, sub_self_div_two
-- Module: Mathlib.Data.Real.Basic
Goal:
f : CauSeq ℚ abs
x : ℝ
h : ∃ (i : ℕ), ∀ j ≥ i, (↑((↑f : ℕ → ℚ) j) : ℝ) ≤ x
obtain : ∀ (i : ℕ) (H : ∀ j ≥ i, (↑((↑f : ℕ → ℚ) j) : ℝ) ≤ x), mk f ≤ x
⊢ mk f ≤ x

Tactic:
obtain ⟨i, H⟩ := h
-- Module: Mathlib.Data.Real.Basic
Goal:
f : CauSeq ℚ abs
x : ℝ
i : ℕ
H : ∀ j ≥ i, (↑((↑f : ℕ → ℚ) j) : ℝ) ≤ x
rw : -x ≤ mk (-f)
⊢ mk f ≤ x

Tactic:
rw [← neg_le_neg_iff, ← mk_neg]

Premises used: Real.mk_neg, neg_le_neg_iff
-- Module: Mathlib.Data.Real.Basic
Goal:
f : CauSeq ℚ abs
x : ℝ
i : ℕ
H : ∀ j ≥ i, (↑((↑f : ℕ → ℚ) j) : ℝ) ≤ x
j : ℕ
ij : j ≥ i
⊢ -x ≤ (↑((↑(-f) : ℕ → ℚ) j) : ℝ)

Tactic:
simp [H _ ij]
-- Module: Mathlib.Data.Real.Basic
Goal:
f : CauSeq ℚ abs
x : ℝ
i : ℕ
H : ∀ j ≥ i, (↑((↑f : ℕ → ℚ) j) : ℝ) ≤ x
⊢ -x ≤ mk (-f)

Tactic:
exact le_mk_of_forall_le ⟨i, fun j ij => by simp [H _ ij]⟩

Premises used: Real.le_mk_of_forall_le, Exists.intro
-- Module: Mathlib.Data.Real.Basic
Goal:
f : CauSeq ℚ abs
x ε : ℝ
H : ∃ (i : ℕ), ∀ j ≥ i, |(↑((↑f : ℕ → ℚ) j) : ℝ) - x| ≤ ε
⊢ |mk f - x| ≤ ε

Tactic:
abs_sub_le_iff.2
    ⟨sub_le_iff_le_add'.2 <|
        mk_le_of_forall_le <|
          H.imp fun _ h j ij => sub_le_iff_le_add'.1 (abs_sub_le_iff.1 <| h j ij).1,
      sub_le_comm.1 <|
        le_mk_of_forall_le <| H.imp fun _ h j ij => sub_le_comm.1 (abs_sub_le_iff.1 <| h j ij).2⟩

Premises used: Iff.mpr, Real.mk_le_of_forall_le, Real.le_mk_of_forall_le, abs_sub_le_iff, Exists.imp, sub_le_comm, sub_le_iff_le_add', And.right, And.left, And.intro, Iff.mp
-- Module: Mathlib.Data.Real.Basic
Goal:
a : ℝ
ha : 0 ≤ a
b : ℕ
inl : ∀ (ha : LE.le (α := ℝ) 0 0), HMul.hMul (α := ℝ) 0 (↑b : ℝ) + 1 ≤ HAdd.hAdd (α := ℝ) 0 1 ^ b
inr : ∀ (ha' : 0 < a), a * (↑b : ℝ) + 1 ≤ (a + 1) ^ b
⊢ a * (↑b : ℝ) + 1 ≤ (a + 1) ^ b

Tactic:
rcases ha.eq_or_lt with rfl | ha'

Premises used: LE.le.eq_or_lt, rfl
-- Module: Mathlib.Data.Real.Basic
Goal:
b : ℕ
ha : LE.le (α := ℝ) 0 0
⊢ HMul.hMul (α := ℝ) 0 (↑b : ℝ) + 1 ≤ HAdd.hAdd (α := ℝ) 0 1 ^ b

Tactic:
simp
-- Module: Mathlib.Data.Real.Basic
Goal:
a : ℝ
ha' : 0 < a
⊢ a * (↑0 : ℝ) + 1 ≤ HPow.hPow (β := ℕ) (a + 1) 0

Tactic:
simp
-- Module: Mathlib.Data.Real.Basic
Goal:
b : ℕ
hb : ∀ {a : ℝ} (ha' : 0 < a), a * (↑b : ℝ) + 1 ≤ (a + 1) ^ b
a : ℝ
ha' : 0 < a
⊢ a * (↑(b + 1) : ℝ) + 1 = HAdd.hAdd (α := ℝ) 0 1 ^ b * a + (a * (↑b : ℝ) + 1)

Tactic:
simp [mul_add, add_assoc, add_left_comm]

Premises used: add_left_comm, add_assoc, mul_add
-- Module: Mathlib.Data.Real.Basic
Goal:
b : ℕ
hb : ∀ {a : ℝ} (ha' : 0 < a), a * (↑b : ℝ) + 1 ≤ (a + 1) ^ b
a : ℝ
ha' : 0 < a
h₁ : 0 ≤ HAdd.hAdd (α := ℝ) 0 1
h₂ : a * (↑b : ℝ) + 1 ≤ (a + 1) ^ b
⊢ HAdd.hAdd (α := ℝ) 0 1 ^ b * a + (a * (↑b : ℝ) + 1) ≤ (a + 1) ^ b * a + (a + 1) ^ b

Tactic:
gcongr
-- Module: Mathlib.Data.Real.Basic
Goal:
b : ℕ
hb : ∀ {a : ℝ} (ha' : 0 < a), a * (↑b : ℝ) + 1 ≤ (a + 1) ^ b
a : ℝ
ha' : 0 < a
⊢ 0 ≤ HAdd.hAdd (α := ℝ) 0 1

Tactic:
norm_num
-- Module: Mathlib.Data.Real.Basic
Goal:
b : ℕ
hb : ∀ {a : ℝ} (ha' : 0 < a), a * (↑b : ℝ) + 1 ≤ (a + 1) ^ b
a : ℝ
ha' : 0 < a
⊢ a * (↑b : ℝ) + 1 ≤ (a + 1) ^ b

Tactic:
hb ha'
-- Module: Mathlib.Data.Real.Basic
Goal:
b : ℕ
hb : ∀ {a : ℝ} (ha' : 0 < a), a * (↑b : ℝ) + 1 ≤ (a + 1) ^ b
a : ℝ
ha' : 0 < a
⊢ a * (↑b : ℝ) + 1 ≤ (a + 1) ^ b

Tactic:
exact hb ha'
-- Module: Mathlib.Data.Real.Basic
Goal:
b : ℕ
hb : ∀ {a : ℝ} (ha' : 0 < a), a * (↑b : ℝ) + 1 ≤ (a + 1) ^ b
a : ℝ
ha' : 0 < a
⊢ (a + 1) ^ b * a + (a + 1) ^ b = (a + 1) ^ (b + 1)

Tactic:
simp [pow_succ, mul_add]

Premises used: pow_succ, mul_add
-- Module: Mathlib.Data.Real.Basic
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₃ : (a + 1) ^ b * a + (a + 1) ^ b = (a + 1) ^ (b + 1)
⊢ a * (↑(b + 1) : ℝ) + 1 ≤ (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]

Premises used: HMul.hMul, Nat.cast, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Data.Real.Basic
Goal:
a : ℝ
b : ℕ
ha' : 0 < a
inr : ∀ {a : ℝ} (ha' : 0 < a), a * (↑0 : ℝ) + 1 ≤ HPow.hPow (β := ℕ) (a + 1) 0
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)
⊢ a * (↑b : ℝ) + 1 ≤ (a + 1) ^ b

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]

Premises used: HMul.hMul, _private.0.Real.zero, Nat.cast, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Data.Real.Basic
Goal:
R : Type u_1
inst : Monoid R
f : R → ℝ
hf : IsPowMul f
rw : HPow.hPow (β := ℕ) (f 1) 2
| f 1

Tactic:
rw [← one_pow 2, hf _ one_le_two]

Premises used: one_pow, one_le_two, OfNat.ofNat
-- Module: Mathlib.Data.Real.Basic
Goal:
R : Type u_1
inst : Monoid R
f : R → ℝ
hf : IsPowMul f
conv_rhs : HPow.hPow (β := ℕ) (f 1) 2 = f 1
conv_rhs₁ : HPow.hPow (β := ℕ) (f 1) 2 = HPow.hPow (β := ℕ) (f 1) 2
⊢ HPow.hPow (β := ℕ) (f 1) 2 = f 1

Tactic:
conv_rhs => rw [← one_pow 2, hf _ one_le_two]

Premises used: one_pow, one_le_two, OfNat.ofNat
-- Module: Mathlib.Data.Real.Basic
Goal:
R : Type u_1
inst : Monoid R
f : R → ℝ
hf : IsPowMul f
⊢ 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]
-- Module: Mathlib.Data.Real.Basic
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
inr : ∀ (h : f 1 = 1), f 1 ≤ 1
⊢ f 1 ≤ 1

Tactic:
rcases eq_zero_or_one_of_sq_eq_self hf1 with h | h

Premises used: eq_zero_or_one_of_sq_eq_self
-- Module: Mathlib.Data.Real.Basic
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
inl : LE.le (α := ℝ) 0 1
⊢ f 1 ≤ 1

Tactic:
rw [h]
-- Module: Mathlib.Data.Real.Basic
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
inr inr₁ : LE.le (α := ℝ) 1 1
⊢ f 1 ≤ 1

Tactic:
rw [h]
-- Module: Mathlib.Data.Real.Basic
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
⊢ LE.le (α := ℝ) 0 1

Tactic:
zero_le_one

Premises used: zero_le_one
-- Module: Mathlib.Data.Real.Basic
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
⊢ LE.le (α := ℝ) 0 1

Tactic:
exact zero_le_one

Premises used: zero_le_one
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q r : ℝ
h : p.HolderTriple q r
⊢ 0 < p

Tactic:
h.left_pos

Premises used: Real.HolderTriple.left_pos
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q r : ℝ
h : p.HolderTriple q r
⊢ 0 ≤ p

Tactic:
h.pos.le

Premises used: Real.HolderTriple.pos, LT.lt.le
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q r : ℝ
h : p.HolderTriple q r
⊢ p ≠ 0

Tactic:
h.pos.ne'

Premises used: Real.HolderTriple.pos, LT.lt.ne'
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q r : ℝ
h : p.HolderTriple q r
⊢ 0 < p⁻¹

Tactic:
inv_pos.2 h.pos

Premises used: Iff.mpr, Real.HolderTriple.pos, inv_pos
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q r : ℝ
h : p.HolderTriple q r
⊢ 0 ≤ p⁻¹

Tactic:
h.inv_pos.le

Premises used: LT.lt.le, Real.HolderTriple.inv_pos
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q r : ℝ
h : p.HolderTriple q r
⊢ p⁻¹ ≠ 0

Tactic:
h.inv_pos.ne'

Premises used: LT.lt.ne', Real.HolderTriple.inv_pos
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q r : ℝ
h : p.HolderTriple q r
⊢ 0 < 1 / p

Tactic:
_root_.one_div_pos.2 h.pos

Premises used: Iff.mpr, Real.HolderTriple.pos, one_div_pos
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q r : ℝ
h : p.HolderTriple q r
⊢ 0 ≤ 1 / p

Tactic:
le_of_lt h.one_div_pos

Premises used: le_of_lt, Real.HolderTriple.one_div_pos
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q r : ℝ
h : p.HolderTriple q r
⊢ 1 / p ≠ 0

Tactic:
ne_of_gt h.one_div_pos

Premises used: ne_of_gt, Real.HolderTriple.one_div_pos
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q r : ℝ
h : p.HolderTriple q r
⊢ 0 < r

Tactic:
inv_pos.mp <| h.inv_add_inv_eq_inv ▸ add_pos h.inv_pos h.symm.inv_pos

Premises used: Real.HolderTriple.inv_add_inv_eq_inv, add_pos, Eq.rec, inv_pos, Real.HolderTriple.symm, Real.HolderTriple.inv_pos, Iff.mp
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q r : ℝ
h : p.HolderTriple q r
⊢ 0 ≤ r

Tactic:
h.pos'.le

Premises used: LT.lt.le, Real.HolderTriple.pos'
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q r : ℝ
h : p.HolderTriple q r
⊢ r ≠ 0

Tactic:
h.pos'.ne'

Premises used: LT.lt.ne', Real.HolderTriple.pos'
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q r : ℝ
h : p.HolderTriple q r
⊢ 0 < r⁻¹

Tactic:
inv_pos.2 h.pos'

Premises used: Iff.mpr, inv_pos, Real.HolderTriple.pos'
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q r : ℝ
h : p.HolderTriple q r
⊢ 0 ≤ r⁻¹

Tactic:
h.inv_pos'.le

Premises used: LT.lt.le, Real.HolderTriple.inv_pos'
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q r : ℝ
h : p.HolderTriple q r
⊢ r⁻¹ ≠ 0

Tactic:
h.inv_pos'.ne'

Premises used: LT.lt.ne', Real.HolderTriple.inv_pos'
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q r : ℝ
h : p.HolderTriple q r
⊢ 0 < 1 / r

Tactic:
_root_.one_div_pos.2 h.pos'

Premises used: Iff.mpr, one_div_pos, Real.HolderTriple.pos'
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q r : ℝ
h : p.HolderTriple q r
⊢ 0 ≤ 1 / r

Tactic:
le_of_lt h.one_div_pos'

Premises used: le_of_lt, Real.HolderTriple.one_div_pos'
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q r : ℝ
h : p.HolderTriple q r
⊢ 1 / r ≠ 0

Tactic:
ne_of_gt h.one_div_pos'

Premises used: ne_of_gt, Real.HolderTriple.one_div_pos'
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q r : ℝ
h : p.HolderTriple q r
⊢ 0 < p ∧ 0 < q ∧ 0 < r

Tactic:
⟨h.pos, h.symm.pos, h.pos'⟩

Premises used: Real.HolderTriple.pos, Real.HolderTriple.symm, And.intro, Real.HolderTriple.pos'
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q r : ℝ
h : p.HolderTriple q r
⊢ r⁻¹ = p⁻¹ + q⁻¹

Tactic:
h.inv_add_inv_eq_inv.symm

Premises used: Real.HolderTriple.inv_add_inv_eq_inv, Eq.symm
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q r : ℝ
h : p.HolderTriple q r
⊢ 1 / p + 1 / q = 1 / r

Tactic:
simpa using h.inv_add_inv_eq_inv

Premises used: Real.HolderTriple.inv_add_inv_eq_inv
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q r : ℝ
h : p.HolderTriple q r
⊢ 1 / r = 1 / p + 1 / q

Tactic:
h.one_div_add_one_div.symm

Premises used: Real.HolderTriple.one_div_add_one_div, Eq.symm
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q r : ℝ
h : p.HolderTriple q r
⊢ (p⁻¹ + q⁻¹)⁻¹ = r

Tactic:
simp [h.inv_add_inv_eq_inv]

Premises used: Real.HolderTriple.inv_add_inv_eq_inv
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q r : ℝ
h : p.HolderTriple q r
bc : 0 < q⁻¹
⊢ p⁻¹ + 0 < p⁻¹ + q⁻¹

Tactic:
gcongr
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q r : ℝ
h : p.HolderTriple q r
⊢ 0 < q⁻¹

Tactic:
h.symm.inv_pos

Premises used: Real.HolderTriple.symm, Real.HolderTriple.inv_pos
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q r : ℝ
h : p.HolderTriple q r
⊢ 0 < q⁻¹

Tactic:
exact h.symm.inv_pos

Premises used: Real.HolderTriple.symm, Real.HolderTriple.inv_pos
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q r : ℝ
h : p.HolderTriple q r
⊢ r < p

Tactic:
simpa using inv_strictAnti₀ h.inv_pos h.inv_lt_inv

Premises used: Real.HolderTriple.inv_pos, inv_strictAnti₀, Real.HolderTriple.inv_lt_inv
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q r : ℝ
h : p.HolderTriple q r
⊢ r⁻¹ - q⁻¹ = p⁻¹

Tactic:
sub_eq_of_eq_add h.inv_eq

Premises used: Real.HolderTriple.inv_eq, sub_eq_of_eq_add
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q r : ℝ
h : p.HolderTriple q r
⊢ (p / r)⁻¹ + (q / r)⁻¹ = 1⁻¹

Tactic:
simp [div_eq_mul_inv, ← mul_add, h.inv_add_inv_eq_inv, h.ne_zero']

Premises used: Real.HolderTriple.inv_add_inv_eq_inv, div_eq_mul_inv, Real.HolderTriple.ne_zero', mul_add
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q r : ℝ
h : p.HolderTriple q r
⊢ 0 < p

Tactic:
have := h.left_pos
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q r : ℝ
h : p.HolderTriple q r
this : 0 < p
⊢ 0 < r

Tactic:
have := h.pos'
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q r : ℝ
h : p.HolderTriple q r
this_1 : 0 < p
this : 0 < r
⊢ 0 < p / r

Tactic:
positivity
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q r : ℝ
h : p.HolderTriple q r
⊢ 0 < q

Tactic:
have := h.right_pos
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q r : ℝ
h : p.HolderTriple q r
this : 0 < q
⊢ 0 < r

Tactic:
have := h.pos'
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q r : ℝ
h : p.HolderTriple q r
this_1 : 0 < q
this : 0 < r
⊢ 0 < q / r

Tactic:
positivity
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
⊢ HAdd.hAdd (α := ℝ) 2⁻¹ 2⁻¹ = 1⁻¹

Tactic:
norm_num
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q : ℝ
h : p.HolderConjugate q
⊢ q.HolderConjugate p

Tactic:
HolderTriple.symm h

Premises used: Real.HolderTriple.symm
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q : ℝ
h : p.HolderConjugate q
⊢ p⁻¹ + q⁻¹ = 1

Tactic:
inv_one (G := ℝ) ▸ h.inv_add_inv_eq_inv

Premises used: Real.HolderTriple.inv_add_inv_eq_inv, inv_one, Eq.rec
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q : ℝ
h : p.HolderConjugate q
⊢ 0 < p - 1

Tactic:
sub_pos.2 h.lt

Premises used: Iff.mpr, sub_pos, Real.HolderTriple.lt
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q : ℝ
h : p.HolderConjugate q
⊢ p - 1 ≠ 0

Tactic:
h.sub_one_pos.ne'

Premises used: LT.lt.ne', Real.HolderConjugate.sub_one_pos
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q : ℝ
h : p.HolderConjugate q
h₁ : p / (p - 1) = (1⁻¹ - p⁻¹)⁻¹
⊢ q = p / (p - 1)

Tactic:
convert! inv_inv q ▸ congr($(h.symm.inv_sub_inv_eq_inv.symm)⁻¹) using 1
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q : ℝ
h : p.HolderConjugate q
⊢ p / (p - 1) = (1⁻¹ - p⁻¹)⁻¹

Tactic:
field [h.ne_zero]

Premises used: Real.HolderTriple.ne_zero
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q : ℝ
h : p.HolderConjugate q
⊢ p.conjExponent = q

Tactic:
h.conjugate_eq.symm

Premises used: Real.HolderConjugate.conjugate_eq, Real.conjExponent, Eq.symm
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q : ℝ
h : p.HolderConjugate q
⊢ 1 - p⁻¹ = q⁻¹

Tactic:
sub_eq_of_eq_add h.symm.inv_add_inv_eq_one.symm

Premises used: Real.HolderConjugate.symm, Real.HolderConjugate.inv_add_inv_eq_one, sub_eq_of_eq_add, Eq.symm
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q : ℝ
h : p.HolderConjugate q
⊢ p⁻¹ - 1 = -q⁻¹

Tactic:
simpa using congr(-$(h.one_sub_inv))

Premises used: Real.HolderConjugate.one_sub_inv
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q : ℝ
h : p.HolderConjugate q
⊢ (p - 1) * q = p

Tactic:
mul_comm q (p - 1) ▸ (eq_div_iff h.sub_one_ne_zero).1 h.conjugate_eq

Premises used: Real.HolderConjugate.sub_one_ne_zero, HSub.hSub, Eq.rec, Real.HolderConjugate.conjugate_eq, Iff.mp, mul_comm, OfNat.ofNat, eq_div_iff
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q : ℝ
h : p.HolderConjugate q
⊢ p * q = p + q

Tactic:
simpa only [sub_mul, sub_eq_iff_eq_add, one_mul] using h.sub_one_mul_conj

Premises used: sub_mul, sub_eq_iff_eq_add, Real.HolderConjugate.sub_one_mul_conj, one_mul
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q : ℝ
h : p.HolderConjugate q
field_simp : p = q * (p - 1)
⊢ p / q = p - 1

Tactic:
field_simp [h.symm.ne_zero]

Premises used: Real.HolderTriple.ne_zero, Real.HolderConjugate.symm
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q : ℝ
h : p.HolderConjugate q
⊢ p = q * (p - 1)

Tactic:
linear_combination -h.sub_one_mul_conj

Premises used: Real.HolderConjugate.sub_one_mul_conj
-- Module: Mathlib.Data.Real.ConjExponents
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
rw₄ rw₅ : ENNReal.ofReal 1 = ENNReal.ofReal 1
⊢ (ENNReal.ofReal p)⁻¹ + (ENNReal.ofReal q)⁻¹ = 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]

Premises used: Real.HolderTriple.inv_nonneg, Real.HolderConjugate.symm, Real.HolderTriple.pos, ENNReal.ofReal_one, Real.HolderConjugate.inv_add_inv_eq_one, ENNReal.ofReal_inv_of_pos, ENNReal.ofReal_add
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q : ℝ
⊢ p.HolderConjugate q ↔ 1 < p ∧ p⁻¹ + q⁻¹ = 1

Tactic:
⟨fun h ↦ ⟨h.lt, h.inv_add_inv_eq_one⟩, ?_⟩

Premises used: Real.HolderConjugate.inv_add_inv_eq_one, And.intro, Iff.intro, Real.HolderTriple.lt
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q : ℝ
refine : 1 < p ∧ p⁻¹ + q⁻¹ = 1 → p.HolderConjugate q
⊢ p.HolderConjugate q ↔ 1 < p ∧ p⁻¹ + q⁻¹ = 1

Tactic:
refine ⟨fun h ↦ ⟨h.lt, h.inv_add_inv_eq_one⟩, ?_⟩
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q : ℝ
hp : 1 < p
h : p⁻¹ + q⁻¹ = 1
⊢ 0 < p

Tactic:
have hp' := zero_lt_one.trans hp
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q : ℝ
hp : 1 < p
h : p⁻¹ + q⁻¹ = 1
hp' : 0 < p
⊢ p.HolderConjugate q

Tactic:
⟨inv_one (G := ℝ) |>.symm ▸ h, hp', ?_⟩

Premises used: inv_one, Eq.rec, Real.HolderTriple.mk, Eq.symm
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q : ℝ
hp : 1 < p
h : p⁻¹ + q⁻¹ = 1
hp' : 0 < p
refine : 0 < q
⊢ p.HolderConjugate q

Tactic:
refine ⟨inv_one (G := ℝ) |>.symm ▸ h, hp', ?_⟩
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q : ℝ
hp : 1 < p
h : p⁻¹ + q⁻¹ = 1
hp' : 0 < p
⊢ 0 < 1 - p⁻¹

Tactic:
rw [← inv_lt_one₀ hp', ← sub_pos] at hp

Premises used: sub_pos, inv_lt_one₀
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q : ℝ
hp : 1 < p
h : p⁻¹ + q⁻¹ = 1
hp' : 0 < p
hp₁ : 0 < 1 - p⁻¹
⊢ p⁻¹ + q⁻¹ = 1

Tactic:
rw [← inv_lt_one₀ hp', ← sub_pos] at hp

Premises used: sub_pos, inv_lt_one₀
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q : ℝ
hp : 1 < p
h : p⁻¹ + q⁻¹ = 1
hp' : 0 < p
hp₁ : 0 < 1 - p⁻¹
h₁ : p⁻¹ + q⁻¹ = 1
⊢ 0 < p

Tactic:
rw [← inv_lt_one₀ hp', ← sub_pos] at hp

Premises used: sub_pos, inv_lt_one₀
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q : ℝ
hp : 0 < 1 - p⁻¹
h : p⁻¹ + q⁻¹ = 1
hp' : 0 < p
⊢ 0 < q

Tactic:
inv_pos.mp <| eq_sub_of_add_eq' h ▸ hp

Premises used: Eq.rec, inv_pos, eq_sub_of_add_eq', Iff.mp, Eq.symm
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q : ℝ
hp : 0 < 1 - p⁻¹
h : p⁻¹ + q⁻¹ = 1
hp' : 0 < p
⊢ 0 < q

Tactic:
exact inv_pos.mp <| eq_sub_of_add_eq' h ▸ hp

Premises used: inv_pos, Iff.mp
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a⁻¹⁻¹ + b⁻¹⁻¹ = 1⁻¹

Tactic:
simpa using hab
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
a : ℝ
ha₀ : 0 < a
ha₁ : a < 1
⊢ a⁻¹⁻¹ + (1 - a)⁻¹⁻¹ = 1

Tactic:
simp
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
a : ℝ
ha₀ : 0 < a
ha₁ : a < 1
⊢ (1 - a)⁻¹.HolderConjugate a⁻¹

Tactic:
(inv_one_sub_inv ha₀ ha₁).symm

Premises used: Real.HolderConjugate.symm, Real.HolderConjugate.inv_one_sub_inv
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q : ℝ
⊢ p.HolderConjugate q ↔ q.HolderConjugate p

Tactic:
⟨.symm, .symm⟩

Premises used: Real.HolderConjugate.symm, Iff.intro
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q : ℝ
hp : 1 < p
h : q = p / (p - 1)
⊢ p⁻¹ + q⁻¹ = 1

Tactic:
simp [field, h]
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p : ℝ
h : 1 < p
⊢ p.HolderConjugate p.conjExponent

Tactic:
(holderConjugate_iff_eq_conjExponent h).2 rfl

Premises used: Iff.mpr, Real.holderConjugate_iff_eq_conjExponent, rfl
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ (1 / a).HolderConjugate (1 / b)

Tactic:
simpa using HolderConjugate.inv_inv ha hb hab

Premises used: Real.HolderConjugate.inv_inv
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q r : ℝ≥0
rw_mod_cast rw_mod_cast₁ rw_mod_cast₂ :
  (↑p : ℝ)⁻¹ + (↑q : ℝ)⁻¹ = (↑r : ℝ)⁻¹ ∧ 0 < (↑p : ℝ) ∧ 0 < (↑q : ℝ) ↔ p.HolderTriple q r
⊢ (↑p : ℝ).HolderTriple (↑q : ℝ) (↑r : ℝ) ↔ p.HolderTriple q r

Tactic:
rw_mod_cast [Real.holderTriple_iff, holderTriple_iff]

Premises used: Real.holderTriple_iff, NNReal.holderTriple_iff
-- Module: Mathlib.Data.Real.ConjExponents
Goal:
p q : ℝ≥0
⊢ (↑p : ℝ).HolderConjugate (↑q : ℝ) ↔ p.HolderConjugate q

Tactic:
holderTriple_coe_iff (r := 1)

Premises used: NNReal.holderTriple_coe_iff, NNReal.toReal