-- Mathlib/Topology/Bases.lean
lemma isOpenMap_eval (i : ι) : IsOpenMap (Function.eval i : (∀ i, π i) → π i)

Proof state:
case neg
ι : Type u_1
π : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (π i)
i : ι
U : (i : ι) → Set (π i)
s : Finset ι
hU : ∀ i ∈ s, U i ∈ {U | IsOpen U}
h : ((↑s).pi U).Nonempty
hi : i ∉ s
⊢ IsOpen univ

Tactic:
exact isOpen_univ

Result:
no goals

Proof state:
case intro.intro.intro.inr
ι : Type u_1
π : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (π i)
i : ι
U : (i : ι) → Set (π i)
s : Finset ι
hU : ∀ i ∈ s, U i ∈ {U | IsOpen U}
h : ((↑s).pi U).Nonempty
⊢ IsOpen (eval i '' (↑s).pi U)

Tactic:
by_cases hi : i ∈ s

Result:
case pos
ι : Type u_1
π : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (π i)
i : ι
U : (i : ι) → Set (π i)
s : Finset ι
hU : ∀ i ∈ s, U i ∈ {U | IsOpen U}
h : ((↑s).pi U).Nonempty
hi : i ∈ s
⊢ IsOpen (eval i '' (↑s).pi U)

case neg
ι : Type u_1
π : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (π i)
i : ι
U : (i : ι) → Set (π i)
s : Finset ι
hU : ∀ i ∈ s, U i ∈ {U | IsOpen U}
h : ((↑s).pi U).Nonempty
hi : i ∉ s
⊢ IsOpen (eval i '' (↑s).pi U)

Proof state:
ι : Type u_1
π : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (π i)
i : ι
⊢ ∀ s ∈ {S | ∃ U F, (∀ i ∈ F, U i ∈ {U | IsOpen U}) ∧ S = (↑F).pi U}, IsOpen (eval i '' s)

Tactic:
rintro _ ⟨U, s, hU, rfl⟩

Result:
case intro.intro.intro
ι : Type u_1
π : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (π i)
i : ι
U : (i : ι) → Set (π i)
s : Finset ι
hU : ∀ i ∈ s, U i ∈ {U | IsOpen U}
⊢ IsOpen (eval i '' (↑s).pi U)

Proof state:
case neg
ι : Type u_1
π : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (π i)
i : ι
U : (i : ι) → Set (π i)
s : Finset ι
hU : ∀ i ∈ s, U i ∈ {U | IsOpen U}
h : ((↑s).pi U).Nonempty
hi : i ∉ s
⊢ IsOpen (eval i '' (↑s).pi U)

Tactic:
rw [eval_image_pi_of_not_mem (mod_cast hi), if_pos h]

Result:
case neg
ι : Type u_1
π : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (π i)
i : ι
U : (i : ι) → Set (π i)
s : Finset ι
hU : ∀ i ∈ s, U i ∈ {U | IsOpen U}
h : ((↑s).pi U).Nonempty
hi : i ∉ s
⊢ IsOpen univ

Proof state:
case pos
ι : Type u_1
π : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (π i)
i : ι
U : (i : ι) → Set (π i)
s : Finset ι
hU : ∀ i ∈ s, U i ∈ {U | IsOpen U}
h : ((↑s).pi U).Nonempty
hi : i ∈ s
⊢ IsOpen (U i)

Tactic:
exact hU _ hi

Result:
no goals

Proof state:
case intro.intro.intro.inl
ι : Type u_1
π : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (π i)
i : ι
U : (i : ι) → Set (π i)
s : Finset ι
hU : ∀ i ∈ s, U i ∈ {U | IsOpen U}
h : (↑s).pi U = ∅
⊢ IsOpen (eval i '' (↑s).pi U)

Tactic:
simp [h]

Result:
no goals

Proof state:
ι : Type u_1
π : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (π i)
i : ι
⊢ IsOpenMap (eval i)

Tactic:
refine (isTopologicalBasis_pi fun _ ↦ isTopologicalBasis_opens).isOpenMap_iff.2 ?_

Result:
ι : Type u_1
π : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (π i)
i : ι
⊢ ∀ s ∈ {S | ∃ U F, (∀ i ∈ F, U i ∈ {U | IsOpen U}) ∧ S = (↑F).pi U}, IsOpen (eval i '' s)

Proof state:
case pos
ι : Type u_1
π : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (π i)
i : ι
U : (i : ι) → Set (π i)
s : Finset ι
hU : ∀ i ∈ s, U i ∈ {U | IsOpen U}
h : ((↑s).pi U).Nonempty
hi : i ∈ s
⊢ IsOpen (eval i '' (↑s).pi U)

Tactic:
rw [eval_image_pi (mod_cast hi) h]

Result:
case pos
ι : Type u_1
π : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (π i)
i : ι
U : (i : ι) → Set (π i)
s : Finset ι
hU : ∀ i ∈ s, U i ∈ {U | IsOpen U}
h : ((↑s).pi U).Nonempty
hi : i ∈ s
⊢ IsOpen (U i)

Proof state:
case intro.intro.intro
ι : Type u_1
π : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (π i)
i : ι
U : (i : ι) → Set (π i)
s : Finset ι
hU : ∀ i ∈ s, U i ∈ {U | IsOpen U}
⊢ IsOpen (eval i '' (↑s).pi U)

Tactic:
obtain h | h := ((s : Set ι).pi U).eq_empty_or_nonempty

Result:
case intro.intro.intro.inl
ι : Type u_1
π : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (π i)
i : ι
U : (i : ι) → Set (π i)
s : Finset ι
hU : ∀ i ∈ s, U i ∈ {U | IsOpen U}
h : (↑s).pi U = ∅
⊢ IsOpen (eval i '' (↑s).pi U)

case intro.intro.intro.inr
ι : Type u_1
π : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (π i)
i : ι
U : (i : ι) → Set (π i)
s : Finset ι
hU : ∀ i ∈ s, U i ∈ {U | IsOpen U}
h : ((↑s).pi U).Nonempty
⊢ IsOpen (eval i '' (↑s).pi U)