awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
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 : ℕ∞ω
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
inst_11 : IsManifold I n M
inst_12 : IsManifold I' n M'
e : OpenPartialHomeomorph M H
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) e
e' : OpenPartialHomeomorph M' H'
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M' H')) (maximalAtlas I' n M') e'
f : OpenPartialHomeomorph M H
hf : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) f
f' : OpenPartialHomeomorph M' H'
hf' : Membership.mem (γ := Set (OpenPartialHomeomorph M' H')) (atlas H' M') f'
⊢ e'.symm ≫ₕ f' ∈ contDiffGroupoid n I'

Tactic:
grind [compatible_of_mem_maximalAtlas, subset_maximalAtlas]

Premises used: IsManifold.compatible_of_mem_maximalAtlas, IsManifold.subset_maximalAtlas
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
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 : ℕ∞ω
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
inst_11 : IsManifold I n M
inst_12 : IsManifold I' n M'
e : OpenPartialHomeomorph M H
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) e
e' : OpenPartialHomeomorph M' H'
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M' H')) (maximalAtlas I' n M') e'
f : OpenPartialHomeomorph M H
hf : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) f
f' : OpenPartialHomeomorph M' H'
hf' : Membership.mem (γ := Set (OpenPartialHomeomorph M' H')) (atlas H' M') f'
⊢ f.symm ≫ₕ e ∈ contDiffGroupoid n I

Tactic:
grind [compatible_of_mem_maximalAtlas, subset_maximalAtlas]

Premises used: IsManifold.compatible_of_mem_maximalAtlas, IsManifold.subset_maximalAtlas
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
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 : ℕ∞ω
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
inst_11 : IsManifold I n M
inst_12 : IsManifold I' n M'
e : OpenPartialHomeomorph M H
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) e
e' : OpenPartialHomeomorph M' H'
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M' H')) (maximalAtlas I' n M') e'
f : OpenPartialHomeomorph M H
hf : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) f
f' : OpenPartialHomeomorph M' H'
hf' : Membership.mem (γ := Set (OpenPartialHomeomorph M' H')) (atlas H' M') f'
⊢ f'.symm ≫ₕ e' ∈ contDiffGroupoid n I'

Tactic:
grind [compatible_of_mem_maximalAtlas, subset_maximalAtlas]

Premises used: IsManifold.compatible_of_mem_maximalAtlas, IsManifold.subset_maximalAtlas
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
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
n : ℕ∞ω
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'
hM : IsManifold I n M
hM' : IsManifold I n M'
e e' : OpenPartialHomeomorph (M ⊕ M') H
he : Membership.mem (γ := Set (OpenPartialHomeomorph (M ⊕ M') H)) (atlas H (M ⊕ M')) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph (M ⊕ M') H)) (atlas H (M ⊕ M')) e'
inl : ∀ (h : IsEmpty H), e.symm ≫ₕ e' ∈ contDiffGroupoid n I
inr : ∀ (h : Nonempty H), e.symm ≫ₕ e' ∈ contDiffGroupoid n I
⊢ e.symm ≫ₕ e' ∈ contDiffGroupoid n I

Tactic:
obtain (h | h) := isEmpty_or_nonempty H

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
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
n : ℕ∞ω
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'
hM : IsManifold I n M
hM' : IsManifold I n M'
e e' : OpenPartialHomeomorph (M ⊕ M') H
he : Membership.mem (γ := Set (OpenPartialHomeomorph (M ⊕ M') H)) (atlas H (M ⊕ M')) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph (M ⊕ M') H)) (atlas H (M ⊕ M')) e'
h : IsEmpty H
⊢ e.symm ≫ₕ e' ∈ contDiffGroupoid n I

Tactic:
ContDiffGroupoid.mem_of_source_eq_empty _ (eq_empty_of_isEmpty _)

Premises used: Set.eq_empty_of_isEmpty, ContDiffGroupoid.mem_of_source_eq_empty
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
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
n : ℕ∞ω
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'
hM : IsManifold I n M
hM' : IsManifold I n M'
e e' : OpenPartialHomeomorph (M ⊕ M') H
he : Membership.mem (γ := Set (OpenPartialHomeomorph (M ⊕ M') H)) (atlas H (M ⊕ M')) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph (M ⊕ M') H)) (atlas H (M ⊕ M')) e'
h : IsEmpty H
⊢ e.symm ≫ₕ e' ∈ contDiffGroupoid n I

Tactic:
exact ContDiffGroupoid.mem_of_source_eq_empty _ (eq_empty_of_isEmpty _)

Premises used: Set.eq_empty_of_isEmpty, ContDiffGroupoid.mem_of_source_eq_empty
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
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
n : ℕ∞ω
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'
hM : IsManifold I n M
hM' : IsManifold I n M'
e e' : OpenPartialHomeomorph (M ⊕ M') H
he : Membership.mem (γ := Set (OpenPartialHomeomorph (M ⊕ M') H)) (atlas H (M ⊕ M')) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph (M ⊕ M') H)) (atlas H (M ⊕ M')) e'
h : Nonempty H
inr :
  ∀ (f : OpenPartialHomeomorph M H) (hf : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) f)
    (hef : e = f.lift_openEmbedding ⋯), e.symm ≫ₕ e' ∈ contDiffGroupoid n I
inr₁ :
  ∀ (f : OpenPartialHomeomorph M' H) (hf : Membership.mem (γ := Set (OpenPartialHomeomorph M' H)) (atlas H M') f)
    (hef : e = f.lift_openEmbedding ⋯), e.symm ≫ₕ e' ∈ contDiffGroupoid n I
⊢ e.symm ≫ₕ e' ∈ contDiffGroupoid n I

Tactic:
obtain (⟨f, hf, hef⟩ | ⟨f, hf, hef⟩) := ChartedSpace.mem_atlas_sum he

Premises used: ChartedSpace.mem_atlas_sum
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
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
n : ℕ∞ω
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'
hM : IsManifold I n M
hM' : IsManifold I n M'
e e' : OpenPartialHomeomorph (M ⊕ M') H
he : Membership.mem (γ := Set (OpenPartialHomeomorph (M ⊕ M') H)) (atlas H (M ⊕ M')) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph (M ⊕ M') H)) (atlas H (M ⊕ M')) e'
h : Nonempty H
f : OpenPartialHomeomorph M H
hf : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) f
hef : e = f.lift_openEmbedding ⋯
inr :
  ∀ (f' : OpenPartialHomeomorph M H) (hf' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) f')
    (he'f' : e' = f'.lift_openEmbedding ⋯), e.symm ≫ₕ e' ∈ contDiffGroupoid n I
inr₁ :
  ∀ (f' : OpenPartialHomeomorph M' H) (hf' : Membership.mem (γ := Set (OpenPartialHomeomorph M' H)) (atlas H M') f')
    (he'f' : e' = f'.lift_openEmbedding ⋯), e.symm ≫ₕ e' ∈ contDiffGroupoid n I
⊢ e.symm ≫ₕ e' ∈ contDiffGroupoid n I

Tactic:
obtain (⟨f', hf', he'f'⟩ | ⟨f', hf', he'f'⟩) := ChartedSpace.mem_atlas_sum he'

Premises used: ChartedSpace.mem_atlas_sum
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
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
n : ℕ∞ω
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'
hM : IsManifold I n M
hM' : IsManifold I n M'
e e' : OpenPartialHomeomorph (M ⊕ M') H
he : Membership.mem (γ := Set (OpenPartialHomeomorph (M ⊕ M') H)) (atlas H (M ⊕ M')) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph (M ⊕ M') H)) (atlas H (M ⊕ M')) e'
h : Nonempty H
f : OpenPartialHomeomorph M H
hf : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) f
hef : e = f.lift_openEmbedding ⋯
f' : OpenPartialHomeomorph M H
hf' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) f'
he'f' : e' = f'.lift_openEmbedding ⋯
inr : f.symm ≫ₕ f' ∈ contDiffGroupoid n I
⊢ e.symm ≫ₕ e' ∈ contDiffGroupoid n I

Tactic:
rw [hef, he'f', f.lift_openEmbedding_trans f' IsOpenEmbedding.inl]

Premises used: OpenPartialHomeomorph.lift_openEmbedding_trans, Topology.IsOpenEmbedding.inl
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
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
n : ℕ∞ω
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'
hM : IsManifold I n M
hM' : IsManifold I n M'
e e' : OpenPartialHomeomorph (M ⊕ M') H
he : Membership.mem (γ := Set (OpenPartialHomeomorph (M ⊕ M') H)) (atlas H (M ⊕ M')) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph (M ⊕ M') H)) (atlas H (M ⊕ M')) e'
h : Nonempty H
f : OpenPartialHomeomorph M H
hf : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) f
hef : e = f.lift_openEmbedding ⋯
f' : OpenPartialHomeomorph M H
hf' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) f'
he'f' : e' = f'.lift_openEmbedding ⋯
⊢ f.symm ≫ₕ f' ∈ contDiffGroupoid n I

Tactic:
hM.compatible hf hf'

Premises used: HasGroupoid.compatible
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
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
n : ℕ∞ω
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'
hM : IsManifold I n M
hM' : IsManifold I n M'
e e' : OpenPartialHomeomorph (M ⊕ M') H
he : Membership.mem (γ := Set (OpenPartialHomeomorph (M ⊕ M') H)) (atlas H (M ⊕ M')) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph (M ⊕ M') H)) (atlas H (M ⊕ M')) e'
h : Nonempty H
f : OpenPartialHomeomorph M H
hf : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) f
hef : e = f.lift_openEmbedding ⋯
f' : OpenPartialHomeomorph M H
hf' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) f'
he'f' : e' = f'.lift_openEmbedding ⋯
⊢ f.symm ≫ₕ f' ∈ contDiffGroupoid n I

Tactic:
exact hM.compatible hf hf'

Premises used: HasGroupoid.compatible
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
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
n : ℕ∞ω
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'
hM : IsManifold I n M
hM' : IsManifold I n M'
e e' : OpenPartialHomeomorph (M ⊕ M') H
he : Membership.mem (γ := Set (OpenPartialHomeomorph (M ⊕ M') H)) (atlas H (M ⊕ M')) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph (M ⊕ M') H)) (atlas H (M ⊕ M')) e'
h : Nonempty H
f : OpenPartialHomeomorph M H
hf : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) f
hef : e = f.lift_openEmbedding ⋯
f' : OpenPartialHomeomorph M' H
hf' : Membership.mem (γ := Set (OpenPartialHomeomorph M' H)) (atlas H M') f'
he'f' : e' = f'.lift_openEmbedding ⋯
inr : OpenPartialHomeomorph.symm (f.lift_openEmbedding ⋯) ≫ₕ f'.lift_openEmbedding ⋯ ∈ contDiffGroupoid n I
⊢ e.symm ≫ₕ e' ∈ contDiffGroupoid n I

Tactic:
rw [hef, he'f']
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
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
n : ℕ∞ω
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'
hM : IsManifold I n M
hM' : IsManifold I n M'
e e' : OpenPartialHomeomorph (M ⊕ M') H
he : Membership.mem (γ := Set (OpenPartialHomeomorph (M ⊕ M') H)) (atlas H (M ⊕ M')) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph (M ⊕ M') H)) (atlas H (M ⊕ M')) e'
h : Nonempty H
f : OpenPartialHomeomorph M H
hf : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) f
hef : e = f.lift_openEmbedding ⋯
f' : OpenPartialHomeomorph M' H
hf' : Membership.mem (γ := Set (OpenPartialHomeomorph M' H)) (atlas H M') f'
he'f' : e' = f'.lift_openEmbedding ⋯
inr : (OpenPartialHomeomorph.symm (f.lift_openEmbedding ⋯) ≫ₕ f'.lift_openEmbedding ⋯).source = ∅
⊢ OpenPartialHomeomorph.symm (f.lift_openEmbedding ⋯) ≫ₕ f'.lift_openEmbedding ⋯ ∈ contDiffGroupoid n I

Tactic:
apply ContDiffGroupoid.mem_of_source_eq_empty

Premises used: ContDiffGroupoid.mem_of_source_eq_empty
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
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
n : ℕ∞ω
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'
hM : IsManifold I n M
hM' : IsManifold I n M'
e e' : OpenPartialHomeomorph (M ⊕ M') H
he : Membership.mem (γ := Set (OpenPartialHomeomorph (M ⊕ M') H)) (atlas H (M ⊕ M')) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph (M ⊕ M') H)) (atlas H (M ⊕ M')) e'
h : Nonempty H
f : OpenPartialHomeomorph M H
hf : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) f
hef : e = f.lift_openEmbedding ⋯
f' : OpenPartialHomeomorph M' H
hf' : Membership.mem (γ := Set (OpenPartialHomeomorph M' H)) (atlas H M') f'
he'f' : e' = f'.lift_openEmbedding ⋯
inr :
  ∀ (x : H),
    x ∈ (OpenPartialHomeomorph.symm (f.lift_openEmbedding ⋯) ≫ₕ f'.lift_openEmbedding ⋯).source ↔
      Membership.mem (γ := Set H) ∅ x
⊢ (OpenPartialHomeomorph.symm (f.lift_openEmbedding ⋯) ≫ₕ f'.lift_openEmbedding ⋯).source = ∅

Tactic:
ext x
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
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
n : ℕ∞ω
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'
hM : IsManifold I n M
hM' : IsManifold I n M'
e e' : OpenPartialHomeomorph (M ⊕ M') H
he : Membership.mem (γ := Set (OpenPartialHomeomorph (M ⊕ M') H)) (atlas H (M ⊕ M')) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph (M ⊕ M') H)) (atlas H (M ⊕ M')) e'
h : Nonempty H
f : OpenPartialHomeomorph M H
hf : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) f
hef : e = f.lift_openEmbedding ⋯
f' : OpenPartialHomeomorph M' H
hf' : Membership.mem (γ := Set (OpenPartialHomeomorph M' H)) (atlas H M') f'
he'f' : e' = f'.lift_openEmbedding ⋯
x : H
h_1 : x ∈ (OpenPartialHomeomorph.symm (f.lift_openEmbedding ⋯) ≫ₕ f'.lift_openEmbedding ⋯).source
hx₁ :
  x ∈
    target (α := M ⊕ M')
      (OpenPartialHomeomorph.toPartialEquiv
        (OpenPartialHomeomorph.symm (OpenPartialHomeomorph.symm (f.lift_openEmbedding ⋯))))
hx₂ :
  x ∈
    (↑(OpenPartialHomeomorph.symm (OpenPartialHomeomorph.symm (OpenPartialHomeomorph.symm (f.lift_openEmbedding ⋯)))) :
        H → M ⊕ M') ⁻¹'
      source (OpenPartialHomeomorph.toPartialEquiv (f'.lift_openEmbedding ⋯))
⊢ Membership.mem (γ := Set H) ∅ x

Tactic:
simp_all
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
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
n : ℕ∞ω
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'
hM : IsManifold I n M
hM' : IsManifold I n M'
e e' : OpenPartialHomeomorph (M ⊕ M') H
he : Membership.mem (γ := Set (OpenPartialHomeomorph (M ⊕ M') H)) (atlas H (M ⊕ M')) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph (M ⊕ M') H)) (atlas H (M ⊕ M')) e'
h : Nonempty H
f : OpenPartialHomeomorph M H
hf : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) f
hef : e = f.lift_openEmbedding ⋯
f' : OpenPartialHomeomorph M' H
hf' : Membership.mem (γ := Set (OpenPartialHomeomorph M' H)) (atlas H M') f'
he'f' : e' = f'.lift_openEmbedding ⋯
x : H
⊢ x ∈ (OpenPartialHomeomorph.symm (f.lift_openEmbedding ⋯) ≫ₕ f'.lift_openEmbedding ⋯).source ↔
    Membership.mem (γ := Set H) ∅ x

Tactic:
exact ⟨fun ⟨hx₁, hx₂⟩ ↦ by simp_all, fun hx ↦ hx.elim⟩
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
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
n : ℕ∞ω
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'
hM : IsManifold I n M
hM' : IsManifold I n M'
e e' : OpenPartialHomeomorph (M ⊕ M') H
he : Membership.mem (γ := Set (OpenPartialHomeomorph (M ⊕ M') H)) (atlas H (M ⊕ M')) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph (M ⊕ M') H)) (atlas H (M ⊕ M')) e'
h : Nonempty H
f : OpenPartialHomeomorph M' H
hf : Membership.mem (γ := Set (OpenPartialHomeomorph M' H)) (atlas H M') f
hef : e = f.lift_openEmbedding ⋯
inr :
  ∀ (f' : OpenPartialHomeomorph M H) (hf' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) f')
    (he'f' : e' = f'.lift_openEmbedding ⋯), e.symm ≫ₕ e' ∈ contDiffGroupoid n I
inr₁ :
  ∀ (f' : OpenPartialHomeomorph M' H) (hf' : Membership.mem (γ := Set (OpenPartialHomeomorph M' H)) (atlas H M') f')
    (he'f' : e' = f'.lift_openEmbedding ⋯), e.symm ≫ₕ e' ∈ contDiffGroupoid n I
⊢ e.symm ≫ₕ e' ∈ contDiffGroupoid n I

Tactic:
obtain (⟨f', hf', he'f'⟩ | ⟨f', hf', he'f'⟩) := ChartedSpace.mem_atlas_sum he'

Premises used: ChartedSpace.mem_atlas_sum
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
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
n : ℕ∞ω
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'
hM : IsManifold I n M
hM' : IsManifold I n M'
e e' : OpenPartialHomeomorph (M ⊕ M') H
he : Membership.mem (γ := Set (OpenPartialHomeomorph (M ⊕ M') H)) (atlas H (M ⊕ M')) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph (M ⊕ M') H)) (atlas H (M ⊕ M')) e'
h : Nonempty H
f : OpenPartialHomeomorph M' H
hf : Membership.mem (γ := Set (OpenPartialHomeomorph M' H)) (atlas H M') f
hef : e = f.lift_openEmbedding ⋯
f' : OpenPartialHomeomorph M H
hf' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) f'
he'f' : e' = f'.lift_openEmbedding ⋯
inr : OpenPartialHomeomorph.symm (f.lift_openEmbedding ⋯) ≫ₕ f'.lift_openEmbedding ⋯ ∈ contDiffGroupoid n I
⊢ e.symm ≫ₕ e' ∈ contDiffGroupoid n I

Tactic:
rw [hef, he'f']
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
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
n : ℕ∞ω
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'
hM : IsManifold I n M
hM' : IsManifold I n M'
e e' : OpenPartialHomeomorph (M ⊕ M') H
he : Membership.mem (γ := Set (OpenPartialHomeomorph (M ⊕ M') H)) (atlas H (M ⊕ M')) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph (M ⊕ M') H)) (atlas H (M ⊕ M')) e'
h : Nonempty H
f : OpenPartialHomeomorph M' H
hf : Membership.mem (γ := Set (OpenPartialHomeomorph M' H)) (atlas H M') f
hef : e = f.lift_openEmbedding ⋯
f' : OpenPartialHomeomorph M H
hf' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) f'
he'f' : e' = f'.lift_openEmbedding ⋯
inr : (OpenPartialHomeomorph.symm (f.lift_openEmbedding ⋯) ≫ₕ f'.lift_openEmbedding ⋯).source = ∅
⊢ OpenPartialHomeomorph.symm (f.lift_openEmbedding ⋯) ≫ₕ f'.lift_openEmbedding ⋯ ∈ contDiffGroupoid n I

Tactic:
apply ContDiffGroupoid.mem_of_source_eq_empty

Premises used: ContDiffGroupoid.mem_of_source_eq_empty
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
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
n : ℕ∞ω
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'
hM : IsManifold I n M
hM' : IsManifold I n M'
e e' : OpenPartialHomeomorph (M ⊕ M') H
he : Membership.mem (γ := Set (OpenPartialHomeomorph (M ⊕ M') H)) (atlas H (M ⊕ M')) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph (M ⊕ M') H)) (atlas H (M ⊕ M')) e'
h : Nonempty H
f : OpenPartialHomeomorph M' H
hf : Membership.mem (γ := Set (OpenPartialHomeomorph M' H)) (atlas H M') f
hef : e = f.lift_openEmbedding ⋯
f' : OpenPartialHomeomorph M H
hf' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) f'
he'f' : e' = f'.lift_openEmbedding ⋯
inr :
  ∀ (x : H),
    x ∈ (OpenPartialHomeomorph.symm (f.lift_openEmbedding ⋯) ≫ₕ f'.lift_openEmbedding ⋯).source ↔
      Membership.mem (γ := Set H) ∅ x
⊢ (OpenPartialHomeomorph.symm (f.lift_openEmbedding ⋯) ≫ₕ f'.lift_openEmbedding ⋯).source = ∅

Tactic:
ext x