-- Mathlib/Topology/Bases.lean
theorem IsTopologicalBasis.iInf_induced {β : Type*} {ι : Type*} {X : ι → Type*}
    [t : Π i, TopologicalSpace (X i)] {T : Π i, Set (Set (X i))}
    (cond : ∀ i, IsTopologicalBasis (T i)) (f : Π i, β → X i) :
    IsTopologicalBasis (t := ⨅ i, induced (f i) (t i))
      { S | ∃ (U : ∀ i, Set (X i)) (F : Finset ι),
        (∀ i, i ∈ F → U i ∈ T i) ∧ S = ⋂ (i) (_ : i ∈ F), f i ⁻¹' U i }

Proof state:
case h.e'_3.h.e'_2.h.a.mpr.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
S : Set β
U : ι → Set β
F : Finset ι
hSU : S = ⋂ i ∈ F, U i
U' : (i : ι) → Set (X i)
hU' : ∀ i ∈ F, U' i ∈ T i
hUU' : ∀ i ∈ F, f i ⁻¹' U' i = U i
⊢ ∃ U F, (∀ i ∈ F, U i ∈ T i) ∧ S = ⋂ i ∈ F, f i ⁻¹' U i

Tactic:
exact ⟨U', F, hU', hSU ▸ (.symm <| iInter₂_congr hUU')⟩

Result:
no goals

Proof state:
β : 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 ∈ F, U i ∈ T i) ∧ S = ⋂ i ∈ F, f i ⁻¹' U i}

Tactic:
convert IsTopologicalBasis.iInf (fun i ↦ (cond i).induced (f i)) with S

Result:
case h.e'_3.h.e'_2.h.a
β : 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
S : Set β
⊢ (∃ U F, (∀ i ∈ F, U i ∈ T i) ∧ S = ⋂ i ∈ F, f i ⁻¹' U i) ↔
    ∃ U F, (∀ i ∈ F, U i ∈ preimage (f i) '' T i) ∧ S = ⋂ i ∈ F, U i

Proof state:
case h.e'_3.h.e'_2.h.a.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
S : Set β
U : (i : ι) → Set (X i)
F : Finset ι
hUT : ∀ i ∈ F, U i ∈ T i
hSU : S = ⋂ i ∈ F, f i ⁻¹' U i
⊢ ∃ U F, (∀ i ∈ F, U i ∈ preimage (f i) '' T i) ∧ S = ⋂ i ∈ F, U i

Tactic:
exact ⟨fun i ↦ (f i) ⁻¹' (U i), F, fun i hi ↦ mem_image_of_mem _ (hUT i hi), hSU⟩

Result:
no goals

Proof state:
case h.e'_3.h.e'_2.h.a.mpr.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
S : Set β
U : ι → Set β
F : Finset ι
hUT : ∀ i ∈ F, U i ∈ preimage (f i) '' T i
hSU : S = ⋂ i ∈ F, U i
⊢ ∃ U F, (∀ i ∈ F, U i ∈ T i) ∧ S = ⋂ i ∈ F, f i ⁻¹' U i

Tactic:
choose! U' hU' hUU' using hUT

Result:
case h.e'_3.h.e'_2.h.a.mpr.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
S : Set β
U : ι → Set β
F : Finset ι
hSU : S = ⋂ i ∈ F, U i
U' : (i : ι) → Set (X i)
hU' : ∀ i ∈ F, U' i ∈ T i
hUU' : ∀ i ∈ F, f i ⁻¹' U' i = U i
⊢ ∃ U F, (∀ i ∈ F, U i ∈ T i) ∧ S = ⋂ i ∈ F, f i ⁻¹' U i

Proof state:
case h.e'_3.h.e'_2.h.a
β : 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
S : Set β
⊢ (∃ U F, (∀ i ∈ F, U i ∈ T i) ∧ S = ⋂ i ∈ F, f i ⁻¹' U i) ↔
    ∃ U F, (∀ i ∈ F, U i ∈ preimage (f i) '' T i) ∧ S = ⋂ i ∈ F, U i

Tactic:
constructor <;> rintro ⟨U, F, hUT, hSU⟩

Result:
case h.e'_3.h.e'_2.h.a.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
S : Set β
U : (i : ι) → Set (X i)
F : Finset ι
hUT : ∀ i ∈ F, U i ∈ T i
hSU : S = ⋂ i ∈ F, f i ⁻¹' U i
⊢ ∃ U F, (∀ i ∈ F, U i ∈ preimage (f i) '' T i) ∧ S = ⋂ i ∈ F, U i

case h.e'_3.h.e'_2.h.a.mpr.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
S : Set β
U : ι → Set β
F : Finset ι
hUT : ∀ i ∈ F, U i ∈ preimage (f i) '' T i
hSU : S = ⋂ i ∈ F, U i
⊢ ∃ U F, (∀ i ∈ F, U i ∈ T i) ∧ S = ⋂ i ∈ F, f i ⁻¹' U i