-- Mathlib/Topology/Constructions.lean
theorem isOpen_pi_iff' [Finite ι] {s : Set (∀ a, π a)} :
    IsOpen s ↔
      ∀ f, f ∈ s → ∃ u : ∀ a, Set (π a), (∀ a, IsOpen (u a) ∧ f a ∈ u a) ∧ univ.pi u ⊆ s

Proof state:
case intro.refine_1.intro.intro.intro
ι : Type u_5
π : ι → Type u_6
T : (i : ι) → TopologicalSpace (π i)
inst✝ : Finite ι
s : Set ((a : ι) → π a)
val✝ : Fintype ι
a : (a : ι) → π a
x✝ : a ∈ s
I : Finset ι
t : (i : ι) → Set (π i)
h1 : ∀ (i : ι), ∃ t_1 ⊆ t i, IsOpen t_1 ∧ a i ∈ t_1
h2 : (↑I).pi t ⊆ s
⊢ ∃ u, (∀ (a_1 : ι), IsOpen (u a_1) ∧ a a_1 ∈ u a_1) ∧ univ.pi 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)⟩⟩

Result:
case intro.refine_1.intro.intro.intro
ι : Type u_5
π : ι → Type u_6
T : (i : ι) → TopologicalSpace (π i)
inst✝ : Finite ι
s : Set ((a : ι) → π a)
val✝ : Fintype ι
a : (a : ι) → π a
x✝ : a ∈ s
I : Finset ι
t : (i : ι) → Set (π i)
h1 : ∀ (i : ι), ∃ t_1 ⊆ t i, IsOpen t_1 ∧ a i ∈ t_1
h2 : (↑I).pi t ⊆ s
⊢ univ.pi t ⊆ (↑I).pi t

Proof state:
case intro.refine_1.intro.intro.intro
ι : Type u_5
π : ι → Type u_6
T : (i : ι) → TopologicalSpace (π i)
inst✝ : Finite ι
s : Set ((a : ι) → π a)
val✝ : Fintype ι
a : (a : ι) → π a
x✝ : a ∈ s
I : Finset ι
t : (i : ι) → Set (π i)
h1 : ∀ (i : ι), ∃ t_1 ⊆ t i, IsOpen t_1 ∧ a i ∈ t_1
h2 : (↑I).pi t ⊆ s
⊢ (↑I).pi t ∩ (↑I)ᶜ.pi t ⊆ (↑I).pi t

Tactic:
exact inter_subset_left

Result:
no goals

Proof state:
case intro
ι : Type u_5
π : ι → Type u_6
T : (i : ι) → TopologicalSpace (π i)
inst✝ : Finite ι
s : Set ((a : ι) → π a)
val✝ : Fintype ι
⊢ (∀ x ∈ s, ∃ I t, (∀ (i : ι), ∃ t_1 ⊆ t i, IsOpen t_1 ∧ x i ∈ t_1) ∧ (↑I).pi t ⊆ s) ↔
    ∀ f ∈ s, ∃ u, (∀ (a : ι), IsOpen (u a) ∧ f a ∈ u a) ∧ univ.pi u ⊆ s

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

Result:
case intro.refine_1
ι : Type u_5
π : ι → Type u_6
T : (i : ι) → TopologicalSpace (π i)
inst✝ : Finite ι
s : Set ((a : ι) → π a)
val✝ : Fintype ι
a : (a : ι) → π a
x✝ : a ∈ s
⊢ (∃ I t, (∀ (i : ι), ∃ t_1 ⊆ t i, IsOpen t_1 ∧ a i ∈ t_1) ∧ (↑I).pi t ⊆ s) →
    ∃ u, (∀ (a_2 : ι), IsOpen (u a_2) ∧ a a_2 ∈ u a_2) ∧ univ.pi u ⊆ s

case intro.refine_2
ι : Type u_5
π : ι → Type u_6
T : (i : ι) → TopologicalSpace (π i)
inst✝ : Finite ι
s : Set ((a : ι) → π a)
val✝ : Fintype ι
a : (a : ι) → π a
x✝ : a ∈ s
⊢ (∃ u, (∀ (a_1 : ι), IsOpen (u a_1) ∧ a a_1 ∈ u a_1) ∧ univ.pi u ⊆ s) →
    ∃ I t, (∀ (i : ι), ∃ t_1 ⊆ t i, IsOpen t_1 ∧ a i ∈ t_1) ∧ (↑I).pi t ⊆ s

Proof state:
case intro
ι : Type u_5
π : ι → Type u_6
T : (i : ι) → TopologicalSpace (π i)
inst✝ : Finite ι
s : Set ((a : ι) → π a)
val✝ : Fintype ι
⊢ (∀ x ∈ s, 𝓝 x ≤ 𝓟 s) ↔ ∀ f ∈ s, ∃ u, (∀ (a : ι), IsOpen (u a) ∧ f a ∈ u a) ∧ univ.pi u ⊆ s

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

Result:
case intro
ι : Type u_5
π : ι → Type u_6
T : (i : ι) → TopologicalSpace (π i)
inst✝ : Finite ι
s : Set ((a : ι) → π a)
val✝ : Fintype ι
⊢ (∀ x ∈ s, ∃ I t, (∀ (i : ι), ∃ t_1 ⊆ t i, IsOpen t_1 ∧ x i ∈ t_1) ∧ (↑I).pi t ⊆ s) ↔
    ∀ f ∈ s, ∃ u, (∀ (a : ι), IsOpen (u a) ∧ f a ∈ u a) ∧ univ.pi u ⊆ s

Proof state:
case intro.refine_1.intro.intro.intro
ι : Type u_5
π : ι → Type u_6
T : (i : ι) → TopologicalSpace (π i)
inst✝ : Finite ι
s : Set ((a : ι) → π a)
val✝ : Fintype ι
a : (a : ι) → π a
x✝ : a ∈ s
I : Finset ι
t : (i : ι) → Set (π i)
h1 : ∀ (i : ι), ∃ t_1 ⊆ t i, IsOpen t_1 ∧ a i ∈ t_1
h2 : (↑I).pi t ⊆ s
⊢ univ.pi t ⊆ (↑I).pi t

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

Result:
case intro.refine_1.intro.intro.intro
ι : Type u_5
π : ι → Type u_6
T : (i : ι) → TopologicalSpace (π i)
inst✝ : Finite ι
s : Set ((a : ι) → π a)
val✝ : Fintype ι
a : (a : ι) → π a
x✝ : a ∈ s
I : Finset ι
t : (i : ι) → Set (π i)
h1 : ∀ (i : ι), ∃ t_1 ⊆ t i, IsOpen t_1 ∧ a i ∈ t_1
h2 : (↑I).pi t ⊆ s
⊢ (↑I).pi t ∩ (↑I)ᶜ.pi t ⊆ (↑I).pi t

Proof state:
case intro.refine_2
ι : Type u_5
π : ι → Type u_6
T : (i : ι) → TopologicalSpace (π i)
inst✝ : Finite ι
s : Set ((a : ι) → π a)
val✝ : Fintype ι
a : (a : ι) → π a
x✝ : a ∈ s
⊢ (∃ u, (∀ (a_1 : ι), IsOpen (u a_1) ∧ a a_1 ∈ u a_1) ∧ univ.pi u ⊆ s) →
    ∃ I t, (∀ (i : ι), ∃ t_1 ⊆ t i, IsOpen t_1 ∧ a i ∈ t_1) ∧ (↑I).pi t ⊆ s

Tactic:
exact fun ⟨u, ⟨h1, _⟩⟩ =>
  ⟨Finset.univ, u, ⟨fun i => ⟨u i, ⟨rfl.subset, h1 i⟩⟩, by rwa [Finset.coe_univ]⟩⟩

Result:
no goals

Proof state:
ι : Type u_5
π : ι → Type u_6
T : (i : ι) → TopologicalSpace (π i)
inst✝ : Finite ι
s : Set ((a : ι) → π a)
val✝ : Fintype ι
a : (a : ι) → π a
x✝¹ : a ∈ s
x✝ : ∃ u, (∀ (a_1 : ι), IsOpen (u a_1) ∧ a a_1 ∈ u a_1) ∧ univ.pi u ⊆ s
u : (a : ι) → Set (π a)
h1 : ∀ (a_1 : ι), IsOpen (u a_1) ∧ a a_1 ∈ u a_1
right✝ : univ.pi u ⊆ s
⊢ (↑Finset.univ).pi u ⊆ s

Tactic:
rwa [Finset.coe_univ]

Result:
no goals

Proof state:
case intro.refine_1
ι : Type u_5
π : ι → Type u_6
T : (i : ι) → TopologicalSpace (π i)
inst✝ : Finite ι
s : Set ((a : ι) → π a)
val✝ : Fintype ι
a : (a : ι) → π a
x✝ : a ∈ s
⊢ (∃ I t, (∀ (i : ι), ∃ t_1 ⊆ t i, IsOpen t_1 ∧ a i ∈ t_1) ∧ (↑I).pi t ⊆ s) →
    ∃ u, (∀ (a_2 : ι), IsOpen (u a_2) ∧ a a_2 ∈ u a_2) ∧ univ.pi u ⊆ s

Tactic:
rintro ⟨I, t, ⟨h1, h2⟩⟩

Result:
case intro.refine_1.intro.intro.intro
ι : Type u_5
π : ι → Type u_6
T : (i : ι) → TopologicalSpace (π i)
inst✝ : Finite ι
s : Set ((a : ι) → π a)
val✝ : Fintype ι
a : (a : ι) → π a
x✝ : a ∈ s
I : Finset ι
t : (i : ι) → Set (π i)
h1 : ∀ (i : ι), ∃ t_1 ⊆ t i, IsOpen t_1 ∧ a i ∈ t_1
h2 : (↑I).pi t ⊆ s
⊢ ∃ u, (∀ (a_1 : ι), IsOpen (u a_1) ∧ a a_1 ∈ u a_1) ∧ univ.pi u ⊆ s

Proof state:
ι : Type u_5
π : ι → Type u_6
T : (i : ι) → TopologicalSpace (π i)
inst✝ : Finite ι
s : Set ((a : ι) → π a)
⊢ IsOpen s ↔ ∀ f ∈ s, ∃ u, (∀ (a : ι), IsOpen (u a) ∧ f a ∈ u a) ∧ univ.pi u ⊆ s

Tactic:
cases nonempty_fintype ι

Result:
case intro
ι : Type u_5
π : ι → Type u_6
T : (i : ι) → TopologicalSpace (π i)
inst✝ : Finite ι
s : Set ((a : ι) → π a)
val✝ : Fintype ι
⊢ IsOpen s ↔ ∀ f ∈ s, ∃ u, (∀ (a : ι), IsOpen (u a) ∧ f a ∈ u a) ∧ univ.pi u ⊆ s

Proof state:
case intro
ι : Type u_5
π : ι → Type u_6
T : (i : ι) → TopologicalSpace (π i)
inst✝ : Finite ι
s : Set ((a : ι) → π a)
val✝ : Fintype ι
⊢ IsOpen s ↔ ∀ f ∈ s, ∃ u, (∀ (a : ι), IsOpen (u a) ∧ f a ∈ u a) ∧ univ.pi u ⊆ s

Tactic:
rw [isOpen_iff_nhds]

Result:
case intro
ι : Type u_5
π : ι → Type u_6
T : (i : ι) → TopologicalSpace (π i)
inst✝ : Finite ι
s : Set ((a : ι) → π a)
val✝ : Fintype ι
⊢ (∀ x ∈ s, 𝓝 x ≤ 𝓟 s) ↔ ∀ f ∈ s, ∃ u, (∀ (a : ι), IsOpen (u a) ∧ f a ∈ u a) ∧ univ.pi u ⊆ s