awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
ι : Type u_1
s : Multiset ι
f : ι → ℝ≥0
r : ℝ
⊢ Multiset.prod (Multiset.map (fun (x : ι) ↦ f x ^ r) s) = (Multiset.map f s).prod ^ r

Tactic:
s.prod_hom' (rpowMonoidHom r) _

Premises used: NNReal.rpowMonoidHom, Multiset.prod_hom'
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
ι : Type u_1
s : Finset ι
f : ι → ℝ≥0
r : ℝ
⊢ ∏ i ∈ s, f i ^ r = HPow.hPow (α := ℝ≥0) (∏ i ∈ s, f i) r

Tactic:
multiset_prod_map_rpow _ _ _

Premises used: Finset.prod, NNReal.multiset_prod_map_rpow
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
l : List ℝ
hl : ∀ x ∈ l, 0 ≤ x
r : ℝ
⊢ ∀ x ∈ l, 0 ≤ x

Tactic:
hl
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
l : List ℝ
hl : ∀ x ∈ l, 0 ≤ x
r : ℝ
lift : ∀ (l : List ℝ≥0), List.prod (List.map (fun (x : ℝ) ↦ x ^ r) (List.map toReal l)) = (List.map toReal l).prod ^ r
⊢ List.prod (List.map (fun (x : ℝ) ↦ x ^ r) l) = l.prod ^ r

Tactic:
lift l to List ℝ≥0 using hl

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

Tactic:
have := congr_arg ((↑) : ℝ≥0 → ℝ) (NNReal.list_prod_map_rpow l r)
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
r : ℝ
l : List ℝ≥0
this : (↑(List.prod (List.map (fun (x : ℝ≥0) ↦ x ^ r) l)) : ℝ) = (↑(l.prod ^ r) : ℝ)
⊢ (List.map toReal (List.map (fun (x : ℝ≥0) ↦ x ^ r) l)).prod = (List.map toReal l).prod ^ r

Tactic:
push_cast at this
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
r : ℝ
l : List ℝ≥0
this : (List.map toReal (List.map (fun (x : ℝ≥0) ↦ x ^ r) l)).prod = (List.map toReal l).prod ^ r
rw :
  ∀ (this : (List.map (toReal ∘ fun (x : ℝ≥0) ↦ x ^ r) l).prod = (List.map toReal l).prod ^ r),
    List.prod (List.map ((fun (x : ℝ) ↦ x ^ r) ∘ toReal) l) = (List.map toReal l).prod ^ r
⊢ List.prod (List.map (fun (x : ℝ) ↦ x ^ r) (List.map toReal l)) = (List.map toReal l).prod ^ r

Tactic:
rw [List.map_map] at this ⊢

Premises used: List.map_map
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
r : ℝ
l : List ℝ≥0
this : (List.map (toReal ∘ fun (x : ℝ≥0) ↦ x ^ r) l).prod = (List.map toReal l).prod ^ r
⊢ List.prod (List.map ((fun (x : ℝ) ↦ x ^ r) ∘ toReal) l) = (List.map toReal l).prod ^ r

Tactic:
mod_cast this

Premises used: List.map, cast, Function.comp, HPow.hPow, Eq.refl, Eq, NNReal.toReal, List.prod
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
r : ℝ
l : List ℝ≥0
this : (List.map (toReal ∘ fun (x : ℝ≥0) ↦ x ^ r) l).prod = (List.map toReal l).prod ^ r
⊢ List.prod (List.map ((fun (x : ℝ) ↦ x ^ r) ∘ toReal) l) = (List.map toReal l).prod ^ r

Tactic:
exact mod_cast this
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
ι : Type u_1
l : List ι
f : ι → ℝ
hl : ∀ i ∈ l, 0 ≤ f i
r : ℝ
rw : Eq (α := ℝ) (List.prod (List.map (fun (x : ι) ↦ f x ^ r) l)) (List.prod (List.map ((fun (x : ℝ) ↦ x ^ r) ∘ f) l))
rw₁ : ∀ x ∈ List.map f l, 0 ≤ x
⊢ List.prod (List.map (fun (x : ι) ↦ f x ^ r) l) = (List.map f l).prod ^ r

Tactic:
rw [← Real.list_prod_map_rpow (l.map f) _ r, List.map_map]

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

Tactic:
rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
ι : Type u_1
l : List ι
f : ι → ℝ
hl : ∀ i ∈ l, 0 ≤ f i
r : ℝ
⊢ ∀ x ∈ List.map f l, 0 ≤ x

Tactic:
simpa using hl
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
ι : Type u_1
s : Multiset ι
f : ι → ℝ
hs : ∀ i ∈ s, 0 ≤ f i
r : ℝ
mk :
  ∀ (l : List ι)
    (hs :
      ∀ (i : ι),
        Membership.mem (γ := Multiset ι) (Quot.mk (⇑(List.isSetoid ι) : List ι → List ι → Prop) l) i → 0 ≤ f i),
    Multiset.prod (Multiset.map (fun (x : ι) ↦ f x ^ r) (Quot.mk (⇑(List.isSetoid ι) : List ι → List ι → Prop) l)) =
      (Multiset.map f (Quot.mk (⇑(List.isSetoid ι) : List ι → List ι → Prop) l)).prod ^ r
⊢ Multiset.prod (Multiset.map (fun (x : ι) ↦ f x ^ r) s) = (Multiset.map f s).prod ^ r

Tactic:
obtain ⟨l⟩ := s
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
ι : Type u_1
s : Multiset ι
f : ι → ℝ
r : ℝ
l : List ι
hs : ∀ (i : ι), Membership.mem (γ := Multiset ι) (Quot.mk (⇑(List.isSetoid ι) : List ι → List ι → Prop) l) i → 0 ≤ f i
⊢ Multiset.prod (Multiset.map (fun (x : ι) ↦ f x ^ r) (Quot.mk (⇑(List.isSetoid ι) : List ι → List ι → Prop) l)) =
    (Multiset.map f (Quot.mk (⇑(List.isSetoid ι) : List ι → List ι → Prop) l)).prod ^ r

Tactic:
simpa using Real.list_prod_map_rpow' l f hs r

Premises used: Real.list_prod_map_rpow'
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
ι : Type u_1
s : Finset ι
f : ι → ℝ
hs : ∀ i ∈ s, 0 ≤ f i
r : ℝ
⊢ ∏ i ∈ s, f i ^ r = HPow.hPow (α := ℝ) (∏ i ∈ s, f i) r

Tactic:
Real.multiset_prod_map_rpow s.val f hs r

Premises used: Real.multiset_prod_map_rpow, Finset.val, Finset.prod
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x y : ℝ≥0
z : ℝ
h₁ : x ≤ y
h₂ : 0 ≤ z
⊢ x ^ z ≤ y ^ z

Tactic:
Real.rpow_le_rpow x.2 h₁ h₂

Premises used: Real.rpow_le_rpow, Subtype.property
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x y : ℝ≥0
z : ℝ
h₁ : x < y
h₂ : 0 < z
⊢ x ^ z < y ^ z

Tactic:
Real.rpow_lt_rpow x.2 h₁ h₂

Premises used: Real.rpow_lt_rpow, Subtype.property
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x y : ℝ≥0
z : ℝ
hz : 0 < z
⊢ x ^ z < y ^ z ↔ x < y

Tactic:
Real.rpow_lt_rpow_iff x.2 y.2 hz

Premises used: Real.rpow_lt_rpow_iff, NNReal.toReal, Subtype.property
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x y : ℝ≥0
z : ℝ
hz : 0 < z
⊢ x ^ z ≤ y ^ z ↔ x ≤ y

Tactic:
Real.rpow_le_rpow_iff x.2 y.2 hz

Premises used: Real.rpow_le_rpow_iff, NNReal.toReal, Subtype.property
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x y : ℝ≥0
z : ℝ
hz : 0 < z
rw : x ^ z ≤ (y ^ z⁻¹) ^ z ↔ x ^ z ≤ y
rw₁ : x ^ z ≤ (y ^ (1 / z)) ^ z ↔ x ^ z ≤ y
rw₂ rw₃ : x ^ z ≤ y ↔ x ^ z ≤ y
⊢ x ≤ y ^ z⁻¹ ↔ x ^ z ≤ y

Tactic:
rw [← rpow_le_rpow_iff hz, ← one_div, rpow_self_rpow_inv hz.ne']

Premises used: LT.lt.ne', one_div, NNReal.rpow_self_rpow_inv, NNReal.rpow_le_rpow_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x y : ℝ≥0
z : ℝ
hz : 0 < z
rw : (x ^ z⁻¹) ^ z ≤ y ^ z ↔ x ≤ y ^ z
rw₁ : (x ^ (1 / z)) ^ z ≤ y ^ z ↔ x ≤ y ^ z
rw₂ rw₃ : x ≤ y ^ z ↔ x ≤ y ^ z
⊢ x ^ z⁻¹ ≤ y ↔ x ≤ y ^ z

Tactic:
rw [← rpow_le_rpow_iff hz, ← one_div, rpow_self_rpow_inv hz.ne']

Premises used: LT.lt.ne', one_div, NNReal.rpow_self_rpow_inv, NNReal.rpow_le_rpow_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x y : ℝ≥0
z : ℝ
hz : 0 < z
⊢ x < y ^ z⁻¹ ↔ x ^ z < y

Tactic:
simp only [← not_le, rpow_inv_le_iff hz]

Premises used: not_le, NNReal.rpow_inv_le_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x y : ℝ≥0
z : ℝ
hz : 0 < z
⊢ x ^ z⁻¹ < y ↔ x < y ^ z

Tactic:
simp only [← not_le, le_rpow_inv_iff hz]

Premises used: not_le, NNReal.le_rpow_inv_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0
z : ℝ
y : ℝ≥0
hx : 0 < x
hxy : x < y
hz : z < 0
⊢ y ^ z < x ^ z

Tactic:
Real.rpow_lt_rpow_of_neg hx hxy hz

Premises used: Real.rpow_lt_rpow_of_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0
z : ℝ
y : ℝ≥0
hx : 0 < x
hxy : x ≤ y
hz : z ≤ 0
⊢ y ^ z ≤ x ^ z

Tactic:
Real.rpow_le_rpow_of_nonpos hx hxy hz

Premises used: Real.rpow_le_rpow_of_nonpos
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0
z : ℝ
y : ℝ≥0
hx : 0 < x
hy : 0 < y
hz : z < 0
⊢ x ^ z < y ^ z ↔ y < x

Tactic:
Real.rpow_lt_rpow_iff_of_neg hx hy hz

Premises used: Real.rpow_lt_rpow_iff_of_neg, NNReal.toReal
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0
z : ℝ
y : ℝ≥0
hx : 0 < x
hy : 0 < y
hz : z < 0
⊢ x ^ z ≤ y ^ z ↔ y ≤ x

Tactic:
Real.rpow_le_rpow_iff_of_neg hx hy hz

Premises used: Real.rpow_le_rpow_iff_of_neg, NNReal.toReal
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
z : ℝ
y : ℝ≥0
hy : 0 ≤ y
hz : 0 < z
x : ℝ≥0
⊢ x ≤ y ^ z⁻¹ ↔ x ^ z ≤ y

Tactic:
Real.le_rpow_inv_iff_of_pos x.2 hy hz

Premises used: Real.le_rpow_inv_iff_of_pos, NNReal.toReal, Subtype.property
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
z : ℝ
y : ℝ≥0
hy : 0 ≤ y
hz : 0 < z
x : ℝ≥0
⊢ x ^ z⁻¹ ≤ y ↔ x ≤ y ^ z

Tactic:
Real.rpow_inv_le_iff_of_pos x.2 hy hz

Premises used: Real.rpow_inv_le_iff_of_pos, NNReal.toReal, Subtype.property
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
z : ℝ
y : ℝ≥0
hy : 0 ≤ y
hz : 0 < z
x : ℝ≥0
⊢ x < y ^ z⁻¹ ↔ x ^ z < y

Tactic:
Real.lt_rpow_inv_iff_of_pos x.2 hy hz

Premises used: Real.lt_rpow_inv_iff_of_pos, NNReal.toReal, Subtype.property
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
z : ℝ
y : ℝ≥0
hy : 0 ≤ y
hz : 0 < z
x : ℝ≥0
⊢ x ^ z⁻¹ < y ↔ x < y ^ z

Tactic:
Real.rpow_inv_lt_iff_of_pos x.2 hy hz

Premises used: Real.rpow_inv_lt_iff_of_pos, NNReal.toReal, Subtype.property
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0
z : ℝ
y : ℝ≥0
hx : 0 < x
hy : 0 < y
hz : z < 0
⊢ x ≤ y ^ z⁻¹ ↔ y ≤ x ^ z

Tactic:
Real.le_rpow_inv_iff_of_neg hx hy hz

Premises used: Real.le_rpow_inv_iff_of_neg, NNReal.toReal
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0
z : ℝ
y : ℝ≥0
hx : 0 < x
hy : 0 < y
hz : z < 0
⊢ x < y ^ z⁻¹ ↔ y < x ^ z

Tactic:
Real.lt_rpow_inv_iff_of_neg hx hy hz

Premises used: Real.lt_rpow_inv_iff_of_neg, NNReal.toReal
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0
z : ℝ
y : ℝ≥0
hx : 0 < x
hy : 0 < y
hz : z < 0
⊢ x ^ z⁻¹ < y ↔ y ^ z < x

Tactic:
Real.rpow_inv_lt_iff_of_neg hx hy hz

Premises used: Real.rpow_inv_lt_iff_of_neg, NNReal.toReal
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0
z : ℝ
y : ℝ≥0
hx : 0 < x
hy : 0 < y
hz : z < 0
⊢ x ^ z⁻¹ ≤ y ↔ y ^ z ≤ x

Tactic:
Real.rpow_inv_le_iff_of_neg hx hy hz

Premises used: Real.rpow_inv_le_iff_of_neg, NNReal.toReal
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0
y z : ℝ
hx : 1 < x
hyz : y < z
⊢ x ^ y < x ^ z

Tactic:
Real.rpow_lt_rpow_of_exponent_lt hx hyz

Premises used: Real.rpow_lt_rpow_of_exponent_lt
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0
y z : ℝ
hx : 1 ≤ x
hyz : y ≤ z
⊢ x ^ y ≤ x ^ z

Tactic:
Real.rpow_le_rpow_of_exponent_le hx hyz

Premises used: Real.rpow_le_rpow_of_exponent_le
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0
y z : ℝ
hx0 : 0 < x
hx1 : x < 1
hyz : z < y
⊢ x ^ y < x ^ z

Tactic:
Real.rpow_lt_rpow_of_exponent_gt hx0 hx1 hyz

Premises used: Real.rpow_lt_rpow_of_exponent_gt
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0
y z : ℝ
hx0 : 0 < x
hx1 : x ≤ 1
hyz : z ≤ y
⊢ x ^ y ≤ x ^ z

Tactic:
Real.rpow_le_rpow_of_exponent_ge hx0 hx1 hyz

Premises used: Real.rpow_le_rpow_of_exponent_ge
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
p_1 : ℝ
x : ℝ≥0
hx_pos : 0 < x
p : ℝ
hp_pos : 0 < p
rw : HPow.hPow (α := ℝ≥0) 0 p < x ^ p
⊢ 0 < x ^ p

Tactic:
rw [← zero_rpow hp_pos.ne']

Premises used: NNReal.zero_rpow, LT.lt.ne'
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
p_1 : ℝ
x : ℝ≥0
hx_pos : 0 < x
p : ℝ
hp_pos : 0 < p
⊢ HPow.hPow (α := ℝ≥0) 0 p < x ^ p

Tactic:
rpow_lt_rpow hx_pos hp_pos

Premises used: NNReal.rpow_lt_rpow
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
p_1 : ℝ
x : ℝ≥0
hx_pos : 0 < x
p : ℝ
hp_pos : 0 < p
⊢ HPow.hPow (α := ℝ≥0) 0 p < x ^ p

Tactic:
exact rpow_lt_rpow hx_pos hp_pos

Premises used: NNReal.rpow_lt_rpow
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
p : ℝ
x : ℝ≥0
hx_pos : 0 < x
⊢ ∀ {p : ℝ}, 0 < p → 0 < x ^ p

Tactic:
have rpow_pos_of_nonneg : ∀ {p : ℝ}, 0 < p → 0 < x ^ p := by
    intro p hp_pos
    rw [← zero_rpow hp_pos.ne']
    exact rpow_lt_rpow hx_pos hp_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
p : ℝ
x : ℝ≥0
hx_pos : 0 < x
rpow_pos_of_nonneg : ∀ {p : ℝ}, 0 < p → 0 < x ^ p
inl : ∀ (hp_pos : 0 < p), 0 < x ^ p
inr : 0 < HPow.hPow (β := ℝ) x 0
inr₁ : ∀ (hp_neg : p < 0), 0 < x ^ p
⊢ 0 < x ^ p

Tactic:
rcases lt_trichotomy (0 : ℝ) p with (hp_pos | rfl | hp_neg)

Premises used: OfNat.ofNat, rfl, lt_trichotomy
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
p : ℝ
x : ℝ≥0
hx_pos : 0 < x
rpow_pos_of_nonneg : ∀ {p : ℝ}, 0 < p → 0 < x ^ p
hp_pos : 0 < p
⊢ 0 < x ^ p

Tactic:
rpow_pos_of_nonneg hp_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
p : ℝ
x : ℝ≥0
hx_pos : 0 < x
rpow_pos_of_nonneg : ∀ {p : ℝ}, 0 < p → 0 < x ^ p
hp_pos : 0 < p
⊢ 0 < x ^ p

Tactic:
exact rpow_pos_of_nonneg hp_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0
hx_pos : 0 < x
rpow_pos_of_nonneg : ∀ {p : ℝ}, 0 < p → 0 < x ^ p
⊢ 0 < HPow.hPow (β := ℝ) x 0

Tactic:
simp only [zero_lt_one, rpow_zero]

Premises used: zero_lt_one, NNReal.rpow_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
p : ℝ
x : ℝ≥0
hx_pos : 0 < x
rpow_pos_of_nonneg : ∀ {p : ℝ}, 0 < p → 0 < x ^ p
hp_neg : p < 0
inr : 0 < x ^ (-p)
⊢ 0 < x ^ p

Tactic:
rw [← neg_neg p, rpow_neg, inv_pos]

Premises used: neg_neg, inv_pos, NNReal.rpow_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
p : ℝ
x : ℝ≥0
hx_pos : 0 < x
rpow_pos_of_nonneg : ∀ {p : ℝ}, 0 < p → 0 < x ^ p
hp_neg : p < 0
⊢ 0 < x ^ (-p)

Tactic:
rpow_pos_of_nonneg (neg_pos.mpr hp_neg)

Premises used: Iff.mpr, neg_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
p : ℝ
x : ℝ≥0
hx_pos : 0 < x
rpow_pos_of_nonneg : ∀ {p : ℝ}, 0 < p → 0 < x ^ p
hp_neg : p < 0
⊢ 0 < x ^ (-p)

Tactic:
exact rpow_pos_of_nonneg (neg_pos.mpr hp_neg)

Premises used: Iff.mpr, neg_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0
z : ℝ
hx1 : x < 1
hz : 0 < z
⊢ x ^ z < 1

Tactic:
Real.rpow_lt_one (coe_nonneg x) hx1 hz

Premises used: Real.rpow_lt_one, NNReal.coe_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0
z : ℝ
hx2 : x ≤ 1
hz : 0 ≤ z
⊢ x ^ z ≤ 1

Tactic:
Real.rpow_le_one x.2 hx2 hz

Premises used: Real.rpow_le_one, Subtype.property
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0
z : ℝ
hx : 1 < x
hz : z < 0
⊢ x ^ z < 1

Tactic:
Real.rpow_lt_one_of_one_lt_of_neg hx hz

Premises used: Real.rpow_lt_one_of_one_lt_of_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0
z : ℝ
hx : 1 ≤ x
hz : z ≤ 0
⊢ x ^ z ≤ 1

Tactic:
Real.rpow_le_one_of_one_le_of_nonpos hx hz

Premises used: Real.rpow_le_one_of_one_le_of_nonpos
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0
z : ℝ
hx : 1 < x
hz : 0 < z
⊢ 1 < x ^ z

Tactic:
Real.one_lt_rpow hx hz

Premises used: Real.one_lt_rpow
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0
z : ℝ
h : 1 ≤ x
h₁ : 0 ≤ z
⊢ 1 ≤ x ^ z

Tactic:
Real.one_le_rpow h h₁

Premises used: Real.one_le_rpow
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0
z : ℝ
hx1 : 0 < x
hx2 : x < 1
hz : z < 0
⊢ 1 < x ^ z

Tactic:
Real.one_lt_rpow_of_pos_of_lt_one_of_neg hx1 hx2 hz

Premises used: Real.one_lt_rpow_of_pos_of_lt_one_of_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0
z : ℝ
hx1 : 0 < x
hx2 : x ≤ 1
hz : z ≤ 0
⊢ 1 ≤ x ^ z

Tactic:
Real.one_le_rpow_of_pos_of_le_one_of_nonpos hx1 hx2 hz

Premises used: Real.one_le_rpow_of_pos_of_le_one_of_nonpos
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0
z : ℝ
hx : x ≤ 1
h_one_le : 1 ≤ z
inl : ∀ (hx : LE.le (α := ℝ≥0) ⊥ 1), HPow.hPow (α := ℝ≥0) ⊥ z ≤ ⊥
inr : ∀ (h : 0 < x), x ^ z ≤ x
⊢ x ^ z ≤ x

Tactic:
rcases eq_bot_or_bot_lt x with (rfl | (h : 0 < x))

Premises used: eq_bot_or_bot_lt, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
z : ℝ
h_one_le : 1 ≤ z
hx : LE.le (α := ℝ≥0) ⊥ 1
linarith : z = 0 → -1 + (1 - z) + (z - 0) = 0
⊢ z ≠ 0

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
z : ℝ
h_one_le : 1 ≤ z
hx : LE.le (α := ℝ≥0) ⊥ 1
⊢ z ≠ 0

Tactic:
have : z ≠ 0 := by linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
z : ℝ
h_one_le : 1 ≤ z
hx : LE.le (α := ℝ≥0) ⊥ 1
this : z ≠ 0
⊢ HPow.hPow (α := ℝ≥0) ⊥ z ≤ ⊥

Tactic:
simp [this]
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0
z : ℝ
hx : x ≤ 1
h_one_le : 1 ≤ z
h : 0 < x
inr : x ^ z ≤ HPow.hPow (β := ℝ) x 1
⊢ x ^ z ≤ x

Tactic:
nth_rw 2 [← NNReal.rpow_one x]

Premises used: NNReal.rpow_one
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0
z : ℝ
hx : x ≤ 1
h_one_le : 1 ≤ z
h : 0 < x
⊢ x ^ z ≤ HPow.hPow (β := ℝ) x 1

Tactic:
NNReal.rpow_le_rpow_of_exponent_ge h hx h_one_le

Premises used: NNReal.rpow_le_rpow_of_exponent_ge
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0
z : ℝ
hx : x ≤ 1
h_one_le : 1 ≤ z
h : 0 < x
⊢ x ^ z ≤ HPow.hPow (β := ℝ) x 1

Tactic:
exact NNReal.rpow_le_rpow_of_exponent_ge h hx h_one_le

Premises used: NNReal.rpow_le_rpow_of_exponent_ge
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ
hx : x ≠ 0
y z : ℝ≥0
hyz : Eq (α := ℝ≥0) ((fun (y : ℝ≥0) ↦ y ^ x) y) ((fun (y : ℝ≥0) ↦ y ^ x) z)
⊢ y = z

Tactic:
simpa only [rpow_inv_rpow_self hx] using congr_arg (fun y => y ^ (1 / x)) hyz

Premises used: HDiv.hDiv, NNReal.rpow_inv_rpow_self, congr_arg, HPow.hPow, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x y : ℝ≥0
z : ℝ
hz : z ≠ 0
⊢ x ^ z = y ^ z ↔ x = y

Tactic:
(rpow_left_injective hz).eq_iff

Premises used: Function.Injective.eq_iff, NNReal.rpow_left_injective
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ
hx : x ≠ 0
y : ℝ≥0
simp_rw simp_rw₁ : (y ^ x⁻¹) ^ x = y
simp_rw₂ : y ^ (x⁻¹ * x) = y
simp_rw₃ : HPow.hPow (β := ℝ) y 1 = y
⊢ (fun (y : ℝ≥0) ↦ y ^ x) (y ^ x⁻¹) = y

Tactic:
simp_rw [← rpow_mul, inv_mul_cancel₀ hx, rpow_one]

Premises used: NNReal.rpow_mul, NNReal.rpow_one, inv_mul_cancel₀
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ
hx : x ≠ 0
⊢ Bijective (β := ℝ≥0) fun (y : ℝ≥0) ↦ y ^ x

Tactic:
⟨rpow_left_injective hx, rpow_left_surjective hx⟩

Premises used: NNReal.rpow_left_injective, And.intro, Function.Bijective, NNReal.rpow_left_surjective
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0
y z : ℝ
hx₀ : x ≠ 0
hx₁ : x ≠ 1
⊢ 0 < x

Tactic:
rw [← pos_iff_ne_zero] at hx₀

Premises used: pos_iff_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0
y z : ℝ
hx₀ : x ≠ 0
hx₁ : x ≠ 1
hx₂ : 0 < x
⊢ x ≠ 1

Tactic:
rw [← pos_iff_ne_zero] at hx₀

Premises used: pos_iff_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0
y z : ℝ
hx₀ : 0 < x
hx₁ : x ≠ 1
rify : ∀ (hx₀ : 0 < (↑x : ℝ)) (hx₁ : (↑x : ℝ) ≠ 1), (↑x : ℝ) ^ y = (↑x : ℝ) ^ z ↔ y = z
⊢ x ^ y = x ^ z ↔ y = z

Tactic:
rify at *
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0
y z : ℝ
hx₀ : 0 < (↑x : ℝ)
hx₁ : (↑x : ℝ) ≠ 1
⊢ (↑x : ℝ) ^ y = (↑x : ℝ) ^ z ↔ y = z

Tactic:
grind [Real.rpow_right_inj]

Premises used: Real.rpow_right_inj
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0
y z : ℝ
inl :
  HPow.hPow (α := ℝ≥0) 0 y = HPow.hPow (α := ℝ≥0) 0 z ↔ y = z ∨ Eq (α := ℝ≥0) 0 1 ∨ Eq (α := ℝ≥0) 0 0 ∧ (y = 0 ↔ z = 0)
inr : ∀ (hx₀ : x ≠ 0), x ^ y = x ^ z ↔ y = z ∨ x = 1 ∨ x = 0 ∧ (y = 0 ↔ z = 0)
⊢ x ^ y = x ^ z ↔ y = z ∨ x = 1 ∨ x = 0 ∧ (y = 0 ↔ z = 0)

Tactic:
obtain rfl | hx₀ := eq_or_ne x 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y z : ℝ
inl :
  HPow.hPow (α := ℝ≥0) 0 y = HPow.hPow (α := ℝ≥0) (β := ℝ) 0 0 ↔
    y = 0 ∨ Eq (α := ℝ≥0) 0 1 ∨ Eq (α := ℝ≥0) 0 0 ∧ (y = 0 ↔ Eq (α := ℝ) 0 0)
inl₁ :
  ∀ (hz : z ≠ 0),
    HPow.hPow (α := ℝ≥0) 0 y = HPow.hPow (α := ℝ≥0) 0 z ↔
      y = z ∨ Eq (α := ℝ≥0) 0 1 ∨ Eq (α := ℝ≥0) 0 0 ∧ (y = 0 ↔ z = 0)
⊢ HPow.hPow (α := ℝ≥0) 0 y = HPow.hPow (α := ℝ≥0) 0 z ↔ y = z ∨ Eq (α := ℝ≥0) 0 1 ∨ Eq (α := ℝ≥0) 0 0 ∧ (y = 0 ↔ z = 0)

Tactic:
obtain rfl | hz := eq_or_ne z 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y : ℝ
⊢ HPow.hPow (α := ℝ≥0) 0 y = HPow.hPow (α := ℝ≥0) (β := ℝ) 0 0 ↔
    y = 0 ∨ Eq (α := ℝ≥0) 0 1 ∨ Eq (α := ℝ≥0) 0 0 ∧ (y = 0 ↔ Eq (α := ℝ) 0 0)

Tactic:
simp [zero_rpow_def]

Premises used: NNReal.zero_rpow_def
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y z : ℝ
hz : z ≠ 0
⊢ HPow.hPow (α := ℝ≥0) 0 y = HPow.hPow (α := ℝ≥0) 0 z ↔ y = z ∨ Eq (α := ℝ≥0) 0 1 ∨ Eq (α := ℝ≥0) 0 0 ∧ (y = 0 ↔ z = 0)

Tactic:
simp +contextual [hz]
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0
y z : ℝ
hx₀ : x ≠ 0
inr :
  ∀ (hx₀ : Ne (α := ℝ≥0) 1 0),
    HPow.hPow (α := ℝ≥0) 1 y = HPow.hPow (α := ℝ≥0) 1 z ↔
      y = z ∨ Eq (α := ℝ≥0) 1 1 ∨ Eq (α := ℝ≥0) 1 0 ∧ (y = 0 ↔ z = 0)
inr₁ : ∀ (hx₁ : x ≠ 1), x ^ y = x ^ z ↔ y = z ∨ x = 1 ∨ x = 0 ∧ (y = 0 ↔ z = 0)
⊢ x ^ y = x ^ z ↔ y = z ∨ x = 1 ∨ x = 0 ∧ (y = 0 ↔ z = 0)

Tactic:
obtain rfl | hx₁ := eq_or_ne x 1

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y z : ℝ
hx₀ : Ne (α := ℝ≥0) 1 0
⊢ HPow.hPow (α := ℝ≥0) 1 y = HPow.hPow (α := ℝ≥0) 1 z ↔ y = z ∨ Eq (α := ℝ≥0) 1 1 ∨ Eq (α := ℝ≥0) 1 0 ∧ (y = 0 ↔ z = 0)

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0
y z : ℝ
hx₀ : x ≠ 0
hx₁ : x ≠ 1
⊢ x ^ y = x ^ z ↔ y = z ∨ x = 1 ∨ x = 0 ∧ (y = 0 ↔ z = 0)

Tactic:
simpa [hx₀, hx₁] using rpow_right_inj (y := y) (z := z) hx₀ hx₁

Premises used: NNReal.rpow_right_inj
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0
y : ℝ
⊢ x ^ y = x ↔ x = 1 ∨ y = 1 ∨ x = 0 ∧ y ≠ 0

Tactic:
simpa [or_left_comm] using rpow_eq_rpow_right_iff (x := x) (y := y) (z := 1)

Premises used: or_left_comm, NNReal.rpow_eq_rpow_right_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x y : ℝ≥0
z : ℝ
hz : z ≠ 0
rw : x ^ z = (y ^ z⁻¹) ^ z ↔ x ^ z = y
rw₁ : x ^ z = (y ^ (1 / z)) ^ z ↔ x ^ z = y
rw₂ rw₃ : x ^ z = y ↔ x ^ z = y
⊢ x = y ^ z⁻¹ ↔ x ^ z = y

Tactic:
rw [← rpow_eq_rpow_iff hz, ← one_div, rpow_self_rpow_inv hz]

Premises used: NNReal.rpow_eq_rpow_iff, one_div, NNReal.rpow_self_rpow_inv
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x y : ℝ≥0
z : ℝ
hz : z ≠ 0
rw : (x ^ z⁻¹) ^ z = y ^ z ↔ x = y ^ z
rw₁ : (x ^ (1 / z)) ^ z = y ^ z ↔ x = y ^ z
rw₂ rw₃ : x = y ^ z ↔ x = y ^ z
⊢ x ^ z⁻¹ = y ↔ x = y ^ z

Tactic:
rw [← rpow_eq_rpow_iff hz, ← one_div, rpow_self_rpow_inv hz]

Premises used: NNReal.rpow_eq_rpow_iff, one_div, NNReal.rpow_self_rpow_inv
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y : ℝ
hy : y ≠ 0
x : ℝ≥0
rw : x ^ (y * y⁻¹) = x
rw₁ : HPow.hPow (β := ℝ) x 1 = x
rw₂ rw₃ : x = x
⊢ (x ^ y) ^ y⁻¹ = x

Tactic:
rw [← rpow_mul, mul_inv_cancel₀ hy, rpow_one]

Premises used: mul_inv_cancel₀, NNReal.rpow_mul, NNReal.rpow_one
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y : ℝ
hy : y ≠ 0
x : ℝ≥0
rw : x ^ (y⁻¹ * y) = x
rw₁ : HPow.hPow (β := ℝ) x 1 = x
rw₂ rw₃ : x = x
⊢ (x ^ y⁻¹) ^ y = x

Tactic:
rw [← rpow_mul, inv_mul_cancel₀ hy, rpow_one]

Premises used: NNReal.rpow_mul, NNReal.rpow_one, inv_mul_cancel₀
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0
y : ℝ
⊢ (x ^ y) ^ y⁻¹ = x ↔ y ≠ 0 ∨ x = 1

Tactic:
grind only [rpow_rpow_inv, rpow_zero]

Premises used: NNReal.rpow_rpow_inv, NNReal.rpow_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0
y : ℝ
⊢ (x ^ y⁻¹) ^ y = x ↔ y ≠ 0 ∨ x = 1

Tactic:
grind [rpow_rpow_inv_eq_iff]

Premises used: NNReal.rpow_rpow_inv_eq_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0
n : ℕ
hn : n ≠ 0
rw : HPow.hPow (β := ℝ) ((↑x : ℝ) ^ n) (↑n : ℝ)⁻¹ = (↑x : ℝ)
⊢ HPow.hPow (β := ℝ) (x ^ n) (↑n : ℝ)⁻¹ = x

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

Premises used: NNReal.coe_rpow, NNReal.coe_pow, NNReal.coe_inj
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0
n : ℕ
hn : n ≠ 0
⊢ HPow.hPow (β := ℝ) ((↑x : ℝ) ^ n) (↑n : ℝ)⁻¹ = (↑x : ℝ)

Tactic:
Real.pow_rpow_inv_natCast x.2 hn

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

Tactic:
exact Real.pow_rpow_inv_natCast x.2 hn

Premises used: Real.pow_rpow_inv_natCast, Subtype.property