awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Covering.AddCircle (goal)
Goal:
𝕜 : Type u_1
inst : TopologicalSpace 𝕜
inst_1 : Ring 𝕜
inst_2 : IsTopologicalRing 𝕜
p : 𝕜
inst_3 : T0Space.{u_1} (AddCircle p)
n : ℕ
hn : IsUnit.{u_1} (M := 𝕜) (↑n : 𝕜)
h : ∀ (x : AddCircle p), Eq (α := AddCircle p → AddCircle p) (HSMul.hSMul n) (HSMul.hSMul (α := ℤ) (↑n : ℤ))
⊢ IsAddQuotientCoveringMap (X := AddCircle p) (fun (x : AddCircle p) ↦ n • x) ↥(AddMonoidHom.ker (nsmulAddMonoidHom n))
have h₁ : ∀ (x : AddCircle p), Eq.{u_1 + 1} (α := AddCircle p →+ AddCircle p) (nsmulAddMonoidHom n) (zsmulAddGroupHom (↑n : ℤ))
Tactic: convert! isAddQuotientCoveringMap_zsmul p (n := n) (mod_cast hn)
-- Lean 4 proof step from Mathlib.Topology.Covering.AddCircle (goal)
Goal:
𝕜 : Type u_1
inst : TopologicalSpace 𝕜
inst_1 : Ring 𝕜
inst_2 : IsTopologicalRing 𝕜
p : 𝕜
inst_3 : T0Space.{u_1} (AddCircle p)
n : ℕ
hn : IsUnit.{u_1} (M := 𝕜) (↑n : 𝕜)
h : ∀ (x : AddCircle p), Eq (α := AddCircle p → AddCircle p) (HSMul.hSMul n) (HSMul.hSMul (α := ℤ) (↑n : ℤ))
h₁ :
  ∀ (x : AddCircle p), Eq.{u_1 + 1} (α := AddCircle p →+ AddCircle p) (nsmulAddMonoidHom n) (zsmulAddGroupHom (↑n : ℤ))
⊢ IsAddQuotientCoveringMap (X := AddCircle p) (fun (x : AddCircle p) ↦ n • x) ↥(AddMonoidHom.ker (nsmulAddMonoidHom n))
have h₂ : ↥(AddMonoidHom.ker (nsmulAddMonoidHom n)) = ↥(AddMonoidHom.ker (zsmulAddGroupHom (↑n : ℤ))) →
  Eq.{u_1 + 1} (α := AddCircle p →+ AddCircle p) (nsmulAddMonoidHom n) (zsmulAddGroupHom (↑n : ℤ))
Tactic: convert! isAddQuotientCoveringMap_zsmul p (n := n) (mod_cast hn)
-- Lean 4 proof step from Mathlib.Topology.Covering.AddCircle (goal)
Goal:
𝕜 : Type u_1
inst : TopologicalSpace 𝕜
inst_1 : Ring 𝕜
inst_2 : IsTopologicalRing 𝕜
p : 𝕜
inst_3 : T0Space.{u_1} (AddCircle p)
n : ℕ
hn : IsUnit.{u_1} (M := 𝕜) (↑n : 𝕜)
h : ∀ (x : AddCircle p), Eq (α := AddCircle p → AddCircle p) (HSMul.hSMul n) (HSMul.hSMul (α := ℤ) (↑n : ℤ))
h₁ :
  ∀ (x : AddCircle p), Eq.{u_1 + 1} (α := AddCircle p →+ AddCircle p) (nsmulAddMonoidHom n) (zsmulAddGroupHom (↑n : ℤ))
h₂ :
  ↥(AddMonoidHom.ker (nsmulAddMonoidHom n)) = ↥(AddMonoidHom.ker (zsmulAddGroupHom (↑n : ℤ))) →
    Eq.{u_1 + 1} (α := AddCircle p →+ AddCircle p) (nsmulAddMonoidHom n) (zsmulAddGroupHom (↑n : ℤ))
⊢ IsAddQuotientCoveringMap (X := AddCircle p) (fun (x : AddCircle p) ↦ n • x) ↥(AddMonoidHom.ker (nsmulAddMonoidHom n))
have h₃ : ↥(AddMonoidHom.ker (nsmulAddMonoidHom n)) = ↥(AddMonoidHom.ker (zsmulAddGroupHom (↑n : ℤ))) →
  HEq.{u_1 + 1} (α := AddGroup ↥(AddMonoidHom.ker (nsmulAddMonoidHom n)))
      (AddSubgroup.toAddGroup (AddMonoidHom.ker (nsmulAddMonoidHom n))) (β :=
      AddGroup ↥(AddMonoidHom.ker (zsmulAddGroupHom (↑n : ℤ))))
      (AddSubgroup.toAddGroup (AddMonoidHom.ker (zsmulAddGroupHom (↑n : ℤ)))) →
    Eq.{u_1 + 1} (α := AddCircle p →+ AddCircle p) (nsmulAddMonoidHom n) (zsmulAddGroupHom (↑n : ℤ))
Tactic: convert! isAddQuotientCoveringMap_zsmul p (n := n) (mod_cast hn)
-- Lean 4 proof step from Mathlib.Topology.Covering.AddCircle (goal)
Goal:
𝕜 : Type u_1
inst : TopologicalSpace 𝕜
inst_1 : Ring 𝕜
inst_2 : IsTopologicalRing 𝕜
p : 𝕜
inst_3 : T0Space.{u_1} (AddCircle p)
n : ℕ
hn : IsUnit.{u_1} (M := 𝕜) (↑n : 𝕜)
x : AddCircle p
⊢ Eq (α := AddCircle p → AddCircle p) (HSMul.hSMul n) (HSMul.hSMul (α := ℤ) (↑n : ℤ))
have h : ∀ (x : AddCircle p), n • x = HSMul.hSMul (α := ℤ) (↑n : ℤ) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Covering.AddCircle (goal)
Goal:
𝕜 : Type u_1
inst : TopologicalSpace 𝕜
inst_1 : Ring 𝕜
inst_2 : IsTopologicalRing 𝕜
p : 𝕜
inst_3 : T0Space.{u_1} (AddCircle p)
n : ℕ
hn : IsUnit.{u_1} (M := 𝕜) (↑n : 𝕜)
x : AddCircle p
⊢ Eq.{u_1 + 1} (α := AddCircle p →+ AddCircle p) (nsmulAddMonoidHom n) (zsmulAddGroupHom (↑n : ℤ))
have h : ∀ (x : 𝕜),
  Eq (α := AddCircle p)
    ((AddMonoidHom.comp (nsmulAddMonoidHom n) (QuotientAddGroup.mk' (AddSubgroup.zmultiples p)) : (a : 𝕜) → AddCircle p)
        x :
      AddCircle p)
    ((AddMonoidHom.comp (zsmulAddGroupHom (↑n : ℤ)) (QuotientAddGroup.mk' (AddSubgroup.zmultiples p)) :
          (a : 𝕜) → AddCircle p)
        x :
      AddCircle p)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Covering.AddCircle (goal)
Goal:
𝕜 : Type u_1
inst : TopologicalSpace 𝕜
inst_1 : Ring 𝕜
inst_2 : IsTopologicalRing 𝕜
p : 𝕜
inst_3 : T0Space.{u_1} (AddCircle p)
n : ℕ
hn : IsUnit.{u_1} (M := 𝕜) (↑n : 𝕜)
e_6 : ↥(AddMonoidHom.ker (nsmulAddMonoidHom n)) = ↥(AddMonoidHom.ker (zsmulAddGroupHom (↑n : ℤ)))
⊢ Eq.{u_1 + 1} (α := AddCircle p →+ AddCircle p) (nsmulAddMonoidHom n) (zsmulAddGroupHom (↑n : ℤ))
have h : ∀ (x : 𝕜),
  Eq (α := AddCircle p)
    ((AddMonoidHom.comp (nsmulAddMonoidHom n) (QuotientAddGroup.mk' (AddSubgroup.zmultiples p)) : (a : 𝕜) → AddCircle p)
        x :
      AddCircle p)
    ((AddMonoidHom.comp (zsmulAddGroupHom (↑n : ℤ)) (QuotientAddGroup.mk' (AddSubgroup.zmultiples p)) :
          (a : 𝕜) → AddCircle p)
        x :
      AddCircle p)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Covering.AddCircle (goal)
Goal:
𝕜 : Type u_1
inst : TopologicalSpace 𝕜
inst_1 : Ring 𝕜
inst_2 : IsTopologicalRing 𝕜
p : 𝕜
inst_3 : T0Space.{u_1} (AddCircle p)
n : ℕ
hn : IsUnit.{u_1} (M := 𝕜) (↑n : 𝕜)
e_6 : ↥(AddMonoidHom.ker (nsmulAddMonoidHom n)) = ↥(AddMonoidHom.ker (zsmulAddGroupHom (↑n : ℤ)))
e_7 :
  HEq.{u_1 + 1} (α := AddGroup ↥(AddMonoidHom.ker (nsmulAddMonoidHom n)))
    (AddSubgroup.toAddGroup (AddMonoidHom.ker (nsmulAddMonoidHom n))) (β :=
    AddGroup ↥(AddMonoidHom.ker (zsmulAddGroupHom (↑n : ℤ))))
    (AddSubgroup.toAddGroup (AddMonoidHom.ker (zsmulAddGroupHom (↑n : ℤ))))
⊢ Eq.{u_1 + 1} (α := AddCircle p →+ AddCircle p) (nsmulAddMonoidHom n) (zsmulAddGroupHom (↑n : ℤ))
have h : ∀ (x : 𝕜),
  Eq (α := AddCircle p)
    ((AddMonoidHom.comp (nsmulAddMonoidHom n) (QuotientAddGroup.mk' (AddSubgroup.zmultiples p)) : (a : 𝕜) → AddCircle p)
        x :
      AddCircle p)
    ((AddMonoidHom.comp (zsmulAddGroupHom (↑n : ℤ)) (QuotientAddGroup.mk' (AddSubgroup.zmultiples p)) :
          (a : 𝕜) → AddCircle p)
        x :
      AddCircle p)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Covering.AddCircle (goal)
Goal:
𝕜 : Type u_1
inst : TopologicalSpace 𝕜
inst_1 : Ring 𝕜
inst_2 : IsTopologicalRing 𝕜
p : 𝕜
inst_3 : T0Space.{u_1} (AddCircle p)
inst_4 : Algebra ℚ 𝕜
n : ℤ
inst_5 : NeZero n
⊢ IsUnit.{u_1} (M := 𝕜) (↑n : 𝕜)
have h : Eq (α := 𝕜) ((↑n : 𝕜) : 𝕜) ((algebraMap ℚ 𝕜 : (a : ℚ) → 𝕜) (↑n : ℚ) : 𝕜)
Tactic: convert! (Int.cast_ne_zero.mpr <| NeZero.ne n).isUnit.map (algebraMap ℚ 𝕜)
-- Lean 4 proof step from Mathlib.Topology.Covering.AddCircle (goal)
Goal:
𝕜 : Type u_1
inst : TopologicalSpace 𝕜
inst_1 : Ring 𝕜
inst_2 : IsTopologicalRing 𝕜
p : 𝕜
inst_3 : T0Space.{u_1} (AddCircle p)
inst_4 : Algebra ℚ 𝕜
n : ℕ
inst_5 : NeZero n
⊢ IsUnit.{u_1} (M := 𝕜) (↑n : 𝕜)
have h : Eq (α := 𝕜) ((↑n : 𝕜) : 𝕜) ((algebraMap ℚ 𝕜 : (a : ℚ) → 𝕜) (↑n : ℚ) : 𝕜)
Tactic: convert! (Nat.cast_ne_zero.mpr <| NeZero.ne n).isUnit.map (algebraMap ℚ 𝕜)
-- 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
I : Type u_3
inst_2 : TopologicalSpace I
x : X
h : IsEvenlyCovered f x I
⊢ Homeomorph.{u_3, u_1} I (↑(f ⁻¹' {x}) : Type u_1)
have choose : DiscreteTopology I →
  (U : Set X) →
    (hxU : x ∈ U) →
      (hU : IsOpen[inst_1] U) →
        (hfU : IsOpen[inst] (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)) →
              Homeomorph.{u_3, u_1} I (↑(f ⁻¹' {x}) : Type u_1)
Tactic: choose _ U hxU hU hfU H hH using h
Cleared hypotheses: h
-- 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
I : Type u_3
inst_2 : TopologicalSpace I
x : X
h : DiscreteTopology I
U : Set X
hxU : x ∈ U
hU : IsOpen[inst_1] U
hfU : IsOpen[inst] (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)
e : (↑(f ⁻¹' {x}) : Type u_1)
⊢ (↑e : E) ∈ f ⁻¹' U
have rwa : f (↑e : E) ∈ U
Tactic: rwa [Set.mem_preimage, (e.2 : f e = x)]
-- 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
I : Type u_3
inst_2 : TopologicalSpace I
x : X
inst_3 : Nonempty I
h : IsEvenlyCovered f x I
⊢ Trivialization I f
have choose : DiscreteTopology I →
  (U : Set X) →
    (hxU : x ∈ U) →
      (hU : IsOpen[inst_1] U) →
        (hfU : IsOpen[inst] (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)) →
              Trivialization I f
Tactic: choose _ U hxU hU hfU H hH using h
Cleared hypotheses: h
-- 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
I : Type u_3
inst_2 : TopologicalSpace I
inst_3 : DiscreteTopology I
x : X
t : Trivialization I f
hx : x ∈ t.baseSet
xi : Prod.{u_2, u_3} (↑t.baseSet : Type u_2) I
⊢ t.invFun ((↑xi.1 : X), xi.2) ∈ f ⁻¹' t.baseSet
have rw : t.invFun ((↑xi.1 : X), xi.2) ∈ t.source
Tactic: rw [Set.mem_preimage, ← t.mem_source]
-- Lean 4 proof step from Mathlib.Topology.Covering.Basic (goal)
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)
⊢ Subtype.val (p := fun (x : X) ↦ x ∈ s) ∘ f ⁻¹' Subtype.val (p := fun (x : X) ↦ x ∈ s) '' U = f ⁻¹' U
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Covering.Basic (goal)
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 ∈ s
have 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)
Tactic: convert! Set.mem_preimage.mp (H.symm (⟨y, hy⟩, Classical.arbitrary I)).1.2
-- Lean 4 proof step from Mathlib.Topology.Covering.Basic (goal)
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
⊢ 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
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Covering.Basic (goal)
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)
⊢ (↑((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)
have 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 sorry ((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)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Topology.Covering.Basic (goal)
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)
⊢ Eq.{u_4 + 1} (α := Set E') (f ∘ (⇑g : (a : E') → E) ⁻¹' U) ((⇑g.symm : (a : E) → E') '' f ⁻¹' U)
have rw : Eq.{u_4 + 1} (α := Set E') ((⇑g : (a : E') → E) ⁻¹' f ⁻¹' U) ((⇑g.symm : (a : E) → E') '' f ⁻¹' U)
Tactic: rw [Set.preimage_comp, g.image_symm]
-- Lean 4 proof step from Mathlib.Topology.Covering.Basic (goal)
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)
⊢ Eq.{u_4 + 1} (α := Set E') (f ∘ (⇑g : (a : E') → E) ⁻¹' U) ((⇑g.symm : (a : E) → E') '' f ⁻¹' U)
have rw₁ : Eq.{u_4 + 1} (α := Set E') ((⇑g : (a : E') → E) ⁻¹' f ⁻¹' U) ((⇑g : (a : E') → E) ⁻¹' f ⁻¹' U)
Tactic: rw [Set.preimage_comp, g.image_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
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 f x I
have h₁ : f = Function.comp.{u_1 + 1, u_4 + 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
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
⊢ f = Function.comp.{u_1 + 1, u_4 + 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_4 + 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
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 f x I
have h₁ : f = Function.comp.{u_1 + 1, u_4 + 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
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)
⊢ IsEvenlyCovered f x I
have h₂ : x = (g.symm : (a : Y) → X) ((g : (a : X) → Y) x : Y)
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
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
⊢ f = Function.comp.{u_1 + 1, u_4 + 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_4 + 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
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
⊢ f = Function.comp.{u_1 + 1, u_4 + 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_4 + 1, u_2 + 1} (β := Y) (⇑g.symm : (a : Y) → X) ((⇑g : (a : X) → Y) ∘ f) x
Tactic: try 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
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
⊢ IsEvenlyCovered f x (↑(f ⁻¹' {x}) : Type u_1)
have lift : ∀ (x : { x : X // x ∈ s }), IsEvenlyCovered f (↑x : X) (↑(f ⁻¹' {(↑x : X)}) : Type u_1)
Tactic: lift x to s using hx
Cleared hypotheses: x, hx
-- 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 }
⊢ IsEvenlyCovered f (↑x : X) (↑(f ⁻¹' {(↑x : X)}) : Type u_1)
have pos : ∀ (hxf : (↑x : X) ∈ Set.range f), IsEvenlyCovered f (↑x : X) (↑(f ⁻¹' {(↑x : X)}) : Type u_1)
Tactic: by_cases hxf : x.1 ∈ Set.range f
-- 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 }
pos : ∀ (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)
have neg : ∀ (hxf : (↑x : X) ∉ Set.range f), IsEvenlyCovered f (↑x : X) (↑(f ⁻¹' {(↑x : X)}) : Type u_1)
Tactic: by_cases hxf : x.1 ∈ Set.range f