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 : 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
a : Membership.mem.{u_2, u_2} (α := E) (γ := Set E) ((⇑iso : (a : E) → F) ⁻¹' s) ((iso.symm : (a : F) → E) y : E)
⊢ 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)

Tactic:
apply 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 : 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
⊢ 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
⊢ Differentiable.{u_1, u_2, u_4} 𝕜 (E := E) (f ∘ (⇑iso : (a : E) → F)) ↔ Differentiable 𝕜 f

Tactic:
simp only [← differentiableOn_univ, ← iso.comp_right_differentiableOn_iff, preimage_univ]

Premises used: differentiableOn_univ, ContinuousLinearEquiv.comp_right_differentiableOn_iff, Set.preimage_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
x : E
f' : F →L[𝕜] G
⊢ HasFDerivWithinAt (f ∘ (⇑iso : (a : E) → F)) (f' ∘SL (↑iso : E →L[𝕜] F)) ((⇑iso : (a : E) → F) ⁻¹' s) x ↔
    HasFDerivWithinAt f f' s ((iso : (a : E) → F) x)

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

Premises used: Set.mapsTo_preimage, ContinuousLinearEquiv.hasFDerivWithinAt, HasFDerivWithinAt.comp, 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
x : E
f' : F →L[𝕜] G
refine :
  ∀ (H : HasFDerivWithinAt (f ∘ (⇑iso : (a : E) → F)) (f' ∘SL (↑iso : E →L[𝕜] F)) ((⇑iso : (a : E) → F) ⁻¹' s) x),
    HasFDerivWithinAt f f' s ((iso : (a : E) → F) x)
⊢ HasFDerivWithinAt (f ∘ (⇑iso : (a : E) → F)) (f' ∘SL (↑iso : E →L[𝕜] F)) ((⇑iso : (a : E) → F) ⁻¹' s) x ↔
    HasFDerivWithinAt f f' s ((iso : (a : E) → F) x)

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

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
f' : F →L[𝕜] G
H :
  HasFDerivWithinAt (f ∘ (⇑iso : (a : E) → F)) (f' ∘SL (↑iso : E →L[𝕜] F)) ((⇑iso : (a : E) → F) ⁻¹' s)
    ((iso.symm : (a : F) → E) ((iso : (a : E) → F) x : F))
rw : f = f ∘ id
⊢ f = Function.comp.{u_3 + 1, u_2 + 1, u_4 + 1} (β := E) (f ∘ (⇑iso : (a : E) → F)) (⇑iso.symm : (a : F) → E)

Tactic:
rw [Function.comp_assoc, iso.self_comp_symm]

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
s : Set F
x : E
f' : F →L[𝕜] G
H :
  HasFDerivWithinAt (f ∘ (⇑iso : (a : E) → F)) (f' ∘SL (↑iso : E →L[𝕜] F)) ((⇑iso : (a : E) → F) ⁻¹' s)
    ((iso.symm : (a : F) → E) ((iso : (a : E) → F) x : F))
⊢ f = f ∘ id

Tactic:
rfl
-- 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
f' : F →L[𝕜] G
H :
  HasFDerivWithinAt (f ∘ (⇑iso : (a : E) → F)) (f' ∘SL (↑iso : E →L[𝕜] F)) ((⇑iso : (a : E) → F) ⁻¹' s)
    ((iso.symm : (a : F) → E) ((iso : (a : E) → F) x : F))
⊢ f = Function.comp.{u_3 + 1, u_2 + 1, u_4 + 1} (β := E) (f ∘ (⇑iso : (a : E) → F)) (⇑iso.symm : (a : F) → E)

Tactic:
have A : f = (f ∘ iso) ∘ iso.symm := by
    rw [Function.comp_assoc, iso.self_comp_symm]
    rfl
-- 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
f' : F →L[𝕜] G
H :
  HasFDerivWithinAt (f ∘ (⇑iso : (a : E) → F)) (f' ∘SL (↑iso : E →L[𝕜] F)) ((⇑iso : (a : E) → F) ⁻¹' s)
    ((iso.symm : (a : F) → E) ((iso : (a : E) → F) x : F))
A : f = Function.comp.{u_3 + 1, u_2 + 1, u_4 + 1} (β := E) (f ∘ (⇑iso : (a : E) → F)) (⇑iso.symm : (a : F) → E)
rw : f' = f' ∘SL (↑iso : E →L[𝕜] F) ∘SL (↑iso.symm : F →L[𝕜] E)
rw₁ : f' = f' ∘SL ContinuousLinearMap.id 𝕜 F
rw₂ rw₃ : f' = f'
⊢ f' = (f' ∘SL (↑iso : E →L[𝕜] F)) ∘SL (↑iso.symm : F →L[𝕜] E)

Tactic:
rw [ContinuousLinearMap.comp_assoc, iso.coe_comp_coe_symm, ContinuousLinearMap.comp_id]

Premises used: ContinuousLinearEquiv.coe_comp_coe_symm, ContinuousLinearMap.comp_assoc, ContinuousLinearMap.comp_id
-- 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
f' : F →L[𝕜] G
H :
  HasFDerivWithinAt (f ∘ (⇑iso : (a : E) → F)) (f' ∘SL (↑iso : E →L[𝕜] F)) ((⇑iso : (a : E) → F) ⁻¹' s)
    ((iso.symm : (a : F) → E) ((iso : (a : E) → F) x : F))
A : f = Function.comp.{u_3 + 1, u_2 + 1, u_4 + 1} (β := E) (f ∘ (⇑iso : (a : E) → F)) (⇑iso.symm : (a : F) → E)
⊢ f' = (f' ∘SL (↑iso : E →L[𝕜] F)) ∘SL (↑iso.symm : F →L[𝕜] E)

Tactic:
have B : f' = (f'.comp (iso : E →L[𝕜] F)).comp (iso.symm : F →L[𝕜] E) := by
    rw [ContinuousLinearMap.comp_assoc, iso.coe_comp_coe_symm, ContinuousLinearMap.comp_id]
-- 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
f' : F →L[𝕜] G
H :
  HasFDerivWithinAt (f ∘ (⇑iso : (a : E) → F)) (f' ∘SL (↑iso : E →L[𝕜] F)) ((⇑iso : (a : E) → F) ⁻¹' s)
    ((iso.symm : (a : F) → E) ((iso : (a : E) → F) x : F))
A : f = Function.comp.{u_3 + 1, u_2 + 1, u_4 + 1} (β := E) (f ∘ (⇑iso : (a : E) → F)) (⇑iso.symm : (a : F) → E)
B : f' = (f' ∘SL (↑iso : E →L[𝕜] F)) ∘SL (↑iso.symm : F →L[𝕜] E)
rw :
  HasFDerivWithinAt
    (Function.comp.{u_3 + 1, u_2 + 1, u_4 + 1} (β := E) (f ∘ (⇑iso : (a : E) → F)) (⇑iso.symm : (a : F) → E))
    ((f' ∘SL (↑iso : E →L[𝕜] F)) ∘SL (↑iso.symm : F →L[𝕜] E)) s ((iso : (a : E) → F) x)
⊢ HasFDerivWithinAt f f' s ((iso : (a : E) → F) x)

Tactic:
rw [A, B]
-- 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
f' : F →L[𝕜] G
H :
  HasFDerivWithinAt (f ∘ (⇑iso : (a : E) → F)) (f' ∘SL (↑iso : E →L[𝕜] F)) ((⇑iso : (a : E) → F) ⁻¹' s)
    ((iso.symm : (a : F) → E) ((iso : (a : E) → F) x : F))
A : f = Function.comp.{u_3 + 1, u_2 + 1, u_4 + 1} (β := E) (f ∘ (⇑iso : (a : E) → F)) (⇑iso.symm : (a : F) → E)
B : f' = (f' ∘SL (↑iso : E →L[𝕜] F)) ∘SL (↑iso.symm : F →L[𝕜] E)
apply : MapsTo.{u_3, u_2} (β := E) (⇑iso.symm : (a : F) → E) s ((⇑iso : (a : E) → F) ⁻¹' s)
⊢ HasFDerivWithinAt
    (Function.comp.{u_3 + 1, u_2 + 1, u_4 + 1} (β := E) (f ∘ (⇑iso : (a : E) → F)) (⇑iso.symm : (a : F) → E))
    ((f' ∘SL (↑iso : E →L[𝕜] F)) ∘SL (↑iso.symm : F →L[𝕜] E)) s ((iso : (a : E) → F) x)

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

Premises used: ContinuousLinearEquiv.symm, ContinuousLinearEquiv.hasFDerivWithinAt, HasFDerivWithinAt.comp, 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
f' : F →L[𝕜] G
H :
  HasFDerivWithinAt (f ∘ (⇑iso : (a : E) → F)) (f' ∘SL (↑iso : E →L[𝕜] F)) ((⇑iso : (a : E) → F) ⁻¹' s)
    ((iso.symm : (a : F) → E) ((iso : (a : E) → F) x : F))
A : f = Function.comp.{u_3 + 1, u_2 + 1, u_4 + 1} (β := E) (f ∘ (⇑iso : (a : E) → F)) (⇑iso.symm : (a : F) → E)
B : f' = (f' ∘SL (↑iso : E →L[𝕜] F)) ∘SL (↑iso.symm : F →L[𝕜] 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
x : E
f' : F →L[𝕜] G
⊢ HasFDerivAt (f ∘ (⇑iso : (a : E) → F)) (f' ∘SL (↑iso : E →L[𝕜] F)) x ↔ HasFDerivAt f f' ((iso : (a : E) → F) x)

Tactic:
simp only [← hasFDerivWithinAt_univ, ← comp_right_hasFDerivWithinAt_iff, preimage_univ]

Premises used: ContinuousLinearEquiv.comp_right_hasFDerivWithinAt_iff, Set.preimage_univ, 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 : F → G
s : Set F
x : E
f' : E →L[𝕜] G
rw :
  HasFDerivWithinAt (f ∘ (⇑iso : (a : E) → F)) f' ((⇑iso : (a : E) → F) ⁻¹' s) x ↔
    HasFDerivWithinAt (f ∘ (⇑iso : (a : E) → F)) ((f' ∘SL (↑iso.symm : F →L[𝕜] E)) ∘SL (↑iso : E →L[𝕜] F))
      ((⇑iso : (a : E) → F) ⁻¹' s) x
rw₁ :
  HasFDerivWithinAt (f ∘ (⇑iso : (a : E) → F)) f' ((⇑iso : (a : E) → F) ⁻¹' s) x ↔
    HasFDerivWithinAt (f ∘ (⇑iso : (a : E) → F)) (f' ∘SL (↑iso.symm : F →L[𝕜] E) ∘SL (↑iso : E →L[𝕜] F))
      ((⇑iso : (a : E) → F) ⁻¹' s) x
rw₂ :
  HasFDerivWithinAt (f ∘ (⇑iso : (a : E) → F)) f' ((⇑iso : (a : E) → F) ⁻¹' s) x ↔
    HasFDerivWithinAt (f ∘ (⇑iso : (a : E) → F)) (f' ∘SL ContinuousLinearMap.id 𝕜 E) ((⇑iso : (a : E) → F) ⁻¹' s) x
rw₃ rw₄ :
  HasFDerivWithinAt (f ∘ (⇑iso : (a : E) → F)) f' ((⇑iso : (a : E) → F) ⁻¹' s) x ↔
    HasFDerivWithinAt (f ∘ (⇑iso : (a : E) → F)) f' ((⇑iso : (a : E) → F) ⁻¹' s) x
⊢ HasFDerivWithinAt (f ∘ (⇑iso : (a : E) → F)) f' ((⇑iso : (a : E) → F) ⁻¹' s) x ↔
    HasFDerivWithinAt f (f' ∘SL (↑iso.symm : F →L[𝕜] E)) s ((iso : (a : E) → F) x)

Tactic:
rw [← iso.comp_right_hasFDerivWithinAt_iff, ContinuousLinearMap.comp_assoc,
    iso.coe_symm_comp_coe, ContinuousLinearMap.comp_id]

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

Tactic:
simp only [← hasFDerivWithinAt_univ, ← iso.comp_right_hasFDerivWithinAt_iff', preimage_univ]

Premises used: ContinuousLinearEquiv.comp_right_hasFDerivWithinAt_iff', Set.preimage_univ, 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 : F → G
s : Set F
x : E
hxs : UniqueDiffWithinAt 𝕜 ((⇑iso : (a : E) → F) ⁻¹' s) x
pos :
  ∀ (h : DifferentiableWithinAt 𝕜 f s ((iso : (a : E) → F) x)),
    Eq (α := E →L[𝕜] G) (fderivWithin 𝕜 (f ∘ (⇑iso : (a : E) → F)) ((⇑iso : (a : E) → F) ⁻¹' s) x)
      (fderivWithin 𝕜 f s ((iso : (a : E) → F) x) ∘SL (↑iso : E →L[𝕜] F))
neg :
  ∀ (h : ¬DifferentiableWithinAt 𝕜 f s ((iso : (a : E) → F) x)),
    Eq (α := E →L[𝕜] G) (fderivWithin 𝕜 (f ∘ (⇑iso : (a : E) → F)) ((⇑iso : (a : E) → F) ⁻¹' s) x)
      (fderivWithin 𝕜 f s ((iso : (a : E) → F) x) ∘SL (↑iso : E →L[𝕜] F))
⊢ Eq (α := E →L[𝕜] G) (fderivWithin 𝕜 (f ∘ (⇑iso : (a : E) → F)) ((⇑iso : (a : E) → F) ⁻¹' s) x)
    (fderivWithin 𝕜 f s ((iso : (a : E) → F) x) ∘SL (↑iso : E →L[𝕜] F))

Tactic:
by_cases h : DifferentiableWithinAt 𝕜 f s (iso x)

Premises used: 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
hxs : UniqueDiffWithinAt 𝕜 ((⇑iso : (a : E) → F) ⁻¹' s) x
h : DifferentiableWithinAt 𝕜 f s ((iso : (a : E) → F) x)
⊢ Eq (α := E →L[𝕜] G) (fderivWithin 𝕜 (f ∘ (⇑iso : (a : E) → F)) ((⇑iso : (a : E) → F) ⁻¹' s) x)
    (fderivWithin 𝕜 f s ((iso : (a : E) → F) x) ∘SL (↑iso : E →L[𝕜] F))

Tactic:
(iso.comp_right_hasFDerivWithinAt_iff.2 h.hasFDerivWithinAt).fderivWithin hxs

Premises used: Iff.mpr, ContinuousLinearEquiv.comp_right_hasFDerivWithinAt_iff, HasFDerivWithinAt.fderivWithin, DifferentiableWithinAt.hasFDerivWithinAt
-- 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
hxs : UniqueDiffWithinAt 𝕜 ((⇑iso : (a : E) → F) ⁻¹' s) x
h : DifferentiableWithinAt 𝕜 f s ((iso : (a : E) → F) x)
⊢ Eq (α := E →L[𝕜] G) (fderivWithin 𝕜 (f ∘ (⇑iso : (a : E) → F)) ((⇑iso : (a : E) → F) ⁻¹' s) x)
    (fderivWithin 𝕜 f s ((iso : (a : E) → F) x) ∘SL (↑iso : E →L[𝕜] F))

Tactic:
exact (iso.comp_right_hasFDerivWithinAt_iff.2 h.hasFDerivWithinAt).fderivWithin hxs

Premises used: Iff.mpr, ContinuousLinearEquiv.comp_right_hasFDerivWithinAt_iff, HasFDerivWithinAt.fderivWithin, DifferentiableWithinAt.hasFDerivWithinAt
-- 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
hxs : UniqueDiffWithinAt 𝕜 ((⇑iso : (a : E) → F) ⁻¹' s) x
h : ¬DifferentiableWithinAt 𝕜 f s ((iso : (a : E) → F) x)
h' : DifferentiableWithinAt 𝕜 (f ∘ (⇑iso : (a : E) → F)) ((⇑iso : (a : E) → F) ⁻¹' s) x
⊢ False

Tactic:
h (iso.comp_right_differentiableWithinAt_iff.1 h')

Premises used: ContinuousLinearEquiv.comp_right_differentiableWithinAt_iff, Iff.mp
-- 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
hxs : UniqueDiffWithinAt 𝕜 ((⇑iso : (a : E) → F) ⁻¹' s) x
h : ¬DifferentiableWithinAt 𝕜 f s ((iso : (a : E) → F) x)
h' : DifferentiableWithinAt 𝕜 (f ∘ (⇑iso : (a : E) → F)) ((⇑iso : (a : E) → F) ⁻¹' s) x
⊢ False

Tactic:
exact h (iso.comp_right_differentiableWithinAt_iff.1 h')

Premises used: ContinuousLinearEquiv.comp_right_differentiableWithinAt_iff, Iff.mp
-- 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
hxs : UniqueDiffWithinAt 𝕜 ((⇑iso : (a : E) → F) ⁻¹' s) x
h : ¬DifferentiableWithinAt 𝕜 f s ((iso : (a : E) → F) x)
⊢ ¬DifferentiableWithinAt 𝕜 (f ∘ (⇑iso : (a : E) → F)) ((⇑iso : (a : E) → F) ⁻¹' s) x

Tactic:
have : ¬DifferentiableWithinAt 𝕜 (f ∘ iso) (iso ⁻¹' s) x := by
      intro h'
      exact h (iso.comp_right_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 : F → G
s : Set F
x : E
hxs : UniqueDiffWithinAt 𝕜 ((⇑iso : (a : E) → F) ⁻¹' s) x
h : ¬DifferentiableWithinAt 𝕜 f s ((iso : (a : E) → F) x)
this : ¬DifferentiableWithinAt 𝕜 (f ∘ (⇑iso : (a : E) → F)) ((⇑iso : (a : E) → F) ⁻¹' s) x
neg :
  Eq (α := E →L[𝕜] G) (fderivWithin 𝕜 (f ∘ (⇑iso : (a : E) → F)) ((⇑iso : (a : E) → F) ⁻¹' s) x)
    (comp (σ₂₃ := RingHom.id 𝕜) 0 (↑iso : E →L[𝕜] F))
neg₁ : Eq (α := E →L[𝕜] G) 0 (comp (σ₂₃ := RingHom.id 𝕜) 0 (↑iso : E →L[𝕜] F))
neg₂ neg₃ : Eq (α := E →L[𝕜] G) 0 0
⊢ Eq (α := E →L[𝕜] G) (fderivWithin 𝕜 (f ∘ (⇑iso : (a : E) → F)) ((⇑iso : (a : E) → F) ⁻¹' s) x)
    (fderivWithin 𝕜 f s ((iso : (a : E) → F) x) ∘SL (↑iso : E →L[𝕜] F))

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

Premises used: ContinuousLinearMap.zero_comp, 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 : F → G
x : E
rw : UniqueDiffWithinAt 𝕜 (preimage.{u_2, u_3} (β := F) (⇑iso : (a : E) → F) univ) x
⊢ Eq (α := E →L[𝕜] G) (fderiv 𝕜 (f ∘ (⇑iso : (a : E) → F)) x)
    (fderiv 𝕜 f ((iso : (a : E) → F) x) ∘SL (↑iso : E →L[𝕜] F))

Tactic:
rw [← fderivWithin_univ, ← fderivWithin_univ, ← iso.comp_right_fderivWithin, preimage_univ]

Premises used: fderivWithin_univ, ContinuousLinearEquiv.comp_right_fderivWithin, Set.preimage_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
x : E
⊢ UniqueDiffWithinAt 𝕜 (preimage.{u_2, u_3} (β := F) (⇑iso : (a : E) → F) univ) x

Tactic:
uniqueDiffWithinAt_univ

Premises used: Set.Mem, Set.univ, setOf, Set.preimage, uniqueDiffWithinAt_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
x : E
⊢ UniqueDiffWithinAt 𝕜 (preimage.{u_2, u_3} (β := F) (⇑iso : (a : E) → F) univ) x

Tactic:
exact uniqueDiffWithinAt_univ

Premises used: uniqueDiffWithinAt_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
x : E
iso : E ≃ₗᵢ[𝕜] F
⊢ HasStrictFDerivAt (⇑iso : (a : E) → F) (↑(↑iso : E ≃L[𝕜] F) : E →L[𝕜] F) x

Tactic:
(iso : E ≃L[𝕜] F).hasStrictFDerivAt

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

Tactic:
(iso : E ≃L[𝕜] F).hasFDerivWithinAt

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

Tactic:
(iso : E ≃L[𝕜] F).hasFDerivAt

Premises used: ContinuousLinearEquiv.hasFDerivAt, LinearIsometryEquiv.toContinuousLinearEquiv