C : Type u
inst✝ : Category C
F : C ⥤ C
A A₀ A₁ A₂ : Algebra F
f : A₀ ⟶ A₁
g : A₁ ⟶ A₂
h : Limits.IsInitial A
⊢ F.map ((Limits.IsInitial.to h { a := F.obj A.a, str := F.map A.str }).f ≫ A.str) = F.map (𝟙 A.a)
C : Type u
inst✝ : Category C
F : C ⥤ C
A A₀ A₁ A₂ : Algebra F
f : A₀ ⟶ A₁
g : A₁ ⟶ A₂
h : Limits.IsInitial A
⊢ A.str ≫ strInv h = 𝟙 (F.obj A.a)
rw [strInv, ← (h.to ⟨F.obj A.1, F.map A.str⟩).h, ← F.map_id, ← F.map_comp]
case e_a
C : Type u
inst✝ : Category C
F : C ⥤ C
A A₀ A₁ A₂ : Algebra F
f : A₀ ⟶ A₁
g : A₁ ⟶ A₂
h : Limits.IsInitial A
⊢ (Limits.IsInitial.to h { a := F.obj A.a, str := F.map A.str }).f ≫ A.str = 𝟙 A.a
C : Type u
inst✝ : Category C
F : C ⥤ C
A A₀ A₁ A₂ : Algebra F
f : A₀ ⟶ A₁
g : A₁ ⟶ A₂
h : Limits.IsInitial A
⊢ F.map ((Limits.IsInitial.to h { a := F.obj A.a, str := F.map A.str }).f ≫ A.str) = F.map (𝟙 A.a)
congr
no goals
case e_a
C : Type u
inst✝ : Category C
F : C ⥤ C
A A₀ A₁ A₂ : Algebra F
f : A₀ ⟶ A₁
g : A₁ ⟶ A₂
h : Limits.IsInitial A
⊢ (Limits.IsInitial.to h { a := F.obj A.a, str := F.map A.str }).f ≫ A.str = 𝟙 A.a
exact left_inv h