-- Mathlib/CategoryTheory/Sites/Coherent/RegularSheaves.lean
theorem parallelPair_pullback_initial {X B : C} (π : X ⟶ B)
    (c : PullbackCone π π) (hc : IsLimit c) :
    (parallelPair (C := (Sieve.ofArrows (fun (_ : Unit) => X) (fun _ => π)).arrows.categoryᵒᵖ)
    (Y := op ((Presieve.categoryMk _ (c.fst ≫ π) ⟨_, c.fst, π, ofArrows.mk (), rfl⟩)))
    (X := op ((Presieve.categoryMk _ π (Sieve.ofArrows_mk _ _ Unit.unit))))
    (Quiver.Hom.op (Over.homMk c.fst))
    (Quiver.Hom.op (Over.homMk c.snd c.condition.symm))).Initial

Proof state:
case h₂.refine_1
C : Type u_1
inst✝ : Category.{u_4, u_1} C
X B : C
π : X ⟶ B
c : PullbackCone π π
hc : IsLimit c
Z : (Sieve.ofArrows (fun x => X) fun x => π).arrows.category
i j : unop (op Z) ⟶ unop (op ((Sieve.ofArrows (fun x => X) fun x => π).arrows.categoryMk π ⋯))
ij : (unop (op Z)).obj.left ⟶ c.pt := PullbackCone.IsLimit.lift hc i.left j.left ⋯
⊢ op i = (Over.homMk c.fst ⋯).op ≫ (Over.homMk ij ⋯).op

case h₂.refine_2
C : Type u_1
inst✝ : Category.{u_4, u_1} C
X B : C
π : X ⟶ B
c : PullbackCone π π
hc : IsLimit c
Z : (Sieve.ofArrows (fun x => X) fun x => π).arrows.category
i j : unop (op Z) ⟶ unop (op ((Sieve.ofArrows (fun x => X) fun x => π).arrows.categoryMk π ⋯))
ij : (unop (op Z)).obj.left ⟶ c.pt := PullbackCone.IsLimit.lift hc i.left j.left ⋯
⊢ op j = (Over.homMk c.snd ⋯).op ≫ (Over.homMk ij ⋯).op

Tactic:
all_goals congr

Result:
case h₂.refine_1.e_unop
C : Type u_1
inst✝ : Category.{u_4, u_1} C
X B : C
π : X ⟶ B
c : PullbackCone π π
hc : IsLimit c
Z : (Sieve.ofArrows (fun x => X) fun x => π).arrows.category
i j : unop (op Z) ⟶ unop (op ((Sieve.ofArrows (fun x => X) fun x => π).arrows.categoryMk π ⋯))
ij : (unop (op Z)).obj.left ⟶ c.pt := PullbackCone.IsLimit.lift hc i.left j.left ⋯
⊢ i = (Over.homMk ij ⋯).op.unop ≫ (Over.homMk c.fst ⋯).op.unop

case h₂.refine_2.e_unop
C : Type u_1
inst✝ : Category.{u_4, u_1} C
X B : C
π : X ⟶ B
c : PullbackCone π π
hc : IsLimit c
Z : (Sieve.ofArrows (fun x => X) fun x => π).arrows.category
i j : unop (op Z) ⟶ unop (op ((Sieve.ofArrows (fun x => X) fun x => π).arrows.categoryMk π ⋯))
ij : (unop (op Z)).obj.left ⟶ c.pt := PullbackCone.IsLimit.lift hc i.left j.left ⋯
⊢ j = (Over.homMk ij ⋯).op.unop ≫ (Over.homMk c.snd ⋯).op.unop

Proof state:
case h₂.refine_1.e_unop
C : Type u_1
inst✝ : Category.{u_4, u_1} C
X B : C
π : X ⟶ B
c : PullbackCone π π
hc : IsLimit c
Z : (Sieve.ofArrows (fun x => X) fun x => π).arrows.category
i j : unop (op Z) ⟶ unop (op ((Sieve.ofArrows (fun x => X) fun x => π).arrows.categoryMk π ⋯))
ij : (unop (op Z)).obj.left ⟶ c.pt := PullbackCone.IsLimit.lift hc i.left j.left ⋯
⊢ i = (Over.homMk ij ⋯).op.unop ≫ (Over.homMk c.fst ⋯).op.unop

case h₂.refine_2.e_unop
C : Type u_1
inst✝ : Category.{u_4, u_1} C
X B : C
π : X ⟶ B
c : PullbackCone π π
hc : IsLimit c
Z : (Sieve.ofArrows (fun x => X) fun x => π).arrows.category
i j : unop (op Z) ⟶ unop (op ((Sieve.ofArrows (fun x => X) fun x => π).arrows.categoryMk π ⋯))
ij : (unop (op Z)).obj.left ⟶ c.pt := PullbackCone.IsLimit.lift hc i.left j.left ⋯
⊢ j = (Over.homMk ij ⋯).op.unop ≫ (Over.homMk c.snd ⋯).op.unop

Tactic:
all_goals exact Comma.hom_ext _ _ (by erw [Over.comp_left]; simp [ij]) rfl

Result:
no goals

Proof state:
C : Type u_1
inst✝ : Category.{u_4, u_1} C
X B : C
π : X ⟶ B
c : PullbackCone π π
hc : IsLimit c
Z : (Sieve.ofArrows (fun x => X) fun x => π).arrows.category
i j : unop (op Z) ⟶ unop (op ((Sieve.ofArrows (fun x => X) fun x => π).arrows.categoryMk π ⋯))
ij : (unop (op Z)).obj.left ⟶ c.pt := PullbackCone.IsLimit.lift hc i.left j.left ⋯
⊢ j.left = (Over.homMk ij ⋯).op.unop.left ≫ (Over.homMk c.snd ⋯).op.unop.left

Tactic:
simp [ij]

Result:
no goals

Proof state:
case h₂.refine_2
C : Type u_1
inst✝ : Category.{u_4, u_1} C
X B : C
π : X ⟶ B
c : PullbackCone π π
hc : IsLimit c
Z : (Sieve.ofArrows (fun x => X) fun x => π).arrows.category
i j : unop (op Z) ⟶ unop (op ((Sieve.ofArrows (fun x => X) fun x => π).arrows.categoryMk π ⋯))
ij : (unop (op Z)).obj.left ⟶ c.pt := PullbackCone.IsLimit.lift hc i.left j.left ⋯
⊢ op j = (Over.homMk c.snd ⋯).op ≫ (Over.homMk ij ⋯).op

Tactic:
congr

Result:
case h₂.refine_2.e_unop
C : Type u_1
inst✝ : Category.{u_4, u_1} C
X B : C
π : X ⟶ B
c : PullbackCone π π
hc : IsLimit c
Z : (Sieve.ofArrows (fun x => X) fun x => π).arrows.category
i j : unop (op Z) ⟶ unop (op ((Sieve.ofArrows (fun x => X) fun x => π).arrows.categoryMk π ⋯))
ij : (unop (op Z)).obj.left ⟶ c.pt := PullbackCone.IsLimit.lift hc i.left j.left ⋯
⊢ j = (Over.homMk ij ⋯).op.unop ≫ (Over.homMk c.snd ⋯).op.unop

Proof state:
case h₂.refine_2.e_unop
C : Type u_1
inst✝ : Category.{u_4, u_1} C
X B : C
π : X ⟶ B
c : PullbackCone π π
hc : IsLimit c
Z : (Sieve.ofArrows (fun x => X) fun x => π).arrows.category
i j : unop (op Z) ⟶ unop (op ((Sieve.ofArrows (fun x => X) fun x => π).arrows.categoryMk π ⋯))
ij : (unop (op Z)).obj.left ⟶ c.pt := PullbackCone.IsLimit.lift hc i.left j.left ⋯
⊢ j = (Over.homMk ij ⋯).op.unop ≫ (Over.homMk c.snd ⋯).op.unop

Tactic:
exact Comma.hom_ext _ _ (by erw [Over.comp_left]; simp [ij]) rfl

Result:
no goals

Proof state:
case h₁.intro.intro.intro.intro.mk
C : Type u_1
inst✝ : Category.{u_4, u_1} C
X B : C
π : X ⟶ B
c : PullbackCone π π
hc : IsLimit c
Z : (Sieve.ofArrows (fun x => X) fun x => π).arrows.category
Y : C
i✝ : Unit
f : (𝟭 C).obj Z.obj.left ⟶ X
hh : f ≫ π = Z.obj.hom
X' : (ofArrows (fun x => X) fun x =>
    match x with
    | PUnit.unit => π).category :=
  (ofArrows (fun x => X) fun x =>
        match x with
        | PUnit.unit => π).categoryMk
    π ⋯
f' : Z.obj.left ⟶ X'.obj.left := f
⊢ Nonempty (op ((Sieve.ofArrows (fun x => X) fun x => π).arrows.categoryMk π ⋯) ⟶ op Z)

Tactic:
exact ⟨(Over.homMk f').op⟩

Result:
no goals

Proof state:
C : Type u_1
inst✝ : Category.{u_4, u_1} C
X B : C
π : X ⟶ B
c : PullbackCone π π
hc : IsLimit c
Z : (Sieve.ofArrows (fun x => X) fun x => π).arrows.category
i j : unop (op Z) ⟶ unop (op ((Sieve.ofArrows (fun x => X) fun x => π).arrows.categoryMk π ⋯))
ij : (unop (op Z)).obj.left ⟶ c.pt := PullbackCone.IsLimit.lift hc i.left j.left ⋯
⊢ j.left = ((Over.homMk ij ⋯).op.unop ≫ (Over.homMk c.snd ⋯).op.unop).left

Tactic:
erw [Over.comp_left]

Result:
C : Type u_1
inst✝ : Category.{u_4, u_1} C
X B : C
π : X ⟶ B
c : PullbackCone π π
hc : IsLimit c
Z : (Sieve.ofArrows (fun x => X) fun x => π).arrows.category
i j : unop (op Z) ⟶ unop (op ((Sieve.ofArrows (fun x => X) fun x => π).arrows.categoryMk π ⋯))
ij : (unop (op Z)).obj.left ⟶ c.pt := PullbackCone.IsLimit.lift hc i.left j.left ⋯
⊢ j.left = (Over.homMk ij ⋯).op.unop.left ≫ (Over.homMk c.snd ⋯).op.unop.left

Proof state:
C : Type u_1
inst✝ : Category.{u_4, u_1} C
X B : C
π : X ⟶ B
c : PullbackCone π π
hc : IsLimit c
Z : (Sieve.ofArrows (fun x => X) fun x => π).arrows.category
i j : unop (op Z) ⟶ unop (op ((Sieve.ofArrows (fun x => X) fun x => π).arrows.categoryMk π ⋯))
⊢ (unop (op Z)).obj.hom ≫ (fromPUnit B).map i.right = (unop (op Z)).obj.hom ≫ (fromPUnit B).map j.right

Tactic:
rfl

Result:
no goals