Theorem: CategoryTheory.Equalizer.Presieve.sheaf_condition' (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
⊢ 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]
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

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]
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

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]
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

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
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)

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 _
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

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
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

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
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

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]
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

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
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

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
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

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
q : Presieve.FamilyOfElements.IsAmalgamation x t
⊢ ↑(firstObjEqFamily P S).toEquiv (forkMap P (fun {Y} {f} => S f) t) = x
Tactic:
funext Y f hf
State after:
case H.h.mp.h.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
q : Presieve.FamilyOfElements.IsAmalgamation x t
Y : C
f : Y ⟶ X
hf : S f
⊢ ↑(firstObjEqFamily P S).toEquiv (forkMap P (fun {Y} {f} => S f) t) f hf = x f hf

State before:
case H.h.mp.h.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
q : Presieve.FamilyOfElements.IsAmalgamation x t
Y : C
f : Y ⟶ X
hf : S f
⊢ ↑(firstObjEqFamily P S).toEquiv (forkMap P (fun {Y} {f} => S f) t) f hf = x f hf
Tactic:
simpa [forkMap] using q _ _
State after:
no goals

State before:
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
Tactic:
intro q Y f hf
State after:
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
q : ↑(firstObjEqFamily P S).toEquiv (forkMap P (fun {Y} {f} => S f) t) = x
Y : C
f : Y ⟶ X
hf : S f
⊢ P.map f.op t = x f hf

State before:
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
q : ↑(firstObjEqFamily P S).toEquiv (forkMap P (fun {Y} {f} => S f) t) = x
Y : C
f : Y ⟶ X
hf : S f
⊢ P.map f.op t = x f hf
Tactic:
rw [← q]
State after:
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
q : ↑(firstObjEqFamily P S).toEquiv (forkMap P (fun {Y} {f} => S f) t) = x
Y : C
f : Y ⟶ X
hf : S f
⊢ P.map f.op t = ↑(firstObjEqFamily P S).toEquiv (forkMap P (fun {Y} {f} => S f) t) f hf

State before:
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
q : ↑(firstObjEqFamily P S).toEquiv (forkMap P (fun {Y} {f} => S f) t) = x
Y : C
f : Y ⟶ X
hf : S f
⊢ P.map f.op t = ↑(firstObjEqFamily P S).toEquiv (forkMap P (fun {Y} {f} => S f) t) f hf
Tactic:
simp [forkMap]
State after:
no goals