[GOAL]
β : Type w
C : Type u
inst✝¹ : Category.{v, u} C
J : Type ?u.69019
f : J → C
inst✝ : HasProduct f
j j' : J
w : j = j'
⊢ f j = f j'
[PROOFSTEP]
simp [w]
[GOAL]
β : Type w
C : Type u
inst✝¹ : Category.{v, u} C
J : Type u_1
f : J → C
inst✝ : HasProduct f
j j' : J
w : j = j'
⊢ π f j ≫ eqToHom (_ : f j = f j') = π f j'
[PROOFSTEP]
cases w
[GOAL]
case refl
β : Type w
C : Type u
inst✝¹ : Category.{v, u} C
J : Type u_1
f : J → C
inst✝ : HasProduct f
j : J
⊢ π f j ≫ eqToHom (_ : f j = f j) = π f j
[PROOFSTEP]
simp
  -- The `simpNF` linter incorrectly identifies these as simp lemmas that could never apply.
  -- https://github.com/leanprover-community/mathlib4/issues/5049
  -- They are used by `simp` in `Sigma.whisker_equiv` below.
[GOAL]
β : Type w
C : Type u
inst✝¹ : Category.{v, u} C
J : Type ?u.69987
f : J → C
inst✝ : HasCoproduct f
j j' : J
w : j = j'
⊢ f j = f j'
[PROOFSTEP]
simp [w]
[GOAL]
β : Type w
C : Type u
inst✝¹ : Category.{v, u} C
J : Type u_1
f : J → C
inst✝ : HasCoproduct f
j j' : J
w : j = j'
⊢ eqToHom (_ : f j = f j') ≫ ι f j' = ι f j
[PROOFSTEP]
cases w
[GOAL]
case refl
β : Type w
C : Type u
inst✝¹ : Category.{v, u} C
J : Type u_1
f : J → C
inst✝ : HasCoproduct f
j : J
⊢ eqToHom (_ : f j = f j) ≫ ι f j = ι f j
[PROOFSTEP]
simp
[GOAL]
β : Type w
C : Type u
inst✝³ : Category.{v, u} C
f g : β → C
inst✝² : HasProduct f
inst✝¹ : HasProduct g
p : (b : β) → f b ⟶ g b
inst✝ : ∀ (i : β), Mono (p i)
⊢ ∀ (j : Discrete β), Mono (NatTrans.app (Discrete.natTrans fun X => p X.as) j)
[PROOFSTEP]
dsimp
[GOAL]
β : Type w
C : Type u
inst✝³ : Category.{v, u} C
f g : β → C
inst✝² : HasProduct f
inst✝¹ : HasProduct g
p : (b : β) → f b ⟶ g b
inst✝ : ∀ (i : β), Mono (p i)
⊢ ∀ (j : Discrete β), Mono (p j.as)
[PROOFSTEP]
infer_instance
[GOAL]
β : Type w
C : Type u
inst✝³ : Category.{v, u} C
f g : β → C
inst✝² : HasCoproduct f
inst✝¹ : HasCoproduct g
p : (b : β) → f b ⟶ g b
inst✝ : ∀ (i : β), Epi (p i)
⊢ ∀ (j : Discrete β), Epi (NatTrans.app (Discrete.natTrans fun X => p X.as) j)
[PROOFSTEP]
dsimp
[GOAL]
β : Type w
C : Type u
inst✝³ : Category.{v, u} C
f g : β → C
inst✝² : HasCoproduct f
inst✝¹ : HasCoproduct g
p : (b : β) → f b ⟶ g b
inst✝ : ∀ (i : β), Epi (p i)
⊢ ∀ (j : Discrete β), Epi (p j.as)
[PROOFSTEP]
infer_instance
[GOAL]
β : Type w
C : Type u
inst✝² : Category.{v, u} C
J : Type ?u.78866
K : Type ?u.78950
f : J → C
g : K → C
e : J ≃ K
w : (j : J) → g (↑e j) ≅ f j
inst✝¹ : HasProduct f
inst✝ : HasProduct g
k : K
⊢ g (↑e (↑e.symm k)) = g k
[PROOFSTEP]
simp
[GOAL]
β : Type w
C : Type u
inst✝² : Category.{v, u} C
J : Type ?u.94443
K : Type ?u.94527
f : J → C
g : K → C
e : J ≃ K
w : (j : J) → g (↑e j) ≅ f j
inst✝¹ : HasCoproduct f
inst✝ : HasCoproduct g
k : K
⊢ g k = g (↑e (↑e.symm k))
[PROOFSTEP]
simp
[GOAL]
β : Type w
C : Type u
inst✝³ : Category.{v, u} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
f : β → C
inst✝¹ : HasProduct f
inst✝ : HasProduct fun b => G.obj (f b)
P : C
g : (j : β) → P ⟶ f j
⊢ G.map (Pi.lift g) ≫ piComparison G f = Pi.lift fun j => G.map (g j)
[PROOFSTEP]
ext j
[GOAL]
case h
β : Type w
C : Type u
inst✝³ : Category.{v, u} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
f : β → C
inst✝¹ : HasProduct f
inst✝ : HasProduct fun b => G.obj (f b)
P : C
g : (j : β) → P ⟶ f j
j : β
⊢ (G.map (Pi.lift g) ≫ piComparison G f) ≫ Pi.π (fun b => G.obj (f b)) j =
    (Pi.lift fun j => G.map (g j)) ≫ Pi.π (fun b => G.obj (f b)) j
[PROOFSTEP]
simp only [Discrete.functor_obj, Category.assoc, piComparison_comp_π, ← G.map_comp, limit.lift_π, Fan.mk_pt,
  Fan.mk_π_app]
[GOAL]
β : Type w
C : Type u
inst✝³ : Category.{v, u} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
f : β → C
inst✝¹ : HasCoproduct f
inst✝ : HasCoproduct fun b => G.obj (f b)
P : C
g : (j : β) → f j ⟶ P
⊢ sigmaComparison G f ≫ G.map (Sigma.desc g) = Sigma.desc fun j => G.map (g j)
[PROOFSTEP]
ext j
[GOAL]
case h
β : Type w
C : Type u
inst✝³ : Category.{v, u} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
f : β → C
inst✝¹ : HasCoproduct f
inst✝ : HasCoproduct fun b => G.obj (f b)
P : C
g : (j : β) → f j ⟶ P
j : β
⊢ Sigma.ι (fun b => G.obj (f b)) j ≫ sigmaComparison G f ≫ G.map (Sigma.desc g) =
    Sigma.ι (fun b => G.obj (f b)) j ≫ Sigma.desc fun j => G.map (g j)
[PROOFSTEP]
simp only [Discrete.functor_obj, ι_comp_sigmaComparison_assoc, ← G.map_comp, colimit.ι_desc, Cofan.mk_pt,
  Cofan.mk_ι_app]
[GOAL]
β : Type w
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Unique β
f : β → C
x✝ : Discrete β
j : β
⊢ ((Functor.const (Discrete β)).obj (f default)).obj { as := j } = (Discrete.functor f).obj { as := j }
[PROOFSTEP]
dsimp
[GOAL]
β : Type w
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Unique β
f : β → C
x✝ : Discrete β
j : β
⊢ f default = f j
[PROOFSTEP]
congr
[GOAL]
case e_a
β : Type w
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Unique β
f : β → C
x✝ : Discrete β
j : β
⊢ default = j
[PROOFSTEP]
apply Subsingleton.elim
[GOAL]
β : Type w
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Unique β
f : β → C
s : Cone (Discrete.functor f)
j : Discrete β
⊢ (fun s => NatTrans.app s.π default) s ≫
      NatTrans.app
        { pt := f default,
            π :=
              Discrete.natTrans fun x =>
                match x with
                | { as := j } =>
                  eqToHom
                    (_ :
                      ((Functor.const (Discrete β)).obj (f default)).obj { as := j } =
                        (Discrete.functor f).obj { as := j }) }.π
        j =
    NatTrans.app s.π j
[PROOFSTEP]
have h := Subsingleton.elim j default
[GOAL]
β : Type w
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Unique β
f : β → C
s : Cone (Discrete.functor f)
j : Discrete β
h : j = default
⊢ (fun s => NatTrans.app s.π default) s ≫
      NatTrans.app
        { pt := f default,
            π :=
              Discrete.natTrans fun x =>
                match x with
                | { as := j } =>
                  eqToHom
                    (_ :
                      ((Functor.const (Discrete β)).obj (f default)).obj { as := j } =
                        (Discrete.functor f).obj { as := j }) }.π
        j =
    NatTrans.app s.π j
[PROOFSTEP]
subst h
[GOAL]
β : Type w
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Unique β
f : β → C
s : Cone (Discrete.functor f)
⊢ (fun s => NatTrans.app s.π default) s ≫
      NatTrans.app
        { pt := f default,
            π :=
              Discrete.natTrans fun x =>
                match x with
                | { as := j } =>
                  eqToHom
                    (_ :
                      ((Functor.const (Discrete β)).obj (f default)).obj { as := j } =
                        (Discrete.functor f).obj { as := j }) }.π
        default =
    NatTrans.app s.π default
[PROOFSTEP]
simp
[GOAL]
β : Type w
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Unique β
f : β → C
s : Cone (Discrete.functor f)
m :
  s.pt ⟶
    { pt := f default,
        π :=
          Discrete.natTrans fun x =>
            match x with
            | { as := j } =>
              eqToHom
                (_ :
                  ((Functor.const (Discrete β)).obj (f default)).obj { as := j } =
                    (Discrete.functor f).obj { as := j }) }.pt
w :
  ∀ (j : Discrete β),
    m ≫
        NatTrans.app
          { pt := f default,
              π :=
                Discrete.natTrans fun x =>
                  match x with
                  | { as := j } =>
                    eqToHom
                      (_ :
                        ((Functor.const (Discrete β)).obj (f default)).obj { as := j } =
                          (Discrete.functor f).obj { as := j }) }.π
          j =
      NatTrans.app s.π j
⊢ m = (fun s => NatTrans.app s.π default) s
[PROOFSTEP]
specialize w default
[GOAL]
β : Type w
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Unique β
f : β → C
s : Cone (Discrete.functor f)
m :
  s.pt ⟶
    { pt := f default,
        π :=
          Discrete.natTrans fun x =>
            match x with
            | { as := j } =>
              eqToHom
                (_ :
                  ((Functor.const (Discrete β)).obj (f default)).obj { as := j } =
                    (Discrete.functor f).obj { as := j }) }.pt
w :
  m ≫
      NatTrans.app
        { pt := f default,
            π :=
              Discrete.natTrans fun x =>
                match x with
                | { as := j } =>
                  eqToHom
                    (_ :
                      ((Functor.const (Discrete β)).obj (f default)).obj { as := j } =
                        (Discrete.functor f).obj { as := j }) }.π
        default =
    NatTrans.app s.π default
⊢ m = (fun s => NatTrans.app s.π default) s
[PROOFSTEP]
simpa using w
[GOAL]
β : Type w
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Unique β
f : β → C
x✝ : Discrete β
j : β
⊢ (Discrete.functor f).obj { as := j } = ((Functor.const (Discrete β)).obj (f default)).obj { as := j }
[PROOFSTEP]
dsimp
[GOAL]
β : Type w
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Unique β
f : β → C
x✝ : Discrete β
j : β
⊢ f j = f default
[PROOFSTEP]
congr
[GOAL]
case e_a
β : Type w
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Unique β
f : β → C
x✝ : Discrete β
j : β
⊢ j = default
[PROOFSTEP]
apply Subsingleton.elim
[GOAL]
β : Type w
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Unique β
f : β → C
s : Cocone (Discrete.functor f)
j : Discrete β
⊢ NatTrans.app
        { pt := f default,
            ι :=
              Discrete.natTrans fun x =>
                match x with
                | { as := j } =>
                  eqToHom
                    (_ :
                      (Discrete.functor f).obj { as := j } =
                        ((Functor.const (Discrete β)).obj (f default)).obj { as := j }) }.ι
        j ≫
      (fun s => NatTrans.app s.ι default) s =
    NatTrans.app s.ι j
[PROOFSTEP]
have h := Subsingleton.elim j default
[GOAL]
β : Type w
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Unique β
f : β → C
s : Cocone (Discrete.functor f)
j : Discrete β
h : j = default
⊢ NatTrans.app
        { pt := f default,
            ι :=
              Discrete.natTrans fun x =>
                match x with
                | { as := j } =>
                  eqToHom
                    (_ :
                      (Discrete.functor f).obj { as := j } =
                        ((Functor.const (Discrete β)).obj (f default)).obj { as := j }) }.ι
        j ≫
      (fun s => NatTrans.app s.ι default) s =
    NatTrans.app s.ι j
[PROOFSTEP]
subst h
[GOAL]
β : Type w
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Unique β
f : β → C
s : Cocone (Discrete.functor f)
⊢ NatTrans.app
        { pt := f default,
            ι :=
              Discrete.natTrans fun x =>
                match x with
                | { as := j } =>
                  eqToHom
                    (_ :
                      (Discrete.functor f).obj { as := j } =
                        ((Functor.const (Discrete β)).obj (f default)).obj { as := j }) }.ι
        default ≫
      (fun s => NatTrans.app s.ι default) s =
    NatTrans.app s.ι default
[PROOFSTEP]
apply Category.id_comp
[GOAL]
β : Type w
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Unique β
f : β → C
s : Cocone (Discrete.functor f)
m :
  { pt := f default,
        ι :=
          Discrete.natTrans fun x =>
            match x with
            | { as := j } =>
              eqToHom
                (_ :
                  (Discrete.functor f).obj { as := j } =
                    ((Functor.const (Discrete β)).obj (f default)).obj { as := j }) }.pt ⟶
    s.pt
w :
  ∀ (j : Discrete β),
    NatTrans.app
          { pt := f default,
              ι :=
                Discrete.natTrans fun x =>
                  match x with
                  | { as := j } =>
                    eqToHom
                      (_ :
                        (Discrete.functor f).obj { as := j } =
                          ((Functor.const (Discrete β)).obj (f default)).obj { as := j }) }.ι
          j ≫
        m =
      NatTrans.app s.ι j
⊢ m = (fun s => NatTrans.app s.ι default) s
[PROOFSTEP]
specialize w default
[GOAL]
β : Type w
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Unique β
f : β → C
s : Cocone (Discrete.functor f)
m :
  { pt := f default,
        ι :=
          Discrete.natTrans fun x =>
            match x with
            | { as := j } =>
              eqToHom
                (_ :
                  (Discrete.functor f).obj { as := j } =
                    ((Functor.const (Discrete β)).obj (f default)).obj { as := j }) }.pt ⟶
    s.pt
w :
  NatTrans.app
        { pt := f default,
            ι :=
              Discrete.natTrans fun x =>
                match x with
                | { as := j } =>
                  eqToHom
                    (_ :
                      (Discrete.functor f).obj { as := j } =
                        ((Functor.const (Discrete β)).obj (f default)).obj { as := j }) }.ι
        default ≫
      m =
    NatTrans.app s.ι default
⊢ m = (fun s => NatTrans.app s.ι default) s
[PROOFSTEP]
erw [Category.id_comp] at w 
[GOAL]
β : Type w
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Unique β
f : β → C
s : Cocone (Discrete.functor f)
m :
  { pt := f default,
        ι :=
          Discrete.natTrans fun x =>
            match x with
            | { as := j } =>
              eqToHom
                (_ :
                  (Discrete.functor f).obj { as := j } =
                    ((Functor.const (Discrete β)).obj (f default)).obj { as := j }) }.pt ⟶
    s.pt
w : m = NatTrans.app s.ι default
⊢ m = (fun s => NatTrans.app s.ι default) s
[PROOFSTEP]
exact w
[GOAL]
β : Type w
C : Type u
inst✝² : Category.{v, u} C
γ : Type v
ε : β ≃ γ
f : γ → C
inst✝¹ : HasProduct f
inst✝ : HasProduct (f ∘ ↑ε)
b : β
⊢ (reindex ε f).hom ≫ π f (↑ε b) = π (f ∘ ↑ε) b
[PROOFSTEP]
dsimp [Pi.reindex]
[GOAL]
β : Type w
C : Type u
inst✝² : Category.{v, u} C
γ : Type v
ε : β ≃ γ
f : γ → C
inst✝¹ : HasProduct f
inst✝ : HasProduct (f ∘ ↑ε)
b : β
⊢ (HasLimit.isoOfEquivalence (Discrete.equivalence ε)
          (Discrete.natIso fun x =>
            Iso.refl ((Discrete.functor f).obj ((Discrete.functor (Discrete.mk ∘ ↑ε)).obj x)))).hom ≫
      π f (↑ε b) =
    π (f ∘ ↑ε) b
[PROOFSTEP]
simp only [HasLimit.isoOfEquivalence_hom_π, Discrete.equivalence_inverse, Discrete.functor_obj, Function.comp_apply,
  Functor.id_obj, Discrete.equivalence_functor, Functor.comp_obj, Discrete.natIso_inv_app, Iso.refl_inv,
  Category.id_comp]
[GOAL]
β : Type w
C : Type u
inst✝² : Category.{v, u} C
γ : Type v
ε : β ≃ γ
f : γ → C
inst✝¹ : HasProduct f
inst✝ : HasProduct (f ∘ ↑ε)
b : β
⊢ limit.π (Discrete.functor (f ∘ ↑ε)) { as := ↑ε.symm (↑ε b) } ≫
      (Discrete.functor f).map (NatTrans.app (Equivalence.counit (Discrete.equivalence ε)) { as := ↑ε b }) =
    π (f ∘ ↑ε) b
[PROOFSTEP]
exact limit.w (Discrete.functor (f ∘ ε)) (Discrete.eqToHom' (ε.symm_apply_apply b))
[GOAL]
β : Type w
C : Type u
inst✝² : Category.{v, u} C
γ : Type v
ε : β ≃ γ
f : γ → C
inst✝¹ : HasProduct f
inst✝ : HasProduct (f ∘ ↑ε)
b : β
⊢ (reindex ε f).inv ≫ π (f ∘ ↑ε) b = π f (↑ε b)
[PROOFSTEP]
simp [Iso.inv_comp_eq]
[GOAL]
β : Type w
C : Type u
inst✝² : Category.{v, u} C
γ : Type v
ε : β ≃ γ
f : γ → C
inst✝¹ : HasCoproduct f
inst✝ : HasCoproduct (f ∘ ↑ε)
b : β
⊢ ι (f ∘ ↑ε) b ≫ (reindex ε f).hom = ι f (↑ε b)
[PROOFSTEP]
dsimp [Sigma.reindex]
[GOAL]
β : Type w
C : Type u
inst✝² : Category.{v, u} C
γ : Type v
ε : β ≃ γ
f : γ → C
inst✝¹ : HasCoproduct f
inst✝ : HasCoproduct (f ∘ ↑ε)
b : β
⊢ ι (f ∘ ↑ε) b ≫
      (HasColimit.isoOfEquivalence (Discrete.equivalence ε)
          (Discrete.natIso fun x =>
            Iso.refl ((Discrete.functor f).obj ((Discrete.functor (Discrete.mk ∘ ↑ε)).obj x)))).hom =
    ι f (↑ε b)
[PROOFSTEP]
simp only [HasColimit.isoOfEquivalence_hom_π, Functor.id_obj, Discrete.functor_obj, Function.comp_apply,
  Discrete.equivalence_functor, Discrete.equivalence_inverse, Functor.comp_obj, Discrete.natIso_inv_app, Iso.refl_inv,
  Category.id_comp]
[GOAL]
β : Type w
C : Type u
inst✝² : Category.{v, u} C
γ : Type v
ε : β ≃ γ
f : γ → C
inst✝¹ : HasCoproduct f
inst✝ : HasCoproduct (f ∘ ↑ε)
b : β
⊢ (Discrete.functor (f ∘ ↑ε)).map (NatTrans.app (Equivalence.unit (Discrete.equivalence ε)) { as := b }) ≫
      colimit.ι (Discrete.functor f) { as := ↑ε (↑ε.symm (↑ε b)) } =
    ι f (↑ε b)
[PROOFSTEP]
have h := colimit.w (Discrete.functor f) (Discrete.eqToHom' (ε.apply_symm_apply (ε b)))
[GOAL]
β : Type w
C : Type u
inst✝² : Category.{v, u} C
γ : Type v
ε : β ≃ γ
f : γ → C
inst✝¹ : HasCoproduct f
inst✝ : HasCoproduct (f ∘ ↑ε)
b : β
h :
  (Discrete.functor f).map (Discrete.eqToHom' (_ : ↑ε (↑ε.symm (↑ε b)) = ↑ε b)) ≫
      colimit.ι (Discrete.functor f) { as := ↑ε b } =
    colimit.ι (Discrete.functor f) { as := ↑ε (↑ε.symm (↑ε b)) }
⊢ (Discrete.functor (f ∘ ↑ε)).map (NatTrans.app (Equivalence.unit (Discrete.equivalence ε)) { as := b }) ≫
      colimit.ι (Discrete.functor f) { as := ↑ε (↑ε.symm (↑ε b)) } =
    ι f (↑ε b)
[PROOFSTEP]
simp only [Discrete.functor_obj] at h 
[GOAL]
β : Type w
C : Type u
inst✝² : Category.{v, u} C
γ : Type v
ε : β ≃ γ
f : γ → C
inst✝¹ : HasCoproduct f
inst✝ : HasCoproduct (f ∘ ↑ε)
b : β
h :
  (Discrete.functor f).map (Discrete.eqToHom' (_ : ↑ε (↑ε.symm (↑ε b)) = ↑ε b)) ≫
      colimit.ι (Discrete.functor f) { as := ↑ε b } =
    colimit.ι (Discrete.functor f) { as := ↑ε (↑ε.symm (↑ε b)) }
⊢ (Discrete.functor (f ∘ ↑ε)).map (NatTrans.app (Equivalence.unit (Discrete.equivalence ε)) { as := b }) ≫
      colimit.ι (Discrete.functor f) { as := ↑ε (↑ε.symm (↑ε b)) } =
    ι f (↑ε b)
[PROOFSTEP]
erw [← h, eqToHom_map, eqToHom_map, eqToHom_trans_assoc]
[GOAL]
β : Type w
C : Type u
inst✝² : Category.{v, u} C
γ : Type v
ε : β ≃ γ
f : γ → C
inst✝¹ : HasCoproduct f
inst✝ : HasCoproduct (f ∘ ↑ε)
b : β
h :
  (Discrete.functor f).map (Discrete.eqToHom' (_ : ↑ε (↑ε.symm (↑ε b)) = ↑ε b)) ≫
      colimit.ι (Discrete.functor f) { as := ↑ε b } =
    colimit.ι (Discrete.functor f) { as := ↑ε (↑ε.symm (↑ε b)) }
⊢ eqToHom (_ : f (↑ε b) = f (↑ε b)) ≫ colimit.ι (Discrete.functor f) { as := ↑ε b } = ι f (↑ε b)
case p
β : Type w
C : Type u
inst✝² : Category.{v, u} C
γ : Type v
ε : β ≃ γ
f : γ → C
inst✝¹ : HasCoproduct f
inst✝ : HasCoproduct (f ∘ ↑ε)
b : β
h :
  (Discrete.functor f).map (Discrete.eqToHom' (_ : ↑ε (↑ε.symm (↑ε b)) = ↑ε b)) ≫
      colimit.ι (Discrete.functor f) { as := ↑ε b } =
    colimit.ι (Discrete.functor f) { as := ↑ε (↑ε.symm (↑ε b)) }
⊢ { as := b } = { as := ↑ε.symm (↑ε b) }
case p
β : Type w
C : Type u
inst✝² : Category.{v, u} C
γ : Type v
ε : β ≃ γ
f : γ → C
inst✝¹ : HasCoproduct f
inst✝ : HasCoproduct (f ∘ ↑ε)
b : β
h :
  (Discrete.functor f).map (Discrete.eqToHom' (_ : ↑ε (↑ε.symm (↑ε b)) = ↑ε b)) ≫
      colimit.ι (Discrete.functor f) { as := ↑ε b } =
    colimit.ι (Discrete.functor f) { as := ↑ε (↑ε.symm (↑ε b)) }
⊢ { as := b } = { as := ↑ε.symm (↑ε b) }
case p
β : Type w
C : Type u
inst✝² : Category.{v, u} C
γ : Type v
ε : β ≃ γ
f : γ → C
inst✝¹ : HasCoproduct f
inst✝ : HasCoproduct (f ∘ ↑ε)
b : β
h :
  (Discrete.functor f).map (Discrete.eqToHom' (_ : ↑ε (↑ε.symm (↑ε b)) = ↑ε b)) ≫
      colimit.ι (Discrete.functor f) { as := ↑ε b } =
    colimit.ι (Discrete.functor f) { as := ↑ε (↑ε.symm (↑ε b)) }
⊢ { as := b } = { as := ↑ε.symm (↑ε b) }
[PROOFSTEP]
all_goals {simp
}
[GOAL]
β : Type w
C : Type u
inst✝² : Category.{v, u} C
γ : Type v
ε : β ≃ γ
f : γ → C
inst✝¹ : HasCoproduct f
inst✝ : HasCoproduct (f ∘ ↑ε)
b : β
h :
  (Discrete.functor f).map (Discrete.eqToHom' (_ : ↑ε (↑ε.symm (↑ε b)) = ↑ε b)) ≫
      colimit.ι (Discrete.functor f) { as := ↑ε b } =
    colimit.ι (Discrete.functor f) { as := ↑ε (↑ε.symm (↑ε b)) }
⊢ eqToHom (_ : f (↑ε b) = f (↑ε b)) ≫ colimit.ι (Discrete.functor f) { as := ↑ε b } = ι f (↑ε b)
[PROOFSTEP]
{simp
}
[GOAL]
β : Type w
C : Type u
inst✝² : Category.{v, u} C
γ : Type v
ε : β ≃ γ
f : γ → C
inst✝¹ : HasCoproduct f
inst✝ : HasCoproduct (f ∘ ↑ε)
b : β
h :
  (Discrete.functor f).map (Discrete.eqToHom' (_ : ↑ε (↑ε.symm (↑ε b)) = ↑ε b)) ≫
      colimit.ι (Discrete.functor f) { as := ↑ε b } =
    colimit.ι (Discrete.functor f) { as := ↑ε (↑ε.symm (↑ε b)) }
⊢ eqToHom (_ : f (↑ε b) = f (↑ε b)) ≫ colimit.ι (Discrete.functor f) { as := ↑ε b } = ι f (↑ε b)
[PROOFSTEP]
simp
[GOAL]
case p
β : Type w
C : Type u
inst✝² : Category.{v, u} C
γ : Type v
ε : β ≃ γ
f : γ → C
inst✝¹ : HasCoproduct f
inst✝ : HasCoproduct (f ∘ ↑ε)
b : β
h :
  (Discrete.functor f).map (Discrete.eqToHom' (_ : ↑ε (↑ε.symm (↑ε b)) = ↑ε b)) ≫
      colimit.ι (Discrete.functor f) { as := ↑ε b } =
    colimit.ι (Discrete.functor f) { as := ↑ε (↑ε.symm (↑ε b)) }
⊢ { as := b } = { as := ↑ε.symm (↑ε b) }
[PROOFSTEP]
{simp
}
[GOAL]
case p
β : Type w
C : Type u
inst✝² : Category.{v, u} C
γ : Type v
ε : β ≃ γ
f : γ → C
inst✝¹ : HasCoproduct f
inst✝ : HasCoproduct (f ∘ ↑ε)
b : β
h :
  (Discrete.functor f).map (Discrete.eqToHom' (_ : ↑ε (↑ε.symm (↑ε b)) = ↑ε b)) ≫
      colimit.ι (Discrete.functor f) { as := ↑ε b } =
    colimit.ι (Discrete.functor f) { as := ↑ε (↑ε.symm (↑ε b)) }
⊢ { as := b } = { as := ↑ε.symm (↑ε b) }
[PROOFSTEP]
simp
[GOAL]
β : Type w
C : Type u
inst✝² : Category.{v, u} C
γ : Type v
ε : β ≃ γ
f : γ → C
inst✝¹ : HasCoproduct f
inst✝ : HasCoproduct (f ∘ ↑ε)
b : β
⊢ ι f (↑ε b) ≫ (reindex ε f).inv = ι (f ∘ ↑ε) b
[PROOFSTEP]
simp [Iso.comp_inv_eq]
