calc
  Continuous TZ (ProductTopology T) f
  _ ↔ f ⁎ TZ ∈ lowerBounds (Set.range (fun i ↦ (fun x ↦ x i) ^* (T i))) := by {
        rw [CompleteLattice.I_isInf]
        exact Iff.rfl
        }
  _ ↔ ∀ i, f ⁎ TZ ≤ (fun x ↦ x i) ^* (T i)        := by rw [lowerBounds_range]
  _ ↔ ∀ i, (fun x ↦ x i) ⁎ (f ⁎ TZ) ≤ T i        := by {
        apply forall_congr'
        intro i
        rw [pull, ← adjunction_of_Sup (fun s ↦ push_Sup _), push_push]
        }
  _ ↔ ∀ i,  Continuous TZ (T i) (fun z ↦ f z i)  := Iff.rfl
ι : Type
X : ι → Type
T : Π (i : ι), Topology (X i)
Z : Type
TZ : Topology Z
f : Z → Π (i : ι), X i
⊢ Continuous TZ (ProductTopology T) f ↔ ∀ (i : ι), Continuous TZ (T i) fun z => f z i
no goals