awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Sequences (goal)
Goal:
X : Type u_1
inst : UniformSpace X
s : Set X
inst_1 : (𝓤 X).IsCountablyGenerated
hs : IsSeqCompact s
l : Filter X
hl : Cauchy l
hls : l ≤ 𝓟 s
this : l.NeBot
V : ℕ → Set (X × X)
hV : (𝓤 X).HasAntitoneBasis V
W : (n : ℕ) → Set (X × X)
hW : ∀ (n : ℕ), W n ∈ 𝓤 X
hWV : ∀ (n : ℕ), SetRel.comp (W n) (W n) ⊆ V n
hWV' : ∀ (n : ℕ), W n ⊆ V n
t : ℕ → Set X
ht_anti : Antitone t
htl : ∀ (n : ℕ), t n ∈ l
htW : ∀ (n : ℕ), t n ×ˢ t n ⊆ W n
hts : ∀ (n : ℕ), t n ⊆ s
⊢ ∃ x ∈ s, l ≤ 𝓝 x
have choose : ∀ (u : (n : ℕ) → X) (hu : ∀ (n : ℕ), u n ∈ t n), ∃ x ∈ s, l ≤ 𝓝 x
Tactic: choose u hu using fun n => Filter.nonempty_of_mem (htl n)
-- Lean 4 proof step from Mathlib.Topology.Sequences (hypothesis)
Goal:
X : Type u_1
inst : UniformSpace X
s : Set X
inst_1 : (𝓤 X).IsCountablyGenerated
hs : IsSeqCompact s
l : Filter X
hl : Cauchy l
hls : l ≤ 𝓟 s
this : l.NeBot
V : ℕ → Set (X × X)
hV : (𝓤 X).HasAntitoneBasis V
W : (n : ℕ) → Set (X × X)
hW : ∀ (n : ℕ), W n ∈ 𝓤 X
hWV : ∀ (n : ℕ), SetRel.comp (W n) (W n) ⊆ V n
hWV' : ∀ (n : ℕ), W n ⊆ V n
t : ℕ → Set X
ht_anti : Antitone t
htl : ∀ (n : ℕ), t n ∈ l
htW : ∀ (n : ℕ), t n ×ˢ t n ⊆ W n
hts : ∀ (n : ℕ), t n ⊆ s
u : (n : ℕ) → X
hu : ∀ (n : ℕ), u n ∈ t n
⊢ ∃ x ∈ s, l ≤ 𝓝 x
have huc : CauchySeq u
Tactic: have huc : CauchySeq u := hV.toHasBasis.cauchySeq_iff.2 fun N _ =>
      ⟨N, fun m hm n hn => hWV' _ <| @htW N (_, _) ⟨ht_anti hm (hu _), ht_anti hn (hu _)⟩⟩
-- Lean 4 proof step from Mathlib.Topology.Sequences (goal)
Goal:
X : Type u_1
inst : UniformSpace X
s : Set X
inst_1 : (𝓤 X).IsCountablyGenerated
hs : IsSeqCompact s
l : Filter X
hl : Cauchy l
hls : l ≤ 𝓟 s
this : l.NeBot
V : ℕ → Set (X × X)
hV : (𝓤 X).HasAntitoneBasis V
W : (n : ℕ) → Set (X × X)
hW : ∀ (n : ℕ), W n ∈ 𝓤 X
hWV : ∀ (n : ℕ), SetRel.comp (W n) (W n) ⊆ V n
hWV' : ∀ (n : ℕ), W n ⊆ V n
t : ℕ → Set X
ht_anti : Antitone t
htl : ∀ (n : ℕ), t n ∈ l
htW : ∀ (n : ℕ), t n ×ˢ t n ⊆ W n
hts : ∀ (n : ℕ), t n ⊆ s
u : (n : ℕ) → X
hu : ∀ (n : ℕ), u n ∈ t n
huc : CauchySeq u
⊢ ∃ x ∈ s, l ≤ 𝓝 x
have rcases : ∀ (x : X) (hxs : x ∈ s) (hx : Tendsto u atTop (𝓝 x)), ∃ x ∈ s, l ≤ 𝓝 x
Tactic: rcases hs.exists_tendsto (fun n => hts n (hu n)) huc with ⟨x, hxs, hx⟩
-- Lean 4 proof step from Mathlib.Topology.Sequences (goal)
Goal:
X : Type u_1
inst : UniformSpace X
s : Set X
inst_1 : (𝓤 X).IsCountablyGenerated
hs : IsSeqCompact s
l : Filter X
hl : Cauchy l
hls : l ≤ 𝓟 s
this : l.NeBot
V : ℕ → Set (X × X)
hV : (𝓤 X).HasAntitoneBasis V
W : (n : ℕ) → Set (X × X)
hW : ∀ (n : ℕ), W n ∈ 𝓤 X
hWV : ∀ (n : ℕ), SetRel.comp (W n) (W n) ⊆ V n
hWV' : ∀ (n : ℕ), W n ⊆ V n
t : ℕ → Set X
ht_anti : Antitone t
htl : ∀ (n : ℕ), t n ∈ l
htW : ∀ (n : ℕ), t n ×ˢ t n ⊆ W n
hts : ∀ (n : ℕ), t n ⊆ s
u : (n : ℕ) → X
hu : ∀ (n : ℕ), u n ∈ t n
huc : CauchySeq u
x : X
hxs : x ∈ s
hx : Tendsto u atTop (𝓝 x)
⊢ ∃ x ∈ s, l ≤ 𝓝 x
have refine : ∀ (N : ℕ), True → ball x (V N) ∈ l
Tactic: refine ⟨x, hxs, (nhds_basis_uniformity' hV.toHasBasis).ge_iff.2 fun N _ => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Sequences (goal)
Goal:
X : Type u_1
inst : UniformSpace X
s : Set X
inst_1 : (𝓤 X).IsCountablyGenerated
hs : IsSeqCompact s
l : Filter X
hl : Cauchy l
hls : l ≤ 𝓟 s
this : l.NeBot
V : ℕ → Set (X × X)
hV : (𝓤 X).HasAntitoneBasis V
W : (n : ℕ) → Set (X × X)
hW : ∀ (n : ℕ), W n ∈ 𝓤 X
hWV : ∀ (n : ℕ), SetRel.comp (W n) (W n) ⊆ V n
hWV' : ∀ (n : ℕ), W n ⊆ V n
t : ℕ → Set X
ht_anti : Antitone t
htl : ∀ (n : ℕ), t n ∈ l
htW : ∀ (n : ℕ), t n ×ˢ t n ⊆ W n
hts : ∀ (n : ℕ), t n ⊆ s
u : (n : ℕ) → X
hu : ∀ (n : ℕ), u n ∈ t n
huc : CauchySeq u
x : X
hxs : x ∈ s
hx : Tendsto u atTop (𝓝 x)
N : ℕ
h : True
⊢ ball x (V N) ∈ l
have obtain : ∀ (n : ℕ) (hNn : N ≤ n) (hn : u n ∈ ball x (W N)), ball x (V N) ∈ l
Tactic: obtain ⟨n, hNn, hn⟩ : ∃ n, N ≤ n ∧ u n ∈ ball x (W N) :=
    ((eventually_ge_atTop N).and (hx <| ball_mem_nhds x (hW N))).exists
-- Lean 4 proof step from Mathlib.Topology.Sequences (goal)
Goal:
X : Type u_1
inst : UniformSpace X
s : Set X
inst_1 : (𝓤 X).IsCountablyGenerated
hs : IsSeqCompact s
l : Filter X
hl : Cauchy l
hls : l ≤ 𝓟 s
this : l.NeBot
V : ℕ → Set (X × X)
hV : (𝓤 X).HasAntitoneBasis V
W : (n : ℕ) → Set (X × X)
hW : ∀ (n : ℕ), W n ∈ 𝓤 X
hWV : ∀ (n : ℕ), SetRel.comp (W n) (W n) ⊆ V n
hWV' : ∀ (n : ℕ), W n ⊆ V n
t : ℕ → Set X
ht_anti : Antitone t
htl : ∀ (n : ℕ), t n ∈ l
htW : ∀ (n : ℕ), t n ×ˢ t n ⊆ W n
hts : ∀ (n : ℕ), t n ⊆ s
u : (n : ℕ) → X
hu : ∀ (n : ℕ), u n ∈ t n
huc : CauchySeq u
x : X
hxs : x ∈ s
hx : Tendsto u atTop (𝓝 x)
N : ℕ
h : True
n : ℕ
hNn : N ≤ n
hn : u n ∈ ball x (W N)
⊢ ball x (V N) ∈ l
have refine : ∀ (y : X) (hy : y ∈ t n), (u n, y) ∈ t N ×ˢ t N
Tactic: refine mem_of_superset (htl n) fun y hy => hWV N ⟨u n, hn, htW N ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Sets.Closeds (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s t : Closeds α
h : s.carrier = t.carrier
⊢ s = t
have mk : ∀ (carrier : Set α) (isClosed' : IsClosed[inst] carrier)
  (h : { carrier := carrier, isClosed' := isClosed' : Closeds α }.carrier = t.carrier),
  { carrier := carrier, isClosed' := isClosed' : Closeds α } = t
Tactic: cases s
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.Topology.Sets.Closeds (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
t : Closeds α
carrier : Set α
isClosed' : IsClosed[inst] carrier
h : { carrier := carrier, isClosed' := isClosed' : Closeds α }.carrier = t.carrier
⊢ { carrier := carrier, isClosed' := isClosed' : Closeds α } = t
have mk : ∀ (carrier_1 : Set α) (isClosed'_1 : IsClosed[inst] carrier_1)
  (h :
    { carrier := carrier, isClosed' := isClosed' : Closeds α }.carrier =
      { carrier := carrier_1, isClosed' := isClosed'_1 : Closeds α }.carrier),
  { carrier := carrier, isClosed' := isClosed' : Closeds α } = { carrier := carrier_1, isClosed' := isClosed'_1 }
Tactic: cases t
Cleared hypotheses: t, h
-- Lean 4 proof step from Mathlib.Topology.Sets.Closeds (goal)
Goal:
α : Type u_2
inst : TopologicalSpace α
ι : Sort u_4
s : ι → Closeds α
⊢ (↑(⨅ (i : ι), s i) : Set α) = ⋂ (i : ι), (↑(s i) : Set α)
have h : ∀ (x : α), x ∈ (↑(⨅ (i : ι), s i) : Set α) ↔ Membership.mem (γ := Set α) (⋂ (i : ι), (↑(s i) : Set α)) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Sets.Closeds (goal)
Goal:
α : Type u_2
inst : TopologicalSpace α
ι : Sort u_4
s : ι → Closeds α
⊢ Eq.{u_2 + 1} (α := Closeds α) (⨅ (i : ι), s i) { carrier := ⋂ (i : ι), (↑(s i) : Set α), isClosed' := ⋯ }
have h : (↑(⨅ (i : ι), s i) : Set α) = (↑{ carrier := ⋂ (i : ι), (↑(s i) : Set α), isClosed' := sorry } : Set α)
Tactic: ext1
-- Lean 4 proof step from Mathlib.Topology.Sets.Closeds (goal)
Goal:
α : Type u_2
inst : TopologicalSpace α
inst_1 : T0Space α
s : Closeds α
hs : IsAtom s
⊢ ∃ (a : α), (↑s : Set α) = {a}
have refine : ∀ (t : Set α) (hts : t ⊆ (↑s : Set α)) (ht : t.Nonempty) (ht' : IsClosed[inst] t), t = (↑s : Set α)
Tactic: refine minimal_nonempty_closed_eq_singleton s.2 (coe_nonempty.2 hs.1) fun t hts ht ht' ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Sets.Closeds (goal)
Goal:
α : Type u_2
inst : TopologicalSpace α
inst_1 : T0Space α
s : Closeds α
hs : IsAtom s
t : Set α
hts : t ⊆ (↑s : Set α)
ht : t.Nonempty
ht' : IsClosed[inst] t
⊢ t = (↑s : Set α)
have lift : ∀ (t : Closeds α) (hts : (↑t : Set α) ⊆ (↑s : Set α)) (ht : (↑t : Set α).Nonempty), (↑t : Set α) = (↑s : Set α)
Tactic: lift t to Closeds α using ht'
Cleared hypotheses: t, hts, ht, ht'
-- Lean 4 proof step from Mathlib.Topology.Sets.Closeds (goal)
Goal:
α : Type u_2
inst : TopologicalSpace α
inst_1 : T1Space α
s : Closeds α
t : Set α
ht : IsAtom t
⊢ (↑(Closeds.closure t) : Set α) = t
have obtain : ∀ (x : α) (ht : IsAtom (α := Set α) {x}), (↑(Closeds.closure {x}) : Set α) = {x}
Tactic: obtain ⟨x, rfl⟩ := Set.isAtom_iff.1 ht
Cleared hypotheses: t, ht
-- Lean 4 proof step from Mathlib.Topology.Sets.Closeds (goal)
Goal:
α : Type u_2
inst : TopologicalSpace α
inst_1 : T1Space α
s : Opens α
⊢ IsCoatom s ↔ ∃ (x : α), s = Closeds.compl {x}
have rw : IsAtom (α := (Opens α)ᵒᵈ) ((toDual : (a : Opens α) → (Opens α)ᵒᵈ) s.compl.compl : (Opens α)ᵒᵈ) ↔
  ∃ (x : α), s.compl.compl = Closeds.compl {x}
Tactic: rw [← s.compl_compl, ← isAtom_dual_iff_isCoatom]
-- Lean 4 proof step from Mathlib.Topology.Sets.Closeds (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s t : Clopens α
h : Eq.{u_2 + 1} (α := Set α) ((fun (s : Clopens α) ↦ s.carrier) s) ((fun (s : Clopens α) ↦ s.carrier) t)
⊢ s = t
have mk : ∀ (carrier : Set α) (isClopen' : IsClopen carrier)
  (h :
    Eq.{u_2 + 1} (α := Set α) ((fun (s : Clopens α) ↦ s.carrier) { carrier := carrier, isClopen' := isClopen' })
      ((fun (s : Clopens α) ↦ s.carrier) t)),
  { carrier := carrier, isClopen' := isClopen' : Clopens α } = t
Tactic: cases s
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.Topology.Sets.Closeds (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
t : Clopens α
carrier : Set α
isClopen' : IsClopen carrier
h :
  Eq.{u_2 + 1} (α := Set α) ((fun (s : Clopens α) ↦ s.carrier) { carrier := carrier, isClopen' := isClopen' })
    ((fun (s : Clopens α) ↦ s.carrier) t)
⊢ { carrier := carrier, isClopen' := isClopen' : Clopens α } = t
have mk : ∀ (carrier_1 : Set α) (isClopen'_1 : IsClopen carrier_1)
  (h :
    Eq.{u_2 + 1} (α := Set α) ((fun (s : Clopens α) ↦ s.carrier) { carrier := carrier, isClopen' := isClopen' })
      ((fun (s : Clopens α) ↦ s.carrier) { carrier := carrier_1, isClopen' := isClopen'_1 })),
  { carrier := carrier, isClopen' := isClopen' : Clopens α } = { carrier := carrier_1, isClopen' := isClopen'_1 }
Tactic: cases t
Cleared hypotheses: t, h
-- Lean 4 proof step from Mathlib.Topology.Sets.Closeds (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : TopologicalSpace α
s : Finset ι
U : ι → Clopens α
⊢ (↑(s.sup U) : Set α) = ⋃ i ∈ s, (↑(U i) : Set α)
have empty : (↑(Finset.sup ∅ U) : Set α) = ⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Finset ι) ∅ i), (↑(U i) : Set α)
Tactic: induction s using Finset.induction_on with
  | empty => simp
  | insert _ _ _ IH => simp [IH]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Topology.Sets.Closeds (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : TopologicalSpace α
s : Finset ι
U : ι → Clopens α
empty : (↑(Finset.sup ∅ U) : Set α) = ⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Finset ι) ∅ i), (↑(U i) : Set α)
⊢ (↑(s.sup U) : Set α) = ⋃ i ∈ s, (↑(U i) : Set α)
have insert : ∀ (a : ι) (s : Finset ι),
  a ∉ s →
    ∀ (IH : (↑(s.sup U) : Set α) = ⋃ i ∈ s, (↑(U i) : Set α)),
      (↑((insert a s).sup U) : Set α) = ⋃ i ∈ insert a s, (↑(U i) : Set α)
Tactic: induction s using Finset.induction_on with
  | empty => simp
  | insert _ _ _ IH => simp [IH]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Topology.Sets.Closeds (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : TopologicalSpace α
s : Finset ι
U : ι → Clopens α
⊢ (↑(s.sup U) : Set α) = ⋃ i ∈ s, (↑(U i) : Set α)
have empty : (↑(Finset.sup ∅ U) : Set α) = ⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Finset ι) ∅ i), (↑(U i) : Set α)
Tactic: classical
  induction s using Finset.induction_on with
  | empty => simp
  | insert _ _ _ IH => simp [IH]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Topology.Sets.Closeds (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : TopologicalSpace α
s : Finset ι
U : ι → Clopens α
empty : (↑(Finset.sup ∅ U) : Set α) = ⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Finset ι) ∅ i), (↑(U i) : Set α)
⊢ (↑(s.sup U) : Set α) = ⋃ i ∈ s, (↑(U i) : Set α)
have insert : ∀ (a : ι) (s : Finset ι),
  a ∉ s →
    ∀ (IH : (↑(s.sup U) : Set α) = ⋃ i ∈ s, (↑(U i) : Set α)),
      (↑((insert a s).sup U) : Set α) = ⋃ i ∈ insert a s, (↑(U i) : Set α)
Tactic: classical
  induction s using Finset.induction_on with
  | empty => simp
  | insert _ _ _ IH => simp [IH]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Topology.Sets.Closeds (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s t : IrreducibleCloseds α
h : s.carrier = t.carrier
⊢ s = t
have mk : ∀ (carrier : Set α) (isIrreducible' : IsIrreducible carrier) (isClosed' : IsClosed[inst] carrier)
  (h :
    { carrier := carrier, isIrreducible' := isIrreducible', isClosed' := isClosed' : IrreducibleCloseds α }.carrier =
      t.carrier),
  { carrier := carrier, isIrreducible' := isIrreducible', isClosed' := isClosed' : IrreducibleCloseds α } = t
Tactic: cases s
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.Topology.Sets.Closeds (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
t : IrreducibleCloseds α
carrier : Set α
isIrreducible' : IsIrreducible carrier
isClosed' : IsClosed[inst] carrier
h :
  { carrier := carrier, isIrreducible' := isIrreducible', isClosed' := isClosed' : IrreducibleCloseds α }.carrier =
    t.carrier
⊢ { carrier := carrier, isIrreducible' := isIrreducible', isClosed' := isClosed' : IrreducibleCloseds α } = t
have mk : ∀ (carrier_1 : Set α) (isIrreducible'_1 : IsIrreducible carrier_1) (isClosed'_1 : IsClosed[inst] carrier_1)
  (h :
    { carrier := carrier, isIrreducible' := isIrreducible', isClosed' := isClosed' : IrreducibleCloseds α }.carrier =
      { carrier := carrier_1, isIrreducible' := isIrreducible'_1, isClosed' := isClosed'_1 :
          IrreducibleCloseds α }.carrier),
  { carrier := carrier, isIrreducible' := isIrreducible', isClosed' := isClosed' : IrreducibleCloseds α } =
    { carrier := carrier_1, isIrreducible' := isIrreducible'_1, isClosed' := isClosed'_1 }
Tactic: cases t
Cleared hypotheses: t, h
-- Lean 4 proof step from Mathlib.Topology.Sets.Closeds (goal)
Goal:
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : β → α
hf : IsInducing f
A B : IrreducibleCloseds β
h_images_eq : map f ⋯ A = map f ⋯ B
⊢ A = B
have a : (↑A : Set β) = (↑B : Set β)
Tactic: apply SetLike.coe_injective
-- Lean 4 proof step from Mathlib.Topology.Sets.Closeds (hypothesis)
Goal:
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : β → α
hf : IsInducing f
A B : IrreducibleCloseds β
h_images_eq : map f ⋯ A = map f ⋯ B
⊢ (↑A : Set β) = (↑B : Set β)
have h_images_eq₁ : closure[inst] (f '' (↑A : Set β)) = closure[inst] (f '' (↑B : Set β))
Tactic: replace h_images_eq : closure (f '' A) = closure (f '' B) := congr($h_images_eq)
Cleared hypotheses: h_images_eq
-- Lean 4 proof step from Mathlib.Topology.Sets.Closeds (goal)
Goal:
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : β → α
hf : IsInducing f
A B : IrreducibleCloseds β
h_images_eq : closure[inst] (f '' (↑A : Set β)) = closure[inst] (f '' (↑B : Set β))
⊢ (↑A : Set β) = (↑B : Set β)
have a : closure[inst_1] (↑A : Set β) = (↑B : Set β)
Tactic: rw [← A.isClosed.closure_eq, hf.closure_eq_preimage_closure_image, h_images_eq,
    ← hf.closure_eq_preimage_closure_image, B.isClosed.closure_eq]
-- Lean 4 proof step from Mathlib.Topology.Sets.Closeds (goal)
Goal:
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : β → α
hf : IsInducing f
A B : IrreducibleCloseds β
h_images_eq : closure[inst] (f '' (↑A : Set β)) = closure[inst] (f '' (↑B : Set β))
a : closure[inst_1] (↑A : Set β) = (↑B : Set β)
⊢ (↑A : Set β) = (↑B : Set β)
have a₁ : f ⁻¹' closure[inst] (f '' (↑A : Set β)) = (↑B : Set β)
Tactic: rw [← A.isClosed.closure_eq, hf.closure_eq_preimage_closure_image, h_images_eq,
    ← hf.closure_eq_preimage_closure_image, B.isClosed.closure_eq]
-- Lean 4 proof step from Mathlib.Topology.Sets.Closeds (goal)
Goal:
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : β → α
hf : IsInducing f
A B : IrreducibleCloseds β
h_images_eq : closure[inst] (f '' (↑A : Set β)) = closure[inst] (f '' (↑B : Set β))
a : closure[inst_1] (↑A : Set β) = (↑B : Set β)
a₁ : f ⁻¹' closure[inst] (f '' (↑A : Set β)) = (↑B : Set β)
⊢ (↑A : Set β) = (↑B : Set β)
have a₂ : f ⁻¹' closure[inst] (f '' (↑B : Set β)) = (↑B : Set β)
Tactic: rw [← A.isClosed.closure_eq, hf.closure_eq_preimage_closure_image, h_images_eq,
    ← hf.closure_eq_preimage_closure_image, B.isClosed.closure_eq]
-- Lean 4 proof step from Mathlib.Topology.Sets.Closeds (goal)
Goal:
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : β → α
hf : IsInducing f
A B : IrreducibleCloseds β
h_images_eq : closure[inst] (f '' (↑A : Set β)) = closure[inst] (f '' (↑B : Set β))
a : closure[inst_1] (↑A : Set β) = (↑B : Set β)
a₁ : f ⁻¹' closure[inst] (f '' (↑A : Set β)) = (↑B : Set β)
a₂ : f ⁻¹' closure[inst] (f '' (↑B : Set β)) = (↑B : Set β)
⊢ (↑A : Set β) = (↑B : Set β)
have a₃ : closure[inst_1] (↑B : Set β) = (↑B : Set β)
Tactic: rw [← A.isClosed.closure_eq, hf.closure_eq_preimage_closure_image, h_images_eq,
    ← hf.closure_eq_preimage_closure_image, B.isClosed.closure_eq]
-- Lean 4 proof step from Mathlib.Topology.Sets.Closeds (goal)
Goal:
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : β → α
hf : IsInducing f
A B : IrreducibleCloseds β
h_images_eq : closure[inst] (f '' (↑A : Set β)) = closure[inst] (f '' (↑B : Set β))
a : closure[inst_1] (↑A : Set β) = (↑B : Set β)
a₁ : f ⁻¹' closure[inst] (f '' (↑A : Set β)) = (↑B : Set β)
a₂ : f ⁻¹' closure[inst] (f '' (↑B : Set β)) = (↑B : Set β)
a₃ : closure[inst_1] (↑B : Set β) = (↑B : Set β)
⊢ (↑A : Set β) = (↑B : Set β)
have a₄ : (↑B : Set β) = (↑B : Set β)
Tactic: rw [← A.isClosed.closure_eq, hf.closure_eq_preimage_closure_image, h_images_eq,
    ← hf.closure_eq_preimage_closure_image, B.isClosed.closure_eq]
-- Lean 4 proof step from Mathlib.Topology.Sets.Closeds (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : β → α
h : IsOpenEmbedding f
V : IrreducibleCloseds β
⊢ (fun (V : (↑{V : IrreducibleCloseds α | (f ⁻¹' (↑V : Set α)).Nonempty} : Type u_2)) ↦
        { carrier := f ⁻¹' (↑(↑V : IrreducibleCloseds α) : Set α), isIrreducible' := ⋯, isClosed' := ⋯ :
          IrreducibleCloseds β })
      ((fun (T : IrreducibleCloseds β) ↦
          (Subtype.mk (p := fun (x : IrreducibleCloseds α) ↦
              Membership.mem (γ := Set (IrreducibleCloseds α))
                {V : IrreducibleCloseds α | (f ⁻¹' (↑V : Set α)).Nonempty} x)
              (map f ⋯ T) ⋯ :
            { x : IrreducibleCloseds α //
              Membership.mem (γ := Set (IrreducibleCloseds α))
                {V : IrreducibleCloseds α | (f ⁻¹' (↑V : Set α)).Nonempty} x }))
        V) =
    V
have h₁ : ∀ (x : β),
  x ∈
      (↑((fun (V : (↑{V : IrreducibleCloseds α | (f ⁻¹' (↑V : Set α)).Nonempty} : Type u_2)) ↦
              { carrier := f ⁻¹' (↑(↑V : IrreducibleCloseds α) : Set α), isIrreducible' := sorry, isClosed' := sorry :
                IrreducibleCloseds β })
            ((fun (T : IrreducibleCloseds β) ↦
                (Subtype.mk (p := fun (x : IrreducibleCloseds α) ↦
                    Membership.mem (γ := Set (IrreducibleCloseds α))
                      {V : IrreducibleCloseds α | (f ⁻¹' (↑V : Set α)).Nonempty} x)
                    (map f sorry T) sorry :
                  { x : IrreducibleCloseds α //
                    Membership.mem (γ := Set (IrreducibleCloseds α))
                      {V : IrreducibleCloseds α | (f ⁻¹' (↑V : Set α)).Nonempty} x }))
              V)) :
        Set β) ↔
    x ∈ (↑V : Set β)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Sets.Closeds (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : β → α
h : IsOpenEmbedding f
V : (↑{V : IrreducibleCloseds α | (f ⁻¹' (↑V : Set α)).Nonempty} : Type u_2)
⊢ (fun (T : IrreducibleCloseds β) ↦
        (Subtype.mk (p := fun (x : IrreducibleCloseds α) ↦
            Membership.mem (γ := Set (IrreducibleCloseds α)) {V : IrreducibleCloseds α | (f ⁻¹' (↑V : Set α)).Nonempty}
              x)
            (map f ⋯ T) ⋯ :
          { x : IrreducibleCloseds α //
            Membership.mem (γ := Set (IrreducibleCloseds α)) {V : IrreducibleCloseds α | (f ⁻¹' (↑V : Set α)).Nonempty}
              x }))
      ((fun (V : (↑{V : IrreducibleCloseds α | (f ⁻¹' (↑V : Set α)).Nonempty} : Type u_2)) ↦
          { carrier := f ⁻¹' (↑(↑V : IrreducibleCloseds α) : Set α), isIrreducible' := ⋯, isClosed' := ⋯ :
            IrreducibleCloseds β })
        V) =
    V
have a : ∀ (x : α),
  x ∈
      (↑(↑((fun (T : IrreducibleCloseds β) ↦
                  (Subtype.mk (p := fun (x : IrreducibleCloseds α) ↦
                      Membership.mem (γ := Set (IrreducibleCloseds α))
                        {V : IrreducibleCloseds α | (f ⁻¹' (↑V : Set α)).Nonempty} x)
                      (map f sorry T) sorry :
                    { x : IrreducibleCloseds α //
                      Membership.mem (γ := Set (IrreducibleCloseds α))
                        {V : IrreducibleCloseds α | (f ⁻¹' (↑V : Set α)).Nonempty} x }))
                ((fun (V : (↑{V : IrreducibleCloseds α | (f ⁻¹' (↑V : Set α)).Nonempty} : Type u_2)) ↦
                    { carrier := f ⁻¹' (↑(↑V : IrreducibleCloseds α) : Set α), isIrreducible' := sorry, isClosed' := sorry :
                      IrreducibleCloseds β })
                  V)) :
            IrreducibleCloseds α) :
        Set α) ↔
    x ∈ (↑(↑V : IrreducibleCloseds α) : Set α)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Sets.CompactOpenCovered (goal)
Goal:
S : Type u_1
ι : Type u_2
X : ι → Type u_3
f : (i : ι) → X i → S
inst : (i : ι) → TopologicalSpace (X i)
U : Set S
inst_1 : Unique ι
⊢ IsCompactOpenCovered (X := X) f U ↔ ∃ (V : Opens (X default)), IsCompact V.carrier ∧ f default '' V.carrier = U
have refine_1 : IsCompactOpenCovered (X := X) f U →
  ∀ (s : Set ι) (hs : s.Finite) (V : (i : ι) → i ∈ s → Opens (X i))
    (hc : ∀ (i : ι) (h : i ∈ s), IsCompact (V i h).carrier)
    (hcov : ⋃ (i : ι), ⋃ (h : i ∈ s), f i '' (↑(V i h) : Set (X i)) = U),
    ∃ (V : Opens (X default)), IsCompact V.carrier ∧ f default '' V.carrier = U
Tactic: refine ⟨fun ⟨s, hs, V, hc, hcov⟩ ↦ ?_, fun ⟨V, hc, h⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Sets.CompactOpenCovered (goal)
Goal:
S : Type u_1
ι : Type u_2
X : ι → Type u_3
f : (i : ι) → X i → S
inst : (i : ι) → TopologicalSpace (X i)
U : Set S
inst_1 : Unique ι
refine_1 :
  IsCompactOpenCovered (X := X) f U →
    ∀ (s : Set ι) (hs : s.Finite) (V : (i : ι) → i ∈ s → Opens (X i))
      (hc : ∀ (i : ι) (h : i ∈ s), IsCompact (V i h).carrier)
      (hcov : ⋃ (i : ι), ⋃ (h : i ∈ s), f i '' (↑(V i h) : Set (X i)) = U),
      ∃ (V : Opens (X default)), IsCompact V.carrier ∧ f default '' V.carrier = U
⊢ IsCompactOpenCovered (X := X) f U ↔ ∃ (V : Opens (X default)), IsCompact V.carrier ∧ f default '' V.carrier = U
have refine_2 : (∃ (V : Opens (X default)), IsCompact V.carrier ∧ f default '' V.carrier = U) →
  ∀ (V : Opens (X default)) (hc : IsCompact V.carrier) (h : f default '' V.carrier = U),
    IsCompactOpenCovered (X := X) f U
Tactic: refine ⟨fun ⟨s, hs, V, hc, hcov⟩ ↦ ?_, fun ⟨V, hc, h⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Sets.CompactOpenCovered (goal)
Goal:
S : Type u_1
ι : Type u_2
X : ι → Type u_3
f : (i : ι) → X i → S
inst : (i : ι) → TopologicalSpace (X i)
U : Set S
inst_1 : Unique ι
h : IsCompactOpenCovered (X := X) f U
s : Set ι
hs : s.Finite
V : (i : ι) → i ∈ s → Opens (X i)
hc : ∀ (i : ι) (h : i ∈ s), IsCompact (V i h).carrier
hcov : ⋃ (i : ι), ⋃ (h : i ∈ s), f i '' (↑(V i h) : Set (X i)) = U
⊢ ∃ (V : Opens (X default)), IsCompact V.carrier ∧ f default '' V.carrier = U
have refine_1 : s = ∅ → ∃ (V : Opens (X default)), IsCompact V.carrier ∧ f default '' V.carrier = U
Tactic: cases s.eq_empty_or_singleton_of_unique