awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Filter.Lift (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
inst : Nonempty ι
f : ι → Filter α
g : Set α → Filter β
hg : ∀ (s t : Set α), g (s ∩ t) = g s ⊓ g t
s : Set β
t : Set α
ht : t ∈ iInf f
⊢ ⨅ (i : ι), (f i).lift g ≤ g univ
have refine_1 : ∀ (inhabited_h : Inhabited ι), ⨅ (i : ι), (f i).lift g ≤ g univ
Tactic: inhabit ι
-- Lean 4 proof step from Mathlib.Order.Filter.Lift (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
inst : Nonempty ι
f : ι → Filter α
g : Set α → Filter β
hg : ∀ (s t : Set α), g (s ∩ t) = g s ⊓ g t
s : Set β
t : Set α
ht_1 : t ∈ iInf f
i : ι
s₁ s₂ : Set α
hs : s₁ ∈ f i
ht : ⨅ (i : ι), (f i).lift g ≤ g s₂
⊢ ⨅ (i : ι), (f i).lift g ≤ g (s₁ ∩ s₂)
have refine_2 : ⨅ (i : ι), (f i).lift g ≤ g s₁ ⊓ g s₂
Tactic: rw [hg]
-- Lean 4 proof step from Mathlib.Order.Filter.Lift (hypothesis)
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
inst : Nonempty ι
f : ι → Filter α
g : Set α → Filter β
hg : ∀ (s t : Set α), g (s ∩ t) = g s ⊓ g t
s : Set β
⊢ s ∈ (iInf f).lift g → Membership.mem (γ := Filter β) (⨅ (i : ι), (f i).lift g) s
have H : ∀ t ∈ iInf f, ⨅ (i : ι), (f i).lift g ≤ g t
Tactic: have H : ∀ t ∈ iInf f, ⨅ i, (f i).lift g ≤ g t := by
    intro t ht
    refine iInf_sets_induct ht ?_ fun hs ht => ?_
    · inhabit ι
      exact iInf₂_le_of_le default univ (iInf_le _ univ_mem)
    · rw [hg]
      exact le_inf (iInf₂_le_of_le _ _ <| iInf_le _ hs) ht
-- Lean 4 proof step from Mathlib.Order.Filter.Lift (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
inst : Nonempty ι
f : ι → Filter α
g : Set α → Filter β
hg : ∀ (s t : Set α), g (s ∩ t) = g s ⊓ g t
s : Set β
H : ∀ t ∈ iInf f, ⨅ (i : ι), (f i).lift g ≤ g t
⊢ s ∈ (iInf f).lift g → Membership.mem (γ := Filter β) (⨅ (i : ι), (f i).lift g) s
have simp : ∀ x ∈ iInf f, s ∈ g x → Membership.mem (γ := Filter β) (⨅ (i : ι), (f i).lift g) s
Tactic: simp only [mem_lift_sets (Monotone.of_map_inf hg), exists_imp, and_imp]
-- Lean 4 proof step from Mathlib.Order.Filter.Lift (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
inst : Nonempty ι
f : ι → Filter α
g : Set α → Filter β
hf : Directed (fun (x1 x2 : Filter α) ↦ x1 ≥ x2) f
hg : Monotone g
s : Set β
⊢ s ∈ (iInf f).lift g → Membership.mem (γ := Filter β) (⨅ (i : ι), (f i).lift g) s
have simp : ∀ (x : Set α) (x_1 : ι), x ∈ f x_1 → s ∈ g x → Membership.mem (γ := Filter β) (⨅ (i : ι), (f i).lift g) s
Tactic: simp only [mem_lift_sets hg, exists_imp, and_imp, mem_iInf_of_directed hf]
-- Lean 4 proof step from Mathlib.Order.Filter.Lift (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
f : ι → Filter α
g : Set α → Filter β
hg : ∀ (s t : Set α), g (s ∩ t) = g s ⊓ g t
hg' : g univ = ⊤
⊢ (iInf f).lift g = ⨅ (i : ι), (f i).lift g
have inl : IsEmpty ι → (iInf f).lift g = ⨅ (i : ι), (f i).lift g
Tactic: cases isEmpty_or_nonempty ι
-- Lean 4 proof step from Mathlib.Order.Filter.Lift (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
f : ι → Filter α
g : Set α → Filter β
hg : ∀ (s t : Set α), g (s ∩ t) = g s ⊓ g t
hg' : g univ = ⊤
inl : IsEmpty ι → (iInf f).lift g = ⨅ (i : ι), (f i).lift g
⊢ (iInf f).lift g = ⨅ (i : ι), (f i).lift g
have inr : Nonempty ι → (iInf f).lift g = ⨅ (i : ι), (f i).lift g
Tactic: cases isEmpty_or_nonempty ι
-- Lean 4 proof step from Mathlib.Order.Filter.Lift (goal)
Goal:
α : Type u_1
β : Type u_2
h : Set α → Set β
a : α
hh : Monotone h
⊢ Filter.lift' (pure a) h = 𝓟 (h {a})
have rw : Filter.lift' (𝓟 {a}) h = 𝓟 (h {a})
Tactic: rw [← principal_singleton, lift'_principal hh]
-- Lean 4 proof step from Mathlib.Order.Filter.Lift (goal)
Goal:
α : Type u_1
β : Type u_2
h : Set α → Set β
a : α
hh : Monotone h
rw : Filter.lift' (𝓟 {a}) h = 𝓟 (h {a})
⊢ Filter.lift' (pure a) h = 𝓟 (h {a})
have rw₁ : 𝓟 (h {a}) = 𝓟 (h {a})
Tactic: rw [← principal_singleton, lift'_principal hh]
-- Lean 4 proof step from Mathlib.Order.Filter.Lift (goal)
Goal:
α : Type u_1
β : Type u_2
h : Set α → Set β
hh : Monotone h
⊢ Filter.lift' ⊥ h = 𝓟 (h ∅)
have rw : Filter.lift' (𝓟 ∅) h = 𝓟 (h ∅)
Tactic: rw [← principal_empty, lift'_principal hh]
-- Lean 4 proof step from Mathlib.Order.Filter.Lift (goal)
Goal:
α : Type u_1
β : Type u_2
h : Set α → Set β
hh : Monotone h
rw : Filter.lift' (𝓟 ∅) h = 𝓟 (h ∅)
⊢ Filter.lift' ⊥ h = 𝓟 (h ∅)
have rw₁ : 𝓟 (h ∅) = 𝓟 (h ∅)
Tactic: rw [← principal_empty, lift'_principal hh]
-- Lean 4 proof step from Mathlib.Order.Filter.Lift (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
f : ι → Filter α
g : Set α → Set β
hg : ∀ {s t : Set α}, g (s ∩ t) = g s ∩ g t
hg' : g univ = univ
⊢ (𝓟 ∘ g) univ = ⊤
have rw : 𝓟 (g univ) = ⊤
Tactic: rw [Function.comp_apply, hg', principal_univ]
-- Lean 4 proof step from Mathlib.Order.Filter.Lift (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
f : ι → Filter α
g : Set α → Set β
hg : ∀ {s t : Set α}, g (s ∩ t) = g s ∩ g t
hg' : g univ = univ
rw : 𝓟 (g univ) = ⊤
⊢ (𝓟 ∘ g) univ = ⊤
have rw₁ : Eq.{u_2 + 1} (α := Filter β) (𝓟 univ) ⊤
Tactic: rw [Function.comp_apply, hg', principal_univ]
-- Lean 4 proof step from Mathlib.Order.Filter.Lift (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
f : ι → Filter α
g : Set α → Set β
hg : ∀ {s t : Set α}, g (s ∩ t) = g s ∩ g t
hg' : g univ = univ
rw : 𝓟 (g univ) = ⊤
rw₁ : Eq.{u_2 + 1} (α := Filter β) (𝓟 univ) ⊤
⊢ (𝓟 ∘ g) univ = ⊤
have rw₂ : Eq.{u_2 + 1} (α := Filter β) ⊤ ⊤
Tactic: rw [Function.comp_apply, hg', principal_univ]
-- Lean 4 proof step from Mathlib.Order.Filter.Lift (goal)
Goal:
α : Type u_1
β : Type u_2
f g : Filter α
s : Set α → Set β
hs : ∀ (t₁ t₂ : Set α), s (t₁ ∩ t₂) = s t₁ ∩ s t₂
⊢ (f ⊓ g).lift' s = f.lift' s ⊓ g.lift' s
have rw : Eq.{u_2 + 1} (α := Filter β) (⨅ (i : Bool), (bif i then f else g).lift' s)
  (⨅ (b : Bool), bif b then f.lift' s else g.lift' s)
Tactic: rw [inf_eq_iInf, inf_eq_iInf, lift'_iInf hs]
-- Lean 4 proof step from Mathlib.Order.Filter.Lift (goal)
Goal:
α : Type u_1
β : Type u_2
f g : Filter α
s : Set α → Set β
hs : ∀ (t₁ t₂ : Set α), s (t₁ ∩ t₂) = s t₁ ∩ s t₂
⊢ Eq.{u_2 + 1} (α := Filter β) (⨅ (i : Bool), (bif i then f else g).lift' s)
    (⨅ (b : Bool), bif b then f.lift' s else g.lift' s)
have refine : ∀ (i : Bool), (bif i then f else g).lift' s = bif i then f.lift' s else g.lift' s
Tactic: refine iInf_congr ?_
-- Lean 4 proof step from Mathlib.Order.Filter.Lift (goal)
Goal:
α₁ : Type u_5
α₂ : Type u_6
β₁ : Type u_7
β₂ : Type u_8
f₁ : Filter α₁
f₂ : Filter α₂
g₁ : Set α₁ → Filter β₁
g₂ : Set α₂ → Filter β₂
hg₁ : Monotone g₁
hg₂ : Monotone g₂
⊢ f₁.lift g₁ ×ˢ f₂.lift g₂ = f₁.lift fun (s : Set α₁) ↦ f₂.lift fun (t : Set α₂) ↦ g₁ s ×ˢ g₂ t
have simp : Eq (α := Filter (β₁ × β₂))
  (f₁.lift fun (s : Set α₁) ↦ (g₁ s).lift fun (s : Set β₁) ↦ (f₂.lift g₂).lift' fun (t : Set β₂) ↦ s ×ˢ t)
  (f₁.lift fun (s : Set α₁) ↦
    f₂.lift fun (t : Set α₂) ↦ (g₁ s).lift fun (s : Set β₁) ↦ (g₂ t).lift' fun (t : Set β₂) ↦ s ×ˢ t)
Tactic: simp only [prod_def, lift_assoc hg₁]
-- Lean 4 proof step from Mathlib.Order.Filter.Lift (goal)
Goal:
α₁ : Type u_5
α₂ : Type u_6
β₁ : Type u_7
β₂ : Type u_8
f₁ : Filter α₁
f₂ : Filter α₂
g₁ : Set α₁ → Filter β₁
g₂ : Set α₂ → Filter β₂
hg₁ : Monotone g₁
hg₂ : Monotone g₂
⊢ Eq (α := Filter (β₁ × β₂))
    (f₁.lift fun (s : Set α₁) ↦ (g₁ s).lift fun (s : Set β₁) ↦ (f₂.lift g₂).lift' fun (t : Set β₂) ↦ s ×ˢ t)
    (f₁.lift fun (s : Set α₁) ↦
      f₂.lift fun (t : Set α₂) ↦ (g₁ s).lift fun (s : Set β₁) ↦ (g₂ t).lift' fun (t : Set β₂) ↦ s ×ˢ t)
have h : Eq (α := (s : Set α₁) → Filter (β₁ × β₂))
  (fun (s : Set α₁) ↦ (g₁ s).lift fun (s : Set β₁) ↦ (f₂.lift g₂).lift' fun (t : Set β₂) ↦ s ×ˢ t) fun (s : Set α₁) ↦
  f₂.lift fun (t : Set α₂) ↦ (g₁ s).lift fun (s : Set β₁) ↦ (g₂ t).lift' fun (t : Set β₂) ↦ s ×ˢ t
Tactic: apply congr_arg
-- Lean 4 proof step from Mathlib.Order.Filter.Lift (goal)
Goal:
α₁ : Type u_5
α₂ : Type u_6
β₁ : Type u_7
β₂ : Type u_8
f₁ : Filter α₁
f₂ : Filter α₂
g₁ : Set α₁ → Filter β₁
g₂ : Set α₂ → Filter β₂
hg₁ : Monotone g₁
hg₂ : Monotone g₂
⊢ Eq (α := (s : Set α₁) → Filter (β₁ × β₂))
    (fun (s : Set α₁) ↦ (g₁ s).lift fun (s : Set β₁) ↦ (f₂.lift g₂).lift' fun (t : Set β₂) ↦ s ×ˢ t) fun (s : Set α₁) ↦
    f₂.lift fun (t : Set α₂) ↦ (g₁ s).lift fun (s : Set β₁) ↦ (g₂ t).lift' fun (t : Set β₂) ↦ s ×ˢ t
have h : ∀ (x : Set α₁),
  Eq (α := Filter (β₁ × β₂)) ((g₁ x).lift fun (s : Set β₁) ↦ (f₂.lift g₂).lift' fun (t : Set β₂) ↦ s ×ˢ t)
    (f₂.lift fun (t : Set α₂) ↦ (g₁ x).lift fun (s : Set β₁) ↦ (g₂ t).lift' fun (t : Set β₂) ↦ s ×ˢ t)
Tactic: funext x
-- Lean 4 proof step from Mathlib.Order.Filter.Lift (goal)
Goal:
α₁ : Type u_5
α₂ : Type u_6
β₁ : Type u_7
β₂ : Type u_8
f₁ : Filter α₁
f₂ : Filter α₂
g₁ : Set α₁ → Filter β₁
g₂ : Set α₂ → Filter β₂
hg₁ : Monotone g₁
hg₂ : Monotone g₂
x : Set α₁
⊢ Eq (α := Filter (β₁ × β₂)) ((g₁ x).lift fun (s : Set β₁) ↦ (f₂.lift g₂).lift' fun (t : Set β₂) ↦ s ×ˢ t)
    (f₂.lift fun (t : Set α₂) ↦ (g₁ x).lift fun (s : Set β₁) ↦ (g₂ t).lift' fun (t : Set β₂) ↦ s ×ˢ t)
have h : Eq (α := Filter (β₁ × β₂)) ((g₁ x).lift fun (s : Set β₁) ↦ (f₂.lift g₂).lift' fun (t : Set β₂) ↦ s ×ˢ t)
  ((g₁ x).lift fun (t : Set β₁) ↦ f₂.lift fun (s : Set α₂) ↦ (g₂ s).lift' fun (t_1 : Set β₂) ↦ t ×ˢ t_1)
Tactic: rw [lift_comm]
-- Lean 4 proof step from Mathlib.Order.Filter.Lift (goal)
Goal:
α₁ : Type u_5
α₂ : Type u_6
β₁ : Type u_7
β₂ : Type u_8
f₁ : Filter α₁
f₂ : Filter α₂
g₁ : Set α₁ → Filter β₁
g₂ : Set α₂ → Filter β₂
hg₁ : Monotone g₁
hg₂ : Monotone g₂
x : Set α₁
⊢ Eq (α := Filter (β₁ × β₂)) ((g₁ x).lift fun (s : Set β₁) ↦ (f₂.lift g₂).lift' fun (t : Set β₂) ↦ s ×ˢ t)
    ((g₁ x).lift fun (t : Set β₁) ↦ f₂.lift fun (s : Set α₂) ↦ (g₂ s).lift' fun (t_1 : Set β₂) ↦ t ×ˢ t_1)
have h : Eq (α := (s : Set β₁) → Filter (β₁ × β₂)) (fun (s : Set β₁) ↦ (f₂.lift g₂).lift' fun (t : Set β₂) ↦ s ×ˢ t)
  fun (t : Set β₁) ↦ f₂.lift fun (s : Set α₂) ↦ (g₂ s).lift' fun (t_1 : Set β₂) ↦ t ×ˢ t_1
Tactic: apply congr_arg
-- Lean 4 proof step from Mathlib.Order.Filter.Lift (goal)
Goal:
α₁ : Type u_5
α₂ : Type u_6
β₁ : Type u_7
β₂ : Type u_8
f₁ : Filter α₁
f₂ : Filter α₂
g₁ : Set α₁ → Filter β₁
g₂ : Set α₂ → Filter β₂
hg₁ : Monotone g₁
hg₂ : Monotone g₂
x : Set α₁
⊢ Eq (α := (s : Set β₁) → Filter (β₁ × β₂)) (fun (s : Set β₁) ↦ (f₂.lift g₂).lift' fun (t : Set β₂) ↦ s ×ˢ t)
    fun (t : Set β₁) ↦ f₂.lift fun (s : Set α₂) ↦ (g₂ s).lift' fun (t_1 : Set β₂) ↦ t ×ˢ t_1
have h : ∀ (y : Set β₁),
  Eq (α := Filter (β₁ × β₂)) ((f₂.lift g₂).lift' fun (t : Set β₂) ↦ y ×ˢ t)
    (f₂.lift fun (s : Set α₂) ↦ (g₂ s).lift' fun (t : Set β₂) ↦ y ×ˢ t)
Tactic: funext y
-- Lean 4 proof step from Mathlib.Order.Filter.ListTraverse (goal)
Goal:
α β : Type u
f : β → Filter α
fs : List β
t : Set (List α)
⊢ t ∈ traverse f fs ↔ ∃ (us : List (Set α)), Forall₂ (fun (b : β) (s : Set α) ↦ s ∈ f b) fs us ∧ sequence us ⊆ t
have mp : t ∈ traverse f fs → ∃ (us : List (Set α)), Forall₂ (fun (b : β) (s : Set α) ↦ s ∈ f b) fs us ∧ sequence us ⊆ t
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Filter.ListTraverse (goal)
Goal:
α β : Type u
f : β → Filter α
fs : List β
t : Set (List α)
mp : t ∈ traverse f fs → ∃ (us : List (Set α)), Forall₂ (fun (b : β) (s : Set α) ↦ s ∈ f b) fs us ∧ sequence us ⊆ t
⊢ t ∈ traverse f fs ↔ ∃ (us : List (Set α)), Forall₂ (fun (b : β) (s : Set α) ↦ s ∈ f b) fs us ∧ sequence us ⊆ t
have mpr : (∃ (us : List (Set α)), Forall₂ (fun (b : β) (s : Set α) ↦ s ∈ f b) fs us ∧ sequence us ⊆ t) → t ∈ traverse f fs
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Filter.ListTraverse (goal)
Goal:
α β : Type u
f : β → Filter α
b : β
fs : List β
ih : ∀ t ∈ traverse f fs, ∃ (us : List (Set α)), Forall₂ (fun (b : β) (s : Set α) ↦ s ∈ f b) fs us ∧ sequence us ⊆ t
t : Set (List α)
ht : t ∈ traverse f (b :: fs)
⊢ ∃ (us : List (Set α)), Forall₂ (fun (b : β) (s : Set α) ↦ s ∈ f b) (b :: fs) us ∧ sequence us ⊆ t
have mp : ∀ (u : Set (List α → List α)) (hu : u ∈ cons <$> f b) (v : Set (List α))
  (hv : Membership.mem (γ := Filter (List α)) ((fun (x : Unit) ↦ List.traverse f fs) ()) v) (ht : u.seq v ⊆ t),
  ∃ (us : List (Set α)), Forall₂ (fun (b : β) (s : Set α) ↦ s ∈ f b) (b :: fs) us ∧ sequence us ⊆ t
Tactic: rcases mem_seq_iff.1 ht with ⟨u, hu, v, hv, ht⟩
-- Lean 4 proof step from Mathlib.Order.Filter.ListTraverse (goal)
Goal:
α β : Type u
f : β → Filter α
b : β
fs : List β
ih : ∀ t ∈ traverse f fs, ∃ (us : List (Set α)), Forall₂ (fun (b : β) (s : Set α) ↦ s ∈ f b) fs us ∧ sequence us ⊆ t
t : Set (List α)
ht_1 : t ∈ traverse f (b :: fs)
u : Set (List α → List α)
hu : u ∈ cons <$> f b
v : Set (List α)
hv : Membership.mem (γ := Filter (List α)) ((fun (x : Unit) ↦ List.traverse f fs) ()) v
ht : u.seq v ⊆ t
⊢ ∃ (us : List (Set α)), Forall₂ (fun (b : β) (s : Set α) ↦ s ∈ f b) (b :: fs) us ∧ sequence us ⊆ t
have mp : ∀ (w : Set α) (hw : w ∈ f b) (hwu : cons '' w ⊆ u),
  ∃ (us : List (Set α)), Forall₂ (fun (b : β) (s : Set α) ↦ s ∈ f b) (b :: fs) us ∧ sequence us ⊆ t
Tactic: rcases mem_map_iff_exists_image.1 hu with ⟨w, hw, hwu⟩
-- Lean 4 proof step from Mathlib.Order.Filter.ListTraverse (goal)
Goal:
α β : Type u
f : β → Filter α
b : β
fs : List β
ih : ∀ t ∈ traverse f fs, ∃ (us : List (Set α)), Forall₂ (fun (b : β) (s : Set α) ↦ s ∈ f b) fs us ∧ sequence us ⊆ t
t : Set (List α)
ht_1 : t ∈ traverse f (b :: fs)
u : Set (List α → List α)
hu : u ∈ cons <$> f b
v : Set (List α)
hv : Membership.mem (γ := Filter (List α)) ((fun (x : Unit) ↦ List.traverse f fs) ()) v
ht : u.seq v ⊆ t
w : Set α
hw : w ∈ f b
hwu : cons '' w ⊆ u
⊢ ∃ (us : List (Set α)), Forall₂ (fun (b : β) (s : Set α) ↦ s ∈ f b) (b :: fs) us ∧ sequence us ⊆ t
have mp : ∀ (us : List (Set α)) (hus : Forall₂ (fun (b : β) (s : Set α) ↦ s ∈ f b) fs us) (hu : sequence us ⊆ v),
  ∃ (us : List (Set α)), Forall₂ (fun (b : β) (s : Set α) ↦ s ∈ f b) (b :: fs) us ∧ sequence us ⊆ t
Tactic: rcases ih v hv with ⟨us, hus, hu⟩
-- Lean 4 proof step from Mathlib.Order.Filter.ListTraverse (goal)
Goal:
α β : Type u
f : β → Filter α
fs : List β
t : Set (List α)
⊢ t ∈ traverse f fs → ∃ (us : List (Set α)), Forall₂ (fun (b : β) (s : Set α) ↦ s ∈ f b) fs us ∧ sequence us ⊆ t
have mp : ∀ t ∈ traverse f [], ∃ (us : List (Set α)), Forall₂ (fun (b : β) (s : Set α) ↦ s ∈ f b) [] us ∧ sequence us ⊆ t
Tactic: induction fs generalizing t with
    | nil =>
      simp only [sequence, mem_pure, imp_self, forall₂_nil_left_iff, exists_eq_left, Set.pure_def,
        singleton_subset_iff, traverse_nil]
    | cons b fs ih =>
      intro ht
      rcases mem_seq_iff.1 ht with ⟨u, hu, v, hv, ht⟩
      rcases mem_map_iff_exists_image.1 hu with ⟨w, hw, hwu⟩
      rcases ih v hv with ⟨us, hus, hu⟩
      exact ⟨w::us, Forall₂.cons hw hus, (Set.seq_mono hwu hu).trans ht⟩
Cleared hypotheses: fs, t
-- Lean 4 proof step from Mathlib.Order.Filter.ListTraverse (goal)
Goal:
α β : Type u
f : β → Filter α
fs : List β
t : Set (List α)
mp : ∀ t ∈ traverse f [], ∃ (us : List (Set α)), Forall₂ (fun (b : β) (s : Set α) ↦ s ∈ f b) [] us ∧ sequence us ⊆ t
⊢ t ∈ traverse f fs → ∃ (us : List (Set α)), Forall₂ (fun (b : β) (s : Set α) ↦ s ∈ f b) fs us ∧ sequence us ⊆ t
have mp₁ : ∀ (b : β) (fs : List β)
  (ih :
    ∀ t ∈ traverse f fs, ∃ (us : List (Set α)), Forall₂ (fun (b : β) (s : Set α) ↦ s ∈ f b) fs us ∧ sequence us ⊆ t),
  ∀ t ∈ traverse f (b :: fs),
    ∃ (us : List (Set α)), Forall₂ (fun (b : β) (s : Set α) ↦ s ∈ f b) (b :: fs) us ∧ sequence us ⊆ t
Tactic: induction fs generalizing t with
    | nil =>
      simp only [sequence, mem_pure, imp_self, forall₂_nil_left_iff, exists_eq_left, Set.pure_def,
        singleton_subset_iff, traverse_nil]
    | cons b fs ih =>
      intro ht
      rcases mem_seq_iff.1 ht with ⟨u, hu, v, hv, ht⟩
      rcases mem_map_iff_exists_image.1 hu with ⟨w, hw, hwu⟩
      rcases ih v hv with ⟨us, hus, hu⟩
      exact ⟨w::us, Forall₂.cons hw hus, (Set.seq_mono hwu hu).trans ht⟩
Cleared hypotheses: fs, t
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
f : Filter α
m : α → β
s : Set α
hf : Injective m
h : m '' s ∈ map m f
⊢ s ∈ f
have rwa : m ⁻¹' m '' s ∈ f
Tactic: rwa [← preimage_image_eq s hf]
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
f : Filter α
m : α → β
⊢ range m ∈ map m f
have rw : m '' univ ∈ map m f
Tactic: rw [← image_univ]
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
x : α
s : Set β
F : Filter (α × β)
⊢ s ∈ comap (Prod.mk x) F ↔ {p : α × β | p.1 = x → p.2 ∈ s} ∈ F
have simp_rw : {y : α × β | ∀ ⦃x_1 : β⦄, (x, x_1) = y → x_1 ∈ s} ∈ F ↔ {p : α × β | p.1 = x → p.2 ∈ s} ∈ F
Tactic: simp_rw [mem_comap', Prod.ext_iff, and_imp, @forall_comm β (_ = _), forall_eq, eq_comm]
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
x : α
s : Set β
F : Filter (α × β)
simp_rw : {y : α × β | ∀ ⦃x_1 : β⦄, (x, x_1) = y → x_1 ∈ s} ∈ F ↔ {p : α × β | p.1 = x → p.2 ∈ s} ∈ F
⊢ s ∈ comap (Prod.mk x) F ↔ {p : α × β | p.1 = x → p.2 ∈ s} ∈ F
have simp_rw₁ : {y : α × β | ∀ ⦃x_1 : β⦄, x = y.1 ∧ x_1 = y.2 → x_1 ∈ s} ∈ F ↔ {p : α × β | p.1 = x → p.2 ∈ s} ∈ F
Tactic: simp_rw [mem_comap', Prod.ext_iff, and_imp, @forall_comm β (_ = _), forall_eq, eq_comm]
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
x : α
s : Set β
F : Filter (α × β)
simp_rw : {y : α × β | ∀ ⦃x_1 : β⦄, (x, x_1) = y → x_1 ∈ s} ∈ F ↔ {p : α × β | p.1 = x → p.2 ∈ s} ∈ F
simp_rw₁ : {y : α × β | ∀ ⦃x_1 : β⦄, x = y.1 ∧ x_1 = y.2 → x_1 ∈ s} ∈ F ↔ {p : α × β | p.1 = x → p.2 ∈ s} ∈ F
⊢ s ∈ comap (Prod.mk x) F ↔ {p : α × β | p.1 = x → p.2 ∈ s} ∈ F
have simp_rw₂ : {y : α × β | ∀ ⦃x_1 : β⦄, x = y.1 → x_1 = y.2 → x_1 ∈ s} ∈ F ↔ {p : α × β | p.1 = x → p.2 ∈ s} ∈ F
Tactic: simp_rw [mem_comap', Prod.ext_iff, and_imp, @forall_comm β (_ = _), forall_eq, eq_comm]
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
x : α
s : Set β
F : Filter (α × β)
simp_rw : {y : α × β | ∀ ⦃x_1 : β⦄, (x, x_1) = y → x_1 ∈ s} ∈ F ↔ {p : α × β | p.1 = x → p.2 ∈ s} ∈ F
simp_rw₁ : {y : α × β | ∀ ⦃x_1 : β⦄, x = y.1 ∧ x_1 = y.2 → x_1 ∈ s} ∈ F ↔ {p : α × β | p.1 = x → p.2 ∈ s} ∈ F
simp_rw₂ : {y : α × β | ∀ ⦃x_1 : β⦄, x = y.1 → x_1 = y.2 → x_1 ∈ s} ∈ F ↔ {p : α × β | p.1 = x → p.2 ∈ s} ∈ F
⊢ s ∈ comap (Prod.mk x) F ↔ {p : α × β | p.1 = x → p.2 ∈ s} ∈ F
have simp_rw₃ : {y : α × β | ∀ (b : x = y.1) (a : β), a = y.2 → a ∈ s} ∈ F ↔ {p : α × β | p.1 = x → p.2 ∈ s} ∈ F
Tactic: simp_rw [mem_comap', Prod.ext_iff, and_imp, @forall_comm β (_ = _), forall_eq, eq_comm]
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
x : α
s : Set β
F : Filter (α × β)
simp_rw : {y : α × β | ∀ ⦃x_1 : β⦄, (x, x_1) = y → x_1 ∈ s} ∈ F ↔ {p : α × β | p.1 = x → p.2 ∈ s} ∈ F
simp_rw₁ : {y : α × β | ∀ ⦃x_1 : β⦄, x = y.1 ∧ x_1 = y.2 → x_1 ∈ s} ∈ F ↔ {p : α × β | p.1 = x → p.2 ∈ s} ∈ F
simp_rw₂ : {y : α × β | ∀ ⦃x_1 : β⦄, x = y.1 → x_1 = y.2 → x_1 ∈ s} ∈ F ↔ {p : α × β | p.1 = x → p.2 ∈ s} ∈ F
simp_rw₃ : {y : α × β | ∀ (b : x = y.1) (a : β), a = y.2 → a ∈ s} ∈ F ↔ {p : α × β | p.1 = x → p.2 ∈ s} ∈ F
⊢ s ∈ comap (Prod.mk x) F ↔ {p : α × β | p.1 = x → p.2 ∈ s} ∈ F
have simp_rw₄ : {y : α × β | ∀ (b : x = y.1), y.2 ∈ s} ∈ F ↔ {p : α × β | p.1 = x → p.2 ∈ s} ∈ F
Tactic: simp_rw [mem_comap', Prod.ext_iff, and_imp, @forall_comm β (_ = _), forall_eq, eq_comm]
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
l : Filter β
s : Set α
⊢ sᶜ ∈ comap f l ↔ (f '' s)ᶜ ∈ l
have rw : (f '' sᶜᶜ)ᶜ ∈ l ↔ (f '' s)ᶜ ∈ l
Tactic: rw [mem_comap_iff_compl, compl_compl]
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
l : Filter β
s : Set α
rw : (f '' sᶜᶜ)ᶜ ∈ l ↔ (f '' s)ᶜ ∈ l
⊢ sᶜ ∈ comap f l ↔ (f '' s)ᶜ ∈ l
have rw₁ : (f '' s)ᶜ ∈ l ↔ (f '' s)ᶜ ∈ l
Tactic: rw [mem_comap_iff_compl, compl_compl]
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := Filter α) (⨆ (a : α), pure a) ⊤
have rw : Eq.{u_1 + 1} (α := Filter α) (⨆ (a : α), pure a) (𝓟 univ)
Tactic: rw [← principal_univ, ← biSup_pure_eq_principal, iSup_univ]
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
rw : Eq.{u_1 + 1} (α := Filter α) (⨆ (a : α), pure a) (𝓟 univ)
⊢ Eq.{u_1 + 1} (α := Filter α) (⨆ (a : α), pure a) ⊤
have rw₁ : Eq.{u_1 + 1} (α := Filter α) (⨆ (a : α), pure a) (⨆ (a : α), ⨆ (_ : Membership.mem (γ := Set α) univ a), pure a)
Tactic: rw [← principal_univ, ← biSup_pure_eq_principal, iSup_univ]
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
rw : Eq.{u_1 + 1} (α := Filter α) (⨆ (a : α), pure a) (𝓟 univ)
rw₁ : Eq.{u_1 + 1} (α := Filter α) (⨆ (a : α), pure a) (⨆ (a : α), ⨆ (_ : Membership.mem (γ := Set α) univ a), pure a)
⊢ Eq.{u_1 + 1} (α := Filter α) (⨆ (a : α), pure a) ⊤
have rw₂ : Eq.{u_1 + 1} (α := Filter α) (⨆ (a : α), pure a) (⨆ (x : α), pure x)
Tactic: rw [← principal_univ, ← biSup_pure_eq_principal, iSup_univ]
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
f : Filter α
inst : f.NeBot
c : β
⊢ map (fun (x : α) ↦ c) f = pure c
have h : ∀ (s : Set β), Membership.mem (γ := Filter β) (map (fun (x : α) ↦ c) f) s ↔ Membership.mem (γ := Filter β) (pure c) s
Tactic: ext s
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
f : Filter α
inst : f.NeBot
c : β
s : Set β
⊢ Membership.mem (γ := Filter β) (map (fun (x : α) ↦ c) f) s ↔ Membership.mem (γ := Filter β) (pure c) s
have pos : ∀ (h : c ∈ s), Membership.mem (γ := Filter β) (map (fun (x : α) ↦ c) f) s ↔ Membership.mem (γ := Filter β) (pure c) s
Tactic: by_cases h : c ∈ s
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
f : Filter α
inst : f.NeBot
c : β
s : Set β
pos :
  ∀ (h : c ∈ s), Membership.mem (γ := Filter β) (map (fun (x : α) ↦ c) f) s ↔ Membership.mem (γ := Filter β) (pure c) s
⊢ Membership.mem (γ := Filter β) (map (fun (x : α) ↦ c) f) s ↔ Membership.mem (γ := Filter β) (pure c) s
have neg : ∀ (h : c ∉ s), Membership.mem (γ := Filter β) (map (fun (x : α) ↦ c) f) s ↔ Membership.mem (γ := Filter β) (pure c) s
Tactic: by_cases h : c ∈ s
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
φ : α → β
θ : α → γ
ψ : β → δ
ρ : γ → δ
H : ψ ∘ φ = ρ ∘ θ
F : Filter α
⊢ map ψ (map φ F) = map ρ (map θ F)
have rw : map (ψ ∘ φ) F = map ρ (map θ F)
Tactic: rw [Filter.map_map, H, ← Filter.map_map]
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
φ : α → β
θ : α → γ
ψ : β → δ
ρ : γ → δ
H : ψ ∘ φ = ρ ∘ θ
F : Filter α
rw : map (ψ ∘ φ) F = map ρ (map θ F)
⊢ map ψ (map φ F) = map ρ (map θ F)
have rw₁ : map (ρ ∘ θ) F = map ρ (map θ F)
Tactic: rw [Filter.map_map, H, ← Filter.map_map]
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
φ : α → β
θ : α → γ
ψ : β → δ
ρ : γ → δ
H : ψ ∘ φ = ρ ∘ θ
F : Filter α
rw : map (ψ ∘ φ) F = map ρ (map θ F)
rw₁ : map (ρ ∘ θ) F = map ρ (map θ F)
⊢ map ψ (map φ F) = map ρ (map θ F)
have rw₂ : map ρ (map θ F) = map ρ (map θ F)
Tactic: rw [Filter.map_map, H, ← Filter.map_map]
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
φ : α → β
θ : α → γ
ψ : β → δ
ρ : γ → δ
H : ψ ∘ φ = ρ ∘ θ
G : Filter δ
⊢ comap φ (comap ψ G) = comap θ (comap ρ G)
have rw : comap (ψ ∘ φ) G = comap θ (comap ρ G)
Tactic: rw [Filter.comap_comap, H, ← Filter.comap_comap]
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
φ : α → β
θ : α → γ
ψ : β → δ
ρ : γ → δ
H : ψ ∘ φ = ρ ∘ θ
G : Filter δ
rw : comap (ψ ∘ φ) G = comap θ (comap ρ G)
⊢ comap φ (comap ψ G) = comap θ (comap ρ G)
have rw₁ : comap (ρ ∘ θ) G = comap θ (comap ρ G)
Tactic: rw [Filter.comap_comap, H, ← Filter.comap_comap]
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
φ : α → β
θ : α → γ
ψ : β → δ
ρ : γ → δ
H : ψ ∘ φ = ρ ∘ θ
G : Filter δ
rw : comap (ψ ∘ φ) G = comap θ (comap ρ G)
rw₁ : comap (ρ ∘ θ) G = comap θ (comap ρ G)
⊢ comap φ (comap ψ G) = comap θ (comap ρ G)
have rw₂ : comap θ (comap ρ G) = comap θ (comap ρ G)
Tactic: rw [Filter.comap_comap, H, ← Filter.comap_comap]
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
g : β → α
hfg : LeftInverse g f
F : Filter α
⊢ map g (map f F) = F
have rw : map (g ∘ f) F = F
Tactic: rw [map_map, hfg.comp_eq_id, map_id]