[GOAL]
p q : ℝ
h : IsConjugateExponent p q
⊢ q = p / (p - 1)
[PROOFSTEP]
have := h.inv_add_inv_conj
[GOAL]
p q : ℝ
h : IsConjugateExponent p q
this : 1 / p + 1 / q = 1
⊢ q = p / (p - 1)
[PROOFSTEP]
rw [← eq_sub_iff_add_eq', one_div, inv_eq_iff_eq_inv] at this 
[GOAL]
p q : ℝ
h : IsConjugateExponent p q
this : q = (1 - 1 / p)⁻¹
⊢ q = p / (p - 1)
[PROOFSTEP]
field_simp [this, h.ne_zero]
[GOAL]
p q : ℝ
h : IsConjugateExponent p q
⊢ p * q = p + q
[PROOFSTEP]
simpa only [sub_mul, sub_eq_iff_eq_add, one_mul] using h.sub_one_mul_conj
[GOAL]
p q : ℝ
h : IsConjugateExponent p q
⊢ 1 < q
[PROOFSTEP]
rw [h.conj_eq]
[GOAL]
p q : ℝ
h : IsConjugateExponent p q
⊢ 1 < p / (p - 1)
[PROOFSTEP]
exact (one_lt_div h.sub_one_pos).mpr (sub_one_lt p)
[GOAL]
p q : ℝ
h : IsConjugateExponent p q
⊢ 1 / q + 1 / p = 1
[PROOFSTEP]
simpa [add_comm] using h.inv_add_inv_conj
[GOAL]
p q : ℝ
h : IsConjugateExponent p q
⊢ p / q = p - 1
[PROOFSTEP]
field_simp [h.symm.ne_zero]
[GOAL]
p q : ℝ
h : IsConjugateExponent p q
⊢ p = (p - 1) * q
[PROOFSTEP]
rw [h.sub_one_mul_conj]
[GOAL]
p q : ℝ
h : IsConjugateExponent p q
⊢ 1 < toNNReal p
[PROOFSTEP]
rw [← Real.toNNReal_one, Real.toNNReal_lt_toNNReal_iff h.pos]
[GOAL]
p q : ℝ
h : IsConjugateExponent p q
⊢ 1 < p
[PROOFSTEP]
exact h.one_lt
[GOAL]
p q : ℝ
h : IsConjugateExponent p q
⊢ 1 / toNNReal p + 1 / toNNReal q = 1
[PROOFSTEP]
rw [← Real.toNNReal_one, ← Real.toNNReal_div' h.nonneg, ← Real.toNNReal_div' h.symm.nonneg, ←
  Real.toNNReal_add h.one_div_nonneg h.symm.one_div_nonneg, h.inv_add_inv_conj]
[GOAL]
p q : ℝ
h : IsConjugateExponent p q
⊢ 1 / ENNReal.ofReal p + 1 / ENNReal.ofReal q = 1
[PROOFSTEP]
rw [← ENNReal.ofReal_one, ← ENNReal.ofReal_div_of_pos h.pos, ← ENNReal.ofReal_div_of_pos h.symm.pos, ←
  ENNReal.ofReal_add h.one_div_nonneg h.symm.one_div_nonneg, h.inv_add_inv_conj]
[GOAL]
p q : ℝ
h : 1 < p
H : q = p / (p - 1)
⊢ 1 / p + 1 / q = 1
[PROOFSTEP]
field_simp [H, ne_of_gt (lt_trans zero_lt_one h)]
[GOAL]
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ 1 < 1 / a
[PROOFSTEP]
rw [lt_div_iff ha, one_mul]
[GOAL]
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a < 1
[PROOFSTEP]
linarith
[GOAL]
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ 1 / (1 / a) + 1 / (1 / b) = 1
[PROOFSTEP]
simp_rw [one_div_one_div]
[GOAL]
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a + b = 1
[PROOFSTEP]
exact hab
