awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.FDeriv.Defs
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : E → F
f' : E →L[𝕜] F
x : E
s : Set E
⊢ HasFDerivWithinAt f f' s x ↔
    IsLittleOTVS.{u_1, u_2, u_3, u_2} 𝕜 (E := F) (F := E) (𝓝[s] x)
      (fun (x' : E) ↦ HSub.hSub (β := F) (f x' - f x) ((f' : (a : E) → F) (x' - x) : F)) fun (x' : E) ↦ x' - x

Tactic:
simp [HasFDerivWithinAt, hasFDerivAtFilter_iff_isLittleOTVS, Function.comp_def]

Premises used: HasFDerivWithinAt, hasFDerivAtFilter_iff_isLittleOTVS, Function.comp_def
-- Module: Mathlib.Analysis.Calculus.FDeriv.Defs
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : E → F
f' : E →L[𝕜] F
x : E
⊢ HasStrictFDerivAt f f' x ↔
    IsLittleOTVS.{u_1, u_2, u_3, u_2} 𝕜 (E := F) (F := E) (𝓝 (x, x))
      (fun (p : E × E) ↦ HSub.hSub (β := F) (f p.1 - f p.2) ((f' : (a : E) → F) (p.1 - p.2) : F)) fun (p : E × E) ↦
      p.1 - p.2

Tactic:
hasFDerivAtFilter_iff_isLittleOTVS ..

Premises used: hasFDerivAtFilter_iff_isLittleOTVS, HasStrictFDerivAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Defs
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : E → F
x : E
s : Set E
h : ¬DifferentiableWithinAt 𝕜 f s x
⊢ Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 f s x) 0

Tactic:
simp [fderivWithin, h]

Premises used: fderivWithin
-- Module: Mathlib.Analysis.Calculus.FDeriv.Defs
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : E → F
h :
  ∀ (x x_1 : E),
    Eq.{u_3 + 1} (α := F) ((fderivWithin 𝕜 f univ x : (a : E) → F) x_1 : F) ((fderiv 𝕜 f x : (a : E) → F) x_1 : F)
⊢ Eq (α := (x : E) → E →L[𝕜] F) (fderivWithin 𝕜 f univ) (fderiv 𝕜 f)

Tactic:
ext
-- Module: Mathlib.Analysis.Calculus.FDeriv.Defs
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : E → F
x x_1 : E
h h₁ :
  Eq.{u_3 + 1} (α := F) ((fderivWithin 𝕜 f univ x : (a : E) → F) x_1 : F)
    ((fderivWithin 𝕜 f univ x : (a : E) → F) x_1 : F)
⊢ Eq.{u_3 + 1} (α := F) ((fderivWithin 𝕜 f univ x : (a : E) → F) x_1 : F) ((fderiv 𝕜 f x : (a : E) → F) x_1 : F)

Tactic:
rw [fderiv]

Premises used: fderiv
-- Module: Mathlib.Analysis.Calculus.FDeriv.Defs
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
L : Filter (E × E)
⊢ HasFDerivAtFilter f f' L ↔
    IsLittleO.{u_2, u_3, u_2} (E := F) (F := E) L
      (fun (p : E × E) ↦ HSub.hSub (β := F) (f p.1 - f p.2) ((f' : (a : E) → F) (p.1 - p.2) : F)) fun (p : E × E) ↦
      p.1 - p.2

Tactic:
(hasFDerivAtFilter_iff_isLittleOTVS ..).trans isLittleOTVS_iff_isLittleO

Premises used: Asymptotics.isLittleOTVS_iff_isLittleO, hasFDerivAtFilter_iff_isLittleOTVS, Iff.trans
-- Module: Mathlib.Analysis.Calculus.FDeriv.Defs
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x : E
⊢ HasFDerivAt f f' x ↔
    IsLittleO.{u_2, u_3, u_2} (E := F) (F := E) (𝓝 x)
      (fun (x' : E) ↦ HSub.hSub (β := F) (f x' - f x) ((f' : (a : E) → F) (x' - x) : F)) fun (x' : E) ↦ x' - x

Tactic:
hasFDerivAt_iff_isLittleOTVS.trans isLittleOTVS_iff_isLittleO

Premises used: Asymptotics.isLittleOTVS_iff_isLittleO, hasFDerivAt_iff_isLittleOTVS, Iff.trans
-- Module: Mathlib.Analysis.Calculus.FDeriv.Defs
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
s : Set E
x : E
⊢ HasFDerivWithinAt f f' s x ↔
    IsLittleO.{u_2, u_3, u_2} (E := F) (F := E) (𝓝[s] x)
      (fun (x' : E) ↦ HSub.hSub (β := F) (f x' - f x) ((f' : (a : E) → F) (x' - x) : F)) fun (x' : E) ↦ x' - x

Tactic:
hasFDerivWithinAt_iff_isLittleOTVS.trans isLittleOTVS_iff_isLittleO

Premises used: Asymptotics.isLittleOTVS_iff_isLittleO, Iff.trans, hasFDerivWithinAt_iff_isLittleOTVS
-- Module: Mathlib.Analysis.Calculus.FDeriv.Defs
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x : E
⊢ HasStrictFDerivAt f f' x ↔
    IsLittleO.{u_2, u_3, u_2} (E := F) (F := E) (𝓝 (x, x))
      (fun (p : E × E) ↦ HSub.hSub (β := F) (f p.1 - f p.2) ((f' : (a : E) → F) (p.1 - p.2) : F)) fun (p : E × E) ↦
      p.1 - p.2

Tactic:
(hasStrictFDerivAt_iff_isLittleOTVS ..).trans isLittleOTVS_iff_isLittleO

Premises used: hasStrictFDerivAt_iff_isLittleOTVS, Asymptotics.isLittleOTVS_iff_isLittleO, Iff.trans
-- 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
x : E
iso : E ≃L[𝕜] F
⊢ HasStrictFDerivAt (⇑iso : (a : E) → F) (↑iso : E →L[𝕜] F) x

Tactic:
iso.toContinuousLinearMap.hasStrictFDerivAt

Premises used: ContinuousLinearMap.hasStrictFDerivAt, ContinuousLinearEquiv.toContinuousLinearMap
-- 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
x : E
s : Set E
iso : E ≃L[𝕜] F
⊢ HasFDerivWithinAt (⇑iso : (a : E) → F) (↑iso : E →L[𝕜] F) s x

Tactic:
iso.toContinuousLinearMap.hasFDerivWithinAt

Premises used: ContinuousLinearMap.hasFDerivWithinAt, ContinuousLinearEquiv.toContinuousLinearMap
-- 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
x : E
iso : E ≃L[𝕜] F
⊢ HasFDerivAt (⇑iso : (a : E) → F) (↑iso : E →L[𝕜] F) x

Tactic:
iso.toContinuousLinearMap.hasFDerivAtFilter

Premises used: HasFDerivAt, ContinuousLinearMap.hasFDerivAtFilter, ContinuousLinearEquiv.toContinuousLinearMap
-- 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
x : E
iso : E ≃L[𝕜] F
⊢ DifferentiableAt.{u_1, u_2, u_3} 𝕜 (F := F) (⇑iso : (a : E) → F) x

Tactic:
iso.hasFDerivAt.differentiableAt

Premises used: HasFDerivAt.differentiableAt, ContinuousLinearEquiv.hasFDerivAt
-- 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
x : E
s : Set E
iso : E ≃L[𝕜] F
⊢ DifferentiableWithinAt.{u_1, u_2, u_3} 𝕜 (F := F) (⇑iso : (a : E) → F) s x

Tactic:
iso.differentiableAt.differentiableWithinAt

Premises used: DifferentiableAt.differentiableWithinAt, ContinuousLinearEquiv.differentiableAt
-- 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
x : E
iso : E ≃L[𝕜] F
⊢ fderiv 𝕜 (⇑iso : (a : E) → F) x = (↑iso : E →L[𝕜] F)

Tactic:
iso.hasFDerivAt.fderiv

Premises used: HasFDerivAt.fderiv, ContinuousLinearEquiv.hasFDerivAt
-- 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
x : E
s : Set E
iso : E ≃L[𝕜] F
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ fderivWithin 𝕜 (⇑iso : (a : E) → F) s x = (↑iso : E →L[𝕜] F)

Tactic:
iso.toContinuousLinearMap.fderivWithin hxs

Premises used: ContinuousLinearMap.fderivWithin, ContinuousLinearEquiv.toContinuousLinearMap
-- 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
iso : E ≃L[𝕜] F
⊢ Differentiable.{u_1, u_2, u_3} 𝕜 (E := E) (F := F) (⇑iso : (a : E) → F)

Tactic:
fun _ => iso.differentiableAt

Premises used: Differentiable, ContinuousLinearEquiv.differentiableAt
-- 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
s : Set E
iso : E ≃L[𝕜] F
⊢ DifferentiableOn.{u_1, u_2, u_3} 𝕜 (F := F) (⇑iso : (a : E) → F) s

Tactic:
iso.differentiable.differentiableOn

Premises used: ContinuousLinearEquiv.differentiable, Differentiable.differentiableOn
-- 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
⊢ DifferentiableWithinAt.{u_1, u_4, u_3} 𝕜 (F := F) ((⇑iso : (a : E) → F) ∘ f) s x ↔ DifferentiableWithinAt 𝕜 f s x

Tactic:
⟨fun H => ?_, fun H => iso.differentiable.differentiableAt.comp_differentiableWithinAt x H⟩

Premises used: ContinuousLinearEquiv.differentiable, Differentiable.differentiableAt, Iff.intro, DifferentiableAt.comp_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
refine :
  ∀ (H : DifferentiableWithinAt.{u_1, u_4, u_3} 𝕜 (F := F) ((⇑iso : (a : E) → F) ∘ f) s x),
    DifferentiableWithinAt 𝕜 f s x
⊢ DifferentiableWithinAt.{u_1, u_4, u_3} 𝕜 (F := F) ((⇑iso : (a : E) → F) ∘ f) s x ↔ DifferentiableWithinAt 𝕜 f s x

Tactic:
refine ⟨fun H => ?_, fun H => iso.differentiable.differentiableAt.comp_differentiableWithinAt x 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
H : DifferentiableWithinAt.{u_1, u_4, u_3} 𝕜 (F := F) ((⇑iso : (a : E) → F) ∘ f) s x
⊢ DifferentiableWithinAt.{u_1, u_4, u_2} 𝕜 (F := E)
    (Function.comp.{u_4 + 1, u_3 + 1, u_2 + 1} (β := F) (⇑iso.symm : (a : F) → E) ((⇑iso : (a : E) → F) ∘ f)) s x

Tactic:
have : DifferentiableWithinAt 𝕜 (iso.symm ∘ iso ∘ f) s x :=
    iso.symm.differentiable.differentiableAt.comp_differentiableWithinAt x 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
H : DifferentiableWithinAt.{u_1, u_4, u_3} 𝕜 (F := F) ((⇑iso : (a : E) → F) ∘ f) s x
this :
  DifferentiableWithinAt.{u_1, u_4, u_2} 𝕜 (F := E)
    (Function.comp.{u_4 + 1, u_3 + 1, u_2 + 1} (β := F) (⇑iso.symm : (a : F) → E) ((⇑iso : (a : E) → F) ∘ f)) s x
rwa :
  ∀
    (this :
      DifferentiableWithinAt 𝕜 (F := E)
        (Function.comp.{u_2 + 1, u_3 + 1, u_2 + 1} (β := F) (⇑iso.symm : (a : F) → E) (⇑iso : (a : E) → F) ∘ f) s x),
    DifferentiableWithinAt 𝕜 f s x
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (this : DifferentiableWithinAt 𝕜 (id ∘ f) s x), DifferentiableWithinAt 𝕜 f s x
⊢ DifferentiableWithinAt 𝕜 f s x

Tactic:
rwa [← Function.comp_assoc iso.symm iso f, iso.symm_comp_self] at this

Premises used: ContinuousLinearEquiv.symm, ContinuousLinearEquiv.symm_comp_self, DFunLike.coe, 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 : G → E
x : G
rw : DifferentiableWithinAt.{u_1, u_4, u_3} 𝕜 (F := F) ((⇑iso : (a : E) → F) ∘ f) univ x ↔ DifferentiableAt 𝕜 f x
rw₁ :
  DifferentiableWithinAt.{u_1, u_4, u_3} 𝕜 (F := F) ((⇑iso : (a : E) → F) ∘ f) univ x ↔
    DifferentiableWithinAt 𝕜 f univ x
rw₂ rw₃ : DifferentiableWithinAt 𝕜 f univ x ↔ DifferentiableWithinAt 𝕜 f univ x
⊢ DifferentiableAt.{u_1, u_4, u_3} 𝕜 (F := F) ((⇑iso : (a : E) → F) ∘ f) x ↔ DifferentiableAt 𝕜 f x

Tactic:
rw [← differentiableWithinAt_univ, ← differentiableWithinAt_univ,
    iso.comp_differentiableWithinAt_iff]

Premises used: differentiableWithinAt_univ, ContinuousLinearEquiv.comp_differentiableWithinAt_iff
-- 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 ∈ s, DifferentiableWithinAt.{u_1, u_4, u_3} 𝕜 (F := F) ((⇑iso : (a : E) → F) ∘ f) s x) ↔
    ∀ x ∈ s, DifferentiableWithinAt 𝕜 f s x

Tactic:
simp only [iso.comp_differentiableWithinAt_iff]

Premises used: ContinuousLinearEquiv.comp_differentiableWithinAt_iff
-- 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
rw : DifferentiableOn.{u_1, u_4, u_3} 𝕜 (F := F) ((⇑iso : (a : E) → F) ∘ f) univ ↔ DifferentiableOn 𝕜 f univ
⊢ Differentiable.{u_1, u_4, u_3} 𝕜 (F := F) ((⇑iso : (a : E) → F) ∘ f) ↔ Differentiable 𝕜 f

Tactic:
rw [← differentiableOn_univ, ← differentiableOn_univ]

Premises used: differentiableOn_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
⊢ DifferentiableOn.{u_1, u_4, u_3} 𝕜 (F := F) ((⇑iso : (a : E) → F) ∘ f) univ ↔ DifferentiableOn 𝕜 f univ

Tactic:
iso.comp_differentiableOn_iff

Premises used: ContinuousLinearEquiv.comp_differentiableOn_iff
-- 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
⊢ DifferentiableOn.{u_1, u_4, u_3} 𝕜 (F := F) ((⇑iso : (a : E) → F) ∘ f) univ ↔ DifferentiableOn 𝕜 f univ

Tactic:
exact iso.comp_differentiableOn_iff

Premises used: ContinuousLinearEquiv.comp_differentiableOn_iff
-- 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[𝕜] E
⊢ HasFDerivWithinAt ((⇑iso : (a : E) → F) ∘ f) ((↑iso : E →L[𝕜] F) ∘SL f') s x ↔ HasFDerivWithinAt f f' s x

Tactic:
⟨fun H => ?_, fun H => iso.hasFDerivAt.comp_hasFDerivWithinAt x H⟩

Premises used: HasFDerivAt.comp_hasFDerivWithinAt, Iff.intro, ContinuousLinearEquiv.hasFDerivAt
-- 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[𝕜] E
refine :
  ∀ (H : HasFDerivWithinAt ((⇑iso : (a : E) → F) ∘ f) ((↑iso : E →L[𝕜] F) ∘SL f') s x), HasFDerivWithinAt f f' s x
⊢ HasFDerivWithinAt ((⇑iso : (a : E) → F) ∘ f) ((↑iso : E →L[𝕜] F) ∘SL f') s x ↔ HasFDerivWithinAt f f' s x

Tactic:
refine ⟨fun H => ?_, fun H => iso.hasFDerivAt.comp_hasFDerivWithinAt x 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
f' : G →L[𝕜] E
H : HasFDerivWithinAt ((⇑iso : (a : E) → F) ∘ f) ((↑iso : E →L[𝕜] F) ∘SL f') s x
⊢ HasFDerivWithinAt f f' s x

Tactic:
simpa [Function.comp_def, ← ContinuousLinearMap.comp_assoc]
    using iso.symm.hasFDerivAt.comp_hasFDerivWithinAt x H

Premises used: ContinuousLinearEquiv.symm, HasFDerivAt.comp_hasFDerivWithinAt, Function.comp_def, ContinuousLinearMap.comp_assoc, ContinuousLinearEquiv.hasFDerivAt
-- 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
⊢ HasStrictFDerivAt ((⇑iso : (a : E) → F) ∘ f) ((↑iso : E →L[𝕜] F) ∘SL f') x ↔ HasStrictFDerivAt f f' x

Tactic:
⟨fun H => ?_, fun H => iso.hasStrictFDerivAt.comp x H⟩

Premises used: ContinuousLinearEquiv.hasStrictFDerivAt, Iff.intro, HasStrictFDerivAt.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[𝕜] E
refine : ∀ (H : HasStrictFDerivAt ((⇑iso : (a : E) → F) ∘ f) ((↑iso : E →L[𝕜] F) ∘SL f') x), HasStrictFDerivAt f f' x
⊢ HasStrictFDerivAt ((⇑iso : (a : E) → F) ∘ f) ((↑iso : E →L[𝕜] F) ∘SL f') x ↔ HasStrictFDerivAt f f' x

Tactic:
refine ⟨fun H => ?_, fun H => iso.hasStrictFDerivAt.comp x 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
x : G
f' : G →L[𝕜] E
H : HasStrictFDerivAt ((⇑iso : (a : E) → F) ∘ f) ((↑iso : E →L[𝕜] F) ∘SL f') x
⊢ HasStrictFDerivAt (fun (x : G) ↦ (iso.symm : (a : F) → E) (((⇑iso : (a : E) → F) ∘ f) x))
    ((↑iso.symm : F →L[𝕜] E) ∘SL (↑iso : E →L[𝕜] F) ∘SL f') x

Tactic:
iso.symm.hasStrictFDerivAt.comp x H

Premises used: ContinuousLinearEquiv.symm, ContinuousLinearEquiv.hasStrictFDerivAt, HasStrictFDerivAt.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[𝕜] E
H : HasStrictFDerivAt ((⇑iso : (a : E) → F) ∘ f) ((↑iso : E →L[𝕜] F) ∘SL f') x
h : f = fun (x : G) ↦ (iso.symm : (a : F) → E) (((⇑iso : (a : E) → F) ∘ f) x)
h₁ : f' = (↑iso.symm : F →L[𝕜] E) ∘SL (↑iso : E →L[𝕜] F) ∘SL f'
⊢ HasStrictFDerivAt f f' x

Tactic:
convert! iso.symm.hasStrictFDerivAt.comp x H using 1

Premises used: ContinuousLinearEquiv.symm, ContinuousLinearEquiv.hasStrictFDerivAt, HasStrictFDerivAt.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[𝕜] E
H : HasStrictFDerivAt ((⇑iso : (a : E) → F) ∘ f) ((↑iso : E →L[𝕜] F) ∘SL f') x
h : ∀ (z : G), f z = (iso.symm : (a : F) → E) (((⇑iso : (a : E) → F) ∘ f) z)
⊢ f = fun (x : G) ↦ (iso.symm : (a : F) → E) (((⇑iso : (a : E) → F) ∘ f) x)

Tactic:
ext z
-- 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
H : HasStrictFDerivAt ((⇑iso : (a : E) → F) ∘ f) ((↑iso : E →L[𝕜] F) ∘SL f') x
h :
  ∀ (z : G),
    Eq.{u_2 + 1} (α := E) ((f' : (a : G) → E) z : E)
      (((↑iso.symm : F →L[𝕜] E) ∘SL (↑iso : E →L[𝕜] F) ∘SL f' : (a : G) → E) z : E)
⊢ f' = (↑iso.symm : F →L[𝕜] E) ∘SL (↑iso : E →L[𝕜] F) ∘SL f'

Tactic:
ext z
-- 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
H : HasStrictFDerivAt ((⇑iso : (a : E) → F) ∘ f) ((↑iso : E →L[𝕜] F) ∘SL f') x
z : G
⊢ f z = (iso.symm : (a : F) → E) (((⇑iso : (a : E) → F) ∘ f) z)

Tactic:
apply (iso.symm_apply_apply _).symm

Premises used: ContinuousLinearEquiv.symm_apply_apply, Eq.symm
-- 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
H : HasStrictFDerivAt ((⇑iso : (a : E) → F) ∘ f) ((↑iso : E →L[𝕜] F) ∘SL f') x
z : G
⊢ Eq.{u_2 + 1} (α := E) ((f' : (a : G) → E) z : E)
    (((↑iso.symm : F →L[𝕜] E) ∘SL (↑iso : E →L[𝕜] F) ∘SL f' : (a : G) → E) z : E)

Tactic:
apply (iso.symm_apply_apply _).symm

Premises used: ContinuousLinearEquiv.symm_apply_apply, Eq.symm