awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
Goal:
n a b : ℕ
hn : n ≠ 0
⊢ a ≤ n.nthRoot b ∨ n.nthRoot b < a

Tactic:
cases le_or_gt a (nthRoot n b) with
  | inl hle =>
    simp only [hle, true_iff]
    refine le_trans ?_ (pow_nthRoot_le (.inl hn))
    gcongr
  | inr hlt =>
    simp only [hlt.not_ge, false_iff, not_le]
    refine (lt_pow_nthRoot_add_one hn b).trans_le ?_
    gcongr
    assumption

Premises used: not_le, true_iff, Nat.nthRoot, Nat.lt_pow_nthRoot_add_one, false_iff, le_or_gt, LT.lt.trans_le, Or.inl, Nat.pow_nthRoot_le, le_trans
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
Goal:
n a b : ℕ
hn : n ≠ 0
⊢ n.nthRoot a < b ↔ a < b ^ n

Tactic:
simp only [← not_le, le_nthRoot_iff hn]

Premises used: not_le, Nat.le_nthRoot_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
Goal:
n : ℕ
hn : n ≠ 0
a : ℕ
⊢ n.nthRoot (a ^ n) = a

Tactic:
eq_of_forall_le_iff fun b ↦ ?_

Premises used: eq_of_forall_le_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
Goal:
n : ℕ
hn : n ≠ 0
a : ℕ
refine : ∀ (b : ℕ), b ≤ n.nthRoot (a ^ n) ↔ b ≤ a
⊢ n.nthRoot (a ^ n) = a

Tactic:
refine eq_of_forall_le_iff fun b ↦ ?_

Premises used: eq_of_forall_le_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
Goal:
n : ℕ
hn : n ≠ 0
a b : ℕ
rw : b ^ n ≤ a ^ n ↔ b ≤ a
⊢ b ≤ n.nthRoot (a ^ n) ↔ b ≤ a

Tactic:
rw [le_nthRoot_iff hn]

Premises used: Nat.le_nthRoot_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
Goal:
n : ℕ
hn : n ≠ 0
a b : ℕ
⊢ b ^ n ≤ a ^ n ↔ b ≤ a

Tactic:
(Nat.pow_left_strictMono hn).le_iff_le

Premises used: Nat.pow_left_strictMono, StrictMono.le_iff_le
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
Goal:
n : ℕ
hn : n ≠ 0
a b : ℕ
⊢ b ^ n ≤ a ^ n ↔ b ≤ a

Tactic:
exact (Nat.pow_left_strictMono hn).le_iff_le

Premises used: Nat.pow_left_strictMono, StrictMono.le_iff_le
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
Goal:
n a b : ℕ
h₁ : a ^ n ≤ b
h₂ : b < (a + 1) ^ n
inl : ∀ (h₁ : HPow.hPow (β := ℕ) a 0 ≤ b) (h₂ : b < HPow.hPow (β := ℕ) (a + 1) 0), nthRoot 0 b = a
inr : ∀ (hn : n ≠ 0), n.nthRoot b = a
⊢ n.nthRoot b = a

Tactic:
rcases eq_or_ne n 0 with rfl | hn

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
Goal:
a b : ℕ
h₁ : HPow.hPow (β := ℕ) a 0 ≤ b
h₂ : b < HPow.hPow (β := ℕ) (a + 1) 0
⊢ nthRoot 0 b = a

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
Goal:
n a b : ℕ
h₁ : a ^ n ≤ b
h₂ : b < (a + 1) ^ n
hn : n ≠ 0
⊢ a ≤ n.nthRoot b

Tactic:
simp only [← le_nthRoot_iff hn, ← nthRoot_lt_iff hn] at h₁ h₂

Premises used: Nat.nthRoot_lt_iff, Nat.le_nthRoot_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
Goal:
n a b : ℕ
h₁ : a ^ n ≤ b
h₂ : b < (a + 1) ^ n
hn : n ≠ 0
h₃ : a ≤ n.nthRoot b
⊢ n.nthRoot b < a + 1

Tactic:
simp only [← le_nthRoot_iff hn, ← nthRoot_lt_iff hn] at h₁ h₂

Premises used: Nat.nthRoot_lt_iff, Nat.le_nthRoot_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
Goal:
n a b : ℕ
hn : n ≠ 0
h₁ : a ≤ n.nthRoot b
h₂ : n.nthRoot b < a + 1
⊢ n.nthRoot b = a

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
Goal:
n a : ℕ
hn : n ≠ 0
mp : (∃ (x : ℕ), x ^ n = a) → n.nthRoot a ^ n = a
mpr : n.nthRoot a ^ n = a → ∃ (x : ℕ), x ^ n = a
⊢ (∃ (x : ℕ), x ^ n = a) ↔ n.nthRoot a ^ n = a

Tactic:
constructor
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
Goal:
n : ℕ
hn : n ≠ 0
x : ℕ
mp mp₁ : x ^ n = x ^ n
⊢ n.nthRoot (x ^ n) ^ n = x ^ n

Tactic:
rw [nthRoot_pow hn]

Premises used: Nat.nthRoot_pow
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
Goal:
n a : ℕ
hn : n ≠ 0
⊢ n.nthRoot a ^ n = a → ∃ (x : ℕ), x ^ n = a

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
Goal:
n a : ℕ
inl :
  (∃ (x : ℕ), HPow.hPow (β := ℕ) x 0 = a) ↔
    Eq (α := ℕ) 0 0 ∧ a = 1 ∨ Ne (α := ℕ) 0 0 ∧ HPow.hPow (β := ℕ) (nthRoot 0 a) 0 = a
inr : n ≠ 0 → ((∃ (x : ℕ), x ^ n = a) ↔ n = 0 ∧ a = 1 ∨ n ≠ 0 ∧ n.nthRoot a ^ n = a)
⊢ (∃ (x : ℕ), x ^ n = a) ↔ n = 0 ∧ a = 1 ∨ n ≠ 0 ∧ n.nthRoot a ^ n = a

Tactic:
rcases eq_or_ne n 0 with rfl | _

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
Goal:
a : ℕ
⊢ (∃ (x : ℕ), HPow.hPow (β := ℕ) x 0 = a) ↔
    Eq (α := ℕ) 0 0 ∧ a = 1 ∨ Ne (α := ℕ) 0 0 ∧ HPow.hPow (β := ℕ) (nthRoot 0 a) 0 = a

Tactic:
grind [exists_pow_eq_iff']

Premises used: Nat.exists_pow_eq_iff'
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
Goal:
n a : ℕ
h : n ≠ 0
⊢ (∃ (x : ℕ), x ^ n = a) ↔ n = 0 ∧ a = 1 ∨ n ≠ 0 ∧ n.nthRoot a ^ n = a

Tactic:
grind [exists_pow_eq_iff']

Premises used: Nat.exists_pow_eq_iff'
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y : ℝ
⊢ x.rpow y = x ^ y

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y : ℝ
⊢ x ^ y = ((↑x : ℂ) ^ (↑y : ℂ)).re

Tactic:
rfl

Premises used: Real.rpow, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
hx : 0 ≤ x
y : ℝ
pos : (↑x : ℂ) = 0 → (↑y : ℂ) = 0 → x = 0 → y = 0 → Complex.re 1 = 1
neg : (↑x : ℂ) = 0 → (↑y : ℂ) = 0 → x = 0 → ¬y = 0 → Complex.re 1 = 0
neg₁ : (↑x : ℂ) = 0 → (↑y : ℂ) = 0 → ¬x = 0 → Complex.re 1 = rexp (log x * y)
pos₁ : (↑x : ℂ) = 0 → ¬(↑y : ℂ) = 0 → x = 0 → y = 0 → Complex.re 0 = 1
neg₂ : (↑x : ℂ) = 0 → ¬(↑y : ℂ) = 0 → x = 0 → ¬y = 0 → Complex.re 0 = 0
neg₃ : (↑x : ℂ) = 0 → ¬(↑y : ℂ) = 0 → ¬x = 0 → Complex.re 0 = rexp (log x * y)
pos₂ : ¬(↑x : ℂ) = 0 → x = 0 → y = 0 → (Complex.exp (Complex.log (↑x : ℂ) * (↑y : ℂ))).re = 1
neg₄ : ¬(↑x : ℂ) = 0 → x = 0 → ¬y = 0 → (Complex.exp (Complex.log (↑x : ℂ) * (↑y : ℂ))).re = 0
neg₅ : ¬(↑x : ℂ) = 0 → ¬x = 0 → (Complex.exp (Complex.log (↑x : ℂ) * (↑y : ℂ))).re = rexp (log x * y)
⊢ (if (↑x : ℂ) = 0 then if (↑y : ℂ) = 0 then 1 else 0 else Complex.exp (Complex.log (↑x : ℂ) * (↑y : ℂ))).re =
    if x = 0 then if y = 0 then 1 else 0 else rexp (log x * y)

Tactic:
split_ifs
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
hx : 0 ≤ x
y : ℝ
h : (↑x : ℂ) = 0
h_1 : (↑y : ℂ) = 0
h_2 : x = 0
h_3 : y = 0
⊢ Complex.re 1 = 1

Tactic:
simp_all [(Complex.ofReal_log hx).symm, -Complex.ofReal_mul,
      (Complex.ofReal_mul _ _).symm, Complex.exp_ofReal_re, Complex.ofReal_eq_zero]

Premises used: Complex.ofReal_log, Complex.exp_ofReal_re, Complex.ofReal_eq_zero, Eq.symm, Complex.ofReal_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
hx : 0 ≤ x
y : ℝ
h : (↑x : ℂ) = 0
h_1 : (↑y : ℂ) = 0
h_2 : x = 0
h_3 : ¬y = 0
⊢ Complex.re 1 = 0

Tactic:
simp_all [(Complex.ofReal_log hx).symm, -Complex.ofReal_mul,
      (Complex.ofReal_mul _ _).symm, Complex.exp_ofReal_re, Complex.ofReal_eq_zero]

Premises used: Complex.ofReal_log, Complex.exp_ofReal_re, Complex.ofReal_eq_zero, Eq.symm, Complex.ofReal_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
hx : 0 ≤ x
y : ℝ
h : (↑x : ℂ) = 0
h_1 : (↑y : ℂ) = 0
h_2 : ¬x = 0
⊢ Complex.re 1 = rexp (log x * y)

Tactic:
simp_all [(Complex.ofReal_log hx).symm, -Complex.ofReal_mul,
      (Complex.ofReal_mul _ _).symm, Complex.exp_ofReal_re, Complex.ofReal_eq_zero]

Premises used: Complex.ofReal_log, Complex.exp_ofReal_re, Complex.ofReal_eq_zero, Eq.symm, Complex.ofReal_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
hx : 0 ≤ x
y : ℝ
h : (↑x : ℂ) = 0
h_1 : ¬(↑y : ℂ) = 0
h_2 : x = 0
h_3 : y = 0
⊢ Complex.re 0 = 1

Tactic:
simp_all [(Complex.ofReal_log hx).symm, -Complex.ofReal_mul,
      (Complex.ofReal_mul _ _).symm, Complex.exp_ofReal_re, Complex.ofReal_eq_zero]

Premises used: Complex.ofReal_log, Complex.exp_ofReal_re, Complex.ofReal_eq_zero, Eq.symm, Complex.ofReal_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
hx : 0 ≤ x
y : ℝ
h : (↑x : ℂ) = 0
h_1 : ¬(↑y : ℂ) = 0
h_2 : x = 0
h_3 : ¬y = 0
⊢ Complex.re 0 = 0

Tactic:
simp_all [(Complex.ofReal_log hx).symm, -Complex.ofReal_mul,
      (Complex.ofReal_mul _ _).symm, Complex.exp_ofReal_re, Complex.ofReal_eq_zero]

Premises used: Complex.ofReal_log, Complex.exp_ofReal_re, Complex.ofReal_eq_zero, Eq.symm, Complex.ofReal_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
hx : 0 ≤ x
y : ℝ
h : (↑x : ℂ) = 0
h_1 : ¬(↑y : ℂ) = 0
h_2 : ¬x = 0
⊢ Complex.re 0 = rexp (log x * y)

Tactic:
simp_all [(Complex.ofReal_log hx).symm, -Complex.ofReal_mul,
      (Complex.ofReal_mul _ _).symm, Complex.exp_ofReal_re, Complex.ofReal_eq_zero]

Premises used: Complex.ofReal_log, Complex.exp_ofReal_re, Complex.ofReal_eq_zero, Eq.symm, Complex.ofReal_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
hx : 0 ≤ x
y : ℝ
h : ¬(↑x : ℂ) = 0
h_1 : x = 0
h_2 : y = 0
⊢ (Complex.exp (Complex.log (↑x : ℂ) * (↑y : ℂ))).re = 1

Tactic:
simp_all [(Complex.ofReal_log hx).symm, -Complex.ofReal_mul,
      (Complex.ofReal_mul _ _).symm, Complex.exp_ofReal_re, Complex.ofReal_eq_zero]

Premises used: Complex.ofReal_log, Complex.exp_ofReal_re, Complex.ofReal_eq_zero, Eq.symm, Complex.ofReal_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
hx : 0 ≤ x
y : ℝ
h : ¬(↑x : ℂ) = 0
h_1 : x = 0
h_2 : ¬y = 0
⊢ (Complex.exp (Complex.log (↑x : ℂ) * (↑y : ℂ))).re = 0

Tactic:
simp_all [(Complex.ofReal_log hx).symm, -Complex.ofReal_mul,
      (Complex.ofReal_mul _ _).symm, Complex.exp_ofReal_re, Complex.ofReal_eq_zero]

Premises used: Complex.ofReal_log, Complex.exp_ofReal_re, Complex.ofReal_eq_zero, Eq.symm, Complex.ofReal_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
hx : 0 ≤ x
y : ℝ
h : ¬(↑x : ℂ) = 0
h_1 : ¬x = 0
⊢ (Complex.exp (Complex.log (↑x : ℂ) * (↑y : ℂ))).re = rexp (log x * y)

Tactic:
simp_all [(Complex.ofReal_log hx).symm, -Complex.ofReal_mul,
      (Complex.ofReal_mul _ _).symm, Complex.exp_ofReal_re, Complex.ofReal_eq_zero]

Premises used: Complex.ofReal_log, Complex.exp_ofReal_re, Complex.ofReal_eq_zero, Eq.symm, Complex.ofReal_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
hx : 0 < x
y : ℝ
rw : (if x = 0 then if y = 0 then 1 else 0 else rexp (log x * y)) = rexp (log x * y)
rw₁ rw₂ : rexp (log x * y) = rexp (log x * y)
⊢ x ^ y = rexp (log x * y)

Tactic:
rw [rpow_def_of_nonneg (le_of_lt hx), if_neg (ne_of_gt hx)]

Premises used: le_of_lt, ne_of_gt, Real.rpow_def_of_nonneg, if_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y : ℝ
rw : rexp (x * y) = rexp (log (rexp x) * y)
rw₁ rw₂ : rexp (x * y) = rexp (x * y)
⊢ rexp (x * y) = rexp x ^ y

Tactic:
rw [rpow_def_of_pos (exp_pos _), log_exp]

Premises used: Real.log_exp, Real.rpow_def_of_pos, Real.exp_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
n : ℤ
⊢ HPow.hPow (β := ℝ) x (↑n : ℝ) = x ^ n

Tactic:
simp only [rpow_def, ← Complex.ofReal_zpow, Complex.cpow_intCast, Complex.ofReal_intCast,
    Complex.ofReal_re]

Premises used: Complex.cpow_intCast, Complex.ofReal_zpow, Complex.ofReal_intCast, Complex.ofReal_re, Real.rpow_def
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
n : ℕ
⊢ HPow.hPow (β := ℝ) x (↑n : ℝ) = x ^ n

Tactic:
simpa using rpow_intCast x n

Premises used: Nat.cast, Real.rpow_intCast
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
n : ℕ
rw : HPow.hPow (β := ℝ) x (-(↑n : ℝ)) = HPow.hPow (β := ℝ) x (↑(-(↑n : ℤ)) : ℝ)
rw₁ : HPow.hPow (β := ℝ) x (-(↑n : ℝ)) = HPow.hPow (β := ℝ) x (-(↑(↑n : ℤ) : ℝ))
rw₂ rw₃ : HPow.hPow (β := ℝ) x (-(↑n : ℝ)) = HPow.hPow (β := ℝ) x (-(↑n : ℝ))
⊢ HPow.hPow (β := ℝ) x (-(↑n : ℝ)) = HPow.hPow (β := ℤ) x (-(↑n : ℤ))

Tactic:
rw [← rpow_intCast, Int.cast_neg, Int.cast_natCast]

Premises used: Int.cast_neg, Int.cast_natCast, Real.rpow_intCast
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
n : ℕ
inst : n.AtLeastTwo
⊢ HPow.hPow (β := ℝ) x (OfNat.ofNat n) = HPow.hPow (β := ℕ) x (OfNat.ofNat n)

Tactic:
rpow_natCast x n

Premises used: Real.rpow_natCast
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
n : ℕ
inst : n.AtLeastTwo
⊢ HPow.hPow (β := ℝ) x (-OfNat.ofNat n) = HPow.hPow (β := ℤ) x (-OfNat.ofNat n)

Tactic:
rpow_neg_natCast _ _

Premises used: Real.rpow_neg_natCast
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
rw : rexp (1 * x) = rexp x
rw₁ rw₂ : rexp x = rexp x
⊢ rexp 1 ^ x = rexp x

Tactic:
rw [← exp_mul, one_mul]

Premises used: Real.exp_mul, one_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
n : ℕ
rw : HPow.hPow (β := ℝ) (rexp 1) (↑n : ℝ) = rexp (↑n : ℝ)
rw₁ rw₂ : rexp (↑n : ℝ) = rexp (↑n : ℝ)
⊢ rexp 1 ^ n = rexp (↑n : ℝ)

Tactic:
rw [← rpow_natCast, exp_one_rpow]

Premises used: Real.exp_one_rpow, Real.rpow_natCast
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y : ℝ
hx : 0 ≤ x
simp : (if x = 0 then if y = 0 then 1 else 0 else rexp (log x * y)) = 0 ↔ x = 0 ∧ y ≠ 0
⊢ x ^ y = 0 ↔ x = 0 ∧ y ≠ 0

Tactic:
simp only [rpow_def_of_nonneg hx]

Premises used: Real.rpow_def_of_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y : ℝ
hx : 0 ≤ x
pos : x = 0 → y = 0 → (Eq (α := ℝ) 1 0 ↔ x = 0 ∧ y ≠ 0)
neg : x = 0 → ¬y = 0 → (Eq (α := ℝ) 0 0 ↔ x = 0 ∧ y ≠ 0)
neg₁ : ¬x = 0 → (rexp (log x * y) = 0 ↔ x = 0 ∧ y ≠ 0)
⊢ (if x = 0 then if y = 0 then 1 else 0 else rexp (log x * y)) = 0 ↔ x = 0 ∧ y ≠ 0

Tactic:
split_ifs
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y : ℝ
hx : 0 ≤ x
h : x = 0
h_1 : y = 0
⊢ Eq (α := ℝ) 1 0 ↔ x = 0 ∧ y ≠ 0

Tactic:
simp [*, exp_ne_zero]

Premises used: Real.exp_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y : ℝ
hx : 0 ≤ x
h : x = 0
h_1 : ¬y = 0
⊢ Eq (α := ℝ) 0 0 ↔ x = 0 ∧ y ≠ 0

Tactic:
simp [*, exp_ne_zero]

Premises used: Real.exp_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y : ℝ
hx : 0 ≤ x
h : ¬x = 0
⊢ rexp (log x * y) = 0 ↔ x = 0 ∧ y ≠ 0

Tactic:
simp [*, exp_ne_zero]

Premises used: Real.exp_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y : ℝ
hx : 0 ≤ x
hy : y ≠ 0
⊢ x ^ y = 0 ↔ x = 0

Tactic:
simp [rpow_eq_zero_iff_of_nonneg, *]

Premises used: Real.rpow_eq_zero_iff_of_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y : ℝ
hx : 0 ≤ x
hy : y ≠ 0
⊢ x ^ y ≠ 0 ↔ x ≠ 0

Tactic:
simp [hx, hy]
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
hx : x < 0
y : ℝ
rw : (Complex.exp (Complex.log (↑x : ℂ) * (↑y : ℂ))).re = rexp (log x * y) * cos (y * π)
hnc : ¬(↑x : ℂ) = 0
⊢ x ^ y = rexp (log x * y) * cos (y * π)

Tactic:
rw [rpow_def, Complex.cpow_def, if_neg]

Premises used: Complex.cpow_def, if_neg, Real.rpow_def
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
hx : x < 0
y : ℝ
simp : ((↑(log x) : ℂ) + (↑π : ℂ) * Complex.I) * (↑y : ℂ) = (↑(log x) : ℂ) * (↑y : ℂ) + (↑y : ℂ) * (↑π : ℂ) * Complex.I
⊢ Complex.log (↑x : ℂ) * (↑y : ℂ) = (↑(log (-x) * y) : ℂ) + (↑(y * π) : ℂ) * Complex.I

Tactic:
simp only [Complex.log, Complex.norm_real, norm_eq_abs, abs_of_neg hx, log_neg_eq_log,
        Complex.arg_ofReal_of_neg hx, Complex.ofReal_mul]

Premises used: Complex.log, Real.log_neg_eq_log, abs_of_neg, Complex.norm_real, Complex.arg_ofReal_of_neg, Real.norm_eq_abs, Complex.ofReal_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
hx : x < 0
y : ℝ
⊢ ((↑(log x) : ℂ) + (↑π : ℂ) * Complex.I) * (↑y : ℂ) = (↑(log x) : ℂ) * (↑y : ℂ) + (↑y : ℂ) * (↑π : ℂ) * Complex.I

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
hx : x < 0
y : ℝ
⊢ Complex.log (↑x : ℂ) * (↑y : ℂ) = (↑(log (-x) * y) : ℂ) + (↑(y * π) : ℂ) * Complex.I

Tactic:
have : Complex.log x * y = ↑(log (-x) * y) + ↑(y * π) * Complex.I := by
      simp only [Complex.log, Complex.norm_real, norm_eq_abs, abs_of_neg hx, log_neg_eq_log,
        Complex.arg_ofReal_of_neg hx, Complex.ofReal_mul]
      ring
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
hx : x < 0
y : ℝ
this : Complex.log (↑x : ℂ) * (↑y : ℂ) = (↑(log (-x) * y) : ℂ) + (↑(y * π) : ℂ) * Complex.I
rw :
  rexp (log x * y) * cos (y * π) + ((↑(rexp (log x * y) * sin (y * π)) : ℂ).re * 0 - 0 * Complex.I.im) =
    rexp (log x * y) * cos (y * π)
⊢ (Complex.exp (Complex.log (↑x : ℂ) * (↑y : ℂ))).re = rexp (log x * y) * cos (y * π)

Tactic:
rw [this, Complex.exp_add_mul_I, ← Complex.ofReal_exp, ← Complex.ofReal_cos, ←
      Complex.ofReal_sin, mul_add, ← Complex.ofReal_mul, ← mul_assoc, ← Complex.ofReal_mul,
      Complex.add_re, Complex.ofReal_re, Complex.mul_re, Complex.I_re, Complex.ofReal_im,
      Real.log_neg_eq_log]

Premises used: Complex.exp_add_mul_I, Complex.mul_re, Real.log_neg_eq_log, mul_assoc, Complex.add_re, Complex.ofReal_exp, Complex.I_re, Complex.ofReal_cos, Complex.ofReal_re, Complex.ofReal_sin, mul_add, Complex.ofReal_im, Complex.ofReal_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
hx : x < 0
y : ℝ
this : Complex.log (↑x : ℂ) * (↑y : ℂ) = (↑(log (-x) * y) : ℂ) + (↑(y * π) : ℂ) * Complex.I
⊢ rexp (log x * y) * cos (y * π) + ((↑(rexp (log x * y) * sin (y * π)) : ℂ).re * 0 - 0 * Complex.I.im) =
    rexp (log x * y) * cos (y * π)

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
hx : x < 0
y : ℝ
hnc : ¬x = 0
⊢ ¬(↑x : ℂ) = 0

Tactic:
rw [Complex.ofReal_eq_zero]

Premises used: Complex.ofReal_eq_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
hx : x < 0
y : ℝ
⊢ ¬x = 0

Tactic:
ne_of_lt hx

Premises used: ne_of_lt
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
hx : x < 0
y : ℝ
⊢ ¬x = 0

Tactic:
exact ne_of_lt hx

Premises used: ne_of_lt
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
hx : x ≤ 0
y : ℝ
pos : ∀ (h : x = 0), y = 0 → x ^ y = 1
neg : ∀ (h : x = 0), ¬y = 0 → x ^ y = 0
neg₁ : ∀ (h : ¬x = 0), x ^ y = rexp (log x * y) * cos (y * π)
⊢ x ^ y = if x = 0 then if y = 0 then 1 else 0 else rexp (log x * y) * cos (y * π)

Tactic:
split_ifs with h
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
hx : x ≤ 0
y : ℝ
h : x = 0
h_1 : y = 0
⊢ x ^ y = 1

Tactic:
simp [rpow_def, *]

Premises used: Real.rpow_def
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
hx : x ≤ 0
y : ℝ
h : x = 0
h_1 : ¬y = 0
⊢ x ^ y = 0

Tactic:
simp [rpow_def, *]

Premises used: Real.rpow_def
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
hx : x ≤ 0
y : ℝ
h : ¬x = 0
⊢ ((↑x : ℂ) ^ (↑y : ℂ)).re = rexp (log x * y) * cos (y * π)

Tactic:
rpow_def_of_neg (lt_of_le_of_ne hx h) _

Premises used: Real.rpow_def_of_neg, Real.rpow, lt_of_le_of_ne
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
hx : x ≤ 0
y : ℝ
h : ¬x = 0
⊢ ((↑x : ℂ) ^ (↑y : ℂ)).re = rexp (log x * y) * cos (y * π)

Tactic:
exact rpow_def_of_neg (lt_of_le_of_ne hx h) _

Premises used: Real.rpow_def_of_neg, lt_of_le_of_ne
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
hx : 0 < x
y : ℝ
rw : 0 < rexp (log x * y)
⊢ 0 < x ^ y

Tactic:
rw [rpow_def_of_pos hx]

Premises used: Real.rpow_def_of_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
hx : 0 < x
y : ℝ
⊢ 0 < rexp (log x * y)

Tactic:
apply exp_pos

Premises used: Real.exp_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
⊢ HPow.hPow (β := ℝ) x 0 = 1

Tactic:
simp [rpow_def]

Premises used: Real.rpow_def
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
⊢ 0 < HPow.hPow (β := ℝ) x 0

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
α : Type u_1
f : α → ℝ
h : ∀ (x : α), HPow.hPow (β := ℝ) f 0 x = 1 x
⊢ HPow.hPow (β := ℝ) f 0 = 1

Tactic:
ext
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
α : Type u_1
f : α → ℝ
x : α
⊢ HPow.hPow (β := ℝ) f 0 x = 1 x

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
h : x ≠ 0
⊢ HPow.hPow (α := ℝ) 0 x = 0

Tactic:
simp [rpow_def, *]

Premises used: Real.rpow_def
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x a : ℝ
mp : HPow.hPow (α := ℝ) 0 x = a → x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1
mpr : x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1 → HPow.hPow (α := ℝ) 0 x = a
⊢ HPow.hPow (α := ℝ) 0 x = a ↔ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1

Tactic:
constructor
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x a : ℝ
hyp : (HPow.hPow (α := ℂ) 0 (↑x : ℂ)).re = a
pos : ∀ (h : x = 0), x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1
neg : ∀ (h : ¬x = 0), x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1
⊢ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1

Tactic:
by_cases h : x = 0
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x a : ℝ
hyp : (HPow.hPow (α := ℂ) 0 (↑x : ℂ)).re = a
h : x = 0
pos : ∀ (hyp : (HPow.hPow (α := ℂ) 0 (↑0 : ℂ)).re = a), Ne (α := ℝ) 0 0 ∧ a = 0 ∨ Eq (α := ℝ) 0 0 ∧ a = 1
⊢ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1

Tactic:
subst h
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
a : ℝ
hyp : (HPow.hPow (α := ℂ) 0 (↑0 : ℂ)).re = a
⊢ 1 = a

Tactic:
simp only [Complex.one_re, Complex.ofReal_zero, Complex.cpow_zero] at hyp

Premises used: Complex.ofReal_zero, Complex.one_re, Complex.cpow_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
a : ℝ
hyp : 1 = a
⊢ Ne (α := ℝ) 0 0 ∧ a = 0 ∨ Eq (α := ℝ) 0 0 ∧ a = 1

Tactic:
Or.inr ⟨rfl, hyp.symm⟩

Premises used: And.intro, Eq.symm, Or.inr, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
a : ℝ
hyp : 1 = a
⊢ Ne (α := ℝ) 0 0 ∧ a = 0 ∨ Eq (α := ℝ) 0 0 ∧ a = 1

Tactic:
exact Or.inr ⟨rfl, hyp.symm⟩

Premises used: Or.inr
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x a : ℝ
hyp : (HPow.hPow (α := ℂ) 0 (↑x : ℂ)).re = a
h : ¬x = 0
⊢ Complex.re 0 = a

Tactic:
rw [Complex.zero_cpow (Complex.ofReal_ne_zero.mpr h)] at hyp

Premises used: Iff.mpr, Complex.ofReal_ne_zero, Complex.zero_cpow
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x a : ℝ
hyp : (HPow.hPow (α := ℂ) 0 (↑x : ℂ)).re = a
h : ¬x = 0
hyp₁ : Complex.re 0 = a
⊢ ¬x = 0

Tactic:
rw [Complex.zero_cpow (Complex.ofReal_ne_zero.mpr h)] at hyp

Premises used: Iff.mpr, Complex.ofReal_ne_zero, Complex.zero_cpow
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x a : ℝ
hyp : Complex.re 0 = a
h : ¬x = 0
⊢ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1

Tactic:
Or.inl ⟨h, hyp.symm⟩

Premises used: And.intro, Or.inl, Eq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x a : ℝ
hyp : Complex.re 0 = a
h : ¬x = 0
⊢ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1

Tactic:
exact Or.inl ⟨h, hyp.symm⟩

Premises used: Or.inl
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
h : x ≠ 0
⊢ HPow.hPow (α := ℝ) 0 x = 0

Tactic:
zero_rpow h

Premises used: Real.zero_rpow
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
h : x ≠ 0
⊢ HPow.hPow (α := ℝ) 0 x = 0

Tactic:
exact zero_rpow h

Premises used: Real.zero_rpow
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
⊢ HPow.hPow (α := ℝ) (β := ℝ) 0 0 = 1

Tactic:
rpow_zero _

Premises used: Real.rpow_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
⊢ HPow.hPow (α := ℝ) (β := ℝ) 0 0 = 1

Tactic:
exact rpow_zero _

Premises used: Real.rpow_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x a : ℝ
rw : a = HPow.hPow (α := ℝ) 0 x ↔ HPow.hPow (α := ℝ) 0 x = a
rw₁ rw₂ : HPow.hPow (α := ℝ) 0 x = a ↔ HPow.hPow (α := ℝ) 0 x = a
⊢ a = HPow.hPow (α := ℝ) 0 x ↔ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1

Tactic:
rw [← zero_rpow_eq_iff, eq_comm]

Premises used: Real.zero_rpow_eq_iff, eq_comm
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
⊢ HPow.hPow (β := ℝ) x 1 = x

Tactic:
simp [rpow_def]

Premises used: Real.rpow_def
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
α : Type u_1
f : α → ℝ
h : ∀ (x : α), HPow.hPow (β := ℝ) f 1 x = f x
⊢ HPow.hPow (β := ℝ) f 1 = f

Tactic:
ext
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
α : Type u_1
f : α → ℝ
x : α
⊢ HPow.hPow (β := ℝ) f 1 x = f x

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
⊢ HPow.hPow (α := ℝ) 1 x = 1

Tactic:
simp [rpow_def]

Premises used: Real.rpow_def
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
pos : ∀ (h : x = 0), HPow.hPow (α := ℝ) 0 x ≤ 1
neg : ∀ (h : ¬x = 0), HPow.hPow (α := ℝ) 0 x ≤ 1
⊢ HPow.hPow (α := ℝ) 0 x ≤ 1

Tactic:
by_cases h : x = 0
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
h : x = 0
⊢ HPow.hPow (α := ℝ) 0 x ≤ 1

Tactic:
simp [h, zero_le_one]

Premises used: zero_le_one
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
h : ¬x = 0
⊢ HPow.hPow (α := ℝ) 0 x ≤ 1

Tactic:
simp [h, zero_le_one]

Premises used: zero_le_one