mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck

Goal state before:
pp: case h
C : Type u_3
inst✝ : Category.{u_2, u_3} C
J : Precoverage C
P : Cᵒᵖ ⥤ Type u_1
X✝ : C
S✝ : Sieve X✝
X : C
R S : Sieve X
hS : J.Saturate X R
h✝ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → J.Saturate Y (Sieve.pullback f S)
Y : C
f : Y ⟶ X
H :
  ∀ {X Y : C} {f : Y ⟶ X},
    ∀ R ∈ J.coverings X,
      Presieve.IsSeparatedFor P (Sieve.pullback f (Sieve.generate R)).arrows ∧
        ∀ (x : Presieve.FamilyOfElements P (Sieve.pullback f (Sieve.generate R)).arrows),
          x.Compatible → ∃ t, x.IsAmalgamation t
H1 : ∀ ⦃Y : C⦄ (f : Y ⟶ X), Presieve.IsSeparatedFor P (Sieve.pullback f R).arrows
H1' :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (x : Presieve.FamilyOfElements P (Sieve.pullback f R).arrows),
    x.Compatible → ∃ t, x.IsAmalgamation t
H2 :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f → ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y), Presieve.IsSeparatedFor P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows
H2' :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f →
      ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y) (x : Presieve.FamilyOfElements P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows),
        x.Compatible → ∃ t, x.IsAmalgamation t
x : Presieve.FamilyOfElements P (Sieve.pullback f S).arrows
hx : x.Compatible
y : ⦃Z : C⦄ → (g : Z ⟶ Y) → Presieve.FamilyOfElements P (Sieve.pullback (𝟙 Z) (Sieve.pullback (g ≫ f) S)).arrows :=
  fun Z g ZZ gg hgg ↦ x (gg ≫ g) ⋯
hy : ∀ ⦃Z : C⦄ (g : Z ⟶ Y), (y g).Compatible
z : ⦃Z : C⦄ → ⦃g : Z ⟶ Y⦄ → (Sieve.pullback f R).arrows g → P.obj (Opposite.op Z)
hz : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ Y⦄ (hg : (Sieve.pullback f R).arrows g), (y g).IsAmalgamation (z hg)
q : Presieve.FamilyOfElements P (Sieve.pullback f R).arrows := fun Z g hg ↦ z hg
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ Y
f₂ : Y₂ ⟶ Y
h₁ : (Sieve.pullback f R).arrows f₁
h₂ : (Sieve.pullback f R).arrows f₂
h : g₁ ≫ f₁ = g₂ ≫ f₂
ZZ : C
gg : ZZ ⟶ Z
hgg : (Sieve.pullback g₁ (Sieve.pullback (f₁ ≫ f) S)).arrows gg
⊢ (Sieve.pullback (𝟙 Y₂) (Sieve.pullback (f₂ ≫ f) S)).arrows (gg ≫ g₂)

Tactic:
simpa [reassoc_of% h] using hgg

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: 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
⊢ ∀ (i : E.I₁'),
    d.inj i ≫ (Cofan.IsColimit.desc hd fun x ↦ E.p₁ x.snd ≫ c.inj x.fst.1) ≫ Cofan.IsColimit.desc hc E.f =
      d.inj i ≫ (Cofan.IsColimit.desc hd fun x ↦ E.p₂ x.snd ≫ c.inj x.fst.2) ≫ Cofan.IsColimit.desc hc E.f

Tactic:
by simp [E.w]

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

Goal state before:
pp: 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
A : Type w
inst✝¹ : Category.{w', w} A
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝ : G.IsCocontinuous J K
F : Cᵒᵖ ⥤ A
hF : Presheaf.IsSheaf J F
R : Dᵒᵖ ⥤ A
α : G.op ⋙ R ⟶ F
hR : (Functor.RightExtension.mk R α).IsPointwiseRightKanExtension
X : D
S : K.Cover X
s : Multifork (S.index R)
i : S.Arrow
j : StructuredArrow (op i.Y) G.op
eq : lift hF hR s ≫ R.map i.f.op ≫ R.map j.hom ≫ α.app j.right = liftAux hF α s (j.hom.unop ≫ i.f)
⊢ lift hF hR s ≫ R.map i.f.op ≫ R.map j.hom ≫ α.app j.right = s.ι i ≫ R.map j.hom ≫ α.app j.right

Tactic:
eq

Goal state after:
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
A : Type w
inst✝¹ : Category.{w', w} A
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝ : G.IsCocontinuous J K
F : Cᵒᵖ ⥤ A
hF : Presheaf.IsSheaf J F
R : Dᵒᵖ ⥤ A
α : G.op ⋙ R ⟶ F
hR : (Functor.RightExtension.mk R α).IsPointwiseRightKanExtension
X : D
S : K.Cover X
s : Multifork (S.index R)
i : S.Arrow
j : StructuredArrow (op i.Y) G.op
eq : lift hF hR s ≫ R.map i.f.op ≫ R.map j.hom ≫ α.app j.right = liftAux hF α s (j.hom.unop ≫ i.f)
⊢ liftAux hF α s (j.hom.unop ≫ i.f) = s.ι i ≫ R.map j.hom ≫ α.app j.right
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: 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
x✝² x✝¹ : (E.sigmaOfIsColimit hc).I₀
x✝ : PUnit.{w + 1}
⊢ ∀ (i : E.I₁'),
    d.inj i ≫ (Cofan.IsColimit.desc hd fun i ↦ E.p₁ i.snd ≫ c.inj i.fst.1) ≫ (E.sigmaOfIsColimit hc).f x✝² =
      d.inj i ≫ (Cofan.IsColimit.desc hd fun i ↦ E.p₂ i.snd ≫ c.inj i.fst.2) ≫ (E.sigmaOfIsColimit hc).f x✝¹

Tactic:
by simp [E.w]

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

Goal state before:
pp: 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
A : Type w
inst✝⁵ : Category.{w', w} A
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝⁴ : G.IsCocontinuous J K
inst✝³ : ∀ (F : Cᵒᵖ ⥤ A), G.op.HasPointwiseRightKanExtension F
inst✝² : G.IsContinuous J K
inst✝¹ : HasWeakSheafify J A
inst✝ : HasWeakSheafify K A
F : Dᵒᵖ ⥤ A
adj₁ : (whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op ⊣ G.op.ran := G.op.ranAdjunction A
adj₂ : presheafToSheaf J A ⊣ sheafToPresheaf J A := sheafificationAdjunction J A
adj₃ : presheafToSheaf K A ⊣ sheafToPresheaf K A := sheafificationAdjunction K A
adj₄ : G.sheafPushforwardContinuous A J K ⊣ G.sheafPushforwardCocontinuous A J K := G.sheafAdjunctionCocontinuous A J K
eq :
  adj₁.unit.app F ≫
      G.op.ran.map (adj₂.unit.app (((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj F)) ≫
        G.op.ran.map ((sheafToPresheaf J A).map (((adj₁.comp adj₂).leftAdjointUniq (adj₃.comp adj₄)).hom.app F)) =
    adj₃.unit.app F ≫ (sheafToPresheaf K A).map (adj₄.unit.app ((presheafToSheaf K A).obj F))
⊢ adj₁.unit.app F ≫
      G.op.ran.map (adj₂.unit.app (((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj F)) ≫
        G.op.ran.map ((sheafToPresheaf J A).map (((adj₁.comp adj₂).leftAdjointUniq (adj₃.comp adj₄)).hom.app F)) =
    (adj₁.homEquiv F ((sheafToPresheaf J A).obj ((presheafToSheaf K A ⋙ G.sheafPushforwardContinuous A J K).obj F)))
      (((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).map (adj₃.unit.app F))

Tactic:
eq

Goal state after:
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
A : Type w
inst✝⁵ : Category.{w', w} A
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝⁴ : G.IsCocontinuous J K
inst✝³ : ∀ (F : Cᵒᵖ ⥤ A), G.op.HasPointwiseRightKanExtension F
inst✝² : G.IsContinuous J K
inst✝¹ : HasWeakSheafify J A
inst✝ : HasWeakSheafify K A
F : Dᵒᵖ ⥤ A
adj₁ : (whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op ⊣ G.op.ran := G.op.ranAdjunction A
adj₂ : presheafToSheaf J A ⊣ sheafToPresheaf J A := sheafificationAdjunction J A
adj₃ : presheafToSheaf K A ⊣ sheafToPresheaf K A := sheafificationAdjunction K A
adj₄ : G.sheafPushforwardContinuous A J K ⊣ G.sheafPushforwardCocontinuous A J K := G.sheafAdjunctionCocontinuous A J K
eq :
  adj₁.unit.app F ≫
      G.op.ran.map (adj₂.unit.app (((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj F)) ≫
        G.op.ran.map ((sheafToPresheaf J A).map (((adj₁.comp adj₂).leftAdjointUniq (adj₃.comp adj₄)).hom.app F)) =
    adj₃.unit.app F ≫ (sheafToPresheaf K A).map (adj₄.unit.app ((presheafToSheaf K A).obj F))
⊢ adj₃.unit.app F ≫ (sheafToPresheaf K A).map (adj₄.unit.app ((presheafToSheaf K A).obj F)) =
    (adj₁.homEquiv F ((sheafToPresheaf J A).obj ((presheafToSheaf K A ⋙ G.sheafPushforwardContinuous A J K).obj F)))
      (((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).map (adj₃.unit.app F))
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic

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
K : GrothendieckTopology D
G : C ⥤ D
ℱ : Dᵒᵖ ⥤ Type v
ℱ' : Sheaf K (Type v)
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj
inst✝ : G.IsLocallyFull K
X✝ Y✝ : C
i✝ : G.obj X✝ ⟶ G.obj Y✝
x✝ : (fun X ↦ X) ((G.op ⋙ ℱ).obj (op Y✝))
X Y : C
i : X ⟶ Y
x : (fun X ↦ X) ((G.op ⋙ ℱ).obj (op Y))
⊢ (ConcreteCategory.hom (ℱ'.obj.map (G.map i).op)) ((ConcreteCategory.hom (α.app (op Y))) x) =
    (ConcreteCategory.hom (α.app (op X))) ((ConcreteCategory.hom (ℱ.map (G.map i).op)) x)

Tactic:
exact ConcreteCategory.congr_hom (α.naturality i.op).symm x

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
A : Type u_1
inst✝² : Category.{v_1, u_1} A
S : C
E✝ : PreOneHypercover S
E : PreOneHypercover S
F : PreOneHypercover S
inst✝¹ : ∀ (i : E.I₀) (j : F.I₀), HasPullback (E.f i) (F.f j)
inst✝ : ∀ (i j : E.I₀) (k : E.I₁ i j) (a b : F.I₀) (l : F.I₁ a b), HasPullback (E.p₁ k ≫ E.f i) (F.p₁ l ≫ F.f a)
i j : __spread✝⁻⁰.I₀
k : E.I₁ i.1 j.1 × F.I₁ i.2 j.2
⊢ (E.p₁ k.1 ≫ E.f i.1) ≫ 𝟙 S = E.p₂ k.1 ≫ E.f ((Equiv.sigmaEquivProd E.I₀ F.toPreZeroHypercover.1).symm j).fst

Tactic:
by simp [E.w]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
A : Type u_1
inst✝² : Category.{v_1, u_1} A
S : C
E✝ : PreOneHypercover S
E : PreOneHypercover S
F : PreOneHypercover S
inst✝¹ : ∀ (i : E.I₀) (j : F.I₀), HasPullback (E.f i) (F.f j)
inst✝ : ∀ (i j : E.I₀) (k : E.I₁ i j) (a b : F.I₀) (l : F.I₁ a b), HasPullback (E.p₁ k ≫ E.f i) (F.p₁ l ≫ F.f a)
⊢ ∀ ⦃i₁ i₂ : (E.inter F.toPreZeroHypercover).I₀⦄ (j : E.I₁ i₁.1 i₂.1 × F.I₁ i₁.2 i₂.2),
    pullback.map (E.p₁ j.1 ≫ E.f i₁.1) (F.p₁ j.2 ≫ F.f i₁.2)
          (E.f ((Equiv.sigmaEquivProd E.I₀ F.toPreZeroHypercover.1).symm i₁).fst)
          (F.f ((Equiv.sigmaEquivProd E.I₀ F.toPreZeroHypercover.1).symm i₁).snd) (E.p₁ j.1) (F.p₁ j.2) (𝟙 S) ⋯ ⋯ ≫
        (E.inter F.toPreZeroHypercover).f i₁ =
      pullback.map (E.p₁ j.1 ≫ E.f i₁.1) (F.p₁ j.2 ≫ F.f i₁.2)
          (E.f ((Equiv.sigmaEquivProd E.I₀ F.toPreZeroHypercover.1).symm i₂).fst)
          (F.f ((Equiv.sigmaEquivProd E.I₀ F.toPreZeroHypercover.1).symm i₂).snd) (E.p₂ j.1) (F.p₂ j.2) (𝟙 S) ⋯ ⋯ ≫
        (E.inter F.toPreZeroHypercover).f i₂

Tactic:
by simp [E.w]

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

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
K : GrothendieckTopology D
A : Type u_4
inst✝² : Category.{v_4, u_4} A
G : C ⥤ D
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj
⊢ G.op.whiskerLeft (sheafHom α) = α

Tactic:
ext X

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
K : GrothendieckTopology D
A : Type u_4
inst✝² : Category.{v_4, u_4} A
G : C ⥤ D
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj
X : Cᵒᵖ
⊢ (G.op.whiskerLeft (sheafHom α)).app X = α.app X
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic

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
K : GrothendieckTopology D
A : Type u_4
inst✝² : Category.{v_4, u_4} A
G : C ⥤ D
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α : ℱ ⟶ ℱ'.obj
⊢ sheafHom (G.op.whiskerLeft α) = α

Tactic:
ext X

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
K : GrothendieckTopology D
A : Type u_4
inst✝² : Category.{v_4, u_4} A
G : C ⥤ D
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α : ℱ ⟶ ℱ'.obj
X : Dᵒᵖ
⊢ (sheafHom (G.op.whiskerLeft α)).app X = α.app X
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic

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
K : GrothendieckTopology D
G : C ⥤ D
inst✝² : G.IsCoverDense K
inst✝¹ : G.IsLocallyFull K
inst✝ : G.IsLocallyFaithful K
ℱ : Sheaf K (Type u_5)
Z : C
T : Presieve Z
x : FamilyOfElements (G.op ⋙ ℱ.obj) T
hx : x.Compatible
Y₁ Y₂ : C
X : D
f₁ : X ⟶ G.obj Y₁
f₂ : X ⟶ G.obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : T g₁
hg₂ : T g₂
⊢ f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂ →
    (ConcreteCategory.hom (ℱ.obj.map f₁.op)) (x g₁ hg₁) = (ConcreteCategory.hom (ℱ.obj.map f₂.op)) (x g₂ hg₂)

Tactic:
eq

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
K : GrothendieckTopology D
G : C ⥤ D
inst✝² : G.IsCoverDense K
inst✝¹ : G.IsLocallyFull K
inst✝ : G.IsLocallyFaithful K
ℱ : Sheaf K (Type u_5)
Z : C
T : Presieve Z
x : FamilyOfElements (G.op ⋙ ℱ.obj) T
hx : x.Compatible
Y₁ Y₂ : C
X : D
f₁ : X ⟶ G.obj Y₁
f₂ : X ⟶ G.obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : T g₁
hg₂ : T g₂
eq : f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂
⊢ (ConcreteCategory.hom (ℱ.obj.map f₁.op)) (x g₁ hg₁) = (ConcreteCategory.hom (ℱ.obj.map f₂.op)) (x g₂ hg₂)
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic

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
E : Type u_3
inst✝² : Category.{v_3, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
G : C ⥤ D
A : Type u_4
inst✝¹ : Category.{v_4, u_4} A
inst✝ : IsDenseSubsite J K G
F : Sheaf J A
X Y : C
f : G.obj X ⟶ G.obj Y
W₀ : C
a : W₀ ⟶ X
ha : (↑⟨G.imageSieve f, ⋯⟩).arrows a
W₀' : C
a' : W₀' ⟶ X
ha' : (↑⟨G.imageSieve f, ⋯⟩).arrows a'
T₀ : C
p₁ : T₀ ⟶ { Y := W₀, f := a, hf := ha }.Y
p₂ : T₀ ⟶ { Y := W₀', f := a', hf := ha' }.Y
fac : p₁ ≫ { Y := W₀, f := a, hf := ha }.f = p₂ ≫ { Y := W₀', f := a', hf := ha' }.f
⊢ G.map { Z := T₀, g₁ := p₁, g₂ := p₂, w := fac }.g₁ ≫ G.map a ≫ f =
    G.map { Z := T₀, g₁ := p₁, g₂ := p₂, w := fac }.g₂ ≫ G.map a' ≫ f

Tactic:
← Functor.map_comp_assoc,

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
E : Type u_3
inst✝² : Category.{v_3, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
G : C ⥤ D
A : Type u_4
inst✝¹ : Category.{v_4, u_4} A
inst✝ : IsDenseSubsite J K G
F : Sheaf J A
X Y : C
f : G.obj X ⟶ G.obj Y
W₀ : C
a : W₀ ⟶ X
ha : (↑⟨G.imageSieve f, ⋯⟩).arrows a
W₀' : C
a' : W₀' ⟶ X
ha' : (↑⟨G.imageSieve f, ⋯⟩).arrows a'
T₀ : C
p₁ : T₀ ⟶ { Y := W₀, f := a, hf := ha }.Y
p₂ : T₀ ⟶ { Y := W₀', f := a', hf := ha' }.Y
fac : p₁ ≫ { Y := W₀, f := a, hf := ha }.f = p₂ ≫ { Y := W₀', f := a', hf := ha' }.f
⊢ G.map ({ Z := T₀, g₁ := p₁, g₂ := p₂, w := fac }.g₁ ≫ a) ≫ f =
    G.map { Z := T₀, g₁ := p₁, g₂ := p₂, w := fac }.g₂ ≫ G.map a' ≫ f
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic

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
E : Type u_3
inst✝² : Category.{v_3, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
G : C ⥤ D
A : Type u_4
inst✝¹ : Category.{v_4, u_4} A
inst✝ : IsDenseSubsite J K G
F : Sheaf J A
X Y : C
f : G.obj X ⟶ G.obj Y
W₀ : C
a : W₀ ⟶ X
ha : (↑⟨G.imageSieve f, ⋯⟩).arrows a
W₀' : C
a' : W₀' ⟶ X
ha' : (↑⟨G.imageSieve f, ⋯⟩).arrows a'
T₀ : C
p₁ : T₀ ⟶ { Y := W₀, f := a, hf := ha }.Y
p₂ : T₀ ⟶ { Y := W₀', f := a', hf := ha' }.Y
fac : p₁ ≫ { Y := W₀, f := a, hf := ha }.f = p₂ ≫ { Y := W₀', f := a', hf := ha' }.f
⊢ G.map ({ Z := T₀, g₁ := p₁, g₂ := p₂, w := fac }.g₁ ≫ a) ≫ f =
    G.map { Z := T₀, g₁ := p₁, g₂ := p₂, w := fac }.g₂ ≫ G.map a' ≫ f

Tactic:
← Functor.map_comp_assoc,

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
E : Type u_3
inst✝² : Category.{v_3, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
G : C ⥤ D
A : Type u_4
inst✝¹ : Category.{v_4, u_4} A
inst✝ : IsDenseSubsite J K G
F : Sheaf J A
X Y : C
f : G.obj X ⟶ G.obj Y
W₀ : C
a : W₀ ⟶ X
ha : (↑⟨G.imageSieve f, ⋯⟩).arrows a
W₀' : C
a' : W₀' ⟶ X
ha' : (↑⟨G.imageSieve f, ⋯⟩).arrows a'
T₀ : C
p₁ : T₀ ⟶ { Y := W₀, f := a, hf := ha }.Y
p₂ : T₀ ⟶ { Y := W₀', f := a', hf := ha' }.Y
fac : p₁ ≫ { Y := W₀, f := a, hf := ha }.f = p₂ ≫ { Y := W₀', f := a', hf := ha' }.f
⊢ G.map ({ Z := T₀, g₁ := p₁, g₂ := p₂, w := fac }.g₁ ≫ a) ≫ f =
    G.map ({ Z := T₀, g₁ := p₁, g₂ := p₂, w := fac }.g₂ ≫ a') ≫ f
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
A : Type u_1
inst✝ : Category.{v_1, u_1} A
S : C
E : PreOneHypercover S
F : PreOneHypercover S
f : E.Hom F
P : Cᵒᵖ ⥤ A
c : Multifork (E.multicospanIndex P)
hc : IsLimit c
d : Multifork (F.multicospanIndex P)
a : E.I₀
⊢ f.mapMultiforkOfIsLimit P hc d ≫ c.ι a = d.ι (f.s₀ a) ≫ P.map (f.h₀ a).op

Tactic:
simp [mapMultiforkOfIsLimit]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
A : Type u_1
inst✝ : Category.{v_1, u_1} A
S : C
E✝¹ E✝ : PreOneHypercover S
F✝ : PreOneHypercover S
G : PreOneHypercover S
E : PreOneHypercover S
F : PreOneHypercover S
f g : E.Hom F
hs₀ : f.s₀ = g.s₀
hh₀ : ∀ (i : E.I₀), f.h₀ i = g.h₀ i ≫ eqToHom ⋯
hs₁ : ∀ (i j : E.I₀) (k : E.I₁ i j), f.s₁ k = (congrIndexOneOfEq ⋯ ⋯) (g.s₁ k)
i j : E.I₀
k : E.I₁ i j
⊢ F.Y ((congrIndexOneOfEq ⋯ ⋯) (g.s₁ k)) = F.Y (f.s₁ k)

Tactic:
by rw [PreOneHypercover.congrIndexOneOfEq_congrFun hs₀ hs₁]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
A : Type u_1
inst✝ : Category.{v_1, u_1} A
S : C
E✝¹ E✝ : PreOneHypercover S
F✝ : PreOneHypercover S
G : PreOneHypercover S
E : PreOneHypercover S
F : PreOneHypercover S
f g : E.Hom F
hs₀ : f.s₀ = g.s₀
x✝ : ∀ (i : E.I₀), f.h₀ i = g.h₀ i ≫ eqToHom ⋯
hs₁ : ∀ (i j : E.I₀) (k : E.I₁ i j), f.s₁ k = (congrIndexOneOfEq ⋯ ⋯) (g.s₁ k)
i j : E.I₀
k : E.I₁ i j
⊢ F.Y ((congrIndexOneOfEq ⋯ ⋯) (g.s₁ k)) = F.Y (f.s₁ k)

Tactic:
by rw [PreOneHypercover.congrIndexOneOfEq_congrFun hs₀ hs₁]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
S : C
E : J.OneHypercover S
i₁ i₂ : E.I₀
inst✝ : HasPullback (E.f i₁) (E.f i₂)
⊢ E.sieve₁' i₁ i₂ ∈ J (Limits.pullback (E.f i₁) (E.f i₂))

Tactic:
rw [E.sieve₁'_eq_sieve₁]
  exact mem₁ _ _ _ _ _ pullback.condition

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

Goal state before:
pp: case refine_1.transitive
C : Type u
inst✝² : Category.{v, u} C
K : Precoverage C
inst✝¹ : K.HasPullbacks
inst✝ : K.IsStableUnderBaseChange
X Y✝ : C
right : Discrete PUnit.{1}
R✝ : Sieve Y✝
Y : C
R S : Sieve Y
hR : K.toCoverage.Saturate Y R
H : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, R.arrows f → K.toCoverage.Saturate Y_1 (Sieve.pullback f S)
ih :
  ∀ (s : Y ⟶ X),
    (Sieve.overEquiv { left := Y, right := right, hom := s }).symm R ∈
      (Precoverage.comap (Over.forget X) K).toGrothendieck { left := Y, right := right, hom := s }
ih' :
  ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄,
    R.arrows f →
      ∀ (s : Y_1 ⟶ X),
        (Sieve.overEquiv { left := Y_1, right := right, hom := s }).symm (Sieve.pullback f S) ∈
          (Precoverage.comap (Over.forget X) K).toGrothendieck { left := Y_1, right := right, hom := s }
s : Y ⟶ X
Z : Over X
g : Z ⟶ { left := Y, right := right, hom := s }
hg : ((Sieve.overEquiv { left := Y, right := right, hom := s }).symm R).arrows g
⊢ Sieve.pullback g ((Sieve.overEquiv { left := Y, right := right, hom := s }).symm S) ∈
    (Precoverage.comap (Over.forget X) K).toGrothendieck Z

Tactic:
obtain rfl : right = Z.right := Subsingleton.elim _ _

Goal state after:
case refine_1.transitive
C : Type u
inst✝² : Category.{v, u} C
K : Precoverage C
inst✝¹ : K.HasPullbacks
inst✝ : K.IsStableUnderBaseChange
X Y✝ : C
R✝ : Sieve Y✝
Y : C
R S : Sieve Y
hR : K.toCoverage.Saturate Y R
H : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, R.arrows f → K.toCoverage.Saturate Y_1 (Sieve.pullback f S)
s : Y ⟶ X
Z : Over X
ih :
  ∀ (s : Y ⟶ X),
    (Sieve.overEquiv { left := Y, right := Z.right, hom := s }).symm R ∈
      (Precoverage.comap (Over.forget X) K).toGrothendieck { left := Y, right := Z.right, hom := s }
ih' :
  ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄,
    R.arrows f →
      ∀ (s : Y_1 ⟶ X),
        (Sieve.overEquiv { left := Y_1, right := Z.right, hom := s }).symm (Sieve.pullback f S) ∈
          (Precoverage.comap (Over.forget X) K).toGrothendieck { left := Y_1, right := Z.right, hom := s }
g : Z ⟶ { left := Y, right := Z.right, hom := s }
hg : ((Sieve.overEquiv { left := Y, right := Z.right, hom := s }).symm R).arrows g
⊢ Sieve.pullback g ((Sieve.overEquiv { left := Y, right := Z.right, hom := s }).symm S) ∈
    (Precoverage.comap (Over.forget X) K).toGrothendieck Z
Module: Mathlib.CategoryTheory.Limits.Final.Type

Goal state before:
pp: case refine_2
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
h : ∀ (Y : D), ∃ a, ∀ (j : CostructuredArrow F Y), (ConcreteCategory.hom (P.map j.hom)) (↑t j.left) = a
⊢ ∃ a, F.sectionsPrecomp a = t

Tactic:
choose val hval using h

Goal state after:
case refine_2
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
val : (Y : D) → P.obj Y
hval : ∀ (Y : D) (j : CostructuredArrow F Y), (ConcreteCategory.hom (P.map j.hom)) (↑t j.left) = val Y
⊢ ∃ a, F.sectionsPrecomp a = t
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
M : SheafOfModules R
f : unit R ⟶ M
⊢ pushforwardSections φ (M.unitHomEquiv f) =
    ((pushforward φ).obj M).unitHomEquiv (unitToPushforwardObjUnit φ ≫ (pushforward φ).map f)

Tactic:
ext X

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
M : SheafOfModules R
f : unit R ⟶ M
X : Cᵒᵖ
⊢ ↑(pushforwardSections φ (M.unitHomEquiv f)) X =
    ↑(((pushforward φ).obj M).unitHomEquiv (unitToPushforwardObjUnit φ ≫ (pushforward φ).map f)) X
Module: Mathlib.CategoryTheory.Simple

Goal state before:
pp: case mpr
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X : C
inst✝ : IsSimpleOrder (Subobject X)
Y : C
f : Y ⟶ X
hf : Mono f
⊢ f ≠ 0 → IsIso f

Tactic:
· intro i
    rcases IsSimpleOrder.eq_bot_or_eq_top (Subobject.mk f) with (h | h)
    · rw [Subobject.mk_eq_bot_iff_zero] at h
      exact False.elim (i h)
    · exact (Subobject.isIso_iff_mk_eq_top _).mpr h

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Lattice

Goal state before:
pp: α : Type u
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
x y z : α
f : z ⟶ x
g : z ⟶ y
⊢ colimit (span f g) = Finset.univ.sup (span f g).obj

Tactic:
by rw [finite_colimit_eq_finset_univ_sup]

Goal state after: