Products of Cauchy filter are Cauchy, a shameful proof

prod_cauchy.lean

import analysis.topology.uniform_space

variables {α : Type*} {β : Type*} [uniform_space α] [uniform_space β]

lemma prod_cauchy {f : filter α} {g : filter β} : cauchy f → cauchy g → cauchy (filter.prod f g) :=
begin
  rintros ⟨f_neq, f_prod⟩ ⟨g_neq, g_prod⟩,
  split,
  { rw filter.prod_neq_bot,
    cc },
  { let p_α := λ (p : (α × β) × α × β), ((p.fst).fst, (p.snd).fst),
    let p_β := λ (p : (α × β) × α × β), ((p.fst).snd, (p.snd).snd),
    rw uniformity_prod,
    have h1 : filter.prod (filter.prod f g) (filter.prod f g) ≤
    filter.vmap p_α uniformity, 
    { intros r r_in,
      rw filter.mem_vmap_sets at r_in,
      rcases r_in with ⟨t, t_in, ht⟩,
      rw filter.mem_prod_iff,
      suffices : ∃ (t₁ ∈ (filter.prod f g).sets) (t₂ ∈ (filter.prod f g).sets),
        set.prod t₁ t₂ ⊆ p_α ⁻¹' t,
      { rcases this with ⟨t₁, in₁, t₂, in₂, H⟩,
        existsi [t₁, in₁, t₂, in₂],
        exact set.subset.trans H ht },
      
      have t_in_ff := f_prod t_in,
      have univ_in_gg : set.univ ∈ (filter.prod g g).sets := filter.univ_mem_sets,
      rw filter.mem_prod_iff at t_in_ff,
      rw filter.mem_prod_iff at univ_in_gg,
      rcases t_in_ff with ⟨a₁, a₁_in, a₂, a₂_in, ha⟩,
      rcases univ_in_gg with ⟨b₁, b₁_in, b₂, b₂_in, hb⟩,
      let p₁ := set.prod a₁ b₁, 
      have in₁ : p₁ ∈ (filter.prod f g).sets,
      by apply filter.prod_mem_prod ; assumption,
      let p₂ := set.prod a₂ b₂, 
      have in₂ : p₂ ∈ (filter.prod f g).sets,
      by apply filter.prod_mem_prod ; assumption,
      existsi [p₁, in₁, p₂, in₂],
      intros x x_in,
      apply ha,
      dsimp[p_α],
      dsimp [p₁, p₂] at x_in,
      dsimp[set.prod] at x_in,
      cc },
    have h2 : filter.prod (filter.prod f g) (filter.prod f g) ≤ filter.vmap p_β uniformity, 
    { intros r r_in,
      rw filter.mem_vmap_sets at r_in,
      rcases r_in with ⟨t, t_in, ht⟩,
      rw filter.mem_prod_iff,
      suffices : ∃ (t₁ ∈ (filter.prod f g).sets) (t₂ ∈ (filter.prod f g).sets),
        set.prod t₁ t₂ ⊆ p_β ⁻¹' t,
      { rcases this with ⟨t₁, in₁, t₂, in₂, H⟩,
        existsi [t₁, in₁, t₂, in₂],
        exact set.subset.trans H ht },
      
      have t_in_gg := g_prod t_in,
      have univ_in_ff : set.univ ∈ (filter.prod f f).sets := filter.univ_mem_sets,
      rw filter.mem_prod_iff at t_in_gg,
      rw filter.mem_prod_iff at univ_in_ff,
      rcases t_in_gg with ⟨b₁, b₁_in, b₂, b₂_in, hb⟩,
      rcases univ_in_ff with ⟨a₁, a₁_in, a₂, a₂_in, ha⟩,
      let p₁ := set.prod a₁ b₁, 
      have in₁ : p₁ ∈ (filter.prod f g).sets,
      by apply filter.prod_mem_prod ; assumption,
      let p₂ := set.prod a₂ b₂, 
      have in₂ : p₂ ∈ (filter.prod f g).sets,
      by apply filter.prod_mem_prod ; assumption,
      existsi [p₁, in₁, p₂, in₂],
      intros x x_in,
      apply hb,
      dsimp[p_β],
      dsimp [p₁, p₂] at x_in,
      dsimp[set.prod] at x_in,
      cc },
    exact lattice.le_inf h1 h2 },
end