awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
f : Filter (α → β)
a : α
refine_1 : ∀ (s : Set (α → β)) (hs : s ∈ f), (fun (g : α → β) ↦ g a) '' s ∈ f.seq (pure a)
⊢ f.seq (pure a) = map (fun (g : α → β) ↦ g a) f
have refine_2 : ∀ (s : Set (α → β)) (hs : s ∈ f) (t : Set α) (ht : Membership.mem (γ := Filter α) (pure a) t),
  Membership.mem (γ := Filter β) (map (fun (g : α → β) ↦ g a) f) (s.seq t)
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
f : Filter (α → β)
a : α
s : Set (α → β)
hs : s ∈ f
⊢ (fun (g : α → β) ↦ g a) '' s ∈ f.seq (pure a)
have refine_1 : s.seq {a} ∈ f.seq (pure a)
Tactic: rw [← seq_singleton]
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
f : Filter (α → β)
a : α
s : Set (α → β)
hs : s ∈ f
t : Set α
ht : Membership.mem (γ := Filter α) (pure a) t
⊢ Membership.mem (γ := Filter β) (map (fun (g : α → β) ↦ g a) f) (s.seq t)
have refine_2 : (fun (g : α → β) ↦ g a) '' s ⊆ s.seq t
Tactic: refine sets_of_superset (map (fun g : α → β => g a) f) (image_mem_map hs) ?_
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
x : Filter α
g : Filter (α → β)
h : Filter (β → γ)
⊢ h.seq (g.seq x) = seq (seq (map (fun (x1 : β → γ) (x2 : α → β) ↦ x1 ∘ x2) h) g) x
have refine_1 : ∀ (s : Set (α → γ))
  (hs : Membership.mem (γ := Filter (α → γ)) (seq (map (fun (x1 : β → γ) (x2 : α → β) ↦ x1 ∘ x2) h) g) s) (t : Set α)
  (ht : t ∈ x), s.seq t ∈ h.seq (g.seq x)
Tactic: refine le_antisymm (le_seq fun s hs t ht => ?_) (le_seq fun s hs t ht => ?_)
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
x : Filter α
g : Filter (α → β)
h : Filter (β → γ)
refine_1 :
  ∀ (s : Set (α → γ))
    (hs : Membership.mem (γ := Filter (α → γ)) (seq (map (fun (x1 : β → γ) (x2 : α → β) ↦ x1 ∘ x2) h) g) s) (t : Set α)
    (ht : t ∈ x), s.seq t ∈ h.seq (g.seq x)
⊢ h.seq (g.seq x) = seq (seq (map (fun (x1 : β → γ) (x2 : α → β) ↦ x1 ∘ x2) h) g) x
have refine_2 : ∀ (s : Set (β → γ)) (hs : s ∈ h) (t : Set β) (ht : t ∈ g.seq x),
  Membership.mem (γ := Filter γ) (seq (seq (map (fun (x1 : β → γ) (x2 : α → β) ↦ x1 ∘ x2) h) g) x) (s.seq t)
Tactic: refine le_antisymm (le_seq fun s hs t ht => ?_) (le_seq fun s hs t ht => ?_)
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
x : Filter α
g : Filter (α → β)
h : Filter (β → γ)
s : Set (α → γ)
hs : Membership.mem (γ := Filter (α → γ)) (seq (map (fun (x1 : β → γ) (x2 : α → β) ↦ x1 ∘ x2) h) g) s
t : Set α
ht : t ∈ x
⊢ s.seq t ∈ h.seq (g.seq x)
have refine_1 : ∀ (u : Set ((α → β) → α → γ))
  (hu : Membership.mem (γ := Filter ((α → β) → α → γ)) (map (fun (x1 : β → γ) (x2 : α → β) ↦ x1 ∘ x2) h) u)
  (v : Set (α → β)) (hv : v ∈ g) (hs : u.seq v ⊆ s), s.seq t ∈ h.seq (g.seq x)
Tactic: rcases mem_seq_iff.1 hs with ⟨u, hu, v, hv, hs⟩
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
x : Filter α
g : Filter (α → β)
h : Filter (β → γ)
s : Set (α → γ)
hs_1 : Membership.mem (γ := Filter (α → γ)) (seq (map (fun (x1 : β → γ) (x2 : α → β) ↦ x1 ∘ x2) h) g) s
t : Set α
ht : t ∈ x
u : Set ((α → β) → α → γ)
hu : Membership.mem (γ := Filter ((α → β) → α → γ)) (map (fun (x1 : β → γ) (x2 : α → β) ↦ x1 ∘ x2) h) u
v : Set (α → β)
hv : v ∈ g
hs : u.seq v ⊆ s
⊢ s.seq t ∈ h.seq (g.seq x)
have refine_1 : ∀ (w : Set (β → γ)) (hw : w ∈ h) (hu : (fun (x1 : β → γ) (x2 : α → β) ↦ x1 ∘ x2) '' w ⊆ u), s.seq t ∈ h.seq (g.seq x)
Tactic: rcases mem_map_iff_exists_image.1 hu with ⟨w, hw, hu⟩
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
x : Filter α
g : Filter (α → β)
h : Filter (β → γ)
s : Set (α → γ)
hs_1 : Membership.mem (γ := Filter (α → γ)) (seq (map (fun (x1 : β → γ) (x2 : α → β) ↦ x1 ∘ x2) h) g) s
t : Set α
ht : t ∈ x
u : Set ((α → β) → α → γ)
hu_1 : Membership.mem (γ := Filter ((α → β) → α → γ)) (map (fun (x1 : β → γ) (x2 : α → β) ↦ x1 ∘ x2) h) u
v : Set (α → β)
hv : v ∈ g
hs : u.seq v ⊆ s
w : Set (β → γ)
hw : w ∈ h
hu : (fun (x1 : β → γ) (x2 : α → β) ↦ x1 ∘ x2) '' w ⊆ u
⊢ s.seq t ∈ h.seq (g.seq x)
have refine_1 : Set.seq (Set.seq ((fun (x1 : β → γ) (x2 : α → β) ↦ x1 ∘ x2) '' w) v) t ∈ h.seq (g.seq x)
Tactic: grw [← hs, ← hu]
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
x : Filter α
g : Filter (α → β)
h : Filter (β → γ)
s : Set (α → γ)
hs_1 : Membership.mem (γ := Filter (α → γ)) (seq (map (fun (x1 : β → γ) (x2 : α → β) ↦ x1 ∘ x2) h) g) s
t : Set α
ht : t ∈ x
u : Set ((α → β) → α → γ)
hu_1 : Membership.mem (γ := Filter ((α → β) → α → γ)) (map (fun (x1 : β → γ) (x2 : α → β) ↦ x1 ∘ x2) h) u
v : Set (α → β)
hv : v ∈ g
hs : u.seq v ⊆ s
w : Set (β → γ)
hw : w ∈ h
hu : (fun (x1 : β → γ) (x2 : α → β) ↦ x1 ∘ x2) '' w ⊆ u
⊢ Set.seq (Set.seq ((fun (x1 : β → γ) (x2 : α → β) ↦ x1 ∘ x2) '' w) v) t ∈ h.seq (g.seq x)
have refine_1 : w.seq (v.seq t) ∈ h.seq (g.seq x)
Tactic: rw [← Set.seq_seq]
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
x : Filter α
g : Filter (α → β)
h : Filter (β → γ)
s : Set (β → γ)
hs : s ∈ h
t : Set β
ht : t ∈ g.seq x
⊢ Membership.mem (γ := Filter γ) (seq (seq (map (fun (x1 : β → γ) (x2 : α → β) ↦ x1 ∘ x2) h) g) x) (s.seq t)
have refine_2 : ∀ (u : Set (α → β)) (hu : u ∈ g) (v : Set α) (hv : v ∈ x) (ht : u.seq v ⊆ t),
  Membership.mem (γ := Filter γ) (seq (seq (map (fun (x1 : β → γ) (x2 : α → β) ↦ x1 ∘ x2) h) g) x) (s.seq t)
Tactic: rcases mem_seq_iff.1 ht with ⟨u, hu, v, hv, ht⟩
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
x : Filter α
g : Filter (α → β)
h : Filter (β → γ)
s : Set (β → γ)
hs : s ∈ h
t : Set β
ht_1 : t ∈ g.seq x
u : Set (α → β)
hu : u ∈ g
v : Set α
hv : v ∈ x
ht : u.seq v ⊆ t
⊢ Membership.mem (γ := Filter γ) (seq (seq (map (fun (x1 : β → γ) (x2 : α → β) ↦ x1 ∘ x2) h) g) x) (s.seq t)
have refine_2 : Membership.mem (γ := Filter γ) (seq (seq (map (fun (x1 : β → γ) (x2 : α → β) ↦ x1 ∘ x2) h) g) x) (s.seq (u.seq v))
Tactic: grw [← ht]
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
x : Filter α
g : Filter (α → β)
h : Filter (β → γ)
s : Set (β → γ)
hs : s ∈ h
t : Set β
ht_1 : t ∈ g.seq x
u : Set (α → β)
hu : u ∈ g
v : Set α
hv : v ∈ x
ht : u.seq v ⊆ t
⊢ Membership.mem (γ := Filter γ) (seq (seq (map (fun (x1 : β → γ) (x2 : α → β) ↦ x1 ∘ x2) h) g) x) (s.seq (u.seq v))
have refine_2 : Membership.mem (γ := Filter γ) (seq (seq (map (fun (x1 : β → γ) (x2 : α → β) ↦ x1 ∘ x2) h) g) x)
  (Set.seq (Set.seq ((fun (x1 : β → γ) (x2 : α → β) ↦ x1 ∘ x2) '' s) u) v)
Tactic: rw [Set.seq_seq]
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
⊢ seq (map Prod.mk f) g = seq (map (fun (b : β) (a : α) ↦ (a, b)) g) f
have refine_1 : ∀ (s : Set (α → α × β)) (hs : Membership.mem (γ := Filter (α → α × β)) (map (fun (b : β) (a : α) ↦ (a, b)) g) s)
  (t : Set α) (ht : t ∈ f), s.seq t ∈ seq (map Prod.mk f) g
Tactic: refine le_antisymm (le_seq fun s hs t ht => ?_) (le_seq fun s hs t ht => ?_)
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
refine_1 :
  ∀ (s : Set (α → α × β)) (hs : Membership.mem (γ := Filter (α → α × β)) (map (fun (b : β) (a : α) ↦ (a, b)) g) s)
    (t : Set α) (ht : t ∈ f), s.seq t ∈ seq (map Prod.mk f) g
⊢ seq (map Prod.mk f) g = seq (map (fun (b : β) (a : α) ↦ (a, b)) g) f
have refine_2 : ∀ (s : Set (β → α × β)) (hs : Membership.mem (γ := Filter (β → α × β)) (map Prod.mk f) s) (t : Set β) (ht : t ∈ g),
  Membership.mem (γ := Filter (α × β)) (seq (map (fun (b : β) (a : α) ↦ (a, b)) g) f) (s.seq t)
Tactic: refine le_antisymm (le_seq fun s hs t ht => ?_) (le_seq fun s hs t ht => ?_)
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
s : Set (α → α × β)
hs : Membership.mem (γ := Filter (α → α × β)) (map (fun (b : β) (a : α) ↦ (a, b)) g) s
t : Set α
ht : t ∈ f
⊢ s.seq t ∈ seq (map Prod.mk f) g
have refine_1 : ∀ (u : Set β) (hu : u ∈ g) (hs : (fun (b : β) (a : α) ↦ (a, b)) '' u ⊆ s), s.seq t ∈ seq (map Prod.mk f) g
Tactic: rcases mem_map_iff_exists_image.1 hs with ⟨u, hu, hs⟩
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
s : Set (α → α × β)
hs_1 : Membership.mem (γ := Filter (α → α × β)) (map (fun (b : β) (a : α) ↦ (a, b)) g) s
t : Set α
ht : t ∈ f
u : Set β
hu : u ∈ g
hs : (fun (b : β) (a : α) ↦ (a, b)) '' u ⊆ s
⊢ s.seq t ∈ seq (map Prod.mk f) g
have refine_1 : Set.seq ((fun (b : β) (a : α) ↦ (a, b)) '' u) t ∈ seq (map Prod.mk f) g
Tactic: grw [← hs]
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
s : Set (α → α × β)
hs_1 : Membership.mem (γ := Filter (α → α × β)) (map (fun (b : β) (a : α) ↦ (a, b)) g) s
t : Set α
ht : t ∈ f
u : Set β
hu : u ∈ g
hs : (fun (b : β) (a : α) ↦ (a, b)) '' u ⊆ s
⊢ Set.seq ((fun (b : β) (a : α) ↦ (a, b)) '' u) t ∈ seq (map Prod.mk f) g
have refine_1 : Set.seq (Prod.mk '' t) u ∈ seq (map Prod.mk f) g
Tactic: rw [← Set.prod_image_seq_comm]
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
s : Set (β → α × β)
hs : Membership.mem (γ := Filter (β → α × β)) (map Prod.mk f) s
t : Set β
ht : t ∈ g
⊢ Membership.mem (γ := Filter (α × β)) (seq (map (fun (b : β) (a : α) ↦ (a, b)) g) f) (s.seq t)
have refine_2 : ∀ (u : Set α) (hu : u ∈ f) (hs : Prod.mk '' u ⊆ s),
  Membership.mem (γ := Filter (α × β)) (seq (map (fun (b : β) (a : α) ↦ (a, b)) g) f) (s.seq t)
Tactic: rcases mem_map_iff_exists_image.1 hs with ⟨u, hu, hs⟩
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
s : Set (β → α × β)
hs_1 : Membership.mem (γ := Filter (β → α × β)) (map Prod.mk f) s
t : Set β
ht : t ∈ g
u : Set α
hu : u ∈ f
hs : Prod.mk '' u ⊆ s
⊢ Membership.mem (γ := Filter (α × β)) (seq (map (fun (b : β) (a : α) ↦ (a, b)) g) f) (s.seq t)
have refine_2 : Membership.mem (γ := Filter (α × β)) (seq (map (fun (b : β) (a : α) ↦ (a, b)) g) f) (Set.seq (Prod.mk '' u) t)
Tactic: grw [← hs]
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
s : Set (β → α × β)
hs_1 : Membership.mem (γ := Filter (β → α × β)) (map Prod.mk f) s
t : Set β
ht : t ∈ g
u : Set α
hu : u ∈ f
hs : Prod.mk '' u ⊆ s
⊢ Membership.mem (γ := Filter (α × β)) (seq (map (fun (b : β) (a : α) ↦ (a, b)) g) f) (Set.seq (Prod.mk '' u) t)
have refine_2 : Membership.mem (γ := Filter (α × β)) (seq (map (fun (b : β) (a : α) ↦ (a, b)) g) f)
  (Set.seq ((fun (b : β) (a : α) ↦ (a, b)) '' t) u)
Tactic: rw [Set.prod_image_seq_comm]
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
f : Filter α
m : α → Filter β
p : β → Prop
⊢ (∃ᶠ (y : β) in f.bind m, p y) ↔ ∃ᶠ (x : α) in f, ∃ᶠ (y : β) in m x, p y
have rw : (¬∃ᶠ (y : β) in f.bind m, p y) ↔ ¬∃ᶠ (x : α) in f, ∃ᶠ (y : β) in m x, p y
Tactic: rw [← not_iff_not]
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
f₁ f₂ : Filter α
g₁ g₂ : α → Filter β
hf : f₁ ≤ f₂
hg : g₁ ≤ᶠ[f₁] g₂
⊢ f₁.bind g₁ ≤ f₂.bind g₂
have refine : ∀ (s : Set β) (hs : s ∈ (map g₂ f₁).join), s ∈ f₁.bind g₁
Tactic: refine le_trans (fun s hs => ?_) (join_mono <| map_mono hf)
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
f₁ f₂ : Filter α
g₁ g₂ : α → Filter β
hf : f₁ ≤ f₂
hg : g₁ ≤ᶠ[f₁] g₂
s : Set β
hs : s ∈ (map g₂ f₁).join
⊢ s ∈ f₁.bind g₁
have simp : ∀ (hs : g₂ ⁻¹' {t : Filter β | s ∈ t} ∈ f₁), {a : α | s ∈ g₁ a} ∈ f₁
Tactic: simp only [mem_join, mem_bind', mem_map] at hs ⊢
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
f₁ f₂ : Filter α
g₁ g₂ : α → Filter β
hf : f₁ ≤ f₂
hg : g₁ ≤ᶠ[f₁] g₂
s : Set β
hs : g₂ ⁻¹' {t : Filter β | s ∈ t} ∈ f₁
⊢ {a : α | s ∈ g₁ a} ∈ f₁
have h : ∀ (a : α),
  Membership.mem (γ := Set α)
    {x : α |
      Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ g₁ x ≤ g₂ x) x} x →
        Membership.mem (γ := Set α)
          {x : α | x ∈ g₂ ⁻¹' {t : Filter β | s ∈ t} → Membership.mem (γ := Set α) {a : α | s ∈ g₁ a} x} x}
    a
Tactic: filter_upwards [hg, hs] with _ hx hs using hx hs
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
f₁ f₂ : Filter α
g₁ g₂ : α → Filter β
hf : f₁ ≤ f₂
hg : g₁ ≤ᶠ[f₁] g₂
s : Set β
hs : g₂ ⁻¹' {t : Filter β | s ∈ t} ∈ f₁
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ g₁ x ≤ g₂ x) x} x →
          Membership.mem (γ := Set α)
            {x : α | x ∈ g₂ ⁻¹' {t : Filter β | s ∈ t} → Membership.mem (γ := Set α) {a : α | s ∈ g₁ a} x} x}
      a
⊢ {a : α | s ∈ g₁ a} ∈ f₁
have h₁ : ∀ (a : α), g₁ a ≤ g₂ a → a ∈ g₂ ⁻¹' {t : Filter β | s ∈ t} → s ∈ g₁ a
Tactic: filter_upwards [hg, hs] with _ hx hs using hx hs
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
F : Filter α
G : Filter β
m : α → β
⊢ SurjOn (map m) (Iic F) (Iic G) ↔ G ≤ map m F
have refine_1 : ∀ (hm : SurjOn (map m) (Iic F) (Iic G)), G ≤ map m F
Tactic: refine ⟨fun hm ↦ ?_, fun hm ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
F : Filter α
G : Filter β
m : α → β
refine_1 : ∀ (hm : SurjOn (map m) (Iic F) (Iic G)), G ≤ map m F
⊢ SurjOn (map m) (Iic F) (Iic G) ↔ G ≤ map m F
have refine_2 : ∀ (hm : G ≤ map m F), SurjOn (map m) (Iic F) (Iic G)
Tactic: refine ⟨fun hm ↦ ?_, fun hm ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
F : Filter α
G : Filter β
m : α → β
hm : SurjOn (map m) (Iic F) (Iic G)
⊢ G ≤ map m F
have refine_1 : ∀ (H : Filter α) (hHF : H ≤ F) (hm : SurjOn (map m) (Iic F) (Iic (map m H))), map m H ≤ map m F
Tactic: rcases hm self_mem_Iic with ⟨H, (hHF : H ≤ F), rfl⟩
Cleared hypotheses: G, hm
-- Lean 4 proof step from Mathlib.Order.Filter.Map (hypothesis)
Goal:
α : Type u_1
β : Type u_2
F : Filter α
G : Filter β
m : α → β
hm : G ≤ map m F
⊢ SurjOn (map m) (Iic F) (Iic G)
have this : RightInvOn (fun (x : Filter β) ↦ F ⊓ comap m x) (map m) (Iic G)
Tactic: have : RightInvOn (F ⊓ comap m ·) (map m) (Iic G) :=
      fun H (hHG : H ≤ G) ↦ by simpa [Filter.push_pull] using hHG.trans hm
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
m : α → β
⊢ SurjOn (map m) (Iic (𝓟 s)) (Iic (𝓟 t)) ↔ SurjOn m s t
have rw : 𝓟 t ≤ map m (𝓟 s) ↔ SurjOn m s t
Tactic: rw [map_surjOn_Iic_iff_le_map, map_principal, principal_mono, SurjOn]
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
m : α → β
rw : 𝓟 t ≤ map m (𝓟 s) ↔ SurjOn m s t
⊢ SurjOn (map m) (Iic (𝓟 s)) (Iic (𝓟 t)) ↔ SurjOn m s t
have rw₁ : 𝓟 t ≤ 𝓟 (m '' s) ↔ SurjOn m s t
Tactic: rw [map_surjOn_Iic_iff_le_map, map_principal, principal_mono, SurjOn]
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
m : α → β
rw : 𝓟 t ≤ map m (𝓟 s) ↔ SurjOn m s t
rw₁ : 𝓟 t ≤ 𝓟 (m '' s) ↔ SurjOn m s t
⊢ SurjOn (map m) (Iic (𝓟 s)) (Iic (𝓟 t)) ↔ SurjOn m s t
have rw₂ : t ⊆ m '' s ↔ SurjOn m s t
Tactic: rw [map_surjOn_Iic_iff_le_map, map_principal, principal_mono, SurjOn]
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
m : α → β
rw : 𝓟 t ≤ map m (𝓟 s) ↔ SurjOn m s t
rw₁ : 𝓟 t ≤ 𝓟 (m '' s) ↔ SurjOn m s t
rw₂ : t ⊆ m '' s ↔ SurjOn m s t
⊢ SurjOn (map m) (Iic (𝓟 s)) (Iic (𝓟 t)) ↔ SurjOn m s t
have rw₃ : t ⊆ m '' s ↔ t ⊆ m '' s
Tactic: rw [map_surjOn_Iic_iff_le_map, map_principal, principal_mono, SurjOn]
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
m : α → β
⊢ InjOn (map m) (Iic (𝓟 s)) ↔ InjOn m s
have refine_1 : ∀ (hm : InjOn (map m) (Iic (𝓟 s))) (x : α) (hx : x ∈ s) (y : α) (hy : y ∈ s) (hxy : m x = m y), x = y
Tactic: refine ⟨fun hm x hx y hy hxy ↦ ?_, fun hm F hF G hG ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
m : α → β
refine_1 : ∀ (hm : InjOn (map m) (Iic (𝓟 s))) (x : α) (hx : x ∈ s) (y : α) (hy : y ∈ s) (hxy : m x = m y), x = y
⊢ InjOn (map m) (Iic (𝓟 s)) ↔ InjOn m s
have refine_2 : ∀ (hm : InjOn m s) (F : Filter α) (hF : F ∈ Iic (𝓟 s)) (G : Filter α) (hG : G ∈ Iic (𝓟 s)), map m F = map m G → F = G
Tactic: refine ⟨fun hm x hx y hy hxy ↦ ?_, fun hm F hF G hG ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
m : α → β
hm : InjOn (map m) (Iic (𝓟 s))
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : m x = m y
⊢ x = y
have refine_1 : ∀ (hxy : map m (pure x) = map m (pure y)), pure x ∈ Iic (𝓟 s)
Tactic: rwa [← pure_injective.eq_iff, ← map_pure, ← map_pure, hm.eq_iff, pure_injective.eq_iff]
      at hxy
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
m : α → β
hm : InjOn (map m) (Iic (𝓟 s))
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : m x = m y
refine_1 : ∀ (hxy : map m (pure x) = map m (pure y)), pure x ∈ Iic (𝓟 s)
⊢ x = y
have refine_1₁ : ∀ (hxy : map m (pure x) = map m (pure y)), pure y ∈ Iic (𝓟 s)
Tactic: rwa [← pure_injective.eq_iff, ← map_pure, ← map_pure, hm.eq_iff, pure_injective.eq_iff]
      at hxy
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
m : α → β
hm : InjOn (map m) (Iic (𝓟 s))
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : map m (pure x) = map m (pure y)
⊢ pure x ∈ Iic (𝓟 s)
have refine_1 : pure x ≤ 𝓟 s
Tactic: rwa [mem_Iic, pure_le_principal]
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
m : α → β
hm : InjOn (map m) (Iic (𝓟 s))
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : map m (pure x) = map m (pure y)
⊢ pure y ∈ Iic (𝓟 s)
have refine_1 : pure y ≤ 𝓟 s
Tactic: rwa [mem_Iic, pure_le_principal]
-- Lean 4 proof step from Mathlib.Order.Filter.NAry (goal)
Goal:
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
δ' : Type u_8
ε : Type u_9
ε' : Type u_10
m_1 : α → β → γ
f_1 f₁ f₂ : Filter α
g_1 g₁ g₂ : Filter β
h : Filter γ
s : Set α
t : Set β
u : Set γ
a : α
b : β
m : α → β → γ
f : Filter α
g : Filter β
x : Set γ
⊢ Membership.mem (γ := Set (Set γ)) {s : Set γ | ∃ u ∈ f, ∃ v ∈ g, image2 m u v ⊆ s} x ↔ x ∈ map (uncurry m) (f ×ˢ g)
have simp : Membership.mem (γ := Set (Set γ)) {s : Set γ | ∃ u ∈ f, ∃ v ∈ g, ∀ x ∈ u, ∀ y ∈ v, m x y ∈ s} x ↔
  ∃ t₁ ∈ f, ∃ t₂ ∈ g, ∀ x_1 ∈ t₁, ∀ y ∈ t₂, (x_1, y) ∈ uncurry m ⁻¹' x
Tactic: simp only [mem_map, mem_prod_iff, image2_subset_iff, prod_subset_iff]
-- Lean 4 proof step from Mathlib.Order.Filter.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
m : α → β → γ
f : Filter α
g : Filter β
⊢ map (fun (p : α × β) ↦ m p.1 p.2) (f ×ˢ g) = map₂ m f g
have rw : map (fun (p : α × β) ↦ m p.1 p.2) (f ×ˢ g) =
  (map (uncurry m) (f ×ˢ g)).copy {s : Set γ | ∃ u ∈ f, ∃ v ∈ g, image2 m u v ⊆ s} sorry
Tactic: rw [map₂, copy_eq, uncurry_def]
-- Lean 4 proof step from Mathlib.Order.Filter.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
m : α → β → γ
f : Filter α
g : Filter β
rw :
  map (fun (p : α × β) ↦ m p.1 p.2) (f ×ˢ g) =
    (map (uncurry m) (f ×ˢ g)).copy {s : Set γ | ∃ u ∈ f, ∃ v ∈ g, image2 m u v ⊆ s} ⋯
⊢ map (fun (p : α × β) ↦ m p.1 p.2) (f ×ˢ g) = map₂ m f g
have rw₁ : map (fun (p : α × β) ↦ m p.1 p.2) (f ×ˢ g) = map (uncurry m) (f ×ˢ g)
Tactic: rw [map₂, copy_eq, uncurry_def]
-- Lean 4 proof step from Mathlib.Order.Filter.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
m : α → β → γ
f : Filter α
g : Filter β
rw :
  map (fun (p : α × β) ↦ m p.1 p.2) (f ×ˢ g) =
    (map (uncurry m) (f ×ˢ g)).copy {s : Set γ | ∃ u ∈ f, ∃ v ∈ g, image2 m u v ⊆ s} ⋯
rw₁ : map (fun (p : α × β) ↦ m p.1 p.2) (f ×ˢ g) = map (uncurry m) (f ×ˢ g)
⊢ map (fun (p : α × β) ↦ m p.1 p.2) (f ×ˢ g) = map₂ m f g
have rw₂ : Eq.{u_5 + 1} (α := Filter γ) (map (fun (p : α × β) ↦ m p.1 p.2) (f ×ˢ g)) (map (fun (p : α × β) ↦ m p.1 p.2) (f ×ˢ g))
Tactic: rw [map₂, copy_eq, uncurry_def]
-- Lean 4 proof step from Mathlib.Order.Filter.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
m : α → β → γ
f₁ f₂ : Filter α
g : Filter β
⊢ map₂ m (f₁ ⊔ f₂) g = map₂ m f₁ g ⊔ map₂ m f₂ g
have simp_rw : Eq.{u_5 + 1} (α := Filter γ) (map (fun (p : α × β) ↦ m p.1 p.2) ((f₁ ⊔ f₂) ×ˢ g))
  (map (fun (p : α × β) ↦ m p.1 p.2) (f₁ ×ˢ g) ⊔ map (fun (p : α × β) ↦ m p.1 p.2) (f₂ ×ˢ g))
Tactic: simp_rw [← map_prod_eq_map₂, sup_prod, map_sup]
-- Lean 4 proof step from Mathlib.Order.Filter.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
m : α → β → γ
f₁ f₂ : Filter α
g : Filter β
simp_rw :
  Eq.{u_5 + 1} (α := Filter γ) (map (fun (p : α × β) ↦ m p.1 p.2) ((f₁ ⊔ f₂) ×ˢ g))
    (map (fun (p : α × β) ↦ m p.1 p.2) (f₁ ×ˢ g) ⊔ map (fun (p : α × β) ↦ m p.1 p.2) (f₂ ×ˢ g))
⊢ map₂ m (f₁ ⊔ f₂) g = map₂ m f₁ g ⊔ map₂ m f₂ g
have simp_rw₁ : Eq.{u_5 + 1} (α := Filter γ) (map (fun (p : α × β) ↦ m p.1 p.2) (f₁ ×ˢ g ⊔ f₂ ×ˢ g))
  (map (fun (p : α × β) ↦ m p.1 p.2) (f₁ ×ˢ g) ⊔ map (fun (p : α × β) ↦ m p.1 p.2) (f₂ ×ˢ g))
Tactic: simp_rw [← map_prod_eq_map₂, sup_prod, map_sup]
-- Lean 4 proof step from Mathlib.Order.Filter.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
m : α → β → γ
f : Filter α
g₁ g₂ : Filter β
⊢ map₂ m f (g₁ ⊔ g₂) = map₂ m f g₁ ⊔ map₂ m f g₂
have simp_rw : Eq.{u_5 + 1} (α := Filter γ) (map (fun (p : α × β) ↦ m p.1 p.2) (f ×ˢ (g₁ ⊔ g₂)))
  (map (fun (p : α × β) ↦ m p.1 p.2) (f ×ˢ g₁) ⊔ map (fun (p : α × β) ↦ m p.1 p.2) (f ×ˢ g₂))
Tactic: simp_rw [← map_prod_eq_map₂, prod_sup, map_sup]
-- Lean 4 proof step from Mathlib.Order.Filter.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
m : α → β → γ
f : Filter α
g₁ g₂ : Filter β
simp_rw :
  Eq.{u_5 + 1} (α := Filter γ) (map (fun (p : α × β) ↦ m p.1 p.2) (f ×ˢ (g₁ ⊔ g₂)))
    (map (fun (p : α × β) ↦ m p.1 p.2) (f ×ˢ g₁) ⊔ map (fun (p : α × β) ↦ m p.1 p.2) (f ×ˢ g₂))
⊢ map₂ m f (g₁ ⊔ g₂) = map₂ m f g₁ ⊔ map₂ m f g₂
have simp_rw₁ : Eq.{u_5 + 1} (α := Filter γ) (map (fun (p : α × β) ↦ m p.1 p.2) (f ×ˢ g₁ ⊔ f ×ˢ g₂))
  (map (fun (p : α × β) ↦ m p.1 p.2) (f ×ˢ g₁) ⊔ map (fun (p : α × β) ↦ m p.1 p.2) (f ×ˢ g₂))
Tactic: simp_rw [← map_prod_eq_map₂, prod_sup, map_sup]
-- Lean 4 proof step from Mathlib.Order.Filter.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
m : α → β → γ
g : Filter β
a : α
⊢ map₂ m (pure a) g = map (m a) g
have rw : map ((fun (p : α × β) ↦ m p.1 p.2) ∘ Prod.mk a) g = map (m a) g
Tactic: rw [← map_prod_eq_map₂, pure_prod, map_map]
-- Lean 4 proof step from Mathlib.Order.Filter.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
m : α → β → γ
f : Filter α
b : β
⊢ map₂ m f (pure b) = map (fun (x : α) ↦ m x b) f
have rw : Eq.{u_5 + 1} (α := Filter γ) (map ((fun (p : α × β) ↦ m p.1 p.2) ∘ fun (a : α) ↦ (a, b)) f)
  (map (fun (x : α) ↦ m x b) f)
Tactic: rw [← map_prod_eq_map₂, prod_pure, map_map]
-- Lean 4 proof step from Mathlib.Order.Filter.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
m : α → β → γ
a : α
b : β
⊢ map₂ m (pure a) (pure b) = pure (m a b)
have rw : map (fun (x : α) ↦ m x b) (pure a) = pure (m a b)
Tactic: rw [map₂_pure_right, map_pure]
-- Lean 4 proof step from Mathlib.Order.Filter.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
m : α → β → γ
a : α
b : β
rw : map (fun (x : α) ↦ m x b) (pure a) = pure (m a b)
⊢ map₂ m (pure a) (pure b) = pure (m a b)
have rw₁ : Eq (α := Filter γ) (pure (m a b)) (pure (m a b))
Tactic: rw [map₂_pure_right, map_pure]
-- Lean 4 proof step from Mathlib.Order.Filter.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
m : α → β → γ
f : Filter α
g : Filter β
⊢ map₂ m f g = map₂ (fun (a : β) (b : α) ↦ m b a) g f
have rw : Eq.{u_5 + 1} (α := Filter γ) (map (fun (x : β × α) ↦ m x.swap.1 x.swap.2) (g ×ˢ f))
  (map (fun (p : β × α) ↦ m p.2 p.1) (g ×ˢ f))
Tactic: rw [← map_prod_eq_map₂, prod_comm, map_map, ← map_prod_eq_map₂, Function.comp_def]