Theorem: CategoryTheory.Presieve.pullbackCompatible_iff' (Sieves/isSheafForPullbackSieve.lean)

State before:
C : Type u₁
inst✝ : Category C
X : C
S : Presieve X
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
hS : isPullbackPresieve S
x : FamilyOfElements P S
⊢ FamilyOfElements.Compatible x ↔
    FamilyOfElements.PullbackCompatible' P (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) x
Tactic:
constructor
State after:
case mp
C : Type u₁
inst✝ : Category C
X : C
S : Presieve X
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
hS : isPullbackPresieve S
x : FamilyOfElements P S
⊢ FamilyOfElements.Compatible x →
    FamilyOfElements.PullbackCompatible' P (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) x

case mpr
C : Type u₁
inst✝ : Category C
X : C
S : Presieve X
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
hS : isPullbackPresieve S
x : FamilyOfElements P S
⊢ FamilyOfElements.PullbackCompatible' P (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) x →
    FamilyOfElements.Compatible x

State before:
case mp
C : Type u₁
inst✝ : Category C
X : C
S : Presieve X
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
hS : isPullbackPresieve S
x : FamilyOfElements P S
⊢ FamilyOfElements.Compatible x →
    FamilyOfElements.PullbackCompatible' P (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) x
Tactic:
intro t Y₁ Y₂ f₁ f₂ hf₁ hf₂
State after:
case mp
C : Type u₁
inst✝ : Category C
X : C
S : Presieve X
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
hS : isPullbackPresieve S
x : FamilyOfElements P S
t : FamilyOfElements.Compatible x
Y₁ Y₂ : C
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
hf₁ : S f₁
hf₂ : S f₂
⊢ let_fun this := (_ : HasPullback f₁ f₂);
  P.map pullback.fst.op (x f₁ hf₁) = P.map pullback.snd.op (x f₂ hf₂)

State before:
case mp
C : Type u₁
inst✝ : Category C
X : C
S : Presieve X
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
hS : isPullbackPresieve S
x : FamilyOfElements P S
t : FamilyOfElements.Compatible x
Y₁ Y₂ : C
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
hf₁ : S f₁
hf₂ : S f₂
⊢ let_fun this := (_ : HasPullback f₁ f₂);
  P.map pullback.fst.op (x f₁ hf₁) = P.map pullback.snd.op (x f₂ hf₂)
Tactic:
apply t
State after:
case mp.a
C : Type u₁
inst✝ : Category C
X : C
S : Presieve X
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
hS : isPullbackPresieve S
x : FamilyOfElements P S
t : FamilyOfElements.Compatible x
Y₁ Y₂ : C
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
hf₁ : S f₁
hf₂ : S f₂
⊢ pullback.fst ≫ f₁ = pullback.snd ≫ f₂

State before:
case mp.a
C : Type u₁
inst✝ : Category C
X : C
S : Presieve X
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
hS : isPullbackPresieve S
x : FamilyOfElements P S
t : FamilyOfElements.Compatible x
Y₁ Y₂ : C
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
hf₁ : S f₁
hf₂ : S f₂
⊢ pullback.fst ≫ f₁ = pullback.snd ≫ f₂
Tactic:
have := hS hf₁ hf₂
State after:
case mp.a
C : Type u₁
inst✝ : Category C
X : C
S : Presieve X
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
hS : isPullbackPresieve S
x : FamilyOfElements P S
t : FamilyOfElements.Compatible x
Y₁ Y₂ : C
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
hf₁ : S f₁
hf₂ : S f₂
this : HasPullback f₁ f₂
⊢ pullback.fst ≫ f₁ = pullback.snd ≫ f₂

State before:
case mp.a
C : Type u₁
inst✝ : Category C
X : C
S : Presieve X
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
hS : isPullbackPresieve S
x : FamilyOfElements P S
t : FamilyOfElements.Compatible x
Y₁ Y₂ : C
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
hf₁ : S f₁
hf₂ : S f₂
this : HasPullback f₁ f₂
⊢ pullback.fst ≫ f₁ = pullback.snd ≫ f₂
Tactic:
apply pullback.condition
State after:
no goals

State before:
case mpr
C : Type u₁
inst✝ : Category C
X : C
S : Presieve X
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
hS : isPullbackPresieve S
x : FamilyOfElements P S
⊢ FamilyOfElements.PullbackCompatible' P (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) x →
    FamilyOfElements.Compatible x
Tactic:
intro t Y₁ Y₂ Z g₁ g₂ f₁ f₂ hf₁ hf₂ comm
State after:
case mpr
C : Type u₁
inst✝ : Category C
X : C
S : Presieve X
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
hS : isPullbackPresieve S
x : FamilyOfElements P S
t : FamilyOfElements.PullbackCompatible' P (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) x
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
hf₁ : S f₁
hf₂ : S f₂
comm : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ P.map g₁.op (x f₁ hf₁) = P.map g₂.op (x f₂ hf₂)

State before:
case mpr
C : Type u₁
inst✝ : Category C
X : C
S : Presieve X
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
hS : isPullbackPresieve S
x : FamilyOfElements P S
t : FamilyOfElements.PullbackCompatible' P (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) x
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
hf₁ : S f₁
hf₂ : S f₂
comm : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ P.map g₁.op (x f₁ hf₁) = P.map g₂.op (x f₂ hf₂)
Tactic:
have := hS hf₁ hf₂
State after:
case mpr
C : Type u₁
inst✝ : Category C
X : C
S : Presieve X
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
hS : isPullbackPresieve S
x : FamilyOfElements P S
t : FamilyOfElements.PullbackCompatible' P (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) x
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
hf₁ : S f₁
hf₂ : S f₂
comm : g₁ ≫ f₁ = g₂ ≫ f₂
this : HasPullback f₁ f₂
⊢ P.map g₁.op (x f₁ hf₁) = P.map g₂.op (x f₂ hf₂)

State before:
case mpr
C : Type u₁
inst✝ : Category C
X : C
S : Presieve X
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
hS : isPullbackPresieve S
x : FamilyOfElements P S
t : FamilyOfElements.PullbackCompatible' P (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) x
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
hf₁ : S f₁
hf₂ : S f₂
comm : g₁ ≫ f₁ = g₂ ≫ f₂
this : HasPullback f₁ f₂
⊢ P.map g₁.op (x f₁ hf₁) = P.map g₂.op (x f₂ hf₂)
Tactic:
rw [← pullback.lift_fst _ _ comm, op_comp, FunctorToTypes.map_comp_apply, t hf₁ hf₂,
  ← FunctorToTypes.map_comp_apply, ← op_comp, pullback.lift_snd]
State after:
no goals