awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Covering.Basic
Goal:
E : Type u_1
X : Type u_2
inst_1 : TopologicalSpace E
inst_2 : TopologicalSpace X
f : E → X
s : Set X
I : Type u_3
inst_3 : TopologicalSpace I
x : X
hxs : x ∈ s
h : IsEvenlyCovered f x I
inst : DiscreteTopology I
U : Set X
hxU : x ∈ U
hU : IsOpen[inst_2] U
hfU : IsOpen[inst_1] (f ⁻¹' U)
H : (↑(f ⁻¹' U) : Type u_1) ≃ₜ Prod.{u_2, u_3} (↑U : Type u_2) I
hH :
  ∀ (x : (↑(f ⁻¹' U) : Type u_1)), (↑((H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × I) x).1 : X) = f (↑x : E)
x_1 : (↑(s.restrictPreimage f ⁻¹' Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' U) : Type u_1)
⊢ (↑(↑(({
                    toFun :=
                      fun (e : (↑(s.restrictPreimage f ⁻¹' Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' U) : Type u_1)) ↦
                      (Subtype.mk (p := fun (x : (↑s : Type u_2)) ↦
                          Membership.mem (γ := Set (↑s : Type u_2)) (Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' U) x)
                          (Subtype.mk (p := fun (x : X) ↦ x ∈ s)
                            (↑((H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × I)
                                    (Subtype.mk (p := fun (x : E) ↦ x ∈ f ⁻¹' U) (↑(↑e : (↑(f ⁻¹' s) : Type u_1)) : E)
                                      ⋯)).1 :
                              X)
                            ⋯)
                          ⋯,
                        ((H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × I)
                            (Subtype.mk (p := fun (x : E) ↦ x ∈ f ⁻¹' U) (↑(↑e : (↑(f ⁻¹' s) : Type u_1)) : E) ⋯)).2),
                    invFun := fun (x : Prod.{u_2, u_3} (↑(Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' U) : Type u_2) I) ↦
                      Subtype.mk (p := fun (x : (↑(f ⁻¹' s) : Type u_1)) ↦
                        x ∈ s.restrictPreimage f ⁻¹' Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' U)
                        (Subtype.mk (p := fun (x : E) ↦ x ∈ f ⁻¹' s)
                          (↑((H.symm : (a : (↑U : Type u_2) × I) → (↑(f ⁻¹' U) : Type u_1))
                                (Subtype.mk (p := fun (x : X) ↦ x ∈ U) (↑(↑x.1 : (↑s : Type u_2)) : X) ⋯, x.2)) :
                            E)
                          ⋯)
                        ⋯,
                    left_inv := ⋯, right_inv := ⋯, continuous_toFun := ⋯, continuous_invFun := ⋯ } :
                  (a : (↑(s.restrictPreimage f ⁻¹' Subtype.val ⁻¹' U) : Type u_1)) →
                    (↑(Subtype.val ⁻¹' U) : Type u_2) × I)
                x_1).1 :
          (↑s : Type u_2)) :
      X) =
    (↑(s.restrictPreimage f (↑x_1 : (↑(f ⁻¹' s) : Type u_1))) : X)

Tactic:
apply hH
-- Module: Mathlib.Topology.Covering.Basic
Goal:
E : Type u_1
X : Type u_2
inst_1 : TopologicalSpace E
inst_2 : TopologicalSpace X
s : Set X
I : Type u_3
inst_3 : TopologicalSpace I
hs : IsOpen[inst_2] s
x : (↑s : Type u_2)
f : E → (↑s : Type u_2)
h : IsEvenlyCovered f x I
inst : DiscreteTopology I
U : Set (↑s : Type u_2)
hxU : x ∈ U
hU : IsOpen[instTopologicalSpaceSubtype] U
hfU : IsOpen[inst_1] (f ⁻¹' U)
H : (↑(f ⁻¹' U) : Type u_1) ≃ₜ Prod.{u_2, u_3} (↑U : Type u_2) I
hH :
  ∀ (x : (↑(f ⁻¹' U) : Type u_1)),
    (↑((H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × I) x).1 : (↑s : Type u_2)) = f (↑x : E)
h₁ :
  ∀ (x : E),
    x ∈ Subtype.val (p := fun (x : X) ↦ x ∈ s) ∘ f ⁻¹' Subtype.val (p := fun (x : X) ↦ x ∈ s) '' U ↔ x ∈ f ⁻¹' U
⊢ Subtype.val (p := fun (x : X) ↦ x ∈ s) ∘ f ⁻¹' Subtype.val (p := fun (x : X) ↦ x ∈ s) '' U = f ⁻¹' U

Tactic:
ext
-- Module: Mathlib.Topology.Covering.Basic
Goal:
E : Type u_1
X : Type u_2
inst_1 : TopologicalSpace E
inst_2 : TopologicalSpace X
s : Set X
I : Type u_3
inst_3 : TopologicalSpace I
hs : IsOpen[inst_2] s
x : (↑s : Type u_2)
f : E → (↑s : Type u_2)
h : IsEvenlyCovered f x I
inst : DiscreteTopology I
U : Set (↑s : Type u_2)
hxU : x ∈ U
hU : IsOpen[instTopologicalSpaceSubtype] U
hfU : IsOpen[inst_1] (f ⁻¹' U)
H : (↑(f ⁻¹' U) : Type u_1) ≃ₜ Prod.{u_2, u_3} (↑U : Type u_2) I
hH :
  ∀ (x : (↑(f ⁻¹' U) : Type u_1)),
    (↑((H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × I) x).1 : (↑s : Type u_2)) = f (↑x : E)
x_1 : E
⊢ x_1 ∈ Subtype.val (p := fun (x : X) ↦ x ∈ s) ∘ f ⁻¹' Subtype.val (p := fun (x : X) ↦ x ∈ s) '' U ↔ x_1 ∈ f ⁻¹' U

Tactic:
simp
-- Module: Mathlib.Topology.Covering.Basic
Goal:
E : Type u_1
X : Type u_2
inst_1 : TopologicalSpace E
inst_2 : TopologicalSpace X
s : Set X
I : Type u_3
inst_3 : TopologicalSpace I
hs : IsOpen[inst_2] s
x : (↑s : Type u_2)
f : E → (↑s : Type u_2)
h : IsEvenlyCovered f x I
inst : DiscreteTopology I
U : Set (↑s : Type u_2)
hxU : x ∈ U
hU : IsOpen[instTopologicalSpaceSubtype] U
hfU : IsOpen[inst_1] (f ⁻¹' U)
H : (↑(f ⁻¹' U) : Type u_1) ≃ₜ Prod.{u_2, u_3} (↑U : Type u_2) I
hH :
  ∀ (x : (↑(f ⁻¹' U) : Type u_1)),
    (↑((H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × I) x).1 : (↑s : Type u_2)) = f (↑x : E)
this : Subtype.val (p := fun (x : X) ↦ x ∈ s) ∘ f ⁻¹' Subtype.val (p := fun (x : X) ↦ x ∈ s) '' U = f ⁻¹' U
rwa rwa₁ rwa₂ rwa₃ : IsOpen[inst_1] (f ⁻¹' U)
⊢ IsOpen[inst_1] (Subtype.val (p := fun (x : X) ↦ x ∈ s) ∘ f ⁻¹' Subtype.val (p := fun (x : X) ↦ x ∈ s) '' U)

Tactic:
rwa [this]
-- Module: Mathlib.Topology.Covering.Basic
Goal:
E : Type u_1
X : Type u_2
inst_1 : TopologicalSpace E
inst_2 : TopologicalSpace X
f : E → X
s : Set X
I : Type u_3
inst_3 : TopologicalSpace I
hs : IsOpen[inst_2] s
hfs : IsOpen[inst_1] (f ⁻¹' s)
x : X
hx : x ∈ s
h : IsEvenlyCovered (fun (e : (↑(f ⁻¹' s) : Type u_1)) ↦ f (↑e : E)) x I
inst : DiscreteTopology I
U : Set X
hxU : x ∈ U
hU : IsOpen[inst_2] U
hfU : IsOpen[instTopologicalSpaceSubtype] ((fun (e : (↑(f ⁻¹' s) : Type u_1)) ↦ f (↑e : E)) ⁻¹' U)
H : (↑((fun (e : (↑(f ⁻¹' s) : Type u_1)) ↦ f (↑e : E)) ⁻¹' U) : Type u_1) ≃ₜ Prod.{u_2, u_3} (↑U : Type u_2) I
hH :
  ∀ (x : (↑((fun (e : (↑(f ⁻¹' s) : Type u_1)) ↦ f (↑e : E)) ⁻¹' U) : Type u_1)),
    Eq.{u_2 + 1} (α := X)
      (↑((H : (a : (↑((fun (e : (↑(f ⁻¹' s) : Type u_1)) ↦ f (↑e : E)) ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × I) x).1 :
        X)
      ((fun (e : (↑(f ⁻¹' s) : Type u_1)) ↦ f (↑e : E)) (↑x : (↑(f ⁻¹' s) : Type u_1)))
h_1 : Nonempty I
y : X
hy : y ∈ U
⊢ f
      (↑(↑((H.symm : (a : (↑U : Type u_2) × I) → (↑((fun (e : (↑(f ⁻¹' s) : Type u_1)) ↦ f (↑e : E)) ⁻¹' U) : Type u_1))
                (Subtype.mk (p := fun (x : X) ↦ x ∈ U) y hy, Classical.arbitrary I)) :
            (↑(f ⁻¹' s) : Type u_1)) :
        E) ∈
    s

Tactic:
Set.mem_preimage.mp (H.symm (⟨y, hy⟩, Classical.arbitrary I)).1.2

Premises used: Prod.mk, Subtype.mk, Homeomorph.symm, Classical.arbitrary, Iff.mp, Subtype.val, DFunLike.coe, Set.mem_preimage, Subtype.property
-- Module: Mathlib.Topology.Covering.Basic
Goal:
E : Type u_1
X : Type u_2
inst_1 : TopologicalSpace E
inst_2 : TopologicalSpace X
f : E → X
s : Set X
I : Type u_3
inst_3 : TopologicalSpace I
hs : IsOpen[inst_2] s
hfs : IsOpen[inst_1] (f ⁻¹' s)
x : X
hx : x ∈ s
h : IsEvenlyCovered (fun (e : (↑(f ⁻¹' s) : Type u_1)) ↦ f (↑e : E)) x I
inst : DiscreteTopology I
U : Set X
hxU : x ∈ U
hU : IsOpen[inst_2] U
hfU : IsOpen[instTopologicalSpaceSubtype] ((fun (e : (↑(f ⁻¹' s) : Type u_1)) ↦ f (↑e : E)) ⁻¹' U)
H : (↑((fun (e : (↑(f ⁻¹' s) : Type u_1)) ↦ f (↑e : E)) ⁻¹' U) : Type u_1) ≃ₜ Prod.{u_2, u_3} (↑U : Type u_2) I
hH :
  ∀ (x : (↑((fun (e : (↑(f ⁻¹' s) : Type u_1)) ↦ f (↑e : E)) ⁻¹' U) : Type u_1)),
    Eq.{u_2 + 1} (α := X)
      (↑((H : (a : (↑((fun (e : (↑(f ⁻¹' s) : Type u_1)) ↦ f (↑e : E)) ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × I) x).1 :
        X)
      ((fun (e : (↑(f ⁻¹' s) : Type u_1)) ↦ f (↑e : E)) (↑x : (↑(f ⁻¹' s) : Type u_1)))
h_1 : Nonempty I
y : X
hy : y ∈ U
h₁ :
  y =
    f
      (↑(↑((H.symm : (a : (↑U : Type u_2) × I) → (↑((fun (e : (↑(f ⁻¹' s) : Type u_1)) ↦ f (↑e : E)) ⁻¹' U) : Type u_1))
                (Subtype.mk (p := fun (x : X) ↦ x ∈ U) y hy, Classical.arbitrary I)) :
            (↑(f ⁻¹' s) : Type u_1)) :
        E)
⊢ y ∈ s

Tactic:
convert! Set.mem_preimage.mp (H.symm (⟨y, hy⟩, Classical.arbitrary I)).1.2

Premises used: Prod.mk, Subtype.mk, Homeomorph.symm, Classical.arbitrary, Iff.mp, Subtype.val, DFunLike.coe, Set.mem_preimage, Subtype.property
-- Module: Mathlib.Topology.Covering.Basic
Goal:
E : Type u_1
X : Type u_2
inst_1 : TopologicalSpace E
inst_2 : TopologicalSpace X
f : E → X
s : Set X
I : Type u_3
inst_3 : TopologicalSpace I
hs : IsOpen[inst_2] s
hfs : IsOpen[inst_1] (f ⁻¹' s)
x : X
hx : x ∈ s
h : IsEvenlyCovered (fun (e : (↑(f ⁻¹' s) : Type u_1)) ↦ f (↑e : E)) x I
inst : DiscreteTopology I
U : Set X
hxU : x ∈ U
hU : IsOpen[inst_2] U
hfU : IsOpen[instTopologicalSpaceSubtype] ((fun (e : (↑(f ⁻¹' s) : Type u_1)) ↦ f (↑e : E)) ⁻¹' U)
H : (↑((fun (e : (↑(f ⁻¹' s) : Type u_1)) ↦ f (↑e : E)) ⁻¹' U) : Type u_1) ≃ₜ Prod.{u_2, u_3} (↑U : Type u_2) I
hH :
  ∀ (x : (↑((fun (e : (↑(f ⁻¹' s) : Type u_1)) ↦ f (↑e : E)) ⁻¹' U) : Type u_1)),
    Eq.{u_2 + 1} (α := X)
      (↑((H : (a : (↑((fun (e : (↑(f ⁻¹' s) : Type u_1)) ↦ f (↑e : E)) ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × I) x).1 :
        X)
      ((fun (e : (↑(f ⁻¹' s) : Type u_1)) ↦ f (↑e : E)) (↑x : (↑(f ⁻¹' s) : Type u_1)))
h_1 : Nonempty I
y : X
hy : y ∈ U
⊢ y =
    f
      (↑(↑((H.symm : (a : (↑U : Type u_2) × I) → (↑((fun (e : (↑(f ⁻¹' s) : Type u_1)) ↦ f (↑e : E)) ⁻¹' U) : Type u_1))
                (Subtype.mk (p := fun (x : X) ↦ x ∈ U) y hy, Classical.arbitrary I)) :
            (↑(f ⁻¹' s) : Type u_1)) :
        E)

Tactic:
simp [← hH]
-- Module: Mathlib.Topology.Covering.Basic
Goal:
E : Type u_1
X : Type u_2
inst_1 : TopologicalSpace E
inst_2 : TopologicalSpace X
f : E → X
s : Set X
I : Type u_3
inst_3 : TopologicalSpace I
hs : IsOpen[inst_2] s
hfs : IsOpen[inst_1] (f ⁻¹' s)
x : X
hx : x ∈ s
h : IsEvenlyCovered (fun (e : (↑(f ⁻¹' s) : Type u_1)) ↦ f (↑e : E)) x I
inst : DiscreteTopology I
U : Set X
hxU : x ∈ U
hU : IsOpen[inst_2] U
hfU : IsOpen[instTopologicalSpaceSubtype] ((fun (e : (↑(f ⁻¹' s) : Type u_1)) ↦ f (↑e : E)) ⁻¹' U)
H : (↑((fun (e : (↑(f ⁻¹' s) : Type u_1)) ↦ f (↑e : E)) ⁻¹' U) : Type u_1) ≃ₜ Prod.{u_2, u_3} (↑U : Type u_2) I
hH :
  ∀ (x : (↑((fun (e : (↑(f ⁻¹' s) : Type u_1)) ↦ f (↑e : E)) ⁻¹' U) : Type u_1)),
    Eq.{u_2 + 1} (α := X)
      (↑((H : (a : (↑((fun (e : (↑(f ⁻¹' s) : Type u_1)) ↦ f (↑e : E)) ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × I) x).1 :
        X)
      ((fun (e : (↑(f ⁻¹' s) : Type u_1)) ↦ f (↑e : E)) (↑x : (↑(f ⁻¹' s) : Type u_1)))
h_1 : Nonempty I
hUs : U ⊆ s
h₁ :
  ∀ (x : E),
    Membership.mem (γ := Set E)
        (Set.image (α := { x : E // x ∈ f ⁻¹' s }) (Subtype.val (p := fun (x : E) ↦ x ∈ f ⁻¹' s))
          ((fun (e : (↑(f ⁻¹' s) : Type u_1)) ↦ f (↑e : E)) ⁻¹' U))
        x ↔
      x ∈ f ⁻¹' U
⊢ Set.image (α := { x : E // x ∈ f ⁻¹' s }) (Subtype.val (p := fun (x : E) ↦ x ∈ f ⁻¹' s))
      ((fun (e : (↑(f ⁻¹' s) : Type u_1)) ↦ f (↑e : E)) ⁻¹' U) =
    f ⁻¹' U

Tactic:
ext
-- Module: Mathlib.Topology.Covering.Basic
Goal:
E : Type u_1
X : Type u_2
inst_1 : TopologicalSpace E
inst_2 : TopologicalSpace X
f : E → X
s : Set X
I : Type u_3
inst_3 : TopologicalSpace I
hs : IsOpen[inst_2] s
hfs : IsOpen[inst_1] (f ⁻¹' s)
x : X
hx : x ∈ s
h : IsEvenlyCovered (fun (e : (↑(f ⁻¹' s) : Type u_1)) ↦ f (↑e : E)) x I
inst : DiscreteTopology I
U : Set X
hxU : x ∈ U
hU : IsOpen[inst_2] U
hfU : IsOpen[instTopologicalSpaceSubtype] ((fun (e : (↑(f ⁻¹' s) : Type u_1)) ↦ f (↑e : E)) ⁻¹' U)
H : (↑((fun (e : (↑(f ⁻¹' s) : Type u_1)) ↦ f (↑e : E)) ⁻¹' U) : Type u_1) ≃ₜ Prod.{u_2, u_3} (↑U : Type u_2) I
hH :
  ∀ (x : (↑((fun (e : (↑(f ⁻¹' s) : Type u_1)) ↦ f (↑e : E)) ⁻¹' U) : Type u_1)),
    Eq.{u_2 + 1} (α := X)
      (↑((H : (a : (↑((fun (e : (↑(f ⁻¹' s) : Type u_1)) ↦ f (↑e : E)) ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × I) x).1 :
        X)
      ((fun (e : (↑(f ⁻¹' s) : Type u_1)) ↦ f (↑e : E)) (↑x : (↑(f ⁻¹' s) : Type u_1)))
h_1 : Nonempty I
hUs : U ⊆ s
x_1 : E
⊢ Membership.mem (γ := Set E)
      (Set.image (α := { x : E // x ∈ f ⁻¹' s }) (Subtype.val (p := fun (x : E) ↦ x ∈ f ⁻¹' s))
        ((fun (e : (↑(f ⁻¹' s) : Type u_1)) ↦ f (↑e : E)) ⁻¹' U))
      x_1 ↔
    x_1 ∈ f ⁻¹' U

Tactic:
simpa using @hUs _
-- Module: Mathlib.Topology.Covering.Basic
Goal:
E : Type u_1
X : Type u_2
inst_1 : TopologicalSpace E
inst_2 : TopologicalSpace X
f : E → X
s : Set X
I : Type u_3
inst_3 : TopologicalSpace I
hs : IsOpen[inst_2] s
hfs : IsOpen[inst_1] (f ⁻¹' s)
x_1 : X
hx : x_1 ∈ s
h : IsEvenlyCovered (fun (e : (↑(f ⁻¹' s) : Type u_1)) ↦ f (↑e : E)) x_1 I
inst : DiscreteTopology I
U : Set X
hxU : x_1 ∈ U
hU : IsOpen[inst_2] U
hfU : IsOpen[instTopologicalSpaceSubtype] ((fun (e : (↑(f ⁻¹' s) : Type u_1)) ↦ f (↑e : E)) ⁻¹' U)
H : (↑((fun (e : (↑(f ⁻¹' s) : Type u_1)) ↦ f (↑e : E)) ⁻¹' U) : Type u_1) ≃ₜ Prod.{u_2, u_3} (↑U : Type u_2) I
hH :
  ∀ (x : (↑((fun (e : (↑(f ⁻¹' s) : Type u_1)) ↦ f (↑e : E)) ⁻¹' U) : Type u_1)),
    Eq.{u_2 + 1} (α := X)
      (↑((H : (a : (↑((fun (e : (↑(f ⁻¹' s) : Type u_1)) ↦ f (↑e : E)) ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × I) x).1 :
        X)
      ((fun (e : (↑(f ⁻¹' s) : Type u_1)) ↦ f (↑e : E)) (↑x : (↑(f ⁻¹' s) : Type u_1)))
h_1 : Nonempty I
hUs : U ⊆ s
this :
  Set.image (α := { x : E // x ∈ f ⁻¹' s }) (Subtype.val (p := fun (x : E) ↦ x ∈ f ⁻¹' s))
      ((fun (e : (↑(f ⁻¹' s) : Type u_1)) ↦ f (↑e : E)) ⁻¹' U) =
    f ⁻¹' U
x : (↑(f ⁻¹' U) : Type u_1)
dsimp :
  (↑((H : (a : (↑((fun (e : (↑(f ⁻¹' s) : Type u_1)) ↦ f (↑e : E)) ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × I)
            ((Homeomorph.symm (IsEmbedding.homeomorphImage ⋯ ((fun (e : (↑(f ⁻¹' s) : Type u_1)) ↦ f (↑e : E)) ⁻¹' U)) :
                (a : (↑(Subtype.val '' (fun (e : (↑(f ⁻¹' s) : Type u_1)) ↦ f (↑e : E)) ⁻¹' U) : Type u_1)) →
                  (↑((fun (e : (↑(f ⁻¹' s) : Type u_1)) ↦ f (↑e : E)) ⁻¹' U) : Type u_1))
              ((Homeomorph.symm
                    (Homeomorph.setCongr (s :=
                      Set.image (α := { x : E // x ∈ f ⁻¹' s }) (Subtype.val (p := fun (x : E) ↦ x ∈ f ⁻¹' s))
                        ((fun (e : (↑(f ⁻¹' s) : Type u_1)) ↦ f (↑e : E)) ⁻¹' U))
                      (t := f ⁻¹' U) this) :
                  (a : (↑(f ⁻¹' U) : Type u_1)) →
                    (↑(Subtype.val '' (fun (e : (↑(f ⁻¹' s) : Type u_1)) ↦ f (↑e : E)) ⁻¹' U) : Type u_1))
                x))).1 :
      X) =
    f (↑x : E)
⊢ (↑((Homeomorph.trans
                (Homeomorph.symm
                  (Homeomorph.trans
                    (IsEmbedding.homeomorphImage ⋯ ((fun (e : (↑(f ⁻¹' s) : Type u_1)) ↦ f (↑e : E)) ⁻¹' U))
                    (Homeomorph.setCongr (s :=
                      Set.image (α := { x : E // x ∈ f ⁻¹' s }) (Subtype.val (p := fun (x : E) ↦ x ∈ f ⁻¹' s))
                        ((fun (e : (↑(f ⁻¹' s) : Type u_1)) ↦ f (↑e : E)) ⁻¹' U))
                      (t := f ⁻¹' U) this)))
                H :
              (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × I)
            x).1 :
      X) =
    f (↑x : E)

Tactic:
dsimp
-- Module: Mathlib.Topology.Covering.Basic
Goal:
E : Type u_1
X : Type u_2
inst_1 : TopologicalSpace E
inst_2 : TopologicalSpace X
f : E → X
s : Set X
I : Type u_3
inst_3 : TopologicalSpace I
hs : IsOpen[inst_2] s
hfs : IsOpen[inst_1] (f ⁻¹' s)
x_1 : X
hx : x_1 ∈ s
h : IsEvenlyCovered (fun (e : (↑(f ⁻¹' s) : Type u_1)) ↦ f (↑e : E)) x_1 I
inst : DiscreteTopology I
U : Set X
hxU : x_1 ∈ U
hU : IsOpen[inst_2] U
hfU : IsOpen[instTopologicalSpaceSubtype] ((fun (e : (↑(f ⁻¹' s) : Type u_1)) ↦ f (↑e : E)) ⁻¹' U)
H : (↑((fun (e : (↑(f ⁻¹' s) : Type u_1)) ↦ f (↑e : E)) ⁻¹' U) : Type u_1) ≃ₜ Prod.{u_2, u_3} (↑U : Type u_2) I
hH :
  ∀ (x : (↑((fun (e : (↑(f ⁻¹' s) : Type u_1)) ↦ f (↑e : E)) ⁻¹' U) : Type u_1)),
    Eq.{u_2 + 1} (α := X)
      (↑((H : (a : (↑((fun (e : (↑(f ⁻¹' s) : Type u_1)) ↦ f (↑e : E)) ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × I) x).1 :
        X)
      ((fun (e : (↑(f ⁻¹' s) : Type u_1)) ↦ f (↑e : E)) (↑x : (↑(f ⁻¹' s) : Type u_1)))
h_1 : Nonempty I
hUs : U ⊆ s
this :
  Set.image (α := { x : E // x ∈ f ⁻¹' s }) (Subtype.val (p := fun (x : E) ↦ x ∈ f ⁻¹' s))
      ((fun (e : (↑(f ⁻¹' s) : Type u_1)) ↦ f (↑e : E)) ⁻¹' U) =
    f ⁻¹' U
x : (↑(f ⁻¹' U) : Type u_1)
⊢ Eq.{u_2 + 1} (α := X)
    (↑((H : (a : (↑((fun (e : (↑(f ⁻¹' s) : Type u_1)) ↦ f (↑e : E)) ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × I)
            (Subtype.mk (p := fun (x : (↑(f ⁻¹' s) : Type u_1)) ↦
              Membership.mem (γ := Set (↑(f ⁻¹' s) : Type u_1)) ((fun (e : (↑(f ⁻¹' s) : Type u_1)) ↦ f (↑e : E)) ⁻¹' U)
                x)
              (Subtype.mk (p := fun (x : E) ↦ x ∈ f ⁻¹' s) (↑x : E) ⋯) ⋯)).1 :
      X)
    ((fun (e : (↑(f ⁻¹' s) : Type u_1)) ↦ f (↑e : E))
      (↑(Subtype.mk (p := fun (x : (↑(f ⁻¹' s) : Type u_1)) ↦
            Membership.mem (γ := Set (↑(f ⁻¹' s) : Type u_1)) ((fun (e : (↑(f ⁻¹' s) : Type u_1)) ↦ f (↑e : E)) ⁻¹' U)
              x)
            (Subtype.mk (p := fun (x : E) ↦ x ∈ f ⁻¹' s) (↑x : E) ⋯) ⋯) :
        (↑(f ⁻¹' s) : Type u_1)))

Tactic:
hH ⟨⟨x, hUs x.2⟩, x.2⟩

Premises used: Subtype.mk, Subtype.val, Subtype.property
-- Module: Mathlib.Topology.Covering.Basic
Goal:
E : Type u_1
X : Type u_2
inst_1 : TopologicalSpace E
inst_2 : TopologicalSpace X
f : E → X
s : Set X
I : Type u_3
inst_3 : TopologicalSpace I
hs : IsOpen[inst_2] s
hfs : IsOpen[inst_1] (f ⁻¹' s)
x_1 : X
hx : x_1 ∈ s
h : IsEvenlyCovered (fun (e : (↑(f ⁻¹' s) : Type u_1)) ↦ f (↑e : E)) x_1 I
inst : DiscreteTopology I
U : Set X
hxU : x_1 ∈ U
hU : IsOpen[inst_2] U
hfU : IsOpen[instTopologicalSpaceSubtype] ((fun (e : (↑(f ⁻¹' s) : Type u_1)) ↦ f (↑e : E)) ⁻¹' U)
H : (↑((fun (e : (↑(f ⁻¹' s) : Type u_1)) ↦ f (↑e : E)) ⁻¹' U) : Type u_1) ≃ₜ Prod.{u_2, u_3} (↑U : Type u_2) I
hH :
  ∀ (x : (↑((fun (e : (↑(f ⁻¹' s) : Type u_1)) ↦ f (↑e : E)) ⁻¹' U) : Type u_1)),
    Eq.{u_2 + 1} (α := X)
      (↑((H : (a : (↑((fun (e : (↑(f ⁻¹' s) : Type u_1)) ↦ f (↑e : E)) ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × I) x).1 :
        X)
      ((fun (e : (↑(f ⁻¹' s) : Type u_1)) ↦ f (↑e : E)) (↑x : (↑(f ⁻¹' s) : Type u_1)))
h_1 : Nonempty I
hUs : U ⊆ s
this :
  Set.image (α := { x : E // x ∈ f ⁻¹' s }) (Subtype.val (p := fun (x : E) ↦ x ∈ f ⁻¹' s))
      ((fun (e : (↑(f ⁻¹' s) : Type u_1)) ↦ f (↑e : E)) ⁻¹' U) =
    f ⁻¹' U
x : (↑(f ⁻¹' U) : Type u_1)
⊢ Eq (α :=
    (↑(Set.image (α := { x : E // x ∈ f ⁻¹' s }) (Subtype.val (p := fun (x : E) ↦ x ∈ f ⁻¹' s))
          ((fun (e : (↑(f ⁻¹' s) : Type u_1)) ↦ f (↑e : E)) ⁻¹' U)) :
      Type u_1))
    ((Homeomorph.symm
            (Homeomorph.setCongr (s :=
              Set.image (α := { x : E // x ∈ f ⁻¹' s }) (Subtype.val (p := fun (x : E) ↦ x ∈ f ⁻¹' s))
                ((fun (e : (↑(f ⁻¹' s) : Type u_1)) ↦ f (↑e : E)) ⁻¹' U))
              (t := f ⁻¹' U) this) :
          (a : (↑(f ⁻¹' U) : Type u_1)) →
            (↑(Subtype.val '' (fun (e : (↑(f ⁻¹' s) : Type u_1)) ↦ f (↑e : E)) ⁻¹' U) : Type u_1))
        x :
      (↑(Set.image (α := { x : E // x ∈ f ⁻¹' s }) (Subtype.val (p := fun (x : E) ↦ x ∈ f ⁻¹' s))
            ((fun (e : (↑(f ⁻¹' s) : Type u_1)) ↦ f (↑e : E)) ⁻¹' U)) :
        Type u_1))
    ((IsEmbedding.homeomorphImage ⋯ ((fun (e : (↑(f ⁻¹' s) : Type u_1)) ↦ f (↑e : E)) ⁻¹' U) :
          (a : (↑((fun (e : (↑(f ⁻¹' s) : Type u_1)) ↦ f (↑e : E)) ⁻¹' U) : Type u_1)) →
            (↑(Subtype.val '' (fun (e : (↑(f ⁻¹' s) : Type u_1)) ↦ f (↑e : E)) ⁻¹' U) : Type u_1))
        (Subtype.mk (p := fun (x : (↑(f ⁻¹' s) : Type u_1)) ↦
          Membership.mem (γ := Set (↑(f ⁻¹' s) : Type u_1)) ((fun (e : (↑(f ⁻¹' s) : Type u_1)) ↦ f (↑e : E)) ⁻¹' U) x)
          (Subtype.mk (p := fun (x : E) ↦ x ∈ f ⁻¹' s) (↑x : E) ⋯) ⋯) :
      (↑(Set.image (α := { x : E // x ∈ f ⁻¹' s }) (Subtype.val (p := fun (x : E) ↦ x ∈ f ⁻¹' s))
            ((fun (e : (↑(f ⁻¹' s) : Type u_1)) ↦ f (↑e : E)) ⁻¹' U)) :
        Type u_1))

Tactic:
rfl
-- Module: Mathlib.Topology.Covering.Basic
Goal:
E : Type u_1
X : Type u_2
inst_1 : TopologicalSpace E
inst_2 : TopologicalSpace X
f : E → X
I : Type u_3
inst_3 : TopologicalSpace I
x : X
h : IsEvenlyCovered f x I
E' : Type u_4
inst_4 : TopologicalSpace E'
g : E' ≃ₜ E
inst : DiscreteTopology I
U : Set X
hxU : x ∈ U
hU : IsOpen[inst_2] U
hfU : IsOpen[inst_1] (f ⁻¹' U)
H : (↑(f ⁻¹' U) : Type u_1) ≃ₜ Prod.{u_2, u_3} (↑U : Type u_2) I
hH :
  ∀ (x : (↑(f ⁻¹' U) : Type u_1)), (↑((H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × I) x).1 : X) = f (↑x : E)
rw : Eq.{u_4 + 1} (α := Set E') ((⇑g : (a : E') → E) ⁻¹' f ⁻¹' U) ((⇑g.symm : (a : E) → E') '' f ⁻¹' U)
rw₁ rw₂ : Eq.{u_4 + 1} (α := Set E') ((⇑g : (a : E') → E) ⁻¹' f ⁻¹' U) ((⇑g : (a : E') → E) ⁻¹' f ⁻¹' U)
⊢ Eq.{u_4 + 1} (α := Set E') (f ∘ (⇑g : (a : E') → E) ⁻¹' U) ((⇑g.symm : (a : E) → E') '' f ⁻¹' U)

Tactic:
rw [Set.preimage_comp, g.image_symm]

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

Tactic:
h.comp_homeomorph g.symm

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

Tactic:
convert! h.comp_homeomorph g.symm

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

Tactic:
simp
-- Module: Mathlib.Topology.Covering.Basic
Goal:
E : Type u_1
X : Type u_2
inst_1 : TopologicalSpace E
inst_2 : TopologicalSpace X
f : E → X
I : Type u_3
inst_3 : TopologicalSpace I
x : X
h : IsEvenlyCovered f x I
Y : Type u_4
inst_4 : TopologicalSpace Y
g : X ≃ₜ Y
inst : DiscreteTopology I
U : Set X
hxU : x ∈ U
hU : IsOpen[inst_2] U
hfU : IsOpen[inst_1] (f ⁻¹' U)
H : (↑(f ⁻¹' U) : Type u_1) ≃ₜ Prod.{u_2, u_3} (↑U : Type u_2) I
hH :
  ∀ (x : (↑(f ⁻¹' U) : Type u_1)), (↑((H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × I) x).1 : X) = f (↑x : E)
⊢ IsOpen[inst_1] (Set.preimage.{u_1, u_4} (β := Y) ((⇑g : (a : X) → Y) ∘ f) ((⇑g : (a : X) → Y) '' U))

Tactic:
simpa [Set.preimage_comp]

Premises used: Set.preimage_comp
-- Module: Mathlib.Topology.Covering.Basic
Goal:
E : Type u_1
X : Type u_2
inst_1 : TopologicalSpace E
inst_2 : TopologicalSpace X
f : E → X
I : Type u_3
inst_3 : TopologicalSpace I
x : X
h : IsEvenlyCovered f x I
Y : Type u_4
inst_4 : TopologicalSpace Y
g : X ≃ₜ Y
inst : DiscreteTopology I
U : Set X
hxU : x ∈ U
hU : IsOpen[inst_2] U
hfU : IsOpen[inst_1] (f ⁻¹' U)
H : (↑(f ⁻¹' U) : Type u_1) ≃ₜ Prod.{u_2, u_3} (↑U : Type u_2) I
hH :
  ∀ (x : (↑(f ⁻¹' U) : Type u_1)), (↑((H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × I) x).1 : X) = f (↑x : E)
⊢ Set.preimage.{u_1, u_4} (β := Y) ((⇑g : (a : X) → Y) ∘ f) ((⇑g : (a : X) → Y) '' U) = f ⁻¹' U

Tactic:
simp [Set.preimage_comp]

Premises used: Set.preimage_comp