awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.Implicit
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : CompleteSpace E
F : Type u_3
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
inst_7 : FiniteDimensional 𝕜 F
f : E → F
f' : E →L[𝕜] F
a : E
hf : HasStrictFDerivAt f f' a
hf' : (↑f' : E →ₗ[𝕜] F).range = ⊤
⊢ ∀ᶠ (p : Prod.{u_3, u_2} F ↥(↑f' : E →ₗ[𝕜] F).ker) in 𝓝 (f a, 0), f (implicitFunction f f' hf hf' p.1 p.2) = p.1

Tactic:
have := FiniteDimensional.complete 𝕜 F
  map_implicitFunctionOfComplemented_eq ..

Premises used: HasStrictFDerivAt.map_implicitFunctionOfComplemented_eq, Set.Mem, ImplicitFunctionData.implicitFunction, HasStrictFDerivAt.implicitToOpenPartialHomeomorphOfComplemented, _private.0.HasStrictFDerivAt.implicitToOpenPartialHomeomorph._proof_2, HasStrictFDerivAt.implicitToOpenPartialHomeomorph, HasStrictFDerivAt.implicitFunctionOfComplemented, HasStrictFDerivAt.implicitFunction, FiniteDimensional.complete
-- Module: Mathlib.Analysis.Calculus.Implicit
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : CompleteSpace E
F : Type u_3
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
inst_7 : FiniteDimensional 𝕜 F
f : E → F
f' : E →L[𝕜] F
a : E
hf : HasStrictFDerivAt f f' a
hf' : (↑f' : E →ₗ[𝕜] F).range = ⊤
⊢ CompleteSpace F

Tactic:
have := FiniteDimensional.complete 𝕜 F
-- Module: Mathlib.Analysis.Calculus.Implicit
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : CompleteSpace E
F : Type u_3
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
inst_7 : FiniteDimensional 𝕜 F
f : E → F
f' : E →L[𝕜] F
a : E
hf : HasStrictFDerivAt f f' a
hf' : (↑f' : E →ₗ[𝕜] F).range = ⊤
this : CompleteSpace F
⊢ implicitFunction f f' hf hf' (f a) 0 = a

Tactic:
apply implicitFunctionOfComplemented_apply_image

Premises used: HasStrictFDerivAt.implicitFunctionOfComplemented_apply_image
-- Module: Mathlib.Analysis.Calculus.Implicit
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : CompleteSpace E
F : Type u_3
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
inst_7 : FiniteDimensional 𝕜 F
f : E → F
f' : E →L[𝕜] F
a : E
hf : HasStrictFDerivAt f f' a
hf' : (↑f' : E →ₗ[𝕜] F).range = ⊤
⊢ ∀ᶠ (x : E) in 𝓝 a,
    implicitFunction f f' hf hf' (f x)
        ((↑(implicitToOpenPartialHomeomorph f f' hf hf') : E → F × ↥(↑f' : E →ₗ[𝕜] F).ker) x).2 =
      x

Tactic:
have := FiniteDimensional.complete 𝕜 F
  eq_implicitFunctionOfComplemented ..

Premises used: Set.Mem, HasStrictFDerivAt.eq_implicitFunctionOfComplemented, ImplicitFunctionData.implicitFunction, HasStrictFDerivAt.implicitToOpenPartialHomeomorphOfComplemented, _private.0.HasStrictFDerivAt.implicitToOpenPartialHomeomorph._proof_2, HasStrictFDerivAt.implicitToOpenPartialHomeomorph, HasStrictFDerivAt.implicitFunctionOfComplemented, HasStrictFDerivAt.implicitFunction, FiniteDimensional.complete
-- Module: Mathlib.Analysis.Calculus.Implicit
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : CompleteSpace E
F : Type u_3
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
inst_7 : FiniteDimensional 𝕜 F
f : E → F
f' : E →L[𝕜] F
a : E
hf : HasStrictFDerivAt f f' a
hf' : (↑f' : E →ₗ[𝕜] F).range = ⊤
⊢ HasStrictFDerivAt (implicitFunction f f' hf hf' (f a)) (↑f' : E →ₗ[𝕜] F).ker.subtypeL 0

Tactic:
have := FiniteDimensional.complete 𝕜 F
  to_implicitFunctionOfComplemented ..

Premises used: Set.Mem, ImplicitFunctionData.implicitFunction, HasStrictFDerivAt.to_implicitFunctionOfComplemented, HasStrictFDerivAt.implicitToOpenPartialHomeomorphOfComplemented, _private.0.HasStrictFDerivAt.implicitToOpenPartialHomeomorph._proof_2, HasStrictFDerivAt.implicitToOpenPartialHomeomorph, HasStrictFDerivAt.implicitFunctionOfComplemented, HasStrictFDerivAt.implicitFunction, FiniteDimensional.complete
-- Module: Mathlib.Analysis.Calculus.ImplicitContDiff
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E₁ : Type u_2
inst_1 : NormedAddCommGroup E₁
inst_2 : NormedSpace 𝕜 E₁
inst_3 : CompleteSpace E₁
E₂ : Type u_3
inst_4 : NormedAddCommGroup E₂
inst_5 : NormedSpace 𝕜 E₂
inst_6 : CompleteSpace E₂
F : Type u_4
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace 𝕜 F
inst_9 : CompleteSpace F
φ : ImplicitFunctionData 𝕜 E₁ E₂ F
n : ℕ∞ω
hl : ContDiffAt 𝕜 n φ.leftFun φ.pt
hr : ContDiffAt 𝕜 n φ.rightFun φ.pt
pn : n ≠ 0
rw :
  ContDiffAt 𝕜 n
    (HasStrictFDerivAt.localInverse φ.prodFun (φ.leftDeriv.equivProdOfSurjectiveOfIsCompl φ.rightDeriv ⋯ ⋯ ⋯) φ.pt ⋯)
    (φ.prodFun φ.pt)
⊢ ContDiffAt 𝕜 n (Function.uncurry φ.implicitFunction) (φ.prodFun φ.pt)

Tactic:
rw [implicitFunction_def, Function.uncurry_curry, ← HasStrictFDerivAt.localInverse_def]

Premises used: Function.uncurry_curry, HasStrictFDerivAt.localInverse_def, ImplicitFunctionData.implicitFunction_def
-- Module: Mathlib.Analysis.Calculus.ImplicitContDiff
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E₁ : Type u_2
inst_1 : NormedAddCommGroup E₁
inst_2 : NormedSpace 𝕜 E₁
inst_3 : CompleteSpace E₁
E₂ : Type u_3
inst_4 : NormedAddCommGroup E₂
inst_5 : NormedSpace 𝕜 E₂
inst_6 : CompleteSpace E₂
F : Type u_4
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace 𝕜 F
inst_9 : CompleteSpace F
φ : ImplicitFunctionData 𝕜 E₁ E₂ F
n : ℕ∞ω
hl : ContDiffAt 𝕜 n φ.leftFun φ.pt
hr : ContDiffAt 𝕜 n φ.rightFun φ.pt
pn : n ≠ 0
refine : ContDiffAt 𝕜 n φ.prodFun φ.pt
⊢ ContDiffAt 𝕜 n
    (HasStrictFDerivAt.localInverse φ.prodFun (φ.leftDeriv.equivProdOfSurjectiveOfIsCompl φ.rightDeriv ⋯ ⋯ ⋯) φ.pt ⋯)
    (φ.prodFun φ.pt)

Tactic:
refine ContDiffAt.to_localInverse ?_ (φ.hasStrictFDerivAt.hasFDerivAt) pn

Premises used: ImplicitFunctionData.hasStrictFDerivAt, HasStrictFDerivAt.hasFDerivAt, ContDiffAt.to_localInverse
-- Module: Mathlib.Analysis.Calculus.ImplicitContDiff
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E₁ : Type u_2
inst_1 : NormedAddCommGroup E₁
inst_2 : NormedSpace 𝕜 E₁
inst_3 : CompleteSpace E₁
E₂ : Type u_3
inst_4 : NormedAddCommGroup E₂
inst_5 : NormedSpace 𝕜 E₂
inst_6 : CompleteSpace E₂
F : Type u_4
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace 𝕜 F
inst_9 : CompleteSpace F
φ : ImplicitFunctionData 𝕜 E₁ E₂ F
n : ℕ∞ω
hl : ContDiffAt 𝕜 n φ.leftFun φ.pt
hr : ContDiffAt 𝕜 n φ.rightFun φ.pt
pn : n ≠ 0
⊢ ContDiffAt 𝕜 (F := E₂ × F) n (fun (x : E₁) ↦ (φ.leftFun x, φ.rightFun x)) φ.pt

Tactic:
hl.prodMk hr

Premises used: ContDiffAt.prodMk
-- Module: Mathlib.Analysis.Calculus.ImplicitContDiff
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E₁ : Type u_2
inst_1 : NormedAddCommGroup E₁
inst_2 : NormedSpace 𝕜 E₁
inst_3 : CompleteSpace E₁
E₂ : Type u_3
inst_4 : NormedAddCommGroup E₂
inst_5 : NormedSpace 𝕜 E₂
inst_6 : CompleteSpace E₂
F : Type u_4
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace 𝕜 F
inst_9 : CompleteSpace F
φ : ImplicitFunctionData 𝕜 E₁ E₂ F
n : ℕ∞ω
hl : ContDiffAt 𝕜 n φ.leftFun φ.pt
hr : ContDiffAt 𝕜 n φ.rightFun φ.pt
pn : n ≠ 0
h : ∀ (x : E₁), (φ.prodFun x).1 = φ.leftFun x
h₁ : ∀ (x : E₁), (φ.prodFun x).2 = φ.rightFun x
⊢ ContDiffAt 𝕜 n φ.prodFun φ.pt

Tactic:
convert! hl.prodMk hr

Premises used: ContDiffAt.prodMk
-- Module: Mathlib.Analysis.Calculus.ImplicitContDiff
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E₁ : Type u_2
inst_1 : NormedAddCommGroup E₁
inst_2 : NormedSpace 𝕜 E₁
inst_3 : CompleteSpace E₁
E₂ : Type u_3
inst_4 : NormedAddCommGroup E₂
inst_5 : NormedSpace 𝕜 E₂
inst_6 : CompleteSpace E₂
F : Type u_4
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace 𝕜 F
inst_9 : CompleteSpace F
φ : ImplicitFunctionData 𝕜 E₁ E₂ F
n : ℕ∞ω
hl : ContDiffAt 𝕜 n φ.leftFun φ.pt
hr : ContDiffAt 𝕜 n φ.rightFun φ.pt
pn : n ≠ 0
x : E₁
⊢ (φ.prodFun x).1 = φ.leftFun x

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.ImplicitContDiff
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E₁ : Type u_2
inst_1 : NormedAddCommGroup E₁
inst_2 : NormedSpace 𝕜 E₁
inst_3 : CompleteSpace E₁
E₂ : Type u_3
inst_4 : NormedAddCommGroup E₂
inst_5 : NormedSpace 𝕜 E₂
inst_6 : CompleteSpace E₂
F : Type u_4
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace 𝕜 F
inst_9 : CompleteSpace F
φ : ImplicitFunctionData 𝕜 E₁ E₂ F
n : ℕ∞ω
hl : ContDiffAt 𝕜 n φ.leftFun φ.pt
hr : ContDiffAt 𝕜 n φ.rightFun φ.pt
pn : n ≠ 0
x : E₁
⊢ (φ.prodFun x).2 = φ.rightFun x

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.ImplicitContDiff
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E₁ : Type u_2
inst_1 : NormedAddCommGroup E₁
inst_2 : NormedSpace 𝕜 E₁
inst_3 : CompleteSpace E₁
E₂ : Type u_3
inst_4 : NormedAddCommGroup E₂
inst_5 : NormedSpace 𝕜 E₂
inst_6 : CompleteSpace E₂
F : Type u_4
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace 𝕜 F
inst_9 : CompleteSpace F
u : E₁ × E₂
f : E₁ × E₂ → F
n : ℕ∞ω
cdf : ContDiffAt 𝕜 n f u
pn : n ≠ 0
if₂ :
  ContinuousLinearMap.IsInvertible.{u_1, u_3, u_4} (M := E₂)
    (ContinuousLinearMap.comp (σ₁₂ := RingHom.id 𝕜) (fderiv 𝕜 f u) (ContinuousLinearMap.inr 𝕜 E₁ E₂))
⊢ cdf.implicitFunction pn if₂ = ⋯.implicitFunctionOfProdDomain if₂

Tactic:
rfl
-- Module: Mathlib.Analysis.Calculus.ImplicitContDiff
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E₁ : Type u_2
inst_1 : NormedAddCommGroup E₁
inst_2 : NormedSpace 𝕜 E₁
inst_3 : CompleteSpace E₁
E₂ : Type u_3
inst_4 : NormedAddCommGroup E₂
inst_5 : NormedSpace 𝕜 E₂
inst_6 : CompleteSpace E₂
F : Type u_4
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace 𝕜 F
inst_9 : CompleteSpace F
u : E₁ × E₂
f : E₁ × E₂ → F
n : ℕ∞ω
cdf : ContDiffAt 𝕜 n f u
pn : n ≠ 0
if₂ :
  ContinuousLinearMap.IsInvertible.{u_1, u_3, u_4} (M := E₂)
    (ContinuousLinearMap.comp (σ₁₂ := RingHom.id 𝕜) (fderiv 𝕜 f u) (ContinuousLinearMap.inr 𝕜 E₁ E₂))
⊢ cdf.implicitFunction pn if₂ u.1 = u.2

Tactic:
eq_of_tendsto_nhds ((cdf.hasStrictFDerivAt pn).tendsto_implicitFunctionOfProdDomain if₂)

Premises used: ContDiffAt.hasStrictFDerivAt, HasStrictFDerivAt.tendsto_implicitFunctionOfProdDomain, eq_of_tendsto_nhds
-- Module: Mathlib.Analysis.Calculus.ImplicitContDiff
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E₁ : Type u_2
inst_1 : NormedAddCommGroup E₁
inst_2 : NormedSpace 𝕜 E₁
inst_3 : CompleteSpace E₁
E₂ : Type u_3
inst_4 : NormedAddCommGroup E₂
inst_5 : NormedSpace 𝕜 E₂
inst_6 : CompleteSpace E₂
F : Type u_4
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace 𝕜 F
inst_9 : CompleteSpace F
u : E₁ × E₂
f : E₁ × E₂ → F
n : ℕ∞ω
cdf : ContDiffAt 𝕜 n f u
pn : n ≠ 0
if₂ :
  ContinuousLinearMap.IsInvertible.{u_1, u_3, u_4} (M := E₂)
    (ContinuousLinearMap.comp (σ₁₂ := RingHom.id 𝕜) (fderiv 𝕜 f u) (ContinuousLinearMap.inr 𝕜 E₁ E₂))
⊢ ∀ᶠ (x : E₁) in 𝓝 u.1, f (x, cdf.implicitFunction pn if₂ x) = f u

Tactic:
(cdf.hasStrictFDerivAt pn).eventually_apply_implicitFunctionOfProdDomain if₂

Premises used: ContDiffAt.hasStrictFDerivAt, HasStrictFDerivAt.eventually_apply_implicitFunctionOfProdDomain, ContDiffAt.implicitFunction
-- Module: Mathlib.Analysis.Calculus.ImplicitContDiff
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E₁ : Type u_2
inst_1 : NormedAddCommGroup E₁
inst_2 : NormedSpace 𝕜 E₁
inst_3 : CompleteSpace E₁
E₂ : Type u_3
inst_4 : NormedAddCommGroup E₂
inst_5 : NormedSpace 𝕜 E₂
inst_6 : CompleteSpace E₂
F : Type u_4
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace 𝕜 F
inst_9 : CompleteSpace F
u : E₁ × E₂
f : E₁ × E₂ → F
n : ℕ∞ω
cdf : ContDiffAt 𝕜 n f u
pn : n ≠ 0
if₂ :
  ContinuousLinearMap.IsInvertible.{u_1, u_3, u_4} (M := E₂)
    (ContinuousLinearMap.comp (σ₁₂ := RingHom.id 𝕜) (fderiv 𝕜 f u) (ContinuousLinearMap.inr 𝕜 E₁ E₂))
⊢ ∀ᶠ (v : E₁ × E₂) in 𝓝 u, f v = f u ↔ cdf.implicitFunction pn if₂ v.1 = v.2

Tactic:
(cdf.hasStrictFDerivAt pn).eventually_apply_eq_iff_implicitFunctionOfProdDomain if₂

Premises used: HasStrictFDerivAt.eventually_apply_eq_iff_implicitFunctionOfProdDomain, ContDiffAt.hasStrictFDerivAt, ContDiffAt.implicitFunction
-- Module: Mathlib.Analysis.Calculus.ImplicitContDiff
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E₁ : Type u_2
inst_1 : NormedAddCommGroup E₁
inst_2 : NormedSpace 𝕜 E₁
inst_3 : CompleteSpace E₁
E₂ : Type u_3
inst_4 : NormedAddCommGroup E₂
inst_5 : NormedSpace 𝕜 E₂
inst_6 : CompleteSpace E₂
F : Type u_4
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace 𝕜 F
inst_9 : CompleteSpace F
u : E₁ × E₂
f : E₁ × E₂ → F
n : ℕ∞ω
cdf : ContDiffAt 𝕜 n f u
pn : n ≠ 0
if₂ :
  ContinuousLinearMap.IsInvertible.{u_1, u_3, u_4} (M := E₂)
    (ContinuousLinearMap.comp (σ₁₂ := RingHom.id 𝕜) (fderiv 𝕜 f u) (ContinuousLinearMap.inr 𝕜 E₁ E₂))
⊢ HasStrictFDerivAt (cdf.implicitFunction pn if₂)
    (-ContinuousLinearMap.inverse
          (ContinuousLinearMap.comp (σ₁₂ := RingHom.id 𝕜) (fderiv 𝕜 f u) (ContinuousLinearMap.inr 𝕜 E₁ E₂)) ∘SL
        ContinuousLinearMap.comp (σ₁₂ := RingHom.id 𝕜) (fderiv 𝕜 f u) (ContinuousLinearMap.inl 𝕜 E₁ E₂))
    u.1

Tactic:
(cdf.hasStrictFDerivAt pn).hasStrictFDerivAt_implicitFunctionOfProdDomain if₂

Premises used: setOf, HasStrictFDerivAt.hasStrictFDerivAt_implicitFunctionOfProdDomain, ContDiffAt.hasStrictFDerivAt, ContDiffAt.implicitFunction
-- Module: Mathlib.Analysis.Calculus.ImplicitContDiff
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E₁ : Type u_2
inst_1 : NormedAddCommGroup E₁
inst_2 : NormedSpace 𝕜 E₁
inst_3 : CompleteSpace E₁
E₂ : Type u_3
inst_4 : NormedAddCommGroup E₂
inst_5 : NormedSpace 𝕜 E₂
inst_6 : CompleteSpace E₂
F : Type u_4
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace 𝕜 F
inst_9 : CompleteSpace F
u : E₁ × E₂
f : E₁ × E₂ → F
n : ℕ∞ω
cdf : ContDiffAt 𝕜 n f u
pn : n ≠ 0
if₂ :
  ContinuousLinearMap.IsInvertible.{u_1, u_3, u_4} (M := E₂)
    (ContinuousLinearMap.comp (σ₁₂ := RingHom.id 𝕜) (fderiv 𝕜 f u) (ContinuousLinearMap.inr 𝕜 E₁ E₂))
rw :
  ContDiffAt.{u_1, u_2, u_3} 𝕜 (F := E₂) n
    (fun (x : E₁) ↦
      (ImplicitFunctionData.implicitFunction
          (⋯.implicitFunctionDataOfProdDomain if₂ : ImplicitFunctionData 𝕜 (E₁ × E₂) F E₁) (f u) x).2)
    u.1
⊢ ContDiffAt 𝕜 n (cdf.implicitFunction pn if₂) u.1

Tactic:
rw [ContDiffAt.implicitFunction_def, HasStrictFDerivAt.implicitFunctionOfProdDomain_def]

Premises used: ContDiffAt.implicitFunction_def, HasStrictFDerivAt.implicitFunctionOfProdDomain_def
-- Module: Mathlib.Analysis.Calculus.ImplicitContDiff
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E₁ : Type u_2
inst_1 : NormedAddCommGroup E₁
inst_2 : NormedSpace 𝕜 E₁
inst_3 : CompleteSpace E₁
E₂ : Type u_3
inst_4 : NormedAddCommGroup E₂
inst_5 : NormedSpace 𝕜 E₂
inst_6 : CompleteSpace E₂
F : Type u_4
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace 𝕜 F
inst_9 : CompleteSpace F
u : E₁ × E₂
f : E₁ × E₂ → F
n : ℕ∞ω
cdf : ContDiffAt 𝕜 n f u
pn : n ≠ 0
if₂ :
  ContinuousLinearMap.IsInvertible.{u_1, u_3, u_4} (M := E₂)
    (ContinuousLinearMap.comp (σ₁₂ := RingHom.id 𝕜) (fderiv 𝕜 f u) (ContinuousLinearMap.inr 𝕜 E₁ E₂))
set :
  let φ : ImplicitFunctionData 𝕜 (E₁ × E₂) F E₁ := ⋯.implicitFunctionDataOfProdDomain if₂;
  ContDiffAt.{u_1, u_2, u_3} 𝕜 (F := E₂) n (fun (x : E₁) ↦ (φ.implicitFunction (f u) x).2) u.1
⊢ ContDiffAt.{u_1, u_2, u_3} 𝕜 (F := E₂) n
    (fun (x : E₁) ↦
      (ImplicitFunctionData.implicitFunction
          (⋯.implicitFunctionDataOfProdDomain if₂ : ImplicitFunctionData 𝕜 (E₁ × E₂) F E₁) (f u) x).2)
    u.1

Tactic:
set φ := (cdf.hasStrictFDerivAt pn).implicitFunctionDataOfProdDomain if₂

Premises used: ContDiffAt.hasStrictFDerivAt, HasStrictFDerivAt.implicitFunctionDataOfProdDomain
-- Module: Mathlib.Analysis.Calculus.ImplicitContDiff
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E₁ : Type u_2
inst_1 : NormedAddCommGroup E₁
inst_2 : NormedSpace 𝕜 E₁
inst_3 : CompleteSpace E₁
E₂ : Type u_3
inst_4 : NormedAddCommGroup E₂
inst_5 : NormedSpace 𝕜 E₂
inst_6 : CompleteSpace E₂
F : Type u_4
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace 𝕜 F
inst_9 : CompleteSpace F
u : E₁ × E₂
f : E₁ × E₂ → F
n : ℕ∞ω
cdf : ContDiffAt 𝕜 n f u
pn : n ≠ 0
if₂ :
  ContinuousLinearMap.IsInvertible.{u_1, u_3, u_4} (M := E₂)
    (ContinuousLinearMap.comp (σ₁₂ := RingHom.id 𝕜) (fderiv 𝕜 f u) (ContinuousLinearMap.inr 𝕜 E₁ E₂))
φ : ImplicitFunctionData 𝕜 (E₁ × E₂) F E₁ := ⋯.implicitFunctionDataOfProdDomain if₂
⊢ ContDiffAt 𝕜 n φ.leftFun φ.pt

Tactic:
simpa [φ] using cdf
-- Module: Mathlib.Analysis.Calculus.ImplicitContDiff
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E₁ : Type u_2
inst_1 : NormedAddCommGroup E₁
inst_2 : NormedSpace 𝕜 E₁
inst_3 : CompleteSpace E₁
E₂ : Type u_3
inst_4 : NormedAddCommGroup E₂
inst_5 : NormedSpace 𝕜 E₂
inst_6 : CompleteSpace E₂
F : Type u_4
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace 𝕜 F
inst_9 : CompleteSpace F
u : E₁ × E₂
f : E₁ × E₂ → F
n : ℕ∞ω
cdf : ContDiffAt 𝕜 n f u
pn : n ≠ 0
if₂ :
  ContinuousLinearMap.IsInvertible.{u_1, u_3, u_4} (M := E₂)
    (ContinuousLinearMap.comp (σ₁₂ := RingHom.id 𝕜) (fderiv 𝕜 f u) (ContinuousLinearMap.inr 𝕜 E₁ E₂))
φ : ImplicitFunctionData 𝕜 (E₁ × E₂) F E₁ := ⋯.implicitFunctionDataOfProdDomain if₂
⊢ ContDiffAt 𝕜 n φ.rightFun φ.pt

Tactic:
simpa [φ] using contDiffAt_fst

Premises used: contDiffAt_fst
-- Module: Mathlib.Analysis.Calculus.ImplicitContDiff
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E₁ : Type u_2
inst_1 : NormedAddCommGroup E₁
inst_2 : NormedSpace 𝕜 E₁
inst_3 : CompleteSpace E₁
E₂ : Type u_3
inst_4 : NormedAddCommGroup E₂
inst_5 : NormedSpace 𝕜 E₂
inst_6 : CompleteSpace E₂
F : Type u_4
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace 𝕜 F
inst_9 : CompleteSpace F
u : E₁ × E₂
f : E₁ × E₂ → F
n : ℕ∞ω
cdf : ContDiffAt 𝕜 n f u
pn : n ≠ 0
if₂ :
  ContinuousLinearMap.IsInvertible.{u_1, u_3, u_4} (M := E₂)
    (ContinuousLinearMap.comp (σ₁₂ := RingHom.id 𝕜) (fderiv 𝕜 f u) (ContinuousLinearMap.inr 𝕜 E₁ E₂))
φ : ImplicitFunctionData 𝕜 (E₁ × E₂) F E₁ := ⋯.implicitFunctionDataOfProdDomain if₂
⊢ ContDiffAt 𝕜 n (Function.uncurry φ.implicitFunction) (f u, u.1)

Tactic:
simpa [φ] using φ.contDiffAt_implicitFunction
      (by simpa [φ] using cdf) (by simpa [φ] using contDiffAt_fst) pn

Premises used: ImplicitFunctionData.contDiffAt_implicitFunction
-- Module: Mathlib.Analysis.Calculus.ImplicitContDiff
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E₁ : Type u_2
inst_1 : NormedAddCommGroup E₁
inst_2 : NormedSpace 𝕜 E₁
inst_3 : CompleteSpace E₁
E₂ : Type u_3
inst_4 : NormedAddCommGroup E₂
inst_5 : NormedSpace 𝕜 E₂
inst_6 : CompleteSpace E₂
F : Type u_4
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace 𝕜 F
inst_9 : CompleteSpace F
u : E₁ × E₂
f : E₁ × E₂ → F
n : ℕ∞ω
cdf : ContDiffAt 𝕜 n f u
pn : n ≠ 0
if₂ :
  ContinuousLinearMap.IsInvertible.{u_1, u_3, u_4} (M := E₂)
    (ContinuousLinearMap.comp (σ₁₂ := RingHom.id 𝕜) (fderiv 𝕜 f u) (ContinuousLinearMap.inr 𝕜 E₁ E₂))
φ : ImplicitFunctionData 𝕜 (E₁ × E₂) F E₁ := ⋯.implicitFunctionDataOfProdDomain if₂
⊢ ContDiffAt 𝕜 n (Function.uncurry φ.implicitFunction) (f u, u.1)

Tactic:
have : ContDiffAt 𝕜 n φ.implicitFunction.uncurry (f u, u.1) := by
    simpa [φ] using φ.contDiffAt_implicitFunction
      (by simpa [φ] using cdf) (by simpa [φ] using contDiffAt_fst) pn
-- Module: Mathlib.Analysis.Calculus.ImplicitContDiff
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E₁ : Type u_2
inst_1 : NormedAddCommGroup E₁
inst_2 : NormedSpace 𝕜 E₁
inst_3 : CompleteSpace E₁
E₂ : Type u_3
inst_4 : NormedAddCommGroup E₂
inst_5 : NormedSpace 𝕜 E₂
inst_6 : CompleteSpace E₂
F : Type u_4
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace 𝕜 F
inst_9 : CompleteSpace F
u : E₁ × E₂
f : E₁ × E₂ → F
n : ℕ∞ω
cdf : ContDiffAt 𝕜 n f u
pn : n ≠ 0
if₂ :
  ContinuousLinearMap.IsInvertible.{u_1, u_3, u_4} (M := E₂)
    (ContinuousLinearMap.comp (σ₁₂ := RingHom.id 𝕜) (fderiv 𝕜 f u) (ContinuousLinearMap.inr 𝕜 E₁ E₂))
φ : ImplicitFunctionData 𝕜 (E₁ × E₂) F E₁ := ⋯.implicitFunctionDataOfProdDomain if₂
this : ContDiffAt 𝕜 n (Function.uncurry φ.implicitFunction) (f u, u.1)
⊢ ContDiffAt.{u_1, u_2, u_3} 𝕜 (F := E₂) n (fun (x : E₁) ↦ (φ.implicitFunction (f u) x).2) u.1

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Calculus.ImplicitFunction.Bivariate
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : IsRCLikeNormedField 𝕜
E₁ : Type u_2
inst_2 : NormedAddCommGroup E₁
inst_3 : NormedSpace 𝕜 E₁
inst_4 : CompleteSpace E₁
E₂ : Type u_3
inst_5 : NormedAddCommGroup E₂
inst_6 : NormedSpace 𝕜 E₂
inst_7 : CompleteSpace E₂
F : Type u_4
inst_8 : NormedAddCommGroup F
inst_9 : NormedSpace 𝕜 F
inst_10 : CompleteSpace F
u : E₁ × E₂
f : E₁ → E₂ → F
f₁ : E₁ → E₂ → E₁ →L[𝕜] F
f₂ : E₁ → E₂ → E₂ →L[𝕜] F
df₁ : ∀ᶠ (v : E₁ × E₂) in 𝓝 u, HasFDerivAt (fun (x : E₁) ↦ f x v.2) (f₁ v.1 v.2) v.1
df₂ : ∀ᶠ (v : E₁ × E₂) in 𝓝 u, HasFDerivAt (fun (x : E₂) ↦ f v.1 x) (f₂ v.1 v.2) v.2
cf₁ : ContinuousAt (↿f₁) u
cf₂ : ContinuousAt (↿f₂) u
if₂u : (f₂ u.1 u.2).IsInvertible
⊢ ((↿f₁ u).coprod (↿f₂ u) ∘SL ContinuousLinearMap.inr 𝕜 E₁ E₂).IsInvertible

Tactic:
simpa using if₂u
-- Module: Mathlib.Analysis.Calculus.ImplicitFunction.Bivariate
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : IsRCLikeNormedField 𝕜
E₁ : Type u_2
inst_2 : NormedAddCommGroup E₁
inst_3 : NormedSpace 𝕜 E₁
inst_4 : CompleteSpace E₁
E₂ : Type u_3
inst_5 : NormedAddCommGroup E₂
inst_6 : NormedSpace 𝕜 E₂
inst_7 : CompleteSpace E₂
F : Type u_4
inst_8 : NormedAddCommGroup F
inst_9 : NormedSpace 𝕜 F
inst_10 : CompleteSpace F
u : E₁ × E₂
f : E₁ → E₂ → F
f₁ : E₁ → E₂ → E₁ →L[𝕜] F
f₂ : E₁ → E₂ → E₂ →L[𝕜] F
df₁ : ∀ᶠ (v : E₁ × E₂) in 𝓝 u, HasFDerivAt (fun (x : E₁) ↦ f x v.2) (f₁ v.1 v.2) v.1
df₂ : ∀ᶠ (v : E₁ × E₂) in 𝓝 u, HasFDerivAt (fun (x : E₂) ↦ f v.1 x) (f₂ v.1 v.2) v.2
cf₁ : ContinuousAt (↿f₁) u
cf₂ : ContinuousAt (↿f₂) u
if₂u : (f₂ u.1 u.2).IsInvertible
⊢ implicitFunctionOfBivariate df₁ df₂ cf₁ cf₂ if₂u = ⋯.implicitFunctionOfProdDomain ⋯

Tactic:
rfl
-- Module: Mathlib.Analysis.Calculus.ImplicitFunction.Bivariate
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : IsRCLikeNormedField 𝕜
E₁ : Type u_2
inst_2 : NormedAddCommGroup E₁
inst_3 : NormedSpace 𝕜 E₁
inst_4 : CompleteSpace E₁
E₂ : Type u_3
inst_5 : NormedAddCommGroup E₂
inst_6 : NormedSpace 𝕜 E₂
inst_7 : CompleteSpace E₂
F : Type u_4
inst_8 : NormedAddCommGroup F
inst_9 : NormedSpace 𝕜 F
inst_10 : CompleteSpace F
u : E₁ × E₂
f : E₁ → E₂ → F
f₁ : E₁ → E₂ → E₁ →L[𝕜] F
f₂ : E₁ → E₂ → E₂ →L[𝕜] F
df₁ : ∀ᶠ (v : E₁ × E₂) in 𝓝 u, HasFDerivAt (fun (x : E₁) ↦ f x v.2) (f₁ v.1 v.2) v.1
df₂ : ∀ᶠ (v : E₁ × E₂) in 𝓝 u, HasFDerivAt (fun (x : E₂) ↦ f v.1 x) (f₂ v.1 v.2) v.2
cf₁ : ContinuousAt (↿f₁) u
cf₂ : ContinuousAt (↿f₂) u
if₂u : (f₂ u.1 u.2).IsInvertible
⊢ Tendsto (implicitFunctionOfBivariate df₁ df₂ cf₁ cf₂ if₂u) (𝓝 u.1) (𝓝 u.2)

Tactic:
simpa using HasStrictFDerivAt.tendsto_implicitFunctionOfProdDomain
    (hasStrictFDerivAt_uncurry_coprod df₁ df₂ cf₁ cf₂) (by simpa using if₂u)

Premises used: hasStrictFDerivAt_uncurry_coprod, HasStrictFDerivAt.tendsto_implicitFunctionOfProdDomain
-- Module: Mathlib.Analysis.Calculus.ImplicitFunction.Bivariate
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : IsRCLikeNormedField 𝕜
E₁ : Type u_2
inst_2 : NormedAddCommGroup E₁
inst_3 : NormedSpace 𝕜 E₁
inst_4 : CompleteSpace E₁
E₂ : Type u_3
inst_5 : NormedAddCommGroup E₂
inst_6 : NormedSpace 𝕜 E₂
inst_7 : CompleteSpace E₂
F : Type u_4
inst_8 : NormedAddCommGroup F
inst_9 : NormedSpace 𝕜 F
inst_10 : CompleteSpace F
u : E₁ × E₂
f : E₁ → E₂ → F
f₁ : E₁ → E₂ → E₁ →L[𝕜] F
f₂ : E₁ → E₂ → E₂ →L[𝕜] F
df₁ : ∀ᶠ (v : E₁ × E₂) in 𝓝 u, HasFDerivAt (fun (x : E₁) ↦ f x v.2) (f₁ v.1 v.2) v.1
df₂ : ∀ᶠ (v : E₁ × E₂) in 𝓝 u, HasFDerivAt (fun (x : E₂) ↦ f v.1 x) (f₂ v.1 v.2) v.2
cf₁ : ContinuousAt (↿f₁) u
cf₂ : ContinuousAt (↿f₂) u
if₂u : (f₂ u.1 u.2).IsInvertible
⊢ ∀ᶠ (x : E₁) in 𝓝 u.1, f x (implicitFunctionOfBivariate df₁ df₂ cf₁ cf₂ if₂u x) = f u.1 u.2

Tactic:
simpa using HasStrictFDerivAt.eventually_apply_implicitFunctionOfProdDomain
    (hasStrictFDerivAt_uncurry_coprod df₁ df₂ cf₁ cf₂) (by simpa using if₂u)

Premises used: hasStrictFDerivAt_uncurry_coprod, HasStrictFDerivAt.eventually_apply_implicitFunctionOfProdDomain