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 : α → β
g : β → α
hfg : LeftInverse g f
F : Filter α
rw : map (g ∘ f) F = F
⊢ map g (map f F) = F
have rw₁ : map id F = F
Tactic: rw [map_map, hfg.comp_eq_id, map_id]
-- 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 α
rw : map (g ∘ f) F = F
rw₁ : map id F = F
⊢ map g (map f F) = F
have rw₂ : F = F
Tactic: rw [map_map, hfg.comp_eq_id, map_id]
-- 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 α
⊢ comap f (comap g F) = F
have rw : comap (g ∘ f) F = F
Tactic: rw [comap_comap, hfg.comp_eq_id, comap_id]
-- 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 α
rw : comap (g ∘ f) F = F
⊢ comap f (comap g F) = F
have rw₁ : comap id F = F
Tactic: rw [comap_comap, hfg.comp_eq_id, comap_id]
-- 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 α
rw : comap (g ∘ f) F = F
rw₁ : comap id F = F
⊢ comap f (comap g F) = F
have rw₂ : F = F
Tactic: rw [comap_comap, hfg.comp_eq_id, comap_id]
-- Lean 4 proof step from Mathlib.Order.Filter.Map (hypothesis)
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
g : β → α
hfg : LeftInvOn g f s
F : Filter α
hF : F ≤ 𝓟 s
⊢ map g (map f F) = F
have this : g ∘ f =ᶠ[𝓟 s] id
Tactic: have : (g ∘ f) =ᶠ[𝓟 s] id := by simpa only [eventuallyEq_principal] using hfg
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
g : β → α
hfg : LeftInvOn g f s
F : Filter α
hF : F ≤ 𝓟 s
this : g ∘ f =ᶠ[𝓟 s] id
⊢ map g (map f F) = F
have rw : map (g ∘ f) F = F
Tactic: rw [map_map, map_congr (this.filter_mono hF), map_id]
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
g : β → α
hfg : LeftInvOn g f s
F : Filter α
hF : F ≤ 𝓟 s
this : g ∘ f =ᶠ[𝓟 s] id
rw : map (g ∘ f) F = F
⊢ map g (map f F) = F
have rw₁ : map id F = F
Tactic: rw [map_map, map_congr (this.filter_mono hF), map_id]
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
g : β → α
hfg : LeftInvOn g f s
F : Filter α
hF : F ≤ 𝓟 s
this : g ∘ f =ᶠ[𝓟 s] id
rw : map (g ∘ f) F = F
rw₁ : map id F = F
⊢ map g (map f F) = F
have rw₂ : F = F
Tactic: rw [map_map, map_congr (this.filter_mono hF), map_id]
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
F : Filter α
G : Filter β
f_1 f₁ f₂ : Filter α
g g₁ g₂ : Filter β
m_1 : α → β
m' : β → γ
s_1 : Set α
t_1 : Set β
m : α → β
f : Filter α
t : Set β
s : Set α
hs : s ∈ f.sets
hst : kernImage m s ⊆ t
⊢ t ∈ kernImage m '' f.sets
have refine : kernImage m (s ∪ m ⁻¹' t) = t
Tactic: refine ⟨s ∪ m ⁻¹' t, mem_of_superset hs subset_union_left, ?_⟩
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
F : Filter α
G : Filter β
f_1 f₁ f₂ : Filter α
g g₁ g₂ : Filter β
m_1 : α → β
m' : β → γ
s_1 : Set α
t_1 : Set β
m : α → β
f : Filter α
t : Set β
s : Set α
hs : s ∈ f.sets
hst : kernImage m s ⊆ t
⊢ kernImage m (s ∪ m ⁻¹' t) = t
have rw : kernImage m s ∪ t = t
Tactic: rw [kernImage_union_preimage, union_eq_right.mpr hst]
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
F : Filter α
G : Filter β
f_1 f₁ f₂ : Filter α
g g₁ g₂ : Filter β
m_1 : α → β
m' : β → γ
s_1 : Set α
t_1 : Set β
m : α → β
f : Filter α
t : Set β
s : Set α
hs : s ∈ f.sets
hst : kernImage m s ⊆ t
rw : kernImage m s ∪ t = t
⊢ kernImage m (s ∪ m ⁻¹' t) = t
have rw₁ : t = t
Tactic: rw [kernImage_union_preimage, union_eq_right.mpr hst]
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
m : α → β
f : Filter α
s : Set β
⊢ s ∈ kernMap m f ↔ ∃ (t : Set α), tᶜ ∈ f ∧ m '' t = sᶜ
have rw : (∃ (x : Set α), xᶜ ∈ f ∧ kernImage m xᶜ = s) ↔ ∃ (t : Set α), tᶜ ∈ f ∧ m '' t = sᶜ
Tactic: rw [mem_kernMap, compl_surjective.exists]
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
m : α → β
f : Filter α
s : Set β
⊢ (∃ (x : Set α), xᶜ ∈ f ∧ kernImage m xᶜ = s) ↔ ∃ (t : Set α), tᶜ ∈ f ∧ m '' t = sᶜ
have refine : ∀ (x : Set α), xᶜ ∈ f → (kernImage m xᶜ = s ↔ m '' x = sᶜ)
Tactic: refine exists_congr (fun x ↦ and_congr_right fun _ ↦ ?_)
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
m : α → β
f : Filter α
s : Set β
x : Set α
h : xᶜ ∈ f
⊢ kernImage m xᶜ = s ↔ m '' x = sᶜ
have rw : (m '' x)ᶜ = s ↔ m '' x = sᶜ
Tactic: rw [kernImage_compl, compl_eq_comm, eq_comm]
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
m : α → β
f : Filter α
s : Set β
x : Set α
h : xᶜ ∈ f
rw : (m '' x)ᶜ = s ↔ m '' x = sᶜ
⊢ kernImage m xᶜ = s ↔ m '' x = sᶜ
have rw₁ : sᶜ = m '' x ↔ m '' x = sᶜ
Tactic: rw [kernImage_compl, compl_eq_comm, eq_comm]
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
m : α → β
f : Filter α
s : Set β
x : Set α
h : xᶜ ∈ f
rw : (m '' x)ᶜ = s ↔ m '' x = sᶜ
rw₁ : sᶜ = m '' x ↔ m '' x = sᶜ
⊢ kernImage m xᶜ = s ↔ m '' x = sᶜ
have rw₂ : m '' x = sᶜ ↔ m '' x = sᶜ
Tactic: rw [kernImage_compl, compl_eq_comm, eq_comm]
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
m : α → β
f : Filter α
s : Set β
⊢ sᶜ ∈ kernMap m f ↔ ∃ (t : Set α), tᶜ ∈ f ∧ m '' t = s
have simp_rw : (∃ (t : Set α), tᶜ ∈ f ∧ m '' t = sᶜᶜ) ↔ ∃ (t : Set α), tᶜ ∈ f ∧ m '' t = s
Tactic: simp_rw [mem_kernMap_iff_compl, compl_compl]
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
m : α → β
s : Set α
⊢ kernMap m (𝓟 s) = 𝓟 (kernImage m s)
have refine : ∀ (g : Filter β), g ≤ kernMap m (𝓟 s) ↔ g ≤ 𝓟 (kernImage m s)
Tactic: refine eq_of_forall_le_iff (fun g ↦ ?_)
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
m : α → β
s : Set α
g : Filter β
⊢ g ≤ kernMap m (𝓟 s) ↔ g ≤ 𝓟 (kernImage m s)
have rw : comap m g ≤ 𝓟 s ↔ g ≤ 𝓟 (kernImage m s)
Tactic: rw [← comap_le_iff_le_kernMap, le_principal_iff, le_principal_iff, mem_comap'']
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
m : α → β
s : Set α
g : Filter β
rw : comap m g ≤ 𝓟 s ↔ g ≤ 𝓟 (kernImage m s)
⊢ g ≤ kernMap m (𝓟 s) ↔ g ≤ 𝓟 (kernImage m s)
have rw₁ : s ∈ comap m g ↔ g ≤ 𝓟 (kernImage m s)
Tactic: rw [← comap_le_iff_le_kernMap, le_principal_iff, le_principal_iff, mem_comap'']
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
m : α → β
s : Set α
g : Filter β
rw : comap m g ≤ 𝓟 s ↔ g ≤ 𝓟 (kernImage m s)
rw₁ : s ∈ comap m g ↔ g ≤ 𝓟 (kernImage m s)
⊢ g ≤ kernMap m (𝓟 s) ↔ g ≤ 𝓟 (kernImage m s)
have rw₂ : s ∈ comap m g ↔ kernImage m s ∈ g
Tactic: rw [← comap_le_iff_le_kernMap, le_principal_iff, le_principal_iff, mem_comap'']
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
m : α → β
s : Set α
g : Filter β
rw : comap m g ≤ 𝓟 s ↔ g ≤ 𝓟 (kernImage m s)
rw₁ : s ∈ comap m g ↔ g ≤ 𝓟 (kernImage m s)
rw₂ : s ∈ comap m g ↔ kernImage m s ∈ g
⊢ g ≤ kernMap m (𝓟 s) ↔ g ≤ 𝓟 (kernImage m s)
have rw₃ : kernImage m s ∈ g ↔ kernImage m s ∈ g
Tactic: rw [← comap_le_iff_le_kernMap, le_principal_iff, le_principal_iff, mem_comap'']
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_6
s : Set α
t : Set (↑s : Type u_6)
⊢ 𝓟 t = comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (𝓟 (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t))
have rw : 𝓟 t = 𝓟 (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t)
Tactic: rw [comap_principal, preimage_image_eq _ Subtype.coe_injective]
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_6
s : Set α
t : Set (↑s : Type u_6)
rw : 𝓟 t = 𝓟 (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t)
⊢ 𝓟 t = comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (𝓟 (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t))
have rw₁ : 𝓟 t = 𝓟 t
Tactic: rw [comap_principal, preimage_image_eq _ Subtype.coe_injective]
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
m : α → β
b : β
⊢ comap m (pure b) = 𝓟 (m ⁻¹' {b})
have rw : comap m (𝓟 {b}) = 𝓟 (m ⁻¹' {b})
Tactic: rw [← principal_singleton, comap_principal]
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
m : α → β
b : β
rw : comap m (𝓟 {b}) = 𝓟 (m ⁻¹' {b})
⊢ comap m (pure b) = 𝓟 (m ⁻¹' {b})
have rw₁ : 𝓟 (m ⁻¹' {b}) = 𝓟 (m ⁻¹' {b})
Tactic: rw [← principal_singleton, comap_principal]
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
⊢ map f ⊤ = 𝓟 (range f)
have rw : map f (𝓟 univ) = 𝓟 (range f)
Tactic: rw [← principal_univ, map_principal, image_univ]
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
rw : map f (𝓟 univ) = 𝓟 (range f)
⊢ map f ⊤ = 𝓟 (range f)
have rw₁ : 𝓟 (f '' univ) = 𝓟 (range f)
Tactic: rw [← principal_univ, map_principal, image_univ]
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
rw : map f (𝓟 univ) = 𝓟 (range f)
rw₁ : 𝓟 (f '' univ) = 𝓟 (range f)
⊢ map f ⊤ = 𝓟 (range f)
have rw₂ : 𝓟 (range f) = 𝓟 (range f)
Tactic: rw [← principal_univ, map_principal, image_univ]
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
l : Filter α
⊢ l ≤ comap f ⊤
have rw : l ≤ ⊤
Tactic: rw [comap_top]
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
g : Filter β
m : α → β
h : (comap m g).NeBot
⊢ g.NeBot
have rw : ∀ (h : comap m g ≠ ⊥), g ≠ ⊥
Tactic: rw [neBot_iff] at *
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
g : Filter β
m : α → β
h : comap m g ≠ ⊥
⊢ g ≠ ⊥
have contrapose : ∀ (h : g = ⊥), comap m g = ⊥
Tactic: contrapose h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
g : Filter β
m : α → β
h : g = ⊥
⊢ comap m g = ⊥
have rw : comap m ⊥ = ⊥
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
g₁ g₂ : Filter β
m : α → β
⊢ comap m (g₁ ⊔ g₂) = comap m g₁ ⊔ comap m g₂
have rw : comap m (⨆ (b : Bool), bif b then g₁ else g₂) = comap m g₁ ⊔ comap m g₂
Tactic: rw [sup_eq_iSup, comap_iSup, iSup_bool_eq, Bool.cond_true, Bool.cond_false]
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
g₁ g₂ : Filter β
m : α → β
rw : comap m (⨆ (b : Bool), bif b then g₁ else g₂) = comap m g₁ ⊔ comap m g₂
⊢ comap m (g₁ ⊔ g₂) = comap m g₁ ⊔ comap m g₂
have rw₁ : ⨆ (i : Bool), comap m (bif i then g₁ else g₂) = comap m g₁ ⊔ comap m g₂
Tactic: rw [sup_eq_iSup, comap_iSup, iSup_bool_eq, Bool.cond_true, Bool.cond_false]
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
g₁ g₂ : Filter β
m : α → β
rw : comap m (⨆ (b : Bool), bif b then g₁ else g₂) = comap m g₁ ⊔ comap m g₂
rw₁ : ⨆ (i : Bool), comap m (bif i then g₁ else g₂) = comap m g₁ ⊔ comap m g₂
⊢ comap m (g₁ ⊔ g₂) = comap m g₁ ⊔ comap m g₂
have rw₂ : comap m (bif true then g₁ else g₂) ⊔ comap m (bif false then g₁ else g₂) = comap m g₁ ⊔ comap m g₂
Tactic: rw [sup_eq_iSup, comap_iSup, iSup_bool_eq, Bool.cond_true, Bool.cond_false]
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
g₁ g₂ : Filter β
m : α → β
rw : comap m (⨆ (b : Bool), bif b then g₁ else g₂) = comap m g₁ ⊔ comap m g₂
rw₁ : ⨆ (i : Bool), comap m (bif i then g₁ else g₂) = comap m g₁ ⊔ comap m g₂
rw₂ : comap m (bif true then g₁ else g₂) ⊔ comap m (bif false then g₁ else g₂) = comap m g₁ ⊔ comap m g₂
⊢ comap m (g₁ ⊔ g₂) = comap m g₁ ⊔ comap m g₂
have rw₃ : comap m g₁ ⊔ comap m (bif false then g₁ else g₂) = comap m g₁ ⊔ comap m g₂
Tactic: rw [sup_eq_iSup, comap_iSup, iSup_bool_eq, Bool.cond_true, Bool.cond_false]
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
g₁ g₂ : Filter β
m : α → β
rw : comap m (⨆ (b : Bool), bif b then g₁ else g₂) = comap m g₁ ⊔ comap m g₂
rw₁ : ⨆ (i : Bool), comap m (bif i then g₁ else g₂) = comap m g₁ ⊔ comap m g₂
rw₂ : comap m (bif true then g₁ else g₂) ⊔ comap m (bif false then g₁ else g₂) = comap m g₁ ⊔ comap m g₂
rw₃ : comap m g₁ ⊔ comap m (bif false then g₁ else g₂) = comap m g₁ ⊔ comap m g₂
⊢ comap m (g₁ ⊔ g₂) = comap m g₁ ⊔ comap m g₂
have rw₄ : comap m g₁ ⊔ comap m g₂ = comap m g₁ ⊔ comap m g₂
Tactic: rw [sup_eq_iSup, comap_iSup, iSup_bool_eq, Bool.cond_true, Bool.cond_false]
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
f : Filter β
m : α → β
⊢ map m (comap m f) = f ⊓ 𝓟 (range m)
have refine : f ⊓ 𝓟 (range m) ≤ map m (comap m f)
Tactic: refine le_antisymm (le_inf map_comap_le <| le_principal_iff.2 range_mem_map) ?_
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
f : Filter β
m : α → β
t' t : Set β
ht : t ∈ f
sub : m ⁻¹' t ⊆ m ⁻¹' t'
⊢ t' ∈ f ⊓ 𝓟 (range m)
have refine : t ⊆ {x : β | x ∈ range m → x ∈ t'}
Tactic: refine mem_inf_principal.2 (mem_of_superset ht ?_)
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
β : Type u_2
f : Filter β
s : Set β
⊢ map (α := { x : β // x ∈ s }) (Subtype.val (p := fun (x : β) ↦ x ∈ s))
      (comap (Subtype.val (p := fun (x : β) ↦ x ∈ s)) f) =
    f ⊓ 𝓟 s
have rw : f ⊓ 𝓟 (range (ι := { x : β // x ∈ s }) (Subtype.val (p := fun (x : β) ↦ x ∈ s))) = f ⊓ 𝓟 s
Tactic: rw [map_comap, Subtype.range_val]
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
β : Type u_2
f : Filter β
s : Set β
rw : f ⊓ 𝓟 (range (ι := { x : β // x ∈ s }) (Subtype.val (p := fun (x : β) ↦ x ∈ s))) = f ⊓ 𝓟 s
⊢ map (α := { x : β // x ∈ s }) (Subtype.val (p := fun (x : β) ↦ x ∈ s))
      (comap (Subtype.val (p := fun (x : β) ↦ x ∈ s)) f) =
    f ⊓ 𝓟 s
have rw₁ : f ⊓ 𝓟 s = f ⊓ 𝓟 s
Tactic: rw [map_comap, Subtype.range_val]
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
f : Filter β
m : α → β
hf : range m ∈ f
⊢ map m (comap m f) = f
have rw : f ⊓ 𝓟 (range m) = f
Tactic: rw [map_comap, inf_eq_left.2 (le_principal_iff.2 hf)]
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
f : Filter β
m : α → β
hf : range m ∈ f
rw : f ⊓ 𝓟 (range m) = f
⊢ map m (comap m f) = f
have rw₁ : f = f
Tactic: rw [map_comap, inf_eq_left.2 (le_principal_iff.2 hf)]
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
s : Set α
f : Filter α
⊢ map (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s))
      (comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) f) =
    f ⊓ 𝓟 s
have rw : f ⊓ 𝓟 (range (ι := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s))) = f ⊓ 𝓟 s
Tactic: rw [map_comap, Subtype.range_coe]
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
s : Set α
f : Filter α
rw : f ⊓ 𝓟 (range (ι := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s))) = f ⊓ 𝓟 s
⊢ map (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s))
      (comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) f) =
    f ⊓ 𝓟 s
have rw₁ : f ⊓ 𝓟 s = f ⊓ 𝓟 s
Tactic: rw [map_comap, Subtype.range_coe]
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
f : Filter α
c : β → α
h : range c ∈ f
W : Set β
W_in : W ∈ comap c f
⊢ c '' W ∈ f
have rw : c '' W ∈ map c (comap c f)
Tactic: rw [← map_comap_of_mem h]
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
f : Filter β
m : α → β
inj : Injective m
large : range m ∈ f
S : Set α
⊢ S ∈ comap m f ↔ m '' S ∈ f
have rw : m '' S ∈ map m (comap m f) ↔ m '' S ∈ f
Tactic: rw [← image_mem_map_iff inj, map_comap_of_mem large]
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
f : Filter β
m : α → β
inj : Injective m
large : range m ∈ f
S : Set α
rw : m '' S ∈ map m (comap m f) ↔ m '' S ∈ f
⊢ S ∈ comap m f ↔ m '' S ∈ f
have rw₁ : m '' S ∈ f ↔ m '' S ∈ f
Tactic: rw [← image_mem_map_iff inj, map_comap_of_mem large]
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
f g : Filter α
m : α → β
hm : Injective m
⊢ map m f ≤ map m g ↔ f ≤ g
have rw : f ≤ comap m (map m g) ↔ f ≤ g
Tactic: rw [map_le_iff_le_comap, comap_map hm]
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
f g : Filter α
m : α → β
hm : Injective m
rw : f ≤ comap m (map m g) ↔ f ≤ g
⊢ map m f ≤ map m g ↔ f ≤ g
have rw₁ : f ≤ g ↔ f ≤ g
Tactic: rw [map_le_iff_le_comap, comap_map hm]
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
f : Filter β
m : α → β
⊢ (comap m f).NeBot ↔ ∀ t ∈ f, ∃ (a : α), m a ∈ t
have simp : (∀ (s : Set α), ∀ x ∈ f, m ⁻¹' x ⊆ s → s.Nonempty) ↔ ∀ t ∈ f, ∃ (a : α), m a ∈ t
Tactic: simp only [← forall_mem_nonempty_iff_neBot, mem_comap, forall_exists_index, and_imp]
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
f : Filter β
m : α → β
hm : Surjective m
⊢ comap m f = ⊥ ↔ f = ⊥
have rw : (range m)ᶜ ∈ f ↔ f = ⊥
Tactic: rw [comap_eq_bot_iff_compl_range, hm.range_eq, compl_univ, empty_mem_iff_bot]
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
f : Filter β
m : α → β
hm : Surjective m
rw : (range m)ᶜ ∈ f ↔ f = ⊥
⊢ comap m f = ⊥ ↔ f = ⊥
have rw₁ : univᶜ ∈ f ↔ f = ⊥
Tactic: rw [comap_eq_bot_iff_compl_range, hm.range_eq, compl_univ, empty_mem_iff_bot]
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
f : Filter β
m : α → β
hm : Surjective m
rw : (range m)ᶜ ∈ f ↔ f = ⊥
rw₁ : univᶜ ∈ f ↔ f = ⊥
⊢ comap m f = ⊥ ↔ f = ⊥
have rw₂ : ∅ ∈ f ↔ f = ⊥
Tactic: rw [comap_eq_bot_iff_compl_range, hm.range_eq, compl_univ, empty_mem_iff_bot]
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
f : Filter β
m : α → β
hm : Surjective m
rw : (range m)ᶜ ∈ f ↔ f = ⊥
rw₁ : univᶜ ∈ f ↔ f = ⊥
rw₂ : ∅ ∈ f ↔ f = ⊥
⊢ comap m f = ⊥ ↔ f = ⊥
have rw₃ : f = ⊥ ↔ f = ⊥
Tactic: rw [comap_eq_bot_iff_compl_range, hm.range_eq, compl_univ, empty_mem_iff_bot]
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
g₁ g₂ : Filter β
m : α → β
h : Surjective m
⊢ Disjoint (comap m g₁) (comap m g₂) ↔ Disjoint g₁ g₂
have rw : comap m g₁ ⊓ comap m g₂ = ⊥ ↔ Disjoint g₁ g₂
Tactic: rw [disjoint_iff, disjoint_iff, ← comap_inf, comap_surjective_eq_bot h]
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
g₁ g₂ : Filter β
m : α → β
h : Surjective m
rw : comap m g₁ ⊓ comap m g₂ = ⊥ ↔ Disjoint g₁ g₂
⊢ Disjoint (comap m g₁) (comap m g₂) ↔ Disjoint g₁ g₂
have rw₁ : comap m g₁ ⊓ comap m g₂ = ⊥ ↔ g₁ ⊓ g₂ = ⊥
Tactic: rw [disjoint_iff, disjoint_iff, ← comap_inf, comap_surjective_eq_bot h]
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
g₁ g₂ : Filter β
m : α → β
h : Surjective m
rw : comap m g₁ ⊓ comap m g₂ = ⊥ ↔ Disjoint g₁ g₂
rw₁ : comap m g₁ ⊓ comap m g₂ = ⊥ ↔ g₁ ⊓ g₂ = ⊥
⊢ Disjoint (comap m g₁) (comap m g₂) ↔ Disjoint g₁ g₂
have rw₂ : comap m (g₁ ⊓ g₂) = ⊥ ↔ g₁ ⊓ g₂ = ⊥
Tactic: rw [disjoint_iff, disjoint_iff, ← comap_inf, comap_surjective_eq_bot h]
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
g₁ g₂ : Filter β
m : α → β
h : Surjective m
rw : comap m g₁ ⊓ comap m g₂ = ⊥ ↔ Disjoint g₁ g₂
rw₁ : comap m g₁ ⊓ comap m g₂ = ⊥ ↔ g₁ ⊓ g₂ = ⊥
rw₂ : comap m (g₁ ⊓ g₂) = ⊥ ↔ g₁ ⊓ g₂ = ⊥
⊢ Disjoint (comap m g₁) (comap m g₂) ↔ Disjoint g₁ g₂
have rw₃ : g₁ ⊓ g₂ = ⊥ ↔ g₁ ⊓ g₂ = ⊥
Tactic: rw [disjoint_iff, disjoint_iff, ← comap_inf, comap_surjective_eq_bot h]
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
g : Filter β
⊢ Eq.{u_1 + 1} (α := Filter α) (comap inl (map inr g)) ⊥
have h : ∀ (s : Set α), Membership.mem (γ := Filter α) (comap inl (map inr g)) s ↔ Membership.mem (γ := Filter α) ⊥ s
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
g : Filter β
s : Set α
⊢ Membership.mem (γ := Filter α) (comap inl (map inr g)) s ↔ Membership.mem (γ := Filter α) ⊥ s
have h : Membership.mem (γ := Filter (α ⊕ β)) (map inr g) (inl '' sᶜ)ᶜ ↔ Membership.mem (γ := Filter α) ⊥ s
Tactic: rw [mem_comap_iff_compl]
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
f : Filter α
⊢ Eq.{u_2 + 1} (α := Filter β) (comap inr (map inl f)) ⊥
have h : ∀ (s : Set β), Membership.mem (γ := Filter β) (comap inr (map inl f)) s ↔ Membership.mem (γ := Filter β) ⊥ s
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
f : Filter α
s : Set β
⊢ Membership.mem (γ := Filter β) (comap inr (map inl f)) s ↔ Membership.mem (γ := Filter β) ⊥ s
have h : Membership.mem (γ := Filter (α ⊕ β)) (map inl f) (inr '' sᶜ)ᶜ ↔ Membership.mem (γ := Filter β) ⊥ s
Tactic: rw [mem_comap_iff_compl]
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
⊢ map inl f ⊓ map inr g = ⊥
have apply : map inl f ⊓ map inr g ≤ ⊥
Tactic: apply le_bot_iff.mp
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
⊢ map inl f ⊓ map inr g ≤ ⊥
have trans : map inl f ⊓ map inr g ≤ map inl ⊤ ⊓ map inr ⊤
Tactic: trans map inl ⊤ ⊓ map inr ⊤
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
trans : map inl f ⊓ map inr g ≤ map inl ⊤ ⊓ map inr ⊤
⊢ map inl f ⊓ map inr g ≤ ⊥
have trans₁ : LE.le (α := Filter (α ⊕ β)) (map inl ⊤ ⊓ map inr ⊤) ⊥
Tactic: trans map inl ⊤ ⊓ map inr ⊤
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
⊢ map inl f ⊓ map inr g ≤ map inl ⊤ ⊓ map inr ⊤
have h₁ : LE.le (α := Filter (α ⊕ β)) (map inl f) (map inl ⊤)
Tactic: apply inf_le_inf
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
h₁ : LE.le (α := Filter (α ⊕ β)) (map inl f) (map inl ⊤)
⊢ map inl f ⊓ map inr g ≤ map inl ⊤ ⊓ map inr ⊤
have h₂ : LE.le (α := Filter (α ⊕ β)) (map inr g) (map inr ⊤)
Tactic: apply inf_le_inf
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
⊢ map inr f ⊓ map inl g = ⊥
have rw : map inl g ⊓ map inr f = ⊥
Tactic: rw [inf_comm, map_inl_inf_map_inr]
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
rw : map inl g ⊓ map inr f = ⊥
⊢ map inr f ⊓ map inl g = ⊥
have rw₁ : Eq (α := Filter (β ⊕ α)) ⊥ ⊥
Tactic: rw [inf_comm, map_inl_inf_map_inr]
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
l : Filter γ
m₁ : α → γ
m₂ : β → γ
⊢ comap (Sum.elim m₁ m₂) l = map inl (comap m₁ l) ⊔ map inr (comap m₂ l)
have h : ∀ (s : Set (α ⊕ β)), s ∈ comap (Sum.elim m₁ m₂) l ↔ s ∈ map inl (comap m₁ l) ⊔ map inr (comap m₂ l)
Tactic: ext s
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
l : Filter γ
m₁ : α → γ
m₂ : β → γ
s : Set (α ⊕ β)
⊢ s ∈ comap (Sum.elim m₁ m₂) l ↔ s ∈ map inl (comap m₁ l) ⊔ map inr (comap m₂ l)
have h : (Sum.elim m₁ m₂ '' sᶜ)ᶜ ∈ l ↔ (m₁ '' (inl ⁻¹' s)ᶜ)ᶜ ∈ l ∧ (m₂ '' (inr ⁻¹' s)ᶜ)ᶜ ∈ l
Tactic: simp_rw [mem_sup, mem_map, mem_comap_iff_compl]
-- Lean 4 proof step from Mathlib.Order.Filter.Map (goal)
Goal:
α : Type u_1
β : Type u_2
l : Filter (α ⊕ β)
⊢ map inl (comap inl l) ⊔ map inr (comap inr l) = l
have rw : comap (Sum.elim inl inr) l = l
Tactic: rw [← comap_sumElim_eq, Sum.elim_inl_inr, comap_id]