awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Filter.Prod (goal)
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
⊢ f ×ˢ g = ⊥ ↔ f = ⊥ ∨ g = ⊥
have simp_rw₇ : ((∃ (x : { a : Set α // a ∈ f }), (↑x : Set α) = ∅) ∨ ∃ (x : { a : Set β // a ∈ g }), (↑x : Set β) = ∅) ↔ ∅ ∈ 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]
-- Lean 4 proof step from Mathlib.Order.Filter.Prod (goal)
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
⊢ f ×ˢ g = ⊥ ↔ f = ⊥ ∨ g = ⊥
have simp_rw₈ : ((∃ (a : Set α) (_ : a ∈ f), a = ∅) ∨ ∃ (a : Set β) (_ : a ∈ g), a = ∅) ↔ ∅ ∈ 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]
-- Lean 4 proof step from Mathlib.Order.Filter.Prod (goal)
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
⊢ f ×ˢ g = ⊥ ↔ f = ⊥ ∨ g = ⊥
have simp_rw₉ : ((∃ a ∈ f, a = ∅) ∨ ∃ a ∈ g, a = ∅) ↔ ∅ ∈ 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]
-- Lean 4 proof step from Mathlib.Order.Filter.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
p : α → Prop
q : β → Prop
⊢ (∃ᶠ (x : α × β) in f ×ˢ g, p x.1 ∧ q x.2) ↔ (∃ᶠ (a : α) in f, p a) ∧ ∃ᶠ (b : β) in g, q b
have simp : (f ×ˢ g ⊓ 𝓟 {x : α × β | p x.1 ∧ q x.2}).NeBot ↔
  (f ×ˢ g ⊓ 𝓟 (SProd.sprod (α := Set α) (β := Set β) {a : α | p a} {b : β | q b})).NeBot
Tactic: simp only [frequently_iff_neBot, ← prod_neBot, ← prod_inf_prod, prod_principal_principal]
-- Lean 4 proof step from Mathlib.Order.Filter.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
⊢ f.coprod g = SProd.sprod (β := Filter β) f ⊤ ⊔ SProd.sprod (α := Filter α) ⊤ g
have rw : f.coprod g = comap Prod.fst f ⊔ comap Prod.snd g
Tactic: rw [prod_top, top_prod]
-- Lean 4 proof step from Mathlib.Order.Filter.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
f₁ f₂ : Filter α
g₁ g₂ : Filter β
⊢ f₁.coprod g₁ ⊓ f₂ ×ˢ g₂ = (SProd.sprod (β := Filter β) f₁ ⊤ ⊔ SProd.sprod (α := Filter α) ⊤ g₁) ⊓ f₂ ×ˢ g₂
have rw : (SProd.sprod (β := Filter β) f₁ ⊤ ⊔ SProd.sprod (α := Filter α) ⊤ g₁) ⊓ f₂ ×ˢ g₂ =
  (SProd.sprod (β := Filter β) f₁ ⊤ ⊔ SProd.sprod (α := Filter α) ⊤ g₁) ⊓ f₂ ×ˢ g₂
Tactic: rw [coprod_eq_prod_top_sup_top_prod]
-- Lean 4 proof step from Mathlib.Order.Filter.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ (𝓟 s).coprod (𝓟 t) = 𝓟 (sᶜ ×ˢ tᶜ)ᶜ
have rw : comap Prod.fst (𝓟 s) ⊔ comap Prod.snd (𝓟 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]
-- Lean 4 proof step from Mathlib.Order.Filter.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
rw : comap Prod.fst (𝓟 s) ⊔ comap Prod.snd (𝓟 t) = 𝓟 (sᶜ ×ˢ tᶜ)ᶜ
⊢ (𝓟 s).coprod (𝓟 t) = 𝓟 (sᶜ ×ˢ tᶜ)ᶜ
have rw₁ : 𝓟 (Prod.fst ⁻¹' s) ⊔ comap Prod.snd (𝓟 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]
-- Lean 4 proof step from Mathlib.Order.Filter.Prod (goal)
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ᶜ)ᶜ
⊢ (𝓟 s).coprod (𝓟 t) = 𝓟 (sᶜ ×ˢ tᶜ)ᶜ
have rw₂ : 𝓟 (Prod.fst ⁻¹' s) ⊔ 𝓟 (Prod.snd ⁻¹' 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]
-- Lean 4 proof step from Mathlib.Order.Filter.Prod (goal)
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ᶜ)ᶜ
⊢ (𝓟 s).coprod (𝓟 t) = 𝓟 (sᶜ ×ˢ tᶜ)ᶜ
have rw₃ : 𝓟 (Prod.fst ⁻¹' s ∪ Prod.snd ⁻¹' 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]
-- Lean 4 proof step from Mathlib.Order.Filter.Prod (goal)
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ᶜ)ᶜ
⊢ (𝓟 s).coprod (𝓟 t) = 𝓟 (sᶜ ×ˢ tᶜ)ᶜ
have rw₄ : 𝓟 (Prod.fst ⁻¹' s ∪ Prod.snd ⁻¹' t) = 𝓟 (Prod.fst ⁻¹' sᶜ ∩ Prod.snd ⁻¹' tᶜ)ᶜ
Tactic: rw [Filter.coprod, comap_principal, comap_principal, sup_principal, Set.prod_eq, compl_inter,
    preimage_compl, preimage_compl, compl_compl, compl_compl]
-- Lean 4 proof step from Mathlib.Order.Filter.Prod (goal)
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ᶜ)ᶜ
⊢ (𝓟 s).coprod (𝓟 t) = 𝓟 (sᶜ ×ˢ tᶜ)ᶜ
have rw₅ : 𝓟 (Prod.fst ⁻¹' s ∪ Prod.snd ⁻¹' t) = 𝓟 ((Prod.fst ⁻¹' sᶜ)ᶜ ∪ (Prod.snd ⁻¹' tᶜ)ᶜ)
Tactic: rw [Filter.coprod, comap_principal, comap_principal, sup_principal, Set.prod_eq, compl_inter,
    preimage_compl, preimage_compl, compl_compl, compl_compl]
-- Lean 4 proof step from Mathlib.Order.Filter.Prod (goal)
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ᶜ)ᶜ)
⊢ (𝓟 s).coprod (𝓟 t) = 𝓟 (sᶜ ×ˢ tᶜ)ᶜ
have rw₆ : 𝓟 (Prod.fst ⁻¹' s ∪ Prod.snd ⁻¹' t) = 𝓟 ((Prod.fst ⁻¹' s)ᶜᶜ ∪ (Prod.snd ⁻¹' tᶜ)ᶜ)
Tactic: rw [Filter.coprod, comap_principal, comap_principal, sup_principal, Set.prod_eq, compl_inter,
    preimage_compl, preimage_compl, compl_compl, compl_compl]
-- Lean 4 proof step from Mathlib.Order.Filter.Prod (goal)
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ᶜ)ᶜ)
⊢ (𝓟 s).coprod (𝓟 t) = 𝓟 (sᶜ ×ˢ tᶜ)ᶜ
have rw₇ : 𝓟 (Prod.fst ⁻¹' s ∪ Prod.snd ⁻¹' t) = 𝓟 ((Prod.fst ⁻¹' s)ᶜᶜ ∪ (Prod.snd ⁻¹' t)ᶜᶜ)
Tactic: rw [Filter.coprod, comap_principal, comap_principal, sup_principal, Set.prod_eq, compl_inter,
    preimage_compl, preimage_compl, compl_compl, compl_compl]
-- Lean 4 proof step from Mathlib.Order.Filter.Prod (goal)
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)ᶜᶜ)
⊢ (𝓟 s).coprod (𝓟 t) = 𝓟 (sᶜ ×ˢ tᶜ)ᶜ
have rw₈ : 𝓟 (Prod.fst ⁻¹' s ∪ Prod.snd ⁻¹' t) = 𝓟 (Prod.fst ⁻¹' s ∪ (Prod.snd ⁻¹' t)ᶜᶜ)
Tactic: rw [Filter.coprod, comap_principal, comap_principal, sup_principal, Set.prod_eq, compl_inter,
    preimage_compl, preimage_compl, compl_compl, compl_compl]
-- Lean 4 proof step from Mathlib.Order.Filter.Prod (goal)
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)ᶜᶜ)
⊢ (𝓟 s).coprod (𝓟 t) = 𝓟 (sᶜ ×ˢ tᶜ)ᶜ
have rw₉ : 𝓟 (Prod.fst ⁻¹' s ∪ Prod.snd ⁻¹' t) = 𝓟 (Prod.fst ⁻¹' s ∪ Prod.snd ⁻¹' t)
Tactic: rw [Filter.coprod, comap_principal, comap_principal, sup_principal, Set.prod_eq, compl_inter,
    preimage_compl, preimage_compl, compl_compl, compl_compl]
-- Lean 4 proof step from Mathlib.Order.Filter.Prod (goal)
Goal:
α₁ : Type u
α₂ : Type v
β₁ : Type w
β₂ : Type x
f₁ : Filter α₁
f₂ : Filter α₂
m₁ : α₁ → β₁
m₂ : α₂ → β₂
s : Set (β₁ × β₂)
⊢ s ∈ (map m₁ f₁).coprod (map m₂ f₂) → s ∈ map (Prod.map m₁ m₂) (f₁.coprod f₂)
have 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
Tactic: simp only [mem_map, mem_coprod_iff]
-- Lean 4 proof step from Mathlib.Order.Filter.Prod (goal)
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
have refine_1 : ∀ (x : α₁ × α₂) (hx : Membership.mem (γ := Set (α₁ × α₂)) (Prod.fst ⁻¹' m₁ ⁻¹' u₁) x),
  Membership.mem (γ := Set (β₁ × β₂)) (Prod.fst ⁻¹' u₁) (Prod.map m₁ m₂ x)
Tactic: refine ⟨⟨m₁ ⁻¹' u₁, hu₁, fun _ hx => h₁ ?_⟩, ⟨m₂ ⁻¹' u₂, hu₂, fun _ hx => h₂ ?_⟩⟩
-- Lean 4 proof step from Mathlib.Order.Filter.Prod (goal)
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)
⊢ (∃ t₁ ∈ f₁, Prod.fst ⁻¹' t₁ ⊆ Prod.map m₁ m₂ ⁻¹' s) ∧ ∃ t₂ ∈ f₂, Prod.snd ⁻¹' t₂ ⊆ Prod.map m₁ m₂ ⁻¹' s
have refine_2 : ∀ (x : α₁ × α₂) (hx : Membership.mem (γ := Set (α₁ × α₂)) (Prod.snd ⁻¹' m₂ ⁻¹' u₂) x),
  Membership.mem (γ := Set (β₁ × β₂)) (Prod.snd ⁻¹' u₂) (Prod.map m₁ m₂ x)
Tactic: refine ⟨⟨m₁ ⁻¹' u₁, hu₁, fun _ hx => h₁ ?_⟩, ⟨m₂ ⁻¹' u₂, hu₂, fun _ hx => h₂ ?_⟩⟩
-- Lean 4 proof step from Mathlib.Order.Filter.Prod (goal)
Goal:
α : Type u_6
β : Type u_7
ι : Type u_8
a : α
b : β
i : ι
⊢ map (α := α × ι) (Prod.map (fun (x : α) ↦ b) id) (Filter.coprod (𝓟 {a}) (𝓟 {i})) =
    𝓟 (SProd.sprod (α := Set β) (β := Set ι) {b} univ)
have rw : 𝓟 (Prod.map (fun (x : α) ↦ b) id '' (SProd.sprod (α := Set α) (β := Set ι) {a}ᶜ {i}ᶜ)ᶜ) =
  𝓟 (SProd.sprod (α := Set β) (β := Set ι) {b} univ)
Tactic: rw [principal_coprod_principal, map_principal]
-- Lean 4 proof step from Mathlib.Order.Filter.Prod (goal)
Goal:
α : Type u_6
β : Type u_7
ι : Type u_8
a : α
b : β
i : ι
⊢ 𝓟 (Prod.map (fun (x : α) ↦ b) id '' (SProd.sprod (α := Set α) (β := Set ι) {a}ᶜ {i}ᶜ)ᶜ) =
    𝓟 (SProd.sprod (α := Set β) (β := Set ι) {b} univ)
have e_s : Prod.map (fun (x : α) ↦ b) id '' (SProd.sprod (α := Set α) (β := Set ι) {a}ᶜ {i}ᶜ)ᶜ =
  SProd.sprod (α := Set β) (β := Set ι) {b} univ
Tactic: congr
-- Lean 4 proof step from Mathlib.Order.Filter.Prod (goal)
Goal:
α : Type u_6
β : Type u_7
ι : Type u_8
a : α
b : β
i : ι
⊢ Prod.map (fun (x : α) ↦ b) id '' (SProd.sprod (α := Set α) (β := Set ι) {a}ᶜ {i}ᶜ)ᶜ =
    SProd.sprod (α := Set β) (β := Set ι) {b} univ
have 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
Tactic: ext ⟨b', i'⟩
-- Lean 4 proof step from Mathlib.Order.Filter.Prod (goal)
Goal:
α : Type u_6
β : Type u_7
ι : Type u_8
a : α
b : β
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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Filter.Prod (goal)
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
⊢ 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
have 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')
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Filter.Prod (goal)
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
⊢ Membership.mem (γ := Set (β × ι))
    (Prod.map (fun (x : α) ↦ b) id '' (SProd.sprod (α := Set α) (β := Set ι) {a}ᶜ {i}ᶜ)ᶜ) (b', i')
have h : (a, i') ∈ (SProd.sprod (α := Set α) (β := Set ι) {a}ᶜ {i}ᶜ)ᶜ ∧ Prod.map (fun (x : α) ↦ b) id (a, i') = (b', i')
Tactic: use (a, i')
-- Lean 4 proof step from Mathlib.Order.Filter.Prod (goal)
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
⊢ Tendsto f (la.coprod lb) lc
have 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
Tactic: simp_all [tendsto_prod_iff, coprod_eq_prod_top_sup_top_prod]
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.Order.Filter.Prod (goal)
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
⊢ Tendsto f (la.coprod lb) lc
have 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
Tactic: simp_all [tendsto_prod_iff, coprod_eq_prod_top_sup_top_prod]
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.Order.Filter.Ring (goal)
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₂
⊢ f₁ * g₁ ≤ᶠ[l] f₂ * g₂
have 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
Tactic: filter_upwards [hf, hg, hg₀, hf₀] with x using _root_.mul_le_mul
-- Lean 4 proof step from Mathlib.Order.Filter.Ring (goal)
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
⊢ f₁ * g₁ ≤ᶠ[l] f₂ * g₂
have h₁ : ∀ (a : α), f₁ a ≤ f₂ a → g₁ a ≤ g₂ a → 0 a ≤ g₁ a → 0 a ≤ f₂ a → (f₁ * g₁) a ≤ (f₂ * g₂) a
Tactic: filter_upwards [hf, hg, hg₀, hf₀] with x using _root_.mul_le_mul
-- Lean 4 proof step from Mathlib.Order.Filter.Ring (goal)
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₂
⊢ f₁ * g₁ ≤ᶠ[l] f₂ * g₂
have 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
Tactic: filter_upwards [hf, hg] with x hfx hgx using _root_.mul_le_mul' hfx hgx
-- Lean 4 proof step from Mathlib.Order.Filter.Ring (goal)
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
⊢ f₁ * g₁ ≤ᶠ[l] f₂ * g₂
have h₁ : ∀ (a : α), f₁ a ≤ f₂ a → g₁ a ≤ g₂ a → (f₁ * g₁) a ≤ (f₂ * g₂) a
Tactic: filter_upwards [hf, hg] with x hfx hgx using _root_.mul_le_mul' hfx hgx
-- Lean 4 proof step from Mathlib.Order.Filter.Ring (goal)
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
⊢ 0 ≤ᶠ[l] f * g
have 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
Tactic: filter_upwards [hf, hg] with x using _root_.mul_nonneg
-- Lean 4 proof step from Mathlib.Order.Filter.Ring (goal)
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
⊢ 0 ≤ᶠ[l] f * g
have h₁ : ∀ (a : α), 0 a ≤ f a → 0 a ≤ g a → 0 a ≤ (f * g) a
Tactic: filter_upwards [hf, hg] with x using _root_.mul_nonneg
-- Lean 4 proof step from Mathlib.Order.Filter.SmallSets (goal)
Goal:
α : Type u_1
f : Filter α
⊢ f.smallSets = generate (powerset '' f.sets)
have simp_rw : f.smallSets = ⨅ s ∈ powerset '' f.sets, 𝓟 s
Tactic: simp_rw [generate_eq_biInf, smallSets, iInf_image, Filter.lift', Filter.lift, Function.comp_apply,
    Filter.mem_sets]