Theorem: CategoryTheory.Equalizer.Presieve.w' (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
⊢ forkMap P S ≫ firstMap' P (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) =
    forkMap P S ≫ secondMap' P (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g)
Tactic:
ext fg
State after:
case h.h
C : Type u₁
inst✝ : Category C
X : C
S : Presieve X
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
hS : isPullbackPresieve S
fg : ((Y : C) × { f // S f }) × (Z : C) × { g // S g }
a✝ : P.obj X.op
⊢ ((forkMap P S ≫ firstMap' P (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g)) ≫
        Pi.π (fun fg => P.obj (Limits.pullback ↑fg.fst.snd ↑fg.snd.snd).op) fg)
      a✝ =
    ((forkMap P S ≫ secondMap' P (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g)) ≫
        Pi.π (fun fg => P.obj (Limits.pullback ↑fg.fst.snd ↑fg.snd.snd).op) fg)
      a✝

State before:
case h.h
C : Type u₁
inst✝ : Category C
X : C
S : Presieve X
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
hS : isPullbackPresieve S
fg : ((Y : C) × { f // S f }) × (Z : C) × { g // S g }
a✝ : P.obj X.op
⊢ ((forkMap P S ≫ firstMap' P (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g)) ≫
        Pi.π (fun fg => P.obj (Limits.pullback ↑fg.fst.snd ↑fg.snd.snd).op) fg)
      a✝ =
    ((forkMap P S ≫ secondMap' P (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g)) ≫
        Pi.π (fun fg => P.obj (Limits.pullback ↑fg.fst.snd ↑fg.snd.snd).op) fg)
      a✝
Tactic:
simp only [firstMap', secondMap', forkMap]
State after:
case h.h
C : Type u₁
inst✝ : Category C
X : C
S : Presieve X
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
hS : isPullbackPresieve S
fg : ((Y : C) × { f // S f }) × (Z : C) × { g // S g }
a✝ : P.obj X.op
⊢ (((Pi.lift fun f => P.map (↑f.snd).op) ≫
          Pi.lift fun fg => Pi.π (fun f => P.obj f.fst.op) fg.fst ≫ P.map pullback.fst.op) ≫
        Pi.π (fun fg => P.obj (Limits.pullback ↑fg.fst.snd ↑fg.snd.snd).op) fg)
      a✝ =
    (((Pi.lift fun f => P.map (↑f.snd).op) ≫
          Pi.lift fun fg => Pi.π (fun f => P.obj f.fst.op) fg.snd ≫ P.map pullback.snd.op) ≫
        Pi.π (fun fg => P.obj (Limits.pullback ↑fg.fst.snd ↑fg.snd.snd).op) fg)
      a✝

State before:
case h.h
C : Type u₁
inst✝ : Category C
X : C
S : Presieve X
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
hS : isPullbackPresieve S
fg : ((Y : C) × { f // S f }) × (Z : C) × { g // S g }
a✝ : P.obj X.op
⊢ (((Pi.lift fun f => P.map (↑f.snd).op) ≫
          Pi.lift fun fg => Pi.π (fun f => P.obj f.fst.op) fg.fst ≫ P.map pullback.fst.op) ≫
        Pi.π (fun fg => P.obj (Limits.pullback ↑fg.fst.snd ↑fg.snd.snd).op) fg)
      a✝ =
    (((Pi.lift fun f => P.map (↑f.snd).op) ≫
          Pi.lift fun fg => Pi.π (fun f => P.obj f.fst.op) fg.snd ≫ P.map pullback.snd.op) ≫
        Pi.π (fun fg => P.obj (Limits.pullback ↑fg.fst.snd ↑fg.snd.snd).op) fg)
      a✝
Tactic:
simp only [limit.lift_π, limit.lift_π_assoc, assoc, Fan.mk_π_app]
State after:
case h.h
C : Type u₁
inst✝ : Category C
X : C
S : Presieve X
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
hS : isPullbackPresieve S
fg : ((Y : C) × { f // S f }) × (Z : C) × { g // S g }
a✝ : P.obj X.op
⊢ (P.map (↑fg.fst.snd).op ≫ P.map pullback.fst.op) a✝ = (P.map (↑fg.snd.snd).op ≫ P.map pullback.snd.op) a✝

State before:
case h.h
C : Type u₁
inst✝ : Category C
X : C
S : Presieve X
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
hS : isPullbackPresieve S
fg : ((Y : C) × { f // S f }) × (Z : C) × { g // S g }
a✝ : P.obj X.op
⊢ (P.map (↑fg.fst.snd).op ≫ P.map pullback.fst.op) a✝ = (P.map (↑fg.snd.snd).op ≫ P.map pullback.snd.op) a✝
Tactic:
have := hS fg.1.2.2 fg.2.2.2
State after:
case h.h
C : Type u₁
inst✝ : Category C
X : C
S : Presieve X
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
hS : isPullbackPresieve S
fg : ((Y : C) × { f // S f }) × (Z : C) × { g // S g }
a✝ : P.obj X.op
this : HasPullback ↑fg.fst.snd ↑fg.snd.snd
⊢ (P.map (↑fg.fst.snd).op ≫ P.map pullback.fst.op) a✝ = (P.map (↑fg.snd.snd).op ≫ P.map pullback.snd.op) a✝

State before:
case h.h
C : Type u₁
inst✝ : Category C
X : C
S : Presieve X
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
hS : isPullbackPresieve S
fg : ((Y : C) × { f // S f }) × (Z : C) × { g // S g }
a✝ : P.obj X.op
this : HasPullback ↑fg.fst.snd ↑fg.snd.snd
⊢ (P.map (↑fg.fst.snd).op ≫ P.map pullback.fst.op) a✝ = (P.map (↑fg.snd.snd).op ≫ P.map pullback.snd.op) a✝
Tactic:
rw [← P.map_comp, ← op_comp, pullback.condition]
State after:
case h.h
C : Type u₁
inst✝ : Category C
X : C
S : Presieve X
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
hS : isPullbackPresieve S
fg : ((Y : C) × { f // S f }) × (Z : C) × { g // S g }
a✝ : P.obj X.op
this : HasPullback ↑fg.fst.snd ↑fg.snd.snd
⊢ P.map (pullback.snd ≫ ↑fg.snd.snd).op a✝ = (P.map (↑fg.snd.snd).op ≫ P.map pullback.snd.op) a✝

State before:
case h.h
C : Type u₁
inst✝ : Category C
X : C
S : Presieve X
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
hS : isPullbackPresieve S
fg : ((Y : C) × { f // S f }) × (Z : C) × { g // S g }
a✝ : P.obj X.op
this : HasPullback ↑fg.fst.snd ↑fg.snd.snd
⊢ P.map (pullback.snd ≫ ↑fg.snd.snd).op a✝ = (P.map (↑fg.snd.snd).op ≫ P.map pullback.snd.op) a✝
Tactic:
simp
State after:
no goals