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
hf : IsCoveringMapOn f Set.univ
t : Set X
⊢ IsCoveringMapOn (t.restrictPreimage f) Set.univ

Tactic:
hf.restrictPreimage t

Premises used: Set.Mem, Set.univ, setOf, IsCoveringMapOn.restrictPreimage, 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
hf : IsCoveringMapOn f Set.univ
t : Set X
⊢ IsCoveringMapOn (t.restrictPreimage f) Set.univ

Tactic:
exact hf.restrictPreimage t

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
hf : IsCoveringMap f
E' : Type u_3
inst_2 : TopologicalSpace E'
g : E' ≃ₜ E
rw :
  ∀ (hf : IsCoveringMapOn f Set.univ) {E' : Type u_3} [inst_3 : TopologicalSpace E'] (g : E' ≃ₜ E),
    IsCoveringMapOn.{u_3, u_2} (E := E') (f ∘ (⇑g : (a : E') → E)) Set.univ
⊢ IsCoveringMap.{u_3, u_2} (E := E') (f ∘ (⇑g : (a : E') → E))

Tactic:
rw [isCoveringMap_iff_isCoveringMapOn_univ] at hf ⊢

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

Tactic:
hf.comp_homeomorph g

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

Tactic:
exact hf.comp_homeomorph g

Premises used: IsCoveringMapOn.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
hf : IsCoveringMap f
Y : Type u_3
inst_2 : TopologicalSpace Y
g : X ≃ₜ Y
rw :
  ∀ (hf : IsCoveringMapOn f Set.univ) {Y : Type u_3} [inst_3 : TopologicalSpace Y] (g : X ≃ₜ Y),
    IsCoveringMapOn.{u_1, u_3} (X := Y) ((⇑g : (a : X) → Y) ∘ f) Set.univ
⊢ IsCoveringMap.{u_1, u_3} (X := Y) ((⇑g : (a : X) → Y) ∘ f)

Tactic:
rw [isCoveringMap_iff_isCoveringMapOn_univ] at hf ⊢

Premises used: 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
hf : IsCoveringMapOn f Set.univ
Y : Type u_3
inst_2 : TopologicalSpace Y
g : X ≃ₜ Y
⊢ IsCoveringMapOn.{u_1, u_3} (X := Y) ((⇑g : (a : X) → Y) ∘ f) Set.univ

Tactic:
hf.homeomorph_comp g

Premises used: Set.Mem, Set.univ, setOf, Set.preimage, 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
hf : IsCoveringMapOn f Set.univ
Y : Type u_3
inst_2 : TopologicalSpace Y
g : X ≃ₜ Y
⊢ IsCoveringMapOn.{u_1, u_3} (X := Y) ((⇑g : (a : X) → Y) ∘ f) Set.univ

Tactic:
exact hf.homeomorph_comp g

Premises used: 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
E' : Type u_3
inst_2 : TopologicalSpace E'
g : E' ≃ₜ E
h : IsCoveringMap.{u_3, u_2} (E := E') (f ∘ (⇑g : (a : E') → E))
⊢ IsCoveringMap.{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'))

Tactic:
h.comp_homeomorph g.symm

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

Tactic:
convert! h.comp_homeomorph g.symm

Premises used: IsCoveringMap.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
E' : Type u_3
inst_2 : TopologicalSpace E'
g : E' ≃ₜ E
h : IsCoveringMap.{u_3, u_2} (E := E') (f ∘ (⇑g : (a : E') → E))
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
E' : Type u_3
inst_2 : TopologicalSpace E'
g : E' ≃ₜ E
h : IsCoveringMap.{u_3, u_2} (E := E') (f ∘ (⇑g : (a : E') → E))
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
Y : Type u_3
inst_2 : TopologicalSpace Y
g : X ≃ₜ Y
h : IsCoveringMap.{u_1, u_3} (X := Y) ((⇑g : (a : X) → Y) ∘ f)
⊢ IsCoveringMap.{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))

Tactic:
h.homeomorph_comp g.symm

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

Tactic:
convert! h.homeomorph_comp g.symm

Premises used: Homeomorph.symm, IsCoveringMap.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
Y : Type u_3
inst_2 : TopologicalSpace Y
g : X ≃ₜ Y
h : IsCoveringMap.{u_1, u_3} (X := Y) ((⇑g : (a : X) → Y) ∘ f)
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
Y : Type u_3
inst_2 : TopologicalSpace Y
g : X ≃ₜ Y
h : IsCoveringMap.{u_1, u_3} (X := Y) ((⇑g : (a : X) → Y) ∘ f)
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
s : Set X
hs : IsOpen[inst_1] s
f : E → X
h : ∀ (x : E), f x ∈ s
hf : IsCoveringMap.{u_1, u_2} (X := { x : X // x ∈ s }) fun (x : E) ↦ Subtype.mk (p := fun (x : X) ↦ x ∈ s) (f x) ⋯
⊢ f ⁻¹' s = Set.univ

Tactic:
simpa [Set.range, Set.subset_def] using h

Premises used: Set.subset_def, Set.range
-- Module: Mathlib.Topology.Covering.Basic
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
s : Set X
hs : IsOpen[inst_1] s
f : E → X
h : ∀ (x : E), f x ∈ s
hf : IsCoveringMap.{u_1, u_2} (X := { x : X // x ∈ s }) fun (x : E) ↦ Subtype.mk (p := fun (x : X) ↦ x ∈ s) (f x) ⋯
eq : f ⁻¹' s = Set.univ
⊢ IsOpen[inst] (f ⁻¹' s)

Tactic:
simp [eq]
-- 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 : Type u_3
inst_2 : TopologicalSpace F
inst_3 : DiscreteTopology F
hf : ∀ (x : X), ∃ (e : Trivialization F f), x ∈ e.baseSet
⊢ IsCoveringMap f

Tactic:
IsCoveringMap.mk f (fun _ => F) (fun x => Classical.choose (hf x)) fun x =>
    Classical.choose_spec (hf x)

Premises used: Classical.choose_spec, Classical.choose, IsCoveringMap.mk
-- Module: Mathlib.Topology.Covering.Basic
Goal:
X : Type u_2
inst : TopologicalSpace X
F : Type u_3
E : X → Type u_4
inst_1 : TopologicalSpace F
inst_2 : DiscreteTopology F
inst_3 : TopologicalSpace (TotalSpace F E)
inst_4 : (x : X) → TopologicalSpace (E x)
inst_5 : FiberBundle F E
⊢ IsCoveringMap (E := TotalSpace F E) (TotalSpace.proj (E := E))

Tactic:
IsFiberBundle.isCoveringMap fun x => ⟨trivializationAt F E x, mem_baseSet_trivializationAt F E x⟩

Premises used: IsFiberBundle.isCoveringMap, FiberBundle.trivializationAt, Exists.intro, FiberBundle.mem_baseSet_trivializationAt
-- 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 : Nonempty (X → E)
ι : Type u_3
inst_3 : Nonempty ι
inst_4 : TopologicalSpace ι
inst_5 : DiscreteTopology ι
U : ι → Set E
V : Set X
open_V : IsOpen[inst_1] V
open_iff : ∀ (i : ι) {W : Set X}, W ⊆ V → (IsOpen[inst_1] W ↔ IsOpen[inst] (f ⁻¹' W ∩ U i))
inj : ∀ (i : ι), Set.InjOn f (U i)
surj : ∀ (i : ι), Set.SurjOn f (U i) V
disjoint : Pairwise (Disjoint on U)
exhaustive : f ⁻¹' V ⊆ ⋃ (i : ι), U i
⊢ f ⁻¹' V ⊆ ⋃ (i : ι), U i

Tactic:
have exhaustive' := exhaustive
-- 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 : Nonempty (X → E)
ι : Type u_3
inst_3 : Nonempty ι
inst_4 : TopologicalSpace ι
inst_5 : DiscreteTopology ι
U : ι → Set E
V : Set X
open_V : IsOpen[inst_1] V
open_iff : ∀ (i : ι) {W : Set X}, W ⊆ V → (IsOpen[inst_1] W ↔ IsOpen[inst] (f ⁻¹' W ∩ U i))
inj : ∀ (i : ι), Set.InjOn f (U i)
surj : ∀ (i : ι), Set.SurjOn f (U i) V
disjoint : Pairwise (Disjoint on U)
exhaustive exhaustive' : f ⁻¹' V ⊆ ⋃ (i : ι), U i
⊢ ∀ x ∈ f ⁻¹' V, ∃ (i : ι), x ∈ U i

Tactic:
simp_rw [Set.subset_def, Set.mem_iUnion] at exhaustive

Premises used: Set.subset_def, Set.mem_iUnion
-- 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 : Nonempty (X → E)
ι : Type u_3
inst_3 : Nonempty ι
inst_4 : TopologicalSpace ι
inst_5 : DiscreteTopology ι
U : ι → Set E
V : Set X
open_V : IsOpen[inst_1] V
open_iff : ∀ (i : ι) {W : Set X}, W ⊆ V → (IsOpen[inst_1] W ↔ IsOpen[inst] (f ⁻¹' W ∩ U i))
inj : ∀ (i : ι), Set.InjOn f (U i)
surj : ∀ (i : ι), Set.SurjOn f (U i) V
disjoint : Pairwise (Disjoint on U)
exhaustive' : f ⁻¹' V ⊆ ⋃ (i : ι), U i
exhaustive : ∀ x ∈ f ⁻¹' V, ∃ (i : ι), x ∈ U i
choose : (idx : (x : E) → x ∈ f ⁻¹' V → ι) → (idx_U : ∀ (x : E) (a : x ∈ f ⁻¹' V), x ∈ U (idx x a)) → Trivialization ι f
⊢ Trivialization ι f

Tactic:
choose idx idx_U using exhaustive
-- 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 : Nonempty (X → E)
ι : Type u_3
inst_3 : Nonempty ι
inst_4 : TopologicalSpace ι
inst_5 : DiscreteTopology ι
U : ι → Set E
V : Set X
open_V : IsOpen[inst_1] V
open_iff : ∀ (i : ι) {W : Set X}, W ⊆ V → (IsOpen[inst_1] W ↔ IsOpen[inst] (f ⁻¹' W ∩ U i))
inj : ∀ (i : ι), Set.InjOn f (U i)
surj : ∀ (i : ι), Set.SurjOn f (U i) V
disjoint : Pairwise (Disjoint on U)
exhaustive' : f ⁻¹' V ⊆ ⋃ (i : ι), U i
idx : (x : E) → x ∈ f ⁻¹' V → ι
idx_U : ∀ (x : E) (a : x ∈ f ⁻¹' V), x ∈ U (idx x a)
choose :
  (inv : (i : ι) → ⦃a : X⦄ → a ∈ V → E) →
    (inv_U : ∀ (i : ι) ⦃a : X⦄ (a_1 : a ∈ V), inv i a_1 ∈ U i) →
      (f_inv : ∀ (i : ι) ⦃a : X⦄ (a_1 : a ∈ V), f (inv i a_1) = a) → Trivialization ι f
⊢ Trivialization ι f

Tactic:
choose inv inv_U f_inv using surj
-- 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 : Nonempty (X → E)
ι : Type ?u.94810
inst_3 : Nonempty ι
inst_4 : TopologicalSpace ι
inst_5 : DiscreteTopology ι
U : ι → Set E
V : Set X
open_V : IsOpen[inst_1] V
open_iff : ∀ (i : ι) {W : Set X}, W ⊆ V → (IsOpen[inst_1] W ↔ IsOpen[inst] (f ⁻¹' W ∩ U i))
inj : ∀ (i : ι), Set.InjOn f (U i)
disjoint : Pairwise (Disjoint on U)
exhaustive' : f ⁻¹' V ⊆ ⋃ (i : ι), U i
idx : (x : E) → x ∈ f ⁻¹' V → ι
idx_U : ∀ (x : E) (a : x ∈ f ⁻¹' V), x ∈ U (idx x a)
inv : (i : ι) → ⦃a : X⦄ → a ∈ V → E
inv_U : ∀ (i : ι) ⦃a : X⦄ (a_1 : a ∈ V), inv i a_1 ∈ U i
f_inv : ∀ (i : ι) ⦃a : X⦄ (a_1 : a ∈ V), f (inv i a_1) = a
x : X × ι
hx : Membership.mem.{max u_2 ?u.94810, max u_2 ?u.94810} (SProd.sprod (β := Set ι) V Set.univ) x
rw : inv x.2 ⋯ ∈ f ⁻¹' V
⊢ (if hx : x.1 ∈ V then inv x.2 hx else Classical.arbitrary (X → E) x.1) ∈ f ⁻¹' V

Tactic:
rw [dif_pos hx.1]

Premises used: dif_pos, And.left
-- 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 : Nonempty (X → E)
ι : Type ?u.94810
inst_3 : Nonempty ι
inst_4 : TopologicalSpace ι
inst_5 : DiscreteTopology ι
U : ι → Set E
V : Set X
open_V : IsOpen[inst_1] V
open_iff : ∀ (i : ι) {W : Set X}, W ⊆ V → (IsOpen[inst_1] W ↔ IsOpen[inst] (f ⁻¹' W ∩ U i))
inj : ∀ (i : ι), Set.InjOn f (U i)
disjoint : Pairwise (Disjoint on U)
exhaustive' : f ⁻¹' V ⊆ ⋃ (i : ι), U i
idx : (x : E) → x ∈ f ⁻¹' V → ι
idx_U : ∀ (x : E) (a : x ∈ f ⁻¹' V), x ∈ U (idx x a)
inv : (i : ι) → ⦃a : X⦄ → a ∈ V → E
inv_U : ∀ (i : ι) ⦃a : X⦄ (a_1 : a ∈ V), inv i a_1 ∈ U i
f_inv : ∀ (i : ι) ⦃a : X⦄ (a_1 : a ∈ V), f (inv i a_1) = a
x : X × ι
hx : Membership.mem.{max u_2 ?u.94810, max u_2 ?u.94810} (SProd.sprod (β := Set ι) V Set.univ) x
⊢ inv x.2 ⋯ ∈ f ⁻¹' V

Tactic:
apply (f_inv _ hx.1).symm ▸ hx.1
-- 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 : Nonempty (X → E)
ι : Type ?u.94810
inst_3 : Nonempty ι
inst_4 : TopologicalSpace ι
inst_5 : DiscreteTopology ι
U : ι → Set E
V : Set X
open_V : IsOpen[inst_1] V
open_iff : ∀ (i : ι) {W : Set X}, W ⊆ V → (IsOpen[inst_1] W ↔ IsOpen[inst] (f ⁻¹' W ∩ U i))
inj : ∀ (i : ι), Set.InjOn f (U i)
disjoint : Pairwise (Disjoint on U)
exhaustive' : f ⁻¹' V ⊆ ⋃ (i : ι), U i
idx : (x : E) → x ∈ f ⁻¹' V → ι
idx_U : ∀ (x : E) (a : x ∈ f ⁻¹' V), x ∈ U (idx x a)
inv : (i : ι) → ⦃a : X⦄ → a ∈ V → E
inv_U : ∀ (i : ι) ⦃a : X⦄ (a_1 : a ∈ V), inv i a_1 ∈ U i
f_inv : ∀ (i : ι) ⦃a : X⦄ (a_1 : a ∈ V), f (inv i a_1) = a
e : E
he : e ∈ f ⁻¹' V
simp_rw : inv (idx e ⋯) ⋯ = e
⊢ (if hx : (f e, if he : f e ∈ V then idx e he else Classical.arbitrary ι).1 ∈ V then
      inv (f e, if he : f e ∈ V then idx e he else Classical.arbitrary ι).2 hx
    else Classical.arbitrary (X → E) (f e, if he : f e ∈ V then idx e he else Classical.arbitrary ι).1) =
    e

Tactic:
simp_rw [dif_pos (id he : f e ∈ V)]

Premises used: dif_pos, id
-- 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 : Nonempty (X → E)
ι : Type ?u.94810
inst_3 : Nonempty ι
inst_4 : TopologicalSpace ι
inst_5 : DiscreteTopology ι
U : ι → Set E
V : Set X
open_V : IsOpen[inst_1] V
open_iff : ∀ (i : ι) {W : Set X}, W ⊆ V → (IsOpen[inst_1] W ↔ IsOpen[inst] (f ⁻¹' W ∩ U i))
inj : ∀ (i : ι), Set.InjOn f (U i)
disjoint : Pairwise (Disjoint on U)
exhaustive' : f ⁻¹' V ⊆ ⋃ (i : ι), U i
idx : (x : E) → x ∈ f ⁻¹' V → ι
idx_U : ∀ (x : E) (a : x ∈ f ⁻¹' V), x ∈ U (idx x a)
inv : (i : ι) → ⦃a : X⦄ → a ∈ V → E
inv_U : ∀ (i : ι) ⦃a : X⦄ (a_1 : a ∈ V), inv i a_1 ∈ U i
f_inv : ∀ (i : ι) ⦃a : X⦄ (a_1 : a ∈ V), f (inv i a_1) = a
e : E
he : e ∈ f ⁻¹' V
⊢ inv (idx e ⋯) ⋯ = e

Tactic:
inj _ (inv_U _ he) (idx_U e he) (f_inv _ _)
-- 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 : Nonempty (X → E)
ι : Type ?u.94810
inst_3 : Nonempty ι
inst_4 : TopologicalSpace ι
inst_5 : DiscreteTopology ι
U : ι → Set E
V : Set X
open_V : IsOpen[inst_1] V
open_iff : ∀ (i : ι) {W : Set X}, W ⊆ V → (IsOpen[inst_1] W ↔ IsOpen[inst] (f ⁻¹' W ∩ U i))
inj : ∀ (i : ι), Set.InjOn f (U i)
disjoint : Pairwise (Disjoint on U)
exhaustive' : f ⁻¹' V ⊆ ⋃ (i : ι), U i
idx : (x : E) → x ∈ f ⁻¹' V → ι
idx_U : ∀ (x : E) (a : x ∈ f ⁻¹' V), x ∈ U (idx x a)
inv : (i : ι) → ⦃a : X⦄ → a ∈ V → E
inv_U : ∀ (i : ι) ⦃a : X⦄ (a_1 : a ∈ V), inv i a_1 ∈ U i
f_inv : ∀ (i : ι) ⦃a : X⦄ (a_1 : a ∈ V), f (inv i a_1) = a
e : E
he : e ∈ f ⁻¹' V
⊢ inv (idx e ⋯) ⋯ = e

Tactic:
exact inj _ (inv_U _ he) (idx_U e he) (f_inv _ _)
-- 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 : Nonempty (X → E)
ι : Type ?u.94810
inst_3 : Nonempty ι
inst_4 : TopologicalSpace ι
inst_5 : DiscreteTopology ι
U : ι → Set E
V : Set X
open_V : IsOpen[inst_1] V
open_iff : ∀ (i : ι) {W : Set X}, W ⊆ V → (IsOpen[inst_1] W ↔ IsOpen[inst] (f ⁻¹' W ∩ U i))
inj : ∀ (i : ι), Set.InjOn f (U i)
disjoint : Pairwise (Disjoint on U)
exhaustive' : f ⁻¹' V ⊆ ⋃ (i : ι), U i
idx : (x : E) → x ∈ f ⁻¹' V → ι
idx_U : ∀ (x : E) (a : x ∈ f ⁻¹' V), x ∈ U (idx x a)
inv : (i : ι) → ⦃a : X⦄ → a ∈ V → E
inv_U : ∀ (i : ι) ⦃a : X⦄ (a_1 : a ∈ V), inv i a_1 ∈ U i
f_inv : ∀ (i : ι) ⦃a : X⦄ (a_1 : a ∈ V), f (inv i a_1) = a
x : X × ι
hx : Membership.mem.{max u_2 ?u.94810, max u_2 ?u.94810} (SProd.sprod (β := Set ι) V Set.univ) x
rw :
  Eq.{(max u_2 ?u.94810) + 1}
    (f (inv x.2 ⋯), if he : f (inv x.2 ⋯) ∈ V then idx (inv x.2 ⋯) he else Classical.arbitrary ι) x
⊢ Eq.{(max u_2 ?u.94810) + 1}
    (f (if hx : x.1 ∈ V then inv x.2 hx else Classical.arbitrary (X → E) x.1),
      if he : f (if hx : x.1 ∈ V then inv x.2 hx else Classical.arbitrary (X → E) x.1) ∈ V then
        idx (if hx : x.1 ∈ V then inv x.2 hx else Classical.arbitrary (X → E) x.1) he
      else Classical.arbitrary ι)
    x

Tactic:
rw [dif_pos hx.1]

Premises used: dif_pos, And.left
-- 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 : Nonempty (X → E)
ι : Type ?u.94810
inst_3 : Nonempty ι
inst_4 : TopologicalSpace ι
inst_5 : DiscreteTopology ι
U : ι → Set E
V : Set X
open_V : IsOpen[inst_1] V
open_iff : ∀ (i : ι) {W : Set X}, W ⊆ V → (IsOpen[inst_1] W ↔ IsOpen[inst] (f ⁻¹' W ∩ U i))
inj : ∀ (i : ι), Set.InjOn f (U i)
disjoint : Pairwise (Disjoint on U)
exhaustive' : f ⁻¹' V ⊆ ⋃ (i : ι), U i
idx : (x : E) → x ∈ f ⁻¹' V → ι
idx_U : ∀ (x : E) (a : x ∈ f ⁻¹' V), x ∈ U (idx x a)
inv : (i : ι) → ⦃a : X⦄ → a ∈ V → E
inv_U : ∀ (i : ι) ⦃a : X⦄ (a_1 : a ∈ V), inv i a_1 ∈ U i
f_inv : ∀ (i : ι) ⦃a : X⦄ (a_1 : a ∈ V), f (inv i a_1) = a
x : X × ι
hx : Membership.mem.{max u_2 ?u.94810, max u_2 ?u.94810} (SProd.sprod (β := Set ι) V Set.univ) x
⊢ Eq.{(max u_2 ?u.94810) + 1}
    (f (inv x.2 ⋯), if he : f (inv x.2 ⋯) ∈ V then idx (inv x.2 ⋯) he else Classical.arbitrary ι) x

Tactic:
Prod.ext (f_inv _ hx.1) ?_

Premises used: And.left, Prod.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
inst_2 : Nonempty (X → E)
ι : Type ?u.94810
inst_3 : Nonempty ι
inst_4 : TopologicalSpace ι
inst_5 : DiscreteTopology ι
U : ι → Set E
V : Set X
open_V : IsOpen[inst_1] V
open_iff : ∀ (i : ι) {W : Set X}, W ⊆ V → (IsOpen[inst_1] W ↔ IsOpen[inst] (f ⁻¹' W ∩ U i))
inj : ∀ (i : ι), Set.InjOn f (U i)
disjoint : Pairwise (Disjoint on U)
exhaustive' : f ⁻¹' V ⊆ ⋃ (i : ι), U i
idx : (x : E) → x ∈ f ⁻¹' V → ι
idx_U : ∀ (x : E) (a : x ∈ f ⁻¹' V), x ∈ U (idx x a)
inv : (i : ι) → ⦃a : X⦄ → a ∈ V → E
inv_U : ∀ (i : ι) ⦃a : X⦄ (a_1 : a ∈ V), inv i a_1 ∈ U i
f_inv : ∀ (i : ι) ⦃a : X⦄ (a_1 : a ∈ V), f (inv i a_1) = a
x : X × ι
hx : Membership.mem.{max u_2 ?u.94810, max u_2 ?u.94810} (SProd.sprod (β := Set ι) V Set.univ) x
refine : (f (inv x.2 ⋯), if he : f (inv x.2 ⋯) ∈ V then idx (inv x.2 ⋯) he else Classical.arbitrary ι).2 = x.2
⊢ Eq.{(max u_2 ?u.94810) + 1}
    (f (inv x.2 ⋯), if he : f (inv x.2 ⋯) ∈ V then idx (inv x.2 ⋯) he else Classical.arbitrary ι) x

Tactic:
refine Prod.ext (f_inv _ hx.1) ?_

Premises used: Prod.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
inst_2 : Nonempty (X → E)
ι : Type ?u.94810
inst_3 : Nonempty ι
inst_4 : TopologicalSpace ι
inst_5 : DiscreteTopology ι
U : ι → Set E
V : Set X
open_V : IsOpen[inst_1] V
open_iff : ∀ (i : ι) {W : Set X}, W ⊆ V → (IsOpen[inst_1] W ↔ IsOpen[inst] (f ⁻¹' W ∩ U i))
inj : ∀ (i : ι), Set.InjOn f (U i)
disjoint : Pairwise (Disjoint on U)
exhaustive' : f ⁻¹' V ⊆ ⋃ (i : ι), U i
idx : (x : E) → x ∈ f ⁻¹' V → ι
idx_U : ∀ (x : E) (a : x ∈ f ⁻¹' V), x ∈ U (idx x a)
inv : (i : ι) → ⦃a : X⦄ → a ∈ V → E
inv_U : ∀ (i : ι) ⦃a : X⦄ (a_1 : a ∈ V), inv i a_1 ∈ U i
f_inv : ∀ (i : ι) ⦃a : X⦄ (a_1 : a ∈ V), f (inv i a_1) = a
x : X × ι
hx : Membership.mem.{max u_2 ?u.94810, max u_2 ?u.94810} (SProd.sprod (β := Set ι) V Set.univ) x
rw : (f (inv x.2 ⋯), idx (inv x.2 ⋯) ⋯).2 = x.2
⊢ (f (inv x.2 ⋯), if he : f (inv x.2 ⋯) ∈ V then idx (inv x.2 ⋯) he else Classical.arbitrary ι).2 = x.2

Tactic:
rw [dif_pos ((f_inv _ hx.1).symm ▸ hx.1)]

Premises used: dif_pos
-- 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 : Nonempty (X → E)
ι : Type ?u.94810
inst_3 : Nonempty ι
inst_4 : TopologicalSpace ι
inst_5 : DiscreteTopology ι
U : ι → Set E
V : Set X
open_V : IsOpen[inst_1] V
open_iff : ∀ (i : ι) {W : Set X}, W ⊆ V → (IsOpen[inst_1] W ↔ IsOpen[inst] (f ⁻¹' W ∩ U i))
inj : ∀ (i : ι), Set.InjOn f (U i)
disjoint : Pairwise (Disjoint on U)
exhaustive' : f ⁻¹' V ⊆ ⋃ (i : ι), U i
idx : (x : E) → x ∈ f ⁻¹' V → ι
idx_U : ∀ (x : E) (a : x ∈ f ⁻¹' V), x ∈ U (idx x a)
inv : (i : ι) → ⦃a : X⦄ → a ∈ V → E
inv_U : ∀ (i : ι) ⦃a : X⦄ (a_1 : a ∈ V), inv i a_1 ∈ U i
f_inv : ∀ (i : ι) ⦃a : X⦄ (a_1 : a ∈ V), f (inv i a_1) = a
x : X × ι
hx : Membership.mem.{max u_2 ?u.94810, max u_2 ?u.94810} (SProd.sprod (β := Set ι) V Set.univ) x
by_contra : ∀ (h : ¬(f (inv x.2 ⋯), idx (inv x.2 ⋯) ⋯).2 = x.2), False
⊢ (f (inv x.2 ⋯), idx (inv x.2 ⋯) ⋯).2 = x.2

Tactic:
by_contra h
-- 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 : Nonempty (X → E)
ι : Type ?u.94810
inst_3 : Nonempty ι
inst_4 : TopologicalSpace ι
inst_5 : DiscreteTopology ι
U : ι → Set E
V : Set X
open_V : IsOpen[inst_1] V
open_iff : ∀ (i : ι) {W : Set X}, W ⊆ V → (IsOpen[inst_1] W ↔ IsOpen[inst] (f ⁻¹' W ∩ U i))
inj : ∀ (i : ι), Set.InjOn f (U i)
disjoint : Pairwise (Disjoint on U)
exhaustive' : f ⁻¹' V ⊆ ⋃ (i : ι), U i
idx : (x : E) → x ∈ f ⁻¹' V → ι
idx_U : ∀ (x : E) (a : x ∈ f ⁻¹' V), x ∈ U (idx x a)
inv : (i : ι) → ⦃a : X⦄ → a ∈ V → E
inv_U : ∀ (i : ι) ⦃a : X⦄ (a_1 : a ∈ V), inv i a_1 ∈ U i
f_inv : ∀ (i : ι) ⦃a : X⦄ (a_1 : a ∈ V), f (inv i a_1) = a
x : X × ι
hx : Membership.mem.{max u_2 ?u.94810, max u_2 ?u.94810} (SProd.sprod (β := Set ι) V Set.univ) x
h : ¬(f (inv x.2 ⋯), idx (inv x.2 ⋯) ⋯).2 = x.2
⊢ False

Tactic:
(disjoint h).le_bot ⟨idx_U .., inv_U _ _⟩

Premises used: Disjoint.le_bot, Set.Mem, And.intro