-- Mathlib/Topology/StoneCech.lean
lemma eq_if_preStoneCechUnit_eq {a b : α} (h : preStoneCechUnit a = preStoneCechUnit b) :
    g a = g b

Proof state:
α : Type u
inst✝³ : TopologicalSpace α
β : Type v
inst✝² : TopologicalSpace β
inst✝¹ : T2Space β
inst✝ : CompactSpace β
g : α → β
hg : Continuous g
a b : α
h : preStoneCechUnit a = preStoneCechUnit b
e : Ultrafilter.extend g ∘ pure = g
⊢ Ultrafilter.extend g (pure a) = Ultrafilter.extend g (pure b)

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

Result:
α : Type u
inst✝³ : TopologicalSpace α
β : Type v
inst✝² : TopologicalSpace β
inst✝¹ : T2Space β
inst✝ : CompactSpace β
g : α → β
hg : Continuous g
a b : α
h : Relation.EqvGen (fun F G => ∃ x, ↑F ≤ 𝓝 x ∧ ↑G ≤ 𝓝 x) (pure a) (pure b)
e : Ultrafilter.extend g ∘ pure = g
⊢ Ultrafilter.extend g (pure a) = Ultrafilter.extend g (pure b)

Proof state:
α : Type u
inst✝³ : TopologicalSpace α
β : Type v
inst✝² : TopologicalSpace β
inst✝¹ : T2Space β
inst✝ : CompactSpace β
g : α → β
hg : Continuous g
a b : α
h : preStoneCechUnit a = preStoneCechUnit b
⊢ g a = g b

Tactic:
have e := ultrafilter_extend_extends g

Result:
α : Type u
inst✝³ : TopologicalSpace α
β : Type v
inst✝² : TopologicalSpace β
inst✝¹ : T2Space β
inst✝ : CompactSpace β
g : α → β
hg : Continuous g
a b : α
h : preStoneCechUnit a = preStoneCechUnit b
e : Ultrafilter.extend g ∘ pure = g
⊢ g a = g b

Proof state:
α : Type u
inst✝³ : TopologicalSpace α
β : Type v
inst✝² : TopologicalSpace β
inst✝¹ : T2Space β
inst✝ : CompactSpace β
g : α → β
hg : Continuous g
a b : α
h : Relation.EqvGen (fun F G => ∃ x, ↑F ≤ 𝓝 x ∧ ↑G ≤ 𝓝 x) (pure a) (pure b)
e : Ultrafilter.extend g ∘ pure = g
⊢ Ultrafilter.extend g (pure a) = Ultrafilter.extend g (pure b)

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

Result:
α : Type u
inst✝³ : TopologicalSpace α
β : Type v
inst✝² : TopologicalSpace β
inst✝¹ : T2Space β
inst✝ : CompactSpace β
g : α → β
hg : Continuous g
a b : α
e : Ultrafilter.extend g ∘ pure = g
F : Ultrafilter α
h : Relation.EqvGen (fun F G => ∃ x, ↑F ≤ 𝓝 x ∧ ↑G ≤ 𝓝 x) F (pure b)
⊢ Ultrafilter.extend g F = Ultrafilter.extend g (pure b)

Proof state:
α : Type u
inst✝³ : TopologicalSpace α
β : Type v
inst✝² : TopologicalSpace β
inst✝¹ : T2Space β
inst✝ : CompactSpace β
g : α → β
hg : Continuous g
a b : α
h : preStoneCechUnit a = preStoneCechUnit b
e : Ultrafilter.extend g ∘ pure = g
⊢ g a = g b

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

Result:
α : Type u
inst✝³ : TopologicalSpace α
β : Type v
inst✝² : TopologicalSpace β
inst✝¹ : T2Space β
inst✝ : CompactSpace β
g : α → β
hg : Continuous g
a b : α
h : preStoneCechUnit a = preStoneCechUnit b
e : Ultrafilter.extend g ∘ pure = g
⊢ Ultrafilter.extend g (pure a) = Ultrafilter.extend g (pure b)

Proof state:
case rel
α : Type u
inst✝³ : TopologicalSpace α
β : Type v
inst✝² : TopologicalSpace β
inst✝¹ : T2Space β
inst✝ : CompactSpace β
g : α → β
hg : Continuous g
a✝ b : α
e : Ultrafilter.extend g ∘ pure = g
F G x y : Ultrafilter α
a : ∃ x_1, ↑x ≤ 𝓝 x_1 ∧ ↑y ≤ 𝓝 x_1
⊢ Ultrafilter.extend g x = Ultrafilter.extend g y

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

Result:
no goals

Proof state:
case trans
α : Type u
inst✝³ : TopologicalSpace α
β : Type v
inst✝² : TopologicalSpace β
inst✝¹ : T2Space β
inst✝ : CompactSpace β
g : α → β
hg : Continuous g
a b : α
e : Ultrafilter.extend g ∘ pure = g
F G x y z : Ultrafilter α
a✝¹ : Relation.EqvGen (fun F G => ∃ x, ↑F ≤ 𝓝 x ∧ ↑G ≤ 𝓝 x) x y
a✝ : Relation.EqvGen (fun F G => ∃ x, ↑F ≤ 𝓝 x ∧ ↑G ≤ 𝓝 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'

Result:
no goals

Proof state:
case symm
α : Type u
inst✝³ : TopologicalSpace α
β : Type v
inst✝² : TopologicalSpace β
inst✝¹ : T2Space β
inst✝ : CompactSpace β
g : α → β
hg : Continuous g
a b : α
e : Ultrafilter.extend g ∘ pure = g
F G x y : Ultrafilter α
a✝ : Relation.EqvGen (fun F G => ∃ x, ↑F ≤ 𝓝 x ∧ ↑G ≤ 𝓝 x) x y
h : Ultrafilter.extend g x = Ultrafilter.extend g y
⊢ Ultrafilter.extend g y = Ultrafilter.extend g x

Tactic:
rw [h]

Result:
no goals

Proof state:
α : Type u
inst✝³ : TopologicalSpace α
β : Type v
inst✝² : TopologicalSpace β
inst✝¹ : T2Space β
inst✝ : CompactSpace β
g : α → β
hg : Continuous g
a b : α
e : Ultrafilter.extend g ∘ pure = g
F : Ultrafilter α
h : Relation.EqvGen (fun F G => ∃ x, ↑F ≤ 𝓝 x ∧ ↑G ≤ 𝓝 x) F (pure b)
⊢ Ultrafilter.extend g F = Ultrafilter.extend g (pure b)

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

Result:
α : Type u
inst✝³ : TopologicalSpace α
β : Type v
inst✝² : TopologicalSpace β
inst✝¹ : T2Space β
inst✝ : CompactSpace β
g : α → β
hg : Continuous g
a b : α
e : Ultrafilter.extend g ∘ pure = g
F G : Ultrafilter α
h : Relation.EqvGen (fun F G => ∃ x, ↑F ≤ 𝓝 x ∧ ↑G ≤ 𝓝 x) F G
⊢ Ultrafilter.extend g F = Ultrafilter.extend g G

Proof state:
case refl
α : Type u
inst✝³ : TopologicalSpace α
β : Type v
inst✝² : TopologicalSpace β
inst✝¹ : T2Space β
inst✝ : CompactSpace β
g : α → β
hg : Continuous g
a b : α
e : Ultrafilter.extend g ∘ pure = g
F G x : Ultrafilter α
⊢ Ultrafilter.extend g x = Ultrafilter.extend g x

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u
inst✝³ : TopologicalSpace α
β : Type v
inst✝² : TopologicalSpace β
inst✝¹ : T2Space β
inst✝ : CompactSpace β
g : α → β
hg : Continuous g
a b : α
e : Ultrafilter.extend g ∘ pure = g
F G : Ultrafilter α
h : Relation.EqvGen (fun F G => ∃ x, ↑F ≤ 𝓝 x ∧ ↑G ≤ 𝓝 x) F G
⊢ 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'

Result:
no goals