Moving the forall around

Stream: new members

[Callum Cassidy-Nolan]

I'm working through this proof:

def intersection_of_topologies {X : Type*} {ι : Sort*}
  (f : ι → topological_space X) : topological_space X :=
{ is_open := λ s, ∀ i, (f i).is_open s,
  is_open_univ :=
  begin
    intro i,
    exact (f i).is_open_univ,
  end,
  is_open_inter :=
  begin
    intros s t hos hot i,
    specialize hos i,
    specialize hot i,
    exact (f i).is_open_inter s t hos hot,
  end,
  is_open_sUnion :=
  begin
    intros s ht j,
    have x := (f j).is_open_sUnion s,
  end
   }

the tactic state looks like this:

tactic failed, there are unsolved goals
state:
X : Type ?,
ι : Sort ?,
f : ι → topological_space X,
s : set (set X),
ht : ∀ (t : set X), t ∈ s → ∀ (i : ι), (f i).is_open t,
j : ι,
x : (∀ (t : set X), t ∈ s → (f j).is_open t) → (f j).is_open (⋃₀ s)
⊢ (f j).is_open (⋃₀ s)

As you can see x and ht look quite similar, and I wish I could write exact x ht to finish the proof, but that won't work. It's like I need to use specialize but only on the right side of the implication of ht, I haven't been able to figure out how to do this, but I have tried writing rw imp_forall_iff at ht to bring the quantifier out front, but it didn't work either saying

rewrite tactic failed, did not find instance of the pattern in the target expression
  ?m_1 → Π (x : ?m_2), ?m_3 x

Any tips on how to move forward with the proof?

[Callum Cassidy-Nolan]

The line have h : ∀ (t : set X), t ∈ s → (f j).is_open t, by tauto, suggested by Eric R solves it, is there a more explicit way to do this though?

[Junyan Xu]

It's surprising to me that simp_rw imp_forall_iff at ht also doesn't work, which should be able to rewrite under quantifier. The tactic-mode solution is apply x, intros t h, exact ht t h j, and if you want the term you'd do exact x (λ t h, ht t h j),