mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff

Goal state before:
pp: E : Type u_1
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : FiniteDimensional ℝ E
F : Type u_2
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
inst✝⁴ : IsManifold I ∞ M
inst✝³ : MeasurableSpace M
inst✝² : BorelSpace M
inst✝¹ : T2Space M
f : M → F
μ : Measure M
inst✝ : SigmaCompactSpace M
hf : LocallyIntegrable f μ
h : ∀ (g : M → ℝ), ContMDiff I 𝓘(ℝ, ℝ) ∞ g → HasCompactSupport g → ∫ (x : M), g x • f x ∂μ = 0
this✝² : LocallyCompactSpace H
this✝¹ : LocallyCompactSpace M
this✝ : SecondCountableTopology H
this : SecondCountableTopology M
x✝¹ : MetricSpace M := metrizableSpaceMetric M
s : Set M
hs : IsCompact s
δ : ℝ
δpos : 0 < δ
hδ : IsCompact (cthickening δ s)
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), u n ∈ Ioo 0 δ
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → Set M := fun n ↦ thickening (u n) s
K : Set M
K_compact : IsCompact K
vK : ∀ (n : ℕ), v n ⊆ K
g : ℕ → M → ℝ
g_supp : ∀ (n : ℕ), support (g n) = v n
g_diff : ∀ (n : ℕ), ContMDiff I 𝓘(ℝ, ℝ) ∞ (g n)
g_range : ∀ (n : ℕ), range (g n) ⊆ Icc 0 1
hg : ∀ (n : ℕ), ∀ x ∈ s, g n x = 1
bound : M → ℝ := K.indicator fun x ↦ ‖f x‖
A : ∀ (n : ℕ), AEStronglyMeasurable (fun x ↦ g n x • f x) μ
B : Integrable bound μ
n : ℕ
x : M
x✝ : x ∈ K
⊢ ‖g n x‖ ≤ 1

Tactic:
have := g_range n (mem_range_self (f := g n) x)

Goal state after:
E : Type u_1
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : FiniteDimensional ℝ E
F : Type u_2
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
inst✝⁴ : IsManifold I ∞ M
inst✝³ : MeasurableSpace M
inst✝² : BorelSpace M
inst✝¹ : T2Space M
f : M → F
μ : Measure M
inst✝ : SigmaCompactSpace M
hf : LocallyIntegrable f μ
h : ∀ (g : M → ℝ), ContMDiff I 𝓘(ℝ, ℝ) ∞ g → HasCompactSupport g → ∫ (x : M), g x • f x ∂μ = 0
this✝³ : LocallyCompactSpace H
this✝² : LocallyCompactSpace M
this✝¹ : SecondCountableTopology H
this✝ : SecondCountableTopology M
x✝¹ : MetricSpace M := metrizableSpaceMetric M
s : Set M
hs : IsCompact s
δ : ℝ
δpos : 0 < δ
hδ : IsCompact (cthickening δ s)
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), u n ∈ Ioo 0 δ
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → Set M := fun n ↦ thickening (u n) s
K : Set M
K_compact : IsCompact K
vK : ∀ (n : ℕ), v n ⊆ K
g : ℕ → M → ℝ
g_supp : ∀ (n : ℕ), support (g n) = v n
g_diff : ∀ (n : ℕ), ContMDiff I 𝓘(ℝ, ℝ) ∞ (g n)
g_range : ∀ (n : ℕ), range (g n) ⊆ Icc 0 1
hg : ∀ (n : ℕ), ∀ x ∈ s, g n x = 1
bound : M → ℝ := K.indicator fun x ↦ ‖f x‖
A : ∀ (n : ℕ), AEStronglyMeasurable (fun x ↦ g n x • f x) μ
B : Integrable bound μ
n : ℕ
x : M
x✝ : x ∈ K
this : g n x ∈ Icc 0 1
⊢ ‖g n x‖ ≤ 1
Module: Mathlib.Geometry.Manifold.PartitionOfUnity

Goal state before:
pp: E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
H : Type uH
inst✝¹ : TopologicalSpace H
I : ModelWithCorners ℝ E H
inst✝ : FiniteDimensional ℝ E
n : ℕ∞
s : Set H
hs : IsOpen[inst✝¹] s
⊢ ∃ f, support f = s ∧ ContMDiff I 𝓘(ℝ, ℝ) (↑n) f ∧ range f ⊆ Icc 0 1

Tactic:
by
  have h's : IsOpen (I.symm ⁻¹' s) := I.continuous_symm.isOpen_preimage _ hs
  rcases h's.exists_contDiff_support_eq with ⟨f, f_supp, f_diff, f_range⟩
  refine ⟨f ∘ I, ?_, ?_, ?_⟩
  · rw [support_comp_eq_preimage, f_supp, ← preimage_comp]
    simp only [ModelWithCorners.symm_comp_self, preimage_id_eq, id_eq]
  · exact f_diff.comp_contMDiff I.contMDiff
  · exact Subset.trans (range_comp_subset_range _ _) f_range

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

Goal state before:
pp: case refine_2
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : α → E
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn f s μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∫ (x : α) in s, f x ∂μ = 0
hf : AEFinStronglyMeasurable f μ
t : Set α := hf.sigmaFiniteSet
this : SigmaFinite (μ.restrict t)
⊢ ∀ (s : Set α), MeasurableSet s → (μ.restrict t) s < ∞ → ∫ (x : α) in s, f x ∂μ.restrict t = 0

Tactic:
· intro s hs hμs
    rw [Measure.restrict_restrict hs]
    rw [Measure.restrict_apply hs] at hμs
    exact hf_zero _ (hs.inter hf.measurableSet) hμs

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 β
μ : Measure β
f : β → E
hf : Integrable f μ
h'f : ∀ (s : Set β), IsClosed[inst✝²] s → ∫ (x : β) in s, f x ∂μ = 0
t : Set β
t_meas : MeasurableSet t
ht : ∫ (x : β) in t, f x ∂μ = 0
I : ∫ (x : β), f x ∂μ = 0
⊢ ∫ (x : β) in tᶜ, f x ∂μ = 0

Tactic:
simpa [ht, I] using integral_add_compl t_meas hf

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

Goal state before:
pp: X : Type u_1
inst✝ : PseudoMetricSpace X
f : ℝ → X
d b y : ℝ
hdb : d ≤ b
hf : AbsolutelyContinuousOnInterval f d b
u : Set (ℝ × ℝ)
hu₁ : ∀ z ∈ u, d < z.1 ∧ z.1 < z.2 ∧ z.2 < b
hu₂ : u.PairwiseDisjoint fun z ↦ Icc z.1 z.2
hu₃ : HasSum (fun z ↦ (↑z).2 - (↑z).1) (b - d)
hu₄ : HasSum (fun z ↦ dist (f (↑z).1) (f (↑z).2)) y
⊢ dist (f d) (f b) ≤ y

Tactic:
let u_coe (s : Finset u) : Finset (ℝ × ℝ) := s.image Subtype.val

Goal state after:
X : Type u_1
inst✝ : PseudoMetricSpace X
f : ℝ → X
d b y : ℝ
hdb : d ≤ b
hf : AbsolutelyContinuousOnInterval f d b
u : Set (ℝ × ℝ)
hu₁ : ∀ z ∈ u, d < z.1 ∧ z.1 < z.2 ∧ z.2 < b
hu₂ : u.PairwiseDisjoint fun z ↦ Icc z.1 z.2
hu₃ : HasSum (fun z ↦ (↑z).2 - (↑z).1) (b - d)
hu₄ : HasSum (fun z ↦ dist (f (↑z).1) (f (↑z).2)) y
u_coe : Finset ↑u → Finset (ℝ × ℝ) := fun s ↦ Finset.image Subtype.val s
⊢ dist (f d) (f b) ≤ y
Module: Mathlib.Analysis.Calculus.Taylor

Goal state before:
pp: f g g' : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n) f [[x₀, x]]
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f [[x₀, x]]) (uIoo x₀ x)
gcont : ContinuousOn g [[x₀, x]]
gdiff : ∀ x_1 ∈ uIoo x₀ x, HasDerivAt g (g' x_1) x_1
g'_ne : ∀ x_1 ∈ uIoo x₀ x, g' x_1 ≠ 0
hx₁ : min x₀ x < max x₀ x
y : ℝ
hy : y ∈ Ioo (min x₀ x) (max x₀ x)
h :
  (g (max x₀ x) - g (min x₀ x)) * ((↑n !)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f [[x₀, x]] y =
    (taylorWithinEval f n [[x₀, x]] (max x₀ x) x - taylorWithinEval f n [[x₀, x]] (min x₀ x) x) * g' y
⊢ ∃ x' ∈ uIoo x₀ x,
    f x - taylorWithinEval f n [[x₀, x]] x₀ x =
      ((x - x') ^ n / ↑n ! * (g x - g x₀) / g' x') • iteratedDerivWithin (n + 1) f [[x₀, x]] x'

Tactic:
use y, hy

Goal state after:
case right
f g g' : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n) f [[x₀, x]]
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f [[x₀, x]]) (uIoo x₀ x)
gcont : ContinuousOn g [[x₀, x]]
gdiff : ∀ x_1 ∈ uIoo x₀ x, HasDerivAt g (g' x_1) x_1
g'_ne : ∀ x_1 ∈ uIoo x₀ x, g' x_1 ≠ 0
hx₁ : min x₀ x < max x₀ x
y : ℝ
hy : y ∈ Ioo (min x₀ x) (max x₀ x)
h :
  (g (max x₀ x) - g (min x₀ x)) * ((↑n !)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f [[x₀, x]] y =
    (taylorWithinEval f n [[x₀, x]] (max x₀ x) x - taylorWithinEval f n [[x₀, x]] (min x₀ x) x) * g' y
⊢ f x - taylorWithinEval f n [[x₀, x]] x₀ x =
    ((x - y) ^ n / ↑n ! * (g x - g x₀) / g' y) • iteratedDerivWithin (n + 1) f [[x₀, x]] y
Module: Mathlib.Analysis.Calculus.Taylor

Goal state before:
pp: f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n) f [[x₀, x]]
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f [[x₀, x]]) (uIoo x₀ x)
gcont : ContinuousOn (fun t ↦ (x - t) ^ (n + 1)) [[x₀, x]]
xy_ne : ∀ y ∈ uIoo x₀ x, (x - y) ^ n ≠ 0
hg' : ∀ y ∈ uIoo x₀ x, -(↑n + 1) * (x - y) ^ n ≠ 0
y : ℝ
hy : y ∈ uIoo x₀ x
h :
  f x - taylorWithinEval f n [[x₀, x]] x₀ x =
    ((x - y) ^ n / ↑n ! * ((x - x) ^ (n + 1) - (x - x₀) ^ (n + 1)) / (-(↑n + 1) * (x - y) ^ n)) •
      iteratedDerivWithin (n + 1) f [[x₀, x]] y
⊢ ∃ x' ∈ uIoo x₀ x,
    f x - taylorWithinEval f n [[x₀, x]] x₀ x =
      iteratedDerivWithin (n + 1) f [[x₀, x]] x' * (x - x₀) ^ (n + 1) / ↑(n + 1)!

Tactic:
use y, hy

Goal state after:
case right
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n) f [[x₀, x]]
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f [[x₀, x]]) (uIoo x₀ x)
gcont : ContinuousOn (fun t ↦ (x - t) ^ (n + 1)) [[x₀, x]]
xy_ne : ∀ y ∈ uIoo x₀ x, (x - y) ^ n ≠ 0
hg' : ∀ y ∈ uIoo x₀ x, -(↑n + 1) * (x - y) ^ n ≠ 0
y : ℝ
hy : y ∈ uIoo x₀ x
h :
  f x - taylorWithinEval f n [[x₀, x]] x₀ x =
    ((x - y) ^ n / ↑n ! * ((x - x) ^ (n + 1) - (x - x₀) ^ (n + 1)) / (-(↑n + 1) * (x - y) ^ n)) •
      iteratedDerivWithin (n + 1) f [[x₀, x]] y
⊢ f x - taylorWithinEval f n [[x₀, x]] x₀ x = iteratedDerivWithin (n + 1) f [[x₀, x]] y * (x - x₀) ^ (n + 1) / ↑(n + 1)!
Module: Mathlib.Analysis.Calculus.Taylor

Goal state before:
pp: f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n + 1) f [[x₀, x]]
⊢ ∃ x' ∈ uIoo x₀ x,
    f x - taylorWithinEval f n [[x₀, x]] x₀ x = iteratedDeriv (n + 1) f x' * (x - x₀) ^ (n + 1) / ↑(n + 1)!

Tactic:
have hu : UniqueDiffOn ℝ (uIcc x₀ x) := uniqueDiffOn_uIcc hx
  have hd : DifferentiableOn ℝ (iteratedDerivWithin n f (uIcc x₀ x)) (uIcc x₀ x) := by
    refine hf.differentiableOn_iteratedDerivWithin ?_ hu
    norm_cast
    simp
  obtain ⟨x', h1, h2⟩ := taylor_mean_remainder_lagrange hx hf.of_succ (hd.mono Ioo_subset_Icc_self)
  use x', h1
  rw [h2, iteratedDeriv_eq_iteratedFDeriv, iteratedDerivWithin_eq_iteratedFDerivWithin,
    iteratedFDerivWithin_eq_iteratedFDeriv hu _ ⟨le_of_lt h1.1, le_of_lt h1.2⟩]
  exact hf.contDiffAt (Icc_mem_nhds_iff.2 h1)

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

Goal state before:
pp: f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n) f [[x₀, x]]
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f [[x₀, x]]) (uIoo x₀ x)
gcont : ContinuousOn id [[x₀, x]]
gdiff : ∀ x_1 ∈ uIoo x₀ x, HasDerivAt id ((fun x ↦ 1) x_1) x_1
y : ℝ
hy : y ∈ uIoo x₀ x
h :
  f x - taylorWithinEval f n [[x₀, x]] x₀ x =
    ((x - y) ^ n / ↑n ! * (id x - id x₀) / 1) • iteratedDerivWithin (n + 1) f [[x₀, x]] y
⊢ ∃ x' ∈ uIoo x₀ x,
    f x - taylorWithinEval f n [[x₀, x]] x₀ x =
      iteratedDerivWithin (n + 1) f [[x₀, x]] x' * (x - x') ^ n / ↑n ! * (x - x₀)

Tactic:
use y, hy

Goal state after:
case right
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n) f [[x₀, x]]
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f [[x₀, x]]) (uIoo x₀ x)
gcont : ContinuousOn id [[x₀, x]]
gdiff : ∀ x_1 ∈ uIoo x₀ x, HasDerivAt id ((fun x ↦ 1) x_1) x_1
y : ℝ
hy : y ∈ uIoo x₀ x
h :
  f x - taylorWithinEval f n [[x₀, x]] x₀ x =
    ((x - y) ^ n / ↑n ! * (id x - id x₀) / 1) • iteratedDerivWithin (n + 1) f [[x₀, x]] y
⊢ f x - taylorWithinEval f n [[x₀, x]] x₀ x = iteratedDerivWithin (n + 1) f [[x₀, x]] y * (x - y) ^ n / ↑n ! * (x - x₀)
Module: Mathlib.Analysis.Calculus.Taylor

Goal state before:
pp: E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a : ℝ
n : ℕ
hab : a ≤ a
hf : ContDiffOn ℝ (↑n + 1) f (Icc a a)
x : ℝ
hx : x ∈ Icc a a
⊢ x = a

Tactic:
simpa [← le_antisymm_iff] using hx

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

Goal state before:
pp: case h
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
n : ℕ
hab : a ≤ b
hf : ContDiffOn ℝ (↑n + 1) f (Icc a b)
h : a < b
g : ℝ → ℝ := fun y ↦ ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖
x : ℝ
hx : x ∈ Icc a b
y : ℝ
⊢ y ∈ Icc a b → ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ sSup (g '' Icc a b)

Tactic:
exact (hf.continuousOn_iteratedDerivWithin rfl.le <| uniqueDiffOn_Icc h).norm.le_sSup_image_Icc

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

Goal state before:
pp: M : ℝ
hM : M ≤ 1
z : ℂ
⊢ z ∈ {z | ‖z‖ < 1 ∧ ‖1 - z‖ < M * (1 - ‖z‖)} ↔ z ∈ ∅

Tactic:
Set.mem_ofPred,

Goal state after:
M : ℝ
hM : M ≤ 1
z : ℂ
⊢ ‖z‖ < 1 ∧ ‖1 - z‖ < M * (1 - ‖z‖) ↔ z ∈ ∅
Module: Mathlib.Analysis.Normed.Module.Ray

Goal state before:
pp: E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x y : E
h : SameRay ℝ x y
⊢ ‖x + y‖ = ‖x‖ + ‖y‖

Tactic:
rcases h.exists_eq_smul with ⟨u, a, b, ha, hb, -, rfl, rfl⟩
  rw [← add_smul, norm_smul_of_nonneg (add_nonneg ha hb), norm_smul_of_nonneg ha,
    norm_smul_of_nonneg hb, add_mul]

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

Goal state before:
pp: E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
h : ∀ (x y : E), ‖x‖ = 1 → ‖y‖ = 1 → ‖x + y‖ = 2 → SameRay ℝ x y
x : E
hx : ‖x‖ = 1
y : E
hy : ‖y‖ = 1
h₂ : ‖x + y‖ = 2
⊢ x = y

Tactic:
exact (sameRay_iff_of_norm_eq (hx.trans hy.symm)).1 (h x y hx hy h₂)

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

Goal state before:
pp: E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : StrictConvexSpace ℝ E
x y : E
h : ¬SameRay ℝ x y
⊢ ‖x + y‖ < ‖x‖ + ‖y‖

Tactic:
simp only [sameRay_iff_inv_norm_smul_eq, not_or, ← Ne.eq_def] at h
  rcases h with ⟨hx, hy, hne⟩
  rw [← norm_pos_iff] at hx hy
  have hxy : 0 < ‖x‖ + ‖y‖ := add_pos hx hy
  have :=
    combo_mem_ball_of_ne (inv_norm_smul_mem_unitClosedBall x)
      (inv_norm_smul_mem_unitClosedBall y) hne (div_pos hx hxy) (div_pos hy hxy)
      (by rw [← add_div, div_self hxy.ne'])
  rwa [mem_ball_zero_iff, div_eq_inv_mul, div_eq_inv_mul, mul_smul, mul_smul, smul_inv_smul₀ hx.ne',
    smul_inv_smul₀ hy.ne', ← smul_add, norm_smul, Real.norm_of_nonneg (inv_pos.2 hxy).le, ←
    div_eq_inv_mul, div_lt_one hxy] at this

Goal state after:
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‖
⊢ 1 - ‖z‖ ≤ δ'

Tactic:
sub_le_comm

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‖
⊢ 1 - δ' ≤ ‖z‖
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)
h : ∀ w ∈ Ioo x y, deriv f w ≠ 0
A : DifferentiableOn ℝ f (Ioo x y)
a : ℝ
ha : deriv f a = (f y - f x) / (y - x)
hxa : x < a
hay : a < y
⊢ ∃ a ∈ Ioo x y, (f y - f x) / (y - x) < deriv f a

Tactic:
rcases nonempty_Ioo.2 hay with ⟨b, ⟨hab, hby⟩⟩

Goal state after:
x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
h : ∀ w ∈ Ioo x y, deriv f w ≠ 0
A : DifferentiableOn ℝ f (Ioo x y)
a : ℝ
ha : deriv f a = (f y - f x) / (y - x)
hxa : x < a
hay : a < y
b : ℝ
hab : a < b
hby : b < y
⊢ ∃ a ∈ Ioo x y, (f y - f x) / (y - x) < deriv f a
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

Goal state before:
pp: x : ℂ
h : cos x = 0
⊢ tan x = 0

Tactic:
obtain ⟨k, hxk⟩ := cos_eq_zero_iff.mp h

Goal state after:
x : ℂ
h : cos x = 0
k : ℤ
hxk : x = (2 * ↑k + 1) * ↑π / 2
⊢ tan x = 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

Goal state before:
pp: this : ContinuousOn (fun x ↦ sin x / cos x) {x | cos x ≠ 0}
⊢ (fun x ↦ sin x / cos x) = tan

Tactic:
ext1 x

Goal state after:
this : ContinuousOn (fun x ↦ sin x / cos x) {x | cos x ≠ 0}
x : ℝ
⊢ sin x / cos x = tan x
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

Goal state before:
pp: ⊢ arctan (√3)⁻¹ = π / 6

Tactic:
rw [inv_eq_one_div, ← tan_pi_div_six, arctan_tan]
  all_goals
  · field_simp
    norm_num

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

Goal state before:
pp: x : ℝ
h : 0 ≤ x
⊢ x / √(1 + x ^ 2) = √(1 - (√(1 + x ^ 2))⁻¹ ^ 2)

Tactic:
rw_mod_cast [← sqrt_inv, sq_sqrt, ← one_div, one_sub_div, add_sub_cancel_left, sqrt_div,
    sqrt_sq h]

Goal state after:
case hx
x : ℝ
h : 0 ≤ x
⊢ 0 ≤ x ^ 2

x : ℝ
h : 0 ≤ x
⊢ 1 + x ^ 2 ≠ 0

x : ℝ
h : 0 ≤ x
⊢ 0 ≤ (1 + x ^ 2)⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds

Goal state before:
pp: case e'_3
x : ℝ
hx1 : -(3 * π / 2) ≤ x
hx2 : x ≤ 3 * π / 2
hx3 : x ≠ 0
this : ∀ {y : ℝ}, 0 < y → y ≤ 3 * π / 2 → cos y < 1 / √(y ^ 2 + 1)
h✝ : x < 0
⊢ cos x = cos (-x)

Tactic:
cos_neg

Goal state after:
case e'_3
x : ℝ
hx1 : -(3 * π / 2) ≤ x
hx2 : x ≤ 3 * π / 2
hx3 : x ≠ 0
this : ∀ {y : ℝ}, 0 < y → y ≤ 3 * π / 2 → cos y < 1 / √(y ^ 2 + 1)
h✝ : x < 0
⊢ cos x = cos x
Module: Mathlib.Analysis.Complex.BorelCaratheodory

Goal state before:
pp: case hdb
M : ℝ
w : ℂ
hM : 0 < M
hw : ‖w‖ < 1
⊢ ‖1‖ - ‖w‖ ≤ ‖1 + w‖

Tactic:
exact norm_sub_le_norm_add 1 w

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

Goal state before:
pp: S : Set ℝ
f : ℝ → ℝ
hfc : StrictConvexOn ℝ S f
hfd : DifferentiableOn ℝ f S
⊢ StrictMonoOn (derivWithin f S) S

Tactic:
by
  intro x hx y hy hxy
  exact (hfc.derivWithin_lt_slope hx hy hxy (hfd x hx)).trans
    (hfc.slope_lt_derivWithin hx hy hxy (hfd y hy))

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

Goal state before:
pp: z : 𝔻
n : ℕ+
⊢ z ^ n = 0 ↔ z = 0

Tactic:
← coe_inj,

Goal state after:
z : 𝔻
n : ℕ+
⊢ ↑(z ^ n) = ↑0 ↔ z = 0
Module: Mathlib.Analysis.Meromorphic.IsolatedZeros

Goal state before:
pp: case h
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f g : 𝕜 → E
hf : MeromorphicOn f U
hg : MeromorphicOn g U
hU : Preperfect U
h : f =ᶠ[codiscreteWithin U] g
⊢ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {x | f =ᶠ[𝓝[≠] x] g} ∧
    U ⊆ {x | f =ᶠ[𝓝[≠] x] g} ∧ ∀ x ∈ {x | f =ᶠ[𝓝[≠] x] g}, f =ᶠ[𝓝[≠] x] g

Tactic:
simp only [Set.mem_ofPred_eq, imp_self, implies_true, and_true]

Goal state after:
case h
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f g : 𝕜 → E
hf : MeromorphicOn f U
hg : MeromorphicOn g U
hU : Preperfect U
h : f =ᶠ[codiscreteWithin U] g
⊢ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {x | f =ᶠ[𝓝[≠] x] g} ∧ U ⊆ {x | f =ᶠ[𝓝[≠] x] g}
Module: Mathlib.Analysis.Meromorphic.Divisor

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
U : Set 𝕜
n : ℕ
⊢ divisor (OfNat.ofNat n) U = 0

Tactic:
by
  convert! divisor_const (n : 𝕜)
  simp [Semiring.toGrindSemiring_ofNat 𝕜 n]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
U : Set 𝕜
hf₁ : MeromorphicOn f₁ U
hf₂ : MeromorphicOn f₂ U
⊢ (divisor f₁ U)⁻ ⊔ (divisor f₂ U)⁻ ≤ (divisor f₁ U)⁻ + (divisor f₂ U)⁻

Tactic:
by_cases h : (divisor f₁ U)⁻ ≤ (divisor f₂ U)⁻

Goal state after:
case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
U : Set 𝕜
hf₁ : MeromorphicOn f₁ U
hf₂ : MeromorphicOn f₂ U
h : (divisor f₁ U)⁻ ≤ (divisor f₂ U)⁻
⊢ (divisor f₁ U)⁻ ⊔ (divisor f₂ U)⁻ ≤ (divisor f₁ U)⁻ + (divisor f₂ U)⁻

case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
U : Set 𝕜
hf₁ : MeromorphicOn f₁ U
hf₂ : MeromorphicOn f₂ U
h : ¬(divisor f₁ U)⁻ ≤ (divisor f₂ U)⁻
⊢ (divisor f₁ U)⁻ ⊔ (divisor f₂ U)⁻ ≤ (divisor f₁ U)⁻ + (divisor f₂ U)⁻
Module: Mathlib.Analysis.Meromorphic.Divisor

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ : 𝕜 → 𝕜
f₂ : 𝕜 → E
h₁f₁ : MeromorphicOn f₁ U
h₁f₂ : MeromorphicOn f₂ U
h₂f₁ : ∀ z ∈ U, meromorphicOrderAt f₁ z ≠ ⊤
h₂f₂ : ∀ z ∈ U, meromorphicOrderAt f₂ z ≠ ⊤
⊢ divisor (f₁ • f₂) U = divisor f₁ U + divisor f₂ U

Tactic:
by
  ext z
  by_cases hz : z ∈ U
  · lift meromorphicOrderAt f₁ z to ℤ using (h₂f₁ z hz) with a₁ ha₁
    lift meromorphicOrderAt f₂ z to ℤ using (h₂f₂ z hz) with a₂ ha₂
    simp [h₁f₁, h₁f₂, h₁f₁.smul h₁f₂, hz, meromorphicOrderAt_smul (h₁f₁ z hz) (h₁f₂ z hz),
      ← ha₁, ← ha₂, ← WithTop.coe_add]
  · simp [hz]

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

Goal state before:
pp: case mpr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
⊢ AnalyticAt 𝕜 f x ∨ MeromorphicAt f x ∧ meromorphicOrderAt f x < 0 ∧ f x = 0 → MeromorphicNFAt f x

Tactic:
· rintro (h | ⟨h₁, h₂, h₃⟩)
    · by_cases h₂f : analyticOrderAt f x = ⊤
      · rw [analyticOrderAt_eq_top] at h₂f
        tauto
      · right
        use analyticOrderNatAt f x
        have : analyticOrderAt f x ≠ ⊤ := h₂f
        rw [← ENat.natCast_toNat_eq_self, eq_comm, h.analyticOrderAt_eq_natCast] at this
        obtain ⟨g, h₁g, h₂g, h₃g⟩ := this
        use g, h₁g, h₂g
        simpa
    · right
      lift meromorphicOrderAt f x to ℤ using LT.lt.ne_top h₂ with n hn
      obtain ⟨g, h₁g, h₂g, h₃g⟩ := (meromorphicOrderAt_eq_int_iff h₁).1 hn.symm
      use n, g, h₁g, h₂g
      filter_upwards [eventually_nhdsWithin_iff.1 h₃g]
      intro z hz
      by_cases h₁z : z = x
      · simp only [h₁z, Pi.smul_apply', Pi.pow_apply, sub_self]
        rw [h₃]
        apply (smul_eq_zero_of_left (zero_zpow n _) (g x)).symm
        by_contra hCon
        simp [hCon] at h₂
      · exact hz h₁z

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

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
ι : Type u_3
f : ι → 𝕜 → 𝕜
h₁f : ∀ (i : ι), MeromorphicNFAt (f i) x
h₂f : {σ | f σ x = 0}.Subsingleton
h₃f : Function.HasFiniteMulSupport f
⊢ MeromorphicNFAt (∏ᶠ (i : ι), f i) x

Tactic:
finprod_eq_prod f h₃f

Goal state after:
case pos
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
ι : Type u_3
f : ι → 𝕜 → 𝕜
h₁f : ∀ (i : ι), MeromorphicNFAt (f i) x
h₂f : {σ | f σ x = 0}.Subsingleton
h₃f : Function.HasFiniteMulSupport f
⊢ MeromorphicNFAt (∏ i ∈ Finite.toFinset h₃f, f i) x
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicAt f x
h : ¬analyticOrderAt (fun z ↦ (z - x) ^ Exists.choose hf • f z) x = ⊤
m : ℕ
hm : ↑m = analyticOrderAt (fun z ↦ (z - x) ^ Exists.choose hf • f z) x
⊢ ¬∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = 0

Tactic:
contrapose h

Goal state after:
case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicAt f x
m : ℕ
hm : ↑m = analyticOrderAt (fun z ↦ (z - x) ^ Exists.choose hf • f z) x
h : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = 0
⊢ analyticOrderAt (fun z ↦ (z - x) ^ Exists.choose hf • f z) x = ⊤
Module: Mathlib.Analysis.Complex.CanonicalDecomposition

Goal state before:
pp: R : ℝ
w : ℂ
⊢ canonicalFactor R w w = 0

Tactic:
by
  simp [canonicalFactor_apply]

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

Goal state before:
pp: case neg
R : ℝ
F : locallyFinsuppWithin (ball 0 R) ℤ
w : ℂ
hw : w ∉ ball 0 R
⊢ MeromorphicNFOn (canonicalFactor R w ^ F w) (ball 0 R)

Tactic:
simp only [hw, not_false_eq_true, locallyFinsuppWithin.apply_eq_zero_of_notMem, zpow_zero]

Goal state after:
case neg
R : ℝ
F : locallyFinsuppWithin (ball 0 R) ℤ
w : ℂ
hw : w ∉ ball 0 R
⊢ MeromorphicNFOn 1 (ball 0 R)