awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Filter.Ultrafilter.Defs
Goal:
α : Type u
f : Ultrafilter α
⊢ map (fun (x : α) ↦ x) f = f

Tactic:
map_id _

Premises used: Ultrafilter.map_id
-- Module: Mathlib.Order.Filter.Ultrafilter.Defs
Goal:
α : Type u
β : Type v
γ : Type u_1
f : Ultrafilter α
m : α → β
n : β → γ
⊢ map n (map m f) = map (n ∘ m) f

Tactic:
coe_injective map_map

Premises used: Filter.map_map, Ultrafilter.coe_injective
-- Module: Mathlib.Order.Filter.Ultrafilter.Defs
Goal:
α : Type u
β : Type v
γ : Type u_1
f g_1 : Ultrafilter α
s t : Set α
p q : α → Prop
m : α → β
u : Ultrafilter β
inj : Injective m
large : range m ∈ u
g : Filter α
hg : g.NeBot
hgu : g ≤ Filter.comap m (↑u : Filter β)
⊢ Filter.comap m (↑u : Filter β) ≤ g

Tactic:
simp only [← u.unique (map_le_iff_le_comap.2 hgu), comap_map inj, le_rfl]

Premises used: Iff.mpr, le_rfl, Filter.comap_map, Filter.map_le_iff_le_comap, Ultrafilter.unique
-- Module: Mathlib.Order.Filter.Ultrafilter.Defs
Goal:
α : Type u
β : Type v
m : α → β
u : Ultrafilter β
inj : Injective m
large : range m ∈ u
s : Set α
⊢ s ∈ u.comap inj large ↔ m '' s ∈ u

Tactic:
mem_comap_iff inj large

Premises used: Set.Mem, Filter.mem_comap_iff
-- Module: Mathlib.Order.Filter.Ultrafilter.Defs
Goal:
α : Type u
β : Type v
m : α → β
u : Ultrafilter β
inj : Injective m
large : range m ∈ u
⊢ (↑(u.comap inj large) : Filter α) = Filter.comap m (↑u : Filter β)

Tactic:
rfl

Premises used: rfl, Filter.comap
-- Module: Mathlib.Order.Filter.Ultrafilter.Defs
Goal:
α : Type u
β : Type v
γ : Type u_1
f_1 g : Ultrafilter α
s t : Set α
p q : α → Prop
f : Ultrafilter α
h₀ : optParam (Injective.{u + 1, u + 1} (α := α) id) ⋯
rw : univ ∈ f
⊢ range id ∈ f

Tactic:
rw [range_id]

Premises used: Set.range_id
-- Module: Mathlib.Order.Filter.Ultrafilter.Defs
Goal:
α : Type u
β : Type v
γ : Type u_1
f_1 g : Ultrafilter α
s t : Set α
p q : α → Prop
f : Ultrafilter α
h₀ : optParam (Injective.{u + 1, u + 1} (α := α) id) ⋯
⊢ univ ∈ f

Tactic:
univ_mem

Premises used: Filter.univ_mem
-- Module: Mathlib.Order.Filter.Ultrafilter.Defs
Goal:
α : Type u
β : Type v
γ : Type u_1
f_1 g : Ultrafilter α
s t : Set α
p q : α → Prop
f : Ultrafilter α
h₀ : optParam (Injective.{u + 1, u + 1} (α := α) id) ⋯
⊢ univ ∈ f

Tactic:
exact univ_mem

Premises used: Filter.univ_mem
-- Module: Mathlib.Order.Filter.Ultrafilter.Defs
Goal:
α : Type u
f : Ultrafilter α
h₀ : Injective.{u + 1, u + 1} (α := α) id
h₁ : range id ∈ f
⊢ f.comap h₀ h₁ = f

Tactic:
coe_injective comap_id

Premises used: Filter.comap_id, Ultrafilter.coe_injective
-- Module: Mathlib.Order.Filter.Ultrafilter.Defs
Goal:
α : Type u
β : Type v
γ : Type u_1
f_1 g : Ultrafilter α
s t : Set α
p q : α → Prop
f : Ultrafilter γ
m : α → β
n : β → γ
inj₀ : Injective n
large₀ : range n ∈ f
inj₁ : Injective m
large₁ : range m ∈ f.comap inj₀ large₀
inj₂ : optParam (Injective (n ∘ m)) ⋯
rw : n '' range m ∈ f
⊢ range (n ∘ m) ∈ f

Tactic:
rw [range_comp]

Premises used: Set.range_comp
-- Module: Mathlib.Order.Filter.Ultrafilter.Defs
Goal:
α : Type u
β : Type v
γ : Type u_1
f_1 g : Ultrafilter α
s t : Set α
p q : α → Prop
f : Ultrafilter γ
m : α → β
n : β → γ
inj₀ : Injective n
large₀ : range n ∈ f
inj₁ : Injective m
large₁ : range m ∈ f.comap inj₀ large₀
inj₂ : optParam (Injective (n ∘ m)) ⋯
⊢ n '' range m ∈ f

Tactic:
image_mem_of_mem_comap large₀ large₁

Premises used: Filter.image_mem_of_mem_comap
-- Module: Mathlib.Order.Filter.Ultrafilter.Defs
Goal:
α : Type u
β : Type v
γ : Type u_1
f_1 g : Ultrafilter α
s t : Set α
p q : α → Prop
f : Ultrafilter γ
m : α → β
n : β → γ
inj₀ : Injective n
large₀ : range n ∈ f
inj₁ : Injective m
large₁ : range m ∈ f.comap inj₀ large₀
inj₂ : optParam (Injective (n ∘ m)) ⋯
⊢ n '' range m ∈ f

Tactic:
exact image_mem_of_mem_comap large₀ large₁

Premises used: Filter.image_mem_of_mem_comap
-- Module: Mathlib.Order.Filter.Ultrafilter.Defs
Goal:
α : Type u
β : Type v
γ : Type u_1
f : Ultrafilter γ
m : α → β
n : β → γ
inj₀ : Injective n
large₀ : range n ∈ f
inj₁ : Injective m
large₁ : range m ∈ f.comap inj₀ large₀
inj₂ : Injective (n ∘ m)
large₂ : range (n ∘ m) ∈ f
⊢ (f.comap inj₀ large₀).comap inj₁ large₁ = f.comap inj₂ large₂

Tactic:
coe_injective comap_comap

Premises used: Filter.comap_comap, Ultrafilter.coe_injective
-- Module: Mathlib.Order.Filter.Ultrafilter.Defs
Goal:
α : Type u
β : Type v
γ : Type u_1
f g : Ultrafilter α
s_1 t : Set α
p q : α → Prop
α_1 : Type u_2
a : α_1
s : Set α_1
⊢ sᶜ ∉ pure a ↔ Membership.mem (γ := Filter α_1) (pure a) s

Tactic:
simp
-- Module: Mathlib.Order.Filter.Ultrafilter.Defs
Goal:
α : Type u
a : α
s : Set α
⊢ Membership.mem (γ := Ultrafilter α) (pure a) s ↔ a ∈ s

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.Order.Filter.Ultrafilter.Defs
Goal:
α : Type u
a : α
⊢ (↑(pure a) : Filter α) = pure a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Filter.Ultrafilter.Defs
Goal:
α : Type u
β : Type v
m : α → β
a : α
⊢ map m (pure a) = pure (m a)

Tactic:
rfl

Premises used: Set.Mem, Filter.map, setOf, Set.preimage, Filter.copy, Ultrafilter.map, rfl
-- Module: Mathlib.Order.Filter.Ultrafilter.Defs
Goal:
α : Type u
β : Type v
m : α → β
a : α
inj : Injective m
large : Membership.mem (γ := Ultrafilter β) (pure (m a)) (range m)
rw : 𝓟 (m ⁻¹' {m a}) = pure a
rw₁ : 𝓟 (m ⁻¹' {m a}) = 𝓟 {a}
rw₂ : 𝓟 (m ⁻¹' m '' {a}) = 𝓟 {a}
rw₃ rw₄ : Eq (α := Filter α) (𝓟 {a}) (𝓟 {a})
⊢ 𝓟 (m ⁻¹' {m a}) = (↑(pure a) : Filter α)

Tactic:
rw [coe_pure, ← principal_singleton, ← image_singleton, preimage_image_eq _ inj]

Premises used: Ultrafilter.coe_pure, Set.image_singleton, Filter.principal_singleton, Set.preimage_image_eq
-- Module: Mathlib.Order.Filter.Ultrafilter.Defs
Goal:
α : Type u
⊢ Injective.{u + 1, u + 1} (α := α) (β := Ultrafilter α) pure

Tactic:
fun _ _ h =>
  Filter.pure_injective (congr_arg Ultrafilter.toFilter h :)

Premises used: Filter.pure_injective, congr_arg, Function.Injective, Ultrafilter.toFilter
-- Module: Mathlib.Order.Filter.Ultrafilter.Defs
Goal:
α : Type u
β : Type v
γ : Type u_1
f g : Ultrafilter α
s t : Set α
p q : α → Prop
inst : Nonempty α
⊢ Nonempty.{u + 1} (Ultrafilter α)

Tactic:
Nonempty.map pure inferInstance

Premises used: Pure.pure, inferInstance, Nonempty.map
-- Module: Mathlib.Order.Filter.Ultrafilter.Defs
Goal:
α : Type u
β : Type v
γ : Type u_1
f_1 g : Ultrafilter α
s_1 t : Set α
p q : α → Prop
f : Ultrafilter α
m : α → Ultrafilter β
s : Set β
⊢ (sᶜ ∉ (↑f : Filter α).bind fun (x : α) ↦ (↑(m x) : Filter β)) ↔
    Membership.mem (γ := Filter β) ((↑f : Filter α).bind fun (x : α) ↦ (↑(m x) : Filter β)) s

Tactic:
simp only [mem_bind', mem_coe, ← compl_mem_iff_notMem, compl_setOf, compl_compl]

Premises used: compl_compl, Filter.mem_bind', Ultrafilter.compl_mem_iff_notMem, Ultrafilter.mem_coe, Set.compl_setOf
-- Module: Mathlib.Order.Filter.Ultrafilter.Defs
Goal:
α : Type u
f : Filter α
h : f.NeBot
⊢ ∃ (u : Ultrafilter α), (↑u : Filter α) ≤ f

Tactic:
let ⟨u, hu, huf⟩ := (eq_bot_or_exists_atom_le f).resolve_left h.ne
  ⟨ofAtom u hu, huf⟩

Premises used: Filter.NeBot.ne, IsAtomic.eq_bot_or_exists_atom_le, Exists, Or.resolve_left, LE.le, Exists.intro, Ultrafilter.ofAtom, Ultrafilter.toFilter, _private.0.Ultrafilter.exists_le.match_1
-- Module: Mathlib.Order.Filter.Ultrafilter.Defs
Goal:
α : Type u
f : Filter α
inst : f.NeBot
⊢ (↑(of f) : Filter α) ≤ f

Tactic:
Classical.choose_spec (exists_le f)

Premises used: Set.Mem, Classical.choose_spec, Ultrafilter.exists_le
-- Module: Mathlib.Order.Filter.Ultrafilter.Defs
Goal:
α : Type u
f : Ultrafilter α
⊢ of (↑f : Filter α) = f

Tactic:
coe_inj.1 <| f.unique (of_le f.toFilter)

Premises used: Ultrafilter.coe_inj, Ultrafilter.of_le, Iff.mp, Ultrafilter.unique, Ultrafilter.toFilter
-- Module: Mathlib.Order.Filter.Ultrafilter.Defs
Goal:
α : Type u
a : α
⊢ IsAtom (α := Filter α) (pure a)

Tactic:
(pure a : Ultrafilter α).isAtom

Premises used: Pure.pure, Ultrafilter.isAtom
-- Module: Mathlib.Order.Filter.Ultrafilter.Defs
Goal:
α : Type u
f : Filter α
a : α
hf : f.NeBot
⊢ f ≤ pure a ↔ f = pure a

Tactic:
⟨Ultrafilter.unique (pure a), le_of_eq⟩

Premises used: Pure.pure, Iff.intro, Ultrafilter.unique, le_of_eq
-- Module: Mathlib.Order.Filter.Ultrafilter.Defs
Goal:
α : Type u
f : Filter α
hf : f.NeBot
x : α
rw : f ≤ pure x ↔ {x} ∈ f
rw₁ rw₂ : {x} ∈ f ↔ {x} ∈ f
⊢ f = pure x ↔ {x} ∈ f

Tactic:
rw [← hf.le_pure_iff, le_pure_iff]

Premises used: Filter.le_pure_iff, Filter.NeBot.le_pure_iff
-- Module: Mathlib.Order.Filter.Ultrafilter.Defs
Goal:
α : Type u
f : Filter α
a : α
⊢ f < pure a ↔ f = ⊥

Tactic:
isAtom_pure.lt_iff

Premises used: IsAtom.lt_iff, Filter.isAtom_pure
-- Module: Mathlib.Order.Filter.Ultrafilter.Defs
Goal:
α : Type u
f : Filter α
a : α
⊢ f ≤ pure a ↔ f = ⊥ ∨ f = pure a

Tactic:
isAtom_pure.le_iff

Premises used: Filter.isAtom_pure, IsAtom.le_iff
-- Module: Mathlib.Order.Filter.Ultrafilter.Defs
Goal:
α : Type u
a : α
⊢ Eq (α := Set (Filter α)) (Iic (pure a)) {⊥, pure a}

Tactic:
isAtom_pure.Iic_eq

Premises used: Filter.isAtom_pure, IsAtom.Iic_eq
-- Module: Mathlib.Order.Filter.Ultrafilter.Defs
Goal:
α : Type u
f : Filter α
s : Set α
⊢ s ∈ f ↔ ∀ (g : Ultrafilter α), (↑g : Filter α) ≤ f → s ∈ g

Tactic:
⟨fun hf g hg => hg hf, fun H => by_contra fun hf => ?_⟩

Premises used: Iff.intro, by_contra
-- Module: Mathlib.Order.Filter.Ultrafilter.Defs
Goal:
α : Type u
f : Filter α
s : Set α
refine : ∀ (H : ∀ (g : Ultrafilter α), (↑g : Filter α) ≤ f → s ∈ g) (hf : s ∉ f), False
⊢ s ∈ f ↔ ∀ (g : Ultrafilter α), (↑g : Filter α) ≤ f → s ∈ g

Tactic:
refine ⟨fun hf g hg => hg hf, fun H => by_contra fun hf => ?_⟩
-- Module: Mathlib.Order.Filter.Ultrafilter.Defs
Goal:
α : Type u
f : Filter α
s : Set α
H : ∀ (g : Ultrafilter α), (↑g : Filter α) ≤ f → s ∈ g
hf : s ∉ f
g : Filter (↑sᶜ : Type u) := comap (Subtype.val (p := fun (x : α) ↦ x ∈ sᶜ)) f
⊢ (range (ι := (↑sᶜ : Type u)) (Subtype.val (p := fun (x : α) ↦ x ∈ sᶜ)))ᶜ ∉ f

Tactic:
simpa [compl_setOf]

Premises used: Set.compl_setOf
-- Module: Mathlib.Order.Filter.Ultrafilter.Defs
Goal:
α : Type u
f : Filter α
s : Set α
H : ∀ (g : Ultrafilter α), (↑g : Filter α) ≤ f → s ∈ g
hf : s ∉ f
g : Filter (↑sᶜ : Type u) := comap (Subtype.val (p := fun (x : α) ↦ x ∈ sᶜ)) f
⊢ g.NeBot

Tactic:
haveI : NeBot g := comap_neBot_iff_compl_range.2 (by simpa [compl_setOf])
-- Module: Mathlib.Order.Filter.Ultrafilter.Defs
Goal:
α : Type u
f : Filter α
s : Set α
H : ∀ (g : Ultrafilter α), (↑g : Filter α) ≤ f → s ∈ g
hf : s ∉ f
g : Filter (↑sᶜ : Type u) := comap (Subtype.val (p := fun (x : α) ↦ x ∈ sᶜ)) f
this : g.NeBot
⊢ False

Tactic:
simpa using H ((of g).map (↑)) (map_le_iff_le_comap.mpr (of_le g))

Premises used: Iff.mpr, Ultrafilter.of, Filter.map_le_iff_le_comap, Ultrafilter.map
-- Module: Mathlib.Order.Filter.Ultrafilter.Defs
Goal:
α : Type u
f₁ f₂ : Filter α
⊢ f₁ ≤ f₂ ↔ ∀ (g : Ultrafilter α), (↑g : Filter α) ≤ f₁ → (↑g : Filter α) ≤ f₂

Tactic:
⟨fun h _ h₁ => h₁.trans h, fun h _ hs => mem_iff_ultrafilter.2 fun g hg => h g hg hs⟩

Premises used: Iff.mpr, Filter.mem_iff_ultrafilter, Iff.intro, LE.le.trans
-- Module: Mathlib.Order.Filter.Ultrafilter.Defs
Goal:
α : Type u
f f' : Filter α
⊢ ⨆ (g : Ultrafilter α), ⨆ (_ : (↑g : Filter α) ≤ f), (↑g : Filter α) ≤ f' ↔ f ≤ f'

Tactic:
simp only [iSup_le_iff, ← le_iff_ultrafilter]

Premises used: iSup_le_iff, Filter.le_iff_ultrafilter
-- Module: Mathlib.Order.Filter.Ultrafilter.Defs
Goal:
α : Type u
f : Filter α
⊢ (∃ (u : Ultrafilter α), (↑u : Filter α) ≤ f) ↔ f.NeBot

Tactic:
⟨fun ⟨_, uf⟩ => neBot_of_le uf, fun h => @exists_ultrafilter_le _ _ h⟩

Premises used: Filter.NeBot, _private.0.Filter.exists_ultrafilter_iff.match_1, Filter.exists_ultrafilter_le, Iff.intro, Filter.neBot_of_le
-- Module: Mathlib.Order.Filter.Ultrafilter.Defs
Goal:
α : Type u
g : Filter α
p : Filter α → Prop
hp : Monotone p
⊢ (∀ (f : Filter α), f.NeBot → f ≤ g → p f) ↔ ∀ (f : Ultrafilter α), (↑f : Filter α) ≤ g → p (↑f : Filter α)

Tactic:
⟨fun H f hf => H f f.neBot hf, ?_⟩

Premises used: Ultrafilter.neBot, Iff.intro, Ultrafilter.toFilter
-- Module: Mathlib.Order.Filter.Ultrafilter.Defs
Goal:
α : Type u
g : Filter α
p : Filter α → Prop
hp : Monotone p
refine : (∀ (f : Ultrafilter α), (↑f : Filter α) ≤ g → p (↑f : Filter α)) → ∀ (f : Filter α), f.NeBot → f ≤ g → p f
⊢ (∀ (f : Filter α), f.NeBot → f ≤ g → p f) ↔ ∀ (f : Ultrafilter α), (↑f : Filter α) ≤ g → p (↑f : Filter α)

Tactic:
refine ⟨fun H f hf => H f f.neBot hf, ?_⟩
-- Module: Mathlib.Order.Filter.Ultrafilter.Defs
Goal:
α : Type u
g : Filter α
p : Filter α → Prop
hp : Monotone p
H : ∀ (f : Ultrafilter α), (↑f : Filter α) ≤ g → p (↑f : Filter α)
f : Filter α
hf : f.NeBot
hfg : f ≤ g
⊢ p f

Tactic:
hp (of_le f) (H _ ((of_le f).trans hfg))

Premises used: Ultrafilter.of_le, LE.le.trans
-- Module: Mathlib.Order.Filter.Ultrafilter.Defs
Goal:
α : Type u
g : Filter α
p : Filter α → Prop
hp : Monotone p
H : ∀ (f : Ultrafilter α), (↑f : Filter α) ≤ g → p (↑f : Filter α)
f : Filter α
hf : f.NeBot
hfg : f ≤ g
⊢ p f

Tactic:
exact hp (of_le f) (H _ ((of_le f).trans hfg))

Premises used: Ultrafilter.of_le, LE.le.trans
-- Module: Mathlib.Order.Filter.Ultrafilter.Defs
Goal:
α : Type u
β : Type v
m : α → β
s : Set α
g : Ultrafilter β
h : m '' s ∈ g
⊢ (Filter.comap m (↑g : Filter β) ⊓ 𝓟 s).NeBot

Tactic:
Filter.comap_inf_principal_neBot_of_image_mem g.neBot h

Premises used: Ultrafilter.neBot, Filter.comap_inf_principal_neBot_of_image_mem
-- Module: Mathlib.Order.Filter.Ultrafilter.Defs
Goal:
α : Type u
β : Type v
m : α → β
s : Set α
g : Ultrafilter β
h : m '' s ∈ g
f : Filter α := Filter.comap m (↑g : Filter β) ⊓ 𝓟 s
⊢ f.NeBot

Tactic:
haveI : f.NeBot := comap_inf_principal_neBot_of_image_mem h
-- Module: Mathlib.Order.Filter.Ultrafilter.Defs
Goal:
α : Type u
β : Type v
m : α → β
s : Set α
g : Ultrafilter β
h : m '' s ∈ g
f : Filter α := Filter.comap m (↑g : Filter β) ⊓ 𝓟 s
this : f.NeBot
⊢ s ∈ f

Tactic:
have : s ∈ f := mem_inf_of_right (mem_principal_self s)
-- Module: Mathlib.Order.Filter.Ultrafilter.Defs
Goal:
α : Type u
β : Type v
m : α → β
s : Set α
g : Ultrafilter β
h : m '' s ∈ g
f : Filter α := Filter.comap m (↑g : Filter β) ⊓ 𝓟 s
this_1 : f.NeBot
this : s ∈ f
⊢ s ∈ ofComapInfPrincipal (s := s) h

Tactic:
le_def.mp (of_le _) s this

Premises used: Set.Mem, Ultrafilter.of_le, Iff.mp, Filter.le_def
-- Module: Mathlib.Order.Filter.Ultrafilter.Defs
Goal:
α : Type u
β : Type v
m : α → β
s : Set α
g : Ultrafilter β
h : m '' s ∈ g
f : Filter α := Filter.comap m (↑g : Filter β) ⊓ 𝓟 s
this_1 : f.NeBot
this : s ∈ f
⊢ s ∈ ofComapInfPrincipal (s := s) h

Tactic:
exact le_def.mp (of_le _) s this

Premises used: Ultrafilter.of_le, Iff.mp, Filter.le_def
-- Module: Mathlib.Order.Filter.Ultrafilter.Defs
Goal:
α : Type u
β : Type v
m : α → β
s : Set α
g : Ultrafilter β
h : m '' s ∈ g
f : Filter α := Filter.comap m (↑g : Filter β) ⊓ 𝓟 s
this : f.NeBot
h₁ : (↑(map m (ofComapInfPrincipal (s := s) h)) : Filter β) ≤ (↑g : Filter β)
⊢ map m (ofComapInfPrincipal (s := s) h) = g

Tactic:
apply eq_of_le

Premises used: Ultrafilter.eq_of_le
-- Module: Mathlib.Order.Filter.Ultrafilter.Defs
Goal:
α : Type u
β : Type v
m : α → β
s : Set α
g : Ultrafilter β
h : m '' s ∈ g
f : Filter α := Filter.comap m (↑g : Filter β) ⊓ 𝓟 s
this : f.NeBot
⊢ Filter.map m (↑(of f) : Filter α) ≤ Filter.map m f

Tactic:
map_mono (of_le _)

Premises used: Filter.map_mono, Ultrafilter.of_le
-- Module: Mathlib.Order.Filter.Ultrafilter.Defs
Goal:
α : Type u
β : Type v
m : α → β
s : Set α
g : Ultrafilter β
h : m '' s ∈ g
f : Filter α := Filter.comap m (↑g : Filter β) ⊓ 𝓟 s
this : f.NeBot
⊢ Filter.map m f ≤ Filter.map m (Filter.comap m (↑g : Filter β)) ⊓ Filter.map m (𝓟 s)

Tactic:
map_inf_le

Premises used: Set.Mem, setOf, Filter.map_inf_le
-- Module: Mathlib.Order.Filter.Ultrafilter.Defs
Goal:
α : Type u
β : Type v
m : α → β
s : Set α
g : Ultrafilter β
h : m '' s ∈ g
f : Filter α := Filter.comap m (↑g : Filter β) ⊓ 𝓟 s
this : f.NeBot
rw rw₁ :
  Filter.map m (Filter.comap m (↑g : Filter β)) ⊓ 𝓟 (m '' s) =
    Filter.map m (Filter.comap m (↑g : Filter β)) ⊓ 𝓟 (m '' s)
⊢ Filter.map m (Filter.comap m (↑g : Filter β)) ⊓ Filter.map m (𝓟 s) =
    Filter.map m (Filter.comap m (↑g : Filter β)) ⊓ 𝓟 (m '' s)

Tactic:
rw [map_principal]

Premises used: Filter.map_principal
-- Module: Mathlib.Order.Filter.Ultrafilter.Defs
Goal:
α : Type u
β : Type v
m : α → β
s : Set α
g : Ultrafilter β
h : m '' s ∈ g
f : Filter α := Filter.comap m (↑g : Filter β) ⊓ 𝓟 s
this : f.NeBot
⊢ Filter.map m (Filter.comap m (↑g : Filter β)) ⊓ 𝓟 (m '' s) ≤ (↑g : Filter β) ⊓ 𝓟 (m '' s)

Tactic:
inf_le_inf_right _ map_comap_le

Premises used: Set.Mem, inf_le_inf_right, Filter.map_comap_le
-- Module: Mathlib.Order.Filter.Ultrafilter.Defs
Goal:
α : Type u
β : Type v
m : α → β
s : Set α
g : Ultrafilter β
h : m '' s ∈ g
f : Filter α := Filter.comap m (↑g : Filter β) ⊓ 𝓟 s
this : f.NeBot
⊢ (↑g : Filter β) ⊓ 𝓟 (m '' s) = (↑g : Filter β)

Tactic:
inf_of_le_left (le_principal_iff.mpr h)

Premises used: Iff.mpr, Filter.le_principal_iff, inf_of_le_left
-- Module: Mathlib.Order.Filter.Ultrafilter.Defs
Goal:
α : Type u
β : Type v
m : α → β
s : Set α
g : Ultrafilter β
h : m '' s ∈ g
f : Filter α := Filter.comap m (↑g : Filter β) ⊓ 𝓟 s
this : f.NeBot
m₁ :
  Filter.map m (Filter.comap m (↑g : Filter β)) ⊓ Filter.map m (𝓟 s) =
    Filter.map m (Filter.comap m (↑g : Filter β)) ⊓ 𝓟 (m '' s)
⊢ (↑(map m (ofComapInfPrincipal (s := s) h)) : Filter β) ≤ (↑g : Filter β)

Tactic:
calc
    Filter.map m (of f) ≤ Filter.map m f := map_mono (of_le _)
    _ ≤ (Filter.map m <| Filter.comap m g) ⊓ Filter.map m (𝓟 s) := map_inf_le
    _ = (Filter.map m <| Filter.comap m g) ⊓ (𝓟 <| m '' s) := by rw [map_principal]
    _ ≤ ↑g ⊓ (𝓟 <| m '' s) := inf_le_inf_right _ map_comap_le
    _ = ↑g := inf_of_le_left (le_principal_iff.mpr h)

Premises used: Iff.mpr, Filter.map_mono, Filter.le_principal_iff, inf_of_le_left, Filter.map, Ultrafilter.of_le, Filter.map_inf_le, inf_le_inf_right, Ultrafilter.of, Filter.principal, Set.image, Filter.map_comap_le, Ultrafilter.toFilter, Filter.comap
-- Module: Mathlib.Order.Filter.Ultrafilter.Defs
Goal:
X : Type u_2
α : Filter X
hα : α.NeBot
x y : X
hx : α ≤ pure x
hy : α ≤ pure y
⊢ x = y

Tactic:
Filter.pure_injective (hα.le_pure_iff.mp hx ▸ hα.le_pure_iff.mp hy)

Premises used: Filter.pure_injective, Eq.rec, Filter.NeBot.le_pure_iff, Iff.mp
-- Module: Mathlib.Probability.Independence.Integrable
Goal:
Ω : Type u_1
E : Type u_2
F : Type u_3
inst : MeasurableSpace Ω
μ : Measure Ω
inst_1 : NormedAddCommGroup E
inst_2 : MeasurableSpace E
inst_3 : OpensMeasurableSpace E
inst_4 : MeasurableSpace F
f : Ω → E
g : Ω → F
p : ℝ≥0∞
hp : p ≠ 0
hp' : p ≠ ∞
hℒp : MemLp f p μ
h'f : ¬∀ᵐ (ω : Ω) ∂μ, f ω = 0
hindep : f ⟂ᵢ[μ] g
contrapose! :
  ∀
    (h'f :
      ∀ (c : ℝ≥0) (_ : 0 < c), LE.le (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) {ω : Ω | c ≤ ‖f ω‖₊} : ℝ≥0∞) (0 : ℝ≥0∞)),
    ∀ᵐ (ω : Ω) ∂μ, f ω = 0
⊢ ∃ (c : ℝ≥0), 0 < c ∧ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) {ω : Ω | c ≤ ‖f ω‖₊} : ℝ≥0∞)

Tactic:
contrapose! h'f
-- Module: Mathlib.Probability.Independence.Integrable
Goal:
Ω : Type u_1
E : Type u_2
F : Type u_3
inst : MeasurableSpace Ω
μ : Measure Ω
inst_1 : NormedAddCommGroup E
inst_2 : MeasurableSpace E
inst_3 : OpensMeasurableSpace E
inst_4 : MeasurableSpace F
f : Ω → E
g : Ω → F
p : ℝ≥0∞
hp : p ≠ 0
hp' : p ≠ ∞
hℒp : MemLp f p μ
hindep : f ⟂ᵢ[μ] g
h'f : ∀ (c : ℝ≥0) (_ : 0 < c), LE.le (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) {ω : Ω | c ≤ ‖f ω‖₊} : ℝ≥0∞) (0 : ℝ≥0∞)
c : ℝ≥0
hc : 0 < c
⊢ ∀ᵐ (ω : Ω) ∂μ, ‖f ω‖₊ < c

Tactic:
simpa [ae_iff] using h'f c hc

Premises used: MeasureTheory.ae_iff
-- Module: Mathlib.Probability.Independence.Integrable
Goal:
Ω : Type u_1
E : Type u_2
F : Type u_3
inst : MeasurableSpace Ω
μ : Measure Ω
inst_1 : NormedAddCommGroup E
inst_2 : MeasurableSpace E
inst_3 : OpensMeasurableSpace E
inst_4 : MeasurableSpace F
f : Ω → E
g : Ω → F
p : ℝ≥0∞
hp : p ≠ 0
hp' : p ≠ ∞
hℒp : MemLp f p μ
hindep : f ⟂ᵢ[μ] g
h'f : ∀ (c : ℝ≥0) (_ : 0 < c), LE.le (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) {ω : Ω | c ≤ ‖f ω‖₊} : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ∀ (c : ℝ≥0) (hc : 0 < c), ∀ᵐ (ω : Ω) ∂μ, ‖f ω‖₊ < c

Tactic:
have A (c : ℝ≥0) (hc : 0 < c) : ∀ᵐ ω ∂μ, ‖f ω‖₊ < c := by simpa [ae_iff] using h'f c hc
-- Module: Mathlib.Probability.Independence.Integrable
Goal:
Ω : Type u_1
E : Type u_2
F : Type u_3
inst : MeasurableSpace Ω
μ : Measure Ω
inst_1 : NormedAddCommGroup E
inst_2 : MeasurableSpace E
inst_3 : OpensMeasurableSpace E
inst_4 : MeasurableSpace F
f : Ω → E
g : Ω → F
p : ℝ≥0∞
hp : p ≠ 0
hp' : p ≠ ∞
hℒp : MemLp f p μ
hindep : f ⟂ᵢ[μ] g
h'f : ∀ (c : ℝ≥0) (_ : 0 < c), LE.le (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) {ω : Ω | c ≤ ‖f ω‖₊} : ℝ≥0∞) (0 : ℝ≥0∞)
A : ∀ (c : ℝ≥0) (hc : 0 < c), ∀ᵐ (ω : Ω) ∂μ, ‖f ω‖₊ < c
⊢ ∃ (u : ℕ → ℝ≥0), StrictAnti u ∧ (∀ (n : ℕ), 0 < u n) ∧ Tendsto u atTop (𝓝 0)

Tactic:
exists_seq_strictAnti_tendsto (0 : ℝ≥0)

Premises used: exists_seq_strictAnti_tendsto, OfNat.ofNat
-- Module: Mathlib.Probability.Independence.Integrable
Goal:
Ω : Type u_1
E : Type u_2
F : Type u_3
inst : MeasurableSpace Ω
μ : Measure Ω
inst_1 : NormedAddCommGroup E
inst_2 : MeasurableSpace E
inst_3 : OpensMeasurableSpace E
inst_4 : MeasurableSpace F
f : Ω → E
g : Ω → F
p : ℝ≥0∞
hp : p ≠ 0
hp' : p ≠ ∞
hℒp : MemLp f p μ
hindep : f ⟂ᵢ[μ] g
h'f : ∀ (c : ℝ≥0) (_ : 0 < c), LE.le (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) {ω : Ω | c ≤ ‖f ω‖₊} : ℝ≥0∞) (0 : ℝ≥0∞)
A : ∀ (c : ℝ≥0) (hc : 0 < c), ∀ᵐ (ω : Ω) ∂μ, ‖f ω‖₊ < c
obtain : ∀ (u : ℕ → ℝ≥0) (u_pos : ∀ (n : ℕ), 0 < u n) (u_lim : Tendsto u atTop (𝓝 0)), ∀ᵐ (ω : Ω) ∂μ, f ω = 0
⊢ ∀ᵐ (ω : Ω) ∂μ, f ω = 0

Tactic:
obtain ⟨u, -, u_pos, u_lim⟩ : ∃ u, StrictAnti u ∧ (∀ (n : ℕ), 0 < u n)
      ∧ Tendsto u atTop (𝓝 0) := exists_seq_strictAnti_tendsto (0 : ℝ≥0)

Premises used: exists_seq_strictAnti_tendsto, OfNat.ofNat
-- Module: Mathlib.Probability.Independence.Integrable
Goal:
Ω : Type u_1
E : Type u_2
F : Type u_3
inst : MeasurableSpace Ω
μ : Measure Ω
inst_1 : NormedAddCommGroup E
inst_2 : MeasurableSpace E
inst_3 : OpensMeasurableSpace E
inst_4 : MeasurableSpace F
f : Ω → E
g : Ω → F
p : ℝ≥0∞
hp : p ≠ 0
hp' : p ≠ ∞
hℒp : MemLp f p μ
hindep : f ⟂ᵢ[μ] g
h'f : ∀ (c : ℝ≥0) (_ : 0 < c), LE.le (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) {ω : Ω | c ≤ ‖f ω‖₊} : ℝ≥0∞) (0 : ℝ≥0∞)
A : ∀ (c : ℝ≥0) (hc : 0 < c), ∀ᵐ (ω : Ω) ∂μ, ‖f ω‖₊ < c
u : ℕ → ℝ≥0
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
h : ∀ (ω : Ω) (hω : ∀ (i : ℕ), ‖f ω‖₊ < u i), f ω = 0
⊢ ∀ᵐ (ω : Ω) ∂μ, f ω = 0

Tactic:
filter_upwards [ae_all_iff.2 (fun n ↦ A (u n) (u_pos n))] with ω hω

Premises used: Iff.mpr, MeasureTheory.ae_all_iff
-- Module: Mathlib.Probability.Independence.Integrable
Goal:
Ω : Type u_1
E : Type u_2
F : Type u_3
inst : MeasurableSpace Ω
μ : Measure Ω
inst_1 : NormedAddCommGroup E
inst_2 : MeasurableSpace E
inst_3 : OpensMeasurableSpace E
inst_4 : MeasurableSpace F
f : Ω → E
g : Ω → F
p : ℝ≥0∞
hp : p ≠ 0
hp' : p ≠ ∞
hℒp : MemLp f p μ
hindep : f ⟂ᵢ[μ] g
h'f : ∀ (c : ℝ≥0) (_ : 0 < c), LE.le (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) {ω : Ω | c ≤ ‖f ω‖₊} : ℝ≥0∞) (0 : ℝ≥0∞)
A : ∀ (c : ℝ≥0) (hc : 0 < c), ∀ᵐ (ω : Ω) ∂μ, ‖f ω‖₊ < c
u : ℕ → ℝ≥0
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
ω : Ω
hω : ∀ (i : ℕ), ‖f ω‖₊ < u i
⊢ f ω = 0

Tactic:
simpa using ge_of_tendsto' u_lim (fun i ↦ (hω i).le)

Premises used: LT.lt.le, ge_of_tendsto'
-- Module: Mathlib.Probability.Independence.Integrable
Goal:
Ω : Type u_1
E : Type u_2
F : Type u_3
inst : MeasurableSpace Ω
μ : Measure Ω
inst_1 : NormedAddCommGroup E
inst_2 : MeasurableSpace E
inst_3 : OpensMeasurableSpace E
inst_4 : MeasurableSpace F
f : Ω → E
g : Ω → F
p : ℝ≥0∞
hp : p ≠ 0
hp' : p ≠ ∞
hℒp : MemLp f p μ
h'f : ¬∀ᵐ (ω : Ω) ∂μ, f ω = 0
hindep : f ⟂ᵢ[μ] g
obtain :
  ∀ (c : ℝ≥0) (c_pos : 0 < c)
    (hc : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) {ω : Ω | c ≤ ‖f ω‖₊} : ℝ≥0∞)), IsProbabilityMeasure μ
⊢ IsProbabilityMeasure μ

Tactic:
obtain ⟨c, c_pos, hc⟩ : ∃ (c : ℝ≥0), 0 < c ∧ 0 < μ {ω | c ≤ ‖f ω‖₊} := by
    contrapose! h'f
    have A (c : ℝ≥0) (hc : 0 < c) : ∀ᵐ ω ∂μ, ‖f ω‖₊ < c := by simpa [ae_iff] using h'f c hc
    obtain ⟨u, -, u_pos, u_lim⟩ : ∃ u, StrictAnti u ∧ (∀ (n : ℕ), 0 < u n)
      ∧ Tendsto u atTop (𝓝 0) := exists_seq_strictAnti_tendsto (0 : ℝ≥0)
    filter_upwards [ae_all_iff.2 (fun n ↦ A (u n) (u_pos n))] with ω hω
    simpa using ge_of_tendsto' u_lim (fun i ↦ (hω i).le)