awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
p : Nat.Primes
s : ℂ
hs : 1 < s.re
⊢ HPow.hPow (α := ℝ) 2 (-s).re ≤ HPow.hPow (α := ℝ) (β := ℝ) 2 (-1)

Tactic:
Real.rpow_le_rpow_of_exponent_le one_le_two <| (neg_lt_neg hs).le

Premises used: neg_lt_neg, LT.lt.le, one_le_two, Real.rpow_le_rpow_of_exponent_le
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
p : Nat.Primes
s : ℂ
hs : 1 < s.re
⊢ HPow.hPow (α := ℝ) 2 (-s).re ≤ HPow.hPow (α := ℝ) (β := ℝ) 2 (-1)

Tactic:
exact Real.rpow_le_rpow_of_exponent_le one_le_two <| (neg_lt_neg hs).le

Premises used: neg_lt_neg, LT.lt.le, one_le_two, Real.rpow_le_rpow_of_exponent_le
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
p : ℕ
hp : Nat.Prime p
s : ℂ
hs : 1 < s.re
⊢ 1 - HPow.hPow (α := ℂ) (↑p : ℂ) (-s) ≠ 0

Tactic:
sub_ne_zero_of_ne fun H ↦ ?_

Premises used: sub_ne_zero_of_ne
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
p : ℕ
hp : Nat.Prime p
s : ℂ
hs : 1 < s.re
refine : ∀ (H : 1 = HPow.hPow (α := ℂ) (↑p : ℂ) (-s)), False
⊢ 1 - HPow.hPow (α := ℂ) (↑p : ℂ) (-s) ≠ 0

Tactic:
refine sub_ne_zero_of_ne fun H ↦ ?_

Premises used: sub_ne_zero_of_ne
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
p : ℕ
hp : Nat.Prime p
s : ℂ
hs : 1 < s.re
H : 1 = HPow.hPow (α := ℂ) (↑p : ℂ) (-s)
⊢ ‖HPow.hPow (α := ℂ) (↑(↑(Subtype.mk (p := fun (p : ℕ) ↦ Nat.Prime p) p hp) : ℕ) : ℂ) (-s)‖ ≤ 1 / 2

Tactic:
have := norm_prime_cpow_le_one_half ⟨p, hp⟩ hs
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
p : ℕ
hp : Nat.Prime p
s : ℂ
hs : 1 < s.re
H : 1 = HPow.hPow (α := ℂ) (↑p : ℂ) (-s)
this : ‖HPow.hPow (α := ℂ) (↑p : ℂ) (-s)‖ ≤ 1 / 2
⊢ 1 ≤ 1 / 2

Tactic:
rw [← H, norm_one] at this

Premises used: NormOneClass.norm_one
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
p : ℕ
hp : Nat.Prime p
s : ℂ
hs : 1 < s.re
H : 1 = HPow.hPow (α := ℂ) (↑p : ℂ) (-s)
this : 1 ≤ 1 / 2
⊢ False

Tactic:
norm_num at this
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
n : ℕ
hn : 0 < n
w z : ℂ
h : w.re ≤ z.re
simp_rw : HPow.hPow (α := ℝ) (↑n : ℝ) w.re ≤ HPow.hPow (α := ℝ) (↑n : ℝ) z.re
⊢ ‖HPow.hPow (α := ℂ) (↑n : ℂ) w‖ ≤ ‖HPow.hPow (α := ℂ) (↑n : ℂ) z‖

Tactic:
simp_rw [norm_natCast_cpow_of_pos hn]

Premises used: Complex.norm_natCast_cpow_of_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
n : ℕ
hn : 0 < n
w z : ℂ
h : w.re ≤ z.re
⊢ LE.le (α := ℝ) 1 (↑n : ℝ)

Tactic:
exact_mod_cast hn
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
n : ℕ
hn : 0 < n
w z : ℂ
h : w.re ≤ z.re
⊢ HPow.hPow (α := ℝ) (↑n : ℝ) w.re ≤ HPow.hPow (α := ℝ) (↑n : ℝ) z.re

Tactic:
exact Real.rpow_le_rpow_of_exponent_le (by exact_mod_cast hn) h

Premises used: Real.rpow_le_rpow_of_exponent_le
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
n : ℕ
hn : 1 < n
w z : ℂ
simp_rw : HPow.hPow (α := ℝ) (↑n : ℝ) w.re ≤ HPow.hPow (α := ℝ) (↑n : ℝ) z.re ↔ w.re ≤ z.re
⊢ ‖HPow.hPow (α := ℂ) (↑n : ℂ) w‖ ≤ ‖HPow.hPow (α := ℂ) (↑n : ℂ) z‖ ↔ w.re ≤ z.re

Tactic:
simp_rw [norm_natCast_cpow_of_pos (Nat.zero_lt_of_lt hn),
    Real.rpow_le_rpow_left_iff (Nat.one_lt_cast.mpr hn)]

Premises used: Iff.mpr, Nat.zero_lt_of_lt, Real.rpow_le_rpow_left_iff, Complex.norm_natCast_cpow_of_pos, Nat.one_lt_cast
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
n : ℕ
ε : ℝ
hε : 0 < ε
inl : ‖log (↑0 : ℂ)‖ ≤ HPow.hPow (α := ℝ) (↑0 : ℝ) ε / ε
inr : ∀ (h : n > 0), ‖log (↑n : ℂ)‖ ≤ HPow.hPow (α := ℝ) (↑n : ℝ) ε / ε
⊢ ‖log (↑n : ℂ)‖ ≤ HPow.hPow (α := ℝ) (↑n : ℝ) ε / ε

Tactic:
rcases n.eq_zero_or_pos with rfl | h

Premises used: Nat.eq_zero_or_pos, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
ε : ℝ
hε : 0 < ε
inl : ‖log 0‖ ≤ HPow.hPow (α := ℝ) (↑0 : ℝ) ε / ε
inl₁ : ‖log 0‖ ≤ HPow.hPow (α := ℝ) 0 ε / ε
inl₂ : Norm.norm (E := ℂ) 0 ≤ HPow.hPow (α := ℝ) 0 ε / ε
inl₃ : 0 ≤ HPow.hPow (α := ℝ) 0 ε / ε
inl₄ : 0 ≤ 0 / ε
inl₅ inl₆ : LE.le (α := ℝ) 0 0
⊢ ‖log (↑0 : ℂ)‖ ≤ HPow.hPow (α := ℝ) (↑0 : ℝ) ε / ε

Tactic:
rw [Nat.cast_zero, Nat.cast_zero, log_zero, norm_zero, Real.zero_rpow hε.ne', zero_div]

Premises used: norm_zero, zero_div, Real.zero_rpow, LT.lt.ne', Nat.cast_zero, Complex.log_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
n : ℕ
ε : ℝ
hε : 0 < ε
h : n > 0
⊢ LE.le (α := ℝ) 1 (↑n : ℝ)

Tactic:
exact_mod_cast Nat.one_le_of_lt h.lt

Premises used: GT.gt.lt, Nat.one_le_of_lt
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
n : ℕ
ε : ℝ
hε : 0 < ε
h : n > 0
inr : Real.log (↑n : ℝ) ≤ HPow.hPow (α := ℝ) (↑n : ℝ) ε / ε
⊢ ‖log (↑n : ℂ)‖ ≤ HPow.hPow (α := ℝ) (↑n : ℝ) ε / ε

Tactic:
rw [← natCast_log, norm_real, norm_of_nonneg <| Real.log_nonneg <| by
    exact_mod_cast Nat.one_le_of_lt h.lt]

Premises used: Complex.natCast_log, Complex.norm_real, Real.log_nonneg, Real.norm_of_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
n : ℕ
ε : ℝ
hε : 0 < ε
h : n > 0
⊢ Real.log (↑n : ℝ) ≤ HPow.hPow (α := ℝ) (↑n : ℝ) ε / ε

Tactic:
Real.log_natCast_le_rpow_div n hε

Premises used: Real.log_natCast_le_rpow_div
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
n : ℕ
ε : ℝ
hε : 0 < ε
h : n > 0
⊢ Real.log (↑n : ℝ) ≤ HPow.hPow (α := ℝ) (↑n : ℝ) ε / ε

Tactic:
exact Real.log_natCast_le_rpow_div n hε

Premises used: Real.log_natCast_le_rpow_div
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
inl : ∀ (h : 0 ≤ x), √x = x ^ (1 / 2)
inr : ∀ (h : x < 0), √x = x ^ (1 / 2)
⊢ √x = x ^ (1 / 2)

Tactic:
obtain h | h := le_or_gt 0 x

Premises used: le_or_gt, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
h : 0 ≤ x
inl : x = x ^ (1 / 2 * (↑2 : ℝ))
⊢ √x = x ^ (1 / 2)

Tactic:
rw [← mul_self_inj_of_nonneg (sqrt_nonneg _) (rpow_nonneg h _), mul_self_sqrt h, ← sq,
      ← rpow_natCast, ← rpow_mul h]

Premises used: mul_self_inj_of_nonneg, Real.mul_self_sqrt, sq, Real.rpow_nonneg, Real.sqrt_nonneg, Real.rpow_mul, Real.rpow_natCast
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
h : 0 ≤ x
⊢ x = x ^ (1 / 2 * (↑2 : ℝ))

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
h : x < 0
⊢ 1 / 2 * π = π / 2

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
h : x < 0
⊢ 1 / 2 * π = π / 2

Tactic:
have : 1 / (2 : ℝ) * π = π / (2 : ℝ) := by ring
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
h : x < 0
this : 1 / 2 * π = π / 2
inr : 0 = x ^ (1 / 2)
inr₁ : 0 = rexp (log x * (1 / 2)) * cos (1 / 2 * π)
inr₂ : 0 = rexp (log x * (1 / 2)) * cos (π / 2)
inr₃ : 0 = rexp (log x * (1 / 2)) * 0
inr₄ inr₅ : Eq (α := ℝ) 0 0
⊢ √x = x ^ (1 / 2)

Tactic:
rw [sqrt_eq_zero_of_nonpos h.le, rpow_def_of_neg h, this, cos_pi_div_two, mul_zero]

Premises used: Real.sqrt_eq_zero_of_nonpos, Real.cos_pi_div_two, Real.rpow_def_of_neg, LT.lt.le, MulZeroClass.mul_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x r : ℝ
hx : 0 ≤ x
rw : x ^ (r / 2) = x ^ (1 / 2 * r)
⊢ x ^ (r / 2) = √x ^ r

Tactic:
rw [sqrt_eq_rpow, ← rpow_mul hx]

Premises used: Real.rpow_mul, Real.sqrt_eq_rpow
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x r : ℝ
hx : 0 ≤ x
e_a : r / 2 = 1 / 2 * r
⊢ x ^ (r / 2) = x ^ (1 / 2 * r)

Tactic:
congr
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x r : ℝ
hx : 0 ≤ x
⊢ r / 2 = 1 / 2 * r

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℂ
hx : 0 ≤ ‖x‖
hl : -π ≤ x.arg
hr : x.arg ≤ π
⊢ (HPow.hPow (β := ℂ) x 2⁻¹).re = √((‖x‖ + x.re) / 2)

Tactic:
rw [← ofReal_ofNat, ← ofReal_inv, cpow_ofReal_re, ← div_eq_mul_inv, ← one_div,
    ← Real.sqrt_eq_rpow, cos_half, ← sqrt_mul, ← mul_div_assoc, mul_add, mul_one, norm_mul_cos_arg]

Premises used: mul_div_assoc, Complex.norm_mul_cos_arg, Complex.cpow_ofReal_re, Real.sqrt_mul, div_eq_mul_inv, Real.cos_half, one_div, mul_add, mul_one, Complex.ofReal_ofNat, Complex.ofReal_inv, Real.sqrt_eq_rpow
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℂ
⊢ 0 ≤ ‖x‖

Tactic:
norm_nonneg _

Premises used: norm_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℂ
⊢ -π ≤ x.arg

Tactic:
(neg_pi_lt_arg _).le

Premises used: LT.lt.le, Complex.neg_pi_lt_arg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℂ
⊢ x.arg ≤ π

Tactic:
arg_le_pi _

Premises used: Complex.arg_le_pi
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℂ
⊢ 0 ≤ ‖x‖

Tactic:
exacts [norm_nonneg _, (neg_pi_lt_arg _).le, arg_le_pi _]

Premises used: Complex.arg_le_pi, LT.lt.le, Complex.neg_pi_lt_arg, norm_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℂ
hx : 0 ≤ x.im
hl : 0 ≤ x.arg
hr : x.arg ≤ 2 * π
⊢ (HPow.hPow (β := ℂ) x 2⁻¹).im = √((‖x‖ - x.re) / 2)

Tactic:
rw [← ofReal_ofNat, ← ofReal_inv, cpow_ofReal_im, ← div_eq_mul_inv, ← one_div,
    ← Real.sqrt_eq_rpow, sin_half_eq_sqrt, ← sqrt_mul (norm_nonneg _), ← mul_div_assoc, mul_sub,
    mul_one, norm_mul_cos_arg]

Premises used: mul_sub, mul_div_assoc, Complex.norm_mul_cos_arg, Real.sqrt_mul, div_eq_mul_inv, one_div, Complex.cpow_ofReal_im, mul_one, Complex.ofReal_ofNat, Complex.ofReal_inv, norm_nonneg, Real.sqrt_eq_rpow, Real.sin_half_eq_sqrt
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℂ
hx hl hl₁ hl₂ hl₃ : 0 ≤ x.im
⊢ 0 ≤ x.arg

Tactic:
rwa [arg_nonneg_iff]

Premises used: Complex.arg_nonneg_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℂ
hx : 0 ≤ x.im
linarith : 2 * π < x.arg → 2 * π - x.arg + (0 - π) + (x.arg - π) = 0
⊢ x.arg ≤ 2 * π

Tactic:
linarith [pi_pos, arg_le_pi x]

Premises used: Complex.arg_le_pi, Real.pi_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℂ
hx : x.im < 0
hl : -(2 * π) ≤ x.arg
hr : x.arg ≤ 0
⊢ (HPow.hPow (β := ℂ) x 2⁻¹).im = -√((‖x‖ - x.re) / 2)

Tactic:
rw [← ofReal_ofNat, ← ofReal_inv, cpow_ofReal_im, ← div_eq_mul_inv, ← one_div,
    ← Real.sqrt_eq_rpow, sin_half_eq_neg_sqrt, mul_neg, ← sqrt_mul (norm_nonneg _),
    ← mul_div_assoc, mul_sub, mul_one, norm_mul_cos_arg]

Premises used: mul_sub, mul_div_assoc, Complex.norm_mul_cos_arg, Real.sqrt_mul, div_eq_mul_inv, Real.sin_half_eq_neg_sqrt, one_div, Complex.cpow_ofReal_im, mul_one, Complex.ofReal_ofNat, Complex.ofReal_inv, norm_nonneg, Real.sqrt_eq_rpow, mul_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℂ
hx : x.im < 0
linarith : x.arg < -(2 * π) → x.arg - -(2 * π) + (0 - π) + (-π - x.arg) = 0
⊢ -(2 * π) ≤ x.arg

Tactic:
linarith [pi_pos, neg_pi_lt_arg x]

Premises used: Real.pi_pos, Complex.neg_pi_lt_arg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℂ
hx : x.im < 0
⊢ x.arg ≤ 0

Tactic:
(arg_neg_iff.2 hx).le

Premises used: Iff.mpr, LT.lt.le, Complex.arg_neg_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℂ
hx : x.im < 0
⊢ x.arg ≤ 0

Tactic:
exact (arg_neg_iff.2 hx).le

Premises used: Iff.mpr, LT.lt.le, Complex.arg_neg_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℂ
rw : |(x ^ (↑2 : ℂ)⁻¹).im| = √((‖x‖ - x.re) / 2)
rw₁ : |(x ^ (↑2⁻¹ : ℂ)).im| = √((‖x‖ - x.re) / 2)
rw₂ : |HPow.hPow (β := ℝ) ‖x‖ 2⁻¹ * Real.sin (x.arg * 2⁻¹)| = √((‖x‖ - x.re) / 2)
rw₃ : |HPow.hPow (β := ℝ) ‖x‖ 2⁻¹ * Real.sin (x.arg / 2)| = √((‖x‖ - x.re) / 2)
rw₄ : |‖x‖ ^ HDiv.hDiv (α := ℝ) 1 2 * Real.sin (x.arg / 2)| = √((‖x‖ - x.re) / 2)
rw₅ : |√‖x‖ * Real.sin (x.arg / 2)| = √((‖x‖ - x.re) / 2)
rw₆ : |√‖x‖| * |Real.sin (x.arg / 2)| = √((‖x‖ - x.re) / 2)
rw₇ : √‖x‖ * |Real.sin (x.arg / 2)| = √((‖x‖ - x.re) / 2)
rw₈ : √‖x‖ * √((1 - Real.cos x.arg) / 2) = √((‖x‖ - x.re) / 2)
rw₉ : √(‖x‖ * ((1 - Real.cos x.arg) / 2)) = √((‖x‖ - x.re) / 2)
rw₁₀ : √(‖x‖ * (1 - Real.cos x.arg) / 2) = √((‖x‖ - x.re) / 2)
rw₁₁ : √((‖x‖ * 1 - ‖x‖ * Real.cos x.arg) / 2) = √((‖x‖ - x.re) / 2)
rw₁₂ : √((‖x‖ - ‖x‖ * Real.cos x.arg) / 2) = √((‖x‖ - x.re) / 2)
rw₁₃ rw₁₄ : √((‖x‖ - x.re) / 2) = √((‖x‖ - x.re) / 2)
⊢ |(HPow.hPow (β := ℂ) x 2⁻¹).im| = √((‖x‖ - x.re) / 2)

Tactic:
rw [← ofReal_ofNat, ← ofReal_inv, cpow_ofReal_im, ← div_eq_mul_inv, ← one_div,
    ← Real.sqrt_eq_rpow, abs_mul, abs_of_nonneg (sqrt_nonneg _), abs_sin_half,
    ← sqrt_mul (norm_nonneg _), ← mul_div_assoc, mul_sub, mul_one, norm_mul_cos_arg]

Premises used: mul_sub, mul_div_assoc, Complex.norm_mul_cos_arg, abs_mul, Real.sqrt_mul, Real.abs_sin_half, div_eq_mul_inv, one_div, Complex.cpow_ofReal_im, abs_of_nonneg, mul_one, Real.sqrt_nonneg, Complex.ofReal_ofNat, Complex.ofReal_inv, norm_nonneg, Real.sqrt_eq_rpow
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
⊢ 0 < (HPow.hPow (α := ℂ) (↑n : ℂ) (↑x : ℂ))⁻¹

Tactic:
RCLike.inv_pos_of_pos ?_

Premises used: RCLike.inv_pos_of_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
refine : 0 < HPow.hPow (α := ℂ) (↑n : ℂ) (↑x : ℂ)
⊢ 0 < (HPow.hPow (α := ℂ) (↑n : ℂ) (↑x : ℂ))⁻¹

Tactic:
refine RCLike.inv_pos_of_pos ?_

Premises used: RCLike.inv_pos_of_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
rw : 0 < (↑(HPow.hPow (α := ℝ) (↑n : ℝ) x) : ℂ)
⊢ 0 < HPow.hPow (α := ℂ) (↑n : ℂ) (↑x : ℂ)

Tactic:
rw [show (n : ℂ) ^ (x : ℂ) = (n : ℝ) ^ (x : ℂ) from rfl, ← ofReal_cpow n.cast_nonneg']

Premises used: Complex.ofReal_cpow, Nat.cast_nonneg', rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
⊢ 0 < (↑(HPow.hPow (α := ℝ) (↑n : ℝ) x) : ℂ)

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

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

Premises used: Mathlib.Meta.NormNum.IsNat.out, Real.rpow_natCast
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
b : ℝ
n : ℕ
h : IsInt b (Int.negOfNat n)
a : ℝ
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, Real.rpow_intCast, Int.negOfNat_eq, zpow_neg, Int.ofNat_eq_natCast, zpow_natCast]

Premises used: zpow_natCast, Int.ofNat_eq_natCast, zpow_neg, Real.rpow_intCast, Mathlib.Meta.NormNum.IsInt.out, Int.negOfNat_eq
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
a 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 (α := ℝ) (↑m : ℝ) b) r
⊢ IsNat (a ^ b) r

Tactic:
rcases ha with ⟨rfl⟩

Premises used: rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
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 (α := ℝ) (↑m : ℝ) b = (↑r : ℝ)
⊢ IsNat (HPow.hPow (α := ℝ) (↑m : ℝ) b) r

Tactic:
constructor
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
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.Real
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
out : LE.le (α := ℝ) 0 (↑r : ℝ)
out₁ : d ≠ 0
out₂ : LE.le (α := ℝ) 0 (↑m : ℝ)
⊢ HPow.hPow (α := ℝ) (↑m : ℝ) b = (↑r : ℝ)

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

Premises used: Mathlib.Meta.NormNum.IsNNRat.to_eq, Real.pow_rpow_inv_natCast, div_eq_mul_inv, Nat.cast_pow, rfl, Real.rpow_natCast_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
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
⊢ LE.le (α := ℝ) 0 (↑r : ℝ)

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
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.Real
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
⊢ LE.le (α := ℝ) 0 (↑m : ℝ)

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

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

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

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

Tactic:
apply IsNNRat.of_raw

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

Tactic:
rw [← hden.1]

Premises used: Mathlib.Meta.NormNum.IsNat.out
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
a b : ℝ
na da : ℕ
ha : IsNNRat a na da
nr dr : ℕ
hnum : IsNat (HPow.hPow (α := ℝ) (↑na : ℝ) b) nr
hden : IsNat (HPow.hPow (α := ℝ) (↑da : ℝ) b) dr
apply : LT.lt (α := ℝ) 0 (↑da : ℝ)
⊢ HPow.hPow (α := ℝ) (↑da : ℝ) b ≠ 0

Tactic:
apply (Real.rpow_pos_of_pos _ _).ne'

Premises used: Real.rpow_pos_of_pos, LT.lt.ne'
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
a b : ℝ
na da : ℕ
ha : IsNNRat a na da
nr dr : ℕ
hnum : IsNat (HPow.hPow (α := ℝ) (↑na : ℝ) b) nr
hden : IsNat (HPow.hPow (α := ℝ) (↑da : ℝ) b) dr
⊢ LT.lt (α := ℝ) 0 (↑da : ℝ)

Tactic:
lt_of_le_of_ne' da.cast_nonneg ha.den_nz

Premises used: Mathlib.Meta.NormNum.IsNNRat.den_nz, Nat.cast_nonneg, lt_of_le_of_ne'
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
a b : ℝ
na da : ℕ
ha : IsNNRat a na da
nr dr : ℕ
hnum : IsNat (HPow.hPow (α := ℝ) (↑na : ℝ) b) nr
hden : IsNat (HPow.hPow (α := ℝ) (↑da : ℝ) b) dr
⊢ LT.lt (α := ℝ) 0 (↑da : ℝ)

Tactic:
exact lt_of_le_of_ne' da.cast_nonneg ha.den_nz

Premises used: Mathlib.Meta.NormNum.IsNNRat.den_nz, Nat.cast_nonneg, lt_of_le_of_ne'
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
a b : ℝ
n d : ℕ
hb : IsRat b (Int.negOfNat 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 [← Real.rpow_neg_eq_inv_rpow, hb.neg_to_eq rfl rfl]

Premises used: Real.rpow_neg_eq_inv_rpow, rfl, Mathlib.Meta.NormNum.IsRat.neg_to_eq
-- Module: Mathlib.Analysis.SpecialFunctions.Sigmoid
Goal:
x : ℝ
⊢ x.sigmoid = (1 + rexp (-x))⁻¹

Tactic:
rfl

Premises used: Real.sigmoid, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Sigmoid
Goal:
⊢ sigmoid 0 = 2⁻¹

Tactic:
norm_num [sigmoid]

Premises used: Real.sigmoid
-- Module: Mathlib.Analysis.SpecialFunctions.Sigmoid
Goal:
x : ℝ
⊢ 0 < (1 + rexp (-x))⁻¹

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Sigmoid
Goal:
x : ℝ
⊢ 0 ≤ x.sigmoid

Tactic:
(sigmoid_pos x).le

Premises used: Real.sigmoid_pos, LT.lt.le
-- Module: Mathlib.Analysis.SpecialFunctions.Sigmoid
Goal:
x : ℝ
⊢ x.sigmoid < 1

Tactic:
inv_lt_one_of_one_lt₀ <| (lt_add_iff_pos_right 1).mpr <| exp_pos _

Premises used: Iff.mpr, lt_add_iff_pos_right, inv_lt_one_of_one_lt₀, Real.sigmoid, OfNat.ofNat, Real.exp_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Sigmoid
Goal:
x : ℝ
⊢ x.sigmoid ≤ 1

Tactic:
(sigmoid_lt_one x).le

Premises used: LT.lt.le, Real.sigmoid_lt_one
-- Module: Mathlib.Analysis.SpecialFunctions.Sigmoid
Goal:
a b : ℝ
hab : a < b
hb : 0 < 1 + rexp (-b)
⊢ (1 + rexp (-a))⁻¹ < (1 + rexp (-b))⁻¹

Tactic:
gcongr
-- Module: Mathlib.Analysis.SpecialFunctions.Sigmoid
Goal:
a b : ℝ
⊢ a.sigmoid ≤ b.sigmoid ↔ a ≤ b

Tactic:
sigmoid_strictMono.le_iff_le

Premises used: StrictMono.le_iff_le, Real.sigmoid_strictMono
-- Module: Mathlib.Analysis.SpecialFunctions.Sigmoid
Goal:
a b : ℝ
⊢ a ≤ b → a.sigmoid ≤ b.sigmoid

Tactic:
sigmoid_le_iff.mpr

Premises used: Iff.mpr, Real.sigmoid_le_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Sigmoid
Goal:
a b : ℝ
⊢ a.sigmoid < b.sigmoid ↔ a < b

Tactic:
sigmoid_strictMono.lt_iff_lt

Premises used: StrictMono.lt_iff_lt, Real.sigmoid_strictMono
-- Module: Mathlib.Analysis.SpecialFunctions.Sigmoid
Goal:
a b : ℝ
⊢ a < b → a.sigmoid < b.sigmoid

Tactic:
sigmoid_lt_iff.mpr

Premises used: Iff.mpr, Real.sigmoid_lt_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Sigmoid
Goal:
⊢ Monotone sigmoid

Tactic:
sigmoid_strictMono.monotone

Premises used: StrictMono.monotone, Real.sigmoid_strictMono
-- Module: Mathlib.Analysis.SpecialFunctions.Sigmoid
Goal:
⊢ Function.Injective sigmoid

Tactic:
sigmoid_strictMono.injective

Premises used: StrictMono.injective, Real.sigmoid_strictMono
-- Module: Mathlib.Analysis.SpecialFunctions.Sigmoid
Goal:
a b : ℝ
⊢ a.sigmoid = b.sigmoid ↔ a = b

Tactic:
sigmoid_injective.eq_iff

Premises used: Function.Injective.eq_iff, Real.sigmoid_injective
-- Module: Mathlib.Analysis.SpecialFunctions.Sigmoid
Goal:
x : ℝ
field_simp : 1 + rexp (-x) = (1 + rexp x) * (1 + rexp (-x) - 1)
⊢ (1 + rexp (- -x))⁻¹ = 1 - (1 + rexp (-x))⁻¹

Tactic:
field_simp
-- Module: Mathlib.Analysis.SpecialFunctions.Sigmoid
Goal:
x : ℝ
⊢ 1 + rexp (-x) = (1 + rexp x) * (1 + rexp (-x) - 1)

Tactic:
simp [add_mul, ← Real.exp_add, add_comm (1 : ℝ)]

Premises used: add_mul, add_comm, OfNat.ofNat, Real.exp_add
-- Module: Mathlib.Analysis.SpecialFunctions.Sigmoid
Goal:
x : ℝ
rw : (1 + rexp (-x))⁻¹ * rexp (-x) = 1 - (1 + rexp (-x))⁻¹
⊢ x.sigmoid * rexp (-x) = (-x).sigmoid

Tactic:
rw [sigmoid_neg, sigmoid_def]

Premises used: Real.sigmoid_neg, Real.sigmoid_def
-- Module: Mathlib.Analysis.SpecialFunctions.Sigmoid
Goal:
x : ℝ
⊢ (1 + rexp (-x))⁻¹ * rexp (-x) = 1 - (1 + rexp (-x))⁻¹

Tactic:
field
-- Module: Mathlib.Analysis.SpecialFunctions.Sigmoid
Goal:
⊢ range sigmoid = Ioo 0 1

Tactic:
subset_antisymm ?_ fun x hx ↦ ?_

Premises used: subset_antisymm
-- Module: Mathlib.Analysis.SpecialFunctions.Sigmoid
Goal:
refine_1 : range sigmoid ⊆ Ioo 0 1
refine_2 : ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Ioo 0 1) x), x ∈ range sigmoid
⊢ range sigmoid = Ioo 0 1

Tactic:
refine subset_antisymm ?_ fun x hx ↦ ?_

Premises used: subset_antisymm
-- Module: Mathlib.Analysis.SpecialFunctions.Sigmoid
Goal:
x : ℝ
⊢ 0 < x.sigmoid ∧ x.sigmoid < 1

Tactic:
bound
-- Module: Mathlib.Analysis.SpecialFunctions.Sigmoid
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioo 0 1) x
rwa : 1 < x⁻¹
rwa₁ rwa₂ rwa₃ rwa₄ : 0 < x ∧ x < 1
⊢ 0 < x⁻¹ - 1

Tactic:
rwa [sub_pos, one_lt_inv_iff₀]

Premises used: sub_pos, one_lt_inv_iff₀
-- Module: Mathlib.Analysis.SpecialFunctions.Sigmoid
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioo 0 1) x
⊢ 0 < x⁻¹ - 1

Tactic:
replace hx : 0 < x⁻¹ - 1 := by rwa [sub_pos, one_lt_inv_iff₀]
-- Module: Mathlib.Analysis.SpecialFunctions.Sigmoid
Goal:
x : ℝ
hx : 0 < x⁻¹ - 1
⊢ (-log (x⁻¹ - 1)).sigmoid = x

Tactic:
simp [sigmoid_def, exp_log hx]

Premises used: Real.sigmoid_def, Real.exp_log
-- Module: Mathlib.Analysis.SpecialFunctions.Sigmoid
Goal:
x : ℝ
hx : 0 < x⁻¹ - 1
⊢ x ∈ range sigmoid

Tactic:
exact ⟨-(log (x⁻¹ - 1)), by simp [sigmoid_def, exp_log hx]⟩
-- Module: Mathlib.Analysis.SpecialFunctions.Sigmoid
Goal:
⊢ HAdd.hAdd (α := ℝ) 1 0 ≠ 0

Tactic:
norm_num
-- Module: Mathlib.Analysis.SpecialFunctions.Sigmoid
Goal:
⊢ Tendsto sigmoid atTop (𝓝 1)

Tactic:
simpa using Real.tendsto_exp_comp_nhds_zero.mpr tendsto_neg_atTop_atBot |>.const_add 1 |>.inv₀ <|
    by norm_num

Premises used: Iff.mpr, Real.tendsto_exp_comp_nhds_zero, Filter.tendsto_neg_atTop_atBot, Filter.Tendsto.inv₀, Filter.Tendsto.const_add, OfNat.ofNat