awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Order (goal)
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)
⊢ ⨅ (s : Set α), ⨅ (_ : Membership.mem (γ := Set (Set α)) {s : Set α | a ∈ s ∧ s ∈ g} s), 𝓟 s ≤ 𝓟 s
have 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)
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)
Cleared hypotheses: ha, hs
-- Lean 4 proof step from Mathlib.Topology.Order (goal)
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)
⊢ ⨅ (s : Set α), ⨅ (_ : Membership.mem (γ := Set (Set α)) {s : Set α | a ∈ s ∧ s ∈ g} s), 𝓟 s ≤ 𝓟 s
have 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)
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)
Cleared hypotheses: ha, hs
-- Lean 4 proof step from Mathlib.Topology.Order (goal)
Goal:
α : Type u
β : Type u_1
m : α → β
f : Filter α
g : Set (Set β)
b : β
⊢ Tendsto m f (𝓝 b) ↔ ∀ s ∈ g, b ∈ s → m ⁻¹' s ∈ f
have simp : (∀ (i : Set β) (b_1 : i ∈ g) (a : b ∈ i), ∀ᶠ (a : α) in f, m a ∈ i) ↔ ∀ s ∈ g, b ∈ s → m ⁻¹' s ∈ f
Tactic: simp only [nhds_generateFrom, @forall_comm (b ∈ _), tendsto_iInf, mem_setOf_eq, and_imp,
    tendsto_principal]
-- Lean 4 proof step from Mathlib.Topology.Order (goal)
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 = n a
have a₁ : 𝓝 a ≤ n a
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Topology.Order (goal)
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
have a₂ : n a ≤ 𝓝 a
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Topology.Order (hypothesis)
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
⊢ U ∈ 𝓝 a
have hpure₁ : pure ≤ n
Tactic: replace hpure : pure ≤ n := fun x ↦ (hb x).ge_iff.2 (hpure x)
Cleared hypotheses: hpure
-- Lean 4 proof step from Mathlib.Topology.Order (goal)
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
have a₁ : ∀ (x : α) (hx : Membership.mem (γ := Set α) {x : α | U ∈ n x} x), {x : α | U ∈ n x} ∈ n x
Tactic: refine mem_nhds_iff.2 ⟨{x | U ∈ n x}, fun x hx ↦ hpure x hx, fun x hx ↦ ?_, hU⟩
-- Lean 4 proof step from Mathlib.Topology.Order (goal)
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
⊢ {x : α | U ∈ n x} ∈ n x
have a₁ : ∀ (i : ι x) (hpi : p x i) (hi : s x i ⊆ U), {x : α | U ∈ n x} ∈ n x
Tactic: rcases (hb x).mem_iff.1 hx with ⟨i, hpi, hi⟩
-- Lean 4 proof step from Mathlib.Topology.Order (goal)
Goal:
α : Type u
inst : DecidableEq α
a₀ : α
l : Filter α
h : pure a₀ ≤ l
b : α
⊢ 𝓝 b = update (β := fun (a : α) ↦ Filter α) pure a₀ l b
have 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
Tactic: refine nhds_mkOfNhds _ _ (le_update_iff.mpr ⟨h, fun _ _ => le_rfl⟩) fun a s hs => ?_
-- Lean 4 proof step from Mathlib.Topology.Order (goal)
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
⊢ ∀ᶠ (y : α) in update (β := fun (a : α) ↦ Filter α) pure a₀ l a, s ∈ update (β := fun (a : α) ↦ Filter α) pure a₀ l y
have 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
Tactic: rcases eq_or_ne a a₀ with (rfl | ha)
Cleared hypotheses: a₀, h, hs
-- Lean 4 proof step from Mathlib.Topology.Order (goal)
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
⊢ ∀ᶠ (y : α) in update (β := fun (a : α) ↦ Filter α) pure a₀ l a, s ∈ update (β := fun (a : α) ↦ Filter α) pure a₀ l y
have inr : ∀ (ha : a ≠ a₀),
  ∀ᶠ (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)
-- Lean 4 proof step from Mathlib.Topology.Order (goal)
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
⊢ ∀ᶠ (y : α) in update (β := fun (a : α) ↦ Filter α) pure a l a, s ∈ update (β := fun (a : α) ↦ Filter α) pure a l y
have h₁ : ∀ (b : α) (hb : b ∈ s), s ∈ update (β := fun (a : α) ↦ Filter α) pure a l b
Tactic: filter_upwards [hs] with b hb
-- Lean 4 proof step from Mathlib.Topology.Order (goal)
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
⊢ s ∈ update (β := fun (a : α) ↦ Filter α) pure a l b
have h₁ : ∀ (h : pure b ≤ l) (hs : s ∈ update (β := fun (a : α) ↦ Filter α) pure b l b),
  s ∈ update (β := fun (a : α) ↦ Filter α) pure b l b
Tactic: rcases eq_or_ne b a with (rfl | hb)
Cleared hypotheses: a, h, hs
-- Lean 4 proof step from Mathlib.Topology.Order (goal)
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
⊢ s ∈ update (β := fun (a : α) ↦ Filter α) pure a l b
have h₂ : ∀ (hb : b ≠ a), s ∈ update (β := fun (a : α) ↦ Filter α) pure a l b
Tactic: rcases eq_or_ne b a with (rfl | hb)
-- Lean 4 proof step from Mathlib.Topology.Order (goal)
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
⊢ s ∈ update (β := fun (a : α) ↦ Filter α) pure a l b
have h₁ : Membership.mem (γ := Filter α) (pure b) s
Tactic: rwa [update_of_ne hb]
-- Lean 4 proof step from Mathlib.Topology.Order (goal)
Goal:
α : Type u
s : Set (Set α)
hs : {u : Set α | GenerateOpen s u} = s
⊢ Eq.{u + 1} (α := Set α → Prop) IsOpen[TopologicalSpace.mkOfClosure s hs] IsOpen[generateFrom s]
have h : ∀ (U : Set α), IsOpen[TopologicalSpace.mkOfClosure s hs] U ↔ IsOpen[generateFrom s] U
Tactic: ext U
-- Lean 4 proof step from Mathlib.Topology.Order (goal)
Goal:
α : Type u_1
t₂ : TopologicalSpace α
inst : IndiscreteTopology α
U : Set α
⊢ IsOpen[t₂] U ↔ U = ∅ ∨ U = univ
have refl : ∀ [IndiscreteTopology α], IsOpen[⊤] U ↔ U = ∅ ∨ U = univ
Tactic: cases IndiscreteTopology.eq_top α
Cleared hypotheses: t₂, inst
-- Lean 4 proof step from Mathlib.Topology.Order (goal)
Goal:
α : Type u_1
U : Set α
inst : IndiscreteTopology α
⊢ IsOpen[⊤] U ↔ U = ∅ ∨ U = univ
have refl : ∀ (h : IsOpen[⊤] U), U = ∅ ∨ U = univ
Tactic: refine ⟨fun h => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Order (goal)
Goal:
α : Type u_1
U : Set α
inst : IndiscreteTopology α
refl : ∀ (h : IsOpen[⊤] U), U = ∅ ∨ U = univ
⊢ IsOpen[⊤] U ↔ U = ∅ ∨ U = univ
have refl₁ : U = ∅ ∨ U = univ → IsOpen[⊤] U
Tactic: refine ⟨fun h => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Order (goal)
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
⊢ s ∩ t = ∅ ∨ s ∩ t = univ
have refl : TopologicalSpace.GenerateOpen.{u_1} (α := α) ((OrderDual.ofDual : (a : (Set (Set α))ᵒᵈ) → Set (Set α)) ⊤) ∅ →
  ∅ ∩ t = ∅ ∨ ∅ ∩ t = univ
Tactic: rcases h₁ with (rfl | rfl)
Cleared hypotheses: s, h, h₁
-- Lean 4 proof step from Mathlib.Topology.Order (goal)
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
⊢ s ∩ t = ∅ ∨ s ∩ t = univ
have refl₁ : TopologicalSpace.GenerateOpen.{u_1} (α := α) ((OrderDual.ofDual : (a : (Set (Set α))ᵒᵈ) → Set (Set α)) ⊤) univ →
  univ ∩ t = ∅ ∨ univ ∩ t = univ
Tactic: rcases h₁ with (rfl | rfl)
Cleared hypotheses: s, h, h₁
-- Lean 4 proof step from Mathlib.Topology.Order (goal)
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 α)) ⊤) ∅
⊢ ∅ ∩ t = ∅ ∨ ∅ ∩ t = univ
have refl : TopologicalSpace.GenerateOpen.{u_1} (α := α) ((OrderDual.ofDual : (a : (Set (Set α))ᵒᵈ) → Set (Set α)) ⊤) ∅ →
  Eq.{u_1 + 1} (α := Set α) (∅ ∩ ∅) ∅ ∨ Eq.{u_1 + 1} (α := Set α) (∅ ∩ ∅) univ
Tactic: rcases h₂ with (rfl | rfl)
Cleared hypotheses: t, h, h₂
-- Lean 4 proof step from Mathlib.Topology.Order (goal)
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
⊢ ∅ ∩ t = ∅ ∨ ∅ ∩ t = univ
have 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
Tactic: rcases h₂ with (rfl | rfl)
Cleared hypotheses: t, h, h₂
-- Lean 4 proof step from Mathlib.Topology.Order (goal)
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
⊢ univ ∩ t = ∅ ∨ univ ∩ t = univ
have 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
Tactic: rcases h₂ with (rfl | rfl)
Cleared hypotheses: t, h, h₂
-- Lean 4 proof step from Mathlib.Topology.Order (goal)
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
⊢ univ ∩ t = ∅ ∨ univ ∩ t = univ
have 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
Tactic: rcases h₂ with (rfl | rfl)
Cleared hypotheses: t, h, h₂
-- Lean 4 proof step from Mathlib.Topology.Order (goal)
Goal:
α : Type u_1
U : Set α
inst : IndiscreteTopology α
h : IsOpen[⊤] U
⊢ U = ∅ ∨ U = univ
have refl : ∀ (s : Set α)
  (h : Membership.mem (γ := Set (Set α)) ((OrderDual.ofDual : (a : (Set (Set α))ᵒᵈ) → Set (Set α)) ⊤ : Set (Set α)) s),
  s = ∅ ∨ s = univ
Tactic: induction h with
    | basic _ h => exact False.elim h
    | univ => exact .inr rfl
    | inter _ _ _ _ h₁ h₂ =>
      rcases h₁ with (rfl | rfl) <;> rcases h₂ with (rfl | rfl) <;> simp
    | sUnion _ _ ih => exact sUnion_mem_empty_univ ih
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Order (goal)
Goal:
α : Type u_1
U : Set α
inst : IndiscreteTopology α
h : IsOpen[⊤] U
refl :
  ∀ (s : Set α)
    (h :
      Membership.mem (γ := Set (Set α)) ((OrderDual.ofDual : (a : (Set (Set α))ᵒᵈ) → Set (Set α)) ⊤ : Set (Set α)) s),
    s = ∅ ∨ s = univ
⊢ U = ∅ ∨ U = univ
have refl₁ : Eq.{u_1 + 1} (α := Set α) univ ∅ ∨ Eq.{u_1 + 1} (α := Set α) univ univ
Tactic: induction h with
    | basic _ h => exact False.elim h
    | univ => exact .inr rfl
    | inter _ _ _ _ h₁ h₂ =>
      rcases h₁ with (rfl | rfl) <;> rcases h₂ with (rfl | rfl) <;> simp
    | sUnion _ _ ih => exact sUnion_mem_empty_univ ih
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Order (goal)
Goal:
α : Type u_1
U : Set α
inst : IndiscreteTopology α
h : IsOpen[⊤] U
refl :
  ∀ (s : Set α)
    (h :
      Membership.mem (γ := Set (Set α)) ((OrderDual.ofDual : (a : (Set (Set α))ᵒᵈ) → Set (Set α)) ⊤ : Set (Set α)) s),
    s = ∅ ∨ s = univ
refl₁ : Eq.{u_1 + 1} (α := Set α) univ ∅ ∨ Eq.{u_1 + 1} (α := Set α) univ univ
⊢ U = ∅ ∨ U = univ
have refl₂ : ∀ (s t : Set α),
  TopologicalSpace.GenerateOpen ((OrderDual.ofDual : (a : (Set (Set α))ᵒᵈ) → Set (Set α)) ⊤) s →
    TopologicalSpace.GenerateOpen ((OrderDual.ofDual : (a : (Set (Set α))ᵒᵈ) → Set (Set α)) ⊤) t →
      ∀ (h₁ : s = ∅ ∨ s = univ) (h₂ : t = ∅ ∨ t = univ), s ∩ t = ∅ ∨ s ∩ t = univ
Tactic: induction h with
    | basic _ h => exact False.elim h
    | univ => exact .inr rfl
    | inter _ _ _ _ h₁ h₂ =>
      rcases h₁ with (rfl | rfl) <;> rcases h₂ with (rfl | rfl) <;> simp
    | sUnion _ _ ih => exact sUnion_mem_empty_univ ih
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Order (goal)
Goal:
α : Type u_1
U : Set α
inst : IndiscreteTopology α
h : IsOpen[⊤] U
refl :
  ∀ (s : Set α)
    (h :
      Membership.mem (γ := Set (Set α)) ((OrderDual.ofDual : (a : (Set (Set α))ᵒᵈ) → Set (Set α)) ⊤ : Set (Set α)) s),
    s = ∅ ∨ s = univ
refl₁ : Eq.{u_1 + 1} (α := Set α) univ ∅ ∨ Eq.{u_1 + 1} (α := Set α) univ univ
refl₂ :
  ∀ (s t : Set α),
    TopologicalSpace.GenerateOpen ((OrderDual.ofDual : (a : (Set (Set α))ᵒᵈ) → Set (Set α)) ⊤) s →
      TopologicalSpace.GenerateOpen ((OrderDual.ofDual : (a : (Set (Set α))ᵒᵈ) → Set (Set α)) ⊤) t →
        ∀ (h₁ : s = ∅ ∨ s = univ) (h₂ : t = ∅ ∨ t = univ), s ∩ t = ∅ ∨ s ∩ t = univ
⊢ U = ∅ ∨ U = univ
have refl₃ : ∀ (S : Set (Set α)),
  (∀ s ∈ S, TopologicalSpace.GenerateOpen ((OrderDual.ofDual : (a : (Set (Set α))ᵒᵈ) → Set (Set α)) ⊤) s) →
    ∀ (ih : ∀ s ∈ S, s = ∅ ∨ s = univ), ⋃₀ S = ∅ ∨ ⋃₀ S = univ
Tactic: induction h with
    | basic _ h => exact False.elim h
    | univ => exact .inr rfl
    | inter _ _ _ _ h₁ h₂ =>
      rcases h₁ with (rfl | rfl) <;> rcases h₂ with (rfl | rfl) <;> simp
    | sUnion _ _ ih => exact sUnion_mem_empty_univ ih
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Order (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : DiscreteTopology α
ι : Type u_3
f : ι → α
⊢ DenseRange f ↔ Surjective f
have rw : Dense (range f) ↔ Surjective f
Tactic: rw [DenseRange, dense_discrete, range_eq_univ]
-- Lean 4 proof step from Mathlib.Topology.Order (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : DiscreteTopology α
ι : Type u_3
f : ι → α
rw : Dense (range f) ↔ Surjective f
⊢ DenseRange f ↔ Surjective f
have rw₁ : range f = univ ↔ Surjective f
Tactic: rw [DenseRange, dense_discrete, range_eq_univ]
-- Lean 4 proof step from Mathlib.Topology.Order (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : DiscreteTopology α
ι : Type u_3
f : ι → α
rw : Dense (range f) ↔ Surjective f
rw₁ : range f = univ ↔ Surjective f
⊢ DenseRange f ↔ Surjective f
have rw₂ : Surjective f ↔ Surjective f
Tactic: rw [DenseRange, dense_discrete, range_eq_univ]
-- Lean 4 proof step from Mathlib.Topology.Order (goal)
Goal:
β : Type u_2
α : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : DiscreteTopology β
f : α → β
h : ∀ (b : β), IsOpen[inst] (f ⁻¹' {b})
s : Set β
h_1 : IsOpen[inst_1] s
⊢ IsOpen[inst] (f ⁻¹' s)
have rw : IsOpen[inst] (⋃ i ∈ s, f ⁻¹' {i})
Tactic: rw [← biUnion_of_singleton s, preimage_iUnion₂]
-- Lean 4 proof step from Mathlib.Topology.Order (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : DiscreteTopology α
x : α
s : Set α
⊢ s ∈ 𝓝 x ↔ x ∈ s
have rw : Membership.mem (γ := Filter α) (pure x) s ↔ x ∈ s
Tactic: rw [nhds_discrete, mem_pure]
-- Lean 4 proof step from Mathlib.Topology.Order (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : DiscreteTopology α
x : α
s : Set α
rw : Membership.mem (γ := Filter α) (pure x) s ↔ x ∈ s
⊢ s ∈ 𝓝 x ↔ x ∈ s
have rw₁ : x ∈ s ↔ x ∈ s
Tactic: rw [nhds_discrete, mem_pure]
-- Lean 4 proof step from Mathlib.Topology.Order (goal)
Goal:
α : Type u_1
t₁ t₂ : TopologicalSpace α
h : ∀ (x : α), 𝓝 x ≤ 𝓝 x
s : Set α
⊢ IsOpen[t₂] s → IsOpen[t₁] s
have rw : (∀ x ∈ s, s ∈ 𝓝 x) → ∀ x ∈ s, s ∈ 𝓝 x
Tactic: rw [@isOpen_iff_mem_nhds _ t₁, @isOpen_iff_mem_nhds _ t₂]
-- Lean 4 proof step from Mathlib.Topology.Order (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
⊢ DiscreteTopology α ↔ ∀ (x : α), 𝓝 x = pure x
have simp : (∀ (x : α), {x} ∈ 𝓝 x) ↔ ∀ (x : α), 𝓝 x = pure x
Tactic: simp only [discreteTopology_iff_singleton_mem_nhds]
-- Lean 4 proof step from Mathlib.Topology.Order (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
⊢ (∀ (x : α), {x} ∈ 𝓝 x) ↔ ∀ (x : α), 𝓝 x = pure x
have apply : ∀ (x : α), {x} ∈ 𝓝 x ↔ 𝓝 x = pure x
Tactic: apply forall_congr' (fun x ↦ ?_)
-- Lean 4 proof step from Mathlib.Topology.Order (goal)
Goal:
α : Type u_1
β : Type u_2
t : TopologicalSpace β
s : Set α
f : α → β
this : TopologicalSpace α := TopologicalSpace.induced f t
⊢ IsClosed[TopologicalSpace.induced f t] s ↔ ∃ (t_1 : Set β), IsClosed[t] t_1 ∧ f ⁻¹' t_1 = s
have simp : (∃ (t_1 : Set β), IsOpen[t] t_1 ∧ f ⁻¹' t_1 = sᶜ) ↔ ∃ (t_1 : Set β), IsOpen[t] t_1ᶜ ∧ f ⁻¹' t_1 = s
Tactic: simp only [← isOpen_compl_iff, isOpen_induced_iff]
-- Lean 4 proof step from Mathlib.Topology.Order (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
π : α → β
s : Set β
a : α
hs : s ∈ 𝓝 (π a)
this : TopologicalSpace β := TopologicalSpace.coinduced π inst
⊢ π ⁻¹' s ∈ 𝓝 a
have rcases : ∀ (V : Set β) (hVs : V ⊆ s) (V_op : IsOpen[TopologicalSpace.coinduced π inst] V) (mem_V : π a ∈ V), π ⁻¹' s ∈ 𝓝 a
Tactic: rcases mem_nhds_iff.mp hs with ⟨V, hVs, V_op, mem_V⟩
-- Lean 4 proof step from Mathlib.Topology.Order (goal)
Goal:
α : Type u_1
β : Type u_2
g : β → α
s : Set (TopologicalSpace α)
⊢ TopologicalSpace.induced g (sInf s) = sInf (TopologicalSpace.induced g '' s)
have rw : TopologicalSpace.induced g (⨅ (a : (↑s : Type u_1)), (↑a : TopologicalSpace α)) = sInf (TopologicalSpace.induced g '' s)
Tactic: rw [sInf_eq_iInf', sInf_image', induced_iInf]
-- Lean 4 proof step from Mathlib.Topology.Order (goal)
Goal:
α : Type u_1
β : Type u_2
g : β → α
s : Set (TopologicalSpace α)
rw :
  TopologicalSpace.induced g (⨅ (a : (↑s : Type u_1)), (↑a : TopologicalSpace α)) =
    sInf (TopologicalSpace.induced g '' s)
⊢ TopologicalSpace.induced g (sInf s) = sInf (TopologicalSpace.induced g '' s)
have rw₁ : TopologicalSpace.induced g (⨅ (a : (↑s : Type u_1)), (↑a : TopologicalSpace α)) =
  ⨅ (a : (↑s : Type u_1)), TopologicalSpace.induced g (↑a : TopologicalSpace α)
Tactic: rw [sInf_eq_iInf', sInf_image', induced_iInf]
-- Lean 4 proof step from Mathlib.Topology.Order (goal)
Goal:
α : Type u_1
β : Type u_2
g : β → α
s : Set (TopologicalSpace α)
rw :
  TopologicalSpace.induced g (⨅ (a : (↑s : Type u_1)), (↑a : TopologicalSpace α)) =
    sInf (TopologicalSpace.induced g '' s)
rw₁ :
  TopologicalSpace.induced g (⨅ (a : (↑s : Type u_1)), (↑a : TopologicalSpace α)) =
    ⨅ (a : (↑s : Type u_1)), TopologicalSpace.induced g (↑a : TopologicalSpace α)
⊢ TopologicalSpace.induced g (sInf s) = sInf (TopologicalSpace.induced g '' s)
have rw₂ : Eq.{u_2 + 1} (α := TopologicalSpace β) (⨅ (i : (↑s : Type u_1)), TopologicalSpace.induced g (↑i : TopologicalSpace α))
  (⨅ (a : (↑s : Type u_1)), TopologicalSpace.induced g (↑a : TopologicalSpace α))
Tactic: rw [sInf_eq_iInf', sInf_image', induced_iInf]