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)
X : Type u_3
Y : Type u_4
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Y
f : Y × Πʳ (i : ι), [R i, A i] → X
refine :
  ∀
    (H :
      ∀ (S : Set ι) (hS : cofinite ≤ 𝓟 S),
        Continuous[instTopologicalSpaceProd, inst_1] (f ∘ Prod.map id (inclusion R A hS))),
    Continuous[instTopologicalSpaceProd, inst_1] f
⊢ Continuous[instTopologicalSpaceProd, inst_1] f ↔
    ∀ (S : Set ι) (hS : cofinite ≤ 𝓟 S),
      Continuous[instTopologicalSpaceProd, inst_1] (f ∘ Prod.map id (inclusion R A hS))

Tactic:
refine ⟨fun H S hS ↦ H.comp (continuous_id.prodMap (continuous_inclusion hS)),
    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 : Y × Πʳ (i : ι), [R i, A i] → X
H :
  ∀ (S : Set ι) (hS : cofinite ≤ 𝓟 S), Continuous[instTopologicalSpaceProd, inst_1] (f ∘ Prod.map id (inclusion R A hS))
simp_rw : ∀ (x : Y × Πʳ (i : ι), [R i, A i]), 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 : Y × Πʳ (i : ι), [R i, A i] → X
H :
  ∀ (S : Set ι) (hS : cofinite ≤ 𝓟 S), Continuous[instTopologicalSpaceProd, inst_1] (f ∘ Prod.map id (inclusion R A hS))
y : Y
x : Πʳ (i : ι), [R i, A i]
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 : Y × Πʳ (i : ι), [R i, A i] → X
H :
  ∀ (S : Set ι) (hS : cofinite ≤ 𝓟 S), Continuous[instTopologicalSpaceProd, inst_1] (f ∘ Prod.map id (inclusion R A hS))
y : Y
x : Πʳ (i : ι), [R i, A i]
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 : Y × Πʳ (i : ι), [R i, A i] → X
H :
  ∀ (S : Set ι) (hS : cofinite ≤ 𝓟 S), Continuous[instTopologicalSpaceProd, inst_1] (f ∘ Prod.map id (inclusion R A hS))
y : Y
x : Πʳ (i : ι), [R i, A i]
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 (𝓝 (y, x)) (𝓝 (f (y, x)))
⊢ Tendsto f (𝓝 (y, x)) (𝓝 (f (y, x)))

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 : Y × Πʳ (i : ι), [R i, A i] → X
H :
  ∀ (S : Set ι) (hS : cofinite ≤ 𝓟 S), Continuous[instTopologicalSpaceProd, inst_1] (f ∘ Prod.map id (inclusion R A hS))
y : Y
x : Πʳ (i : ι), [R i, A i]
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 : Y × Πʳ (i : ι), [R i, A i]_[𝓟 S]) ↦ (id p.1, inclusion R A hS p.2)) (𝓝 (y, x'))
    (𝓝 (f (y, inclusion R A hS x')))
⊢ Tendsto f (𝓝 (y, x)) (𝓝 (f (y, x)))

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 : Y × Πʳ (i : ι), [R i, A i] → X
H :
  ∀ (S : Set ι) (hS : cofinite ≤ 𝓟 S), Continuous[instTopologicalSpaceProd, inst_1] (f ∘ Prod.map id (inclusion R A hS))
y : Y
x : Πʳ (i : ι), [R i, A i]
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 : Y × Πʳ (i : ι), [R i, A i]_[𝓟 S]) ↦ (id p.1, inclusion R A hS p.2)) (𝓝 (y, x'))
    (𝓝 (f (y, inclusion R A hS x')))

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

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 : Y × Πʳ (i : ι), [R i, A i] → X
H :
  ∀ (S : Set ι) (hS : cofinite ≤ 𝓟 S), Continuous[instTopologicalSpaceProd, inst_1] (f ∘ Prod.map id (inclusion R A hS))
y : Y
x : Πʳ (i : ι), [R i, A i]
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 : Y × Πʳ (i : ι), [R i, A i]_[𝓟 S]) ↦ (id p.1, inclusion R A hS p.2)) (𝓝 (y, x'))
    (𝓝 (f (y, inclusion R A hS x')))

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

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)
R' : ι → Type u_3
A' : (i : ι) → Set (R' i)
inst_1 : (i : ι) → TopologicalSpace (R' i)
hAopen' : ∀ (i : ι), IsOpen[inst_1 i] (A' i)
X : Type u_4
inst_2 : TopologicalSpace X
f : Πʳ (i : ι), [R i, A i] × Πʳ (i : ι), [R' i, A' i] → X
simp_rw :
  (∀ (S : Set ι) (hS : cofinite ≤ 𝓟 S) (S_1 : Set ι) (hS_1 : cofinite ≤ 𝓟 S_1),
      Continuous[instTopologicalSpaceProd, inst_2]
        ((f ∘ Prod.map (inclusion R A hS) id) ∘ Prod.map id (inclusion R' A' hS_1))) ↔
    ∀ (S : Set ι) (hS : cofinite ≤ 𝓟 S),
      Continuous[instTopologicalSpaceProd, inst_2] (f ∘ Prod.map (inclusion R A hS) (inclusion R' A' hS))
⊢ Continuous[instTopologicalSpaceProd, inst_2] f ↔
    ∀ (S : Set ι) (hS : cofinite ≤ 𝓟 S),
      Continuous[instTopologicalSpaceProd, inst_2] (f ∘ Prod.map (inclusion R A hS) (inclusion R' A' hS))

Tactic:
simp_rw [continuous_dom_prod_right hAopen, continuous_dom_prod_left hAopen']

Premises used: RestrictedProduct.continuous_dom_prod_right, RestrictedProduct.continuous_dom_prod_left
-- 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)
R' : ι → Type u_3
A' : (i : ι) → Set (R' i)
inst_1 : (i : ι) → TopologicalSpace (R' i)
hAopen' : ∀ (i : ι), IsOpen[inst_1 i] (A' i)
X : Type u_4
inst_2 : TopologicalSpace X
f : Πʳ (i : ι), [R i, A i] × Πʳ (i : ι), [R' i, A' i] → X
⊢ (∀ (S : Set ι) (hS : cofinite ≤ 𝓟 S) (S_1 : Set ι) (hS_1 : cofinite ≤ 𝓟 S_1),
      Continuous[instTopologicalSpaceProd, inst_2]
        ((f ∘ Prod.map (inclusion R A hS) id) ∘ Prod.map id (inclusion R' A' hS_1))) ↔
    ∀ (S : Set ι) (hS : cofinite ≤ 𝓟 S),
      Continuous[instTopologicalSpaceProd, inst_2] (f ∘ Prod.map (inclusion R A hS) (inclusion R' A' hS))

Tactic:
⟨fun H S hS ↦ H S hS S hS, fun H S hS T hT ↦ ?_⟩

Premises used: 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)
R' : ι → Type u_3
A' : (i : ι) → Set (R' i)
inst_1 : (i : ι) → TopologicalSpace (R' i)
hAopen' : ∀ (i : ι), IsOpen[inst_1 i] (A' i)
X : Type u_4
inst_2 : TopologicalSpace X
f : Πʳ (i : ι), [R i, A i] × Πʳ (i : ι), [R' i, A' i] → X
refine :
  ∀
    (H :
      ∀ (S : Set ι) (hS : cofinite ≤ 𝓟 S),
        Continuous[instTopologicalSpaceProd, inst_2] (f ∘ Prod.map (inclusion R A hS) (inclusion R' A' hS)))
    (S : Set ι) (hS : cofinite ≤ 𝓟 S) (T : Set ι) (hT : cofinite ≤ 𝓟 T),
    Continuous[instTopologicalSpaceProd, inst_2]
      ((f ∘ Prod.map (inclusion R A hS) id) ∘ Prod.map id (inclusion R' A' hT))
⊢ (∀ (S : Set ι) (hS : cofinite ≤ 𝓟 S) (S_1 : Set ι) (hS_1 : cofinite ≤ 𝓟 S_1),
      Continuous[instTopologicalSpaceProd, inst_2]
        ((f ∘ Prod.map (inclusion R A hS) id) ∘ Prod.map id (inclusion R' A' hS_1))) ↔
    ∀ (S : Set ι) (hS : cofinite ≤ 𝓟 S),
      Continuous[instTopologicalSpaceProd, inst_2] (f ∘ Prod.map (inclusion R A hS) (inclusion R' A' hS))

Tactic:
refine ⟨fun H S hS ↦ H S hS S hS, fun H S hS T hT ↦ ?_⟩
-- 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)
R' : ι → Type u_3
A' : (i : ι) → Set (R' i)
inst_1 : (i : ι) → TopologicalSpace (R' i)
hAopen' : ∀ (i : ι), IsOpen[inst_1 i] (A' i)
X : Type u_4
inst_2 : TopologicalSpace X
f : Πʳ (i : ι), [R i, A i] × Πʳ (i : ι), [R' i, A' i] → X
H :
  ∀ (S : Set ι) (hS : cofinite ≤ 𝓟 S),
    Continuous[instTopologicalSpaceProd, inst_2] (f ∘ Prod.map (inclusion R A hS) (inclusion R' A' hS))
S : Set ι
hS : cofinite ≤ 𝓟 S
T : Set ι
hT : cofinite ≤ 𝓟 T
U : Set ι := S ∩ T
⊢ cofinite ≤ 𝓟 (S ∩ T)

Tactic:
have hU : cofinite ≤ 𝓟 (S ∩ T) := inf_principal ▸ le_inf hS hT
-- 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)
R' : ι → Type u_3
A' : (i : ι) → Set (R' i)
inst_1 : (i : ι) → TopologicalSpace (R' i)
hAopen' : ∀ (i : ι), IsOpen[inst_1 i] (A' i)
X : Type u_4
inst_2 : TopologicalSpace X
f : Πʳ (i : ι), [R i, A i] × Πʳ (i : ι), [R' i, A' i] → X
H :
  ∀ (S : Set ι) (hS : cofinite ≤ 𝓟 S),
    Continuous[instTopologicalSpaceProd, inst_2] (f ∘ Prod.map (inclusion R A hS) (inclusion R' A' hS))
S : Set ι
hS : cofinite ≤ 𝓟 S
T : Set ι
hT : cofinite ≤ 𝓟 T
U : Set ι := S ∩ T
hU : cofinite ≤ 𝓟 (S ∩ T)
⊢ 𝓟 U ≤ 𝓟 S

Tactic:
have hSU : 𝓟 U ≤ 𝓟 S := principal_mono.mpr inter_subset_left
-- 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)
R' : ι → Type u_3
A' : (i : ι) → Set (R' i)
inst_1 : (i : ι) → TopologicalSpace (R' i)
hAopen' : ∀ (i : ι), IsOpen[inst_1 i] (A' i)
X : Type u_4
inst_2 : TopologicalSpace X
f : Πʳ (i : ι), [R i, A i] × Πʳ (i : ι), [R' i, A' i] → X
H :
  ∀ (S : Set ι) (hS : cofinite ≤ 𝓟 S),
    Continuous[instTopologicalSpaceProd, inst_2] (f ∘ Prod.map (inclusion R A hS) (inclusion R' A' hS))
S : Set ι
hS : cofinite ≤ 𝓟 S
T : Set ι
hT : cofinite ≤ 𝓟 T
U : Set ι := S ∩ T
hU : cofinite ≤ 𝓟 (S ∩ T)
hSU : 𝓟 U ≤ 𝓟 S
⊢ 𝓟 U ≤ 𝓟 T

Tactic:
have hTU : 𝓟 U ≤ 𝓟 T := principal_mono.mpr inter_subset_right
-- 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)
R' : ι → Type u_3
A' : (i : ι) → Set (R' i)
inst_1 : (i : ι) → TopologicalSpace (R' i)
hAopen' : ∀ (i : ι), IsOpen[inst_1 i] (A' i)
X : Type u_4
inst_2 : TopologicalSpace X
f : Πʳ (i : ι), [R i, A i] × Πʳ (i : ι), [R' i, A' i] → X
H :
  ∀ (S : Set ι) (hS : cofinite ≤ 𝓟 S),
    Continuous[instTopologicalSpaceProd, inst_2] (f ∘ Prod.map (inclusion R A hS) (inclusion R' A' hS))
S : Set ι
hS : cofinite ≤ 𝓟 S
T : Set ι
hT : cofinite ≤ 𝓟 T
U : Set ι := S ∩ T
hU : cofinite ≤ 𝓟 (S ∩ T)
hSU : 𝓟 U ≤ 𝓟 S
hTU : 𝓟 U ≤ 𝓟 T
⊢ Continuous[instTopologicalSpaceProd, inst_2] ((f ∘ Prod.map (inclusion R A hS) id) ∘ Prod.map id (inclusion R' A' hT))

Tactic:
(H U hU).comp ((continuous_inclusion hSU).prodMap (continuous_inclusion hTU))

Premises used: Continuous.prodMap, Set.Mem, RestrictedProduct.inclusion, Filter.Eventually, Continuous.comp, setOf, Prod.map, Set.inter, Set.Subset, RestrictedProduct, RestrictedProduct.continuous_inclusion, 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)
hAopen : ∀ (i : ι), IsOpen[inst i] (A i)
R' : ι → Type u_3
A' : (i : ι) → Set (R' i)
inst_1 : (i : ι) → TopologicalSpace (R' i)
hAopen' : ∀ (i : ι), IsOpen[inst_1 i] (A' i)
X : Type u_4
inst_2 : TopologicalSpace X
f : Πʳ (i : ι), [R i, A i] × Πʳ (i : ι), [R' i, A' i] → X
H :
  ∀ (S : Set ι) (hS : cofinite ≤ 𝓟 S),
    Continuous[instTopologicalSpaceProd, inst_2] (f ∘ Prod.map (inclusion R A hS) (inclusion R' A' hS))
S : Set ι
hS : cofinite ≤ 𝓟 S
T : Set ι
hT : cofinite ≤ 𝓟 T
U : Set ι := S ∩ T
hU : cofinite ≤ 𝓟 (S ∩ T)
hSU : 𝓟 U ≤ 𝓟 S
hTU : 𝓟 U ≤ 𝓟 T
⊢ Continuous[instTopologicalSpaceProd, inst_2] ((f ∘ Prod.map (inclusion R A hS) id) ∘ Prod.map id (inclusion R' A' hT))

Tactic:
exact (H U hU).comp ((continuous_inclusion hSU).prodMap (continuous_inclusion hTU))

Premises used: Continuous.prodMap, Continuous.comp, RestrictedProduct.continuous_inclusion
-- 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
⊢ Continuous[Pi.topologicalSpace, inst_1] f →
    ∀ (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)

Tactic:
fun_prop
-- 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
refine :
  ∀
    (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)),
    Continuous[Pi.topologicalSpace, inst_1] f
⊢ Continuous[Pi.topologicalSpace, inst_1] f ↔
    ∀ (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)

Tactic:
refine ⟨by fun_prop, fun H ↦ ?_⟩
-- 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)
simp_rw : ∀ (x : (j : n) → Πʳ (i : ι), [A j i, C j i]), Tendsto f (𝓝 x) (𝓝 (f x))
⊢ Continuous[Pi.topologicalSpace, 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
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}
rw : Membership.mem (γ := Filter ι) cofinite S
⊢ cofinite ≤ 𝓟 S

Tactic:
rw [le_principal_iff]

Premises used: Filter.le_principal_iff
-- 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}
change : ∀ᶠ (i : ι) in cofinite, ∀ (j : n), (x j : (a : ι) → A j a) i ∈ C j i
⊢ Membership.mem (γ := Filter ι) cofinite S

Tactic:
change ∀ᶠ i in cofinite, ∀ j : n, x j i ∈ C j i

Premises used: Filter.cofinite
-- 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}
⊢ ∀ᶠ (i : ι) in cofinite, ∀ (j : n), (x j : (a : ι) → A j a) i ∈ C j i

Tactic:
simp [-eventually_cofinite]

Premises used: Filter.eventually_cofinite
-- 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}
⊢ cofinite ≤ 𝓟 S

Tactic:
have hS : cofinite ≤ 𝓟 S := by
    rw [le_principal_iff]
    change ∀ᶠ i in cofinite, ∀ j : n, x j i ∈ C j i
    simp [-eventually_cofinite]
-- 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) ⋯
⊢ 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

Tactic:
have hxx' : Pi.map (fun j ↦ inclusion _ _ hS) x' = x := rfl
-- 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
simp_rw :
  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')))
⊢ Tendsto f (𝓝 x) (𝓝 (f x))

Tactic:
simp_rw [← hxx', nhds_pi, Pi.map_apply, nhds_eq_map_inclusion (hCopen _), ← map_piMap_pi_finite,
    tendsto_map'_iff, ← nhds_pi]

Premises used: Filter.tendsto_map'_iff, nhds_pi, Filter.map_piMap_pi_finite, Pi.map_apply, RestrictedProduct.nhds_eq_map_inclusion