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

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
x : E
s : Set E
R : Type u_4
inst✝⁴ : Monoid R
inst✝³ : DistribMulAction R F
inst✝² : SMulCommClass 𝕜 R F
inst✝¹ : ContinuousConstSMul R F
c : R
inst✝ : Invertible c
hs : UniqueDiffWithinAt 𝕜 s x
⊢ fderivWithin 𝕜 (c • f) s x = c • fderivWithin 𝕜 f s x

Tactic:
by_cases h : DifferentiableWithinAt 𝕜 f s x

Goal state after:
case pos
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
f : E → F
x : E
s : Set E
R : Type u_4
inst✝⁴ : Monoid R
inst✝³ : DistribMulAction R F
inst✝² : SMulCommClass 𝕜 R F
inst✝¹ : ContinuousConstSMul R F
c : R
inst✝ : Invertible c
hs : UniqueDiffWithinAt 𝕜 s x
h : DifferentiableWithinAt 𝕜 f s x
⊢ fderivWithin 𝕜 (c • f) s x = c • fderivWithin 𝕜 f s x

case neg
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
f : E → F
x : E
s : Set E
R : Type u_4
inst✝⁴ : Monoid R
inst✝³ : DistribMulAction R F
inst✝² : SMulCommClass 𝕜 R F
inst✝¹ : ContinuousConstSMul R F
c : R
inst✝ : Invertible c
hs : UniqueDiffWithinAt 𝕜 s x
h : ¬DifferentiableWithinAt 𝕜 f s x
⊢ fderivWithin 𝕜 (c • f) s x = c • fderivWithin 𝕜 f s x
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
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : G → E
s : Set G
x : G
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ fderivWithin 𝕜 (⇑iso ∘ f) s x = ↑iso ∘SL fderivWithin 𝕜 f s x

Tactic:
by_cases h : DifferentiableWithinAt 𝕜 f s x

Goal state after:
case pos
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : G → E
s : Set G
x : G
hxs : UniqueDiffWithinAt 𝕜 s x
h : DifferentiableWithinAt 𝕜 f s x
⊢ fderivWithin 𝕜 (⇑iso ∘ f) s x = ↑iso ∘SL fderivWithin 𝕜 f s x

case neg
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : G → E
s : Set G
x : G
hxs : UniqueDiffWithinAt 𝕜 s x
h : ¬DifferentiableWithinAt 𝕜 f s x
⊢ fderivWithin 𝕜 (⇑iso ∘ f) s x = ↑iso ∘SL fderivWithin 𝕜 f s x
Module: Mathlib.Analysis.Calculus.FDeriv.Add

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
L : Filter (E × E)
ι : Type u_4
u : Finset ι
A : ι → E → F
A' : ι → E →L[𝕜] F
h : ∀ i ∈ u, HasFDerivAtFilter (A i) (A' i) L
⊢ HasFDerivAtFilter (fun y ↦ ∑ i ∈ u, A i y) (∑ i ∈ u, A' i) L

Tactic:
simp only [hasFDerivAtFilter_iff_isLittleO] at *
  convert! IsLittleO.sum h
  simp

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

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
x : E
s : Set E
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ fderivWithin 𝕜 (fun y ↦ -f y) s x = -fderivWithin 𝕜 f s x

Tactic:
by_cases h : DifferentiableWithinAt 𝕜 f s x

Goal state after:
case pos
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
s : Set E
hxs : UniqueDiffWithinAt 𝕜 s x
h : DifferentiableWithinAt 𝕜 f s x
⊢ fderivWithin 𝕜 (fun y ↦ -f y) s x = -fderivWithin 𝕜 f s x

case neg
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
s : Set E
hxs : UniqueDiffWithinAt 𝕜 s x
h : ¬DifferentiableWithinAt 𝕜 f s x
⊢ fderivWithin 𝕜 (fun y ↦ -f y) s x = -fderivWithin 𝕜 f s x
Module: Mathlib.Analysis.Calculus.FDeriv.Add

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
x : E
c : F
⊢ fderiv 𝕜 (fun y ↦ f y - c) x = fderiv 𝕜 f x

Tactic:
by
  simp only [sub_eq_add_neg, fderiv_add_const]

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

Goal state before:
pp: case step
𝕜 : 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 : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
k m : ℕ
hf : HasFTaylorSeriesUpTo n f p
l : ℕ
h : k.le l
ih : ↑l ≤ n → (tsupport fun x ↦ p x l) ⊆ tsupport fun x ↦ p x k
h2 : ↑l.succ ≤ n
hl : ↑l < n
x : E [×l.succ]→L[𝕜] F
⊢ x.curryLeft = 0 ↔ x = 0

Tactic:
exact (continuousMultilinearCurryLeftEquiv _ _ _).map_eq_zero_iff (x := x)

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

Goal state before:
pp: case succ
𝕜 : 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 : ℕ
IH : tsupport (iteratedFDeriv 𝕜 n f) ⊆ tsupport f
⊢ tsupport (iteratedFDeriv 𝕜 (n + 1) f) ⊆ tsupport f

Tactic:
iteratedFDeriv_succ_eq_comp_left

Goal state after:
case succ
𝕜 : 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 : ℕ
IH : tsupport (iteratedFDeriv 𝕜 n f) ⊆ tsupport f
⊢ tsupport (⇑(continuousMultilinearCurryLeftEquiv 𝕜 (fun x ↦ E) F).symm ∘ fderiv 𝕜 (iteratedFDeriv 𝕜 n f)) ⊆ tsupport f
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
f : E → F
s : Set E
inst✝ : CompleteSpace F
h : AnalyticOnNhd 𝕜 f s
n : ℕ
IH : AnalyticOnNhd 𝕜 (iteratedFDeriv 𝕜 n f) s
⊢ AnalyticOnNhd 𝕜 (iteratedFDeriv 𝕜 (n + 1) f) s

Tactic:
iteratedFDeriv_succ_eq_comp_left

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
f : E → F
s : Set E
inst✝ : CompleteSpace F
h : AnalyticOnNhd 𝕜 f s
n : ℕ
IH : AnalyticOnNhd 𝕜 (iteratedFDeriv 𝕜 n f) s
⊢ AnalyticOnNhd 𝕜 (⇑(continuousMultilinearCurryLeftEquiv 𝕜 (fun x ↦ E) F).symm ∘ fderiv 𝕜 (iteratedFDeriv 𝕜 n f)) s
Module: Mathlib.Analysis.Calculus.FDeriv.Analytic

Goal state before:
pp: case refine_1
𝕜 : 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
inst✝ : CompleteSpace F
n : WithTop ℕ∞
h : AnalyticOnNhd 𝕜 f s
m : ℕ
_hm : ↑m < n
x : E
hx : x ∈ s
⊢ HasFDerivWithinAt (fun x ↦ ftaylorSeries 𝕜 f x m) (ftaylorSeries 𝕜 f x m.succ).curryLeft s x

pp: case refine_2
𝕜 : 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
inst✝ : CompleteSpace F
n : WithTop ℕ∞
h : AnalyticOnNhd 𝕜 f s
m : ℕ
_hm : ↑m ≤ n
x : E
hx : x ∈ s
⊢ ContinuousWithinAt (fun x ↦ ftaylorSeries 𝕜 f x m) s x

Tactic:
· apply HasFDerivAt.hasFDerivWithinAt
    exact ((h.iteratedFDeriv m x hx).differentiableAt).hasFDerivAt

Goal state after:
case refine_2
𝕜 : 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
inst✝ : CompleteSpace F
n : WithTop ℕ∞
h : AnalyticOnNhd 𝕜 f s
m : ℕ
_hm : ↑m ≤ n
x : E
hx : x ∈ s
⊢ ContinuousWithinAt (fun x ↦ ftaylorSeries 𝕜 f x m) s x
Module: Mathlib.Analysis.Calculus.Deriv.Mul

Goal state before:
pp: case e'_9
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝔸 : Type u_3
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸
d : 𝕜 → 𝔸
d' c : 𝔸
hd : HasDerivWithinAt d d' s x
⊢ c * d' = 0 * d x + c * d'

Tactic:
rw [zero_mul, zero_add]

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

Goal state before:
pp: case e'_9
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
𝔸 : Type u_3
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸
d : 𝕜 → 𝔸
d' c : 𝔸
hd : HasStrictDerivAt d d' x
⊢ c * d' = 0 * d x + c * d'

Tactic:
rw [zero_mul, zero_add]

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
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
h : CPolynomialOn 𝕜 f s
n : ℕ
IH : CPolynomialOn 𝕜 (_root_.iteratedFDeriv 𝕜 n f) s
⊢ CPolynomialOn 𝕜 (_root_.iteratedFDeriv 𝕜 (n + 1) f) s

Tactic:
iteratedFDeriv_succ_eq_comp_left

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
f : E → F
s : Set E
h : CPolynomialOn 𝕜 f s
n : ℕ
IH : CPolynomialOn 𝕜 (_root_.iteratedFDeriv 𝕜 n f) s
⊢ CPolynomialOn 𝕜
    (⇑(continuousMultilinearCurryLeftEquiv 𝕜 (fun x ↦ E) F).symm ∘ _root_.fderiv 𝕜 (_root_.iteratedFDeriv 𝕜 n f)) s
Module: Mathlib.LinearAlgebra.AffineSpace.Slope

Goal state before:
pp: case pos
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : Field k
inst✝² : AddCommGroup E
inst✝¹ : Module k E
inst✝ : AddTorsor E PE
f : k → PE
a b c : k
hab : a = b
⊢ ((b - a) / (c - a)) • slope f a b + ((c - b) / (c - a)) • slope f b c = slope f a c

Tactic:
subst hab
    rw [sub_self, zero_div, zero_smul, zero_add]
    by_cases hac : a = c
    · simp [hac]
    · rw [div_self (sub_ne_zero.2 <| Ne.symm hac), one_smul]

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

Goal state before:
pp: k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : Field k
inst✝² : AddCommGroup E
inst✝¹ : Module k E
inst✝ : AddTorsor E PE
f : k → PE
a b c : k
h : a ≠ c
⊢ (lineMap (slope f a b) (slope f b c)) ((c - b) / (c - a)) = slope f a c

Tactic:
simp only [lineMap_apply_module, ← sub_div_sub_smul_slope_add_sub_div_sub_smul_slope f a b c,
    add_left_inj]
  match_scalars
  field [sub_ne_zero.2 h.symm]

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

Goal state before:
pp: case neg.h
𝕜 : 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
n : ℕ
x v : (i : ι) → E i
m : Fin n → (i : ι) → E i
e : Fin n.succ ↪ ι
k : ι
hkf : k ∉ range ⇑((Equiv.embeddingFinSucc n ι) e).fst
hke : ⟨k, ⋯⟩ = ((Equiv.embeddingFinSucc n ι) e).snd
⊢ k ∈ range ⇑e

Tactic:
show k = _ from Subtype.ext_iff.1 hke,

Goal state after:
case neg.h
𝕜 : 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
n : ℕ
x v : (i : ι) → E i
m : Fin n → (i : ι) → E i
e : Fin n.succ ↪ ι
k : ι
hkf : k ∉ range ⇑((Equiv.embeddingFinSucc n ι) e).fst
hke : ⟨k, ⋯⟩ = ((Equiv.embeddingFinSucc n ι) e).snd
⊢ ↑((Equiv.embeddingFinSucc n ι) e).snd ∈ range ⇑e
Module: Mathlib.Analysis.Analytic.Uniqueness

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
inst✝ : CompleteSpace F
f : E → F
U : Set E
hf : AnalyticOnNhd 𝕜 f U
hU : IsPreconnected U
z₀ : E
h₀ : z₀ ∈ U
hfz₀ : f =ᶠ[𝓝 z₀] 0
⊢ EqOn f 0 U

Tactic:
by
  /- Let `u` be the set of points around which `f` vanishes. It is clearly open. We have to show
    that its limit points in `U` still belong to it, from which the inclusion `U ⊆ u` will follow
    by connectedness. -/
  let u := {x | f =ᶠ[𝓝 x] 0}
  suffices main : closure u ∩ U ⊆ u by
    have Uu : U ⊆ u :=
      hU.subset_of_closure_inter_subset isOpen_setOfPred_eventually_nhds ⟨z₀, h₀, hfz₀⟩ main
    intro z hz
    simpa using mem_of_mem_nhds (Uu hz)
  /- Take a limit point `x`, then a ball `B (x, r)` on which it has a power series expansion, and
    then `y ∈ B (x, r/2) ∩ u`. Then `f` has a power series expansion on `B (y, r/2)` as it is
    contained in `B (x, r)`. All the coefficients in this series expansion vanish, as `f` is zero
    on a neighborhood of `y`. Therefore, `f` is zero on `B (y, r/2)`. As this ball contains `x`,
    it follows that `f` vanishes on a neighborhood of `x`, proving the claim. -/
  rintro x ⟨xu, xU⟩
  rcases hf x xU with ⟨p, r, hp⟩
  obtain ⟨y, yu, hxy⟩ : ∃ y ∈ u, edist x y < r / 2 :=
    EMetric.mem_closure_iff.1 xu (r / 2) (ENNReal.half_pos hp.r_pos.ne')
  let q := p.changeOrigin (y - x)
  have has_series : HasFPowerSeriesOnBall f q y (r / 2) := by
    have A : (‖y - x‖₊ : ℝ≥0∞) < r / 2 := by rwa [edist_comm, edist_eq_enorm_sub] at hxy
    have := hp.changeOrigin (A.trans_le ENNReal.half_le_self)
    simp only [add_sub_cancel] at this
    apply this.mono (ENNReal.half_pos hp.r_pos.ne')
    apply ENNReal.le_sub_of_add_le_left ENNReal.coe_ne_top
    apply (add_le_add A.le (le_refl (r / 2))).trans (le_of_eq _)
    exact ENNReal.add_halves _
  have M : Metric.eball y (r / 2) ∈ 𝓝 x := Metric.isOpen_eball.mem_nhds hxy
  filter_upwards [M] with z hz
  have A : HasSum (fun n : ℕ => q n fun _ : Fin n => z - y) (f z) := has_series.hasSum_sub hz
  have B : HasSum (fun n : ℕ => q n fun _ : Fin n => z - y) 0 := by
    have : HasFPowerSeriesAt 0 q y := has_series.hasFPowerSeriesAt.congr yu
    convert! hasSum_zero (α := F) using 1
    ext n
    exact this.apply_eq_zero n _
  exact HasSum.unique A B

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

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
𝕜' : Type u_5
inst✝⁴ : NormedRing 𝕜'
inst✝³ : NormedAlgebra 𝕜 𝕜'
inst✝² : Module 𝕜' F
inst✝¹ : IsBoundedSMul 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
c : E → 𝕜'
c' : E →L[𝕜] 𝕜'
hc : HasFDerivAt c c' x
hf : HasFDerivAt f f' x
⊢ HasFDerivAt (c • f) (c x • f' + c'.smulRight (f x)) x

Tactic:
exact (isBoundedBilinearMap_smul.hasFDerivAt (𝕜 := 𝕜) (c x, f x)).comp x <| hc.prodMk hf

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
ι : Type u_5
𝔸 : Type u_6
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸
f : ι → E → 𝔸
f' : ι → E →L[𝕜] 𝔸
l : List ι
x : E
h : ∀ i ∈ l, HasStrictFDerivAt (fun x ↦ f i x) (f' i) x
⊢ HasStrictFDerivAt (fun x ↦ (List.map (fun x_1 ↦ f x_1 x) l).prod)
    (∑ i,
      (List.map (fun x_1 ↦ f x_1 x) (List.take (↑i) l)).prod •>
        (f' l[i] <• (List.map (fun x_1 ↦ f x_1 x) (List.drop (↑i).succ l)).prod))
    x

Tactic:
by
  simp_rw [Fin.getElem_fin, ← l.get_eq_getElem, ← List.map_get_finRange l, List.map_map]
  -- After https://github.com/leanprover-community/mathlib4/issues/19108, we have to be optimistic with `:)`s; otherwise Lean decides it need to find
  -- `NormedAddCommGroup (List 𝔸)` which is nonsense.
  refine .congr_fderiv (hasStrictFDerivAt_list_prod_finRange'.comp x
    (hasStrictFDerivAt_pi.mpr fun i ↦ h (l.get i) (List.getElem_mem ..)) :) ?_
  ext m
  simp_rw [List.map_take, List.map_drop, List.map_map, comp_apply, sum_apply, smul_apply,
    proj_apply, pi_apply, Function.comp_def]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
R : Type u_5
inst✝² : NormedRing R
inst✝¹ : HasSummableGeomSeries R
inst✝ : NormedAlgebra 𝕜 R
x : Rˣ
⊢ HasStrictFDerivAt Ring.inverse (-((mulLeftRight 𝕜 R) ↑x⁻¹) ↑x⁻¹) ↑x

Tactic:
convert! (analyticAt_inverse (𝕜 := 𝕜) x).hasStrictFDerivAt
  exact (fderiv_inverse x).symm

Goal state after:
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:
ContinuousLinearMap.toSpanSingleton_pow

Goal state after:
𝕜 : 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
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:
ContinuousLinearMap.toSpanSingleton_pow

Goal state after:
𝕜 : 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
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:
ContinuousLinearMap.toSpanSingleton_pow

Goal state after:
𝕜 : 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
Module: Mathlib.Analysis.Calculus.MeanValue

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
f' : ℝ → E
C : ℝ
hf : ∀ x ∈ Icc a b, HasDerivWithinAt f (f' x) (Icc a b) x
bound : ∀ x ∈ Ico a b, ‖f' x‖ ≤ C
x : ℝ
hx : x ∈ Ico a b
⊢ HasDerivWithinAt f (f' x) (Ici x) x

Tactic:
exact (hf x <| Ico_subset_Icc_self hx).mono_of_mem_nhdsWithin (Icc_mem_nhdsGE_of_mem hx)

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

Goal state before:
pp: case inr
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
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hs' : IsPreconnected s
hf : DifferentiableOn 𝕜 f s
hf' : EqOn (fderiv 𝕜 f) 0 s
y : E
hy : y ∈ s
x : E
hx : x ∈ s
h₁ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s ∩ f ⁻¹' {f y})
h₂ : Continuous[instTopologicalSpaceSubtype, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (f ∘ Subtype.val)
⊢ f x = f y

Tactic:
by_contra h₃

Goal state after:
case inr
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
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hs' : IsPreconnected s
hf : DifferentiableOn 𝕜 f s
hf' : EqOn (fderiv 𝕜 f) 0 s
y : E
hy : y ∈ s
x : E
hx : x ∈ s
h₁ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s ∩ f ⁻¹' {f y})
h₂ : Continuous[instTopologicalSpaceSubtype, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (f ∘ Subtype.val)
h₃ : ¬f x = f y
⊢ False
Module: Mathlib.Analysis.Calculus.ContDiff.Basic

Goal state before:
pp: case succ
𝕜 : 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
g : F ≃L[𝕜] G
f : E → F
hs : UniqueDiffOn 𝕜 s
i : ℕ
IH :
  ∀ {x : E},
    x ∈ s → iteratedFDerivWithin 𝕜 i (⇑g ∘ f) s x = (↑g).compContinuousMultilinearMap (iteratedFDerivWithin 𝕜 i f s x)
x : E
hx : x ∈ s
m : Fin (i + 1) → E
⊢ (iteratedFDerivWithin 𝕜 (i + 1) (⇑g ∘ f) s x) m =
    ((↑g).compContinuousMultilinearMap (iteratedFDerivWithin 𝕜 (i + 1) f s x)) m

Tactic:
| succ i IH =>

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

Goal state before:
pp: case succ
𝕜 : 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
g : G ≃L[𝕜] E
f : E → F
hs : UniqueDiffOn 𝕜 s
i : ℕ
IH :
  ∀ {x : G},
    g x ∈ s →
      iteratedFDerivWithin 𝕜 i (f ∘ ⇑g) (⇑g ⁻¹' s) x =
        (iteratedFDerivWithin 𝕜 i f s (g x)).compContinuousLinearMap fun x ↦ ↑g
x : G
hx : g x ∈ s
m : Fin (i + 1) → G
⊢ (iteratedFDerivWithin 𝕜 (i + 1) (f ∘ ⇑g) (⇑g ⁻¹' s) x) m =
    ((iteratedFDerivWithin 𝕜 (i + 1) f s (g x)).compContinuousLinearMap fun x ↦ ↑g) m

Tactic:
| succ i IH =>

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✝ : ℕ∞ω
n : ℕ∞
⊢ ContDiffWithinAt 𝕜 (↑n) f (insert x s) x ↔ ContDiffWithinAt 𝕜 (↑n) f s x

Tactic:
ContDiffWithinAt,

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
x : E
n✝ : ℕ∞ω
n : ℕ∞
⊢ (∀ (m : ℕ), ↑m ≤ n → ∃ u ∈ 𝓝[insert x (insert x s)] x, ∃ p, HasFTaylorSeriesUpToOn (↑m) f p u) ↔
    ∀ (m : ℕ), ↑m ≤ n → ∃ u ∈ 𝓝[insert x s] x, ∃ p, HasFTaylorSeriesUpToOn (↑m) f p u
Module: Mathlib.Analysis.Calculus.ContDiff.Defs

Goal state before:
pp: 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
m : ℕ∞ω
hm : m ≤ ω
h' : m = ∞ → ω = ω
h : ContDiffWithinAt 𝕜 ω f s x
⊢ ∃ u, IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u ∧ x ∈ u ∧ ContDiffOn 𝕜 m f (insert x s ∩ u)

Tactic:
obtain ⟨t, ht, p, hp, h'p⟩ := h
    rcases mem_nhdsWithin.1 ht with ⟨u, huo, hxu, hut⟩
    rw [inter_comm] at hut
    refine ⟨u, huo, hxu, ?_⟩
    suffices ContDiffOn 𝕜 ω f (insert x s ∩ u) from this.of_le le_top
    intro y hy
    refine ⟨insert x s ∩ u, ?_, p, hp.mono hut, fun i ↦ (h'p i).mono hut⟩
    simp only [insert_eq_of_mem, hy, self_mem_nhdsWithin]

Goal state after: