awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : G → E
x : G
f' : G →L[𝕜] E
simp_rw :
  HasFDerivWithinAt ((⇑iso : (a : E) → F) ∘ f) ((↑iso : E →L[𝕜] F) ∘SL f') univ x ↔ HasFDerivWithinAt f f' univ x
⊢ HasFDerivAt ((⇑iso : (a : E) → F) ∘ f) ((↑iso : E →L[𝕜] F) ∘SL f') x ↔ HasFDerivAt f f' x

Tactic:
simp_rw [← hasFDerivWithinAt_univ, iso.comp_hasFDerivWithinAt_iff]

Premises used: ContinuousLinearEquiv.comp_hasFDerivWithinAt_iff, hasFDerivWithinAt_univ
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : G → E
s : Set G
x : G
f' : G →L[𝕜] F
rw :
  HasFDerivWithinAt ((⇑iso : (a : E) → F) ∘ f) f' s x ↔
    HasFDerivWithinAt ((⇑iso : (a : E) → F) ∘ f) ((↑iso : E →L[𝕜] F) ∘SL (↑iso.symm : F →L[𝕜] E) ∘SL f') s x
rw₁ :
  HasFDerivWithinAt ((⇑iso : (a : E) → F) ∘ f) f' s x ↔
    HasFDerivWithinAt ((⇑iso : (a : E) → F) ∘ f) (((↑iso : E →L[𝕜] F) ∘SL (↑iso.symm : F →L[𝕜] E)) ∘SL f') s x
rw₂ :
  HasFDerivWithinAt ((⇑iso : (a : E) → F) ∘ f) f' s x ↔
    HasFDerivWithinAt ((⇑iso : (a : E) → F) ∘ f) (ContinuousLinearMap.id 𝕜 F ∘SL f') s x
rw₃ rw₄ : HasFDerivWithinAt ((⇑iso : (a : E) → F) ∘ f) f' s x ↔ HasFDerivWithinAt ((⇑iso : (a : E) → F) ∘ f) f' s x
⊢ HasFDerivWithinAt ((⇑iso : (a : E) → F) ∘ f) f' s x ↔ HasFDerivWithinAt f ((↑iso.symm : F →L[𝕜] E) ∘SL f') s x

Tactic:
rw [← iso.comp_hasFDerivWithinAt_iff, ← ContinuousLinearMap.comp_assoc, iso.coe_comp_coe_symm,
    ContinuousLinearMap.id_comp]

Premises used: ContinuousLinearEquiv.coe_comp_coe_symm, ContinuousLinearEquiv.comp_hasFDerivWithinAt_iff, ContinuousLinearMap.comp_assoc, ContinuousLinearMap.id_comp
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : G → E
x : G
f' : G →L[𝕜] F
simp_rw :
  HasFDerivWithinAt ((⇑iso : (a : E) → F) ∘ f) f' univ x ↔ HasFDerivWithinAt f ((↑iso.symm : F →L[𝕜] E) ∘SL f') univ x
⊢ HasFDerivAt ((⇑iso : (a : E) → F) ∘ f) f' x ↔ HasFDerivAt f ((↑iso.symm : F →L[𝕜] E) ∘SL f') x

Tactic:
simp_rw [← hasFDerivWithinAt_univ, iso.comp_hasFDerivWithinAt_iff']

Premises used: ContinuousLinearEquiv.comp_hasFDerivWithinAt_iff', hasFDerivWithinAt_univ
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : G → E
s : Set G
x : G
hxs : UniqueDiffWithinAt 𝕜 s x
pos :
  ∀ (h : DifferentiableWithinAt 𝕜 f s x),
    Eq (α := G →L[𝕜] F) (fderivWithin 𝕜 ((⇑iso : (a : E) → F) ∘ f) s x) ((↑iso : E →L[𝕜] F) ∘SL fderivWithin 𝕜 f s x)
neg :
  ∀ (h : ¬DifferentiableWithinAt 𝕜 f s x),
    Eq (α := G →L[𝕜] F) (fderivWithin 𝕜 ((⇑iso : (a : E) → F) ∘ f) s x) ((↑iso : E →L[𝕜] F) ∘SL fderivWithin 𝕜 f s x)
⊢ Eq (α := G →L[𝕜] F) (fderivWithin 𝕜 ((⇑iso : (a : E) → F) ∘ f) s x) ((↑iso : E →L[𝕜] F) ∘SL fderivWithin 𝕜 f s x)

Tactic:
by_cases h : DifferentiableWithinAt 𝕜 f s x

Premises used: DifferentiableWithinAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : G → E
s : Set G
x : G
hxs : UniqueDiffWithinAt 𝕜 s x
h : DifferentiableWithinAt 𝕜 f s x
pos :
  Eq (α := G →L[𝕜] F) (fderiv 𝕜 (⇑iso : (a : E) → F) (f x) ∘SL fderivWithin 𝕜 f s x)
    ((↑iso : E →L[𝕜] F) ∘SL fderivWithin 𝕜 f s x)
pos₁ pos₂ :
  Eq (α := G →L[𝕜] F) ((↑iso : E →L[𝕜] F) ∘SL fderivWithin 𝕜 f s x) ((↑iso : E →L[𝕜] F) ∘SL fderivWithin 𝕜 f s x)
⊢ Eq (α := G →L[𝕜] F) (fderivWithin 𝕜 ((⇑iso : (a : E) → F) ∘ f) s x) ((↑iso : E →L[𝕜] F) ∘SL fderivWithin 𝕜 f s x)

Tactic:
rw [fderiv_comp_fderivWithin x iso.differentiableAt h hxs, iso.fderiv]

Premises used: ContinuousLinearEquiv.differentiableAt, fderiv_comp_fderivWithin, ContinuousLinearEquiv.fderiv
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : G → E
s : Set G
x : G
hxs : UniqueDiffWithinAt 𝕜 s x
h : ¬DifferentiableWithinAt 𝕜 f s x
⊢ ¬DifferentiableWithinAt.{u_1, u_4, u_3} 𝕜 (F := F) ((⇑iso : (a : E) → F) ∘ f) s x

Tactic:
have : ¬DifferentiableWithinAt 𝕜 (iso ∘ f) s x := mt iso.comp_differentiableWithinAt_iff.1 h
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : G → E
s : Set G
x : G
hxs : UniqueDiffWithinAt 𝕜 s x
h : ¬DifferentiableWithinAt 𝕜 f s x
this : ¬DifferentiableWithinAt.{u_1, u_4, u_3} 𝕜 (F := F) ((⇑iso : (a : E) → F) ∘ f) s x
neg :
  Eq (α := G →L[𝕜] F) (fderivWithin 𝕜 ((⇑iso : (a : E) → F) ∘ f) s x) ((↑iso : E →L[𝕜] F).comp (σ₁₂ := RingHom.id 𝕜) 0)
neg₁ : Eq (α := G →L[𝕜] F) 0 ((↑iso : E →L[𝕜] F).comp (σ₁₂ := RingHom.id 𝕜) 0)
neg₂ neg₃ : Eq (α := G →L[𝕜] F) 0 0
⊢ Eq (α := G →L[𝕜] F) (fderivWithin 𝕜 ((⇑iso : (a : E) → F) ∘ f) s x) ((↑iso : E →L[𝕜] F) ∘SL fderivWithin 𝕜 f s x)

Tactic:
rw [fderivWithin_zero_of_not_differentiableWithinAt h,
      fderivWithin_zero_of_not_differentiableWithinAt this, ContinuousLinearMap.comp_zero]

Premises used: ContinuousLinearMap.comp_zero, fderivWithin_zero_of_not_differentiableWithinAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : G → E
x : G
rw :
  Eq (α := G →L[𝕜] F) (fderivWithin 𝕜 ((⇑iso : (a : E) → F) ∘ f) univ x)
    ((↑iso : E →L[𝕜] F) ∘SL fderivWithin 𝕜 f univ x)
⊢ Eq (α := G →L[𝕜] F) (fderiv 𝕜 ((⇑iso : (a : E) → F) ∘ f) x) ((↑iso : E →L[𝕜] F) ∘SL fderiv 𝕜 f x)

Tactic:
rw [← fderivWithin_univ, ← fderivWithin_univ]

Premises used: fderivWithin_univ
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : G → E
x : G
⊢ Eq (α := G →L[𝕜] F) (fderivWithin 𝕜 ((⇑iso : (a : E) → F) ∘ f) univ x)
    ((↑iso : E →L[𝕜] F) ∘SL fderivWithin 𝕜 f univ x)

Tactic:
iso.comp_fderivWithin uniqueDiffWithinAt_univ

Premises used: uniqueDiffWithinAt_univ, ContinuousLinearEquiv.comp_fderivWithin
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : G → E
x : G
⊢ Eq (α := G →L[𝕜] F) (fderivWithin 𝕜 ((⇑iso : (a : E) → F) ∘ f) univ x)
    ((↑iso : E →L[𝕜] F) ∘SL fderivWithin 𝕜 f univ x)

Tactic:
exact iso.comp_fderivWithin uniqueDiffWithinAt_univ

Premises used: uniqueDiffWithinAt_univ, ContinuousLinearEquiv.comp_fderivWithin
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
G' : Type u_5
inst_7 : NormedAddCommGroup G'
inst_8 : NormedSpace 𝕜 G'
x : E
s : Set E
L : G ≃L[𝕜] G'
f : E → F →L[𝕜] G
hs : UniqueDiffWithinAt 𝕜 s x
change :
  Eq (α := E →L[𝕜] F →L[𝕜] G')
    (fderivWithin 𝕜 ((⇑(arrowCongr (ContinuousLinearEquiv.refl 𝕜 F) L) : (a : F →L[𝕜] G) → F →L[𝕜] G') ∘ f) s x)
    ((↑(arrowCongr (ContinuousLinearEquiv.refl 𝕜 F) L) : (F →L[𝕜] G) →L[𝕜] F →L[𝕜] G') ∘SL fderivWithin 𝕜 f s x)
⊢ Eq (α := E →L[𝕜] F →L[𝕜] G') (fderivWithin 𝕜 (fun (x : E) ↦ (↑L : G →L[𝕜] G') ∘SL f x) s x)
    ((↑(arrowCongr (ContinuousLinearEquiv.refl 𝕜 F) L) : (F →L[𝕜] G) →L[𝕜] F →L[𝕜] G') ∘SL fderivWithin 𝕜 f s x)

Tactic:
change fderivWithin 𝕜 (((ContinuousLinearEquiv.refl 𝕜 F).arrowCongr L) ∘ f) s x = _

Premises used: Function.comp, ContinuousLinearEquiv.arrowCongr, ContinuousLinearEquiv.refl, fderivWithin, DFunLike.coe
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
G' : Type u_5
inst_7 : NormedAddCommGroup G'
inst_8 : NormedSpace 𝕜 G'
x : E
s : Set E
L : G ≃L[𝕜] G'
f : E → F →L[𝕜] G
hs : UniqueDiffWithinAt 𝕜 s x
rw rw₁ :
  Eq (α := E →L[𝕜] F →L[𝕜] G')
    ((↑(arrowCongr (ContinuousLinearEquiv.refl 𝕜 F) L) : (F →L[𝕜] G) →L[𝕜] F →L[𝕜] G') ∘SL fderivWithin 𝕜 f s x)
    ((↑(arrowCongr (ContinuousLinearEquiv.refl 𝕜 F) L) : (F →L[𝕜] G) →L[𝕜] F →L[𝕜] G') ∘SL fderivWithin 𝕜 f s x)
⊢ Eq (α := E →L[𝕜] F →L[𝕜] G')
    (fderivWithin 𝕜 ((⇑(arrowCongr (ContinuousLinearEquiv.refl 𝕜 F) L) : (a : F →L[𝕜] G) → F →L[𝕜] G') ∘ f) s x)
    ((↑(arrowCongr (ContinuousLinearEquiv.refl 𝕜 F) L) : (F →L[𝕜] G) →L[𝕜] F →L[𝕜] G') ∘SL fderivWithin 𝕜 f s x)

Tactic:
rw [ContinuousLinearEquiv.comp_fderivWithin _ hs]

Premises used: ContinuousLinearEquiv.comp_fderivWithin
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
G' : Type u_5
inst_7 : NormedAddCommGroup G'
inst_8 : NormedSpace 𝕜 G'
L : G ≃L[𝕜] G'
f : E → F →L[𝕜] G
x : E
change :
  Eq (α := E →L[𝕜] F →L[𝕜] G')
    (fderiv 𝕜 ((⇑(arrowCongr (ContinuousLinearEquiv.refl 𝕜 F) L) : (a : F →L[𝕜] G) → F →L[𝕜] G') ∘ f) x)
    ((↑(arrowCongr (ContinuousLinearEquiv.refl 𝕜 F) L) : (F →L[𝕜] G) →L[𝕜] F →L[𝕜] G') ∘SL fderiv 𝕜 f x)
⊢ Eq (α := E →L[𝕜] F →L[𝕜] G') (fderiv 𝕜 (fun (x : E) ↦ (↑L : G →L[𝕜] G') ∘SL f x) x)
    ((↑(arrowCongr (ContinuousLinearEquiv.refl 𝕜 F) L) : (F →L[𝕜] G) →L[𝕜] F →L[𝕜] G') ∘SL fderiv 𝕜 f x)

Tactic:
change fderiv 𝕜 (((ContinuousLinearEquiv.refl 𝕜 F).arrowCongr L) ∘ f) x = _

Premises used: Function.comp, ContinuousLinearEquiv.arrowCongr, fderiv, ContinuousLinearEquiv.refl, DFunLike.coe
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
G' : Type u_5
inst_7 : NormedAddCommGroup G'
inst_8 : NormedSpace 𝕜 G'
L : G ≃L[𝕜] G'
f : E → F →L[𝕜] G
x : E
rw rw₁ :
  Eq (α := E →L[𝕜] F →L[𝕜] G')
    ((↑(arrowCongr (ContinuousLinearEquiv.refl 𝕜 F) L) : (F →L[𝕜] G) →L[𝕜] F →L[𝕜] G') ∘SL fderiv 𝕜 f x)
    ((↑(arrowCongr (ContinuousLinearEquiv.refl 𝕜 F) L) : (F →L[𝕜] G) →L[𝕜] F →L[𝕜] G') ∘SL fderiv 𝕜 f x)
⊢ Eq (α := E →L[𝕜] F →L[𝕜] G')
    (fderiv 𝕜 ((⇑(arrowCongr (ContinuousLinearEquiv.refl 𝕜 F) L) : (a : F →L[𝕜] G) → F →L[𝕜] G') ∘ f) x)
    ((↑(arrowCongr (ContinuousLinearEquiv.refl 𝕜 F) L) : (F →L[𝕜] G) →L[𝕜] F →L[𝕜] G') ∘SL fderiv 𝕜 f x)

Tactic:
rw [ContinuousLinearEquiv.comp_fderiv]

Premises used: ContinuousLinearEquiv.comp_fderiv
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
G' : Type u_5
inst_7 : NormedAddCommGroup G'
inst_8 : NormedSpace 𝕜 G'
L : G ≃L[𝕜] G'
f : E → F →L[𝕜] G
h :
  ∀ (x : E),
    Eq (α := E →L[𝕜] F →L[𝕜] G') (fderiv 𝕜 (fun (x : E) ↦ (↑L : G →L[𝕜] G') ∘SL f x) x)
      ((↑(arrowCongr (ContinuousLinearEquiv.refl 𝕜 F) L) : (F →L[𝕜] G) →L[𝕜] F →L[𝕜] G') ∘SL fderiv 𝕜 f x)
⊢ Eq (α := (x : E) → E →L[𝕜] F →L[𝕜] G') (fderiv 𝕜 fun (x : E) ↦ (↑L : G →L[𝕜] G') ∘SL f x) fun (x : E) ↦
    (↑(arrowCongr (ContinuousLinearEquiv.refl 𝕜 F) L) : (F →L[𝕜] G) →L[𝕜] F →L[𝕜] G') ∘SL fderiv 𝕜 f x

Tactic:
ext x : 1
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
G' : Type u_5
inst_7 : NormedAddCommGroup G'
inst_8 : NormedSpace 𝕜 G'
L : G ≃L[𝕜] G'
f : E → F →L[𝕜] G
x : E
⊢ Eq (α := E →L[𝕜] F →L[𝕜] G') (fderiv 𝕜 (fun (x : E) ↦ (↑L : G →L[𝕜] G') ∘SL f x) x)
    ((↑(arrowCongr (ContinuousLinearEquiv.refl 𝕜 F) L) : (F →L[𝕜] G) →L[𝕜] F →L[𝕜] G') ∘SL fderiv 𝕜 f x)

Tactic:
fderiv_continuousLinearEquiv_comp L f x

Premises used: fderiv_continuousLinearEquiv_comp
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
G' : Type u_5
inst_7 : NormedAddCommGroup G'
inst_8 : NormedSpace 𝕜 G'
L : G ≃L[𝕜] G'
f : E → F →L[𝕜] G
x : E
⊢ Eq (α := E →L[𝕜] F →L[𝕜] G') (fderiv 𝕜 (fun (x : E) ↦ (↑L : G →L[𝕜] G') ∘SL f x) x)
    ((↑(arrowCongr (ContinuousLinearEquiv.refl 𝕜 F) L) : (F →L[𝕜] G) →L[𝕜] F →L[𝕜] G') ∘SL fderiv 𝕜 f x)

Tactic:
exact fderiv_continuousLinearEquiv_comp L f x

Premises used: fderiv_continuousLinearEquiv_comp
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : F → G
s : Set F
x : E
⊢ DifferentiableWithinAt 𝕜 (f ∘ (⇑iso : (a : E) → F)) ((⇑iso : (a : E) → F) ⁻¹' s) x ↔
    DifferentiableWithinAt 𝕜 f s ((iso : (a : E) → F) x)

Tactic:
⟨fun H => ?_, fun H => H.comp x iso.differentiableWithinAt (mapsTo_preimage _ s)⟩

Premises used: DifferentiableWithinAt.comp, Set.mapsTo_preimage, Iff.intro, ContinuousLinearEquiv.differentiableWithinAt, DFunLike.coe
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : F → G
s : Set F
x : E
refine :
  ∀ (H : DifferentiableWithinAt 𝕜 (f ∘ (⇑iso : (a : E) → F)) ((⇑iso : (a : E) → F) ⁻¹' s) x),
    DifferentiableWithinAt 𝕜 f s ((iso : (a : E) → F) x)
⊢ DifferentiableWithinAt 𝕜 (f ∘ (⇑iso : (a : E) → F)) ((⇑iso : (a : E) → F) ⁻¹' s) x ↔
    DifferentiableWithinAt 𝕜 f s ((iso : (a : E) → F) x)

Tactic:
refine ⟨fun H => ?_, fun H => H.comp x iso.differentiableWithinAt (mapsTo_preimage _ s)⟩
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : F → G
s : Set F
x : E
H : DifferentiableWithinAt 𝕜 (f ∘ (⇑iso : (a : E) → F)) ((⇑iso : (a : E) → F) ⁻¹' s) x
⊢ DifferentiableWithinAt.{u_1, u_2, u_4} 𝕜 (E := E) (f ∘ (⇑iso : (a : E) → F) : E → G)
    ((⇑iso : (a : E) → F) ⁻¹' s : Set E) ((iso.symm : (a : F) → E) ((iso : (a : E) → F) x : F) : E)

Tactic:
rw [← iso.symm_apply_apply x] at H

Premises used: ContinuousLinearEquiv.symm_apply_apply
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : F → G
s : Set F
x : E
H :
  DifferentiableWithinAt.{u_1, u_2, u_4} 𝕜 (E := E) (f ∘ (⇑iso : (a : E) → F) : E → G)
    ((⇑iso : (a : E) → F) ⁻¹' s : Set E) ((iso.symm : (a : F) → E) ((iso : (a : E) → F) x : F) : E)
apply : MapsTo.{u_3, u_2} (β := E) (⇑iso.symm : (a : F) → E) s ((⇑iso : (a : E) → F) ⁻¹' s)
⊢ DifferentiableWithinAt 𝕜
    (Function.comp.{u_3 + 1, u_2 + 1, u_4 + 1} (β := E) (f ∘ (⇑iso : (a : E) → F)) (⇑iso.symm : (a : F) → E)) s
    ((iso : (a : E) → F) x)

Tactic:
apply H.comp (iso x) iso.symm.differentiableWithinAt

Premises used: ContinuousLinearEquiv.symm, DifferentiableWithinAt.comp, ContinuousLinearEquiv.differentiableWithinAt, DFunLike.coe
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : F → G
s : Set F
x : E
H :
  DifferentiableWithinAt.{u_1, u_2, u_4} 𝕜 (E := E) (f ∘ (⇑iso : (a : E) → F) : E → G)
    ((⇑iso : (a : E) → F) ⁻¹' s : Set E) ((iso.symm : (a : F) → E) ((iso : (a : E) → F) x : F) : E)
y : F
hy : y ∈ s
⊢ Membership.mem.{u_2, u_2} (α := E) (γ := Set E) ((⇑iso : (a : E) → F) ⁻¹' s) ((iso.symm : (a : F) → E) y : E)

Tactic:
simpa only [mem_preimage, apply_symm_apply] using hy

Premises used: ContinuousLinearEquiv.apply_symm_apply, Set.mem_preimage
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : F → G
s : Set F
x : E
H : DifferentiableWithinAt 𝕜 (f ∘ (⇑iso : (a : E) → F)) ((⇑iso : (a : E) → F) ⁻¹' s) x
⊢ DifferentiableWithinAt 𝕜
    (Function.comp.{u_3 + 1, u_2 + 1, u_4 + 1} (β := E) (f ∘ (⇑iso : (a : E) → F)) (⇑iso.symm : (a : F) → E)) s
    ((iso : (a : E) → F) x)

Tactic:
have : DifferentiableWithinAt 𝕜 ((f ∘ iso) ∘ iso.symm) s (iso x) := by
    rw [← iso.symm_apply_apply x] at H
    apply H.comp (iso x) iso.symm.differentiableWithinAt
    intro y hy
    simpa only [mem_preimage, apply_symm_apply] using hy
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : F → G
s : Set F
x : E
H : DifferentiableWithinAt 𝕜 (f ∘ (⇑iso : (a : E) → F)) ((⇑iso : (a : E) → F) ⁻¹' s) x
this :
  DifferentiableWithinAt 𝕜
    (Function.comp.{u_3 + 1, u_2 + 1, u_4 + 1} (β := E) (f ∘ (⇑iso : (a : E) → F)) (⇑iso.symm : (a : F) → E)) s
    ((iso : (a : E) → F) x)
rwa :
  ∀
    (this :
      DifferentiableWithinAt 𝕜
        (f ∘ Function.comp.{u_3 + 1, u_2 + 1, u_3 + 1} (β := E) (⇑iso : (a : E) → F) (⇑iso.symm : (a : F) → E)) s
        ((iso : (a : E) → F) x)),
    DifferentiableWithinAt 𝕜 f s ((iso : (a : E) → F) x)
rwa₁ rwa₂ rwa₃ rwa₄ :
  ∀ (this : DifferentiableWithinAt 𝕜 (f ∘ id) s ((iso : (a : E) → F) x)),
    DifferentiableWithinAt 𝕜 f s ((iso : (a : E) → F) x)
⊢ DifferentiableWithinAt 𝕜 f s ((iso : (a : E) → F) x)

Tactic:
rwa [Function.comp_assoc, iso.self_comp_symm] at this

Premises used: ContinuousLinearEquiv.self_comp_symm, Function.comp_assoc
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : F → G
x : E
⊢ DifferentiableAt 𝕜 (f ∘ (⇑iso : (a : E) → F)) x ↔ DifferentiableAt 𝕜 f ((iso : (a : E) → F) x)

Tactic:
simp only [← differentiableWithinAt_univ, ← iso.comp_right_differentiableWithinAt_iff,
    preimage_univ]

Premises used: ContinuousLinearEquiv.comp_right_differentiableWithinAt_iff, Set.preimage_univ, differentiableWithinAt_univ
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : F → G
s : Set F
⊢ DifferentiableOn.{u_1, u_2, u_4} 𝕜 (E := E) (f ∘ (⇑iso : (a : E) → F)) ((⇑iso : (a : E) → F) ⁻¹' s) ↔
    DifferentiableOn 𝕜 f s

Tactic:
⟨fun H y hy => ?_, fun H y hy => iso.comp_right_differentiableWithinAt_iff.2 (H _ hy)⟩

Premises used: Iff.mpr, ContinuousLinearEquiv.comp_right_differentiableWithinAt_iff, Iff.intro, DFunLike.coe
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : F → G
s : Set F
refine :
  ∀ (H : DifferentiableOn.{u_1, u_2, u_4} 𝕜 (E := E) (f ∘ (⇑iso : (a : E) → F)) ((⇑iso : (a : E) → F) ⁻¹' s)) (y : F)
    (hy : y ∈ s), DifferentiableWithinAt 𝕜 f s y
⊢ DifferentiableOn.{u_1, u_2, u_4} 𝕜 (E := E) (f ∘ (⇑iso : (a : E) → F)) ((⇑iso : (a : E) → F) ⁻¹' s) ↔
    DifferentiableOn 𝕜 f s

Tactic:
refine ⟨fun H y hy => ?_, fun H y hy => iso.comp_right_differentiableWithinAt_iff.2 (H _ hy)⟩
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : F → G
s : Set F
H : DifferentiableOn.{u_1, u_2, u_4} 𝕜 (E := E) (f ∘ (⇑iso : (a : E) → F)) ((⇑iso : (a : E) → F) ⁻¹' s)
y : F
hy : y ∈ s
rw :
  DifferentiableWithinAt.{u_1, u_2, u_4} 𝕜 (E := E) (f ∘ (⇑iso : (a : E) → F) : E → G)
    ((⇑iso : (a : E) → F) ⁻¹' s : Set E) ((iso.symm : (a : F) → E) y : E)
⊢ DifferentiableWithinAt 𝕜 f s y

Tactic:
rw [← iso.apply_symm_apply y, ← comp_right_differentiableWithinAt_iff]

Premises used: ContinuousLinearEquiv.comp_right_differentiableWithinAt_iff, ContinuousLinearEquiv.apply_symm_apply