awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Homeomorph.Lemmas (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set Y
h : X ≃ₜ Y
rw : IsPreconnected.{u_1} (α := X) ((⇑h.symm : (a : Y) → X) '' s) ↔ IsPreconnected s
⊢ IsPreconnected.{u_1} (α := X) ((⇑h : (a : X) → Y) ⁻¹' s) ↔ IsPreconnected s
have rw₁ : IsPreconnected s ↔ IsPreconnected s
Tactic: rw [← image_symm, isPreconnected_image]
-- Lean 4 proof step from Mathlib.Topology.Homeomorph.Lemmas (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set Y
h : X ≃ₜ Y
⊢ IsConnected.{u_1} (α := X) ((⇑h : (a : X) → Y) ⁻¹' s) ↔ IsConnected s
have rw : IsConnected.{u_1} (α := X) ((⇑h.symm : (a : Y) → X) '' s) ↔ IsConnected s
Tactic: rw [← image_symm, isConnected_image]
-- Lean 4 proof step from Mathlib.Topology.Homeomorph.Lemmas (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set Y
h : X ≃ₜ Y
rw : IsConnected.{u_1} (α := X) ((⇑h.symm : (a : Y) → X) '' s) ↔ IsConnected s
⊢ IsConnected.{u_1} (α := X) ((⇑h : (a : X) → Y) ⁻¹' s) ↔ IsConnected s
have rw₁ : IsConnected s ↔ IsConnected s
Tactic: rw [← image_symm, isConnected_image]
-- Lean 4 proof step from Mathlib.Topology.Homeomorph.Lemmas (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
h : X ≃ₜ Y
x : X
hx : x ∈ s
⊢ Eq.{u_2 + 1} (α := Set Y) ((⇑h : (a : X) → Y) '' connectedComponentIn s x : Set Y)
    (connectedComponentIn ((⇑h : (a : X) → Y) '' s) ((h : (a : X) → Y) x) : Set Y)
have refine : Subset.{u_2} (α := Set Y) (connectedComponentIn ((⇑h : (a : X) → Y) '' s) ((h : (a : X) → Y) x) : Set Y)
  ((⇑h : (a : X) → Y) '' connectedComponentIn s x : Set Y)
Tactic: refine (h.continuous.image_connectedComponentIn_subset hx).antisymm ?_
-- Lean 4 proof step from Mathlib.Topology.Homeomorph.Lemmas (hypothesis)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
h : X ≃ₜ Y
x : X
hx : x ∈ s
⊢ Subset.{u_2} (α := Set Y) (connectedComponentIn ((⇑h : (a : X) → Y) '' s) ((h : (a : X) → Y) x) : Set Y)
    ((⇑h : (a : X) → Y) '' connectedComponentIn s x : Set Y)
have this : Subset.{u_1} (α := Set X)
  (image.{u_2, u_1} (α := Y) ((⇑h.symm : (a : Y) → X) : (a : Y) → X)
      (connectedComponentIn ((⇑h : (a : X) → Y) '' s) ((h : (a : X) → Y) x) : Set Y) :
    Set X)
  (connectedComponentIn (image.{u_2, u_1} (α := Y) (⇑h.symm : (a : Y) → X) ((⇑h : (a : X) → Y) '' s))
      ((h.symm : (a : Y) → X) ((h : (a : X) → Y) x : Y)) :
    Set X)
Tactic: have := h.symm.continuous.image_connectedComponentIn_subset (mem_image_of_mem h hx)
-- Lean 4 proof step from Mathlib.Topology.Homeomorph.Lemmas (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
h : X ≃ₜ Y
x : X
hx : x ∈ s
this :
  Subset.{u_1} (α := Set X)
    (image.{u_2, u_1} (α := Y) ((⇑h.symm : (a : Y) → X) : (a : Y) → X)
        (connectedComponentIn ((⇑h : (a : X) → Y) '' s) ((h : (a : X) → Y) x) : Set Y) :
      Set X)
    (connectedComponentIn (image.{u_2, u_1} (α := Y) (⇑h.symm : (a : Y) → X) ((⇑h : (a : X) → Y) '' s))
        ((h.symm : (a : Y) → X) ((h : (a : X) → Y) x : Y)) :
      Set X)
⊢ Subset.{u_2} (α := Set Y) (connectedComponentIn ((⇑h : (a : X) → Y) '' s) ((h : (a : X) → Y) x) : Set Y)
    ((⇑h : (a : X) → Y) '' connectedComponentIn s x : Set Y)
have rwa : ∀
  (this :
    Subset.{u_2} (α := Set Y) (connectedComponentIn ((⇑h : (a : X) → Y) '' s) ((h : (a : X) → Y) x) : Set Y)
      (preimage.{u_2, u_1} (β := X) ((⇑h.symm : (a : Y) → X) : (a : Y) → X)
          (connectedComponentIn (image.{u_2, u_1} (α := Y) (⇑h.symm : (a : Y) → X) ((⇑h : (a : X) → Y) '' s))
              ((h.symm : (a : Y) → X) ((h : (a : X) → Y) x : Y)) :
            Set X) :
        Set Y)),
  Subset.{u_2} (α := Set Y) (connectedComponentIn ((⇑h : (a : X) → Y) '' s) ((h : (a : X) → Y) x) : Set Y)
    ((⇑h : (a : X) → Y) '' connectedComponentIn s x : Set Y)
Tactic: rwa [image_subset_iff, h.preimage_symm, h.image_symm, h.preimage_image, h.symm_apply_apply]
    at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Homeomorph.Lemmas (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
h : X ≃ₜ Y
x : X
hx : x ∈ s
this :
  Subset.{u_1} (α := Set X)
    (image.{u_2, u_1} (α := Y) ((⇑h.symm : (a : Y) → X) : (a : Y) → X)
        (connectedComponentIn ((⇑h : (a : X) → Y) '' s) ((h : (a : X) → Y) x) : Set Y) :
      Set X)
    (connectedComponentIn (image.{u_2, u_1} (α := Y) (⇑h.symm : (a : Y) → X) ((⇑h : (a : X) → Y) '' s))
        ((h.symm : (a : Y) → X) ((h : (a : X) → Y) x : Y)) :
      Set X)
rwa :
  ∀
    (this :
      Subset.{u_2} (α := Set Y) (connectedComponentIn ((⇑h : (a : X) → Y) '' s) ((h : (a : X) → Y) x) : Set Y)
        (preimage.{u_2, u_1} (β := X) ((⇑h.symm : (a : Y) → X) : (a : Y) → X)
            (connectedComponentIn (image.{u_2, u_1} (α := Y) (⇑h.symm : (a : Y) → X) ((⇑h : (a : X) → Y) '' s))
                ((h.symm : (a : Y) → X) ((h : (a : X) → Y) x : Y)) :
              Set X) :
          Set Y)),
    Subset.{u_2} (α := Set Y) (connectedComponentIn ((⇑h : (a : X) → Y) '' s) ((h : (a : X) → Y) x) : Set Y)
      ((⇑h : (a : X) → Y) '' connectedComponentIn s x : Set Y)
⊢ Subset.{u_2} (α := Set Y) (connectedComponentIn ((⇑h : (a : X) → Y) '' s) ((h : (a : X) → Y) x) : Set Y)
    ((⇑h : (a : X) → Y) '' connectedComponentIn s x : Set Y)
have rwa₁ : ∀
  (this :
    Subset.{u_2} (α := Set Y) (connectedComponentIn ((⇑h : (a : X) → Y) '' s) ((h : (a : X) → Y) x) : Set Y)
      (image.{u_1, u_2} (α := X) ((⇑h : (a : X) → Y) : (a : X) → Y)
          (connectedComponentIn (image.{u_2, u_1} (α := Y) (⇑h.symm : (a : Y) → X) ((⇑h : (a : X) → Y) '' s))
              ((h.symm : (a : Y) → X) ((h : (a : X) → Y) x : Y)) :
            Set X) :
        Set Y)),
  Subset.{u_2} (α := Set Y) (connectedComponentIn ((⇑h : (a : X) → Y) '' s) ((h : (a : X) → Y) x) : Set Y)
    ((⇑h : (a : X) → Y) '' connectedComponentIn s x : Set Y)
Tactic: rwa [image_subset_iff, h.preimage_symm, h.image_symm, h.preimage_image, h.symm_apply_apply]
    at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Homeomorph.Lemmas (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
h : X ≃ₜ Y
x : X
hx : x ∈ s
this :
  Subset.{u_1} (α := Set X)
    (image.{u_2, u_1} (α := Y) ((⇑h.symm : (a : Y) → X) : (a : Y) → X)
        (connectedComponentIn ((⇑h : (a : X) → Y) '' s) ((h : (a : X) → Y) x) : Set Y) :
      Set X)
    (connectedComponentIn (image.{u_2, u_1} (α := Y) (⇑h.symm : (a : Y) → X) ((⇑h : (a : X) → Y) '' s))
        ((h.symm : (a : Y) → X) ((h : (a : X) → Y) x : Y)) :
      Set X)
rwa :
  ∀
    (this :
      Subset.{u_2} (α := Set Y) (connectedComponentIn ((⇑h : (a : X) → Y) '' s) ((h : (a : X) → Y) x) : Set Y)
        (preimage.{u_2, u_1} (β := X) ((⇑h.symm : (a : Y) → X) : (a : Y) → X)
            (connectedComponentIn (image.{u_2, u_1} (α := Y) (⇑h.symm : (a : Y) → X) ((⇑h : (a : X) → Y) '' s))
                ((h.symm : (a : Y) → X) ((h : (a : X) → Y) x : Y)) :
              Set X) :
          Set Y)),
    Subset.{u_2} (α := Set Y) (connectedComponentIn ((⇑h : (a : X) → Y) '' s) ((h : (a : X) → Y) x) : Set Y)
      ((⇑h : (a : X) → Y) '' connectedComponentIn s x : Set Y)
rwa₁ :
  ∀
    (this :
      Subset.{u_2} (α := Set Y) (connectedComponentIn ((⇑h : (a : X) → Y) '' s) ((h : (a : X) → Y) x) : Set Y)
        (image.{u_1, u_2} (α := X) ((⇑h : (a : X) → Y) : (a : X) → Y)
            (connectedComponentIn (image.{u_2, u_1} (α := Y) (⇑h.symm : (a : Y) → X) ((⇑h : (a : X) → Y) '' s))
                ((h.symm : (a : Y) → X) ((h : (a : X) → Y) x : Y)) :
              Set X) :
          Set Y)),
    Subset.{u_2} (α := Set Y) (connectedComponentIn ((⇑h : (a : X) → Y) '' s) ((h : (a : X) → Y) x) : Set Y)
      ((⇑h : (a : X) → Y) '' connectedComponentIn s x : Set Y)
⊢ Subset.{u_2} (α := Set Y) (connectedComponentIn ((⇑h : (a : X) → Y) '' s) ((h : (a : X) → Y) x) : Set Y)
    ((⇑h : (a : X) → Y) '' connectedComponentIn s x : Set Y)
have rwa₂ : ∀
  (this :
    Subset.{u_2} (α := Set Y) (connectedComponentIn ((⇑h : (a : X) → Y) '' s) ((h : (a : X) → Y) x) : Set Y)
      (image.{u_1, u_2} (α := X) ((⇑h : (a : X) → Y) : (a : X) → Y)
          (connectedComponentIn (preimage.{u_1, u_2} (β := Y) (⇑h : (a : X) → Y) ((⇑h : (a : X) → Y) '' s))
              ((h.symm : (a : Y) → X) ((h : (a : X) → Y) x : Y)) :
            Set X) :
        Set Y)),
  Subset.{u_2} (α := Set Y) (connectedComponentIn ((⇑h : (a : X) → Y) '' s) ((h : (a : X) → Y) x) : Set Y)
    ((⇑h : (a : X) → Y) '' connectedComponentIn s x : Set Y)
Tactic: rwa [image_subset_iff, h.preimage_symm, h.image_symm, h.preimage_image, h.symm_apply_apply]
    at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Homeomorph.Lemmas (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
h : X ≃ₜ Y
x : X
hx : x ∈ s
this :
  Subset.{u_1} (α := Set X)
    (image.{u_2, u_1} (α := Y) ((⇑h.symm : (a : Y) → X) : (a : Y) → X)
        (connectedComponentIn ((⇑h : (a : X) → Y) '' s) ((h : (a : X) → Y) x) : Set Y) :
      Set X)
    (connectedComponentIn (image.{u_2, u_1} (α := Y) (⇑h.symm : (a : Y) → X) ((⇑h : (a : X) → Y) '' s))
        ((h.symm : (a : Y) → X) ((h : (a : X) → Y) x : Y)) :
      Set X)
rwa :
  ∀
    (this :
      Subset.{u_2} (α := Set Y) (connectedComponentIn ((⇑h : (a : X) → Y) '' s) ((h : (a : X) → Y) x) : Set Y)
        (preimage.{u_2, u_1} (β := X) ((⇑h.symm : (a : Y) → X) : (a : Y) → X)
            (connectedComponentIn (image.{u_2, u_1} (α := Y) (⇑h.symm : (a : Y) → X) ((⇑h : (a : X) → Y) '' s))
                ((h.symm : (a : Y) → X) ((h : (a : X) → Y) x : Y)) :
              Set X) :
          Set Y)),
    Subset.{u_2} (α := Set Y) (connectedComponentIn ((⇑h : (a : X) → Y) '' s) ((h : (a : X) → Y) x) : Set Y)
      ((⇑h : (a : X) → Y) '' connectedComponentIn s x : Set Y)
rwa₁ :
  ∀
    (this :
      Subset.{u_2} (α := Set Y) (connectedComponentIn ((⇑h : (a : X) → Y) '' s) ((h : (a : X) → Y) x) : Set Y)
        (image.{u_1, u_2} (α := X) ((⇑h : (a : X) → Y) : (a : X) → Y)
            (connectedComponentIn (image.{u_2, u_1} (α := Y) (⇑h.symm : (a : Y) → X) ((⇑h : (a : X) → Y) '' s))
                ((h.symm : (a : Y) → X) ((h : (a : X) → Y) x : Y)) :
              Set X) :
          Set Y)),
    Subset.{u_2} (α := Set Y) (connectedComponentIn ((⇑h : (a : X) → Y) '' s) ((h : (a : X) → Y) x) : Set Y)
      ((⇑h : (a : X) → Y) '' connectedComponentIn s x : Set Y)
rwa₂ :
  ∀
    (this :
      Subset.{u_2} (α := Set Y) (connectedComponentIn ((⇑h : (a : X) → Y) '' s) ((h : (a : X) → Y) x) : Set Y)
        (image.{u_1, u_2} (α := X) ((⇑h : (a : X) → Y) : (a : X) → Y)
            (connectedComponentIn (preimage.{u_1, u_2} (β := Y) (⇑h : (a : X) → Y) ((⇑h : (a : X) → Y) '' s))
                ((h.symm : (a : Y) → X) ((h : (a : X) → Y) x : Y)) :
              Set X) :
          Set Y)),
    Subset.{u_2} (α := Set Y) (connectedComponentIn ((⇑h : (a : X) → Y) '' s) ((h : (a : X) → Y) x) : Set Y)
      ((⇑h : (a : X) → Y) '' connectedComponentIn s x : Set Y)
⊢ Subset.{u_2} (α := Set Y) (connectedComponentIn ((⇑h : (a : X) → Y) '' s) ((h : (a : X) → Y) x) : Set Y)
    ((⇑h : (a : X) → Y) '' connectedComponentIn s x : Set Y)
have rwa₃ : ∀
  (this :
    Subset.{u_2} (α := Set Y) (connectedComponentIn ((⇑h : (a : X) → Y) '' s) ((h : (a : X) → Y) x) : Set Y)
      ((⇑h : (a : X) → Y) '' connectedComponentIn s ((h.symm : (a : Y) → X) ((h : (a : X) → Y) x : Y)) : Set Y)),
  Subset.{u_2} (α := Set Y) (connectedComponentIn ((⇑h : (a : X) → Y) '' s) ((h : (a : X) → Y) x) : Set Y)
    ((⇑h : (a : X) → Y) '' connectedComponentIn s x : Set Y)
Tactic: rwa [image_subset_iff, h.preimage_symm, h.image_symm, h.preimage_image, h.symm_apply_apply]
    at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Homeomorph.Lemmas (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
h : X ≃ₜ Y
⊢ map (⇑h : (a : X) → Y) (cocompact X) = cocompact Y
have rw : map.{u_1, u_2} (α := X) (⇑h : (a : X) → Y) (comap (⇑h : (a : X) → Y) (cocompact Y)) = cocompact Y
Tactic: rw [← h.comap_cocompact, map_comap_of_surjective h.surjective]
-- Lean 4 proof step from Mathlib.Topology.Homeomorph.Lemmas (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
h : X ≃ₜ Y
rw : map.{u_1, u_2} (α := X) (⇑h : (a : X) → Y) (comap (⇑h : (a : X) → Y) (cocompact Y)) = cocompact Y
⊢ map (⇑h : (a : X) → Y) (cocompact X) = cocompact Y
have rw₁ : cocompact Y = cocompact Y
Tactic: rw [← h.comap_cocompact, map_comap_of_surjective h.surjective]
-- Lean 4 proof step from Mathlib.Topology.Homeomorph.Lemmas (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
h : X ≃ₜ Y
x : X
⊢ Eq (α := Filter Y) (map (⇑h : (a : X) → Y) (𝓝[≠] x) : Filter Y) (𝓝[≠] (h : (a : X) → Y) x : Filter Y)
have h₁ : Eq (α := Set Y) (singleton (α := Y) ((h : (a : X) → Y) x : Y))ᶜ (image (α := X) (⇑h : (a : X) → Y) {x}ᶜ)
Tactic: convert! h.isEmbedding.map_nhdsWithin_eq ({ x }ᶜ) x
-- Lean 4 proof step from Mathlib.Topology.Homeomorph.Lemmas (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
h : X ≃ₜ Y
x : X
⊢ Eq (α := Set Y) (singleton (α := Y) ((h : (a : X) → Y) x : Y))ᶜ (image (α := X) (⇑h : (a : X) → Y) {x}ᶜ)
have h₁ : Eq (α := Set Y) (singleton (α := Y) ((h : (a : X) → Y) x : Y))ᶜ (image (α := X) (⇑h : (a : X) → Y) {x})ᶜ
Tactic: rw [h.image_compl, Set.image_singleton]
-- Lean 4 proof step from Mathlib.Topology.Homeomorph.Lemmas (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
h : X ≃ₜ Y
x : X
h₁ : Eq (α := Set Y) (singleton (α := Y) ((h : (a : X) → Y) x : Y))ᶜ (image (α := X) (⇑h : (a : X) → Y) {x})ᶜ
⊢ Eq (α := Set Y) (singleton (α := Y) ((h : (a : X) → Y) x : Y))ᶜ (image (α := X) (⇑h : (a : X) → Y) {x}ᶜ)
have h₂ : Eq (α := Set Y) (singleton (α := Y) ((h : (a : X) → Y) x : Y))ᶜ (singleton (α := Y) ((h : (a : X) → Y) x : Y))ᶜ
Tactic: rw [h.image_compl, Set.image_singleton]
-- Lean 4 proof step from Mathlib.Topology.Homeomorph.Lemmas (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
h : X ≃ₜ Y
⊢ map (⇑h : (a : X) → Y) (coclosedCompact X) = coclosedCompact Y
have rw : map.{u_1, u_2} (α := X) (⇑h : (a : X) → Y) (comap (⇑h : (a : X) → Y) (coclosedCompact Y)) = coclosedCompact Y
Tactic: rw [← h.comap_coclosedCompact, map_comap_of_surjective h.surjective]
-- Lean 4 proof step from Mathlib.Topology.Homeomorph.Lemmas (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
h : X ≃ₜ Y
rw : map.{u_1, u_2} (α := X) (⇑h : (a : X) → Y) (comap (⇑h : (a : X) → Y) (coclosedCompact Y)) = coclosedCompact Y
⊢ map (⇑h : (a : X) → Y) (coclosedCompact X) = coclosedCompact Y
have rw₁ : coclosedCompact Y = coclosedCompact Y
Tactic: rw [← h.comap_coclosedCompact, map_comap_of_surjective h.surjective]
-- Lean 4 proof step from Mathlib.Topology.Homeomorph.Lemmas (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
i : LocallyConnectedSpace Y
h : X ≃ₜ Y
x : X
⊢ (𝓝 x).HasBasis
    (fun (s : Set Y) ↦ IsOpen[inst_1] s ∧ Membership.mem (α := Y) s ((h : (a : X) → Y) x : Y) ∧ IsConnected s)
    fun (x : Set Y) ↦ (⇑h.symm : (a : Y) → X) '' x
have rw : HasBasis.{u_1, u_2 + 1} (α := X)
  (map.{u_2, u_1} (α := Y) ((⇑h.symm : (a : Y) → X) : (a : Y) → X) (𝓝 ((h : (a : X) → Y) x) : Filter Y))
  (fun (s : Set Y) ↦ IsOpen[inst_1] s ∧ Membership.mem (α := Y) s ((h : (a : X) → Y) x : Y) ∧ IsConnected s)
  fun (x : Set Y) ↦ (⇑h.symm : (a : Y) → X) '' x
Tactic: rw [← h.symm_map_nhds_eq]
-- Lean 4 proof step from Mathlib.Topology.Homeomorph.Lemmas (hypothesis)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
i : LocallyConnectedSpace Y
h : X ≃ₜ Y
⊢ LocallyConnectedSpace X
have this : ∀ (x : X),
  (𝓝 x).HasBasis
    (fun (s : Set Y) ↦ IsOpen[inst_1] s ∧ Membership.mem (α := Y) s ((h : (a : X) → Y) x : Y) ∧ IsConnected s)
    fun (x : Set Y) ↦ (⇑h.symm : (a : Y) → X) '' x
Tactic: have : ∀ x, (𝓝 x).HasBasis (fun s ↦ IsOpen s ∧ h x ∈ s ∧ IsConnected s)
      (h.symm '' ·) := fun x ↦ by
    rw [← h.symm_map_nhds_eq]
    exact (i.1 _).map _
-- Lean 4 proof step from Mathlib.Topology.Homeomorph.Lemmas (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
i : LocallyConnectedSpace Y
h : X ≃ₜ Y
this :
  ∀ (x : X),
    (𝓝 x).HasBasis
      (fun (s : Set Y) ↦ IsOpen[inst_1] s ∧ Membership.mem (α := Y) s ((h : (a : X) → Y) x : Y) ∧ IsConnected s)
      fun (x : Set Y) ↦ (⇑h.symm : (a : Y) → X) '' x
⊢ LocallyConnectedSpace X
have refine : ∀ (x : X) (x_1 : Set Y)
  (hs : IsOpen[inst_1] x_1 ∧ Membership.mem (α := Y) x_1 ((h : (a : X) → Y) x : Y) ∧ IsConnected x_1),
  IsPreconnected.{u_1} (α := X) ((⇑h.symm : (a : Y) → X) '' x_1)
Tactic: refine locallyConnectedSpace_of_connected_bases _ _ this fun _ _ hs ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Homeomorph.Lemmas (goal)
Goal:
X : Type u_1
Y : Type u_2
W : Type u_3
Z : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace W
inst_3 : TopologicalSpace Z
X' : Type u_5
Y' : Type u_6
inst_4 : TopologicalSpace X'
inst_5 : TopologicalSpace Y'
S : Type u_7
T : Type u_8
A : S ⊕ T → Type u_9
inst_6 : (st : S ⊕ T) → TopologicalSpace (A st)
s : S
⊢ Continuous[instTopologicalSpaceProd, inst_6 (Sum.inl s)]
    fun (a : ((s : S) → A (Sum.inl s)) × ((t : T) → A (Sum.inr t))) ↦ (Equiv.sumPiEquivProdPi A).invFun a (Sum.inl s)
have inl : Continuous[instTopologicalSpaceProd, inst_6 (Sum.inl s)]
  fun (a : ((s : S) → A (Sum.inl s)) × ((t : T) → A (Sum.inr t))) ↦ a.1 s
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Topology.Homeomorph.Lemmas (goal)
Goal:
X : Type u_1
Y : Type u_2
W : Type u_3
Z : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace W
inst_3 : TopologicalSpace Z
X' : Type u_5
Y' : Type u_6
inst_4 : TopologicalSpace X'
inst_5 : TopologicalSpace Y'
S : Type u_7
T : Type u_8
A : S ⊕ T → Type u_9
inst_6 : (st : S ⊕ T) → TopologicalSpace (A st)
t : T
⊢ Continuous[instTopologicalSpaceProd, inst_6 (Sum.inr t)]
    fun (a : ((s : S) → A (Sum.inl s)) × ((t : T) → A (Sum.inr t))) ↦ (Equiv.sumPiEquivProdPi A).invFun a (Sum.inr t)
have inr : Continuous[instTopologicalSpaceProd, inst_6 (Sum.inr t)]
  fun (a : ((s : S) → A (Sum.inl s)) × ((t : T) → A (Sum.inr t))) ↦ a.2 t
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Topology.Homeomorph.Lemmas (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
m n : ℕ
⊢ Eq.{u_1 + 1} (α := (Fin m → X) × (Fin n → X) ≃ (Fin (m + n) → X)) (Fin.appendEquiv m n)
    (toEquiv
      (Homeomorph.trans (Homeomorph.symm sumArrowHomeomorphProdArrow)
        (piCongrLeft (Y := fun (x : Fin (m + n)) ↦ X) finSumFinEquiv)))
have a : Eq.{max 1 (u_1 + 1)} (α := (Fin (m + n) → X) ≃ (Fin m → X) × (Fin n → X)) (Equiv.symm (Fin.appendEquiv m n))
  (Equiv.symm
    (toEquiv
      (Homeomorph.trans (Homeomorph.symm sumArrowHomeomorphProdArrow)
        (piCongrLeft (Y := fun (x : Fin (m + n)) ↦ X) finSumFinEquiv))))
Tactic: apply Equiv.symm_bijective.injective
-- Lean 4 proof step from Mathlib.Topology.Homeomorph.Lemmas (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
m n : ℕ
⊢ Eq.{max 1 (u_1 + 1)} (α := (Fin (m + n) → X) ≃ (Fin m → X) × (Fin n → X)) (Equiv.symm (Fin.appendEquiv m n))
    (Equiv.symm
      (toEquiv
        (Homeomorph.trans (Homeomorph.symm sumArrowHomeomorphProdArrow)
          (piCongrLeft (Y := fun (x : Fin (m + n)) ↦ X) finSumFinEquiv))))
have a : ∀ (x : Fin (m + n) → X) (i : Fin m),
  Eq.{u_1 + 1} (α := X) (((Equiv.symm (Fin.appendEquiv m n) : (a : Fin (m + n) → X) → (Fin m → X) × (Fin n → X)) x).1 i)
    (((Equiv.symm
              (toEquiv
                (Homeomorph.trans (Homeomorph.symm sumArrowHomeomorphProdArrow)
                  (piCongrLeft (Y := fun (x : Fin (m + n)) ↦ X) finSumFinEquiv))) :
            (a : Fin (m + n) → X) → (Fin m → X) × (Fin n → X))
          x).1
      i)
Tactic: ext x i
-- Lean 4 proof step from Mathlib.Topology.Homeomorph.Lemmas (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
m n : ℕ
a :
  ∀ (x : Fin (m + n) → X) (i : Fin m),
    Eq.{u_1 + 1} (α := X)
      (((Equiv.symm (Fin.appendEquiv m n) : (a : Fin (m + n) → X) → (Fin m → X) × (Fin n → X)) x).1 i)
      (((Equiv.symm
                (toEquiv
                  (Homeomorph.trans (Homeomorph.symm sumArrowHomeomorphProdArrow)
                    (piCongrLeft (Y := fun (x : Fin (m + n)) ↦ X) finSumFinEquiv))) :
              (a : Fin (m + n) → X) → (Fin m → X) × (Fin n → X))
            x).1
        i)
⊢ Eq.{max 1 (u_1 + 1)} (α := (Fin (m + n) → X) ≃ (Fin m → X) × (Fin n → X)) (Equiv.symm (Fin.appendEquiv m n))
    (Equiv.symm
      (toEquiv
        (Homeomorph.trans (Homeomorph.symm sumArrowHomeomorphProdArrow)
          (piCongrLeft (Y := fun (x : Fin (m + n)) ↦ X) finSumFinEquiv))))
have a₁ : ∀ (x : Fin (m + n) → X) (i : Fin n),
  Eq.{u_1 + 1} (α := X) (((Equiv.symm (Fin.appendEquiv m n) : (a : Fin (m + n) → X) → (Fin m → X) × (Fin n → X)) x).2 i)
    (((Equiv.symm
              (toEquiv
                (Homeomorph.trans (Homeomorph.symm sumArrowHomeomorphProdArrow)
                  (piCongrLeft (Y := fun (x : Fin (m + n)) ↦ X) finSumFinEquiv))) :
            (a : Fin (m + n) → X) → (Fin m → X) × (Fin n → X))
          x).2
      i)
Tactic: ext x i
-- Lean 4 proof step from Mathlib.Topology.Homeomorph.Lemmas (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
m n : ℕ
⊢ Continuous[instTopologicalSpaceProd, Pi.topologicalSpace] fun (p : (Fin m → X) × (Fin n → X)) ↦ Fin.append p.1 p.2
have suffices : Continuous[instTopologicalSpaceProd, Pi.topologicalSpace]
  (⇑(Fin.appendEquiv m n) : (a : (Fin m → X) × (Fin n → X)) → Fin (m + n) → X)
Tactic: suffices Continuous (Fin.appendEquiv m n) by exact this
-- Lean 4 proof step from Mathlib.Topology.Homeomorph.Lemmas (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
m n : ℕ
⊢ Continuous[instTopologicalSpaceProd, Pi.topologicalSpace]
    (⇑(Fin.appendEquiv m n) : (a : (Fin m → X) × (Fin n → X)) → Fin (m + n) → X)
have rw : Continuous[instTopologicalSpaceProd, Pi.topologicalSpace]
  (⇑(toEquiv
        (Homeomorph.trans (Homeomorph.symm sumArrowHomeomorphProdArrow)
          (piCongrLeft (Y := fun (x : Fin (m + n)) ↦ X) finSumFinEquiv))) :
    (a : (Fin m → X) × (Fin n → X)) → Fin (m + n) → X)
Tactic: rw [Fin.appendEquiv_eq_homeomorph]
-- Lean 4 proof step from Mathlib.Topology.Homeomorph.Lemmas (goal)
Goal:
X : Type u_1
Y_1 : Type u_2
W : Type u_3
Z : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y_1
inst_2 : TopologicalSpace W
inst_3 : TopologicalSpace Z
X' : Type u_5
Y' : Type u_6
inst_4 : TopologicalSpace X'
inst_5 : TopologicalSpace Y'
ι : Type u_7
p : ι → Prop
Y : ι → Type u_8
inst_6 : (i : ι) → TopologicalSpace (Y i)
inst_7 : DecidablePred p
j : ι
⊢ Continuous[instTopologicalSpaceProd, inst_6 j]
    fun (a : ((i : { x : ι // p x }) → Y (↑i : ι)) × ((i : { x : ι // ¬p x }) → Y (↑i : ι))) ↦
    (Equiv.piEquivPiSubtypeProd p Y).invFun a j
have dsimp : Continuous[instTopologicalSpaceProd, inst_6 j]
  fun (a : ((i : { x : ι // p x }) → Y (↑i : ι)) × ((i : { x : ι // ¬p x }) → Y (↑i : ι))) ↦
  if h : p j then a.1 (Subtype.mk (p := fun (x : ι) ↦ p x) j h) else a.2 (Subtype.mk (p := fun (x : ι) ↦ ¬p x) j h)
Tactic: dsimp only [Equiv.piEquivPiSubtypeProd]