Theorem: Profinite.EffectiveEpiFamily.π'_comp_ι_hom (Profinite/Epi.lean)

State before:
X✝ Y B✝ : Profinite
f : X✝ ⟶ B✝
g : Y ⟶ B✝
α : Type
inst✝ : Fintype α
B : Profinite
X : α → Profinite
π : (a : α) → X a ⟶ B
surj : ∀ (b : ↑B.toCompHaus.toTop), ∃ a x, ↑(π a) x = b
a : α
⊢ π' π surj a ≫ (ι₂Iso π surj).hom = π a
Tactic:
ext
State after:
case w
X✝ Y B✝ : Profinite
f : X✝ ⟶ B✝
g : Y ⟶ B✝
α : Type
inst✝ : Fintype α
B : Profinite
X : α → Profinite
π : (a : α) → X a ⟶ B
surj : ∀ (b : ↑B.toCompHaus.toTop), ∃ a x, ↑(π a) x = b
a : α
x✝ : (forget Profinite).obj (X a)
⊢ ↑(π' π surj a ≫ (ι₂Iso π surj).hom) x✝ = ↑(π a) x✝

State before:
case w
X✝ Y B✝ : Profinite
f : X✝ ⟶ B✝
g : Y ⟶ B✝
α : Type
inst✝ : Fintype α
B : Profinite
X : α → Profinite
π : (a : α) → X a ⟶ B
surj : ∀ (b : ↑B.toCompHaus.toTop), ∃ a x, ↑(π a) x = b
a : α
x✝ : (forget Profinite).obj (X a)
⊢ ↑(π' π surj a ≫ (ι₂Iso π surj).hom) x✝ = ↑(π a) x✝
Tactic:
rfl
State after:
no goals