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

State before:
α : Type
inst✝ : Fintype α
Z✝¹ : α → Profinite
X Y Z✝ : Profinite
f : X ⟶ Z✝
g i : Y ⟶ Z✝
Z : Profinite
a b : Z ⟶ pullback f g
hfst : a ≫ fst f g = b ≫ fst f g
hsnd : a ≫ snd f g = b ≫ snd f g
⊢ a = b
Tactic:
ext z
State after:
case w
α : Type
inst✝ : Fintype α
Z✝¹ : α → Profinite
X Y Z✝ : Profinite
f : X ⟶ Z✝
g i : Y ⟶ Z✝
Z : Profinite
a b : Z ⟶ pullback f g
hfst : a ≫ fst f g = b ≫ fst f g
hsnd : a ≫ snd f g = b ≫ snd f g
z : (forget Profinite).obj Z
⊢ ↑a z = ↑b z

State before:
case w
α : Type
inst✝ : Fintype α
Z✝¹ : α → Profinite
X Y Z✝ : Profinite
f : X ⟶ Z✝
g i : Y ⟶ Z✝
Z : Profinite
a b : Z ⟶ pullback f g
hfst : a ≫ fst f g = b ≫ fst f g
hsnd : a ≫ snd f g = b ≫ snd f g
z : (forget Profinite).obj Z
⊢ ↑a z = ↑b z
Tactic:
apply_fun (fun q => q z) at hfst hsnd
State after:
case w
α : Type
inst✝ : Fintype α
Z✝¹ : α → Profinite
X Y Z✝ : Profinite
f : X ⟶ Z✝
g i : Y ⟶ Z✝
Z : Profinite
a b : Z ⟶ pullback f g
z : (forget Profinite).obj Z
hfst : ↑(a ≫ fst f g) z = ↑(b ≫ fst f g) z
hsnd : ↑(a ≫ snd f g) z = ↑(b ≫ snd f g) z
⊢ ↑a z = ↑b z

State before:
case w
α : Type
inst✝ : Fintype α
Z✝¹ : α → Profinite
X Y Z✝ : Profinite
f : X ⟶ Z✝
g i : Y ⟶ Z✝
Z : Profinite
a b : Z ⟶ pullback f g
z : (forget Profinite).obj Z
hfst : ↑(a ≫ fst f g) z = ↑(b ≫ fst f g) z
hsnd : ↑(a ≫ snd f g) z = ↑(b ≫ snd f g) z
⊢ ↑a z = ↑b z
Tactic:
apply Subtype.ext
State after:
case w.a
α : Type
inst✝ : Fintype α
Z✝¹ : α → Profinite
X Y Z✝ : Profinite
f : X ⟶ Z✝
g i : Y ⟶ Z✝
Z : Profinite
a b : Z ⟶ pullback f g
z : (forget Profinite).obj Z
hfst : ↑(a ≫ fst f g) z = ↑(b ≫ fst f g) z
hsnd : ↑(a ≫ snd f g) z = ↑(b ≫ snd f g) z
⊢ ↑(↑a z) = ↑(↑b z)

State before:
case w.a
α : Type
inst✝ : Fintype α
Z✝¹ : α → Profinite
X Y Z✝ : Profinite
f : X ⟶ Z✝
g i : Y ⟶ Z✝
Z : Profinite
a b : Z ⟶ pullback f g
z : (forget Profinite).obj Z
hfst : ↑(a ≫ fst f g) z = ↑(b ≫ fst f g) z
hsnd : ↑(a ≫ snd f g) z = ↑(b ≫ snd f g) z
⊢ ↑(↑a z) = ↑(↑b z)
Tactic:
apply Prod.ext
State after:
case w.a.h₁
α : Type
inst✝ : Fintype α
Z✝¹ : α → Profinite
X Y Z✝ : Profinite
f : X ⟶ Z✝
g i : Y ⟶ Z✝
Z : Profinite
a b : Z ⟶ pullback f g
z : (forget Profinite).obj Z
hfst : ↑(a ≫ fst f g) z = ↑(b ≫ fst f g) z
hsnd : ↑(a ≫ snd f g) z = ↑(b ≫ snd f g) z
⊢ (↑(↑a z)).fst = (↑(↑b z)).fst

case w.a.h₂
α : Type
inst✝ : Fintype α
Z✝¹ : α → Profinite
X Y Z✝ : Profinite
f : X ⟶ Z✝
g i : Y ⟶ Z✝
Z : Profinite
a b : Z ⟶ pullback f g
z : (forget Profinite).obj Z
hfst : ↑(a ≫ fst f g) z = ↑(b ≫ fst f g) z
hsnd : ↑(a ≫ snd f g) z = ↑(b ≫ snd f g) z
⊢ (↑(↑a z)).snd = (↑(↑b z)).snd

State before:
case w.a.h₁
α : Type
inst✝ : Fintype α
Z✝¹ : α → Profinite
X Y Z✝ : Profinite
f : X ⟶ Z✝
g i : Y ⟶ Z✝
Z : Profinite
a b : Z ⟶ pullback f g
z : (forget Profinite).obj Z
hfst : ↑(a ≫ fst f g) z = ↑(b ≫ fst f g) z
hsnd : ↑(a ≫ snd f g) z = ↑(b ≫ snd f g) z
⊢ (↑(↑a z)).fst = (↑(↑b z)).fst
Tactic:
exact hfst
State after:
no goals

State before:
case w.a.h₂
α : Type
inst✝ : Fintype α
Z✝¹ : α → Profinite
X Y Z✝ : Profinite
f : X ⟶ Z✝
g i : Y ⟶ Z✝
Z : Profinite
a b : Z ⟶ pullback f g
z : (forget Profinite).obj Z
hfst : ↑(a ≫ fst f g) z = ↑(b ≫ fst f g) z
hsnd : ↑(a ≫ snd f g) z = ↑(b ≫ snd f g) z
⊢ (↑(↑a z)).snd = (↑(↑b z)).snd
Tactic:
exact hsnd
State after:
no goals