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

Goal state before:
pp: case mp
C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : ObjectProperty C
X Y : C
f : X ⟶ Y
hX : P X
hY : P Y
⊢ P.isLocal f → IsIso f

Tactic:
intro hf

Goal state after:
case mp
C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : ObjectProperty C
X Y : C
f : X ⟶ Y
hX : P X
hY : P Y
hf : P.isLocal f
⊢ IsIso f
Module: Mathlib.CategoryTheory.Localization.Bousfield

Goal state before:
pp: case mp
C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : ObjectProperty C
X Y : C
f : X ⟶ Y
hX : P X
hY : P Y
⊢ P.isColocal f → IsIso f

Tactic:
intro hf

Goal state after:
case mp
C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : ObjectProperty C
X Y : C
f : X ⟶ Y
hX : P X
hY : P Y
hf : P.isColocal f
⊢ IsIso f
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
F : C ⥤ D
G : D ⥤ C
adj : G ⊣ F
inst✝¹ : F.Full
inst✝ : F.Faithful
X : D
⊢ isLocal (fun x ↦ x ∈ Set.range F.obj) (adj.unit.app X)

Tactic:
rintro _ ⟨Y, rfl⟩

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
F : C ⥤ D
G : D ⥤ C
adj : G ⊣ F
inst✝¹ : F.Full
inst✝ : F.Faithful
X : D
Y : C
⊢ Function.Bijective fun g ↦ adj.unit.app X ≫ g
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
F : C ⥤ D
G : D ⥤ C
adj : G ⊣ F
inst✝¹ : G.Full
inst✝ : G.Faithful
X : C
⊢ isColocal (fun x ↦ x ∈ Set.range G.obj) (adj.counit.app X)

Tactic:
rintro _ ⟨Y, rfl⟩

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
F : C ⥤ D
G : D ⥤ C
adj : G ⊣ F
inst✝¹ : G.Full
inst✝ : G.Faithful
X : C
Y : D
⊢ Function.Bijective fun f ↦ f ≫ adj.counit.app X
Module: Mathlib.CategoryTheory.Limits.VanKampen

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
c : BinaryCofan X Y
cofans : (X Y : C) → BinaryCofan X Y
colimits : (X Y : C) → IsColimit (cofans X Y)
cones : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → PullbackCone f g
limits : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → IsLimit (cones f g)
h₁ :
  ∀ {X' Y' : C} (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : (cofans X' Y').pt ⟶ c.pt),
    αX ≫ c.inl = (cofans X' Y').inl ≫ f →
      αY ≫ c.inr = (cofans X' Y').inr ≫ f →
        IsPullback (cofans X' Y').inl αX f c.inl ∧ IsPullback (cofans X' Y').inr αY f c.inr
h₂ : {Z : C} → (f : Z ⟶ c.pt) → IsColimit (BinaryCofan.mk (cones f c.inl).fst (cones f c.inr).fst)
X' Y' : C
c' : BinaryCofan X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hX : αX ≫ c.inl = c'.inl ≫ f
hY : αY ≫ c.inr = c'.inr ≫ f
H₁ : IsPullback c'.inl αX f c.inl
H₂ : IsPullback c'.inr αY f c.inr
e₁ : X' ≅ (cones f c.inl).pt := H₁.isLimit.conePointUniqueUpToIso (limits f c.inl)
e₂ : Y' ≅ (cones f c.inr).pt := H₂.isLimit.conePointUniqueUpToIso (limits f c.inr)
he₁ : c'.inl = e₁.hom ≫ (cones f c.inl).fst
⊢ c'.inr = e₂.hom ≫ (cones f c.inr).fst

Tactic:
simp [e₂]

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
J : GrothendieckTopology C
A : Type u_2
inst✝ : Category.{v_2, u_2} A
G : (Cᵒᵖ ⥤ A) ⥤ Sheaf J A
adj : G ⊣ sheafToPresheaf J A
⊢ J.W = (MorphismProperty.isomorphisms (Sheaf J A)).inverseImage G

Tactic:
by
  rw [W_eq_isLocal_range_sheafToPresheaf_obj,
    ObjectProperty.isLocal_eq_inverseImage_isomorphisms adj]

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

Goal state before:
pp: case a
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₀'
Z : C
g : Z ⟶ Opposite.unop (Opposite.op Y)
hg : (Presheaf.equalizerSieve r₀ r₀' ⊓ Presheaf.equalizerSieve m₀ m₀').arrows g
⊢ (ConcreteCategory.hom (A.map g.op)) ((ConcreteCategory.hom (φ.app (Opposite.op Y))) (r₀ • m₀)) =
    (ConcreteCategory.hom (A.map g.op)) ((ConcreteCategory.hom (φ.app (Opposite.op Y))) (r₀' • m₀'))

Tactic:
rw [← NatTrans.naturality_apply (D := Ab), ← NatTrans.naturality_apply (D := Ab)]

Goal state after:
case a
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₀'
Z : C
g : Z ⟶ Opposite.unop (Opposite.op Y)
hg : (Presheaf.equalizerSieve r₀ r₀' ⊓ Presheaf.equalizerSieve m₀ m₀').arrows g
⊢ (ConcreteCategory.hom (φ.app (Opposite.op Z))) ((ConcreteCategory.hom (M₀.presheaf.map g.op)) (r₀ • m₀)) =
    (ConcreteCategory.hom (φ.app (Opposite.op Z))) ((ConcreteCategory.hom (M₀.presheaf.map g.op)) (r₀' • m₀'))
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafification

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 α
inst✝¹ : J.WEqualsLocallyBijective AddCommGrpCat
inst✝ : HasWeakSheafify J AddCommGrpCat
P : PresheafOfModules R₀
F : SheafOfModules R
f : (sheafification α).obj P ⟶ F
⊢ ((sheafificationAdjunction J AddCommGrpCat).homEquiv P.presheaf ((SheafOfModules.toSheaf R).obj F))
      ((SheafOfModules.toSheaf R).map ((sheafificationHomEquiv α).symm ((sheafificationHomEquiv α) f))) =
    ((sheafificationAdjunction J AddCommGrpCat).homEquiv P.presheaf ((SheafOfModules.toSheaf R).obj F))
      (((sheafificationAdjunction J AddCommGrpCat).homEquiv P.presheaf ((SheafOfModules.toSheaf R).obj F)).symm
        ((toPresheaf R₀).map ((sheafificationHomEquiv α) f)))

Tactic:
Equiv.apply_symm_apply,

Goal state after:
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 α
inst✝¹ : J.WEqualsLocallyBijective AddCommGrpCat
inst✝ : HasWeakSheafify J AddCommGrpCat
P : PresheafOfModules R₀
F : SheafOfModules R
f : (sheafification α).obj P ⟶ F
⊢ ((sheafificationAdjunction J AddCommGrpCat).homEquiv P.presheaf ((SheafOfModules.toSheaf R).obj F))
      ((SheafOfModules.toSheaf R).map ((sheafificationHomEquiv α).symm ((sheafificationHomEquiv α) f))) =
    (toPresheaf R₀).map ((sheafificationHomEquiv α) f)
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)
this : ∀ ⦃d : ℕ⦄ ⦃Y : C⦄ (e : Ext X Y d) (k : ℕ), d = n + k → e = 0
i : ℕ
hi : n ≤ i
Y : C
e : Ext X Y i
⊢ e = 0

Tactic:
obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le hi

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)
this : ∀ ⦃d : ℕ⦄ ⦃Y : C⦄ (e : Ext X Y d) (k : ℕ), d = n + k → e = 0
Y : C
k : ℕ
hi : n ≤ n + k
e : Ext X Y (n + k)
⊢ e = 0
Module: Mathlib.CategoryTheory.Limits.Bicones

Goal state before:
pp: case left_id
J : Type u₁
inst✝ : Category.{v₁, u₁} J
Z✝ : Bicone J
g : BiconeHom J Bicone.left Z✝
⊢ BiconeHom J Bicone.left Z✝

pp: case right_id
J : Type u₁
inst✝ : Category.{v₁, u₁} J
Z✝ : Bicone J
g : BiconeHom J Bicone.right Z✝
⊢ BiconeHom J Bicone.right Z✝

pp: case left
J : Type u₁
inst✝ : Category.{v₁, u₁} J
Z✝ : Bicone J
j✝ : J
g : BiconeHom J (Bicone.diagram j✝) Z✝
⊢ BiconeHom J Bicone.left Z✝

pp: case right
J : Type u₁
inst✝ : Category.{v₁, u₁} J
Z✝ : Bicone J
j✝ : J
g : BiconeHom J (Bicone.diagram j✝) Z✝
⊢ BiconeHom J Bicone.right Z✝

pp: case diagram
J : Type u₁
inst✝ : Category.{v₁, u₁} J
Z✝ : Bicone J
j✝ k✝ : J
f : j✝ ⟶ k✝
g : BiconeHom J (Bicone.diagram k✝) Z✝
⊢ BiconeHom J (Bicone.diagram j✝) Z✝

Tactic:
· exact g

Goal state after:
case right_id
J : Type u₁
inst✝ : Category.{v₁, u₁} J
Z✝ : Bicone J
g : BiconeHom J Bicone.right Z✝
⊢ BiconeHom J Bicone.right Z✝

case left
J : Type u₁
inst✝ : Category.{v₁, u₁} J
Z✝ : Bicone J
j✝ : J
g : BiconeHom J (Bicone.diagram j✝) Z✝
⊢ BiconeHom J Bicone.left Z✝

case right
J : Type u₁
inst✝ : Category.{v₁, u₁} J
Z✝ : Bicone J
j✝ : J
g : BiconeHom J (Bicone.diagram j✝) Z✝
⊢ BiconeHom J Bicone.right Z✝

case diagram
J : Type u₁
inst✝ : Category.{v₁, u₁} J
Z✝ : Bicone J
j✝ k✝ : J
f : j✝ ⟶ k✝
g : BiconeHom J (Bicone.diagram k✝) Z✝
⊢ BiconeHom J (Bicone.diagram j✝) Z✝
Module: Mathlib.CategoryTheory.Limits.Bicones

Goal state before:
pp: case right_id
J : Type u₁
inst✝ : Category.{v₁, u₁} J
Z✝ : Bicone J
g : BiconeHom J Bicone.right Z✝
⊢ BiconeHom J Bicone.right Z✝

pp: case left
J : Type u₁
inst✝ : Category.{v₁, u₁} J
Z✝ : Bicone J
j✝ : J
g : BiconeHom J (Bicone.diagram j✝) Z✝
⊢ BiconeHom J Bicone.left Z✝

pp: case right
J : Type u₁
inst✝ : Category.{v₁, u₁} J
Z✝ : Bicone J
j✝ : J
g : BiconeHom J (Bicone.diagram j✝) Z✝
⊢ BiconeHom J Bicone.right Z✝

pp: case diagram
J : Type u₁
inst✝ : Category.{v₁, u₁} J
Z✝ : Bicone J
j✝ k✝ : J
f : j✝ ⟶ k✝
g : BiconeHom J (Bicone.diagram k✝) Z✝
⊢ BiconeHom J (Bicone.diagram j✝) Z✝

Tactic:
· exact g

Goal state after:
case left
J : Type u₁
inst✝ : Category.{v₁, u₁} J
Z✝ : Bicone J
j✝ : J
g : BiconeHom J (Bicone.diagram j✝) Z✝
⊢ BiconeHom J Bicone.left Z✝

case right
J : Type u₁
inst✝ : Category.{v₁, u₁} J
Z✝ : Bicone J
j✝ : J
g : BiconeHom J (Bicone.diagram j✝) Z✝
⊢ BiconeHom J Bicone.right Z✝

case diagram
J : Type u₁
inst✝ : Category.{v₁, u₁} J
Z✝ : Bicone J
j✝ k✝ : J
f : j✝ ⟶ k✝
g : BiconeHom J (Bicone.diagram k✝) Z✝
⊢ BiconeHom J (Bicone.diagram j✝) Z✝
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
⊢ Presieve.IsSeparatedFor (Functor.closedSieves J₁).toFunctor S.arrows

Tactic:
rintro x ⟨M, hM⟩ ⟨N, hN⟩ hM₂ hN₂

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 : (Functor.sieves C).obj (Opposite.op X)
hM : M ∈ (Functor.closedSieves J₁).obj (Opposite.op X)
N : (Functor.sieves C).obj (Opposite.op X)
hN : N ∈ (Functor.closedSieves J₁).obj (Opposite.op X)
hM₂ : x.IsAmalgamation ⟨M, hM⟩
hN₂ : x.IsAmalgamation ⟨N, hN⟩
⊢ ⟨M, hM⟩ = ⟨N, hN⟩
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
⊢ J₁.Covers M f → J₁.Covers N f

Tactic:
intro hf

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
⊢ J₁.Covers N f
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
⊢ J₁.Covers N f → J₁.Covers M f

Tactic:
intro hf

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
⊢ J₁.Covers M f
Module: Mathlib.CategoryTheory.Sites.Closed

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
c : (X : C) → ClosureOperator (Sieve X)
hc : ∀ ⦃X Y : C⦄ (f : Y ⟶ X) (S : Sieve X), (c Y) (Sieve.pullback f S) = Sieve.pullback f ((c X) S)
X Y : C
S : Sieve X
f : Y ⟶ X
hS : S ∈ {S | (c X) S = ⊤}
⊢ Sieve.pullback f S ∈ {S | (c Y) S = ⊤}

Tactic:
rw [Set.mem_ofPred_eq] at hS

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
c : (X : C) → ClosureOperator (Sieve X)
hc : ∀ ⦃X Y : C⦄ (f : Y ⟶ X) (S : Sieve X), (c Y) (Sieve.pullback f S) = Sieve.pullback f ((c X) S)
X Y : C
S : Sieve X
f : Y ⟶ X
hS : (c X) S = ⊤
⊢ Sieve.pullback f S ∈ {S | (c Y) S = ⊤}
Module: Mathlib.CategoryTheory.Sites.Closed

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
c : (X : C) → ClosureOperator (Sieve X)
hc : ∀ ⦃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
hS : S ∈ {S | (c X) S = ⊤}
R : Sieve X
hR : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Sieve.pullback f R ∈ {S | (c Y) S = ⊤}
⊢ R ∈ {S | (c X) S = ⊤}

Tactic:
rw [Set.mem_ofPred_eq] at hS

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
c : (X : C) → ClosureOperator (Sieve X)
hc : ∀ ⦃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
hS : (c X) S = ⊤
R : Sieve X
hR : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Sieve.pullback f R ∈ {S | (c Y) S = ⊤}
⊢ R ∈ {S | (c X) S = ⊤}
Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero

Goal state before:
pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
J : Precoverage C
inst✝ : J.RespectsIso
S : C
E F : PreZeroHypercover S
e : E ≅ F
hE : E.presieve₀ ∈ J.coverings S
Z : C
g✝ : Z ⟶ S
i : F.I₀
⊢ ∃ Y e, E.presieve₀ (e.hom ≫ F.f i)

Tactic:
use E.X (e.inv.s₀ i), (asIso (e.inv.h₀ i)).symm

Goal state after:
case h
C : Type u
inst✝¹ : Category.{v, u} C
J : Precoverage C
inst✝ : J.RespectsIso
S : C
E F : PreZeroHypercover S
e : E ≅ F
hE : E.presieve₀ ∈ J.coverings S
Z : C
g✝ : Z ⟶ S
i : F.I₀
⊢ E.presieve₀ ((asIso (e.inv.h₀ i)).symm.hom ≫ F.f i)
Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : Precoverage C
S T : C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F✝ : C ⥤ D
K : Precoverage D
F : C ⥤ D
E : J.ZeroHypercover S
h : J ≤ comap F K
⊢ Presieve.map F E.presieve₀ ∈ K.coverings (F.obj S)

Tactic:
← mem_comap_iff

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
J : Precoverage C
S T : C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F✝ : C ⥤ D
K : Precoverage D
F : C ⥤ D
E : J.ZeroHypercover S
h : J ≤ comap F K
⊢ E.presieve₀ ∈ (comap F K).coverings S
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

pp: case refine_2
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✝ : ∃ R ∈ J.coverings X, R ≤ S.arrows
R : Presieve X
hR : R ∈ J.coverings X
hle : R ≤ S.arrows
⊢ S ∈ J.toGrothendieck X

Tactic:
· induction hS with
    | of X R hR =>
      use R, hR
      exact Sieve.le_generate R
    | top X =>
      exact ⟨Presieve.singleton (𝟙 X), mem_coverings_of_isIso (𝟙 X), by simp⟩
    | pullback X S hS Y f h =>
      obtain ⟨R, hR, hle⟩ := h
      have : R.HasPullbacks f := J.hasPullbacks_of_mem f hR
      refine ⟨R.pullbackArrows f, pullbackArrows_mem f hR, ?_⟩
      rw [← Sieve.generate_le_iff, Sieve.pullbackArrows_comm]
      apply Sieve.pullback_monotone
      rwa [Sieve.generate_le_iff]
    | transitive X S T hS hT hleS hleT =>
      obtain ⟨R, hR, hle⟩ := hleS
      rw [mem_iff_exists_zeroHypercover] at hR
      obtain ⟨E, rfl⟩ := hR
      replace hleT (i : E.I₀) : ∃ (F : J.ZeroHypercover (E.X i)),
          F.presieve₀ ≤ (Sieve.pullback (E.f i) T).arrows := by
        obtain ⟨R', hR', hle'⟩ := hleT (hle _ _ ⟨i⟩)
        rw [mem_iff_exists_zeroHypercover] at hR'
        obtain ⟨F, rfl⟩ := hR'
        use F
      choose F hle' using hleT
      refine ⟨(E.bind F).presieve₀, (E.bind F).mem₀, ?_⟩
      rw [Presieve.ofArrows_le_iff]
      intro i
      exact hle' _ _ _ ⟨i.snd⟩

Goal state after:
case refine_2
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✝ : ∃ R ∈ J.coverings X, R ≤ S.arrows
R : Presieve X
hR : R ∈ J.coverings X
hle : R ≤ S.arrows
⊢ S ∈ J.toGrothendieck X
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

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

Tactic:
intro (k : E.I₁')
    simp only [multicospanIndex_right, multicospanShape_fst, multicospanIndex_left,
      multicospanIndex_fst, assoc, multicospanShape_snd, multicospanIndex_snd]
    have heq := d.condition (f.s₁' k)
    simp only [Hom.s₁', multicospanIndex_right, multicospanShape_fst, multicospanIndex_left,
      multicospanIndex_fst, multicospanShape_snd, multicospanIndex_snd] at heq
    rw [← Functor.map_comp, ← op_comp, ← Hom.w₁₁, ← Functor.map_comp, ← op_comp, ← Hom.w₁₂]
    rw [op_comp, Functor.map_comp, reassoc_of% heq, op_comp, Functor.map_comp]

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
F : PreOneHypercover S
toHomf : E.Hom F.toPreZeroHypercover
fs₁ : {i j : E.I₀} → E.I₁ i j → F.I₁ (toHomf.s₀ i) (toHomf.s₀ j)
fh₁ : {i j : E.I₀} → (k : E.I₁ i j) → E.Y k ⟶ F.Y (fs₁ k)
w₁₁✝¹ : ∀ {i j : E.I₀} (k : E.I₁ i j), fh₁ k ≫ F.p₁ (fs₁ k) = E.p₁ k ≫ toHomf.h₀ i
w₁₂✝¹ : ∀ {i j : E.I₀} (k : E.I₁ i j), fh₁ k ≫ F.p₂ (fs₁ k) = E.p₂ k ≫ toHomf.h₀ j
gs₁ : {i j : E.I₀} → E.I₁ i j → F.I₁ (toHomf.s₀ i) (toHomf.s₀ j)
gh₁ : {i j : E.I₀} → (k : E.I₁ i j) → E.Y k ⟶ F.Y (gs₁ k)
w₁₁✝ : ∀ {i j : E.I₀} (k : E.I₁ i j), gh₁ k ≫ F.p₁ (gs₁ k) = E.p₁ k ≫ toHomf.h₀ i
w₁₂✝ : ∀ {i j : E.I₀} (k : E.I₁ i j), gh₁ k ≫ F.p₂ (gs₁ k) = E.p₂ k ≫ toHomf.h₀ j
hs₀ :
  { toHom := toHomf, s₁ := fs₁, h₁ := fh₁, w₁₁ := w₁₁✝¹, w₁₂ := w₁₂✝¹ }.s₀ =
    { toHom := toHomf, s₁ := gs₁, h₁ := gh₁, w₁₁ := w₁₁✝, w₁₂ := w₁₂✝ }.s₀
hh₀ :
  ∀ (i : E.I₀),
    { toHom := toHomf, s₁ := fs₁, h₁ := fh₁, w₁₁ := w₁₁✝¹, w₁₂ := w₁₂✝¹ }.h₀ i =
      { toHom := toHomf, s₁ := gs₁, h₁ := gh₁, w₁₁ := w₁₁✝, w₁₂ := w₁₂✝ }.h₀ i ≫ eqToHom ⋯
hs₁ :
  ∀ (i j : E.I₀) (k : E.I₁ i j),
    { toHom := toHomf, s₁ := fs₁, h₁ := fh₁, w₁₁ := w₁₁✝¹, w₁₂ := w₁₂✝¹ }.s₁ k =
      (congrIndexOneOfEq ⋯ ⋯) ({ toHom := toHomf, s₁ := gs₁, h₁ := gh₁, w₁₁ := w₁₁✝, w₁₂ := w₁₂✝ }.s₁ k)
hh₁ :
  ∀ (i j : E.I₀) (k : E.I₁ i j),
    { toHom := toHomf, s₁ := fs₁, h₁ := fh₁, w₁₁ := w₁₁✝¹, w₁₂ := w₁₂✝¹ }.h₁ k =
      { toHom := toHomf, s₁ := gs₁, h₁ := gh₁, w₁₁ := w₁₁✝, w₁₂ := w₁₂✝ }.h₁ k ≫
        (congrIndexOneOfEqIso ⋯ ⋯ ({ toHom := toHomf, s₁ := gs₁, h₁ := gh₁, w₁₁ := w₁₁✝, w₁₂ := w₁₂✝ }.s₁ k)).inv ≫
          eqToHom ⋯
i j : E.I₀
k : E.I₁ i j
⊢ fs₁ k = gs₁ k

Tactic:
simpa using hs₁ i j k

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

Goal state before:
pp: case mpr
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
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝³ : Category.{u, v} A
inst✝² : G.LocallyCoverDense K
inst✝¹ : G.IsLocallyFull K
inst✝ : G.IsLocallyFaithful K
X : C
Y : Over X
T : ↑(J ((Over.forget X).obj Y))
Z : C
f : Z ⟶ (Over.forget X).obj Y
⊢ (↑T).arrows f → (Sieve.functorPushforward (Over.forget X) (Sieve.functorPullback (Over.forget X) ↑T)).arrows f

Tactic:
intro hf

Goal state after:
case mpr
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
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝³ : Category.{u, v} A
inst✝² : G.LocallyCoverDense K
inst✝¹ : G.IsLocallyFull K
inst✝ : G.IsLocallyFaithful K
X : C
Y : Over X
T : ↑(J ((Over.forget X).obj Y))
Z : C
f : Z ⟶ (Over.forget X).obj Y
hf : (↑T).arrows f
⊢ (Sieve.functorPushforward (Over.forget X) (Sieve.functorPullback (Over.forget X) ↑T)).arrows f
Module: Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
F : Cᵒᵖ ⥤ D
inst✝ : CreatesFiniteCoproducts F
x✝¹ : Type
x✝ : Fintype x✝¹
⊢ CreatesLimitsOfShape (Discrete x✝¹) F.rightOp

Tactic:
by
    apply +allowSynthFailures createsLimitsOfShapeRightOp
    exact createsColimitsOfShapeOfEquiv (Discrete.opposite _).symm _

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
I : Type u_1
Y : I → C
hY : J.CoversTop Y
F : Sheaf J (Type u_2)
x y : ↑F.obj.sections
h : ∀ (i : I), ↑x (Opposite.op (Y i)) = ↑y (Opposite.op (Y i))
W : Cᵒᵖ
⊢ ↑x W = ↑y W

Tactic:
apply (((isSheaf_iff_isSheaf_of_type _ _).1 F.2).isSeparated _ (hY W.unop)).ext

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
I : Type u_1
Y : I → C
hY : J.CoversTop Y
F : Sheaf J (Type u_2)
x y : ↑F.obj.sections
h : ∀ (i : I), ↑x (Opposite.op (Y i)) = ↑y (Opposite.op (Y i))
W : Cᵒᵖ
⊢ ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Opposite.unop W⦄,
    (Sieve.ofObjects Y (Opposite.unop W)).arrows f →
      (ConcreteCategory.hom (F.obj.map f.op)) (↑x W) = (ConcreteCategory.hom (F.obj.map f.op)) (↑y W)
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
⊢ (↑S).arrows f → S.preOneHypercover.sieve₀.arrows f

Tactic:
intro hf

Goal state after:
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