-- Mathlib/AlgebraicGeometry/Pullbacks.lean
theorem cocycle (i j k : 𝒰.J) : t' 𝒰 f g i j k ≫ t' 𝒰 f g j k i ≫ t' 𝒰 f g k i j = 𝟙 _

Proof state:
case h₀
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f) g
i j k : 𝒰.J
⊢ (t' 𝒰 f g i j k ≫ t' 𝒰 f g j k i ≫ t' 𝒰 f g k i j) ≫ pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k) =
    pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k)

Tactic:
apply pullback.hom_ext

Result:
case h₀.h₀
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f) g
i j k : 𝒰.J
⊢ ((t' 𝒰 f g i j k ≫ t' 𝒰 f g j k i ≫ t' 𝒰 f g k i j) ≫ pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k)) ≫
      pullback.fst (pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map j) =
    pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫ pullback.fst (pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map j)

case h₀.h₁
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f) g
i j k : 𝒰.J
⊢ ((t' 𝒰 f g i j k ≫ t' 𝒰 f g j k i ≫ t' 𝒰 f g k i j) ≫ pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k)) ≫
      pullback.snd (pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map j) =
    pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫ pullback.snd (pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map j)

Proof state:
case h₁.h₀.h₁
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f) g
i j k : 𝒰.J
⊢ (((t' 𝒰 f g i j k ≫ t' 𝒰 f g j k i ≫ t' 𝒰 f g k i j) ≫ pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k)) ≫
        pullback.fst (pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map k)) ≫
      pullback.snd (𝒰.map i ≫ f) g =
    (pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫ pullback.fst (pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map k)) ≫
      pullback.snd (𝒰.map i ≫ f) g

Tactic:
simp_rw [Category.assoc, cocycle_snd_fst_snd 𝒰 f g i j k]

Result:
no goals

Proof state:
case h₁.h₀
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f) g
i j k : 𝒰.J
⊢ ((t' 𝒰 f g i j k ≫ t' 𝒰 f g j k i ≫ t' 𝒰 f g k i j) ≫ pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k)) ≫
      pullback.fst (pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map k) =
    pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫ pullback.fst (pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map k)

Tactic:
apply pullback.hom_ext

Result:
case h₁.h₀.h₀
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f) g
i j k : 𝒰.J
⊢ (((t' 𝒰 f g i j k ≫ t' 𝒰 f g j k i ≫ t' 𝒰 f g k i j) ≫ pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k)) ≫
        pullback.fst (pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map k)) ≫
      pullback.fst (𝒰.map i ≫ f) g =
    (pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫ pullback.fst (pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map k)) ≫
      pullback.fst (𝒰.map i ≫ f) g

case h₁.h₀.h₁
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f) g
i j k : 𝒰.J
⊢ (((t' 𝒰 f g i j k ≫ t' 𝒰 f g j k i ≫ t' 𝒰 f g k i j) ≫ pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k)) ≫
        pullback.fst (pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map k)) ≫
      pullback.snd (𝒰.map i ≫ f) g =
    (pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫ pullback.fst (pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map k)) ≫
      pullback.snd (𝒰.map i ≫ f) g

Proof state:
case h₁
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f) g
i j k : 𝒰.J
⊢ (t' 𝒰 f g i j k ≫ t' 𝒰 f g j k i ≫ t' 𝒰 f g k i j) ≫ pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k) =
    pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k)

Tactic:
apply pullback.hom_ext

Result:
case h₁.h₀
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f) g
i j k : 𝒰.J
⊢ ((t' 𝒰 f g i j k ≫ t' 𝒰 f g j k i ≫ t' 𝒰 f g k i j) ≫ pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k)) ≫
      pullback.fst (pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map k) =
    pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫ pullback.fst (pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map k)

case h₁.h₁
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f) g
i j k : 𝒰.J
⊢ ((t' 𝒰 f g i j k ≫ t' 𝒰 f g j k i ≫ t' 𝒰 f g k i j) ≫ pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k)) ≫
      pullback.snd (pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map k) =
    pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫ pullback.snd (pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map k)

Proof state:
case h₁.h₁
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f) g
i j k : 𝒰.J
⊢ ((t' 𝒰 f g i j k ≫ t' 𝒰 f g j k i ≫ t' 𝒰 f g k i j) ≫ pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k)) ≫
      pullback.snd (pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map k) =
    pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫ pullback.snd (pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map k)

Tactic:
simp_rw [Category.assoc, cocycle_snd_snd 𝒰 f g i j k]

Result:
no goals

Proof state:
case h₁.h₀.h₀
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f) g
i j k : 𝒰.J
⊢ (((t' 𝒰 f g i j k ≫ t' 𝒰 f g j k i ≫ t' 𝒰 f g k i j) ≫ pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k)) ≫
        pullback.fst (pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map k)) ≫
      pullback.fst (𝒰.map i ≫ f) g =
    (pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫ pullback.fst (pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map k)) ≫
      pullback.fst (𝒰.map i ≫ f) g

Tactic:
simp_rw [Category.assoc, cocycle_snd_fst_fst 𝒰 f g i j k]

Result:
no goals

Proof state:
case h₀.h₀.h₁
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f) g
i j k : 𝒰.J
⊢ (((t' 𝒰 f g i j k ≫ t' 𝒰 f g j k i ≫ t' 𝒰 f g k i j) ≫ pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k)) ≫
        pullback.fst (pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map j)) ≫
      pullback.snd (𝒰.map i ≫ f) g =
    (pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫ pullback.fst (pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map j)) ≫
      pullback.snd (𝒰.map i ≫ f) g

Tactic:
simp_rw [Category.assoc, cocycle_fst_fst_snd 𝒰 f g i j k]

Result:
no goals

Proof state:
case h₀.h₁
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f) g
i j k : 𝒰.J
⊢ ((t' 𝒰 f g i j k ≫ t' 𝒰 f g j k i ≫ t' 𝒰 f g k i j) ≫ pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k)) ≫
      pullback.snd (pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map j) =
    pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫ pullback.snd (pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map j)

Tactic:
simp_rw [Category.assoc, cocycle_fst_snd 𝒰 f g i j k]

Result:
no goals

Proof state:
case h₀.h₀.h₀
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f) g
i j k : 𝒰.J
⊢ (((t' 𝒰 f g i j k ≫ t' 𝒰 f g j k i ≫ t' 𝒰 f g k i j) ≫ pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k)) ≫
        pullback.fst (pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map j)) ≫
      pullback.fst (𝒰.map i ≫ f) g =
    (pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫ pullback.fst (pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map j)) ≫
      pullback.fst (𝒰.map i ≫ f) g

Tactic:
simp_rw [Category.assoc, cocycle_fst_fst_fst 𝒰 f g i j k]

Result:
no goals