mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.Manifold.VectorBundle.Basic

Goal state before:
pp: B : Type u_2
F : Type u_4
E : B → Type u_6
inst✝⁶ : TopologicalSpace F
inst✝⁵ : TopologicalSpace (TotalSpace F E)
inst✝⁴ : (x : B) → TopologicalSpace (E x)
HB : Type u_7
inst✝³ : TopologicalSpace HB
inst✝² : TopologicalSpace B
inst✝¹ : ChartedSpace HB B
inst✝ : FiberBundle F E
x : TotalSpace F E
⊢ chartAt (ModelProd HB F) x =
    (trivializationAt F E x.proj).toOpenPartialHomeomorph ≫ₕ (chartAt HB x.proj).prod (OpenPartialHomeomorph.refl F)

Tactic:
dsimp only [chartAt_comp, prodChartedSpace_chartAt, FiberBundle.chartedSpace'_chartAt,
    chartAt_self_eq]

Goal state after:
B : Type u_2
F : Type u_4
E : B → Type u_6
inst✝⁶ : TopologicalSpace F
inst✝⁵ : TopologicalSpace (TotalSpace F E)
inst✝⁴ : (x : B) → TopologicalSpace (E x)
HB : Type u_7
inst✝³ : TopologicalSpace HB
inst✝² : TopologicalSpace B
inst✝¹ : ChartedSpace HB B
inst✝ : FiberBundle F E
x : TotalSpace F E
⊢ (trivializationAt F E x.proj).toOpenPartialHomeomorph ≫ₕ
      (chartAt HB (↑(trivializationAt F E x.proj).toOpenPartialHomeomorph x).1).prod (OpenPartialHomeomorph.refl F) =
    (trivializationAt F E x.proj).toOpenPartialHomeomorph ≫ₕ (chartAt HB x.proj).prod (OpenPartialHomeomorph.refl F)
Module: Mathlib.Geometry.Manifold.VectorBundle.Tangent

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
n : ℕ∞ω
E : Type u_2
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹¹ : NormedAddCommGroup E'
inst✝¹⁰ : NormedSpace 𝕜 E'
H : Type u_4
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝⁸ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_6
inst✝⁷ : TopologicalSpace M
inst✝⁶ : ChartedSpace H M
M' : Type u_7
inst✝⁵ : TopologicalSpace M'
inst✝⁴ : ChartedSpace H' M'
F : Type u_8
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : IsManifold I 1 M
inst✝ : IsManifold I' 1 M'
i : ↑(atlas H M)
x : M
hx : x ∈ (↑i).source
v : E
⊢ UniqueDiffWithinAt 𝕜 (range ↑I) (↑((↑i).extend I) x)

Tactic:
exact I.uniqueDiffWithinAt_image

Goal state after:
Module: Mathlib.Geometry.Manifold.VectorBundle.Tangent

Goal state before:
pp: case hxs
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
n : ℕ∞ω
E : Type u_2
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹¹ : NormedAddCommGroup E'
inst✝¹⁰ : NormedSpace 𝕜 E'
H : Type u_4
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝⁸ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_6
inst✝⁷ : TopologicalSpace M
inst✝⁶ : ChartedSpace H M
M' : Type u_7
inst✝⁵ : TopologicalSpace M'
inst✝⁴ : ChartedSpace H' M'
F : Type u_8
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : IsManifold I 1 M
inst✝ : IsManifold I' 1 M'
this : IsManifold I (0 + 1) M
i j k : ↑(atlas H M)
x : M
hxk : x ∈ (↑k).source
hxi : x ∈ (↑i).source
hxj : x ∈ (↑j).source
v : E
⊢ UniqueDiffWithinAt 𝕜 (range ↑I) (↑((↑i).extend I) x)

Tactic:
exact I.uniqueDiffWithinAt_image

Goal state after:
Module: Mathlib.Topology.ShrinkingLemma

Goal state before:
pp: ι : Type u_1
X : Type u_2
inst✝ : TopologicalSpace X
u : ι → Set X
s : Set X
p : Set X → Prop
c : Set (PartialRefinement u s p)
hc : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
ne : c.Nonempty
hfin : ∀ x ∈ s, {i | x ∈ u i}.Finite
hU : s ⊆ ⋃ i, u i
i : ι
hi : i ∈ chainSupCarrier c
v : PartialRefinement u s p
hv : v ∈ c ∧ i ∈ v.carrier
⊢ p ((find c ne i).toFun i)

Tactic:
find_apply_of_mem hc ne hv.1 hv.2

Goal state after:
ι : Type u_1
X : Type u_2
inst✝ : TopologicalSpace X
u : ι → Set X
s : Set X
p : Set X → Prop
c : Set (PartialRefinement u s p)
hc : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
ne : c.Nonempty
hfin : ∀ x ∈ s, {i | x ∈ u i}.Finite
hU : s ⊆ ⋃ i, u i
i : ι
hi : i ∈ chainSupCarrier c
v : PartialRefinement u s p
hv : v ∈ c ∧ i ∈ v.carrier
⊢ p (v.toFun i)
Module: Mathlib.Topology.ShrinkingLemma

Goal state before:
pp: ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
u : ι → Set X
s : Set X
inst✝ : NormalSpace X
v : PartialRefinement u s ⊤
hs : IsClosed s
i : ι
hi : i ∉ v.carrier
I : s ∩ ⋂ j, ⋂ (_ : j ≠ i), (v.toFun j)ᶜ ⊆ v.toFun i
C : IsClosed (s ∩ ⋂ j, ⋂ (_ : j ≠ i), (v.toFun j)ᶜ)
⊢ ∃ v', v < v'

Tactic:
rcases normal_exists_closure_subset C (v.isOpen i) I with ⟨vi, ovi, hvi, cvi⟩

Goal state after:
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
u : ι → Set X
s : Set X
inst✝ : NormalSpace X
v : PartialRefinement u s ⊤
hs : IsClosed s
i : ι
hi : i ∉ v.carrier
I : s ∩ ⋂ j, ⋂ (_ : j ≠ i), (v.toFun j)ᶜ ⊆ v.toFun i
C : IsClosed (s ∩ ⋂ j, ⋂ (_ : j ≠ i), (v.toFun j)ᶜ)
vi : Set X
ovi : IsOpen vi
hvi : s ∩ ⋂ j, ⋂ (_ : j ≠ i), (v.toFun j)ᶜ ⊆ vi
cvi : closure vi ⊆ v.toFun i
⊢ ∃ v', v < v'
Module: Mathlib.Topology.ShrinkingLemma

Goal state before:
pp: ι : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
u : ι → Set X
s : Set X
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
v : PartialRefinement u s fun w ↦ IsCompact (closure w)
hs : IsCompact s
i : ι
hi : i ∉ v.carrier
si : Set X := ⋯
hsi : si = s ∩ ⋂ i_1, ⋂ (_ : ¬i_1 = i), (v.toFun i_1)ᶜ
hsic : IsCompact si
x : X
hx : x ∈ s ∩ ⋂ i_1, ⋂ (_ : ¬i_1 = i), (v.toFun i_1)ᶜ
j : ι
hj : j ≠ i
⊢ x ∈ (v.toFun j)ᶜ

Tactic:
have hsi' : x ∈ (⋂ i_1, ⋂ (_ : ¬i_1 = i), (v.toFun i_1)ᶜ) := Set.mem_of_mem_inter_right hx

Goal state after:
ι : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
u : ι → Set X
s : Set X
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
v : PartialRefinement u s fun w ↦ IsCompact (closure w)
hs : IsCompact s
i : ι
hi : i ∉ v.carrier
si : Set X := s ∩ (⋃ j, ⋃ (_ : j ≠ i), v.toFun j)ᶜ
hsi : si = s ∩ ⋂ i_1, ⋂ (_ : ¬i_1 = i), (v.toFun i_1)ᶜ
hsic : IsCompact si
x : X
hx : x ∈ s ∩ ⋂ i_1, ⋂ (_ : ¬i_1 = i), (v.toFun i_1)ᶜ
j : ι
hj : j ≠ i
hsi' : x ∈ ⋂ i_1, ⋂ (_ : ¬i_1 = i), (v.toFun i_1)ᶜ
⊢ x ∈ (v.toFun j)ᶜ
Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hf : Integrable f μ
hg : Integrable g μ
hf_le : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∫ (x : α) in s, f x ∂μ ≤ ∫ (x : α) in s, g x ∂μ
s : Set α
hs : MeasurableSet s
⊢ μ s < ∞ → ∫ (a : α) in s, f a ∂μ ≤ ∫ (a : α) in s, g a ∂μ

Tactic:
exact hf_le s hs

Goal state after:
Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral

Goal state before:
pp: E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : CompleteSpace E
β : Type u_3
inst✝⁴ : TopologicalSpace β
inst✝³ : MeasurableSpace β
inst✝² : BorelSpace β
inst✝¹ : SigmaCompactSpace β
inst✝ : R1Space β
μ : Measure β
f : β → E
hf : Integrable f μ
h'f : ∀ (s : Set β), IsCompact s → ∫ (x : β) in s, f x ∂μ = 0
s : Set β
hs : IsClosed[inst✝⁴] s
t : ℕ → Set β := fun n ↦ closure[inst✝⁴] (compactCovering β n) ∩ s
H : Tendsto (fun n ↦ ∫ (x : β) in t n, f x ∂μ) atTop (𝓝 (∫ (x : β) in s, f x ∂μ))
⊢ ∫ (x : β) in s, f x ∂μ = 0

Tactic:
by
    have A : ∀ n, ∫ x in t n, f x ∂μ = 0 :=
      fun n ↦ h'f _ ((isCompact_compactCovering β n).closure.inter_right hs)
    simp_rw [A, tendsto_const_nhds_iff] at H
    exact H.symm

Goal state after:
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun

Goal state before:
pp: case μB
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → F
d b η : ℝ
hdb✝ : d ≤ b
hf : ∀ᵐ (x : ℝ), x ∈ Ioo d b → HasDerivAt f (f' x) x
hη : 0 < η
hdb : d < b
t : Set (ℝ × ℝ) := ⋯
s : Set ℝ := ⋯
⊢ ∀ a ∈ t, volume (Metric.closedBall a.1 (3 * (Prod.snd - Prod.fst) a)) ≤ ↑6 * volume (Icc a.1 a.2)

Tactic:
intro A hA

Goal state after:
case μB
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → F
d b η : ℝ
hdb✝ : d ≤ b
hf : ∀ᵐ (x : ℝ), x ∈ Ioo d b → HasDerivAt f (f' x) x
hη : 0 < η
hdb : d < b
t : Set (ℝ × ℝ) := {z | (d < z.1 ∧ z.1 < z.2 ∧ z.2 < b) ∧ dist (slope f z.1 z.2) (f' z.1) < η}
s : Set ℝ := {x | x ∈ Ioo d b ∧ HasDerivAt f (f' x) x}
A : ℝ × ℝ
hA : A ∈ t
⊢ volume (Metric.closedBall A.1 (3 * (Prod.snd - Prod.fst) A)) ≤ ↑6 * volume (Icc A.1 A.2)
Module: Mathlib.Analysis.Calculus.Taylor

Goal state before:
pp: case e_a
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
n : ℕ
s : Set ℝ
x₀ x : ℝ
⊢ (x - x₀) ^ (n + 1) • taylorCoeffWithin f (n + 1) s x₀ =
    ((↑n !)⁻¹ * (↑n + 1)⁻¹ * (x - x₀) ^ (n + 1)) • iteratedDerivWithin (n + 1) f s x₀

Tactic:
dsimp only [taylorCoeffWithin]

Goal state after:
case e_a
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
n : ℕ
s : Set ℝ
x₀ x : ℝ
⊢ (x - x₀) ^ (n + 1) • (↑(n + 1)!)⁻¹ • iteratedDerivWithin (n + 1) f s x₀ =
    ((↑n !)⁻¹ * (↑n + 1)⁻¹ * (x - x₀) ^ (n + 1)) • iteratedDerivWithin (n + 1) f s x₀
Module: Mathlib.Analysis.Calculus.Taylor

Goal state before:
pp: E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
s : Set ℝ
x₀ x : ℝ
⊢ (PolynomialModule.eval x)
      (∑ k ∈ Finset.range (0 + 1),
        (PolynomialModule.comp (Polynomial.X - Polynomial.C x₀))
          (PolynomialModule.single ℝ k (taylorCoeffWithin f k s x₀))) =
    f x₀

Tactic:
dsimp only [taylorCoeffWithin]

Goal state after:
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
s : Set ℝ
x₀ x : ℝ
⊢ (PolynomialModule.eval x)
      (∑ k ∈ Finset.range (0 + 1),
        (PolynomialModule.comp (Polynomial.X - Polynomial.C x₀))
          (PolynomialModule.single ℝ k ((↑k !)⁻¹ • iteratedDerivWithin k f s x₀))) =
    f x₀
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun

Goal state before:
pp: F✝ : Type u_2
inst✝³ : NormedAddCommGroup F✝
inst✝² : NormedSpace ℝ F✝
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
hf₀ : ∀ᵐ (x : ℝ), x ∈ Icc a b → HasDerivAt f 0 x
hab : a ≤ b
d : ℝ
hd : d ∈ Icc a b
this : f d ≠ f b
⊢ ∃ r > 0, r < dist (f d) (f b)

Tactic:
exact exists_between (dist_pos.mpr this)

Goal state after:
Module: Mathlib.Analysis.Calculus.Taylor

Goal state before:
pp: F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : ℝ → F
x x₀ : ℝ
n : ℕ
hf : ContDiffOn ℝ (↑(n + 1)) f [[x₀, x]]
this✝ : x₀ ≠ x
this : UniqueDiffOn ℝ [[x₀, x]]
k : ℕ
hk : k ≤ n
⊢ k ≤ n + 1

Tactic:
omega

Goal state after:
Module: Mathlib.Analysis.Calculus.Taylor

Goal state before:
pp: F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : ℝ → F
x x₀ : ℝ
n : ℕ
hf : ContDiffOn ℝ (↑(n + 1)) f [[x₀, x]]
this✝ : x₀ ≠ x
this : UniqueDiffOn ℝ [[x₀, x]]
k : ℕ
hk : k ≤ n
t : ℝ
ht : t ∈ Ioo (min x₀ x) (max x₀ x)
⊢ k < n + 1

Tactic:
omega

Goal state after:
Module: Mathlib.Analysis.Calculus.Taylor

Goal state before:
pp: F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : ℝ → F
x x₀ : ℝ
n : ℕ
hf : ContDiffOn ℝ (↑(n + 1)) f [[x₀, x]]
this✝ : x₀ ≠ x
this : UniqueDiffOn ℝ [[x₀, x]]
k : ℕ
hk : k ≤ n
⊢ k + 1 ≤ n + 1

Tactic:
omega

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

Goal state before:
pp: E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
u : E
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
h : SameRay ℝ (a • u) (b • u)
hab : 0 ≤ a - b
⊢ ‖a • u - b • u‖ = |‖a • u‖ - ‖b • u‖|

Tactic:
rw [← sub_smul, norm_smul_of_nonneg hab, norm_smul_of_nonneg ha, norm_smul_of_nonneg hb, ←
    sub_mul, abs_of_nonneg (mul_nonneg hab (norm_nonneg _))]

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

Goal state before:
pp: f : ℕ → ℂ
l : ℂ
h : Tendsto (fun n ↦ ∑ i ∈ range n, f i) atTop (𝓝 l)
z : ℂ
hz : ‖z‖ < 1
s : ℕ → ℂ := fun n ↦ ∑ i ∈ range n, f i
k :
  Tendsto (fun n ↦ (1 - z) * ∑ j ∈ range n, (∑ k ∈ range n, f k - ∑ k ∈ range (j + 1), f k) * z ^ j) atTop
    (𝓝 (l - ∑' (i : ℕ), f i * z ^ i))
this :
  Tendsto (fun n ↦ (1 - z) * ∑ i ∈ range n, (l - ∑ k ∈ range (i + 1), f k) * z ^ i) atTop
    (𝓝 (0 + (l - ∑' (i : ℕ), f i * z ^ i)))
⊢ Tendsto (fun n ↦ (1 - z) * ∑ i ∈ range n, (l - ∑ j ∈ range (i + 1), f j) * z ^ i) atTop
    (𝓝 (l - ∑' (n : ℕ), f n * z ^ n))

Tactic:
zero_add

Goal state after:
f : ℕ → ℂ
l : ℂ
h : Tendsto (fun n ↦ ∑ i ∈ range n, f i) atTop (𝓝 l)
z : ℂ
hz : ‖z‖ < 1
s : ℕ → ℂ := fun n ↦ ∑ i ∈ range n, f i
k :
  Tendsto (fun n ↦ (1 - z) * ∑ j ∈ range n, (∑ k ∈ range n, f k - ∑ k ∈ range (j + 1), f k) * z ^ j) atTop
    (𝓝 (l - ∑' (i : ℕ), f i * z ^ i))
this :
  Tendsto (fun n ↦ (1 - z) * ∑ i ∈ range n, (l - ∑ k ∈ range (i + 1), f k) * z ^ i) atTop
    (𝓝 (l - ∑' (i : ℕ), f i * z ^ i))
⊢ Tendsto (fun n ↦ (1 - z) * ∑ i ∈ range n, (l - ∑ j ∈ range (i + 1), f j) * z ^ i) atTop
    (𝓝 (l - ∑' (n : ℕ), f n * z ^ n))
Module: Mathlib.Analysis.Convex.Uniform

Goal state before:
pp: E : Type u_1
inst✝² : SeminormedAddCommGroup E
inst✝¹ : UniformConvexSpace E
ε : ℝ
inst✝ : NormedSpace ℝ E
hε : 0 < ε
hε' : 0 < ε / 3
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε / 3 ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
δ' : ℝ := min (1 / 2) (min (ε / 3) (δ / 3))
x : E
hx : ‖x‖ ≤ 1
y : E
hy : ‖y‖ ≤ 1
hxy : ε ≤ ‖x - y‖
hx' : 1 - δ' < ‖x‖
hy' : 1 - δ' < ‖y‖
hδ' : 0 < 1 - δ'
h₁ : ∀ (z : E), 1 - δ' < ‖z‖ → ‖‖z‖⁻¹ • z‖ = 1
z : E
hz : ‖z‖ ≤ 1
hδz : 1 - δ' ≤ ‖z‖
⊢ ‖‖z‖⁻¹ • z - z‖ ≤ δ'

Tactic:
← one_smul ℝ z

Goal state after:
E : Type u_1
inst✝² : SeminormedAddCommGroup E
inst✝¹ : UniformConvexSpace E
ε : ℝ
inst✝ : NormedSpace ℝ E
hε : 0 < ε
hε' : 0 < ε / 3
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε / 3 ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
δ' : ℝ := min (1 / 2) (min (ε / 3) (δ / 3))
x : E
hx : ‖x‖ ≤ 1
y : E
hy : ‖y‖ ≤ 1
hxy : ε ≤ ‖x - y‖
hx' : 1 - δ' < ‖x‖
hy' : 1 - δ' < ‖y‖
hδ' : 0 < 1 - δ'
h₁ : ∀ (z : E), 1 - δ' < ‖z‖ → ‖‖z‖⁻¹ • z‖ = 1
z : E
hz : ‖z‖ ≤ 1
hδz : 1 - δ' ≤ ‖z‖
⊢ ‖‖z‖⁻¹ • z - 1 • z‖ ≤ δ'
Module: Mathlib.Analysis.Normed.Module.Extr

Goal state before:
pp: α : Type u_1
E : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → E
l : Filter α
c : α
y : E
h : IsMaxFilter (norm ∘ f) l c
hy : SameRay ℝ (f c) y
x : α
hx : (norm ∘ f) x ≤ (norm ∘ f) c
⊢ (fun x ↦ ‖f x + y‖) x ≤ (fun x ↦ ‖f x + y‖) c

Tactic:
by dsimp at hx ⊢; grw [hy.norm_add, norm_add_le, hx]

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

Goal state before:
pp: x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
w : ℝ
hw : deriv f w = 0
hxw : x < w
hwy : w < y
⊢ ∃ a ∈ Ioo x w, (f w - f x) / (w - x) < deriv f a

Tactic:
apply StrictMonoOn.exists_slope_lt_deriv_aux _ hxw _ _
      · exact hf.mono (Icc_subset_Icc le_rfl hwy.le)
      · exact hf'_mono.mono (Ioo_subset_Ioo le_rfl hwy.le)
      · intro z hz
        rw [← hw]
        apply ne_of_lt
        exact hf'_mono ⟨hz.1, hz.2.trans hwy⟩ ⟨hxw, hwy⟩ hz.2

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

Goal state before:
pp: x : ℝ
⊢ -(π / 2) < x → x < π / 2 → ¬∃ k, x = (2 * ↑k + 1) * π / 2

Tactic:
rintro hx_gt hx_lt ⟨r, hxr_eq⟩

Goal state after:
x : ℝ
hx_gt : -(π / 2) < x
hx_lt : x < π / 2
r : ℤ
hxr_eq : x = (2 * ↑r + 1) * π / 2
⊢ False
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

Goal state before:
pp: x : ℝ
h : 0 < x
⊢ arctan x⁻¹ = arctan (tan (π / 2 - arctan x))

pp: case hx₁
x : ℝ
h : 0 < x
⊢ -(π / 2) < π / 2 - arctan x

pp: case hx₂
x : ℝ
h : 0 < x
⊢ π / 2 - arctan x < π / 2

Tactic:
tan_pi_div_two_sub,

Goal state after:
x : ℝ
h : 0 < x
⊢ arctan x⁻¹ = arctan (tan (arctan x))⁻¹

case hx₁
x : ℝ
h : 0 < x
⊢ -(π / 2) < π / 2 - arctan x

case hx₂
x : ℝ
h : 0 < x
⊢ π / 2 - arctan x < π / 2
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds

Goal state before:
pp: x : ℝ
h1 : 0 ≤ x
h2 : x < π / 2
⊢ x ≤ tan x

Tactic:
rcases eq_or_lt_of_le h1 with (rfl | h1')
  · rw [tan_zero]
  · exact le_of_lt (lt_tan h1' h2)

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x : V
hx : x ≠ 0
⊢ arccos (⟪x, x⟫ / (‖x‖ * ‖x‖)) = 0

Tactic:
← real_inner_self_eq_norm_mul_norm,

Goal state after:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x : V
hx : x ≠ 0
⊢ arccos (⟪x, x⟫ / ⟪x, x⟫) = 0
Module: Mathlib.Analysis.Complex.BorelCaratheodory

Goal state before:
pp: f : ℂ → ℂ
M R : ℝ
z : ℂ
hM : 0 < M
hf : DifferentiableOn ℂ f (ball 0 R)
hf₁ : Set.MapsTo f (ball 0 R) {z | z.re ≤ M}
hR : 0 < R
hz : z ∈ ball 0 R
hf₂ : f 0 = 0
⊢ ‖f z‖ ≤ 2 * M * ‖z‖ / (R - ‖z‖)

Tactic:
set w := f z / (2 * M - f z)

Goal state after:
f : ℂ → ℂ
M R : ℝ
z : ℂ
hM : 0 < M
hf : DifferentiableOn ℂ f (ball 0 R)
hf₁ : Set.MapsTo f (ball 0 R) {z | z.re ≤ M}
hR : 0 < R
hz : z ∈ ball 0 R
hf₂ : f 0 = 0
w : ℂ := f z / (2 * ↑M - f z)
⊢ ‖f z‖ ≤ 2 * M * ‖z‖ / (R - ‖z‖)
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
⊢ ‖x + y‖ = ‖x - y‖ ↔ angle x y = π / 2

Tactic:
← sq_eq_sq₀ (norm_nonneg (x + y)) (norm_nonneg (x - y)),

Goal state after:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
⊢ ‖x + y‖ ^ 2 = ‖x - y‖ ^ 2 ↔ angle x y = π / 2
Module: Mathlib.Analysis.Complex.Schwarz

Goal state before:
pp: case ho.refine_2
f : ℂ → ℂ
c z : ℂ
R₂ : ℝ
n : ℕ
hn : (fun x ↦ f x - f c) =o[𝓝 c] fun w ↦ (w - c) ^ n
R₁ : ℝ
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hd : DifferentiableOn ℂ f (closedBall c R₁)
h_maps : MapsTo f (closedBall c R₁) (closedBall (f c) R₂)
hne : z ≠ c
g : ℂ → ℂ := fun w ↦ ((w - c) ^ (n + 1))⁻¹ * (f w - f c)
g' : ℂ → ℂ := update g c ((𝓝[≠] c).limUnder g)
w : ℂ
hw : w - c ≠ 0
⊢ (fun x ↦ ((x - c) ^ (n + 1))⁻¹ * (x - c) ^ n) w = (fun z ↦ (z - c)⁻¹) w

Tactic:
simp [pow_succ, field]

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

Goal state before:
pp: case inr
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : ProperSpace 𝕜
n : ℕ
hn : ↑(-↑n) ≠ 0
surj : Function.Surjective fun x ↦ x ^ (-↑n)
⊢ IsQuotientCoveringMap (fun x ↦ x ^ (-↑n)) ↥(zpowGroupHom (-↑n)).ker

Tactic:
show (zpowGroupHom (α := 𝕜ˣ) (-n)).ker = (powMonoidHom n).ker by ext; simp

Goal state after:
case inr
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : ProperSpace 𝕜
n : ℕ
hn : ↑(-↑n) ≠ 0
surj : Function.Surjective fun x ↦ x ^ (-↑n)
⊢ IsQuotientCoveringMap (fun x ↦ x ^ (-↑n)) ↥(powMonoidHom n).ker
Module: Mathlib.Analysis.Complex.Schwarz

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
R₁ R₂ : ℝ
f : E → F
c z : E
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
hz : z ∈ ball c R₁
⊢ dist (f z) (f c) ≤ R₂ / R₁ * dist z c

Tactic:
refine dist_le_mul_div_pow_of_mapsTo_ball_of_isLittleO (n := 0) hd h_maps ?_ hz |>.trans_eq ?_
  · simpa using hd.continuousOn.continuousAt
      (ball_mem_nhds _ <| nonempty_ball.mp ⟨_, hz⟩) |>.sub_const (f c)
  · simp [field]

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

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
R₁ R₂ : ℝ
f : ℂ → E
c z₀ : ℂ
inst✝ : StrictConvexSpace ℝ E
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
h_z₀ : z₀ ∈ ball c R₁
h_eq : ‖dslope f c z₀‖ = R₂ / R₁
e : E →L[ℂ] UniformSpace.Completion E := UniformSpace.Completion.toComplL
g : ℂ → UniformSpace.Completion E := dslope (⇑e ∘ f) c
z : ℂ
hz : z ∈ ball c R₁
h_R₁ : 0 < R₁
hg' : g = ⇑e ∘ dslope f c
g_le_div : ∀ z ∈ ball c R₁, ‖g z‖ ≤ R₂ / R₁
g_max : IsMaxOn (norm ∘ g) (ball c R₁) z₀
g_diff : DifferentiableOn ℂ g (ball c R₁)
heq : ‖dslope f c z‖ = ‖dslope f c z₀‖
⊢ ‖dslope f c z + dslope f c z₀‖ = ‖dslope f c z₀ + dslope f c z₀‖

Tactic:
simpa [hg', e, ← UniformSpace.Completion.coe_add]
      using norm_eqOn_of_isPreconnected_of_isMaxOn (convex_ball c R₁).isPreconnected
        isOpen_ball (g_diff.add_const (g z₀)) h_z₀ g_max.norm_add_self hz

Goal state after:
Module: Mathlib.Analysis.Meromorphic.NormalForm

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
g : 𝕜 → 𝕜
x : 𝕜
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
n : ℤ
g_f : 𝕜 → E
h₁g_f : AnalyticAt 𝕜 g_f x
h₂g_f : g_f x ≠ 0
h₃g_f : f =ᶠ[𝓝 x] (fun x_1 ↦ x_1 - x) ^ n • g_f
y : 𝕜
hy : f y = ((fun x_1 ↦ x_1 - x) ^ n • g_f) y
⊢ g y • (y - x) ^ n • g_f y = (y - x) ^ n • g y • g_f y

Tactic:
smul_comm

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
g : 𝕜 → 𝕜
x : 𝕜
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
n : ℤ
g_f : 𝕜 → E
h₁g_f : AnalyticAt 𝕜 g_f x
h₂g_f : g_f x ≠ 0
h₃g_f : f =ᶠ[𝓝 x] (fun x_1 ↦ x_1 - x) ^ n • g_f
y : 𝕜
hy : f y = ((fun x_1 ↦ x_1 - x) ^ n • g_f) y
⊢ (y - x) ^ n • g y • g_f y = (y - x) ^ n • g y • g_f y
Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
h₁ : AnalyticAt 𝕜 f x
h₂ : f x ≠ 0
⊢ meromorphicTrailingCoeffAt f x = f x

Tactic:
rw [h₁.meromorphicTrailingCoeffAt_of_ne_zero_of_eq_nhdsNE (n := 0) h₂]
  filter_upwards
  simp

Goal state after:
Module: Mathlib.Analysis.Meromorphic.NormalForm

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x z : 𝕜
hz : z = x
h₀f : MeromorphicNFAt f x
n : ℤ
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : f =ᶠ[𝓝 x] (fun x_1 ↦ x_1 - x) ^ n • g
this✝ : meromorphicOrderAt f x = ↑n
h₃f : meromorphicOrderAt f x = 0
hn : n = 0
this : g =ᶠ[𝓝 x] Classical.choose ⋯
⊢ Function.update f x (Classical.choose ⋯ x) x = g x

Tactic:
simp only [Function.update_self]

Goal state after:
case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x z : 𝕜
hz : z = x
h₀f : MeromorphicNFAt f x
n : ℤ
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : f =ᶠ[𝓝 x] (fun x_1 ↦ x_1 - x) ^ n • g
this✝ : meromorphicOrderAt f x = ↑n
h₃f : meromorphicOrderAt f x = 0
hn : n = 0
this : g =ᶠ[𝓝 x] Classical.choose ⋯
⊢ Classical.choose ⋯ x = g x
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
hf : MeromorphicOn f U
h'f : ∀ x ∈ U, meromorphicOrderAt f x ≠ ⊤
⊢ ∀ᶠ (x : 𝕜) in codiscreteWithin U, f x ≠ 0

Tactic:
simp_rw [eventually_iff, mem_codiscreteWithin, disjoint_principal_right]

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
hf : MeromorphicOn f U
h'f : ∀ x ∈ U, meromorphicOrderAt f x ≠ ⊤
⊢ ∀ x ∈ U, (U \ {x | f x ≠ 0})ᶜ ∈ 𝓝[≠] x
Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f₁ f₂ : 𝕜 → E
hf₁ : MeromorphicAt f₁ x
hf₂ : MeromorphicAt f₂ x
h₁ : meromorphicOrderAt f₁ x = meromorphicOrderAt f₂ x
h₂ : meromorphicTrailingCoeffAt f₁ x + meromorphicTrailingCoeffAt f₂ x ≠ 0
h₁f₁ : meromorphicOrderAt f₁ x = ⊤
⊢ meromorphicTrailingCoeffAt (f₁ + f₂) x = 0 + meromorphicTrailingCoeffAt f₂ x

Tactic:
zero_add

Goal state after:
case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f₁ f₂ : 𝕜 → E
hf₁ : MeromorphicAt f₁ x
hf₂ : MeromorphicAt f₂ x
h₁ : meromorphicOrderAt f₁ x = meromorphicOrderAt f₂ x
h₂ : meromorphicTrailingCoeffAt f₁ x + meromorphicTrailingCoeffAt f₂ x ≠ 0
h₁f₁ : meromorphicOrderAt f₁ x = ⊤
⊢ meromorphicTrailingCoeffAt (f₁ + f₂) x = meromorphicTrailingCoeffAt f₂ x
Module: Mathlib.Analysis.Meromorphic.NormalForm

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
x : 𝕜
hx : x ∈ Uᶜ
⊢ toMeromorphicNFOn f U x = f x

Tactic:
simp_all [toMeromorphicNFOn]

Goal state after: