awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Filter.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set (α × β)
f : Filter α
g : Filter β
mp : s ∈ f ×ˢ g → ∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ ×ˢ t₂ ⊆ s
⊢ s ∈ f ×ˢ g ↔ ∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ ×ˢ t₂ ⊆ s
have mpr : (∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ ×ˢ t₂ ⊆ s) → s ∈ f ×ˢ g
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Filter.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
t : Set β
f : Filter α
s : Set (α × β)
⊢ s ∈ f ×ˢ 𝓟 t ↔ {a : α | ∀ b ∈ t, (a, b) ∈ s} ∈ f
have rw : (∃ t₁ ∈ f, ∃ t₂ ∈ 𝓟 t, t₁ ×ˢ t₂ ⊆ s) ↔ ∃ t_1 ∈ f, t_1 ⊆ {a : α | ∀ b ∈ t, (a, b) ∈ s}
Tactic: rw [← @exists_mem_subset_iff _ f, mem_prod_iff]
-- Lean 4 proof step from Mathlib.Order.Filter.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
t : Set β
f : Filter α
s : Set (α × β)
⊢ (∃ t₁ ∈ f, ∃ t₂ ∈ 𝓟 t, t₁ ×ˢ t₂ ⊆ s) ↔ ∃ t_1 ∈ f, t_1 ⊆ {a : α | ∀ b ∈ t, (a, b) ∈ s}
have refine_1 : ∀ (u : Set α), (∃ t₂ ∈ 𝓟 t, u ×ˢ t₂ ⊆ s) → u ⊆ {a : α | ∀ b ∈ t, (a, b) ∈ s}
Tactic: refine exists_congr fun u => Iff.rfl.and ⟨?_, fun h => ⟨t, mem_principal_self t, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Order.Filter.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
t : Set β
f : Filter α
s : Set (α × β)
refine_1 : ∀ (u : Set α), (∃ t₂ ∈ 𝓟 t, u ×ˢ t₂ ⊆ s) → u ⊆ {a : α | ∀ b ∈ t, (a, b) ∈ s}
⊢ (∃ t₁ ∈ f, ∃ t₂ ∈ 𝓟 t, t₁ ×ˢ t₂ ⊆ s) ↔ ∃ t_1 ∈ f, t_1 ⊆ {a : α | ∀ b ∈ t, (a, b) ∈ s}
have refine_2 : ∀ (u : Set α) (h : u ⊆ {a : α | ∀ b ∈ t, (a, b) ∈ s}), u ×ˢ t ⊆ s
Tactic: refine exists_congr fun u => Iff.rfl.and ⟨?_, fun h => ⟨t, mem_principal_self t, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Order.Filter.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
f : Filter α
s : Set (α × β)
⊢ s ∈ SProd.sprod (β := Filter β) f ⊤ ↔ {a : α | ∀ (b : β), (a, b) ∈ s} ∈ f
have rw : {a : α | ∀ (b : β), Membership.mem (γ := Set β) univ b → (a, b) ∈ s} ∈ f ↔ {a : α | ∀ (b : β), (a, b) ∈ s} ∈ f
Tactic: rw [← principal_univ, mem_prod_principal]
-- Lean 4 proof step from Mathlib.Order.Filter.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
f : Filter α
p : α × β → Prop
s : Set β
⊢ (∀ᶠ (x : α × β) in f ×ˢ 𝓟 s, p x) ↔ ∀ᶠ (x : α) in f, ∀ y ∈ s, p (x, y)
have rw : {a : α | ∀ b ∈ s, Membership.mem (γ := Set (α × β)) {x : α × β | p x} (a, b)} ∈ f ↔ {x : α | ∀ y ∈ s, p (x, y)} ∈ f
Tactic: rw [eventually_iff, eventually_iff, mem_prod_principal]
-- Lean 4 proof step from Mathlib.Order.Filter.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β × γ
b : Filter β
c : Filter γ
⊢ comap f (b ×ˢ c) = comap (Prod.fst ∘ f) b ⊓ comap (Prod.snd ∘ f) c
have rw : comap f (comap Prod.fst b ⊓ comap Prod.snd c) = comap (Prod.fst ∘ f) b ⊓ comap (Prod.snd ∘ f) c
Tactic: rw [prod_eq_inf, comap_inf, Filter.comap_comap, Filter.comap_comap]
-- Lean 4 proof step from Mathlib.Order.Filter.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β × γ
b : Filter β
c : Filter γ
rw : comap f (comap Prod.fst b ⊓ comap Prod.snd c) = comap (Prod.fst ∘ f) b ⊓ comap (Prod.snd ∘ f) c
⊢ comap f (b ×ˢ c) = comap (Prod.fst ∘ f) b ⊓ comap (Prod.snd ∘ f) c
have rw₁ : comap f (comap Prod.fst b) ⊓ comap f (comap Prod.snd c) = comap (Prod.fst ∘ f) b ⊓ comap (Prod.snd ∘ f) c
Tactic: rw [prod_eq_inf, comap_inf, Filter.comap_comap, Filter.comap_comap]
-- Lean 4 proof step from Mathlib.Order.Filter.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β × γ
b : Filter β
c : Filter γ
rw : comap f (comap Prod.fst b ⊓ comap Prod.snd c) = comap (Prod.fst ∘ f) b ⊓ comap (Prod.snd ∘ f) c
rw₁ : comap f (comap Prod.fst b) ⊓ comap f (comap Prod.snd c) = comap (Prod.fst ∘ f) b ⊓ comap (Prod.snd ∘ f) c
⊢ comap f (b ×ˢ c) = comap (Prod.fst ∘ f) b ⊓ comap (Prod.snd ∘ f) c
have rw₂ : comap (Prod.fst ∘ f) b ⊓ comap f (comap Prod.snd c) = comap (Prod.fst ∘ f) b ⊓ comap (Prod.snd ∘ f) c
Tactic: rw [prod_eq_inf, comap_inf, Filter.comap_comap, Filter.comap_comap]
-- Lean 4 proof step from Mathlib.Order.Filter.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β × γ
b : Filter β
c : Filter γ
rw : comap f (comap Prod.fst b ⊓ comap Prod.snd c) = comap (Prod.fst ∘ f) b ⊓ comap (Prod.snd ∘ f) c
rw₁ : comap f (comap Prod.fst b) ⊓ comap f (comap Prod.snd c) = comap (Prod.fst ∘ f) b ⊓ comap (Prod.snd ∘ f) c
rw₂ : comap (Prod.fst ∘ f) b ⊓ comap f (comap Prod.snd c) = comap (Prod.fst ∘ f) b ⊓ comap (Prod.snd ∘ f) c
⊢ comap f (b ×ˢ c) = comap (Prod.fst ∘ f) b ⊓ comap (Prod.snd ∘ f) c
have rw₃ : comap (Prod.fst ∘ f) b ⊓ comap (Prod.snd ∘ f) c = comap (Prod.fst ∘ f) b ⊓ comap (Prod.snd ∘ f) c
Tactic: rw [prod_eq_inf, comap_inf, Filter.comap_comap, Filter.comap_comap]
-- Lean 4 proof step from Mathlib.Order.Filter.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
f : Filter α
⊢ SProd.sprod (β := Filter β) f ⊤ = comap Prod.fst f
have rw : Eq (α := Filter (α × β)) (comap Prod.fst f ⊓ comap Prod.snd ⊤) (comap Prod.fst f)
Tactic: rw [prod_eq_inf, comap_top, inf_top_eq]
-- Lean 4 proof step from Mathlib.Order.Filter.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
f : Filter α
rw : Eq (α := Filter (α × β)) (comap Prod.fst f ⊓ comap Prod.snd ⊤) (comap Prod.fst f)
⊢ SProd.sprod (β := Filter β) f ⊤ = comap Prod.fst f
have rw₁ : Eq (α := Filter (α × β)) (comap Prod.fst f ⊓ ⊤) (comap Prod.fst f)
Tactic: rw [prod_eq_inf, comap_top, inf_top_eq]
-- Lean 4 proof step from Mathlib.Order.Filter.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
f : Filter α
rw : Eq (α := Filter (α × β)) (comap Prod.fst f ⊓ comap Prod.snd ⊤) (comap Prod.fst f)
rw₁ : Eq (α := Filter (α × β)) (comap Prod.fst f ⊓ ⊤) (comap Prod.fst f)
⊢ SProd.sprod (β := Filter β) f ⊤ = comap Prod.fst f
have rw₂ : Eq (α := Filter (α × β)) (comap Prod.fst f) (comap Prod.fst f)
Tactic: rw [prod_eq_inf, comap_top, inf_top_eq]
-- Lean 4 proof step from Mathlib.Order.Filter.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
g : Filter β
⊢ SProd.sprod (α := Filter α) ⊤ g = comap Prod.snd g
have rw : Eq (α := Filter (α × β)) (comap Prod.fst ⊤ ⊓ comap Prod.snd g) (comap Prod.snd g)
Tactic: rw [prod_eq_inf, comap_top, top_inf_eq]
-- Lean 4 proof step from Mathlib.Order.Filter.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
g : Filter β
rw : Eq (α := Filter (α × β)) (comap Prod.fst ⊤ ⊓ comap Prod.snd g) (comap Prod.snd g)
⊢ SProd.sprod (α := Filter α) ⊤ g = comap Prod.snd g
have rw₁ : Eq (α := Filter (α × β)) (⊤ ⊓ comap Prod.snd g) (comap Prod.snd g)
Tactic: rw [prod_eq_inf, comap_top, top_inf_eq]
-- Lean 4 proof step from Mathlib.Order.Filter.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
g : Filter β
rw : Eq (α := Filter (α × β)) (comap Prod.fst ⊤ ⊓ comap Prod.snd g) (comap Prod.snd g)
rw₁ : Eq (α := Filter (α × β)) (⊤ ⊓ comap Prod.snd g) (comap Prod.snd g)
⊢ SProd.sprod (α := Filter α) ⊤ g = comap Prod.snd g
have rw₂ : Eq (α := Filter (α × β)) (comap Prod.snd g) (comap Prod.snd g)
Tactic: rw [prod_eq_inf, comap_top, top_inf_eq]
-- Lean 4 proof step from Mathlib.Order.Filter.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
la : Filter α
lb : Filter β
p : α × β → Prop
h : ∀ᶠ (x : α × β) in la ×ˢ lb, p x
⊢ ∀ᶠ (x : α) in la, ∀ᶠ (y : β) in lb, p (x, y)
have rcases : ∀ (pa : α → Prop) (ha : ∀ᶠ (x : α) in la, pa x) (pb : β → Prop) (hb : ∀ᶠ (y : β) in lb, pb y)
  (h : ∀ {x : α}, pa x → ∀ {y : β}, pb y → p (x, y)), ∀ᶠ (x : α) in la, ∀ᶠ (y : β) in lb, p (x, y)
Tactic: rcases eventually_prod_iff.1 h with ⟨pa, ha, pb, hb, h⟩
-- Lean 4 proof step from Mathlib.Order.Filter.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
la : Filter α
lb : Filter β
p : α → β → Prop
h : ∃ᶠ (x : α) in la, ∃ᶠ (y : β) in lb, p x y
⊢ ∃ᶠ (xy : α × β) in la ×ˢ lb, p xy.1 xy.2
have contrapose! : ∀ (h : ∀ᶠ (x : α × β) in la ×ˢ lb, ¬p x.1 x.2), ∀ᶠ (x : α) in la, ∀ᶠ (x_1 : β) in lb, ¬p x x_1
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.Filter.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
y : α → β
r : α → β → Prop
hy : Tendsto y f g
hr : ∀ᶠ (p : α × β) in f ×ˢ g, r p.1 p.2
⊢ ∀ᶠ (x : α) in f, r x (y x)
have obtain : ∀ (p : α → Prop) (hp : ∀ᶠ (x : α) in f, p x) (q : β → Prop) (hq : ∀ᶠ (y : β) in g, q y)
  (hr : ∀ {x : α}, p x → ∀ {y : β}, q y → r (x, y).1 (x, y).2), ∀ᶠ (x : α) in f, r x (y x)
Tactic: obtain ⟨p, hp, q, hq, hr⟩ := eventually_prod_iff.mp hr
-- Lean 4 proof step from Mathlib.Order.Filter.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
y : α → β
r : α → β → Prop
hy : Tendsto y f g
hr_1 : ∀ᶠ (p : α × β) in f ×ˢ g, r p.1 p.2
p : α → Prop
hp : ∀ᶠ (x : α) in f, p x
q : β → Prop
hq : ∀ᶠ (y : β) in g, q y
hr : ∀ {x : α}, p x → ∀ {y : β}, q y → r (x, y).1 (x, y).2
⊢ ∀ᶠ (x : α) in f, r x (y x)
have h : ∀ (a : α),
  Membership.mem (γ := Set α)
    {x : α |
      Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ p x) x} x →
        Membership.mem (γ := Set α)
          {x : α |
            Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ q (y x)) x} x →
              Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ r x (y x)) x} x}
          x}
    a
Tactic: filter_upwards [hp, hy.eventually hq] with _ hp hq using hr hp hq
-- Lean 4 proof step from Mathlib.Order.Filter.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
y : α → β
r : α → β → Prop
hy : Tendsto y f g
hr_1 : ∀ᶠ (p : α × β) in f ×ˢ g, r p.1 p.2
p : α → Prop
hp : ∀ᶠ (x : α) in f, p x
q : β → Prop
hq : ∀ᶠ (y : β) in g, q y
hr : ∀ {x : α}, p x → ∀ {y : β}, q y → r (x, y).1 (x, y).2
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ p x) x} x →
          Membership.mem (γ := Set α)
            {x : α |
              Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ q (y x)) x} x →
                Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ r x (y x)) x} x}
            x}
      a
⊢ ∀ᶠ (x : α) in f, r x (y x)
have h₁ : ∀ (a : α), p a → q (y a) → r a (y a)
Tactic: filter_upwards [hp, hy.eventually hq] with _ hp hq using hr hp hq
-- Lean 4 proof step from Mathlib.Order.Filter.Prod (goal)
Goal:
α : Type u_1
γ : Type u_3
f : Filter α
g : Filter γ
p : Prod.{u_1, u_3} (α × α) γ → Prop
h : ∀ᶠ (x : Prod.{u_1, u_3} (α × α) γ) in (f ×ˢ f) ×ˢ g, p x
⊢ ∀ᶠ (x : α × γ) in f ×ˢ g, p ((x.1, x.1), x.2)
have obtain : ∀ (t : α × α → Prop) (ht : ∀ᶠ (x : α × α) in f ×ˢ f, t x) (s : γ → Prop) (hs : ∀ᶠ (y : γ) in g, s y)
  (hst : ∀ {x : α × α}, t x → ∀ {y : γ}, s y → p (x, y)), ∀ᶠ (x : α × γ) in f ×ˢ g, p ((x.1, x.1), x.2)
Tactic: obtain ⟨t, ht, s, hs, hst⟩ := eventually_prod_iff.1 h
-- Lean 4 proof step from Mathlib.Order.Filter.Prod (goal)
Goal:
α : Type u_1
γ : Type u_3
f : Filter α
g : Filter γ
p : Prod.{u_1, u_3} α (γ × γ) → Prop
h : ∀ᶠ (x : Prod.{u_1, u_3} α (γ × γ)) in f ×ˢ g ×ˢ g, p x
⊢ ∀ᶠ (x : α × γ) in f ×ˢ g, p (x.1, x.2, x.2)
have obtain : ∀ (t : α → Prop) (ht : ∀ᶠ (x : α) in f, t x) (s : γ × γ → Prop) (hs : ∀ᶠ (y : γ × γ) in g ×ˢ g, s y)
  (hst : ∀ {x : α}, t x → ∀ {y : γ × γ}, s y → p (x, y)), ∀ᶠ (x : α × γ) in f ×ˢ g, p (x.1, x.2, x.2)
Tactic: obtain ⟨t, ht, s, hs, hst⟩ := eventually_prod_iff.1 h
-- Lean 4 proof step from Mathlib.Order.Filter.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
⊢ f ×ˢ g = map Prod.swap (g ×ˢ f)
have rw : comap Prod.swap (g ×ˢ f) = map Prod.swap (g ×ˢ f)
Tactic: rw [prod_comm', ← map_swap_eq_comap_swap]
-- Lean 4 proof step from Mathlib.Order.Filter.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
rw : comap Prod.swap (g ×ˢ f) = map Prod.swap (g ×ˢ f)
⊢ f ×ˢ g = map Prod.swap (g ×ˢ f)
have rw₁ : map Prod.swap (g ×ˢ f) = map Prod.swap (g ×ˢ f)
Tactic: rw [prod_comm', ← map_swap_eq_comap_swap]
-- Lean 4 proof step from Mathlib.Order.Filter.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
s : Set (α × β)
⊢ s ∈ f ×ˢ g ↔ ∃ t ∈ f, ∀ᶠ (y : β) in g, ∀ x ∈ t, (x, y) ∈ s
have simp : (∃ t₁ ∈ f, ∃ t₂ ∈ g, ∀ x ∈ t₁, ∀ y ∈ t₂, (x, y) ∈ s) ↔ ∃ t ∈ f, ∀ᶠ (y : β) in g, ∀ x ∈ t, (x, y) ∈ s
Tactic: simp only [mem_prod_iff, prod_subset_iff]
-- Lean 4 proof step from Mathlib.Order.Filter.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
s : Set (α × β)
⊢ (∃ t₁ ∈ f, ∃ t₂ ∈ g, ∀ x ∈ t₁, ∀ y ∈ t₂, (x, y) ∈ s) ↔ ∃ t ∈ f, ∀ᶠ (y : β) in g, ∀ x ∈ t, (x, y) ∈ s
have refine : ∀ (x : Set α),
  (∃ t₂ ∈ g, ∀ x_1 ∈ x, ∀ y ∈ t₂, (x_1, y) ∈ s) ↔ ∃ t ∈ g, t ⊆ {x_1 : β | (fun (y : β) ↦ ∀ x_2 ∈ x, (x_2, y) ∈ s) x_1}
Tactic: refine exists_congr fun _ => Iff.rfl.and <| Iff.trans ?_ exists_mem_subset_iff
-- Lean 4 proof step from Mathlib.Order.Filter.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
s : Set (α × β)
⊢ s ∈ f ×ˢ g ↔ ∃ t ∈ g, ∀ᶠ (x : α) in f, ∀ y ∈ t, (x, y) ∈ s
have rw : (∃ t ∈ g, ∀ᶠ (y : α) in f, ∀ x ∈ t, (x, y) ∈ Prod.swap ⁻¹' s) ↔ ∃ t ∈ g, ∀ᶠ (x : α) in f, ∀ y ∈ t, (x, y) ∈ s
Tactic: rw [prod_comm, mem_map, mem_prod_iff_left]
-- Lean 4 proof step from Mathlib.Order.Filter.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
inst : g.NeBot
⊢ map Prod.fst (f ×ˢ g) = f
have h : ∀ (s : Set α), s ∈ map Prod.fst (f ×ˢ g) ↔ s ∈ f
Tactic: ext s
-- Lean 4 proof step from Mathlib.Order.Filter.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
inst : f.NeBot
⊢ map Prod.snd (f ×ˢ g) = g
have rw : map (Prod.snd ∘ Prod.swap) (g ×ˢ f) = g
Tactic: rw [prod_comm, map_map]
-- Lean 4 proof step from Mathlib.Order.Filter.Prod (goal)
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₂
have refine : ∀ (h : f₁ ×ˢ g₁ = f₂ ×ˢ g₂), f₁ = f₂ ∧ g₁ = g₂
Tactic: refine ⟨fun h => ?_, fun h => h.1 ▸ h.2 ▸ rfl⟩
-- Lean 4 proof step from Mathlib.Order.Filter.Prod (hypothesis)
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₂
have hle : f₁ ≤ f₂ ∧ g₁ ≤ g₂
Tactic: have hle : f₁ ≤ f₂ ∧ g₁ ≤ g₂ := prod_le_prod.1 h.le
-- Lean 4 proof step from Mathlib.Order.Filter.Prod (hypothesis)
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₁ = f₂ ∧ g₁ = g₂
have this : f₂.NeBot
Tactic: haveI := neBot_of_le hle.1
-- Lean 4 proof step from Mathlib.Order.Filter.Prod (hypothesis)
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
⊢ f₁ = f₂ ∧ g₁ = g₂
have this₁ : g₂.NeBot
Tactic: haveI := neBot_of_le hle.2
-- Lean 4 proof step from Mathlib.Order.Filter.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
p : α × β → Prop
⊢ (∀ᶠ (x : α × β) in f ×ˢ g, p x) ↔ ∀ᶠ (y : β × α) in g ×ˢ f, p y.swap
have rw : (∀ᶠ (x : α × β) in map Prod.swap (g ×ˢ f), p x) ↔ ∀ᶠ (y : β × α) in g ×ˢ f, p y.swap
Tactic: rw [prod_comm]
-- 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 γ
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
have refine : ∀ {x : α} (hx : ∀ᶠ (y : β) in g, p x y) {z : γ} (hz : ∀ᶠ (y : β) in g, q y z), r (x, z).1 (x, z).2
Tactic: refine eventually_prod_iff.mpr ⟨_, hp, _, hq, fun {x} hx {z} hz ↦ ?_⟩
-- 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 γ
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
⊢ r (x, z).1 (x, z).2
have rcases : ∀ (y : β) (hpy : p x y) (hqy : q y z), r (x, z).1 (x, z).2
Tactic: rcases (hx.and hz).exists with ⟨y, hpy, hqy⟩
-- 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 α β γ) : (a : (α × β) × γ) → α × β × γ) ((f ×ˢ g) ×ˢ h) = f ×ˢ g ×ˢ h
have simp_rw : comap (⇑(Equiv.prodAssoc α β γ).symm : (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]
-- 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
⊢ map (⇑(Equiv.prodAssoc α β γ) : (a : (α × β) × γ) → α × β × γ) ((f ×ˢ g) ×ˢ h) = f ×ˢ g ×ˢ h
have 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)
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 γ
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)
⊢ map (⇑(Equiv.prodAssoc α β γ) : (a : (α × β) × γ) → α × β × γ) ((f ×ˢ g) ×ˢ h) = f ×ˢ g ×ˢ h
have 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))
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 γ
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))
⊢ map (⇑(Equiv.prodAssoc α β γ) : (a : (α × β) × γ) → α × β × γ) ((f ×ˢ g) ×ˢ h) = f ×ˢ g ×ˢ h
have 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)
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 γ
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)
⊢ map (⇑(Equiv.prodAssoc α β γ) : (a : (α × β) × γ) → α × β × γ) ((f ×ˢ g) ×ˢ h) = f ×ˢ g ×ˢ h
have 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)
Tactic: simp_rw [← comap_equiv_symm, prod_eq_inf, comap_inf, comap_comap, inf_assoc,
    Function.comp_def, Equiv.prodAssoc_symm_apply]