-- Mathlib/CategoryTheory/Subobject/Basic.lean
theorem map_pullback [HasPullbacks C] {X Y Z W : C} {f : X ⟶ Y} {g : X ⟶ Z} {h : Y ⟶ W} {k : Z ⟶ W}
    [Mono h] [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)

Proof state:
case h.a.g.refine_1
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
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 k ≫ ((MonoOver.forget Y).obj a).hom) ≫ h =
    pullback.snd ((MonoOver.forget W).obj ((MonoOver.map h).obj a)).hom k ≫ k

Tactic:
rw [← pullback.condition, assoc]

Result:
case h.a.g.refine_1
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
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 k ≫ ((MonoOver.forget Y).obj a).hom ≫ h =
    pullback.fst ((MonoOver.forget W).obj ((MonoOver.map h).obj a)).hom k ≫
      ((MonoOver.forget W).obj ((MonoOver.map h).obj a)).hom

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
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)

Tactic:
revert p

Result:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
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)

Proof state:
case h
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
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))

Tactic:
apply Quotient.sound

Result:
case h.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
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)

Proof state:
case h.a.f
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
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 f ≫ ((MonoOver.forget W).obj ((MonoOver.map h).obj a)).hom =
    ((MonoOver.map g).obj ((MonoOver.pullback f).obj a)).arrow ≫ k

Tactic:
change _ ≫ a.arrow ≫ h = (pullback.snd _ _ ≫ g) ≫ _

Result:
case h.a.f
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
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 f ≫ a.arrow ≫ h =
    (pullback.snd ((MonoOver.forget Y).obj a).hom f ≫ g) ≫ k

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
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)

Tactic:
apply Quotient.ind'

Result:
case h
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
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))

Proof state:
case h.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
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)

Tactic:
apply ThinSkeleton.equiv_of_both_ways

Result:
case h.a.f
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
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)

case h.a.g
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
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)

Proof state:
case h.a.g.refine_1
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
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 k ≫ ((MonoOver.forget Y).obj a).hom ≫ h =
    pullback.fst ((MonoOver.forget W).obj ((MonoOver.map h).obj a)).hom k ≫
      ((MonoOver.forget W).obj ((MonoOver.map h).obj a)).hom

Tactic:
rfl

Result:
no goals

Proof state:
case h.a.f
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
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)

Tactic:
refine MonoOver.homMk (pullback.lift (pullback.fst _ _) _ ?_) (pullback.lift_snd _ _ _)

Result:
case h.a.f
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
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 f ≫ ((MonoOver.forget W).obj ((MonoOver.map h).obj a)).hom =
    ((MonoOver.map g).obj ((MonoOver.pullback f).obj a)).arrow ≫ k

Proof state:
case h.a.g.refine_2
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
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 (a.arrow ≫ h) k)
        (PullbackCone.IsLimit.lift t (pullback.fst (a.arrow ≫ h) k ≫ a.arrow) (pullback.snd (a.arrow ≫ h) k) ⋯) ⋯ ≫
      pullback.snd a.arrow f ≫ g =
    pullback.snd (a.arrow ≫ h) k

Tactic:
rw [pullback.lift_snd_assoc]

Result:
case h.a.g.refine_2
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
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 (a.arrow ≫ h) k ≫ a.arrow) (pullback.snd (a.arrow ≫ h) k) ⋯ ≫ g =
    pullback.snd (a.arrow ≫ h) k