Theorem: Profinite.EffectiveEpiFamily.ιFun_injective (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.Injective (ιFun π)
Tactic:
rintro ⟨⟨a,x⟩⟩ ⟨⟨b,y⟩⟩ (h : π _ _ = π _ _)
State after:
case mk.mk.mk.mk
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₁✝ : Quotient (relation π)
a : α
x : ↑((fun a => X a) a).toCompHaus.toTop
a₂✝ : Quotient (relation π)
b : α
y : ↑((fun a => X a) b).toCompHaus.toTop
h : ↑(π a) x = ↑(π b) y
⊢ Quot.mk Setoid.r { fst := a, snd := x } = Quot.mk Setoid.r { fst := b, snd := y }

State before:
case mk.mk.mk.mk
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₁✝ : Quotient (relation π)
a : α
x : ↑((fun a => X a) a).toCompHaus.toTop
a₂✝ : Quotient (relation π)
b : α
y : ↑((fun a => X a) b).toCompHaus.toTop
h : ↑(π a) x = ↑(π b) y
⊢ Quot.mk Setoid.r { fst := a, snd := x } = Quot.mk Setoid.r { fst := b, snd := y }
Tactic:
apply Quotient.sound'
State after:
case mk.mk.mk.mk.a
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₁✝ : Quotient (relation π)
a : α
x : ↑((fun a => X a) a).toCompHaus.toTop
a₂✝ : Quotient (relation π)
b : α
y : ↑((fun a => X a) b).toCompHaus.toTop
h : ↑(π a) x = ↑(π b) y
⊢ Setoid.r { fst := a, snd := x } { fst := b, snd := y }

State before:
case mk.mk.mk.mk.a
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₁✝ : Quotient (relation π)
a : α
x : ↑((fun a => X a) a).toCompHaus.toTop
a₂✝ : Quotient (relation π)
b : α
y : ↑((fun a => X a) b).toCompHaus.toTop
h : ↑(π a) x = ↑(π b) y
⊢ Setoid.r { fst := a, snd := x } { fst := b, snd := y }
Tactic:
refine ⟨pullback (π a) (π b), ⟨⟨x,y⟩,h⟩, pullback.fst _ _, pullback.snd _ _, ?_, rfl, rfl⟩
State after:
case mk.mk.mk.mk.a
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₁✝ : Quotient (relation π)
a : α
x : ↑((fun a => X a) a).toCompHaus.toTop
a₂✝ : Quotient (relation π)
b : α
y : ↑((fun a => X a) b).toCompHaus.toTop
h : ↑(π a) x = ↑(π b) y
⊢ pullback.fst (π a) (π b) ≫ π { fst := a, snd := x }.fst = pullback.snd (π a) (π b) ≫ π { fst := b, snd := y }.fst

State before:
case mk.mk.mk.mk.a
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₁✝ : Quotient (relation π)
a : α
x : ↑((fun a => X a) a).toCompHaus.toTop
a₂✝ : Quotient (relation π)
b : α
y : ↑((fun a => X a) b).toCompHaus.toTop
h : ↑(π a) x = ↑(π b) y
⊢ pullback.fst (π a) (π b) ≫ π { fst := a, snd := x }.fst = pullback.snd (π a) (π b) ≫ π { fst := b, snd := y }.fst
Tactic:
ext ⟨_, h⟩
State after:
case mk.mk.mk.mk.a.w.mk
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₁✝ : Quotient (relation π)
a : α
x : ↑((fun a => X a) a).toCompHaus.toTop
a₂✝ : Quotient (relation π)
b : α
y : ↑((fun a => X a) b).toCompHaus.toTop
h✝ : ↑(π a) x = ↑(π b) y
val✝ : ↑(X a).toCompHaus.toTop × ↑(X b).toCompHaus.toTop
h : val✝ ∈ {xy | ↑(π a) xy.fst = ↑(π b) xy.snd}
⊢ ↑(pullback.fst (π a) (π b) ≫ π { fst := a, snd := x }.fst) { val := val✝, property := h } =
    ↑(pullback.snd (π a) (π b) ≫ π { fst := b, snd := y }.fst) { val := val✝, property := h }

State before:
case mk.mk.mk.mk.a.w.mk
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₁✝ : Quotient (relation π)
a : α
x : ↑((fun a => X a) a).toCompHaus.toTop
a₂✝ : Quotient (relation π)
b : α
y : ↑((fun a => X a) b).toCompHaus.toTop
h✝ : ↑(π a) x = ↑(π b) y
val✝ : ↑(X a).toCompHaus.toTop × ↑(X b).toCompHaus.toTop
h : val✝ ∈ {xy | ↑(π a) xy.fst = ↑(π b) xy.snd}
⊢ ↑(pullback.fst (π a) (π b) ≫ π { fst := a, snd := x }.fst) { val := val✝, property := h } =
    ↑(pullback.snd (π a) (π b) ≫ π { fst := b, snd := y }.fst) { val := val✝, property := h }
Tactic:
exact h
State after:
no goals