-- Mathlib/Geometry/Manifold/LocalInvariantProperties.lean
theorem HasGroupoid.comp
    (H : ∀ e ∈ G₂, LiftPropOn (IsLocalStructomorphWithinAt G₁) (e : H₂ → H₂) e.source) :
    @HasGroupoid H₁ _ H₃ _ (ChartedSpace.comp H₁ H₂ H₃) G₁ :=
  let _ := ChartedSpace.comp H₁ H₂ H₃ -- Porting note: need this to synthesize `ChartedSpace H₁ H₃`
  { compatible

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro
H₁ : Type u_6
inst✝⁷ : TopologicalSpace H₁
H₂ : Type u_7
inst✝⁶ : TopologicalSpace H₂
H₃ : Type u_8
inst✝⁵ : TopologicalSpace H₃
inst✝⁴ : ChartedSpace H₁ H₂
inst✝³ : ChartedSpace H₂ H₃
G₁ : StructureGroupoid H₁
inst✝² : HasGroupoid H₂ G₁
inst✝¹ : ClosedUnderRestriction G₁
G₂ : StructureGroupoid H₂
inst✝ : HasGroupoid H₃ G₂
H : ∀ e ∈ G₂, LiftPropOn G₁.IsLocalStructomorphWithinAt (↑e) e.source
x✝ : ChartedSpace H₁ H₃ := ChartedSpace.comp H₁ H₂ H₃
e : PartialHomeomorph H₃ H₂
he : e ∈ atlas H₂ H₃
f : PartialHomeomorph H₂ H₁
hf : f ∈ atlas H₁ H₂
e' : PartialHomeomorph H₃ H₂
he' : e' ∈ atlas H₂ H₃
f' : PartialHomeomorph H₂ H₁
hf' : f' ∈ atlas H₁ H₂
⊢ ∀ x ∈ ((e ≫ₕ f).symm ≫ₕ e' ≫ₕ f').source, ∃ s, IsOpen s ∧ x ∈ s ∧ ((e ≫ₕ f).symm ≫ₕ e' ≫ₕ f').restr s ∈ G₁

Tactic:
intro x hx

Result:
case intro.intro.intro.intro.intro.intro.intro.intro
H₁ : Type u_6
inst✝⁷ : TopologicalSpace H₁
H₂ : Type u_7
inst✝⁶ : TopologicalSpace H₂
H₃ : Type u_8
inst✝⁵ : TopologicalSpace H₃
inst✝⁴ : ChartedSpace H₁ H₂
inst✝³ : ChartedSpace H₂ H₃
G₁ : StructureGroupoid H₁
inst✝² : HasGroupoid H₂ G₁
inst✝¹ : ClosedUnderRestriction G₁
G₂ : StructureGroupoid H₂
inst✝ : HasGroupoid H₃ G₂
H : ∀ e ∈ G₂, LiftPropOn G₁.IsLocalStructomorphWithinAt (↑e) e.source
x✝ : ChartedSpace H₁ H₃ := ChartedSpace.comp H₁ H₂ H₃
e : PartialHomeomorph H₃ H₂
he : e ∈ atlas H₂ H₃
f : PartialHomeomorph H₂ H₁
hf : f ∈ atlas H₁ H₂
e' : PartialHomeomorph H₃ H₂
he' : e' ∈ atlas H₂ H₃
f' : PartialHomeomorph H₂ H₁
hf' : f' ∈ atlas H₁ H₂
x : H₁
hx : x ∈ ((e ≫ₕ f).symm ≫ₕ e' ≫ₕ f').source
⊢ ∃ s, IsOpen s ∧ x ∈ s ∧ ((e ≫ₕ f).symm ≫ₕ e' ≫ₕ f').restr s ∈ G₁

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro
H₁ : Type u_6
inst✝⁷ : TopologicalSpace H₁
H₂ : Type u_7
inst✝⁶ : TopologicalSpace H₂
H₃ : Type u_8
inst✝⁵ : TopologicalSpace H₃
inst✝⁴ : ChartedSpace H₁ H₂
inst✝³ : ChartedSpace H₂ H₃
G₁ : StructureGroupoid H₁
inst✝² : HasGroupoid H₂ G₁
inst✝¹ : ClosedUnderRestriction G₁
G₂ : StructureGroupoid H₂
inst✝ : HasGroupoid H₃ G₂
H : ∀ e ∈ G₂, LiftPropOn G₁.IsLocalStructomorphWithinAt (↑e) e.source
x✝ : ChartedSpace H₁ H₃ := ChartedSpace.comp H₁ H₂ H₃
e : PartialHomeomorph H₃ H₂
he : e ∈ atlas H₂ H₃
f : PartialHomeomorph H₂ H₁
hf : f ∈ atlas H₁ H₂
e' : PartialHomeomorph H₃ H₂
he' : e' ∈ atlas H₂ H₃
f' : PartialHomeomorph H₂ H₁
hf' : f' ∈ atlas H₁ H₂
x : H₁
hx : (x ∈ f.target ∧ ↑f.symm x ∈ e.target) ∧ ↑e.symm (↑f.symm x) ∈ e'.source ∧ ↑e' (↑e.symm (↑f.symm x)) ∈ f'.source
hxs : x ∈ ↑f.symm ⁻¹' (e.symm ≫ₕ e').source
hxs' : x ∈ f.target ∩ ↑f.symm ⁻¹' ((e.symm ≫ₕ e').source ∩ ↑(e.symm ≫ₕ e') ⁻¹' f'.source)
⊢ ∃ s, IsOpen 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

Result:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
H₁ : Type u_6
inst✝⁷ : TopologicalSpace H₁
H₂ : Type u_7
inst✝⁶ : TopologicalSpace H₂
H₃ : Type u_8
inst✝⁵ : TopologicalSpace H₃
inst✝⁴ : ChartedSpace H₁ H₂
inst✝³ : ChartedSpace H₂ H₃
G₁ : StructureGroupoid H₁
inst✝² : HasGroupoid H₂ G₁
inst✝¹ : ClosedUnderRestriction G₁
G₂ : StructureGroupoid H₂
inst✝ : HasGroupoid H₃ G₂
H : ∀ e ∈ G₂, LiftPropOn G₁.IsLocalStructomorphWithinAt (↑e) e.source
x✝ : ChartedSpace H₁ H₃ := ChartedSpace.comp H₁ H₂ H₃
e : PartialHomeomorph H₃ H₂
he : e ∈ atlas H₂ H₃
f : PartialHomeomorph H₂ H₁
hf : f ∈ atlas H₁ H₂
e' : PartialHomeomorph H₃ H₂
he' : e' ∈ atlas H₂ H₃
f' : PartialHomeomorph H₂ H₁
hf' : f' ∈ atlas H₁ H₂
x : H₁
hx : (x ∈ f.target ∧ ↑f.symm x ∈ e.target) ∧ ↑e.symm (↑f.symm x) ∈ e'.source ∧ ↑e' (↑e.symm (↑f.symm x)) ∈ f'.source
hxs : x ∈ ↑f.symm ⁻¹' (e.symm ≫ₕ e').source
hxs' : x ∈ f.target ∩ ↑f.symm ⁻¹' ((e.symm ≫ₕ e').source ∩ ↑(e.symm ≫ₕ e') ⁻¹' f'.source)
φ : PartialHomeomorph H₁ H₁
hφG₁ : φ ∈ G₁
hφ : EqOn (↑f' ∘ ↑(e.symm ≫ₕ e') ∘ ↑f.symm) (↑φ.toPartialEquiv) (↑f.symm ⁻¹' (e.symm ≫ₕ e').source ∩ φ.source)
hφ_dom : x ∈ φ.source
⊢ ∃ s, IsOpen s ∧ x ∈ s ∧ ((e ≫ₕ f).symm ≫ₕ e' ≫ₕ f').restr s ∈ G₁

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro
H₁ : Type u_6
inst✝⁷ : TopologicalSpace H₁
H₂ : Type u_7
inst✝⁶ : TopologicalSpace H₂
H₃ : Type u_8
inst✝⁵ : TopologicalSpace H₃
inst✝⁴ : ChartedSpace H₁ H₂
inst✝³ : ChartedSpace H₂ H₃
G₁ : StructureGroupoid H₁
inst✝² : HasGroupoid H₂ G₁
inst✝¹ : ClosedUnderRestriction G₁
G₂ : StructureGroupoid H₂
inst✝ : HasGroupoid H₃ G₂
H : ∀ e ∈ G₂, LiftPropOn G₁.IsLocalStructomorphWithinAt (↑e) e.source
x✝ : ChartedSpace H₁ H₃ := ChartedSpace.comp H₁ H₂ H₃
e : PartialHomeomorph H₃ H₂
he : e ∈ atlas H₂ H₃
f : PartialHomeomorph H₂ H₁
hf : f ∈ atlas H₁ H₂
e' : PartialHomeomorph H₃ H₂
he' : e' ∈ atlas H₂ H₃
f' : PartialHomeomorph H₂ H₁
hf' : f' ∈ atlas H₁ H₂
x : H₁
hx : (x ∈ f.target ∧ ↑f.symm x ∈ e.target) ∧ ↑e.symm (↑f.symm x) ∈ e'.source ∧ ↑e' (↑e.symm (↑f.symm x)) ∈ f'.source
hxs : x ∈ ↑f.symm ⁻¹' (e.symm ≫ₕ e').source
⊢ ∃ s, IsOpen s ∧ x ∈ s ∧ ((e ≫ₕ f).symm ≫ₕ e' ≫ₕ f').restr s ∈ G₁

Tactic:
have hxs' : x ∈ f.target ∩ f.symm ⁻¹' ((e.symm ≫ₕ e').source ∩ e.symm ≫ₕ e' ⁻¹' f'.source) :=
  by simp only [hx, mfld_simps]

Result:
case intro.intro.intro.intro.intro.intro.intro.intro
H₁ : Type u_6
inst✝⁷ : TopologicalSpace H₁
H₂ : Type u_7
inst✝⁶ : TopologicalSpace H₂
H₃ : Type u_8
inst✝⁵ : TopologicalSpace H₃
inst✝⁴ : ChartedSpace H₁ H₂
inst✝³ : ChartedSpace H₂ H₃
G₁ : StructureGroupoid H₁
inst✝² : HasGroupoid H₂ G₁
inst✝¹ : ClosedUnderRestriction G₁
G₂ : StructureGroupoid H₂
inst✝ : HasGroupoid H₃ G₂
H : ∀ e ∈ G₂, LiftPropOn G₁.IsLocalStructomorphWithinAt (↑e) e.source
x✝ : ChartedSpace H₁ H₃ := ChartedSpace.comp H₁ H₂ H₃
e : PartialHomeomorph H₃ H₂
he : e ∈ atlas H₂ H₃
f : PartialHomeomorph H₂ H₁
hf : f ∈ atlas H₁ H₂
e' : PartialHomeomorph H₃ H₂
he' : e' ∈ atlas H₂ H₃
f' : PartialHomeomorph H₂ H₁
hf' : f' ∈ atlas H₁ H₂
x : H₁
hx : (x ∈ f.target ∧ ↑f.symm x ∈ e.target) ∧ ↑e.symm (↑f.symm x) ∈ e'.source ∧ ↑e' (↑e.symm (↑f.symm x)) ∈ f'.source
hxs : x ∈ ↑f.symm ⁻¹' (e.symm ≫ₕ e').source
hxs' : x ∈ f.target ∩ ↑f.symm ⁻¹' ((e.symm ≫ₕ e').source ∩ ↑(e.symm ≫ₕ e') ⁻¹' f'.source)
⊢ ∃ s, IsOpen s ∧ x ∈ s ∧ ((e ≫ₕ f).symm ≫ₕ e' ≫ₕ f').restr s ∈ G₁