[GOAL]
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : CompleteSpace E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : CompleteSpace F
G : Type u_4
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : CompleteSpace G
φ : ImplicitFunctionData 𝕜 E F G
⊢ map (Prod.fst ∘ prodFun φ) (𝓝 φ.pt) = 𝓝 (prodFun φ φ.pt).fst
[PROOFSTEP]
rw [← map_map, φ.hasStrictFDerivAt.map_nhds_eq_of_equiv, map_fst_nhds]
[GOAL]
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : CompleteSpace E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : CompleteSpace F
G : Type u_4
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : CompleteSpace G
φ : ImplicitFunctionData 𝕜 E F G
g'inv : G →L[𝕜] E
hg'inv : ContinuousLinearMap.comp φ.rightDeriv g'inv = ContinuousLinearMap.id 𝕜 G
hg'invf : ContinuousLinearMap.comp φ.leftDeriv g'inv = 0
⊢ HasStrictFDerivAt (implicitFunction φ (leftFun φ φ.pt)) g'inv (rightFun φ φ.pt)
[PROOFSTEP]
have := φ.hasStrictFDerivAt.to_localInverse
[GOAL]
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : CompleteSpace E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : CompleteSpace F
G : Type u_4
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : CompleteSpace G
φ : ImplicitFunctionData 𝕜 E F G
g'inv : G →L[𝕜] E
hg'inv : ContinuousLinearMap.comp φ.rightDeriv g'inv = ContinuousLinearMap.id 𝕜 G
hg'invf : ContinuousLinearMap.comp φ.leftDeriv g'inv = 0
this :
  HasStrictFDerivAt
    (HasStrictFDerivAt.localInverse (prodFun φ)
      (ContinuousLinearMap.equivProdOfSurjectiveOfIsCompl φ.leftDeriv φ.rightDeriv (_ : range φ.leftDeriv = ⊤)
        (_ : range φ.rightDeriv = ⊤) (_ : IsCompl (ker φ.leftDeriv) (ker φ.rightDeriv)))
      φ.pt
      (_ :
        HasStrictFDerivAt (prodFun φ)
          (↑(ContinuousLinearMap.equivProdOfSurjectiveOfIsCompl φ.leftDeriv φ.rightDeriv (_ : range φ.leftDeriv = ⊤)
              (_ : range φ.rightDeriv = ⊤) (_ : IsCompl (ker φ.leftDeriv) (ker φ.rightDeriv))))
          φ.pt))
    (↑(ContinuousLinearEquiv.symm
        (ContinuousLinearMap.equivProdOfSurjectiveOfIsCompl φ.leftDeriv φ.rightDeriv (_ : range φ.leftDeriv = ⊤)
          (_ : range φ.rightDeriv = ⊤) (_ : IsCompl (ker φ.leftDeriv) (ker φ.rightDeriv)))))
    (prodFun φ φ.pt)
⊢ HasStrictFDerivAt (implicitFunction φ (leftFun φ φ.pt)) g'inv (rightFun φ φ.pt)
[PROOFSTEP]
simp only [prodFun] at this 
[GOAL]
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : CompleteSpace E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : CompleteSpace F
G : Type u_4
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : CompleteSpace G
φ : ImplicitFunctionData 𝕜 E F G
g'inv : G →L[𝕜] E
hg'inv : ContinuousLinearMap.comp φ.rightDeriv g'inv = ContinuousLinearMap.id 𝕜 G
hg'invf : ContinuousLinearMap.comp φ.leftDeriv g'inv = 0
this :
  HasStrictFDerivAt
    (HasStrictFDerivAt.localInverse (fun x => (leftFun φ x, rightFun φ x))
      (ContinuousLinearMap.equivProdOfSurjectiveOfIsCompl φ.leftDeriv φ.rightDeriv (_ : range φ.leftDeriv = ⊤)
        (_ : range φ.rightDeriv = ⊤) (_ : IsCompl (ker φ.leftDeriv) (ker φ.rightDeriv)))
      φ.pt
      (_ :
        HasStrictFDerivAt (prodFun φ)
          (↑(ContinuousLinearMap.equivProdOfSurjectiveOfIsCompl φ.leftDeriv φ.rightDeriv (_ : range φ.leftDeriv = ⊤)
              (_ : range φ.rightDeriv = ⊤) (_ : IsCompl (ker φ.leftDeriv) (ker φ.rightDeriv))))
          φ.pt))
    ↑(ContinuousLinearEquiv.symm
        (ContinuousLinearMap.equivProdOfSurjectiveOfIsCompl φ.leftDeriv φ.rightDeriv (_ : range φ.leftDeriv = ⊤)
          (_ : range φ.rightDeriv = ⊤) (_ : IsCompl (ker φ.leftDeriv) (ker φ.rightDeriv))))
    (leftFun φ φ.pt, rightFun φ φ.pt)
⊢ HasStrictFDerivAt (implicitFunction φ (leftFun φ φ.pt)) g'inv (rightFun φ φ.pt)
[PROOFSTEP]
convert
  this.comp (φ.rightFun φ.pt)
    ((hasStrictFDerivAt_const _ _).prod (hasStrictFDerivAt_id _))
      -- porting note: added parentheses to help `simp`
[GOAL]
case h.e'_10
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : CompleteSpace E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : CompleteSpace F
G : Type u_4
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : CompleteSpace G
φ : ImplicitFunctionData 𝕜 E F G
g'inv : G →L[𝕜] E
hg'inv : ContinuousLinearMap.comp φ.rightDeriv g'inv = ContinuousLinearMap.id 𝕜 G
hg'invf : ContinuousLinearMap.comp φ.leftDeriv g'inv = 0
this :
  HasStrictFDerivAt
    (HasStrictFDerivAt.localInverse (fun x => (leftFun φ x, rightFun φ x))
      (ContinuousLinearMap.equivProdOfSurjectiveOfIsCompl φ.leftDeriv φ.rightDeriv (_ : range φ.leftDeriv = ⊤)
        (_ : range φ.rightDeriv = ⊤) (_ : IsCompl (ker φ.leftDeriv) (ker φ.rightDeriv)))
      φ.pt
      (_ :
        HasStrictFDerivAt (prodFun φ)
          (↑(ContinuousLinearMap.equivProdOfSurjectiveOfIsCompl φ.leftDeriv φ.rightDeriv (_ : range φ.leftDeriv = ⊤)
              (_ : range φ.rightDeriv = ⊤) (_ : IsCompl (ker φ.leftDeriv) (ker φ.rightDeriv))))
          φ.pt))
    ↑(ContinuousLinearEquiv.symm
        (ContinuousLinearMap.equivProdOfSurjectiveOfIsCompl φ.leftDeriv φ.rightDeriv (_ : range φ.leftDeriv = ⊤)
          (_ : range φ.rightDeriv = ⊤) (_ : IsCompl (ker φ.leftDeriv) (ker φ.rightDeriv))))
    (leftFun φ φ.pt, rightFun φ φ.pt)
⊢ g'inv =
    ContinuousLinearMap.comp
      (↑(ContinuousLinearEquiv.symm
          (ContinuousLinearMap.equivProdOfSurjectiveOfIsCompl φ.leftDeriv φ.rightDeriv (_ : range φ.leftDeriv = ⊤)
            (_ : range φ.rightDeriv = ⊤) (_ : IsCompl (ker φ.leftDeriv) (ker φ.rightDeriv)))))
      (ContinuousLinearMap.prod 0 (ContinuousLinearMap.id 𝕜 G))
[PROOFSTEP]
simp only [ContinuousLinearMap.ext_iff, (ContinuousLinearMap.comp_apply)] at hg'inv hg'invf ⊢
  -- porting note: was `simp [ContinuousLinearEquiv.eq_symm_apply]`;
    -- both `simp` and `rw` fail here, `erw` works
[GOAL]
case h.e'_10
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : CompleteSpace E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : CompleteSpace F
G : Type u_4
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : CompleteSpace G
φ : ImplicitFunctionData 𝕜 E F G
g'inv : G →L[𝕜] E
this :
  HasStrictFDerivAt
    (HasStrictFDerivAt.localInverse (fun x => (leftFun φ x, rightFun φ x))
      (ContinuousLinearMap.equivProdOfSurjectiveOfIsCompl φ.leftDeriv φ.rightDeriv (_ : range φ.leftDeriv = ⊤)
        (_ : range φ.rightDeriv = ⊤) (_ : IsCompl (ker φ.leftDeriv) (ker φ.rightDeriv)))
      φ.pt
      (_ :
        HasStrictFDerivAt (prodFun φ)
          (↑(ContinuousLinearMap.equivProdOfSurjectiveOfIsCompl φ.leftDeriv φ.rightDeriv (_ : range φ.leftDeriv = ⊤)
              (_ : range φ.rightDeriv = ⊤) (_ : IsCompl (ker φ.leftDeriv) (ker φ.rightDeriv))))
          φ.pt))
    ↑(ContinuousLinearEquiv.symm
        (ContinuousLinearMap.equivProdOfSurjectiveOfIsCompl φ.leftDeriv φ.rightDeriv (_ : range φ.leftDeriv = ⊤)
          (_ : range φ.rightDeriv = ⊤) (_ : IsCompl (ker φ.leftDeriv) (ker φ.rightDeriv))))
    (leftFun φ φ.pt, rightFun φ φ.pt)
hg'inv : ∀ (x : G), ↑φ.rightDeriv (↑g'inv x) = ↑(ContinuousLinearMap.id 𝕜 G) x
hg'invf : ∀ (x : G), ↑φ.leftDeriv (↑g'inv x) = ↑0 x
⊢ ∀ (x : G),
    ↑g'inv x =
      ↑↑(ContinuousLinearEquiv.symm
              (ContinuousLinearMap.equivProdOfSurjectiveOfIsCompl φ.leftDeriv φ.rightDeriv (_ : range φ.leftDeriv = ⊤)
                (_ : range φ.rightDeriv = ⊤) (_ : IsCompl (ker φ.leftDeriv) (ker φ.rightDeriv))))
        (↑(ContinuousLinearMap.prod 0 (ContinuousLinearMap.id 𝕜 G)) x)
[PROOFSTEP]
intro x
[GOAL]
case h.e'_10
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : CompleteSpace E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : CompleteSpace F
G : Type u_4
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : CompleteSpace G
φ : ImplicitFunctionData 𝕜 E F G
g'inv : G →L[𝕜] E
this :
  HasStrictFDerivAt
    (HasStrictFDerivAt.localInverse (fun x => (leftFun φ x, rightFun φ x))
      (ContinuousLinearMap.equivProdOfSurjectiveOfIsCompl φ.leftDeriv φ.rightDeriv (_ : range φ.leftDeriv = ⊤)
        (_ : range φ.rightDeriv = ⊤) (_ : IsCompl (ker φ.leftDeriv) (ker φ.rightDeriv)))
      φ.pt
      (_ :
        HasStrictFDerivAt (prodFun φ)
          (↑(ContinuousLinearMap.equivProdOfSurjectiveOfIsCompl φ.leftDeriv φ.rightDeriv (_ : range φ.leftDeriv = ⊤)
              (_ : range φ.rightDeriv = ⊤) (_ : IsCompl (ker φ.leftDeriv) (ker φ.rightDeriv))))
          φ.pt))
    ↑(ContinuousLinearEquiv.symm
        (ContinuousLinearMap.equivProdOfSurjectiveOfIsCompl φ.leftDeriv φ.rightDeriv (_ : range φ.leftDeriv = ⊤)
          (_ : range φ.rightDeriv = ⊤) (_ : IsCompl (ker φ.leftDeriv) (ker φ.rightDeriv))))
    (leftFun φ φ.pt, rightFun φ φ.pt)
hg'inv : ∀ (x : G), ↑φ.rightDeriv (↑g'inv x) = ↑(ContinuousLinearMap.id 𝕜 G) x
hg'invf : ∀ (x : G), ↑φ.leftDeriv (↑g'inv x) = ↑0 x
x : G
⊢ ↑g'inv x =
    ↑↑(ContinuousLinearEquiv.symm
            (ContinuousLinearMap.equivProdOfSurjectiveOfIsCompl φ.leftDeriv φ.rightDeriv (_ : range φ.leftDeriv = ⊤)
              (_ : range φ.rightDeriv = ⊤) (_ : IsCompl (ker φ.leftDeriv) (ker φ.rightDeriv))))
      (↑(ContinuousLinearMap.prod 0 (ContinuousLinearMap.id 𝕜 G)) x)
[PROOFSTEP]
erw [ContinuousLinearEquiv.eq_symm_apply]
[GOAL]
case h.e'_10
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : CompleteSpace E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : CompleteSpace F
G : Type u_4
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : CompleteSpace G
φ : ImplicitFunctionData 𝕜 E F G
g'inv : G →L[𝕜] E
this :
  HasStrictFDerivAt
    (HasStrictFDerivAt.localInverse (fun x => (leftFun φ x, rightFun φ x))
      (ContinuousLinearMap.equivProdOfSurjectiveOfIsCompl φ.leftDeriv φ.rightDeriv (_ : range φ.leftDeriv = ⊤)
        (_ : range φ.rightDeriv = ⊤) (_ : IsCompl (ker φ.leftDeriv) (ker φ.rightDeriv)))
      φ.pt
      (_ :
        HasStrictFDerivAt (prodFun φ)
          (↑(ContinuousLinearMap.equivProdOfSurjectiveOfIsCompl φ.leftDeriv φ.rightDeriv (_ : range φ.leftDeriv = ⊤)
              (_ : range φ.rightDeriv = ⊤) (_ : IsCompl (ker φ.leftDeriv) (ker φ.rightDeriv))))
          φ.pt))
    ↑(ContinuousLinearEquiv.symm
        (ContinuousLinearMap.equivProdOfSurjectiveOfIsCompl φ.leftDeriv φ.rightDeriv (_ : range φ.leftDeriv = ⊤)
          (_ : range φ.rightDeriv = ⊤) (_ : IsCompl (ker φ.leftDeriv) (ker φ.rightDeriv))))
    (leftFun φ φ.pt, rightFun φ φ.pt)
hg'inv : ∀ (x : G), ↑φ.rightDeriv (↑g'inv x) = ↑(ContinuousLinearMap.id 𝕜 G) x
hg'invf : ∀ (x : G), ↑φ.leftDeriv (↑g'inv x) = ↑0 x
x : G
⊢ ↑(ContinuousLinearMap.equivProdOfSurjectiveOfIsCompl φ.leftDeriv φ.rightDeriv (_ : range φ.leftDeriv = ⊤)
          (_ : range φ.rightDeriv = ⊤) (_ : IsCompl (ker φ.leftDeriv) (ker φ.rightDeriv)))
      (↑g'inv x) =
    ↑(ContinuousLinearMap.prod 0 (ContinuousLinearMap.id 𝕜 G)) x
[PROOFSTEP]
simp [*]
[GOAL]
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : CompleteSpace E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
f : E → F
f' : E →L[𝕜] F
a : E
hf : HasStrictFDerivAt f f' a
hf' : range f' = ⊤
hker : Submodule.ClosedComplemented (ker f')
y : { x // x ∈ ker f' }
⊢ ↑(implicitToLocalHomeomorphOfComplemented f f' hf hf' hker) (↑y + a) = (f (↑y + a), y)
[PROOFSTEP]
simp only [implicitToLocalHomeomorphOfComplemented_apply, add_sub_cancel, Classical.choose_spec hker]
[GOAL]
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : CompleteSpace E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
f : E → F
f' : E →L[𝕜] F
a : E
hf : HasStrictFDerivAt f f' a
hf' : range f' = ⊤
hker : Submodule.ClosedComplemented (ker f')
⊢ ↑(implicitToLocalHomeomorphOfComplemented f f' hf hf' hker) a = (f a, 0)
[PROOFSTEP]
simp [hf.implicitToLocalHomeomorphOfComplemented_apply]
[GOAL]
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : CompleteSpace E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
f : E → F
f' : E →L[𝕜] F
a : E
hf : HasStrictFDerivAt f f' a
hf' : range f' = ⊤
hker : Submodule.ClosedComplemented (ker f')
⊢ (f a, 0) ∈ (implicitToLocalHomeomorphOfComplemented f f' hf hf' hker).toLocalEquiv.target
[PROOFSTEP]
simpa only [implicitToLocalHomeomorphOfComplemented_self] using
  (hf.implicitToLocalHomeomorphOfComplemented f f' hf' hker).map_source <|
    hf.mem_implicitToLocalHomeomorphOfComplemented_source hf' hker
[GOAL]
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : CompleteSpace E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
f : E → F
f' : E →L[𝕜] F
a : E
hf : HasStrictFDerivAt f f' a
hf' : range f' = ⊤
hker : Submodule.ClosedComplemented (ker f')
⊢ implicitFunctionOfComplemented f f' hf hf' hker (f a) 0 = a
[PROOFSTEP]
simpa only [implicitToLocalHomeomorphOfComplemented_self] using
  (hf.implicitToLocalHomeomorphOfComplemented f f' hf' hker).left_inv
    (hf.mem_implicitToLocalHomeomorphOfComplemented_source hf' hker)
[GOAL]
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : CompleteSpace E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
f : E → F
f' : E →L[𝕜] F
a : E
hf : HasStrictFDerivAt f f' a
hf' : range f' = ⊤
hker : Submodule.ClosedComplemented (ker f')
⊢ HasStrictFDerivAt (implicitFunctionOfComplemented f f' hf hf' hker (f a)) (Submodule.subtypeL (ker f')) 0
[PROOFSTEP]
convert (implicitFunctionDataOfComplemented f f' hf hf' hker).implicitFunction_hasStrictFDerivAt (ker f').subtypeL _ _
[GOAL]
case h.e'_11
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : CompleteSpace E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
f : E → F
f' : E →L[𝕜] F
a : E
hf : HasStrictFDerivAt f f' a
hf' : range f' = ⊤
hker : Submodule.ClosedComplemented (ker f')
⊢ 0 =
    ImplicitFunctionData.rightFun (implicitFunctionDataOfComplemented f f' hf hf' hker)
      (implicitFunctionDataOfComplemented f f' hf hf' hker).pt
case convert_1
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : CompleteSpace E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
f : E → F
f' : E →L[𝕜] F
a : E
hf : HasStrictFDerivAt f f' a
hf' : range f' = ⊤
hker : Submodule.ClosedComplemented (ker f')
⊢ ContinuousLinearMap.comp (implicitFunctionDataOfComplemented f f' hf hf' hker).rightDeriv
      (Submodule.subtypeL (ker f')) =
    ContinuousLinearMap.id 𝕜 { x // x ∈ ker f' }
case convert_2
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : CompleteSpace E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
f : E → F
f' : E →L[𝕜] F
a : E
hf : HasStrictFDerivAt f f' a
hf' : range f' = ⊤
hker : Submodule.ClosedComplemented (ker f')
⊢ ContinuousLinearMap.comp (implicitFunctionDataOfComplemented f f' hf hf' hker).leftDeriv
      (Submodule.subtypeL (ker f')) =
    0
[PROOFSTEP]
swap
[GOAL]
case convert_1
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : CompleteSpace E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
f : E → F
f' : E →L[𝕜] F
a : E
hf : HasStrictFDerivAt f f' a
hf' : range f' = ⊤
hker : Submodule.ClosedComplemented (ker f')
⊢ ContinuousLinearMap.comp (implicitFunctionDataOfComplemented f f' hf hf' hker).rightDeriv
      (Submodule.subtypeL (ker f')) =
    ContinuousLinearMap.id 𝕜 { x // x ∈ ker f' }
[PROOFSTEP]
ext
  -- Porting note: added parentheses to help `simp`
[GOAL]
case convert_1.h.a
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : CompleteSpace E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
f : E → F
f' : E →L[𝕜] F
a : E
hf : HasStrictFDerivAt f f' a
hf' : range f' = ⊤
hker : Submodule.ClosedComplemented (ker f')
x✝ : { x // x ∈ ker f' }
⊢ ↑(↑(ContinuousLinearMap.comp (implicitFunctionDataOfComplemented f f' hf hf' hker).rightDeriv
            (Submodule.subtypeL (ker f')))
        x✝) =
    ↑(↑(ContinuousLinearMap.id 𝕜 { x // x ∈ ker f' }) x✝)
[PROOFSTEP]
simp only [Classical.choose_spec hker, implicitFunctionDataOfComplemented, (ContinuousLinearMap.comp_apply),
  Submodule.coe_subtypeL', Submodule.coeSubtype, (ContinuousLinearMap.id_apply)]
[GOAL]
case h.e'_11
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : CompleteSpace E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
f : E → F
f' : E →L[𝕜] F
a : E
hf : HasStrictFDerivAt f f' a
hf' : range f' = ⊤
hker : Submodule.ClosedComplemented (ker f')
⊢ 0 =
    ImplicitFunctionData.rightFun (implicitFunctionDataOfComplemented f f' hf hf' hker)
      (implicitFunctionDataOfComplemented f f' hf hf' hker).pt
case convert_2
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : CompleteSpace E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
f : E → F
f' : E →L[𝕜] F
a : E
hf : HasStrictFDerivAt f f' a
hf' : range f' = ⊤
hker : Submodule.ClosedComplemented (ker f')
⊢ ContinuousLinearMap.comp (implicitFunctionDataOfComplemented f f' hf hf' hker).leftDeriv
      (Submodule.subtypeL (ker f')) =
    0
[PROOFSTEP]
swap
[GOAL]
case convert_2
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : CompleteSpace E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
f : E → F
f' : E →L[𝕜] F
a : E
hf : HasStrictFDerivAt f f' a
hf' : range f' = ⊤
hker : Submodule.ClosedComplemented (ker f')
⊢ ContinuousLinearMap.comp (implicitFunctionDataOfComplemented f f' hf hf' hker).leftDeriv
      (Submodule.subtypeL (ker f')) =
    0
[PROOFSTEP]
ext
  -- Porting note: added parentheses to help `simp`
[GOAL]
case convert_2.h
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : CompleteSpace E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
f : E → F
f' : E →L[𝕜] F
a : E
hf : HasStrictFDerivAt f f' a
hf' : range f' = ⊤
hker : Submodule.ClosedComplemented (ker f')
x✝ : { x // x ∈ ker f' }
⊢ ↑(ContinuousLinearMap.comp (implicitFunctionDataOfComplemented f f' hf hf' hker).leftDeriv
          (Submodule.subtypeL (ker f')))
      x✝ =
    ↑0 x✝
[PROOFSTEP]
simp only [(ContinuousLinearMap.comp_apply), Submodule.coe_subtypeL', Submodule.coeSubtype, LinearMap.map_coe_ker,
  (ContinuousLinearMap.zero_apply)]
[GOAL]
case h.e'_11
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : CompleteSpace E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
f : E → F
f' : E →L[𝕜] F
a : E
hf : HasStrictFDerivAt f f' a
hf' : range f' = ⊤
hker : Submodule.ClosedComplemented (ker f')
⊢ 0 =
    ImplicitFunctionData.rightFun (implicitFunctionDataOfComplemented f f' hf hf' hker)
      (implicitFunctionDataOfComplemented f f' hf hf' hker).pt
[PROOFSTEP]
simp only [implicitFunctionDataOfComplemented, map_sub, sub_self]
[GOAL]
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : CompleteSpace 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : CompleteSpace E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : FiniteDimensional 𝕜 F
f : E → F
f' : E →L[𝕜] F
a : E
hf : HasStrictFDerivAt f f' a
hf' : range f' = ⊤
α : Type u_4
l : Filter α
g₁ : α → F
g₂ : α → { x // x ∈ ker f' }
h₁ : Tendsto g₁ l (𝓝 (f a))
h₂ : Tendsto g₂ l (𝓝 0)
⊢ Tendsto (fun t => implicitFunction f f' hf hf' (g₁ t) (g₂ t)) l (𝓝 a)
[PROOFSTEP]
refine' ((hf.implicitToLocalHomeomorph f f' hf').tendsto_symm (hf.mem_implicitToLocalHomeomorph_source hf')).comp _
[GOAL]
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : CompleteSpace 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : CompleteSpace E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : FiniteDimensional 𝕜 F
f : E → F
f' : E →L[𝕜] F
a : E
hf : HasStrictFDerivAt f f' a
hf' : range f' = ⊤
α : Type u_4
l : Filter α
g₁ : α → F
g₂ : α → { x // x ∈ ker f' }
h₁ : Tendsto g₁ l (𝓝 (f a))
h₂ : Tendsto g₂ l (𝓝 0)
⊢ Tendsto (fun t => (g₁ t, g₂ t)) l (𝓝 (↑(implicitToLocalHomeomorph f f' hf hf') a))
[PROOFSTEP]
rw [implicitToLocalHomeomorph_self]
[GOAL]
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : CompleteSpace 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : CompleteSpace E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : FiniteDimensional 𝕜 F
f : E → F
f' : E →L[𝕜] F
a : E
hf : HasStrictFDerivAt f f' a
hf' : range f' = ⊤
α : Type u_4
l : Filter α
g₁ : α → F
g₂ : α → { x // x ∈ ker f' }
h₁ : Tendsto g₁ l (𝓝 (f a))
h₂ : Tendsto g₂ l (𝓝 0)
⊢ Tendsto (fun t => (g₁ t, g₂ t)) l (𝓝 (f a, 0))
[PROOFSTEP]
exact h₁.prod_mk_nhds h₂
[GOAL]
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : CompleteSpace 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : CompleteSpace E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : FiniteDimensional 𝕜 F
f : E → F
f' : E →L[𝕜] F
a : E
hf : HasStrictFDerivAt f f' a
hf' : range f' = ⊤
⊢ implicitFunction f f' hf hf' (f a) 0 = a
[PROOFSTEP]
haveI := FiniteDimensional.complete 𝕜 F
[GOAL]
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : CompleteSpace 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : CompleteSpace E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : FiniteDimensional 𝕜 F
f : E → F
f' : E →L[𝕜] F
a : E
hf : HasStrictFDerivAt f f' a
hf' : range f' = ⊤
this : CompleteSpace F
⊢ implicitFunction f f' hf hf' (f a) 0 = a
[PROOFSTEP]
apply implicitFunctionOfComplemented_apply_image
