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
⊢ Nonempty (X → E)

Tactic:
have : Nonempty (X → E) := ⟨Function.surjInv hf.surjective⟩
-- 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)
refine_1 : IsOpen[inst_1] (f '' U)
refine_2 :
  ∀ (g : G) (W : Set X) (hWU : W ⊆ f '' U)
    (isOpen : IsOpen[inst] (f ⁻¹' W ∩ (fun (g : G) ↦ ((fun (x : E) ↦ g • x) ⁻¹' U : Set E)) g)), IsOpen[inst] (f ⁻¹' W)
refine_3 :
  ∀ (g : G) (e₁ : E) (h₁ : Membership.mem (γ := Set E) ((fun (g : G) ↦ ((fun (x : E) ↦ g • x) ⁻¹' U : Set E)) g) e₁)
    (e₂ : E) (h₂ : Membership.mem (γ := Set E) ((fun (g : G) ↦ ((fun (x : E) ↦ g • x) ⁻¹' U : Set E)) g) e₂)
    (he : f e₁ = f e₂), e₁ = e₂
refine_4 : ∀ (i : G), Set.SurjOn f ((fun (g : G) ↦ ((fun (x : E) ↦ g • x) ⁻¹' U : Set E)) i) (f '' U)
refine_5 :
  ∀ {g₁ g₂ : G} (hne : g₁ ≠ g₂) (e : E),
    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),
        Eq.{u_1 + 1} (α := E) ((fun (x : E) ↦ (g₁ * g₂⁻¹) • x) ((fun (x : E) ↦ g₂ • x) e)) ((fun (x : E) ↦ g₁ • x) e)
⊢ Trivialization G f

Tactic:
refine IsOpen.trivializationDiscrete (fun g ↦ (g • ·) ⁻¹' U) (f '' U)
    ?_ (fun g W hWU ↦ ⟨fun hoW ↦ (hoW.preimage hf.continuous).inter (open_U.preimage <|
      continuous_const_smul g), fun isOpen ↦ hf.isOpen_preimage.mp ?_⟩) (fun g e₁ h₁ e₂ h₂ he ↦ ?_)
    ?_ (fun {g₁ g₂} hne ↦ disjoint_iff_inf_le.mpr fun e ⟨h₁, h₂⟩ ↦ hne <|
      mul_inv_eq_one.mp (disjoint _ ⟨_, ⟨_, h₂, ?_⟩, h₁⟩)) preim_im.subset

Premises used: Iff.mpr, Topology.IsQuotientMap.trivializationOfSMulDisjoint.match_3, ContinuousConstSMul.continuous_const_smul, HMul.hMul, mul_inv_eq_one, IsOpen.trivializationDiscrete, Membership.mem, Bot.bot, Topology.IsCoinducing.isOpen_preimage, Eq.subset, Inv.inv, Set.preimage, Topology.IsQuotientMap.continuous, And.intro, IsOpen.inter, Iff.intro, Topology.IsQuotientMap.isCoinducing, Exists.intro, Iff.mp, Set.image, HSMul.hSMul, disjoint_iff_inf_le, IsOpen.preimage
-- 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)
refine_1 : IsOpen[inst] (⋃ (g : G), (fun (x : E) ↦ g • x) ⁻¹' U)
⊢ IsOpen[inst_1] (f '' U)

Tactic:
rw [← hf.isOpen_preimage, preim_im]

Premises used: Topology.IsCoinducing.isOpen_preimage, Topology.IsQuotientMap.isCoinducing
-- 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)
⊢ IsOpen[inst] (⋃ (g : G), (fun (x : E) ↦ g • x) ⁻¹' U)

Tactic:
isOpen_iUnion fun g ↦ open_U.preimage (continuous_const_smul g)

Premises used: ContinuousConstSMul.continuous_const_smul, isOpen_iUnion, IsOpen.preimage
-- 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)
⊢ IsOpen[inst] (⋃ (g : G), (fun (x : E) ↦ g • x) ⁻¹' U)

Tactic:
exact isOpen_iUnion fun g ↦ open_U.preimage (continuous_const_smul g)

Premises used: ContinuousConstSMul.continuous_const_smul, isOpen_iUnion, IsOpen.preimage
-- 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
W : Set X
hWU : W ⊆ f '' U
isOpen : IsOpen[inst] (f ⁻¹' W ∩ (fun (g : G) ↦ ((fun (x : E) ↦ g • x) ⁻¹' U : Set E)) g)
⊢ IsOpen[inst]
    (⋃ (i : G), (fun (x : E) ↦ i • x) ⁻¹' (f ⁻¹' W ∩ (fun (g : G) ↦ ((fun (x : E) ↦ g • x) ⁻¹' U : Set E)) g))

Tactic:
isOpen_iUnion fun g : G ↦ isOpen.preimage (continuous_const_smul g)

Premises used: ContinuousConstSMul.continuous_const_smul, isOpen_iUnion, IsOpen.preimage
-- 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
W : Set X
hWU : W ⊆ f '' U
isOpen : IsOpen[inst] (f ⁻¹' W ∩ (fun (g : G) ↦ ((fun (x : E) ↦ g • x) ⁻¹' U : Set E)) g)
h : f ⁻¹' W = ⋃ (i : G), (fun (x : E) ↦ i • x) ⁻¹' (f ⁻¹' W ∩ (fun (g : G) ↦ ((fun (x : E) ↦ g • x) ⁻¹' U : Set E)) g)
⊢ IsOpen[inst] (f ⁻¹' W)

Tactic:
convert! isOpen_iUnion fun g : G ↦ isOpen.preimage (continuous_const_smul g)

Premises used: ContinuousConstSMul.continuous_const_smul, isOpen_iUnion, IsOpen.preimage
-- 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
W : Set X
hWU : W ⊆ f '' U
isOpen : IsOpen[inst] (f ⁻¹' W ∩ (fun (g : G) ↦ ((fun (x : E) ↦ g • x) ⁻¹' U : Set E)) g)
h :
  ∀ (e : E),
    e ∈ f ⁻¹' W ↔
      Membership.mem (γ := Set E)
        (⋃ (i : G), (fun (x : E) ↦ i • x) ⁻¹' (f ⁻¹' W ∩ (fun (g : G) ↦ ((fun (x : E) ↦ g • x) ⁻¹' U : Set E)) g)) e
⊢ f ⁻¹' W = ⋃ (i : G), (fun (x : E) ↦ i • x) ⁻¹' (f ⁻¹' W ∩ (fun (g : G) ↦ ((fun (x : E) ↦ g • x) ⁻¹' U : Set E)) g)

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
preim_im : f ⁻¹' f '' U = ⋃ (g : G), (fun (x : E) ↦ g • x) ⁻¹' U
this : Nonempty (X → E)
g : G
W : Set X
hWU : W ⊆ f '' U
isOpen : IsOpen[inst] (f ⁻¹' W ∩ (fun (g : G) ↦ ((fun (x : E) ↦ g • x) ⁻¹' U : Set E)) g)
e : E
⊢ e ∈ f ⁻¹' W ↔
    Membership.mem (γ := Set E)
      (⋃ (i : G), (fun (x : E) ↦ i • x) ⁻¹' (f ⁻¹' W ∩ (fun (g : G) ↦ ((fun (x : E) ↦ g • x) ⁻¹' U : Set E)) g)) e

Tactic:
⟨fun hW ↦ ?_, ?_⟩

Premises used: Iff.intro
-- 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
W : Set X
hWU : W ⊆ f '' U
isOpen : IsOpen[inst] (f ⁻¹' W ∩ (fun (g : G) ↦ ((fun (x : E) ↦ g • x) ⁻¹' U : Set E)) g)
e : E
h :
  ∀ (hW : e ∈ f ⁻¹' W),
    Membership.mem (γ := Set E)
      (⋃ (i : G), (fun (x : E) ↦ i • x) ⁻¹' (f ⁻¹' W ∩ (fun (g : G) ↦ ((fun (x : E) ↦ g • x) ⁻¹' U : Set E)) g)) e
h₁ :
  Membership.mem (γ := Set E)
      (⋃ (i : G), (fun (x : E) ↦ i • x) ⁻¹' (f ⁻¹' W ∩ (fun (g : G) ↦ ((fun (x : E) ↦ g • x) ⁻¹' U : Set E)) g)) e →
    e ∈ f ⁻¹' W
⊢ e ∈ f ⁻¹' W ↔
    Membership.mem (γ := Set E)
      (⋃ (i : G), (fun (x : E) ↦ i • x) ⁻¹' (f ⁻¹' W ∩ (fun (g : G) ↦ ((fun (x : E) ↦ g • x) ⁻¹' U : Set E)) g)) e

Tactic:
refine ⟨fun hW ↦ ?_, ?_⟩
-- 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
W : Set X
hWU : W ⊆ f '' U
isOpen : IsOpen[inst] (f ⁻¹' W ∩ (fun (g : G) ↦ ((fun (x : E) ↦ g • x) ⁻¹' U : Set E)) g)
e : E
hW : e ∈ f ⁻¹' W
h :
  ∀ (e' : E) (he' : e' ∈ U) (hfe : f e' = f e),
    Membership.mem (γ := Set E)
      (⋃ (i : G), (fun (x : E) ↦ i • x) ⁻¹' (f ⁻¹' W ∩ (fun (g : G) ↦ ((fun (x : E) ↦ g • x) ⁻¹' U : Set E)) g)) e
⊢ Membership.mem (γ := Set E)
    (⋃ (i : G), (fun (x : E) ↦ i • x) ⁻¹' (f ⁻¹' W ∩ (fun (g : G) ↦ ((fun (x : E) ↦ g • x) ⁻¹' U : Set E)) g)) e

Tactic:
have ⟨e', he', hfe⟩ := hWU hW
-- 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
W : Set X
hWU : W ⊆ f '' U
isOpen : IsOpen[inst] (f ⁻¹' W ∩ (fun (g : G) ↦ ((fun (x : E) ↦ g • x) ⁻¹' U : Set E)) g)
e : E
hW : e ∈ f ⁻¹' W
e' : E
he' : e' ∈ U
hfe : f e' = f e
h :
  ∀ (g' : G) (he' : (fun (m : G) ↦ m • e) g' ∈ U) (hfe : f ((fun (m : G) ↦ m • e) g') = f e),
    Membership.mem (γ := Set E)
      (⋃ (i : G), (fun (x : E) ↦ i • x) ⁻¹' (f ⁻¹' W ∩ (fun (g : G) ↦ ((fun (x : E) ↦ g • x) ⁻¹' U : Set E)) g)) e
⊢ Membership.mem (γ := Set E)
    (⋃ (i : G), (fun (x : E) ↦ i • x) ⁻¹' (f ⁻¹' W ∩ (fun (g : G) ↦ ((fun (x : E) ↦ g • x) ⁻¹' U : Set E)) g)) e

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

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
preim_im : f ⁻¹' f '' U = ⋃ (g : G), (fun (x : E) ↦ g • x) ⁻¹' U
this : Nonempty (X → E)
g : G
W : Set X
hWU : W ⊆ f '' U
isOpen : IsOpen[inst] (f ⁻¹' W ∩ (fun (g : G) ↦ ((fun (x : E) ↦ g • x) ⁻¹' U : Set E)) g)
e : E
hW : e ∈ f ⁻¹' W
g' : G
he' : (fun (m : G) ↦ m • e) g' ∈ U
hfe : f ((fun (m : G) ↦ m • e) g') = f e
⊢ Membership.mem (γ := Set E)
    (⋃ (i : G), (fun (x : E) ↦ i • x) ⁻¹' (f ⁻¹' W ∩ (fun (g : G) ↦ ((fun (x : E) ↦ g • x) ⁻¹' U : Set E)) g)) e

Tactic:
⟨_, ⟨g⁻¹ * g', rfl⟩, ?_, ?_⟩

Premises used: HMul.hMul, Set.Mem, iSup, setOf, Inv.inv, 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
preim_im : f ⁻¹' f '' U = ⋃ (g : G), (fun (x : E) ↦ g • x) ⁻¹' U
this : Nonempty (X → E)
g : G
W : Set X
hWU : W ⊆ f '' U
isOpen : IsOpen[inst] (f ⁻¹' W ∩ (fun (g : G) ↦ ((fun (x : E) ↦ g • x) ⁻¹' U : Set E)) g)
e : E
hW : e ∈ f ⁻¹' W
g' : G
he' : (fun (m : G) ↦ m • e) g' ∈ U
hfe : f ((fun (m : G) ↦ m • e) g') = f e
h : (fun (x : E) ↦ (g⁻¹ * g') • x) e ∈ f ⁻¹' W
h₁ :
  Membership.mem (γ := Set E) ((fun (g : G) ↦ ((fun (x : E) ↦ g • x) ⁻¹' U : Set E)) g)
    ((fun (x : E) ↦ (g⁻¹ * g') • x) e)
⊢ Membership.mem (γ := Set E)
    (⋃ (i : G), (fun (x : E) ↦ i • x) ⁻¹' (f ⁻¹' W ∩ (fun (g : G) ↦ ((fun (x : E) ↦ g • x) ⁻¹' U : Set E)) g)) e

Tactic:
refine ⟨_, ⟨g⁻¹ * 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
preim_im : f ⁻¹' f '' U = ⋃ (g : G), (fun (x : E) ↦ g • x) ⁻¹' U
this : Nonempty (X → E)
g : G
W : Set X
hWU : W ⊆ f '' U
isOpen : IsOpen[inst] (f ⁻¹' W ∩ (fun (g : G) ↦ ((fun (x : E) ↦ g • x) ⁻¹' U : Set E)) g)
e : E
hW : e ∈ f ⁻¹' W
g' : G
he' : (fun (m : G) ↦ m • e) g' ∈ U
hfe : f ((fun (m : G) ↦ m • e) g') = f e
⊢ (fun (x : E) ↦ (g⁻¹ * g') • x) e ∈ f ⁻¹' W

Tactic:
apply Set.mem_of_eq_of_mem (pGE _ e) hW

Premises used: Set.mem_of_eq_of_mem
-- 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
W : Set X
hWU : W ⊆ f '' U
isOpen : IsOpen[inst] (f ⁻¹' W ∩ (fun (g : G) ↦ ((fun (x : E) ↦ g • x) ⁻¹' U : Set E)) g)
e : E
hW : e ∈ f ⁻¹' W
g' : G
he' : (fun (m : G) ↦ m • e) g' ∈ U
hfe : f ((fun (m : G) ↦ m • e) g') = f e
apply : Eq.{u_1 + 1} (α := E) ((fun (x : E) ↦ g • x) ((fun (x : E) ↦ (g⁻¹ * g') • x) e)) ((fun (m : G) ↦ m • e) g')
⊢ Membership.mem (γ := Set E) ((fun (g : G) ↦ ((fun (x : E) ↦ g • x) ⁻¹' U : Set E)) g)
    ((fun (x : E) ↦ (g⁻¹ * g') • x) e)

Tactic:
apply Set.mem_of_eq_of_mem _ he'

Premises used: Set.mem_of_eq_of_mem
-- 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
W : Set X
hWU : W ⊆ f '' U
isOpen : IsOpen[inst] (f ⁻¹' W ∩ (fun (g : G) ↦ ((fun (x : E) ↦ g • x) ⁻¹' U : Set E)) g)
e : E
hW : e ∈ f ⁻¹' W
g' : G
he' : (fun (m : G) ↦ m • e) g' ∈ U
hfe : f ((fun (m : G) ↦ m • e) g') = f e
simp_rw simp_rw₁ : g • (g⁻¹ * g') • e = g' • e
simp_rw₂ : g • g⁻¹ • g' • e = g' • e
⊢ Eq.{u_1 + 1} (α := E) ((fun (x : E) ↦ g • x) ((fun (x : E) ↦ (g⁻¹ * g') • x) e)) ((fun (m : G) ↦ m • e) g')

Tactic:
simp_rw [mul_smul, smul_inv_smul]

Premises used: smul_inv_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₂
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_1 : G
W : Set X
hWU : W ⊆ f '' U
isOpen : IsOpen[inst] (f ⁻¹' W ∩ (fun (g : G) ↦ ((fun (x : E) ↦ g • x) ⁻¹' U : Set E)) g_1)
e : E
g : G
hW : (fun (x : E) ↦ g • x) e ∈ f ⁻¹' W
⊢ e ∈ f ⁻¹' W

Tactic:
apply Set.mem_of_eq_of_mem (pGE _ e).symm hW

Premises used: Set.mem_of_eq_of_mem, Eq.symm
-- 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
h₁ : Membership.mem (γ := Set E) ((fun (g : G) ↦ ((fun (x : E) ↦ g • x) ⁻¹' U : Set E)) g) e₁
e₂ : E
h₂ : Membership.mem (γ := Set E) ((fun (g : G) ↦ ((fun (x : E) ↦ g • x) ⁻¹' U : Set E)) g) e₂
he : f e₁ = f e₂
⊢ f (g • e₁) = f (g • e₂)

Tactic:
rw [← pGE g, ← pGE g e₂] at 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
preim_im : f ⁻¹' f '' U = ⋃ (g : G), (fun (x : E) ↦ g • x) ⁻¹' U
this : Nonempty (X → E)
g : G
e₁ : E
h₁ : Membership.mem (γ := Set E) ((fun (g : G) ↦ ((fun (x : E) ↦ g • x) ⁻¹' U : Set E)) g) e₁
e₂ : E
h₂ : Membership.mem (γ := Set E) ((fun (g : G) ↦ ((fun (x : E) ↦ g • x) ⁻¹' U : Set E)) g) e₂
he : f (g • e₁) = f (g • e₂)
refine_3 : ∀ (g' : G) (he : (fun (m : G) ↦ m • g • e₂) g' = g • e₁), e₁ = e₂
⊢ e₁ = e₂

Tactic:
have ⟨g', he⟩ := hfG.mp 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
preim_im : f ⁻¹' f '' U = ⋃ (g : G), (fun (x : E) ↦ g • x) ⁻¹' U
this : Nonempty (X → E)
g : G
e₁ : E
h₁ : Membership.mem (γ := Set E) ((fun (g : G) ↦ ((fun (x : E) ↦ g • x) ⁻¹' U : Set E)) g) e₁
e₂ : E
h₂ : Membership.mem (γ := Set E) ((fun (g : G) ↦ ((fun (x : E) ↦ g • x) ⁻¹' U : Set E)) g) e₂
he_1 : f (g • e₁) = f (g • e₂)
g' : G
he : (fun (m : G) ↦ m • g • e₂) g' = g • e₁
refine_3 : (fun (m : G) ↦ m • g • e₂) 1 = g • e₂
⊢ e₁ = e₂

Tactic:
rw [← smul_left_cancel_iff g, ← he, disjoint g' ⟨_, ⟨_, h₂, he⟩, h₁⟩]

Premises used: And.intro, Exists.intro, smul_left_cancel_iff
-- 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
h₁ : Membership.mem (γ := Set E) ((fun (g : G) ↦ ((fun (x : E) ↦ g • x) ⁻¹' U : Set E)) g) e₁
e₂ : E
h₂ : Membership.mem (γ := Set E) ((fun (g : G) ↦ ((fun (x : E) ↦ g • x) ⁻¹' U : Set E)) g) e₂
he_1 : f (g • e₁) = f (g • e₂)
g' : G
he : (fun (m : G) ↦ m • g • e₂) g' = g • e₁
⊢ (fun (m : G) ↦ m • g • e₂) 1 = g • e₂

Tactic:
apply one_smul

Premises used: one_smul