[GOAL]
C : Type u
inst✝ : Category.{v, u} C
β : Type u_1
X Y : GradedObject β C
f g : X ⟶ Y
h : ∀ (x : β), f x = g x
⊢ f = g
[PROOFSTEP]
funext
[GOAL]
case h
C : Type u
inst✝ : Category.{v, u} C
β : Type u_1
X Y : GradedObject β C
f g : X ⟶ Y
h : ∀ (x : β), f x = g x
x✝ : β
⊢ f x✝ = g x✝
[PROOFSTEP]
apply h
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
I : Type u_1
x x' : GradedObject I C
h : x = x'
i : I
⊢ eqToHom h i = eqToHom (_ : x i = x' i)
[PROOFSTEP]
subst h
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
I : Type u_1
x : GradedObject I C
i : I
⊢ eqToHom (_ : x = x) i = eqToHom (_ : x i = x i)
[PROOFSTEP]
rfl
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
β γ : Type w
f g : β → γ
h : f = g
X : GradedObject γ C
b : β
⊢ (comap C f).obj X b = (comap C g).obj X b
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
β γ : Type w
f g : β → γ
h : f = g
X : GradedObject γ C
b : β
⊢ X (f b) = X (g b)
[PROOFSTEP]
simp only [h]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
β γ : Type w
f g : β → γ
h : f = g
X : GradedObject γ C
b : β
⊢ (comap C g).obj X b = (comap C f).obj X b
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
β γ : Type w
f g : β → γ
h : f = g
X : GradedObject γ C
b : β
⊢ X (g b) = X (f b)
[PROOFSTEP]
simp only [h]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
β γ : Type w
f g : β → γ
h : f = g
⊢ comapEq C (_ : g = f) = (comapEq C h).symm
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
β γ : Type w
f g h : β → γ
k : f = g
l : g = h
⊢ comapEq C (_ : f = h) = comapEq C k ≪≫ comapEq C l
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
β : Type w
X Y : β → C
h : X = Y
b : β
⊢ X b = Y b
[PROOFSTEP]
rw [h]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
β : Type w
X Y : β → C
h : X = Y
b : β
⊢ eqToHom h b = eqToHom (_ : X b = Y b)
[PROOFSTEP]
subst h
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
β : Type w
X : β → C
b : β
⊢ eqToHom (_ : X = X) b = eqToHom (_ : X b = X b)
[PROOFSTEP]
rfl
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
β γ : Type w
e : β ≃ γ
⊢ (fun i => i) = ↑e.symm ∘ ↑e
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u
inst✝ : Category.{v, u} C
β γ : Type w
e : β ≃ γ
x✝ : β
⊢ x✝ = (↑e.symm ∘ ↑e) x✝
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
β γ : Type w
e : β ≃ γ
⊢ ↑e ∘ ↑e.symm = fun i => i
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u
inst✝ : Category.{v, u} C
β γ : Type w
e : β ≃ γ
x✝ : γ
⊢ (↑e ∘ ↑e.symm) x✝ = x✝
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
β : Type u_1
inst✝ : AddCommGroup β
s : β
⊢ (fun b => b + 0 • s) = id
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
β : Type u_1
inst✝ : AddCommGroup β
s : β
m n : ℤ
⊢ (fun b => b + (m + n) • s) = (fun b => b + m • s) ∘ fun b => b + n • s
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u
inst✝¹ : Category.{v, u} C
β : Type u_1
inst✝ : AddCommGroup β
s : β
m n : ℤ
x✝ : β
⊢ x✝ + (m + n) • s = ((fun b => b + m • s) ∘ fun b => b + n • s) x✝
[PROOFSTEP]
dsimp
[GOAL]
case h
C : Type u
inst✝¹ : Category.{v, u} C
β : Type u_1
inst✝ : AddCommGroup β
s : β
m n : ℤ
x✝ : β
⊢ x✝ + (m + n) • s = x✝ + n • s + m • s
[PROOFSTEP]
rw [add_comm m n, add_zsmul, add_assoc]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
β : Type w
⊢ HasZeroObject (GradedObject β C)
[PROOFSTEP]
refine' ⟨⟨fun _ => 0, fun X => ⟨⟨⟨fun b => 0⟩, fun f => _⟩⟩, fun X => ⟨⟨⟨fun b => 0⟩, fun f => _⟩⟩⟩⟩
[GOAL]
case refine'_1
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
β : Type w
X : GradedObject β C
f : (fun x => 0) ⟶ X
⊢ f = default
[PROOFSTEP]
aesop_cat
[GOAL]
case refine'_2
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
β : Type w
X : GradedObject β C
f : X ⟶ fun x => 0
⊢ f = default
[PROOFSTEP]
aesop_cat
[GOAL]
β : Type
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasCoproducts C
inst✝ : HasZeroMorphisms C
X Y : GradedObject β C
f g : X ⟶ Y
w : (total β C).map f = (total β C).map g
⊢ f = g
[PROOFSTEP]
ext i
[GOAL]
case h
β : Type
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasCoproducts C
inst✝ : HasZeroMorphisms C
X Y : GradedObject β C
f g : X ⟶ Y
w : (total β C).map f = (total β C).map g
i : β
⊢ f i = g i
[PROOFSTEP]
replace w := Sigma.ι (fun i : β => X i) i ≫= w
[GOAL]
case h
β : Type
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasCoproducts C
inst✝ : HasZeroMorphisms C
X Y : GradedObject β C
f g : X ⟶ Y
i : β
w : Sigma.ι (fun i => X i) i ≫ (total β C).map f = Sigma.ι (fun i => X i) i ≫ (total β C).map g
⊢ f i = g i
[PROOFSTEP]
erw [colimit.ι_map, colimit.ι_map] at w 
[GOAL]
case h
β : Type
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasCoproducts C
inst✝ : HasZeroMorphisms C
X Y : GradedObject β C
f g : X ⟶ Y
i : β
w✝¹ : Sigma.ι (fun i => X i) i ≫ (total β C).map f = Sigma.ι (fun i => X i) i ≫ (total β C).map g
w✝ :
  NatTrans.app (Discrete.natTrans fun X => (fun i => f i) X.as) { as := i } ≫
      colimit.ι (Discrete.functor fun i => Y i) { as := i } =
    Sigma.ι (fun i => X i) i ≫ (total β C).map g
w :
  NatTrans.app (Discrete.natTrans fun X => (fun i => f i) X.as) { as := i } ≫
      colimit.ι (Discrete.functor fun i => Y i) { as := i } =
    NatTrans.app (Discrete.natTrans fun X => (fun i => g i) X.as) { as := i } ≫
      colimit.ι (Discrete.functor fun i => Y i) { as := i }
⊢ f i = g i
[PROOFSTEP]
simp at *
[GOAL]
case h
β : Type
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasCoproducts C
inst✝ : HasZeroMorphisms C
X Y : GradedObject β C
f g : X ⟶ Y
i : β
w✝¹ : Sigma.ι (fun i => X i) i ≫ (total β C).map f = Sigma.ι (fun i => X i) i ≫ (total β C).map g
w✝ : f i ≫ colimit.ι (Discrete.functor fun i => Y i) { as := i } = Sigma.ι (fun i => X i) i ≫ (total β C).map g
w :
  f i ≫ colimit.ι (Discrete.functor fun i => Y i) { as := i } =
    g i ≫ colimit.ι (Discrete.functor fun i => Y i) { as := i }
⊢ f i = g i
[PROOFSTEP]
exact Mono.right_cancellation _ _ w
