Theorem: CategoryTheory.isSheafForExtensiveSieve (Sieves/ExtensiveRegular.lean)

State before:
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
hS : S ∈ ExtensiveSieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
⊢ Presieve.IsSheafFor F S
Tactic:
refine' (Equalizer.Presieve.sheaf_condition' F <| isPullbackSieve_ExtensiveSieve hS).2 _
State after:
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
hS : S ∈ ExtensiveSieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
⊢ Nonempty
    (IsLimit
      (Fork.ofι (Equalizer.forkMap F fun {Y} {f} => S f)
        (_ :
          (Equalizer.forkMap F fun {Y} {f} => S f) ≫
              Equalizer.Presieve.firstMap' F (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) =
            (Equalizer.forkMap F fun {Y} {f} => S f) ≫
              Equalizer.Presieve.secondMap' F
                (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g))))

State before:
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
hS : S ∈ ExtensiveSieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
⊢ Nonempty
    (IsLimit
      (Fork.ofι (Equalizer.forkMap F fun {Y} {f} => S f)
        (_ :
          (Equalizer.forkMap F fun {Y} {f} => S f) ≫
              Equalizer.Presieve.firstMap' F (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) =
            (Equalizer.forkMap F fun {Y} {f} => S f) ≫
              Equalizer.Presieve.secondMap' F
                (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g))))
Tactic:
rw [Limits.Types.type_equalizer_iff_unique]
State after:
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
hS : S ∈ ExtensiveSieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
⊢ ∀ (y : Equalizer.FirstObj F fun {Y} {f} => S f),
    Equalizer.Presieve.firstMap' F (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) y =
        Equalizer.Presieve.secondMap' F (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) y →
      ∃! x, Equalizer.forkMap F (fun {Y} {f} => S f) x = y

State before:
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
hS : S ∈ ExtensiveSieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
⊢ ∀ (y : Equalizer.FirstObj F fun {Y} {f} => S f),
    Equalizer.Presieve.firstMap' F (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) y =
        Equalizer.Presieve.secondMap' F (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) y →
      ∃! x, Equalizer.forkMap F (fun {Y} {f} => S f) x = y
Tactic:
dsimp [Equalizer.FirstObj]
State after:
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
hS : S ∈ ExtensiveSieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
⊢ ∀ (y : ∏ fun f => F.obj f.fst.op),
    Equalizer.Presieve.firstMap' F (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) y =
        Equalizer.Presieve.secondMap' F (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) y →
      ∃! x, Equalizer.forkMap F (fun {Y} {f} => S f) x = y

State before:
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
hS : S ∈ ExtensiveSieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
⊢ IsIso (Equalizer.forkMap F S)
Tactic:
exact isSheafForDagurSieveIsIsoFork hS hF
State after:
no goals

State before:
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
hS : S ∈ ExtensiveSieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
this : IsIso (Equalizer.forkMap F S)
⊢ ∀ (y : ∏ fun f => F.obj f.fst.op),
    Equalizer.Presieve.firstMap' F (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) y =
        Equalizer.Presieve.secondMap' F (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) y →
      ∃! x, Equalizer.forkMap F (fun {Y} {f} => S f) x = y
Tactic:
intro y _
State after:
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
hS : S ∈ ExtensiveSieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
this : IsIso (Equalizer.forkMap F S)
y : ∏ fun f => F.obj f.fst.op
a✝ :
  Equalizer.Presieve.firstMap' F (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) y =
    Equalizer.Presieve.secondMap' F (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) y
⊢ ∃! x, Equalizer.forkMap F (fun {Y} {f} => S f) x = y

State before:
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
hS : S ∈ ExtensiveSieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
this : IsIso (Equalizer.forkMap F S)
y : ∏ fun f => F.obj f.fst.op
a✝ :
  Equalizer.Presieve.firstMap' F (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) y =
    Equalizer.Presieve.secondMap' F (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) y
⊢ ∃! x, Equalizer.forkMap F (fun {Y} {f} => S f) x = y
Tactic:
refine' ⟨inv (Equalizer.forkMap F S) y, _, fun y₁ hy₁ => _⟩
State after:
case refine'_1
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
hS : S ∈ ExtensiveSieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
this : IsIso (Equalizer.forkMap F S)
y : ∏ fun f => F.obj f.fst.op
a✝ :
  Equalizer.Presieve.firstMap' F (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) y =
    Equalizer.Presieve.secondMap' F (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) y
⊢ (fun x => Equalizer.forkMap F (fun {Y} {f} => S f) x = y) (inv (Equalizer.forkMap F S) y)

case refine'_2
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
hS : S ∈ ExtensiveSieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
this : IsIso (Equalizer.forkMap F S)
y : ∏ fun f => F.obj f.fst.op
a✝ :
  Equalizer.Presieve.firstMap' F (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) y =
    Equalizer.Presieve.secondMap' F (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) y
y₁ : F.obj X.op
hy₁ : (fun x => Equalizer.forkMap F (fun {Y} {f} => S f) x = y) y₁
⊢ y₁ = inv (Equalizer.forkMap F S) y

State before:
case refine'_1
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
hS : S ∈ ExtensiveSieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
this : IsIso (Equalizer.forkMap F S)
y : ∏ fun f => F.obj f.fst.op
a✝ :
  Equalizer.Presieve.firstMap' F (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) y =
    Equalizer.Presieve.secondMap' F (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) y
⊢ (fun x => Equalizer.forkMap F (fun {Y} {f} => S f) x = y) (inv (Equalizer.forkMap F S) y)
Tactic:
change (inv (Equalizer.forkMap F S) ≫ (Equalizer.forkMap F S)) y = y
State after:
case refine'_1
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
hS : S ∈ ExtensiveSieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
this : IsIso (Equalizer.forkMap F S)
y : ∏ fun f => F.obj f.fst.op
a✝ :
  Equalizer.Presieve.firstMap' F (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) y =
    Equalizer.Presieve.secondMap' F (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) y
⊢ (inv (Equalizer.forkMap F S) ≫ Equalizer.forkMap F S) y = y

State before:
case refine'_1
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
hS : S ∈ ExtensiveSieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
this : IsIso (Equalizer.forkMap F S)
y : ∏ fun f => F.obj f.fst.op
a✝ :
  Equalizer.Presieve.firstMap' F (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) y =
    Equalizer.Presieve.secondMap' F (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) y
⊢ (inv (Equalizer.forkMap F S) ≫ Equalizer.forkMap F S) y = y
Tactic:
rw [IsIso.inv_hom_id, types_id_apply]
State after:
no goals

State before:
case refine'_2
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
hS : S ∈ ExtensiveSieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
this : IsIso (Equalizer.forkMap F S)
y : ∏ fun f => F.obj f.fst.op
a✝ :
  Equalizer.Presieve.firstMap' F (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) y =
    Equalizer.Presieve.secondMap' F (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) y
y₁ : F.obj X.op
hy₁ : (fun x => Equalizer.forkMap F (fun {Y} {f} => S f) x = y) y₁
⊢ y₁ = inv (Equalizer.forkMap F S) y
Tactic:
replace hy₁ := congr_arg (inv (Equalizer.forkMap F S)) hy₁
State after:
case refine'_2
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
hS : S ∈ ExtensiveSieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
this : IsIso (Equalizer.forkMap F S)
y : ∏ fun f => F.obj f.fst.op
a✝ :
  Equalizer.Presieve.firstMap' F (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) y =
    Equalizer.Presieve.secondMap' F (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) y
y₁ : F.obj X.op
hy₁ : inv (Equalizer.forkMap F S) (Equalizer.forkMap F (fun {Y} {f} => S f) y₁) = inv (Equalizer.forkMap F S) y
⊢ y₁ = inv (Equalizer.forkMap F S) y

State before:
case refine'_2
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
hS : S ∈ ExtensiveSieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
this : IsIso (Equalizer.forkMap F S)
y : ∏ fun f => F.obj f.fst.op
a✝ :
  Equalizer.Presieve.firstMap' F (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) y =
    Equalizer.Presieve.secondMap' F (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) y
y₁ : F.obj X.op
hy₁ : inv (Equalizer.forkMap F S) (Equalizer.forkMap F (fun {Y} {f} => S f) y₁) = inv (Equalizer.forkMap F S) y
⊢ y₁ = inv (Equalizer.forkMap F S) y
Tactic:
change ((Equalizer.forkMap F S) ≫ inv (Equalizer.forkMap F S)) _ = _ at hy₁
State after:
case refine'_2
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
hS : S ∈ ExtensiveSieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
this : IsIso (Equalizer.forkMap F S)
y : ∏ fun f => F.obj f.fst.op
a✝ :
  Equalizer.Presieve.firstMap' F (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) y =
    Equalizer.Presieve.secondMap' F (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) y
y₁ : F.obj X.op
hy₁ : (Equalizer.forkMap F S ≫ inv (Equalizer.forkMap F S)) y₁ = inv (Equalizer.forkMap F S) y
⊢ y₁ = inv (Equalizer.forkMap F S) y

State before:
case refine'_2
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
hS : S ∈ ExtensiveSieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
this : IsIso (Equalizer.forkMap F S)
y : ∏ fun f => F.obj f.fst.op
a✝ :
  Equalizer.Presieve.firstMap' F (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) y =
    Equalizer.Presieve.secondMap' F (_ : ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g) y
y₁ : F.obj X.op
hy₁ : (Equalizer.forkMap F S ≫ inv (Equalizer.forkMap F S)) y₁ = inv (Equalizer.forkMap F S) y
⊢ y₁ = inv (Equalizer.forkMap F S) y
Tactic:
rwa [IsIso.hom_inv_id, types_id_apply] at hy₁
State after:
no goals