-- 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₁
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ᵒᵖ),
    Nonempty (op ((Sieve.ofArrows (fun x => X) fun x => π).arrows.categoryMk π ⋯) ⟶ Z)

Tactic:
intro ⟨Z⟩

Result:
case h₁
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
⊢ Nonempty (op ((Sieve.ofArrows (fun x => X) fun x => π).arrows.categoryMk π ⋯) ⟶ op Z)

Proof state:
case h₂
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 ⋯
⊢ ∃ a, op i = (Over.homMk c.fst ⋯).op ≫ a ∧ op j = (Over.homMk c.snd ⋯).op ≫ a

Tactic:
refine ⟨Quiver.Hom.op (Over.homMk ij (by simpa [ij] using i.w)), ?_, ?_⟩

Result:
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

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 ⋯
⊢ ij ≫ ((Sieve.ofArrows (fun x => X) fun x => π).arrows.categoryMk (c.fst ≫ π) ⋯).obj.hom = Z.obj.hom

Tactic:
simpa [ij] using i.w

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
⊢ (parallelPair (Over.homMk c.fst ⋯).op (Over.homMk c.snd ⋯).op).Initial

Tactic:
apply Limits.parallelPair_initial_mk

Result:
case h₁
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ᵒᵖ),
    Nonempty (op ((Sieve.ofArrows (fun x => X) fun x => π).arrows.categoryMk π ⋯) ⟶ Z)

case h₂
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 : op ((Sieve.ofArrows (fun x => X) fun x => π).arrows.categoryMk π ⋯) ⟶ Z),
    ∃ a, i = (Over.homMk c.fst ⋯).op ≫ a ∧ j = (Over.homMk c.snd ⋯).op ≫ a

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 π ⋯))
⊢ i.left ≫ π = j.left ≫ π

Tactic:
erw [i.w, j.w]

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 π ⋯))
⊢ (unop (op Z)).obj.hom ≫ (fromPUnit B).map i.right = (unop (op Z)).obj.hom ≫ (fromPUnit B).map j.right

Proof state:
case h₂
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 : op ((Sieve.ofArrows (fun x => X) fun x => π).arrows.categoryMk π ⋯) ⟶ Z),
    ∃ a, i = (Over.homMk c.fst ⋯).op ≫ a ∧ j = (Over.homMk c.snd ⋯).op ≫ a

Tactic:
intro ⟨Z⟩ ⟨i⟩ ⟨j⟩

Result:
case h₂
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 π ⋯))
⊢ ∃ a, op i = (Over.homMk c.fst ⋯).op ≫ a ∧ op j = (Over.homMk c.snd ⋯).op ≫ a

Proof state:
case h₂
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 π ⋯))
⊢ ∃ a, op i = (Over.homMk c.fst ⋯).op ≫ a ∧ op j = (Over.homMk c.snd ⋯).op ≫ a

Tactic:
let ij := PullbackCone.IsLimit.lift hc i.left j.left (by erw [i.w, j.w]; rfl)

Result:
case h₂
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 ⋯
⊢ ∃ a, op i = (Over.homMk c.fst ⋯).op ≫ a ∧ op j = (Over.homMk c.snd ⋯).op ≫ a

Proof state:
case h₁
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
⊢ Nonempty (op ((Sieve.ofArrows (fun x => X) fun x => π).arrows.categoryMk π ⋯) ⟶ op Z)

Tactic:
obtain ⟨_, f, g, ⟨⟩, hh⟩ := Z.property

Result:
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
⊢ Nonempty (op ((Sieve.ofArrows (fun x => X) fun x => π).arrows.categoryMk π ⋯) ⟶ op Z)