awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ImplicitContDiff (goal)
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 𝕜 n φ.prodFun φ.pt
have h : ∀ (x : E₁), (φ.prodFun x).1 = φ.leftFun x
Tactic: convert! hl.prodMk hr
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ImplicitContDiff (goal)
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
⊢ ContDiffAt 𝕜 n φ.prodFun φ.pt
have h₁ : ∀ (x : E₁), (φ.prodFun x).2 = φ.rightFun x
Tactic: convert! hl.prodMk hr
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ImplicitContDiff (goal)
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₂))
⊢ ContDiffAt 𝕜 n (cdf.implicitFunction pn if₂) u.1
have rw : ContDiffAt.{u_1, u_2, u_3} 𝕜 (F := E₂) n
  (fun (x : E₁) ↦
    (ImplicitFunctionData.implicitFunction
        (sorry.implicitFunctionDataOfProdDomain if₂ : ImplicitFunctionData 𝕜 (E₁ × E₂) F E₁) (f u) x).2)
  u.1
Tactic: rw [ContDiffAt.implicitFunction_def, HasStrictFDerivAt.implicitFunctionOfProdDomain_def]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ImplicitContDiff (hypothesis)
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.{u_1, u_2, u_3} 𝕜 (F := E₂) n (fun (x : E₁) ↦ (φ.implicitFunction (f u) x).2) u.1
have this : 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
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ImplicitFunction.ProdDomain (hypothesis)
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 : E₁ × E₂ →ₗ[𝕜] F).range = ⊤
have this : (↑(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 ..
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ImplicitFunction.ProdDomain (goal)
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
⊢ (↑f'u : E₁ × E₂ →ₗ[𝕜] F).range = ⊤
have rwa : ∀ (this : ⊤ ≤ (↑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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ImplicitFunction.ProdDomain (goal)
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 = ⊤
⊢ (↑f'u : E₁ × E₂ →ₗ[𝕜] F).range = ⊤
have rwa₁ : ∀ (this : (↑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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ImplicitFunction.ProdDomain (goal)
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
⊢ IsCompl (↑f'u : E₁ × E₂ →ₗ[𝕜] F).ker
    (LinearMap.ker (R₂ := 𝕜) (M₂ := E₁) (τ₁₂ := RingHom.id 𝕜) (↑(ContinuousLinearMap.fst 𝕜 E₁ E₂) : E₁ × E₂ →ₗ[𝕜] E₁))
have disjoint : Disjoint (↑f'u : E₁ × E₂ →ₗ[𝕜] F).ker
  (LinearMap.ker (R₂ := 𝕜) (M₂ := E₁) (τ₁₂ := RingHom.id 𝕜) (↑(ContinuousLinearMap.fst 𝕜 E₁ E₂) : E₁ × E₂ →ₗ[𝕜] E₁))
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ImplicitFunction.ProdDomain (goal)
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₁))
⊢ IsCompl (↑f'u : E₁ × E₂ →ₗ[𝕜] F).ker
    (LinearMap.ker (R₂ := 𝕜) (M₂ := E₁) (τ₁₂ := RingHom.id 𝕜) (↑(ContinuousLinearMap.fst 𝕜 E₁ E₂) : E₁ × E₂ →ₗ[𝕜] E₁))
have codisjoint : Codisjoint (↑f'u : E₁ × E₂ →ₗ[𝕜] F).ker
  (LinearMap.ker (R₂ := 𝕜) (M₂ := E₁) (τ₁₂ := RingHom.id 𝕜) (↑(ContinuousLinearMap.fst 𝕜 E₁ E₂) : E₁ × E₂ →ₗ[𝕜] E₁))
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ImplicitFunction.ProdDomain (goal)
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 (↑f'u : E₁ × E₂ →ₗ[𝕜] F).ker
    (LinearMap.ker (R₂ := 𝕜) (M₂ := E₁) (τ₁₂ := RingHom.id 𝕜) (↑(ContinuousLinearMap.fst 𝕜 E₁ E₂) : E₁ × E₂ →ₗ[𝕜] E₁))
have 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
Tactic: rw [LinearMap.disjoint_ker]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ImplicitFunction.ProdDomain (goal)
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 (↑f'u : E₁ × E₂ →ₗ[𝕜] F).ker
    (LinearMap.ker (R₂ := 𝕜) (M₂ := E₁) (τ₁₂ := RingHom.id 𝕜) (↑(ContinuousLinearMap.fst 𝕜 E₁ E₂) : E₁ × E₂ →ₗ[𝕜] E₁))
have 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
Tactic: rw [Submodule.codisjoint_iff_exists_add_eq]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ImplicitFunction.ProdDomain (goal)
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₂
⊢ ∃ (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
have 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
Tactic: have ⟨y, hy⟩ := if₂u.surjective (f'u v)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ImplicitFunction.ProdDomain (goal)
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)
⊢ ∃ (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
have 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
Tactic: use v - (0, y), (0, y)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ImplicitFunction.ProdDomain (goal)
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₂) in 𝓝 u, f v = f u ↔ dfu.implicitFunctionOfProdDomain if₂u v.1 = v.2
have 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)
Tactic: filter_upwards [φ.leftFun_eq_iff_implicitFunction, φ.rightFun_implicitFunction_eq_rightFun]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ImplicitFunction.ProdDomain (goal)
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
⊢ HasStrictFDerivAt (dfu.implicitFunctionOfProdDomain if₂u)
    (-(f'u ∘SL ContinuousLinearMap.inr 𝕜 E₁ E₂).inverse ∘SL f'u ∘SL ContinuousLinearMap.inl 𝕜 E₁ E₂) u.1
have 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
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
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ImplicitFunction.ProdDomain (goal)
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.prod (ContinuousLinearMap.id 𝕜 E₁)
        (-(f'u ∘SL ContinuousLinearMap.inr 𝕜 E₁ E₂).inverse ∘SL f'u ∘SL ContinuousLinearMap.inl 𝕜 E₁ E₂) =
    0
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ImplicitFunction.ProdDomain (goal)
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₁
⊢ 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)
have 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
Tactic: rw [f'u.comp_apply, ← f'u.comp_inl_add_comp_inr]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ImplicitFunction.ProdDomain (hypothesis)
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) (𝓝 u.2)
have this : Tendsto (dfu.implicitFunctionOfProdDomain if₂u) (𝓝 u.1) (𝓝 (dfu.implicitFunctionOfProdDomain if₂u u.1))
Tactic: have := (dfu.hasStrictFDerivAt_implicitFunctionOfProdDomain if₂u).continuousAt.tendsto
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ImplicitFunction.ProdDomain (goal)
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 : Tendsto (dfu.implicitFunctionOfProdDomain if₂u) (𝓝 u.1) (𝓝 (dfu.implicitFunctionOfProdDomain if₂u u.1))
⊢ Tendsto (dfu.implicitFunctionOfProdDomain if₂u) (𝓝 u.1) (𝓝 u.2)
have rwa : ∀ (this : Tendsto (dfu.implicitFunctionOfProdDomain if₂u) (𝓝 u.1) (𝓝 u.2)),
  Tendsto (dfu.implicitFunctionOfProdDomain if₂u) (𝓝 u.1) (𝓝 u.2)
Tactic: rwa [(dfu.eventually_apply_eq_iff_implicitFunctionOfProdDomain if₂u).self_of_nhds.mp rfl] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ImplicitFunction.ProdDomain (hypothesis)
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₁) in 𝓝 u.1, f (x, dfu.implicitFunctionOfProdDomain if₂u x) = f u
have hψ : Tendsto (dfu.implicitFunctionOfProdDomain if₂u) (𝓝 u.1) (𝓝 u.2)
Tactic: have hψ := dfu.tendsto_implicitFunctionOfProdDomain if₂u
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ImplicitFunction.ProdDomain (goal)
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ψ : Tendsto (dfu.implicitFunctionOfProdDomain if₂u) (𝓝 u.1) (𝓝 u.2)
⊢ ∀ᶠ (x : E₁) in 𝓝 u.1, f (x, dfu.implicitFunctionOfProdDomain if₂u x) = f u
have set : let ψ := dfu.implicitFunctionOfProdDomain if₂u;
∀ (hψ : Tendsto ψ (𝓝 u.1) (𝓝 u.2)), ∀ᶠ (x : E₁) in 𝓝 u.1, f (x, ψ x) = f u
Tactic: set ψ := dfu.implicitFunctionOfProdDomain if₂u
Cleared hypotheses: hψ
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ImplicitFunction.ProdDomain (goal)
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
ψ : E₁ → E₂ := dfu.implicitFunctionOfProdDomain if₂u
hψ : Tendsto ψ (𝓝 u.1) (𝓝 u.2)
⊢ ∀ᶠ (x : E₁) in 𝓝 u.1, f (x, ψ x) = f u
have suffices : ∀ᶠ (x : E₁) in 𝓝 u.1, f (x, ψ x) = f u ↔ ψ x = ψ x
Tactic: suffices ∀ᶠ x in 𝓝 u.1, f (x, ψ x) = f u ↔ ψ x = ψ x by simpa using this
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ImplicitFunction.ProdDomain (goal)
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
ψ : E₁ → E₂ := dfu.implicitFunctionOfProdDomain if₂u
hψ : Tendsto ψ (𝓝 u.1) (𝓝 u.2)
⊢ ∀ᶠ (x : E₁) in 𝓝 u.1, f (x, ψ x) = f u ↔ ψ x = ψ x
have apply : ∀ᶠ (p : E₁ × E₂) in 𝓝 u.1 ×ˢ 𝓝 u.2, f (p.1, p.2) = f u ↔ ψ p.1 = p.2
Tactic: apply Eventually.image_of_prod (r := fun x y => f (x, y) = f u ↔ ψ x = y) hψ
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ImplicitFunction.ProdDomain (goal)
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
ψ : E₁ → E₂ := dfu.implicitFunctionOfProdDomain if₂u
hψ : Tendsto ψ (𝓝 u.1) (𝓝 u.2)
⊢ ∀ᶠ (p : E₁ × E₂) in 𝓝 u.1 ×ˢ 𝓝 u.2, f (p.1, p.2) = f u ↔ ψ p.1 = p.2
have rw : ∀ᶠ (p : E₁ × E₂) in 𝓝 (u.1, u.2), f (p.1, p.2) = f u ↔ ψ p.1 = p.2
Tactic: rw [← nhds_prod_eq]