awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary (goal)
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
have push : ∃ (b : H), ∀ (a : E), (fderiv ℝ f x : (a : E) → H) a ≠ b
Tactic: push Not
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary (goal)
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
have refine : ∀ (z : E), Ne (α := ℝ) ((F : (a : H) → ℝ) ((fderiv ℝ f x : (a : E) → H) z : H) : ℝ) ((F : (a : H) → ℝ) (f x - y) : ℝ)
Tactic: refine ⟨f x - y, fun z ↦ ne_of_apply_ne F ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary (goal)
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
⊢ Ne (α := ℝ) ((F : (a : H) → ℝ) ((fderiv ℝ f x : (a : E) → H) z : H) : ℝ) ((F : (a : H) → ℝ) (f x - y) : ℝ)
have rw : 0 ≠ HSub.hSub (α := ℝ) (β := ℝ) ((F : (a : H) → ℝ) (f x) : ℝ) ((F : (a : H) → ℝ) y : ℝ)
Tactic: rw [h z, F.map_sub]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary (goal)
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) : ℝ)
⊢ ¬Surjective.{u_5 + 1, u_6 + 1} (α := E) (β := H) (⇑(fderiv ℝ f x) : (a : E) → H)
have suffices : ∀ (y : E), Eq (α := ℝ) ((F : (a : H) → ℝ) ((fderiv ℝ f x : (a : E) → H) y : H) : ℝ) (0 : ℝ)
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
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary (goal)
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 ℝ)
have rw : MapsTo (β := ℝ) ((⇑F : (a : H) → ℝ) : (a : H) → ℝ)
  (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior s))
  (closure (Iio ((F : (a : H) → ℝ) (f x))) : Set ℝ)
Tactic: rw [← hs'.closure_eq, ← closure_Iio, ← hs.closure_interior_eq_closure_of_nonempty_interior hs'']
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary (hypothesis)
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) : ℝ)
⊢ ∀ (y : E), Eq (α := ℝ) ((F : (a : H) → ℝ) ((fderiv ℝ f x : (a : E) → H) y : H) : ℝ) (0 : ℝ)
have hF' : 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
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary (hypothesis)
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 ℝ)
⊢ ∀ (y : E), Eq (α := ℝ) ((F : (a : H) → ℝ) ((fderiv ℝ f x : (a : E) → H) y : H) : ℝ) (0 : ℝ)
have hFφ : IsLocalMax (β := ℝ) ((⇑F : (a : H) → ℝ) ∘ f) x
Tactic: have hFφ : IsLocalMax (F ∘ f) x := Filter.eventually_of_mem hu fun y hy ↦ hF' <| hfus hy
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary (hypothesis)
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
⊢ ∀ (y : E), Eq (α := ℝ) ((F : (a : H) → ℝ) ((fderiv ℝ f x : (a : E) → H) y : H) : ℝ) (0 : ℝ)
have h : Eq (α := E →L[ℝ] ℝ) (fderiv ℝ ((⇑F : (a : H) → ℝ) ∘ f) x) 0
Tactic: have h := hFφ.fderiv_eq_zero
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary (hypothesis)
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
⊢ ∀ (y : E), Eq (α := ℝ) ((F : (a : H) → ℝ) ((fderiv ℝ f x : (a : E) → H) y : H) : ℝ) (0 : ℝ)
have h₁ : Eq (α := E →L[ℝ] ℝ) (F ∘SL fderiv ℝ f x) 0
Tactic: rw [fderiv_comp _ (by fun_prop) hf, ContinuousLinearMap.fderiv] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary (hypothesis)
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'
⊢ (↑(e'.extend I) : M → E) x ∈ interior (e'.extend I).target
have hφ : ContDiffOn 𝕜 n (↑φ : E → E) φ.source
Tactic: have hφ : ContDiffOn 𝕜 n φ φ.source := contDiffOn_extendCoordChange
    (IsManifold.subset_maximalAtlas he) (IsManifold.subset_maximalAtlas he')
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary (goal)
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'.extend I) : M → E) x ∈ interior (e'.extend I).target
have refine : Surjective (α := E) (β := E) (⇑(fderivWithin 𝕜 (↑φ : E → E) φ.source ((↑(e.extend I) : M → E) x)) : (a : E) → E)
Tactic: refine e'.mem_interior_extend_target (by simp [hex']) <| h ?_
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary (goal)
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
⊢ (↑(e'.extend I) : M → E) x ∈ interior (e'.extend I).target
have 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))
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
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary (goal)
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)
⊢ (↑(e'.extend I) : M → E) x ∈ interior (range (↑I : H → E))
have inr : ∀
  (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))),
  ¬IsRCLikeNormedField 𝕜 → (↑(e'.extend I) : M → E) x ∈ interior (range (↑I : H → E))
Tactic: wlog _ : IsRCLikeNormedField 𝕜
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary (goal)
Goal:
𝕜_1 : Type u_1
inst : NontriviallyNormedField 𝕜_1
E_1 : Type u_2
inst_1 : NormedAddCommGroup E_1
inst_2 : NormedSpace 𝕜_1 E_1
H_1 : Type u_3
inst_3 : TopologicalSpace H_1
I_1 : ModelWithCorners 𝕜_1 E_1 H_1
M_1 : Type u_4
inst_4 : TopologicalSpace M_1
inst_5 : ChartedSpace H_1 M_1
n_1 : WithTop ℕ∞
e_1 e'_1 : OpenPartialHomeomorph M_1 H_1
x_1 : M_1
𝕜 : Type u_1
inst_6 : 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 ℕ∞
inst_12 : 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)
h : IsRCLikeNormedField 𝕜
x_2 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
x_3 : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
⊢ φ.source ∈ 𝓝 ((↑(e.extend I) : M → E) x)
have simp_rw : (↑(e.extend I).symm : E → M) ⁻¹' e'.source ∈ 𝓝 ((↑(e.extend I) : M → E) x)
Tactic: simp_rw [φ, extendCoordChange, PartialEquiv.trans_source, PartialEquiv.symm_source,
      Filter.inter_mem_iff, mem_interior_iff_mem_nhds.1 hx, true_and, e'.extend_source]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary (hypothesis)
Goal:
𝕜_1 : Type u_1
inst : NontriviallyNormedField 𝕜_1
E_1 : Type u_2
inst_1 : NormedAddCommGroup E_1
inst_2 : NormedSpace 𝕜_1 E_1
H_1 : Type u_3
inst_3 : TopologicalSpace H_1
I_1 : ModelWithCorners 𝕜_1 E_1 H_1
M_1 : Type u_4
inst_4 : TopologicalSpace M_1
inst_5 : ChartedSpace H_1 M_1
n_1 : WithTop ℕ∞
e_1 e'_1 : OpenPartialHomeomorph M_1 H_1
x_1 : M_1
𝕜 : Type u_1
inst_6 : 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 ℕ∞
inst_12 : 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)
h : IsRCLikeNormedField 𝕜
x_2 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
x_3 : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
⊢ (↑(e'.extend I) : M → E) x ∈ interior (range (↑I : H → E))
have hφx : φ.source ∈ 𝓝 ((↑(e.extend I) : M → E) x)
Tactic: have hφx : φ.source ∈ 𝓝 (e.extend I x) := by
    simp_rw [φ, extendCoordChange, PartialEquiv.trans_source, PartialEquiv.symm_source,
      Filter.inter_mem_iff, mem_interior_iff_mem_nhds.1 hx, true_and, e'.extend_source]
    exact e.extend_preimage_mem_nhds hex <| e'.open_source.mem_nhds hex'
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary (hypothesis)
Goal:
𝕜_1 : Type u_1
inst : NontriviallyNormedField 𝕜_1
E_1 : Type u_2
inst_1 : NormedAddCommGroup E_1
inst_2 : NormedSpace 𝕜_1 E_1
H_1 : Type u_3
inst_3 : TopologicalSpace H_1
I_1 : ModelWithCorners 𝕜_1 E_1 H_1
M_1 : Type u_4
inst_4 : TopologicalSpace M_1
inst_5 : ChartedSpace H_1 M_1
n_1 : WithTop ℕ∞
e_1 e'_1 : OpenPartialHomeomorph M_1 H_1
x_1 : M_1
𝕜 : Type u_1
inst_6 : 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 ℕ∞
inst_12 : 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)
h : IsRCLikeNormedField 𝕜
x_2 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
x_3 : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
hφx : φ.source ∈ 𝓝 ((↑(e.extend I) : M → E) x)
⊢ (↑(e'.extend I) : M → E) x ∈ interior (range (↑I : H → E))
have hφx'₁ : Surjective (α := E) (β := E) (⇑(fderiv ℝ (↑φ : E → E) ((↑(e.extend I) : M → E) x)) : (a : E) → E)
Tactic: rw [← ContinuousLinearMap.coe_restrictScalars' (R := ℝ),
    (hφ.differentiableOn hn _ (by simp [φ, hex, hex'])).restrictScalars_fderivWithin (𝕜 := ℝ)
      (uniqueDiffWithinAt_of_mem_nhds hφx), fderivWithin_of_mem_nhds <| hφx] at hφx'
Cleared hypotheses: hφx', hφx
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary (goal)
Goal:
𝕜_1 : Type u_1
inst : NontriviallyNormedField 𝕜_1
E_1 : Type u_2
inst_1 : NormedAddCommGroup E_1
inst_2 : NormedSpace 𝕜_1 E_1
H_1 : Type u_3
inst_3 : TopologicalSpace H_1
I_1 : ModelWithCorners 𝕜_1 E_1 H_1
M_1 : Type u_4
inst_4 : TopologicalSpace M_1
inst_5 : ChartedSpace H_1 M_1
n_1 : WithTop ℕ∞
e_1 e'_1 : OpenPartialHomeomorph M_1 H_1
x_1 : M_1
𝕜 : Type u_1
inst_6 : 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 ℕ∞
inst_12 : 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 : IsRCLikeNormedField 𝕜
x_2 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
x_3 : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
hφx' : Surjective (α := E) (β := E) (⇑(fderiv ℝ (↑φ : E → E) ((↑(e.extend I) : M → E) x)) : (a : E) → E)
hφx : φ.source ∈ 𝓝 ((↑(e.extend I) : M → E) x)
⊢ (↑(e'.extend I) : M → E) x ∈ interior (range (↑I : H → E))
have rw : (↑φ : E → E) ((↑(e.extend I) : M → E) x) ∈ interior (range (↑I : H → E))
Tactic: rw [show e'.extend I x = φ (e.extend I x) by simp [φ, hex]]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary (hypothesis)
Goal:
𝕜_1 : Type u_1
inst : NontriviallyNormedField 𝕜_1
E_1 : Type u_2
inst_1 : NormedAddCommGroup E_1
inst_2 : NormedSpace 𝕜_1 E_1
H_1 : Type u_3
inst_3 : TopologicalSpace H_1
I_1 : ModelWithCorners 𝕜_1 E_1 H_1
M_1 : Type u_4
inst_4 : TopologicalSpace M_1
inst_5 : ChartedSpace H_1 M_1
n_1 : WithTop ℕ∞
e_1 e'_1 : OpenPartialHomeomorph M_1 H_1
x_1 : M_1
𝕜 : Type u_1
inst_6 : 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 ℕ∞
inst_12 : 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 : IsRCLikeNormedField 𝕜
x_2 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
x_3 : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
hφx' : Surjective (α := E) (β := E) (⇑(fderiv ℝ (↑φ : E → E) ((↑(e.extend I) : M → E) x)) : (a : E) → E)
hφx : φ.source ∈ 𝓝 ((↑(e.extend I) : M → E) x)
⊢ (↑φ : E → E) ((↑(e.extend I) : M → E) x) ∈ interior (range (↑I : H → E))
have hφ₁ : DifferentiableAt ℝ (↑φ : E → E) ((↑(e.extend I) : M → E) x)
Tactic: replace hφ := ((hφ.restrict_scalars ℝ).differentiableOn hn).differentiableAt hφx
Cleared hypotheses: hφ
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary (goal)
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
⊢ (↑(e.extend I) : M → E) x ∈ interior (e.extend I).target ↔ (↑(e'.extend I) : M → E) x ∈ interior (e'.extend I).target
have mp : (↑(e.extend I) : M → E) x ∈ interior (e.extend I).target → (↑(e'.extend I) : M → E) x ∈ interior (e'.extend I).target
Tactic: constructor