awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Compactification.StoneCech
Goal:
α : Type u
inst : TopologicalSpace α
x : α
g : Ultrafilter α
gx : (↑g : Filter α) ≤ 𝓝 x
this_1 : (↑(Ultrafilter.map pure g) : Filter (Ultrafilter α)) ≤ 𝓝 g
this :
  LE.le (α := Filter (PreStoneCech α)) (map preStoneCechUnit (↑g : Filter α))
    (𝓝 (Quot.mk (fun (F G : Ultrafilter α) ↦ ∃ (x : α), (↑F : Filter α) ≤ 𝓝 x ∧ (↑G : Filter α) ≤ 𝓝 x) g))
⊢ Eq (α := PreStoneCech α) (preStoneCechUnit x)
    (Quot.mk (fun (F G : Ultrafilter α) ↦ ∃ (x : α), (↑F : Filter α) ≤ 𝓝 x ∧ (↑G : Filter α) ≤ 𝓝 x) g)

Tactic:
exact Quot.sound ⟨x, pure_le_nhds x, gx⟩

Premises used: Quot.sound
-- Module: Mathlib.Topology.Compactification.StoneCech
Goal:
α : Type u
inst : TopologicalSpace α
⊢ DenseRange.{u, u} (X := PreStoneCech α) preStoneCechUnit

Tactic:
Quot.mk_surjective.denseRange.comp denseRange_pure continuous_coinduced_rng

Premises used: denseRange_pure, preStoneCechUnit, Function.Surjective.denseRange, PreStoneCech, DenseRange.comp, Quot.mk_surjective, continuous_coinduced_rng
-- Module: Mathlib.Topology.Compactification.StoneCech
Goal:
α : Type u
inst : TopologicalSpace α
β : Type v
inst_1 : TopologicalSpace β
inst_2 : T2Space β
g₁ g₂ : PreStoneCech α → β
h₁ : Continuous[_, inst_1] g₁
h₂ : Continuous[_, inst_1] g₂
h : g₁ ∘ preStoneCechUnit = g₂ ∘ preStoneCechUnit
apply : EqOn g₁ g₂ (range preStoneCechUnit)
⊢ g₁ = g₂

Tactic:
apply Continuous.ext_on denseRange_preStoneCechUnit h₁ h₂

Premises used: denseRange_preStoneCechUnit, Continuous.ext_on
-- Module: Mathlib.Topology.Compactification.StoneCech
Goal:
α : Type u
inst : TopologicalSpace α
β : Type v
inst_1 : TopologicalSpace β
inst_2 : T2Space β
g₁ g₂ : PreStoneCech α → β
h₁ : Continuous[_, inst_1] g₁
h₂ : Continuous[_, inst_1] g₂
h : g₁ ∘ preStoneCechUnit = g₂ ∘ preStoneCechUnit
x : α
⊢ g₁ (preStoneCechUnit x) = g₂ (preStoneCechUnit x)

Tactic:
apply congr_fun h x

Premises used: congr_fun
-- Module: Mathlib.Topology.Compactification.StoneCech
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
⊢ map g (↑F : Filter α) ≤ 𝓝 (g x)

Tactic:
replace hF := (map_mono hF).trans hg.continuousAt
-- Module: Mathlib.Topology.Compactification.StoneCech
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)
⊢ map g (↑G : Filter α) ≤ 𝓝 (g x)

Tactic:
replace hG := (map_mono hG).trans hg.continuousAt
-- Module: Mathlib.Topology.Compactification.StoneCech
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.map g G) : Filter β) ≤ 𝓝 (g x)
rwa₁ rwa₂ rwa₃ rwa₄ : map g (↑G : Filter α) ≤ 𝓝 (g x)
⊢ Ultrafilter.extend g G = g x

Tactic:
rwa [ultrafilter_extend_eq_iff, G.coe_map]

Premises used: Ultrafilter.coe_map, ultrafilter_extend_eq_iff
-- Module: Mathlib.Topology.Compactification.StoneCech
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
rwa₁ : (↑(Ultrafilter.map g F) : Filter β) ≤ 𝓝 (g x)
rwa₂ rwa₃ rwa₄ rwa₅ : map g (↑F : Filter α) ≤ 𝓝 (g x)
⊢ Ultrafilter.extend g F = Ultrafilter.extend g G

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]

Premises used: Ultrafilter.coe_map, ultrafilter_extend_eq_iff
-- Module: Mathlib.Topology.Compactification.StoneCech
Goal:
α : Type u
inst : TopologicalSpace α
β : Type v
inst_1 : TopologicalSpace β
inst_2 : T2Space β
inst_3 : CompactSpace β
g : α → β
hg : Continuous[inst, inst_1] g
⊢ preStoneCechExtend hg ∘ preStoneCechUnit = g

Tactic:
ultrafilter_extend_extends g

Premises used: ultrafilter_extend_extends, preStoneCechExtend
-- Module: Mathlib.Topology.Compactification.StoneCech
Goal:
α : Type u
inst : TopologicalSpace α
β : Type v
inst_1 : TopologicalSpace β
inst_2 : T2Space β
inst_3 : CompactSpace β
g : α → β
hg : Continuous[inst, inst_1] g
a : α
⊢ preStoneCechExtend hg (preStoneCechUnit a) = g a

Tactic:
congr_fun (preStoneCechExtend_extends hg) a

Premises used: Classical.epsilon, preStoneCechExtend, preStoneCechExtend_extends, Ultrafilter.extend, Filter.lim, congr_fun, Filter.limUnder, IsDenseInducing.extend
-- Module: Mathlib.Topology.Compactification.StoneCech
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)
⊢ Ultrafilter.extend g ∘ pure = g

Tactic:
have e := ultrafilter_extend_extends g
-- Module: Mathlib.Topology.Compactification.StoneCech
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
rw : Ultrafilter.extend g (pure a) = Ultrafilter.extend g (pure b)
⊢ g a = g b

Tactic:
rw [← congrFun e a, ← congrFun e b, Function.comp_apply, Function.comp_apply]

Premises used: congrFun, Function.comp_apply
-- Module: Mathlib.Topology.Compactification.StoneCech
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
⊢ 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

Premises used: preStoneCechUnit, Quot.eq
-- Module: Mathlib.Topology.Compactification.StoneCech
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
h₁ :
  Relation.EqvGen (fun (F G : Ultrafilter α) ↦ ∃ (x : α), (↑F : Filter α) ≤ 𝓝 x ∧ (↑G : Filter α) ≤ 𝓝 x) (pure a)
    (pure b)
⊢ Ultrafilter.extend g ∘ pure = g

Tactic:
rw [preStoneCechUnit, preStoneCechUnit, Quot.eq] at h

Premises used: preStoneCechUnit, Quot.eq
-- Module: Mathlib.Topology.Compactification.StoneCech
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
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)
⊢ Ultrafilter.extend g (pure a) = Ultrafilter.extend g (pure b)

Tactic:
generalize (pure a : Ultrafilter α) = F at h

Premises used: Pure.pure
-- Module: Mathlib.Topology.Compactification.StoneCech
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)
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
⊢ Ultrafilter.extend g F = Ultrafilter.extend g (pure b)

Tactic:
generalize (pure b : Ultrafilter α) = G at h

Premises used: Pure.pure
-- Module: Mathlib.Topology.Compactification.StoneCech
Goal:
α : Type u
inst : TopologicalSpace α
β : Type v
inst_1 : TopologicalSpace β
inst_2 : T2Space β
inst_3 : CompactSpace β
g : α → β
hg : Continuous[inst, inst_1] g
a_1 b : α
e : Ultrafilter.extend g ∘ pure = g
F G x y : Ultrafilter α
a : ∃ (x_1 : α), (↑x : Filter α) ≤ 𝓝 x_1 ∧ (↑y : Filter α) ≤ 𝓝 x_1
⊢ Ultrafilter.extend g x = Ultrafilter.extend g y

Tactic:
let ⟨a, hx, hy⟩ := a; preStoneCechCompat hg hx hy

Premises used: _private.0.eq_if_preStoneCechUnit_eq.match_2, Ultrafilter.extend, Eq, preStoneCechCompat
-- Module: Mathlib.Topology.Compactification.StoneCech
Goal:
α : Type u
inst : TopologicalSpace α
β : Type v
inst_1 : TopologicalSpace β
inst_2 : T2Space β
inst_3 : CompactSpace β
g : α → β
hg : Continuous[inst, inst_1] g
a_1 b : α
e : Ultrafilter.extend g ∘ pure = g
F G x y : Ultrafilter α
a : ∃ (x_1 : α), (↑x : Filter α) ≤ 𝓝 x_1 ∧ (↑y : Filter α) ≤ 𝓝 x_1
⊢ Ultrafilter.extend g x = Ultrafilter.extend g y

Tactic:
exact let ⟨a, hx, hy⟩ := a; preStoneCechCompat hg hx hy
-- Module: Mathlib.Topology.Compactification.StoneCech
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 : Ultrafilter α
⊢ Ultrafilter.extend g x = Ultrafilter.extend g x

Tactic:
rfl
-- Module: Mathlib.Topology.Compactification.StoneCech
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
symm symm₁ : Ultrafilter.extend g y = Ultrafilter.extend g y
⊢ Ultrafilter.extend g y = Ultrafilter.extend g x

Tactic:
rw [h]
-- Module: Mathlib.Topology.Compactification.StoneCech
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 z : Ultrafilter α
h_1 : Relation.EqvGen (fun (F G : Ultrafilter α) ↦ ∃ (x : α), (↑F : Filter α) ≤ 𝓝 x ∧ (↑G : Filter α) ≤ 𝓝 x) x y
h_2 : 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:
h.trans h'

Premises used: Eq.trans
-- Module: Mathlib.Topology.Compactification.StoneCech
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 z : Ultrafilter α
h_1 : Relation.EqvGen (fun (F G : Ultrafilter α) ↦ ∃ (x : α), (↑F : Filter α) ≤ 𝓝 x ∧ (↑G : Filter α) ≤ 𝓝 x) x y
h_2 : 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:
exact h.trans h'

Premises used: Eq.trans
-- Module: Mathlib.Topology.Compactification.StoneCech
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
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
⊢ Ultrafilter.extend g F = Ultrafilter.extend g G

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'

Premises used: symm, refl
-- Module: Mathlib.Topology.Compactification.StoneCech
Goal:
α : Type u
inst : TopologicalSpace α
β : Type v
inst_1 : TopologicalSpace β
inst_2 : T2Space β
inst_3 : CompactSpace β
g : α → β
hg : Continuous[inst, inst_1] g
⊢ Continuous[_, inst_1] (preStoneCechExtend hg)

Tactic:
continuous_quot_lift _ (continuous_ultrafilter_extend g)

Premises used: continuous_quot_lift, preStoneCechExtend, PreStoneCech, continuous_ultrafilter_extend
-- Module: Mathlib.Topology.Compactification.StoneCech
Goal:
α : Type u
inst : TopologicalSpace α
⊢ T2Space.{u} (StoneCech α)

Tactic:
inferInstanceAs <| T2Space <| T2Quotient _

Premises used: _private.0.instT2SpaceStoneCech._proof_1
-- Module: Mathlib.Topology.Compactification.StoneCech
Goal:
α : Type u
inst : TopologicalSpace α
⊢ CompactSpace.{u} (StoneCech α)

Tactic:
Quot.compactSpace

Premises used: T2Quotient, Quotient, Quotient.mk', Quot.compactSpace, StoneCech
-- Module: Mathlib.Topology.Compactification.StoneCech
Goal:
α : Type u
inst : TopologicalSpace α
⊢ Continuous[inst, _] stoneCechUnit

Tactic:
(T2Quotient.continuous_mk _).comp continuous_preStoneCechUnit

Premises used: Continuous.comp, T2Quotient.mk, T2Quotient.continuous_mk, stoneCechUnit, continuous_preStoneCechUnit, StoneCech
-- Module: Mathlib.Topology.Compactification.StoneCech
Goal:
α : Type u
inst : TopologicalSpace α
⊢ Function.Surjective.{u + 1, u + 1} (α := PreStoneCech α) (β := T2Quotient (PreStoneCech α)) T2Quotient.mk

Tactic:
Quot.mk_surjective

Premises used: T2Quotient.mk, T2Quotient, Quotient, Quot.mk_surjective
-- Module: Mathlib.Topology.Compactification.StoneCech
Goal:
α : Type u
inst : TopologicalSpace α
⊢ Function.Surjective.{u + 1, u + 1} (α := PreStoneCech α) (β := T2Quotient (PreStoneCech α)) T2Quotient.mk

Tactic:
exact Quot.mk_surjective

Premises used: Quot.mk_surjective
-- Module: Mathlib.Topology.Compactification.StoneCech
Goal:
α : Type u
inst : TopologicalSpace α
⊢ Function.Surjective.{u + 1, u + 1} (α := PreStoneCech α) (β := T2Quotient (PreStoneCech α)) T2Quotient.mk

Tactic:
have : Function.Surjective (T2Quotient.mk : PreStoneCech α → StoneCech α) := by
    exact Quot.mk_surjective
-- Module: Mathlib.Topology.Compactification.StoneCech
Goal:
α : Type u
inst : TopologicalSpace α
this : Function.Surjective.{u + 1, u + 1} (α := PreStoneCech α) (β := T2Quotient (PreStoneCech α)) T2Quotient.mk
⊢ DenseRange (X := StoneCech α) fun (x : α) ↦ ⟦preStoneCechUnit x⟧

Tactic:
this.denseRange.comp denseRange_preStoneCechUnit continuous_coinduced_rng

Premises used: Function.Surjective.denseRange, T2Quotient.mk, denseRange_preStoneCechUnit, DenseRange.comp, StoneCech, continuous_coinduced_rng
-- Module: Mathlib.Topology.Compactification.StoneCech
Goal:
α : Type u
inst : TopologicalSpace α
this : Function.Surjective.{u + 1, u + 1} (α := PreStoneCech α) (β := T2Quotient (PreStoneCech α)) T2Quotient.mk
⊢ DenseRange (X := StoneCech α) fun (x : α) ↦ ⟦preStoneCechUnit x⟧

Tactic:
exact this.denseRange.comp denseRange_preStoneCechUnit continuous_coinduced_rng

Premises used: Function.Surjective.denseRange, denseRange_preStoneCechUnit, DenseRange.comp, continuous_coinduced_rng
-- Module: Mathlib.Topology.Compactification.StoneCech
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
apply : EqOn g₁ g₂ (range stoneCechUnit)
⊢ g₁ = g₂

Tactic:
apply h₁.ext_on denseRange_stoneCechUnit h₂

Premises used: Continuous.ext_on, denseRange_stoneCechUnit
-- Module: Mathlib.Topology.Compactification.StoneCech
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
x : α
⊢ g₁ (stoneCechUnit x) = g₂ (stoneCechUnit x)

Tactic:
congr_fun h x

Premises used: congr_fun
-- Module: Mathlib.Topology.Compactification.StoneCech
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
x : α
⊢ g₁ (stoneCechUnit x) = g₂ (stoneCechUnit x)

Tactic:
exact congr_fun h x

Premises used: congr_fun
-- Module: Mathlib.Topology.Compactification.StoneCech
Goal:
α : Type u
inst : TopologicalSpace α
β : Type v
inst_1 : TopologicalSpace β
inst_2 : T2Space β
g : α → β
hg : Continuous[inst, inst_1] g
inst_3 : CompactSpace β
h : ∀ (x : α), (stoneCechExtend hg ∘ stoneCechUnit) x = g x
⊢ stoneCechExtend hg ∘ stoneCechUnit = g

Tactic:
ext x
-- Module: Mathlib.Topology.Compactification.StoneCech
Goal:
α : Type u
inst : TopologicalSpace α
β : Type v
inst_1 : TopologicalSpace β
inst_2 : T2Space β
g : α → β
hg : Continuous[inst, inst_1] g
inst_3 : CompactSpace β
x : α
⊢ preStoneCechExtend hg (preStoneCechUnit x) = g x

Tactic:
apply congrFun (preStoneCechExtend_extends hg)

Premises used: preStoneCechExtend_extends, congrFun
-- Module: Mathlib.Topology.Compactification.StoneCech
Goal:
α : Type u
inst : TopologicalSpace α
β : Type v
inst_1 : TopologicalSpace β
inst_2 : T2Space β
g : α → β
hg : Continuous[inst, inst_1] g
inst_3 : CompactSpace β
a : α
⊢ stoneCechExtend hg (stoneCechUnit a) = g a

Tactic:
congr_fun (stoneCechExtend_extends hg) a

Premises used: Classical.epsilon, preStoneCechExtend, T2Quotient.lift, stoneCechExtend_extends, Ultrafilter.extend, Filter.lim, congr_fun, Filter.limUnder, stoneCechExtend, IsDenseInducing.extend
-- Module: Mathlib.Topology.Compactification.StoneCech
Goal:
α : Type u
inst : TopologicalSpace α
β : Type v
inst_1 : TopologicalSpace β
inst_2 : T2Space β
g : α → β
hg : Continuous[inst, inst_1] g
inst_3 : CompactSpace β
⊢ Continuous[_, inst_1] (stoneCechExtend hg)

Tactic:
continuous_coinduced_dom.mpr (continuous_preStoneCechExtend hg)

Premises used: Iff.mpr, continuous_coinduced_dom, continuous_preStoneCechExtend, T2Quotient, StoneCech
-- Module: Mathlib.Topology.Compactification.StoneCech
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)
rw : (stoneCechExtend hcf ∘ stoneCechUnit) a = (stoneCechExtend hcf ∘ stoneCechUnit) b
⊢ f a = f b

Tactic:
rw [← congrFun (stoneCechExtend_extends hcf), ← congrFun (stoneCechExtend_extends hcf)]

Premises used: stoneCechExtend_extends, congrFun
-- Module: Mathlib.Topology.Compactification.StoneCech
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)
⊢ (stoneCechExtend hcf ∘ stoneCechUnit) a = (stoneCechExtend hcf ∘ stoneCechUnit) b

Tactic:
congrArg (stoneCechExtend hcf) h

Premises used: Classical.epsilon, congrArg, preStoneCechExtend, T2Quotient.lift, Ultrafilter.extend, Filter.lim, Filter.limUnder, stoneCechExtend, IsDenseInducing.extend
-- Module: Mathlib.Topology.Compactification.StoneCech
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)
⊢ (stoneCechExtend hcf ∘ stoneCechUnit) a = (stoneCechExtend hcf ∘ stoneCechUnit) b

Tactic:
exact congrArg (stoneCechExtend hcf) h

Premises used: congrArg, stoneCechExtend
-- Module: Mathlib.Topology.Compactness.Bases
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
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
⊢ ∃ (s : Set ι), s.Finite ∧ U = ⋃ i ∈ s, b i

Tactic:
obtain ⟨Y, f, e, hf⟩ := hb.open_eq_iUnion hUo

Premises used: TopologicalSpace.IsTopologicalBasis.open_eq_iUnion
-- Module: Mathlib.Topology.Compactness.Bases
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
choose : ∀ (f' : (i : Y) → ι) (hf' : ∀ (i : Y), b (f' i) = f i), ∃ (s : Set ι), s.Finite ∧ U = ⋃ i ∈ s, b i
⊢ ∃ (s : Set ι), s.Finite ∧ U = ⋃ i ∈ s, b i

Tactic:
choose f' hf' using hf
-- Module: Mathlib.Topology.Compactness.Bases
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
⊢ b ∘ f' = f

Tactic:
have : b ∘ f' = f := funext hf'
-- Module: Mathlib.Topology.Compactness.Bases
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
⊢ U = ⋃ (i : Y), (b ∘ f') i

Tactic:
subst this
-- Module: Mathlib.Topology.Compactness.Bases
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
⊢ ∀ (i : Y), b (f' i) = (b ∘ f') i

Tactic:
subst this
-- Module: Mathlib.Topology.Compactness.Bases
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
rw rw₁ : Subset.{u_1} (α := Set X) (⋃ (i : Y), (b ∘ f') i) (⋃ (i : Y), (b ∘ f') i)
⊢ U ⊆ ⋃ (i : Y), (b ∘ f') i

Tactic:
rw [e]
-- Module: Mathlib.Topology.Compactness.Bases
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
obtain : ∀ (t : Finset Y) (ht : U ⊆ ⋃ i ∈ t, (b ∘ f') i), ∃ (s : Set ι), s.Finite ∧ U = ⋃ i ∈ s, b 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])

Premises used: Set.mem_range_self, TopologicalSpace.IsTopologicalBasis.isOpen, Function.comp, IsCompact.elim_finite_subcover