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

Proof state:
case refine_1.intro.intro.intro.refine_1
ι : Type u_5
π : ι → Type u_6
T : (i : ι) → TopologicalSpace (π i)
s : Set ((a : ι) → π a)
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 : ι
hi : i ∈ I
⊢ IsOpen ⋯.choose ∧ a i ∈ ⋯.choose

Tactic:
exact (h1 i).choose_spec.2

Result:
no goals

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

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

Result:
case refine_1.intro.intro.intro
ι : Type u_5
π : ι → Type u_6
T : (i : ι) → TopologicalSpace (π i)
s : Set ((a : ι) → π a)
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 u, (∀ a_1 ∈ I, IsOpen (u a_1) ∧ a a_1 ∈ u a_1) ∧ (↑I).pi u ⊆ s

Proof state:
case h
ι : Type u_5
π : ι → Type u_6
T : (i : ι) → TopologicalSpace (π i)
s : Set ((a : ι) → π a)
a : (a : ι) → π a
x✝ : a ∈ s
I : Finset ι
t : (a : ι) → Set (π a)
h1 : ∀ a_1 ∈ I, IsOpen (t a_1) ∧ a a_1 ∈ t a_1
h2 : (↑I).pi t ⊆ s
i : ι
hi : i ∈ I
⊢ t i ⊆ t i ∧ IsOpen (t i) ∧ a i ∈ t i

Tactic:
exact ⟨Subset.rfl, (h1 i) hi⟩

Result:
no goals

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

Tactic:
refine ⟨I, fun a => ite (a ∈ I) (t a) univ, fun i => ?_, ?_⟩

Result:
case refine_2.intro.intro.intro.refine_1
ι : Type u_5
π : ι → Type u_6
T : (i : ι) → TopologicalSpace (π i)
s : Set ((a : ι) → π a)
a : (a : ι) → π a
x✝ : a ∈ s
I : Finset ι
t : (a : ι) → Set (π a)
h1 : ∀ a_1 ∈ I, IsOpen (t a_1) ∧ a a_1 ∈ t a_1
h2 : (↑I).pi t ⊆ s
i : ι
⊢ ∃ t_1 ⊆ (fun a => if a ∈ I then t a else univ) i, IsOpen t_1 ∧ a i ∈ t_1

case refine_2.intro.intro.intro.refine_2
ι : Type u_5
π : ι → Type u_6
T : (i : ι) → TopologicalSpace (π i)
s : Set ((a : ι) → π a)
a : (a : ι) → π a
x✝ : a ∈ s
I : Finset ι
t : (a : ι) → Set (π a)
h1 : ∀ a_1 ∈ I, IsOpen (t a_1) ∧ a a_1 ∈ t a_1
h2 : (↑I).pi t ⊆ s
⊢ ((↑I).pi fun a => if a ∈ I then t a else univ) ⊆ s

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

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

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

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

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

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

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

Proof state:
case refine_1.intro.intro.intro
ι : Type u_5
π : ι → Type u_6
T : (i : ι) → TopologicalSpace (π i)
s : Set ((a : ι) → π a)
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 u, (∀ a_1 ∈ I, IsOpen (u a_1) ∧ a a_1 ∈ u a_1) ∧ (↑I).pi u ⊆ s

Tactic:
refine ⟨I, fun a => eval a '' (I : Set ι).pi fun a => (h1 a).choose, fun i hi => ?_, ?_⟩

Result:
case refine_1.intro.intro.intro.refine_1
ι : Type u_5
π : ι → Type u_6
T : (i : ι) → TopologicalSpace (π i)
s : Set ((a : ι) → π a)
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 : ι
hi : i ∈ I
⊢ IsOpen ((fun a_1 => eval a_1 '' (↑I).pi fun a_2 => ⋯.choose) i) ∧
    a i ∈ (fun a_1 => eval a_1 '' (↑I).pi fun a_2 => ⋯.choose) i

case refine_1.intro.intro.intro.refine_2
ι : Type u_5
π : ι → Type u_6
T : (i : ι) → TopologicalSpace (π i)
s : Set ((a : ι) → π a)
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 fun a_1 => eval a_1 '' (↑I).pi fun a_2 => ⋯.choose) ⊆ s

Proof state:
case h
ι : Type u_5
π : ι → Type u_6
T : (i : ι) → TopologicalSpace (π i)
s : Set ((a : ι) → π a)
a : (a : ι) → π a
x✝ : a ∈ s
I : Finset ι
t : (a : ι) → Set (π a)
h1 : ∀ a_1 ∈ I, IsOpen (t a_1) ∧ a a_1 ∈ t a_1
h2 : (↑I).pi t ⊆ s
i : ι
hi : i ∈ I
⊢ t i ⊆ (fun a => if a ∈ I then t a else univ) i ∧ IsOpen (t i) ∧ a i ∈ t i

Tactic:
simp_rw [if_pos hi]

Result:
case h
ι : Type u_5
π : ι → Type u_6
T : (i : ι) → TopologicalSpace (π i)
s : Set ((a : ι) → π a)
a : (a : ι) → π a
x✝ : a ∈ s
I : Finset ι
t : (a : ι) → Set (π a)
h1 : ∀ a_1 ∈ I, IsOpen (t a_1) ∧ a a_1 ∈ t a_1
h2 : (↑I).pi t ⊆ s
i : ι
hi : i ∈ I
⊢ t i ⊆ t i ∧ IsOpen (t i) ∧ a i ∈ t i

Proof state:
ι : Type u_5
π : ι → Type u_6
T : (i : ι) → TopologicalSpace (π i)
s : Set ((a : ι) → π a)
⊢ (∀ x ∈ s, 𝓝 x ≤ 𝓟 s) ↔ ∀ f ∈ s, ∃ I u, (∀ a ∈ I, IsOpen (u a) ∧ f a ∈ u a) ∧ (↑I).pi u ⊆ s

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

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

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

Tactic:
rw [isOpen_iff_nhds]

Result:
ι : Type u_5
π : ι → Type u_6
T : (i : ι) → TopologicalSpace (π i)
s : Set ((a : ι) → π a)
⊢ (∀ x ∈ s, 𝓝 x ≤ 𝓟 s) ↔ ∀ f ∈ s, ∃ I u, (∀ a ∈ I, IsOpen (u a) ∧ f a ∈ u a) ∧ (↑I).pi u ⊆ s

Proof state:
case refine_2.intro.intro.intro.refine_2
ι : Type u_5
π : ι → Type u_6
T : (i : ι) → TopologicalSpace (π i)
s : Set ((a : ι) → π a)
a : (a : ι) → π a
x✝ : a ∈ s
I : Finset ι
t : (a : ι) → Set (π a)
h1 : ∀ a_1 ∈ I, IsOpen (t a_1) ∧ a a_1 ∈ t a_1
h2 : (↑I).pi t ⊆ s
⊢ ((↑I).pi fun a => if a ∈ I then t a else univ) ⊆ s

Tactic:
rw [← univ_pi_ite]

Result:
case refine_2.intro.intro.intro.refine_2
ι : Type u_5
π : ι → Type u_6
T : (i : ι) → TopologicalSpace (π i)
s : Set ((a : ι) → π a)
a : (a : ι) → π a
x✝ : a ∈ s
I : Finset ι
t : (a : ι) → Set (π a)
h1 : ∀ a_1 ∈ I, IsOpen (t a_1) ∧ a a_1 ∈ t a_1
h2 : (↑I).pi t ⊆ s
⊢ (univ.pi fun i => if i ∈ ↑I then if i ∈ I then t i else univ else univ) ⊆ s