awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
simp_rw : ∅ ∈ f ×ˢ g ↔ ∅ ∈ f ∨ ∅ ∈ g
simp_rw₁ : (∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ ×ˢ t₂ ⊆ ∅) ↔ ∅ ∈ f ∨ ∅ ∈ g
simp_rw₂ : (∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ ×ˢ t₂ = ∅) ↔ ∅ ∈ f ∨ ∅ ∈ g
simp_rw₃ : (∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ = ∅ ∨ t₂ = ∅) ↔ ∅ ∈ f ∨ ∅ ∈ g
simp_rw₄ : (∃ (t₁ : Set α) (_ : t₁ ∈ f) (t₂ : Set β) (_ : t₂ ∈ g), t₁ = ∅ ∨ t₂ = ∅) ↔ ∅ ∈ f ∨ ∅ ∈ g
simp_rw₅ :
  (∃ (x : { a : Set α // a ∈ f }) (x_1 : { a : Set β // a ∈ g }), (↑x : Set α) = ∅ ∨ (↑x_1 : Set β) = ∅) ↔ ∅ ∈ f ∨ ∅ ∈ g
simp_rw₆ :
  ((∃ (x : { a : Set α // a ∈ f }) (x_1 : { a : Set β // a ∈ g }), (↑x : Set α) = ∅) ∨
      ∃ (x : { a : Set α // a ∈ f }) (x : { a : Set β // a ∈ g }), (↑x : Set β) = ∅) ↔
    ∅ ∈ f ∨ ∅ ∈ g
simp_rw₇ :
  ((∃ (x : { a : Set α // a ∈ f }), (↑x : Set α) = ∅) ∨ ∃ (x : { a : Set β // a ∈ g }), (↑x : Set β) = ∅) ↔
    ∅ ∈ f ∨ ∅ ∈ g
simp_rw₈ : ((∃ (a : Set α) (_ : a ∈ f), a = ∅) ∨ ∃ (a : Set β) (_ : a ∈ g), a = ∅) ↔ ∅ ∈ f ∨ ∅ ∈ g
simp_rw₉ : ((∃ a ∈ f, a = ∅) ∨ ∃ a ∈ g, a = ∅) ↔ ∅ ∈ f ∨ ∅ ∈ g
⊢ f ×ˢ g = ⊥ ↔ f = ⊥ ∨ g = ⊥

Tactic:
simp_rw [← empty_mem_iff_bot, mem_prod_iff, subset_empty_iff, prod_eq_empty_iff, ← exists_prop,
    Subtype.exists', exists_or, exists_const, Subtype.exists, exists_prop, exists_eq_right]

Premises used: exists_or, Subtype.exists, exists_eq_right, Subtype.exists', exists_prop, Filter.empty_mem_iff_bot, exists_const, Set.prod_eq_empty_iff, Set.subset_empty_iff, Filter.mem_prod_iff
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
f : Filter α
⊢ SProd.sprod (β := Filter β) f ⊥ = ⊥

Tactic:
prod_eq_bot.2 <| Or.inr rfl

Premises used: Iff.mpr, Filter.prod_eq_bot, Or.inr, rfl
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
g : Filter β
⊢ SProd.sprod (α := Filter α) ⊥ g = ⊥

Tactic:
prod_eq_bot.2 <| Or.inl rfl

Premises used: Iff.mpr, Or.inl, Filter.prod_eq_bot, rfl
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
⊢ (f ×ˢ g).NeBot ↔ f.NeBot ∧ g.NeBot

Tactic:
simp only [neBot_iff, Ne, prod_eq_bot, not_or]

Premises used: Filter.neBot_iff, Ne, not_or, Filter.prod_eq_bot
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
hf : f.NeBot
hg : g.NeBot
⊢ (f ×ˢ g).NeBot

Tactic:
prod_neBot.2 ⟨hf, hg⟩

Premises used: Iff.mpr, Filter.prod_neBot, And.intro
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f : Filter α
g : Filter β
hf : f.NeBot
hg : g.NeBot
⊢ (f ×ˢ g).NeBot

Tactic:
hf.prod hg

Premises used: Filter.NeBot.prod
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
f' : Filter α
g' : Filter β
⊢ Disjoint (f ×ˢ g) (f' ×ˢ g') ↔ Disjoint f f' ∨ Disjoint g g'

Tactic:
simp only [disjoint_iff, prod_inf_prod, prod_eq_bot]

Premises used: Filter.prod_inf_prod, disjoint_iff, Filter.prod_eq_bot
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
p : α → Prop
q : β → Prop
simp :
  (f ×ˢ g ⊓ 𝓟 {x : α × β | p x.1 ∧ q x.2}).NeBot ↔
    (f ×ˢ g ⊓ 𝓟 (SProd.sprod (α := Set α) (β := Set β) {a : α | p a} {b : β | q b})).NeBot
⊢ (∃ᶠ (x : α × β) in f ×ˢ g, p x.1 ∧ q x.2) ↔ (∃ᶠ (a : α) in f, p a) ∧ ∃ᶠ (b : β) in g, q b

Tactic:
simp only [frequently_iff_neBot, ← prod_neBot, ← prod_inf_prod, prod_principal_principal]

Premises used: Filter.prod_inf_prod, Filter.prod_principal_principal, Filter.prod_neBot, Filter.frequently_iff_neBot
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
p : α → Prop
q : β → Prop
⊢ (f ×ˢ g ⊓ 𝓟 {x : α × β | p x.1 ∧ q x.2}).NeBot ↔
    (f ×ˢ g ⊓ 𝓟 (SProd.sprod (α := Set α) (β := Set β) {a : α | p a} {b : β | q b})).NeBot

Tactic:
rfl
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α × β → γ
x : Filter α
y : Filter β
z : Filter γ
⊢ Tendsto f (x ×ˢ y) z ↔ ∀ W ∈ z, ∃ U ∈ x, ∃ V ∈ y, ∀ (x : α) (y : β), x ∈ U → y ∈ V → f (x, y) ∈ W

Tactic:
simp only [tendsto_def, mem_prod_iff, prod_sub_preimage_iff]

Premises used: Filter.tendsto_def, Set.prod_sub_preimage_iff, Filter.mem_prod_iff
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : Filter α
g : Filter β
g' : Filter γ
s : α → β × γ
⊢ Tendsto s f (g ×ˢ g') ↔ Tendsto (fun (n : α) ↦ (s n).1) f g ∧ Tendsto (fun (n : α) ↦ (s n).2) f g'

Tactic:
simp only [prod_eq_inf, tendsto_inf, tendsto_comap_iff, Function.comp_def]

Premises used: Filter.tendsto_inf, Filter.prod_eq_inf, Filter.tendsto_comap_iff, Function.comp_def
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
f : Filter (α × β)
g : Filter α
g' : Filter β
⊢ f ≤ g ×ˢ g' ↔ Tendsto Prod.fst f g ∧ Tendsto Prod.snd f g'

Tactic:
tendsto_prod_iff'

Premises used: Set.Mem, setOf, Filter.tendsto_prod_iff', Set.preimage, Filter.Tendsto
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
rw : f.coprod g = comap Prod.fst f ⊔ comap Prod.snd g
⊢ f.coprod g = SProd.sprod (β := Filter β) f ⊤ ⊔ SProd.sprod (α := Filter α) ⊤ g

Tactic:
rw [prod_top, top_prod]

Premises used: Filter.top_prod, Filter.prod_top
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
⊢ f.coprod g = comap Prod.fst f ⊔ comap Prod.snd g

Tactic:
rfl
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
s : Set (α × β)
f : Filter α
g : Filter β
⊢ s ∈ f.coprod g ↔ (∃ t₁ ∈ f, Prod.fst ⁻¹' t₁ ⊆ s) ∧ ∃ t₂ ∈ g, Prod.snd ⁻¹' t₂ ⊆ s

Tactic:
simp [Filter.coprod]

Premises used: Filter.coprod
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
l : Filter β
⊢ Eq (α := Filter (α × β)) (Filter.coprod ⊥ l) (comap Prod.snd l)

Tactic:
simp [Filter.coprod]

Premises used: Filter.coprod
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
l : Filter α
⊢ Eq (α := Filter (α × β)) (l.coprod ⊥) (comap Prod.fst l)

Tactic:
simp [Filter.coprod]

Premises used: Filter.coprod
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
⊢ Eq (α := Filter (α × β)) (Filter.coprod ⊥ ⊥) ⊥

Tactic:
simp
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
s : Set (α × β)
la : Filter α
lb : Filter β
⊢ sᶜ ∈ la.coprod lb ↔ (Prod.fst '' s)ᶜ ∈ la ∧ (Prod.snd '' s)ᶜ ∈ lb

Tactic:
simp only [Filter.coprod, mem_sup, compl_mem_comap]

Premises used: Filter.mem_sup, Filter.compl_mem_comap, Filter.coprod
-- 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₁.coprod g₁ ≤ f₂.coprod g₂

Tactic:
sup_le_sup (comap_mono hf) (comap_mono hg)

Premises used: sup_le_sup, Set.Mem, Filter.comap_mono
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
⊢ (f.coprod g).NeBot ↔ f.NeBot ∧ Nonempty β ∨ Nonempty α ∧ g.NeBot

Tactic:
simp [Filter.coprod]

Premises used: Filter.coprod
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
inst : f.NeBot
inst_1 : Nonempty β
⊢ (f.coprod g).NeBot

Tactic:
coprod_neBot_iff.2 (Or.inl ⟨‹_›, ‹_›⟩)

Premises used: Iff.mpr, And.intro, Or.inl, Filter.coprod_neBot_iff
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
inst : g.NeBot
inst_1 : Nonempty α
⊢ (f.coprod g).NeBot

Tactic:
coprod_neBot_iff.2 (Or.inr ⟨‹_›, ‹_›⟩)

Premises used: Iff.mpr, And.intro, Or.inr, Filter.coprod_neBot_iff
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
f₁ f₂ : Filter α
g₁ g₂ : Filter β
rw rw₁ :
  (SProd.sprod (β := Filter β) f₁ ⊤ ⊔ SProd.sprod (α := Filter α) ⊤ g₁) ⊓ f₂ ×ˢ g₂ =
    (SProd.sprod (β := Filter β) f₁ ⊤ ⊔ SProd.sprod (α := Filter α) ⊤ g₁) ⊓ f₂ ×ˢ g₂
⊢ f₁.coprod g₁ ⊓ f₂ ×ˢ g₂ = (SProd.sprod (β := Filter β) f₁ ⊤ ⊔ SProd.sprod (α := Filter α) ⊤ g₁) ⊓ f₂ ×ˢ g₂

Tactic:
rw [coprod_eq_prod_top_sup_top_prod]

Premises used: Filter.coprod_eq_prod_top_sup_top_prod
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
f₁ f₂ : Filter α
g₁ g₂ : Filter β
⊢ SProd.sprod (β := Filter β) f₁ ⊤ ⊓ f₂ ×ˢ g₂ ⊔ SProd.sprod (α := Filter α) ⊤ g₁ ⊓ f₂ ×ˢ g₂ =
    (f₁ ⊓ f₂) ×ˢ g₂ ⊔ f₂ ×ˢ (g₁ ⊓ g₂)

Tactic:
simp [prod_inf_prod]

Premises used: Filter.prod_inf_prod
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
rw : comap Prod.fst (𝓟 s) ⊔ comap Prod.snd (𝓟 t) = 𝓟 (sᶜ ×ˢ tᶜ)ᶜ
rw₁ : 𝓟 (Prod.fst ⁻¹' s) ⊔ comap Prod.snd (𝓟 t) = 𝓟 (sᶜ ×ˢ tᶜ)ᶜ
rw₂ : 𝓟 (Prod.fst ⁻¹' s) ⊔ 𝓟 (Prod.snd ⁻¹' t) = 𝓟 (sᶜ ×ˢ tᶜ)ᶜ
rw₃ : 𝓟 (Prod.fst ⁻¹' s ∪ Prod.snd ⁻¹' t) = 𝓟 (sᶜ ×ˢ tᶜ)ᶜ
rw₄ : 𝓟 (Prod.fst ⁻¹' s ∪ Prod.snd ⁻¹' t) = 𝓟 (Prod.fst ⁻¹' sᶜ ∩ Prod.snd ⁻¹' tᶜ)ᶜ
rw₅ : 𝓟 (Prod.fst ⁻¹' s ∪ Prod.snd ⁻¹' t) = 𝓟 ((Prod.fst ⁻¹' sᶜ)ᶜ ∪ (Prod.snd ⁻¹' tᶜ)ᶜ)
rw₆ : 𝓟 (Prod.fst ⁻¹' s ∪ Prod.snd ⁻¹' t) = 𝓟 ((Prod.fst ⁻¹' s)ᶜᶜ ∪ (Prod.snd ⁻¹' tᶜ)ᶜ)
rw₇ : 𝓟 (Prod.fst ⁻¹' s ∪ Prod.snd ⁻¹' t) = 𝓟 ((Prod.fst ⁻¹' s)ᶜᶜ ∪ (Prod.snd ⁻¹' t)ᶜᶜ)
rw₈ : 𝓟 (Prod.fst ⁻¹' s ∪ Prod.snd ⁻¹' t) = 𝓟 (Prod.fst ⁻¹' s ∪ (Prod.snd ⁻¹' t)ᶜᶜ)
rw₉ rw₁₀ : 𝓟 (Prod.fst ⁻¹' s ∪ Prod.snd ⁻¹' t) = 𝓟 (Prod.fst ⁻¹' s ∪ Prod.snd ⁻¹' t)
⊢ (𝓟 s).coprod (𝓟 t) = 𝓟 (sᶜ ×ˢ tᶜ)ᶜ

Tactic:
rw [Filter.coprod, comap_principal, comap_principal, sup_principal, Set.prod_eq, compl_inter,
    preimage_compl, preimage_compl, compl_compl, compl_compl]

Premises used: Filter.sup_principal, compl_compl, Set.compl_inter, Set.prod_eq, Filter.comap_principal, Set.preimage_compl, Filter.coprod
-- Module: Mathlib.Order.Filter.Prod
Goal:
α₁ : Type u
α₂ : Type v
β₁ : Type w
β₂ : Type x
f₁ : Filter α₁
f₂ : Filter α₂
m₁ : α₁ → β₁
m₂ : α₂ → β₂
s : Set (β₁ × β₂)
simp :
  ((∃ (t₁ : Set β₁), m₁ ⁻¹' t₁ ∈ f₁ ∧ Prod.fst ⁻¹' t₁ ⊆ s) ∧ ∃ (t₂ : Set β₂), m₂ ⁻¹' t₂ ∈ f₂ ∧ Prod.snd ⁻¹' t₂ ⊆ s) →
    (∃ t₁ ∈ f₁, Prod.fst ⁻¹' t₁ ⊆ Prod.map m₁ m₂ ⁻¹' s) ∧ ∃ t₂ ∈ f₂, Prod.snd ⁻¹' t₂ ⊆ Prod.map m₁ m₂ ⁻¹' s
⊢ s ∈ (map m₁ f₁).coprod (map m₂ f₂) → s ∈ map (Prod.map m₁ m₂) (f₁.coprod f₂)

Tactic:
simp only [mem_map, mem_coprod_iff]

Premises used: Filter.mem_coprod_iff, Filter.mem_map
-- Module: Mathlib.Order.Filter.Prod
Goal:
α₁ : Type u
α₂ : Type v
β₁ : Type w
β₂ : Type x
f₁ : Filter α₁
f₂ : Filter α₂
m₁ : α₁ → β₁
m₂ : α₂ → β₂
s : Set (β₁ × β₂)
u₁ : Set β₁
hu₁ : m₁ ⁻¹' u₁ ∈ f₁
h₁ : Prod.fst ⁻¹' u₁ ⊆ s
u₂ : Set β₂
hu₂ : m₂ ⁻¹' u₂ ∈ f₂
h₂ : Prod.snd ⁻¹' u₂ ⊆ s
⊢ (∃ t₁ ∈ f₁, Prod.fst ⁻¹' t₁ ⊆ Prod.map m₁ m₂ ⁻¹' s) ∧ ∃ t₂ ∈ f₂, Prod.snd ⁻¹' t₂ ⊆ Prod.map m₁ m₂ ⁻¹' s

Tactic:
⟨⟨m₁ ⁻¹' u₁, hu₁, fun _ hx => h₁ ?_⟩, ⟨m₂ ⁻¹' u₂, hu₂, fun _ hx => h₂ ?_⟩⟩

Premises used: Set.preimage, And.intro, Exists.intro
-- Module: Mathlib.Order.Filter.Prod
Goal:
α₁ : Type u
α₂ : Type v
β₁ : Type w
β₂ : Type x
f₁ : Filter α₁
f₂ : Filter α₂
m₁ : α₁ → β₁
m₂ : α₂ → β₂
s : Set (β₁ × β₂)
u₁ : Set β₁
hu₁ : m₁ ⁻¹' u₁ ∈ f₁
h₁ : Prod.fst ⁻¹' u₁ ⊆ s
u₂ : Set β₂
hu₂ : m₂ ⁻¹' u₂ ∈ f₂
h₂ : Prod.snd ⁻¹' u₂ ⊆ s
refine_1 :
  ∀ (x : α₁ × α₂) (hx : Membership.mem (γ := Set (α₁ × α₂)) (Prod.fst ⁻¹' m₁ ⁻¹' u₁) x),
    Membership.mem (γ := Set (β₁ × β₂)) (Prod.fst ⁻¹' u₁) (Prod.map m₁ m₂ x)
refine_2 :
  ∀ (x : α₁ × α₂) (hx : Membership.mem (γ := Set (α₁ × α₂)) (Prod.snd ⁻¹' m₂ ⁻¹' u₂) x),
    Membership.mem (γ := Set (β₁ × β₂)) (Prod.snd ⁻¹' u₂) (Prod.map m₁ m₂ x)
⊢ (∃ t₁ ∈ f₁, Prod.fst ⁻¹' t₁ ⊆ Prod.map m₁ m₂ ⁻¹' s) ∧ ∃ t₂ ∈ f₂, Prod.snd ⁻¹' t₂ ⊆ Prod.map m₁ m₂ ⁻¹' s

Tactic:
refine ⟨⟨m₁ ⁻¹' u₁, hu₁, fun _ hx => h₁ ?_⟩, ⟨m₂ ⁻¹' u₂, hu₂, fun _ hx => h₂ ?_⟩⟩
-- Module: Mathlib.Order.Filter.Prod
Goal:
α₁ : Type u
α₂ : Type v
β₁ : Type w
β₂ : Type x
f₁ : Filter α₁
f₂ : Filter α₂
m₁ : α₁ → β₁
m₂ : α₂ → β₂
s : Set (β₁ × β₂)
u₁ : Set β₁
hu₁ : m₁ ⁻¹' u₁ ∈ f₁
h₁ : Prod.fst ⁻¹' u₁ ⊆ s
u₂ : Set β₂
hu₂ : m₂ ⁻¹' u₂ ∈ f₂
h₂ : Prod.snd ⁻¹' u₂ ⊆ s
x : α₁ × α₂
hx : Membership.mem (γ := Set (α₁ × α₂)) (Prod.fst ⁻¹' m₁ ⁻¹' u₁) x
⊢ Membership.mem (γ := Set (α₁ × α₂)) (Prod.fst ⁻¹' m₁ ⁻¹' u₁) x

Tactic:
hx
-- Module: Mathlib.Order.Filter.Prod
Goal:
α₁ : Type u
α₂ : Type v
β₁ : Type w
β₂ : Type x
f₁ : Filter α₁
f₂ : Filter α₂
m₁ : α₁ → β₁
m₂ : α₂ → β₂
s : Set (β₁ × β₂)
u₁ : Set β₁
hu₁ : m₁ ⁻¹' u₁ ∈ f₁
h₁ : Prod.fst ⁻¹' u₁ ⊆ s
u₂ : Set β₂
hu₂ : m₂ ⁻¹' u₂ ∈ f₂
h₂ : Prod.snd ⁻¹' u₂ ⊆ s
x : α₁ × α₂
hx : Membership.mem (γ := Set (α₁ × α₂)) (Prod.fst ⁻¹' m₁ ⁻¹' u₁) x
⊢ Membership.mem (γ := Set (β₁ × β₂)) (Prod.fst ⁻¹' u₁) (Prod.map m₁ m₂ x)

Tactic:
convert!
    hx
-- Module: Mathlib.Order.Filter.Prod
Goal:
α₁ : Type u
α₂ : Type v
β₁ : Type w
β₂ : Type x
f₁ : Filter α₁
f₂ : Filter α₂
m₁ : α₁ → β₁
m₂ : α₂ → β₂
s : Set (β₁ × β₂)
u₁ : Set β₁
hu₁ : m₁ ⁻¹' u₁ ∈ f₁
h₁ : Prod.fst ⁻¹' u₁ ⊆ s
u₂ : Set β₂
hu₂ : m₂ ⁻¹' u₂ ∈ f₂
h₂ : Prod.snd ⁻¹' u₂ ⊆ s
x : α₁ × α₂
hx : Membership.mem (γ := Set (α₁ × α₂)) (Prod.snd ⁻¹' m₂ ⁻¹' u₂) x
⊢ Membership.mem (γ := Set (α₁ × α₂)) (Prod.snd ⁻¹' m₂ ⁻¹' u₂) x

Tactic:
hx
-- Module: Mathlib.Order.Filter.Prod
Goal:
α₁ : Type u
α₂ : Type v
β₁ : Type w
β₂ : Type x
f₁ : Filter α₁
f₂ : Filter α₂
m₁ : α₁ → β₁
m₂ : α₂ → β₂
s : Set (β₁ × β₂)
u₁ : Set β₁
hu₁ : m₁ ⁻¹' u₁ ∈ f₁
h₁ : Prod.fst ⁻¹' u₁ ⊆ s
u₂ : Set β₂
hu₂ : m₂ ⁻¹' u₂ ∈ f₂
h₂ : Prod.snd ⁻¹' u₂ ⊆ s
x : α₁ × α₂
hx : Membership.mem (γ := Set (α₁ × α₂)) (Prod.snd ⁻¹' m₂ ⁻¹' u₂) x
⊢ Membership.mem (γ := Set (β₁ × β₂)) (Prod.snd ⁻¹' u₂) (Prod.map m₁ m₂ x)

Tactic:
convert!
    hx
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_6
β : Type u_7
ι : Type u_8
a : α
b : β
i : ι
⊢ Filter.coprod (map (fun (x : α) ↦ b) (𝓟 {a})) (map id (𝓟 {i})) =
    𝓟 (SProd.sprod (α := Set β) (β := Set ι) {b} univ ∪ SProd.sprod (α := Set β) (β := Set ι) univ {i})

Tactic:
simp only [map_principal, Filter.coprod, comap_principal, sup_principal, image_singleton,
    prod_univ, univ_prod, id]

Premises used: Filter.sup_principal, Set.image_singleton, Set.univ_prod, Set.prod_univ, id, Filter.comap_principal, Filter.map_principal, Filter.coprod
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_6
β : Type u_7
ι : Type u_8
a : α
b : β
i : ι
rw :
  𝓟 (Prod.map (fun (x : α) ↦ b) id '' (SProd.sprod (α := Set α) (β := Set ι) {a}ᶜ {i}ᶜ)ᶜ) =
    𝓟 (SProd.sprod (α := Set β) (β := Set ι) {b} univ)
⊢ map (α := α × ι) (Prod.map (fun (x : α) ↦ b) id) (Filter.coprod (𝓟 {a}) (𝓟 {i})) =
    𝓟 (SProd.sprod (α := Set β) (β := Set ι) {b} univ)

Tactic:
rw [principal_coprod_principal, map_principal]

Premises used: Filter.principal_coprod_principal, Filter.map_principal
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_6
β : Type u_7
ι : Type u_8
a : α
b : β
i : ι
e_s :
  Prod.map (fun (x : α) ↦ b) id '' (SProd.sprod (α := Set α) (β := Set ι) {a}ᶜ {i}ᶜ)ᶜ =
    SProd.sprod (α := Set β) (β := Set ι) {b} univ
⊢ 𝓟 (Prod.map (fun (x : α) ↦ b) id '' (SProd.sprod (α := Set α) (β := Set ι) {a}ᶜ {i}ᶜ)ᶜ) =
    𝓟 (SProd.sprod (α := Set β) (β := Set ι) {b} univ)

Tactic:
congr
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_6
β : Type u_7
ι : Type u_8
a : α
b : β
i : ι
e_s :
  ∀ (b' : β) (i' : ι),
    Membership.mem (γ := Set (β × ι))
        (Prod.map (fun (x : α) ↦ b) id '' (SProd.sprod (α := Set α) (β := Set ι) {a}ᶜ {i}ᶜ)ᶜ) (b', i') ↔
      (b', i') ∈ SProd.sprod (α := Set β) (β := Set ι) {b} univ
⊢ Prod.map (fun (x : α) ↦ b) id '' (SProd.sprod (α := Set α) (β := Set ι) {a}ᶜ {i}ᶜ)ᶜ =
    SProd.sprod (α := Set β) (β := Set ι) {b} univ

Tactic:
ext ⟨b', i'⟩
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_6
β : Type u_7
ι : Type u_8
a : α
b : β
i : ι
b' : β
i' : ι
e_s :
  Membership.mem (γ := Set (β × ι))
      (Prod.map (fun (x : α) ↦ b) id '' (SProd.sprod (α := Set α) (β := Set ι) {a}ᶜ {i}ᶜ)ᶜ) (b', i') →
    (b', i') ∈ SProd.sprod (α := Set β) (β := Set ι) {b} univ
e_s₁ :
  (b', i') ∈ SProd.sprod (α := Set β) (β := Set ι) {b} univ →
    Membership.mem (γ := Set (β × ι))
      (Prod.map (fun (x : α) ↦ b) id '' (SProd.sprod (α := Set α) (β := Set ι) {a}ᶜ {i}ᶜ)ᶜ) (b', i')
⊢ Membership.mem (γ := Set (β × ι))
      (Prod.map (fun (x : α) ↦ b) id '' (SProd.sprod (α := Set α) (β := Set ι) {a}ᶜ {i}ᶜ)ᶜ) (b', i') ↔
    (b', i') ∈ SProd.sprod (α := Set β) (β := Set ι) {b} univ

Tactic:
constructor
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_6
β : Type u_7
ι : Type u_8
a : α
b : β
i : ι
a'' : α
i'' : ι
left : (a'', i'') ∈ (SProd.sprod (α := Set α) (β := Set ι) {a}ᶜ {i}ᶜ)ᶜ
⊢ ((fun (x : α) ↦ b) a'', id i'') ∈ SProd.sprod (α := Set β) (β := Set ι) {b} univ

Tactic:
simp
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_6
β : Type u_7
ι : Type u_8
a : α
b : β
i : ι
b' : β
i' : ι
h₁ : Membership.mem (γ := Set β) {b} (b', i').1
right : Membership.mem (γ := Set ι) univ (b', i').2
h : (a, i') ∈ (SProd.sprod (α := Set α) (β := Set ι) {a}ᶜ {i}ᶜ)ᶜ ∧ Prod.map (fun (x : α) ↦ b) id (a, i') = (b', i')
⊢ Membership.mem (γ := Set (β × ι))
    (Prod.map (fun (x : α) ↦ b) id '' (SProd.sprod (α := Set α) (β := Set ι) {a}ᶜ {i}ᶜ)ᶜ) (b', i')

Tactic:
use (a, i')

Premises used: Prod.mk
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_6
β : Type u_7
ι : Type u_8
a : α
b : β
i : ι
b' : β
i' : ι
h₁ : Membership.mem (γ := Set β) {b} (b', i').1
right : Membership.mem (γ := Set ι) univ (b', i').2
⊢ (a, i') ∈ (SProd.sprod (α := Set α) (β := Set ι) {a}ᶜ {i}ᶜ)ᶜ ∧ Prod.map (fun (x : α) ↦ b) id (a, i') = (b', i')

Tactic:
simpa using h₁.symm

Premises used: Eq.symm
-- 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
⊢ Tendsto (Prod.map f g) (a.coprod b) (c.coprod d)

Tactic:
map_prodMap_coprod_le.trans (coprod_mono hf hg)

Premises used: Filter.map_prodMap_coprod_le, Filter.coprod_mono, Filter.Tendsto, LE.le.trans
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α × β → γ
la : Filter α
lb : Filter β
lc : Filter γ
h₁ : ∀ s ∈ la, Tendsto f (𝓟 sᶜ ×ˢ lb) lc
h₂ : Tendsto f (SProd.sprod (β := Filter β) la ⊤) lc
simp_all :
  ∀ (h₁ : ∀ s ∈ la, ∀ W ∈ lc, ∃ (U : Set α), sᶜ ⊆ U ∧ ∃ V ∈ lb, ∀ (x : α) (y : β), x ∈ U → y ∈ V → f (x, y) ∈ W)
    (h₂ : ∀ W ∈ lc, ∃ U ∈ la, ∀ (x : α) (y : β), x ∈ U → f (x, y) ∈ W),
    ∀ W ∈ lc, ∃ V ∈ lb, ∀ (x : α), ∀ y ∈ V, f (x, y) ∈ W
⊢ Tendsto f (la.coprod lb) lc

Tactic:
simp_all [tendsto_prod_iff, coprod_eq_prod_top_sup_top_prod]

Premises used: Filter.tendsto_prod_iff, Filter.coprod_eq_prod_top_sup_top_prod
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α × β → γ
la : Filter α
lb : Filter β
lc : Filter γ
h₁ : ∀ s ∈ la, ∀ W ∈ lc, ∃ (U : Set α), sᶜ ⊆ U ∧ ∃ V ∈ lb, ∀ (x : α) (y : β), x ∈ U → y ∈ V → f (x, y) ∈ W
h₂ : ∀ W ∈ lc, ∃ U ∈ la, ∀ (x : α) (y : β), x ∈ U → f (x, y) ∈ W
⊢ ∀ W ∈ lc, ∃ V ∈ lb, ∀ (x : α), ∀ y ∈ V, f (x, y) ∈ W

Tactic:
grind
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α × β → γ
la : Filter α
lb : Filter β
lc : Filter γ
h₁ : ∀ s ∈ lb, Tendsto f (la ×ˢ 𝓟 sᶜ) lc
h₂ : Tendsto f (SProd.sprod (α := Filter α) ⊤ lb) lc
simp_all :
  ∀ (h₁ : ∀ s ∈ lb, ∀ W ∈ lc, ∃ U ∈ la, ∃ (V : Set β), sᶜ ⊆ V ∧ ∀ (x : α) (y : β), x ∈ U → y ∈ V → f (x, y) ∈ W)
    (h₂ : ∀ W ∈ lc, ∃ V ∈ lb, ∀ (x : α), ∀ y ∈ V, f (x, y) ∈ W),
    ∀ W ∈ lc, ∃ U ∈ la, ∀ (x : α) (y : β), x ∈ U → f (x, y) ∈ W
⊢ Tendsto f (la.coprod lb) lc

Tactic:
simp_all [tendsto_prod_iff, coprod_eq_prod_top_sup_top_prod]

Premises used: Filter.tendsto_prod_iff, Filter.coprod_eq_prod_top_sup_top_prod
-- Module: Mathlib.Order.Filter.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α × β → γ
la : Filter α
lb : Filter β
lc : Filter γ
h₁ : ∀ s ∈ lb, ∀ W ∈ lc, ∃ U ∈ la, ∃ (V : Set β), sᶜ ⊆ V ∧ ∀ (x : α) (y : β), x ∈ U → y ∈ V → f (x, y) ∈ W
h₂ : ∀ W ∈ lc, ∃ V ∈ lb, ∀ (x : α), ∀ y ∈ V, f (x, y) ∈ W
⊢ ∀ W ∈ lc, ∃ U ∈ la, ∀ (x : α) (y : β), x ∈ U → f (x, y) ∈ W

Tactic:
grind
-- Module: Mathlib.Order.Filter.Ring
Goal:
α : Type u
β : Type v
inst : MulZeroClass β
inst_1 : Preorder β
inst_2 : PosMulMono β
inst_3 : MulPosMono β
l : Filter α
f₁ f₂ g₁ g₂ : α → β
hf : f₁ ≤ᶠ[l] f₂
hg : g₁ ≤ᶠ[l] g₂
hg₀ : 0 ≤ᶠ[l] g₁
hf₀ : 0 ≤ᶠ[l] f₂
x : α
⊢ f₁ x ≤ f₂ x → g₁ x ≤ g₂ x → 0 x ≤ g₁ x → 0 x ≤ f₂ x → (f₁ * g₁) x ≤ (f₂ * g₂) x

Tactic:
_root_.mul_le_mul

Premises used: mul_le_mul
-- Module: Mathlib.Order.Filter.Ring
Goal:
α : Type u
β : Type v
inst : MulZeroClass β
inst_1 : Preorder β
inst_2 : PosMulMono β
inst_3 : MulPosMono β
l : Filter α
f₁ f₂ g₁ g₂ : α → β
hf : f₁ ≤ᶠ[l] f₂
hg : g₁ ≤ᶠ[l] g₂
hg₀ : 0 ≤ᶠ[l] g₁
hf₀ : 0 ≤ᶠ[l] f₂
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f₁ x ≤ f₂ x) x} x →
          Membership.mem (γ := Set α)
            {x : α |
              Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ g₁ x ≤ g₂ x) x} x →
                Membership.mem (γ := Set α)
                  {x : α |
                    Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ 0 x ≤ g₁ x) x} x →
                      Membership.mem (γ := Set α)
                        {x : α |
                          Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ 0 x ≤ f₂ x) x} x →
                            Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ (f₁ * g₁) x ≤ (f₂ * g₂) x) x} x}
                        x}
                  x}
            x}
      a
h₁ h₂ : ∀ (x : α), f₁ x ≤ f₂ x → g₁ x ≤ g₂ x → 0 x ≤ g₁ x → 0 x ≤ f₂ x → (f₁ * g₁) x ≤ (f₂ * g₂) x
⊢ f₁ * g₁ ≤ᶠ[l] f₂ * g₂

Tactic:
filter_upwards [hf, hg, hg₀, hf₀] with x using _root_.mul_le_mul

Premises used: mul_le_mul
-- Module: Mathlib.Order.Filter.Ring
Goal:
α : Type u
β : Type v
inst : Mul β
inst_1 : Preorder β
inst_2 : MulLeftMono β
inst_3 : MulRightMono β
l : Filter α
f₁ f₂ g₁ g₂ : α → β
hf : f₁ ≤ᶠ[l] f₂
hg : g₁ ≤ᶠ[l] g₂
x : α
hfx : f₁ x ≤ f₂ x
hgx : g₁ x ≤ g₂ x
⊢ (f₁ * g₁) x ≤ (f₂ * g₂) x

Tactic:
_root_.mul_le_mul' hfx hgx

Premises used: mul_le_mul'
-- Module: Mathlib.Order.Filter.Ring
Goal:
α : Type u
β : Type v
inst : Mul β
inst_1 : Preorder β
inst_2 : MulLeftMono β
inst_3 : MulRightMono β
l : Filter α
f₁ f₂ g₁ g₂ : α → β
hf : f₁ ≤ᶠ[l] f₂
hg : g₁ ≤ᶠ[l] g₂
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f₁ x ≤ f₂ x) x} x →
          Membership.mem (γ := Set α)
            {x : α |
              Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ g₁ x ≤ g₂ x) x} x →
                Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ (f₁ * g₁) x ≤ (f₂ * g₂) x) x} x}
            x}
      a
h₁ h₂ : ∀ (x : α) (hfx : f₁ x ≤ f₂ x) (hgx : g₁ x ≤ g₂ x), (f₁ * g₁) x ≤ (f₂ * g₂) x
⊢ f₁ * g₁ ≤ᶠ[l] f₂ * g₂

Tactic:
filter_upwards [hf, hg] with x hfx hgx using _root_.mul_le_mul' hfx hgx
-- Module: Mathlib.Order.Filter.Ring
Goal:
α : Type u
β : Type v
inst : Semiring β
inst_1 : PartialOrder β
inst_2 : IsOrderedRing β
l : Filter α
f g : α → β
hf : 0 ≤ᶠ[l] f
hg : 0 ≤ᶠ[l] g
x : α
⊢ 0 x ≤ f x → 0 x ≤ g x → 0 x ≤ (f * g) x

Tactic:
_root_.mul_nonneg

Premises used: mul_nonneg
-- Module: Mathlib.Order.Filter.Ring
Goal:
α : Type u
β : Type v
inst : Semiring β
inst_1 : PartialOrder β
inst_2 : IsOrderedRing β
l : Filter α
f g : α → β
hf : 0 ≤ᶠ[l] f
hg : 0 ≤ᶠ[l] g
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ 0 x ≤ f x) x} x →
          Membership.mem (γ := Set α)
            {x : α |
              Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ 0 x ≤ g x) x} x →
                Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ 0 x ≤ (f * g) x) x} x}
            x}
      a
h₁ h₂ : ∀ (x : α), 0 x ≤ f x → 0 x ≤ g x → 0 x ≤ (f * g) x
⊢ 0 ≤ᶠ[l] f * g

Tactic:
filter_upwards [hf, hg] with x using _root_.mul_nonneg

Premises used: mul_nonneg
-- Module: Mathlib.Order.Filter.Ring
Goal:
α : Type u
β : Type v
inst : AddGroup β
inst_1 : LE β
inst_2 : AddRightMono β
l : Filter α
f g : α → β
⊢ 0 ≤ᶠ[l] g - f ↔ f ≤ᶠ[l] g

Tactic:
eventually_congr <| Eventually.of_forall fun _ => sub_nonneg

Premises used: Filter.Eventually.of_forall, Filter.EventuallyLE, Filter.eventually_congr, sub_nonneg