mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: a : ℕ
⊢ ⌊√↑a⌋₊ = a.sqrt

Tactic:
Nat.floor_eq_iff (sqrt_nonneg a)

Goal state after:
a : ℕ
⊢ ↑a.sqrt ≤ √↑a ∧ √↑a < ↑a.sqrt + 1
Module: Mathlib.Analysis.Complex.Norm

Goal state before:
pp: n : ℤ
hn : 0 ≤ n
⊢ ‖↑n‖ = ↑n

Tactic:
norm_intCast,

Goal state after:
n : ℤ
hn : 0 ≤ n
⊢ |↑n| = ↑n
Module: Mathlib.Analysis.Complex.Norm

Goal state before:
pp: z : ℂ
⊢ ‖z‖ ^ 2 - z.im ^ 2 = z.re ^ 2

Tactic:
by
  rw [← sq_norm_sub_sq_re, sub_sub_cancel]

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

Goal state before:
pp: r : ℝ
z : ℂ
hz : ↑r ≤ z
⊢ z = ↑z.re

Tactic:
rw [eq_comm, ← conj_eq_iff_re, conj_eq_iff_im, ← (Complex.le_def.1 hz).2, Complex.ofReal_im]

Goal state after:
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: z : ℂ
h : z ≠ 0
⊢ ↑1 = 1

Tactic:
ofReal_one

Goal state after:
z : ℂ
h : z ≠ 0
⊢ 1 = 1
Module: Mathlib.Analysis.Normed.Group.Hom

Goal state before:
pp: V₁ : Type u_2
V₂ : Type u_3
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
x : V₁
C : ℝ
_Cpos : 0 < C
hC : ‖f x‖ ≤ C * ‖x‖
h : ¬‖x‖ = 0
hlt : 0 < ‖x‖
c : ℝ
x✝ : c ∈ {c | 0 ≤ c ∧ ∀ (x : V₁), ‖f x‖ ≤ c * ‖x‖}
left✝ : 0 ≤ c
hc : ∀ (x : V₁), ‖f x‖ ≤ c * ‖x‖
⊢ ‖f x‖ ≤ c * ‖x‖

Tactic:
by apply hc

Goal state after:
Module: Mathlib.Algebra.Star.Unitary

Goal state before:
pp: R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarMul R
u : R
hu : IsUnit u
⊢ star u * u = 1 ∧ u * star u = 1 ↔ star u * u = 1

Tactic:
and_iff_left_of_imp fun h_mul => ?_

Goal state after:
R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarMul R
u : R
hu : IsUnit u
⊢ star u * u = 1 ↔ star u * u = 1

R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarMul R
u : R
hu : IsUnit u
h_mul : star u * u = 1
⊢ u * star u = 1
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
I' : A
hf : I' * I' = -1
⊢ 1 + 0 • I' = 1

Tactic:
zero_smul,

Goal state after:
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
I' : A
hf : I' * I' = -1
⊢ 1 + 0 = 1
Module: Mathlib.Analysis.Complex.Basic

Goal state before:
pp: n : ℤ
⊢ ‖↑n‖₊ = ‖n‖₊

Tactic:
by
  ext; exact norm_intCast n

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

Goal state before:
pp: r : ℝ
s : Set ℂ
hs : s ⊆ sphere 0 r
⊢ (∃ x ∈ s, x ≤ 0) ↔ -↑r ∈ s

Tactic:
refine ⟨?_, fun hr ↦ ⟨_, hr, by simpa using hs hr⟩⟩

Goal state after:
r : ℝ
s : Set ℂ
hs : s ⊆ sphere 0 r
⊢ (∃ x ∈ s, x ≤ 0) → -↑r ∈ s
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
x : K
hx : x ≠ 0
⊢ ‖↑‖x‖ / x‖ = 1 ∧ ↑‖x‖ = ↑‖x‖ / x * x

Tactic:
simp [norm_ne_zero_iff.2, hx]

Goal state after:
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
x : K
hx : x ≠ 0
⊢ ‖x / ↑‖x‖‖ = 1 ∧ x / ↑‖x‖ * ↑‖x‖ = x

Tactic:
simp [norm_ne_zero_iff.2, hx]

Goal state after:
Module: Mathlib.Topology.PartialHomeomorph.Basic

Goal state before:
pp: case h
X : Type u_1
Y : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
h : IsEmbedding f
inst✝ : Nonempty X
x : X
⊢ x ∈ (toPartialHomeomorph f h).source

Tactic:
exact Set.mem_univ _

Goal state after:
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ z ≤ 0 ↔ ∃ x ≤ 0, ↑x = z

Tactic:
simp_rw [nonpos_iff (K := K), ext_iff (K := K)]; aesop

Goal state after:
Module: Mathlib.Topology.OpenPartialHomeomorph.Basic

Goal state before:
pp: case h
X : Type u_1
Y : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
h : IsOpenEmbedding f
inst✝ : Nonempty X
x : X
⊢ x ∈ (toOpenPartialHomeomorph f h).source

Tactic:
exact Set.mem_univ _

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

Goal state before:
pp: α : Type u_1
𝕜 : Type u_14
𝕜' : Type u_15
inst✝¹ : NormedField 𝕜
inst✝ : NormedField 𝕜'
l : Filter α
f : α → 𝕜
g : α → 𝕜'
h : f =Θ[l] g
n : ℤ
⊢ (fun x ↦ f x ^ n) =Θ[l] fun x ↦ g x ^ n

Tactic:
cases n
  · simpa only [Int.ofNat_eq_natCast, zpow_natCast] using h.pow _
  · simpa only [zpow_negSucc] using (h.pow _).inv

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

Goal state before:
pp: case mpr
α : Type u_1
E' : Type u_6
E'' : Type u_9
inst✝¹ : SeminormedAddCommGroup E'
inst✝ : NormedAddCommGroup E''
f' : α → E'
l : Filter α
c : E''
hc : c ≠ 0
⊢ (∃ b, 0 < b ∧ ∀ᶠ (x : α) in l, b ≤ ‖f' x‖) → (fun _x ↦ c) =O[l] f'

Tactic:
rintro ⟨b, hb₀, hb⟩
    refine IsBigO.of_bound (‖c‖ / b) (hb.mono fun x hx => ?_)
    rw [div_mul_eq_mul_div, mul_div_assoc]
    exact le_mul_of_one_le_right (norm_nonneg _) ((one_le_div hb₀).2 hx)

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

Goal state before:
pp: x : ℝ
⊢ ↑(sinh x) = ↑((rexp x - rexp (-x)) / 2)

Tactic:
by simp [Complex.sinh]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: n : ℕ
C : ℝ
hC₁ : 1 ≤ C
hC₀ : 0 < C
this : 0 < (rexp 1 * C)⁻¹
N : ℕ
hN : ∀ k ≥ N, ↑k ^ n < rexp ↑k / (rexp 1 * C)
⊢ ∃ ia, True ∧ ∀ x ∈ Set.Ioi ia, rexp x / x ^ n ∈ Set.Ici C

Tactic:
refine ⟨N, trivial, fun x hx => ?_⟩

Goal state after:
n : ℕ
C : ℝ
hC₁ : 1 ≤ C
hC₀ : 0 < C
this : 0 < (rexp 1 * C)⁻¹
N : ℕ
hN : ∀ k ≥ N, ↑k ^ n < rexp ↑k / (rexp 1 * C)
x : ℝ
hx : x ∈ Set.Ioi ↑N
⊢ rexp x / x ^ n ∈ Set.Ici C
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: x : ℝ
hx₁ : -π < x
hx₂ : x < π
h : sin x = 0
⊢ x = 0

Tactic:
contrapose! h
    cases h.lt_or_gt with
    | inl h0 => exact (sin_neg_of_neg_of_neg_pi_lt h0 hx₁).ne
    | inr h0 => exact (sin_pos_of_pos_of_lt_pi h0 hx₂).ne'

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

Goal state before:
pp: M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
h : ↑S.topologicalClosure ≠ univ
⊢ ∃ x, 0 < ‖↑x‖

Tactic:
refine (Set.nonempty_compl.2 h).imp fun x hx ↦ ?_
    exact (norm_nonneg _).lt_of_ne' <| mt norm_mk_eq_zero_iff_mem_closure.1 hx

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

Goal state before:
pp: E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
s : Set E
⊢ s * ball 1 δ = ⋃ x ∈ s, ball x δ

Tactic:
convert! iUnion₂_mul (fun x (_ : x ∈ s) => { x }) (ball (1 : E) δ)

Goal state after:
case e'_2
E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
s : Set E
⊢ s = ⋃ i ∈ s, {i}

case e'_3.f
E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
s : Set E
x✝¹ : E
x✝ : x✝¹ ∈ s
⊢ ball x✝¹ δ = {x✝¹} * ball 1 δ
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedDivisionRing 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : NormSMulClass 𝕜 E
c : 𝕜
hc : c ≠ 0
s : Set E
x : E
⊢ infEDist (c • x) (c • s) = ‖c‖₊ • infEDist x s

Tactic:
simp_rw [infEDist]

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedDivisionRing 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : NormSMulClass 𝕜 E
c : 𝕜
hc : c ≠ 0
s : Set E
x : E
⊢ ⨅ y ∈ c • s, edist (c • x) y = ‖c‖₊ • ⨅ y ∈ s, edist x y
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
⊢ y ∈ ball x (dist y x)

Tactic:
by
    have h1 : (1 : ℝ) ∈ interior (Icc (-1 : ℝ) 1) :=
      interior_mono this (preimage_interior_subset_interior_preimage (by fun_prop) (by simpa [f]))
    simp at h1

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

Goal state before:
pp: R : Type u_2
S : Type u_3
inst✝⁵ : Field R
inst✝⁴ : Field S
inst✝³ : LinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : IsStrictOrderedRing S
inst✝ : Archimedean S
_i : OrderTopology S
v : AbsoluteValue R S
a : R
ha : v a < 1
⊢ Tendsto (fun n ↦ v (1 / (1 + a ^ n))) atTop (𝓝 1)

Tactic:
by
  simp_rw [map_div₀ v, v.map_one]
  apply one_div_one (G := S) ▸ Tendsto.div tendsto_const_nhds _ one_ne_zero
  have h_add := (tendsto_pow_atTop_nhds_zero_of_lt_one (v.nonneg _) ha).const_add 1
  have h_sub := (tendsto_pow_atTop_nhds_zero_of_lt_one (v.nonneg _) ha).const_sub 1
  exact tendsto_of_tendsto_of_tendsto_of_le_of_le (by simpa using h_sub) (by simpa using h_add)
    (fun n ↦ le_trans (by simp) (v.le_add _ _))
    (fun n ↦ le_trans (v.add_le _ _) (by simp))

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

Goal state before:
pp: R : Type u_4
inst✝ : NormedRing R
x : R
h : ‖x‖ < 1
⊢ ‖∑' (n : ℕ), x ^ n‖ ≤ ‖1‖ - 1 + (1 - ‖x‖)⁻¹

Tactic:
by
  by_cases hx : Summable (fun n ↦ x ^ n)
  · rw [hx.tsum_eq_zero_add]
    simp only [_root_.pow_zero]
    refine le_trans (norm_add_le _ _) ?_
    have : ‖∑' b : ℕ, (fun n ↦ x ^ (n + 1)) b‖ ≤ (1 - ‖x‖)⁻¹ - 1 := by
      refine tsum_of_norm_bounded ?_ fun b ↦ norm_pow_le' _ (Nat.succ_pos b)
      convert! (hasSum_nat_add_iff' 1).mpr (hasSum_geometric_of_lt_one (norm_nonneg x) h)
      simp
    linarith
  · simp only [tsum_eq_zero_of_not_summable hx, norm_zero]
    nontriviality R
    have : 1 ≤ ‖(1 : R)‖ := one_le_norm_one R
    have : 0 ≤ (1 - ‖x‖)⁻¹ := inv_nonneg.2 (by linarith)
    linarith

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

Goal state before:
pp: E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x y : E
δ ε : ℝ
hδ : 0 < δ
hε : 0 < ε
h : Disjoint (ball x δ) (ball y ε)
hxy : dist x y < ε + δ
z : E
hxz : dist x z < δ
hzy : dist z y < ε
⊢ False

Tactic:
rw [dist_comm] at hxz

Goal state after:
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x y : E
δ ε : ℝ
hδ : 0 < δ
hε : 0 < ε
h : Disjoint (ball x δ) (ball y ε)
hxy : dist x y < ε + δ
z : E
hxz : dist z x < δ
hzy : dist z y < ε
⊢ False
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

Goal state before:
pp: E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x y : E
δ ε : ℝ
hδ : 0 < δ
hε : 0 ≤ ε
h : Disjoint (ball x δ) (closedBall y ε)
hxy : dist x y < ε + δ
z : E
hxz : dist x z < δ
hzy : dist z y ≤ ε
⊢ False

Tactic:
rw [dist_comm] at hxz

Goal state after:
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x y : E
δ ε : ℝ
hδ : 0 < δ
hε : 0 ≤ ε
h : Disjoint (ball x δ) (closedBall y ε)
hxy : dist x y < ε + δ
z : E
hxz : dist z x < δ
hzy : dist z y ≤ ε
⊢ False
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

Goal state before:
pp: E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x y : E
δ ε : ℝ
hδ : 0 ≤ δ
hε : 0 ≤ ε
h : Disjoint (closedBall x δ) (closedBall y ε)
hxy : dist x y ≤ ε + δ
z : E
hxz : dist x z ≤ δ
hzy : dist z y ≤ ε
⊢ False

Tactic:
rw [dist_comm] at hxz

Goal state after:
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x y : E
δ ε : ℝ
hδ : 0 ≤ δ
hε : 0 ≤ ε
h : Disjoint (closedBall x δ) (closedBall y ε)
hxy : dist x y ≤ ε + δ
z : E
hxz : dist z x ≤ δ
hzy : dist z y ≤ ε
⊢ False
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: case mp
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
h : x ∈ pathComponent y
z : X
h' : z ∈ pathComponent x
⊢ y ∈ pathComponent z

Tactic:
exact (h.trans h').symm

Goal state after:
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y : X
F : Set X
h : x ∈ pathComponentIn F y
x✝ : X
⊢ x✝ ∈ pathComponentIn F x ↔ x✝ ∈ pathComponentIn F y

Tactic:
exact ⟨h.trans, h.symm.trans⟩

Goal state after:
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x : X
⊢ IsPathConnected (pathComponentIn univ x)

Tactic:
exact isPathConnected_pathComponentIn (mem_univ x)

Goal state after:
Module: Mathlib.Topology.Path

Goal state before:
pp: case pos
X : Type u_1
inst✝ : TopologicalSpace X
x y z : X
γ : Path x y
γ' : Path y z
t : ↑I
h✝ : ¬↑(σ t) ≤ 1 / 2
h : ¬1 - ↑t ≤ 1 / 2
h₂ : ↑t ≤ 1 / 2
⊢ ↑⟨2 * ↑(σ t) - 1, ⋯⟩ = ↑(σ ⟨2 * ↑t, ⋯⟩)

Tactic:
simp only [coe_symm_eq]

Goal state after:
case pos
X : Type u_1
inst✝ : TopologicalSpace X
x y z : X
γ : Path x y
γ' : Path y z
t : ↑I
h✝ : ¬↑(σ t) ≤ 1 / 2
h : ¬1 - ↑t ≤ 1 / 2
h₂ : ↑t ≤ 1 / 2
⊢ 2 * (1 - ↑t) - 1 = 1 - 2 * ↑t
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
x y z : X
ι : Type u_3
F : Set X
inst✝ : PathConnectedSpace X
⊢ ConnectedSpace X

Tactic:
rw [connectedSpace_iff_connectedComponent]
  rcases isPathConnected_iff_eq.mp (pathConnectedSpace_iff_univ.mp ‹_›) with ⟨x, _x_in, hx⟩
  use x
  rw [← univ_subset_iff]
  exact (by simpa using hx : pathComponent x = univ) ▸ pathComponent_subset_component x

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

Goal state before:
pp: case refine_1
x r : ℝ
hr : r ≤ ‖↑x‖
⊢ r ≤ |x - ↑(round x)|

Tactic:
rw [abs_sub_round_eq_min, le_inf_iff]
    rw [le_norm_iff] at hr
    constructor
    · simpa [abs_of_nonneg] using hr (fract x)
    · simpa [abs_sub_comm (fract x)] using hr (fract x - 1) (by simp)

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

Goal state before:
pp: case inl
E : Type u_5
inst✝⁶ : Ring E
inst✝⁵ : LinearOrder E
inst✝⁴ : IsOrderedRing E
inst✝³ : UniformSpace E
inst✝² : IsUniformAddGroup E
inst✝¹ : CompleteSpace E
inst✝ : OrderClosedTopology E
f : ℕ → E
hfa : Antitone f
hfs : Summable f
h✝ : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, (-1) ^ i * f i) atTop (𝓝 (∑' (i : ℕ), (-1) ^ i * f i))
I : ∀ (n : ℕ), 0 ≤ f n
n : ℕ
upper : ∑ i ∈ Finset.range (2 * n), (-1) ^ i * f i ≤ ∑' (i : ℕ), (-1) ^ i * f i
h : Even (2 * n)
lower : ∑' (i : ℕ), (-1) ^ i * f i ≤ ∑ i ∈ Finset.range (2 * n), (-1) ^ i * f i + f (2 * n)
⊢ |∑' (i : ℕ), (-1) ^ i * f i - ∑ i ∈ Finset.range (2 * n), (-1) ^ i * f i| ≤ f (2 * n)

Tactic:
abs_sub_le_iff

Goal state after:
case inl
E : Type u_5
inst✝⁶ : Ring E
inst✝⁵ : LinearOrder E
inst✝⁴ : IsOrderedRing E
inst✝³ : UniformSpace E
inst✝² : IsUniformAddGroup E
inst✝¹ : CompleteSpace E
inst✝ : OrderClosedTopology E
f : ℕ → E
hfa : Antitone f
hfs : Summable f
h✝ : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, (-1) ^ i * f i) atTop (𝓝 (∑' (i : ℕ), (-1) ^ i * f i))
I : ∀ (n : ℕ), 0 ≤ f n
n : ℕ
upper : ∑ i ∈ Finset.range (2 * n), (-1) ^ i * f i ≤ ∑' (i : ℕ), (-1) ^ i * f i
h : Even (2 * n)
lower : ∑' (i : ℕ), (-1) ^ i * f i ≤ ∑ i ∈ Finset.range (2 * n), (-1) ^ i * f i + f (2 * n)
⊢ ∑' (i : ℕ), (-1) ^ i * f i - ∑ i ∈ Finset.range (2 * n), (-1) ^ i * f i ≤ f (2 * n) ∧
    ∑ i ∈ Finset.range (2 * n), (-1) ^ i * f i - ∑' (i : ℕ), (-1) ^ i * f i ≤ f (2 * n)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

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

Tactic:
rw [← arcsin_projIcc, projIcc_of_le_left _ hx, Subtype.coe_mk, arcsin_neg_one]

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

Goal state before:
pp: case inr
E : Type u_5
inst✝⁶ : Ring E
inst✝⁵ : LinearOrder E
inst✝⁴ : IsOrderedRing E
inst✝³ : UniformSpace E
inst✝² : IsUniformAddGroup E
inst✝¹ : CompleteSpace E
inst✝ : OrderClosedTopology E
f : ℕ → E
hfa : Antitone f
hfs : Summable f
h✝ : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, (-1) ^ i * f i) atTop (𝓝 (∑' (i : ℕ), (-1) ^ i * f i))
I : ∀ (n : ℕ), 0 ≤ f n
n : ℕ
lower : ∑' (i : ℕ), (-1) ^ i * f i ≤ ∑ i ∈ Finset.range (2 * n + 1), (-1) ^ i * f i
upper : ∑ x ∈ Finset.range (2 * n + 1), (-1) ^ x * f x + (-1) ^ (2 * n + 1) * f (2 * n + 1) ≤ ∑' (i : ℕ), (-1) ^ i * f i
h : Odd (2 * n + 1)
⊢ |∑' (i : ℕ), (-1) ^ i * f i - ∑ i ∈ Finset.range (2 * n + 1), (-1) ^ i * f i| ≤ f (2 * n + 1)

Tactic:
abs_sub_le_iff

Goal state after:
case inr
E : Type u_5
inst✝⁶ : Ring E
inst✝⁵ : LinearOrder E
inst✝⁴ : IsOrderedRing E
inst✝³ : UniformSpace E
inst✝² : IsUniformAddGroup E
inst✝¹ : CompleteSpace E
inst✝ : OrderClosedTopology E
f : ℕ → E
hfa : Antitone f
hfs : Summable f
h✝ : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, (-1) ^ i * f i) atTop (𝓝 (∑' (i : ℕ), (-1) ^ i * f i))
I : ∀ (n : ℕ), 0 ≤ f n
n : ℕ
lower : ∑' (i : ℕ), (-1) ^ i * f i ≤ ∑ i ∈ Finset.range (2 * n + 1), (-1) ^ i * f i
upper : ∑ x ∈ Finset.range (2 * n + 1), (-1) ^ x * f x + (-1) ^ (2 * n + 1) * f (2 * n + 1) ≤ ∑' (i : ℕ), (-1) ^ i * f i
h : Odd (2 * n + 1)
⊢ ∑' (i : ℕ), (-1) ^ i * f i - ∑ i ∈ Finset.range (2 * n + 1), (-1) ^ i * f i ≤ f (2 * n + 1) ∧
    ∑ i ∈ Finset.range (2 * n + 1), (-1) ^ i * f i - ∑' (i : ℕ), (-1) ^ i * f i ≤ f (2 * n + 1)
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: case neg
x : ℝ
h : ¬x = 0
⊢ log |x| = log x

Tactic:
rw [← exp_eq_exp, exp_log_eq_abs h, exp_log_eq_abs (abs_pos.2 h).ne', abs_abs]

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

Goal state before:
pp: x y : ℂ
⊢ x.arg < y.arg + 2 * π

Tactic:
grind [arg_le_pi x, neg_pi_lt_arg y]

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

Goal state before:
pp: case inr
x : ℂ
r : ℝ
hr : 0 < r
hx : x ≠ 0
⊢ (↑r * x).arg = x.arg

Tactic:
conv_lhs =>
    rw [← norm_mul_cos_add_sin_mul_I x, ← mul_assoc, ← ofReal_mul,
      arg_mul_cos_add_sin_mul_I (mul_pos hr (norm_pos_iff.mpr hx)) x.arg_mem_Ioc]

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

Goal state before:
pp: case neg.mpr
x : ℝ
h : x < 0
h₀ : ¬{ re := x, im := 0 } = 0
⊢ { re := x, im := 0 }.arg = (↑(-x) * -1).arg

Tactic:
simp [← ofReal_def]

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

Goal state before:
pp: case hbdd
R : Type u_4
K : Type u_5
inst✝¹⁰ : NormedRing K
inst✝⁹ : IsDomain K
inst✝⁸ : NormedAddCommGroup R
inst✝⁷ : Module K R
inst✝⁶ : IsTorsionFree K R
inst✝⁵ : NormSMulClass K R
inst✝⁴ : NormSMulClass ℤ K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : FloorSemiring K
inst✝ : HasSolidNorm K
g : ℕ → R
t : R
hg : Tendsto (fun n ↦ ↑n • g n) atTop (𝓝 t)
⊢ IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) atTop fun x ↦ ‖↑⌊x⌋₊ - x‖

Tactic:
apply isBoundedUnder_of_eventually_le (a := ‖(1 : K)‖)
    apply Eventually.mono _ (fun x h ↦ norm_le_norm_of_abs_le_abs h)
    simpa using ⟨0, fun _ h ↦ mod_cast Nat.abs_floor_sub_le h⟩

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

Goal state before:
pp: x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x < y
⊢ |y| < |x|

Tactic:
rwa [abs_of_neg hy, abs_of_neg hx, neg_lt_neg_iff]

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

Goal state before:
pp: case succ.inr
x : ℝ
n : ℕ
ih : log (x ^ n) = ↑n * log x
hx : x ≠ 0
⊢ log (x ^ n * x) = ↑(n + 1) * log x

Tactic:
log_mul (pow_ne_zero _ hx) hx,

Goal state after:
case succ.inr
x : ℝ
n : ℕ
ih : log (x ^ n) = ↑n * log x
hx : x ≠ 0
⊢ log (x ^ n) + log x = ↑(n + 1) * log x
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: ψ θ : Angle
this : Int.natAbs 2 = 2
⊢ ψ = θ + 0 • ↑(2 * π / ↑2) ∨ ψ = θ + 1 • ↑(2 * π / ↑2) ↔ ψ = θ ∨ ψ = θ + ↑π

Tactic:
zero_smul,

Goal state after:
ψ θ : Angle
this : Int.natAbs 2 = 2
⊢ ψ = θ + 0 ∨ ψ = θ + 1 • ↑(2 * π / ↑2) ↔ ψ = θ ∨ ψ = θ + ↑π
Module: Mathlib.Analysis.SpecialFunctions.Complex.Log

Goal state before:
pp: k N : ℕ
hN : N ≠ 0
n : ℤ
| 2 * ↑π * I * ↑k / ↑N = ↑n * (2 * ↑π * I)

Tactic:
rw [← mul_comm (2 * π * I), mul_div_assoc, mul_right_inj' (by simp)]

Goal state after:
k N : ℕ
hN : N ≠ 0
n : ℤ
| ↑k / ↑N = ↑n
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: y : ℝ
⊢ Tendsto (fun x ↦ log (x + y) - log x) atTop (𝓝 0)

Tactic:
by
  have : Tendsto (fun x ↦ 1 + y / x) atTop (𝓝 (1 + 0)) :=
    tendsto_const_nhds.add (tendsto_const_nhds.div_atTop tendsto_id)
  rw [← comap_exp_nhds_exp, exp_zero, tendsto_comap_iff, ← add_zero (1 : ℝ)]
  refine this.congr' ?_
  filter_upwards [eventually_gt_atTop (0 : ℝ), eventually_gt_atTop (-y)] with x hx₀ hxy
  rw [comp_apply, exp_sub, exp_log, exp_log, one_add_div] <;> linarith

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

Goal state before:
pp: θ : Angle
⊢ (-θ).cos = θ.cos

Tactic:
induction θ using Real.Angle.induction_on
  exact Real.cos_neg _

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

Goal state before:
pp: case h
x✝ : ℝ
⊢ (↑x✝).cos ^ 2 + (↑x✝).sin ^ 2 = 1

Tactic:
exact Real.cos_sq_add_sin_sq _

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

Goal state before:
pp: ⊢ ↑(π / 2) ≠ 0

Tactic:
by
  rw [← toReal_injective.ne_iff, toReal_pi_div_two, toReal_zero]
  exact div_ne_zero Real.pi_ne_zero two_ne_zero

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

Goal state before:
pp: θ ψ : Angle
h : 2 • θ + 2 • ψ = ↑π
⊢ |θ.cos| = |ψ.sin|

Tactic:
exact abs_cos_eq_abs_sin_of_two_nsmul_add_two_nsmul_eq_pi h

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

Goal state before:
pp: case refine_1
z : ℂ
hre : z.re < 0
him : z.im = 0
this : arg =ᶠ[𝓝[{z | 0 ≤ z.im}] z] fun x ↦ Real.arcsin ((-x).im / ‖x‖) + π
⊢ ContinuousWithinAt (fun x ↦ Real.arcsin ((-x).im / ‖x‖) + π) {z | 0 ≤ z.im} z

Tactic:
refine
      (Real.continuousAt_arcsin.comp_continuousWithinAt
            ((continuous_im.continuousAt.comp_continuousWithinAt continuousWithinAt_neg).div
              continuous_norm.continuousWithinAt ?_)).add
        tendsto_const_nhds
    lift z to ℝ using him
    simpa using hre.ne

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

Goal state before:
pp: θ : Angle
⊢ (2 • θ).sign = θ.sign ↔ θ = ↑π ∨ |θ.toReal| < π / 2

Tactic:
rw [two_zsmul, ← two_nsmul, sign_two_nsmul_eq_sign_iff]

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

Goal state before:
pp: y : ℝ
hy : 0 < y
b : ℝ≥0
c : ℝ
hc : ∀ (a : ℝ), c ≤ a → ↑b ≤ a ^ y
⊢ ∃ i, ∀ (a : ℝ≥0), i ≤ a → b ≤ a ^ y

Tactic:
use c.toNNReal

Goal state after:
case h
y : ℝ
hy : 0 < y
b : ℝ≥0
c : ℝ
hc : ∀ (a : ℝ), c ≤ a → ↑b ≤ a ^ y
⊢ ∀ (a : ℝ≥0), c.toNNReal ≤ a → b ≤ a ^ y
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case pos
x : ℝ
hx : 0 ≤ x
y z : ℝ
H : 0 = x
h : y + z = 0
⊢ x ^ y * x ^ z ≤ x ^ (y + z)

pp: case neg
x : ℝ
hx : 0 ≤ x
y z : ℝ
H : 0 = x
h : ¬y + z = 0
⊢ x ^ y * x ^ z ≤ x ^ (y + z)

Tactic:
· simp only [H.symm, h, rpow_zero]
      calc
        (0 : ℝ) ^ y * 0 ^ z ≤ 1 * 1 := by
          gcongr
          exacts [zero_rpow_nonneg z, zero_rpow_le_one y, zero_rpow_le_one z]
        _ = 1 := by simp

Goal state after:
case neg
x : ℝ
hx : 0 ≤ x
y z : ℝ
H : 0 = x
h : ¬y + z = 0
⊢ x ^ y * x ^ z ≤ x ^ (y + z)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: case refine_1
𝕜 : Type u_2
inst✝ : RCLike 𝕜
g : ℕ → 𝕜
a : 𝕜
r : ℝ
hlim : Tendsto (fun n ↦ g n / ↑(↑n ^ r)) atTop (𝓝 a)
⊢ ∀ᶠ (x : ℕ) in atTop, ↑x ^ r = 0 → ‖g x‖ = 0

pp: case refine_2
𝕜 : Type u_2
inst✝ : RCLike 𝕜
g : ℕ → 𝕜
a : 𝕜
r : ℝ
hlim : Tendsto (fun n ↦ g n / ↑(↑n ^ r)) atTop (𝓝 a)
⊢ Tendsto ((fun x ↦ ‖g x‖) / fun n ↦ ↑n ^ r) atTop (𝓝 ‖a‖)

Tactic:
· filter_upwards [eventually_ne_atTop 0] with _ h
    simp [Real.rpow_eq_zero_iff_of_nonneg, h]

Goal state after:
case refine_2
𝕜 : Type u_2
inst✝ : RCLike 𝕜
g : ℕ → 𝕜
a : 𝕜
r : ℝ
hlim : Tendsto (fun n ↦ g n / ↑(↑n ^ r)) atTop (𝓝 a)
⊢ Tendsto ((fun x ↦ ‖g x‖) / fun n ↦ ↑n ^ r) atTop (𝓝 ‖a‖)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: 𝕜 : Type u_2
inst✝ : RCLike 𝕜
g : ℕ → 𝕜
a : 𝕜
r : ℝ
hlim : Tendsto (fun n ↦ g n / ↑(↑n ^ r)) atTop (𝓝 a)
n : ℕ
⊢ ‖g n / ↑(↑n ^ r)‖ = ((fun x ↦ ‖g x‖) / fun n ↦ ↑n ^ r) n

Tactic:
simp [abs_of_nonneg, show 0 ≤ (n : ℝ) ^ r by positivity]

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

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
y z : ℝ
⊢ ↑(x ^ (y * z)) = ↑((x ^ y) ^ z)

Tactic:
Complex.ofReal_cpow (rpow_nonneg hx _),

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

Goal state before:
pp: a b : ℂ
ha : a ≠ 0
cpow_eq : (fun x ↦ a ^ x) = fun x ↦ cexp (Complex.log a * x)
⊢ ContinuousAt (fun x ↦ a ^ x) b

Tactic:
cpow_eq

Goal state after:
a b : ℂ
ha : a ≠ 0
cpow_eq : (fun x ↦ a ^ x) = fun x ↦ cexp (Complex.log a * x)
⊢ ContinuousAt (fun x ↦ cexp (Complex.log a * x)) b
Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity

Goal state before:
pp: case inr.inr.hf
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : x < 0
A : ContinuousAt (fun p ↦ (-↑p.1, p.2)) (x, y)
⊢ ContinuousAt (fun p ↦ (-↑p.1) ^ p.2) (x, y)

Tactic:
refine (continuousAt_cpow (Or.inl ?_)).comp A
      rwa [neg_re, ofReal_re, neg_pos]

Goal state after: