awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.FDeriv.Norm
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
t : ℝ
h : Nontrivial E
hd : ¬DifferentiableAt ℝ (F := ℝ) (fun (x : E) ↦ ‖x‖) x
neg : 0 = HSMul.hSMul (α := ℝ) (β := E →L[ℝ] ℝ) (↑((SignType.sign : (a : ℝ) → SignType) t) : ℝ) 0
neg₁ : ¬DifferentiableAt ℝ (F := ℝ) (fun (x : E) ↦ ‖x‖) (t • x)
⊢ fderiv ℝ (fun (x : E) ↦ ‖x‖) (t • x) =
    HSMul.hSMul (α := ℝ) (β := E →L[ℝ] ℝ) (↑((SignType.sign : (a : ℝ) → SignType) t) : ℝ)
      (fderiv ℝ (fun (x : E) ↦ ‖x‖) x)

Tactic:
rw [fderiv_zero_of_not_differentiableAt hd, fderiv_zero_of_not_differentiableAt]

Premises used: fderiv_zero_of_not_differentiableAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Norm
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
t : ℝ
h : Nontrivial E
hd : ¬DifferentiableAt ℝ (F := ℝ) (fun (x : E) ↦ ‖x‖) x
⊢ 0 = HSMul.hSMul (α := ℝ) (β := E →L[ℝ] ℝ) (↑((SignType.sign : (a : ℝ) → SignType) t) : ℝ) 0

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.FDeriv.Norm
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
t : ℝ
h : Nontrivial E
hd : ¬DifferentiableAt ℝ (F := ℝ) (fun (x : E) ↦ ‖x‖) x
⊢ ¬DifferentiableAt ℝ (F := ℝ) (fun (x : E) ↦ ‖x‖) (t • x)

Tactic:
mt DifferentiableAt.differentiableAt_norm_of_smul hd

Premises used: mt, DifferentiableAt.differentiableAt_norm_of_smul
-- Module: Mathlib.Analysis.Calculus.FDeriv.Norm
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
t : ℝ
h : Nontrivial E
hd : ¬DifferentiableAt ℝ (F := ℝ) (fun (x : E) ↦ ‖x‖) x
⊢ ¬DifferentiableAt ℝ (F := ℝ) (fun (x : E) ↦ ‖x‖) (t • x)

Tactic:
exact mt DifferentiableAt.differentiableAt_norm_of_smul hd

Premises used: mt, DifferentiableAt.differentiableAt_norm_of_smul
-- Module: Mathlib.Analysis.Calculus.FDeriv.Norm
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
t : ℝ
ht : 0 < t
⊢ Eq (α := E →L[ℝ] ℝ) (fderiv ℝ (fun (x : E) ↦ ‖x‖) (t • x)) (fderiv ℝ (fun (x : E) ↦ ‖x‖) x)

Tactic:
simp [fderiv_norm_smul, ht]

Premises used: fderiv_norm_smul
-- Module: Mathlib.Analysis.Calculus.FDeriv.Norm
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
t : ℝ
ht : t < 0
⊢ Eq (α := E →L[ℝ] ℝ) (fderiv ℝ (fun (x : E) ↦ ‖x‖) (t • x)) (-fderiv ℝ (fun (x : E) ↦ ‖x‖) x)

Tactic:
simp [fderiv_norm_smul, ht]

Premises used: fderiv_norm_smul
-- Module: Mathlib.Analysis.Calculus.FDeriv.Norm
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
inst_2 : Nontrivial E
h : DifferentiableAt ℝ (F := ℝ) (fun (x : E) ↦ ‖x‖) x
⊢ x ≠ 0

Tactic:
have : x ≠ 0 := fun hx ↦ not_differentiableAt_norm_zero E (hx ▸ h)
-- Module: Mathlib.Analysis.Calculus.FDeriv.Norm
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
inst_2 : Nontrivial E
h : DifferentiableAt ℝ (F := ℝ) (fun (x : E) ↦ ‖x‖) x
this : x ≠ 0
⊢ Norm.norm (E := E →L[ℝ] ℝ) (fderiv ℝ (fun (x : E) ↦ ‖x‖) x) = 1

Tactic:
le_antisymm (NNReal.coe_one ▸ norm_fderiv_le_of_lipschitz ℝ lipschitzWith_one_norm) ?_

Premises used: le_antisymm
-- Module: Mathlib.Analysis.Calculus.FDeriv.Norm
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
inst_2 : Nontrivial E
h : DifferentiableAt ℝ (F := ℝ) (fun (x : E) ↦ ‖x‖) x
this : x ≠ 0
refine : 1 ≤ Norm.norm (E := E →L[ℝ] ℝ) (fderiv ℝ (fun (x : E) ↦ ‖x‖) x)
⊢ Norm.norm (E := E →L[ℝ] ℝ) (fderiv ℝ (fun (x : E) ↦ ‖x‖) x) = 1

Tactic:
refine le_antisymm (NNReal.coe_one ▸ norm_fderiv_le_of_lipschitz ℝ lipschitzWith_one_norm) ?_

Premises used: le_antisymm
-- Module: Mathlib.Analysis.Calculus.FDeriv.Norm
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
inst_2 : Nontrivial E
h : DifferentiableAt ℝ (F := ℝ) (fun (x : E) ↦ ‖x‖) x
this : x ≠ 0
apply : 1 * ‖x‖ ≤ Norm.norm (E := E →L[ℝ] ℝ) (fderiv ℝ (fun (x : E) ↦ ‖x‖) x) * ‖x‖
⊢ 1 ≤ Norm.norm (E := E →L[ℝ] ℝ) (fderiv ℝ (fun (x : E) ↦ ‖x‖) x)

Tactic:
apply le_of_mul_le_mul_right _ (norm_pos_iff.2 this)

Premises used: Iff.mpr, norm_pos_iff, le_of_mul_le_mul_right
-- Module: Mathlib.Analysis.Calculus.FDeriv.Norm
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
inst_2 : Nontrivial E
h : DifferentiableAt ℝ (F := ℝ) (fun (x : E) ↦ ‖x‖) x
this : x ≠ 0
rw : ‖x‖ = (fderiv ℝ (fun (x : E) ↦ ‖x‖) x : (a : E) → ℝ) x
rw₁ rw₂ : ‖x‖ = ‖x‖
⊢ 1 * ‖x‖ = (fderiv ℝ (fun (x : E) ↦ ‖x‖) x : (a : E) → ℝ) x

Tactic:
rw [one_mul, h.fderiv_norm_self]

Premises used: DifferentiableAt.fderiv_norm_self, one_mul
-- Module: Mathlib.Analysis.Calculus.FDeriv.Norm
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
inst_2 : Nontrivial E
h : DifferentiableAt ℝ (F := ℝ) (fun (x : E) ↦ ‖x‖) x
this : x ≠ 0
⊢ (fderiv ℝ (fun (x : E) ↦ ‖x‖) x : (a : E) → ℝ) x ≤
    Norm.norm (E := ℝ) ((fderiv ℝ (fun (x : E) ↦ ‖x‖) x : (a : E) → ℝ) x : ℝ)

Tactic:
le_norm_self _

Premises used: Real.le_norm_self
-- Module: Mathlib.Analysis.Calculus.FDeriv.Norm
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
inst_2 : Nontrivial E
h : DifferentiableAt ℝ (F := ℝ) (fun (x : E) ↦ ‖x‖) x
this : x ≠ 0
⊢ Norm.norm (E := ℝ) ((fderiv ℝ (fun (x : E) ↦ ‖x‖) x : (a : E) → ℝ) x : ℝ) ≤
    Norm.norm (E := E →L[ℝ] ℝ) (fderiv ℝ (fun (x : E) ↦ ‖x‖) x) * ‖x‖

Tactic:
le_opNorm _ _

Premises used: ContinuousLinearMap.le_opNorm
-- Module: Mathlib.Analysis.Calculus.FDeriv.Norm
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
inst_2 : Nontrivial E
h : DifferentiableAt ℝ (F := ℝ) (fun (x : E) ↦ ‖x‖) x
this : x ≠ 0
fderiv : 1 * ‖x‖ = (_root_.fderiv ℝ (fun (x : E) ↦ ‖x‖) x : (a : E) → ℝ) x
⊢ 1 * ‖x‖ ≤ Norm.norm (E := E →L[ℝ] ℝ) (_root_.fderiv ℝ (fun (x : E) ↦ ‖x‖) x) * ‖x‖

Tactic:
calc
    1 * ‖x‖ = fderiv ℝ (‖·‖) x x := by rw [one_mul, h.fderiv_norm_self]
    _ ≤ ‖fderiv ℝ (‖·‖) x x‖ := le_norm_self _
    _ ≤ ‖fderiv ℝ (‖·‖) x‖ * ‖x‖ := le_opNorm _ _

Premises used: Norm.norm, Real, ContinuousLinearMap.le_opNorm, fderiv, Real.le_norm_self, DFunLike.coe
-- 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
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)
⊢ HasFDerivAtFilter g g' lE

Tactic:
.of_isLittleOTVS <| ho.trans_isLittleOTVS <| .triangle (.symm ?_) hh.isLittleOTVS

Premises used: Asymptotics.IsLittleOTVS.triangle, Asymptotics.IsBigOTVS.trans_isLittleOTVS, HasFDerivAtFilter.of_isLittleOTVS, HasFDerivAtFilter.isLittleOTVS, Asymptotics.IsLittleOTVS.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
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 :
  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
⊢ HasFDerivAtFilter g g' lE

Tactic:
refine .of_isLittleOTVS <| ho.trans_isLittleOTVS <| .triangle (.symm ?_) hh.isLittleOTVS

Premises used: Asymptotics.IsBigOTVS.trans_isLittleOTVS
-- 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
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

Tactic:
(hf.isLittleOTVS.comp_tendsto htendsto).congr' ?_ .rfl |>.trans_isBigOTVS ?_

Premises used: Asymptotics.IsLittleOTVS.trans_isBigOTVS, Asymptotics.IsLittleOTVS.congr', Asymptotics.IsLittleOTVS.comp_tendsto, HasFDerivAtFilter.isLittleOTVS, Filter.EventuallyEq.rfl
-- 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
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)
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
⊢ 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

Tactic:
refine (hf.isLittleOTVS.comp_tendsto htendsto).congr' ?_ .rfl |>.trans_isBigOTVS ?_

Premises used: Asymptotics.IsLittleOTVS.trans_isBigOTVS, Asymptotics.IsLittleOTVS.congr', Asymptotics.IsLittleOTVS.comp_tendsto, HasFDerivAtFilter.isLittleOTVS, Filter.EventuallyEq.rfl
-- 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
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)

Tactic:
hcomp.mono ?_

Premises used: Filter.EventuallyEq, Filter.Eventually.mono
-- 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
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 :
  ∀ (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
⊢ (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 hcomp.mono ?_

Premises used: Filter.Eventually.mono
-- 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
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)
⊢ ∀ (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:
simp +contextual
-- 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
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

Tactic:
hf.isThetaTVS_sub hf_emb.isInducing |>.symm.isBigOTVS.comp_tendsto htendsto |>.trans ?_

Premises used: Asymptotics.IsBigOTVS.comp_tendsto, HasFDerivAtFilter.isThetaTVS_sub, Topology.IsEmbedding.isInducing, Asymptotics.IsThetaTVS.isBigOTVS, Asymptotics.IsThetaTVS.symm, Asymptotics.IsBigOTVS.trans
-- 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
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_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
⊢ 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.isThetaTVS_sub hf_emb.isInducing |>.symm.isBigOTVS.comp_tendsto htendsto |>.trans ?_

Premises used: Asymptotics.IsBigOTVS.comp_tendsto, HasFDerivAtFilter.isThetaTVS_sub, Topology.IsEmbedding.isInducing, Asymptotics.IsThetaTVS.isBigOTVS, Asymptotics.IsThetaTVS.symm, Asymptotics.IsBigOTVS.trans
-- 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
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

Tactic:
hh.isBigOTVS_sub.congr' (hcomp.mono ?_) .rfl

Premises used: Asymptotics.IsBigOTVS.congr', HasFDerivAtFilter.isBigOTVS_sub, Filter.Eventually.mono, Filter.EventuallyEq.rfl
-- 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
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_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)
⊢ 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 hh.isBigOTVS_sub.congr' (hcomp.mono ?_) .rfl

Premises used: Asymptotics.IsBigOTVS.congr', HasFDerivAtFilter.isBigOTVS_sub, Filter.Eventually.mono, Filter.EventuallyEq.rfl
-- 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
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)
⊢ ∀ (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:
simp +contextual