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)
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:
exact H i 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)
⊢ Subset (α := Set Πʳ (i : ι), [R i, A i]_[𝓟 S]) (DFunLike.coe (β := R) ⁻¹' U) (DFunLike.coe (β := R) ⁻¹' Q)

Tactic:
have QU : (↑) ⁻¹' U ⊆ ((↑) ⁻¹' Q : Set (Πʳ i, [R i, A i]_[𝓟 S])) := fun y H i _ ↦ by
      dsimp only
      split_ifs with hi
      · exact y.2 hi
      · exact H i 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)
QU : Subset (α := Set Πʳ (i : ι), [R i, A i]_[𝓟 S]) (DFunLike.coe (β := R) ⁻¹' U) (DFunLike.coe (β := R) ⁻¹' Q)
⊢ ∃ (s : Set Πʳ (i : ι), [R i, A i]_[𝓟 S]), IsCompact s ∧ s ∈ 𝓝 x

Tactic:
⟨((↑) ⁻¹' Q), ?_, mem_of_superset ?_ QU⟩

Premises used: Set.preimage, And.intro, Exists.intro, Filter.mem_of_superset
-- 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)
QU : Subset (α := Set Πʳ (i : ι), [R i, A i]_[𝓟 S]) (DFunLike.coe (β := R) ⁻¹' U) (DFunLike.coe (β := R) ⁻¹' Q)
refine_1 : IsCompact (X := Πʳ (i : ι), [R i, A i]_[𝓟 S]) (DFunLike.coe (β := R) ⁻¹' Q)
refine_2 : DFunLike.coe (β := R) ⁻¹' U ∈ 𝓝 x
⊢ ∃ (s : Set Πʳ (i : ι), [R i, A i]_[𝓟 S]), IsCompact s ∧ s ∈ 𝓝 x

Tactic:
refine ⟨((↑) ⁻¹' Q), ?_, mem_of_superset ?_ QU⟩
-- 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)
QU : Subset (α := Set Πʳ (i : ι), [R i, A i]_[𝓟 S]) (DFunLike.coe (β := R) ⁻¹' U) (DFunLike.coe (β := R) ⁻¹' Q)
⊢ IsCompact (X := Πʳ (i : ι), [R i, A i]_[𝓟 S]) (DFunLike.coe (β := R) ⁻¹' Q)

Tactic:
isEmbedding_coe_of_principal.isCompact_preimage_iff ?_ |>.mpr Q_compact

Premises used: Iff.mpr, RestrictedProduct.isEmbedding_coe_of_principal, Topology.IsEmbedding.toIsInducing, Topology.IsInducing.isCompact_preimage_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]
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)
QU : Subset (α := Set Πʳ (i : ι), [R i, A i]_[𝓟 S]) (DFunLike.coe (β := R) ⁻¹' U) (DFunLike.coe (β := R) ⁻¹' Q)
refine_1 : Q ⊆ range (ι := Πʳ (i : ι), [R i, A i]_[𝓟 S]) (DFunLike.coe (β := R))
⊢ IsCompact (X := Πʳ (i : ι), [R i, A i]_[𝓟 S]) (DFunLike.coe (β := R) ⁻¹' Q)

Tactic:
refine isEmbedding_coe_of_principal.isCompact_preimage_iff ?_ |>.mpr Q_compact

Premises used: Iff.mpr, RestrictedProduct.isEmbedding_coe_of_principal, Topology.IsEmbedding.toIsInducing, Topology.IsInducing.isCompact_preimage_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]
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)
QU : Subset (α := Set Πʳ (i : ι), [R i, A i]_[𝓟 S]) (DFunLike.coe (β := R) ⁻¹' U) (DFunLike.coe (β := R) ⁻¹' Q)
refine_1 : Set.pi (α := R) {i : ι | i ∈ S} A ∩ Set.pi (α := R) {i : ι | i ∉ S} K ⊆ S.pi (α := R) A
⊢ Q ⊆ range (ι := Πʳ (i : ι), [R i, A i]_[𝓟 S]) (DFunLike.coe (β := R))

Tactic:
simp_rw [range_coe_principal, Q_def, pi_if, mem_univ, true_and]

Premises used: RestrictedProduct.range_coe_principal, Set.pi_if, Set.mem_univ, true_and
-- 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)
QU : Subset (α := Set Πʳ (i : ι), [R i, A i]_[𝓟 S]) (DFunLike.coe (β := R) ⁻¹' U) (DFunLike.coe (β := R) ⁻¹' Q)
⊢ Set.pi (α := R) {i : ι | i ∈ S} A ∩ Set.pi (α := R) {i : ι | i ∉ S} K ⊆ S.pi (α := R) A

Tactic:
inter_subset_left

Premises used: Set.Mem, setOf, Set.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)
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)
QU : Subset (α := Set Πʳ (i : ι), [R i, A i]_[𝓟 S]) (DFunLike.coe (β := R) ⁻¹' U) (DFunLike.coe (β := R) ⁻¹' Q)
⊢ Set.pi (α := R) {i : ι | i ∈ S} A ∩ Set.pi (α := R) {i : ι | i ∉ S} K ⊆ S.pi (α := R) A

Tactic:
exact inter_subset_left

Premises used: Set.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)
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)
QU : Subset (α := Set Πʳ (i : ι), [R i, A i]_[𝓟 S]) (DFunLike.coe (β := R) ⁻¹' U) (DFunLike.coe (β := R) ⁻¹' Q)
⊢ DFunLike.coe (β := R) ⁻¹' U ∈ 𝓝 x

Tactic:
simpa only [isEmbedding_coe_of_principal.nhds_eq_comap] using preimage_mem_comap U_nhds

Premises used: Topology.IsInducing.nhds_eq_comap, RestrictedProduct.isEmbedding_coe_of_principal, Filter.preimage_mem_comap, Topology.IsEmbedding.toIsInducing
-- 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)
S : Set ι
inst_1 : ∀ (i : ι), WeaklyLocallyCompactSpace.{u_2} (R i)
hS : Fact (cofinite ≤ 𝓟 S)
hAcompact : ∀ (i : ι), CompactSpace.{u_2} (↑(A i) : Type u_2)
⊢ WeaklyLocallyCompactSpace Πʳ (i : ι), [R i, A i]_[𝓟 S]

Tactic:
weaklyLocallyCompactSpace_of_principal hS.out
    fun _ _ ↦ isCompact_iff_compactSpace.mpr inferInstance

Premises used: Iff.mpr, isCompact_iff_compactSpace, inferInstance, RestrictedProduct.weaklyLocallyCompactSpace_of_principal, Fact.out
-- 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)
simp_rw :
  topologicalSpace R A 𝓕 =
    ⨆ (S : Set ι),
      ⨆ (x : 𝓕 ≤ 𝓟 S),
        TopologicalSpace.coinduced (inclusion R A ⋯) (TopologicalSpace.induced (DFunLike.coe (β := R)) inferInstance)
⊢ topologicalSpace R A 𝓕 =
    ⨆ (S : Set ι), ⨆ (hS : 𝓕 ≤ 𝓟 S), TopologicalSpace.coinduced (inclusion R A hS) (topologicalSpace R A (𝓟 S))

Tactic:
simp_rw [topologicalSpace_eq_of_principal, topologicalSpace]

Premises used: RestrictedProduct.topologicalSpace, RestrictedProduct.topologicalSpace_eq_of_principal
-- 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)
X : Type u_3
inst_1 : TopologicalSpace X
f : Πʳ (i : ι), [R i, A i]_[𝓕] → X
simp_rw :
  Continuous[topologicalSpace R A 𝓕, inst_1] f ↔
    ∀ (S : Set ι) (hS : 𝓕 ≤ 𝓟 S),
      Continuous[TopologicalSpace.induced DFunLike.coe inferInstance, inst_1] (f ∘ inclusion R A hS)
simp_rw₁ :
  (∀ (i : Set ι) (i_1 : 𝓕 ≤ 𝓟 i),
      Continuous[TopologicalSpace.coinduced (inclusion R A i_1) (TopologicalSpace.induced DFunLike.coe inferInstance),
          inst_1]
        f) ↔
    ∀ (S : Set ι) (hS : 𝓕 ≤ 𝓟 S),
      Continuous[TopologicalSpace.induced DFunLike.coe inferInstance, inst_1] (f ∘ inclusion R A hS)
⊢ Continuous[topologicalSpace R A 𝓕, inst_1] f ↔
    ∀ (S : Set ι) (hS : 𝓕 ≤ 𝓟 S), Continuous[topologicalSpace R A (𝓟 S), inst_1] (f ∘ inclusion R A hS)

Tactic:
simp_rw +instances [topologicalSpace_eq_of_principal, continuous_iSup_dom,
    continuous_coinduced_dom]

Premises used: continuous_coinduced_dom, continuous_iSup_dom, RestrictedProduct.topologicalSpace_eq_of_principal
-- 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)
S : Set ι
hS : 𝓕 ≤ 𝓟 S
⊢ IsEmbedding (inclusion R A hS)

Tactic:
.of_comp (continuous_inclusion hS) continuous_coe isEmbedding_coe_of_principal

Premises used: RestrictedProduct.continuous_coe, RestrictedProduct.isEmbedding_coe_of_principal, RestrictedProduct.continuous_inclusion, Topology.IsEmbedding.of_comp
-- 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)
⊢ IsEmbedding (X := Πʳ (i : ι), [R i, A i]_[⊤]) (Y := Πʳ (i : ι), [R i, A i]_[𝓕]) (inclusion R A ⋯)

Tactic:
.of_comp (continuous_inclusion _) continuous_coe isEmbedding_coe_of_top

Premises used: RestrictedProduct.continuous_coe, RestrictedProduct.continuous_inclusion, RestrictedProduct.isEmbedding_coe_of_top, Topology.IsEmbedding.of_comp
-- 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)
⊢ IsEmbedding (structureMap R A 𝓕)

Tactic:
isEmbedding_inclusion_top.comp homeoTop.isEmbedding

Premises used: RestrictedProduct.homeoTop, RestrictedProduct.structureMap, Homeomorph.isEmbedding, RestrictedProduct.inclusion, Topology.IsEmbedding.comp, RestrictedProduct.isEmbedding_inclusion_top
-- 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
p : ι → Prop
rw :
  ∀ (hS : Membership.mem (γ := Filter ι) cofinite S) {p : ι → Prop},
    IsOpen[topologicalSpace R A (𝓟 S)]
      {f : Πʳ (i : ι), [R i, A i]_[𝓟 S] | ∀ (i : ι), p i → (↑f : (i : ι) → (fun (i : ι) ↦ R i) i) i ∈ A i}
⊢ IsOpen[topologicalSpace R A (𝓟 S)]
    {f : Πʳ (i : ι), [R i, A i]_[𝓟 S] | ∀ (i : ι), p i → (↑f : (i : ι) → (fun (i : ι) ↦ R i) i) i ∈ A i}

Tactic:
rw [le_principal_iff] at hS

Premises used: 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)
hAopen : ∀ (i : ι), IsOpen[inst i] (A i)
S : Set ι
hS : Membership.mem (γ := Filter ι) cofinite S
p : ι → Prop
⊢ IsOpen[topologicalSpace R A (𝓟 S)] (DFunLike.coe (β := R) ⁻¹' (Sᶜ ∩ {i : ι | p i}).pi (α := R) A)

Tactic:
isOpen_set_pi (hS.inter_of_left {i | p i}) (fun i _ ↦ hAopen i) |>.preimage continuous_coe

Premises used: RestrictedProduct.continuous_coe, Set.Finite.inter_of_left, setOf, isOpen_set_pi, IsOpen.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)
S : Set ι
hS : Membership.mem (γ := Filter ι) cofinite S
p : ι → Prop
h :
  Eq (α := Set Πʳ (i : ι), [R i, A i]_[𝓟 S])
    {f : Πʳ (i : ι), [R i, A i]_[𝓟 S] | ∀ (i : ι), p i → (↑f : (i : ι) → (fun (i : ι) ↦ R i) i) i ∈ A i}
    (DFunLike.coe (β := R) ⁻¹' (Sᶜ ∩ {i : ι | p i}).pi (α := R) A)
⊢ IsOpen[topologicalSpace R A (𝓟 S)]
    {f : Πʳ (i : ι), [R i, A i]_[𝓟 S] | ∀ (i : ι), p i → (↑f : (i : ι) → (fun (i : ι) ↦ R i) i) i ∈ A i}

Tactic:
convert!
    isOpen_set_pi (hS.inter_of_left {i | p i}) (fun i _ ↦ hAopen i) |>.preimage continuous_coe

Premises used: RestrictedProduct.continuous_coe, Set.Finite.inter_of_left, setOf, isOpen_set_pi, IsOpen.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)
S : Set ι
hS : Membership.mem (γ := Filter ι) cofinite S
p : ι → Prop
h :
  ∀ (f : Πʳ (i : ι), [R i, A i]_[𝓟 S]),
    Membership.mem (γ := Set Πʳ (i : ι), [R i, A i]_[𝓟 S])
        {f : Πʳ (i : ι), [R i, A i]_[𝓟 S] | ∀ (i : ι), p i → (↑f : (i : ι) → (fun (i : ι) ↦ R i) i) i ∈ A i} f ↔
      Membership.mem (γ := Set Πʳ (i : ι), [R i, A i]_[𝓟 S])
        (DFunLike.coe (β := R) ⁻¹' (Sᶜ ∩ {i : ι | p i}).pi (α := R) A) f
⊢ Eq (α := Set Πʳ (i : ι), [R i, A i]_[𝓟 S])
    {f : Πʳ (i : ι), [R i, A i]_[𝓟 S] | ∀ (i : ι), p i → (↑f : (i : ι) → (fun (i : ι) ↦ R i) i) i ∈ A i}
    (DFunLike.coe (β := R) ⁻¹' (Sᶜ ∩ {i : ι | p i}).pi (α := R) A)

Tactic:
ext f
-- 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 : Membership.mem (γ := Filter ι) cofinite S
p : ι → Prop
f : Πʳ (i : ι), [R i, A i]_[𝓟 S]
⊢ Membership.mem (γ := Set Πʳ (i : ι), [R i, A i]_[𝓟 S])
      {f : Πʳ (i : ι), [R i, A i]_[𝓟 S] | ∀ (i : ι), p i → (↑f : (i : ι) → (fun (i : ι) ↦ R i) i) i ∈ A i} f ↔
    Membership.mem (γ := Set Πʳ (i : ι), [R i, A i]_[𝓟 S])
      (DFunLike.coe (β := R) ⁻¹' (Sᶜ ∩ {i : ι | p i}).pi (α := R) A) f

Tactic:
⟨fun H i hi ↦ H i hi.2, fun H i hiT ↦ ?_⟩

Premises used: And.right, 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)
S : Set ι
hS : Membership.mem (γ := Filter ι) cofinite S
p : ι → Prop
f : Πʳ (i : ι), [R i, A i]_[𝓟 S]
h :
  ∀
    (H :
      Membership.mem (γ := Set Πʳ (i : ι), [R i, A i]_[𝓟 S])
        (DFunLike.coe (β := R) ⁻¹' (Sᶜ ∩ {i : ι | p i}).pi (α := R) A) f)
    (i : ι) (hiT : p i), (↑f : (i : ι) → (fun (i : ι) ↦ R i) i) i ∈ A i
⊢ Membership.mem (γ := Set Πʳ (i : ι), [R i, A i]_[𝓟 S])
      {f : Πʳ (i : ι), [R i, A i]_[𝓟 S] | ∀ (i : ι), p i → (↑f : (i : ι) → (fun (i : ι) ↦ R i) i) i ∈ A i} f ↔
    Membership.mem (γ := Set Πʳ (i : ι), [R i, A i]_[𝓟 S])
      (DFunLike.coe (β := R) ⁻¹' (Sᶜ ∩ {i : ι | p i}).pi (α := R) A) f

Tactic:
refine ⟨fun H i hi ↦ H i hi.2, fun H i hiT ↦ ?_⟩
-- 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 : Membership.mem (γ := Filter ι) cofinite S
p : ι → Prop
f : Πʳ (i : ι), [R i, A i]_[𝓟 S]
H :
  Membership.mem (γ := Set Πʳ (i : ι), [R i, A i]_[𝓟 S]) (DFunLike.coe (β := R) ⁻¹' (Sᶜ ∩ {i : ι | p i}).pi (α := R) A)
    f
i : ι
hiT : p i
pos : ∀ (hiS : i ∈ S), (↑f : (i : ι) → (fun (i : ι) ↦ R i) i) i ∈ A i
neg : ∀ (hiS : i ∉ S), (↑f : (i : ι) → (fun (i : ι) ↦ R i) i) i ∈ A i
⊢ (↑f : (i : ι) → (fun (i : ι) ↦ R i) i) i ∈ A i

Tactic:
by_cases hiS : i ∈ S
-- 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 : Membership.mem (γ := Filter ι) cofinite S
p : ι → Prop
f : Πʳ (i : ι), [R i, A i]_[𝓟 S]
H :
  Membership.mem (γ := Set Πʳ (i : ι), [R i, A i]_[𝓟 S]) (DFunLike.coe (β := R) ⁻¹' (Sᶜ ∩ {i : ι | p i}).pi (α := R) A)
    f
i : ι
hiT : p i
hiS : i ∈ S
⊢ (↑f : (i : ι) → (fun (i : ι) ↦ R i) i) i ∈ A i

Tactic:
f.2 hiS

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)
hAopen : ∀ (i : ι), IsOpen[inst i] (A i)
S : Set ι
hS : Membership.mem (γ := Filter ι) cofinite S
p : ι → Prop
f : Πʳ (i : ι), [R i, A i]_[𝓟 S]
H :
  Membership.mem (γ := Set Πʳ (i : ι), [R i, A i]_[𝓟 S]) (DFunLike.coe (β := R) ⁻¹' (Sᶜ ∩ {i : ι | p i}).pi (α := R) A)
    f
i : ι
hiT : p i
hiS : i ∈ S
⊢ (↑f : (i : ι) → (fun (i : ι) ↦ R i) i) i ∈ A i

Tactic:
exact f.2 hiS

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)
hAopen : ∀ (i : ι), IsOpen[inst i] (A i)
S : Set ι
hS : Membership.mem (γ := Filter ι) cofinite S
p : ι → Prop
f : Πʳ (i : ι), [R i, A i]_[𝓟 S]
H :
  Membership.mem (γ := Set Πʳ (i : ι), [R i, A i]_[𝓟 S]) (DFunLike.coe (β := R) ⁻¹' (Sᶜ ∩ {i : ι | p i}).pi (α := R) A)
    f
i : ι
hiT : p i
hiS : i ∉ S
⊢ (↑f : (i : ι) → (fun (i : ι) ↦ R i) i) i ∈ A i

Tactic:
H i ⟨hiS, hiT⟩

Premises used: Set.Mem, And.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)
S : Set ι
hS : Membership.mem (γ := Filter ι) cofinite S
p : ι → Prop
f : Πʳ (i : ι), [R i, A i]_[𝓟 S]
H :
  Membership.mem (γ := Set Πʳ (i : ι), [R i, A i]_[𝓟 S]) (DFunLike.coe (β := R) ⁻¹' (Sᶜ ∩ {i : ι | p i}).pi (α := R) A)
    f
i : ι
hiT : p i
hiS : i ∉ S
⊢ (↑f : (i : ι) → (fun (i : ι) ↦ R i) i) i ∈ A i

Tactic:
exact H i ⟨hiS, hiT⟩

Premises used: And.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)
S : Set ι
hS : cofinite ≤ 𝓟 S
⊢ IsOpen[topologicalSpace R A (𝓟 S)]
    {f : Πʳ (i : ι), [R i, A i]_[𝓟 S] | ∀ (i : ι), True → (↑f : (i : ι) → (fun (i : ι) ↦ R i) i) i ∈ A i}

Tactic:
isOpen_forall_imp_mem_of_principal hAopen hS (p := fun _ ↦ True)

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)
S : Set ι
hS : cofinite ≤ 𝓟 S
h :
  ∀ (x : Πʳ (i : ι), [R i, A i]_[𝓟 S]) (a : ι),
    (↑x : (i : ι) → (fun (i : ι) ↦ R i) i) a ∈ A a ↔ True → (↑x : (i : ι) → (fun (i : ι) ↦ R i) i) a ∈ A a
⊢ IsOpen[topologicalSpace R A (𝓟 S)]
    {f : Πʳ (i : ι), [R i, A i]_[𝓟 S] | ∀ (i : ι), (↑f : (i : ι) → (fun (i : ι) ↦ R i) i) i ∈ A i}

Tactic:
convert! isOpen_forall_imp_mem_of_principal hAopen hS (p := fun _ ↦ True)

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)
S : Set ι
hS : cofinite ≤ 𝓟 S
x : Πʳ (i : ι), [R i, A i]_[𝓟 S]
a : ι
⊢ (↑x : (i : ι) → (fun (i : ι) ↦ R i) i) a ∈ A a ↔ True → (↑x : (i : ι) → (fun (i : ι) ↦ R i) i) a ∈ A a

Tactic:
simp