awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
g : Set (Set α)
a : α
this : TopologicalSpace α := generateFrom g
s : Set α
S : Set (Set α)
h : ∀ s ∈ S, GenerateOpen g s
hS :
  ∀ s ∈ S,
    ∀ (ha : a ∈ s), ⨅ (s : Set α), ⨅ (_ : Membership.mem (γ := Set (Set α)) {s : Set α | a ∈ s ∧ s ∈ g} s), 𝓟 s ≤ 𝓟 s
ha : a ∈ ⋃₀ S
t : Set α
htS : t ∈ S
hat : a ∈ t
⊢ ⨅ (s : Set α), ⨅ (_ : Membership.mem (γ := Set (Set α)) {s : Set α | a ∈ s ∧ s ∈ g} s), 𝓟 s ≤ 𝓟 (⋃₀ S)

Tactic:
(hS t htS hat).trans (principal_mono.2 <| subset_sUnion_of_mem htS)

Premises used: Iff.mpr, Filter.principal_mono, Set.subset_sUnion_of_mem, LE.le.trans
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
g : Set (Set α)
a : α
this : TopologicalSpace α := generateFrom g
s : Set α
S : Set (Set α)
h : ∀ s ∈ S, GenerateOpen g s
hS :
  ∀ s ∈ S,
    ∀ (ha : a ∈ s), ⨅ (s : Set α), ⨅ (_ : Membership.mem (γ := Set (Set α)) {s : Set α | a ∈ s ∧ s ∈ g} s), 𝓟 s ≤ 𝓟 s
ha : a ∈ ⋃₀ S
t : Set α
htS : t ∈ S
hat : a ∈ t
⊢ ⨅ (s : Set α), ⨅ (_ : Membership.mem (γ := Set (Set α)) {s : Set α | a ∈ s ∧ s ∈ g} s), 𝓟 s ≤ 𝓟 (⋃₀ S)

Tactic:
exact (hS t htS hat).trans (principal_mono.2 <| subset_sUnion_of_mem htS)

Premises used: Iff.mpr, Filter.principal_mono, Set.subset_sUnion_of_mem, LE.le.trans
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
g : Set (Set α)
a : α
this : TopologicalSpace α := generateFrom g
s : Set α
ha : a ∈ s
hs : IsOpen[generateFrom g] s
basic :
  ∀ (s : Set α) (hs : s ∈ g) (ha : a ∈ s),
    ⨅ (s : Set α), ⨅ (_ : Membership.mem (γ := Set (Set α)) {s : Set α | a ∈ s ∧ s ∈ g} s), 𝓟 s ≤ 𝓟 s
univ :
  ∀ (ha : Membership.mem (γ := Set α) Set.univ a),
    LE.le.{u} (α := Filter α)
      (⨅ (s : Set α), ⨅ (_ : Membership.mem (γ := Set (Set α)) {s : Set α | a ∈ s ∧ s ∈ g} s), 𝓟 s) (𝓟 Set.univ)
inter :
  ∀ (s t : Set α),
    GenerateOpen g s →
      GenerateOpen g t →
        ∀
          (hs :
            ∀ (ha : a ∈ s),
              ⨅ (s : Set α), ⨅ (_ : Membership.mem (γ := Set (Set α)) {s : Set α | a ∈ s ∧ s ∈ g} s), 𝓟 s ≤ 𝓟 s)
          (ht :
            ∀ (ha : a ∈ t),
              ⨅ (s : Set α), ⨅ (_ : Membership.mem (γ := Set (Set α)) {s : Set α | a ∈ s ∧ s ∈ g} s), 𝓟 s ≤ 𝓟 t)
          (ha : a ∈ s ∩ t),
          ⨅ (s : Set α), ⨅ (_ : Membership.mem (γ := Set (Set α)) {s : Set α | a ∈ s ∧ s ∈ g} s), 𝓟 s ≤ 𝓟 (s ∩ t)
sUnion :
  ∀ (S : Set (Set α)),
    (∀ s ∈ S, GenerateOpen g s) →
      ∀
        (hS :
          ∀ s ∈ S,
            ∀ (ha : a ∈ s),
              ⨅ (s : Set α), ⨅ (_ : Membership.mem (γ := Set (Set α)) {s : Set α | a ∈ s ∧ s ∈ g} s), 𝓟 s ≤ 𝓟 s)
        (ha : a ∈ ⋃₀ S),
        ⨅ (s : Set α), ⨅ (_ : Membership.mem (γ := Set (Set α)) {s : Set α | a ∈ s ∧ s ∈ g} s), 𝓟 s ≤ 𝓟 (⋃₀ S)
⊢ ⨅ (s : Set α), ⨅ (_ : Membership.mem (γ := Set (Set α)) {s : Set α | a ∈ s ∧ s ∈ g} s), 𝓟 s ≤ 𝓟 s

Tactic:
induction hs with
  | basic _ hs => exact iInf₂_le _ ⟨ha, hs⟩
  | univ => exact le_top.trans_eq principal_univ.symm
  | inter _ _ _ _ hs ht => exact (le_inf (hs ha.1) (ht ha.2)).trans_eq inf_principal
  | sUnion _ _ hS =>
    let ⟨t, htS, hat⟩ := ha
    exact (hS t htS hat).trans (principal_mono.2 <| subset_sUnion_of_mem htS)

Premises used: LE.le.trans_eq, Set.univ, iInf₂_le, Set.sUnion, Filter.principal_univ, le_top, Eq.symm
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
β : Type u_1
m : α → β
f : Filter α
g : Set (Set β)
b : β
simp : (∀ (i : Set β) (b_1 : i ∈ g) (a : b ∈ i), ∀ᶠ (a : α) in f, m a ∈ i) ↔ ∀ s ∈ g, b ∈ s → m ⁻¹' s ∈ f
⊢ Tendsto m f (𝓝 b) ↔ ∀ s ∈ g, b ∈ s → m ⁻¹' s ∈ f

Tactic:
simp only [nhds_generateFrom, @forall_comm (b ∈ _), tendsto_iInf, mem_setOf_eq, and_imp,
    tendsto_principal]

Premises used: and_imp, forall_comm, TopologicalSpace.nhds_generateFrom, Filter.tendsto_principal, Set.mem_setOf_eq, Filter.tendsto_iInf
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
β : Type u_1
m : α → β
f : Filter α
g : Set (Set β)
b : β
⊢ (∀ (i : Set β) (b_1 : i ∈ g) (a : b ∈ i), ∀ᶠ (a : α) in f, m a ∈ i) ↔ ∀ s ∈ g, b ∈ s → m ⁻¹' s ∈ f

Tactic:
rfl
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
n : α → Filter α
ι : α → Sort u_1
p : (a : α) → ι a → Prop
s : (a : α) → ι a → Set α
hb : ∀ (a : α), (n a).HasBasis (p a) (s a)
hpure : ∀ (a : α) (i : ι a), p a i → a ∈ s a i
hopen : ∀ (a : α) (i : ι a), p a i → ∀ᶠ (x : α) in n a, s a i ∈ n x
a : α
t : TopologicalSpace α := TopologicalSpace.mkOfNhds n
a₁ : 𝓝 a ≤ n a
a₂ : n a ≤ 𝓝 a
⊢ 𝓝 a = n a

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
n : α → Filter α
ι : α → Sort u_1
p : (a : α) → ι a → Prop
s : (a : α) → ι a → Set α
hb : ∀ (a : α), (n a).HasBasis (p a) (s a)
hpure : ∀ (a : α) (i : ι a), p a i → a ∈ s a i
hopen : ∀ (a : α) (i : ι a), p a i → ∀ᶠ (x : α) in n a, s a i ∈ n x
a : α
t : TopologicalSpace α := TopologicalSpace.mkOfNhds n
U : Set α
hU : U ∈ n a
⊢ pure ≤ n

Tactic:
replace hpure : pure ≤ n := fun x ↦ (hb x).ge_iff.2 (hpure x)
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
n : α → Filter α
ι : α → Sort u_1
p : (a : α) → ι a → Prop
s : (a : α) → ι a → Set α
hb : ∀ (a : α), (n a).HasBasis (p a) (s a)
hopen : ∀ (a : α) (i : ι a), p a i → ∀ᶠ (x : α) in n a, s a i ∈ n x
a : α
t : TopologicalSpace α := TopologicalSpace.mkOfNhds n
U : Set α
hU : U ∈ n a
hpure : pure ≤ n
⊢ U ∈ 𝓝 a

Tactic:
mem_nhds_iff.2 ⟨{x | U ∈ n x}, fun x hx ↦ hpure x hx, fun x hx ↦ ?_, hU⟩

Premises used: Iff.mpr, mem_nhds_iff, setOf, Membership.mem, And.intro, Exists.intro
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
n : α → Filter α
ι : α → Sort u_1
p : (a : α) → ι a → Prop
s : (a : α) → ι a → Set α
hb : ∀ (a : α), (n a).HasBasis (p a) (s a)
hopen : ∀ (a : α) (i : ι a), p a i → ∀ᶠ (x : α) in n a, s a i ∈ n x
a : α
t : TopologicalSpace α := TopologicalSpace.mkOfNhds n
U : Set α
hU : U ∈ n a
hpure : pure ≤ n
a₁ : ∀ (x : α) (hx : Membership.mem (γ := Set α) {x : α | U ∈ n x} x), {x : α | U ∈ n x} ∈ n x
⊢ U ∈ 𝓝 a

Tactic:
refine mem_nhds_iff.2 ⟨{x | U ∈ n x}, fun x hx ↦ hpure x hx, fun x hx ↦ ?_, hU⟩

Premises used: Iff.mpr, mem_nhds_iff, setOf, Membership.mem, And.intro, Exists.intro
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
n : α → Filter α
ι : α → Sort u_1
p : (a : α) → ι a → Prop
s : (a : α) → ι a → Set α
hb : ∀ (a : α), (n a).HasBasis (p a) (s a)
hopen : ∀ (a : α) (i : ι a), p a i → ∀ᶠ (x : α) in n a, s a i ∈ n x
a : α
t : TopologicalSpace α := TopologicalSpace.mkOfNhds n
U : Set α
hU : U ∈ n a
hpure : pure ≤ n
x : α
hx : Membership.mem (γ := Set α) {x : α | U ∈ n x} x
a₁ : ∀ (i : ι x) (hpi : p x i) (hi : s x i ⊆ U), {x : α | U ∈ n x} ∈ n x
⊢ {x : α | U ∈ n x} ∈ n x

Tactic:
rcases (hb x).mem_iff.1 hx with ⟨i, hpi, hi⟩

Premises used: Filter.HasBasis.mem_iff, Iff.mp
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
n : α → Filter α
ι : α → Sort u_1
p : (a : α) → ι a → Prop
s : (a : α) → ι a → Set α
hb : ∀ (a : α), (n a).HasBasis (p a) (s a)
hopen : ∀ (a : α) (i : ι a), p a i → ∀ᶠ (x : α) in n a, s a i ∈ n x
a : α
t : TopologicalSpace α := TopologicalSpace.mkOfNhds n
U : Set α
hU : U ∈ n a
hpure : pure ≤ n
x : α
hx : Membership.mem (γ := Set α) {x : α | U ∈ n x} x
i : ι x
hpi : p x i
hi : s x i ⊆ U
y : α
⊢ s x i ∈ n y → U ∈ n y

Tactic:
gcongr
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
n : α → Filter α
ι : α → Sort u_1
p : (a : α) → ι a → Prop
s : (a : α) → ι a → Set α
hb : ∀ (a : α), (n a).HasBasis (p a) (s a)
hopen : ∀ (a : α) (i : ι a), p a i → ∀ᶠ (x : α) in n a, s a i ∈ n x
a : α
t : TopologicalSpace α := TopologicalSpace.mkOfNhds n
U : Set α
hU : U ∈ n a
hpure : pure ≤ n
x : α
hx : Membership.mem (γ := Set α) {x : α | U ∈ n x} x
i : ι x
hpi : p x i
hi : s x i ⊆ U
⊢ {x : α | U ∈ n x} ∈ n x

Tactic:
exact (hopen x i hpi).mono fun y ↦ by gcongr

Premises used: Filter.Eventually.mono
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
n : α → Filter α
ι : α → Sort u_1
p : (a : α) → ι a → Prop
s : (a : α) → ι a → Set α
hb : ∀ (a : α), (n a).HasBasis (p a) (s a)
hpure : ∀ (a : α) (i : ι a), p a i → a ∈ s a i
hopen : ∀ (a : α) (i : ι a), p a i → ∀ᶠ (x : α) in n a, s a i ∈ n x
a : α
t : TopologicalSpace α := TopologicalSpace.mkOfNhds n
⊢ n a ≤ 𝓝 a

Tactic:
(nhds_basis_opens a).ge_iff.2 fun U ⟨haU, hUo⟩ ↦ hUo a haU

Premises used: Iff.mpr, Set.Mem, Membership.mem, Filter.HasBasis.ge_iff, _private.0.TopologicalSpace.nhds_mkOfNhds_of_hasBasis.match_1, nhds_basis_opens
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
n : α → Filter α
ι : α → Sort u_1
p : (a : α) → ι a → Prop
s : (a : α) → ι a → Set α
hb : ∀ (a : α), (n a).HasBasis (p a) (s a)
hpure : ∀ (a : α) (i : ι a), p a i → a ∈ s a i
hopen : ∀ (a : α) (i : ι a), p a i → ∀ᶠ (x : α) in n a, s a i ∈ n x
a : α
t : TopologicalSpace α := TopologicalSpace.mkOfNhds n
⊢ n a ≤ 𝓝 a

Tactic:
exact (nhds_basis_opens a).ge_iff.2 fun U ⟨haU, hUo⟩ ↦ hUo a haU

Premises used: Iff.mpr, Membership.mem, Filter.HasBasis.ge_iff, _private.0.TopologicalSpace.nhds_mkOfNhds_of_hasBasis.match_1, nhds_basis_opens
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
n : α → Filter α
a : α
h₀ : pure ≤ n
h₁ : ∀ (a : α), ∀ s ∈ n a, ∀ᶠ (y : α) in n a, s ∈ n y
⊢ 𝓝 a = n a

Tactic:
nhds_mkOfNhds_of_hasBasis (fun a ↦ (n a).basis_sets) h₀ h₁ _

Premises used: TopologicalSpace.nhds_mkOfNhds_of_hasBasis, Filter.basis_sets
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
inst : DecidableEq α
a₀ : α
l : Filter α
h : pure a₀ ≤ l
b : α
⊢ 𝓝 b = update (β := fun (a : α) ↦ Filter α) pure a₀ l b

Tactic:
nhds_mkOfNhds _ _ (le_update_iff.mpr ⟨h, fun _ _ => le_rfl⟩) fun a s hs => ?_

Premises used: Iff.mpr, le_rfl, le_update_iff, And.intro, TopologicalSpace.nhds_mkOfNhds
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
inst : DecidableEq α
a₀ : α
l : Filter α
h : pure a₀ ≤ l
b : α
refine :
  ∀ (a : α) (s : Set α) (hs : s ∈ update (β := fun (a : α) ↦ Filter α) pure a₀ l a),
    ∀ᶠ (y : α) in update (β := fun (a : α) ↦ Filter α) pure a₀ l a, s ∈ update (β := fun (a : α) ↦ Filter α) pure a₀ l y
⊢ 𝓝 b = update (β := fun (a : α) ↦ Filter α) pure a₀ l b

Tactic:
refine nhds_mkOfNhds _ _ (le_update_iff.mpr ⟨h, fun _ _ => le_rfl⟩) fun a s hs => ?_

Premises used: Iff.mpr, le_rfl, le_update_iff, And.intro, TopologicalSpace.nhds_mkOfNhds
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
inst : DecidableEq α
a₀ : α
l : Filter α
h : pure a₀ ≤ l
b a : α
s : Set α
hs : s ∈ update (β := fun (a : α) ↦ Filter α) pure a₀ l a
inl :
  ∀ (h : pure a ≤ l) (hs : s ∈ update (β := fun (a : α) ↦ Filter α) pure a l a),
    ∀ᶠ (y : α) in update (β := fun (a : α) ↦ Filter α) pure a l a, s ∈ update (β := fun (a : α) ↦ Filter α) pure a l y
inr :
  ∀ (ha : a ≠ a₀),
    ∀ᶠ (y : α) in update (β := fun (a : α) ↦ Filter α) pure a₀ l a, s ∈ update (β := fun (a : α) ↦ Filter α) pure a₀ l y
⊢ ∀ᶠ (y : α) in update (β := fun (a : α) ↦ Filter α) pure a₀ l a, s ∈ update (β := fun (a : α) ↦ Filter α) pure a₀ l y

Tactic:
rcases eq_or_ne a a₀ with (rfl | ha)

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
inst : DecidableEq α
l : Filter α
b a : α
s : Set α
h : pure a ≤ l
hs : s ∈ update (β := fun (a : α) ↦ Filter α) pure a l a
h₁ : ∀ (b : α) (hb : b ∈ s), s ∈ update (β := fun (a : α) ↦ Filter α) pure a l b
⊢ ∀ᶠ (y : α) in update (β := fun (a : α) ↦ Filter α) pure a l a, s ∈ update (β := fun (a : α) ↦ Filter α) pure a l y

Tactic:
filter_upwards [hs] with b hb
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
inst : DecidableEq α
l : Filter α
b_1 a : α
s : Set α
h : pure a ≤ l
hs : s ∈ update (β := fun (a : α) ↦ Filter α) pure a l a
b : α
hb : b ∈ s
h₁ :
  ∀ (h : pure b ≤ l) (hs : s ∈ update (β := fun (a : α) ↦ Filter α) pure b l b),
    s ∈ update (β := fun (a : α) ↦ Filter α) pure b l b
h₂ : ∀ (hb : b ≠ a), s ∈ update (β := fun (a : α) ↦ Filter α) pure a l b
⊢ s ∈ update (β := fun (a : α) ↦ Filter α) pure a l b

Tactic:
rcases eq_or_ne b a with (rfl | hb)

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
inst : DecidableEq α
l : Filter α
b_1 : α
s : Set α
b : α
hb : b ∈ s
h : pure b ≤ l
hs : s ∈ update (β := fun (a : α) ↦ Filter α) pure b l b
⊢ s ∈ update (β := fun (a : α) ↦ Filter α) pure b l b

Tactic:
hs
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
inst : DecidableEq α
l : Filter α
b_1 : α
s : Set α
b : α
hb : b ∈ s
h : pure b ≤ l
hs : s ∈ update (β := fun (a : α) ↦ Filter α) pure b l b
⊢ s ∈ update (β := fun (a : α) ↦ Filter α) pure b l b

Tactic:
exact hs
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
inst : DecidableEq α
l : Filter α
b_1 a : α
s : Set α
h : pure a ≤ l
hs : s ∈ update (β := fun (a : α) ↦ Filter α) pure a l a
b : α
hb_1 : b ∈ s
hb : b ≠ a
h₁ h₂ h₃ h₄ : Membership.mem (γ := Filter α) (pure b) s
⊢ s ∈ update (β := fun (a : α) ↦ Filter α) pure a l b

Tactic:
rwa [update_of_ne hb]

Premises used: Function.update_of_ne
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
inst : DecidableEq α
a₀ : α
l : Filter α
h : pure a₀ ≤ l
b a : α
s : Set α
hs : s ∈ update (β := fun (a : α) ↦ Filter α) pure a₀ l a
ha : a ≠ a₀
⊢ ∀ᶠ (y : α) in update (β := fun (a : α) ↦ Filter α) pure a₀ l a, s ∈ update (β := fun (a : α) ↦ Filter α) pure a₀ l y

Tactic:
simpa only [update_of_ne ha, mem_pure, eventually_pure] using hs

Premises used: Filter.eventually_pure, Filter.mem_pure, Function.update_of_ne
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
B : α → FilterBasis α
a : α
h₀ : ∀ (x : α), ∀ n ∈ B x, x ∈ n
h₁ : ∀ (x : α), ∀ n ∈ B x, ∃ n₁ ∈ B x, ∀ x' ∈ n₁, ∃ n₂ ∈ B x', n₂ ⊆ n
⊢ 𝓝 a = (B a).filter

Tactic:
nhds_mkOfNhds_of_hasBasis (fun a ↦ (B a).hasBasis) h₀ h₁ a

Premises used: FilterBasis.hasBasis, TopologicalSpace.nhds_mkOfNhds_of_hasBasis
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_1
t s : TopologicalSpace α
⊢ t ≤ s ↔ LE.le.{u_1} (α := Set α → Prop) IsOpen[s] IsOpen[t]

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
g : Set (Set α)
t : TopologicalSpace α
⊢ t ≤ generateFrom g ↔ g ⊆ {s : Set α | IsOpen[t] s}

Tactic:
⟨fun ht s hs => ht _ <| .basic s hs, fun hg _s hs =>
    hs.recOn (fun _ h => hg h) isOpen_univ (fun _ _ _ _ => IsOpen.inter) fun _ _ => isOpen_sUnion⟩

Premises used: TopologicalSpace.GenerateOpen.basic, TopologicalSpace.GenerateOpen.recOn, Iff.intro
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
s : Set (Set α)
hs : {u : Set α | GenerateOpen s u} = s
h : ∀ (U : Set α), IsOpen[TopologicalSpace.mkOfClosure s hs] U ↔ IsOpen[generateFrom s] U
⊢ Eq.{u + 1} (α := Set α → Prop) IsOpen[TopologicalSpace.mkOfClosure s hs] IsOpen[generateFrom s]

Tactic:
ext U
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
s : Set (Set α)
hs : {u : Set α | GenerateOpen s u} = s
U : Set α
⊢ IsOpen[TopologicalSpace.mkOfClosure s hs] U ↔ IsOpen[generateFrom s] U

Tactic:
Set.ext_iff.mp hs.symm U

Premises used: Set.Mem, setOf, Iff.mp, IsOpen, Set.ext_iff, Eq.symm
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
s : Set (Set α)
hs : {u : Set α | GenerateOpen s u} = s
U : Set α
⊢ IsOpen[TopologicalSpace.mkOfClosure s hs] U ↔ IsOpen[generateFrom s] U

Tactic:
exact Set.ext_iff.mp hs.symm U

Premises used: Iff.mp, Set.ext_iff, Eq.symm
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_1
⊢ GaloisConnection (β := (Set (Set α))ᵒᵈ)
    (fun (t : TopologicalSpace α) ↦ (OrderDual.toDual : (a : Set (Set α)) → (Set (Set α))ᵒᵈ) {s : Set α | IsOpen s})
    (generateFrom ∘ (⇑OrderDual.ofDual : (a : (Set (Set α))ᵒᵈ) → Set (Set α)))

Tactic:
fun _ _ =>
  le_generateFrom_iff_subset_isOpen.symm

Premises used: setOf, IsOpen, Iff.symm, TopologicalSpace.le_generateFrom_iff_subset_isOpen, GaloisConnection
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_1
g₁ g₂ : Set (Set α)
h : g₁ ⊆ g₂
⊢ generateFrom g₂ ≤ generateFrom g₁

Tactic:
(gc_generateFrom _).monotone_u h

Premises used: GaloisConnection.monotone_u, TopologicalSpace.gc_generateFrom
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
t : TopologicalSpace α
⊢ generateFrom {s : Set α | IsOpen[t] s} = t

Tactic:
(gciGenerateFrom α).u_l_eq t

Premises used: setOf, TopologicalSpace.gciGenerateFrom, IsOpen, GaloisCoinsertion.u_l_eq
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
⊢ LeftInverse generateFrom fun (t : TopologicalSpace α) ↦ {s : Set α | IsOpen s}

Tactic:
(gciGenerateFrom α).leftInverse_u_l

Premises used: setOf, TopologicalSpace.gciGenerateFrom, GaloisCoinsertion.leftInverse_u_l, IsOpen, OrderDual
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
⊢ Surjective.{u + 1, u + 1} (α := Set (Set α)) generateFrom

Tactic:
(gciGenerateFrom α).u_surjective

Premises used: TopologicalSpace.gciGenerateFrom, OrderDual, GaloisCoinsertion.u_surjective
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
⊢ Injective (β := Set (Set α)) fun (t : TopologicalSpace α) ↦ {s : Set α | IsOpen s}

Tactic:
(gciGenerateFrom α).l_injective

Premises used: GaloisCoinsertion.l_injective, setOf, TopologicalSpace.gciGenerateFrom, IsOpen, OrderDual
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_1
t₁ t₂ : TopologicalSpace α
s : Set α
hs : IsOpen[t₂] s
h : t₁ ≤ t₂
⊢ IsOpen[t₁] s

Tactic:
h s hs
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_1
t₁ t₂ : TopologicalSpace α
s : Set α
hs : IsClosed[t₂] s
h : t₁ ≤ t₂
⊢ IsClosed[t₁] s

Tactic:
(@isOpen_compl_iff α s t₁).mp <| hs.isOpen_compl.mono h

Premises used: IsClosed.isOpen_compl, Iff.mp, isOpen_compl_iff, IsOpen.mono
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_1
t₁ t₂ : TopologicalSpace α
s : Set α
h : t₁ ≤ t₂
⊢ closure[t₁] s ⊆ closure[t₂] s

Tactic:
@closure_minimal _ t₁ s (@closure _ t₂ s) subset_closure (IsClosed.mono isClosed_closure h)

Premises used: subset_closure, closure_minimal, IsClosed.mono, isClosed_closure
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_1
t₁ t₂ : TopologicalSpace α
⊢ (∀ (s : Set α), IsOpen[t₁] s → IsOpen[t₂] s) ↔ t₂ ≤ t₁

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_1
t t₁ t₂ : TopologicalSpace α
s : Set α
⊢ IndiscreteTopology α

Tactic:
@IndiscreteTopology.mk _ ⊤ rfl

Premises used: IndiscreteTopology.mk, rfl
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_2
inst : TopologicalSpace α
⊢ IndiscreteTopology α ∨ NontrivialTopology α

Tactic:
(eq_or_ne ‹TopologicalSpace α› ⊤).imp .mk .mk

Premises used: IndiscreteTopology.mk, NontrivialTopology.mk, Or.imp
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
⊢ ¬IndiscreteTopology α ↔ NontrivialTopology α

Tactic:
⟨fun h => ⟨fun x => h ⟨x⟩⟩, fun h x => h.ne_top x.eq_top⟩

Premises used: IndiscreteTopology.mk, NontrivialTopology.mk, IndiscreteTopology.eq_top, NontrivialTopology.ne_top, Iff.intro
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
⊢ ¬NontrivialTopology α ↔ IndiscreteTopology α

Tactic:
TopologicalSpace.not_indiscrete_iff.not_right.symm

Premises used: TopologicalSpace.not_indiscrete_iff, Iff.not_right, Iff.symm
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_1
t₂ : TopologicalSpace α
inst : IndiscreteTopology α
U : Set α
refl : ∀ [IndiscreteTopology α], IsOpen[⊤] U ↔ U = ∅ ∨ U = univ
⊢ IsOpen[t₂] U ↔ U = ∅ ∨ U = univ

Tactic:
cases IndiscreteTopology.eq_top α

Premises used: IndiscreteTopology.eq_top
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_1
U : Set α
inst : IndiscreteTopology α
⊢ IsOpen[⊤] U ↔ U = ∅ ∨ U = univ

Tactic:
⟨fun h => ?_, ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_1
U : Set α
inst : IndiscreteTopology α
refl : ∀ (h : IsOpen[⊤] U), U = ∅ ∨ U = univ
refl₁ : U = ∅ ∨ U = univ → IsOpen[⊤] U
⊢ IsOpen[⊤] U ↔ U = ∅ ∨ U = univ

Tactic:
refine ⟨fun h => ?_, ?_⟩
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_1
U : Set α
inst : IndiscreteTopology α
s : Set α
h : Membership.mem (γ := Set (Set α)) ((OrderDual.ofDual : (a : (Set (Set α))ᵒᵈ) → Set (Set α)) ⊤ : Set (Set α)) s
⊢ s = ∅ ∨ s = univ

Tactic:
False.elim h

Premises used: False.elim
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_1
U : Set α
inst : IndiscreteTopology α
s : Set α
h : Membership.mem (γ := Set (Set α)) ((OrderDual.ofDual : (a : (Set (Set α))ᵒᵈ) → Set (Set α)) ⊤ : Set (Set α)) s
⊢ s = ∅ ∨ s = univ

Tactic:
exact False.elim h

Premises used: False.elim
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_1
U : Set α
inst : IndiscreteTopology α
⊢ Eq.{u_1 + 1} (α := Set α) univ ∅ ∨ Eq.{u_1 + 1} (α := Set α) univ univ

Tactic:
.inr rfl

Premises used: Or.inr, rfl
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_1
U : Set α
inst : IndiscreteTopology α
⊢ Eq.{u_1 + 1} (α := Set α) univ ∅ ∨ Eq.{u_1 + 1} (α := Set α) univ univ

Tactic:
exact .inr rfl
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_1
U : Set α
inst : IndiscreteTopology α
s t : Set α
h : TopologicalSpace.GenerateOpen ((OrderDual.ofDual : (a : (Set (Set α))ᵒᵈ) → Set (Set α)) ⊤) s
h_1 : TopologicalSpace.GenerateOpen ((OrderDual.ofDual : (a : (Set (Set α))ᵒᵈ) → Set (Set α)) ⊤) t
h₁ : s = ∅ ∨ s = univ
h₂ : t = ∅ ∨ t = univ
refl :
  TopologicalSpace.GenerateOpen.{u_1} (α := α) ((OrderDual.ofDual : (a : (Set (Set α))ᵒᵈ) → Set (Set α)) ⊤) ∅ →
    ∅ ∩ t = ∅ ∨ ∅ ∩ t = univ
refl₁ :
  TopologicalSpace.GenerateOpen.{u_1} (α := α) ((OrderDual.ofDual : (a : (Set (Set α))ᵒᵈ) → Set (Set α)) ⊤) univ →
    univ ∩ t = ∅ ∨ univ ∩ t = univ
⊢ s ∩ t = ∅ ∨ s ∩ t = univ

Tactic:
rcases h₁ with (rfl | rfl)

Premises used: rfl
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_1
U : Set α
inst : IndiscreteTopology α
t : Set α
h : TopologicalSpace.GenerateOpen ((OrderDual.ofDual : (a : (Set (Set α))ᵒᵈ) → Set (Set α)) ⊤) t
h₂ : t = ∅ ∨ t = univ
h_1 : TopologicalSpace.GenerateOpen.{u_1} (α := α) ((OrderDual.ofDual : (a : (Set (Set α))ᵒᵈ) → Set (Set α)) ⊤) ∅
refl :
  TopologicalSpace.GenerateOpen.{u_1} (α := α) ((OrderDual.ofDual : (a : (Set (Set α))ᵒᵈ) → Set (Set α)) ⊤) ∅ →
    Eq.{u_1 + 1} (α := Set α) (∅ ∩ ∅) ∅ ∨ Eq.{u_1 + 1} (α := Set α) (∅ ∩ ∅) univ
refl₁ :
  TopologicalSpace.GenerateOpen.{u_1} (α := α) ((OrderDual.ofDual : (a : (Set (Set α))ᵒᵈ) → Set (Set α)) ⊤) univ →
    Eq.{u_1 + 1} (α := Set α) (∅ ∩ univ) ∅ ∨ Eq.{u_1 + 1} (α := Set α) (∅ ∩ univ) univ
⊢ ∅ ∩ t = ∅ ∨ ∅ ∩ t = univ

Tactic:
rcases h₂ with (rfl | rfl)

Premises used: rfl
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_1
U : Set α
inst : IndiscreteTopology α
t : Set α
h : TopologicalSpace.GenerateOpen ((OrderDual.ofDual : (a : (Set (Set α))ᵒᵈ) → Set (Set α)) ⊤) t
h₂ : t = ∅ ∨ t = univ
h_1 : TopologicalSpace.GenerateOpen.{u_1} (α := α) ((OrderDual.ofDual : (a : (Set (Set α))ᵒᵈ) → Set (Set α)) ⊤) univ
refl :
  TopologicalSpace.GenerateOpen.{u_1} (α := α) ((OrderDual.ofDual : (a : (Set (Set α))ᵒᵈ) → Set (Set α)) ⊤) ∅ →
    Eq.{u_1 + 1} (α := Set α) (univ ∩ ∅) ∅ ∨ Eq.{u_1 + 1} (α := Set α) (univ ∩ ∅) univ
refl₁ :
  TopologicalSpace.GenerateOpen.{u_1} (α := α) ((OrderDual.ofDual : (a : (Set (Set α))ᵒᵈ) → Set (Set α)) ⊤) univ →
    Eq.{u_1 + 1} (α := Set α) (univ ∩ univ) ∅ ∨ Eq.{u_1 + 1} (α := Set α) (univ ∩ univ) univ
⊢ univ ∩ t = ∅ ∨ univ ∩ t = univ

Tactic:
rcases h₂ with (rfl | rfl)

Premises used: rfl
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_1
U : Set α
inst : IndiscreteTopology α
h h_1 : TopologicalSpace.GenerateOpen.{u_1} (α := α) ((OrderDual.ofDual : (a : (Set (Set α))ᵒᵈ) → Set (Set α)) ⊤) ∅
⊢ Eq.{u_1 + 1} (α := Set α) (∅ ∩ ∅) ∅ ∨ Eq.{u_1 + 1} (α := Set α) (∅ ∩ ∅) univ

Tactic:
simp
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_1
U : Set α
inst : IndiscreteTopology α
h : TopologicalSpace.GenerateOpen.{u_1} (α := α) ((OrderDual.ofDual : (a : (Set (Set α))ᵒᵈ) → Set (Set α)) ⊤) ∅
h_1 : TopologicalSpace.GenerateOpen.{u_1} (α := α) ((OrderDual.ofDual : (a : (Set (Set α))ᵒᵈ) → Set (Set α)) ⊤) univ
⊢ Eq.{u_1 + 1} (α := Set α) (∅ ∩ univ) ∅ ∨ Eq.{u_1 + 1} (α := Set α) (∅ ∩ univ) univ

Tactic:
simp
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_1
U : Set α
inst : IndiscreteTopology α
h : TopologicalSpace.GenerateOpen.{u_1} (α := α) ((OrderDual.ofDual : (a : (Set (Set α))ᵒᵈ) → Set (Set α)) ⊤) univ
h_1 : TopologicalSpace.GenerateOpen.{u_1} (α := α) ((OrderDual.ofDual : (a : (Set (Set α))ᵒᵈ) → Set (Set α)) ⊤) ∅
⊢ Eq.{u_1 + 1} (α := Set α) (univ ∩ ∅) ∅ ∨ Eq.{u_1 + 1} (α := Set α) (univ ∩ ∅) univ

Tactic:
simp
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_1
U : Set α
inst : IndiscreteTopology α
h h_1 : TopologicalSpace.GenerateOpen.{u_1} (α := α) ((OrderDual.ofDual : (a : (Set (Set α))ᵒᵈ) → Set (Set α)) ⊤) univ
⊢ Eq.{u_1 + 1} (α := Set α) (univ ∩ univ) ∅ ∨ Eq.{u_1 + 1} (α := Set α) (univ ∩ univ) univ

Tactic:
simp