awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
preim_im : f ⁻¹' f '' U = ⋃ (g : G), (fun (x : E) ↦ g • x) ⁻¹' U
this : Nonempty (X → E)
g : G
e : E
hU : e ∈ U
⊢ Membership.mem (γ := Set E) ((fun (g : G) ↦ ((fun (x : E) ↦ g • x) ⁻¹' U : Set E)) g) (g⁻¹ • e)

Tactic:
apply (smul_inv_smul g e).symm ▸ hU
-- 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
preim_im : f ⁻¹' f '' U = ⋃ (g : G), (fun (x : E) ↦ g • x) ⁻¹' U
this : Nonempty (X → E)
g : G
e : E
hU : e ∈ U
⊢ f e ∈ f '' (fun (g : G) ↦ ((fun (x : E) ↦ g • x) ⁻¹' U : Set E)) g

Tactic:
exact ⟨g⁻¹ • e, by apply (smul_inv_smul g e).symm ▸ hU, pGE _ 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
preim_im : f ⁻¹' f '' U = ⋃ (g : G), (fun (x : E) ↦ g • x) ⁻¹' U
this : Nonempty (X → E)
g₁ g₂ : G
hne : g₁ ≠ g₂
e : E
h :
  Membership.mem (γ := Set E)
    ((fun (g : G) ↦ ((fun (x : E) ↦ g • x) ⁻¹' U : Set E)) g₁ ⊓
      (fun (g : G) ↦ ((fun (x : E) ↦ g • x) ⁻¹' U : Set E)) g₂)
    e
h₁ : Membership.mem (γ := Set E) ((fun (g : G) ↦ ((fun (x : E) ↦ g • x) ⁻¹' U : Set E)) g₁) e
h₂ : Membership.mem (γ := Set E) ((fun (g : G) ↦ ((fun (x : E) ↦ g • x) ⁻¹' U : Set E)) g₂) e
refine_5 refine_5₁ : (g₁ * g₂⁻¹) • g₂ • e = g₁ • e
refine_5₂ : g₁ • g₂⁻¹ • g₂ • e = g₁ • e
⊢ Eq.{u_1 + 1} (α := E) ((fun (x : E) ↦ (g₁ * g₂⁻¹) • x) ((fun (x : E) ↦ g₂ • x) e)) ((fun (x : E) ↦ g₁ • x) e)

Tactic:
simp_rw [mul_smul, inv_smul_smul]

Premises used: inv_smul_smul, 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
hf : IsQuotientMap f
inst_4 : ContinuousConstSMul G E
hfG : ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ MulAction.orbit G e₂
disjoint : ∀ (e : E), ∃ U ∈ 𝓝 e, ∀ (g : G), ((fun (x : E) ↦ g • x) '' U ∩ U).Nonempty → g • e = e
this : TopologicalSpace G := ⊥
⊢ DiscreteTopology G

Tactic:
have : DiscreteTopology 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₂
disjoint : ∀ (e : E), ∃ U ∈ 𝓝 e, ∀ (g : G), ((fun (x : E) ↦ g • x) '' U ∩ U).Nonempty → g • e = e
this_1 : TopologicalSpace G := ⊥
this_2 : DiscreteTopology G
this : ∀ x ∈ f '' {e : E | Eq (α := Subgroup G) (MulAction.stabilizer G e) ⊥}, ∃ (t : Trivialization G f), x ∈ t.baseSet
choose :
  ∀ (t : (x : X) → x ∈ f '' {e : E | Eq (α := Subgroup G) (MulAction.stabilizer G e) ⊥} → Trivialization G f)
    (ht : ∀ (x : X) (a : x ∈ f '' {e : E | Eq (α := Subgroup G) (MulAction.stabilizer G e) ⊥}), x ∈ (t x a).baseSet),
    IsCoveringMapOn f (f '' {e : E | Eq (α := Subgroup G) (MulAction.stabilizer G e) ⊥})
⊢ IsCoveringMapOn f (f '' {e : E | Eq (α := Subgroup G) (MulAction.stabilizer G e) ⊥})

Tactic:
choose t ht using this
-- 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₂
disjoint : ∀ (e : E), ∃ U ∈ 𝓝 e, ∀ (g : G), ((fun (x : E) ↦ g • x) '' U ∩ U).Nonempty → g • e = e
this_1 : TopologicalSpace G := ⊥
this : DiscreteTopology G
t : (x : X) → x ∈ f '' {e : E | Eq (α := Subgroup G) (MulAction.stabilizer G e) ⊥} → Trivialization G f
ht : ∀ (x : X) (a : x ∈ f '' {e : E | Eq (α := Subgroup G) (MulAction.stabilizer G e) ⊥}), x ∈ (t x a).baseSet
⊢ IsCoveringMapOn f (f '' {e : E | Eq (α := Subgroup G) (MulAction.stabilizer G e) ⊥})

Tactic:
IsCoveringMapOn.mk _ _ _ _ fun x ↦ ht x x.2

Premises used: IsCoveringMapOn.mk, Subtype.val, Subtype.property
-- 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₂
disjoint : ∀ (e : E), ∃ U ∈ 𝓝 e, ∀ (g : G), ((fun (x : E) ↦ g • x) '' U ∩ U).Nonempty → g • e = e
this_1 : TopologicalSpace G := ⊥
this : DiscreteTopology G
t : (x : X) → x ∈ f '' {e : E | Eq (α := Subgroup G) (MulAction.stabilizer G e) ⊥} → Trivialization G f
ht : ∀ (x : X) (a : x ∈ f '' {e : E | Eq (α := Subgroup G) (MulAction.stabilizer G e) ⊥}), x ∈ (t x a).baseSet
⊢ IsCoveringMapOn f (f '' {e : E | Eq (α := Subgroup G) (MulAction.stabilizer G e) ⊥})

Tactic:
exact IsCoveringMapOn.mk _ _ _ _ fun x ↦ ht x x.2

Premises used: IsCoveringMapOn.mk
-- 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₂
disjoint : ∀ (e : E), ∃ U ∈ 𝓝 e, ∀ (g : G), ((fun (x : E) ↦ g • x) '' U ∩ U).Nonempty → g • e = e
this_1 : TopologicalSpace G := ⊥
this : DiscreteTopology G
suffices :
  ∀ x ∈ f '' {e : E | Eq (α := Subgroup G) (MulAction.stabilizer G e) ⊥}, ∃ (t : Trivialization G f), x ∈ t.baseSet
⊢ IsCoveringMapOn f (f '' {e : E | Eq (α := Subgroup G) (MulAction.stabilizer G e) ⊥})

Tactic:
suffices ∀ x ∈ f '' {e | MulAction.stabilizer G e = ⊥}, ∃ t : Trivialization G f, x ∈ t.baseSet by
    choose t ht using this; exact IsCoveringMapOn.mk _ _ _ _ fun x ↦ ht x x.2
-- 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₂
disjoint : ∀ (e : E), ∃ U ∈ 𝓝 e, ∀ (g : G), ((fun (x : E) ↦ g • x) '' U ∩ U).Nonempty → g • e = e
this_1 : TopologicalSpace G := ⊥
this : DiscreteTopology G
e : E
he : Membership.mem (γ := Set E) {e : E | Eq (α := Subgroup G) (MulAction.stabilizer G e) ⊥} e
have :
  ∀ (U : Set E) (heU : U ∈ 𝓝 e) (hU : ∀ (g : G), ((fun (x : E) ↦ g • x) '' U ∩ U).Nonempty → g • e = e),
    ∃ (t : Trivialization G f), f e ∈ t.baseSet
⊢ ∃ (t : Trivialization G f), f e ∈ t.baseSet

Tactic:
have ⟨U, heU, hU⟩ := 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
hf : IsQuotientMap f
inst_4 : ContinuousConstSMul G E
hfG : ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ MulAction.orbit G e₂
disjoint : ∀ (e : E), ∃ U ∈ 𝓝 e, ∀ (g : G), ((fun (x : E) ↦ g • x) '' U ∩ U).Nonempty → g • e = e
this_1 : TopologicalSpace G := ⊥
this : DiscreteTopology G
e : E
he : Membership.mem (γ := Set E) {e : E | Eq (α := Subgroup G) (MulAction.stabilizer G e) ⊥} e
U : Set E
heU : U ∈ 𝓝 e
hU : ∀ (g : G), ((fun (x : E) ↦ g • x) '' U ∩ U).Nonempty → g • e = e
⊢ ∃ (t : Trivialization G f), f e ∈ t.baseSet

Tactic:
⟨hf.trivializationOfSMulDisjoint hfG (interior U) isOpen_interior
    fun g hg ↦ ?_, e, mem_interior_iff_mem_nhds.mpr heU, rfl⟩

Premises used: Iff.mpr, mem_interior_iff_mem_nhds, isOpen_interior, And.intro, interior, Exists.intro, Topology.IsQuotientMap.trivializationOfSMulDisjoint, 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₂
disjoint : ∀ (e : E), ∃ U ∈ 𝓝 e, ∀ (g : G), ((fun (x : E) ↦ g • x) '' U ∩ U).Nonempty → g • e = e
this_1 : TopologicalSpace G := ⊥
this : DiscreteTopology G
e : E
he : Membership.mem (γ := Set E) {e : E | Eq (α := Subgroup G) (MulAction.stabilizer G e) ⊥} e
U : Set E
heU : U ∈ 𝓝 e
hU : ∀ (g : G), ((fun (x : E) ↦ g • x) '' U ∩ U).Nonempty → g • e = e
refine : ∀ (g : G) (hg : ((fun (x : E) ↦ g • x) '' interior U ∩ interior U).Nonempty), g = 1
⊢ ∃ (t : Trivialization G f), f e ∈ t.baseSet

Tactic:
refine ⟨hf.trivializationOfSMulDisjoint hfG (interior U) isOpen_interior
    fun g hg ↦ ?_, e, mem_interior_iff_mem_nhds.mpr heU, 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₂
disjoint : ∀ (e : E), ∃ U ∈ 𝓝 e, ∀ (g : G), ((fun (x : E) ↦ g • x) '' U ∩ U).Nonempty → g • e = e
this_1 : TopologicalSpace G := ⊥
this : DiscreteTopology G
e : E
he : Membership.mem (γ := Set E) {e : E | Eq (α := Subgroup G) (MulAction.stabilizer G e) ⊥} e
U : Set E
heU : U ∈ 𝓝 e
hU : ∀ (g : G), ((fun (x : E) ↦ g • x) '' U ∩ U).Nonempty → g • e = e
g : G
hg : ((fun (x : E) ↦ g • x) '' interior U ∩ interior U).Nonempty
rw : Membership.mem (γ := Subgroup G) (MulAction.stabilizer G e) g
⊢ g = 1

Tactic:
rw [← Subgroup.mem_bot, ← he]

Premises used: Subgroup.mem_bot
-- 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₂
disjoint : ∀ (e : E), ∃ U ∈ 𝓝 e, ∀ (g : G), ((fun (x : E) ↦ g • x) '' U ∩ U).Nonempty → g • e = e
this_1 : TopologicalSpace G := ⊥
this : DiscreteTopology G
e : E
he : Membership.mem (γ := Set E) {e : E | Eq (α := Subgroup G) (MulAction.stabilizer G e) ⊥} e
U : Set E
heU : U ∈ 𝓝 e
hU : ∀ (g : G), ((fun (x : E) ↦ g • x) '' U ∩ U).Nonempty → g • e = e
g : G
hg : ((fun (x : E) ↦ g • x) '' interior U ∩ interior U).Nonempty
grw grw₁ : (fun (x : E) ↦ g • x) '' U ∩ U ⊆ (fun (x : E) ↦ g • x) '' U ∩ U
⊢ (fun (x : E) ↦ g • x) '' interior U ∩ interior U ⊆ (fun (x : E) ↦ g • x) '' U ∩ U

Tactic:
grw [interior_subset]

Premises used: interior_subset
-- 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₂
disjoint : ∀ (e : E), ∃ U ∈ 𝓝 e, ∀ (g : G), ((fun (x : E) ↦ g • x) '' U ∩ U).Nonempty → g • e = e
this_1 : TopologicalSpace G := ⊥
this : DiscreteTopology G
e : E
he : Membership.mem (γ := Set E) {e : E | Eq (α := Subgroup G) (MulAction.stabilizer G e) ⊥} e
U : Set E
heU : U ∈ 𝓝 e
hU : ∀ (g : G), ((fun (x : E) ↦ g • x) '' U ∩ U).Nonempty → g • e = e
g : G
hg : ((fun (x : E) ↦ g • x) '' interior U ∩ interior U).Nonempty
⊢ Membership.mem (γ := Subgroup G) (MulAction.stabilizer G e) g

Tactic:
exact hU _ (hg.mono (by grw [interior_subset]))

Premises used: Set.Nonempty.mono
-- 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 : ProperlyDiscontinuousSMul G E
inst_6 : LocallyCompactSpace E
inst_7 : T2Space E
⊢ IsCoveringMapOn f (f '' {e : E | Eq (α := Subgroup G) (MulAction.stabilizer G e) ⊥})

Tactic:
hf.isCoveringMapOn_of_smul_disjoint hfG
    (ProperlyDiscontinuousSMul.exists_nhds_image_smul_eq_self G)

Premises used: ProperlyDiscontinuousSMul.exists_nhds_image_smul_eq_self, Topology.IsQuotientMap.isCoveringMapOn_of_smul_disjoint
-- Module: Mathlib.Topology.Covering.Quotient
Goal:
E : Type u_1
inst : TopologicalSpace E
G : Type u_3
inst_1 : Group G
inst_2 : MulAction G E
inst_3 : ContinuousConstSMul G E
inst_4 : ProperlyDiscontinuousSMul G E
inst_5 : LocallyCompactSpace E
inst_6 : T2Space E
⊢ IsCoveringMapOn (Quotient.mk (MulAction.orbitRel G E))
    (Quotient.mk (MulAction.orbitRel G E) '' {e : E | Eq (α := Subgroup G) (MulAction.stabilizer G e) ⊥})

Tactic:
isQuotientMap_quotient_mk'.isCoveringMapOn_of_properlyDiscontinuousSMul Quotient.eq''

Premises used: isQuotientMap_quotient_mk', Quotient.eq'', Topology.IsQuotientMap.isCoveringMapOn_of_properlyDiscontinuousSMul, Quotient.mk'
-- Module: Mathlib.Topology.Covering.Quotient
Goal:
E : Type u_1
inst : TopologicalSpace E
G : Type u_3
inst_1 : Group G
inst_2 : MulAction G E
inst_3 : ContinuousConstSMul G E
inst_4 : ProperlyDiscontinuousSMul G E
inst_5 : LocallyCompactSpace E
inst_6 : T2Space E
inst_7 : IsCancelSMul G E
⊢ IsQuotientCoveringMap (Quotient.mk (MulAction.orbitRel G E)) G

Tactic:
isQuotientMap_quotient_mk'.isQuotientCoveringMap_of_properlyDiscontinuousSMul Quotient.eq''

Premises used: isQuotientMap_quotient_mk', Quotient.eq'', Quotient.mk', Topology.IsQuotientMap.isQuotientCoveringMap_of_properlyDiscontinuousSMul
-- Module: Mathlib.Topology.Covering.Quotient
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
hf : IsQuotientMap f
inst_2 : Group E
inst_3 : IsTopologicalGroup E
G : Subgroup E
hG : IsDiscrete (↑G : Set E)
hfG : ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₂ * e₁⁻¹ ∈ G
e : E
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 1) U
left : U⁻¹ = U
disj : ∀ g ∈ G, ((fun (x : E) ↦ g * x) '' U ∩ U).Nonempty → g = 1
s : ↥G
hs : ((fun (x : E) ↦ s • x) '' (U * {e}) ∩ (U * {e})).Nonempty
obtain :
  ∀ (x : E) (hx : x ∈ U) (y : E) (hy : y ∈ U) (g : E)
    (he :
      Eq.{u_1 + 1} (α := E) ((fun (x1 x2 : E) ↦ x1 * x2) y g)
        ((fun (x : E) ↦ s • x) ((fun (x1 x2 : E) ↦ x1 * x2) x g))),
    ((fun (x : E) ↦ (↑s : E) * x) '' U ∩ U).Nonempty
⊢ ((fun (x : E) ↦ (↑s : E) * x) '' U ∩ U).Nonempty

Tactic:
obtain ⟨_, ⟨_, ⟨x, hx, _, rfl, rfl⟩, rfl⟩, y, hy, g, rfl, he⟩ := hs

Premises used: 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
hf : IsQuotientMap f
inst_2 : Group E
inst_3 : IsTopologicalGroup E
G : Subgroup E
hG : IsDiscrete (↑G : Set E)
hfG : ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₂ * e₁⁻¹ ∈ G
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 1) U
left : U⁻¹ = U
disj : ∀ g ∈ G, ((fun (x : E) ↦ g * x) '' U ∩ U).Nonempty → g = 1
s : ↥G
x : E
hx : x ∈ U
y : E
hy : y ∈ U
g : E
he : Eq.{u_1 + 1} (α := E) ((fun (x1 x2 : E) ↦ x1 * x2) y g) ((fun (x : E) ↦ s • x) ((fun (x1 x2 : E) ↦ x1 * x2) x g))
⊢ ((fun (x : E) ↦ (↑s : E) * x) '' U ∩ U).Nonempty

Tactic:
⟨y, ⟨x, hx, mul_right_cancel ((mul_assoc ..).trans he.symm)⟩, hy⟩

Premises used: mul_assoc, Set.Nonempty, And.intro, Exists.intro, mul_right_cancel, Eq.symm, Eq.trans
-- Module: Mathlib.Topology.Covering.Quotient
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
hf : IsQuotientMap f
inst_2 : Group E
inst_3 : IsTopologicalGroup E
G : Subgroup E
hG : IsDiscrete (↑G : Set E)
hfG : ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₂ * e₁⁻¹ ∈ G
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 1) U
left : U⁻¹ = U
disj : ∀ g ∈ G, ((fun (x : E) ↦ g * x) '' U ∩ U).Nonempty → g = 1
s : ↥G
x : E
hx : x ∈ U
y : E
hy : y ∈ U
g : E
he : Eq.{u_1 + 1} (α := E) ((fun (x1 x2 : E) ↦ x1 * x2) y g) ((fun (x : E) ↦ s • x) ((fun (x1 x2 : E) ↦ x1 * x2) x g))
⊢ ((fun (x : E) ↦ (↑s : E) * x) '' U ∩ U).Nonempty

Tactic:
exact ⟨y, ⟨x, hx, mul_right_cancel ((mul_assoc ..).trans he.symm)⟩, hy⟩
-- Module: Mathlib.Topology.Covering.Quotient
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
hf : IsQuotientMap f
inst_2 : Group E
inst_3 : IsTopologicalGroup E
G : Subgroup E
hG : IsDiscrete (↑G : Set E)
hfG : ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁⁻¹ * e₂ ∈ G
e : E
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 1) U
left : U⁻¹ = U
disj : ∀ g ∈ G, ((fun (x : E) ↦ x * g) '' U ∩ U).Nonempty → g = 1
x : ↥G.op
s : E
hS : { unop' := s : PreOpposite E } ∈ G.op
hs :
  ((fun (x : E) ↦ Subtype.mk (p := fun (x : Eᵐᵒᵖ) ↦ x ∈ G.op) { unop' := s : PreOpposite E } hS • x) '' ({e} * U) ∩
      ({e} * U)).Nonempty
obtain :
  ∀ (x : E) (hx : x ∈ U) (g y : E) (hy : y ∈ U)
    (he :
      Eq.{u_1 + 1} (α := E) ((fun (x1 x2 : E) ↦ x1 * x2) g y)
        ((fun (x : E) ↦ Subtype.mk (p := fun (x : Eᵐᵒᵖ) ↦ x ∈ G.op) { unop' := s : PreOpposite E } hS • x)
          ((fun (x1 x2 : E) ↦ x1 * x2) g x))),
    ((fun (x : E) ↦
            x *
              MulOpposite.unop
                (↑(Subtype.mk (p := fun (x : Eᵐᵒᵖ) ↦ x ∈ G.op) { unop' := s : PreOpposite E } hS) : Eᵐᵒᵖ)) ''
          U ∩
        U).Nonempty
⊢ ((fun (x : E) ↦
          x *
            MulOpposite.unop
              (↑(Subtype.mk (p := fun (x : Eᵐᵒᵖ) ↦ x ∈ G.op) { unop' := s : PreOpposite E } hS) : Eᵐᵒᵖ)) ''
        U ∩
      U).Nonempty

Tactic:
obtain ⟨_, ⟨_, ⟨_, rfl, x, hx, rfl⟩, rfl⟩, g, rfl, y, hy, he⟩ := hs

Premises used: 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
hf : IsQuotientMap f
inst_2 : Group E
inst_3 : IsTopologicalGroup E
G : Subgroup E
hG : IsDiscrete (↑G : Set E)
hfG : ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁⁻¹ * e₂ ∈ G
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 1) U
left : U⁻¹ = U
disj : ∀ g ∈ G, ((fun (x : E) ↦ x * g) '' U ∩ U).Nonempty → g = 1
x_1 : ↥G.op
s : E
hS : { unop' := s : PreOpposite E } ∈ G.op
x : E
hx : x ∈ U
g y : E
hy : y ∈ U
he :
  Eq.{u_1 + 1} (α := E) ((fun (x1 x2 : E) ↦ x1 * x2) g y)
    ((fun (x : E) ↦ Subtype.mk (p := fun (x : Eᵐᵒᵖ) ↦ x ∈ G.op) { unop' := s : PreOpposite E } hS • x)
      ((fun (x1 x2 : E) ↦ x1 * x2) g x))
⊢ ((fun (x : E) ↦
          x *
            MulOpposite.unop
              (↑(Subtype.mk (p := fun (x : Eᵐᵒᵖ) ↦ x ∈ G.op) { unop' := s : PreOpposite E } hS) : Eᵐᵒᵖ)) ''
        U ∩
      U).Nonempty

Tactic:
⟨y, ⟨x, hx, mul_left_cancel (he.trans <| mul_assoc ..).symm⟩, hy⟩

Premises used: mul_assoc, mul_left_cancel, Set.Nonempty, And.intro, Exists.intro, Eq.symm, Eq.trans
-- Module: Mathlib.Topology.Covering.Quotient
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
hf : IsQuotientMap f
inst_2 : Group E
inst_3 : IsTopologicalGroup E
G : Subgroup E
hG : IsDiscrete (↑G : Set E)
hfG : ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁⁻¹ * e₂ ∈ G
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 1) U
left : U⁻¹ = U
disj : ∀ g ∈ G, ((fun (x : E) ↦ x * g) '' U ∩ U).Nonempty → g = 1
x_1 : ↥G.op
s : E
hS : { unop' := s : PreOpposite E } ∈ G.op
x : E
hx : x ∈ U
g y : E
hy : y ∈ U
he :
  Eq.{u_1 + 1} (α := E) ((fun (x1 x2 : E) ↦ x1 * x2) g y)
    ((fun (x : E) ↦ Subtype.mk (p := fun (x : Eᵐᵒᵖ) ↦ x ∈ G.op) { unop' := s : PreOpposite E } hS • x)
      ((fun (x1 x2 : E) ↦ x1 * x2) g x))
⊢ ((fun (x : E) ↦
          x *
            MulOpposite.unop
              (↑(Subtype.mk (p := fun (x : Eᵐᵒᵖ) ↦ x ∈ G.op) { unop' := s : PreOpposite E } hS) : Eᵐᵒᵖ)) ''
        U ∩
      U).Nonempty

Tactic:
exact ⟨y, ⟨x, hx, mul_left_cancel (he.trans <| mul_assoc ..).symm⟩, hy⟩
-- Module: Mathlib.Topology.Covering.Quotient
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
inst_2 : Group E
inst_3 : IsTopologicalGroup E
inst_4 : Group X
f : E →* X
hf : IsQuotientMap.{u_1, u_2} (X := E) (Y := X) (⇑f : (a : E) → X)
disc : IsDiscrete (↑f.ker : Set E)
x x_1 : E
rw : Eq.{u_2 + 1} (α := X) ((f : (a : E) → X) (x_1 * x⁻¹) : X) (1 : X) ↔ x_1 * x⁻¹ ∈ f.ker
⊢ Eq.{u_2 + 1} (α := X) ((f : (a : E) → X) x : X) ((f : (a : E) → X) x_1 : X) ↔ x_1 * x⁻¹ ∈ f.ker

Tactic:
rw [eq_comm, ← mul_inv_eq_one, ← map_inv, ← map_mul]

Premises used: map_inv, mul_inv_eq_one, eq_comm, map_mul
-- Module: Mathlib.Topology.Covering.Quotient
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
inst_2 : Group E
inst_3 : IsTopologicalGroup E
inst_4 : Group X
f : E →* X
hf : IsQuotientMap.{u_1, u_2} (X := E) (Y := X) (⇑f : (a : E) → X)
disc : IsDiscrete (↑f.ker : Set E)
x x_1 : E
⊢ Eq.{u_2 + 1} (α := X) ((f : (a : E) → X) (x_1 * x⁻¹) : X) (1 : X) ↔ x_1 * x⁻¹ ∈ f.ker

Tactic:
rfl
-- Module: Mathlib.Topology.Covering.Quotient
Goal:
G : Type u_4
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
S : Subgroup G
hS : IsDiscrete (↑S : Set G)
⊢ IsQuotientCoveringMap.{u_4, u_4, u_4} (E := G) (X := G ⧸ S) QuotientGroup.mk ↥S.op

Tactic:
isQuotientMap_quotient_mk'.isQuotientCoveringMap_of_subgroupOp S hS <|
    Quotient.eq''.trans QuotientGroup.leftRel_apply

Premises used: isQuotientMap_quotient_mk', Quotient.eq'', Topology.IsQuotientMap.isQuotientCoveringMap_of_subgroupOp, Quotient.mk', Iff.trans, QuotientGroup.leftRel_apply
-- Module: Mathlib.Topology.Covering.Quotient
Goal:
G : Type u_4
inst : CommGroup G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
S : Subgroup G
hS : IsDiscrete (↑S : Set G)
e₁ e₂ : G
rw rw₁ : e₂ * e₁⁻¹ ∈ S ↔ e₂ * e₁⁻¹ ∈ S
⊢ e₁⁻¹ * e₂ ∈ S ↔ e₂ * e₁⁻¹ ∈ S

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- 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
⊢ ContinuousConstSMul G E

Tactic:
have := h.toContinuousConstSMul
-- 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
this : ContinuousConstSMul G E
⊢ IsCoveringMapOn f (f '' {e : E | Eq (α := Subgroup G) (MulAction.stabilizer G e) ⊥})

Tactic:
h.isCoveringMapOn_of_smul_disjoint h.apply_eq_iff_mem_orbit fun e ↦ ?_

Premises used: IsQuotientCoveringMap.apply_eq_iff_mem_orbit, Topology.IsQuotientMap.isCoveringMapOn_of_smul_disjoint, IsQuotientCoveringMap.toIsQuotientMap
-- 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
this : ContinuousConstSMul G E
h₁ : f '' {e : E | Eq (α := Subgroup G) (MulAction.stabilizer G e) ⊥} = Set.univ
convert! : ∀ (e : E), ∃ U ∈ 𝓝 e, ∀ (g : G), ((fun (x : E) ↦ g • x) '' U ∩ U).Nonempty → g • e = e
⊢ IsCoveringMapOn f Set.univ

Tactic:
convert! ← h.isCoveringMapOn_of_smul_disjoint h.apply_eq_iff_mem_orbit fun e ↦ ?_

Premises used: IsQuotientCoveringMap.apply_eq_iff_mem_orbit, Topology.IsQuotientMap.isCoveringMapOn_of_smul_disjoint, IsQuotientCoveringMap.toIsQuotientMap