awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.HasGroupoid (goal)
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 : ChartedSpace H M
inst_3 : TopologicalSpace M'
inst_4 : TopologicalSpace M''
G : StructureGroupoid H
inst_5 : ChartedSpace H M'
inst_6 : ChartedSpace H M''
e : Structomorph G M M'
e' : Structomorph G M' M''
c : OpenPartialHomeomorph M H
c' : OpenPartialHomeomorph M'' H
hc : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) c
hc' : Membership.mem (γ := Set (OpenPartialHomeomorph M'' H)) (atlas H M'') c'
x : H
hx : x ∈ (c.symm ≫ₕ (e.trans e'.toHomeomorph).toOpenPartialHomeomorph ≫ₕ c').source
f₁ : OpenPartialHomeomorph M M' := e.toOpenPartialHomeomorph
f₂ : OpenPartialHomeomorph M' M'' := e'.toOpenPartialHomeomorph
f : OpenPartialHomeomorph M M'' := (e.trans e'.toHomeomorph).toOpenPartialHomeomorph
feq : f = f₁ ≫ₕ f₂
y : M' := (↑(c.symm ≫ₕ f₁) : H → M') x
g : OpenPartialHomeomorph M' H := chartAt H y
hg₁ : Membership.mem (γ := Set (OpenPartialHomeomorph M' H)) (atlas H M') (chartAt H y)
hg₂ : y ∈ (toPartialEquiv (chartAt H y)).source
s : Set H := (c.symm ≫ₕ f₁).source ∩ (↑(c.symm ≫ₕ f₁) : H → M') ⁻¹' g.source
hs : IsOpen[inst] (c.symm ≫ₕ f₁).source
⊢ IsOpen[inst] s
have ht : IsOpen[inst_3] g.source
Tactic: apply (c.symm ≫ₕ f₁).continuousOn_toFun.isOpen_inter_preimage
-- Lean 4 proof step from Mathlib.Geometry.Manifold.HasGroupoid (hypothesis)
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 : ChartedSpace H M
inst_3 : TopologicalSpace M'
inst_4 : TopologicalSpace M''
G : StructureGroupoid H
inst_5 : ChartedSpace H M'
inst_6 : ChartedSpace H M''
e : Structomorph G M M'
e' : Structomorph G M' M''
c : OpenPartialHomeomorph M H
c' : OpenPartialHomeomorph M'' H
hc : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) c
hc' : Membership.mem (γ := Set (OpenPartialHomeomorph M'' H)) (atlas H M'') c'
x : H
hx : x ∈ (c.symm ≫ₕ (e.trans e'.toHomeomorph).toOpenPartialHomeomorph ≫ₕ c').source
f₁ : OpenPartialHomeomorph M M' := e.toOpenPartialHomeomorph
f₂ : OpenPartialHomeomorph M' M'' := e'.toOpenPartialHomeomorph
f : OpenPartialHomeomorph M M'' := (e.trans e'.toHomeomorph).toOpenPartialHomeomorph
feq : f = f₁ ≫ₕ f₂
y : M' := (↑(c.symm ≫ₕ f₁) : H → M') x
g : OpenPartialHomeomorph M' H := chartAt H y
hg₁ : Membership.mem (γ := Set (OpenPartialHomeomorph M' H)) (atlas H M') (chartAt H y)
hg₂ : y ∈ (toPartialEquiv (chartAt H y)).source
s : Set H := (c.symm ≫ₕ f₁).source ∩ (↑(c.symm ≫ₕ f₁) : H → M') ⁻¹' g.source
⊢ ∃ (s : Set H),
    IsOpen[inst] s ∧ x ∈ s ∧ (c.symm ≫ₕ (e.trans e'.toHomeomorph).toOpenPartialHomeomorph ≫ₕ c').restr s ∈ G
have open_s : IsOpen[inst] s
Tactic: have open_s : IsOpen s := by
        apply (c.symm ≫ₕ f₁).continuousOn_toFun.isOpen_inter_preimage <;> apply open_source
-- Lean 4 proof step from Mathlib.Geometry.Manifold.HasGroupoid (goal)
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 : ChartedSpace H M
inst_3 : TopologicalSpace M'
inst_4 : TopologicalSpace M''
G : StructureGroupoid H
inst_5 : ChartedSpace H M'
inst_6 : ChartedSpace H M''
e : Structomorph G M M'
e' : Structomorph G M' M''
c : OpenPartialHomeomorph M H
c' : OpenPartialHomeomorph M'' H
hc : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) c
hc' : Membership.mem (γ := Set (OpenPartialHomeomorph M'' H)) (atlas H M'') c'
x : H
hx : x ∈ (c.symm ≫ₕ (e.trans e'.toHomeomorph).toOpenPartialHomeomorph ≫ₕ c').source
f₁ : OpenPartialHomeomorph M M' := e.toOpenPartialHomeomorph
f₂ : OpenPartialHomeomorph M' M'' := e'.toOpenPartialHomeomorph
f : OpenPartialHomeomorph M M'' := (e.trans e'.toHomeomorph).toOpenPartialHomeomorph
feq : f = f₁ ≫ₕ f₂
y : M' := (↑(c.symm ≫ₕ f₁) : H → M') x
g : OpenPartialHomeomorph M' H := chartAt H y
hg₁ : Membership.mem (γ := Set (OpenPartialHomeomorph M' H)) (atlas H M') (chartAt H y)
hg₂ : y ∈ (toPartialEquiv (chartAt H y)).source
s : Set H := (c.symm ≫ₕ f₁).source ∩ (↑(c.symm ≫ₕ f₁) : H → M') ⁻¹' g.source
open_s : IsOpen[inst] s
⊢ x ∈ s
have left : x ∈ (c.symm ≫ₕ f₁).source
Tactic: constructor
-- Lean 4 proof step from Mathlib.Geometry.Manifold.HasGroupoid (goal)
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 : ChartedSpace H M
inst_3 : TopologicalSpace M'
inst_4 : TopologicalSpace M''
G : StructureGroupoid H
inst_5 : ChartedSpace H M'
inst_6 : ChartedSpace H M''
e : Structomorph G M M'
e' : Structomorph G M' M''
c : OpenPartialHomeomorph M H
c' : OpenPartialHomeomorph M'' H
hc : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) c
hc' : Membership.mem (γ := Set (OpenPartialHomeomorph M'' H)) (atlas H M'') c'
x : H
hx : x ∈ (c.symm ≫ₕ (e.trans e'.toHomeomorph).toOpenPartialHomeomorph ≫ₕ c').source
f₁ : OpenPartialHomeomorph M M' := e.toOpenPartialHomeomorph
f₂ : OpenPartialHomeomorph M' M'' := e'.toOpenPartialHomeomorph
f : OpenPartialHomeomorph M M'' := (e.trans e'.toHomeomorph).toOpenPartialHomeomorph
feq : f = f₁ ≫ₕ f₂
y : M' := (↑(c.symm ≫ₕ f₁) : H → M') x
g : OpenPartialHomeomorph M' H := chartAt H y
hg₁ : Membership.mem (γ := Set (OpenPartialHomeomorph M' H)) (atlas H M') (chartAt H y)
hg₂ : y ∈ (toPartialEquiv (chartAt H y)).source
s : Set H := (c.symm ≫ₕ f₁).source ∩ (↑(c.symm ≫ₕ f₁) : H → M') ⁻¹' g.source
open_s : IsOpen[inst] s
left : x ∈ (c.symm ≫ₕ f₁).source
⊢ x ∈ s
have right : x ∈ (↑(c.symm ≫ₕ f₁) : H → M') ⁻¹' g.source
Tactic: constructor
-- Lean 4 proof step from Mathlib.Geometry.Manifold.HasGroupoid (goal)
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 : ChartedSpace H M
inst_3 : TopologicalSpace M'
inst_4 : TopologicalSpace M''
G : StructureGroupoid H
inst_5 : ChartedSpace H M'
inst_6 : ChartedSpace H M''
e : Structomorph G M M'
e' : Structomorph G M' M''
c : OpenPartialHomeomorph M H
c' : OpenPartialHomeomorph M'' H
hc : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) c
hc' : Membership.mem (γ := Set (OpenPartialHomeomorph M'' H)) (atlas H M'') c'
x : H
hx : x ∈ (c.symm ≫ₕ (e.trans e'.toHomeomorph).toOpenPartialHomeomorph ≫ₕ c').source
f₁ : OpenPartialHomeomorph M M' := e.toOpenPartialHomeomorph
f₂ : OpenPartialHomeomorph M' M'' := e'.toOpenPartialHomeomorph
f : OpenPartialHomeomorph M M'' := (e.trans e'.toHomeomorph).toOpenPartialHomeomorph
feq : f = f₁ ≫ₕ f₂
y : M' := (↑(c.symm ≫ₕ f₁) : H → M') x
g : OpenPartialHomeomorph M' H := chartAt H y
hg₁ : Membership.mem (γ := Set (OpenPartialHomeomorph M' H)) (atlas H M') (chartAt H y)
hg₂ : y ∈ (toPartialEquiv (chartAt H y)).source
s : Set H := (c.symm ≫ₕ f₁).source ∩ (↑(c.symm ≫ₕ f₁) : H → M') ⁻¹' g.source
open_s : IsOpen[inst] s
⊢ x ∈ (c.symm ≫ₕ f₁).source
have left : x ∈ c.symm.source
Tactic: simp only [f₁, trans_source, preimage_univ, inter_univ,
            Homeomorph.toOpenPartialHomeomorph_source]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.HasGroupoid (hypothesis)
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 : ChartedSpace H M
inst_3 : TopologicalSpace M'
inst_4 : TopologicalSpace M''
G : StructureGroupoid H
inst_5 : ChartedSpace H M'
inst_6 : ChartedSpace H M''
e : Structomorph G M M'
e' : Structomorph G M' M''
c : OpenPartialHomeomorph M H
c' : OpenPartialHomeomorph M'' H
hc : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) c
hc' : Membership.mem (γ := Set (OpenPartialHomeomorph M'' H)) (atlas H M'') c'
x : H
hx : x ∈ (c.symm ≫ₕ (e.trans e'.toHomeomorph).toOpenPartialHomeomorph ≫ₕ c').source
f₁ : OpenPartialHomeomorph M M' := e.toOpenPartialHomeomorph
f₂ : OpenPartialHomeomorph M' M'' := e'.toOpenPartialHomeomorph
f : OpenPartialHomeomorph M M'' := (e.trans e'.toHomeomorph).toOpenPartialHomeomorph
feq : f = f₁ ≫ₕ f₂
y : M' := (↑(c.symm ≫ₕ f₁) : H → M') x
g : OpenPartialHomeomorph M' H := chartAt H y
hg₁ : Membership.mem (γ := Set (OpenPartialHomeomorph M' H)) (atlas H M') (chartAt H y)
hg₂ : y ∈ (toPartialEquiv (chartAt H y)).source
s : Set H := (c.symm ≫ₕ f₁).source ∩ (↑(c.symm ≫ₕ f₁) : H → M') ⁻¹' g.source
open_s : IsOpen[inst] s
⊢ x ∈ c.symm.source
have hx₁ : x ∈ c.symm.source ∩ (↑c.symm : H → M) ⁻¹' ((e.trans e'.toHomeomorph).toOpenPartialHomeomorph ≫ₕ c').source
Tactic: rw [trans_source] at hx
Cleared hypotheses: hx, f₁, f₂, f, feq, y, g, hg₁, hg₂, s, open_s
-- Lean 4 proof step from Mathlib.Geometry.Manifold.HasGroupoid (hypothesis)
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 : ChartedSpace H M
inst_3 : TopologicalSpace M'
inst_4 : TopologicalSpace M''
G : StructureGroupoid H
inst_5 : ChartedSpace H M'
inst_6 : ChartedSpace H M''
e : Structomorph G M M'
e' : Structomorph G M' M''
c : OpenPartialHomeomorph M H
c' : OpenPartialHomeomorph M'' H
hc : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) c
hc' : Membership.mem (γ := Set (OpenPartialHomeomorph M'' H)) (atlas H M'') c'
x : H
hx : x ∈ (c.symm ≫ₕ (e.trans e'.toHomeomorph).toOpenPartialHomeomorph ≫ₕ c').source
f₁ : OpenPartialHomeomorph M M' := e.toOpenPartialHomeomorph
f₂ : OpenPartialHomeomorph M' M'' := e'.toOpenPartialHomeomorph
f : OpenPartialHomeomorph M M'' := (e.trans e'.toHomeomorph).toOpenPartialHomeomorph
feq : f = f₁ ≫ₕ f₂
y : M' := (↑(c.symm ≫ₕ f₁) : H → M') x
g : OpenPartialHomeomorph M' H := chartAt H y
hg₁ : Membership.mem (γ := Set (OpenPartialHomeomorph M' H)) (atlas H M') (chartAt H y)
hg₂ : y ∈ (toPartialEquiv (chartAt H y)).source
s : Set H := (c.symm ≫ₕ f₁).source ∩ (↑(c.symm ≫ₕ f₁) : H → M') ⁻¹' g.source
open_s : IsOpen[inst] s
⊢ ∃ (s : Set H),
    IsOpen[inst] s ∧ x ∈ s ∧ (c.symm ≫ₕ (e.trans e'.toHomeomorph).toOpenPartialHomeomorph ≫ₕ c').restr s ∈ G
have this : x ∈ s
Tactic: have : x ∈ s := by
        constructor
        · simp only [f₁, trans_source, preimage_univ, inter_univ,
            Homeomorph.toOpenPartialHomeomorph_source]
          rw [trans_source] at hx
          exact hx.1
        · exact hg₂
-- Lean 4 proof step from Mathlib.Geometry.Manifold.HasGroupoid (goal)
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 : ChartedSpace H M
inst_3 : TopologicalSpace M'
inst_4 : TopologicalSpace M''
G : StructureGroupoid H
inst_5 : ChartedSpace H M'
inst_6 : ChartedSpace H M''
e : Structomorph G M M'
e' : Structomorph G M' M''
c : OpenPartialHomeomorph M H
c' : OpenPartialHomeomorph M'' H
hc : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) c
hc' : Membership.mem (γ := Set (OpenPartialHomeomorph M'' H)) (atlas H M'') c'
x : H
hx : x ∈ (c.symm ≫ₕ (e.trans e'.toHomeomorph).toOpenPartialHomeomorph ≫ₕ c').source
f₁ : OpenPartialHomeomorph M M' := e.toOpenPartialHomeomorph
f₂ : OpenPartialHomeomorph M' M'' := e'.toOpenPartialHomeomorph
f : OpenPartialHomeomorph M M'' := (e.trans e'.toHomeomorph).toOpenPartialHomeomorph
feq : f = f₁ ≫ₕ f₂
y : M' := (↑(c.symm ≫ₕ f₁) : H → M') x
g : OpenPartialHomeomorph M' H := chartAt H y
hg₁ : Membership.mem (γ := Set (OpenPartialHomeomorph M' H)) (atlas H M') (chartAt H y)
hg₂ : y ∈ (toPartialEquiv (chartAt H y)).source
s : Set H := (c.symm ≫ₕ f₁).source ∩ (↑(c.symm ≫ₕ f₁) : H → M') ⁻¹' g.source
open_s : IsOpen[inst] s
this : x ∈ s
⊢ ∃ (s : Set H),
    IsOpen[inst] s ∧ x ∈ s ∧ (c.symm ≫ₕ (e.trans e'.toHomeomorph).toOpenPartialHomeomorph ≫ₕ c').restr s ∈ G
have refine : (c.symm ≫ₕ (e.trans e'.toHomeomorph).toOpenPartialHomeomorph ≫ₕ c').restr s ∈ G
Tactic: refine ⟨s, open_s, this, ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.HasGroupoid (hypothesis)
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 : ChartedSpace H M
inst_3 : TopologicalSpace M'
inst_4 : TopologicalSpace M''
G : StructureGroupoid H
inst_5 : ChartedSpace H M'
inst_6 : ChartedSpace H M''
e : Structomorph G M M'
e' : Structomorph G M' M''
c : OpenPartialHomeomorph M H
c' : OpenPartialHomeomorph M'' H
hc : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) c
hc' : Membership.mem (γ := Set (OpenPartialHomeomorph M'' H)) (atlas H M'') c'
x : H
hx : x ∈ (c.symm ≫ₕ (e.trans e'.toHomeomorph).toOpenPartialHomeomorph ≫ₕ c').source
f₁ : OpenPartialHomeomorph M M' := e.toOpenPartialHomeomorph
f₂ : OpenPartialHomeomorph M' M'' := e'.toOpenPartialHomeomorph
f : OpenPartialHomeomorph M M'' := (e.trans e'.toHomeomorph).toOpenPartialHomeomorph
feq : f = f₁ ≫ₕ f₂
y : M' := (↑(c.symm ≫ₕ f₁) : H → M') x
g : OpenPartialHomeomorph M' H := chartAt H y
hg₁ : Membership.mem (γ := Set (OpenPartialHomeomorph M' H)) (atlas H M') (chartAt H y)
hg₂ : y ∈ (toPartialEquiv (chartAt H y)).source
s : Set H := (c.symm ≫ₕ f₁).source ∩ (↑(c.symm ≫ₕ f₁) : H → M') ⁻¹' g.source
open_s : IsOpen[inst] s
this : x ∈ s
F₁ : OpenPartialHomeomorph H H := (c.symm ≫ₕ f₁ ≫ₕ g) ≫ₕ g.symm ≫ₕ f₂ ≫ₕ c'
⊢ (c.symm ≫ₕ (e.trans e'.toHomeomorph).toOpenPartialHomeomorph ≫ₕ c').restr s ∈ G
have A : F₁ ∈ G
Tactic: have A : F₁ ∈ G := G.trans (e.mem_groupoid c g hc hg₁) (e'.mem_groupoid g c' hg₁ hc')
-- Lean 4 proof step from Mathlib.Geometry.Manifold.HasGroupoid (goal)
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 : ChartedSpace H M
inst_3 : TopologicalSpace M'
inst_4 : TopologicalSpace M''
G : StructureGroupoid H
inst_5 : ChartedSpace H M'
inst_6 : ChartedSpace H M''
e : Structomorph G M M'
e' : Structomorph G M' M''
c : OpenPartialHomeomorph M H
c' : OpenPartialHomeomorph M'' H
hc : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) c
hc' : Membership.mem (γ := Set (OpenPartialHomeomorph M'' H)) (atlas H M'') c'
x : H
hx : x ∈ (c.symm ≫ₕ (e.trans e'.toHomeomorph).toOpenPartialHomeomorph ≫ₕ c').source
f₁ : OpenPartialHomeomorph M M' := e.toOpenPartialHomeomorph
f₂ : OpenPartialHomeomorph M' M'' := e'.toOpenPartialHomeomorph
f : OpenPartialHomeomorph M M'' := (e.trans e'.toHomeomorph).toOpenPartialHomeomorph
feq : f = f₁ ≫ₕ f₂
y : M' := (↑(c.symm ≫ₕ f₁) : H → M') x
g : OpenPartialHomeomorph M' H := chartAt H y
hg₁ : Membership.mem (γ := Set (OpenPartialHomeomorph M' H)) (atlas H M') (chartAt H y)
hg₂ : y ∈ (toPartialEquiv (chartAt H y)).source
s : Set H := (c.symm ≫ₕ f₁).source ∩ (↑(c.symm ≫ₕ f₁) : H → M') ⁻¹' g.source
open_s : IsOpen[inst] s
this : x ∈ s
F₁ : OpenPartialHomeomorph H H := (c.symm ≫ₕ f₁ ≫ₕ g) ≫ₕ g.symm ≫ₕ f₂ ≫ₕ c'
A : F₁ ∈ G
F₂ : OpenPartialHomeomorph H H := (c.symm ≫ₕ f ≫ₕ c').restr s
⊢ ((c.symm ≫ₕ f₁) ≫ₕ ofSet g.source ⋯) ≫ₕ f₂ ≫ₕ c' ≈ (c.symm ≫ₕ f₁).restr s ≫ₕ f₂ ≫ₕ c'
have rw : (eqOnSourceSetoid : OpenPartialHomeomorph H H → OpenPartialHomeomorph H H → Prop)
  ((c.symm ≫ₕ f₁).restr ((c.symm ≫ₕ f₁).source ∩ (↑(c.symm ≫ₕ f₁) : H → M') ⁻¹' g.source) ≫ₕ f₂ ≫ₕ c')
  ((c.symm ≫ₕ f₁).restr ((c.symm ≫ₕ f₁).source ∩ (↑(c.symm ≫ₕ f₁) : H → M') ⁻¹' g.source) ≫ₕ f₂ ≫ₕ c')
Tactic: rw [trans_of_set']
-- Lean 4 proof step from Mathlib.Geometry.Manifold.HasGroupoid (goal)
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 : ChartedSpace H M
inst_3 : TopologicalSpace M'
inst_4 : TopologicalSpace M''
G : StructureGroupoid H
inst_5 : ChartedSpace H M'
inst_6 : ChartedSpace H M''
e : Structomorph G M M'
e' : Structomorph G M' M''
c : OpenPartialHomeomorph M H
c' : OpenPartialHomeomorph M'' H
hc : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) c
hc' : Membership.mem (γ := Set (OpenPartialHomeomorph M'' H)) (atlas H M'') c'
x : H
hx : x ∈ (c.symm ≫ₕ (e.trans e'.toHomeomorph).toOpenPartialHomeomorph ≫ₕ c').source
f₁ : OpenPartialHomeomorph M M' := e.toOpenPartialHomeomorph
f₂ : OpenPartialHomeomorph M' M'' := e'.toOpenPartialHomeomorph
f : OpenPartialHomeomorph M M'' := (e.trans e'.toHomeomorph).toOpenPartialHomeomorph
feq : f = f₁ ≫ₕ f₂
y : M' := (↑(c.symm ≫ₕ f₁) : H → M') x
g : OpenPartialHomeomorph M' H := chartAt H y
hg₁ : Membership.mem (γ := Set (OpenPartialHomeomorph M' H)) (atlas H M') (chartAt H y)
hg₂ : y ∈ (toPartialEquiv (chartAt H y)).source
s : Set H := (c.symm ≫ₕ f₁).source ∩ (↑(c.symm ≫ₕ f₁) : H → M') ⁻¹' g.source
open_s : IsOpen[inst] s
this : x ∈ s
F₁ : OpenPartialHomeomorph H H := (c.symm ≫ₕ f₁ ≫ₕ g) ≫ₕ g.symm ≫ₕ f₂ ≫ₕ c'
A : F₁ ∈ G
F₂ : OpenPartialHomeomorph H H := (c.symm ≫ₕ f ≫ₕ c').restr s
⊢ (c.symm ≫ₕ f₁).restr s ≫ₕ f₂ ≫ₕ c' ≈ ((c.symm ≫ₕ f₁) ≫ₕ f₂ ≫ₕ c').restr s
have rw : (eqOnSourceSetoid : OpenPartialHomeomorph H H → OpenPartialHomeomorph H H → Prop) (((c.symm ≫ₕ f₁) ≫ₕ f₂ ≫ₕ c').restr s)
  (((c.symm ≫ₕ f₁) ≫ₕ f₂ ≫ₕ c').restr s)
Tactic: rw [restr_trans]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.HasGroupoid (hypothesis)
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 : ChartedSpace H M
inst_3 : TopologicalSpace M'
inst_4 : TopologicalSpace M''
G : StructureGroupoid H
inst_5 : ChartedSpace H M'
inst_6 : ChartedSpace H M''
e : Structomorph G M M'
e' : Structomorph G M' M''
c : OpenPartialHomeomorph M H
c' : OpenPartialHomeomorph M'' H
hc : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) c
hc' : Membership.mem (γ := Set (OpenPartialHomeomorph M'' H)) (atlas H M'') c'
x : H
hx : x ∈ (c.symm ≫ₕ (e.trans e'.toHomeomorph).toOpenPartialHomeomorph ≫ₕ c').source
f₁ : OpenPartialHomeomorph M M' := e.toOpenPartialHomeomorph
f₂ : OpenPartialHomeomorph M' M'' := e'.toOpenPartialHomeomorph
f : OpenPartialHomeomorph M M'' := (e.trans e'.toHomeomorph).toOpenPartialHomeomorph
feq : f = f₁ ≫ₕ f₂
y : M' := (↑(c.symm ≫ₕ f₁) : H → M') x
g : OpenPartialHomeomorph M' H := chartAt H y
hg₁ : Membership.mem (γ := Set (OpenPartialHomeomorph M' H)) (atlas H M') (chartAt H y)
hg₂ : y ∈ (toPartialEquiv (chartAt H y)).source
s : Set H := (c.symm ≫ₕ f₁).source ∩ (↑(c.symm ≫ₕ f₁) : H → M') ⁻¹' g.source
open_s : IsOpen[inst] s
this : x ∈ s
F₁ : OpenPartialHomeomorph H H := (c.symm ≫ₕ f₁ ≫ₕ g) ≫ₕ g.symm ≫ₕ f₂ ≫ₕ c'
A : F₁ ∈ G
F₂ : OpenPartialHomeomorph H H := (c.symm ≫ₕ f ≫ₕ c').restr s
⊢ (c.symm ≫ₕ (e.trans e'.toHomeomorph).toOpenPartialHomeomorph ≫ₕ c').restr s ∈ G
have this₁ : F₁ ≈ F₂
Tactic: have : F₁ ≈ F₂ := calc
        F₁ ≈ c.symm ≫ₕ f₁ ≫ₕ (g ≫ₕ g.symm) ≫ₕ f₂ ≫ₕ c' := by
            simp only [F₁, trans_assoc, _root_.refl]
        _ ≈ c.symm ≫ₕ f₁ ≫ₕ ofSet g.source g.open_source ≫ₕ f₂ ≫ₕ c' :=
          EqOnSource.trans' (_root_.refl _) (EqOnSource.trans' (_root_.refl _)
            (EqOnSource.trans' (self_trans_symm g) (_root_.refl _)))
        _ ≈ ((c.symm ≫ₕ f₁) ≫ₕ ofSet g.source g.open_source) ≫ₕ f₂ ≫ₕ c' := by
          simp only [trans_assoc, _root_.refl]
        _ ≈ (c.symm ≫ₕ f₁).restr s ≫ₕ f₂ ≫ₕ c' := by rw [trans_of_set']
        _ ≈ ((c.symm ≫ₕ f₁) ≫ₕ f₂ ≫ₕ c').restr s := by rw [restr_trans]
        _ ≈ (c.symm ≫ₕ (f₁ ≫ₕ f₂) ≫ₕ c').restr s := by
          simp only [trans_assoc, _root_.refl]
        _ ≈ F₂ := by simp only [F₂, feq, _root_.refl]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.HasGroupoid (hypothesis)
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
G : StructureGroupoid H
e : OpenPartialHomeomorph M H
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e
hs : Nonempty.{u_2 + 1} (↑e.source : Type u_2)
inst_3 : HasGroupoid M G
inst_4 : ClosedUnderRestriction G
s : Opens M := { carrier := e.source, is_open' := ⋯ }
t : Opens H := { carrier := e.target, is_open' := ⋯ }
c' : OpenPartialHomeomorph (↥t) H
hc' : Membership.mem (γ := Set (OpenPartialHomeomorph (↥t) H)) (atlas H ↥t) c'
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph.{u_2, u} (↥s) H)) (maximalAtlas (↥s) G)
    (e.toHomeomorphSourceTarget.toOpenPartialHomeomorph ≫ₕ c')
have this : Nonempty.{u + 1} ↥t
Tactic: have : Nonempty t := nonempty_coe_sort.mpr (e.mapsTo.nonempty (nonempty_coe_sort.mp hs))
-- Lean 4 proof step from Mathlib.Geometry.Manifold.HasGroupoid (goal)
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
G : StructureGroupoid H
e : OpenPartialHomeomorph M H
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e
hs : Nonempty.{u_2 + 1} (↑e.source : Type u_2)
inst_3 : HasGroupoid M G
inst_4 : ClosedUnderRestriction G
s : Opens M := { carrier := e.source, is_open' := ⋯ }
t : Opens H := { carrier := e.target, is_open' := ⋯ }
c' : OpenPartialHomeomorph (↥t) H
hc' : Membership.mem (γ := Set (OpenPartialHomeomorph (↥t) H)) (atlas H ↥t) c'
this : Nonempty.{u + 1} ↥t
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph.{u_2, u} (↥s) H)) (maximalAtlas (↥s) G)
    (e.toHomeomorphSourceTarget.toOpenPartialHomeomorph ≫ₕ c')
have obtain : ∀ (x : ↥t) (hc' : c' = subtypeRestr (chartAt H (↑x : H)) this),
  Membership.mem (γ := Set (OpenPartialHomeomorph.{u_2, u} (↥s) H)) (maximalAtlas (↥s) G)
    (e.toHomeomorphSourceTarget.toOpenPartialHomeomorph ≫ₕ c')
Tactic: obtain ⟨x, hc'⟩ := Opens.chart_eq this hc'
-- Lean 4 proof step from Mathlib.Geometry.Manifold.HasGroupoid (goal)
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
G : StructureGroupoid H
e : OpenPartialHomeomorph M H
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e
hs : Nonempty.{u_2 + 1} (↑e.source : Type u_2)
inst_3 : HasGroupoid M G
inst_4 : ClosedUnderRestriction G
s : Opens M := { carrier := e.source, is_open' := ⋯ }
t : Opens H := { carrier := e.target, is_open' := ⋯ }
c' : OpenPartialHomeomorph (↥t) H
hc'_1 : Membership.mem (γ := Set (OpenPartialHomeomorph (↥t) H)) (atlas H ↥t) c'
this : Nonempty.{u + 1} ↥t
x : ↥t
hc' : c' = subtypeRestr (chartAt H (↑x : H)) this
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph.{u_2, u} (↥s) H)) (maximalAtlas (↥s) G)
    (e.toHomeomorphSourceTarget.toOpenPartialHomeomorph ≫ₕ c')
have rw : Membership.mem (γ := Set (OpenPartialHomeomorph.{u_2, u} (↥s) H)) (maximalAtlas (↥s) G)
  (e.toHomeomorphSourceTarget.toOpenPartialHomeomorph ≫ₕ subtypeRestr (OpenPartialHomeomorph.refl H) this)
Tactic: rw [hc', (chartAt_self_eq)]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.HasGroupoid (goal)
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
G : StructureGroupoid H
e : OpenPartialHomeomorph M H
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e
hs : Nonempty.{u_2 + 1} (↑e.source : Type u_2)
inst_3 : HasGroupoid M G
inst_4 : ClosedUnderRestriction G
s : Opens M := { carrier := e.source, is_open' := ⋯ }
t : Opens H := { carrier := e.target, is_open' := ⋯ }
c' : OpenPartialHomeomorph (↥t) H
hc'_1 : Membership.mem (γ := Set (OpenPartialHomeomorph (↥t) H)) (atlas H ↥t) c'
this : Nonempty.{u + 1} ↥t
x : ↥t
hc' : c' = subtypeRestr (chartAt H (↑x : H)) this
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph.{u_2, u} (↥s) H)) (maximalAtlas (↥s) G)
    (e.toHomeomorphSourceTarget.toOpenPartialHomeomorph ≫ₕ subtypeRestr (OpenPartialHomeomorph.refl H) this)
have rw : Membership.mem (γ := Set (OpenPartialHomeomorph.{u_2, u} (↥s) H)) (maximalAtlas (↥s) G)
  (e.toHomeomorphSourceTarget.toOpenPartialHomeomorph ≫ₕ t.openPartialHomeomorphSubtypeCoe this)
Tactic: rw [OpenPartialHomeomorph.subtypeRestr_def, OpenPartialHomeomorph.trans_refl]