mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Calculus.ContDiff.Comp

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
n✝ : ℕ∞ω
s : Set E
t : Set F
g : F → G
f : E → F
x : E
st : MapsTo f s t
n : ℕ∞
hg : ContDiffWithinAt 𝕜 (↑n) g t (f x)
hf : ContDiffWithinAt 𝕜 (↑n) f s x
m : ℕ
hm : ↑m ≤ n
u : Set E
hu : u ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn (↑m) f p u
v : Set F
hv : v ∈ 𝓝[insert (f x) t] f x
q : F → FormalMultilinearSeries 𝕜 F G
hq : HasFTaylorSeriesUpToOn (↑m) g q v
w : Set E := ⋯
wv : w ⊆ f ⁻¹' v
wu : w ⊆ u
⊢ f '' s ⊆ t

Tactic:
exact image_subset_iff.mpr st

Goal state after:
Module: Mathlib.Analysis.Calculus.ContDiff.Comp

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
f : E → F
g : F → G
x : E
n : ℕ∞ω
t : Set F
hg : ContDiffWithinAt 𝕜 n g t (f x)
hf : ContDiffWithinAt 𝕜 n f s x
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hxs : x ∈ s
hst : ∀ᶠ (y : E) in 𝓝[s] x, f y ∈ t
i : ℕ
hi : ↑i ≤ n
⊢ iteratedFDerivWithin 𝕜 i (g ∘ f) s x = (ftaylorSeriesWithin 𝕜 g t (f x)).taylorComp (ftaylorSeriesWithin 𝕜 f s x) i

Tactic:
obtain ⟨u, hxu, huo, hfu, hgu⟩ : ∃ u, x ∈ u ∧ IsOpen u ∧
      HasFTaylorSeriesUpToOn i f (ftaylorSeriesWithin 𝕜 f s) (s ∩ u) ∧
      HasFTaylorSeriesUpToOn i g (ftaylorSeriesWithin 𝕜 g t) (f '' (s ∩ u)) := by
    have hxt : f x ∈ t := hst.self_of_nhdsWithin hxs
    have hf_tendsto : Tendsto f (𝓝[s] x) (𝓝[t] (f x)) :=
      tendsto_nhdsWithin_iff.mpr ⟨hf.continuousWithinAt, hst⟩
    have H₁ : ∀ᶠ u in (𝓝[s] x).smallSets,
        HasFTaylorSeriesUpToOn i f (ftaylorSeriesWithin 𝕜 f s) u :=
      hf.eventually_hasFTaylorSeriesUpToOn hs hxs hi
    have H₂ : ∀ᶠ u in (𝓝[s] x).smallSets,
        HasFTaylorSeriesUpToOn i g (ftaylorSeriesWithin 𝕜 g t) (f '' u) :=
      hf_tendsto.image_smallSets.eventually (hg.eventually_hasFTaylorSeriesUpToOn ht hxt hi)
    rcases (nhdsWithin_basis_open _ _).smallSets.eventually_iff.mp (H₁.and H₂)
      with ⟨u, ⟨hxu, huo⟩, hu⟩
    exact ⟨u, hxu, huo, hu (by simp [inter_comm])⟩
  exact .symm <| (hgu.comp hfu (mapsTo_image _ _)).eq_iteratedFDerivWithin_of_uniqueDiffOn le_rfl
    (hs.inter huo) ⟨hxs, hxu⟩ |>.trans <| iteratedFDerivWithin_inter_open huo hxu

Goal state after:
Module: Mathlib.Analysis.Calculus.Deriv.Inverse

Goal state before:
pp: 𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
f g h : 𝕜 → 𝕜
f' h' a : 𝕜
hst : ContinuousAt g a
hf : HasDerivAt f f' (g a)
hh : HasDerivAt h h' a
hf' : f' ≠ 0
hcomp : f ∘ g =ᶠ[𝓝 a] h
x✝ : 𝕜
⊢ (ContinuousLinearMap.toSpanSingleton 𝕜 f'⁻¹) ((ContinuousLinearMap.toSpanSingleton 𝕜 f') x✝) = x✝

Tactic:
simp [hf']

Goal state after:
Module: Mathlib.Analysis.Calculus.IteratedDeriv.Defs

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
m : Fin n → 𝕜
⊢ (iteratedFDerivWithin 𝕜 n f s x) m = (∏ i, m i) • iteratedDerivWithin n f s x

Tactic:
iteratedDerivWithin_eq_iteratedFDerivWithin,

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
m : Fin n → 𝕜
⊢ (iteratedFDerivWithin 𝕜 n f s x) m = (∏ i, m i) • (iteratedFDerivWithin 𝕜 n f s x) fun x ↦ 1
Module: Mathlib.Analysis.Calculus.IteratedDeriv.Defs

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
hxs : AccPt x (𝓟 s)
⊢ iteratedDerivWithin (n + 1) f s x = derivWithin (iteratedDerivWithin n f s) s x

Tactic:
iteratedDerivWithin_eq_iteratedFDerivWithin,

Goal state after:
case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
hxs : AccPt x (𝓟 s)
⊢ ((iteratedFDerivWithin 𝕜 (n + 1) f s x) fun x ↦ 1) = derivWithin (iteratedDerivWithin n f s) s x
Module: Mathlib.Analysis.Calculus.IteratedDeriv.Defs

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
hxs : AccPt x (𝓟 s)
⊢ ((fderivWithin 𝕜 (⇑(ContinuousMultilinearMap.piFieldEquiv 𝕜 (Fin n) F) ∘ iteratedDerivWithin n f s) s x) 1)
      (Fin.tail fun x ↦ 1) =
    derivWithin (iteratedDerivWithin n f s) s x

Tactic:
LinearIsometryEquiv.comp_fderivWithin _ hxs.uniqueDiffWithinAt,

Goal state after:
case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
hxs : AccPt x (𝓟 s)
⊢ ((↑↑(ContinuousMultilinearMap.piFieldEquiv 𝕜 (Fin n) F) ∘SL fderivWithin 𝕜 (iteratedDerivWithin n f s) s x) 1)
      (Fin.tail fun x ↦ 1) =
    derivWithin (iteratedDerivWithin n f s) s x
Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno

Goal state before:
pp: case inl
n : ℕ
c : OrderedFinpartition n
j : Fin c.length
h : range ((c.extendMiddle j).emb j) = {0}
⊢ False

Tactic:
have : Fin.succ (c.emb j 0) ∈ ({0} : Set (Fin n.succ)) := by
      rw [← h]
      simp only [Nat.succ_eq_add_one, mem_range]
      have A : (c.extendMiddle j).partSize j = c.partSize j + 1 := by simp [extendMiddle]
      refine ⟨Fin.cast A.symm (succ 0), ?_⟩
      simp only [extendMiddle, ↓reduceDIte, comp_apply, Fin.cast_cast, cast_eq_self, cases_succ]
    simp only [mem_singleton_iff] at this
    exact Fin.succ_ne_zero _ this

Goal state after:
Module: Mathlib.Analysis.Calculus.ContDiff.Defs

Goal state before:
pp: 𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
⊢ ContDiff 𝕜 ∞ f ↔ ∀ (n : ℕ), ContDiff 𝕜 (↑n) f

Tactic:
by
  simp [contDiffOn_univ.symm, contDiffOn_infty]

Goal state after:
Module: Mathlib.Analysis.Calculus.ContDiff.Defs

Goal state before:
pp: 𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
⊢ ContDiff 𝕜 0 f ↔
    Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
      f

Tactic:
rw [← contDiffOn_univ, ← continuousOn_univ]
  exact contDiffOn_zero

Goal state after:
Module: Mathlib.Analysis.Normed.Algebra.Exponential

Goal state before:
pp: 𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁵ : Field 𝕂
inst✝⁴ : Ring 𝔸
inst✝³ : Algebra 𝕂 𝔸
inst✝² : TopologicalSpace 𝔸
inst✝¹ : IsTopologicalRing 𝔸
inst✝ : Algebra ℚ 𝔸
x✝ : 𝔸
⊢ (expSeries 𝕂 𝔸).sum x✝ = (expSeries ℚ 𝔸).sum x✝

Tactic:
expSeries_sum_eq,

Goal state after:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁵ : Field 𝕂
inst✝⁴ : Ring 𝔸
inst✝³ : Algebra 𝕂 𝔸
inst✝² : TopologicalSpace 𝔸
inst✝¹ : IsTopologicalRing 𝔸
inst✝ : Algebra ℚ 𝔸
x✝ : 𝔸
⊢ ∑' (n : ℕ), (↑n !)⁻¹ • x✝ ^ n = ∑' (n : ℕ), (↑n !)⁻¹ • x✝ ^ n
Module: Mathlib.Analysis.Normed.Algebra.Exponential

Goal state before:
pp: case pos
𝔸 : Type u_2
inst✝² : Ring 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : IsTopologicalRing 𝔸
h✝ : Nonempty (Algebra ℚ 𝔸)
⊢ (expSeries ℚ 𝔸).sum 0 = 1

Tactic:
expSeries_sum_eq,

Goal state after:
case pos
𝔸 : Type u_2
inst✝² : Ring 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : IsTopologicalRing 𝔸
h✝ : Nonempty (Algebra ℚ 𝔸)
⊢ ∑' (n : ℕ), (↑n !)⁻¹ • 0 ^ n = 1
Module: Mathlib.Topology.MetricSpace.CauSeqFilter

Goal state before:
pp: β : Type v
inst✝¹ : NormedRing β
hn : IsAbsoluteValue norm
f : CauSeq β norm
inst✝ : IsComplete β norm
⊢ ∀ (s : Set β), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s → f.lim ∈ s → ↑f ⁻¹' s ∈ atTop

Tactic:
intro s

Goal state after:
β : Type v
inst✝¹ : NormedRing β
hn : IsAbsoluteValue norm
f : CauSeq β norm
inst✝ : IsComplete β norm
s : Set β
⊢ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s → f.lim ∈ s → ↑f ⁻¹' s ∈ atTop
Module: Mathlib.Topology.MetricSpace.CauSeqFilter

Goal state before:
pp: β : Type v
inst✝¹ : NormedRing β
hn : IsAbsoluteValue norm
f : CauSeq β norm
inst✝ : IsComplete β norm
s : Set β
os : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
lfs : f.lim ∈ s
ε : ℝ
hε : ε > 0
hεs : Metric.ball f.lim ε ⊆ s
N : ℕ
hN : ∀ j ≥ N, ‖↑(const norm f.lim - f) j‖ < ε
⊢ ∃ a, ∀ b ≥ a, ↑f b ∈ s

Tactic:
exists N

Goal state after:
β : Type v
inst✝¹ : NormedRing β
hn : IsAbsoluteValue norm
f : CauSeq β norm
inst✝ : IsComplete β norm
s : Set β
os : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
lfs : f.lim ∈ s
ε : ℝ
hε : ε > 0
hεs : Metric.ball f.lim ε ⊆ s
N : ℕ
hN : ∀ j ≥ N, ‖↑(const norm f.lim - f) j‖ < ε
⊢ ∀ b ≥ N, ↑f b ∈ s
Module: Mathlib.Topology.MetricSpace.CauSeqFilter

Goal state before:
pp: β : Type v
inst✝ : NormedField β
f : ℕ → β
hf : CauchySeq f
hf1 : (map f atTop).NeBot
hf2 : ∀ s ∈ uniformity β, ∃ t ∈ map f atTop, t ×ˢ t ⊆ s
ε : ℝ
hε : ε > 0
t : Set β
htsub : t ×ˢ t ⊆ {x | dist x.1 x.2 < ε}
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → f b ∈ t
⊢ ∃ i, ∀ j ≥ i, ‖f j - f i‖ < ε

Tactic:
exists N

Goal state after:
β : Type v
inst✝ : NormedField β
f : ℕ → β
hf : CauchySeq f
hf1 : (map f atTop).NeBot
hf2 : ∀ s ∈ uniformity β, ∃ t ∈ map f atTop, t ×ˢ t ⊆ s
ε : ℝ
hε : ε > 0
t : Set β
htsub : t ×ˢ t ⊆ {x | dist x.1 x.2 < ε}
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → f b ∈ t
⊢ ∀ j ≥ N, ‖f j - f N‖ < ε
Module: Mathlib.Topology.MetricSpace.CauSeqFilter

Goal state before:
pp: case left
β : Type v
inst✝ : NormedField β
f : CauSeq β norm
s : Set (β × β)
hs : s ∈ uniformity β
ε : ℝ
hε : ε > 0
hεs : ∀ ⦃a b : β⦄, dist a b < ε → (a, b) ∈ s
N : ℕ
hN : ∀ j ≥ N, ∀ k ≥ N, ‖↑f j - ↑f k‖ < ε
⊢ ∃ a, ∀ (b : ℕ), a ≤ b → b ∈ ↑f ⁻¹' ↑f '' {n | n ≥ N}

Tactic:
exists N

Goal state after:
case left
β : Type v
inst✝ : NormedField β
f : CauSeq β norm
s : Set (β × β)
hs : s ∈ uniformity β
ε : ℝ
hε : ε > 0
hεs : ∀ ⦃a b : β⦄, dist a b < ε → (a, b) ∈ s
N : ℕ
hN : ∀ j ≥ N, ∀ k ≥ N, ‖↑f j - ↑f k‖ < ε
⊢ ∀ (b : ℕ), N ≤ b → b ∈ ↑f ⁻¹' ↑f '' {n | n ≥ N}
Module: Mathlib.Topology.MetricSpace.CauSeqFilter

Goal state before:
pp: β : Type v
inst✝¹ : NormedField β
inst✝ : CauSeq.IsComplete β norm
u : ℕ → β
hu : CauchySeq u
C : IsCauSeq norm u
ε : ℝ
εpos : ε > 0
N : ℕ
hN : ∀ j ≥ N, ‖↑(⟨u, C⟩ - CauSeq.const norm (CauSeq.lim ⟨u, C⟩)) j‖ < ε
⊢ ∃ N, ∀ n ≥ N, dist (u n) (CauSeq.lim ⟨u, C⟩) < ε

Tactic:
exists N

Goal state after:
β : Type v
inst✝¹ : NormedField β
inst✝ : CauSeq.IsComplete β norm
u : ℕ → β
hu : CauchySeq u
C : IsCauSeq norm u
ε : ℝ
εpos : ε > 0
N : ℕ
hN : ∀ j ≥ N, ‖↑(⟨u, C⟩ - CauSeq.const norm (CauSeq.lim ⟨u, C⟩)) j‖ < ε
⊢ ∀ n ≥ N, dist (u n) (CauSeq.lim ⟨u, C⟩) < ε
Module: Mathlib.Topology.MetricSpace.CauSeqFilter

Goal state before:
pp: β : Type v
inst✝¹ : NormedField β
inst✝ : CauSeq.IsComplete β norm
⊢ CompleteSpace β

Tactic:
apply complete_of_cauchySeq_tendsto
  intro u hu
  have C : IsCauSeq norm u := isCauSeq_iff_cauchySeq.2 hu
  exists CauSeq.lim ⟨u, C⟩
  rw [Metric.tendsto_atTop]
  intro ε εpos
  obtain ⟨N, hN⟩ := (CauSeq.equiv_lim ⟨u, C⟩) _ εpos
  exists N
  simpa [dist_eq_norm] using hN

Goal state after:
Module: Mathlib.Analysis.Calculus.LocalExtr.Basic

Goal state before:
pp: E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a : E
⊢ Monotone fun s ↦ posTangentConeAt s a

Tactic:
intro s

Goal state after:
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a : E
s : Set E
⊢ ∀ ⦃b : Set E⦄, s ⊆ b → (fun s ↦ posTangentConeAt s a) s ⊆ (fun s ↦ posTangentConeAt s a) b
Module: Mathlib.Analysis.Calculus.ContDiff.Operations

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : E
i : ℕ
f : E → F
⊢ iteratedFDerivWithin 𝕜 i (-f) univ x = -iteratedFDerivWithin 𝕜 i f univ x

Tactic:
exact iteratedFDerivWithin_neg_apply uniqueDiffOn_univ (Set.mem_univ _)

Goal state after:
Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set 𝕜
f g : 𝕜 → F
hfg : EqOn f g s
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
n : ℕ
⊢ EqOn (iteratedDeriv n f) (iteratedDeriv n g) s

Tactic:
by
  refine fun x hx ↦ Filter.EventuallyEq.iteratedDeriv_eq n ?_
  filter_upwards [IsOpen.mem_nhds hs hx] with a ha
  exact hfg ha

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Bochner.FundThmCalculus

Goal state before:
pp: X : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁴ : MeasurableSpace X
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure X
l : Filter X
inst✝ : l.IsMeasurablyGenerated
f : X → E
b : E
h : Tendsto f (l ⊓ ae μ) (𝓝 b)
hfm : StronglyMeasurableAtFilter f l μ
hμ : μ.FiniteAtFilter l
s : ι → Set X
li : Filter ι
hs : Tendsto s li l.smallSets
m : ι → ℝ
hsμ : (fun i ↦ μ.real (s i)) =ᶠ[li] m
ε : ℝ
ε₀ : 0 < ε
this : ∀ᶠ (s : Set X) in l.smallSets, ∀ᵐ (x : X) ∂μ, x ∈ s → f x ∈ closedBall b ε
⊢ ∀ (a : Set X),
    μ a < ⊤ →
      IntegrableOn f a μ →
        AEStronglyMeasurable f (μ.restrict a) →
          (∀ᵐ (x : X) ∂μ, x ∈ a → ‖f x - b‖ ≤ ε) → ‖∫ (x : X) in a, f x ∂μ - μ.real a • b‖ ≤ ε * ‖μ.real a‖

Tactic:
intro s

Goal state after:
X : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁴ : MeasurableSpace X
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure X
l : Filter X
inst✝ : l.IsMeasurablyGenerated
f : X → E
b : E
h : Tendsto f (l ⊓ ae μ) (𝓝 b)
hfm : StronglyMeasurableAtFilter f l μ
hμ : μ.FiniteAtFilter l
s✝ : ι → Set X
li : Filter ι
hs : Tendsto s✝ li l.smallSets
m : ι → ℝ
hsμ : (fun i ↦ μ.real (s✝ i)) =ᶠ[li] m
ε : ℝ
ε₀ : 0 < ε
this : ∀ᶠ (s : Set X) in l.smallSets, ∀ᵐ (x : X) ∂μ, x ∈ s → f x ∈ closedBall b ε
s : Set X
⊢ μ s < ⊤ →
    IntegrableOn f s μ →
      AEStronglyMeasurable f (μ.restrict s) →
        (∀ᵐ (x : X) ∂μ, x ∈ s → ‖f x - b‖ ≤ ε) → ‖∫ (x : X) in s, f x ∂μ - μ.real s • b‖ ≤ ε * ‖μ.real s‖
Module: Mathlib.Analysis.Calculus.Deriv.MeanValue

Goal state before:
pp: case inl
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
C : ℝ
hf'_ge : ∀ x ∈ interior D, C ≤ deriv f x
x : ℝ
hx : x ∈ D
y : ℝ
hy : y ∈ D
hxy : x ≤ y
hxy' : x = y
⊢ C * (y - x) ≤ f y - f x

Tactic:
rw [hxy', sub_self, sub_self, mul_zero]

Goal state after:
Module: Mathlib.Analysis.Calculus.FDeriv.Measurable

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
K : Set (E →L[𝕜] F)
hK : IsComplete K
P : ∀ {n : ℕ}, 0 < (1 / 2) ^ n
c : 𝕜
hc : 1 < ‖c‖
x : E
hx : x ∈ D f K
n : ℕ → ℕ
L : ℕ → ℕ → ℕ → E →L[𝕜] F
hn :
  ∀ (e p q : ℕ),
    n e ≤ p →
      n e ≤ q → L e p q ∈ K ∧ x ∈ A f (L e p q) ((1 / 2) ^ p) ((1 / 2) ^ e) ∩ A f (L e p q) ((1 / 2) ^ q) ((1 / 2) ^ e)
M :
  ∀ (e p q e' p' q' : ℕ),
    n e ≤ p → n e ≤ q → n e' ≤ p' → n e' ≤ q' → e ≤ e' → ‖L e p q - L e' p' q'‖ ≤ 12 * ‖c‖ * (1 / 2) ^ e
L0 : ℕ → E →L[𝕜] F := ⋯
this : CauchySeq L0
f' : E →L[𝕜] F
f'K : f' ∈ K
hf' : Tendsto L0 atTop (𝓝 f')
e p : ℕ
hp : n e ≤ p
⊢ ∀ᶠ (c_1 : ℕ) in atTop, ‖L e (n e) p - L0 c_1‖ ≤ 12 * ‖c‖ * (1 / 2) ^ e

Tactic:
rw [eventually_atTop]

Goal state after:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
K : Set (E →L[𝕜] F)
hK : IsComplete K
P : ∀ {n : ℕ}, 0 < (1 / 2) ^ n
c : 𝕜
hc : 1 < ‖c‖
x : E
hx : x ∈ D f K
n : ℕ → ℕ
L : ℕ → ℕ → ℕ → E →L[𝕜] F
hn :
  ∀ (e p q : ℕ),
    n e ≤ p →
      n e ≤ q → L e p q ∈ K ∧ x ∈ A f (L e p q) ((1 / 2) ^ p) ((1 / 2) ^ e) ∩ A f (L e p q) ((1 / 2) ^ q) ((1 / 2) ^ e)
M :
  ∀ (e p q e' p' q' : ℕ),
    n e ≤ p → n e ≤ q → n e' ≤ p' → n e' ≤ q' → e ≤ e' → ‖L e p q - L e' p' q'‖ ≤ 12 * ‖c‖ * (1 / 2) ^ e
L0 : ℕ → E →L[𝕜] F := fun e ↦ L e (n e) (n e)
this : CauchySeq L0
f' : E →L[𝕜] F
f'K : f' ∈ K
hf' : Tendsto L0 atTop (𝓝 f')
e p : ℕ
hp : n e ≤ p
⊢ ∃ a, ∀ (b : ℕ), a ≤ b → ‖L e (n e) p - L0 b‖ ≤ 12 * ‖c‖ * (1 / 2) ^ e
Module: Mathlib.Analysis.Convex.Gauge

Goal state before:
pp: E : Type u_2
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
s : Set E
x : E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
hc : Convex ℝ s
hs₀ : s ∈ 𝓝 0
ha : Absorbent ℝ s
⊢ ContinuousAt (gauge s) x

Tactic:
refine (nhds_basis_Icc_pos _).tendsto_right_iff.2 fun ε hε₀ ↦ ?_

Goal state after:
E : Type u_2
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
s : Set E
x : E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
hc : Convex ℝ s
hs₀ : s ∈ 𝓝 0
ha : Absorbent ℝ s
ε : ℝ
hε₀ : 0 < ε
⊢ ∀ᶠ (x_1 : E) in 𝓝 x, gauge s x_1 ∈ Icc (gauge s x - ε) (gauge s x + ε)
Module: Mathlib.Analysis.LocallyConvex.Separation

Goal state before:
pp: E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s t : Set E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
hs : Convex ℝ s
ht : Convex ℝ t
hst : Disjoint (interior s) t
hsint : (interior s).Nonempty
htne : t.Nonempty
⊢ ∃ f u, f ≠ 0 ∧ (∀ a ∈ s, f a ≤ u) ∧ ∀ b ∈ t, u ≤ f b

Tactic:
obtain ⟨f, u, hfA, hfB⟩ :=
    geometric_hahn_banach_open hs.interior isOpen_interior ht hst

Goal state after:
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s t : Set E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
hs : Convex ℝ s
ht : Convex ℝ t
hst : Disjoint (interior s) t
hsint : (interior s).Nonempty
htne : t.Nonempty
f : StrongDual ℝ E
u : ℝ
hfA : ∀ a ∈ interior s, f a < u
hfB : ∀ b ∈ t, u ≤ f b
⊢ ∃ f u, f ≠ 0 ∧ (∀ a ∈ s, f a ≤ u) ∧ ∀ b ∈ t, u ≤ f b
Module: Mathlib.Analysis.LocallyConvex.SeparatingDual

Goal state before:
pp: R : Type u_4
V : Type u_5
W : Type u_6
inst✝¹³ : NormedField R
inst✝¹² : AddCommGroup V
inst✝¹¹ : AddCommGroup W
inst✝¹⁰ : TopologicalSpace R
inst✝⁹ : TopologicalSpace V
inst✝⁸ : TopologicalSpace W
inst✝⁷ : IsTopologicalRing R
inst✝⁶ : Module R V
inst✝⁵ : Module R W
inst✝⁴ : SeparatingDual R V
inst✝³ : IsTopologicalAddGroup V
inst✝² : IsTopologicalAddGroup W
inst✝¹ : ContinuousSMul R V
inst✝ : ContinuousSMul R W
f g : V ≃L[R] W
⊢ (∀ (x : V →L[R] V), ↑g ∘SL x ∘SL ↑g.symm = ↑f ∘SL x ∘SL ↑f.symm) ↔ ∃ α, f = α • g

Tactic:
← eq_toContinuousLinearMap_symm_comp,

Goal state after:
R : Type u_4
V : Type u_5
W : Type u_6
inst✝¹³ : NormedField R
inst✝¹² : AddCommGroup V
inst✝¹¹ : AddCommGroup W
inst✝¹⁰ : TopologicalSpace R
inst✝⁹ : TopologicalSpace V
inst✝⁸ : TopologicalSpace W
inst✝⁷ : IsTopologicalRing R
inst✝⁶ : Module R V
inst✝⁵ : Module R W
inst✝⁴ : SeparatingDual R V
inst✝³ : IsTopologicalAddGroup V
inst✝² : IsTopologicalAddGroup W
inst✝¹ : ContinuousSMul R V
inst✝ : ContinuousSMul R W
f g : V ≃L[R] W
⊢ (∀ (x : V →L[R] V), x ∘SL ↑g.symm = ↑g.symm ∘SL ↑f ∘SL x ∘SL ↑f.symm) ↔ ∃ α, f = α • g
Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory

Goal state before:
pp: α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : μ.WeaklyRegular
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f μ
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := NNReal.mk (ε / 2) ⋯
δpos : 0 < δ
fp : α → ℝ≥0 := fun x ↦ (f x).toNNReal
int_fp : Integrable (fun x ↦ ↑(fp x)) μ
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ∞
gp_integrable : Integrable (fun x ↦ (gp x).toReal) μ
gpint : ∫ (x : α), (gp x).toReal ∂μ < ∫ (x : α), ↑(fp x) ∂μ + ↑δ
fm : α → ℝ≥0 := fun x ↦ (-f x).toNNReal
int_fm : Integrable (fun x ↦ ↑(fm x)) μ
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable (fun x ↦ ↑(gm x)) μ
gmint : ∫ (x : α), ↑(fm x) ∂μ - ↑δ ≤ ∫ (x : α), ↑(gm x) ∂μ
g : α → EReal := fun x ↦ ↑(gp x) - ↑↑(gm x)
ae_g : ∀ᵐ (x : α) ∂μ, (g x).toReal = (↑(gp x)).toReal - (↑↑(gm x)).toReal
⊢ ∀ᵐ (x : α) ∂μ, g x < ⊤

Tactic:
show ∀ᵐ x : α ∂μ, g x < ⊤

Goal state after:
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : μ.WeaklyRegular
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f μ
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := NNReal.mk (ε / 2) ⋯
δpos : 0 < δ
fp : α → ℝ≥0 := fun x ↦ (f x).toNNReal
int_fp : Integrable (fun x ↦ ↑(fp x)) μ
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ∞
gp_integrable : Integrable (fun x ↦ (gp x).toReal) μ
gpint : ∫ (x : α), (gp x).toReal ∂μ < ∫ (x : α), ↑(fp x) ∂μ + ↑δ
fm : α → ℝ≥0 := fun x ↦ (-f x).toNNReal
int_fm : Integrable (fun x ↦ ↑(fm x)) μ
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable (fun x ↦ ↑(gm x)) μ
gmint : ∫ (x : α), ↑(fm x) ∂μ - ↑δ ≤ ∫ (x : α), ↑(gm x) ∂μ
g : α → EReal := fun x ↦ ↑(gp x) - ↑↑(gm x)
ae_g : ∀ᵐ (x : α) ∂μ, (g x).toReal = (↑(gp x)).toReal - (↑↑(gm x)).toReal
⊢ ∀ᵐ (x : α) ∂μ, g x < ⊤
Module: Mathlib.Analysis.LocallyConvex.Separation

Goal state before:
pp: E : Type u_2
inst✝⁵ : TopologicalSpace E
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
s t : Set E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
hs₁ : Convex ℝ s
hs₂ : IsCompact s
ht₁ : Convex ℝ t
ht₂ : IsClosed t
disj : Disjoint s t
hs : s.Nonempty
_ht : t.Nonempty
U V : Set E
hU : IsOpen U
hV : IsOpen V
hU₁ : Convex ℝ U
hV₁ : Convex ℝ V
sU : s ⊆ U
tV : t ⊆ V
disj' : Disjoint U V
f : StrongDual ℝ E
u : ℝ
hf₁ : ∀ a ∈ U, f a < u
hf₂ : ∀ b ∈ V, u < f b
x : E
hx₁ : x ∈ s
hx₂ : IsMaxOn (⇑f) s x
this : f x < u
a : E
ha : a ∈ s
⊢ f a < (f x + u) / 2

Tactic:
by have := hx₂ ha; dsimp at this; linarith

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

Goal state before:
pp: R : Type u_4
V : Type u_5
W : Type u_6
inst✝¹³ : NormedField R
inst✝¹² : AddCommGroup V
inst✝¹¹ : AddCommGroup W
inst✝¹⁰ : TopologicalSpace R
inst✝⁹ : TopologicalSpace V
inst✝⁸ : TopologicalSpace W
inst✝⁷ : IsTopologicalRing R
inst✝⁶ : Module R V
inst✝⁵ : Module R W
inst✝⁴ : SeparatingDual R V
inst✝³ : IsTopologicalAddGroup V
inst✝² : IsTopologicalAddGroup W
inst✝¹ : ContinuousSMul R V
inst✝ : ContinuousSMul R W
f g : V ≃L[R] W
⊢ (∃ y, (algebraMap R (V →L[R] V)) y = ↑g.symm ∘SL ↑f) ↔ ∃ α, f = α • g

Tactic:
Algebra.algebraMap_eq_smul_one,

Goal state after:
R : Type u_4
V : Type u_5
W : Type u_6
inst✝¹³ : NormedField R
inst✝¹² : AddCommGroup V
inst✝¹¹ : AddCommGroup W
inst✝¹⁰ : TopologicalSpace R
inst✝⁹ : TopologicalSpace V
inst✝⁸ : TopologicalSpace W
inst✝⁷ : IsTopologicalRing R
inst✝⁶ : Module R V
inst✝⁵ : Module R W
inst✝⁴ : SeparatingDual R V
inst✝³ : IsTopologicalAddGroup V
inst✝² : IsTopologicalAddGroup W
inst✝¹ : ContinuousSMul R V
inst✝ : ContinuousSMul R W
f g : V ≃L[R] W
⊢ (∃ y, y • 1 = ↑g.symm ∘SL ↑f) ↔ ∃ α, f = α • g
Module: Mathlib.Analysis.Normed.Operator.CompleteCodomain

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : SeparatingDual 𝕜 E
inst✝¹ : Nontrivial E
inst✝ : CompleteSpace (E →L[𝕜] F)
f : ℕ → F
hf : CauchySeq f
v : E
hv : v ≠ 0
φ : StrongDual 𝕜 E
hφ : φ v = 1
⊢ ∃ a, Tendsto f atTop (𝓝 a)

Tactic:
let g : ℕ → (E →L[𝕜] F) := fun n ↦ ContinuousLinearMap.smulRightL 𝕜 E F φ (f n)

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : SeparatingDual 𝕜 E
inst✝¹ : Nontrivial E
inst✝ : CompleteSpace (E →L[𝕜] F)
f : ℕ → F
hf : CauchySeq f
v : E
hv : v ≠ 0
φ : StrongDual 𝕜 E
hφ : φ v = 1
g : ℕ → E →L[𝕜] F := fun n ↦ ((ContinuousLinearMap.smulRightL 𝕜 E F) φ) (f n)
⊢ ∃ a, Tendsto f atTop (𝓝 a)