-- Mathlib/Analysis/Calculus/FDeriv/Equiv.lean
theorem HasFDerivWithinAt.of_local_left_inverse {g : F → E} {f' : E ≃L[𝕜] F} {a : F} {t : Set F}
    (hg : Tendsto g (𝓝[t] a) (𝓝[s] (g a))) (hf : HasFDerivWithinAt f (f' : E →L[𝕜] F) s (g a))
    (ha : a ∈ t) (hfg : ∀ᶠ y in 𝓝[t] a, f (g y) = y) :
    HasFDerivWithinAt g (f'.symm : F →L[𝕜] E) t a

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
f : E → F
s : Set E
g : F → E
f' : E ≃L[𝕜] F
a : F
t : Set F
hg : Tendsto g (𝓝[t] a) (𝓝[s] g a)
hf : HasFDerivWithinAt f (↑f') s (g a)
ha : a ∈ t
hfg : ∀ᶠ (y : F) in 𝓝[t] a, f (g y) = y
this : (fun x => g x - g a - f'.symm (x - a)) =O[𝓝[t] a] fun x => f' (g x - g a) - (x - a)
⊢ HasFDerivWithinAt g (↑f'.symm) t a

Tactic:
refine .of_isLittleO <| this.trans_isLittleO ?_

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
f : E → F
s : Set E
g : F → E
f' : E ≃L[𝕜] F
a : F
t : Set F
hg : Tendsto g (𝓝[t] a) (𝓝[s] g a)
hf : HasFDerivWithinAt f (↑f') s (g a)
ha : a ∈ t
hfg : ∀ᶠ (y : F) in 𝓝[t] a, f (g y) = y
this : (fun x => g x - g a - f'.symm (x - a)) =O[𝓝[t] a] fun x => f' (g x - g a) - (x - a)
⊢ (fun x => f' (g x - g a) - (x - a)) =o[𝓝[t] a] fun x' => x' - a

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
f : E → F
s : Set E
g : F → E
f' : E ≃L[𝕜] F
a : F
t : Set F
hg : Tendsto g (𝓝[t] a) (𝓝[s] g a)
hf : HasFDerivWithinAt f (↑f') s (g a)
ha : a ∈ t
hfg : ∀ᶠ (y : F) in 𝓝[t] a, f (g y) = y
this : (fun x => g x - g a - f'.symm (x - a)) =O[𝓝[t] a] fun x => f' (g x - g a) - (x - a)
⊢ (fun x => f' (g x - g a) - (x - a)) =o[𝓝[t] a] fun x' => x' - a

Tactic:
clear this

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
f : E → F
s : Set E
g : F → E
f' : E ≃L[𝕜] F
a : F
t : Set F
hg : Tendsto g (𝓝[t] a) (𝓝[s] g a)
hf : HasFDerivWithinAt f (↑f') s (g a)
ha : a ∈ t
hfg : ∀ᶠ (y : F) in 𝓝[t] a, f (g y) = y
⊢ (fun x => f' (g x - g a) - (x - a)) =o[𝓝[t] a] fun x' => x' - a

Proof state:
case refine_2
𝕜 : 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
f : E → F
s : Set E
g : F → E
f' : E ≃L[𝕜] F
a : F
t : Set F
hg : Tendsto g (𝓝[t] a) (𝓝[s] g a)
hf : HasFDerivWithinAt f (↑f') s (g a)
ha : a ∈ t
hfg : ∀ᶠ (y : F) in 𝓝[t] a, f (g y) = y
⊢ ∀ (x : F), f (g x) = x → ((fun x' => f x' - f (g a)) ∘ g) x = (fun x' => x' - a) x

Tactic:
rintro p hp

Result:
case refine_2
𝕜 : 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
f : E → F
s : Set E
g : F → E
f' : E ≃L[𝕜] F
a : F
t : Set F
hg : Tendsto g (𝓝[t] a) (𝓝[s] g a)
hf : HasFDerivWithinAt f (↑f') s (g a)
ha : a ∈ t
hfg : ∀ᶠ (y : F) in 𝓝[t] a, f (g y) = y
p : F
hp : f (g p) = p
⊢ ((fun x' => f x' - f (g a)) ∘ g) p = (fun x' => x' - a) p

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
f : E → F
s : Set E
g : F → E
f' : E ≃L[𝕜] F
a : F
t : Set F
hg : Tendsto g (𝓝[t] a) (𝓝[s] g a)
hf : HasFDerivWithinAt f (↑f') s (g a)
ha : a ∈ t
hfg : ∀ᶠ (y : F) in 𝓝[t] a, f (g y) = y
⊢ HasFDerivWithinAt g (↑f'.symm) t a

Tactic:
have : (fun x : F => g x - g a - f'.symm (x - a)) =O[𝓝[t] a]
    fun x : F => f' (g x - g a) - (x - a) :=
  ((f'.symm : F →L[𝕜] E).isBigO_comp _ _).congr (fun x ↦ by simp) fun _ ↦ 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
f : E → F
s : Set E
g : F → E
f' : E ≃L[𝕜] F
a : F
t : Set F
hg : Tendsto g (𝓝[t] a) (𝓝[s] g a)
hf : HasFDerivWithinAt f (↑f') s (g a)
ha : a ∈ t
hfg : ∀ᶠ (y : F) in 𝓝[t] a, f (g y) = y
this : (fun x => g x - g a - f'.symm (x - a)) =O[𝓝[t] a] fun x => f' (g x - g a) - (x - a)
⊢ HasFDerivWithinAt g (↑f'.symm) t a

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
f : E → F
s : Set E
g : F → E
f' : E ≃L[𝕜] F
a : F
t : Set F
hg : Tendsto g (𝓝[t] a) (𝓝[s] g a)
hf : HasFDerivWithinAt f (↑f') s (g a)
ha : a ∈ t
hfg : ∀ᶠ (y : F) in 𝓝[t] a, f (g y) = y
⊢ (fun x => f' (g x - g a) - (x - a)) =o[𝓝[t] a] fun x' => x' - a

Tactic:
refine ((hf.isLittleO.comp_tendsto hg).symm.congr' (hfg.mono ?_) .rfl).trans_isBigO ?_

Result:
case refine_1
𝕜 : 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
f : E → F
s : Set E
g : F → E
f' : E ≃L[𝕜] F
a : F
t : Set F
hg : Tendsto g (𝓝[t] a) (𝓝[s] g a)
hf : HasFDerivWithinAt f (↑f') s (g a)
ha : a ∈ t
hfg : ∀ᶠ (y : F) in 𝓝[t] a, f (g y) = y
⊢ ∀ (x : F), f (g x) = x → (fun x => ↑f' (g x - g a) - (f (g x) - f (g a))) x = f' (g x - g a) - (x - a)

case refine_2
𝕜 : 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
f : E → F
s : Set E
g : F → E
f' : E ≃L[𝕜] F
a : F
t : Set F
hg : Tendsto g (𝓝[t] a) (𝓝[s] g a)
hf : HasFDerivWithinAt f (↑f') s (g a)
ha : a ∈ t
hfg : ∀ᶠ (y : F) in 𝓝[t] a, f (g y) = y
⊢ ((fun x' => x' - g a) ∘ g) =O[𝓝[t] a] fun x' => x' - a

Proof state:
case refine_2
𝕜 : 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
f : E → F
s : Set E
g : F → E
f' : E ≃L[𝕜] F
a : F
t : Set F
hg : Tendsto g (𝓝[t] a) (𝓝[s] g a)
hf : HasFDerivWithinAt f (↑f') s (g a)
ha : a ∈ t
hfg : ∀ᶠ (y : F) in 𝓝[t] a, f (g y) = y
⊢ ((fun x' => x' - g a) ∘ g) =O[𝓝[t] a] fun x' => x' - a

Tactic:
refine ((hf.isBigO_sub_rev f'.antilipschitz).comp_tendsto hg).congr'
  (Eventually.of_forall fun _ => rfl) (hfg.mono ?_)

Result:
case refine_2
𝕜 : 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
f : E → F
s : Set E
g : F → E
f' : E ≃L[𝕜] F
a : F
t : Set F
hg : Tendsto g (𝓝[t] a) (𝓝[s] g a)
hf : HasFDerivWithinAt f (↑f') s (g a)
ha : a ∈ t
hfg : ∀ᶠ (y : F) in 𝓝[t] a, f (g y) = y
⊢ ∀ (x : F), f (g x) = x → ((fun x' => f x' - f (g a)) ∘ g) x = (fun x' => x' - a) 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
f : E → F
s : Set E
g : F → E
f' : E ≃L[𝕜] F
a : F
t : Set F
hg : Tendsto g (𝓝[t] a) (𝓝[s] g a)
hf : HasFDerivWithinAt f (↑f') s (g a)
ha : a ∈ t
hfg : ∀ᶠ (y : F) in 𝓝[t] a, f (g y) = y
x : F
⊢ ↑f'.symm (f' (g x - g a) - (x - a)) = g x - g a - f'.symm (x - a)

Tactic:
simp

Result:
no goals