β : Type u_1
ι : Type u_2
X : ι → Type u_3
t : (i : ι) → TopologicalSpace (X i)
T : (i : ι) → Set (Set (X i))
cond : ∀ (i : ι), IsTopologicalBasis (T i)
f : (i : ι) → β → X i
this : TopologicalSpace β := ⨅ (i : ι), induced (f i) (t i)
⊢ IsTopologicalBasis {S | ∃ U F, (∀ (i : ι), i ∈ F → U i ∈ T i) ∧ S = ⋂ (i : ι) (_ : i ∈ F), f i ⁻¹' U i}
β : Type u_1
ι : Type u_2
X : ι → Type u_3
t : (i : ι) → TopologicalSpace (X i)
T : (i : ι) → Set (Set (X i))
cond : ∀ (i : ι), IsTopologicalBasis (T i)
f : (i : ι) → β → X i
⊢ IsTopologicalBasis {S | ∃ U F, (∀ (i : ι), i ∈ F → U i ∈ T i) ∧ S = ⋂ (i : ι) (_ : i ∈ F), f i ⁻¹' U i}
letI := ⨅ i, induced (f i) (t i)
case h.e'_3
β : Type u_1
ι : Type u_2
X : ι → Type u_3
t : (i : ι) → TopologicalSpace (X i)
T : (i : ι) → Set (Set (X i))
cond : ∀ (i : ι), IsTopologicalBasis (T i)
f : (i : ι) → β → X i
this : TopologicalSpace β := ⨅ (i : ι), induced (f i) (t i)
⊢ {S | ∃ U F, (∀ (i : ι), i ∈ F → U i ∈ T i) ∧ S = ⋂ (i : ι) (_ : i ∈ F), f i ⁻¹' U i} =
    (preimage fun x i => f i x) '' {S | ∃ U F, (∀ (i : ι), i ∈ F → U i ∈ T i) ∧ S = Set.pi (↑F) U}
β : Type u_1
ι : Type u_2
X : ι → Type u_3
t : (i : ι) → TopologicalSpace (X i)
T : (i : ι) → Set (Set (X i))
cond : ∀ (i : ι), IsTopologicalBasis (T i)
f : (i : ι) → β → X i
this : TopologicalSpace β := ⨅ (i : ι), induced (f i) (t i)
⊢ IsTopologicalBasis {S | ∃ U F, (∀ (i : ι), i ∈ F → U i ∈ T i) ∧ S = ⋂ (i : ι) (_ : i ∈ F), f i ⁻¹' U i}
convert (isTopologicalBasis_pi cond).inducing (inducing_iInf_to_pi f)
case h.e'_3.h
β : Type u_1
ι : Type u_2
X : ι → Type u_3
t : (i : ι) → TopologicalSpace (X i)
T : (i : ι) → Set (Set (X i))
cond : ∀ (i : ι), IsTopologicalBasis (T i)
f : (i : ι) → β → X i
this : TopologicalSpace β := ⨅ (i : ι), induced (f i) (t i)
V : Set β
⊢ V ∈ {S | ∃ U F, (∀ (i : ι), i ∈ F → U i ∈ T i) ∧ S = ⋂ (i : ι) (_ : i ∈ F), f i ⁻¹' U i} ↔
    V ∈ (preimage fun x i => f i x) '' {S | ∃ U F, (∀ (i : ι), i ∈ F → U i ∈ T i) ∧ S = Set.pi (↑F) U}
case h.e'_3
β : Type u_1
ι : Type u_2
X : ι → Type u_3
t : (i : ι) → TopologicalSpace (X i)
T : (i : ι) → Set (Set (X i))
cond : ∀ (i : ι), IsTopologicalBasis (T i)
f : (i : ι) → β → X i
this : TopologicalSpace β := ⨅ (i : ι), induced (f i) (t i)
⊢ {S | ∃ U F, (∀ (i : ι), i ∈ F → U i ∈ T i) ∧ S = ⋂ (i : ι) (_ : i ∈ F), f i ⁻¹' U i} =
    (preimage fun x i => f i x) '' {S | ∃ U F, (∀ (i : ι), i ∈ F → U i ∈ T i) ∧ S = Set.pi (↑F) U}
ext V
case h.e'_3.h.mp
β : Type u_1
ι : Type u_2
X : ι → Type u_3
t : (i : ι) → TopologicalSpace (X i)
T : (i : ι) → Set (Set (X i))
cond : ∀ (i : ι), IsTopologicalBasis (T i)
f : (i : ι) → β → X i
this : TopologicalSpace β := ⨅ (i : ι), induced (f i) (t i)
V : Set β
⊢ V ∈ {S | ∃ U F, (∀ (i : ι), i ∈ F → U i ∈ T i) ∧ S = ⋂ (i : ι) (_ : i ∈ F), f i ⁻¹' U i} →
    V ∈ (preimage fun x i => f i x) '' {S | ∃ U F, (∀ (i : ι), i ∈ F → U i ∈ T i) ∧ S = Set.pi (↑F) U}

case h.e'_3.h.mpr
β : Type u_1
ι : Type u_2
X : ι → Type u_3
t : (i : ι) → TopologicalSpace (X i)
T : (i : ι) → Set (Set (X i))
cond : ∀ (i : ι), IsTopologicalBasis (T i)
f : (i : ι) → β → X i
this : TopologicalSpace β := ⨅ (i : ι), induced (f i) (t i)
V : Set β
⊢ V ∈ (preimage fun x i => f i x) '' {S | ∃ U F, (∀ (i : ι), i ∈ F → U i ∈ T i) ∧ S = Set.pi (↑F) U} →
    V ∈ {S | ∃ U F, (∀ (i : ι), i ∈ F → U i ∈ T i) ∧ S = ⋂ (i : ι) (_ : i ∈ F), f i ⁻¹' U i}
case h.e'_3.h
β : Type u_1
ι : Type u_2
X : ι → Type u_3
t : (i : ι) → TopologicalSpace (X i)
T : (i : ι) → Set (Set (X i))
cond : ∀ (i : ι), IsTopologicalBasis (T i)
f : (i : ι) → β → X i
this : TopologicalSpace β := ⨅ (i : ι), induced (f i) (t i)
V : Set β
⊢ V ∈ {S | ∃ U F, (∀ (i : ι), i ∈ F → U i ∈ T i) ∧ S = ⋂ (i : ι) (_ : i ∈ F), f i ⁻¹' U i} ↔
    V ∈ (preimage fun x i => f i x) '' {S | ∃ U F, (∀ (i : ι), i ∈ F → U i ∈ T i) ∧ S = Set.pi (↑F) U}
constructor
case h.e'_3.h.mp.intro.intro.intro
β : Type u_1
ι : Type u_2
X : ι → Type u_3
t : (i : ι) → TopologicalSpace (X i)
T : (i : ι) → Set (Set (X i))
cond : ∀ (i : ι), IsTopologicalBasis (T i)
f : (i : ι) → β → X i
this : TopologicalSpace β := ⨅ (i : ι), induced (f i) (t i)
U : (i : ι) → Set (X i)
F : Finset ι
h1 : ∀ (i : ι), i ∈ F → U i ∈ T i
⊢ (⋂ (i : ι) (_ : i ∈ F), f i ⁻¹' U i) ∈
    (preimage fun x i => f i x) '' {S | ∃ U F, (∀ (i : ι), i ∈ F → U i ∈ T i) ∧ S = Set.pi (↑F) U}
case h.e'_3.h.mp
β : Type u_1
ι : Type u_2
X : ι → Type u_3
t : (i : ι) → TopologicalSpace (X i)
T : (i : ι) → Set (Set (X i))
cond : ∀ (i : ι), IsTopologicalBasis (T i)
f : (i : ι) → β → X i
this : TopologicalSpace β := ⨅ (i : ι), induced (f i) (t i)
V : Set β
⊢ V ∈ {S | ∃ U F, (∀ (i : ι), i ∈ F → U i ∈ T i) ∧ S = ⋂ (i : ι) (_ : i ∈ F), f i ⁻¹' U i} →
    V ∈ (preimage fun x i => f i x) '' {S | ∃ U F, (∀ (i : ι), i ∈ F → U i ∈ T i) ∧ S = Set.pi (↑F) U}
rintro ⟨U, F, h1, rfl⟩
case h.e'_3.h.mp.intro.intro.intro
β : Type u_1
ι : Type u_2
X : ι → Type u_3
t : (i : ι) → TopologicalSpace (X i)
T : (i : ι) → Set (Set (X i))
cond : ∀ (i : ι), IsTopologicalBasis (T i)
f : (i : ι) → β → X i
this : TopologicalSpace β := ⨅ (i : ι), induced (f i) (t i)
U : (i : ι) → Set (X i)
F : Finset ι
h1 : ∀ (i : ι), i ∈ F → U i ∈ T i
⊢ (fun x i => f i x) ⁻¹' Set.pi (↑F) U = ⋂ (i : ι) (_ : i ∈ F), f i ⁻¹' U i
case h.e'_3.h.mp.intro.intro.intro
β : Type u_1
ι : Type u_2
X : ι → Type u_3
t : (i : ι) → TopologicalSpace (X i)
T : (i : ι) → Set (Set (X i))
cond : ∀ (i : ι), IsTopologicalBasis (T i)
f : (i : ι) → β → X i
this : TopologicalSpace β := ⨅ (i : ι), induced (f i) (t i)
U : (i : ι) → Set (X i)
F : Finset ι
h1 : ∀ (i : ι), i ∈ F → U i ∈ T i
⊢ (⋂ (i : ι) (_ : i ∈ F), f i ⁻¹' U i) ∈
    (preimage fun x i => f i x) '' {S | ∃ U F, (∀ (i : ι), i ∈ F → U i ∈ T i) ∧ S = Set.pi (↑F) U}
refine' ⟨(F : Set ι).pi U, ⟨U, F, h1, rfl⟩, _⟩
case h.e'_3.h.mp.intro.intro.intro
β : Type u_1
ι : Type u_2
X : ι → Type u_3
t : (i : ι) → TopologicalSpace (X i)
T : (i : ι) → Set (Set (X i))
cond : ∀ (i : ι), IsTopologicalBasis (T i)
f : (i : ι) → β → X i
this : TopologicalSpace β := ⨅ (i : ι), induced (f i) (t i)
U : (i : ι) → Set (X i)
F : Finset ι
h1 : ∀ (i : ι), i ∈ F → U i ∈ T i
⊢ (⋂ (i : ι) (_ : i ∈ ↑F), (fun x i => f i x) ⁻¹' (eval i ⁻¹' U i)) = ⋂ (i : ι) (_ : i ∈ F), f i ⁻¹' U i
case h.e'_3.h.mp.intro.intro.intro
β : Type u_1
ι : Type u_2
X : ι → Type u_3
t : (i : ι) → TopologicalSpace (X i)
T : (i : ι) → Set (Set (X i))
cond : ∀ (i : ι), IsTopologicalBasis (T i)
f : (i : ι) → β → X i
this : TopologicalSpace β := ⨅ (i : ι), induced (f i) (t i)
U : (i : ι) → Set (X i)
F : Finset ι
h1 : ∀ (i : ι), i ∈ F → U i ∈ T i
⊢ (fun x i => f i x) ⁻¹' Set.pi (↑F) U = ⋂ (i : ι) (_ : i ∈ F), f i ⁻¹' U i
simp_rw [pi_def, Set.preimage_iInter]
no goals
case h.e'_3.h.mp.intro.intro.intro
β : Type u_1
ι : Type u_2
X : ι → Type u_3
t : (i : ι) → TopologicalSpace (X i)
T : (i : ι) → Set (Set (X i))
cond : ∀ (i : ι), IsTopologicalBasis (T i)
f : (i : ι) → β → X i
this : TopologicalSpace β := ⨅ (i : ι), induced (f i) (t i)
U : (i : ι) → Set (X i)
F : Finset ι
h1 : ∀ (i : ι), i ∈ F → U i ∈ T i
⊢ (⋂ (i : ι) (_ : i ∈ ↑F), (fun x i => f i x) ⁻¹' (eval i ⁻¹' U i)) = ⋂ (i : ι) (_ : i ∈ F), f i ⁻¹' U i
rfl
case h.e'_3.h.mpr.intro.intro.intro.intro.intro
β : Type u_1
ι : Type u_2
X : ι → Type u_3
t : (i : ι) → TopologicalSpace (X i)
T : (i : ι) → Set (Set (X i))
cond : ∀ (i : ι), IsTopologicalBasis (T i)
f : (i : ι) → β → X i
this : TopologicalSpace β := ⨅ (i : ι), induced (f i) (t i)
U : (i : ι) → Set (X i)
F : Finset ι
h1 : ∀ (i : ι), i ∈ F → U i ∈ T i
⊢ (fun x i => f i x) ⁻¹' Set.pi (↑F) U ∈
    {S | ∃ U F, (∀ (i : ι), i ∈ F → U i ∈ T i) ∧ S = ⋂ (i : ι) (_ : i ∈ F), f i ⁻¹' U i}
case h.e'_3.h.mpr
β : Type u_1
ι : Type u_2
X : ι → Type u_3
t : (i : ι) → TopologicalSpace (X i)
T : (i : ι) → Set (Set (X i))
cond : ∀ (i : ι), IsTopologicalBasis (T i)
f : (i : ι) → β → X i
this : TopologicalSpace β := ⨅ (i : ι), induced (f i) (t i)
V : Set β
⊢ V ∈ (preimage fun x i => f i x) '' {S | ∃ U F, (∀ (i : ι), i ∈ F → U i ∈ T i) ∧ S = Set.pi (↑F) U} →
    V ∈ {S | ∃ U F, (∀ (i : ι), i ∈ F → U i ∈ T i) ∧ S = ⋂ (i : ι) (_ : i ∈ F), f i ⁻¹' U i}
rintro ⟨U, ⟨U, F, h1, rfl⟩, rfl⟩
case h.e'_3.h.mpr.intro.intro.intro.intro.intro
β : Type u_1
ι : Type u_2
X : ι → Type u_3
t : (i : ι) → TopologicalSpace (X i)
T : (i : ι) → Set (Set (X i))
cond : ∀ (i : ι), IsTopologicalBasis (T i)
f : (i : ι) → β → X i
this : TopologicalSpace β := ⨅ (i : ι), induced (f i) (t i)
U : (i : ι) → Set (X i)
F : Finset ι
h1 : ∀ (i : ι), i ∈ F → U i ∈ T i
⊢ (fun x i => f i x) ⁻¹' Set.pi (↑F) U = ⋂ (i : ι) (_ : i ∈ F), f i ⁻¹' U i
case h.e'_3.h.mpr.intro.intro.intro.intro.intro
β : Type u_1
ι : Type u_2
X : ι → Type u_3
t : (i : ι) → TopologicalSpace (X i)
T : (i : ι) → Set (Set (X i))
cond : ∀ (i : ι), IsTopologicalBasis (T i)
f : (i : ι) → β → X i
this : TopologicalSpace β := ⨅ (i : ι), induced (f i) (t i)
U : (i : ι) → Set (X i)
F : Finset ι
h1 : ∀ (i : ι), i ∈ F → U i ∈ T i
⊢ (fun x i => f i x) ⁻¹' Set.pi (↑F) U ∈
    {S | ∃ U F, (∀ (i : ι), i ∈ F → U i ∈ T i) ∧ S = ⋂ (i : ι) (_ : i ∈ F), f i ⁻¹' U i}
refine' ⟨U, F, h1, _⟩
case h.e'_3.h.mpr.intro.intro.intro.intro.intro
β : Type u_1
ι : Type u_2
X : ι → Type u_3
t : (i : ι) → TopologicalSpace (X i)
T : (i : ι) → Set (Set (X i))
cond : ∀ (i : ι), IsTopologicalBasis (T i)
f : (i : ι) → β → X i
this : TopologicalSpace β := ⨅ (i : ι), induced (f i) (t i)
U : (i : ι) → Set (X i)
F : Finset ι
h1 : ∀ (i : ι), i ∈ F → U i ∈ T i
⊢ (⋂ (i : ι) (_ : i ∈ ↑F), (fun x i => f i x) ⁻¹' (eval i ⁻¹' U i)) = ⋂ (i : ι) (_ : i ∈ F), f i ⁻¹' U i
case h.e'_3.h.mpr.intro.intro.intro.intro.intro
β : Type u_1
ι : Type u_2
X : ι → Type u_3
t : (i : ι) → TopologicalSpace (X i)
T : (i : ι) → Set (Set (X i))
cond : ∀ (i : ι), IsTopologicalBasis (T i)
f : (i : ι) → β → X i
this : TopologicalSpace β := ⨅ (i : ι), induced (f i) (t i)
U : (i : ι) → Set (X i)
F : Finset ι
h1 : ∀ (i : ι), i ∈ F → U i ∈ T i
⊢ (fun x i => f i x) ⁻¹' Set.pi (↑F) U = ⋂ (i : ι) (_ : i ∈ F), f i ⁻¹' U i
simp_rw [pi_def, Set.preimage_iInter]
no goals
case h.e'_3.h.mpr.intro.intro.intro.intro.intro
β : Type u_1
ι : Type u_2
X : ι → Type u_3
t : (i : ι) → TopologicalSpace (X i)
T : (i : ι) → Set (Set (X i))
cond : ∀ (i : ι), IsTopologicalBasis (T i)
f : (i : ι) → β → X i
this : TopologicalSpace β := ⨅ (i : ι), induced (f i) (t i)
U : (i : ι) → Set (X i)
F : Finset ι
h1 : ∀ (i : ι), i ∈ F → U i ∈ T i
⊢ (⋂ (i : ι) (_ : i ∈ ↑F), (fun x i => f i x) ⁻¹' (eval i ⁻¹' U i)) = ⋂ (i : ι) (_ : i ∈ F), f i ⁻¹' U i
rfl