mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Calculus.FDeriv.Analytic

Goal state before:
pp: case e'_5
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
h : HasFPowerSeriesWithinOnBall f p s x r
f' : E →L[𝕜] F
y : E
hy : ↑‖y‖₊ < r
h'y : x + y ∈ insert x s
hf' : HasFDerivWithinAt f f' (insert x s) (x + y)
hu : UniqueDiffOn 𝕜 (insert x s)
F' : Type v := UniformSpace.Completion F
a : F →L[𝕜] F' := UniformSpace.Completion.toComplL
b : (E →L[𝕜] F) →ₗᵢ[𝕜] E →L[𝕜] F' := UniformSpace.Completion.toComplₗᵢ.postcomp
this✝ : HasFPowerSeriesWithinOnBall (⇑a ∘ f) (a.compFormalMultilinearSeries p) s x r
Z : HasSum (fun n ↦ ((a.compFormalMultilinearSeries p).derivSeries n) fun x ↦ y) (a ∘SL f')
this : fderivWithin 𝕜 (⇑a ∘ f) (insert x s) (x + y) = a ∘SL f'
n : ℕ
v : E
⊢ ((⇑b ∘ fun n ↦ (p.derivSeries n) fun x ↦ y) n) v = (((a.compFormalMultilinearSeries p).derivSeries n) fun x ↦ y) v

Tactic:
simp only [FormalMultilinearSeries.derivSeries, sum_apply,
    ContinuousLinearMap.compFormalMultilinearSeries_apply,
    FormalMultilinearSeries.changeOriginSeries,
    ContinuousLinearMap.compContinuousMultilinearMap_coe, ContinuousLinearEquiv.coe_coe,
    LinearIsometryEquiv.coe_coe, Function.comp_apply, sum_apply, map_sum]

Goal state after:
case e'_5
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
h : HasFPowerSeriesWithinOnBall f p s x r
f' : E →L[𝕜] F
y : E
hy : ↑‖y‖₊ < r
h'y : x + y ∈ insert x s
hf' : HasFDerivWithinAt f f' (insert x s) (x + y)
hu : UniqueDiffOn 𝕜 (insert x s)
F' : Type v := UniformSpace.Completion F
a : F →L[𝕜] F' := UniformSpace.Completion.toComplL
b : (E →L[𝕜] F) →ₗᵢ[𝕜] E →L[𝕜] F' := UniformSpace.Completion.toComplₗᵢ.postcomp
this✝ : HasFPowerSeriesWithinOnBall (⇑a ∘ f) (a.compFormalMultilinearSeries p) s x r
Z : HasSum (fun n ↦ ((a.compFormalMultilinearSeries p).derivSeries n) fun x ↦ y) (a ∘SL f')
this : fderivWithin 𝕜 (⇑a ∘ f) (insert x s) (x + y) = a ∘SL f'
n : ℕ
v : E
⊢ ∑ i, (b ((continuousMultilinearCurryFin1 𝕜 E F) ((p.changeOriginSeriesTerm 1 n ↑i ⋯) fun x ↦ y))) v =
    ∑ i,
      ((continuousMultilinearCurryFin1 𝕜 E F')
          (((a.compFormalMultilinearSeries p).changeOriginSeriesTerm 1 n ↑i ⋯) fun x ↦ y))
        v
Module: Mathlib.Analysis.Calculus.FDeriv.Analytic

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
n : WithTop ℕ∞
h : AnalyticOn 𝕜 f s
hu : UniqueDiffOn 𝕜 s
⊢ HasFTaylorSeriesUpToOn n f (ftaylorSeriesWithin 𝕜 f s) s

Tactic:
by
  refine ⟨fun x _hx ↦ rfl, fun m _hm x hx ↦ ?_, fun m _hm x hx ↦ ?_⟩
  · have := (h.iteratedFDerivWithin hu m x hx).differentiableWithinAt.hasFDerivWithinAt
    rwa [insert_eq_of_mem hx] at this
  · exact (h.iteratedFDerivWithin hu m x hx).continuousWithinAt

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

Goal state before:
pp: 𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Algebra R 𝕜
q : R[X]
x : 𝕜
⊢ HasStrictDerivAt (fun x ↦ (aeval x) q) ((aeval x) (derivative q)) x

Tactic:
simpa only [aeval_def, eval₂_eq_eval_map, derivative_map] using
    (q.map (algebraMap R 𝕜)).hasStrictDerivAt x

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

Goal state before:
pp: 𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Algebra R 𝕜
q : R[X]
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun x ↦ (aeval x) q) s x = (aeval x) (derivative q)

Tactic:
by
  simpa only [aeval_def, eval₂_eq_eval_map, derivative_map] using
    (q.map (algebraMap R 𝕜)).derivWithin hxs

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
ι : Type u_5
𝔸' : Type u_7
inst✝³ : NormedCommRing 𝔸'
inst✝² : NormedAlgebra 𝕜 𝔸'
u : Finset ι
inst✝¹ : DecidableEq ι
inst✝ : Finite ι
x : ι → 𝔸'
⊢ HasStrictFDerivAt (fun x ↦ ∏ i ∈ u, x i) (∑ i ∈ u, (∏ j ∈ u.erase i, x j) •> proj i) x

Tactic:
simp only [Finset.sum_eq_multiset_sum, Finset.prod_eq_multiset_prod]
  exact hasStrictFDerivAt_multiset_prod

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

Goal state before:
pp: E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → G
C : ℝ
s : Set E
x y : E
f' : E → E →L[𝕜] G
φ : E →L[𝕜] G
hf : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
bound : ∀ x ∈ s, ‖f' x - φ‖ ≤ C
hs : Convex ℝ s
xs : x ∈ s
ys : y ∈ s
g : E → G := fun y ↦ f y - φ y
⊢ ‖f y - f x - φ (y - x)‖ ≤ C * ‖y - x‖

Tactic:
have hg : ∀ x ∈ s, HasFDerivWithinAt g (f' x - φ) s x := fun x xs =>
    (hf x xs).sub φ.hasFDerivWithinAt

Goal state after:
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → G
C : ℝ
s : Set E
x y : E
f' : E → E →L[𝕜] G
φ : E →L[𝕜] G
hf : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
bound : ∀ x ∈ s, ‖f' x - φ‖ ≤ C
hs : Convex ℝ s
xs : x ∈ s
ys : y ∈ s
g : E → G := fun y ↦ f y - φ y
hg : ∀ x ∈ s, HasFDerivWithinAt g (f' x - φ) s x
⊢ ‖f y - f x - φ (y - x)‖ ≤ C * ‖y - x‖
Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno

Goal state before:
pp: n : ℕ
c : OrderedFinpartition (n + 1)
hc : range (c.emb (c.index 0)) ≠ {0}
this : c.partSize (c.index 0) = Nat.card ↑(range (c.emb (c.index 0)))
h : c.index 0 = 0
⊢ {0} ⊂ range (c.emb (c.index 0))

Tactic:
apply ssubset_of_subset_of_ne ?_ hc.symm

Goal state after:
n : ℕ
c : OrderedFinpartition (n + 1)
hc : range (c.emb (c.index 0)) ≠ {0}
this : c.partSize (c.index 0) = Nat.card ↑(range (c.emb (c.index 0)))
h : c.index 0 = 0
⊢ {0} ⊆ range (c.emb (c.index 0))
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
n : ℕ∞ω
m : ℕ
x : E
h : ContDiffAt 𝕜 n f x
hmn : ↑m < n
⊢ iteratedFDeriv 𝕜 m f = iteratedFDerivWithin 𝕜 m f univ

Tactic:
exact iteratedFDerivWithin_univ.symm

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
n : ℕ∞ω
hf : ContDiff 𝕜 n f
⊢ HasFTaylorSeriesUpTo n f (_root_.ftaylorSeries 𝕜 f)

Tactic:
simp only [← contDiffOn_univ, ← hasFTaylorSeriesUpToOn_univ_iff, ← ftaylorSeriesWithin_univ]
    at hf ⊢

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
f : E → F
n : ℕ∞ω
hf : ContDiffOn 𝕜 n f univ
⊢ HasFTaylorSeriesUpToOn n f (ftaylorSeriesWithin 𝕜 f univ) univ
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
n : ℕ∞ω
hf : ContDiff 𝕜 n f
⊢ HasFTaylorSeriesUpTo n f (_root_.ftaylorSeries 𝕜 f)

Tactic:
by
  simp only [← contDiffOn_univ, ← hasFTaylorSeriesUpToOn_univ_iff, ← ftaylorSeriesWithin_univ]
    at hf ⊢
  exact ContDiffOn.ftaylorSeriesWithin hf uniqueDiffOn_univ

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

Goal state before:
pp: f : ℂ → ℂ
s : Set ℂ
f' x : ℂ
h : HasDerivWithinAt f f' s x
⊢ HasFDerivWithinAt f (f' • 1) s x

Tactic:
by
  simpa only [Complex.restrictScalars_toSpanSingleton] using h.hasFDerivWithinAt.restrictScalars ℝ

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

Goal state before:
pp: 𝕂 : Type u_1
𝕂' : Type u_2
𝔸 : Type u_3
inst✝⁶ : Field 𝕂
inst✝⁵ : Field 𝕂'
inst✝⁴ : Ring 𝔸
inst✝³ : Algebra 𝕂 𝔸
inst✝² : Algebra 𝕂' 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : IsTopologicalRing 𝔸
n : ℕ
x : 𝔸
⊢ (↑n !)⁻¹ • x ^ n = (↑n !)⁻¹ • x ^ n

Tactic:
inv_natCast_smul_eq 𝕂 𝕂'

Goal state after:
𝕂 : Type u_1
𝕂' : Type u_2
𝔸 : Type u_3
inst✝⁶ : Field 𝕂
inst✝⁵ : Field 𝕂'
inst✝⁴ : Ring 𝔸
inst✝³ : Algebra 𝕂 𝔸
inst✝² : Algebra 𝕂' 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : IsTopologicalRing 𝔸
n : ℕ
x : 𝔸
⊢ (↑n !)⁻¹ • x ^ n = (↑n !)⁻¹ • x ^ n
Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
n : ℕ
x : 𝕜
s : Set 𝕜
hx : x ∈ s
h : UniqueDiffOn 𝕜 s
⊢ iteratedDerivWithin n id s x = if n = 0 then x else if n = 1 then 1 else 0

Tactic:
obtain (_ | n) := n

Goal state after:
case zero
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
hx : x ∈ s
h : UniqueDiffOn 𝕜 s
⊢ iteratedDerivWithin 0 id s x = if 0 = 0 then x else if 0 = 1 then 1 else 0

case succ
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
hx : x ∈ s
h : UniqueDiffOn 𝕜 s
n : ℕ
⊢ iteratedDerivWithin (n + 1) id s x = if n + 1 = 0 then x else if n + 1 = 1 then 1 else 0
Module: Mathlib.Topology.Order.ExtendFrom

Goal state before:
pp: case neg.hf.inl
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
f : α → β
b : α
la : β
inst✝ : RegularSpace β
x : α
hf : ContinuousOn f (Ioo x b)
ha : Tendsto f (𝓝[>] x) (𝓝 la)
hab : x < b
x_in : x ∈ Ico x b
⊢ ∃ y, Tendsto f (𝓝[Ioo x b] x) (𝓝 y)

pp: case neg.hf.inr
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
f : α → β
a b : α
la : β
inst✝ : RegularSpace β
hf : ContinuousOn f (Ioo a b)
ha : Tendsto f (𝓝[>] a) (𝓝 la)
hab : a < b
x : α
x_in : x ∈ Ico a b
h : x ∈ Ioo a b
⊢ ∃ y, Tendsto f (𝓝[Ioo a b] x) (𝓝 y)

Tactic:
· use la
      simpa [hab]

Goal state after:
case neg.hf.inr
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
f : α → β
a b : α
la : β
inst✝ : RegularSpace β
hf : ContinuousOn f (Ioo a b)
ha : Tendsto f (𝓝[>] a) (𝓝 la)
hab : a < b
x : α
x_in : x ∈ Ico a b
h : x ∈ Ioo a b
⊢ ∃ y, Tendsto f (𝓝[Ioo a b] x) (𝓝 y)
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
ι : Type u_7
n : ℕ
x : 𝕜
f : ι → 𝕜 → F
I : Finset ι
s : Set 𝕜
hx : x ∈ s
hs : UniqueDiffOn 𝕜 s
hf : ∀ i ∈ I, ContDiffWithinAt 𝕜 (↑n) (f i) s x
⊢ iteratedDerivWithin n (∑ i ∈ I, f i) s x = ∑ i ∈ I, iteratedDerivWithin n (f i) s x

Tactic:
induction I using Finset.induction_on with

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
ι : Type u_7
n : ℕ
x : 𝕜
f : ι → 𝕜 → F
I : Finset ι
s : Set 𝕜
hx : x ∈ s
hs : UniqueDiffOn 𝕜 s
hf : ∀ i ∈ I, ContDiffWithinAt 𝕜 (↑n) (f i) s x
⊢ iteratedDerivWithin n (∑ i ∈ I, f i) s x = ∑ i ∈ I, iteratedDerivWithin n (f i) s x

Tactic:
by
  classical
  induction I using Finset.induction_on with
  | empty => simp
  | insert i t hi IH =>
    rw [forall_mem_insert] at hf
    simp only [sum_insert hi, sum_fn] at IH ⊢
    rw [iteratedDerivWithin_add hx hs hf.1 (.sum hf.2), IH hf.2]

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

Goal state before:
pp: 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
z : ℝ
hz : z ∈ Ioc a b
⊢ DifferentiableWithinAt ℝ f (Ioc a b) z

Tactic:
refine DifferentiableWithinAt.mono (t := Ioi a) ?_ Ioc_subset_Ioi_self
        have : derivWithin f (Ioi a) z ≠ 0 := ne_of_gt <| by
          simp_all only [and_imp, mem_Ioc, max_lt_iff]
        exact differentiableWithinAt_of_derivWithin_ne_zero this

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

Goal state before:
pp: case refine_2
α : 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 : α), g1 x ∂μ ≤ 0 + ε / 2

Tactic:
convert! g1_int

Goal state after:
case e'_4
α : 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
⊢ 0 = ∫⁻ (x : α), s.indicator (fun _x ↦ ∞) x ∂μ
Module: Mathlib.Geometry.Convex.Cone.Basic

Goal state before:
pp: case inl
R : Type u_7
M : Type u_8
inst✝⁵ : Ring R
inst✝⁴ : LinearOrder R
inst✝³ : AddLeftStrictMono R
inst✝² : AddCommGroup M
inst✝¹ : Nontrivial M
inst✝ : Module R M
C : ConvexCone R M
h : Submodule.span R ↑C = ⊤
x : M
hne : (↑C).Nonempty
r : R
y : M
hy : y ∈ ↑C
z : M
hz : z ∈ ↑C
hr : r < 0
⊢ r • y - r • z = r • (y - z)

Tactic:
smul_sub

Goal state after:
case inl
R : Type u_7
M : Type u_8
inst✝⁵ : Ring R
inst✝⁴ : LinearOrder R
inst✝³ : AddLeftStrictMono R
inst✝² : AddCommGroup M
inst✝¹ : Nontrivial M
inst✝ : Module R M
C : ConvexCone R M
h : Submodule.span R ↑C = ⊤
x : M
hne : (↑C).Nonempty
r : R
y : M
hy : y ∈ ↑C
z : M
hz : z ∈ ↑C
hr : r < 0
⊢ r • y - r • z = r • y - r • z
Module: Mathlib.Geometry.Convex.Cone.Basic

Goal state before:
pp: case smul_mem'
𝕜 : Type u_1
R : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup M
inst✝ : Module 𝕜 M
s : Set M
hs : Convex 𝕜 s
⊢ ∀ ⦃c : 𝕜⦄, 0 < c → ∀ ⦃x : M⦄, (∃ i, ∃ (_ : 0 < i), ∃ y ∈ s, i • y = x) → ∃ i, ∃ (_ : 0 < i), ∃ y ∈ s, i • y = c • x

pp: case add_mem'
𝕜 : Type u_1
R : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup M
inst✝ : Module 𝕜 M
s : Set M
hs : Convex 𝕜 s
⊢ ∀ ⦃x : M⦄,
    (∃ i, ∃ (_ : 0 < i), ∃ y ∈ s, i • y = x) →
      ∀ ⦃y : M⦄, (∃ i, ∃ (_ : 0 < i), ∃ y_1 ∈ s, i • y_1 = y) → ∃ i, ∃ (_ : 0 < i), ∃ y_1 ∈ s, i • y_1 = x + y

Tactic:
· rintro c c_pos _ ⟨c', c'_pos, x, hx, rfl⟩
    exact ⟨c * c', mul_pos c_pos c'_pos, x, hx, (smul_smul _ _ _).symm⟩

Goal state after:
case add_mem'
𝕜 : Type u_1
R : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup M
inst✝ : Module 𝕜 M
s : Set M
hs : Convex 𝕜 s
⊢ ∀ ⦃x : M⦄,
    (∃ i, ∃ (_ : 0 < i), ∃ y ∈ s, i • y = x) →
      ∀ ⦃y : M⦄, (∃ i, ∃ (_ : 0 < i), ∃ y_1 ∈ s, i • y_1 = y) → ∃ i, ∃ (_ : 0 < i), ∃ y_1 ∈ s, i • y_1 = x + y
Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv

Goal state before:
pp: case refine_2
y : ℝ
n : ℕ
hy₁ : -1 < y
hy₂ : y < 1
this : ∑ i ∈ Finset.range n, (2 * ↑i + 1) * y ^ (2 * i) / (2 * ↑i + 1) = ∑ i ∈ Finset.range n, (y ^ 2) ^ i
⊢ 1 / 2 * ((1 * (1 - y) - (1 + y) * -1) / (1 - y) ^ 2 / (HAdd.hAdd 1 / HSub.hSub 1) y) -
      ∑ i ∈ Finset.range n, ↑(2 * i + 1) * y ^ (2 * i + 1 - 1) / (2 * ↑i + 1) =
    (y ^ 2) ^ n / (1 - y ^ 2)

Tactic:
have hy₃ : y ^ 2 ≠ 1 := by simp [hy₁.ne', hy₂.ne]

Goal state after:
case refine_2
y : ℝ
n : ℕ
hy₁ : -1 < y
hy₂ : y < 1
this : ∑ i ∈ Finset.range n, (2 * ↑i + 1) * y ^ (2 * i) / (2 * ↑i + 1) = ∑ i ∈ Finset.range n, (y ^ 2) ^ i
hy₃ : y ^ 2 ≠ 1
⊢ 1 / 2 * ((1 * (1 - y) - (1 + y) * -1) / (1 - y) ^ 2 / (HAdd.hAdd 1 / HSub.hSub 1) y) -
      ∑ i ∈ Finset.range n, ↑(2 * i + 1) * y ^ (2 * i + 1 - 1) / (2 * ↑i + 1) =
    (y ^ 2) ^ n / (1 - y ^ 2)
Module: Mathlib.Analysis.Convex.Cone.Extension

Goal state before:
pp: E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : PointedCone ℝ E
f : E →ₗ.[ℝ] ℝ
nonneg : ∀ (x : ↥f.domain), ↑x ∈ s → 0 ≤ ↑f x
dense : ∀ (y : E), ∃ x, ↑x + y ∈ s
hdom : f.domain ≠ ⊤
y : E
hy : y ∉ f.domain
⊢ ∃ g, f < g ∧ ∀ (x : ↥g.domain), ↑x ∈ s → 0 ≤ ↑g x

Tactic:
obtain ⟨c, le_c, c_le⟩ :
      ∃ c, (∀ x : f.domain, -(x : E) - y ∈ s → f x ≤ c) ∧
        ∀ x : f.domain, (x : E) + y ∈ s → c ≤ f x := by
    set Sp := f '' { x : f.domain | (x : E) + y ∈ s }
    set Sn := f '' { x : f.domain | -(x : E) - y ∈ s }
    suffices (upperBounds Sn ∩ lowerBounds Sp).Nonempty by
      simpa only [Sp, Sn, Set.Nonempty, upperBounds, lowerBounds, forall_mem_image] using! this
    refine exists_between_of_forall_le (Nonempty.image f ?_) (Nonempty.image f (dense y)) ?_
    · rcases dense (-y) with ⟨x, hx⟩
      rw [← neg_neg x, NegMemClass.coe_neg, ← sub_eq_add_neg] at hx
      exact ⟨_, hx⟩
    rintro a ⟨xn, hxn, rfl⟩ b ⟨xp, hxp, rfl⟩
    have := s.add_mem hxp hxn
    rw [add_assoc, add_sub_cancel, ← sub_eq_add_neg, ← AddSubgroupClass.coe_sub] at this
    replace := nonneg _ this
    rwa [f.map_sub, sub_nonneg] at this

Goal state after:
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : PointedCone ℝ E
f : E →ₗ.[ℝ] ℝ
nonneg : ∀ (x : ↥f.domain), ↑x ∈ s → 0 ≤ ↑f x
dense : ∀ (y : E), ∃ x, ↑x + y ∈ s
hdom : f.domain ≠ ⊤
y : E
hy : y ∉ f.domain
c : ℝ
le_c : ∀ (x : ↥f.domain), -↑x - y ∈ s → ↑f x ≤ c
c_le : ∀ (x : ↥f.domain), ↑x + y ∈ s → c ≤ ↑f x
⊢ ∃ g, f < g ∧ ∀ (x : ↥g.domain), ↑x ∈ s → 0 ≤ ↑g x
Module: Mathlib.Analysis.Convex.Gauge

Goal state before:
pp: E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
x : E
a : ℝ
hs₀ : StarConvex ℝ 0 s
hs₂ : Absorbs ℝ s {x}
hx : x ∉ a • s
⊢ a ≤ gauge s x

Tactic:
rw [starConvex_zero_iff] at hs₀

Goal state after:
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
x : E
a : ℝ
hs₀ : ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃a : ℝ⦄, 0 ≤ a → a ≤ 1 → a • x ∈ s
hs₂ : Absorbs ℝ s {x}
hx : x ∉ a • s
⊢ a ≤ gauge s x
Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : μ.WeaklyRegular
f : α → ℝ≥0
fint : Integrable (fun x ↦ ↑(f x)) μ
ε : ℝ≥0
εpos : 0 < ↑ε
⊢ ∃ g,
    (∀ (x : α), g x ≤ f x) ∧
      UpperSemicontinuous g ∧ Integrable (fun x ↦ ↑(g x)) μ ∧ ∫ (x : α), ↑(f x) ∂μ - ↑ε ≤ ∫ (x : α), ↑(g x) ∂μ

Tactic:
NNReal.coe_pos,

Goal state after:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : μ.WeaklyRegular
f : α → ℝ≥0
fint : Integrable (fun x ↦ ↑(f x)) μ
ε : ℝ≥0
εpos : 0 < ε
⊢ ∃ g,
    (∀ (x : α), g x ≤ f x) ∧
      UpperSemicontinuous g ∧ Integrable (fun x ↦ ↑(g x)) μ ∧ ∫ (x : α), ↑(f x) ∂μ - ↑ε ≤ ∫ (x : α), ↑(g x) ∂μ
Module: Mathlib.Analysis.LocallyConvex.Separation

Goal state before:
pp: case inr.inr
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
hs₂ : IsOpen s
ht : Convex ℝ t
disj : Disjoint s t
a₀ : E
ha₀ : a₀ ∈ s
b₀ : E
hb₀ : b₀ ∈ t
x₀ : E := b₀ - a₀
C : Set E := x₀ +ᵥ s - t
this✝¹ : 0 ∈ C
this✝ : Convex ℝ C
this : x₀ ∉ C
f : StrongDual ℝ E
hf₁ : f x₀ = 1
hf₂ : ∀ x ∈ C, f x < 1
forall_le : ∀ a ∈ s, ∀ b ∈ t, f a ≤ f b
⊢ ∃ f u, (∀ a ∈ s, f a < u) ∧ ∀ b ∈ t, u ≤ f b

Tactic:
refine ⟨f, sInf (f '' t), image_subset_iff.1 (?_ : f '' s ⊆ Iio (sInf (f '' t))), fun b hb => ?_⟩

Goal state after:
case inr.inr.refine_1
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
hs₂ : IsOpen s
ht : Convex ℝ t
disj : Disjoint s t
a₀ : E
ha₀ : a₀ ∈ s
b₀ : E
hb₀ : b₀ ∈ t
x₀ : E := b₀ - a₀
C : Set E := x₀ +ᵥ s - t
this✝¹ : 0 ∈ C
this✝ : Convex ℝ C
this : x₀ ∉ C
f : StrongDual ℝ E
hf₁ : f x₀ = 1
hf₂ : ∀ x ∈ C, f x < 1
forall_le : ∀ a ∈ s, ∀ b ∈ t, f a ≤ f b
⊢ ⇑f '' s ⊆ Iio (sInf (⇑f '' t))

case inr.inr.refine_2
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
hs₂ : IsOpen s
ht : Convex ℝ t
disj : Disjoint s t
a₀ : E
ha₀ : a₀ ∈ s
b₀ : E
hb₀ : b₀ ∈ t
x₀ : E := b₀ - a₀
C : Set E := x₀ +ᵥ s - t
this✝¹ : 0 ∈ C
this✝ : Convex ℝ C
this : x₀ ∉ C
f : StrongDual ℝ E
hf₁ : f x₀ = 1
hf₂ : ∀ x ∈ C, f x < 1
forall_le : ∀ a ∈ s, ∀ b ∈ t, f a ≤ f b
b : E
hb : b ∈ t
⊢ sInf (⇑f '' t) ≤ f b
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₂ : IsClosed s✝
ht₁ : Convex ℝ t✝
ht₂ : IsCompact t✝
disj : Disjoint s✝ t✝
f : StrongDual ℝ E
s t : ℝ
hs : ∀ a ∈ t✝, f a < s
st : s < t
ht : ∀ b ∈ s✝, t < f b
⊢ ∀ a ∈ s✝, (-f) a < -t

Tactic:
by simpa using ht

Goal state after:
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
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul R V
x y : V
hx : x ≠ 0
hy : y ≠ 0
G : StrongDual R V
Gx : G x = 1
Gy : G y ≠ 0
z : V
⊢ z + G z • (y - x) + (1 * G z) • (x - y) = z

Tactic:
simp only [smul_sub, one_mul]

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
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul R V
x y : V
hx : x ≠ 0
hy : y ≠ 0
G : StrongDual R V
Gx : G x = 1
Gy : G y ≠ 0
z : V
⊢ z + (G z • y - G z • x) + (G z • x - G z • y) = z
Module: Mathlib.Analysis.LocallyConvex.Separation

Goal state before:
pp: 𝕜 : 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
inst✝ : LocallyConvexSpace ℝ E
hs₁ : Convex ℝ s✝
hs₂ : IsClosed s✝
ht₁ : Convex ℝ t✝
ht₂ : IsCompact t✝
disj : Disjoint s✝ t✝
f : StrongDual 𝕜 E
s t : ℝ
hs : ∀ a ∈ t✝, re (f a) < s
st : s < t
ht : ∀ b ∈ s✝, t < re (f b)
⊢ ∀ a ∈ s✝, re ((-f) a) < -t

Tactic:
by simpa using ht

Goal state after: