awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.ExtChartAt (goal)
Goal:
E : Type u_8
𝕜 : Type u_9
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_10
inst_3 : TopologicalSpace H
M : Type u_11
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
I : ModelWithCorners 𝕜 E H
inst_6 : LocallyCompactSpace M
x : M
y : E
hy : y ∈ interior (extChartAt I x).target
h'y : y ∈ (extChartAt I x).target
⊢ LocallyCompactSpace E
have obtain : ∀ (s : Set M) (hmem : s ∈ 𝓝 ((↑(extChartAt I x).symm : E → M) y)) (hss : s ⊆ (extChartAt I x).source)
  (hcom : IsCompact s), LocallyCompactSpace E
Tactic: obtain ⟨s, hmem, hss, hcom⟩ :=
    LocallyCompactSpace.local_compact_nhds ((extChartAt I x).symm y) (extChartAt I x).source
      ((isOpen_extChartAt_source x).mem_nhds ((extChartAt I x).map_target h'y))
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.ExtChartAt (hypothesis)
Goal:
E : Type u_8
𝕜 : Type u_9
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_10
inst_3 : TopologicalSpace H
M : Type u_11
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
I : ModelWithCorners 𝕜 E H
inst_6 : LocallyCompactSpace M
x : M
y : E
hy : y ∈ interior (extChartAt I x).target
h'y : y ∈ (extChartAt I x).target
s : Set M
hmem : s ∈ 𝓝 ((↑(extChartAt I x).symm : E → M) y)
hss : s ⊆ (extChartAt I x).source
hcom : IsCompact s
⊢ LocallyCompactSpace E
have this : IsCompact ((↑(extChartAt I x) : M → E) '' s)
Tactic: have : IsCompact <| (extChartAt I x) '' s :=
    hcom.image_of_continuousOn <| (continuousOn_extChartAt x).mono hss
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.ExtChartAt (goal)
Goal:
E : Type u_8
𝕜 : Type u_9
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_10
inst_3 : TopologicalSpace H
M : Type u_11
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
I : ModelWithCorners 𝕜 E H
inst_6 : LocallyCompactSpace M
x : M
y : E
hy : y ∈ interior (extChartAt I x).target
h'y : y ∈ (extChartAt I x).target
s : Set M
hmem : s ∈ 𝓝 ((↑(extChartAt I x).symm : E → M) y)
hss : s ⊆ (extChartAt I x).source
hcom : IsCompact s
this : IsCompact ((↑(extChartAt I x) : M → E) '' s)
⊢ LocallyCompactSpace E
have apply : (↑(extChartAt I x) : M → E) '' s ∈ 𝓝 y
Tactic: apply this.locallyCompactSpace_of_mem_nhds_of_addGroup (x := y)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.ExtChartAt (goal)
Goal:
E : Type u_8
𝕜 : Type u_9
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_10
inst_3 : TopologicalSpace H
M : Type u_11
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
I : ModelWithCorners 𝕜 E H
inst_6 : LocallyCompactSpace M
x : M
y : E
hy : y ∈ interior (extChartAt I x).target
h'y : y ∈ (extChartAt I x).target
s : Set M
hmem : s ∈ 𝓝 ((↑(extChartAt I x).symm : E → M) y)
hss : s ⊆ (extChartAt I x).source
hcom : IsCompact s
this : IsCompact ((↑(extChartAt I x) : M → E) '' s)
⊢ (↑(extChartAt I x) : M → E) '' s ∈ 𝓝 y
have rw : (↑(extChartAt I x) : M → E) '' s ∈ 𝓝 ((↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y))
Tactic: rw [← (extChartAt I x).right_inv h'y]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.ExtChartAt (goal)
Goal:
E : Type u_8
𝕜 : Type u_9
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_10
inst_3 : TopologicalSpace H
M : Type u_11
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
I : ModelWithCorners 𝕜 E H
inst_6 : LocallyCompactSpace M
x : M
y : E
hy : y ∈ interior (extChartAt I x).target
h'y : y ∈ (extChartAt I x).target
s : Set M
hmem : s ∈ 𝓝 ((↑(extChartAt I x).symm : E → M) y)
hss : s ⊆ (extChartAt I x).source
hcom : IsCompact s
this : IsCompact ((↑(extChartAt I x) : M → E) '' s)
⊢ (↑(extChartAt I x) : M → E) '' s ∈ 𝓝 ((↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y))
have apply : (↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y) ∈ interior (range (↑I : H → E))
Tactic: apply extChartAt_image_nhds_mem_nhds_of_mem_interior_range
    (PartialEquiv.map_target (extChartAt I x) h'y) _ hmem
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.ExtChartAt (goal)
Goal:
E : Type u_8
𝕜 : Type u_9
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_10
inst_3 : TopologicalSpace H
M : Type u_11
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
I : ModelWithCorners 𝕜 E H
inst_6 : LocallyCompactSpace M
x : M
y : E
hy : y ∈ interior (extChartAt I x).target
h'y : y ∈ (extChartAt I x).target
s : Set M
hmem : s ∈ 𝓝 ((↑(extChartAt I x).symm : E → M) y)
hss : s ⊆ (extChartAt I x).source
hcom : IsCompact s
this : IsCompact ((↑(extChartAt I x) : M → E) '' s)
⊢ (↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y) ∈ interior (range (↑I : H → E))
have simp : y ∈ interior (range (↑I : H → E))
Tactic: simp only [(extChartAt I x).right_inv h'y]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.ExtChartAt (hypothesis)
Goal:
E : Type u_8
𝕜 : Type u_9
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_10
inst_3 : TopologicalSpace H
M : Type u_11
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
inst_6 : CompleteSpace 𝕜
I : ModelWithCorners 𝕜 E H
inst_7 : Nonempty M
inst_8 : LocallyCompactSpace M
⊢ FiniteDimensional 𝕜 E
have this : LocallyCompactSpace E
Tactic: have := LocallyCompactSpace.of_locallyCompact_manifold M I
-- 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
x : M
⊢ I.IsInteriorPoint x ∨ I.IsBoundaryPoint x
have rw : (↑(extChartAt I x) : M → E) x ∉ interior (range (↑I : H → E)) →
  (↑(extChartAt I x) : M → E) x ∈ range (↑I : H → E) ∧ (↑(extChartAt I x) : M → E) x ∉ interior (range (↑I : H → E))
Tactic: rw [IsInteriorPoint, or_iff_not_imp_left, I.isBoundaryPoint_iff, ← closure_diff_interior,
    I.isClosed_range.closure_eq, mem_diff]
-- 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
⊢ Disjoint (ModelWithCorners.interior.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M)
    (ModelWithCorners.boundary.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M)
have by_contra : ∀
  (h :
    ¬Disjoint (ModelWithCorners.interior.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M)
        (ModelWithCorners.boundary.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M)),
  False
Tactic: by_contra 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
h :
  ¬Disjoint (ModelWithCorners.interior.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M)
      (ModelWithCorners.boundary.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M)
⊢ False
have obtain : ∀ (x : M) (h1 : x ∈ ModelWithCorners.interior.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M)
  (h2 : x ∈ ModelWithCorners.boundary.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M), False
Tactic: obtain ⟨x, h1, h2⟩ := not_disjoint_iff.mp 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
h :
  ¬Disjoint (ModelWithCorners.interior.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M)
      (ModelWithCorners.boundary.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M)
x : M
h1 : x ∈ ModelWithCorners.interior.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M
h2 : x ∈ ModelWithCorners.boundary.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M
⊢ False
have rw : (↑(extChartAt I x) : M → E) x ∈ interior (range (↑I : H → E)) ∧
  (↑(extChartAt I x) : M → E) x ∈ frontier (range (↑I : H → E))
Tactic: rw [← mem_empty_iff_false (extChartAt I x x),
    ← disjoint_iff_inter_eq_empty.mp disjoint_interior_frontier, mem_inter_iff]
-- 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
h :
  ¬Disjoint (ModelWithCorners.interior.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M)
      (ModelWithCorners.boundary.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M)
x : M
h1 : x ∈ ModelWithCorners.interior.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M
h2 : x ∈ ModelWithCorners.boundary.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M
rw :
  (↑(extChartAt I x) : M → E) x ∈ interior (range (↑I : H → E)) ∧
    (↑(extChartAt I x) : M → E) x ∈ frontier (range (↑I : H → E))
⊢ False
have rw₁ : Set E
Tactic: rw [← mem_empty_iff_false (extChartAt I x x),
    ← disjoint_iff_inter_eq_empty.mp disjoint_interior_frontier, mem_inter_iff]
-- 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
x : M
⊢ I.IsInteriorPoint x ↔ ¬I.IsBoundaryPoint x
have refine : I.IsInteriorPoint x → ¬I.IsBoundaryPoint x
Tactic: refine ⟨?_,
    by simpa only [or_iff_not_imp_right] using isInteriorPoint_or_isBoundaryPoint x (I := I)⟩
-- 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
x : M
⊢ I.IsInteriorPoint x → ¬I.IsBoundaryPoint x
have by_contra! : ∀ (h : I.IsInteriorPoint x ∧ I.IsBoundaryPoint x), False
Tactic: by_contra! 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
x : M
h : I.IsInteriorPoint x ∧ I.IsBoundaryPoint x
⊢ False
have rw : (↑(extChartAt I x) : M → E) x ∈ interior (range (↑I : H → E)) ∧
  (↑(extChartAt I x) : M → E) x ∈ frontier (range (↑I : H → E))
Tactic: rw [← mem_empty_iff_false (extChartAt I x x),
    ← disjoint_iff_inter_eq_empty.mp disjoint_interior_frontier, mem_inter_iff]
-- 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
x : M
h : I.IsInteriorPoint x ∧ I.IsBoundaryPoint x
rw :
  (↑(extChartAt I x) : M → E) x ∈ interior (range (↑I : H → E)) ∧
    (↑(extChartAt I x) : M → E) x ∈ frontier (range (↑I : H → E))
⊢ False
have rw₁ : Set E
Tactic: rw [← mem_empty_iff_false (extChartAt I x x),
    ← disjoint_iff_inter_eq_empty.mp disjoint_interior_frontier, mem_inter_iff]
-- 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
⊢ (ModelWithCorners.interior.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M)ᶜ =
    ModelWithCorners.boundary.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M
have apply : ModelWithCorners.interior.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M ⊓
    ModelWithCorners.boundary.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M =
  ⊥
Tactic: apply compl_unique ?_ I.interior_union_boundary_eq_univ
-- 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
⊢ (ModelWithCorners.boundary.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M)ᶜ =
    ModelWithCorners.interior.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M
have rw : (ModelWithCorners.interior.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M)ᶜᶜ =
  ModelWithCorners.interior.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M
Tactic: rw [← compl_interior, compl_compl]
-- 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
rw :
  (ModelWithCorners.interior.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M)ᶜᶜ =
    ModelWithCorners.interior.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M
⊢ (ModelWithCorners.boundary.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M)ᶜ =
    ModelWithCorners.interior.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M
have rw₁ : ModelWithCorners.interior.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M =
  ModelWithCorners.interior.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M
Tactic: rw [← compl_interior, compl_compl]
-- 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
x : M
h : I.IsInteriorPoint x
⊢ range (↑I : H → E) ∈ 𝓝 ((↑(extChartAt I x) : M → E) x)
have rw : ∃ t ⊆ range (↑I : H → E),
  IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t ∧ (↑(extChartAt I x) : M → E) x ∈ t
Tactic: rw [mem_nhds_iff]
-- 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
inst_6 : I.Boundaryless
x : M
r : interior (OpenPartialHomeomorph.extend (chartAt H x) I).target =
  (OpenPartialHomeomorph.extend (chartAt H x) I).target :=
  ⋯
⊢ I.IsInteriorPoint x
have this : extChartAt I x = OpenPartialHomeomorph.extend (chartAt H x) I
Tactic: have : extChartAt I x = (chartAt H x).extend I := rfl
-- 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
inst_6 : I.Boundaryless
x : M
r : interior (OpenPartialHomeomorph.extend (chartAt H x) I).target =
  (OpenPartialHomeomorph.extend (chartAt H x) I).target :=
  ⋯
this : extChartAt I x = OpenPartialHomeomorph.extend (chartAt H x) I
⊢ I.IsInteriorPoint x
have r₁ : interior (extChartAt I x).target = (extChartAt I x).target
Tactic: rw [← this] at r
Cleared hypotheses: r, this
-- 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
inst_6 : I.Boundaryless
x : M
r : interior (extChartAt I x).target = (extChartAt I x).target
this : extChartAt I x = OpenPartialHomeomorph.extend (chartAt H x) I
⊢ I.IsInteriorPoint x
have rw : (↑(extChartAt I x) : M → E) x ∈ (extChartAt I x).target
Tactic: rw [isInteriorPoint_iff, r]
-- 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
inst_6 : BoundarylessManifold I M
⊢ ModelWithCorners.boundary.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M = ∅
have rw : (ModelWithCorners.interior.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M)ᶜ = ∅
Tactic: rw [← I.compl_interior, I.interior_eq_univ, compl_empty_iff]
-- 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
inst_6 : BoundarylessManifold I M
rw : (ModelWithCorners.interior.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M)ᶜ = ∅
⊢ ModelWithCorners.boundary.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M = ∅
have rw₁ : Eq.{u_4 + 1} (α := Set M) univᶜ ∅
Tactic: rw [← I.compl_interior, I.interior_eq_univ, compl_empty_iff]
-- 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
inst_6 : BoundarylessManifold I M
rw : (ModelWithCorners.interior.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M)ᶜ = ∅
rw₁ : Eq.{u_4 + 1} (α := Set M) univᶜ ∅
⊢ ModelWithCorners.boundary.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M = ∅
have rw₂ : Eq.{u_4 + 1} (α := Set M) univ univ
Tactic: rw [← I.compl_interior, I.interior_eq_univ, compl_empty_iff]
-- 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
⊢ ModelWithCorners.boundary.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M = ∅ ↔ BoundarylessManifold I M
have refine : ∀ (h : ModelWithCorners.boundary.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M = ∅) (x : M),
  I.IsInteriorPoint x
Tactic: refine ⟨fun h ↦ { isInteriorPoint' := ?_ }, fun a ↦ boundary_eq_empty⟩
-- 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
h : ModelWithCorners.boundary.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M = ∅
x : M
⊢ x ∈ ModelWithCorners.interior.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M
have rw : ∀ (h : ModelWithCorners.interior.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M = univ) (x : M),
  x ∈ ModelWithCorners.interior.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M
Tactic: rw [← compl_interior, compl_empty_iff] at h
Cleared hypotheses: h, x
-- 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
h : ModelWithCorners.interior.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M = univ
x : M
⊢ x ∈ ModelWithCorners.interior.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M
have rw : Membership.mem (γ := Set M) univ x
Tactic: rw [h]
-- 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 : Surjective.{u_5 + 1, u_6 + 1} (α := E) (β := H) (⇑(fderiv ℝ f x) : (a : E) → H)
⊢ f x ∈ interior s
have contrapose : ∀ (hfx : f x ∉ interior s), ¬Surjective.{u_5 + 1, u_6 + 1} (α := E) (β := H) (⇑(fderiv ℝ f x) : (a : E) → H)
Tactic: contrapose hfx
Cleared hypotheses: hfx
-- 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
⊢ ¬Surjective.{u_5 + 1, u_6 + 1} (α := E) (β := H) (⇑(fderiv ℝ f x) : (a : E) → H)
have have : ∀ (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)
Tactic: have ⟨F, hF⟩ := geometric_hahn_banach_open_point hs.interior isOpen_interior hfx
-- 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 : ℝ)
⊢ ¬Surjective.{u_5 + 1, u_6 + 1} (α := E) (β := H) (⇑(fderiv ℝ f x) : (a : E) → H)
have have : ∀ (y : H) (hy : y ∈ interior s), ¬Surjective.{u_5 + 1, u_6 + 1} (α := E) (β := H) (⇑(fderiv ℝ f x) : (a : E) → H)
Tactic: have ⟨y, hy⟩ := hs''