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 : OpenPartialHomeomorph H H
he :
  Membership.mem (γ := Set (OpenPartialHomeomorph H H))
    ({OpenPartialHomeomorph.refl H} ∪ {e : OpenPartialHomeomorph H H | e.source = ∅}) e
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph H H))
    ({OpenPartialHomeomorph.refl H} ∪ {e : OpenPartialHomeomorph H H | e.source = ∅}) e.symm
have inl : ∀ (E : Membership.mem (γ := Set (OpenPartialHomeomorph H H)) {OpenPartialHomeomorph.refl H} e),
  Membership.mem (γ := Set (OpenPartialHomeomorph H H))
    ({OpenPartialHomeomorph.refl H} ∪ {e : OpenPartialHomeomorph H H | e.source = ∅}) e.symm
Tactic: rcases (mem_union _ _ _).1 he with E | 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 : OpenPartialHomeomorph H H
he :
  Membership.mem (γ := Set (OpenPartialHomeomorph H H))
    ({OpenPartialHomeomorph.refl H} ∪ {e : OpenPartialHomeomorph H H | e.source = ∅}) e
inl :
  ∀ (E : Membership.mem (γ := Set (OpenPartialHomeomorph H H)) {OpenPartialHomeomorph.refl H} e),
    Membership.mem (γ := Set (OpenPartialHomeomorph H H))
      ({OpenPartialHomeomorph.refl H} ∪ {e : OpenPartialHomeomorph H H | e.source = ∅}) e.symm
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph H H))
    ({OpenPartialHomeomorph.refl H} ∪ {e : OpenPartialHomeomorph H H | e.source = ∅}) e.symm
have inr : ∀ (E : 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.symm
Tactic: rcases (mem_union _ _ _).1 he with E | 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 : OpenPartialHomeomorph H H
he :
  Membership.mem (γ := Set (OpenPartialHomeomorph H H))
    ({OpenPartialHomeomorph.refl H} ∪ {e : OpenPartialHomeomorph H H | e.source = ∅}) e
E : 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.symm
have inr : Membership.mem (γ := Set (OpenPartialHomeomorph H H)) {e : OpenPartialHomeomorph H H | e.source = ∅} e.symm
Tactic: right
-- 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 : OpenPartialHomeomorph H H
he :
  ∀ x ∈ e.source,
    ∃ (s : Set H),
      IsOpen[inst_1] s ∧
        x ∈ s ∧
          Membership.mem (γ := Set (OpenPartialHomeomorph H H))
            ({OpenPartialHomeomorph.refl H} ∪ {e : OpenPartialHomeomorph H H | e.source = ∅}) (e.restr s)
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph H H))
    ({OpenPartialHomeomorph.refl H} ∪ {e : OpenPartialHomeomorph H H | e.source = ∅}) e
have inl : ∀ (h : e.source = ∅),
  Membership.mem (γ := Set (OpenPartialHomeomorph H H))
    ({OpenPartialHomeomorph.refl H} ∪ {e : OpenPartialHomeomorph H H | e.source = ∅}) e
Tactic: rcases e.source.eq_empty_or_nonempty with h | h
-- 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 : OpenPartialHomeomorph H H
he :
  ∀ x ∈ e.source,
    ∃ (s : Set H),
      IsOpen[inst_1] s ∧
        x ∈ s ∧
          Membership.mem (γ := Set (OpenPartialHomeomorph H H))
            ({OpenPartialHomeomorph.refl H} ∪ {e : OpenPartialHomeomorph H H | e.source = ∅}) (e.restr s)
inl :
  ∀ (h : e.source = ∅),
    Membership.mem (γ := Set (OpenPartialHomeomorph H H))
      ({OpenPartialHomeomorph.refl 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 : ∀ (h : e.source.Nonempty),
  Membership.mem (γ := Set (OpenPartialHomeomorph H H))
    ({OpenPartialHomeomorph.refl H} ∪ {e : OpenPartialHomeomorph H H | e.source = ∅}) e
Tactic: rcases e.source.eq_empty_or_nonempty with h | h
-- 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 : OpenPartialHomeomorph H H
he :
  ∀ x ∈ e.source,
    ∃ (s : Set H),
      IsOpen[inst_1] s ∧
        x ∈ s ∧
          Membership.mem (γ := Set (OpenPartialHomeomorph H H))
            ({OpenPartialHomeomorph.refl H} ∪ {e : OpenPartialHomeomorph H H | e.source = ∅}) (e.restr s)
h : e.source = ∅
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph H H))
    ({OpenPartialHomeomorph.refl H} ∪ {e : OpenPartialHomeomorph H H | e.source = ∅}) e
have inl : Membership.mem (γ := Set (OpenPartialHomeomorph H H)) {e : OpenPartialHomeomorph H H | e.source = ∅} e
Tactic: right
-- 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 : OpenPartialHomeomorph H H
he :
  ∀ x ∈ e.source,
    ∃ (s : Set H),
      IsOpen[inst_1] s ∧
        x ∈ s ∧
          Membership.mem (γ := Set (OpenPartialHomeomorph H H))
            ({OpenPartialHomeomorph.refl H} ∪ {e : OpenPartialHomeomorph H H | e.source = ∅}) (e.restr s)
h : e.source.Nonempty
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph H H))
    ({OpenPartialHomeomorph.refl H} ∪ {e : OpenPartialHomeomorph H H | e.source = ∅}) e
have inr : Membership.mem (γ := Set (OpenPartialHomeomorph H H)) {OpenPartialHomeomorph.refl H} e
Tactic: left
-- 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 : OpenPartialHomeomorph H H
he :
  ∀ x ∈ e.source,
    ∃ (s : Set H),
      IsOpen[inst_1] s ∧
        x ∈ s ∧
          Membership.mem (γ := Set (OpenPartialHomeomorph H H))
            ({OpenPartialHomeomorph.refl H} ∪ {e : OpenPartialHomeomorph H H | e.source = ∅}) (e.restr s)
h : e.source.Nonempty
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph H H)) {OpenPartialHomeomorph.refl H} e
have inr : ∀ (x : H) (hx : x ∈ e.source), Membership.mem (γ := Set (OpenPartialHomeomorph H H)) {OpenPartialHomeomorph.refl H} e
Tactic: rcases h with ⟨x, hx⟩
Cleared hypotheses: h
-- 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 : OpenPartialHomeomorph H H
he :
  ∀ x ∈ e.source,
    ∃ (s : Set H),
      IsOpen[inst_1] s ∧
        x ∈ s ∧
          Membership.mem (γ := Set (OpenPartialHomeomorph H H))
            ({OpenPartialHomeomorph.refl H} ∪ {e : OpenPartialHomeomorph H H | e.source = ∅}) (e.restr s)
x : H
hx : x ∈ e.source
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph H H)) {OpenPartialHomeomorph.refl H} e
have inr : ∀ (s : Set H) (open_s : IsOpen[inst_1] s) (xs : x ∈ s)
  (hs :
    Membership.mem (γ := Set (OpenPartialHomeomorph H H))
      ({OpenPartialHomeomorph.refl H} ∪ {e : OpenPartialHomeomorph H H | e.source = ∅}) (e.restr s)),
  Membership.mem (γ := Set (OpenPartialHomeomorph H H)) {OpenPartialHomeomorph.refl H} e
Tactic: rcases he x hx with ⟨s, open_s, xs, hs⟩
-- 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 : OpenPartialHomeomorph H H
he :
  ∀ x ∈ e.source,
    ∃ (s : Set H),
      IsOpen[inst_1] s ∧
        x ∈ s ∧
          Membership.mem (γ := Set (OpenPartialHomeomorph H H))
            ({OpenPartialHomeomorph.refl H} ∪ {e : OpenPartialHomeomorph H H | e.source = ∅}) (e.restr s)
x : H
hx : x ∈ e.source
s : Set H
open_s : IsOpen[inst_1] s
xs : x ∈ s
hs :
  Membership.mem (γ := Set (OpenPartialHomeomorph H H))
    ({OpenPartialHomeomorph.refl H} ∪ {e : OpenPartialHomeomorph H H | e.source = ∅}) (e.restr s)
⊢ x ∈ (e.restr s).source
have rw : x ∈ e.source ∩ s
Tactic: rw [restr_source, open_s.interior_eq]
-- 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 : OpenPartialHomeomorph H H
he :
  ∀ x ∈ e.source,
    ∃ (s : Set H),
      IsOpen[inst_1] s ∧
        x ∈ s ∧
          Membership.mem (γ := Set (OpenPartialHomeomorph H H))
            ({OpenPartialHomeomorph.refl H} ∪ {e : OpenPartialHomeomorph H H | e.source = ∅}) (e.restr s)
x : H
hx : x ∈ e.source
s : Set H
open_s : IsOpen[inst_1] s
xs : x ∈ s
hs :
  Membership.mem (γ := Set (OpenPartialHomeomorph H H))
    ({OpenPartialHomeomorph.refl H} ∪ {e : OpenPartialHomeomorph H H | e.source = ∅}) (e.restr s)
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph H H)) {OpenPartialHomeomorph.refl H} e
have x's : x ∈ (e.restr s).source
Tactic: have x's : x ∈ (e.restr s).source := by
        rw [restr_source, open_s.interior_eq]
        exact ⟨hx, xs⟩
-- 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 : OpenPartialHomeomorph H H
he :
  ∀ x ∈ e.source,
    ∃ (s : Set H),
      IsOpen[inst_1] s ∧
        x ∈ s ∧
          Membership.mem (γ := Set (OpenPartialHomeomorph H H))
            ({OpenPartialHomeomorph.refl H} ∪ {e : OpenPartialHomeomorph H H | e.source = ∅}) (e.restr s)
x : H
hx : x ∈ e.source
s : Set H
open_s : IsOpen[inst_1] s
xs : x ∈ s
hs :
  Membership.mem (γ := Set (OpenPartialHomeomorph H H))
    ({OpenPartialHomeomorph.refl H} ∪ {e : OpenPartialHomeomorph H H | e.source = ∅}) (e.restr s)
x's : x ∈ (e.restr s).source
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph H H)) {OpenPartialHomeomorph.refl H} e
have inr : ∀ (hs : Membership.mem (γ := Set (OpenPartialHomeomorph H H)) {OpenPartialHomeomorph.refl H} (e.restr s)),
  Membership.mem (γ := Set (OpenPartialHomeomorph H H)) {OpenPartialHomeomorph.refl H} e
Tactic: rcases hs with hs | hs
Cleared hypotheses: hs
-- 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 : OpenPartialHomeomorph H H
he :
  ∀ x ∈ e.source,
    ∃ (s : Set H),
      IsOpen[inst_1] s ∧
        x ∈ s ∧
          Membership.mem (γ := Set (OpenPartialHomeomorph H H))
            ({OpenPartialHomeomorph.refl H} ∪ {e : OpenPartialHomeomorph H H | e.source = ∅}) (e.restr s)
x : H
hx : x ∈ e.source
s : Set H
open_s : IsOpen[inst_1] s
xs : x ∈ s
hs :
  Membership.mem (γ := Set (OpenPartialHomeomorph H H))
    ({OpenPartialHomeomorph.refl H} ∪ {e : OpenPartialHomeomorph H H | e.source = ∅}) (e.restr s)
x's : x ∈ (e.restr s).source
inr :
  ∀ (hs : Membership.mem (γ := Set (OpenPartialHomeomorph H H)) {OpenPartialHomeomorph.refl H} (e.restr s)),
    Membership.mem (γ := Set (OpenPartialHomeomorph H H)) {OpenPartialHomeomorph.refl H} e
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph H H)) {OpenPartialHomeomorph.refl H} e
have inr₁ : ∀
  (hs :
    Membership.mem (γ := Set (OpenPartialHomeomorph H H)) {e : OpenPartialHomeomorph H H | e.source = ∅} (e.restr s)),
  Membership.mem (γ := Set (OpenPartialHomeomorph H H)) {OpenPartialHomeomorph.refl H} e
Tactic: rcases hs with hs | hs
Cleared hypotheses: hs
-- 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 : OpenPartialHomeomorph H H
he :
  ∀ x ∈ e.source,
    ∃ (s : Set H),
      IsOpen[inst_1] s ∧
        x ∈ s ∧
          Membership.mem (γ := Set (OpenPartialHomeomorph H H))
            ({OpenPartialHomeomorph.refl H} ∪ {e : OpenPartialHomeomorph H H | e.source = ∅}) (e.restr s)
x : H
hx : x ∈ e.source
s : Set H
open_s : IsOpen[inst_1] s
xs : x ∈ s
x's : x ∈ (e.restr s).source
hs : Membership.mem (γ := Set (OpenPartialHomeomorph H H)) {OpenPartialHomeomorph.refl H} (e.restr s)
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph H H)) {OpenPartialHomeomorph.refl H} e
have hs₁ : e.restr s = OpenPartialHomeomorph.refl H
Tactic: replace hs : OpenPartialHomeomorph.restr e s = OpenPartialHomeomorph.refl H := by
          simpa only using hs
Cleared hypotheses: hs
-- 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 : OpenPartialHomeomorph H H
he :
  ∀ x ∈ e.source,
    ∃ (s : Set H),
      IsOpen[inst_1] s ∧
        x ∈ s ∧
          Membership.mem (γ := Set (OpenPartialHomeomorph H H))
            ({OpenPartialHomeomorph.refl H} ∪ {e : OpenPartialHomeomorph H H | e.source = ∅}) (e.restr s)
x : H
hx : x ∈ e.source
s : Set H
open_s : IsOpen[inst_1] s
xs : x ∈ s
x's : x ∈ (e.restr s).source
hs : e.restr s = OpenPartialHomeomorph.refl H
⊢ (e.restr s).source = univ
have rw : (toPartialEquiv (OpenPartialHomeomorph.refl H)).source = univ
Tactic: rw [hs]
-- 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 : OpenPartialHomeomorph H H
he :
  ∀ x ∈ e.source,
    ∃ (s : Set H),
      IsOpen[inst_1] s ∧
        x ∈ s ∧
          Membership.mem (γ := Set (OpenPartialHomeomorph H H))
            ({OpenPartialHomeomorph.refl H} ∪ {e : OpenPartialHomeomorph H H | e.source = ∅}) (e.restr s)
x : H
hx : x ∈ e.source
s : Set H
open_s : IsOpen[inst_1] s
xs : x ∈ s
x's : x ∈ (e.restr s).source
hs : e.restr s = OpenPartialHomeomorph.refl H
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph H H)) {OpenPartialHomeomorph.refl H} e
have this : (e.restr s).source = univ
Tactic: have : (e.restr s).source = univ := by
          rw [hs]
          simp
-- 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 : OpenPartialHomeomorph H H
he :
  ∀ x ∈ e.source,
    ∃ (s : Set H),
      IsOpen[inst_1] s ∧
        x ∈ s ∧
          Membership.mem (γ := Set (OpenPartialHomeomorph H H))
            ({OpenPartialHomeomorph.refl H} ∪ {e : OpenPartialHomeomorph H H | e.source = ∅}) (e.restr s)
x : H
hx : x ∈ e.source
s : Set H
open_s : IsOpen[inst_1] s
xs : x ∈ s
x's : x ∈ (e.restr s).source
hs : e.restr s = OpenPartialHomeomorph.refl H
this : (e.restr s).source = univ
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph H H)) {OpenPartialHomeomorph.refl H} e
have this₁ : e.source ∩ interior s = univ
Tactic: have : e.toPartialEquiv.source ∩ interior s = univ := this
-- 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 : OpenPartialHomeomorph H H
he :
  ∀ x ∈ e.source,
    ∃ (s : Set H),
      IsOpen[inst_1] s ∧
        x ∈ s ∧
          Membership.mem (γ := Set (OpenPartialHomeomorph H H))
            ({OpenPartialHomeomorph.refl H} ∪ {e : OpenPartialHomeomorph H H | e.source = ∅}) (e.restr s)
x : H
hx : x ∈ e.source
s : Set H
open_s : IsOpen[inst_1] s
xs : x ∈ s
x's : x ∈ (e.restr s).source
hs : e.restr s = OpenPartialHomeomorph.refl H
this_1 : (e.restr s).source = univ
this : e.source ∩ interior s = univ
⊢ univ ⊆ interior s
have rw : e.source ∩ interior s ⊆ interior s
Tactic: rw [← this]
-- 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 : OpenPartialHomeomorph H H
he :
  ∀ x ∈ e.source,
    ∃ (s : Set H),
      IsOpen[inst_1] s ∧
        x ∈ s ∧
          Membership.mem (γ := Set (OpenPartialHomeomorph H H))
            ({OpenPartialHomeomorph.refl H} ∪ {e : OpenPartialHomeomorph H H | e.source = ∅}) (e.restr s)
x : H
hx : x ∈ e.source
s : Set H
open_s : IsOpen[inst_1] s
xs : x ∈ s
x's : x ∈ (e.restr s).source
hs : e.restr s = OpenPartialHomeomorph.refl H
this_1 : (e.restr s).source = univ
this : e.source ∩ interior s = univ
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph H H)) {OpenPartialHomeomorph.refl H} e
have this₁ : univ ⊆ interior s
Tactic: have : univ ⊆ interior s := by
          rw [← this]
          exact inter_subset_right
-- 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 : OpenPartialHomeomorph H H
he :
  ∀ x ∈ e.source,
    ∃ (s : Set H),
      IsOpen[inst_1] s ∧
        x ∈ s ∧
          Membership.mem (γ := Set (OpenPartialHomeomorph H H))
            ({OpenPartialHomeomorph.refl H} ∪ {e : OpenPartialHomeomorph H H | e.source = ∅}) (e.restr s)
x : H
hx : x ∈ e.source
s : Set H
open_s : IsOpen[inst_1] s
xs : x ∈ s
x's : x ∈ (e.restr s).source
hs : e.restr s = OpenPartialHomeomorph.refl H
this_1 : (e.restr s).source = univ
this_2 : e.source ∩ interior s = univ
this : univ ⊆ interior s
⊢ s = univ
have rwa : ∀ (this : univ ⊆ s), s = univ
Tactic: rwa [open_s.interior_eq, univ_subset_iff] at this
Cleared hypotheses: this
-- 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 : OpenPartialHomeomorph H H
he :
  ∀ x ∈ e.source,
    ∃ (s : Set H),
      IsOpen[inst_1] s ∧
        x ∈ s ∧
          Membership.mem (γ := Set (OpenPartialHomeomorph H H))
            ({OpenPartialHomeomorph.refl H} ∪ {e : OpenPartialHomeomorph H H | e.source = ∅}) (e.restr s)
x : H
hx : x ∈ e.source
s : Set H
open_s : IsOpen[inst_1] s
xs : x ∈ s
x's : x ∈ (e.restr s).source
hs : e.restr s = OpenPartialHomeomorph.refl H
this_1 : (e.restr s).source = univ
this_2 : e.source ∩ interior s = univ
this : univ ⊆ interior s
rwa : ∀ (this : univ ⊆ s), s = univ
⊢ s = univ
have rwa₁ : ∀ (this : s = univ), s = univ
Tactic: rwa [open_s.interior_eq, univ_subset_iff] at this
Cleared hypotheses: this
-- 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 : OpenPartialHomeomorph H H
he :
  ∀ x ∈ e.source,
    ∃ (s : Set H),
      IsOpen[inst_1] s ∧
        x ∈ s ∧
          Membership.mem (γ := Set (OpenPartialHomeomorph H H))
            ({OpenPartialHomeomorph.refl H} ∪ {e : OpenPartialHomeomorph H H | e.source = ∅}) (e.restr s)
x : H
hx : x ∈ e.source
s : Set H
open_s : IsOpen[inst_1] s
xs : x ∈ s
x's : x ∈ (e.restr s).source
hs : e.restr s = OpenPartialHomeomorph.refl H
this_1 : (e.restr s).source = univ
this_2 : e.source ∩ interior s = univ
this : univ ⊆ interior s
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph H H)) {OpenPartialHomeomorph.refl H} e
have this₁ : s = univ
Tactic: have : s = univ := by rwa [open_s.interior_eq, univ_subset_iff] at this
-- 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 : OpenPartialHomeomorph H H
he :
  ∀ x ∈ e.source,
    ∃ (s : Set H),
      IsOpen[inst_1] s ∧
        x ∈ s ∧
          Membership.mem (γ := Set (OpenPartialHomeomorph H H))
            ({OpenPartialHomeomorph.refl H} ∪ {e : OpenPartialHomeomorph H H | e.source = ∅}) (e.restr s)
x : H
hx : x ∈ e.source
s : Set H
open_s : IsOpen[inst_1] s
xs : x ∈ s
x's : x ∈ (e.restr s).source
hs : Membership.mem (γ := Set (OpenPartialHomeomorph H H)) {e : OpenPartialHomeomorph H H | e.source = ∅} (e.restr s)
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph H H)) {OpenPartialHomeomorph.refl H} e
have inr : False
Tactic: exfalso
-- 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 : OpenPartialHomeomorph H H
he :
  ∀ x ∈ e.source,
    ∃ (s : Set H),
      IsOpen[inst_1] s ∧
        x ∈ s ∧
          Membership.mem (γ := Set (OpenPartialHomeomorph H H))
            ({OpenPartialHomeomorph.refl H} ∪ {e : OpenPartialHomeomorph H H | e.source = ∅}) (e.restr s)
x : H
hx : x ∈ e.source
s : Set H
open_s : IsOpen[inst_1] s
xs : x ∈ s
x's : x ∈ (e.restr s).source
hs : Membership.mem (γ := Set (OpenPartialHomeomorph H H)) {e : OpenPartialHomeomorph H H | e.source = ∅} (e.restr s)
⊢ False
have hs₁ : (e.restr s).source = ∅
Tactic: rw [mem_setOf_eq] at hs
Cleared hypotheses: hs
-- 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 : OpenPartialHomeomorph H H
he :
  ∀ x ∈ e.source,
    ∃ (s : Set H),
      IsOpen[inst_1] s ∧
        x ∈ s ∧
          Membership.mem (γ := Set (OpenPartialHomeomorph H H))
            ({OpenPartialHomeomorph.refl H} ∪ {e : OpenPartialHomeomorph H H | e.source = ∅}) (e.restr s)
x : H
hx : x ∈ e.source
s : Set H
open_s : IsOpen[inst_1] s
xs : x ∈ s
x's : x ∈ (e.restr s).source
hs : (e.restr s).source = ∅
⊢ False
have inr : ∀ (x's : Membership.mem (γ := Set H) ∅ x) (hs : (e.restr s).source = ∅), False
Tactic: rwa [hs] at x's
Cleared hypotheses: x's, hs
-- 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 :
  Membership.mem (γ := Set (OpenPartialHomeomorph H H))
    ({OpenPartialHomeomorph.refl H} ∪ {e : OpenPartialHomeomorph H H | e.source = ∅}) e
he'e : e' ≈ e
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph H H))
    ({OpenPartialHomeomorph.refl H} ∪ {e : OpenPartialHomeomorph H H | e.source = ∅}) e'
have inl : ∀ (he : Membership.mem (γ := Set (OpenPartialHomeomorph H H)) {OpenPartialHomeomorph.refl H} e),
  Membership.mem (γ := Set (OpenPartialHomeomorph H H))
    ({OpenPartialHomeomorph.refl H} ∪ {e : OpenPartialHomeomorph H H | e.source = ∅}) e'
Tactic: rcases he with he | he
Cleared hypotheses: 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 :
  Membership.mem (γ := Set (OpenPartialHomeomorph H H))
    ({OpenPartialHomeomorph.refl H} ∪ {e : OpenPartialHomeomorph H H | e.source = ∅}) e
he'e : e' ≈ e
inl :
  ∀ (he : Membership.mem (γ := Set (OpenPartialHomeomorph H H)) {OpenPartialHomeomorph.refl H} e),
    Membership.mem (γ := Set (OpenPartialHomeomorph H H))
      ({OpenPartialHomeomorph.refl 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 : ∀ (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'
Tactic: rcases he with he | he
Cleared hypotheses: 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
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph H H))
    ({OpenPartialHomeomorph.refl H} ∪ {e : OpenPartialHomeomorph H H | e.source = ∅}) e'
have inl : Membership.mem (γ := Set (OpenPartialHomeomorph H H)) {OpenPartialHomeomorph.refl H} e'
Tactic: left
-- 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 = e'
have refine_1 : e.source = univ
Tactic: refine eq_of_eqOnSource_univ (Setoid.symm he'e) ?_ ?_