-- Mathlib/CategoryTheory/Sites/IsSheafFor.lean
theorem FamilyOfElements.Compatible.pullback (f : Y ⟶ X) {x : FamilyOfElements P S.arrows}
    (h : x.Compatible) : (x.pullback f).Compatible

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X Y : C
S : Sieve X
f : Y ⟶ X
x : FamilyOfElements P S.arrows
h : x.SieveCompatible
W Z : C
f₁ : W ⟶ Y
f₂ : Z ⟶ W
hf : (Sieve.pullback f S).arrows f₁
⊢ FamilyOfElements.pullback f x (f₂ ≫ f₁) ⋯ = P.map f₂.op (FamilyOfElements.pullback f x f₁ hf)

Tactic:
unfold FamilyOfElements.pullback

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X Y : C
S : Sieve X
f : Y ⟶ X
x : FamilyOfElements P S.arrows
h : x.SieveCompatible
W Z : C
f₁ : W ⟶ Y
f₂ : Z ⟶ W
hf : (Sieve.pullback f S).arrows f₁
⊢ x ((f₂ ≫ f₁) ≫ f) ⋯ = P.map f₂.op (x (f₁ ≫ f) hf)

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X Y : C
S : Sieve X
f : Y ⟶ X
x : FamilyOfElements P S.arrows
h : x.SieveCompatible
⊢ (FamilyOfElements.pullback f x).SieveCompatible

Tactic:
intro W Z f₁ f₂ hf

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X Y : C
S : Sieve X
f : Y ⟶ X
x : FamilyOfElements P S.arrows
h : x.SieveCompatible
W Z : C
f₁ : W ⟶ Y
f₂ : Z ⟶ W
hf : (Sieve.pullback f S).arrows f₁
⊢ FamilyOfElements.pullback f x (f₂ ≫ f₁) ⋯ = P.map f₂.op (FamilyOfElements.pullback f x f₁ hf)

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X Y : C
S : Sieve X
f : Y ⟶ X
x : FamilyOfElements P S.arrows
h : x.Compatible
⊢ (FamilyOfElements.pullback f x).Compatible

Tactic:
simp only [compatible_iff_sieveCompatible] at h ⊢

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X Y : C
S : Sieve X
f : Y ⟶ X
x : FamilyOfElements P S.arrows
h : x.SieveCompatible
⊢ (FamilyOfElements.pullback f x).SieveCompatible

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X Y : C
S : Sieve X
f : Y ⟶ X
x : FamilyOfElements P S.arrows
h : x.SieveCompatible
W Z : C
f₁ : W ⟶ Y
f₂ : Z ⟶ W
hf : (Sieve.pullback f S).arrows f₁
⊢ x ((f₂ ≫ f₁) ≫ f) ⋯ = P.map f₂.op (x (f₁ ≫ f) hf)

Tactic:
rw [← h (f₁ ≫ f) f₂ hf]

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X Y : C
S : Sieve X
f : Y ⟶ X
x : FamilyOfElements P S.arrows
h : x.SieveCompatible
W Z : C
f₁ : W ⟶ Y
f₂ : Z ⟶ W
hf : (Sieve.pullback f S).arrows f₁
⊢ x ((f₂ ≫ f₁) ≫ f) ⋯ = x (f₂ ≫ f₁ ≫ f) ⋯

Proof state:
case e_f
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X Y : C
S : Sieve X
f : Y ⟶ X
x : FamilyOfElements P S.arrows
h : x.SieveCompatible
W Z : C
f₁ : W ⟶ Y
f₂ : Z ⟶ W
hf : (Sieve.pullback f S).arrows f₁
⊢ (f₂ ≫ f₁) ≫ f = f₂ ≫ f₁ ≫ f

Tactic:
simp only [assoc]

Result:
no goals

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X Y : C
S : Sieve X
f : Y ⟶ X
x : FamilyOfElements P S.arrows
h : x.SieveCompatible
W Z : C
f₁ : W ⟶ Y
f₂ : Z ⟶ W
hf : (Sieve.pullback f S).arrows f₁
⊢ x ((f₂ ≫ f₁) ≫ f) ⋯ = x (f₂ ≫ f₁ ≫ f) ⋯

Tactic:
congr 1

Result:
case e_f
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X Y : C
S : Sieve X
f : Y ⟶ X
x : FamilyOfElements P S.arrows
h : x.SieveCompatible
W Z : C
f₁ : W ⟶ Y
f₂ : Z ⟶ W
hf : (Sieve.pullback f S).arrows f₁
⊢ (f₂ ≫ f₁) ≫ f = f₂ ≫ f₁ ≫ f