[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : C
⊢ PartialOrder (Subobject X)
[PROOFSTEP]
dsimp only [Subobject]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : C
⊢ PartialOrder (ThinSkeleton (MonoOver X))
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : C
p : Subobject X → Prop
h : ∀ ⦃A : C⦄ (f : A ⟶ X) [inst : Mono f], p (mk f)
P : Subobject X
⊢ p P
[PROOFSTEP]
apply Quotient.inductionOn'
[GOAL]
case h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : C
p : Subobject X → Prop
h : ∀ ⦃A : C⦄ (f : A ⟶ X) [inst : Mono f], p (mk f)
P : Subobject X
⊢ ∀ (a : MonoOver X), p (Quotient.mk'' a)
[PROOFSTEP]
intro a
[GOAL]
case h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : C
p : Subobject X → Prop
h : ∀ ⦃A : C⦄ (f : A ⟶ X) [inst : Mono f], p (mk f)
P : Subobject X
a : MonoOver X
⊢ p (Quotient.mk'' a)
[PROOFSTEP]
exact h a.arrow
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : C
p : Subobject X → Subobject X → Prop
h : ∀ ⦃A B : C⦄ (f : A ⟶ X) (g : B ⟶ X) [inst : Mono f] [inst_1 : Mono g], p (mk f) (mk g)
P Q : Subobject X
⊢ p P Q
[PROOFSTEP]
apply Quotient.inductionOn₂'
[GOAL]
case h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : C
p : Subobject X → Subobject X → Prop
h : ∀ ⦃A B : C⦄ (f : A ⟶ X) (g : B ⟶ X) [inst : Mono f] [inst_1 : Mono g], p (mk f) (mk g)
P Q : Subobject X
⊢ ∀ (a₁ a₂ : MonoOver X), p (Quotient.mk'' a₁) (Quotient.mk'' a₂)
[PROOFSTEP]
intro a b
[GOAL]
case h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : C
p : Subobject X → Subobject X → Prop
h : ∀ ⦃A B : C⦄ (f : A ⟶ X) (g : B ⟶ X) [inst : Mono f] [inst_1 : Mono g], p (mk f) (mk g)
P Q : Subobject X
a b : MonoOver X
⊢ p (Quotient.mk'' a) (Quotient.mk'' b)
[PROOFSTEP]
exact h a.arrow b.arrow
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
A : C
X Y : Subobject A
h : X = Y
⊢ eqToHom (_ : underlying.obj X = underlying.obj Y) ≫ arrow Y = arrow X
[PROOFSTEP]
induction h
[GOAL]
case refl
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
A : C
X Y : Subobject A
⊢ eqToHom (_ : underlying.obj X = underlying.obj X) ≫ arrow X = arrow X
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
P : Subobject X
Q : MonoOver X
⊢ mk (arrow (Quotient.mk'' Q)) = Quotient.mk'' Q
[PROOFSTEP]
obtain ⟨e⟩ := @Quotient.mk_out' _ (isIsomorphicSetoid _) Q
[GOAL]
case intro
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
P : Subobject X
Q : MonoOver X
e : Quotient.out' (Quotient.mk'' Q) ≅ Q
⊢ mk (arrow (Quotient.mk'' Q)) = Quotient.mk'' Q
[PROOFSTEP]
exact Quotient.sound' ⟨MonoOver.isoMk (Iso.refl _) ≪≫ e⟩
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
B : C
X Y : Subobject B
f : underlying.obj X ⟶ underlying.obj Y
w : f ≫ arrow Y = arrow X
⊢ X ≤ Y
[PROOFSTEP]
convert mk_le_mk_of_comm _ w
[GOAL]
case h.e'_3
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
B : C
X Y : Subobject B
f : underlying.obj X ⟶ underlying.obj Y
w : f ≫ arrow Y = arrow X
⊢ X = mk (arrow X)
[PROOFSTEP]
simp
[GOAL]
case h.e'_4
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
B : C
X Y : Subobject B
f : underlying.obj X ⟶ underlying.obj Y
w : f ≫ arrow Y = arrow X
⊢ Y = mk (arrow Y)
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X✝ Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
B A : C
X : Subobject B
f : A ⟶ B
inst✝ : Mono f
g : underlying.obj X ⟶ A
w : g ≫ f = arrow X
⊢ (g ≫ (underlyingIso f).inv) ≫ arrow (mk f) = arrow X
[PROOFSTEP]
simp [w]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X✝ Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
B A : C
X : Subobject B
f : A ⟶ B
inst✝ : Mono f
g : A ⟶ underlying.obj X
w : g ≫ arrow X = f
⊢ ((underlyingIso f).hom ≫ g) ≫ arrow X = arrow (mk f)
[PROOFSTEP]
simp [w]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X✝ Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
B A : C
X : Subobject B
f : A ⟶ B
inst✝ : Mono f
i : underlying.obj X ≅ A
w : i.hom ≫ f = arrow X
⊢ (i ≪≫ (underlyingIso f).symm).hom ≫ arrow (mk f) = arrow X
[PROOFSTEP]
simp [w]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X✝ Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
B A : C
X : Subobject B
f : A ⟶ B
inst✝ : Mono f
i : A ≅ underlying.obj X
w : i.hom ≫ arrow X = f
⊢ i.symm.hom ≫ f = arrow X
[PROOFSTEP]
rw [Iso.symm_hom, Iso.inv_comp_eq, w]
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
B A₁ A₂ : C
f : A₁ ⟶ B
g : A₂ ⟶ B
inst✝¹ : Mono f
inst✝ : Mono g
i : A₁ ≅ A₂
w : i.hom ≫ g = f
⊢ (underlyingIso f ≪≫ i).hom ≫ g = arrow (mk f)
[PROOFSTEP]
simp [w]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
B : C
X Y : Subobject B
h : X ≤ Y
⊢ Mono (ofLE X Y h)
[PROOFSTEP]
fconstructor
[GOAL]
case right_cancellation
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
B : C
X Y : Subobject B
h : X ≤ Y
⊢ ∀ {Z : C} (g h_1 : Z ⟶ underlying.obj X), g ≫ ofLE X Y h = h_1 ≫ ofLE X Y h → g = h_1
[PROOFSTEP]
intro Z f g w
[GOAL]
case right_cancellation
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ Z✝ : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
B : C
X Y : Subobject B
h : X ≤ Y
Z : C
f g : Z ⟶ underlying.obj X
w : f ≫ ofLE X Y h = g ≫ ofLE X Y h
⊢ f = g
[PROOFSTEP]
replace w := w =≫ Y.arrow
[GOAL]
case right_cancellation
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ Z✝ : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
B : C
X Y : Subobject B
h : X ≤ Y
Z : C
f g : Z ⟶ underlying.obj X
w : (f ≫ ofLE X Y h) ≫ arrow Y = (g ≫ ofLE X Y h) ≫ arrow Y
⊢ f = g
[PROOFSTEP]
ext
[GOAL]
case right_cancellation.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ Z✝ : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
B : C
X Y : Subobject B
h : X ≤ Y
Z : C
f g : Z ⟶ underlying.obj X
w : (f ≫ ofLE X Y h) ≫ arrow Y = (g ≫ ofLE X Y h) ≫ arrow Y
⊢ f ≫ arrow X = g ≫ arrow X
[PROOFSTEP]
simpa using w
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
B A₁ A₂ : C
f₁ : A₁ ⟶ B
f₂ : A₂ ⟶ B
inst✝¹ : Mono f₁
inst✝ : Mono f₂
g : A₁ ⟶ A₂
w : g ≫ f₂ = f₁
⊢ ofLE (mk f₁) (mk f₂) (_ : mk f₁ ≤ mk f₂) = (underlyingIso f₁).hom ≫ g ≫ (underlyingIso f₂).inv
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
B A₁ A₂ : C
f₁ : A₁ ⟶ B
f₂ : A₂ ⟶ B
inst✝¹ : Mono f₁
inst✝ : Mono f₂
g : A₁ ⟶ A₂
w : g ≫ f₂ = f₁
⊢ ofLE (mk f₁) (mk f₂) (_ : mk f₁ ≤ mk f₂) ≫ arrow (mk f₂) =
    ((underlyingIso f₁).hom ≫ g ≫ (underlyingIso f₂).inv) ≫ arrow (mk f₂)
[PROOFSTEP]
simp [w]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X✝ Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
B A : C
X : Subobject B
f : A ⟶ B
inst✝ : Mono f
h : X ≤ mk f
⊢ Mono (ofLEMk X f h)
[PROOFSTEP]
dsimp only [ofLEMk]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X✝ Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
B A : C
X : Subobject B
f : A ⟶ B
inst✝ : Mono f
h : X ≤ mk f
⊢ Mono (ofLE X (mk f) h ≫ (underlyingIso f).hom)
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X✝ Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
B A : C
X : Subobject B
f : A ⟶ B
inst✝ : Mono f
h : X ≤ mk f
⊢ ofLEMk X f h ≫ f = arrow X
[PROOFSTEP]
simp [ofLEMk]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X✝ Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
B A : C
f : A ⟶ B
inst✝ : Mono f
X : Subobject B
h : mk f ≤ X
⊢ Mono (ofMkLE f X h)
[PROOFSTEP]
dsimp only [ofMkLE]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X✝ Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
B A : C
f : A ⟶ B
inst✝ : Mono f
X : Subobject B
h : mk f ≤ X
⊢ Mono ((underlyingIso f).inv ≫ ofLE (mk f) X h)
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X✝ Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
B A : C
f : A ⟶ B
inst✝ : Mono f
X : Subobject B
h : mk f ≤ X
⊢ ofMkLE f X h ≫ arrow X = f
[PROOFSTEP]
simp [ofMkLE]
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
B A₁ A₂ : C
f : A₁ ⟶ B
g : A₂ ⟶ B
inst✝¹ : Mono f
inst✝ : Mono g
h : mk f ≤ mk g
⊢ Mono (ofMkLEMk f g h)
[PROOFSTEP]
dsimp only [ofMkLEMk]
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
B A₁ A₂ : C
f : A₁ ⟶ B
g : A₂ ⟶ B
inst✝¹ : Mono f
inst✝ : Mono g
h : mk f ≤ mk g
⊢ Mono ((underlyingIso f).inv ≫ ofLE (mk f) (mk g) h ≫ (underlyingIso g).hom)
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
B A₁ A₂ : C
f : A₁ ⟶ B
g : A₂ ⟶ B
inst✝¹ : Mono f
inst✝ : Mono g
h : mk f ≤ mk g
⊢ ofMkLEMk f g h ≫ g = f
[PROOFSTEP]
simp [ofMkLEMk]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ Z✝ : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
B : C
X Y Z : Subobject B
h₁ : X ≤ Y
h₂ : Y ≤ Z
⊢ ofLE X Y h₁ ≫ ofLE Y Z h₂ = ofLE X Z (_ : X ≤ Z)
[PROOFSTEP]
simp only [ofLE, ← Functor.map_comp underlying]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ Z✝ : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
B : C
X Y Z : Subobject B
h₁ : X ≤ Y
h₂ : Y ≤ Z
⊢ underlying.map (LE.le.hom h₁ ≫ LE.le.hom h₂) = underlying.map (LE.le.hom (_ : X ≤ Z))
[PROOFSTEP]
congr 1
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X✝ Y✝ Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
B A : C
X Y : Subobject B
f : A ⟶ B
inst✝ : Mono f
h₁ : X ≤ Y
h₂ : Y ≤ mk f
⊢ ofLE X Y h₁ ≫ ofLEMk Y f h₂ = ofLEMk X f (_ : X ≤ mk f)
[PROOFSTEP]
simp only [ofMkLE, ofLEMk, ofLE, ← Functor.map_comp_assoc underlying]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X✝ Y✝ Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
B A : C
X Y : Subobject B
f : A ⟶ B
inst✝ : Mono f
h₁ : X ≤ Y
h₂ : Y ≤ mk f
⊢ underlying.map (LE.le.hom h₁ ≫ LE.le.hom h₂) ≫ (underlyingIso f).hom =
    underlying.map (LE.le.hom (_ : X ≤ mk f)) ≫ (underlyingIso f).hom
[PROOFSTEP]
congr 1
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X✝ Y✝ Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
B A : C
X : Subobject B
f : A ⟶ B
inst✝ : Mono f
Y : Subobject B
h₁ : X ≤ mk f
h₂ : mk f ≤ Y
⊢ ofLEMk X f h₁ ≫ ofMkLE f Y h₂ = ofLE X Y (_ : X ≤ Y)
[PROOFSTEP]
simp only [ofMkLE, ofLEMk, ofLE, ← Functor.map_comp underlying, assoc, Iso.hom_inv_id_assoc]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X✝ Y✝ Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
B A : C
X : Subobject B
f : A ⟶ B
inst✝ : Mono f
Y : Subobject B
h₁ : X ≤ mk f
h₂ : mk f ≤ Y
⊢ underlying.map (LE.le.hom h₁ ≫ LE.le.hom h₂) = underlying.map (LE.le.hom (_ : X ≤ Y))
[PROOFSTEP]
congr 1
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X✝ Y Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
B A₁ A₂ : C
X : Subobject B
f : A₁ ⟶ B
inst✝¹ : Mono f
g : A₂ ⟶ B
inst✝ : Mono g
h₁ : X ≤ mk f
h₂ : mk f ≤ mk g
⊢ ofLEMk X f h₁ ≫ ofMkLEMk f g h₂ = ofLEMk X g (_ : X ≤ mk g)
[PROOFSTEP]
simp only [ofMkLE, ofLEMk, ofLE, ofMkLEMk, ← Functor.map_comp_assoc underlying, assoc, Iso.hom_inv_id_assoc]
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X✝ Y Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
B A₁ A₂ : C
X : Subobject B
f : A₁ ⟶ B
inst✝¹ : Mono f
g : A₂ ⟶ B
inst✝ : Mono g
h₁ : X ≤ mk f
h₂ : mk f ≤ mk g
⊢ underlying.map (LE.le.hom h₁ ≫ LE.le.hom h₂) ≫ (underlyingIso g).hom =
    underlying.map (LE.le.hom (_ : X ≤ mk g)) ≫ (underlyingIso g).hom
[PROOFSTEP]
congr 1
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X✝ Y✝ Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
B A₁ : C
f : A₁ ⟶ B
inst✝ : Mono f
X Y : Subobject B
h₁ : mk f ≤ X
h₂ : X ≤ Y
⊢ ofMkLE f X h₁ ≫ ofLE X Y h₂ = ofMkLE f Y (_ : mk f ≤ Y)
[PROOFSTEP]
simp only [ofMkLE, ofLEMk, ofLE, ofMkLEMk, ← Functor.map_comp underlying, assoc]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X✝ Y✝ Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
B A₁ : C
f : A₁ ⟶ B
inst✝ : Mono f
X Y : Subobject B
h₁ : mk f ≤ X
h₂ : X ≤ Y
⊢ (underlyingIso f).inv ≫ underlying.map (LE.le.hom h₁ ≫ LE.le.hom h₂) =
    (underlyingIso f).inv ≫ underlying.map (LE.le.hom (_ : mk f ≤ Y))
[PROOFSTEP]
congr 1
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X✝ Y Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
B A₁ A₂ : C
f : A₁ ⟶ B
inst✝¹ : Mono f
X : Subobject B
g : A₂ ⟶ B
inst✝ : Mono g
h₁ : mk f ≤ X
h₂ : X ≤ mk g
⊢ ofMkLE f X h₁ ≫ ofLEMk X g h₂ = ofMkLEMk f g (_ : mk f ≤ mk g)
[PROOFSTEP]
simp only [ofMkLE, ofLEMk, ofLE, ofMkLEMk, ← Functor.map_comp_assoc underlying, assoc]
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X✝ Y Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
B A₁ A₂ : C
f : A₁ ⟶ B
inst✝¹ : Mono f
X : Subobject B
g : A₂ ⟶ B
inst✝ : Mono g
h₁ : mk f ≤ X
h₂ : X ≤ mk g
⊢ (underlyingIso f).inv ≫ underlying.map (LE.le.hom h₁ ≫ LE.le.hom h₂) ≫ (underlyingIso g).hom =
    (underlyingIso f).inv ≫ underlying.map (LE.le.hom (_ : mk f ≤ mk g)) ≫ (underlyingIso g).hom
[PROOFSTEP]
congr 1
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X✝ Y Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
B A₁ A₂ : C
f : A₁ ⟶ B
inst✝¹ : Mono f
g : A₂ ⟶ B
inst✝ : Mono g
X : Subobject B
h₁ : mk f ≤ mk g
h₂ : mk g ≤ X
⊢ ofMkLEMk f g h₁ ≫ ofMkLE g X h₂ = ofMkLE f X (_ : mk f ≤ X)
[PROOFSTEP]
simp only [ofMkLE, ofLEMk, ofLE, ofMkLEMk, ← Functor.map_comp underlying, assoc, Iso.hom_inv_id_assoc]
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X✝ Y Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
B A₁ A₂ : C
f : A₁ ⟶ B
inst✝¹ : Mono f
g : A₂ ⟶ B
inst✝ : Mono g
X : Subobject B
h₁ : mk f ≤ mk g
h₂ : mk g ≤ X
⊢ (underlyingIso f).inv ≫ underlying.map (LE.le.hom h₁ ≫ LE.le.hom h₂) =
    (underlyingIso f).inv ≫ underlying.map (LE.le.hom (_ : mk f ≤ X))
[PROOFSTEP]
congr 1
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
B A₁ A₂ A₃ : C
f : A₁ ⟶ B
inst✝² : Mono f
g : A₂ ⟶ B
inst✝¹ : Mono g
h : A₃ ⟶ B
inst✝ : Mono h
h₁ : mk f ≤ mk g
h₂ : mk g ≤ mk h
⊢ ofMkLEMk f g h₁ ≫ ofMkLEMk g h h₂ = ofMkLEMk f h (_ : mk f ≤ mk h)
[PROOFSTEP]
simp only [ofMkLE, ofLEMk, ofLE, ofMkLEMk, ← Functor.map_comp_assoc underlying, assoc, Iso.hom_inv_id_assoc]
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
B A₁ A₂ A₃ : C
f : A₁ ⟶ B
inst✝² : Mono f
g : A₂ ⟶ B
inst✝¹ : Mono g
h : A₃ ⟶ B
inst✝ : Mono h
h₁ : mk f ≤ mk g
h₂ : mk g ≤ mk h
⊢ (underlyingIso f).inv ≫ underlying.map (LE.le.hom h₁ ≫ LE.le.hom h₂) ≫ (underlyingIso h).hom =
    (underlyingIso f).inv ≫ underlying.map (LE.le.hom (_ : mk f ≤ mk h)) ≫ (underlyingIso h).hom
[PROOFSTEP]
congr 1
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
B : C
X : Subobject B
⊢ ofLE X X (_ : X ≤ X) = 𝟙 (underlying.obj X)
[PROOFSTEP]
apply (cancel_mono X.arrow).mp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
B : C
X : Subobject B
⊢ ofLE X X (_ : X ≤ X) ≫ arrow X = 𝟙 (underlying.obj X) ≫ arrow X
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
B A₁ : C
f : A₁ ⟶ B
inst✝ : Mono f
⊢ ofMkLEMk f f (_ : mk f ≤ mk f) = 𝟙 A₁
[PROOFSTEP]
apply (cancel_mono f).mp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
B A₁ : C
f : A₁ ⟶ B
inst✝ : Mono f
⊢ ofMkLEMk f f (_ : mk f ≤ mk f) ≫ f = 𝟙 A₁ ≫ f
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
A : C
B : D
e : MonoOver A ≌ MonoOver B
⊢ 𝟭 (Subobject A) ≅ lower e.functor ⋙ lower e.inverse
[PROOFSTEP]
apply eqToIso
[GOAL]
case p
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
A : C
B : D
e : MonoOver A ≌ MonoOver B
⊢ 𝟭 (Subobject A) = lower e.functor ⋙ lower e.inverse
[PROOFSTEP]
convert ThinSkeleton.map_iso_eq e.unitIso
[GOAL]
case h.e'_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
A : C
B : D
e : MonoOver A ≌ MonoOver B
⊢ 𝟭 (Subobject A) = ThinSkeleton.map (𝟭 (MonoOver A))
[PROOFSTEP]
exact ThinSkeleton.map_id_eq.symm
[GOAL]
case h.e'_3
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
A : C
B : D
e : MonoOver A ≌ MonoOver B
⊢ lower e.functor ⋙ lower e.inverse = ThinSkeleton.map (e.functor ⋙ e.inverse)
[PROOFSTEP]
exact (ThinSkeleton.map_comp_eq _ _).symm
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
A : C
B : D
e : MonoOver A ≌ MonoOver B
⊢ lower e.inverse ⋙ lower e.functor ≅ 𝟭 (Subobject B)
[PROOFSTEP]
apply eqToIso
[GOAL]
case p
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
A : C
B : D
e : MonoOver A ≌ MonoOver B
⊢ lower e.inverse ⋙ lower e.functor = 𝟭 (Subobject B)
[PROOFSTEP]
convert ThinSkeleton.map_iso_eq e.counitIso
[GOAL]
case h.e'_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
A : C
B : D
e : MonoOver A ≌ MonoOver B
⊢ lower e.inverse ⋙ lower e.functor = ThinSkeleton.map (e.inverse ⋙ e.functor)
[PROOFSTEP]
exact (ThinSkeleton.map_comp_eq _ _).symm
[GOAL]
case h.e'_3
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
A : C
B : D
e : MonoOver A ≌ MonoOver B
⊢ 𝟭 (Subobject B) = ThinSkeleton.map (𝟭 (MonoOver B))
[PROOFSTEP]
exact ThinSkeleton.map_id_eq.symm
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasPullbacks C
x : Subobject X
⊢ (pullback (𝟙 X)).obj x = x
[PROOFSTEP]
induction' x using Quotient.inductionOn' with f
[GOAL]
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasPullbacks C
f : MonoOver X
⊢ (pullback (𝟙 X)).obj (Quotient.mk'' f) = Quotient.mk'' f
[PROOFSTEP]
exact Quotient.sound ⟨MonoOver.pullbackId.app f⟩
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasPullbacks C
f : X ⟶ Y
g : Y ⟶ Z
x : Subobject Z
⊢ (pullback (f ≫ g)).obj x = (pullback f).obj ((pullback g).obj x)
[PROOFSTEP]
induction' x using Quotient.inductionOn' with t
[GOAL]
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasPullbacks C
f : X ⟶ Y
g : Y ⟶ Z
t : MonoOver Z
⊢ (pullback (f ≫ g)).obj (Quotient.mk'' t) = (pullback f).obj ((pullback g).obj (Quotient.mk'' t))
[PROOFSTEP]
exact Quotient.sound ⟨(MonoOver.pullbackComp _ _).app t⟩
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
x : Subobject X
⊢ (map (𝟙 X)).obj x = x
[PROOFSTEP]
induction' x using Quotient.inductionOn' with f
[GOAL]
case h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
f : MonoOver X
⊢ (map (𝟙 X)).obj (Quotient.mk'' f) = Quotient.mk'' f
[PROOFSTEP]
exact Quotient.sound ⟨MonoOver.mapId.app f⟩
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : Mono f
inst✝ : Mono g
x : Subobject X
⊢ (map (f ≫ g)).obj x = (map g).obj ((map f).obj x)
[PROOFSTEP]
induction' x using Quotient.inductionOn' with t
[GOAL]
case h
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : Mono f
inst✝ : Mono g
t : MonoOver X
⊢ (map (f ≫ g)).obj (Quotient.mk'' t) = (map g).obj ((map f).obj (Quotient.mk'' t))
[PROOFSTEP]
exact Quotient.sound ⟨(MonoOver.mapComp _ _).app t⟩
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : X ≅ Y
g : Subobject X
⊢ (map e.inv).obj ((map e.hom).obj g) = g
[PROOFSTEP]
simp_rw [← map_comp, e.hom_inv_id, map_id]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : X ≅ Y
g : Subobject Y
⊢ (map e.hom).obj ((map e.inv).obj g) = g
[PROOFSTEP]
simp_rw [← map_comp, e.inv_hom_id, map_id]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : X ≅ Y
A B : Subobject X
⊢ ↑{ toFun := (map e.hom).toPrefunctor.obj, invFun := (map e.inv).toPrefunctor.obj,
            left_inv := (_ : ∀ (g : Subobject X), (map e.inv).obj ((map e.hom).obj g) = g),
            right_inv := (_ : ∀ (g : Subobject Y), (map e.hom).obj ((map e.inv).obj g) = g) }
        A ≤
      ↑{ toFun := (map e.hom).toPrefunctor.obj, invFun := (map e.inv).toPrefunctor.obj,
            left_inv := (_ : ∀ (g : Subobject X), (map e.inv).obj ((map e.hom).obj g) = g),
            right_inv := (_ : ∀ (g : Subobject Y), (map e.hom).obj ((map e.inv).obj g) = g) }
        B ↔
    A ≤ B
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : X ≅ Y
A B : Subobject X
⊢ (map e.hom).obj A ≤ (map e.hom).obj B ↔ A ≤ B
[PROOFSTEP]
constructor
[GOAL]
case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : X ≅ Y
A B : Subobject X
⊢ (map e.hom).obj A ≤ (map e.hom).obj B → A ≤ B
[PROOFSTEP]
intro h
[GOAL]
case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : X ≅ Y
A B : Subobject X
h : (map e.hom).obj A ≤ (map e.hom).obj B
⊢ A ≤ B
[PROOFSTEP]
apply_fun (map e.inv).obj at h
[GOAL]
case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : X ≅ Y
A B : Subobject X
h : (map e.inv).obj ((map e.hom).obj A) ≤ (map e.inv).obj ((map e.hom).obj B)
⊢ A ≤ B
[PROOFSTEP]
simpa only [← map_comp, e.hom_inv_id, map_id] using h
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : X ≅ Y
A B : Subobject X
h : (map e.hom).obj A ≤ (map e.hom).obj B
⊢ Monotone (map e.inv).toPrefunctor.obj
[PROOFSTEP]
apply Functor.monotone
[GOAL]
case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : X ≅ Y
A B : Subobject X
⊢ A ≤ B → (map e.hom).obj A ≤ (map e.hom).obj B
[PROOFSTEP]
intro h
[GOAL]
case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : X ≅ Y
A B : Subobject X
h : A ≤ B
⊢ (map e.hom).obj A ≤ (map e.hom).obj B
[PROOFSTEP]
apply_fun (map e.hom).obj at h
[GOAL]
case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : X ≅ Y
A B : Subobject X
h : (map e.hom).obj A ≤ (map e.hom).obj B
⊢ (map e.hom).obj A ≤ (map e.hom).obj B
[PROOFSTEP]
exact h
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : X ≅ Y
A B : Subobject X
h : A ≤ B
⊢ Monotone (map e.hom).toPrefunctor.obj
[PROOFSTEP]
apply Functor.monotone
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasPullbacks C
f : X ⟶ Y
inst✝ : Mono f
g : Subobject X
⊢ (pullback f).obj ((map f).obj g) = g
[PROOFSTEP]
revert g
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasPullbacks C
f : X ⟶ Y
inst✝ : Mono f
⊢ ∀ (g : Subobject X), (pullback f).obj ((map f).obj g) = g
[PROOFSTEP]
exact Quotient.ind (fun g' => Quotient.sound ⟨(MonoOver.pullbackMapSelf f).app _⟩)
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
X✝ Y✝ Z✝ : C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : HasPullbacks C
X Y Z W : C
f : X ⟶ Y
g : X ⟶ Z
h : Y ⟶ W
k : Z ⟶ W
inst✝¹ : Mono h
inst✝ : Mono g
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
p : Subobject Y
⊢ (map g).obj ((pullback f).obj p) = (pullback k).obj ((map h).obj p)
[PROOFSTEP]
revert p
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
X✝ Y✝ Z✝ : C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : HasPullbacks C
X Y Z W : C
f : X ⟶ Y
g : X ⟶ Z
h : Y ⟶ W
k : Z ⟶ W
inst✝¹ : Mono h
inst✝ : Mono g
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
⊢ ∀ (p : Subobject Y), (map g).obj ((pullback f).obj p) = (pullback k).obj ((map h).obj p)
[PROOFSTEP]
apply Quotient.ind'
[GOAL]
case h
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
X✝ Y✝ Z✝ : C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : HasPullbacks C
X Y Z W : C
f : X ⟶ Y
g : X ⟶ Z
h : Y ⟶ W
k : Z ⟶ W
inst✝¹ : Mono h
inst✝ : Mono g
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
⊢ ∀ (a : MonoOver Y),
    (map g).obj ((pullback f).obj (Quotient.mk'' a)) = (pullback k).obj ((map h).obj (Quotient.mk'' a))
[PROOFSTEP]
intro a
[GOAL]
case h
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
X✝ Y✝ Z✝ : C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : HasPullbacks C
X Y Z W : C
f : X ⟶ Y
g : X ⟶ Z
h : Y ⟶ W
k : Z ⟶ W
inst✝¹ : Mono h
inst✝ : Mono g
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
a : MonoOver Y
⊢ (map g).obj ((pullback f).obj (Quotient.mk'' a)) = (pullback k).obj ((map h).obj (Quotient.mk'' a))
[PROOFSTEP]
apply Quotient.sound
[GOAL]
case h.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
X✝ Y✝ Z✝ : C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : HasPullbacks C
X Y Z W : C
f : X ⟶ Y
g : X ⟶ Z
h : Y ⟶ W
k : Z ⟶ W
inst✝¹ : Mono h
inst✝ : Mono g
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
a : MonoOver Y
⊢ (MonoOver.map g).obj ((MonoOver.pullback f).obj a) ≈ (MonoOver.pullback k).obj ((MonoOver.map h).obj a)
[PROOFSTEP]
apply ThinSkeleton.equiv_of_both_ways
[GOAL]
case h.a.f
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
X✝ Y✝ Z✝ : C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : HasPullbacks C
X Y Z W : C
f : X ⟶ Y
g : X ⟶ Z
h : Y ⟶ W
k : Z ⟶ W
inst✝¹ : Mono h
inst✝ : Mono g
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
a : MonoOver Y
⊢ (MonoOver.map g).obj ((MonoOver.pullback f).obj a) ⟶ (MonoOver.pullback k).obj ((MonoOver.map h).obj a)
[PROOFSTEP]
refine' MonoOver.homMk (pullback.lift pullback.fst _ _) (pullback.lift_snd _ _ _)
[GOAL]
case h.a.f
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
X✝ Y✝ Z✝ : C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : HasPullbacks C
X Y Z W : C
f : X ⟶ Y
g : X ⟶ Z
h : Y ⟶ W
k : Z ⟶ W
inst✝¹ : Mono h
inst✝ : Mono g
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
a : MonoOver Y
⊢ pullback.fst ≫ ((MonoOver.forget W).obj ((MonoOver.map h).obj a)).hom =
    MonoOver.arrow ((MonoOver.map g).obj ((MonoOver.pullback f).obj a)) ≫ k
[PROOFSTEP]
change _ ≫ a.arrow ≫ h = (pullback.snd ≫ g) ≫ _
[GOAL]
case h.a.f
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
X✝ Y✝ Z✝ : C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : HasPullbacks C
X Y Z W : C
f : X ⟶ Y
g : X ⟶ Z
h : Y ⟶ W
k : Z ⟶ W
inst✝¹ : Mono h
inst✝ : Mono g
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
a : MonoOver Y
⊢ pullback.fst ≫ MonoOver.arrow a ≫ h = (pullback.snd ≫ g) ≫ k
[PROOFSTEP]
rw [assoc, ← comm, pullback.condition_assoc]
[GOAL]
case h.a.g
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
X✝ Y✝ Z✝ : C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : HasPullbacks C
X Y Z W : C
f : X ⟶ Y
g : X ⟶ Z
h : Y ⟶ W
k : Z ⟶ W
inst✝¹ : Mono h
inst✝ : Mono g
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
a : MonoOver Y
⊢ (MonoOver.pullback k).obj ((MonoOver.map h).obj a) ⟶ (MonoOver.map g).obj ((MonoOver.pullback f).obj a)
[PROOFSTEP]
refine'
  MonoOver.homMk
    (pullback.lift pullback.fst (PullbackCone.IsLimit.lift t (pullback.fst ≫ a.arrow) pullback.snd _)
      (PullbackCone.IsLimit.lift_fst _ _ _ _).symm)
    _
[GOAL]
case h.a.g.refine'_1
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
X✝ Y✝ Z✝ : C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : HasPullbacks C
X Y Z W : C
f : X ⟶ Y
g : X ⟶ Z
h : Y ⟶ W
k : Z ⟶ W
inst✝¹ : Mono h
inst✝ : Mono g
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
a : MonoOver Y
⊢ (pullback.fst ≫ ((MonoOver.forget Y).obj a).hom) ≫ h = pullback.snd ≫ k
[PROOFSTEP]
rw [← pullback.condition, assoc]
[GOAL]
case h.a.g.refine'_1
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
X✝ Y✝ Z✝ : C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : HasPullbacks C
X Y Z W : C
f : X ⟶ Y
g : X ⟶ Z
h : Y ⟶ W
k : Z ⟶ W
inst✝¹ : Mono h
inst✝ : Mono g
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
a : MonoOver Y
⊢ pullback.fst ≫ ((MonoOver.forget Y).obj a).hom ≫ h =
    pullback.fst ≫ ((MonoOver.forget W).obj ((MonoOver.map h).obj a)).hom
[PROOFSTEP]
rfl
[GOAL]
case h.a.g.refine'_2
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
X✝ Y✝ Z✝ : C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : HasPullbacks C
X Y Z W : C
f : X ⟶ Y
g : X ⟶ Z
h : Y ⟶ W
k : Z ⟶ W
inst✝¹ : Mono h
inst✝ : Mono g
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
a : MonoOver Y
⊢ pullback.lift pullback.fst
        (PullbackCone.IsLimit.lift t (pullback.fst ≫ MonoOver.arrow a) pullback.snd
          (_ : (pullback.fst ≫ ((MonoOver.forget Y).obj a).hom) ≫ h = pullback.snd ≫ k))
        (_ :
          pullback.fst ≫ ((MonoOver.forget Y).obj a).hom =
            PullbackCone.IsLimit.lift t (pullback.fst ≫ ((MonoOver.forget Y).obj a).hom) pullback.snd
                (_ : (pullback.fst ≫ ((MonoOver.forget Y).obj a).hom) ≫ h = pullback.snd ≫ k) ≫
              PullbackCone.fst (PullbackCone.mk f g comm)) ≫
      MonoOver.arrow ((MonoOver.map g).obj ((MonoOver.pullback f).obj a)) =
    MonoOver.arrow ((MonoOver.pullback k).obj ((MonoOver.map h).obj a))
[PROOFSTEP]
dsimp
[GOAL]
case h.a.g.refine'_2
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
X✝ Y✝ Z✝ : C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : HasPullbacks C
X Y Z W : C
f : X ⟶ Y
g : X ⟶ Z
h : Y ⟶ W
k : Z ⟶ W
inst✝¹ : Mono h
inst✝ : Mono g
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
a : MonoOver Y
⊢ pullback.lift pullback.fst
        (PullbackCone.IsLimit.lift t (pullback.fst ≫ MonoOver.arrow a) pullback.snd
          (_ : (pullback.fst ≫ MonoOver.arrow a) ≫ h = pullback.snd ≫ k))
        (_ :
          pullback.fst ≫ MonoOver.arrow a =
            PullbackCone.IsLimit.lift t (pullback.fst ≫ MonoOver.arrow a) pullback.snd
                (_ : (pullback.fst ≫ MonoOver.arrow a) ≫ h = pullback.snd ≫ k) ≫
              f) ≫
      pullback.snd ≫ g =
    pullback.snd
[PROOFSTEP]
rw [pullback.lift_snd_assoc]
[GOAL]
case h.a.g.refine'_2
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
X✝ Y✝ Z✝ : C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : HasPullbacks C
X Y Z W : C
f : X ⟶ Y
g : X ⟶ Z
h : Y ⟶ W
k : Z ⟶ W
inst✝¹ : Mono h
inst✝ : Mono g
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
a : MonoOver Y
⊢ PullbackCone.IsLimit.lift t (pullback.fst ≫ MonoOver.arrow a) pullback.snd
        (_ : (pullback.fst ≫ MonoOver.arrow a) ≫ h = pullback.snd ≫ k) ≫
      g =
    pullback.snd
[PROOFSTEP]
apply PullbackCone.IsLimit.lift_snd


[GOAL]
C D : Cat
F : C ⟶ D
⊢ 𝟙 C ≫ F = F
[PROOFSTEP]
cases F
[GOAL]
case mk
C D : Cat
toPrefunctor✝ : ↑C ⥤q ↑D
map_id✝ : ∀ (X : ↑C), toPrefunctor✝.map (𝟙 X) = 𝟙 (toPrefunctor✝.obj X)
map_comp✝ :
  ∀ {X Y Z : ↑C} (f : X ⟶ Y) (g : Y ⟶ Z), toPrefunctor✝.map (f ≫ g) = toPrefunctor✝.map f ≫ toPrefunctor✝.map g
⊢ 𝟙 C ≫ Functor.mk toPrefunctor✝ = Functor.mk toPrefunctor✝
[PROOFSTEP]
rfl
[GOAL]
C D : Cat
F : C ⟶ D
⊢ F ≫ 𝟙 D = F
[PROOFSTEP]
cases F
[GOAL]
case mk
C D : Cat
toPrefunctor✝ : ↑C ⥤q ↑D
map_id✝ : ∀ (X : ↑C), toPrefunctor✝.map (𝟙 X) = 𝟙 (toPrefunctor✝.obj X)
map_comp✝ :
  ∀ {X Y Z : ↑C} (f : X ⟶ Y) (g : Y ⟶ Z), toPrefunctor✝.map (f ≫ g) = toPrefunctor✝.map f ≫ toPrefunctor✝.map g
⊢ Functor.mk toPrefunctor✝ ≫ 𝟙 D = Functor.mk toPrefunctor✝
[PROOFSTEP]
rfl
[GOAL]
⊢ ∀ {a b c d : Cat} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d), (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
intros
[GOAL]
a✝ b✝ c✝ d✝ : Cat
f✝ : a✝ ⟶ b✝
g✝ : b✝ ⟶ c✝
h✝ : c✝ ⟶ d✝
⊢ (f✝ ≫ g✝) ≫ h✝ = f✝ ≫ g✝ ≫ h✝
[PROOFSTEP]
rfl
[GOAL]
X Y : Type u
f : X ⟶ Y
⊢ (fun X => Cat.of (Discrete X)) X ⟶ (fun X => Cat.of (Discrete X)) Y
[PROOFSTEP]
dsimp
[GOAL]
X Y : Type u
f : X ⟶ Y
⊢ Cat.of (Discrete X) ⟶ Cat.of (Discrete Y)
[PROOFSTEP]
exact Discrete.functor (Discrete.mk ∘ f)
[GOAL]
X : Type u
⊢ { obj := fun X => Cat.of (Discrete X), map := fun {X Y} f => id (Discrete.functor (Discrete.mk ∘ f)) }.map (𝟙 X) =
    𝟙 ({ obj := fun X => Cat.of (Discrete X), map := fun {X Y} f => id (Discrete.functor (Discrete.mk ∘ f)) }.obj X)
[PROOFSTEP]
apply Functor.ext
[GOAL]
case h_map
X : Type u
⊢ autoParam
    (∀
      (X_1 Y :
        ↑({ obj := fun X => Cat.of (Discrete X), map := fun {X Y} f => id (Discrete.functor (Discrete.mk ∘ f)) }.obj X))
      (f : X_1 ⟶ Y),
      ({ obj := fun X => Cat.of (Discrete X), map := fun {X Y} f => id (Discrete.functor (Discrete.mk ∘ f)) }.map
              (𝟙 X)).map
          f =
        eqToHom (_ : ?F.obj X_1 = ?G.obj X_1) ≫
          (𝟙
                  ({ obj := fun X => Cat.of (Discrete X),
                        map := fun {X Y} f => id (Discrete.functor (Discrete.mk ∘ f)) }.obj
                    X)).map
              f ≫
            eqToHom
              (_ :
                (𝟙
                        ({ obj := fun X => Cat.of (Discrete X),
                              map := fun {X Y} f => id (Discrete.functor (Discrete.mk ∘ f)) }.obj
                          X)).obj
                    Y =
                  ({ obj := fun X => Cat.of (Discrete X),
                            map := fun {X Y} f => id (Discrete.functor (Discrete.mk ∘ f)) }.map
                        (𝟙 X)).obj
                    Y))
    _auto✝
[PROOFSTEP]
intro X Y f
[GOAL]
case h_map
X✝ : Type u
X Y : ↑({ obj := fun X => Cat.of (Discrete X), map := fun {X Y} f => id (Discrete.functor (Discrete.mk ∘ f)) }.obj X✝)
f : X ⟶ Y
⊢ ({ obj := fun X => Cat.of (Discrete X), map := fun {X Y} f => id (Discrete.functor (Discrete.mk ∘ f)) }.map
          (𝟙 X✝)).map
      f =
    eqToHom (_ : ?F.obj X = ?G.obj X) ≫
      (𝟙
              ({ obj := fun X => Cat.of (Discrete X),
                    map := fun {X Y} f => id (Discrete.functor (Discrete.mk ∘ f)) }.obj
                X✝)).map
          f ≫
        eqToHom
          (_ :
            (𝟙
                    ({ obj := fun X => Cat.of (Discrete X),
                          map := fun {X Y} f => id (Discrete.functor (Discrete.mk ∘ f)) }.obj
                      X✝)).obj
                Y =
              ({ obj := fun X => Cat.of (Discrete X),
                        map := fun {X Y} f => id (Discrete.functor (Discrete.mk ∘ f)) }.map
                    (𝟙 X✝)).obj
                Y)
[PROOFSTEP]
cases f
[GOAL]
case h_map.up
X✝ : Type u
X Y : ↑({ obj := fun X => Cat.of (Discrete X), map := fun {X Y} f => id (Discrete.functor (Discrete.mk ∘ f)) }.obj X✝)
down✝ : PLift (X.as = Y.as)
⊢ ({ obj := fun X => Cat.of (Discrete X), map := fun {X Y} f => id (Discrete.functor (Discrete.mk ∘ f)) }.map
          (𝟙 X✝)).map
      { down := down✝ } =
    eqToHom (_ : ?F.obj X = ?G.obj X) ≫
      (𝟙
              ({ obj := fun X => Cat.of (Discrete X),
                    map := fun {X Y} f => id (Discrete.functor (Discrete.mk ∘ f)) }.obj
                X✝)).map
          { down := down✝ } ≫
        eqToHom
          (_ :
            (𝟙
                    ({ obj := fun X => Cat.of (Discrete X),
                          map := fun {X Y} f => id (Discrete.functor (Discrete.mk ∘ f)) }.obj
                      X✝)).obj
                Y =
              ({ obj := fun X => Cat.of (Discrete X),
                        map := fun {X Y} f => id (Discrete.functor (Discrete.mk ∘ f)) }.map
                    (𝟙 X✝)).obj
                Y)
[PROOFSTEP]
simp only [id_eq, eqToHom_refl, Cat.id_map, Category.comp_id, Category.id_comp]
[GOAL]
case h_map.up
X✝ : Type u
X Y : ↑({ obj := fun X => Cat.of (Discrete X), map := fun {X Y} f => id (Discrete.functor (Discrete.mk ∘ f)) }.obj X✝)
down✝ : PLift (X.as = Y.as)
⊢ (Discrete.functor (Discrete.mk ∘ 𝟙 X✝)).map { down := down✝ } = { down := down✝ }
[PROOFSTEP]
apply ULift.ext
[GOAL]
case h_map.up.h
X✝ : Type u
X Y : ↑({ obj := fun X => Cat.of (Discrete X), map := fun {X Y} f => id (Discrete.functor (Discrete.mk ∘ f)) }.obj X✝)
down✝ : PLift (X.as = Y.as)
⊢ ((Discrete.functor (Discrete.mk ∘ 𝟙 X✝)).map { down := down✝ }).down = { down := down✝ }.down
[PROOFSTEP]
aesop_cat
[GOAL]
case h_obj
X : Type u
⊢ ∀
    (X_1 :
      ↑({ obj := fun X => Cat.of (Discrete X), map := fun {X Y} f => id (Discrete.functor (Discrete.mk ∘ f)) }.obj X)),
    ({ obj := fun X => Cat.of (Discrete X), map := fun {X Y} f => id (Discrete.functor (Discrete.mk ∘ f)) }.map
            (𝟙 X)).obj
        X_1 =
      (𝟙
            ({ obj := fun X => Cat.of (Discrete X), map := fun {X Y} f => id (Discrete.functor (Discrete.mk ∘ f)) }.obj
              X)).obj
        X_1
[PROOFSTEP]
aesop_cat
[GOAL]
X✝ Y✝ Z✝ : Type u
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ { obj := fun X => Cat.of (Discrete X), map := fun {X Y} f => id (Discrete.functor (Discrete.mk ∘ f)) }.map (f ≫ g) =
    { obj := fun X => Cat.of (Discrete X), map := fun {X Y} f => id (Discrete.functor (Discrete.mk ∘ f)) }.map f ≫
      { obj := fun X => Cat.of (Discrete X), map := fun {X Y} f => id (Discrete.functor (Discrete.mk ∘ f)) }.map g
[PROOFSTEP]
apply Functor.ext
[GOAL]
case h_map
X✝ Y✝ Z✝ : Type u
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ autoParam
    (∀
      (X Y :
        ↑({ obj := fun X => Cat.of (Discrete X), map := fun {X Y} f => id (Discrete.functor (Discrete.mk ∘ f)) }.obj
            X✝))
      (f_1 : X ⟶ Y),
      ({ obj := fun X => Cat.of (Discrete X), map := fun {X Y} f => id (Discrete.functor (Discrete.mk ∘ f)) }.map
              (f ≫ g)).map
          f_1 =
        eqToHom (_ : ?F.obj X = ?G.obj X) ≫
          ({ obj := fun X => Cat.of (Discrete X), map := fun {X Y} f => id (Discrete.functor (Discrete.mk ∘ f)) }.map
                    f ≫
                  { obj := fun X => Cat.of (Discrete X),
                        map := fun {X Y} f => id (Discrete.functor (Discrete.mk ∘ f)) }.map
                    g).map
              f_1 ≫
            eqToHom
              (_ :
                ({ obj := fun X => Cat.of (Discrete X),
                              map := fun {X Y} f => id (Discrete.functor (Discrete.mk ∘ f)) }.map
                          f ≫
                        { obj := fun X => Cat.of (Discrete X),
                              map := fun {X Y} f => id (Discrete.functor (Discrete.mk ∘ f)) }.map
                          g).obj
                    Y =
                  ({ obj := fun X => Cat.of (Discrete X),
                            map := fun {X Y} f => id (Discrete.functor (Discrete.mk ∘ f)) }.map
                        (f ≫ g)).obj
                    Y))
    _auto✝
case h_obj
X✝ Y✝ Z✝ : Type u
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ ∀
    (X :
      ↑({ obj := fun X => Cat.of (Discrete X), map := fun {X Y} f => id (Discrete.functor (Discrete.mk ∘ f)) }.obj X✝)),
    ({ obj := fun X => Cat.of (Discrete X), map := fun {X Y} f => id (Discrete.functor (Discrete.mk ∘ f)) }.map
            (f ≫ g)).obj
        X =
      ({ obj := fun X => Cat.of (Discrete X), map := fun {X Y} f => id (Discrete.functor (Discrete.mk ∘ f)) }.map f ≫
            { obj := fun X => Cat.of (Discrete X), map := fun {X Y} f => id (Discrete.functor (Discrete.mk ∘ f)) }.map
              g).obj
        X
[PROOFSTEP]
aesop_cat
[GOAL]
⊢ ∀ {X Y : Type u} (f : typeToCat.obj X ⟶ typeToCat.obj Y),
    typeToCat.map ((fun {X Y} F => Discrete.as ∘ F.obj ∘ Discrete.mk) f) = f
[PROOFSTEP]
intro X Y F
[GOAL]
X Y : Type u
F : typeToCat.obj X ⟶ typeToCat.obj Y
⊢ typeToCat.map ((fun {X Y} F => Discrete.as ∘ F.obj ∘ Discrete.mk) F) = F
[PROOFSTEP]
apply Functor.ext
[GOAL]
case h_map
X Y : Type u
F : typeToCat.obj X ⟶ typeToCat.obj Y
⊢ autoParam
    (∀ (X_1 Y_1 : ↑(typeToCat.obj X)) (f : X_1 ⟶ Y_1),
      (typeToCat.map ((fun {X Y} F => Discrete.as ∘ F.obj ∘ Discrete.mk) F)).map f =
        eqToHom (_ : ?F.obj X_1 = ?G.obj X_1) ≫
          F.map f ≫
            eqToHom (_ : F.obj Y_1 = (typeToCat.map ((fun {X Y} F => Discrete.as ∘ F.obj ∘ Discrete.mk) F)).obj Y_1))
    _auto✝
[PROOFSTEP]
intro x y f
[GOAL]
case h_map
X Y : Type u
F : typeToCat.obj X ⟶ typeToCat.obj Y
x y : ↑(typeToCat.obj X)
f : x ⟶ y
⊢ (typeToCat.map ((fun {X Y} F => Discrete.as ∘ F.obj ∘ Discrete.mk) F)).map f =
    eqToHom (_ : ?F.obj x = ?G.obj x) ≫
      F.map f ≫ eqToHom (_ : F.obj y = (typeToCat.map ((fun {X Y} F => Discrete.as ∘ F.obj ∘ Discrete.mk) F)).obj y)
[PROOFSTEP]
dsimp
[GOAL]
case h_map
X Y : Type u
F : typeToCat.obj X ⟶ typeToCat.obj Y
x y : ↑(typeToCat.obj X)
f : x ⟶ y
⊢ (Discrete.functor (Discrete.mk ∘ Discrete.as ∘ F.obj ∘ Discrete.mk)).map f =
    𝟙 ((Discrete.functor (Discrete.mk ∘ Discrete.as ∘ F.obj ∘ Discrete.mk)).obj x) ≫ F.map f ≫ 𝟙 (F.obj y)
[PROOFSTEP]
apply ULift.ext
[GOAL]
case h_map.h
X Y : Type u
F : typeToCat.obj X ⟶ typeToCat.obj Y
x y : ↑(typeToCat.obj X)
f : x ⟶ y
⊢ ((Discrete.functor (Discrete.mk ∘ Discrete.as ∘ F.obj ∘ Discrete.mk)).map f).down =
    (𝟙 ((Discrete.functor (Discrete.mk ∘ Discrete.as ∘ F.obj ∘ Discrete.mk)).obj x) ≫ F.map f ≫ 𝟙 (F.obj y)).down
[PROOFSTEP]
aesop_cat
[GOAL]
case h_obj
X Y : Type u
F : typeToCat.obj X ⟶ typeToCat.obj Y
⊢ ∀ (X_1 : ↑(typeToCat.obj X)),
    (typeToCat.map ((fun {X Y} F => Discrete.as ∘ F.obj ∘ Discrete.mk) F)).obj X_1 = F.obj X_1
[PROOFSTEP]
rintro ⟨x⟩
[GOAL]
case h_obj.mk
X Y : Type u
F : typeToCat.obj X ⟶ typeToCat.obj Y
x : X
⊢ (typeToCat.map ((fun {X Y} F => Discrete.as ∘ F.obj ∘ Discrete.mk) F)).obj { as := x } = F.obj { as := x }
[PROOFSTEP]
apply Discrete.ext
[GOAL]
case h_obj.mk.as
X Y : Type u
F : typeToCat.obj X ⟶ typeToCat.obj Y
x : X
⊢ ((typeToCat.map ((fun {X Y} F => Discrete.as ∘ F.obj ∘ Discrete.mk) F)).obj { as := x }).as = (F.obj { as := x }).as
[PROOFSTEP]
rfl


[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
X✝ Y✝ Z✝ : C ⊕ D
X Y Z : C
x✝¹ : inl X ⟶ inl Y
x✝ : inl Y ⟶ inl Z
⊢ {
          obj := fun X =>
            match X with
            | inl X => inr X
            | inr X => inl X,
          map := fun X Y f =>
            match X, Y, f with
            | inl val, inl val_1, f => f
            | inr val, inr val_1, f => f }.map
      (x✝¹ ≫ x✝) =
    {
            obj := fun X =>
              match X with
              | inl X => inr X
              | inr X => inl X,
            map := fun X Y f =>
              match X, Y, f with
              | inl val, inl val_1, f => f
              | inr val, inr val_1, f => f }.map
        x✝¹ ≫
      {
            obj := fun X =>
              match X with
              | inl X => inr X
              | inr X => inl X,
            map := fun X Y f =>
              match X, Y, f with
              | inl val, inl val_1, f => f
              | inr val, inr val_1, f => f }.map
        x✝
[PROOFSTEP]
rfl
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
X✝ Y✝ Z✝ : C ⊕ D
X Y Z : D
x✝¹ : inr X ⟶ inr Y
x✝ : inr Y ⟶ inr Z
⊢ {
          obj := fun X =>
            match X with
            | inl X => inr X
            | inr X => inl X,
          map := fun X Y f =>
            match X, Y, f with
            | inl val, inl val_1, f => f
            | inr val, inr val_1, f => f }.map
      (x✝¹ ≫ x✝) =
    {
            obj := fun X =>
              match X with
              | inl X => inr X
              | inr X => inl X,
            map := fun X Y f =>
              match X, Y, f with
              | inl val, inl val_1, f => f
              | inr val, inr val_1, f => f }.map
        x✝¹ ≫
      {
            obj := fun X =>
              match X with
              | inl X => inr X
              | inr X => inl X,
            map := fun X Y f =>
              match X, Y, f with
              | inl val, inl val_1, f => f
              | inr val, inr val_1, f => f }.map
        x✝
[PROOFSTEP]
rfl
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
X : C ⊕ D
⊢ (𝟭 (C ⊕ D)).obj X = (swap C D ⋙ swap D C).obj X
[PROOFSTEP]
cases X
[GOAL]
case inl
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
val✝ : C
⊢ (𝟭 (C ⊕ D)).obj (inl val✝) = (swap C D ⋙ swap D C).obj (inl val✝)
[PROOFSTEP]
rfl
[GOAL]
case inr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
val✝ : D
⊢ (𝟭 (C ⊕ D)).obj (inr val✝) = (swap C D ⋙ swap D C).obj (inr val✝)
[PROOFSTEP]
rfl
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
⊢ ∀ {X Y : C ⊕ D} (f : X ⟶ Y),
    (𝟭 (C ⊕ D)).map f ≫ ((fun X => eqToIso (_ : (𝟭 (C ⊕ D)).obj X = (swap C D ⋙ swap D C).obj X)) Y).hom =
      ((fun X => eqToIso (_ : (𝟭 (C ⊕ D)).obj X = (swap C D ⋙ swap D C).obj X)) X).hom ≫ (swap C D ⋙ swap D C).map f
[PROOFSTEP]
simp only [swap]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
⊢ ∀ {X Y : C ⊕ D} (f : X ⟶ Y),
    (𝟭 (C ⊕ D)).map f ≫ (eqToIso (_ : (𝟭 (C ⊕ D)).obj Y = (swap C D ⋙ swap D C).obj Y)).hom =
      (eqToIso (_ : (𝟭 (C ⊕ D)).obj X = (swap C D ⋙ swap D C).obj X)).hom ≫
        (Functor.mk
                {
                  obj := fun X =>
                    match X with
                    | inl X => inr X
                    | inr X => inl X,
                  map := fun X Y f =>
                    match X, Y, f with
                    | inl val, inl val_1, f => f
                    | inr val, inr val_1, f => f } ⋙
              Functor.mk
                {
                  obj := fun X =>
                    match X with
                    | inl X => inr X
                    | inr X => inl X,
                  map := fun X Y f =>
                    match X, Y, f with
                    | inl val, inl val_1, f => f
                    | inr val, inr val_1, f => f }).map
          f
[PROOFSTEP]
aesop_cat_nonterminal
[GOAL]
case inl.inr
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
val : C
val_1 : D
f : inl val ⟶ inr val_1
⊢ f =
    match inr val, inl val_1,
      match inl val, inr val_1, f with
      | inl val, inl val_2, f => f
      | inr val, inr val_2, f => f with
    | inl val, inl val_2, f => f
    | inr val, inr val_2, f => f
case inr.inl
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
val : D
val_1 : C
f : inr val ⟶ inl val_1
⊢ f =
    match inl val, inr val_1,
      match inr val, inl val_1, f with
      | inl val, inl val_2, f => f
      | inr val, inr val_2, f => f with
    | inl val, inl val_2, f => f
    | inr val, inr val_2, f => f
[PROOFSTEP]
cases f
[GOAL]
case inr.inl
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
val : D
val_1 : C
f : inr val ⟶ inl val_1
⊢ f =
    match inl val, inr val_1,
      match inr val, inl val_1, f with
      | inl val, inl val_2, f => f
      | inr val, inr val_2, f => f with
    | inl val, inl val_2, f => f
    | inr val, inr val_2, f => f
[PROOFSTEP]
cases f
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
X : D ⊕ C
⊢ (swap D C ⋙ swap C D).obj X = (𝟭 (D ⊕ C)).obj X
[PROOFSTEP]
cases X
[GOAL]
case inl
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
val✝ : D
⊢ (swap D C ⋙ swap C D).obj (inl val✝) = (𝟭 (D ⊕ C)).obj (inl val✝)
[PROOFSTEP]
rfl
[GOAL]
case inr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
val✝ : C
⊢ (swap D C ⋙ swap C D).obj (inr val✝) = (𝟭 (D ⊕ C)).obj (inr val✝)
[PROOFSTEP]
rfl
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
⊢ ∀ {X Y : D ⊕ C} (f : X ⟶ Y),
    (swap D C ⋙ swap C D).map f ≫ ((fun X => eqToIso (_ : (swap D C ⋙ swap C D).obj X = (𝟭 (D ⊕ C)).obj X)) Y).hom =
      ((fun X => eqToIso (_ : (swap D C ⋙ swap C D).obj X = (𝟭 (D ⊕ C)).obj X)) X).hom ≫ (𝟭 (D ⊕ C)).map f
[PROOFSTEP]
simp only [swap]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
⊢ ∀ {X Y : D ⊕ C} (f : X ⟶ Y),
    (Functor.mk
                {
                  obj := fun X =>
                    match X with
                    | inl X => inr X
                    | inr X => inl X,
                  map := fun X Y f =>
                    match X, Y, f with
                    | inl val, inl val_1, f => f
                    | inr val, inr val_1, f => f } ⋙
              Functor.mk
                {
                  obj := fun X =>
                    match X with
                    | inl X => inr X
                    | inr X => inl X,
                  map := fun X Y f =>
                    match X, Y, f with
                    | inl val, inl val_1, f => f
                    | inr val, inr val_1, f => f }).map
          f ≫
        (eqToIso (_ : (swap D C ⋙ swap C D).obj Y = (𝟭 (D ⊕ C)).obj Y)).hom =
      (eqToIso (_ : (swap D C ⋙ swap C D).obj X = (𝟭 (D ⊕ C)).obj X)).hom ≫ (𝟭 (D ⊕ C)).map f
[PROOFSTEP]
aesop_cat_nonterminal
[GOAL]
case inl.inr
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
val : D
val_1 : C
f : inl val ⟶ inr val_1
⊢ (match inr val, inl val_1,
      match inl val, inr val_1, f with
      | inl val, inl val_2, f => f
      | inr val, inr val_2, f => f with
    | inl val, inl val_2, f => f
    | inr val, inr val_2, f => f) =
    f
case inr.inl
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
val : C
val_1 : D
f : inr val ⟶ inl val_1
⊢ (match inl val, inr val_1,
      match inr val, inl val_1, f with
      | inl val, inl val_2, f => f
      | inr val, inr val_2, f => f with
    | inl val, inl val_2, f => f
    | inr val, inr val_2, f => f) =
    f
[PROOFSTEP]
cases f
[GOAL]
case inr.inl
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
val : C
val_1 : D
f : inr val ⟶ inl val_1
⊢ (match inl val, inr val_1,
      match inr val, inl val_1, f with
      | inl val, inl val_2, f => f
      | inr val, inr val_2, f => f with
    | inl val, inl val_2, f => f
    | inr val, inr val_2, f => f) =
    f
[PROOFSTEP]
cases f
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
⊢ IsEquivalence (equivalence C D).functor
[PROOFSTEP]
infer_instance
[GOAL]
A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₁
inst✝² : Category.{v₁, u₁} B
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : A ⥤ B
G : C ⥤ D
X : A ⊕ C
⊢ {
          obj := fun X =>
            match X with
            | inl X => inl (F.obj X)
            | inr X => inr (G.obj X),
          map := fun X Y f =>
            match X, Y, f with
            | inl X, inl Y, f => F.map f
            | inr X, inr Y, f => G.map f }.map
      (𝟙 X) =
    𝟙
      ({
            obj := fun X =>
              match X with
              | inl X => inl (F.obj X)
              | inr X => inr (G.obj X),
            map := fun X Y f =>
              match X, Y, f with
              | inl X, inl Y, f => F.map f
              | inr X, inr Y, f => G.map f }.obj
        X)
[PROOFSTEP]
cases X
[GOAL]
case inl
A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₁
inst✝² : Category.{v₁, u₁} B
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : A ⥤ B
G : C ⥤ D
val✝ : A
⊢ {
          obj := fun X =>
            match X with
            | inl X => inl (F.obj X)
            | inr X => inr (G.obj X),
          map := fun X Y f =>
            match X, Y, f with
            | inl X, inl Y, f => F.map f
            | inr X, inr Y, f => G.map f }.map
      (𝟙 (inl val✝)) =
    𝟙
      ({
            obj := fun X =>
              match X with
              | inl X => inl (F.obj X)
              | inr X => inr (G.obj X),
            map := fun X Y f =>
              match X, Y, f with
              | inl X, inl Y, f => F.map f
              | inr X, inr Y, f => G.map f }.obj
        (inl val✝))
[PROOFSTEP]
aesop_cat_nonterminal
[GOAL]
case inr
A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₁
inst✝² : Category.{v₁, u₁} B
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : A ⥤ B
G : C ⥤ D
val✝ : C
⊢ {
          obj := fun X =>
            match X with
            | inl X => inl (F.obj X)
            | inr X => inr (G.obj X),
          map := fun X Y f =>
            match X, Y, f with
            | inl X, inl Y, f => F.map f
            | inr X, inr Y, f => G.map f }.map
      (𝟙 (inr val✝)) =
    𝟙
      ({
            obj := fun X =>
              match X with
              | inl X => inl (F.obj X)
              | inr X => inr (G.obj X),
            map := fun X Y f =>
              match X, Y, f with
              | inl X, inl Y, f => F.map f
              | inr X, inr Y, f => G.map f }.obj
        (inr val✝))
[PROOFSTEP]
aesop_cat_nonterminal
[GOAL]
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₁
inst_1 : Category.{v₁, u₁} B
C : Type u₁
inst_2 : Category.{v₁, u₁} C
D : Type u₁
inst_3 : Category.{v₁, u₁} D
F : A ⥤ B
G : C ⥤ D
val : A
⊢ F.map (𝟙 (inl val)) = 𝟙 (inl (F.obj val))
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₁
inst_1 : Category.{v₁, u₁} B
C : Type u₁
inst_2 : Category.{v₁, u₁} C
D : Type u₁
inst_3 : Category.{v₁, u₁} D
F : A ⥤ B
G : C ⥤ D
val : C
⊢ G.map (𝟙 (inr val)) = 𝟙 (inr (G.obj val))
[PROOFSTEP]
erw [F.map_id]
[GOAL]
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₁
inst_1 : Category.{v₁, u₁} B
C : Type u₁
inst_2 : Category.{v₁, u₁} C
D : Type u₁
inst_3 : Category.{v₁, u₁} D
F : A ⥤ B
G : C ⥤ D
val : A
⊢ 𝟙 (F.obj val) = 𝟙 (inl (F.obj val))
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₁
inst_1 : Category.{v₁, u₁} B
C : Type u₁
inst_2 : Category.{v₁, u₁} C
D : Type u₁
inst_3 : Category.{v₁, u₁} D
F : A ⥤ B
G : C ⥤ D
val : C
⊢ G.map (𝟙 (inr val)) = 𝟙 (inr (G.obj val))
[PROOFSTEP]
rfl
[GOAL]
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₁
inst_1 : Category.{v₁, u₁} B
C : Type u₁
inst_2 : Category.{v₁, u₁} C
D : Type u₁
inst_3 : Category.{v₁, u₁} D
F : A ⥤ B
G : C ⥤ D
val : C
⊢ G.map (𝟙 (inr val)) = 𝟙 (inr (G.obj val))
[PROOFSTEP]
erw [G.map_id]
[GOAL]
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₁
inst_1 : Category.{v₁, u₁} B
C : Type u₁
inst_2 : Category.{v₁, u₁} C
D : Type u₁
inst_3 : Category.{v₁, u₁} D
F : A ⥤ B
G : C ⥤ D
val : C
⊢ 𝟙 (G.obj val) = 𝟙 (inr (G.obj val))
[PROOFSTEP]
rfl
[GOAL]
A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₁
inst✝² : Category.{v₁, u₁} B
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : A ⥤ B
G : C ⥤ D
X✝ Y✝ Z✝ : A ⊕ C
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
X Y Z : A
f : inl X ⟶ inl Y
g : inl Y ⟶ inl Z
⊢ {
          obj := fun X =>
            match X with
            | inl X => inl (F.obj X)
            | inr X => inr (G.obj X),
          map := fun X Y f =>
            match X, Y, f with
            | inl X, inl Y, f => F.map f
            | inr X, inr Y, f => G.map f }.map
      (f ≫ g) =
    {
            obj := fun X =>
              match X with
              | inl X => inl (F.obj X)
              | inr X => inr (G.obj X),
            map := fun X Y f =>
              match X, Y, f with
              | inl X, inl Y, f => F.map f
              | inr X, inr Y, f => G.map f }.map
        f ≫
      {
            obj := fun X =>
              match X with
              | inl X => inl (F.obj X)
              | inr X => inr (G.obj X),
            map := fun X Y f =>
              match X, Y, f with
              | inl X, inl Y, f => F.map f
              | inr X, inr Y, f => G.map f }.map
        g
[PROOFSTEP]
aesop_cat_nonterminal
[GOAL]
case inl.inl.inl
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₁
inst_1 : Category.{v₁, u₁} B
C : Type u₁
inst_2 : Category.{v₁, u₁} C
D : Type u₁
inst_3 : Category.{v₁, u₁} D
F : A ⥤ B
G : C ⥤ D
X Y Z : A
f : inl X ⟶ inl Y
g : inl Y ⟶ inl Z
val val_1 : A
f_1 : inl val ⟶ inl val_1
val_2 : A
g_1 : inl val_1 ⟶ inl val_2
⊢ F.map (f ≫ g) = F.map f ≫ F.map g
[PROOFSTEP]
erw [F.map_comp]
[GOAL]
case inl.inl.inr
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₁
inst_1 : Category.{v₁, u₁} B
C : Type u₁
inst_2 : Category.{v₁, u₁} C
D : Type u₁
inst_3 : Category.{v₁, u₁} D
F : A ⥤ B
G : C ⥤ D
X Y Z : A
f : inl X ⟶ inl Y
g : inl Y ⟶ inl Z
val val_1 : A
f_1 : inl val ⟶ inl val_1
val_2 : C
g_1 : inl val_1 ⟶ inr val_2
⊢ F.map (f ≫ g) = F.map f ≫ F.map g
[PROOFSTEP]
erw [F.map_comp]
[GOAL]
case inl.inr.inl
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₁
inst_1 : Category.{v₁, u₁} B
C : Type u₁
inst_2 : Category.{v₁, u₁} C
D : Type u₁
inst_3 : Category.{v₁, u₁} D
F : A ⥤ B
G : C ⥤ D
X Y Z : A
f : inl X ⟶ inl Y
g : inl Y ⟶ inl Z
val : A
val_1 : C
f_1 : inl val ⟶ inr val_1
val_2 : A
g_1 : inr val_1 ⟶ inl val_2
⊢ F.map (f ≫ g) = F.map f ≫ F.map g
[PROOFSTEP]
erw [F.map_comp]
[GOAL]
case inl.inr.inr
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₁
inst_1 : Category.{v₁, u₁} B
C : Type u₁
inst_2 : Category.{v₁, u₁} C
D : Type u₁
inst_3 : Category.{v₁, u₁} D
F : A ⥤ B
G : C ⥤ D
X Y Z : A
f : inl X ⟶ inl Y
g : inl Y ⟶ inl Z
val : A
val_1 : C
f_1 : inl val ⟶ inr val_1
val_2 : C
g_1 : inr val_1 ⟶ inr val_2
⊢ F.map (f ≫ g) = F.map f ≫ F.map g
[PROOFSTEP]
erw [F.map_comp]
[GOAL]
case inr.inl.inl
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₁
inst_1 : Category.{v₁, u₁} B
C : Type u₁
inst_2 : Category.{v₁, u₁} C
D : Type u₁
inst_3 : Category.{v₁, u₁} D
F : A ⥤ B
G : C ⥤ D
X Y Z : A
f : inl X ⟶ inl Y
g : inl Y ⟶ inl Z
val : C
val_1 : A
f_1 : inr val ⟶ inl val_1
val_2 : A
g_1 : inl val_1 ⟶ inl val_2
⊢ F.map (f ≫ g) = F.map f ≫ F.map g
[PROOFSTEP]
erw [F.map_comp]
[GOAL]
case inr.inl.inr
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₁
inst_1 : Category.{v₁, u₁} B
C : Type u₁
inst_2 : Category.{v₁, u₁} C
D : Type u₁
inst_3 : Category.{v₁, u₁} D
F : A ⥤ B
G : C ⥤ D
X Y Z : A
f : inl X ⟶ inl Y
g : inl Y ⟶ inl Z
val : C
val_1 : A
f_1 : inr val ⟶ inl val_1
val_2 : C
g_1 : inl val_1 ⟶ inr val_2
⊢ F.map (f ≫ g) = F.map f ≫ F.map g
[PROOFSTEP]
erw [F.map_comp]
[GOAL]
case inr.inr.inl
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₁
inst_1 : Category.{v₁, u₁} B
C : Type u₁
inst_2 : Category.{v₁, u₁} C
D : Type u₁
inst_3 : Category.{v₁, u₁} D
F : A ⥤ B
G : C ⥤ D
X Y Z : A
f : inl X ⟶ inl Y
g : inl Y ⟶ inl Z
val val_1 : C
f_1 : inr val ⟶ inr val_1
val_2 : A
g_1 : inr val_1 ⟶ inl val_2
⊢ F.map (f ≫ g) = F.map f ≫ F.map g
[PROOFSTEP]
erw [F.map_comp]
[GOAL]
case inr.inr.inr
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₁
inst_1 : Category.{v₁, u₁} B
C : Type u₁
inst_2 : Category.{v₁, u₁} C
D : Type u₁
inst_3 : Category.{v₁, u₁} D
F : A ⥤ B
G : C ⥤ D
X Y Z : A
f : inl X ⟶ inl Y
g : inl Y ⟶ inl Z
val val_1 : C
f_1 : inr val ⟶ inr val_1
val_2 : C
g_1 : inr val_1 ⟶ inr val_2
⊢ F.map (f ≫ g) = F.map f ≫ F.map g
[PROOFSTEP]
erw [F.map_comp]
[GOAL]
case inl.inl.inl
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₁
inst_1 : Category.{v₁, u₁} B
C : Type u₁
inst_2 : Category.{v₁, u₁} C
D : Type u₁
inst_3 : Category.{v₁, u₁} D
F : A ⥤ B
G : C ⥤ D
X Y Z : A
f : inl X ⟶ inl Y
g : inl Y ⟶ inl Z
val val_1 : A
f_1 : inl val ⟶ inl val_1
val_2 : A
g_1 : inl val_1 ⟶ inl val_2
⊢ F.map f ≫ F.map g = F.map f ≫ F.map g
[PROOFSTEP]
rfl
[GOAL]
case inl.inl.inr
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₁
inst_1 : Category.{v₁, u₁} B
C : Type u₁
inst_2 : Category.{v₁, u₁} C
D : Type u₁
inst_3 : Category.{v₁, u₁} D
F : A ⥤ B
G : C ⥤ D
X Y Z : A
f : inl X ⟶ inl Y
g : inl Y ⟶ inl Z
val val_1 : A
f_1 : inl val ⟶ inl val_1
val_2 : C
g_1 : inl val_1 ⟶ inr val_2
⊢ F.map f ≫ F.map g = F.map f ≫ F.map g
[PROOFSTEP]
rfl
[GOAL]
case inl.inr.inl
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₁
inst_1 : Category.{v₁, u₁} B
C : Type u₁
inst_2 : Category.{v₁, u₁} C
D : Type u₁
inst_3 : Category.{v₁, u₁} D
F : A ⥤ B
G : C ⥤ D
X Y Z : A
f : inl X ⟶ inl Y
g : inl Y ⟶ inl Z
val : A
val_1 : C
f_1 : inl val ⟶ inr val_1
val_2 : A
g_1 : inr val_1 ⟶ inl val_2
⊢ F.map f ≫ F.map g = F.map f ≫ F.map g
[PROOFSTEP]
rfl
[GOAL]
case inl.inr.inr
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₁
inst_1 : Category.{v₁, u₁} B
C : Type u₁
inst_2 : Category.{v₁, u₁} C
D : Type u₁
inst_3 : Category.{v₁, u₁} D
F : A ⥤ B
G : C ⥤ D
X Y Z : A
f : inl X ⟶ inl Y
g : inl Y ⟶ inl Z
val : A
val_1 : C
f_1 : inl val ⟶ inr val_1
val_2 : C
g_1 : inr val_1 ⟶ inr val_2
⊢ F.map f ≫ F.map g = F.map f ≫ F.map g
[PROOFSTEP]
rfl
[GOAL]
case inr.inl.inl
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₁
inst_1 : Category.{v₁, u₁} B
C : Type u₁
inst_2 : Category.{v₁, u₁} C
D : Type u₁
inst_3 : Category.{v₁, u₁} D
F : A ⥤ B
G : C ⥤ D
X Y Z : A
f : inl X ⟶ inl Y
g : inl Y ⟶ inl Z
val : C
val_1 : A
f_1 : inr val ⟶ inl val_1
val_2 : A
g_1 : inl val_1 ⟶ inl val_2
⊢ F.map f ≫ F.map g = F.map f ≫ F.map g
[PROOFSTEP]
rfl
[GOAL]
case inr.inl.inr
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₁
inst_1 : Category.{v₁, u₁} B
C : Type u₁
inst_2 : Category.{v₁, u₁} C
D : Type u₁
inst_3 : Category.{v₁, u₁} D
F : A ⥤ B
G : C ⥤ D
X Y Z : A
f : inl X ⟶ inl Y
g : inl Y ⟶ inl Z
val : C
val_1 : A
f_1 : inr val ⟶ inl val_1
val_2 : C
g_1 : inl val_1 ⟶ inr val_2
⊢ F.map f ≫ F.map g = F.map f ≫ F.map g
[PROOFSTEP]
rfl
[GOAL]
case inr.inr.inl
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₁
inst_1 : Category.{v₁, u₁} B
C : Type u₁
inst_2 : Category.{v₁, u₁} C
D : Type u₁
inst_3 : Category.{v₁, u₁} D
F : A ⥤ B
G : C ⥤ D
X Y Z : A
f : inl X ⟶ inl Y
g : inl Y ⟶ inl Z
val val_1 : C
f_1 : inr val ⟶ inr val_1
val_2 : A
g_1 : inr val_1 ⟶ inl val_2
⊢ F.map f ≫ F.map g = F.map f ≫ F.map g
[PROOFSTEP]
rfl
[GOAL]
case inr.inr.inr
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₁
inst_1 : Category.{v₁, u₁} B
C : Type u₁
inst_2 : Category.{v₁, u₁} C
D : Type u₁
inst_3 : Category.{v₁, u₁} D
F : A ⥤ B
G : C ⥤ D
X Y Z : A
f : inl X ⟶ inl Y
g : inl Y ⟶ inl Z
val val_1 : C
f_1 : inr val ⟶ inr val_1
val_2 : C
g_1 : inr val_1 ⟶ inr val_2
⊢ F.map f ≫ F.map g = F.map f ≫ F.map g
[PROOFSTEP]
rfl
[GOAL]
A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₁
inst✝² : Category.{v₁, u₁} B
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : A ⥤ B
G : C ⥤ D
X✝ Y✝ Z✝ : A ⊕ C
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
X Y Z : C
f : inr X ⟶ inr Y
g : inr Y ⟶ inr Z
⊢ {
          obj := fun X =>
            match X with
            | inl X => inl (F.obj X)
            | inr X => inr (G.obj X),
          map := fun X Y f =>
            match X, Y, f with
            | inl X, inl Y, f => F.map f
            | inr X, inr Y, f => G.map f }.map
      (f ≫ g) =
    {
            obj := fun X =>
              match X with
              | inl X => inl (F.obj X)
              | inr X => inr (G.obj X),
            map := fun X Y f =>
              match X, Y, f with
              | inl X, inl Y, f => F.map f
              | inr X, inr Y, f => G.map f }.map
        f ≫
      {
            obj := fun X =>
              match X with
              | inl X => inl (F.obj X)
              | inr X => inr (G.obj X),
            map := fun X Y f =>
              match X, Y, f with
              | inl X, inl Y, f => F.map f
              | inr X, inr Y, f => G.map f }.map
        g
[PROOFSTEP]
aesop_cat_nonterminal
[GOAL]
case inl.inl.inl
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₁
inst_1 : Category.{v₁, u₁} B
C : Type u₁
inst_2 : Category.{v₁, u₁} C
D : Type u₁
inst_3 : Category.{v₁, u₁} D
F : A ⥤ B
G : C ⥤ D
X Y Z : C
f : inr X ⟶ inr Y
g : inr Y ⟶ inr Z
val val_1 : A
f_1 : inl val ⟶ inl val_1
val_2 : A
g_1 : inl val_1 ⟶ inl val_2
⊢ G.map (f ≫ g) = G.map f ≫ G.map g
[PROOFSTEP]
erw [G.map_comp]
[GOAL]
case inl.inl.inr
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₁
inst_1 : Category.{v₁, u₁} B
C : Type u₁
inst_2 : Category.{v₁, u₁} C
D : Type u₁
inst_3 : Category.{v₁, u₁} D
F : A ⥤ B
G : C ⥤ D
X Y Z : C
f : inr X ⟶ inr Y
g : inr Y ⟶ inr Z
val val_1 : A
f_1 : inl val ⟶ inl val_1
val_2 : C
g_1 : inl val_1 ⟶ inr val_2
⊢ G.map (f ≫ g) = G.map f ≫ G.map g
[PROOFSTEP]
erw [G.map_comp]
[GOAL]
case inl.inr.inl
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₁
inst_1 : Category.{v₁, u₁} B
C : Type u₁
inst_2 : Category.{v₁, u₁} C
D : Type u₁
inst_3 : Category.{v₁, u₁} D
F : A ⥤ B
G : C ⥤ D
X Y Z : C
f : inr X ⟶ inr Y
g : inr Y ⟶ inr Z
val : A
val_1 : C
f_1 : inl val ⟶ inr val_1
val_2 : A
g_1 : inr val_1 ⟶ inl val_2
⊢ G.map (f ≫ g) = G.map f ≫ G.map g
[PROOFSTEP]
erw [G.map_comp]
[GOAL]
case inl.inr.inr
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₁
inst_1 : Category.{v₁, u₁} B
C : Type u₁
inst_2 : Category.{v₁, u₁} C
D : Type u₁
inst_3 : Category.{v₁, u₁} D
F : A ⥤ B
G : C ⥤ D
X Y Z : C
f : inr X ⟶ inr Y
g : inr Y ⟶ inr Z
val : A
val_1 : C
f_1 : inl val ⟶ inr val_1
val_2 : C
g_1 : inr val_1 ⟶ inr val_2
⊢ G.map (f ≫ g) = G.map f ≫ G.map g
[PROOFSTEP]
erw [G.map_comp]
[GOAL]
case inr.inl.inl
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₁
inst_1 : Category.{v₁, u₁} B
C : Type u₁
inst_2 : Category.{v₁, u₁} C
D : Type u₁
inst_3 : Category.{v₁, u₁} D
F : A ⥤ B
G : C ⥤ D
X Y Z : C
f : inr X ⟶ inr Y
g : inr Y ⟶ inr Z
val : C
val_1 : A
f_1 : inr val ⟶ inl val_1
val_2 : A
g_1 : inl val_1 ⟶ inl val_2
⊢ G.map (f ≫ g) = G.map f ≫ G.map g
[PROOFSTEP]
erw [G.map_comp]
[GOAL]
case inr.inl.inr
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₁
inst_1 : Category.{v₁, u₁} B
C : Type u₁
inst_2 : Category.{v₁, u₁} C
D : Type u₁
inst_3 : Category.{v₁, u₁} D
F : A ⥤ B
G : C ⥤ D
X Y Z : C
f : inr X ⟶ inr Y
g : inr Y ⟶ inr Z
val : C
val_1 : A
f_1 : inr val ⟶ inl val_1
val_2 : C
g_1 : inl val_1 ⟶ inr val_2
⊢ G.map (f ≫ g) = G.map f ≫ G.map g
[PROOFSTEP]
erw [G.map_comp]
[GOAL]
case inr.inr.inl
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₁
inst_1 : Category.{v₁, u₁} B
C : Type u₁
inst_2 : Category.{v₁, u₁} C
D : Type u₁
inst_3 : Category.{v₁, u₁} D
F : A ⥤ B
G : C ⥤ D
X Y Z : C
f : inr X ⟶ inr Y
g : inr Y ⟶ inr Z
val val_1 : C
f_1 : inr val ⟶ inr val_1
val_2 : A
g_1 : inr val_1 ⟶ inl val_2
⊢ G.map (f ≫ g) = G.map f ≫ G.map g
[PROOFSTEP]
erw [G.map_comp]
[GOAL]
case inr.inr.inr
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₁
inst_1 : Category.{v₁, u₁} B
C : Type u₁
inst_2 : Category.{v₁, u₁} C
D : Type u₁
inst_3 : Category.{v₁, u₁} D
F : A ⥤ B
G : C ⥤ D
X Y Z : C
f : inr X ⟶ inr Y
g : inr Y ⟶ inr Z
val val_1 : C
f_1 : inr val ⟶ inr val_1
val_2 : C
g_1 : inr val_1 ⟶ inr val_2
⊢ G.map (f ≫ g) = G.map f ≫ G.map g
[PROOFSTEP]
erw [G.map_comp]
[GOAL]
case inl.inl.inl
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₁
inst_1 : Category.{v₁, u₁} B
C : Type u₁
inst_2 : Category.{v₁, u₁} C
D : Type u₁
inst_3 : Category.{v₁, u₁} D
F : A ⥤ B
G : C ⥤ D
X Y Z : C
f : inr X ⟶ inr Y
g : inr Y ⟶ inr Z
val val_1 : A
f_1 : inl val ⟶ inl val_1
val_2 : A
g_1 : inl val_1 ⟶ inl val_2
⊢ G.map f ≫ G.map g = G.map f ≫ G.map g
[PROOFSTEP]
rfl
[GOAL]
case inl.inl.inr
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₁
inst_1 : Category.{v₁, u₁} B
C : Type u₁
inst_2 : Category.{v₁, u₁} C
D : Type u₁
inst_3 : Category.{v₁, u₁} D
F : A ⥤ B
G : C ⥤ D
X Y Z : C
f : inr X ⟶ inr Y
g : inr Y ⟶ inr Z
val val_1 : A
f_1 : inl val ⟶ inl val_1
val_2 : C
g_1 : inl val_1 ⟶ inr val_2
⊢ G.map f ≫ G.map g = G.map f ≫ G.map g
[PROOFSTEP]
rfl
[GOAL]
case inl.inr.inl
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₁
inst_1 : Category.{v₁, u₁} B
C : Type u₁
inst_2 : Category.{v₁, u₁} C
D : Type u₁
inst_3 : Category.{v₁, u₁} D
F : A ⥤ B
G : C ⥤ D
X Y Z : C
f : inr X ⟶ inr Y
g : inr Y ⟶ inr Z
val : A
val_1 : C
f_1 : inl val ⟶ inr val_1
val_2 : A
g_1 : inr val_1 ⟶ inl val_2
⊢ G.map f ≫ G.map g = G.map f ≫ G.map g
[PROOFSTEP]
rfl
[GOAL]
case inl.inr.inr
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₁
inst_1 : Category.{v₁, u₁} B
C : Type u₁
inst_2 : Category.{v₁, u₁} C
D : Type u₁
inst_3 : Category.{v₁, u₁} D
F : A ⥤ B
G : C ⥤ D
X Y Z : C
f : inr X ⟶ inr Y
g : inr Y ⟶ inr Z
val : A
val_1 : C
f_1 : inl val ⟶ inr val_1
val_2 : C
g_1 : inr val_1 ⟶ inr val_2
⊢ G.map f ≫ G.map g = G.map f ≫ G.map g
[PROOFSTEP]
rfl
[GOAL]
case inr.inl.inl
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₁
inst_1 : Category.{v₁, u₁} B
C : Type u₁
inst_2 : Category.{v₁, u₁} C
D : Type u₁
inst_3 : Category.{v₁, u₁} D
F : A ⥤ B
G : C ⥤ D
X Y Z : C
f : inr X ⟶ inr Y
g : inr Y ⟶ inr Z
val : C
val_1 : A
f_1 : inr val ⟶ inl val_1
val_2 : A
g_1 : inl val_1 ⟶ inl val_2
⊢ G.map f ≫ G.map g = G.map f ≫ G.map g
[PROOFSTEP]
rfl
[GOAL]
case inr.inl.inr
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₁
inst_1 : Category.{v₁, u₁} B
C : Type u₁
inst_2 : Category.{v₁, u₁} C
D : Type u₁
inst_3 : Category.{v₁, u₁} D
F : A ⥤ B
G : C ⥤ D
X Y Z : C
f : inr X ⟶ inr Y
g : inr Y ⟶ inr Z
val : C
val_1 : A
f_1 : inr val ⟶ inl val_1
val_2 : C
g_1 : inl val_1 ⟶ inr val_2
⊢ G.map f ≫ G.map g = G.map f ≫ G.map g
[PROOFSTEP]
rfl
[GOAL]
case inr.inr.inl
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₁
inst_1 : Category.{v₁, u₁} B
C : Type u₁
inst_2 : Category.{v₁, u₁} C
D : Type u₁
inst_3 : Category.{v₁, u₁} D
F : A ⥤ B
G : C ⥤ D
X Y Z : C
f : inr X ⟶ inr Y
g : inr Y ⟶ inr Z
val val_1 : C
f_1 : inr val ⟶ inr val_1
val_2 : A
g_1 : inr val_1 ⟶ inl val_2
⊢ G.map f ≫ G.map g = G.map f ≫ G.map g
[PROOFSTEP]
rfl
[GOAL]
case inr.inr.inr
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₁
inst_1 : Category.{v₁, u₁} B
C : Type u₁
inst_2 : Category.{v₁, u₁} C
D : Type u₁
inst_3 : Category.{v₁, u₁} D
F : A ⥤ B
G : C ⥤ D
X Y Z : C
f : inr X ⟶ inr Y
g : inr Y ⟶ inr Z
val val_1 : C
f_1 : inr val ⟶ inr val_1
val_2 : C
g_1 : inr val_1 ⟶ inr val_2
⊢ G.map f ≫ G.map g = G.map f ≫ G.map g
[PROOFSTEP]
rfl
[GOAL]
A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₁
inst✝² : Category.{v₁, u₁} B
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F G : A ⥤ B
H I : C ⥤ D
α : F ⟶ G
β : H ⟶ I
X✝ Y✝ : A ⊕ C
f✝ : X✝ ⟶ Y✝
X Y : A
f : inl X ⟶ inl Y
⊢ (Functor.sum F H).map f ≫
      (fun X =>
          match X with
          | inl X => app α X
          | inr X => app β X)
        (inl Y) =
    (fun X =>
          match X with
          | inl X => app α X
          | inr X => app β X)
        (inl X) ≫
      (Functor.sum G I).map f
[PROOFSTEP]
aesop_cat_nonterminal
[GOAL]
case inl.inl
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₁
inst_1 : Category.{v₁, u₁} B
C : Type u₁
inst_2 : Category.{v₁, u₁} C
D : Type u₁
inst_3 : Category.{v₁, u₁} D
F G : A ⥤ B
H I : C ⥤ D
α : F ⟶ G
β : H ⟶ I
X Y : A
f : inl X ⟶ inl Y
val val_1 : A
f_1 : inl val ⟶ inl val_1
⊢ F.map f ≫ app α Y = app α X ≫ G.map f
[PROOFSTEP]
erw [α.naturality]
[GOAL]
case inl.inr
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₁
inst_1 : Category.{v₁, u₁} B
C : Type u₁
inst_2 : Category.{v₁, u₁} C
D : Type u₁
inst_3 : Category.{v₁, u₁} D
F G : A ⥤ B
H I : C ⥤ D
α : F ⟶ G
β : H ⟶ I
X Y : A
f : inl X ⟶ inl Y
val : A
val_1 : C
f_1 : inl val ⟶ inr val_1
⊢ F.map f ≫ app α Y = app α X ≫ G.map f
[PROOFSTEP]
erw [α.naturality]
[GOAL]
case inr.inl
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₁
inst_1 : Category.{v₁, u₁} B
C : Type u₁
inst_2 : Category.{v₁, u₁} C
D : Type u₁
inst_3 : Category.{v₁, u₁} D
F G : A ⥤ B
H I : C ⥤ D
α : F ⟶ G
β : H ⟶ I
X Y : A
f : inl X ⟶ inl Y
val : C
val_1 : A
f_1 : inr val ⟶ inl val_1
⊢ F.map f ≫ app α Y = app α X ≫ G.map f
[PROOFSTEP]
erw [α.naturality]
[GOAL]
case inr.inr
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₁
inst_1 : Category.{v₁, u₁} B
C : Type u₁
inst_2 : Category.{v₁, u₁} C
D : Type u₁
inst_3 : Category.{v₁, u₁} D
F G : A ⥤ B
H I : C ⥤ D
α : F ⟶ G
β : H ⟶ I
X Y : A
f : inl X ⟶ inl Y
val val_1 : C
f_1 : inr val ⟶ inr val_1
⊢ F.map f ≫ app α Y = app α X ≫ G.map f
[PROOFSTEP]
erw [α.naturality]
[GOAL]
case inl.inl
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₁
inst_1 : Category.{v₁, u₁} B
C : Type u₁
inst_2 : Category.{v₁, u₁} C
D : Type u₁
inst_3 : Category.{v₁, u₁} D
F G : A ⥤ B
H I : C ⥤ D
α : F ⟶ G
β : H ⟶ I
X Y : A
f : inl X ⟶ inl Y
val val_1 : A
f_1 : inl val ⟶ inl val_1
⊢ app α X ≫ G.map f = app α X ≫ G.map f
[PROOFSTEP]
rfl
[GOAL]
case inl.inr
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₁
inst_1 : Category.{v₁, u₁} B
C : Type u₁
inst_2 : Category.{v₁, u₁} C
D : Type u₁
inst_3 : Category.{v₁, u₁} D
F G : A ⥤ B
H I : C ⥤ D
α : F ⟶ G
β : H ⟶ I
X Y : A
f : inl X ⟶ inl Y
val : A
val_1 : C
f_1 : inl val ⟶ inr val_1
⊢ app α X ≫ G.map f = app α X ≫ G.map f
[PROOFSTEP]
rfl
[GOAL]
case inr.inl
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₁
inst_1 : Category.{v₁, u₁} B
C : Type u₁
inst_2 : Category.{v₁, u₁} C
D : Type u₁
inst_3 : Category.{v₁, u₁} D
F G : A ⥤ B
H I : C ⥤ D
α : F ⟶ G
β : H ⟶ I
X Y : A
f : inl X ⟶ inl Y
val : C
val_1 : A
f_1 : inr val ⟶ inl val_1
⊢ app α X ≫ G.map f = app α X ≫ G.map f
[PROOFSTEP]
rfl
[GOAL]
case inr.inr
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₁
inst_1 : Category.{v₁, u₁} B
C : Type u₁
inst_2 : Category.{v₁, u₁} C
D : Type u₁
inst_3 : Category.{v₁, u₁} D
F G : A ⥤ B
H I : C ⥤ D
α : F ⟶ G
β : H ⟶ I
X Y : A
f : inl X ⟶ inl Y
val val_1 : C
f_1 : inr val ⟶ inr val_1
⊢ app α X ≫ G.map f = app α X ≫ G.map f
[PROOFSTEP]
rfl
[GOAL]
A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₁
inst✝² : Category.{v₁, u₁} B
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F G : A ⥤ B
H I : C ⥤ D
α : F ⟶ G
β : H ⟶ I
X✝ Y✝ : A ⊕ C
f✝ : X✝ ⟶ Y✝
X Y : C
f : inr X ⟶ inr Y
⊢ (Functor.sum F H).map f ≫
      (fun X =>
          match X with
          | inl X => app α X
          | inr X => app β X)
        (inr Y) =
    (fun X =>
          match X with
          | inl X => app α X
          | inr X => app β X)
        (inr X) ≫
      (Functor.sum G I).map f
[PROOFSTEP]
aesop_cat_nonterminal
[GOAL]
case inl.inl
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₁
inst_1 : Category.{v₁, u₁} B
C : Type u₁
inst_2 : Category.{v₁, u₁} C
D : Type u₁
inst_3 : Category.{v₁, u₁} D
F G : A ⥤ B
H I : C ⥤ D
α : F ⟶ G
β : H ⟶ I
X Y : C
f : inr X ⟶ inr Y
val val_1 : A
f_1 : inl val ⟶ inl val_1
⊢ H.map f ≫ app β Y = app β X ≫ I.map f
[PROOFSTEP]
erw [β.naturality]
[GOAL]
case inl.inr
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₁
inst_1 : Category.{v₁, u₁} B
C : Type u₁
inst_2 : Category.{v₁, u₁} C
D : Type u₁
inst_3 : Category.{v₁, u₁} D
F G : A ⥤ B
H I : C ⥤ D
α : F ⟶ G
β : H ⟶ I
X Y : C
f : inr X ⟶ inr Y
val : A
val_1 : C
f_1 : inl val ⟶ inr val_1
⊢ H.map f ≫ app β Y = app β X ≫ I.map f
[PROOFSTEP]
erw [β.naturality]
[GOAL]
case inr.inl
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₁
inst_1 : Category.{v₁, u₁} B
C : Type u₁
inst_2 : Category.{v₁, u₁} C
D : Type u₁
inst_3 : Category.{v₁, u₁} D
F G : A ⥤ B
H I : C ⥤ D
α : F ⟶ G
β : H ⟶ I
X Y : C
f : inr X ⟶ inr Y
val : C
val_1 : A
f_1 : inr val ⟶ inl val_1
⊢ H.map f ≫ app β Y = app β X ≫ I.map f
[PROOFSTEP]
erw [β.naturality]
[GOAL]
case inr.inr
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₁
inst_1 : Category.{v₁, u₁} B
C : Type u₁
inst_2 : Category.{v₁, u₁} C
D : Type u₁
inst_3 : Category.{v₁, u₁} D
F G : A ⥤ B
H I : C ⥤ D
α : F ⟶ G
β : H ⟶ I
X Y : C
f : inr X ⟶ inr Y
val val_1 : C
f_1 : inr val ⟶ inr val_1
⊢ H.map f ≫ app β Y = app β X ≫ I.map f
[PROOFSTEP]
erw [β.naturality]
[GOAL]
case inl.inl
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₁
inst_1 : Category.{v₁, u₁} B
C : Type u₁
inst_2 : Category.{v₁, u₁} C
D : Type u₁
inst_3 : Category.{v₁, u₁} D
F G : A ⥤ B
H I : C ⥤ D
α : F ⟶ G
β : H ⟶ I
X Y : C
f : inr X ⟶ inr Y
val val_1 : A
f_1 : inl val ⟶ inl val_1
⊢ app β X ≫ I.map f = app β X ≫ I.map f
[PROOFSTEP]
rfl
[GOAL]
case inl.inr
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₁
inst_1 : Category.{v₁, u₁} B
C : Type u₁
inst_2 : Category.{v₁, u₁} C
D : Type u₁
inst_3 : Category.{v₁, u₁} D
F G : A ⥤ B
H I : C ⥤ D
α : F ⟶ G
β : H ⟶ I
X Y : C
f : inr X ⟶ inr Y
val : A
val_1 : C
f_1 : inl val ⟶ inr val_1
⊢ app β X ≫ I.map f = app β X ≫ I.map f
[PROOFSTEP]
rfl
[GOAL]
case inr.inl
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₁
inst_1 : Category.{v₁, u₁} B
C : Type u₁
inst_2 : Category.{v₁, u₁} C
D : Type u₁
inst_3 : Category.{v₁, u₁} D
F G : A ⥤ B
H I : C ⥤ D
α : F ⟶ G
β : H ⟶ I
X Y : C
f : inr X ⟶ inr Y
val : C
val_1 : A
f_1 : inr val ⟶ inl val_1
⊢ app β X ≫ I.map f = app β X ≫ I.map f
[PROOFSTEP]
rfl
[GOAL]
case inr.inr
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₁
inst_1 : Category.{v₁, u₁} B
C : Type u₁
inst_2 : Category.{v₁, u₁} C
D : Type u₁
inst_3 : Category.{v₁, u₁} D
F G : A ⥤ B
H I : C ⥤ D
α : F ⟶ G
β : H ⟶ I
X Y : C
f : inr X ⟶ inr Y
val val_1 : C
f_1 : inr val ⟶ inr val_1
⊢ app β X ≫ I.map f = app β X ≫ I.map f
[PROOFSTEP]
rfl


[GOAL]
ι α : Type v
U : ι → α
inst✝ : CompleteLattice α
s : Cocone (diagram U)
⊢ (cocone U).pt ≤ s.pt
[PROOFSTEP]
apply CompleteSemilatticeSup.sSup_le
[GOAL]
case a
ι α : Type v
U : ι → α
inst✝ : CompleteLattice α
s : Cocone (diagram U)
⊢ ∀ (b : α), b ∈ Set.range U → b ≤ s.pt
[PROOFSTEP]
rintro _ ⟨j, rfl⟩
[GOAL]
case a.intro
ι α : Type v
U : ι → α
inst✝ : CompleteLattice α
s : Cocone (diagram U)
j : ι
⊢ U j ≤ s.pt
[PROOFSTEP]
exact (s.ι.app (single j)).le


[GOAL]
C : Type ?u.30361
inst✝ : Category.{?u.30362, ?u.30361} C
X Y : C
f : X ⟶ Y
⊢ 𝟙 X ≫ f = f
[PROOFSTEP]
simp
[GOAL]
C : Type ?u.30529
inst✝ : Category.{?u.30530, ?u.30529} C
X Y : C
f : X ⟶ Y
⊢ f ≫ 𝟙 Y = f
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f g : X ⟶ Y
w : f = g
h : Y ⟶ Z
⊢ f ≫ h = g ≫ h
[PROOFSTEP]
rw [w]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g h : Y ⟶ Z
w : g = h
⊢ f ≫ g = f ≫ h
[PROOFSTEP]
rw [w]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f g : X ⟶ Y
w : ∀ {Z : C} (h : Y ⟶ Z), f ≫ h = g ≫ h
⊢ f = g
[PROOFSTEP]
convert w (𝟙 Y)
[GOAL]
case h.e'_2
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f g : X ⟶ Y
w : ∀ {Z : C} (h : Y ⟶ Z), f ≫ h = g ≫ h
⊢ f = f ≫ 𝟙 Y
[PROOFSTEP]
aesop
[GOAL]
case h.e'_3
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f g : X ⟶ Y
w : ∀ {Z : C} (h : Y ⟶ Z), f ≫ h = g ≫ h
⊢ g = g ≫ 𝟙 Y
[PROOFSTEP]
aesop
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f g : Y ⟶ Z
w : ∀ {X : C} (h : X ⟶ Y), h ≫ f = h ≫ g
⊢ f = g
[PROOFSTEP]
convert w (𝟙 Y)
[GOAL]
case h.e'_2
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f g : Y ⟶ Z
w : ∀ {X : C} (h : X ⟶ Y), h ≫ f = h ≫ g
⊢ f = 𝟙 Y ≫ f
[PROOFSTEP]
aesop
[GOAL]
case h.e'_3
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f g : Y ⟶ Z
w : ∀ {X : C} (h : X ⟶ Y), h ≫ f = h ≫ g
⊢ g = 𝟙 Y ≫ g
[PROOFSTEP]
aesop
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y Z✝ : C
f g : X ⟶ Y
w : (fun {Z} h => f ≫ h) = fun {Z} h => g ≫ h
Z : C
h : Y ⟶ Z
⊢ f ≫ h = g ≫ h
[PROOFSTEP]
convert congr_fun (congr_fun w Z) h
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ Y Z : C
f g : Y ⟶ Z
w : (fun {X} h => h ≫ f) = fun {X} h => h ≫ g
X : C
h : X ⟶ Y
⊢ h ≫ f = h ≫ g
[PROOFSTEP]
convert congr_fun (congr_fun w X) h
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : X ⟶ X
w : ∀ {Y : C} (g : X ⟶ Y), f ≫ g = g
⊢ f = 𝟙 X
[PROOFSTEP]
convert w (𝟙 X)
[GOAL]
case h.e'_2
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : X ⟶ X
w : ∀ {Y : C} (g : X ⟶ Y), f ≫ g = g
⊢ f = f ≫ 𝟙 X
[PROOFSTEP]
aesop
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : X ⟶ X
w : ∀ {Y : C} (g : Y ⟶ X), g ≫ f = g
⊢ f = 𝟙 X
[PROOFSTEP]
convert w (𝟙 X)
[GOAL]
case h.e'_2
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : X ⟶ X
w : ∀ {Y : C} (g : Y ⟶ X), g ≫ f = g
⊢ f = 𝟙 X ≫ f
[PROOFSTEP]
aesop
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ Z✝ : C
P : Prop
inst✝ : Decidable P
X Y Z : C
f : X ⟶ Y
g g' : Y ⟶ Z
⊢ (f ≫ if P then g else g') = if P then f ≫ g else f ≫ g'
[PROOFSTEP]
aesop
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ Z✝ : C
P : Prop
inst✝ : Decidable P
X Y Z : C
f f' : X ⟶ Y
g : Y ⟶ Z
⊢ (if P then f else f') ≫ g = if P then f ≫ g else f' ≫ g
[PROOFSTEP]
aesop
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ Z✝ : C
P : Prop
inst✝ : Decidable P
X Y Z : C
f : X ⟶ Y
g : P → (Y ⟶ Z)
g' : ¬P → (Y ⟶ Z)
⊢ (f ≫ if h : P then g h else g' h) = if h : P then f ≫ g h else f ≫ g' h
[PROOFSTEP]
aesop
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ Z✝ : C
P : Prop
inst✝ : Decidable P
X Y Z : C
f : P → (X ⟶ Y)
f' : ¬P → (X ⟶ Y)
g : Y ⟶ Z
⊢ (if h : P then f h else f' h) ≫ g = if h : P then f h ≫ g else f' h ≫ g
[PROOFSTEP]
aesop
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ Y Z X Z✝ : C
g h : X ⟶ Z✝
w : 𝟙 X ≫ g = 𝟙 X ≫ h
⊢ g = h
[PROOFSTEP]
aesop
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ Y Z X Z✝ : C
g h : Z✝ ⟶ X
w : g ≫ 𝟙 X = h ≫ 𝟙 X
⊢ g = h
[PROOFSTEP]
aesop
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
inst✝ : Epi f
h : Y ⟶ Y
⊢ f ≫ h = f ↔ h = 𝟙 Y
[PROOFSTEP]
convert cancel_epi f
[GOAL]
case h.e'_1.h.e'_3.h
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
inst✝ : Epi f
h : Y ⟶ Y
⊢ f = f ≫ 𝟙 Y
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
inst✝ : Mono f
g : X ⟶ X
⊢ g ≫ f = f ↔ g = 𝟙 X
[PROOFSTEP]
convert cancel_mono f
[GOAL]
case h.e'_1.h.e'_3.h
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
inst✝ : Mono f
g : X ⟶ X
⊢ f = 𝟙 X ≫ f
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ Z✝ X Y Z : C
f : X ⟶ Y
inst✝¹ : Epi f
g : Y ⟶ Z
inst✝ : Epi g
⊢ Epi (f ≫ g)
[PROOFSTEP]
constructor
[GOAL]
case left_cancellation
C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ Z✝ X Y Z : C
f : X ⟶ Y
inst✝¹ : Epi f
g : Y ⟶ Z
inst✝ : Epi g
⊢ ∀ {Z_1 : C} (g_1 h : Z ⟶ Z_1), (f ≫ g) ≫ g_1 = (f ≫ g) ≫ h → g_1 = h
[PROOFSTEP]
intro Z a b w
[GOAL]
case left_cancellation
C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ Z✝¹ X Y Z✝ : C
f : X ⟶ Y
inst✝¹ : Epi f
g : Y ⟶ Z✝
inst✝ : Epi g
Z : C
a b : Z✝ ⟶ Z
w : (f ≫ g) ≫ a = (f ≫ g) ≫ b
⊢ a = b
[PROOFSTEP]
apply (cancel_epi g).1
[GOAL]
case left_cancellation
C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ Z✝¹ X Y Z✝ : C
f : X ⟶ Y
inst✝¹ : Epi f
g : Y ⟶ Z✝
inst✝ : Epi g
Z : C
a b : Z✝ ⟶ Z
w : (f ≫ g) ≫ a = (f ≫ g) ≫ b
⊢ g ≫ a = g ≫ b
[PROOFSTEP]
apply (cancel_epi f).1
[GOAL]
case left_cancellation
C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ Z✝¹ X Y Z✝ : C
f : X ⟶ Y
inst✝¹ : Epi f
g : Y ⟶ Z✝
inst✝ : Epi g
Z : C
a b : Z✝ ⟶ Z
w : (f ≫ g) ≫ a = (f ≫ g) ≫ b
⊢ f ≫ g ≫ a = f ≫ g ≫ b
[PROOFSTEP]
simpa using w
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ Z✝ X Y Z : C
f : X ⟶ Y
inst✝¹ : Mono f
g : Y ⟶ Z
inst✝ : Mono g
⊢ Mono (f ≫ g)
[PROOFSTEP]
constructor
[GOAL]
case right_cancellation
C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ Z✝ X Y Z : C
f : X ⟶ Y
inst✝¹ : Mono f
g : Y ⟶ Z
inst✝ : Mono g
⊢ ∀ {Z_1 : C} (g_1 h : Z_1 ⟶ X), g_1 ≫ f ≫ g = h ≫ f ≫ g → g_1 = h
[PROOFSTEP]
intro Z a b w
[GOAL]
case right_cancellation
C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ Z✝¹ X Y Z✝ : C
f : X ⟶ Y
inst✝¹ : Mono f
g : Y ⟶ Z✝
inst✝ : Mono g
Z : C
a b : Z ⟶ X
w : a ≫ f ≫ g = b ≫ f ≫ g
⊢ a = b
[PROOFSTEP]
apply (cancel_mono f).1
[GOAL]
case right_cancellation
C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ Z✝¹ X Y Z✝ : C
f : X ⟶ Y
inst✝¹ : Mono f
g : Y ⟶ Z✝
inst✝ : Mono g
Z : C
a b : Z ⟶ X
w : a ≫ f ≫ g = b ≫ f ≫ g
⊢ a ≫ f = b ≫ f
[PROOFSTEP]
apply (cancel_mono g).1
[GOAL]
case right_cancellation
C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ Z✝¹ X Y Z✝ : C
f : X ⟶ Y
inst✝¹ : Mono f
g : Y ⟶ Z✝
inst✝ : Mono g
Z : C
a b : Z ⟶ X
w : a ≫ f ≫ g = b ≫ f ≫ g
⊢ (a ≫ f) ≫ g = (b ≫ f) ≫ g
[PROOFSTEP]
simpa using w
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ Z✝ X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : Mono (f ≫ g)
⊢ Mono f
[PROOFSTEP]
constructor
[GOAL]
case right_cancellation
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ Z✝ X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : Mono (f ≫ g)
⊢ ∀ {Z : C} (g h : Z ⟶ X), g ≫ f = h ≫ f → g = h
[PROOFSTEP]
intro Z a b w
[GOAL]
case right_cancellation
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ Z✝¹ X Y Z✝ : C
f : X ⟶ Y
g : Y ⟶ Z✝
inst✝ : Mono (f ≫ g)
Z : C
a b : Z ⟶ X
w : a ≫ f = b ≫ f
⊢ a = b
[PROOFSTEP]
replace w := congr_arg (fun k => k ≫ g) w
[GOAL]
case right_cancellation
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ Z✝¹ X Y Z✝ : C
f : X ⟶ Y
g : Y ⟶ Z✝
inst✝ : Mono (f ≫ g)
Z : C
a b : Z ⟶ X
w : (fun k => k ≫ g) (a ≫ f) = (fun k => k ≫ g) (b ≫ f)
⊢ a = b
[PROOFSTEP]
dsimp at w
[GOAL]
case right_cancellation
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ Z✝¹ X Y Z✝ : C
f : X ⟶ Y
g : Y ⟶ Z✝
inst✝ : Mono (f ≫ g)
Z : C
a b : Z ⟶ X
w : (a ≫ f) ≫ g = (b ≫ f) ≫ g
⊢ a = b
[PROOFSTEP]
rw [Category.assoc, Category.assoc] at w
[GOAL]
case right_cancellation
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ Z✝¹ X Y Z✝ : C
f : X ⟶ Y
g : Y ⟶ Z✝
inst✝ : Mono (f ≫ g)
Z : C
a b : Z ⟶ X
w : a ≫ f ≫ g = b ≫ f ≫ g
⊢ a = b
[PROOFSTEP]
exact (cancel_mono _).1 w
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ Z✝ X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h : X ⟶ Z
inst✝ : Mono h
w : f ≫ g = h
⊢ Mono f
[PROOFSTEP]
subst h
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ Z✝ X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : Mono (f ≫ g)
⊢ Mono f
[PROOFSTEP]
exact mono_of_mono f g
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ Z✝ X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : Epi (f ≫ g)
⊢ Epi g
[PROOFSTEP]
constructor
[GOAL]
case left_cancellation
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ Z✝ X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : Epi (f ≫ g)
⊢ ∀ {Z_1 : C} (g_1 h : Z ⟶ Z_1), g ≫ g_1 = g ≫ h → g_1 = h
[PROOFSTEP]
intro Z a b w
[GOAL]
case left_cancellation
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ Z✝¹ X Y Z✝ : C
f : X ⟶ Y
g : Y ⟶ Z✝
inst✝ : Epi (f ≫ g)
Z : C
a b : Z✝ ⟶ Z
w : g ≫ a = g ≫ b
⊢ a = b
[PROOFSTEP]
replace w := congr_arg (fun k => f ≫ k) w
[GOAL]
case left_cancellation
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ Z✝¹ X Y Z✝ : C
f : X ⟶ Y
g : Y ⟶ Z✝
inst✝ : Epi (f ≫ g)
Z : C
a b : Z✝ ⟶ Z
w : (fun k => f ≫ k) (g ≫ a) = (fun k => f ≫ k) (g ≫ b)
⊢ a = b
[PROOFSTEP]
dsimp at w
[GOAL]
case left_cancellation
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ Z✝¹ X Y Z✝ : C
f : X ⟶ Y
g : Y ⟶ Z✝
inst✝ : Epi (f ≫ g)
Z : C
a b : Z✝ ⟶ Z
w : f ≫ g ≫ a = f ≫ g ≫ b
⊢ a = b
[PROOFSTEP]
rw [← Category.assoc, ← Category.assoc] at w
[GOAL]
case left_cancellation
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ Z✝¹ X Y Z✝ : C
f : X ⟶ Y
g : Y ⟶ Z✝
inst✝ : Epi (f ≫ g)
Z : C
a b : Z✝ ⟶ Z
w : (f ≫ g) ≫ a = (f ≫ g) ≫ b
⊢ a = b
[PROOFSTEP]
exact (cancel_epi _).1 w
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ Z✝ X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h : X ⟶ Z
inst✝ : Epi h
w : f ≫ g = h
⊢ Epi g
[PROOFSTEP]
subst h
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ Z✝ X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : Epi (f ≫ g)
⊢ Epi g
[PROOFSTEP]
exact epi_of_epi f g
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u
inst✝ : SmallCategory D
⊢ LargeCategory (ULift D)
[PROOFSTEP]
infer_instance