awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.FDeriv.OfCompLeft
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
g : E → F
f : F → G
h : E → G
f' : F →L[𝕜] G
h' : E →L[𝕜] G
f'symm : G →L[𝕜] F
a : E
hgc : ContinuousAt g a
hf : HasStrictFDerivAt f f' (g a)
hh : HasStrictFDerivAt h h' a
hcomp : f ∘ g =ᶠ[𝓝 a] h
hf'symm : Function.LeftInverse.{u_3 + 1, u_4 + 1} (α := F) (β := G) (⇑f'symm : (a : G) → F) (⇑f' : (a : F) → G)
⊢ HasStrictFDerivAt g (f'symm ∘SL h') a

Tactic:
HasFDerivAtFilter.of_comp_of_leftInverse (hgc.prodMap_nhds hgc) hf hh
    (hcomp.prodMap_nhds hcomp) hf'symm

Premises used: HasFDerivAtFilter.of_comp_of_leftInverse, HasStrictFDerivAt, Filter.EventuallyEq.prodMap_nhds, Filter.Tendsto.prodMap_nhds
-- Module: Mathlib.Analysis.Calculus.FDeriv.OfCompLeft
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
g : E → F
f : F → G
h : E → G
g' : E →L[𝕜] F
f' : F →L[𝕜] G
lE : Filter (E × E)
lF : Filter (F × F)
hg : Tendsto (Prod.map g g) lE lF
hf : HasFDerivAtFilter f f' lF
hf' : Topology.IsEmbedding.{u_3, u_4} (X := F) (Y := G) (⇑f' : (a : F) → G)
hh : HasFDerivAtFilter h (f' ∘SL g') lE
hcomp : Prod.map (f ∘ g) (f ∘ g) =ᶠ[lE] Prod.map h h
hf_emb : Topology.IsEmbedding.{u_3, u_4} (X := F) (Y := G) (⇑f' : (a : F) → G)
htendsto : Tendsto (Prod.map g g) lE lF
hh₁ : HasFDerivAtFilter h (f' ∘SL g') lE
hf₁ : HasFDerivAtFilter f f' lF
hcomp₁ : Prod.map (f ∘ g) (f ∘ g) =ᶠ[lE] Prod.map h h
ho :
  Asymptotics.IsBigOTVS.{u_1, u_2, u_3, u_4} 𝕜 (E := F) (F := G) lE
    (fun (x : E × E) ↦
      match (motive := E × E → F) x with
      | (x, y) => HSub.hSub (β := F) (g x - g y) ((g' : (a : E) → F) (x - y) : F))
    fun (x : E × E) ↦
    match (motive := E × E → G) x with
    | (x, y) => HSub.hSub (α := G) (β := G) ((f' : (a : F) → G) (g x - g y) : G) ((f' ∘SL g' : (a : E) → G) (x - y) : G)
apply : E → G
apply₁ : E →L[𝕜] G
apply₂ : Filter (F × F)
⊢ HasFDerivAtFilter g g' lE

Tactic:
apply of_comp_aux (f := f) (f' := f')

Premises used: _private.0.HasFDerivAtFilter.of_comp_aux
-- Module: Mathlib.Analysis.Calculus.FDeriv.OfCompLeft
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
g : E → F
f : F → G
h : E → G
g' : E →L[𝕜] F
f' : F →L[𝕜] G
lE : Filter (E × E)
lF : Filter (F × F)
hg : Tendsto (Prod.map g g) lE lF
hf : HasFDerivAtFilter f f' lF
hf' : Topology.IsEmbedding.{u_3, u_4} (X := F) (Y := G) (⇑f' : (a : F) → G)
hh : HasFDerivAtFilter h (f' ∘SL g') lE
hcomp : Prod.map (f ∘ g) (f ∘ g) =ᶠ[lE] Prod.map h h
⊢ Topology.IsEmbedding.{u_3, u_4} (X := F) (Y := G) (⇑f' : (a : F) → G)

Tactic:
assumption
-- Module: Mathlib.Analysis.Calculus.FDeriv.OfCompLeft
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
g : E → F
f : F → G
h : E → G
g' : E →L[𝕜] F
f' : F →L[𝕜] G
lE : Filter (E × E)
lF : Filter (F × F)
hg : Tendsto (Prod.map g g) lE lF
hf : HasFDerivAtFilter f f' lF
hf' : Topology.IsEmbedding.{u_3, u_4} (X := F) (Y := G) (⇑f' : (a : F) → G)
hh : HasFDerivAtFilter h (f' ∘SL g') lE
hcomp : Prod.map (f ∘ g) (f ∘ g) =ᶠ[lE] Prod.map h h
⊢ Topology.IsEmbedding.{u_3, u_4} (X := F) (Y := G) (⇑f' : (a : F) → G)

Tactic:
try assumption
-- Module: Mathlib.Analysis.Calculus.FDeriv.OfCompLeft
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
g : E → F
f : F → G
h : E → G
g' : E →L[𝕜] F
f' : F →L[𝕜] G
lE : Filter (E × E)
lF : Filter (F × F)
hg : Tendsto (Prod.map g g) lE lF
hf : HasFDerivAtFilter f f' lF
hf' : Topology.IsEmbedding.{u_3, u_4} (X := F) (Y := G) (⇑f' : (a : F) → G)
hh : HasFDerivAtFilter h (f' ∘SL g') lE
hcomp : Prod.map (f ∘ g) (f ∘ g) =ᶠ[lE] Prod.map h h
⊢ Tendsto (Prod.map g g) lE lF

Tactic:
assumption
-- Module: Mathlib.Analysis.Calculus.FDeriv.OfCompLeft
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
g : E → F
f : F → G
h : E → G
g' : E →L[𝕜] F
f' : F →L[𝕜] G
lE : Filter (E × E)
lF : Filter (F × F)
hg : Tendsto (Prod.map g g) lE lF
hf : HasFDerivAtFilter f f' lF
hf' : Topology.IsEmbedding.{u_3, u_4} (X := F) (Y := G) (⇑f' : (a : F) → G)
hh : HasFDerivAtFilter h (f' ∘SL g') lE
hcomp : Prod.map (f ∘ g) (f ∘ g) =ᶠ[lE] Prod.map h h
⊢ Tendsto (Prod.map g g) lE lF

Tactic:
try assumption
-- Module: Mathlib.Analysis.Calculus.FDeriv.OfCompLeft
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
g : E → F
f : F → G
h : E → G
g' : E →L[𝕜] F
f' : F →L[𝕜] G
lE : Filter (E × E)
lF : Filter (F × F)
hg : Tendsto (Prod.map g g) lE lF
hf : HasFDerivAtFilter f f' lF
hf' : Topology.IsEmbedding.{u_3, u_4} (X := F) (Y := G) (⇑f' : (a : F) → G)
hh : HasFDerivAtFilter h (f' ∘SL g') lE
hcomp : Prod.map (f ∘ g) (f ∘ g) =ᶠ[lE] Prod.map h h
⊢ HasFDerivAtFilter h (f' ∘SL g') lE

Tactic:
assumption
-- Module: Mathlib.Analysis.Calculus.FDeriv.OfCompLeft
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
g : E → F
f : F → G
h : E → G
g' : E →L[𝕜] F
f' : F →L[𝕜] G
lE : Filter (E × E)
lF : Filter (F × F)
hg : Tendsto (Prod.map g g) lE lF
hf : HasFDerivAtFilter f f' lF
hf' : Topology.IsEmbedding.{u_3, u_4} (X := F) (Y := G) (⇑f' : (a : F) → G)
hh : HasFDerivAtFilter h (f' ∘SL g') lE
hcomp : Prod.map (f ∘ g) (f ∘ g) =ᶠ[lE] Prod.map h h
⊢ HasFDerivAtFilter h (f' ∘SL g') lE

Tactic:
try assumption
-- Module: Mathlib.Analysis.Calculus.FDeriv.OfCompLeft
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
g : E → F
f : F → G
h : E → G
g' : E →L[𝕜] F
f' : F →L[𝕜] G
lE : Filter (E × E)
lF : Filter (F × F)
hg : Tendsto (Prod.map g g) lE lF
hf : HasFDerivAtFilter f f' lF
hf' : Topology.IsEmbedding.{u_3, u_4} (X := F) (Y := G) (⇑f' : (a : F) → G)
hh : HasFDerivAtFilter h (f' ∘SL g') lE
hcomp : Prod.map (f ∘ g) (f ∘ g) =ᶠ[lE] Prod.map h h
⊢ HasFDerivAtFilter f f' lF

Tactic:
assumption
-- Module: Mathlib.Analysis.Calculus.FDeriv.OfCompLeft
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
g : E → F
f : F → G
h : E → G
g' : E →L[𝕜] F
f' : F →L[𝕜] G
lE : Filter (E × E)
lF : Filter (F × F)
hg : Tendsto (Prod.map g g) lE lF
hf : HasFDerivAtFilter f f' lF
hf' : Topology.IsEmbedding.{u_3, u_4} (X := F) (Y := G) (⇑f' : (a : F) → G)
hh : HasFDerivAtFilter h (f' ∘SL g') lE
hcomp : Prod.map (f ∘ g) (f ∘ g) =ᶠ[lE] Prod.map h h
⊢ HasFDerivAtFilter f f' lF

Tactic:
try assumption
-- Module: Mathlib.Analysis.Calculus.FDeriv.OfCompLeft
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
g : E → F
f : F → G
h : E → G
g' : E →L[𝕜] F
f' : F →L[𝕜] G
lE : Filter (E × E)
lF : Filter (F × F)
hg : Tendsto (Prod.map g g) lE lF
hf : HasFDerivAtFilter f f' lF
hf' : Topology.IsEmbedding.{u_3, u_4} (X := F) (Y := G) (⇑f' : (a : F) → G)
hh : HasFDerivAtFilter h (f' ∘SL g') lE
hcomp : Prod.map (f ∘ g) (f ∘ g) =ᶠ[lE] Prod.map h h
⊢ Prod.map (f ∘ g) (f ∘ g) =ᶠ[lE] Prod.map h h

Tactic:
assumption
-- Module: Mathlib.Analysis.Calculus.FDeriv.OfCompLeft
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
g : E → F
f : F → G
h : E → G
g' : E →L[𝕜] F
f' : F →L[𝕜] G
lE : Filter (E × E)
lF : Filter (F × F)
hg : Tendsto (Prod.map g g) lE lF
hf : HasFDerivAtFilter f f' lF
hf' : Topology.IsEmbedding.{u_3, u_4} (X := F) (Y := G) (⇑f' : (a : F) → G)
hh : HasFDerivAtFilter h (f' ∘SL g') lE
hcomp : Prod.map (f ∘ g) (f ∘ g) =ᶠ[lE] Prod.map h h
⊢ Prod.map (f ∘ g) (f ∘ g) =ᶠ[lE] Prod.map h h

Tactic:
try assumption
-- Module: Mathlib.Analysis.Calculus.FDeriv.OfCompLeft
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
g : E → F
f : F → G
h : E → G
g' : E →L[𝕜] F
f' : F →L[𝕜] G
lE : Filter (E × E)
lF : Filter (F × F)
hg : Tendsto (Prod.map g g) lE lF
hf : HasFDerivAtFilter f f' lF
hf' : Topology.IsEmbedding.{u_3, u_4} (X := F) (Y := G) (⇑f' : (a : F) → G)
hh : HasFDerivAtFilter h (f' ∘SL g') lE
hcomp : Prod.map (f ∘ g) (f ∘ g) =ᶠ[lE] Prod.map h h
⊢ Asymptotics.IsBigOTVS.{u_1, u_2, u_3, u_4} 𝕜 (E := F) (F := G) lE
    (fun (x : E × E) ↦
      match (motive := E × E → F) x with
      | (x, y) => HSub.hSub (β := F) (g x - g y) ((g' : (a : E) → F) (x - y) : F))
    fun (x : E × E) ↦
    match (motive := E × E → G) x with
    | (x, y) => HSub.hSub (α := G) (β := G) ((f' : (a : F) → G) (g x - g y) : G) ((f' ∘SL g' : (a : E) → G) (x - y) : G)

Tactic:
f'.isThetaTVS_comp hf'.isInducing |>.symm.isBigOTVS.congr_right ?_

Premises used: Topology.IsEmbedding.isInducing, Asymptotics.IsBigOTVS.congr_right, Asymptotics.IsThetaTVS.isBigOTVS, Asymptotics.IsThetaTVS.symm, ContinuousLinearMap.isThetaTVS_comp
-- Module: Mathlib.Analysis.Calculus.FDeriv.OfCompLeft
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
g : E → F
f : F → G
h : E → G
g' : E →L[𝕜] F
f' : F →L[𝕜] G
lE : Filter (E × E)
lF : Filter (F × F)
hg : Tendsto (Prod.map g g) lE lF
hf : HasFDerivAtFilter f f' lF
hf' : Topology.IsEmbedding.{u_3, u_4} (X := F) (Y := G) (⇑f' : (a : F) → G)
hh : HasFDerivAtFilter h (f' ∘SL g') lE
hcomp : Prod.map (f ∘ g) (f ∘ g) =ᶠ[lE] Prod.map h h
ho :
  ∀ (x : E × E),
    Eq.{u_4 + 1} (α := G)
      (Function.comp.{u_2 + 1, u_3 + 1, u_4 + 1} (β := F) (⇑f' : (a : F) → G)
          (fun (x : E × E) ↦
            match (motive := E × E → F) x with
            | (x, y) => HSub.hSub (β := F) (g x - g y) ((g' : (a : E) → F) (x - y) : F))
          x :
        G)
      (match (motive := E × E → G) x with
        | (x, y) =>
          HSub.hSub (α := G) (β := G) ((f' : (a : F) → G) (g x - g y) : G) ((f' ∘SL g' : (a : E) → G) (x - y) : G) :
        G)
⊢ Asymptotics.IsBigOTVS.{u_1, u_2, u_3, u_4} 𝕜 (E := F) (F := G) lE
    (fun (x : E × E) ↦
      match (motive := E × E → F) x with
      | (x, y) => HSub.hSub (β := F) (g x - g y) ((g' : (a : E) → F) (x - y) : F))
    fun (x : E × E) ↦
    match (motive := E × E → G) x with
    | (x, y) => HSub.hSub (α := G) (β := G) ((f' : (a : F) → G) (g x - g y) : G) ((f' ∘SL g' : (a : E) → G) (x - y) : G)

Tactic:
refine f'.isThetaTVS_comp hf'.isInducing |>.symm.isBigOTVS.congr_right ?_

Premises used: Topology.IsEmbedding.isInducing, Asymptotics.IsBigOTVS.congr_right, Asymptotics.IsThetaTVS.isBigOTVS, Asymptotics.IsThetaTVS.symm, ContinuousLinearMap.isThetaTVS_comp
-- Module: Mathlib.Analysis.Calculus.FDeriv.OfCompLeft
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
g : E → F
f : F → G
h : E → G
g' : E →L[𝕜] F
f' : F →L[𝕜] G
lE : Filter (E × E)
lF : Filter (F × F)
hg : Tendsto (Prod.map g g) lE lF
hf : HasFDerivAtFilter f f' lF
hf' : Topology.IsEmbedding.{u_3, u_4} (X := F) (Y := G) (⇑f' : (a : F) → G)
hh : HasFDerivAtFilter h (f' ∘SL g') lE
hcomp : Prod.map (f ∘ g) (f ∘ g) =ᶠ[lE] Prod.map h h
⊢ ∀ (x : E × E),
    Eq.{u_4 + 1} (α := G)
      (Function.comp.{u_2 + 1, u_3 + 1, u_4 + 1} (β := F) (⇑f' : (a : F) → G)
          (fun (x : E × E) ↦
            match (motive := E × E → F) x with
            | (x, y) => HSub.hSub (β := F) (g x - g y) ((g' : (a : E) → F) (x - y) : F))
          x :
        G)
      (match (motive := E × E → G) x with
        | (x, y) =>
          HSub.hSub (α := G) (β := G) ((f' : (a : F) → G) (g x - g y) : G) ((f' ∘SL g' : (a : E) → G) (x - y) : G) :
        G)

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.FDeriv.OfCompLeft
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
g : E → F
f : F → G
h : E → G
g' : E →L[𝕜] F
f' : F →L[𝕜] G
a : E
s : Set E
t : Set F
hg : Tendsto g (𝓝[s] a) (𝓝[t] g a)
hf : HasFDerivWithinAt f f' t (g a)
hf' : Topology.IsEmbedding.{u_3, u_4} (X := F) (Y := G) (⇑f' : (a : F) → G)
hh : HasFDerivWithinAt h (f' ∘SL g') s a
hcomp : f ∘ g =ᶠ[𝓝[s] a] h
ha : a ∈ s
⊢ HasFDerivWithinAt g g' s a

Tactic:
HasFDerivAtFilter.of_comp_of_isEmbedding ?_ hf hf' hh ?_

Premises used: HasFDerivAtFilter.of_comp_of_isEmbedding, HasFDerivWithinAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.OfCompLeft
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
g : E → F
f : F → G
h : E → G
g' : E →L[𝕜] F
f' : F →L[𝕜] G
a : E
s : Set E
t : Set F
hg : Tendsto g (𝓝[s] a) (𝓝[t] g a)
hf : HasFDerivWithinAt f f' t (g a)
hf' : Topology.IsEmbedding.{u_3, u_4} (X := F) (Y := G) (⇑f' : (a : F) → G)
hh : HasFDerivWithinAt h (f' ∘SL g') s a
hcomp : f ∘ g =ᶠ[𝓝[s] a] h
ha : a ∈ s
refine_1 :
  Tendsto (Prod.map g g) (SProd.sprod (β := Filter E) (𝓝[s] a) (pure a))
    (SProd.sprod (β := Filter F) (𝓝[t] g a) (pure (g a)))
refine_2 : Prod.map (f ∘ g) (f ∘ g) =ᶠ[SProd.sprod (β := Filter E) (𝓝[s] a) (pure a)] Prod.map h h
⊢ HasFDerivWithinAt g g' s a

Tactic:
refine HasFDerivAtFilter.of_comp_of_isEmbedding ?_ hf hf' hh ?_

Premises used: HasFDerivAtFilter.of_comp_of_isEmbedding
-- Module: Mathlib.Analysis.Calculus.FDeriv.OfCompLeft
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
g : E → F
f : F → G
h : E → G
g' : E →L[𝕜] F
f' : F →L[𝕜] G
a : E
s : Set E
t : Set F
hg : Tendsto g (𝓝[s] a) (𝓝[t] g a)
hf : HasFDerivWithinAt f f' t (g a)
hf' : Topology.IsEmbedding.{u_3, u_4} (X := F) (Y := G) (⇑f' : (a : F) → G)
hh : HasFDerivWithinAt h (f' ∘SL g') s a
hcomp : f ∘ g =ᶠ[𝓝[s] a] h
ha : a ∈ s
⊢ Tendsto g (pure a) (pure (g a))

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.FDeriv.OfCompLeft
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
g : E → F
f : F → G
h : E → G
g' : E →L[𝕜] F
f' : F →L[𝕜] G
a : E
s : Set E
t : Set F
hg : Tendsto g (𝓝[s] a) (𝓝[t] g a)
hf : HasFDerivWithinAt f f' t (g a)
hf' : Topology.IsEmbedding.{u_3, u_4} (X := F) (Y := G) (⇑f' : (a : F) → G)
hh : HasFDerivWithinAt h (f' ∘SL g') s a
hcomp : f ∘ g =ᶠ[𝓝[s] a] h
ha : a ∈ s
⊢ Tendsto (Prod.map g g) (SProd.sprod (β := Filter E) (𝓝[s] a) (pure a))
    (SProd.sprod (β := Filter F) (𝓝[t] g a) (pure (g a)))

Tactic:
exact hg.prodMap (by simp)

Premises used: Filter.Tendsto.prodMap
-- Module: Mathlib.Analysis.Calculus.FDeriv.OfCompLeft
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
g : E → F
f : F → G
h : E → G
g' : E →L[𝕜] F
f' : F →L[𝕜] G
a : E
s : Set E
t : Set F
hg : Tendsto g (𝓝[s] a) (𝓝[t] g a)
hf : HasFDerivWithinAt f f' t (g a)
hf' : Topology.IsEmbedding.{u_3, u_4} (X := F) (Y := G) (⇑f' : (a : F) → G)
hh : HasFDerivWithinAt h (f' ∘SL g') s a
hcomp : f ∘ g =ᶠ[𝓝[s] a] h
ha : a ∈ s
⊢ Prod.map (f ∘ g) (f ∘ g) =ᶠ[SProd.sprod (β := Filter E) (𝓝[s] a) (pure a)] Prod.map h h

Tactic:
hcomp.prodMap <| hcomp.self_of_nhdsWithin ha

Premises used: Filter.Eventually.self_of_nhdsWithin, Filter.EventuallyEq.prodMap
-- Module: Mathlib.Analysis.Calculus.FDeriv.OfCompLeft
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
g : E → F
f : F → G
h : E → G
g' : E →L[𝕜] F
f' : F →L[𝕜] G
a : E
s : Set E
t : Set F
hg : Tendsto g (𝓝[s] a) (𝓝[t] g a)
hf : HasFDerivWithinAt f f' t (g a)
hf' : Topology.IsEmbedding.{u_3, u_4} (X := F) (Y := G) (⇑f' : (a : F) → G)
hh : HasFDerivWithinAt h (f' ∘SL g') s a
hcomp : f ∘ g =ᶠ[𝓝[s] a] h
ha : a ∈ s
⊢ Prod.map (f ∘ g) (f ∘ g) =ᶠ[SProd.sprod (β := Filter E) (𝓝[s] a) (pure a)] Prod.map h h

Tactic:
exact hcomp.prodMap <| hcomp.self_of_nhdsWithin ha

Premises used: Filter.Eventually.self_of_nhdsWithin, Filter.EventuallyEq.prodMap
-- Module: Mathlib.Analysis.Calculus.FDeriv.OfCompLeft
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
g : E → F
f : F → G
h : E → G
g' : E →L[𝕜] F
f' : F →L[𝕜] G
a : E
hg : ContinuousAt g a
hf : HasFDerivAt f f' (g a)
hf' : Topology.IsEmbedding.{u_3, u_4} (X := F) (Y := G) (⇑f' : (a : F) → G)
hh : HasFDerivAt h (f' ∘SL g') a
hcomp : f ∘ g =ᶠ[𝓝 a] h
⊢ HasFDerivAt g g' a

Tactic:
HasFDerivAtFilter.of_comp_of_isEmbedding ?_ hf hf' hh ?_

Premises used: HasFDerivAt, HasFDerivAtFilter.of_comp_of_isEmbedding
-- Module: Mathlib.Analysis.Calculus.FDeriv.OfCompLeft
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
g : E → F
f : F → G
h : E → G
g' : E →L[𝕜] F
f' : F →L[𝕜] G
a : E
hg : ContinuousAt g a
hf : HasFDerivAt f f' (g a)
hf' : Topology.IsEmbedding.{u_3, u_4} (X := F) (Y := G) (⇑f' : (a : F) → G)
hh : HasFDerivAt h (f' ∘SL g') a
hcomp : f ∘ g =ᶠ[𝓝 a] h
refine_1 :
  Tendsto (Prod.map g g) (SProd.sprod (β := Filter E) (𝓝 a) (pure a))
    (SProd.sprod (β := Filter F) (𝓝 (g a)) (pure (g a)))
refine_2 : Prod.map (f ∘ g) (f ∘ g) =ᶠ[SProd.sprod (β := Filter E) (𝓝 a) (pure a)] Prod.map h h
⊢ HasFDerivAt g g' a

Tactic:
refine HasFDerivAtFilter.of_comp_of_isEmbedding ?_ hf hf' hh ?_

Premises used: HasFDerivAtFilter.of_comp_of_isEmbedding
-- Module: Mathlib.Analysis.Calculus.FDeriv.OfCompLeft
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
g : E → F
f : F → G
h : E → G
g' : E →L[𝕜] F
f' : F →L[𝕜] G
a : E
hg : ContinuousAt g a
hf : HasFDerivAt f f' (g a)
hf' : Topology.IsEmbedding.{u_3, u_4} (X := F) (Y := G) (⇑f' : (a : F) → G)
hh : HasFDerivAt h (f' ∘SL g') a
hcomp : f ∘ g =ᶠ[𝓝 a] h
⊢ Tendsto g (pure a) (pure (g a))

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.FDeriv.OfCompLeft
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
g : E → F
f : F → G
h : E → G
g' : E →L[𝕜] F
f' : F →L[𝕜] G
a : E
hg : ContinuousAt g a
hf : HasFDerivAt f f' (g a)
hf' : Topology.IsEmbedding.{u_3, u_4} (X := F) (Y := G) (⇑f' : (a : F) → G)
hh : HasFDerivAt h (f' ∘SL g') a
hcomp : f ∘ g =ᶠ[𝓝 a] h
⊢ Tendsto (Prod.map g g) (SProd.sprod (β := Filter E) (𝓝 a) (pure a))
    (SProd.sprod (β := Filter F) (𝓝 (g a)) (pure (g a)))

Tactic:
exact hg.tendsto.prodMap (by simp)

Premises used: ContinuousAt.tendsto, Filter.Tendsto.prodMap
-- Module: Mathlib.Analysis.Calculus.FDeriv.OfCompLeft
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
g : E → F
f : F → G
h : E → G
g' : E →L[𝕜] F
f' : F →L[𝕜] G
a : E
hg : ContinuousAt g a
hf : HasFDerivAt f f' (g a)
hf' : Topology.IsEmbedding.{u_3, u_4} (X := F) (Y := G) (⇑f' : (a : F) → G)
hh : HasFDerivAt h (f' ∘SL g') a
hcomp : f ∘ g =ᶠ[𝓝 a] h
⊢ Prod.map (f ∘ g) (f ∘ g) =ᶠ[SProd.sprod (β := Filter E) (𝓝 a) (pure a)] Prod.map h h

Tactic:
hcomp.prodMap hcomp.self_of_nhds

Premises used: Filter.Eventually.self_of_nhds, Filter.EventuallyEq.prodMap
-- Module: Mathlib.Analysis.Calculus.FDeriv.OfCompLeft
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
g : E → F
f : F → G
h : E → G
g' : E →L[𝕜] F
f' : F →L[𝕜] G
a : E
hg : ContinuousAt g a
hf : HasFDerivAt f f' (g a)
hf' : Topology.IsEmbedding.{u_3, u_4} (X := F) (Y := G) (⇑f' : (a : F) → G)
hh : HasFDerivAt h (f' ∘SL g') a
hcomp : f ∘ g =ᶠ[𝓝 a] h
⊢ Prod.map (f ∘ g) (f ∘ g) =ᶠ[SProd.sprod (β := Filter E) (𝓝 a) (pure a)] Prod.map h h

Tactic:
exact hcomp.prodMap hcomp.self_of_nhds
-- Module: Mathlib.Analysis.Calculus.FDeriv.OfCompLeft
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
g : E → F
f : F → G
h : E → G
g' : E →L[𝕜] F
f' : F →L[𝕜] G
a : E
hg : ContinuousAt g a
hf : HasStrictFDerivAt f f' (g a)
hf' : Topology.IsEmbedding.{u_3, u_4} (X := F) (Y := G) (⇑f' : (a : F) → G)
hh : HasStrictFDerivAt h (f' ∘SL g') a
hcomp : f ∘ g =ᶠ[𝓝 a] h
⊢ HasStrictFDerivAt g g' a

Tactic:
HasFDerivAtFilter.of_comp_of_isEmbedding (hg.prodMap hg) hf hf' hh (hcomp.prodMap_nhds hcomp)

Premises used: ContinuousAt.prodMap, HasFDerivAtFilter.of_comp_of_isEmbedding, HasStrictFDerivAt, Filter.EventuallyEq.prodMap_nhds