awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Homeomorph.Lemmas
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
h : X ≃ₜ Y
tdc : TotallyDisconnectedSpace X
⊢ TotallyDisconnectedSpace Y

Tactic:
(totallyDisconnectedSpace_iff Y).mpr
    (h.range_coe ▸ ((IsEmbedding.isTotallyDisconnected_range h.isEmbedding).mpr tdc))

Premises used: Iff.mpr, Homeomorph.isEmbedding, Eq.rec, Topology.IsEmbedding.isTotallyDisconnected_range, Homeomorph.range_coe, totallyDisconnectedSpace_iff
-- Module: Mathlib.Topology.Homeomorph.Lemmas
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
h : X ≃ₜ Y
x : X
⊢ Eq.{u_2 + 1} (α := Filter Y) (map (⇑h : (a : X) → Y) (𝓝[≠] x) : Filter Y)
    (𝓝[image (α := X) (⇑h : (a : X) → Y) {x}ᶜ] (h : (a : X) → Y) x : Filter Y)

Tactic:
h.isEmbedding.map_nhdsWithin_eq ({ x }ᶜ) x

Premises used: Homeomorph.isEmbedding, Compl.compl, Topology.IsEmbedding.map_nhdsWithin_eq, Singleton.singleton
-- Module: Mathlib.Topology.Homeomorph.Lemmas
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 (α := Filter Y) (map (⇑h : (a : X) → Y) (𝓝[≠] x) : Filter Y) (𝓝[≠] (h : (a : X) → Y) x : Filter Y)

Tactic:
convert! h.isEmbedding.map_nhdsWithin_eq ({ x }ᶜ) x

Premises used: Homeomorph.isEmbedding, Compl.compl, Topology.IsEmbedding.map_nhdsWithin_eq, Singleton.singleton
-- Module: Mathlib.Topology.Homeomorph.Lemmas
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})ᶜ
h₂ h₃ : Eq (α := Set Y) (singleton (α := Y) ((h : (a : X) → Y) x : Y))ᶜ (singleton (α := Y) ((h : (a : X) → Y) x : Y))ᶜ
⊢ 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]

Premises used: Set.image_singleton, Homeomorph.image_compl
-- Module: Mathlib.Topology.Homeomorph.Lemmas
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
h : X ≃ₜ Y
⊢ (coclosedCompact X).HasBasis (fun (s : Set Y) ↦ IsClosed[inst_1] s ∧ IsCompact s) fun (i : Set Y) ↦
    (⇑h : (a : X) → Y) ⁻¹' iᶜ

Tactic:
simpa [comp_def] using hasBasis_coclosedCompact.comp_surjective h.injective.preimage_surjective

Premises used: Function.Injective.preimage_surjective, Filter.hasBasis_coclosedCompact, Function.comp_def, Homeomorph.injective, Filter.HasBasis.comp_surjective
-- Module: Mathlib.Topology.Homeomorph.Lemmas
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
rw₁ rw₂ : coclosedCompact Y = coclosedCompact Y
⊢ map (⇑h : (a : X) → Y) (coclosedCompact X) = coclosedCompact Y

Tactic:
rw [← h.comap_coclosedCompact, map_comap_of_surjective h.surjective]

Premises used: Homeomorph.comap_coclosedCompact, Filter.map_comap_of_surjective, Homeomorph.surjective
-- Module: Mathlib.Topology.Homeomorph.Lemmas
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
i : LocallyConnectedSpace Y
h : X ≃ₜ Y
x : X
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
⊢ (𝓝 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:
rw [← h.symm_map_nhds_eq]

Premises used: Homeomorph.symm_map_nhds_eq
-- Module: Mathlib.Topology.Homeomorph.Lemmas
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
i : LocallyConnectedSpace Y
h : X ≃ₜ Y
x : X
⊢ 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:
(i.1 _).map _

Premises used: Filter.HasBasis.map, LocallyConnectedSpace.open_connected_basis
-- Module: Mathlib.Topology.Homeomorph.Lemmas
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
i : LocallyConnectedSpace Y
h : X ≃ₜ Y
x : X
⊢ 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:
exact (i.1 _).map _

Premises used: Filter.HasBasis.map, LocallyConnectedSpace.open_connected_basis
-- Module: Mathlib.Topology.Homeomorph.Lemmas
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

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 _
-- Module: Mathlib.Topology.Homeomorph.Lemmas
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

Tactic:
locallyConnectedSpace_of_connected_bases _ _ this fun _ _ hs ↦ ?_

Premises used: locallyConnectedSpace_of_connected_bases
-- Module: Mathlib.Topology.Homeomorph.Lemmas
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
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)
⊢ LocallyConnectedSpace X

Tactic:
refine locallyConnectedSpace_of_connected_bases _ _ this fun _ _ hs ↦ ?_

Premises used: locallyConnectedSpace_of_connected_bases
-- Module: Mathlib.Topology.Homeomorph.Lemmas
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
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:
hs.2.2.2.image _ h.symm.continuous.continuousOn

Premises used: Continuous.continuousOn, Homeomorph.continuous, IsPreconnected.image, And.right, Homeomorph.symm
-- Module: Mathlib.Topology.Homeomorph.Lemmas
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
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:
exact hs.2.2.2.image _ h.symm.continuous.continuousOn

Premises used: Continuous.continuousOn, Homeomorph.continuous, IsPreconnected.image, And.right, Homeomorph.symm
-- Module: Mathlib.Topology.Homeomorph.Lemmas
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
h : X ≃ₜ Y
⊢ LocallyCompactSpace X ↔ LocallyCompactSpace Y

Tactic:
⟨fun _ => h.symm.isOpenEmbedding.locallyCompactSpace,
    fun _ => h.isClosedEmbedding.locallyCompactSpace⟩

Premises used: Topology.IsOpenEmbedding.locallyCompactSpace, Homeomorph.symm, Iff.intro, Homeomorph.isOpenEmbedding, Homeomorph.isClosedEmbedding, Topology.IsClosedEmbedding.locallyCompactSpace
-- Module: Mathlib.Topology.Homeomorph.Lemmas
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
h : X ≃ₜ Y
⊢ LocallyCompactSpace X ↔ LocallyCompactSpace Y

Tactic:
exact ⟨fun _ => h.symm.isOpenEmbedding.locallyCompactSpace,
    fun _ => h.isClosedEmbedding.locallyCompactSpace⟩
-- Module: Mathlib.Topology.Homeomorph.Lemmas
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
h : X ≃ₜ Y
f : Z → X
s : Set Z
⊢ ContinuousOn.{u_4, u_2} (Y := Y) ((⇑h : (a : X) → Y) ∘ f) s ↔ ContinuousOn f s

Tactic:
h.isInducing.continuousOn_iff.symm

Premises used: Homeomorph.isInducing, Topology.IsInducing.continuousOn_iff, Iff.symm
-- Module: Mathlib.Topology.Homeomorph.Lemmas
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
h : X ≃ₜ Y
f : Z → X
s : Set Z
z : Z
⊢ ContinuousWithinAt f s z ↔ ContinuousWithinAt.{u_4, u_2} (Y := Y) ((⇑h : (a : X) → Y) ∘ f) s z

Tactic:
h.isInducing.continuousWithinAt_iff

Premises used: Homeomorph.isInducing, Topology.IsInducing.continuousWithinAt_iff
-- Module: Mathlib.Topology.Homeomorph.Lemmas
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
p : X → Prop
q : Y → Prop
h : X ≃ₜ Y
h_iff : ∀ (x : X), p x ↔ q ((h : (a : X) → Y) x)
⊢ (h.subtype (p := p) (q := q) h_iff).toEquiv = h.subtypeEquiv (p := p) (q := q) h_iff

Tactic:
rfl

Premises used: Equiv.subtypeEquiv, rfl
-- Module: Mathlib.Topology.Homeomorph.Lemmas
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : Unique Y
⊢ Eq (α := (a : X × Y) → X) (⇑(prodUnique X Y) : (a : X × Y) → X) Prod.fst

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Homeomorph.Lemmas
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : Unique X
⊢ Eq (α := (a : X × Y) → Y) (⇑(uniqueProd X Y) : (a : X × Y) → Y) Prod.snd

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Homeomorph.Lemmas
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
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
⊢ 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)

Tactic:
dsimp
-- Module: Mathlib.Topology.Homeomorph.Lemmas
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
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
⊢ 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)

Tactic:
dsimp
-- Module: Mathlib.Topology.Homeomorph.Lemmas
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))) ↦ a.1 s

Tactic:
fun_prop
-- Module: Mathlib.Topology.Homeomorph.Lemmas
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))) ↦ a.2 t

Tactic:
fun_prop
-- Module: Mathlib.Topology.Homeomorph.Lemmas
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
ι' : Type u_8
Y : ι' → Type u_9
inst_6 : (j : ι') → TopologicalSpace (Y j)
e : ι ≃ ι'
i : ι
⊢ Continuous[Pi.topologicalSpace, inst_6 ((e : (a : ι) → ι') i)] fun (a : (i : ι) → Y ((e : (a : ι) → ι') i)) ↦
    (Equiv.piCongrLeft Y e).toFun a ((e : (a : ι) → ι') i)

Tactic:
simpa only [Equiv.toFun_as_coe, Equiv.piCongrLeft_apply_apply] using continuous_apply i

Premises used: Equiv.toFun_as_coe, continuous_apply, Equiv.piCongrLeft_apply_apply
-- Module: Mathlib.Topology.Homeomorph.Lemmas
Goal:
ι : Type u_7
X : ι → Type u_8
inst : (i : ι) → TopologicalSpace (X i)
⊢ Eq (α := ((i : ι) → X ((Equiv.refl ι : (a : ι) → ι) i)) ≃ₜ ((j : ι) → X j)) (piCongrLeft (Y := X) (Equiv.refl ι))
    (Homeomorph.refl ((i : ι) → X i))

Tactic:
rfl

Premises used: Homeomorph.piCongrLeft, Equiv.piCongrLeft, Homeomorph.refl, Equiv.symm, Equiv.refl, rfl
-- Module: Mathlib.Topology.Homeomorph.Lemmas
Goal:
ι : Type u_7
ι' : Type u_8
Y : ι' → Type u_9
inst : (j : ι') → TopologicalSpace (Y j)
e : ι ≃ ι'
⊢ Eq (α := (a : (j : ι') → Y j) → (i : ι) → Y ((e : (a : ι) → ι') i))
    (⇑(Homeomorph.symm (piCongrLeft (Y := Y) e)) : (a : (j : ι') → Y j) → (i : ι) → Y ((e : (a : ι) → ι') i))
    fun (x1 : (j : ι') → Y j) (x2 : ι) ↦ x1 ((e : (a : ι) → ι') x2)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Homeomorph.Lemmas
Goal:
ι : Type u_7
ι' : Type u_8
Y : ι' → Type u_9
inst : (j : ι') → TopologicalSpace (Y j)
e : ι ≃ ι'
x : (i : ι) → Y ((e : (a : ι) → ι') i)
i : ι
⊢ (piCongrLeft (Y := Y) e : (a : (i : ι) → Y ((e : (a : ι) → ι') i)) → (j : ι') → Y j) x ((e : (a : ι) → ι') i) = x i

Tactic:
Equiv.piCongrLeft_apply_apply ..

Premises used: Equiv.piCongrLeft_apply_apply
-- Module: Mathlib.Topology.Homeomorph.Lemmas
Goal:
ι : Type u_7
Y₁ : ι → Type u_8
Y₂ : ι → Type u_9
inst : (i : ι) → TopologicalSpace (Y₁ i)
inst_1 : (i : ι) → TopologicalSpace (Y₂ i)
F : (i : ι) → Homeomorph.{u_8, u_9} (Y₁ i) (Y₂ i)
⊢ (piCongrRight (Y₁ := Y₁) (Y₂ := Y₂) F).symm = piCongrRight (Y₁ := Y₂) (Y₂ := Y₁) fun (i : ι) ↦ (F i).symm

Tactic:
rfl

Premises used: Homeomorph.piCongrRight, Pi.map, Homeomorph.symm, Equiv.piCongrRight, Equiv.symm, rfl
-- Module: Mathlib.Topology.Homeomorph.Lemmas
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'
ι : Type u_7
ι' : Type u_8
⊢ Continuous[Pi.topologicalSpace, instTopologicalSpaceProd] fun (f : ι ⊕ ι' → X) ↦ (f ∘ Sum.inl, f ∘ Sum.inr)

Tactic:
fun_prop
-- Module: Mathlib.Topology.Homeomorph.Lemmas
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'
ι : Type u_7
ι' : Type u_8
i_1 : ι ⊕ ι'
i : ι
⊢ Continuous[instTopologicalSpaceProd, inst] fun (a : (ι → X) × (ι' → X)) ↦
    (Equiv.sumArrowEquivProdArrow ι ι' X).invFun a (Sum.inl i)

Tactic:
apply (continuous_apply _).comp' continuous_fst

Premises used: Continuous.comp', continuous_fst, continuous_apply
-- Module: Mathlib.Topology.Homeomorph.Lemmas
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'
ι : Type u_7
ι' : Type u_8
i_1 : ι ⊕ ι'
i : ι'
⊢ Continuous[instTopologicalSpaceProd, inst] fun (a : (ι → X) × (ι' → X)) ↦
    (Equiv.sumArrowEquivProdArrow ι ι' X).invFun a (Sum.inr i)

Tactic:
apply (continuous_apply _).comp' continuous_snd

Premises used: Continuous.comp', continuous_snd, continuous_apply
-- Module: Mathlib.Topology.Homeomorph.Lemmas
Goal:
X : Type u_1
inst : TopologicalSpace X
m n : ℕ
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))))
⊢ 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)))

Tactic:
apply Equiv.symm_bijective.injective

Premises used: Function.Bijective.injective, Equiv.symm_bijective
-- Module: Mathlib.Topology.Homeomorph.Lemmas
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)
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)
⊢ 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:
ext x i
-- Module: Mathlib.Topology.Homeomorph.Lemmas
Goal:
X : Type u_1
inst : TopologicalSpace X
m n : ℕ
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:
simp
-- Module: Mathlib.Topology.Homeomorph.Lemmas
Goal:
X : Type u_1
inst : TopologicalSpace X
m n : ℕ
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:
simp
-- Module: Mathlib.Topology.Homeomorph.Lemmas
Goal:
X : Type u_1
inst : TopologicalSpace X
m n : ℕ
this :
  Continuous[instTopologicalSpaceProd, Pi.topologicalSpace]
    (⇑(Fin.appendEquiv m n) : (a : (Fin m → X) × (Fin n → X)) → Fin (m + n) → X)
⊢ Continuous[instTopologicalSpaceProd, Pi.topologicalSpace] fun (p : (Fin m → X) × (Fin n → X)) ↦ Fin.append p.1 p.2

Tactic:
this

Premises used: Fin.addCases, dite, Fin.append
-- Module: Mathlib.Topology.Homeomorph.Lemmas
Goal:
X : Type u_1
inst : TopologicalSpace X
m n : ℕ
this :
  Continuous[instTopologicalSpaceProd, Pi.topologicalSpace]
    (⇑(Fin.appendEquiv m n) : (a : (Fin m → X) × (Fin n → X)) → Fin (m + n) → X)
⊢ Continuous[instTopologicalSpaceProd, Pi.topologicalSpace] fun (p : (Fin m → X) × (Fin n → X)) ↦ Fin.append p.1 p.2

Tactic:
exact this
-- Module: Mathlib.Topology.Homeomorph.Lemmas
Goal:
X : Type u_1
inst : TopologicalSpace X
m n : ℕ
suffices :
  Continuous[instTopologicalSpaceProd, Pi.topologicalSpace]
    (⇑(Fin.appendEquiv m n) : (a : (Fin m → X) × (Fin n → X)) → Fin (m + n) → X)
⊢ Continuous[instTopologicalSpaceProd, Pi.topologicalSpace] fun (p : (Fin m → X) × (Fin n → X)) ↦ Fin.append p.1 p.2

Tactic:
suffices Continuous (Fin.appendEquiv m n) by exact this
-- Module: Mathlib.Topology.Homeomorph.Lemmas
Goal:
X : Type u_1
inst : TopologicalSpace X
m n : ℕ
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)
⊢ Continuous[instTopologicalSpaceProd, Pi.topologicalSpace]
    (⇑(Fin.appendEquiv m n) : (a : (Fin m → X) × (Fin n → X)) → Fin (m + n) → X)

Tactic:
rw [Fin.appendEquiv_eq_homeomorph]

Premises used: _private.0.Fin.appendEquiv_eq_homeomorph
-- Module: Mathlib.Topology.Homeomorph.Lemmas
Goal:
X : Type u_1
inst : TopologicalSpace X
m n : ℕ
⊢ 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:
Homeomorph.continuous_toFun _

Premises used: Homeomorph.continuous_toFun
-- Module: Mathlib.Topology.Homeomorph.Lemmas
Goal:
X : Type u_1
inst : TopologicalSpace X
m n : ℕ
⊢ 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:
exact Homeomorph.continuous_toFun _

Premises used: Homeomorph.continuous_toFun
-- Module: Mathlib.Topology.Homeomorph.Lemmas
Goal:
X : Type u_1
inst : TopologicalSpace X
m n : ℕ
⊢ Eq.{u_1 + 1} (α := (Fin m → X) × (Fin n → X) ≃ (Fin (m + n) → X)) (toEquiv (Fin.appendHomeomorph m n))
    (Fin.appendEquiv m n)

Tactic:
rfl

Premises used: Fin.appendEquiv, rfl