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

Goal state before:
pp: 𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
hx : x ≠ 0
this : (fun p ↦ (p.1 - p.2) * ((x * x)⁻¹ - (p.1 * p.2)⁻¹)) =o[𝓝 (x, x)] fun p ↦ (p.1 - p.2) * 1
⊢ ∀ (x_1 : 𝕜 × 𝕜),
    ({y | y ≠ 0} ×ˢ {y | y ≠ 0}) x_1 →
      (fun p ↦ (p.1 - p.2) * ((x * x)⁻¹ - (p.1 * p.2)⁻¹)) x_1 =
        (fun p ↦ p.1⁻¹ - p.2⁻¹ - (toSpanSingleton 𝕜 (-(x ^ 2)⁻¹)) (p.1 - p.2)) x_1

Tactic:
rintro ⟨y, z⟩ ⟨hy, hz⟩

Goal state after:
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
hx : x ≠ 0
this : (fun p ↦ (p.1 - p.2) * ((x * x)⁻¹ - (p.1 * p.2)⁻¹)) =o[𝓝 (x, x)] fun p ↦ (p.1 - p.2) * 1
y z : 𝕜
hy : (y, z).1 ∈ {y | y ≠ 0}
hz : (y, z).2 ∈ {y | y ≠ 0}
⊢ (fun p ↦ (p.1 - p.2) * ((x * x)⁻¹ - (p.1 * p.2)⁻¹)) (y, z) =
    (fun p ↦ p.1⁻¹ - p.2⁻¹ - (toSpanSingleton 𝕜 (-(x ^ 2)⁻¹)) (p.1 - p.2)) (y, z)
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_7
inst✝² : NormedCommRing 𝔸'
inst✝¹ : NormedAlgebra 𝕜 𝔸'
g : ι → E → 𝔸'
g' : ι → E →L[𝕜] 𝔸'
inst✝ : DecidableEq ι
u : Multiset ι
x : E
h : ∀ i ∈ u, HasFDerivAt (fun x ↦ g i x) (g' i) x
x✝ : E
⊢ ((Multiset.map (fun i ↦ (Multiset.map (fun i ↦ g (↑i) x) (u.attach.erase i)).prod •> proj i) u.attach).sum ∘SL
        pi fun i ↦ g' ↑i)
      x✝ =
    (Multiset.map
          ((fun x_1 ↦
              (Multiset.map (fun x_2 ↦ g x_2 x) ((Multiset.map Subtype.val u.attach).erase x_1)).prod •> g' x_1) ∘
            Subtype.val)
          u.attach).sum
      x✝

Tactic:
simp [Finset.sum_multiset_map_count, u.erase_attach_map (g · x)]

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
s : Set E
ι : Type u_5
𝔸' : Type u_7
inst✝² : NormedCommRing 𝔸'
inst✝¹ : NormedAlgebra 𝕜 𝔸'
g : ι → E → 𝔸'
g' : ι → E →L[𝕜] 𝔸'
inst✝ : DecidableEq ι
u : Multiset ι
x : E
h : ∀ i ∈ u, HasFDerivWithinAt (fun x ↦ g i x) (g' i) s x
x✝ : E
⊢ ((Multiset.map (fun i ↦ (Multiset.map (fun i ↦ g (↑i) x) (u.attach.erase i)).prod •> proj i) u.attach).sum ∘SL
        pi fun i ↦ g' ↑i)
      x✝ =
    (Multiset.map
          ((fun x_1 ↦
              (Multiset.map (fun x_2 ↦ g x_2 x) ((Multiset.map Subtype.val u.attach).erase x_1)).prod •> g' x_1) ∘
            Subtype.val)
          u.attach).sum
      x✝

Tactic:
simp [Finset.sum_multiset_map_count, u.erase_attach_map (g · x)]

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

Goal state before:
pp: 𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
𝕜' : Type u_1
inst✝³ : NontriviallyNormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
t' : Set 𝕜'
h : 𝕜 → 𝕜'
g₁ : 𝕜' → F
y : 𝕜'
hg : DifferentiableWithinAt 𝕜' g₁ t' (h x)
hh : DifferentiableWithinAt 𝕜 h s x
hs : MapsTo h s t'
hy : y = h x
⊢ derivWithin (g₁ ∘ h) s x = derivWithin h s x • derivWithin g₁ t' (h x)

Tactic:
exact derivWithin.scomp x hg hh hs

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

Goal state before:
pp: 𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
h₂ : 𝕜' → 𝕜'
h₂' y : 𝕜'
f : E → 𝕜'
f' : E →L[𝕜] 𝕜'
x : E
hh : HasStrictDerivAt h₂ h₂' y
hf : HasStrictFDerivAt f f' x
hy : y = f x
⊢ HasStrictFDerivAt (h₂ ∘ f) (h₂' • f') x

Tactic:
rw [hy] at hh; exact hh.comp_hasStrictFDerivAt x hf

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

Goal state before:
pp: case e'_9
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
m : ℤ
x : 𝕜
h : x ≠ 0 ∨ 0 ≤ m
this✝ : ∀ (m : ℤ), 0 < m → HasStrictDerivAt (fun x ↦ x ^ m) (↑m * x ^ (m - 1)) x
hm : m < 0
hx : x ≠ 0
this : HasStrictDerivAt (fun x ↦ x ^ m) (↑(-m) * x ^ (-m - 1) * -((x ^ m)⁻¹ ^ 2)⁻¹) x
⊢ ↑m * x ^ (m - 1) = ↑m * (x ^ (-m - 1) * x ^ (m + m))

Tactic:
←
      zpow_add₀ hx

Goal state after:
case e'_9
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
m : ℤ
x : 𝕜
h : x ≠ 0 ∨ 0 ≤ m
this✝ : ∀ (m : ℤ), 0 < m → HasStrictDerivAt (fun x ↦ x ^ m) (↑m * x ^ (m - 1)) x
hm : m < 0
hx : x ≠ 0
this : HasStrictDerivAt (fun x ↦ x ^ m) (↑(-m) * x ^ (-m - 1) * -((x ^ m)⁻¹ ^ 2)⁻¹) x
⊢ ↑m * x ^ (m - 1) = ↑m * x ^ (-m - 1 + (m + m))
Module: Mathlib.Analysis.Analytic.IsolatedZeros

Goal state before:
pp: case h
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
s : Set E
hfx : AnalyticAt 𝕜 f x
hs : s ∈ 𝓝[≠] f x
this : ∀ᶠ (z : 𝕜) in 𝓝 x, f z ∈ insert (f x) s
h : ¬f ⁻¹' s ∈ 𝓝[≠] x
⊢ ∀ (x_1 : 𝕜), (f x_1 ∈ s → False) ∧ f x_1 ∈ insert (f x) s → f x_1 = f x

Tactic:
intro z

Goal state after:
case h
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
s : Set E
hfx : AnalyticAt 𝕜 f x
hs : s ∈ 𝓝[≠] f x
this : ∀ᶠ (z : 𝕜) in 𝓝 x, f z ∈ insert (f x) s
h : ¬f ⁻¹' s ∈ 𝓝[≠] x
z : 𝕜
⊢ (f z ∈ s → False) ∧ f z ∈ insert (f x) s → f z = f x
Module: Mathlib.Analysis.Calculus.LogDeriv

Goal state before:
pp: 𝕜 : 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
⊢ EqOn (deriv (f * g⁻¹)) (deriv f * g⁻¹ - f * deriv g / g ^ 2) s

Tactic:
intro z

Goal state after:
𝕜 : 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
z : 𝕜
⊢ z ∈ s → deriv (f * g⁻¹) z = (deriv f * g⁻¹ - f * deriv g / g ^ 2) z
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
s : Set E
x : E
f' : E → E →L[𝕜] G
hs : Convex ℝ s
f : E → G
hder : ∀ᶠ (y : E) in 𝓝[s] x, HasFDerivWithinAt f (f' y) s y
hcont : ContinuousWithinAt f' s x
K : ℝ≥0
hK : ‖f' x‖₊ < K
⊢ ∃ t ∈ 𝓝[s] x, LipschitzOnWith K f t

Tactic:
obtain ⟨ε, ε0, hε⟩ : ∃ ε > 0,
      ball x ε ∩ s ⊆ { y | HasFDerivWithinAt f (f' y) s y ∧ ‖f' y‖₊ < K } :=
    mem_nhdsWithin_iff.1 (hder.and <| hcont.nnnorm.eventually (gt_mem_nhds hK))

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
s : Set E
x : E
f' : E → E →L[𝕜] G
hs : Convex ℝ s
f : E → G
hder : ∀ᶠ (y : E) in 𝓝[s] x, HasFDerivWithinAt f (f' y) s y
hcont : ContinuousWithinAt f' s x
K : ℝ≥0
hK : ‖f' x‖₊ < K
ε : ℝ
ε0 : ε > 0
hε : ball x ε ∩ s ⊆ {y | HasFDerivWithinAt f (f' y) s y ∧ ‖f' y‖₊ < K}
⊢ ∃ t ∈ 𝓝[s] x, LipschitzOnWith K f t
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 g : E → G
s : Set E
x : E
hs : Convex ℝ s
hf : DifferentiableOn 𝕜 f s
hg : DifferentiableOn 𝕜 g s
hs' : UniqueDiffOn 𝕜 s
hf' : EqOn (fderivWithin 𝕜 f s) (fderivWithin 𝕜 g s) s
hx : x ∈ s
hfgx : f x = g x
y : E
hy : y ∈ s
this : f x - g x = f y - g y
⊢ f y = g y

Tactic:
hfgx,

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 g : E → G
s : Set E
x : E
hs : Convex ℝ s
hf : DifferentiableOn 𝕜 f s
hg : DifferentiableOn 𝕜 g s
hs' : UniqueDiffOn 𝕜 s
hf' : EqOn (fderivWithin 𝕜 f s) (fderivWithin 𝕜 g s) s
hx : x ∈ s
hfgx : f x = g x
y : E
hy : y ∈ s
this : g x - g x = f y - g y
⊢ f y = g y
Module: Mathlib.Analysis.Calculus.MeanValue

Goal state before:
pp: case refine_1
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
hf : DifferentiableOn 𝕜 f s
hf' : EqOn (fderiv 𝕜 f) 0 s
t : Set G
y : E
x✝ : y ∈ s ∩ f ⁻¹' t
hy : y ∈ s
hy' : y ∈ f ⁻¹' t
r : ℝ
hr : r > 0
h : ball y r ⊆ s
x : E
hx : x ∈ ball y r
⊢ ∀ x ∈ ball y r, fderivWithin 𝕜 f (ball y r) x = 0

Tactic:
intro z

Goal state after:
case refine_1
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
hf : DifferentiableOn 𝕜 f s
hf' : EqOn (fderiv 𝕜 f) 0 s
t : Set G
y : E
x✝ : y ∈ s ∩ f ⁻¹' t
hy : y ∈ s
hy' : y ∈ f ⁻¹' t
r : ℝ
hr : r > 0
h : ball y r ⊆ s
x : E
hx : x ∈ ball y r
z : E
⊢ z ∈ ball y r → fderivWithin 𝕜 f (ball y r) z = 0
Module: Mathlib.Analysis.Calculus.ContDiff.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
n : ℕ
c : F
⊢ iteratedFDerivWithin 𝕜 (n + 1) (fun x ↦ c) s = 0

Tactic:
by
  induction n with
  | zero =>
    ext1
    simp [iteratedFDerivWithin_succ_eq_comp_left, iteratedFDerivWithin_zero_eq_comp, comp_def]
  | succ n IH =>
    rw [iteratedFDerivWithin_succ_eq_comp_left, IH]
    simp only [Pi.zero_def, comp_def, fderivWithin_fun_const, map_zero]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
n : ℕ∞ω
f : E → F → G
g : E → F
t : Set F
hn : n ≠ ∞
x₀ : E
hf : ContDiffWithinAt 𝕜 (n + 1) (uncurry f) (insert x₀ s ×ˢ t) (x₀, g x₀)
hg : ContDiffWithinAt 𝕜 n g s x₀
hgt : t ∈ 𝓝[g '' s] g x₀
⊢ s ⊆ insert x₀ s ∧ s ⊆ g ⁻¹' g '' s

Tactic:
subset_insert,

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
s : Set E
n : ℕ∞ω
f : E → F → G
g : E → F
t : Set F
hn : n ≠ ∞
x₀ : E
hf : ContDiffWithinAt 𝕜 (n + 1) (uncurry f) (insert x₀ s ×ˢ t) (x₀, g x₀)
hg : ContDiffWithinAt 𝕜 n g s x₀
hgt : t ∈ 𝓝[g '' s] g x₀
⊢ True ∧ s ⊆ g ⁻¹' g '' s
Module: Mathlib.Analysis.Calculus.ContDiff.Comp

Goal state before:
pp: case refine_2
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
n : ℕ∞ω
f : E → F → G
g : E → F
t : Set F
hn : n ≠ ∞
x₀ : E
hf : ContDiffWithinAt 𝕜 (n + 1) (uncurry f) (insert x₀ s ×ˢ t) (x₀, g x₀)
hg : ContDiffWithinAt 𝕜 n g s x₀
hgt : t ∈ 𝓝[g '' s] g x₀
hst : insert x₀ s ×ˢ t ∈ 𝓝[(fun x ↦ (x, g x)) '' s] (x₀, g x₀)
v : Set (E × F)
hv : v ∈ 𝓝[insert (x₀, g x₀) (insert x₀ s ×ˢ t)] (x₀, g x₀)
hvs : v ⊆ insert (x₀, g x₀) (insert x₀ s ×ˢ t)
f_an : n = ω → AnalyticOn 𝕜 (uncurry f) v
f' : E × F → E × F →L[𝕜] G
hvf' : ∀ x ∈ v, HasFDerivWithinAt (uncurry f) (f' x) (insert x₀ s ×ˢ t) x
hf' : ContDiffWithinAt 𝕜 n f' (insert x₀ s ×ˢ t) (x₀, g x₀)
⊢ ∀ x ∈ (fun z ↦ (z, g z)) ⁻¹' v ∩ insert x₀ s,
    HasFDerivWithinAt (f x) ((fun z ↦ f' (z, g z) ∘SL ContinuousLinearMap.inr 𝕜 E F) x) t (g x)

Tactic:
intro z

Goal state after:
case refine_2
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
n : ℕ∞ω
f : E → F → G
g : E → F
t : Set F
hn : n ≠ ∞
x₀ : E
hf : ContDiffWithinAt 𝕜 (n + 1) (uncurry f) (insert x₀ s ×ˢ t) (x₀, g x₀)
hg : ContDiffWithinAt 𝕜 n g s x₀
hgt : t ∈ 𝓝[g '' s] g x₀
hst : insert x₀ s ×ˢ t ∈ 𝓝[(fun x ↦ (x, g x)) '' s] (x₀, g x₀)
v : Set (E × F)
hv : v ∈ 𝓝[insert (x₀, g x₀) (insert x₀ s ×ˢ t)] (x₀, g x₀)
hvs : v ⊆ insert (x₀, g x₀) (insert x₀ s ×ˢ t)
f_an : n = ω → AnalyticOn 𝕜 (uncurry f) v
f' : E × F → E × F →L[𝕜] G
hvf' : ∀ x ∈ v, HasFDerivWithinAt (uncurry f) (f' x) (insert x₀ s ×ˢ t) x
hf' : ContDiffWithinAt 𝕜 n f' (insert x₀ s ×ˢ t) (x₀, g x₀)
z : E
⊢ z ∈ (fun z ↦ (z, g z)) ⁻¹' v ∩ insert x₀ s →
    HasFDerivWithinAt (f z) ((fun z ↦ f' (z, g z) ∘SL ContinuousLinearMap.inr 𝕜 E F) z) t (g z)
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:
← h

Goal state after:
case inl
n : ℕ
c : OrderedFinpartition (n + 1)
hc : range (c.emb (c.index 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)))
Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno

Goal state before:
pp: n : ℕ
c : OrderedFinpartition n
j : Fin c.length
h : range ((c.extendMiddle j).emb j) = {0}
⊢ (c.emb j 0).succ ∈ {0}

Tactic:
← h

Goal state after:
n : ℕ
c : OrderedFinpartition n
j : Fin c.length
h : range ((c.extendMiddle j).emb j) = {0}
⊢ (c.emb j 0).succ ∈ range ((c.extendMiddle j).emb j)
Module: Mathlib.Analysis.SpecialFunctions.Exponential

Goal state before:
pp: 𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕂
inst✝³ : NormedCommRing 𝔸
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : CompleteSpace 𝔸
inst✝ : CharZero 𝕂
x : 𝔸
hx : x ∈ Metric.eball 0 (expSeries 𝕂 𝔸).radius
this : ∀ᶠ (h : 𝔸) in 𝓝 0, h ∈ Metric.eball 0 (expSeries 𝕂 𝔸).radius
a✝ : 𝔸
hh : a✝ ∈ Metric.eball 0 (expSeries 𝕂 𝔸).radius
⊢ exp x * (exp a✝ - 1 - (ContinuousLinearMap.id 𝕂 𝔸) a✝) =
    exp x * exp a✝ - exp x - exp x • (ContinuousLinearMap.id 𝕂 𝔸) a✝

Tactic:
ContinuousLinearMap.id_apply,

Goal state after:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕂
inst✝³ : NormedCommRing 𝔸
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : CompleteSpace 𝔸
inst✝ : CharZero 𝕂
x : 𝔸
hx : x ∈ Metric.eball 0 (expSeries 𝕂 𝔸).radius
this : ∀ᶠ (h : 𝔸) in 𝓝 0, h ∈ Metric.eball 0 (expSeries 𝕂 𝔸).radius
a✝ : 𝔸
hh : a✝ ∈ Metric.eball 0 (expSeries 𝕂 𝔸).radius
⊢ exp x * (exp a✝ - 1 - a✝) = exp x * exp a✝ - exp x - exp x • a✝
Module: Mathlib.Topology.ExtendFrom

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : RegularSpace Y
f : X → Y
A B : Set X
hB : B ⊆ closure[inst✝²] A
hf : ∀ x ∈ B, ∃ y, Tendsto f (𝓝[A] x) (𝓝 y)
φ : X → Y := extendFrom A f
x : X
x_in : x ∈ B
V' : Set Y
V'_in : V' ∈ 𝓝 (φ x)
V'_closed : IsClosed[inst✝¹] V'
⊢ ∃ V ∈ 𝓝 x, IsOpen[inst✝²] V ∧ V ∩ A ⊆ f ⁻¹' V'

Tactic:
by
    have := tendsto_extendFrom (hf x x_in)
    rcases (nhdsWithin_basis_open x A).tendsto_left_iff.mp this V' V'_in with ⟨V, ⟨hxV, V_op⟩, hV⟩
    exact ⟨V, IsOpen.mem_nhds V_op hxV, V_op, hV⟩

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

Goal state before:
pp: case insert
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ∞ω
ι : Type u_3
f : ι → E → F
t : Set E
x : E
i : ι
s : Finset ι
is : i ∉ s
IH : (∀ i ∈ s, ContDiffWithinAt 𝕜 n (fun x ↦ f i x) t x) → ContDiffWithinAt 𝕜 n (fun x ↦ ∑ i ∈ s, f i x) t x
h : ∀ i_1 ∈ insert i s, ContDiffWithinAt 𝕜 n (fun x ↦ f i_1 x) t x
⊢ ContDiffWithinAt 𝕜 n (fun x ↦ ∑ i ∈ insert i s, f i x) t x

Tactic:
| insert i s is IH =>

Goal state after:
Module: Mathlib.Topology.Order.ExtendFrom

Goal state before:
pp: case neg.hf
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
f : α → β
a b : α
la lb : β
inst✝ : RegularSpace β
hf : ContinuousOn f (Ioo a b)
ha : Tendsto f (𝓝[>] a) (𝓝 la)
hb : Tendsto f (𝓝[<] b) (𝓝 lb)
hab : a ≠ b
x : α
x_in : x ∈ Icc a b
⊢ ∃ y, Tendsto f (𝓝[Ioo a b] x) (𝓝 y)

Tactic:
rcases eq_endpoints_or_mem_Ioo_of_mem_Icc x_in with (rfl | rfl | h)

Goal state after:
case neg.hf.inl
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
f : α → β
b : α
la lb : β
inst✝ : RegularSpace β
hb : Tendsto f (𝓝[<] b) (𝓝 lb)
x : α
hf : ContinuousOn f (Ioo x b)
ha : Tendsto f (𝓝[>] x) (𝓝 la)
hab : x ≠ b
x_in : x ∈ Icc x b
⊢ ∃ y, Tendsto f (𝓝[Ioo x b] x) (𝓝 y)

case neg.hf.inr.inl
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
f : α → β
a : α
la lb : β
inst✝ : RegularSpace β
ha : Tendsto f (𝓝[>] a) (𝓝 la)
x : α
hf : ContinuousOn f (Ioo a x)
hb : Tendsto f (𝓝[<] x) (𝓝 lb)
hab : a ≠ x
x_in : x ∈ Icc a x
⊢ ∃ y, Tendsto f (𝓝[Ioo a x] x) (𝓝 y)

case neg.hf.inr.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 (Ioo a b)
ha : Tendsto f (𝓝[>] a) (𝓝 la)
hb : Tendsto f (𝓝[<] b) (𝓝 lb)
hab : a ≠ b
x : α
x_in : x ∈ Icc a b
h : x ∈ Ioo a b
⊢ ∃ y, Tendsto f (𝓝[Ioo a b] x) (𝓝 y)
Module: Mathlib.Analysis.Calculus.ContDiff.Operations

Goal state before:
pp: case succ
𝕜 : 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
⊢ ((a ^ i • fderiv 𝕜 (fun x ↦ iteratedFDeriv 𝕜 i f (a • x)) v) (x✝ 0)) (tail x✝) =
    a ^ (i + 1) • ((fderiv 𝕜 (iteratedFDeriv 𝕜 i f) (a • v)) (x✝ 0)) (tail x✝)

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:
fderiv_comp_smul,

Goal state after:
case succ
𝕜 : 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
⊢ ((a ^ i • a • fderiv 𝕜 (iteratedFDeriv 𝕜 i f) (a • v)) (x✝ 0)) (tail x✝) =
    a ^ (i + 1) • ((fderiv 𝕜 (iteratedFDeriv 𝕜 i f) (a • v)) (x✝ 0)) (tail x✝)

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
Module: Mathlib.Analysis.Calculus.Deriv.MeanValue

Goal state before:
pp: f f' : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
g g' : ℝ → ℝ
hgc : ContinuousOn g (Icc a b)
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
h : ℝ → ℝ := fun x ↦ (g b - g a) * f x - (f b - f a) * g x
hI : h a = h b
⊢ ∃ c ∈ Ioo a b, (g b - g a) * f' c = (f b - f a) * g' c

Tactic:
let h' x := (g b - g a) * f' x - (f b - f a) * g' x

Goal state after:
f f' : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
g g' : ℝ → ℝ
hgc : ContinuousOn g (Icc a b)
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
h : ℝ → ℝ := fun x ↦ (g b - g a) * f x - (f b - f a) * g x
hI : h a = h b
h' : ℝ → ℝ := fun x ↦ (g b - g a) * f' x - (f b - f a) * g' x
⊢ ∃ c ∈ Ioo a b, (g b - g a) * f' c = (f b - f a) * g' c
Module: Mathlib.Analysis.Calculus.Deriv.MeanValue

Goal state before:
pp: f : ℝ → ℝ
a : ℝ
hf : Tendsto (derivWithin f (Ioi a)) (𝓝[>] a) atTop
hcont_at_a : ContinuousWithinAt f (Ici a) a
hdiff : Tendsto (slope f a) (𝓝[>] a) (𝓝 (derivWithin f (Ioi a) a))
h₀ : ∀ᶠ (b : ℝ) in 𝓝[>] a, ∀ x ∈ Ioc a b, max (derivWithin f (Ioi a) a + 1) 0 < derivWithin f (Ioi a) x
h₁ : ∀ᶠ (b : ℝ) in 𝓝[>] a, slope f a b < derivWithin f (Ioi a) a + 1
b : ℝ
hb : ∀ x ∈ Ioc a b, max (derivWithin f (Ioi a) a + 1) 0 < derivWithin f (Ioi a) x
hslope : slope f a b < derivWithin f (Ioi a) a + 1
hab : a < b
hdiff' : DifferentiableOn ℝ f (Ioc a b)
⊢ ∀ z ∈ Ioc a b, ContinuousWithinAt f (Icc a b) z

Tactic:
intro z

Goal state after:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (derivWithin f (Ioi a)) (𝓝[>] a) atTop
hcont_at_a : ContinuousWithinAt f (Ici a) a
hdiff : Tendsto (slope f a) (𝓝[>] a) (𝓝 (derivWithin f (Ioi a) a))
h₀ : ∀ᶠ (b : ℝ) in 𝓝[>] a, ∀ x ∈ Ioc a b, max (derivWithin f (Ioi a) a + 1) 0 < derivWithin f (Ioi a) x
h₁ : ∀ᶠ (b : ℝ) in 𝓝[>] a, slope f a b < derivWithin f (Ioi a) a + 1
b : ℝ
hb : ∀ x ∈ Ioc a b, max (derivWithin f (Ioi a) a + 1) 0 < derivWithin f (Ioi a) x
hslope : slope f a b < derivWithin f (Ioi a) a + 1
hab : a < b
hdiff' : DifferentiableOn ℝ f (Ioc a b)
z : ℝ
⊢ z ∈ Ioc a b → ContinuousWithinAt f (Icc a b) z
Module: Mathlib.Analysis.Calculus.Deriv.MeanValue

Goal state before:
pp: f : ℝ → ℝ
a : ℝ
hf : Tendsto (derivWithin f (Ioi a)) (𝓝[>] a) atTop
hcont_at_a : ContinuousWithinAt f (Ici a) a
hdiff : Tendsto (slope f a) (𝓝[>] a) (𝓝 (derivWithin f (Ioi a) a))
h₀ : ∀ᶠ (b : ℝ) in 𝓝[>] a, ∀ x ∈ Ioc a b, max (derivWithin f (Ioi a) a + 1) 0 < derivWithin f (Ioi a) x
h₁ : ∀ᶠ (b : ℝ) in 𝓝[>] a, slope f a b < derivWithin f (Ioi a) a + 1
b : ℝ
hb : ∀ x ∈ Ioc a b, max (derivWithin f (Ioi a) a + 1) 0 < derivWithin f (Ioi a) x
hslope : slope f a b < derivWithin f (Ioi a) a + 1
hab : a < b
hdiff' : DifferentiableOn ℝ f (Ioc a b)
hcont_Ioc : ∀ z ∈ Ioc a b, ContinuousWithinAt f (Icc a b) z
⊢ ContinuousOn f (Icc a b)

Tactic:
intro z

Goal state after:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (derivWithin f (Ioi a)) (𝓝[>] a) atTop
hcont_at_a : ContinuousWithinAt f (Ici a) a
hdiff : Tendsto (slope f a) (𝓝[>] a) (𝓝 (derivWithin f (Ioi a) a))
h₀ : ∀ᶠ (b : ℝ) in 𝓝[>] a, ∀ x ∈ Ioc a b, max (derivWithin f (Ioi a) a + 1) 0 < derivWithin f (Ioi a) x
h₁ : ∀ᶠ (b : ℝ) in 𝓝[>] a, slope f a b < derivWithin f (Ioi a) a + 1
b : ℝ
hb : ∀ x ∈ Ioc a b, max (derivWithin f (Ioi a) a + 1) 0 < derivWithin f (Ioi a) x
hslope : slope f a b < derivWithin f (Ioi a) a + 1
hab : a < b
hdiff' : DifferentiableOn ℝ f (Ioc a b)
hcont_Ioc : ∀ z ∈ Ioc a b, ContinuousWithinAt f (Icc a b) z
z : ℝ
⊢ z ∈ Icc a b → ContinuousWithinAt f (Icc a b) z