awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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
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 ⋯ : OpenPartialHomeomorph (M ⊕ M') H)) x)
          (f.lift_openEmbedding ⋯)) ∨
    ∃ (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 ⋯ : OpenPartialHomeomorph (M ⊕ M') H)) x)
          (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:
rw [← hxe]
-- 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
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
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 ⋯ : OpenPartialHomeomorph (M ⊕ M') H)) x)
        (f.lift_openEmbedding ⋯)
⊢ (∃ (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 ⋯ : OpenPartialHomeomorph (M ⊕ M') H)) x)
          (f.lift_openEmbedding ⋯)) ∨
    ∃ (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 ⋯ : OpenPartialHomeomorph (M ⊕ M') H)) x)
          (f'.lift_openEmbedding ⋯)

Tactic:
left
-- 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
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
w : OpenPartialHomeomorph M H
h₁ :
  Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) x ∧
    Eq (α := OpenPartialHomeomorph (M ⊕ M') H)
      ((fun (e : OpenPartialHomeomorph M H) ↦ (e.lift_openEmbedding ⋯ : OpenPartialHomeomorph (M ⊕ M') H)) x)
      (x.lift_openEmbedding ⋯)
⊢ ∃ (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 ⋯ : OpenPartialHomeomorph (M ⊕ M') H)) x)
        (f.lift_openEmbedding ⋯)

Tactic:
use 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'
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
inr :
  (∃ (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 ⋯ : OpenPartialHomeomorph (M ⊕ M') H)) x)
          (f.lift_openEmbedding ⋯)) ∨
    ∃ (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 ⋯ : OpenPartialHomeomorph (M ⊕ M') H)) x)
          (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:
rw [← hxe]
-- 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
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
inr :
  ∃ (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 ⋯ : OpenPartialHomeomorph (M ⊕ M') H)) x)
        (f'.lift_openEmbedding ⋯)
⊢ (∃ (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 ⋯ : OpenPartialHomeomorph (M ⊕ M') H)) x)
          (f.lift_openEmbedding ⋯)) ∨
    ∃ (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 ⋯ : OpenPartialHomeomorph (M ⊕ M') H)) x)
          (f'.lift_openEmbedding ⋯)

Tactic:
right
-- 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
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
w : OpenPartialHomeomorph M' H
h₁ :
  Membership.mem (γ := Set (OpenPartialHomeomorph M' H)) (atlas H M') x ∧
    Eq (α := OpenPartialHomeomorph (M ⊕ M') H)
      ((fun (e : OpenPartialHomeomorph M' H) ↦ (e.lift_openEmbedding ⋯ : OpenPartialHomeomorph (M ⊕ M') H)) x)
      (x.lift_openEmbedding ⋯)
⊢ ∃ (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 ⋯ : OpenPartialHomeomorph (M ⊕ M') H)) x)
        (f'.lift_openEmbedding ⋯)

Tactic:
use x
-- 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 M'
inst_2 : TopologicalSpace H
inst_3 : ChartedSpace H M
f : M → M'
hf : IsLocalHomeomorph f
g : M' → M
hg : Function.RightInverse g f
q : M'
nth_rw : f (g q) ∈ (toPartialEquiv (hf.localInverseAt (g q) ≫ₕ chartAt H (g q))).source
⊢ q ∈ (toPartialEquiv (hf.localInverseAt (g q) ≫ₕ chartAt H (g q))).source

Tactic:
nth_rw 3 [← hg.eq q]

Premises used: Function.RightInverse.eq
-- 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 M'
inst_2 : TopologicalSpace H
inst_3 : ChartedSpace H M
f : M → M'
hf : IsLocalHomeomorph f
g : M' → M
hg : Function.RightInverse g f
q : M'
⊢ f (g q) ∈ (toPartialEquiv (hf.localInverseAt (g q) ≫ₕ chartAt H (g q))).source

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 M'
inst_2 : TopologicalSpace H
inst_3 : ChartedSpace H M
f : M → M'
hf : IsLocalHomeomorph f
g : M' → M
hg : Function.RightInverse g f
⊢ ∀ (x : M'),
    Membership.mem (γ := Set (OpenPartialHomeomorph M' H))
      {x : OpenPartialHomeomorph M' H | ∃ (q : M'), hf.localInverseAt (g q) ≫ₕ chartAt H (g q) = x}
      (hf.localInverseAt (g x) ≫ₕ chartAt H (g x))

Tactic:
simp
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
c : ChartedSpaceCore H M
e : PartialEquiv M H
he : e ∈ c.atlas
a :
  Membership.mem (γ := Set (Set M))
    (⋃ e ∈ c.atlas, ⋃ (s : Set H), ⋃ (_ : IsOpen[inst] s), {(↑e : M → H) ⁻¹' s ∩ e.source}) e.source
⊢ IsOpen[c.toTopologicalSpace] e.source

Tactic:
apply TopologicalSpace.GenerateOpen.basic

Premises used: TopologicalSpace.GenerateOpen.basic
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
c : ChartedSpaceCore H M
e : PartialEquiv M H
he : e ∈ c.atlas
a : ∃ i ∈ c.atlas, ∃ (i_1 : Set H), IsOpen[inst] i_1 ∧ e.source = (↑i : M → H) ⁻¹' i_1 ∩ i.source
⊢ Membership.mem (γ := Set (Set M))
    (⋃ e ∈ c.atlas, ⋃ (s : Set H), ⋃ (_ : IsOpen[inst] s), {(↑e : M → H) ⁻¹' s ∩ e.source}) e.source

Tactic:
simp only [exists_prop, mem_iUnion, mem_singleton_iff]

Premises used: Set.mem_iUnion, exists_prop, Set.mem_singleton_iff
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
c : ChartedSpaceCore H M
e : PartialEquiv M H
he : e ∈ c.atlas
⊢ ∃ i ∈ c.atlas, ∃ (i_1 : Set H), IsOpen[inst] i_1 ∧ e.source = (↑i : M → H) ⁻¹' i_1 ∩ i.source

Tactic:
⟨e, he, univ, isOpen_univ, ?_⟩

Premises used: Set.univ, isOpen_univ, And.intro, Exists.intro
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
c : ChartedSpaceCore H M
e : PartialEquiv M H
he : e ∈ c.atlas
a : e.source = (↑e : M → H) ⁻¹' univ ∩ e.source
⊢ ∃ i ∈ c.atlas, ∃ (i_1 : Set H), IsOpen[inst] i_1 ∧ e.source = (↑i : M → H) ⁻¹' i_1 ∩ i.source

Tactic:
refine ⟨e, he, univ, isOpen_univ, ?_⟩
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
c : ChartedSpaceCore H M
e : PartialEquiv M H
he : e ∈ c.atlas
⊢ e.source = (↑e : M → H) ⁻¹' univ ∩ e.source

Tactic:
simp only [Set.univ_inter, Set.preimage_univ]

Premises used: Set.univ_inter, Set.preimage_univ
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
c : ChartedSpaceCore H M
e : PartialEquiv M H
he : e ∈ c.atlas
⊢ e.target ∩ (↑e.symm : H → M) ⁻¹' e.source = e.target

Tactic:
have E : e.target ∩ e.symm ⁻¹' e.source = e.target :=
    Subset.antisymm inter_subset_left fun x hx ↦
      ⟨hx, PartialEquiv.target_subset_preimage_source _ hx⟩
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
c : ChartedSpaceCore H M
e : PartialEquiv M H
he : e ∈ c.atlas
E : e.target ∩ (↑e.symm : H → M) ⁻¹' e.source = e.target
⊢ IsOpen[inst] e.target

Tactic:
simpa [PartialEquiv.trans_source, E] using c.open_source e e he he

Premises used: PartialEquiv.trans_source, ChartedSpaceCore.open_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
c : ChartedSpaceCore H M
e_1 e : PartialEquiv M H
he : e ∈ c.atlas
⊢ IsOpen[c.toTopologicalSpace] e.source

Tactic:
c.open_source' he

Premises used: ChartedSpaceCore.open_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
c : ChartedSpaceCore H M
e_1 e : PartialEquiv M H
he : e ∈ c.atlas
⊢ IsOpen[c.toTopologicalSpace] e.source

Tactic:
convert! c.open_source' he

Premises used: ChartedSpaceCore.open_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
c : ChartedSpaceCore H M
e_1 e : PartialEquiv M H
he : e ∈ c.atlas
⊢ IsOpen[inst] e.target

Tactic:
c.open_target he

Premises used: ChartedSpaceCore.open_target
-- 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
c : ChartedSpaceCore H M
e_1 e : PartialEquiv M H
he : e ∈ c.atlas
⊢ IsOpen[inst] e.target

Tactic:
convert! c.open_target he

Premises used: ChartedSpaceCore.open_target
-- 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
c : ChartedSpaceCore H M
e_1 e : PartialEquiv M H
he : e ∈ c.atlas
this : TopologicalSpace M := c.toTopologicalSpace
rw : ∀ (t : Set H), IsOpen[inst] t → IsOpen[c.toTopologicalSpace] (e.source ∩ (↑e : M → H) ⁻¹' t)
⊢ ContinuousOn (↑e : M → H) e.source

Tactic:
rw [continuousOn_open_iff (c.open_source' he)]

Premises used: continuousOn_open_iff, ChartedSpaceCore.open_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
c : ChartedSpaceCore H M
e_1 e : PartialEquiv M H
he : e ∈ c.atlas
this : TopologicalSpace M := c.toTopologicalSpace
s : Set H
s_open : IsOpen[inst] s
rw : IsOpen[c.toTopologicalSpace] ((↑e : M → H) ⁻¹' s ∩ e.source)
⊢ IsOpen[c.toTopologicalSpace] (e.source ∩ (↑e : M → H) ⁻¹' s)

Tactic:
rw [inter_comm]

Premises used: Set.inter_comm
-- 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
c : ChartedSpaceCore H M
e_1 e : PartialEquiv M H
he : e ∈ c.atlas
this : TopologicalSpace M := c.toTopologicalSpace
s : Set H
s_open : IsOpen[inst] s
a :
  Membership.mem (γ := Set (Set M))
    (⋃ e ∈ c.atlas, ⋃ (s : Set H), ⋃ (_ : IsOpen[inst] s), {(↑e : M → H) ⁻¹' s ∩ e.source})
    ((↑e : M → H) ⁻¹' s ∩ e.source)
⊢ IsOpen[c.toTopologicalSpace] ((↑e : M → H) ⁻¹' s ∩ e.source)

Tactic:
apply TopologicalSpace.GenerateOpen.basic

Premises used: TopologicalSpace.GenerateOpen.basic
-- 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
c : ChartedSpaceCore H M
e_1 e : PartialEquiv M H
he : e ∈ c.atlas
this : TopologicalSpace M := c.toTopologicalSpace
s : Set H
s_open : IsOpen[inst] s
a : ∃ i ∈ c.atlas, ∃ (i_1 : Set H), IsOpen[inst] i_1 ∧ (↑e : M → H) ⁻¹' s ∩ e.source = (↑i : M → H) ⁻¹' i_1 ∩ i.source
⊢ Membership.mem (γ := Set (Set M))
    (⋃ e ∈ c.atlas, ⋃ (s : Set H), ⋃ (_ : IsOpen[inst] s), {(↑e : M → H) ⁻¹' s ∩ e.source})
    ((↑e : M → H) ⁻¹' s ∩ e.source)

Tactic:
simp only [exists_prop, mem_iUnion, mem_singleton_iff]

Premises used: Set.mem_iUnion, exists_prop, Set.mem_singleton_iff
-- 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
c : ChartedSpaceCore H M
e_1 e : PartialEquiv M H
he : e ∈ c.atlas
this : TopologicalSpace M := c.toTopologicalSpace
s : Set H
s_open : IsOpen[inst] s
⊢ ∃ i ∈ c.atlas, ∃ (i_1 : Set H), IsOpen[inst] i_1 ∧ (↑e : M → H) ⁻¹' s ∩ e.source = (↑i : M → H) ⁻¹' i_1 ∩ i.source

Tactic:
⟨e, he, ⟨s, s_open, rfl⟩⟩

Premises used: And.intro, Exists.intro, 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
c : ChartedSpaceCore H M
e_1 e : PartialEquiv M H
he : e ∈ c.atlas
this : TopologicalSpace M := c.toTopologicalSpace
s : Set H
s_open : IsOpen[inst] s
⊢ ∃ i ∈ c.atlas, ∃ (i_1 : Set H), IsOpen[inst] i_1 ∧ (↑e : M → H) ⁻¹' s ∩ e.source = (↑i : M → H) ⁻¹' i_1 ∩ i.source

Tactic:
exact ⟨e, he, ⟨s, s_open, 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
c : ChartedSpaceCore H M
e_1 e : PartialEquiv M H
he : e ∈ c.atlas
this : TopologicalSpace M := c.toTopologicalSpace
h :
  ∀ (t : Set M),
    Membership.mem (γ := Set (Set M))
        (⋃ e ∈ c.atlas, ⋃ (s : Set H), ⋃ (_ : IsOpen[inst] s), {(↑e : M → H) ⁻¹' s ∩ e.source}) t →
      IsOpen[inst] (e.target ∩ e.invFun ⁻¹' t)
⊢ ContinuousOn e.invFun e.target

Tactic:
apply continuousOn_isOpen_of_generateFrom

Premises used: continuousOn_isOpen_of_generateFrom
-- 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
c : ChartedSpaceCore H M
e_1 e : PartialEquiv M H
he : e ∈ c.atlas
this : TopologicalSpace M := c.toTopologicalSpace
t : Set M
ht :
  Membership.mem (γ := Set (Set M))
    (⋃ e ∈ c.atlas, ⋃ (s : Set H), ⋃ (_ : IsOpen[inst] s), {(↑e : M → H) ⁻¹' s ∩ e.source}) t
⊢ ∃ i ∈ c.atlas, ∃ (i_1 : Set H), IsOpen[inst] i_1 ∧ t = (↑i : M → H) ⁻¹' i_1 ∩ i.source

Tactic:
simp only [exists_prop, mem_iUnion, mem_singleton_iff] at ht

Premises used: Set.mem_iUnion, exists_prop, Set.mem_singleton_iff
-- 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
c : ChartedSpaceCore H M
e_1 e : PartialEquiv M H
he : e ∈ c.atlas
this : TopologicalSpace M := c.toTopologicalSpace
t : Set M
ht : ∃ i ∈ c.atlas, ∃ (i_1 : Set H), IsOpen[inst] i_1 ∧ t = (↑i : M → H) ⁻¹' i_1 ∩ i.source
h :
  ∀ (e' : PartialEquiv M H) (e'_atlas : e' ∈ c.atlas) (s : Set H) (s_open : IsOpen[inst] s)
    (ts : t = (↑e' : M → H) ⁻¹' s ∩ e'.source), IsOpen[inst] (e.target ∩ e.invFun ⁻¹' t)
⊢ IsOpen[inst] (e.target ∩ e.invFun ⁻¹' t)

Tactic:
rcases ht with ⟨e', e'_atlas, s, s_open, ts⟩
-- 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
c : ChartedSpaceCore H M
e_1 e : PartialEquiv M H
he : e ∈ c.atlas
this : TopologicalSpace M := c.toTopologicalSpace
t : Set M
e' : PartialEquiv M H
e'_atlas : e' ∈ c.atlas
s : Set H
s_open : IsOpen[inst] s
ts : t = (↑e' : M → H) ⁻¹' s ∩ e'.source
h : IsOpen[inst] (e.target ∩ e.invFun ⁻¹' ((↑e' : M → H) ⁻¹' s ∩ e'.source))
⊢ IsOpen[inst] (e.target ∩ e.invFun ⁻¹' t)

Tactic:
rw [ts]
-- 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
c : ChartedSpaceCore H M
e_1 e : PartialEquiv M H
he : e ∈ c.atlas
this : TopologicalSpace M := c.toTopologicalSpace
t : Set M
e' : PartialEquiv M H
e'_atlas : e' ∈ c.atlas
s : Set H
s_open : IsOpen[inst] s
ts : t = (↑e' : M → H) ⁻¹' s ∩ e'.source
f : PartialEquiv H H := e.symm ≫ e'
⊢ IsOpen[inst] ((↑f : H → H) ⁻¹' s ∩ f.source)

Tactic:
simpa [f, inter_comm] using (continuousOn_open_iff (c.open_source e e' he e'_atlas)).1
          (c.continuousOn_toFun e e' he e'_atlas) s s_open

Premises used: ChartedSpaceCore.continuousOn_toFun, Set.inter_comm, Iff.mp, ChartedSpaceCore.open_source, continuousOn_open_iff
-- 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
c : ChartedSpaceCore H M
e_1 e : PartialEquiv M H
he : e ∈ c.atlas
this : TopologicalSpace M := c.toTopologicalSpace
t : Set M
e' : PartialEquiv M H
e'_atlas : e' ∈ c.atlas
s : Set H
s_open : IsOpen[inst] s
ts : t = (↑e' : M → H) ⁻¹' s ∩ e'.source
f : PartialEquiv H H := e.symm ≫ e'
⊢ IsOpen[inst] ((↑f : H → H) ⁻¹' s ∩ f.source)

Tactic:
have : IsOpen (f ⁻¹' s ∩ f.source) := by
        simpa [f, inter_comm] using (continuousOn_open_iff (c.open_source e e' he e'_atlas)).1
          (c.continuousOn_toFun e e' he e'_atlas) s s_open
-- 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
c : ChartedSpaceCore H M
e_1 e : PartialEquiv M H
he : e ∈ c.atlas
this_1 : TopologicalSpace M := c.toTopologicalSpace
t : Set M
e' : PartialEquiv M H
e'_atlas : e' ∈ c.atlas
s : Set H
s_open : IsOpen[inst] s
ts : t = (↑e' : M → H) ⁻¹' s ∩ e'.source
f : PartialEquiv H H := e.symm ≫ e'
this : IsOpen[inst] ((↑f : H → H) ⁻¹' s ∩ f.source)
rw :
  (↑e' : M → H) ∘ (↑e.symm : H → M) ⁻¹' s ∩ e.target ∩ (↑e.symm : H → M) ⁻¹' e'.source =
    e.target ∩ (↑e' : M → H) ∘ (↑e.symm : H → M) ⁻¹' s ∩ (↑e.symm : H → M) ⁻¹' e'.source
⊢ (↑e' : M → H) ∘ (↑e.symm : H → M) ⁻¹' s ∩ (e.target ∩ (↑e.symm : H → M) ⁻¹' e'.source) =
    e.target ∩ ((↑e' : M → H) ∘ (↑e.symm : H → M) ⁻¹' s ∩ (↑e.symm : H → M) ⁻¹' e'.source)

Tactic:
rw [← inter_assoc, ← inter_assoc]

Premises used: Set.inter_assoc
-- 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
c : ChartedSpaceCore H M
e_1 e : PartialEquiv M H
he : e ∈ c.atlas
this_1 : TopologicalSpace M := c.toTopologicalSpace
t : Set M
e' : PartialEquiv M H
e'_atlas : e' ∈ c.atlas
s : Set H
s_open : IsOpen[inst] s
ts : t = (↑e' : M → H) ⁻¹' s ∩ e'.source
f : PartialEquiv H H := e.symm ≫ e'
this : IsOpen[inst] ((↑f : H → H) ⁻¹' s ∩ f.source)
e_a : (↑e' : M → H) ∘ (↑e.symm : H → M) ⁻¹' s ∩ e.target = e.target ∩ (↑e' : M → H) ∘ (↑e.symm : H → M) ⁻¹' s
⊢ (↑e' : M → H) ∘ (↑e.symm : H → M) ⁻¹' s ∩ e.target ∩ (↑e.symm : H → M) ⁻¹' e'.source =
    e.target ∩ (↑e' : M → H) ∘ (↑e.symm : H → M) ⁻¹' s ∩ (↑e.symm : H → M) ⁻¹' e'.source

Tactic:
congr 1
-- 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
c : ChartedSpaceCore H M
e_1 e : PartialEquiv M H
he : e ∈ c.atlas
this_1 : TopologicalSpace M := c.toTopologicalSpace
t : Set M
e' : PartialEquiv M H
e'_atlas : e' ∈ c.atlas
s : Set H
s_open : IsOpen[inst] s
ts : t = (↑e' : M → H) ⁻¹' s ∩ e'.source
f : PartialEquiv H H := e.symm ≫ e'
this : IsOpen[inst] ((↑f : H → H) ⁻¹' s ∩ f.source)
⊢ (↑e' : M → H) ∘ (↑e.symm : H → M) ⁻¹' s ∩ e.target = e.target ∩ (↑e' : M → H) ∘ (↑e.symm : H → M) ⁻¹' s

Tactic:
inter_comm _ _

Premises used: Set.inter_comm
-- 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
c : ChartedSpaceCore H M
e_1 e : PartialEquiv M H
he : e ∈ c.atlas
this_1 : TopologicalSpace M := c.toTopologicalSpace
t : Set M
e' : PartialEquiv M H
e'_atlas : e' ∈ c.atlas
s : Set H
s_open : IsOpen[inst] s
ts : t = (↑e' : M → H) ⁻¹' s ∩ e'.source
f : PartialEquiv H H := e.symm ≫ e'
this : IsOpen[inst] ((↑f : H → H) ⁻¹' s ∩ f.source)
⊢ (↑e' : M → H) ∘ (↑e.symm : H → M) ⁻¹' s ∩ e.target = e.target ∩ (↑e' : M → H) ∘ (↑e.symm : H → M) ⁻¹' s

Tactic:
exact inter_comm _ _

Premises used: Set.inter_comm