awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Covering.Basic (goal)
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)
have neg : ∀ (U : Set X) (hUx : U ∈ 𝓝 (↑x : X)) (hfU : f ⁻¹' U = ∅), IsEvenlyCovered f (↑x : X) (↑(f ⁻¹' {(↑x : X)}) : Type u_1)
Tactic: have ⟨U, hUx, hfU⟩ := h x hxf
-- Lean 4 proof step from Mathlib.Topology.Covering.Basic (goal)
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
⊢ IsCoveringMapOn f s
have inl : IsEmpty E → IsCoveringMapOn f s
Tactic: cases isEmpty_or_nonempty E
-- Lean 4 proof step from Mathlib.Topology.Covering.Basic (goal)
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
⊢ IsCoveringMapOn f s
have inr : Nonempty E → IsCoveringMapOn f s
Tactic: cases isEmpty_or_nonempty E
-- Lean 4 proof step from Mathlib.Topology.Covering.Basic (goal)
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
have inr : ∀ (x : (↑s : Type u_2)) (hx : (↑x : X) ∉ Set.range f), (↑x : X) ∈ Set.range f
Tactic: refine .mk' _ _ _ (fun x _ ↦ ⟨e x, h x⟩) fun x hx ↦ (hx ?_).elim
-- Lean 4 proof step from Mathlib.Topology.Covering.Basic (goal)
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)
have refine : ∀ (x : E) (hx : x ∈ f ⁻¹' s), ∃ (e : OpenPartialHomeomorph E X), x ∈ e.source ∧ Set.EqOn f (↑e : E → X) e.source
Tactic: refine IsLocalHomeomorphOn.mk f (f ⁻¹' s) fun x hx ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Covering.Basic (hypothesis)
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
⊢ ∃ (e : OpenPartialHomeomorph E X), x ∈ e.source ∧ Set.EqOn f (↑e : E → X) e.source
have this : Nonempty.{u_1 + 1} (↑(f ⁻¹' {f x}) : Type u_1)
Tactic: have : Nonempty (f ⁻¹' {f x}) := ⟨⟨x, rfl⟩⟩
-- Lean 4 proof step from Mathlib.Topology.Covering.Basic (hypothesis)
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
⊢ ∃ (e : OpenPartialHomeomorph E X), x ∈ e.source ∧ Set.EqOn f (↑e : E → X) e.source
have h : f x ∈ sorry.toTrivialization.baseSet
Tactic: have h := (hf (f x) hx).mem_toTrivialization_baseSet
-- Lean 4 proof step from Mathlib.Topology.Covering.Basic (goal)
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.symm.symm : E → X × (↑(f ⁻¹' {f x}) : Type u_1)) x).1 ∈ e.baseSet
have rwa : ((↑e.toOpenPartialHomeomorph : E → X × (↑(f ⁻¹' {f x}) : Type u_1)) x).1 ∈ e.baseSet
Tactic: rwa [e.toOpenPartialHomeomorph.symm_symm, e.proj_toFun x he]
-- Lean 4 proof step from Mathlib.Topology.Covering.Basic (goal)
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 f s
have h₁ : f = Function.comp.{u_1 + 1, u_3 + 1, u_2 + 1} (β := E') (f ∘ (⇑g : (a : E') → E)) (⇑g.symm : (a : E) → E')
Tactic: convert! h.comp_homeomorph g.symm
-- Lean 4 proof step from Mathlib.Topology.Covering.Basic (goal)
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
⊢ f = Function.comp.{u_1 + 1, u_3 + 1, u_2 + 1} (β := E') (f ∘ (⇑g : (a : E') → E)) (⇑g.symm : (a : E) → E')
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Covering.Basic (goal)
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 f s
have h₁ : f = Function.comp.{u_1 + 1, u_3 + 1, u_2 + 1} (β := Y) (⇑g.symm : (a : Y) → X) ((⇑g : (a : X) → Y) ∘ f)
Tactic: convert! h.homeomorph_comp g.symm
-- Lean 4 proof step from Mathlib.Topology.Covering.Basic (goal)
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)
⊢ IsCoveringMapOn f s
have h₂ : s = Set.preimage.{u_2, u_3} (β := Y) (⇑g.symm.symm : (a : X) → Y) ((⇑g.symm : (a : Y) → X) ⁻¹' s)
Tactic: convert! h.homeomorph_comp g.symm
-- Lean 4 proof step from Mathlib.Topology.Covering.Basic (goal)
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)
⊢ f = Function.comp.{u_1 + 1, u_3 + 1, u_2 + 1} (β := Y) (⇑g.symm : (a : Y) → X) ((⇑g : (a : X) → Y) ∘ f)
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Covering.Basic (goal)
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)
⊢ s = Set.preimage.{u_2, u_3} (β := Y) (⇑g.symm.symm : (a : X) → Y) ((⇑g.symm : (a : Y) → X) ⁻¹' s)
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Covering.Basic (hypothesis)
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₂
⊢ ∃ (s₁ : Set E) (s₂ : Set E), IsOpen[inst] s₁ ∧ IsOpen[inst] s₂ ∧ e₁ ∈ s₁ ∧ e₂ ∈ s₂ ∧ Disjoint s₁ s₂
have this : Nonempty.{u_1 + 1} (↑(f ⁻¹' {f e₁}) : Type u_1)
Tactic: have : Nonempty (f ⁻¹' {f e₁}) := ⟨⟨e₁, rfl⟩⟩
-- Lean 4 proof step from Mathlib.Topology.Covering.Basic (hypothesis)
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)
⊢ ∃ (s₁ : Set E) (s₂ : Set E), IsOpen[inst] s₁ ∧ IsOpen[inst] s₂ ∧ e₁ ∈ s₁ ∧ e₂ ∈ s₂ ∧ Disjoint s₁ s₂
have hf₁ : IsEvenlyCovered f (f e₁) (↑(f ⁻¹' {f e₁}) : Type u_1)
Tactic: specialize hf (f e₁)
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Topology.Covering.Basic (hypothesis)
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
⊢ ∃ (s₁ : Set E) (s₂ : Set E), IsOpen[inst] s₁ ∧ IsOpen[inst] s₂ ∧ e₁ ∈ s₁ ∧ e₂ ∈ s₂ ∧ Disjoint s₁ s₂
have this₁ : DiscreteTopology.{u_1} (↑(f ⁻¹' {f e₁}) : Type u_1)
Tactic: have := hf.discreteTopology_fiber
-- Lean 4 proof step from Mathlib.Topology.Covering.Basic (hypothesis)
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)
⊢ ∃ (s₁ : Set E) (s₂ : Set E), IsOpen[inst] s₁ ∧ IsOpen[inst] s₂ ∧ e₁ ∈ s₁ ∧ e₂ ∈ s₂ ∧ Disjoint s₁ s₂
have he₁ : f e₁ ∈ hf.toTrivialization.baseSet
Tactic: have he₁ := hf.mem_toTrivialization_baseSet
-- Lean 4 proof step from Mathlib.Topology.Covering.Basic (hypothesis)
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
⊢ ∃ (s₁ : Set E) (s₂ : Set E), IsOpen[inst] s₁ ∧ IsOpen[inst] s₂ ∧ e₁ ∈ s₁ ∧ e₂ ∈ s₂ ∧ Disjoint s₁ s₂
have he₃ : f e₂ ∈ hf.toTrivialization.baseSet
Tactic: simp_rw [he] at he₂
Cleared hypotheses: he₂
-- Lean 4 proof step from Mathlib.Topology.Covering.Basic (hypothesis)
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
⊢ ∃ (s₁ : Set E) (s₂ : Set E), IsOpen[inst] s₁ ∧ IsOpen[inst] s₂ ∧ e₁ ∈ s₁ ∧ e₂ ∈ s₂ ∧ Disjoint s₁ s₂
have he₃ : e₁ ∈ t.source
Tactic: rw [← t.mem_source] at he₁ he₂
Cleared hypotheses: he₁, he₂
-- Lean 4 proof step from Mathlib.Topology.Covering.Basic (hypothesis)
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
⊢ ∃ (s₁ : Set E) (s₂ : Set E), IsOpen[inst] s₁ ∧ IsOpen[inst] s₂ ∧ e₁ ∈ s₁ ∧ e₂ ∈ s₂ ∧ Disjoint s₁ s₂
have he₄ : e₂ ∈ t.source
Tactic: rw [← t.mem_source] at he₁ he₂
Cleared hypotheses: he₁, he₂
-- Lean 4 proof step from Mathlib.Topology.Covering.Basic (goal)
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₂
have 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})
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₂ ?_)⟩
-- Lean 4 proof step from Mathlib.Topology.Covering.Basic (goal)
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})
⊢ ∃ (s₁ : Set E) (s₂ : Set E), IsOpen[inst] s₁ ∧ IsOpen[inst] s₂ ∧ e₁ ∈ s₁ ∧ e₂ ∈ s₂ ∧ Disjoint s₁ s₂
have 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})
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₂ ?_)⟩
-- Lean 4 proof step from Mathlib.Topology.Covering.Basic (goal)
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})
⊢ ∃ (s₁ : Set E) (s₂ : Set E), IsOpen[inst] s₁ ∧ IsOpen[inst] s₂ ∧ e₁ ∈ s₁ ∧ e₂ ∈ s₂ ∧ Disjoint s₁ s₂
have 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₂
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₂ ?_)⟩
-- Lean 4 proof step from Mathlib.Topology.Covering.Basic (goal)
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₂
have 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
Tactic: refine Prod.ext ?_ (h₁.2.symm.trans h₂.2)
-- Lean 4 proof step from Mathlib.Topology.Covering.Basic (goal)
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₁).1 =
    ((↑t.toOpenPartialHomeomorph : E → X × (↑(f ⁻¹' {f e₁}) : Type u_1)) e₂).1
have refine_3 : f e₁ = ((↑t.toOpenPartialHomeomorph : E → X × (↑(f ⁻¹' {f e₁}) : Type u_1)) e₂).1
Tactic: rwa [t.proj_toFun e₁ he₁, t.proj_toFun e₂ he₂]
-- Lean 4 proof step from Mathlib.Topology.Covering.Basic (goal)
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
⊢ IsCoveringMap (t.restrictPreimage f)
have rw : ∀ (hf : IsCoveringMapOn f Set.univ) (t : Set X), IsCoveringMapOn (t.restrictPreimage f) Set.univ
Tactic: rw [isCoveringMap_iff_isCoveringMapOn_univ] at hf ⊢
Cleared hypotheses: hf, t
-- Lean 4 proof step from Mathlib.Topology.Covering.Basic (goal)
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
⊢ IsCoveringMap.{u_3, u_2} (E := E') (f ∘ (⇑g : (a : E') → E))
have 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
Tactic: rw [isCoveringMap_iff_isCoveringMapOn_univ] at hf ⊢
Cleared hypotheses: hf, E', inst_2, g
-- Lean 4 proof step from Mathlib.Topology.Covering.Basic (goal)
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
⊢ IsCoveringMap.{u_1, u_3} (X := Y) ((⇑g : (a : X) → Y) ∘ f)
have 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
Tactic: rw [isCoveringMap_iff_isCoveringMapOn_univ] at hf ⊢
Cleared hypotheses: hf, Y, inst_2, g
-- Lean 4 proof step from Mathlib.Topology.Covering.Basic (goal)
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 f
have h₁ : f = Function.comp.{u_1 + 1, u_3 + 1, u_2 + 1} (β := E') (f ∘ (⇑g : (a : E') → E)) (⇑g.symm : (a : E) → E')
Tactic: convert! h.comp_homeomorph g.symm
-- Lean 4 proof step from Mathlib.Topology.Covering.Basic (goal)
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))
⊢ f = Function.comp.{u_1 + 1, u_3 + 1, u_2 + 1} (β := E') (f ∘ (⇑g : (a : E') → E)) (⇑g.symm : (a : E) → E')
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Covering.Basic (goal)
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 f
have h₁ : f = Function.comp.{u_1 + 1, u_3 + 1, u_2 + 1} (β := Y) (⇑g.symm : (a : Y) → X) ((⇑g : (a : X) → Y) ∘ f)
Tactic: convert! h.homeomorph_comp g.symm
-- Lean 4 proof step from Mathlib.Topology.Covering.Basic (goal)
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)
⊢ f = Function.comp.{u_1 + 1, u_3 + 1, u_2 + 1} (β := Y) (⇑g.symm : (a : Y) → X) ((⇑g : (a : X) → Y) ∘ f)
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Covering.Basic (hypothesis)
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
⊢ Trivialization ι f
have exhaustive₁ : ∀ x ∈ f ⁻¹' V, ∃ (i : ι), x ∈ U i
Tactic: simp_rw [Set.subset_def, Set.mem_iUnion] at exhaustive
Cleared hypotheses: exhaustive
-- Lean 4 proof step from Mathlib.Topology.Covering.Basic (goal)
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
⊢ Trivialization ι f
have choose : (idx : (x : E) → x ∈ f ⁻¹' V → ι) → (idx_U : ∀ (x : E) (a : x ∈ f ⁻¹' V), x ∈ U (idx x a)) → Trivialization ι f
Tactic: choose idx idx_U using exhaustive
Cleared hypotheses: exhaustive
-- Lean 4 proof step from Mathlib.Topology.Covering.Basic (goal)
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)
⊢ Trivialization ι f
have 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
Tactic: choose inv inv_U f_inv using surj
Cleared hypotheses: surj