awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
s : Set ((a : ι) → A a)
a : (a : ι) → A a
h : a ∈ s
I : Finset ι
t : (a : ι) → Set (A a)
h1 : ∀ a_1 ∈ I, IsOpen[T a_1] (t a_1) ∧ a a_1 ∈ t a_1
h2 : (↑I : Set ι).pi (α := A) t ⊆ s
i : ι
hi : i ∉ I
⊢ Subset.{u_6} (α := Set (A i)) univ univ ∧ IsOpen[T i] univ ∧ Membership.mem (γ := Set (A i)) univ (a i)

Tactic:
exact ⟨Subset.rfl, isOpen_univ, mem_univ _⟩
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
s : Set ((a : ι) → A a)
a : (a : ι) → A a
h : a ∈ s
I : Finset ι
t : (a : ι) → Set (A a)
h1 : ∀ a_1 ∈ I, IsOpen[T a_1] (t a_1) ∧ a a_1 ∈ t a_1
h2 : (↑I : Set ι).pi (α := A) t ⊆ s
refine_2 : (Set.pi (α := A) univ fun (i : ι) ↦ if i ∈ (↑I : Set ι) then if i ∈ I then t i else univ else univ) ⊆ s
⊢ ((↑I : Set ι).pi (α := A) fun (a : ι) ↦ if a ∈ I then t a else univ) ⊆ s

Tactic:
rw [← univ_pi_ite]

Premises used: Set.univ_pi_ite
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
s : Set ((a : ι) → A a)
a : (a : ι) → A a
h : a ∈ s
I : Finset ι
t : (a : ι) → Set (A a)
h1 : ∀ a_1 ∈ I, IsOpen[T a_1] (t a_1) ∧ a a_1 ∈ t a_1
h2 : (↑I : Set ι).pi (α := A) t ⊆ s
⊢ (Set.pi (α := A) univ fun (i : ι) ↦ if i ∈ (↑I : Set ι) then if i ∈ I then t i else univ else univ) ⊆ s

Tactic:
simp only [← ite_and, ← Finset.mem_coe, and_self_iff, univ_pi_ite, h2]

Premises used: Set.univ_pi_ite, and_self_iff, ite_and, Finset.mem_coe
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
s : Set ((a : ι) → A a)
a : (a : ι) → A a
h : a ∈ s
I : Finset ι
t : (a : ι) → Set (A a)
h1 : ∀ a_1 ∈ I, IsOpen[T a_1] (t a_1) ∧ a a_1 ∈ t a_1
h2 : (↑I : Set ι).pi (α := A) t ⊆ s
refine_2 : ∀ (i : ι), ∃ t_1 ⊆ (fun (a : ι) ↦ if a ∈ I then t a else univ) i, IsOpen[T i] t_1 ∧ a i ∈ t_1
refine_2₁ refine_2₂ : ((↑I : Set ι).pi (α := A) fun (a : ι) ↦ if a ∈ I then t a else univ) ⊆ s
⊢ ∃ (I : Finset ι) (t : (i : ι) → Set (A i)),
    (∀ (i : ι), ∃ t_1 ⊆ t i, IsOpen[T i] t_1 ∧ a i ∈ t_1) ∧ (↑I : Set ι).pi (α := A) t ⊆ s

Tactic:
classical
    refine ⟨I, fun a => ite (a ∈ I) (t a) univ, fun i => ?_, ?_⟩
    · by_cases hi : i ∈ I
      · use t i
        simp_rw [if_pos hi]
        exact ⟨Subset.rfl, (h1 i) hi⟩
      · use univ
        simp_rw [if_neg hi]
        exact ⟨Subset.rfl, isOpen_univ, mem_univ _⟩
    · rw [← univ_pi_ite]
      simp only [← ite_and, ← Finset.mem_coe, and_self_iff, univ_pi_ite, h2]

Premises used: Set.univ, Set.univ_pi_ite, and_self_iff, ite_and, Finset.mem_coe
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
inst : Finite ι
s : Set ((a : ι) → A a)
intro :
  ∀ (val : Fintype ι),
    IsOpen[Pi.topologicalSpace] s ↔
      ∀ f ∈ s, ∃ (u : (a : ι) → Set (A a)), (∀ (a : ι), IsOpen[T a] (u a) ∧ f a ∈ u a) ∧ Set.pi (α := A) univ u ⊆ s
⊢ IsOpen[Pi.topologicalSpace] s ↔
    ∀ f ∈ s, ∃ (u : (a : ι) → Set (A a)), (∀ (a : ι), IsOpen[T a] (u a) ∧ f a ∈ u a) ∧ Set.pi (α := A) univ u ⊆ s

Tactic:
cases nonempty_fintype ι

Premises used: nonempty_fintype
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
inst : Finite ι
s : Set ((a : ι) → A a)
val : Fintype ι
intro :
  (∀ x ∈ s, 𝓝 x ≤ 𝓟 s) ↔
    ∀ f ∈ s, ∃ (u : (a : ι) → Set (A a)), (∀ (a : ι), IsOpen[T a] (u a) ∧ f a ∈ u a) ∧ Set.pi (α := A) univ u ⊆ s
⊢ IsOpen[Pi.topologicalSpace] s ↔
    ∀ f ∈ s, ∃ (u : (a : ι) → Set (A a)), (∀ (a : ι), IsOpen[T a] (u a) ∧ f a ∈ u a) ∧ Set.pi (α := A) univ u ⊆ s

Tactic:
rw [isOpen_iff_nhds]

Premises used: isOpen_iff_nhds
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
inst : Finite ι
s : Set ((a : ι) → A a)
val : Fintype ι
intro :
  (∀ x ∈ s,
      ∃ (I : Finset ι) (t : (i : ι) → Set (A i)),
        (∀ (i : ι), ∃ t_1 ⊆ t i, IsOpen[T i] t_1 ∧ x i ∈ t_1) ∧ (↑I : Set ι).pi (α := A) t ⊆ s) ↔
    ∀ f ∈ s, ∃ (u : (a : ι) → Set (A a)), (∀ (a : ι), IsOpen[T a] (u a) ∧ f a ∈ u a) ∧ Set.pi (α := A) univ u ⊆ s
⊢ (∀ x ∈ s, 𝓝 x ≤ 𝓟 s) ↔
    ∀ f ∈ s, ∃ (u : (a : ι) → Set (A a)), (∀ (a : ι), IsOpen[T a] (u a) ∧ f a ∈ u a) ∧ Set.pi (α := A) univ u ⊆ s

Tactic:
simp_rw [le_principal_iff, nhds_pi, Filter.mem_pi', mem_nhds_iff]

Premises used: Filter.mem_pi', Filter.le_principal_iff, mem_nhds_iff, nhds_pi
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
inst : Finite ι
s : Set ((a : ι) → A a)
val : Fintype ι
⊢ (∀ x ∈ s,
      ∃ (I : Finset ι) (t : (i : ι) → Set (A i)),
        (∀ (i : ι), ∃ t_1 ⊆ t i, IsOpen[T i] t_1 ∧ x i ∈ t_1) ∧ (↑I : Set ι).pi (α := A) t ⊆ s) ↔
    ∀ f ∈ s, ∃ (u : (a : ι) → Set (A a)), (∀ (a : ι), IsOpen[T a] (u a) ∧ f a ∈ u a) ∧ Set.pi (α := A) univ u ⊆ s

Tactic:
forall₂_congr fun a _ => ⟨?_, ?_⟩

Premises used: forall₂_congr, Iff.intro
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
inst : Finite ι
s : Set ((a : ι) → A a)
val : Fintype ι
intro :
  ∀ a ∈ s,
    (∃ (I : Finset ι) (t : (i : ι) → Set (A i)),
        (∀ (i : ι), ∃ t_1 ⊆ t i, IsOpen[T i] t_1 ∧ a i ∈ t_1) ∧ (↑I : Set ι).pi (α := A) t ⊆ s) →
      ∃ (u : (a : ι) → Set (A a)), (∀ (a_2 : ι), IsOpen[T a_2] (u a_2) ∧ a a_2 ∈ u a_2) ∧ Set.pi (α := A) univ u ⊆ s
intro₁ :
  ∀ a ∈ s,
    (∃ (u : (a : ι) → Set (A a)), (∀ (a_1 : ι), IsOpen[T a_1] (u a_1) ∧ a a_1 ∈ u a_1) ∧ Set.pi (α := A) univ u ⊆ s) →
      ∃ (I : Finset ι) (t : (i : ι) → Set (A i)),
        (∀ (i : ι), ∃ t_1 ⊆ t i, IsOpen[T i] t_1 ∧ a i ∈ t_1) ∧ (↑I : Set ι).pi (α := A) t ⊆ s
⊢ (∀ x ∈ s,
      ∃ (I : Finset ι) (t : (i : ι) → Set (A i)),
        (∀ (i : ι), ∃ t_1 ⊆ t i, IsOpen[T i] t_1 ∧ x i ∈ t_1) ∧ (↑I : Set ι).pi (α := A) t ⊆ s) ↔
    ∀ f ∈ s, ∃ (u : (a : ι) → Set (A a)), (∀ (a : ι), IsOpen[T a] (u a) ∧ f a ∈ u a) ∧ Set.pi (α := A) univ u ⊆ s

Tactic:
refine forall₂_congr fun a _ => ⟨?_, ?_⟩

Premises used: forall₂_congr, Iff.intro
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
inst : Finite ι
s : Set ((a : ι) → A a)
val : Fintype ι
a : (a : ι) → A a
h : a ∈ s
I : Finset ι
t : (i : ι) → Set (A i)
h1 : ∀ (i : ι), ∃ t_1 ⊆ t i, IsOpen[T i] t_1 ∧ a i ∈ t_1
h2 : (↑I : Set ι).pi (α := A) t ⊆ s
⊢ ∃ (u : (a : ι) → Set (A a)), (∀ (a_1 : ι), IsOpen[T a_1] (u a_1) ∧ a a_1 ∈ u a_1) ∧ Set.pi (α := A) univ u ⊆ s

Tactic:
⟨fun i => (h1 i).choose,
        ⟨fun i => (h1 i).choose_spec.2,
          (pi_mono fun i _ => (h1 i).choose_spec.1).trans (Subset.trans ?_ h2)⟩⟩

Premises used: Exists.choose_spec, Set.Subset.trans, HasSubset.Subset.trans, And.right, And.left, And.intro, Exists.intro, Exists.choose, Set.pi_mono
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
inst : Finite ι
s : Set ((a : ι) → A a)
val : Fintype ι
a : (a : ι) → A a
h : a ∈ s
I : Finset ι
t : (i : ι) → Set (A i)
h1 : ∀ (i : ι), ∃ t_1 ⊆ t i, IsOpen[T i] t_1 ∧ a i ∈ t_1
h2 : (↑I : Set ι).pi (α := A) t ⊆ s
intro : Set.pi (α := A) univ t ⊆ (↑I : Set ι).pi (α := A) t
⊢ ∃ (u : (a : ι) → Set (A a)), (∀ (a_1 : ι), IsOpen[T a_1] (u a_1) ∧ a a_1 ∈ u a_1) ∧ Set.pi (α := A) univ u ⊆ s

Tactic:
refine
      ⟨fun i => (h1 i).choose,
        ⟨fun i => (h1 i).choose_spec.2,
          (pi_mono fun i _ => (h1 i).choose_spec.1).trans (Subset.trans ?_ h2)⟩⟩
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
inst : Finite ι
s : Set ((a : ι) → A a)
val : Fintype ι
a : (a : ι) → A a
h : a ∈ s
I : Finset ι
t : (i : ι) → Set (A i)
h1 : ∀ (i : ι), ∃ t_1 ⊆ t i, IsOpen[T i] t_1 ∧ a i ∈ t_1
h2 : (↑I : Set ι).pi (α := A) t ⊆ s
intro : (↑I : Set ι).pi (α := A) t ∩ (↑I : Set ι)ᶜ.pi (α := A) t ⊆ (↑I : Set ι).pi (α := A) t
⊢ Set.pi (α := A) univ t ⊆ (↑I : Set ι).pi (α := A) t

Tactic:
rw [← pi_inter_compl (I : Set ι)]

Premises used: SetLike.coe, Set.pi_inter_compl
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
inst : Finite ι
s : Set ((a : ι) → A a)
val : Fintype ι
a : (a : ι) → A a
h : a ∈ s
I : Finset ι
t : (i : ι) → Set (A i)
h1 : ∀ (i : ι), ∃ t_1 ⊆ t i, IsOpen[T i] t_1 ∧ a i ∈ t_1
h2 : (↑I : Set ι).pi (α := A) t ⊆ s
⊢ (↑I : Set ι).pi (α := A) t ∩ (↑I : Set ι)ᶜ.pi (α := A) t ⊆ (↑I : Set ι).pi (α := A) t

Tactic:
inter_subset_left

Premises used: Set.inter_subset_left
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
inst : Finite ι
s : Set ((a : ι) → A a)
val : Fintype ι
a : (a : ι) → A a
h : a ∈ s
I : Finset ι
t : (i : ι) → Set (A i)
h1 : ∀ (i : ι), ∃ t_1 ⊆ t i, IsOpen[T i] t_1 ∧ a i ∈ t_1
h2 : (↑I : Set ι).pi (α := A) t ⊆ s
⊢ (↑I : Set ι).pi (α := A) t ∩ (↑I : Set ι)ᶜ.pi (α := A) t ⊆ (↑I : Set ι).pi (α := A) t

Tactic:
exact inter_subset_left

Premises used: Set.inter_subset_left
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
inst : Finite ι
s : Set ((a : ι) → A a)
val : Fintype ι
a : (a : ι) → A a
h : a ∈ s
h_1 : ∃ (u : (a : ι) → Set (A a)), (∀ (a_1 : ι), IsOpen[T a_1] (u a_1) ∧ a a_1 ∈ u a_1) ∧ Set.pi (α := A) univ u ⊆ s
u : (a : ι) → Set (A a)
h1 : ∀ (a_1 : ι), IsOpen[T a_1] (u a_1) ∧ a a_1 ∈ u a_1
right rwa rwa₁ rwa₂ rwa₃ : Set.pi (α := A) univ u ⊆ s
⊢ (↑Finset.univ : Set ι).pi (α := A) u ⊆ s

Tactic:
rwa [Finset.coe_univ]

Premises used: Finset.coe_univ
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
inst : Finite ι
s : Set ((a : ι) → A a)
val : Fintype ι
a : (a : ι) → A a
h : a ∈ s
⊢ (∃ (u : (a : ι) → Set (A a)), (∀ (a_1 : ι), IsOpen[T a_1] (u a_1) ∧ a a_1 ∈ u a_1) ∧ Set.pi (α := A) univ u ⊆ s) →
    ∃ (I : Finset ι) (t : (i : ι) → Set (A i)),
      (∀ (i : ι), ∃ t_1 ⊆ t i, IsOpen[T i] t_1 ∧ a i ∈ t_1) ∧ (↑I : Set ι).pi (α := A) t ⊆ s

Tactic:
exact fun ⟨u, ⟨h1, _⟩⟩ =>
      ⟨Finset.univ, u, ⟨fun i => ⟨u i, ⟨rfl.subset, h1 i⟩⟩, by rwa [Finset.coe_univ]⟩⟩
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
i : Set ι
s : (a : ι) → Set (A a)
hs : ∀ a ∈ i, IsClosed[T a] (s a)
rw : IsClosed[Pi.topologicalSpace] (⋂ a ∈ i, eval (β := A) a ⁻¹' s a)
⊢ IsClosed[Pi.topologicalSpace] (i.pi (α := A) s)

Tactic:
rw [pi_def]

Premises used: Set.pi_def
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
i : Set ι
s : (a : ι) → Set (A a)
hs : ∀ a ∈ i, IsClosed[T a] (s a)
⊢ IsClosed[Pi.topologicalSpace] (⋂ a ∈ i, eval (β := A) a ⁻¹' s a)

Tactic:
isClosed_biInter fun a ha => (hs _ ha).preimage (continuous_apply _)

Premises used: isClosed_biInter, continuous_apply, IsClosed.preimage
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
i : Set ι
s : (a : ι) → Set (A a)
hs : ∀ a ∈ i, IsClosed[T a] (s a)
⊢ IsClosed[Pi.topologicalSpace] (⋂ a ∈ i, eval (β := A) a ⁻¹' s a)

Tactic:
exact isClosed_biInter fun a ha => (hs _ ha).preimage (continuous_apply _)

Premises used: isClosed_biInter, continuous_apply, IsClosed.preimage
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
A : ι → Type u_6
B : ι → Type u_7
T : (i : ι) → TopologicalSpace (A i)
inst : (i : ι) → TopologicalSpace (B i)
f : (i : ι) → A i → B i
hf : ∀ (i : ι), IsClosedEmbedding (f i)
⊢ IsClosed[Pi.topologicalSpace] (range (Pi.map (α := A) (β := B) f))

Tactic:
simpa using isClosed_set_pi fun i _ ↦ (hf i).2

Premises used: isClosed_set_pi, Topology.IsClosedEmbedding.isClosed_range
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
A : ι → Type u_6
B : ι → Type u_7
T : (i : ι) → TopologicalSpace (A i)
inst : (i : ι) → TopologicalSpace (B i)
inst_1 : Finite ι
f : (i : ι) → A i → B i
hf : ∀ (i : ι), IsOpenEmbedding (f i)
⊢ IsOpen[Pi.topologicalSpace] (range (Pi.map (α := A) (β := B) f))

Tactic:
simpa using isOpen_set_pi Set.finite_univ fun i _ ↦ (hf i).2

Premises used: Topology.IsOpenEmbedding.isOpen_range, isOpen_set_pi, Set.finite_univ
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
I : Set ι
s : (i : ι) → Set (A i)
a : (i : ι) → A i
hs : I.pi (α := A) s ∈ 𝓝 a
i : ι
hi : i ∈ I
rw :
  ∀ (hs : Membership.mem (γ := Filter ((i : ι) → A i)) (Filter.pi (α := A) fun (i : ι) ↦ 𝓝 (a i)) (I.pi (α := A) s))
    {i : ι} (hi : i ∈ I), s i ∈ 𝓝 (a i)
⊢ s i ∈ 𝓝 (a i)

Tactic:
rw [nhds_pi] at hs

Premises used: nhds_pi
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
I : Set ι
s : (i : ι) → Set (A i)
a : (i : ι) → A i
hs : Membership.mem (γ := Filter ((i : ι) → A i)) (Filter.pi (α := A) fun (i : ι) ↦ 𝓝 (a i)) (I.pi (α := A) s)
i : ι
hi : i ∈ I
⊢ s i ∈ 𝓝 (a i)

Tactic:
mem_of_pi_mem_pi hs hi

Premises used: Filter.mem_of_pi_mem_pi
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
I : Set ι
s : (i : ι) → Set (A i)
a : (i : ι) → A i
hs : Membership.mem (γ := Filter ((i : ι) → A i)) (Filter.pi (α := A) fun (i : ι) ↦ 𝓝 (a i)) (I.pi (α := A) s)
i : ι
hi : i ∈ I
⊢ s i ∈ 𝓝 (a i)

Tactic:
exact mem_of_pi_mem_pi hs hi

Premises used: Filter.mem_of_pi_mem_pi
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
i : Set ι
s : (a : ι) → Set (A a)
x : (a : ι) → A a
hi : i.Finite
hs : ∀ a ∈ i, s a ∈ 𝓝 (x a)
rw : ∀ i_1 ∈ i, eval (β := A) i_1 ⁻¹' s i_1 ∈ 𝓝 x
⊢ i.pi (α := A) s ∈ 𝓝 x

Tactic:
rw [pi_def, biInter_mem hi]

Premises used: Filter.biInter_mem, Set.pi_def
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
i : Set ι
s : (a : ι) → Set (A a)
x : (a : ι) → A a
hi : i.Finite
hs : ∀ a ∈ i, s a ∈ 𝓝 (x a)
⊢ ∀ i_1 ∈ i, eval (β := A) i_1 ⁻¹' s i_1 ∈ 𝓝 x

Tactic:
fun a ha => (continuous_apply a).continuousAt (hs a ha)

Premises used: Set.Mem, setOf, Continuous.continuousAt, Set.preimage, continuous_apply
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
i : Set ι
s : (a : ι) → Set (A a)
x : (a : ι) → A a
hi : i.Finite
hs : ∀ a ∈ i, s a ∈ 𝓝 (x a)
⊢ ∀ i_1 ∈ i, eval (β := A) i_1 ⁻¹' s i_1 ∈ 𝓝 x

Tactic:
exact fun a ha => (continuous_apply a).continuousAt (hs a ha)

Premises used: Continuous.continuousAt, continuous_apply
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
I : Set ι
hI : I.Finite
s : (i : ι) → Set (A i)
a : (i : ι) → A i
rw :
  Membership.mem (γ := Filter ((i : ι) → A i)) (Filter.pi (α := A) fun (i : ι) ↦ 𝓝 (a i)) (I.pi (α := A) s) ↔
    ∀ i ∈ I, s i ∈ 𝓝 (a i)
rw₁ rw₂ : (∀ i ∈ I, s i ∈ 𝓝 (a i)) ↔ ∀ i ∈ I, s i ∈ 𝓝 (a i)
⊢ I.pi (α := A) s ∈ 𝓝 a ↔ ∀ i ∈ I, s i ∈ 𝓝 (a i)

Tactic:
rw [nhds_pi, pi_mem_pi_iff hI]

Premises used: Filter.pi_mem_pi_iff, nhds_pi
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
I : Set ι
hI : I.Finite
s : (i : ι) → Set (A i)
h :
  ∀ (a : (i : ι) → A i),
    a ∈ interior (I.pi (α := A) s) ↔
      Membership.mem (γ := Set ((i : ι) → A i)) (I.pi (α := A) fun (i : ι) ↦ interior (s i)) a
⊢ interior (I.pi (α := A) s) = I.pi (α := A) fun (i : ι) ↦ interior (s i)

Tactic:
ext a
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
I : Set ι
hI : I.Finite
s : (i : ι) → Set (A i)
a : (i : ι) → A i
⊢ a ∈ interior (I.pi (α := A) s) ↔
    Membership.mem (γ := Set ((i : ι) → A i)) (I.pi (α := A) fun (i : ι) ↦ interior (s i)) a

Tactic:
simp only [Set.mem_pi, mem_interior_iff_mem_nhds, set_pi_mem_nhds_iff hI]

Premises used: mem_interior_iff_mem_nhds, Set.mem_pi, set_pi_mem_nhds_iff
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
inst : DecidableEq ι
s : Set ((a : ι) → A a)
x : (a : ι) → A a
hs : s ∈ 𝓝 x
y : (a : ι) → A a
⊢ ∃ (I : Finset ι) (t : (i : ι) → Set (A i)), (∀ (i : ι), t i ∈ 𝓝 (x i)) ∧ (↑I : Set ι).pi (α := A) t ⊆ s

Tactic:
simp only [nhds_pi, Filter.mem_pi'] at hs

Premises used: Filter.mem_pi', nhds_pi
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
inst : DecidableEq ι
s : Set ((a : ι) → A a)
x y : (a : ι) → A a
hs : ∃ (I : Finset ι) (t : (i : ι) → Set (A i)), (∀ (i : ι), t i ∈ 𝓝 (x i)) ∧ (↑I : Set ι).pi (α := A) t ⊆ s
rcases :
  ∀ (I : Finset ι) (t : (i : ι) → Set (A i)) (htx : ∀ (i : ι), t i ∈ 𝓝 (x i)) (hts : (↑I : Set ι).pi (α := A) t ⊆ s),
    ∃ (I : Finset ι), I.piecewise (π := A) x y ∈ s
⊢ ∃ (I : Finset ι), I.piecewise (π := A) x y ∈ s

Tactic:
rcases hs with ⟨I, t, htx, hts⟩
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
inst : DecidableEq ι
s : Set ((a : ι) → A a)
x y : (a : ι) → A a
I : Finset ι
t : (i : ι) → Set (A i)
htx : ∀ (i : ι), t i ∈ 𝓝 (x i)
hts : (↑I : Set ι).pi (α := A) t ⊆ s
⊢ ∃ (I : Finset ι), I.piecewise (π := A) x y ∈ s

Tactic:
⟨I, hts fun i hi => ?_⟩

Premises used: Exists.intro
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
inst : DecidableEq ι
s : Set ((a : ι) → A a)
x y : (a : ι) → A a
I : Finset ι
t : (i : ι) → Set (A i)
htx : ∀ (i : ι), t i ∈ 𝓝 (x i)
hts : (↑I : Set ι).pi (α := A) t ⊆ s
refine : ∀ (i : ι) (hi : i ∈ (↑I : Set ι)), I.piecewise (π := A) x y i ∈ t i
⊢ ∃ (I : Finset ι), I.piecewise (π := A) x y ∈ s

Tactic:
refine ⟨I, hts fun i hi => ?_⟩
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
inst : DecidableEq ι
s : Set ((a : ι) → A a)
x y : (a : ι) → A a
I : Finset ι
t : (i : ι) → Set (A i)
htx : ∀ (i : ι), t i ∈ 𝓝 (x i)
hts : (↑I : Set ι).pi (α := A) t ⊆ s
i : ι
hi : i ∈ (↑I : Set ι)
⊢ I.piecewise (π := A) x y i ∈ t i

Tactic:
simpa [Finset.mem_coe.1 hi] using mem_of_mem_nhds (htx i)

Premises used: mem_of_mem_nhds, Iff.mp, Finset.mem_coe
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
A : ι → Type u_9
g : (a : ι) → Set (Set (A a))
⊢ Eq (α := TopologicalSpace ((i : ι) → A i)) (Pi.topologicalSpace (Y := A))
    (generateFrom
      {t : Set ((i : ι) → A i) |
        ∃ (s : (a : ι) → Set (A a)) (i : Finset ι), (∀ a ∈ i, s a ∈ g a) ∧ t = (↑i : Set ι).pi (α := A) s})

Tactic:
le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
A : ι → Type u_9
g : (a : ι) → Set (Set (A a))
refine_1 :
  LE.le (α := TopologicalSpace ((i : ι) → A i)) (Pi.topologicalSpace (Y := A))
    (generateFrom
      {t : Set ((i : ι) → A i) |
        ∃ (s : (a : ι) → Set (A a)) (i : Finset ι), (∀ a ∈ i, s a ∈ g a) ∧ t = (↑i : Set ι).pi (α := A) s})
refine_2 :
  LE.le (α := TopologicalSpace ((i : ι) → A i))
    (generateFrom
      {t : Set ((i : ι) → A i) |
        ∃ (s : (a : ι) → Set (A a)) (i : Finset ι), (∀ a ∈ i, s a ∈ g a) ∧ t = (↑i : Set ι).pi (α := A) s})
    (Pi.topologicalSpace (Y := A))
⊢ Eq (α := TopologicalSpace ((i : ι) → A i)) (Pi.topologicalSpace (Y := A))
    (generateFrom
      {t : Set ((i : ι) → A i) |
        ∃ (s : (a : ι) → Set (A a)) (i : Finset ι), (∀ a ∈ i, s a ∈ g a) ∧ t = (↑i : Set ι).pi (α := A) s})

Tactic:
refine le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
A : ι → Type u_9
g : (a : ι) → Set (Set (A a))
refine_1 :
  ∀ (s : Set ((i : ι) → A i)),
    Membership.mem (γ := Set (Set ((i : ι) → A i)))
        {t : Set ((i : ι) → A i) |
          ∃ (s : (a : ι) → Set (A a)) (i : Finset ι), (∀ a ∈ i, s a ∈ g a) ∧ t = (↑i : Set ι).pi (α := A) s}
        s →
      IsOpen[Pi.topologicalSpace] s
⊢ LE.le (α := TopologicalSpace ((i : ι) → A i)) (Pi.topologicalSpace (Y := A))
    (generateFrom
      {t : Set ((i : ι) → A i) |
        ∃ (s : (a : ι) → Set (A a)) (i : Finset ι), (∀ a ∈ i, s a ∈ g a) ∧ t = (↑i : Set ι).pi (α := A) s})

Tactic:
apply le_generateFrom

Premises used: le_generateFrom
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
A : ι → Type u_9
g : (a : ι) → Set (Set (A a))
s : (a : ι) → Set (A a)
i : Finset ι
hi : ∀ a ∈ i, s a ∈ g a
this : (a : ι) → TopologicalSpace (A a) := fun (a : ι) ↦ generateFrom (g a)
⊢ IsOpen[Pi.topologicalSpace] ((↑i : Set ι).pi (α := A) s)

Tactic:
isOpen_set_pi i.finite_toSet (fun a ha => GenerateOpen.basic _ (hi a ha))

Premises used: TopologicalSpace.GenerateOpen.basic, isOpen_set_pi, Finset.finite_toSet
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
A : ι → Type u_9
g : (a : ι) → Set (Set (A a))
s : (a : ι) → Set (A a)
i : Finset ι
hi : ∀ a ∈ i, s a ∈ g a
this : (a : ι) → TopologicalSpace (A a) := fun (a : ι) ↦ generateFrom (g a)
⊢ IsOpen[Pi.topologicalSpace] ((↑i : Set ι).pi (α := A) s)

Tactic:
exact isOpen_set_pi i.finite_toSet (fun a ha => GenerateOpen.basic _ (hi a ha))
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
A : ι → Type u_9
g : (a : ι) → Set (Set (A a))
⊢ LE.le (α := TopologicalSpace ((i : ι) → A i))
    (generateFrom
      {t : Set ((i : ι) → A i) |
        ∃ (s : (a : ι) → Set (A a)) (i : Finset ι), (∀ a ∈ i, s a ∈ g a) ∧ t = (↑i : Set ι).pi (α := A) s})
    (Pi.topologicalSpace (Y := A))

Tactic:
le_iInf fun i => coinduced_le_iff_le_induced.1 <| le_generateFrom fun s hs => ?_

Premises used: le_iInf, coinduced_le_iff_le_induced, Iff.mp, le_generateFrom
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
A : ι → Type u_9
g : (a : ι) → Set (Set (A a))
refine_2 :
  ∀ (i : ι) (s : Set (A i)) (hs : s ∈ g i),
    IsOpen[coinduced (fun (f : (i : ι) → A i) ↦ f i)
          (generateFrom
            {t : Set ((i : ι) → A i) |
              ∃ (s : (a : ι) → Set (A a)) (i : Finset ι), (∀ a ∈ i, s a ∈ g a) ∧ t = (↑i : Set ι).pi s})]
      s
⊢ LE.le (α := TopologicalSpace ((i : ι) → A i))
    (generateFrom
      {t : Set ((i : ι) → A i) |
        ∃ (s : (a : ι) → Set (A a)) (i : Finset ι), (∀ a ∈ i, s a ∈ g a) ∧ t = (↑i : Set ι).pi (α := A) s})
    (Pi.topologicalSpace (Y := A))

Tactic:
refine le_iInf fun i => coinduced_le_iff_le_induced.1 <| le_generateFrom fun s hs => ?_

Premises used: le_iInf, coinduced_le_iff_le_induced, Iff.mp, le_generateFrom
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
A : ι → Type u_9
g : (a : ι) → Set (Set (A a))
i : ι
s : Set (A i)
hs : s ∈ g i
⊢ IsOpen[coinduced (fun (f : (i : ι) → A i) ↦ f i)
        (generateFrom
          {t : Set ((i : ι) → A i) |
            ∃ (s : (a : ι) → Set (A a)) (i : Finset ι), (∀ a ∈ i, s a ∈ g a) ∧ t = (↑i : Set ι).pi s})]
    s

Tactic:
GenerateOpen.basic _ ⟨update (fun i => univ) i s, {i}, ?_⟩

Premises used: Function.update, Set.univ, TopologicalSpace.GenerateOpen.basic, Exists.intro, IsOpen, Singleton.singleton
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
A : ι → Type u_9
g : (a : ι) → Set (Set (A a))
i : ι
s : Set (A i)
hs : s ∈ g i
refine_2 :
  (∀ (a : ι),
      Membership.mem (γ := Finset ι) {i} a →
        Membership.mem (α := Set (A a)) (g a)
          (update (β := fun (a : ι) ↦ Set (A a)) (fun (i : ι) ↦ univ) i s a : Set (A a))) ∧
    Eq (α := Set ((i : ι) → A i)) ((fun (f : (i : ι) → A i) ↦ f i) ⁻¹' s)
      ((↑{i} : Set ι).pi (α := A) (update (β := fun (a : ι) ↦ Set (A a)) (fun (i : ι) ↦ univ) i s))
⊢ IsOpen[coinduced (fun (f : (i : ι) → A i) ↦ f i)
        (generateFrom
          {t : Set ((i : ι) → A i) |
            ∃ (s : (a : ι) → Set (A a)) (i : Finset ι), (∀ a ∈ i, s a ∈ g a) ∧ t = (↑i : Set ι).pi s})]
    s

Tactic:
refine GenerateOpen.basic _ ⟨update (fun i => univ) i s, {i}, ?_⟩
-- Module: Mathlib.Topology.Constructions
Goal:
ι : Type u_5
A : ι → Type u_9
g : (a : ι) → Set (Set (A a))
i : ι
s : Set (A i)
hs : s ∈ g i
⊢ (∀ (a : ι),
      Membership.mem (γ := Finset ι) {i} a →
        Membership.mem (α := Set (A a)) (g a)
          (update (β := fun (a : ι) ↦ Set (A a)) (fun (i : ι) ↦ univ) i s a : Set (A a))) ∧
    Eq (α := Set ((i : ι) → A i)) ((fun (f : (i : ι) → A i) ↦ f i) ⁻¹' s)
      ((↑{i} : Set ι).pi (α := A) (update (β := fun (a : ι) ↦ Set (A a)) (fun (i : ι) ↦ univ) i s))

Tactic:
simp [hs]