awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst : (i : ι) → TopologicalSpace (R i)
hAopen : ∀ (i : ι), IsOpen[inst i] (A i)
p : ι → Prop
simp_rw :
  ∀ (i : Set ι) (i_1 : cofinite ≤ 𝓟 i),
    IsOpen[topologicalSpace R A (𝓟 i)]
      (inclusion R A i_1 ⁻¹' {f : Πʳ (i : ι), [R i, A i] | ∀ (i : ι), p i → (↑f : (i : ι) → R i) i ∈ A i})
⊢ IsOpen[topologicalSpace R A cofinite]
    {f : Πʳ (i : ι), [R i, A i] | ∀ (i : ι), p i → (↑f : (i : ι) → (fun (i : ι) ↦ R i) i) i ∈ A i}

Tactic:
simp_rw +instances [topologicalSpace_eq_iSup cofinite, isOpen_iSup_iff, isOpen_coinduced]

Premises used: isOpen_iSup_iff, isOpen_coinduced, Filter.cofinite, RestrictedProduct.topologicalSpace_eq_iSup
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst : (i : ι) → TopologicalSpace (R i)
hAopen : ∀ (i : ι), IsOpen[inst i] (A i)
p : ι → Prop
⊢ ∀ (i : Set ι) (i_1 : cofinite ≤ 𝓟 i),
    IsOpen[topologicalSpace R A (𝓟 i)]
      (inclusion R A i_1 ⁻¹' {f : Πʳ (i : ι), [R i, A i] | ∀ (i : ι), p i → (↑f : (i : ι) → R i) i ∈ A i})

Tactic:
fun S hS ↦ isOpen_forall_imp_mem_of_principal hAopen hS

Premises used: Set.Mem, setOf, Set.preimage, RestrictedProduct.isOpen_forall_imp_mem_of_principal
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst : (i : ι) → TopologicalSpace (R i)
hAopen : ∀ (i : ι), IsOpen[inst i] (A i)
p : ι → Prop
⊢ ∀ (i : Set ι) (i_1 : cofinite ≤ 𝓟 i),
    IsOpen[topologicalSpace R A (𝓟 i)]
      (inclusion R A i_1 ⁻¹' {f : Πʳ (i : ι), [R i, A i] | ∀ (i : ι), p i → (↑f : (i : ι) → R i) i ∈ A i})

Tactic:
exact fun S hS ↦ isOpen_forall_imp_mem_of_principal hAopen hS

Premises used: RestrictedProduct.isOpen_forall_imp_mem_of_principal
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst : (i : ι) → TopologicalSpace (R i)
hAopen : ∀ (i : ι), IsOpen[inst i] (A i)
simp_rw :
  ∀ (i : Set ι) (i_1 : cofinite ≤ 𝓟 i),
    IsOpen[topologicalSpace R A (𝓟 i)]
      (inclusion R A i_1 ⁻¹' {f : Πʳ (i : ι), [R i, A i] | ∀ (i : ι), (↑f : (i : ι) → R i) i ∈ A i})
⊢ IsOpen[topologicalSpace R A cofinite]
    {f : Πʳ (i : ι), [R i, A i] | ∀ (i : ι), (↑f : (i : ι) → (fun (i : ι) ↦ R i) i) i ∈ A i}

Tactic:
simp_rw +instances [topologicalSpace_eq_iSup cofinite, isOpen_iSup_iff, isOpen_coinduced]

Premises used: isOpen_iSup_iff, isOpen_coinduced, Filter.cofinite, RestrictedProduct.topologicalSpace_eq_iSup
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst : (i : ι) → TopologicalSpace (R i)
hAopen : ∀ (i : ι), IsOpen[inst i] (A i)
⊢ ∀ (i : Set ι) (i_1 : cofinite ≤ 𝓟 i),
    IsOpen[topologicalSpace R A (𝓟 i)]
      (inclusion R A i_1 ⁻¹' {f : Πʳ (i : ι), [R i, A i] | ∀ (i : ι), (↑f : (i : ι) → R i) i ∈ A i})

Tactic:
fun S hS ↦ isOpen_forall_mem_of_principal hAopen hS

Premises used: RestrictedProduct.isOpen_forall_mem_of_principal, Set.Mem, setOf, Set.preimage
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst : (i : ι) → TopologicalSpace (R i)
hAopen : ∀ (i : ι), IsOpen[inst i] (A i)
⊢ ∀ (i : Set ι) (i_1 : cofinite ≤ 𝓟 i),
    IsOpen[topologicalSpace R A (𝓟 i)]
      (inclusion R A i_1 ⁻¹' {f : Πʳ (i : ι), [R i, A i] | ∀ (i : ι), (↑f : (i : ι) → R i) i ∈ A i})

Tactic:
exact fun S hS ↦ isOpen_forall_mem_of_principal hAopen hS

Premises used: RestrictedProduct.isOpen_forall_mem_of_principal
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst : (i : ι) → TopologicalSpace (R i)
hAopen : ∀ (i : ι), IsOpen[inst i] (A i)
S : Set ι
hS : cofinite ≤ 𝓟 S
rw : IsOpen[topologicalSpace R A cofinite] {x : Πʳ (i : ι), [R i, A i] | ∀ᶠ (i : ι) in 𝓟 S, (x : (a : ι) → R a) i ∈ A i}
⊢ IsOpen[topologicalSpace R A cofinite] (range (inclusion R A hS))

Tactic:
rw [range_inclusion]

Premises used: RestrictedProduct.range_inclusion
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst : (i : ι) → TopologicalSpace (R i)
hAopen : ∀ (i : ι), IsOpen[inst i] (A i)
S : Set ι
hS : cofinite ≤ 𝓟 S
⊢ IsOpen[topologicalSpace R A cofinite] {x : Πʳ (i : ι), [R i, A i] | ∀ᶠ (i : ι) in 𝓟 S, (x : (a : ι) → R a) i ∈ A i}

Tactic:
isOpen_forall_imp_mem hAopen

Premises used: Set.Mem, Filter.Eventually, setOf, RestrictedProduct.isOpen_forall_imp_mem, Set.Subset
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst : (i : ι) → TopologicalSpace (R i)
hAopen : ∀ (i : ι), IsOpen[inst i] (A i)
S : Set ι
hS : cofinite ≤ 𝓟 S
⊢ IsOpen[topologicalSpace R A cofinite] {x : Πʳ (i : ι), [R i, A i] | ∀ᶠ (i : ι) in 𝓟 S, (x : (a : ι) → R a) i ∈ A i}

Tactic:
exact isOpen_forall_imp_mem hAopen

Premises used: RestrictedProduct.isOpen_forall_imp_mem
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst : (i : ι) → TopologicalSpace (R i)
hAopen : ∀ (i : ι), IsOpen[inst i] (A i)
rw :
  IsOpen[topologicalSpace R A cofinite]
    {f : Πʳ (i : ι), [R i, A i] | ∀ (i : ι), (↑f : (i : ι) → (fun (i : ι) ↦ R i) i) i ∈ A i}
⊢ IsOpen[topologicalSpace R A cofinite] (range (structureMap R A cofinite))

Tactic:
rw [range_structureMap]

Premises used: RestrictedProduct.range_structureMap
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst : (i : ι) → TopologicalSpace (R i)
hAopen : ∀ (i : ι), IsOpen[inst i] (A i)
⊢ IsOpen[topologicalSpace R A cofinite]
    {f : Πʳ (i : ι), [R i, A i] | ∀ (i : ι), (↑f : (i : ι) → (fun (i : ι) ↦ R i) i) i ∈ A i}

Tactic:
isOpen_forall_mem hAopen

Premises used: setOf, RestrictedProduct.isOpen_forall_mem
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst : (i : ι) → TopologicalSpace (R i)
hAopen : ∀ (i : ι), IsOpen[inst i] (A i)
⊢ IsOpen[topologicalSpace R A cofinite]
    {f : Πʳ (i : ι), [R i, A i] | ∀ (i : ι), (↑f : (i : ι) → (fun (i : ι) ↦ R i) i) i ∈ A i}

Tactic:
exact isOpen_forall_mem hAopen

Premises used: RestrictedProduct.isOpen_forall_mem
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst : (i : ι) → TopologicalSpace (R i)
hAopen : ∀ (i : ι), IsOpen[inst i] (A i)
S : Set ι
hS : cofinite ≤ 𝓟 S
x : Πʳ (i : ι), [R i, A i]_[𝓟 S]
rw rw₁ : 𝓝 (inclusion R A hS x) = 𝓝 (inclusion R A hS x)
⊢ 𝓝 (inclusion R A hS x) = Filter.map (inclusion R A hS) (𝓝 x)

Tactic:
rw [isOpenEmbedding_inclusion_principal hAopen hS |>.map_nhds_eq x]

Premises used: Topology.IsOpenEmbedding.map_nhds_eq, RestrictedProduct.isOpenEmbedding_inclusion_principal
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst : (i : ι) → TopologicalSpace (R i)
hAopen : ∀ (i : ι), IsOpen[inst i] (A i)
x : (i : ι) → (↑(A i) : Type u_2)
rw rw₁ : Eq (α := Filter Πʳ (i : ι), [R i, A i]) (𝓝 (structureMap R A cofinite x)) (𝓝 (structureMap R A cofinite x))
⊢ Eq (α := Filter Πʳ (i : ι), [R i, A i]) (𝓝 (structureMap R A cofinite x))
    (Filter.map (structureMap R A cofinite) (𝓝 x))

Tactic:
rw [isOpenEmbedding_structureMap hAopen |>.map_nhds_eq x]

Premises used: Topology.IsOpenEmbedding.map_nhds_eq, RestrictedProduct.isOpenEmbedding_structureMap
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst : (i : ι) → TopologicalSpace (R i)
hAopen : ∀ (i : ι), IsOpen[inst i] (A i)
inst_1 : ∀ (i : ι), WeaklyLocallyCompactSpace.{u_2} (R i)
hAcompact : ∀ᶠ (i : ι) in cofinite, IsCompact (A i)
x : Πʳ (i : ι), [R i, A i]
S : Set ι := {i : ι | IsCompact (A i) ∧ (x : (a : ι) → R a) i ∈ A i}
⊢ cofinite ≤ 𝓟 S

Tactic:
have hS : cofinite ≤ 𝓟 S := le_principal_iff.mpr (hAcompact.and x.2)
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst : (i : ι) → TopologicalSpace (R i)
hAopen : ∀ (i : ι), IsOpen[inst i] (A i)
inst_1 : ∀ (i : ι), WeaklyLocallyCompactSpace.{u_2} (R i)
hAcompact : ∀ᶠ (i : ι) in cofinite, IsCompact (A i)
x : Πʳ (i : ι), [R i, A i]
S : Set ι := {i : ι | IsCompact (A i) ∧ (x : (a : ι) → R a) i ∈ A i}
hS : cofinite ≤ 𝓟 S
⊢ ∀ i ∈ S, (x : (a : ι) → R a) i ∈ A i

Tactic:
have hSx : ∀ i ∈ S, x i ∈ A i := fun i hi ↦ hi.2
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst : (i : ι) → TopologicalSpace (R i)
hAopen : ∀ (i : ι), IsOpen[inst i] (A i)
inst_1 : ∀ (i : ι), WeaklyLocallyCompactSpace.{u_2} (R i)
hAcompact : ∀ᶠ (i : ι) in cofinite, IsCompact (A i)
x : Πʳ (i : ι), [R i, A i]
S : Set ι := {i : ι | IsCompact (A i) ∧ (x : (a : ι) → R a) i ∈ A i}
hS : cofinite ≤ 𝓟 S
hSx : ∀ i ∈ S, (x : (a : ι) → R a) i ∈ A i
⊢ ∀ i ∈ S, IsCompact (A i)

Tactic:
have hSA : ∀ i ∈ S, IsCompact (A i) := fun i hi ↦ hi.1
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst : (i : ι) → TopologicalSpace (R i)
hAopen : ∀ (i : ι), IsOpen[inst i] (A i)
inst_1 : ∀ (i : ι), WeaklyLocallyCompactSpace.{u_2} (R i)
hAcompact : ∀ᶠ (i : ι) in cofinite, IsCompact (A i)
x : Πʳ (i : ι), [R i, A i]
S : Set ι := {i : ι | IsCompact (A i) ∧ (x : (a : ι) → R a) i ∈ A i}
hS : cofinite ≤ 𝓟 S
hSx : ∀ i ∈ S, (x : (a : ι) → R a) i ∈ A i
hSA : ∀ i ∈ S, IsCompact (A i)
⊢ WeaklyLocallyCompactSpace Πʳ (i : ι), [R i, A i]_[𝓟 S]

Tactic:
haveI := weaklyLocallyCompactSpace_of_principal hS hSA
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst : (i : ι) → TopologicalSpace (R i)
hAopen : ∀ (i : ι), IsOpen[inst i] (A i)
inst_1 : ∀ (i : ι), WeaklyLocallyCompactSpace.{u_2} (R i)
hAcompact : ∀ᶠ (i : ι) in cofinite, IsCompact (A i)
x : Πʳ (i : ι), [R i, A i]
S : Set ι := {i : ι | IsCompact (A i) ∧ (x : (a : ι) → R a) i ∈ A i}
hS : cofinite ≤ 𝓟 S
hSx : ∀ i ∈ S, (x : (a : ι) → R a) i ∈ A i
hSA : ∀ i ∈ S, IsCompact (A i)
this : WeaklyLocallyCompactSpace Πʳ (i : ι), [R i, A i]_[𝓟 S]
rcases :
  ∀ (x' : Πʳ (i : ι), [R i, A i]_[𝓟 S]) (hxx' : inclusion R A hS x' = x),
    ∃ (s : Set Πʳ (i : ι), [R i, A i]), IsCompact s ∧ s ∈ 𝓝 x
⊢ ∃ (s : Set Πʳ (i : ι), [R i, A i]), IsCompact s ∧ s ∈ 𝓝 x

Tactic:
rcases exists_inclusion_eq_of_eventually R A hS hSx with ⟨x', hxx'⟩

Premises used: RestrictedProduct.exists_inclusion_eq_of_eventually
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst : (i : ι) → TopologicalSpace (R i)
hAopen : ∀ (i : ι), IsOpen[inst i] (A i)
inst_1 : ∀ (i : ι), WeaklyLocallyCompactSpace.{u_2} (R i)
hAcompact : ∀ᶠ (i : ι) in cofinite, IsCompact (A i)
x : Πʳ (i : ι), [R i, A i]
S : Set ι := {i : ι | IsCompact (A i) ∧ (x : (a : ι) → R a) i ∈ A i}
hS : cofinite ≤ 𝓟 S
hSx : ∀ i ∈ S, (x : (a : ι) → R a) i ∈ A i
hSA : ∀ i ∈ S, IsCompact (A i)
this : WeaklyLocallyCompactSpace Πʳ (i : ι), [R i, A i]_[𝓟 S]
x' : Πʳ (i : ι), [R i, A i]_[𝓟 S]
hxx' : inclusion R A hS x' = x
rw : ∃ (s : Set Πʳ (i : ι), [R i, A i]), IsCompact s ∧ s ∈ Filter.map (inclusion R A hS) (𝓝 x')
⊢ ∃ (s : Set Πʳ (i : ι), [R i, A i]), IsCompact s ∧ s ∈ 𝓝 x

Tactic:
rw [← hxx', nhds_eq_map_inclusion hAopen]

Premises used: RestrictedProduct.nhds_eq_map_inclusion
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst : (i : ι) → TopologicalSpace (R i)
hAopen : ∀ (i : ι), IsOpen[inst i] (A i)
inst_1 : ∀ (i : ι), WeaklyLocallyCompactSpace.{u_2} (R i)
hAcompact : ∀ᶠ (i : ι) in cofinite, IsCompact (A i)
x : Πʳ (i : ι), [R i, A i]
S : Set ι := {i : ι | IsCompact (A i) ∧ (x : (a : ι) → R a) i ∈ A i}
hS : cofinite ≤ 𝓟 S
hSx : ∀ i ∈ S, (x : (a : ι) → R a) i ∈ A i
hSA : ∀ i ∈ S, IsCompact (A i)
this : WeaklyLocallyCompactSpace Πʳ (i : ι), [R i, A i]_[𝓟 S]
x' : Πʳ (i : ι), [R i, A i]_[𝓟 S]
hxx' : inclusion R A hS x' = x
rcases :
  ∀ (K : Set Πʳ (i : ι), [R i, A i]_[𝓟 S]) (K_compact : IsCompact K) (hK : K ∈ 𝓝 x'),
    ∃ (s : Set Πʳ (i : ι), [R i, A i]), IsCompact s ∧ s ∈ Filter.map (inclusion R A hS) (𝓝 x')
⊢ ∃ (s : Set Πʳ (i : ι), [R i, A i]), IsCompact s ∧ s ∈ Filter.map (inclusion R A hS) (𝓝 x')

Tactic:
rcases exists_compact_mem_nhds x' with ⟨K, K_compact, hK⟩

Premises used: WeaklyLocallyCompactSpace.exists_compact_mem_nhds
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst : (i : ι) → TopologicalSpace (R i)
hAopen : ∀ (i : ι), IsOpen[inst i] (A i)
inst_1 : ∀ (i : ι), WeaklyLocallyCompactSpace.{u_2} (R i)
hAcompact : ∀ᶠ (i : ι) in cofinite, IsCompact (A i)
x : Πʳ (i : ι), [R i, A i]
S : Set ι := {i : ι | IsCompact (A i) ∧ (x : (a : ι) → R a) i ∈ A i}
hS : cofinite ≤ 𝓟 S
hSx : ∀ i ∈ S, (x : (a : ι) → R a) i ∈ A i
hSA : ∀ i ∈ S, IsCompact (A i)
this : WeaklyLocallyCompactSpace Πʳ (i : ι), [R i, A i]_[𝓟 S]
x' : Πʳ (i : ι), [R i, A i]_[𝓟 S]
hxx' : inclusion R A hS x' = x
K : Set Πʳ (i : ι), [R i, A i]_[𝓟 S]
K_compact : IsCompact K
hK : K ∈ 𝓝 x'
⊢ ∃ (s : Set Πʳ (i : ι), [R i, A i]), IsCompact s ∧ s ∈ Filter.map (inclusion R A hS) (𝓝 x')

Tactic:
⟨inclusion R A hS '' K, K_compact.image (continuous_inclusion hS), image_mem_map hK⟩

Premises used: RestrictedProduct.inclusion, Filter.image_mem_map, RestrictedProduct.continuous_inclusion, And.intro, Exists.intro, Set.image, IsCompact.image
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst : (i : ι) → TopologicalSpace (R i)
hAopen : ∀ (i : ι), IsOpen[inst i] (A i)
inst_1 : ∀ (i : ι), WeaklyLocallyCompactSpace.{u_2} (R i)
hAcompact : ∀ᶠ (i : ι) in cofinite, IsCompact (A i)
x : Πʳ (i : ι), [R i, A i]
S : Set ι := {i : ι | IsCompact (A i) ∧ (x : (a : ι) → R a) i ∈ A i}
hS : cofinite ≤ 𝓟 S
hSx : ∀ i ∈ S, (x : (a : ι) → R a) i ∈ A i
hSA : ∀ i ∈ S, IsCompact (A i)
this : WeaklyLocallyCompactSpace Πʳ (i : ι), [R i, A i]_[𝓟 S]
x' : Πʳ (i : ι), [R i, A i]_[𝓟 S]
hxx' : inclusion R A hS x' = x
K : Set Πʳ (i : ι), [R i, A i]_[𝓟 S]
K_compact : IsCompact K
hK : K ∈ 𝓝 x'
⊢ ∃ (s : Set Πʳ (i : ι), [R i, A i]), IsCompact s ∧ s ∈ Filter.map (inclusion R A hS) (𝓝 x')

Tactic:
exact ⟨inclusion R A hS '' K, K_compact.image (continuous_inclusion hS), image_mem_map hK⟩
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
𝓕_1 𝓖 : Filter ι
R' : ?m.1
A' : ?m.2
𝓕 : Filter ι
inst : (i : ι) → TopologicalSpace (R i)
hAopen_1 : ∀ (i : ι), IsOpen[inst i] (A i)
hAopen : Fact (∀ (i : ι), IsOpen[inst i] (A i))
inst_1 : ∀ (i : ι), WeaklyLocallyCompactSpace.{u_2} (R i)
hAcompact : ∀ (i : ι), CompactSpace.{u_2} (↑(A i) : Type u_2)
⊢ WeaklyLocallyCompactSpace Πʳ (i : ι), [R i, A i]

Tactic:
weaklyLocallyCompactSpace_of_cofinite hAopen.out <|
    .of_forall fun _ ↦ isCompact_iff_compactSpace.mpr inferInstance

Premises used: Iff.mpr, isCompact_iff_compactSpace, inferInstance, Filter.Eventually.of_forall, RestrictedProduct.weaklyLocallyCompactSpace_of_cofinite, Fact.out
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst : (i : ι) → TopologicalSpace (R i)
hAopen : ∀ (i : ι), IsOpen[inst i] (A i)
X : Type u_3
Y : Type u_4
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Y
f : Πʳ (i : ι), [R i, A i] × Y → X
⊢ Continuous[instTopologicalSpaceProd, inst_1] f ↔
    ∀ (S : Set ι) (hS : cofinite ≤ 𝓟 S),
      Continuous[instTopologicalSpaceProd, inst_1] (f ∘ Prod.map (inclusion R A hS) id)

Tactic:
⟨fun H S hS ↦ H.comp ((continuous_inclusion hS).prodMap continuous_id),
    fun H ↦ ?_⟩

Premises used: Continuous.prodMap, Continuous.comp, RestrictedProduct.continuous_inclusion, continuous_id, Iff.intro
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst : (i : ι) → TopologicalSpace (R i)
hAopen : ∀ (i : ι), IsOpen[inst i] (A i)
X : Type u_3
Y : Type u_4
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Y
f : Πʳ (i : ι), [R i, A i] × Y → X
refine :
  ∀
    (H :
      ∀ (S : Set ι) (hS : cofinite ≤ 𝓟 S),
        Continuous[instTopologicalSpaceProd, inst_1] (f ∘ Prod.map (inclusion R A hS) id)),
    Continuous[instTopologicalSpaceProd, inst_1] f
⊢ Continuous[instTopologicalSpaceProd, inst_1] f ↔
    ∀ (S : Set ι) (hS : cofinite ≤ 𝓟 S),
      Continuous[instTopologicalSpaceProd, inst_1] (f ∘ Prod.map (inclusion R A hS) id)

Tactic:
refine ⟨fun H S hS ↦ H.comp ((continuous_inclusion hS).prodMap continuous_id),
    fun H ↦ ?_⟩
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst : (i : ι) → TopologicalSpace (R i)
hAopen : ∀ (i : ι), IsOpen[inst i] (A i)
X : Type u_3
Y : Type u_4
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Y
f : Πʳ (i : ι), [R i, A i] × Y → X
H :
  ∀ (S : Set ι) (hS : cofinite ≤ 𝓟 S), Continuous[instTopologicalSpaceProd, inst_1] (f ∘ Prod.map (inclusion R A hS) id)
simp_rw : ∀ (x : Πʳ (i : ι), [R i, A i] × Y), Tendsto f (𝓝 x) (𝓝 (f x))
⊢ Continuous[instTopologicalSpaceProd, inst_1] f

Tactic:
simp_rw [continuous_iff_continuousAt, ContinuousAt]

Premises used: ContinuousAt, continuous_iff_continuousAt
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst : (i : ι) → TopologicalSpace (R i)
hAopen : ∀ (i : ι), IsOpen[inst i] (A i)
X : Type u_3
Y : Type u_4
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Y
f : Πʳ (i : ι), [R i, A i] × Y → X
H :
  ∀ (S : Set ι) (hS : cofinite ≤ 𝓟 S), Continuous[instTopologicalSpaceProd, inst_1] (f ∘ Prod.map (inclusion R A hS) id)
x : Πʳ (i : ι), [R i, A i]
y : Y
S : Set ι := {i : ι | (x : (a : ι) → R a) i ∈ A i}
⊢ cofinite ≤ 𝓟 S

Tactic:
have hS : cofinite ≤ 𝓟 S := le_principal_iff.mpr x.2
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst : (i : ι) → TopologicalSpace (R i)
hAopen : ∀ (i : ι), IsOpen[inst i] (A i)
X : Type u_3
Y : Type u_4
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Y
f : Πʳ (i : ι), [R i, A i] × Y → X
H :
  ∀ (S : Set ι) (hS : cofinite ≤ 𝓟 S), Continuous[instTopologicalSpaceProd, inst_1] (f ∘ Prod.map (inclusion R A hS) id)
x : Πʳ (i : ι), [R i, A i]
y : Y
S : Set ι := {i : ι | (x : (a : ι) → R a) i ∈ A i}
hS : cofinite ≤ 𝓟 S
⊢ ∀ i ∈ S, (x : (a : ι) → R a) i ∈ A i

Tactic:
have hxS : ∀ i ∈ S, x i ∈ A i := fun i hi ↦ hi
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst : (i : ι) → TopologicalSpace (R i)
hAopen : ∀ (i : ι), IsOpen[inst i] (A i)
X : Type u_3
Y : Type u_4
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Y
f : Πʳ (i : ι), [R i, A i] × Y → X
H :
  ∀ (S : Set ι) (hS : cofinite ≤ 𝓟 S), Continuous[instTopologicalSpaceProd, inst_1] (f ∘ Prod.map (inclusion R A hS) id)
x : Πʳ (i : ι), [R i, A i]
y : Y
S : Set ι := {i : ι | (x : (a : ι) → R a) i ∈ A i}
hS : cofinite ≤ 𝓟 S
hxS : ∀ i ∈ S, (x : (a : ι) → R a) i ∈ A i
rcases : ∀ (x' : Πʳ (i : ι), [R i, A i]_[𝓟 S]) (hxx' : inclusion R A hS x' = x), Tendsto f (𝓝 (x, y)) (𝓝 (f (x, y)))
⊢ Tendsto f (𝓝 (x, y)) (𝓝 (f (x, y)))

Tactic:
rcases exists_inclusion_eq_of_eventually R A hS hxS with ⟨x', hxx'⟩

Premises used: RestrictedProduct.exists_inclusion_eq_of_eventually
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst : (i : ι) → TopologicalSpace (R i)
hAopen : ∀ (i : ι), IsOpen[inst i] (A i)
X : Type u_3
Y : Type u_4
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Y
f : Πʳ (i : ι), [R i, A i] × Y → X
H :
  ∀ (S : Set ι) (hS : cofinite ≤ 𝓟 S), Continuous[instTopologicalSpaceProd, inst_1] (f ∘ Prod.map (inclusion R A hS) id)
x : Πʳ (i : ι), [R i, A i]
y : Y
S : Set ι := {i : ι | (x : (a : ι) → R a) i ∈ A i}
hS : cofinite ≤ 𝓟 S
hxS : ∀ i ∈ S, (x : (a : ι) → R a) i ∈ A i
x' : Πʳ (i : ι), [R i, A i]_[𝓟 S]
hxx' : inclusion R A hS x' = x
rw :
  Tendsto (f ∘ fun (p : Πʳ (i : ι), [R i, A i]_[𝓟 S] × Y) ↦ (inclusion R A hS p.1, id p.2)) (𝓝 (x', y))
    (𝓝 (f (inclusion R A hS x', y)))
⊢ Tendsto f (𝓝 (x, y)) (𝓝 (f (x, y)))

Tactic:
rw [← hxx', nhds_prod_eq, nhds_eq_map_inclusion hAopen hS x',
    ← Filter.map_id (f := 𝓝 y), prod_map_map_eq, ← nhds_prod_eq, tendsto_map'_iff]

Premises used: Filter.tendsto_map'_iff, Filter.map_id, nhds_prod_eq, Filter.prod_map_map_eq, RestrictedProduct.nhds_eq_map_inclusion
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst : (i : ι) → TopologicalSpace (R i)
hAopen : ∀ (i : ι), IsOpen[inst i] (A i)
X : Type u_3
Y : Type u_4
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Y
f : Πʳ (i : ι), [R i, A i] × Y → X
H :
  ∀ (S : Set ι) (hS : cofinite ≤ 𝓟 S), Continuous[instTopologicalSpaceProd, inst_1] (f ∘ Prod.map (inclusion R A hS) id)
x : Πʳ (i : ι), [R i, A i]
y : Y
S : Set ι := {i : ι | (x : (a : ι) → R a) i ∈ A i}
hS : cofinite ≤ 𝓟 S
hxS : ∀ i ∈ S, (x : (a : ι) → R a) i ∈ A i
x' : Πʳ (i : ι), [R i, A i]_[𝓟 S]
hxx' : inclusion R A hS x' = x
⊢ Tendsto (f ∘ fun (p : Πʳ (i : ι), [R i, A i]_[𝓟 S] × Y) ↦ (inclusion R A hS p.1, id p.2)) (𝓝 (x', y))
    (𝓝 (f (inclusion R A hS x', y)))

Tactic:
H S hS |>.tendsto ⟨x', y⟩

Premises used: Prod.mk, Prod.map, Continuous.tendsto
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst : (i : ι) → TopologicalSpace (R i)
hAopen : ∀ (i : ι), IsOpen[inst i] (A i)
X : Type u_3
Y : Type u_4
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Y
f : Πʳ (i : ι), [R i, A i] × Y → X
H :
  ∀ (S : Set ι) (hS : cofinite ≤ 𝓟 S), Continuous[instTopologicalSpaceProd, inst_1] (f ∘ Prod.map (inclusion R A hS) id)
x : Πʳ (i : ι), [R i, A i]
y : Y
S : Set ι := {i : ι | (x : (a : ι) → R a) i ∈ A i}
hS : cofinite ≤ 𝓟 S
hxS : ∀ i ∈ S, (x : (a : ι) → R a) i ∈ A i
x' : Πʳ (i : ι), [R i, A i]_[𝓟 S]
hxx' : inclusion R A hS x' = x
⊢ Tendsto (f ∘ fun (p : Πʳ (i : ι), [R i, A i]_[𝓟 S] × Y) ↦ (inclusion R A hS p.1, id p.2)) (𝓝 (x', y))
    (𝓝 (f (inclusion R A hS x', y)))

Tactic:
exact H S hS |>.tendsto ⟨x', y⟩

Premises used: Prod.mk, Continuous.tendsto
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst : (i : ι) → TopologicalSpace (R i)
hAopen : ∀ (i : ι), IsOpen[inst i] (A i)
X : Type u_3
Y : Type u_4
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Y
f : Y × Πʳ (i : ι), [R i, A i] → X
⊢ Continuous[instTopologicalSpaceProd, inst_1] f ↔
    ∀ (S : Set ι) (hS : cofinite ≤ 𝓟 S),
      Continuous[instTopologicalSpaceProd, inst_1] (f ∘ Prod.map id (inclusion R A hS))

Tactic:
⟨fun H S hS ↦ H.comp (continuous_id.prodMap (continuous_inclusion hS)),
    fun H ↦ ?_⟩

Premises used: Continuous.prodMap, Continuous.comp, RestrictedProduct.continuous_inclusion, continuous_id, Iff.intro