awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Covering.Basic
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
inst_2 : T2Space E
x : X
hf : IsClosedMap f
fin : (f ⁻¹' {x}).Finite
h_1 : ∀ e ∈ f ⁻¹' {x}, ∃ (φ : OpenPartialHomeomorph E X), e ∈ φ.source ∧ (↑φ : E → X) = f
this_1 : DiscreteTopology.{u_1} (↑(f ⁻¹' {x}) : Type u_1)
φ : (e : (↑(f ⁻¹' {x}) : Type u_1)) → OpenPartialHomeomorph E X
hφ : ∀ (e : (↑(f ⁻¹' {x}) : Type u_1)), (↑e : E) ∈ (φ e).source ∧ (↑(φ e) : E → X) = f
V : E → Set E
hV : ∀ (x : E), x ∈ V x ∧ IsOpen[inst] (V x)
disj : (f ⁻¹' {x}).PairwiseDisjoint V
V' : (e : (↑(f ⁻¹' {x}) : Type u_1)) → Set E := fun (e : (↑(f ⁻¹' {x}) : Type u_1)) ↦ V (↑e : E) ∩ (φ e).source
hV' : ∀ (e : (↑(f ⁻¹' {x}) : Type u_1)), IsOpen[inst] (V' e)
this_2 : ⋃ (e : (↑(f ⁻¹' {x}) : Type u_1)), V' e ∈ 𝓝ˢ (f ⁻¹' {x})
W : Set X
hWx : W ∈ 𝓝 x
hWV : f ⁻¹' W ⊆ ⋃ (e : (↑(f ⁻¹' {x}) : Type u_1)), V' e
h_2 : Nonempty.{u_1 + 1} (↑(f ⁻¹' {x}) : Type u_1)
U : Set X
hUW : U ⊆ W
hU : IsOpen[inst_1] U
hxU : x ∈ U
U' : Set X := U ∩ ⋂ (e : (↑(f ⁻¹' {x}) : Type u_1)), f '' V' e
this_3 : Finite.{u_1 + 1} (↑(f ⁻¹' {x}) : Type u_1)
hU' : IsOpen[inst_1] U'
hUV : ∀ (e : (↑(f ⁻¹' {x}) : Type u_1)), U' ⊆ f '' V' e
this_4 : Nonempty E
e : (↑(f ⁻¹' {x}) : Type u_1)
s : Set X
hs : s ⊆ U'
h_3 : IsOpen[inst] (f ⁻¹' s ∩ V' e)
this : s ⊆ (φ e).target
e' : E
h : e' ∈ f ⁻¹' s ∩ (φ e).source
h₁ : ∀ e'' ∈ V (↑e : E), ∀ (mem : e'' ∈ (φ e).source) (eq : f e'' = f e'), e' ∈ V (↑e : E)
⊢ e' ∈ V (↑e : E)

Tactic:
have ⟨e'', ⟨_, mem⟩, eq⟩ := mem_iInter.mp (hs h.1).2 e
-- Module: Mathlib.Topology.Covering.Basic
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
inst_2 : T2Space E
x : X
hf : IsClosedMap f
fin : (f ⁻¹' {x}).Finite
h_1 : ∀ e ∈ f ⁻¹' {x}, ∃ (φ : OpenPartialHomeomorph E X), e ∈ φ.source ∧ (↑φ : E → X) = f
this_1 : DiscreteTopology.{u_1} (↑(f ⁻¹' {x}) : Type u_1)
φ : (e : (↑(f ⁻¹' {x}) : Type u_1)) → OpenPartialHomeomorph E X
hφ : ∀ (e : (↑(f ⁻¹' {x}) : Type u_1)), (↑e : E) ∈ (φ e).source ∧ (↑(φ e) : E → X) = f
V : E → Set E
hV : ∀ (x : E), x ∈ V x ∧ IsOpen[inst] (V x)
disj : (f ⁻¹' {x}).PairwiseDisjoint V
V' : (e : (↑(f ⁻¹' {x}) : Type u_1)) → Set E := fun (e : (↑(f ⁻¹' {x}) : Type u_1)) ↦ V (↑e : E) ∩ (φ e).source
hV' : ∀ (e : (↑(f ⁻¹' {x}) : Type u_1)), IsOpen[inst] (V' e)
this_2 : ⋃ (e : (↑(f ⁻¹' {x}) : Type u_1)), V' e ∈ 𝓝ˢ (f ⁻¹' {x})
W : Set X
hWx : W ∈ 𝓝 x
hWV : f ⁻¹' W ⊆ ⋃ (e : (↑(f ⁻¹' {x}) : Type u_1)), V' e
h_2 : Nonempty.{u_1 + 1} (↑(f ⁻¹' {x}) : Type u_1)
U : Set X
hUW : U ⊆ W
hU : IsOpen[inst_1] U
hxU : x ∈ U
U' : Set X := U ∩ ⋂ (e : (↑(f ⁻¹' {x}) : Type u_1)), f '' V' e
this_3 : Finite.{u_1 + 1} (↑(f ⁻¹' {x}) : Type u_1)
hU' : IsOpen[inst_1] U'
hUV : ∀ (e : (↑(f ⁻¹' {x}) : Type u_1)), U' ⊆ f '' V' e
this_4 : Nonempty E
e : (↑(f ⁻¹' {x}) : Type u_1)
s : Set X
hs : s ⊆ U'
h_3 : IsOpen[inst] (f ⁻¹' s ∩ V' e)
this : s ⊆ (φ e).target
e' : E
h : e' ∈ f ⁻¹' s ∩ (φ e).source
e'' : E
left : e'' ∈ V (↑e : E)
mem : e'' ∈ (φ e).source
eq rwa rwa₁ rwa₂ rwa₃ : f e'' = f e'
⊢ (↑(φ e) : E → X) e'' = (↑(φ e) : E → X) e'

Tactic:
rwa [(hφ e).2]

Premises used: And.right
-- Module: Mathlib.Topology.Covering.Basic
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
inst_2 : T2Space E
x : X
hf : IsClosedMap f
fin : (f ⁻¹' {x}).Finite
h_1 : ∀ e ∈ f ⁻¹' {x}, ∃ (φ : OpenPartialHomeomorph E X), e ∈ φ.source ∧ (↑φ : E → X) = f
this_1 : DiscreteTopology.{u_1} (↑(f ⁻¹' {x}) : Type u_1)
φ : (e : (↑(f ⁻¹' {x}) : Type u_1)) → OpenPartialHomeomorph E X
hφ : ∀ (e : (↑(f ⁻¹' {x}) : Type u_1)), (↑e : E) ∈ (φ e).source ∧ (↑(φ e) : E → X) = f
V : E → Set E
hV : ∀ (x : E), x ∈ V x ∧ IsOpen[inst] (V x)
disj : (f ⁻¹' {x}).PairwiseDisjoint V
V' : (e : (↑(f ⁻¹' {x}) : Type u_1)) → Set E := fun (e : (↑(f ⁻¹' {x}) : Type u_1)) ↦ V (↑e : E) ∩ (φ e).source
hV' : ∀ (e : (↑(f ⁻¹' {x}) : Type u_1)), IsOpen[inst] (V' e)
this_2 : ⋃ (e : (↑(f ⁻¹' {x}) : Type u_1)), V' e ∈ 𝓝ˢ (f ⁻¹' {x})
W : Set X
hWx : W ∈ 𝓝 x
hWV : f ⁻¹' W ⊆ ⋃ (e : (↑(f ⁻¹' {x}) : Type u_1)), V' e
h_2 : Nonempty.{u_1 + 1} (↑(f ⁻¹' {x}) : Type u_1)
U : Set X
hUW : U ⊆ W
hU : IsOpen[inst_1] U
hxU : x ∈ U
U' : Set X := U ∩ ⋂ (e : (↑(f ⁻¹' {x}) : Type u_1)), f '' V' e
this_3 : Finite.{u_1 + 1} (↑(f ⁻¹' {x}) : Type u_1)
hU' : IsOpen[inst_1] U'
hUV : ∀ (e : (↑(f ⁻¹' {x}) : Type u_1)), U' ⊆ f '' V' e
this_4 : Nonempty E
e : (↑(f ⁻¹' {x}) : Type u_1)
s : Set X
hs : s ⊆ U'
h_3 : IsOpen[inst] (f ⁻¹' s ∩ V' e)
this : s ⊆ (φ e).target
e' : E
h : e' ∈ f ⁻¹' s ∩ (φ e).source
e'' : E
left : e'' ∈ V (↑e : E)
mem : e'' ∈ (φ e).source
eq : f e'' = f e'
h₁ h₂ h₃ h₄ : e'' ∈ V (↑e : E)
⊢ e' ∈ V (↑e : E)

Tactic:
rwa [← (φ e).injOn mem h.2 (by rwa [(hφ e).2])]

Premises used: And.right, OpenPartialHomeomorph.injOn
-- Module: Mathlib.Topology.Covering.Basic
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
inst_2 : T2Space E
x : X
hf : IsClosedMap f
fin : (f ⁻¹' {x}).Finite
h : ∀ e ∈ f ⁻¹' {x}, ∃ (φ : OpenPartialHomeomorph E X), e ∈ φ.source ∧ (↑φ : E → X) = f
this_1 : DiscreteTopology.{u_1} (↑(f ⁻¹' {x}) : Type u_1)
φ : (e : (↑(f ⁻¹' {x}) : Type u_1)) → OpenPartialHomeomorph E X
hφ : ∀ (e : (↑(f ⁻¹' {x}) : Type u_1)), (↑e : E) ∈ (φ e).source ∧ (↑(φ e) : E → X) = f
V : E → Set E
hV : ∀ (x : E), x ∈ V x ∧ IsOpen[inst] (V x)
disj : (f ⁻¹' {x}).PairwiseDisjoint V
V' : (e : (↑(f ⁻¹' {x}) : Type u_1)) → Set E := fun (e : (↑(f ⁻¹' {x}) : Type u_1)) ↦ V (↑e : E) ∩ (φ e).source
hV' : ∀ (e : (↑(f ⁻¹' {x}) : Type u_1)), IsOpen[inst] (V' e)
this_2 : ⋃ (e : (↑(f ⁻¹' {x}) : Type u_1)), V' e ∈ 𝓝ˢ (f ⁻¹' {x})
W : Set X
hWx : W ∈ 𝓝 x
hWV : f ⁻¹' W ⊆ ⋃ (e : (↑(f ⁻¹' {x}) : Type u_1)), V' e
h_1 : Nonempty.{u_1 + 1} (↑(f ⁻¹' {x}) : Type u_1)
U : Set X
hUW : U ⊆ W
hU : IsOpen[inst_1] U
hxU : x ∈ U
U' : Set X := U ∩ ⋂ (e : (↑(f ⁻¹' {x}) : Type u_1)), f '' V' e
this_3 : Finite.{u_1 + 1} (↑(f ⁻¹' {x}) : Type u_1)
hU' : IsOpen[inst_1] U'
hUV : ∀ (e : (↑(f ⁻¹' {x}) : Type u_1)), U' ⊆ f '' V' e
this : Nonempty E
e : (↑(f ⁻¹' {x}) : Type u_1)
⊢ InjOn (↑(φ e) : E → X) (V (↑e : E) ∩ (φ e).source)

Tactic:
(φ e).injOn.mono inter_subset_right

Premises used: OpenPartialHomeomorph.injOn, Set.InjOn.mono, Set.inter_subset_right
-- Module: Mathlib.Topology.Covering.Basic
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
inst_2 : T2Space E
x : X
hf : IsClosedMap f
fin : (f ⁻¹' {x}).Finite
h : ∀ e ∈ f ⁻¹' {x}, ∃ (φ : OpenPartialHomeomorph E X), e ∈ φ.source ∧ (↑φ : E → X) = f
this_1 : DiscreteTopology.{u_1} (↑(f ⁻¹' {x}) : Type u_1)
φ : (e : (↑(f ⁻¹' {x}) : Type u_1)) → OpenPartialHomeomorph E X
hφ : ∀ (e : (↑(f ⁻¹' {x}) : Type u_1)), (↑e : E) ∈ (φ e).source ∧ (↑(φ e) : E → X) = f
V : E → Set E
hV : ∀ (x : E), x ∈ V x ∧ IsOpen[inst] (V x)
disj : (f ⁻¹' {x}).PairwiseDisjoint V
V' : (e : (↑(f ⁻¹' {x}) : Type u_1)) → Set E := fun (e : (↑(f ⁻¹' {x}) : Type u_1)) ↦ V (↑e : E) ∩ (φ e).source
hV' : ∀ (e : (↑(f ⁻¹' {x}) : Type u_1)), IsOpen[inst] (V' e)
this_2 : ⋃ (e : (↑(f ⁻¹' {x}) : Type u_1)), V' e ∈ 𝓝ˢ (f ⁻¹' {x})
W : Set X
hWx : W ∈ 𝓝 x
hWV : f ⁻¹' W ⊆ ⋃ (e : (↑(f ⁻¹' {x}) : Type u_1)), V' e
h_1 : Nonempty.{u_1 + 1} (↑(f ⁻¹' {x}) : Type u_1)
U : Set X
hUW : U ⊆ W
hU : IsOpen[inst_1] U
hxU : x ∈ U
U' : Set X := U ∩ ⋂ (e : (↑(f ⁻¹' {x}) : Type u_1)), f '' V' e
this_3 : Finite.{u_1 + 1} (↑(f ⁻¹' {x}) : Type u_1)
hU' : IsOpen[inst_1] U'
hUV : ∀ (e : (↑(f ⁻¹' {x}) : Type u_1)), U' ⊆ f '' V' e
this : Nonempty E
e : (↑(f ⁻¹' {x}) : Type u_1)
h₁ : (↑(φ e) : E → X) = f
⊢ InjOn f (V' e)

Tactic:
convert! ← (φ e).injOn.mono inter_subset_right

Premises used: OpenPartialHomeomorph.injOn, Set.InjOn.mono, Set.inter_subset_right
-- Module: Mathlib.Topology.Covering.Basic
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
inst_2 : T2Space E
x : X
hf : IsClosedMap f
fin : (f ⁻¹' {x}).Finite
h : ∀ e ∈ f ⁻¹' {x}, ∃ (φ : OpenPartialHomeomorph E X), e ∈ φ.source ∧ (↑φ : E → X) = f
this_1 : DiscreteTopology.{u_1} (↑(f ⁻¹' {x}) : Type u_1)
φ : (e : (↑(f ⁻¹' {x}) : Type u_1)) → OpenPartialHomeomorph E X
hφ : ∀ (e : (↑(f ⁻¹' {x}) : Type u_1)), (↑e : E) ∈ (φ e).source ∧ (↑(φ e) : E → X) = f
V : E → Set E
hV : ∀ (x : E), x ∈ V x ∧ IsOpen[inst] (V x)
disj : (f ⁻¹' {x}).PairwiseDisjoint V
V' : (e : (↑(f ⁻¹' {x}) : Type u_1)) → Set E := fun (e : (↑(f ⁻¹' {x}) : Type u_1)) ↦ V (↑e : E) ∩ (φ e).source
hV' : ∀ (e : (↑(f ⁻¹' {x}) : Type u_1)), IsOpen[inst] (V' e)
this_2 : ⋃ (e : (↑(f ⁻¹' {x}) : Type u_1)), V' e ∈ 𝓝ˢ (f ⁻¹' {x})
W : Set X
hWx : W ∈ 𝓝 x
hWV : f ⁻¹' W ⊆ ⋃ (e : (↑(f ⁻¹' {x}) : Type u_1)), V' e
h_1 : Nonempty.{u_1 + 1} (↑(f ⁻¹' {x}) : Type u_1)
U : Set X
hUW : U ⊆ W
hU : IsOpen[inst_1] U
hxU : x ∈ U
U' : Set X := U ∩ ⋂ (e : (↑(f ⁻¹' {x}) : Type u_1)), f '' V' e
this_3 : Finite.{u_1 + 1} (↑(f ⁻¹' {x}) : Type u_1)
hU' : IsOpen[inst_1] U'
hUV : ∀ (e : (↑(f ⁻¹' {x}) : Type u_1)), U' ⊆ f '' V' e
this : Nonempty E
e : (↑(f ⁻¹' {x}) : Type u_1)
⊢ (↑(φ e) : E → X) = f

Tactic:
(hφ e).2

Premises used: And.right
-- Module: Mathlib.Topology.Covering.Basic
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
inst_2 : T2Space E
x : X
hf : IsClosedMap f
fin : (f ⁻¹' {x}).Finite
h : ∀ e ∈ f ⁻¹' {x}, ∃ (φ : OpenPartialHomeomorph E X), e ∈ φ.source ∧ (↑φ : E → X) = f
this_1 : DiscreteTopology.{u_1} (↑(f ⁻¹' {x}) : Type u_1)
φ : (e : (↑(f ⁻¹' {x}) : Type u_1)) → OpenPartialHomeomorph E X
hφ : ∀ (e : (↑(f ⁻¹' {x}) : Type u_1)), (↑e : E) ∈ (φ e).source ∧ (↑(φ e) : E → X) = f
V : E → Set E
hV : ∀ (x : E), x ∈ V x ∧ IsOpen[inst] (V x)
disj : (f ⁻¹' {x}).PairwiseDisjoint V
V' : (e : (↑(f ⁻¹' {x}) : Type u_1)) → Set E := fun (e : (↑(f ⁻¹' {x}) : Type u_1)) ↦ V (↑e : E) ∩ (φ e).source
hV' : ∀ (e : (↑(f ⁻¹' {x}) : Type u_1)), IsOpen[inst] (V' e)
this_2 : ⋃ (e : (↑(f ⁻¹' {x}) : Type u_1)), V' e ∈ 𝓝ˢ (f ⁻¹' {x})
W : Set X
hWx : W ∈ 𝓝 x
hWV : f ⁻¹' W ⊆ ⋃ (e : (↑(f ⁻¹' {x}) : Type u_1)), V' e
h_1 : Nonempty.{u_1 + 1} (↑(f ⁻¹' {x}) : Type u_1)
U : Set X
hUW : U ⊆ W
hU : IsOpen[inst_1] U
hxU : x ∈ U
U' : Set X := U ∩ ⋂ (e : (↑(f ⁻¹' {x}) : Type u_1)), f '' V' e
this_3 : Finite.{u_1 + 1} (↑(f ⁻¹' {x}) : Type u_1)
hU' : IsOpen[inst_1] U'
hUV : ∀ (e : (↑(f ⁻¹' {x}) : Type u_1)), U' ⊆ f '' V' e
this : Nonempty E
e : (↑(f ⁻¹' {x}) : Type u_1)
⊢ (↑(φ e) : E → X) = f

Tactic:
exact (hφ e).2

Premises used: And.right
-- Module: Mathlib.Topology.Covering.Basic
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
s : Set X
inst_2 : T2Space E
hf : IsClosedMap f
hs : ∀ x ∈ s, (f ⁻¹' {x}).Finite
h : ∀ e ∈ f ⁻¹' s, ∃ (φ : OpenPartialHomeomorph E X), e ∈ φ.source ∧ (↑φ : E → X) = f
x : X
hx : x ∈ s
e : E
he : e ∈ f ⁻¹' {x}
⊢ e ∈ f ⁻¹' s

Tactic:
apply he ▸ hx
-- Module: Mathlib.Topology.Covering.Basic
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
inst_2 : T2Space E
inst_3 : T2Space X
inst_4 : CompactSpace E
x : X
hf : Continuous[inst, inst_1] f
h : ∀ e ∈ f ⁻¹' {x}, ∃ (φ : OpenPartialHomeomorph E X), e ∈ φ.source ∧ (↑φ : E → X) = f
⊢ IsEvenlyCovered f x (↑(f ⁻¹' {x}) : Type u_1)

Tactic:
hf.isClosedMap.isEvenlyCovered_of_openPartialHomeomorph
    ((isClosed_singleton.preimage hf).isCompact.finite (.of_openPartialHomeomorph f subset_rfl h)) h

Premises used: IsClosedMap.isEvenlyCovered_of_openPartialHomeomorph, IsDiscrete.of_openPartialHomeomorph, Continuous.isClosedMap, IsClosed.isCompact, IsClosed.preimage, isClosed_singleton, subset_rfl, IsCompact.finite
-- Module: Mathlib.Topology.Covering.Basic
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
s : Set X
inst_2 : T2Space E
inst_3 : T2Space X
inst_4 : CompactSpace E
hf : Continuous[inst, inst_1] f
h : ∀ e ∈ f ⁻¹' s, ∃ (φ : OpenPartialHomeomorph E X), e ∈ φ.source ∧ (↑φ : E → X) = f
x : X
hx : x ∈ s
e : E
he : e ∈ f ⁻¹' {x}
⊢ e ∈ f ⁻¹' s

Tactic:
apply he ▸ hx
-- Module: Mathlib.Topology.Covering.Quotient
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
G : Type u_3
inst_2 : Group G
inst_3 : MulAction G E
S S' : Subgroup G
eq : S = S'
rw rw₁ : IsQuotientCoveringMap.{u_1, u_2, u_3} f ↥S' ↔ IsQuotientCoveringMap.{u_1, u_2, u_3} f ↥S'
⊢ IsQuotientCoveringMap.{u_1, u_2, u_3} f ↥S ↔ IsQuotientCoveringMap.{u_1, u_2, u_3} f ↥S'

Tactic:
rw [eq]
-- Module: Mathlib.Topology.Covering.Quotient
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
G : Type u_3
inst_2 : Group G
inst_3 : MulAction G E
h : IsQuotientCoveringMap f G
g g' : G
e : E
eq : g • e = g' • e
have : ∀ (U : Set E) (heU : U ∈ 𝓝 e) (hU : ∀ (g : G), ((fun (x : E) ↦ g • x) '' U ∩ U).Nonempty → g = 1), g = g'
⊢ g = g'

Tactic:
have ⟨U, heU, hU⟩ := h.disjoint e
-- Module: Mathlib.Topology.Covering.Quotient
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
G : Type u_3
inst_2 : Group G
inst_3 : MulAction G E
h : IsQuotientCoveringMap f G
g g' : G
e : E
eq : g • e = g' • e
U : Set E
heU : U ∈ 𝓝 e
hU : ∀ (g : G), ((fun (x : E) ↦ g • x) '' U ∩ U).Nonempty → g = 1
⊢ (fun (x : E) ↦ (g'⁻¹ * g) • x) e = e

Tactic:
simpa [mul_smul, inv_smul_eq_iff]

Premises used: inv_smul_eq_iff, SemigroupAction.mul_smul
-- Module: Mathlib.Topology.Covering.Quotient
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
G : Type u_3
inst_2 : Group G
inst_3 : MulAction G E
h : IsQuotientCoveringMap f G
g g' : G
e : E
eq : g • e = g' • e
U : Set E
heU : U ∈ 𝓝 e
hU : ∀ (g : G), ((fun (x : E) ↦ g • x) '' U ∩ U).Nonempty → g = 1
⊢ g = g'

Tactic:
simpa [inv_mul_eq_one, eq_comm] using hU (g'⁻¹ * g)
      ⟨e, ⟨e, mem_of_mem_nhds heU, by simpa [mul_smul, inv_smul_eq_iff]⟩, mem_of_mem_nhds heU⟩

Premises used: HMul.hMul, mem_of_mem_nhds, eq_comm, Inv.inv, And.intro, Exists.intro, inv_mul_eq_one
-- Module: Mathlib.Topology.Covering.Quotient
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
G : Type u_3
inst_2 : Group G
inst_3 : MulAction G E
h : IsQuotientCoveringMap f G
Y : Type u_4
inst_4 : TopologicalSpace Y
φ : X ≃ₜ Y
⊢ ∀ {e₁ e₂ : E},
    Eq.{u_4 + 1} (α := Y) (((⇑φ : (a : X) → Y) ∘ f) e₁) (((⇑φ : (a : X) → Y) ∘ f) e₂) ↔ e₁ ∈ MulAction.orbit G e₂

Tactic:
simpa using @h.apply_eq_iff_mem_orbit

Premises used: IsQuotientCoveringMap.apply_eq_iff_mem_orbit
-- Module: Mathlib.Topology.Covering.Quotient
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
G : Type u_3
inst_2 : Group G
inst_3 : MulAction G E
Y : Type u_4
inst_4 : TopologicalSpace Y
φ : X ≃ₜ Y
h : IsQuotientCoveringMap.{u_1, u_4, u_3} (X := Y) ((⇑φ : (a : X) → Y) ∘ f) G
⊢ IsQuotientCoveringMap.{u_1, u_2, u_3} (X := X)
    (Function.comp.{u_1 + 1, u_4 + 1, u_2 + 1} (β := Y) (⇑φ.symm : (a : Y) → X) ((⇑φ : (a : X) → Y) ∘ f)) G

Tactic:
h.homeomorph_comp φ.symm

Premises used: Homeomorph.symm, IsQuotientCoveringMap.homeomorph_comp
-- Module: Mathlib.Topology.Covering.Quotient
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
G : Type u_3
inst_2 : Group G
inst_3 : MulAction G E
Y : Type u_4
inst_4 : TopologicalSpace Y
φ : X ≃ₜ Y
h : IsQuotientCoveringMap.{u_1, u_4, u_3} (X := Y) ((⇑φ : (a : X) → Y) ∘ f) G
h₁ : f = Function.comp.{u_1 + 1, u_4 + 1, u_2 + 1} (β := Y) (⇑φ.symm : (a : Y) → X) ((⇑φ : (a : X) → Y) ∘ f)
⊢ IsQuotientCoveringMap f G

Tactic:
convert! h.homeomorph_comp φ.symm

Premises used: Homeomorph.symm, IsQuotientCoveringMap.homeomorph_comp
-- Module: Mathlib.Topology.Covering.Quotient
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
G : Type u_3
inst_2 : Group G
inst_3 : MulAction G E
Y : Type u_4
inst_4 : TopologicalSpace Y
φ : X ≃ₜ Y
h : IsQuotientCoveringMap.{u_1, u_4, u_3} (X := Y) ((⇑φ : (a : X) → Y) ∘ f) G
h₁ :
  ∀ (x : E), f x = Function.comp.{u_1 + 1, u_4 + 1, u_2 + 1} (β := Y) (⇑φ.symm : (a : Y) → X) ((⇑φ : (a : X) → Y) ∘ f) x
⊢ f = Function.comp.{u_1 + 1, u_4 + 1, u_2 + 1} (β := Y) (⇑φ.symm : (a : Y) → X) ((⇑φ : (a : X) → Y) ∘ f)

Tactic:
ext
-- Module: Mathlib.Topology.Covering.Quotient
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
G : Type u_3
inst_2 : Group G
inst_3 : MulAction G E
Y : Type u_4
inst_4 : TopologicalSpace Y
φ : X ≃ₜ Y
h : IsQuotientCoveringMap.{u_1, u_4, u_3} (X := Y) ((⇑φ : (a : X) → Y) ∘ f) G
x : E
⊢ f x = Function.comp.{u_1 + 1, u_4 + 1, u_2 + 1} (β := Y) (⇑φ.symm : (a : Y) → X) ((⇑φ : (a : X) → Y) ∘ f) x

Tactic:
simp
-- Module: Mathlib.Topology.Covering.Quotient
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
G : Type u_3
inst_2 : Group G
inst_3 : MulAction G E
hf : IsQuotientMap f
inst_4 : ContinuousConstSMul G E
hfG : ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ MulAction.orbit G e₂
inst_5 : TopologicalSpace G
inst_6 : DiscreteTopology G
U : Set E
open_U : IsOpen[inst] U
disjoint : ∀ (g : G), ((fun (x : E) ↦ g • x) '' U ∩ U).Nonempty → g = 1
⊢ ∀ (g : G) (e : E), f (g • e) = f e

Tactic:
have pGE (g : G) e : f (g • e) = f e := hfG.mpr ⟨g, rfl⟩
-- Module: Mathlib.Topology.Covering.Quotient
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
G : Type u_3
inst_2 : Group G
inst_3 : MulAction G E
hf : IsQuotientMap f
inst_4 : ContinuousConstSMul G E
hfG : ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ MulAction.orbit G e₂
inst_5 : TopologicalSpace G
inst_6 : DiscreteTopology G
U : Set E
open_U : IsOpen[inst] U
disjoint : ∀ (g : G), ((fun (x : E) ↦ g • x) '' U ∩ U).Nonempty → g = 1
pGE : ∀ (g : G) (e : E), f (g • e) = f e
h : ∀ (e : E), e ∈ f ⁻¹' f '' U ↔ Membership.mem (γ := Set E) (⋃ (g : G), (fun (x : E) ↦ g • x) ⁻¹' U) e
⊢ f ⁻¹' f '' U = ⋃ (g : G), (fun (x : E) ↦ g • x) ⁻¹' U

Tactic:
ext e
-- Module: Mathlib.Topology.Covering.Quotient
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
G : Type u_3
inst_2 : Group G
inst_3 : MulAction G E
hf : IsQuotientMap f
inst_4 : ContinuousConstSMul G E
hfG : ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ MulAction.orbit G e₂
inst_5 : TopologicalSpace G
inst_6 : DiscreteTopology G
U : Set E
open_U : IsOpen[inst] U
disjoint : ∀ (g : G), ((fun (x : E) ↦ g • x) '' U ∩ U).Nonempty → g = 1
pGE : ∀ (g : G) (e : E), f (g • e) = f e
e : E
⊢ e ∈ f ⁻¹' f '' U ↔ Membership.mem (γ := Set E) (⋃ (g : G), (fun (x : E) ↦ g • x) ⁻¹' U) e

Tactic:
⟨fun ⟨e', heU, he⟩ ↦ ?_, ?_⟩

Premises used: Membership.mem, Set.preimage, Iff.intro, Topology.IsQuotientMap.trivializationOfSMulDisjoint.match_1, HSMul.hSMul, Set.iUnion
-- Module: Mathlib.Topology.Covering.Quotient
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
G : Type u_3
inst_2 : Group G
inst_3 : MulAction G E
hf : IsQuotientMap f
inst_4 : ContinuousConstSMul G E
hfG : ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ MulAction.orbit G e₂
inst_5 : TopologicalSpace G
inst_6 : DiscreteTopology G
U : Set E
open_U : IsOpen[inst] U
disjoint : ∀ (g : G), ((fun (x : E) ↦ g • x) '' U ∩ U).Nonempty → g = 1
pGE : ∀ (g : G) (e : E), f (g • e) = f e
e : E
h :
  e ∈ f ⁻¹' f '' U →
    ∀ (e' : E) (heU : e' ∈ U) (he : f e' = f e), Membership.mem (γ := Set E) (⋃ (g : G), (fun (x : E) ↦ g • x) ⁻¹' U) e
h₁ : Membership.mem (γ := Set E) (⋃ (g : G), (fun (x : E) ↦ g • x) ⁻¹' U) e → e ∈ f ⁻¹' f '' U
⊢ e ∈ f ⁻¹' f '' U ↔ Membership.mem (γ := Set E) (⋃ (g : G), (fun (x : E) ↦ g • x) ⁻¹' U) e

Tactic:
refine ⟨fun ⟨e', heU, he⟩ ↦ ?_, ?_⟩
-- Module: Mathlib.Topology.Covering.Quotient
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
G : Type u_3
inst_2 : Group G
inst_3 : MulAction G E
hf : IsQuotientMap f
inst_4 : ContinuousConstSMul G E
hfG : ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ MulAction.orbit G e₂
inst_5 : TopologicalSpace G
inst_6 : DiscreteTopology G
U : Set E
open_U : IsOpen[inst] U
disjoint : ∀ (g : G), ((fun (x : E) ↦ g • x) '' U ∩ U).Nonempty → g = 1
pGE : ∀ (g : G) (e : E), f (g • e) = f e
e : E
h_1 : e ∈ f ⁻¹' f '' U
e' : E
heU : e' ∈ U
he : f e' = f e
h :
  ∀ (g : G) (heU : (fun (m : G) ↦ m • e) g ∈ U) (he : f ((fun (m : G) ↦ m • e) g) = f e),
    Membership.mem (γ := Set E) (⋃ (g : G), (fun (x : E) ↦ g • x) ⁻¹' U) e
⊢ Membership.mem (γ := Set E) (⋃ (g : G), (fun (x : E) ↦ g • x) ⁻¹' U) e

Tactic:
obtain ⟨g, rfl⟩ := hfG.mp he

Premises used: Iff.mp, rfl
-- Module: Mathlib.Topology.Covering.Quotient
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
G : Type u_3
inst_2 : Group G
inst_3 : MulAction G E
hf : IsQuotientMap f
inst_4 : ContinuousConstSMul G E
hfG : ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ MulAction.orbit G e₂
inst_5 : TopologicalSpace G
inst_6 : DiscreteTopology G
U : Set E
open_U : IsOpen[inst] U
disjoint : ∀ (g : G), ((fun (x : E) ↦ g • x) '' U ∩ U).Nonempty → g = 1
pGE : ∀ (g : G) (e : E), f (g • e) = f e
e : E
h : e ∈ f ⁻¹' f '' U
g : G
heU : (fun (m : G) ↦ m • e) g ∈ U
he : f ((fun (m : G) ↦ m • e) g) = f e
⊢ Membership.mem (γ := Set E) (⋃ (g : G), (fun (x : E) ↦ g • x) ⁻¹' U) e

Tactic:
⟨_, ⟨g, rfl⟩, heU⟩

Premises used: Set.Mem, iSup, setOf, And.intro, Exists.intro, Set.iUnion, rfl
-- Module: Mathlib.Topology.Covering.Quotient
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
G : Type u_3
inst_2 : Group G
inst_3 : MulAction G E
hf : IsQuotientMap f
inst_4 : ContinuousConstSMul G E
hfG : ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ MulAction.orbit G e₂
inst_5 : TopologicalSpace G
inst_6 : DiscreteTopology G
U : Set E
open_U : IsOpen[inst] U
disjoint : ∀ (g : G), ((fun (x : E) ↦ g • x) '' U ∩ U).Nonempty → g = 1
pGE : ∀ (g : G) (e : E), f (g • e) = f e
e : E
h : e ∈ f ⁻¹' f '' U
g : G
heU : (fun (m : G) ↦ m • e) g ∈ U
he : f ((fun (m : G) ↦ m • e) g) = f e
⊢ Membership.mem (γ := Set E) (⋃ (g : G), (fun (x : E) ↦ g • x) ⁻¹' U) e

Tactic:
exact ⟨_, ⟨g, rfl⟩, heU⟩
-- Module: Mathlib.Topology.Covering.Quotient
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
G : Type u_3
inst_2 : Group G
inst_3 : MulAction G E
hf : IsQuotientMap f
inst_4 : ContinuousConstSMul G E
hfG : ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ MulAction.orbit G e₂
inst_5 : TopologicalSpace G
inst_6 : DiscreteTopology G
U : Set E
open_U : IsOpen[inst] U
disjoint : ∀ (g : G), ((fun (x : E) ↦ g • x) '' U ∩ U).Nonempty → g = 1
pGE : ∀ (g : G) (e : E), f (g • e) = f e
e : E
g : G
hg : Membership.mem (γ := Set E) ((fun (g : G) ↦ ((fun (x : E) ↦ g • x) ⁻¹' U : Set E)) g) e
⊢ e ∈ f ⁻¹' f '' U

Tactic:
⟨_, hg, pGE g e⟩

Premises used: Set.Mem, setOf, Set.preimage, And.intro, Exists.intro, Set.image
-- Module: Mathlib.Topology.Covering.Quotient
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
G : Type u_3
inst_2 : Group G
inst_3 : MulAction G E
hf : IsQuotientMap f
inst_4 : ContinuousConstSMul G E
hfG : ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ MulAction.orbit G e₂
inst_5 : TopologicalSpace G
inst_6 : DiscreteTopology G
U : Set E
open_U : IsOpen[inst] U
disjoint : ∀ (g : G), ((fun (x : E) ↦ g • x) '' U ∩ U).Nonempty → g = 1
pGE : ∀ (g : G) (e : E), f (g • e) = f e
e : E
g : G
hg : Membership.mem (γ := Set E) ((fun (g : G) ↦ ((fun (x : E) ↦ g • x) ⁻¹' U : Set E)) g) e
⊢ e ∈ f ⁻¹' f '' U

Tactic:
exact ⟨_, hg, pGE g e⟩
-- Module: Mathlib.Topology.Covering.Quotient
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
G : Type u_3
inst_2 : Group G
inst_3 : MulAction G E
hf : IsQuotientMap f
inst_4 : ContinuousConstSMul G E
hfG : ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ MulAction.orbit G e₂
inst_5 : TopologicalSpace G
inst_6 : DiscreteTopology G
U : Set E
open_U : IsOpen[inst] U
disjoint : ∀ (g : G), ((fun (x : E) ↦ g • x) '' U ∩ U).Nonempty → g = 1
pGE : ∀ (g : G) (e : E), f (g • e) = f e
⊢ f ⁻¹' f '' U = ⋃ (g : G), (fun (x : E) ↦ g • x) ⁻¹' U

Tactic:
have preim_im : f ⁻¹' f '' U = ⋃ g : G, (g • ·) ⁻¹' U := by
    ext e; refine ⟨fun ⟨e', heU, he⟩ ↦ ?_, ?_⟩
    · obtain ⟨g, rfl⟩ := hfG.mp he; exact ⟨_, ⟨g, rfl⟩, heU⟩
    · intro ⟨_, ⟨g, rfl⟩, hg⟩; exact ⟨_, hg, pGE g e⟩