-- Mathlib/CategoryTheory/Sites/Sieves.lean
theorem ofArrows_pullback [HasPullbacks C] {ι : Type*} (Z : ι → C) (g : ∀ i : ι, Z i ⟶ X) :
    (ofArrows (fun i => pullback (g i) f) fun _ => pullback.snd _ _) =
      pullbackArrows f (ofArrows Z g)

Proof state:
case h.h.mpr.mk.mk
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y✝¹ : C
f : Y✝¹ ⟶ X
inst✝ : HasPullbacks C
ι : Type u_1
Z : ι → C
g : (i : ι) → Z i ⟶ X
Y✝ Y : C
i✝ : ι
⊢ pullback.snd (g i✝) f ∈ ofArrows (fun i => pullback (g i) f) fun x => pullback.snd (g x) f

Tactic:
apply ofArrows.mk

Result:
no goals

Proof state:
case h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
f : Y ⟶ X
inst✝ : HasPullbacks C
ι : Type u_1
Z : ι → C
g : (i : ι) → Z i ⟶ X
T : C
⊢ (ofArrows (fun i => pullback (g i) f) fun x => pullback.snd (g x) f) = pullbackArrows f (ofArrows Z g)

Tactic:
ext h

Result:
case h.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
f : Y ⟶ X
inst✝ : HasPullbacks C
ι : Type u_1
Z : ι → C
g : (i : ι) → Z i ⟶ X
T : C
h : T ⟶ Y
⊢ (h ∈ ofArrows (fun i => pullback (g i) f) fun x => pullback.snd (g x) f) ↔ h ∈ pullbackArrows f (ofArrows Z g)

Proof state:
case h.h.mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
f : Y ⟶ X
inst✝ : HasPullbacks C
ι : Type u_1
Z : ι → C
g : (i : ι) → Z i ⟶ X
T : C
h : T ⟶ Y
⊢ (h ∈ ofArrows (fun i => pullback (g i) f) fun x => pullback.snd (g x) f) → h ∈ pullbackArrows f (ofArrows Z g)

Tactic:
rintro ⟨hk⟩

Result:
case h.h.mp.mk
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y✝ : C
f : Y✝ ⟶ X
inst✝ : HasPullbacks C
ι : Type u_1
Z : ι → C
g : (i : ι) → Z i ⟶ X
Y : C
hk : ι
⊢ pullback.snd (g hk) f ∈ pullbackArrows f (ofArrows Z g)

Proof state:
case h.h.mp.mk
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y✝ : C
f : Y✝ ⟶ X
inst✝ : HasPullbacks C
ι : Type u_1
Z : ι → C
g : (i : ι) → Z i ⟶ X
Y : C
hk : ι
⊢ pullback.snd (g hk) f ∈ pullbackArrows f (ofArrows Z g)

Tactic:
exact pullbackArrows.mk _ _ (ofArrows.mk hk)

Result:
no goals

Proof state:
case h.h.mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
f : Y ⟶ X
inst✝ : HasPullbacks C
ι : Type u_1
Z : ι → C
g : (i : ι) → Z i ⟶ X
T : C
h : T ⟶ Y
⊢ h ∈ pullbackArrows f (ofArrows Z g) → h ∈ ofArrows (fun i => pullback (g i) f) fun x => pullback.snd (g x) f

Tactic:
rintro ⟨W, k, ⟨_⟩⟩

Result:
case h.h.mpr.mk.mk
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y✝¹ : C
f : Y✝¹ ⟶ X
inst✝ : HasPullbacks C
ι : Type u_1
Z : ι → C
g : (i : ι) → Z i ⟶ X
Y✝ Y : C
i✝ : ι
⊢ pullback.snd (g i✝) f ∈ ofArrows (fun i => pullback (g i) f) fun x => pullback.snd (g x) f

Proof state:
case h.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
f : Y ⟶ X
inst✝ : HasPullbacks C
ι : Type u_1
Z : ι → C
g : (i : ι) → Z i ⟶ X
T : C
h : T ⟶ Y
⊢ (h ∈ ofArrows (fun i => pullback (g i) f) fun x => pullback.snd (g x) f) ↔ h ∈ pullbackArrows f (ofArrows Z g)

Tactic:
constructor

Result:
case h.h.mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
f : Y ⟶ X
inst✝ : HasPullbacks C
ι : Type u_1
Z : ι → C
g : (i : ι) → Z i ⟶ X
T : C
h : T ⟶ Y
⊢ (h ∈ ofArrows (fun i => pullback (g i) f) fun x => pullback.snd (g x) f) → h ∈ pullbackArrows f (ofArrows Z g)

case h.h.mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
f : Y ⟶ X
inst✝ : HasPullbacks C
ι : Type u_1
Z : ι → C
g : (i : ι) → Z i ⟶ X
T : C
h : T ⟶ Y
⊢ h ∈ pullbackArrows f (ofArrows Z g) → h ∈ ofArrows (fun i => pullback (g i) f) fun x => pullback.snd (g x) f

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
f : Y ⟶ X
inst✝ : HasPullbacks C
ι : Type u_1
Z : ι → C
g : (i : ι) → Z i ⟶ X
⊢ (ofArrows (fun i => pullback (g i) f) fun x => pullback.snd (g x) f) = pullbackArrows f (ofArrows Z g)

Tactic:
funext T

Result:
case h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
f : Y ⟶ X
inst✝ : HasPullbacks C
ι : Type u_1
Z : ι → C
g : (i : ι) → Z i ⟶ X
T : C
⊢ (ofArrows (fun i => pullback (g i) f) fun x => pullback.snd (g x) f) = pullbackArrows f (ofArrows Z g)