Theorem: Profinite.toExplicitCompFromExcplict (Profinite/ExplicitLimits.lean)

State before:
α : Type
inst✝ : Fintype α
Z✝ : α → Profinite
X Y Z : Profinite
f : X ⟶ Z
g i : Y ⟶ Z
⊢ toExplicit f i ≫ fromExplicit f i = 𝟙 (Limits.pullback f i)
Tactic:
refine' Limits.pullback.hom_ext (k := (toExplicit f i ≫ fromExplicit f i)) _ _
State after:
case refine'_1
α : Type
inst✝ : Fintype α
Z✝ : α → Profinite
X Y Z : Profinite
f : X ⟶ Z
g i : Y ⟶ Z
⊢ (toExplicit f i ≫ fromExplicit f i) ≫ Limits.pullback.fst = 𝟙 (Limits.pullback f i) ≫ Limits.pullback.fst

case refine'_2
α : Type
inst✝ : Fintype α
Z✝ : α → Profinite
X Y Z : Profinite
f : X ⟶ Z
g i : Y ⟶ Z
⊢ (toExplicit f i ≫ fromExplicit f i) ≫ Limits.pullback.snd = 𝟙 (Limits.pullback f i) ≫ Limits.pullback.snd

State before:
case refine'_1
α : Type
inst✝ : Fintype α
Z✝ : α → Profinite
X Y Z : Profinite
f : X ⟶ Z
g i : Y ⟶ Z
⊢ (toExplicit f i ≫ fromExplicit f i) ≫ Limits.pullback.fst = 𝟙 (Limits.pullback f i) ≫ Limits.pullback.fst
Tactic:
simp [toExplicit, fromExplicit]
State after:
no goals

State before:
case refine'_2
α : Type
inst✝ : Fintype α
Z✝ : α → Profinite
X Y Z : Profinite
f : X ⟶ Z
g i : Y ⟶ Z
⊢ (toExplicit f i ≫ fromExplicit f i) ≫ Limits.pullback.snd = 𝟙 (Limits.pullback f i) ≫ Limits.pullback.snd
Tactic:
rw [Category.id_comp, Category.assoc, fromExplicit, Limits.pullback.lift_snd,
  toExplicit, pullback.lift_snd]
State after:
no goals