-- 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 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
⊢ univ ⊆ (fun a => if a ∈ I then t a else univ) i ∧ IsOpen univ ∧ a i ∈ univ

Tactic:
simp_rw [if_neg 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
⊢ univ ⊆ univ ∧ IsOpen univ ∧ a i ∈ univ

Proof state:
case pos
ι : 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_1 ⊆ (fun a => if a ∈ I then t a else univ) i, IsOpen t_1 ∧ a i ∈ t_1

Tactic:
use t i

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 ⊆ (fun a => if a ∈ I then t a else univ) i ∧ IsOpen (t i) ∧ a i ∈ t i

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
⊢ univ ⊆ univ ∧ IsOpen univ ∧ a i ∈ univ

Tactic:
exact ⟨Subset.rfl, isOpen_univ, mem_univ _⟩

Result:
no goals

Proof state:
case neg
ι : 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_1 ⊆ (fun a => if a ∈ I then t a else univ) i, IsOpen t_1 ∧ a i ∈ t_1

Tactic:
use univ

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
⊢ univ ⊆ (fun a => if a ∈ I then t a else univ) i ∧ IsOpen univ ∧ a i ∈ univ

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 ((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

Tactic:
simp_rw [eval_image_pi (Finset.mem_coe.mpr hi)
    (pi_nonempty_iff.mpr fun i => ⟨_, fun _ => (h1 i).choose_spec.2.2⟩)]

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 ⋯.choose ∧ a i ∈ ⋯.choose

Proof state:
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

Tactic:
by_cases hi : i ∈ I

Result:
case pos
ι : 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_1 ⊆ (fun a => if a ∈ I then t a else univ) i, IsOpen t_1 ∧ a i ∈ t_1

case neg
ι : 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_1 ⊆ (fun a => if a ∈ I then t a else univ) i, IsOpen t_1 ∧ a i ∈ t_1

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
⊢ (univ.pi fun i => if i ∈ ↑I 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]

Result:
no goals

Proof state:
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

Tactic:
exact Subset.trans
  (pi_mono fun i hi => (eval_image_pi_subset hi).trans (h1 i).choose_spec.1) h2

Result:
no goals