awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
l : Filter (α ⊕ β)
rw : comap (Sum.elim inl inr) l = l
⊢ map inl (comap inl l) ⊔ map inr (comap inr l) = l
have rw₁ : comap id l = l
Tactic: rw [← comap_sumElim_eq, Sum.elim_inl_inr, comap_id]
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
l : Filter (α ⊕ β)
rw : comap (Sum.elim inl inr) l = l
rw₁ : comap id l = l
⊢ map inl (comap inl l) ⊔ map inr (comap inr l) = l
have rw₂ : l = l
Tactic: rw [← comap_sumElim_eq, Sum.elim_inl_inr, comap_id]
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
l : Filter (α ⊕ β)
m₁ : α → γ
m₂ : β → γ
⊢ map (Sum.elim m₁ m₂) l = map m₁ (comap inl l) ⊔ map m₂ (comap inr l)
have rw : map (Sum.elim m₁ m₂) (map inl (comap inl l) ⊔ map inr (comap inr l)) =
  map m₁ (comap inl (map inl (comap inl l) ⊔ map inr (comap inr l))) ⊔
    map m₂ (comap inr (map inl (comap inl l) ⊔ map inr (comap inr l)))
Tactic: rw [← map_comap_inl_sup_map_comap_inr l]
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
f : Filter α
⊢ NeBot (α := α × β) (comap Prod.fst f) ↔ f.NeBot ∧ Nonempty β
have inl : IsEmpty β → (NeBot (α := α × β) (comap Prod.fst f) ↔ f.NeBot ∧ Nonempty β)
Tactic: cases isEmpty_or_nonempty β
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
f : Filter α
inl : IsEmpty β → (NeBot (α := α × β) (comap Prod.fst f) ↔ f.NeBot ∧ Nonempty β)
⊢ NeBot (α := α × β) (comap Prod.fst f) ↔ f.NeBot ∧ Nonempty β
have inr : Nonempty β → (NeBot (α := α × β) (comap Prod.fst f) ↔ f.NeBot ∧ Nonempty β)
Tactic: cases isEmpty_or_nonempty β
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
f : Filter α
h : IsEmpty β
⊢ NeBot (α := α × β) (comap Prod.fst f) ↔ f.NeBot ∧ Nonempty β
have inl : ¬NeBot (α := α × β) ⊥ ↔ ¬(f.NeBot ∧ Nonempty β)
Tactic: rw [filter_eq_bot_of_isEmpty (f.comap _), ← not_iff_not]
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
f : Filter β
⊢ NeBot (α := α × β) (comap Prod.snd f) ↔ Nonempty α ∧ f.NeBot
have inl : ∀ (hα : IsEmpty α), NeBot (α := α × β) (comap Prod.snd f) ↔ Nonempty α ∧ f.NeBot
Tactic: rcases isEmpty_or_nonempty α with hα | hα
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
f : Filter β
inl : ∀ (hα : IsEmpty α), NeBot (α := α × β) (comap Prod.snd f) ↔ Nonempty α ∧ f.NeBot
⊢ NeBot (α := α × β) (comap Prod.snd f) ↔ Nonempty α ∧ f.NeBot
have inr : ∀ (hα : Nonempty α), NeBot (α := α × β) (comap Prod.snd f) ↔ Nonempty α ∧ f.NeBot
Tactic: rcases isEmpty_or_nonempty α with hα | hα
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
f : Filter β
hα : IsEmpty α
⊢ NeBot (α := α × β) (comap Prod.snd f) ↔ Nonempty α ∧ f.NeBot
have inl : ¬NeBot (α := α × β) ⊥ ↔ ¬(Nonempty α ∧ f.NeBot)
Tactic: rw [filter_eq_bot_of_isEmpty (f.comap _), ← not_iff_not]
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
ι : Type u_6
α : ι → Type u_7
i : ι
f : Filter (α i)
⊢ (comap (eval (β := α) i) f).NeBot ↔ (∀ (j : ι), Nonempty.{u_7 + 1} (α j)) ∧ f.NeBot
have inl : ∀ (H : IsEmpty ((j : ι) → α j)), (comap (eval (β := α) i) f).NeBot ↔ (∀ (j : ι), Nonempty.{u_7 + 1} (α j)) ∧ f.NeBot
Tactic: rcases isEmpty_or_nonempty (∀ j, α j) with H | H
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
ι : Type u_6
α : ι → Type u_7
i : ι
f : Filter (α i)
inl :
  ∀ (H : IsEmpty ((j : ι) → α j)), (comap (eval (β := α) i) f).NeBot ↔ (∀ (j : ι), Nonempty.{u_7 + 1} (α j)) ∧ f.NeBot
⊢ (comap (eval (β := α) i) f).NeBot ↔ (∀ (j : ι), Nonempty.{u_7 + 1} (α j)) ∧ f.NeBot
have inr : ∀ (H : Nonempty ((j : ι) → α j)), (comap (eval (β := α) i) f).NeBot ↔ (∀ (j : ι), Nonempty.{u_7 + 1} (α j)) ∧ f.NeBot
Tactic: rcases isEmpty_or_nonempty (∀ j, α j) with H | H
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
ι : Type u_6
α : ι → Type u_7
i : ι
f : Filter (α i)
H : IsEmpty ((j : ι) → α j)
⊢ (comap (eval (β := α) i) f).NeBot ↔ (∀ (j : ι), Nonempty.{u_7 + 1} (α j)) ∧ f.NeBot
have inl : ¬NeBot (α := (x : ι) → α x) ⊥ ↔ ¬((∀ (j : ι), Nonempty.{u_7 + 1} (α j)) ∧ f.NeBot)
Tactic: rw [filter_eq_bot_of_isEmpty (f.comap _), ← not_iff_not]
-- Lean 4 proof step from Mathlib.Order.Filter.Map (hypothesis)
Goal:
ι : Type u_6
α : ι → Type u_7
i : ι
f : Filter (α i)
H : Nonempty ((j : ι) → α j)
⊢ (comap (eval (β := α) i) f).NeBot ↔ (∀ (j : ι), Nonempty.{u_7 + 1} (α j)) ∧ f.NeBot
have this : ∀ (j : ι), Nonempty.{u_7 + 1} (α j)
Tactic: have : ∀ j, Nonempty (α j) := Classical.nonempty_pi.1 H
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
f : Filter α
m : α → β
⊢ map m f = ⊥ → f = ⊥
have rw : ∅ ∈ map m f → ∅ ∈ f
Tactic: rw [← empty_mem_iff_bot, ← empty_mem_iff_bot]
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
f : Filter α
m : α → β
⊢ ⊥ = map m f ↔ f = ⊥
have rw : map m f = ⊥ ↔ f = ⊥
Tactic: rw [eq_comm, map_eq_bot_iff]
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
f : Filter α
m : α → β
rw : map m f = ⊥ ↔ f = ⊥
⊢ ⊥ = map m f ↔ f = ⊥
have rw₁ : f = ⊥ ↔ f = ⊥
Tactic: rw [eq_comm, map_eq_bot_iff]
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
F : Filter β
⊢ ⋂₀ (comap f F).sets = ⋂ U ∈ F, f ⁻¹' U
have h : ∀ (x : α), x ∈ ⋂₀ (comap f F).sets ↔ Membership.mem (γ := Set α) (⋂ U ∈ F, f ⁻¹' U) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
F : Filter β
x : α
⊢ x ∈ ⋂₀ (comap f F).sets ↔ Membership.mem (γ := Set α) (⋂ U ∈ F, f ⁻¹' U) x
have h : (∀ (A : Set α), ∀ B ∈ F, f ⁻¹' B ⊆ A → x ∈ A) ↔ ∀ B ∈ F, f x ∈ B
Tactic: suffices (∀ (A : Set α) (B : Set β), B ∈ F → f ⁻¹' B ⊆ A → x ∈ A) ↔
      ∀ B : Set β, B ∈ F → f x ∈ B by
    simp only [mem_sInter, mem_iInter, Filter.mem_sets, mem_comap, this, and_imp,
      mem_preimage, exists_imp]
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
F : Filter β
x : α
⊢ (∀ (A : Set α), ∀ B ∈ F, f ⁻¹' B ⊆ A → x ∈ A) ↔ ∀ B ∈ F, f x ∈ B
have h : (∀ (A : Set α), ∀ B ∈ F, f ⁻¹' B ⊆ A → x ∈ A) → ∀ B ∈ F, f x ∈ B
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
F : Filter β
x : α
h : (∀ (A : Set α), ∀ B ∈ F, f ⁻¹' B ⊆ A → x ∈ A) → ∀ B ∈ F, f x ∈ B
⊢ (∀ (A : Set α), ∀ B ∈ F, f ⁻¹' B ⊆ A → x ∈ A) ↔ ∀ B ∈ F, f x ∈ B
have h₁ : (∀ B ∈ F, f x ∈ B) → ∀ (A : Set α), ∀ B ∈ F, f ⁻¹' B ⊆ A → x ∈ A
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Filter.Map (hypothesis)
Goal:
α : Type u_1
β : Type u_2
ι : Type w
f : ι → Filter α
m : α → β
p : ι → Prop
h : DirectedOn (f ⁻¹'o fun (x1 x2 : Filter α) ↦ x1 ≥ x2) {x : ι | p x}
ne : ∃ (i : ι), p i
⊢ map m (⨅ (i : ι), ⨅ (_ : p i), f i) = ⨅ (i : ι), ⨅ (_ : p i), map m (f i)
have this : Nonempty.{max 1 (w + 1)} (Subtype p)
Tactic: haveI := nonempty_subtype.2 ne
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type w
f : ι → Filter α
m : α → β
p : ι → Prop
h : DirectedOn (f ⁻¹'o fun (x1 x2 : Filter α) ↦ x1 ≥ x2) {x : ι | p x}
ne : ∃ (i : ι), p i
this : Nonempty.{max 1 (w + 1)} (Subtype p)
⊢ map m (⨅ (i : ι), ⨅ (_ : p i), f i) = ⨅ (i : ι), ⨅ (_ : p i), map m (f i)
have simp : map m (⨅ (x : Subtype p), f (↑x : ι)) = ⨅ (x : Subtype p), map m (f (↑x : ι))
Tactic: simp only [iInf_subtype']
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
f g : Filter α
m : α → β
h : Injective m
⊢ map m (f ⊓ g) = map m f ⊓ map m g
have refine : map m f ⊓ map m g ≤ map m (f ⊓ g)
Tactic: refine map_inf_le.antisymm ?_
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
f g : Filter α
m : α → β
h : Injective m
t : Set β
s₁ : Set α
hs₁ : s₁ ∈ f
s₂ : Set α
hs₂ : s₂ ∈ g
ht : m ⁻¹' t = s₁ ∩ s₂
⊢ t ∈ map m f ⊓ map m g
have refine : m '' s₁ ∩ m '' s₂ ⊆ t
Tactic: refine mem_inf_of_inter (image_mem_map hs₁) (image_mem_map hs₂) ?_
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
f g : Filter α
m : α → β
h : Injective m
t : Set β
s₁ : Set α
hs₁ : s₁ ∈ f
s₂ : Set α
hs₂ : s₂ ∈ g
ht : m ⁻¹' t = s₁ ∩ s₂
⊢ m '' s₁ ∩ m '' s₂ ⊆ t
have rw : m '' (s₁ ∩ s₂) ⊆ t
Tactic: rw [← image_inter h, image_subset_iff, ht]
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
f g : Filter α
m : α → β
h : Injective m
t : Set β
s₁ : Set α
hs₁ : s₁ ∈ f
s₂ : Set α
hs₂ : s₂ ∈ g
ht : m ⁻¹' t = s₁ ∩ s₂
rw : m '' (s₁ ∩ s₂) ⊆ t
⊢ m '' s₁ ∩ m '' s₂ ⊆ t
have rw₁ : s₁ ∩ s₂ ⊆ m ⁻¹' t
Tactic: rw [← image_inter h, image_subset_iff, ht]
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
f g : Filter α
m : α → β
h : Injective m
t : Set β
s₁ : Set α
hs₁ : s₁ ∈ f
s₂ : Set α
hs₂ : s₂ ∈ g
ht : m ⁻¹' t = s₁ ∩ s₂
rw : m '' (s₁ ∩ s₂) ⊆ t
rw₁ : s₁ ∩ s₂ ⊆ m ⁻¹' t
⊢ m '' s₁ ∩ m '' s₂ ⊆ t
have rw₂ : s₁ ∩ s₂ ⊆ s₁ ∩ s₂
Tactic: rw [← image_inter h, image_subset_iff, ht]
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
f g : Filter α
m : α → β
t : Set α
htf : t ∈ f
htg : t ∈ g
h : InjOn m t
⊢ map m (f ⊓ g) = map m f ⊓ map m g
have lift : ∀ (f : Filter (↑t : Type u_1)),
  map m (map (Subtype.val (p := fun (x : α) ↦ x ∈ t)) f ⊓ g) =
    map m (map (Subtype.val (p := fun (x : α) ↦ x ∈ t)) f) ⊓ map m g
Tactic: lift f to Filter t using htf
Cleared hypotheses: f, htf
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
g : Filter α
m : α → β
t : Set α
htg : t ∈ g
h : InjOn m t
f : Filter (↑t : Type u_1)
⊢ map m (map (Subtype.val (p := fun (x : α) ↦ x ∈ t)) f ⊓ g) =
    map m (map (Subtype.val (p := fun (x : α) ↦ x ∈ t)) f) ⊓ map m g
have lift : ∀ (g : Filter (↑t : Type u_1)),
  map m (map (Subtype.val (p := fun (x : α) ↦ x ∈ t)) f ⊓ map (Subtype.val (p := fun (x : α) ↦ x ∈ t)) g) =
    map m (map (Subtype.val (p := fun (x : α) ↦ x ∈ t)) f) ⊓ map m (map (Subtype.val (p := fun (x : α) ↦ x ∈ t)) g)
Tactic: lift g to Filter t using htg
Cleared hypotheses: g, htg
-- Lean 4 proof step from Mathlib.Order.Filter.Map (hypothesis)
Goal:
α : Type u_1
β : Type u_2
m : α → β
t : Set α
h : InjOn m t
f g : Filter (↑t : Type u_1)
⊢ map m (map (Subtype.val (p := fun (x : α) ↦ x ∈ t)) f ⊓ map (Subtype.val (p := fun (x : α) ↦ x ∈ t)) g) =
    map m (map (Subtype.val (p := fun (x : α) ↦ x ∈ t)) f) ⊓ map m (map (Subtype.val (p := fun (x : α) ↦ x ∈ t)) g)
have h₁ : Injective (α := { x : α // x ∈ t }) (m ∘ Subtype.val (p := fun (x : α) ↦ x ∈ t))
Tactic: replace h : Injective (m ∘ ((↑) : t → α)) := h.injective
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
f : Filter β
⊢ Eq.{u_2 + 1} (α := Filter β) (map.{u_1, u_2} (α := α) (⇑e : (a : α) → β) (map (⇑e.symm : (a : β) → α) f))
    (map.{u_1, u_2} (α := α) (⇑e : (a : α) → β) (comap (⇑e : (a : α) → β) f))
have rw : Eq (α := Filter β) (map (comp.{u_2 + 1, u_1 + 1, u_2 + 1} (β := α) (⇑e : (a : α) → β) (⇑e.symm : (a : β) → α)) f)
  (map.{u_1, u_2} (α := α) (⇑e : (a : α) → β) (comap (⇑e : (a : α) → β) f))
Tactic: rw [map_map, e.self_comp_symm, map_id, map_comap_of_surjective e.surjective]
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
f : Filter β
rw :
  Eq (α := Filter β) (map (comp.{u_2 + 1, u_1 + 1, u_2 + 1} (β := α) (⇑e : (a : α) → β) (⇑e.symm : (a : β) → α)) f)
    (map.{u_1, u_2} (α := α) (⇑e : (a : α) → β) (comap (⇑e : (a : α) → β) f))
⊢ Eq.{u_2 + 1} (α := Filter β) (map.{u_1, u_2} (α := α) (⇑e : (a : α) → β) (map (⇑e.symm : (a : β) → α) f))
    (map.{u_1, u_2} (α := α) (⇑e : (a : α) → β) (comap (⇑e : (a : α) → β) f))
have rw₁ : map id f = map.{u_1, u_2} (α := α) (⇑e : (a : α) → β) (comap (⇑e : (a : α) → β) f)
Tactic: rw [map_map, e.self_comp_symm, map_id, map_comap_of_surjective e.surjective]
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
f : Filter β
rw :
  Eq (α := Filter β) (map (comp.{u_2 + 1, u_1 + 1, u_2 + 1} (β := α) (⇑e : (a : α) → β) (⇑e.symm : (a : β) → α)) f)
    (map.{u_1, u_2} (α := α) (⇑e : (a : α) → β) (comap (⇑e : (a : α) → β) f))
rw₁ : map id f = map.{u_1, u_2} (α := α) (⇑e : (a : α) → β) (comap (⇑e : (a : α) → β) f)
⊢ Eq.{u_2 + 1} (α := Filter β) (map.{u_1, u_2} (α := α) (⇑e : (a : α) → β) (map (⇑e.symm : (a : β) → α) f))
    (map.{u_1, u_2} (α := α) (⇑e : (a : α) → β) (comap (⇑e : (a : α) → β) f))
have rw₂ : f = map.{u_1, u_2} (α := α) (⇑e : (a : α) → β) (comap (⇑e : (a : α) → β) f)
Tactic: rw [map_map, e.self_comp_symm, map_id, map_comap_of_surjective e.surjective]
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
f : Filter β
rw :
  Eq (α := Filter β) (map (comp.{u_2 + 1, u_1 + 1, u_2 + 1} (β := α) (⇑e : (a : α) → β) (⇑e.symm : (a : β) → α)) f)
    (map.{u_1, u_2} (α := α) (⇑e : (a : α) → β) (comap (⇑e : (a : α) → β) f))
rw₁ : map id f = map.{u_1, u_2} (α := α) (⇑e : (a : α) → β) (comap (⇑e : (a : α) → β) f)
rw₂ : f = map.{u_1, u_2} (α := α) (⇑e : (a : α) → β) (comap (⇑e : (a : α) → β) f)
⊢ Eq.{u_2 + 1} (α := Filter β) (map.{u_1, u_2} (α := α) (⇑e : (a : α) → β) (map (⇑e.symm : (a : β) → α) f))
    (map.{u_1, u_2} (α := α) (⇑e : (a : α) → β) (comap (⇑e : (a : α) → β) f))
have rw₃ : f = f
Tactic: rw [map_map, e.self_comp_symm, map_id, map_comap_of_surjective e.surjective]
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
F : Filter α
G : Filter β
⊢ map f (F ⊓ comap f G) = map f F ⊓ G
have a : map f (F ⊓ comap f G) ≤ map f F ⊓ G
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
F : Filter α
G : Filter β
a : map f (F ⊓ comap f G) ≤ map f F ⊓ G
⊢ map f (F ⊓ comap f G) = map f F ⊓ G
have a₁ : map f F ⊓ G ≤ map f (F ⊓ comap f G)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
F : Filter α
G : Filter β
U : Set β
V : Set α
V_in : V ∈ F
W : Set α
h : f ⁻¹' U = V ∩ W
Z : Set β
Z_in : Z ∈ G
hZ : f ⁻¹' Z ⊆ W
⊢ U ∈ map f F ⊓ G
have a : f '' V ∩ Z ⊆ U
Tactic: apply mem_inf_of_inter (image_mem_map V_in) Z_in
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
F : Filter α
G : Filter β
U : Set β
V : Set α
V_in : V ∈ F
W : Set α
h : f ⁻¹' U = V ∩ W
Z : Set β
Z_in : Z ∈ G
hZ : f ⁻¹' Z ⊆ W
⊢ f '' V ∩ Z = f '' (V ∩ f ⁻¹' Z)
have rw : f '' V ∩ Z = f '' V ∩ Z
Tactic: rw [image_inter_preimage]
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
F : Filter α
G : Filter β
U : Set β
V : Set α
V_in : V ∈ F
W : Set α
h : f ⁻¹' U = V ∩ W
Z : Set β
Z_in : Z ∈ G
hZ : f ⁻¹' Z ⊆ W
⊢ f '' (V ∩ W) = f '' f ⁻¹' U
have rw : f '' (V ∩ W) = f '' (V ∩ W)
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
F : Filter α
G : Filter β
U : Set β
V : Set α
V_in : V ∈ F
W : Set α
h : f ⁻¹' U = V ∩ W
Z : Set β
Z_in : Z ∈ G
hZ : f ⁻¹' Z ⊆ W
⊢ f '' V ∩ Z ⊆ U
have f₁ : f '' V ∩ Z = f '' (V ∩ f ⁻¹' Z)
Tactic: calc
      f '' V ∩ Z = f '' (V ∩ f ⁻¹' Z) := by rw [image_inter_preimage]
      _ ⊆ f '' (V ∩ W) := by gcongr
      _ = f '' f ⁻¹' U := by rw [h]
      _ ⊆ U := image_preimage_subset f U
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
F : Filter α
G : Filter β
U : Set β
V : Set α
V_in : V ∈ F
W : Set α
h : f ⁻¹' U = V ∩ W
Z : Set β
Z_in : Z ∈ G
hZ : f ⁻¹' Z ⊆ W
f₁ : f '' V ∩ Z = f '' (V ∩ f ⁻¹' Z)
⊢ f '' V ∩ Z ⊆ U
have f₂ : f '' (V ∩ f ⁻¹' Z) ⊆ f '' (V ∩ W)
Tactic: calc
      f '' V ∩ Z = f '' (V ∩ f ⁻¹' Z) := by rw [image_inter_preimage]
      _ ⊆ f '' (V ∩ W) := by gcongr
      _ = f '' f ⁻¹' U := by rw [h]
      _ ⊆ U := image_preimage_subset f U
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
F : Filter α
G : Filter β
U : Set β
V : Set α
V_in : V ∈ F
W : Set α
h : f ⁻¹' U = V ∩ W
Z : Set β
Z_in : Z ∈ G
hZ : f ⁻¹' Z ⊆ W
f₁ : f '' V ∩ Z = f '' (V ∩ f ⁻¹' Z)
f₂ : f '' (V ∩ f ⁻¹' Z) ⊆ f '' (V ∩ W)
⊢ f '' V ∩ Z ⊆ U
have f₃ : f '' (V ∩ W) = f '' f ⁻¹' U
Tactic: calc
      f '' V ∩ Z = f '' (V ∩ f ⁻¹' Z) := by rw [image_inter_preimage]
      _ ⊆ f '' (V ∩ W) := by gcongr
      _ = f '' f ⁻¹' U := by rw [h]
      _ ⊆ U := image_preimage_subset f U
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
F : Filter α
G : Filter β
⊢ (F ⊓ comap f G).NeBot ↔ (map f F ⊓ G).NeBot
have rw : (map f (F ⊓ comap f G)).NeBot ↔ (map f F ⊓ G).NeBot
Tactic: rw [← map_neBot_iff, Filter.push_pull]
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
F : Filter α
G : Filter β
rw : (map f (F ⊓ comap f G)).NeBot ↔ (map f F ⊓ G).NeBot
f₁ : α → β
rw₁ : Type u_2
⊢ (F ⊓ comap f G).NeBot ↔ (map f F ⊓ G).NeBot
have rw₂ : (map f F ⊓ G).NeBot ↔ (map f F ⊓ G).NeBot
Tactic: rw [← map_neBot_iff, Filter.push_pull]
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
F : Filter α
G : Filter β
⊢ (comap f G ⊓ F).NeBot ↔ (G ⊓ map f F).NeBot
have rw : (map f (comap f G ⊓ F)).NeBot ↔ (G ⊓ map f F).NeBot
Tactic: rw [← map_neBot_iff, Filter.push_pull']
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
F : Filter α
G : Filter β
rw : (map f (comap f G ⊓ F)).NeBot ↔ (G ⊓ map f F).NeBot
f₁ : α → β
rw₁ : Type u_2
⊢ (comap f G ⊓ F).NeBot ↔ (G ⊓ map f F).NeBot
have rw₂ : (G ⊓ map f F).NeBot ↔ (G ⊓ map f F).NeBot
Tactic: rw [← map_neBot_iff, Filter.push_pull']
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
f : Filter β
m : α → β
hf : f.NeBot
s : Set α
hs : m '' s ∈ f
⊢ (comap m f ⊓ 𝓟 s).NeBot
have rw : ∃ᶠ (x : β) in f, x ∈ m '' s
Tactic: rw [neBot_inf_comap_iff_map', map_principal, ← frequently_mem_iff_neBot]
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
F : Filter α
s : Set α
⊢ F ⊓ 𝓟 s = ⊥ ↔ Eq (α := Filter { x : α // x ∈ s }) (comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) F) ⊥
have rw : F ⊓ map (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s)) ⊤ = ⊥ ↔
  Eq (α := Filter { x : α // x ∈ s }) (comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) F) ⊥
Tactic: rw [principal_eq_map_coe_top s, ← Filter.push_pull', inf_top_eq, map_eq_bot_iff]
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
F : Filter α
s : Set α
rw :
  F ⊓ map (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s)) ⊤ = ⊥ ↔
    Eq (α := Filter { x : α // x ∈ s }) (comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) F) ⊥
⊢ F ⊓ 𝓟 s = ⊥ ↔ Eq (α := Filter { x : α // x ∈ s }) (comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) F) ⊥
have rw₁ : map (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s))
      (comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) F ⊓ ⊤) =
    ⊥ ↔
  Eq (α := Filter { x : α // x ∈ s }) (comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) F) ⊥
Tactic: rw [principal_eq_map_coe_top s, ← Filter.push_pull', inf_top_eq, map_eq_bot_iff]
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
F : Filter α
s : Set α
rw :
  F ⊓ map (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s)) ⊤ = ⊥ ↔
    Eq (α := Filter { x : α // x ∈ s }) (comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) F) ⊥
rw₁ :
  map (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s))
        (comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) F ⊓ ⊤) =
      ⊥ ↔
    Eq (α := Filter { x : α // x ∈ s }) (comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) F) ⊥
⊢ F ⊓ 𝓟 s = ⊥ ↔ Eq (α := Filter { x : α // x ∈ s }) (comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) F) ⊥
have rw₂ : map (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s))
      (comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) F) =
    ⊥ ↔
  Eq (α := Filter { x : α // x ∈ s }) (comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) F) ⊥
Tactic: rw [principal_eq_map_coe_top s, ← Filter.push_pull', inf_top_eq, map_eq_bot_iff]
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
F : Filter α
s : Set α
rw :
  F ⊓ map (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s)) ⊤ = ⊥ ↔
    Eq (α := Filter { x : α // x ∈ s }) (comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) F) ⊥
rw₁ :
  map (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s))
        (comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) F ⊓ ⊤) =
      ⊥ ↔
    Eq (α := Filter { x : α // x ∈ s }) (comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) F) ⊥
rw₂ :
  map (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s))
        (comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) F) =
      ⊥ ↔
    Eq (α := Filter { x : α // x ∈ s }) (comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) F) ⊥
⊢ F ⊓ 𝓟 s = ⊥ ↔ Eq (α := Filter { x : α // x ∈ s }) (comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) F) ⊥
have rw₃ : Eq (α := Filter { x : α // x ∈ s }) (comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) F) ⊥ ↔
  Eq (α := Filter { x : α // x ∈ s }) (comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) F) ⊥
Tactic: rw [principal_eq_map_coe_top s, ← Filter.push_pull', inf_top_eq, map_eq_bot_iff]
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
U : Set (Set β)
f : β → α
⊢ map f (generate U) ≤ generate ((fun (x : Set α) ↦ f ⁻¹' x) ⁻¹' U)
have rw : (fun (x : Set α) ↦ f ⁻¹' x) ⁻¹' U ⊆ (map f (generate U)).sets
Tactic: rw [le_generate_iff]
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
U : Set (Set α)
f : β → α
⊢ generate ((fun (x : Set α) ↦ f ⁻¹' x) '' U) ≤ comap f (generate U)
have rw : U ⊆ (map f (generate ((fun (x : Set α) ↦ f ⁻¹' x) '' U))).sets
Tactic: rw [← map_le_iff_le_comap, le_generate_iff]
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
f : Filter α
a : α
⊢ f ≤ pure a ↔ {a} ∈ f
have rw : f ≤ 𝓟 {a} ↔ {a} ∈ f
Tactic: rw [← principal_singleton, le_principal_iff]
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
f : Filter α
a : α
rw : f ≤ 𝓟 {a} ↔ {a} ∈ f
⊢ f ≤ pure a ↔ {a} ∈ f
have rw₁ : {a} ∈ f ↔ {a} ∈ f
Tactic: rw [← principal_singleton, le_principal_iff]
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
g : α → β
f : Filter α
⊢ seq (pure g) f = map g f
have refine_1 : ∀ (s : Set α) (hs : s ∈ f), g '' s ∈ seq (pure g) f
Tactic: refine le_antisymm (le_map fun s hs => ?_) (le_seq fun s hs t ht => ?_)
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
g : α → β
f : Filter α
refine_1 : ∀ (s : Set α) (hs : s ∈ f), g '' s ∈ seq (pure g) f
⊢ seq (pure g) f = map g f
have refine_2 : ∀ (s : Set (α → β)) (hs : Membership.mem (γ := Filter (α → β)) (pure g) s) (t : Set α) (ht : t ∈ f), s.seq t ∈ map g f
Tactic: refine le_antisymm (le_map fun s hs => ?_) (le_seq fun s hs t ht => ?_)
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
g : α → β
f : Filter α
s : Set α
hs : s ∈ f
⊢ g '' s ∈ seq (pure g) f
have refine_1 : Set.seq {g} s ∈ seq (pure g) f
Tactic: rw [← singleton_seq]
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
g : α → β
f : Filter α
s : Set α
hs : s ∈ f
⊢ Set.seq {g} s ∈ seq (pure g) f
have apply : Membership.mem (γ := Filter (α → β)) (pure g) {g}
Tactic: apply seq_mem_seq _ hs
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
g : α → β
f : Filter α
s : Set (α → β)
hs : Membership.mem (γ := Filter (α → β)) (pure g) s
t : Set α
ht : t ∈ f
⊢ s.seq t ∈ map g f
have refine_2 : g '' t ⊆ s.seq t
Tactic: refine sets_of_superset (map g f) (image_mem_map ht) ?_
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
f : Filter (α → β)
a : α
⊢ f.seq (pure a) = map (fun (g : α → β) ↦ g a) f
have refine_1 : ∀ (s : Set (α → β)) (hs : s ∈ f), (fun (g : α → β) ↦ g a) '' s ∈ f.seq (pure a)
Tactic: refine le_antisymm (le_map fun s hs => ?_) (le_seq fun s hs t ht => ?_)