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
I : Type u_3
inst_2 : TopologicalSpace I
x : X
Y : Type u_4
inst_3 : TopologicalSpace Y
g : X ≃ₜ Y
h : IsEvenlyCovered.{u_1, u_4, u_3} (X := Y) ((⇑g : (a : X) → Y) ∘ f : E → Y) ((g : (a : X) → Y) x : Y) I
⊢ IsEvenlyCovered.{u_1, u_2, u_3} (X := X)
    (Function.comp.{u_1 + 1, u_4 + 1, u_2 + 1} (β := Y) (⇑g.symm : (a : Y) → X) ((⇑g : (a : X) → Y) ∘ f) : E → X)
    ((g.symm : (a : Y) → X) ((g : (a : X) → Y) x : Y) : X) I

Tactic:
h.homeomorph_comp g.symm

Premises used: IsEvenlyCovered.homeomorph_comp, Homeomorph.symm
-- Module: Mathlib.Topology.Covering.Basic
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
I : Type u_3
inst_2 : TopologicalSpace I
x : X
Y : Type u_4
inst_3 : TopologicalSpace Y
g : X ≃ₜ Y
h : IsEvenlyCovered.{u_1, u_4, u_3} (X := Y) ((⇑g : (a : X) → Y) ∘ f : E → Y) ((g : (a : X) → Y) x : Y) I
h₁ : f = Function.comp.{u_1 + 1, u_4 + 1, u_2 + 1} (β := Y) (⇑g.symm : (a : Y) → X) ((⇑g : (a : X) → Y) ∘ f)
h₂ : x = (g.symm : (a : Y) → X) ((g : (a : X) → Y) x : Y)
⊢ IsEvenlyCovered f x I

Tactic:
convert! h.homeomorph_comp g.symm

Premises used: IsEvenlyCovered.homeomorph_comp, Homeomorph.symm
-- Module: Mathlib.Topology.Covering.Basic
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
I : Type u_3
inst_2 : TopologicalSpace I
x : X
Y : Type u_4
inst_3 : TopologicalSpace Y
g : X ≃ₜ Y
h : IsEvenlyCovered.{u_1, u_4, u_3} (X := Y) ((⇑g : (a : X) → Y) ∘ f : E → Y) ((g : (a : X) → Y) x : Y) I
h₁ :
  ∀ (x : E), f x = Function.comp.{u_1 + 1, u_4 + 1, u_2 + 1} (β := Y) (⇑g.symm : (a : Y) → X) ((⇑g : (a : X) → Y) ∘ f) x
⊢ f = Function.comp.{u_1 + 1, u_4 + 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
I : Type u_3
inst_2 : TopologicalSpace I
x : X
Y : Type u_4
inst_3 : TopologicalSpace Y
g : X ≃ₜ Y
h : IsEvenlyCovered.{u_1, u_4, u_3} (X := Y) ((⇑g : (a : X) → Y) ∘ f : E → Y) ((g : (a : X) → Y) x : Y) I
h₁ :
  ∀ (x : E), f x = Function.comp.{u_1 + 1, u_4 + 1, u_2 + 1} (β := Y) (⇑g.symm : (a : Y) → X) ((⇑g : (a : X) → Y) ∘ f) x
⊢ f = Function.comp.{u_1 + 1, u_4 + 1, u_2 + 1} (β := Y) (⇑g.symm : (a : Y) → X) ((⇑g : (a : X) → Y) ∘ f)

Tactic:
try 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
I : Type u_3
inst_2 : TopologicalSpace I
x : X
Y : Type u_4
inst_3 : TopologicalSpace Y
g : X ≃ₜ Y
h : IsEvenlyCovered.{u_1, u_4, u_3} (X := Y) ((⇑g : (a : X) → Y) ∘ f : E → Y) ((g : (a : X) → Y) x : Y) I
x_1 : E
⊢ f x_1 = Function.comp.{u_1 + 1, u_4 + 1, u_2 + 1} (β := Y) (⇑g.symm : (a : Y) → X) ((⇑g : (a : X) → Y) ∘ f) x_1

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
I : Type u_3
inst_2 : TopologicalSpace I
x : X
Y : Type u_4
inst_3 : TopologicalSpace Y
g : X ≃ₜ Y
h : IsEvenlyCovered.{u_1, u_4, u_3} (X := Y) ((⇑g : (a : X) → Y) ∘ f : E → Y) ((g : (a : X) → Y) x : Y) I
⊢ x = (g.symm : (a : Y) → X) ((g : (a : X) → Y) x : Y)

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
inst_2 : IsEmpty E
⊢ IsCoveringMapOn f s

Tactic:
fun _ _ ↦ .to_isEvenlyCovered_preimage
  (.of_preimage_eq_empty Empty Filter.univ_mem <| Set.eq_empty_of_isEmpty _)

Premises used: IsEvenlyCovered.of_preimage_eq_empty, Set.univ, IsCoveringMapOn, Empty, Set.preimage, Filter.univ_mem, Set.eq_empty_of_isEmpty, 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
s : Set X
F : (↑s : Type u_2) → Type u_3
inst_2 : (x : (↑s : Type u_2)) → TopologicalSpace (F x)
hF : ∀ (x : (↑s : Type u_2)), DiscreteTopology.{u_3} (F x)
t :
  (x : (↑s : Type u_2)) →
    (↑x : X) ∈ Set.range f → { t : Trivialization.{u_2, u_3, u_1} (F x) f // (↑x : X) ∈ t.baseSet }
h : ∀ (x : (↑s : Type u_2)), (↑x : X) ∉ Set.range f → ∃ U ∈ 𝓝 (↑x : X), f ⁻¹' U = ∅
x : X
hx : x ∈ s
⊢ x ∈ s

Tactic:
hx
-- Module: Mathlib.Topology.Covering.Basic
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
s : Set X
F : (↑s : Type u_2) → Type u_3
inst_2 : (x : (↑s : Type u_2)) → TopologicalSpace (F x)
hF : ∀ (x : (↑s : Type u_2)), DiscreteTopology.{u_3} (F x)
t :
  (x : (↑s : Type u_2)) →
    (↑x : X) ∈ Set.range f → { t : Trivialization.{u_2, u_3, u_1} (F x) f // (↑x : X) ∈ t.baseSet }
h : ∀ (x : (↑s : Type u_2)), (↑x : X) ∉ Set.range f → ∃ U ∈ 𝓝 (↑x : X), f ⁻¹' U = ∅
x : X
hx : x ∈ s
lift : ∀ (x : { x : X // x ∈ s }), IsEvenlyCovered f (↑x : X) (↑(f ⁻¹' {(↑x : X)}) : Type u_1)
⊢ IsEvenlyCovered f x (↑(f ⁻¹' {x}) : Type u_1)

Tactic:
lift x to s using hx
-- Module: Mathlib.Topology.Covering.Basic
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
s : Set X
F : (↑s : Type u_2) → Type u_3
inst_2 : (x : (↑s : Type u_2)) → TopologicalSpace (F x)
hF : ∀ (x : (↑s : Type u_2)), DiscreteTopology.{u_3} (F x)
t :
  (x : (↑s : Type u_2)) →
    (↑x : X) ∈ Set.range f → { t : Trivialization.{u_2, u_3, u_1} (F x) f // (↑x : X) ∈ t.baseSet }
h : ∀ (x : (↑s : Type u_2)), (↑x : X) ∉ Set.range f → ∃ U ∈ 𝓝 (↑x : X), f ⁻¹' U = ∅
x : { x : X // x ∈ s }
pos : ∀ (hxf : (↑x : X) ∈ Set.range f), IsEvenlyCovered f (↑x : X) (↑(f ⁻¹' {(↑x : X)}) : Type u_1)
neg : ∀ (hxf : (↑x : X) ∉ Set.range f), IsEvenlyCovered f (↑x : X) (↑(f ⁻¹' {(↑x : X)}) : Type u_1)
⊢ IsEvenlyCovered f (↑x : X) (↑(f ⁻¹' {(↑x : X)}) : Type u_1)

Tactic:
by_cases hxf : x.1 ∈ Set.range f

Premises used: Set.range, 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
s : Set X
F : (↑s : Type u_2) → Type u_3
inst_2 : (x : (↑s : Type u_2)) → TopologicalSpace (F x)
hF : ∀ (x : (↑s : Type u_2)), DiscreteTopology.{u_3} (F x)
t :
  (x : (↑s : Type u_2)) →
    (↑x : X) ∈ Set.range f → { t : Trivialization.{u_2, u_3, u_1} (F x) f // (↑x : X) ∈ t.baseSet }
h : ∀ (x : (↑s : Type u_2)), (↑x : X) ∉ Set.range f → ∃ U ∈ 𝓝 (↑x : X), f ⁻¹' U = ∅
x : { x : X // x ∈ s }
hxf : (↑x : X) ∈ Set.range f
⊢ IsEvenlyCovered f (↑x : X) (↑(f ⁻¹' {(↑x : X)}) : Type u_1)

Tactic:
.to_isEvenlyCovered_preimage (.of_trivialization (t x hxf).2)

Premises used: IsEvenlyCovered.of_trivialization, IsEvenlyCovered.to_isEvenlyCovered_preimage, 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
s : Set X
F : (↑s : Type u_2) → Type u_3
inst_2 : (x : (↑s : Type u_2)) → TopologicalSpace (F x)
hF : ∀ (x : (↑s : Type u_2)), DiscreteTopology.{u_3} (F x)
t :
  (x : (↑s : Type u_2)) →
    (↑x : X) ∈ Set.range f → { t : Trivialization.{u_2, u_3, u_1} (F x) f // (↑x : X) ∈ t.baseSet }
h : ∀ (x : (↑s : Type u_2)), (↑x : X) ∉ Set.range f → ∃ U ∈ 𝓝 (↑x : X), f ⁻¹' U = ∅
x : { x : X // x ∈ s }
hxf : (↑x : X) ∈ Set.range f
⊢ IsEvenlyCovered f (↑x : X) (↑(f ⁻¹' {(↑x : X)}) : Type u_1)

Tactic:
exact .to_isEvenlyCovered_preimage (.of_trivialization (t x hxf).2)
-- 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
F : (↑s : Type u_2) → Type u_3
inst_2 : (x : (↑s : Type u_2)) → TopologicalSpace (F x)
hF : ∀ (x : (↑s : Type u_2)), DiscreteTopology.{u_3} (F x)
t :
  (x : (↑s : Type u_2)) →
    (↑x : X) ∈ Set.range f → { t : Trivialization.{u_2, u_3, u_1} (F x) f // (↑x : X) ∈ t.baseSet }
h : ∀ (x : (↑s : Type u_2)), (↑x : X) ∉ Set.range f → ∃ U ∈ 𝓝 (↑x : X), f ⁻¹' U = ∅
x : { x : X // x ∈ s }
hxf : (↑x : X) ∉ Set.range f
neg :
  ∀ (U : Set X) (hUx : U ∈ 𝓝 (↑x : X)) (hfU : f ⁻¹' U = ∅), IsEvenlyCovered f (↑x : X) (↑(f ⁻¹' {(↑x : X)}) : Type u_1)
⊢ IsEvenlyCovered f (↑x : X) (↑(f ⁻¹' {(↑x : X)}) : Type u_1)

Tactic:
have ⟨U, hUx, hfU⟩ := h x hxf
-- 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
F : (↑s : Type u_2) → Type u_3
inst_2 : (x : (↑s : Type u_2)) → TopologicalSpace (F x)
hF : ∀ (x : (↑s : Type u_2)), DiscreteTopology.{u_3} (F x)
t :
  (x : (↑s : Type u_2)) →
    (↑x : X) ∈ Set.range f → { t : Trivialization.{u_2, u_3, u_1} (F x) f // (↑x : X) ∈ t.baseSet }
h : ∀ (x : (↑s : Type u_2)), (↑x : X) ∉ Set.range f → ∃ U ∈ 𝓝 (↑x : X), f ⁻¹' U = ∅
x : { x : X // x ∈ s }
hxf : (↑x : X) ∉ Set.range f
U : Set X
hUx : U ∈ 𝓝 (↑x : X)
hfU : f ⁻¹' U = ∅
⊢ IsEvenlyCovered f (↑x : X) (↑(f ⁻¹' {(↑x : X)}) : Type u_1)

Tactic:
.to_isEvenlyCovered_preimage (.of_preimage_eq_empty Empty hUx hfU)

Premises used: IsEvenlyCovered.of_preimage_eq_empty, Empty, 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
s : Set X
F : (↑s : Type u_2) → Type u_3
inst_2 : (x : (↑s : Type u_2)) → TopologicalSpace (F x)
hF : ∀ (x : (↑s : Type u_2)), DiscreteTopology.{u_3} (F x)
t :
  (x : (↑s : Type u_2)) →
    (↑x : X) ∈ Set.range f → { t : Trivialization.{u_2, u_3, u_1} (F x) f // (↑x : X) ∈ t.baseSet }
h : ∀ (x : (↑s : Type u_2)), (↑x : X) ∉ Set.range f → ∃ U ∈ 𝓝 (↑x : X), f ⁻¹' U = ∅
x : { x : X // x ∈ s }
hxf : (↑x : X) ∉ Set.range f
U : Set X
hUx : U ∈ 𝓝 (↑x : X)
hfU : f ⁻¹' U = ∅
⊢ IsEvenlyCovered f (↑x : X) (↑(f ⁻¹' {(↑x : X)}) : Type u_1)

Tactic:
exact .to_isEvenlyCovered_preimage (.of_preimage_eq_empty Empty hUx hfU)
-- 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
F : (↑s : Type u_2) → Type u_3
inst_2 : (x : (↑s : Type u_2)) → TopologicalSpace (F x)
hF : ∀ (x : (↑s : Type u_2)), DiscreteTopology.{u_3} (F x)
e : (x : (↑s : Type u_2)) → Trivialization.{u_2, u_3, u_1} (F x) f
h : ∀ (x : (↑s : Type u_2)), (↑x : X) ∈ (e x).baseSet
inl : IsEmpty E → IsCoveringMapOn f s
inr : Nonempty E → IsCoveringMapOn f s
⊢ IsCoveringMapOn f s

Tactic:
cases isEmpty_or_nonempty E

Premises used: isEmpty_or_nonempty
-- 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
F : (↑s : Type u_2) → Type u_3
inst_2 : (x : (↑s : Type u_2)) → TopologicalSpace (F x)
hF : ∀ (x : (↑s : Type u_2)), DiscreteTopology.{u_3} (F x)
e : (x : (↑s : Type u_2)) → Trivialization.{u_2, u_3, u_1} (F x) f
h : ∀ (x : (↑s : Type u_2)), (↑x : X) ∈ (e x).baseSet
h_1 : IsEmpty E
⊢ IsCoveringMapOn f s

Tactic:
.of_isEmpty _ _

Premises used: IsCoveringMapOn.of_isEmpty
-- 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
F : (↑s : Type u_2) → Type u_3
inst_2 : (x : (↑s : Type u_2)) → TopologicalSpace (F x)
hF : ∀ (x : (↑s : Type u_2)), DiscreteTopology.{u_3} (F x)
e : (x : (↑s : Type u_2)) → Trivialization.{u_2, u_3, u_1} (F x) f
h : ∀ (x : (↑s : Type u_2)), (↑x : X) ∈ (e x).baseSet
h_1 : IsEmpty E
⊢ IsCoveringMapOn f s

Tactic:
exact .of_isEmpty _ _
-- 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
F : (↑s : Type u_2) → Type u_3
inst_2 : (x : (↑s : Type u_2)) → TopologicalSpace (F x)
hF : ∀ (x : (↑s : Type u_2)), DiscreteTopology.{u_3} (F x)
e : (x : (↑s : Type u_2)) → Trivialization.{u_2, u_3, u_1} (F x) f
h : ∀ (x : (↑s : Type u_2)), (↑x : X) ∈ (e x).baseSet
h_1 : Nonempty E
⊢ IsCoveringMapOn f s

Tactic:
.mk' _ _ _ (fun x _ ↦ ⟨e x, h x⟩) fun x hx ↦ (hx ?_).elim

Premises used: False.elim, Subtype.mk, IsCoveringMapOn.mk'
-- 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
F : (↑s : Type u_2) → Type u_3
inst_2 : (x : (↑s : Type u_2)) → TopologicalSpace (F x)
hF : ∀ (x : (↑s : Type u_2)), DiscreteTopology.{u_3} (F x)
e : (x : (↑s : Type u_2)) → Trivialization.{u_2, u_3, u_1} (F x) f
h : ∀ (x : (↑s : Type u_2)), (↑x : X) ∈ (e x).baseSet
h_1 : Nonempty E
inr : ∀ (x : (↑s : Type u_2)) (hx : (↑x : X) ∉ Set.range f), (↑x : X) ∈ Set.range f
⊢ IsCoveringMapOn f s

Tactic:
refine .mk' _ _ _ (fun x _ ↦ ⟨e x, h x⟩) fun x hx ↦ (hx ?_).elim
-- 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
F : (↑s : Type u_2) → Type u_3
inst_2 : (x : (↑s : Type u_2)) → TopologicalSpace (F x)
hF : ∀ (x : (↑s : Type u_2)), DiscreteTopology.{u_3} (F x)
e : (x : (↑s : Type u_2)) → Trivialization.{u_2, u_3, u_1} (F x) f
h : ∀ (x : (↑s : Type u_2)), (↑x : X) ∈ (e x).baseSet
h_1 : Nonempty E
x : (↑s : Type u_2)
hx : (↑x : X) ∉ Set.range f
⊢ (↑x : X) ∈ Set.range f

Tactic:
⟨(e x).invFun (x, (e x <| Classical.arbitrary E).2), (e x).proj_symm_apply' (h x)⟩

Premises used: Bundle.Trivialization.toFun', Set.Mem, setOf, Prod.mk, Exists.intro, Classical.arbitrary, PartialEquiv.invFun, Set.range, OpenPartialHomeomorph.toPartialEquiv, Subtype.val, Prod.snd, Bundle.Trivialization.proj_symm_apply', 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
s : Set X
F : (↑s : Type u_2) → Type u_3
inst_2 : (x : (↑s : Type u_2)) → TopologicalSpace (F x)
hF : ∀ (x : (↑s : Type u_2)), DiscreteTopology.{u_3} (F x)
e : (x : (↑s : Type u_2)) → Trivialization.{u_2, u_3, u_1} (F x) f
h : ∀ (x : (↑s : Type u_2)), (↑x : X) ∈ (e x).baseSet
h_1 : Nonempty E
x : (↑s : Type u_2)
hx : (↑x : X) ∉ Set.range f
⊢ (↑x : X) ∈ Set.range f

Tactic:
exact ⟨(e x).invFun (x, (e x <| Classical.arbitrary E).2), (e x).proj_symm_apply' (h x)⟩
-- 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 t : Set X
hf : IsCoveringMapOn f s
ht : t ⊆ s
⊢ IsCoveringMapOn f t

Tactic:
fun x hx ↦ hf x (ht hx)

Premises used: 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
s : Set X
hf : IsCoveringMapOn f s
x : E
hx : f x ∈ s
⊢ ContinuousAt f x

Tactic:
(hf (f x) hx).continuousAt

Premises used: IsEvenlyCovered.continuousAt
-- 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
⊢ ContinuousOn f (f ⁻¹' s)

Tactic:
continuousOn_of_forall_continuousAt fun _ ↦ hf.continuousAt

Premises used: continuousOn_of_forall_continuousAt, IsCoveringMapOn.continuousAt
-- 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
⊢ IsLocalHomeomorphOn f (f ⁻¹' s)

Tactic:
IsLocalHomeomorphOn.mk f (f ⁻¹' s) fun x hx ↦ ?_

Premises used: IsLocalHomeomorphOn.mk, Set.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
s : Set X
hf : IsCoveringMapOn f s
refine :
  ∀ (x : E) (hx : x ∈ f ⁻¹' s), ∃ (e : OpenPartialHomeomorph E X), x ∈ e.source ∧ Set.EqOn f (↑e : E → X) e.source
⊢ IsLocalHomeomorphOn f (f ⁻¹' s)

Tactic:
refine IsLocalHomeomorphOn.mk f (f ⁻¹' s) fun x hx ↦ ?_

Premises used: IsLocalHomeomorphOn.mk, Set.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
s : Set X
hf : IsCoveringMapOn f s
x : E
hx : x ∈ f ⁻¹' s
⊢ Nonempty.{u_1 + 1} (↑(f ⁻¹' {f x}) : Type u_1)

Tactic:
have : Nonempty (f ⁻¹' {f x}) := ⟨⟨x, 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
s : Set X
hf : IsCoveringMapOn f s
x : E
hx : x ∈ f ⁻¹' s
this : Nonempty.{u_1 + 1} (↑(f ⁻¹' {f x}) : Type u_1)
e : Trivialization (↑(f ⁻¹' {f x}) : Type u_1) f := ⋯.toTrivialization
⊢ f x ∈ ⋯.toTrivialization.baseSet

Tactic:
have h := (hf (f x) hx).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
s : Set X
hf : IsCoveringMapOn f s
x : E
hx : x ∈ f ⁻¹' s
this : Nonempty.{u_1 + 1} (↑(f ⁻¹' {f x}) : Type u_1)
e : Trivialization (↑(f ⁻¹' {f x}) : Type u_1) f := ⋯.toTrivialization
h : f x ∈ ⋯.toTrivialization.baseSet
he : x ∈ e.source := ⋯
⊢ ContinuousOn (Y := Prod.{u_2, u_1} X (↑(f ⁻¹' {f x}) : Type u_1))
    (fun (p : X) ↦ (p, Subtype.mk (p := fun (x_1 : E) ↦ x_1 ∈ f ⁻¹' {f x}) x ⋯)) e.baseSet

Tactic:
fun_prop
-- 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
x : E
hx : x ∈ f ⁻¹' s
this : Nonempty.{u_1 + 1} (↑(f ⁻¹' {f x}) : Type u_1)
e : Trivialization (↑(f ⁻¹' {f x}) : Type u_1) f := ⋯.toTrivialization
h : f x ∈ ⋯.toTrivialization.baseSet
he : x ∈ e.source := ⋯
rwa : ((↑e.toOpenPartialHomeomorph : E → X × (↑(f ⁻¹' {f x}) : Type u_1)) x).1 ∈ e.baseSet
rwa₁ rwa₂ rwa₃ rwa₄ : f x ∈ e.baseSet
⊢ ((↑e.symm.symm : E → X × (↑(f ⁻¹' {f x}) : Type u_1)) x).1 ∈ e.baseSet

Tactic:
rwa [e.toOpenPartialHomeomorph.symm_symm, e.proj_toFun x he]

Premises used: OpenPartialHomeomorph.symm_symm, Bundle.Trivialization.toOpenPartialHomeomorph, 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
s : Set X
hf : IsCoveringMapOn f s
x : E
hx : x ∈ f ⁻¹' s
this : Nonempty.{u_1 + 1} (↑(f ⁻¹' {f x}) : Type u_1)
e : Trivialization (↑(f ⁻¹' {f x}) : Type u_1) f := ⋯.toTrivialization
h : f x ∈ ⋯.toTrivialization.baseSet
he : x ∈ e.source := ⋯
⊢ ∃ (e : OpenPartialHomeomorph E X), x ∈ e.source ∧ Set.EqOn f (↑e : E → X) e.source

Tactic:
refine
    ⟨e.toOpenPartialHomeomorph.trans
        { toFun := fun p => p.1
          invFun := fun p => ⟨p, x, rfl⟩
          source := e.baseSet ×ˢ ({⟨x, rfl⟩} : Set (f ⁻¹' {f x}))
          target := e.baseSet
          open_source :=
            e.open_baseSet.prod (discreteTopology_iff_isOpen_singleton.1 (hf (f x) hx).1 ⟨x, rfl⟩)
          open_target := e.open_baseSet
          map_source' := fun p => And.left
          map_target' := fun p hp => ⟨hp, rfl⟩
          left_inv' := fun p hp => Prod.ext rfl hp.2.symm
          right_inv' := fun p _ => rfl
          continuousOn_toFun := continuousOn_fst
          continuousOn_invFun := by fun_prop },
      ⟨he, by rwa [e.toOpenPartialHomeomorph.symm_symm, e.proj_toFun x he],
        (hf (f x) hx).toTrivialization_apply⟩,
      fun p h => (e.proj_toFun p h.1).symm⟩
-- 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
t : Set X
⊢ IsCoveringMapOn (t.restrictPreimage f) (Subtype.val (p := fun (x : X) ↦ x ∈ t) ⁻¹' s)

Tactic:
fun x hs ↦ ((hf x hs).restrictPreimage t x.2).to_isEvenlyCovered_preimage

Premises used: Set.Mem, IsCoveringMapOn, IsEvenlyCovered.restrictPreimage, Subtype.val, IsEvenlyCovered.to_isEvenlyCovered_preimage, 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
s : Set X
hf : IsCoveringMapOn f s
E' : Type u_3
inst_2 : TopologicalSpace E'
g : E' ≃ₜ E
⊢ IsCoveringMapOn.{u_3, u_2} (E := E') (f ∘ (⇑g : (a : E') → E)) s

Tactic:
fun x hx ↦ ((hf x hx).comp_homeomorph _).to_isEvenlyCovered_preimage

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

Tactic:
h.comp_homeomorph g.symm

Premises used: IsCoveringMapOn.comp_homeomorph, Homeomorph.symm
-- 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
E' : Type u_3
inst_2 : TopologicalSpace E'
g : E' ≃ₜ E
h : IsCoveringMapOn.{u_3, u_2} (E := E') (f ∘ (⇑g : (a : E') → E)) s
h₁ : f = Function.comp.{u_1 + 1, u_3 + 1, u_2 + 1} (β := E') (f ∘ (⇑g : (a : E') → E)) (⇑g.symm : (a : E) → E')
⊢ IsCoveringMapOn f s

Tactic:
convert! h.comp_homeomorph g.symm

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

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

Tactic:
fun y hy ↦ (g.apply_symm_apply y ▸ (hf _ hy).homeomorph_comp _).to_isEvenlyCovered_preimage

Premises used: 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
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)
⊢ IsCoveringMapOn.{u_1, u_2} (X := X)
    (Function.comp.{u_1 + 1, u_3 + 1, u_2 + 1} (β := Y) (⇑g.symm : (a : Y) → X) ((⇑g : (a : X) → Y) ∘ f))
    (Set.preimage.{u_2, u_3} (β := Y) (⇑g.symm.symm : (a : X) → Y) ((⇑g.symm : (a : Y) → X) ⁻¹' s))

Tactic:
h.homeomorph_comp g.symm

Premises used: Homeomorph.symm, IsCoveringMapOn.homeomorph_comp
-- 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₁ : f = Function.comp.{u_1 + 1, u_3 + 1, u_2 + 1} (β := Y) (⇑g.symm : (a : Y) → X) ((⇑g : (a : X) → Y) ∘ f)
h₂ : s = Set.preimage.{u_2, u_3} (β := Y) (⇑g.symm.symm : (a : X) → Y) ((⇑g.symm : (a : Y) → X) ⁻¹' s)
⊢ IsCoveringMapOn f s

Tactic:
convert! h.homeomorph_comp g.symm

Premises used: Homeomorph.symm, IsCoveringMapOn.homeomorph_comp