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

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

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

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