mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Adjunction

Goal state before:
pp: R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
this : Algebra R S := f.toAlgebra
M : ModuleCat R
m : ↑M
⊢ (ConcreteCategory.hom (λ_ ((extendScalars f).obj M)).inv) (1 ⊗ₜ[R] m) =
    (Hom.hom (↟↑(AlgebraTensorModule.rid R S S) ▷ (extendScalars f).obj M))
      ((Hom.hom (↟↑(AlgebraTensorModule.distribBaseChange R S ↑(𝟙_ (ModuleCat R)) ↑M))) (1 ⊗ₜ[R] (1 ⊗ₜ[R] m)))

Tactic:
MonoidalCategory.leftUnitor_inv_apply

Goal state after:
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
this : Algebra R S := f.toAlgebra
M : ModuleCat R
m : ↑M
⊢ 1 ⊗ₜ[S] (1 ⊗ₜ[R] m) =
    (Hom.hom (↟↑(AlgebraTensorModule.rid R S S) ▷ (extendScalars f).obj M))
      ((Hom.hom (↟↑(AlgebraTensorModule.distribBaseChange R S ↑(𝟙_ (ModuleCat R)) ↑M))) (1 ⊗ₜ[R] (1 ⊗ₜ[R] m)))
Module: Mathlib.CategoryTheory.Monoidal.FunctorCategory

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F G H K : C ⥤ D
X : C
⊢ (α_ (F.obj X) (G.obj X) (H.obj X)).hom ▷ K.obj X ≫
      (α_ (F.obj X) (G.obj X ⊗ H.obj X) (K.obj X)).hom ≫ F.obj X ◁ (α_ (G.obj X) (H.obj X) (K.obj X)).hom =
    (α_ (F.obj X ⊗ G.obj X) (H.obj X) (K.obj X)).hom ≫ (α_ (F.obj X) (G.obj X) (H.obj X ⊗ K.obj X)).hom

Tactic:
pentagon

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F G H K : C ⥤ D
X : C
⊢ (α_ (F.obj X ⊗ G.obj X) (H.obj X) (K.obj X)).hom ≫ (α_ (F.obj X) (G.obj X) (H.obj X ⊗ K.obj X)).hom =
    (α_ (F.obj X ⊗ G.obj X) (H.obj X) (K.obj X)).hom ≫ (α_ (F.obj X) (G.obj X) (H.obj X ⊗ K.obj X)).hom
Module: Mathlib.CategoryTheory.Limits.IsConnected

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
x : C
h : Limits.IsTerminal x
⊢ IsConnected C

Tactic:
by
  let : Nonempty C := ⟨x⟩
  apply isConnected_of_zigzag
  intro j₁ j₂
  use [x, j₂]
  simp only [List.isChain_cons_cons, List.isChain_singleton, and_true, ne_eq,
    reduceCtorEq, not_false_eq_true, List.getLast_cons, List.cons_ne_self, List.getLast_singleton]
  exact ⟨Zag.of_hom <| h.from _, Zag.symm <| Zag.of_hom <| h.from _⟩

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
F : Cᵒᵖ ⥤ Type u
G✝ : PresheafOfModules R
F₁ F₂ : Cᵒᵖ ⥤ Type u
G : PresheafOfModules R
f : F₁ ⟶ F₂
g : F₂ ⟶ (toPresheaf R ⋙ (Functor.whiskeringRight Cᵒᵖ Ab (Type u)).obj (forget Ab)).obj G
⊢ freeAdjunctionUnit R F₁ ≫ Functor.whiskerRight ((toPresheaf R).map (freeHomEquiv.symm (f ≫ g))) (forget Ab) =
    freeAdjunctionUnit R F₁ ≫
      Functor.whiskerRight ((toPresheaf R).map ((free R).map f ≫ freeHomEquiv.symm g)) (forget Ab)

Tactic:
ext; simp [freeHomEquiv, toPresheaf]

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : LocallySmall.{w, v, u} C
inst✝¹ : IsCofiltered C
inst✝ : InitiallySmall C
R : Cᵒᵖ ⥤ RingCat
cR : Cocone R
hcR : IsColimit cR
M : PresheafOfModules R
cM : Cocone M.presheaf
hcM : IsColimit cM
r : ↑cR.pt
m : ModuleColimit hcR hcM
⊢ ∃ U a x, (ιR cR) a = r ∧ ιM x = m

Tactic:
by
  obtain ⟨U, ⟨a, x⟩, h⟩ := Types.jointly_surjective_of_isColimit
    ((isColimitOfPreserves (forget RingCat) hcR).tensor
      (isColimitOfPreserves (forget AddCommGrpCat) hcM)) ⟨r, m⟩
  rw [Prod.ext_iff] at h
  obtain ⟨rfl, rfl⟩ := h
  exact ⟨U, a, x, rfl, rfl⟩

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.PartialAdjoint

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : D ⥤ C
X Y : F.PartialLeftAdjointSource
f : X ⟶ Y
⊢ F.partialLeftAdjointHomEquiv (F.partialLeftAdjointMap f) =
    f.hom ≫ F.partialLeftAdjointHomEquiv (𝟙 (F.partialLeftAdjointObj Y))

Tactic:
simp [partialLeftAdjointMap]

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.PartialAdjoint

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
J : Type u_1
inst✝ : Category.{v_1, u_1} J
R : J ⥤ F.PartialRightAdjointSource
c : Cone (R ⋙ F.rightAdjointObjIsDefined.ι)
hc : IsLimit c
c' : Cone (R ⋙ F.partialRightAdjoint)
hc' : IsLimit c'
Y : C
g : (F.op ⋙ yoneda.obj c.pt).obj (op Y)
j j' : J
φ : j ⟶ j'
this : c.π.app j ≫ (R.map φ).hom = c.π.app j'
⊢ g ≫ c.π.app j' = g ≫ c.π.app j ≫ (R.map φ).hom

Tactic:
this

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
J : Type u_1
inst✝ : Category.{v_1, u_1} J
R : J ⥤ F.PartialRightAdjointSource
c : Cone (R ⋙ F.rightAdjointObjIsDefined.ι)
hc : IsLimit c
c' : Cone (R ⋙ F.partialRightAdjoint)
hc' : IsLimit c'
Y : C
g : (F.op ⋙ yoneda.obj c.pt).obj (op Y)
j j' : J
φ : j ⟶ j'
this : c.π.app j ≫ (R.map φ).hom = c.π.app j'
⊢ g ≫ c.π.app j' = g ≫ c.π.app j'
Module: Mathlib.CategoryTheory.Sites.Grothendieck

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : C
S✝ R : Sieve X✝
J : GrothendieckTopology C
hro : RightOreCondition C
X Y : C
S : Sieve X
h : Y ⟶ X
Z : C
f : Z ⟶ X
hf : S.arrows f
W : C
g : W ⟶ Y
k : W ⟶ Z
comm : g ≫ h = k ≫ f
⊢ Sieve.pullback h S ∈ {S | ∃ Y_1 f, S.arrows f}

Tactic:
refine ⟨_, g, ?_⟩

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : C
S✝ R : Sieve X✝
J : GrothendieckTopology C
hro : RightOreCondition C
X Y : C
S : Sieve X
h : Y ⟶ X
Z : C
f : Z ⟶ X
hf : S.arrows f
W : C
g : W ⟶ Y
k : W ⟶ Z
comm : g ≫ h = k ≫ f
⊢ (Sieve.pullback h S).arrows g
Module: Mathlib.CategoryTheory.Sites.Pretopology

Goal state before:
pp: case a
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : sorry.HasPullbacks
inst✝³ : Limits.HasPullbacks C
J : Precoverage C
inst✝² : J.HasIsos
inst✝¹ : J.IsStableUnderBaseChange
inst✝ : J.IsStableUnderComposition
X : C
ι : Type (max u v)
Z : ι → C
g : (i : ι) → Z i ⟶ X
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → ofArrows Z g f → Presieve Y
hR : ofArrows Z g ∈ J.coverings X
hTi : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : ofArrows Z g f), Ti f H ∈ J.coverings Y
κ : ⦃Y : C⦄ → (f : Y ⟶ X) → ofArrows Z g f → Type (max u v)
W : ⦃Y : C⦄ → (f : Y ⟶ X) → (hf : ofArrows Z g f) → κ f hf → C
p : ⦃Y : C⦄ → (f : Y ⟶ X) → (hf : ofArrows Z g f) → (i : κ f hf) → W f hf i ⟶ Y
hp : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (hf : ofArrows Z g f), Ti f hf = ofArrows (W f hf) (p f hf)
T Y : C
i : ι
v : T ⟶ Z i
hv : Ti (g i) ⋯ v
⊢ ofArrows (fun ij ↦ W (g ij.fst) ⋯ ij.snd) (fun ij ↦ p (g ij.fst) ⋯ ij.snd ≫ g ij.fst) (v ≫ g i)

Tactic:
rw [hp] at hv

Goal state after:
case a
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : sorry.HasPullbacks
inst✝³ : Limits.HasPullbacks C
J : Precoverage C
inst✝² : J.HasIsos
inst✝¹ : J.IsStableUnderBaseChange
inst✝ : J.IsStableUnderComposition
X : C
ι : Type (max u v)
Z : ι → C
g : (i : ι) → Z i ⟶ X
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → ofArrows Z g f → Presieve Y
hR : ofArrows Z g ∈ J.coverings X
hTi : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : ofArrows Z g f), Ti f H ∈ J.coverings Y
κ : ⦃Y : C⦄ → (f : Y ⟶ X) → ofArrows Z g f → Type (max u v)
W : ⦃Y : C⦄ → (f : Y ⟶ X) → (hf : ofArrows Z g f) → κ f hf → C
p : ⦃Y : C⦄ → (f : Y ⟶ X) → (hf : ofArrows Z g f) → (i : κ f hf) → W f hf i ⟶ Y
hp : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (hf : ofArrows Z g f), Ti f hf = ofArrows (W f hf) (p f hf)
T Y : C
i : ι
v : T ⟶ Z i
hv : ofArrows (W (g i) ⋯) (p (g i) ⋯) v
⊢ ofArrows (fun ij ↦ W (g ij.fst) ⋯ ij.snd) (fun ij ↦ p (g ij.fst) ⋯ ij.snd ≫ g ij.fst) (v ≫ g i)
Module: Mathlib.CategoryTheory.Sites.Pretopology

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : sorry.HasPullbacks
inst✝³ : Limits.HasPullbacks C
J : Precoverage C
inst✝² : J.HasIsos
inst✝¹ : J.IsStableUnderBaseChange
inst✝ : J.IsStableUnderComposition
X : C
ι : Type (max u v)
Z : ι → C
g : (i : ι) → Z i ⟶ X
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → ofArrows Z g f → Presieve Y
hR : ofArrows Z g ∈ J.coverings X
hTi : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : ofArrows Z g f), Ti f H ∈ J.coverings Y
κ : ⦃Y : C⦄ → (f : Y ⟶ X) → ofArrows Z g f → Type (max u v)
W : ⦃Y : C⦄ → (f : Y ⟶ X) → (hf : ofArrows Z g f) → κ f hf → C
p : ⦃Y : C⦄ → (f : Y ⟶ X) → (hf : ofArrows Z g f) → (i : κ f hf) → W f hf i ⟶ Y
hp : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (hf : ofArrows Z g f), Ti f hf = ofArrows (W f hf) (p f hf)
this : (ofArrows Z g).bind Ti = ofArrows (fun ij ↦ W (g ij.fst) ⋯ ij.snd) fun ij ↦ p (g ij.fst) ⋯ ij.snd ≫ g ij.fst
⊢ (ofArrows Z g).bind Ti ∈ J.coverings X

Tactic:
this

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : sorry.HasPullbacks
inst✝³ : Limits.HasPullbacks C
J : Precoverage C
inst✝² : J.HasIsos
inst✝¹ : J.IsStableUnderBaseChange
inst✝ : J.IsStableUnderComposition
X : C
ι : Type (max u v)
Z : ι → C
g : (i : ι) → Z i ⟶ X
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → ofArrows Z g f → Presieve Y
hR : ofArrows Z g ∈ J.coverings X
hTi : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : ofArrows Z g f), Ti f H ∈ J.coverings Y
κ : ⦃Y : C⦄ → (f : Y ⟶ X) → ofArrows Z g f → Type (max u v)
W : ⦃Y : C⦄ → (f : Y ⟶ X) → (hf : ofArrows Z g f) → κ f hf → C
p : ⦃Y : C⦄ → (f : Y ⟶ X) → (hf : ofArrows Z g f) → (i : κ f hf) → W f hf i ⟶ Y
hp : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (hf : ofArrows Z g f), Ti f hf = ofArrows (W f hf) (p f hf)
this : (ofArrows Z g).bind Ti = ofArrows (fun ij ↦ W (g ij.fst) ⋯ ij.snd) fun ij ↦ p (g ij.fst) ⋯ ij.snd ≫ g ij.fst
⊢ (ofArrows (fun ij ↦ W (g ij.fst) ⋯ ij.snd) fun ij ↦ p (g ij.fst) ⋯ ij.snd ≫ g ij.fst) ∈ J.coverings X
Module: Mathlib.CategoryTheory.Sites.SheafOfTypes

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
X : C
S : Sieve X
W : C
x : FamilyOfElements (yoneda.obj W) S.arrows
hx : x.Compatible
H : IsColimit S.arrows.cocone
s : Cocone S.arrows.diagram := S.arrows.compatibleYonedaFamily_toCocone W x hx
⊢ ∃! t, x.IsAmalgamation t

Tactic:
use H.desc s

Goal state after:
case h
C : Type u
inst✝ : Category.{v, u} C
X : C
S : Sieve X
W : C
x : FamilyOfElements (yoneda.obj W) S.arrows
hx : x.Compatible
H : IsColimit S.arrows.cocone
s : Cocone S.arrows.diagram := ⋯
⊢ (fun t ↦ x.IsAmalgamation t) (H.desc s) ∧
    ∀ (y : (yoneda.obj W).obj (op X)), (fun t ↦ x.IsAmalgamation t) y → y = H.desc s
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X : C
ι : Type u_1
inst✝ : IsEmpty ι
Y : ι → C
f : (i : ι) → Y i ⟶ X
⊢ ofArrows Y f = ⊥

Tactic:
by
  rw [eq_bot_iff, ofArrows_le_iff]
  simp

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X : C
R : Presieve X
Y : D
f : Y ⟶ F.obj X
⊢ map F R f ↔ ∃ Z, ∃ (h : F.obj Z = Y), ∃ g, R g ∧ F.map g = eqToHom h ≫ f

Tactic:
refine ⟨fun (.of (u := u) hu) ↦ ⟨_, rfl, u, hu, by simp⟩, fun ⟨Z, h, g, hg, heq⟩ ↦ ?_⟩

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X : C
R : Presieve X
Y : D
f : Y ⟶ F.obj X
x✝ : ∃ Z, ∃ (h : F.obj Z = Y), ∃ g, R g ∧ F.map g = eqToHom h ≫ f
Z : C
h : F.obj Z = Y
g : Z ⟶ X
hg : R g
heq : F.map g = eqToHom h ≫ f
⊢ map F R f
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: case mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
S : Sieve X
x : FamilyOfElements P S.arrows
h : x.SieveCompatible
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
h₁ : S.arrows f₁
h₂ : S.arrows f₂
k : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ (ConcreteCategory.hom (P.map g₁.op)) (x f₁ h₁) = (ConcreteCategory.hom (P.map g₂.op)) (x f₂ h₂)

Tactic:
[

Goal state after:
case mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
S : Sieve X
x : FamilyOfElements P S.arrows
h : x.SieveCompatible
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
h₁ : S.arrows f₁
h₂ : S.arrows f₂
k : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ (ConcreteCategory.hom (P.map g₁.op)) (x f₁ h₁) = (ConcreteCategory.hom (P.map g₂.op)) (x f₂ h₂)
Module: Mathlib.CategoryTheory.Sites.EqualizerSheafCondition

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
S : Sieve X
⊢ Presieve.IsSheafFor P S.arrows ↔
    ∀ (a : Presieve.FamilyOfElements P S.arrows),
      (ConcreteCategory.hom (firstMap P S)) ((firstObjEqFamily P S.arrows).toEquiv.symm a) =
          (ConcreteCategory.hom (secondMap P S)) ((firstObjEqFamily P S.arrows).toEquiv.symm a) →
        ∃! x, (ConcreteCategory.hom (forkMap P S.arrows)) x = (firstObjEqFamily P S.arrows).toEquiv.symm a

Tactic:
[

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
S : Sieve X
⊢ Presieve.IsSheafFor P S.arrows ↔
    ∀ (a : Presieve.FamilyOfElements P S.arrows),
      (ConcreteCategory.hom (firstMap P S)) ((firstObjEqFamily P S.arrows).toEquiv.symm a) =
          (ConcreteCategory.hom (secondMap P S)) ((firstObjEqFamily P S.arrows).toEquiv.symm a) →
        ∃! x, (ConcreteCategory.hom (forkMap P S.arrows)) x = (firstObjEqFamily P S.arrows).toEquiv.symm a
Module: Mathlib.CategoryTheory.Sites.EqualizerSheafCondition

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve X
inst✝ : R.HasPairwisePullbacks
⊢ Presieve.IsSheafFor P R ↔
    ∀ (a : Presieve.FamilyOfElements P R),
      (ConcreteCategory.hom (firstMap P R)) ((firstObjEqFamily P R).toEquiv.symm a) =
          (ConcreteCategory.hom (secondMap P R)) ((firstObjEqFamily P R).toEquiv.symm a) →
        ∃! x, (ConcreteCategory.hom (forkMap P R)) x = (firstObjEqFamily P R).toEquiv.symm a

Tactic:
[

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve X
inst✝ : R.HasPairwisePullbacks
⊢ Presieve.IsSheafFor P R ↔
    ∀ (a : Presieve.FamilyOfElements P R),
      (ConcreteCategory.hom (firstMap P R)) ((firstObjEqFamily P R).toEquiv.symm a) =
          (ConcreteCategory.hom (secondMap P R)) ((firstObjEqFamily P R).toEquiv.symm a) →
        ∃! x, (ConcreteCategory.hom (forkMap P R)) x = (firstObjEqFamily P R).toEquiv.symm a
Module: Mathlib.CategoryTheory.Sites.EqualizerSheafCondition

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve X
inst✝ : R.HasPairwisePullbacks
⊢ Presieve.IsSheafFor P R ↔
    ∀ (a : Presieve.FamilyOfElements P R),
      ((firstObjEqFamily P R).toEquiv ((firstObjEqFamily P R).toEquiv.symm a)).Compatible →
        ∃! x, (ConcreteCategory.hom (forkMap P R)) x = (firstObjEqFamily P R).toEquiv.symm a

Tactic:
[

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve X
inst✝ : R.HasPairwisePullbacks
⊢ Presieve.IsSheafFor P R ↔
    ∀ (a : Presieve.FamilyOfElements P R),
      ((firstObjEqFamily P R).toEquiv ((firstObjEqFamily P R).toEquiv.symm a)).Compatible →
        ∃! x, (ConcreteCategory.hom (forkMap P R)) x = (firstObjEqFamily P R).toEquiv.symm a
Module: Mathlib.CategoryTheory.Sites.Sheaf

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : Type u₂
inst✝ : Category.{v₂, u₂} A
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
⊢ Nonempty (IsLimit (P.mapCone S.arrows.cocone.op)) ↔
    ∀ (E : Aᵒᵖ) (x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows), x.Compatible → ∃! t, x.IsAmalgamation t

Tactic:
[

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : Type u₂
inst✝ : Category.{v₂, u₂} A
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
⊢ Nonempty (IsLimit (P.mapCone S.arrows.cocone.op)) ↔
    ∀ (E : Aᵒᵖ) (x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows), x.Compatible → ∃! t, x.IsAmalgamation t
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X✝ Y✝ Z✝ : C
f✝ : Y✝ ⟶ X✝
S✝ R : Sieve X✝
inst✝ : LocallySmall.{w, v₁, u₁} C
X : C
S : Sieve X
Y Z : Cᵒᵖ
g : Y ⟶ Z
f : (shrinkYoneda.{w, v₁, u₁}.obj X).obj Y
hf : f ∈ {f | S.arrows (shrinkYonedaObjObjEquiv f)}
⊢ f ∈ ⇑(hom ((shrinkYoneda.{w, v₁, u₁}.obj X).map g)) ⁻¹' {f | S.arrows (shrinkYonedaObjObjEquiv f)}

Tactic:
by
    simpa [shrinkYonedaObjObjEquiv_obj_map] using S.downward_closed hf _

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type t
inst✝¹ : Small.{w, t} I
X : I → C
π : (i : I) → X i ⟶ B
inst✝ : (Presieve.ofArrows X π).HasPairwisePullbacks
⊢ (∀ (x : (i : I) → P.obj (op (X i))),
      Arrows.Compatible P π x → ∃! t, ∀ (i : I), (ConcreteCategory.hom (P.map (π i).op)) t = x i) ↔
    ∀ (a : (j : I) → P.obj (op (X j))),
      (ConcreteCategory.hom (firstMap P X π))
            (((equivShrink ((j : I) → P.obj (op (X j)))).trans
                (Types.Small.productIso fun i ↦ P.obj (op (X i))).toEquiv.symm)
              a) =
          (ConcreteCategory.hom (secondMap P X π))
            (((equivShrink ((j : I) → P.obj (op (X j)))).trans
                (Types.Small.productIso fun i ↦ P.obj (op (X i))).toEquiv.symm)
              a) →
        ∃! x,
          (ConcreteCategory.hom (forkMap P X π)) x =
            ((equivShrink ((j : I) → P.obj (op (X j)))).trans
                (Types.Small.productIso fun i ↦ P.obj (op (X i))).toEquiv.symm)
              a

Tactic:
[

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type t
inst✝¹ : Small.{w, t} I
X : I → C
π : (i : I) → X i ⟶ B
inst✝ : (Presieve.ofArrows X π).HasPairwisePullbacks
⊢ (∀ (x : (i : I) → P.obj (op (X i))),
      Arrows.Compatible P π x → ∃! t, ∀ (i : I), (ConcreteCategory.hom (P.map (π i).op)) t = x i) ↔
    ∀ (a : (j : I) → P.obj (op (X j))),
      (ConcreteCategory.hom (firstMap P X π))
            (((equivShrink ((j : I) → P.obj (op (X j)))).trans
                (Types.Small.productIso fun i ↦ P.obj (op (X i))).toEquiv.symm)
              a) =
          (ConcreteCategory.hom (secondMap P X π))
            (((equivShrink ((j : I) → P.obj (op (X j)))).trans
                (Types.Small.productIso fun i ↦ P.obj (op (X i))).toEquiv.symm)
              a) →
        ∃! x,
          (ConcreteCategory.hom (forkMap P X π)) x =
            ((equivShrink ((j : I) → P.obj (op (X j)))).trans
                (Types.Small.productIso fun i ↦ P.obj (op (X i))).toEquiv.symm)
              a
Module: Mathlib.CategoryTheory.Sites.Sheaf

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
A : Type u₂
inst✝¹ : Category.{v₂, u₂} A
P : Cᵒᵖ ⥤ A
inst✝ : HasPullbacks C
K : Pretopology C
⊢ (∀ (E : A), Presieve.IsSheaf K.toGrothendieck (P ⋙ coyoneda.obj (op E))) ↔
    ∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, Nonempty (IsLimit (P.mapCone (generate R).arrows.cocone.op))

Tactic:
[

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
A : Type u₂
inst✝¹ : Category.{v₂, u₂} A
P : Cᵒᵖ ⥤ A
inst✝ : HasPullbacks C
K : Pretopology C
⊢ (∀ (E : A), Presieve.IsSheaf K.toGrothendieck (P ⋙ coyoneda.obj (op E))) ↔
    ∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, Nonempty (IsLimit (P.mapCone (generate R).arrows.cocone.op))
Module: Mathlib.CategoryTheory.Sites.EqualizerSheafCondition

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type u_1
X Y : C
f : X ⟶ Y
c : PullbackCone f f
hc : IsLimit c
h :
  ∀ (x : F.obj (op X)),
    (∀ {Z : C} (p₁ p₂ : Z ⟶ X),
        p₁ ≫ f = p₂ ≫ f → (ConcreteCategory.hom (F.map p₁.op)) x = (ConcreteCategory.hom (F.map p₂.op)) x) ↔
      (ConcreteCategory.hom (F.map c.fst.op)) x = (ConcreteCategory.hom (F.map c.snd.op)) x
⊢ (∀ (x : F.obj (op X)),
      (∀ {Z : C} (p₁ p₂ : Z ⟶ X),
          p₁ ≫ f = p₂ ≫ f → (ConcreteCategory.hom (F.map p₁.op)) x = (ConcreteCategory.hom (F.map p₂.op)) x) →
        ∃! y, (ConcreteCategory.hom (F.map f.op)) y = x) ↔
    ∀ (y : F.obj (op X)),
      (ConcreteCategory.hom (F.map c.fst.op)) y = (ConcreteCategory.hom (F.map c.snd.op)) y →
        ∃! x, (ConcreteCategory.hom (F.map f.op)) x = y

Tactic:
[

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type u_1
X Y : C
f : X ⟶ Y
c : PullbackCone f f
hc : IsLimit c
h :
  ∀ (x : F.obj (op X)),
    (∀ {Z : C} (p₁ p₂ : Z ⟶ X),
        p₁ ≫ f = p₂ ≫ f → (ConcreteCategory.hom (F.map p₁.op)) x = (ConcreteCategory.hom (F.map p₂.op)) x) ↔
      (ConcreteCategory.hom (F.map c.fst.op)) x = (ConcreteCategory.hom (F.map c.snd.op)) x
⊢ (∀ (x : F.obj (op X)),
      (∀ {Z : C} (p₁ p₂ : Z ⟶ X),
          p₁ ≫ f = p₂ ≫ f → (ConcreteCategory.hom (F.map p₁.op)) x = (ConcreteCategory.hom (F.map p₂.op)) x) →
        ∃! y, (ConcreteCategory.hom (F.map f.op)) y = x) ↔
    ∀ (y : F.obj (op X)),
      (ConcreteCategory.hom (F.map c.fst.op)) y = (ConcreteCategory.hom (F.map c.snd.op)) y →
        ∃! x, (ConcreteCategory.hom (F.map f.op)) x = y
Module: Mathlib.CategoryTheory.Sites.Plus

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{w', w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
P✝ : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
X Y : Cᵒᵖ
f : X ⟶ Y
j✝ : (J.Cover (unop X))ᵒᵖ
⊢ Multiequalizer.lift ((unop ((J.pullback f.unop).op.obj j✝)).index P) ((J.diagram P (unop X)).obj j✝)
        (fun I ↦ Multiequalizer.ι ((unop j✝).index P) (Cover.Arrow.base I)) ⋯ ≫
      (J.diagramNatTrans η (unop Y)).app ((J.pullback f.unop).op.obj j✝) ≫
        colimit.ι (J.diagram Q (unop Y)) ((J.pullback f.unop).op.obj j✝) =
    (J.diagramNatTrans η (unop X)).app j✝ ≫
      Multiequalizer.lift ((unop ((J.pullback f.unop).op.obj j✝)).index Q) ((J.diagram Q (unop X)).obj j✝)
          (fun I ↦ Multiequalizer.ι ((unop j✝).index Q) (Cover.Arrow.base I)) ⋯ ≫
        colimit.ι (J.diagram Q (unop Y)) ((J.pullback f.unop).op.obj j✝)

Tactic:
[

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{w', w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
P✝ : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
X Y : Cᵒᵖ
f : X ⟶ Y
j✝ : (J.Cover (unop X))ᵒᵖ
⊢ Multiequalizer.lift ((unop ((J.pullback f.unop).op.obj j✝)).index P) ((J.diagram P (unop X)).obj j✝)
        (fun I ↦ Multiequalizer.ι ((unop j✝).index P) (Cover.Arrow.base I)) ⋯ ≫
      (J.diagramNatTrans η (unop Y)).app ((J.pullback f.unop).op.obj j✝) ≫
        colimit.ι (J.diagram Q (unop Y)) ((J.pullback f.unop).op.obj j✝) =
    (J.diagramNatTrans η (unop X)).app j✝ ≫
      Multiequalizer.lift ((unop ((J.pullback f.unop).op.obj j✝)).index Q) ((J.diagram Q (unop X)).obj j✝)
          (fun I ↦ Multiequalizer.ι ((unop j✝).index Q) (Cover.Arrow.base I)) ⋯ ≫
        colimit.ι (J.diagram Q (unop Y)) ((J.pullback f.unop).op.obj j✝)
Module: Mathlib.CategoryTheory.Sites.Plus

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{w', w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
x✝ : Cᵒᵖ
⊢ η.app x✝ ≫
      Multiequalizer.lift (⊤.index Q) (Q.obj (op (unop x✝))) (fun I ↦ Q.map I.f.op) ⋯ ≫
        colimit.ι (J.diagram Q (unop x✝)) (op ⊤) =
    Multiequalizer.lift (⊤.index P) (P.obj (op (unop x✝))) (fun I ↦ P.map I.f.op) ⋯ ≫
      (J.diagramNatTrans η (unop x✝)).app (op ⊤) ≫ colimit.ι (J.diagram Q (unop x✝)) (op ⊤)

Tactic:
[

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{w', w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
x✝ : Cᵒᵖ
⊢ η.app x✝ ≫
      Multiequalizer.lift (⊤.index Q) (Q.obj (op (unop x✝))) (fun I ↦ Q.map I.f.op) ⋯ ≫
        colimit.ι (J.diagram Q (unop x✝)) (op ⊤) =
    Multiequalizer.lift (⊤.index P) (P.obj (op (unop x✝))) (fun I ↦ P.map I.f.op) ⋯ ≫
      (J.diagramNatTrans η (unop x✝)).app (op ⊤) ≫ colimit.ι (J.diagram Q (unop x✝)) (op ⊤)