Theorem: CategoryTheory.Equalizer.Presieve.compatible_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 : FirstObj P S
⊢ Presieve.FamilyOfElements.Compatible ((firstObjEqFamily P S).hom x) ↔
    firstMap' P (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) x =
      secondMap' P (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) x
Tactic:
rw [Presieve.pullbackCompatible_iff' _ hS]
State after:
C : Type u₁
inst✝ : Category C
X : C
S : Presieve X
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
hS : isPullbackPresieve S
x : FirstObj P S
⊢ Presieve.FamilyOfElements.PullbackCompatible' P
      (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) ((firstObjEqFamily P S).hom x) ↔
    firstMap' P (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) x =
      secondMap' P (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) x

State before:
C : Type u₁
inst✝ : Category C
X : C
S : Presieve X
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
hS : isPullbackPresieve S
x : FirstObj P S
⊢ Presieve.FamilyOfElements.PullbackCompatible' P
      (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) ((firstObjEqFamily P S).hom x) ↔
    firstMap' P (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) x =
      secondMap' 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 : FirstObj P S
⊢ Presieve.FamilyOfElements.PullbackCompatible' P
      (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) ((firstObjEqFamily P S).hom x) →
    firstMap' P (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) x =
      secondMap' 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 : FirstObj P S
⊢ firstMap' P (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) x =
      secondMap' P (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) x →
    Presieve.FamilyOfElements.PullbackCompatible' P
      (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) ((firstObjEqFamily P S).hom 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 : FirstObj P S
⊢ Presieve.FamilyOfElements.PullbackCompatible' P
      (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) ((firstObjEqFamily P S).hom x) →
    firstMap' P (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) x =
      secondMap' 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 : FirstObj P S
⊢ firstMap' P (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) x =
      secondMap' P (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) x →
    Presieve.FamilyOfElements.PullbackCompatible' P
      (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) ((firstObjEqFamily P S).hom x)
Tactic:
. intro t
  apply Limits.Types.limit_ext.{max u₁ v₁, u₁}
  rintro ⟨⟨Y, f, hf⟩, Z, g, hg⟩
  simpa [firstMap', secondMap'] using t hf hg
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 : FirstObj P S
⊢ firstMap' P (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) x =
      secondMap' P (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) x →
    Presieve.FamilyOfElements.PullbackCompatible' P
      (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) ((firstObjEqFamily P S).hom 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 : FirstObj P S
⊢ Presieve.FamilyOfElements.PullbackCompatible' P
      (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) ((firstObjEqFamily P S).hom x) →
    firstMap' P (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) x =
      secondMap' P (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) x
Tactic:
intro t
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 : FirstObj P S
t :
  Presieve.FamilyOfElements.PullbackCompatible' P
    (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) ((firstObjEqFamily P S).hom x)
⊢ firstMap' P (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) x =
    secondMap' P (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) 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 : FirstObj P S
t :
  Presieve.FamilyOfElements.PullbackCompatible' P
    (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) ((firstObjEqFamily P S).hom x)
⊢ firstMap' P (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) x =
    secondMap' P (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) x
Tactic:
apply Limits.Types.limit_ext.{max u₁ v₁, u₁}
State after:
case mp.w
C : Type u₁
inst✝ : Category C
X : C
S : Presieve X
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
hS : isPullbackPresieve S
x : FirstObj P S
t :
  Presieve.FamilyOfElements.PullbackCompatible' P
    (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) ((firstObjEqFamily P S).hom x)
⊢ ∀ (j : Discrete (((Y : C) × Subtype fun f {Y} {f} => S f) × (Z : C) × Subtype fun g {Y} {f} => S f)),
    limit.π
        (Discrete.functor fun fg =>
          let_fun this := (_ : HasPullback ↑fg.fst.snd ↑fg.snd.snd);
          P.obj (Limits.pullback ↑fg.fst.snd ↑fg.snd.snd).op)
        j (firstMap' P (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) x) =
      limit.π
        (Discrete.functor fun fg =>
          let_fun this := (_ : HasPullback ↑fg.fst.snd ↑fg.snd.snd);
          P.obj (Limits.pullback ↑fg.fst.snd ↑fg.snd.snd).op)
        j (secondMap' P (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) x)

State before:
case mp.w
C : Type u₁
inst✝ : Category C
X : C
S : Presieve X
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
hS : isPullbackPresieve S
x : FirstObj P S
t :
  Presieve.FamilyOfElements.PullbackCompatible' P
    (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) ((firstObjEqFamily P S).hom x)
⊢ ∀ (j : Discrete (((Y : C) × Subtype fun f {Y} {f} => S f) × (Z : C) × Subtype fun g {Y} {f} => S f)),
    limit.π
        (Discrete.functor fun fg =>
          let_fun this := (_ : HasPullback ↑fg.fst.snd ↑fg.snd.snd);
          P.obj (Limits.pullback ↑fg.fst.snd ↑fg.snd.snd).op)
        j (firstMap' P (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) x) =
      limit.π
        (Discrete.functor fun fg =>
          let_fun this := (_ : HasPullback ↑fg.fst.snd ↑fg.snd.snd);
          P.obj (Limits.pullback ↑fg.fst.snd ↑fg.snd.snd).op)
        j (secondMap' P (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) x)
Tactic:
rintro ⟨⟨Y, f, hf⟩, Z, g, hg⟩
State after:
case mp.w.mk.mk.mk.mk.mk.mk
C : Type u₁
inst✝ : Category C
X : C
S : Presieve X
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
hS : isPullbackPresieve S
x : FirstObj P S
t :
  Presieve.FamilyOfElements.PullbackCompatible' P
    (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) ((firstObjEqFamily P S).hom x)
Y : C
f : Y ⟶ X
hf : S f
Z : C
g : Z ⟶ X
hg : S g
⊢ limit.π
      (Discrete.functor fun fg =>
        let_fun this := (_ : HasPullback ↑fg.fst.snd ↑fg.snd.snd);
        P.obj (Limits.pullback ↑fg.fst.snd ↑fg.snd.snd).op)
      { as := ({ fst := Y, snd := { val := f, property := hf } }, { fst := Z, snd := { val := g, property := hg } }) }
      (firstMap' P (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) x) =
    limit.π
      (Discrete.functor fun fg =>
        let_fun this := (_ : HasPullback ↑fg.fst.snd ↑fg.snd.snd);
        P.obj (Limits.pullback ↑fg.fst.snd ↑fg.snd.snd).op)
      { as := ({ fst := Y, snd := { val := f, property := hf } }, { fst := Z, snd := { val := g, property := hg } }) }
      (secondMap' P (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) x)

State before:
case mp.w.mk.mk.mk.mk.mk.mk
C : Type u₁
inst✝ : Category C
X : C
S : Presieve X
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
hS : isPullbackPresieve S
x : FirstObj P S
t :
  Presieve.FamilyOfElements.PullbackCompatible' P
    (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) ((firstObjEqFamily P S).hom x)
Y : C
f : Y ⟶ X
hf : S f
Z : C
g : Z ⟶ X
hg : S g
⊢ limit.π
      (Discrete.functor fun fg =>
        let_fun this := (_ : HasPullback ↑fg.fst.snd ↑fg.snd.snd);
        P.obj (Limits.pullback ↑fg.fst.snd ↑fg.snd.snd).op)
      { as := ({ fst := Y, snd := { val := f, property := hf } }, { fst := Z, snd := { val := g, property := hg } }) }
      (firstMap' P (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) x) =
    limit.π
      (Discrete.functor fun fg =>
        let_fun this := (_ : HasPullback ↑fg.fst.snd ↑fg.snd.snd);
        P.obj (Limits.pullback ↑fg.fst.snd ↑fg.snd.snd).op)
      { as := ({ fst := Y, snd := { val := f, property := hf } }, { fst := Z, snd := { val := g, property := hg } }) }
      (secondMap' P (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) x)
Tactic:
simpa [firstMap', secondMap'] using t hf hg
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 : FirstObj P S
⊢ firstMap' P (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) x =
      secondMap' P (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) x →
    Presieve.FamilyOfElements.PullbackCompatible' P
      (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) ((firstObjEqFamily P S).hom x)
Tactic:
intro t Y Z f g hf hg
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 : FirstObj P S
t :
  firstMap' P (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) x =
    secondMap' P (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) x
Y Z : C
f : Y ⟶ X
g : Z ⟶ X
hf : S f
hg : S g
⊢ let_fun this := (_ : HasPullback f g);
  P.map pullback.fst.op ((firstObjEqFamily P S).hom x f hf) = P.map pullback.snd.op ((firstObjEqFamily P S).hom x g hg)

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 : FirstObj P S
t :
  firstMap' P (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) x =
    secondMap' P (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) x
Y Z : C
f : Y ⟶ X
g : Z ⟶ X
hf : S f
hg : S g
⊢ let_fun this := (_ : HasPullback f g);
  P.map pullback.fst.op ((firstObjEqFamily P S).hom x f hf) = P.map pullback.snd.op ((firstObjEqFamily P S).hom x g hg)
Tactic:
rw [Types.limit_ext_iff'] at t
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 : FirstObj P S
t :
  ∀ (j : Discrete (((Y : C) × Subtype fun f {Y} {f} => S f) × (Z : C) × Subtype fun g {Y} {f} => S f)),
    limit.π
        (Discrete.functor fun fg =>
          let_fun this := (_ : HasPullback ↑fg.fst.snd ↑fg.snd.snd);
          P.obj (Limits.pullback ↑fg.fst.snd ↑fg.snd.snd).op)
        j (firstMap' P (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) x) =
      limit.π
        (Discrete.functor fun fg =>
          let_fun this := (_ : HasPullback ↑fg.fst.snd ↑fg.snd.snd);
          P.obj (Limits.pullback ↑fg.fst.snd ↑fg.snd.snd).op)
        j (secondMap' P (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) x)
Y Z : C
f : Y ⟶ X
g : Z ⟶ X
hf : S f
hg : S g
⊢ let_fun this := (_ : HasPullback f g);
  P.map pullback.fst.op ((firstObjEqFamily P S).hom x f hf) = P.map pullback.snd.op ((firstObjEqFamily P S).hom x g hg)

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 : FirstObj P S
t :
  ∀ (j : Discrete (((Y : C) × Subtype fun f {Y} {f} => S f) × (Z : C) × Subtype fun g {Y} {f} => S f)),
    limit.π
        (Discrete.functor fun fg =>
          let_fun this := (_ : HasPullback ↑fg.fst.snd ↑fg.snd.snd);
          P.obj (Limits.pullback ↑fg.fst.snd ↑fg.snd.snd).op)
        j (firstMap' P (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) x) =
      limit.π
        (Discrete.functor fun fg =>
          let_fun this := (_ : HasPullback ↑fg.fst.snd ↑fg.snd.snd);
          P.obj (Limits.pullback ↑fg.fst.snd ↑fg.snd.snd).op)
        j (secondMap' P (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) x)
Y Z : C
f : Y ⟶ X
g : Z ⟶ X
hf : S f
hg : S g
⊢ let_fun this := (_ : HasPullback f g);
  P.map pullback.fst.op ((firstObjEqFamily P S).hom x f hf) = P.map pullback.snd.op ((firstObjEqFamily P S).hom x g hg)
Tactic:
simpa [firstMap', secondMap'] using t ⟨⟨⟨Y, f, hf⟩, Z, g, hg⟩⟩
State after:
no goals