awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Group.Rat
Goal:
m : ℤ
⊢ norm (E := ℝ) (↑(↑m : ℚ) : ℝ) = norm (E := ℝ) (↑m : ℝ)

Tactic:
congr 1
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp.Completion
Goal:
V : SemiNormedGrp
⊢ CompleteSpace.{u_1} (completion.obj V).carrier

Tactic:
Completion.completeSpace _

Premises used: UniformSpace.Completion.completeSpace, Quotient, SeparationQuotient, UniformSpace.Completion
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp.Completion
Goal:
V : SemiNormedGrp
v : V.carrier
⊢ norm (E := Completion V.carrier) (↑v : Completion V.carrier) ≤ 1 * ‖v‖

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp.Completion
Goal:
V : SemiNormedGrp
v : V.carrier
⊢ norm (E := (completion.obj V).carrier)
      ((ConcreteCategory.hom (FC := fun (x1 x2 : SemiNormedGrp.{u_1}) ↦ NormedAddGroupHom x1.carrier x2.carrier) (CC :=
              carrier) (X := V) incl :
            (a : V.carrier) → (completion.obj V).carrier)
          v :
        (completion.obj V).carrier) =
    ‖v‖

Tactic:
UniformSpace.Completion.norm_coe _

Premises used: UniformSpace.Completion.coe', UniformSpace.Completion.norm_coe, SeparationQuotient.mk
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp.Completion
Goal:
V W : SemiNormedGrp
f : V ⟶ W
hf : (Hom.hom f).NormNoninc
⊢ (Hom.hom (completion.map f)).NormNoninc

Tactic:
NormedAddGroupHom.NormNoninc.normNoninc_iff_norm_le_one.2 <|
    (NormedAddGroupHom.norm_completion f.hom).le.trans <|
      NormedAddGroupHom.NormNoninc.normNoninc_iff_norm_le_one.1 hf

Premises used: Iff.mpr, NormedAddGroupHom.NormNoninc.normNoninc_iff_norm_le_one, NormedAddGroupHom.norm_completion, Eq.le, SemiNormedGrp.Hom.hom, Iff.mp, LE.le.trans
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp.Completion
Goal:
V W : SemiNormedGrp
⊢ Eq (α := completion.obj V ⟶ completion.obj W) (completion.map 0) 0

Tactic:
(completion.mapHom V W).map_zero

Premises used: AddMonoidHom.map_zero, SemiNormedGrp.completion.mapHom
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp.Completion
Goal:
V W : SemiNormedGrp
inst : CompleteSpace.{u_1} W.carrier
inst_1 : T0Space.{u_1} W.carrier
f : V ⟶ W
⊢ incl ≫ lift f = f

Tactic:
ext <| NormedAddGroupHom.extension_coe _

Premises used: NormedAddGroupHom.extension_coe, SemiNormedGrp.ext
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp.Completion
Goal:
V W : SemiNormedGrp
inst : CompleteSpace.{u_1} W.carrier
inst_1 : T0Space.{u_1} W.carrier
f : V ⟶ W
g : completion.obj V ⟶ W
⊢ incl ≫ g = f → g = lift f

Tactic:
fun h => SemiNormedGrp.hom_ext (NormedAddGroupHom.extension_unique _ fun v =>
    ((SemiNormedGrp.ext_iff.1 h) v).symm).symm

Premises used: CategoryTheory.ConcreteCategory.hom, SemiNormedGrp.ext_iff, SemiNormedGrp.hom_ext, NormedAddGroupHom.extension_unique, Iff.mp, Eq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p t : ℝ
⊢ p.rpowIntegrand₀₁ t 0 = 0

Tactic:
simp [rpowIntegrand₀₁]

Premises used: Real.rpowIntegrand₀₁
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p x : ℝ
hp : 0 < p
⊢ p.rpowIntegrand₀₁ 0 x = 0

Tactic:
simp [rpowIntegrand₀₁, Real.zero_rpow hp.ne']

Premises used: Real.zero_rpow, Real.rpowIntegrand₀₁, LT.lt.ne'
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p t : ℝ
hp : p ≠ 1
ht : 0 < t
h : ∀ (x : ℝ), t ^ p * (t⁻¹ - (t + x)⁻¹) = t ^ (p - 1) - t ^ p * (t + x)⁻¹
⊢ Eq (α := (x : ℝ) → ℝ) (fun (x : ℝ) ↦ t ^ p * (t⁻¹ - (t + x)⁻¹)) fun (x : ℝ) ↦ t ^ (p - 1) - t ^ p * (t + x)⁻¹

Tactic:
ext x
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p t : ℝ
hp : p ≠ 1
ht : 0 < t
x : ℝ
⊢ 0 ≤ t

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p t : ℝ
hp : p ≠ 1
ht : 0 < t
x : ℝ
⊢ p + -1 ≠ 0

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p t : ℝ
hp : p ≠ 1
ht : 0 < t
x : ℝ
h : t ^ (p + -1) - t ^ p * (t + x)⁻¹ = t ^ (p - 1) - t ^ p * (t + x)⁻¹
⊢ t ^ p * (t⁻¹ - (t + x)⁻¹) = t ^ (p - 1) - t ^ p * (t + x)⁻¹

Tactic:
rw [mul_sub, ← rpow_neg_one, ← rpow_add' (by grind) (by grind)]

Premises used: Real.rpow_neg_one, mul_sub, Real.rpow_add'
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p t : ℝ
hp : p ≠ 1
ht : 0 < t
x : ℝ
⊢ t ^ (p + -1) - t ^ p * (t + x)⁻¹ = t ^ (p - 1) - t ^ p * (t + x)⁻¹

Tactic:
grind only
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p t x : ℝ
hp : 0 < p
ht : 0 ≤ t
hx : 0 ≤ x
ht_zero : t = 0
⊢ 0 ≤ t ^ p * (t⁻¹ - (t + x)⁻¹)

Tactic:
simp [ht_zero, Real.zero_rpow (ne_of_gt hp)]

Premises used: ne_of_gt, Real.zero_rpow
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p t x : ℝ
hp : 0 < p
ht : 0 ≤ t
hx : 0 ≤ x
ht_pos : 0 < t
⊢ 0 ≤ t ^ p

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p t x : ℝ
hp : 0 < p
ht : 0 ≤ t
hx : 0 ≤ x
ht_pos : 0 < t
inr : 0 ≤ t⁻¹ - (t + x)⁻¹
⊢ 0 ≤ t ^ p * (t⁻¹ - (t + x)⁻¹)

Tactic:
refine mul_nonneg (by positivity) ?_

Premises used: mul_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p t x : ℝ
hp : 0 < p
ht : 0 ≤ t
hx : 0 ≤ x
ht_pos : 0 < t
inr : (t + x)⁻¹ ≤ t⁻¹
⊢ 0 ≤ t⁻¹ - (t + x)⁻¹

Tactic:
rw [sub_nonneg]

Premises used: sub_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p t x : ℝ
hp : 0 < p
ht : 0 ≤ t
hx : 0 ≤ x
ht_pos : 0 < t
inr : t ≤ t + x
⊢ (t + x)⁻¹ ≤ t⁻¹

Tactic:
gcongr
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p t x : ℝ
hp : 0 < p
ht : 0 ≤ t
hx : 0 ≤ x
ht_pos : 0 < t
linarith : t + x < t → 0 - x + (t + x - t) = 0
⊢ t ≤ t + x

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p t x : ℝ
hp : 0 < p
ht : 0 ≤ t
hx : 0 ≤ x
⊢ t = 0 ∨ 0 < t

Tactic:
cases eq_or_lt_of_le' ht with
  | inl ht_zero => simp [ht_zero, Real.zero_rpow (ne_of_gt hp)]
  | inr ht_pos =>
    refine mul_nonneg (by positivity) ?_
    rw [sub_nonneg]
    gcongr
    linarith

Premises used: mul_nonneg, ne_of_gt, eq_or_lt_of_le', Real.zero_rpow, sub_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p t x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 ≤ t
hx : 0 ≤ x
by_cases : ∀ (ht' : t = 0), p.rpowIntegrand₀₁ t x = t ^ (p - 1) * x / (t + x)
by_cases₁ : ∀ (ht' : ¬t = 0), p.rpowIntegrand₀₁ t x = t ^ (p - 1) * x / (t + x)
⊢ p.rpowIntegrand₀₁ t x = t ^ (p - 1) * x / (t + x)

Tactic:
by_cases ht' : t = 0
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p t x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 ≤ t
hx : 0 ≤ x
ht' : ¬t = 0
⊢ t + x ≠ 0

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p t x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 ≤ t
hx : 0 ≤ x
ht' : ¬t = 0
⊢ t + x ≠ 0

Tactic:
have hxt : t + x ≠ 0 := by positivity
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p t x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 ≤ t
hx : 0 ≤ x
ht' : ¬t = 0
hxt : t + x ≠ 0
⊢ t ^ p * (t⁻¹ - (t + x)⁻¹) = t ^ p * (t⁻¹ - (t + x)⁻¹)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p t x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 ≤ t
hx : 0 ≤ x
ht' : ¬t = 0
hxt : t + x ≠ 0
simp : t ^ p * (1 / t - 1 / (t + x)) = t ^ p * ((t + x - t) / (t * (t + x)))
⊢ t ^ p * (t⁻¹ - (t + x)⁻¹) = t ^ p * ((t + x - t) / (t * (t + x)))

Tactic:
simp only [inv_eq_one_div]

Premises used: inv_eq_one_div
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p t x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 ≤ t
hx : 0 ≤ x
ht' : ¬t = 0
hxt : t + x ≠ 0
⊢ t ≠ 0

Tactic:
lia
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p t x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 ≤ t
hx : 0 ≤ x
ht' : ¬t = 0
hxt : t + x ≠ 0
⊢ t + x ≠ 0

Tactic:
lia
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p t x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 ≤ t
hx : 0 ≤ x
ht' : ¬t = 0
hxt : t + x ≠ 0
rw : t ^ p * ((1 * (t + x) - t * 1) / (t * (t + x))) = t ^ p * ((t + x - t) / (t * (t + x)))
⊢ t ^ p * (1 / t - 1 / (t + x)) = t ^ p * ((t + x - t) / (t * (t + x)))

Tactic:
rw [div_sub_div _ _ (by lia) (by lia)]

Premises used: div_sub_div
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p t x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 ≤ t
hx : 0 ≤ x
ht' : ¬t = 0
hxt : t + x ≠ 0
⊢ t ^ p * ((1 * (t + x) - t * 1) / (t * (t + x))) = t ^ p * ((t + x - t) / (t * (t + x)))

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p t x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 ≤ t
hx : 0 ≤ x
ht' : ¬t = 0
hxt : t + x ≠ 0
⊢ t ^ p * ((t + x - t) / (t * (t + x))) = t ^ p / t * x / (t + x)

Tactic:
simp [field]
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p t x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 ≤ t
hx : 0 ≤ x
ht' : ¬t = 0
hxt : t + x ≠ 0
e_a : t ^ p / t = t ^ (p - 1)
⊢ t ^ p / t * x / (t + x) = t ^ (p - 1) * x / (t + x)

Tactic:
congr
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p t x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 ≤ t
hx : 0 ≤ x
ht' : ¬t = 0
hxt : t + x ≠ 0
⊢ t ^ p / t = t ^ (p - 1)

Tactic:
(Real.rpow_sub_one ht' p).symm

Premises used: Real.rpow_sub_one, Eq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p t x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 ≤ t
hx : 0 ≤ x
ht' : ¬t = 0
hxt : t + x ≠ 0
⊢ t ^ p / t = t ^ (p - 1)

Tactic:
exact (Real.rpow_sub_one ht' p).symm

Premises used: Real.rpow_sub_one, Eq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p t x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 ≤ t
hx : 0 ≤ x
ht' : ¬t = 0
hxt : t + x ≠ 0
calc : t ^ p * (t⁻¹ - (t + x)⁻¹) = t ^ p * ((t + x - t) / (t * (t + x)))
calc₁ : t ^ p * ((t + x - t) / (t * (t + x))) = t ^ p / t * x / (t + x)
calc₂ : t ^ p / t * x / (t + x) = t ^ (p - 1) * x / (t + x)
⊢ p.rpowIntegrand₀₁ t x = t ^ (p - 1) * x / (t + x)

Tactic:
calc _ = (t : ℝ) ^ p * (t⁻¹ - (t + x)⁻¹) := rfl
      _ = (t : ℝ) ^ p * ((t + x - t) / (t * (t + x))) := by
          simp only [inv_eq_one_div]
          rw [div_sub_div _ _ (by lia) (by lia)]
          simp
      _ = t ^ p / t * x / (t + x) := by simp [field]
      _ = t ^ (p - 1) * x / (t + x) := by congr; exact (Real.rpow_sub_one ht' p).symm

Premises used: HMul.hMul, HSub.hSub, HDiv.hDiv, Inv.inv, HAdd.hAdd, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p t x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 ≤ t
hx : 0 ≤ x
ht' : ¬t = 0
⊢ p.rpowIntegrand₀₁ t x = t ^ (p - 1) * x / (t + x)

Tactic:
case neg =>
    have hxt : t + x ≠ 0 := by positivity
    calc _ = (t : ℝ) ^ p * (t⁻¹ - (t + x)⁻¹) := rfl
      _ = (t : ℝ) ^ p * ((t + x - t) / (t * (t + x))) := by
          simp only [inv_eq_one_div]
          rw [div_sub_div _ _ (by lia) (by lia)]
          simp
      _ = t ^ p / t * x / (t + x) := by simp [field]
      _ = t ^ (p - 1) * x / (t + x) := by congr; exact (Real.rpow_sub_one ht' p).symm

Premises used: HMul.hMul, HSub.hSub, HDiv.hDiv, Inv.inv, HAdd.hAdd, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p t x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 ≤ t
hx : 0 ≤ x
ht' : t = 0
⊢ 0 < p ∧ p < 1

Tactic:
push _ ∈ _ at hp
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p t x : ℝ
ht : 0 ≤ t
hx : 0 ≤ x
ht' : t = 0
hp : 0 < p ∧ p < 1
linarith : p - 1 = 0 → p - 1 + -(p - 1 - 0) = 0
⊢ p - 1 ≠ 0

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p t x : ℝ
ht : 0 ≤ t
hx : 0 ≤ x
ht' : t = 0
hp : 0 < p ∧ p < 1
⊢ p - 1 ≠ 0

Tactic:
have hp₂ : p - 1 ≠ 0 := by linarith
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p t x : ℝ
ht : 0 ≤ t
hx : 0 ≤ x
ht' : t = 0
hp : 0 < p ∧ p < 1
hp₂ : p - 1 ≠ 0
⊢ p.rpowIntegrand₀₁ t x = t ^ (p - 1) * x / (t + x)

Tactic:
simp [rpowIntegrand₀₁, ht', hp.1.ne', hp₂]

Premises used: Real.rpowIntegrand₀₁, LT.lt.ne', And.left
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p t x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 ≤ t
hx : 0 ≤ x
ht' : t = 0
case : ∀ (hp : 0 < p ∧ p < 1), p.rpowIntegrand₀₁ t x = t ^ (p - 1) * x / (t + x)
case₁ : ∀ (hp : 0 < p ∧ p < 1) (hp₂ : p - 1 ≠ 0), p.rpowIntegrand₀₁ t x = t ^ (p - 1) * x / (t + x)
⊢ p.rpowIntegrand₀₁ t x = t ^ (p - 1) * x / (t + x)

Tactic:
case pos =>
    push _ ∈ _ at hp
    have hp₂ : p - 1 ≠ 0 := by linarith
    simp [rpowIntegrand₀₁, ht', hp.1.ne', hp₂]

Premises used: Real.rpowIntegrand₀₁, LT.lt.ne', And.left
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
hx : 0 ≤ x
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioi 0) t
⊢ Eq (α := ℝ) ((fun (x_1 : ℝ) ↦ p.rpowIntegrand₀₁ x_1 x) t) ((fun (t : ℝ) ↦ t ^ (p - 1) * x / (t + x)) t)

Tactic:
simp [rpowIntegrand₀₁_eq_pow_div hp (le_of_lt ht) hx]

Premises used: le_of_lt, Real.rpowIntegrand₀₁_eq_pow_div
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p t x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 ≤ t
hx : 0 ≤ x
⊢ 0 ≤ x * t

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p t x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 ≤ t
hx : 0 ≤ x
⊢ 0 ≤ x * t

Tactic:
have hxt : 0 ≤ x * t := by positivity
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p t x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 ≤ t
hx : 0 ≤ x
hxt : 0 ≤ x * t
rw : (x * t) ^ (p - 1) * x / (x * t + x) = t ^ (p - 1) * 1 / (t + 1) * x ^ (p - 1)
⊢ p.rpowIntegrand₀₁ (x * t) x = p.rpowIntegrand₀₁ t 1 * x ^ (p - 1)

Tactic:
rw [rpowIntegrand₀₁_eq_pow_div hp hxt hx, rpowIntegrand₀₁_eq_pow_div hp ht zero_le_one]

Premises used: zero_le_one, Real.rpowIntegrand₀₁_eq_pow_div
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p t x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 ≤ t
hx : 0 ≤ x
hxt : 0 ≤ x * t
by_cases : ∀ (hx_zero : x = 0), (x * t) ^ (p - 1) * x / (x * t + x) = t ^ (p - 1) * 1 / (t + 1) * x ^ (p - 1)
by_cases₁ : ∀ (hx_zero : ¬x = 0), (x * t) ^ (p - 1) * x / (x * t + x) = t ^ (p - 1) * 1 / (t + 1) * x ^ (p - 1)
⊢ (x * t) ^ (p - 1) * x / (x * t + x) = t ^ (p - 1) * 1 / (t + 1) * x ^ (p - 1)

Tactic:
by_cases hx_zero : x = 0
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p t x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 ≤ t
hx : 0 ≤ x
hxt : 0 ≤ x * t
hx_zero : ¬x = 0
rw : (x * t) ^ (p - 1) * x / (x * t + x) = x ^ (p - 1) * t ^ (p - 1) * (x / (x * t + x))
rw₁ : (x * t) ^ (p - 1) * (x / (x * t + x)) = x ^ (p - 1) * t ^ (p - 1) * (x / (x * t + x))
rw₂ rw₃ : x ^ (p - 1) * t ^ (p - 1) * (x / (x * t + x)) = x ^ (p - 1) * t ^ (p - 1) * (x / (x * t + x))
⊢ (x * t) ^ (p - 1) * x / (x * t + x) = x ^ (p - 1) * (t ^ (p - 1) * (x / (x * t + x)))

Tactic:
rw [← mul_assoc, mul_div_assoc, Real.mul_rpow hx ht]

Premises used: mul_assoc, mul_div_assoc, Real.mul_rpow
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p t x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 ≤ t
hx : 0 ≤ x
hxt : 0 ≤ x * t
hx_zero : ¬x = 0
⊢ x * t + x = x * (t + 1)

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p t x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 ≤ t
hx : 0 ≤ x
hxt : 0 ≤ x * t
hx_zero : ¬x = 0
⊢ x * t + x = x * (t + 1)

Tactic:
have : x * t + x = x * (t + 1) := by ring
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p t x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 ≤ t
hx : 0 ≤ x
hxt : 0 ≤ x * t
hx_zero : ¬x = 0
this : x * t + x = x * (t + 1)
rw : x ^ (p - 1) * (t ^ (p - 1) * (x / (x * t + x))) = x ^ (p - 1) * (t ^ (p - 1) * (1 / (t + 1)))
rw₁ : x ^ (p - 1) * (t ^ (p - 1) * (x / (x * (t + 1)))) = x ^ (p - 1) * (t ^ (p - 1) * (1 / (t + 1)))
rw₂ : x ^ (p - 1) * (t ^ (p - 1) * (x / x * (1 / (t + 1)))) = x ^ (p - 1) * (t ^ (p - 1) * (1 / (t + 1)))
rw₃ : x ^ (p - 1) * (t ^ (p - 1) * (1 * (1 / (t + 1)))) = x ^ (p - 1) * (t ^ (p - 1) * (1 / (t + 1)))
rw₄ rw₅ : x ^ (p - 1) * (t ^ (p - 1) * (1 / (t + 1))) = x ^ (p - 1) * (t ^ (p - 1) * (1 / (t + 1)))
⊢ x ^ (p - 1) * (t ^ (p - 1) * (x / (x * t + x))) = x ^ (p - 1) * (t ^ (p - 1) * 1 / (t + 1))

Tactic:
rw [mul_div_assoc, this, div_mul_eq_div_mul_one_div, div_self hx_zero, one_mul]

Premises used: mul_div_assoc, div_mul_eq_div_mul_one_div, one_mul, div_self
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p t x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 ≤ t
hx : 0 ≤ x
hxt : 0 ≤ x * t
hx_zero : ¬x = 0
rw rw₁ : t ^ (p - 1) * 1 / (t + 1) * x ^ (p - 1) = t ^ (p - 1) * 1 / (t + 1) * x ^ (p - 1)
⊢ x ^ (p - 1) * (t ^ (p - 1) * 1 / (t + 1)) = t ^ (p - 1) * 1 / (t + 1) * x ^ (p - 1)

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p t x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 ≤ t
hx : 0 ≤ x
hxt : 0 ≤ x * t
hx_zero : ¬x = 0
calc : (x * t) ^ (p - 1) * x / (x * t + x) = x ^ (p - 1) * (t ^ (p - 1) * (x / (x * t + x)))
calc₁ : x ^ (p - 1) * (t ^ (p - 1) * (x / (x * t + x))) = x ^ (p - 1) * (t ^ (p - 1) * 1 / (t + 1))
calc₂ : x ^ (p - 1) * (t ^ (p - 1) * 1 / (t + 1)) = t ^ (p - 1) * 1 / (t + 1) * x ^ (p - 1)
⊢ (x * t) ^ (p - 1) * x / (x * t + x) = t ^ (p - 1) * 1 / (t + 1) * x ^ (p - 1)

Tactic:
calc _ = x ^ (p - 1) * (t ^ (p - 1) * (x / (x * t + x))) := by
              rw [← mul_assoc, mul_div_assoc, Real.mul_rpow hx ht]
      _ = x ^ (p - 1) * (t ^ (p - 1) * 1 / (t + 1)) := by
              have : x * t + x = x * (t + 1) := by ring
              rw [mul_div_assoc, this, div_mul_eq_div_mul_one_div, div_self hx_zero, one_mul]
      _ = t ^ (p - 1) * 1 / (t + 1) * x ^ (p - 1) := by rw [mul_comm]

Premises used: HMul.hMul, HSub.hSub, HDiv.hDiv, HPow.hPow, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p t x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 ≤ t
hx : 0 ≤ x
hxt : 0 ≤ x * t
hx_zero : ¬x = 0
⊢ (x * t) ^ (p - 1) * x / (x * t + x) = t ^ (p - 1) * 1 / (t + 1) * x ^ (p - 1)

Tactic:
case neg =>
    calc _ = x ^ (p - 1) * (t ^ (p - 1) * (x / (x * t + x))) := by
              rw [← mul_assoc, mul_div_assoc, Real.mul_rpow hx ht]
      _ = x ^ (p - 1) * (t ^ (p - 1) * 1 / (t + 1)) := by
              have : x * t + x = x * (t + 1) := by ring
              rw [mul_div_assoc, this, div_mul_eq_div_mul_one_div, div_self hx_zero, one_mul]
      _ = t ^ (p - 1) * 1 / (t + 1) * x ^ (p - 1) := by rw [mul_comm]

Premises used: HMul.hMul, HSub.hSub, HDiv.hDiv, HPow.hPow, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p t x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 ≤ t
hx : 0 ≤ x
hxt : 0 ≤ x * t
hx_zero : x = 0
⊢ 0 < p ∧ p < 1

Tactic:
rw [mem_Ioo] at hp

Premises used: Set.mem_Ioo
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p t x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 ≤ t
hx : 0 ≤ x
hxt : 0 ≤ x * t
hx_zero : x = 0
hp₁ : 0 < p ∧ p < 1
⊢ 0 ≤ t

Tactic:
rw [mem_Ioo] at hp

Premises used: Set.mem_Ioo
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p t x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 ≤ t
hx : 0 ≤ x
hxt : 0 ≤ x * t
hx_zero : x = 0
hp₁ : 0 < p ∧ p < 1
ht₁ : 0 ≤ t
⊢ 0 ≤ x

Tactic:
rw [mem_Ioo] at hp

Premises used: Set.mem_Ioo
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p t x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 ≤ t
hx : 0 ≤ x
hxt : 0 ≤ x * t
hx_zero : x = 0
hp₁ : 0 < p ∧ p < 1
ht₁ : 0 ≤ t
hx₁ : 0 ≤ x
⊢ 0 ≤ x * t

Tactic:
rw [mem_Ioo] at hp

Premises used: Set.mem_Ioo
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p t x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 ≤ t
hx : 0 ≤ x
hxt : 0 ≤ x * t
hx_zero : x = 0
hp₁ : 0 < p ∧ p < 1
ht₁ : 0 ≤ t
hx₁ : 0 ≤ x
hxt₁ : 0 ≤ x * t
⊢ x = 0

Tactic:
rw [mem_Ioo] at hp

Premises used: Set.mem_Ioo
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p t x : ℝ
hp : 0 < p ∧ p < 1
ht : 0 ≤ t
hx : 0 ≤ x
hxt : 0 ≤ x * t
hx_zero : x = 0
linarith : p - 1 = 0 → p - 1 + -(p - 1 - 0) = 0
⊢ p - 1 ≠ 0

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p t x : ℝ
hp : 0 < p ∧ p < 1
ht : 0 ≤ t
hx : 0 ≤ x
hxt : 0 ≤ x * t
hx_zero : x = 0
⊢ (x * t) ^ (p - 1) * x / (x * t + x) = t ^ (p - 1) * 1 / (t + 1) * x ^ (p - 1)

Tactic:
simp [hx_zero, Real.zero_rpow (by linarith : p - 1 ≠ 0)]

Premises used: Real.zero_rpow
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p t x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 ≤ t
hx : 0 ≤ x
hxt : 0 ≤ x * t
hx_zero : x = 0
case case₁ case₂ :
  ∀ (hp : 0 < p ∧ p < 1) (ht : 0 ≤ t) (hx : 0 ≤ x) (hxt : 0 ≤ x * t) (hx_zero : x = 0),
    (x * t) ^ (p - 1) * x / (x * t + x) = t ^ (p - 1) * 1 / (t + 1) * x ^ (p - 1)
⊢ (x * t) ^ (p - 1) * x / (x * t + x) = t ^ (p - 1) * 1 / (t + 1) * x ^ (p - 1)

Tactic:
case pos =>
    rw [mem_Ioo] at hp
    simp [hx_zero, Real.zero_rpow (by linarith : p - 1 ≠ 0)]

Premises used: Set.mem_Ioo, Real.zero_rpow
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p t x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 ≤ t
hx : 0 ≤ x
simp : p.rpowIntegrand₀₁ t 1 * (x ^ (p - 1) * x) = p.rpowIntegrand₀₁ t 1 * x ^ p
⊢ p.rpowIntegrand₀₁ (x * t) x * x = p.rpowIntegrand₀₁ t 1 * x ^ p

Tactic:
simp only [rpowIntegrand₀₁_apply_mul hp ht hx, mul_assoc]

Premises used: mul_assoc, Real.rpowIntegrand₀₁_apply_mul
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p t x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 ≤ t
hx : 0 ≤ x
e_a : x ^ (p - 1) * x = x ^ p
⊢ p.rpowIntegrand₀₁ t 1 * (x ^ (p - 1) * x) = p.rpowIntegrand₀₁ t 1 * x ^ p

Tactic:
congr