-- Mathlib/CategoryTheory/Sites/Sieves.lean
theorem ofArrows_bind {ι : Type*} (Z : ι → C) (g : ∀ i : ι, Z i ⟶ X)
    (j : ∀ ⦃Y⦄ (f : Y ⟶ X), ofArrows Z g f → Type*) (W : ∀ ⦃Y⦄ (f : Y ⟶ X) (H), j f H → C)
    (k : ∀ ⦃Y⦄ (f : Y ⟶ X) (H i), W f H i ⟶ Y) :
    ((ofArrows Z g).bind fun _ f H => ofArrows (W f H) (k f H)) =
      ofArrows (fun i : Σi, j _ (ofArrows.mk i) => W (g i.1) _ i.2) fun ij =>
        k (g ij.1) _ ij.2 ≫ g ij.1

Proof state:
case h.h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
ι : Type u_1
Z : ι → C
g : (i : ι) → Z i ⟶ X
j : ⦃Y : C⦄ → (f : Y ⟶ X) → ofArrows Z g f → Type u_2
W : ⦃Y : C⦄ → (f : Y ⟶ X) → (H : ofArrows Z g f) → j f H → C
k : ⦃Y : C⦄ → (f : Y ⟶ X) → (H : ofArrows Z g f) → (i : j f H) → W f H i ⟶ Y
Y : C
f : Y ⟶ X
⊢ (f ∈ (ofArrows Z g).bind fun x f H => ofArrows (W f H) (k f H)) ↔
    f ∈ ofArrows (fun i => W (g i.fst) ⋯ i.snd) fun ij => k (g ij.fst) ⋯ ij.snd ≫ g ij.fst

Tactic:
constructor

Result:
case h.h.mp
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
ι : Type u_1
Z : ι → C
g : (i : ι) → Z i ⟶ X
j : ⦃Y : C⦄ → (f : Y ⟶ X) → ofArrows Z g f → Type u_2
W : ⦃Y : C⦄ → (f : Y ⟶ X) → (H : ofArrows Z g f) → j f H → C
k : ⦃Y : C⦄ → (f : Y ⟶ X) → (H : ofArrows Z g f) → (i : j f H) → W f H i ⟶ Y
Y : C
f : Y ⟶ X
⊢ (f ∈ (ofArrows Z g).bind fun x f H => ofArrows (W f H) (k f H)) →
    f ∈ ofArrows (fun i => W (g i.fst) ⋯ i.snd) fun ij => k (g ij.fst) ⋯ ij.snd ≫ g ij.fst

case h.h.mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
ι : Type u_1
Z : ι → C
g : (i : ι) → Z i ⟶ X
j : ⦃Y : C⦄ → (f : Y ⟶ X) → ofArrows Z g f → Type u_2
W : ⦃Y : C⦄ → (f : Y ⟶ X) → (H : ofArrows Z g f) → j f H → C
k : ⦃Y : C⦄ → (f : Y ⟶ X) → (H : ofArrows Z g f) → (i : j f H) → W f H i ⟶ Y
Y : C
f : Y ⟶ X
⊢ (f ∈ ofArrows (fun i => W (g i.fst) ⋯ i.snd) fun ij => k (g ij.fst) ⋯ ij.snd ≫ g ij.fst) →
    f ∈ (ofArrows Z g).bind fun x f H => ofArrows (W f H) (k f H)

Proof state:
case h.h.mp
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
ι : Type u_1
Z : ι → C
g : (i : ι) → Z i ⟶ X
j : ⦃Y : C⦄ → (f : Y ⟶ X) → ofArrows Z g f → Type u_2
W : ⦃Y : C⦄ → (f : Y ⟶ X) → (H : ofArrows Z g f) → j f H → C
k : ⦃Y : C⦄ → (f : Y ⟶ X) → (H : ofArrows Z g f) → (i : j f H) → W f H i ⟶ Y
Y : C
f : Y ⟶ X
⊢ (f ∈ (ofArrows Z g).bind fun x f H => ofArrows (W f H) (k f H)) →
    f ∈ ofArrows (fun i => W (g i.fst) ⋯ i.snd) fun ij => k (g ij.fst) ⋯ ij.snd ≫ g ij.fst

Tactic:
rintro ⟨_, _, _, ⟨i⟩, ⟨i'⟩, rfl⟩

Result:
case h.h.mp.intro.intro.intro.intro.mk.intro.mk
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
ι : Type u_1
Z : ι → C
g : (i : ι) → Z i ⟶ X
j : ⦃Y : C⦄ → (f : Y ⟶ X) → ofArrows Z g f → Type u_2
W : ⦃Y : C⦄ → (f : Y ⟶ X) → (H : ofArrows Z g f) → j f H → C
k : ⦃Y : C⦄ → (f : Y ⟶ X) → (H : ofArrows Z g f) → (i : j f H) → W f H i ⟶ Y
Y✝ : C
i : ι
Y : C
i' : j (g i) ⋯
⊢ k (g i) ⋯ i' ≫ g i ∈ ofArrows (fun i => W (g i.fst) ⋯ i.snd) fun ij => k (g ij.fst) ⋯ ij.snd ≫ g ij.fst

Proof state:
case h.h.mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
ι : Type u_1
Z : ι → C
g : (i : ι) → Z i ⟶ X
j : ⦃Y : C⦄ → (f : Y ⟶ X) → ofArrows Z g f → Type u_2
W : ⦃Y : C⦄ → (f : Y ⟶ X) → (H : ofArrows Z g f) → j f H → C
k : ⦃Y : C⦄ → (f : Y ⟶ X) → (H : ofArrows Z g f) → (i : j f H) → W f H i ⟶ Y
Y : C
f : Y ⟶ X
⊢ (f ∈ ofArrows (fun i => W (g i.fst) ⋯ i.snd) fun ij => k (g ij.fst) ⋯ ij.snd ≫ g ij.fst) →
    f ∈ (ofArrows Z g).bind fun x f H => ofArrows (W f H) (k f H)

Tactic:
rintro ⟨i⟩

Result:
case h.h.mpr.mk
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
ι : Type u_1
Z : ι → C
g : (i : ι) → Z i ⟶ X
j : ⦃Y : C⦄ → (f : Y ⟶ X) → ofArrows Z g f → Type u_2
W : ⦃Y : C⦄ → (f : Y ⟶ X) → (H : ofArrows Z g f) → j f H → C
k : ⦃Y : C⦄ → (f : Y ⟶ X) → (H : ofArrows Z g f) → (i : j f H) → W f H i ⟶ Y
Y : C
i : (i : ι) × j (g i) ⋯
⊢ k (g i.fst) ⋯ i.snd ≫ g i.fst ∈ (ofArrows Z g).bind fun x f H => ofArrows (W f H) (k f H)

Proof state:
case h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
ι : Type u_1
Z : ι → C
g : (i : ι) → Z i ⟶ X
j : ⦃Y : C⦄ → (f : Y ⟶ X) → ofArrows Z g f → Type u_2
W : ⦃Y : C⦄ → (f : Y ⟶ X) → (H : ofArrows Z g f) → j f H → C
k : ⦃Y : C⦄ → (f : Y ⟶ X) → (H : ofArrows Z g f) → (i : j f H) → W f H i ⟶ Y
Y : C
⊢ ((ofArrows Z g).bind fun x f H => ofArrows (W f H) (k f H)) =
    ofArrows (fun i => W (g i.fst) ⋯ i.snd) fun ij => k (g ij.fst) ⋯ ij.snd ≫ g ij.fst

Tactic:
ext f

Result:
case h.h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
ι : Type u_1
Z : ι → C
g : (i : ι) → Z i ⟶ X
j : ⦃Y : C⦄ → (f : Y ⟶ X) → ofArrows Z g f → Type u_2
W : ⦃Y : C⦄ → (f : Y ⟶ X) → (H : ofArrows Z g f) → j f H → C
k : ⦃Y : C⦄ → (f : Y ⟶ X) → (H : ofArrows Z g f) → (i : j f H) → W f H i ⟶ Y
Y : C
f : Y ⟶ X
⊢ (f ∈ (ofArrows Z g).bind fun x f H => ofArrows (W f H) (k f H)) ↔
    f ∈ ofArrows (fun i => W (g i.fst) ⋯ i.snd) fun ij => k (g ij.fst) ⋯ ij.snd ≫ g ij.fst

Proof state:
case h.h.mp.intro.intro.intro.intro.mk.intro.mk
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
ι : Type u_1
Z : ι → C
g : (i : ι) → Z i ⟶ X
j : ⦃Y : C⦄ → (f : Y ⟶ X) → ofArrows Z g f → Type u_2
W : ⦃Y : C⦄ → (f : Y ⟶ X) → (H : ofArrows Z g f) → j f H → C
k : ⦃Y : C⦄ → (f : Y ⟶ X) → (H : ofArrows Z g f) → (i : j f H) → W f H i ⟶ Y
Y✝ : C
i : ι
Y : C
i' : j (g i) ⋯
⊢ k (g i) ⋯ i' ≫ g i ∈ ofArrows (fun i => W (g i.fst) ⋯ i.snd) fun ij => k (g ij.fst) ⋯ ij.snd ≫ g ij.fst

Tactic:
exact ofArrows.mk (Sigma.mk _ _)

Result:
no goals

Proof state:
case h.h.mpr.mk
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
ι : Type u_1
Z : ι → C
g : (i : ι) → Z i ⟶ X
j : ⦃Y : C⦄ → (f : Y ⟶ X) → ofArrows Z g f → Type u_2
W : ⦃Y : C⦄ → (f : Y ⟶ X) → (H : ofArrows Z g f) → j f H → C
k : ⦃Y : C⦄ → (f : Y ⟶ X) → (H : ofArrows Z g f) → (i : j f H) → W f H i ⟶ Y
Y : C
i : (i : ι) × j (g i) ⋯
⊢ k (g i.fst) ⋯ i.snd ≫ g i.fst ∈ (ofArrows Z g).bind fun x f H => ofArrows (W f H) (k f H)

Tactic:
exact bind_comp _ (ofArrows.mk _) (ofArrows.mk _)

Result:
no goals

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
ι : Type u_1
Z : ι → C
g : (i : ι) → Z i ⟶ X
j : ⦃Y : C⦄ → (f : Y ⟶ X) → ofArrows Z g f → Type u_2
W : ⦃Y : C⦄ → (f : Y ⟶ X) → (H : ofArrows Z g f) → j f H → C
k : ⦃Y : C⦄ → (f : Y ⟶ X) → (H : ofArrows Z g f) → (i : j f H) → W f H i ⟶ Y
⊢ ((ofArrows Z g).bind fun x f H => ofArrows (W f H) (k f H)) =
    ofArrows (fun i => W (g i.fst) ⋯ i.snd) fun ij => k (g ij.fst) ⋯ ij.snd ≫ g ij.fst

Tactic:
funext Y

Result:
case h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
ι : Type u_1
Z : ι → C
g : (i : ι) → Z i ⟶ X
j : ⦃Y : C⦄ → (f : Y ⟶ X) → ofArrows Z g f → Type u_2
W : ⦃Y : C⦄ → (f : Y ⟶ X) → (H : ofArrows Z g f) → j f H → C
k : ⦃Y : C⦄ → (f : Y ⟶ X) → (H : ofArrows Z g f) → (i : j f H) → W f H i ⟶ Y
Y : C
⊢ ((ofArrows Z g).bind fun x f H => ofArrows (W f H) (k f H)) =
    ofArrows (fun i => W (g i.fst) ⋯ i.snd) fun ij => k (g ij.fst) ⋯ ij.snd ≫ g ij.fst