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

Goal state before:
pp: case inr.refine_1
𝕜 : 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
x : (i : ι) → E i
inst✝ : DecidableEq ι
y : (i : ι) → E i
h✝ : Nonempty ι
⊢ Fin (Nat.succ 0 + (Fintype.card ι - Nat.succ 0)) → { s // #s = Fintype.card ι - 1 }

Tactic:
exact (⟨{·}ᶜ, by
      rw [card_compl, Fintype.card_fin, Finset.card_singleton, Nat.add_sub_cancel_left]⟩)

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 : k
⊢ (b - a)⁻¹ • (f b -ᵥ f a) = (a - b)⁻¹ • (f a -ᵥ f b)

Tactic:
← neg_vsub_eq_vsub_rev,

Goal state after:
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 : k
⊢ (b - a)⁻¹ • -(f a -ᵥ f b) = (a - b)⁻¹ • (f a -ᵥ f b)
Module: Mathlib.LinearAlgebra.AffineSpace.Slope

Goal state before:
pp: 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
⊢ f x ≤ f y ∧ ¬0 = slope f x y ↔ f x ≤ f y ∧ ¬f x = f y

Tactic:
eq_comm,

Goal state after:
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
⊢ f x ≤ f y ∧ ¬slope f x y = 0 ↔ f x ≤ f y ∧ ¬f x = f y
Module: Mathlib.Analysis.Calculus.FDeriv.RestrictScalars

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
𝕜' : Type u_2
inst✝⁹ : NontriviallyNormedField 𝕜'
inst✝⁸ : NormedAlgebra 𝕜 𝕜'
E : Type u_3
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedSpace 𝕜' E
inst✝⁴ : IsScalarTower 𝕜 𝕜' E
F : Type u_4
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
f : E → F
x : E
hf : DifferentiableAt 𝕜 f x
⊢ DifferentiableAt 𝕜' f x ↔ ∃ g', restrictScalars 𝕜 g' = fderiv 𝕜 f x

Tactic:
rw [← differentiableWithinAt_univ, ← fderivWithin_univ]

Goal state after:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
𝕜' : Type u_2
inst✝⁹ : NontriviallyNormedField 𝕜'
inst✝⁸ : NormedAlgebra 𝕜 𝕜'
E : Type u_3
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedSpace 𝕜' E
inst✝⁴ : IsScalarTower 𝕜 𝕜' E
F : Type u_4
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
f : E → F
x : E
hf : DifferentiableAt 𝕜 f x
⊢ DifferentiableWithinAt 𝕜' f univ x ↔ ∃ g', restrictScalars 𝕜 g' = fderivWithin 𝕜 f univ x
Module: Mathlib.Analysis.Calculus.FDeriv.Analytic

Goal state before:
pp: case e'_3.e'_5
𝕜 : 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
n : ℕ
x : E
⊢ n + 1 = (1 + n).choose n

Tactic:
eq_comm,

Goal state after:
case e'_3.e'_5
𝕜 : 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
n : ℕ
x : E
⊢ (1 + n).choose n = n + 1
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, HasStrictFDerivAt (fun x ↦ g i x) (g' i) x
⊢ HasStrictFDerivAt (fun x ↦ (Multiset.map (fun x_1 ↦ g x_1 x) u).prod)
    (Multiset.map (fun i ↦ (Multiset.map (fun x_1 ↦ g x_1 x) (u.erase i)).prod •> g' i) u).sum x

Tactic:
by
  simp only [← Multiset.attach_map_val u, Multiset.map_map]
  exact .congr_fderiv
    (hasStrictFDerivAt_multiset_prod.comp x <|
      hasStrictFDerivAt_pi.mpr fun i ↦ h (Subtype.val i) i.prop :)
    (by ext; simp [Finset.sum_multiset_map_count, u.erase_attach_map (g · x)])

Goal state after:
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 : 𝕜 → E
z₀ : 𝕜
m n : ℤ
hm : ∃ g, AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = (z - z₀) ^ m • g z
hn : ∃ g, AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = (z - z₀) ^ n • g z
⊢ m = n

Tactic:
by
  wlog! h_le : n ≤ m generalizing m n
  · exact ((this hn hm) h_le.le).symm
  let ⟨g, hg_an, _, hg_eq⟩ := hm
  let ⟨j, hj_an, hj_ne, hj_eq⟩ := hn
  contrapose! hj_ne
  have : ∃ᶠ z in 𝓝[≠] z₀, j z = (z - z₀) ^ (m - n) • g z := by
    apply Filter.Eventually.frequently
    rw [eventually_nhdsWithin_iff] at hg_eq hj_eq ⊢
    filter_upwards [hg_eq, hj_eq] with z hfz hfz' hz
    rw [← add_sub_cancel_left n m, add_sub_assoc, zpow_add₀ <| sub_ne_zero.mpr hz, mul_smul,
      hfz' hz, smul_right_inj <| zpow_ne_zero _ <| sub_ne_zero.mpr hz] at hfz
    exact hfz hz
  rw [frequently_eq_iff_eventually_eq hj_an] at this
  · rw [EventuallyEq.eq_of_nhds this, sub_self, zero_zpow _ (sub_ne_zero.mpr hj_ne), zero_smul]
  conv => enter [2, z, 1]; rw [← Int.toNat_sub_of_le h_le, zpow_natCast]
  exact ((analyticAt_id.sub analyticAt_const).pow _).smul hg_an

Goal state after:
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 : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
n : ℕ
g : 𝕜 → E
hg_an : AnalyticAt 𝕜 g z₀
hg_eq : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z
hg_ne : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0
z : 𝕜
hf_eq : 0 = (z - z₀) ^ n • g z
hf0 : f z = 0
hz : z ∈ {z₀}ᶜ
⊢ g z = 0

Tactic:
eq_comm,

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
n : ℕ
g : 𝕜 → E
hg_an : AnalyticAt 𝕜 g z₀
hg_eq : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z
hg_ne : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0
z : 𝕜
hf_eq : (z - z₀) ^ n • g z = 0
hf0 : f z = 0
hz : z ∈ {z₀}ᶜ
⊢ g z = 0
Module: Mathlib.Analysis.Calculus.ContDiff.RCLike

Goal state before:
pp: E : Type u_4
F : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
x : E
hf : ContDiffWithinAt ℝ 1 f s x
hs : Convex ℝ s
t : Set E
hst : t ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries ℝ E F
hp : HasFTaylorSeriesUpToOn (↑1) f p t
ε : ℝ
ε0 : ε > 0
hε : Metric.ball x ε ∩ insert x s ⊆ t
⊢ ∃ K, ∃ t ∈ 𝓝[s] x, LipschitzOnWith K f t

Tactic:
replace hp : HasFTaylorSeriesUpToOn 1 f p (Metric.ball x ε ∩ insert x s) := hp.mono hε

Goal state after:
E : Type u_4
F : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
x : E
hf : ContDiffWithinAt ℝ 1 f s x
hs : Convex ℝ s
t : Set E
hst : t ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries ℝ E F
ε : ℝ
ε0 : ε > 0
hε : Metric.ball x ε ∩ insert x s ⊆ t
hp : HasFTaylorSeriesUpToOn 1 f p (Metric.ball x ε ∩ insert x s)
⊢ ∃ K, ∃ t ∈ 𝓝[s] x, LipschitzOnWith K f t
Module: Mathlib.Analysis.Calculus.LogDeriv

Goal state before:
pp: case cons.hdg
𝕜 : 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 : f a x ≠ 0 ∧ ∀ x_1 ∈ s, f x_1 x ≠ 0
hd : DifferentiableAt 𝕜 (f a) x ∧ ∀ x_1 ∈ s, DifferentiableAt 𝕜 (f x_1) x
⊢ DifferentiableAt 𝕜 (fun x ↦ ∏ i ∈ s, f i x) x

Tactic:
exact .fun_finsetProd hd.2

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
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ε : s ∩ ball x ε ⊆ {y | HasFDerivWithinAt f (f' y) s y ∧ ‖f' y‖₊ < K}
⊢ ∃ t ∈ 𝓝[s] x, LipschitzOnWith K f t

Tactic:
refine ⟨s ∩ ball x ε, inter_mem_nhdsWithin _ (ball_mem_nhds _ ε0), ?_⟩

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ε : s ∩ ball x ε ⊆ {y | HasFDerivWithinAt f (f' y) s y ∧ ‖f' y‖₊ < K}
⊢ LipschitzOnWith K f (s ∩ ball x ε)
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))
  rw [inter_comm] at hε
  refine ⟨s ∩ ball x ε, inter_mem_nhdsWithin _ (ball_mem_nhds _ ε0), ?_⟩
  exact
    (hs.inter (convex_ball _ _)).lipschitzOnWith_of_nnnorm_hasFDerivWithin_le
      (fun y hy => (hε hy).1.mono inter_subset_left) fun y hy => (hε hy).2.le

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 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 : 0 = f y - g y
⊢ f y = g y

Tactic:
eq_comm,

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 : f y - g y = 0
⊢ f y = g y
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
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hs' : IsPreconnected s
hf : DifferentiableOn 𝕜 f s
hg : DifferentiableOn 𝕜 g s
hf' : EqOn (fderiv 𝕜 f) (fderiv 𝕜 g) s
⊢ ∃ a, ∀ ⦃x : E⦄, x ∈ s → f x - g x = a

Tactic:
refine hs.exists_is_const_of_fderiv_eq_zero hs' (hf.sub hg) fun x hx ↦ ?_

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
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hs' : IsPreconnected s
hf : DifferentiableOn 𝕜 f s
hg : DifferentiableOn 𝕜 g s
hf' : EqOn (fderiv 𝕜 f) (fderiv 𝕜 g) s
x : E
hx : x ∈ s
⊢ fderiv 𝕜 (fun x ↦ f x - g x) x = 0 x
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
s : Set E
f : E → F
n : ℕ∞ω
x : G
g : G →L[𝕜] E
hf : ContDiffWithinAt 𝕜 n f s (g x)
⊢ ContDiffWithinAt 𝕜 n (f ∘ ⇑g) (⇑g ⁻¹' s) x

Tactic:
match n with
  | ω =>
    obtain ⟨u, hu, p, hp, h'p⟩ := hf
    refine ⟨g ⁻¹' u, ?_, _, hp.compContinuousLinearMap g, ?_⟩
    · refine g.continuous.continuousWithinAt.tendsto_nhdsWithin ?_ hu
      exact (mapsTo_singleton.2 <| mem_singleton _).union_union (mapsTo_preimage _ _)
    · intro i
      change AnalyticOn 𝕜 (fun x ↦
        ContinuousMultilinearMap.compContinuousLinearMapL (fun _ ↦ g) (p (g x) i)) (⇑g ⁻¹' u)
      apply AnalyticOn.comp _ _ (Set.mapsTo_univ _ _)
      · exact ContinuousLinearMap.analyticOn _ _
      · exact (h'p i).comp (g.analyticOn _) (mapsTo_preimage _ _)
  | (n : ℕ∞) =>
    intro m hm
    rcases hf m hm with ⟨u, hu, p, hp⟩
    refine ⟨g ⁻¹' u, ?_, _, hp.compContinuousLinearMap g⟩
    refine g.continuous.continuousWithinAt.tendsto_nhdsWithin ?_ hu
    exact (mapsTo_singleton.2 <| mem_singleton _).union_union (mapsTo_preimage _ _)

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
h : ContDiffWithinAt 𝕜 ω f s x
⊢ AnalyticWithinAt 𝕜 f s x

Tactic:
obtain ⟨u, hu, hf⟩ := h.analyticOn

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
h : ContDiffWithinAt 𝕜 ω f s x
u : Set E
hu : u ∈ 𝓝[insert x s] x
hf : AnalyticOn 𝕜 f u
⊢ AnalyticWithinAt 𝕜 f s x
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
x : 𝕜
⊢ iteratedDeriv n f x = deriv^[n] f x

Tactic:
← iteratedDerivWithin_univ

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
x : 𝕜
⊢ iteratedDerivWithin n f univ x = deriv^[n] f x
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 : ℕ
x : 𝕜
⊢ iteratedDeriv n (fun x ↦ 0) x = 0

Tactic:
simpa using @iteratedDeriv_const 𝕜 _ F _ _ n 0

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

Goal state before:
pp: case inr
n : ℕ
c : OrderedFinpartition n
i j : Fin c.length
h : range ((c.extendMiddle i).emb j) = {0}
hij : j ≠ i
this : (c.extendMiddle i).emb j 0 ∈ range ((c.extendMiddle i).emb j)
⊢ False

Tactic:
rw [h] at this

Goal state after:
case inr
n : ℕ
c : OrderedFinpartition n
i j : Fin c.length
h : range ((c.extendMiddle i).emb j) = {0}
hij : j ≠ i
this : (c.extendMiddle i).emb j 0 ∈ {0}
⊢ False
Module: Mathlib.Analysis.Calculus.ContDiff.Defs

Goal state before:
pp: case ht
𝕜 : 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 : ℕ
hs : UniqueDiffOn 𝕜 s
h : ContDiffAt 𝕜 (↑n) f x
hx : x ∈ s
u : Set E
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xu : x ∈ u
hu : ContDiffOn 𝕜 (↑n) f (insert x univ ∩ u)
⊢ UniqueDiffOn 𝕜 (univ ∩ u)

Tactic:
apply uniqueDiffOn_univ.inter u_open

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
f : E → F
n : ℕ∞ω
⊢ ContDiff 𝕜 n f ↔ ∀ (x : E), ContDiffAt 𝕜 n f x

Tactic:
by
  simp [← contDiffOn_univ, ContDiffOn, ContDiffAt]

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

Goal state before:
pp: case inl.refine_2
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
c✝ : OrderedFinpartition n
c : OrderedFinpartition (n + 1)
hc : range (c.emb 0) ≠ {0}
x : Fin n
j : Fin (c.partSize (c.index 0))
hij : c.emb (c.index 0) j = x.succ
j_ne : j ≠ 0
je_ne' : ↑j ≠ 0
A : c.partSize (c.index 0) - 1 + 1 = c.partSize (c.index 0)
B : update c.partSize (c.index 0) (c.partSize (c.index 0) - 1) (c.index 0) = c.partSize (c.index 0) - 1
this : x = x.succ.pred ⋯
⊢ Fin.cast ⋯ (Fin.cast ⋯ ((Fin.cast ⋯ j).pred ⋯)).succ = j

Tactic:
← val_eq_val

Goal state after:
case inl.refine_2
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
c✝ : OrderedFinpartition n
c : OrderedFinpartition (n + 1)
hc : range (c.emb 0) ≠ {0}
x : Fin n
j : Fin (c.partSize (c.index 0))
hij : c.emb (c.index 0) j = x.succ
j_ne : j ≠ 0
je_ne' : ↑j ≠ 0
A : c.partSize (c.index 0) - 1 + 1 = c.partSize (c.index 0)
B : update c.partSize (c.index 0) (c.partSize (c.index 0) - 1) (c.index 0) = c.partSize (c.index 0) - 1
this : x = x.succ.pred ⋯
⊢ ↑(Fin.cast ⋯ (Fin.cast ⋯ ((Fin.cast ⋯ j).pred ⋯)).succ) = ↑j
Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno

Goal state before:
pp: case pos.partSize
𝕜 : 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✝
n : ℕ
c : OrderedFinpartition (n + 1)
h : range (c.emb 0) = {0}
A : c.length - 1 + 1 = c.length
i : Fin (c.length - 1 + 1)
⊢ { length := c.length - 1 + 1, partSize := cons 1 fun i ↦ c.partSize (Fin.cast ⋯ i.succ), partSize_pos := ⋯,
          emb := fun i ↦
            cases (motive := fun x ↦ Fin (cons 1 (fun i ↦ c.partSize (Fin.cast ⋯ i.succ)) x) → Fin (n + 1)) (fun x ↦ 0)
              (fun m ↦ succ ∘ fun j ↦ (c.emb (Fin.cast ⋯ m.succ) j).pred ⋯) i,
          emb_strictMono := ⋯, parts_strictMono := ⋯, disjoint := ⋯, cover := ⋯ }.partSize
      i =
    c.partSize ⟨↑i, ⋯⟩

Tactic:
induction i using Fin.induction with
        | zero => change 1 = c.partSize 0; simp [c.partSize_eq_one_of_range_emb_eq_singleton h]
        | succ i => simp only [cons_succ, val_succ]; rfl

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

Goal state before:
pp: β : Type v
inst✝¹ : NormedField β
inst✝ : CauSeq.IsComplete β norm
u : ℕ → β
hu : CauchySeq u
⊢ ∃ a, Tendsto u atTop (𝓝 a)

Tactic:
have C : IsCauSeq norm u := isCauSeq_iff_cauchySeq.2 hu

Goal state after:
β : Type v
inst✝¹ : NormedField β
inst✝ : CauSeq.IsComplete β norm
u : ℕ → β
hu : CauchySeq u
C : IsCauSeq norm u
⊢ ∃ a, Tendsto u atTop (𝓝 a)
Module: Mathlib.Topology.Order.ExtendFrom

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
f : α → β
a b : α
lb : β
inst✝ : RegularSpace β
hf : ContinuousOn f (Ioo a b)
hb : Tendsto f (𝓝[<] b) (𝓝 lb)
this :
  ContinuousOn (f ∘ ⇑OrderDual.ofDual) (Ioo (OrderDual.toDual b) (OrderDual.toDual a)) →
    Tendsto (f ∘ ⇑OrderDual.ofDual) (𝓝[>] OrderDual.toDual b) (𝓝 lb) →
      ContinuousOn (extendFrom (Ioo (OrderDual.toDual b) (OrderDual.toDual a)) (f ∘ ⇑OrderDual.ofDual))
        (Ico (OrderDual.toDual b) (OrderDual.toDual a))
⊢ ContinuousOn (extendFrom (Ioo a b) f) (Ioc a b)

Tactic:
Ico_toDual,

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
f : α → β
a b : α
lb : β
inst✝ : RegularSpace β
hf : ContinuousOn f (Ioo a b)
hb : Tendsto f (𝓝[<] b) (𝓝 lb)
this :
  ContinuousOn (f ∘ ⇑OrderDual.ofDual) (Ioo (OrderDual.toDual b) (OrderDual.toDual a)) →
    Tendsto (f ∘ ⇑OrderDual.ofDual) (𝓝[>] OrderDual.toDual b) (𝓝 lb) →
      ContinuousOn (extendFrom (Ioo (OrderDual.toDual b) (OrderDual.toDual a)) (f ∘ ⇑OrderDual.ofDual))
        (⇑OrderDual.ofDual ⁻¹' Ioc a b)
⊢ ContinuousOn (extendFrom (Ioo a b) f) (Ioc a b)
Module: Mathlib.Analysis.Calculus.Deriv.MeanValue

Goal state before:
pp: f f' : ℝ → ℝ
a b : ℝ
hab : a < b
g g' : ℝ → ℝ
lfa lga lfb lgb : ℝ
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
hfa : Tendsto f (𝓝[>] a) (𝓝 lfa)
hga : Tendsto g (𝓝[>] a) (𝓝 lga)
hfb : Tendsto f (𝓝[<] b) (𝓝 lfb)
hgb : Tendsto g (𝓝[<] b) (𝓝 lgb)
⊢ ∃ c ∈ Ioo a b, (lgb - lga) * f' c = (lfb - lfa) * g' c

Tactic:
let h x := (lgb - lga) * f x - (lfb - lfa) * g x
  have hha : Tendsto h (𝓝[>] a) (𝓝 <| lgb * lfa - lfb * lga) := by
    have : Tendsto h (𝓝[>] a) (𝓝 <| (lgb - lga) * lfa - (lfb - lfa) * lga) :=
      (tendsto_const_nhds.mul hfa).sub (tendsto_const_nhds.mul hga)
    convert! this using 2
    ring
  have hhb : Tendsto h (𝓝[<] b) (𝓝 <| lgb * lfa - lfb * lga) := by
    have : Tendsto h (𝓝[<] b) (𝓝 <| (lgb - lga) * lfb - (lfb - lfa) * lgb) :=
      (tendsto_const_nhds.mul hfb).sub (tendsto_const_nhds.mul hgb)
    convert! this using 2
    ring
  let h' x := (lgb - lga) * f' x - (lfb - lfa) * g' x
  have hhh' : ∀ x ∈ Ioo a b, HasDerivAt h (h' x) x := by
    intro x hx
    exact ((hff' x hx).const_mul _).sub ((hgg' x hx).const_mul _)
  rcases exists_hasDerivAt_eq_zero' hab hha hhb hhh' with ⟨c, cmem, hc⟩
  exact ⟨c, cmem, sub_eq_zero.1 hc⟩

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv

Goal state before:
pp: case hf
n : ℕ∞ω
x : ℝ
hx✝ : x ≠ 0
A : ∀ (y : ℝ), 0 < y → ContDiffAt ℝ n log y
hx : x < 0
⊢ ContDiffAt ℝ n (fun y ↦ -y) x

Tactic:
apply contDiffAt_id.neg

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv

Goal state before:
pp: f : ℝ → ℝ
x : ℝ
h₁ : DifferentiableAt ℝ f x
h₂ : f x ≠ 0
⊢ deriv (log ∘ f) x = logDeriv f x

Tactic:
simp only [logDeriv, Pi.div_apply, ← deriv.log h₁ h₂, Function.comp_def]

Goal state after: