awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Compactification.StoneCech (hypothesis)
Goal:
α : Type u
inst : TopologicalSpace α
β : Type v
inst_1 : TopologicalSpace β
inst_2 : T2Space β
inst_3 : CompactSpace β
g : α → β
hg : Continuous[inst, inst_1] g
F G : Ultrafilter α
x : α
hF : (↑F : Filter α) ≤ 𝓝 x
hG : (↑G : Filter α) ≤ 𝓝 x
⊢ Ultrafilter.extend g F = Ultrafilter.extend g G
have hF₁ : map g (↑F : Filter α) ≤ 𝓝 (g x)
Tactic: replace hF := (map_mono hF).trans hg.continuousAt
Cleared hypotheses: hF
-- Lean 4 proof step from Mathlib.Topology.Compactification.StoneCech (hypothesis)
Goal:
α : Type u
inst : TopologicalSpace α
β : Type v
inst_1 : TopologicalSpace β
inst_2 : T2Space β
inst_3 : CompactSpace β
g : α → β
hg : Continuous[inst, inst_1] g
F G : Ultrafilter α
x : α
hG : (↑G : Filter α) ≤ 𝓝 x
hF : map g (↑F : Filter α) ≤ 𝓝 (g x)
⊢ Ultrafilter.extend g F = Ultrafilter.extend g G
have hG₁ : map g (↑G : Filter α) ≤ 𝓝 (g x)
Tactic: replace hG := (map_mono hG).trans hg.continuousAt
Cleared hypotheses: hG
-- Lean 4 proof step from Mathlib.Topology.Compactification.StoneCech (goal)
Goal:
α : Type u
inst : TopologicalSpace α
β : Type v
inst_1 : TopologicalSpace β
inst_2 : T2Space β
inst_3 : CompactSpace β
g : α → β
hg : Continuous[inst, inst_1] g
F G : Ultrafilter α
x : α
hF : map g (↑F : Filter α) ≤ 𝓝 (g x)
hG : map g (↑G : Filter α) ≤ 𝓝 (g x)
⊢ Ultrafilter.extend g G = g x
have rwa : (↑(Ultrafilter.map g G) : Filter β) ≤ 𝓝 (g x)
Tactic: rwa [ultrafilter_extend_eq_iff, G.coe_map]
-- Lean 4 proof step from Mathlib.Topology.Compactification.StoneCech (goal)
Goal:
α : Type u
inst : TopologicalSpace α
β : Type v
inst_1 : TopologicalSpace β
inst_2 : T2Space β
inst_3 : CompactSpace β
g : α → β
hg : Continuous[inst, inst_1] g
F G : Ultrafilter α
x : α
hF : map g (↑F : Filter α) ≤ 𝓝 (g x)
hG : map g (↑G : Filter α) ≤ 𝓝 (g x)
⊢ Ultrafilter.extend g F = Ultrafilter.extend g G
have rwa : Ultrafilter.extend g F = g x
Tactic: rwa [show Ultrafilter.extend g G = g x by rwa [ultrafilter_extend_eq_iff, G.coe_map],
       ultrafilter_extend_eq_iff, F.coe_map]
-- Lean 4 proof step from Mathlib.Topology.Compactification.StoneCech (goal)
Goal:
α : Type u
inst : TopologicalSpace α
β : Type v
inst_1 : TopologicalSpace β
inst_2 : T2Space β
inst_3 : CompactSpace β
g : α → β
hg : Continuous[inst, inst_1] g
F G : Ultrafilter α
x : α
hF : map g (↑F : Filter α) ≤ 𝓝 (g x)
hG : map g (↑G : Filter α) ≤ 𝓝 (g x)
rwa : Ultrafilter.extend g F = g x
⊢ Ultrafilter.extend g F = Ultrafilter.extend g G
have rwa₁ : (↑(Ultrafilter.map g F) : Filter β) ≤ 𝓝 (g x)
Tactic: rwa [show Ultrafilter.extend g G = g x by rwa [ultrafilter_extend_eq_iff, G.coe_map],
       ultrafilter_extend_eq_iff, F.coe_map]
-- Lean 4 proof step from Mathlib.Topology.Compactification.StoneCech (hypothesis)
Goal:
α : Type u
inst : TopologicalSpace α
β : Type v
inst_1 : TopologicalSpace β
inst_2 : T2Space β
inst_3 : CompactSpace β
g : α → β
hg : Continuous[inst, inst_1] g
a b : α
h : Eq (α := PreStoneCech α) (preStoneCechUnit a) (preStoneCechUnit b)
⊢ g a = g b
have e : Ultrafilter.extend g ∘ pure = g
Tactic: have e := ultrafilter_extend_extends g
-- Lean 4 proof step from Mathlib.Topology.Compactification.StoneCech (goal)
Goal:
α : Type u
inst : TopologicalSpace α
β : Type v
inst_1 : TopologicalSpace β
inst_2 : T2Space β
inst_3 : CompactSpace β
g : α → β
hg : Continuous[inst, inst_1] g
a b : α
h : Eq (α := PreStoneCech α) (preStoneCechUnit a) (preStoneCechUnit b)
e : Ultrafilter.extend g ∘ pure = g
⊢ g a = g b
have rw : Ultrafilter.extend g (pure a) = Ultrafilter.extend g (pure b)
Tactic: rw [← congrFun e a, ← congrFun e b, Function.comp_apply, Function.comp_apply]
-- Lean 4 proof step from Mathlib.Topology.Compactification.StoneCech (hypothesis)
Goal:
α : Type u
inst : TopologicalSpace α
β : Type v
inst_1 : TopologicalSpace β
inst_2 : T2Space β
inst_3 : CompactSpace β
g : α → β
hg : Continuous[inst, inst_1] g
a b : α
h : Eq (α := PreStoneCech α) (preStoneCechUnit a) (preStoneCechUnit b)
e : Ultrafilter.extend g ∘ pure = g
⊢ Ultrafilter.extend g (pure a) = Ultrafilter.extend g (pure b)
have h₁ : Relation.EqvGen (fun (F G : Ultrafilter α) ↦ ∃ (x : α), (↑F : Filter α) ≤ 𝓝 x ∧ (↑G : Filter α) ≤ 𝓝 x) (pure a) (pure b)
Tactic: rw [preStoneCechUnit, preStoneCechUnit, Quot.eq] at h
Cleared hypotheses: h, e
-- Lean 4 proof step from Mathlib.Topology.Compactification.StoneCech (goal)
Goal:
α : Type u
inst : TopologicalSpace α
β : Type v
inst_1 : TopologicalSpace β
inst_2 : T2Space β
inst_3 : CompactSpace β
g : α → β
hg : Continuous[inst, inst_1] g
a b : α
h :
  Relation.EqvGen (fun (F G : Ultrafilter α) ↦ ∃ (x : α), (↑F : Filter α) ≤ 𝓝 x ∧ (↑G : Filter α) ≤ 𝓝 x) (pure a)
    (pure b)
e : Ultrafilter.extend g ∘ pure = g
⊢ Ultrafilter.extend g (pure a) = Ultrafilter.extend g (pure b)
have generalize : ∀ (F : Ultrafilter α)
  (h :
    Relation.EqvGen (fun (F G : Ultrafilter α) ↦ ∃ (x : α), (↑F : Filter α) ≤ 𝓝 x ∧ (↑G : Filter α) ≤ 𝓝 x) F (pure b)),
  Ultrafilter.extend g F = Ultrafilter.extend g (pure b)
Tactic: generalize (pure a : Ultrafilter α) = F at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Compactification.StoneCech (goal)
Goal:
α : Type u
inst : TopologicalSpace α
β : Type v
inst_1 : TopologicalSpace β
inst_2 : T2Space β
inst_3 : CompactSpace β
g : α → β
hg : Continuous[inst, inst_1] g
a b : α
e : Ultrafilter.extend g ∘ pure = g
F : Ultrafilter α
h : Relation.EqvGen (fun (F G : Ultrafilter α) ↦ ∃ (x : α), (↑F : Filter α) ≤ 𝓝 x ∧ (↑G : Filter α) ≤ 𝓝 x) F (pure b)
⊢ Ultrafilter.extend g F = Ultrafilter.extend g (pure b)
have generalize : ∀ (G : Ultrafilter α)
  (h : Relation.EqvGen (fun (F G : Ultrafilter α) ↦ ∃ (x : α), (↑F : Filter α) ≤ 𝓝 x ∧ (↑G : Filter α) ≤ 𝓝 x) F G),
  Ultrafilter.extend g F = Ultrafilter.extend g G
Tactic: generalize (pure b : Ultrafilter α) = G at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Compactification.StoneCech (goal)
Goal:
α : Type u
inst : TopologicalSpace α
β : Type v
inst_1 : TopologicalSpace β
inst_2 : T2Space β
inst_3 : CompactSpace β
g : α → β
hg : Continuous[inst, inst_1] g
a b : α
e : Ultrafilter.extend g ∘ pure = g
F G x y : Ultrafilter α
h_1 : Relation.EqvGen (fun (F G : Ultrafilter α) ↦ ∃ (x : α), (↑F : Filter α) ≤ 𝓝 x ∧ (↑G : Filter α) ≤ 𝓝 x) x y
h : Ultrafilter.extend g x = Ultrafilter.extend g y
⊢ Ultrafilter.extend g y = Ultrafilter.extend g x
have symm : Ultrafilter.extend g y = Ultrafilter.extend g y
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Topology.Compactification.StoneCech (goal)
Goal:
α : Type u
inst : TopologicalSpace α
β : Type v
inst_1 : TopologicalSpace β
inst_2 : T2Space β
inst_3 : CompactSpace β
g : α → β
hg : Continuous[inst, inst_1] g
a b : α
e : Ultrafilter.extend g ∘ pure = g
F G : Ultrafilter α
h : Relation.EqvGen (fun (F G : Ultrafilter α) ↦ ∃ (x : α), (↑F : Filter α) ≤ 𝓝 x ∧ (↑G : Filter α) ≤ 𝓝 x) F G
⊢ Ultrafilter.extend g F = Ultrafilter.extend g G
have rel : ∀ (x y : Ultrafilter α) (a : ∃ (x_1 : α), (↑x : Filter α) ≤ 𝓝 x_1 ∧ (↑y : Filter α) ≤ 𝓝 x_1),
  Ultrafilter.extend g x = Ultrafilter.extend g y
Tactic: induction h with
  | rel x y a => exact let ⟨a, hx, hy⟩ := a; preStoneCechCompat hg hx hy
  | refl x => rfl
  | symm x y _ h => rw [h]
  | trans x y z _ _ h h' => exact h.trans h'
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Compactification.StoneCech (goal)
Goal:
α : Type u
inst : TopologicalSpace α
β : Type v
inst_1 : TopologicalSpace β
inst_2 : T2Space β
inst_3 : CompactSpace β
g : α → β
hg : Continuous[inst, inst_1] g
a b : α
e : Ultrafilter.extend g ∘ pure = g
F G : Ultrafilter α
h : Relation.EqvGen (fun (F G : Ultrafilter α) ↦ ∃ (x : α), (↑F : Filter α) ≤ 𝓝 x ∧ (↑G : Filter α) ≤ 𝓝 x) F G
rel :
  ∀ (x y : Ultrafilter α) (a : ∃ (x_1 : α), (↑x : Filter α) ≤ 𝓝 x_1 ∧ (↑y : Filter α) ≤ 𝓝 x_1),
    Ultrafilter.extend g x = Ultrafilter.extend g y
⊢ Ultrafilter.extend g F = Ultrafilter.extend g G
have refl : ∀ (x : Ultrafilter α), Ultrafilter.extend g x = Ultrafilter.extend g x
Tactic: induction h with
  | rel x y a => exact let ⟨a, hx, hy⟩ := a; preStoneCechCompat hg hx hy
  | refl x => rfl
  | symm x y _ h => rw [h]
  | trans x y z _ _ h h' => exact h.trans h'
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Compactification.StoneCech (goal)
Goal:
α : Type u
inst : TopologicalSpace α
β : Type v
inst_1 : TopologicalSpace β
inst_2 : T2Space β
inst_3 : CompactSpace β
g : α → β
hg : Continuous[inst, inst_1] g
a b : α
e : Ultrafilter.extend g ∘ pure = g
F G : Ultrafilter α
h : Relation.EqvGen (fun (F G : Ultrafilter α) ↦ ∃ (x : α), (↑F : Filter α) ≤ 𝓝 x ∧ (↑G : Filter α) ≤ 𝓝 x) F G
rel :
  ∀ (x y : Ultrafilter α) (a : ∃ (x_1 : α), (↑x : Filter α) ≤ 𝓝 x_1 ∧ (↑y : Filter α) ≤ 𝓝 x_1),
    Ultrafilter.extend g x = Ultrafilter.extend g y
refl : ∀ (x : Ultrafilter α), Ultrafilter.extend g x = Ultrafilter.extend g x
⊢ Ultrafilter.extend g F = Ultrafilter.extend g G
have symm : ∀ (x y : Ultrafilter α),
  Relation.EqvGen (fun (F G : Ultrafilter α) ↦ ∃ (x : α), (↑F : Filter α) ≤ 𝓝 x ∧ (↑G : Filter α) ≤ 𝓝 x) x y →
    ∀ (h : Ultrafilter.extend g x = Ultrafilter.extend g y), Ultrafilter.extend g y = Ultrafilter.extend g x
Tactic: induction h with
  | rel x y a => exact let ⟨a, hx, hy⟩ := a; preStoneCechCompat hg hx hy
  | refl x => rfl
  | symm x y _ h => rw [h]
  | trans x y z _ _ h h' => exact h.trans h'
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Compactification.StoneCech (goal)
Goal:
α : Type u
inst : TopologicalSpace α
β : Type v
inst_1 : TopologicalSpace β
inst_2 : T2Space β
inst_3 : CompactSpace β
g : α → β
hg : Continuous[inst, inst_1] g
a b : α
e : Ultrafilter.extend g ∘ pure = g
F G : Ultrafilter α
h : Relation.EqvGen (fun (F G : Ultrafilter α) ↦ ∃ (x : α), (↑F : Filter α) ≤ 𝓝 x ∧ (↑G : Filter α) ≤ 𝓝 x) F G
rel :
  ∀ (x y : Ultrafilter α) (a : ∃ (x_1 : α), (↑x : Filter α) ≤ 𝓝 x_1 ∧ (↑y : Filter α) ≤ 𝓝 x_1),
    Ultrafilter.extend g x = Ultrafilter.extend g y
refl : ∀ (x : Ultrafilter α), Ultrafilter.extend g x = Ultrafilter.extend g x
symm :
  ∀ (x y : Ultrafilter α),
    Relation.EqvGen (fun (F G : Ultrafilter α) ↦ ∃ (x : α), (↑F : Filter α) ≤ 𝓝 x ∧ (↑G : Filter α) ≤ 𝓝 x) x y →
      ∀ (h : Ultrafilter.extend g x = Ultrafilter.extend g y), Ultrafilter.extend g y = Ultrafilter.extend g x
⊢ Ultrafilter.extend g F = Ultrafilter.extend g G
have trans : ∀ (x y z : Ultrafilter α),
  Relation.EqvGen (fun (F G : Ultrafilter α) ↦ ∃ (x : α), (↑F : Filter α) ≤ 𝓝 x ∧ (↑G : Filter α) ≤ 𝓝 x) x y →
    Relation.EqvGen (fun (F G : Ultrafilter α) ↦ ∃ (x : α), (↑F : Filter α) ≤ 𝓝 x ∧ (↑G : Filter α) ≤ 𝓝 x) y z →
      ∀ (h : Ultrafilter.extend g x = Ultrafilter.extend g y) (h' : Ultrafilter.extend g y = Ultrafilter.extend g z),
        Ultrafilter.extend g x = Ultrafilter.extend g z
Tactic: induction h with
  | rel x y a => exact let ⟨a, hx, hy⟩ := a; preStoneCechCompat hg hx hy
  | refl x => rfl
  | symm x y _ h => rw [h]
  | trans x y z _ _ h h' => exact h.trans h'
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Compactification.StoneCech (hypothesis)
Goal:
α : Type u
inst : TopologicalSpace α
⊢ DenseRange (X := StoneCech α) fun (x : α) ↦ ⟦preStoneCechUnit x⟧
have this : Function.Surjective.{u + 1, u + 1} (α := PreStoneCech α) (β := T2Quotient (PreStoneCech α)) T2Quotient.mk
Tactic: have : Function.Surjective (T2Quotient.mk : PreStoneCech α → StoneCech α) := by
    exact Quot.mk_surjective
-- Lean 4 proof step from Mathlib.Topology.Compactification.StoneCech (goal)
Goal:
α : Type u
inst : TopologicalSpace α
β : Type v
inst_1 : TopologicalSpace β
inst_2 : T2Space β
g₁ g₂ : StoneCech α → β
h₁ : Continuous[_, inst_1] g₁
h₂ : Continuous[_, inst_1] g₂
h : g₁ ∘ stoneCechUnit = g₂ ∘ stoneCechUnit
⊢ g₁ = g₂
have apply : EqOn g₁ g₂ (range stoneCechUnit)
Tactic: apply h₁.ext_on denseRange_stoneCechUnit h₂
-- Lean 4 proof step from Mathlib.Topology.Compactification.StoneCech (goal)
Goal:
α : Type u
inst : TopologicalSpace α
β : Type v
inst_1 : TopologicalSpace β
inst_2 : T2Space β
g : α → β
hg : Continuous[inst, inst_1] g
inst_3 : CompactSpace β
⊢ stoneCechExtend hg ∘ stoneCechUnit = g
have h : ∀ (x : α), (stoneCechExtend hg ∘ stoneCechUnit) x = g x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.Compactification.StoneCech (goal)
Goal:
α : Type u
inst : TopologicalSpace α
β : Type v
inst_1 : TopologicalSpace β
inst_2 : T2Space β
inst_3 : CompactSpace β
a b : α
f : α → β
hcf : Continuous[inst, inst_1] f
h : Eq (α := StoneCech α) (stoneCechUnit a) (stoneCechUnit b)
⊢ f a = f b
have rw : (stoneCechExtend hcf ∘ stoneCechUnit) a = (stoneCechExtend hcf ∘ stoneCechUnit) b
Tactic: rw [← congrFun (stoneCechExtend_extends hcf), ← congrFun (stoneCechExtend_extends hcf)]
-- Lean 4 proof step from Mathlib.Topology.Compactness.Bases (goal)
Goal:
X : Type u_1
ι : Type u_2
inst : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
U : Set X
hUc : IsCompact U
hUo : IsOpen U
⊢ ∃ (s : Set ι), s.Finite ∧ U = ⋃ i ∈ s, b i
have obtain : ∀ (Y : Type u_1) (f : Y → Set X) (e : U = ⋃ (i : Y), f i) (hf : ∀ (i : Y), f i ∈ range b),
  ∃ (s : Set ι), s.Finite ∧ U = ⋃ i ∈ s, b i
Tactic: obtain ⟨Y, f, e, hf⟩ := hb.open_eq_iUnion hUo
-- Lean 4 proof step from Mathlib.Topology.Compactness.Bases (goal)
Goal:
X : Type u_1
ι : Type u_2
inst : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
U : Set X
hUc : IsCompact U
hUo : IsOpen U
Y : Type u_1
f : Y → Set X
e : U = ⋃ (i : Y), f i
hf : ∀ (i : Y), f i ∈ range b
⊢ ∃ (s : Set ι), s.Finite ∧ U = ⋃ i ∈ s, b i
have choose : ∀ (f' : (i : Y) → ι) (hf' : ∀ (i : Y), b (f' i) = f i), ∃ (s : Set ι), s.Finite ∧ U = ⋃ i ∈ s, b i
Tactic: choose f' hf' using hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Topology.Compactness.Bases (hypothesis)
Goal:
X : Type u_1
ι : Type u_2
inst : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
U : Set X
hUc : IsCompact U
hUo : IsOpen U
Y : Type u_1
f : Y → Set X
e : U = ⋃ (i : Y), f i
f' : (i : Y) → ι
hf' : ∀ (i : Y), b (f' i) = f i
⊢ ∃ (s : Set ι), s.Finite ∧ U = ⋃ i ∈ s, b i
have this : b ∘ f' = f
Tactic: have : b ∘ f' = f := funext hf'
-- Lean 4 proof step from Mathlib.Topology.Compactness.Bases (hypothesis)
Goal:
X : Type u_1
ι : Type u_2
inst : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
U : Set X
hUc : IsCompact U
hUo : IsOpen U
Y : Type u_1
f : Y → Set X
e : U = ⋃ (i : Y), f i
f' : (i : Y) → ι
hf' : ∀ (i : Y), b (f' i) = f i
this : b ∘ f' = f
⊢ ∃ (s : Set ι), s.Finite ∧ U = ⋃ i ∈ s, b i
have e₁ : U = ⋃ (i : Y), (b ∘ f') i
Tactic: subst this
Cleared hypotheses: f, e, hf', this
-- Lean 4 proof step from Mathlib.Topology.Compactness.Bases (hypothesis)
Goal:
X : Type u_1
ι : Type u_2
inst : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
U : Set X
hUc : IsCompact U
hUo : IsOpen U
Y : Type u_1
f : Y → Set X
e : U = ⋃ (i : Y), f i
f' : (i : Y) → ι
hf' : ∀ (i : Y), b (f' i) = f i
this : b ∘ f' = f
e₁ : U = ⋃ (i : Y), (b ∘ f') i
⊢ ∃ (s : Set ι), s.Finite ∧ U = ⋃ i ∈ s, b i
have hf'₁ : ∀ (i : Y), b (f' i) = (b ∘ f') i
Tactic: subst this
Cleared hypotheses: f, e, hf', this
-- Lean 4 proof step from Mathlib.Topology.Compactness.Bases (goal)
Goal:
X : Type u_1
ι : Type u_2
inst : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
U : Set X
hUc : IsCompact U
hUo : IsOpen U
Y : Type u_1
f' : (i : Y) → ι
e : U = ⋃ (i : Y), (b ∘ f') i
hf' : ∀ (i : Y), b (f' i) = (b ∘ f') i
⊢ U ⊆ ⋃ (i : Y), (b ∘ f') i
have rw : Subset.{u_1} (α := Set X) (⋃ (i : Y), (b ∘ f') i) (⋃ (i : Y), (b ∘ f') i)
Tactic: rw [e]
-- Lean 4 proof step from Mathlib.Topology.Compactness.Bases (goal)
Goal:
X : Type u_1
ι : Type u_2
inst : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
U : Set X
hUc : IsCompact U
hUo : IsOpen U
Y : Type u_1
f' : (i : Y) → ι
e : U = ⋃ (i : Y), (b ∘ f') i
hf' : ∀ (i : Y), b (f' i) = (b ∘ f') i
⊢ ∃ (s : Set ι), s.Finite ∧ U = ⋃ i ∈ s, b i
have obtain : ∀ (t : Finset Y) (ht : U ⊆ ⋃ i ∈ t, (b ∘ f') i), ∃ (s : Set ι), s.Finite ∧ U = ⋃ i ∈ s, b i
Tactic: obtain ⟨t, ht⟩ :=
    hUc.elim_finite_subcover (b ∘ f') (fun i => hb.isOpen (Set.mem_range_self _)) (by rw [e])
-- Lean 4 proof step from Mathlib.Topology.Compactness.Bases (goal)
Goal:
X : Type u_1
ι : Type u_2
inst : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
U : Set X
hUc : IsCompact U
hUo : IsOpen U
Y : Type u_1
f' : (i : Y) → ι
e : U = ⋃ (i : Y), (b ∘ f') i
hf' : ∀ (i : Y), b (f' i) = (b ∘ f') i
t : Finset Y
ht : U ⊆ ⋃ i ∈ t, (b ∘ f') i
⊢ ∃ (s : Set ι), s.Finite ∧ U = ⋃ i ∈ s, b i
have refine_1 : U ≤ ⋃ i ∈ (↑(Finset.image f' t) : Set ι), b i
Tactic: refine ⟨t.image f', Set.toFinite _, le_antisymm ?_ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.Bases (goal)
Goal:
X : Type u_1
ι : Type u_2
inst : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
U : Set X
hUc : IsCompact U
hUo : IsOpen U
Y : Type u_1
f' : (i : Y) → ι
e : U = ⋃ (i : Y), (b ∘ f') i
hf' : ∀ (i : Y), b (f' i) = (b ∘ f') i
t : Finset Y
ht : U ⊆ ⋃ i ∈ t, (b ∘ f') i
refine_1 : U ≤ ⋃ i ∈ (↑(Finset.image f' t) : Set ι), b i
⊢ ∃ (s : Set ι), s.Finite ∧ U = ⋃ i ∈ s, b i
have refine_2 : ⋃ i ∈ (↑(Finset.image f' t) : Set ι), b i ≤ U
Tactic: refine ⟨t.image f', Set.toFinite _, le_antisymm ?_ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.Bases (goal)
Goal:
X : Type u_1
ι : Type u_2
inst : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
U : Set X
hUc : IsCompact U
hUo : IsOpen U
Y : Type u_1
f' : (i : Y) → ι
e : U = ⋃ (i : Y), (b ∘ f') i
hf' : ∀ (i : Y), b (f' i) = (b ∘ f') i
t : Finset Y
ht : U ⊆ ⋃ i ∈ t, (b ∘ f') i
⊢ U ≤ ⋃ i ∈ (↑(Finset.image f' t) : Set ι), b i
have refine_1 : Subset.{u_1} (α := Set X) (⋃ i ∈ t, (b ∘ f') i) (⋃ i ∈ (↑(Finset.image f' t) : Set ι), b i)
Tactic: refine Set.Subset.trans ht ?_
-- Lean 4 proof step from Mathlib.Topology.Compactness.Bases (goal)
Goal:
X : Type u_1
ι : Type u_2
inst : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
U : Set X
hUc : IsCompact U
hUo : IsOpen U
Y : Type u_1
f' : (i : Y) → ι
e : U = ⋃ (i : Y), (b ∘ f') i
hf' : ∀ (i : Y), b (f' i) = (b ∘ f') i
t : Finset Y
ht : U ⊆ ⋃ i ∈ t, (b ∘ f') i
⊢ Subset.{u_1} (α := Set X) (⋃ i ∈ t, (b ∘ f') i) (⋃ i ∈ (↑(Finset.image f' t) : Set ι), b i)
have refine_1 : ∀ (i : Y) (i_1 : i ∈ t), (b ∘ f') i ⊆ ⋃ i ∈ (↑(Finset.image f' t) : Set ι), b i
Tactic: simp only [Set.iUnion_subset_iff]
-- Lean 4 proof step from Mathlib.Topology.Compactness.Bases (goal)
Goal:
X : Type u_1
ι : Type u_2
inst : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
U : Set X
hUc : IsCompact U
hUo : IsOpen U
Y : Type u_1
f' : (i : Y) → ι
e : U = ⋃ (i : Y), (b ∘ f') i
hf' : ∀ (i : Y), b (f' i) = (b ∘ f') i
t : Finset Y
ht : U ⊆ ⋃ i ∈ t, (b ∘ f') i
⊢ ⋃ i ∈ (↑(Finset.image f' t) : Set ι), b i ≤ U
have refine_2 : ∀ (i : ι) (j : i ∈ (↑(Finset.image f' t) : Set ι)), b i ⊆ U
Tactic: apply Set.iUnion₂_subset
-- Lean 4 proof step from Mathlib.Topology.Compactness.Bases (goal)
Goal:
X : Type u_1
ι : Type u_2
inst : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
U : Set X
hUc : IsCompact U
hUo : IsOpen U
Y : Type u_1
f' : (i : Y) → ι
e : U = ⋃ (i : Y), (b ∘ f') i
hf' : ∀ (i : Y), b (f' i) = (b ∘ f') i
t : Finset Y
ht : U ⊆ ⋃ i ∈ t, (b ∘ f') i
i : ι
hi : i ∈ (↑(Finset.image f' t) : Set ι)
⊢ b i ⊆ U
have refine_2 : ∀ (j : Y) (hi : f' j ∈ (↑(Finset.image f' t) : Set ι)), b (f' j) ⊆ U
Tactic: obtain ⟨j, -, rfl⟩ := Finset.mem_image.mp hi
Cleared hypotheses: i, hi
-- Lean 4 proof step from Mathlib.Topology.Compactness.Bases (goal)
Goal:
X : Type u_1
ι : Type u_2
inst : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
U : Set X
hUc : IsCompact U
hUo : IsOpen U
Y : Type u_1
f' : (i : Y) → ι
e : U = ⋃ (i : Y), (b ∘ f') i
hf' : ∀ (i : Y), b (f' i) = (b ∘ f') i
t : Finset Y
ht : U ⊆ ⋃ i ∈ t, (b ∘ f') i
j : Y
hi : f' j ∈ (↑(Finset.image f' t) : Set ι)
⊢ b (f' j) ⊆ U
have refine_2 : b (f' j) ⊆ ⋃ (i : Y), (b ∘ f') i
Tactic: rw [e]
-- Lean 4 proof step from Mathlib.Topology.Compactness.Bases (goal)
Goal:
X : Type u_1
ι : Type u_2
inst : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
U : Set X
hUc : IsCompact U
hUo : IsOpen U
Y : Type u_1
f' : (i : Y) → ι
e : U = ⋃ (i : Y), (b ∘ f') i
hf' : ∀ (i : Y), b (f' i) = (b ∘ f') i
t : Finset Y
ht : U ⊆ ⋃ i ∈ t, (b ∘ f') i
⊢ ∃ (s : Set ι), s.Finite ∧ U = ⋃ i ∈ s, b i
have refine_1 : U ≤ ⋃ i ∈ (↑(Finset.image f' t) : Set ι), b i
Tactic: classical
  refine ⟨t.image f', Set.toFinite _, le_antisymm ?_ ?_⟩
  · refine Set.Subset.trans ht ?_
    simp only [Set.iUnion_subset_iff]
    intro i hi
    simpa using subset_iUnion₂ (s := fun i _ => b (f' i)) i hi
  · apply Set.iUnion₂_subset
    rintro i hi
    obtain ⟨j, -, rfl⟩ := Finset.mem_image.mp hi
    rw [e]
    exact Set.subset_iUnion (b ∘ f') j
-- Lean 4 proof step from Mathlib.Topology.Compactness.Bases (goal)
Goal:
X : Type u_1
ι : Type u_2
inst : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
U : Set X
hUc : IsCompact U
hUo : IsOpen U
Y : Type u_1
f' : (i : Y) → ι
e : U = ⋃ (i : Y), (b ∘ f') i
hf' : ∀ (i : Y), b (f' i) = (b ∘ f') i
t : Finset Y
ht : U ⊆ ⋃ i ∈ t, (b ∘ f') i
refine_1 : U ≤ ⋃ i ∈ (↑(Finset.image f' t) : Set ι), b i
⊢ ∃ (s : Set ι), s.Finite ∧ U = ⋃ i ∈ s, b i
have refine_2 : ⋃ i ∈ (↑(Finset.image f' t) : Set ι), b i ≤ U
Tactic: classical
  refine ⟨t.image f', Set.toFinite _, le_antisymm ?_ ?_⟩
  · refine Set.Subset.trans ht ?_
    simp only [Set.iUnion_subset_iff]
    intro i hi
    simpa using subset_iUnion₂ (s := fun i _ => b (f' i)) i hi
  · apply Set.iUnion₂_subset
    rintro i hi
    obtain ⟨j, -, rfl⟩ := Finset.mem_image.mp hi
    rw [e]
    exact Set.subset_iUnion (b ∘ f') j
-- Lean 4 proof step from Mathlib.Topology.Compactness.Bases (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
b : Set (Set X)
hb : IsTopologicalBasis b
U : Set X
hUc : IsCompact U
hUo : IsOpen U
⊢ ∃ (s : Finset (↑b : Type u_1)), U = ⋃₀ (Subtype.val (p := fun (x : Set X) ↦ x ∈ b) '' (↑s : Set (↑b : Type u_1)))
have hb' : b = range fun (i : (↑b : Type u_1)) ↦ (↑i : Set X)
Tactic: have hb' : b = range (fun i ↦ i : b → Set X) := by simp
-- Lean 4 proof step from Mathlib.Topology.Compactness.Bases (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
b : Set (Set X)
hb : IsTopologicalBasis b
U : Set X
hUc : IsCompact U
hUo : IsOpen U
hb' : b = range fun (i : (↑b : Type u_1)) ↦ (↑i : Set X)
⊢ ∃ (s : Finset (↑b : Type u_1)), U = ⋃₀ (Subtype.val (p := fun (x : Set X) ↦ x ∈ b) '' (↑s : Set (↑b : Type u_1)))
have rw : ∀ (hb : IsTopologicalBasis.{u_1} (α := X) (range fun (i : (↑b : Type u_1)) ↦ (↑i : Set X))) (U : Set X)
  (hUc : IsCompact U) (hUo : IsOpen U) (hb' : b = range fun (i : (↑b : Type u_1)) ↦ (↑i : Set X)),
  ∃ (s : Finset (↑b : Type u_1)), U = ⋃₀ (Subtype.val (p := fun (x : Set X) ↦ x ∈ b) '' (↑s : Set (↑b : Type u_1)))
Tactic: rw [hb'] at hb
Cleared hypotheses: hb, U, hUc, hUo, hb'
-- Lean 4 proof step from Mathlib.Topology.Compactness.Bases (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
b : Set (Set X)
hb : IsTopologicalBasis.{u_1} (α := X) (range fun (i : (↑b : Type u_1)) ↦ (↑i : Set X))
U : Set X
hUc : IsCompact U
hUo : IsOpen U
hb' : b = range fun (i : (↑b : Type u_1)) ↦ (↑i : Set X)
⊢ ∃ (s : Finset (↑b : Type u_1)), U = ⋃₀ (Subtype.val (p := fun (x : Set X) ↦ x ∈ b) '' (↑s : Set (↑b : Type u_1)))
have choose : ∀ (s : Set (↑b : Type u_1)) (hs : s.Finite) (hU : U = ⋃ i ∈ s, (↑i : Set X)),
  ∃ (s : Finset (↑b : Type u_1)), U = ⋃₀ (Subtype.val (p := fun (x : Set X) ↦ x ∈ b) '' (↑s : Set (↑b : Type u_1)))
Tactic: choose s hs hU using eq_finite_iUnion_of_isTopologicalBasis_of_isCompact_open _ hb U hUc hUo
-- Lean 4 proof step from Mathlib.Topology.Compactness.Bases (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
b : Set (Set X)
hb : IsTopologicalBasis.{u_1} (α := X) (range fun (i : (↑b : Type u_1)) ↦ (↑i : Set X))
U : Set X
hUc : IsCompact U
hUo : IsOpen U
hb' : b = range fun (i : (↑b : Type u_1)) ↦ (↑i : Set X)
s : Set (↑b : Type u_1)
hs : s.Finite
hU : U = ⋃ i ∈ s, (↑i : Set X)
⊢ ∃ (s : Finset (↑b : Type u_1)), U = ⋃₀ (Subtype.val (p := fun (x : Set X) ↦ x ∈ b) '' (↑s : Set (↑b : Type u_1)))
have this : Finite.{u_1 + 1} (↑s : Type u_1)
Tactic: have : Finite s := hs