awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Gradient.Basic (goal)
Goal:
𝕜 : Type u_1
F : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace 𝕜 F
inst_3 : CompleteSpace F
f : F → 𝕜
x : F
f₁ : F → 𝕜
hL : f₁ =ᶠ[𝓝 x] f
⊢ Eq.{u_2 + 1} (α := F)
    ((LinearIsometryEquiv.symm (toDual 𝕜 F) : (a : StrongDual 𝕜 F) → F) (fderiv 𝕜 f₁ x : F →L[𝕜] 𝕜) : F)
    ((LinearIsometryEquiv.symm (toDual 𝕜 F) : (a : StrongDual 𝕜 F) → F) (fderiv 𝕜 f x : F →L[𝕜] 𝕜) : F)
have rwa : Eq.{u_2 + 1} (α := F)
  ((LinearIsometryEquiv.symm (toDual 𝕜 F) : (a : StrongDual 𝕜 F) → F) (fderiv 𝕜 f x : F →L[𝕜] 𝕜) : F)
  ((LinearIsometryEquiv.symm (toDual 𝕜 F) : (a : StrongDual 𝕜 F) → F) (fderiv 𝕜 f x : F →L[𝕜] 𝕜) : F)
Tactic: rwa [Filter.EventuallyEq.fderiv_eq]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Gradient.Basic (goal)
Goal:
𝕜 : Type u_1
F : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace 𝕜 F
inst_3 : CompleteSpace F
x : F
L : Filter F
c : 𝕜
⊢ HasGradientAtFilter.{u_1, u_2} (𝕜 := 𝕜) (fun (x : F) ↦ c) 0 x L
have rw : HasFDerivAtFilter.{u_1, u_2, u_1} (𝕜 := 𝕜) (F := 𝕜) (fun (x : F) ↦ c) 0 (SProd.sprod (β := Filter F) L (pure x))
Tactic: rw [HasGradientAtFilter, map_zero]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Implicit (goal)
Goal:
𝕜 : 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
φ : ImplicitFunctionData 𝕜 E F G
⊢ ContinuousLinearMap.IsInvertible (fderiv 𝕜 φ.prodFun φ.pt)
have rw : (↑(φ.leftDeriv.equivProdOfSurjectiveOfIsCompl φ.rightDeriv sorry sorry sorry) : E →L[𝕜] F × G).IsInvertible
Tactic: rw [φ.hasStrictFDerivAt.hasFDerivAt.fderiv]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Implicit (hypothesis)
Goal:
𝕜 : 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
φ : ImplicitFunctionData 𝕜 E F G
⊢ ∀ᶠ (x : E) in 𝓝 φ.pt, φ.leftFun (φ.implicitFunction (φ.leftFun φ.pt) (φ.rightFun x)) = φ.leftFun φ.pt
have this : ∀ᶠ (x : F × G) in 𝓝 (φ.leftFun φ.pt, φ.rightFun φ.pt),
  φ.leftFun (φ.implicitFunction (φ.leftFun φ.pt, x.2).1 (φ.leftFun φ.pt, x.2).2) = (φ.leftFun φ.pt, x.2).1
Tactic: have := φ.leftFun_implicitFunction.curry_nhds.self_of_nhds.prod_inr_nhds (φ.leftFun φ.pt)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Implicit (goal)
Goal:
𝕜 : 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
φ : ImplicitFunctionData 𝕜 E F G
this :
  ∀ᶠ (x : F × G) in 𝓝 (φ.leftFun φ.pt, φ.rightFun φ.pt),
    φ.leftFun (φ.implicitFunction (φ.leftFun φ.pt, x.2).1 (φ.leftFun φ.pt, x.2).2) = (φ.leftFun φ.pt, x.2).1
⊢ ∀ᶠ (x : E) in 𝓝 φ.pt, φ.leftFun (φ.implicitFunction (φ.leftFun φ.pt) (φ.rightFun x)) = φ.leftFun φ.pt
have rwa : ∀
  (this :
    ∀ᶠ (x : F × G) in 𝓝 (φ.prodFun φ.pt),
      φ.leftFun (φ.implicitFunction (φ.leftFun φ.pt, x.2).1 (φ.leftFun φ.pt, x.2).2) = (φ.leftFun φ.pt, x.2).1),
  ∀ᶠ (x : E) in 𝓝 φ.pt, φ.leftFun (φ.implicitFunction (φ.leftFun φ.pt) (φ.rightFun x)) = φ.leftFun φ.pt
Tactic: rwa [← prodFun_apply, ← φ.hasStrictFDerivAt.map_nhds_eq_of_equiv, eventually_map] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Implicit (goal)
Goal:
𝕜 : 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
φ : ImplicitFunctionData 𝕜 E F G
this :
  ∀ᶠ (x : F × G) in 𝓝 (φ.leftFun φ.pt, φ.rightFun φ.pt),
    φ.leftFun (φ.implicitFunction (φ.leftFun φ.pt, x.2).1 (φ.leftFun φ.pt, x.2).2) = (φ.leftFun φ.pt, x.2).1
rwa :
  ∀
    (this :
      ∀ᶠ (x : F × G) in 𝓝 (φ.prodFun φ.pt),
        φ.leftFun (φ.implicitFunction (φ.leftFun φ.pt, x.2).1 (φ.leftFun φ.pt, x.2).2) = (φ.leftFun φ.pt, x.2).1),
    ∀ᶠ (x : E) in 𝓝 φ.pt, φ.leftFun (φ.implicitFunction (φ.leftFun φ.pt) (φ.rightFun x)) = φ.leftFun φ.pt
⊢ ∀ᶠ (x : E) in 𝓝 φ.pt, φ.leftFun (φ.implicitFunction (φ.leftFun φ.pt) (φ.rightFun x)) = φ.leftFun φ.pt
have rwa₁ : ∀
  (this :
    ∀ᶠ (x : F × G) in map φ.prodFun (𝓝 φ.pt),
      φ.leftFun (φ.implicitFunction (φ.leftFun φ.pt, x.2).1 (φ.leftFun φ.pt, x.2).2) = (φ.leftFun φ.pt, x.2).1),
  ∀ᶠ (x : E) in 𝓝 φ.pt, φ.leftFun (φ.implicitFunction (φ.leftFun φ.pt) (φ.rightFun x)) = φ.leftFun φ.pt
Tactic: rwa [← prodFun_apply, ← φ.hasStrictFDerivAt.map_nhds_eq_of_equiv, eventually_map] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Implicit (goal)
Goal:
𝕜 : 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
φ : ImplicitFunctionData 𝕜 E F G
this :
  ∀ᶠ (x : F × G) in 𝓝 (φ.leftFun φ.pt, φ.rightFun φ.pt),
    φ.leftFun (φ.implicitFunction (φ.leftFun φ.pt, x.2).1 (φ.leftFun φ.pt, x.2).2) = (φ.leftFun φ.pt, x.2).1
rwa :
  ∀
    (this :
      ∀ᶠ (x : F × G) in 𝓝 (φ.prodFun φ.pt),
        φ.leftFun (φ.implicitFunction (φ.leftFun φ.pt, x.2).1 (φ.leftFun φ.pt, x.2).2) = (φ.leftFun φ.pt, x.2).1),
    ∀ᶠ (x : E) in 𝓝 φ.pt, φ.leftFun (φ.implicitFunction (φ.leftFun φ.pt) (φ.rightFun x)) = φ.leftFun φ.pt
rwa₁ :
  ∀
    (this :
      ∀ᶠ (x : F × G) in map φ.prodFun (𝓝 φ.pt),
        φ.leftFun (φ.implicitFunction (φ.leftFun φ.pt, x.2).1 (φ.leftFun φ.pt, x.2).2) = (φ.leftFun φ.pt, x.2).1),
    ∀ᶠ (x : E) in 𝓝 φ.pt, φ.leftFun (φ.implicitFunction (φ.leftFun φ.pt) (φ.rightFun x)) = φ.leftFun φ.pt
⊢ ∀ᶠ (x : E) in 𝓝 φ.pt, φ.leftFun (φ.implicitFunction (φ.leftFun φ.pt) (φ.rightFun x)) = φ.leftFun φ.pt
have rwa₂ : ∀
  (this :
    ∀ᶠ (a : E) in 𝓝 φ.pt,
      φ.leftFun (φ.implicitFunction (φ.leftFun φ.pt, (φ.prodFun a).2).1 (φ.leftFun φ.pt, (φ.prodFun a).2).2) =
        (φ.leftFun φ.pt, (φ.prodFun a).2).1),
  ∀ᶠ (x : E) in 𝓝 φ.pt, φ.leftFun (φ.implicitFunction (φ.leftFun φ.pt) (φ.rightFun x)) = φ.leftFun φ.pt
Tactic: rwa [← prodFun_apply, ← φ.hasStrictFDerivAt.map_nhds_eq_of_equiv, eventually_map] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Implicit (hypothesis)
Goal:
𝕜 : 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
φ : ImplicitFunctionData 𝕜 E F G
⊢ ∀ᶠ (x : E) in 𝓝 φ.pt, φ.rightFun (φ.implicitFunction (φ.leftFun φ.pt) (φ.rightFun x)) = φ.rightFun x
have this : ∀ᶠ (x : F × G) in 𝓝 (φ.leftFun φ.pt, φ.rightFun φ.pt),
  φ.rightFun (φ.implicitFunction (φ.leftFun φ.pt, x.2).1 (φ.leftFun φ.pt, x.2).2) = (φ.leftFun φ.pt, x.2).2
Tactic: have := φ.rightFun_implicitFunction.curry_nhds.self_of_nhds.prod_inr_nhds (φ.leftFun φ.pt)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Implicit (goal)
Goal:
𝕜 : 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
φ : ImplicitFunctionData 𝕜 E F G
this :
  ∀ᶠ (x : F × G) in 𝓝 (φ.leftFun φ.pt, φ.rightFun φ.pt),
    φ.rightFun (φ.implicitFunction (φ.leftFun φ.pt, x.2).1 (φ.leftFun φ.pt, x.2).2) = (φ.leftFun φ.pt, x.2).2
⊢ ∀ᶠ (x : E) in 𝓝 φ.pt, φ.rightFun (φ.implicitFunction (φ.leftFun φ.pt) (φ.rightFun x)) = φ.rightFun x
have rwa : ∀
  (this :
    ∀ᶠ (x : F × G) in 𝓝 (φ.prodFun φ.pt),
      φ.rightFun (φ.implicitFunction (φ.leftFun φ.pt, x.2).1 (φ.leftFun φ.pt, x.2).2) = (φ.leftFun φ.pt, x.2).2),
  ∀ᶠ (x : E) in 𝓝 φ.pt, φ.rightFun (φ.implicitFunction (φ.leftFun φ.pt) (φ.rightFun x)) = φ.rightFun x
Tactic: rwa [← prodFun_apply, ← φ.hasStrictFDerivAt.map_nhds_eq_of_equiv, eventually_map] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Implicit (goal)
Goal:
𝕜 : 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
φ : ImplicitFunctionData 𝕜 E F G
this :
  ∀ᶠ (x : F × G) in 𝓝 (φ.leftFun φ.pt, φ.rightFun φ.pt),
    φ.rightFun (φ.implicitFunction (φ.leftFun φ.pt, x.2).1 (φ.leftFun φ.pt, x.2).2) = (φ.leftFun φ.pt, x.2).2
rwa :
  ∀
    (this :
      ∀ᶠ (x : F × G) in 𝓝 (φ.prodFun φ.pt),
        φ.rightFun (φ.implicitFunction (φ.leftFun φ.pt, x.2).1 (φ.leftFun φ.pt, x.2).2) = (φ.leftFun φ.pt, x.2).2),
    ∀ᶠ (x : E) in 𝓝 φ.pt, φ.rightFun (φ.implicitFunction (φ.leftFun φ.pt) (φ.rightFun x)) = φ.rightFun x
⊢ ∀ᶠ (x : E) in 𝓝 φ.pt, φ.rightFun (φ.implicitFunction (φ.leftFun φ.pt) (φ.rightFun x)) = φ.rightFun x
have rwa₁ : ∀
  (this :
    ∀ᶠ (x : F × G) in map φ.prodFun (𝓝 φ.pt),
      φ.rightFun (φ.implicitFunction (φ.leftFun φ.pt, x.2).1 (φ.leftFun φ.pt, x.2).2) = (φ.leftFun φ.pt, x.2).2),
  ∀ᶠ (x : E) in 𝓝 φ.pt, φ.rightFun (φ.implicitFunction (φ.leftFun φ.pt) (φ.rightFun x)) = φ.rightFun x
Tactic: rwa [← prodFun_apply, ← φ.hasStrictFDerivAt.map_nhds_eq_of_equiv, eventually_map] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Implicit (goal)
Goal:
𝕜 : 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
φ : ImplicitFunctionData 𝕜 E F G
this :
  ∀ᶠ (x : F × G) in 𝓝 (φ.leftFun φ.pt, φ.rightFun φ.pt),
    φ.rightFun (φ.implicitFunction (φ.leftFun φ.pt, x.2).1 (φ.leftFun φ.pt, x.2).2) = (φ.leftFun φ.pt, x.2).2
rwa :
  ∀
    (this :
      ∀ᶠ (x : F × G) in 𝓝 (φ.prodFun φ.pt),
        φ.rightFun (φ.implicitFunction (φ.leftFun φ.pt, x.2).1 (φ.leftFun φ.pt, x.2).2) = (φ.leftFun φ.pt, x.2).2),
    ∀ᶠ (x : E) in 𝓝 φ.pt, φ.rightFun (φ.implicitFunction (φ.leftFun φ.pt) (φ.rightFun x)) = φ.rightFun x
rwa₁ :
  ∀
    (this :
      ∀ᶠ (x : F × G) in map φ.prodFun (𝓝 φ.pt),
        φ.rightFun (φ.implicitFunction (φ.leftFun φ.pt, x.2).1 (φ.leftFun φ.pt, x.2).2) = (φ.leftFun φ.pt, x.2).2),
    ∀ᶠ (x : E) in 𝓝 φ.pt, φ.rightFun (φ.implicitFunction (φ.leftFun φ.pt) (φ.rightFun x)) = φ.rightFun x
⊢ ∀ᶠ (x : E) in 𝓝 φ.pt, φ.rightFun (φ.implicitFunction (φ.leftFun φ.pt) (φ.rightFun x)) = φ.rightFun x
have rwa₂ : ∀
  (this :
    ∀ᶠ (a : E) in 𝓝 φ.pt,
      φ.rightFun (φ.implicitFunction (φ.leftFun φ.pt, (φ.prodFun a).2).1 (φ.leftFun φ.pt, (φ.prodFun a).2).2) =
        (φ.leftFun φ.pt, (φ.prodFun a).2).2),
  ∀ᶠ (x : E) in 𝓝 φ.pt, φ.rightFun (φ.implicitFunction (φ.leftFun φ.pt) (φ.rightFun x)) = φ.rightFun x
Tactic: rwa [← prodFun_apply, ← φ.hasStrictFDerivAt.map_nhds_eq_of_equiv, eventually_map] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Implicit (goal)
Goal:
𝕜 : 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
φ : ImplicitFunctionData 𝕜 E F G
⊢ ∀ᶠ (x : E) in 𝓝 φ.pt, φ.leftFun x = φ.leftFun φ.pt ↔ φ.implicitFunction (φ.leftFun φ.pt) (φ.rightFun x) = x
have h : ∀ (x : E),
  φ.implicitFunction (φ.leftFun x) (φ.rightFun x) = x →
    φ.leftFun (φ.implicitFunction (φ.leftFun φ.pt) (φ.rightFun x)) = φ.leftFun φ.pt →
      (φ.leftFun x = φ.leftFun φ.pt ↔ φ.implicitFunction (φ.leftFun φ.pt) (φ.rightFun x) = x)
Tactic: filter_upwards [φ.implicitFunction_apply_image, φ.leftFun_implicitFunction_eq_leftFun] with x _ _
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Implicit (goal)
Goal:
𝕜 : 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
φ : ImplicitFunctionData 𝕜 E F G
x : E
h : φ.implicitFunction (φ.leftFun x) (φ.rightFun x) = x
h_1 : φ.leftFun (φ.implicitFunction (φ.leftFun φ.pt) (φ.rightFun x)) = φ.leftFun φ.pt
⊢ φ.leftFun x = φ.leftFun φ.pt ↔ φ.implicitFunction (φ.leftFun φ.pt) (φ.rightFun x) = x
have h : φ.leftFun x = φ.leftFun φ.pt → φ.implicitFunction (φ.leftFun φ.pt) (φ.rightFun x) = x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Implicit (goal)
Goal:
𝕜 : 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
φ : ImplicitFunctionData 𝕜 E F G
x : E
h_1 : φ.implicitFunction (φ.leftFun x) (φ.rightFun x) = x
h_2 : φ.leftFun (φ.implicitFunction (φ.leftFun φ.pt) (φ.rightFun x)) = φ.leftFun φ.pt
h : φ.leftFun x = φ.leftFun φ.pt → φ.implicitFunction (φ.leftFun φ.pt) (φ.rightFun x) = x
⊢ φ.leftFun x = φ.leftFun φ.pt ↔ φ.implicitFunction (φ.leftFun φ.pt) (φ.rightFun x) = x
have h₁ : φ.implicitFunction (φ.leftFun φ.pt) (φ.rightFun x) = x → φ.leftFun x = φ.leftFun φ.pt
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Implicit (goal)
Goal:
𝕜 : 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
φ : ImplicitFunctionData 𝕜 E F G
⊢ map (Prod.fst ∘ φ.prodFun) (𝓝 φ.pt) = 𝓝 (φ.prodFun φ.pt).1
have rw : map Prod.fst (map φ.prodFun (𝓝 φ.pt)) = 𝓝 (φ.prodFun φ.pt).1
Tactic: rw [← map_map, φ.hasStrictFDerivAt.map_nhds_eq_of_equiv, map_fst_nhds]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Implicit (goal)
Goal:
𝕜 : 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
φ : ImplicitFunctionData 𝕜 E F G
rw : map Prod.fst (map φ.prodFun (𝓝 φ.pt)) = 𝓝 (φ.prodFun φ.pt).1
⊢ map (Prod.fst ∘ φ.prodFun) (𝓝 φ.pt) = 𝓝 (φ.prodFun φ.pt).1
have rw₁ : map Prod.fst (𝓝 (φ.prodFun φ.pt)) = 𝓝 (φ.prodFun φ.pt).1
Tactic: rw [← map_map, φ.hasStrictFDerivAt.map_nhds_eq_of_equiv, map_fst_nhds]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Implicit (goal)
Goal:
𝕜 : 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
φ : ImplicitFunctionData 𝕜 E F G
rw : map Prod.fst (map φ.prodFun (𝓝 φ.pt)) = 𝓝 (φ.prodFun φ.pt).1
rw₁ : map Prod.fst (𝓝 (φ.prodFun φ.pt)) = 𝓝 (φ.prodFun φ.pt).1
⊢ map (Prod.fst ∘ φ.prodFun) (𝓝 φ.pt) = 𝓝 (φ.prodFun φ.pt).1
have rw₂ : 𝓝 (φ.prodFun φ.pt).1 = 𝓝 (φ.prodFun φ.pt).1
Tactic: rw [← map_map, φ.hasStrictFDerivAt.map_nhds_eq_of_equiv, map_fst_nhds]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Implicit (hypothesis)
Goal:
𝕜 : 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
φ : ImplicitFunctionData 𝕜 E F G
⊢ HasStrictFDerivAt (φ.implicitFunction (φ.leftFun φ.pt))
    (fderiv 𝕜 (φ.implicitFunction (φ.leftFun φ.pt)) (φ.rightFun φ.pt)) (φ.rightFun φ.pt)
have this : HasStrictFDerivAt
  (fun (x : G) ↦
    HasStrictFDerivAt.localInverse φ.prodFun (φ.leftDeriv.equivProdOfSurjectiveOfIsCompl φ.rightDeriv sorry sorry sorry) φ.pt sorry
      (φ.leftFun φ.pt, x))
  ((↑(φ.leftDeriv.equivProdOfSurjectiveOfIsCompl φ.rightDeriv sorry sorry sorry).symm : F × G →L[𝕜] E).comp (σ₁₂ := RingHom.id 𝕜)
    (ContinuousLinearMap.prod 0 (ContinuousLinearMap.id 𝕜 G)))
  (φ.rightFun φ.pt)
Tactic: have := φ.hasStrictFDerivAt.to_localInverse.comp (φ.rightFun φ.pt)
    ((hasStrictFDerivAt_const _ _).prodMk (hasStrictFDerivAt_id _))
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Implicit (goal)
Goal:
𝕜 : 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
φ : ImplicitFunctionData 𝕜 E F G
this :
  HasStrictFDerivAt
    (fun (x : G) ↦
      HasStrictFDerivAt.localInverse φ.prodFun (φ.leftDeriv.equivProdOfSurjectiveOfIsCompl φ.rightDeriv ⋯ ⋯ ⋯) φ.pt ⋯
        (φ.leftFun φ.pt, x))
    ((↑(φ.leftDeriv.equivProdOfSurjectiveOfIsCompl φ.rightDeriv ⋯ ⋯ ⋯).symm : F × G →L[𝕜] E).comp (σ₁₂ := RingHom.id 𝕜)
      (ContinuousLinearMap.prod 0 (ContinuousLinearMap.id 𝕜 G)))
    (φ.rightFun φ.pt)
⊢ HasStrictFDerivAt (φ.implicitFunction (φ.leftFun φ.pt))
    (fderiv 𝕜 (φ.implicitFunction (φ.leftFun φ.pt)) (φ.rightFun φ.pt)) (φ.rightFun φ.pt)
have h : fderiv 𝕜 (φ.implicitFunction (φ.leftFun φ.pt)) (φ.rightFun φ.pt) =
  (↑(φ.leftDeriv.equivProdOfSurjectiveOfIsCompl φ.rightDeriv sorry sorry sorry).symm : F × G →L[𝕜] E).comp (σ₁₂ := RingHom.id 𝕜)
    (ContinuousLinearMap.prod 0 (ContinuousLinearMap.id 𝕜 G))
Tactic: convert! this
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Implicit (goal)
Goal:
𝕜 : 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
φ : ImplicitFunctionData 𝕜 E F G
x : G
y : E
⊢ (fderiv 𝕜 (φ.implicitFunction (φ.leftFun φ.pt)) (φ.rightFun φ.pt) : (a : G) → E) x = y ↔
    Eq.{u_3 + 1} (α := F) ((φ.leftDeriv : (a : E) → F) y : F) (0 : F) ∧ (φ.rightDeriv : (a : E) → G) y = x
have unfold : (fderiv 𝕜
          (fun (b : G) ↦
            (↑(HasStrictFDerivAt.toOpenPartialHomeomorph φ.prodFun sorry).symm : F × G → E) (φ.leftFun φ.pt, b))
          (φ.rightFun φ.pt) :
        (a : G) → E)
      x =
    y ↔
  Eq.{u_3 + 1} (α := F) ((φ.leftDeriv : (a : E) → F) y : F) (0 : F) ∧ (φ.rightDeriv : (a : E) → G) y = x
Tactic: unfold implicitFunction Function.curry toOpenPartialHomeomorph
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Implicit (goal)
Goal:
𝕜 : 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
φ : ImplicitFunctionData 𝕜 E F G
x : G
y : E
⊢ (fderiv 𝕜
            (fun (b : G) ↦
              (↑(HasStrictFDerivAt.toOpenPartialHomeomorph φ.prodFun ⋯).symm : F × G → E) (φ.leftFun φ.pt, b))
            (φ.rightFun φ.pt) :
          (a : G) → E)
        x =
      y ↔
    Eq.{u_3 + 1} (α := F) ((φ.leftDeriv : (a : E) → F) y : F) (0 : F) ∧ (φ.rightDeriv : (a : E) → G) y = x
have simp : (fderiv 𝕜
          (fun (b : G) ↦
            HasStrictFDerivAt.localInverse φ.prodFun (φ.leftDeriv.equivProdOfSurjectiveOfIsCompl φ.rightDeriv sorry sorry sorry)
              φ.pt sorry (φ.leftFun φ.pt, b))
          (φ.rightFun φ.pt) :
        (a : G) → E)
      x =
    y ↔
  Eq.{u_3 + 1} (α := F) ((φ.leftDeriv : (a : E) → F) y : F) (0 : F) ∧ (φ.rightDeriv : (a : E) → G) y = x
Tactic: simp only [← HasStrictFDerivAt.localInverse_def]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Implicit (goal)
Goal:
𝕜 : 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
φ : ImplicitFunctionData 𝕜 E F G
x : G
y : E
⊢ (fderiv 𝕜
            (fun (b : G) ↦
              HasStrictFDerivAt.localInverse φ.prodFun (φ.leftDeriv.equivProdOfSurjectiveOfIsCompl φ.rightDeriv ⋯ ⋯ ⋯)
                φ.pt ⋯ (φ.leftFun φ.pt, b))
            (φ.rightFun φ.pt) :
          (a : G) → E)
        x =
      y ↔
    Eq.{u_3 + 1} (α := F) ((φ.leftDeriv : (a : E) → F) y : F) (0 : F) ∧ (φ.rightDeriv : (a : E) → G) y = x
have rw : ((↑(φ.leftDeriv.equivProdOfSurjectiveOfIsCompl φ.rightDeriv sorry sorry sorry).symm : F × G →L[𝕜] E).comp (σ₁₂ := RingHom.id 𝕜)
          (ContinuousLinearMap.prod 0 (ContinuousLinearMap.id 𝕜 G)) :
        (a : G) → E)
      x =
    y ↔
  Eq.{u_3 + 1} (α := F) ((φ.leftDeriv : (a : E) → F) y : F) (0 : F) ∧ (φ.rightDeriv : (a : E) → G) y = x
Tactic: rw [φ.hasStrictFDerivAt.to_localInverse.comp (φ.rightFun φ.pt)
    ((hasStrictFDerivAt_const _ _).prodMk (hasStrictFDerivAt_id _)) |>.hasFDerivAt |>.fderiv]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Implicit (goal)
Goal:
𝕜 : 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
φ : ImplicitFunctionData 𝕜 E F G
g'inv : G →L[𝕜] E
hg'inv : φ.rightDeriv ∘SL g'inv = ContinuousLinearMap.id 𝕜 G
hg'invf : φ.leftDeriv ∘SL g'inv = 0
⊢ HasStrictFDerivAt (φ.implicitFunction (φ.leftFun φ.pt)) g'inv (φ.rightFun φ.pt)
have h : g'inv = fderiv 𝕜 (φ.implicitFunction (φ.leftFun φ.pt)) (φ.rightFun φ.pt)
Tactic: convert! φ.hasStrictFDerivAt_implicitFunction_fderiv
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Implicit (goal)
Goal:
𝕜 : 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
φ : ImplicitFunctionData 𝕜 E F G
g'inv : G →L[𝕜] E
hg'inv : φ.rightDeriv ∘SL g'inv = ContinuousLinearMap.id 𝕜 G
hg'invf : φ.leftDeriv ∘SL g'inv = 0
⊢ g'inv = fderiv 𝕜 (φ.implicitFunction (φ.leftFun φ.pt)) (φ.rightFun φ.pt)
have h : ∀ (x : G),
  Eq.{u_2 + 1} (α := E) ((g'inv : (a : G) → E) x : E)
    ((fderiv 𝕜 (φ.implicitFunction (φ.leftFun φ.pt)) (φ.rightFun φ.pt) : (a : G) → E) x : E)
Tactic: ext1 x