awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H₁ : Type u_6
inst : TopologicalSpace H₁
H₂ : Type u_7
inst_1 : TopologicalSpace H₂
H₃ : Type u_8
inst_2 : TopologicalSpace H₃
inst_3 : ChartedSpace H₁ H₂
inst_4 : ChartedSpace H₂ H₃
G₁ : StructureGroupoid H₁
inst_5 : HasGroupoid H₂ G₁
inst_6 : ClosedUnderRestriction G₁
G₂ : StructureGroupoid H₂
inst_7 : HasGroupoid H₃ G₂
H : ∀ e ∈ G₂, LiftPropOn G₁.IsLocalStructomorphWithinAt (↑e : H₂ → H₂) e.source
x_1 : ChartedSpace H₁ H₃ := ChartedSpace.comp H₁ H₂ H₃
e : OpenPartialHomeomorph H₃ H₂
he : Membership.mem (γ := Set (OpenPartialHomeomorph H₃ H₂)) (atlas H₂ H₃) e
f : OpenPartialHomeomorph H₂ H₁
hf : Membership.mem (γ := Set (OpenPartialHomeomorph H₂ H₁)) (atlas H₁ H₂) f
e' : OpenPartialHomeomorph H₃ H₂
he' : Membership.mem (γ := Set (OpenPartialHomeomorph H₃ H₂)) (atlas H₂ H₃) e'
f' : OpenPartialHomeomorph H₂ H₁
hf' : Membership.mem (γ := Set (OpenPartialHomeomorph H₂ H₁)) (atlas H₁ H₂) f'
x : H₁
hx :
  (x ∈ f.target ∧ (↑f.symm : H₁ → H₂) x ∈ e.target) ∧
    (↑e.symm : H₂ → H₃) ((↑f.symm : H₁ → H₂) x) ∈ e'.source ∧
      (↑e' : H₃ → H₂) ((↑e.symm : H₂ → H₃) ((↑f.symm : H₁ → H₂) x)) ∈ f'.source
hxs : x ∈ (↑f.symm : H₁ → H₂) ⁻¹' (e.symm ≫ₕ e').source
hxs' : x ∈ f.target ∩ (↑f.symm : H₁ → H₂) ⁻¹' ((e.symm ≫ₕ e').source ∩ (↑(e.symm ≫ₕ e') : H₂ → H₂) ⁻¹' f'.source)
obtain :
  ∀ (φ : OpenPartialHomeomorph H₁ H₁) (hφG₁ : φ ∈ G₁)
    (hφ :
      EqOn ((↑f' : H₂ → H₁) ∘ (↑(e.symm ≫ₕ e') : H₂ → H₂) ∘ (↑f.symm : H₁ → H₂)) (↑φ.toPartialEquiv : H₁ → H₁)
        ((↑f.symm : H₁ → H₂) ⁻¹' (e.symm ≫ₕ e').source ∩ φ.source))
    (hφ_dom : x ∈ φ.source), ∃ (s : Set H₁), IsOpen[inst] s ∧ x ∈ s ∧ ((e ≫ₕ f).symm ≫ₕ e' ≫ₕ f').restr s ∈ G₁
⊢ ∃ (s : Set H₁), IsOpen[inst] s ∧ x ∈ s ∧ ((e ≫ₕ f).symm ≫ₕ e' ≫ₕ f').restr s ∈ G₁

Tactic:
obtain ⟨φ, hφG₁, hφ, hφ_dom⟩ := LocalInvariantProp.liftPropOn_indep_chart
        (isLocalStructomorphWithinAt_localInvariantProp G₁) (G₁.subset_maximalAtlas hf)
        (G₁.subset_maximalAtlas hf') (H _ (G₂.compatible he he')) hxs' hxs

Premises used: StructureGroupoid.LocalInvariantProp.liftPropOn_indep_chart, StructureGroupoid.compatible, StructureGroupoid.subset_maximalAtlas, StructureGroupoid.isLocalStructomorphWithinAt_localInvariantProp
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H₁ : Type u_6
inst : TopologicalSpace H₁
H₂ : Type u_7
inst_1 : TopologicalSpace H₂
H₃ : Type u_8
inst_2 : TopologicalSpace H₃
inst_3 : ChartedSpace H₁ H₂
inst_4 : ChartedSpace H₂ H₃
G₁ : StructureGroupoid H₁
inst_5 : HasGroupoid H₂ G₁
inst_6 : ClosedUnderRestriction G₁
G₂ : StructureGroupoid H₂
inst_7 : HasGroupoid H₃ G₂
H : ∀ e ∈ G₂, LiftPropOn G₁.IsLocalStructomorphWithinAt (↑e : H₂ → H₂) e.source
x_1 : ChartedSpace H₁ H₃ := ChartedSpace.comp H₁ H₂ H₃
e : OpenPartialHomeomorph H₃ H₂
he : Membership.mem (γ := Set (OpenPartialHomeomorph H₃ H₂)) (atlas H₂ H₃) e
f : OpenPartialHomeomorph H₂ H₁
hf : Membership.mem (γ := Set (OpenPartialHomeomorph H₂ H₁)) (atlas H₁ H₂) f
e' : OpenPartialHomeomorph H₃ H₂
he' : Membership.mem (γ := Set (OpenPartialHomeomorph H₃ H₂)) (atlas H₂ H₃) e'
f' : OpenPartialHomeomorph H₂ H₁
hf' : Membership.mem (γ := Set (OpenPartialHomeomorph H₂ H₁)) (atlas H₁ H₂) f'
x : H₁
hx :
  (x ∈ f.target ∧ (↑f.symm : H₁ → H₂) x ∈ e.target) ∧
    (↑e.symm : H₂ → H₃) ((↑f.symm : H₁ → H₂) x) ∈ e'.source ∧
      (↑e' : H₃ → H₂) ((↑e.symm : H₂ → H₃) ((↑f.symm : H₁ → H₂) x)) ∈ f'.source
hxs : x ∈ (↑f.symm : H₁ → H₂) ⁻¹' (e.symm ≫ₕ e').source
hxs' : x ∈ f.target ∩ (↑f.symm : H₁ → H₂) ⁻¹' ((e.symm ≫ₕ e').source ∩ (↑(e.symm ≫ₕ e') : H₂ → H₂) ⁻¹' f'.source)
φ : OpenPartialHomeomorph H₁ H₁
hφG₁ : φ ∈ G₁
hφ :
  EqOn ((↑f' : H₂ → H₁) ∘ (↑(e.symm ≫ₕ e') : H₂ → H₂) ∘ (↑f.symm : H₁ → H₂)) (↑φ.toPartialEquiv : H₁ → H₁)
    ((↑f.symm : H₁ → H₂) ⁻¹' (e.symm ≫ₕ e').source ∩ φ.source)
hφ_dom : x ∈ φ.source
⊢ EqOn (↑(f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f') : H₁ → H₁) (↑φ.toPartialEquiv : H₁ → H₁)
    ((↑f.symm : H₁ → H₂) ⁻¹' (e.symm ≫ₕ e').source ∩ φ.source)

Tactic:
simp_rw [← OpenPartialHomeomorph.coe_trans, OpenPartialHomeomorph.trans_assoc] at hφ

Premises used: OpenPartialHomeomorph.trans_assoc, OpenPartialHomeomorph.coe_trans
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H₁ : Type u_6
inst : TopologicalSpace H₁
H₂ : Type u_7
inst_1 : TopologicalSpace H₂
H₃ : Type u_8
inst_2 : TopologicalSpace H₃
inst_3 : ChartedSpace H₁ H₂
inst_4 : ChartedSpace H₂ H₃
G₁ : StructureGroupoid H₁
inst_5 : HasGroupoid H₂ G₁
inst_6 : ClosedUnderRestriction G₁
G₂ : StructureGroupoid H₂
inst_7 : HasGroupoid H₃ G₂
H : ∀ e ∈ G₂, LiftPropOn G₁.IsLocalStructomorphWithinAt (↑e : H₂ → H₂) e.source
x_1 : ChartedSpace H₁ H₃ := ChartedSpace.comp H₁ H₂ H₃
e : OpenPartialHomeomorph H₃ H₂
he : Membership.mem (γ := Set (OpenPartialHomeomorph H₃ H₂)) (atlas H₂ H₃) e
f : OpenPartialHomeomorph H₂ H₁
hf : Membership.mem (γ := Set (OpenPartialHomeomorph H₂ H₁)) (atlas H₁ H₂) f
e' : OpenPartialHomeomorph H₃ H₂
he' : Membership.mem (γ := Set (OpenPartialHomeomorph H₃ H₂)) (atlas H₂ H₃) e'
f' : OpenPartialHomeomorph H₂ H₁
hf' : Membership.mem (γ := Set (OpenPartialHomeomorph H₂ H₁)) (atlas H₁ H₂) f'
x : H₁
hx :
  (x ∈ f.target ∧ (↑f.symm : H₁ → H₂) x ∈ e.target) ∧
    (↑e.symm : H₂ → H₃) ((↑f.symm : H₁ → H₂) x) ∈ e'.source ∧
      (↑e' : H₃ → H₂) ((↑e.symm : H₂ → H₃) ((↑f.symm : H₁ → H₂) x)) ∈ f'.source
hxs : x ∈ (↑f.symm : H₁ → H₂) ⁻¹' (e.symm ≫ₕ e').source
hxs' : x ∈ f.target ∩ (↑f.symm : H₁ → H₂) ⁻¹' ((e.symm ≫ₕ e').source ∩ (↑(e.symm ≫ₕ e') : H₂ → H₂) ⁻¹' f'.source)
φ : OpenPartialHomeomorph H₁ H₁
hφG₁ : φ ∈ G₁
hφ_dom : x ∈ φ.source
hφ :
  EqOn (↑(f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f') : H₁ → H₁) (↑φ.toPartialEquiv : H₁ → H₁)
    ((↑f.symm : H₁ → H₂) ⁻¹' (e.symm ≫ₕ e').source ∩ φ.source)
simp_rw : ∃ (s : Set H₁), IsOpen[inst] s ∧ x ∈ s ∧ (f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f').restr s ∈ G₁
⊢ ∃ (s : Set H₁), IsOpen[inst] s ∧ x ∈ s ∧ ((e ≫ₕ f).symm ≫ₕ e' ≫ₕ f').restr s ∈ G₁

Tactic:
simp_rw [OpenPartialHomeomorph.trans_symm_eq_symm_trans_symm,
        OpenPartialHomeomorph.trans_assoc]

Premises used: OpenPartialHomeomorph.trans_assoc, OpenPartialHomeomorph.trans_symm_eq_symm_trans_symm
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H₁ : Type u_6
inst : TopologicalSpace H₁
H₂ : Type u_7
inst_1 : TopologicalSpace H₂
H₃ : Type u_8
inst_2 : TopologicalSpace H₃
inst_3 : ChartedSpace H₁ H₂
inst_4 : ChartedSpace H₂ H₃
G₁ : StructureGroupoid H₁
inst_5 : HasGroupoid H₂ G₁
inst_6 : ClosedUnderRestriction G₁
G₂ : StructureGroupoid H₂
inst_7 : HasGroupoid H₃ G₂
H : ∀ e ∈ G₂, LiftPropOn G₁.IsLocalStructomorphWithinAt (↑e : H₂ → H₂) e.source
x_1 : ChartedSpace H₁ H₃ := ChartedSpace.comp H₁ H₂ H₃
e : OpenPartialHomeomorph H₃ H₂
he : Membership.mem (γ := Set (OpenPartialHomeomorph H₃ H₂)) (atlas H₂ H₃) e
f : OpenPartialHomeomorph H₂ H₁
hf : Membership.mem (γ := Set (OpenPartialHomeomorph H₂ H₁)) (atlas H₁ H₂) f
e' : OpenPartialHomeomorph H₃ H₂
he' : Membership.mem (γ := Set (OpenPartialHomeomorph H₃ H₂)) (atlas H₂ H₃) e'
f' : OpenPartialHomeomorph H₂ H₁
hf' : Membership.mem (γ := Set (OpenPartialHomeomorph H₂ H₁)) (atlas H₁ H₂) f'
x : H₁
hx :
  (x ∈ f.target ∧ (↑f.symm : H₁ → H₂) x ∈ e.target) ∧
    (↑e.symm : H₂ → H₃) ((↑f.symm : H₁ → H₂) x) ∈ e'.source ∧
      (↑e' : H₃ → H₂) ((↑e.symm : H₂ → H₃) ((↑f.symm : H₁ → H₂) x)) ∈ f'.source
hxs : x ∈ (↑f.symm : H₁ → H₂) ⁻¹' (e.symm ≫ₕ e').source
hxs' : x ∈ f.target ∩ (↑f.symm : H₁ → H₂) ⁻¹' ((e.symm ≫ₕ e').source ∩ (↑(e.symm ≫ₕ e') : H₂ → H₂) ⁻¹' f'.source)
φ : OpenPartialHomeomorph H₁ H₁
hφG₁ : φ ∈ G₁
hφ_dom : x ∈ φ.source
hφ :
  EqOn (↑(f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f') : H₁ → H₁) (↑φ.toPartialEquiv : H₁ → H₁)
    ((↑f.symm : H₁ → H₂) ⁻¹' (e.symm ≫ₕ e').source ∩ φ.source)
⊢ IsOpen[inst] (f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f').source

Tactic:
have hs : IsOpen (f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f').source :=
        (f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f').open_source
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H₁ : Type u_6
inst : TopologicalSpace H₁
H₂ : Type u_7
inst_1 : TopologicalSpace H₂
H₃ : Type u_8
inst_2 : TopologicalSpace H₃
inst_3 : ChartedSpace H₁ H₂
inst_4 : ChartedSpace H₂ H₃
G₁ : StructureGroupoid H₁
inst_5 : HasGroupoid H₂ G₁
inst_6 : ClosedUnderRestriction G₁
G₂ : StructureGroupoid H₂
inst_7 : HasGroupoid H₃ G₂
H : ∀ e ∈ G₂, LiftPropOn G₁.IsLocalStructomorphWithinAt (↑e : H₂ → H₂) e.source
x_1 : ChartedSpace H₁ H₃ := ChartedSpace.comp H₁ H₂ H₃
e : OpenPartialHomeomorph H₃ H₂
he : Membership.mem (γ := Set (OpenPartialHomeomorph H₃ H₂)) (atlas H₂ H₃) e
f : OpenPartialHomeomorph H₂ H₁
hf : Membership.mem (γ := Set (OpenPartialHomeomorph H₂ H₁)) (atlas H₁ H₂) f
e' : OpenPartialHomeomorph H₃ H₂
he' : Membership.mem (γ := Set (OpenPartialHomeomorph H₃ H₂)) (atlas H₂ H₃) e'
f' : OpenPartialHomeomorph H₂ H₁
hf' : Membership.mem (γ := Set (OpenPartialHomeomorph H₂ H₁)) (atlas H₁ H₂) f'
x : H₁
hx :
  (x ∈ f.target ∧ (↑f.symm : H₁ → H₂) x ∈ e.target) ∧
    (↑e.symm : H₂ → H₃) ((↑f.symm : H₁ → H₂) x) ∈ e'.source ∧
      (↑e' : H₃ → H₂) ((↑e.symm : H₂ → H₃) ((↑f.symm : H₁ → H₂) x)) ∈ f'.source
hxs : x ∈ (↑f.symm : H₁ → H₂) ⁻¹' (e.symm ≫ₕ e').source
hxs' : x ∈ f.target ∩ (↑f.symm : H₁ → H₂) ⁻¹' ((e.symm ≫ₕ e').source ∩ (↑(e.symm ≫ₕ e') : H₂ → H₂) ⁻¹' f'.source)
φ : OpenPartialHomeomorph H₁ H₁
hφG₁ : φ ∈ G₁
hφ_dom : x ∈ φ.source
hφ :
  EqOn (↑(f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f') : H₁ → H₁) (↑φ.toPartialEquiv : H₁ → H₁)
    ((↑f.symm : H₁ → H₂) ⁻¹' (e.symm ≫ₕ e').source ∩ φ.source)
hs : IsOpen[inst] (f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f').source
⊢ ∃ (s : Set H₁), IsOpen[inst] s ∧ x ∈ s ∧ (f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f').restr s ∈ G₁

Tactic:
⟨_, hs.inter φ.open_source, ?_, ?_⟩

Premises used: OpenPartialHomeomorph.open_source, And.intro, IsOpen.inter, Exists.intro
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H₁ : Type u_6
inst : TopologicalSpace H₁
H₂ : Type u_7
inst_1 : TopologicalSpace H₂
H₃ : Type u_8
inst_2 : TopologicalSpace H₃
inst_3 : ChartedSpace H₁ H₂
inst_4 : ChartedSpace H₂ H₃
G₁ : StructureGroupoid H₁
inst_5 : HasGroupoid H₂ G₁
inst_6 : ClosedUnderRestriction G₁
G₂ : StructureGroupoid H₂
inst_7 : HasGroupoid H₃ G₂
H : ∀ e ∈ G₂, LiftPropOn G₁.IsLocalStructomorphWithinAt (↑e : H₂ → H₂) e.source
x_1 : ChartedSpace H₁ H₃ := ChartedSpace.comp H₁ H₂ H₃
e : OpenPartialHomeomorph H₃ H₂
he : Membership.mem (γ := Set (OpenPartialHomeomorph H₃ H₂)) (atlas H₂ H₃) e
f : OpenPartialHomeomorph H₂ H₁
hf : Membership.mem (γ := Set (OpenPartialHomeomorph H₂ H₁)) (atlas H₁ H₂) f
e' : OpenPartialHomeomorph H₃ H₂
he' : Membership.mem (γ := Set (OpenPartialHomeomorph H₃ H₂)) (atlas H₂ H₃) e'
f' : OpenPartialHomeomorph H₂ H₁
hf' : Membership.mem (γ := Set (OpenPartialHomeomorph H₂ H₁)) (atlas H₁ H₂) f'
x : H₁
hx :
  (x ∈ f.target ∧ (↑f.symm : H₁ → H₂) x ∈ e.target) ∧
    (↑e.symm : H₂ → H₃) ((↑f.symm : H₁ → H₂) x) ∈ e'.source ∧
      (↑e' : H₃ → H₂) ((↑e.symm : H₂ → H₃) ((↑f.symm : H₁ → H₂) x)) ∈ f'.source
hxs : x ∈ (↑f.symm : H₁ → H₂) ⁻¹' (e.symm ≫ₕ e').source
hxs' : x ∈ f.target ∩ (↑f.symm : H₁ → H₂) ⁻¹' ((e.symm ≫ₕ e').source ∩ (↑(e.symm ≫ₕ e') : H₂ → H₂) ⁻¹' f'.source)
φ : OpenPartialHomeomorph H₁ H₁
hφG₁ : φ ∈ G₁
hφ_dom : x ∈ φ.source
hφ :
  EqOn (↑(f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f') : H₁ → H₁) (↑φ.toPartialEquiv : H₁ → H₁)
    ((↑f.symm : H₁ → H₂) ⁻¹' (e.symm ≫ₕ e').source ∩ φ.source)
hs : IsOpen[inst] (f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f').source
refine_1 : x ∈ (f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f').source ∩ φ.source
refine_2 : (f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f').restr ((f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f').source ∩ φ.source) ∈ G₁
⊢ ∃ (s : Set H₁), IsOpen[inst] s ∧ x ∈ s ∧ (f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f').restr s ∈ G₁

Tactic:
refine ⟨_, hs.inter φ.open_source, ?_, ?_⟩
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H₁ : Type u_6
inst : TopologicalSpace H₁
H₂ : Type u_7
inst_1 : TopologicalSpace H₂
H₃ : Type u_8
inst_2 : TopologicalSpace H₃
inst_3 : ChartedSpace H₁ H₂
inst_4 : ChartedSpace H₂ H₃
G₁ : StructureGroupoid H₁
inst_5 : HasGroupoid H₂ G₁
inst_6 : ClosedUnderRestriction G₁
G₂ : StructureGroupoid H₂
inst_7 : HasGroupoid H₃ G₂
H : ∀ e ∈ G₂, LiftPropOn G₁.IsLocalStructomorphWithinAt (↑e : H₂ → H₂) e.source
x_1 : ChartedSpace H₁ H₃ := ChartedSpace.comp H₁ H₂ H₃
e : OpenPartialHomeomorph H₃ H₂
he : Membership.mem (γ := Set (OpenPartialHomeomorph H₃ H₂)) (atlas H₂ H₃) e
f : OpenPartialHomeomorph H₂ H₁
hf : Membership.mem (γ := Set (OpenPartialHomeomorph H₂ H₁)) (atlas H₁ H₂) f
e' : OpenPartialHomeomorph H₃ H₂
he' : Membership.mem (γ := Set (OpenPartialHomeomorph H₃ H₂)) (atlas H₂ H₃) e'
f' : OpenPartialHomeomorph H₂ H₁
hf' : Membership.mem (γ := Set (OpenPartialHomeomorph H₂ H₁)) (atlas H₁ H₂) f'
x : H₁
hx :
  (x ∈ f.target ∧ (↑f.symm : H₁ → H₂) x ∈ e.target) ∧
    (↑e.symm : H₂ → H₃) ((↑f.symm : H₁ → H₂) x) ∈ e'.source ∧
      (↑e' : H₃ → H₂) ((↑e.symm : H₂ → H₃) ((↑f.symm : H₁ → H₂) x)) ∈ f'.source
hxs : x ∈ (↑f.symm : H₁ → H₂) ⁻¹' (e.symm ≫ₕ e').source
hxs' : x ∈ f.target ∩ (↑f.symm : H₁ → H₂) ⁻¹' ((e.symm ≫ₕ e').source ∩ (↑(e.symm ≫ₕ e') : H₂ → H₂) ⁻¹' f'.source)
φ : OpenPartialHomeomorph H₁ H₁
hφG₁ : φ ∈ G₁
hφ_dom : x ∈ φ.source
hφ :
  EqOn (↑(f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f') : H₁ → H₁) (↑φ.toPartialEquiv : H₁ → H₁)
    ((↑f.symm : H₁ → H₂) ⁻¹' (e.symm ≫ₕ e').source ∩ φ.source)
hs : IsOpen[inst] (f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f').source
⊢ x ∈ (f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f').source ∩ φ.source

Tactic:
simp only [hx, hφ_dom, mfld_simps]
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H₁ : Type u_6
inst : TopologicalSpace H₁
H₂ : Type u_7
inst_1 : TopologicalSpace H₂
H₃ : Type u_8
inst_2 : TopologicalSpace H₃
inst_3 : ChartedSpace H₁ H₂
inst_4 : ChartedSpace H₂ H₃
G₁ : StructureGroupoid H₁
inst_5 : HasGroupoid H₂ G₁
inst_6 : ClosedUnderRestriction G₁
G₂ : StructureGroupoid H₂
inst_7 : HasGroupoid H₃ G₂
H : ∀ e ∈ G₂, LiftPropOn G₁.IsLocalStructomorphWithinAt (↑e : H₂ → H₂) e.source
x_1 : ChartedSpace H₁ H₃ := ChartedSpace.comp H₁ H₂ H₃
e : OpenPartialHomeomorph H₃ H₂
he : Membership.mem (γ := Set (OpenPartialHomeomorph H₃ H₂)) (atlas H₂ H₃) e
f : OpenPartialHomeomorph H₂ H₁
hf : Membership.mem (γ := Set (OpenPartialHomeomorph H₂ H₁)) (atlas H₁ H₂) f
e' : OpenPartialHomeomorph H₃ H₂
he' : Membership.mem (γ := Set (OpenPartialHomeomorph H₃ H₂)) (atlas H₂ H₃) e'
f' : OpenPartialHomeomorph H₂ H₁
hf' : Membership.mem (γ := Set (OpenPartialHomeomorph H₂ H₁)) (atlas H₁ H₂) f'
x : H₁
hx :
  (x ∈ f.target ∧ (↑f.symm : H₁ → H₂) x ∈ e.target) ∧
    (↑e.symm : H₂ → H₃) ((↑f.symm : H₁ → H₂) x) ∈ e'.source ∧
      (↑e' : H₃ → H₂) ((↑e.symm : H₂ → H₃) ((↑f.symm : H₁ → H₂) x)) ∈ f'.source
hxs : x ∈ (↑f.symm : H₁ → H₂) ⁻¹' (e.symm ≫ₕ e').source
hxs' : x ∈ f.target ∩ (↑f.symm : H₁ → H₂) ⁻¹' ((e.symm ≫ₕ e').source ∩ (↑(e.symm ≫ₕ e') : H₂ → H₂) ⁻¹' f'.source)
φ : OpenPartialHomeomorph H₁ H₁
hφG₁ : φ ∈ G₁
hφ_dom : x ∈ φ.source
hφ :
  EqOn (↑(f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f') : H₁ → H₁) (↑φ.toPartialEquiv : H₁ → H₁)
    ((↑f.symm : H₁ → H₂) ⁻¹' (e.symm ≫ₕ e').source ∩ φ.source)
hs : IsOpen[inst] (f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f').source
⊢ (f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f').restr ((f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f').source ∩ φ.source) ∈ G₁

Tactic:
G₁.mem_of_eqOnSource (closedUnderRestriction' hφG₁ hs) ?_

Premises used: StructureGroupoid.mem_of_eqOnSource, closedUnderRestriction'
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H₁ : Type u_6
inst : TopologicalSpace H₁
H₂ : Type u_7
inst_1 : TopologicalSpace H₂
H₃ : Type u_8
inst_2 : TopologicalSpace H₃
inst_3 : ChartedSpace H₁ H₂
inst_4 : ChartedSpace H₂ H₃
G₁ : StructureGroupoid H₁
inst_5 : HasGroupoid H₂ G₁
inst_6 : ClosedUnderRestriction G₁
G₂ : StructureGroupoid H₂
inst_7 : HasGroupoid H₃ G₂
H : ∀ e ∈ G₂, LiftPropOn G₁.IsLocalStructomorphWithinAt (↑e : H₂ → H₂) e.source
x_1 : ChartedSpace H₁ H₃ := ChartedSpace.comp H₁ H₂ H₃
e : OpenPartialHomeomorph H₃ H₂
he : Membership.mem (γ := Set (OpenPartialHomeomorph H₃ H₂)) (atlas H₂ H₃) e
f : OpenPartialHomeomorph H₂ H₁
hf : Membership.mem (γ := Set (OpenPartialHomeomorph H₂ H₁)) (atlas H₁ H₂) f
e' : OpenPartialHomeomorph H₃ H₂
he' : Membership.mem (γ := Set (OpenPartialHomeomorph H₃ H₂)) (atlas H₂ H₃) e'
f' : OpenPartialHomeomorph H₂ H₁
hf' : Membership.mem (γ := Set (OpenPartialHomeomorph H₂ H₁)) (atlas H₁ H₂) f'
x : H₁
hx :
  (x ∈ f.target ∧ (↑f.symm : H₁ → H₂) x ∈ e.target) ∧
    (↑e.symm : H₂ → H₃) ((↑f.symm : H₁ → H₂) x) ∈ e'.source ∧
      (↑e' : H₃ → H₂) ((↑e.symm : H₂ → H₃) ((↑f.symm : H₁ → H₂) x)) ∈ f'.source
hxs : x ∈ (↑f.symm : H₁ → H₂) ⁻¹' (e.symm ≫ₕ e').source
hxs' : x ∈ f.target ∩ (↑f.symm : H₁ → H₂) ⁻¹' ((e.symm ≫ₕ e').source ∩ (↑(e.symm ≫ₕ e') : H₂ → H₂) ⁻¹' f'.source)
φ : OpenPartialHomeomorph H₁ H₁
hφG₁ : φ ∈ G₁
hφ_dom : x ∈ φ.source
hφ :
  EqOn (↑(f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f') : H₁ → H₁) (↑φ.toPartialEquiv : H₁ → H₁)
    ((↑f.symm : H₁ → H₂) ⁻¹' (e.symm ≫ₕ e').source ∩ φ.source)
hs : IsOpen[inst] (f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f').source
refine_2 :
  (f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f').restr ((f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f').source ∩ φ.source) ≈
    φ.restr (f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f').source
⊢ (f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f').restr ((f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f').source ∩ φ.source) ∈ G₁

Tactic:
refine G₁.mem_of_eqOnSource (closedUnderRestriction' hφG₁ hs) ?_

Premises used: StructureGroupoid.mem_of_eqOnSource, closedUnderRestriction'
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H₁ : Type u_6
inst : TopologicalSpace H₁
H₂ : Type u_7
inst_1 : TopologicalSpace H₂
H₃ : Type u_8
inst_2 : TopologicalSpace H₃
inst_3 : ChartedSpace H₁ H₂
inst_4 : ChartedSpace H₂ H₃
G₁ : StructureGroupoid H₁
inst_5 : HasGroupoid H₂ G₁
inst_6 : ClosedUnderRestriction G₁
G₂ : StructureGroupoid H₂
inst_7 : HasGroupoid H₃ G₂
H : ∀ e ∈ G₂, LiftPropOn G₁.IsLocalStructomorphWithinAt (↑e : H₂ → H₂) e.source
x_1 : ChartedSpace H₁ H₃ := ChartedSpace.comp H₁ H₂ H₃
e : OpenPartialHomeomorph H₃ H₂
he : Membership.mem (γ := Set (OpenPartialHomeomorph H₃ H₂)) (atlas H₂ H₃) e
f : OpenPartialHomeomorph H₂ H₁
hf : Membership.mem (γ := Set (OpenPartialHomeomorph H₂ H₁)) (atlas H₁ H₂) f
e' : OpenPartialHomeomorph H₃ H₂
he' : Membership.mem (γ := Set (OpenPartialHomeomorph H₃ H₂)) (atlas H₂ H₃) e'
f' : OpenPartialHomeomorph H₂ H₁
hf' : Membership.mem (γ := Set (OpenPartialHomeomorph H₂ H₁)) (atlas H₁ H₂) f'
x : H₁
hx :
  (x ∈ f.target ∧ (↑f.symm : H₁ → H₂) x ∈ e.target) ∧
    (↑e.symm : H₂ → H₃) ((↑f.symm : H₁ → H₂) x) ∈ e'.source ∧
      (↑e' : H₃ → H₂) ((↑e.symm : H₂ → H₃) ((↑f.symm : H₁ → H₂) x)) ∈ f'.source
hxs : x ∈ (↑f.symm : H₁ → H₂) ⁻¹' (e.symm ≫ₕ e').source
hxs' : x ∈ f.target ∩ (↑f.symm : H₁ → H₂) ⁻¹' ((e.symm ≫ₕ e').source ∩ (↑(e.symm ≫ₕ e') : H₂ → H₂) ⁻¹' f'.source)
φ : OpenPartialHomeomorph H₁ H₁
hφG₁ : φ ∈ G₁
hφ_dom : x ∈ φ.source
hφ :
  EqOn (↑(f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f') : H₁ → H₁) (↑φ.toPartialEquiv : H₁ → H₁)
    ((↑f.symm : H₁ → H₂) ⁻¹' (e.symm ≫ₕ e').source ∩ φ.source)
hs : IsOpen[inst] (f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f').source
refine_2 : (f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f').restr φ.source ≈ φ.restr (f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f').source
⊢ (f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f').restr ((f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f').source ∩ φ.source) ≈
    φ.restr (f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f').source

Tactic:
rw [OpenPartialHomeomorph.restr_source_inter]

Premises used: OpenPartialHomeomorph.restr_source_inter
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H₁ : Type u_6
inst : TopologicalSpace H₁
H₂ : Type u_7
inst_1 : TopologicalSpace H₂
H₃ : Type u_8
inst_2 : TopologicalSpace H₃
inst_3 : ChartedSpace H₁ H₂
inst_4 : ChartedSpace H₂ H₃
G₁ : StructureGroupoid H₁
inst_5 : HasGroupoid H₂ G₁
inst_6 : ClosedUnderRestriction G₁
G₂ : StructureGroupoid H₂
inst_7 : HasGroupoid H₃ G₂
H : ∀ e ∈ G₂, LiftPropOn G₁.IsLocalStructomorphWithinAt (↑e : H₂ → H₂) e.source
x_1 : ChartedSpace H₁ H₃ := ChartedSpace.comp H₁ H₂ H₃
e : OpenPartialHomeomorph H₃ H₂
he : Membership.mem (γ := Set (OpenPartialHomeomorph H₃ H₂)) (atlas H₂ H₃) e
f : OpenPartialHomeomorph H₂ H₁
hf : Membership.mem (γ := Set (OpenPartialHomeomorph H₂ H₁)) (atlas H₁ H₂) f
e' : OpenPartialHomeomorph H₃ H₂
he' : Membership.mem (γ := Set (OpenPartialHomeomorph H₃ H₂)) (atlas H₂ H₃) e'
f' : OpenPartialHomeomorph H₂ H₁
hf' : Membership.mem (γ := Set (OpenPartialHomeomorph H₂ H₁)) (atlas H₁ H₂) f'
x : H₁
hx :
  (x ∈ f.target ∧ (↑f.symm : H₁ → H₂) x ∈ e.target) ∧
    (↑e.symm : H₂ → H₃) ((↑f.symm : H₁ → H₂) x) ∈ e'.source ∧
      (↑e' : H₃ → H₂) ((↑e.symm : H₂ → H₃) ((↑f.symm : H₁ → H₂) x)) ∈ f'.source
hxs : x ∈ (↑f.symm : H₁ → H₂) ⁻¹' (e.symm ≫ₕ e').source
hxs' : x ∈ f.target ∩ (↑f.symm : H₁ → H₂) ⁻¹' ((e.symm ≫ₕ e').source ∩ (↑(e.symm ≫ₕ e') : H₂ → H₂) ⁻¹' f'.source)
φ : OpenPartialHomeomorph H₁ H₁
hφG₁ : φ ∈ G₁
hφ_dom : x ∈ φ.source
hφ :
  EqOn (↑(f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f') : H₁ → H₁) (↑φ.toPartialEquiv : H₁ → H₁)
    ((↑f.symm : H₁ → H₂) ⁻¹' (e.symm ≫ₕ e').source ∩ φ.source)
hs : IsOpen[inst] (f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f').source
⊢ (f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f').restr φ.source ≈ φ.restr (f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f').source

Tactic:
OpenPartialHomeomorph.Set.EqOn.restr_eqOn_source (hφ.mono ?_)

Premises used: OpenPartialHomeomorph.Set.EqOn.restr_eqOn_source, Set.EqOn.mono
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H₁ : Type u_6
inst : TopologicalSpace H₁
H₂ : Type u_7
inst_1 : TopologicalSpace H₂
H₃ : Type u_8
inst_2 : TopologicalSpace H₃
inst_3 : ChartedSpace H₁ H₂
inst_4 : ChartedSpace H₂ H₃
G₁ : StructureGroupoid H₁
inst_5 : HasGroupoid H₂ G₁
inst_6 : ClosedUnderRestriction G₁
G₂ : StructureGroupoid H₂
inst_7 : HasGroupoid H₃ G₂
H : ∀ e ∈ G₂, LiftPropOn G₁.IsLocalStructomorphWithinAt (↑e : H₂ → H₂) e.source
x_1 : ChartedSpace H₁ H₃ := ChartedSpace.comp H₁ H₂ H₃
e : OpenPartialHomeomorph H₃ H₂
he : Membership.mem (γ := Set (OpenPartialHomeomorph H₃ H₂)) (atlas H₂ H₃) e
f : OpenPartialHomeomorph H₂ H₁
hf : Membership.mem (γ := Set (OpenPartialHomeomorph H₂ H₁)) (atlas H₁ H₂) f
e' : OpenPartialHomeomorph H₃ H₂
he' : Membership.mem (γ := Set (OpenPartialHomeomorph H₃ H₂)) (atlas H₂ H₃) e'
f' : OpenPartialHomeomorph H₂ H₁
hf' : Membership.mem (γ := Set (OpenPartialHomeomorph H₂ H₁)) (atlas H₁ H₂) f'
x : H₁
hx :
  (x ∈ f.target ∧ (↑f.symm : H₁ → H₂) x ∈ e.target) ∧
    (↑e.symm : H₂ → H₃) ((↑f.symm : H₁ → H₂) x) ∈ e'.source ∧
      (↑e' : H₃ → H₂) ((↑e.symm : H₂ → H₃) ((↑f.symm : H₁ → H₂) x)) ∈ f'.source
hxs : x ∈ (↑f.symm : H₁ → H₂) ⁻¹' (e.symm ≫ₕ e').source
hxs' : x ∈ f.target ∩ (↑f.symm : H₁ → H₂) ⁻¹' ((e.symm ≫ₕ e').source ∩ (↑(e.symm ≫ₕ e') : H₂ → H₂) ⁻¹' f'.source)
φ : OpenPartialHomeomorph H₁ H₁
hφG₁ : φ ∈ G₁
hφ_dom : x ∈ φ.source
hφ :
  EqOn (↑(f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f') : H₁ → H₁) (↑φ.toPartialEquiv : H₁ → H₁)
    ((↑f.symm : H₁ → H₂) ⁻¹' (e.symm ≫ₕ e').source ∩ φ.source)
hs : IsOpen[inst] (f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f').source
refine_2 : (f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f').source ∩ φ.source ⊆ (↑f.symm : H₁ → H₂) ⁻¹' (e.symm ≫ₕ e').source ∩ φ.source
⊢ (f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f').restr φ.source ≈ φ.restr (f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f').source

Tactic:
refine OpenPartialHomeomorph.Set.EqOn.restr_eqOn_source (hφ.mono ?_)

Premises used: OpenPartialHomeomorph.Set.EqOn.restr_eqOn_source, Set.EqOn.mono