awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0∞
z : ℝ
H : z < 0
inl : (HPow.hPow (α := ℝ≥0∞) ∞ z).toNNReal = ENNReal.toNNReal ∞ ^ z
inl₁ : ∀ (x : ℝ≥0), ((↑x : ℝ≥0∞) ^ z).toNNReal = (↑x : ℝ≥0∞).toNNReal ^ z
⊢ (x ^ z).toNNReal = x.toNNReal ^ z

Tactic:
cases x with
    | top => simp [H, ne_of_lt]
    | coe x =>
      by_cases hx : x = 0
      · simp [hx, H, ne_of_lt]
      · simp [← coe_rpow_of_ne_zero hx]

Premises used: ne_of_lt
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0∞
z : ℝ
H : z = 0
⊢ (x ^ z).toNNReal = x.toNNReal ^ z

Tactic:
simp [H]
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0∞
z : ℝ
H : 0 < z
inr : (HPow.hPow (α := ℝ≥0∞) ∞ z).toNNReal = ENNReal.toNNReal ∞ ^ z
inr₁ : ∀ (x : ℝ≥0), ((↑x : ℝ≥0∞) ^ z).toNNReal = (↑x : ℝ≥0∞).toNNReal ^ z
⊢ (x ^ z).toNNReal = x.toNNReal ^ z

Tactic:
cases x
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
z : ℝ
H : 0 < z
⊢ (HPow.hPow (α := ℝ≥0∞) ∞ z).toNNReal = ENNReal.toNNReal ∞ ^ z

Tactic:
simp [H, ne_of_gt]

Premises used: ne_of_gt
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
z : ℝ
H : 0 < z
x : ℝ≥0
⊢ ((↑x : ℝ≥0∞) ^ z).toNNReal = (↑x : ℝ≥0∞).toNNReal ^ z

Tactic:
simp [← coe_rpow_of_nonneg _ (le_of_lt H)]

Premises used: le_of_lt, ENNReal.coe_rpow_of_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ≥0∞
z : ℝ
rw : (↑x.toNNReal : ℝ) ^ z = (x ^ z).toReal
rw₁ : (↑x.toNNReal : ℝ) ^ z = (↑(x ^ z).toNNReal : ℝ)
rw₂ : (↑(x.toNNReal ^ z) : ℝ) = (↑(x ^ z).toNNReal : ℝ)
rw₃ rw₄ : (↑(x.toNNReal ^ z) : ℝ) = (↑(x.toNNReal ^ z) : ℝ)
⊢ x.toReal ^ z = (x ^ z).toReal

Tactic:
rw [ENNReal.toReal, ENNReal.toReal, ← NNReal.coe_rpow, ENNReal.toNNReal_rpow]

Premises used: NNReal.coe_rpow, ENNReal.toNNReal_rpow, ENNReal.toReal
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x p : ℝ
hx_pos : 0 < x
h : x.toNNReal ≠ 0
⊢ (↑x.toNNReal : ℝ≥0∞) ^ p = (↑(x ^ p).toNNReal : ℝ≥0∞)

Tactic:
rw [← coe_rpow_of_ne_zero, coe_inj, Real.toNNReal_rpow_of_nonneg hx_pos.le]

Premises used: ENNReal.coe_inj, LT.lt.le, ENNReal.coe_rpow_of_ne_zero, Real.toNNReal_rpow_of_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x p : ℝ
hx_pos : 0 < x
⊢ x.toNNReal ≠ 0

Tactic:
simp [hx_pos]
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x p : ℝ
hx_nonneg : 0 ≤ x
hp_nonneg : 0 ≤ p
pos : ∀ (hp0 : p = 0), ENNReal.ofReal x ^ p = ENNReal.ofReal (x ^ p)
neg : ∀ (hp0 : ¬p = 0), ENNReal.ofReal x ^ p = ENNReal.ofReal (x ^ p)
⊢ ENNReal.ofReal x ^ p = ENNReal.ofReal (x ^ p)

Tactic:
by_cases hp0 : p = 0
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x p : ℝ
hx_nonneg : 0 ≤ x
hp_nonneg : 0 ≤ p
hp0 : p = 0
⊢ ENNReal.ofReal x ^ p = ENNReal.ofReal (x ^ p)

Tactic:
simp [hp0]
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x p : ℝ
hx_nonneg : 0 ≤ x
hp_nonneg : 0 ≤ p
hp0 : ¬p = 0
pos : ∀ (hx0 : x = 0), ENNReal.ofReal x ^ p = ENNReal.ofReal (x ^ p)
neg : ∀ (hx0 : ¬x = 0), ENNReal.ofReal x ^ p = ENNReal.ofReal (x ^ p)
⊢ ENNReal.ofReal x ^ p = ENNReal.ofReal (x ^ p)

Tactic:
by_cases hx0 : x = 0
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x p : ℝ
hx_nonneg : 0 ≤ x
hp_nonneg : 0 ≤ p
hp0 : ¬p = 0
hx0 : x = 0
⊢ p ≠ 0

Tactic:
rw [← Ne] at hp0

Premises used: Ne
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x p : ℝ
hx_nonneg : 0 ≤ x
hp_nonneg : 0 ≤ p
hp0 : ¬p = 0
hx0 : x = 0
hp0₁ : p ≠ 0
⊢ x = 0

Tactic:
rw [← Ne] at hp0

Premises used: Ne
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x p : ℝ
hx_nonneg : 0 ≤ x
hp_nonneg : 0 ≤ p
hp0 : p ≠ 0
hx0 : x = 0
⊢ 0 < p

Tactic:
have hp_pos : 0 < p := lt_of_le_of_ne hp_nonneg hp0.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x p : ℝ
hx_nonneg : 0 ≤ x
hp_nonneg : 0 ≤ p
hp0 : p ≠ 0
hx0 : x = 0
hp_pos : 0 < p
⊢ ENNReal.ofReal x ^ p = ENNReal.ofReal (x ^ p)

Tactic:
simp [hx0, hp_pos, hp_pos.ne.symm]

Premises used: Ne.symm, LT.lt.ne
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x p : ℝ
hx_nonneg : 0 ≤ x
hp_nonneg : 0 ≤ p
hp0 : ¬p = 0
hx0 : ¬x = 0
⊢ x ≠ 0

Tactic:
rw [← Ne] at hx0

Premises used: Ne
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x p : ℝ
hx_nonneg : 0 ≤ x
hp_nonneg : 0 ≤ p
hp0 : ¬p = 0
hx0 : x ≠ 0
⊢ ENNReal.ofReal x ^ p = ENNReal.ofReal (x ^ p)

Tactic:
ofReal_rpow_of_pos (hx_nonneg.lt_of_ne hx0.symm)

Premises used: ENNReal.ofReal_rpow_of_pos, Ne.symm, LE.le.lt_of_ne
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x p : ℝ
hx_nonneg : 0 ≤ x
hp_nonneg : 0 ≤ p
hp0 : ¬p = 0
hx0 : x ≠ 0
⊢ ENNReal.ofReal x ^ p = ENNReal.ofReal (x ^ p)

Tactic:
exact ofReal_rpow_of_pos (hx_nonneg.lt_of_ne hx0.symm)

Premises used: ENNReal.ofReal_rpow_of_pos, Ne.symm, LE.le.lt_of_ne
-- 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: ENNReal.rpow_mul, mul_inv_cancel₀, ENNReal.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: ENNReal.rpow_mul, ENNReal.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 [rpow_zero, rpow_rpow_inv]

Premises used: ENNReal.rpow_rpow_inv, ENNReal.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: ENNReal.rpow_rpow_inv_eq_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ≥0∞
⊢ Ne (α := ℝ) (↑n : ℝ) 0

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ≥0∞
rw : HPow.hPow (β := ℝ) (HPow.hPow (β := ℝ) x (↑n : ℝ)) (↑n : ℝ)⁻¹ = x
rw₁ : x ^ HMul.hMul (α := ℝ) (↑n : ℝ) (↑n : ℝ)⁻¹ = x
rw₂ : HPow.hPow (β := ℝ) x 1 = x
rw₃ rw₄ : x = x
⊢ HPow.hPow (β := ℝ) (x ^ n) (↑n : ℝ)⁻¹ = x

Tactic:
rw [← rpow_natCast, ← rpow_mul, mul_inv_cancel₀ (by positivity), rpow_one]

Premises used: ENNReal.rpow_mul, mul_inv_cancel₀, ENNReal.rpow_one, ENNReal.rpow_natCast
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ≥0∞
rw : HPow.hPow (β := ℝ) (HPow.hPow (β := ℝ) x (↑n : ℝ)⁻¹) (↑n : ℝ) = x
rw₁ : x ^ HMul.hMul (α := ℝ) (↑n : ℝ)⁻¹ (↑n : ℝ) = x
rw₂ : HPow.hPow (β := ℝ) x 1 = x
rw₃ rw₄ : x = x
⊢ HPow.hPow (β := ℝ) x (↑n : ℝ)⁻¹ ^ n = x

Tactic:
rw [← rpow_natCast, ← rpow_mul, inv_mul_cancel₀ (by positivity), rpow_one]

Premises used: ENNReal.rpow_mul, ENNReal.rpow_one, ENNReal.rpow_natCast, inv_mul_cancel₀
-- 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: ENNReal.rpow_mul, ENNReal.rpow_natCast
-- 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: ENNReal.rpow_mul, ENNReal.rpow_natCast
-- 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: ENNReal.rpow_mul, ENNReal.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: ENNReal.rpow_mul, ENNReal.rpow_intCast
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ
hx : x ≠ 0
⊢ Injective (β := ℝ≥0∞) fun (y : ℝ≥0∞) ↦ y ^ x

Tactic:
HasLeftInverse.injective ⟨fun y ↦ y ^ x⁻¹, rpow_rpow_inv hx⟩

Premises used: Function.HasLeftInverse.injective, ENNReal.rpow_rpow_inv, Inv.inv, HPow.hPow, Exists.intro
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x : ℝ
hx : x ≠ 0
⊢ Surjective (β := ℝ≥0∞) fun (y : ℝ≥0∞) ↦ y ^ x

Tactic:
HasRightInverse.surjective ⟨fun y ↦ y ^ x⁻¹, rpow_inv_rpow hx⟩

Premises used: ENNReal.rpow_inv_rpow, Function.HasRightInverse.surjective, Inv.inv, HPow.hPow, Exists.intro
-- 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: ENNReal.rpow_left_injective, ENNReal.rpow_left_surjective, And.intro, Function.Bijective
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
x y : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
⊢ ‖x ^ y‖ₑ = ‖x‖ₑ ^ y

Tactic:
simp [enorm, nnnorm_rpow_of_nonneg hx, coe_rpow_of_nonneg _ hy]

Premises used: ENNReal.coe_rpow_of_nonneg, ENorm.enorm, Real.nnnorm_rpow_of_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
p : ℝ
a b : ℝ≥0∞
hp : 0 ≤ p
rw : (a + b) ^ p ≤ (max a b + max a b) ^ p
⊢ (a + b) ^ p ≤ (2 * max a b) ^ p

Tactic:
rw [two_mul]

Premises used: two_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
p : ℝ
a b : ℝ≥0∞
hp : 0 ≤ p
h₁ : a ≤ max a b
h₂ : b ≤ max a b
⊢ (a + b) ^ p ≤ (max a b + max a b) ^ p

Tactic:
gcongr
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
p : ℝ
a b : ℝ≥0∞
hp : 0 ≤ p
⊢ a ≤ max a b

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
p : ℝ
a b : ℝ≥0∞
hp : 0 ≤ p
⊢ b ≤ max a b

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
p : ℝ
a b : ℝ≥0∞
hp : 0 ≤ p
rw rw₁ : HPow.hPow (α := ℝ≥0∞) 2 p * max (a ^ p) (b ^ p) = HPow.hPow (α := ℝ≥0∞) 2 p * max (a ^ p) (b ^ p)
⊢ HPow.hPow (α := ℝ≥0∞) 2 p * max a b ^ p = HPow.hPow (α := ℝ≥0∞) 2 p * max (a ^ p) (b ^ p)

Tactic:
rw [max_rpow hp]

Premises used: ENNReal.max_rpow
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
p : ℝ
a b : ℝ≥0∞
hp : 0 ≤ p
bc : max (a ^ p) (b ^ p) ≤ a ^ p + b ^ p
⊢ HPow.hPow (α := ℝ≥0∞) 2 p * max (a ^ p) (b ^ p) ≤ HPow.hPow (α := ℝ≥0∞) 2 p * (a ^ p + b ^ p)

Tactic:
gcongr
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
p : ℝ
a b : ℝ≥0∞
hp : 0 ≤ p
bc : 0 ≤ a ^ p
bc₁ : 0 ≤ b ^ p
⊢ max (a ^ p) (b ^ p) ≤ a ^ p + b ^ p

Tactic:
apply max_le_add_of_nonneg

Premises used: max_le_add_of_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
p : ℝ
a b : ℝ≥0∞
hp : 0 ≤ p
⊢ 0 ≤ a ^ p

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
p : ℝ
a b : ℝ≥0∞
hp : 0 ≤ p
⊢ 0 ≤ b ^ p

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
b : ℝ
n : ℕ
h : IsNat b n
a : ℝ≥0
rw : HPow.hPow (β := ℝ) a (↑n : ℝ) = a ^ n
rw₁ rw₂ : a ^ n = a ^ n
⊢ a ^ b = a ^ n

Tactic:
rw [h.1, NNReal.rpow_natCast]

Premises used: NNReal.rpow_natCast, Mathlib.Meta.NormNum.IsNat.out
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
b : ℝ
n : ℕ
h : IsInt b (Int.negOfNat n)
a : ℝ≥0
rw : HPow.hPow (β := ℝ) a (↑(Int.negOfNat n) : ℝ) = (a ^ n)⁻¹
rw₁ : a ^ Int.negOfNat n = (a ^ n)⁻¹
rw₂ : a ^ (-Int.ofNat n) = (a ^ n)⁻¹
rw₃ : (a ^ Int.ofNat n)⁻¹ = (a ^ n)⁻¹
rw₄ : (HPow.hPow (β := ℤ) a (↑n : ℤ))⁻¹ = (a ^ n)⁻¹
rw₅ rw₆ : (a ^ n)⁻¹ = (a ^ n)⁻¹
⊢ a ^ b = (a ^ n)⁻¹

Tactic:
rw [h.1, NNReal.rpow_intCast, Int.negOfNat_eq, zpow_neg, Int.ofNat_eq_natCast, zpow_natCast]

Premises used: zpow_natCast, Int.ofNat_eq_natCast, NNReal.rpow_intCast, zpow_neg, Mathlib.Meta.NormNum.IsInt.out, Int.negOfNat_eq
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
a : ℝ≥0
b : ℝ
m n d r : ℕ
ha : IsNat a m
hb : IsNNRat b n d
k : ℕ
hr : r ^ d = k
l : ℕ
hm : m ^ n = l
hkl : k = l
rcases : IsNat (HPow.hPow (α := ℝ≥0) (↑m : ℝ≥0) b) r
⊢ IsNat (a ^ b) r

Tactic:
rcases ha with ⟨rfl⟩

Premises used: rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
b : ℝ
m n d r : ℕ
hb : IsNNRat b n d
k : ℕ
hr : r ^ d = k
l : ℕ
hm : m ^ n = l
hkl : k = l
out : HPow.hPow (α := ℝ≥0) (↑m : ℝ≥0) b = (↑r : ℝ≥0)
⊢ IsNat (HPow.hPow (α := ℝ≥0) (↑m : ℝ≥0) b) r

Tactic:
constructor
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
b : ℝ
m n d r : ℕ
hb : IsNNRat b n d
k : ℕ
hr : r ^ d = k
l : ℕ
hm : m ^ n = l
hkl : k = l
⊢ d ≠ 0

Tactic:
have : d ≠ 0 := mod_cast hb.den_nz
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
b : ℝ
m n d r : ℕ
hb : IsNNRat b n d
k : ℕ
hr : r ^ d = k
l : ℕ
hm : m ^ n = l
hkl : k = l
this out : d ≠ 0
⊢ HPow.hPow (α := ℝ≥0) (↑m : ℝ≥0) b = (↑r : ℝ≥0)

Tactic:
rw [hb.to_eq rfl rfl, div_eq_mul_inv, NNReal.rpow_natCast_mul, ← Nat.cast_pow, hm, ← hkl, ← hr,
    Nat.cast_pow, NNReal.pow_rpow_inv_natCast]

Premises used: NNReal.pow_rpow_inv_natCast, Mathlib.Meta.NormNum.IsNNRat.to_eq, NNReal.rpow_natCast_mul, div_eq_mul_inv, Nat.cast_pow, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
b : ℝ
m n d r : ℕ
hb : IsNNRat b n d
k : ℕ
hr : r ^ d = k
l : ℕ
hm : m ^ n = l
hkl : k = l
this : d ≠ 0
⊢ d ≠ 0

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
a : ℝ≥0
b : ℝ
na da : ℕ
ha : IsNNRat a na da
nr dr : ℕ
hnum : IsNat (HPow.hPow (α := ℝ≥0) (↑na : ℝ≥0) b) nr
hden : IsNat (HPow.hPow (α := ℝ≥0) (↑da : ℝ≥0) b) dr
this : IsNNRat (HDiv.hDiv (α := ℝ≥0) (↑nr : ℝ≥0) (↑dr : ℝ≥0)) nr dr
⊢ IsNNRat (a ^ b) nr dr

Tactic:
simpa [ha.to_eq, NNReal.div_rpow, hnum.1, hden.1]

Premises used: Mathlib.Meta.NormNum.IsNNRat.to_eq, Mathlib.Meta.NormNum.IsNat.out, NNReal.div_rpow
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
a : ℝ≥0
b : ℝ
na da : ℕ
ha : IsNNRat a na da
nr dr : ℕ
hnum : IsNat (HPow.hPow (α := ℝ≥0) (↑na : ℝ≥0) b) nr
hden : IsNat (HPow.hPow (α := ℝ≥0) (↑da : ℝ≥0) b) dr
suffices : IsNNRat (HDiv.hDiv (α := ℝ≥0) (↑nr : ℝ≥0) (↑dr : ℝ≥0)) nr dr
⊢ IsNNRat (a ^ b) nr dr

Tactic:
suffices IsNNRat (nr / dr : ℝ≥0) nr dr by
    simpa [ha.to_eq, NNReal.div_rpow, hnum.1, hden.1]
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
a : ℝ≥0
b : ℝ
na da : ℕ
ha : IsNNRat a na da
nr dr : ℕ
hnum : IsNat (HPow.hPow (α := ℝ≥0) (↑na : ℝ≥0) b) nr
hden : IsNat (HPow.hPow (α := ℝ≥0) (↑da : ℝ≥0) b) dr
h : Ne (α := ℝ≥0) (↑dr : ℝ≥0) 0
⊢ IsNNRat (HDiv.hDiv (α := ℝ≥0) (↑nr : ℝ≥0) (↑dr : ℝ≥0)) nr dr

Tactic:
apply IsNNRat.of_raw

Premises used: Mathlib.Meta.NormNum.IsNNRat.of_raw
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
a : ℝ≥0
b : ℝ
na da : ℕ
ha : IsNNRat a na da
nr dr : ℕ
hnum : IsNat (HPow.hPow (α := ℝ≥0) (↑na : ℝ≥0) b) nr
hden : IsNat (HPow.hPow (α := ℝ≥0) (↑da : ℝ≥0) b) dr
⊢ Ne (α := ℝ≥0) (↑dr : ℝ≥0) 0

Tactic:
simp [← hden.1, ha.den_nz]

Premises used: Mathlib.Meta.NormNum.IsNNRat.den_nz, Mathlib.Meta.NormNum.IsNat.out
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Goal:
a : ℝ≥0
b : ℝ
n d : ℕ
hb : IsRat b (Int.negOfNat n) d
rw : a ^ b = (a ^ HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑d : ℝ))⁻¹
rw₁ : a ^ b = a ^ (-HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑d : ℝ))
rw₂ rw₃ : a ^ (-HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑d : ℝ)) = a ^ (-HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑d : ℝ))
⊢ a ^ b = a⁻¹ ^ HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑d : ℝ)

Tactic:
rw [NNReal.inv_rpow, ← NNReal.rpow_neg, hb.neg_to_eq rfl rfl]

Premises used: NNReal.inv_rpow, NNReal.rpow_neg, rfl, Mathlib.Meta.NormNum.IsRat.neg_to_eq
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Goal:
x : ℂ
⊢ HasStrictDerivAt (fun (y : ℂ) ↦ HSub.hSub (β := ℂ → ℂ) cexp (fun (x : ℂ) ↦ cexp (-id x)) y * 2⁻¹)
    ((cexp x - cexp (-id x) * -1) * 2⁻¹) x

Tactic:
((hasStrictDerivAt_exp x).sub (hasStrictDerivAt_id x).fun_neg.cexp).mul_const (2 : ℂ)⁻¹

Premises used: HasStrictDerivAt.mul_const, HasStrictDerivAt.cexp, HasStrictDerivAt.sub, Inv.inv, Complex.hasStrictDerivAt_exp, HasStrictDerivAt.fun_neg, OfNat.ofNat, hasStrictDerivAt_id
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Goal:
x : ℂ
h : (cexp x + cexp (-x)) * 2⁻¹ = (cexp x - cexp (-id x) * -1) * 2⁻¹
⊢ HasStrictDerivAt sinh ((cexp x + cexp (-x)) * 2⁻¹) x

Tactic:
convert!
    ((hasStrictDerivAt_exp x).sub (hasStrictDerivAt_id x).fun_neg.cexp).mul_const (2 : ℂ)⁻¹ using 1

Premises used: HasStrictDerivAt.mul_const, HasStrictDerivAt.cexp, HasStrictDerivAt.sub, Inv.inv, Complex.hasStrictDerivAt_exp, HasStrictDerivAt.fun_neg, OfNat.ofNat, hasStrictDerivAt_id
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Goal:
x : ℂ
h : (cexp x + cexp (-x)) * 2⁻¹ = (cexp x - cexp (-x) * -1) * 2⁻¹
h₁ : (cexp x + cexp (-x)) * 2⁻¹ = (cexp x - -cexp (-x)) * 2⁻¹
h₂ : (cexp x + cexp (-x)) * 2⁻¹ = (cexp x + - -cexp (-x)) * 2⁻¹
h₃ h₄ : (cexp x + cexp (-x)) * 2⁻¹ = (cexp x + cexp (-x)) * 2⁻¹
⊢ (cexp x + cexp (-x)) * 2⁻¹ = (cexp x - cexp (-id x) * -1) * 2⁻¹

Tactic:
rw [id, mul_neg_one, sub_eq_add_neg, neg_neg]

Premises used: sub_eq_add_neg, neg_neg, id, mul_neg_one
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Goal:
x : ℂ
⊢ HasDerivAt sinh (cosh x) x

Tactic:
(hasStrictDerivAt_sinh x).hasDerivAt

Premises used: Complex.hasStrictDerivAt_sinh, HasStrictDerivAt.hasDerivAt
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Goal:
⊢ sinh ~[𝓝 0] id

Tactic:
simpa using (hasDerivAt_sinh 0).isLittleO

Premises used: HasDerivAt.isLittleO, Complex.hasDerivAt_sinh, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Goal:
n : WithTop ℕ∞
⊢ ContDiff ℂ n sinh

Tactic:
(contDiff_exp.sub contDiff_neg.cexp).div_const _

Premises used: ContDiff.sub, ContDiff.div_const, Complex.sinh, ContDiff.cexp, Complex.contDiff_exp, contDiff_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Goal:
⊢ Differentiable ℂ sinh

Tactic:
fun x => (hasDerivAt_sinh x).differentiableAt

Premises used: Differentiable, HasDerivAt.differentiableAt, Complex.hasDerivAt_sinh
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Goal:
x : ℂ
⊢ DifferentiableAt ℂ sinh x

Tactic:
differentiable_sinh x

Premises used: Complex.differentiable_sinh
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Goal:
x : ℂ
⊢ AnalyticAt ℂ sinh x

Tactic:
contDiff_sinh.contDiffAt.analyticAt

Premises used: Complex.contDiff_sinh, ContDiffAt.analyticAt, ContDiff.contDiffAt
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Goal:
x : ℂ
s : Set ℂ
⊢ AnalyticWithinAt ℂ sinh s x

Tactic:
contDiff_sinh.contDiffWithinAt.analyticWithinAt

Premises used: Complex.contDiff_sinh, ContDiff.contDiffWithinAt, ContDiffWithinAt.analyticWithinAt
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Goal:
s : Set ℂ
⊢ AnalyticOnNhd ℂ sinh s

Tactic:
fun _ _ ↦ analyticAt_sinh

Premises used: AnalyticOnNhd, Complex.analyticAt_sinh
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Goal:
s : Set ℂ
⊢ AnalyticOn ℂ sinh s

Tactic:
contDiff_sinh.contDiffOn.analyticOn

Premises used: ContDiff.contDiffOn, ContDiffOn.analyticOn, Complex.contDiff_sinh
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Goal:
⊢ deriv sinh = cosh

Tactic:
funext fun x => (hasDerivAt_sinh x).deriv

Premises used: HasDerivAt.deriv, Complex.hasDerivAt_sinh, funext
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Goal:
x : ℂ
⊢ HasStrictDerivAt (fun (y : ℂ) ↦ HAdd.hAdd (β := ℂ → ℂ) cexp (fun (x : ℂ) ↦ cexp (-id x)) y * 2⁻¹)
    ((cexp x + cexp (-id x) * -1) * 2⁻¹) x

Tactic:
((hasStrictDerivAt_exp x).add (hasStrictDerivAt_id x).fun_neg.cexp).mul_const (2 : ℂ)⁻¹

Premises used: HasStrictDerivAt.mul_const, HasStrictDerivAt.cexp, HasStrictDerivAt.add, Inv.inv, Complex.hasStrictDerivAt_exp, HasStrictDerivAt.fun_neg, OfNat.ofNat, hasStrictDerivAt_id
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Goal:
x : ℂ
h : (cexp x - cexp (-x)) * 2⁻¹ = (cexp x + cexp (-id x) * -1) * 2⁻¹
⊢ HasStrictDerivAt cosh ((cexp x - cexp (-x)) * 2⁻¹) x

Tactic:
convert!
    ((hasStrictDerivAt_exp x).add (hasStrictDerivAt_id x).fun_neg.cexp).mul_const (2 : ℂ)⁻¹ using 1

Premises used: HasStrictDerivAt.mul_const, HasStrictDerivAt.cexp, HasStrictDerivAt.add, Inv.inv, Complex.hasStrictDerivAt_exp, HasStrictDerivAt.fun_neg, OfNat.ofNat, hasStrictDerivAt_id
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Goal:
x : ℂ
h : (cexp x - cexp (-x)) * 2⁻¹ = (cexp x + cexp (-x) * -1) * 2⁻¹
h₁ : (cexp x - cexp (-x)) * 2⁻¹ = (cexp x + -cexp (-x)) * 2⁻¹
h₂ h₃ : (cexp x + -cexp (-x)) * 2⁻¹ = (cexp x + -cexp (-x)) * 2⁻¹
⊢ (cexp x - cexp (-x)) * 2⁻¹ = (cexp x + cexp (-id x) * -1) * 2⁻¹

Tactic:
rw [id, mul_neg_one, sub_eq_add_neg]

Premises used: sub_eq_add_neg, id, mul_neg_one
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Goal:
x : ℂ
⊢ HasDerivAt cosh (sinh x) x

Tactic:
(hasStrictDerivAt_cosh x).hasDerivAt

Premises used: Complex.hasStrictDerivAt_cosh, HasStrictDerivAt.hasDerivAt
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Goal:
n : WithTop ℕ∞
⊢ ContDiff ℂ n cosh

Tactic:
(contDiff_exp.add contDiff_neg.cexp).div_const _

Premises used: ContDiff.div_const, ContDiff.cexp, Complex.contDiff_exp, contDiff_neg, ContDiff.add, Complex.cosh
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Goal:
⊢ Differentiable ℂ cosh

Tactic:
fun x => (hasDerivAt_cosh x).differentiableAt

Premises used: Differentiable, HasDerivAt.differentiableAt, Complex.hasDerivAt_cosh
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Goal:
x : ℂ
⊢ DifferentiableAt ℂ cosh x

Tactic:
differentiable_cosh x

Premises used: Complex.differentiable_cosh
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Goal:
x : ℂ
⊢ AnalyticAt ℂ cosh x

Tactic:
contDiff_cosh.contDiffAt.analyticAt

Premises used: Complex.contDiff_cosh, ContDiffAt.analyticAt, ContDiff.contDiffAt
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Goal:
x : ℂ
s : Set ℂ
⊢ AnalyticWithinAt ℂ cosh s x

Tactic:
contDiff_cosh.contDiffWithinAt.analyticWithinAt

Premises used: Complex.contDiff_cosh, ContDiff.contDiffWithinAt, ContDiffWithinAt.analyticWithinAt
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Goal:
s : Set ℂ
⊢ AnalyticOnNhd ℂ cosh s

Tactic:
fun _ _ ↦ analyticAt_cosh

Premises used: Complex.analyticAt_cosh, AnalyticOnNhd
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Goal:
s : Set ℂ
⊢ AnalyticOn ℂ cosh s

Tactic:
contDiff_cosh.contDiffOn.analyticOn

Premises used: ContDiff.contDiffOn, Complex.contDiff_cosh, ContDiffOn.analyticOn
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Goal:
⊢ deriv cosh = sinh

Tactic:
funext fun x => (hasDerivAt_cosh x).deriv

Premises used: HasDerivAt.deriv, funext, Complex.hasDerivAt_cosh
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Goal:
f : ℂ → ℂ
f' x : ℂ
hf : HasStrictDerivAt f f' x
⊢ HasStrictDerivAt (fun (x : ℂ) ↦ Complex.cosh (f x)) (Complex.sinh (f x) * f') x

Tactic:
(Complex.hasStrictDerivAt_cosh (f x)).comp x hf

Premises used: HasStrictDerivAt.comp, Complex.hasStrictDerivAt_cosh, Complex.cosh
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Goal:
f : ℂ → ℂ
f' x : ℂ
hf : HasDerivAt f f' x
⊢ HasDerivAt (fun (x : ℂ) ↦ Complex.cosh (f x)) (Complex.sinh (f x) * f') x

Tactic:
(Complex.hasDerivAt_cosh (f x)).comp x hf

Premises used: HasDerivAt.comp, Complex.hasDerivAt_cosh, Complex.cosh
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Goal:
f : ℂ → ℂ
f' x : ℂ
s : Set ℂ
hf : HasDerivWithinAt f f' s x
⊢ HasDerivWithinAt (fun (x : ℂ) ↦ Complex.cosh (f x)) (Complex.sinh (f x) * f') s x

Tactic:
(Complex.hasDerivAt_cosh (f x)).comp_hasDerivWithinAt x hf

Premises used: Complex.hasDerivAt_cosh, HasDerivAt.comp_hasDerivWithinAt, Complex.cosh
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Goal:
f : ℂ → ℂ
x : ℂ
s : Set ℂ
hf : DifferentiableWithinAt ℂ f s x
hxs : UniqueDiffWithinAt ℂ s x
⊢ derivWithin (fun (x : ℂ) ↦ Complex.cosh (f x)) s x = Complex.sinh (f x) * derivWithin f s x

Tactic:
hf.hasDerivWithinAt.ccosh.derivWithin hxs

Premises used: DifferentiableWithinAt.hasDerivWithinAt, HasDerivWithinAt.derivWithin, HasDerivWithinAt.ccosh