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

Tactic:
Set.eq_univ_of_forall fun x ↦ ?_

Premises used: Set.eq_univ_of_forall
-- 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₁ : ∀ (x : X), x ∈ f '' {e : E | Eq (α := Subgroup G) (MulAction.stabilizer G e) ⊥}
⊢ f '' {e : E | Eq (α := Subgroup G) (MulAction.stabilizer G e) ⊥} = Set.univ

Tactic:
refine Set.eq_univ_of_forall fun x ↦ ?_

Premises used: Set.eq_univ_of_forall
-- 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
x : X
h₁ : ∀ (e : E), f e ∈ f '' {e : E | Eq (α := Subgroup G) (MulAction.stabilizer G e) ⊥}
⊢ x ∈ f '' {e : E | Eq (α := Subgroup G) (MulAction.stabilizer G e) ⊥}

Tactic:
obtain ⟨e, rfl⟩ := h.surjective x

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

Tactic:
have ⟨U, hU, hGU⟩ := 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
this : ContinuousConstSMul G E
e : E
U : Set E
hU : U ∈ 𝓝 e
hGU : ∀ (g : G), ((fun (x : E) ↦ g • x) '' U ∩ U).Nonempty → g = 1
⊢ e ∈ U

Tactic:
replace hU := mem_of_mem_nhds 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
h : IsQuotientCoveringMap f G
this : ContinuousConstSMul G E
e : E
U : Set E
hGU : ∀ (g : G), ((fun (x : E) ↦ g • x) '' U ∩ U).Nonempty → g = 1
hU : e ∈ U
⊢ f e ∈ f '' {e : E | Eq (α := Subgroup G) (MulAction.stabilizer G e) ⊥}

Tactic:
⟨e, (Subgroup.eq_bot_iff_forall _).mpr fun g hg ↦ hGU g (⟨e, ⟨e, hU, hg⟩, hU⟩), rfl⟩

Premises used: Iff.mpr, Set.Mem, setOf, Subgroup.eq_bot_iff_forall, And.intro, Exists.intro, Set.image, 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
h : IsQuotientCoveringMap f G
this : ContinuousConstSMul G E
e : E
U : Set E
hGU : ∀ (g : G), ((fun (x : E) ↦ g • x) '' U ∩ U).Nonempty → g = 1
hU : e ∈ U
⊢ f e ∈ f '' {e : E | Eq (α := Subgroup G) (MulAction.stabilizer G e) ⊥}

Tactic:
exact ⟨e, (Subgroup.eq_bot_iff_forall _).mpr fun g hg ↦ hGU g (⟨e, ⟨e, hU, hg⟩, hU⟩), 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
h : IsQuotientCoveringMap f G
this : ContinuousConstSMul G E
e : E
have :
  ∀ (U : Set E) (hU : U ∈ 𝓝 e) (hGU : ∀ (g : G), ((fun (x : E) ↦ g • x) '' U ∩ U).Nonempty → g = 1),
    ∃ U ∈ 𝓝 e, ∀ (g : G), ((fun (x : E) ↦ g • x) '' U ∩ U).Nonempty → g • e = e
⊢ ∃ U ∈ 𝓝 e, ∀ (g : G), ((fun (x : E) ↦ g • x) '' U ∩ U).Nonempty → g • e = e

Tactic:
have ⟨U, hU, hGU⟩ := 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
this : ContinuousConstSMul G E
e : E
U : Set E
hU : U ∈ 𝓝 e
hGU : ∀ (g : G), ((fun (x : E) ↦ g • x) '' U ∩ U).Nonempty → g = 1
g : G
hg : ((fun (x : E) ↦ g • x) '' U ∩ U).Nonempty
rw : HSMul.hSMul.{u_3, u_1, u_1} (α := G) 1 e = e
rw₁ rw₂ : e = e
⊢ g • e = e

Tactic:
rw [hGU g hg, one_smul]

Premises used: one_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
this : ContinuousConstSMul G E
e : E
U : Set E
hU : U ∈ 𝓝 e
hGU : ∀ (g : G), ((fun (x : E) ↦ g • x) '' U ∩ U).Nonempty → g = 1
⊢ ∃ U ∈ 𝓝 e, ∀ (g : G), ((fun (x : E) ↦ g • x) '' U ∩ U).Nonempty → g • e = e

Tactic:
exact ⟨U, hU, fun g hg ↦ by rw [hGU g hg, one_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 :
  IsCoveringMap f ∧
    Function.Surjective f ∧
      ContinuousConstSMul G E ∧ IsCancelSMul G E ∧ ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ MulAction.orbit G e₂
e : E
left : DiscreteTopology.{u_1} (↑(f ⁻¹' {f e}) : Type u_1)
U : Set X
heU : f e ∈ U
hU : IsOpen[inst_1] U
hfU : IsOpen[inst] (f ⁻¹' U)
H : (↑(f ⁻¹' U) : Type u_1) ≃ₜ Prod.{u_2, u_1} (↑U : Type u_2) (↑(f ⁻¹' {f e}) : Type u_1)
hH :
  ∀ (x : (↑(f ⁻¹' U) : Type u_1)),
    (↑((H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × (↑(f ⁻¹' {f e}) : Type u_1)) x).1 : X) = f (↑x : E)
⊢ Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceSubtype]
    (Function.comp (β := Prod.{u_2, u_1} (↑U : Type u_2) (↑(f ⁻¹' {f e}) : Type u_1)) Prod.snd
      (⇑H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × (↑(f ⁻¹' {f e}) : Type u_1)))

Tactic:
fun_prop
-- 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 :
  IsCoveringMap f ∧
    Function.Surjective f ∧
      ContinuousConstSMul G E ∧ IsCancelSMul G E ∧ ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ MulAction.orbit G e₂
e : E
left : DiscreteTopology.{u_1} (↑(f ⁻¹' {f e}) : Type u_1)
U : Set X
heU : f e ∈ U
hU : IsOpen[inst_1] U
hfU : IsOpen[inst] (f ⁻¹' U)
H : (↑(f ⁻¹' U) : Type u_1) ≃ₜ Prod.{u_2, u_1} (↑U : Type u_2) (↑(f ⁻¹' {f e}) : Type u_1)
hH :
  ∀ (x : (↑(f ⁻¹' U) : Type u_1)),
    (↑((H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × (↑(f ⁻¹' {f e}) : Type u_1)) x).1 : X) = f (↑x : E)
g : G
x : { x : E // x ∈ f ⁻¹' U }
hx :
  Membership.mem (γ := Set { x : E // x ∈ f ⁻¹' U })
    (Set.preimage (β := (↑(f ⁻¹' {f e}) : Type u_1))
      (Function.comp (β := Prod.{u_2, u_1} (↑U : Type u_2) (↑(f ⁻¹' {f e}) : Type u_1)) Prod.snd
        (⇑H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × (↑(f ⁻¹' {f e}) : Type u_1)))
      {((H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × (↑(f ⁻¹' {f e}) : Type u_1))
            (Subtype.mk (p := fun (x : E) ↦ x ∈ f ⁻¹' U) e heU)).2})
    x
y : { x : E // x ∈ f ⁻¹' U }
hy :
  Membership.mem (γ := Set { x : E // x ∈ f ⁻¹' U })
    (Set.preimage (β := (↑(f ⁻¹' {f e}) : Type u_1))
      (Function.comp (β := Prod.{u_2, u_1} (↑U : Type u_2) (↑(f ⁻¹' {f e}) : Type u_1)) Prod.snd
        (⇑H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × (↑(f ⁻¹' {f e}) : Type u_1)))
      {((H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × (↑(f ⁻¹' {f e}) : Type u_1))
            (Subtype.mk (p := fun (x : E) ↦ x ∈ f ⁻¹' U) e heU)).2})
    y
eq : (↑y : E) = (fun (x : E) ↦ g • x) (↑x : E)
⊢ IsCancelSMul G E

Tactic:
have := h.2.2.2.1
-- 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 :
  IsCoveringMap f ∧
    Function.Surjective f ∧
      ContinuousConstSMul G E ∧ IsCancelSMul G E ∧ ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ MulAction.orbit G e₂
e : E
left : DiscreteTopology.{u_1} (↑(f ⁻¹' {f e}) : Type u_1)
U : Set X
heU : f e ∈ U
hU : IsOpen[inst_1] U
hfU : IsOpen[inst] (f ⁻¹' U)
H : (↑(f ⁻¹' U) : Type u_1) ≃ₜ Prod.{u_2, u_1} (↑U : Type u_2) (↑(f ⁻¹' {f e}) : Type u_1)
hH :
  ∀ (x : (↑(f ⁻¹' U) : Type u_1)),
    (↑((H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × (↑(f ⁻¹' {f e}) : Type u_1)) x).1 : X) = f (↑x : E)
g : G
x : { x : E // x ∈ f ⁻¹' U }
hx :
  Membership.mem (γ := Set { x : E // x ∈ f ⁻¹' U })
    (Set.preimage (β := (↑(f ⁻¹' {f e}) : Type u_1))
      (Function.comp (β := Prod.{u_2, u_1} (↑U : Type u_2) (↑(f ⁻¹' {f e}) : Type u_1)) Prod.snd
        (⇑H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × (↑(f ⁻¹' {f e}) : Type u_1)))
      {((H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × (↑(f ⁻¹' {f e}) : Type u_1))
            (Subtype.mk (p := fun (x : E) ↦ x ∈ f ⁻¹' U) e heU)).2})
    x
y : { x : E // x ∈ f ⁻¹' U }
hy :
  Membership.mem (γ := Set { x : E // x ∈ f ⁻¹' U })
    (Set.preimage (β := (↑(f ⁻¹' {f e}) : Type u_1))
      (Function.comp (β := Prod.{u_2, u_1} (↑U : Type u_2) (↑(f ⁻¹' {f e}) : Type u_1)) Prod.snd
        (⇑H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × (↑(f ⁻¹' {f e}) : Type u_1)))
      {((H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × (↑(f ⁻¹' {f e}) : Type u_1))
            (Subtype.mk (p := fun (x : E) ↦ x ∈ f ⁻¹' U) e heU)).2})
    y
eq : (↑y : E) = (fun (x : E) ↦ g • x) (↑x : E)
this : IsCancelSMul G E
apply : g • (↑x : E) = HSMul.hSMul.{u_3, u_1, u_1} (α := G) 1 (↑x : E)
⊢ g = 1

Tactic:
apply IsCancelSMul.right_cancel _ _ x.1

Premises used: IsCancelSMul.right_cancel, Subtype.val
-- 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 :
  IsCoveringMap f ∧
    Function.Surjective f ∧
      ContinuousConstSMul G E ∧ IsCancelSMul G E ∧ ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ MulAction.orbit G e₂
e : E
left : DiscreteTopology.{u_1} (↑(f ⁻¹' {f e}) : Type u_1)
U : Set X
heU : f e ∈ U
hU : IsOpen[inst_1] U
hfU : IsOpen[inst] (f ⁻¹' U)
H : (↑(f ⁻¹' U) : Type u_1) ≃ₜ Prod.{u_2, u_1} (↑U : Type u_2) (↑(f ⁻¹' {f e}) : Type u_1)
hH :
  ∀ (x : (↑(f ⁻¹' U) : Type u_1)),
    (↑((H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × (↑(f ⁻¹' {f e}) : Type u_1)) x).1 : X) = f (↑x : E)
g : G
x : { x : E // x ∈ f ⁻¹' U }
hx :
  Membership.mem (γ := Set { x : E // x ∈ f ⁻¹' U })
    (Set.preimage (β := (↑(f ⁻¹' {f e}) : Type u_1))
      (Function.comp (β := Prod.{u_2, u_1} (↑U : Type u_2) (↑(f ⁻¹' {f e}) : Type u_1)) Prod.snd
        (⇑H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × (↑(f ⁻¹' {f e}) : Type u_1)))
      {((H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × (↑(f ⁻¹' {f e}) : Type u_1))
            (Subtype.mk (p := fun (x : E) ↦ x ∈ f ⁻¹' U) e heU)).2})
    x
y : { x : E // x ∈ f ⁻¹' U }
hy :
  Membership.mem (γ := Set { x : E // x ∈ f ⁻¹' U })
    (Set.preimage (β := (↑(f ⁻¹' {f e}) : Type u_1))
      (Function.comp (β := Prod.{u_2, u_1} (↑U : Type u_2) (↑(f ⁻¹' {f e}) : Type u_1)) Prod.snd
        (⇑H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × (↑(f ⁻¹' {f e}) : Type u_1)))
      {((H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × (↑(f ⁻¹' {f e}) : Type u_1))
            (Subtype.mk (p := fun (x : E) ↦ x ∈ f ⁻¹' U) e heU)).2})
    y
eq : (↑y : E) = (fun (x : E) ↦ g • x) (↑x : E)
this : IsCancelSMul G E
simp_rw : (↑y : E) = (↑x : E)
⊢ g • (↑x : E) = HSMul.hSMul.{u_3, u_1, u_1} (α := G) 1 (↑x : E)

Tactic:
simp_rw [← eq, one_smul]

Premises used: one_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 :
  IsCoveringMap f ∧
    Function.Surjective f ∧
      ContinuousConstSMul G E ∧ IsCancelSMul G E ∧ ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ MulAction.orbit G e₂
e : E
left : DiscreteTopology.{u_1} (↑(f ⁻¹' {f e}) : Type u_1)
U : Set X
heU : f e ∈ U
hU : IsOpen[inst_1] U
hfU : IsOpen[inst] (f ⁻¹' U)
H : (↑(f ⁻¹' U) : Type u_1) ≃ₜ Prod.{u_2, u_1} (↑U : Type u_2) (↑(f ⁻¹' {f e}) : Type u_1)
hH :
  ∀ (x : (↑(f ⁻¹' U) : Type u_1)),
    (↑((H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × (↑(f ⁻¹' {f e}) : Type u_1)) x).1 : X) = f (↑x : E)
g : G
x : { x : E // x ∈ f ⁻¹' U }
hx :
  Membership.mem (γ := Set { x : E // x ∈ f ⁻¹' U })
    (Set.preimage (β := (↑(f ⁻¹' {f e}) : Type u_1))
      (Function.comp (β := Prod.{u_2, u_1} (↑U : Type u_2) (↑(f ⁻¹' {f e}) : Type u_1)) Prod.snd
        (⇑H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × (↑(f ⁻¹' {f e}) : Type u_1)))
      {((H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × (↑(f ⁻¹' {f e}) : Type u_1))
            (Subtype.mk (p := fun (x : E) ↦ x ∈ f ⁻¹' U) e heU)).2})
    x
y : { x : E // x ∈ f ⁻¹' U }
hy :
  Membership.mem (γ := Set { x : E // x ∈ f ⁻¹' U })
    (Set.preimage (β := (↑(f ⁻¹' {f e}) : Type u_1))
      (Function.comp (β := Prod.{u_2, u_1} (↑U : Type u_2) (↑(f ⁻¹' {f e}) : Type u_1)) Prod.snd
        (⇑H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × (↑(f ⁻¹' {f e}) : Type u_1)))
      {((H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × (↑(f ⁻¹' {f e}) : Type u_1))
            (Subtype.mk (p := fun (x : E) ↦ x ∈ f ⁻¹' U) e heU)).2})
    y
eq : (↑y : E) = (fun (x : E) ↦ g • x) (↑x : E)
this : IsCancelSMul G E
⊢ (↑y : E) = (↑x : E)

Tactic:
congr($(H.injective <| Prod.ext (Subtype.ext ?_) <| hy.trans hx.symm))

Premises used: congrArg, id, Homeomorph.injective, Prod.ext, Eq.symm, Subtype.val, Eq.trans, Subtype.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
h :
  IsCoveringMap f ∧
    Function.Surjective f ∧
      ContinuousConstSMul G E ∧ IsCancelSMul G E ∧ ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ MulAction.orbit G e₂
e : E
left : DiscreteTopology.{u_1} (↑(f ⁻¹' {f e}) : Type u_1)
U : Set X
heU : f e ∈ U
hU : IsOpen[inst_1] U
hfU : IsOpen[inst] (f ⁻¹' U)
H : (↑(f ⁻¹' U) : Type u_1) ≃ₜ Prod.{u_2, u_1} (↑U : Type u_2) (↑(f ⁻¹' {f e}) : Type u_1)
hH :
  ∀ (x : (↑(f ⁻¹' U) : Type u_1)),
    (↑((H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × (↑(f ⁻¹' {f e}) : Type u_1)) x).1 : X) = f (↑x : E)
g : G
x : { x : E // x ∈ f ⁻¹' U }
hx :
  Membership.mem (γ := Set { x : E // x ∈ f ⁻¹' U })
    (Set.preimage (β := (↑(f ⁻¹' {f e}) : Type u_1))
      (Function.comp (β := Prod.{u_2, u_1} (↑U : Type u_2) (↑(f ⁻¹' {f e}) : Type u_1)) Prod.snd
        (⇑H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × (↑(f ⁻¹' {f e}) : Type u_1)))
      {((H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × (↑(f ⁻¹' {f e}) : Type u_1))
            (Subtype.mk (p := fun (x : E) ↦ x ∈ f ⁻¹' U) e heU)).2})
    x
y : { x : E // x ∈ f ⁻¹' U }
hy :
  Membership.mem (γ := Set { x : E // x ∈ f ⁻¹' U })
    (Set.preimage (β := (↑(f ⁻¹' {f e}) : Type u_1))
      (Function.comp (β := Prod.{u_2, u_1} (↑U : Type u_2) (↑(f ⁻¹' {f e}) : Type u_1)) Prod.snd
        (⇑H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × (↑(f ⁻¹' {f e}) : Type u_1)))
      {((H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × (↑(f ⁻¹' {f e}) : Type u_1))
            (Subtype.mk (p := fun (x : E) ↦ x ∈ f ⁻¹' U) e heU)).2})
    y
eq : (↑y : E) = (fun (x : E) ↦ g • x) (↑x : E)
this : IsCancelSMul G E
refine :
  Eq.{u_2 + 1} (α := X) (↑((H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × (↑(f ⁻¹' {f e}) : Type u_1)) y).1 : X)
    (↑((H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × (↑(f ⁻¹' {f e}) : Type u_1)) x).1 : X)
⊢ (↑y : E) = (↑x : E)

Tactic:
refine congr($(H.injective <| Prod.ext (Subtype.ext ?_) <| hy.trans hx.symm))

Premises used: Homeomorph.injective, Prod.ext, Eq.symm, Eq.trans, Subtype.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
h :
  IsCoveringMap f ∧
    Function.Surjective f ∧
      ContinuousConstSMul G E ∧ IsCancelSMul G E ∧ ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ MulAction.orbit G e₂
e : E
left : DiscreteTopology.{u_1} (↑(f ⁻¹' {f e}) : Type u_1)
U : Set X
heU : f e ∈ U
hU : IsOpen[inst_1] U
hfU : IsOpen[inst] (f ⁻¹' U)
H : (↑(f ⁻¹' U) : Type u_1) ≃ₜ Prod.{u_2, u_1} (↑U : Type u_2) (↑(f ⁻¹' {f e}) : Type u_1)
hH :
  ∀ (x : (↑(f ⁻¹' U) : Type u_1)),
    (↑((H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × (↑(f ⁻¹' {f e}) : Type u_1)) x).1 : X) = f (↑x : E)
g : G
x : { x : E // x ∈ f ⁻¹' U }
hx :
  Membership.mem (γ := Set { x : E // x ∈ f ⁻¹' U })
    (Set.preimage (β := (↑(f ⁻¹' {f e}) : Type u_1))
      (Function.comp (β := Prod.{u_2, u_1} (↑U : Type u_2) (↑(f ⁻¹' {f e}) : Type u_1)) Prod.snd
        (⇑H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × (↑(f ⁻¹' {f e}) : Type u_1)))
      {((H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × (↑(f ⁻¹' {f e}) : Type u_1))
            (Subtype.mk (p := fun (x : E) ↦ x ∈ f ⁻¹' U) e heU)).2})
    x
y : { x : E // x ∈ f ⁻¹' U }
hy :
  Membership.mem (γ := Set { x : E // x ∈ f ⁻¹' U })
    (Set.preimage (β := (↑(f ⁻¹' {f e}) : Type u_1))
      (Function.comp (β := Prod.{u_2, u_1} (↑U : Type u_2) (↑(f ⁻¹' {f e}) : Type u_1)) Prod.snd
        (⇑H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × (↑(f ⁻¹' {f e}) : Type u_1)))
      {((H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × (↑(f ⁻¹' {f e}) : Type u_1))
            (Subtype.mk (p := fun (x : E) ↦ x ∈ f ⁻¹' U) e heU)).2})
    y
eq : (↑y : E) = (fun (x : E) ↦ g • x) (↑x : E)
this : IsCancelSMul G E
simp_rw : f (↑y : E) = f (↑x : E)
⊢ Eq.{u_2 + 1} (α := X) (↑((H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × (↑(f ⁻¹' {f e}) : Type u_1)) y).1 : X)
    (↑((H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × (↑(f ⁻¹' {f e}) : Type u_1)) x).1 : X)

Tactic:
simp_rw [hH]
-- 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 :
  IsCoveringMap f ∧
    Function.Surjective f ∧
      ContinuousConstSMul G E ∧ IsCancelSMul G E ∧ ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ MulAction.orbit G e₂
e : E
left : DiscreteTopology.{u_1} (↑(f ⁻¹' {f e}) : Type u_1)
U : Set X
heU : f e ∈ U
hU : IsOpen[inst_1] U
hfU : IsOpen[inst] (f ⁻¹' U)
H : (↑(f ⁻¹' U) : Type u_1) ≃ₜ Prod.{u_2, u_1} (↑U : Type u_2) (↑(f ⁻¹' {f e}) : Type u_1)
hH :
  ∀ (x : (↑(f ⁻¹' U) : Type u_1)),
    (↑((H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × (↑(f ⁻¹' {f e}) : Type u_1)) x).1 : X) = f (↑x : E)
g : G
x : { x : E // x ∈ f ⁻¹' U }
hx :
  Membership.mem (γ := Set { x : E // x ∈ f ⁻¹' U })
    (Set.preimage (β := (↑(f ⁻¹' {f e}) : Type u_1))
      (Function.comp (β := Prod.{u_2, u_1} (↑U : Type u_2) (↑(f ⁻¹' {f e}) : Type u_1)) Prod.snd
        (⇑H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × (↑(f ⁻¹' {f e}) : Type u_1)))
      {((H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × (↑(f ⁻¹' {f e}) : Type u_1))
            (Subtype.mk (p := fun (x : E) ↦ x ∈ f ⁻¹' U) e heU)).2})
    x
y : { x : E // x ∈ f ⁻¹' U }
hy :
  Membership.mem (γ := Set { x : E // x ∈ f ⁻¹' U })
    (Set.preimage (β := (↑(f ⁻¹' {f e}) : Type u_1))
      (Function.comp (β := Prod.{u_2, u_1} (↑U : Type u_2) (↑(f ⁻¹' {f e}) : Type u_1)) Prod.snd
        (⇑H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × (↑(f ⁻¹' {f e}) : Type u_1)))
      {((H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × (↑(f ⁻¹' {f e}) : Type u_1))
            (Subtype.mk (p := fun (x : E) ↦ x ∈ f ⁻¹' U) e heU)).2})
    y
eq : (↑y : E) = (fun (x : E) ↦ g • x) (↑x : E)
this : IsCancelSMul G E
⊢ f (↑y : E) = f (↑x : E)

Tactic:
h.2.2.2.2.mpr ⟨_, eq.symm⟩

Premises used: Iff.mpr, And.right, Exists.intro, 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
h :
  IsCoveringMap f ∧
    Function.Surjective f ∧
      ContinuousConstSMul G E ∧ IsCancelSMul G E ∧ ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ MulAction.orbit G e₂
e : E
left : DiscreteTopology.{u_1} (↑(f ⁻¹' {f e}) : Type u_1)
U : Set X
heU : f e ∈ U
hU : IsOpen[inst_1] U
hfU : IsOpen[inst] (f ⁻¹' U)
H : (↑(f ⁻¹' U) : Type u_1) ≃ₜ Prod.{u_2, u_1} (↑U : Type u_2) (↑(f ⁻¹' {f e}) : Type u_1)
hH :
  ∀ (x : (↑(f ⁻¹' U) : Type u_1)),
    (↑((H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × (↑(f ⁻¹' {f e}) : Type u_1)) x).1 : X) = f (↑x : E)
g : G
x : { x : E // x ∈ f ⁻¹' U }
hx :
  Membership.mem (γ := Set { x : E // x ∈ f ⁻¹' U })
    (Set.preimage (β := (↑(f ⁻¹' {f e}) : Type u_1))
      (Function.comp (β := Prod.{u_2, u_1} (↑U : Type u_2) (↑(f ⁻¹' {f e}) : Type u_1)) Prod.snd
        (⇑H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × (↑(f ⁻¹' {f e}) : Type u_1)))
      {((H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × (↑(f ⁻¹' {f e}) : Type u_1))
            (Subtype.mk (p := fun (x : E) ↦ x ∈ f ⁻¹' U) e heU)).2})
    x
y : { x : E // x ∈ f ⁻¹' U }
hy :
  Membership.mem (γ := Set { x : E // x ∈ f ⁻¹' U })
    (Set.preimage (β := (↑(f ⁻¹' {f e}) : Type u_1))
      (Function.comp (β := Prod.{u_2, u_1} (↑U : Type u_2) (↑(f ⁻¹' {f e}) : Type u_1)) Prod.snd
        (⇑H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × (↑(f ⁻¹' {f e}) : Type u_1)))
      {((H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × (↑(f ⁻¹' {f e}) : Type u_1))
            (Subtype.mk (p := fun (x : E) ↦ x ∈ f ⁻¹' U) e heU)).2})
    y
eq : (↑y : E) = (fun (x : E) ↦ g • x) (↑x : E)
this : IsCancelSMul G E
⊢ f (↑y : E) = f (↑x : E)

Tactic:
exact h.2.2.2.2.mpr ⟨_, eq.symm⟩

Premises used: Iff.mpr, And.right, Exists.intro, Eq.symm
-- Module: Mathlib.Topology.Defs.Basic
Goal:
X : Type u
inst : TopologicalSpace X
⊢ IsOpen.{u} (X := X) univ

Tactic:
TopologicalSpace.isOpen_univ

Premises used: IsOpen, TopologicalSpace.isOpen_univ
-- Module: Mathlib.Topology.Defs.Basic
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
hs : IsOpen s
ht : IsOpen t
⊢ IsOpen (s ∩ t)

Tactic:
TopologicalSpace.isOpen_inter s t hs ht

Premises used: IsOpen, TopologicalSpace.isOpen_inter
-- Module: Mathlib.Topology.Defs.Basic
Goal:
X : Type u
inst : TopologicalSpace X
s : Set (Set X)
h : ∀ (t : Set X), t ∈ s → IsOpen t
⊢ IsOpen (⋃₀ s)

Tactic:
TopologicalSpace.isOpen_sUnion s h

Premises used: IsOpen, TopologicalSpace.isOpen_sUnion
-- Module: Mathlib.Topology.Defs.Induced
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
t : TopologicalSpace Y
s'₁ : Set Y
hs₁ : IsOpen[t] s'₁
s'₂ : Set Y
hs₂ : IsOpen[t] s'₂
⊢ ∃ (t_1 : Set Y), IsOpen[t] t_1 ∧ f ⁻¹' t_1 = f ⁻¹' s'₁ ∩ f ⁻¹' s'₂

Tactic:
⟨s'₁ ∩ s'₂, hs₁.inter hs₂, preimage_inter⟩

Premises used: Set.preimage_inter, Inter.inter, And.intro, IsOpen.inter, Exists.intro
-- Module: Mathlib.Topology.Defs.Induced
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
t : TopologicalSpace Y
s'₁ : Set Y
hs₁ : IsOpen[t] s'₁
s'₂ : Set Y
hs₂ : IsOpen[t] s'₂
⊢ ∃ (t_1 : Set Y), IsOpen[t] t_1 ∧ f ⁻¹' t_1 = f ⁻¹' s'₁ ∩ f ⁻¹' s'₂

Tactic:
exact ⟨s'₁ ∩ s'₂, hs₁.inter hs₂, preimage_inter⟩
-- Module: Mathlib.Topology.Defs.Induced
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
t : TopologicalSpace Y
S : Set (Set X)
h : ∀ t_1 ∈ S, ∃ (t_2 : Set Y), IsOpen[t] t_2 ∧ f ⁻¹' t_2 = t_1
choose! :
  ∀ (g : (t : Set X) → Set Y) (hgo : ∀ t_1 ∈ S, IsOpen[t] (g t_1)) (hfg : ∀ t ∈ S, f ⁻¹' g t = t),
    ∃ (t_1 : Set Y), IsOpen[t] t_1 ∧ f ⁻¹' t_1 = ⋃₀ S
⊢ ∃ (t_1 : Set Y), IsOpen[t] t_1 ∧ f ⁻¹' t_1 = ⋃₀ S

Tactic:
choose! g hgo hfg using h
-- Module: Mathlib.Topology.Defs.Induced
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
t : TopologicalSpace Y
S : Set (Set X)
g : (t : Set X) → Set Y
hgo : ∀ t_1 ∈ S, IsOpen[t] (g t_1)
hfg : ∀ t ∈ S, f ⁻¹' g t = t
⊢ ∃ (t_1 : Set Y), IsOpen[t] t_1 ∧ f ⁻¹' t_1 = ⋃₀ S

Tactic:
⟨⋃₀ (g '' S), isOpen_sUnion <| forall_mem_image.2 hgo, ?_⟩

Premises used: Iff.mpr, Set.sUnion, And.intro, Exists.intro, Set.image, isOpen_sUnion, Set.forall_mem_image