awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.OfCompLeft (goal)
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
h' : E →L[𝕜] G
lE : Filter (E × E)
lF : Filter (F × F)
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) ((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) ((h' : (a : E) → G) (x - y) : G)
⊢ Asymptotics.IsLittleOTVS 𝕜 (F := E) lE
    (HSub.hSub (α := E × E → G) (fun (p : E × E) ↦ h p.1 - h p.2) fun (x : E × E) ↦ (f' : (a : F) → G) (g x.1 - g x.2))
    fun (p : E × E) ↦ p.1 - p.2
have refine_1 : (fun (p : F × F) ↦ HSub.hSub (β := G) (f p.1 - f p.2) ((f' : (a : F) → G) (p.1 - p.2) : G)) ∘ Prod.map g g =ᶠ[lE]
  HSub.hSub (α := E × E → G) (fun (p : E × E) ↦ h p.1 - h p.2) fun (x : E × E) ↦ (f' : (a : F) → G) (g x.1 - g x.2)
Tactic: refine (hf.isLittleOTVS.comp_tendsto htendsto).congr' ?_ .rfl |>.trans_isBigOTVS ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.OfCompLeft (goal)
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
h' : E →L[𝕜] G
lE : Filter (E × E)
lF : Filter (F × F)
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) ((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) ((h' : (a : E) → G) (x - y) : G)
refine_1 :
  (fun (p : F × F) ↦ HSub.hSub (β := G) (f p.1 - f p.2) ((f' : (a : F) → G) (p.1 - p.2) : G)) ∘ Prod.map g g =ᶠ[lE]
    HSub.hSub (α := E × E → G) (fun (p : E × E) ↦ h p.1 - h p.2) fun (x : E × E) ↦ (f' : (a : F) → G) (g x.1 - g x.2)
⊢ Asymptotics.IsLittleOTVS 𝕜 (F := E) lE
    (HSub.hSub (α := E × E → G) (fun (p : E × E) ↦ h p.1 - h p.2) fun (x : E × E) ↦ (f' : (a : F) → G) (g x.1 - g x.2))
    fun (p : E × E) ↦ p.1 - p.2
have refine_2 : Asymptotics.IsBigOTVS 𝕜 (E := F) (F := E) lE ((fun (p : F × F) ↦ p.1 - p.2) ∘ Prod.map g g) fun (p : E × E) ↦ p.1 - p.2
Tactic: refine (hf.isLittleOTVS.comp_tendsto htendsto).congr' ?_ .rfl |>.trans_isBigOTVS ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.OfCompLeft (goal)
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
h' : E →L[𝕜] G
lE : Filter (E × E)
lF : Filter (F × F)
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) ((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) ((h' : (a : E) → G) (x - y) : G)
⊢ (fun (p : F × F) ↦ HSub.hSub (β := G) (f p.1 - f p.2) ((f' : (a : F) → G) (p.1 - p.2) : G)) ∘ Prod.map g g =ᶠ[lE]
    HSub.hSub (α := E × E → G) (fun (p : E × E) ↦ h p.1 - h p.2) fun (x : E × E) ↦ (f' : (a : F) → G) (g x.1 - g x.2)
have refine_1 : ∀ (x : E × E),
  Prod.map (f ∘ g) (f ∘ g) x = Prod.map h h x →
    ((fun (p : F × F) ↦ HSub.hSub (β := G) (f p.1 - f p.2) ((f' : (a : F) → G) (p.1 - p.2) : G)) ∘ Prod.map g g) x =
      HSub.hSub (α := E × E → G) (β := E × E → G) (fun (p : E × E) ↦ h p.1 - h p.2)
        (fun (x : E × E) ↦ (f' : (a : F) → G) (g x.1 - g x.2)) x
Tactic: refine hcomp.mono ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.OfCompLeft (goal)
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
h' : E →L[𝕜] G
lE : Filter (E × E)
lF : Filter (F × F)
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) ((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) ((h' : (a : E) → G) (x - y) : G)
⊢ Asymptotics.IsBigOTVS 𝕜 (E := F) (F := E) lE ((fun (p : F × F) ↦ p.1 - p.2) ∘ Prod.map g g) fun (p : E × E) ↦
    p.1 - p.2
have refine_2 : Asymptotics.IsBigOTVS.{u_1, u_2, u_4, u_2} 𝕜 (E := G) (F := E) lE ((fun (p : F × F) ↦ f p.1 - f p.2) ∘ Prod.map g g)
  fun (p : E × E) ↦ p.1 - p.2
Tactic: refine hf.isThetaTVS_sub hf_emb.isInducing |>.symm.isBigOTVS.comp_tendsto htendsto |>.trans ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.OfCompLeft (goal)
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
h' : E →L[𝕜] G
lE : Filter (E × E)
lF : Filter (F × F)
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) ((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) ((h' : (a : E) → G) (x - y) : G)
⊢ Asymptotics.IsBigOTVS.{u_1, u_2, u_4, u_2} 𝕜 (E := G) (F := E) lE ((fun (p : F × F) ↦ f p.1 - f p.2) ∘ Prod.map g g)
    fun (p : E × E) ↦ p.1 - p.2
have refine_2 : ∀ (x : E × E),
  Prod.map (f ∘ g) (f ∘ g) x = Prod.map h h x →
    Eq.{u_4 + 1} (α := G) ((fun (p : E × E) ↦ h p.1 - h p.2) x) (((fun (p : F × F) ↦ f p.1 - f p.2) ∘ Prod.map g g) x)
Tactic: refine hh.isBigOTVS_sub.congr' (hcomp.mono ?_) .rfl
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.OfCompLeft (goal)
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 g (f'symm ∘SL h') lE
have hf_emb : Topology.IsEmbedding.{u_3, u_4} (X := F) (Y := G) (⇑f' : (a : F) → G)
Tactic: apply of_comp_aux (f := f) (f' := f')
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.OfCompLeft (goal)
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
⊢ HasFDerivAtFilter g (f'symm ∘SL h') lE
have 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)
Tactic: apply of_comp_aux (f := f) (f' := f')
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.OfCompLeft (goal)
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)
have 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)
Tactic: refine f'symm.isBigOTVS_comp.congr_left ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.OfCompLeft (goal)
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
have 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)))
Tactic: refine HasFDerivAtFilter.of_comp_of_leftInverse ?_ hf hh ?_ hf'symm
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.OfCompLeft (goal)
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)))
⊢ HasFDerivWithinAt g (f'symm ∘SL h') s a
have refine_2 : Prod.map (f ∘ g) (f ∘ g) =ᶠ[SProd.sprod (β := Filter E) (𝓝[s] a) (pure a)] Prod.map h h
Tactic: refine HasFDerivAtFilter.of_comp_of_leftInverse ?_ hf hh ?_ hf'symm
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.OfCompLeft (goal)
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
have refine_1 : Tendsto (Prod.map g g) (SProd.sprod (β := Filter E) (𝓝 a) (pure a)) (SProd.sprod (β := Filter F) (𝓝 (g a)) (pure (g a)))
Tactic: refine HasFDerivAtFilter.of_comp_of_leftInverse ?_ hf hh ?_ hf'symm
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.OfCompLeft (goal)
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)))
⊢ HasFDerivAt g (f'symm ∘SL h') a
have refine_2 : Prod.map (f ∘ g) (f ∘ g) =ᶠ[SProd.sprod (β := Filter E) (𝓝 a) (pure a)] Prod.map h h
Tactic: refine HasFDerivAtFilter.of_comp_of_leftInverse ?_ hf hh ?_ hf'symm
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.OfCompLeft (goal)
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
⊢ HasFDerivAtFilter g g' lE
have 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)
Tactic: apply of_comp_aux (f := f) (f' := f')
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.OfCompLeft (goal)
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
⊢ HasFDerivAtFilter g g' lE
have apply₁ : E →L[𝕜] G
Tactic: apply of_comp_aux (f := f) (f' := f')
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.OfCompLeft (goal)
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)
have 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)
Tactic: refine f'.isThetaTVS_comp hf'.isInducing |>.symm.isBigOTVS.congr_right ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.OfCompLeft (goal)
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
have 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)))
Tactic: refine HasFDerivAtFilter.of_comp_of_isEmbedding ?_ hf hf' hh ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.OfCompLeft (goal)
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)))
⊢ HasFDerivWithinAt g g' s a
have refine_2 : Prod.map (f ∘ g) (f ∘ g) =ᶠ[SProd.sprod (β := Filter E) (𝓝[s] a) (pure a)] Prod.map h h
Tactic: refine HasFDerivAtFilter.of_comp_of_isEmbedding ?_ hf hf' hh ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.OfCompLeft (goal)
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
have refine_1 : Tendsto (Prod.map g g) (SProd.sprod (β := Filter E) (𝓝 a) (pure a)) (SProd.sprod (β := Filter F) (𝓝 (g a)) (pure (g a)))
Tactic: refine HasFDerivAtFilter.of_comp_of_isEmbedding ?_ hf hf' hh ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.OfCompLeft (goal)
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)))
⊢ HasFDerivAt g g' a
have refine_2 : Prod.map (f ∘ g) (f ∘ g) =ᶠ[SProd.sprod (β := Filter E) (𝓝 a) (pure a)] Prod.map h h
Tactic: refine HasFDerivAtFilter.of_comp_of_isEmbedding ?_ hf hf' hh ?_