Theorem: Profinite.pullback.condition (Profinite/ExplicitLimits.lean)

State before:
α : Type
inst✝ : Fintype α
Z✝ : α → Profinite
X Y Z : Profinite
f : X ⟶ Z
g i : Y ⟶ Z
⊢ fst f g ≫ f = snd f g ≫ g
Tactic:
ext ⟨_,h⟩
State after:
case w.mk
α : Type
inst✝ : Fintype α
Z✝ : α → Profinite
X Y Z : Profinite
f : X ⟶ Z
g i : Y ⟶ Z
val✝ : ↑X.toCompHaus.toTop × ↑Y.toCompHaus.toTop
h : val✝ ∈ {xy | ↑f xy.fst = ↑g xy.snd}
⊢ ↑(fst f g ≫ f) { val := val✝, property := h } = ↑(snd f g ≫ g) { val := val✝, property := h }

State before:
case w.mk
α : Type
inst✝ : Fintype α
Z✝ : α → Profinite
X Y Z : Profinite
f : X ⟶ Z
g i : Y ⟶ Z
val✝ : ↑X.toCompHaus.toTop × ↑Y.toCompHaus.toTop
h : val✝ ∈ {xy | ↑f xy.fst = ↑g xy.snd}
⊢ ↑(fst f g ≫ f) { val := val✝, property := h } = ↑(snd f g ≫ g) { val := val✝, property := h }
Tactic:
exact h
State after:
no goals