Theorem: Profinite.finiteCoproduct.hom_ext (Profinite/Epi.lean)

State before:
α : Type
inst✝ : Fintype α
X : α → Profinite
B : Profinite
f g : finiteCoproduct X ⟶ B
h : ∀ (a : α), ι X a ≫ f = ι X a ≫ g
⊢ f = g
Tactic:
ext ⟨a,x⟩
State after:
case w.mk
α : Type
inst✝ : Fintype α
X : α → Profinite
B : Profinite
f g : finiteCoproduct X ⟶ B
h : ∀ (a : α), ι X a ≫ f = ι X a ≫ g
a : α
x : ↑(X a).toCompHaus.toTop
⊢ ↑f { fst := a, snd := x } = ↑g { fst := a, snd := x }

State before:
case w.mk
α : Type
inst✝ : Fintype α
X : α → Profinite
B : Profinite
f g : finiteCoproduct X ⟶ B
h : ∀ (a : α), ι X a ≫ f = ι X a ≫ g
a : α
x : ↑(X a).toCompHaus.toTop
⊢ ↑f { fst := a, snd := x } = ↑g { fst := a, snd := x }
Tactic:
specialize h a
State after:
case w.mk
α : Type
inst✝ : Fintype α
X : α → Profinite
B : Profinite
f g : finiteCoproduct X ⟶ B
a : α
x : ↑(X a).toCompHaus.toTop
h : ι X a ≫ f = ι X a ≫ g
⊢ ↑f { fst := a, snd := x } = ↑g { fst := a, snd := x }

State before:
case w.mk
α : Type
inst✝ : Fintype α
X : α → Profinite
B : Profinite
f g : finiteCoproduct X ⟶ B
a : α
x : ↑(X a).toCompHaus.toTop
h : ι X a ≫ f = ι X a ≫ g
⊢ ↑f { fst := a, snd := x } = ↑g { fst := a, snd := x }
Tactic:
apply_fun (fun q => q x) at h
State after:
case w.mk
α : Type
inst✝ : Fintype α
X : α → Profinite
B : Profinite
f g : finiteCoproduct X ⟶ B
a : α
x : ↑(X a).toCompHaus.toTop
h : ↑(ι X a ≫ f) x = ↑(ι X a ≫ g) x
⊢ ↑f { fst := a, snd := x } = ↑g { fst := a, snd := x }

State before:
case w.mk
α : Type
inst✝ : Fintype α
X : α → Profinite
B : Profinite
f g : finiteCoproduct X ⟶ B
a : α
x : ↑(X a).toCompHaus.toTop
h : ↑(ι X a ≫ f) x = ↑(ι X a ≫ g) x
⊢ ↑f { fst := a, snd := x } = ↑g { fst := a, snd := x }
Tactic:
exact h
State after:
no goals