awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p t : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 < t
a : A
ha : 0 ≤ a
b : A
hb : 0 ≤ b
hab : a ≤ b
⊢ 0 ≤ t⁻¹ • b

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p t : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 < t
a : A
ha : 0 ≤ a
b : A
hb : 0 ≤ b
hab : a ≤ b
rw rw₁ :
  t ^ (p - 1) • cfcₙ (p := IsSelfAdjoint) (p.rpowIntegrand₀₁ 1) (t⁻¹ • b) =
    t ^ (p - 1) • cfcₙ (p := IsSelfAdjoint) (p.rpowIntegrand₀₁ 1) (t⁻¹ • b)
⊢ t ^ (p - 1) • cfcₙ (p := IsSelfAdjoint) (p.rpowIntegrand₀₁ 1) (t⁻¹ • b) =
    cfcₙ (p := IsSelfAdjoint) (p.rpowIntegrand₀₁ t) b

Tactic:
rw [cfcₙ_rpowIntegrand₀₁_eq_cfcₙ_rpowIntegrand₀₁_one hp ht b hb]

Premises used: CFC.cfcₙ_rpowIntegrand₀₁_eq_cfcₙ_rpowIntegrand₀₁_one
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p t : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 < t
a : A
ha : 0 ≤ a
b : A
hb : 0 ≤ b
hab : a ≤ b
_ :
  cfcₙ (p := IsSelfAdjoint) (p.rpowIntegrand₀₁ t) a =
    t ^ (p - 1) • cfcₙ (p := IsSelfAdjoint) (p.rpowIntegrand₀₁ 1) (t⁻¹ • a)
_₁ :
  t ^ (p - 1) • cfcₙ (p := IsSelfAdjoint) (p.rpowIntegrand₀₁ 1) (t⁻¹ • a) ≤
    t ^ (p - 1) • cfcₙ (p := IsSelfAdjoint) (p.rpowIntegrand₀₁ 1) (t⁻¹ • b)
_₂ :
  t ^ (p - 1) • cfcₙ (p := IsSelfAdjoint) (p.rpowIntegrand₀₁ 1) (t⁻¹ • b) =
    cfcₙ (p := IsSelfAdjoint) (p.rpowIntegrand₀₁ t) b
⊢ cfcₙ (p := IsSelfAdjoint) (p.rpowIntegrand₀₁ t) a ≤ cfcₙ (p := IsSelfAdjoint) (p.rpowIntegrand₀₁ t) b

Tactic:
calc
    _ = t ^ ((p : ℝ) - 1) • cfcₙ (rpowIntegrand₀₁ p 1) (t⁻¹ • a) := by
      rw [cfcₙ_rpowIntegrand₀₁_eq_cfcₙ_rpowIntegrand₀₁_one hp ht a ha]
    _ ≤ t ^ ((p : ℝ) - 1) • cfcₙ (rpowIntegrand₀₁ p 1) (t⁻¹ • b) := by
      gcongr
      unfold rpowIntegrand₀₁
      simp only [Real.one_rpow, one_mul, inv_one]
      refine CFC.monotoneOn_one_sub_one_add_inv_real
        (?_ : 0 ≤ t⁻¹ • a) (?_ : 0 ≤ t⁻¹ • b) (by gcongr)
      all_goals positivity
    _ = cfcₙ (rpowIntegrand₀₁ p t) b := by
      rw [cfcₙ_rpowIntegrand₀₁_eq_cfcₙ_rpowIntegrand₀₁_one hp ht b hb]

Premises used: cfcₙ, HSub.hSub, Real.rpowIntegrand₀₁, Inv.inv, HSMul.hSMul, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p t : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 < t
hf : ConcaveOn ℝ (Unitization.inr '' Ici 0) (cfc (p := IsSelfAdjoint) (p.rpowIntegrand₀₁ t))
⊢ ConcaveOn ℝ (Ici 0) (cfcₙ (p := IsSelfAdjoint) (p.rpowIntegrand₀₁ t))

Tactic:
apply concaveOn_cfcₙ_of_concaveOn_cfc

Premises used: CStarAlgebra.concaveOn_cfcₙ_of_concaveOn_cfc
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p t : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 < t
⊢ ConcaveOn ℝ (Unitization.inr '' Ici 0) (cfc (p := IsSelfAdjoint) (p.rpowIntegrand₀₁ t))

Tactic:
ConcaveOn.subset (concaveOn_cfc_rpowIntegrand₀₁ hp ht) inr_map_Ici_zero ?_

Premises used: ConcaveOn.subset, CStarAlgebra.inr_map_Ici_zero, CFC.concaveOn_cfc_rpowIntegrand₀₁
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p t : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 < t
hf : Convex.{0, u_1} ℝ (E := Unitization ℂ A) (Unitization.inr '' Ici 0)
⊢ ConcaveOn ℝ (Unitization.inr '' Ici 0) (cfc (p := IsSelfAdjoint) (p.rpowIntegrand₀₁ t))

Tactic:
refine ConcaveOn.subset (concaveOn_cfc_rpowIntegrand₀₁ hp ht) inr_map_Ici_zero ?_

Premises used: ConcaveOn.subset, CFC.concaveOn_cfc_rpowIntegrand₀₁
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p t : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 < t
⊢ Convex.{0, u_1} ℝ (E := Unitization ℂ A) (Unitization.inr '' Ici 0)

Tactic:
Convex.linear_image (convex_Ici _) (Unitization.inrHom ℝ ℂ A)

Premises used: Real, Unitization.inr, Convex.linear_image, Unitization.inrHom, convex_Ici, Complex
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p t : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 < t
⊢ Convex.{0, u_1} ℝ (E := Unitization ℂ A) (Unitization.inr '' Ici 0)

Tactic:
exact Convex.linear_image (convex_Ici _) (Unitization.inrHom ℝ ℂ A)

Premises used: Real, Convex.linear_image, Unitization.inrHom, convex_Ici, Complex
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0
y : ℝ
⊢ x.rpow y = x ^ y

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0
y : ℝ
⊢ (↑(x ^ y) : ℝ) = (↑x : ℝ) ^ y

Tactic:
rfl

Premises used: NNReal.toReal, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0
⊢ HPow.hPow (β := ℝ) x 0 = 1

Tactic:
NNReal.eq <| Real.rpow_zero _

Premises used: Real.rpow_zero, NNReal.eq
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0
rw : LT.lt (α := ℝ≥0) 0 1
⊢ 0 < HPow.hPow (β := ℝ) x 0

Tactic:
rw [rpow_zero]

Premises used: NNReal.rpow_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0
⊢ LT.lt (α := ℝ≥0) 0 1

Tactic:
one_pos

Premises used: one_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0
⊢ LT.lt (α := ℝ≥0) 0 1

Tactic:
exact one_pos

Premises used: one_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0
y : ℝ
rw : (↑x : ℝ) ^ y = (↑0 : ℝ) ↔ (↑x : ℝ) = 0 ∧ y ≠ 0
⊢ x ^ y = 0 ↔ x = 0 ∧ y ≠ 0

Tactic:
rw [← NNReal.coe_inj, coe_rpow, ← NNReal.coe_eq_zero]

Premises used: NNReal.coe_rpow, NNReal.coe_eq_zero, NNReal.coe_inj
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0
y : ℝ
⊢ (↑x : ℝ) ^ y = (↑0 : ℝ) ↔ (↑x : ℝ) = 0 ∧ y ≠ 0

Tactic:
Real.rpow_eq_zero_iff_of_nonneg x.2

Premises used: Real.rpow_eq_zero_iff_of_nonneg, NNReal.toReal, Subtype.property
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0
y : ℝ
⊢ (↑x : ℝ) ^ y = (↑0 : ℝ) ↔ (↑x : ℝ) = 0 ∧ y ≠ 0

Tactic:
exact Real.rpow_eq_zero_iff_of_nonneg x.2

Premises used: Real.rpow_eq_zero_iff_of_nonneg, Subtype.property
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0
y : ℝ
hy : y ≠ 0
⊢ x ^ y = 0 ↔ x = 0

Tactic:
simp [hy]
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ
h : x ≠ 0
⊢ HPow.hPow (α := ℝ≥0) 0 x = 0

Tactic:
NNReal.eq <| Real.zero_rpow h

Premises used: NNReal.eq, Real.zero_rpow
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y : ℝ
pos : ∀ (h : y = 0), HPow.hPow (α := ℝ≥0) 0 y = 1
neg : ∀ (h : ¬y = 0), HPow.hPow (α := ℝ≥0) 0 y = 0
⊢ HPow.hPow (α := ℝ≥0) 0 y = if y = 0 then 1 else 0

Tactic:
split_ifs with h
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y : ℝ
h : y = 0
⊢ HPow.hPow (α := ℝ≥0) 0 y = 1

Tactic:
simp [h]
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y : ℝ
h : ¬y = 0
⊢ HPow.hPow (α := ℝ≥0) 0 y = 0

Tactic:
simp [h]
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0
⊢ HPow.hPow (β := ℝ) x 1 = x

Tactic:
NNReal.eq <| Real.rpow_one _

Premises used: NNReal.eq, Real.rpow_one
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0
y : ℝ
⊢ x ^ (-y) = (x ^ y)⁻¹

Tactic:
NNReal.eq <| Real.rpow_neg x.2 _

Premises used: NNReal.eq, Real.rpow_neg, Subtype.property
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0
n : ℕ
⊢ (↑(HPow.hPow (β := ℝ) x (↑n : ℝ)) : ℝ) = (↑(x ^ n) : ℝ)

Tactic:
simpa only [coe_rpow, coe_pow] using Real.rpow_natCast x n

Premises used: NNReal.coe_rpow, NNReal.coe_pow, NNReal.toReal, Real.rpow_natCast
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0
n : ℤ
ofNat : ∀ (a : ℕ), HPow.hPow (β := ℝ) x (↑(Int.ofNat a) : ℝ) = x ^ Int.ofNat a
negSucc : ∀ (a : ℕ), HPow.hPow (β := ℝ) x (↑(Int.negSucc a) : ℝ) = x ^ Int.negSucc a
⊢ HPow.hPow (β := ℝ) x (↑n : ℝ) = x ^ n

Tactic:
cases n
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0
a : ℕ
⊢ HPow.hPow (β := ℝ) x (↑(Int.ofNat a) : ℝ) = x ^ Int.ofNat a

Tactic:
simp only [Int.ofNat_eq_natCast, Int.cast_natCast, rpow_natCast, zpow_natCast,
    Int.cast_negSucc, rpow_neg, zpow_negSucc]

Premises used: zpow_natCast, Int.cast_natCast, NNReal.rpow_natCast, zpow_negSucc, Int.ofNat_eq_natCast, Int.cast_negSucc, NNReal.rpow_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0
a : ℕ
⊢ HPow.hPow (β := ℝ) x (↑(Int.negSucc a) : ℝ) = x ^ Int.negSucc a

Tactic:
simp only [Int.ofNat_eq_natCast, Int.cast_natCast, rpow_natCast, zpow_natCast,
    Int.cast_negSucc, rpow_neg, zpow_negSucc]

Premises used: zpow_natCast, Int.cast_natCast, NNReal.rpow_natCast, zpow_negSucc, Int.ofNat_eq_natCast, Int.cast_negSucc, NNReal.rpow_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ
⊢ HPow.hPow (α := ℝ≥0) 1 x = 1

Tactic:
NNReal.eq <| Real.one_rpow _

Premises used: NNReal.eq, Real.one_rpow
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0
hx : x ≠ 0
y z : ℝ
⊢ x ^ (y + z) = x ^ y * x ^ z

Tactic:
NNReal.eq <| Real.rpow_add ((NNReal.coe_pos.trans pos_iff_ne_zero).mpr hx) _ _

Premises used: Iff.mpr, NNReal.eq, Iff.trans, Real.rpow_add, NNReal.coe_pos, pos_iff_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y z : ℝ
h : y + z ≠ 0
x : ℝ≥0
⊢ x ^ (y + z) = x ^ y * x ^ z

Tactic:
NNReal.eq <| Real.rpow_add' x.2 h

Premises used: NNReal.eq, Real.rpow_add', Subtype.property
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0
hx : x ≠ 0
y : ℝ
n : ℤ
a : (↑(x ^ (y + (↑n : ℝ))) : ℝ) = (↑(x ^ y * x ^ n) : ℝ)
⊢ x ^ (y + (↑n : ℝ)) = x ^ y * x ^ n

Tactic:
ext
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0
hx : x ≠ 0
y : ℝ
n : ℤ
⊢ (↑(x ^ (y + (↑n : ℝ))) : ℝ) = (↑(x ^ y * x ^ n) : ℝ)

Tactic:
Real.rpow_add_intCast (mod_cast hx) _ _

Premises used: Real.rpow_add_intCast, NNReal.toReal
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0
hx : x ≠ 0
y : ℝ
n : ℤ
⊢ (↑(x ^ (y + (↑n : ℝ))) : ℝ) = (↑(x ^ y * x ^ n) : ℝ)

Tactic:
exact Real.rpow_add_intCast (mod_cast hx) _ _

Premises used: Real.rpow_add_intCast
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0
hx : x ≠ 0
y : ℝ
n : ℕ
a : (↑(x ^ (y + (↑n : ℝ))) : ℝ) = (↑(x ^ y * x ^ n) : ℝ)
⊢ x ^ (y + (↑n : ℝ)) = x ^ y * x ^ n

Tactic:
ext
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0
hx : x ≠ 0
y : ℝ
n : ℕ
⊢ (↑(x ^ (y + (↑n : ℝ))) : ℝ) = (↑(x ^ y * x ^ n) : ℝ)

Tactic:
Real.rpow_add_natCast (mod_cast hx) _ _

Premises used: Real.rpow_add_natCast, NNReal.toReal
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0
hx : x ≠ 0
y : ℝ
n : ℕ
⊢ (↑(x ^ (y + (↑n : ℝ))) : ℝ) = (↑(x ^ y * x ^ n) : ℝ)

Tactic:
exact Real.rpow_add_natCast (mod_cast hx) _ _

Premises used: Real.rpow_add_natCast
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0
hx : x ≠ 0
y : ℝ
n : ℕ
a : (↑(x ^ (y - (↑n : ℝ))) : ℝ) = (↑(x ^ y / x ^ n) : ℝ)
⊢ x ^ (y - (↑n : ℝ)) = x ^ y / x ^ n

Tactic:
ext
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0
hx : x ≠ 0
y : ℝ
n : ℕ
⊢ (↑(x ^ (y - (↑n : ℝ))) : ℝ) = (↑(x ^ y / x ^ n) : ℝ)

Tactic:
Real.rpow_sub_intCast (mod_cast hx) _ _

Premises used: zpowRec, Real.rpow_sub_intCast, NNReal.toReal
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0
hx : x ≠ 0
y : ℝ
n : ℕ
⊢ (↑(x ^ (y - (↑n : ℝ))) : ℝ) = (↑(x ^ y / x ^ n) : ℝ)

Tactic:
exact Real.rpow_sub_intCast (mod_cast hx) _ _

Premises used: Real.rpow_sub_intCast
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0
hx : x ≠ 0
y : ℝ
n : ℕ
⊢ (↑(x ^ (y - (↑n : ℝ))) : ℝ) = (↑(x ^ y / x ^ n) : ℝ)

Tactic:
Real.rpow_sub_natCast (mod_cast hx) _ _

Premises used: Real.rpow_sub_natCast, NNReal.toReal
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0
hx : x ≠ 0
y : ℝ
n : ℕ
⊢ (↑(x ^ (y - (↑n : ℝ))) : ℝ) = (↑(x ^ y / x ^ n) : ℝ)

Tactic:
exact Real.rpow_sub_natCast (mod_cast hx) _ _

Premises used: Real.rpow_sub_natCast
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y : ℝ
n : ℤ
h : y + (↑n : ℝ) ≠ 0
x : ℝ≥0
a : (↑(x ^ (y + (↑n : ℝ))) : ℝ) = (↑(x ^ y * x ^ n) : ℝ)
⊢ x ^ (y + (↑n : ℝ)) = x ^ y * x ^ n

Tactic:
ext
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y : ℝ
n : ℤ
h : y + (↑n : ℝ) ≠ 0
x : ℝ≥0
⊢ (↑(x ^ (y + (↑n : ℝ))) : ℝ) = (↑(x ^ y * x ^ n) : ℝ)

Tactic:
Real.rpow_add_intCast' (mod_cast x.2) h

Premises used: NNReal.toReal, Real.rpow_add_intCast'
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y : ℝ
n : ℤ
h : y + (↑n : ℝ) ≠ 0
x : ℝ≥0
⊢ (↑(x ^ (y + (↑n : ℝ))) : ℝ) = (↑(x ^ y * x ^ n) : ℝ)

Tactic:
exact Real.rpow_add_intCast' (mod_cast x.2) h

Premises used: Real.rpow_add_intCast'
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y : ℝ
n : ℕ
h : y + (↑n : ℝ) ≠ 0
x : ℝ≥0
a : (↑(x ^ (y + (↑n : ℝ))) : ℝ) = (↑(x ^ y * x ^ n) : ℝ)
⊢ x ^ (y + (↑n : ℝ)) = x ^ y * x ^ n

Tactic:
ext
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y : ℝ
n : ℕ
h : y + (↑n : ℝ) ≠ 0
x : ℝ≥0
⊢ (↑(x ^ (y + (↑n : ℝ))) : ℝ) = (↑(x ^ y * x ^ n) : ℝ)

Tactic:
Real.rpow_add_natCast' (mod_cast x.2) h

Premises used: Real.rpow_add_natCast', congrArg, NNReal.coe_le_coe._simp_1, cast, LE.le, congrFun', Nat.cast_zero, Eq.symm, Subtype.val, NNReal.toReal, Eq.trans, Subtype.property
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y : ℝ
n : ℕ
h : y + (↑n : ℝ) ≠ 0
x : ℝ≥0
⊢ (↑(x ^ (y + (↑n : ℝ))) : ℝ) = (↑(x ^ y * x ^ n) : ℝ)

Tactic:
exact Real.rpow_add_natCast' (mod_cast x.2) h

Premises used: Real.rpow_add_natCast'
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y : ℝ
n : ℤ
h : y - (↑n : ℝ) ≠ 0
x : ℝ≥0
a : (↑(x ^ (y - (↑n : ℝ))) : ℝ) = (↑(x ^ y / x ^ n) : ℝ)
⊢ x ^ (y - (↑n : ℝ)) = x ^ y / x ^ n

Tactic:
ext
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y : ℝ
n : ℤ
h : y - (↑n : ℝ) ≠ 0
x : ℝ≥0
⊢ (↑(x ^ (y - (↑n : ℝ))) : ℝ) = (↑(x ^ y / x ^ n) : ℝ)

Tactic:
Real.rpow_sub_intCast' (mod_cast x.2) h

Premises used: Real.rpow_sub_intCast', NNReal.toReal
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y : ℝ
n : ℤ
h : y - (↑n : ℝ) ≠ 0
x : ℝ≥0
⊢ (↑(x ^ (y - (↑n : ℝ))) : ℝ) = (↑(x ^ y / x ^ n) : ℝ)

Tactic:
exact Real.rpow_sub_intCast' (mod_cast x.2) h

Premises used: Real.rpow_sub_intCast'
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y : ℝ
n : ℕ
h : y - (↑n : ℝ) ≠ 0
x : ℝ≥0
a : (↑(x ^ (y - (↑n : ℝ))) : ℝ) = (↑(x ^ y / x ^ n) : ℝ)
⊢ x ^ (y - (↑n : ℝ)) = x ^ y / x ^ n

Tactic:
ext
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y : ℝ
n : ℕ
h : y - (↑n : ℝ) ≠ 0
x : ℝ≥0
⊢ (↑(x ^ (y - (↑n : ℝ))) : ℝ) = (↑(x ^ y / x ^ n) : ℝ)

Tactic:
Real.rpow_sub_natCast' (mod_cast x.2) h

Premises used: congrArg, NNReal.coe_le_coe._simp_1, cast, LE.le, Real.rpow_sub_natCast', congrFun', Nat.cast_zero, Eq.symm, Subtype.val, NNReal.toReal, Eq.trans, Subtype.property
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y : ℝ
n : ℕ
h : y - (↑n : ℝ) ≠ 0
x : ℝ≥0
⊢ (↑(x ^ (y - (↑n : ℝ))) : ℝ) = (↑(x ^ y / x ^ n) : ℝ)

Tactic:
exact Real.rpow_sub_natCast' (mod_cast x.2) h

Premises used: Real.rpow_sub_natCast'
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0
hx : x ≠ 0
y : ℝ
⊢ x ^ (y + 1) = x ^ y * x

Tactic:
simpa using rpow_add_natCast hx y 1

Premises used: NNReal.rpow_add_natCast, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0
hx : x ≠ 0
y : ℝ
⊢ x ^ (y - 1) = x ^ y / x

Tactic:
simpa using rpow_sub_natCast hx y 1

Premises used: NNReal.rpow_sub_natCast, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y : ℝ
h : y + 1 ≠ 0
x : ℝ≥0
rw : x ^ y * HPow.hPow (β := ℝ) x 1 = x ^ y * x
rw₁ rw₂ : x ^ y * x = x ^ y * x
⊢ x ^ (y + 1) = x ^ y * x

Tactic:
rw [rpow_add' h, rpow_one]

Premises used: NNReal.rpow_add', NNReal.rpow_one
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y : ℝ
h : 1 + y ≠ 0
x : ℝ≥0
rw : HPow.hPow (β := ℝ) x 1 * x ^ y = x * x ^ y
rw₁ rw₂ : x * x ^ y = x * x ^ y
⊢ x ^ (1 + y) = x * x ^ y

Tactic:
rw [rpow_add' h, rpow_one]

Premises used: NNReal.rpow_add', NNReal.rpow_one
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0
y z : ℝ
hy : 0 ≤ y
hz : 0 ≤ z
a : (↑(x ^ (y + z)) : ℝ) = (↑(x ^ y * x ^ z) : ℝ)
⊢ x ^ (y + z) = x ^ y * x ^ z

Tactic:
ext
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0
y z : ℝ
hy : 0 ≤ y
hz : 0 ≤ z
⊢ (↑(x ^ (y + z)) : ℝ) = (↑(x ^ y * x ^ z) : ℝ)

Tactic:
Real.rpow_add_of_nonneg x.2 hy hz

Premises used: Real.rpow_add_of_nonneg, NNReal.toReal, Subtype.property
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0
y z : ℝ
hy : 0 ≤ y
hz : 0 ≤ z
⊢ (↑(x ^ (y + z)) : ℝ) = (↑(x ^ y * x ^ z) : ℝ)

Tactic:
exact Real.rpow_add_of_nonneg x.2 hy hz

Premises used: Real.rpow_add_of_nonneg, Subtype.property
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
w y z : ℝ
x : ℝ≥0
hw : w ≠ 0
h : y + z = w
h₁ : y + z ≠ 0
⊢ x ^ w = x ^ y * x ^ z

Tactic:
rw [← h, rpow_add']

Premises used: NNReal.rpow_add'
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
w y z : ℝ
x : ℝ≥0
hw : w ≠ 0
h : y + z = w
h₁ h₂ h₃ h₄ : w ≠ 0
⊢ y + z ≠ 0

Tactic:
rwa [h]
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0
y z : ℝ
⊢ x ^ (y * z) = (x ^ y) ^ z

Tactic:
NNReal.eq <| Real.rpow_mul x.2 y z

Premises used: NNReal.eq, Real.rpow_mul, Subtype.property
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0
n : ℕ
z : ℝ
rw : HPow.hPow (β := ℝ) x (↑n : ℝ) ^ z = (x ^ n) ^ z
rw₁ rw₂ : (x ^ n) ^ z = (x ^ n) ^ z
⊢ x ^ ((↑n : ℝ) * z) = (x ^ n) ^ z

Tactic:
rw [rpow_mul, rpow_natCast]

Premises used: NNReal.rpow_natCast, NNReal.rpow_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0
y : ℝ
n : ℕ
rw : HPow.hPow (β := ℝ) (x ^ y) (↑n : ℝ) = (x ^ y) ^ n
rw₁ rw₂ : (x ^ y) ^ n = (x ^ y) ^ n
⊢ x ^ (y * (↑n : ℝ)) = (x ^ y) ^ n

Tactic:
rw [rpow_mul, rpow_natCast]

Premises used: NNReal.rpow_natCast, NNReal.rpow_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0
n : ℤ
z : ℝ
rw : HPow.hPow (β := ℝ) x (↑n : ℝ) ^ z = (x ^ n) ^ z
rw₁ rw₂ : (x ^ n) ^ z = (x ^ n) ^ z
⊢ x ^ ((↑n : ℝ) * z) = (x ^ n) ^ z

Tactic:
rw [rpow_mul, rpow_intCast]

Premises used: NNReal.rpow_mul, NNReal.rpow_intCast
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0
y : ℝ
n : ℤ
rw : HPow.hPow (β := ℝ) (x ^ y) (↑n : ℝ) = (x ^ y) ^ n
rw₁ rw₂ : (x ^ y) ^ n = (x ^ y) ^ n
⊢ x ^ (y * (↑n : ℝ)) = (x ^ y) ^ n

Tactic:
rw [rpow_mul, rpow_intCast]

Premises used: NNReal.rpow_mul, NNReal.rpow_intCast
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0
⊢ HPow.hPow (β := ℝ) x (-1) = x⁻¹

Tactic:
simp [rpow_neg]

Premises used: NNReal.rpow_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0
hx : x ≠ 0
y z : ℝ
⊢ x ^ (y - z) = x ^ y / x ^ z

Tactic:
NNReal.eq <| Real.rpow_sub ((NNReal.coe_pos.trans pos_iff_ne_zero).mpr hx) y z

Premises used: Iff.mpr, NNReal.eq, Iff.trans, NNReal.coe_pos, Real.rpow_sub, pos_iff_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y z : ℝ
h : y - z ≠ 0
x : ℝ≥0
⊢ x ^ (y - z) = x ^ y / x ^ z

Tactic:
NNReal.eq <| Real.rpow_sub' x.2 h

Premises used: Real.rpow_sub', NNReal.eq, Subtype.property
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y : ℝ
h : y - 1 ≠ 0
x : ℝ≥0
rw : x ^ y / HPow.hPow (β := ℝ) x 1 = x ^ y / x
rw₁ rw₂ : x ^ y / x = x ^ y / x
⊢ x ^ (y - 1) = x ^ y / x

Tactic:
rw [rpow_sub' h, rpow_one]

Premises used: NNReal.rpow_sub', NNReal.rpow_one
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y : ℝ
h : 1 - y ≠ 0
x : ℝ≥0
rw : HPow.hPow (β := ℝ) x 1 / x ^ y = x / x ^ y
rw₁ rw₂ : x / x ^ y = x / x ^ y
⊢ x ^ (1 - y) = x / x ^ y

Tactic:
rw [rpow_sub' h, rpow_one]

Premises used: NNReal.rpow_sub', NNReal.rpow_one
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y : ℝ
hy : y ≠ 0
x : ℝ≥0
rw : x ^ (y * (1 / y)) = x
⊢ (x ^ y) ^ (1 / y) = x

Tactic:
rw [← rpow_mul]

Premises used: NNReal.rpow_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y : ℝ
hy : y ≠ 0
x : ℝ≥0
field_simp : HPow.hPow (β := ℝ) x 1 = x
⊢ x ^ (y * (1 / y)) = x

Tactic:
field_simp
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y : ℝ
hy : y ≠ 0
x : ℝ≥0
⊢ HPow.hPow (β := ℝ) x 1 = x

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y : ℝ
hy : y ≠ 0
x : ℝ≥0
rw : x ^ (1 / y * y) = x
⊢ (x ^ (1 / y)) ^ y = x

Tactic:
rw [← rpow_mul]

Premises used: NNReal.rpow_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y : ℝ
hy : y ≠ 0
x : ℝ≥0
field_simp : HPow.hPow (β := ℝ) x 1 = x
⊢ x ^ (1 / y * y) = x

Tactic:
field_simp
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0
y : ℝ
⊢ x⁻¹ ^ y = (x ^ y)⁻¹

Tactic:
NNReal.eq <| Real.inv_rpow x.2 y

Premises used: Real.inv_rpow, NNReal.eq, Subtype.property
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x y : ℝ≥0
z : ℝ
⊢ (x / y) ^ z = x ^ z / y ^ z

Tactic:
NNReal.eq <| Real.div_rpow x.2 y.2 z

Premises used: NNReal.eq, Real.div_rpow, Subtype.property
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0
⊢ (sqrt : (a : ℝ≥0) → ℝ≥0) x = x ^ (1 / 2)

Tactic:
NNReal.eq ?_

Premises used: NNReal.eq
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0
refine : (↑((sqrt : (a : ℝ≥0) → ℝ≥0) x) : ℝ) = (↑(x ^ (1 / 2)) : ℝ)
⊢ (sqrt : (a : ℝ≥0) → ℝ≥0) x = x ^ (1 / 2)

Tactic:
refine NNReal.eq ?_

Premises used: NNReal.eq
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0
push_cast : √(↑x : ℝ) = (↑x : ℝ) ^ (1 / 2)
⊢ (↑((sqrt : (a : ℝ≥0) → ℝ≥0) x) : ℝ) = (↑(x ^ (1 / 2)) : ℝ)

Tactic:
push_cast
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0
⊢ √(↑x : ℝ) = (↑x : ℝ) ^ (1 / 2)

Tactic:
Real.sqrt_eq_rpow x.1

Premises used: Subtype.val, NNReal.toReal, Real.sqrt_eq_rpow
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0
⊢ √(↑x : ℝ) = (↑x : ℝ) ^ (1 / 2)

Tactic:
exact Real.sqrt_eq_rpow x.1

Premises used: Subtype.val, Real.sqrt_eq_rpow
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0
n : ℕ
inst : n.AtLeastTwo
⊢ HPow.hPow (β := ℝ) x (OfNat.ofNat n) = HPow.hPow (β := ℕ) x (OfNat.ofNat n)

Tactic:
rpow_natCast x n

Premises used: NNReal.rpow_natCast
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0
⊢ HPow.hPow (β := ℝ) x 2 = HPow.hPow (β := ℕ) x 2

Tactic:
rpow_ofNat x 2

Premises used: NNReal.rpow_ofNat, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x y : ℝ≥0
z : ℝ
⊢ (x * y) ^ z = x ^ z * y ^ z

Tactic:
NNReal.eq <| Real.mul_rpow x.2 y.2

Premises used: Real.mul_rpow, NNReal.eq, Subtype.property
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
l : List ℝ≥0
r : ℝ
⊢ List.prod (List.map (fun (x : ℝ≥0) ↦ x ^ r) l) = l.prod ^ r

Tactic:
l.prod_hom (rpowMonoidHom r)

Premises used: List.prod_hom, NNReal.rpowMonoidHom
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
ι : Type u_1
l : List ι
f : ι → ℝ≥0
r : ℝ
rw :
  Eq (α := ℝ≥0) (List.prod (List.map (fun (x : ι) ↦ f x ^ r) l)) (List.prod (List.map ((fun (x : ℝ≥0) ↦ x ^ r) ∘ f) l))
⊢ List.prod (List.map (fun (x : ι) ↦ f x ^ r) l) = (List.map f l).prod ^ r

Tactic:
rw [← list_prod_map_rpow, List.map_map]

Premises used: List.map_map, NNReal.list_prod_map_rpow
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
ι : Type u_1
l : List ι
f : ι → ℝ≥0
r : ℝ
⊢ Eq (α := ℝ≥0) (List.prod (List.map (fun (x : ι) ↦ f x ^ r) l)) (List.prod (List.map ((fun (x : ℝ≥0) ↦ x ^ r) ∘ f) l))

Tactic:
rfl