awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
Goal:
E : Type u_5
H : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup H
inst_3 : NormedSpace ℝ H
f : E → H
x : E
hf : DifferentiableAt ℝ f x
u : Set E
hu : u ∈ 𝓝 x
s : Set H
hs : Convex ℝ s
hs' : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hs'' : (interior s).Nonempty
hfus : MapsTo f u s
hfx : f x ∉ interior s
F : StrongDual ℝ H
hF : ∀ a ∈ interior s, LT.lt (α := ℝ) ((F : (a : H) → ℝ) a : ℝ) ((F : (a : H) → ℝ) (f x) : ℝ)
h : ∀ (y : E), Eq (α := ℝ) ((F : (a : H) → ℝ) ((fderiv ℝ f x : (a : E) → H) y : H) : ℝ) (0 : ℝ)
y : H
hy : y ∈ interior s
push : ∃ (b : H), ∀ (a : E), (fderiv ℝ f x : (a : E) → H) a ≠ b
⊢ ¬∀ (b : H), ∃ (a : E), (fderiv ℝ f x : (a : E) → H) a = b

Tactic:
push Not

Premises used: Not
-- Module: Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
Goal:
E : Type u_5
H : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup H
inst_3 : NormedSpace ℝ H
f : E → H
x : E
hf : DifferentiableAt ℝ f x
u : Set E
hu : u ∈ 𝓝 x
s : Set H
hs : Convex ℝ s
hs' : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hs'' : (interior s).Nonempty
hfus : MapsTo f u s
hfx : f x ∉ interior s
F : StrongDual ℝ H
hF : ∀ a ∈ interior s, LT.lt (α := ℝ) ((F : (a : H) → ℝ) a : ℝ) ((F : (a : H) → ℝ) (f x) : ℝ)
h : ∀ (y : E), Eq (α := ℝ) ((F : (a : H) → ℝ) ((fderiv ℝ f x : (a : E) → H) y : H) : ℝ) (0 : ℝ)
y : H
hy : y ∈ interior s
⊢ ∃ (b : H), ∀ (a : E), (fderiv ℝ f x : (a : E) → H) a ≠ b

Tactic:
⟨f x - y, fun z ↦ ne_of_apply_ne F ?_⟩

Premises used: HSub.hSub, ne_of_apply_ne, Exists.intro, DFunLike.coe
-- Module: Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
Goal:
E : Type u_5
H : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup H
inst_3 : NormedSpace ℝ H
f : E → H
x : E
hf : DifferentiableAt ℝ f x
u : Set E
hu : u ∈ 𝓝 x
s : Set H
hs : Convex ℝ s
hs' : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hs'' : (interior s).Nonempty
hfus : MapsTo f u s
hfx : f x ∉ interior s
F : StrongDual ℝ H
hF : ∀ a ∈ interior s, LT.lt (α := ℝ) ((F : (a : H) → ℝ) a : ℝ) ((F : (a : H) → ℝ) (f x) : ℝ)
h : ∀ (y : E), Eq (α := ℝ) ((F : (a : H) → ℝ) ((fderiv ℝ f x : (a : E) → H) y : H) : ℝ) (0 : ℝ)
y : H
hy : y ∈ interior s
refine :
  ∀ (z : E), Ne (α := ℝ) ((F : (a : H) → ℝ) ((fderiv ℝ f x : (a : E) → H) z : H) : ℝ) ((F : (a : H) → ℝ) (f x - y) : ℝ)
⊢ ∃ (b : H), ∀ (a : E), (fderiv ℝ f x : (a : E) → H) a ≠ b

Tactic:
refine ⟨f x - y, fun z ↦ ne_of_apply_ne F ?_⟩
-- Module: Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
Goal:
E : Type u_5
H : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup H
inst_3 : NormedSpace ℝ H
f : E → H
x : E
hf : DifferentiableAt ℝ f x
u : Set E
hu : u ∈ 𝓝 x
s : Set H
hs : Convex ℝ s
hs' : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hs'' : (interior s).Nonempty
hfus : MapsTo f u s
hfx : f x ∉ interior s
F : StrongDual ℝ H
hF : ∀ a ∈ interior s, LT.lt (α := ℝ) ((F : (a : H) → ℝ) a : ℝ) ((F : (a : H) → ℝ) (f x) : ℝ)
h : ∀ (y : E), Eq (α := ℝ) ((F : (a : H) → ℝ) ((fderiv ℝ f x : (a : E) → H) y : H) : ℝ) (0 : ℝ)
y : H
hy : y ∈ interior s
z : E
rw : 0 ≠ HSub.hSub (α := ℝ) (β := ℝ) ((F : (a : H) → ℝ) (f x) : ℝ) ((F : (a : H) → ℝ) y : ℝ)
⊢ Ne (α := ℝ) ((F : (a : H) → ℝ) ((fderiv ℝ f x : (a : E) → H) z : H) : ℝ) ((F : (a : H) → ℝ) (f x - y) : ℝ)

Tactic:
rw [h z, F.map_sub]

Premises used: ContinuousLinearMap.map_sub
-- Module: Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
Goal:
E : Type u_5
H : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup H
inst_3 : NormedSpace ℝ H
f : E → H
x : E
hf : DifferentiableAt ℝ f x
u : Set E
hu : u ∈ 𝓝 x
s : Set H
hs : Convex ℝ s
hs' : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hs'' : (interior s).Nonempty
hfus : MapsTo f u s
hfx : f x ∉ interior s
F : StrongDual ℝ H
hF : ∀ a ∈ interior s, LT.lt (α := ℝ) ((F : (a : H) → ℝ) a : ℝ) ((F : (a : H) → ℝ) (f x) : ℝ)
h : ∀ (y : E), Eq (α := ℝ) ((F : (a : H) → ℝ) ((fderiv ℝ f x : (a : E) → H) y : H) : ℝ) (0 : ℝ)
y : H
hy : y ∈ interior s
z : E
⊢ 0 ≠ HSub.hSub (α := ℝ) (β := ℝ) ((F : (a : H) → ℝ) (f x) : ℝ) ((F : (a : H) → ℝ) y : ℝ)

Tactic:
(sub_pos.2 <| hF _ hy).ne

Premises used: Iff.mpr, sub_pos, LT.lt.ne
-- Module: Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
Goal:
E : Type u_5
H : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup H
inst_3 : NormedSpace ℝ H
f : E → H
x : E
hf : DifferentiableAt ℝ f x
u : Set E
hu : u ∈ 𝓝 x
s : Set H
hs : Convex ℝ s
hs' : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hs'' : (interior s).Nonempty
hfus : MapsTo f u s
hfx : f x ∉ interior s
F : StrongDual ℝ H
hF : ∀ a ∈ interior s, LT.lt (α := ℝ) ((F : (a : H) → ℝ) a : ℝ) ((F : (a : H) → ℝ) (f x) : ℝ)
h : ∀ (y : E), Eq (α := ℝ) ((F : (a : H) → ℝ) ((fderiv ℝ f x : (a : E) → H) y : H) : ℝ) (0 : ℝ)
y : H
hy : y ∈ interior s
z : E
⊢ 0 ≠ HSub.hSub (α := ℝ) (β := ℝ) ((F : (a : H) → ℝ) (f x) : ℝ) ((F : (a : H) → ℝ) y : ℝ)

Tactic:
exact (sub_pos.2 <| hF _ hy).ne

Premises used: Iff.mpr, sub_pos, LT.lt.ne
-- Module: Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
Goal:
E : Type u_5
H : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup H
inst_3 : NormedSpace ℝ H
f : E → H
x : E
hf : DifferentiableAt ℝ f x
u : Set E
hu : u ∈ 𝓝 x
s : Set H
hs : Convex ℝ s
hs' : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hs'' : (interior s).Nonempty
hfus : MapsTo f u s
hfx : f x ∉ interior s
F : StrongDual ℝ H
hF : ∀ a ∈ interior s, LT.lt (α := ℝ) ((F : (a : H) → ℝ) a : ℝ) ((F : (a : H) → ℝ) (f x) : ℝ)
suffices : ∀ (y : E), Eq (α := ℝ) ((F : (a : H) → ℝ) ((fderiv ℝ f x : (a : E) → H) y : H) : ℝ) (0 : ℝ)
⊢ ¬Surjective.{u_5 + 1, u_6 + 1} (α := E) (β := H) (⇑(fderiv ℝ f x) : (a : E) → H)

Tactic:
suffices h : ∀ y, F (fderiv ℝ f x y) = 0 by
    have ⟨y, hy⟩ := hs''
    unfold Function.Surjective; push Not
    refine ⟨f x - y, fun z ↦ ne_of_apply_ne F ?_⟩
    rw [h z, F.map_sub]
    exact (sub_pos.2 <| hF _ hy).ne
-- Module: Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
Goal:
E : Type u_5
H : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup H
inst_3 : NormedSpace ℝ H
f : E → H
x : E
hf : DifferentiableAt ℝ f x
u : Set E
hu : u ∈ 𝓝 x
s : Set H
hs : Convex ℝ s
hs' : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hs'' : (interior s).Nonempty
hfus : MapsTo f u s
hfx : f x ∉ interior s
F : StrongDual ℝ H
hF : ∀ a ∈ interior s, LT.lt (α := ℝ) ((F : (a : H) → ℝ) a : ℝ) ((F : (a : H) → ℝ) (f x) : ℝ)
rw :
  MapsTo (β := ℝ) ((⇑F : (a : H) → ℝ) : (a : H) → ℝ)
    (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior s))
    (closure (Iio ((F : (a : H) → ℝ) (f x))) : Set ℝ)
⊢ MapsTo (β := ℝ) ((⇑F : (a : H) → ℝ) : (a : H) → ℝ) s (Iic ((F : (a : H) → ℝ) (f x)) : Set ℝ)

Tactic:
rw [← hs'.closure_eq, ← closure_Iio, ← hs.closure_interior_eq_closure_of_nonempty_interior hs'']

Premises used: IsClosed.closure_eq, Convex.closure_interior_eq_closure_of_nonempty_interior, closure_Iio
-- Module: Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
Goal:
E : Type u_5
H : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup H
inst_3 : NormedSpace ℝ H
f : E → H
x : E
hf : DifferentiableAt ℝ f x
u : Set E
hu : u ∈ 𝓝 x
s : Set H
hs : Convex ℝ s
hs' : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hs'' : (interior s).Nonempty
hfus : MapsTo f u s
hfx : f x ∉ interior s
F : StrongDual ℝ H
hF : ∀ a ∈ interior s, LT.lt (α := ℝ) ((F : (a : H) → ℝ) a : ℝ) ((F : (a : H) → ℝ) (f x) : ℝ)
⊢ MapsTo (β := ℝ) ((⇑F : (a : H) → ℝ) : (a : H) → ℝ)
    (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior s))
    (closure (Iio ((F : (a : H) → ℝ) (f x))) : Set ℝ)

Tactic:
.closure hF F.continuous

Premises used: Set.MapsTo.closure, ContinuousLinearMap.continuous
-- Module: Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
Goal:
E : Type u_5
H : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup H
inst_3 : NormedSpace ℝ H
f : E → H
x : E
hf : DifferentiableAt ℝ f x
u : Set E
hu : u ∈ 𝓝 x
s : Set H
hs : Convex ℝ s
hs' : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hs'' : (interior s).Nonempty
hfus : MapsTo f u s
hfx : f x ∉ interior s
F : StrongDual ℝ H
hF : ∀ a ∈ interior s, LT.lt (α := ℝ) ((F : (a : H) → ℝ) a : ℝ) ((F : (a : H) → ℝ) (f x) : ℝ)
⊢ MapsTo (β := ℝ) ((⇑F : (a : H) → ℝ) : (a : H) → ℝ)
    (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior s))
    (closure (Iio ((F : (a : H) → ℝ) (f x))) : Set ℝ)

Tactic:
exact .closure hF F.continuous
-- Module: Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
Goal:
E : Type u_5
H : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup H
inst_3 : NormedSpace ℝ H
f : E → H
x : E
hf : DifferentiableAt ℝ f x
u : Set E
hu : u ∈ 𝓝 x
s : Set H
hs : Convex ℝ s
hs' : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hs'' : (interior s).Nonempty
hfus : MapsTo f u s
hfx : f x ∉ interior s
F : StrongDual ℝ H
hF : ∀ a ∈ interior s, LT.lt (α := ℝ) ((F : (a : H) → ℝ) a : ℝ) ((F : (a : H) → ℝ) (f x) : ℝ)
⊢ MapsTo (β := ℝ) ((⇑F : (a : H) → ℝ) : (a : H) → ℝ) s (Iic ((F : (a : H) → ℝ) (f x)) : Set ℝ)

Tactic:
have hF' : MapsTo F s (Iic (F (f x))) := by
    rw [← hs'.closure_eq, ← closure_Iio, ← hs.closure_interior_eq_closure_of_nonempty_interior hs'']
    exact .closure hF F.continuous
-- Module: Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
Goal:
E : Type u_5
H : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup H
inst_3 : NormedSpace ℝ H
f : E → H
x : E
hf : DifferentiableAt ℝ f x
u : Set E
hu : u ∈ 𝓝 x
s : Set H
hs : Convex ℝ s
hs' : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hs'' : (interior s).Nonempty
hfus : MapsTo f u s
hfx : f x ∉ interior s
F : StrongDual ℝ H
hF : ∀ a ∈ interior s, LT.lt (α := ℝ) ((F : (a : H) → ℝ) a : ℝ) ((F : (a : H) → ℝ) (f x) : ℝ)
hF' : MapsTo (β := ℝ) ((⇑F : (a : H) → ℝ) : (a : H) → ℝ) s (Iic ((F : (a : H) → ℝ) (f x)) : Set ℝ)
⊢ IsLocalMax (β := ℝ) ((⇑F : (a : H) → ℝ) ∘ f) x

Tactic:
have hFφ : IsLocalMax (F ∘ f) x := Filter.eventually_of_mem hu fun y hy ↦ hF' <| hfus hy
-- Module: Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
Goal:
E : Type u_5
H : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup H
inst_3 : NormedSpace ℝ H
f : E → H
x : E
hf : DifferentiableAt ℝ f x
u : Set E
hu : u ∈ 𝓝 x
s : Set H
hs : Convex ℝ s
hs' : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hs'' : (interior s).Nonempty
hfus : MapsTo f u s
hfx : f x ∉ interior s
F : StrongDual ℝ H
hF : ∀ a ∈ interior s, LT.lt (α := ℝ) ((F : (a : H) → ℝ) a : ℝ) ((F : (a : H) → ℝ) (f x) : ℝ)
hF' : MapsTo (β := ℝ) ((⇑F : (a : H) → ℝ) : (a : H) → ℝ) s (Iic ((F : (a : H) → ℝ) (f x)) : Set ℝ)
hFφ : IsLocalMax (β := ℝ) ((⇑F : (a : H) → ℝ) ∘ f) x
⊢ Eq (α := E →L[ℝ] ℝ) (fderiv ℝ ((⇑F : (a : H) → ℝ) ∘ f) x) 0

Tactic:
have h := hFφ.fderiv_eq_zero
-- Module: Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
Goal:
E : Type u_5
H : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup H
inst_3 : NormedSpace ℝ H
f : E → H
x : E
hf : DifferentiableAt ℝ f x
u : Set E
hu : u ∈ 𝓝 x
s : Set H
hs : Convex ℝ s
hs' : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hs'' : (interior s).Nonempty
hfus : MapsTo f u s
hfx : f x ∉ interior s
F : StrongDual ℝ H
hF : ∀ a ∈ interior s, LT.lt (α := ℝ) ((F : (a : H) → ℝ) a : ℝ) ((F : (a : H) → ℝ) (f x) : ℝ)
hF' : MapsTo (β := ℝ) ((⇑F : (a : H) → ℝ) : (a : H) → ℝ) s (Iic ((F : (a : H) → ℝ) (f x)) : Set ℝ)
hFφ : IsLocalMax (β := ℝ) ((⇑F : (a : H) → ℝ) ∘ f) x
h : Eq (α := E →L[ℝ] ℝ) (fderiv ℝ ((⇑F : (a : H) → ℝ) ∘ f) x) 0
⊢ DifferentiableAt ℝ (F := ℝ) (⇑F : (a : H) → ℝ) (f x)

Tactic:
fun_prop
-- Module: Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
Goal:
E : Type u_5
H : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup H
inst_3 : NormedSpace ℝ H
f : E → H
x : E
hf : DifferentiableAt ℝ f x
u : Set E
hu : u ∈ 𝓝 x
s : Set H
hs : Convex ℝ s
hs' : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hs'' : (interior s).Nonempty
hfus : MapsTo f u s
hfx : f x ∉ interior s
F : StrongDual ℝ H
hF : ∀ a ∈ interior s, LT.lt (α := ℝ) ((F : (a : H) → ℝ) a : ℝ) ((F : (a : H) → ℝ) (f x) : ℝ)
hF' : MapsTo (β := ℝ) ((⇑F : (a : H) → ℝ) : (a : H) → ℝ) s (Iic ((F : (a : H) → ℝ) (f x)) : Set ℝ)
hFφ : IsLocalMax (β := ℝ) ((⇑F : (a : H) → ℝ) ∘ f) x
h : Eq (α := E →L[ℝ] ℝ) (fderiv ℝ ((⇑F : (a : H) → ℝ) ∘ f) x) 0
⊢ Eq (α := E →L[ℝ] ℝ) (F ∘SL fderiv ℝ f x) 0

Tactic:
rw [fderiv_comp _ (by fun_prop) hf, ContinuousLinearMap.fderiv] at h

Premises used: ContinuousLinearMap.fderiv, fderiv_comp
-- Module: Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
Goal:
E : Type u_5
H : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup H
inst_3 : NormedSpace ℝ H
f : E → H
x : E
hf : DifferentiableAt ℝ f x
u : Set E
hu : u ∈ 𝓝 x
s : Set H
hs : Convex ℝ s
hs' : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hs'' : (interior s).Nonempty
hfus : MapsTo f u s
hfx : f x ∉ interior s
F : StrongDual ℝ H
hF : ∀ a ∈ interior s, LT.lt (α := ℝ) ((F : (a : H) → ℝ) a : ℝ) ((F : (a : H) → ℝ) (f x) : ℝ)
hF' : MapsTo (β := ℝ) ((⇑F : (a : H) → ℝ) : (a : H) → ℝ) s (Iic ((F : (a : H) → ℝ) (f x)) : Set ℝ)
hFφ : IsLocalMax (β := ℝ) ((⇑F : (a : H) → ℝ) ∘ f) x
h : Eq (α := E →L[ℝ] ℝ) (F ∘SL fderiv ℝ f x) 0
⊢ ∀ (y : E), Eq (α := ℝ) ((F : (a : H) → ℝ) ((fderiv ℝ f x : (a : E) → H) y : H) : ℝ) (0 : ℝ)

Tactic:
DFunLike.congr_fun h

Premises used: DFunLike.congr_fun
-- Module: Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
Goal:
E : Type u_5
H : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup H
inst_3 : NormedSpace ℝ H
f : E → H
x : E
hf : DifferentiableAt ℝ f x
u : Set E
hu : u ∈ 𝓝 x
s : Set H
hs : Convex ℝ s
hs' : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hs'' : (interior s).Nonempty
hfus : MapsTo f u s
hfx : f x ∉ interior s
F : StrongDual ℝ H
hF : ∀ a ∈ interior s, LT.lt (α := ℝ) ((F : (a : H) → ℝ) a : ℝ) ((F : (a : H) → ℝ) (f x) : ℝ)
hF' : MapsTo (β := ℝ) ((⇑F : (a : H) → ℝ) : (a : H) → ℝ) s (Iic ((F : (a : H) → ℝ) (f x)) : Set ℝ)
hFφ : IsLocalMax (β := ℝ) ((⇑F : (a : H) → ℝ) ∘ f) x
h : Eq (α := E →L[ℝ] ℝ) (F ∘SL fderiv ℝ f x) 0
⊢ ∀ (y : E), Eq (α := ℝ) ((F : (a : H) → ℝ) ((fderiv ℝ f x : (a : E) → H) y : H) : ℝ) (0 : ℝ)

Tactic:
exact DFunLike.congr_fun h

Premises used: DFunLike.congr_fun
-- Module: Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
n : WithTop ℕ∞
inst_6 : IsManifold I n M
e e' : OpenPartialHomeomorph M H
x : M
hn : n ≠ 0
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e'
hex : x ∈ e.source
hex' : x ∈ e'.source
hx : (↑(e.extend I) : M → E) x ∈ interior (e.extend I).target
φ : PartialEquiv E E := extendCoordChange.{u_1, u_2, u_4, u_3} (𝕜 := 𝕜) (I := I) e e'
⊢ ContDiffOn 𝕜 n (↑φ : E → E) φ.source

Tactic:
have hφ : ContDiffOn 𝕜 n φ φ.source := contDiffOn_extendCoordChange
    (IsManifold.subset_maximalAtlas he) (IsManifold.subset_maximalAtlas he')
-- Module: Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
n : WithTop ℕ∞
inst_6 : IsManifold I n M
e e' : OpenPartialHomeomorph M H
x : M
hn : n ≠ 0
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e'
hex : x ∈ e.source
hex' : x ∈ e'.source
hx : (↑(e.extend I) : M → E) x ∈ interior (e.extend I).target
φ : PartialEquiv E E := extendCoordChange.{u_1, u_2, u_4, u_3} (𝕜 := 𝕜) (I := I) e e'
hφ : ContDiffOn 𝕜 n (↑φ : E → E) φ.source
h :
  Surjective (α := E) (β := E) (⇑(fderivWithin 𝕜 (↑φ : E → E) φ.source ((↑(e.extend I) : M → E) x)) : (a : E) → E) →
    (↑(e'.extend I) : M → E) x ∈ interior (range (↑I : H → E))
⊢ (↑(e'.symm.restr I.source).symm : M → H) x ∈ e'.target

Tactic:
simp [hex']
-- Module: Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
n : WithTop ℕ∞
inst_6 : IsManifold I n M
e e' : OpenPartialHomeomorph M H
x : M
hn : n ≠ 0
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e'
hex : x ∈ e.source
hex' : x ∈ e'.source
hx : (↑(e.extend I) : M → E) x ∈ interior (e.extend I).target
φ : PartialEquiv E E := extendCoordChange.{u_1, u_2, u_4, u_3} (𝕜 := 𝕜) (I := I) e e'
hφ : ContDiffOn 𝕜 n (↑φ : E → E) φ.source
h :
  Surjective (α := E) (β := E) (⇑(fderivWithin 𝕜 (↑φ : E → E) φ.source ((↑(e.extend I) : M → E) x)) : (a : E) → E) →
    (↑(e'.extend I) : M → E) x ∈ interior (range (↑I : H → E))
refine :
  Surjective (α := E) (β := E) (⇑(fderivWithin 𝕜 (↑φ : E → E) φ.source ((↑(e.extend I) : M → E) x)) : (a : E) → E)
⊢ (↑(e'.extend I) : M → E) x ∈ interior (e'.extend I).target

Tactic:
refine e'.mem_interior_extend_target (by simp [hex']) <| h ?_

Premises used: OpenPartialHomeomorph.mem_interior_extend_target
-- Module: Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
n : WithTop ℕ∞
inst_6 : IsManifold I n M
e e' : OpenPartialHomeomorph M H
x : M
hn : n ≠ 0
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e'
hex : x ∈ e.source
hex' : x ∈ e'.source
hx : (↑(e.extend I) : M → E) x ∈ interior (e.extend I).target
φ : PartialEquiv E E := extendCoordChange.{u_1, u_2, u_4, u_3} (𝕜 := 𝕜) (I := I) e e'
hφ : ContDiffOn 𝕜 n (↑φ : E → E) φ.source
h :
  Surjective (α := E) (β := E) (⇑(fderivWithin 𝕜 (↑φ : E → E) φ.source ((↑(e.extend I) : M → E) x)) : (a : E) → E) →
    (↑(e'.extend I) : M → E) x ∈ interior (range (↑I : H → E))
⊢ Membership.mem (γ := Set E) (PartialEquiv.source (extendCoordChange.{u_1, u_2, u_4, u_3} (𝕜 := 𝕜) (I := I) e e'))
    ((↑(e.extend I) : M → E) x)

Tactic:
simp [hex, hex']
-- Module: Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
n : WithTop ℕ∞
inst_6 : IsManifold I n M
e e' : OpenPartialHomeomorph M H
x : M
hn : n ≠ 0
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e'
hex : x ∈ e.source
hex' : x ∈ e'.source
hx : (↑(e.extend I) : M → E) x ∈ interior (e.extend I).target
φ : PartialEquiv E E := extendCoordChange.{u_1, u_2, u_4, u_3} (𝕜 := 𝕜) (I := I) e e'
hφ : ContDiffOn 𝕜 n (↑φ : E → E) φ.source
h :
  Surjective (α := E) (β := E) (⇑(fderivWithin 𝕜 (↑φ : E → E) φ.source ((↑(e.extend I) : M → E) x)) : (a : E) → E) →
    (↑(e'.extend I) : M → E) x ∈ interior (range (↑I : H → E))
⊢ Surjective (α := E) (β := E) (⇑(fderivWithin 𝕜 (↑φ : E → E) φ.source ((↑(e.extend I) : M → E) x)) : (a : E) → E)

Tactic:
exact (isInvertible_fderivWithin_extendCoordChange hn (IsManifold.subset_maximalAtlas he)
      (IsManifold.subset_maximalAtlas he') <| by simp [hex, hex']).surjective

Premises used: ContinuousLinearMap.IsInvertible.surjective, ModelWithCorners.isInvertible_fderivWithin_extendCoordChange, IsManifold.subset_maximalAtlas
-- Module: Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
n : WithTop ℕ∞
inst_6 : IsManifold I n M
e e' : OpenPartialHomeomorph M H
x : M
hn : n ≠ 0
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e'
hex : x ∈ e.source
hex' : x ∈ e'.source
hx : (↑(e.extend I) : M → E) x ∈ interior (e.extend I).target
φ : PartialEquiv E E := extendCoordChange.{u_1, u_2, u_4, u_3} (𝕜 := 𝕜) (I := I) e e'
hφ : ContDiffOn 𝕜 n (↑φ : E → E) φ.source
suffices :
  Surjective (α := E) (β := E) (⇑(fderivWithin 𝕜 (↑φ : E → E) φ.source ((↑(e.extend I) : M → E) x)) : (a : E) → E) →
    (↑(e'.extend I) : M → E) x ∈ interior (range (↑I : H → E))
⊢ (↑(e'.extend I) : M → E) x ∈ interior (e'.extend I).target

Tactic:
suffices h : Function.Surjective (fderivWithin 𝕜 φ φ.source (e.extend I x)) →
      e'.extend I x ∈ interior (range I) by
    refine e'.mem_interior_extend_target (by simp [hex']) <| h ?_
    exact (isInvertible_fderivWithin_extendCoordChange hn (IsManifold.subset_maximalAtlas he)
      (IsManifold.subset_maximalAtlas he') <| by simp [hex, hex']).surjective
-- Module: Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
n : WithTop ℕ∞
inst_6 : IsManifold I n M
e e' : OpenPartialHomeomorph M H
x : M
hn : n ≠ 0
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e'
hex : x ∈ e.source
hex' : x ∈ e'.source
hx : (↑(e.extend I) : M → E) x ∈ interior (e.extend I).target
φ : PartialEquiv E E := extendCoordChange.{u_1, u_2, u_4, u_3} (𝕜 := 𝕜) (I := I) e e'
hφ : ContDiffOn 𝕜 n (↑φ : E → E) φ.source
hφx' : Surjective (α := E) (β := E) (⇑(fderivWithin 𝕜 (↑φ : E → E) φ.source ((↑(e.extend I) : M → E) x)) : (a : E) → E)
this :
  ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_7 : NormedAddCommGroup E]
    [inst_8 : NormedSpace 𝕜 E] {H : Type u_3} [inst_9 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
    [inst_10 : TopologicalSpace M] [inst_11 : ChartedSpace H M] {n : WithTop ℕ∞} [IsManifold I n M]
    {e e' : OpenPartialHomeomorph M H} {x : M} (hn : n ≠ 0)
    (he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e)
    (he' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e') (hex : x ∈ e.source)
    (hex' : x ∈ e'.source) (hx : (↑(e.extend I) : M → E) x ∈ interior (e.extend I).target),
    let φ : PartialEquiv E E := extendCoordChange.{u_1, u_2, u_4, u_3} (𝕜 := 𝕜) (I := I) e e';
    ∀ (hφ : ContDiffOn 𝕜 n (↑φ : E → E) φ.source)
      (hφx' :
        Surjective (α := E) (β := E)
          (⇑(fderivWithin 𝕜 (↑φ : E → E) φ.source ((↑(e.extend I) : M → E) x)) : (a : E) → E))
      (h : IsRCLikeNormedField 𝕜), (↑(e'.extend I) : M → E) x ∈ interior (range (↑I : H → E))
h : ¬IsRCLikeNormedField 𝕜
⊢ (↑(e'.extend I) : M → E) x ∈ interior (range (↑I : H → E))

Tactic:
simp [I.range_eq_univ_of_not_isRCLikeNormedField ‹_›]

Premises used: ModelWithCorners.range_eq_univ_of_not_isRCLikeNormedField