[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
