mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℝ
hx : 0 < x
⊢ x + 1 < 1 + x + x ^ 2 / 2

Tactic:
nlinarith

Goal state after:
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
n j : ℕ
hn : 0 < n
⊢ ∑ m ∈ range (j - n), 1 / ↑(m + n).factorial ≤ ∑ m ∈ range (j - n), (↑n.factorial * ↑n.succ ^ m)⁻¹

Tactic:
by
      simp_rw [one_div]
      gcongr
      rw [← Nat.cast_pow, ← Nat.cast_mul, Nat.cast_le, add_comm]
      exact Nat.factorial_mul_pow_le_factorial

Goal state after:
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: case e_f
x : ℂ
n j : ℕ
hj : j ≥ n
i : ℕ
⊢ ‖x ^ i / ↑i.factorial‖ = ‖x‖ ^ i / ↑i.factorial

Tactic:
simp [Complex.norm_pow, Complex.norm_natCast]

Goal state after:
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℂ
n j : ℕ
hj : j ≥ n
⊢ ↑(cauSeqNorm (exp' x - const norm (∑ m ∈ range n, x ^ m / ↑m.factorial))) j ≤
    ↑(const abs (Real.exp ‖x‖ - ∑ m ∈ range n, ‖x‖ ^ m / ↑m.factorial)) j

Tactic:
calc ‖(∑ m ∈ range j, x ^ m / m.factorial) - ∑ m ∈ range n, x ^ m / m.factorial‖
  _ ≤ (∑ m ∈ range j, ‖x‖ ^ m / m.factorial) - ∑ m ∈ range n, ‖x‖ ^ m / m.factorial := by
    rw [sum_range_sub_sum_range hj, sum_range_sub_sum_range hj]
    refine (IsAbsoluteValue.abv_sum norm ..).trans_eq ?_
    congr with i
    simp [Complex.norm_pow, Complex.norm_natCast]
  _ ≤ Real.exp ‖x‖ - ∑ m ∈ range n, ‖x‖ ^ m / m.factorial := by
    gcongr
    exact Real.sum_le_exp_of_nonneg (norm_nonneg _) _

Goal state after:
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℂ
n j : ℕ
hj : j ≥ n
⊢ ‖∑ m ∈ Ico n j, x ^ m / ↑m.factorial‖ = ‖∑ m ∈ Ico n j, x ^ n * (x ^ (m - n) / ↑m.factorial)‖

Tactic:
by
      refine congr_arg norm (sum_congr rfl fun m hm => ?_)
      rw [mem_Ico] at hm
      rw [← mul_div_assoc, ← pow_add, add_tsub_cancel_of_le hm.1]

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
l : Filter α
f g h : α → 𝕜
c : ℝ
hf : ∀ᶠ (x : α) in l, f x ≠ 0
⊢ IsBigOWith c l (fun x ↦ f x * g x) h ↔ IsBigOWith c l g fun x ↦ h x / f x

Tactic:
rw [isBigOWith_iff, isBigOWith_iff]
  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩ <;>
  · refine h.congr <| Eventually.mp hf <| Eventually.of_forall fun x hx ↦ ?_
    rw [norm_mul, norm_div, ← mul_div_assoc, le_div_iff₀' (norm_pos_iff.mpr hx)]

Goal state after:
Module: Mathlib.Analysis.Normed.Ring.InfiniteSum

Goal state before:
pp: R : Type u_1
inst✝ : NormedRing R
f g : ℕ → R
hf : Summable fun x ↦ ‖f x‖
h'f : Summable f
hg : Summable fun x ↦ ‖g x‖
h'g : Summable g
⊢ Summable fun n ↦ ∑ k ∈ range (n + 1), f k * g (n - k)

Tactic:
by
  simp_rw [← sum_antidiagonal_eq_sum_range_succ fun k l => f k * g l]
  exact summable_sum_mul_antidiagonal_of_summable_norm' hf h'f hg h'g

Goal state after:
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℝ
h1 : 0 < x
h2 : x < 1
H : 0 < 1 - (1 + x + x ^ 2) * (1 - x)
⊢ 1 + x + x ^ 2 / 2 + x ^ 3 * 4 / 18 ≤ 1 + x + x ^ 2

Tactic:
nlinarith

Goal state after:
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℝ
h1 : 0 < x
h2 : x < 1
H : 0 < 1 - (1 + x + x ^ 2) * (1 - x)
⊢ (1 + x + x ^ 2) * (1 - x) < 1

Tactic:
nlinarith

Goal state after:
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℝ
h1 : 0 < x
h2 : x < 1
H : 0 < 1 - (1 + x + x ^ 2) * (1 - x)
⊢ 0 < 1 - x

Tactic:
nlinarith

Goal state after:
Module: Mathlib.Algebra.Order.CauSeq.BigOperators

Goal state before:
pp: α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : Archimedean α
f : ℕ → α
a : α
m : ℕ
ham : ∀ n ≥ m, |f n| ≤ a
hnm : ∀ n ≥ m, f n.succ ≤ f n
ε : α
ε0 : ε > 0
k : ℕ
hk : a ≤ k • ε
h : ∃ l, ∀ n ≥ m, a - l • ε < f n
l : ℕ := Nat.find h
hl : ∀ n ≥ m, f n > a - l • ε
hl0 : l = 0
⊢ a < f m

Tactic:
have := hl m (le_refl m); simpa [hl0] using this

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
E : Type u_3
inst✝¹ : Norm E
F : Type u_4
inst✝ : Norm F
e : OpenPartialHomeomorph α β
b : β
hb : b ∈ e.target
f : β → E
g : β → F
⊢ (∃ c, IsBigOWith c (𝓝 b) f g) ↔ ∃ c, IsBigOWith c (𝓝 (↑e.symm b)) (f ∘ ↑e) (g ∘ ↑e)

Tactic:
exact exists_congr fun C => e.isBigOWith_congr hb

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: α : Type u_1
inst✝² : NormedRing α
inst✝¹ : NormSMulClass ℤ α
inst✝ : Nontrivial α
⊢ Tendsto Int.cast (atBot ⊔ atTop) (Bornology.cobounded α)

Tactic:
by
  rw [← tendsto_norm_atTop_iff_cobounded]
  simpa [norm_intCast_eq_abs_mul_norm_one] using tendsto_intCast_atTop_atTop
    |>.comp (tendsto_abs_atBot_atTop.sup tendsto_abs_atTop_atTop)
    |>.atTop_mul_const (norm_pos_iff.mpr one_ne_zero)

Goal state after:
Module: Mathlib.Algebra.Order.CauSeq.BigOperators

Goal state before:

Tactic:
f i ≤ a - Nat.pred l • ε := hi.2
    _ = a - l • ε + ε := by
      conv =>
        rhs
        rw [← Nat.succ_pred_eq_of_pos (Nat.pos_of_ne_zero hl0), succ_nsmul, sub_add,
          add_sub_cancel_right]
    _ < f j + ε := by gcongr; exact hl _ <| hi.1.trans hj

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: n : ℤ
hx₁ : -(↑n * (2 * π)) < 2 * π
hx₂ : ↑n < 1
h : cos (↑n * (2 * π)) = 1
⊢ ↑n * (2 * π) = 0

Tactic:
neg_mul_eq_neg_mul,

Goal state after:
n : ℤ
hx₁ : -↑n * (2 * π) < 2 * π
hx₂ : ↑n < 1
h : cos (↑n * (2 * π)) = 1
⊢ ↑n * (2 * π) = 0
Module: Mathlib.Analysis.Normed.Module.RCLike.Real

Goal state before:
pp: E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x y : E
hr✝ : dist y x ≠ 0
hr : 0 < dist y x
hy : y ∈ interior (closedBall x (dist y x))
f : ℝ → E := fun c ↦ c • (y - x) + x
this : f ⁻¹' closedBall x (dist y x) ⊆ Icc (-1) 1
h1 : 1 ∈ interior (Icc (-1) 1)
⊢ y ∈ ball x (dist y x)

Tactic:
simp at h1

Goal state after:
Module: Mathlib.Analysis.Normed.Module.RCLike.Real

Goal state before:
pp: E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
r : ℝ
hr : r ≠ 0
⊢ frontier (sphere x r) = sphere x r

Tactic:
by
  rw [isClosed_sphere.frontier_eq, interior_sphere x hr, sdiff_empty]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: case inl
c : ℝ := cos (π / 5)
this : 4 * (c * c) + -2 * c + -1 = 0
hd : discrim 4 (-2) (-1) = 2 * √5 * (2 * √5)
h : c = (- -2 + 2 * √5) / (2 * 4)
⊢ c = (1 + √5) / 4

pp: case inr
c : ℝ := cos (π / 5)
this : 4 * (c * c) + -2 * c + -1 = 0
hd : discrim 4 (-2) (-1) = 2 * √5 * (2 * √5)
h : c = (- -2 - 2 * √5) / (2 * 4)
⊢ c = (1 + √5) / 4

Tactic:
· simp [h]; linarith

Goal state after:
case inr
c : ℝ := cos (π / 5)
this : 4 * (c * c) + -2 * c + -1 = 0
hd : discrim 4 (-2) (-1) = 2 * √5 * (2 * √5)
h : c = (- -2 - 2 * √5) / (2 * 4)
⊢ c = (1 + √5) / 4
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: R : Type u_4
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
k✝ : ℕ
r : R
hr : ‖r‖ < 1
k : ℕ
hk : ∀ m < k, Summable fun n ↦ ↑n ^ m * r ^ n
⊢ ∃ a, ∀ (n : ℕ), (n + k).descFactorial k = n ^ k + ∑ i ∈ Finset.range k, a i * n ^ i

Tactic:
by
    let P : Polynomial ℕ := (ascPochhammer ℕ k).comp (Polynomial.X + C 1)
    refine ⟨fun i ↦ P.coeff i, fun n ↦ ?_⟩
    have mP : Monic P := Monic.comp_X_add_C (monic_ascPochhammer ℕ k) _
    have dP : P.natDegree = k := by
      simp only [P, natDegree_comp, ascPochhammer_natDegree, mul_one, natDegree_X_add_C]
    have A : (n + k).descFactorial k = P.eval n := by
      have : n + 1 + k - 1 = n + k := by lia
      simp [P, ascPochhammer_nat_eq_descFactorial, this]
    conv_lhs => rw [A, mP.as_sum, dP]
    simp [eval_finsetSum]

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: α : Type u_1
inst✝ : SeminormedAddCommGroup α
C r : ℝ
hr : r < 1
u : ℕ → α
h : ∀ (n : ℕ), ‖u n - u (n + 1)‖ ≤ C * r ^ n
⊢ ∀ (n : ℕ), dist (u n) (u (n + 1)) ≤ C * r ^ n

Tactic:
simpa [dist_eq_norm] using h

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: α : Type u_1
inst✝ : SeminormedAddCommGroup α
C : ℝ
u : ℕ → α
N : ℕ
r : ℝ
hr₀ : 0 < r
hr₁ : r < 1
h : ∀ n ≥ N, ‖u n‖ ≤ C * r ^ n
v : ℕ → α := fun n ↦ if n < N then 0 else u n
⊢ CauchySeq fun n ↦ ∑ k ∈ Finset.range (n + 1), u k

Tactic:
have hC : 0 ≤ C :=
    (mul_nonneg_iff_of_pos_right <| pow_pos hr₀ N).mp ((norm_nonneg _).trans <| h N <| le_refl N)

Goal state after:
α : Type u_1
inst✝ : SeminormedAddCommGroup α
C : ℝ
u : ℕ → α
N : ℕ
r : ℝ
hr₀ : 0 < r
hr₁ : r < 1
h : ∀ n ≥ N, ‖u n‖ ≤ C * r ^ n
v : ℕ → α := fun n ↦ if n < N then 0 else u n
hC : 0 ≤ C
⊢ CauchySeq fun n ↦ ∑ k ∈ Finset.range (n + 1), u k
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: case mp
X : Type u_1
inst✝ : TopologicalSpace X
F : Set X
x : X
x_in : x ∈ F
h : ∀ ⦃y : X⦄, y ∈ F → JoinedIn F x y
⊢ ∃ x ∈ F, pathComponentIn F x = F

Tactic:
use x, x_in

Goal state after:
case right
X : Type u_1
inst✝ : TopologicalSpace X
F : Set X
x : X
x_in : x ∈ F
h : ∀ ⦃y : X⦄, y ∈ F → JoinedIn F x y
⊢ pathComponentIn F x = F
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: case mpr
X : Type u_1
inst✝ : TopologicalSpace X
F : Set X
x : X
x_in : x ∈ F
h : pathComponentIn F x = F
⊢ IsPathConnected F

Tactic:
use x, x_in

Goal state after:
case right
X : Type u_1
inst✝ : TopologicalSpace X
F : Set X
x : X
x_in : x ∈ F
h : pathComponentIn F x = F
⊢ ∀ ⦃y : X⦄, y ∈ F → JoinedIn F x y
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : PathConnectedSpace X
n : ℕ
p : Fin (n + 1) → X
this : IsPathConnected univ
γ : Path (p 0) (p (last n))
t : Fin (n + 1) → ↑I
h : ∀ (i : Fin (n + 1)), γ (t i) = p i
⊢ ∃ γ t, ∀ (i : Fin (n + 1)), γ (t i) = p i

Tactic:
exact ⟨γ, t, h⟩

Goal state after:
Module: Mathlib.Topology.Instances.ZMultiples

Goal state before:
pp: case inr
α : Type u
β : Type v
γ : Type w
a : ℝ
ha : a ≠ 0
⊢ Subtype.val ⁻¹' ball 0 |a| = {0}

Tactic:
ext ⟨x, hx⟩

Goal state after:
case inr
α : Type u
β : Type v
γ : Type w
a : ℝ
ha : a ≠ 0
x : ℝ
hx : x ∈ AddSubgroup.zmultiples a
⊢ ⟨x, hx⟩ ∈ Subtype.val ⁻¹' ball 0 |a| ↔ ⟨x, hx⟩ ∈ {0}
Module: Mathlib.Analysis.Normed.Group.AddCircle

Goal state before:
pp: p x ε : ℝ
s : Set ℝ
hε : ε < |p| / 2
z : ℤ
hs : s ⊆ Icc (x - |p| / 2) (x + |p| / 2)
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hy₁ : x + ↑z * p - ε ≤ y
hy₂ : y ≤ x + ↑z * p + ε
hy₃ : x - |p| / 2 ≤ y
hy₄ : y ≤ x + |p| / 2
hp : 0 < p
hz' : ↑z ≤ -1
⊢ ↑z * p ≤ -p

Tactic:
nlinarith

Goal state after:
Module: Mathlib.Analysis.Normed.Group.AddCircle

Goal state before:
pp: p x ε : ℝ
s : Set ℝ
hε : ε < |p| / 2
z : ℤ
hs : s ⊆ Icc (x - |p| / 2) (x + |p| / 2)
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hy₁ : x + ↑z * p - ε ≤ y
hy₂ : y ≤ x + ↑z * p + ε
hy₃ : x - |p| / 2 ≤ y
hy₄ : y ≤ x + |p| / 2
hp : 0 < p
hz' : 1 ≤ ↑z
⊢ p ≤ ↑z * p

Tactic:
nlinarith

Goal state after:
Module: Mathlib.Analysis.Normed.Group.AddCircle

Goal state before:
pp: p x ε : ℝ
s : Set ℝ
hε : ε < |p| / 2
z : ℤ
hs : s ⊆ Icc (x - |p| / 2) (x + |p| / 2)
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hy₁ : x + ↑z * p - ε ≤ y
hy₂ : y ≤ x + ↑z * p + ε
hy₃ : x - |p| / 2 ≤ y
hy₄ : y ≤ x + |p| / 2
hp : p < 0
hz' : ↑z ≤ -1
⊢ -p ≤ ↑z * p

Tactic:
nlinarith

Goal state after:
Module: Mathlib.Analysis.Normed.Group.AddCircle

Goal state before:
pp: p x ε : ℝ
s : Set ℝ
hε : ε < |p| / 2
z : ℤ
hs : s ⊆ Icc (x - |p| / 2) (x + |p| / 2)
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hy₁ : x + ↑z * p - ε ≤ y
hy₂ : y ≤ x + ↑z * p + ε
hy₃ : x - |p| / 2 ≤ y
hy₄ : y ≤ x + |p| / 2
hp : p < 0
hz' : 1 ≤ ↑z
⊢ ↑z * p ≤ p

Tactic:
nlinarith

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

Goal state before:
pp: ⊢ range arcsin = Icc (-(π / 2)) (π / 2)

Tactic:
rw [arcsin, range_comp Subtype.val]

Goal state after:
⊢ Subtype.val '' range (IccExtend arcsin._proof_2 ⇑sinOrderIso.symm) = Icc (-(π / 2)) (π / 2)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

Goal state before:
pp: x : ℝ
hx : 1 ≤ x
⊢ arcsin x = π / 2

Tactic:
← arcsin_projIcc,

Goal state after:
x : ℝ
hx : 1 ≤ x
⊢ arcsin ↑(projIcc (-1) 1 ⋯ x) = π / 2
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

Goal state before:
pp: x : ℝ
hx : x ≤ -1
⊢ arcsin x = -(π / 2)

Tactic:
← arcsin_projIcc,

Goal state after:
x : ℝ
hx : x ≤ -1
⊢ arcsin ↑(projIcc (-1) 1 ⋯ x) = -(π / 2)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

Goal state before:
pp: case neg
x : ℝ
hx₁ : x < -1
⊢ 1 - x ^ 2 ≤ 0

Tactic:
nlinarith

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

Goal state before:
pp: case neg
x : ℝ
hx₁ : -1 ≤ x
hx₂ : 1 < x
⊢ 1 - x ^ 2 ≤ 0

Tactic:
nlinarith

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

Goal state before:
pp: x : ℝ
hx₁ : ¬-1 ≤ x
⊢ 1 - x ^ 2 ≤ 0

Tactic:
nlinarith

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

Goal state before:
pp: x : ℝ
hx₁ : -1 ≤ x
hx₂ : ¬x ≤ 1
⊢ 1 - x ^ 2 ≤ 0

Tactic:
nlinarith

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

Goal state before:
pp: x y : ℝ
hlt : x ≤ y
⊢ arccos y ≤ arccos x

Tactic:
by unfold arccos; gcongr

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: x y : ℝ
hx : x ≠ 0
hy : y ≠ 0
⊢ rexp (log (x / y)) = rexp (log x - log y)

Tactic:
exp_log_eq_abs (div_ne_zero hx hy),

Goal state after:
x y : ℝ
hx : x ≠ 0
hy : y ≠ 0
⊢ |x / y| = rexp (log x - log y)
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: n : ℕ
hn : ¬n = 0
⊢ 0 ≤ log ↑n

Tactic:
have : (1 : ℝ) ≤ n := mod_cast Nat.one_le_of_lt <| Nat.pos_of_ne_zero hn

Goal state after:
n : ℕ
hn : ¬n = 0
this : 1 ≤ ↑n
⊢ 0 ≤ log ↑n
Module: Mathlib.Analysis.SpecialFunctions.Complex.Log

Goal state before:
pp: x y : ℂ
hx₀ : x ≠ 0
hy₀ : y ≠ 0
⊢ log (x * y) = log x + log y ↔ x.arg + y.arg ∈ Ioc (-π) π

Tactic:
refine Complex.ext_iff.trans <| Iff.trans ?_ <| arg_mul_eq_add_arg_iff hx₀ hy₀

Goal state after:
x y : ℂ
hx₀ : x ≠ 0
hy₀ : y ≠ 0
⊢ (log (x * y)).re = (log x + log y).re ∧ (log (x * y)).im = (log x + log y).im ↔ (x * y).arg = x.arg + y.arg
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: ψ θ : ℝ
⊢ ↑ψ = ↑θ ↔ ∃ k, θ - ψ = 2 * π * ↑k

Tactic:
rw [Angle.coe, Angle.coe, QuotientAddGroup.eq]

Goal state after:
ψ θ : ℝ
⊢ -ψ + θ ∈ AddSubgroup.zmultiples (2 * π) ↔ ∃ k, θ - ψ = 2 * π * ↑k
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ : Angle
⊢ 2 • θ = 0 ↔ θ = 0 ∨ θ = ↑π

Tactic:
two_nsmul_eq_zero_iff

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ : Angle
⊢ 2 • θ = 0 ↔ θ = 0 ∨ θ = ↑π

Tactic:
two_nsmul_eq_zero_iff

Goal state after:
θ : Angle
⊢ θ = 0 ∨ θ = ↑π ↔ θ = 0 ∨ θ = ↑π
Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex

Goal state before:
pp: x y : ℂ
n : ℕ
⊢ x ^ (↑n * y) = (x ^ y) ^ n

Tactic:
cpow_nat_mul

Goal state after:
x y : ℂ
n : ℕ
⊢ (x ^ y) ^ n = (x ^ y) ^ n
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case inr.inl.inl
x : ℂ
hi : x.im = 0
hr : x.re < 0
⊢ (-↑x.re).arg = π - π ↔ 0 < (↑x.re).im ∨ (↑x.re).im = 0 ∧ (↑x.re).re < 0

Tactic:
← ofReal_neg,

Goal state after:
case inr.inl.inl
x : ℂ
hi : x.im = 0
hr : x.re < 0
⊢ (↑(-x.re)).arg = π - π ↔ 0 < (↑x.re).im ∨ (↑x.re).im = 0 ∧ (↑x.re).re < 0
Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex

Goal state before:
pp: a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
r : ℂ
⊢ (↑a * (↑b)⁻¹) ^ r = ↑a ^ r / ↑b ^ r

Tactic:
← ofReal_inv,

Goal state after:
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
r : ℂ
⊢ (↑a * ↑b⁻¹) ^ r = ↑a ^ r / ↑b ^ r
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case inr.inl.inr.inr
x : ℂ
hi : x.im = 0
hr : 0 < x.re
⊢ (-↑x.re).arg = 0 - π ↔ 0 < (↑x.re).im ∨ (↑x.re).im = 0 ∧ (↑x.re).re < 0

Tactic:
← ofReal_neg,

Goal state after:
case inr.inl.inr.inr
x : ℂ
hi : x.im = 0
hr : 0 < x.re
⊢ (↑(-x.re)).arg = 0 - π ↔ 0 < (↑x.re).im ∨ (↑x.re).im = 0 ∧ (↑x.re).re < 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case h
x✝ : ℝ
⊢ toIocMod two_pi_pos (-π) (toIocMod two_pi_pos (-π) x✝) = toIocMod two_pi_pos (-π) x✝

Tactic:
exact toIocMod_toIocMod _ _ _ _

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case inr.inl.inl
x : ℂ
hi : x.im = 0
hr : x.re < 0
⊢ (-↑x.re).arg = π + π ↔ (↑x.re).im < 0 ∨ (↑x.re).im = 0 ∧ 0 < (↑x.re).re

Tactic:
← ofReal_neg,

Goal state after:
case inr.inl.inl
x : ℂ
hi : x.im = 0
hr : x.re < 0
⊢ (↑(-x.re)).arg = π + π ↔ (↑x.re).im < 0 ∨ (↑x.re).im = 0 ∧ 0 < (↑x.re).re
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case inr.inl.inr.inr
x : ℂ
hi : x.im = 0
hr : 0 < x.re
⊢ (-↑x.re).arg = 0 + π ↔ (↑x.re).im < 0 ∨ (↑x.re).im = 0 ∧ 0 < (↑x.re).re

Tactic:
← ofReal_neg,

Goal state after:
case inr.inl.inr.inr
x : ℂ
hi : x.im = 0
hr : 0 < x.re
⊢ (↑(-x.re)).arg = 0 + π ↔ (↑x.re).im < 0 ∨ (↑x.re).im = 0 ∧ 0 < (↑x.re).re
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ : ℝ
k : ℤ
⊢ (↑θ).toReal = θ - 2 * ↑k * π ↔ θ ∈ Set.Ioc ((2 * ↑k - 1) * π) ((2 * ↑k + 1) * π)

Tactic:
← sub_zero (θ : Angle),

Goal state after:
θ : ℝ
k : ℤ
⊢ (↑θ - 0).toReal = θ - 2 * ↑k * π ↔ θ ∈ Set.Ioc ((2 * ↑k - 1) * π) ((2 * ↑k + 1) * π)
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case inr.inl.inl
x : ℂ
hx : x ≠ 0
hi : x.im = 0
hr : x.re < 0
⊢ ↑(-↑x.re).arg = ↑π + ↑π

Tactic:
← ofReal_neg,

Goal state after:
case inr.inl.inl
x : ℂ
hx : x ≠ 0
hi : x.im = 0
hr : x.re < 0
⊢ ↑(↑(-x.re)).arg = ↑π + ↑π
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case inr.inl.inr.inr
x : ℂ
hx : x ≠ 0
hi : x.im = 0
hr : 0 < x.re
⊢ ↑(-↑x.re).arg = ↑0 + ↑π

Tactic:
← ofReal_neg,

Goal state after:
case inr.inl.inr.inr
x : ℂ
hx : x ≠ 0
hi : x.im = 0
hr : 0 < x.re
⊢ ↑(↑(-x.re)).arg = ↑0 + ↑π
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case inl
n : ℕ
⊢ ↑(0 ^ n).arg = n • ↑(arg 0)

Tactic:
by_cases n0 : n = 0

Goal state after:
case pos
n : ℕ
n0 : n = 0
⊢ ↑(0 ^ n).arg = n • ↑(arg 0)

case neg
n : ℕ
n0 : ¬n = 0
⊢ ↑(0 ^ n).arg = n • ↑(arg 0)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: ⊢ Function.Periodic tan ↑π

Tactic:
by
  intro θ
  induction θ using Real.Angle.induction_on
  rw [← coe_add, tan_coe, tan_coe]
  exact Real.tan_periodic _

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ ψ : Angle
h : 2 • θ + 2 • ψ = ↑π
⊢ ψ.tan = θ.tan⁻¹

Tactic:
by
  induction θ using Real.Angle.induction_on
  induction ψ using Real.Angle.induction_on
  rw [← smul_add, ← coe_add, ← coe_nsmul, two_nsmul, ← two_mul, angle_eq_iff_two_pi_dvd_sub] at h
  rcases h with ⟨k, h⟩
  rw [sub_eq_iff_eq_add, ← mul_inv_cancel_left₀ two_ne_zero π, mul_assoc, ← mul_add,
    mul_right_inj' (two_ne_zero' ℝ), ← eq_sub_iff_add_eq', mul_inv_cancel_left₀ two_ne_zero π,
    inv_mul_eq_div, mul_comm] at h
  rw [tan_coe, tan_coe, ← tan_pi_div_two_sub, h, add_sub_assoc, add_comm]
  exact Real.tan_periodic.int_mul _ _

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case mp
a b : Angle
ha : a.sign ≠ 0
h✝ : a.sign = b.sign
h : a = b ∨ a = b + ↑π
⊢ a = b

Tactic:
rcases h with h1 | h2

Goal state after:
case mp.inl
a b : Angle
ha : a.sign ≠ 0
h : a.sign = b.sign
h1 : a = b
⊢ a = b

case mp.inr
a b : Angle
ha : a.sign ≠ 0
h : a.sign = b.sign
h2 : a = b + ↑π
⊢ a = b
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case pos
x y : ℝ
hx : x = 0
⊢ |x| ^ y ≤ rexp (log x * y)

Tactic:
by_cases hy : y = 0

Goal state after:
case pos
x y : ℝ
hx : x = 0
hy : y = 0
⊢ |x| ^ y ≤ rexp (log x * y)

case neg
x y : ℝ
hx : x = 0
hy : ¬y = 0
⊢ |x| ^ y ≤ rexp (log x * y)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case inr
x : ℝ
hx : x ≤ 0
y : ℂ
hlt : x < 0
hne : ↑x ≠ 0
⊢ cexp ((↑(Real.log ‖↑x‖) + ↑π * I) * y) = cexp ((↑(Real.log ‖↑x‖) + ↑(-↑x).arg * I + ↑π * I) * y)

Tactic:
← ofReal_neg,

Goal state after:
case inr
x : ℝ
hx : x ≤ 0
y : ℂ
hlt : x < 0
hne : ↑x ≠ 0
⊢ cexp ((↑(Real.log ‖↑x‖) + ↑π * I) * y) = cexp ((↑(Real.log ‖↑x‖) + ↑(↑(-x)).arg * I + ↑π * I) * y)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: E : Type u_2
inst✝ : SeminormedRing E
a b c : ℝ
f g : ℝ → E
hf : f =O[atTop] fun t ↦ t ^ a
hg : g =O[atTop] fun t ↦ t ^ b
h : a + b ≤ c
t : ℝ
ht : 1 ≤ t
⊢ ‖t ^ a * t ^ b‖ ≤ t ^ c

Tactic:
rw [← Real.rpow_add (zero_lt_one.trans_le ht), Real.norm_of_nonneg (Real.rpow_nonneg
    (zero_le_one.trans ht) (a + b))]

Goal state after:
E : Type u_2
inst✝ : SeminormedRing E
a b c : ℝ
f g : ℝ → E
hf : f =O[atTop] fun t ↦ t ^ a
hg : g =O[atTop] fun t ↦ t ^ b
h : a + b ≤ c
t : ℝ
ht : 1 ≤ t
⊢ t ^ (a + b) ≤ t ^ c
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: E : Type u_2
inst✝ : SeminormedRing E
a b c : ℝ
f g : ℕ → E
hf : f =O[atTop] fun n ↦ ↑n ^ a
hg : g =O[atTop] fun n ↦ ↑n ^ b
h : a + b ≤ c
t : ℕ
ht : 1 ≤ ↑t
⊢ ‖↑t ^ a * ↑t ^ b‖ ≤ ↑t ^ c

Tactic:
rw [← Real.rpow_add (zero_lt_one.trans_le ht), Real.norm_of_nonneg (Real.rpow_nonneg
    (zero_le_one.trans ht) (a + b))]

Goal state after:
E : Type u_2
inst✝ : SeminormedRing E
a b c : ℝ
f g : ℕ → E
hf : f =O[atTop] fun n ↦ ↑n ^ a
hg : g =O[atTop] fun n ↦ ↑n ^ b
h : a + b ≤ c
t : ℕ
ht : 1 ≤ ↑t
⊢ ↑t ^ (a + b) ≤ ↑t ^ c
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: x : ℝ≥0
hx : x ≠ 0
y : ℝ
n : ℤ
⊢ ↑(x ^ (y + ↑n)) = ↑(x ^ y * x ^ n)

Tactic:
exact Real.rpow_add_intCast (mod_cast hx) _ _

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity

Goal state before:
pp: α : Type u_1
l : Filter α
f : α → ℝ
x p : ℝ
hf : Tendsto f l (𝓝 x)
h : x ≠ 0 ∨ 0 ≤ p
h0 : 0 = p
⊢ Tendsto (fun a ↦ f a ^ 0) l (𝓝 (x ^ 0))

Tactic:
by simp [tendsto_const_nhds]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: x y : ℝ
hx : 0 ≤ x
⊢ (x ^ y).toNNReal = x.toNNReal ^ y

Tactic:
← Real.coe_toNNReal x hx

Goal state after:
x y : ℝ
hx : 0 ≤ x
⊢ (↑x.toNNReal ^ y).toNNReal = x.toNNReal ^ y
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : z < 0
⊢ x ^ z⁻¹ ≤ y ↔ y ^ z ≤ x

Tactic:
← rpow_le_rpow_iff_of_neg hy _ hz,

Goal state after:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : z < 0
⊢ y ^ z ≤ (x ^ z⁻¹) ^ z ↔ y ^ z ≤ x

x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : z < 0
⊢ 0 < x ^ z⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x y : ℝ
hx : 0 < x
⊢ x ^ y < 1 ↔ 1 < x ∧ y < 0 ∨ x < 1 ∧ 0 < y

Tactic:
rw [rpow_def_of_pos hx, exp_lt_one_iff, mul_neg_iff, log_pos_iff hx.le, log_neg_iff hx]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case inl.inr
y z : ℝ
hyz : z ≤ y
hx0 : 0 ≤ 0
hx1 : 0 ≤ 1
h : 0 = 0 → y = 0 → z = 0
hy0 : y ≠ 0
⊢ 0 ^ y ≤ 0 ^ z

Tactic:
rw [zero_rpow hy0]
      apply zero_rpow_nonneg

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case inl
x y z : ℝ
x1 : 1 ≤ x
yz : y ≤ z
⊢ x ^ y ≤ x ^ z

pp: case inr
x y z : ℝ
x0 : 0 < x
x1 : x ≤ 1
zy : z ≤ y
⊢ x ^ y ≤ x ^ z

Tactic:
· exact Real.rpow_le_rpow_of_exponent_le x1 yz

Goal state after:
case inr
x y z : ℝ
x0 : 0 < x
x1 : x ≤ 1
zy : z ≤ y
⊢ x ^ y ≤ x ^ z
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℂ
⊢ (x ^ (↑2)⁻¹).re = √((‖x‖ + x.re) / 2)

Tactic:
← ofReal_inv,

Goal state after:
x : ℂ
⊢ (x ^ ↑2⁻¹).re = √((‖x‖ + x.re) / 2)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℂ
hx : 0 ≤ x.im
⊢ (x ^ (↑2)⁻¹).im = √((‖x‖ - x.re) / 2)

Tactic:
← ofReal_inv,

Goal state after:
x : ℂ
hx : 0 ≤ x.im
⊢ (x ^ ↑2⁻¹).im = √((‖x‖ - x.re) / 2)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℂ
hx : x.im < 0
⊢ (x ^ (↑2)⁻¹).im = -√((‖x‖ - x.re) / 2)

Tactic:
← ofReal_inv,

Goal state after:
x : ℂ
hx : x.im < 0
⊢ (x ^ ↑2⁻¹).im = -√((‖x‖ - x.re) / 2)