mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X Y : C
h : Retract X Y
n : ℕ
inst✝ : HasProjectiveDimensionLT Y n
this : HasExt C := HasExt.standard C
i : ℕ
hi : n ≤ i
T : C
⊢ ∀ (e : Ext X T i), e = 0

Tactic:
x

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X Y : C
h : Retract X Y
n : ℕ
inst✝ : HasProjectiveDimensionLT Y n
this : HasExt C := HasExt.standard C
i : ℕ
hi : n ≤ i
T : C
x : Ext X T i
⊢ x = 0
Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
inst✝ : EnoughInjectives C
X : C
n : ℕ
hX : ∀ (Y : C), Subsingleton (Ext X Y n)
d : ℕ
Y : C
⊢ ∀ (e : Ext X Y d) (k : ℕ), d = n + k → e = 0

Tactic:
e

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
inst✝ : EnoughInjectives C
X : C
n : ℕ
hX : ∀ (Y : C), Subsingleton (Ext X Y n)
d : ℕ
Y : C
e : Ext X Y d
⊢ ∀ (k : ℕ), d = n + k → e = 0
Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension

Goal state before:
pp: case coe.coe
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
d : ℕ
hd : projectiveDimension X = ↑↑d
⊢ ↑↑d ≠ ⊤ ↔ ∃ n, HasProjectiveDimensionLE X n

Tactic:
simp only [ne_eq, WithBot.coe_eq_top, ENat.natCast_ne_top, not_false_eq_true, true_iff]
      exact ⟨d, by simpa only [← projectiveDimension_le_iff] using! hd.le⟩

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.SigmaConst

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
R : C
inst✝ : HasCoproducts C
α β : Type w
f : α ⟶ β
⊢ HasCokernel ((sigmaConst.obj R).map f)

Tactic:
by
  dsimp; infer_instance

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
J : GrothendieckTopology C
R₀ : Cᵒᵖ ⥤ RingCat
R : Sheaf J RingCat
α : R₀ ⟶ R.obj
inst✝³ : Presheaf.IsLocallyInjective J α
inst✝² : Presheaf.IsLocallySurjective J α
M₀ : PresheafOfModules R₀
A : Sheaf J AddCommGrpCat
φ : M₀.presheaf ⟶ A.obj
inst✝¹ : Presheaf.IsLocallyInjective J φ
inst✝ : Presheaf.IsLocallySurjective J φ
X Y : Cᵒᵖ
π : X ⟶ Y
r : ↑(R.obj.obj X)
m : ↑(A.obj.obj X)
⊢ (ConcreteCategory.hom (A.obj.map π)) (smul α φ r m) =
    smul α φ ((ConcreteCategory.hom (R.obj.map π)) r) ((ConcreteCategory.hom (A.obj.map π)) m)

Tactic:
let S := Presheaf.imageSieve α (R.obj.map π r) ⊓ Presheaf.imageSieve φ (A.obj.map π m)
  have hS : S ∈ J Y.unop := by
    apply J.intersection_covering
    all_goals apply Presheaf.imageSieve_mem
  apply A.isSeparated _ _ hS
  rintro Y f ⟨⟨r₀,
    (hr₀ : (α.app (Opposite.op Y)).hom r₀ = (R.obj.map f.op).hom ((R.obj.map π).hom r))⟩,
    ⟨m₀, (hm₀ : (φ.app _) _ = _)⟩⟩
  rw [← ConcreteCategory.comp_apply, ← Functor.map_comp,
    map_smul_eq α φ r m (π ≫ f.op) r₀ (by rw [hr₀, Functor.map_comp, RingCat.comp_apply]) m₀
      (by rw [hm₀, Functor.map_comp, ConcreteCategory.comp_apply]),
    map_smul_eq α φ (R.obj.map π r) (A.obj.map π m) f.op r₀ hr₀ m₀ hm₀]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X Y : C
f : Y ⟶ X
S : Sieve X
hS : J₁.IsClosed S
Z : C
g : Z ⟶ Y
hg : J₁.Covers (Sieve.pullback f S) g
⊢ J₁.Covers S (g ≫ f)

Tactic:
by rwa [J₁.covers_iff, Sieve.pullback_comp]

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

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁).toFunctor S.arrows
M : Sieve X
hM : M ∈ (Functor.closedSieves J₁).obj (Opposite.op X)
N : Sieve X
hN : N ∈ (Functor.closedSieves J₁).obj (Opposite.op X)
hM₂ : x.IsAmalgamation ⟨M, hM⟩
hN₂ : x.IsAmalgamation ⟨N, hN⟩
⊢ ⟨M, hM⟩ = ⟨N, hN⟩

Tactic:
ext Y f

Goal state after:
case refine_1
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁).toFunctor S.arrows
M : Sieve X
hM : M ∈ (Functor.closedSieves J₁).obj (Opposite.op X)
N : Sieve X
hN : N ∈ (Functor.closedSieves J₁).obj (Opposite.op X)
hM₂ : x.IsAmalgamation ⟨M, hM⟩
hN₂ : x.IsAmalgamation ⟨N, hN⟩
Y : C
f : Y ⟶ X
⊢ (↑⟨M, hM⟩).arrows f ↔ (↑⟨N, hN⟩).arrows f
Module: Mathlib.CategoryTheory.Sites.Closed

Goal state before:
pp: case refine_1.mp
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁).toFunctor S.arrows
M : Sieve X
hM : M ∈ (Functor.closedSieves J₁).obj (Opposite.op X)
N : Sieve X
hN : N ∈ (Functor.closedSieves J₁).obj (Opposite.op X)
hM₂ : x.IsAmalgamation ⟨M, hM⟩
hN₂ : x.IsAmalgamation ⟨N, hN⟩
Y : C
f : Y ⟶ X
q : ∀ ⦃Z : C⦄ (g : Z ⟶ X), S.arrows g → Sieve.pullback g M = Sieve.pullback g N
MSNS : M ⊓ S = N ⊓ S
hf : J₁.Covers M f
⊢ Sieve.pullback f N ∈ J₁ Y

Tactic:
apply J₁.superset_covering (Sieve.pullback_monotone f inf_le_left)

Goal state after:
case refine_1.mp
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁).toFunctor S.arrows
M : Sieve X
hM : M ∈ (Functor.closedSieves J₁).obj (Opposite.op X)
N : Sieve X
hN : N ∈ (Functor.closedSieves J₁).obj (Opposite.op X)
hM₂ : x.IsAmalgamation ⟨M, hM⟩
hN₂ : x.IsAmalgamation ⟨N, hN⟩
Y : C
f : Y ⟶ X
q : ∀ ⦃Z : C⦄ (g : Z ⟶ X), S.arrows g → Sieve.pullback g M = Sieve.pullback g N
MSNS : M ⊓ S = N ⊓ S
hf : J₁.Covers M f
⊢ Sieve.pullback f (N ⊓ ?m.161) ∈ J₁ Y

C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁).toFunctor S.arrows
M : Sieve X
hM : M ∈ (Functor.closedSieves J₁).obj (Opposite.op X)
N : Sieve X
hN : N ∈ (Functor.closedSieves J₁).obj (Opposite.op X)
hM₂ : x.IsAmalgamation ⟨M, hM⟩
hN₂ : x.IsAmalgamation ⟨N, hN⟩
Y : C
f : Y ⟶ X
q : ∀ ⦃Z : C⦄ (g : Z ⟶ X), S.arrows g → Sieve.pullback g M = Sieve.pullback g N
MSNS : M ⊓ S = N ⊓ S
hf : J₁.Covers M f
⊢ Sieve X
Module: Mathlib.CategoryTheory.Sites.Closed

Goal state before:
pp: case refine_1.mpr
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁).toFunctor S.arrows
M : Sieve X
hM : M ∈ (Functor.closedSieves J₁).obj (Opposite.op X)
N : Sieve X
hN : N ∈ (Functor.closedSieves J₁).obj (Opposite.op X)
hM₂ : x.IsAmalgamation ⟨M, hM⟩
hN₂ : x.IsAmalgamation ⟨N, hN⟩
Y : C
f : Y ⟶ X
q : ∀ ⦃Z : C⦄ (g : Z ⟶ X), S.arrows g → Sieve.pullback g M = Sieve.pullback g N
MSNS : M ⊓ S = N ⊓ S
hf : J₁.Covers N f
⊢ Sieve.pullback f M ∈ J₁ Y

Tactic:
apply J₁.superset_covering (Sieve.pullback_monotone f inf_le_left)

Goal state after:
case refine_1.mpr
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁).toFunctor S.arrows
M : Sieve X
hM : M ∈ (Functor.closedSieves J₁).obj (Opposite.op X)
N : Sieve X
hN : N ∈ (Functor.closedSieves J₁).obj (Opposite.op X)
hM₂ : x.IsAmalgamation ⟨M, hM⟩
hN₂ : x.IsAmalgamation ⟨N, hN⟩
Y : C
f : Y ⟶ X
q : ∀ ⦃Z : C⦄ (g : Z ⟶ X), S.arrows g → Sieve.pullback g M = Sieve.pullback g N
MSNS : M ⊓ S = N ⊓ S
hf : J₁.Covers N f
⊢ Sieve.pullback f (M ⊓ ?m.197) ∈ J₁ Y

C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁).toFunctor S.arrows
M : Sieve X
hM : M ∈ (Functor.closedSieves J₁).obj (Opposite.op X)
N : Sieve X
hN : N ∈ (Functor.closedSieves J₁).obj (Opposite.op X)
hM₂ : x.IsAmalgamation ⟨M, hM⟩
hN₂ : x.IsAmalgamation ⟨N, hN⟩
Y : C
f : Y ⟶ X
q : ∀ ⦃Z : C⦄ (g : Z ⟶ X), S.arrows g → Sieve.pullback g M = Sieve.pullback g N
MSNS : M ⊓ S = N ⊓ S
hf : J₁.Covers N f
⊢ Sieve X
Module: Mathlib.CategoryTheory.Limits.Bicones

Goal state before:
pp: case left.diagram
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
val✝ : J
⊢ Fintype (Bicone.left ⟶ Bicone.diagram val✝)

Tactic:
exact
    { elems := {BiconeHom.left _}
      complete := fun f => by cases f; simp }

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
c : (X : C) → ClosureOperator (Sieve X)
pb : ∀ ⦃X Y : C⦄ (f : Y ⟶ X) (S : Sieve X), (c Y) (Sieve.pullback f S) = Sieve.pullback f ((c X) S)
X : C
S : Sieve X
⊢ (topologyOfClosureOperator c pb).close S = (c X) S

Tactic:
ext Y f

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
c : (X : C) → ClosureOperator (Sieve X)
pb : ∀ ⦃X Y : C⦄ (f : Y ⟶ X) (S : Sieve X), (c Y) (Sieve.pullback f S) = Sieve.pullback f ((c X) S)
X : C
S : Sieve X
Y : C
f : Y ⟶ X
⊢ ((topologyOfClosureOperator c pb).close S).arrows f ↔ ((c X) S).arrows f
Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero

Goal state before:
pp: case refine_2
C : Type u
inst✝² : Category.{v, u} C
K : Precoverage C
inst✝¹ : K.IsStableUnderComposition
inst✝ : K.HasIsos
X : C
E F : PreZeroHypercover X
e : E ≅ F
hE : E.presieve₀ ∈ K.coverings X
this : F.presieve₀ = Presieve.ofArrows (fun i ↦ F.X i.fst) fun i ↦ e.inv.h₀ i.fst ≫ E.f (e.inv.s₀ i.fst)
i : F.I₀
⊢ Presieve.singleton (e.inv.h₀ i) ∈ K.coverings (E.X (e.inv.s₀ i))

Tactic:
exact K.mem_coverings_of_isIso _

Goal state after:
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:
by intros; ext; simp

Goal state after:
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:
by intros; ext; simp

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
ι : Type (max u_4 u_3)
Y : ι → C
f : (i : ι) → Y i ⟶ X
inst✝¹ : (ofArrows Y f).HasPairwisePullbacks
inst✝ : F.PreservesPairwisePullbacks (ofArrows Y f)
this : (ofArrows (fun i ↦ F.obj (Y i)) fun i ↦ F.map (f i)).HasPairwisePullbacks
⊢ IsSheafFor (F.op ⋙ P) (ofArrows Y f) ↔ IsSheafFor P (ofArrows (fun i ↦ F.obj (Y i)) fun i ↦ F.map (f i))

Tactic:
Presieve.isSheafFor_arrows_iff_pullbacks

Goal state after:
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
ι : Type (max u_4 u_3)
Y : ι → C
f : (i : ι) → Y i ⟶ X
inst✝¹ : (ofArrows Y f).HasPairwisePullbacks
inst✝ : F.PreservesPairwisePullbacks (ofArrows Y f)
this : (ofArrows (fun i ↦ F.obj (Y i)) fun i ↦ F.map (f i)).HasPairwisePullbacks
⊢ (∀ (x : (i : ι) → (F.op ⋙ P).obj (Opposite.op (Y i))),
      Arrows.PullbackCompatible (F.op ⋙ P) f x →
        ∃! t, ∀ (i : ι), (ConcreteCategory.hom ((F.op ⋙ P).map (f i).op)) t = x i) ↔
    ∀ (x : (i : ι) → P.obj (Opposite.op (F.obj (Y i)))),
      Arrows.PullbackCompatible P (fun i ↦ F.map (f i)) x →
        ∃! t, ∀ (i : ι), (ConcreteCategory.hom (P.map (F.map (f i)).op)) t = x i
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},
    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:
x

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
⊢ 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.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:
e

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₂
e : 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: C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
inst✝ : HasPullbacks C
i j : E.I₀ × F.I₀
W : C
p₁ : W ⟶ pullback (E.f i.1) (F.f i.2)
p₂ : W ⟶ pullback (E.f j.1) (F.f j.2)
w : p₁ ≫ pullback.fst (E.f i.1) (F.f i.2) ≫ E.f i.1 = p₂ ≫ pullback.fst (E.f j.1) (F.f j.2) ≫ E.f j.1
⊢ (E.inter F).sieve₁ p₁ p₂ =
    Sieve.bind (E.sieve₁ (p₁ ≫ pullback.fst (E.f i.1) (F.f i.2)) (p₂ ≫ pullback.fst (E.f j.1) (F.f j.2))).arrows
      fun x f x_1 ↦
      Sieve.pullback f (F.sieve₁ (p₁ ≫ pullback.snd (E.f i.1) (F.f i.2)) (p₂ ≫ pullback.snd (E.f j.1) (F.f j.2)))

Tactic:
ext Y f

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
inst✝ : HasPullbacks C
i j : E.I₀ × F.I₀
W : C
p₁ : W ⟶ pullback (E.f i.1) (F.f i.2)
p₂ : W ⟶ pullback (E.f j.1) (F.f j.2)
w : p₁ ≫ pullback.fst (E.f i.1) (F.f i.2) ≫ E.f i.1 = p₂ ≫ pullback.fst (E.f j.1) (F.f j.2) ≫ E.f j.1
Y : C
f : Y ⟶ W
⊢ ((E.inter F).sieve₁ p₁ p₂).arrows f ↔
    (Sieve.bind (E.sieve₁ (p₁ ≫ pullback.fst (E.f i.1) (F.f i.2)) (p₂ ≫ pullback.fst (E.f j.1) (F.f j.2))).arrows
          fun x f x_1 ↦
          Sieve.pullback f
            (F.sieve₁ (p₁ ≫ pullback.snd (E.f i.1) (F.f i.2)) (p₂ ≫ pullback.snd (E.f j.1) (F.f j.2)))).arrows
      f
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.SheafEquiv

Goal state before:
pp: case left
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₁ f₂ : (yoneda.obj (((G.op.ran ⋙ (whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj Y.obj).obj (op U))).obj (op X)
⊢ (ConcreteCategory.hom ((yoneda.map ((G.op.ranCounit.app Y.obj).app (op U))).app (op X))) f₁ =
      (ConcreteCategory.hom ((yoneda.map ((G.op.ranCounit.app Y.obj).app (op U))).app (op X))) f₂ →
    f₁ = f₂

Tactic:
e

Goal state after:
case left
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₁ f₂ : (yoneda.obj (((G.op.ran ⋙ (whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj Y.obj).obj (op U))).obj (op X)
e :
  (ConcreteCategory.hom ((yoneda.map ((G.op.ranCounit.app Y.obj).app (op U))).app (op X))) f₁ =
    (ConcreteCategory.hom ((yoneda.map ((G.op.ranCounit.app Y.obj).app (op U))).app (op X))) f₂
⊢ f₁ = 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
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},
    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:
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
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
⊢ 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
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
inst✝ : G.IsContinuous J K
ℱ ℱ' : Sheaf K A
α β : ℱ ⟶ ℱ'
⊢ (G.sheafPushforwardContinuous A J K).map α = (G.sheafPushforwardContinuous A J K).map β → α = β

Tactic:
e

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
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
inst✝ : G.IsContinuous J K
ℱ ℱ' : Sheaf K A
α β : ℱ ⟶ ℱ'
e : (G.sheafPushforwardContinuous A J K).map α = (G.sheafPushforwardContinuous A J K).map β
⊢ α = β
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
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
inst✝ : G.IsContinuous J K
ℱ ℱ' : Sheaf K A
α β : ℱ ⟶ ℱ'
e : G.op.whiskerLeft α.hom = G.op.whiskerLeft β.hom
⊢ sheafHom (G.op.whiskerLeft α.hom) = sheafHom (G.op.whiskerLeft β.hom)

Tactic:
e

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
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
inst✝ : G.IsContinuous J K
ℱ ℱ' : Sheaf K A
α β : ℱ ⟶ ℱ'
e : G.op.whiskerLeft α.hom = G.op.whiskerLeft β.hom
⊢ sheafHom (G.op.whiskerLeft β.hom) = sheafHom (G.op.whiskerLeft β.hom)
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
g : G.obj Y ⟶ G.obj Z
T₀ : C
a : T₀ ⟶ X
b : T₀ ⟶ Y
fac₁ : G.map b = G.map a ≫ f
U₀ : C
c : U₀ ⟶ T₀
d : U₀ ⟶ Z
fac₂ : G.map d = G.map (c ≫ b) ≫ g
⊢ mapPreimage K G F (f ≫ g) ≫ F.obj.map (c ≫ a).op = mapPreimage K G F g ≫ mapPreimage K G F f ≫ F.obj.map (c ≫ a).op

Tactic:
rw [mapPreimage_map_of_fac K G F (f ≫ g) (c ≫ a) d,
        mapPreimage_map_of_fac K G F f (c ≫ a) (c ≫ b),
        mapPreimage_map_of_fac K G F g (c ≫ b) d]

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
g : G.obj Y ⟶ G.obj Z
T₀ : C
a : T₀ ⟶ X
b : T₀ ⟶ Y
fac₁ : G.map b = G.map a ≫ f
U₀ : C
c : U₀ ⟶ T₀
d : U₀ ⟶ Z
fac₂ : G.map d = G.map (c ≫ b) ≫ g
⊢ G.map (c ≫ b) ≫ g = G.map d

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
g : G.obj Y ⟶ G.obj Z
T₀ : C
a : T₀ ⟶ X
b : T₀ ⟶ Y
fac₁ : G.map b = G.map a ≫ f
U₀ : C
c : U₀ ⟶ T₀
d : U₀ ⟶ Z
fac₂ : G.map d = G.map (c ≫ b) ≫ g
⊢ G.map (c ≫ a) ≫ f = G.map (c ≫ b)

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
g : G.obj Y ⟶ G.obj Z
T₀ : C
a : T₀ ⟶ X
b : T₀ ⟶ Y
fac₁ : G.map b = G.map a ≫ f
U₀ : C
c : U₀ ⟶ T₀
d : U₀ ⟶ Z
fac₂ : G.map d = G.map (c ≫ b) ≫ g
⊢ G.map (c ≫ a) ≫ f ≫ g = G.map d
Module: Mathlib.CategoryTheory.Sites.Canonical

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P✝ : Cᵒᵖ ⥤ Type w
X✝ : C
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type w
X : C
S : Sieve X
hS : S ∈ {S | ∀ (Y : C) (f : Y ⟶ X), Presieve.IsSheafFor P (Sieve.pullback f S).arrows}
R : Sieve X
hR :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    S.arrows f → Sieve.pullback f R ∈ {S | ∀ (Y_1 : C) (f : Y_1 ⟶ Y), Presieve.IsSheafFor P (Sieve.pullback f S).arrows}
Z : C
g : Z ⟶ X
⊢ Presieve.IsSheafFor P (Sieve.pullback g R).arrows

Tactic:
refine Presieve.isSheafFor_trans P (pullback g S) _ (hS Z g) ?_ ?_
    · intro Y f _
      rw [← pullback_comp]
      apply (hS _ _).isSeparatedFor
    · intro Y f hf
      have := hR hf _ (𝟙 _)
      rw [pullback_id, pullback_comp] at this
      apply this

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
K : GrothendieckTopology D
e✝ : C ≌ D
G : D ⥤ C
A : Type u₃
inst✝¹ : Category.{v₃, u₃} A
inst✝ : G.IsEquivalence
U : C
e : C ≌ D := G.asEquivalence.symm
⊢ Sieve.coverByImage G U = ⊤

Tactic:
ext Y f

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
K : GrothendieckTopology D
e✝ : C ≌ D
G : D ⥤ C
A : Type u₃
inst✝¹ : Category.{v₃, u₃} A
inst✝ : G.IsEquivalence
U : C
e : C ≌ D := G.asEquivalence.symm
Y : C
f : Y ⟶ U
⊢ (Sieve.coverByImage G U).arrows f ↔ ⊤.arrows f