Theorem: Profinite.finiteCoproduct.ι_desc_apply (Profinite/ExplicitLimits.lean)

State before:
α✝ : Type
inst✝¹ : Fintype α✝
Z✝ : α✝ → Profinite
α : Type
inst✝ : Fintype α
X : Profinite
Z : α → Profinite
π : (a : α) → Z a ⟶ X
a : α
⊢ ∀ (x : (forget Profinite).obj (Z a)), ↑(desc Z π) (↑(ι Z a) x) = ↑(π a) x
Tactic:
intro x
State after:
α✝ : Type
inst✝¹ : Fintype α✝
Z✝ : α✝ → Profinite
α : Type
inst✝ : Fintype α
X : Profinite
Z : α → Profinite
π : (a : α) → Z a ⟶ X
a : α
x : (forget Profinite).obj (Z a)
⊢ ↑(desc Z π) (↑(ι Z a) x) = ↑(π a) x

State before:
α✝ : Type
inst✝¹ : Fintype α✝
Z✝ : α✝ → Profinite
α : Type
inst✝ : Fintype α
X : Profinite
Z : α → Profinite
π : (a : α) → Z a ⟶ X
a : α
x : (forget Profinite).obj (Z a)
⊢ ↑(desc Z π) (↑(ι Z a) x) = ↑(π a) x
Tactic:
change (ι Z a ≫ desc Z π) _ = _
State after:
α✝ : Type
inst✝¹ : Fintype α✝
Z✝ : α✝ → Profinite
α : Type
inst✝ : Fintype α
X : Profinite
Z : α → Profinite
π : (a : α) → Z a ⟶ X
a : α
x : (forget Profinite).obj (Z a)
⊢ ↑(ι Z a ≫ desc Z π) x = ↑(π a) x

State before:
α✝ : Type
inst✝¹ : Fintype α✝
Z✝ : α✝ → Profinite
α : Type
inst✝ : Fintype α
X : Profinite
Z : α → Profinite
π : (a : α) → Z a ⟶ X
a : α
x : (forget Profinite).obj (Z a)
⊢ ↑(ι Z a ≫ desc Z π) x = ↑(π a) x
Tactic:
simp only [ι_desc]
State after:
no goals