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

Goal state before:
pp: case refine_1
C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝⁴ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst✝³ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝² : ConcreteCategory A FA
F₁ F₂ F₃ : Cᵒᵖ ⥤ A
f₁ : F₁ ⟶ F₂
f₂ : F₂ ⟶ F₃
inst✝¹ : IsLocallySurjective J (f₁ ≫ f₂)
inst✝ : IsLocallyInjective J f₂
X : C
x : ToType (F₂.obj (op X))
S : Sieve X := imageSieve (f₁ ≫ f₂) ((ConcreteCategory.hom (f₂.app (op X))) x)
T : ⦃Y : C⦄ → (f : Y ⟶ X) → S.arrows f → Sieve Y :=
  fun Y f hf ↦
    equalizerSieve
      ((ConcreteCategory.hom (f₁.app (op Y))) (localPreimage (f₁ ≫ f₂) ((ConcreteCategory.hom (f₂.app (op X))) x) f hf))
      ((ConcreteCategory.hom (F₂.map f.op)) x)
⊢ Sieve.bind S.arrows T ≤ imageSieve f₁ x

Tactic:
rintro Y _ ⟨Z, a, g, hg, ha, rfl⟩

Goal state after:
case refine_1
C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝⁴ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst✝³ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝² : ConcreteCategory A FA
F₁ F₂ F₃ : Cᵒᵖ ⥤ A
f₁ : F₁ ⟶ F₂
f₂ : F₂ ⟶ F₃
inst✝¹ : IsLocallySurjective J (f₁ ≫ f₂)
inst✝ : IsLocallyInjective J f₂
X : C
x : ToType (F₂.obj (op X))
S : Sieve X := imageSieve (f₁ ≫ f₂) ((ConcreteCategory.hom (f₂.app (op X))) x)
T : ⦃Y : C⦄ → (f : Y ⟶ X) → S.arrows f → Sieve Y :=
  fun Y f hf ↦
    equalizerSieve
      ((ConcreteCategory.hom (f₁.app (op Y))) (localPreimage (f₁ ≫ f₂) ((ConcreteCategory.hom (f₂.app (op X))) x) f hf))
      ((ConcreteCategory.hom (F₂.map f.op)) x)
Y Z : C
a : Y ⟶ Z
g : Z ⟶ unop (op X)
hg : S.arrows g
ha : (T g hg).arrows a
⊢ (imageSieve f₁ x).arrows (a ≫ g)
Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension

Goal state before:
pp: case succ
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)
k : ℕ
hk : ∀ ⦃d : ℕ⦄ ⦃Y : C⦄ (e : Ext X Y d), d = n + k → e = 0
d : ℕ
Y : C
hd✝ : d = n + (k + 1)
p : InjectivePresentation Y
h : { X₁ := Y, X₂ := p.J, X₃ := cokernel p.f, f := p.f, g := cokernel.π p.f, zero := ⋯ }.ShortExact
hd : n + k + 1 = d
x : Ext X { X₁ := Y, X₂ := p.J, X₃ := cokernel p.f, f := p.f, g := cokernel.π p.f, zero := ⋯ }.X₃ (n + k)
⊢ x.comp h.extClass hd = 0

Tactic:
simp [hk x rfl]

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

Goal state before:
pp: J : Type u₁
inst✝ : Category.{v₁, u₁} J
X✝ Y✝ : Bicone J
f : X✝ ⟶ Y✝
⊢ 𝟙 X✝ ≫ f = f

Tactic:
by cases f <;> simp

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

Goal state before:
pp: J : Type u₁
inst✝ : Category.{v₁, u₁} J
X✝ Y✝ : Bicone J
f : X✝ ⟶ Y✝
⊢ f ≫ 𝟙 Y✝ = f

Tactic:
by cases f <;> simp

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⟩
Y : C
f : Y ⟶ X
q : ∀ ⦃Z : C⦄ (g : Z ⟶ X), S.arrows g → Sieve.pullback g M = Sieve.pullback g N
⊢ J₁.Covers M f ↔ J₁.Covers N f

Tactic:
have MSNS : M ⊓ S = N ⊓ S := by
      ext
      grind [Sieve.inter_apply, Sieve.mem_iff_pullback_eq_top]

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
q : ∀ ⦃Z : C⦄ (g : Z ⟶ X), S.arrows g → Sieve.pullback g M = Sieve.pullback g N
MSNS : M ⊓ S = N ⊓ S
⊢ J₁.Covers M f ↔ J₁.Covers N f
Module: Mathlib.CategoryTheory.Sites.Coverage

Goal state before:
pp: C : Type u_2
inst✝ : Category.{v_1, u_2} C
K L : Coverage C
P : Cᵒᵖ ⥤ Type u_1
h : (∀ {X : C}, ∀ R ∈ K.coverings X, IsSheafFor P R) ∧ ∀ {X : C}, ∀ R ∈ L.coverings X, IsSheafFor P R
⊢ IsSheaf (K ⊔ L).toGrothendieck P

Tactic:
rw [isSheaf_coverage]

Goal state after:
C : Type u_2
inst✝ : Category.{v_1, u_2} C
K L : Coverage C
P : Cᵒᵖ ⥤ Type u_1
h : (∀ {X : C}, ∀ R ∈ K.coverings X, IsSheafFor P R) ∧ ∀ {X : C}, ∀ R ∈ L.coverings X, IsSheafFor P R
⊢ ∀ {X : C}, ∀ R ∈ (K ⊔ L).coverings X, IsSheafFor P R
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 using hgg

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

Goal state before:
pp: case refine_1.transitive
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 T : Sieve X
hS : J.Saturate X S
hT : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → J.Saturate Y (Sieve.pullback f T)
hleT : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → ∃ R ∈ J.coverings Y, R ≤ (Sieve.pullback f T).arrows
R : Presieve X
hR : ∃ 𝒰, R = Presieve.ofArrows 𝒰.X 𝒰.f
hle : R ≤ S.arrows
⊢ ∃ R ∈ J.coverings X, R ≤ T.arrows

Tactic:
obtain ⟨E, rfl⟩ := hR

Goal state after:
case refine_1.transitive
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 T : Sieve X
hS : J.Saturate X S
hT : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → J.Saturate Y (Sieve.pullback f T)
hleT : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → ∃ R ∈ J.coverings Y, R ≤ (Sieve.pullback f T).arrows
E : J.ZeroHypercover X
hle : Presieve.ofArrows E.X E.f ≤ S.arrows
⊢ ∃ R ∈ J.coverings X, R ≤ T.arrows
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
⊢ (∀ (x : (i : ι) → P.obj (Opposite.op (F.obj (Y i)))),
      (∀ (i j : ι),
          (ConcreteCategory.hom (P.map (F.map (pullback.fst (f i) (f j))).op)) (x i) =
            (ConcreteCategory.hom (P.map (F.map (pullback.snd (f i) (f j))).op)) (x j)) →
        ∃! t, ∀ (i : ι), (ConcreteCategory.hom (P.map (F.map (f i)).op)) t = x i) ↔
    ∀ (x : (i : ι) → P.obj (Opposite.op (F.obj (Y i)))),
      (∀ (i j : ι),
          (ConcreteCategory.hom (P.map (pullback.fst (F.map (f i)) (F.map (f j))).op)) (x i) =
            (ConcreteCategory.hom (P.map (pullback.snd (F.map (f i)) (F.map (f j))).op)) (x j)) →
        ∃! t, ∀ (i : ι), (ConcreteCategory.hom (P.map (F.map (f i)).op)) t = x i

Tactic:
congr! with x

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 : ι) → P.obj (Opposite.op (F.obj (Y i)))
⊢ ((∀ (i j : ι),
        (ConcreteCategory.hom (P.map (F.map (pullback.fst (f i) (f j))).op)) (x i) =
          (ConcreteCategory.hom (P.map (F.map (pullback.snd (f i) (f j))).op)) (x j)) →
      ∃! t, ∀ (i : ι), (ConcreteCategory.hom (P.map (F.map (f i)).op)) t = x i) ↔
    (∀ (i j : ι),
        (ConcreteCategory.hom (P.map (pullback.fst (F.map (f i)) (F.map (f j))).op)) (x i) =
          (ConcreteCategory.hom (P.map (pullback.snd (F.map (f i)) (F.map (f j))).op)) (x j)) →
      ∃! t, ∀ (i : ι), (ConcreteCategory.hom (P.map (F.map (f i)).op)) t = x 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
G : C ⥤ D
K : GrothendieckTopology D
h : ∀ (B : D), ∃ X f, Sieve.generate (Presieve.singleton f) ∈ K B
B : D
⊢ Sieve.coverByImage G B ∈ K B

Tactic:
obtain ⟨X, f, h⟩ := h B
    refine K.superset_covering ?_ h
    intro Y f ⟨Z, g, _, h, w⟩
    cases h
    exact ⟨⟨_, g, _, 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
G : C ⥤ D
ℱ : Dᵒᵖ ⥤ Type v
ℱ' : Sheaf K (Type v)
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
X : D
x : ℱ.obj (op X)
this :
  ∀ {Z : D} {W₁ W₂ : C} (iWX₁ : G.obj W₁ ⟶ X) (iWX₂ : G.obj W₂ ⟶ X) (iZW₁ : Z ⟶ G.obj W₁) (iZW₂ : Z ⟶ G.obj W₂),
    iZW₁ ≫ iWX₁ = iZW₂ ≫ iWX₂ →
      (ConcreteCategory.hom (ℱ'.obj.map iZW₁.op))
          ((ConcreteCategory.hom (α.app (op W₁))) ((ConcreteCategory.hom (ℱ.map iWX₁.op)) x)) =
        (ConcreteCategory.hom (ℱ'.obj.map iZW₂.op))
          ((ConcreteCategory.hom (α.app (op W₂))) ((ConcreteCategory.hom (ℱ.map iWX₂.op)) x))
Y₁ Y₂ Z : D
iZY₁ : Z ⟶ Y₁
iZY₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
h₁ : coverByImage G X f₁
h₂ : coverByImage G X f₂
e : iZY₁ ≫ f₁ = iZY₂ ≫ f₂
⊢ (ConcreteCategory.hom (ℱ'.obj.map (iZY₁ ≫ (Nonempty.some h₁).lift).op))
      ((ConcreteCategory.hom (α.app (op (Nonempty.some h₁).1)))
        ((ConcreteCategory.hom (ℱ.map (Nonempty.some h₁).map.op)) x)) =
    (ConcreteCategory.hom (ℱ'.obj.map (iZY₂ ≫ (Nonempty.some h₂).lift).op))
      ((ConcreteCategory.hom (α.app (op (Nonempty.some h₂).1)))
        ((ConcreteCategory.hom (ℱ.map (Nonempty.some h₂).map.op)) x))

Tactic:
generalize Nonempty.some h₁ = l₁

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
ℱ : Dᵒᵖ ⥤ Type v
ℱ' : Sheaf K (Type v)
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
X : D
x : ℱ.obj (op X)
this :
  ∀ {Z : D} {W₁ W₂ : C} (iWX₁ : G.obj W₁ ⟶ X) (iWX₂ : G.obj W₂ ⟶ X) (iZW₁ : Z ⟶ G.obj W₁) (iZW₂ : Z ⟶ G.obj W₂),
    iZW₁ ≫ iWX₁ = iZW₂ ≫ iWX₂ →
      (ConcreteCategory.hom (ℱ'.obj.map iZW₁.op))
          ((ConcreteCategory.hom (α.app (op W₁))) ((ConcreteCategory.hom (ℱ.map iWX₁.op)) x)) =
        (ConcreteCategory.hom (ℱ'.obj.map iZW₂.op))
          ((ConcreteCategory.hom (α.app (op W₂))) ((ConcreteCategory.hom (ℱ.map iWX₂.op)) x))
Y₁ Y₂ Z : D
iZY₁ : Z ⟶ Y₁
iZY₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
h₁ : coverByImage G X f₁
h₂ : coverByImage G X f₂
e : iZY₁ ≫ f₁ = iZY₂ ≫ f₂
l₁ : CoverByImageStructure G f₁
⊢ (ConcreteCategory.hom (ℱ'.obj.map (iZY₁ ≫ l₁.lift).op))
      ((ConcreteCategory.hom (α.app (op l₁.1))) ((ConcreteCategory.hom (ℱ.map l₁.map.op)) x)) =
    (ConcreteCategory.hom (ℱ'.obj.map (iZY₂ ≫ (Nonempty.some h₂).lift).op))
      ((ConcreteCategory.hom (α.app (op (Nonempty.some h₂).1)))
        ((ConcreteCategory.hom (ℱ.map (Nonempty.some h₂).map.op)) 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
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
⊢ ⋯.amalgamate ⟨G.imageSieve f, ⋯⟩
        (fun x ↦
          match x with
          | { Y := W₀, f := a, hf := ha } => F.obj.map (Exists.choose ha).op)
        ⋯ ≫
      F.obj.map (a ≫ p).op =
    F.obj.map g.op ≫ F.obj.map a.op

Tactic:
rw [F.2.amalgamate_map ⟨_, imageSieve_mem J K G f⟩
        (fun ⟨W₀, a, ha⟩ ↦ F.obj.map ha.choose.op) _ ⟨W₀, a ≫ p, ha⟩,
        ← Functor.map_comp, ← op_comp]

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
⊢ (match { Y := W₀, f := a ≫ p, hf := ha } with
    | { Y := W₀, f := a, hf := ha } => F.obj.map (Exists.choose ha).op) =
    F.obj.map (a ≫ g).op
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology

Goal state before:
pp: C : Type u_3
D : Type u_4
inst✝⁷ : Category.{v_3, u_3} C
inst✝⁶ : Category.{v_4, u_4} D
F : C ⥤ D
K : Precoverage D
inst✝⁵ : K.HasIsos
inst✝⁴ : K.IsStableUnderBaseChange
inst✝³ : K.IsStableUnderComposition
inst✝² : K.HasPullbacks
inst✝¹ : F.Faithful
inst✝ : F.Full
H : ∀ {S : C} {R : Presieve (F.obj S)}, R ∈ K.coverings (F.obj S) → map F (functorPullback F R) ∈ K.coverings (F.obj S)
⊢ (comap F K).toGrothendieck = F.restrictedTopology K.toGrothendieck

Tactic:
have : F.LocallyCoverDense K.toGrothendieck :=
    K.locallyCoverDense_of_map_functorPullback_mem F H
  refine le_antisymm ?_ fun X T hT ↦ ?_
  · apply toGrothendieck_comap_le_restrictedTopology
  · rw [Functor.mem_restrictedTopology_iff] at hT
    rw [Precoverage.mem_toGrothendieck_iff_of_isStableUnderComposition] at hT
    obtain ⟨R, hR, hle⟩ := hT
    refine GrothendieckTopology.superset_covering
        (S := Sieve.generate (Presieve.functorPullback F R)) _ ?_ ?_
    · refine le_trans (le_trans (Sieve.generate_functorPullback_le F R)
        (Sieve.functorPullback_monotone _ _ (Sieve.generate_mono hle))) ?_
      rw [Sieve.generate_sieve, Sieve.functorPullback_functorPushforward_eq]
    · exact Precoverage.generate_mem_toGrothendieck (H hR)

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 ∈ J U

Tactic:
convert! J.top_mem U

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
⊢ Sieve.coverByImage G U = ⊤
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
inst✝³ : IsDenseSubsite K J e.inverse
A : Type u_1
inst✝² : Category.{v_1, u_1} A
B : Type u_2
inst✝¹ : Category.{v_2, u_2} B
F : A ⥤ B
inst✝ : K.HasSheafCompose F
P : Cᵒᵖ ⥤ A
hP : Presheaf.IsSheaf J P
⊢ Presheaf.IsSheaf J (P ⋙ F)

Tactic:
have hP' : Presheaf.IsSheaf K (e.inverse.op ⋙ P ⋙ F) := by
      change Presheaf.IsSheaf K ((_ ⋙ _) ⋙ _)
      apply HasSheafCompose.isSheaf
      exact e.inverse.op_comp_isSheaf K J ⟨P, hP⟩

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
inst✝³ : IsDenseSubsite K J e.inverse
A : Type u_1
inst✝² : Category.{v_1, u_1} A
B : Type u_2
inst✝¹ : Category.{v_2, u_2} B
F : A ⥤ B
inst✝ : K.HasSheafCompose F
P : Cᵒᵖ ⥤ A
hP : Presheaf.IsSheaf J P
hP' : Presheaf.IsSheaf K (e.inverse.op ⋙ P ⋙ F)
⊢ Presheaf.IsSheaf J (P ⋙ F)
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
G : D ⥤ C
A : Type u₃
inst✝⁷ : Category.{v₃, u₃} A
B : Type u₄
inst✝⁶ : Category.{v₄, u₄} B
F : A ⥤ B
inst✝⁵ : G.IsCoverDense J
inst✝⁴ : G.Full
inst✝³ : G.IsContinuous K J
inst✝² : (G.sheafPushforwardContinuous B K J).EssSurj
inst✝¹ : (G.sheafPushforwardContinuous A K J).EssSurj
inst✝ : K.PreservesSheafification F
P Q : Cᵒᵖ ⥤ A
f : P ⟶ Q
hf : K.W (G.op.whiskerLeft f)
this : K.W ((G.op.associator P F).hom ≫ G.op.whiskerLeft (whiskerRight f F) ≫ (G.op.associator Q F).inv)
⊢ J.W.inverseImage ((whiskeringRight Cᵒᵖ A B).obj F) f

Tactic:
have := K.W.of_postcomp (W' := MorphismProperty.isomorphisms _) _ _ (Iso.isIso_inv _) <|
      K.W.of_precomp (W' := MorphismProperty.isomorphisms _) _ _ (Iso.isIso_hom _) this

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
G : D ⥤ C
A : Type u₃
inst✝⁷ : Category.{v₃, u₃} A
B : Type u₄
inst✝⁶ : Category.{v₄, u₄} B
F : A ⥤ B
inst✝⁵ : G.IsCoverDense J
inst✝⁴ : G.Full
inst✝³ : G.IsContinuous K J
inst✝² : (G.sheafPushforwardContinuous B K J).EssSurj
inst✝¹ : (G.sheafPushforwardContinuous A K J).EssSurj
inst✝ : K.PreservesSheafification F
P Q : Cᵒᵖ ⥤ A
f : P ⟶ Q
hf : K.W (G.op.whiskerLeft f)
this✝ : K.W ((G.op.associator P F).hom ≫ G.op.whiskerLeft (whiskerRight f F) ≫ (G.op.associator Q F).inv)
this : K.W (G.op.whiskerLeft (whiskerRight f F))
⊢ J.W.inverseImage ((whiskeringRight Cᵒᵖ A B).obj F) f
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
hg : ((overEquiv Y).symm (generate R)).arrows g
⊢ (generate (Presieve.functorPullback (Over.forget X) R)).arrows g

Tactic:
rw [overEquiv_symm_iff] at hg
    obtain ⟨W, p, q, hq, hpq⟩ := hg
    refine ⟨.mk (q ≫ Y.hom), Over.homMk p (by simp [reassoc_of% hpq]), Over.homMk q rfl, hq, ?_⟩
    ext
    exact hpq

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

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X : C
S : J.Cover X
Y : C
f : Y ⟶ X
hf : (↑S).arrows f
⊢ S.preOneHypercover.sieve₀.arrows f

Tactic:
exact Sieve.ofArrows_mk _ _ ({ hf := hf, .. } : S.Arrow)

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F : C ⥤ D
X : C
U : Over X
S : Sieve U
⊢ (overEquiv ((Over.post F).obj U)) (functorPushforward (Over.post F) S) = functorPushforward F ((overEquiv U) S)

Tactic:
by
  simp [Sieve.overEquiv, ← Sieve.functorPushforward_comp, ← Over.post_forget_eq_forget_comp]

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

Goal state before:
pp: case e'_2
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X Y : C
f : X ⟶ Y
F : Sheaf (J.over Y) (Type u_1)
Z : Over X
x✝ : Presieve Z
x : Presieve.FamilyOfElements ((Over.map f).op ⋙ F.obj) x✝
hx : x.Compatible
Y₁ Y₂ : Over X
W : Over Y
f₁ : W ⟶ (Over.map f).obj Y₁
f₂ : W ⟶ (Over.map f).obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : x✝ g₁
hg₂ : x✝ g₂
h : f₁ ≫ (Over.map f).map g₁ = f₂ ≫ (Over.map f).map g₂
W' : Over X := Over.mk (Over.Hom.left f₁ ≫ Y₁.hom)
g₁' : W' ⟶ Y₁ := Over.homMk (Over.Hom.left f₁) ⋯
g₂' : W' ⟶ Y₂ := Over.homMk (Over.Hom.left f₂) ⋯
e : (Over.map f).obj W' ≅ W := Over.isoMk (Iso.refl ((Over.map f).obj W').left) ⋯
⊢ f₁.op = ((Over.map f).map (Over.homMk (Over.Hom.left f₁) ⋯)).op ≫ (Over.isoMk (Iso.refl W.left) ⋯).inv.op

Tactic:
rw [← op_comp]

Goal state after:
case e'_2
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X Y : C
f : X ⟶ Y
F : Sheaf (J.over Y) (Type u_1)
Z : Over X
x✝ : Presieve Z
x : Presieve.FamilyOfElements ((Over.map f).op ⋙ F.obj) x✝
hx : x.Compatible
Y₁ Y₂ : Over X
W : Over Y
f₁ : W ⟶ (Over.map f).obj Y₁
f₂ : W ⟶ (Over.map f).obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : x✝ g₁
hg₂ : x✝ g₂
h : f₁ ≫ (Over.map f).map g₁ = f₂ ≫ (Over.map f).map g₂
W' : Over X := Over.mk (Over.Hom.left f₁ ≫ Y₁.hom)
g₁' : W' ⟶ Y₁ := Over.homMk (Over.Hom.left f₁) ⋯
g₂' : W' ⟶ Y₂ := Over.homMk (Over.Hom.left f₂) ⋯
e : (Over.map f).obj W' ≅ W := Over.isoMk (Iso.refl ((Over.map f).obj W').left) ⋯
⊢ f₁.op = ((Over.isoMk (Iso.refl W.left) ⋯).inv ≫ (Over.map f).map (Over.homMk (Over.Hom.left f₁) ⋯)).op
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: case e'_3
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X Y : C
f : X ⟶ Y
F : Sheaf (J.over Y) (Type u_1)
Z : Over X
x✝ : Presieve Z
x : Presieve.FamilyOfElements ((Over.map f).op ⋙ F.obj) x✝
hx : x.Compatible
Y₁ Y₂ : Over X
W : Over Y
f₁ : W ⟶ (Over.map f).obj Y₁
f₂ : W ⟶ (Over.map f).obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : x✝ g₁
hg₂ : x✝ g₂
h : f₁ ≫ (Over.map f).map g₁ = f₂ ≫ (Over.map f).map g₂
W' : Over X := Over.mk (Over.Hom.left f₁ ≫ Y₁.hom)
g₁' : W' ⟶ Y₁ := Over.homMk (Over.Hom.left f₁) ⋯
g₂' : W' ⟶ Y₂ := Over.homMk (Over.Hom.left f₂) ⋯
e : (Over.map f).obj W' ≅ W := Over.isoMk (Iso.refl ((Over.map f).obj W').left) ⋯
⊢ f₂.op = ((Over.map f).map (Over.homMk (Over.Hom.left f₂) ⋯)).op ≫ (Over.isoMk (Iso.refl W.left) ⋯).inv.op

Tactic:
rw [← op_comp]

Goal state after:
case e'_3
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X Y : C
f : X ⟶ Y
F : Sheaf (J.over Y) (Type u_1)
Z : Over X
x✝ : Presieve Z
x : Presieve.FamilyOfElements ((Over.map f).op ⋙ F.obj) x✝
hx : x.Compatible
Y₁ Y₂ : Over X
W : Over Y
f₁ : W ⟶ (Over.map f).obj Y₁
f₂ : W ⟶ (Over.map f).obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : x✝ g₁
hg₂ : x✝ g₂
h : f₁ ≫ (Over.map f).map g₁ = f₂ ≫ (Over.map f).map g₂
W' : Over X := Over.mk (Over.Hom.left f₁ ≫ Y₁.hom)
g₁' : W' ⟶ Y₁ := Over.homMk (Over.Hom.left f₁) ⋯
g₂' : W' ⟶ Y₂ := Over.homMk (Over.Hom.left f₂) ⋯
e : (Over.map f).obj W' ≅ W := Over.isoMk (Iso.refl ((Over.map f).obj W').left) ⋯
⊢ f₂.op = ((Over.isoMk (Iso.refl W.left) ⋯).inv ≫ (Over.map f).map (Over.homMk (Over.Hom.left f₂) ⋯)).op