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
lE : Filter (E × E)
lF : Filter (F × F)
hg : Tendsto (Prod.map g g) lE lF
hf : HasFDerivAtFilter f f' lF
hh : HasFDerivAtFilter h h' lE
hcomp : Prod.map (f ∘ g) (f ∘ g) =ᶠ[lE] Prod.map h h
hf'symm : Function.LeftInverse.{u_3 + 1, u_4 + 1} (α := F) (β := G) (⇑f'symm : (a : G) → F) (⇑f' : (a : F) → G)
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 h' 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) ((f'symm ∘SL h' : (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) ((h' : (a : E) → G) (x - y) : G)
apply : E → G
apply₁ : E →L[𝕜] G
apply₂ : Filter (F × F)
⊢ HasFDerivAtFilter g (f'symm ∘SL h') 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
f' : F →L[𝕜] G
h' : E →L[𝕜] G
f'symm : G →L[𝕜] F
lE : Filter (E × E)
lF : Filter (F × F)
hg : Tendsto (Prod.map g g) lE lF
hf : HasFDerivAtFilter f f' lF
hh : HasFDerivAtFilter h h' lE
hcomp : Prod.map (f ∘ g) (f ∘ g) =ᶠ[lE] Prod.map h h
hf'symm : Function.LeftInverse.{u_3 + 1, u_4 + 1} (α := F) (β := G) (⇑f'symm : (a : G) → F) (⇑f' : (a : F) → G)
⊢ 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
f' : F →L[𝕜] G
h' : E →L[𝕜] G
f'symm : G →L[𝕜] F
lE : Filter (E × E)
lF : Filter (F × F)
hg : Tendsto (Prod.map g g) lE lF
hf : HasFDerivAtFilter f f' lF
hh : HasFDerivAtFilter h h' lE
hcomp : Prod.map (f ∘ g) (f ∘ g) =ᶠ[lE] Prod.map h h
hf'symm : Function.LeftInverse.{u_3 + 1, u_4 + 1} (α := F) (β := G) (⇑f'symm : (a : G) → F) (⇑f' : (a : F) → G)
⊢ 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
f' : F →L[𝕜] G
h' : E →L[𝕜] G
f'symm : G →L[𝕜] F
lE : Filter (E × E)
lF : Filter (F × F)
hg : Tendsto (Prod.map g g) lE lF
hf : HasFDerivAtFilter f f' lF
hh : HasFDerivAtFilter h h' lE
hcomp : Prod.map (f ∘ g) (f ∘ g) =ᶠ[lE] Prod.map h h
hf'symm : Function.LeftInverse.{u_3 + 1, u_4 + 1} (α := F) (β := G) (⇑f'symm : (a : G) → F) (⇑f' : (a : F) → G)
⊢ HasFDerivAtFilter h h' 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
f' : F →L[𝕜] G
h' : E →L[𝕜] G
f'symm : G →L[𝕜] F
lE : Filter (E × E)
lF : Filter (F × F)
hg : Tendsto (Prod.map g g) lE lF
hf : HasFDerivAtFilter f f' lF
hh : HasFDerivAtFilter h h' lE
hcomp : Prod.map (f ∘ g) (f ∘ g) =ᶠ[lE] Prod.map h h
hf'symm : Function.LeftInverse.{u_3 + 1, u_4 + 1} (α := F) (β := G) (⇑f'symm : (a : G) → F) (⇑f' : (a : F) → G)
⊢ HasFDerivAtFilter h h' 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
f' : F →L[𝕜] G
h' : E →L[𝕜] G
f'symm : G →L[𝕜] F
lE : Filter (E × E)
lF : Filter (F × F)
hg : Tendsto (Prod.map g g) lE lF
hf : HasFDerivAtFilter f f' lF
hh : HasFDerivAtFilter h h' lE
hcomp : Prod.map (f ∘ g) (f ∘ g) =ᶠ[lE] Prod.map h h
hf'symm : Function.LeftInverse.{u_3 + 1, u_4 + 1} (α := F) (β := G) (⇑f'symm : (a : G) → F) (⇑f' : (a : F) → G)
⊢ 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
f' : F →L[𝕜] G
h' : E →L[𝕜] G
f'symm : G →L[𝕜] F
lE : Filter (E × E)
lF : Filter (F × F)
hg : Tendsto (Prod.map g g) lE lF
hf : HasFDerivAtFilter f f' lF
hh : HasFDerivAtFilter h h' lE
hcomp : Prod.map (f ∘ g) (f ∘ g) =ᶠ[lE] Prod.map h h
hf'symm : Function.LeftInverse.{u_3 + 1, u_4 + 1} (α := F) (β := G) (⇑f'symm : (a : G) → F) (⇑f' : (a : F) → G)
⊢ 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
f' : F →L[𝕜] G
h' : E →L[𝕜] G
f'symm : G →L[𝕜] F
lE : Filter (E × E)
lF : Filter (F × F)
hg : Tendsto (Prod.map g g) lE lF
hf : HasFDerivAtFilter f f' lF
hh : HasFDerivAtFilter h h' lE
hcomp : Prod.map (f ∘ g) (f ∘ g) =ᶠ[lE] Prod.map h h
hf'symm : Function.LeftInverse.{u_3 + 1, u_4 + 1} (α := F) (β := G) (⇑f'symm : (a : G) → F) (⇑f' : (a : F) → G)
⊢ 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
f' : F →L[𝕜] G
h' : E →L[𝕜] G
f'symm : G →L[𝕜] F
lE : Filter (E × E)
lF : Filter (F × F)
hg : Tendsto (Prod.map g g) lE lF
hf : HasFDerivAtFilter f f' lF
hh : HasFDerivAtFilter h h' lE
hcomp : Prod.map (f ∘ g) (f ∘ g) =ᶠ[lE] Prod.map h h
hf'symm : Function.LeftInverse.{u_3 + 1, u_4 + 1} (α := F) (β := G) (⇑f'symm : (a : G) → F) (⇑f' : (a : F) → G)
⊢ 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
f' : F →L[𝕜] G
h' : E →L[𝕜] G
f'symm : G →L[𝕜] F
lE : Filter (E × E)
lF : Filter (F × F)
hg : Tendsto (Prod.map g g) lE lF
hf : HasFDerivAtFilter f f' lF
hh : HasFDerivAtFilter h h' lE
hcomp : Prod.map (f ∘ g) (f ∘ g) =ᶠ[lE] Prod.map h h
hf'symm : Function.LeftInverse.{u_3 + 1, u_4 + 1} (α := F) (β := G) (⇑f'symm : (a : G) → F) (⇑f' : (a : F) → G)
⊢ Topology.IsEmbedding.{u_3, u_4} (X := F) (Y := G) (⇑f' : (a : F) → G)

Tactic:
Topology.IsEmbedding.of_leftInverse hf'symm (map_continuous _) (map_continuous _)

Premises used: Topology.IsEmbedding.of_leftInverse, ContinuousMapClass.map_continuous
-- 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
lE : Filter (E × E)
lF : Filter (F × F)
hg : Tendsto (Prod.map g g) lE lF
hf : HasFDerivAtFilter f f' lF
hh : HasFDerivAtFilter h h' lE
hcomp : Prod.map (f ∘ g) (f ∘ g) =ᶠ[lE] Prod.map h h
hf'symm : Function.LeftInverse.{u_3 + 1, u_4 + 1} (α := F) (β := G) (⇑f'symm : (a : G) → F) (⇑f' : (a : F) → G)
⊢ Topology.IsEmbedding.{u_3, u_4} (X := F) (Y := G) (⇑f' : (a : F) → G)

Tactic:
exact Topology.IsEmbedding.of_leftInverse hf'symm (map_continuous _) (map_continuous _)

Premises used: Topology.IsEmbedding.of_leftInverse, ContinuousMapClass.map_continuous
-- 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
lE : Filter (E × E)
lF : Filter (F × F)
hg : Tendsto (Prod.map g g) lE lF
hf : HasFDerivAtFilter f f' lF
hh : HasFDerivAtFilter h h' lE
hcomp : Prod.map (f ∘ g) (f ∘ g) =ᶠ[lE] Prod.map h h
hf'symm : Function.LeftInverse.{u_3 + 1, u_4 + 1} (α := F) (β := G) (⇑f'symm : (a : G) → F) (⇑f' : (a : F) → 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) ((f'symm ∘SL h' : (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) ((h' : (a : E) → G) (x - y) : G)

Tactic:
f'symm.isBigOTVS_comp.congr_left ?_

Premises used: Asymptotics.IsBigOTVS.congr_left, ContinuousLinearMap.isBigOTVS_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
f' : F →L[𝕜] G
h' : E →L[𝕜] G
f'symm : G →L[𝕜] F
lE : Filter (E × E)
lF : Filter (F × F)
hg : Tendsto (Prod.map g g) lE lF
hf : HasFDerivAtFilter f f' lF
hh : HasFDerivAtFilter h h' lE
hcomp : Prod.map (f ∘ g) (f ∘ g) =ᶠ[lE] Prod.map h h
hf'symm : Function.LeftInverse.{u_3 + 1, u_4 + 1} (α := F) (β := G) (⇑f'symm : (a : G) → F) (⇑f' : (a : F) → G)
ho :
  ∀ (x : E × E),
    Eq.{u_3 + 1} (α := F)
      (Function.comp.{u_2 + 1, u_4 + 1, u_3 + 1} (β := G) (⇑f'symm : (a : G) → 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) ((h' : (a : E) → G) (x - y) : G))
          x :
        F)
      (match (motive := E × E → F) x with
        | (x, y) => HSub.hSub (β := F) (g x - g y) ((f'symm ∘SL h' : (a : E) → F) (x - y) : F) :
        F)
⊢ 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) ((f'symm ∘SL h' : (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) ((h' : (a : E) → G) (x - y) : G)

Tactic:
refine f'symm.isBigOTVS_comp.congr_left ?_

Premises used: Asymptotics.IsBigOTVS.congr_left, ContinuousLinearMap.isBigOTVS_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
f' : F →L[𝕜] G
h' : E →L[𝕜] G
f'symm : G →L[𝕜] F
lE : Filter (E × E)
lF : Filter (F × F)
hg : Tendsto (Prod.map g g) lE lF
hf : HasFDerivAtFilter f f' lF
hh : HasFDerivAtFilter h h' lE
hcomp : Prod.map (f ∘ g) (f ∘ g) =ᶠ[lE] Prod.map h h
hf'symm : Function.LeftInverse.{u_3 + 1, u_4 + 1} (α := F) (β := G) (⇑f'symm : (a : G) → F) (⇑f' : (a : F) → G)
⊢ ∀ (x : E × E),
    Eq.{u_3 + 1} (α := F)
      (Function.comp.{u_2 + 1, u_4 + 1, u_3 + 1} (β := G) (⇑f'symm : (a : G) → 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) ((h' : (a : E) → G) (x - y) : G))
          x :
        F)
      (match (motive := E × E → F) x with
        | (x, y) => HSub.hSub (β := F) (g x - g y) ((f'symm ∘SL h' : (a : E) → F) (x - y) : F) :
        F)

Tactic:
simp [hf'symm _]
-- 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
s : Set E
t : Set F
hst : Tendsto g (𝓝[s] a) (𝓝[t] g a)
hf : HasFDerivWithinAt f f' t (g a)
hh : HasFDerivWithinAt h h' s a
hcomp : f ∘ g =ᶠ[𝓝[s] a] h
hf'symm : Function.LeftInverse.{u_3 + 1, u_4 + 1} (α := F) (β := G) (⇑f'symm : (a : G) → F) (⇑f' : (a : F) → G)
ha : a ∈ s
⊢ HasFDerivWithinAt g (f'symm ∘SL h') s a

Tactic:
HasFDerivAtFilter.of_comp_of_leftInverse ?_ hf hh ?_ hf'symm

Premises used: HasFDerivWithinAt, HasFDerivAtFilter.of_comp_of_leftInverse
-- 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
s : Set E
t : Set F
hst : Tendsto g (𝓝[s] a) (𝓝[t] g a)
hf : HasFDerivWithinAt f f' t (g a)
hh : HasFDerivWithinAt h h' s a
hcomp : f ∘ g =ᶠ[𝓝[s] a] h
hf'symm : Function.LeftInverse.{u_3 + 1, u_4 + 1} (α := F) (β := G) (⇑f'symm : (a : G) → F) (⇑f' : (a : F) → G)
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 (f'symm ∘SL h') s a

Tactic:
refine HasFDerivAtFilter.of_comp_of_leftInverse ?_ hf hh ?_ hf'symm

Premises used: HasFDerivAtFilter.of_comp_of_leftInverse
-- 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
s : Set E
t : Set F
hst : Tendsto g (𝓝[s] a) (𝓝[t] g a)
hf : HasFDerivWithinAt f f' t (g a)
hh : HasFDerivWithinAt h h' s a
hcomp : f ∘ g =ᶠ[𝓝[s] a] h
hf'symm : Function.LeftInverse.{u_3 + 1, u_4 + 1} (α := F) (β := G) (⇑f'symm : (a : G) → F) (⇑f' : (a : F) → G)
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
f' : F →L[𝕜] G
h' : E →L[𝕜] G
f'symm : G →L[𝕜] F
a : E
s : Set E
t : Set F
hst : Tendsto g (𝓝[s] a) (𝓝[t] g a)
hf : HasFDerivWithinAt f f' t (g a)
hh : HasFDerivWithinAt h h' s a
hcomp : f ∘ g =ᶠ[𝓝[s] a] h
hf'symm : Function.LeftInverse.{u_3 + 1, u_4 + 1} (α := F) (β := G) (⇑f'symm : (a : G) → F) (⇑f' : (a : F) → G)
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 hst.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
f' : F →L[𝕜] G
h' : E →L[𝕜] G
f'symm : G →L[𝕜] F
a : E
s : Set E
t : Set F
hst : Tendsto g (𝓝[s] a) (𝓝[t] g a)
hf : HasFDerivWithinAt f f' t (g a)
hh : HasFDerivWithinAt h h' s a
hcomp : f ∘ g =ᶠ[𝓝[s] a] h
hf'symm : Function.LeftInverse.{u_3 + 1, u_4 + 1} (α := F) (β := G) (⇑f'symm : (a : G) → F) (⇑f' : (a : F) → G)
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
f' : F →L[𝕜] G
h' : E →L[𝕜] G
f'symm : G →L[𝕜] F
a : E
s : Set E
t : Set F
hst : Tendsto g (𝓝[s] a) (𝓝[t] g a)
hf : HasFDerivWithinAt f f' t (g a)
hh : HasFDerivWithinAt h h' s a
hcomp : f ∘ g =ᶠ[𝓝[s] a] h
hf'symm : Function.LeftInverse.{u_3 + 1, u_4 + 1} (α := F) (β := G) (⇑f'symm : (a : G) → F) (⇑f' : (a : F) → G)
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)
-- 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 : HasFDerivAt f f' (g a)
hh : HasFDerivAt 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)
⊢ HasFDerivAt g (f'symm ∘SL h') a

Tactic:
HasFDerivAtFilter.of_comp_of_leftInverse ?_ hf hh ?_ hf'symm

Premises used: HasFDerivAt, HasFDerivAtFilter.of_comp_of_leftInverse
-- 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 : HasFDerivAt f f' (g a)
hh : HasFDerivAt 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)
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 (f'symm ∘SL h') a

Tactic:
refine HasFDerivAtFilter.of_comp_of_leftInverse ?_ hf hh ?_ hf'symm

Premises used: HasFDerivAtFilter.of_comp_of_leftInverse
-- 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 : HasFDerivAt f f' (g a)
hh : HasFDerivAt 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)
⊢ 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
f' : F →L[𝕜] G
h' : E →L[𝕜] G
f'symm : G →L[𝕜] F
a : E
hgc : ContinuousAt g a
hf : HasFDerivAt f f' (g a)
hh : HasFDerivAt 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)
⊢ Tendsto (Prod.map g g) (SProd.sprod (β := Filter E) (𝓝 a) (pure a))
    (SProd.sprod (β := Filter F) (𝓝 (g a)) (pure (g a)))

Tactic:
exact hgc.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
f' : F →L[𝕜] G
h' : E →L[𝕜] G
f'symm : G →L[𝕜] F
a : E
hgc : ContinuousAt g a
hf : HasFDerivAt f f' (g a)
hh : HasFDerivAt 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)
⊢ 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
f' : F →L[𝕜] G
h' : E →L[𝕜] G
f'symm : G →L[𝕜] F
a : E
hgc : ContinuousAt g a
hf : HasFDerivAt f f' (g a)
hh : HasFDerivAt 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)
⊢ 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