Module: Mathlib.Geometry.Manifold.StructureGroupoid

Goal state before:
pp: case mk.mk
H✝ : Type u_1
inst✝¹ : TopologicalSpace H✝
H : Type u_2
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, 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✝ : 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, 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 :
  (fun s ↦ s.members)
      { members := members✝¹, trans' := trans'✝¹, symm' := symm'✝¹, id_mem' := id_mem'✝¹, locality' := locality'✝¹,
        mem_of_eqOnSource' := mem_of_eqOnSource'✝¹ } =
    (fun s ↦ s.members)
      { members := members✝, trans' := trans'✝, symm' := symm'✝, id_mem' := id_mem'✝, locality' := locality'✝,
        mem_of_eqOnSource' := mem_of_eqOnSource'✝ }
⊢ { members := members✝¹, trans' := trans'✝¹, symm' := symm'✝¹, id_mem' := id_mem'✝¹, locality' := locality'✝¹,
      mem_of_eqOnSource' := mem_of_eqOnSource'✝¹ } =
    { members := members✝, trans' := trans'✝, symm' := symm'✝, id_mem' := id_mem'✝, locality' := locality'✝,
      mem_of_eqOnSource' := mem_of_eqOnSource'✝ }

Tactic:
;

Goal state after:
case mk.mk
H✝ : Type u_1
inst✝¹ : TopologicalSpace H✝
H : Type u_2
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, 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✝ : 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, 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 :
  (fun s ↦ s.members)
      { members := members✝¹, trans' := trans'✝¹, symm' := symm'✝¹, id_mem' := id_mem'✝¹, locality' := locality'✝¹,
        mem_of_eqOnSource' := mem_of_eqOnSource'✝¹ } =
    (fun s ↦ s.members)
      { members := members✝, trans' := trans'✝, symm' := symm'✝, id_mem' := id_mem'✝, locality' := locality'✝,
        mem_of_eqOnSource' := mem_of_eqOnSource'✝ }
⊢ { members := members✝¹, trans' := trans'✝¹, symm' := symm'✝¹, id_mem' := id_mem'✝¹, locality' := locality'✝¹,
      mem_of_eqOnSource' := mem_of_eqOnSource'✝¹ } =
    { members := members✝, trans' := trans'✝, symm' := symm'✝, id_mem' := id_mem'✝, locality' := locality'✝,
      mem_of_eqOnSource' := mem_of_eqOnSource'✝ }