internlm/Lean-Github huggingface dataset:
Theorem: CategoryTheory.Equalizer.Presieve.w'
Proof 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
Proof state after:
no goals
Theorem: CategoryTheory.Equalizer.Presieve.compatible_iff'
Proof 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]
Proof 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
Theorem: CategoryTheory.Equalizer.Presieve.compatible_iff'
Proof 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
Proof 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)
Theorem: CategoryTheory.Equalizer.Presieve.compatible_iff'
Proof 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
Proof 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)
Theorem: CategoryTheory.Equalizer.Presieve.compatible_iff'
Proof 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
Proof 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
Theorem: CategoryTheory.Equalizer.Presieve.compatible_iff'
Proof 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₁}
Proof 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)
Theorem: CategoryTheory.Equalizer.Presieve.compatible_iff'
Proof 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⟩
Proof 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)
Theorem: CategoryTheory.Equalizer.Presieve.compatible_iff'
Proof 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
Proof state after:
no goals
Theorem: CategoryTheory.Equalizer.Presieve.compatible_iff'
Proof 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
Proof 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)
Theorem: CategoryTheory.Equalizer.Presieve.compatible_iff'
Proof 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
Proof 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)
Theorem: CategoryTheory.Equalizer.Presieve.compatible_iff'
Proof 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⟩⟩
Proof state after:
no goals
Theorem: CategoryTheory.Equalizer.Presieve.sheaf_condition'
Proof state before:
C : Type u₁
inst✝ : Category C
X : C
S : Presieve X
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
hS : isPullbackPresieve S
⊢ Presieve.IsSheafFor P S ↔
    Nonempty
      (IsLimit
        (Fork.ofι (forkMap P fun {Y} {f} => S f)
          (_ :
            (forkMap P fun {Y} {f} => S f) ≫
                firstMap' P (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) =
              (forkMap P fun {Y} {f} => S f) ≫
                secondMap' P (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g))))
Tactic:
rw [Types.type_equalizer_iff_unique]
Proof state after:
C : Type u₁
inst✝ : Category C
X : C
S : Presieve X
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
hS : isPullbackPresieve S
⊢ Presieve.IsSheafFor P S ↔
    ∀ (y : FirstObj P fun {Y} {f} => S f),
      firstMap' P (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) y =
          secondMap' P (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) y →
        ∃! x, forkMap P (fun {Y} {f} => S f) x = y
Theorem: CategoryTheory.Equalizer.Presieve.sheaf_condition'
Proof state before:
C : Type u₁
inst✝ : Category C
X : C
S : Presieve X
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
hS : isPullbackPresieve S
⊢ Presieve.IsSheafFor P S ↔
    ∀ (y : FirstObj P fun {Y} {f} => S f),
      firstMap' P (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) y =
          secondMap' P (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) y →
        ∃! x, forkMap P (fun {Y} {f} => S f) x = y
Tactic:
erw [← Equiv.forall_congr_left (firstObjEqFamily P S).toEquiv.symm]
Proof state after:
C : Type u₁
inst✝ : Category C
X : C
S : Presieve X
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
hS : isPullbackPresieve S
⊢ Presieve.IsSheafFor P S ↔
    ∀ (x : Presieve.FamilyOfElements P S),
      firstMap' P (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g)
            (↑(firstObjEqFamily P S).symm x) =
          secondMap' P (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g)
            (↑(firstObjEqFamily P S).symm x) →
        ∃! x_1, forkMap P (fun {Y} {f} => S f) x_1 = ↑(firstObjEqFamily P S).symm x
Theorem: CategoryTheory.Equalizer.Presieve.sheaf_condition'
Proof state before:
C : Type u₁
inst✝ : Category C
X : C
S : Presieve X
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
hS : isPullbackPresieve S
⊢ Presieve.IsSheafFor P S ↔
    ∀ (x : Presieve.FamilyOfElements P S),
      firstMap' P (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g)
            (↑(firstObjEqFamily P S).symm x) =
          secondMap' P (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g)
            (↑(firstObjEqFamily P S).symm x) →
        ∃! x_1, forkMap P (fun {Y} {f} => S f) x_1 = ↑(firstObjEqFamily P S).symm x
Tactic:
simp_rw [← compatible_iff', ← Iso.toEquiv_fun, Equiv.apply_symm_apply]
Proof state after:
C : Type u₁
inst✝ : Category C
X : C
S : Presieve X
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
hS : isPullbackPresieve S
⊢ Presieve.IsSheafFor P S ↔
    ∀ (x : Presieve.FamilyOfElements P S),
      Presieve.FamilyOfElements.Compatible x →
        ∃! x_1, forkMap P (fun {Y} {f} => S f) x_1 = ↑(firstObjEqFamily P S).symm x
Theorem: CategoryTheory.Equalizer.Presieve.sheaf_condition'
Proof state before:
C : Type u₁
inst✝ : Category C
X : C
S : Presieve X
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
hS : isPullbackPresieve S
⊢ Presieve.IsSheafFor P S ↔
    ∀ (x : Presieve.FamilyOfElements P S),
      Presieve.FamilyOfElements.Compatible x →
        ∃! x_1, forkMap P (fun {Y} {f} => S f) x_1 = ↑(firstObjEqFamily P S).symm x
Tactic:
apply ball_congr
Proof state after:
case H
C : Type u₁
inst✝ : Category C
X : C
S : Presieve X
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
hS : isPullbackPresieve S
⊢ ∀ (x : Presieve.FamilyOfElements P S),
    Presieve.FamilyOfElements.Compatible x →
      ((∃! t, Presieve.FamilyOfElements.IsAmalgamation x t) ↔
        ∃! x_1, forkMap P (fun {Y} {f} => S f) x_1 = ↑(firstObjEqFamily P S).symm x)
Theorem: CategoryTheory.Equalizer.Presieve.sheaf_condition'
Proof state before:
case H
C : Type u₁
inst✝ : Category C
X : C
S : Presieve X
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
hS : isPullbackPresieve S
⊢ ∀ (x : Presieve.FamilyOfElements P S),
    Presieve.FamilyOfElements.Compatible x →
      ((∃! t, Presieve.FamilyOfElements.IsAmalgamation x t) ↔
        ∃! x_1, forkMap P (fun {Y} {f} => S f) x_1 = ↑(firstObjEqFamily P S).symm x)
Tactic:
intro x _
Proof state after:
case H
C : Type u₁
inst✝ : Category C
X : C
S : Presieve X
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
hS : isPullbackPresieve S
x : Presieve.FamilyOfElements P S
h✝ : Presieve.FamilyOfElements.Compatible x
⊢ (∃! t, Presieve.FamilyOfElements.IsAmalgamation x t) ↔
    ∃! x_1, forkMap P (fun {Y} {f} => S f) x_1 = ↑(firstObjEqFamily P S).symm x
Theorem: CategoryTheory.Equalizer.Presieve.sheaf_condition'
Proof state before:
case H
C : Type u₁
inst✝ : Category C
X : C
S : Presieve X
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
hS : isPullbackPresieve S
x : Presieve.FamilyOfElements P S
h✝ : Presieve.FamilyOfElements.Compatible x
⊢ (∃! t, Presieve.FamilyOfElements.IsAmalgamation x t) ↔
    ∃! x_1, forkMap P (fun {Y} {f} => S f) x_1 = ↑(firstObjEqFamily P S).symm x
Tactic:
apply exists_unique_congr
Proof 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
x : Presieve.FamilyOfElements P S
h✝ : Presieve.FamilyOfElements.Compatible x
⊢ ∀ (a : P.obj X.op),
    Presieve.FamilyOfElements.IsAmalgamation x a ↔ forkMap P (fun {Y} {f} => S f) a = ↑(firstObjEqFamily P S).symm x
Theorem: CategoryTheory.Equalizer.Presieve.sheaf_condition'
Proof 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
x : Presieve.FamilyOfElements P S
h✝ : Presieve.FamilyOfElements.Compatible x
⊢ ∀ (a : P.obj X.op),
    Presieve.FamilyOfElements.IsAmalgamation x a ↔ forkMap P (fun {Y} {f} => S f) a = ↑(firstObjEqFamily P S).symm x
Tactic:
intro t
Proof 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
x : Presieve.FamilyOfElements P S
h✝ : Presieve.FamilyOfElements.Compatible x
t : P.obj X.op
⊢ Presieve.FamilyOfElements.IsAmalgamation x t ↔ forkMap P (fun {Y} {f} => S f) t = ↑(firstObjEqFamily P S).symm x
Theorem: CategoryTheory.Equalizer.Presieve.sheaf_condition'
Proof 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
x : Presieve.FamilyOfElements P S
h✝ : Presieve.FamilyOfElements.Compatible x
t : P.obj X.op
⊢ Presieve.FamilyOfElements.IsAmalgamation x t ↔ forkMap P (fun {Y} {f} => S f) t = ↑(firstObjEqFamily P S).symm x
Tactic:
rw [Equiv.eq_symm_apply]
Proof 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
x : Presieve.FamilyOfElements P S
h✝ : Presieve.FamilyOfElements.Compatible x
t : P.obj X.op
⊢ Presieve.FamilyOfElements.IsAmalgamation x t ↔ ↑(firstObjEqFamily P S).toEquiv (forkMap P (fun {Y} {f} => S f) t) = x
Theorem: CategoryTheory.Equalizer.Presieve.sheaf_condition'
Proof 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
x : Presieve.FamilyOfElements P S
h✝ : Presieve.FamilyOfElements.Compatible x
t : P.obj X.op
⊢ Presieve.FamilyOfElements.IsAmalgamation x t ↔ ↑(firstObjEqFamily P S).toEquiv (forkMap P (fun {Y} {f} => S f) t) = x
Tactic:
constructor
Proof state after:
case H.h.mp
C : Type u₁
inst✝ : Category C
X : C
S : Presieve X
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
hS : isPullbackPresieve S
x : Presieve.FamilyOfElements P S
h✝ : Presieve.FamilyOfElements.Compatible x
t : P.obj X.op
⊢ Presieve.FamilyOfElements.IsAmalgamation x t → ↑(firstObjEqFamily P S).toEquiv (forkMap P (fun {Y} {f} => S f) t) = x

case H.h.mpr
C : Type u₁
inst✝ : Category C
X : C
S : Presieve X
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
hS : isPullbackPresieve S
x : Presieve.FamilyOfElements P S
h✝ : Presieve.FamilyOfElements.Compatible x
t : P.obj X.op
⊢ ↑(firstObjEqFamily P S).toEquiv (forkMap P (fun {Y} {f} => S f) t) = x → Presieve.FamilyOfElements.IsAmalgamation x t
Theorem: CategoryTheory.Equalizer.Presieve.sheaf_condition'
Proof state before:
case H.h.mp
C : Type u₁
inst✝ : Category C
X : C
S : Presieve X
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
hS : isPullbackPresieve S
x : Presieve.FamilyOfElements P S
h✝ : Presieve.FamilyOfElements.Compatible x
t : P.obj X.op
⊢ Presieve.FamilyOfElements.IsAmalgamation x t → ↑(firstObjEqFamily P S).toEquiv (forkMap P (fun {Y} {f} => S f) t) = x
Tactic:
intro q
Proof state after:
case H.h.mp
C : Type u₁
inst✝ : Category C
X : C
S : Presieve X
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
hS : isPullbackPresieve S
x : Presieve.FamilyOfElements P S
h✝ : Presieve.FamilyOfElements.Compatible x
t : P.obj X.op
q : Presieve.FamilyOfElements.IsAmalgamation x t
⊢ ↑(firstObjEqFamily P S).toEquiv (forkMap P (fun {Y} {f} => S f) t) = x