awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
Goal:
ι : Type u_1
n : Type u_3
inst : Finite n
X : Type u_4
inst_1 : TopologicalSpace X
A : n → ι → Type u_5
inst_2 : (j : n) → (i : ι) → TopologicalSpace (A j i)
C : (j : n) → (i : ι) → Set (A j i)
hCopen : ∀ (j : n) (i : ι), IsOpen[inst_2 j i] (C j i)
f : ((j : n) → Πʳ (i : ι), [A j i, C j i]) → X
H :
  ∀ (S : Set ι) (hS : cofinite ≤ 𝓟 S),
    Continuous[Pi.topologicalSpace, inst_1]
      (f ∘
        Pi.map (α := fun (x : n) ↦ Πʳ (i : ι), [A x i, C x i]_[𝓟 S]) (β := fun (j : n) ↦ Πʳ (i : ι), [A j i, C j i])
          fun (x : n) ↦ inclusion (A x) (C x) hS)
x : (j : n) → Πʳ (i : ι), [A j i, C j i]
S : Set ι := {i : ι | ∀ (j : n), (x j : (a : ι) → A j a) i ∈ C j i}
hS : cofinite ≤ 𝓟 S
x' : (j : n) → Πʳ (i : ι), [A j i, C j i]_[𝓟 S] :=
  fun (j : n) ↦ mk (R := A j) (A := C j) (fun (i : ι) ↦ (x j : (a : ι) → A j a) i) ⋯
hxx' :
  Pi.map (α := fun (j : n) ↦ Πʳ (i : ι), [A j i, C j i]_[𝓟 S]) (β := fun (j : n) ↦ Πʳ (i : ι), [A j i, C j i])
      (fun (j : n) ↦ inclusion (A j) (C j) hS) x' =
    x
⊢ Tendsto
    (f ∘
      Pi.map (α := fun (i : n) ↦ Πʳ (i_1 : ι), [A i i_1, C i i_1]_[𝓟 S]) (β := fun (i : n) ↦
        Πʳ (i_1 : ι), [A i i_1, C i i_1]) fun (i : n) ↦ inclusion (A i) (C i) hS)
    (𝓝 x')
    (𝓝
      (f
        (Pi.map (α := fun (j : n) ↦ Πʳ (i : ι), [A j i, C j i]_[𝓟 S]) (β := fun (j : n) ↦ Πʳ (i : ι), [A j i, C j i])
          (fun (i : n) ↦ inclusion (A i) (C i) hS) x')))

Tactic:
(H _ _).tendsto _

Premises used: Pi.map, Continuous.tendsto
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
Goal:
ι : Type u_1
n : Type u_3
inst : Finite n
X : Type u_4
inst_1 : TopologicalSpace X
A : n → ι → Type u_5
inst_2 : (j : n) → (i : ι) → TopologicalSpace (A j i)
C : (j : n) → (i : ι) → Set (A j i)
hCopen : ∀ (j : n) (i : ι), IsOpen[inst_2 j i] (C j i)
f : ((j : n) → Πʳ (i : ι), [A j i, C j i]) → X
H :
  ∀ (S : Set ι) (hS : cofinite ≤ 𝓟 S),
    Continuous[Pi.topologicalSpace, inst_1]
      (f ∘
        Pi.map (α := fun (x : n) ↦ Πʳ (i : ι), [A x i, C x i]_[𝓟 S]) (β := fun (j : n) ↦ Πʳ (i : ι), [A j i, C j i])
          fun (x : n) ↦ inclusion (A x) (C x) hS)
x : (j : n) → Πʳ (i : ι), [A j i, C j i]
S : Set ι := {i : ι | ∀ (j : n), (x j : (a : ι) → A j a) i ∈ C j i}
hS : cofinite ≤ 𝓟 S
x' : (j : n) → Πʳ (i : ι), [A j i, C j i]_[𝓟 S] :=
  fun (j : n) ↦ mk (R := A j) (A := C j) (fun (i : ι) ↦ (x j : (a : ι) → A j a) i) ⋯
hxx' :
  Pi.map (α := fun (j : n) ↦ Πʳ (i : ι), [A j i, C j i]_[𝓟 S]) (β := fun (j : n) ↦ Πʳ (i : ι), [A j i, C j i])
      (fun (j : n) ↦ inclusion (A j) (C j) hS) x' =
    x
⊢ Tendsto
    (f ∘
      Pi.map (α := fun (i : n) ↦ Πʳ (i_1 : ι), [A i i_1, C i i_1]_[𝓟 S]) (β := fun (i : n) ↦
        Πʳ (i_1 : ι), [A i i_1, C i i_1]) fun (i : n) ↦ inclusion (A i) (C i) hS)
    (𝓝 x')
    (𝓝
      (f
        (Pi.map (α := fun (j : n) ↦ Πʳ (i : ι), [A j i, C j i]_[𝓟 S]) (β := fun (j : n) ↦ Πʳ (i : ι), [A j i, C j i])
          (fun (i : n) ↦ inclusion (A i) (C i) hS) x')))

Tactic:
exact (H _ _).tendsto _

Premises used: Continuous.tendsto
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
𝓕_1 𝓖 : Filter ι
S : ι → Type u_3
inst : (i : ι) → SetLike.{u_3, u_2} (S i) (R i)
B : (i : ι) → S i
T : Set ι
𝓕 : Filter ι
inst_1 : (i : ι) → TopologicalSpace (R i)
inst_2 : (i : ι) → Inv (R i)
inst_3 : ∀ (i : ι), InvMemClass.{u_3, u_2} (S i) (R i)
inst_4 : ∀ (i : ι), ContinuousInv.{u_2} (R i)
rw :
  ∀ (S_1 : Set ι) (hS : 𝓕 ≤ 𝓟 S_1),
    Continuous[topologicalSpace R (fun (i : ι) ↦ (↑(B i) : Set ((fun (i : ι) ↦ R i) i))) (𝓟 S_1),
        topologicalSpace R (fun (i : ι) ↦ (↑(B i) : Set ((fun (i : ι) ↦ R i) i))) 𝓕]
      ((fun (a : Πʳ (i : ι), [R i, (↑(B i) : Set ((fun (i : ι) ↦ R i) i))]_[𝓕]) ↦ a⁻¹) ∘
        inclusion R (fun (i : ι) ↦ (↑(B i) : Set ((fun (i : ι) ↦ R i) i))) hS)
⊢ Continuous[topologicalSpace R (fun (i : ι) ↦ (↑(B i) : Set ((fun (i : ι) ↦ R i) i))) 𝓕,
      topologicalSpace R (fun (i : ι) ↦ (↑(B i) : Set ((fun (i : ι) ↦ R i) i))) 𝓕]
    fun (a : Πʳ (i : ι), [R i, (↑(B i) : Set ((fun (i : ι) ↦ R i) i))]_[𝓕]) ↦ a⁻¹

Tactic:
rw [continuous_dom]

Premises used: RestrictedProduct.continuous_dom
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
𝓕_1 𝓖 : Filter ι
S : ι → Type u_3
inst : (i : ι) → SetLike.{u_3, u_2} (S i) (R i)
B : (i : ι) → S i
T_1 : Set ι
𝓕 : Filter ι
inst_1 : (i : ι) → TopologicalSpace (R i)
inst_2 : (i : ι) → Inv (R i)
inst_3 : ∀ (i : ι), InvMemClass.{u_3, u_2} (S i) (R i)
inst_4 : ∀ (i : ι), ContinuousInv.{u_2} (R i)
T : Set ι
hT : 𝓕 ≤ 𝓟 T
⊢ ContinuousInv Πʳ (i : ι), [R i, (↑(B i) : Set ((fun (i : ι) ↦ R i) i))]_[𝓟 T]

Tactic:
haveI : ContinuousInv (Πʳ i, [R i, B i]_[𝓟 T]) :=
      isEmbedding_coe_of_principal.continuousInv fun _ ↦ rfl
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
𝓕_1 𝓖 : Filter ι
S : ι → Type u_3
inst : (i : ι) → SetLike.{u_3, u_2} (S i) (R i)
B : (i : ι) → S i
T_1 : Set ι
𝓕 : Filter ι
inst_1 : (i : ι) → TopologicalSpace (R i)
inst_2 : (i : ι) → Inv (R i)
inst_3 : ∀ (i : ι), InvMemClass.{u_3, u_2} (S i) (R i)
inst_4 : ∀ (i : ι), ContinuousInv.{u_2} (R i)
T : Set ι
hT : 𝓕 ≤ 𝓟 T
this : ContinuousInv Πʳ (i : ι), [R i, (↑(B i) : Set ((fun (i : ι) ↦ R i) i))]_[𝓟 T]
⊢ Continuous[topologicalSpace R (fun (i : ι) ↦ (↑(B i) : Set ((fun (i : ι) ↦ R i) i))) (𝓟 T),
      topologicalSpace R (fun (i : ι) ↦ (↑(B i) : Set ((fun (i : ι) ↦ R i) i))) 𝓕]
    ((fun (a : Πʳ (i : ι), [R i, (↑(B i) : Set ((fun (i : ι) ↦ R i) i))]_[𝓕]) ↦ a⁻¹) ∘
      inclusion R (fun (i : ι) ↦ (↑(B i) : Set ((fun (i : ι) ↦ R i) i))) hT)

Tactic:
(continuous_inclusion hT).comp continuous_inv

Premises used: Set.Mem, RestrictedProduct.inclusion, Continuous.comp, RestrictedProduct.continuous_inclusion, ContinuousInv.continuous_inv
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
𝓕_1 𝓖 : Filter ι
S : ι → Type u_3
inst : (i : ι) → SetLike.{u_3, u_2} (S i) (R i)
B : (i : ι) → S i
T_1 : Set ι
𝓕 : Filter ι
inst_1 : (i : ι) → TopologicalSpace (R i)
inst_2 : (i : ι) → Inv (R i)
inst_3 : ∀ (i : ι), InvMemClass.{u_3, u_2} (S i) (R i)
inst_4 : ∀ (i : ι), ContinuousInv.{u_2} (R i)
T : Set ι
hT : 𝓕 ≤ 𝓟 T
this : ContinuousInv Πʳ (i : ι), [R i, (↑(B i) : Set ((fun (i : ι) ↦ R i) i))]_[𝓟 T]
⊢ Continuous[topologicalSpace R (fun (i : ι) ↦ (↑(B i) : Set ((fun (i : ι) ↦ R i) i))) (𝓟 T),
      topologicalSpace R (fun (i : ι) ↦ (↑(B i) : Set ((fun (i : ι) ↦ R i) i))) 𝓕]
    ((fun (a : Πʳ (i : ι), [R i, (↑(B i) : Set ((fun (i : ι) ↦ R i) i))]_[𝓕]) ↦ a⁻¹) ∘
      inclusion R (fun (i : ι) ↦ (↑(B i) : Set ((fun (i : ι) ↦ R i) i))) hT)

Tactic:
exact (continuous_inclusion hT).comp continuous_inv

Premises used: Continuous.comp, RestrictedProduct.continuous_inclusion, ContinuousInv.continuous_inv
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
𝓕_1 𝓖 : Filter ι
S : ι → Type u_3
inst : (i : ι) → SetLike.{u_3, u_2} (S i) (R i)
B : (i : ι) → S i
T : Set ι
𝓕 : Filter ι
inst_1 : (i : ι) → TopologicalSpace (R i)
G : Type u_4
inst_2 : (i : ι) → SMul.{u_4, u_2} G (R i)
inst_3 : ∀ (i : ι), SMulMemClass.{u_3, u_4, u_2} (S i) G (R i)
inst_4 : ∀ (i : ι), ContinuousConstSMul.{u_4, u_2} G (R i)
g : G
rw :
  ∀ (S_1 : Set ι) (hS : 𝓕 ≤ 𝓟 S_1),
    Continuous[topologicalSpace R (fun (i : ι) ↦ (↑(B i) : Set ((fun (i : ι) ↦ R i) i))) (𝓟 S_1),
        topologicalSpace R (fun (i : ι) ↦ (↑(B i) : Set ((fun (i : ι) ↦ R i) i))) 𝓕]
      ((fun (x : Πʳ (i : ι), [R i, (↑(B i) : Set ((fun (i : ι) ↦ R i) i))]_[𝓕]) ↦ g • x) ∘
        inclusion R (fun (i : ι) ↦ (↑(B i) : Set ((fun (i : ι) ↦ R i) i))) hS)
⊢ Continuous[topologicalSpace R (fun (i : ι) ↦ (↑(B i) : Set ((fun (i : ι) ↦ R i) i))) 𝓕,
      topologicalSpace R (fun (i : ι) ↦ (↑(B i) : Set ((fun (i : ι) ↦ R i) i))) 𝓕]
    fun (x : Πʳ (i : ι), [R i, (↑(B i) : Set ((fun (i : ι) ↦ R i) i))]_[𝓕]) ↦ g • x

Tactic:
rw [continuous_dom]

Premises used: RestrictedProduct.continuous_dom
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
𝓕_1 𝓖 : Filter ι
S : ι → Type u_3
inst : (i : ι) → SetLike.{u_3, u_2} (S i) (R i)
B : (i : ι) → S i
T_1 : Set ι
𝓕 : Filter ι
inst_1 : (i : ι) → TopologicalSpace (R i)
G : Type u_4
inst_2 : (i : ι) → SMul.{u_4, u_2} G (R i)
inst_3 : ∀ (i : ι), SMulMemClass.{u_3, u_4, u_2} (S i) G (R i)
inst_4 : ∀ (i : ι), ContinuousConstSMul.{u_4, u_2} G (R i)
g : G
T : Set ι
hT : 𝓕 ≤ 𝓟 T
⊢ ContinuousConstSMul G Πʳ (i : ι), [R i, (↑(B i) : Set ((fun (i : ι) ↦ R i) i))]_[𝓟 T]

Tactic:
haveI : ContinuousConstSMul G (Πʳ i, [R i, B i]_[𝓟 T]) :=
      isEmbedding_coe_of_principal.continuousConstSMul id rfl
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
𝓕_1 𝓖 : Filter ι
S : ι → Type u_3
inst : (i : ι) → SetLike.{u_3, u_2} (S i) (R i)
B : (i : ι) → S i
T_1 : Set ι
𝓕 : Filter ι
inst_1 : (i : ι) → TopologicalSpace (R i)
G : Type u_4
inst_2 : (i : ι) → SMul.{u_4, u_2} G (R i)
inst_3 : ∀ (i : ι), SMulMemClass.{u_3, u_4, u_2} (S i) G (R i)
inst_4 : ∀ (i : ι), ContinuousConstSMul.{u_4, u_2} G (R i)
g : G
T : Set ι
hT : 𝓕 ≤ 𝓟 T
this : ContinuousConstSMul G Πʳ (i : ι), [R i, (↑(B i) : Set ((fun (i : ι) ↦ R i) i))]_[𝓟 T]
⊢ Continuous[topologicalSpace R (fun (i : ι) ↦ (↑(B i) : Set ((fun (i : ι) ↦ R i) i))) (𝓟 T),
      topologicalSpace R (fun (i : ι) ↦ (↑(B i) : Set ((fun (i : ι) ↦ R i) i))) 𝓕]
    ((fun (x : Πʳ (i : ι), [R i, (↑(B i) : Set ((fun (i : ι) ↦ R i) i))]_[𝓕]) ↦ g • x) ∘
      inclusion R (fun (i : ι) ↦ (↑(B i) : Set ((fun (i : ι) ↦ R i) i))) hT)

Tactic:
(continuous_inclusion hT).comp (continuous_const_smul g)

Premises used: ContinuousConstSMul.continuous_const_smul, Set.Mem, RestrictedProduct.inclusion, Continuous.comp, RestrictedProduct.continuous_inclusion
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
𝓕_1 𝓖 : Filter ι
S : ι → Type u_3
inst : (i : ι) → SetLike.{u_3, u_2} (S i) (R i)
B : (i : ι) → S i
T_1 : Set ι
𝓕 : Filter ι
inst_1 : (i : ι) → TopologicalSpace (R i)
G : Type u_4
inst_2 : (i : ι) → SMul.{u_4, u_2} G (R i)
inst_3 : ∀ (i : ι), SMulMemClass.{u_3, u_4, u_2} (S i) G (R i)
inst_4 : ∀ (i : ι), ContinuousConstSMul.{u_4, u_2} G (R i)
g : G
T : Set ι
hT : 𝓕 ≤ 𝓟 T
this : ContinuousConstSMul G Πʳ (i : ι), [R i, (↑(B i) : Set ((fun (i : ι) ↦ R i) i))]_[𝓟 T]
⊢ Continuous[topologicalSpace R (fun (i : ι) ↦ (↑(B i) : Set ((fun (i : ι) ↦ R i) i))) (𝓟 T),
      topologicalSpace R (fun (i : ι) ↦ (↑(B i) : Set ((fun (i : ι) ↦ R i) i))) 𝓕]
    ((fun (x : Πʳ (i : ι), [R i, (↑(B i) : Set ((fun (i : ι) ↦ R i) i))]_[𝓕]) ↦ g • x) ∘
      inclusion R (fun (i : ι) ↦ (↑(B i) : Set ((fun (i : ι) ↦ R i) i))) hT)

Tactic:
exact (continuous_inclusion hT).comp (continuous_const_smul g)

Premises used: ContinuousConstSMul.continuous_const_smul, Continuous.comp, RestrictedProduct.continuous_inclusion
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
𝓕_1 𝓖 : Filter ι
S : ι → Type u_3
inst : (i : ι) → SetLike.{u_3, u_2} (S i) (R i)
B : (i : ι) → S i
T : Set ι
𝓕 : Filter ι
inst_1 : (i : ι) → TopologicalSpace (R i)
inst_2 : (i : ι) → Mul (R i)
inst_3 : ∀ (i : ι), MulMemClass.{u_3, u_2} (S i) (R i)
inst_4 : ∀ (i : ι), ContinuousMul.{u_2} (R i)
⊢ ContinuousMul Πʳ (i : ι), [R i, (↑(B i) : Set ((fun (i : ι) ↦ R i) i))]_[𝓟 T]

Tactic:
let φ : Πʳ i, [R i, B i]_[𝓟 T] →ₙ* Π i, R i :=
  { toFun := (↑)
    map_mul' := fun _ _ ↦ rfl }
  isEmbedding_coe_of_principal.continuousMul φ

Premises used: Topology.IsInducing.continuousMul, RestrictedProduct.isEmbedding_coe_of_principal, MulHom.mk, Topology.IsEmbedding.toIsInducing, DFunLike.coe, rfl
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
𝓕_1 𝓖 : Filter ι
S : ι → Type u_3
inst : (i : ι) → SetLike.{u_3, u_2} (S i) (R i)
B : (i : ι) → S i
T : Set ι
𝓕 : Filter ι
inst_1 : (i : ι) → TopologicalSpace (R i)
G : Type u_4
inst_2 : TopologicalSpace G
inst_3 : (i : ι) → SMul.{u_4, u_2} G (R i)
inst_4 : ∀ (i : ι), SMulMemClass.{u_3, u_4, u_2} (S i) G (R i)
inst_5 : ∀ (i : ι), ContinuousSMul.{u_4, u_2} G (R i)
⊢ ContinuousSMul G Πʳ (i : ι), [R i, (↑(B i) : Set ((fun (i : ι) ↦ R i) i))]_[𝓟 T]

Tactic:
isEmbedding_coe_of_principal.continuousSMul continuous_id rfl

Premises used: Topology.IsInducing.continuousSMul, RestrictedProduct.isEmbedding_coe_of_principal, continuous_id, Topology.IsEmbedding.toIsInducing, rfl
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
Goal:
ι : Type u_1
R : ι → Type u_2
S : ι → Type u_3
inst : (i : ι) → SetLike.{u_3, u_2} (S i) (R i)
B : (i : ι) → S i
T : Set ι
inst_1 : (i : ι) → TopologicalSpace (R i)
inst_2 : (i : ι) → Zero (R i)
inst_3 : ∀ (i : ι), ZeroMemClass.{u_3, u_2} (S i) (R i)
hBopen : ∀ (i : ι), IsOpen[inst_1 i] (↑(B i) : Set (R i))
hT : cofinite ≤ 𝓟 T
⊢ Eq (α := Filter Πʳ (i : ι), [R i, (fun (i : ι) ↦ (↑(B i) : Set (R i))) i])
    (𝓝 (inclusion R (fun (i : ι) ↦ (↑(B i) : Set (R i))) hT 0))
    (Filter.map (inclusion R (fun (i : ι) ↦ (↑(B i) : Set (R i))) hT) (𝓝 0))

Tactic:
nhds_eq_map_inclusion hBopen hT 0

Premises used: OfNat.ofNat, RestrictedProduct.nhds_eq_map_inclusion
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
Goal:
ι : Type u_1
R : ι → Type u_2
S : ι → Type u_3
inst : (i : ι) → SetLike.{u_3, u_2} (S i) (R i)
B : (i : ι) → S i
inst_1 : (i : ι) → TopologicalSpace (R i)
inst_2 : (i : ι) → Zero (R i)
inst_3 : ∀ (i : ι), ZeroMemClass.{u_3, u_2} (S i) (R i)
hBopen : ∀ (i : ι), IsOpen[inst_1 i] (↑(B i) : Set (R i))
⊢ Eq (α := Filter Πʳ (i : ι), [R i, (fun (i : ι) ↦ (↑(B i) : Set (R i))) i])
    (𝓝 (structureMap R (fun (i : ι) ↦ (↑(B i) : Set (R i))) cofinite 0))
    (Filter.map (structureMap R (fun (i : ι) ↦ (↑(B i) : Set (R i))) cofinite) (𝓝 0))

Tactic:
nhds_eq_map_structureMap hBopen 0

Premises used: RestrictedProduct.nhds_eq_map_structureMap, OfNat.ofNat
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
𝓕_1 𝓖 : Filter ι
S : ι → Type u_3
inst : (i : ι) → SetLike.{u_3, u_2} (S i) (R i)
B : (i : ι) → S i
T : Set ι
𝓕 : Filter ι
inst_1 : (i : ι) → TopologicalSpace (R i)
hBopen : Fact (∀ (i : ι), IsOpen[inst_1 i] (↑(B i) : Set (R i)))
inst_2 : (i : ι) → Mul (R i)
inst_3 : ∀ (i : ι), MulMemClass.{u_3, u_2} (S i) (R i)
inst_4 : ∀ (i : ι), ContinuousMul.{u_2} (R i)
rw :
  ∀ (S_1 : Set ι) (hS : cofinite ≤ 𝓟 S_1),
    Continuous[instTopologicalSpaceProd,
        topologicalSpace R (fun (i : ι) ↦ (↑(B i) : Set ((fun (i : ι) ↦ R i) i))) cofinite]
      ((fun
            (p :
              Πʳ (i : ι), [R i, (↑(B i) : Set ((fun (i : ι) ↦ R i) i))] ×
                Πʳ (i : ι), [R i, (↑(B i) : Set ((fun (i : ι) ↦ R i) i))]) ↦
          p.1 * p.2) ∘
        Prod.map (inclusion R (fun (i : ι) ↦ (↑(B i) : Set (R i))) hS)
          (inclusion R (fun (i : ι) ↦ (↑(B i) : Set (R i))) hS))
⊢ Continuous[instTopologicalSpaceProd,
      topologicalSpace R (fun (i : ι) ↦ (↑(B i) : Set ((fun (i : ι) ↦ R i) i))) cofinite]
    fun
      (p :
        Πʳ (i : ι), [R i, (↑(B i) : Set ((fun (i : ι) ↦ R i) i))] ×
          Πʳ (i : ι), [R i, (↑(B i) : Set ((fun (i : ι) ↦ R i) i))]) ↦
    p.1 * p.2

Tactic:
rw [continuous_dom_prod hBopen.out hBopen.out]

Premises used: RestrictedProduct.continuous_dom_prod, Fact.out
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
𝓕_1 𝓖 : Filter ι
S : ι → Type u_3
inst : (i : ι) → SetLike.{u_3, u_2} (S i) (R i)
B : (i : ι) → S i
T : Set ι
𝓕 : Filter ι
inst_1 : (i : ι) → TopologicalSpace (R i)
hBopen : Fact (∀ (i : ι), IsOpen[inst_1 i] (↑(B i) : Set (R i)))
inst_2 : (i : ι) → Mul (R i)
inst_3 : ∀ (i : ι), MulMemClass.{u_3, u_2} (S i) (R i)
inst_4 : ∀ (i : ι), ContinuousMul.{u_2} (R i)
⊢ ∀ (S_1 : Set ι) (hS : cofinite ≤ 𝓟 S_1),
    Continuous[instTopologicalSpaceProd,
        topologicalSpace R (fun (i : ι) ↦ (↑(B i) : Set ((fun (i : ι) ↦ R i) i))) cofinite]
      ((fun
            (p :
              Πʳ (i : ι), [R i, (↑(B i) : Set ((fun (i : ι) ↦ R i) i))] ×
                Πʳ (i : ι), [R i, (↑(B i) : Set ((fun (i : ι) ↦ R i) i))]) ↦
          p.1 * p.2) ∘
        Prod.map (inclusion R (fun (i : ι) ↦ (↑(B i) : Set (R i))) hS)
          (inclusion R (fun (i : ι) ↦ (↑(B i) : Set (R i))) hS))

Tactic:
fun S hS ↦ (continuous_inclusion hS).comp continuous_mul

Premises used: Set.Mem, RestrictedProduct.inclusion, continuous_mul, Continuous.comp, RestrictedProduct.continuous_inclusion
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
𝓕_1 𝓖 : Filter ι
S : ι → Type u_3
inst : (i : ι) → SetLike.{u_3, u_2} (S i) (R i)
B : (i : ι) → S i
T : Set ι
𝓕 : Filter ι
inst_1 : (i : ι) → TopologicalSpace (R i)
hBopen : Fact (∀ (i : ι), IsOpen[inst_1 i] (↑(B i) : Set (R i)))
inst_2 : (i : ι) → Mul (R i)
inst_3 : ∀ (i : ι), MulMemClass.{u_3, u_2} (S i) (R i)
inst_4 : ∀ (i : ι), ContinuousMul.{u_2} (R i)
⊢ ∀ (S_1 : Set ι) (hS : cofinite ≤ 𝓟 S_1),
    Continuous[instTopologicalSpaceProd,
        topologicalSpace R (fun (i : ι) ↦ (↑(B i) : Set ((fun (i : ι) ↦ R i) i))) cofinite]
      ((fun
            (p :
              Πʳ (i : ι), [R i, (↑(B i) : Set ((fun (i : ι) ↦ R i) i))] ×
                Πʳ (i : ι), [R i, (↑(B i) : Set ((fun (i : ι) ↦ R i) i))]) ↦
          p.1 * p.2) ∘
        Prod.map (inclusion R (fun (i : ι) ↦ (↑(B i) : Set (R i))) hS)
          (inclusion R (fun (i : ι) ↦ (↑(B i) : Set (R i))) hS))

Tactic:
exact fun S hS ↦ (continuous_inclusion hS).comp continuous_mul

Premises used: continuous_mul, Continuous.comp, RestrictedProduct.continuous_inclusion
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
𝓕_1 𝓖 : Filter ι
S : ι → Type u_3
inst : (i : ι) → SetLike.{u_3, u_2} (S i) (R i)
B : (i : ι) → S i
T : Set ι
𝓕 : Filter ι
inst_1 : (i : ι) → TopologicalSpace (R i)
hBopen : Fact (∀ (i : ι), IsOpen[inst_1 i] (↑(B i) : Set (R i)))
G : Type u_4
inst_2 : TopologicalSpace G
inst_3 : (i : ι) → SMul.{u_4, u_2} G (R i)
inst_4 : ∀ (i : ι), SMulMemClass.{u_3, u_4, u_2} (S i) G (R i)
inst_5 : ∀ (i : ι), ContinuousSMul.{u_4, u_2} G (R i)
rw :
  ∀ (S_1 : Set ι) (hS : cofinite ≤ 𝓟 S_1),
    Continuous[instTopologicalSpaceProd,
        topologicalSpace R (fun (i : ι) ↦ (↑(B i) : Set ((fun (i : ι) ↦ R i) i))) cofinite]
      ((fun (p : G × Πʳ (i : ι), [R i, (↑(B i) : Set ((fun (i : ι) ↦ R i) i))]) ↦ p.1 • p.2) ∘
        Prod.map id (inclusion R (fun (i : ι) ↦ (↑(B i) : Set (R i))) hS))
⊢ Continuous[instTopologicalSpaceProd,
      topologicalSpace R (fun (i : ι) ↦ (↑(B i) : Set ((fun (i : ι) ↦ R i) i))) cofinite]
    fun (p : G × Πʳ (i : ι), [R i, (↑(B i) : Set ((fun (i : ι) ↦ R i) i))]) ↦ p.1 • p.2

Tactic:
rw [continuous_dom_prod_left hBopen.out]

Premises used: RestrictedProduct.continuous_dom_prod_left, Fact.out
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
𝓕_1 𝓖 : Filter ι
S : ι → Type u_3
inst : (i : ι) → SetLike.{u_3, u_2} (S i) (R i)
B : (i : ι) → S i
T : Set ι
𝓕 : Filter ι
inst_1 : (i : ι) → TopologicalSpace (R i)
hBopen : Fact (∀ (i : ι), IsOpen[inst_1 i] (↑(B i) : Set (R i)))
G : Type u_4
inst_2 : TopologicalSpace G
inst_3 : (i : ι) → SMul.{u_4, u_2} G (R i)
inst_4 : ∀ (i : ι), SMulMemClass.{u_3, u_4, u_2} (S i) G (R i)
inst_5 : ∀ (i : ι), ContinuousSMul.{u_4, u_2} G (R i)
⊢ ∀ (S_1 : Set ι) (hS : cofinite ≤ 𝓟 S_1),
    Continuous[instTopologicalSpaceProd,
        topologicalSpace R (fun (i : ι) ↦ (↑(B i) : Set ((fun (i : ι) ↦ R i) i))) cofinite]
      ((fun (p : G × Πʳ (i : ι), [R i, (↑(B i) : Set ((fun (i : ι) ↦ R i) i))]) ↦ p.1 • p.2) ∘
        Prod.map id (inclusion R (fun (i : ι) ↦ (↑(B i) : Set (R i))) hS))

Tactic:
fun S hS ↦ (continuous_inclusion hS).comp continuous_smul

Premises used: Set.Mem, RestrictedProduct.inclusion, Filter.Eventually, Continuous.comp, setOf, Set.Finite, Set.Subset, RestrictedProduct, RestrictedProduct.continuous_inclusion, Filter.principal, Filter.cofinite, ContinuousSMul.continuous_smul
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
𝓕_1 𝓖 : Filter ι
S : ι → Type u_3
inst : (i : ι) → SetLike.{u_3, u_2} (S i) (R i)
B : (i : ι) → S i
T : Set ι
𝓕 : Filter ι
inst_1 : (i : ι) → TopologicalSpace (R i)
hBopen : Fact (∀ (i : ι), IsOpen[inst_1 i] (↑(B i) : Set (R i)))
G : Type u_4
inst_2 : TopologicalSpace G
inst_3 : (i : ι) → SMul.{u_4, u_2} G (R i)
inst_4 : ∀ (i : ι), SMulMemClass.{u_3, u_4, u_2} (S i) G (R i)
inst_5 : ∀ (i : ι), ContinuousSMul.{u_4, u_2} G (R i)
⊢ ∀ (S_1 : Set ι) (hS : cofinite ≤ 𝓟 S_1),
    Continuous[instTopologicalSpaceProd,
        topologicalSpace R (fun (i : ι) ↦ (↑(B i) : Set ((fun (i : ι) ↦ R i) i))) cofinite]
      ((fun (p : G × Πʳ (i : ι), [R i, (↑(B i) : Set ((fun (i : ι) ↦ R i) i))]) ↦ p.1 • p.2) ∘
        Prod.map id (inclusion R (fun (i : ι) ↦ (↑(B i) : Set (R i))) hS))

Tactic:
exact fun S hS ↦ (continuous_inclusion hS).comp continuous_smul

Premises used: Continuous.comp, RestrictedProduct.continuous_inclusion, ContinuousSMul.continuous_smul
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
Goal:
ι : Type u_1
R : ι → Type u_2
S : ι → Type u_3
inst : (i : ι) → SetLike.{u_3, u_2} (S i) (R i)
B : (i : ι) → S i
inst_1 : (i : ι) → TopologicalSpace (R i)
hBopen : Fact (∀ (i : ι), IsOpen[inst_1 i] (↑(B i) : Set (R i)))
inst_2 : (i : ι) → Group (R i)
inst_3 : ∀ (i : ι), SubgroupClass.{u_3, u_2} (S i) (R i)
inst_4 : ∀ (i : ι), IsTopologicalGroup.{u_2} (R i)
inst_5 : ∀ (i : ι), LocallyCompactSpace.{u_2} (R i)
hBcompact : ∀ᶠ (i : ι) in cofinite, IsCompact (↑(B i) : Set (R i))
⊢ LocallyCompactSpace Πʳ (i : ι), [R i, (↑(B i) : Set ((fun (i : ι) ↦ R i) i))]

Tactic:
haveI : WeaklyLocallyCompactSpace (Πʳ i, [R i, B i]) :=
    weaklyLocallyCompactSpace_of_cofinite hBopen.out hBcompact
  inferInstance

Premises used: inferInstance
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
𝓕_1 𝓖 : Filter ι
S : ι → Type u_3
inst : (i : ι) → SetLike.{u_3, u_2} (S i) (R i)
B : (i : ι) → S i
T : Set ι
𝓕 : Filter ι
inst_1 : (i : ι) → TopologicalSpace (R i)
hBopen : Fact (∀ (i : ι), IsOpen[inst_1 i] (↑(B i) : Set (R i)))
inst_2 : (i : ι) → Group (R i)
inst_3 : ∀ (i : ι), SubgroupClass.{u_3, u_2} (S i) (R i)
inst_4 : ∀ (i : ι), IsTopologicalGroup.{u_2} (R i)
hAcompact : ∀ (i : ι), CompactSpace.{u_2} ↥(B i)
i : ι
x : R i
⊢ x ∈ x • (↑(B i) : Set (R i))

Tactic:
simpa using smul_mem_smul_set (a := x) (one_mem (B i))

Premises used: OneMemClass.one_mem, Set.smul_mem_smul_set
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
Goal:
ι₁ : Type u_3
ι₂ : Type u_4
R₁ : ι₁ → Type u_5
R₂ : ι₂ → Type u_6
inst : (i : ι₁) → TopologicalSpace (R₁ i)
inst_1 : (i : ι₂) → TopologicalSpace (R₂ i)
𝓕₁ : Filter ι₁
𝓕₂ : Filter ι₂
A₁ : (i : ι₁) → Set (R₁ i)
A₂ : (i : ι₂) → Set (R₂ i)
f : ι₂ → ι₁
hf : Tendsto f 𝓕₂ 𝓕₁
φ : (j : ι₂) → R₁ (f j) → R₂ j
hφ : ∀ᶠ (j : ι₂) in 𝓕₂, MapsTo (φ j) (A₁ (f j)) (A₂ j)
φ_cont : ∀ (j : ι₂), Continuous[inst (f j), inst_1 j] (φ j)
rw :
  ∀ (S : Set ι₁) (hS : 𝓕₁ ≤ 𝓟 S),
    Continuous[topologicalSpace R₁ A₁ (𝓟 S), topologicalSpace R₂ A₂ 𝓕₂]
      (mapAlong R₁ R₂ (A₁ := A₁) (A₂ := A₂) f hf φ hφ ∘ inclusion R₁ A₁ hS)
⊢ Continuous[topologicalSpace R₁ A₁ 𝓕₁, topologicalSpace R₂ A₂ 𝓕₂] (mapAlong R₁ R₂ (A₁ := A₁) (A₂ := A₂) f hf φ hφ)

Tactic:
rw [continuous_dom]

Premises used: RestrictedProduct.continuous_dom