awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.Implicit
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
⊢ (φ.leftFun φ.pt, φ.rightFun φ.pt) ∈ φ.toOpenPartialHomeomorph.target

Tactic:
φ.toOpenPartialHomeomorph.map_source <| φ.pt_mem_toOpenPartialHomeomorph_source

Premises used: Set.Mem, ImplicitFunctionData.pt_mem_toOpenPartialHomeomorph_source, OpenPartialHomeomorph.toFun', ImplicitFunctionData.toOpenPartialHomeomorph, OpenPartialHomeomorph.map_source, ImplicitFunctionData.prodFun
-- Module: Mathlib.Analysis.Calculus.Implicit
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
⊢ ∀ᶠ (p : F × G) in 𝓝 (φ.prodFun φ.pt), φ.prodFun (φ.implicitFunction p.1 p.2) = p

Tactic:
φ.hasStrictFDerivAt.eventually_right_inverse.mono fun ⟨_, _⟩ h => h

Premises used: ImplicitFunctionData.implicitFunction, _private.0.ImplicitFunctionData.prodFun_implicitFunction.match_1, setOf, Prod.fst, ImplicitFunctionData.hasStrictFDerivAt, Filter.Eventually.mono, HasStrictFDerivAt.eventually_right_inverse, ImplicitFunctionData.prodFun, Eq, Prod.snd
-- Module: Mathlib.Analysis.Calculus.Implicit
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
⊢ ∀ᶠ (p : F × G) in 𝓝 (φ.prodFun φ.pt), φ.leftFun (φ.implicitFunction p.1 p.2) = p.1

Tactic:
φ.prodFun_implicitFunction.mono fun _ => congr_arg Prod.fst

Premises used: Prod.fst, Filter.Eventually.mono, congr_arg, ImplicitFunctionData.prodFun_implicitFunction
-- Module: Mathlib.Analysis.Calculus.Implicit
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
⊢ ∀ᶠ (p : F × G) in 𝓝 (φ.prodFun φ.pt), φ.rightFun (φ.implicitFunction p.1 p.2) = p.2

Tactic:
φ.prodFun_implicitFunction.mono fun _ => congr_arg Prod.snd

Premises used: Filter.Eventually.mono, congr_arg, Prod.snd, ImplicitFunctionData.prodFun_implicitFunction
-- Module: Mathlib.Analysis.Calculus.Implicit
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, φ.implicitFunction (φ.leftFun x) (φ.rightFun x) = x

Tactic:
φ.hasStrictFDerivAt.eventually_left_inverse

Premises used: ImplicitFunctionData.implicitFunction, setOf, HasStrictFDerivAt.eventually_left_inverse, HasStrictFDerivAt.localInverse, ImplicitFunctionData.hasStrictFDerivAt, ImplicitFunctionData.toOpenPartialHomeomorph, ImplicitFunctionData.prodFun
-- Module: Mathlib.Analysis.Calculus.Implicit
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 : 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)
-- Module: Mathlib.Analysis.Calculus.Implicit
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
rwa₂ rwa₃ rwa₄ 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
⊢ ∀ᶠ (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

Premises used: HasStrictFDerivAt.map_nhds_eq_of_equiv, ImplicitFunctionData.prodFun_apply, Filter.eventually_map, ImplicitFunctionData.hasStrictFDerivAt
-- Module: Mathlib.Analysis.Calculus.Implicit
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 : 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)
-- Module: Mathlib.Analysis.Calculus.Implicit
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
rwa₂ rwa₃ rwa₄ 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
⊢ ∀ᶠ (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

Premises used: HasStrictFDerivAt.map_nhds_eq_of_equiv, ImplicitFunctionData.prodFun_apply, Filter.eventually_map, ImplicitFunctionData.hasStrictFDerivAt
-- Module: Mathlib.Analysis.Calculus.Implicit
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 →
    φ.leftFun (φ.implicitFunction (φ.leftFun φ.pt) (φ.rightFun x)) = φ.leftFun φ.pt →
      (φ.leftFun x = φ.leftFun φ.pt ↔ φ.implicitFunction (φ.leftFun φ.pt) (φ.rightFun x) = x)
⊢ φ.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:
_
-- Module: Mathlib.Analysis.Calculus.Implicit
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 :
  φ.leftFun (φ.implicitFunction (φ.leftFun φ.pt) (φ.rightFun x)) = φ.leftFun φ.pt →
    (φ.leftFun x = φ.leftFun φ.pt ↔ φ.implicitFunction (φ.leftFun φ.pt) (φ.rightFun x) = x)
⊢ φ.leftFun (φ.implicitFunction (φ.leftFun φ.pt) (φ.rightFun x)) = φ.leftFun φ.pt →
    (φ.leftFun x = φ.leftFun φ.pt ↔ φ.implicitFunction (φ.leftFun φ.pt) (φ.rightFun x) = x)

Tactic:
_
-- Module: Mathlib.Analysis.Calculus.Implicit
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
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)
⊢ ∀ᶠ (x : E) in 𝓝 φ.pt, φ.leftFun x = φ.leftFun φ.pt ↔ φ.implicitFunction (φ.leftFun φ.pt) (φ.rightFun x) = x

Tactic:
filter_upwards [φ.implicitFunction_apply_image, φ.leftFun_implicitFunction_eq_leftFun] with x _ _

Premises used: ImplicitFunctionData.leftFun_implicitFunction_eq_leftFun, ImplicitFunctionData.implicitFunction_apply_image
-- Module: Mathlib.Analysis.Calculus.Implicit
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
h₁ : φ.implicitFunction (φ.leftFun φ.pt) (φ.rightFun x) = x → φ.leftFun x = φ.leftFun φ.pt
⊢ φ.leftFun x = φ.leftFun φ.pt ↔ φ.implicitFunction (φ.leftFun φ.pt) (φ.rightFun x) = x

Tactic:
constructor
-- Module: Mathlib.Analysis.Calculus.Implicit
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
rwa rwa₁ rwa₂ rwa₃ : φ.implicitFunction (φ.leftFun x) (φ.rightFun x) = x
⊢ φ.implicitFunction (φ.leftFun φ.pt) (φ.rightFun x) = x

Tactic:
rwa [← h]
-- Module: Mathlib.Analysis.Calculus.Implicit
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

Tactic:
exact fun h => by rwa [← h]
-- Module: Mathlib.Analysis.Calculus.Implicit
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 : φ.implicitFunction (φ.leftFun φ.pt) (φ.rightFun x) = x
rwa rwa₁ rwa₂ rwa₃ : φ.leftFun (φ.implicitFunction (φ.leftFun φ.pt) (φ.rightFun x)) = φ.leftFun φ.pt
⊢ φ.leftFun x = φ.leftFun φ.pt

Tactic:
rwa [← h]
-- Module: Mathlib.Analysis.Calculus.Implicit
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
⊢ φ.implicitFunction (φ.leftFun φ.pt) (φ.rightFun x) = x → φ.leftFun x = φ.leftFun φ.pt

Tactic:
exact fun h => by rwa [← h]
-- Module: Mathlib.Analysis.Calculus.Implicit
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
rw₂ rw₃ : 𝓝 (φ.prodFun φ.pt).1 = 𝓝 (φ.prodFun φ.pt).1
⊢ map (Prod.fst ∘ φ.prodFun) (𝓝 φ.pt) = 𝓝 (φ.prodFun φ.pt).1

Tactic:
rw [← map_map, φ.hasStrictFDerivAt.map_nhds_eq_of_equiv, map_fst_nhds]

Premises used: HasStrictFDerivAt.map_nhds_eq_of_equiv, Filter.map_map, ImplicitFunctionData.hasStrictFDerivAt, map_fst_nhds
-- Module: Mathlib.Analysis.Calculus.Implicit
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
    (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)

Tactic:
have := φ.hasStrictFDerivAt.to_localInverse.comp (φ.rightFun φ.pt)
    ((hasStrictFDerivAt_const _ _).prodMk (hasStrictFDerivAt_id _))
-- Module: Mathlib.Analysis.Calculus.Implicit
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
    (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)

Tactic:
this
-- Module: Mathlib.Analysis.Calculus.Implicit
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)
h :
  fderiv 𝕜 (φ.implicitFunction (φ.leftFun φ.pt)) (φ.rightFun φ.pt) =
    (↑(φ.leftDeriv.equivProdOfSurjectiveOfIsCompl φ.rightDeriv ⋯ ⋯ ⋯).symm : F × G →L[𝕜] E).comp (σ₁₂ := RingHom.id 𝕜)
      (ContinuousLinearMap.prod 0 (ContinuousLinearMap.id 𝕜 G))
⊢ HasStrictFDerivAt (φ.implicitFunction (φ.leftFun φ.pt))
    (fderiv 𝕜 (φ.implicitFunction (φ.leftFun φ.pt)) (φ.rightFun φ.pt)) (φ.rightFun φ.pt)

Tactic:
convert! this
-- Module: Mathlib.Analysis.Calculus.Implicit
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)
⊢ fderiv 𝕜 (φ.implicitFunction (φ.leftFun φ.pt)) (φ.rightFun φ.pt) =
    (↑(φ.leftDeriv.equivProdOfSurjectiveOfIsCompl φ.rightDeriv ⋯ ⋯ ⋯).symm : F × G →L[𝕜] E).comp (σ₁₂ := RingHom.id 𝕜)
      (ContinuousLinearMap.prod 0 (ContinuousLinearMap.id 𝕜 G))

Tactic:
this.hasFDerivAt.fderiv

Premises used: ImplicitFunctionData.implicitFunction, setOf, HasStrictFDerivAt.localInverse, HasStrictFDerivAt.hasFDerivAt, ImplicitFunctionData.toOpenPartialHomeomorph, HasFDerivAt.fderiv
-- Module: Mathlib.Analysis.Calculus.Implicit
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)
⊢ fderiv 𝕜 (φ.implicitFunction (φ.leftFun φ.pt)) (φ.rightFun φ.pt) =
    (↑(φ.leftDeriv.equivProdOfSurjectiveOfIsCompl φ.rightDeriv ⋯ ⋯ ⋯).symm : F × G →L[𝕜] E).comp (σ₁₂ := RingHom.id 𝕜)
      (ContinuousLinearMap.prod 0 (ContinuousLinearMap.id 𝕜 G))

Tactic:
exact this.hasFDerivAt.fderiv

Premises used: HasStrictFDerivAt.hasFDerivAt, HasFDerivAt.fderiv
-- Module: Mathlib.Analysis.Calculus.Implicit
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
⊢ DifferentiableAt 𝕜 (φ.implicitFunction (φ.leftFun φ.pt)) (φ.rightFun φ.pt)

Tactic:
φ.hasStrictFDerivAt_implicitFunction_fderiv.hasFDerivAt.differentiableAt

Premises used: ImplicitFunctionData.hasStrictFDerivAt_implicitFunction_fderiv, HasStrictFDerivAt.hasFDerivAt, HasFDerivAt.differentiableAt
-- Module: Mathlib.Analysis.Calculus.Implicit
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
unfold :
  (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
⊢ (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

Tactic:
unfold implicitFunction Function.curry toOpenPartialHomeomorph

Premises used: ImplicitFunctionData.implicitFunction, Function.curry, ImplicitFunctionData.toOpenPartialHomeomorph