awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.FDeriv.Congr
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : E → F
f' : E →L[𝕜] F
x : E
s t : Set E
inst_7 : T1Space E
y : E
h : s =ᶠ[𝓝[{y}ᶜ] x] t
hne : x ≠ y
⊢ s =ᶠ[𝓝 x] t

Tactic:
rw [hne.nhdsWithin_compl_singleton] at h

Premises used: Ne.nhdsWithin_compl_singleton
-- Module: Mathlib.Analysis.Calculus.FDeriv.Congr
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : E → F
f' : E →L[𝕜] F
x : E
s t : Set E
inst_7 : T1Space E
y : E
h : s =ᶠ[𝓝[{y}ᶜ] x] t
hne : x ≠ y
h₁ : s =ᶠ[𝓝 x] t
⊢ x ≠ y

Tactic:
rw [hne.nhdsWithin_compl_singleton] at h

Premises used: Ne.nhdsWithin_compl_singleton
-- Module: Mathlib.Analysis.Calculus.FDeriv.Congr
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : E → F
f' : E →L[𝕜] F
x : E
s t : Set E
inst_7 : T1Space E
y : E
h : s =ᶠ[𝓝 x] t
hne : x ≠ y
⊢ HasFDerivWithinAt f f' s x ↔ HasFDerivWithinAt f f' t x

Tactic:
hasFDerivWithinAt_congr_set h

Premises used: hasFDerivWithinAt_congr_set
-- Module: Mathlib.Analysis.Calculus.FDeriv.Congr
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : E → F
f' : E →L[𝕜] F
x : E
s t : Set E
inst_7 : T1Space E
y : E
h : s =ᶠ[𝓝 x] t
hne : x ≠ y
⊢ HasFDerivWithinAt f f' s x ↔ HasFDerivWithinAt f f' t x

Tactic:
exact hasFDerivWithinAt_congr_set h

Premises used: hasFDerivWithinAt_congr_set
-- Module: Mathlib.Analysis.Calculus.FDeriv.Congr
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : E → F
x : E
s t : Set E
h : s =ᶠ[𝓝[≠] x] t
⊢ DifferentiableWithinAt 𝕜 f s x ↔ DifferentiableWithinAt 𝕜 f t x

Tactic:
exists_congr fun _ => hasFDerivWithinAt_congr_set_nhdsNE h

Premises used: exists_congr, hasFDerivWithinAt_congr_set_nhdsNE, DifferentiableWithinAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Congr
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : E → F
x : E
s t : Set E
inst_7 : T1Space E
y : E
h : s =ᶠ[𝓝[{y}ᶜ] x] t
⊢ DifferentiableWithinAt 𝕜 f s x ↔ DifferentiableWithinAt 𝕜 f t x

Tactic:
exists_congr fun _ => hasFDerivWithinAt_congr_set' _ h

Premises used: exists_congr, hasFDerivWithinAt_congr_set', DifferentiableWithinAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Congr
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : E → F
x : E
s t : Set E
h : s =ᶠ[𝓝 x] t
⊢ DifferentiableWithinAt 𝕜 f s x ↔ DifferentiableWithinAt 𝕜 f t x

Tactic:
exists_congr fun _ => hasFDerivWithinAt_congr_set h

Premises used: exists_congr, DifferentiableWithinAt, hasFDerivWithinAt_congr_set
-- Module: Mathlib.Analysis.Calculus.FDeriv.Congr
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : E → F
x : E
s t : Set E
h : s =ᶠ[𝓝[≠] x] t
⊢ Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 f s x) (fderivWithin 𝕜 f t x)

Tactic:
simp only [fderivWithin, differentiableWithinAt_congr_set_nhdsNE h,
    hasFDerivWithinAt_congr_set_nhdsNE h]

Premises used: fderivWithin, hasFDerivWithinAt_congr_set_nhdsNE, differentiableWithinAt_congr_set_nhdsNE
-- Module: Mathlib.Analysis.Calculus.FDeriv.Congr
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : E → F
x : E
s t : Set E
h : s =ᶠ[𝓝[≠] x] t
⊢ Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 f s x) (fderivWithin 𝕜 f t x)

Tactic:
classical
  simp only [fderivWithin, differentiableWithinAt_congr_set_nhdsNE h,
    hasFDerivWithinAt_congr_set_nhdsNE h]

Premises used: fderivWithin, hasFDerivWithinAt_congr_set_nhdsNE, differentiableWithinAt_congr_set_nhdsNE
-- Module: Mathlib.Analysis.Calculus.FDeriv.Congr
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : E → F
x : E
s t : Set E
inst_7 : T1Space E
y : E
h : s =ᶠ[𝓝[{y}ᶜ] x] t
⊢ Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 f s x) (fderivWithin 𝕜 f t x)

Tactic:
simp only [fderivWithin, differentiableWithinAt_congr_set' _ h, hasFDerivWithinAt_congr_set' _ h]

Premises used: fderivWithin, differentiableWithinAt_congr_set', hasFDerivWithinAt_congr_set'
-- Module: Mathlib.Analysis.Calculus.FDeriv.Congr
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : E → F
x : E
s t : Set E
inst_7 : T1Space E
y : E
h : s =ᶠ[𝓝[{y}ᶜ] x] t
⊢ Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 f s x) (fderivWithin 𝕜 f t x)

Tactic:
classical
  simp only [fderivWithin, differentiableWithinAt_congr_set' _ h, hasFDerivWithinAt_congr_set' _ h]

Premises used: fderivWithin, differentiableWithinAt_congr_set', hasFDerivWithinAt_congr_set'
-- Module: Mathlib.Analysis.Calculus.FDeriv.Congr
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : E → F
x : E
s t : Set E
h : s =ᶠ[𝓝 x] t
⊢ Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 f s x) (fderivWithin 𝕜 f t x)

Tactic:
fderivWithin_congr_set_nhdsNE <| h.filter_mono inf_le_left

Premises used: Filter.EventuallyEq.filter_mono, fderivWithin_congr_set_nhdsNE, inf_le_left
-- Module: Mathlib.Analysis.Calculus.FDeriv.Congr
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : E → F
x : E
s t : Set E
inst_7 : T1Space E
y : E
h : s =ᶠ[𝓝[{y}ᶜ] x] t
⊢ (𝓝 x).EventuallyEq (β := E →L[𝕜] F) (fderivWithin 𝕜 f s) (fderivWithin 𝕜 f t)

Tactic:
(eventually_nhds_nhdsWithin.2 h).mono fun _ => fderivWithin_congr_set' y

Premises used: Iff.mpr, eventually_nhds_nhdsWithin, Filter.EventuallyEq, fderivWithin_congr_set', Filter.Eventually.mono
-- Module: Mathlib.Analysis.Calculus.FDeriv.Congr
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : E → F
x : E
s t : Set E
h : s =ᶠ[𝓝 x] t
⊢ (𝓝 x).EventuallyEq (β := E →L[𝕜] F) (fderivWithin 𝕜 f s) (fderivWithin 𝕜 f t)

Tactic:
(eventually_eventually_nhds.2 h).mono fun _ => fderivWithin_congr_set

Premises used: Iff.mpr, Filter.EventuallyEq, Filter.Eventually.mono, eventually_eventually_nhds, fderivWithin_congr_set
-- Module: Mathlib.Analysis.Calculus.FDeriv.Congr
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f₀ f₁ : E → F
f₀' f₁' : E →L[𝕜] F
L : Filter (E × E)
h₀ : Prod.map f₀ f₀ =ᶠ[L] Prod.map f₁ f₁
h₁ : ∀ (x : E), Eq.{u_3 + 1} (α := F) ((f₀' : (a : E) → F) x : F) ((f₁' : (a : E) → F) x : F)
simp :
  (IsLittleOTVS.{u_1, u_2, u_3, u_2} 𝕜 (E := F) (F := E) L
      (fun (p : E × E) ↦ HSub.hSub (β := F) (f₀ p.1 - f₀ p.2) ((f₀' : (a : E) → F) (p.1 - p.2) : F)) fun (p : E × E) ↦
      p.1 - p.2) ↔
    IsLittleOTVS.{u_1, u_2, u_3, u_2} 𝕜 (E := F) (F := E) L
      (fun (p : E × E) ↦ HSub.hSub (β := F) (f₁ p.1 - f₁ p.2) ((f₁' : (a : E) → F) (p.1 - p.2) : F)) fun (p : E × E) ↦
      p.1 - p.2
⊢ HasFDerivAtFilter f₀ f₀' L ↔ HasFDerivAtFilter f₁ f₁' L

Tactic:
simp only [hasFDerivAtFilter_iff_isLittleOTVS]

Premises used: hasFDerivAtFilter_iff_isLittleOTVS
-- Module: Mathlib.Analysis.Calculus.FDeriv.Congr
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f₀ f₁ : E → F
f₀' f₁' : E →L[𝕜] F
L : Filter (E × E)
h₀ : Prod.map f₀ f₀ =ᶠ[L] Prod.map f₁ f₁
h₁ : ∀ (x : E), Eq.{u_3 + 1} (α := F) ((f₀' : (a : E) → F) x : F) ((f₁' : (a : E) → F) x : F)
y : E × E
hy : Prod.map f₀ f₀ y = Prod.map f₁ f₁ y
⊢ Eq.{u_3 + 1} (α := F)
    ((fun (p : E × E) ↦ HSub.hSub (β := F) (f₀ p.1 - f₀ p.2) ((f₀' : (a : E) → F) (p.1 - p.2) : F)) y)
    ((fun (p : E × E) ↦ HSub.hSub (β := F) (f₁ p.1 - f₁ p.2) ((f₁' : (a : E) → F) (p.1 - p.2) : F)) y)

Tactic:
simp_all [Prod.map]

Premises used: Prod.map
-- Module: Mathlib.Analysis.Calculus.FDeriv.Congr
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f₀ f₁ : E → F
f₀' f₁' : E →L[𝕜] F
L : Filter (E × E)
h₀ : Prod.map f₀ f₀ =ᶠ[L] Prod.map f₁ f₁
h₁ : ∀ (x : E), Eq.{u_3 + 1} (α := F) ((f₀' : (a : E) → F) x : F) ((f₁' : (a : E) → F) x : F)
⊢ (IsLittleOTVS.{u_1, u_2, u_3, u_2} 𝕜 (E := F) (F := E) L
      (fun (p : E × E) ↦ HSub.hSub (β := F) (f₀ p.1 - f₀ p.2) ((f₀' : (a : E) → F) (p.1 - p.2) : F)) fun (p : E × E) ↦
      p.1 - p.2) ↔
    IsLittleOTVS.{u_1, u_2, u_3, u_2} 𝕜 (E := F) (F := E) L
      (fun (p : E × E) ↦ HSub.hSub (β := F) (f₁ p.1 - f₁ p.2) ((f₁' : (a : E) → F) (p.1 - p.2) : F)) fun (p : E × E) ↦
      p.1 - p.2

Tactic:
exact isLittleOTVS_congr (h₀.mono fun y hy => by simp_all [Prod.map]) .rfl

Premises used: Filter.Eventually.mono, Asymptotics.isLittleOTVS_congr, Filter.EventuallyEq.rfl
-- Module: Mathlib.Analysis.Calculus.FDeriv.Congr
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f₀ f₁ : E → F
f₀' f₁' : E →L[𝕜] F
x : E
h : f₀ =ᶠ[𝓝 x] f₁
h' : ∀ (y : E), Eq.{u_3 + 1} (α := F) ((f₀' : (a : E) → F) y : F) ((f₁' : (a : E) → F) y : F)
⊢ HasStrictFDerivAt f₀ f₀' x ↔ HasStrictFDerivAt f₁ f₁' x

Tactic:
h.prodMap_nhds h |>.hasFDerivAtFilter_iff h'

Premises used: HasStrictFDerivAt, Filter.EventuallyEq.hasFDerivAtFilter_iff, Filter.EventuallyEq.prodMap_nhds
-- Module: Mathlib.Analysis.Calculus.FDeriv.Congr
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : E → F
f' g' : E →L[𝕜] F
x : E
h : HasStrictFDerivAt f f' x
h' : f' = g'
⊢ HasStrictFDerivAt f g' x

Tactic:
h' ▸ h

Premises used: Eq.rec
-- Module: Mathlib.Analysis.Calculus.FDeriv.Congr
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : E → F
f' g' : E →L[𝕜] F
x : E
h : HasFDerivAt f f' x
h' : f' = g'
⊢ HasFDerivAt f g' x

Tactic:
h' ▸ h

Premises used: Eq.rec
-- Module: Mathlib.Analysis.Calculus.FDeriv.Congr
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : E → F
f' g' : E →L[𝕜] F
x : E
s : Set E
h : HasFDerivWithinAt f f' s x
h' : f' = g'
⊢ HasFDerivWithinAt f g' s x

Tactic:
h' ▸ h

Premises used: Eq.rec
-- Module: Mathlib.Analysis.Calculus.FDeriv.Congr
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f f₁ : E → F
f' : E →L[𝕜] F
x : E
h : HasStrictFDerivAt f f' x
h₁ : f =ᶠ[𝓝 x] f₁
⊢ HasStrictFDerivAt f₁ f' x

Tactic:
(h₁.hasStrictFDerivAt_iff fun _ => rfl).1 h

Premises used: Filter.EventuallyEq.hasStrictFDerivAt_iff, Iff.mp, rfl
-- Module: Mathlib.Analysis.Calculus.FDeriv.Congr
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f f₁ : E → F
f' : E →L[𝕜] F
L : Filter (E × E)
h : HasFDerivAtFilter f f' L
hL : Prod.map f₁ f₁ =ᶠ[L] Prod.map f f
⊢ HasFDerivAtFilter f₁ f' L

Tactic:
(hL.hasFDerivAtFilter_iff fun _ => rfl).2 h

Premises used: Iff.mpr, Filter.EventuallyEq.hasFDerivAtFilter_iff, rfl
-- Module: Mathlib.Analysis.Calculus.FDeriv.Congr
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f₀ f₁ : E → F
f' : E →L[𝕜] F
x : E
h : f₀ =ᶠ[𝓝 x] f₁
⊢ HasFDerivAt f₀ f' x ↔ HasFDerivAt f₁ f' x

Tactic:
h.prodMap (h.filter_mono <| pure_le_nhds _) |>.hasFDerivAtFilter_iff fun _ => rfl

Premises used: HasFDerivAt, Filter.EventuallyEq.filter_mono, pure_le_nhds, Filter.EventuallyEq.hasFDerivAtFilter_iff, rfl, Filter.EventuallyEq.prodMap
-- Module: Mathlib.Analysis.Calculus.FDeriv.Congr
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f₀ f₁ : E → F
x : E
h : f₀ =ᶠ[𝓝 x] f₁
⊢ DifferentiableAt 𝕜 f₀ x ↔ DifferentiableAt 𝕜 f₁ x

Tactic:
exists_congr fun _ => h.hasFDerivAt_iff

Premises used: DifferentiableAt, Filter.EventuallyEq.hasFDerivAt_iff, exists_congr
-- Module: Mathlib.Analysis.Calculus.FDeriv.Congr
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f₀ f₁ : E → F
f' : E →L[𝕜] F
x : E
s : Set E
h : f₀ =ᶠ[𝓝[s] x] f₁
hx : f₀ x = f₁ x
⊢ f₀ =ᶠ[pure x] f₁

Tactic:
assumption
-- Module: Mathlib.Analysis.Calculus.FDeriv.Congr
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f₀ f₁ : E → F
f' : E →L[𝕜] F
x : E
s : Set E
h : f₀ =ᶠ[𝓝[s] x] f₁
hx : x ∈ s
⊢ HasFDerivWithinAt f₀ f' s x ↔ HasFDerivWithinAt f₁ f' s x

Tactic:
h.hasFDerivWithinAt_iff (h.eq_of_nhdsWithin hx)

Premises used: Filter.EventuallyEq.hasFDerivWithinAt_iff, Filter.EventuallyEq.eq_of_nhdsWithin
-- Module: Mathlib.Analysis.Calculus.FDeriv.Congr
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f₀ f₁ : E → F
x : E
s : Set E
h : f₀ =ᶠ[𝓝[s] x] f₁
hx : f₀ x = f₁ x
⊢ DifferentiableWithinAt 𝕜 f₀ s x ↔ DifferentiableWithinAt 𝕜 f₁ s x

Tactic:
exists_congr fun _ => h.hasFDerivWithinAt_iff hx

Premises used: Filter.EventuallyEq.hasFDerivWithinAt_iff, exists_congr, DifferentiableWithinAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Congr
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f₀ f₁ : E → F
x : E
s : Set E
h : f₀ =ᶠ[𝓝[s] x] f₁
hx : x ∈ s
⊢ DifferentiableWithinAt 𝕜 f₀ s x ↔ DifferentiableWithinAt 𝕜 f₁ s x

Tactic:
h.differentiableWithinAt_iff (h.eq_of_nhdsWithin hx)

Premises used: Filter.EventuallyEq.eq_of_nhdsWithin, Filter.EventuallyEq.differentiableWithinAt_iff
-- Module: Mathlib.Analysis.Calculus.FDeriv.Congr
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f f₁ : E → F
f' : E →L[𝕜] F
x : E
s : Set E
h : HasFDerivWithinAt f f' s x
h₁ : f₁ =ᶠ[𝓝[s] x] f
hx : f₁ x = f x
⊢ HasFDerivWithinAt f₁ f' s x

Tactic:
h₁.hasFDerivWithinAt_iff hx |>.mpr h

Premises used: Iff.mpr, Filter.EventuallyEq.hasFDerivWithinAt_iff
-- Module: Mathlib.Analysis.Calculus.FDeriv.Congr
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f f₁ : E → F
f' : E →L[𝕜] F
x : E
s : Set E
h : HasFDerivWithinAt f f' s x
hs : EqOn f₁ f s
hx : f₁ x = f x
⊢ HasFDerivWithinAt f₁ f' s x

Tactic:
h.congr_of_eventuallyEq hs.eventuallyEq_nhdsWithin hx

Premises used: HasFDerivWithinAt.congr_of_eventuallyEq, Set.EqOn.eventuallyEq_nhdsWithin
-- Module: Mathlib.Analysis.Calculus.FDeriv.Congr
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f f₁ : E → F
f' : E →L[𝕜] F
x : E
s : Set E
h : HasFDerivWithinAt f f' s x
hs : EqOn f₁ f s
hx : x ∈ s
⊢ HasFDerivWithinAt f₁ f' s x

Tactic:
h.congr hs (hs hx)

Premises used: HasFDerivWithinAt.congr
-- Module: Mathlib.Analysis.Calculus.FDeriv.Congr
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f f₁ : E → F
f' : E →L[𝕜] F
x : E
s t : Set E
h : HasFDerivWithinAt f f' s x
ht : EqOn f₁ f t
hx : f₁ x = f x
h₁ : t ⊆ s
⊢ HasFDerivWithinAt f₁ f' t x

Tactic:
h.mono h₁ |>.congr ht hx

Premises used: HasFDerivWithinAt.mono, HasFDerivWithinAt.congr
-- Module: Mathlib.Analysis.Calculus.FDeriv.Congr
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f f₁ : E → F
f' : E →L[𝕜] F
x : E
h : HasFDerivAt f f' x
h₁ : f₁ =ᶠ[𝓝 x] f
⊢ HasFDerivAt f₁ f' x

Tactic:
h₁.hasFDerivAt_iff.mpr h

Premises used: Iff.mpr, Filter.EventuallyEq.hasFDerivAt_iff
-- Module: Mathlib.Analysis.Calculus.FDeriv.Congr
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f f₁ : E → F
x : E
s t : Set E
h : DifferentiableWithinAt 𝕜 f s x
ht : EqOn f₁ f t
hx : f₁ x = f x
h₁ : t ⊆ s
⊢ DifferentiableWithinAt 𝕜 f₁ t x

Tactic:
(HasFDerivWithinAt.congr_mono h.hasFDerivWithinAt ht hx h₁).differentiableWithinAt

Premises used: HasFDerivWithinAt.differentiableWithinAt, HasFDerivWithinAt.congr_mono, DifferentiableWithinAt.hasFDerivWithinAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Congr
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f f₁ : E → F
x : E
s : Set E
h : DifferentiableWithinAt 𝕜 f s x
ht : ∀ x ∈ s, f₁ x = f x
hx : f₁ x = f x
⊢ DifferentiableWithinAt 𝕜 f₁ s x

Tactic:
DifferentiableWithinAt.congr_mono h ht hx (Subset.refl _)

Premises used: Set.Subset.refl, DifferentiableWithinAt.congr_mono
-- Module: Mathlib.Analysis.Calculus.FDeriv.Congr
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f f₁ : E → F
x : E
s : Set E
h : DifferentiableWithinAt 𝕜 f s x
h₁ : f₁ =ᶠ[𝓝[s] x] f
hx : f₁ x = f x
⊢ DifferentiableWithinAt 𝕜 f₁ s x

Tactic:
(h.hasFDerivWithinAt.congr_of_eventuallyEq h₁ hx).differentiableWithinAt

Premises used: HasFDerivWithinAt.congr_of_eventuallyEq, HasFDerivWithinAt.differentiableWithinAt, DifferentiableWithinAt.hasFDerivWithinAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Congr
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f f₁ : E → F
x : E
s : Set E
h : DifferentiableWithinAt 𝕜 f s x
h₁ : f₁ =ᶠ[𝓝[s] x] f
hx : x ∈ s
⊢ DifferentiableWithinAt 𝕜 f₁ s x

Tactic:
h.congr_of_eventuallyEq h₁ (mem_of_mem_nhdsWithin hx h₁ :)

Premises used: DifferentiableWithinAt.congr_of_eventuallyEq, mem_of_mem_nhdsWithin
-- Module: Mathlib.Analysis.Calculus.FDeriv.Congr
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f f₁ : E → F
x : E
s : Set E
h : DifferentiableWithinAt 𝕜 f s x
h₁ : f₁ =ᶠ[𝓝[insert x s] x] f
⊢ DifferentiableWithinAt 𝕜 f₁ s x

Tactic:
(h.insert.congr_of_eventuallyEq_of_mem h₁ (mem_insert _ _)).of_insert

Premises used: DifferentiableWithinAt.of_insert, DifferentiableWithinAt.insert, Set.mem_insert, DifferentiableWithinAt.congr_of_eventuallyEq_of_mem
-- Module: Mathlib.Analysis.Calculus.FDeriv.Congr
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f f₁ : E → F
s t : Set E
h : DifferentiableOn 𝕜 f s
h' : ∀ x ∈ t, f₁ x = f x
h₁ : t ⊆ s
⊢ DifferentiableOn 𝕜 f₁ t

Tactic:
fun x hx => (h x (h₁ hx)).congr_mono h' (h' x hx) h₁

Premises used: DifferentiableWithinAt.congr_mono, DifferentiableOn
-- Module: Mathlib.Analysis.Calculus.FDeriv.Congr
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f f₁ : E → F
s : Set E
h : DifferentiableOn 𝕜 f s
h' : ∀ x ∈ s, f₁ x = f x
⊢ DifferentiableOn 𝕜 f₁ s

Tactic:
fun x hx => (h x hx).congr h' (h' x hx)

Premises used: DifferentiableWithinAt.congr, DifferentiableOn
-- Module: Mathlib.Analysis.Calculus.FDeriv.Congr
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f f₁ : E → F
s : Set E
h' : ∀ x ∈ s, f₁ x = f x
⊢ DifferentiableOn 𝕜 f₁ s ↔ DifferentiableOn 𝕜 f s

Tactic:
⟨fun h => DifferentiableOn.congr h fun y hy => (h' y hy).symm, fun h =>
    DifferentiableOn.congr h h'⟩

Premises used: DifferentiableOn.congr, Iff.intro, Eq.symm
-- Module: Mathlib.Analysis.Calculus.FDeriv.Congr
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f f₁ : E → F
x : E
h : DifferentiableAt 𝕜 f x
hL : f₁ =ᶠ[𝓝 x] f
⊢ DifferentiableAt 𝕜 f₁ x

Tactic:
hL.differentiableAt_iff.2 h

Premises used: Iff.mpr, Filter.EventuallyEq.differentiableAt_iff