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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace 𝕜 H
r : FormalMultilinearSeries 𝕜 G H
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
v : Fin n → E
f : (a : Composition n) × Composition a.length → H :=
  fun c ↦ (r c.snd.length) (q.applyComposition c.snd (p.applyComposition c.fst v))
g : (c : Composition n) × ((i : Fin c.length) → Composition (c.blocksFun i)) → H :=
  fun c ↦ (r c.fst.length) fun i ↦ (q (c.snd i).length) (p.applyComposition (c.snd i) (v ∘ ⇑(c.fst.embedding i)))
a : Composition n
b : Composition a.length
a✝ : ⟨a, b⟩ ∈ Finset.univ
⊢ f ⟨a, b⟩ = g ⟨a.gather b, a.sigmaCompositionAux b⟩

Tactic:
apply r.congr (Composition.length_gather a b).symm

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace 𝕜 H
r : FormalMultilinearSeries 𝕜 G H
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
v : Fin n → E
f : (a : Composition n) × Composition a.length → H := ⋯
g : (c : Composition n) × ((i : Fin c.length) → Composition (c.blocksFun i)) → H := ⋯
a : Composition n
b : Composition a.length
a✝ : ⟨a, b⟩ ∈ Finset.univ
⊢ ∀ (i : ℕ) (him : i < b.length) (hin : i < (a.gather b).length),
    q.applyComposition ⟨a, b⟩.snd (p.applyComposition ⟨a, b⟩.fst v) ⟨i, him⟩ =
      (q (⟨a.gather b, a.sigmaCompositionAux b⟩.snd ⟨i, hin⟩).length)
        (p.applyComposition (⟨a.gather b, a.sigmaCompositionAux b⟩.snd ⟨i, hin⟩)
          (v ∘ ⇑(⟨a.gather b, a.sigmaCompositionAux b⟩.fst.embedding ⟨i, hin⟩)))
Module: Mathlib.Analysis.Calculus.FDeriv.Equiv

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
f' : E →L[𝕜] F
x : E
h : HasFDerivAt f f' x
hf' : ∃ C, AntilipschitzWith C ⇑f'
t : Set F
ht : ¬AccPt (f x) (𝓟 t)
⊢ ∀ᶠ (z : E) in 𝓝[≠] x, f z ∉ t

Tactic:
by
  simpa only [compl_eq_univ_sdiff] using (hasFDerivWithinAt_univ.2 h).eventually_notMem hf' t ht

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Alternating.Basic

Goal state before:
pp: 𝕜 : Type u
n : ℕ
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : SeminormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : SeminormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
g : E →L[𝕜] F
f : F [⋀^ι]→L[𝕜] G
dg : E →L[𝕜] F
v : ι → E
⊢ ∀ x ∈ univ,
    ‖f fun j ↦ (Function.update (fun x ↦ g) x dg j) (v j)‖ ≤ ‖g‖ ^ (Fintype.card ι - 1) * (‖f‖ * (‖dg‖ * ∏ i, ‖v i‖))

Tactic:
rintro i -

Goal state after:
𝕜 : Type u
n : ℕ
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : SeminormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : SeminormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
g : E →L[𝕜] F
f : F [⋀^ι]→L[𝕜] G
dg : E →L[𝕜] F
v : ι → E
i : ι
⊢ ‖f fun j ↦ (Function.update (fun x ↦ g) i dg j) (v j)‖ ≤ ‖g‖ ^ (Fintype.card ι - 1) * (‖f‖ * (‖dg‖ * ∏ i, ‖v i‖))
Module: Mathlib.Topology.MetricSpace.Completion

Goal state before:
pp: case refine_2
α : Type u
inst✝ : PseudoMetricSpace α
x y z : Completion α
⊢ ∀ (a b c : α), dist ↑a ↑c ≤ dist ↑a ↑b + dist ↑b ↑c

Tactic:
· intro a b c
    rw [Completion.dist_eq, Completion.dist_eq, Completion.dist_eq]
    exact dist_triangle a b c

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

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 f₁ : E → F
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpToOn n f p s
h₁ : ∀ x ∈ s, f₁ x = f x
x : E
hx : x ∈ s
⊢ (p x 0).curry0 = f x

Tactic:
exact h.zero_eq x hx

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

Goal state before:
pp: 𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
𝔸 : Type u_3
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸
d : 𝕜 → 𝔸
d' c : 𝔸
hd : HasDerivWithinAt d d' univ x
⊢ HasDerivWithinAt (fun y ↦ c * d y) (c * d') univ x

Tactic:
exact hd.const_mul c

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Slope

Goal state before:
pp: case neg.refine_1
k : Type u_1
E : Type u_2
inst✝⁷ : Field k
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module k E
inst✝⁴ : LinearOrder k
inst✝³ : IsStrictOrderedRing k
inst✝² : PartialOrder E
inst✝¹ : IsOrderedAddMonoid E
inst✝ : PosSMulMono k E
f : k → E
x y : k
hxy : x ≤ y
hxeqy : ¬x = y
h : 0 ≤ slope f x y
this : 0 ≤ f y - f x
⊢ f x ≤ f y

Tactic:
sub_nonneg

Goal state after:
case neg.refine_1
k : Type u_1
E : Type u_2
inst✝⁷ : Field k
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module k E
inst✝⁴ : LinearOrder k
inst✝³ : IsStrictOrderedRing k
inst✝² : PartialOrder E
inst✝¹ : IsOrderedAddMonoid E
inst✝ : PosSMulMono k E
f : k → E
x y : k
hxy : x ≤ y
hxeqy : ¬x = y
h : 0 ≤ slope f x y
this : f x ≤ f y
⊢ f x ≤ f y
Module: Mathlib.LinearAlgebra.AffineSpace.Slope

Goal state before:
pp: case neg.refine_2
k : Type u_1
E : Type u_2
inst✝⁷ : Field k
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module k E
inst✝⁴ : LinearOrder k
inst✝³ : IsStrictOrderedRing k
inst✝² : PartialOrder E
inst✝¹ : IsOrderedAddMonoid E
inst✝ : PosSMulMono k E
f : k → E
x y : k
hxy : x ≤ y
hxeqy : ¬x = y
h : f x ≤ f y
⊢ 0 ≤ f y - f x

Tactic:
sub_nonneg

Goal state after:
case neg.refine_2
k : Type u_1
E : Type u_2
inst✝⁷ : Field k
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module k E
inst✝⁴ : LinearOrder k
inst✝³ : IsStrictOrderedRing k
inst✝² : PartialOrder E
inst✝¹ : IsOrderedAddMonoid E
inst✝ : PosSMulMono k E
f : k → E
x y : k
hxy : x ≤ y
hxeqy : ¬x = y
h : f x ≤ f y
⊢ f x ≤ f y
Module: Mathlib.Analysis.Calculus.FDeriv.Analytic

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst✝² : (i : ι) → NormedAddCommGroup (E i)
inst✝¹ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝ : Fintype ι
f : ContinuousMultilinearMap 𝕜 E F
⊢ HasFTaylorSeriesUpTo ⊤ ⇑f fun v n ↦ f.iteratedFDeriv n v

Tactic:
constructor
  · simp [ContinuousMultilinearMap.iteratedFDeriv]
  · rintro n - x
    suffices H : curryLeft (f.iteratedFDeriv (Nat.succ n) x) = (∑ e : Fin n ↪ ι,
          ((iteratedFDerivComponent f e.toEquivRange).linearDeriv
            (Pi.compRightL 𝕜 _ Subtype.val x)) ∘L (Pi.compRightL 𝕜 _ Subtype.val)) by
      have A : HasFDerivAt (f.iteratedFDeriv n) (∑ e : Fin n ↪ ι,
          ((iteratedFDerivComponent f e.toEquivRange).linearDeriv (Pi.compRightL 𝕜 _ Subtype.val x))
            ∘L (Pi.compRightL 𝕜 _ Subtype.val)) x := by
        apply HasFDerivAt.fun_sum (fun s _hs ↦ ?_)
        exact (ContinuousMultilinearMap.hasFDerivAt _ _).comp x (ContinuousLinearMap.hasFDerivAt _)
      rwa [← H] at A
    ext v m
    simp only [ContinuousMultilinearMap.iteratedFDeriv, curryLeft_apply, sum_apply,
      iteratedFDerivComponent_apply, Finset.univ_sigma_univ,
      Pi.compRightL_apply, _root_.sum_apply, ContinuousLinearMap.comp_apply, linearDeriv_apply,
      Finset.sum_sigma']
    rw [← (Equiv.embeddingFinSucc n ι).sum_comp]
    congr with e
    congr with k
    by_cases hke : k ∈ Set.range e
    · simp only [hke, ↓reduceDIte]
      split_ifs with hkf
      · simp only [← Equiv.succ_embeddingFinSucc_fst_symm_apply e hkf hke, Fin.cons_succ]
      · obtain rfl : k = e 0 := by
          rcases hke with ⟨j, rfl⟩
          simpa using hkf
        simp only [Function.Embedding.toEquivRange_symm_apply_self, Fin.cons_zero, Function.update,
          Pi.compRightL_apply]
        split_ifs with h
        · congr!
        · exfalso
          apply h
          simp_rw [← Equiv.embeddingFinSucc_snd e]
    · have hkf : k ∉ Set.range (Equiv.embeddingFinSucc n ι e).1 := by
        contrapose hke
        rw [Equiv.embeddingFinSucc_fst] at hke
        exact Set.range_comp_subset_range _ _ hke
      simp only [hke, hkf, ↓reduceDIte, Pi.compRightL,
        ContinuousLinearMap.coe_mk', LinearMap.coe_mk, AddHom.coe_mk]
      rw [Function.update_of_ne]
      contrapose hke
      rw [show k = _ from Subtype.ext_iff.1 hke, Equiv.embeddingFinSucc_snd e]
      exact Set.mem_range_self _
  · rintro n -
    apply continuous_finsetSum _ (fun e _ ↦ ?_)
    exact (ContinuousMultilinearMap.coe_continuous _).comp (ContinuousLinearMap.continuous _)

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

Goal state before:
pp: case succ
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
x : E
r : ℝ≥0∞
y : E
n : ℕ
ih :
  ∀ {F : Type (max u v)} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace 𝕜 F] [CompleteSpace F]
    {p : FormalMultilinearSeries 𝕜 E F} {f : E → F},
    HasFPowerSeriesOnBall f p x r → (n ! • (p n) fun x ↦ y) = (iteratedFDeriv 𝕜 n f x) fun x ↦ y
F : Type (max u v)
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
p : FormalMultilinearSeries 𝕜 E F
f : E → F
h : HasFPowerSeriesOnBall f p x r
⊢ ((iteratedFDeriv 𝕜 n (fderiv 𝕜 f) x) fun x ↦ y) y = (iteratedFDeriv 𝕜 (n + 1) f x) fun x ↦ y

Tactic:
iteratedFDeriv_succ_apply_right

Goal state after:
case succ
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
x : E
r : ℝ≥0∞
y : E
n : ℕ
ih :
  ∀ {F : Type (max u v)} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace 𝕜 F] [CompleteSpace F]
    {p : FormalMultilinearSeries 𝕜 E F} {f : E → F},
    HasFPowerSeriesOnBall f p x r → (n ! • (p n) fun x ↦ y) = (iteratedFDeriv 𝕜 n f x) fun x ↦ y
F : Type (max u v)
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
p : FormalMultilinearSeries 𝕜 E F
f : E → F
h : HasFPowerSeriesOnBall f p x r
⊢ ((iteratedFDeriv 𝕜 n (fderiv 𝕜 f) x) fun x ↦ y) y =
    ((iteratedFDeriv 𝕜 n (fun y ↦ fderiv 𝕜 f y) x) (Fin.init fun x ↦ y)) y
Module: Mathlib.Analysis.Calculus.FDeriv.Analytic

Goal state before:
pp: case succ
𝕜 : 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
f : E → F
x : E
r : ℝ≥0∞
h : HasFPowerSeriesOnBall f p x r
y : E
inst✝ : CompleteSpace F
n✝ : ℕ
⊢ ((iteratedFDeriv 𝕜 n✝ (fderiv 𝕜 f) x) fun x ↦ y) y = (iteratedFDeriv 𝕜 (n✝ + 1) f x) fun x ↦ y

Tactic:
iteratedFDeriv_succ_apply_right

Goal state after:
case succ
𝕜 : 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
f : E → F
x : E
r : ℝ≥0∞
h : HasFPowerSeriesOnBall f p x r
y : E
inst✝ : CompleteSpace F
n✝ : ℕ
⊢ ((iteratedFDeriv 𝕜 n✝ (fderiv 𝕜 f) x) fun x ↦ y) y =
    ((iteratedFDeriv 𝕜 n✝ (fun y ↦ fderiv 𝕜 f y) x) (Fin.init fun x ↦ y)) y
Module: Mathlib.Analysis.Calculus.Deriv.Comp

Goal state before:
pp: 𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
L : Filter (𝕜 × 𝕜)
f : 𝕜 → 𝕜
f' : 𝕜
hf : HasDerivAtFilter f f' L
hL : Tendsto (Prod.map f f) L L
n : ℕ
this : HasFDerivAtFilter f^[n] (ContinuousLinearMap.toSpanSingleton 𝕜 f' ^ n) L
⊢ HasDerivAtFilter f^[n] (f' ^ n) L

Tactic:
rwa [ContinuousLinearMap.toSpanSingleton_pow] at this

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

Goal state before:
pp: 𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
f' : 𝕜
hf : HasDerivWithinAt f f' s x
hx : f x = x
hs : MapsTo f s s
n : ℕ
this : HasFDerivWithinAt f^[n] (ContinuousLinearMap.toSpanSingleton 𝕜 f' ^ n) s x
⊢ HasDerivWithinAt f^[n] (f' ^ n) s x

Tactic:
rwa [ContinuousLinearMap.toSpanSingleton_pow] at this

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

Goal state before:
pp: 𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
f : 𝕜 → 𝕜
f' : 𝕜
hf : HasStrictDerivAt f f' x
hx : f x = x
n : ℕ
this : HasStrictFDerivAt f^[n] (ContinuousLinearMap.toSpanSingleton 𝕜 f' ^ n) x
⊢ HasStrictDerivAt f^[n] (f' ^ n) x

Tactic:
rwa [ContinuousLinearMap.toSpanSingleton_pow] at this

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

Goal state before:
pp: case succ
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
c d : 𝕜
k : ℕ
ihk : (deriv^[k] fun x ↦ (c * x + d)⁻¹) = fun x ↦ (-1) ^ k * ↑k ! * c ^ k * (c * x + d) ^ (-1 - ↑k)
z : 𝕜
⊢ (-1) ^ k * ↑k ! * c ^ k * deriv (fun x ↦ (c * x + d) ^ (-1 - ↑k)) z =
    (-1) ^ (1 + k) * ↑((1 + k) * k !) * c ^ (1 + k) * (c * z + d) ^ (-1 - (1 + ↑k))

Tactic:
by_cases hd : c = 0

Goal state after:
case pos
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
c d : 𝕜
k : ℕ
ihk : (deriv^[k] fun x ↦ (c * x + d)⁻¹) = fun x ↦ (-1) ^ k * ↑k ! * c ^ k * (c * x + d) ^ (-1 - ↑k)
z : 𝕜
hd : c = 0
⊢ (-1) ^ k * ↑k ! * c ^ k * deriv (fun x ↦ (c * x + d) ^ (-1 - ↑k)) z =
    (-1) ^ (1 + k) * ↑((1 + k) * k !) * c ^ (1 + k) * (c * z + d) ^ (-1 - (1 + ↑k))

case neg
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
c d : 𝕜
k : ℕ
ihk : (deriv^[k] fun x ↦ (c * x + d)⁻¹) = fun x ↦ (-1) ^ k * ↑k ! * c ^ k * (c * x + d) ^ (-1 - ↑k)
z : 𝕜
hd : ¬c = 0
⊢ (-1) ^ k * ↑k ! * c ^ k * deriv (fun x ↦ (c * x + d) ^ (-1 - ↑k)) z =
    (-1) ^ (1 + k) * ↑((1 + k) * k !) * c ^ (1 + k) * (c * z + d) ^ (-1 - (1 + ↑k))
Module: Mathlib.Analysis.Calculus.LogDeriv

Goal state before:
pp: case inr.mp
𝕜 : Type u_1
𝕜' : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NontriviallyNormedField 𝕜'
inst✝¹ : NormedAlgebra 𝕜 𝕜'
inst✝ : IsRCLikeNormedField 𝕜
f g : 𝕜 → 𝕜'
s : Set 𝕜
hf : DifferentiableOn 𝕜 f s
hg : DifferentiableOn 𝕜 g s
hs2 : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hsc : IsPreconnected s
hgn : ∀ x ∈ s, g x ≠ 0
hfn : ∀ x ∈ s, f x ≠ 0
t : 𝕜
ht : t ∈ s
⊢ EqOn (logDeriv f) (logDeriv g) s → ∃ z, z ≠ 0 ∧ EqOn f (z • g) s

Tactic:
refine fun h ↦ ⟨f t * (g t)⁻¹, by grind, fun y hy ↦ ?_⟩

Goal state after:
case inr.mp
𝕜 : Type u_1
𝕜' : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NontriviallyNormedField 𝕜'
inst✝¹ : NormedAlgebra 𝕜 𝕜'
inst✝ : IsRCLikeNormedField 𝕜
f g : 𝕜 → 𝕜'
s : Set 𝕜
hf : DifferentiableOn 𝕜 f s
hg : DifferentiableOn 𝕜 g s
hs2 : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hsc : IsPreconnected s
hgn : ∀ x ∈ s, g x ≠ 0
hfn : ∀ x ∈ s, f x ≠ 0
t : 𝕜
ht : t ∈ s
h : EqOn (logDeriv f) (logDeriv g) s
y : 𝕜
hy : y ∈ s
⊢ f y = ((f t * (g t)⁻¹) • g) y
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
hf : ContDiffWithinAt 𝕜 ω f s x
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
v : Set F
hv : v ∈ 𝓝[insert (f x) t] f x
q : F → FormalMultilinearSeries 𝕜 F G
hq : HasFTaylorSeriesUpToOn ω g q v
h'q : ∀ (i : ℕ), AnalyticOn 𝕜 (fun x ↦ q x i) v
w : Set E := insert x s ∩ (u ∩ f ⁻¹' v)
⊢ ContDiffWithinAt 𝕜 ω (g ∘ f) s x

Tactic:
have wv : w ⊆ f ⁻¹' v := fun y hy => hy.2.2

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
hf : ContDiffWithinAt 𝕜 ω f s x
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
v : Set F
hv : v ∈ 𝓝[insert (f x) t] f x
q : F → FormalMultilinearSeries 𝕜 F G
hq : HasFTaylorSeriesUpToOn ω g q v
h'q : ∀ (i : ℕ), AnalyticOn 𝕜 (fun x ↦ q x i) v
w : Set E := insert x s ∩ (u ∩ f ⁻¹' v)
wv : w ⊆ f ⁻¹' v
⊢ ContDiffWithinAt 𝕜 ω (g ∘ f) s x
Module: Mathlib.Analysis.Calculus.ContDiff.Comp

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

Tactic:
have wv : w ⊆ f ⁻¹' v := fun y hy => hy.2.2

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
w : Set E := insert x s ∩ (u ∩ f ⁻¹' v)
wv : w ⊆ f ⁻¹' v
⊢ ∃ u ∈ 𝓝[insert x s] x, ∃ p, HasFTaylorSeriesUpToOn (↑m) (g ∘ f) p u
Module: Mathlib.Analysis.Calculus.ContDiff.Deriv

Goal state before:
pp: 𝕜 : Type u_1
F : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ∞ω
f : 𝕜 → F
s : Set 𝕜
h : ContDiffOn 𝕜 n f s
hs : IsOpen s
hn : 1 ≤ n
⊢ ContinuousOn (deriv f) s

Tactic:
rw [show (1 : ℕ∞ω) = 0 + 1 from rfl] at hn
  exact ((contDiffOn_succ_iff_deriv_of_isOpen hs).1 (h.of_le hn)).2.2.continuousOn

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

Goal state before:
pp: case 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
i : Fin (c.length + 1)
j : Fin c.length
a✝ :
  i < j.castSucc →
    (fun m ↦
          cases (motive := fun x ↦ Fin (cons 1 c.partSize x) → Fin (n + 1)) (fun x ↦ 0) (fun m ↦ succ ∘ c.emb m) m
            ⟨cons 1 c.partSize m - 1, ⋯⟩)
        i <
      (fun m ↦
          cases (motive := fun x ↦ Fin (cons 1 c.partSize x) → Fin (n + 1)) (fun x ↦ 0) (fun m ↦ succ ∘ c.emb m) m
            ⟨cons 1 c.partSize m - 1, ⋯⟩)
        j.castSucc
hij : i < j.succ
⊢ (fun m ↦
        cases (motive := fun x ↦ Fin (cons 1 c.partSize x) → Fin (n + 1)) (fun x ↦ 0) (fun m ↦ succ ∘ c.emb m) m
          ⟨cons 1 c.partSize m - 1, ⋯⟩)
      i <
    (fun m ↦
        cases (motive := fun x ↦ Fin (cons 1 c.partSize x) → Fin (n + 1)) (fun x ↦ 0) (fun m ↦ succ ∘ c.emb m) m
          ⟨cons 1 c.partSize m - 1, ⋯⟩)
      j.succ

Tactic:
| succ j =>

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

Goal state before:
pp: case 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
i : Fin c.length
hi : i.succ ∈ univ
j : Fin c.length
a✝¹ :
  j.castSucc ∈ univ →
    (i.castSucc ∈ univ →
        i.castSucc ≠ j.castSucc →
          j.castSucc < i.castSucc →
            (Disjoint on fun m ↦
                range
                  (cases (motive := fun x ↦ Fin (cons 1 c.partSize x) → Fin (n + 1)) (fun x ↦ 0)
                    (fun m ↦ succ ∘ c.emb m) m))
              i.castSucc j.castSucc) →
      i.succ ≠ j.castSucc →
        j.castSucc < i.succ →
          (Disjoint on fun m ↦
              range
                (cases (motive := fun x ↦ Fin (cons 1 c.partSize x) → Fin (n + 1)) (fun x ↦ 0) (fun m ↦ succ ∘ c.emb m)
                  m))
            i.succ j.castSucc
hj : j.succ ∈ univ
a✝ :
  i.castSucc ∈ univ →
    i.castSucc ≠ j.succ →
      j.succ < i.castSucc →
        (Disjoint on fun m ↦
            range
              (cases (motive := fun x ↦ Fin (cons 1 c.partSize x) → Fin (n + 1)) (fun x ↦ 0) (fun m ↦ succ ∘ c.emb m)
                m))
          i.castSucc j.succ
hij : i.succ ≠ j.succ
h : j.succ < i.succ
⊢ (Disjoint on fun m ↦
      range (cases (motive := fun x ↦ Fin (cons 1 c.partSize x) → Fin (n + 1)) (fun x ↦ 0) (fun m ↦ succ ∘ c.emb m) m))
    i.succ j.succ

Tactic:
| succ j =>

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
⊢ iteratedFDeriv 𝕜 n f = ⇑(ContinuousMultilinearMap.piFieldEquiv 𝕜 (Fin n) F) ∘ iteratedDeriv n f

Tactic:
rw [iteratedDeriv_eq_equiv_comp, ← Function.comp_assoc, LinearIsometryEquiv.self_comp_symm,
    Function.id_comp]

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

Goal state before:
pp: 𝕜 : Type u_3
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : CompleteSpace 𝕜
inst✝ : CharZero 𝕜
f : 𝕜 → 𝕜
x : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 𝕜
r : ENNReal
hpr : HasFPowerSeriesOnBall f p x r
n : ℕ
h_fact_smul : ∀ (n : ℕ), ↑n.factorial * p.coeff n = (iteratedFDeriv 𝕜 n f x) fun x ↦ 1
⊢ iteratedDeriv n f x = (iteratedFDeriv 𝕜 n f x) fun x ↦ 1

pp: 𝕜 : Type u_3
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : CompleteSpace 𝕜
inst✝ : CharZero 𝕜
f : 𝕜 → 𝕜
x : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 𝕜
r : ENNReal
hpr : HasFPowerSeriesOnBall f p x r
n : ℕ
h_fact_smul : ∀ (n : ℕ), ↑n.factorial * p.coeff n = (iteratedFDeriv 𝕜 n f x) fun x ↦ 1
⊢ ↑n.factorial ≠ 0

Tactic:
← iteratedDeriv_eq_iteratedFDeriv

Goal state after:
𝕜 : Type u_3
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : CompleteSpace 𝕜
inst✝ : CharZero 𝕜
f : 𝕜 → 𝕜
x : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 𝕜
r : ENNReal
hpr : HasFPowerSeriesOnBall f p x r
n : ℕ
h_fact_smul : ∀ (n : ℕ), ↑n.factorial * p.coeff n = (iteratedFDeriv 𝕜 n f x) fun x ↦ 1
⊢ iteratedDeriv n f x = iteratedDeriv n f x

𝕜 : Type u_3
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : CompleteSpace 𝕜
inst✝ : CharZero 𝕜
f : 𝕜 → 𝕜
x : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 𝕜
r : ENNReal
hpr : HasFPowerSeriesOnBall f p x r
n : ℕ
h_fact_smul : ∀ (n : ℕ), ↑n.factorial * p.coeff n = (iteratedFDeriv 𝕜 n f x) fun x ↦ 1
⊢ ↑n.factorial ≠ 0