-- Mathlib/Topology/UniformSpace/UniformConvergence.lean
theorem UniformCauchySeqOnFilter.comp {γ : Type*} (hf : UniformCauchySeqOnFilter F p p')
    (g : γ → α) : UniformCauchySeqOnFilter (fun n => F n ∘ g) p (p'.comap g) := fun u hu => by
  obtain ⟨pa, hpa, pb, hpb, hpapb⟩ := eventually_prod_iff.mp (hf u hu)
  rw [eventually_prod_iff]
  refine ⟨pa, hpa, pb ∘ g, ?_, fun hx _ hy => hpapb hx hy⟩
  exact eventually_comap.mpr (hpb.mono fun x hx y hy => by simp only [hx, hy, Function.comp_apply])

Proof state:
α : Type u
β : Type v
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
p : Filter ι
p' : Filter α
γ : Type u_1
hf : UniformCauchySeqOnFilter F p p'
g : γ → α
u : Set (β × β)
hu : u ∈ 𝓤 β
pa : ι × ι → Prop
hpa : ∀ᶠ (x : ι × ι) in p ×ˢ p, pa x
pb : α → Prop
hpb : ∀ᶠ (y : α) in p', pb y
hpapb : ∀ {x : ι × ι}, pa x → ∀ {y : α}, pb y → (F (x, y).1.1 (x, y).2, F (x, y).1.2 (x, y).2) ∈ u
x : α
hx : pb x
y : γ
hy : g y = x
⊢ (pb ∘ g) y

Tactic:
simp only [hx, hy, Function.comp_apply]

Result:
no goals

Proof state:
case intro.intro.intro.intro
α : Type u
β : Type v
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
p : Filter ι
p' : Filter α
γ : Type u_1
hf : UniformCauchySeqOnFilter F p p'
g : γ → α
u : Set (β × β)
hu : u ∈ 𝓤 β
pa : ι × ι → Prop
hpa : ∀ᶠ (x : ι × ι) in p ×ˢ p, pa x
pb : α → Prop
hpb : ∀ᶠ (y : α) in p', pb y
hpapb : ∀ {x : ι × ι}, pa x → ∀ {y : α}, pb y → (F (x, y).1.1 (x, y).2, F (x, y).1.2 (x, y).2) ∈ u
⊢ ∃ pa,
    (∀ᶠ (x : ι × ι) in p ×ˢ p, pa x) ∧
      ∃ pb,
        (∀ᶠ (y : γ) in comap g p', pb y) ∧
          ∀ {x : ι × ι},
            pa x →
              ∀ {y : γ}, pb y → ((fun n => F n ∘ g) (x, y).1.1 (x, y).2, (fun n => F n ∘ g) (x, y).1.2 (x, y).2) ∈ u

Tactic:
refine ⟨pa, hpa, pb ∘ g, ?_, fun hx _ hy => hpapb hx hy⟩

Result:
case intro.intro.intro.intro
α : Type u
β : Type v
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
p : Filter ι
p' : Filter α
γ : Type u_1
hf : UniformCauchySeqOnFilter F p p'
g : γ → α
u : Set (β × β)
hu : u ∈ 𝓤 β
pa : ι × ι → Prop
hpa : ∀ᶠ (x : ι × ι) in p ×ˢ p, pa x
pb : α → Prop
hpb : ∀ᶠ (y : α) in p', pb y
hpapb : ∀ {x : ι × ι}, pa x → ∀ {y : α}, pb y → (F (x, y).1.1 (x, y).2, F (x, y).1.2 (x, y).2) ∈ u
⊢ ∀ᶠ (y : γ) in comap g p', (pb ∘ g) y

Proof state:
case intro.intro.intro.intro
α : Type u
β : Type v
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
p : Filter ι
p' : Filter α
γ : Type u_1
hf : UniformCauchySeqOnFilter F p p'
g : γ → α
u : Set (β × β)
hu : u ∈ 𝓤 β
pa : ι × ι → Prop
hpa : ∀ᶠ (x : ι × ι) in p ×ˢ p, pa x
pb : α → Prop
hpb : ∀ᶠ (y : α) in p', pb y
hpapb : ∀ {x : ι × ι}, pa x → ∀ {y : α}, pb y → (F (x, y).1.1 (x, y).2, F (x, y).1.2 (x, y).2) ∈ u
⊢ ∀ᶠ (m : (ι × ι) × γ) in (p ×ˢ p) ×ˢ comap g p', ((fun n => F n ∘ g) m.1.1 m.2, (fun n => F n ∘ g) m.1.2 m.2) ∈ u

Tactic:
rw [eventually_prod_iff]

Result:
case intro.intro.intro.intro
α : Type u
β : Type v
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
p : Filter ι
p' : Filter α
γ : Type u_1
hf : UniformCauchySeqOnFilter F p p'
g : γ → α
u : Set (β × β)
hu : u ∈ 𝓤 β
pa : ι × ι → Prop
hpa : ∀ᶠ (x : ι × ι) in p ×ˢ p, pa x
pb : α → Prop
hpb : ∀ᶠ (y : α) in p', pb y
hpapb : ∀ {x : ι × ι}, pa x → ∀ {y : α}, pb y → (F (x, y).1.1 (x, y).2, F (x, y).1.2 (x, y).2) ∈ u
⊢ ∃ pa,
    (∀ᶠ (x : ι × ι) in p ×ˢ p, pa x) ∧
      ∃ pb,
        (∀ᶠ (y : γ) in comap g p', pb y) ∧
          ∀ {x : ι × ι},
            pa x →
              ∀ {y : γ}, pb y → ((fun n => F n ∘ g) (x, y).1.1 (x, y).2, (fun n => F n ∘ g) (x, y).1.2 (x, y).2) ∈ u

Proof state:
α : Type u
β : Type v
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
p : Filter ι
p' : Filter α
γ : Type u_1
hf : UniformCauchySeqOnFilter F p p'
g : γ → α
u : Set (β × β)
hu : u ∈ 𝓤 β
⊢ ∀ᶠ (m : (ι × ι) × γ) in (p ×ˢ p) ×ˢ comap g p', ((fun n => F n ∘ g) m.1.1 m.2, (fun n => F n ∘ g) m.1.2 m.2) ∈ u

Tactic:
obtain ⟨pa, hpa, pb, hpb, hpapb⟩ := eventually_prod_iff.mp (hf u hu)

Result:
case intro.intro.intro.intro
α : Type u
β : Type v
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
p : Filter ι
p' : Filter α
γ : Type u_1
hf : UniformCauchySeqOnFilter F p p'
g : γ → α
u : Set (β × β)
hu : u ∈ 𝓤 β
pa : ι × ι → Prop
hpa : ∀ᶠ (x : ι × ι) in p ×ˢ p, pa x
pb : α → Prop
hpb : ∀ᶠ (y : α) in p', pb y
hpapb : ∀ {x : ι × ι}, pa x → ∀ {y : α}, pb y → (F (x, y).1.1 (x, y).2, F (x, y).1.2 (x, y).2) ∈ u
⊢ ∀ᶠ (m : (ι × ι) × γ) in (p ×ˢ p) ×ˢ comap g p', ((fun n => F n ∘ g) m.1.1 m.2, (fun n => F n ∘ g) m.1.2 m.2) ∈ u

Proof state:
case intro.intro.intro.intro
α : Type u
β : Type v
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
p : Filter ι
p' : Filter α
γ : Type u_1
hf : UniformCauchySeqOnFilter F p p'
g : γ → α
u : Set (β × β)
hu : u ∈ 𝓤 β
pa : ι × ι → Prop
hpa : ∀ᶠ (x : ι × ι) in p ×ˢ p, pa x
pb : α → Prop
hpb : ∀ᶠ (y : α) in p', pb y
hpapb : ∀ {x : ι × ι}, pa x → ∀ {y : α}, pb y → (F (x, y).1.1 (x, y).2, F (x, y).1.2 (x, y).2) ∈ u
⊢ ∀ᶠ (y : γ) in comap g p', (pb ∘ g) y

Tactic:
exact eventually_comap.mpr (hpb.mono fun x hx y hy => by simp only [hx, hy, Function.comp_apply])

Result:
no goals