awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x y : ℝ≥0∞
hx : x ≠ 0
hy : y ≠ 0
z : ℝ
⊢ (x * y) ^ z = x ^ z * y ^ z

Tactic:
simp [*, mul_rpow_eq_ite]

Premises used: ENNReal.mul_rpow_eq_ite
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x y : ℝ≥0∞
z : ℝ
hz : 0 ≤ z
⊢ (x * y) ^ z = x ^ z * y ^ z

Tactic:
simp [hz.not_gt, mul_rpow_eq_ite]

Premises used: ENNReal.mul_rpow_eq_ite, LE.le.not_gt
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
ι : Type u_1
f : ι → ℝ≥0∞
r : ℝ
hf : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → f i ≠ ∞
⊢ ∏ i ∈ ∅, f i ^ r = HPow.hPow (α := ℝ≥0∞) (∏ i ∈ ∅, f i) r

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
ι : Type u_1
f : ι → ℝ≥0∞
r : ℝ
i : ι
s : Finset ι
hi : i ∉ s
ih : ∀ (hf : ∀ i ∈ s, f i ≠ ∞), ∏ i ∈ s, f i ^ r = HPow.hPow (α := ℝ≥0∞) (∏ i ∈ s, f i) r
hf : ∀ i_1 ∈ insert i s, f i_1 ≠ ∞
⊢ ∀ i ∈ s, f i ≠ ∞

Tactic:
have h2f : ∀ i ∈ s, f i ≠ ∞ := fun i hi ↦ hf i <| mem_insert_of_mem hi
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
ι : Type u_1
f : ι → ℝ≥0∞
r : ℝ
i : ι
s : Finset ι
hi : i ∉ s
ih : ∀ (hf : ∀ i ∈ s, f i ≠ ∞), ∏ i ∈ s, f i ^ r = HPow.hPow (α := ℝ≥0∞) (∏ i ∈ s, f i) r
hf : ∀ i_1 ∈ Insert.insert i s, f i_1 ≠ ∞
h2f : ∀ i ∈ s, f i ≠ ∞
insert : Ne (α := ℝ≥0∞) (∏ i ∈ s, f i) ∞
⊢ ∏ i ∈ Insert.insert i s, f i ^ r = HPow.hPow (α := ℝ≥0∞) (∏ i ∈ Insert.insert i s, f i) r

Tactic:
rw [prod_insert hi, prod_insert hi, ih h2f, ← mul_rpow_of_ne_top <| hf i <| mem_insert_self ..]

Premises used: Finset.prod_insert, Finset.mem_insert_self, ENNReal.mul_rpow_of_ne_top
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
ι : Type u_1
f : ι → ℝ≥0∞
r : ℝ
i : ι
s : Finset ι
hi : i ∉ s
ih : ∀ (hf : ∀ i ∈ s, f i ≠ ∞), ∏ i ∈ s, f i ^ r = HPow.hPow (α := ℝ≥0∞) (∏ i ∈ s, f i) r
hf : ∀ i_1 ∈ insert i s, f i_1 ≠ ∞
h2f : ∀ i ∈ s, f i ≠ ∞
⊢ Ne (α := ℝ≥0∞) (∏ i ∈ s, f i) ∞

Tactic:
apply prod_ne_top h2f

Premises used: ENNReal.prod_ne_top
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
ι : Type u_1
s : Finset ι
f : ι → ℝ≥0∞
hf : ∀ i ∈ s, f i ≠ ∞
r : ℝ
empty :
  ∀ (hf : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → f i ≠ ∞),
    ∏ i ∈ ∅, f i ^ r = HPow.hPow (α := ℝ≥0∞) (∏ i ∈ ∅, f i) r
insert :
  ∀ (i : ι) (s : Finset ι) (hi : i ∉ s)
    (ih : ∀ (hf : ∀ i ∈ s, f i ≠ ∞), ∏ i ∈ s, f i ^ r = HPow.hPow (α := ℝ≥0∞) (∏ i ∈ s, f i) r)
    (hf : ∀ i_1 ∈ Insert.insert i s, f i_1 ≠ ∞),
    ∏ i ∈ Insert.insert i s, f i ^ r = HPow.hPow (α := ℝ≥0∞) (∏ i ∈ Insert.insert i s, f i) r
⊢ ∏ i ∈ s, f i ^ r = HPow.hPow (α := ℝ≥0∞) (∏ i ∈ s, f i) r

Tactic:
induction s using Finset.induction with
  | empty => simp
  | insert i s hi ih =>
    have h2f : ∀ i ∈ s, f i ≠ ∞ := fun i hi ↦ hf i <| mem_insert_of_mem hi
    rw [prod_insert hi, prod_insert hi, ih h2f, ← mul_rpow_of_ne_top <| hf i <| mem_insert_self ..]
    apply prod_ne_top h2f

Premises used: Finset.mem_insert_self, Insert.insert, ENNReal.mul_rpow_of_ne_top
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
ι : Type u_1
s : Finset ι
f : ι → ℝ≥0∞
hf : ∀ i ∈ s, f i ≠ ∞
r : ℝ
empty :
  ∀ (hf : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → f i ≠ ∞),
    ∏ i ∈ ∅, f i ^ r = HPow.hPow (α := ℝ≥0∞) (∏ i ∈ ∅, f i) r
insert :
  ∀ (i : ι) (s : Finset ι) (hi : i ∉ s)
    (ih : ∀ (hf : ∀ i ∈ s, f i ≠ ∞), ∏ i ∈ s, f i ^ r = HPow.hPow (α := ℝ≥0∞) (∏ i ∈ s, f i) r)
    (hf : ∀ i_1 ∈ Insert.insert i s, f i_1 ≠ ∞),
    ∏ i ∈ Insert.insert i s, f i ^ r = HPow.hPow (α := ℝ≥0∞) (∏ i ∈ Insert.insert i s, f i) r
⊢ ∏ i ∈ s, f i ^ r = HPow.hPow (α := ℝ≥0∞) (∏ i ∈ s, f i) r

Tactic:
classical
  induction s using Finset.induction with
  | empty => simp
  | insert i s hi ih =>
    have h2f : ∀ i ∈ s, f i ≠ ∞ := fun i hi ↦ hf i <| mem_insert_of_mem hi
    rw [prod_insert hi, prod_insert hi, ih h2f, ← mul_rpow_of_ne_top <| hf i <| mem_insert_self ..]
    apply prod_ne_top h2f

Premises used: Finset.mem_insert_self, Insert.insert, ENNReal.mul_rpow_of_ne_top
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
ι : Type u_1
f : ι → ℝ≥0∞
r : ℝ
hr : 0 ≤ r
⊢ ∏ i ∈ ∅, f i ^ r = HPow.hPow (α := ℝ≥0∞) (∏ i ∈ ∅, f i) r

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
ι : Type u_1
f : ι → ℝ≥0∞
r : ℝ
hr : 0 ≤ r
a : ι
s : Finset ι
hi : a ∉ s
ih : ∏ i ∈ s, f i ^ r = HPow.hPow (α := ℝ≥0∞) (∏ i ∈ s, f i) r
insert : f a ^ r * ∏ i ∈ s, f i ^ r = (f a * ∏ i ∈ s, f i) ^ r
insert₁ : f a ^ r * HPow.hPow (α := ℝ≥0∞) (∏ i ∈ s, f i) r = (f a * ∏ i ∈ s, f i) ^ r
⊢ ∏ i ∈ Insert.insert a s, f i ^ r = HPow.hPow (α := ℝ≥0∞) (∏ i ∈ Insert.insert a s, f i) r

Tactic:
simp_rw [prod_insert hi, ih, ← mul_rpow_of_nonneg _ _ hr]

Premises used: Finset.prod_insert, ENNReal.mul_rpow_of_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
ι : Type u_1
s : Finset ι
f : ι → ℝ≥0∞
r : ℝ
hr : 0 ≤ r
empty : ∏ i ∈ ∅, f i ^ r = HPow.hPow (α := ℝ≥0∞) (∏ i ∈ ∅, f i) r
insert :
  ∀ (a : ι) (s : Finset ι) (hi : a ∉ s) (ih : ∏ i ∈ s, f i ^ r = HPow.hPow (α := ℝ≥0∞) (∏ i ∈ s, f i) r),
    ∏ i ∈ Insert.insert a s, f i ^ r = HPow.hPow (α := ℝ≥0∞) (∏ i ∈ Insert.insert a s, f i) r
⊢ ∏ i ∈ s, f i ^ r = HPow.hPow (α := ℝ≥0∞) (∏ i ∈ s, f i) r

Tactic:
induction s using Finset.induction with
  | empty => simp
  | insert _ _ hi ih => simp_rw [prod_insert hi, ih, ← mul_rpow_of_nonneg _ _ hr]

Premises used: ENNReal.mul_rpow_of_nonneg, Insert.insert
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
ι : Type u_1
s : Finset ι
f : ι → ℝ≥0∞
r : ℝ
hr : 0 ≤ r
empty : ∏ i ∈ ∅, f i ^ r = HPow.hPow (α := ℝ≥0∞) (∏ i ∈ ∅, f i) r
insert :
  ∀ (a : ι) (s : Finset ι) (hi : a ∉ s) (ih : ∏ i ∈ s, f i ^ r = HPow.hPow (α := ℝ≥0∞) (∏ i ∈ s, f i) r),
    ∏ i ∈ Insert.insert a s, f i ^ r = HPow.hPow (α := ℝ≥0∞) (∏ i ∈ Insert.insert a s, f i) r
⊢ ∏ i ∈ s, f i ^ r = HPow.hPow (α := ℝ≥0∞) (∏ i ∈ s, f i) r

Tactic:
classical
  induction s using Finset.induction with
  | empty => simp
  | insert _ _ hi ih => simp_rw [prod_insert hi, ih, ← mul_rpow_of_nonneg _ _ hr]

Premises used: ENNReal.mul_rpow_of_nonneg, Insert.insert
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0∞
y : ℝ
inl : HPow.hPow (β := ℝ) x⁻¹ 0 = (HPow.hPow (β := ℝ) x 0)⁻¹
inr : ∀ (hy : y ≠ 0), x⁻¹ ^ y = (x ^ y)⁻¹
⊢ x⁻¹ ^ y = (x ^ y)⁻¹

Tactic:
rcases eq_or_ne y 0 with (rfl | hy)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0∞
⊢ HPow.hPow (β := ℝ) x⁻¹ 0 = (HPow.hPow (β := ℝ) x 0)⁻¹

Tactic:
simp only [rpow_zero, inv_one]

Premises used: inv_one, ENNReal.rpow_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0∞
y : ℝ
hy : y ≠ 0
⊢ y < 0 ∨ 0 < y

Tactic:
replace hy := hy.lt_or_gt
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0∞
y : ℝ
hy : y < 0 ∨ 0 < y
inr : HPow.hPow (α := ℝ≥0∞) 0⁻¹ y = (HPow.hPow (α := ℝ≥0∞) 0 y)⁻¹
inr₁ : ∀ (h0 : x ≠ 0), x⁻¹ ^ y = (x ^ y)⁻¹
⊢ x⁻¹ ^ y = (x ^ y)⁻¹

Tactic:
rcases eq_or_ne x 0 with (rfl | h0)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y : ℝ
hy : y < 0 ∨ 0 < y
inr : y < 0 → HPow.hPow (α := ℝ≥0∞) 0⁻¹ y = (HPow.hPow (α := ℝ≥0∞) 0 y)⁻¹
inr₁ : 0 < y → HPow.hPow (α := ℝ≥0∞) 0⁻¹ y = (HPow.hPow (α := ℝ≥0∞) 0 y)⁻¹
⊢ HPow.hPow (α := ℝ≥0∞) 0⁻¹ y = (HPow.hPow (α := ℝ≥0∞) 0 y)⁻¹

Tactic:
cases hy
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y : ℝ
h : y < 0
⊢ HPow.hPow (α := ℝ≥0∞) 0⁻¹ y = (HPow.hPow (α := ℝ≥0∞) 0 y)⁻¹

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

Tactic:
simp [*]
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0∞
y : ℝ
hy : y < 0 ∨ 0 < y
h0 : x ≠ 0
inr : ∀ (h0 : Ne (α := ℝ≥0∞) ∞ 0), HPow.hPow (α := ℝ≥0∞) ∞⁻¹ y = (HPow.hPow (α := ℝ≥0∞) ∞ y)⁻¹
inr₁ : ∀ (h_top : x ≠ ∞), x⁻¹ ^ y = (x ^ y)⁻¹
⊢ x⁻¹ ^ y = (x ^ y)⁻¹

Tactic:
rcases eq_or_ne x ⊤ with (rfl | h_top)

Premises used: eq_or_ne, Top.top, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y : ℝ
hy : y < 0 ∨ 0 < y
h0 : Ne (α := ℝ≥0∞) ∞ 0
inr : y < 0 → HPow.hPow (α := ℝ≥0∞) ∞⁻¹ y = (HPow.hPow (α := ℝ≥0∞) ∞ y)⁻¹
inr₁ : 0 < y → HPow.hPow (α := ℝ≥0∞) ∞⁻¹ y = (HPow.hPow (α := ℝ≥0∞) ∞ y)⁻¹
⊢ HPow.hPow (α := ℝ≥0∞) ∞⁻¹ y = (HPow.hPow (α := ℝ≥0∞) ∞ y)⁻¹

Tactic:
cases hy
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y : ℝ
h0 : Ne (α := ℝ≥0∞) ∞ 0
h : y < 0
⊢ HPow.hPow (α := ℝ≥0∞) ∞⁻¹ y = (HPow.hPow (α := ℝ≥0∞) ∞ y)⁻¹

Tactic:
simp [*]
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y : ℝ
h0 : Ne (α := ℝ≥0∞) ∞ 0
h : 0 < y
⊢ HPow.hPow (α := ℝ≥0∞) ∞⁻¹ y = (HPow.hPow (α := ℝ≥0∞) ∞ y)⁻¹

Tactic:
simp [*]
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0∞
y : ℝ
hy : y < 0 ∨ 0 < y
h0 : x ≠ 0
h_top : x ≠ ∞
inr : x⁻¹ ^ y * x ^ y = 1
⊢ x⁻¹ ^ y = (x ^ y)⁻¹

Tactic:
apply ENNReal.eq_inv_of_mul_eq_one_left

Premises used: ENNReal.eq_inv_of_mul_eq_one_left
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0∞
y : ℝ
hy : y < 0 ∨ 0 < y
h0 : x ≠ 0
h_top : x ≠ ∞
inr : (x⁻¹ * x) ^ y = 1
inr₁ : HPow.hPow (α := ℝ≥0∞) 1 y = 1
inr₂ inr₃ : Eq (α := ℝ≥0∞) 1 1
⊢ x⁻¹ ^ y * x ^ y = 1

Tactic:
rw [← mul_rpow_of_ne_zero (ENNReal.inv_ne_zero.2 h_top) h0, ENNReal.inv_mul_cancel h0 h_top,
    one_rpow]

Premises used: ENNReal.one_rpow, Iff.mpr, ENNReal.mul_rpow_of_ne_zero, ENNReal.inv_ne_zero, ENNReal.inv_mul_cancel
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x y : ℝ≥0∞
z : ℝ
hz : 0 ≤ z
rw : (x * y⁻¹) ^ z = x ^ z / y ^ z
rw₁ : x ^ z * y⁻¹ ^ z = x ^ z / y ^ z
rw₂ : x ^ z * (y ^ z)⁻¹ = x ^ z / y ^ z
rw₃ rw₄ : x ^ z * (y ^ z)⁻¹ = x ^ z * (y ^ z)⁻¹
⊢ (x / y) ^ z = x ^ z / y ^ z

Tactic:
rw [div_eq_mul_inv, mul_rpow_of_nonneg _ _ hz, inv_rpow, div_eq_mul_inv]

Premises used: ENNReal.inv_rpow, ENNReal.mul_rpow_of_nonneg, div_eq_mul_inv
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
z : ℝ
h : 0 < z
x y : ℝ≥0∞
hxy : x < y
⊢ x ≠ ∞

Tactic:
ne_top_of_lt hxy

Premises used: ne_top_of_lt
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
z : ℝ
h : 0 < z
x y : ℝ≥0∞
hxy : x < y
lift :
  ∀ (x : ℝ≥0) (hxy : (↑x : ℝ≥0∞) < y),
    LT.lt (α := ℝ≥0∞) ((fun (x : ℝ≥0∞) ↦ x ^ z) (↑x : ℝ≥0∞)) ((fun (x : ℝ≥0∞) ↦ x ^ z) y)
⊢ LT.lt (α := ℝ≥0∞) ((fun (x : ℝ≥0∞) ↦ x ^ z) x) ((fun (x : ℝ≥0∞) ↦ x ^ z) y)

Tactic:
lift x to ℝ≥0 using ne_top_of_lt hxy

Premises used: ne_top_of_lt
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
z : ℝ
h : 0 < z
y : ℝ≥0∞
x : ℝ≥0
hxy : (↑x : ℝ≥0∞) < y
inl : ∀ (hxy : (↑x : ℝ≥0∞) < ∞), LT.lt (α := ℝ≥0∞) ((fun (x : ℝ≥0∞) ↦ x ^ z) (↑x : ℝ≥0∞)) ((fun (x : ℝ≥0∞) ↦ x ^ z) ∞)
inr : ∀ (hy : y ≠ ∞), LT.lt (α := ℝ≥0∞) ((fun (x : ℝ≥0∞) ↦ x ^ z) (↑x : ℝ≥0∞)) ((fun (x : ℝ≥0∞) ↦ x ^ z) y)
⊢ LT.lt (α := ℝ≥0∞) ((fun (x : ℝ≥0∞) ↦ x ^ z) (↑x : ℝ≥0∞)) ((fun (x : ℝ≥0∞) ↦ x ^ z) y)

Tactic:
rcases eq_or_ne y ∞ with (rfl | hy)

Premises used: eq_or_ne, Top.top, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
z : ℝ
h : 0 < z
x : ℝ≥0
hxy : (↑x : ℝ≥0∞) < ∞
⊢ LT.lt (α := ℝ≥0∞) ((fun (x : ℝ≥0∞) ↦ x ^ z) (↑x : ℝ≥0∞)) ((fun (x : ℝ≥0∞) ↦ x ^ z) ∞)

Tactic:
simp only [top_rpow_of_pos h, ← coe_rpow_of_nonneg _ h.le, coe_lt_top]

Premises used: ENNReal.coe_rpow_of_nonneg, LT.lt.le, ENNReal.top_rpow_of_pos, ENNReal.coe_lt_top
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
z : ℝ
h : 0 < z
y : ℝ≥0∞
x : ℝ≥0
hxy : (↑x : ℝ≥0∞) < y
hy : y ≠ ∞
⊢ y ≠ ∞

Tactic:
hy
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
z : ℝ
h : 0 < z
y : ℝ≥0∞
x : ℝ≥0
hxy : (↑x : ℝ≥0∞) < y
hy : y ≠ ∞
inr :
  ∀ (y : ℝ≥0) (hxy : (↑x : ℝ≥0∞) < (↑y : ℝ≥0∞)),
    LT.lt (α := ℝ≥0∞) ((fun (x : ℝ≥0∞) ↦ x ^ z) (↑x : ℝ≥0∞)) ((fun (x : ℝ≥0∞) ↦ x ^ z) (↑y : ℝ≥0∞))
⊢ LT.lt (α := ℝ≥0∞) ((fun (x : ℝ≥0∞) ↦ x ^ z) (↑x : ℝ≥0∞)) ((fun (x : ℝ≥0∞) ↦ x ^ z) y)

Tactic:
lift y to ℝ≥0 using hy
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
z : ℝ
h : 0 < z
x y : ℝ≥0
hxy : (↑x : ℝ≥0∞) < (↑y : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) ((fun (x : ℝ≥0∞) ↦ x ^ z) (↑x : ℝ≥0∞)) ((fun (x : ℝ≥0∞) ↦ x ^ z) (↑y : ℝ≥0∞))

Tactic:
simp only [← coe_rpow_of_nonneg _ h.le, NNReal.rpow_lt_rpow (coe_lt_coe.1 hxy) h, coe_lt_coe]

Premises used: NNReal.rpow_lt_rpow, ENNReal.coe_rpow_of_nonneg, ENNReal.coe_lt_coe, LT.lt.le, Iff.mp
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
z : ℝ
h : 0 ≤ z
h0 : 0 = z
⊢ Monotone (β := ℝ≥0∞) fun (x : ℝ≥0∞) ↦ HPow.hPow (β := ℝ) x 0

Tactic:
simp only [rpow_zero, monotone_const]

Premises used: monotone_const, ENNReal.rpow_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y : ℝ
hy : 0 < y
x : ℝ≥0∞
rw : x ^ (1 / y * y) = x
rw₁ : HPow.hPow (β := ℝ) x 1 = x
rw₂ rw₃ : x = x
⊢ (x ^ (1 / y)) ^ y = x

Tactic:
rw [← rpow_mul, one_div_mul_cancel hy.ne.symm, rpow_one]

Premises used: ENNReal.rpow_mul, ENNReal.rpow_one, Ne.symm, one_div_mul_cancel, LT.lt.ne
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y : ℝ
hy : 0 < y
simp :
  (StrictMono.orderIsoOfRightInverse (fun (x : ℝ≥0∞) ↦ x ^ y) ⋯ (fun (x : ℝ≥0∞) ↦ x ^ (1 / y)) ⋯).symm =
    StrictMono.orderIsoOfRightInverse (fun (x : ℝ≥0∞) ↦ x ^ (1 / y)) ⋯ (fun (x : ℝ≥0∞) ↦ x ^ y) ⋯
⊢ (orderIsoRpow y hy).symm = orderIsoRpow (1 / y) ⋯

Tactic:
simp only [orderIsoRpow, one_div_one_div]

Premises used: ENNReal.orderIsoRpow, one_div_one_div
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y : ℝ
hy : 0 < y
⊢ (StrictMono.orderIsoOfRightInverse (fun (x : ℝ≥0∞) ↦ x ^ y) ⋯ (fun (x : ℝ≥0∞) ↦ x ^ (1 / y)) ⋯).symm =
    StrictMono.orderIsoOfRightInverse (fun (x : ℝ≥0∞) ↦ x ^ (1 / y)) ⋯ (fun (x : ℝ≥0∞) ↦ x ^ y) ⋯

Tactic:
rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x y : ℝ≥0∞
z : ℝ
h₁ : x ≤ y
h₂ : 0 ≤ z
⊢ x ^ z ≤ y ^ z

Tactic:
monotone_rpow_of_nonneg h₂ h₁

Premises used: ENNReal.monotone_rpow_of_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x y : ℝ≥0∞
z : ℝ
h₁ : x < y
h₂ : 0 < z
⊢ x ^ z < y ^ z

Tactic:
strictMono_rpow_of_pos h₂ h₁

Premises used: ENNReal.strictMono_rpow_of_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x y : ℝ≥0∞
z : ℝ
hz : 0 < z
⊢ x ^ z ≤ y ^ z ↔ x ≤ y

Tactic:
(strictMono_rpow_of_pos hz).le_iff_le

Premises used: ENNReal.strictMono_rpow_of_pos, StrictMono.le_iff_le
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x y : ℝ≥0∞
z : ℝ
hz : 0 < z
⊢ x ^ z < y ^ z ↔ x < y

Tactic:
(strictMono_rpow_of_pos hz).lt_iff_lt

Premises used: StrictMono.lt_iff_lt, ENNReal.strictMono_rpow_of_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x y : ℝ≥0∞
p : ℝ
hp : 0 ≤ p
inl : ∀ (hxy : x ≤ y), max x y ^ p = max (x ^ p) (y ^ p)
inr : ∀ (hxy : y ≤ x), max x y ^ p = max (x ^ p) (y ^ p)
⊢ max x y ^ p = max (x ^ p) (y ^ p)

Tactic:
rcases le_total x y with hxy | hxy

Premises used: le_total
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x y : ℝ≥0∞
p : ℝ
hp : 0 ≤ p
hxy : x ≤ y
inl : y ^ p = max (x ^ p) (y ^ p)
inl₁ inl₂ : y ^ p = y ^ p
⊢ max x y ^ p = max (x ^ p) (y ^ p)

Tactic:
rw [max_eq_right hxy, max_eq_right (rpow_le_rpow hxy hp)]

Premises used: max_eq_right, ENNReal.rpow_le_rpow
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x y : ℝ≥0∞
p : ℝ
hp : 0 ≤ p
hxy : y ≤ x
inr : x ^ p = max (x ^ p) (y ^ p)
inr₁ inr₂ : x ^ p = x ^ p
⊢ max x y ^ p = max (x ^ p) (y ^ p)

Tactic:
rw [max_eq_left hxy, max_eq_left (rpow_le_rpow hxy hp)]

Premises used: max_eq_left, ENNReal.rpow_le_rpow
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x y : ℝ≥0∞
z : ℝ
hz : 0 < z
nth_rw : HPow.hPow (β := ℝ) x 1 ≤ y ^ z⁻¹ ↔ x ^ z ≤ y
⊢ x ≤ y ^ z⁻¹ ↔ x ^ z ≤ y

Tactic:
nth_rw 1 [← rpow_one x]

Premises used: ENNReal.rpow_one
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x y : ℝ≥0∞
z : ℝ
hz : 0 < z
nth_rw : x ^ (z * z⁻¹) ≤ y ^ z⁻¹ ↔ x ^ z ≤ y
⊢ HPow.hPow (β := ℝ) x 1 ≤ y ^ z⁻¹ ↔ x ^ z ≤ y

Tactic:
nth_rw 1 [← @mul_inv_cancel₀ _ _ z hz.ne']

Premises used: mul_inv_cancel₀, LT.lt.ne'
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x y : ℝ≥0∞
z : ℝ
hz : 0 < z
⊢ 0 < z⁻¹

Tactic:
simp [hz]
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x y : ℝ≥0∞
z : ℝ
hz : 0 < z
rw : (x ^ z) ^ z⁻¹ ≤ y ^ z⁻¹ ↔ x ^ z ≤ y
rw₁ rw₂ : x ^ z ≤ y ↔ x ^ z ≤ y
⊢ x ^ (z * z⁻¹) ≤ y ^ z⁻¹ ↔ x ^ z ≤ y

Tactic:
rw [rpow_mul, @rpow_le_rpow_iff _ _ z⁻¹ (by simp [hz])]

Premises used: ENNReal.rpow_mul, ENNReal.rpow_le_rpow_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, ENNReal.le_rpow_inv_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x y : ℝ≥0∞
z : ℝ
hz : 0 < z
nth_rw : HPow.hPow (β := ℝ) x 1 < y ^ z⁻¹ ↔ x ^ z < y
⊢ x < y ^ z⁻¹ ↔ x ^ z < y

Tactic:
nth_rw 1 [← rpow_one x]

Premises used: ENNReal.rpow_one
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x y : ℝ≥0∞
z : ℝ
hz : 0 < z
nth_rw : x ^ (z * z⁻¹) < y ^ z⁻¹ ↔ x ^ z < y
⊢ HPow.hPow (β := ℝ) x 1 < y ^ z⁻¹ ↔ x ^ z < y

Tactic:
nth_rw 1 [← @mul_inv_cancel₀ _ _ z (ne_of_lt hz).symm]

Premises used: mul_inv_cancel₀, Ne.symm, ne_of_lt
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x y : ℝ≥0∞
z : ℝ
hz : 0 < z
rw : (x ^ z) ^ z⁻¹ < y ^ z⁻¹ ↔ x ^ z < y
rw₁ rw₂ : x ^ z < y ↔ x ^ z < y
⊢ x ^ (z * z⁻¹) < y ^ z⁻¹ ↔ x ^ z < y

Tactic:
rw [rpow_mul, @rpow_lt_rpow_iff _ _ z⁻¹ (by simp [hz])]

Premises used: ENNReal.rpow_mul, ENNReal.rpow_lt_rpow_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x y : ℝ≥0∞
z : ℝ
hz : 0 < z
nth_rw : x ^ z⁻¹ ≤ HPow.hPow (β := ℝ) y 1 ↔ x ≤ y ^ z
⊢ x ^ z⁻¹ ≤ y ↔ x ≤ y ^ z

Tactic:
nth_rw 1 [← ENNReal.rpow_one y]

Premises used: ENNReal.rpow_one
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x y : ℝ≥0∞
z : ℝ
hz : 0 < z
nth_rw : x ^ z⁻¹ ≤ y ^ (z * z⁻¹) ↔ x ≤ y ^ z
⊢ x ^ z⁻¹ ≤ HPow.hPow (β := ℝ) y 1 ↔ x ≤ y ^ z

Tactic:
nth_rw 1 [← @mul_inv_cancel₀ _ _ z hz.ne.symm]

Premises used: mul_inv_cancel₀, Ne.symm, LT.lt.ne
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x y : ℝ≥0∞
z : ℝ
hz : 0 < z
rw : x ^ z⁻¹ ≤ (y ^ z) ^ z⁻¹ ↔ x ≤ y ^ z
rw₁ rw₂ : x ≤ y ^ z ↔ x ≤ y ^ z
⊢ x ^ z⁻¹ ≤ y ^ (z * z⁻¹) ↔ x ≤ y ^ z

Tactic:
rw [ENNReal.rpow_mul, ENNReal.rpow_le_rpow_iff (inv_pos.2 hz)]

Premises used: Iff.mpr, ENNReal.rpow_mul, inv_pos, ENNReal.rpow_le_rpow_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0∞
y z : ℝ
hx : 1 < x
hx' : x ≠ ∞
hyz : y < z
⊢ x ≠ ∞

Tactic:
hx'
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0∞
y z : ℝ
hx : 1 < x
hx' : x ≠ ∞
hyz : y < z
lift : ∀ (x : ℝ≥0) (hx : 1 < (↑x : ℝ≥0∞)), (↑x : ℝ≥0∞) ^ y < (↑x : ℝ≥0∞) ^ z
⊢ x ^ y < x ^ z

Tactic:
lift x to ℝ≥0 using hx'
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y z : ℝ
hyz : y < z
x : ℝ≥0
hx : 1 < (↑x : ℝ≥0∞)
⊢ 1 < x

Tactic:
rw [one_lt_coe_iff] at hx

Premises used: ENNReal.one_lt_coe_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y z : ℝ
hyz : y < z
x : ℝ≥0
hx : 1 < x
⊢ (↑x : ℝ≥0∞) ^ y < (↑x : ℝ≥0∞) ^ z

Tactic:
simp [← coe_rpow_of_ne_zero (lt_trans zero_lt_one hx).ne',
    NNReal.rpow_lt_rpow_of_exponent_lt hx hyz]

Premises used: lt_trans, NNReal.rpow_lt_rpow_of_exponent_lt, ENNReal.coe_rpow_of_ne_zero, LT.lt.ne', zero_lt_one
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0∞
y z : ℝ
hx : 1 ≤ x
hyz : y ≤ z
top : ∀ (hx : LE.le (α := ℝ≥0∞) 1 ∞), HPow.hPow (α := ℝ≥0∞) ∞ y ≤ HPow.hPow (α := ℝ≥0∞) ∞ z
coe : ∀ (x : ℝ≥0) (hx : 1 ≤ (↑x : ℝ≥0∞)), (↑x : ℝ≥0∞) ^ y ≤ (↑x : ℝ≥0∞) ^ z
⊢ x ^ y ≤ x ^ z

Tactic:
cases x
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y z : ℝ
hyz : y ≤ z
hx : LE.le (α := ℝ≥0∞) 1 ∞
top : ∀ (Hy : y < 0), HPow.hPow (α := ℝ≥0∞) ∞ y ≤ HPow.hPow (α := ℝ≥0∞) ∞ z
top₁ : ∀ (Hy : y = 0), HPow.hPow (α := ℝ≥0∞) ∞ y ≤ HPow.hPow (α := ℝ≥0∞) ∞ z
top₂ : ∀ (Hy : 0 < y), HPow.hPow (α := ℝ≥0∞) ∞ y ≤ HPow.hPow (α := ℝ≥0∞) ∞ z
⊢ HPow.hPow (α := ℝ≥0∞) ∞ y ≤ HPow.hPow (α := ℝ≥0∞) ∞ z

Tactic:
rcases lt_trichotomy y 0 with (Hy | Hy | Hy)

Premises used: OfNat.ofNat, lt_trichotomy
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y z : ℝ
hyz : y ≤ z
hx : LE.le (α := ℝ≥0∞) 1 ∞
Hy : y < 0
top : ∀ (Hz : z < 0), HPow.hPow (α := ℝ≥0∞) ∞ y ≤ HPow.hPow (α := ℝ≥0∞) ∞ z
top₁ : ∀ (Hz : z = 0), HPow.hPow (α := ℝ≥0∞) ∞ y ≤ HPow.hPow (α := ℝ≥0∞) ∞ z
top₂ : ∀ (Hz : 0 < z), HPow.hPow (α := ℝ≥0∞) ∞ y ≤ HPow.hPow (α := ℝ≥0∞) ∞ z
⊢ HPow.hPow (α := ℝ≥0∞) ∞ y ≤ HPow.hPow (α := ℝ≥0∞) ∞ z

Tactic:
rcases lt_trichotomy z 0 with (Hz | Hz | Hz)

Premises used: OfNat.ofNat, lt_trichotomy
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y z : ℝ
hyz : y ≤ z
hx : LE.le (α := ℝ≥0∞) 1 ∞
Hy : y = 0
top : ∀ (Hz : z < 0), HPow.hPow (α := ℝ≥0∞) ∞ y ≤ HPow.hPow (α := ℝ≥0∞) ∞ z
top₁ : ∀ (Hz : z = 0), HPow.hPow (α := ℝ≥0∞) ∞ y ≤ HPow.hPow (α := ℝ≥0∞) ∞ z
top₂ : ∀ (Hz : 0 < z), HPow.hPow (α := ℝ≥0∞) ∞ y ≤ HPow.hPow (α := ℝ≥0∞) ∞ z
⊢ HPow.hPow (α := ℝ≥0∞) ∞ y ≤ HPow.hPow (α := ℝ≥0∞) ∞ z

Tactic:
rcases lt_trichotomy z 0 with (Hz | Hz | Hz)

Premises used: OfNat.ofNat, lt_trichotomy
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y z : ℝ
hyz : y ≤ z
hx : LE.le (α := ℝ≥0∞) 1 ∞
Hy : 0 < y
top : ∀ (Hz : z < 0), HPow.hPow (α := ℝ≥0∞) ∞ y ≤ HPow.hPow (α := ℝ≥0∞) ∞ z
top₁ : ∀ (Hz : z = 0), HPow.hPow (α := ℝ≥0∞) ∞ y ≤ HPow.hPow (α := ℝ≥0∞) ∞ z
top₂ : ∀ (Hz : 0 < z), HPow.hPow (α := ℝ≥0∞) ∞ y ≤ HPow.hPow (α := ℝ≥0∞) ∞ z
⊢ HPow.hPow (α := ℝ≥0∞) ∞ y ≤ HPow.hPow (α := ℝ≥0∞) ∞ z

Tactic:
rcases lt_trichotomy z 0 with (Hz | Hz | Hz)

Premises used: OfNat.ofNat, lt_trichotomy
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y z : ℝ
hyz : y ≤ z
hx : LE.le (α := ℝ≥0∞) 1 ∞
Hy : y < 0
Hz : z < 0
⊢ HPow.hPow (α := ℝ≥0∞) ∞ y ≤ HPow.hPow (α := ℝ≥0∞) ∞ z

Tactic:
simp [Hy, Hz, top_rpow_of_neg, top_rpow_of_pos]

Premises used: ENNReal.top_rpow_of_pos, ENNReal.top_rpow_of_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y z : ℝ
hyz : y ≤ z
hx : LE.le (α := ℝ≥0∞) 1 ∞
Hy : y < 0
Hz : z = 0
⊢ HPow.hPow (α := ℝ≥0∞) ∞ y ≤ HPow.hPow (α := ℝ≥0∞) ∞ z

Tactic:
simp [Hy, Hz, top_rpow_of_neg, top_rpow_of_pos]

Premises used: ENNReal.top_rpow_of_pos, ENNReal.top_rpow_of_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y z : ℝ
hyz : y ≤ z
hx : LE.le (α := ℝ≥0∞) 1 ∞
Hy : y < 0
Hz : 0 < z
⊢ HPow.hPow (α := ℝ≥0∞) ∞ y ≤ HPow.hPow (α := ℝ≥0∞) ∞ z

Tactic:
simp [Hy, Hz, top_rpow_of_neg, top_rpow_of_pos]

Premises used: ENNReal.top_rpow_of_pos, ENNReal.top_rpow_of_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y z : ℝ
hyz : y ≤ z
hx : LE.le (α := ℝ≥0∞) 1 ∞
Hy : y = 0
Hz : z < 0
top : False
⊢ HPow.hPow (α := ℝ≥0∞) ∞ y ≤ HPow.hPow (α := ℝ≥0∞) ∞ z

Tactic:
simp [Hy, Hz, top_rpow_of_neg, top_rpow_of_pos]

Premises used: ENNReal.top_rpow_of_pos, ENNReal.top_rpow_of_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y z : ℝ
hyz : y ≤ z
hx : LE.le (α := ℝ≥0∞) 1 ∞
Hy : y = 0
Hz : z = 0
⊢ HPow.hPow (α := ℝ≥0∞) ∞ y ≤ HPow.hPow (α := ℝ≥0∞) ∞ z

Tactic:
simp [Hy, Hz, top_rpow_of_neg, top_rpow_of_pos]

Premises used: ENNReal.top_rpow_of_pos, ENNReal.top_rpow_of_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y z : ℝ
hyz : y ≤ z
hx : LE.le (α := ℝ≥0∞) 1 ∞
Hy : y = 0
Hz : 0 < z
⊢ HPow.hPow (α := ℝ≥0∞) ∞ y ≤ HPow.hPow (α := ℝ≥0∞) ∞ z

Tactic:
simp [Hy, Hz, top_rpow_of_neg, top_rpow_of_pos]

Premises used: ENNReal.top_rpow_of_pos, ENNReal.top_rpow_of_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y z : ℝ
hyz : y ≤ z
hx : LE.le (α := ℝ≥0∞) 1 ∞
Hy : 0 < y
Hz : z < 0
top : False
⊢ HPow.hPow (α := ℝ≥0∞) ∞ y ≤ HPow.hPow (α := ℝ≥0∞) ∞ z

Tactic:
simp [Hy, Hz, top_rpow_of_neg, top_rpow_of_pos]

Premises used: ENNReal.top_rpow_of_pos, ENNReal.top_rpow_of_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y z : ℝ
hyz : y ≤ z
hx : LE.le (α := ℝ≥0∞) 1 ∞
Hy : 0 < y
Hz : z = 0
top : False
⊢ HPow.hPow (α := ℝ≥0∞) ∞ y ≤ HPow.hPow (α := ℝ≥0∞) ∞ z

Tactic:
simp [Hy, Hz, top_rpow_of_neg, top_rpow_of_pos]

Premises used: ENNReal.top_rpow_of_pos, ENNReal.top_rpow_of_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
y z : ℝ
hyz : y ≤ z
hx : LE.le (α := ℝ≥0∞) 1 ∞
Hy : 0 < y
Hz : 0 < z
⊢ HPow.hPow (α := ℝ≥0∞) ∞ y ≤ HPow.hPow (α := ℝ≥0∞) ∞ z

Tactic:
simp [Hy, Hz, top_rpow_of_neg, top_rpow_of_pos]

Premises used: ENNReal.top_rpow_of_pos, ENNReal.top_rpow_of_neg