awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ ∀ᶠ (v : E₁ × E₂) in 𝓝 u, f v.1 v.2 = f u.1 u.2 ↔ implicitFunctionOfBivariate df₁ df₂ cf₁ cf₂ if₂u v.1 = v.2

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

Premises used: hasStrictFDerivAt_uncurry_coprod, HasStrictFDerivAt.eventually_apply_eq_iff_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
⊢ HasStrictFDerivAt (implicitFunctionOfBivariate df₁ df₂ cf₁ cf₂ if₂u) (-(f₂ u.1 u.2).inverse ∘SL f₁ u.1 u.2) u.1

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

Premises used: hasStrictFDerivAt_uncurry_coprod, HasStrictFDerivAt.hasStrictFDerivAt_implicitFunctionOfProdDomain
-- Module: Mathlib.Analysis.Calculus.ImplicitFunction.ProdDomain
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
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
f'u : E₁ × E₂ →L[𝕜] F
dfu : HasStrictFDerivAt (𝕜 := 𝕜) f f'u u
if₂u : (f'u ∘SL ContinuousLinearMap.inr 𝕜 E₁ E₂).IsInvertible
⊢ (↑(f'u ∘SL ContinuousLinearMap.inr 𝕜 E₁ E₂) : E₂ →ₗ[𝕜] F).range ≤ (↑f'u : E₁ × E₂ →ₗ[𝕜] F).range

Tactic:
have : (f'u ∘L .inr 𝕜 E₁ E₂).range ≤ f'u.range := LinearMap.range_comp_le_range ..
-- Module: Mathlib.Analysis.Calculus.ImplicitFunction.ProdDomain
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
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
f'u : E₁ × E₂ →L[𝕜] F
dfu : HasStrictFDerivAt (𝕜 := 𝕜) f f'u u
if₂u : (f'u ∘SL ContinuousLinearMap.inr 𝕜 E₁ E₂).IsInvertible
this : (↑(f'u ∘SL ContinuousLinearMap.inr 𝕜 E₁ E₂) : E₂ →ₗ[𝕜] F).range ≤ (↑f'u : E₁ × E₂ →ₗ[𝕜] F).range
rwa : ∀ (this : ⊤ ≤ (↑f'u : E₁ × E₂ →ₗ[𝕜] F).range), (↑f'u : E₁ × E₂ →ₗ[𝕜] F).range = ⊤
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (this : (↑f'u : E₁ × E₂ →ₗ[𝕜] F).range = ⊤), (↑f'u : E₁ × E₂ →ₗ[𝕜] F).range = ⊤
⊢ (↑f'u : E₁ × E₂ →ₗ[𝕜] F).range = ⊤

Tactic:
rwa [LinearMap.range_eq_top.mpr if₂u.surjective, top_le_iff] at this

Premises used: Iff.mpr, ContinuousLinearMap.IsInvertible.surjective, LinearMap.range_eq_top, top_le_iff
-- Module: Mathlib.Analysis.Calculus.ImplicitFunction.ProdDomain
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
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
f'u : E₁ × E₂ →L[𝕜] F
dfu : HasStrictFDerivAt (𝕜 := 𝕜) f f'u u
if₂u : (f'u ∘SL ContinuousLinearMap.inr 𝕜 E₁ E₂).IsInvertible
disjoint :
  Disjoint (↑f'u : E₁ × E₂ →ₗ[𝕜] F).ker
    (LinearMap.ker (R₂ := 𝕜) (M₂ := E₁) (τ₁₂ := RingHom.id 𝕜) (↑(ContinuousLinearMap.fst 𝕜 E₁ E₂) : E₁ × E₂ →ₗ[𝕜] E₁))
codisjoint :
  Codisjoint (↑f'u : E₁ × E₂ →ₗ[𝕜] F).ker
    (LinearMap.ker (R₂ := 𝕜) (M₂ := E₁) (τ₁₂ := RingHom.id 𝕜) (↑(ContinuousLinearMap.fst 𝕜 E₁ E₂) : E₁ × E₂ →ₗ[𝕜] E₁))
⊢ IsCompl (↑f'u : E₁ × E₂ →ₗ[𝕜] F).ker
    (LinearMap.ker (R₂ := 𝕜) (M₂ := E₁) (τ₁₂ := RingHom.id 𝕜) (↑(ContinuousLinearMap.fst 𝕜 E₁ E₂) : E₁ × E₂ →ₗ[𝕜] E₁))

Tactic:
constructor
-- Module: Mathlib.Analysis.Calculus.ImplicitFunction.ProdDomain
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
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
f'u : E₁ × E₂ →L[𝕜] F
dfu : HasStrictFDerivAt (𝕜 := 𝕜) f f'u u
if₂u : (f'u ∘SL ContinuousLinearMap.inr 𝕜 E₁ E₂).IsInvertible
disjoint :
  ∀ x ∈ (↑f'u : E₁ × E₂ →ₗ[𝕜] F).ker,
    Eq.{u_2 + 1} (α := E₁)
        ((((↑(ContinuousLinearMap.fst 𝕜 E₁ E₂) : E₁ × E₂ →ₗ[𝕜] E₁) : E₁ × E₂ →ₗ[𝕜] E₁) : (a : E₁ × E₂) → E₁) x : E₁)
        (0 : E₁) →
      x = 0
⊢ Disjoint (↑f'u : E₁ × E₂ →ₗ[𝕜] F).ker
    (LinearMap.ker (R₂ := 𝕜) (M₂ := E₁) (τ₁₂ := RingHom.id 𝕜) (↑(ContinuousLinearMap.fst 𝕜 E₁ E₂) : E₁ × E₂ →ₗ[𝕜] E₁))

Tactic:
rw [LinearMap.disjoint_ker]

Premises used: LinearMap.disjoint_ker
-- Module: Mathlib.Analysis.Calculus.ImplicitFunction.ProdDomain
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
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
f'u : E₁ × E₂ →L[𝕜] F
dfu : HasStrictFDerivAt (𝕜 := 𝕜) f f'u u
if₂u : (f'u ∘SL ContinuousLinearMap.inr 𝕜 E₁ E₂).IsInvertible
y : E₂
h : (0, y) ∈ (↑f'u : E₁ × E₂ →ₗ[𝕜] F).ker
⊢ Eq (α := E₁ × E₂) (0, y) 0

Tactic:
simpa using (injective_iff_map_eq_zero _).mp if₂u.injective y h

Premises used: injective_iff_map_eq_zero, Iff.mp, ContinuousLinearMap.IsInvertible.injective
-- Module: Mathlib.Analysis.Calculus.ImplicitFunction.ProdDomain
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
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
f'u : E₁ × E₂ →L[𝕜] F
dfu : HasStrictFDerivAt (𝕜 := 𝕜) f f'u u
if₂u : (f'u ∘SL ContinuousLinearMap.inr 𝕜 E₁ E₂).IsInvertible
codisjoint :
  ∀ (z : E₁ × E₂),
    ∃ (x : E₁ × E₂) (y : E₁ × E₂),
      x ∈ (↑f'u : E₁ × E₂ →ₗ[𝕜] F).ker ∧
        Membership.mem (γ := Submodule 𝕜 (E₁ × E₂))
            (LinearMap.ker (R₂ := 𝕜) (M₂ := E₁) (τ₁₂ := RingHom.id 𝕜)
                (↑(ContinuousLinearMap.fst 𝕜 E₁ E₂) : E₁ × E₂ →ₗ[𝕜] E₁) :
              Submodule 𝕜 (E₁ × E₂))
            y ∧
          x + y = z
⊢ Codisjoint (↑f'u : E₁ × E₂ →ₗ[𝕜] F).ker
    (LinearMap.ker (R₂ := 𝕜) (M₂ := E₁) (τ₁₂ := RingHom.id 𝕜) (↑(ContinuousLinearMap.fst 𝕜 E₁ E₂) : E₁ × E₂ →ₗ[𝕜] E₁))

Tactic:
rw [Submodule.codisjoint_iff_exists_add_eq]

Premises used: Submodule.codisjoint_iff_exists_add_eq
-- Module: Mathlib.Analysis.Calculus.ImplicitFunction.ProdDomain
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
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
f'u : E₁ × E₂ →L[𝕜] F
dfu : HasStrictFDerivAt (𝕜 := 𝕜) f f'u u
if₂u : (f'u ∘SL ContinuousLinearMap.inr 𝕜 E₁ E₂).IsInvertible
v : E₁ × E₂
codisjoint :
  ∀ (y : E₂)
    (hy :
      Eq.{u_4 + 1} (α := F) ((f'u ∘SL ContinuousLinearMap.inr 𝕜 E₁ E₂ : (a : E₂) → F) y : F)
        ((f'u : (a : E₁ × E₂) → F) v : F)),
    ∃ (x : E₁ × E₂) (y : E₁ × E₂),
      x ∈ (↑f'u : E₁ × E₂ →ₗ[𝕜] F).ker ∧
        Membership.mem (γ := Submodule 𝕜 (E₁ × E₂))
            (LinearMap.ker (R₂ := 𝕜) (M₂ := E₁) (τ₁₂ := RingHom.id 𝕜)
                (↑(ContinuousLinearMap.fst 𝕜 E₁ E₂) : E₁ × E₂ →ₗ[𝕜] E₁) :
              Submodule 𝕜 (E₁ × E₂))
            y ∧
          x + y = v
⊢ ∃ (x : E₁ × E₂) (y : E₁ × E₂),
    x ∈ (↑f'u : E₁ × E₂ →ₗ[𝕜] F).ker ∧
      Membership.mem (γ := Submodule 𝕜 (E₁ × E₂))
          (LinearMap.ker (R₂ := 𝕜) (M₂ := E₁) (τ₁₂ := RingHom.id 𝕜)
              (↑(ContinuousLinearMap.fst 𝕜 E₁ E₂) : E₁ × E₂ →ₗ[𝕜] E₁) :
            Submodule 𝕜 (E₁ × E₂))
          y ∧
        x + y = v

Tactic:
have ⟨y, hy⟩ := if₂u.surjective (f'u v)
-- Module: Mathlib.Analysis.Calculus.ImplicitFunction.ProdDomain
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
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
f'u : E₁ × E₂ →L[𝕜] F
dfu : HasStrictFDerivAt (𝕜 := 𝕜) f f'u u
if₂u : (f'u ∘SL ContinuousLinearMap.inr 𝕜 E₁ E₂).IsInvertible
v : E₁ × E₂
y : E₂
hy :
  Eq.{u_4 + 1} (α := F) ((f'u ∘SL ContinuousLinearMap.inr 𝕜 E₁ E₂ : (a : E₂) → F) y : F)
    ((f'u : (a : E₁ × E₂) → F) v : F)
h :
  v - (0, y) ∈ (↑f'u : E₁ × E₂ →ₗ[𝕜] F).ker ∧
    Membership.mem (γ := Submodule 𝕜 (E₁ × E₂))
        (LinearMap.ker (R₂ := 𝕜) (M₂ := E₁) (τ₁₂ := RingHom.id 𝕜)
            (↑(ContinuousLinearMap.fst 𝕜 E₁ E₂) : E₁ × E₂ →ₗ[𝕜] E₁) :
          Submodule 𝕜 (E₁ × E₂))
        (0, y) ∧
      v - (0, y) + (0, y) = v
⊢ ∃ (x : E₁ × E₂) (y : E₁ × E₂),
    x ∈ (↑f'u : E₁ × E₂ →ₗ[𝕜] F).ker ∧
      Membership.mem (γ := Submodule 𝕜 (E₁ × E₂))
          (LinearMap.ker (R₂ := 𝕜) (M₂ := E₁) (τ₁₂ := RingHom.id 𝕜)
              (↑(ContinuousLinearMap.fst 𝕜 E₁ E₂) : E₁ × E₂ →ₗ[𝕜] E₁) :
            Submodule 𝕜 (E₁ × E₂))
          y ∧
        x + y = v

Tactic:
use v - (0, y), (0, y)

Premises used: Prod.mk, OfNat.ofNat
-- Module: Mathlib.Analysis.Calculus.ImplicitFunction.ProdDomain
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
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
f'u : E₁ × E₂ →L[𝕜] F
dfu : HasStrictFDerivAt (𝕜 := 𝕜) f f'u u
if₂u : (f'u ∘SL ContinuousLinearMap.inr 𝕜 E₁ E₂).IsInvertible
v : E₁ × E₂
y : E₂
hy :
  Eq.{u_4 + 1} (α := F) ((f'u ∘SL ContinuousLinearMap.inr 𝕜 E₁ E₂ : (a : E₂) → F) y : F)
    ((f'u : (a : E₁ × E₂) → F) v : F)
⊢ v - (0, y) ∈ (↑f'u : E₁ × E₂ →ₗ[𝕜] F).ker ∧
    Membership.mem (γ := Submodule 𝕜 (E₁ × E₂))
        (LinearMap.ker (R₂ := 𝕜) (M₂ := E₁) (τ₁₂ := RingHom.id 𝕜)
            (↑(ContinuousLinearMap.fst 𝕜 E₁ E₂) : E₁ × E₂ →ₗ[𝕜] E₁) :
          Submodule 𝕜 (E₁ × E₂))
        (0, y) ∧
      v - (0, y) + (0, y) = v

Tactic:
aesop
-- Module: Mathlib.Analysis.Calculus.ImplicitFunction.ProdDomain
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
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
f'u : E₁ × E₂ →L[𝕜] F
dfu : HasStrictFDerivAt (𝕜 := 𝕜) f f'u u
if₂u : (f'u ∘SL ContinuousLinearMap.inr 𝕜 E₁ E₂).IsInvertible
⊢ ImplicitFunctionData.pt (dfu.implicitFunctionDataOfProdDomain if₂u : ImplicitFunctionData 𝕜 (E₁ × E₂) F E₁) = u

Tactic:
rfl
-- Module: Mathlib.Analysis.Calculus.ImplicitFunction.ProdDomain
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
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
f'u : E₁ × E₂ →L[𝕜] F
dfu : HasStrictFDerivAt (𝕜 := 𝕜) f f'u u
if₂u : (f'u ∘SL ContinuousLinearMap.inr 𝕜 E₁ E₂).IsInvertible
⊢ ImplicitFunctionData.leftFun (dfu.implicitFunctionDataOfProdDomain if₂u : ImplicitFunctionData 𝕜 (E₁ × E₂) F E₁) = f

Tactic:
rfl
-- Module: Mathlib.Analysis.Calculus.ImplicitFunction.ProdDomain
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
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
f'u : E₁ × E₂ →L[𝕜] F
dfu : HasStrictFDerivAt (𝕜 := 𝕜) f f'u u
if₂u : (f'u ∘SL ContinuousLinearMap.inr 𝕜 E₁ E₂).IsInvertible
⊢ ImplicitFunctionData.rightFun (dfu.implicitFunctionDataOfProdDomain if₂u : ImplicitFunctionData 𝕜 (E₁ × E₂) F E₁) =
    Prod.fst

Tactic:
rfl
-- Module: Mathlib.Analysis.Calculus.ImplicitFunction.ProdDomain
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
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
f'u : E₁ × E₂ →L[𝕜] F
dfu : HasStrictFDerivAt (𝕜 := 𝕜) f f'u u
if₂u : (f'u ∘SL ContinuousLinearMap.inr 𝕜 E₁ E₂).IsInvertible
⊢ dfu.implicitFunctionOfProdDomain if₂u = fun (x : E₁) ↦
    (ImplicitFunctionData.implicitFunction
        (dfu.implicitFunctionDataOfProdDomain if₂u : ImplicitFunctionData 𝕜 (E₁ × E₂) F E₁) (f u) x).2

Tactic:
rfl
-- Module: Mathlib.Analysis.Calculus.ImplicitFunction.ProdDomain
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
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
f'u : E₁ × E₂ →L[𝕜] F
dfu : HasStrictFDerivAt (𝕜 := 𝕜) f f'u u
if₂u : (f'u ∘SL ContinuousLinearMap.inr 𝕜 E₁ E₂).IsInvertible
φ : ImplicitFunctionData 𝕜 (E₁ × E₂) F E₁ := dfu.implicitFunctionDataOfProdDomain if₂u
h :
  ∀ (a : E₁ × E₂),
    (φ.leftFun a = φ.leftFun φ.pt ↔ φ.implicitFunction (φ.leftFun φ.pt) (φ.rightFun a) = a) →
      φ.rightFun (φ.implicitFunction (φ.leftFun φ.pt) (φ.rightFun a)) = φ.rightFun a →
        (f a = f u ↔ dfu.implicitFunctionOfProdDomain if₂u a.1 = a.2)
⊢ ∀ᶠ (v : E₁ × E₂) in 𝓝 u, f v = f u ↔ dfu.implicitFunctionOfProdDomain if₂u v.1 = v.2

Tactic:
filter_upwards [φ.leftFun_eq_iff_implicitFunction, φ.rightFun_implicitFunction_eq_rightFun]

Premises used: ImplicitFunctionData.rightFun_implicitFunction_eq_rightFun, ImplicitFunctionData.leftFun_eq_iff_implicitFunction
-- Module: Mathlib.Analysis.Calculus.ImplicitFunction.ProdDomain
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
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
f'u : E₁ × E₂ →L[𝕜] F
dfu : HasStrictFDerivAt (𝕜 := 𝕜) f f'u u
if₂u : (f'u ∘SL ContinuousLinearMap.inr 𝕜 E₁ E₂).IsInvertible
φ : ImplicitFunctionData 𝕜 (E₁ × E₂) F E₁ := dfu.implicitFunctionDataOfProdDomain if₂u
v : E₁ × E₂
h : φ.leftFun v = φ.leftFun φ.pt ↔ φ.implicitFunction (φ.leftFun φ.pt) (φ.rightFun v) = v
h_1 : φ.rightFun (φ.implicitFunction (φ.leftFun φ.pt) (φ.rightFun v)) = φ.rightFun v
⊢ dfu.implicitFunctionOfProdDomain if₂u v.1 = v.2 → φ.implicitFunction (φ.leftFun φ.pt) (φ.rightFun v) = v

Tactic:
aesop
-- Module: Mathlib.Analysis.Calculus.ImplicitFunction.ProdDomain
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
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
f'u : E₁ × E₂ →L[𝕜] F
dfu : HasStrictFDerivAt (𝕜 := 𝕜) f f'u u
if₂u : (f'u ∘SL ContinuousLinearMap.inr 𝕜 E₁ E₂).IsInvertible
φ : ImplicitFunctionData 𝕜 (E₁ × E₂) F E₁ := dfu.implicitFunctionDataOfProdDomain if₂u
⊢ ∀ (a : E₁ × E₂),
    (φ.leftFun a = φ.leftFun φ.pt ↔ φ.implicitFunction (φ.leftFun φ.pt) (φ.rightFun a) = a) →
      φ.rightFun (φ.implicitFunction (φ.leftFun φ.pt) (φ.rightFun a)) = φ.rightFun a →
        (f a = f u ↔ dfu.implicitFunctionOfProdDomain if₂u a.1 = a.2)

Tactic:
exact fun v h _ => Iff.trans h ⟨congrArg _, by aesop⟩

Premises used: congrArg, Iff.intro, Iff.trans
-- Module: Mathlib.Analysis.Calculus.ImplicitFunction.ProdDomain
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
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
f'u : E₁ × E₂ →L[𝕜] F
dfu : HasStrictFDerivAt (𝕜 := 𝕜) f f'u u
if₂u : (f'u ∘SL ContinuousLinearMap.inr 𝕜 E₁ E₂).IsInvertible
suffices :
  f'u ∘SL
      ContinuousLinearMap.prod (ContinuousLinearMap.id 𝕜 E₁)
        (-(f'u ∘SL ContinuousLinearMap.inr 𝕜 E₁ E₂).inverse ∘SL f'u ∘SL ContinuousLinearMap.inl 𝕜 E₁ E₂) =
    0
⊢ HasStrictFDerivAt (dfu.implicitFunctionOfProdDomain if₂u)
    (-(f'u ∘SL ContinuousLinearMap.inr 𝕜 E₁ E₂).inverse ∘SL f'u ∘SL ContinuousLinearMap.inl 𝕜 E₁ E₂) u.1

Tactic:
suffices f'u ∘L (.prod (.id ..) (-(f'u ∘L .inr ..).inverse ∘L (f'u ∘L .inl ..))) = 0 from
    ((dfu.implicitFunctionDataOfProdDomain if₂u).hasStrictFDerivAt_implicitFunction _
      (ContinuousLinearMap.fst_comp_prod _ _) this).snd
-- Module: Mathlib.Analysis.Calculus.ImplicitFunction.ProdDomain
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
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
f'u : E₁ × E₂ →L[𝕜] F
dfu : HasStrictFDerivAt (𝕜 := 𝕜) f f'u u
if₂u : (f'u ∘SL ContinuousLinearMap.inr 𝕜 E₁ E₂).IsInvertible
h :
  ∀ (x : E₁),
    Eq.{u_4 + 1} (α := F)
      ((f'u ∘SL
              ContinuousLinearMap.prod (ContinuousLinearMap.id 𝕜 E₁)
                (-(f'u ∘SL ContinuousLinearMap.inr 𝕜 E₁ E₂).inverse ∘SL f'u ∘SL ContinuousLinearMap.inl 𝕜 E₁ E₂) :
            (a : E₁) → F)
          x :
        F)
      ((0 : (a : E₁) → F) x : F)
⊢ f'u ∘SL
      ContinuousLinearMap.prod (ContinuousLinearMap.id 𝕜 E₁)
        (-(f'u ∘SL ContinuousLinearMap.inr 𝕜 E₁ E₂).inverse ∘SL f'u ∘SL ContinuousLinearMap.inl 𝕜 E₁ E₂) =
    0

Tactic:
ext
-- Module: Mathlib.Analysis.Calculus.ImplicitFunction.ProdDomain
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
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
f'u : E₁ × E₂ →L[𝕜] F
dfu : HasStrictFDerivAt (𝕜 := 𝕜) f f'u u
if₂u : (f'u ∘SL ContinuousLinearMap.inr 𝕜 E₁ E₂).IsInvertible
x : E₁
h :
  HAdd.hAdd (α := F) (β := F)
      ((f'u ∘SL ContinuousLinearMap.inl 𝕜 E₁ E₂ : (a : E₁) → F)
          ((ContinuousLinearMap.prod (ContinuousLinearMap.id 𝕜 E₁)
                  (-(f'u ∘SL ContinuousLinearMap.inr 𝕜 E₁ E₂).inverse ∘SL f'u ∘SL ContinuousLinearMap.inl 𝕜 E₁ E₂) :
                (a : E₁) → E₁ × E₂)
              x).1 :
        F)
      ((f'u ∘SL ContinuousLinearMap.inr 𝕜 E₁ E₂ : (a : E₂) → F)
          ((ContinuousLinearMap.prod (ContinuousLinearMap.id 𝕜 E₁)
                  (-(f'u ∘SL ContinuousLinearMap.inr 𝕜 E₁ E₂).inverse ∘SL f'u ∘SL ContinuousLinearMap.inl 𝕜 E₁ E₂) :
                (a : E₁) → E₁ × E₂)
              x).2 :
        F) =
    (0 : (a : E₁) → F) x
⊢ Eq.{u_4 + 1} (α := F)
    ((f'u ∘SL
            ContinuousLinearMap.prod (ContinuousLinearMap.id 𝕜 E₁)
              (-(f'u ∘SL ContinuousLinearMap.inr 𝕜 E₁ E₂).inverse ∘SL f'u ∘SL ContinuousLinearMap.inl 𝕜 E₁ E₂) :
          (a : E₁) → F)
        x :
      F)
    ((0 : (a : E₁) → F) x : F)

Tactic:
rw [f'u.comp_apply, ← f'u.comp_inl_add_comp_inr]

Premises used: ContinuousLinearMap.comp_inl_add_comp_inr, ContinuousLinearMap.comp_apply
-- Module: Mathlib.Analysis.Calculus.ImplicitFunction.ProdDomain
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
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
f'u : E₁ × E₂ →L[𝕜] F
dfu : HasStrictFDerivAt (𝕜 := 𝕜) f f'u u
if₂u : (f'u ∘SL ContinuousLinearMap.inr 𝕜 E₁ E₂).IsInvertible
x : E₁
⊢ HAdd.hAdd (α := F) (β := F)
      ((f'u ∘SL ContinuousLinearMap.inl 𝕜 E₁ E₂ : (a : E₁) → F)
          ((ContinuousLinearMap.prod (ContinuousLinearMap.id 𝕜 E₁)
                  (-(f'u ∘SL ContinuousLinearMap.inr 𝕜 E₁ E₂).inverse ∘SL f'u ∘SL ContinuousLinearMap.inl 𝕜 E₁ E₂) :
                (a : E₁) → E₁ × E₂)
              x).1 :
        F)
      ((f'u ∘SL ContinuousLinearMap.inr 𝕜 E₁ E₂ : (a : E₂) → F)
          ((ContinuousLinearMap.prod (ContinuousLinearMap.id 𝕜 E₁)
                  (-(f'u ∘SL ContinuousLinearMap.inr 𝕜 E₁ E₂).inverse ∘SL f'u ∘SL ContinuousLinearMap.inl 𝕜 E₁ E₂) :
                (a : E₁) → E₁ × E₂)
              x).2 :
        F) =
    (0 : (a : E₁) → F) x

Tactic:
simp [map_neg, if₂u]

Premises used: map_neg
-- Module: Mathlib.Analysis.Calculus.ImplicitFunction.ProdDomain
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
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
f'u : E₁ × E₂ →L[𝕜] F
dfu : HasStrictFDerivAt (𝕜 := 𝕜) f f'u u
if₂u : (f'u ∘SL ContinuousLinearMap.inr 𝕜 E₁ E₂).IsInvertible
⊢ Tendsto (dfu.implicitFunctionOfProdDomain if₂u) (𝓝 u.1) (𝓝 (dfu.implicitFunctionOfProdDomain if₂u u.1))

Tactic:
have := (dfu.hasStrictFDerivAt_implicitFunctionOfProdDomain if₂u).continuousAt.tendsto