Theorem: Profinite.EffectiveEpiFamily.ιFun_surjective (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
⊢ Function.Surjective (ιFun π)
Tactic:
intro b
State after:
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
b : ↑B.toCompHaus.toTop
⊢ ∃ a, ιFun π a = b

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
b : ↑B.toCompHaus.toTop
⊢ ∃ a, ιFun π a = b
Tactic:
obtain ⟨a,x,h⟩ := surj b
State after:
case intro.intro
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
b : ↑B.toCompHaus.toTop
a : α
x : ↑(X a).toCompHaus.toTop
h : ↑(π a) x = b
⊢ ∃ a, ιFun π a = b

State before:
case intro.intro
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
b : ↑B.toCompHaus.toTop
a : α
x : ↑(X a).toCompHaus.toTop
h : ↑(π a) x = b
⊢ ∃ a, ιFun π a = b
Tactic:
refine ⟨Quotient.mk _ ⟨a,x⟩, h⟩
State after:
no goals