awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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'
x : M
y : N
inst_11 : BoundarylessManifold I M
inst_12 : BoundarylessManifold J N
⊢ Eq (α := Set (M × N)) (ModelWithCorners.boundary (𝕜 := 𝕜) (E := E × E') (H := ModelProd H H') (I := I.prod J) (M × N))
    ∅
have h : Eq (α := Set (M × N)) (Set.prod univ ∅) ∅ ∧ Eq (α := Set (M × N)) (Set.prod ∅ univ) ∅
Tactic: simp only [boundary_prod, Boundaryless.boundary_eq_empty, union_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
M' : Type u_5
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
x : M
hx : I.IsInteriorPoint x
⊢ I.IsInteriorPoint (M := M ⊕ M') (Sum.inl x)
have rw : (↑(OpenPartialHomeomorph.extend (OpenPartialHomeomorph.lift_openEmbedding (chartAt H x) sorry) I) : M ⊕ M' → E)
    (Sum.inl x) ∈
  interior
    (PartialEquiv.target (α := M ⊕ M')
      (OpenPartialHomeomorph.extend (OpenPartialHomeomorph.lift_openEmbedding (chartAt H x) sorry) I))
Tactic: rw [I.isInteriorPoint_iff, extChartAt, ChartedSpace.sum_chartAt_inl]
-- 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
M' : Type u_5
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
x : M
hx : I.IsInteriorPoint x
⊢ (↑(OpenPartialHomeomorph.extend (OpenPartialHomeomorph.lift_openEmbedding (chartAt H x) ⋯) I) : M ⊕ M' → E)
      (Sum.inl x) ∈
    interior
      (PartialEquiv.target (α := M ⊕ M')
        (OpenPartialHomeomorph.extend (OpenPartialHomeomorph.lift_openEmbedding (chartAt H x) ⋯) I))
have dsimp : (↑I : H → E) (extend Sum.inl (↑(chartAt H x) : M → H) (fun (x_1 : M ⊕ M') ↦ Classical.arbitrary H) (Sum.inl x)) ∈
  interior (I.target ∩ (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target)
Tactic: dsimp
-- 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
M' : Type u_5
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
x : M
hx : I.IsInteriorPoint x
⊢ (↑I : H → E) (extend Sum.inl (↑(chartAt H x) : M → H) (fun (x_1 : M ⊕ M') ↦ Classical.arbitrary H) (Sum.inl x)) ∈
    interior (I.target ∩ (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target)
have rw : (↑I : H → E) ((↑(chartAt H x) : M → H) x) ∈
  interior (I.target ∩ (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target)
Tactic: rw [Sum.inl_injective.extend_apply (chartAt 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
M' : Type u_5
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
x : M
hx : I.IsBoundaryPoint x
⊢ I.IsBoundaryPoint (M := M ⊕ M') (Sum.inl x)
have rw : (↑(OpenPartialHomeomorph.extend (OpenPartialHomeomorph.lift_openEmbedding (chartAt H x) sorry) I) : M ⊕ M' → E)
    (Sum.inl x) ∈
  frontier (range (↑I : H → E))
Tactic: rw [I.isBoundaryPoint_iff, extChartAt, ChartedSpace.sum_chartAt_inl]
-- 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
M' : Type u_5
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
x : M
hx : I.IsBoundaryPoint x
⊢ (↑(OpenPartialHomeomorph.extend (OpenPartialHomeomorph.lift_openEmbedding (chartAt H x) ⋯) I) : M ⊕ M' → E)
      (Sum.inl x) ∈
    frontier (range (↑I : H → E))
have dsimp : (↑I : H → E) (extend Sum.inl (↑(chartAt H x) : M → H) (fun (x_1 : M ⊕ M') ↦ Classical.arbitrary H) (Sum.inl x)) ∈
  frontier (range (↑I : H → E))
Tactic: dsimp
-- 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
M' : Type u_5
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
x : M
hx : I.IsBoundaryPoint x
⊢ (↑I : H → E) (extend Sum.inl (↑(chartAt H x) : M → H) (fun (x_1 : M ⊕ M') ↦ Classical.arbitrary H) (Sum.inl x)) ∈
    frontier (range (↑I : H → E))
have rw : (↑I : H → E) ((↑(chartAt H x) : M → H) x) ∈ frontier (range (↑I : H → E))
Tactic: rw [Sum.inl_injective.extend_apply (chartAt 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
M' : Type u_5
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
x : M'
hx : I.IsInteriorPoint x
⊢ (↑(OpenPartialHomeomorph.extend (OpenPartialHomeomorph.lift_openEmbedding (chartAt H x) ⋯) I) : M ⊕ M' → E)
      (Sum.inr x) ∈
    interior
      (PartialEquiv.target (α := M ⊕ M')
        (OpenPartialHomeomorph.extend (OpenPartialHomeomorph.lift_openEmbedding (chartAt H x) ⋯) I))
have dsimp : (↑I : H → E) (extend Sum.inr (↑(chartAt H x) : M' → H) (fun (x_1 : M ⊕ M') ↦ Classical.arbitrary H) (Sum.inr x)) ∈
  interior (I.target ∩ (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target)
Tactic: dsimp
-- 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
M' : Type u_5
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
x : M'
hx : I.IsInteriorPoint x
⊢ (↑I : H → E) (extend Sum.inr (↑(chartAt H x) : M' → H) (fun (x_1 : M ⊕ M') ↦ Classical.arbitrary H) (Sum.inr x)) ∈
    interior (I.target ∩ (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target)
have rw : (↑I : H → E) ((↑(chartAt H x) : M' → H) x) ∈
  interior (I.target ∩ (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target)
Tactic: rw [Sum.inr_injective.extend_apply (chartAt 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
M' : Type u_5
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
x : M'
hx : I.IsBoundaryPoint x
⊢ I.IsBoundaryPoint (M := M ⊕ M') (Sum.inr x)
have rw : (↑(OpenPartialHomeomorph.extend (OpenPartialHomeomorph.lift_openEmbedding (chartAt H x) sorry) I) : M ⊕ M' → E)
    (Sum.inr x) ∈
  frontier (range (↑I : H → E))
Tactic: rw [I.isBoundaryPoint_iff, extChartAt, ChartedSpace.sum_chartAt_inr]
-- 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
M' : Type u_5
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
x : M'
hx : I.IsBoundaryPoint x
⊢ (↑(OpenPartialHomeomorph.extend (OpenPartialHomeomorph.lift_openEmbedding (chartAt H x) ⋯) I) : M ⊕ M' → E)
      (Sum.inr x) ∈
    frontier (range (↑I : H → E))
have dsimp : (↑I : H → E) (extend Sum.inr (↑(chartAt H x) : M' → H) (fun (x_1 : M ⊕ M') ↦ Classical.arbitrary H) (Sum.inr x)) ∈
  frontier (range (↑I : H → E))
Tactic: dsimp
-- 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
M' : Type u_5
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
x : M'
hx : I.IsBoundaryPoint x
⊢ (↑I : H → E) (extend Sum.inr (↑(chartAt H x) : M' → H) (fun (x_1 : M ⊕ M') ↦ Classical.arbitrary H) (Sum.inr x)) ∈
    frontier (range (↑I : H → E))
have rw : (↑I : H → E) ((↑(chartAt H x) : M' → H) x) ∈ frontier (range (↑I : H → E))
Tactic: rw [Sum.inr_injective.extend_apply (chartAt 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
M' : Type u_5
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
n : WithTop ℕ∞
hM : BoundarylessManifold I M
hM' : BoundarylessManifold I M'
⊢ BoundarylessManifold I (M ⊕ M')
have rw : ∀ (hM : ModelWithCorners.boundary.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M = ∅)
  (hM' : ModelWithCorners.boundary.{u_1, u_2, u_3, u_5} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M' = ∅),
  Eq (α := Set (M ⊕ M')) (ModelWithCorners.boundary (𝕜 := 𝕜) (E := E) (H := H) (I := I) (M ⊕ M')) ∅
Tactic: rw [← Boundaryless.iff_boundary_eq_empty] at hM hM' ⊢
Cleared hypotheses: hM, hM'
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalDiffeomorph (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
H : Type u_4
inst_5 : TopologicalSpace H
G : Type u_5
inst_6 : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
M : Type u_6
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
N : Type u_7
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace G N
n : WithTop ℕ∞
f : M → N
x : M
hf : IsLocalDiffeomorphAt I J n f x
⊢ f x ∈ hf.localInverse.source
have rw : (↑(Exists.choose (p := fun (Φ : PartialDiffeomorph I J M N n) ↦
            x ∈ Φ.source ∧ EqOn f (↑Φ.toPartialEquiv : M → N) Φ.source) hf).toPartialEquiv :
      M → N)
    x ∈
  hf.localInverse.source
Tactic: rw [(hf.choose_spec.2 hf.choose_spec.1)]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalDiffeomorph (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
H : Type u_4
inst_5 : TopologicalSpace H
G : Type u_5
inst_6 : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
M : Type u_6
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
N : Type u_7
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace G N
n : WithTop ℕ∞
f : M → N
x : M
hf : IsLocalDiffeomorphAt I J n f x
y : N
hy : y ∈ hf.localInverse.source
⊢ f ((↑hf.localInverse.toPartialEquiv : N → M) y) = y
have this : (↑hf.localInverse.toPartialEquiv : N → M) y ∈
  (Exists.choose (p := fun (Φ : PartialDiffeomorph I J M N n) ↦
      x ∈ Φ.source ∧ EqOn f (↑Φ.toPartialEquiv : M → N) Φ.source) hf).source
Tactic: have : hf.localInverse y ∈ hf.choose.source := by
    rw [← hf.choose.symm_target]
    exact hf.choose.symm.map_source hy
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalDiffeomorph (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
H : Type u_4
inst_5 : TopologicalSpace H
G : Type u_5
inst_6 : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
M : Type u_6
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
N : Type u_7
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace G N
n : WithTop ℕ∞
f : M → N
x : M
hf : IsLocalDiffeomorphAt I J n f x
y : N
hy : y ∈ hf.localInverse.source
this :
  (↑hf.localInverse.toPartialEquiv : N → M) y ∈
    (Exists.choose (p := fun (Φ : PartialDiffeomorph I J M N n) ↦
        x ∈ Φ.source ∧ EqOn f (↑Φ.toPartialEquiv : M → N) Φ.source) hf).source
⊢ f ((↑hf.localInverse.toPartialEquiv : N → M) y) = y
have rw : (↑(Exists.choose (p := fun (Φ : PartialDiffeomorph I J M N n) ↦
            x ∈ Φ.source ∧ EqOn f (↑Φ.toPartialEquiv : M → N) Φ.source) hf).toPartialEquiv :
      M → N)
    ((↑hf.localInverse.toPartialEquiv : N → M) y) =
  y
Tactic: rw [hf.choose_spec.2 this]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalDiffeomorph (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
H : Type u_4
inst_5 : TopologicalSpace H
G : Type u_5
inst_6 : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
M : Type u_6
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
N : Type u_7
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace G N
n : WithTop ℕ∞
f : M → N
x : M
hf : IsLocalDiffeomorphAt I J n f x
x' : M
hx' : x' ∈ hf.localInverse.target
⊢ (↑hf.localInverse.toPartialEquiv : N → M) (f x') = x'
have rw : (↑hf.localInverse.toPartialEquiv : N → M)
    ((↑(Exists.choose (p := fun (Φ : PartialDiffeomorph I J M N n) ↦
              x ∈ Φ.source ∧ EqOn f (↑Φ.toPartialEquiv : M → N) Φ.source) hf).toPartialEquiv :
        M → N)
      x') =
  x'
Tactic: rw [hf.choose_spec.2 (hf.choose.symm_target ▸ hx')]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalDiffeomorph (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
H : Type u_4
inst_5 : TopologicalSpace H
G : Type u_5
inst_6 : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
M : Type u_6
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
N : Type u_7
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace G N
n : WithTop ℕ∞
f : M → N
x : M
hf : IsLocalDiffeomorphAt I J n f x
⊢ ContMDiffAt I J n f x
have choose : ∀ (Φ : PartialDiffeomorph I J M N n) (hx : x ∈ Φ.source) (heq : EqOn f (↑Φ.toPartialEquiv : M → N) Φ.source),
  ContMDiffAt I J n f x
Tactic: choose Φ hx heq using hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalDiffeomorph (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
H : Type u_4
inst_5 : TopologicalSpace H
G : Type u_5
inst_6 : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
M : Type u_6
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
N : Type u_7
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace G N
n : WithTop ℕ∞
f : M → N
s : Set M
hf : IsLocalDiffeomorphOn I J n f s
⊢ IsLocalHomeomorphOn f s
have h : ∀ x ∈ s, ∃ (e : OpenPartialHomeomorph M N), x ∈ e.source ∧ EqOn f (↑e : M → N) e.source
Tactic: apply IsLocalHomeomorphOn.mk
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalDiffeomorph (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
H : Type u_4
inst_5 : TopologicalSpace H
G : Type u_5
inst_6 : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
M : Type u_6
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
N : Type u_7
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace G N
n : WithTop ℕ∞
f : M → N
s : Set M
hf : IsLocalDiffeomorphOn I J n f s
x : M
hx : x ∈ s
⊢ ∃ (e : OpenPartialHomeomorph M N), x ∈ e.source ∧ EqOn f (↑e : M → N) e.source
have h : ∀ (U : PartialDiffeomorph I J M N n)
  (hyp : (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ s) x hx) : M) ∈ U.source ∧ EqOn f (↑U.toPartialEquiv : M → N) U.source),
  ∃ (e : OpenPartialHomeomorph M N), x ∈ e.source ∧ EqOn f (↑e : M → N) e.source
Tactic: choose U hyp using hf ⟨x, hx⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalDiffeomorph (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
H : Type u_4
inst_5 : TopologicalSpace H
G : Type u_5
inst_6 : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
M : Type u_6
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
N : Type u_7
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace G N
n : WithTop ℕ∞
f : M → N
hf : IsLocalDiffeomorph I J n f
⊢ IsLocalHomeomorph f
have rw : IsLocalHomeomorphOn f univ
Tactic: rw [isLocalHomeomorph_iff_isLocalHomeomorphOn_univ]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalDiffeomorph (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
H : Type u_4
inst_5 : TopologicalSpace H
G : Type u_5
inst_6 : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
M : Type u_6
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
N : Type u_7
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace G N
n : WithTop ℕ∞
f : M → N
hf : IsLocalDiffeomorph I J n f
⊢ IsLocalHomeomorphOn f univ
have hf₁ : IsLocalDiffeomorphOn I J n f univ
Tactic: rw [isLocalDiffeomorph_iff_isLocalDiffeomorphOn_univ] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalDiffeomorph (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
H : Type u_4
inst_5 : TopologicalSpace H
G : Type u_5
inst_6 : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
M : Type u_6
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
N : Type u_7
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace G N
n : WithTop ℕ∞
f : M → N
s : Set M
x : M
hf : IsLocalDiffeomorph I J n f
hf' : Function.Bijective f
⊢ M ≃ₘ^n⟮I, J⟯ N
have choose : (g : N → M) → (hgInverse : Function.LeftInverse g f ∧ Function.RightInverse g f) → M ≃ₘ^n⟮I, J⟯ N
Tactic: choose g hgInverse using (Function.bijective_iff_has_inverse).mp hf'
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalDiffeomorph (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
H : Type u_4
inst_5 : TopologicalSpace H
G : Type u_5
inst_6 : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
M : Type u_6
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
N : Type u_7
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace G N
n : WithTop ℕ∞
f : M → N
s : Set M
x : M
hf : IsLocalDiffeomorph I J n f
hf' : Function.Bijective f
g : N → M
hgInverse : Function.LeftInverse g f ∧ Function.RightInverse g f
⊢ M ≃ₘ^n⟮I, J⟯ N
have choose : (Φ : (x : M) → PartialDiffeomorph I J M N n) →
  (hyp : ∀ (x : M), x ∈ (Φ x).source ∧ EqOn f (↑(Φ x).toPartialEquiv : M → N) (Φ x).source) → M ≃ₘ^n⟮I, J⟯ N
Tactic: choose Φ hyp using (fun x ↦ hf x)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalDiffeomorph (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
H : Type u_4
inst_5 : TopologicalSpace H
G : Type u_5
inst_6 : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
M : Type u_6
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
N : Type u_7
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace G N
n : WithTop ℕ∞
f : M → N
s : Set M
x : M
hf : IsLocalDiffeomorph I J n f
hf' : Function.Bijective f
g : N → M
hgInverse : Function.LeftInverse g f ∧ Function.RightInverse g f
Φ : (x : M) → PartialDiffeomorph I J M N n
hyp : ∀ (x : M), x ∈ (Φ x).source ∧ EqOn f (↑(Φ x).toPartialEquiv : M → N) (Φ x).source
⊢ M ≃ₘ^n⟮I, J⟯ N
have aux : ∀ (x : M), EqOn g (↑(Φ x).symm.toPartialEquiv : N → M) (Φ x).target
Tactic: have aux (x) : EqOn g (Φ x).symm (Φ x).target :=
    eqOn_of_leftInvOn_of_rightInvOn (fun x' _ ↦ hgInverse.1 x')
      (LeftInvOn.congr_left ((Φ x).toOpenPartialHomeomorph).rightInvOn
        ((Φ x).toOpenPartialHomeomorph).symm_mapsTo (hyp x).2.symm)
      (fun _y hy ↦ (Φ x).map_target hy)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalDiffeomorph (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
H : Type u_4
inst_5 : TopologicalSpace H
G : Type u_5
inst_6 : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
M : Type u_6
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
N : Type u_7
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace G N
n : WithTop ℕ∞
f : M → N
s : Set M
x_1 : M
hf : IsLocalDiffeomorph I J n f
hf' : Function.Bijective f
g : N → M
hgInverse : Function.LeftInverse g f ∧ Function.RightInverse g f
Φ : (x : M) → PartialDiffeomorph I J M N n
hyp : ∀ (x : M), x ∈ (Φ x).source ∧ EqOn f (↑(Φ x).toPartialEquiv : M → N) (Φ x).source
aux : ∀ (x : M), EqOn g (↑(Φ x).symm.toPartialEquiv : N → M) (Φ x).target
y : N
x : M := g y
⊢ ContMDiffAt.{u_1, u_3, u_5, u_7, u_2, u_4, u_6} J I (M' := M) n
    (⇑{ toFun := f, invFun := g, left_inv := ⋯, right_inv := ⋯ : M ≃ N }.symm : (a : N) → M) y
have hx : x ∈ (Φ x).source
Tactic: obtain ⟨hx, hfx⟩ := hyp x