awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
t : Set β
f : Filter α
s : Set (α × β)
⊢ (∃ t₁ ∈ f, ∃ t₂ ∈ 𝓟 t, t₁ ×ˢ t₂ ⊆ s) ↔ ∃ t_1 ∈ f, t_1 ⊆ {a : α | ∀ b ∈ t, (a, b) ∈ s}

Tactic:
exists_congr fun u => Iff.rfl.and ⟨?_, fun h => ⟨t, mem_principal_self t, ?_⟩⟩

Premises used: Filter.mem_principal_self, Iff.rfl, exists_congr, Iff.and, And.intro, Iff.intro, Exists.intro
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
t : Set β
f : Filter α
s : Set (α × β)
refine_1 : ∀ (u : Set α), (∃ t₂ ∈ 𝓟 t, u ×ˢ t₂ ⊆ s) → u ⊆ {a : α | ∀ b ∈ t, (a, b) ∈ s}
refine_2 : ∀ (u : Set α) (h : u ⊆ {a : α | ∀ b ∈ t, (a, b) ∈ s}), u ×ˢ t ⊆ s
⊢ (∃ t₁ ∈ f, ∃ t₂ ∈ 𝓟 t, t₁ ×ˢ t₂ ⊆ s) ↔ ∃ t_1 ∈ f, t_1 ⊆ {a : α | ∀ b ∈ t, (a, b) ∈ s}

Tactic:
refine exists_congr fun u => Iff.rfl.and ⟨?_, fun h => ⟨t, mem_principal_self t, ?_⟩⟩

Premises used: Iff.rfl, exists_congr, Iff.and, Iff.intro
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
t : Set β
f : Filter α
s : Set (α × β)
u : Set α
v : Set β
v_in : v ∈ 𝓟 t
hv : u ×ˢ v ⊆ s
a : α
a_in : a ∈ u
b : β
b_in : b ∈ t
⊢ (a, b) ∈ s

Tactic:
hv (mk_mem_prod a_in <| v_in b_in)

Premises used: Set.mk_mem_prod
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
t : Set β
f : Filter α
s : Set (α × β)
u : Set α
v : Set β
v_in : v ∈ 𝓟 t
hv : u ×ˢ v ⊆ s
a : α
a_in : a ∈ u
b : β
b_in : b ∈ t
⊢ (a, b) ∈ s

Tactic:
exact hv (mk_mem_prod a_in <| v_in b_in)

Premises used: Set.mk_mem_prod
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
t : Set β
f : Filter α
s : Set (α × β)
u : Set α
h : u ⊆ {a : α | ∀ b ∈ t, (a, b) ∈ s}
x : α
y : β
hx : (x, y).1 ∈ u
hy : (x, y).2 ∈ t
⊢ (x, y) ∈ s

Tactic:
h hx y hy

Premises used: Set.Mem
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
t : Set β
f : Filter α
s : Set (α × β)
u : Set α
h : u ⊆ {a : α | ∀ b ∈ t, (a, b) ∈ s}
x : α
y : β
hx : (x, y).1 ∈ u
hy : (x, y).2 ∈ t
⊢ (x, y) ∈ s

Tactic:
exact h hx y hy
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
f : Filter α
s : Set (α × β)
rw : {a : α | ∀ (b : β), Membership.mem (γ := Set β) univ b → (a, b) ∈ s} ∈ f ↔ {a : α | ∀ (b : β), (a, b) ∈ s} ∈ f
⊢ s ∈ SProd.sprod (β := Filter β) f ⊤ ↔ {a : α | ∀ (b : β), (a, b) ∈ s} ∈ f

Tactic:
rw [← principal_univ, mem_prod_principal]

Premises used: Filter.mem_prod_principal, Filter.principal_univ
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
f : Filter α
s : Set (α × β)
⊢ {a : α | ∀ (b : β), Membership.mem (γ := Set β) univ b → (a, b) ∈ s} ∈ f ↔ {a : α | ∀ (b : β), (a, b) ∈ s} ∈ f

Tactic:
simp only [mem_univ, forall_true_left]

Premises used: forall_true_left, Set.mem_univ
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
f : Filter α
p : α × β → Prop
s : Set β
rw : {a : α | ∀ b ∈ s, Membership.mem (γ := Set (α × β)) {x : α × β | p x} (a, b)} ∈ f ↔ {x : α | ∀ y ∈ s, p (x, y)} ∈ f
⊢ (∀ᶠ (x : α × β) in f ×ˢ 𝓟 s, p x) ↔ ∀ᶠ (x : α) in f, ∀ y ∈ s, p (x, y)

Tactic:
rw [eventually_iff, eventually_iff, mem_prod_principal]

Premises used: Filter.eventually_iff, Filter.mem_prod_principal
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
f : Filter α
p : α × β → Prop
s : Set β
⊢ {a : α | ∀ b ∈ s, Membership.mem (γ := Set (α × β)) {x : α × β | p x} (a, b)} ∈ f ↔ {x : α | ∀ y ∈ s, p (x, y)} ∈ f

Tactic:
simp only [mem_setOf_eq]

Premises used: Set.mem_setOf_eq
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β × γ
b : Filter β
c : Filter γ
rw : comap f (comap Prod.fst b ⊓ comap Prod.snd c) = comap (Prod.fst ∘ f) b ⊓ comap (Prod.snd ∘ f) c
rw₁ : comap f (comap Prod.fst b) ⊓ comap f (comap Prod.snd c) = comap (Prod.fst ∘ f) b ⊓ comap (Prod.snd ∘ f) c
rw₂ : comap (Prod.fst ∘ f) b ⊓ comap f (comap Prod.snd c) = comap (Prod.fst ∘ f) b ⊓ comap (Prod.snd ∘ f) c
rw₃ rw₄ : comap (Prod.fst ∘ f) b ⊓ comap (Prod.snd ∘ f) c = comap (Prod.fst ∘ f) b ⊓ comap (Prod.snd ∘ f) c
⊢ comap f (b ×ˢ c) = comap (Prod.fst ∘ f) b ⊓ comap (Prod.snd ∘ f) c

Tactic:
rw [prod_eq_inf, comap_inf, Filter.comap_comap, Filter.comap_comap]

Premises used: Filter.prod_eq_inf, Filter.comap_inf, Filter.comap_comap
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α → β
g : γ → δ
lb : Filter β
ld : Filter δ
⊢ comap (Prod.map f g) (lb ×ˢ ld) = comap f lb ×ˢ comap g ld

Tactic:
simp [prod_eq_inf, comap_comap, Function.comp_def]

Premises used: Filter.prod_eq_inf, Function.comp_def, Filter.comap_comap
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
f : Filter α
rw : Eq (α := Filter (α × β)) (comap Prod.fst f ⊓ comap Prod.snd ⊤) (comap Prod.fst f)
rw₁ : Eq (α := Filter (α × β)) (comap Prod.fst f ⊓ ⊤) (comap Prod.fst f)
rw₂ rw₃ : Eq (α := Filter (α × β)) (comap Prod.fst f) (comap Prod.fst f)
⊢ SProd.sprod (β := Filter β) f ⊤ = comap Prod.fst f

Tactic:
rw [prod_eq_inf, comap_top, inf_top_eq]

Premises used: inf_top_eq, Filter.prod_eq_inf, Filter.comap_top
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
g : Filter β
rw : Eq (α := Filter (α × β)) (comap Prod.fst ⊤ ⊓ comap Prod.snd g) (comap Prod.snd g)
rw₁ : Eq (α := Filter (α × β)) (⊤ ⊓ comap Prod.snd g) (comap Prod.snd g)
rw₂ rw₃ : Eq (α := Filter (α × β)) (comap Prod.snd g) (comap Prod.snd g)
⊢ SProd.sprod (α := Filter α) ⊤ g = comap Prod.snd g

Tactic:
rw [prod_eq_inf, comap_top, top_inf_eq]

Premises used: Filter.prod_eq_inf, top_inf_eq, Filter.comap_top
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
f₁ f₂ : Filter α
g : Filter β
⊢ (f₁ ⊔ f₂) ×ˢ g = f₁ ×ˢ g ⊔ f₂ ×ˢ g

Tactic:
simp only [prod_eq_inf, comap_sup, inf_sup_right]

Premises used: Filter.prod_eq_inf, Filter.comap_sup, inf_sup_right
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g₁ g₂ : Filter β
⊢ f ×ˢ (g₁ ⊔ g₂) = f ×ˢ g₁ ⊔ f ×ˢ g₂

Tactic:
simp only [prod_eq_inf, comap_sup, inf_sup_left]

Premises used: Filter.prod_eq_inf, Filter.comap_sup, inf_sup_left
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
p : α × β → Prop
⊢ (∀ᶠ (x : α × β) in f ×ˢ g, p x) ↔
    ∃ (pa : α → Prop),
      (∀ᶠ (x : α) in f, pa x) ∧
        ∃ (pb : β → Prop), (∀ᶠ (y : β) in g, pb y) ∧ ∀ {x : α}, pa x → ∀ {y : β}, pb y → p (x, y)

Tactic:
simpa only [Set.prod_subset_iff] using @mem_prod_iff α β p f g

Premises used: Set.prod_subset_iff, Filter.mem_prod_iff
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
⊢ Tendsto Prod.fst (f ×ˢ g) f

Tactic:
tendsto_inf_left tendsto_comap

Premises used: Filter.tendsto_inf_left, Filter.tendsto_comap
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
⊢ Tendsto Prod.snd (f ×ˢ g) g

Tactic:
tendsto_inf_right tendsto_comap

Premises used: Filter.tendsto_comap, Filter.tendsto_inf_right
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : Filter α
g : Filter β
h : Filter γ
m : α → β × γ
H : Tendsto m f (g ×ˢ h)
⊢ Tendsto (fun (a : α) ↦ (m a).1) f g

Tactic:
tendsto_fst.comp H

Premises used: Filter.Tendsto.comp, Filter.tendsto_fst
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : Filter α
g : Filter β
h : Filter γ
m : α → β × γ
H : Tendsto m f (g ×ˢ h)
⊢ Tendsto (fun (a : α) ↦ (m a).2) f h

Tactic:
tendsto_snd.comp H

Premises used: Filter.Tendsto.comp, Filter.tendsto_snd
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : Filter α
g : Filter β
h : Filter γ
m₁ : α → β
m₂ : α → γ
h₁ : Tendsto m₁ f g
h₂ : Tendsto m₂ f h
⊢ Tendsto (fun (x : α) ↦ (m₁ x, m₂ x)) f (g ×ˢ h)

Tactic:
tendsto_inf.2 ⟨tendsto_comap_iff.2 h₁, tendsto_comap_iff.2 h₂⟩

Premises used: Iff.mpr, Filter.tendsto_inf, Filter.tendsto_comap_iff, And.intro
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
⊢ Tendsto Prod.swap (f ×ˢ g) (g ×ˢ f)

Tactic:
tendsto_snd.prodMk tendsto_fst

Premises used: Filter.Tendsto.prodMk, Prod.swap, Filter.tendsto_snd, Filter.tendsto_fst
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
la : Filter α
p : α → Prop
h : ∀ᶠ (x : α) in la, p x
lb : Filter β
⊢ ∀ᶠ (x : α × β) in la ×ˢ lb, p x.1

Tactic:
tendsto_fst.eventually h

Premises used: Filter.Tendsto.eventually, Filter.tendsto_fst
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
lb : Filter β
p : β → Prop
h : ∀ᶠ (x : β) in lb, p x
la : Filter α
⊢ ∀ᶠ (x : α × β) in la ×ˢ lb, p x.2

Tactic:
tendsto_snd.eventually h

Premises used: Filter.Tendsto.eventually, Filter.tendsto_snd
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
la : Filter α
pa : α → Prop
ha : ∀ᶠ (x : α) in la, pa x
lb : Filter β
pb : β → Prop
hb : ∀ᶠ (y : β) in lb, pb y
⊢ ∀ᶠ (p : α × β) in la ×ˢ lb, pa p.1 ∧ pb p.2

Tactic:
(ha.prod_inl lb).and (hb.prod_inr la)

Premises used: Filter.Eventually.prod_inr, Filter.Eventually.prod_inl, Filter.Eventually.and
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_6
la : Filter α
fa ga : α → γ
ha : fa =ᶠ[la] ga
lb : Filter β
fb gb : β → δ
hb : fb =ᶠ[lb] gb
⊢ Prod.map fa fb =ᶠ[la ×ˢ lb] Prod.map ga gb

Tactic:
(Eventually.prod_mk ha hb).mono fun _ h => Prod.ext h.1 h.2

Premises used: Filter.EventuallyEq, Filter.Eventually.mono, Filter.Eventually.prod_mk, And.right, And.left, Prod.ext
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_6
inst : LE γ
inst_1 : LE δ
la : Filter α
fa ga : α → γ
ha : fa ≤ᶠ[la] ga
lb : Filter β
fb gb : β → δ
hb : fb ≤ᶠ[lb] gb
⊢ Prod.map fa fb ≤ᶠ[la ×ˢ lb] Prod.map ga gb

Tactic:
Eventually.prod_mk ha hb

Premises used: Filter.Eventually.prod_mk, Filter.EventuallyLE
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
la : Filter α
lb : Filter β
p : α × β → Prop
h : ∀ᶠ (x : α × β) in la ×ˢ lb, p x
rcases :
  ∀ (pa : α → Prop) (ha : ∀ᶠ (x : α) in la, pa x) (pb : β → Prop) (hb : ∀ᶠ (y : β) in lb, pb y)
    (h : ∀ {x : α}, pa x → ∀ {y : β}, pb y → p (x, y)), ∀ᶠ (x : α) in la, ∀ᶠ (y : β) in lb, p (x, y)
⊢ ∀ᶠ (x : α) in la, ∀ᶠ (y : β) in lb, p (x, y)

Tactic:
rcases eventually_prod_iff.1 h with ⟨pa, ha, pb, hb, h⟩

Premises used: Filter.eventually_prod_iff, Iff.mp
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
la : Filter α
lb : Filter β
p : α × β → Prop
h_1 : ∀ᶠ (x : α × β) in la ×ˢ lb, p x
pa : α → Prop
ha : ∀ᶠ (x : α) in la, pa x
pb : β → Prop
hb : ∀ᶠ (y : β) in lb, pb y
h : ∀ {x : α}, pa x → ∀ {y : β}, pb y → p (x, y)
⊢ ∀ᶠ (x : α) in la, ∀ᶠ (y : β) in lb, p (x, y)

Tactic:
ha.mono fun a ha => hb.mono fun b hb => h ha hb

Premises used: Filter.Eventually.mono
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
la : Filter α
lb : Filter β
p : α × β → Prop
h_1 : ∀ᶠ (x : α × β) in la ×ˢ lb, p x
pa : α → Prop
ha : ∀ᶠ (x : α) in la, pa x
pb : β → Prop
hb : ∀ᶠ (y : β) in lb, pb y
h : ∀ {x : α}, pa x → ∀ {y : β}, pb y → p (x, y)
⊢ ∀ᶠ (x : α) in la, ∀ᶠ (y : β) in lb, p (x, y)

Tactic:
exact ha.mono fun a ha => hb.mono fun b hb => h ha hb

Premises used: Filter.Eventually.mono
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
la : Filter α
lb : Filter β
p : α → β → Prop
h : ∃ᶠ (x : α) in la, ∃ᶠ (y : β) in lb, p x y
contrapose! : ∀ (h : ∀ᶠ (x : α × β) in la ×ˢ lb, ¬p x.1 x.2), ∀ᶠ (x : α) in la, ∀ᶠ (x_1 : β) in lb, ¬p x x_1
⊢ ∃ᶠ (xy : α × β) in la ×ˢ lb, p xy.1 xy.2

Tactic:
contrapose! h
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
la : Filter α
lb : Filter β
p : α → β → Prop
h : ∀ᶠ (x : α × β) in la ×ˢ lb, ¬p x.1 x.2
⊢ ∀ᶠ (x : α) in la, ∀ᶠ (x_1 : β) in lb, ¬p x x_1

Tactic:
h.curry

Premises used: Filter.Eventually.curry
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
la : Filter α
lb : Filter β
p : α → β → Prop
h : ∀ᶠ (x : α × β) in la ×ˢ lb, ¬p x.1 x.2
⊢ ∀ᶠ (x : α) in la, ∀ᶠ (x_1 : β) in lb, ¬p x x_1

Tactic:
exact h.curry

Premises used: Filter.Eventually.curry
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
la : Filter α
lb : Filter β
p : α × β → Prop
h : ∃ᶠ (x : α) in la, ∃ᶠ (y : β) in lb, p (x, y)
⊢ ∃ᶠ (xy : α × β) in la ×ˢ lb, p xy

Tactic:
h.uncurry

Premises used: Filter.Frequently.uncurry
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
y : α → β
r : α → β → Prop
hy : Tendsto y f g
hr : ∀ᶠ (p : α × β) in f ×ˢ g, r p.1 p.2
obtain :
  ∀ (p : α → Prop) (hp : ∀ᶠ (x : α) in f, p x) (q : β → Prop) (hq : ∀ᶠ (y : β) in g, q y)
    (hr : ∀ {x : α}, p x → ∀ {y : β}, q y → r (x, y).1 (x, y).2), ∀ᶠ (x : α) in f, r x (y x)
⊢ ∀ᶠ (x : α) in f, r x (y x)

Tactic:
obtain ⟨p, hp, q, hq, hr⟩ := eventually_prod_iff.mp hr

Premises used: Filter.eventually_prod_iff, Iff.mp
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
y : α → β
r : α → β → Prop
hy : Tendsto y f g
hr_1 : ∀ᶠ (p : α × β) in f ×ˢ g, r p.1 p.2
p : α → Prop
hp_1 : ∀ᶠ (x : α) in f, p x
q : β → Prop
hq_1 : ∀ᶠ (y : β) in g, q y
hr : ∀ {x : α}, p x → ∀ {y : β}, q y → r (x, y).1 (x, y).2
a : α
hp : p a
hq : q (y a)
⊢ r a (y a)

Tactic:
hr hp hq
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
y : α → β
r : α → β → Prop
hy : Tendsto y f g
hr_1 : ∀ᶠ (p : α × β) in f ×ˢ g, r p.1 p.2
p : α → Prop
hp : ∀ᶠ (x : α) in f, p x
q : β → Prop
hq : ∀ᶠ (y : β) in g, q y
hr : ∀ {x : α}, p x → ∀ {y : β}, q y → r (x, y).1 (x, y).2
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ p x) x} x →
          Membership.mem (γ := Set α)
            {x : α |
              Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ q (y x)) x} x →
                Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ r x (y x)) x} x}
            x}
      a
h₁ h₂ : ∀ (a : α) (hp : p a) (hq : q (y a)), r a (y a)
⊢ ∀ᶠ (x : α) in f, r x (y x)

Tactic:
filter_upwards [hp, hy.eventually hq] with _ hp hq using hr hp hq

Premises used: Filter.Tendsto.eventually
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
f : Filter α
p : α × α → Prop
h : ∀ᶠ (i : α × α) in f ×ˢ f, p i
⊢ ∀ᶠ (i : α) in f, p (i, i)

Tactic:
h.image_of_prod (r := p.curry) tendsto_id

Premises used: Filter.tendsto_id, Filter.Eventually.image_of_prod
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
γ : Type u_3
f : Filter α
g : Filter γ
p : Prod.{u_1, u_3} (α × α) γ → Prop
h : ∀ᶠ (x : Prod.{u_1, u_3} (α × α) γ) in (f ×ˢ f) ×ˢ g, p x
obtain :
  ∀ (t : α × α → Prop) (ht : ∀ᶠ (x : α × α) in f ×ˢ f, t x) (s : γ → Prop) (hs : ∀ᶠ (y : γ) in g, s y)
    (hst : ∀ {x : α × α}, t x → ∀ {y : γ}, s y → p (x, y)), ∀ᶠ (x : α × γ) in f ×ˢ g, p ((x.1, x.1), x.2)
⊢ ∀ᶠ (x : α × γ) in f ×ˢ g, p ((x.1, x.1), x.2)

Tactic:
obtain ⟨t, ht, s, hs, hst⟩ := eventually_prod_iff.1 h

Premises used: Filter.eventually_prod_iff, Iff.mp
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
γ : Type u_3
f : Filter α
g : Filter γ
p : Prod.{u_1, u_3} (α × α) γ → Prop
h : ∀ᶠ (x : Prod.{u_1, u_3} (α × α) γ) in (f ×ˢ f) ×ˢ g, p x
t : α × α → Prop
ht : ∀ᶠ (x : α × α) in f ×ˢ f, t x
s : γ → Prop
hs : ∀ᶠ (y : γ) in g, s y
hst : ∀ {x : α × α}, t x → ∀ {y : γ}, s y → p (x, y)
x : α × γ
hx : t (x.1, x.1) ∧ s x.2
⊢ p ((x.1, x.1), x.2)

Tactic:
simp only [hst hx.1 hx.2]

Premises used: And.right, And.left
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
γ : Type u_3
f : Filter α
g : Filter γ
p : Prod.{u_1, u_3} (α × α) γ → Prop
h : ∀ᶠ (x : Prod.{u_1, u_3} (α × α) γ) in (f ×ˢ f) ×ˢ g, p x
t : α × α → Prop
ht : ∀ᶠ (x : α × α) in f ×ˢ f, t x
s : γ → Prop
hs : ∀ᶠ (y : γ) in g, s y
hst : ∀ {x : α × α}, t x → ∀ {y : γ}, s y → p (x, y)
⊢ ∀ᶠ (x : α × γ) in f ×ˢ g, p ((x.1, x.1), x.2)

Tactic:
exact (ht.diag_of_prod.prod_mk hs).mono fun x hx => by simp only [hst hx.1 hx.2]

Premises used: Filter.Eventually.diag_of_prod, Filter.Eventually.mono, Filter.Eventually.prod_mk
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
γ : Type u_3
f : Filter α
g : Filter γ
p : Prod.{u_1, u_3} α (γ × γ) → Prop
h : ∀ᶠ (x : Prod.{u_1, u_3} α (γ × γ)) in f ×ˢ g ×ˢ g, p x
obtain :
  ∀ (t : α → Prop) (ht : ∀ᶠ (x : α) in f, t x) (s : γ × γ → Prop) (hs : ∀ᶠ (y : γ × γ) in g ×ˢ g, s y)
    (hst : ∀ {x : α}, t x → ∀ {y : γ × γ}, s y → p (x, y)), ∀ᶠ (x : α × γ) in f ×ˢ g, p (x.1, x.2, x.2)
⊢ ∀ᶠ (x : α × γ) in f ×ˢ g, p (x.1, x.2, x.2)

Tactic:
obtain ⟨t, ht, s, hs, hst⟩ := eventually_prod_iff.1 h

Premises used: Filter.eventually_prod_iff, Iff.mp
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
γ : Type u_3
f : Filter α
g : Filter γ
p : Prod.{u_1, u_3} α (γ × γ) → Prop
h : ∀ᶠ (x : Prod.{u_1, u_3} α (γ × γ)) in f ×ˢ g ×ˢ g, p x
t : α → Prop
ht : ∀ᶠ (x : α) in f, t x
s : γ × γ → Prop
hs : ∀ᶠ (y : γ × γ) in g ×ˢ g, s y
hst : ∀ {x : α}, t x → ∀ {y : γ × γ}, s y → p (x, y)
x : α × γ
hx : t x.1 ∧ s (x.2, x.2)
⊢ p (x.1, x.2, x.2)

Tactic:
simp only [hst hx.1 hx.2]

Premises used: And.right, And.left
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
γ : Type u_3
f : Filter α
g : Filter γ
p : Prod.{u_1, u_3} α (γ × γ) → Prop
h : ∀ᶠ (x : Prod.{u_1, u_3} α (γ × γ)) in f ×ˢ g ×ˢ g, p x
t : α → Prop
ht : ∀ᶠ (x : α) in f, t x
s : γ × γ → Prop
hs : ∀ᶠ (y : γ × γ) in g ×ˢ g, s y
hst : ∀ {x : α}, t x → ∀ {y : γ × γ}, s y → p (x, y)
⊢ ∀ᶠ (x : α × γ) in f ×ˢ g, p (x.1, x.2, x.2)

Tactic:
exact (ht.prod_mk hs.diag_of_prod).mono fun x hx => by simp only [hst hx.1 hx.2]

Premises used: Filter.Eventually.diag_of_prod, Filter.Eventually.mono, Filter.Eventually.prod_mk
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
f : Filter α
⊢ Tendsto (fun (i : α) ↦ (i, i)) f (f ×ˢ f)

Tactic:
tendsto_iff_eventually.mpr fun _ hpr => hpr.diag_of_prod

Premises used: Iff.mpr, Filter.Eventually.diag_of_prod, Filter.tendsto_iff_eventually
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
inst : Nonempty ι
f : ι → Filter α
g : Filter β
⊢ SProd.sprod (α := Filter α) (⨅ (i : ι), f i) g = ⨅ (i : ι), f i ×ˢ g

Tactic:
simp only [prod_eq_inf, comap_iInf, iInf_inf]

Premises used: iInf_inf, Filter.prod_eq_inf, Filter.comap_iInf
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
inst : Nonempty ι
f : Filter α
g : ι → Filter β
⊢ SProd.sprod (β := Filter β) f (⨅ (i : ι), g i) = ⨅ (i : ι), f ×ˢ g i

Tactic:
simp only [prod_eq_inf, comap_iInf, inf_iInf]

Premises used: Filter.prod_eq_inf, Filter.comap_iInf, inf_iInf
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
f₁ f₂ : Filter α
g₁ g₂ : Filter β
hf : f₁ ≤ f₂
hg : g₁ ≤ g₂
⊢ f₁ ×ˢ g₁ ≤ f₂ ×ˢ g₂

Tactic:
inf_le_inf (comap_mono hf) (comap_mono hg)

Premises used: inf_le_inf, Set.Mem, Filter.comap_mono
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
g : Filter β
f₁ f₂ : Filter α
hf : f₁ ≤ f₂
⊢ f₁ ×ˢ g ≤ f₂ ×ˢ g

Tactic:
Filter.prod_mono hf rfl.le

Premises used: Filter.prod_mono, Eq.le, rfl
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g₁ g₂ : Filter β
hf : g₁ ≤ g₂
⊢ f ×ˢ g₁ ≤ f ×ˢ g₂

Tactic:
Filter.prod_mono rfl.le hf

Premises used: Filter.prod_mono, Eq.le, rfl
-- Module: Mathlib.Order.Filter.Prod
Goal:
α₁ : Type u
α₂ : Type v
β₁ : Type w
β₂ : Type x
f₁ : Filter α₁
f₂ : Filter α₂
m₁ : β₁ → α₁
m₂ : β₂ → α₂
⊢ comap m₁ f₁ ×ˢ comap m₂ f₂ = comap (fun (p : β₁ × β₂) ↦ (m₁ p.1, m₂ p.2)) (f₁ ×ˢ f₂)

Tactic:
simp only [prod_eq_inf, comap_comap, comap_inf, Function.comp_def]

Premises used: Filter.prod_eq_inf, Filter.comap_inf, Function.comp_def, Filter.comap_comap
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
⊢ f ×ˢ g = comap Prod.swap (g ×ˢ f)

Tactic:
simp only [prod_eq_inf, comap_comap, Function.comp_def, inf_comm, Prod.swap, comap_inf]

Premises used: Filter.prod_eq_inf, inf_comm, Filter.comap_inf, Function.comp_def, Filter.comap_comap, Prod.swap
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
rw : comap Prod.swap (g ×ˢ f) = map Prod.swap (g ×ˢ f)
rw₁ rw₂ : map Prod.swap (g ×ˢ f) = map Prod.swap (g ×ˢ f)
⊢ f ×ˢ g = map Prod.swap (g ×ˢ f)

Tactic:
rw [prod_comm', ← map_swap_eq_comap_swap]

Premises used: Filter.map_swap_eq_comap_swap, Filter.prod_comm'
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
s : Set (α × β)
simp : (∃ t₁ ∈ f, ∃ t₂ ∈ g, ∀ x ∈ t₁, ∀ y ∈ t₂, (x, y) ∈ s) ↔ ∃ t ∈ f, ∀ᶠ (y : β) in g, ∀ x ∈ t, (x, y) ∈ s
⊢ s ∈ f ×ˢ g ↔ ∃ t ∈ f, ∀ᶠ (y : β) in g, ∀ x ∈ t, (x, y) ∈ s

Tactic:
simp only [mem_prod_iff, prod_subset_iff]

Premises used: Set.prod_subset_iff, Filter.mem_prod_iff
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
s : Set (α × β)
⊢ (∃ t₁ ∈ f, ∃ t₂ ∈ g, ∀ x ∈ t₁, ∀ y ∈ t₂, (x, y) ∈ s) ↔ ∃ t ∈ f, ∀ᶠ (y : β) in g, ∀ x ∈ t, (x, y) ∈ s

Tactic:
exists_congr fun _ => Iff.rfl.and <| Iff.trans ?_ exists_mem_subset_iff

Premises used: Iff.rfl, Filter.exists_mem_subset_iff, exists_congr, Iff.and, Iff.trans
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
s : Set (α × β)
refine :
  ∀ (x : Set α),
    (∃ t₂ ∈ g, ∀ x_1 ∈ x, ∀ y ∈ t₂, (x_1, y) ∈ s) ↔ ∃ t ∈ g, t ⊆ {x_1 : β | (fun (y : β) ↦ ∀ x_2 ∈ x, (x_2, y) ∈ s) x_1}
⊢ (∃ t₁ ∈ f, ∃ t₂ ∈ g, ∀ x ∈ t₁, ∀ y ∈ t₂, (x, y) ∈ s) ↔ ∃ t ∈ f, ∀ᶠ (y : β) in g, ∀ x ∈ t, (x, y) ∈ s

Tactic:
refine exists_congr fun _ => Iff.rfl.and <| Iff.trans ?_ exists_mem_subset_iff

Premises used: Iff.rfl, Filter.exists_mem_subset_iff, exists_congr, Iff.and, Iff.trans
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
s : Set (α × β)
x : Set α
⊢ (∃ t₂ ∈ g, ∀ x_1 ∈ x, ∀ y ∈ t₂, (x_1, y) ∈ s) ↔ ∃ t ∈ g, t ⊆ {x_1 : β | (fun (y : β) ↦ ∀ x_2 ∈ x, (x_2, y) ∈ s) x_1}

Tactic:
exists_congr fun _ => Iff.rfl.and forall₂_comm

Premises used: Iff.rfl, exists_congr, Iff.and, forall₂_comm
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
s : Set (α × β)
x : Set α
⊢ (∃ t₂ ∈ g, ∀ x_1 ∈ x, ∀ y ∈ t₂, (x_1, y) ∈ s) ↔ ∃ t ∈ g, t ⊆ {x_1 : β | (fun (y : β) ↦ ∀ x_2 ∈ x, (x_2, y) ∈ s) x_1}

Tactic:
exact exists_congr fun _ => Iff.rfl.and forall₂_comm

Premises used: Iff.rfl, exists_congr, Iff.and, forall₂_comm
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
s : Set (α × β)
rw : (∃ t ∈ g, ∀ᶠ (y : α) in f, ∀ x ∈ t, (x, y) ∈ Prod.swap ⁻¹' s) ↔ ∃ t ∈ g, ∀ᶠ (x : α) in f, ∀ y ∈ t, (x, y) ∈ s
⊢ s ∈ f ×ˢ g ↔ ∃ t ∈ g, ∀ᶠ (x : α) in f, ∀ y ∈ t, (x, y) ∈ s

Tactic:
rw [prod_comm, mem_map, mem_prod_iff_left]

Premises used: Filter.prod_comm, Filter.mem_prod_iff_left, Filter.mem_map
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
s : Set (α × β)
⊢ (∃ t ∈ g, ∀ᶠ (y : α) in f, ∀ x ∈ t, (x, y) ∈ Prod.swap ⁻¹' s) ↔ ∃ t ∈ g, ∀ᶠ (x : α) in f, ∀ y ∈ t, (x, y) ∈ s

Tactic:
rfl
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
inst : g.NeBot
h : ∀ (s : Set α), s ∈ map Prod.fst (f ×ˢ g) ↔ s ∈ f
⊢ map Prod.fst (f ×ˢ g) = f

Tactic:
ext s
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
inst : g.NeBot
s : Set α
⊢ s ∈ map Prod.fst (f ×ˢ g) ↔ s ∈ f

Tactic:
simp only [mem_map, mem_prod_iff_left, mem_preimage, eventually_const, ← subset_def,
    exists_mem_subset_iff]

Premises used: Set.subset_def, Filter.exists_mem_subset_iff, Filter.eventually_const, Filter.mem_prod_iff_left, Filter.mem_map, Set.mem_preimage
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
inst : f.NeBot
rw : map (Prod.snd ∘ Prod.swap) (g ×ˢ f) = g
⊢ map Prod.snd (f ×ˢ g) = g

Tactic:
rw [prod_comm, map_map]

Premises used: Filter.map_map, Filter.prod_comm
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
inst : f.NeBot
⊢ map (Prod.snd ∘ Prod.swap) (g ×ˢ f) = g

Tactic:
apply map_fst_prod

Premises used: Filter.map_fst_prod