mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.VanKampen

Goal state before:
pp: case refine_2.hd₂
C : Type u
inst✝² : Category.{v, u} C
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan fun i ↦ f i.succ
c₂ : BinaryCofan (f 0) c₁.pt
t₁ : IsVanKampenColimit c₁
t₂ : IsVanKampenColimit c₂
inst✝¹ : ∀ {Z : C} (i : Z ⟶ c₂.pt), HasPullback c₂.inr i
inst✝ : HasFiniteCoproducts C
j : Fin (n + 1)
F' : Fin (n + 1) → C
c : Cocone (Discrete.functor F')
α : Discrete.functor F' ⟶ Discrete.functor f
i : c.pt ⟶ (extendCofan c₁ c₂).pt
e : α ≫ (extendCofan c₁ c₂).ι = c.ι ≫ (const (Discrete (Fin (n + 1)))).map i
hα : NatTrans.Equifibered α
Hc : IsColimit c
⊢ ∀ {T : C} (f : F' 0 ⟶ T) (g : (∐ fun j ↦ (Discrete.functor F').obj { as := j.succ }) ⟶ T),
    (BinaryCofan.mk (c.ι.app { as := 0 }) (Sigma.desc fun b ↦ c.ι.app { as := b.succ })).inr ≫
        Hc.desc
          (Cofan.mk T fun i ↦
            Fin.cases f (fun i ↦ Sigma.ι (fun j ↦ (Discrete.functor F').obj { as := j.succ }) i ≫ g) i) =
      g

Tactic:
intro T

Goal state after:
case refine_2.hd₂
C : Type u
inst✝² : Category.{v, u} C
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan fun i ↦ f i.succ
c₂ : BinaryCofan (f 0) c₁.pt
t₁ : IsVanKampenColimit c₁
t₂ : IsVanKampenColimit c₂
inst✝¹ : ∀ {Z : C} (i : Z ⟶ c₂.pt), HasPullback c₂.inr i
inst✝ : HasFiniteCoproducts C
j : Fin (n + 1)
F' : Fin (n + 1) → C
c : Cocone (Discrete.functor F')
α : Discrete.functor F' ⟶ Discrete.functor f
i : c.pt ⟶ (extendCofan c₁ c₂).pt
e : α ≫ (extendCofan c₁ c₂).ι = c.ι ≫ (const (Discrete (Fin (n + 1)))).map i
hα : NatTrans.Equifibered α
Hc : IsColimit c
T : C
⊢ ∀ (f : F' 0 ⟶ T) (g : (∐ fun j ↦ (Discrete.functor F').obj { as := j.succ }) ⟶ T),
    (BinaryCofan.mk (c.ι.app { as := 0 }) (Sigma.desc fun b ↦ c.ι.app { as := b.succ })).inr ≫
        Hc.desc
          (Cofan.mk T fun i ↦
            Fin.cases f (fun i ↦ Sigma.ι (fun j ↦ (Discrete.functor F').obj { as := j.succ }) i ≫ g) i) =
      g
Module: Mathlib.CategoryTheory.Limits.VanKampen

Goal state before:
pp: case refine_2.uniq
C : Type u
inst✝² : Category.{v, u} C
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan fun i ↦ f i.succ
c₂ : BinaryCofan (f 0) c₁.pt
t₁ : IsVanKampenColimit c₁
t₂ : IsVanKampenColimit c₂
inst✝¹ : ∀ {Z : C} (i : Z ⟶ c₂.pt), HasPullback c₂.inr i
inst✝ : HasFiniteCoproducts C
j : Fin (n + 1)
F' : Fin (n + 1) → C
c : Cocone (Discrete.functor F')
α : Discrete.functor F' ⟶ Discrete.functor f
i : c.pt ⟶ (extendCofan c₁ c₂).pt
e : α ≫ (extendCofan c₁ c₂).ι = c.ι ≫ (const (Discrete (Fin (n + 1)))).map i
hα : NatTrans.Equifibered α
Hc : IsColimit c
⊢ ∀ {T : C} (f : F' 0 ⟶ T) (g : (∐ fun j ↦ (Discrete.functor F').obj { as := j.succ }) ⟶ T)
    (m : (BinaryCofan.mk (c.ι.app { as := 0 }) (Sigma.desc fun b ↦ c.ι.app { as := b.succ })).pt ⟶ T),
    (BinaryCofan.mk (c.ι.app { as := 0 }) (Sigma.desc fun b ↦ c.ι.app { as := b.succ })).inl ≫ m = f →
      (BinaryCofan.mk (c.ι.app { as := 0 }) (Sigma.desc fun b ↦ c.ι.app { as := b.succ })).inr ≫ m = g →
        m =
          Hc.desc
            (Cofan.mk T fun i ↦
              Fin.cases f (fun i ↦ Sigma.ι (fun j ↦ (Discrete.functor F').obj { as := j.succ }) i ≫ g) i)

Tactic:
intro T

Goal state after:
case refine_2.uniq
C : Type u
inst✝² : Category.{v, u} C
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan fun i ↦ f i.succ
c₂ : BinaryCofan (f 0) c₁.pt
t₁ : IsVanKampenColimit c₁
t₂ : IsVanKampenColimit c₂
inst✝¹ : ∀ {Z : C} (i : Z ⟶ c₂.pt), HasPullback c₂.inr i
inst✝ : HasFiniteCoproducts C
j : Fin (n + 1)
F' : Fin (n + 1) → C
c : Cocone (Discrete.functor F')
α : Discrete.functor F' ⟶ Discrete.functor f
i : c.pt ⟶ (extendCofan c₁ c₂).pt
e : α ≫ (extendCofan c₁ c₂).ι = c.ι ≫ (const (Discrete (Fin (n + 1)))).map i
hα : NatTrans.Equifibered α
Hc : IsColimit c
T : C
⊢ ∀ (f : F' 0 ⟶ T) (g : (∐ fun j ↦ (Discrete.functor F').obj { as := j.succ }) ⟶ T)
    (m : (BinaryCofan.mk (c.ι.app { as := 0 }) (Sigma.desc fun b ↦ c.ι.app { as := b.succ })).pt ⟶ T),
    (BinaryCofan.mk (c.ι.app { as := 0 }) (Sigma.desc fun b ↦ c.ι.app { as := b.succ })).inl ≫ m = f →
      (BinaryCofan.mk (c.ι.app { as := 0 }) (Sigma.desc fun b ↦ c.ι.app { as := b.succ })).inr ≫ m = g →
        m =
          Hc.desc
            (Cofan.mk T fun i ↦
              Fin.cases f (fun i ↦ Sigma.ι (fun j ↦ (Discrete.functor F').obj { as := j.succ }) i ≫ g) i)
Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
S : C
E : PreZeroHypercover S
ι : Type u_1
f : ι → E.I₀
i : (E.restrictIndex f).I₀
⊢ E.presieve₀ ((E.restrictIndex f).f i)

Tactic:
exact .mk _

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Closed

Goal state before:
pp: case mp
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
⊢ J₁ = J₂ → ∀ (P : Cᵒᵖ ⥤ Type (max v u)), Presieve.IsSheaf J₁ P ↔ Presieve.IsSheaf J₂ P

Tactic:
rintro rfl

Goal state after:
case mp
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
⊢ ∀ (P : Cᵒᵖ ⥤ Type (max v u)), Presieve.IsSheaf J₁ P ↔ Presieve.IsSheaf J₁ P
Module: Mathlib.CategoryTheory.Functor.Flat

Goal state before:
pp: C D : Type u₁
inst✝³ : SmallCategory C
inst✝² : SmallCategory D
E : Type u₂
inst✝¹ : Category.{u₁, u₂} E
F : C ⥤ D
X : D
inst✝ : ∀ (X : D), HasColimitsOfShape (CostructuredArrow F X) E
G₁ G₂ : C ⥤ E
φ : G₁ ⟶ G₂
⊢ ∀ (j : CostructuredArrow F X),
    ((Functor.LeftExtension.mk (F.leftKanExtension G₁) (F.leftKanExtensionUnit G₁)).coconeAt X).ι.app j ≫
        (F.lan ⋙ (evaluation D E).obj X).map φ ≫
          (IsColimit.coconePointUniqueUpToIso (F.isPointwiseLeftKanExtensionLeftKanExtensionUnit G₂ X)
              (colimit.isColimit (CostructuredArrow.proj F X ⋙ G₂))).hom =
      ((Functor.LeftExtension.mk (F.leftKanExtension G₁) (F.leftKanExtensionUnit G₁)).coconeAt X).ι.app j ≫
        (IsColimit.coconePointUniqueUpToIso (F.isPointwiseLeftKanExtensionLeftKanExtensionUnit G₁ X)
              (colimit.isColimit (CostructuredArrow.proj F X ⋙ G₁))).hom ≫
          ((Functor.whiskeringLeft (CostructuredArrow F X) C E).obj (CostructuredArrow.proj F X) ⋙ colim).map φ

Tactic:
intro T

Goal state after:
C D : Type u₁
inst✝³ : SmallCategory C
inst✝² : SmallCategory D
E : Type u₂
inst✝¹ : Category.{u₁, u₂} E
F : C ⥤ D
X : D
inst✝ : ∀ (X : D), HasColimitsOfShape (CostructuredArrow F X) E
G₁ G₂ : C ⥤ E
φ : G₁ ⟶ G₂
T : CostructuredArrow F X
⊢ ((Functor.LeftExtension.mk (F.leftKanExtension G₁) (F.leftKanExtensionUnit G₁)).coconeAt X).ι.app T ≫
      (F.lan ⋙ (evaluation D E).obj X).map φ ≫
        (IsColimit.coconePointUniqueUpToIso (F.isPointwiseLeftKanExtensionLeftKanExtensionUnit G₂ X)
            (colimit.isColimit (CostructuredArrow.proj F X ⋙ G₂))).hom =
    ((Functor.LeftExtension.mk (F.leftKanExtension G₁) (F.leftKanExtensionUnit G₁)).coconeAt X).ι.app T ≫
      (IsColimit.coconePointUniqueUpToIso (F.isPointwiseLeftKanExtensionLeftKanExtensionUnit G₁ X)
            (colimit.isColimit (CostructuredArrow.proj F X ⋙ G₁))).hom ≫
        ((Functor.whiskeringLeft (CostructuredArrow F X) C E).obj (CostructuredArrow.proj F X) ⋙ colim).map φ
Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : Precoverage C
inst✝ : J.RespectsIso
S : C
R T : Presieve S
hR : R ∈ J.coverings S
YR : ⦃Z : C⦄ → (g : Z ⟶ S) → R g → C
eR : ⦃Z : C⦄ → (g : Z ⟶ S) → (a : R g) → YR g a ≅ Z
hTeg : ∀ ⦃Z : C⦄ (g : Z ⟶ S) (a : R g), T ((eR g a).hom ≫ g)
YT : ⦃Z : C⦄ → (g : Z ⟶ S) → T g → C
eT : ⦃Z : C⦄ → (g : Z ⟶ S) → (a : T g) → YT g a ≅ Z
hReg : ∀ ⦃Z : C⦄ (g : Z ⟶ S) (a : T g), R ((eT g a).hom ≫ g)
⊢ T ∈ J.coverings S

Tactic:
let E : PreZeroHypercover S :=
    { I₀ := R.uncurry ⊕ T.uncurry
      X i := i.elim (fun j ↦ j.1.1) (fun j ↦ YT _ j.2)
      f i :=
        match i with
        | .inl i => by exact i.1.2
        | .inr i => by exact (eT _ i.2).hom ≫ i.1.2 }

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
J : Precoverage C
inst✝ : J.RespectsIso
S : C
R T : Presieve S
hR : R ∈ J.coverings S
YR : ⦃Z : C⦄ → (g : Z ⟶ S) → R g → C
eR : ⦃Z : C⦄ → (g : Z ⟶ S) → (a : R g) → YR g a ≅ Z
hTeg : ∀ ⦃Z : C⦄ (g : Z ⟶ S) (a : R g), T ((eR g a).hom ≫ g)
YT : ⦃Z : C⦄ → (g : Z ⟶ S) → T g → C
eT : ⦃Z : C⦄ → (g : Z ⟶ S) → (a : T g) → YT g a ≅ Z
hReg : ∀ ⦃Z : C⦄ (g : Z ⟶ S) (a : T g), R ((eT g a).hom ≫ g)
E : PreZeroHypercover S :=
  { I₀ := ↑R.uncurry ⊕ ↑T.uncurry, X := fun i ↦ Sum.elim (fun j ↦ (↑j).fst) (fun j ↦ YT (↑j).snd ⋯) i,
    f := fun i ↦
      match i with
      | Sum.inl i => (↑i).snd
      | Sum.inr i => (eT (↑i).snd ⋯).hom ≫ (↑i).snd }
⊢ T ∈ J.coverings S
Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : Precoverage C
inst✝ : J.RespectsIso
S : C
R T : Presieve S
hR : R ∈ J.coverings S
YR : ⦃Z : C⦄ → (g : Z ⟶ S) → R g → C
eR : ⦃Z : C⦄ → (g : Z ⟶ S) → (a : R g) → YR g a ≅ Z
hTeg : ∀ ⦃Z : C⦄ (g : Z ⟶ S) (a : R g), T ((eR g a).hom ≫ g)
YT : ⦃Z : C⦄ → (g : Z ⟶ S) → T g → C
eT : ⦃Z : C⦄ → (g : Z ⟶ S) → (a : T g) → YT g a ≅ Z
hReg : ∀ ⦃Z : C⦄ (g : Z ⟶ S) (a : T g), R ((eT g a).hom ≫ g)
E : PreZeroHypercover S :=
  { I₀ := ↑R.uncurry ⊕ ↑T.uncurry, X := fun i ↦ Sum.elim (fun j ↦ (↑j).fst) (fun j ↦ YT (↑j).snd ⋯) i,
    f := fun i ↦
      match i with
      | Sum.inl i => (↑i).snd
      | Sum.inr i => (eT (↑i).snd ⋯).hom ≫ (↑i).snd }
F : PreZeroHypercover S :=
  { I₀ := ↑R.uncurry ⊕ ↑T.uncurry, X := fun i ↦ Sum.elim (fun j ↦ YR (↑j).snd ⋯) (fun j ↦ (↑j).fst) i,
    f := fun i ↦
      match i with
      | Sum.inl i => (eR (↑i).snd ⋯).hom ≫ (↑i).snd
      | Sum.inr i => (↑i).snd }
e : E ≅ F :=
  PreZeroHypercover.isoMk (Equiv.refl E.I₀)
    (fun i ↦
      match i with
      | Sum.inl i => id (eR (↑i).snd ⋯).symm
      | Sum.inr i => id (eT (↑i).snd ⋯))
    ⋯
hER : E.presieve₀ = R
Y : C
i✝ : F.I₀
i : ↑R.uncurry
⊢ T (F.f (Sum.inl i))

Tactic:
apply hTeg

Goal state after:
Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck

Goal state before:
pp: case refine_1.pullback
C : Type u_2
inst✝⁴ : Category.{u_1, u_2} C
J : Precoverage C
inst✝³ : J.IsStableUnderComposition
inst✝² : J.IsStableUnderBaseChange
inst✝¹ : J.HasPullbacks
inst✝ : J.HasIsos
X✝ : C
S✝ : Sieve X✝
X : C
S : Sieve X
hS : J.Saturate X S
Y : C
f : Y ⟶ X
R : Presieve X
hR : R ∈ J.coverings X
hle : R ≤ S.arrows
this : R.HasPullbacks f
⊢ Sieve.generate (Presieve.pullbackArrows f R) ≤ Sieve.pullback f S

Tactic:
Sieve.pullbackArrows_comm

Goal state after:
case refine_1.pullback
C : Type u_2
inst✝⁴ : Category.{u_1, u_2} C
J : Precoverage C
inst✝³ : J.IsStableUnderComposition
inst✝² : J.IsStableUnderBaseChange
inst✝¹ : J.HasPullbacks
inst✝ : J.HasIsos
X✝ : C
S✝ : Sieve X✝
X : C
S : Sieve X
hS : J.Saturate X S
Y : C
f : Y ⟶ X
R : Presieve X
hR : R ∈ J.coverings X
hle : R ≤ S.arrows
this : R.HasPullbacks f
⊢ Sieve.pullback f (Sieve.generate R) ≤ Sieve.pullback f S
Module: Mathlib.CategoryTheory.Sites.CoverPreserving

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝ : RepresentablyFlat F
h : CoverPreserving J K F
⊢ F.IsContinuous J K

Tactic:
apply Functor.isContinuous_of_coverPreserving (compatiblePreservingOfFlat _ _) h

Goal state after:
Module: Mathlib.CategoryTheory.Sites.CoverPreserving

Goal state before:
pp: case refine_2
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝¹ : HasPullbacks C
inst✝ : PreservesLimitsOfShape WalkingCospan F
H : CoverPreserving J K F
U : C
E : J.OneHypercover U
i₁ i₂ : E.I₀
W : D
p₁ : W ⟶ F.obj (E.X i₁)
p₂ : W ⟶ F.obj (E.X i₂)
h : p₁ ≫ F.map (E.f i₁) = p₂ ≫ F.map (E.f i₂)
P : C := Limits.pullback (E.f i₁) (E.f i₂)
this✝ : HasPullback ((E.map F).f i₁) ((E.map F).f i₂)
this :
  (E.map F).sieve₁ (F.map (pullback.fst (E.f i₁) (E.f i₂))) (F.map (pullback.snd (E.f i₁) (E.f i₂))) ∈
    K (F.obj (Limits.pullback (E.f i₁) (E.f i₂)))
⊢ Sieve.pullback (⋯.lift p₁ p₂ h)
      ((E.map F).sieve₁ (F.map (pullback.fst (E.f i₁) (E.f i₂))) (F.map (pullback.snd (E.f i₁) (E.f i₂)))) ≤
    (E.map F).sieve₁ p₁ p₂

Tactic:
simp [PreOneHypercover.pullback_sieve₁]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.LocallyFullyFaithful

Goal state before:
pp: C : Type uC
inst✝² : Category.{vC, uC} C
D : Type uD
inst✝¹ : Category.{vD, uD} D
K : GrothendieckTopology D
G : C ⥤ D
inst✝ : G.IsLocallyFull K
ℱ : Sheaf K (Type u_2)
X Y : C
i : G.obj X ⟶ G.obj Y
s t : ℱ.obj.obj (op (G.obj X))
h :
  ∀ ⦃Z : C⦄ (j : Z ⟶ X) (f : Z ⟶ Y),
    G.map f = G.map j ≫ i →
      (ConcreteCategory.hom (ℱ.obj.map (G.map j).op)) s = (ConcreteCategory.hom (ℱ.obj.map (G.map j).op)) t
⊢ s = t

Tactic:
apply (((isSheaf_iff_isSheaf_of_type _ _).1 ℱ.property) _
    (G.functorPushforward_imageSieve_mem K i)).isSeparatedFor.ext

Goal state after:
C : Type uC
inst✝² : Category.{vC, uC} C
D : Type uD
inst✝¹ : Category.{vD, uD} D
K : GrothendieckTopology D
G : C ⥤ D
inst✝ : G.IsLocallyFull K
ℱ : Sheaf K (Type u_2)
X Y : C
i : G.obj X ⟶ G.obj Y
s t : ℱ.obj.obj (op (G.obj X))
h :
  ∀ ⦃Z : C⦄ (j : Z ⟶ X) (f : Z ⟶ Y),
    G.map f = G.map j ≫ i →
      (ConcreteCategory.hom (ℱ.obj.map (G.map j).op)) s = (ConcreteCategory.hom (ℱ.obj.map (G.map j).op)) t
⊢ ∀ ⦃Y_1 : D⦄ ⦃f : Y_1 ⟶ G.obj X⦄,
    (Sieve.functorPushforward G (G.imageSieve i)).arrows f →
      (ConcreteCategory.hom (ℱ.obj.map f.op)) s = (ConcreteCategory.hom (ℱ.obj.map f.op)) t
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: case refine_4
C : Type u
inst✝³ : Category.{v, u} C
A : Type u_1
inst✝² : Category.{v_1, u_1} A
S : C
E : PreOneHypercover S
c : Cofan E.X
hc : IsColimit c
d : Cofan E.Y'
hd : IsColimit d
F : Cᵒᵖ ⥤ A
inst✝¹ : PreservesLimit (Discrete.functor fun i ↦ op (E.X i)) F
inst✝ : PreservesLimit (Discrete.functor fun i ↦ op (E.Y' i)) F
⊢ ∀ (i : (E.sigmaOfIsColimit hc hd).multicospanShape.R),
    ((E.sigmaOfIsColimit hc hd).multicospanIndex F).fst i ≫
        (Iso.refl (((E.sigmaOfIsColimit hc hd).multicospanIndex F).right i)).hom =
      (Iso.refl
            (((E.sigmaOfIsColimit hc hd).multicospanIndex F).left
              ((E.sigmaOfIsColimit hc hd).multicospanShape.fst i))).hom ≫
        (MulticospanIndex.ofParallelHoms (E.sigmaOfIsColimit hc hd).multicospanShape
              (F.map (Cofan.IsColimit.desc hd fun x ↦ E.p₁ x.snd ≫ c.inj x.fst.1).op)
              (F.map (Cofan.IsColimit.desc hd fun x ↦ E.p₂ x.snd ≫ c.inj x.fst.2).op)).fst
          i

pp: case refine_5
C : Type u
inst✝³ : Category.{v, u} C
A : Type u_1
inst✝² : Category.{v_1, u_1} A
S : C
E : PreOneHypercover S
c : Cofan E.X
hc : IsColimit c
d : Cofan E.Y'
hd : IsColimit d
F : Cᵒᵖ ⥤ A
inst✝¹ : PreservesLimit (Discrete.functor fun i ↦ op (E.X i)) F
inst✝ : PreservesLimit (Discrete.functor fun i ↦ op (E.Y' i)) F
⊢ ∀ (i : (E.sigmaOfIsColimit hc hd).multicospanShape.R),
    ((E.sigmaOfIsColimit hc hd).multicospanIndex F).snd i ≫
        (Iso.refl (((E.sigmaOfIsColimit hc hd).multicospanIndex F).right i)).hom =
      (Iso.refl
            (((E.sigmaOfIsColimit hc hd).multicospanIndex F).left
              ((E.sigmaOfIsColimit hc hd).multicospanShape.snd i))).hom ≫
        (MulticospanIndex.ofParallelHoms (E.sigmaOfIsColimit hc hd).multicospanShape
              (F.map (Cofan.IsColimit.desc hd fun x ↦ E.p₁ x.snd ≫ c.inj x.fst.1).op)
              (F.map (Cofan.IsColimit.desc hd fun x ↦ E.p₂ x.snd ≫ c.inj x.fst.2).op)).snd
          i

pp: case refine_6
C : Type u
inst✝³ : Category.{v, u} C
A : Type u_1
inst✝² : Category.{v_1, u_1} A
S : C
E : PreOneHypercover S
c : Cofan E.X
hc : IsColimit c
d : Cofan E.Y'
hd : IsColimit d
F : Cᵒᵖ ⥤ A
inst✝¹ : PreservesLimit (Discrete.functor fun i ↦ op (E.X i)) F
inst✝ : PreservesLimit (Discrete.functor fun i ↦ op (E.Y' i)) F
⊢ ∀ (i : (E.sigmaOfIsColimit hc hd).multicospanShape.L),
    (Iso.refl ((E.sigmaOfIsColimit hc hd).multifork F).pt).hom ≫
        Multifork.ι
          ((MulticospanIndex.multiforkOfParallelHomsEquivFork (E.sigmaOfIsColimit hc hd).multicospanShape
                    (F.map (Cofan.IsColimit.desc hd fun x ↦ E.p₁ x.snd ≫ c.inj x.fst.1).op)
                    (F.map (Cofan.IsColimit.desc hd fun x ↦ E.p₂ x.snd ≫ c.inj x.fst.2).op)).symm.functor.obj
            (E.forkOfIsColimit hc hd F))
          i =
      ((E.sigmaOfIsColimit hc hd).multifork F).ι i ≫
        (Iso.refl (((E.sigmaOfIsColimit hc hd).multicospanIndex F).left i)).hom

Tactic:
all_goals cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.SheafEquiv

Goal state before:
pp: case refine_2
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type w
inst✝² : Category.{w', w} A
inst✝¹ : ∀ (X : Dᵒᵖ), Limits.HasLimitsOfShape (StructuredArrow X G.op) A
inst✝ : IsDenseSubsite J K G
Y : Sheaf J A
U : C
X : A
f : (yoneda.obj (((𝟭 (Cᵒᵖ ⥤ A)).obj Y.obj).obj (op U))).obj (op X)
l : (X Y Z : C) → (f : X ⟶ Y) → (g : G.obj Y ⟶ G.obj Z) → (G.imageSieve g).arrows f → (X ⟶ Z)
hl :
  ∀ (X Y Z : C) (f : X ⟶ Y) (g : G.obj Y ⟶ G.obj Z) (hf : (G.imageSieve g).arrows f),
    G.map (l X Y Z f g hf) = G.map f ≫ g
g₁ g₂ : StructuredArrow (op (G.obj U)) G.op
i : g₁ ⟶ g₂
⊢ ((const (StructuredArrow (op (G.obj U)) G.op)).obj X).map i ≫
      ⋯.amalgamate ⟨G.imageSieve g₂.hom.unop, ⋯⟩ (fun I ↦ f ≫ Y.obj.map (l I.Y (unop g₂.2) U I.f g₂.hom.unop ⋯).op) ⋯ =
    ⋯.amalgamate ⟨G.imageSieve g₁.hom.unop, ⋯⟩ (fun I ↦ f ≫ Y.obj.map (l I.Y (unop g₁.2) U I.f g₁.hom.unop ⋯).op) ⋯ ≫
      (StructuredArrow.proj (op (G.obj U)) G.op ⋙ Y.obj).map i

Tactic:
obtain ⟨⟨W₁⟩, ⟨g₁⟩, rfl⟩ := g₁.mk_surjective
        obtain ⟨⟨W₂⟩, ⟨g₂⟩, rfl⟩ := g₂.mk_surjective
        obtain ⟨⟨i⟩, hi, rfl⟩ := StructuredArrow.homMk_surjective i
        replace hi := Quiver.Hom.op_inj hi
        dsimp at g₁ g₂ i hi ⊢
        subst hi
        rw [Category.id_comp]
        apply Y.2.hom_ext ⟨_, IsDenseSubsite.imageSieve_mem J K G (G.map i ≫ g₁)⟩
        intro I
        simp only [Presheaf.IsSheaf.amalgamate_map, Category.assoc, ← Functor.map_comp]
        let I' : GrothendieckTopology.Cover.Arrow ⟨_, IsDenseSubsite.imageSieve_mem J K G g₁⟩ :=
          ⟨_, I.f ≫ i, ⟨l _ _ _ _ _ I.hf, by simp [hl]⟩⟩
        refine Eq.trans ?_ (Y.2.amalgamate_map _ _ _ I').symm
        apply (Y.2 X _ (IsDenseSubsite.equalizer_mem J K G (l _ _ _ _ _ I.hf)
          (l _ _ _ _ _ I'.hf) (by simp [I', hl]))).isSeparatedFor.ext
            fun V iUV (hiUV : _ = _) ↦ ?_
        simp [I', ← Functor.map_comp, ← op_comp, hiUV]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.InducedTopology

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
J : GrothendieckTopology E
⊢ F.inducedTopology (G.inducedTopology J) ≤ (F ⋙ G).inducedTopology J

Tactic:
rw [le_inducedTopology_iff]
  exact Functor.isContinuous_comp _ _ _ (G.inducedTopology J) _

Goal state after:
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
D : Type u_2
inst✝⁵ : Category.{v_2, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝⁴ : Category.{u, v} A
inst✝³ : G.LocallyCoverDense K
inst✝² : G.IsLocallyFull K
inst✝¹ : G.IsLocallyFaithful K
inst✝ : G.IsCoverDense K
⊢ IsDenseSubsite (G.inducedTopology K) K G

Tactic:
rw [← restrictedTopology_eq_inducedTopology]

Goal state after:
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
D : Type u_2
inst✝⁵ : Category.{v_2, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝⁴ : Category.{u, v} A
inst✝³ : G.LocallyCoverDense K
inst✝² : G.IsLocallyFull K
inst✝¹ : G.IsLocallyFaithful K
inst✝ : G.IsCoverDense K
⊢ IsDenseSubsite (G.restrictedTopology K) K G
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Category.{v, u} C
X : C
Y : Over X
R : Presieve Y.left
Z : Over X
g : Z ⟶ Y
W : C
p : Z.left ⟶ W
q : W ⟶ Y.left
hq : R q
hpq : p ≫ q = Over.Hom.left g
⊢ Over.Hom.left (Over.homMk p ⋯ ≫ Over.homMk q ⋯) = Over.Hom.left g

Tactic:
exact hpq

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X : C
Y : Over X
S : Sieve Y
hS : S ∈ ⇑(Sieve.overEquiv Y) ⁻¹' J Y.left
R : Sieve Y
hR : ∀ ⦃Y_1 : Over X⦄ ⦃f : Y_1 ⟶ Y⦄, S.arrows f → Sieve.pullback f R ∈ ⇑(Sieve.overEquiv Y_1) ⁻¹' J Y_1.left
Z : C
f : Z ⟶ Y.left
hf : ((Sieve.overEquiv Y) S).arrows f
⊢ Sieve.pullback f ((Sieve.overEquiv Y) R) ∈ J Z

Tactic:
by
    specialize hR ((Sieve.overEquiv_iff _ _).1 hf)
    rwa [Set.mem_preimage, Sieve.overEquiv_pullback] at hR

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Final.Type

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
P : D ⥤ Type w
inst✝ : F.Initial
t : ↑(F ⋙ P).sections
Y : D
⊢ ∀ (j₁ j₂ : CostructuredArrow F Y) (x : j₁ ⟶ j₂),
    (ConcreteCategory.hom (P.map j₁.hom)) (↑t j₁.left) = (ConcreteCategory.hom (P.map j₂.hom)) (↑t j₂.left)

Tactic:
intro Z₁ Z₂ φ

Goal state after:
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
P : D ⥤ Type w
inst✝ : F.Initial
t : ↑(F ⋙ P).sections
Y : D
Z₁ Z₂ : CostructuredArrow F Y
φ : Z₁ ⟶ Z₂
⊢ (ConcreteCategory.hom (P.map Z₁.hom)) (↑t Z₁.left) = (ConcreteCategory.hom (P.map Z₂.hom)) (↑t Z₂.left)
Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackFree

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : GrothendieckTopology C
K : GrothendieckTopology D
F : C ⥤ D
S : Sheaf J RingCat
R : Sheaf K RingCat
inst✝ : F.IsContinuous J K
φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R
X : Cᵒᵖ
r : ↑(S.obj.obj X)
⊢ (forget₂ RingCat AddCommGrpCat).map (φ.hom.app X) ≫ (((pushforward φ).obj (unit R)).val.obj X).smul r =
    ((unit S).val.obj X).smul r ≫ (forget₂ RingCat AddCommGrpCat).map (φ.hom.app X)

Tactic:
ext m

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : GrothendieckTopology C
K : GrothendieckTopology D
F : C ⥤ D
S : Sheaf J RingCat
R : Sheaf K RingCat
inst✝ : F.IsContinuous J K
φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R
X : Cᵒᵖ
r : ↑(S.obj.obj X)
m : ↑((forget₂ (ModuleCat ↑(S.obj.obj X)) AddCommGrpCat).obj ((unit S).val.obj X))
⊢ (AddCommGrpCat.Hom.hom
        ((forget₂ RingCat AddCommGrpCat).map (φ.hom.app X) ≫ (((pushforward φ).obj (unit R)).val.obj X).smul r))
      m =
    (AddCommGrpCat.Hom.hom (((unit S).val.obj X).smul r ≫ (forget₂ RingCat AddCommGrpCat).map (φ.hom.app X))) m
Module: Mathlib.CategoryTheory.Simple

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : Simple Y
i : X ≅ Y
Y✝ : C
f : Y✝ ⟶ X
m : Mono f
h : f ≠ 0
⊢ IsIso (f ≫ i.hom)

Tactic:
apply isIso_of_mono_of_nonzero

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : Simple Y
i : X ≅ Y
Y✝ : C
f : Y✝ ⟶ X
m : Mono f
h : f ≠ 0
⊢ f ≫ i.hom ≠ 0
Module: Mathlib.CategoryTheory.Limits.Lattice

Goal state before:
pp: α : Type u
inst✝¹ : CompleteLattice α
J : Type w
inst✝ : Category.{w', w} J
F : J ⥤ α
s : Cocone F
⊢ ∀ b ∈ Set.range F.obj, b ≤ s.pt

Tactic:
rintro _ ⟨j, rfl⟩; exact (s.ι.app j).le

Goal state after: