awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (hypothesis)
Goal:
r : ℝ
l : List ℝ≥0
this : (↑(List.prod (List.map (fun (x : ℝ≥0) ↦ x ^ r) l)) : ℝ) = (↑(l.prod ^ r) : ℝ)
⊢ List.prod (List.map (fun (x : ℝ) ↦ x ^ r) (List.map toReal l)) = (List.map toReal l).prod ^ r
have this₁ : (List.map toReal (List.map (fun (x : ℝ≥0) ↦ x ^ r) l)).prod = (List.map toReal l).prod ^ r
Tactic: push_cast at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
r : ℝ
l : List ℝ≥0
this : (List.map toReal (List.map (fun (x : ℝ≥0) ↦ x ^ r) l)).prod = (List.map toReal l).prod ^ r
⊢ List.prod (List.map (fun (x : ℝ) ↦ x ^ r) (List.map toReal l)) = (List.map toReal l).prod ^ r
have 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
Tactic: rw [List.map_map] at this ⊢
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
ι : Type u_1
l : List ι
f : ι → ℝ
hl : ∀ i ∈ l, 0 ≤ f i
r : ℝ
⊢ List.prod (List.map (fun (x : ι) ↦ f x ^ r) l) = (List.map f l).prod ^ r
have rw : Eq (α := ℝ) (List.prod (List.map (fun (x : ι) ↦ f x ^ r) l)) (List.prod (List.map ((fun (x : ℝ) ↦ x ^ r) ∘ f) l))
Tactic: rw [← Real.list_prod_map_rpow (l.map f) _ r, List.map_map]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
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))
⊢ List.prod (List.map (fun (x : ι) ↦ f x ^ r) l) = (List.map f l).prod ^ r
have rw₁ : ∀ x ∈ List.map f l, 0 ≤ x
Tactic: rw [← Real.list_prod_map_rpow (l.map f) _ r, List.map_map]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
ι : Type u_1
s : Multiset ι
f : ι → ℝ
hs : ∀ i ∈ s, 0 ≤ f i
r : ℝ
⊢ Multiset.prod (Multiset.map (fun (x : ι) ↦ f x ^ r) s) = (Multiset.map f s).prod ^ r
have 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
Tactic: obtain ⟨l⟩ := s
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x y : ℝ≥0
z : ℝ
hz : 0 < z
⊢ x ≤ y ^ z⁻¹ ↔ x ^ z ≤ y
have rw : x ^ z ≤ (y ^ z⁻¹) ^ z ↔ x ^ z ≤ y
Tactic: rw [← rpow_le_rpow_iff hz, ← one_div, rpow_self_rpow_inv hz.ne']
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x y : ℝ≥0
z : ℝ
hz : 0 < z
rw : x ^ z ≤ (y ^ z⁻¹) ^ z ↔ x ^ z ≤ y
⊢ x ≤ y ^ z⁻¹ ↔ x ^ z ≤ y
have rw₁ : x ^ z ≤ (y ^ (1 / z)) ^ z ↔ x ^ z ≤ y
Tactic: rw [← rpow_le_rpow_iff hz, ← one_div, rpow_self_rpow_inv hz.ne']
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
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
⊢ x ≤ y ^ z⁻¹ ↔ x ^ z ≤ y
have rw₂ : x ^ z ≤ y ↔ x ^ z ≤ y
Tactic: rw [← rpow_le_rpow_iff hz, ← one_div, rpow_self_rpow_inv hz.ne']
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x y : ℝ≥0
z : ℝ
hz : 0 < z
⊢ x ^ z⁻¹ ≤ y ↔ x ≤ y ^ z
have rw : (x ^ z⁻¹) ^ z ≤ y ^ z ↔ x ≤ y ^ z
Tactic: rw [← rpow_le_rpow_iff hz, ← one_div, rpow_self_rpow_inv hz.ne']
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x y : ℝ≥0
z : ℝ
hz : 0 < z
rw : (x ^ z⁻¹) ^ z ≤ y ^ z ↔ x ≤ y ^ z
⊢ x ^ z⁻¹ ≤ y ↔ x ≤ y ^ z
have rw₁ : (x ^ (1 / z)) ^ z ≤ y ^ z ↔ x ≤ y ^ z
Tactic: rw [← rpow_le_rpow_iff hz, ← one_div, rpow_self_rpow_inv hz.ne']
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
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
⊢ x ^ z⁻¹ ≤ y ↔ x ≤ y ^ z
have rw₂ : x ≤ y ^ z ↔ x ≤ y ^ z
Tactic: rw [← rpow_le_rpow_iff hz, ← one_div, rpow_self_rpow_inv hz.ne']
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
p_1 : ℝ
x : ℝ≥0
hx_pos : 0 < x
p : ℝ
hp_pos : 0 < p
⊢ 0 < x ^ p
have rw : HPow.hPow (α := ℝ≥0) 0 p < x ^ p
Tactic: rw [← zero_rpow hp_pos.ne']
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (hypothesis)
Goal:
p : ℝ
x : ℝ≥0
hx_pos : 0 < x
⊢ 0 < x ^ p
have rpow_pos_of_nonneg : ∀ {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
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
p : ℝ
x : ℝ≥0
hx_pos : 0 < x
rpow_pos_of_nonneg : ∀ {p : ℝ}, 0 < p → 0 < x ^ p
⊢ 0 < x ^ p
have inl : ∀ (hp_pos : 0 < p), 0 < x ^ p
Tactic: rcases lt_trichotomy (0 : ℝ) p with (hp_pos | rfl | hp_neg)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
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
⊢ 0 < x ^ p
have inr : 0 < HPow.hPow (β := ℝ) x 0
Tactic: rcases lt_trichotomy (0 : ℝ) p with (hp_pos | rfl | hp_neg)
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
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
⊢ 0 < x ^ p
have inr₁ : ∀ (hp_neg : p < 0), 0 < x ^ p
Tactic: rcases lt_trichotomy (0 : ℝ) p with (hp_pos | rfl | hp_neg)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
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
have inr : 0 < x ^ (-p)
Tactic: rw [← neg_neg p, rpow_neg, inv_pos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x : ℝ≥0
z : ℝ
hx : x ≤ 1
h_one_le : 1 ≤ z
⊢ x ^ z ≤ x
have inl : ∀ (hx : LE.le (α := ℝ≥0) ⊥ 1), HPow.hPow (α := ℝ≥0) ⊥ z ≤ ⊥
Tactic: rcases eq_bot_or_bot_lt x with (rfl | (h : 0 < x))
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x : ℝ≥0
z : ℝ
hx : x ≤ 1
h_one_le : 1 ≤ z
inl : ∀ (hx : LE.le (α := ℝ≥0) ⊥ 1), HPow.hPow (α := ℝ≥0) ⊥ z ≤ ⊥
⊢ x ^ z ≤ x
have inr : ∀ (h : 0 < x), x ^ z ≤ x
Tactic: rcases eq_bot_or_bot_lt x with (rfl | (h : 0 < x))
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
z : ℝ
h_one_le : 1 ≤ z
hx : LE.le (α := ℝ≥0) ⊥ 1
⊢ z ≠ 0
have linarith : z = 0 → -1 + (1 - z) + (z - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (hypothesis)
Goal:
z : ℝ
h_one_le : 1 ≤ z
hx : LE.le (α := ℝ≥0) ⊥ 1
⊢ HPow.hPow (α := ℝ≥0) ⊥ z ≤ ⊥
have this : z ≠ 0
Tactic: have : z ≠ 0 := by linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x : ℝ≥0
z : ℝ
hx : x ≤ 1
h_one_le : 1 ≤ z
h : 0 < x
⊢ x ^ z ≤ x
have inr : x ^ z ≤ HPow.hPow (β := ℝ) x 1
Tactic: nth_rw 2 [← NNReal.rpow_one x]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x : ℝ
hx : x ≠ 0
y : ℝ≥0
simp_rw simp_rw₁ : (y ^ x⁻¹) ^ x = y
⊢ (fun (y : ℝ≥0) ↦ y ^ x) (y ^ x⁻¹) = y
have simp_rw₂ : y ^ (x⁻¹ * x) = y
Tactic: simp_rw [← rpow_mul, inv_mul_cancel₀ hx, rpow_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x : ℝ
hx : x ≠ 0
y : ℝ≥0
simp_rw simp_rw₁ : (y ^ x⁻¹) ^ x = y
simp_rw₂ : y ^ (x⁻¹ * x) = y
⊢ (fun (y : ℝ≥0) ↦ y ^ x) (y ^ x⁻¹) = y
have simp_rw₃ : HPow.hPow (β := ℝ) y 1 = y
Tactic: simp_rw [← rpow_mul, inv_mul_cancel₀ hx, rpow_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (hypothesis)
Goal:
x : ℝ≥0
y z : ℝ
hx₀ : x ≠ 0
hx₁ : x ≠ 1
⊢ x ^ y = x ^ z ↔ y = z
have hx₂ : 0 < x
Tactic: rw [← pos_iff_ne_zero] at hx₀
Cleared hypotheses: hx₀, hx₁
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x : ℝ≥0
y z : ℝ
hx₀ : 0 < x
hx₁ : x ≠ 1
⊢ x ^ y = x ^ z ↔ y = z
have rify : ∀ (hx₀ : 0 < (↑x : ℝ)) (hx₁ : (↑x : ℝ) ≠ 1), (↑x : ℝ) ^ y = (↑x : ℝ) ^ z ↔ y = z
Tactic: rify at *
Cleared hypotheses: hx₀, hx₁
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x : ℝ≥0
y z : ℝ
⊢ x ^ y = x ^ z ↔ y = z ∨ x = 1 ∨ x = 0 ∧ (y = 0 ↔ z = 0)
have 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)
Tactic: obtain rfl | hx₀ := eq_or_ne x 0
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
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)
⊢ x ^ y = x ^ z ↔ y = z ∨ x = 1 ∨ x = 0 ∧ (y = 0 ↔ z = 0)
have inr : ∀ (hx₀ : x ≠ 0), x ^ y = x ^ z ↔ y = z ∨ x = 1 ∨ x = 0 ∧ (y = 0 ↔ z = 0)
Tactic: obtain rfl | hx₀ := eq_or_ne x 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y z : ℝ
⊢ HPow.hPow (α := ℝ≥0) 0 y = HPow.hPow (α := ℝ≥0) 0 z ↔ y = z ∨ Eq (α := ℝ≥0) 0 1 ∨ Eq (α := ℝ≥0) 0 0 ∧ (y = 0 ↔ z = 0)
have 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)
Tactic: obtain rfl | hz := eq_or_ne z 0
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
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)
⊢ HPow.hPow (α := ℝ≥0) 0 y = HPow.hPow (α := ℝ≥0) 0 z ↔ y = z ∨ Eq (α := ℝ≥0) 0 1 ∨ Eq (α := ℝ≥0) 0 0 ∧ (y = 0 ↔ z = 0)
have 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)
Tactic: obtain rfl | hz := eq_or_ne z 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x : ℝ≥0
y z : ℝ
hx₀ : x ≠ 0
⊢ x ^ y = x ^ z ↔ y = z ∨ x = 1 ∨ x = 0 ∧ (y = 0 ↔ z = 0)
have 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)
Tactic: obtain rfl | hx₁ := eq_or_ne x 1
Cleared hypotheses: x, hx₀
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
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)
⊢ x ^ y = x ^ z ↔ y = z ∨ x = 1 ∨ x = 0 ∧ (y = 0 ↔ z = 0)
have inr₁ : ∀ (hx₁ : x ≠ 1), x ^ y = x ^ z ↔ y = z ∨ x = 1 ∨ x = 0 ∧ (y = 0 ↔ z = 0)
Tactic: obtain rfl | hx₁ := eq_or_ne x 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x y : ℝ≥0
z : ℝ
hz : z ≠ 0
⊢ x = y ^ z⁻¹ ↔ x ^ z = y
have rw : x ^ z = (y ^ z⁻¹) ^ z ↔ x ^ z = y
Tactic: rw [← rpow_eq_rpow_iff hz, ← one_div, rpow_self_rpow_inv hz]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x y : ℝ≥0
z : ℝ
hz : z ≠ 0
rw : x ^ z = (y ^ z⁻¹) ^ z ↔ x ^ z = y
⊢ x = y ^ z⁻¹ ↔ x ^ z = y
have rw₁ : x ^ z = (y ^ (1 / z)) ^ z ↔ x ^ z = y
Tactic: rw [← rpow_eq_rpow_iff hz, ← one_div, rpow_self_rpow_inv hz]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
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
⊢ x = y ^ z⁻¹ ↔ x ^ z = y
have rw₂ : x ^ z = y ↔ x ^ z = y
Tactic: rw [← rpow_eq_rpow_iff hz, ← one_div, rpow_self_rpow_inv hz]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x y : ℝ≥0
z : ℝ
hz : z ≠ 0
⊢ x ^ z⁻¹ = y ↔ x = y ^ z
have rw : (x ^ z⁻¹) ^ z = y ^ z ↔ x = y ^ z
Tactic: rw [← rpow_eq_rpow_iff hz, ← one_div, rpow_self_rpow_inv hz]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x y : ℝ≥0
z : ℝ
hz : z ≠ 0
rw : (x ^ z⁻¹) ^ z = y ^ z ↔ x = y ^ z
⊢ x ^ z⁻¹ = y ↔ x = y ^ z
have rw₁ : (x ^ (1 / z)) ^ z = y ^ z ↔ x = y ^ z
Tactic: rw [← rpow_eq_rpow_iff hz, ← one_div, rpow_self_rpow_inv hz]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
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
⊢ x ^ z⁻¹ = y ↔ x = y ^ z
have rw₂ : x = y ^ z ↔ x = y ^ z
Tactic: rw [← rpow_eq_rpow_iff hz, ← one_div, rpow_self_rpow_inv hz]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y : ℝ
hy : y ≠ 0
x : ℝ≥0
⊢ (x ^ y) ^ y⁻¹ = x
have rw : x ^ (y * y⁻¹) = x
Tactic: rw [← rpow_mul, mul_inv_cancel₀ hy, rpow_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y : ℝ
hy : y ≠ 0
x : ℝ≥0
rw : x ^ (y * y⁻¹) = x
⊢ (x ^ y) ^ y⁻¹ = x
have rw₁ : HPow.hPow (β := ℝ) x 1 = x
Tactic: rw [← rpow_mul, mul_inv_cancel₀ hy, rpow_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y : ℝ
hy : y ≠ 0
x : ℝ≥0
rw : x ^ (y * y⁻¹) = x
rw₁ : HPow.hPow (β := ℝ) x 1 = x
⊢ (x ^ y) ^ y⁻¹ = x
have rw₂ : x = x
Tactic: rw [← rpow_mul, mul_inv_cancel₀ hy, rpow_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y : ℝ
hy : y ≠ 0
x : ℝ≥0
⊢ (x ^ y⁻¹) ^ y = x
have rw : x ^ (y⁻¹ * y) = x
Tactic: rw [← rpow_mul, inv_mul_cancel₀ hy, rpow_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y : ℝ
hy : y ≠ 0
x : ℝ≥0
rw : x ^ (y⁻¹ * y) = x
⊢ (x ^ y⁻¹) ^ y = x
have rw₁ : HPow.hPow (β := ℝ) x 1 = x
Tactic: rw [← rpow_mul, inv_mul_cancel₀ hy, rpow_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y : ℝ
hy : y ≠ 0
x : ℝ≥0
rw : x ^ (y⁻¹ * y) = x
rw₁ : HPow.hPow (β := ℝ) x 1 = x
⊢ (x ^ y⁻¹) ^ y = x
have rw₂ : x = x
Tactic: rw [← rpow_mul, inv_mul_cancel₀ hy, rpow_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x : ℝ≥0
n : ℕ
hn : n ≠ 0
⊢ HPow.hPow (β := ℝ) (x ^ n) (↑n : ℝ)⁻¹ = x
have rw : HPow.hPow (β := ℝ) ((↑x : ℝ) ^ n) (↑n : ℝ)⁻¹ = (↑x : ℝ)
Tactic: rw [← NNReal.coe_inj, coe_rpow, NNReal.coe_pow]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x : ℝ≥0
n : ℕ
hn : n ≠ 0
⊢ HPow.hPow (β := ℝ) x (↑n : ℝ)⁻¹ ^ n = x
have rw : HPow.hPow (β := ℝ) (↑x : ℝ) (↑n : ℝ)⁻¹ ^ n = (↑x : ℝ)
Tactic: rw [← NNReal.coe_inj, NNReal.coe_pow, coe_rpow]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x y : ℝ
hx : 0 ≤ x
⊢ (x ^ y).toNNReal = x.toNNReal ^ y
have nth_rw : ((↑x.toNNReal : ℝ) ^ y).toNNReal = x.toNNReal ^ y
Tactic: nth_rw 1 [← Real.coe_toNNReal x hx]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x y : ℝ
hx : 0 ≤ x
⊢ ((↑x.toNNReal : ℝ) ^ y).toNNReal = x.toNNReal ^ y
have rw : (↑(x.toNNReal ^ y) : ℝ).toNNReal = x.toNNReal ^ y
Tactic: rw [← NNReal.coe_rpow, Real.toNNReal_coe]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x y : ℝ
hx : 0 ≤ x
rw : (↑(x.toNNReal ^ y) : ℝ).toNNReal = x.toNNReal ^ y
⊢ ((↑x.toNNReal : ℝ) ^ y).toNNReal = x.toNNReal ^ y
have rw₁ : x.toNNReal ^ y = x.toNNReal ^ y
Tactic: rw [← NNReal.coe_rpow, Real.toNNReal_coe]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x_1 : ℝ≥0
w y_1 z y : ℝ
hy : 0 < y
x : ℝ≥0
⊢ (x ^ (1 / y)) ^ y = x
have rw : x ^ (1 / y * y) = x
Tactic: rw [← rpow_mul, one_div_mul_cancel hy.ne.symm, rpow_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x_1 : ℝ≥0
w y_1 z y : ℝ
hy : 0 < y
x : ℝ≥0
rw : x ^ (1 / y * y) = x
⊢ (x ^ (1 / y)) ^ y = x
have rw₁ : HPow.hPow (β := ℝ) x 1 = x
Tactic: rw [← rpow_mul, one_div_mul_cancel hy.ne.symm, rpow_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x_1 : ℝ≥0
w y_1 z y : ℝ
hy : 0 < y
x : ℝ≥0
rw : x ^ (1 / y * y) = x
rw₁ : HPow.hPow (β := ℝ) x 1 = x
⊢ (x ^ (1 / y)) ^ y = x
have rw₂ : x = x
Tactic: rw [← rpow_mul, one_div_mul_cancel hy.ne.symm, rpow_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y : ℝ
hy : 0 < y
⊢ (orderIsoRpow y hy).symm = orderIsoRpow (1 / y) ⋯
have simp : (StrictMono.orderIsoOfRightInverse (fun (x : ℝ≥0) ↦ x ^ y) sorry (fun (x : ℝ≥0) ↦ x ^ (1 / y)) sorry).symm =
  StrictMono.orderIsoOfRightInverse (fun (x : ℝ≥0) ↦ x ^ (1 / y)) sorry (fun (x : ℝ≥0) ↦ x ^ y) sorry
Tactic: simp only [orderIsoRpow, one_div_one_div]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x y : ℝ
hx : 0 ≤ x
⊢ ‖x ^ y‖₊ = ‖x‖₊ ^ y
have a : (↑‖x ^ y‖₊ : ℝ) = (↑(‖x‖₊ ^ y) : ℝ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x : ℝ≥0∞
⊢ HPow.hPow (β := ℝ) x 0 = 1
have top : HPow.hPow (α := ℝ≥0∞) (β := ℝ) ∞ 0 = 1
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x : ℝ≥0∞
top : HPow.hPow (α := ℝ≥0∞) (β := ℝ) ∞ 0 = 1
⊢ HPow.hPow (β := ℝ) x 0 = 1
have coe : ∀ (x : ℝ≥0), HPow.hPow (β := ℝ) (↑x : ℝ≥0∞) 0 = 1
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x : ℝ≥0∞
⊢ 0 < HPow.hPow (β := ℝ) x 0
have rw : LT.lt (α := ℝ≥0∞) 0 1
Tactic: rw [rpow_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y : ℝ
⊢ HPow.hPow (α := ℝ≥0∞) 0 y = if 0 < y then 0 else if y = 0 then 1 else ∞
have inl : ∀ (H : 0 < y), HPow.hPow (α := ℝ≥0∞) 0 y = if 0 < y then 0 else if y = 0 then 1 else ∞
Tactic: rcases lt_trichotomy (0 : ℝ) y with (H | rfl | H)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y : ℝ
inl : ∀ (H : 0 < y), HPow.hPow (α := ℝ≥0∞) 0 y = if 0 < y then 0 else if y = 0 then 1 else ∞
⊢ HPow.hPow (α := ℝ≥0∞) 0 y = if 0 < y then 0 else if y = 0 then 1 else ∞
have inr : HPow.hPow (α := ℝ≥0∞) (β := ℝ) 0 0 = if LT.lt (α := ℝ) 0 0 then 0 else if Eq (α := ℝ) 0 0 then 1 else ∞
Tactic: rcases lt_trichotomy (0 : ℝ) y with (H | rfl | H)
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y : ℝ
inl : ∀ (H : 0 < y), HPow.hPow (α := ℝ≥0∞) 0 y = if 0 < y then 0 else if y = 0 then 1 else ∞
inr : HPow.hPow (α := ℝ≥0∞) (β := ℝ) 0 0 = if LT.lt (α := ℝ) 0 0 then 0 else if Eq (α := ℝ) 0 0 then 1 else ∞
⊢ HPow.hPow (α := ℝ≥0∞) 0 y = if 0 < y then 0 else if y = 0 then 1 else ∞
have inr₁ : ∀ (H : y < 0), HPow.hPow (α := ℝ≥0∞) 0 y = if 0 < y then 0 else if y = 0 then 1 else ∞
Tactic: rcases lt_trichotomy (0 : ℝ) y with (H | rfl | H)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y : ℝ
⊢ HPow.hPow (α := ℝ≥0∞) 0 y * HPow.hPow (α := ℝ≥0∞) 0 y = HPow.hPow (α := ℝ≥0∞) 0 y
have rw : HMul.hMul (α := ℝ≥0∞) (if 0 < y then 0 else if y = 0 then 1 else ∞) (if 0 < y then 0 else if y = 0 then 1 else ∞) =
  if 0 < y then 0 else if y = 0 then 1 else ∞
Tactic: rw [zero_rpow_def]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y : ℝ
⊢ HMul.hMul (α := ℝ≥0∞) (if 0 < y then 0 else if y = 0 then 1 else ∞) (if 0 < y then 0 else if y = 0 then 1 else ∞) =
    if 0 < y then 0 else if y = 0 then 1 else ∞
have pos : 0 < y → HMul.hMul (α := ℝ≥0∞) 0 0 = 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y : ℝ
pos : 0 < y → HMul.hMul (α := ℝ≥0∞) 0 0 = 0
⊢ HMul.hMul (α := ℝ≥0∞) (if 0 < y then 0 else if y = 0 then 1 else ∞) (if 0 < y then 0 else if y = 0 then 1 else ∞) =
    if 0 < y then 0 else if y = 0 then 1 else ∞
have pos₁ : ¬0 < y → y = 0 → HMul.hMul (α := ℝ≥0∞) 1 1 = 1
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y : ℝ
pos : 0 < y → HMul.hMul (α := ℝ≥0∞) 0 0 = 0
pos₁ : ¬0 < y → y = 0 → HMul.hMul (α := ℝ≥0∞) 1 1 = 1
⊢ HMul.hMul (α := ℝ≥0∞) (if 0 < y then 0 else if y = 0 then 1 else ∞) (if 0 < y then 0 else if y = 0 then 1 else ∞) =
    if 0 < y then 0 else if y = 0 then 1 else ∞
have neg : ¬0 < y → ¬y = 0 → HMul.hMul (α := ℝ≥0∞) ∞ ∞ = ∞
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x : ℝ≥0
y : ℝ
h : 0 ≤ y
⊢ (↑(x ^ y) : ℝ≥0∞) = (↑x : ℝ≥0∞) ^ y
have pos : ∀ (hx : x = 0), (↑(x ^ y) : ℝ≥0∞) = (↑x : ℝ≥0∞) ^ y
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x : ℝ≥0
y : ℝ
h : 0 ≤ y
pos : ∀ (hx : x = 0), (↑(x ^ y) : ℝ≥0∞) = (↑x : ℝ≥0∞) ^ y
⊢ (↑(x ^ y) : ℝ≥0∞) = (↑x : ℝ≥0∞) ^ y
have neg : ∀ (hx : ¬x = 0), (↑(x ^ y) : ℝ≥0∞) = (↑x : ℝ≥0∞) ^ y
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x : ℝ≥0
y : ℝ
h : 0 ≤ y
hx : x = 0
⊢ (↑(x ^ y) : ℝ≥0∞) = (↑x : ℝ≥0∞) ^ y
have pos : ∀ (H : 0 = y), (↑(x ^ y) : ℝ≥0∞) = (↑x : ℝ≥0∞) ^ y
Tactic: rcases le_iff_eq_or_lt.1 h with (H | H)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x : ℝ≥0
y : ℝ
h : 0 ≤ y
hx : x = 0
pos : ∀ (H : 0 = y), (↑(x ^ y) : ℝ≥0∞) = (↑x : ℝ≥0∞) ^ y
⊢ (↑(x ^ y) : ℝ≥0∞) = (↑x : ℝ≥0∞) ^ y
have pos₁ : ∀ (H : 0 < y), (↑(x ^ y) : ℝ≥0∞) = (↑x : ℝ≥0∞) ^ y
Tactic: rcases le_iff_eq_or_lt.1 h with (H | H)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
M : ℝ≥0
P : ℝ
hP : 0 ≤ P
⊢ (↑M : ℝ≥0∞) ^ P = (↑(M ^ P) : ℝ≥0∞)
have rw : (↑M : ℝ≥0∞) ^ P = (↑M : ℝ≥0∞) ^ P
Tactic: rw [ENNReal.coe_rpow_of_nonneg _ hP, ← ENNReal.rpow_eq_pow]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
M : ℝ≥0
P : ℝ
hP : 0 ≤ P
rw : (↑M : ℝ≥0∞) ^ P = (↑M : ℝ≥0∞) ^ P
⊢ (↑M : ℝ≥0∞) ^ P = (↑(M ^ P) : ℝ≥0∞)
have rw₁ : (↑M : ℝ≥0∞).rpow P = (↑M : ℝ≥0∞).rpow P
Tactic: rw [ENNReal.coe_rpow_of_nonneg _ hP, ← ENNReal.rpow_eq_pow]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x : ℝ≥0∞
⊢ HPow.hPow (β := ℝ) x 1 = x
have top : HPow.hPow (α := ℝ≥0∞) (β := ℝ) ∞ 1 = ∞
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x : ℝ≥0∞
top : HPow.hPow (α := ℝ≥0∞) (β := ℝ) ∞ 1 = ∞
⊢ HPow.hPow (β := ℝ) x 1 = x
have coe : ∀ (x : ℝ≥0), HPow.hPow (β := ℝ) (↑x : ℝ≥0∞) 1 = (↑x : ℝ≥0∞)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x : ℝ≥0
⊢ (if x = 0 ∧ LT.lt (α := ℝ) 1 0 then ∞ else (↑(HPow.hPow (β := ℝ) x 1) : ℝ≥0∞)) = (↑x : ℝ≥0∞)
have coe : x = 0 → LT.lt (α := ℝ) 1 0 → False
Tactic: simp only [NNReal.rpow_one, ite_eq_right_iff, top_ne_coe, and_imp]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
x : ℝ
⊢ HPow.hPow (α := ℝ≥0∞) 1 x = 1
have rw : (↑(HPow.hPow (α := ℝ≥0) 1 x) : ℝ≥0∞) = (↑1 : ℝ≥0∞)
Tactic: rw [← coe_one, ← coe_rpow_of_ne_zero one_ne_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y : ℝ
⊢ HPow.hPow (α := ℝ≥0∞) ∞ y = 0 ↔ Eq (α := ℝ≥0∞) ∞ 0 ∧ 0 < y ∨ Eq (α := ℝ≥0∞) ∞ ∞ ∧ y < 0
have top : ∀ (H : y < 0), HPow.hPow (α := ℝ≥0∞) ∞ y = 0 ↔ Eq (α := ℝ≥0∞) ∞ 0 ∧ 0 < y ∨ Eq (α := ℝ≥0∞) ∞ ∞ ∧ y < 0
Tactic: rcases lt_trichotomy y 0 with (H | H | H)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.NNReal (goal)
Goal:
y : ℝ
top : ∀ (H : y < 0), HPow.hPow (α := ℝ≥0∞) ∞ y = 0 ↔ Eq (α := ℝ≥0∞) ∞ 0 ∧ 0 < y ∨ Eq (α := ℝ≥0∞) ∞ ∞ ∧ y < 0
⊢ HPow.hPow (α := ℝ≥0∞) ∞ y = 0 ↔ Eq (α := ℝ≥0∞) ∞ 0 ∧ 0 < y ∨ Eq (α := ℝ≥0∞) ∞ ∞ ∧ y < 0
have top₁ : ∀ (H : y = 0), HPow.hPow (α := ℝ≥0∞) ∞ y = 0 ↔ Eq (α := ℝ≥0∞) ∞ 0 ∧ 0 < y ∨ Eq (α := ℝ≥0∞) ∞ ∞ ∧ y < 0
Tactic: rcases lt_trichotomy y 0 with (H | H | H)