From af8eed890c34bb9b7ca0aa05f10dfb15f7f42e53 Mon Sep 17 00:00:00 2001 From: Dagur Asgeirsson Date: Wed, 8 Jan 2025 12:15:24 +0000 Subject: [PATCH] chore(CategoryTheory): remove data produced by tactic block (#20565) --- .../CategoryTheory/EffectiveEpi/Coproduct.lean | 18 +++++------------- 1 file changed, 5 insertions(+), 13 deletions(-) diff --git a/Mathlib/CategoryTheory/EffectiveEpi/Coproduct.lean b/Mathlib/CategoryTheory/EffectiveEpi/Coproduct.lean index 80a53351c358d..87c5560d945e1 100644 --- a/Mathlib/CategoryTheory/EffectiveEpi/Coproduct.lean +++ b/Mathlib/CategoryTheory/EffectiveEpi/Coproduct.lean @@ -36,20 +36,12 @@ def effectiveEpiStructIsColimitDescOfEffectiveEpiFamily {B : C} {α : Type*} (X uniq e _ m hm := EffectiveEpiFamily.uniq X π (fun a ↦ c.ι.app ⟨a⟩ ≫ e) (fun _ _ _ _ hg ↦ (by simp [← hm, reassoc_of% hg])) m (fun _ ↦ (by simp [← hm])) -/-- -Given an `EffectiveEpiFamily X π` such that the coproduct of `X` exists, `Sigma.desc π` is an -`EffectiveEpi`. --/ -noncomputable -def effectiveEpiStructDescOfEffectiveEpiFamily {B : C} {α : Type*} (X : α → C) - (π : (a : α) → (X a ⟶ B)) [HasCoproduct X] [EffectiveEpiFamily X π] : - EffectiveEpiStruct (Sigma.desc π) := by - simpa [coproductIsCoproduct] using - effectiveEpiStructIsColimitDescOfEffectiveEpiFamily X _ (coproductIsCoproduct _) π - instance {B : C} {α : Type*} (X : α → C) (π : (a : α) → (X a ⟶ B)) [HasCoproduct X] - [EffectiveEpiFamily X π] : EffectiveEpi (Sigma.desc π) := - ⟨⟨effectiveEpiStructDescOfEffectiveEpiFamily X π⟩⟩ + [EffectiveEpiFamily X π] : EffectiveEpi (Sigma.desc π) := by + let e := effectiveEpiStructIsColimitDescOfEffectiveEpiFamily X _ (coproductIsCoproduct _) π + simp only [Cofan.mk_pt, coproductIsCoproduct, colimit.cocone_x, IsColimit.ofIsoColimit_desc, + Cocones.ext_inv_hom, Iso.refl_inv, colimit.isColimit_desc, Category.id_comp] at e + exact ⟨⟨e⟩⟩ example {B : C} {α : Type*} (X : α → C) (π : (a : α) → (X a ⟶ B)) [EffectiveEpiFamily X π] [HasCoproduct X] : Epi (Sigma.desc π) := inferInstance