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
s : Set E
n : ℕ∞ω
f : E → F → G
g : E → F
t : Set F
hn : n ≠ ∞
x₀ : E
hf : ContDiffWithinAt 𝕜 (n + 1) (uncurry f) (insert x₀ s ×ˢ t) (x₀, g x₀)
hg : ContDiffWithinAt 𝕜 n g s x₀
hgt : t ∈ 𝓝[g '' s] g x₀
⊢ ∃ v ∈ 𝓝[insert x₀ s] x₀,
    v ⊆ insert x₀ s ∧ ∃ f', (∀ x ∈ v, HasFDerivWithinAt (f x) (f' x) t (g x)) ∧ ContDiffWithinAt 𝕜 n (fun x ↦ f' x) s x₀

Tactic:
by
  have hst : insert x₀ s ×ˢ t ∈ 𝓝[(fun x => (x, g x)) '' s] (x₀, g x₀) := by
    refine nhdsWithin_mono _ ?_ (nhdsWithin_prod self_mem_nhdsWithin hgt)
    simp_rw [image_subset_iff, mk_preimage_prod, preimage_id', subset_inter_iff, subset_insert,
      true_and, subset_preimage_image]
  obtain ⟨v, hv, hvs, f_an, f', hvf', hf'⟩ :=
    (contDiffWithinAt_succ_iff_hasFDerivWithinAt' hn).mp hf
  refine
    ⟨(fun z => (z, g z)) ⁻¹' v ∩ insert x₀ s, ?_, inter_subset_right, fun z =>
      (f' (z, g z)).comp (ContinuousLinearMap.inr 𝕜 E F), ?_, ?_⟩
  · refine inter_mem ?_ self_mem_nhdsWithin
    have := mem_of_mem_nhdsWithin (mem_insert _ _) hv
    refine mem_nhdsWithin_insert.mpr ⟨this, ?_⟩
    refine (continuousWithinAt_id.prodMk hg.continuousWithinAt).preimage_mem_nhdsWithin' ?_
    rw [← nhdsWithin_le_iff] at hst hv ⊢
    exact (hst.trans <| nhdsWithin_mono _ <| subset_insert _ _).trans hv
  · intro z hz
    have := hvf' (z, g z) hz.1
    refine this.comp _ (hasFDerivAt_prodMk_right _ _).hasFDerivWithinAt ?_
    exact mapsTo_iff_image_subset.mpr (image_prodMk_subset_prod_right hz.2)
  · exact (hf'.continuousLinearMap_comp <| (ContinuousLinearMap.compL 𝕜 F (E × F) G).flip
      (ContinuousLinearMap.inr 𝕜 E F)).comp_of_mem_nhdsWithin_image x₀
      (contDiffWithinAt_id.prodMk hg) hst

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

Goal state before:
pp: case e'_11
𝕜 : 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
n : ℕ∞ω
hn : n ≠ ∞
h'n : n + 1 ≠ ∞
u : Set E
hu : u ∈ 𝓝[insert x s] x
hf : n = ω → AnalyticOn 𝕜 f u
f' : E → E →L[𝕜] F
f'_eq_deriv : ∀ x ∈ u, HasFDerivWithinAt f (f' x) u x
Hf' : ContDiffWithinAt 𝕜 n f' u x
v : Set E
hv : v ∈ 𝓝[insert x u] x
p' : E → FormalMultilinearSeries 𝕜 E (E →L[𝕜] F)
Hp' : HasFTaylorSeriesUpToOn n f' p' v
p'_an : n = ω → ∀ (i : ℕ), AnalyticOn 𝕜 (fun x ↦ p' x i) v
⊢ (fun x ↦ ((p' x).unshift (f x)).shift) = p'

Tactic:
ext x k v y

Goal state after:
case e'_11
𝕜 : 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
n : ℕ∞ω
hn : n ≠ ∞
h'n : n + 1 ≠ ∞
u : Set E
hu : u ∈ 𝓝[insert x✝ s] x✝
hf : n = ω → AnalyticOn 𝕜 f u
f' : E → E →L[𝕜] F
f'_eq_deriv : ∀ x ∈ u, HasFDerivWithinAt f (f' x) u x
Hf' : ContDiffWithinAt 𝕜 n f' u x✝
v✝ : Set E
hv : v✝ ∈ 𝓝[insert x✝ u] x✝
p' : E → FormalMultilinearSeries 𝕜 E (E →L[𝕜] F)
Hp' : HasFTaylorSeriesUpToOn n f' p' v✝
p'_an : n = ω → ∀ (i : ℕ), AnalyticOn 𝕜 (fun x ↦ p' x i) v✝
x : E
k : ℕ
v : Fin k → E
y : E
⊢ ((((p' x).unshift (f x)).shift k) v) y = ((p' x k) v) y
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:
rw [iteratedDerivWithin_eq_iteratedFDerivWithin, iteratedFDerivWithin_succ_apply_left,
      iteratedFDerivWithin_eq_equiv_comp,
      LinearIsometryEquiv.comp_fderivWithin _ hxs.uniqueDiffWithinAt, derivWithin]
    change ((ContinuousMultilinearMap.mkPiRing 𝕜 (Fin n) ((fderivWithin 𝕜
      (iteratedDerivWithin n f s) s x : 𝕜 → F) 1) : (Fin n → 𝕜) → F) fun _ : Fin n => 1) =
      (fderivWithin 𝕜 (iteratedDerivWithin n f s) s x : 𝕜 → F) 1
    simp

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

Goal state before:
pp: case inl.succ.succ
𝕜 : 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✝ c : OrderedFinpartition n
m : Fin c.length
b a' : Fin (c.partSize m)
a✝¹ :
  (a'.castSucc < b.castSucc → cases 0 (succ ∘ c.emb m) a'.castSucc < cases 0 (succ ∘ c.emb m) b.castSucc) →
    a'.castSucc < b.succ → cases 0 (succ ∘ c.emb m) a'.castSucc < cases 0 (succ ∘ c.emb m) b.succ
a✝ : a'.succ < b.castSucc → cases 0 (succ ∘ c.emb m) a'.succ < cases 0 (succ ∘ c.emb m) b.castSucc
h' : a'.succ < b.succ
⊢ c.emb m a' < c.emb m b

Tactic:
exact c.emb_strictMono m (by simpa using 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
f : E → F
x : E
⊢ (∃ f', (∃ u ∈ 𝓝 x, ∀ x ∈ u, HasFDerivAt f (f' x) x) ∧ ContDiffAt 𝕜 0 f' x) ↔
    ∃ f', ∃ u ∈ 𝓝 x, ContinuousOn f' u ∧ ∀ x ∈ u, HasFDerivAt f (f' x) x

Tactic:
contDiffAt_zero,

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
x : E
⊢ (∃ f', (∃ u ∈ 𝓝 x, ∀ x ∈ u, HasFDerivAt f (f' x) x) ∧ ∃ u ∈ 𝓝 x, ContinuousOn f' u) ↔
    ∃ f', ∃ u ∈ 𝓝 x, ContinuousOn f' u ∧ ∀ x ∈ u, HasFDerivAt f (f' x) x
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✝ : CharZero 𝕂
x : 𝔸
⊢ (if h : Nonempty (Algebra ℚ 𝔸) then (expSeries ℚ 𝔸).sum x else 1) = (expSeries 𝕂 𝔸).sum x

Tactic:
dif_pos ⟨RestrictScalars.algebra ℚ 𝕂 𝔸⟩,

Goal state after:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁵ : Field 𝕂
inst✝⁴ : Ring 𝔸
inst✝³ : Algebra 𝕂 𝔸
inst✝² : TopologicalSpace 𝔸
inst✝¹ : IsTopologicalRing 𝔸
inst✝ : CharZero 𝕂
x : 𝔸
⊢ (expSeries ℚ 𝔸).sum x = (expSeries 𝕂 𝔸).sum x
Module: Mathlib.Analysis.Normed.Algebra.Exponential

Goal state before:
pp: 𝕂 : Type u_1
𝔸 : Type u_2
𝔹 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕂
inst✝⁴ : NormedRing 𝔸
inst✝³ : NormedRing 𝔹
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : CompleteSpace 𝔸
inst✝ : CharZero 𝕂
x : 𝔸
hx : x ∈ Metric.eball 0 (expSeries 𝕂 𝔸).radius
hnx : -x ∈ Metric.eball 0 (expSeries 𝕂 𝔸).radius
⊢ exp (-x + x) = 1

Tactic:
neg_add_cancel,

Goal state after:
𝕂 : Type u_1
𝔸 : Type u_2
𝔹 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕂
inst✝⁴ : NormedRing 𝔸
inst✝³ : NormedRing 𝔹
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : CompleteSpace 𝔸
inst✝ : CharZero 𝕂
x : 𝔸
hx : x ∈ Metric.eball 0 (expSeries 𝕂 𝔸).radius
hnx : -x ∈ Metric.eball 0 (expSeries 𝕂 𝔸).radius
⊢ exp 0 = 1
Module: Mathlib.Analysis.Normed.Algebra.Exponential

Goal state before:
pp: 𝕂 : Type u_1
𝔸 : Type u_2
𝔹 : Type u_3
inst✝⁸ : NontriviallyNormedField 𝕂
inst✝⁷ : NormedRing 𝔸
inst✝⁶ : NormedRing 𝔹
inst✝⁵ : NormedAlgebra 𝕂 𝔸
inst✝⁴ : CompleteSpace 𝔸
inst✝³ : Algebra 𝕂 𝔹
inst✝² : CharZero 𝕂
F : Type u_4
inst✝¹ : FunLike F 𝔸 𝔹
inst✝ : RingHomClass F 𝔸 𝔹
f : F
hf :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    ⇑f
x : 𝔸
hx : x ∈ Metric.eball 0 (expSeries 𝕂 𝔸).radius
⊢ f ((fun x ↦ ∑' (n : ℕ), (↑n !)⁻¹ • x ^ n) x) = (fun x ↦ ∑' (n : ℕ), (↑n !)⁻¹ • x ^ n) (f x)

Tactic:
refine ((expSeries_summable_of_mem_ball' _ hx).hasSum.map f hf).tsum_eq.symm.trans ?_

Goal state after:
𝕂 : Type u_1
𝔸 : Type u_2
𝔹 : Type u_3
inst✝⁸ : NontriviallyNormedField 𝕂
inst✝⁷ : NormedRing 𝔸
inst✝⁶ : NormedRing 𝔹
inst✝⁵ : NormedAlgebra 𝕂 𝔸
inst✝⁴ : CompleteSpace 𝔸
inst✝³ : Algebra 𝕂 𝔹
inst✝² : CharZero 𝕂
F : Type u_4
inst✝¹ : FunLike F 𝔸 𝔹
inst✝ : RingHomClass F 𝔸 𝔹
f : F
hf :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    ⇑f
x : 𝔸
hx : x ∈ Metric.eball 0 (expSeries 𝕂 𝔸).radius
⊢ ∑' (b : ℕ), (⇑f ∘ fun n ↦ (↑n !)⁻¹ • x ^ n) b = (fun x ↦ ∑' (n : ℕ), (↑n !)⁻¹ • x ^ n) (f x)
Module: Mathlib.Analysis.Normed.Algebra.Exponential

Goal state before:
pp: 𝔸 : Type u_1
inst✝⁴ : NormedRing 𝔸
inst✝³ : NormedAlgebra ℚ 𝔸
inst✝² : CompleteSpace 𝔸
inst✝¹ : StarRing 𝔸
inst✝ : ContinuousStar 𝔸
x : 𝔸
h : x ∈ skewAdjoint 𝔸
⊢ exp (-x + x) = 1 ∧ exp (x + -x) = 1

Tactic:
neg_add_cancel,

Goal state after:
𝔸 : Type u_1
inst✝⁴ : NormedRing 𝔸
inst✝³ : NormedAlgebra ℚ 𝔸
inst✝² : CompleteSpace 𝔸
inst✝¹ : StarRing 𝔸
inst✝ : ContinuousStar 𝔸
x : 𝔸
h : x ∈ skewAdjoint 𝔸
⊢ exp 0 = 1 ∧ exp (x + -x) = 1
Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas

Goal state before:
pp: case succ
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set 𝕜
h : UniqueDiffOn 𝕜 s
f : 𝕜 → F
c : 𝕜
hs : Set.MapsTo (fun x ↦ c * x) s s
n : ℕ
ih :
  ∀ {x : 𝕜},
    x ∈ s →
      ContDiffOn 𝕜 (↑n) f s → iteratedDerivWithin n (fun x ↦ f (c * x)) s x = c ^ n • iteratedDerivWithin n f s (c * x)
x : 𝕜
hx : x ∈ s
hf : ContDiffOn 𝕜 (↑(n + 1)) f s
hcx : c * x ∈ s
h₀ : Set.EqOn (iteratedDerivWithin n (fun x ↦ f (c * x)) s) (fun x ↦ c ^ n • iteratedDerivWithin n f s (c * x)) s
h₁ : DifferentiableWithinAt 𝕜 (iteratedDerivWithin n f s) s (c * x)
h₂ : DifferentiableWithinAt 𝕜 (fun x ↦ iteratedDerivWithin n f s (c * x)) s x
⊢ (c ^ n * c) • derivWithin (iteratedDerivWithin n f s) s (c * x) =
    c ^ (n + 1) • derivWithin (iteratedDerivWithin n f s) s (c * x)

Tactic:
pow_succ

Goal state after:
case succ
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set 𝕜
h : UniqueDiffOn 𝕜 s
f : 𝕜 → F
c : 𝕜
hs : Set.MapsTo (fun x ↦ c * x) s s
n : ℕ
ih :
  ∀ {x : 𝕜},
    x ∈ s →
      ContDiffOn 𝕜 (↑n) f s → iteratedDerivWithin n (fun x ↦ f (c * x)) s x = c ^ n • iteratedDerivWithin n f s (c * x)
x : 𝕜
hx : x ∈ s
hf : ContDiffOn 𝕜 (↑(n + 1)) f s
hcx : c * x ∈ s
h₀ : Set.EqOn (iteratedDerivWithin n (fun x ↦ f (c * x)) s) (fun x ↦ c ^ n • iteratedDerivWithin n f s (c * x)) s
h₁ : DifferentiableWithinAt 𝕜 (iteratedDerivWithin n f s) s (c * x)
h₂ : DifferentiableWithinAt 𝕜 (fun x ↦ iteratedDerivWithin n f s (c * x)) s x
⊢ (c ^ n * c) • derivWithin (iteratedDerivWithin n f s) s (c * x) =
    (c ^ n * c) • derivWithin (iteratedDerivWithin n f s) s (c * x)
Module: Mathlib.Analysis.SpecialFunctions.Exponential

Goal state before:
pp: 𝕂 : Type u_1
𝕊 : Type u_2
𝔸 : Type u_3
inst✝⁹ : NontriviallyNormedField 𝕂
inst✝⁸ : CharZero 𝕂
inst✝⁷ : NormedCommRing 𝕊
inst✝⁶ : NormedRing 𝔸
inst✝⁵ : NormedSpace 𝕂 𝕊
inst✝⁴ : NormedAlgebra 𝕂 𝔸
inst✝³ : Algebra 𝕊 𝔸
inst✝² : ContinuousSMul 𝕊 𝔸
inst✝¹ : IsScalarTower 𝕂 𝕊 𝔸
inst✝ : CompleteSpace 𝔸
x : 𝔸
t : 𝕊
htx : t • x ∈ Metric.eball 0 (expSeries 𝕂 𝔸).radius
this : Tendsto (fun h ↦ h • x) (𝓝 0) (𝓝 0)
⊢ (fun h ↦ exp (t • x) * (exp ((0 + h) • x) - exp (0 • x) - (ContinuousLinearMap.smulRight 1 x) h)) =ᶠ[𝓝 0] fun h ↦
    exp ((t + h) • x) - exp (t • x) - (exp (t • x) • ContinuousLinearMap.smulRight 1 x) h

Tactic:
have : ∀ᶠ h in 𝓝 (0 : 𝕊), h • x ∈ Metric.eball (0 : 𝔸) (expSeries 𝕂 𝔸).radius :=
    this.eventually (Metric.eball_mem_nhds _ htx.pos)

Goal state after:
𝕂 : Type u_1
𝕊 : Type u_2
𝔸 : Type u_3
inst✝⁹ : NontriviallyNormedField 𝕂
inst✝⁸ : CharZero 𝕂
inst✝⁷ : NormedCommRing 𝕊
inst✝⁶ : NormedRing 𝔸
inst✝⁵ : NormedSpace 𝕂 𝕊
inst✝⁴ : NormedAlgebra 𝕂 𝔸
inst✝³ : Algebra 𝕊 𝔸
inst✝² : ContinuousSMul 𝕊 𝔸
inst✝¹ : IsScalarTower 𝕂 𝕊 𝔸
inst✝ : CompleteSpace 𝔸
x : 𝔸
t : 𝕊
htx : t • x ∈ Metric.eball 0 (expSeries 𝕂 𝔸).radius
this✝ : Tendsto (fun h ↦ h • x) (𝓝 0) (𝓝 0)
this : ∀ᶠ (h : 𝕊) in 𝓝 0, h • x ∈ Metric.eball 0 (expSeries 𝕂 𝔸).radius
⊢ (fun h ↦ exp (t • x) * (exp ((0 + h) • x) - exp (0 • x) - (ContinuousLinearMap.smulRight 1 x) h)) =ᶠ[𝓝 0] fun h ↦
    exp ((t + h) • x) - exp (t • x) - (exp (t • x) • ContinuousLinearMap.smulRight 1 x) h
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
m : ℕ
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
c : OrderedFinpartition m
⊢ (q.compAlongOrderedFinpartition p (c.extend none)).curryLeft =
    ((compAlongOrderedFinpartitionL 𝕜 E F G c).flipMultilinear fun i ↦ p (c.partSize i)) ∘SL
      (q (c.length + 1)).curryLeft ∘SL (continuousMultilinearCurryFin1 𝕜 E F) (p 1)

Tactic:
ext e 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
m : ℕ
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
c : OrderedFinpartition m
e : E
v : Fin m → E
⊢ ((q.compAlongOrderedFinpartition p (c.extend none)).curryLeft e) v =
    ((((compAlongOrderedFinpartitionL 𝕜 E F G c).flipMultilinear fun i ↦ p (c.partSize i)) ∘SL
          (q (c.length + 1)).curryLeft ∘SL (continuousMultilinearCurryFin1 𝕜 E F) (p 1))
        e)
      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
m : ℕ
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
c : OrderedFinpartition m
i : Fin c.length
⊢ (q.compAlongOrderedFinpartition p (c.extend (some i))).curryLeft =
    ((compAlongOrderedFinpartitionL 𝕜 E F G c) (q c.length)).toContinuousLinearMap (fun i ↦ p (c.partSize i)) i ∘SL
      (p (c.partSize i + 1)).curryLeft

Tactic:
ext e 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
m : ℕ
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
c : OrderedFinpartition m
i : Fin c.length
e : E
v : Fin m → E
⊢ ((q.compAlongOrderedFinpartition p (c.extend (some i))).curryLeft e) v =
    ((((compAlongOrderedFinpartitionL 𝕜 E F G c) (q c.length)).toContinuousLinearMap (fun i ↦ p (c.partSize i)) i ∘SL
          (p (c.partSize i + 1)).curryLeft)
        e)
      v
Module: Mathlib.Topology.Order.ExtendFrom

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
f : α → β
a b : α
la lb : β
inst✝ : RegularSpace β
hf : ContinuousOn f (Ioo a b)
ha : Tendsto f (𝓝[>] a) (𝓝 la)
hb : Tendsto f (𝓝[<] b) (𝓝 lb)
⊢ ContinuousOn (extendFrom (Ioo a b) f) (Icc a b)

Tactic:
by
  by_cases! hab : a = b
  · simp [hab]
  apply continuousOn_extendFrom
  · rw [closure_Ioo hab]
  · intro x x_in
    rcases eq_endpoints_or_mem_Ioo_of_mem_Icc x_in with (rfl | rfl | h)
    · exact ⟨la, ha.mono_left <| nhdsWithin_mono _ Ioo_subset_Ioi_self⟩
    · exact ⟨lb, hb.mono_left <| nhdsWithin_mono _ Ioo_subset_Iio_self⟩
    · exact ⟨f x, hf x h⟩

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
n : ℕ
x : 𝕜
𝔸 : Type u_5
inst✝⁴ : NormedRing 𝔸
inst✝³ : NormedAlgebra 𝕜 𝔸
inst✝² : Module 𝔸 F
inst✝¹ : IsBoundedSMul 𝔸 F
inst✝ : IsScalarTower 𝕜 𝔸 F
f : 𝕜 → 𝔸
hf : ContDiffAt 𝕜 (↑n) f x
v : F
⊢ iteratedDeriv n (fun y ↦ f y • v) x = iteratedDeriv n f x • v

Tactic:
simp [iteratedDeriv, iteratedFDeriv_smul_const_apply hf]

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 : 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
c : OrderedFinpartition m
x✝ : c ∈ Finset.univ
B : (F [×c.length]→L[𝕜] G) →L[𝕜] (E [×c.partSize i]→L[𝕜] F) [×c.length]→L[𝕜] E [×m]→L[𝕜] G :=
  compAlongOrderedFinpartitionL 𝕜 E F G c
⊢ ContinuousOn (fun x i ↦ p x (c.partSize i)) s

Tactic:
apply continuousOn_pi.2 (fun i ↦ ?_)

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
c : OrderedFinpartition m
x✝ : c ∈ Finset.univ
B : (F [×c.length]→L[𝕜] G) →L[𝕜] (E [×c.partSize i]→L[𝕜] F) [×c.length]→L[𝕜] E [×m]→L[𝕜] G :=
  compAlongOrderedFinpartitionL 𝕜 E F G c
i : Fin c.length
⊢ ContinuousOn (fun y ↦ p y (c.partSize i)) s
Module: Mathlib.Geometry.Convex.Cone.Basic

Goal state before:
pp: case refine_1
𝕜 : Type u_1
M : Type u_4
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup M
inst✝ : Module 𝕜 M
s : Set M
hs : Convex 𝕜 s
x : M
⊢ (∃ c, 0 < c ∧ ∃ y ∈ s, c • y = x) → ∃ c, 0 < c ∧ c • x ∈ s

Tactic:
rintro ⟨c, hc, y, hy, rfl⟩

Goal state after:
case refine_1
𝕜 : Type u_1
M : Type u_4
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup M
inst✝ : Module 𝕜 M
s : Set M
hs : Convex 𝕜 s
c : 𝕜
hc : 0 < c
y : M
hy : y ∈ s
⊢ ∃ c_1, 0 < c_1 ∧ c_1 • c • y ∈ s
Module: Mathlib.Analysis.Convex.Gauge

Goal state before:
pp: E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
h : s ⊆ 0
⊢ gauge s = 0

Tactic:
obtain rfl | rfl := subset_singleton_iff_eq.1 h
  exacts [gauge_empty, gauge_zero']

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

Goal state before:
pp: case inr.mpr
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module ℝ E
α : Type u_3
inst✝⁶ : Field α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsStrictOrderedRing α
inst✝³ : MulActionWithZero α ℝ
inst✝² : IsStrictOrderedModule α ℝ
inst✝¹ : MulActionWithZero α E
inst✝ : IsScalarTower α ℝ (Set E)
s : Set E
a : α
ha : 0 ≤ a
x : E
ha' : 0 < a
r : ℝ
hr : r ∈ Ioi 0
hx : r⁻¹ • x ∈ s
⊢ a • r ∈ Ioi 0 ∧ (a • r)⁻¹ • a • x ∈ s

Tactic:
rw [mem_Ioi] at hr ⊢

Goal state after:
case inr.mpr
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module ℝ E
α : Type u_3
inst✝⁶ : Field α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsStrictOrderedRing α
inst✝³ : MulActionWithZero α ℝ
inst✝² : IsStrictOrderedModule α ℝ
inst✝¹ : MulActionWithZero α E
inst✝ : IsScalarTower α ℝ (Set E)
s : Set E
a : α
ha : 0 ≤ a
x : E
ha' : 0 < a
r : ℝ
hr : 0 < r
hx : r⁻¹ • x ∈ s
⊢ 0 < a • r ∧ (a • r)⁻¹ • a • x ∈ s
Module: Mathlib.Analysis.Convex.Gauge

Goal state before:
pp: case inr.mpr
E : Type u_2
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : Module ℝ E
α : Type u_3
inst✝⁸ : Field α
inst✝⁷ : LinearOrder α
inst✝⁶ : IsStrictOrderedRing α
inst✝⁵ : MulActionWithZero α ℝ
inst✝⁴ : IsStrictOrderedModule α ℝ
inst✝³ : MulActionWithZero α E
inst✝² : SMulCommClass α ℝ ℝ
inst✝¹ : IsScalarTower α ℝ ℝ
inst✝ : IsScalarTower α ℝ E
s : Set E
a : α
ha : 0 ≤ a
ha' : 0 < a
x : E
r : ℝ
hr : r ∈ Ioi 0
hx : r⁻¹ • x ∈ s
⊢ a⁻¹ • r ∈ Ioi 0 ∧ ∃ y ∈ s, a • y = (a⁻¹ • r)⁻¹ • x

Tactic:
rw [mem_Ioi] at hr ⊢

Goal state after:
case inr.mpr
E : Type u_2
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : Module ℝ E
α : Type u_3
inst✝⁸ : Field α
inst✝⁷ : LinearOrder α
inst✝⁶ : IsStrictOrderedRing α
inst✝⁵ : MulActionWithZero α ℝ
inst✝⁴ : IsStrictOrderedModule α ℝ
inst✝³ : MulActionWithZero α E
inst✝² : SMulCommClass α ℝ ℝ
inst✝¹ : IsScalarTower α ℝ ℝ
inst✝ : IsScalarTower α ℝ E
s : Set E
a : α
ha : 0 ≤ a
ha' : 0 < a
x : E
r : ℝ
hr : 0 < r
hx : r⁻¹ • x ∈ s
⊢ 0 < a⁻¹ • r ∧ ∃ y ∈ s, a • y = (a⁻¹ • r)⁻¹ • x
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))
y_pos : ¬y = 0
yzero : 0 < ‖y‖
y_lt : ‖y‖ < (1 / 2) ^ (n e + 1)
yone : ‖y‖ ≤ 1
k : ℕ
k_gt : n e < k
m : ℕ := k - 1
h'k : ‖y‖ ≤ (1 / 2) ^ (m + 1)
hk : (1 / 2) ^ (m + 1 + 1) < ‖y‖
m_ge : n e ≤ m
km : k = m + 1
J1 : ‖f (x + y) - f x - (L e (n e) m) (x + y - x)‖ ≤ (1 / 2) ^ e * (1 / 2) ^ m
J2 : ‖f (x + y) - f x - (L e (n e) m) y‖ ≤ 4 * (1 / 2) ^ e * ‖y‖
⊢ ‖L e (n e) m - f'‖ * ‖y‖ ≤ 12 * ‖c‖ * (1 / 2) ^ e * ‖y‖

Tactic:
gcongr; exact Lf' _ _ m_ge

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

Goal state before:
pp: F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
L : F
r ε x r' : ℝ
rr' : r' ∈ Ioc (r / 2) r
hr' : ∀ y ∈ Icc x (x + r'), ∀ z ∈ Icc x (x + r'), ‖f z - f y - (z - y) • L‖ ≤ ε * r
s : ℝ
s_gt : r / 2 < s
s_lt : s < r'
this : s ∈ Ioc (r / 2) r
x' : ℝ
hx' : x' ∈ Ioo x (x + r' - s)
⊢ Icc x' (x' + s) ⊆ Icc x (x + r')

Tactic:
apply Icc_subset_Icc hx'.1.le

Goal state after:
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
L : F
r ε x r' : ℝ
rr' : r' ∈ Ioc (r / 2) r
hr' : ∀ y ∈ Icc x (x + r'), ∀ z ∈ Icc x (x + r'), ‖f z - f y - (z - y) • L‖ ≤ ε * r
s : ℝ
s_gt : r / 2 < s
s_lt : s < r'
this : s ∈ Ioc (r / 2) r
x' : ℝ
hx' : x' ∈ Ioo x (x + r' - s)
⊢ x' + s ≤ x + r'
Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap

Goal state before:
pp: X : Type u_1
inst✝¹ : MeasurableSpace X
μ : Measure X
𝕜 : Type u_6
inst✝ : RCLike 𝕜
f : X → 𝕜
hf : Integrable f μ
⊢ ∫ (x : X), ↑(re (f x)) ∂μ + (∫ (x : X), ↑(im (f x)) ∂μ) * I = ∫ (x : X), f x ∂μ

Tactic:
rw [mul_comm, ← smul_eq_mul, ← integral_smul, ← integral_add]
  · congr
    ext1 x
    rw [smul_eq_mul, mul_comm, RCLike.re_add_im]
  · exact hf.re.ofReal
  · exact hf.im.ofReal.smul (𝕜 := 𝕜) (β := 𝕜) RCLike.I

Goal state after:
Module: Mathlib.MeasureTheory.Integral.DominatedConvergence

Goal state before:
pp: case pos
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst✝ : Countable ι
F : ι → α → E
hF_int : ∀ (i : ι), Integrable (F i) μ
hF_sum : Summable fun i ↦ ∫ (a : α), ‖F i a‖ ∂μ
hE : CompleteSpace E
this : ∀ (i : ι), ∫⁻ (a : α), ‖F i a‖ₑ ∂μ = ‖∫ (a : α), ‖F i a‖ ∂μ‖ₑ
⊢ ∑' (x : ι), ‖∫ (a : α), ‖F x a‖ ∂μ‖ₑ ≠ ∞

Tactic:
exact ENNReal.tsum_coe_ne_top_iff_summable.2 <| NNReal.summable_coe.1 hF_sum.abs

Goal state after: