mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Calculus.Deriv.Mul

Goal state before:
pp: 𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
𝕜' : Type u_2
inst✝¹ : NormedDivisionRing 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
v : 𝕜 → 𝕜'
u : 𝕜'
⊢ deriv (fun y ↦ u * v y) x = u * deriv v x

Tactic:
by
  simpa only [← derivWithin_univ] using derivWithin_const_mul_field u

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
inst✝ : CompleteSpace F
h : AnalyticAt 𝕜 f x
⊢ AnalyticAt 𝕜 (deriv f) x

Tactic:
by
  obtain ⟨r, hr, h⟩ := h.exists_ball_analyticOnNhd
  exact h.deriv x (by simp [hr])

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

Goal state before:
pp: case e'_12.hl.e_f
𝕜 : 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 ι
inst✝ : DecidableEq ι
fa : ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)
f : ContinuousMultilinearMap 𝕜 (fun x ↦ ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)) F :=
  (ContinuousLinearMap.id 𝕜 (ContinuousMultilinearMap 𝕜 E F)).continuousMultilinearMapOption
Hf :
  HasStrictFDerivAt (fun x ↦ f fun x_1 ↦ x)
    ((f.linearDeriv fun x ↦ fa) ∘SL
      ContinuousLinearMap.pi fun x ↦ ContinuousLinearMap.id 𝕜 (ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)))
    fa
e_4✝ : Prod.instAddCommGroup = Prod.normedAddCommGroup.toAddCommGroup
e_5✝ : Prod.instModule ≍ Prod.normedSpace.toModule
e_6✝ : instTopologicalSpaceProd = PseudoMetricSpace.toUniformSpace.toTopologicalSpace
g : ContinuousMultilinearMap 𝕜 E F
i : ι
⊢ fa.1 (Function.update fa.2 i 0) = fa.1 fun j ↦ (Function.update (fun x ↦ fa) (some i) (g, 0) (some j)).2 j

Tactic:
congr with j

Goal state after:
case e'_12.hl.e_f.e_6
𝕜 : 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 ι
inst✝ : DecidableEq ι
fa : ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)
f : ContinuousMultilinearMap 𝕜 (fun x ↦ ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)) F :=
  (ContinuousLinearMap.id 𝕜 (ContinuousMultilinearMap 𝕜 E F)).continuousMultilinearMapOption
Hf :
  HasStrictFDerivAt (fun x ↦ f fun x_1 ↦ x)
    ((f.linearDeriv fun x ↦ fa) ∘SL
      ContinuousLinearMap.pi fun x ↦ ContinuousLinearMap.id 𝕜 (ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)))
    fa
e_4✝ : Prod.instAddCommGroup = Prod.normedAddCommGroup.toAddCommGroup
e_5✝ : Prod.instModule ≍ Prod.normedSpace.toModule
e_6✝ : instTopologicalSpaceProd = PseudoMetricSpace.toUniformSpace.toTopologicalSpace
g : ContinuousMultilinearMap 𝕜 E F
i j : ι
⊢ Function.update fa.2 i 0 j = (Function.update (fun x ↦ fa) (some i) (g, 0) (some j)).2 j
Module: Mathlib.Analysis.Calculus.FDeriv.Analytic

Goal state before:
pp: case hr.e_f
𝕜 : 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 ι
inst✝ : DecidableEq ι
fa : ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)
f : ContinuousMultilinearMap 𝕜 (fun x ↦ ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)) F :=
  (ContinuousLinearMap.id 𝕜 (ContinuousMultilinearMap 𝕜 E F)).continuousMultilinearMapOption
Hf :
  HasStrictFDerivAt (fun x ↦ f fun x_1 ↦ x)
    ((f.linearDeriv fun x ↦ fa) ∘SL
      ContinuousLinearMap.pi fun x ↦ ContinuousLinearMap.id 𝕜 (ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)))
    fa
e_4✝ : Prod.instAddCommGroup = Prod.normedAddCommGroup.toAddCommGroup
e_5✝ : Prod.instModule ≍ Prod.normedSpace.toModule
e_6✝ : instTopologicalSpaceProd = PseudoMetricSpace.toUniformSpace.toTopologicalSpace
g : (i : ι) → E i
i : ι
⊢ fa.1 (Function.update fa.2 i (g i)) = fa.1 fun i_1 ↦ (Function.update (fun x ↦ fa) (some i) (0, g) (some i_1)).2 i_1

Tactic:
congr with j

Goal state after:
case hr.e_f.e_6
𝕜 : 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 ι
inst✝ : DecidableEq ι
fa : ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)
f : ContinuousMultilinearMap 𝕜 (fun x ↦ ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)) F :=
  (ContinuousLinearMap.id 𝕜 (ContinuousMultilinearMap 𝕜 E F)).continuousMultilinearMapOption
Hf :
  HasStrictFDerivAt (fun x ↦ f fun x_1 ↦ x)
    ((f.linearDeriv fun x ↦ fa) ∘SL
      ContinuousLinearMap.pi fun x ↦ ContinuousLinearMap.id 𝕜 (ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)))
    fa
e_4✝ : Prod.instAddCommGroup = Prod.normedAddCommGroup.toAddCommGroup
e_5✝ : Prod.instModule ≍ Prod.normedSpace.toModule
e_6✝ : instTopologicalSpaceProd = PseudoMetricSpace.toUniformSpace.toTopologicalSpace
g : (i : ι) → E i
i j : ι
⊢ Function.update fa.2 i (g i) j = (Function.update (fun x ↦ fa) (some i) (0, g) (some j)).2 j
Module: Mathlib.Analysis.Calculus.FDeriv.Analytic

Goal state before:
pp: case pos
𝕜 : 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 : ι
hke : k ∈ range ⇑e
hkf : k ∈ range ⇑((Equiv.embeddingFinSucc n ι) e).fst
⊢ Fin.cons v m (e.toEquivRange.symm ⟨k, ⋯⟩) k = m (((Equiv.embeddingFinSucc n ι) e).fst.toEquivRange.symm ⟨k, hkf⟩) k

Tactic:
simp only [← Equiv.succ_embeddingFinSucc_fst_symm_apply e hkf hke, Fin.cons_succ]

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

Goal state before:
pp: case neg
𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : OrderTopology 𝕜
g : 𝕜 → 𝕜
hg : MonotoneOn g s
hd : DifferentiableWithinAt 𝕜 g s x
hx : ¬AccPt x (𝓟 s)
⊢ 0 ≤ derivWithin g s x

pp: case pos
𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : OrderTopology 𝕜
g : 𝕜 → 𝕜
hg : MonotoneOn g s
hd : DifferentiableWithinAt 𝕜 g s x
hx : AccPt x (𝓟 s)
⊢ 0 ≤ derivWithin g s x

Tactic:
· simp [derivWithin_zero_of_not_accPt hx]

Goal state after:
case pos
𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : OrderTopology 𝕜
g : 𝕜 → 𝕜
hg : MonotoneOn g s
hd : DifferentiableWithinAt 𝕜 g s x
hx : AccPt x (𝓟 s)
⊢ 0 ≤ derivWithin g s x
Module: Mathlib.Analysis.Calculus.FDeriv.Mul

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
R : Type u_5
inst✝¹ : NormedDivisionRing R
inst✝ : NormedAlgebra 𝕜 R
s : Set R
x : R
hx : x ≠ 0
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ fderivWithin 𝕜 (fun x ↦ x⁻¹) s x = -((mulLeftRight 𝕜 R) x⁻¹) x⁻¹

Tactic:
rw [DifferentiableAt.fderivWithin (differentiableAt_inv hx) hxs]

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
R : Type u_5
inst✝¹ : NormedDivisionRing R
inst✝ : NormedAlgebra 𝕜 R
s : Set R
x : R
hx : x ≠ 0
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ fderiv 𝕜 Inv.inv x = -((mulLeftRight 𝕜 R) x⁻¹) x⁻¹
Module: Mathlib.Analysis.Analytic.IsolatedZeros

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f g : 𝕜 → E
z₀ : 𝕜
U : Set 𝕜
hf : AnalyticOnNhd 𝕜 f U
hg : AnalyticOnNhd 𝕜 g U
hU : IsPreconnected U
h₀ : z₀ ∈ U
hfg : ∃ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = g z
z : 𝕜
h : f z = g z
⊢ (f - g) z = 0

Tactic:
rw [Pi.sub_apply, h, sub_self]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
⊢ logDeriv id x = 1 / x

Tactic:
simp [logDeriv_apply]

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

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
a : 𝕜'
x✝ : 𝕜
⊢ logDeriv (fun x ↦ a) x✝ = 0 x✝

Tactic:
simp [logDeriv_apply]

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

Goal state before:
pp: case cons
𝕜 : Type u_1
𝕜' : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
ι : Type u_3
f : ι → 𝕜 → 𝕜'
x : 𝕜
a : ι
s : Finset ι
ha : a ∉ s
ih :
  (∀ i ∈ s, f i x ≠ 0) →
    (∀ i ∈ s, DifferentiableAt 𝕜 (f i) x) → logDeriv (fun x ↦ ∏ i ∈ s, f i x) x = ∑ i ∈ s, logDeriv (f i) x
hf : ∀ i ∈ Finset.cons a s ha, f i x ≠ 0
hd : ∀ i ∈ Finset.cons a s ha, DifferentiableAt 𝕜 (f i) x
⊢ logDeriv (fun x ↦ ∏ i ∈ Finset.cons a s ha, f i x) x = ∑ i ∈ Finset.cons a s ha, logDeriv (f i) x

Tactic:
rw [Finset.forall_mem_cons] at hf hd
    simp_rw [Finset.prod_cons, Finset.sum_cons]
    rw [logDeriv_mul, ih hf.2 hd.2]
    · exact hf.1
    · simpa [Finset.prod_eq_zero_iff] using hf.2
    · exact hd.1
    · exact .fun_finsetProd hd.2

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

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
f : 𝕜' → 𝕜'
g : 𝕜 → 𝕜'
x : 𝕜
hf : DifferentiableAt 𝕜' f (g x)
hg : DifferentiableAt 𝕜 g x
⊢ logDeriv (f ∘ g) x = logDeriv f (g x) * deriv g x

Tactic:
simp only [logDeriv, Pi.div_apply, deriv_comp _ hf hg, comp_apply]
  ring

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

Goal state before:
pp: f f' : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ x ∈ Ico a b, ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[>] x, slope f x z < r
B B' : ℝ → ℝ
ha : f a ≤ B a
hB : ContinuousOn B (Icc a b)
hB' : ∀ x ∈ Ico a b, HasDerivWithinAt B (B' x) (Ici x) x
bound : ∀ x ∈ Ico a b, f x = B x → f' x < B' x
s : Set ℝ := {x | f x ≤ B x} ∩ Icc a b
⊢ Icc a b ⊆ {x | f x ≤ B x}

Tactic:
have A : ContinuousOn (fun x => (f x, B x)) (Icc a b) := hf.prodMk hB

Goal state after:
f f' : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ x ∈ Ico a b, ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[>] x, slope f x z < r
B B' : ℝ → ℝ
ha : f a ≤ B a
hB : ContinuousOn B (Icc a b)
hB' : ∀ x ∈ Ico a b, HasDerivWithinAt B (B' x) (Ici x) x
bound : ∀ x ∈ Ico a b, f x = B x → f' x < B' x
s : Set ℝ := {x | f x ≤ B x} ∩ Icc a b
A : ContinuousOn (fun x ↦ (f x, B x)) (Icc a b)
⊢ Icc a b ⊆ {x | f x ≤ B x}
Module: Mathlib.Analysis.Calculus.MeanValue

Goal state before:
pp: f f' : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ x ∈ Ico a b, ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[>] x, slope f x z < r
B B' : ℝ → ℝ
ha : f a ≤ B a
hB : ContinuousOn B (Icc a b)
hB' : ∀ x ∈ Ico a b, HasDerivWithinAt B (B' x) (Ici x) x
bound : ∀ x ∈ Ico a b, f x = B x → f' x < B' x
s : Set ℝ := {x | f x ≤ B x} ∩ Icc a b
A : ContinuousOn (fun x ↦ (f x, B x)) (Icc a b)
this : IsClosed s
x : ℝ
hxB : f x ≤ B x
xab : x ∈ Ico a b
y : ℝ
hy : y ∈ Ioi x
⊢ ({x | f x ≤ B x} ∩ Ioc x y).Nonempty

Tactic:
rcases hxB.lt_or_eq with hxB | hxB

Goal state after:
case inl
f f' : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ x ∈ Ico a b, ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[>] x, slope f x z < r
B B' : ℝ → ℝ
ha : f a ≤ B a
hB : ContinuousOn B (Icc a b)
hB' : ∀ x ∈ Ico a b, HasDerivWithinAt B (B' x) (Ici x) x
bound : ∀ x ∈ Ico a b, f x = B x → f' x < B' x
s : Set ℝ := {x | f x ≤ B x} ∩ Icc a b
A : ContinuousOn (fun x ↦ (f x, B x)) (Icc a b)
this : IsClosed s
x : ℝ
hxB✝ : f x ≤ B x
xab : x ∈ Ico a b
y : ℝ
hy : y ∈ Ioi x
hxB : f x < B x
⊢ ({x | f x ≤ B x} ∩ Ioc x y).Nonempty

case inr
f f' : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ x ∈ Ico a b, ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[>] x, slope f x z < r
B B' : ℝ → ℝ
ha : f a ≤ B a
hB : ContinuousOn B (Icc a b)
hB' : ∀ x ∈ Ico a b, HasDerivWithinAt B (B' x) (Ici x) x
bound : ∀ x ∈ Ico a b, f x = B x → f' x < B' x
s : Set ℝ := {x | f x ≤ B x} ∩ Icc a b
A : ContinuousOn (fun x ↦ (f x, B x)) (Icc a b)
this : IsClosed s
x : ℝ
hxB✝ : f x ≤ B x
xab : x ∈ Ico a b
y : ℝ
hy : y ∈ Ioi x
hxB : f x = B x
⊢ ({x | f x ≤ B x} ∩ Ioc x y).Nonempty
Module: Mathlib.Analysis.Calculus.MeanValue

Goal state before:
pp: case hB
f : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
B B' : ℝ → ℝ
ha : f a ≤ B a
hB : ContinuousOn B (Icc a b)
hB' : ∀ x ∈ Ico a b, HasDerivWithinAt B (B' x) (Ici x) x
bound : ∀ x ∈ Ico a b, ∀ (r : ℝ), B' x < r → ∃ᶠ (z : ℝ) in 𝓝[>] x, slope f x z < r
x : ℝ
hx : x ∈ Icc a b
r : ℝ
hr : r > 0
⊢ ContinuousOn (fun x ↦ B x + r * (x - a)) (Icc a b)

Tactic:
exact hB.add (continuousOn_const.mul (continuousOn_id.sub continuousOn_const))

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

Goal state before:
pp: E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → G
C : ℝ
s : Set E
x y : E
f' : E → E →L[𝕜] G
hf : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
bound : ∀ x ∈ s, ‖f' x‖ ≤ C
hs : Convex ℝ s
xs : x ∈ s
ys : y ∈ s
this✝ : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this : NormedSpace ℝ G := NormedSpace.restrictScalars ℝ 𝕜 G
g : ℝ → E := ⇑(AffineMap.lineMap x y)
segm : MapsTo g (Icc 0 1) s
hD : ∀ t ∈ Icc 0 1, HasDerivWithinAt (f ∘ g) ((f' (g t)) (y - x)) (Icc 0 1) t
⊢ ‖f y - f x‖ ≤ C * ‖y - x‖

Tactic:
have bound : ∀ t ∈ Ico (0 : ℝ) 1, ‖f' (g t) (y - x)‖ ≤ C * ‖y - x‖ := fun t ht =>
    le_of_opNorm_le _ (bound _ <| segm <| Ico_subset_Icc_self ht) _

Goal state after:
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → G
C : ℝ
s : Set E
x y : E
f' : E → E →L[𝕜] G
hf : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
bound✝ : ∀ x ∈ s, ‖f' x‖ ≤ C
hs : Convex ℝ s
xs : x ∈ s
ys : y ∈ s
this✝ : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this : NormedSpace ℝ G := NormedSpace.restrictScalars ℝ 𝕜 G
g : ℝ → E := ⇑(AffineMap.lineMap x y)
segm : MapsTo g (Icc 0 1) s
hD : ∀ t ∈ Icc 0 1, HasDerivWithinAt (f ∘ g) ((f' (g t)) (y - x)) (Icc 0 1) t
bound : ∀ t ∈ Ico 0 1, ‖(f' (g t)) (y - x)‖ ≤ C * ‖y - x‖
⊢ ‖f y - f x‖ ≤ C * ‖y - x‖
Module: Mathlib.Analysis.Calculus.ContDiff.Basic

Goal state before:
pp: case refine_1
𝕜 : 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
f : E → F
n : ℕ∞ω
x : G
g : G →L[𝕜] E
u : Set E
hu : u ∈ 𝓝[insert (g x) s] g x
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn ω f p u
h'p : ∀ (i : ℕ), AnalyticOn 𝕜 (fun x ↦ p x i) u
⊢ ⇑g ⁻¹' u ∈ 𝓝[insert x (⇑g ⁻¹' s)] x

Tactic:
refine g.continuous.continuousWithinAt.tendsto_nhdsWithin ?_ hu
      exact (mapsTo_singleton.2 <| mem_singleton _).union_union (mapsTo_preimage _ _)

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

Goal state before:
pp: case refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f f' : ℝ → E
x₀ : ℝ
n : ℕ
s : Set ℝ
hs : Convex ℝ s
hx₀s : x₀ ∈ s
hff' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
hf' : f' =o[𝓝[s] x₀] fun x ↦ (x - x₀) ^ n
h : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : ℝ) in 𝓝[s] x₀, ‖f x - f x₀‖ ≤ c * ‖‖x - x₀‖ ^ (n + 1)‖
⊢ ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : ℝ) in 𝓝[s] x₀, ‖f x - f x₀‖ ≤ c * ‖(x - x₀) ^ (n + 1)‖

Tactic:
simpa using h

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

Goal state before:
pp: 𝕜 : Type u_3
inst✝⁴ : RCLike 𝕜
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
H : Type u_5
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace 𝕜 H
f : G → H
f' : G → G →L[𝕜] H
x : G
hder : ∀ᶠ (y : G) in 𝓝 x, HasFDerivAt f (f' y) y
hcont : ContinuousAt f' x
c : ℝ
hc : 0 < c
ε : ℝ
ε0 : ε > 0
hε : ball x ε ⊆ {x | (fun y ↦ HasFDerivAt f (f' y) y) x} ∩ f' ⁻¹' ball (f' x) c
a b : G
h : a ∈ ball x ε ∧ b ∈ ball x ε
x' : G
H' : x' ∈ ball x ε
⊢ dist (f' x') (f' x) ≤ c

Tactic:
exact le_of_lt (hε H').2

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
f : E → F
x : E
n : ℕ∞ω
e : G ≃L[𝕜] E
⊢ ContDiffWithinAt 𝕜 n (f ∘ ⇑e) (?m.94 ⁻¹' univ) (e.symm x) ↔ ContDiffWithinAt 𝕜 n f univ x

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
x : E
n : ℕ∞ω
e : G ≃L[𝕜] E
⊢ Type ?u.73

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
x : E
n : ℕ∞ω
e : G ≃L[𝕜] E
⊢ G → ?m.93

Tactic:
exact e.contDiffWithinAt_comp_iff

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 : ℕ
x✝³ : Fin n
x✝² : x✝³ ∈ univ
x✝¹ : Fin n
x✝ : x✝¹ ∈ univ
h : x✝³ ≠ x✝¹
⊢ (Disjoint on fun m ↦ range fun x ↦ m) x✝³ x✝¹

Tactic:
simpa using h

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 : ℕ
c✝ : OrderedFinpartition n
c : OrderedFinpartition 1
⊢ c = default

Tactic:
by
    have h₁ : c.length = 1 := le_antisymm c.length_le (c.length_pos Nat.zero_lt_one)
    have h₂ (i) : c.partSize i = 1 := le_antisymm (c.partSize_le _) (c.partSize_pos _)
    have h₃ (i j) : c.emb i j = 0 := Subsingleton.elim _ _
    rcases c with ⟨length, partSize, _, emb, _, _, _, _⟩
    subst h₁
    obtain rfl : partSize = fun _ ↦ 1 := funext h₂
    simpa [OrderedFinpartition.ext_iff, funext_iff, Fin.forall_fin_one] 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
s : Set E
f : E → F
x : E
m n : ℕ∞ω
hm : m ≤ n
h' : m = ∞ → n = ω
h : ContDiffWithinAt 𝕜 n f s x
⊢ ∃ u ∈ 𝓝[insert x s] x, u ⊆ insert x s ∧ ContDiffOn 𝕜 m f u

Tactic:
obtain ⟨_u, uo, xu, h⟩ := h.contDiffOn' hm h'
  exact ⟨_, inter_mem_nhdsWithin _ (uo.mem_nhds xu), inter_subset_left, h⟩

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

Goal state before:
pp: case inl
𝕜 : 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 ∈ univ
j : Fin c.length
hj : j ∈ univ
hij h : i ≠ j
⊢ (Disjoint on fun m ↦
      range
        (if h : m = j then
          have this := ⋯;
          (fun i ↦ cases 0 (succ ∘ c.emb j) i) ∘ Fin.cast this
        else
          have this := ⋯;
          succ ∘ c.emb m ∘ Fin.cast this))
    i j

Tactic:
simp only [onFun, ↓reduceDIte]

Goal state after:
case inl
𝕜 : 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 ∈ univ
j : Fin c.length
hj : j ∈ univ
hij h : i ≠ j
⊢ Disjoint
    (range (if h : i = j then (fun i ↦ cases 0 (succ ∘ c.emb j) i) ∘ Fin.cast ⋯ else succ ∘ c.emb i ∘ Fin.cast ⋯))
    (range ((fun i ↦ cases 0 (succ ∘ c.emb j) i) ∘ Fin.cast ⋯))
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
hf : DifferentiableOn 𝕜 f s
h' : ∞ = ω → AnalyticOn 𝕜 f s
h : ContDiffOn 𝕜 ∞ (fun y ↦ fderivWithin 𝕜 f s y) s
⊢ ContDiffOn 𝕜 (∞ + 1) f s

Tactic:
ENat.coe_top_add_one,

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
hf : DifferentiableOn 𝕜 f s
h' : ∞ = ω → AnalyticOn 𝕜 f s
h : ContDiffOn 𝕜 ∞ (fun y ↦ fderivWithin 𝕜 f s y) s
⊢ ContDiffOn 𝕜 ∞ f s
Module: Mathlib.Analysis.Calculus.ContDiff.Defs

Goal state before:
pp: 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
n : ℕ∞ω
hf : DifferentiableOn 𝕜 f s
h' : n = ω → AnalyticOn 𝕜 f s
h : ContDiffOn 𝕜 n (fun y ↦ fderivWithin 𝕜 f s y) s
hn : n ≠ ∞
x : E
hx : x ∈ s
⊢ ContDiffWithinAt 𝕜 (n + 1) f s x

Tactic:
rw [contDiffWithinAt_succ_iff_hasFDerivWithinAt hn,
      insert_eq_of_mem hx]

Goal state after:
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
n : ℕ∞ω
hf : DifferentiableOn 𝕜 f s
h' : n = ω → AnalyticOn 𝕜 f s
h : ContDiffOn 𝕜 n (fun y ↦ fderivWithin 𝕜 f s y) s
hn : n ≠ ∞
x : E
hx : x ∈ s
⊢ ∃ u ∈ 𝓝[s] x,
    (n = ω → AnalyticOn 𝕜 f u) ∧ ∃ f', (∀ x ∈ u, HasFDerivWithinAt f (f' x) u x) ∧ ContDiffWithinAt 𝕜 n f' u x
Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno

Goal state before:
pp: case e'_3.inr
𝕜 : 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✝ : OrderedFinpartition n
c : OrderedFinpartition (n + 1)
hc : range (c.emb 0) ≠ {0}
i j : Fin c.length
hij : i < j
hi : i ≠ c.index 0
⊢ ↑(if h : i = c.index 0 then
          (c.emb i (Fin.cast ⋯ ⟨update c.partSize (c.index 0) (c.partSize (c.index 0) - 1) i - 1, ⋯⟩.succ)).pred ⋯
        else (c.emb i (Fin.cast ⋯ ⟨update c.partSize (c.index 0) (c.partSize (c.index 0) - 1) i - 1, ⋯⟩)).pred ⋯) +
      1 =
    ↑((fun m ↦ c.emb m ⟨c.partSize m - 1, ⋯⟩) i)

Tactic:
simp only [hi, ↓reduceDIte, ne_eq, not_false_eq_true, update_of_ne, cast_mk, val_pred]
        apply Nat.sub_add_cancel
        have : c.emb i ⟨c.partSize i - 1, Nat.sub_one_lt_of_lt (c.partSize_pos i)⟩
            ≠ c.emb (c.index 0) 0 := c.emb_ne_emb_of_ne hi
        simp only [c.emb_zero, ne_eq, ← val_eq_val, val_zero] at this
        omega

Goal state after: