awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ p - 1 + 1 ≠ 0

Tactic:
aesop
-- 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
⊢ x ^ (p - 1) * x = x ^ p

Tactic:
simpa using Eq.symm <| Real.rpow_add' hx (by aesop : (p - 1) + 1 ≠ 0)

Premises used: Real.rpow_add', Eq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
hx : 0 ≤ x
⊢ EqOn (β := ℝ) (fun (t : ℝ) ↦ p.rpowIntegrand₀₁ (x * t) x * x) (fun (t : ℝ) ↦ p.rpowIntegrand₀₁ t 1 * x ^ p) (Ici 0)

Tactic:
fun _ ht => rpowIntegrand₀₁_apply_mul' hp ht hx

Premises used: Set.EqOn, Real.rpowIntegrand₀₁_apply_mul'
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
hx : 0 ≤ x
⊢ ContinuousOn (Y := ℝ) (fun (x_1 : ℝ) ↦ p.rpowIntegrand₀₁ x_1 x) (Ioi 0)

Tactic:
ContinuousOn.congr ?_ <| rpowIntegrand₀₁_eqOn_pow_div hp hx

Premises used: ContinuousOn.congr, Real.rpowIntegrand₀₁_eqOn_pow_div
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
hx : 0 ≤ x
refine : ContinuousOn (Y := ℝ) (fun (t : ℝ) ↦ t ^ (p - 1) * x / (t + x)) (Ioi 0)
⊢ ContinuousOn (Y := ℝ) (fun (x_1 : ℝ) ↦ p.rpowIntegrand₀₁ x_1 x) (Ioi 0)

Tactic:
refine ContinuousOn.congr ?_ <| rpowIntegrand₀₁_eqOn_pow_div hp hx

Premises used: ContinuousOn.congr, Real.rpowIntegrand₀₁_eqOn_pow_div
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
hx : 0 ≤ x
⊢ ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ x) (Ioi 0)

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
hx : 0 ≤ x
⊢ ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ x ^ (p - 1)) (Ioi 0)

Tactic:
have h₀ : ContinuousOn (· ^ (p - 1) : ℝ → ℝ) (Ioi 0) := .rpow_const (by fun_prop) <|
    fun t ht => .inl ht.ne'
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
hx : 0 ≤ x
h₀ : ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ x ^ (p - 1)) (Ioi 0)
⊢ ∀ (x_1 : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) x_1 → x_1 + x ≠ 0

Tactic:
grind -abstractProof
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
hx : 0 ≤ x
h₀ : ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ x ^ (p - 1)) (Ioi 0)
funProp : ∀ (x_1 : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) x_1 → x_1 + x ≠ 0
⊢ ContinuousOn (Y := ℝ) (fun (t : ℝ) ↦ t ^ (p - 1) * x / (t + x)) (Ioi 0)

Tactic:
fun_prop (disch := grind -abstractProof)
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
hx : 0 ≤ x
⊢ AEStronglyMeasurable (β := ℝ) (m₀ := MeasureSpace.toMeasurableSpace) (fun (x_1 : ℝ) ↦ p.rpowIntegrand₀₁ x_1 x)
    (Measure.restrict volume (Ioi 0))

Tactic:
(continuousOn_rpowIntegrand₀₁ hp hx).aestronglyMeasurable measurableSet_Ioi

Premises used: ContinuousOn.aestronglyMeasurable, measurableSet_Ioi, Real.continuousOn_rpowIntegrand₀₁
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p t : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 ≤ t
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ici 0) x
y : ℝ
hy : Membership.mem (γ := Set ℝ) (Ici 0) y
hxy : x ≤ y
by_cases : ∀ (h : x = 0), p.rpowIntegrand₀₁ t x ≤ p.rpowIntegrand₀₁ t y
by_cases₁ : ∀ (h : ¬x = 0), p.rpowIntegrand₀₁ t x ≤ p.rpowIntegrand₀₁ t y
⊢ p.rpowIntegrand₀₁ t x ≤ p.rpowIntegrand₀₁ t y

Tactic:
by_cases h : x = 0
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p t : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 ≤ t
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ici 0) x
y : ℝ
hy : Membership.mem (γ := Set ℝ) (Ici 0) y
hxy : x ≤ y
h : x = 0
⊢ p.rpowIntegrand₀₁ t x ≤ p.rpowIntegrand₀₁ t y

Tactic:
simpa [h, rpowIntegrand₀₁] using rpowIntegrand₀₁_nonneg hp.1 ht hy

Premises used: Real.rpowIntegrand₀₁_nonneg, Real.rpowIntegrand₀₁, And.left
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p t : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 ≤ t
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ici 0) x
y : ℝ
hy : Membership.mem (γ := Set ℝ) (Ici 0) y
hxy : x ≤ y
h : x = 0
⊢ p.rpowIntegrand₀₁ t x ≤ p.rpowIntegrand₀₁ t y

Tactic:
case pos => simpa [h, rpowIntegrand₀₁] using rpowIntegrand₀₁_nonneg hp.1 ht hy

Premises used: Real.rpowIntegrand₀₁_nonneg, Real.rpowIntegrand₀₁, And.left
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p t : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 ≤ t
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ici 0) x
y : ℝ
hy : Membership.mem (γ := Set ℝ) (Ici 0) y
hxy : x ≤ y
h : ¬x = 0
⊢ 0 ≤ x

Tactic:
simp only [rpowIntegrand₀₁, mem_Ici] at hx h ⊢

Premises used: Real.rpowIntegrand₀₁, Set.mem_Ici
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p t : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 ≤ t
x y : ℝ
hy : Membership.mem (γ := Set ℝ) (Ici 0) y
hxy : x ≤ y
h : ¬x = 0
hx : 0 ≤ x
ha : 0 ≤ t ^ p
hbc : 0 < t + x
⊢ t ^ p * (t⁻¹ - (t + x)⁻¹) ≤ t ^ p * (t⁻¹ - (t + y)⁻¹)

Tactic:
gcongr
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p t : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 ≤ t
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ici 0) x
y : ℝ
hy : Membership.mem (γ := Set ℝ) (Ici 0) y
hxy : x ≤ y
h : ¬x = 0
⊢ 0 ≤ x

Tactic:
case neg =>
    simp only [rpowIntegrand₀₁, mem_Ici] at hx h ⊢
    gcongr

Premises used: Real.rpowIntegrand₀₁, Set.mem_Ici
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
s : Set ℝ
hs : s ⊆ Ici 0
g : ℝ × ℝ → ℝ := fun (q : ℝ × ℝ) ↦ q.1 ^ (p - 1) * q.2 / (q.1 + q.2)
⊢ ContinuousOn (Function.uncurry p.rpowIntegrand₀₁) (SProd.sprod (α := Set ℝ) (Ioi 0) s)

Tactic:
ContinuousOn.congr (f := g) ?_ fun q => ?_

Premises used: ContinuousOn.congr
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
s : Set ℝ
hs : s ⊆ Ici 0
g : ℝ × ℝ → ℝ := fun (q : ℝ × ℝ) ↦ q.1 ^ (p - 1) * q.2 / (q.1 + q.2)
refine_1 : ContinuousOn g (SProd.sprod (α := Set ℝ) (Ioi 0) s)
refine_2 : ∀ q ∈ SProd.sprod (α := Set ℝ) (Ioi 0) s, Function.uncurry p.rpowIntegrand₀₁ q = g q
⊢ ContinuousOn (Function.uncurry p.rpowIntegrand₀₁) (SProd.sprod (α := Set ℝ) (Ioi 0) s)

Tactic:
refine ContinuousOn.congr (f := g) ?_ fun q => ?_

Premises used: ContinuousOn.congr
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
s : Set ℝ
hs : s ⊆ Ici 0
g : ℝ × ℝ → ℝ := fun (q : ℝ × ℝ) ↦ q.1 ^ (p - 1) * q.2 / (q.1 + q.2)
refine_1 :
  ContinuousOn (Y := ℝ) (fun (q : ℝ × ℝ) ↦ q.1 ^ (p - 1) * q.2 / (q.1 + q.2)) (SProd.sprod (α := Set ℝ) (Ioi 0) s)
⊢ ContinuousOn g (SProd.sprod (α := Set ℝ) (Ioi 0) s)

Tactic:
simp only [g]
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
s : Set ℝ
hs : s ⊆ Ici 0
g : ℝ × ℝ → ℝ := fun (q : ℝ × ℝ) ↦ q.1 ^ (p - 1) * q.2 / (q.1 + q.2)
⊢ ContinuousOn (Y := ℝ) (fun (q : ℝ × ℝ) ↦ q.1 ^ (p - 1) * q.2 / (q.1 + q.2)) (SProd.sprod (α := Set ℝ) (Ioi 0) s)

Tactic:
ContinuousOn.mul ?_ ?_

Premises used: DivInvMonoid.div', ContinuousOn.mul
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
s : Set ℝ
hs : s ⊆ Ici 0
g : ℝ × ℝ → ℝ := fun (q : ℝ × ℝ) ↦ q.1 ^ (p - 1) * q.2 / (q.1 + q.2)
refine_1 : ContinuousOn (Y := ℝ) (fun (q : ℝ × ℝ) ↦ q.1 ^ (p - 1) * q.2) (SProd.sprod (α := Set ℝ) (Ioi 0) s)
refine_1₁ : ContinuousOn (Y := ℝ) (fun (q : ℝ × ℝ) ↦ (q.1 + q.2)⁻¹) (SProd.sprod (α := Set ℝ) (Ioi 0) s)
⊢ ContinuousOn (Y := ℝ) (fun (q : ℝ × ℝ) ↦ q.1 ^ (p - 1) * q.2 / (q.1 + q.2)) (SProd.sprod (α := Set ℝ) (Ioi 0) s)

Tactic:
refine ContinuousOn.mul ?_ ?_

Premises used: ContinuousOn.mul
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
s : Set ℝ
hs : s ⊆ Ici 0
g : ℝ × ℝ → ℝ := fun (q : ℝ × ℝ) ↦ q.1 ^ (p - 1) * q.2 / (q.1 + q.2)
⊢ ContinuousOn Prod.snd (SProd.sprod (α := Set ℝ) (Ioi 0) s)

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
s : Set ℝ
hs : s ⊆ Ici 0
g : ℝ × ℝ → ℝ := fun (q : ℝ × ℝ) ↦ q.1 ^ (p - 1) * q.2 / (q.1 + q.2)
refine_1 : ContinuousOn (Y := ℝ) (fun (q : ℝ × ℝ) ↦ q.1 ^ (p - 1)) (SProd.sprod (α := Set ℝ) (Ioi 0) s)
⊢ ContinuousOn (Y := ℝ) (fun (q : ℝ × ℝ) ↦ q.1 ^ (p - 1) * q.2) (SProd.sprod (α := Set ℝ) (Ioi 0) s)

Tactic:
refine ContinuousOn.mul ?_ (by fun_prop)

Premises used: ContinuousOn.mul
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
s : Set ℝ
hs : s ⊆ Ici 0
g : ℝ × ℝ → ℝ := fun (q : ℝ × ℝ) ↦ q.1 ^ (p - 1) * q.2 / (q.1 + q.2)
⊢ ContinuousOn Prod.fst (SProd.sprod (α := Set ℝ) (Ioi 0) s)

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
s : Set ℝ
hs : s ⊆ Ici 0
g : ℝ × ℝ → ℝ := fun (q : ℝ × ℝ) ↦ q.1 ^ (p - 1) * q.2 / (q.1 + q.2)
⊢ ∀ x ∈ SProd.sprod (α := Set ℝ) (Ioi 0) s, x.1 ≠ 0 ∨ 0 ≤ p - 1

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
s : Set ℝ
hs : s ⊆ Ici 0
g : ℝ × ℝ → ℝ := fun (q : ℝ × ℝ) ↦ q.1 ^ (p - 1) * q.2 / (q.1 + q.2)
⊢ ContinuousOn (Y := ℝ) (fun (q : ℝ × ℝ) ↦ q.1 ^ (p - 1)) (SProd.sprod (α := Set ℝ) (Ioi 0) s)

Tactic:
exact ContinuousOn.rpow_const (by fun_prop) (by grind)

Premises used: ContinuousOn.rpow_const
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
s : Set ℝ
hs : s ⊆ Ici 0
g : ℝ × ℝ → ℝ := fun (q : ℝ × ℝ) ↦ q.1 ^ (p - 1) * q.2 / (q.1 + q.2)
⊢ ContinuousOn (Y := ℝ) (fun (q : ℝ × ℝ) ↦ q.1 + q.2) (SProd.sprod (α := Set ℝ) (Ioi 0) s)

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
s : Set ℝ
hs : s ⊆ Ici 0
g : ℝ × ℝ → ℝ := fun (q : ℝ × ℝ) ↦ q.1 ^ (p - 1) * q.2 / (q.1 + q.2)
⊢ ∀ x ∈ SProd.sprod (α := Set ℝ) (Ioi 0) s, x.1 + x.2 ≠ 0

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
s : Set ℝ
hs : s ⊆ Ici 0
g : ℝ × ℝ → ℝ := fun (q : ℝ × ℝ) ↦ q.1 ^ (p - 1) * q.2 / (q.1 + q.2)
⊢ ContinuousOn (Y := ℝ) (fun (q : ℝ × ℝ) ↦ (q.1 + q.2)⁻¹) (SProd.sprod (α := Set ℝ) (Ioi 0) s)

Tactic:
exact ContinuousOn.inv₀ (by fun_prop) (by grind)

Premises used: ContinuousOn.inv₀
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
s : Set ℝ
hs : s ⊆ Ici 0
g : ℝ × ℝ → ℝ := fun (q : ℝ × ℝ) ↦ q.1 ^ (p - 1) * q.2 / (q.1 + q.2)
q : ℝ × ℝ
hq : q ∈ SProd.sprod (α := Set ℝ) (Ioi 0) s
⊢ Function.uncurry p.rpowIntegrand₀₁ q = g q

Tactic:
simp [Function.uncurry, g, rpowIntegrand₀₁_eq_pow_div hp (le_of_lt hq.1) (hs hq.2)]

Premises used: le_of_lt, Real.rpowIntegrand₀₁_eq_pow_div, And.right, And.left, Function.uncurry
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p t : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 < t
⊢ ContinuousOn (p.rpowIntegrand₀₁ t) (Ici 0)

Tactic:
(continuousOn_rpowIntegrand₀₁_uncurry hp _ fun _ a => a).uncurry_left _ ht

Premises used: Real.continuousOn_rpowIntegrand₀₁_uncurry, ContinuousOn.uncurry_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
rw rw₁ : t ^ (p - 1) * x / (t + x) = t ^ (p - 1) * x / (t + x)
⊢ p.rpowIntegrand₀₁ t x = t ^ (p - 1) * x / (t + x)

Tactic:
rw [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
hdb : t ≤ t + x
⊢ t ^ (p - 1) * x / (t + x) ≤ t ^ (p - 1) * x / t

Tactic:
gcongr
-- 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
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 : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 < t
hx : 0 ≤ x
⊢ t ^ (p - 1) * x / t = t ^ (p - 1) / t * x

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
e_a : t ^ (p - 1) / t = t ^ (p - 2)
⊢ t ^ (p - 1) / t * x = t ^ (p - 2) * 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
⊢ t ≠ 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
e_a : t ^ (p - 1 - 1) = t ^ (p - 2)
⊢ t ^ (p - 1) / t = t ^ (p - 2)

Tactic:
rw [← Real.rpow_sub_one (by positivity)]

Premises used: Real.rpow_sub_one
-- 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 : p - 1 - 1 = p - 2
⊢ t ^ (p - 1 - 1) = t ^ (p - 2)

Tactic:
congr 1
-- 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
⊢ p - 1 - 1 = p - 2

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
by_cases : ∀ (hx_zero : x = 0), p.rpowIntegrand₀₁ t x ≤ t ^ (p - 1)
by_cases₁ : ∀ (hx_zero : ¬x = 0), p.rpowIntegrand₀₁ t x ≤ t ^ (p - 1)
⊢ p.rpowIntegrand₀₁ t x ≤ t ^ (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
hx_zero : x = 0
simp : 0 ≤ t ^ (p - 1)
⊢ p.rpowIntegrand₀₁ t x ≤ t ^ (p - 1)

Tactic:
simp only [rpowIntegrand₀₁, hx_zero, add_zero, sub_self, mul_zero]

Premises used: sub_self, MulZeroClass.mul_zero, Real.rpowIntegrand₀₁, add_zero
-- 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
hx_zero : x = 0
⊢ 0 ≤ t ^ (p - 1)

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
hx_zero : x = 0
⊢ p.rpowIntegrand₀₁ t x ≤ t ^ (p - 1)

Tactic:
case pos =>
    simp only [rpowIntegrand₀₁, hx_zero, add_zero, sub_self, mul_zero]
    positivity

Premises used: sub_self, MulZeroClass.mul_zero, Real.rpowIntegrand₀₁, add_zero
-- 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
hx_zero : ¬x = 0
rw rw₁ : t ^ (p - 1) * x / (t + x) = t ^ (p - 1) * x / (t + x)
⊢ p.rpowIntegrand₀₁ t x = t ^ (p - 1) * x / (t + x)

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

Premises used: 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
hx_zero : ¬x = 0
hdb : x ≤ t + x
⊢ t ^ (p - 1) * x / (t + x) ≤ t ^ (p - 1) * x / x

Tactic:
gcongr
-- 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
hx_zero : ¬x = 0
linarith : t + x < x → 0 - t + (t + x - x) = 0
⊢ x ≤ t + x

Tactic:
linarith
-- 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
hx_zero : ¬x = 0
⊢ t ^ (p - 1) * x / x = t ^ (p - 1) * (x / x)

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
hx_zero : ¬x = 0
e_a : x / x = 1
⊢ t ^ (p - 1) * (x / x) = t ^ (p - 1) * 1

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
hx_zero : ¬x = 0
⊢ x / x = 1

Tactic:
(div_eq_one_iff_eq hx_zero).mpr rfl

Premises used: Iff.mpr, div_eq_one_iff_eq, 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
hx_zero : ¬x = 0
⊢ x / x = 1

Tactic:
exact (div_eq_one_iff_eq hx_zero).mpr rfl

Premises used: Iff.mpr, div_eq_one_iff_eq, 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
hx_zero : ¬x = 0
⊢ t ^ (p - 1) * 1 = t ^ (p - 1)

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
hx_zero : ¬x = 0
_ : p.rpowIntegrand₀₁ t x = t ^ (p - 1) * x / (t + x)
_₁ : t ^ (p - 1) * x / (t + x) ≤ t ^ (p - 1) * x / x
_₂ : t ^ (p - 1) * x / x = t ^ (p - 1) * (x / x)
_₃ : t ^ (p - 1) * (x / x) = t ^ (p - 1) * 1
_₄ : t ^ (p - 1) * 1 = t ^ (p - 1)
⊢ p.rpowIntegrand₀₁ t x ≤ t ^ (p - 1)

Tactic:
calc
    _ = t ^ (p - 1) * x / (t + x) := by rw [rpowIntegrand₀₁_eq_pow_div hp ht hx]
    _ ≤ t ^ (p - 1) * x / x := by gcongr; linarith
    _ = t ^ (p - 1) * (x / x) := by ring
    _ = t ^ (p - 1) * 1 := by congr; exact (div_eq_one_iff_eq hx_zero).mpr rfl
    _ = _ := by simp

Premises used: HSub.hSub, HDiv.hDiv, 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
hx_zero : ¬x = 0
case : p.rpowIntegrand₀₁ t x = t ^ (p - 1) * x / (t + x)
case₁ : t ^ (p - 1) * x / (t + x) ≤ t ^ (p - 1) * x / x
case₂ : t ^ (p - 1) * x / x = t ^ (p - 1) * (x / x)
case₃ : t ^ (p - 1) * (x / x) = t ^ (p - 1) * 1
case₄ : t ^ (p - 1) * 1 = t ^ (p - 1)
⊢ p.rpowIntegrand₀₁ t x ≤ t ^ (p - 1)

Tactic:
case neg =>
    calc
    _ = t ^ (p - 1) * x / (t + x) := by rw [rpowIntegrand₀₁_eq_pow_div hp ht hx]
    _ ≤ t ^ (p - 1) * x / x := by gcongr; linarith
    _ = t ^ (p - 1) * (x / x) := by ring
    _ = t ^ (p - 1) * 1 := by congr; exact (div_eq_one_iff_eq hx_zero).mpr rfl
    _ = _ := by simp

Premises used: HSub.hSub, HDiv.hDiv, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p t : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 1 ≤ t
⊢ p - 2 = p - 1 - 1

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

Tactic:
have : p - 2 = p - 1 - 1 := by ring
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p t : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 1 ≤ t
this : p - 2 = p - 1 - 1
linarith : t ≤ 0 → -1 + (1 - t) + (t - 0) = 0
⊢ 0 < t

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p t : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 1 ≤ t
this : p - 2 = p - 1 - 1
rw : 1 / 2 * (t ^ (p - 1) / t) = t ^ (p - 1) * (1 / 2 * 1 / t)
⊢ 1 / 2 * t ^ (p - 2) = t ^ (p - 1) * (1 / 2 * 1 / t)

Tactic:
rw [this, Real.rpow_sub (by linarith), Real.rpow_one]

Premises used: Real.rpow_one, Real.rpow_sub
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p t : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 1 ≤ t
this : p - 2 = p - 1 - 1
⊢ 1 / 2 * (t ^ (p - 1) / t) = t ^ (p - 1) * (1 / 2 * 1 / t)

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p t : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 1 ≤ t
hbc : 1 / 2 * 1 / t ≤ 1 / (t + 1)
⊢ t ^ (p - 1) * (1 / 2 * 1 / t) ≤ t ^ (p - 1) * (1 / (t + 1))

Tactic:
gcongr t ^ (p - 1) * ?_

Premises used: HSub.hSub, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p t : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 1 ≤ t
⊢ 0 < 2 * t

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

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

Tactic:
rw [mul_div_assoc, one_div_mul_one_div,
              one_div_le_one_div (by positivity) (by positivity)]

Premises used: mul_div_assoc, one_div_le_one_div, one_div_mul_one_div
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p t : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 1 ≤ t
linarith : 2 * t < t + 1 → 1 - t + (2 * t - (t + 1)) = 0
⊢ t + 1 ≤ 2 * t

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p t : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 1 ≤ t
linarith : t < 0 → -1 + (1 - t) + (t - 0) = 0
⊢ 0 ≤ t

Tactic:
linarith