mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Adjunction.Whiskering

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_3, u_3} E
F : D ⥤ E
G : E ⥤ D
adj : F ⊣ G
⊢ ∀ ⦃X Y : C ⥤ D⦄ (f : X ⟶ Y),
    (𝟭 (C ⥤ D)).map f ≫ ((𝟭 (C ⥤ D)).obj Y).rightUnitor.inv ≫ Y.whiskerLeft adj.unit ≫ (Y.associator F G).inv =
      (((𝟭 (C ⥤ D)).obj X).rightUnitor.inv ≫ X.whiskerLeft adj.unit ≫ (X.associator F G).inv) ≫
        ((whiskeringRight C D E).obj F ⋙ (whiskeringRight C E D).obj G).map f

Tactic:
intros

Goal state after:
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_3, u_3} E
F : D ⥤ E
G : E ⥤ D
adj : F ⊣ G
X✝ Y✝ : C ⥤ D
f✝ : X✝ ⟶ Y✝
⊢ (𝟭 (C ⥤ D)).map f✝ ≫ ((𝟭 (C ⥤ D)).obj Y✝).rightUnitor.inv ≫ Y✝.whiskerLeft adj.unit ≫ (Y✝.associator F G).inv =
    (((𝟭 (C ⥤ D)).obj X✝).rightUnitor.inv ≫ X✝.whiskerLeft adj.unit ≫ (X✝.associator F G).inv) ≫
      ((whiskeringRight C D E).obj F ⋙ (whiskeringRight C E D).obj G).map f✝
Module: Mathlib.CategoryTheory.Adjunction.Whiskering

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_3, u_3} E
F : D ⥤ E
G : E ⥤ D
adj : F ⊣ G
⊢ ∀ ⦃X Y : C ⥤ E⦄ (f : X ⟶ Y),
    ((whiskeringRight C E D).obj G ⋙ (whiskeringRight C D E).obj F).map f ≫
        (Y.associator G F).hom ≫ Y.whiskerLeft adj.counit ≫ Y.rightUnitor.hom =
      ((X.associator G F).hom ≫ X.whiskerLeft adj.counit ≫ X.rightUnitor.hom) ≫ (𝟭 (C ⥤ E)).map f

Tactic:
intros

Goal state after:
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_3, u_3} E
F : D ⥤ E
G : E ⥤ D
adj : F ⊣ G
X✝ Y✝ : C ⥤ E
f✝ : X✝ ⟶ Y✝
⊢ ((whiskeringRight C E D).obj G ⋙ (whiskeringRight C D E).obj F).map f✝ ≫
      (Y✝.associator G F).hom ≫ Y✝.whiskerLeft adj.counit ≫ Y✝.rightUnitor.hom =
    ((X✝.associator G F).hom ≫ X✝.whiskerLeft adj.counit ≫ X✝.rightUnitor.hom) ≫ (𝟭 (C ⥤ E)).map f✝
Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck

Goal state before:
pp: case mpr
C : Type u_3
inst✝ : Category.{u_2, u_3} C
J : Precoverage C
P : Cᵒᵖ ⥤ Type u_1
H : ∀ {X Y : C} {f : Y ⟶ X}, ∀ R ∈ J.coverings X, Presieve.IsSheafFor P (Sieve.pullback f (Sieve.generate R)).arrows
X : C
S : Sieve X
hS : S ∈ J.toGrothendieck X
⊢ ∀ ⦃Y : C⦄ (f : Y ⟶ X), Presieve.IsSheafFor P (Sieve.pullback f S).arrows

Tactic:
induction hS with

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

Goal state before:
pp: case refine_1
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
hS : S ∈ J.toGrothendieck X
⊢ ∃ R ∈ J.coverings X, R ≤ S.arrows

Tactic:
induction hS with

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

Goal state before:
pp: C : Type u_4
inst✝³ : Category.{u_3, u_4} C
D : Type u_1
inst✝² : Category.{v_1, u_1} D
F : C ⥤ D
P : Dᵒᵖ ⥤ Type u_2
X : C
R : Presieve X
inst✝¹ : R.HasPairwisePullbacks
inst✝ : F.PreservesPairwisePullbacks R
⊢ IsSheafFor (F.op ⋙ P) R ↔ IsSheafFor P (map F R)

Tactic:
by
  have : (R.map F).HasPairwisePullbacks := .map_of_preservesPairwisePullbacks _ _
  obtain ⟨ι, Y, f, rfl⟩ := R.exists_eq_ofArrows
  rw [map_ofArrows] at this ⊢
  simp_rw [Presieve.isSheafFor_arrows_iff_pullbacks]
  dsimp [Arrows.PullbackCompatible]
  congr! with x
  rw [forall₂_congr]
  intro i j
  have : PreservesLimit (cospan (f i) (f j)) F :=
    F.preservesLimit_cospan_of_mem_presieve (ofArrows _ f) ⟨i⟩ ⟨j⟩
  have : HasPullback (F.map (f i)) (F.map (f j)) := hasPullback_of_preservesPullback _ _ _
  rw [← pullbackComparison_comp_fst, op_comp, Functor.map_comp,
    ← pullbackComparison_comp_snd, op_comp, Functor.map_comp]
  have : Function.Bijective (P.map (pullbackComparison F (f i) (f j)).op) := by
    rw [← isIso_iff_bijective]
    infer_instance
  exact this.1.eq_iff

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
A : Type u
inst✝² : Category.{t, u} A
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝¹ : F.PreservesOneHypercovers J K
inst✝ : J.IsGeneratedByOneHypercovers
P : Dᵒᵖ ⥤ A
hP : Presheaf.IsSheaf K P
⊢ Presheaf.IsSheaf J (F.op ⋙ P)

Tactic:
rw [Presheaf.isSheaf_iff_of_isGeneratedByOneHypercovers.{w}]

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
A : Type u
inst✝² : Category.{t, u} A
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝¹ : F.PreservesOneHypercovers J K
inst✝ : J.IsGeneratedByOneHypercovers
P : Dᵒᵖ ⥤ A
hP : Presheaf.IsSheaf K P
⊢ ∀ ⦃X : C⦄ (E : J.OneHypercover X), Nonempty (IsLimit (E.multifork (F.op ⋙ P)))
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
K : GrothendieckTopology D
G : C ⥤ D
inst✝ : RepresentablyFlat G
ℱ : Sheaf K (Type u_1)
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:
f₁

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
K : GrothendieckTopology D
G : C ⥤ D
inst✝ : RepresentablyFlat G
ℱ : Sheaf K (Type u_1)
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₂)
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: case refine_1
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
c' : Fan (E.multicospanIndex F).left := Fan.mk (F.obj (op c.pt)) fun i ↦ F.map (c.inj i).op
hc' : IsLimit c' := isLimitFanMkObjOfIsLimit F (fun i ↦ op (E.X i)) (fun i ↦ (c.inj i).op) (Cofan.IsColimit.op hc)
d' : Fan (E.multicospanIndex F).right := Fan.mk (F.obj (op d.pt)) fun i ↦ F.map (d.inj i).op
hd' : IsLimit d' := isLimitFanMkObjOfIsLimit F (fun i ↦ op (E.Y' i)) (fun i ↦ (d.inj i).op) (Cofan.IsColimit.op hd)
i : E.multicospanShape.R
⊢ ((Iso.refl c'.pt).hom ≫ F.map (Cofan.IsColimit.desc hd fun x ↦ E.p₁ x.snd ≫ c.inj x.fst.1).op) ≫ d'.proj i =
    ((E.multicospanIndex F).fstPiMapOfIsLimit c' hd' ≫ (Iso.refl d'.pt).hom) ≫ d'.proj i

Tactic:
simp only [multicospanShape_L, multicospanIndex_right, multicospanShape_R, Iso.refl_hom,
      Y'_apply, id_comp, comp_id]

Goal state after:
case refine_1
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
c' : Fan (E.multicospanIndex F).left := Fan.mk (F.obj (op c.pt)) fun i ↦ F.map (c.inj i).op
hc' : IsLimit c' := isLimitFanMkObjOfIsLimit F (fun i ↦ op (E.X i)) (fun i ↦ (c.inj i).op) (Cofan.IsColimit.op hc)
d' : Fan (E.multicospanIndex F).right := Fan.mk (F.obj (op d.pt)) fun i ↦ F.map (d.inj i).op
hd' : IsLimit d' := isLimitFanMkObjOfIsLimit F (fun i ↦ op (E.Y' i)) (fun i ↦ (d.inj i).op) (Cofan.IsColimit.op hd)
i : E.multicospanShape.R
⊢ F.map (Cofan.IsColimit.desc hd fun x ↦ E.p₁ x.snd ≫ c.inj x.fst.1).op ≫ d'.proj i =
    (E.multicospanIndex F).fstPiMapOfIsLimit c' hd' ≫ d'.proj i
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: case refine_2
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
c' : Fan (E.multicospanIndex F).left := Fan.mk (F.obj (op c.pt)) fun i ↦ F.map (c.inj i).op
hc' : IsLimit c' := isLimitFanMkObjOfIsLimit F (fun i ↦ op (E.X i)) (fun i ↦ (c.inj i).op) (Cofan.IsColimit.op hc)
d' : Fan (E.multicospanIndex F).right := Fan.mk (F.obj (op d.pt)) fun i ↦ F.map (d.inj i).op
hd' : IsLimit d' := isLimitFanMkObjOfIsLimit F (fun i ↦ op (E.Y' i)) (fun i ↦ (d.inj i).op) (Cofan.IsColimit.op hd)
i : E.multicospanShape.R
⊢ ((Iso.refl c'.pt).hom ≫ F.map (Cofan.IsColimit.desc hd fun x ↦ E.p₂ x.snd ≫ c.inj x.fst.2).op) ≫ d'.proj i =
    ((E.multicospanIndex F).sndPiMapOfIsLimit c' hd' ≫ (Iso.refl d'.pt).hom) ≫ d'.proj i

Tactic:
simp only [multicospanShape_L, multicospanIndex_right, multicospanShape_R, Iso.refl_hom,
      Y'_apply, id_comp, comp_id]

Goal state after:
case refine_2
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
c' : Fan (E.multicospanIndex F).left := Fan.mk (F.obj (op c.pt)) fun i ↦ F.map (c.inj i).op
hc' : IsLimit c' := isLimitFanMkObjOfIsLimit F (fun i ↦ op (E.X i)) (fun i ↦ (c.inj i).op) (Cofan.IsColimit.op hc)
d' : Fan (E.multicospanIndex F).right := Fan.mk (F.obj (op d.pt)) fun i ↦ F.map (d.inj i).op
hd' : IsLimit d' := isLimitFanMkObjOfIsLimit F (fun i ↦ op (E.Y' i)) (fun i ↦ (d.inj i).op) (Cofan.IsColimit.op hd)
i : E.multicospanShape.R
⊢ F.map (Cofan.IsColimit.desc hd fun x ↦ E.p₂ x.snd ≫ c.inj x.fst.2).op ≫ d'.proj i =
    (E.multicospanIndex F).sndPiMapOfIsLimit c' hd' ≫ d'.proj i
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
S : C
E : PreOneHypercover S
c : Cofan E.X
hc : IsColimit c
d : Cofan E.Y'
hd : IsColimit d
i : E.I₁'
a b : PUnit.{w + 1}
r : (E.sigmaOfIsColimit hc hd).I₁ a b
⊢ d.inj i ≫ (E.sigmaOfIsColimit hc hd).p₁ r = E.p₁ i.snd ≫ c.inj i.fst.1

Tactic:
simp [sigmaOfIsColimit]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
S : C
E : PreOneHypercover S
c : Cofan E.X
hc : IsColimit c
d : Cofan E.Y'
hd : IsColimit d
i : E.I₁'
a b : PUnit.{w + 1}
r : (E.sigmaOfIsColimit hc hd).I₁ a b
⊢ d.inj i ≫ (E.sigmaOfIsColimit hc hd).p₂ r = E.p₂ i.snd ≫ c.inj i.fst.2

Tactic:
simp [sigmaOfIsColimit]

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
G✝ : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type u_1
inst✝¹ : Category.{v_1, u_1} A
G : C ⥤ D
inst✝ : G.Full
U✝ V✝ : C
f : G.obj U✝ ⟶ G.obj V✝
⊢ Sieve.functorPushforward G (G.imageSieve f) ∈ K (G.obj U✝)

Tactic:
← G.map_preimage f

Goal state after:
C : Type uC
inst✝³ : Category.{vC, uC} C
D : Type uD
inst✝² : Category.{vD, uD} D
G✝ : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type u_1
inst✝¹ : Category.{v_1, u_1} A
G : C ⥤ D
inst✝ : G.Full
U✝ V✝ : C
f : G.obj U✝ ⟶ G.obj V✝
⊢ Sieve.functorPushforward G (G.imageSieve (G.map (G.preimage f))) ∈ K (G.obj U✝)
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.SheafEquiv

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
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
⊢ Limits.Cone (StructuredArrow.proj (op (G.obj U)) G.op ⋙ Y.obj)

Tactic:
refine ⟨X, ⟨fun g ↦ ?_, fun g₁ g₂ i ↦ ?_⟩⟩

Goal state after:
case refine_1
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 : StructuredArrow (op (G.obj U)) G.op
⊢ ((const (StructuredArrow (op (G.obj U)) G.op)).obj X).obj g ⟶ (StructuredArrow.proj (op (G.obj U)) G.op ⋙ Y.obj).obj g

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 ≫ ?refine_1 =
    ?refine_1 ≫ (StructuredArrow.proj (op (G.obj U)) G.op ⋙ Y.obj).map i
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:
f₁

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₂),
    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₁ ≫ a) ≫ f =
    G.map ({ Z := T₀, g₁ := p₁, g₂ := p₂, w := fac }.g₂ ≫ a') ≫ f

Tactic:
fac

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 (p₂ ≫ { Y := W₀', f := a', hf := ha' }.f) ≫ f = G.map ({ Z := T₀, g₁ := p₁, g₂ := p₂, w := fac }.g₂ ≫ 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
J : GrothendieckTopology C
K : GrothendieckTopology D
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 Z : C
f : G.obj X ⟶ G.obj Y
p : Z ⟶ X
g : Z ⟶ Y
fac : G.map p ≫ f = G.map g
W₀ : C
a : W₀ ⟶ Z
ha : (Sieve.pullback p (G.imageSieve f)).arrows a
⊢ G.map a ≫ G.map p ≫ f = G.map a ≫ G.map g

Tactic:
fac

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
J : GrothendieckTopology C
K : GrothendieckTopology D
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 Z : C
f : G.obj X ⟶ G.obj Y
p : Z ⟶ X
g : Z ⟶ Y
fac : G.map p ≫ f = G.map g
W₀ : C
a : W₀ ⟶ Z
ha : (Sieve.pullback p (G.imageSieve f)).arrows a
⊢ G.map a ≫ G.map g = G.map a ≫ G.map g
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
J : GrothendieckTopology C
K : GrothendieckTopology D
G : C ⥤ D
A : Type u_4
inst✝³ : Category.{v_4, u_4} A
inst✝² : IsDenseSubsite J K G
inst✝¹ : (G.sheafPushforwardContinuous A J K).IsEquivalence
inst✝ : HasWeakSheafify J A
P₁ P₂ : Dᵒᵖ ⥤ A
f : P₁ ⟶ P₂
Q : Sheaf K A
g : (sheafifyOfIsEquivalence J K G A).obj P₂ ⟶ Q
⊢ (sheafifyHomEquivOfIsEquivalence J K G) ((sheafifyOfIsEquivalence J K G A).map f ≫ g) =
    f ≫ (sheafifyHomEquivOfIsEquivalence J K G) g

Tactic:
by
  have := IsDenseSubsite.isLocallyFull J K G
  have := IsDenseSubsite.isCoverDense J K G
  let adj₁ := (G.sheafPushforwardContinuous A J K).asEquivalence.symm.toAdjunction
  let adj₂ := sheafificationAdjunction J A
  change IsCoverDense.restrictHomEquivHom (adj₂.homEquiv _ _ (adj₁.homEquiv _ _
    ((sheafifyOfIsEquivalence J K G A).map f ≫ g))) =
      f ≫ IsCoverDense.restrictHomEquivHom (adj₂.homEquiv _ _ (adj₁.homEquiv _ _ g))
  rw [← IsCoverDense.restrictHomEquivHom_naturality_left]
  congr 2
  trans adj₂.homEquiv _ _ ((presheafToSheaf J A).map (G.op.whiskerLeft f) ≫
    (adj₁.homEquiv _ _) g)
  · congr 1
    apply adj₁.homEquiv_naturality_left
  · apply adj₂.homEquiv_naturality_left

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
K : GrothendieckTopology D
inst✝² : G.LocallyCoverDense K
inst✝¹ : G.IsLocallyFull K
inst✝ : G.IsLocallyFaithful K
U✝ : C
S✝ : Sieve U✝
hS : S✝ ∈ (Precoverage.comap G K.toPrecoverage).toGrothendieck U✝
⊢ Sieve.functorPushforward G S✝ ∈ K (G.obj U✝)

Tactic:
induction hS with

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
S : C
E F : PreOneHypercover S
e : E ≅ F
i : E.I₀
⊢ e.hom.h₀ i ≫ e.inv.h₀ (e.hom.s₀ i) = eqToHom ⋯

Tactic:
obtain ⟨hs, hh, _⟩ := Hom.ext'_iff.mp e.hom_inv_id

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
S : C
E F : PreOneHypercover S
e : E ≅ F
i : E.I₀
hs : (e.hom ≫ e.inv).s₀ = (𝟙 E).s₀
hh : ∀ (i : E.I₀), (e.hom ≫ e.inv).h₀ i = (𝟙 E).h₀ i ≫ eqToHom ⋯
h✝ :
  ∃ (hs₁ : ∀ (i j : E.I₀) (k : E.I₁ i j), (e.hom ≫ e.inv).s₁ k = (congrIndexOneOfEq ⋯ ⋯) ((𝟙 E).s₁ k)),
    ∀ (i j : E.I₀) (k : E.I₁ i j),
      (e.hom ≫ e.inv).h₁ k = (𝟙 E).h₁ k ≫ (congrIndexOneOfEqIso ⋯ ⋯ ((𝟙 E).s₁ k)).inv ≫ eqToHom ⋯
⊢ e.hom.h₀ i ≫ e.inv.h₀ (e.hom.s₀ i) = eqToHom ⋯
Module: Mathlib.CategoryTheory.Sites.CoversTop.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
I : Type u_1
Y : I → C
x : FamilyOfElementsOnObjects F Y
hx : x.IsCompatible
X Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
⊢ ∀ ⦃f₁ : Y₁ ⟶ X⦄ ⦃f₂ : Y₂ ⟶ X⦄ (h₁ : (Sieve.ofObjects Y X).arrows f₁) (h₂ : (Sieve.ofObjects Y X).arrows f₂),
    g₁ ≫ f₁ = g₂ ≫ f₂ →
      (ConcreteCategory.hom (F.map g₁.op)) (x.familyOfElements X f₁ h₁) =
        (ConcreteCategory.hom (F.map g₂.op)) (x.familyOfElements X f₂ h₂)

Tactic:
f₁

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
I : Type u_1
Y : I → C
x : FamilyOfElementsOnObjects F Y
hx : x.IsCompatible
X Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
⊢ ∀ ⦃f₂ : Y₂ ⟶ X⦄ (h₁ : (Sieve.ofObjects Y X).arrows f₁) (h₂ : (Sieve.ofObjects Y X).arrows f₂),
    g₁ ≫ f₁ = g₂ ≫ f₂ →
      (ConcreteCategory.hom (F.map g₁.op)) (x.familyOfElements X f₁ h₁) =
        (ConcreteCategory.hom (F.map g₂.op)) (x.familyOfElements X f₂ h₂)
Module: Mathlib.CategoryTheory.Sites.CoversTop.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
I : Type u_1
Y : I → C
x : FamilyOfElementsOnObjects F Y
hx : x.IsCompatible
X Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
⊢ ∀ (h₁ : (Sieve.ofObjects Y X).arrows f₁) (h₂ : (Sieve.ofObjects Y X).arrows f₂),
    g₁ ≫ f₁ = g₂ ≫ f₂ →
      (ConcreteCategory.hom (F.map g₁.op)) (x.familyOfElements X f₁ h₁) =
        (ConcreteCategory.hom (F.map g₂.op)) (x.familyOfElements X f₂ h₂)

Tactic:
⟨i₁, ⟨φ₁⟩⟩

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
I : Type u_1
Y : I → C
x : FamilyOfElementsOnObjects F Y
hx : x.IsCompatible
X Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
i₁ : I
φ₁ : Y₁ ⟶ Y i₁
⊢ ∀ (h₂ : (Sieve.ofObjects Y X).arrows f₂),
    g₁ ≫ f₁ = g₂ ≫ f₂ →
      (ConcreteCategory.hom (F.map g₁.op)) (x.familyOfElements X f₁ ⋯) =
        (ConcreteCategory.hom (F.map g₂.op)) (x.familyOfElements X f₂ h₂)
Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators

Goal state before:
pp: C : Type u'
inst✝⁷ : Category.{v', u'} C
J : GrothendieckTopology C
R : Sheaf J RingCat
inst✝⁶ : HasWeakSheafify J AddCommGrpCat
inst✝⁵ : J.WEqualsLocallyBijective AddCommGrpCat
M✝ N P : SheafOfModules R
C' : Type u₁
inst✝⁴ : Category.{v₁, u₁} C'
J' : GrothendieckTopology C'
S : Sheaf J' RingCat
inst✝³ : HasSheafify J' AddCommGrpCat
inst✝² : J'.WEqualsLocallyBijective AddCommGrpCat
M : SheafOfModules R
G : M.GeneratingSections
F : SheafOfModules R ⥤ SheafOfModules S
inst✝¹ : PreservesColimitsOfSize.{u, u, max u u', max u u₁, max (max (u + 1) u') v', max (max (u + 1) u₁) v₁} F
η : unit S ≅ F.obj (unit R)
inst✝ : IsIso G.π
⊢ IsIso (G.map F η).π

Tactic:
rw [GeneratingSections.map_π_eq]
  infer_instance

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₁ Y₂ : Over X
S₁ : Sieve Y₁
f : Y₂ ⟶ Y₁
h₁ : S₁ ∈ ⇑(Sieve.overEquiv Y₁) ⁻¹' J Y₁.left
⊢ Sieve.pullback (Over.Hom.left f) ((Sieve.overEquiv Y₁) S₁) ∈ J Y₂.left

Tactic:
exact J.pullback_stable _ h₁

Goal state after: