mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Localization.Bousfield

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
P : ObjectProperty C
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
hf : P.isColocal f
hg : P.isColocal g
X : C
hX : P X
⊢ Function.Bijective fun f_1 ↦ f_1 ≫ f ≫ g

Tactic:
convert! Function.Bijective.comp (hg X hX) (hf X hX)

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
P : ObjectProperty C
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
hf : P.isColocal f
hg : P.isColocal g
X : C
hX : P X
x✝ : X ⟶ X✝
⊢ x✝ ≫ f ≫ g = ((fun f ↦ f ≫ g) ∘ fun f_1 ↦ f_1 ≫ f) x✝
Module: Mathlib.CategoryTheory.Sites.LocallyInjective

Goal state before:
pp: case mpr
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
FD : D → D → Type u_1
CD : D → Type w
inst✝¹ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝ : ConcreteCategory D FD
F : Cᵒᵖ ⥤ D
X : Cᵒᵖ
x y : ToType (F.obj X)
⊢ x = y → equalizerSieve x y = ⊤

Tactic:
· rintro rfl
    apply equalizerSieve_self_eq_top

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
FD : D → D → Type u_1
CD : D → Type w
inst✝¹ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝ : ConcreteCategory D FD
J : GrothendieckTopology C
F₁ F₂ : Cᵒᵖ ⥤ D
φ : F₁ ⟶ F₂
hφ : ∀ (X : Cᵒᵖ), Function.Injective ⇑(ConcreteCategory.hom (φ.app X))
X : Cᵒᵖ
x y : ToType (F₁.obj X)
h : (ConcreteCategory.hom (φ.app X)) x = (ConcreteCategory.hom (φ.app X)) y
⊢ equalizerSieve x y ∈ J (unop X)

Tactic:
convert! J.top_mem X.unop

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
FD : D → D → Type u_1
CD : D → Type w
inst✝¹ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝ : ConcreteCategory D FD
J : GrothendieckTopology C
F₁ F₂ : Cᵒᵖ ⥤ D
φ : F₁ ⟶ F₂
hφ : ∀ (X : Cᵒᵖ), Function.Injective ⇑(ConcreteCategory.hom (φ.app X))
X : Cᵒᵖ
x y : ToType (F₁.obj X)
h : (ConcreteCategory.hom (φ.app X)) x = (ConcreteCategory.hom (φ.app X)) y
⊢ equalizerSieve x y = ⊤
Module: Mathlib.CategoryTheory.Sites.LocallyInjective

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
FD : D → D → Type u_1
CD : D → Type w
inst✝² : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝¹ : ConcreteCategory D FD
J : GrothendieckTopology C
F₁ F₂ F₃ : Cᵒᵖ ⥤ D
φ : F₁ ⟶ F₂
ψ : F₂ ⟶ F₃
inst✝ : IsIso φ
X : Cᵒᵖ
⊢ Function.Bijective ⇑(ConcreteCategory.hom (φ.app X))

Tactic:
rw [bijective_iff_isIso_ofHom]

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
FD : D → D → Type u_1
CD : D → Type w
inst✝² : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝¹ : ConcreteCategory D FD
J : GrothendieckTopology C
F₁ F₂ F₃ : Cᵒᵖ ⥤ D
φ : F₁ ⟶ F₂
ψ : F₂ ⟶ F₃
inst✝ : IsIso φ
X : Cᵒᵖ
⊢ IsIso (↾⇑(ConcreteCategory.hom (φ.app X)))
Module: Mathlib.CategoryTheory.Sites.LocallySurjective

Goal state before:
pp: 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 G : Cᵒᵖ ⥤ A
f : F ⟶ G
U : C
s : ToType (G.obj (op U))
⊢ ∀ {Y Z : C} {f_1 : Y ⟶ U},
    (∃ t, (ConcreteCategory.hom (f.app (op Y))) t = (ConcreteCategory.hom (G.map f_1.op)) s) →
      ∀ (g : Z ⟶ Y), ∃ t, (ConcreteCategory.hom (f.app (op Z))) t = (ConcreteCategory.hom (G.map (g ≫ f_1).op)) s

Tactic:
rintro V W i ⟨t, ht⟩ j
    refine ⟨F.map j.op t, ?_⟩
    rw [op_comp, G.map_comp, ConcreteCategory.comp_apply, ← ht, NatTrans.naturality_apply f]

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

Goal state before:
pp: 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 G : Cᵒᵖ ⥤ A
f : F ⟶ G
inst✝ : IsIso f
U : Cᵒᵖ
⊢ Function.Bijective ⇑(ConcreteCategory.hom (f.app U))

Tactic:
rw [bijective_iff_isIso_ofHom]

Goal state after:
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 G : Cᵒᵖ ⥤ A
f : F ⟶ G
inst✝ : IsIso f
U : Cᵒᵖ
⊢ IsIso (↾⇑(ConcreteCategory.hom (f.app U)))
Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Limits

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
R : Sheaf J RingCat
F : D ⥤ SheafOfModules R
inst✝¹ :
  ∀ (X : Cᵒᵖ), Small.{v, max u₂ v} ↑((F ⋙ evaluation R X) ⋙ CategoryTheory.forget (ModuleCat ↑(R.obj.obj X))).sections
inst✝ : HasLimitsOfShape D AddCommGrpCat
X : Cᵒᵖ
⊢ Small.{v, max u₂ v}
    ↑(((F ⋙ forget R) ⋙ PresheafOfModules.evaluation R.obj X) ⋙
          CategoryTheory.forget (ModuleCat ↑(R.obj.obj X))).sections

Tactic:
by
  solve_by_elim

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

Goal state before:
pp: case x.sj
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : GrothendieckTopology C
R₀ R : Cᵒᵖ ⥤ RingCat
α : R₀ ⟶ R
inst✝¹ : Presheaf.IsLocallyInjective J α
M₀ : PresheafOfModules R₀
A : Cᵒᵖ ⥤ AddCommGrpCat
φ : M₀.presheaf ⟶ A
inst✝ : Presheaf.IsLocallyInjective J φ
hA : Presheaf.IsSeparated J A
Y : C
r₀ r₀' : ↑(R₀.obj (Opposite.op Y))
m₀ m₀' : ↑(M₀.obj (Opposite.op Y))
hr₀ : (ConcreteCategory.hom (α.app (Opposite.op Y))) r₀ = (ConcreteCategory.hom (α.app (Opposite.op Y))) r₀'
hm₀ : (ConcreteCategory.hom (φ.app (Opposite.op Y))) m₀ = (ConcreteCategory.hom (φ.app (Opposite.op Y))) m₀'
⊢ Presheaf.equalizerSieve m₀ m₀' ∈ J (Opposite.unop (Opposite.op Y))

Tactic:
· exact Presheaf.equalizerSieve_mem J φ _ _ hm₀

Goal state after:
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 : WithBot ℕ∞
hn : ∀ (i : ℕ), n < ↑i → HasProjectiveDimensionLT Y i
⊢ ∀ (i : ℕ), n < ↑i → HasProjectiveDimensionLT X i

Tactic:
intro i hi

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y : C
h : Retract X Y
n : WithBot ℕ∞
hn : ∀ (i : ℕ), n < ↑i → HasProjectiveDimensionLT Y i
i : ℕ
hi : n < ↑i
⊢ HasProjectiveDimensionLT X i
Module: Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete

Goal state before:
pp: I : Type u_1
B : Type u_2
inst✝² : Category.{v_1, u_1} I
inst✝¹ : Bicategory B
inst✝ : Strict B
F : I ⥤ B
b₀✝ b₁✝ b₂✝ : LocallyDiscrete I
g : b₁✝ ⟶ b₂✝
f : b₀✝.as ⟶ b₁✝.as
⊢ (match { as := f } ≫ g with
    | { as := f } => F.map f) =
    (match { as := f } with
      | { as := f } => F.map f) ≫
      match g with
      | { as := f } => F.map f

Tactic:
obtain ⟨g⟩ := g

Goal state after:
I : Type u_1
B : Type u_2
inst✝² : Category.{v_1, u_1} I
inst✝¹ : Bicategory B
inst✝ : Strict B
F : I ⥤ B
b₀✝ b₁✝ b₂✝ : LocallyDiscrete I
f : b₀✝.as ⟶ b₁✝.as
g : b₁✝.as ⟶ b₂✝.as
⊢ (match { as := f } ≫ { as := g } with
    | { as := f } => F.map f) =
    (match { as := f } with
      | { as := f } => F.map f) ≫
      match { as := g } with
      | { as := f } => F.map f
Module: Mathlib.CategoryTheory.Functor.Flat

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type v₁
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
F : C ⥤ D
inst✝ : RepresentablyFlat F
K : J ⥤ C
c : Cone K
hc : IsLimit c
s : Cone (K ⋙ F)
f₁ f₂ : s.pt ⟶ F.obj c.pt
h₁ : ∀ (j : J), f₁ ≫ (F.mapCone c).π.app j = s.π.app j
h₂ : ∀ (j : J), f₂ ≫ (F.mapCone c).π.app j = s.π.app j
α₁ : (F.mapCone c).toStructuredArrow ⋙ map f₁ ⟶ s.toStructuredArrow := { app := fun X ↦ eqToHom ⋯, naturality := ⋯ }
α₂ : (F.mapCone c).toStructuredArrow ⋙ map f₂ ⟶ s.toStructuredArrow := { app := fun X ↦ eqToHom ⋯, naturality := ⋯ }
c₁ : Cone (s.toStructuredArrow ⋙ pre s.pt K F) :=
  (Cone.postcompose (Functor.whiskerRight α₁ (pre s.pt K F))).obj (c.toStructuredArrowCone F f₁)
⊢ f₁ = f₂

Tactic:
let c₂ : Cone (s.toStructuredArrow ⋙ pre s.pt K F) :=
    (Cone.postcompose (Functor.whiskerRight α₂ (pre s.pt K F) :)).obj
      (c.toStructuredArrowCone F f₂)

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type v₁
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
F : C ⥤ D
inst✝ : RepresentablyFlat F
K : J ⥤ C
c : Cone K
hc : IsLimit c
s : Cone (K ⋙ F)
f₁ f₂ : s.pt ⟶ F.obj c.pt
h₁ : ∀ (j : J), f₁ ≫ (F.mapCone c).π.app j = s.π.app j
h₂ : ∀ (j : J), f₂ ≫ (F.mapCone c).π.app j = s.π.app j
α₁ : (F.mapCone c).toStructuredArrow ⋙ map f₁ ⟶ s.toStructuredArrow := { app := fun X ↦ eqToHom ⋯, naturality := ⋯ }
α₂ : (F.mapCone c).toStructuredArrow ⋙ map f₂ ⟶ s.toStructuredArrow := { app := fun X ↦ eqToHom ⋯, naturality := ⋯ }
c₁ : Cone (s.toStructuredArrow ⋙ pre s.pt K F) :=
  (Cone.postcompose (Functor.whiskerRight α₁ (pre s.pt K F))).obj (c.toStructuredArrowCone F f₁)
c₂ : Cone (s.toStructuredArrow ⋙ pre s.pt K F) :=
  (Cone.postcompose (Functor.whiskerRight α₂ (pre s.pt K F))).obj (c.toStructuredArrowCone F f₂)
⊢ f₁ = f₂
Module: Mathlib.CategoryTheory.Limits.Bicones

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

Tactic:
exact
    { elems := ∅
      complete := fun f => by cases f }

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

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

Tactic:
exact
    { elems := ∅
      complete := fun f => by cases f }

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

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

Tactic:
exact
    { elems := ∅
      complete := fun f => by cases f }

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

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

Tactic:
exact
    { elems := ∅
      complete := fun f => by cases f }

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
S✝ T✝ : C
E✝ : PreZeroHypercover S✝
F : PreZeroHypercover S✝
S T : C
f : S ⟶ T
E : PreZeroHypercover T
inst✝¹ : ∀ (i : E.I₀), HasPullback f (E.f i)
inst✝ : ∀ (i : E.I₀), HasPullback (E.f i) f
⊢ ({ s₀ := id, h₀ := fun i ↦ (pullbackSymmetry f (E.f i)).hom, w₀ := ⋯ } ≫
        { s₀ := id, h₀ := fun i ↦ (pullbackSymmetry f (E.f i)).inv, w₀ := ⋯ }).h₀ ≍
    (𝟙 (pullback₁ f E)).h₀

Tactic:
simp only [heq_eq_eq]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
S✝ T✝ : C
E✝ : PreZeroHypercover S✝
F : PreZeroHypercover S✝
S T : C
f : S ⟶ T
E : PreZeroHypercover T
inst✝¹ : ∀ (i : E.I₀), HasPullback f (E.f i)
inst✝ : ∀ (i : E.I₀), HasPullback (E.f i) f
⊢ ({ s₀ := id, h₀ := fun i ↦ (pullbackSymmetry f (E.f i)).hom, w₀ := ⋯ } ≫
        { s₀ := id, h₀ := fun i ↦ (pullbackSymmetry f (E.f i)).inv, w₀ := ⋯ }).h₀ =
    (𝟙 (pullback₁ f E)).h₀
Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
S✝ T✝ : C
E✝ : PreZeroHypercover S✝
F : PreZeroHypercover S✝
S T : C
f : S ⟶ T
E : PreZeroHypercover T
inst✝¹ : ∀ (i : E.I₀), HasPullback f (E.f i)
inst✝ : ∀ (i : E.I₀), HasPullback (E.f i) f
⊢ ({ s₀ := id, h₀ := fun i ↦ (pullbackSymmetry f (E.f i)).inv, w₀ := ⋯ } ≫
        { s₀ := id, h₀ := fun i ↦ (pullbackSymmetry f (E.f i)).hom, w₀ := ⋯ }).h₀ ≍
    (𝟙 (pullback₂ f E)).h₀

Tactic:
simp only [heq_eq_eq]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
S✝ T✝ : C
E✝ : PreZeroHypercover S✝
F : PreZeroHypercover S✝
S T : C
f : S ⟶ T
E : PreZeroHypercover T
inst✝¹ : ∀ (i : E.I₀), HasPullback f (E.f i)
inst✝ : ∀ (i : E.I₀), HasPullback (E.f i) f
⊢ ({ s₀ := id, h₀ := fun i ↦ (pullbackSymmetry f (E.f i)).inv, w₀ := ⋯ } ≫
        { s₀ := id, h₀ := fun i ↦ (pullbackSymmetry f (E.f i)).hom, w₀ := ⋯ }).h₀ =
    (𝟙 (pullback₂ f E)).h₀
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 : IsSheaf K.toGrothendieck P ∧ IsSheaf L.toGrothendieck P
⊢ IsSheaf (K ⊔ L).toGrothendieck P

Tactic:
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) ∧ IsSheaf L.toGrothendieck P
⊢ IsSheaf (K ⊔ L).toGrothendieck P
Module: Mathlib.CategoryTheory.Sites.Coverage

Goal state before:
pp: case inl
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 : Presieve X
hR : R ∈ K.coverings X
⊢ IsSheafFor P R

pp: case inr
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 : Presieve X
hR : R ∈ L.coverings X
⊢ IsSheafFor P R

Tactic:
· exact h.1 R hR

Goal state after:
case inr
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 : Presieve X
hR : R ∈ L.coverings X
⊢ IsSheafFor P R
Module: Mathlib.CategoryTheory.Functor.KanExtension.Preserves

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
D : Type u_4
inst✝⁶ : Category.{v_1, u_1} A
inst✝⁵ : Category.{v_2, u_2} B
inst✝⁴ : Category.{v_3, u_3} C
inst✝³ : Category.{v_4, u_4} D
G : B ⥤ D
F✝ : A ⥤ B
L : A ⥤ C
inst✝² : G.PreservesLeftKanExtensions L
inst✝¹ : ∀ (F : A ⥤ B), L.HasLeftKanExtension F
inst✝ : ∀ (F : A ⥤ D), L.HasLeftKanExtension F
F F' : A ⥤ B
η : F ⟶ F'
⊢ (L.lan ⋙ (whiskeringRight C B D).obj G).map η ≫ (G.leftKanExtensionCompIsoOfPreserves F' L).hom =
    (G.leftKanExtensionCompIsoOfPreserves F L).hom ≫ ((whiskeringRight A B D).obj G ⋙ L.lan).map η

Tactic:
by
      apply hom_ext_of_isLeftKanExtension (L.leftKanExtension F ⋙ G)
        (whiskerRight (L.leftKanExtensionUnit F) G ≫ (Functor.associator _ _ _).hom)
      dsimp [lan]
      ext
      simp [← G.map_comp_assoc]

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

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

Tactic:
exact ⟨Presieve.singleton (𝟙 X), mem_coverings_of_isIso (𝟙 X), by simp⟩

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

Goal state before:
pp: C : Type u_3
inst✝ : Category.{u_2, u_3} C
F : Cᵒᵖ ⥤ Type u_1
S X Y : C
g : Y ⟶ S
e : X ≅ Y
⊢ IsSheafFor F (ofArrows (fun x ↦ X) fun x ↦ e.hom ≫ g) ↔ IsSheafFor F (singleton g)

Tactic:
← Presieve.ofArrows_pUnit,

Goal state after:
C : Type u_3
inst✝ : Category.{u_2, u_3} C
F : Cᵒᵖ ⥤ Type u_1
S X Y : C
g : Y ⟶ S
e : X ≅ Y
⊢ IsSheafFor F (ofArrows (fun x ↦ X) fun x ↦ e.hom ≫ g) ↔ IsSheafFor F (ofArrows (fun x ↦ Y) fun x ↦ g)
Module: Mathlib.CategoryTheory.Sites.Canonical

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
inst✝ : P.IsRepresentable
⊢ Presheaf.IsSheaf (canonicalTopology C) (uliftYoneda.{w, v, u}.obj (P ⋙ uliftFunctor.{v, w}).reprX)

Tactic:
refine GrothendieckTopology.HasSheafCompose.isSheaf _ ?_

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
inst✝ : P.IsRepresentable
⊢ Presheaf.IsSheaf (canonicalTopology C) (yoneda.obj (P ⋙ uliftFunctor.{v, w}).reprX)
Module: Mathlib.CategoryTheory.Sites.Canonical

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J K : GrothendieckTopology C
h : J ≤ K
inst✝ : K.Subcanonical
x✝³ x✝² : C
x✝¹ : Sieve x✝²
x✝ : x✝¹ ∈ J x✝²
⊢ generate x✝¹.arrows ∈ J x✝²

Tactic:
simpa

Goal state after:
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
⊢ IsIso
    ((yoneda.map (((sheafToPresheaf J A).map ((G.sheafAdjunctionCocontinuous A J K).counit.app Y)).app (op U))).app
      (op X))

Tactic:
simpa [sheafAdjunctionCocontinuous_counit_app_hom]
    using! isIso_ranCounit_app_of_isDenseSubsite G J K Y U X

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

Goal state before:
pp: case mpr
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
inst✝³ : G.IsCoverDense J
inst✝² : G.Full
inst✝¹ : G.IsContinuous K J
inst✝ : (G.sheafPushforwardContinuous A K J).EssSurj
P✝ Q : Cᵒᵖ ⥤ A
f : P✝ ⟶ Q
P : Dᵒᵖ ⥤ A
⊢ ObjectProperty.isoClosure (fun x ↦ x ∈ Set.range (sheafToPresheaf J A ⋙ (whiskeringLeft Dᵒᵖ Cᵒᵖ A).obj G.op).obj) P →
    ObjectProperty.isoClosure (fun x ↦ x ∈ Set.range (sheafToPresheaf K A).obj) P

Tactic:
rintro ⟨_, ⟨R, rfl⟩, ⟨e⟩⟩
      exact ⟨G.op ⋙ R.obj, ⟨(G.sheafPushforwardContinuous A K J).obj R, rfl⟩, ⟨e⟩⟩

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
I : Type u_1
Y : I → C
x : FamilyOfElementsOnObjects F Y
hx : x.IsCompatible
hY : J.CoversTop Y
hF : IsSheaf J F
H : Presieve.IsSheaf J F
s : (X : C) → F.obj (Opposite.op X) := fun X ↦ ⋯.amalgamate (x.familyOfElements X) ⋯
hs : ∀ {X : C} (i : I) (f : X ⟶ Y i), s X = (ConcreteCategory.hom (F.map f.op)) (x i)
⊢ ∀ {W X : C} (a : W ⟶ X) (i : I) (x : W ⟶ Y i), (ConcreteCategory.hom (F.map a.op)) (s X) = s W

Tactic:
intro W X a i b

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
I : Type u_1
Y : I → C
x : FamilyOfElementsOnObjects F Y
hx : x.IsCompatible
hY : J.CoversTop Y
hF : IsSheaf J F
H : Presieve.IsSheaf J F
s : (X : C) → F.obj (Opposite.op X) := fun X ↦ ⋯.amalgamate (x.familyOfElements X) ⋯
hs : ∀ {X : C} (i : I) (f : X ⟶ Y i), s X = (ConcreteCategory.hom (F.map f.op)) (x i)
W X : C
a : W ⟶ X
i : I
b : W ⟶ Y i
⊢ (ConcreteCategory.hom (F.map a.op)) (s X) = s W
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J✝ J : GrothendieckTopology C
X : C
Y : Over X
E : (J.over X).OneHypercover Y
i₁ i₂ : E.I₀
W : C
p₁ : W ⟶ (Over.forget X).obj (E.X i₁)
p₂ : W ⟶ (Over.forget X).obj (E.X i₂)
w : p₁ ≫ (Over.forget X).map (E.f i₁) = p₂ ≫ (Over.forget X).map (E.f i₂)
this : p₁ ≫ (E.X i₁).hom = p₂ ≫ (E.X i₂).hom
⊢ Over.Hom.left (Over.homMk p₁ ⋯ ≫ E.f i₁) = Over.Hom.left (Over.homMk p₂ ⋯ ≫ E.f i₂)

Tactic:
simpa

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

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
J✝ J : GrothendieckTopology C
X : C
Y : Over X
E : (J.over X).OneHypercover Y
i₁ i₂ : E.I₀
W : C
p₁ : W ⟶ (Over.forget X).obj (E.X i₁)
p₂ : W ⟶ (Over.forget X).obj (E.X i₂)
w : p₁ ≫ (Over.forget X).map (E.f i₁) = p₂ ≫ (Over.forget X).map (E.f i₂)
this✝ : p₁ ≫ (E.X i₁).hom = p₂ ≫ (E.X i₂).hom
this : E.sieve₁ (Over.homMk p₁ ⋯) (Over.homMk p₂ ⋯) ∈ (J.over X) (Over.mk (p₁ ≫ (E.X i₁).hom))
⊢ (E.map (Over.forget X)).sieve₁ p₁ p₂ ∈ J W

Tactic:
GrothendieckTopology.mem_over_iff,

Goal state after:
case refine_2
C : Type u
inst✝ : Category.{v, u} C
J✝ J : GrothendieckTopology C
X : C
Y : Over X
E : (J.over X).OneHypercover Y
i₁ i₂ : E.I₀
W : C
p₁ : W ⟶ (Over.forget X).obj (E.X i₁)
p₂ : W ⟶ (Over.forget X).obj (E.X i₂)
w : p₁ ≫ (Over.forget X).map (E.f i₁) = p₂ ≫ (Over.forget X).map (E.f i₂)
this✝ : p₁ ≫ (E.X i₁).hom = p₂ ≫ (E.X i₂).hom
this :
  (Sieve.overEquiv (Over.mk (p₁ ≫ (E.X i₁).hom))) (E.sieve₁ (Over.homMk p₁ ⋯) (Over.homMk p₂ ⋯)) ∈
    J (Over.mk (p₁ ≫ (E.X i₁).hom)).left
⊢ (E.map (Over.forget X)).sieve₁ p₁ p₂ ∈ J W
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: case refine_1
C : Type u
inst✝² : Category.{v, u} C
J✝ : GrothendieckTopology C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
J : GrothendieckTopology C
K : GrothendieckTopology D
F : C ⥤ D
X : C
inst✝ : F.PreservesOneHypercovers J K
Y : Over X
E : (J.over X).OneHypercover Y
E' : K.OneHypercover (F.obj ((Over.forget X).obj Y)) := (E.map (Over.forget X) J).map F K
⊢ Sieve.functorPushforward (Over.post F) E.sieve₀ ∈ (K.over (F.obj X)) ((Over.post F).obj Y)

Tactic:
GrothendieckTopology.mem_over_iff,

Goal state after:
case refine_1
C : Type u
inst✝² : Category.{v, u} C
J✝ : GrothendieckTopology C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
J : GrothendieckTopology C
K : GrothendieckTopology D
F : C ⥤ D
X : C
inst✝ : F.PreservesOneHypercovers J K
Y : Over X
E : (J.over X).OneHypercover Y
E' : K.OneHypercover (F.obj ((Over.forget X).obj Y)) := (E.map (Over.forget X) J).map F K
⊢ (Sieve.overEquiv ((Over.post F).obj Y)) (Sieve.functorPushforward (Over.post F) E.sieve₀) ∈
    K ((Over.post F).obj Y).left
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: case refine_2
C : Type u
inst✝² : Category.{v, u} C
J✝ : GrothendieckTopology C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
J : GrothendieckTopology C
K : GrothendieckTopology D
F : C ⥤ D
X : C
inst✝ : F.PreservesOneHypercovers J K
Y : Over X
E : (J.over X).OneHypercover Y
E' : K.OneHypercover (F.obj ((Over.forget X).obj Y)) := (E.map (Over.forget X) J).map F K
i₁ i₂ : E.I₀
W : Over (F.obj X)
p₁ : W ⟶ (Over.post F).obj (E.X i₁)
p₂ : W ⟶ (Over.post F).obj (E.X i₂)
w : p₁ ≫ (Over.post F).map (E.f i₁) = p₂ ≫ (Over.post F).map (E.f i₂)
⊢ (E.map (Over.post F)).sieve₁ p₁ p₂ ∈ (K.over (F.obj X)) W

Tactic:
GrothendieckTopology.mem_over_iff,

Goal state after:
case refine_2
C : Type u
inst✝² : Category.{v, u} C
J✝ : GrothendieckTopology C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
J : GrothendieckTopology C
K : GrothendieckTopology D
F : C ⥤ D
X : C
inst✝ : F.PreservesOneHypercovers J K
Y : Over X
E : (J.over X).OneHypercover Y
E' : K.OneHypercover (F.obj ((Over.forget X).obj Y)) := (E.map (Over.forget X) J).map F K
i₁ i₂ : E.I₀
W : Over (F.obj X)
p₁ : W ⟶ (Over.post F).obj (E.X i₁)
p₂ : W ⟶ (Over.post F).obj (E.X i₂)
w : p₁ ≫ (Over.post F).map (E.f i₁) = p₂ ≫ (Over.post F).map (E.f i₂)
⊢ (Sieve.overEquiv W) ((E.map (Over.post F)).sieve₁ p₁ p₂) ∈ K W.left
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: case refine_1.of
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
Z : C
S : Presieve Z
hS : S ∈ K.toCoverage.coverings Z
s : Z ⟶ X
⊢ (Sieve.overEquiv { left := Z, right := right, hom := s }).symm (Sieve.generate S) ∈
    (Precoverage.comap (Over.forget X) K).toGrothendieck { left := Z, right := right, hom := s }

Tactic:
Sieve.overEquiv_symm_generate

Goal state after:
case refine_1.of
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
Z : C
S : Presieve Z
hS : S ∈ K.toCoverage.coverings Z
s : Z ⟶ X
⊢ Sieve.generate (Presieve.functorPullback (Over.forget X) S) ∈
    (Precoverage.comap (Over.forget X) K).toGrothendieck { left := Z, right := right, hom := s }
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: 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
Z : C
S : Presieve Z
hS : S ∈ K.toCoverage.coverings Z
s : Z ⟶ X
⊢ Presieve.functorPullback (Over.forget X) S ∈
    (Precoverage.comap (Over.forget X) K).coverings { left := Z, right := right, hom := s }

Tactic:
simpa

Goal state after: