-- Mathlib/CategoryTheory/Sites/IsSheafFor.lean
theorem FamilyOfElements.Compatible.sieveExtend {x : FamilyOfElements P R} (hx : x.Compatible) :
    x.sieveExtend.Compatible

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P R
hx : x.Compatible
Y₁✝ Y₂✝ Z✝ : C
g₁✝ : Z✝ ⟶ Y₁✝
g₂✝ : Z✝ ⟶ Y₂✝
f₁✝ : Y₁✝ ⟶ X
f₂✝ : Y₂✝ ⟶ X
h₁ : (generate R).arrows f₁✝
h₂ : (generate R).arrows f₂✝
comm : g₁✝ ≫ f₁✝ = g₂✝ ≫ f₂✝
⊢ P.map g₁✝.op (x.sieveExtend f₁✝ h₁) = P.map g₂✝.op (x.sieveExtend f₂✝ h₂)

Tactic:
iterate 2 erw [← FunctorToTypes.map_comp_apply]; rw [← op_comp]

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P R
hx : x.Compatible
Y₁✝ Y₂✝ Z✝ : C
g₁✝ : Z✝ ⟶ Y₁✝
g₂✝ : Z✝ ⟶ Y₂✝
f₁✝ : Y₁✝ ⟶ X
f₂✝ : Y₂✝ ⟶ X
h₁ : (generate R).arrows f₁✝
h₂ : (generate R).arrows f₂✝
comm : g₁✝ ≫ f₁✝ = g₂✝ ≫ f₂✝
⊢ P.map (g₁✝ ≫ ⋯.choose).op (x ⋯.choose ⋯) = P.map (g₂✝ ≫ ⋯.choose).op (x ⋯.choose ⋯)

Proof state:
case a
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P R
hx : x.Compatible
Y₁✝ Y₂✝ Z✝ : C
g₁✝ : Z✝ ⟶ Y₁✝
g₂✝ : Z✝ ⟶ Y₂✝
f₁✝ : Y₁✝ ⟶ X
f₂✝ : Y₂✝ ⟶ X
h₁ : (generate R).arrows f₁✝
h₂ : (generate R).arrows f₂✝
comm : g₁✝ ≫ f₁✝ = g₂✝ ≫ f₂✝
⊢ (g₁✝ ≫ ⋯.choose) ≫ ⋯.choose = (g₂✝ ≫ ⋯.choose) ≫ ⋯.choose

Tactic:
simp [comm, h₁.choose_spec.choose_spec.choose_spec.2, h₂.choose_spec.choose_spec.choose_spec.2]

Result:
no goals

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P R
hx : x.Compatible
⊢ x.sieveExtend.Compatible

Tactic:
intro _ _ _ _ _ _ _ h₁ h₂ comm

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P R
hx : x.Compatible
Y₁✝ Y₂✝ Z✝ : C
g₁✝ : Z✝ ⟶ Y₁✝
g₂✝ : Z✝ ⟶ Y₂✝
f₁✝ : Y₁✝ ⟶ X
f₂✝ : Y₂✝ ⟶ X
h₁ : (generate R).arrows f₁✝
h₂ : (generate R).arrows f₂✝
comm : g₁✝ ≫ f₁✝ = g₂✝ ≫ f₂✝
⊢ P.map g₁✝.op (x.sieveExtend f₁✝ h₁) = P.map g₂✝.op (x.sieveExtend f₂✝ h₂)

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P R
hx : x.Compatible
Y₁✝ Y₂✝ Z✝ : C
g₁✝ : Z✝ ⟶ Y₁✝
g₂✝ : Z✝ ⟶ Y₂✝
f₁✝ : Y₁✝ ⟶ X
f₂✝ : Y₂✝ ⟶ X
h₁ : (generate R).arrows f₁✝
h₂ : (generate R).arrows f₂✝
comm : g₁✝ ≫ f₁✝ = g₂✝ ≫ f₂✝
⊢ P.map (g₁✝ ≫ ⋯.choose).op (x ⋯.choose ⋯) = P.map g₂✝.op (x.sieveExtend f₂✝ h₂)

Tactic:
erw [← FunctorToTypes.map_comp_apply]

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P R
hx : x.Compatible
Y₁✝ Y₂✝ Z✝ : C
g₁✝ : Z✝ ⟶ Y₁✝
g₂✝ : Z✝ ⟶ Y₂✝
f₁✝ : Y₁✝ ⟶ X
f₂✝ : Y₂✝ ⟶ X
h₁ : (generate R).arrows f₁✝
h₂ : (generate R).arrows f₂✝
comm : g₁✝ ≫ f₁✝ = g₂✝ ≫ f₂✝
⊢ P.map (g₁✝ ≫ ⋯.choose).op (x ⋯.choose ⋯) = P.map (⋯.choose.op ≫ g₂✝.op) (x ⋯.choose ⋯)

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P R
hx : x.Compatible
Y₁✝ Y₂✝ Z✝ : C
g₁✝ : Z✝ ⟶ Y₁✝
g₂✝ : Z✝ ⟶ Y₂✝
f₁✝ : Y₁✝ ⟶ X
f₂✝ : Y₂✝ ⟶ X
h₁ : (generate R).arrows f₁✝
h₂ : (generate R).arrows f₂✝
comm : g₁✝ ≫ f₁✝ = g₂✝ ≫ f₂✝
⊢ P.map (g₁✝ ≫ ⋯.choose).op (x ⋯.choose ⋯) = P.map (g₂✝ ≫ ⋯.choose).op (x ⋯.choose ⋯)

Tactic:
apply hx

Result:
case a
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P R
hx : x.Compatible
Y₁✝ Y₂✝ Z✝ : C
g₁✝ : Z✝ ⟶ Y₁✝
g₂✝ : Z✝ ⟶ Y₂✝
f₁✝ : Y₁✝ ⟶ X
f₂✝ : Y₂✝ ⟶ X
h₁ : (generate R).arrows f₁✝
h₂ : (generate R).arrows f₂✝
comm : g₁✝ ≫ f₁✝ = g₂✝ ≫ f₂✝
⊢ (g₁✝ ≫ ⋯.choose) ≫ ⋯.choose = (g₂✝ ≫ ⋯.choose) ≫ ⋯.choose

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P R
hx : x.Compatible
Y₁✝ Y₂✝ Z✝ : C
g₁✝ : Z✝ ⟶ Y₁✝
g₂✝ : Z✝ ⟶ Y₂✝
f₁✝ : Y₁✝ ⟶ X
f₂✝ : Y₂✝ ⟶ X
h₁ : (generate R).arrows f₁✝
h₂ : (generate R).arrows f₂✝
comm : g₁✝ ≫ f₁✝ = g₂✝ ≫ f₂✝
⊢ P.map (g₁✝ ≫ ⋯.choose).op (x ⋯.choose ⋯) = P.map (⋯.choose.op ≫ g₂✝.op) (x ⋯.choose ⋯)

Tactic:
rw [← op_comp]

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P R
hx : x.Compatible
Y₁✝ Y₂✝ Z✝ : C
g₁✝ : Z✝ ⟶ Y₁✝
g₂✝ : Z✝ ⟶ Y₂✝
f₁✝ : Y₁✝ ⟶ X
f₂✝ : Y₂✝ ⟶ X
h₁ : (generate R).arrows f₁✝
h₂ : (generate R).arrows f₂✝
comm : g₁✝ ≫ f₁✝ = g₂✝ ≫ f₂✝
⊢ P.map (g₁✝ ≫ ⋯.choose).op (x ⋯.choose ⋯) = P.map (g₂✝ ≫ ⋯.choose).op (x ⋯.choose ⋯)