awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Basic
Goal:
X : Type u
α : Type u_1
s : Set X
inst : TopologicalSpace X
f : α → Set X
ho : ∀ (i : α), IsOpen[inst] (f i)
hU : Eq.{u + 1} (α := Set X) (⋃ (i : α), f i) univ
refine : ∀ (h : ∀ (i : α), IsOpen[inst] (f i ∩ s)), IsOpen[inst] s
⊢ IsOpen[inst] s ↔ ∀ (i : α), IsOpen[inst] (f i ∩ s)

Tactic:
refine ⟨fun h i ↦ (ho i).inter h, fun h ↦ ?_⟩
-- Module: Mathlib.Topology.Basic
Goal:
X : Type u
α : Type u_1
s : Set X
inst : TopologicalSpace X
f : α → Set X
ho : ∀ (i : α), IsOpen[inst] (f i)
hU : Eq.{u + 1} (α := Set X) (⋃ (i : α), f i) univ
h : ∀ (i : α), IsOpen[inst] (f i ∩ s)
rw : IsOpen[inst] (⋃ (i : α), f i ∩ s)
⊢ IsOpen[inst] s

Tactic:
rw [← s.inter_univ, inter_comm, ← hU, iUnion_inter]

Premises used: Set.inter_univ, Set.iUnion_inter, Set.inter_comm
-- Module: Mathlib.Topology.Basic
Goal:
X : Type u
α : Type u_1
s : Set X
inst : TopologicalSpace X
f : α → Set X
ho : ∀ (i : α), IsOpen[inst] (f i)
hU : Eq.{u + 1} (α := Set X) (⋃ (i : α), f i) univ
h : ∀ (i : α), IsOpen[inst] (f i ∩ s)
⊢ IsOpen[inst] (⋃ (i : α), f i ∩ s)

Tactic:
isOpen_iUnion fun i ↦ h i

Premises used: isOpen_iUnion
-- Module: Mathlib.Topology.Basic
Goal:
X : Type u
α : Type u_1
s : Set X
inst : TopologicalSpace X
f : α → Set X
ho : ∀ (i : α), IsOpen[inst] (f i)
hU : Eq.{u + 1} (α := Set X) (⋃ (i : α), f i) univ
h : ∀ (i : α), IsOpen[inst] (f i ∩ s)
⊢ IsOpen[inst] (⋃ (i : α), f i ∩ s)

Tactic:
exact isOpen_iUnion fun i ↦ h i

Premises used: isOpen_iUnion
-- Module: Mathlib.Topology.Basic
Goal:
X : Type u
inst : TopologicalSpace X
rw : IsOpen[inst] (⋃₀ ∅)
⊢ IsOpen[inst] ∅

Tactic:
rw [← sUnion_empty]

Premises used: Set.sUnion_empty
-- Module: Mathlib.Topology.Basic
Goal:
X : Type u
inst : TopologicalSpace X
⊢ IsOpen[inst] (⋃₀ ∅)

Tactic:
isOpen_sUnion fun a => False.elim

Premises used: False.elim, isOpen_sUnion
-- Module: Mathlib.Topology.Basic
Goal:
X : Type u
inst : TopologicalSpace X
⊢ IsOpen[inst] (⋃₀ ∅)

Tactic:
exact isOpen_sUnion fun a => False.elim

Premises used: False.elim, isOpen_sUnion
-- Module: Mathlib.Topology.Basic
Goal:
X : Type u
inst : TopologicalSpace X
s : Set (Set X)
h : ∀ (t : Set X), Membership.mem (γ := Set (Set X)) ∅ t → IsOpen[inst] t
empty : IsOpen[inst] univ
⊢ IsOpen[inst] (⋂₀ ∅)

Tactic:
rw [sInter_empty]

Premises used: Set.sInter_empty
-- Module: Mathlib.Topology.Basic
Goal:
X : Type u
inst : TopologicalSpace X
s : Set (Set X)
h : ∀ (t : Set X), Membership.mem (γ := Set (Set X)) ∅ t → IsOpen[inst] t
⊢ IsOpen[inst] univ

Tactic:
isOpen_univ

Premises used: isOpen_univ
-- Module: Mathlib.Topology.Basic
Goal:
X : Type u
inst : TopologicalSpace X
s : Set (Set X)
h : ∀ (t : Set X), Membership.mem (γ := Set (Set X)) ∅ t → IsOpen[inst] t
⊢ IsOpen[inst] univ

Tactic:
exact isOpen_univ

Premises used: isOpen_univ
-- Module: Mathlib.Topology.Basic
Goal:
X : Type u
inst : TopologicalSpace X
s : Set (Set X)
a : Set X
s_1 : Set (Set X)
h_1 : a ∉ s_1
hs : s_1.Finite
ih : ∀ (h : ∀ t ∈ s_1, IsOpen[inst] t), IsOpen[inst] (⋂₀ s_1)
h : ∀ t ∈ Insert.insert a s_1, IsOpen[inst] t
insert : ∀ (h : IsOpen[inst] a ∧ ∀ x ∈ s_1, IsOpen[inst] x), IsOpen[inst] (a ∩ ⋂₀ s_1)
⊢ IsOpen[inst] (⋂₀ Insert.insert a s_1)

Tactic:
simp only [sInter_insert, forall_mem_insert] at h ⊢

Premises used: Set.forall_mem_insert, Set.sInter_insert
-- Module: Mathlib.Topology.Basic
Goal:
X : Type u
inst : TopologicalSpace X
s : Set (Set X)
a : Set X
s_1 : Set (Set X)
h_1 : a ∉ s_1
hs : s_1.Finite
ih : ∀ (h : ∀ t ∈ s_1, IsOpen[inst] t), IsOpen[inst] (⋂₀ s_1)
h : IsOpen[inst] a ∧ ∀ x ∈ s_1, IsOpen[inst] x
⊢ IsOpen[inst] (a ∩ ⋂₀ s_1)

Tactic:
h.1.inter (ih h.2)

Premises used: And.right, And.left, IsOpen.inter
-- Module: Mathlib.Topology.Basic
Goal:
X : Type u
inst : TopologicalSpace X
s : Set (Set X)
a : Set X
s_1 : Set (Set X)
h_1 : a ∉ s_1
hs : s_1.Finite
ih : ∀ (h : ∀ t ∈ s_1, IsOpen[inst] t), IsOpen[inst] (⋂₀ s_1)
h : IsOpen[inst] a ∧ ∀ x ∈ s_1, IsOpen[inst] x
⊢ IsOpen[inst] (a ∩ ⋂₀ s_1)

Tactic:
exact h.1.inter (ih h.2)

Premises used: And.right, And.left, IsOpen.inter
-- Module: Mathlib.Topology.Basic
Goal:
X : Type u
inst : TopologicalSpace X
s : Set (Set X)
hs : s.Finite
h : ∀ t ∈ s, IsOpen[inst] t
empty : ∀ (h : ∀ (t : Set X), Membership.mem (γ := Set (Set X)) ∅ t → IsOpen[inst] t), IsOpen[inst] (⋂₀ ∅)
insert :
  ∀ {a : Set X} {s : Set (Set X)},
    a ∉ s →
      s.Finite →
        ∀ (ih : ∀ (h : ∀ t ∈ s, IsOpen[inst] t), IsOpen[inst] (⋂₀ s)) (h : ∀ t ∈ Insert.insert a s, IsOpen[inst] t),
          IsOpen[inst] (⋂₀ Insert.insert a s)
⊢ IsOpen[inst] (⋂₀ s)

Tactic:
induction s, hs using Set.Finite.induction_on with
  | empty => rw [sInter_empty]; exact isOpen_univ
  | insert _ _ ih =>
    simp only [sInter_insert, forall_mem_insert] at h ⊢
    exact h.1.inter (ih h.2)

Premises used: Set.forall_mem_insert, Set.sInter_empty, Set.sInter_insert, Insert.insert, isOpen_univ
-- Module: Mathlib.Topology.Basic
Goal:
X : Type u
α : Type u_1
inst : TopologicalSpace X
s : Set α
f : α → Set X
hs : s.Finite
h : ∀ i ∈ s, IsOpen[inst] (f i)
⊢ IsOpen[inst] (⋂ i ∈ s, f i)

Tactic:
sInter_image f s ▸ (hs.image _).isOpen_sInter (forall_mem_image.2 h)

Premises used: Iff.mpr, Eq.rec, Set.Finite.image, Set.sInter_image, Set.Finite.isOpen_sInter, Set.forall_mem_image
-- Module: Mathlib.Topology.Basic
Goal:
X : Type u
ι : Sort v
inst : TopologicalSpace X
inst_1 : Finite ι
s : ι → Set X
h : ∀ (i : ι), IsOpen[inst] (s i)
⊢ IsOpen[inst] (⋂ (i : ι), s i)

Tactic:
(finite_range _).isOpen_sInter (forall_mem_range.2 h)

Premises used: Iff.mpr, iInf, Set.forall_mem_range, Set.iInter, Set.finite_range, Set.Finite.isOpen_sInter
-- Module: Mathlib.Topology.Basic
Goal:
X : Type u
α : Type u_1
inst : TopologicalSpace X
s : Finset α
f : α → Set X
h : ∀ i ∈ s, IsOpen[inst] (f i)
⊢ IsOpen[inst] (⋂ i ∈ s, f i)

Tactic:
s.finite_toSet.isOpen_biInter h

Premises used: Finset.finite_toSet, Set.Finite.isOpen_biInter
-- Module: Mathlib.Topology.Basic
Goal:
X : Type u
inst : TopologicalSpace X
p : Prop
pos : p → IsOpen[inst] {_x : X | p}
neg : ¬p → IsOpen[inst] {_x : X | p}
⊢ IsOpen[inst] {_x : X | p}

Tactic:
by_cases p
-- Module: Mathlib.Topology.Basic
Goal:
X : Type u
inst : TopologicalSpace X
p : Prop
h : p
⊢ IsOpen[inst] {_x : X | p}

Tactic:
simp [*]
-- Module: Mathlib.Topology.Basic
Goal:
X : Type u
inst : TopologicalSpace X
p : Prop
h : ¬p
⊢ IsOpen[inst] {_x : X | p}

Tactic:
simp [*]
-- Module: Mathlib.Topology.Basic
Goal:
X : Type u
p₁ p₂ : X → Prop
inst : TopologicalSpace X
⊢ IsOpen[inst] {x : X | p₁ x} → IsOpen[inst] {x : X | p₂ x} → IsOpen[inst] {x : X | p₁ x ∧ p₂ x}

Tactic:
IsOpen.inter

Premises used: Set.Mem, setOf, Set.inter, IsOpen.inter
-- Module: Mathlib.Topology.Basic
Goal:
X : Type u
s : Set X
inst : TopologicalSpace X
⊢ IsOpen[inst] sᶜ ↔ IsClosed[inst] s

Tactic:
⟨fun h => ⟨h⟩, fun h => h.isOpen_compl⟩

Premises used: IsClosed.isOpen_compl, Iff.intro, IsClosed.mk
-- Module: Mathlib.Topology.Basic
Goal:
X : Type u_2
t₁ t₂ : TopologicalSpace X
rw : (∀ (x : Set X), IsOpen[t₁] xᶜ ↔ IsOpen[t₂] xᶜ) ↔ ∀ (s : Set X), IsClosed[t₁] s ↔ IsClosed[t₂] s
⊢ t₁ = t₂ ↔ ∀ (s : Set X), IsClosed[t₁] s ↔ IsClosed[t₂] s

Tactic:
rw [TopologicalSpace.ext_iff, compl_surjective.forall]

Premises used: Function.Surjective.forall, TopologicalSpace.ext_iff, compl_surjective
-- Module: Mathlib.Topology.Basic
Goal:
X : Type u_2
t₁ t₂ : TopologicalSpace X
⊢ (∀ (x : Set X), IsOpen[t₁] xᶜ ↔ IsOpen[t₂] xᶜ) ↔ ∀ (s : Set X), IsClosed[t₁] s ↔ IsClosed[t₂] s

Tactic:
simp only [@isOpen_compl_iff _ _ t₁, @isOpen_compl_iff _ _ t₂]

Premises used: isOpen_compl_iff
-- Module: Mathlib.Topology.Basic
Goal:
X : Type u
inst : TopologicalSpace X
p : Prop
⊢ IsClosed[inst] {_x : X | p}

Tactic:
⟨isOpen_const (p := ¬p)⟩

Premises used: isOpen_const, IsClosed.mk
-- Module: Mathlib.Topology.Basic
Goal:
X : Type u
inst : TopologicalSpace X
⊢ IsClosed[inst] ∅

Tactic:
isClosed_const

Premises used: setOf, isClosed_const
-- Module: Mathlib.Topology.Basic
Goal:
X : Type u
inst : TopologicalSpace X
⊢ IsClosed[inst] univ

Tactic:
isClosed_const

Premises used: Set.univ, isClosed_const
-- Module: Mathlib.Topology.Basic
Goal:
X : Type u
s : Set X
inst : TopologicalSpace X
hs : IsOpen[inst] s
⊢ IsLocallyClosed s

Tactic:
⟨_, _, hs, isClosed_univ, (inter_univ _).symm⟩

Premises used: isClosed_univ, Set.inter_univ, IsLocallyClosed, And.intro, Exists.intro, Eq.symm
-- Module: Mathlib.Topology.Basic
Goal:
X : Type u
s : Set X
inst : TopologicalSpace X
hs : IsClosed[inst] s
⊢ IsLocallyClosed s

Tactic:
⟨_, _, isOpen_univ, hs, (univ_inter _).symm⟩

Premises used: Set.univ_inter, IsLocallyClosed, isOpen_univ, And.intro, Exists.intro, Eq.symm
-- Module: Mathlib.Topology.Basic
Goal:
X : Type u
s₁ s₂ : Set X
inst : TopologicalSpace X
⊢ IsClosed[inst] s₁ → IsClosed[inst] s₂ → IsClosed[inst] (s₁ ∪ s₂)

Tactic:
simpa only [← isOpen_compl_iff, compl_union] using IsOpen.inter

Premises used: Set.compl_union, IsOpen.inter, isOpen_compl_iff
-- Module: Mathlib.Topology.Basic
Goal:
X : Type u
inst : TopologicalSpace X
s : Set (Set X)
⊢ (∀ t ∈ s, IsClosed[inst] t) → IsClosed[inst] (⋂₀ s)

Tactic:
simpa only [← isOpen_compl_iff, compl_sInter, sUnion_image] using isOpen_biUnion

Premises used: Set.compl_sInter, Set.sUnion_image, isOpen_biUnion, isOpen_compl_iff
-- Module: Mathlib.Topology.Basic
Goal:
X : Type u
ι : Sort v
inst : TopologicalSpace X
f : ι → Set X
h : ∀ (i : ι), IsClosed[inst] (f i)
⊢ IsClosed[inst] (⋂ (i : ι), f i)

Tactic:
isClosed_sInter <| forall_mem_range.2 h

Premises used: Iff.mpr, iInf, Set.forall_mem_range, Set.iInter, isClosed_sInter
-- Module: Mathlib.Topology.Basic
Goal:
X : Type u
α : Type u_1
inst : TopologicalSpace X
s : Set α
f : α → Set X
h : ∀ i ∈ s, IsClosed[inst] (f i)
⊢ IsClosed[inst] (⋂ i ∈ s, f i)

Tactic:
isClosed_iInter fun i => isClosed_iInter <| h i

Premises used: isClosed_iInter
-- Module: Mathlib.Topology.Basic
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
rw : IsOpen[inst] sᶜᶜ ↔ IsOpen[inst] s
rw₁ rw₂ : IsOpen[inst] s ↔ IsOpen[inst] s
⊢ IsClosed[inst] sᶜ ↔ IsOpen[inst] s

Tactic:
rw [← isOpen_compl_iff, compl_compl]

Premises used: compl_compl, isOpen_compl_iff
-- Module: Mathlib.Topology.Basic
Goal:
X : Type u
s t : Set X
inst : TopologicalSpace X
h₁ : IsOpen[inst] s
h₂ : IsClosed[inst] t
⊢ IsOpen[inst] (s \ t)

Tactic:
IsOpen.inter h₁ h₂.isOpen_compl

Premises used: IsClosed.isOpen_compl, Set.Mem, Set.diff, setOf, IsOpen.inter, Not
-- Module: Mathlib.Topology.Basic
Goal:
X : Type u
s₁ s₂ : Set X
inst : TopologicalSpace X
h₁ : IsClosed[inst] s₁
h₂ : IsClosed[inst] s₂
rw : ∀ (h₁ : IsOpen[inst] s₁ᶜ) (h₂ : IsOpen[inst] s₂ᶜ), IsOpen[inst] (s₁ ∩ s₂)ᶜ
⊢ IsClosed[inst] (s₁ ∩ s₂)

Tactic:
rw [← isOpen_compl_iff] at *

Premises used: isOpen_compl_iff
-- Module: Mathlib.Topology.Basic
Goal:
X : Type u
s₁ s₂ : Set X
inst : TopologicalSpace X
h₁ : IsOpen[inst] s₁ᶜ
h₂ : IsOpen[inst] s₂ᶜ
rw : IsOpen[inst] (s₁ᶜ ∪ s₂ᶜ)
⊢ IsOpen[inst] (s₁ ∩ s₂)ᶜ

Tactic:
rw [compl_inter]

Premises used: Set.compl_inter
-- Module: Mathlib.Topology.Basic
Goal:
X : Type u
s₁ s₂ : Set X
inst : TopologicalSpace X
h₁ : IsOpen[inst] s₁ᶜ
h₂ : IsOpen[inst] s₂ᶜ
⊢ IsOpen[inst] (s₁ᶜ ∪ s₂ᶜ)

Tactic:
IsOpen.union h₁ h₂

Premises used: IsOpen.union
-- Module: Mathlib.Topology.Basic
Goal:
X : Type u
s₁ s₂ : Set X
inst : TopologicalSpace X
h₁ : IsOpen[inst] s₁ᶜ
h₂ : IsOpen[inst] s₂ᶜ
⊢ IsOpen[inst] (s₁ᶜ ∪ s₂ᶜ)

Tactic:
exact IsOpen.union h₁ h₂

Premises used: IsOpen.union
-- Module: Mathlib.Topology.Basic
Goal:
X : Type u
s t : Set X
inst : TopologicalSpace X
h₁ : IsClosed[inst] s
h₂ : IsOpen[inst] t
⊢ IsClosed[inst] (s \ t)

Tactic:
IsClosed.inter h₁ (isClosed_compl_iff.mpr h₂)

Premises used: Iff.mpr, Set.Mem, Set.diff, setOf, IsClosed.inter, Not, isClosed_compl_iff
-- Module: Mathlib.Topology.Basic
Goal:
X : Type u
α : Type u_1
inst : TopologicalSpace X
s : Set α
f : α → Set X
hs : s.Finite
h : ∀ i ∈ s, IsClosed[inst] (f i)
simp : ∀ (h : ∀ i ∈ s, IsOpen[inst] (f i)ᶜ), IsOpen[inst] (⋂ i ∈ s, (f i)ᶜ)
⊢ IsClosed[inst] (⋃ i ∈ s, f i)

Tactic:
simp only [← isOpen_compl_iff, compl_iUnion] at *

Premises used: Set.compl_iUnion, isOpen_compl_iff
-- Module: Mathlib.Topology.Basic
Goal:
X : Type u
α : Type u_1
inst : TopologicalSpace X
s : Set α
f : α → Set X
hs : s.Finite
h : ∀ i ∈ s, IsOpen[inst] (f i)ᶜ
⊢ IsOpen[inst] (⋂ i ∈ s, (f i)ᶜ)

Tactic:
hs.isOpen_biInter h

Premises used: Set.Finite.isOpen_biInter
-- Module: Mathlib.Topology.Basic
Goal:
X : Type u
α : Type u_1
inst : TopologicalSpace X
s : Set α
f : α → Set X
hs : s.Finite
h : ∀ i ∈ s, IsOpen[inst] (f i)ᶜ
⊢ IsOpen[inst] (⋂ i ∈ s, (f i)ᶜ)

Tactic:
exact hs.isOpen_biInter h

Premises used: Set.Finite.isOpen_biInter
-- Module: Mathlib.Topology.Basic
Goal:
X : Type u
α : Type u_1
inst : TopologicalSpace X
s : Finset α
f : α → Set X
h : ∀ i ∈ s, IsClosed[inst] (f i)
⊢ IsClosed[inst] (⋃ i ∈ s, f i)

Tactic:
s.finite_toSet.isClosed_biUnion h

Premises used: Finset.finite_toSet, Set.Finite.isClosed_biUnion
-- Module: Mathlib.Topology.Basic
Goal:
X : Type u
ι : Sort v
inst : TopologicalSpace X
inst_1 : Finite ι
s : ι → Set X
h : ∀ (i : ι), IsClosed[inst] (s i)
simp : ∀ (h : ∀ (i : ι), IsOpen[inst] (s i)ᶜ), IsOpen[inst] (⋂ (i : ι), (s i)ᶜ)
⊢ IsClosed[inst] (⋃ (i : ι), s i)

Tactic:
simp only [← isOpen_compl_iff, compl_iUnion] at *

Premises used: Set.compl_iUnion, isOpen_compl_iff
-- Module: Mathlib.Topology.Basic
Goal:
X : Type u
ι : Sort v
inst : TopologicalSpace X
inst_1 : Finite ι
s : ι → Set X
h : ∀ (i : ι), IsOpen[inst] (s i)ᶜ
⊢ IsOpen[inst] (⋂ (i : ι), (s i)ᶜ)

Tactic:
isOpen_iInter_of_finite h

Premises used: isOpen_iInter_of_finite
-- Module: Mathlib.Topology.Basic
Goal:
X : Type u
ι : Sort v
inst : TopologicalSpace X
inst_1 : Finite ι
s : ι → Set X
h : ∀ (i : ι), IsOpen[inst] (s i)ᶜ
⊢ IsOpen[inst] (⋂ (i : ι), (s i)ᶜ)

Tactic:
exact isOpen_iInter_of_finite h

Premises used: isOpen_iInter_of_finite
-- Module: Mathlib.Topology.Basic
Goal:
X : Type u
inst : TopologicalSpace X
p q : X → Prop
hp : IsOpen[inst] {x : X | p x}
hq : IsClosed[inst] {x : X | q x}
⊢ IsClosed[inst] {x : X | p x → q x}

Tactic:
simpa only [imp_iff_not_or] using hp.isClosed_compl.union hq

Premises used: IsClosed.union, imp_iff_not_or, IsOpen.isClosed_compl
-- Module: Mathlib.Topology.Basic
Goal:
X : Type u
p : X → Prop
inst : TopologicalSpace X
⊢ IsClosed[inst] {a : X | p a} → IsOpen[inst] {a : X | ¬p a}

Tactic:
isOpen_compl_iff.mpr

Premises used: Iff.mpr, Set.Mem, setOf, isOpen_compl_iff
-- Module: Mathlib.Topology.Basic
Goal:
X : Type u
p₁ p₂ : X → Prop
inst : TopologicalSpace X
⊢ IsClosed[inst] {x : X | p₁ x} → IsClosed[inst] {x : X | p₂ x} → IsClosed[inst] {x : X | p₁ x ∧ p₂ x}

Tactic:
IsClosed.inter

Premises used: Set.Mem, setOf, Set.inter, IsClosed.inter
-- Module: Mathlib.Topology.Basic
Goal:
X : Type u
inst : TopologicalSpace X
f : Filter X
h : ∃ (x : X), f ≤ 𝓝 x
⊢ f ≤ 𝓝 f.lim

Tactic:
Classical.epsilon_spec h

Premises used: Set.Mem, Filter.lim, Classical.epsilon_spec
-- Module: Mathlib.Topology.Basic
Goal:
X : Type u
α : Type u_1
inst : TopologicalSpace X
f : Filter α
g : α → X
h : ∃ (x : X), Tendsto g f (𝓝 x)
⊢ Tendsto g f (𝓝 (f.limUnder g))

Tactic:
le_nhds_lim h

Premises used: Set.Mem, le_nhds_lim, Filter.Tendsto, Filter.limUnder
-- Module: Mathlib.Topology.Basic
Goal:
X : Type u
α : Type u_1
inst : TopologicalSpace X
hX : Nonempty X
f : Filter α
g : α → X
h : ¬∃ (x : X), map g f ≤ 𝓝 x
simp_rw : (map g f).lim = Classical.choice hX
simp_rw₁ : (Classical.epsilon fun (x : X) ↦ map g f ≤ 𝓝 x) = Classical.choice hX
simp_rw₂ : (↑(Classical.strongIndefiniteDescription (fun (x : X) ↦ map g f ≤ 𝓝 x) hX) : X) = Classical.choice hX
simp_rw₃ :
  (↑(if hp : ∃ (x : X), map g f ≤ 𝓝 x then
          Subtype.mk (p := fun (x : X) ↦ (∃ (y : X), map g f ≤ 𝓝 y) → map g f ≤ 𝓝 x)
            (↑(Classical.indefiniteDescription (fun (x : X) ↦ map g f ≤ 𝓝 x) hp) : X) ⋯
        else Subtype.mk (p := fun (x : X) ↦ (∃ (y : X), map g f ≤ 𝓝 y) → map g f ≤ 𝓝 x) (Classical.choice hX) ⋯) :
      X) =
    Classical.choice hX
⊢ f.limUnder g = Classical.choice hX

Tactic:
simp_rw [limUnder, lim, Classical.epsilon, Classical.strongIndefiniteDescription, dif_neg h]

Premises used: Classical.epsilon, Classical.strongIndefiniteDescription, dif_neg, Filter.lim, Filter.limUnder
-- Module: Mathlib.Topology.Bornology.Absorbs
Goal:
M : Type u_1
α : Type u_2
inst : Bornology M
inst_1 : SMul M α
s : Set α
⊢ Absorbs M s ∅

Tactic:
simp [Absorbs]

Premises used: Absorbs
-- Module: Mathlib.Topology.Bornology.Absorbs
Goal:
M : Type u_1
α : Type u_2
inst : Bornology M
inst_1 : SMul M α
s t : Set α
h : Absorbs M s t
⊢ ∀ᶠ (a : M) in cobounded M, t ⊆ a • s

Tactic:
h

Premises used: Absorbs
-- Module: Mathlib.Topology.Bornology.Absorbs
Goal:
M : Type u_1
α : Type u_2
inst : Bornology M
inst_1 : SMul M α
s t : Set α
inst_2 : BoundedSpace M
⊢ Absorbs M s t

Tactic:
simp [Absorbs]

Premises used: Absorbs
-- Module: Mathlib.Topology.Bornology.Absorbs
Goal:
M : Type u_1
α : Type u_2
inst : Bornology M
inst_1 : SMul M α
s₁ s₂ t : Set α
h : Absorbs M s₁ t
hs : s₁ ⊆ s₂
⊢ Absorbs M s₂ t

Tactic:
h.mono fun _a ha ↦ ha.trans <| smul_set_mono hs

Premises used: HasSubset.Subset.trans, Set.smul_set_mono, Filter.Eventually.mono, Absorbs
-- Module: Mathlib.Topology.Bornology.Absorbs
Goal:
M : Type u_1
α : Type u_2
inst : Bornology M
inst_1 : SMul M α
s t₁ t₂ : Set α
h : Absorbs M s t₁
ht : t₂ ⊆ t₁
⊢ Absorbs M s t₂

Tactic:
h.mono fun _ ↦ ht.trans

Premises used: HasSubset.Subset.trans, Filter.Eventually.mono, Absorbs
-- Module: Mathlib.Topology.Bornology.Absorbs
Goal:
M : Type u_1
α : Type u_2
inst : Bornology M
inst_1 : SMul M α
s₁ s₂ t₁ t₂ : Set α
h : Absorbs M s₁ t₁
hs : s₁ ⊆ s₂
ht : t₂ ⊆ t₁
⊢ Absorbs M s₂ t₂

Tactic:
(h.mono_left hs).mono_right ht

Premises used: Absorbs.mono_left, Absorbs.mono_right
-- Module: Mathlib.Topology.Bornology.Absorbs
Goal:
M : Type u_1
α : Type u_2
inst : Bornology M
inst_1 : SMul M α
s t₁ t₂ : Set α
⊢ Absorbs M s (t₁ ∪ t₂) ↔ Absorbs M s t₁ ∧ Absorbs M s t₂

Tactic:
simp [Absorbs]

Premises used: Absorbs
-- Module: Mathlib.Topology.Bornology.Absorbs
Goal:
M : Type u_1
α : Type u_2
inst : Bornology M
inst_1 : SMul M α
s t₁ t₂ : Set α
h₁ : Absorbs M s t₁
h₂ : Absorbs M s t₂
⊢ Absorbs M s (t₁ ∪ t₂)

Tactic:
absorbs_union.2 ⟨h₁, h₂⟩

Premises used: Iff.mpr, absorbs_union, And.intro
-- Module: Mathlib.Topology.Bornology.Absorbs
Goal:
M : Type u_1
α : Type u_2
inst : Bornology M
inst_1 : SMul M α
s : Set α
T : Set (Set α)
hT : T.Finite
⊢ Absorbs M s (⋃₀ T) ↔ ∀ t ∈ T, Absorbs M s t

Tactic:
simp [Absorbs, hT]

Premises used: Absorbs
-- Module: Mathlib.Topology.Bornology.Absorbs
Goal:
M : Type u_1
α : Type u_2
inst : Bornology M
inst_1 : SMul M α
s : Set α
T : Set (Set α)
hT : T.Finite
hs : ∀ t ∈ T, Absorbs M s t
⊢ Absorbs M s (⋃₀ T)

Tactic:
hT.absorbs_sUnion.2 hs

Premises used: Iff.mpr, Set.Finite.absorbs_sUnion
-- Module: Mathlib.Topology.Bornology.Absorbs
Goal:
M : Type u_1
α : Type u_2
inst : Bornology M
inst_1 : SMul M α
s : Set α
ι : Sort u_3
inst_2 : Finite ι
t : ι → Set α
⊢ Absorbs M s (⋃ (i : ι), t i) ↔ ∀ (i : ι), Absorbs M s (t i)

Tactic:
(finite_range t).absorbs_sUnion.trans forall_mem_range

Premises used: Set.forall_mem_range, Set.Mem, iSup, setOf, Set.finite_range, Iff.trans, Set.iUnion, Set.Finite.absorbs_sUnion
-- Module: Mathlib.Topology.Bornology.Absorbs
Goal:
M : Type u_1
α : Type u_2
inst : Bornology M
inst_1 : SMul M α
s : Set α
ι : Type u_3
t : ι → Set α
I : Set ι
hI : I.Finite
⊢ Absorbs M s (⋃ i ∈ I, t i) ↔ ∀ i ∈ I, Absorbs M s (t i)

Tactic:
simp [Absorbs, hI]

Premises used: Absorbs
-- Module: Mathlib.Topology.Bornology.Absorbs
Goal:
M : Type u_1
α : Type u_2
inst : Bornology M
inst_1 : SMul M α
s : Set α
ι : Type u_3
t : ι → Set α
I : Finset ι
⊢ Absorbs M s (⋃ i ∈ I, t i) ↔ ∀ i ∈ I, Absorbs M s (t i)

Tactic:
I.finite_toSet.absorbs_biUnion

Premises used: Set.Finite.absorbs_biUnion, Finset.finite_toSet
-- Module: Mathlib.Topology.Bornology.Absorbs
Goal:
M : Type u_1
E : Type u_2
inst : Bornology M
s₁ s₂ t₁ t₂ : Set E
inst_1 : AddZeroClass E
inst_2 : DistribSMul M E
h₁ : Absorbs M s₁ t₁
h₂ : Absorbs M s₂ t₂
x : M
hx₁ : t₁ ⊆ x • s₁
hx₂ : t₂ ⊆ x • s₂
rw : t₁ + t₂ ⊆ x • s₁ + x • s₂
⊢ t₁ + t₂ ⊆ x • (s₁ + s₂)

Tactic:
rw [smul_add]

Premises used: smul_add
-- Module: Mathlib.Topology.Bornology.Absorbs
Goal:
M : Type u_1
E : Type u_2
inst : Bornology M
s₁ s₂ t₁ t₂ : Set E
inst_1 : AddZeroClass E
inst_2 : DistribSMul M E
h₁ : Absorbs M s₁ t₁
h₂ : Absorbs M s₂ t₂
x : M
hx₁ : t₁ ⊆ x • s₁
hx₂ : t₂ ⊆ x • s₂
⊢ t₁ + t₂ ⊆ x • s₁ + x • s₂

Tactic:
add_subset_add hx₁ hx₂

Premises used: Set.add_subset_add
-- Module: Mathlib.Topology.Bornology.Absorbs
Goal:
M : Type u_1
E : Type u_2
inst : Bornology M
s₁ s₂ t₁ t₂ : Set E
inst_1 : AddZeroClass E
inst_2 : DistribSMul M E
h₁ : Absorbs M s₁ t₁
h₂ : Absorbs M s₂ t₂
x : M
hx₁ : t₁ ⊆ x • s₁
hx₂ : t₂ ⊆ x • s₂
⊢ t₁ + t₂ ⊆ x • s₁ + x • s₂

Tactic:
exact add_subset_add hx₁ hx₂

Premises used: Set.add_subset_add
-- Module: Mathlib.Topology.Bornology.Absorbs
Goal:
M : Type u_1
E : Type u_2
inst : Bornology M
inst_1 : Zero E
inst_2 : SMulZeroClass M E
s : Set E
hs : 0 ∈ s
⊢ Absorbs M s 0

Tactic:
Eventually.of_forall fun _ ↦ zero_subset.2 <| zero_mem_smul_set hs

Premises used: Iff.mpr, Filter.Eventually.of_forall, Set.zero_subset, Absorbs, Set.zero_mem_smul_set
-- Module: Mathlib.Topology.Bornology.Absorbs
Goal:
G₀ : Type u_1
α : Type u_2
inst : GroupWithZero G₀
inst_1 : Bornology G₀
inst_2 : MulAction G₀ α
s : Set α
a : G₀
ha : a ≠ 0
rw : s ⊆ univ
⊢ s ⊆ HSMul.hSMul (β := Set α) a univ

Tactic:
rw [smul_set_univ₀ ha]

Premises used: Set.smul_set_univ₀
-- Module: Mathlib.Topology.Bornology.Absorbs
Goal:
G₀ : Type u_1
α : Type u_2
inst : GroupWithZero G₀
inst_1 : Bornology G₀
inst_2 : MulAction G₀ α
s : Set α
a : G₀
ha : a ≠ 0
⊢ s ⊆ univ

Tactic:
apply subset_univ

Premises used: Set.subset_univ
-- Module: Mathlib.Topology.Bornology.Absorbs
Goal:
G₀ : Type u_1
α : Type u_2
inst : GroupWithZero G₀
inst_1 : Bornology G₀
inst_2 : MulAction G₀ α
s t : Set α
c : G₀
hc : c ≠ 0
rw : t ⊆ (fun (x : α) ↦ c⁻¹ • x) ⁻¹' s ↔ MapsTo (fun (x : α) ↦ c⁻¹ • x) t s
⊢ t ⊆ c • s ↔ MapsTo (fun (x : α) ↦ c⁻¹ • x) t s

Tactic:
rw [← preimage_smul_inv₀ hc]

Premises used: Set.preimage_smul_inv₀
-- Module: Mathlib.Topology.Bornology.Absorbs
Goal:
G₀ : Type u_1
α : Type u_2
inst : GroupWithZero G₀
inst_1 : Bornology G₀
inst_2 : MulAction G₀ α
s t : Set α
c : G₀
hc : c ≠ 0
⊢ t ⊆ (fun (x : α) ↦ c⁻¹ • x) ⁻¹' s ↔ MapsTo (fun (x : α) ↦ c⁻¹ • x) t s

Tactic:
rfl
-- Module: Mathlib.Topology.Bornology.Absorbs
Goal:
G₀ : Type u_1
α : Type u_2
inst : GroupWithZero G₀
inst_1 : Bornology G₀
inst_2 : MulAction G₀ α
s t u : Set α
⊢ Absorbs G₀ (s ∩ t) u ↔ Absorbs G₀ s u ∧ Absorbs G₀ t u

Tactic:
simp only [absorbs_iff_eventually_cobounded_mapsTo, mapsTo_inter, eventually_and]

Premises used: Filter.eventually_and, absorbs_iff_eventually_cobounded_mapsTo, Set.mapsTo_inter
-- Module: Mathlib.Topology.Bornology.Absorbs
Goal:
G₀ : Type u_1
α : Type u_2
inst : GroupWithZero G₀
inst_1 : Bornology G₀
inst_2 : MulAction G₀ α
s t u : Set α
hs : Absorbs G₀ s u
ht : Absorbs G₀ t u
⊢ Absorbs G₀ (s ∩ t) u

Tactic:
absorbs_inter.2 ⟨hs, ht⟩

Premises used: Iff.mpr, absorbs_inter, And.intro
-- Module: Mathlib.Topology.Bornology.Absorbs
Goal:
G₀ : Type u_1
α : Type u_2
inst : GroupWithZero G₀
inst_1 : Bornology G₀
inst_2 : MulAction G₀ α
s u : Set α
⊢ s ∈ absorbing G₀ u ↔ Absorbs G₀ s u

Tactic:
.rfl

Premises used: Set.Mem, Filter.Eventually, Iff.rfl, setOf, Absorbs
-- Module: Mathlib.Topology.Bornology.Absorbs
Goal:
G₀ : Type u_1
α : Type u_2
inst : GroupWithZero G₀
inst_1 : Bornology G₀
inst_2 : MulAction G₀ α
t : Set α
S : Set (Set α)
hS : S.Finite
⊢ Absorbs G₀ (⋂₀ S) t ↔ ∀ s ∈ S, Absorbs G₀ s t

Tactic:
sInter_mem (f := absorbing G₀ t) hS

Premises used: Set.Mem, Filter.Eventually, setOf, Absorbs, Filter.sInter_mem
-- Module: Mathlib.Topology.Bornology.Absorbs
Goal:
G₀ : Type u_1
α : Type u_2
inst : GroupWithZero G₀
inst_1 : Bornology G₀
inst_2 : MulAction G₀ α
t : Set α
ι : Sort u_3
inst_3 : Finite ι
s : ι → Set α
⊢ Absorbs G₀ (⋂ (i : ι), s i) t ↔ ∀ (i : ι), Absorbs G₀ (s i) t

Tactic:
iInter_mem (f := absorbing G₀ t)

Premises used: Set.Mem, Filter.Eventually, setOf, Filter.iInter_mem, Absorbs