awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.Basic
Goal:
ι : Type u_1
S : ι → Type u_3
G : ι → Type u_4
inst : (i : ι) → SetLike.{u_3, u_4} (S i) (G i)
A : (i : ι) → S i
inst_1 : DecidableEq ι
inst_2 : (i : ι) → Monoid (G i)
inst_3 : ∀ (i : ι), SubmonoidClass.{u_3, u_4} (S i) (G i)
i : ι
r : G i
n : ℕ
h :
  ∀ (i_1 : ι),
    (mulSingle (S := S) (G := G) A i (r ^ n) : (a : ι) → G a) i_1 =
      (HPow.hPow (α := Πʳ (i : ι), [G i, (↑(A i) : Set ((fun (i : ι) ↦ G i) i))]) (mulSingle (S := S) (G := G) A i r)
            n :
          (a : ι) → G a)
        i_1
⊢ mulSingle (S := S) (G := G) A i (r ^ n) =
    HPow.hPow (α := Πʳ (i : ι), [G i, (↑(A i) : Set ((fun (i : ι) ↦ G i) i))]) (mulSingle (S := S) (G := G) A i r) n

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.Basic
Goal:
ι : Type u_1
S : ι → Type u_3
G : ι → Type u_4
inst : (i : ι) → SetLike.{u_3, u_4} (S i) (G i)
A : (i : ι) → S i
inst_1 : DecidableEq ι
inst_2 : (i : ι) → Monoid (G i)
inst_3 : ∀ (i : ι), SubmonoidClass.{u_3, u_4} (S i) (G i)
i : ι
r : G i
n : ℕ
i_1 : ι
⊢ (mulSingle (S := S) (G := G) A i (r ^ n) : (a : ι) → G a) i_1 =
    (HPow.hPow (α := Πʳ (i : ι), [G i, (↑(A i) : Set ((fun (i : ι) ↦ G i) i))]) (mulSingle (S := S) (G := G) A i r) n :
        (a : ι) → G a)
      i_1

Tactic:
simp [Pi.mulSingle_pow, RestrictedProduct.pow_apply]

Premises used: Pi.mulSingle_pow, RestrictedProduct.pow_apply
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.Basic
Goal:
ι : Type u_1
S : ι → Type u_3
G : ι → Type u_4
inst : (i : ι) → SetLike.{u_3, u_4} (S i) (G i)
A : (i : ι) → S i
inst_1 : DecidableEq ι
inst_2 : (i : ι) → Group (G i)
inst_3 : ∀ (i : ι), SubgroupClass.{u_3, u_4} (S i) (G i)
i : ι
r : G i
n : ℤ
h :
  ∀ (i_1 : ι),
    (mulSingle (S := S) (G := G) A i (r ^ n) : (a : ι) → G a) i_1 =
      (HPow.hPow (α := Πʳ (i : ι), [G i, (↑(A i) : Set ((fun (i : ι) ↦ G i) i))]) (mulSingle (S := S) (G := G) A i r)
            n :
          (a : ι) → G a)
        i_1
⊢ mulSingle (S := S) (G := G) A i (r ^ n) =
    HPow.hPow (α := Πʳ (i : ι), [G i, (↑(A i) : Set ((fun (i : ι) ↦ G i) i))]) (mulSingle (S := S) (G := G) A i r) n

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.Basic
Goal:
ι : Type u_1
S : ι → Type u_3
G : ι → Type u_4
inst : (i : ι) → SetLike.{u_3, u_4} (S i) (G i)
A : (i : ι) → S i
inst_1 : DecidableEq ι
inst_2 : (i : ι) → Group (G i)
inst_3 : ∀ (i : ι), SubgroupClass.{u_3, u_4} (S i) (G i)
i : ι
r : G i
n : ℤ
i_1 : ι
⊢ (mulSingle (S := S) (G := G) A i (r ^ n) : (a : ι) → G a) i_1 =
    (HPow.hPow (α := Πʳ (i : ι), [G i, (↑(A i) : Set ((fun (i : ι) ↦ G i) i))]) (mulSingle (S := S) (G := G) A i r) n :
        (a : ι) → G a)
      i_1

Tactic:
simp [Pi.mulSingle_zpow, RestrictedProduct.zpow_apply]

Premises used: Pi.mulSingle_zpow, RestrictedProduct.zpow_apply
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
𝓕 : Filter ι
inst : (i : ι) → TopologicalSpace (R i)
⊢ Continuous[topologicalSpace R A 𝓕, Pi.topologicalSpace] (DFunLike.coe (β := R))

Tactic:
continuous_iSup_dom.mpr fun _ ↦ continuous_iSup_dom.mpr fun _ ↦
    continuous_coinduced_dom.mpr continuous_induced_dom

Premises used: Iff.mpr, continuous_coinduced_dom, continuous_iSup_dom, continuous_induced_dom
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
𝓕 : Filter ι
inst : (i : ι) → TopologicalSpace (R i)
i : ι
⊢ Continuous[topologicalSpace R A 𝓕, inst i] fun (x : Πʳ (i : ι), [R i, A i]_[𝓕]) ↦ (x : (a : ι) → R a) i

Tactic:
continuous_apply _ |>.comp continuous_coe

Premises used: RestrictedProduct.continuous_coe, Continuous.comp, continuous_apply
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
𝓕 : Filter ι
inst : (i : ι) → TopologicalSpace (R i)
𝓖 : Filter ι
h : 𝓕 ≤ 𝓖
simp_rw :
  LE.le (α := TopologicalSpace Πʳ (i : ι), [R i, A i]_[𝓕])
    (⨆ (i : Set ι),
      ⨆ (x : 𝓖 ≤ 𝓟 i),
        TopologicalSpace.coinduced (inclusion R A h ∘ inclusion R A ⋯)
          (TopologicalSpace.induced (DFunLike.coe (β := R)) inferInstance))
    (⨆ (S : Set ι),
      ⨆ (hS : 𝓕 ≤ 𝓟 S),
        TopologicalSpace.coinduced (inclusion R A hS) (TopologicalSpace.induced (DFunLike.coe (β := R)) inferInstance))
⊢ Continuous[topologicalSpace R A 𝓖, topologicalSpace R A 𝓕] (inclusion R A h)

Tactic:
simp_rw [continuous_iff_coinduced_le, topologicalSpace, coinduced_iSup, coinduced_compose]

Premises used: RestrictedProduct.topologicalSpace, coinduced_iSup, coinduced_compose, continuous_iff_coinduced_le
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
𝓕 : Filter ι
inst : (i : ι) → TopologicalSpace (R i)
𝓖 : Filter ι
h : 𝓕 ≤ 𝓖
⊢ LE.le (α := TopologicalSpace Πʳ (i : ι), [R i, A i]_[𝓕])
    (⨆ (i : Set ι),
      ⨆ (x : 𝓖 ≤ 𝓟 i),
        TopologicalSpace.coinduced (inclusion R A h ∘ inclusion R A ⋯)
          (TopologicalSpace.induced (DFunLike.coe (β := R)) inferInstance))
    (⨆ (S : Set ι),
      ⨆ (hS : 𝓕 ≤ 𝓟 S),
        TopologicalSpace.coinduced (inclusion R A hS) (TopologicalSpace.induced (DFunLike.coe (β := R)) inferInstance))

Tactic:
iSup₂_le fun S hS ↦ le_iSup₂_of_le S (le_trans h hS) le_rfl

Premises used: iSup₂_le, le_rfl, le_iSup₂_of_le, le_trans
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
𝓕 : Filter ι
inst : (i : ι) → TopologicalSpace (R i)
𝓖 : Filter ι
h : 𝓕 ≤ 𝓖
⊢ LE.le (α := TopologicalSpace Πʳ (i : ι), [R i, A i]_[𝓕])
    (⨆ (i : Set ι),
      ⨆ (x : 𝓖 ≤ 𝓟 i),
        TopologicalSpace.coinduced (inclusion R A h ∘ inclusion R A ⋯)
          (TopologicalSpace.induced (DFunLike.coe (β := R)) inferInstance))
    (⨆ (S : Set ι),
      ⨆ (hS : 𝓕 ≤ 𝓟 S),
        TopologicalSpace.coinduced (inclusion R A hS) (TopologicalSpace.induced (DFunLike.coe (β := R)) inferInstance))

Tactic:
exact iSup₂_le fun S hS ↦ le_iSup₂_of_le S (le_trans h hS) le_rfl

Premises used: iSup₂_le, le_rfl, le_iSup₂_of_le, le_trans
-- 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)
inst_1 : ∀ (i : ι), T0Space.{u_2} (R i)
⊢ T0Space Πʳ (i : ι), [R i, A i]_[𝓕]

Tactic:
t0Space_of_injective_of_continuous DFunLike.coe_injective continuous_coe

Premises used: RestrictedProduct.continuous_coe, t0Space_of_injective_of_continuous, DFunLike.coe_injective
-- 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)
inst_1 : ∀ (i : ι), T1Space.{u_2} (R i)
⊢ T1Space Πʳ (i : ι), [R i, A i]_[𝓕]

Tactic:
t1Space_of_injective_of_continuous DFunLike.coe_injective continuous_coe

Premises used: RestrictedProduct.continuous_coe, DFunLike.coe_injective, t1Space_of_injective_of_continuous
-- 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)
inst_1 : ∀ (i : ι), T2Space.{u_2} (R i)
⊢ T2Space Πʳ (i : ι), [R i, A i]_[𝓕]

Tactic:
.of_injective_continuous DFunLike.coe_injective continuous_coe

Premises used: RestrictedProduct.continuous_coe, T2Space.of_injective_continuous, DFunLike.coe_injective
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst : (i : ι) → TopologicalSpace (R i)
S : Set ι
rw :
  LE.le (α := TopologicalSpace Πʳ (i : ι), [R i, A i]_[𝓟 S])
    (TopologicalSpace.induced (DFunLike.coe (β := R)) inferInstance)
    (TopologicalSpace.coinduced id (TopologicalSpace.induced (DFunLike.coe (β := R)) inferInstance))
rw₁ rw₂ :
  LE.le (α := TopologicalSpace Πʳ (i : ι), [R i, A i]_[𝓟 S])
    (TopologicalSpace.induced (DFunLike.coe (β := R)) inferInstance)
    (TopologicalSpace.induced (DFunLike.coe (β := R)) inferInstance)
⊢ LE.le (α := TopologicalSpace Πʳ (i : ι), [R i, A i]_[𝓟 S])
    (TopologicalSpace.induced (DFunLike.coe (β := R)) inferInstance)
    (TopologicalSpace.coinduced (inclusion R A ⋯) (TopologicalSpace.induced (DFunLike.coe (β := R)) inferInstance))

Tactic:
rw [inclusion_eq_id R A (𝓟 S), @coinduced_id]

Premises used: RestrictedProduct.inclusion_eq_id, coinduced_id, Filter.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)
⊢ Eq (α := TopologicalSpace Πʳ (i : ι), [R i, A i]_[⊤]) (topologicalSpace R A ⊤)
    (TopologicalSpace.induced (DFunLike.coe (β := R)) inferInstance)

Tactic:
principal_univ ▸ topologicalSpace_eq_of_principal

Premises used: Filter.principal_univ, Eq.rec, RestrictedProduct.topologicalSpace_eq_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)
⊢ Eq (α := TopologicalSpace Πʳ (i : ι), [R i, A i]_[⊥]) (topologicalSpace R A ⊥)
    (TopologicalSpace.induced (DFunLike.coe (β := R)) inferInstance)

Tactic:
principal_empty ▸ topologicalSpace_eq_of_principal

Premises used: Eq.rec, RestrictedProduct.topologicalSpace_eq_of_principal, Filter.principal_empty
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst : (i : ι) → TopologicalSpace (R i)
⊢ IsEmbedding (X := Πʳ (i : ι), [R i, A i]_[⊤]) (DFunLike.coe (β := R))

Tactic:
principal_univ ▸ isEmbedding_coe_of_principal

Premises used: Filter.principal_univ, Eq.rec, RestrictedProduct.isEmbedding_coe_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)
⊢ IsEmbedding (X := Πʳ (i : ι), [R i, A i]_[⊥]) (DFunLike.coe (β := R))

Tactic:
principal_empty ▸ isEmbedding_coe_of_principal

Premises used: Eq.rec, RestrictedProduct.isEmbedding_coe_of_principal, Filter.principal_empty
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst : (i : ι) → TopologicalSpace (R i)
S : Set ι
X : Type u_3
inst_1 : TopologicalSpace X
f : X → Πʳ (i : ι), [R i, A i]_[𝓟 S]
⊢ Continuous[inst_1, topologicalSpace R A (𝓟 S)] f ↔ Continuous[inst_1, Pi.topologicalSpace] (DFunLike.coe (β := R) ∘ f)

Tactic:
isEmbedding_coe_of_principal.continuous_iff

Premises used: RestrictedProduct.isEmbedding_coe_of_principal, Topology.IsEmbedding.continuous_iff
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst : (i : ι) → TopologicalSpace (R i)
X : Type u_3
inst_1 : TopologicalSpace X
f : X → Πʳ (i : ι), [R i, A i]_[⊤]
⊢ Continuous[inst_1, topologicalSpace R A ⊤] f ↔ Continuous[inst_1, Pi.topologicalSpace] (DFunLike.coe (β := R) ∘ f)

Tactic:
isEmbedding_coe_of_top.continuous_iff

Premises used: RestrictedProduct.isEmbedding_coe_of_top, Topology.IsEmbedding.continuous_iff
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst : (i : ι) → TopologicalSpace (R i)
X : Type u_3
inst_1 : TopologicalSpace X
f : X → Πʳ (i : ι), [R i, A i]_[⊥]
⊢ Continuous[inst_1, topologicalSpace R A ⊥] f ↔ Continuous[inst_1, Pi.topologicalSpace] (DFunLike.coe (β := R) ∘ f)

Tactic:
isEmbedding_coe_of_bot.continuous_iff

Premises used: RestrictedProduct.isEmbedding_coe_of_bot, Topology.IsEmbedding.continuous_iff
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst : (i : ι) → TopologicalSpace (R i)
S : Set ι
X : Type u_3
inst_1 : TopologicalSpace X
f : X → Πʳ (i : ι), [R i, A i]_[𝓟 S]
⊢ Continuous[inst_1, topologicalSpace R A (𝓟 S)] f ↔
    ∀ (i : ι), Continuous[inst_1, inst i] ((fun (x : Πʳ (i : ι), [R i, A i]_[𝓟 S]) ↦ (x : (a : ι) → R a) i) ∘ f)

Tactic:
continuous_rng_of_principal.trans continuous_pi_iff

Premises used: RestrictedProduct.continuous_rng_of_principal, continuous_pi_iff, Iff.trans
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst : (i : ι) → TopologicalSpace (R i)
S : Set ι
inst_1 : ∀ (i : ι), WeaklyLocallyCompactSpace.{u_2} (R i)
hS : cofinite ≤ 𝓟 S
hAcompact : ∀ i ∈ S, IsCompact (A i)
x : Πʳ (i : ι), [R i, A i]_[𝓟 S]
rw :
  ∀ (hS : Sᶜ.Finite) (hAcompact : ∀ i ∈ S, IsCompact (A i)) (x : Πʳ (i : ι), [R i, A i]_[𝓟 S]),
    ∃ (s : Set Πʳ (i : ι), [R i, A i]_[𝓟 S]), IsCompact s ∧ s ∈ 𝓝 x
⊢ ∃ (s : Set Πʳ (i : ι), [R i, A i]_[𝓟 S]), IsCompact s ∧ s ∈ 𝓝 x

Tactic:
rw [le_principal_iff, mem_cofinite] at hS

Premises used: Filter.mem_cofinite, Filter.le_principal_iff
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst : (i : ι) → TopologicalSpace (R i)
S : Set ι
inst_1 : ∀ (i : ι), WeaklyLocallyCompactSpace.{u_2} (R i)
hS : Sᶜ.Finite
hAcompact : ∀ i ∈ S, IsCompact (A i)
x : Πʳ (i : ι), [R i, A i]_[𝓟 S]
⊢ ∀ (i : ι), ∃ (K : Set (R i)), IsCompact K ∧ K ∈ 𝓝 ((x : (a : ι) → R a) i)

Tactic:
have : ∀ i, ∃ K, IsCompact K ∧ K ∈ 𝓝 (x i) := fun i ↦ exists_compact_mem_nhds (x i)
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst : (i : ι) → TopologicalSpace (R i)
S : Set ι
inst_1 : ∀ (i : ι), WeaklyLocallyCompactSpace.{u_2} (R i)
hS : Sᶜ.Finite
hAcompact : ∀ i ∈ S, IsCompact (A i)
x : Πʳ (i : ι), [R i, A i]_[𝓟 S]
this : ∀ (i : ι), ∃ (K : Set (R i)), IsCompact K ∧ K ∈ 𝓝 ((x : (a : ι) → R a) i)
choose :
  ∀ (K : (i : ι) → Set (R i)) (K_compact : ∀ (i : ι), IsCompact (K i))
    (hK : ∀ (i : ι), K i ∈ 𝓝 ((x : (a : ι) → R a) i)), ∃ (s : Set Πʳ (i : ι), [R i, A i]_[𝓟 S]), IsCompact s ∧ s ∈ 𝓝 x
⊢ ∃ (s : Set Πʳ (i : ι), [R i, A i]_[𝓟 S]), IsCompact s ∧ s ∈ 𝓝 x

Tactic:
choose K K_compact hK using this
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst : (i : ι) → TopologicalSpace (R i)
S : Set ι
inst_1 : ∀ (i : ι), WeaklyLocallyCompactSpace.{u_2} (R i)
hS : Sᶜ.Finite
hAcompact : ∀ i ∈ S, IsCompact (A i)
x : Πʳ (i : ι), [R i, A i]_[𝓟 S]
K : (i : ι) → Set (R i)
K_compact : ∀ (i : ι), IsCompact (K i)
hK : ∀ (i : ι), K i ∈ 𝓝 ((x : (a : ι) → R a) i)
⊢ let Q : Set ((i : ι) → R i) := Set.pi (α := R) univ fun (i : ι) ↦ if i ∈ S then A i else K i;
  Q = Set.pi (α := R) univ fun (i : ι) ↦ if i ∈ S then A i else K i

Tactic:
set Q : Set (Π i, R i) := univ.pi (fun i ↦ if i ∈ S then A i else K i) with Q_def

Premises used: Set.univ, Membership.mem, Set.pi, ite, Set
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst : (i : ι) → TopologicalSpace (R i)
S : Set ι
inst_1 : ∀ (i : ι), WeaklyLocallyCompactSpace.{u_2} (R i)
hS : Sᶜ.Finite
hAcompact : ∀ i ∈ S, IsCompact (A i)
x : Πʳ (i : ι), [R i, A i]_[𝓟 S]
K : (i : ι) → Set (R i)
K_compact : ∀ (i : ι), IsCompact (K i)
hK : ∀ (i : ι), K i ∈ 𝓝 ((x : (a : ι) → R a) i)
Q : Set ((i : ι) → R i) := Set.pi (α := R) univ fun (i : ι) ↦ if i ∈ S then A i else K i
Q_def : Q = Set.pi (α := R) univ fun (i : ι) ↦ if i ∈ S then A i else K i
i : ι
pos : ∀ (his : i ∈ S), IsCompact (A i)
neg : ∀ (his : i ∉ S), IsCompact (K i)
⊢ IsCompact (if i ∈ S then A i else K i)

Tactic:
split_ifs with his
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst : (i : ι) → TopologicalSpace (R i)
S : Set ι
inst_1 : ∀ (i : ι), WeaklyLocallyCompactSpace.{u_2} (R i)
hS : Sᶜ.Finite
hAcompact : ∀ i ∈ S, IsCompact (A i)
x : Πʳ (i : ι), [R i, A i]_[𝓟 S]
K : (i : ι) → Set (R i)
K_compact : ∀ (i : ι), IsCompact (K i)
hK : ∀ (i : ι), K i ∈ 𝓝 ((x : (a : ι) → R a) i)
Q : Set ((i : ι) → R i) := Set.pi (α := R) univ fun (i : ι) ↦ if i ∈ S then A i else K i
Q_def : Q = Set.pi (α := R) univ fun (i : ι) ↦ if i ∈ S then A i else K i
i : ι
his : i ∈ S
⊢ IsCompact (A i)

Tactic:
hAcompact i his
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst : (i : ι) → TopologicalSpace (R i)
S : Set ι
inst_1 : ∀ (i : ι), WeaklyLocallyCompactSpace.{u_2} (R i)
hS : Sᶜ.Finite
hAcompact : ∀ i ∈ S, IsCompact (A i)
x : Πʳ (i : ι), [R i, A i]_[𝓟 S]
K : (i : ι) → Set (R i)
K_compact : ∀ (i : ι), IsCompact (K i)
hK : ∀ (i : ι), K i ∈ 𝓝 ((x : (a : ι) → R a) i)
Q : Set ((i : ι) → R i) := Set.pi (α := R) univ fun (i : ι) ↦ if i ∈ S then A i else K i
Q_def : Q = Set.pi (α := R) univ fun (i : ι) ↦ if i ∈ S then A i else K i
i : ι
his : i ∈ S
⊢ IsCompact (A i)

Tactic:
exact hAcompact i his
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst : (i : ι) → TopologicalSpace (R i)
S : Set ι
inst_1 : ∀ (i : ι), WeaklyLocallyCompactSpace.{u_2} (R i)
hS : Sᶜ.Finite
hAcompact : ∀ i ∈ S, IsCompact (A i)
x : Πʳ (i : ι), [R i, A i]_[𝓟 S]
K : (i : ι) → Set (R i)
K_compact : ∀ (i : ι), IsCompact (K i)
hK : ∀ (i : ι), K i ∈ 𝓝 ((x : (a : ι) → R a) i)
Q : Set ((i : ι) → R i) := Set.pi (α := R) univ fun (i : ι) ↦ if i ∈ S then A i else K i
Q_def : Q = Set.pi (α := R) univ fun (i : ι) ↦ if i ∈ S then A i else K i
i : ι
his : i ∉ S
⊢ IsCompact (K i)

Tactic:
K_compact i
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst : (i : ι) → TopologicalSpace (R i)
S : Set ι
inst_1 : ∀ (i : ι), WeaklyLocallyCompactSpace.{u_2} (R i)
hS : Sᶜ.Finite
hAcompact : ∀ i ∈ S, IsCompact (A i)
x : Πʳ (i : ι), [R i, A i]_[𝓟 S]
K : (i : ι) → Set (R i)
K_compact : ∀ (i : ι), IsCompact (K i)
hK : ∀ (i : ι), K i ∈ 𝓝 ((x : (a : ι) → R a) i)
Q : Set ((i : ι) → R i) := Set.pi (α := R) univ fun (i : ι) ↦ if i ∈ S then A i else K i
Q_def : Q = Set.pi (α := R) univ fun (i : ι) ↦ if i ∈ S then A i else K i
i : ι
his : i ∉ S
⊢ IsCompact (K i)

Tactic:
exact K_compact i
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst : (i : ι) → TopologicalSpace (R i)
S : Set ι
inst_1 : ∀ (i : ι), WeaklyLocallyCompactSpace.{u_2} (R i)
hS : Sᶜ.Finite
hAcompact : ∀ i ∈ S, IsCompact (A i)
x : Πʳ (i : ι), [R i, A i]_[𝓟 S]
K : (i : ι) → Set (R i)
K_compact : ∀ (i : ι), IsCompact (K i)
hK : ∀ (i : ι), K i ∈ 𝓝 ((x : (a : ι) → R a) i)
Q : Set ((i : ι) → R i) := Set.pi (α := R) univ fun (i : ι) ↦ if i ∈ S then A i else K i
Q_def : Q = Set.pi (α := R) univ fun (i : ι) ↦ if i ∈ S then A i else K i
⊢ IsCompact Q

Tactic:
have Q_compact : IsCompact Q := isCompact_univ_pi fun i ↦ by
      split_ifs with his
      · exact hAcompact i his
      · exact K_compact i
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst : (i : ι) → TopologicalSpace (R i)
S : Set ι
inst_1 : ∀ (i : ι), WeaklyLocallyCompactSpace.{u_2} (R i)
hS : Sᶜ.Finite
hAcompact : ∀ i ∈ S, IsCompact (A i)
x : Πʳ (i : ι), [R i, A i]_[𝓟 S]
K : (i : ι) → Set (R i)
K_compact : ∀ (i : ι), IsCompact (K i)
hK : ∀ (i : ι), K i ∈ 𝓝 ((x : (a : ι) → R a) i)
Q : Set ((i : ι) → R i) := Set.pi (α := R) univ fun (i : ι) ↦ if i ∈ S then A i else K i
Q_def : Q = Set.pi (α := R) univ fun (i : ι) ↦ if i ∈ S then A i else K i
Q_compact : IsCompact Q
U : Set ((i : ι) → R i) := Sᶜ.pi (α := R) K
⊢ U ∈ 𝓝 (⇑x : (a : ι) → R a)

Tactic:
have U_nhds : U ∈ 𝓝 (x : Π i, R i) := set_pi_mem_nhds hS fun i _ ↦ hK i
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst : (i : ι) → TopologicalSpace (R i)
S : Set ι
inst_1 : ∀ (i : ι), WeaklyLocallyCompactSpace.{u_2} (R i)
hS : Sᶜ.Finite
hAcompact : ∀ i ∈ S, IsCompact (A i)
x : Πʳ (i : ι), [R i, A i]_[𝓟 S]
K : (i : ι) → Set (R i)
K_compact : ∀ (i : ι), IsCompact (K i)
hK : ∀ (i : ι), K i ∈ 𝓝 ((x : (a : ι) → R a) i)
Q : Set ((i : ι) → R i) := Set.pi (α := R) univ fun (i : ι) ↦ if i ∈ S then A i else K i
Q_def : Q = Set.pi (α := R) univ fun (i : ι) ↦ if i ∈ S then A i else K i
Q_compact : IsCompact Q
U : Set ((i : ι) → R i) := Sᶜ.pi (α := R) K
U_nhds : U ∈ 𝓝 (⇑x : (a : ι) → R a)
y : Πʳ (i : ι), [R i, A i]_[𝓟 S]
H : Membership.mem (γ := Set Πʳ (i : ι), [R i, A i]_[𝓟 S]) (DFunLike.coe (β := R) ⁻¹' U) y
i : ι
h : Membership.mem (γ := Set ι) univ i
pos : ∀ (hi : i ∈ S), (y : (a : ι) → R a) i ∈ A i
neg : ∀ (hi : i ∉ S), (y : (a : ι) → R a) i ∈ K i
⊢ (y : (a : ι) → R a) i ∈ if i ∈ S then A i else K i

Tactic:
split_ifs with 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)
S : Set ι
inst_1 : ∀ (i : ι), WeaklyLocallyCompactSpace.{u_2} (R i)
hS : Sᶜ.Finite
hAcompact : ∀ i ∈ S, IsCompact (A i)
x : Πʳ (i : ι), [R i, A i]_[𝓟 S]
K : (i : ι) → Set (R i)
K_compact : ∀ (i : ι), IsCompact (K i)
hK : ∀ (i : ι), K i ∈ 𝓝 ((x : (a : ι) → R a) i)
Q : Set ((i : ι) → R i) := Set.pi (α := R) univ fun (i : ι) ↦ if i ∈ S then A i else K i
Q_def : Q = Set.pi (α := R) univ fun (i : ι) ↦ if i ∈ S then A i else K i
Q_compact : IsCompact Q
U : Set ((i : ι) → R i) := Sᶜ.pi (α := R) K
U_nhds : U ∈ 𝓝 (⇑x : (a : ι) → R a)
y : Πʳ (i : ι), [R i, A i]_[𝓟 S]
H : Membership.mem (γ := Set Πʳ (i : ι), [R i, A i]_[𝓟 S]) (DFunLike.coe (β := R) ⁻¹' U) y
i : ι
h : Membership.mem (γ := Set ι) univ i
hi : i ∈ S
⊢ (y : (a : ι) → R a) i ∈ A i

Tactic:
y.2 hi

Premises used: Set.Mem, setOf, Subtype.property
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst : (i : ι) → TopologicalSpace (R i)
S : Set ι
inst_1 : ∀ (i : ι), WeaklyLocallyCompactSpace.{u_2} (R i)
hS : Sᶜ.Finite
hAcompact : ∀ i ∈ S, IsCompact (A i)
x : Πʳ (i : ι), [R i, A i]_[𝓟 S]
K : (i : ι) → Set (R i)
K_compact : ∀ (i : ι), IsCompact (K i)
hK : ∀ (i : ι), K i ∈ 𝓝 ((x : (a : ι) → R a) i)
Q : Set ((i : ι) → R i) := Set.pi (α := R) univ fun (i : ι) ↦ if i ∈ S then A i else K i
Q_def : Q = Set.pi (α := R) univ fun (i : ι) ↦ if i ∈ S then A i else K i
Q_compact : IsCompact Q
U : Set ((i : ι) → R i) := Sᶜ.pi (α := R) K
U_nhds : U ∈ 𝓝 (⇑x : (a : ι) → R a)
y : Πʳ (i : ι), [R i, A i]_[𝓟 S]
H : Membership.mem (γ := Set Πʳ (i : ι), [R i, A i]_[𝓟 S]) (DFunLike.coe (β := R) ⁻¹' U) y
i : ι
h : Membership.mem (γ := Set ι) univ i
hi : i ∈ S
⊢ (y : (a : ι) → R a) i ∈ A i

Tactic:
exact y.2 hi

Premises used: Subtype.property
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst : (i : ι) → TopologicalSpace (R i)
S : Set ι
inst_1 : ∀ (i : ι), WeaklyLocallyCompactSpace.{u_2} (R i)
hS : Sᶜ.Finite
hAcompact : ∀ i ∈ S, IsCompact (A i)
x : Πʳ (i : ι), [R i, A i]_[𝓟 S]
K : (i : ι) → Set (R i)
K_compact : ∀ (i : ι), IsCompact (K i)
hK : ∀ (i : ι), K i ∈ 𝓝 ((x : (a : ι) → R a) i)
Q : Set ((i : ι) → R i) := Set.pi (α := R) univ fun (i : ι) ↦ if i ∈ S then A i else K i
Q_def : Q = Set.pi (α := R) univ fun (i : ι) ↦ if i ∈ S then A i else K i
Q_compact : IsCompact Q
U : Set ((i : ι) → R i) := Sᶜ.pi (α := R) K
U_nhds : U ∈ 𝓝 (⇑x : (a : ι) → R a)
y : Πʳ (i : ι), [R i, A i]_[𝓟 S]
H : Membership.mem (γ := Set Πʳ (i : ι), [R i, A i]_[𝓟 S]) (DFunLike.coe (β := R) ⁻¹' U) y
i : ι
h : Membership.mem (γ := Set ι) univ i
hi : i ∉ S
⊢ (y : (a : ι) → R a) i ∈ K i

Tactic:
H i hi