{𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          [inst_3 : CompleteSpace E] →
            {F : Type u_3} →
              [inst_4 : NormedAddCommGroup F] →
                [inst_5 : NormedSpace 𝕜 F] →
                  [inst_6 : CompleteSpace F] →
                    {G : Type u_4} →
                      [inst_7 : NormedAddCommGroup G] →
                        [inst_8 : NormedSpace 𝕜 G] →
                          [inst_9 : CompleteSpace G] →
                            {motive : ImplicitFunctionData 𝕜 E F G → Sort u} →
                              (t : ImplicitFunctionData 𝕜 E F G) →
                                ((leftFun : E → F) →
                                    (leftDeriv : E →L[𝕜] F) →
                                      (rightFun : E → G) →
                                        (rightDeriv : E →L[𝕜] G) →
                                          (pt : E) →
                                            (hasStrictFDerivAt_leftFun : HasStrictFDerivAt leftFun leftDeriv pt) →
                                              (hasStrictFDerivAt_rightFun : HasStrictFDerivAt rightFun rightDeriv pt) →
                                                (range_leftDeriv : (↑leftDeriv).range = ⊤) →
                                                  (range_rightDeriv : (↑rightDeriv).range = ⊤) →
                                                    (isCompl_ker : IsCompl (↑leftDeriv).ker (↑rightDeriv).ker) →
                                                      motive
                                                        { leftFun := leftFun, leftDeriv := leftDeriv,
                                                          rightFun := rightFun, rightDeriv := rightDeriv, pt := pt,
                                                          hasStrictFDerivAt_leftFun := hasStrictFDerivAt_leftFun,
                                                          hasStrictFDerivAt_rightFun := hasStrictFDerivAt_rightFun,
                                                          range_leftDeriv := range_leftDeriv,
                                                          range_rightDeriv := range_rightDeriv,
                                                          isCompl_ker := isCompl_ker }) →
                                  motive t