awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.StructureGroupoid (goal)
Goal:
H_1 : Type u_1
inst : TopologicalSpace H_1
H : Type u_2
inst_1 : TopologicalSpace H
e e' : OpenPartialHomeomorph H H
he'e : e' ≈ e
he : Membership.mem (γ := Set (OpenPartialHomeomorph H H)) {OpenPartialHomeomorph.refl H} e
refine_1 : e.source = univ
⊢ e = e'
have refine_2 : e.target = univ
Tactic: refine eq_of_eqOnSource_univ (Setoid.symm he'e) ?_ ?_
-- Lean 4 proof step from Mathlib.Geometry.Manifold.StructureGroupoid (goal)
Goal:
H_1 : Type u_1
inst : TopologicalSpace H_1
H : Type u_2
inst_1 : TopologicalSpace H
e e' : OpenPartialHomeomorph H H
he'e : e' ≈ e
he : Membership.mem (γ := Set (OpenPartialHomeomorph H H)) {OpenPartialHomeomorph.refl H} e
⊢ e.source = univ
have refine_1 : (toPartialEquiv (OpenPartialHomeomorph.refl H)).source = univ
Tactic: rw [Set.mem_singleton_iff.1 he]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.StructureGroupoid (goal)
Goal:
H_1 : Type u_1
inst : TopologicalSpace H_1
H : Type u_2
inst_1 : TopologicalSpace H
e e' : OpenPartialHomeomorph H H
he'e : e' ≈ e
he : Membership.mem (γ := Set (OpenPartialHomeomorph H H)) {OpenPartialHomeomorph.refl H} e
⊢ e.target = univ
have refine_2 : (toPartialEquiv (OpenPartialHomeomorph.refl H)).target = univ
Tactic: rw [Set.mem_singleton_iff.1 he]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.StructureGroupoid (hypothesis)
Goal:
H_1 : Type u_1
inst : TopologicalSpace H_1
H : Type u_2
inst_1 : TopologicalSpace H
e e' : OpenPartialHomeomorph H H
he'e : e' ≈ e
he : Membership.mem (γ := Set (OpenPartialHomeomorph H H)) {OpenPartialHomeomorph.refl H} e
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph H H)) {OpenPartialHomeomorph.refl H} e'
have this : e = e'
Tactic: have : e = e' := by
        refine eq_of_eqOnSource_univ (Setoid.symm he'e) ?_ ?_ <;>
          rw [Set.mem_singleton_iff.1 he] <;> rfl
-- Lean 4 proof step from Mathlib.Geometry.Manifold.StructureGroupoid (goal)
Goal:
H_1 : Type u_1
inst : TopologicalSpace H_1
H : Type u_2
inst_1 : TopologicalSpace H
e e' : OpenPartialHomeomorph H H
he'e : e' ≈ e
he : Membership.mem (γ := Set (OpenPartialHomeomorph H H)) {e : OpenPartialHomeomorph H H | e.source = ∅} e
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph H H))
    ({OpenPartialHomeomorph.refl H} ∪ {e : OpenPartialHomeomorph H H | e.source = ∅}) e'
have inr : Membership.mem (γ := Set (OpenPartialHomeomorph H H)) {e : OpenPartialHomeomorph H H | e.source = ∅} e'
Tactic: right
-- Lean 4 proof step from Mathlib.Geometry.Manifold.StructureGroupoid (hypothesis)
Goal:
H_1 : Type u_1
inst : TopologicalSpace H_1
H : Type u_2
inst_1 : TopologicalSpace H
e e' : OpenPartialHomeomorph H H
he'e : e' ≈ e
he : Membership.mem (γ := Set (OpenPartialHomeomorph H H)) {e : OpenPartialHomeomorph H H | e.source = ∅} e
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph H H)) {e : OpenPartialHomeomorph H H | e.source = ∅} e'
have he₁ : e.source = ∅
Tactic: have he : e.toPartialEquiv.source = ∅ := he
-- Lean 4 proof step from Mathlib.Geometry.Manifold.StructureGroupoid (goal)
Goal:
H_1 : Type u_1
inst : TopologicalSpace H_1
H : Type u_2
inst_1 : TopologicalSpace H
e e' : OpenPartialHomeomorph H H
he'e : e' ≈ e
he_1 : Membership.mem (γ := Set (OpenPartialHomeomorph H H)) {e : OpenPartialHomeomorph H H | e.source = ∅} e
he : e.source = ∅
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph H H)) {e : OpenPartialHomeomorph H H | e.source = ∅} e'
have inr : e'.source = ∅
Tactic: rwa [Set.mem_setOf_eq, EqOnSource.source_eq he'e]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.StructureGroupoid (hypothesis)
Goal:
H : Type u_1
inst : TopologicalSpace H
u : StructureGroupoid H
f : OpenPartialHomeomorph H H
hf_1 : Membership.mem (γ := Set (OpenPartialHomeomorph H H)) (StructureGroupoid.members (idGroupoid H)) f
hf :
  Membership.mem (γ := Set (OpenPartialHomeomorph H H))
    ({OpenPartialHomeomorph.refl H} ∪ {e : OpenPartialHomeomorph H H | e.source = ∅}) f
⊢ f ∈ u.members
have hf₁ : f = OpenPartialHomeomorph.refl H ∨ f.source = ∅
Tactic: simp only [singleton_union, mem_setOf_eq, mem_insert_iff] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Geometry.Manifold.StructureGroupoid (goal)
Goal:
H : Type u_1
inst : TopologicalSpace H
u : StructureGroupoid H
f : OpenPartialHomeomorph H H
hf_1 : Membership.mem (γ := Set (OpenPartialHomeomorph H H)) (StructureGroupoid.members (idGroupoid H)) f
hf : f = OpenPartialHomeomorph.refl H ∨ f.source = ∅
⊢ f ∈ u.members
have inl : ∀ (hf : f = OpenPartialHomeomorph.refl H), f ∈ u.members
Tactic: rcases hf with hf | hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Geometry.Manifold.StructureGroupoid (goal)
Goal:
H : Type u_1
inst : TopologicalSpace H
u : StructureGroupoid H
f : OpenPartialHomeomorph H H
hf_1 : Membership.mem (γ := Set (OpenPartialHomeomorph H H)) (StructureGroupoid.members (idGroupoid H)) f
hf : f = OpenPartialHomeomorph.refl H ∨ f.source = ∅
inl : ∀ (hf : f = OpenPartialHomeomorph.refl H), f ∈ u.members
⊢ f ∈ u.members
have inr : ∀ (hf : f.source = ∅), f ∈ u.members
Tactic: rcases hf with hf | hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Geometry.Manifold.StructureGroupoid (goal)
Goal:
H : Type u_1
inst : TopologicalSpace H
u : StructureGroupoid H
f : OpenPartialHomeomorph H H
hf_1 : Membership.mem (γ := Set (OpenPartialHomeomorph H H)) (StructureGroupoid.members (idGroupoid H)) f
hf : f = OpenPartialHomeomorph.refl H
⊢ f ∈ u.members
have inl : OpenPartialHomeomorph.refl H ∈ u.members
Tactic: rw [hf]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.StructureGroupoid (goal)
Goal:
H : Type u_1
inst : TopologicalSpace H
u : StructureGroupoid H
f : OpenPartialHomeomorph H H
hf_1 : Membership.mem (γ := Set (OpenPartialHomeomorph H H)) (StructureGroupoid.members (idGroupoid H)) f
hf : f.source = ∅
⊢ f ∈ u.members
have inr : ∀ x ∈ f.source, ∃ (s : Set H), IsOpen[inst] s ∧ x ∈ s ∧ f.restr s ∈ u
Tactic: apply u.locality
-- Lean 4 proof step from Mathlib.Geometry.Manifold.StructureGroupoid (hypothesis)
Goal:
H : Type u_1
inst : TopologicalSpace H
u : StructureGroupoid H
f : OpenPartialHomeomorph H H
hf_1 : Membership.mem (γ := Set (OpenPartialHomeomorph H H)) (StructureGroupoid.members (idGroupoid H)) f
hf : f.source = ∅
x : H
hx : x ∈ f.source
⊢ ∃ (s : Set H), IsOpen[inst] s ∧ x ∈ s ∧ f.restr s ∈ u
have hx₁ : False
Tactic: rw [hf, mem_empty_iff_false] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Geometry.Manifold.StructureGroupoid (goal)
Goal:
H : Type u_1
inst : TopologicalSpace H
PG : Pregroupoid H
e e' : OpenPartialHomeomorph H H
he :
  Membership.mem (γ := Set (OpenPartialHomeomorph H H))
    {e : OpenPartialHomeomorph H H | PG.property (↑e : H → H) e.source ∧ PG.property (↑e.symm : H → H) e.target} e
he' :
  Membership.mem (γ := Set (OpenPartialHomeomorph H H))
    {e : OpenPartialHomeomorph H H | PG.property (↑e : H → H) e.source ∧ PG.property (↑e.symm : H → H) e.target} e'
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph H H))
    {e : OpenPartialHomeomorph H H | PG.property (↑e : H → H) e.source ∧ PG.property (↑e.symm : H → H) e.target}
    (e ≫ₕ e')
have left : PG.property (↑(e ≫ₕ e') : H → H) (e ≫ₕ e').source
Tactic: constructor
-- Lean 4 proof step from Mathlib.Geometry.Manifold.StructureGroupoid (goal)
Goal:
H : Type u_1
inst : TopologicalSpace H
PG : Pregroupoid H
e e' : OpenPartialHomeomorph H H
he :
  Membership.mem (γ := Set (OpenPartialHomeomorph H H))
    {e : OpenPartialHomeomorph H H | PG.property (↑e : H → H) e.source ∧ PG.property (↑e.symm : H → H) e.target} e
he' :
  Membership.mem (γ := Set (OpenPartialHomeomorph H H))
    {e : OpenPartialHomeomorph H H | PG.property (↑e : H → H) e.source ∧ PG.property (↑e.symm : H → H) e.target} e'
left : PG.property (↑(e ≫ₕ e') : H → H) (e ≫ₕ e').source
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph H H))
    {e : OpenPartialHomeomorph H H | PG.property (↑e : H → H) e.source ∧ PG.property (↑e.symm : H → H) e.target}
    (e ≫ₕ e')
have right : PG.property (↑(e ≫ₕ e').symm : H → H) (e ≫ₕ e').target
Tactic: constructor
-- Lean 4 proof step from Mathlib.Geometry.Manifold.StructureGroupoid (goal)
Goal:
H : Type u_1
inst : TopologicalSpace H
PG : Pregroupoid H
e e' : OpenPartialHomeomorph H H
he :
  Membership.mem (γ := Set (OpenPartialHomeomorph H H))
    {e : OpenPartialHomeomorph H H | PG.property (↑e : H → H) e.source ∧ PG.property (↑e.symm : H → H) e.target} e
he' :
  Membership.mem (γ := Set (OpenPartialHomeomorph H H))
    {e : OpenPartialHomeomorph H H | PG.property (↑e : H → H) e.source ∧ PG.property (↑e.symm : H → H) e.target} e'
⊢ PG.property (↑(e ≫ₕ e') : H → H) (e ≫ₕ e').source
have left : IsOpen[inst] (e.source ∩ (↑e : H → H) ⁻¹' e'.source)
Tactic: apply PG.comp he.1 he'.1 e.open_source e'.open_source
-- Lean 4 proof step from Mathlib.Geometry.Manifold.StructureGroupoid (goal)
Goal:
H : Type u_1
inst : TopologicalSpace H
PG : Pregroupoid H
e e' : OpenPartialHomeomorph H H
he :
  Membership.mem (γ := Set (OpenPartialHomeomorph H H))
    {e : OpenPartialHomeomorph H H | PG.property (↑e : H → H) e.source ∧ PG.property (↑e.symm : H → H) e.target} e
he' :
  Membership.mem (γ := Set (OpenPartialHomeomorph H H))
    {e : OpenPartialHomeomorph H H | PG.property (↑e : H → H) e.source ∧ PG.property (↑e.symm : H → H) e.target} e'
⊢ PG.property (↑(e ≫ₕ e').symm : H → H) (e ≫ₕ e').target
have right : IsOpen[inst] (e'.target ∩ (↑e'.symm : H → H) ⁻¹' e.target)
Tactic: apply PG.comp he'.2 he.2 e'.open_target e.open_target
-- Lean 4 proof step from Mathlib.Geometry.Manifold.StructureGroupoid (goal)
Goal:
H : Type u_1
inst : TopologicalSpace H
PG : Pregroupoid H
e : OpenPartialHomeomorph H H
he :
  ∀ x ∈ e.source,
    ∃ (s : Set H),
      IsOpen[inst] s ∧
        x ∈ s ∧
          Membership.mem (γ := Set (OpenPartialHomeomorph H H))
            {e : OpenPartialHomeomorph H H | PG.property (↑e : H → H) e.source ∧ PG.property (↑e.symm : H → H) e.target}
            (e.restr s)
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph H H))
    {e : OpenPartialHomeomorph H H | PG.property (↑e : H → H) e.source ∧ PG.property (↑e.symm : H → H) e.target} e
have left : PG.property (↑e : H → H) e.source
Tactic: constructor
-- Lean 4 proof step from Mathlib.Geometry.Manifold.StructureGroupoid (goal)
Goal:
H : Type u_1
inst : TopologicalSpace H
PG : Pregroupoid H
e : OpenPartialHomeomorph H H
he :
  ∀ x ∈ e.source,
    ∃ (s : Set H),
      IsOpen[inst] s ∧
        x ∈ s ∧
          Membership.mem (γ := Set (OpenPartialHomeomorph H H))
            {e : OpenPartialHomeomorph H H | PG.property (↑e : H → H) e.source ∧ PG.property (↑e.symm : H → H) e.target}
            (e.restr s)
left : PG.property (↑e : H → H) e.source
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph H H))
    {e : OpenPartialHomeomorph H H | PG.property (↑e : H → H) e.source ∧ PG.property (↑e.symm : H → H) e.target} e
have right : PG.property (↑e.symm : H → H) e.target
Tactic: constructor
-- Lean 4 proof step from Mathlib.Geometry.Manifold.StructureGroupoid (goal)
Goal:
H : Type u_1
inst : TopologicalSpace H
PG : Pregroupoid H
e : OpenPartialHomeomorph H H
he :
  ∀ x ∈ e.source,
    ∃ (s : Set H),
      IsOpen[inst] s ∧
        x ∈ s ∧
          Membership.mem (γ := Set (OpenPartialHomeomorph H H))
            {e : OpenPartialHomeomorph H H | PG.property (↑e : H → H) e.source ∧ PG.property (↑e.symm : H → H) e.target}
            (e.restr s)
⊢ PG.property (↑e : H → H) e.source
have left : ∀ (x : H) (xu : x ∈ e.source), ∃ (v : Set H), IsOpen[inst] v ∧ x ∈ v ∧ PG.property (↑e : H → H) (e.source ∩ v)
Tactic: refine PG.locality e.open_source fun x xu ↦ ?_
-- Lean 4 proof step from Mathlib.Geometry.Manifold.StructureGroupoid (goal)
Goal:
H : Type u_1
inst : TopologicalSpace H
PG : Pregroupoid H
e : OpenPartialHomeomorph H H
he :
  ∀ x ∈ e.source,
    ∃ (s : Set H),
      IsOpen[inst] s ∧
        x ∈ s ∧
          Membership.mem (γ := Set (OpenPartialHomeomorph H H))
            {e : OpenPartialHomeomorph H H | PG.property (↑e : H → H) e.source ∧ PG.property (↑e.symm : H → H) e.target}
            (e.restr s)
x : H
xu : x ∈ e.source
⊢ ∃ (v : Set H), IsOpen[inst] v ∧ x ∈ v ∧ PG.property (↑e : H → H) (e.source ∩ v)
have left : ∀ (s : Set H) (s_open : IsOpen[inst] s) (xs : x ∈ s)
  (hs :
    Membership.mem (γ := Set (OpenPartialHomeomorph H H))
      {e : OpenPartialHomeomorph H H | PG.property (↑e : H → H) e.source ∧ PG.property (↑e.symm : H → H) e.target}
      (e.restr s)),
  ∃ (v : Set H), IsOpen[inst] v ∧ x ∈ v ∧ PG.property (↑e : H → H) (e.source ∩ v)
Tactic: rcases he x xu with ⟨s, s_open, xs, hs⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.StructureGroupoid (goal)
Goal:
H : Type u_1
inst : TopologicalSpace H
PG : Pregroupoid H
e : OpenPartialHomeomorph H H
he :
  ∀ x ∈ e.source,
    ∃ (s : Set H),
      IsOpen[inst] s ∧
        x ∈ s ∧
          Membership.mem (γ := Set (OpenPartialHomeomorph H H))
            {e : OpenPartialHomeomorph H H | PG.property (↑e : H → H) e.source ∧ PG.property (↑e.symm : H → H) e.target}
            (e.restr s)
x : H
xu : x ∈ e.source
s : Set H
s_open : IsOpen[inst] s
xs : x ∈ s
hs :
  Membership.mem (γ := Set (OpenPartialHomeomorph H H))
    {e : OpenPartialHomeomorph H H | PG.property (↑e : H → H) e.source ∧ PG.property (↑e.symm : H → H) e.target}
    (e.restr s)
⊢ ∃ (v : Set H), IsOpen[inst] v ∧ x ∈ v ∧ PG.property (↑e : H → H) (e.source ∩ v)
have left : PG.property (↑e : H → H) (e.source ∩ s)
Tactic: refine ⟨s, s_open, xs, ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.StructureGroupoid (goal)
Goal:
H : Type u_1
inst : TopologicalSpace H
PG : Pregroupoid H
e : OpenPartialHomeomorph H H
he :
  ∀ x ∈ e.source,
    ∃ (s : Set H),
      IsOpen[inst] s ∧
        x ∈ s ∧
          Membership.mem (γ := Set (OpenPartialHomeomorph H H))
            {e : OpenPartialHomeomorph H H | PG.property (↑e : H → H) e.source ∧ PG.property (↑e.symm : H → H) e.target}
            (e.restr s)
x : H
xu : x ∈ e.source
s : Set H
s_open : IsOpen[inst] s
xs : x ∈ s
hs :
  Membership.mem (γ := Set (OpenPartialHomeomorph H H))
    {e : OpenPartialHomeomorph H H | PG.property (↑e : H → H) e.source ∧ PG.property (↑e.symm : H → H) e.target}
    (e.restr s)
⊢ PG.property (↑e : H → H) (e.source ∩ s)
have h : e.source ∩ s = (e.restr s).source
Tactic: convert! hs.1 using 1
-- Lean 4 proof step from Mathlib.Geometry.Manifold.StructureGroupoid (goal)
Goal:
H : Type u_1
inst : TopologicalSpace H
PG : Pregroupoid H
e : OpenPartialHomeomorph H H
he :
  ∀ x ∈ e.source,
    ∃ (s : Set H),
      IsOpen[inst] s ∧
        x ∈ s ∧
          Membership.mem (γ := Set (OpenPartialHomeomorph H H))
            {e : OpenPartialHomeomorph H H | PG.property (↑e : H → H) e.source ∧ PG.property (↑e.symm : H → H) e.target}
            (e.restr s)
x : H
xu : x ∈ e.source
s : Set H
s_open : IsOpen[inst] s
xs : x ∈ s
hs :
  Membership.mem (γ := Set (OpenPartialHomeomorph H H))
    {e : OpenPartialHomeomorph H H | PG.property (↑e : H → H) e.source ∧ PG.property (↑e.symm : H → H) e.target}
    (e.restr s)
⊢ e.source ∩ s = e.source ∩ interior s
have h : e.source ∩ s = e.source ∩ s
Tactic: rw [s_open.interior_eq]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.StructureGroupoid (goal)
Goal:
H : Type u_1
inst : TopologicalSpace H
PG : Pregroupoid H
e : OpenPartialHomeomorph H H
he :
  ∀ x ∈ e.source,
    ∃ (s : Set H),
      IsOpen[inst] s ∧
        x ∈ s ∧
          Membership.mem (γ := Set (OpenPartialHomeomorph H H))
            {e : OpenPartialHomeomorph H H | PG.property (↑e : H → H) e.source ∧ PG.property (↑e.symm : H → H) e.target}
            (e.restr s)
⊢ PG.property (↑e.symm : H → H) e.target
have right : ∀ (x : H) (xu : x ∈ e.target), ∃ (v : Set H), IsOpen[inst] v ∧ x ∈ v ∧ PG.property (↑e.symm : H → H) (e.target ∩ v)
Tactic: refine PG.locality e.open_target fun x xu ↦ ?_
-- Lean 4 proof step from Mathlib.Geometry.Manifold.StructureGroupoid (goal)
Goal:
H : Type u_1
inst : TopologicalSpace H
PG : Pregroupoid H
e : OpenPartialHomeomorph H H
he :
  ∀ x ∈ e.source,
    ∃ (s : Set H),
      IsOpen[inst] s ∧
        x ∈ s ∧
          Membership.mem (γ := Set (OpenPartialHomeomorph H H))
            {e : OpenPartialHomeomorph H H | PG.property (↑e : H → H) e.source ∧ PG.property (↑e.symm : H → H) e.target}
            (e.restr s)
x : H
xu : x ∈ e.target
⊢ ∃ (v : Set H), IsOpen[inst] v ∧ x ∈ v ∧ PG.property (↑e.symm : H → H) (e.target ∩ v)
have right : ∀ (s : Set H) (s_open : IsOpen[inst] s) (xs : (↑e.symm : H → H) x ∈ s)
  (hs :
    Membership.mem (γ := Set (OpenPartialHomeomorph H H))
      {e : OpenPartialHomeomorph H H | PG.property (↑e : H → H) e.source ∧ PG.property (↑e.symm : H → H) e.target}
      (e.restr s)),
  ∃ (v : Set H), IsOpen[inst] v ∧ x ∈ v ∧ PG.property (↑e.symm : H → H) (e.target ∩ v)
Tactic: rcases he (e.symm x) (e.map_target xu) with ⟨s, s_open, xs, hs⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.StructureGroupoid (goal)
Goal:
H : Type u_1
inst : TopologicalSpace H
PG : Pregroupoid H
e : OpenPartialHomeomorph H H
he :
  ∀ x ∈ e.source,
    ∃ (s : Set H),
      IsOpen[inst] s ∧
        x ∈ s ∧
          Membership.mem (γ := Set (OpenPartialHomeomorph H H))
            {e : OpenPartialHomeomorph H H | PG.property (↑e : H → H) e.source ∧ PG.property (↑e.symm : H → H) e.target}
            (e.restr s)
x : H
xu : x ∈ e.target
s : Set H
s_open : IsOpen[inst] s
xs : (↑e.symm : H → H) x ∈ s
hs :
  Membership.mem (γ := Set (OpenPartialHomeomorph H H))
    {e : OpenPartialHomeomorph H H | PG.property (↑e : H → H) e.source ∧ PG.property (↑e.symm : H → H) e.target}
    (e.restr s)
⊢ ∃ (v : Set H), IsOpen[inst] v ∧ x ∈ v ∧ PG.property (↑e.symm : H → H) (e.target ∩ v)
have right : IsOpen[inst] (e.target ∩ (↑e.symm : H → H) ⁻¹' s)
Tactic: refine ⟨e.target ∩ e.symm ⁻¹' s, ?_, ⟨xu, xs⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.StructureGroupoid (goal)
Goal:
H : Type u_1
inst : TopologicalSpace H
PG : Pregroupoid H
e : OpenPartialHomeomorph H H
he :
  ∀ x ∈ e.source,
    ∃ (s : Set H),
      IsOpen[inst] s ∧
        x ∈ s ∧
          Membership.mem (γ := Set (OpenPartialHomeomorph H H))
            {e : OpenPartialHomeomorph H H | PG.property (↑e : H → H) e.source ∧ PG.property (↑e.symm : H → H) e.target}
            (e.restr s)
x : H
xu : x ∈ e.target
s : Set H
s_open : IsOpen[inst] s
xs : (↑e.symm : H → H) x ∈ s
hs :
  Membership.mem (γ := Set (OpenPartialHomeomorph H H))
    {e : OpenPartialHomeomorph H H | PG.property (↑e : H → H) e.source ∧ PG.property (↑e.symm : H → H) e.target}
    (e.restr s)
right : IsOpen[inst] (e.target ∩ (↑e.symm : H → H) ⁻¹' s)
⊢ ∃ (v : Set H), IsOpen[inst] v ∧ x ∈ v ∧ PG.property (↑e.symm : H → H) (e.target ∩ v)
have right₁ : PG.property (↑e.symm : H → H) (e.target ∩ (e.target ∩ (↑e.symm : H → H) ⁻¹' s))
Tactic: refine ⟨e.target ∩ e.symm ⁻¹' s, ?_, ⟨xu, xs⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.StructureGroupoid (goal)
Goal:
H : Type u_1
inst : TopologicalSpace H
PG : Pregroupoid H
e : OpenPartialHomeomorph H H
he :
  ∀ x ∈ e.source,
    ∃ (s : Set H),
      IsOpen[inst] s ∧
        x ∈ s ∧
          Membership.mem (γ := Set (OpenPartialHomeomorph H H))
            {e : OpenPartialHomeomorph H H | PG.property (↑e : H → H) e.source ∧ PG.property (↑e.symm : H → H) e.target}
            (e.restr s)
x : H
xu : x ∈ e.target
s : Set H
s_open : IsOpen[inst] s
xs : (↑e.symm : H → H) x ∈ s
hs :
  Membership.mem (γ := Set (OpenPartialHomeomorph H H))
    {e : OpenPartialHomeomorph H H | PG.property (↑e : H → H) e.source ∧ PG.property (↑e.symm : H → H) e.target}
    (e.restr s)
⊢ PG.property (↑e.symm : H → H) (e.target ∩ (e.target ∩ (↑e.symm : H → H) ⁻¹' s))
have right : PG.property (↑e.symm : H → H) (e.target ∩ (↑e.symm : H → H) ⁻¹' s)
Tactic: rw [← inter_assoc, inter_self]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.StructureGroupoid (goal)
Goal:
H : Type u_1
inst : TopologicalSpace H
PG : Pregroupoid H
e : OpenPartialHomeomorph H H
he :
  ∀ x ∈ e.source,
    ∃ (s : Set H),
      IsOpen[inst] s ∧
        x ∈ s ∧
          Membership.mem (γ := Set (OpenPartialHomeomorph H H))
            {e : OpenPartialHomeomorph H H | PG.property (↑e : H → H) e.source ∧ PG.property (↑e.symm : H → H) e.target}
            (e.restr s)
x : H
xu : x ∈ e.target
s : Set H
s_open : IsOpen[inst] s
xs : (↑e.symm : H → H) x ∈ s
hs :
  Membership.mem (γ := Set (OpenPartialHomeomorph H H))
    {e : OpenPartialHomeomorph H H | PG.property (↑e : H → H) e.source ∧ PG.property (↑e.symm : H → H) e.target}
    (e.restr s)
⊢ PG.property (↑e.symm : H → H) (e.target ∩ (↑e.symm : H → H) ⁻¹' s)
have h : e.target ∩ (↑e.symm : H → H) ⁻¹' s = (e.restr s).target
Tactic: convert! hs.2 using 1
-- Lean 4 proof step from Mathlib.Geometry.Manifold.StructureGroupoid (goal)
Goal:
H : Type u_1
inst : TopologicalSpace H
PG : Pregroupoid H
e : OpenPartialHomeomorph H H
he :
  ∀ x ∈ e.source,
    ∃ (s : Set H),
      IsOpen[inst] s ∧
        x ∈ s ∧
          Membership.mem (γ := Set (OpenPartialHomeomorph H H))
            {e : OpenPartialHomeomorph H H | PG.property (↑e : H → H) e.source ∧ PG.property (↑e.symm : H → H) e.target}
            (e.restr s)
x : H
xu : x ∈ e.target
s : Set H
s_open : IsOpen[inst] s
xs : (↑e.symm : H → H) x ∈ s
hs :
  Membership.mem (γ := Set (OpenPartialHomeomorph H H))
    {e : OpenPartialHomeomorph H H | PG.property (↑e : H → H) e.source ∧ PG.property (↑e.symm : H → H) e.target}
    (e.restr s)
⊢ e.target ∩ (↑e.symm : H → H) ⁻¹' s = e.target ∩ (↑e.symm : H → H) ⁻¹' interior s
have h : e.target ∩ (↑e.symm : H → H) ⁻¹' s = e.target ∩ (↑e.symm : H → H) ⁻¹' s
Tactic: rw [s_open.interior_eq]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.StructureGroupoid (goal)
Goal:
H : Type u_1
inst : TopologicalSpace H
PG : Pregroupoid H
e e' : OpenPartialHomeomorph H H
he :
  Membership.mem (γ := Set (OpenPartialHomeomorph H H))
    {e : OpenPartialHomeomorph H H | PG.property (↑e : H → H) e.source ∧ PG.property (↑e.symm : H → H) e.target} e
ee' : e' ≈ e
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph H H))
    {e : OpenPartialHomeomorph H H | PG.property (↑e : H → H) e.source ∧ PG.property (↑e.symm : H → H) e.target} e'
have left : PG.property (↑e' : H → H) e'.source
Tactic: constructor
-- Lean 4 proof step from Mathlib.Geometry.Manifold.StructureGroupoid (goal)
Goal:
H : Type u_1
inst : TopologicalSpace H
PG : Pregroupoid H
e e' : OpenPartialHomeomorph H H
he :
  Membership.mem (γ := Set (OpenPartialHomeomorph H H))
    {e : OpenPartialHomeomorph H H | PG.property (↑e : H → H) e.source ∧ PG.property (↑e.symm : H → H) e.target} e
ee' : e' ≈ e
left : PG.property (↑e' : H → H) e'.source
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph H H))
    {e : OpenPartialHomeomorph H H | PG.property (↑e : H → H) e.source ∧ PG.property (↑e.symm : H → H) e.target} e'
have right : PG.property (↑e'.symm : H → H) e'.target
Tactic: constructor
-- Lean 4 proof step from Mathlib.Geometry.Manifold.StructureGroupoid (goal)
Goal:
H : Type u_1
inst : TopologicalSpace H
PG : Pregroupoid H
e e' : OpenPartialHomeomorph H H
he :
  Membership.mem (γ := Set (OpenPartialHomeomorph H H))
    {e : OpenPartialHomeomorph H H | PG.property (↑e : H → H) e.source ∧ PG.property (↑e.symm : H → H) e.target} e
ee' : e' ≈ e
⊢ PG.property (↑e' : H → H) e'.source
have left : PG.property (↑e : H → H) e'.source
Tactic: apply PG.congr e'.open_source ee'.2
-- Lean 4 proof step from Mathlib.Geometry.Manifold.StructureGroupoid (hypothesis)
Goal:
H : Type u_1
inst : TopologicalSpace H
PG : Pregroupoid H
e e' : OpenPartialHomeomorph H H
he :
  Membership.mem (γ := Set (OpenPartialHomeomorph H H))
    {e : OpenPartialHomeomorph H H | PG.property (↑e : H → H) e.source ∧ PG.property (↑e.symm : H → H) e.target} e
ee' : e' ≈ e
⊢ PG.property (↑e'.symm : H → H) e'.target
have A : e'.symm ≈ e.symm
Tactic: have A := EqOnSource.symm' ee'
-- Lean 4 proof step from Mathlib.Geometry.Manifold.StructureGroupoid (goal)
Goal:
H : Type u_1
inst : TopologicalSpace H
PG : Pregroupoid H
e e' : OpenPartialHomeomorph H H
he :
  Membership.mem (γ := Set (OpenPartialHomeomorph H H))
    {e : OpenPartialHomeomorph H H | PG.property (↑e : H → H) e.source ∧ PG.property (↑e.symm : H → H) e.target} e
ee' : e' ≈ e
A : e'.symm ≈ e.symm
⊢ PG.property (↑e'.symm : H → H) e'.target
have right : PG.property (↑e.symm : H → H) e'.symm.source
Tactic: apply PG.congr e'.symm.open_source A.2