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
s : Set X
Y : Type u_3
inst_2 : TopologicalSpace Y
g : X ≃ₜ Y
h : IsCoveringMapOn.{u_1, u_3} (X := Y) ((⇑g : (a : X) → Y) ∘ f) ((⇑g.symm : (a : Y) → X) ⁻¹' s)
h₁ :
  ∀ (x : E), f x = Function.comp.{u_1 + 1, u_3 + 1, u_2 + 1} (β := Y) (⇑g.symm : (a : Y) → X) ((⇑g : (a : X) → Y) ∘ f) x
⊢ f = Function.comp.{u_1 + 1, u_3 + 1, u_2 + 1} (β := Y) (⇑g.symm : (a : Y) → X) ((⇑g : (a : X) → Y) ∘ f)

Tactic:
ext
-- 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
Y : Type u_3
inst_2 : TopologicalSpace Y
g : X ≃ₜ Y
h : IsCoveringMapOn.{u_1, u_3} (X := Y) ((⇑g : (a : X) → Y) ∘ f) ((⇑g.symm : (a : Y) → X) ⁻¹' s)
x : E
⊢ f x = Function.comp.{u_1 + 1, u_3 + 1, u_2 + 1} (β := Y) (⇑g.symm : (a : Y) → X) ((⇑g : (a : X) → Y) ∘ f) x

Tactic:
simp
-- 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
Y : Type u_3
inst_2 : TopologicalSpace Y
g : X ≃ₜ Y
h : IsCoveringMapOn.{u_1, u_3} (X := Y) ((⇑g : (a : X) → Y) ∘ f) ((⇑g.symm : (a : Y) → X) ⁻¹' s)
h₁ :
  ∀ (x : X),
    x ∈ s ↔
      Membership.mem (γ := Set X)
        (Set.preimage.{u_2, u_3} (β := Y) (⇑g.symm.symm : (a : X) → Y) ((⇑g.symm : (a : Y) → X) ⁻¹' s)) x
⊢ s = Set.preimage.{u_2, u_3} (β := Y) (⇑g.symm.symm : (a : X) → Y) ((⇑g.symm : (a : Y) → X) ⁻¹' s)

Tactic:
ext
-- 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
Y : Type u_3
inst_2 : TopologicalSpace Y
g : X ≃ₜ Y
h : IsCoveringMapOn.{u_1, u_3} (X := Y) ((⇑g : (a : X) → Y) ∘ f) ((⇑g.symm : (a : Y) → X) ⁻¹' s)
x : X
⊢ x ∈ s ↔
    Membership.mem (γ := Set X)
      (Set.preimage.{u_2, u_3} (β := Y) (⇑g.symm.symm : (a : X) → Y) ((⇑g.symm : (a : Y) → X) ⁻¹' s)) x

Tactic:
simp
-- Module: Mathlib.Topology.Covering.Basic
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
⊢ IsCoveringMap f ↔ IsCoveringMapOn f Set.univ

Tactic:
simp only [IsCoveringMap, IsCoveringMapOn, Set.mem_univ, forall_true_left]

Premises used: forall_true_left, IsCoveringMapOn, Set.mem_univ, IsCoveringMap
-- Module: Mathlib.Topology.Covering.Basic
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
hf : IsCoveringMap f
⊢ IsCoveringMapOn f Set.univ

Tactic:
isCoveringMap_iff_isCoveringMapOn_univ.mp hf

Premises used: isCoveringMap_iff_isCoveringMapOn_univ, Iff.mp
-- 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
hf : IsCoveringMapOn f s
⊢ IsCoveringMapOn (s.restrictPreimage f) Set.univ

Tactic:
simpa using hf.restrictPreimage s

Premises used: IsCoveringMapOn.restrictPreimage
-- 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
hs : IsOpen[inst_1] s
hfs : IsOpen[inst] (f ⁻¹' s)
hf : IsCoveringMap (s.restrictPreimage f)
⊢ IsCoveringMapOn f s

Tactic:
fun x hx ↦
  (((hf ⟨x, hx⟩).subtypeVal_comp _ hs).comp_subtypeVal _ hs hfs hx).to_isEvenlyCovered_preimage

Premises used: IsEvenlyCovered.subtypeVal_comp, IsCoveringMapOn, Subtype.mk, IsEvenlyCovered.comp_subtypeVal, IsEvenlyCovered.to_isEvenlyCovered_preimage
-- 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 : IsEmpty E
⊢ IsCoveringMap f

Tactic:
isCoveringMap_iff_isCoveringMapOn_univ.mpr <| .of_isEmpty _ _

Premises used: Iff.mpr, IsCoveringMapOn.of_isEmpty, isCoveringMap_iff_isCoveringMapOn_univ
-- 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 : DiscreteTopology E
inst_3 : DiscreteTopology X
⊢ IsCoveringMap f

Tactic:
fun x ↦ ⟨inferInstance, {x}, rfl, isOpen_discrete _, isOpen_discrete _,
    { toFun e := ⟨⟨x, rfl⟩, e⟩
      invFun xi := xi.2
      left_inv _ := rfl
      right_inv _ := Prod.ext (Subsingleton.elim ..) rfl },
    (·.2.symm)⟩

Premises used: Homeomorph.mk, Equiv.mk, inferInstance, Prod.mk, IsEvenlyCovered, Prod.fst, Subtype.mk, Set.preimage, Prod.ext, And.intro, isOpen_discrete, Exists.intro, Subsingleton.elim, Singleton.singleton, Eq.symm, Prod.snd, rfl, IsCoveringMap, Subtype.property
-- Module: Mathlib.Topology.Covering.Basic
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
F : X → Type u_3
inst_2 : (x : X) → TopologicalSpace (F x)
inst_3 : ∀ (x : X), DiscreteTopology.{u_3} (F x)
t : (x : X) → x ∈ Set.range f → { t : Trivialization.{u_2, u_3, u_1} (F x) f // x ∈ t.baseSet }
h : IsClosed[inst_1] (Set.range f)
⊢ IsCoveringMap f

Tactic:
isCoveringMap_iff_isCoveringMapOn_univ.mpr <| .mk' f _ _ (fun x h ↦ t x h) fun _x hx ↦
    ⟨_, h.isOpen_compl.mem_nhds hx, Set.eq_empty_of_forall_notMem fun x h ↦ h ⟨x, rfl⟩⟩

Premises used: Iff.mpr, IsClosed.isOpen_compl, Compl.compl, isCoveringMap_iff_isCoveringMapOn_univ, IsCoveringMapOn.mk', Set.eq_empty_of_forall_notMem, And.intro, IsOpen.mem_nhds, Exists.intro, Set.range, Subtype.val, rfl
-- Module: Mathlib.Topology.Covering.Basic
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
F : X → Type u_3
inst_2 : (x : X) → TopologicalSpace (F x)
inst_3 : ∀ (x : X), DiscreteTopology.{u_3} (F x)
e : (x : X) → Trivialization.{u_2, u_3, u_1} (F x) f
h : ∀ (x : X), x ∈ (e x).baseSet
⊢ IsCoveringMap f

Tactic:
isCoveringMap_iff_isCoveringMapOn_univ.mpr <| .mk _ _ _ _ fun x ↦ h x

Premises used: Iff.mpr, isCoveringMap_iff_isCoveringMapOn_univ, IsCoveringMapOn.mk, Subtype.val
-- Module: Mathlib.Topology.Covering.Basic
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
hf : IsCoveringMap f
⊢ Continuous[inst, inst_1] f

Tactic:
continuousOn_univ.mp hf.isCoveringMapOn.continuousOn

Premises used: Iff.mp, continuousOn_univ, IsCoveringMap.isCoveringMapOn, IsCoveringMapOn.continuousOn
-- Module: Mathlib.Topology.Covering.Basic
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
hf : IsCoveringMap f
⊢ IsLocalHomeomorph f

Tactic:
isLocalHomeomorph_iff_isLocalHomeomorphOn_univ.mpr hf.isCoveringMapOn.isLocalHomeomorphOn

Premises used: Iff.mpr, isLocalHomeomorph_iff_isLocalHomeomorphOn_univ, IsCoveringMapOn.isLocalHomeomorphOn, IsCoveringMap.isCoveringMapOn
-- Module: Mathlib.Topology.Covering.Basic
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
hf : IsCoveringMap f
⊢ IsOpenMap f

Tactic:
hf.isLocalHomeomorph.isOpenMap

Premises used: IsCoveringMap.isLocalHomeomorph, IsLocalHomeomorph.isOpenMap
-- Module: Mathlib.Topology.Covering.Basic
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
hf : IsCoveringMap f
hf' : Function.Surjective f
⊢ IsQuotientMap f

Tactic:
hf.isOpenMap.isQuotientMap hf.continuous hf'

Premises used: IsOpenMap.isQuotientMap, IsCoveringMap.isOpenMap, IsCoveringMap.continuous
-- Module: Mathlib.Topology.Covering.Basic
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
hf : IsCoveringMap f
e₁ e₂ : E
he : f e₁ = f e₂
hne : e₁ ≠ e₂
⊢ Nonempty.{u_1 + 1} (↑(f ⁻¹' {f e₁}) : Type u_1)

Tactic:
have : Nonempty (f ⁻¹' {f e₁}) := ⟨⟨e₁, rfl⟩⟩
-- Module: Mathlib.Topology.Covering.Basic
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
hf : IsCoveringMap f
e₁ e₂ : E
he : f e₁ = f e₂
hne : e₁ ≠ e₂
this : Nonempty.{u_1 + 1} (↑(f ⁻¹' {f e₁}) : Type u_1)
⊢ IsEvenlyCovered f (f e₁) (↑(f ⁻¹' {f e₁}) : Type u_1)

Tactic:
specialize hf (f 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
e₁ e₂ : E
he : f e₁ = f e₂
hne : e₁ ≠ e₂
this : Nonempty.{u_1 + 1} (↑(f ⁻¹' {f e₁}) : Type u_1)
hf : IsEvenlyCovered f (f e₁) (↑(f ⁻¹' {f e₁}) : Type u_1)
t : Trivialization (↑(f ⁻¹' {f e₁}) : Type u_1) f := hf.toTrivialization
⊢ DiscreteTopology.{u_1} (↑(f ⁻¹' {f e₁}) : Type u_1)

Tactic:
have := hf.discreteTopology_fiber
-- Module: Mathlib.Topology.Covering.Basic
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
e₁ e₂ : E
he : f e₁ = f e₂
hne : e₁ ≠ e₂
this_1 : Nonempty.{u_1 + 1} (↑(f ⁻¹' {f e₁}) : Type u_1)
hf : IsEvenlyCovered f (f e₁) (↑(f ⁻¹' {f e₁}) : Type u_1)
t : Trivialization (↑(f ⁻¹' {f e₁}) : Type u_1) f := hf.toTrivialization
this : DiscreteTopology.{u_1} (↑(f ⁻¹' {f e₁}) : Type u_1)
⊢ f e₁ ∈ hf.toTrivialization.baseSet

Tactic:
have he₁ := hf.mem_toTrivialization_baseSet
-- Module: Mathlib.Topology.Covering.Basic
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
e₁ e₂ : E
he : f e₁ = f e₂
hne : e₁ ≠ e₂
this_1 : Nonempty.{u_1 + 1} (↑(f ⁻¹' {f e₁}) : Type u_1)
hf : IsEvenlyCovered f (f e₁) (↑(f ⁻¹' {f e₁}) : Type u_1)
t : Trivialization (↑(f ⁻¹' {f e₁}) : Type u_1) f := hf.toTrivialization
this : DiscreteTopology.{u_1} (↑(f ⁻¹' {f e₁}) : Type u_1)
he₁ : f e₁ ∈ hf.toTrivialization.baseSet
⊢ f e₁ ∈ hf.toTrivialization.baseSet

Tactic:
have he₂ := he₁
-- Module: Mathlib.Topology.Covering.Basic
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
e₁ e₂ : E
he : f e₁ = f e₂
hne : e₁ ≠ e₂
this_1 : Nonempty.{u_1 + 1} (↑(f ⁻¹' {f e₁}) : Type u_1)
hf : IsEvenlyCovered f (f e₁) (↑(f ⁻¹' {f e₁}) : Type u_1)
t : Trivialization (↑(f ⁻¹' {f e₁}) : Type u_1) f := hf.toTrivialization
this : DiscreteTopology.{u_1} (↑(f ⁻¹' {f e₁}) : Type u_1)
he₁ he₂ : f e₁ ∈ hf.toTrivialization.baseSet
⊢ f e₂ ∈ hf.toTrivialization.baseSet

Tactic:
simp_rw [he] at he₂
-- Module: Mathlib.Topology.Covering.Basic
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
e₁ e₂ : E
he : f e₁ = f e₂
hne : e₁ ≠ e₂
this_1 : Nonempty.{u_1 + 1} (↑(f ⁻¹' {f e₁}) : Type u_1)
hf : IsEvenlyCovered f (f e₁) (↑(f ⁻¹' {f e₁}) : Type u_1)
t : Trivialization (↑(f ⁻¹' {f e₁}) : Type u_1) f := hf.toTrivialization
this : DiscreteTopology.{u_1} (↑(f ⁻¹' {f e₁}) : Type u_1)
he₁ : f e₁ ∈ hf.toTrivialization.baseSet
he₂ : f e₂ ∈ hf.toTrivialization.baseSet
⊢ e₁ ∈ t.source

Tactic:
rw [← t.mem_source] at he₁ he₂

Premises used: Bundle.Trivialization.mem_source
-- Module: Mathlib.Topology.Covering.Basic
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
e₁ e₂ : E
he : f e₁ = f e₂
hne : e₁ ≠ e₂
this_1 : Nonempty.{u_1 + 1} (↑(f ⁻¹' {f e₁}) : Type u_1)
hf : IsEvenlyCovered f (f e₁) (↑(f ⁻¹' {f e₁}) : Type u_1)
t : Trivialization (↑(f ⁻¹' {f e₁}) : Type u_1) f := hf.toTrivialization
this : DiscreteTopology.{u_1} (↑(f ⁻¹' {f e₁}) : Type u_1)
he₁ : f e₁ ∈ hf.toTrivialization.baseSet
he₂ : f e₂ ∈ hf.toTrivialization.baseSet
he₃ : e₁ ∈ t.source
⊢ e₂ ∈ t.source

Tactic:
rw [← t.mem_source] at he₁ he₂

Premises used: Bundle.Trivialization.mem_source
-- Module: Mathlib.Topology.Covering.Basic
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
e₁ e₂ : E
he : f e₁ = f e₂
hne : e₁ ≠ e₂
this_1 : Nonempty.{u_1 + 1} (↑(f ⁻¹' {f e₁}) : Type u_1)
hf : IsEvenlyCovered f (f e₁) (↑(f ⁻¹' {f e₁}) : Type u_1)
t : Trivialization (↑(f ⁻¹' {f e₁}) : Type u_1) f := hf.toTrivialization
this : DiscreteTopology.{u_1} (↑(f ⁻¹' {f e₁}) : Type u_1)
he₁ : e₁ ∈ t.source
he₂ : e₂ ∈ t.source
⊢ ∃ (s₁ : Set E) (s₂ : Set E), IsOpen[inst] s₁ ∧ IsOpen[inst] s₂ ∧ e₁ ∈ s₁ ∧ e₂ ∈ s₂ ∧ Disjoint s₁ s₂

Tactic:
⟨t.source ∩ (Prod.snd ∘ t) ⁻¹' {(t e₁).2}, t.source ∩ (Prod.snd ∘ t) ⁻¹' {(t e₂).2},
      ?_, ?_, ⟨he₁, rfl⟩, ⟨he₂, rfl⟩, Set.disjoint_left.mpr fun x h₁ h₂ ↦ hne (t.injOn he₁ he₂ ?_)⟩

Premises used: Iff.mpr, Bundle.Trivialization.toFun', Set.disjoint_left, Function.comp, Inter.inter, Set.preimage, And.intro, OpenPartialHomeomorph.injOn, Exists.intro, PartialEquiv.source, Singleton.singleton, OpenPartialHomeomorph.toPartialEquiv, Prod.snd, rfl, Bundle.Trivialization.toOpenPartialHomeomorph
-- Module: Mathlib.Topology.Covering.Basic
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
e₁ e₂ : E
he : f e₁ = f e₂
hne : e₁ ≠ e₂
this_1 : Nonempty.{u_1 + 1} (↑(f ⁻¹' {f e₁}) : Type u_1)
hf : IsEvenlyCovered f (f e₁) (↑(f ⁻¹' {f e₁}) : Type u_1)
t : Trivialization (↑(f ⁻¹' {f e₁}) : Type u_1) f := hf.toTrivialization
this : DiscreteTopology.{u_1} (↑(f ⁻¹' {f e₁}) : Type u_1)
he₁ : e₁ ∈ t.source
he₂ : e₂ ∈ t.source
refine_1 :
  IsOpen[inst]
    (t.source ∩
      Prod.snd ∘ (↑t : E → X × (↑(f ⁻¹' {f e₁}) : Type u_1)) ⁻¹' {((↑t : E → X × (↑(f ⁻¹' {f e₁}) : Type u_1)) e₁).2})
refine_2 :
  IsOpen[inst]
    (t.source ∩
      Prod.snd ∘ (↑t : E → X × (↑(f ⁻¹' {f e₁}) : Type u_1)) ⁻¹' {((↑t : E → X × (↑(f ⁻¹' {f e₁}) : Type u_1)) e₂).2})
refine_3 :
  ∀ (x : E)
    (h₁ :
      x ∈
        t.source ∩
          Prod.snd ∘ (↑t : E → X × (↑(f ⁻¹' {f e₁}) : Type u_1)) ⁻¹'
            {((↑t : E → X × (↑(f ⁻¹' {f e₁}) : Type u_1)) e₁).2})
    (h₂ :
      x ∈
        t.source ∩
          Prod.snd ∘ (↑t : E → X × (↑(f ⁻¹' {f e₁}) : Type u_1)) ⁻¹'
            {((↑t : E → X × (↑(f ⁻¹' {f e₁}) : Type u_1)) e₂).2}),
    (↑t.toOpenPartialHomeomorph : E → X × (↑(f ⁻¹' {f e₁}) : Type u_1)) e₁ =
      (↑t.toOpenPartialHomeomorph : E → X × (↑(f ⁻¹' {f e₁}) : Type u_1)) e₂
⊢ ∃ (s₁ : Set E) (s₂ : Set E), IsOpen[inst] s₁ ∧ IsOpen[inst] s₂ ∧ e₁ ∈ s₁ ∧ e₂ ∈ s₂ ∧ Disjoint s₁ s₂

Tactic:
refine ⟨t.source ∩ (Prod.snd ∘ t) ⁻¹' {(t e₁).2}, t.source ∩ (Prod.snd ∘ t) ⁻¹' {(t e₂).2},
      ?_, ?_, ⟨he₁, rfl⟩, ⟨he₂, rfl⟩, Set.disjoint_left.mpr fun x h₁ h₂ ↦ hne (t.injOn he₁ he₂ ?_)⟩
-- Module: Mathlib.Topology.Covering.Basic
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
e₁ e₂ : E
he : f e₁ = f e₂
hne : e₁ ≠ e₂
this_1 : Nonempty.{u_1 + 1} (↑(f ⁻¹' {f e₁}) : Type u_1)
hf : IsEvenlyCovered f (f e₁) (↑(f ⁻¹' {f e₁}) : Type u_1)
t : Trivialization (↑(f ⁻¹' {f e₁}) : Type u_1) f := hf.toTrivialization
this : DiscreteTopology.{u_1} (↑(f ⁻¹' {f e₁}) : Type u_1)
he₁ : e₁ ∈ t.source
he₂ : e₂ ∈ t.source
⊢ IsOpen[inst]
    (t.source ∩
      Prod.snd ∘ (↑t : E → X × (↑(f ⁻¹' {f e₁}) : Type u_1)) ⁻¹' {((↑t : E → X × (↑(f ⁻¹' {f e₁}) : Type u_1)) e₁).2})

Tactic:
t.continuousOn_toFun.isOpen_inter_preimage t.open_source
        (continuous_snd.isOpen_preimage _ <| isOpen_discrete _)

Premises used: OpenPartialHomeomorph.open_source, Set.Mem, setOf, ContinuousOn.isOpen_inter_preimage, continuous_snd, Prod.map, Set.preimage, isOpen_discrete, Set.singleton, OpenPartialHomeomorph.continuousOn_toFun, Continuous.isOpen_preimage, Bundle.Trivialization.toOpenPartialHomeomorph
-- Module: Mathlib.Topology.Covering.Basic
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
e₁ e₂ : E
he : f e₁ = f e₂
hne : e₁ ≠ e₂
this_1 : Nonempty.{u_1 + 1} (↑(f ⁻¹' {f e₁}) : Type u_1)
hf : IsEvenlyCovered f (f e₁) (↑(f ⁻¹' {f e₁}) : Type u_1)
t : Trivialization (↑(f ⁻¹' {f e₁}) : Type u_1) f := hf.toTrivialization
this : DiscreteTopology.{u_1} (↑(f ⁻¹' {f e₁}) : Type u_1)
he₁ : e₁ ∈ t.source
he₂ : e₂ ∈ t.source
⊢ IsOpen[inst]
    (t.source ∩
      Prod.snd ∘ (↑t : E → X × (↑(f ⁻¹' {f e₁}) : Type u_1)) ⁻¹' {((↑t : E → X × (↑(f ⁻¹' {f e₁}) : Type u_1)) e₁).2})

Tactic:
exact t.continuousOn_toFun.isOpen_inter_preimage t.open_source
        (continuous_snd.isOpen_preimage _ <| isOpen_discrete _)

Premises used: OpenPartialHomeomorph.open_source, ContinuousOn.isOpen_inter_preimage, continuous_snd, isOpen_discrete, OpenPartialHomeomorph.continuousOn_toFun, Continuous.isOpen_preimage, Bundle.Trivialization.toOpenPartialHomeomorph
-- Module: Mathlib.Topology.Covering.Basic
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
e₁ e₂ : E
he : f e₁ = f e₂
hne : e₁ ≠ e₂
this_1 : Nonempty.{u_1 + 1} (↑(f ⁻¹' {f e₁}) : Type u_1)
hf : IsEvenlyCovered f (f e₁) (↑(f ⁻¹' {f e₁}) : Type u_1)
t : Trivialization (↑(f ⁻¹' {f e₁}) : Type u_1) f := hf.toTrivialization
this : DiscreteTopology.{u_1} (↑(f ⁻¹' {f e₁}) : Type u_1)
he₁ : e₁ ∈ t.source
he₂ : e₂ ∈ t.source
⊢ IsOpen[inst]
    (t.source ∩
      Prod.snd ∘ (↑t : E → X × (↑(f ⁻¹' {f e₁}) : Type u_1)) ⁻¹' {((↑t : E → X × (↑(f ⁻¹' {f e₁}) : Type u_1)) e₂).2})

Tactic:
t.continuousOn_toFun.isOpen_inter_preimage t.open_source
        (continuous_snd.isOpen_preimage _ <| isOpen_discrete _)

Premises used: OpenPartialHomeomorph.open_source, Set.Mem, setOf, ContinuousOn.isOpen_inter_preimage, continuous_snd, Prod.map, Set.preimage, isOpen_discrete, Set.singleton, OpenPartialHomeomorph.continuousOn_toFun, Continuous.isOpen_preimage, Bundle.Trivialization.toOpenPartialHomeomorph
-- Module: Mathlib.Topology.Covering.Basic
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
e₁ e₂ : E
he : f e₁ = f e₂
hne : e₁ ≠ e₂
this_1 : Nonempty.{u_1 + 1} (↑(f ⁻¹' {f e₁}) : Type u_1)
hf : IsEvenlyCovered f (f e₁) (↑(f ⁻¹' {f e₁}) : Type u_1)
t : Trivialization (↑(f ⁻¹' {f e₁}) : Type u_1) f := hf.toTrivialization
this : DiscreteTopology.{u_1} (↑(f ⁻¹' {f e₁}) : Type u_1)
he₁ : e₁ ∈ t.source
he₂ : e₂ ∈ t.source
⊢ IsOpen[inst]
    (t.source ∩
      Prod.snd ∘ (↑t : E → X × (↑(f ⁻¹' {f e₁}) : Type u_1)) ⁻¹' {((↑t : E → X × (↑(f ⁻¹' {f e₁}) : Type u_1)) e₂).2})

Tactic:
exact t.continuousOn_toFun.isOpen_inter_preimage t.open_source
        (continuous_snd.isOpen_preimage _ <| isOpen_discrete _)

Premises used: OpenPartialHomeomorph.open_source, ContinuousOn.isOpen_inter_preimage, continuous_snd, isOpen_discrete, OpenPartialHomeomorph.continuousOn_toFun, Continuous.isOpen_preimage, Bundle.Trivialization.toOpenPartialHomeomorph
-- Module: Mathlib.Topology.Covering.Basic
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
e₁ e₂ : E
he : f e₁ = f e₂
hne : e₁ ≠ e₂
this_1 : Nonempty.{u_1 + 1} (↑(f ⁻¹' {f e₁}) : Type u_1)
hf : IsEvenlyCovered f (f e₁) (↑(f ⁻¹' {f e₁}) : Type u_1)
t : Trivialization (↑(f ⁻¹' {f e₁}) : Type u_1) f := hf.toTrivialization
this : DiscreteTopology.{u_1} (↑(f ⁻¹' {f e₁}) : Type u_1)
he₁ : e₁ ∈ t.source
he₂ : e₂ ∈ t.source
x : E
h₁ :
  x ∈
    t.source ∩
      Prod.snd ∘ (↑t : E → X × (↑(f ⁻¹' {f e₁}) : Type u_1)) ⁻¹' {((↑t : E → X × (↑(f ⁻¹' {f e₁}) : Type u_1)) e₁).2}
h₂ :
  x ∈
    t.source ∩
      Prod.snd ∘ (↑t : E → X × (↑(f ⁻¹' {f e₁}) : Type u_1)) ⁻¹' {((↑t : E → X × (↑(f ⁻¹' {f e₁}) : Type u_1)) e₂).2}
⊢ (↑t.toOpenPartialHomeomorph : E → X × (↑(f ⁻¹' {f e₁}) : Type u_1)) e₁ =
    (↑t.toOpenPartialHomeomorph : E → X × (↑(f ⁻¹' {f e₁}) : Type u_1)) e₂

Tactic:
Prod.ext ?_ (h₁.2.symm.trans h₂.2)

Premises used: And.right, Prod.ext, Eq.symm, Eq.trans
-- Module: Mathlib.Topology.Covering.Basic
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
e₁ e₂ : E
he : f e₁ = f e₂
hne : e₁ ≠ e₂
this_1 : Nonempty.{u_1 + 1} (↑(f ⁻¹' {f e₁}) : Type u_1)
hf : IsEvenlyCovered f (f e₁) (↑(f ⁻¹' {f e₁}) : Type u_1)
t : Trivialization (↑(f ⁻¹' {f e₁}) : Type u_1) f := hf.toTrivialization
this : DiscreteTopology.{u_1} (↑(f ⁻¹' {f e₁}) : Type u_1)
he₁ : e₁ ∈ t.source
he₂ : e₂ ∈ t.source
x : E
h₁ :
  x ∈
    t.source ∩
      Prod.snd ∘ (↑t : E → X × (↑(f ⁻¹' {f e₁}) : Type u_1)) ⁻¹' {((↑t : E → X × (↑(f ⁻¹' {f e₁}) : Type u_1)) e₁).2}
h₂ :
  x ∈
    t.source ∩
      Prod.snd ∘ (↑t : E → X × (↑(f ⁻¹' {f e₁}) : Type u_1)) ⁻¹' {((↑t : E → X × (↑(f ⁻¹' {f e₁}) : Type u_1)) e₂).2}
refine_3 :
  ((↑t.toOpenPartialHomeomorph : E → X × (↑(f ⁻¹' {f e₁}) : Type u_1)) e₁).1 =
    ((↑t.toOpenPartialHomeomorph : E → X × (↑(f ⁻¹' {f e₁}) : Type u_1)) e₂).1
⊢ (↑t.toOpenPartialHomeomorph : E → X × (↑(f ⁻¹' {f e₁}) : Type u_1)) e₁ =
    (↑t.toOpenPartialHomeomorph : E → X × (↑(f ⁻¹' {f e₁}) : Type u_1)) e₂

Tactic:
refine Prod.ext ?_ (h₁.2.symm.trans h₂.2)

Premises used: And.right, Prod.ext, Eq.symm, Eq.trans
-- Module: Mathlib.Topology.Covering.Basic
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
e₁ e₂ : E
he : f e₁ = f e₂
hne : e₁ ≠ e₂
this_1 : Nonempty.{u_1 + 1} (↑(f ⁻¹' {f e₁}) : Type u_1)
hf : IsEvenlyCovered f (f e₁) (↑(f ⁻¹' {f e₁}) : Type u_1)
t : Trivialization (↑(f ⁻¹' {f e₁}) : Type u_1) f := hf.toTrivialization
this : DiscreteTopology.{u_1} (↑(f ⁻¹' {f e₁}) : Type u_1)
he₁ : e₁ ∈ t.source
he₂ : e₂ ∈ t.source
x : E
h₁ :
  x ∈
    t.source ∩
      Prod.snd ∘ (↑t : E → X × (↑(f ⁻¹' {f e₁}) : Type u_1)) ⁻¹' {((↑t : E → X × (↑(f ⁻¹' {f e₁}) : Type u_1)) e₁).2}
h₂ :
  x ∈
    t.source ∩
      Prod.snd ∘ (↑t : E → X × (↑(f ⁻¹' {f e₁}) : Type u_1)) ⁻¹' {((↑t : E → X × (↑(f ⁻¹' {f e₁}) : Type u_1)) e₂).2}
refine_3 : f e₁ = ((↑t.toOpenPartialHomeomorph : E → X × (↑(f ⁻¹' {f e₁}) : Type u_1)) e₂).1
refine_3₁ refine_3₂ refine_3₃ refine_3₄ : f e₁ = f e₂
⊢ ((↑t.toOpenPartialHomeomorph : E → X × (↑(f ⁻¹' {f e₁}) : Type u_1)) e₁).1 =
    ((↑t.toOpenPartialHomeomorph : E → X × (↑(f ⁻¹' {f e₁}) : Type u_1)) e₂).1

Tactic:
rwa [t.proj_toFun e₁ he₁, t.proj_toFun e₂ he₂]

Premises used: Bundle.Trivialization.proj_toFun
-- Module: Mathlib.Topology.Covering.Basic
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
hf : IsCoveringMap f
A : Type u_3
inst_2 : TopologicalSpace A
g₁ g₂ : A → E
inst_3 : PreconnectedSpace A
h₁ : Continuous[inst_2, inst] g₁
h₂ : Continuous[inst_2, inst] g₂
he : f ∘ g₁ = f ∘ g₂
a : A
ha : g₁ a = g₂ a
⊢ g₁ = g₂

Tactic:
hf.isSeparatedMap.eq_of_comp_eq hf.isLocalHomeomorph.isLocallyInjective h₁ h₂ he a ha

Premises used: IsSeparatedMap.eq_of_comp_eq, IsCoveringMap.isLocalHomeomorph, IsLocalHomeomorph.isLocallyInjective, IsCoveringMap.isSeparatedMap
-- Module: Mathlib.Topology.Covering.Basic
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
hf : IsCoveringMap f
A : Type u_3
inst_2 : TopologicalSpace A
g : A → E
inst_3 : PreconnectedSpace A
cont : Continuous[inst_2, inst] g
he : ∀ (a a' : A), f (g a) = f (g a')
a a' : A
⊢ g a = g a'

Tactic:
hf.isSeparatedMap.const_of_comp hf.isLocalHomeomorph.isLocallyInjective cont he a a'

Premises used: IsSeparatedMap.const_of_comp, IsCoveringMap.isLocalHomeomorph, IsLocalHomeomorph.isLocallyInjective, IsCoveringMap.isSeparatedMap
-- Module: Mathlib.Topology.Covering.Basic
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
hf : IsCoveringMap f
A : Type u_3
inst_2 : TopologicalSpace A
s : Set A
g₁ g₂ : A → E
hs : IsPreconnected s
h₁ : ContinuousOn g₁ s
h₂ : ContinuousOn g₂ s
he : Set.EqOn (f ∘ g₁) (f ∘ g₂) s
a : A
has : a ∈ s
ha : g₁ a = g₂ a
⊢ Set.EqOn g₁ g₂ s

Tactic:
hf.isSeparatedMap.eqOn_of_comp_eqOn hf.isLocalHomeomorph.isLocallyInjective hs h₁ h₂ he has ha

Premises used: IsSeparatedMap.eqOn_of_comp_eqOn, IsCoveringMap.isLocalHomeomorph, IsLocalHomeomorph.isLocallyInjective, IsCoveringMap.isSeparatedMap
-- Module: Mathlib.Topology.Covering.Basic
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
hf : IsCoveringMap f
A : Type u_3
inst_2 : TopologicalSpace A
s : Set A
g : A → E
hs : IsPreconnected s
cont : ContinuousOn g s
he : ∀ a ∈ s, ∀ a' ∈ s, f (g a) = f (g a')
a a' : A
ha : a ∈ s
ha' : a' ∈ s
⊢ g a = g a'

Tactic:
hf.isSeparatedMap.constOn_of_comp hf.isLocalHomeomorph.isLocallyInjective hs cont he ha ha'

Premises used: IsSeparatedMap.constOn_of_comp, IsCoveringMap.isLocalHomeomorph, IsLocalHomeomorph.isLocallyInjective, IsCoveringMap.isSeparatedMap
-- Module: Mathlib.Topology.Covering.Basic
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
hf : IsCoveringMap f
t : Set X
rw : ∀ (hf : IsCoveringMapOn f Set.univ) (t : Set X), IsCoveringMapOn (t.restrictPreimage f) Set.univ
⊢ IsCoveringMap (t.restrictPreimage f)

Tactic:
rw [isCoveringMap_iff_isCoveringMapOn_univ] at hf ⊢

Premises used: isCoveringMap_iff_isCoveringMapOn_univ