awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Filter.Prod (goal)
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)
⊢ map (⇑(Equiv.prodAssoc α β γ) : (a : (α × β) × γ) → α × β × γ) ((f ×ˢ g) ×ˢ h) = f ×ˢ g ×ˢ h
have 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))
Tactic: simp_rw [← comap_equiv_symm, prod_eq_inf, comap_inf, comap_comap, inf_assoc,
    Function.comp_def, Equiv.prodAssoc_symm_apply]
-- Lean 4 proof step from Mathlib.Order.Filter.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : Filter α
g : Filter β
h : Filter γ
⊢ map (⇑(Equiv.prodAssoc α β γ).symm : (a : α × β × γ) → (α × β) × γ) (f ×ˢ g ×ˢ h) = (f ×ˢ g) ×ˢ h
have simp_rw : comap (⇑(Equiv.prodAssoc α β γ) : (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]
-- Lean 4 proof step from Mathlib.Order.Filter.Prod (goal)
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
⊢ map (⇑(Equiv.prodAssoc α β γ).symm : (a : α × β × γ) → (α × β) × γ) (f ×ˢ g ×ˢ h) = (f ×ˢ g) ×ˢ h
have 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
Tactic: simp_rw [map_equiv_symm, prod_eq_inf, comap_inf, comap_comap, inf_assoc,
    Function.comp_def, Equiv.prodAssoc_apply]
-- Lean 4 proof step from Mathlib.Order.Filter.Prod (goal)
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
⊢ map (⇑(Equiv.prodAssoc α β γ).symm : (a : α × β × γ) → (α × β) × γ) (f ×ˢ g ×ˢ h) = (f ×ˢ g) ×ˢ h
have 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
Tactic: simp_rw [map_equiv_symm, prod_eq_inf, comap_inf, comap_comap, inf_assoc,
    Function.comp_def, Equiv.prodAssoc_apply]
-- Lean 4 proof step from Mathlib.Order.Filter.Prod (goal)
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
⊢ map (⇑(Equiv.prodAssoc α β γ).symm : (a : α × β × γ) → (α × β) × γ) (f ×ˢ g ×ˢ h) = (f ×ˢ g) ×ˢ h
have 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
Tactic: simp_rw [map_equiv_symm, prod_eq_inf, comap_inf, comap_comap, inf_assoc,
    Function.comp_def, Equiv.prodAssoc_apply]
-- Lean 4 proof step from Mathlib.Order.Filter.Prod (goal)
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
⊢ map (⇑(Equiv.prodAssoc α β γ).symm : (a : α × β × γ) → (α × β) × γ) (f ×ˢ g ×ˢ h) = (f ×ˢ g) ×ˢ h
have 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)
Tactic: simp_rw [map_equiv_symm, prod_eq_inf, comap_inf, comap_comap, inf_assoc,
    Function.comp_def, Equiv.prodAssoc_apply]
-- Lean 4 proof step from Mathlib.Order.Filter.Prod (goal)
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)
⊢ map (⇑(Equiv.prodAssoc α β γ).symm : (a : α × β × γ) → (α × β) × γ) (f ×ˢ g ×ˢ h) = (f ×ˢ g) ×ˢ h
have 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))
Tactic: simp_rw [map_equiv_symm, prod_eq_inf, comap_inf, comap_comap, inf_assoc,
    Function.comp_def, Equiv.prodAssoc_apply]
-- Lean 4 proof step from Mathlib.Order.Filter.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : Filter α
g : Filter β
h : Filter γ
k : Filter δ
⊢ map (fun (p : (α × β) × γ × δ) ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) ((f ×ˢ g) ×ˢ h ×ˢ k) = (f ×ˢ h) ×ˢ g ×ˢ k
have 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)
Tactic: simp_rw [map_swap4_eq_comap, prod_eq_inf, comap_inf, comap_comap]
-- 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 (β₁ × β₂)
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
⊢ (m₁ '' s₁) ×ˢ (m₂ '' s₂) ⊆ s
have rwa : (fun (p : α₁ × α₂) ↦ (m₁ p.1, m₂ p.2)) '' s₁ ×ˢ s₂ ⊆ s
Tactic: rwa [prod_image_image_eq, image_subset_iff]
-- Lean 4 proof step from Mathlib.Order.Filter.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
F : Filter α
G : Filter γ
⊢ map f F ×ˢ G = map (Prod.map f id) (F ×ˢ G)
have rw : map f F ×ˢ G = map f F ×ˢ map id G
Tactic: rw [← prod_map_map_eq', map_id]
-- Lean 4 proof step from Mathlib.Order.Filter.Prod (goal)
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
⊢ map f F ×ˢ G = map (Prod.map f id) (F ×ˢ G)
have rw₁ : map f F ×ˢ G = map f F ×ˢ G
Tactic: rw [← prod_map_map_eq', map_id]
-- Lean 4 proof step from Mathlib.Order.Filter.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : β → γ
F : Filter α
G : Filter β
⊢ F ×ˢ map f G = map (Prod.map id f) (F ×ˢ G)
have rw : F ×ˢ map f G = map id F ×ˢ map f G
Tactic: rw [← prod_map_map_eq', map_id]
-- Lean 4 proof step from Mathlib.Order.Filter.Prod (goal)
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
⊢ F ×ˢ map f G = map (Prod.map id f) (F ×ˢ G)
have rw₁ : F ×ˢ map f G = F ×ˢ map f G
Tactic: rw [← prod_map_map_eq', map_id]
-- Lean 4 proof step from Mathlib.Order.Filter.Prod (goal)
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 ×ˢ b) (c ×ˢ d)
have rw : map f a ×ˢ map g b ≤ c ×ˢ d
Tactic: rw [Tendsto, Prod.map_def, ← prod_map_map_eq]
-- Lean 4 proof step from Mathlib.Order.Filter.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
m : α × β → γ
f : Filter α
g : Filter β
⊢ map m (f ×ˢ g) = seq (map (fun (a : α) (b : β) ↦ m (a, b)) f) g
have 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
Tactic: simp only [Filter.ext_iff, mem_map, mem_prod_iff, mem_map_seq_iff, exists_and_left]
-- Lean 4 proof step from Mathlib.Order.Filter.Prod (goal)
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
have mp : (∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ ×ˢ t₂ ⊆ m ⁻¹' s) → ∃ t ∈ g, ∃ x ∈ f, ∀ x_1 ∈ x, ∀ y ∈ t, m (x_1, y) ∈ s
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Filter.Prod (goal)
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
⊢ (∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ ×ˢ t₂ ⊆ m ⁻¹' s) ↔ ∃ t ∈ g, ∃ x ∈ f, ∀ x_1 ∈ x, ∀ y ∈ t, m (x_1, y) ∈ s
have mpr : (∃ t ∈ g, ∃ x ∈ f, ∀ x_1 ∈ x, ∀ y ∈ t, m (x_1, y) ∈ s) → ∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ ×ˢ t₂ ⊆ m ⁻¹' s
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Filter.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
g : Filter β
f₁ f₂ : Filter α
⊢ (f₁ ⊓ f₂) ×ˢ g = f₁ ×ˢ g ⊓ f₂ ×ˢ g
have rw : (f₁ ⊓ f₂) ×ˢ g = (f₁ ⊓ f₂) ×ˢ (g ⊓ g)
Tactic: rw [prod_inf_prod, inf_idem]
-- Lean 4 proof step from Mathlib.Order.Filter.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
g : Filter β
f₁ f₂ : Filter α
rw : (f₁ ⊓ f₂) ×ˢ g = (f₁ ⊓ f₂) ×ˢ (g ⊓ g)
⊢ (f₁ ⊓ f₂) ×ˢ g = f₁ ×ˢ g ⊓ f₂ ×ˢ g
have rw₁ : (f₁ ⊓ f₂) ×ˢ g = (f₁ ⊓ f₂) ×ˢ g
Tactic: rw [prod_inf_prod, inf_idem]
-- Lean 4 proof step from Mathlib.Order.Filter.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g₁ g₂ : Filter β
⊢ f ×ˢ (g₁ ⊓ g₂) = f ×ˢ g₁ ⊓ f ×ˢ g₂
have rw : f ×ˢ (g₁ ⊓ g₂) = (f ⊓ f) ×ˢ (g₁ ⊓ g₂)
Tactic: rw [prod_inf_prod, inf_idem]
-- Lean 4 proof step from Mathlib.Order.Filter.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g₁ g₂ : Filter β
rw : f ×ˢ (g₁ ⊓ g₂) = (f ⊓ f) ×ˢ (g₁ ⊓ g₂)
⊢ f ×ˢ (g₁ ⊓ g₂) = f ×ˢ g₁ ⊓ f ×ˢ g₂
have rw₁ : f ×ˢ (g₁ ⊓ g₂) = f ×ˢ (g₁ ⊓ g₂)
Tactic: rw [prod_inf_prod, inf_idem]
-- Lean 4 proof step from Mathlib.Order.Filter.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ 𝓟 s ×ˢ 𝓟 t = 𝓟 (s ×ˢ t)
have simp : Prod.fst ⁻¹' s ∩ Prod.snd ⁻¹' t = s ×ˢ t
Tactic: simp only [prod_eq_inf, comap_principal, principal_eq_iff_eq, comap_principal, inf_principal]
-- Lean 4 proof step from Mathlib.Order.Filter.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
a : α
f : Filter β
⊢ SProd.sprod (α := Filter α) (pure a) f = map (Prod.mk a) f
have rw : seq (map Prod.mk (pure a)) f = map (Prod.mk a) f
Tactic: rw [prod_eq, map_pure, pure_seq_eq_map]
-- Lean 4 proof step from Mathlib.Order.Filter.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
a : α
f : Filter β
rw : seq (map Prod.mk (pure a)) f = map (Prod.mk a) f
⊢ SProd.sprod (α := Filter α) (pure a) f = map (Prod.mk a) f
have rw₁ : seq (pure (Prod.mk a)) f = map (Prod.mk a) f
Tactic: rw [prod_eq, map_pure, pure_seq_eq_map]
-- Lean 4 proof step from Mathlib.Order.Filter.Prod (goal)
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
⊢ SProd.sprod (α := Filter α) (pure a) f = map (Prod.mk a) f
have rw₂ : map (Prod.mk a) f = map (Prod.mk a) f
Tactic: rw [prod_eq, map_pure, pure_seq_eq_map]
-- Lean 4 proof step from Mathlib.Order.Filter.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
a : α
B : Filter β
⊢ map (Function.uncurry f) (SProd.sprod (α := Filter α) (pure a) B) = map (f a) B
have rw : map (Function.uncurry f) (map (Prod.mk a) B) = map (f a) B
Tactic: rw [Filter.pure_prod]
-- Lean 4 proof step from Mathlib.Order.Filter.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
f : Filter α
b : β
⊢ SProd.sprod (β := Filter β) f (pure b) = map (fun (a : α) ↦ (a, b)) f
have rw : Eq (α := Filter (α × β)) (map ((fun (g : β → α × β) ↦ g b) ∘ Prod.mk) f) (map (fun (a : α) ↦ (a, b)) f)
Tactic: rw [prod_eq, seq_pure, map_map]
-- Lean 4 proof step from Mathlib.Order.Filter.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
⊢ f ×ˢ g = ⊥ ↔ f = ⊥ ∨ g = ⊥
have simp_rw : ∅ ∈ 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]
-- 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
⊢ f ×ˢ g = ⊥ ↔ f = ⊥ ∨ g = ⊥
have simp_rw₁ : (∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ ×ˢ t₂ ⊆ ∅) ↔ ∅ ∈ 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
⊢ f ×ˢ g = ⊥ ↔ f = ⊥ ∨ g = ⊥
have simp_rw₂ : (∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ ×ˢ t₂ = ∅) ↔ ∅ ∈ 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
⊢ f ×ˢ g = ⊥ ↔ f = ⊥ ∨ g = ⊥
have simp_rw₃ : (∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ = ∅ ∨ t₂ = ∅) ↔ ∅ ∈ 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
⊢ f ×ˢ g = ⊥ ↔ f = ⊥ ∨ g = ⊥
have simp_rw₄ : (∃ (t₁ : Set α) (_ : t₁ ∈ f) (t₂ : Set β) (_ : t₂ ∈ g), t₁ = ∅ ∨ t₂ = ∅) ↔ ∅ ∈ 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
⊢ f ×ˢ g = ⊥ ↔ f = ⊥ ∨ g = ⊥
have simp_rw₅ : (∃ (x : { a : Set α // a ∈ f }) (x_1 : { a : Set β // a ∈ g }), (↑x : Set α) = ∅ ∨ (↑x_1 : 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
⊢ f ×ˢ g = ⊥ ↔ f = ⊥ ∨ g = ⊥
have 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
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]