-- Mathlib/Analysis/Calculus/FDeriv/Equiv.lean
theorem comp_hasFDerivWithinAt_iff {f : G → E} {s : Set G} {x : G} {f' : G →L[𝕜] E} :
    HasFDerivWithinAt (iso ∘ f) ((iso : E →L[𝕜] F).comp f') s x ↔ HasFDerivWithinAt f f' s x

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : G → E
s : Set G
x : G
f' : G →L[𝕜] E
H : HasFDerivWithinAt (⇑iso ∘ f) ((↑iso).comp f') s x
A : f = ⇑iso.symm ∘ ⇑iso ∘ f
⊢ HasFDerivWithinAt f f' s x

Tactic:
have B : f' = (iso.symm : F →L[𝕜] E).comp ((iso : E →L[𝕜] F).comp f') := by
  rw [← ContinuousLinearMap.comp_assoc, iso.coe_symm_comp_coe, ContinuousLinearMap.id_comp]

Result:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : G → E
s : Set G
x : G
f' : G →L[𝕜] E
H : HasFDerivWithinAt (⇑iso ∘ f) ((↑iso).comp f') s x
A : f = ⇑iso.symm ∘ ⇑iso ∘ f
B : f' = (↑iso.symm).comp ((↑iso).comp f')
⊢ HasFDerivWithinAt f f' s x

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : G → E
s : Set G
x : G
f' : G →L[𝕜] E
H : HasFDerivWithinAt (⇑iso ∘ f) ((↑iso).comp f') s x
⊢ f = ⇑iso.symm ∘ ⇑iso ∘ f

Tactic:
rw [← Function.comp_assoc, iso.symm_comp_self]

Result:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : G → E
s : Set G
x : G
f' : G →L[𝕜] E
H : HasFDerivWithinAt (⇑iso ∘ f) ((↑iso).comp f') s x
⊢ f = _root_.id ∘ f

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : G → E
s : Set G
x : G
f' : G →L[𝕜] E
H : HasFDerivWithinAt (⇑iso ∘ f) ((↑iso).comp f') s x
⊢ HasFDerivWithinAt f f' s x

Tactic:
have A : f = iso.symm ∘ iso ∘ f := by
  rw [← Function.comp_assoc, iso.symm_comp_self]
  rfl

Result:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : G → E
s : Set G
x : G
f' : G →L[𝕜] E
H : HasFDerivWithinAt (⇑iso ∘ f) ((↑iso).comp f') s x
A : f = ⇑iso.symm ∘ ⇑iso ∘ f
⊢ HasFDerivWithinAt f f' s x

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : G → E
s : Set G
x : G
f' : G →L[𝕜] E
H : HasFDerivWithinAt (⇑iso ∘ f) ((↑iso).comp f') s x
A : f = ⇑iso.symm ∘ ⇑iso ∘ f
⊢ f' = (↑iso.symm).comp ((↑iso).comp f')

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

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : G → E
s : Set G
x : G
f' : G →L[𝕜] E
⊢ HasFDerivWithinAt (⇑iso ∘ f) ((↑iso).comp f') s x ↔ HasFDerivWithinAt f f' s x

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

Result:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : G → E
s : Set G
x : G
f' : G →L[𝕜] E
H : HasFDerivWithinAt (⇑iso ∘ f) ((↑iso).comp f') s x
⊢ HasFDerivWithinAt f f' s x

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : G → E
s : Set G
x : G
f' : G →L[𝕜] E
H : HasFDerivWithinAt (⇑iso ∘ f) ((↑iso).comp f') s x
A : f = ⇑iso.symm ∘ ⇑iso ∘ f
B : f' = (↑iso.symm).comp ((↑iso).comp f')
⊢ HasFDerivWithinAt (⇑iso.symm ∘ ⇑iso ∘ f) ((↑iso.symm).comp ((↑iso).comp f')) s x

Tactic:
exact iso.symm.hasFDerivAt.comp_hasFDerivWithinAt x H

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : G → E
s : Set G
x : G
f' : G →L[𝕜] E
H : HasFDerivWithinAt (⇑iso ∘ f) ((↑iso).comp f') s x
A : f = ⇑iso.symm ∘ ⇑iso ∘ f
B : f' = (↑iso.symm).comp ((↑iso).comp f')
⊢ HasFDerivWithinAt f f' s x

Tactic:
rw [A, B]

Result:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : G → E
s : Set G
x : G
f' : G →L[𝕜] E
H : HasFDerivWithinAt (⇑iso ∘ f) ((↑iso).comp f') s x
A : f = ⇑iso.symm ∘ ⇑iso ∘ f
B : f' = (↑iso.symm).comp ((↑iso).comp f')
⊢ HasFDerivWithinAt (⇑iso.symm ∘ ⇑iso ∘ f) ((↑iso.symm).comp ((↑iso).comp f')) s x

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : G → E
s : Set G
x : G
f' : G →L[𝕜] E
H : HasFDerivWithinAt (⇑iso ∘ f) ((↑iso).comp f') s x
⊢ f = _root_.id ∘ f

Tactic:
rfl

Result:
no goals