awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.SmoothApprox (goal)
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
f : E → F
ε : E → ℝ
n : ℕ∞
f_cont :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
ε_cont : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] ε
ε_pos : ∀ (x : E), 0 < ε x
⊢ ∃ (g : E → F), ContDiff ℝ (↑n : ℕ∞ω) g ∧ (∀ (x : E), dist (g x) (f x) < ε x) ∧ support g ⊆ support f
have obtain : ∀ (g : E → F) (g_contDiff : ContDiff ℝ (↑n : ℕ∞ω) g) (g_approx : ∀ (x : E), dist (g x) (f x) < ε x)
  (g_supp : support g ⊆ support f),
  ∃ (g : E → F), ContDiff ℝ (↑n : ℕ∞ω) g ∧ (∀ (x : E), dist (g x) (f x) < ε x) ∧ support g ⊆ support f
Tactic: obtain ⟨g, g_contDiff, g_approx, -, g_supp⟩ := f_cont.exists_contDiff_approx_and_eqOn n
    ε_cont ε_pos isClosed_empty mem_nhdsSet_empty contDiffOn_empty
-- Lean 4 proof step from Mathlib.Geometry.Manifold.SmoothEmbedding (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E₁ : Type u_2
inst_1 : NormedAddCommGroup E₁
inst_2 : NormedSpace 𝕜 E₁
H : Type u_6
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E₁ H
M : Type u_10
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
n : ℕ∞ω
inst_6 : IsManifold I n M
s : TopologicalSpace.Opens M
⊢ IsSmoothEmbedding.{u_1, u_2, u_2, u_6, u_6, u_10, u_10} I I (M := ↥s) n (Subtype.val (p := fun (x : M) ↦ x ∈ s))
have rw : IsImmersion.{u_2, u_1, u_2, u_6, u_6, u_10, u_10} I I (M := ↥s) n (Subtype.val (p := fun (x : M) ↦ x ∈ s)) ∧
  IsEmbedding.{u_10, u_10} (X := ↥s) (Subtype.val (p := fun (x : M) ↦ x ∈ s))
Tactic: rw [isSmoothEmbedding_iff]
-- 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
N O : StructureGroupoid H
h :
  Eq.{u_2 + 1} (α := Set (OpenPartialHomeomorph H H)) ((fun (s : StructureGroupoid H) ↦ s.members) N)
    ((fun (s : StructureGroupoid H) ↦ s.members) O)
⊢ N = O
have mk : ∀ (members : Set (OpenPartialHomeomorph H H))
  (trans' : ∀ (e e' : OpenPartialHomeomorph H H), e ∈ members → e' ∈ members → e ≫ₕ e' ∈ members)
  (symm' : ∀ e ∈ members, e.symm ∈ members) (id_mem' : OpenPartialHomeomorph.refl H ∈ members)
  (locality' :
    ∀ (e : OpenPartialHomeomorph H H),
      (∀ x ∈ e.source, ∃ (s : Set H), IsOpen[inst_1] s ∧ x ∈ s ∧ e.restr s ∈ members) → e ∈ members)
  (mem_of_eqOnSource' : ∀ (e e' : OpenPartialHomeomorph H H), e ∈ members → e' ≈ e → e' ∈ members)
  (h :
    Eq.{u_2 + 1} (α := Set (OpenPartialHomeomorph H H))
      ((fun (s : StructureGroupoid H) ↦ s.members)
        { members := members, trans' := trans', symm' := symm', id_mem' := id_mem', locality' := locality',
          mem_of_eqOnSource' := mem_of_eqOnSource' })
      ((fun (s : StructureGroupoid H) ↦ s.members) O)),
  { members := members, trans' := trans', symm' := symm', id_mem' := id_mem', locality' := locality',
      mem_of_eqOnSource' := mem_of_eqOnSource' : StructureGroupoid H } =
    O
Tactic: cases N
Cleared hypotheses: N, 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
O : StructureGroupoid H
members : Set (OpenPartialHomeomorph H H)
trans' : ∀ (e e' : OpenPartialHomeomorph H H), e ∈ members → e' ∈ members → e ≫ₕ e' ∈ members
symm' : ∀ e ∈ members, e.symm ∈ members
id_mem' : OpenPartialHomeomorph.refl H ∈ members
locality' :
  ∀ (e : OpenPartialHomeomorph H H),
    (∀ x ∈ e.source, ∃ (s : Set H), IsOpen[inst_1] s ∧ x ∈ s ∧ e.restr s ∈ members) → e ∈ members
mem_of_eqOnSource' : ∀ (e e' : OpenPartialHomeomorph H H), e ∈ members → e' ≈ e → e' ∈ members
h :
  Eq.{u_2 + 1} (α := Set (OpenPartialHomeomorph H H))
    ((fun (s : StructureGroupoid H) ↦ s.members)
      { members := members, trans' := trans', symm' := symm', id_mem' := id_mem', locality' := locality',
        mem_of_eqOnSource' := mem_of_eqOnSource' })
    ((fun (s : StructureGroupoid H) ↦ s.members) O)
⊢ { members := members, trans' := trans', symm' := symm', id_mem' := id_mem', locality' := locality',
      mem_of_eqOnSource' := mem_of_eqOnSource' : StructureGroupoid H } =
    O
have mk : ∀ (members_1 : Set (OpenPartialHomeomorph H H))
  (trans'_1 : ∀ (e e' : OpenPartialHomeomorph H H), e ∈ members_1 → e' ∈ members_1 → e ≫ₕ e' ∈ members_1)
  (symm'_1 : ∀ e ∈ members_1, e.symm ∈ members_1) (id_mem'_1 : OpenPartialHomeomorph.refl H ∈ members_1)
  (locality'_1 :
    ∀ (e : OpenPartialHomeomorph H H),
      (∀ x ∈ e.source, ∃ (s : Set H), IsOpen[inst_1] s ∧ x ∈ s ∧ e.restr s ∈ members_1) → e ∈ members_1)
  (mem_of_eqOnSource'_1 : ∀ (e e' : OpenPartialHomeomorph H H), e ∈ members_1 → e' ≈ e → e' ∈ members_1)
  (h :
    Eq.{u_2 + 1} (α := Set (OpenPartialHomeomorph H H))
      ((fun (s : StructureGroupoid H) ↦ s.members)
        { members := members, trans' := trans', symm' := symm', id_mem' := id_mem', locality' := locality',
          mem_of_eqOnSource' := mem_of_eqOnSource' })
      ((fun (s : StructureGroupoid H) ↦ s.members)
        { members := members_1, trans' := trans'_1, symm' := symm'_1, id_mem' := id_mem'_1, locality' := locality'_1,
          mem_of_eqOnSource' := mem_of_eqOnSource'_1 })),
  { members := members, trans' := trans', symm' := symm', id_mem' := id_mem', locality' := locality',
      mem_of_eqOnSource' := mem_of_eqOnSource' : StructureGroupoid H } =
    { members := members_1, trans' := trans'_1, symm' := symm'_1, id_mem' := id_mem'_1, locality' := locality'_1,
      mem_of_eqOnSource' := mem_of_eqOnSource'_1 }
Tactic: cases O
Cleared hypotheses: O, h
-- Lean 4 proof step from Mathlib.Geometry.Manifold.StructureGroupoid (goal)
Goal:
H : Type u_1
inst : TopologicalSpace H
G G' : StructureGroupoid H
e : OpenPartialHomeomorph H H
hx : ∀ x ∈ e.source, ∃ (s : Set H), IsOpen[inst] s ∧ x ∈ s ∧ e.restr s ∈ G.members ∩ G'.members
⊢ e ∈ G.members ∧ e ∈ G'.members
have refine_1 : ∀ x ∈ e.source, ∃ (s : Set H), IsOpen[inst] s ∧ x ∈ s ∧ e.restr s ∈ G.members
Tactic: refine And.intro (G.locality' e ?_) (G'.locality' e ?_)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.StructureGroupoid (goal)
Goal:
H : Type u_1
inst : TopologicalSpace H
G G' : StructureGroupoid H
e : OpenPartialHomeomorph H H
hx : ∀ x ∈ e.source, ∃ (s : Set H), IsOpen[inst] s ∧ x ∈ s ∧ e.restr s ∈ G.members ∩ G'.members
refine_1 : ∀ x ∈ e.source, ∃ (s : Set H), IsOpen[inst] s ∧ x ∈ s ∧ e.restr s ∈ G.members
⊢ e ∈ G.members ∧ e ∈ G'.members
have refine_2 : ∀ x ∈ e.source, ∃ (s : Set H), IsOpen[inst] s ∧ x ∈ s ∧ e.restr s ∈ G'.members
Tactic: refine And.intro (G.locality' e ?_) (G'.locality' e ?_)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.StructureGroupoid (goal)
Goal:
H : Type u_1
inst : TopologicalSpace H
G G' : StructureGroupoid H
e : OpenPartialHomeomorph H H
hx : ∀ x ∈ e.source, ∃ (s : Set H), IsOpen[inst] s ∧ x ∈ s ∧ e.restr s ∈ G.members ∩ G'.members
x : H
hex : x ∈ e.source
⊢ ∃ (s : Set H), IsOpen[inst] s ∧ x ∈ s ∧ e.restr s ∈ G.members
have refine_1 : ∀ (s : Set H) (hs : IsOpen[inst] s ∧ x ∈ s ∧ e.restr s ∈ G.members ∩ G'.members),
  ∃ (s : Set H), IsOpen[inst] s ∧ x ∈ s ∧ e.restr s ∈ G.members
Tactic: rcases hx x hex with ⟨s, hs⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.StructureGroupoid (goal)
Goal:
H : Type u_1
inst : TopologicalSpace H
G G' : StructureGroupoid H
e : OpenPartialHomeomorph H H
hx : ∀ x ∈ e.source, ∃ (s : Set H), IsOpen[inst] s ∧ x ∈ s ∧ e.restr s ∈ G.members ∩ G'.members
x : H
hex : x ∈ e.source
s : Set H
hs : IsOpen[inst] s ∧ x ∈ s ∧ e.restr s ∈ G.members ∩ G'.members
⊢ ∃ (s : Set H), IsOpen[inst] s ∧ x ∈ s ∧ e.restr s ∈ G.members
have h : IsOpen[inst] s ∧ x ∈ s ∧ e.restr s ∈ G.members
Tactic: use s
-- Lean 4 proof step from Mathlib.Geometry.Manifold.StructureGroupoid (goal)
Goal:
H : Type u_1
inst : TopologicalSpace H
G G' : StructureGroupoid H
e : OpenPartialHomeomorph H H
hx : ∀ x ∈ e.source, ∃ (s : Set H), IsOpen[inst] s ∧ x ∈ s ∧ e.restr s ∈ G.members ∩ G'.members
x : H
hex : x ∈ e.source
s : Set H
hs : IsOpen[inst] s ∧ x ∈ s ∧ e.restr s ∈ G.members ∩ G'.members
⊢ IsOpen[inst] s ∧ x ∈ s ∧ e.restr s ∈ G.members
have h : e.restr s ∈ G.members
Tactic: refine And.intro hs.left (And.intro hs.right.left ?_)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.StructureGroupoid (goal)
Goal:
H : Type u_1
inst : TopologicalSpace H
G G' : StructureGroupoid H
e : OpenPartialHomeomorph H H
hx : ∀ x ∈ e.source, ∃ (s : Set H), IsOpen[inst] s ∧ x ∈ s ∧ e.restr s ∈ G.members ∩ G'.members
x : H
hex : x ∈ e.source
⊢ ∃ (s : Set H), IsOpen[inst] s ∧ x ∈ s ∧ e.restr s ∈ G'.members
have refine_2 : ∀ (s : Set H) (hs : IsOpen[inst] s ∧ x ∈ s ∧ e.restr s ∈ G.members ∩ G'.members),
  ∃ (s : Set H), IsOpen[inst] s ∧ x ∈ s ∧ e.restr s ∈ G'.members
Tactic: rcases hx x hex with ⟨s, hs⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.StructureGroupoid (goal)
Goal:
H : Type u_1
inst : TopologicalSpace H
G G' : StructureGroupoid H
e : OpenPartialHomeomorph H H
hx : ∀ x ∈ e.source, ∃ (s : Set H), IsOpen[inst] s ∧ x ∈ s ∧ e.restr s ∈ G.members ∩ G'.members
x : H
hex : x ∈ e.source
s : Set H
hs : IsOpen[inst] s ∧ x ∈ s ∧ e.restr s ∈ G.members ∩ G'.members
⊢ ∃ (s : Set H), IsOpen[inst] s ∧ x ∈ s ∧ e.restr s ∈ G'.members
have h : IsOpen[inst] s ∧ x ∈ s ∧ e.restr s ∈ G'.members
Tactic: use s
-- Lean 4 proof step from Mathlib.Geometry.Manifold.StructureGroupoid (goal)
Goal:
H : Type u_1
inst : TopologicalSpace H
G G' : StructureGroupoid H
e : OpenPartialHomeomorph H H
hx : ∀ x ∈ e.source, ∃ (s : Set H), IsOpen[inst] s ∧ x ∈ s ∧ e.restr s ∈ G.members ∩ G'.members
x : H
hex : x ∈ e.source
s : Set H
hs : IsOpen[inst] s ∧ x ∈ s ∧ e.restr s ∈ G.members ∩ G'.members
⊢ IsOpen[inst] s ∧ x ∈ s ∧ e.restr s ∈ G'.members
have h : e.restr s ∈ G'.members
Tactic: refine And.intro hs.left (And.intro hs.right.left ?_)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.StructureGroupoid (goal)
Goal:
H : Type u_1
inst : TopologicalSpace H
S : Set (StructureGroupoid H)
⊢ ∀ (e e' : OpenPartialHomeomorph H H),
    Membership.mem (γ := Set (OpenPartialHomeomorph H H)) (⋂ s ∈ S, s.members) e →
      Membership.mem (γ := Set (OpenPartialHomeomorph H H)) (⋂ s ∈ S, s.members) e' →
        Membership.mem (γ := Set (OpenPartialHomeomorph H H)) (⋂ s ∈ S, s.members) (e ≫ₕ e')
have simp : ∀ (e e' : OpenPartialHomeomorph H H),
  (∀ (i : StructureGroupoid H) (i_1 : i ∈ S), e ∈ i.members) →
    (∀ (i : StructureGroupoid H) (i_1 : i ∈ S), e' ∈ i.members) →
      ∀ (i : StructureGroupoid H) (i_1 : i ∈ S), e ≫ₕ e' ∈ i.members
Tactic: simp only [mem_iInter]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.StructureGroupoid (goal)
Goal:
H : Type u_1
inst : TopologicalSpace H
S : Set (StructureGroupoid H)
⊢ ∀ (e : OpenPartialHomeomorph H H),
    Membership.mem (γ := Set (OpenPartialHomeomorph H H)) (⋂ s ∈ S, s.members) e →
      Membership.mem (γ := Set (OpenPartialHomeomorph H H)) (⋂ s ∈ S, s.members) e.symm
have simp : ∀ (e : OpenPartialHomeomorph H H),
  (∀ (i : StructureGroupoid H) (i_1 : i ∈ S), e ∈ i.members) →
    ∀ (i : StructureGroupoid H) (i_1 : i ∈ S), e.symm ∈ i.members
Tactic: simp only [mem_iInter]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.StructureGroupoid (goal)
Goal:
H : Type u_1
inst : TopologicalSpace H
S : Set (StructureGroupoid H)
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph H H)) (⋂ s ∈ S, s.members) (OpenPartialHomeomorph.refl H)
have simp : ∀ (i : StructureGroupoid H) (i_1 : i ∈ S), OpenPartialHomeomorph.refl H ∈ i.members
Tactic: simp only [mem_iInter]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.StructureGroupoid (goal)
Goal:
H : Type u_1
inst : TopologicalSpace H
S : Set (StructureGroupoid H)
⊢ ∀ (e : OpenPartialHomeomorph H H),
    (∀ x ∈ e.source,
        ∃ (s : Set H),
          IsOpen[inst] s ∧
            x ∈ s ∧ Membership.mem (γ := Set (OpenPartialHomeomorph H H)) (⋂ s ∈ S, s.members) (e.restr s)) →
      Membership.mem (γ := Set (OpenPartialHomeomorph H H)) (⋂ s ∈ S, s.members) e
have simp : ∀ (e : OpenPartialHomeomorph H H),
  (∀ x ∈ e.source,
      ∃ (s : Set H), IsOpen[inst] s ∧ x ∈ s ∧ ∀ (i : StructureGroupoid H) (i_1 : i ∈ S), e.restr s ∈ i.members) →
    ∀ (i : StructureGroupoid H) (i_1 : i ∈ S), e ∈ i.members
Tactic: simp only [mem_iInter]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.StructureGroupoid (goal)
Goal:
H : Type u_1
inst : TopologicalSpace H
S : Set (StructureGroupoid H)
e : OpenPartialHomeomorph H H
he :
  ∀ x ∈ e.source,
    ∃ (s : Set H), IsOpen[inst] s ∧ x ∈ s ∧ ∀ (i : StructureGroupoid H) (i_1 : i ∈ S), e.restr s ∈ i.members
i : StructureGroupoid H
hi : i ∈ S
⊢ e ∈ i.members
have refine : ∀ x ∈ e.source, ∃ (s : Set H), IsOpen[inst] s ∧ x ∈ s ∧ e.restr s ∈ i.members
Tactic: refine i.locality' e ?_
-- Lean 4 proof step from Mathlib.Geometry.Manifold.StructureGroupoid (goal)
Goal:
H : Type u_1
inst : TopologicalSpace H
S : Set (StructureGroupoid H)
e : OpenPartialHomeomorph H H
he :
  ∀ x ∈ e.source,
    ∃ (s : Set H), IsOpen[inst] s ∧ x ∈ s ∧ ∀ (i : StructureGroupoid H) (i_1 : i ∈ S), e.restr s ∈ i.members
i : StructureGroupoid H
hi : i ∈ S
x : H
hex : x ∈ e.source
⊢ ∃ (s : Set H), IsOpen[inst] s ∧ x ∈ s ∧ e.restr s ∈ i.members
have rcases : ∀ (s : Set H) (hs : IsOpen[inst] s ∧ x ∈ s ∧ ∀ (i : StructureGroupoid H) (i_1 : i ∈ S), e.restr s ∈ i.members),
  ∃ (s : Set H), IsOpen[inst] s ∧ x ∈ s ∧ e.restr s ∈ i.members
Tactic: rcases he x hex with ⟨s, hs⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.StructureGroupoid (goal)
Goal:
H : Type u_1
inst : TopologicalSpace H
S : Set (StructureGroupoid H)
⊢ ∀ (e e' : OpenPartialHomeomorph H H),
    Membership.mem (γ := Set (OpenPartialHomeomorph H H)) (⋂ s ∈ S, s.members) e →
      e' ≈ e → Membership.mem (γ := Set (OpenPartialHomeomorph H H)) (⋂ s ∈ S, s.members) e'
have simp : ∀ (e e' : OpenPartialHomeomorph H H),
  (∀ (i : StructureGroupoid H) (i_1 : i ∈ S), e ∈ i.members) →
    e' ≈ e → ∀ (i : StructureGroupoid H) (i_1 : i ∈ S), e' ∈ i.members
Tactic: simp only [mem_iInter]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.StructureGroupoid (goal)
Goal:
H : Type u_1
inst : TopologicalSpace H
a b : StructureGroupoid H
h : a.members = b.members
⊢ a = b
have mk : ∀ (members : Set (OpenPartialHomeomorph H H))
  (trans' : ∀ (e e' : OpenPartialHomeomorph H H), e ∈ members → e' ∈ members → e ≫ₕ e' ∈ members)
  (symm' : ∀ e ∈ members, e.symm ∈ members) (id_mem' : OpenPartialHomeomorph.refl H ∈ members)
  (locality' :
    ∀ (e : OpenPartialHomeomorph H H),
      (∀ x ∈ e.source, ∃ (s : Set H), IsOpen[inst] s ∧ x ∈ s ∧ e.restr s ∈ members) → e ∈ members)
  (mem_of_eqOnSource' : ∀ (e e' : OpenPartialHomeomorph H H), e ∈ members → e' ≈ e → e' ∈ members)
  (h :
    { members := members, trans' := trans', symm' := symm', id_mem' := id_mem', locality' := locality',
          mem_of_eqOnSource' := mem_of_eqOnSource' : StructureGroupoid H }.members =
      b.members),
  { members := members, trans' := trans', symm' := symm', id_mem' := id_mem', locality' := locality',
      mem_of_eqOnSource' := mem_of_eqOnSource' : StructureGroupoid H } =
    b
Tactic: cases a
Cleared hypotheses: a, h
-- Lean 4 proof step from Mathlib.Geometry.Manifold.StructureGroupoid (goal)
Goal:
H : Type u_1
inst : TopologicalSpace H
b : StructureGroupoid H
members : Set (OpenPartialHomeomorph H H)
trans' : ∀ (e e' : OpenPartialHomeomorph H H), e ∈ members → e' ∈ members → e ≫ₕ e' ∈ members
symm' : ∀ e ∈ members, e.symm ∈ members
id_mem' : OpenPartialHomeomorph.refl H ∈ members
locality' :
  ∀ (e : OpenPartialHomeomorph H H),
    (∀ x ∈ e.source, ∃ (s : Set H), IsOpen[inst] s ∧ x ∈ s ∧ e.restr s ∈ members) → e ∈ members
mem_of_eqOnSource' : ∀ (e e' : OpenPartialHomeomorph H H), e ∈ members → e' ≈ e → e' ∈ members
h :
  { members := members, trans' := trans', symm' := symm', id_mem' := id_mem', locality' := locality',
        mem_of_eqOnSource' := mem_of_eqOnSource' : StructureGroupoid H }.members =
    b.members
⊢ { members := members, trans' := trans', symm' := symm', id_mem' := id_mem', locality' := locality',
      mem_of_eqOnSource' := mem_of_eqOnSource' : StructureGroupoid H } =
    b
have mk : ∀ (members_1 : Set (OpenPartialHomeomorph H H))
  (trans'_1 : ∀ (e e' : OpenPartialHomeomorph H H), e ∈ members_1 → e' ∈ members_1 → e ≫ₕ e' ∈ members_1)
  (symm'_1 : ∀ e ∈ members_1, e.symm ∈ members_1) (id_mem'_1 : OpenPartialHomeomorph.refl H ∈ members_1)
  (locality'_1 :
    ∀ (e : OpenPartialHomeomorph H H),
      (∀ x ∈ e.source, ∃ (s : Set H), IsOpen[inst] s ∧ x ∈ s ∧ e.restr s ∈ members_1) → e ∈ members_1)
  (mem_of_eqOnSource'_1 : ∀ (e e' : OpenPartialHomeomorph H H), e ∈ members_1 → e' ≈ e → e' ∈ members_1)
  (h :
    { members := members, trans' := trans', symm' := symm', id_mem' := id_mem', locality' := locality',
          mem_of_eqOnSource' := mem_of_eqOnSource' : StructureGroupoid H }.members =
      { members := members_1, trans' := trans'_1, symm' := symm'_1, id_mem' := id_mem'_1, locality' := locality'_1,
          mem_of_eqOnSource' := mem_of_eqOnSource'_1 }.members),
  { members := members, trans' := trans', symm' := symm', id_mem' := id_mem', locality' := locality',
      mem_of_eqOnSource' := mem_of_eqOnSource' : StructureGroupoid H } =
    { members := members_1, trans' := trans'_1, symm' := symm'_1, id_mem' := id_mem'_1, locality' := locality'_1,
      mem_of_eqOnSource' := mem_of_eqOnSource'_1 }
Tactic: cases b
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.Geometry.Manifold.StructureGroupoid (goal)
Goal:
H : Type u_1
inst : TopologicalSpace H
members : Set (OpenPartialHomeomorph H H)
trans' : ∀ (e e' : OpenPartialHomeomorph H H), e ∈ members → e' ∈ members → e ≫ₕ e' ∈ members
symm' : ∀ e ∈ members, e.symm ∈ members
id_mem' : OpenPartialHomeomorph.refl H ∈ members
locality' :
  ∀ (e : OpenPartialHomeomorph H H),
    (∀ x ∈ e.source, ∃ (s : Set H), IsOpen[inst] s ∧ x ∈ s ∧ e.restr s ∈ members) → e ∈ members
mem_of_eqOnSource' : ∀ (e e' : OpenPartialHomeomorph H H), e ∈ members → e' ≈ e → e' ∈ members
members_1 : Set (OpenPartialHomeomorph H H)
trans'_1 : ∀ (e e' : OpenPartialHomeomorph H H), e ∈ members_1 → e' ∈ members_1 → e ≫ₕ e' ∈ members_1
symm'_1 : ∀ e ∈ members_1, e.symm ∈ members_1
id_mem'_1 : OpenPartialHomeomorph.refl H ∈ members_1
locality'_1 :
  ∀ (e : OpenPartialHomeomorph H H),
    (∀ x ∈ e.source, ∃ (s : Set H), IsOpen[inst] s ∧ x ∈ s ∧ e.restr s ∈ members_1) → e ∈ members_1
mem_of_eqOnSource'_1 : ∀ (e e' : OpenPartialHomeomorph H H), e ∈ members_1 → e' ≈ e → e' ∈ members_1
h : members = members_1
⊢ { members := members, trans' := trans', symm' := symm', id_mem' := id_mem', locality' := locality',
      mem_of_eqOnSource' := mem_of_eqOnSource' : StructureGroupoid H } =
    { members := members_1, trans' := trans'_1, symm' := symm'_1, id_mem' := id_mem'_1, locality' := locality'_1,
      mem_of_eqOnSource' := mem_of_eqOnSource'_1 }
have mk : ∀ (trans'_2 : ∀ (e e' : OpenPartialHomeomorph H H), e ∈ members → e' ∈ members → e ≫ₕ e' ∈ members)
  (symm'_2 : ∀ e ∈ members, e.symm ∈ members) (id_mem'_2 : OpenPartialHomeomorph.refl H ∈ members)
  (locality'_2 :
    ∀ (e : OpenPartialHomeomorph H H),
      (∀ x ∈ e.source, ∃ (s : Set H), IsOpen[inst] s ∧ x ∈ s ∧ e.restr s ∈ members) → e ∈ members)
  (mem_of_eqOnSource'_2 : ∀ (e e' : OpenPartialHomeomorph H H), e ∈ members → e' ≈ e → e' ∈ members),
  { members := members, trans' := trans', symm' := symm', id_mem' := id_mem', locality' := locality',
      mem_of_eqOnSource' := mem_of_eqOnSource' : StructureGroupoid H } =
    { members := members, trans' := trans'_2, symm' := symm'_2, id_mem' := id_mem'_2, locality' := locality'_2,
      mem_of_eqOnSource' := mem_of_eqOnSource'_2 }
Tactic: induction h
Cleared hypotheses: trans'_1, symm'_1, id_mem'_1, locality'_1, mem_of_eqOnSource'_1, 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 e' : OpenPartialHomeomorph H H
he :
  Membership.mem (γ := Set (OpenPartialHomeomorph H H))
    ({OpenPartialHomeomorph.refl H} ∪ {e : OpenPartialHomeomorph H H | e.source = ∅}) e
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 ≫ₕ 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 ≫ₕ 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' :
  Membership.mem (γ := Set (OpenPartialHomeomorph H H))
    ({OpenPartialHomeomorph.refl H} ∪ {e : OpenPartialHomeomorph H H | e.source = ∅}) 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 ≫ₕ e')
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph H H))
    ({OpenPartialHomeomorph.refl H} ∪ {e : OpenPartialHomeomorph H H | e.source = ∅}) (e ≫ₕ 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 ≫ₕ e')
Tactic: rcases he with he | he
Cleared hypotheses: 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' :
  Membership.mem (γ := Set (OpenPartialHomeomorph H H))
    ({OpenPartialHomeomorph.refl H} ∪ {e : OpenPartialHomeomorph H H | e.source = ∅}) 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 ≫ₕ e')
have this : (e ≫ₕ e').source ⊆ e.source
Tactic: have : (e ≫ₕ e').source ⊆ e.source := sep_subset _ _
-- 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' :
  Membership.mem (γ := Set (OpenPartialHomeomorph H H))
    ({OpenPartialHomeomorph.refl H} ∪ {e : OpenPartialHomeomorph H H | e.source = ∅}) e'
he : Membership.mem (γ := Set (OpenPartialHomeomorph H H)) {e : OpenPartialHomeomorph H H | e.source = ∅} e
this : (e ≫ₕ e').source ⊆ e.source
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph H H))
    ({OpenPartialHomeomorph.refl H} ∪ {e : OpenPartialHomeomorph H H | e.source = ∅}) (e ≫ₕ e')
have this₁ : (e ≫ₕ e').source ⊆ ∅
Tactic: rw [he] 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 e' : OpenPartialHomeomorph H H
he' :
  Membership.mem (γ := Set (OpenPartialHomeomorph H H))
    ({OpenPartialHomeomorph.refl H} ∪ {e : OpenPartialHomeomorph H H | e.source = ∅}) e'
he : Membership.mem (γ := Set (OpenPartialHomeomorph H H)) {e : OpenPartialHomeomorph H H | e.source = ∅} e
this : (e ≫ₕ e').source ⊆ ∅
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph H H))
    ({OpenPartialHomeomorph.refl H} ∪ {e : OpenPartialHomeomorph H H | e.source = ∅}) (e ≫ₕ e')
have this₁ : Membership.mem (γ := Set (OpenPartialHomeomorph H H)) {e : OpenPartialHomeomorph H H | e.source = ∅} (e ≫ₕ e')
Tactic: have : e ≫ₕ e' ∈ { e : OpenPartialHomeomorph H H | e.source = ∅ } := eq_bot_iff.2 this