awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_7
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace H' N
n : WithTop ℕ∞
hn : n ≠ 0
Φ : M ≃ₘ^n⟮I, I'⟯ N
⊢ (⇑Φ : (a : M) → N) ⁻¹' ModelWithCorners.boundary.{u_1, u_5, u_6, u_7} (𝕜 := 𝕜) (E := E') (H := H') (I := I') N =
    ModelWithCorners.boundary.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M

Tactic:
Φ.isLocalDiffeomorph.preimage_boundary hn

Premises used: Diffeomorph.isLocalDiffeomorph, IsLocalDiffeomorph.preimage_boundary
-- 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
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_7
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace H' N
n : WithTop ℕ∞
hn : n ≠ 0
Φ : M ≃ₘ^n⟮I, I'⟯ N
⊢ (⇑Φ : (a : M) → N) '' ModelWithCorners.interior.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M =
    ModelWithCorners.interior.{u_1, u_5, u_6, u_7} (𝕜 := 𝕜) (E := E') (H := H') (I := I') N

Tactic:
(Φ.eq_preimage_iff_image_eq _ _).1 (Φ.preimage_interior hn).symm

Premises used: Diffeomorph.preimage_interior, Equiv.eq_preimage_iff_image_eq, Diffeomorph.toEquiv, Iff.mp, Eq.symm
-- 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
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_7
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace H' N
n : WithTop ℕ∞
hn : n ≠ 0
Φ : M ≃ₘ^n⟮I, I'⟯ N
⊢ (⇑Φ : (a : M) → N) '' ModelWithCorners.boundary.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M =
    ModelWithCorners.boundary.{u_1, u_5, u_6, u_7} (𝕜 := 𝕜) (E := E') (H := H') (I := I') N

Tactic:
(Φ.eq_preimage_iff_image_eq _ _).1 (Φ.preimage_boundary hn).symm

Premises used: Equiv.eq_preimage_iff_image_eq, Diffeomorph.toEquiv, Iff.mp, Eq.symm, Diffeomorph.preimage_boundary
-- 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
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_7
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace H' N
n : WithTop ℕ∞
hn : n ≠ 0
Φ : M ≃ₘ^n⟮I, I'⟯ N
inst_11 : BoundarylessManifold I M
⊢ BoundarylessManifold I' N

Tactic:
Φ.symm.isLocalDiffeomorph.boundarylessManifold hn

Premises used: Diffeomorph.symm, IsLocalDiffeomorph.boundarylessManifold, Diffeomorph.isLocalDiffeomorph
-- 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
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_7
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace H' N
n : WithTop ℕ∞
hn : n ≠ 0
Φ : M ≃ₘ^n⟮I, I'⟯ N
⊢ BoundarylessManifold I M ↔ BoundarylessManifold I' N

Tactic:
⟨fun _ ↦ Φ.boundarylessManifold hn, fun _ ↦ Φ.symm.boundarylessManifold hn⟩

Premises used: Diffeomorph.symm, Iff.intro, Diffeomorph.boundarylessManifold
-- 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
u : Opens M
x : ↥u
⊢ I.IsInteriorPoint x ↔ I.IsInteriorPoint (↑x : M)

Tactic:
simpa [I.isInteriorPoint_iff, u.chartAt_eq,
    OpenPartialHomeomorph.subtypeRestr, mem_interior_iff_mem_nhds] using
    fun _ _ ↦ (chartAt H x.1).extend_preimage_mem_nhds (mem_chart_source H x.1) (u.2.mem_nhds x.2)

Premises used: TopologicalSpace.Opens.chartAt_eq, mem_chart_source, OpenPartialHomeomorph.subtypeRestr, mem_interior_iff_mem_nhds, chartAt, OpenPartialHomeomorph.extend_preimage_mem_nhds, IsOpen.mem_nhds, ModelWithCorners.isInteriorPoint_iff, TopologicalSpace.Opens.is_open', Subtype.val, Subtype.property
-- 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
u : Opens M
x : ↥u
⊢ I.IsBoundaryPoint x ↔ I.IsBoundaryPoint (↑x : M)

Tactic:
simpa [I.isInteriorPoint_iff_not_isBoundaryPoint, not_iff_not] using
    I.isInteriorPoint_iff_isInteriorPoint_val

Premises used: not_iff_not, ModelWithCorners.isInteriorPoint_iff_isInteriorPoint_val, ModelWithCorners.isInteriorPoint_iff_not_isBoundaryPoint
-- 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
u : Opens M
h :
  ∀ (x : ↥u),
    Membership.mem (γ := Set ↥u) (ModelWithCorners.interior.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) ↥u)
        x ↔
      Membership.mem (γ := Set ↥u)
        (Subtype.val (p := fun (x : M) ↦ x ∈ u) ⁻¹'
          ModelWithCorners.interior.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M)
        x
⊢ Eq (α := Set ↥u) (ModelWithCorners.interior.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) ↥u)
    (Subtype.val (p := fun (x : M) ↦ x ∈ u) ⁻¹'
      ModelWithCorners.interior.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M)

Tactic:
ext1
-- 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
u : Opens M
x : ↥u
⊢ Membership.mem (γ := Set ↥u) (ModelWithCorners.interior.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) ↥u)
      x ↔
    Membership.mem (γ := Set ↥u)
      (Subtype.val (p := fun (x : M) ↦ x ∈ u) ⁻¹'
        ModelWithCorners.interior.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M)
      x

Tactic:
I.isInteriorPoint_iff_isInteriorPoint_val

Premises used: ModelWithCorners.IsInteriorPoint, Set.Mem, ModelWithCorners.interior, ModelWithCorners.isInteriorPoint_iff_isInteriorPoint_val, setOf, Set.sUnion, Set.preimage, interior
-- 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
u : Opens M
x : ↥u
⊢ Membership.mem (γ := Set ↥u) (ModelWithCorners.interior.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) ↥u)
      x ↔
    Membership.mem (γ := Set ↥u)
      (Subtype.val (p := fun (x : M) ↦ x ∈ u) ⁻¹'
        ModelWithCorners.interior.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M)
      x

Tactic:
exact I.isInteriorPoint_iff_isInteriorPoint_val

Premises used: ModelWithCorners.isInteriorPoint_iff_isInteriorPoint_val
-- 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
u : Opens M
⊢ Eq (α := Set ↥u) (ModelWithCorners.boundary.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) ↥u)
    (Subtype.val (p := fun (x : M) ↦ x ∈ u) ⁻¹'
      ModelWithCorners.boundary.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M)

Tactic:
simp [← I.compl_interior, I.interior_open]

Premises used: ModelWithCorners.interior_open, ModelWithCorners.compl_interior
-- 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
inst_6 : BoundarylessManifold I M
u : Opens M
⊢ BoundarylessManifold.{u_1, u_2, u_3, u_4} I ↥u

Tactic:
⟨fun _ ↦ I.isInteriorPoint_iff_isInteriorPoint_val.2 BoundarylessManifold.isInteriorPoint⟩

Premises used: Iff.mpr, BoundarylessManifold.isInteriorPoint, ModelWithCorners.isInteriorPoint_iff_isInteriorPoint_val, BoundarylessManifold.mk
-- 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
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
N : Type u_7
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace H' N
J : ModelWithCorners 𝕜 E' H'
h :
  ∀ (p : M × N),
    Membership.mem (γ := Set (M × N))
        (ModelWithCorners.interior (𝕜 := 𝕜) (E := E × E') (H := ModelProd H H') (I := I.prod J) (M × N)) p ↔
      p ∈
        ModelWithCorners.interior.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M ×ˢ
          ModelWithCorners.interior.{u_1, u_5, u_6, u_7} (𝕜 := 𝕜) (E := E') (H := H') (I := J) N
⊢ ModelWithCorners.interior (𝕜 := 𝕜) (E := E × E') (H := ModelProd H H') (I := I.prod J) (M × N) =
    ModelWithCorners.interior.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M ×ˢ
      ModelWithCorners.interior.{u_1, u_5, u_6, u_7} (𝕜 := 𝕜) (E := E') (H := H') (I := J) N

Tactic:
ext p
-- 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
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
N : Type u_7
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace H' N
J : ModelWithCorners 𝕜 E' H'
p : M × N
rw : interior (range (↑I : H → E) ×ˢ range (↑J : H' → E')) = interior (range (↑(I.prod J) : ModelProd H H' → E × E'))
rw₁ : interior (range (Prod.map (↑I : H → E) (↑J : H' → E'))) = interior (range (↑(I.prod J) : ModelProd H H' → E × E'))
rw₂ rw₃ :
  interior (range (Prod.map (↑I : H → E) (↑J : H' → E'))) = interior (range (Prod.map (↑I : H → E) (↑J : H' → E')))
⊢ interior (range (↑I : H → E)) ×ˢ interior (range (↑J : H' → E')) =
    interior (range (↑(I.prod J) : ModelProd H H' → E × E'))

Tactic:
rw [← interior_prod_eq, ← range_prodMap, modelWithCorners_prod_coe]

Premises used: modelWithCorners_prod_coe, interior_prod_eq, Set.range_prodMap
-- 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
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
N : Type u_7
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace H' N
J : ModelWithCorners 𝕜 E' H'
p : M × N
⊢ interior (range (↑I : H → E)) ×ˢ interior (range (↑J : H' → E')) =
    interior (range (↑(I.prod J) : ModelProd H H' → E × E'))

Tactic:
have aux : (interior (range ↑I)) ×ˢ (interior (range J)) = interior (range (I.prod J)) := by
    rw [← interior_prod_eq, ← range_prodMap, modelWithCorners_prod_coe]
-- 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
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
N : Type u_7
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace H' N
J : ModelWithCorners 𝕜 E' H'
p : M × N
aux :
  interior (range (↑I : H → E)) ×ˢ interior (range (↑J : H' → E')) =
    interior (range (↑(I.prod J) : ModelProd H H' → E × E'))
h :
  Membership.mem (γ := Set (M × N))
      (ModelWithCorners.interior (𝕜 := 𝕜) (E := E × E') (H := ModelProd H H') (I := I.prod J) (M × N)) p →
    p ∈
      ModelWithCorners.interior.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M ×ˢ
        ModelWithCorners.interior.{u_1, u_5, u_6, u_7} (𝕜 := 𝕜) (E := E') (H := H') (I := J) N
h₁ :
  p ∈
      ModelWithCorners.interior.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M ×ˢ
        ModelWithCorners.interior.{u_1, u_5, u_6, u_7} (𝕜 := 𝕜) (E := E') (H := H') (I := J) N →
    Membership.mem (γ := Set (M × N))
      (ModelWithCorners.interior (𝕜 := 𝕜) (E := E × E') (H := ModelProd H H') (I := I.prod J) (M × N)) p
⊢ Membership.mem (γ := Set (M × N))
      (ModelWithCorners.interior (𝕜 := 𝕜) (E := E × E') (H := ModelProd H H') (I := I.prod J) (M × N)) p ↔
    p ∈
      ModelWithCorners.interior.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M ×ˢ
        ModelWithCorners.interior.{u_1, u_5, u_6, u_7} (𝕜 := 𝕜) (E := E') (H := H') (I := J) N

Tactic:
constructor
-- 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
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
N : Type u_7
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace H' N
J : ModelWithCorners 𝕜 E' H'
p : M × N
aux :
  interior (range (↑I : H → E)) ×ˢ interior (range (↑J : H' → E')) =
    interior (range (↑(I.prod J) : ModelProd H H' → E × E'))
hp :
  Membership.mem (γ := Set (M × N))
    (ModelWithCorners.interior (𝕜 := 𝕜) (E := E × E') (H := ModelProd H H') (I := I.prod J) (M × N)) p
⊢ (I.prod J).IsInteriorPoint p

Tactic:
replace hp : (I.prod J).IsInteriorPoint p := hp
-- 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
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
N : Type u_7
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace H' N
J : ModelWithCorners 𝕜 E' H'
p : M × N
aux :
  interior (range (↑I : H → E)) ×ˢ interior (range (↑J : H' → E')) =
    interior (range (↑(I.prod J) : ModelProd H H' → E × E'))
hp : (I.prod J).IsInteriorPoint p
⊢ (↑(extChartAt (I.prod J) p) : M × N → E × E') p ∈ interior (range (↑I : H → E)) ×ˢ interior (range (↑J : H' → E'))

Tactic:
rw [IsInteriorPoint, ← aux] at hp

Premises used: ModelWithCorners.IsInteriorPoint
-- 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
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
N : Type u_7
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace H' N
J : ModelWithCorners 𝕜 E' H'
p : M × N
aux :
  interior (range (↑I : H → E)) ×ˢ interior (range (↑J : H' → E')) =
    interior (range (↑(I.prod J) : ModelProd H H' → E × E'))
hp : (↑(extChartAt (I.prod J) p) : M × N → E × E') p ∈ interior (range (↑I : H → E)) ×ˢ interior (range (↑J : H' → E'))
⊢ p ∈
    ModelWithCorners.interior.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M ×ˢ
      ModelWithCorners.interior.{u_1, u_5, u_6, u_7} (𝕜 := 𝕜) (E := E') (H := H') (I := J) N

Tactic:
hp

Premises used: ModelWithCorners.IsInteriorPoint, Set.Mem, ModelWithCorners.interior, setOf, Set.prod, Set.sUnion, ModelWithCorners.toFun', interior
-- 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
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
N : Type u_7
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace H' N
J : ModelWithCorners 𝕜 E' H'
p : M × N
aux :
  interior (range (↑I : H → E)) ×ˢ interior (range (↑J : H' → E')) =
    interior (range (↑(I.prod J) : ModelProd H H' → E × E'))
hp : (↑(extChartAt (I.prod J) p) : M × N → E × E') p ∈ interior (range (↑I : H → E)) ×ˢ interior (range (↑J : H' → E'))
⊢ p ∈
    ModelWithCorners.interior.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M ×ˢ
      ModelWithCorners.interior.{u_1, u_5, u_6, u_7} (𝕜 := 𝕜) (E := E') (H := H') (I := J) N

Tactic:
exact hp
-- 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
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
N : Type u_7
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace H' N
J : ModelWithCorners 𝕜 E' H'
p : M × N
aux :
  interior (range (↑I : H → E)) ×ˢ interior (range (↑J : H' → E')) =
    interior (range (↑(I.prod J) : ModelProd H H' → E × E'))
hp :
  p ∈
    ModelWithCorners.interior.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M ×ˢ
      ModelWithCorners.interior.{u_1, u_5, u_6, u_7} (𝕜 := 𝕜) (E := E') (H := H') (I := J) N
h : (I.prod J).IsInteriorPoint p
⊢ Membership.mem (γ := Set (M × N))
    (ModelWithCorners.interior (𝕜 := 𝕜) (E := E × E') (H := ModelProd H H') (I := I.prod J) (M × N)) p

Tactic:
change (I.prod J).IsInteriorPoint p

Premises used: ModelWithCorners.IsInteriorPoint, ModelWithCorners.prod
-- 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
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
N : Type u_7
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace H' N
J : ModelWithCorners 𝕜 E' H'
p : M × N
aux :
  interior (range (↑I : H → E)) ×ˢ interior (range (↑J : H' → E')) =
    interior (range (↑(I.prod J) : ModelProd H H' → E × E'))
hp :
  p ∈
    ModelWithCorners.interior.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M ×ˢ
      ModelWithCorners.interior.{u_1, u_5, u_6, u_7} (𝕜 := 𝕜) (E := E') (H := H') (I := J) N
h :
  ((↑(extChartAt (I.prod J) p) : M × N → E × E') p).1 ∈ interior (range (↑I : H → E)) ∧
    ((↑(extChartAt (I.prod J) p) : M × N → E × E') p).2 ∈ interior (range (↑J : H' → E'))
⊢ (I.prod J).IsInteriorPoint p

Tactic:
rw [IsInteriorPoint, ← aux, mem_prod]

Premises used: ModelWithCorners.IsInteriorPoint, Set.mem_prod
-- 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
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
N : Type u_7
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace H' N
J : ModelWithCorners 𝕜 E' H'
p : M × N
aux :
  interior (range (↑I : H → E)) ×ˢ interior (range (↑J : H' → E')) =
    interior (range (↑(I.prod J) : ModelProd H H' → E × E'))
hp :
  p ∈
    ModelWithCorners.interior.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M ×ˢ
      ModelWithCorners.interior.{u_1, u_5, u_6, u_7} (𝕜 := 𝕜) (E := E') (H := H') (I := J) N
⊢ p.1 ∈ ModelWithCorners.interior.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M ∧
    p.2 ∈ ModelWithCorners.interior.{u_1, u_5, u_6, u_7} (𝕜 := 𝕜) (E := E') (H := H') (I := J) N

Tactic:
obtain h := Set.mem_prod.mp hp

Premises used: Set.mem_prod, Iff.mp
-- 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
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
N : Type u_7
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace H' N
J : ModelWithCorners 𝕜 E' H'
p : M × N
aux :
  interior (range (↑I : H → E)) ×ˢ interior (range (↑J : H' → E')) =
    interior (range (↑(I.prod J) : ModelProd H H' → E × E'))
hp :
  p ∈
    ModelWithCorners.interior.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M ×ˢ
      ModelWithCorners.interior.{u_1, u_5, u_6, u_7} (𝕜 := 𝕜) (E := E') (H := H') (I := J) N
h :
  p.1 ∈ ModelWithCorners.interior.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M ∧
    p.2 ∈ ModelWithCorners.interior.{u_1, u_5, u_6, u_7} (𝕜 := 𝕜) (E := E') (H := H') (I := J) N
⊢ Membership.mem (γ := Set M) {x : M | I.IsInteriorPoint x} p.1 ∧
    p.2 ∈ ModelWithCorners.interior.{u_1, u_5, u_6, u_7} (𝕜 := 𝕜) (E := E') (H := H') (I := J) N

Tactic:
rw [ModelWithCorners.interior] at h

Premises used: ModelWithCorners.interior