mathlib-initiative/mathlib-tactics huggingface dataset:
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
s : Set E
f : E → F
x : E
u : Set E
hu : u ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn ω f p u
h'p : ∀ (i : ℕ), AnalyticOn 𝕜 (fun x ↦ p x i) u
⊢ ∃ u ∈ 𝓝[insert x s] x, AnalyticOn 𝕜 f u

Tactic:
exact ⟨u, hu, hp.analyticOn (h'p 0)⟩

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 : ℕ
c : F
s : Set 𝕜
x : 𝕜
⊢ iteratedDerivWithin n (fun x ↦ c) s x = if n = 0 then c else 0

Tactic:
induction n generalizing c with
  | zero => simp
  | succ n h => simp [iteratedDerivWithin_succ', Pi.zero_def, h]

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
n : ℕ∞ω
f : E → F
s : Set E
a : E
h : ContDiffWithinAt 𝕜 n f s a
hs : UniqueDiffOn 𝕜 s
ha : a ∈ s
m : ℕ
hm : ↑m ≤ n
U : Set E
hUo : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
haU : a ∈ U
hfU : ContDiffOn 𝕜 (↑m) f (insert a s ∩ U)
⊢ ∀ᶠ (t : Set E) in (𝓝[s] a).smallSets, HasFTaylorSeriesUpToOn (↑m) f (ftaylorSeriesWithin 𝕜 f s) t

Tactic:
have : ∀ᶠ t in (𝓝[s] a).smallSets, t ⊆ s ∩ U := by
    rw [eventually_smallSets_subset]
    exact inter_mem_nhdsWithin _ <| hUo.mem_nhds haU

Goal state after:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ∞ω
f : E → F
s : Set E
a : E
h : ContDiffWithinAt 𝕜 n f s a
hs : UniqueDiffOn 𝕜 s
ha : a ∈ s
m : ℕ
hm : ↑m ≤ n
U : Set E
hUo : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
haU : a ∈ U
hfU : ContDiffOn 𝕜 (↑m) f (insert a s ∩ U)
this : ∀ᶠ (t : Set E) in (𝓝[s] a).smallSets, t ⊆ s ∩ U
⊢ ∀ᶠ (t : Set E) in (𝓝[s] a).smallSets, HasFTaylorSeriesUpToOn (↑m) f (ftaylorSeriesWithin 𝕜 f s) t
Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno

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
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
c✝ : OrderedFinpartition n
c : OrderedFinpartition (n + 1)
hc : range (c.emb 0) ≠ {0}
i : Fin c.length
j : Fin (update c.partSize (c.index 0) (c.partSize (c.index 0) - 1) i)
⊢ Fin n

Tactic:
by
    by_cases h : i = c.index 0
    · refine Fin.pred (c.emb i (Fin.cast ?_ (succ j))) ?_
      · rw [h]
        simpa using Nat.sub_add_cancel (c.partSize_pos (c.index 0))
      · have : 0 ≤ c.emb i 0 := Fin.zero_le _
        exact (this.trans_lt (c.emb_strictMono _ (succ_pos _))).ne'
    · refine Fin.pred (c.emb i (Fin.cast ?_ j)) ?_
      · simp [h]
      · conv_rhs => rw [← c.emb_invEmbedding 0]
        exact c.emb_ne_emb_of_ne h

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

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
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
t : Set F
q✝ : F → FormalMultilinearSeries 𝕜 F G
p✝ : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
c : OrderedFinpartition n
f : F [×c.length]→L[𝕜] G
p : (i : Fin c.length) → E [×c.partSize i]→L[𝕜] F
m : Fin c.length
q q' : E [×c.partSize m]→L[𝕜] F
⊢ c.compAlongOrderedFinpartition f (update p m (q + q')) =
    c.compAlongOrderedFinpartition f (update p m q) + c.compAlongOrderedFinpartition f (update p m q')

Tactic:
ext v

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
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
t : Set F
q✝ : F → FormalMultilinearSeries 𝕜 F G
p✝ : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
c : OrderedFinpartition n
f : F [×c.length]→L[𝕜] G
p : (i : Fin c.length) → E [×c.partSize i]→L[𝕜] F
m : Fin c.length
q q' : E [×c.partSize m]→L[𝕜] F
v : Fin n → E
⊢ (c.compAlongOrderedFinpartition f (update p m (q + q'))) v =
    (c.compAlongOrderedFinpartition f (update p m q) + c.compAlongOrderedFinpartition f (update p m q')) v
Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno

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
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
t : Set F
q✝ : F → FormalMultilinearSeries 𝕜 F G
p✝ : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
c : OrderedFinpartition n
f : F [×c.length]→L[𝕜] G
p : (i : Fin c.length) → E [×c.partSize i]→L[𝕜] F
m : Fin c.length
a : 𝕜
q : E [×c.partSize m]→L[𝕜] F
⊢ c.compAlongOrderedFinpartition f (update p m (a • q)) = a • c.compAlongOrderedFinpartition f (update p m q)

Tactic:
ext v

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
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
t : Set F
q✝ : F → FormalMultilinearSeries 𝕜 F G
p✝ : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
c : OrderedFinpartition n
f : F [×c.length]→L[𝕜] G
p : (i : Fin c.length) → E [×c.partSize i]→L[𝕜] F
m : Fin c.length
a : 𝕜
q : E [×c.partSize m]→L[𝕜] F
v : Fin n → E
⊢ (c.compAlongOrderedFinpartition f (update p m (a • q))) v = (a • c.compAlongOrderedFinpartition f (update p m q)) v
Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno

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
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n : WithTop ℕ∞
g : F → G
f : E → F
hg : HasFTaylorSeriesUpToOn n g q t
hf : HasFTaylorSeriesUpToOn n f p s
h : MapsTo f s t
m : ℕ
hm : ↑m < n
x : E
hx : x ∈ s
A :
  ∀ (c : OrderedFinpartition m),
    HasFDerivWithinAt (fun x ↦ (q (f x)).compAlongOrderedFinpartition (p x) c)
      (∑ i, ((q (f x)).compAlongOrderedFinpartition (p x) (c.extend i)).curryLeft) s x
B :
  HasFDerivWithinAt (fun x ↦ (q (f x)).taylorComp (p x) m)
    (∑ c, ∑ i, ((q (f x)).compAlongOrderedFinpartition (p x) (c.extend i)).curryLeft) s x
this : ∑ c, ∑ i, (q (f x)).compAlongOrderedFinpartition (p x) (c.extend i) = (q (f x)).taylorComp (p x) (m + 1)
⊢ (∑ c, ∑ i, (q (f x)).compAlongOrderedFinpartition (p x) (c.extend i)).curryLeft =
    ∑ c, ∑ i, ((q (f x)).compAlongOrderedFinpartition (p x) (c.extend i)).curryLeft

Tactic:
ext v

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
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n : WithTop ℕ∞
g : F → G
f : E → F
hg : HasFTaylorSeriesUpToOn n g q t
hf : HasFTaylorSeriesUpToOn n f p s
h : MapsTo f s t
m : ℕ
hm : ↑m < n
x : E
hx : x ∈ s
A :
  ∀ (c : OrderedFinpartition m),
    HasFDerivWithinAt (fun x ↦ (q (f x)).compAlongOrderedFinpartition (p x) c)
      (∑ i, ((q (f x)).compAlongOrderedFinpartition (p x) (c.extend i)).curryLeft) s x
B :
  HasFDerivWithinAt (fun x ↦ (q (f x)).taylorComp (p x) m)
    (∑ c, ∑ i, ((q (f x)).compAlongOrderedFinpartition (p x) (c.extend i)).curryLeft) s x
this : ∑ c, ∑ i, (q (f x)).compAlongOrderedFinpartition (p x) (c.extend i) = (q (f x)).taylorComp (p x) (m + 1)
v : E
x✝ : Fin m → E
⊢ ((∑ c, ∑ i, (q (f x)).compAlongOrderedFinpartition (p x) (c.extend i)).curryLeft v) x✝ =
    ((∑ c, ∑ i, ((q (f x)).compAlongOrderedFinpartition (p x) (c.extend i)).curryLeft) v) x✝
Module: Mathlib.Analysis.Calculus.ContDiff.Operations

Goal state before:
pp: case succ
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
i✝ : ℕ
a : 𝕜
i : ℕ
hi : ContDiff 𝕜 (↑i) f → (iteratedFDeriv 𝕜 i fun z ↦ f (a • z)) = fun x ↦ a ^ i • iteratedFDeriv 𝕜 i f (a • x)
hf : ContDiff 𝕜 (↑(i + 1)) f
⊢ (iteratedFDeriv 𝕜 (i + 1) fun z ↦ f (a • z)) = fun x ↦ a ^ (i + 1) • iteratedFDeriv 𝕜 (i + 1) f (a • x)

Tactic:
ext v

Goal state after:
case succ
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
i✝ : ℕ
a : 𝕜
i : ℕ
hi : ContDiff 𝕜 (↑i) f → (iteratedFDeriv 𝕜 i fun z ↦ f (a • z)) = fun x ↦ a ^ i • iteratedFDeriv 𝕜 i f (a • x)
hf : ContDiff 𝕜 (↑(i + 1)) f
v : E
x✝ : Fin (i + 1) → E
⊢ (iteratedFDeriv 𝕜 (i + 1) (fun z ↦ f (a • z)) v) x✝ = (a ^ (i + 1) • iteratedFDeriv 𝕜 (i + 1) f (a • v)) x✝
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
n : ℕ∞ω
inst✝ : CompleteSpace E
e : E ≃L[𝕜] F
⊢ ContDiffAt 𝕜 n inverse ↑e

Tactic:
nontriviality E
  -- first, we use the lemma `inverse_eq_ringInverse` to rewrite in terms of `Ring.inverse` in the
  -- ring `E →L[𝕜] E`
  let O₁ : (E →L[𝕜] E) → F →L[𝕜] E := fun f => f.comp (e.symm : F →L[𝕜] E)
  let O₂ : (E →L[𝕜] F) → E →L[𝕜] E := fun f => (e.symm : F →L[𝕜] E).comp f
  have : ContinuousLinearMap.inverse = O₁ ∘ Ring.inverse ∘ O₂ := funext (inverse_eq_ringInverse e)
  rw [this]
  -- `O₁` and `O₂` are `ContDiff`,
  -- so we reduce to proving that `Ring.inverse` is `ContDiff`
  have h₁ : ContDiff 𝕜 n O₁ := contDiff_id.clm_comp contDiff_const
  have h₂ : ContDiff 𝕜 n O₂ := contDiff_const.clm_comp contDiff_id
  refine h₁.contDiffAt.comp _ (ContDiffAt.comp _ ?_ h₂.contDiffAt)
  convert! contDiffAt_ringInverse 𝕜 (1 : (E →L[𝕜] E)ˣ)
  simp [O₂, one_def]

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

Goal state before:
pp: case neg
f : ℝ → ℝ
a : ℝ
hf : Tendsto (derivWithin f (Ioi a)) (𝓝[>] a) atTop
hcont_at_a : ContinuousWithinAt f (Ici a) a
hdiff : Tendsto (slope f a) (𝓝[>] a) (𝓝 (derivWithin f (Ioi a) a))
h₀ : ∀ᶠ (b : ℝ) in 𝓝[>] a, ∀ x ∈ Ioc a b, max (derivWithin f (Ioi a) a + 1) 0 < derivWithin f (Ioi a) x
h₁ : ∀ᶠ (b : ℝ) in 𝓝[>] a, slope f a b < derivWithin f (Ioi a) a + 1
b : ℝ
hb : ∀ x ∈ Ioc a b, max (derivWithin f (Ioi a) a + 1) 0 < derivWithin f (Ioi a) x
hslope : slope f a b < derivWithin f (Ioi a) a + 1
hab : a < b
hdiff' : DifferentiableOn ℝ f (Ioc a b)
hcont_Ioc : ∀ z ∈ Ioc a b, ContinuousWithinAt f (Icc a b) z
z : ℝ
hz : z ∈ Icc a b
hz' : ¬z = a
⊢ ContinuousWithinAt f (Icc a b) z

Tactic:
exact hcont_Ioc z ⟨lt_of_le_of_ne hz.1 (Ne.symm hz'), hz.2⟩

Goal state after:
Module: Mathlib.Geometry.Convex.Cone.Basic

Goal state before:
pp: R : Type u_2
G : Type u_3
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : AddCommGroup G
inst✝ : SMul R G
C : ConvexCone R G
⊢ C.Blunt → C.Salient

Tactic:
salient_iff_not_flat,

Goal state after:
R : Type u_2
G : Type u_3
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : AddCommGroup G
inst✝ : SMul R G
C : ConvexCone R G
⊢ C.Blunt → ¬C.Flat
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 : α → ℝ≥0
fmeas : AEMeasurable f μ
ε : ℝ≥0∞
ε0 : ε ≠ 0
this : ε / 2 ≠ 0
g0 : α → ℝ≥0∞
f_lt_g0 : ∀ (x : α), ↑(AEMeasurable.mk f fmeas x) < g0 x
g0_cont : LowerSemicontinuous g0
g0_int : ∫⁻ (x : α), g0 x ∂μ ≤ ∫⁻ (x : α), ↑(AEMeasurable.mk f fmeas x) ∂μ + ε / 2
s : Set α
hs : {x | (fun x ↦ f x = AEMeasurable.mk f fmeas x) x}ᶜ ⊆ s
smeas : MeasurableSet s
μs : μ s = 0
g1 : α → ℝ≥0∞
le_g1 : ∀ (x : α), s.indicator (fun _x ↦ ∞) x ≤ g1 x
g1_cont : LowerSemicontinuous g1
g1_int : ∫⁻ (x : α), g1 x ∂μ ≤ ∫⁻ (x : α), s.indicator (fun _x ↦ ∞) x ∂μ + ε / 2
⊢ ∫⁻ (x : α), ↑(f x) ∂μ + ε / 2 + (0 + ε / 2) = ∫⁻ (x : α), ↑(f x) ∂μ + ε

Tactic:
by simp only [add_assoc, ENNReal.add_halves, zero_add]

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

Goal state before:
pp: x : ℝ
h : |x| < 1
n : ℕ
F : ℝ → ℝ := fun x ↦ ∑ i ∈ Finset.range n, x ^ (i + 1) / (↑i + 1) + log (1 - x)
F' : ℝ → ℝ := fun x ↦ -x ^ n / (1 - x)
y : ℝ
hy : y ∈ Set.Ioo (-1) 1
this : HasDerivAt F (∑ i ∈ Finset.range n, ↑(i + 1) * y ^ i / (↑i + 1) + -1 / (1 - y)) y
⊢ ∑ i ∈ Finset.range n, y ^ i + -1 / (1 - y) = ∑ i ∈ Finset.range n, ↑(i + 1) * y ^ i / (↑i + 1) + -1 / (1 - y)

Tactic:
by
        congr with i
        rw [Nat.cast_succ, mul_div_cancel_left₀ _ (Nat.cast_add_one_pos i).ne']

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

Goal state before:
pp: x : ℝ
h : |x| < 1
⊢ HasSum (fun n ↦ x ^ (n + 1) / (↑n + 1)) (-log (1 - x))

Tactic:
by
  rw [Summable.hasSum_iff_tendsto_nat]
  · show Tendsto (fun n : ℕ => ∑ i ∈ range n, x ^ (i + 1) / (i + 1)) atTop (𝓝 (-log (1 - x)))
    rw [tendsto_iff_norm_sub_tendsto_zero]
    simp only [norm_eq_abs, sub_neg_eq_add]
    refine squeeze_zero (fun n => abs_nonneg _) (abs_log_sub_add_sum_range_le h) ?_
    suffices Tendsto (fun t : ℕ => |x| ^ (t + 1) / (1 - |x|)) atTop (𝓝 (|x| * 0 / (1 - |x|))) by
      simpa
    simp only [pow_succ']
    refine (tendsto_const_nhds.mul ?_).div_const _
    exact tendsto_pow_atTop_nhds_zero_of_lt_one (abs_nonneg _) h
  show Summable fun n : ℕ => x ^ (n + 1) / (n + 1)
  refine .of_norm_bounded (summable_geometric_of_lt_one (abs_nonneg _) h) fun i => ?_
  calc
    ‖x ^ (i + 1) / (i + 1)‖ = |x| ^ (i + 1) / (i + 1) := by
      have : (0 : ℝ) ≤ i + 1 := le_of_lt (Nat.cast_add_one_pos i)
      rw [norm_eq_abs, abs_div, ← pow_abs, abs_of_nonneg this]
    _ ≤ |x| ^ (i + 1) / (0 + 1) := by
      gcongr
      positivity
    _ ≤ |x| ^ i := by
      simpa [pow_succ] using mul_le_of_le_one_right (by positivity) h.le

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 := fun e ↦ L e (n e) (n e)
this : CauchySeq L0
f' : E →L[𝕜] F
f'K : f' ∈ K
hf' : Tendsto L0 atTop (𝓝 f')
Lf' : ∀ (e p : ℕ), n e ≤ p → ‖L e (n e) p - f'‖ ≤ 12 * ‖c‖ * (1 / 2) ^ e
ε : ℝ
εpos : 0 < ε
pos : 0 < 4 + 12 * ‖c‖
e : ℕ
he : (1 / 2) ^ e < ε / (4 + 12 * ‖c‖)
y : E
hy : y ∈ ball 0 ((1 / 2) ^ (n e + 1))
⊢ ‖f (x + y) - f x - f' y‖ ≤ ε * ‖y‖

Tactic:
by_cases y_pos : y = 0

Goal state after:
case pos
𝕜 : 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')
Lf' : ∀ (e p : ℕ), n e ≤ p → ‖L e (n e) p - f'‖ ≤ 12 * ‖c‖ * (1 / 2) ^ e
ε : ℝ
εpos : 0 < ε
pos : 0 < 4 + 12 * ‖c‖
e : ℕ
he : (1 / 2) ^ e < ε / (4 + 12 * ‖c‖)
y : E
hy : y ∈ ball 0 ((1 / 2) ^ (n e + 1))
y_pos : y = 0
⊢ ‖f (x + y) - f x - f' y‖ ≤ ε * ‖y‖

case neg
𝕜 : 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')
Lf' : ∀ (e p : ℕ), n e ≤ p → ‖L e (n e) p - f'‖ ≤ 12 * ‖c‖ * (1 / 2) ^ e
ε : ℝ
εpos : 0 < ε
pos : 0 < 4 + 12 * ‖c‖
e : ℕ
he : (1 / 2) ^ e < ε / (4 + 12 * ‖c‖)
y : E
hy : y ∈ ball 0 ((1 / 2) ^ (n e + 1))
y_pos : ¬y = 0
⊢ ‖f (x + y) - f x - f' y‖ ≤ ε * ‖y‖
Module: Mathlib.Analysis.RCLike.Extend

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : RCLike 𝕜
F : Type u_2
inst✝⁵ : TopologicalSpace F
inst✝⁴ : AddCommGroup F
inst✝³ : Module 𝕜 F
inst✝² : ContinuousConstSMul 𝕜 F
inst✝¹ : Module ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
g : StrongDual ℝ F
x : F
⊢ re (g.extendRCLike x) = g x

Tactic:
by
  simp [extendRCLike_apply]

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

Goal state before:
pp: E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s : Set E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
hs : s ∈ 𝓝 0
⊢ Tendsto (gauge s) (𝓝 0) (𝓝[≥] 0)

Tactic:
refine nhdsGE_basis_Icc.tendsto_right_iff.2 fun ε hε ↦ ?_

Goal state after:
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s : Set E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
hs : s ∈ 𝓝 0
ε : ℝ
hε : 0 < ε
⊢ ∀ᶠ (x : E) in 𝓝 0, gauge s x ∈ Icc 0 ε
Module: Mathlib.Analysis.LocallyConvex.SeparatingDual

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝¹² : Field R
inst✝¹¹ : AddCommGroup V
inst✝¹⁰ : TopologicalSpace R
inst✝⁹ : TopologicalSpace V
inst✝⁸ : IsTopologicalRing R
inst✝⁷ : Module R V
inst✝⁶ : SeparatingDual R V
W : Type u_3
inst✝⁵ : AddCommGroup W
inst✝⁴ : TopologicalSpace W
inst✝³ : Module R W
inst✝² : Nontrivial W
inst✝¹ : ContinuousSMul R W
inst✝ : Nontrivial V
⊢ Nontrivial (V →L[R] W)

Tactic:
obtain ⟨v, hv⟩ := exists_ne (0 : V)

Goal state after:
R : Type u_1
V : Type u_2
inst✝¹² : Field R
inst✝¹¹ : AddCommGroup V
inst✝¹⁰ : TopologicalSpace R
inst✝⁹ : TopologicalSpace V
inst✝⁸ : IsTopologicalRing R
inst✝⁷ : Module R V
inst✝⁶ : SeparatingDual R V
W : Type u_3
inst✝⁵ : AddCommGroup W
inst✝⁴ : TopologicalSpace W
inst✝³ : Module R W
inst✝² : Nontrivial W
inst✝¹ : ContinuousSMul R W
inst✝ : Nontrivial V
v : V
hv : v ≠ 0
⊢ Nontrivial (V →L[R] W)
Module: Mathlib.Analysis.LocallyConvex.SeparatingDual

Goal state before:
pp: case inr.inr
R : Type u_1
V : Type u_2
inst✝⁶ : Field R
inst✝⁵ : AddCommGroup V
inst✝⁴ : TopologicalSpace R
inst✝³ : TopologicalSpace V
inst✝² : IsTopologicalRing R
inst✝¹ : Module R V
inst✝ : SeparatingDual R V
x y : V
hx : x ≠ 0
hy : y ≠ 0
u : StrongDual R V
ux : u x = 1
uy : u y = 0
v : StrongDual R V
vy : v y = 1
vx : v x = 0
⊢ ∃ f, f x = 1 ∧ f y ≠ 0

Tactic:
exact ⟨u + v, by simp [ux, vx], by simp [uy, vy]⟩

Goal state after:
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)
⊢ CompleteSpace F

Tactic:
refine Metric.complete_of_cauchySeq_tendsto fun f hf => ?_

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
⊢ ∃ a, Tendsto f atTop (𝓝 a)
Module: Mathlib.Analysis.LocallyConvex.Separation

Goal state before:
pp: case pos
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
s t : Set E
inst✝⁴ : RCLike 𝕜
inst✝³ : Module 𝕜 E
inst✝² : IsScalarTower ℝ 𝕜 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, (∀ a ∈ s, re (f a) ≤ u) ∧ ∀ b ∈ t, u ≤ re (f b)

pp: case neg
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
s t : Set E
inst✝⁴ : RCLike 𝕜
inst✝³ : Module 𝕜 E
inst✝² : IsScalarTower ℝ 𝕜 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, (∀ a ∈ s, re (f a) ≤ u) ∧ ∀ b ∈ t, u ≤ re (f b)

Tactic:
· have hsep :
        ∃ (f : StrongDual 𝕜 E) (u : ℝ),
          f ≠ 0 ∧ (∀ a ∈ s, re (f a) ≤ u) ∧ ∀ b ∈ t, u ≤ re (f b) :=
        geometric_hahn_banach_of_nonempty_interior hs ht hst hsint htne
    obtain ⟨f, u, -, hs', ht'⟩ := hsep
    exact ⟨f, u, hs', ht'⟩

Goal state after:
case neg
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
s t : Set E
inst✝⁴ : RCLike 𝕜
inst✝³ : Module 𝕜 E
inst✝² : IsScalarTower ℝ 𝕜 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, (∀ a ∈ s, re (f a) ≤ u) ∧ ∀ b ∈ t, u ≤ re (f b)
Module: Mathlib.Analysis.Normed.Operator.CompleteCodomain

Goal state before:
pp: 𝕜 : Type u_1
F : Type u_3
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
ι : Type u_4
inst✝⁴ : Finite ι
M : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace 𝕜 (M i)
inst✝¹ : ∀ (i : ι), SeparatingDual 𝕜 (M i)
inst✝ : CompleteSpace (ContinuousMultilinearMap 𝕜 M F)
m : (i : ι) → M i
hm : ∀ (i : ι), m i ≠ 0
⊢ CompleteSpace F

Tactic:
refine Metric.complete_of_cauchySeq_tendsto fun f hf => ?_

Goal state after:
𝕜 : Type u_1
F : Type u_3
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
ι : Type u_4
inst✝⁴ : Finite ι
M : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace 𝕜 (M i)
inst✝¹ : ∀ (i : ι), SeparatingDual 𝕜 (M i)
inst✝ : CompleteSpace (ContinuousMultilinearMap 𝕜 M F)
m : (i : ι) → M i
hm : ∀ (i : ι), m i ≠ 0
f : ℕ → F
hf : CauchySeq f
⊢ ∃ a, Tendsto f atTop (𝓝 a)
Module: Mathlib.Analysis.Calculus.FDeriv.Measurable

Goal state before:
pp: F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
ε : ℝ
hε : 0 < ε
x : ℝ
hx : DifferentiableWithinAt ℝ f (Ici x) x
this : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x_1 : ℝ) in 𝓝[≥] x, ‖f x_1 - f x - (x_1 - x) • derivWithin f (Ici x) x‖ ≤ c * ‖x_1 - x‖
m : ℝ
xm : m ∈ Ioi x
hm : Ico x m ⊆ {x_1 | (fun x_2 ↦ ‖f x_2 - f x - (x_2 - x) • derivWithin f (Ici x) x‖ ≤ ε / 2 * ‖x_2 - x‖) x_1}
⊢ m - x > 0

Tactic:
linarith [show x < m from xm]

Goal state after: