awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
f₁ f₂ : Filter α
g₁ g₂ : Filter β
inst : f₁.NeBot
inst_1 : g₁.NeBot
⊢ f₁ ×ˢ g₁ ≤ f₂ ×ˢ g₂ ↔ f₁ ≤ f₂ ∧ g₁ ≤ g₂

Tactic:
⟨fun h =>
    ⟨map_fst_prod f₁ g₁ ▸ tendsto_fst.mono_left h, map_snd_prod f₁ g₁ ▸ tendsto_snd.mono_left h⟩,
    fun h => prod_mono h.1 h.2⟩

Premises used: Filter.map_snd_prod, Filter.prod_mono, Eq.rec, And.right, And.left, And.intro, Iff.intro, Filter.Tendsto.mono_left, Filter.tendsto_snd, Filter.map_fst_prod, Filter.tendsto_fst
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
f₁ f₂ : Filter α
g₁ g₂ : Filter β
inst : f₁.NeBot
inst_1 : g₁.NeBot
⊢ f₁ ×ˢ g₁ = f₂ ×ˢ g₂ ↔ f₁ = f₂ ∧ g₁ = g₂

Tactic:
⟨fun h => ?_, fun h => h.1 ▸ h.2 ▸ rfl⟩

Premises used: Eq.rec, And.right, And.left, Iff.intro, rfl
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
f₁ f₂ : Filter α
g₁ g₂ : Filter β
inst : f₁.NeBot
inst_1 : g₁.NeBot
refine : ∀ (h : f₁ ×ˢ g₁ = f₂ ×ˢ g₂), f₁ = f₂ ∧ g₁ = g₂
⊢ f₁ ×ˢ g₁ = f₂ ×ˢ g₂ ↔ f₁ = f₂ ∧ g₁ = g₂

Tactic:
refine ⟨fun h => ?_, fun h => h.1 ▸ h.2 ▸ rfl⟩
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
f₁ f₂ : Filter α
g₁ g₂ : Filter β
inst : f₁.NeBot
inst_1 : g₁.NeBot
h : f₁ ×ˢ g₁ = f₂ ×ˢ g₂
⊢ f₁ ≤ f₂ ∧ g₁ ≤ g₂

Tactic:
have hle : f₁ ≤ f₂ ∧ g₁ ≤ g₂ := prod_le_prod.1 h.le
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
f₁ f₂ : Filter α
g₁ g₂ : Filter β
inst : f₁.NeBot
inst_1 : g₁.NeBot
h : f₁ ×ˢ g₁ = f₂ ×ˢ g₂
hle : f₁ ≤ f₂ ∧ g₁ ≤ g₂
⊢ f₂.NeBot

Tactic:
haveI := neBot_of_le hle.1
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
f₁ f₂ : Filter α
g₁ g₂ : Filter β
inst : f₁.NeBot
inst_1 : g₁.NeBot
h : f₁ ×ˢ g₁ = f₂ ×ˢ g₂
hle : f₁ ≤ f₂ ∧ g₁ ≤ g₂
this : f₂.NeBot
⊢ g₂.NeBot

Tactic:
haveI := neBot_of_le hle.2
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
f₁ f₂ : Filter α
g₁ g₂ : Filter β
inst : f₁.NeBot
inst_1 : g₁.NeBot
h : f₁ ×ˢ g₁ = f₂ ×ˢ g₂
hle : f₁ ≤ f₂ ∧ g₁ ≤ g₂
this_1 : f₂.NeBot
this : g₂.NeBot
⊢ f₁ = f₂ ∧ g₁ = g₂

Tactic:
⟨hle.1.antisymm <| (prod_le_prod.1 h.ge).1, hle.2.antisymm <| (prod_le_prod.1 h.ge).2⟩

Premises used: Eq.ge, LE.le.antisymm, Filter.prod_le_prod, And.right, And.left, And.intro, Iff.mp
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
f₁ f₂ : Filter α
g₁ g₂ : Filter β
inst : f₁.NeBot
inst_1 : g₁.NeBot
h : f₁ ×ˢ g₁ = f₂ ×ˢ g₂
hle : f₁ ≤ f₂ ∧ g₁ ≤ g₂
this_1 : f₂.NeBot
this : g₂.NeBot
⊢ f₁ = f₂ ∧ g₁ = g₂

Tactic:
exact ⟨hle.1.antisymm <| (prod_le_prod.1 h.ge).1, hle.2.antisymm <| (prod_le_prod.1 h.ge).2⟩
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
p : α × β → Prop
rw : (∀ᶠ (x : α × β) in map Prod.swap (g ×ˢ f), p x) ↔ ∀ᶠ (y : β × α) in g ×ˢ f, p y.swap
⊢ (∀ᶠ (x : α × β) in f ×ˢ g, p x) ↔ ∀ᶠ (y : β × α) in g ×ˢ f, p y.swap

Tactic:
rw [prod_comm]

Premises used: Filter.prod_comm
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
p : α × β → Prop
⊢ (∀ᶠ (x : α × β) in map Prod.swap (g ×ˢ f), p x) ↔ ∀ᶠ (y : β × α) in g ×ˢ f, p y.swap

Tactic:
rfl
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : Filter α
g : Filter β
h : Filter γ
inst : g.NeBot
p : α → β → Prop
q : β → γ → Prop
r : α → γ → Prop
hp : ∀ᶠ (x : α) in f, ∀ᶠ (y : β) in g, p x y
hq : ∀ᶠ (z : γ) in h, ∀ᶠ (y : β) in g, q y z
hpqr : ∀ (x : α) (y : β) (z : γ), p x y → q y z → r x z
⊢ ∀ᶠ (xz : α × γ) in f ×ˢ h, r xz.1 xz.2

Tactic:
eventually_prod_iff.mpr ⟨_, hp, _, hq, fun {x} hx {z} hz ↦ ?_⟩

Premises used: Iff.mpr, Filter.eventually_prod_iff, And.intro, Exists.intro
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : Filter α
g : Filter β
h : Filter γ
inst : g.NeBot
p : α → β → Prop
q : β → γ → Prop
r : α → γ → Prop
hp : ∀ᶠ (x : α) in f, ∀ᶠ (y : β) in g, p x y
hq : ∀ᶠ (z : γ) in h, ∀ᶠ (y : β) in g, q y z
hpqr : ∀ (x : α) (y : β) (z : γ), p x y → q y z → r x z
refine : ∀ {x : α} (hx : ∀ᶠ (y : β) in g, p x y) {z : γ} (hz : ∀ᶠ (y : β) in g, q y z), r (x, z).1 (x, z).2
⊢ ∀ᶠ (xz : α × γ) in f ×ˢ h, r xz.1 xz.2

Tactic:
refine eventually_prod_iff.mpr ⟨_, hp, _, hq, fun {x} hx {z} hz ↦ ?_⟩

Premises used: Iff.mpr, Filter.eventually_prod_iff, And.intro, Exists.intro
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : Filter α
g : Filter β
h : Filter γ
inst : g.NeBot
p : α → β → Prop
q : β → γ → Prop
r : α → γ → Prop
hp : ∀ᶠ (x : α) in f, ∀ᶠ (y : β) in g, p x y
hq : ∀ᶠ (z : γ) in h, ∀ᶠ (y : β) in g, q y z
hpqr : ∀ (x : α) (y : β) (z : γ), p x y → q y z → r x z
x : α
hx : ∀ᶠ (y : β) in g, p x y
z : γ
hz : ∀ᶠ (y : β) in g, q y z
rcases : ∀ (y : β) (hpy : p x y) (hqy : q y z), r (x, z).1 (x, z).2
⊢ r (x, z).1 (x, z).2

Tactic:
rcases (hx.and hz).exists with ⟨y, hpy, hqy⟩

Premises used: Filter.Eventually.and, Filter.Eventually.exists
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : Filter α
g : Filter β
h : Filter γ
inst : g.NeBot
p : α → β → Prop
q : β → γ → Prop
r : α → γ → Prop
hp : ∀ᶠ (x : α) in f, ∀ᶠ (y : β) in g, p x y
hq : ∀ᶠ (z : γ) in h, ∀ᶠ (y : β) in g, q y z
hpqr : ∀ (x : α) (y : β) (z : γ), p x y → q y z → r x z
x : α
hx : ∀ᶠ (y : β) in g, p x y
z : γ
hz : ∀ᶠ (y : β) in g, q y z
y : β
hpy : p x y
hqy : q y z
⊢ r (x, z).1 (x, z).2

Tactic:
hpqr x y z hpy hqy
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : Filter α
g : Filter β
h : Filter γ
inst : g.NeBot
p : α → β → Prop
q : β → γ → Prop
r : α → γ → Prop
hp : ∀ᶠ (x : α) in f, ∀ᶠ (y : β) in g, p x y
hq : ∀ᶠ (z : γ) in h, ∀ᶠ (y : β) in g, q y z
hpqr : ∀ (x : α) (y : β) (z : γ), p x y → q y z → r x z
x : α
hx : ∀ᶠ (y : β) in g, p x y
z : γ
hz : ∀ᶠ (y : β) in g, q y z
y : β
hpy : p x y
hqy : q y z
⊢ r (x, z).1 (x, z).2

Tactic:
exact hpqr x y z hpy hqy
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : Filter α
g : Filter β
h : Filter γ
inst : g.NeBot
p : α → β → Prop
q : β → γ → Prop
r : α → γ → Prop
hp : ∀ᶠ (xy : α × β) in f ×ˢ g, p xy.1 xy.2
hq : ∀ᶠ (yz : β × γ) in g ×ˢ h, q yz.1 yz.2
hpqr : ∀ (x : α) (y : β) (z : γ), p x y → q y z → r x z
⊢ ∀ᶠ (xz : α × γ) in f ×ˢ h, r xz.1 xz.2

Tactic:
hp.curry.eventually_prod_of_eventually_swap (eventually_swap_iff.mp hq |>.curry) hpqr

Premises used: Filter.eventually_swap_iff, Filter.Eventually.eventually_prod_of_eventually_swap, Filter.Eventually.curry, Iff.mp
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : Filter α
g : Filter β
h : Filter γ
simp_rw : comap (⇑(Equiv.prodAssoc α β γ).symm : (a : α × β × γ) → (α × β) × γ) ((f ×ˢ g) ×ˢ h) = f ×ˢ g ×ˢ h
simp_rw₁ :
  comap (⇑(Equiv.prodAssoc α β γ).symm : (a : α × β × γ) → (α × β) × γ)
      (comap Prod.fst (comap Prod.fst f ⊓ comap Prod.snd g) ⊓ comap Prod.snd h) =
    comap Prod.fst f ⊓ comap Prod.snd (comap Prod.fst g ⊓ comap Prod.snd h)
simp_rw₂ :
  comap (β := (α × β) × γ) (⇑(Equiv.prodAssoc α β γ).symm : (a : α × β × γ) → (α × β) × γ)
          (comap Prod.fst (comap Prod.fst f)) ⊓
        comap (β := (α × β) × γ) (⇑(Equiv.prodAssoc α β γ).symm : (a : α × β × γ) → (α × β) × γ)
          (comap Prod.fst (comap Prod.snd g)) ⊓
      comap (β := (α × β) × γ) (⇑(Equiv.prodAssoc α β γ).symm : (a : α × β × γ) → (α × β) × γ) (comap Prod.snd h) =
    comap Prod.fst f ⊓ (comap Prod.snd (comap Prod.fst g) ⊓ comap Prod.snd (comap Prod.snd h))
simp_rw₃ :
  comap
          (Function.comp (β := (α × β) × γ) (Prod.fst ∘ Prod.fst)
            (⇑(Equiv.prodAssoc α β γ).symm : (a : α × β × γ) → (α × β) × γ))
          f ⊓
        comap
          (Function.comp (β := (α × β) × γ) (Prod.snd ∘ Prod.fst)
            (⇑(Equiv.prodAssoc α β γ).symm : (a : α × β × γ) → (α × β) × γ))
          g ⊓
      comap (Function.comp (β := (α × β) × γ) Prod.snd (⇑(Equiv.prodAssoc α β γ).symm : (a : α × β × γ) → (α × β) × γ))
        h =
    comap Prod.fst f ⊓ (comap (Prod.fst ∘ Prod.snd) g ⊓ comap (Prod.snd ∘ Prod.snd) h)
simp_rw₄ :
  comap
        (Function.comp (β := (α × β) × γ) (Prod.fst ∘ Prod.fst)
          (⇑(Equiv.prodAssoc α β γ).symm : (a : α × β × γ) → (α × β) × γ))
        f ⊓
      (comap
          (Function.comp (β := (α × β) × γ) (Prod.snd ∘ Prod.fst)
            (⇑(Equiv.prodAssoc α β γ).symm : (a : α × β × γ) → (α × β) × γ))
          g ⊓
        comap
          (Function.comp (β := (α × β) × γ) Prod.snd (⇑(Equiv.prodAssoc α β γ).symm : (a : α × β × γ) → (α × β) × γ))
          h) =
    comap Prod.fst f ⊓ (comap (Prod.fst ∘ Prod.snd) g ⊓ comap (Prod.snd ∘ Prod.snd) h)
simp_rw₅ :
  Eq (α := Filter (α × β × γ))
    (comap (fun (x : α × β × γ) ↦ (((Equiv.prodAssoc α β γ).symm : (a : α × β × γ) → (α × β) × γ) x).1.1) f ⊓
      (comap (fun (x : α × β × γ) ↦ (((Equiv.prodAssoc α β γ).symm : (a : α × β × γ) → (α × β) × γ) x).1.2) g ⊓
        comap (fun (x : α × β × γ) ↦ (((Equiv.prodAssoc α β γ).symm : (a : α × β × γ) → (α × β) × γ) x).2) h))
    (comap Prod.fst f ⊓ (comap (fun (x : α × β × γ) ↦ x.2.1) g ⊓ comap (fun (x : α × β × γ) ↦ x.2.2) h))
⊢ map (⇑(Equiv.prodAssoc α β γ) : (a : (α × β) × γ) → α × β × γ) ((f ×ˢ g) ×ˢ h) = f ×ˢ g ×ˢ h

Tactic:
simp_rw [← comap_equiv_symm, prod_eq_inf, comap_inf, comap_comap, inf_assoc,
    Function.comp_def, Equiv.prodAssoc_symm_apply]

Premises used: Filter.prod_eq_inf, Filter.comap_inf, Function.comp_def, Filter.comap_comap, Equiv.prodAssoc_symm_apply, inf_assoc, Filter.comap_equiv_symm
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : Filter α
g : Filter β
h : Filter γ
simp_rw : comap (⇑(Equiv.prodAssoc α β γ) : (a : (α × β) × γ) → α × β × γ) (f ×ˢ g ×ˢ h) = (f ×ˢ g) ×ˢ h
simp_rw₁ :
  comap (⇑(Equiv.prodAssoc α β γ) : (a : (α × β) × γ) → α × β × γ)
      (comap Prod.fst f ⊓ comap Prod.snd (comap Prod.fst g ⊓ comap Prod.snd h)) =
    comap Prod.fst (comap Prod.fst f ⊓ comap Prod.snd g) ⊓ comap Prod.snd h
simp_rw₂ :
  comap (β := α × β × γ) (⇑(Equiv.prodAssoc α β γ) : (a : (α × β) × γ) → α × β × γ) (comap Prod.fst f) ⊓
      (comap (β := α × β × γ) (⇑(Equiv.prodAssoc α β γ) : (a : (α × β) × γ) → α × β × γ)
          (comap Prod.snd (comap Prod.fst g)) ⊓
        comap (β := α × β × γ) (⇑(Equiv.prodAssoc α β γ) : (a : (α × β) × γ) → α × β × γ)
          (comap Prod.snd (comap Prod.snd h))) =
    comap Prod.fst (comap Prod.fst f) ⊓ comap Prod.fst (comap Prod.snd g) ⊓ comap Prod.snd h
simp_rw₃ :
  comap (Function.comp (β := α × β × γ) Prod.fst (⇑(Equiv.prodAssoc α β γ) : (a : (α × β) × γ) → α × β × γ)) f ⊓
      (comap
          (Function.comp (β := α × β × γ) (Prod.fst ∘ Prod.snd)
            (⇑(Equiv.prodAssoc α β γ) : (a : (α × β) × γ) → α × β × γ))
          g ⊓
        comap
          (Function.comp (β := α × β × γ) (Prod.snd ∘ Prod.snd)
            (⇑(Equiv.prodAssoc α β γ) : (a : (α × β) × γ) → α × β × γ))
          h) =
    comap (Prod.fst ∘ Prod.fst) f ⊓ comap (Prod.snd ∘ Prod.fst) g ⊓ comap Prod.snd h
simp_rw₄ :
  comap (Function.comp (β := α × β × γ) Prod.fst (⇑(Equiv.prodAssoc α β γ) : (a : (α × β) × γ) → α × β × γ)) f ⊓
      (comap
          (Function.comp (β := α × β × γ) (Prod.fst ∘ Prod.snd)
            (⇑(Equiv.prodAssoc α β γ) : (a : (α × β) × γ) → α × β × γ))
          g ⊓
        comap
          (Function.comp (β := α × β × γ) (Prod.snd ∘ Prod.snd)
            (⇑(Equiv.prodAssoc α β γ) : (a : (α × β) × γ) → α × β × γ))
          h) =
    comap (Prod.fst ∘ Prod.fst) f ⊓ (comap (Prod.snd ∘ Prod.fst) g ⊓ comap Prod.snd h)
simp_rw₅ :
  Eq (α := Filter ((α × β) × γ))
    (comap (fun (x : (α × β) × γ) ↦ ((Equiv.prodAssoc α β γ : (a : (α × β) × γ) → α × β × γ) x).1) f ⊓
      (comap (fun (x : (α × β) × γ) ↦ ((Equiv.prodAssoc α β γ : (a : (α × β) × γ) → α × β × γ) x).2.1) g ⊓
        comap (fun (x : (α × β) × γ) ↦ ((Equiv.prodAssoc α β γ : (a : (α × β) × γ) → α × β × γ) x).2.2) h))
    (comap (fun (x : (α × β) × γ) ↦ x.1.1) f ⊓ (comap (fun (x : (α × β) × γ) ↦ x.1.2) g ⊓ comap Prod.snd h))
⊢ map (⇑(Equiv.prodAssoc α β γ).symm : (a : α × β × γ) → (α × β) × γ) (f ×ˢ g ×ˢ h) = (f ×ˢ g) ×ˢ h

Tactic:
simp_rw [map_equiv_symm, prod_eq_inf, comap_inf, comap_comap, inf_assoc,
    Function.comp_def, Equiv.prodAssoc_apply]

Premises used: Equiv.prodAssoc_apply, Filter.prod_eq_inf, Filter.comap_inf, Function.comp_def, Filter.comap_comap, inf_assoc, Filter.map_equiv_symm
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : Filter α
g : Filter β
h : Filter γ
⊢ Tendsto (⇑(Equiv.prodAssoc α β γ) : (a : (α × β) × γ) → α × β × γ) ((f ×ˢ g) ×ˢ h) (f ×ˢ g ×ˢ h)

Tactic:
(prod_assoc f g h).le

Premises used: Eq.le, Filter.Tendsto, Filter.prod_assoc
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : Filter α
g : Filter β
h : Filter γ
⊢ Tendsto (⇑(Equiv.prodAssoc α β γ).symm : (a : α × β × γ) → (α × β) × γ) (f ×ˢ g ×ˢ h) ((f ×ˢ g) ×ˢ h)

Tactic:
(prod_assoc_symm f g h).le

Premises used: Eq.le, Filter.Tendsto, Filter.prod_assoc_symm
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : Filter α
g : Filter β
h : Filter γ
k : Filter δ
simp_rw :
  comap
          (Function.comp (β := (α × β) × γ × δ) (Prod.fst ∘ Prod.fst) fun (p : (α × γ) × β × δ) ↦
            ((p.1.1, p.2.1), p.1.2, p.2.2))
          f ⊓
        comap
          (Function.comp (β := (α × β) × γ × δ) (Prod.snd ∘ Prod.fst) fun (p : (α × γ) × β × δ) ↦
            ((p.1.1, p.2.1), p.1.2, p.2.2))
          g ⊓
      (comap
          (Function.comp (β := (α × β) × γ × δ) (Prod.fst ∘ Prod.snd) fun (p : (α × γ) × β × δ) ↦
            ((p.1.1, p.2.1), p.1.2, p.2.2))
          h ⊓
        comap
          (Function.comp (β := (α × β) × γ × δ) (Prod.snd ∘ Prod.snd) fun (p : (α × γ) × β × δ) ↦
            ((p.1.1, p.2.1), p.1.2, p.2.2))
          k) =
    comap (Prod.fst ∘ Prod.fst) f ⊓ comap (Prod.snd ∘ Prod.fst) h ⊓
      (comap (Prod.fst ∘ Prod.snd) g ⊓ comap (Prod.snd ∘ Prod.snd) k)
⊢ map (fun (p : (α × β) × γ × δ) ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) ((f ×ˢ g) ×ˢ h ×ˢ k) = (f ×ˢ h) ×ˢ g ×ˢ k

Tactic:
simp_rw [map_swap4_eq_comap, prod_eq_inf, comap_inf, comap_comap]

Premises used: Filter.prod_eq_inf, Filter.map_swap4_eq_comap, 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 : Filter α
g : Filter β
h : Filter γ
k : Filter δ
⊢ comap
          (Function.comp (β := (α × β) × γ × δ) (Prod.fst ∘ Prod.fst) fun (p : (α × γ) × β × δ) ↦
            ((p.1.1, p.2.1), p.1.2, p.2.2))
          f ⊓
        comap
          (Function.comp (β := (α × β) × γ × δ) (Prod.snd ∘ Prod.fst) fun (p : (α × γ) × β × δ) ↦
            ((p.1.1, p.2.1), p.1.2, p.2.2))
          g ⊓
      (comap
          (Function.comp (β := (α × β) × γ × δ) (Prod.fst ∘ Prod.snd) fun (p : (α × γ) × β × δ) ↦
            ((p.1.1, p.2.1), p.1.2, p.2.2))
          h ⊓
        comap
          (Function.comp (β := (α × β) × γ × δ) (Prod.snd ∘ Prod.snd) fun (p : (α × γ) × β × δ) ↦
            ((p.1.1, p.2.1), p.1.2, p.2.2))
          k) =
    comap (Prod.fst ∘ Prod.fst) f ⊓ comap (Prod.snd ∘ Prod.fst) h ⊓
      (comap (Prod.fst ∘ Prod.snd) g ⊓ comap (Prod.snd ∘ Prod.snd) k)

Tactic:
ac_rfl
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : Filter α
g : Filter β
h : Filter γ
k : Filter δ
⊢ Tendsto (fun (p : (α × β) × γ × δ) ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) ((f ×ˢ g) ×ˢ h ×ˢ k) ((f ×ˢ h) ×ˢ g ×ˢ k)

Tactic:
map_swap4_prod.le

Premises used: Set.Mem, Eq.le, Filter.Tendsto, Filter.map_swap4_prod
-- Module: Mathlib.Order.Filter.Prod
Goal:
α₁ : Type u
α₂ : Type v
β₁ : Type w
β₂ : Type x
f₁ : Filter α₁
f₂ : Filter α₂
m₁ : α₁ → β₁
m₂ : α₂ → β₂
s : Set (β₁ × β₂)
hs : (fun (p : α₁ × α₂) ↦ (m₁ p.1, m₂ p.2)) ⁻¹' s ∈ f₁ ×ˢ f₂
s₁ : Set α₁
hs₁ : s₁ ∈ f₁
s₂ : Set α₂
hs₂ : s₂ ∈ f₂
h : s₁ ×ˢ s₂ ⊆ (fun (p : α₁ × α₂) ↦ (m₁ p.1, m₂ p.2)) ⁻¹' s
rwa : (fun (p : α₁ × α₂) ↦ (m₁ p.1, m₂ p.2)) '' s₁ ×ˢ s₂ ⊆ s
rwa₁ rwa₂ rwa₃ rwa₄ : s₁ ×ˢ s₂ ⊆ (fun (p : α₁ × α₂) ↦ (m₁ p.1, m₂ p.2)) ⁻¹' s
⊢ (m₁ '' s₁) ×ˢ (m₂ '' s₂) ⊆ s

Tactic:
rwa [prod_image_image_eq, image_subset_iff]

Premises used: Set.prod_image_image_eq, Set.image_subset_iff
-- Module: Mathlib.Order.Filter.Prod
Goal:
α₁ : Type u_6
α₂ : Type u_7
β₁ : Type u_8
β₂ : Type u_9
f : α₁ → α₂
g : β₁ → β₂
F : Filter α₁
G : Filter β₁
⊢ map f F ×ˢ map g G = map (Prod.map f g) (F ×ˢ G)

Tactic:
prod_map_map_eq

Premises used: Prod.map, Filter.prod_map_map_eq
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
F : Filter α
G : Filter γ
rw : map f F ×ˢ G = map f F ×ˢ map id G
rw₁ rw₂ : map f F ×ˢ G = map f F ×ˢ G
⊢ map f F ×ˢ G = map (Prod.map f id) (F ×ˢ G)

Tactic:
rw [← prod_map_map_eq', map_id]

Premises used: Filter.prod_map_map_eq', Filter.map_id
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : β → γ
F : Filter α
G : Filter β
rw : F ×ˢ map f G = map id F ×ˢ map f G
rw₁ rw₂ : F ×ˢ map f G = F ×ˢ map f G
⊢ F ×ˢ map f G = map (Prod.map id f) (F ×ˢ G)

Tactic:
rw [← prod_map_map_eq', map_id]

Premises used: Filter.prod_map_map_eq', Filter.map_id
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
f : Filter (α × β)
⊢ f ≤ map Prod.fst f ×ˢ map Prod.snd f

Tactic:
le_inf le_comap_map le_comap_map

Premises used: Set.Mem, le_inf, Filter.le_comap_map
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_6
f : α → γ
g : β → δ
a : Filter α
b : Filter β
c : Filter γ
d : Filter δ
hf : Tendsto f a c
hg : Tendsto g b d
rw : map f a ×ˢ map g b ≤ c ×ˢ d
⊢ Tendsto (Prod.map f g) (a ×ˢ b) (c ×ˢ d)

Tactic:
rw [Tendsto, Prod.map_def, ← prod_map_map_eq]

Premises used: Filter.Tendsto, Filter.prod_map_map_eq, Prod.map_def
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_6
f : α → γ
g : β → δ
a : Filter α
b : Filter β
c : Filter γ
d : Filter δ
hf : Tendsto f a c
hg : Tendsto g b d
⊢ map f a ×ˢ map g b ≤ c ×ˢ d

Tactic:
Filter.prod_mono hf hg

Premises used: Filter.prod_mono
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_6
f : α → γ
g : β → δ
a : Filter α
b : Filter β
c : Filter γ
d : Filter δ
hf : Tendsto f a c
hg : Tendsto g b d
⊢ map f a ×ˢ map g b ≤ c ×ˢ d

Tactic:
exact Filter.prod_mono hf hg

Premises used: Filter.prod_mono
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
m : α × β → γ
f : Filter α
g : Filter β
simp : ∀ (s : Set γ), (∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ ×ˢ t₂ ⊆ m ⁻¹' s) ↔ ∃ t ∈ g, ∃ x ∈ f, ∀ x_1 ∈ x, ∀ y ∈ t, m (x_1, y) ∈ s
⊢ map m (f ×ˢ g) = seq (map (fun (a : α) (b : β) ↦ m (a, b)) f) g

Tactic:
simp only [Filter.ext_iff, mem_map, mem_prod_iff, mem_map_seq_iff, exists_and_left]

Premises used: exists_and_left, Filter.ext_iff, Filter.mem_prod_iff, Filter.mem_map_seq_iff, Filter.mem_map
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
m : α × β → γ
f : Filter α
g : Filter β
s : Set γ
mp : (∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ ×ˢ t₂ ⊆ m ⁻¹' s) → ∃ t ∈ g, ∃ x ∈ f, ∀ x_1 ∈ x, ∀ y ∈ t, m (x_1, y) ∈ s
mpr : (∃ t ∈ g, ∃ x ∈ f, ∀ x_1 ∈ x, ∀ y ∈ t, m (x_1, y) ∈ s) → ∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ ×ˢ t₂ ⊆ m ⁻¹' s
⊢ (∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ ×ˢ t₂ ⊆ m ⁻¹' s) ↔ ∃ t ∈ g, ∃ x ∈ f, ∀ x_1 ∈ x, ∀ y ∈ t, m (x_1, y) ∈ s

Tactic:
constructor
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
m : α × β → γ
f : Filter α
g : Filter β
s : Set γ
⊢ (∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ ×ˢ t₂ ⊆ m ⁻¹' s) → ∃ t ∈ g, ∃ x ∈ f, ∀ x_1 ∈ x, ∀ y ∈ t, m (x_1, y) ∈ s

Tactic:
fun ⟨t, ht, s, hs, h⟩ => ⟨s, hs, t, ht, fun x hx y hy => @h ⟨x, y⟩ ⟨hx, hy⟩⟩

Premises used: Membership.mem, Exists, And, And.intro, Exists.intro, _private.0.Filter.map_prod.match_3
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
m : α × β → γ
f : Filter α
g : Filter β
s : Set γ
⊢ (∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ ×ˢ t₂ ⊆ m ⁻¹' s) → ∃ t ∈ g, ∃ x ∈ f, ∀ x_1 ∈ x, ∀ y ∈ t, m (x_1, y) ∈ s

Tactic:
exact fun ⟨t, ht, s, hs, h⟩ => ⟨s, hs, t, ht, fun x hx y hy => @h ⟨x, y⟩ ⟨hx, hy⟩⟩
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
m : α × β → γ
f : Filter α
g : Filter β
s : Set γ
⊢ (∃ t ∈ g, ∃ x ∈ f, ∀ x_1 ∈ x, ∀ y ∈ t, m (x_1, y) ∈ s) → ∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ ×ˢ t₂ ⊆ m ⁻¹' s

Tactic:
fun ⟨s, hs, t, ht, h⟩ => ⟨t, ht, s, hs, fun ⟨x, y⟩ ⟨hx, hy⟩ => h x hx y hy⟩

Premises used: SProd.sprod, _private.0.Filter.map_prod.match_5, _private.0.Filter.map_prod.match_4, Membership.mem, Exists, Prod.mk, HasSubset.Subset, And, Set.preimage, And.intro, Exists.intro, _private.0.Filter.map_prod.match_6
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
m : α × β → γ
f : Filter α
g : Filter β
s : Set γ
⊢ (∃ t ∈ g, ∃ x ∈ f, ∀ x_1 ∈ x, ∀ y ∈ t, m (x_1, y) ∈ s) → ∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ ×ˢ t₂ ⊆ m ⁻¹' s

Tactic:
exact fun ⟨s, hs, t, ht, h⟩ => ⟨t, ht, s, hs, fun ⟨x, y⟩ ⟨hx, hy⟩ => h x hx y hy⟩
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
⊢ f ×ˢ g = seq (map Prod.mk f) g

Tactic:
f.map_prod id g

Premises used: Set.Mem, Filter.map, setOf, id, Filter.map_prod, Set.preimage
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
f₁ f₂ : Filter α
g₁ g₂ : Filter β
⊢ f₁ ×ˢ g₁ ⊓ f₂ ×ˢ g₂ = (f₁ ⊓ f₂) ×ˢ (g₁ ⊓ g₂)

Tactic:
simp only [prod_eq_inf, comap_inf, inf_comm, inf_assoc, inf_left_comm]

Premises used: Filter.prod_eq_inf, inf_comm, Filter.comap_inf, inf_assoc, inf_left_comm
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
g : Filter β
f₁ f₂ : Filter α
rw : (f₁ ⊓ f₂) ×ˢ g = (f₁ ⊓ f₂) ×ˢ (g ⊓ g)
rw₁ rw₂ : (f₁ ⊓ f₂) ×ˢ g = (f₁ ⊓ f₂) ×ˢ g
⊢ (f₁ ⊓ f₂) ×ˢ g = f₁ ×ˢ g ⊓ f₂ ×ˢ g

Tactic:
rw [prod_inf_prod, inf_idem]

Premises used: Filter.prod_inf_prod, inf_idem
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g₁ g₂ : Filter β
rw : f ×ˢ (g₁ ⊓ g₂) = (f ⊓ f) ×ˢ (g₁ ⊓ g₂)
rw₁ rw₂ : f ×ˢ (g₁ ⊓ g₂) = f ×ˢ (g₁ ⊓ g₂)
⊢ f ×ˢ (g₁ ⊓ g₂) = f ×ˢ g₁ ⊓ f ×ˢ g₂

Tactic:
rw [prod_inf_prod, inf_idem]

Premises used: Filter.prod_inf_prod, inf_idem
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
simp : Prod.fst ⁻¹' s ∩ Prod.snd ⁻¹' t = s ×ˢ t
⊢ 𝓟 s ×ˢ 𝓟 t = 𝓟 (s ×ˢ t)

Tactic:
simp only [prod_eq_inf, comap_principal, principal_eq_iff_eq, comap_principal, inf_principal]

Premises used: Filter.inf_principal, Filter.prod_eq_inf, Filter.comap_principal, Filter.principal_eq_iff_eq
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ Prod.fst ⁻¹' s ∩ Prod.snd ⁻¹' t = s ×ˢ t

Tactic:
rfl
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
a : α
f : Filter β
rw : seq (map Prod.mk (pure a)) f = map (Prod.mk a) f
rw₁ : seq (pure (Prod.mk a)) f = map (Prod.mk a) f
rw₂ rw₃ : map (Prod.mk a) f = map (Prod.mk a) f
⊢ SProd.sprod (α := Filter α) (pure a) f = map (Prod.mk a) f

Tactic:
rw [prod_eq, map_pure, pure_seq_eq_map]

Premises used: Filter.prod_eq, Filter.map_pure, Filter.pure_seq_eq_map
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
a : α
B : Filter β
rw : map (Function.uncurry f) (map (Prod.mk a) B) = map (f a) B
⊢ map (Function.uncurry f) (SProd.sprod (α := Filter α) (pure a) B) = map (f a) B

Tactic:
rw [Filter.pure_prod]

Premises used: Filter.pure_prod
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
a : α
B : Filter β
⊢ map (Function.uncurry f) (map (Prod.mk a) B) = map (f a) B

Tactic:
rfl
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
f : Filter α
b : β
rw : Eq (α := Filter (α × β)) (map ((fun (g : β → α × β) ↦ g b) ∘ Prod.mk) f) (map (fun (a : α) ↦ (a, b)) f)
⊢ SProd.sprod (β := Filter β) f (pure b) = map (fun (a : α) ↦ (a, b)) f

Tactic:
rw [prod_eq, seq_pure, map_map]

Premises used: Filter.prod_eq, Filter.seq_pure, Filter.map_map
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
f : Filter α
b : β
⊢ Eq (α := Filter (α × β)) (map ((fun (g : β → α × β) ↦ g b) ∘ Prod.mk) f) (map (fun (a : α) ↦ (a, b)) f)

Tactic:
rfl
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
a : α
b : β
⊢ SProd.sprod (α := Filter α) (β := Filter β) (pure a) (pure b) = pure (a, b)

Tactic:
simp