awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
E'_1 : Type u_5
inst_6 : NormedAddCommGroup E'_1
inst_7 : NormedSpace 𝕜_1 E'_1
H'_1 : Type u_6
inst_8 : TopologicalSpace H'_1
I'_1 : ModelWithCorners 𝕜_1 E'_1 H'_1
N_1 : Type u_7
inst_9 : TopologicalSpace N_1
inst_10 : ChartedSpace H'_1 N_1
𝕜 : Type u_1
inst_11 : NontriviallyNormedField 𝕜
E : Type u_2
inst_12 : NormedAddCommGroup E
inst_13 : NormedSpace 𝕜 E
H : Type u_3
inst_14 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_15 : TopologicalSpace M
inst_16 : ChartedSpace H M
E' : Type u_5
inst_17 : NormedAddCommGroup E'
inst_18 : NormedSpace 𝕜 E'
H' : Type u_6
inst_19 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_7
inst_20 : TopologicalSpace N
inst_21 : ChartedSpace H' N
f : M → N
x : M
hf : MDiffAt f x
hx : I.IsInteriorPoint x
h : IsRCLikeNormedField 𝕜
x_1 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
x_2 : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
x_3 : NormedSpace ℝ E' := NormedSpace.restrictScalars ℝ 𝕜 E'
hf' :
  Surjective.{u_2 + 1, u_5 + 1} (α := E) (β := E')
    (⇑(fderiv ℝ (writtenInExtChartAt I I' x f) ((↑(extChartAt I x) : M → E) x)) : (a : E) → E')
hf'' : DifferentiableAt ℝ (writtenInExtChartAt I I' x f) ((↑(extChartAt I x) : M → E) x)
⊢ I'.IsInteriorPoint (f x)
have refine_4 : ∀ (this : writtenInExtChartAt I I' x f ((↑(extChartAt I x) : M → E) x) ∈ interior (range (↑I' : H' → E'))),
  I'.IsInteriorPoint (f x)
Tactic: have := hf''.mem_interior_convex_of_surjective_fderiv (Filter.inter_mem ?_ ?_) I'.convex_range
    I'.isClosed_range I'.nonempty_interior (writtenInExtChartAt_mapsTo.mono_right ?_) hf'
-- 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
E'_1 : Type u_5
inst_6 : NormedAddCommGroup E'_1
inst_7 : NormedSpace 𝕜_1 E'_1
H'_1 : Type u_6
inst_8 : TopologicalSpace H'_1
I'_1 : ModelWithCorners 𝕜_1 E'_1 H'_1
N_1 : Type u_7
inst_9 : TopologicalSpace N_1
inst_10 : ChartedSpace H'_1 N_1
𝕜 : Type u_1
inst_11 : NontriviallyNormedField 𝕜
E : Type u_2
inst_12 : NormedAddCommGroup E
inst_13 : NormedSpace 𝕜 E
H : Type u_3
inst_14 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_15 : TopologicalSpace M
inst_16 : ChartedSpace H M
E' : Type u_5
inst_17 : NormedAddCommGroup E'
inst_18 : NormedSpace 𝕜 E'
H' : Type u_6
inst_19 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_7
inst_20 : TopologicalSpace N
inst_21 : ChartedSpace H' N
f : M → N
x : M
hf : MDiffAt f x
hx : I.IsInteriorPoint x
h : IsRCLikeNormedField 𝕜
x_1 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
x_2 : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
x_3 : NormedSpace ℝ E' := NormedSpace.restrictScalars ℝ 𝕜 E'
hf' :
  Surjective.{u_2 + 1, u_5 + 1} (α := E) (β := E')
    (⇑(fderiv ℝ (writtenInExtChartAt I I' x f) ((↑(extChartAt I x) : M → E) x)) : (a : E) → E')
hf'' : DifferentiableAt ℝ (writtenInExtChartAt I I' x f) ((↑(extChartAt I x) : M → E) x)
refine_4 :
  ∀ (this : writtenInExtChartAt I I' x f ((↑(extChartAt I x) : M → E) x) ∈ interior (range (↑I' : H' → E'))),
    I'.IsInteriorPoint (f x)
⊢ I'.IsInteriorPoint (f x)
have refine_1 : (extChartAt I x).target ∈ 𝓝 ((↑(extChartAt I x) : M → E) x)
Tactic: have := hf''.mem_interior_convex_of_surjective_fderiv (Filter.inter_mem ?_ ?_) I'.convex_range
    I'.isClosed_range I'.nonempty_interior (writtenInExtChartAt_mapsTo.mono_right ?_) hf'
-- 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
E'_1 : Type u_5
inst_6 : NormedAddCommGroup E'_1
inst_7 : NormedSpace 𝕜_1 E'_1
H'_1 : Type u_6
inst_8 : TopologicalSpace H'_1
I'_1 : ModelWithCorners 𝕜_1 E'_1 H'_1
N_1 : Type u_7
inst_9 : TopologicalSpace N_1
inst_10 : ChartedSpace H'_1 N_1
𝕜 : Type u_1
inst_11 : NontriviallyNormedField 𝕜
E : Type u_2
inst_12 : NormedAddCommGroup E
inst_13 : NormedSpace 𝕜 E
H : Type u_3
inst_14 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_15 : TopologicalSpace M
inst_16 : ChartedSpace H M
E' : Type u_5
inst_17 : NormedAddCommGroup E'
inst_18 : NormedSpace 𝕜 E'
H' : Type u_6
inst_19 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_7
inst_20 : TopologicalSpace N
inst_21 : ChartedSpace H' N
f : M → N
x : M
hf : MDiffAt f x
hx : I.IsInteriorPoint x
h : IsRCLikeNormedField 𝕜
x_1 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
x_2 : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
x_3 : NormedSpace ℝ E' := NormedSpace.restrictScalars ℝ 𝕜 E'
hf' :
  Surjective.{u_2 + 1, u_5 + 1} (α := E) (β := E')
    (⇑(fderiv ℝ (writtenInExtChartAt I I' x f) ((↑(extChartAt I x) : M → E) x)) : (a : E) → E')
hf'' : DifferentiableAt ℝ (writtenInExtChartAt I I' x f) ((↑(extChartAt I x) : M → E) x)
refine_4 :
  ∀ (this : writtenInExtChartAt I I' x f ((↑(extChartAt I x) : M → E) x) ∈ interior (range (↑I' : H' → E'))),
    I'.IsInteriorPoint (f x)
refine_1 : (extChartAt I x).target ∈ 𝓝 ((↑(extChartAt I x) : M → E) x)
⊢ I'.IsInteriorPoint (f x)
have refine_2 : f ∘ (↑(extChartAt I x).symm : E → M) ⁻¹' (extChartAt I' (f x)).source ∈ 𝓝 ((↑(extChartAt I x) : M → E) x)
Tactic: have := hf''.mem_interior_convex_of_surjective_fderiv (Filter.inter_mem ?_ ?_) I'.convex_range
    I'.isClosed_range I'.nonempty_interior (writtenInExtChartAt_mapsTo.mono_right ?_) hf'
-- 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
E'_1 : Type u_5
inst_6 : NormedAddCommGroup E'_1
inst_7 : NormedSpace 𝕜_1 E'_1
H'_1 : Type u_6
inst_8 : TopologicalSpace H'_1
I'_1 : ModelWithCorners 𝕜_1 E'_1 H'_1
N_1 : Type u_7
inst_9 : TopologicalSpace N_1
inst_10 : ChartedSpace H'_1 N_1
𝕜 : Type u_1
inst_11 : NontriviallyNormedField 𝕜
E : Type u_2
inst_12 : NormedAddCommGroup E
inst_13 : NormedSpace 𝕜 E
H : Type u_3
inst_14 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_15 : TopologicalSpace M
inst_16 : ChartedSpace H M
E' : Type u_5
inst_17 : NormedAddCommGroup E'
inst_18 : NormedSpace 𝕜 E'
H' : Type u_6
inst_19 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_7
inst_20 : TopologicalSpace N
inst_21 : ChartedSpace H' N
f : M → N
x : M
hf : MDiffAt f x
hx : I.IsInteriorPoint x
h : IsRCLikeNormedField 𝕜
x_1 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
x_2 : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
x_3 : NormedSpace ℝ E' := NormedSpace.restrictScalars ℝ 𝕜 E'
hf' :
  Surjective.{u_2 + 1, u_5 + 1} (α := E) (β := E')
    (⇑(fderiv ℝ (writtenInExtChartAt I I' x f) ((↑(extChartAt I x) : M → E) x)) : (a : E) → E')
hf'' : DifferentiableAt ℝ (writtenInExtChartAt I I' x f) ((↑(extChartAt I x) : M → E) x)
refine_4 :
  ∀ (this : writtenInExtChartAt I I' x f ((↑(extChartAt I x) : M → E) x) ∈ interior (range (↑I' : H' → E'))),
    I'.IsInteriorPoint (f x)
refine_1 : (extChartAt I x).target ∈ 𝓝 ((↑(extChartAt I x) : M → E) x)
refine_2 : f ∘ (↑(extChartAt I x).symm : E → M) ⁻¹' (extChartAt I' (f x)).source ∈ 𝓝 ((↑(extChartAt I x) : M → E) x)
⊢ I'.IsInteriorPoint (f x)
have refine_3 : (extChartAt I' (f x)).target ⊆ range (↑I' : H' → E')
Tactic: have := hf''.mem_interior_convex_of_surjective_fderiv (Filter.inter_mem ?_ ?_) I'.convex_range
    I'.isClosed_range I'.nonempty_interior (writtenInExtChartAt_mapsTo.mono_right ?_) hf'
-- 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
E'_1 : Type u_5
inst_6 : NormedAddCommGroup E'_1
inst_7 : NormedSpace 𝕜_1 E'_1
H'_1 : Type u_6
inst_8 : TopologicalSpace H'_1
I'_1 : ModelWithCorners 𝕜_1 E'_1 H'_1
N_1 : Type u_7
inst_9 : TopologicalSpace N_1
inst_10 : ChartedSpace H'_1 N_1
𝕜 : Type u_1
inst_11 : NontriviallyNormedField 𝕜
E : Type u_2
inst_12 : NormedAddCommGroup E
inst_13 : NormedSpace 𝕜 E
H : Type u_3
inst_14 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_15 : TopologicalSpace M
inst_16 : ChartedSpace H M
E' : Type u_5
inst_17 : NormedAddCommGroup E'
inst_18 : NormedSpace 𝕜 E'
H' : Type u_6
inst_19 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_7
inst_20 : TopologicalSpace N
inst_21 : ChartedSpace H' N
f : M → N
x : M
hf : MDiffAt f x
hx : I.IsInteriorPoint x
h : IsRCLikeNormedField 𝕜
x_1 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
x_2 : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
x_3 : NormedSpace ℝ E' := NormedSpace.restrictScalars ℝ 𝕜 E'
hf' :
  Surjective.{u_2 + 1, u_5 + 1} (α := E) (β := E')
    (⇑(fderiv ℝ (writtenInExtChartAt I I' x f) ((↑(extChartAt I x) : M → E) x)) : (a : E) → E')
hf'' : DifferentiableAt ℝ (writtenInExtChartAt I I' x f) ((↑(extChartAt I x) : M → E) x)
⊢ (extChartAt I x).target ∈ 𝓝 ((↑(extChartAt I x) : M → E) x)
have refine_1 : (extChartAt I x).target ∈ 𝓝[range (↑I : H → E)] (↑(extChartAt I x) : M → E) x
Tactic: rw [← nhdsWithin_eq_nhds.2 (mem_interior_iff_mem_nhds.1 hx)]
-- 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
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
f : M → N
x : M
hf : IsLocalDiffeomorphAt I I' n f x
⊢ I.IsInteriorPoint x ↔ I'.IsInteriorPoint (f x)
have refine_1 : ∀ (h : I.IsInteriorPoint x), I'.IsInteriorPoint (f x)
Tactic: refine ⟨fun h ↦ ?_, fun 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
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
f : M → N
x : M
hf : IsLocalDiffeomorphAt I I' n f x
refine_1 : ∀ (h : I.IsInteriorPoint x), I'.IsInteriorPoint (f x)
⊢ I.IsInteriorPoint x ↔ I'.IsInteriorPoint (f x)
have refine_2 : ∀ (h : I'.IsInteriorPoint (f x)), I.IsInteriorPoint x
Tactic: refine ⟨fun h ↦ ?_, fun 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
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
f : M → N
x : M
hf : IsLocalDiffeomorphAt I I' n f x
h : I'.IsInteriorPoint (f x)
⊢ I.IsInteriorPoint x
have refine_2 : I.IsInteriorPoint ((↑hf.localInverse.toPartialEquiv : N → M) (f x))
Tactic: rw [← hf.localInverse_left_inv hf.localInverse_mem_target]
-- 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
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
f : M → N
x : M
hf : IsLocalDiffeomorphAt I I' n f x
h : I'.IsInteriorPoint (f x)
⊢ I.IsInteriorPoint ((↑hf.localInverse.toPartialEquiv : N → M) (f x))
have refine_2 : Surjective.{u_5 + 1, u_2 + 1} (α := TangentSpace I' (f x)) (β :=
  TangentSpace I ((↑hf.localInverse.toPartialEquiv : N → M) (f x)))
  (⇑(mfderiv% (↑hf.localInverse.toPartialEquiv : N → M) (f x)) :
    (a : TangentSpace I' (f x)) → TangentSpace I ((↑hf.localInverse.toPartialEquiv : N → M) (f x)))
Tactic: refine (hf.localInverse_mdifferentiableAt hn).isInteriorPoint_of_surjective_mfderiv ?_ 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
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
f : M → N
s : Set M
hf : IsLocalDiffeomorphOn I I' n f s
⊢ f ⁻¹' ModelWithCorners.interior.{u_1, u_5, u_6, u_7} (𝕜 := 𝕜) (E := E') (H := H') (I := I') N ∩ s =
    ModelWithCorners.interior.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M ∩ s
have h : ∀ (x : M),
  x ∈ f ⁻¹' ModelWithCorners.interior.{u_1, u_5, u_6, u_7} (𝕜 := 𝕜) (E := E') (H := H') (I := I') N ∩ s ↔
    x ∈ ModelWithCorners.interior.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M ∩ s
Tactic: ext 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
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
f : M → N
s : Set M
hf : IsLocalDiffeomorphOn I I' n f s
⊢ f ⁻¹' ModelWithCorners.boundary.{u_1, u_5, u_6, u_7} (𝕜 := 𝕜) (E := E') (H := H') (I := I') N ∩ s =
    ModelWithCorners.boundary.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M ∩ s
have h : ∀ (x : M),
  x ∈ f ⁻¹' ModelWithCorners.boundary.{u_1, u_5, u_6, u_7} (𝕜 := 𝕜) (E := E') (H := H') (I := I') N ∩ s ↔
    x ∈ ModelWithCorners.boundary.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M ∩ s
Tactic: ext 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
u : Opens M
⊢ 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)
have 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
Tactic: ext1
-- 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
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'
⊢ 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
have 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
Tactic: ext p
-- 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
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'))
have rw : interior (range (↑I : H → E) ×ˢ range (↑J : H' → E')) = interior (range (↑(I.prod J) : ModelProd H H' → E × E'))
Tactic: rw [← interior_prod_eq, ← range_prodMap, modelWithCorners_prod_coe]
-- 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
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'))
⊢ interior (range (↑I : H → E)) ×ˢ interior (range (↑J : H' → E')) =
    interior (range (↑(I.prod J) : ModelProd H H' → E × E'))
have rw₁ : interior (range (Prod.map (↑I : H → E) (↑J : H' → E'))) = interior (range (↑(I.prod J) : ModelProd H H' → E × E'))
Tactic: rw [← interior_prod_eq, ← range_prodMap, modelWithCorners_prod_coe]
-- 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
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'))
⊢ interior (range (↑I : H → E)) ×ˢ interior (range (↑J : H' → E')) =
    interior (range (↑(I.prod J) : ModelProd H H' → E × E'))
have rw₂ : interior (range (Prod.map (↑I : H → E) (↑J : H' → E'))) = interior (range (Prod.map (↑I : H → E) (↑J : H' → E')))
Tactic: rw [← interior_prod_eq, ← range_prodMap, modelWithCorners_prod_coe]
-- 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
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
⊢ 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
have aux : 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]
-- 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
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'))
⊢ 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
have 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
Tactic: constructor