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

Goal state before:
pp: f : CauSeq ℂ fun x ↦ ‖x‖
ε : ℝ
ε0 : ε > 0
i : ℕ
hi : ∀ j ≥ i, (fun x ↦ ‖x‖) (↑f j - ↑f i) < ε
j : ℕ
hj : j ≥ i
⊢ (fun x ↦ ‖x‖) ((fun n ↦ (starRingEnd ℂ) (↑f n)) j - (fun n ↦ (starRingEnd ℂ) (↑f n)) i) < ε

Tactic:
by
    simp_rw [← map_sub, norm_conj]; exact hi j hj

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.ContinuousLinearMap

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
inst✝⁷ : Ring 𝕜
inst✝⁶ : Ring 𝕜₂
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : SeminormedAddCommGroup F
inst✝³ : Module 𝕜 E
inst✝² : Module 𝕜₂ F
σ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
inst✝¹ : RingHomInvPair σ σ₂₁
inst✝ : RingHomInvPair σ₂₁ σ
a : ℝ
ha : 0 < a
f : E ≃ₛₗ[σ] F
⊢ (∀ (x : E), ‖f x‖ = a * ‖x‖) → ∀ (y : F), ‖f.symm y‖ = a⁻¹ * ‖y‖

Tactic:
by
  intro hf y
  simpa [eq_inv_mul_iff_mul_eq₀ (ne_of_gt ha)] using (hf (f.symm y)).symm

Goal state after:
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
x₁ y₁ x₂ y₂ : ℝ
⊢ (algebraMap ℝ A) (x₁ * x₂ - y₁ * y₂) + (x₁ * y₂ + y₁ * x₂) • I' =
    (algebraMap ℝ A) x₁ * (algebraMap ℝ A) x₂ + (algebraMap ℝ A) x₁ * y₂ • I' +
      (y₁ • I' * y₂ • I' + y₁ • I' * (algebraMap ℝ A) x₂)

Tactic:
add_add_add_comm

Goal state after:
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
I' : A
hf : I' * I' = -1
x₁ y₁ x₂ y₂ : ℝ
⊢ (algebraMap ℝ A) (x₁ * x₂ - y₁ * y₂) + (x₁ * y₂ + y₁ * x₂) • I' =
    (algebraMap ℝ A) x₁ * (algebraMap ℝ A) x₂ + y₁ • I' * y₂ • I' +
      ((algebraMap ℝ A) x₁ * y₂ • I' + y₁ • I' * (algebraMap ℝ A) x₂)
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ ↑(re (I * z)) = -(I * ((starRingEnd K) z - z) / 2)

Tactic:
re_eq_add_conj,

Goal state after:
K : Type u_1
inst✝ : RCLike K
z : K
⊢ (I * z + (starRingEnd K) (I * z)) / 2 = -(I * ((starRingEnd K) z - z) / 2)
Module: Mathlib.Analysis.Complex.Basic

Goal state before:
pp: ⊢ Metric.ball 1 1 ⊆ slitPlane

Tactic:
intro z hz

Goal state after:
z : ℂ
hz : z ∈ Metric.ball 1 1
⊢ z ∈ slitPlane
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ im z⁻¹ = -im z / normSq z

Tactic:
by
  rw [inv_def, normSq_eq_def', mul_comm, im_ofReal_mul, conj_im, div_eq_inv_mul]

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

Goal state before:
pp: case neg
K : Type u_1
inst✝ : RCLike K
h : ¬I = 0
⊢ I⁻¹ = -I

Tactic:
· field_simp
    linear_combination I_mul_I_of_nonzero h

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
n : ℤ
⊢ im ↑n = 0

Tactic:
by rw [← ofReal_intCast, ofReal_im]

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

Goal state before:
pp: X : Type u_1
Y : Type u_3
Z : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
e : OpenPartialHomeomorph X Y
f : Y → Z
s : Set Y
h : s ⊆ e.target
⊢ (∀ x ∈ s, ContinuousWithinAt f s x) ↔ ∀ ⦃x : Y⦄, x ∈ s → ContinuousWithinAt (f ∘ ↑e) (↑e.symm '' s) (↑e.symm x)

Tactic:
refine forall₂_congr fun x hx => ?_

Goal state after:
X : Type u_1
Y : Type u_3
Z : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
e : OpenPartialHomeomorph X Y
f : Y → Z
s : Set Y
h : s ⊆ e.target
x : Y
hx : x ∈ s
⊢ ContinuousWithinAt f s x ↔ ContinuousWithinAt (f ∘ ↑e) (↑e.symm '' s) (↑e.symm x)
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
F : Type u_4
E' : Type u_6
inst✝¹ : Norm F
inst✝ : SeminormedAddCommGroup E'
c₁ c₂ : ℝ
g : α → F
l : Filter α
f₁ f₂ : α → E'
h₁ : IsBigOWith c₁ l f₁ g
h₂ : IsBigOWith c₂ l f₂ g
⊢ IsBigOWith (c₁ + c₂) l (fun x ↦ f₁ x + f₂ x) g

Tactic:
rw [IsBigOWith_def] at *
  filter_upwards [h₁, h₂] with x hx₁ hx₂ using
    calc
      ‖f₁ x + f₂ x‖ ≤ c₁ * ‖g x‖ + c₂ * ‖g x‖ := norm_add_le_of_le hx₁ hx₂
      _ = (c₁ + c₂) * ‖g x‖ := (add_mul _ _ _).symm

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

Goal state before:
pp: α : Type u_1
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
f : α → E
g : α → F
⊢ f =O[⊤] g ↔ ∃ C, ∀ (x : α), ‖f x‖ ≤ C * ‖g x‖

Tactic:
simp_rw [isBigO_iff, eventually_top]

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

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

Tactic:
by 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
h₁ : ↑n.succ ≠ 1
h₂ : ↑n.succ ≠ 0
h₃ : ↑n.factorial * ↑n ≠ 0
h₄ : ↑n.succ - 1 = ↑n
⊢ ↑n.factorial * ↑n * ((↑n * ↑n.factorial)⁻¹ * (↑n.succ - (↑n.succ)⁻¹ ^ (j - n) * ↑n.succ)) =
    ↑n.succ - ↑n.succ * (↑n.succ)⁻¹ ^ (j - n)

Tactic:
← mul_assoc (n.factorial * n : α),

Goal state after:
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
n j : ℕ
hn : 0 < n
h₁ : ↑n.succ ≠ 1
h₂ : ↑n.succ ≠ 0
h₃ : ↑n.factorial * ↑n ≠ 0
h₄ : ↑n.succ - 1 = ↑n
⊢ ↑n.factorial * ↑n * (↑n * ↑n.factorial)⁻¹ * (↑n.succ - (↑n.succ)⁻¹ ^ (j - n) * ↑n.succ) =
    ↑n.succ - ↑n.succ * (↑n.succ)⁻¹ ^ (j - n)
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: r : ℝ
hr_nonneg : 0 ≤ r
hr_le : r ≤ 1
x y : ℂ
hyx : ‖y - x‖ < r
hy_eq : y = x + (y - x)
hyx_sq_le : ‖y - x‖ ^ 2 ≤ r * ‖y - x‖
⊢ ∀ (z : ℂ), ‖z‖ ≤ 1 → ‖cexp (x + z) - cexp x‖ ≤ ‖z‖ * ‖cexp x‖ + ‖cexp x‖ * ‖z‖ ^ 2

Tactic:
intro z hz

Goal state after:
r : ℝ
hr_nonneg : 0 ≤ r
hr_le : r ≤ 1
x y : ℂ
hyx : ‖y - x‖ < r
hy_eq : y = x + (y - x)
hyx_sq_le : ‖y - x‖ ^ 2 ≤ r * ‖y - x‖
z : ℂ
hz : ‖z‖ ≤ 1
⊢ ‖cexp (x + z) - cexp x‖ ≤ ‖z‖ * ‖cexp x‖ + ‖cexp x‖ * ‖z‖ ^ 2
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: k : ℕ
r : ℝ
hr : 0 < r
⊢ Summable fun n ↦ ↑n ^ k * rexp (-r) ^ n

Tactic:
apply summable_pow_mul_geometric_of_norm_lt_one

Goal state after:
k : ℕ
r : ℝ
hr : 0 < r
⊢ ‖rexp (-r)‖ < 1
Module: Mathlib.Analysis.Normed.Group.Pointwise

Goal state before:
pp: E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
x y : E
⊢ x • closedBall y δ = closedBall (x • y) δ

Tactic:
smul_closedBall

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

Goal state before:
pp: ⊢ cos (π / 4) = √2 / 2

Tactic:
trans cos (π / 2 ^ 2)
  · congr
    norm_num
  · simp

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

Goal state before:
pp: case inr.coe
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ : ℝ
hδ : 0 < δ
s : Set E
x : E
hs : ENNReal.ofReal δ ≤ infEDist x s
z : E
hz : z ∈ s
r : NNReal
h : dist x z < δ + (↑r - δ)
hr : 0 < ↑r - δ
y : E
hxy : dist x y < ↑r - δ
hyz : dist y z < δ
⊢ ENNReal.ofReal (↑r - δ) + ENNReal.ofReal δ ≤ ↑r

Tactic:
← ofReal_add hr.le hδ.le,

Goal state after:
case inr.coe
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ : ℝ
hδ : 0 < δ
s : Set E
x : E
hs : ENNReal.ofReal δ ≤ infEDist x s
z : E
hz : z ∈ s
r : NNReal
h : dist x z < δ + (↑r - δ)
hr : 0 < ↑r - δ
y : E
hxy : dist x y < ↑r - δ
hyz : dist y z < δ
⊢ ENNReal.ofReal (↑r - δ + δ) ≤ ↑r
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

Goal state before:
pp: case inr
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
c : 𝕜
x : E
r : ℝ
hr : 0 ≤ r
hc : c ≠ 0
⊢ c • sphere x r = sphere (c • x) (‖c‖ * r)

Tactic:
· exact smul_sphere' hc x r

Goal state after:
Module: Mathlib.Topology.Path

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
⊢ ofLine ⋯ ⋯ ⋯ = γ

Tactic:
ext t

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
t : ↑I
⊢ (ofLine ⋯ ⋯ ⋯) t = γ t
Module: Mathlib.Topology.Path

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y z : X
γ : Path x y
γ' : Path y z
⊢ (γ.trans γ').symm = γ'.symm.trans γ.symm

Tactic:
ext t

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
x y z : X
γ : Path x y
γ' : Path y z
t : ↑I
⊢ (γ.trans γ').symm t = (γ'.symm.trans γ.symm) t
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: case mpr
X : Type u_2
Y : Type u_3
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : WeaklyLocallyCompactSpace X
inst✝¹ : T2Space Y
ι : Type u_6
l : Filter ι
inst✝ : l.NeBot
F : ι → C(X, Y)
f : (s : Set X) → IsCompact s → C(↑s, Y)
hf : ∀ (s : Set X) (a : IsCompact s), Tendsto (fun i ↦ restrict s (F i)) l (𝓝 (f s a))
h :
  ∀ (s₁ : Set X) (hs₁ : IsCompact s₁) (s₂ : Set X) (hs₂ : IsCompact s₂) (x : X) (hxs₁ : x ∈ s₁) (hxs₂ : x ∈ s₂),
    (f s₁ hs₁) ⟨x, hxs₁⟩ = (f s₂ hs₂) ⟨x, hxs₂⟩
s : Set X
hs : IsCompact s
⊢ Tendsto (fun i ↦ restrict s (F i)) l
    (𝓝 (restrict s (liftCover' (fun s ↦ ∀ ⦃f : Filter X⦄ [f.NeBot], f ≤ 𝓟 s → ∃ x ∈ s, ClusterPt x f) f h ⋯)))

Tactic:
rw [liftCover_restrict']

Goal state after:
case mpr
X : Type u_2
Y : Type u_3
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : WeaklyLocallyCompactSpace X
inst✝¹ : T2Space Y
ι : Type u_6
l : Filter ι
inst✝ : l.NeBot
F : ι → C(X, Y)
f : (s : Set X) → IsCompact s → C(↑s, Y)
hf : ∀ (s : Set X) (a : IsCompact s), Tendsto (fun i ↦ restrict s (F i)) l (𝓝 (f s a))
h :
  ∀ (s₁ : Set X) (hs₁ : IsCompact s₁) (s₂ : Set X) (hs₂ : IsCompact s₂) (x : X) (hxs₁ : x ∈ s₁) (hxs₂ : x ∈ s₂),
    (f s₁ hs₁) ⟨x, hxs₁⟩ = (f s₂ hs₂) ⟨x, hxs₂⟩
s : Set X
hs : IsCompact s
⊢ Tendsto (fun i ↦ restrict s (F i)) l (𝓝 (f s ?m.230))

X : Type u_2
Y : Type u_3
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : WeaklyLocallyCompactSpace X
inst✝¹ : T2Space Y
ι : Type u_6
l : Filter ι
inst✝ : l.NeBot
F : ι → C(X, Y)
f : (s : Set X) → IsCompact s → C(↑s, Y)
hf : ∀ (s : Set X) (a : IsCompact s), Tendsto (fun i ↦ restrict s (F i)) l (𝓝 (f s a))
h :
  ∀ (s₁ : Set X) (hs₁ : IsCompact s₁) (s₂ : Set X) (hs₂ : IsCompact s₂) (x : X) (hxs₁ : x ∈ s₁) (hxs₂ : x ∈ s₂),
    (f s₁ hs₁) ⟨x, hxs₁⟩ = (f s₂ hs₂) ⟨x, hxs₂⟩
s : Set X
hs : IsCompact s
⊢ s ∈ fun s ↦ ∀ ⦃f : Filter X⦄ [f.NeBot], f ≤ 𝓟 s → ∃ x ∈ s, ClusterPt x f
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: α : Type u_1
inst✝¹ : NormedDivisionRing α
inst✝ : CompleteSpace α
f : ℕ → α
w z : α
h : CauchySeq fun n ↦ ∑ i ∈ Finset.range n, f i * w ^ i
hz : ‖z‖ < ‖w‖
hw : 0 < ‖w‖
C : ℝ
hC : ∀ (n : ℕ), ‖f n * w ^ n‖ ≤ C
⊢ Summable fun n ↦ f n * z ^ n

Tactic:
rw [summable_iff_cauchySeq_finset]

Goal state after:
α : Type u_1
inst✝¹ : NormedDivisionRing α
inst✝ : CompleteSpace α
f : ℕ → α
w z : α
h : CauchySeq fun n ↦ ∑ i ∈ Finset.range n, f i * w ^ i
hz : ‖z‖ < ‖w‖
hw : 0 < ‖w‖
C : ℝ
hC : ∀ (n : ℕ), ‖f n * w ^ n‖ ≤ C
⊢ CauchySeq fun s ↦ ∑ b ∈ s, f b * z ^ b
Module: Mathlib.Topology.Path

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
a b c : X
γ₁ : Path a b
γ₂ : Path b c
⊢ ⇑γ₁.extend '' HMul.hMul 2 '' Iic (1 / 2) ∪ (fun x ↦ γ₂.extend (x - 1)) '' HMul.hMul 2 '' Ici (1 / 2) =
    range ⇑γ₁ ∪ range ⇑γ₂

Tactic:
← image_image γ₂.extend

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
a b c : X
γ₁ : Path a b
γ₂ : Path b c
⊢ ⇑γ₁.extend '' HMul.hMul 2 '' Iic (1 / 2) ∪ ⇑γ₂.extend '' (fun x ↦ x - 1) '' HMul.hMul 2 '' Ici (1 / 2) =
    range ⇑γ₁ ∪ range ⇑γ₂
Module: Mathlib.Topology.Path

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y : X
γ : Path x y
f : X → Y
h : Continuous[inst✝¹, inst✝] f
⊢ ⇑(γ.map h) = f ∘ ⇑γ

Tactic:
ext t

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y : X
γ : Path x y
f : X → Y
h : Continuous[inst✝¹, inst✝] f
t : ↑I
⊢ (γ.map h) t = (f ∘ ⇑γ) t
Module: Mathlib.Topology.Path

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
γ : Path x y
γ' : Path y z
f : X → Y
h : Continuous[inst✝¹, inst✝] f
⊢ (γ.trans γ').map h = (γ.map h).trans (γ'.map h)

Tactic:
ext t

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
γ : Path x y
γ' : Path y z
f : X → Y
h : Continuous[inst✝¹, inst✝] f
t : ↑I
⊢ ((γ.trans γ').map h) t = ((γ.map h).trans (γ'.map h)) t
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: E : Type u_4
inst✝⁴ : Ring E
inst✝³ : PartialOrder E
inst✝² : IsOrderedRing E
inst✝¹ : TopologicalSpace E
inst✝ : OrderClosedTopology E
l : E
f : ℕ → E
hfl : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, (-1) ^ i * f i) atTop (𝓝 l)
hfm : Monotone f
k : ℕ
ha : Antitone fun n ↦ ∑ i ∈ Finset.range (2 * n), (-1) ^ i * f i
n : ℕ
⊢ id n ≤ 2 * n

Tactic:
dsimp; lia

Goal state after:
Module: Mathlib.Topology.Path

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
f : ↑I → ↑I
hfcont : Continuous f
hf₀ : f 0 = 0
hf₁ : f 1 = 1
⊢ range ⇑(γ.reparam f hfcont hf₀ hf₁) = range ⇑γ

Tactic:
change range (γ ∘ f) = range γ

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
f : ↑I → ↑I
hfcont : Continuous f
hf₀ : f 0 = 0
hf₁ : f 1 = 1
⊢ range (⇑γ ∘ f) = range ⇑γ
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: E : Type u_4
inst✝⁴ : Ring E
inst✝³ : PartialOrder E
inst✝² : IsOrderedRing E
inst✝¹ : TopologicalSpace E
inst✝ : OrderClosedTopology E
l : E
f : ℕ → E
hfl : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, (-1) ^ i * f i) atTop (𝓝 l)
hfm : Monotone f
k : ℕ
hm : Monotone fun n ↦ ∑ i ∈ Finset.range (2 * n + 1), (-1) ^ i * f i
n : ℕ
⊢ id n ≤ 2 * n + 1

Tactic:
dsimp; lia

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

Goal state before:
pp: E : Type u_4
inst✝⁴ : Ring E
inst✝³ : PartialOrder E
inst✝² : IsOrderedRing E
inst✝¹ : TopologicalSpace E
inst✝ : OrderClosedTopology E
l : E
f : ℕ → E
hfl : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, (-1) ^ i * f i) atTop (𝓝 l)
hfa : Antitone f
k : ℕ
hm : Monotone fun n ↦ ∑ i ∈ Finset.range (2 * n), (-1) ^ i * f i
n : ℕ
⊢ id n ≤ 2 * n

Tactic:
dsimp; lia

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

Goal state before:
pp: E : Type u_4
inst✝⁴ : Ring E
inst✝³ : PartialOrder E
inst✝² : IsOrderedRing E
inst✝¹ : TopologicalSpace E
inst✝ : OrderClosedTopology E
l : E
f : ℕ → E
hfl : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, (-1) ^ i * f i) atTop (𝓝 l)
hfa : Antitone f
k : ℕ
ha : Antitone fun n ↦ ∑ i ∈ Finset.range (2 * n + 1), (-1) ^ i * f i
n : ℕ
⊢ id n ≤ 2 * n + 1

Tactic:
dsimp; lia

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

Goal state before:
pp: x y : ℝ
hx : x ∈ Icc (-1) 1
hy : y ∈ Icc (-(π / 2)) (π / 2)
⊢ x ≤ sin y ↔ x ≤ sin (arcsin (sin y))

Tactic:
arcsin_sin' hy

Goal state after:
x y : ℝ
hx : x ∈ Icc (-1) 1
hy : y ∈ Icc (-(π / 2)) (π / 2)
⊢ x ≤ sin y ↔ x ≤ sin y
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

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

Tactic:
by 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:
by nlinarith

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

Goal state before:
pp: x : ℝ
hx : 0 < x
⊢ rexp (log x) = x

Tactic:
by
  rw [exp_log_eq_abs hx.ne']
  exact abs_of_pos hx

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

Goal state before:
pp: case neg
x : ℝ
hx0 : ¬x ≤ 0
h : log x + 1 ≤ rexp (log x)
⊢ rexp 1 * x ≤ rexp x

Tactic:
rwa [← exp_le_exp, exp_add, exp_log (lt_of_not_ge hx0), mul_comm] at h

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

Goal state before:
pp: case neg.mpr
y : ℝ
h₀ : ¬{ re := 0, im := y } = 0
hy : y < 0
⊢ { re := 0, im := y }.arg = (-I).arg

Tactic:
← arg_real_mul (-I) (neg_pos.2 hy),

Goal state after:
case neg.mpr
y : ℝ
h₀ : ¬{ re := 0, im := y } = 0
hy : y < 0
⊢ { re := 0, im := y }.arg = (↑(-y) * -I).arg
Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex

Goal state before:
pp: case refine_2
n m : ℕ
z : ℂ
⊢ ↑m * (↑n).arg ≤ π

Tactic:
simp only [natCast_arg, mul_zero, pi_pos.le]

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

Goal state before:
pp: case inr
θ : Angle
h : θ ≠ ↑π
⊢ |(-θ).toReal| = |θ.toReal|

Tactic:
· simp [toReal_neg_eq_neg_toReal_iff.2 h]

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

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

pp: case mp.inr
a b : Angle
ha : a.sign ≠ 0
h : a.sign = b.sign
h2 : a = b + ↑π
⊢ a = b

Tactic:
· exact h1

Goal state after:
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 inr
x y : ℝ
hx : x < 0
⊢ |x ^ y| ≤ |x| ^ y

Tactic:
rw [abs_of_neg hx, rpow_def_of_neg hx, rpow_def_of_pos (neg_pos.2 hx), log_neg_eq_log, abs_mul,
      abs_of_pos (exp_pos _)]
    exact mul_le_of_le_one_right (exp_pos _).le (abs_cos_le_one _)

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

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

Tactic:
rw [zero_rpow h, zero_eq_mul]

Goal state after:
case inl
y z : ℝ
h : y + z ≠ 0
hx : 0 ≤ 0
⊢ 0 ^ y = 0 ∨ 0 ^ z = 0
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℂ
y : ℝ
⊢ x ^ ↑y = ↑(‖x‖ ^ y) * (↑(Real.cos (x.arg * y)) + ↑(Real.sin (x.arg * y)) * I)

Tactic:
by
  rcases eq_or_ne x 0 with rfl | hx
  · simp [ofReal_cpow le_rfl]
  · rw [cpow_def_of_ne_zero hx, exp_eq_exp_re_mul_sin_add_cos, mul_comm (log x)]
    norm_cast
    rw [re_ofReal_mul, im_ofReal_mul, log_re, log_im, mul_comm y, mul_comm y, Real.exp_mul,
      Real.exp_log]
    rwa [norm_pos_iff]

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

Goal state before:
pp: r : ℝ
hr : r < 0
x : ℝ
hx : x ∈ Set.Icc 0 1
⊢ x ∈ {x | (fun x ↦ (fun x ↦ -|log x| ^ 1) x = log x) x}

Tactic:
by
      simp [abs_of_nonpos (log_nonpos hx.1 hx.2)]

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

Goal state before:
pp: h : Tendsto (fun x ↦ log x * x) (𝓝[>] 0) (𝓝 0)
h_eq : ∀ x ∈ Set.Iio 0, (-(fun x ↦ log x * x) ∘ fun x ↦ |x|) x = log x * x
⊢ Tendsto (fun x ↦ log x * x) (𝓝[<] 0) (𝓝 0)

Tactic:
refine tendsto_nhdsWithin_congr h_eq ?_

Goal state after:
h : Tendsto (fun x ↦ log x * x) (𝓝[>] 0) (𝓝 0)
h_eq : ∀ x ∈ Set.Iio 0, (-(fun x ↦ log x * x) ∘ fun x ↦ |x|) x = log x * x
⊢ Tendsto (-(fun x ↦ log x * x) ∘ fun x ↦ |x|) (𝓝[<] 0) (𝓝 0)
Module: Mathlib.GroupTheory.GroupAction.Pointwise

Goal state before:
pp: M : Type u_1
N : Type u_2
F : Type u_3
α : Type u_4
β : Type u_5
σ : M → N
inst✝³ : SMul M α
inst✝² : SMul N β
inst✝¹ : FunLike F α β
inst✝ : MulActionSemiHomClass F σ α β
f : F
t : Set β
c : M
hc : Surjective fun m ↦ c • m
hc' : Injective fun n ↦ σ c • n
⊢ ⇑f ⁻¹' (σ c • t) = c • ⇑f ⁻¹' t

Tactic:
by
  refine Subset.antisymm ?_ (smul_preimage_set_subsetₛₗ f c t)
  rw [subset_def, hc.forall]
  rintro x ⟨y, hy, hxy⟩
  rw [map_smulₛₗ, hc'.eq_iff] at hxy
  subst y
  exact smul_mem_smul_set hy

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

Goal state before:
pp: y : ℝ
x : ℝ≥0∞
hx : 0 < x
hx' : x ≠ ∞
h : x ^ y = ∞
⊢ False

Tactic:
by simp [rpow_eq_top_iff, hx.ne', hx'] at h

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

Goal state before:
pp: x y : ℝ
n : ℤ
hx : 0 < x
hy : 0 < y
⊢ x ^ n ≤ y ↔ ↑n * log x ≤ log y

Tactic:
by
  rw [← rpow_le_iff_le_log hx hy, rpow_intCast]

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

Goal state before:
pp: x y : ℝ
hx : 0 < x
⊢ rexp (log x * y) ≤ 1 ↔ 1 ≤ x ∧ y ≤ 0 ∨ x ≤ 1 ∧ 0 ≤ y

Tactic:
exp_le_one_iff,

Goal state after:
x y : ℝ
hx : 0 < x
⊢ log x * y ≤ 0 ↔ 1 ≤ x ∧ y ≤ 0 ∨ x ≤ 1 ∧ 0 ≤ y
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case inl
x y : ℝ≥0∞
p : ℝ
hp : 0 ≤ p
hxy : x ≤ y
⊢ max x y ^ p = max (x ^ p) (y ^ p)

Tactic:
rw [max_eq_right hxy, max_eq_right (rpow_le_rpow hxy hp)]

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

Goal state before:
pp: b : ℝ
hb₀ : 0 < b
hb₁ : b < 1
⊢ StrictAnti fun x ↦ b ^ x

Tactic:
simp_rw [Real.rpow_def_of_pos hb₀]
  exact exp_strictMono.comp_strictAnti <| StrictMono.const_mul_of_neg strictMono_id
      <| Real.log_neg hb₀ hb₁

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

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

Tactic:
by
  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]
  exacts [norm_nonneg _, (neg_pi_lt_arg _).le, arg_le_pi _]

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

Goal state before:
pp: z : ℝ
hz : z < 0
x : ℝ≥0
hx1 : 0 < x
hx2 : x < 1
⊢ 1 < ↑x ^ z

Tactic:
simp [← coe_rpow_of_ne_zero (ne_of_gt hx1), NNReal.one_lt_rpow_of_pos_of_lt_one_of_neg hx1 hx2 hz]

Goal state after:
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
u : Rˣ
v : Ray R M
⊢ -u • v = -(u • v)

Tactic:
by
  induction v using Module.Ray.ind
  simp only [smul_rayOfNeZero, Units.smul_def, Units.val_neg, neg_smul, neg_rayOfNeZero]

Goal state after:
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsTorsionFree R M
v : M
r : R
hv : v ≠ 0
hr : r ≠ 0
⊢ SameRay R (-v) (r • v) ↔ r < 0

Tactic:
by
  simp only [sameRay_neg_smul_right_iff, hv, or_false, hr.le_iff_lt]

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap

Goal state before:
pp: k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
V3 : Type u_6
P3 : Type u_7
V4 : Type u_8
P4 : Type u_9
inst✝¹² : Ring k
inst✝¹¹ : AddCommGroup V1
inst✝¹⁰ : Module k V1
inst✝⁹ : AffineSpace V1 P1
inst✝⁸ : AddCommGroup V2
inst✝⁷ : Module k V2
inst✝⁶ : AffineSpace V2 P2
inst✝⁵ : AddCommGroup V3
inst✝⁴ : Module k V3
inst✝³ : AffineSpace V3 P3
inst✝² : AddCommGroup V4
inst✝¹ : Module k V4
inst✝ : AffineSpace V4 P4
f g : P1 →ᵃ[k] V2
p : P1
v : V1
⊢ (⇑f - ⇑g) (v +ᵥ p) = (f.linear - g.linear) v +ᵥ (⇑f - ⇑g) p

Tactic:
by simp [sub_add_sub_comm]

Goal state after:
Module: Mathlib.Analysis.Convex.Star

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁷ : Ring 𝕜
inst✝⁶ : PartialOrder 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : PartialOrder E
inst✝³ : IsOrderedAddMonoid E
inst✝² : Module 𝕜 E
inst✝¹ : IsStrictOrderedModule 𝕜 E
inst✝ : PosSMulReflectLT 𝕜 E
x y : E
h : x < y
z : E
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hz : a • y + b • z ≤ x
⊢ (a + b) • x - a • y < b • x

Tactic:
by
      rw [add_smul, sub_lt_iff_lt_add']
      gcongr

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : Ring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
hs : Convex 𝕜 s
ht : Convex 𝕜 t
⊢ Convex 𝕜 (s - t)

Tactic:
by
  rw [sub_eq_add_neg]
  exact hs.add ht.neg

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
F : Type u_4
inst✝² : SeminormedRing 𝕜
inst✝¹ : SMul 𝕜 E
inst✝ : SMul 𝕜 F
s : Set F
hs : Balanced 𝕜 s
f : E →ₑ[id] F
a : 𝕜
ha : ‖a‖ ≤ 1
x : E
x✝ : x ∈ a • ⇑f ⁻¹' s
y : E
hy₁ : y ∈ ⇑f ⁻¹' s
hy₂ : (fun x ↦ a • x) y = x
⊢ f x ∈ s

Tactic:
← hy₂,

Goal state after:
𝕜 : Type u_1
E : Type u_3
F : Type u_4
inst✝² : SeminormedRing 𝕜
inst✝¹ : SMul 𝕜 E
inst✝ : SMul 𝕜 F
s : Set F
hs : Balanced 𝕜 s
f : E →ₑ[id] F
a : 𝕜
ha : ‖a‖ ≤ 1
x : E
x✝ : x ∈ a • ⇑f ⁻¹' s
y : E
hy₁ : y ∈ ⇑f ⁻¹' s
hy₂ : (fun x ↦ a • x) y = x
⊢ f ((fun x ↦ a • x) y) ∈ s