awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ChartedSpace (goal)
Goal:
H : Type u
H' : Type u_1
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : TopologicalSpace M'
cm : ChartedSpace H M
cm' : ChartedSpace H M'
inst_3 : Nonempty H
x w : M'
⊢ Membership.mem (γ := Set (M ⊕ M'))
    (PartialEquiv.source (β := H) (toPartialEquiv (lift_openEmbedding (ChartedSpace.chartAt x) ⋯))) (Sum.inr x)
have left : x ∈ PartialEquiv.source.{u_3, u} (β := H) (toPartialEquiv (ChartedSpace.chartAt x))
Tactic: use x, cm'.mem_chart_source x
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ChartedSpace (goal)
Goal:
H : Type u
H' : Type u_1
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : TopologicalSpace M'
cm : ChartedSpace H M
cm' : ChartedSpace H M'
inst_3 : Nonempty H
x w : M'
left : x ∈ PartialEquiv.source.{u_3, u} (β := H) (toPartialEquiv (ChartedSpace.chartAt x))
⊢ Membership.mem (γ := Set (M ⊕ M'))
    (PartialEquiv.source (β := H) (toPartialEquiv (lift_openEmbedding (ChartedSpace.chartAt x) ⋯))) (Sum.inr x)
have right : Eq (α := M ⊕ M') (Sum.inr x) (Sum.inr x)
Tactic: use x, cm'.mem_chart_source x
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ChartedSpace (goal)
Goal:
H : Type u
H' : Type u_1
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : TopologicalSpace M'
cm : ChartedSpace H M
cm' : ChartedSpace H M'
inst_3 : Nonempty H
p : M ⊕ M'
⊢ Membership.mem (γ := Set (M ⊕ M'))
    (PartialEquiv.source (β := H)
      (toPartialEquiv
        (Sum.elim (fun (x : M) ↦ lift_openEmbedding (ChartedSpace.chartAt x) ⋯)
          (fun (x : M') ↦ lift_openEmbedding (ChartedSpace.chartAt x) ⋯) p)))
    p
have inl : ∀ (x : M),
  Membership.mem (γ := Set (M ⊕ M'))
    (PartialEquiv.source (β := H)
      (toPartialEquiv
        (Sum.elim (fun (x : M) ↦ lift_openEmbedding (ChartedSpace.chartAt x) sorry)
          (fun (x : M') ↦ lift_openEmbedding (ChartedSpace.chartAt x) sorry) (Sum.inl x))))
    (Sum.inl x)
Tactic: cases p with
    | inl x =>
      rw [Sum.elim_inl, lift_openEmbedding_source,
        ← OpenPartialHomeomorph.lift_openEmbedding_source _ IsOpenEmbedding.inl]
      use x, cm.mem_chart_source x
    | inr x =>
      rw [Sum.elim_inr, lift_openEmbedding_source,
        ← OpenPartialHomeomorph.lift_openEmbedding_source _ IsOpenEmbedding.inr]
      use x, cm'.mem_chart_source x
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ChartedSpace (goal)
Goal:
H : Type u
H' : Type u_1
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : TopologicalSpace M'
cm : ChartedSpace H M
cm' : ChartedSpace H M'
inst_3 : Nonempty H
p : M ⊕ M'
inl :
  ∀ (x : M),
    Membership.mem (γ := Set (M ⊕ M'))
      (PartialEquiv.source (β := H)
        (toPartialEquiv
          (Sum.elim (fun (x : M) ↦ lift_openEmbedding (ChartedSpace.chartAt x) ⋯)
            (fun (x : M') ↦ lift_openEmbedding (ChartedSpace.chartAt x) ⋯) (Sum.inl x))))
      (Sum.inl x)
⊢ Membership.mem (γ := Set (M ⊕ M'))
    (PartialEquiv.source (β := H)
      (toPartialEquiv
        (Sum.elim (fun (x : M) ↦ lift_openEmbedding (ChartedSpace.chartAt x) ⋯)
          (fun (x : M') ↦ lift_openEmbedding (ChartedSpace.chartAt x) ⋯) p)))
    p
have inr : ∀ (x : M'),
  Membership.mem (γ := Set (M ⊕ M'))
    (PartialEquiv.source (β := H)
      (toPartialEquiv
        (Sum.elim (fun (x : M) ↦ lift_openEmbedding (ChartedSpace.chartAt x) sorry)
          (fun (x : M') ↦ lift_openEmbedding (ChartedSpace.chartAt x) sorry) (Sum.inr x))))
    (Sum.inr x)
Tactic: cases p with
    | inl x =>
      rw [Sum.elim_inl, lift_openEmbedding_source,
        ← OpenPartialHomeomorph.lift_openEmbedding_source _ IsOpenEmbedding.inl]
      use x, cm.mem_chart_source x
    | inr x =>
      rw [Sum.elim_inr, lift_openEmbedding_source,
        ← OpenPartialHomeomorph.lift_openEmbedding_source _ IsOpenEmbedding.inr]
      use x, cm'.mem_chart_source x
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ChartedSpace (goal)
Goal:
H : Type u
H' : Type u_1
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : TopologicalSpace M'
cm : ChartedSpace H M
cm' : ChartedSpace H M'
inst_3 : Nonempty H
x : M
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph (M ⊕ M') H))
    ((fun (e : OpenPartialHomeomorph M H) ↦ e.lift_openEmbedding ⋯) '' ChartedSpace.atlas ∪
      (fun (e : OpenPartialHomeomorph M' H) ↦ e.lift_openEmbedding ⋯) '' ChartedSpace.atlas)
    (lift_openEmbedding (ChartedSpace.chartAt x) ⋯)
have inl : Membership.mem (γ := Set (OpenPartialHomeomorph (M ⊕ M') H))
  ((fun (e : OpenPartialHomeomorph M H) ↦ e.lift_openEmbedding sorry) '' ChartedSpace.atlas)
  (lift_openEmbedding (ChartedSpace.chartAt x) sorry)
Tactic: left
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ChartedSpace (goal)
Goal:
H : Type u
H' : Type u_1
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : TopologicalSpace M'
cm : ChartedSpace H M
cm' : ChartedSpace H M'
inst_3 : Nonempty H
x : M
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph (M ⊕ M') H))
    ((fun (e : OpenPartialHomeomorph M H) ↦ e.lift_openEmbedding ⋯) '' ChartedSpace.atlas)
    (lift_openEmbedding (ChartedSpace.chartAt x) ⋯)
have w : OpenPartialHomeomorph M H
Tactic: use ChartedSpace.chartAt x, cm.chart_mem_atlas x
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ChartedSpace (goal)
Goal:
H : Type u
H' : Type u_1
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : TopologicalSpace M'
cm : ChartedSpace H M
cm' : ChartedSpace H M'
inst_3 : Nonempty H
x : M
w : OpenPartialHomeomorph M H
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph (M ⊕ M') H))
    ((fun (e : OpenPartialHomeomorph M H) ↦ e.lift_openEmbedding ⋯) '' ChartedSpace.atlas)
    (lift_openEmbedding (ChartedSpace.chartAt x) ⋯)
have left : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) ChartedSpace.atlas (ChartedSpace.chartAt x)
Tactic: use ChartedSpace.chartAt x, cm.chart_mem_atlas x
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ChartedSpace (goal)
Goal:
H : Type u
H' : Type u_1
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : TopologicalSpace M'
cm : ChartedSpace H M
cm' : ChartedSpace H M'
inst_3 : Nonempty H
x : M
w : OpenPartialHomeomorph M H
left : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) ChartedSpace.atlas (ChartedSpace.chartAt x)
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph (M ⊕ M') H))
    ((fun (e : OpenPartialHomeomorph M H) ↦ e.lift_openEmbedding ⋯) '' ChartedSpace.atlas)
    (lift_openEmbedding (ChartedSpace.chartAt x) ⋯)
have right : Eq (α := OpenPartialHomeomorph (M ⊕ M') H)
  ((fun (e : OpenPartialHomeomorph M H) ↦ (e.lift_openEmbedding sorry : OpenPartialHomeomorph (M ⊕ M') H))
    (ChartedSpace.chartAt x))
  (lift_openEmbedding (ChartedSpace.chartAt x) sorry)
Tactic: use ChartedSpace.chartAt x, cm.chart_mem_atlas x
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ChartedSpace (goal)
Goal:
H : Type u
H' : Type u_1
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : TopologicalSpace M'
cm : ChartedSpace H M
cm' : ChartedSpace H M'
inst_3 : Nonempty H
x : M'
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph (M ⊕ M') H))
    ((fun (e : OpenPartialHomeomorph M H) ↦ e.lift_openEmbedding ⋯) '' ChartedSpace.atlas ∪
      (fun (e : OpenPartialHomeomorph M' H) ↦ e.lift_openEmbedding ⋯) '' ChartedSpace.atlas)
    (lift_openEmbedding (ChartedSpace.chartAt x) ⋯)
have inr : Membership.mem (γ := Set (OpenPartialHomeomorph (M ⊕ M') H))
  ((fun (e : OpenPartialHomeomorph M' H) ↦ e.lift_openEmbedding sorry) '' ChartedSpace.atlas)
  (lift_openEmbedding (ChartedSpace.chartAt x) sorry)
Tactic: right
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ChartedSpace (goal)
Goal:
H : Type u
H' : Type u_1
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : TopologicalSpace M'
cm : ChartedSpace H M
cm' : ChartedSpace H M'
inst_3 : Nonempty H
x : M'
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph (M ⊕ M') H))
    ((fun (e : OpenPartialHomeomorph M' H) ↦ e.lift_openEmbedding ⋯) '' ChartedSpace.atlas)
    (lift_openEmbedding (ChartedSpace.chartAt x) ⋯)
have w : OpenPartialHomeomorph M' H
Tactic: use ChartedSpace.chartAt x, cm'.chart_mem_atlas x
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ChartedSpace (goal)
Goal:
H : Type u
H' : Type u_1
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : TopologicalSpace M'
cm : ChartedSpace H M
cm' : ChartedSpace H M'
inst_3 : Nonempty H
x : M'
w : OpenPartialHomeomorph M' H
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph (M ⊕ M') H))
    ((fun (e : OpenPartialHomeomorph M' H) ↦ e.lift_openEmbedding ⋯) '' ChartedSpace.atlas)
    (lift_openEmbedding (ChartedSpace.chartAt x) ⋯)
have left : Membership.mem (γ := Set (OpenPartialHomeomorph M' H)) ChartedSpace.atlas (ChartedSpace.chartAt x)
Tactic: use ChartedSpace.chartAt x, cm'.chart_mem_atlas x
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ChartedSpace (goal)
Goal:
H : Type u
H' : Type u_1
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : TopologicalSpace M'
cm : ChartedSpace H M
cm' : ChartedSpace H M'
inst_3 : Nonempty H
x : M'
w : OpenPartialHomeomorph M' H
left : Membership.mem (γ := Set (OpenPartialHomeomorph M' H)) ChartedSpace.atlas (ChartedSpace.chartAt x)
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph (M ⊕ M') H))
    ((fun (e : OpenPartialHomeomorph M' H) ↦ e.lift_openEmbedding ⋯) '' ChartedSpace.atlas)
    (lift_openEmbedding (ChartedSpace.chartAt x) ⋯)
have right : Eq (α := OpenPartialHomeomorph (M ⊕ M') H)
  ((fun (e : OpenPartialHomeomorph M' H) ↦ (e.lift_openEmbedding sorry : OpenPartialHomeomorph (M ⊕ M') H))
    (ChartedSpace.chartAt x))
  (lift_openEmbedding (ChartedSpace.chartAt x) sorry)
Tactic: use ChartedSpace.chartAt x, cm'.chart_mem_atlas x
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ChartedSpace (goal)
Goal:
H : Type u
H' : Type u_1
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : TopologicalSpace M'
cm : ChartedSpace H M
cm' : ChartedSpace H M'
inst_3 : Nonempty H
p : M ⊕ M'
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph (M ⊕ M') H))
    ((fun (e : OpenPartialHomeomorph M H) ↦ e.lift_openEmbedding ⋯) '' ChartedSpace.atlas ∪
      (fun (e : OpenPartialHomeomorph M' H) ↦ e.lift_openEmbedding ⋯) '' ChartedSpace.atlas)
    (Sum.elim (fun (x : M) ↦ lift_openEmbedding (ChartedSpace.chartAt x) ⋯)
      (fun (x : M') ↦ lift_openEmbedding (ChartedSpace.chartAt x) ⋯) p)
have inl : ∀ (x : M),
  Membership.mem (γ := Set (OpenPartialHomeomorph (M ⊕ M') H))
    ((fun (e : OpenPartialHomeomorph M H) ↦ e.lift_openEmbedding sorry) '' ChartedSpace.atlas ∪
      (fun (e : OpenPartialHomeomorph M' H) ↦ e.lift_openEmbedding sorry) '' ChartedSpace.atlas)
    (Sum.elim (fun (x : M) ↦ lift_openEmbedding (ChartedSpace.chartAt x) sorry)
      (fun (x : M') ↦ lift_openEmbedding (ChartedSpace.chartAt x) sorry) (Sum.inl x))
Tactic: cases p with
    | inl x =>
      rw [Sum.elim_inl]
      left
      use ChartedSpace.chartAt x, cm.chart_mem_atlas x
    | inr x =>
      rw [Sum.elim_inr]
      right
      use ChartedSpace.chartAt x, cm'.chart_mem_atlas x
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ChartedSpace (goal)
Goal:
H : Type u
H' : Type u_1
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : TopologicalSpace M'
cm : ChartedSpace H M
cm' : ChartedSpace H M'
inst_3 : Nonempty H
p : M ⊕ M'
inl :
  ∀ (x : M),
    Membership.mem (γ := Set (OpenPartialHomeomorph (M ⊕ M') H))
      ((fun (e : OpenPartialHomeomorph M H) ↦ e.lift_openEmbedding ⋯) '' ChartedSpace.atlas ∪
        (fun (e : OpenPartialHomeomorph M' H) ↦ e.lift_openEmbedding ⋯) '' ChartedSpace.atlas)
      (Sum.elim (fun (x : M) ↦ lift_openEmbedding (ChartedSpace.chartAt x) ⋯)
        (fun (x : M') ↦ lift_openEmbedding (ChartedSpace.chartAt x) ⋯) (Sum.inl x))
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph (M ⊕ M') H))
    ((fun (e : OpenPartialHomeomorph M H) ↦ e.lift_openEmbedding ⋯) '' ChartedSpace.atlas ∪
      (fun (e : OpenPartialHomeomorph M' H) ↦ e.lift_openEmbedding ⋯) '' ChartedSpace.atlas)
    (Sum.elim (fun (x : M) ↦ lift_openEmbedding (ChartedSpace.chartAt x) ⋯)
      (fun (x : M') ↦ lift_openEmbedding (ChartedSpace.chartAt x) ⋯) p)
have inr : ∀ (x : M'),
  Membership.mem (γ := Set (OpenPartialHomeomorph (M ⊕ M') H))
    ((fun (e : OpenPartialHomeomorph M H) ↦ e.lift_openEmbedding sorry) '' ChartedSpace.atlas ∪
      (fun (e : OpenPartialHomeomorph M' H) ↦ e.lift_openEmbedding sorry) '' ChartedSpace.atlas)
    (Sum.elim (fun (x : M) ↦ lift_openEmbedding (ChartedSpace.chartAt x) sorry)
      (fun (x : M') ↦ lift_openEmbedding (ChartedSpace.chartAt x) sorry) (Sum.inr x))
Tactic: cases p with
    | inl x =>
      rw [Sum.elim_inl]
      left
      use ChartedSpace.chartAt x, cm.chart_mem_atlas x
    | inr x =>
      rw [Sum.elim_inr]
      right
      use ChartedSpace.chartAt x, cm'.chart_mem_atlas x
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ChartedSpace (goal)
Goal:
H : Type u
H' : Type u_1
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : TopologicalSpace M'
cm : ChartedSpace H M
cm' : ChartedSpace H M'
⊢ ChartedSpace H (M ⊕ M')
have pos : (h : Nonempty H) → ChartedSpace H (M ⊕ M')
Tactic: by_cases! h : Nonempty H
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ChartedSpace (goal)
Goal:
H : Type u
H' : Type u_1
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : TopologicalSpace M'
cm : ChartedSpace H M
cm' : ChartedSpace H M'
pos : (h : Nonempty H) → ChartedSpace H (M ⊕ M')
⊢ ChartedSpace H (M ⊕ M')
have neg : (h : IsEmpty H) → ChartedSpace H (M ⊕ M')
Tactic: by_cases! h : Nonempty H
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ChartedSpace (hypothesis)
Goal:
H : Type u
H' : Type u_1
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : TopologicalSpace M'
cm : ChartedSpace H M
cm' : ChartedSpace H M'
h : IsEmpty H
⊢ ChartedSpace H (M ⊕ M')
have this : IsEmpty M
Tactic: have : IsEmpty M := isEmpty_of_chartedSpace H
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ChartedSpace (hypothesis)
Goal:
H : Type u
H' : Type u_1
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : TopologicalSpace M'
cm : ChartedSpace H M
cm' : ChartedSpace H M'
h : IsEmpty H
this : IsEmpty M
⊢ ChartedSpace H (M ⊕ M')
have this₁ : IsEmpty M'
Tactic: have : IsEmpty M' := isEmpty_of_chartedSpace H
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ChartedSpace (goal)
Goal:
H : Type u
M : Type u_2
M' : Type u_3
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : TopologicalSpace M'
cm : ChartedSpace H M
cm' : ChartedSpace H M'
x : M
⊢ Eq (α := OpenPartialHomeomorph (M ⊕ M') H) (chartAt H (Sum.inl x)) (lift_openEmbedding (chartAt H x) ⋯)
have simp : Eq (α := OpenPartialHomeomorph (M ⊕ M') H) (ChartedSpace.chartAt (Sum.inl x))
  (lift_openEmbedding (ChartedSpace.chartAt x) sorry)
Tactic: simp +instances only [chartAt, sum, nonempty_of_chartedSpace x, ↓reduceDIte]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ChartedSpace (goal)
Goal:
H : Type u
M : Type u_2
M' : Type u_3
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : TopologicalSpace M'
cm : ChartedSpace H M
cm' : ChartedSpace H M'
x' : M'
⊢ Eq (α := OpenPartialHomeomorph (M ⊕ M') H) (chartAt H (Sum.inr x')) (lift_openEmbedding (chartAt H x') ⋯)
have simp : Eq (α := OpenPartialHomeomorph (M ⊕ M') H) (ChartedSpace.chartAt (Sum.inr x'))
  (lift_openEmbedding (ChartedSpace.chartAt x') sorry)
Tactic: simp +instances only [chartAt, sum, nonempty_of_chartedSpace x', ↓reduceDIte]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ChartedSpace (hypothesis)
Goal:
H : Type u
M : Type u_2
M' : Type u_3
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : TopologicalSpace M'
cm : ChartedSpace H M
cm' : ChartedSpace H M'
x y : M
⊢ (↑(chartAt H (Sum.inl x)) : M ⊕ M' → H) (Sum.inl y) = (↑(chartAt H x) : M → H) y
have this : Nonempty H
Tactic: haveI : Nonempty H := nonempty_of_chartedSpace x
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ChartedSpace (goal)
Goal:
H : Type u
M : Type u_2
M' : Type u_3
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : TopologicalSpace M'
cm : ChartedSpace H M
cm' : ChartedSpace H M'
x y : M
this : Nonempty H
⊢ (↑(chartAt H (Sum.inl x)) : M ⊕ M' → H) (Sum.inl y) = (↑(chartAt H x) : M → H) y
have rw : (↑(lift_openEmbedding (chartAt H x) sorry) : M ⊕ M' → H) (Sum.inl y) = (↑(chartAt H x) : M → H) y
Tactic: rw [ChartedSpace.sum_chartAt_inl]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ChartedSpace (hypothesis)
Goal:
H : Type u
M : Type u_2
M' : Type u_3
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : TopologicalSpace M'
cm : ChartedSpace H M
cm' : ChartedSpace H M'
x y : M'
⊢ (↑(chartAt H (Sum.inr x)) : M ⊕ M' → H) (Sum.inr y) = (↑(chartAt H x) : M' → H) y
have this : Nonempty H
Tactic: haveI : Nonempty H := nonempty_of_chartedSpace x
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ChartedSpace (goal)
Goal:
H : Type u
M : Type u_2
M' : Type u_3
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : TopologicalSpace M'
cm : ChartedSpace H M
cm' : ChartedSpace H M'
x y : M'
this : Nonempty H
⊢ (↑(chartAt H (Sum.inr x)) : M ⊕ M' → H) (Sum.inr y) = (↑(chartAt H x) : M' → H) y
have rw : (↑(lift_openEmbedding (chartAt H x) sorry) : M ⊕ M' → H) (Sum.inr y) = (↑(chartAt H x) : M' → H) y
Tactic: rw [ChartedSpace.sum_chartAt_inr]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ChartedSpace (hypothesis)
Goal:
H : Type u
M : Type u_2
M' : Type u_3
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : TopologicalSpace M'
cm : ChartedSpace H M
cm' : ChartedSpace H M'
h : Nonempty H
e : OpenPartialHomeomorph (M ⊕ M') H
he : Membership.mem (γ := Set (OpenPartialHomeomorph (M ⊕ M') H)) (atlas H (M ⊕ M')) e
⊢ (∃ (f : OpenPartialHomeomorph M H),
      Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) f ∧ e = f.lift_openEmbedding ⋯) ∨
    ∃ (f' : OpenPartialHomeomorph M' H),
      Membership.mem (γ := Set (OpenPartialHomeomorph M' H)) (atlas H M') f' ∧ e = f'.lift_openEmbedding ⋯
have he₁ : Membership.mem (γ := Set (OpenPartialHomeomorph (M ⊕ M') H)) ChartedSpace.atlas e
Tactic: simp +instances only [atlas, sum, h, ↓reduceDIte] at he
Cleared hypotheses: he
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ChartedSpace (goal)
Goal:
H : Type u
M : Type u_2
M' : Type u_3
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : TopologicalSpace M'
cm : ChartedSpace H M
cm' : ChartedSpace H M'
h : Nonempty H
e : OpenPartialHomeomorph (M ⊕ M') H
he : Membership.mem (γ := Set (OpenPartialHomeomorph (M ⊕ M') H)) ChartedSpace.atlas e
⊢ (∃ (f : OpenPartialHomeomorph M H),
      Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) f ∧ e = f.lift_openEmbedding ⋯) ∨
    ∃ (f' : OpenPartialHomeomorph M' H),
      Membership.mem (γ := Set (OpenPartialHomeomorph M' H)) (atlas H M') f' ∧ e = f'.lift_openEmbedding ⋯
have inl : ∀ (x : OpenPartialHomeomorph M H) (hx : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) ChartedSpace.atlas x)
  (hxe : (fun (e : OpenPartialHomeomorph M H) ↦ (e.lift_openEmbedding sorry : OpenPartialHomeomorph (M ⊕ M') H)) x = e),
  (∃ (f : OpenPartialHomeomorph M H),
      Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) f ∧ e = f.lift_openEmbedding sorry) ∨
    ∃ (f' : OpenPartialHomeomorph M' H),
      Membership.mem (γ := Set (OpenPartialHomeomorph M' H)) (atlas H M') f' ∧ e = f'.lift_openEmbedding sorry
Tactic: obtain (⟨x, hx, hxe⟩ | ⟨x, hx, hxe⟩) := he
Cleared hypotheses: he
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ChartedSpace (goal)
Goal:
H : Type u
M : Type u_2
M' : Type u_3
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : TopologicalSpace M'
cm : ChartedSpace H M
cm' : ChartedSpace H M'
h : Nonempty H
e : OpenPartialHomeomorph (M ⊕ M') H
he : Membership.mem (γ := Set (OpenPartialHomeomorph (M ⊕ M') H)) ChartedSpace.atlas e
inl :
  ∀ (x : OpenPartialHomeomorph M H) (hx : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) ChartedSpace.atlas x)
    (hxe : (fun (e : OpenPartialHomeomorph M H) ↦ (e.lift_openEmbedding ⋯ : OpenPartialHomeomorph (M ⊕ M') H)) x = e),
    (∃ (f : OpenPartialHomeomorph M H),
        Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) f ∧ e = f.lift_openEmbedding ⋯) ∨
      ∃ (f' : OpenPartialHomeomorph M' H),
        Membership.mem (γ := Set (OpenPartialHomeomorph M' H)) (atlas H M') f' ∧ e = f'.lift_openEmbedding ⋯
⊢ (∃ (f : OpenPartialHomeomorph M H),
      Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) f ∧ e = f.lift_openEmbedding ⋯) ∨
    ∃ (f' : OpenPartialHomeomorph M' H),
      Membership.mem (γ := Set (OpenPartialHomeomorph M' H)) (atlas H M') f' ∧ e = f'.lift_openEmbedding ⋯
have inr : ∀ (x : OpenPartialHomeomorph M' H) (hx : Membership.mem (γ := Set (OpenPartialHomeomorph M' H)) ChartedSpace.atlas x)
  (hxe : (fun (e : OpenPartialHomeomorph M' H) ↦ (e.lift_openEmbedding sorry : OpenPartialHomeomorph (M ⊕ M') H)) x = e),
  (∃ (f : OpenPartialHomeomorph M H),
      Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) f ∧ e = f.lift_openEmbedding sorry) ∨
    ∃ (f' : OpenPartialHomeomorph M' H),
      Membership.mem (γ := Set (OpenPartialHomeomorph M' H)) (atlas H M') f' ∧ e = f'.lift_openEmbedding sorry
Tactic: obtain (⟨x, hx, hxe⟩ | ⟨x, hx, hxe⟩) := he
Cleared hypotheses: he
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ChartedSpace (goal)
Goal:
H : Type u
M : Type u_2
M' : Type u_3
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : TopologicalSpace M'
cm : ChartedSpace H M
cm' : ChartedSpace H M'
h : Nonempty H
e : OpenPartialHomeomorph (M ⊕ M') H
x : OpenPartialHomeomorph M H
hx : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) ChartedSpace.atlas x
hxe : (fun (e : OpenPartialHomeomorph M H) ↦ (e.lift_openEmbedding ⋯ : OpenPartialHomeomorph (M ⊕ M') H)) x = e
⊢ (∃ (f : OpenPartialHomeomorph M H),
      Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) f ∧ e = f.lift_openEmbedding ⋯) ∨
    ∃ (f' : OpenPartialHomeomorph M' H),
      Membership.mem (γ := Set (OpenPartialHomeomorph M' H)) (atlas H M') f' ∧ e = f'.lift_openEmbedding ⋯
have inl : (∃ (f : OpenPartialHomeomorph M H),
    Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) f ∧
      Eq (α := OpenPartialHomeomorph (M ⊕ M') H)
        ((fun (e : OpenPartialHomeomorph M H) ↦ (e.lift_openEmbedding sorry : OpenPartialHomeomorph (M ⊕ M') H)) x)
        (f.lift_openEmbedding sorry)) ∨
  ∃ (f' : OpenPartialHomeomorph M' H),
    Membership.mem (γ := Set (OpenPartialHomeomorph M' H)) (atlas H M') f' ∧
      Eq (α := OpenPartialHomeomorph (M ⊕ M') H)
        ((fun (e : OpenPartialHomeomorph M H) ↦ (e.lift_openEmbedding sorry : OpenPartialHomeomorph (M ⊕ M') H)) x)
        (f'.lift_openEmbedding sorry)
Tactic: rw [← hxe]