topological spaces - generated topology

Stream: Lean for the curious mathematician 2020

[Antoine Chambert-Loir]

Hello.
I am stuck in Exercise 2 of topological_spaces.lean, desperately trying to prove lemma is_open_prod_iff, specifically the -> implication,
that if a set s of X \times Y is open then for every (a,b) in s, there are open sets u in X and v in Y such that (a,b) \in s \subset u \times v.
After intros open_s a b ab_in_s, I have to enter the 4 cases of the inductive definition of generated_open, which I do with cases open_s, but I can't manage to make use of the hypothesis
open_s_a: generated_open (X × Y) {U : set (X × Y) | ∃ (Ux : set X) (Uy : set Y) (hx : is_open Ux) (hy : is_open Uy), U = Ux.prod Uy} open_s_A
that I obtain.
I suspect a serious misunderstanding of my part somewhere, but where?

[Patrick Massot]

I think this was not meant to be part of the exercise series. It was left intentionally without a proof.

[Kevin Buzzard]

Did you do induction on the hypothesis rather than cases?

[Antoine Chambert-Loir]

Kevin Buzzard said:

Did you do induction on the hypothesis rather than cases?

Hum… that must be the problem… :-(

[Alex J. Best]

So like Patrick says, I left it without proof, not as an exercise because really its best to build up a library of smaller results to prove this. But I did prove this direction just now with a brainless human powered tactic of me spamming the tactics rcases? library_search use split simp dsimp the result is this monstrosity:

lemma is_open_prod_iff (X Y : Type) [topological_space X] [topological_space Y]
  {s : set (X × Y)} :
is_open s ↔ (∀a b, (a, b) ∈ s → ∃u v, is_open u ∧ is_open v ∧
                                  a ∈ u ∧ b ∈ v ∧ set.prod u v ⊆ s) :=
begin
  split,
  { intros open_s a b ab_in_s,
    induction open_s,
    { rcases open_s_H with ⟨u, v, hu, hv, rfl⟩,
      dsimp at ab_in_s,
      use [u, v, hu, hv],
      refine ⟨ab_in_s.1, ab_in_s.2, _⟩,
      exact subset.rfl, },
    { use [univ,univ,univ_mem,univ_mem, mem_univ _, mem_univ _], exact subset_univ _,},
    { rcases open_s_ih_a ab_in_s.1 with ⟨w, h_w, h_h_left, h_h_right_left, h_h_right_right_left, h_h_right_right_right, k⟩ ,
      rcases open_s_ih_a_1 ab_in_s.2 with ⟨w2, h_w2, h_h_left2, h_h_right_left2, h_h_right_right_left2, h_h_right_right_right2, k2⟩,
      use [w ∩ w2],
      use [h_w ∩ h_w2],
      split,
      exact inter w w2 h_h_left h_h_left2,
      split,
      exact inter h_w h_w2 h_h_right_left h_h_right_left2,
      split, exact mem_inter h_h_right_right_left h_h_right_right_left2,
      split, exact mem_inter h_h_right_right_right h_h_right_right_right2,
      simp,
      split,
      rw ← prod_inter_prod,
      apply subset.trans _ k,
      exact (set.prod w h_w).inter_subset_left (set.prod w2 h_w2),
      rw ← prod_inter_prod,
      apply subset.trans _ k2,
      exact (set.prod w h_w).inter_subset_right (set.prod w2 h_w2),
    },
    { simp * at *,
      dsimp at *,
      rcases ab_in_s with ⟨hxy_w, hxy_h_left, hxy_h_right⟩,
      specialize open_s_a _ hxy_h_left,
      rcases open_s_ih _ hxy_h_left hxy_h_right with ⟨w, h_w, h_h_left, h_h_right_left, h_h_right_right_left, h_h_right_right_right, k⟩,
      use [w, h_h_left, h_w, h_h_right_left, h_h_right_right_left, h_h_right_right_right],
      apply subset.trans,
      exact k,
      exact subset_sUnion_of_mem hxy_h_left, } },
    {sorry,},
end

[Alex J. Best]

I'm sure it doesn't need to be anywhere near this bad, but I didn't want to think at all!

[Antoine Chambert-Loir]

Thanks @Alex J. Best , I'll finish my own (hand made) version of the proof, and I'm not sure it'll be significantly different from that.
(I can't work on it today, but I'll come back to you soon!)