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
⊢ ∃ u ∈ 𝓝[insert x s] x, ∃ p, HasFTaylorSeriesUpToOn (↑m) (g ∘ f) p u

Tactic:
rcases hg m hm with ⟨v, hv, q, hq⟩

Goal state after:
𝕜 : 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
⊢ ∃ u ∈ 𝓝[insert x s] x, ∃ p, HasFTaylorSeriesUpToOn (↑m) (g ∘ f) p u
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
f : E → F
g : F → G
x : E
n : ℕ∞ω
hg : ContDiffAt 𝕜 n g (f x)
hf : ContDiffAt 𝕜 n f x
i : ℕ
hi : ↑i ≤ n
⊢ iteratedFDeriv 𝕜 i (g ∘ f) x = (ftaylorSeries 𝕜 g (f x)).taylorComp (ftaylorSeries 𝕜 f x) i

Tactic:
simp only [← iteratedFDerivWithin_univ, ← ftaylorSeriesWithin_univ]
  exact iteratedFDerivWithin_comp hg.contDiffWithinAt hf.contDiffWithinAt
    uniqueDiffOn_univ uniqueDiffOn_univ (mem_univ _) (mapsTo_univ _ _) hi

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

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
x : E
n✝ : ℕ∞ω
s : Set E
f : E → F
g : E → G
n : ℕ∞
hf : ContDiffWithinAt 𝕜 (↑n) f s x
hg : ContDiffWithinAt 𝕜 (↑n) g 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
⊢ ∃ u ∈ 𝓝[insert x s] x, ∃ p, HasFTaylorSeriesUpToOn (↑m) (fun x ↦ (f x, g x)) p u

Tactic:
rcases hg m hm with ⟨v, hv, q, hq⟩

Goal state after:
𝕜 : 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
x : E
n✝ : ℕ∞ω
s : Set E
f : E → F
g : E → G
n : ℕ∞
hf : ContDiffWithinAt 𝕜 (↑n) f s x
hg : ContDiffWithinAt 𝕜 (↑n) g 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 E
hv : v ∈ 𝓝[insert x s] x
q : E → FormalMultilinearSeries 𝕜 E G
hq : HasFTaylorSeriesUpToOn (↑m) g q v
⊢ ∃ u ∈ 𝓝[insert x s] x, ∃ p, HasFTaylorSeriesUpToOn (↑m) (fun x ↦ (f x, g x)) p u
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
n : ℕ∞ω
hn : ω ≠ ∞
⊢ ContDiffWithinAt 𝕜 ω f s x ↔
    ∃ u ∈ 𝓝[insert x s] x, ∃ p, HasFTaylorSeriesUpToOn ω f p u ∧ (ω = ω → ∀ (i : ℕ), AnalyticOn 𝕜 (fun x ↦ p x i) u)

Tactic:
simp [ContDiffWithinAt]

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
s : Set E
f : E → F
x : E
n : ℕ∞ω
⊢ ContDiffWithinAt 𝕜 ω f (insert x s) x ↔ ContDiffWithinAt 𝕜 ω f s x

Tactic:
simp [ContDiffWithinAt]

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
s : Set E
f : E → F
x : E
n : ℕ∞ω
y : E
⊢ ContDiffWithinAt 𝕜 n f (insert y s) x ↔ ContDiffWithinAt 𝕜 n f s x

Tactic:
rcases eq_or_ne x y with (rfl | hx)

Goal state after:
case inl
𝕜 : 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 : ℕ∞ω
⊢ ContDiffWithinAt 𝕜 n f (insert x s) x ↔ ContDiffWithinAt 𝕜 n f s x

case inr
𝕜 : 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 : ℕ∞ω
y : E
hx : x ≠ y
⊢ ContDiffWithinAt 𝕜 n f (insert y s) x ↔ ContDiffWithinAt 𝕜 n f s x
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
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
⊢ v ∈ 𝓝[u] x

Tactic:
exact nhdsWithin_mono _ (subset_insert x u) hv

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

Goal state before:
pp: case pos
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
c : F
h : ∃ᶠ (y : 𝕜) in 𝓝[s \ {x}] x, f y = c
hf : DifferentiableWithinAt 𝕜 f s x
⊢ derivWithin f s x = 0

Tactic:
contrapose! h
    exact hf.hasDerivWithinAt.eventually_ne h

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

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

Tactic:
rw [← h] at hc
    have : {0} ⊂ range (c.emb (c.index 0)) := by
      apply ssubset_of_subset_of_ne ?_ hc.symm
      simpa only [singleton_subset_iff, mem_range] using ⟨0, emb_zero c⟩
    simpa using Set.Finite.card_lt_card (finite_range _) this

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

Goal state before:
pp: case refine_2
𝕜 : 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
i : Fin c.length
⊢ StrictMono
    (cases (motive := fun x ↦ Fin (cons 1 c.partSize x) → Fin (n + 1)) (fun x ↦ 0) (fun m ↦ succ ∘ c.emb m) i.succ)

Tactic:
exact strictMono_succ.comp (c.emb_strictMono i)

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
s : Set E
f : E → F
x : E
n : ℕ∞ω
h : ContDiffWithinAt 𝕜 n f s x
hn : n ≠ ∞
⊢ ∀ᶠ (y : E) in 𝓝[insert x s] x, ContDiffWithinAt 𝕜 n f s y

Tactic:
rcases h.contDiffOn le_rfl (by simp [hn]) with ⟨u, hu, _, hd⟩
  have : ∀ᶠ y : E in 𝓝[insert x s] x, u ∈ 𝓝[insert x s] y ∧ y ∈ u :=
    (eventually_eventually_nhdsWithin.2 hu).and hu
  refine this.mono fun y hy => (hd y hy.2).mono_of_mem_nhdsWithin ?_
  exact nhdsWithin_mono y (subset_insert _ _) hy.1

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
s : Set E
f : E → F
n : ℕ∞ω
hs : UniqueDiffOn 𝕜 s
H : ContDiffOn 𝕜 (n + 1) f s
x : E
hx : x ∈ s
m : ℕ
hm : ↑m ≤ n
u : Set E
hu : u ∈ 𝓝[insert x s] x
f' : E → E →L[𝕜] F
hff' : ∀ x ∈ u, HasFDerivWithinAt f (f' x) u x
hf' : ContDiffWithinAt 𝕜 (↑m) f' u x
o : Set E
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
xo : x ∈ o
ho : o ∩ insert x s ⊆ u
⊢ ContDiffWithinAt 𝕜 (↑m) (fun y ↦ fderivWithin 𝕜 f s y) s x

Tactic:
rw [inter_comm, insert_eq_of_mem hx] at ho

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
s : Set E
f : E → F
n : ℕ∞ω
hs : UniqueDiffOn 𝕜 s
H : ContDiffOn 𝕜 (n + 1) f s
x : E
hx : x ∈ s
m : ℕ
hm : ↑m ≤ n
u : Set E
hu : u ∈ 𝓝[insert x s] x
f' : E → E →L[𝕜] F
hff' : ∀ x ∈ u, HasFDerivWithinAt f (f' x) u x
hf' : ContDiffWithinAt 𝕜 (↑m) f' u x
o : Set E
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
xo : x ∈ o
ho : s ∩ o ⊆ u
⊢ ContDiffWithinAt 𝕜 (↑m) (fun y ↦ fderivWithin 𝕜 f s y) s x
Module: Mathlib.Analysis.Calculus.ContDiff.Defs

Goal state before:
pp: case mpr
𝕜 : 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✝ : ℕ∞ω
n : ℕ∞
⊢ ContDiff 𝕜 (↑n) f → ContDiffOn 𝕜 (↑n) f univ

Tactic:
rintro ⟨p, hp⟩ x _ m hm
      exact ⟨univ, Filter.univ_sets _, p,
        (hp.hasFTaylorSeriesUpToOn univ).of_le (mod_cast hm)⟩

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

Goal state before:
pp: 𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕂
inst✝³ : NormedRing 𝔸
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : CompleteSpace 𝔸
inst✝ : CharZero 𝕂
x y : 𝔸
hxy : Commute x y
hx : x ∈ Metric.eball 0 (expSeries 𝕂 𝔸).radius
hy : y ∈ Metric.eball 0 (expSeries 𝕂 𝔸).radius
⊢ ∑' (n : ℕ), (↑n !)⁻¹ • (x + y) ^ n =
    ∑' (n : ℕ), ∑ kl ∈ Finset.antidiagonal n, (↑kl.1!)⁻¹ • x ^ kl.1 * (↑kl.2!)⁻¹ • y ^ kl.2

Tactic:
conv_lhs =>
    congr
    ext
    rw [hxy.add_pow' _, Finset.smul_sum]

Goal state after:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕂
inst✝³ : NormedRing 𝔸
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : CompleteSpace 𝔸
inst✝ : CharZero 𝕂
x y : 𝔸
hxy : Commute x y
hx : x ∈ Metric.eball 0 (expSeries 𝕂 𝔸).radius
hy : y ∈ Metric.eball 0 (expSeries 𝕂 𝔸).radius
⊢ ∑' (x_1 : ℕ), ∑ x_2 ∈ Finset.antidiagonal x_1, (↑x_1 !)⁻¹ • x_1.choose x_2.1 • (x ^ x_2.1 * y ^ x_2.2) =
    ∑' (n : ℕ), ∑ kl ∈ Finset.antidiagonal n, (↑kl.1!)⁻¹ • x ^ kl.1 * (↑kl.2!)⁻¹ • y ^ kl.2
Module: Mathlib.Analysis.Normed.Algebra.Exponential

Goal state before:
pp: case inr
𝔸 : Type u_1
inst✝² : NormedDivisionRing 𝔸
inst✝¹ : NormedAlgebra ℚ 𝔸
inst✝ : CompleteSpace 𝔸
x : 𝔸
n : ℕ
⊢ exp (-↑n • x) = exp x ^ (-↑n)

Tactic:
zpow_neg,

Goal state after:
case inr
𝔸 : Type u_1
inst✝² : NormedDivisionRing 𝔸
inst✝¹ : NormedAlgebra ℚ 𝔸
inst✝ : CompleteSpace 𝔸
x : 𝔸
n : ℕ
⊢ exp (-↑n • x) = (exp x ^ ↑n)⁻¹
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 𝕜
𝕝 : Type u_4
inst✝³ : DivisionSemiring 𝕝
inst✝² : Module 𝕝 F
inst✝¹ : SMulCommClass 𝕜 𝕝 F
inst✝ : ContinuousConstSMul 𝕝 F
c : 𝕝
n : ℕ
IH : ∀ {x : 𝕜} (f : 𝕜 → F), iteratedDerivWithin n (c • f) s x = c • iteratedDerivWithin n f s x
x : 𝕜
f : 𝕜 → F
⊢ iteratedDerivWithin (n + 1) (c • f) s x = c • iteratedDerivWithin (n + 1) f s x

Tactic:
simp_rw [iteratedDerivWithin_succ, funext (@IH · f), ← Pi.smul_def,
      derivWithin_const_smul_field]

Goal state after:
Module: Mathlib.Topology.MetricSpace.CauSeqFilter

Goal state before:
pp: β : Type v
inst✝ : NormedField β
f : ℕ → β
hf : CauchySeq f
⊢ IsCauSeq norm f

Tactic:
by
  obtain ⟨hf1, hf2⟩ := cauchy_iff.1 hf
  intro ε hε
  rcases hf2 { x | dist x.1 x.2 < ε } (dist_mem_uniformity hε) with ⟨t, ⟨ht, htsub⟩⟩
  simp only [mem_map, mem_atTop_sets, mem_preimage] at ht; obtain ⟨N, hN⟩ := ht
  exists N
  intro j hj
  rw [← dist_eq_norm]
  apply @htsub (f j, f N)
  apply Set.mk_mem_prod <;> solve_by_elim [le_refl]

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
hq : ∀ (n : ℕ), AnalyticOn 𝕜 (fun x ↦ q x n) t
hp : ∀ (n : ℕ), AnalyticOn 𝕜 (fun x ↦ p x n) s
f : E → F
hf : AnalyticOn 𝕜 f s
h : MapsTo f s t
n : ℕ
c : OrderedFinpartition n
x✝ : c ∈ Finset.univ
B : (F [×c.length]→L[𝕜] G) →L[𝕜] (E [×c.partSize i]→L[𝕜] F) [×c.length]→L[𝕜] E [×n]→L[𝕜] G :=
  OrderedFinpartition.compAlongOrderedFinpartitionL 𝕜 E F G c
⊢ AnalyticOn 𝕜 (fun a ↦ (q (f a)).compAlongOrderedFinpartition (p a) c) s

Tactic:
change AnalyticOn 𝕜
    ((fun p ↦ B p.1 p.2) ∘ (fun x ↦ (q (f x) c.length, fun m ↦ p x (c.partSize m)))) s

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
hq : ∀ (n : ℕ), AnalyticOn 𝕜 (fun x ↦ q x n) t
hp : ∀ (n : ℕ), AnalyticOn 𝕜 (fun x ↦ p x n) s
f : E → F
hf : AnalyticOn 𝕜 f s
h : MapsTo f s t
n : ℕ
c : OrderedFinpartition n
x✝ : c ∈ Finset.univ
B : (F [×c.length]→L[𝕜] G) →L[𝕜] (E [×c.partSize i]→L[𝕜] F) [×c.length]→L[𝕜] E [×n]→L[𝕜] G :=
  OrderedFinpartition.compAlongOrderedFinpartitionL 𝕜 E F G c
⊢ AnalyticOn 𝕜 ((fun p ↦ (B p.1) p.2) ∘ fun x ↦ (q (f x) c.length, fun m ↦ p x (c.partSize m))) s
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
s : Set E
ι : Type u_3
f : ι → E → F
u : Finset ι
i : ℕ
x : E
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
h : ∀ j ∈ u, ContDiffWithinAt 𝕜 (↑i) (f j) s x
⊢ ∑ j ∈ u, f j = fun x ↦ ∑ j ∈ u, f j x

Tactic:
aesop

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

Goal state before:
pp: case cons
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
ι : Type u_3
f : ι → E → F
i : ℕ
x : E
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
a : ι
u : Finset ι
ha : a ∉ u
IH :
  (∀ j ∈ u, ContDiffWithinAt 𝕜 (↑i) (f j) s x) →
    iteratedFDerivWithin 𝕜 i (fun x ↦ ∑ j ∈ u, f j x) s x = ∑ j ∈ u, iteratedFDerivWithin 𝕜 i (f j) s x
h : ContDiffWithinAt 𝕜 (↑i) (f a) s x ∧ ∀ a ∈ u, ContDiffWithinAt 𝕜 (↑i) (f a) s x
⊢ iteratedFDerivWithin 𝕜 i (fun x ↦ f a x + ∑ j ∈ u, f j x) s x =
    iteratedFDerivWithin 𝕜 i (f a) s x + ∑ j ∈ u, iteratedFDerivWithin 𝕜 i (f j) s x

Tactic:
fun_iteratedFDerivWithin_add_apply h.1 (ContDiffWithinAt.sum h.2) hs hx,

Goal state after:
case cons
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
ι : Type u_3
f : ι → E → F
i : ℕ
x : E
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
a : ι
u : Finset ι
ha : a ∉ u
IH :
  (∀ j ∈ u, ContDiffWithinAt 𝕜 (↑i) (f j) s x) →
    iteratedFDerivWithin 𝕜 i (fun x ↦ ∑ j ∈ u, f j x) s x = ∑ j ∈ u, iteratedFDerivWithin 𝕜 i (f j) s x
h : ContDiffWithinAt 𝕜 (↑i) (f a) s x ∧ ∀ a ∈ u, ContDiffWithinAt 𝕜 (↑i) (f a) s x
⊢ iteratedFDerivWithin 𝕜 i (f a) s x + iteratedFDerivWithin 𝕜 i (fun x ↦ ∑ i ∈ u, f i x) s x =
    iteratedFDerivWithin 𝕜 i (f a) s x + ∑ j ∈ u, iteratedFDerivWithin 𝕜 i (f j) s x
Module: Mathlib.Topology.Order.ExtendFrom

Goal state before:
pp: case neg.inr
α : 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 (uIoo a b)
ha : Tendsto f (𝓝[uIoo a b] a) (𝓝 la)
hb : Tendsto f (𝓝[uIoo a b] b) (𝓝 lb)
hab : a ≠ b
hba' : b < a
⊢ ContinuousOn (extendFrom (uIoo a b) f) (uIcc a b)

Tactic:
· simp only [hba', uIoo_of_gt, nhdsWithin_Ioo_eq_nhdsGT, nhdsWithin_Ioo_eq_nhdsLT,
      uIcc_of_gt] at ha hb hf ⊢
    exact continuousOn_Icc_extendFrom_Ioo hf hb ha

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

Goal state before:
pp: case succ.h
𝕜 : 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
⊢ DifferentiableAt 𝕜 (fun x ↦ iteratedFDeriv 𝕜 i f (a • x)) v

Tactic:
← Function.comp_def (g := (a • ·))

Goal state after:
case succ.h
𝕜 : 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
⊢ DifferentiableAt 𝕜 (iteratedFDeriv 𝕜 i f ∘ fun x ↦ a • x) v
Module: Mathlib.Analysis.Calculus.ContDiff.Operations

Goal state before:
pp: case hf
𝕜 : 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
⊢ DifferentiableAt 𝕜 (fun x ↦ a • x) v

Tactic:
exact differentiableAt_id.const_smul _

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

Goal state before:
pp: case neg.refine_2
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : μ.WeaklyRegular
c : ℝ≥0
s : Set α
hs : MeasurableSet s
ε : ℝ≥0∞
ε0 : ε ≠ 0
f : α →ₛ ℝ≥0 := piecewise s hs (const α c) (const α 0)
h : ¬∫⁻ (x : α), ↑(f x) ∂μ = ∞
hc : ¬c = 0
ne_top : μ s ≠ ∞
this : μ s < μ s + ε / ↑c
u : Set α
su : u ⊇ s
u_open : IsOpen u
μu : μ u < μ s + ε / ↑c
⊢ ∫⁻ (x : α), ↑(u.indicator (fun x ↦ c) x) ∂μ ≤ ∫⁻ (x : α), ↑((piecewise s hs (const α c) (const α 0)) x) ∂μ + ε

Tactic:
suffices (c : ℝ≥0∞) * μ u ≤ c * μ s + ε by
        simpa only [ENNReal.coe_indicator, u_open.measurableSet, lintegral_indicator,
          lintegral_const, MeasurableSet.univ, Measure.restrict_apply, Set.univ_inter, const_zero,
          coe_piecewise, coe_const, coe_zero, Set.piecewise_eq_indicator, Function.const_apply, hs]

Goal state after:
case neg.refine_2
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : μ.WeaklyRegular
c : ℝ≥0
s : Set α
hs : MeasurableSet s
ε : ℝ≥0∞
ε0 : ε ≠ 0
f : α →ₛ ℝ≥0 := piecewise s hs (const α c) (const α 0)
h : ¬∫⁻ (x : α), ↑(f x) ∂μ = ∞
hc : ¬c = 0
ne_top : μ s ≠ ∞
this : μ s < μ s + ε / ↑c
u : Set α
su : u ⊇ s
u_open : IsOpen u
μu : μ u < μ s + ε / ↑c
⊢ ↑c * μ u ≤ ↑c * μ s + ε
Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv

Goal state before:
pp: f : ℝ → ℝ
x f' : ℝ
hf : HasStrictDerivAt f f' x
hx : f x ≠ 0
⊢ HasStrictDerivAt (fun y ↦ Real.log (f y)) (f' / f x) x

Tactic:
rw [div_eq_inv_mul]
  exact (hasStrictDerivAt_log hx).comp x hf

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

Goal state before:
pp: R : Type u_1
E : Type u_2
inst✝⁴ : Ring R
inst✝³ : LinearOrder R
inst✝² : IsOrderedRing R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
x✝³ : Submodule R E
x✝² : PointedCone R E
x✝¹ : ↑x✝³ ≤ x✝²
x✝ : E
⊢ x✝ ∈ x✝³ → x✝ ∈ x✝².lineal

Tactic:
aesop

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

Goal state before:
pp: case neg
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
h : 0 ∉ s
⊢ sInf {r | r ∈ Ioi 0 ∧ r⁻¹ • 0 ∈ s} = 0

Tactic:
· simp only [smul_zero, sep_false, h, Real.sInf_empty]

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
x : E
inst✝¹ : TopologicalSpace E
inst✝ : T1Space E
hs : Absorbent ℝ s
hb : Bornology.IsVonNBounded ℝ s
h₀ : gauge s x = 0
hne : x ≠ 0
this : {x}ᶜ ∈ comap (gauge s) (𝓝 0)
r : ℝ
hr₀ : 0 < r
hr : gauge s ⁻¹' {b | |b| < r} ⊆ {x}ᶜ
⊢ x ∈ gauge s ⁻¹' {b | |b| < r}

Tactic:
simpa [h₀]

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

Goal state before:
pp: case refine_1.inr
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : Module ℝ E
inst✝ : ContinuousSMul ℝ E
s : Set E
hs₀ : 0 ∈ s
hs₁ : Convex ℝ s
hs₂ : IsOpen s
x₀ : E
hx₀ : x₀ ∉ s
f : E →ₗ.[ℝ] ℝ := LinearPMap.mkSpanSingleton x₀ 1 ⋯
y : ℝ
hx : y • x₀ ∈ f.domain
h : 0 < y
⊢ 1 ≤ gauge s x₀

Tactic:
exact
      one_le_gauge_of_notMem (hs₁.starConvex hs₀)
        (absorbent_nhds_zero <| hs₂.mem_nhds hs₀).absorbs hx₀

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

Goal state before:
pp: case inr.refine_1
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
p : Seminorm ℝ E
r : ℝ
hr : 0 < r
y : E
hy : p y < 1
hp : {r_1 | 0 < r_1 ∧ (fun x ↦ r • x) y ∈ r_1 • p.ball 0 1}.Nonempty
⊢ r * p y ≤ r

Tactic:
exact mul_le_of_le_one_right hr.le hy.le

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
S : Type u_3
inst✝⁶ : CommSemiring S
inst✝⁵ : Module S V
inst✝⁴ : SMulCommClass R S V
inst✝³ : Algebra S R
inst✝² : IsScalarTower S R V
inst✝¹ : ContinuousConstSMul S V
inst✝ : Algebra.IsCentral S R
f : V →L[R] V
hf : f ∈ Subalgebra.center S (V →L[R] V)
this : ∃ α ∈ Subalgebra.center S R, f = α • ContinuousLinearMap.id R V
w✝ : R
y : S
h✝ : (Algebra.ofId S R).toRingHom y = w✝
right✝ : f = w✝ • ContinuousLinearMap.id R V
⊢ (Algebra.ofId S (V →L[R] V)).toRingHom y = f

Tactic:
aesop

Goal state after: