Theorem: CategoryTheory.ExtrDisc.pullback.hom_ext (ExtrDisc/Pullback.lean)

State before:
X Y Z W : ExtrDisc
f : X ⟶ Z
i : Y ⟶ Z
hi : OpenEmbedding ↑i
a b : W ⟶ (OpenEmbeddingCone f hi).pt
hfst : a ≫ fst f hi = b ≫ fst f hi
⊢ a = b
Tactic:
ext z
State after:
case w
X Y Z W : ExtrDisc
f : X ⟶ Z
i : Y ⟶ Z
hi : OpenEmbedding ↑i
a b : W ⟶ (OpenEmbeddingCone f hi).pt
hfst : a ≫ fst f hi = b ≫ fst f hi
z : (forget ExtrDisc).obj W
⊢ ↑a z = ↑b z

State before:
case w
X Y Z W : ExtrDisc
f : X ⟶ Z
i : Y ⟶ Z
hi : OpenEmbedding ↑i
a b : W ⟶ (OpenEmbeddingCone f hi).pt
hfst : a ≫ fst f hi = b ≫ fst f hi
z : (forget ExtrDisc).obj W
⊢ ↑a z = ↑b z
Tactic:
apply_fun (fun q => q z) at hfst
State after:
case w
X Y Z W : ExtrDisc
f : X ⟶ Z
i : Y ⟶ Z
hi : OpenEmbedding ↑i
a b : W ⟶ (OpenEmbeddingCone f hi).pt
z : (forget ExtrDisc).obj W
hfst : ↑(a ≫ fst f hi) z = ↑(b ≫ fst f hi) z
⊢ ↑a z = ↑b z

State before:
case w
X Y Z W : ExtrDisc
f : X ⟶ Z
i : Y ⟶ Z
hi : OpenEmbedding ↑i
a b : W ⟶ (OpenEmbeddingCone f hi).pt
z : (forget ExtrDisc).obj W
hfst : ↑(a ≫ fst f hi) z = ↑(b ≫ fst f hi) z
⊢ ↑a z = ↑b z
Tactic:
apply Subtype.ext
State after:
case w.a
X Y Z W : ExtrDisc
f : X ⟶ Z
i : Y ⟶ Z
hi : OpenEmbedding ↑i
a b : W ⟶ (OpenEmbeddingCone f hi).pt
z : (forget ExtrDisc).obj W
hfst : ↑(a ≫ fst f hi) z = ↑(b ≫ fst f hi) z
⊢ ↑(↑a z) = ↑(↑b z)

State before:
case w.a
X Y Z W : ExtrDisc
f : X ⟶ Z
i : Y ⟶ Z
hi : OpenEmbedding ↑i
a b : W ⟶ (OpenEmbeddingCone f hi).pt
z : (forget ExtrDisc).obj W
hfst : ↑(a ≫ fst f hi) z = ↑(b ≫ fst f hi) z
⊢ ↑(↑a z) = ↑(↑b z)
Tactic:
exact hfst
State after:
no goals