awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
Goal:
H : Type u_5
inst : TopologicalSpace H
e : OpenPartialHomeomorph H H
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph H H)) (atlas H H) e ↔ e = OpenPartialHomeomorph.refl H

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.singleton
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
Goal:
H : Type u_5
inst : TopologicalSpace H
x : H
⊢ Eq (α := OpenPartialHomeomorph H H) (chartAt H x) (OpenPartialHomeomorph.refl H)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
Goal:
H : Type u
H' : Type u_1
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst : TopologicalSpace M
inst_1 : TopologicalSpace H
inst_2 : DiscreteTopology M
h : Unique H
x : M
⊢ Membership.mem (γ := Set M) (PartialEquiv.source (β := H) (toPartialEquiv (const (a := x) (b := default) ⋯ ⋯))) x

Tactic:
simp
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
Goal:
H : Type u
H' : Type u_1
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst : TopologicalSpace M
inst_1 : TopologicalSpace H
inst_2 : DiscreteTopology M
h : Unique H
x : M
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph M H)) ((fun (x : M) ↦ const (a := x) (b := default) ⋯ ⋯) '' univ)
    (const (a := x) (b := default) ⋯ ⋯)

Tactic:
simp
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace M
inst_1 : TopologicalSpace H
inst_2 : DiscreteTopology M
h : Unique H
x : M
⊢ Eq (α := OpenPartialHomeomorph M H) (chartAt H x) (const (a := x) (b := default) ⋯ ⋯)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
Goal:
H : Type u_5
H' : Type u_6
α : Type u_7
f : H → α
rw : Eq (α := Set (α × H')) (range fun (p : ModelProd H H') ↦ (f p.1, p.2)) (range fun (p : H × H') ↦ (f p.1, p.2))
⊢ (range fun (p : ModelProd H H') ↦ (f p.1, p.2)) = SProd.sprod (β := Set H') (range f) univ

Tactic:
rw [prod_range_univ_eq]

Premises used: Set.prod_range_univ_eq
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
Goal:
H : Type u_5
H' : Type u_6
α : Type u_7
f : H → α
⊢ Eq (α := Set (α × H')) (range fun (p : ModelProd H H') ↦ (f p.1, p.2)) (range fun (p : H × H') ↦ (f p.1, p.2))

Tactic:
rfl
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
Goal:
H : Type u
H' : Type u_1
x y : ModelProd H H'
h₁ : x.1 = y.1
h₂ : x.2 = y.2
⊢ x = y

Tactic:
Prod.ext h₁ h₂

Premises used: Prod.ext, ModelProd
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
Goal:
H : Type u
H' : Type u_1
M : Type u_2
M' : Type u_3
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : TopologicalSpace H'
inst_4 : TopologicalSpace M'
inst_5 : ChartedSpace H' M'
x : M × M'
⊢ Eq (α := OpenPartialHomeomorph (M × M') (ModelProd H H')) (chartAt (ModelProd H H') x)
    (OpenPartialHomeomorph.prod (chartAt H x.1) (chartAt H' x.2))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
Goal:
H : Type u
H' : Type u_1
inst : TopologicalSpace H
inst_1 : TopologicalSpace H'
atlas : Eq (α := Set (OpenPartialHomeomorph (H × H') (ModelProd H H'))) ChartedSpace.atlas ChartedSpace.atlas
chartAt : Eq (α := H × H' → OpenPartialHomeomorph (H × H') (ModelProd H H')) ChartedSpace.chartAt ChartedSpace.chartAt
⊢ Eq (α := ChartedSpace (ModelProd H H') (H × H')) (prodChartedSpace H H H' H') (chartedSpaceSelf (H × H'))

Tactic:
ext1
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
Goal:
H : Type u
H' : Type u_1
inst : TopologicalSpace H
inst_1 : TopologicalSpace H'
⊢ Eq (α := Set (OpenPartialHomeomorph (H × H') (ModelProd H H'))) ChartedSpace.atlas ChartedSpace.atlas

Tactic:
simp [atlas, ChartedSpace.atlas]

Premises used: ChartedSpace.atlas, atlas
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
Goal:
H : Type u
H' : Type u_1
inst : TopologicalSpace H
inst_1 : TopologicalSpace H'
chartAt :
  ∀ (x : H × H'),
    Eq (α := OpenPartialHomeomorph (H × H') (ModelProd H H')) (ChartedSpace.chartAt x) (ChartedSpace.chartAt x)
⊢ Eq (α := H × H' → OpenPartialHomeomorph (H × H') (ModelProd H H')) ChartedSpace.chartAt ChartedSpace.chartAt

Tactic:
ext1
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
Goal:
H : Type u
H' : Type u_1
inst : TopologicalSpace H
inst_1 : TopologicalSpace H'
x : H × H'
chartAt :
  Eq (α := OpenPartialHomeomorph (H × H') (ModelProd H H')) (OpenPartialHomeomorph.refl (H × H'))
    (OpenPartialHomeomorph.refl (ModelProd H H'))
⊢ Eq (α := OpenPartialHomeomorph (H × H') (ModelProd H H')) (ChartedSpace.chartAt x) (ChartedSpace.chartAt x)

Tactic:
simp only [prodChartedSpace_chartAt, chartAt_self_eq, refl_prod_refl]

Premises used: OpenPartialHomeomorph.refl_prod_refl, prodChartedSpace_chartAt, chartAt_self_eq
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
Goal:
H : Type u
H' : Type u_1
inst : TopologicalSpace H
inst_1 : TopologicalSpace H'
x : H × H'
⊢ Eq (α := OpenPartialHomeomorph (H × H') (ModelProd H H')) (OpenPartialHomeomorph.refl (H × H'))
    (OpenPartialHomeomorph.refl (ModelProd H H'))

Tactic:
rfl
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
Goal:
ι : Type u_5
inst : Finite ι
H : ι → Type u_6
inst_1 : (i : ι) → TopologicalSpace (H i)
M : ι → Type u_7
inst_2 : (i : ι) → TopologicalSpace (M i)
inst_3 : (i : ι) → ChartedSpace.{u_6, u_7} (H i) (M i)
f : (i : ι) → M i
⊢ Eq (α := OpenPartialHomeomorph ((i : ι) → M i) (ModelPi H)) (chartAt (ModelPi H) f)
    (OpenPartialHomeomorph.pi (X := M) (Y := H) fun (i : ι) ↦ chartAt (H i) (f i))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
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_2, u} (β := H) (toPartialEquiv (ChartedSpace.chartAt x))
right : Eq (α := M ⊕ M') (Sum.inl x) (Sum.inl x)
⊢ Membership.mem (γ := Set (M ⊕ M'))
    (PartialEquiv.source (β := H) (toPartialEquiv (lift_openEmbedding (ChartedSpace.chartAt x) ⋯))) (Sum.inl x)

Tactic:
use x, cm.mem_chart_source x

Premises used: ChartedSpace.mem_chart_source
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
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))
right : Eq (α := M ⊕ M') (Sum.inr x) (Sum.inr x)
⊢ Membership.mem (γ := Set (M ⊕ M'))
    (PartialEquiv.source (β := H) (toPartialEquiv (lift_openEmbedding (ChartedSpace.chartAt x) ⋯))) (Sum.inr x)

Tactic:
use x, cm'.mem_chart_source x

Premises used: ChartedSpace.mem_chart_source
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
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)
inr :
  ∀ (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.inr x))))
      (Sum.inr 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

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

Premises used: OpenPartialHomeomorph.lift_openEmbedding_source, Topology.IsOpenEmbedding.inr, Sum.elim_inr, Topology.IsOpenEmbedding.inl, Sum.elim_inl
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
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
inl :
  Membership.mem (γ := Set (OpenPartialHomeomorph (M ⊕ M') H))
    ((fun (e : OpenPartialHomeomorph M H) ↦ e.lift_openEmbedding ⋯) '' ChartedSpace.atlas)
    (lift_openEmbedding (ChartedSpace.chartAt 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)
    (lift_openEmbedding (ChartedSpace.chartAt x) ⋯)

Tactic:
left
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
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)
right :
  Eq (α := OpenPartialHomeomorph (M ⊕ M') H)
    ((fun (e : OpenPartialHomeomorph M H) ↦ (e.lift_openEmbedding ⋯ : OpenPartialHomeomorph (M ⊕ M') H))
      (ChartedSpace.chartAt x))
    (lift_openEmbedding (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) ⋯)

Tactic:
use ChartedSpace.chartAt x, cm.chart_mem_atlas x

Premises used: ChartedSpace.chart_mem_atlas, ChartedSpace.chartAt
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
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'
inr :
  Membership.mem (γ := Set (OpenPartialHomeomorph (M ⊕ M') H))
    ((fun (e : OpenPartialHomeomorph M' H) ↦ e.lift_openEmbedding ⋯) '' ChartedSpace.atlas)
    (lift_openEmbedding (ChartedSpace.chartAt 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)
    (lift_openEmbedding (ChartedSpace.chartAt x) ⋯)

Tactic:
right
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
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)
right :
  Eq (α := OpenPartialHomeomorph (M ⊕ M') H)
    ((fun (e : OpenPartialHomeomorph M' H) ↦ (e.lift_openEmbedding ⋯ : OpenPartialHomeomorph (M ⊕ M') H))
      (ChartedSpace.chartAt x))
    (lift_openEmbedding (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) ⋯)

Tactic:
use ChartedSpace.chartAt x, cm'.chart_mem_atlas x

Premises used: ChartedSpace.chart_mem_atlas, ChartedSpace.chartAt
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
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))
inr :
  ∀ (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.inr 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)

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

Premises used: Sum.elim_inr, Sum.elim_inl
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
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')
neg : (h : IsEmpty H) → ChartedSpace H (M ⊕ M')
⊢ ChartedSpace H (M ⊕ M')

Tactic:
by_cases! h : Nonempty H

Premises used: Nonempty
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
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 : Nonempty H
⊢ ChartedSpace H (M ⊕ M')

Tactic:
exact ChartedSpace.sum_of_nonempty

Premises used: ChartedSpace.sum_of_nonempty
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
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
⊢ IsEmpty M

Tactic:
have : IsEmpty M := isEmpty_of_chartedSpace H
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
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
⊢ IsEmpty M'

Tactic:
have : IsEmpty M' := isEmpty_of_chartedSpace H
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
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_1 : IsEmpty M
this : IsEmpty M'
⊢ ChartedSpace H (M ⊕ M')

Tactic:
exact empty H (M ⊕ M')

Premises used: Sum, ChartedSpace.empty
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
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
simp :
  Eq (α := OpenPartialHomeomorph (M ⊕ M') H) (ChartedSpace.chartAt (Sum.inl x))
    (lift_openEmbedding (ChartedSpace.chartAt x) ⋯)
⊢ Eq (α := OpenPartialHomeomorph (M ⊕ M') H) (chartAt H (Sum.inl x)) (lift_openEmbedding (chartAt H x) ⋯)

Tactic:
simp +instances only [chartAt, sum, nonempty_of_chartedSpace x, ↓reduceDIte]

Premises used: ChartedSpace.sum, chartAt, reduceDIte, nonempty_of_chartedSpace
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
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) (ChartedSpace.chartAt (Sum.inl x))
    (lift_openEmbedding (ChartedSpace.chartAt x) ⋯)

Tactic:
rfl
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
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'
simp :
  Eq (α := OpenPartialHomeomorph (M ⊕ M') H) (ChartedSpace.chartAt (Sum.inr x'))
    (lift_openEmbedding (ChartedSpace.chartAt x') ⋯)
⊢ Eq (α := OpenPartialHomeomorph (M ⊕ M') H) (chartAt H (Sum.inr x')) (lift_openEmbedding (chartAt H x') ⋯)

Tactic:
simp +instances only [chartAt, sum, nonempty_of_chartedSpace x', ↓reduceDIte]

Premises used: ChartedSpace.sum, chartAt, reduceDIte, nonempty_of_chartedSpace
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
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) (ChartedSpace.chartAt (Sum.inr x'))
    (lift_openEmbedding (ChartedSpace.chartAt x') ⋯)

Tactic:
rfl
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
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
⊢ Nonempty H

Tactic:
haveI : Nonempty H := nonempty_of_chartedSpace x
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
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
rw : (↑(lift_openEmbedding (chartAt H x) ⋯) : M ⊕ M' → H) (Sum.inl y) = (↑(chartAt H x) : M → H) y
⊢ (↑(chartAt H (Sum.inl x)) : M ⊕ M' → H) (Sum.inl y) = (↑(chartAt H x) : M → H) y

Tactic:
rw [ChartedSpace.sum_chartAt_inl]

Premises used: ChartedSpace.sum_chartAt_inl
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
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
⊢ (↑(lift_openEmbedding (chartAt H x) ⋯) : M ⊕ M' → H) (Sum.inl y) = (↑(chartAt H x) : M → H) y

Tactic:
OpenPartialHomeomorph.lift_openEmbedding_apply _ _

Premises used: OpenPartialHomeomorph.lift_openEmbedding_apply
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
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
⊢ (↑(lift_openEmbedding (chartAt H x) ⋯) : M ⊕ M' → H) (Sum.inl y) = (↑(chartAt H x) : M → H) y

Tactic:
exact OpenPartialHomeomorph.lift_openEmbedding_apply _ _

Premises used: OpenPartialHomeomorph.lift_openEmbedding_apply
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
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'
⊢ Nonempty H

Tactic:
haveI : Nonempty H := nonempty_of_chartedSpace x
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
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
rw : (↑(lift_openEmbedding (chartAt H x) ⋯) : M ⊕ M' → H) (Sum.inr y) = (↑(chartAt H x) : M' → H) y
⊢ (↑(chartAt H (Sum.inr x)) : M ⊕ M' → H) (Sum.inr y) = (↑(chartAt H x) : M' → H) y

Tactic:
rw [ChartedSpace.sum_chartAt_inr]

Premises used: ChartedSpace.sum_chartAt_inr
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
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
⊢ (↑(lift_openEmbedding (chartAt H x) ⋯) : M ⊕ M' → H) (Sum.inr y) = (↑(chartAt H x) : M' → H) y

Tactic:
OpenPartialHomeomorph.lift_openEmbedding_apply _ _

Premises used: OpenPartialHomeomorph.lift_openEmbedding_apply
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
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
⊢ (↑(lift_openEmbedding (chartAt H x) ⋯) : M ⊕ M' → H) (Sum.inr y) = (↑(chartAt H x) : M' → H) y

Tactic:
exact OpenPartialHomeomorph.lift_openEmbedding_apply _ _

Premises used: OpenPartialHomeomorph.lift_openEmbedding_apply
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
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
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph (M ⊕ M') H)) ChartedSpace.atlas e

Tactic:
simp +instances only [atlas, sum, h, ↓reduceDIte] at he

Premises used: ChartedSpace.sum, reduceDIte, atlas
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
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 ⋯
inr :
  ∀ (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 ⋯

Tactic:
obtain (⟨x, hx, hxe⟩ | ⟨x, hx, hxe⟩) := he