mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Submodule

Goal state before:
pp: case mk.mk
C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M : PresheafOfModules R
obj✝¹ : (X : Cᵒᵖ) → _root_.Submodule ↑(R.obj X) ↑(M.obj X)
map✝¹ : ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y), obj✝¹ X ≤ Submodule.comap (M.restrictₛₗ f) (obj✝¹ Y)
obj✝ : (X : Cᵒᵖ) → _root_.Submodule ↑(R.obj X) ↑(M.obj X)
map✝ : ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y), obj✝ X ≤ Submodule.comap (M.restrictₛₗ f) (obj✝ Y)
h : ∀ (X : Cᵒᵖ), { obj := obj✝¹, map := map✝¹ }.obj X = { obj := obj✝, map := map✝ }.obj X
⊢ { obj := obj✝¹, map := map✝¹ } = { obj := obj✝, map := map✝ }

Tactic:
;

Goal state after:
case mk.mk
C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M : PresheafOfModules R
obj✝¹ : (X : Cᵒᵖ) → _root_.Submodule ↑(R.obj X) ↑(M.obj X)
map✝¹ : ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y), obj✝¹ X ≤ Submodule.comap (M.restrictₛₗ f) (obj✝¹ Y)
obj✝ : (X : Cᵒᵖ) → _root_.Submodule ↑(R.obj X) ↑(M.obj X)
map✝ : ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y), obj✝ X ≤ Submodule.comap (M.restrictₛₗ f) (obj✝ Y)
h : ∀ (X : Cᵒᵖ), { obj := obj✝¹, map := map✝¹ }.obj X = { obj := obj✝, map := map✝ }.obj X
⊢ { obj := obj✝¹, map := map✝¹ } = { obj := obj✝, map := map✝ }
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Submodule

Goal state before:
pp: case mk.mk
C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M : PresheafOfModules R
obj✝¹ : (X : Cᵒᵖ) → _root_.Submodule ↑(R.obj X) ↑(M.obj X)
map✝¹ : ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y), obj✝¹ X ≤ Submodule.comap (M.restrictₛₗ f) (obj✝¹ Y)
obj✝ : (X : Cᵒᵖ) → _root_.Submodule ↑(R.obj X) ↑(M.obj X)
map✝ : ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y), obj✝ X ≤ Submodule.comap (M.restrictₛₗ f) (obj✝ Y)
h : ∀ (X : Cᵒᵖ), { obj := obj✝¹, map := map✝¹ }.obj X = { obj := obj✝, map := map✝ }.obj X
⊢ obj✝¹ = obj✝

Tactic:
;

Goal state after:
case mk.mk
C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M : PresheafOfModules R
obj✝¹ : (X : Cᵒᵖ) → _root_.Submodule ↑(R.obj X) ↑(M.obj X)
map✝¹ : ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y), obj✝¹ X ≤ Submodule.comap (M.restrictₛₗ f) (obj✝¹ Y)
obj✝ : (X : Cᵒᵖ) → _root_.Submodule ↑(R.obj X) ↑(M.obj X)
map✝ : ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y), obj✝ X ≤ Submodule.comap (M.restrictₛₗ f) (obj✝ Y)
h : ∀ (X : Cᵒᵖ), { obj := obj✝¹, map := map✝¹ }.obj X = { obj := obj✝, map := map✝ }.obj X
⊢ obj✝¹ = obj✝
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Submodule

Goal state before:
pp: case mk.mk
C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M : PresheafOfModules R
obj✝¹ : (X : Cᵒᵖ) → _root_.Submodule ↑(R.obj X) ↑(M.obj X)
map✝¹ : ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y), obj✝¹ X ≤ Submodule.comap (M.restrictₛₗ f) (obj✝¹ Y)
obj✝ : (X : Cᵒᵖ) → _root_.Submodule ↑(R.obj X) ↑(M.obj X)
map✝ : ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y), obj✝ X ≤ Submodule.comap (M.restrictₛₗ f) (obj✝ Y)
h : ∀ (X : Cᵒᵖ), { obj := obj✝¹, map := map✝¹ }.obj X = { obj := obj✝, map := map✝ }.obj X
X : Cᵒᵖ
⊢ obj✝¹ X = obj✝ X

Tactic:
;

Goal state after:
case mk.mk
C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M : PresheafOfModules R
obj✝¹ : (X : Cᵒᵖ) → _root_.Submodule ↑(R.obj X) ↑(M.obj X)
map✝¹ : ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y), obj✝¹ X ≤ Submodule.comap (M.restrictₛₗ f) (obj✝¹ Y)
obj✝ : (X : Cᵒᵖ) → _root_.Submodule ↑(R.obj X) ↑(M.obj X)
map✝ : ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y), obj✝ X ≤ Submodule.comap (M.restrictₛₗ f) (obj✝ Y)
h : ∀ (X : Cᵒᵖ), { obj := obj✝¹, map := map✝¹ }.obj X = { obj := obj✝, map := map✝ }.obj X
X : Cᵒᵖ
⊢ obj✝¹ X = obj✝ X
Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : S.ShortExact
n : ℕ
h₁ : HasProjectiveDimensionLT S.X₁ n
h₃ : HasProjectiveDimensionLT S.X₃ n
this : HasExt C := HasExt.standard C
i : ℕ
hi : n ≤ i
Y : C
x₂ : Ext S.X₂ Y i
⊢ x₂ = 0

Tactic:
obtain ⟨x₃, rfl⟩ := Ext.contravariant_sequence_exact₂ hS _ x₂
    (Ext.eq_zero_of_hasProjectiveDimensionLT _ n hi)

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : S.ShortExact
n : ℕ
h₁ : HasProjectiveDimensionLT S.X₁ n
h₃ : HasProjectiveDimensionLT S.X₃ n
this : HasExt C := HasExt.standard C
i : ℕ
hi : n ≤ i
Y : C
x₃ : Ext S.X₃ Y i
⊢ (Ext.mk₀ S.g).comp x₃ ⋯ = 0
Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
inst✝ : EnoughInjectives C
X : C
n : ℕ
hX : ∀ (Y : C), Subsingleton (Ext X Y n)
k : ℕ
hk : ∀ ⦃d : ℕ⦄ ⦃Y : C⦄ (e : Ext X Y d), d = n + k → e = 0
Y : C
p : InjectivePresentation Y
h : { X₁ := Y, X₂ := p.J, X₃ := cokernel p.f, f := p.f, g := cokernel.π p.f, zero := ⋯ }.ShortExact
e : Ext X Y (n + k + 1)
hd : n + k + 1 = n + (k + 1)
⊢ e.comp (Ext.mk₀ { X₁ := Y, X₂ := p.J, X₃ := cokernel p.f, f := p.f, g := cokernel.π p.f, zero := ⋯ }.f) ⋯ = 0

Tactic:
;

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)
k : ℕ
hk : ∀ ⦃d : ℕ⦄ ⦃Y : C⦄ (e : Ext X Y d), d = n + k → e = 0
Y : C
p : InjectivePresentation Y
h : { X₁ := Y, X₂ := p.J, X₃ := cokernel p.f, f := p.f, g := cokernel.π p.f, zero := ⋯ }.ShortExact
e : Ext X Y (n + k + 1)
hd : n + k + 1 = n + (k + 1)
⊢ e.comp (Ext.mk₀ { X₁ := Y, X₂ := p.J, X₃ := cokernel p.f, f := p.f, g := cokernel.π p.f, zero := ⋯ }.f) ⋯ = 0
Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
n : ℕ
⊢ projectiveDimension X < ↑n ↔ HasProjectiveDimensionLT X n

Tactic:
;

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
n : ℕ
⊢ projectiveDimension X < ↑n ↔ HasProjectiveDimensionLT X n
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
M : SheafOfModules R
⊢ ((CategoryTheory.sheafificationAdjunction J AddCommGrpCat).homEquiv
          ((SheafOfModules.forget R ⋙ restrictScalars α).obj M).presheaf
          ((SheafOfModules.toSheaf R).obj ((𝟭 (SheafOfModules R)).obj M))).symm
      ((toPresheaf R₀).map (𝟙 ((SheafOfModules.forget R ⋙ restrictScalars α).obj M))) =
    ((CategoryTheory.sheafificationAdjunction J AddCommGrpCat).homEquiv
          ((sheafToPresheaf J AddCommGrpCat).obj ((SheafOfModules.toSheaf R).obj M))
          ((SheafOfModules.toSheaf R).obj M)).symm
      (𝟙 ((sheafToPresheaf J AddCommGrpCat).obj ((SheafOfModules.toSheaf R).obj M)))

Tactic:
;

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
M : SheafOfModules R
⊢ ((CategoryTheory.sheafificationAdjunction J AddCommGrpCat).homEquiv
          ((SheafOfModules.forget R ⋙ restrictScalars α).obj M).presheaf
          ((SheafOfModules.toSheaf R).obj ((𝟭 (SheafOfModules R)).obj M))).symm
      ((toPresheaf R₀).map (𝟙 ((SheafOfModules.forget R ⋙ restrictScalars α).obj M))) =
    ((CategoryTheory.sheafificationAdjunction J AddCommGrpCat).homEquiv
          ((sheafToPresheaf J AddCommGrpCat).obj ((SheafOfModules.toSheaf R).obj M))
          ((SheafOfModules.toSheaf R).obj M)).symm
      (𝟙 ((sheafToPresheaf J AddCommGrpCat).obj ((SheafOfModules.toSheaf R).obj M)))
Module: Mathlib.CategoryTheory.Bicategory.LocallyDiscrete

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
a✝ b✝ c✝ d✝ : LocallyDiscrete C
f : a✝ ⟶ b✝
g : b✝ ⟶ c✝
h : c✝ ⟶ d✝
⊢ ((f ≫ g) ≫ h).as = (f ≫ g ≫ h).as

Tactic:
;

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
a✝ b✝ c✝ d✝ : LocallyDiscrete C
f : a✝ ⟶ b✝
g : b✝ ⟶ c✝
h : c✝ ⟶ d✝
⊢ ((f ≫ g) ≫ h).as = (f ≫ g ≫ h).as
Module: Mathlib.CategoryTheory.Bicategory.LocallyDiscrete

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
a✝ b✝ : LocallyDiscrete C
f : a✝ ⟶ b✝
⊢ (𝟙 a✝ ≫ f).as = f.as

Tactic:
;

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
a✝ b✝ : LocallyDiscrete C
f : a✝ ⟶ b✝
⊢ (𝟙 a✝ ≫ f).as = f.as
Module: Mathlib.CategoryTheory.Bicategory.LocallyDiscrete

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
a✝ b✝ : LocallyDiscrete C
f : a✝ ⟶ b✝
⊢ (f ≫ 𝟙 b✝).as = f.as

Tactic:
;

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
a✝ b✝ : LocallyDiscrete C
f : a✝ ⟶ b✝
⊢ (f ≫ 𝟙 b✝).as = f.as
Module: Mathlib.CategoryTheory.Bicategory.LocallyDiscrete

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
a : C
⊢ (eqToHom ⋯).toLoc = eqToHom ⋯

Tactic:
;

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
a : C
⊢ (eqToHom ⋯).toLoc = eqToHom ⋯
Module: Mathlib.Algebra.Category.ModuleCat.Pseudofunctor

Goal state before:
pp: case refine_1
b₀✝ b₁✝ b₂✝ b₃✝ : CommRingCat
f✝ : b₀✝ ⟶ b₁✝
g✝ : b₁✝ ⟶ b₂✝
h✝ : b₂✝ ⟶ b₃✝
⊢ (Cat.Hom.isoMk (extendScalarsComp (Hom.hom (f✝ ≫ g✝)) (Hom.hom h✝))).hom ≫
      Bicategory.whiskerRight (Cat.Hom.isoMk (extendScalarsComp (Hom.hom f✝) (Hom.hom g✝))).hom
          (extendScalars (Hom.hom h✝)).toCatHom ≫
        (Bicategory.associator (extendScalars (Hom.hom f✝)).toCatHom (extendScalars (Hom.hom g✝)).toCatHom
              (extendScalars (Hom.hom h✝)).toCatHom).hom ≫
          Bicategory.whiskerLeft (extendScalars (Hom.hom f✝)).toCatHom
              (Cat.Hom.isoMk (extendScalarsComp (Hom.hom g✝) (Hom.hom h✝))).inv ≫
            (Cat.Hom.isoMk (extendScalarsComp (Hom.hom f✝) (Hom.hom (g✝ ≫ h✝)))).inv =
    eqToHom ⋯

Tactic:
;

Goal state after:
case refine_1
b₀✝ b₁✝ b₂✝ b₃✝ : CommRingCat
f✝ : b₀✝ ⟶ b₁✝
g✝ : b₁✝ ⟶ b₂✝
h✝ : b₂✝ ⟶ b₃✝
⊢ (Cat.Hom.isoMk (extendScalarsComp (Hom.hom (f✝ ≫ g✝)) (Hom.hom h✝))).hom ≫
      Bicategory.whiskerRight (Cat.Hom.isoMk (extendScalarsComp (Hom.hom f✝) (Hom.hom g✝))).hom
          (extendScalars (Hom.hom h✝)).toCatHom ≫
        (Bicategory.associator (extendScalars (Hom.hom f✝)).toCatHom (extendScalars (Hom.hom g✝)).toCatHom
              (extendScalars (Hom.hom h✝)).toCatHom).hom ≫
          Bicategory.whiskerLeft (extendScalars (Hom.hom f✝)).toCatHom
              (Cat.Hom.isoMk (extendScalarsComp (Hom.hom g✝) (Hom.hom h✝))).inv ≫
            (Cat.Hom.isoMk (extendScalarsComp (Hom.hom f✝) (Hom.hom (g✝ ≫ h✝)))).inv =
    eqToHom ⋯
Module: Mathlib.Algebra.Category.ModuleCat.Pseudofunctor

Goal state before:
pp: case refine_1
b₀✝ b₁✝ b₂✝ b₃✝ : CommRingCat
f✝ : b₀✝ ⟶ b₁✝
g✝ : b₁✝ ⟶ b₂✝
h✝ : b₂✝ ⟶ b₃✝
⊢ ((Cat.Hom.isoMk (extendScalarsComp (Hom.hom (f✝ ≫ g✝)) (Hom.hom h✝))).hom ≫
        Bicategory.whiskerRight (Cat.Hom.isoMk (extendScalarsComp (Hom.hom f✝) (Hom.hom g✝))).hom
            (extendScalars (Hom.hom h✝)).toCatHom ≫
          (Bicategory.associator (extendScalars (Hom.hom f✝)).toCatHom (extendScalars (Hom.hom g✝)).toCatHom
                (extendScalars (Hom.hom h✝)).toCatHom).hom ≫
            Bicategory.whiskerLeft (extendScalars (Hom.hom f✝)).toCatHom
                (Cat.Hom.isoMk (extendScalarsComp (Hom.hom g✝) (Hom.hom h✝))).inv ≫
              (Cat.Hom.isoMk (extendScalarsComp (Hom.hom f✝) (Hom.hom (g✝ ≫ h✝)))).inv).toNatTrans =
    (eqToHom ⋯).toNatTrans

Tactic:
;

Goal state after:
case refine_1
b₀✝ b₁✝ b₂✝ b₃✝ : CommRingCat
f✝ : b₀✝ ⟶ b₁✝
g✝ : b₁✝ ⟶ b₂✝
h✝ : b₂✝ ⟶ b₃✝
⊢ ((Cat.Hom.isoMk (extendScalarsComp (Hom.hom (f✝ ≫ g✝)) (Hom.hom h✝))).hom ≫
        Bicategory.whiskerRight (Cat.Hom.isoMk (extendScalarsComp (Hom.hom f✝) (Hom.hom g✝))).hom
            (extendScalars (Hom.hom h✝)).toCatHom ≫
          (Bicategory.associator (extendScalars (Hom.hom f✝)).toCatHom (extendScalars (Hom.hom g✝)).toCatHom
                (extendScalars (Hom.hom h✝)).toCatHom).hom ≫
            Bicategory.whiskerLeft (extendScalars (Hom.hom f✝)).toCatHom
                (Cat.Hom.isoMk (extendScalarsComp (Hom.hom g✝) (Hom.hom h✝))).inv ≫
              (Cat.Hom.isoMk (extendScalarsComp (Hom.hom f✝) (Hom.hom (g✝ ≫ h✝)))).inv).toNatTrans =
    (eqToHom ⋯).toNatTrans
Module: Mathlib.Algebra.Category.ModuleCat.Pseudofunctor

Goal state before:
pp: case refine_2
b₀✝ b₁✝ : CommRingCat
f✝ : b₀✝ ⟶ b₁✝
⊢ (Cat.Hom.isoMk (extendScalarsComp (Hom.hom (𝟙 b₀✝)) (Hom.hom f✝))).hom ≫
      Bicategory.whiskerRight (Cat.Hom.isoMk (extendScalarsId ↑b₀✝)).hom (extendScalars (Hom.hom f✝)).toCatHom ≫
        (Bicategory.leftUnitor (extendScalars (Hom.hom f✝)).toCatHom).hom =
    eqToHom ⋯

Tactic:
;

Goal state after:
case refine_2
b₀✝ b₁✝ : CommRingCat
f✝ : b₀✝ ⟶ b₁✝
⊢ (Cat.Hom.isoMk (extendScalarsComp (Hom.hom (𝟙 b₀✝)) (Hom.hom f✝))).hom ≫
      Bicategory.whiskerRight (Cat.Hom.isoMk (extendScalarsId ↑b₀✝)).hom (extendScalars (Hom.hom f✝)).toCatHom ≫
        (Bicategory.leftUnitor (extendScalars (Hom.hom f✝)).toCatHom).hom =
    eqToHom ⋯
Module: Mathlib.Algebra.Category.ModuleCat.Pseudofunctor

Goal state before:
pp: case refine_2
b₀✝ b₁✝ : CommRingCat
f✝ : b₀✝ ⟶ b₁✝
⊢ ((Cat.Hom.isoMk (extendScalarsComp (Hom.hom (𝟙 b₀✝)) (Hom.hom f✝))).hom ≫
        Bicategory.whiskerRight (Cat.Hom.isoMk (extendScalarsId ↑b₀✝)).hom (extendScalars (Hom.hom f✝)).toCatHom ≫
          (Bicategory.leftUnitor (extendScalars (Hom.hom f✝)).toCatHom).hom).toNatTrans =
    (eqToHom ⋯).toNatTrans

Tactic:
;

Goal state after:
case refine_2
b₀✝ b₁✝ : CommRingCat
f✝ : b₀✝ ⟶ b₁✝
⊢ ((Cat.Hom.isoMk (extendScalarsComp (Hom.hom (𝟙 b₀✝)) (Hom.hom f✝))).hom ≫
        Bicategory.whiskerRight (Cat.Hom.isoMk (extendScalarsId ↑b₀✝)).hom (extendScalars (Hom.hom f✝)).toCatHom ≫
          (Bicategory.leftUnitor (extendScalars (Hom.hom f✝)).toCatHom).hom).toNatTrans =
    (eqToHom ⋯).toNatTrans
Module: Mathlib.Algebra.Category.ModuleCat.Pseudofunctor

Goal state before:
pp: case refine_3
b₀✝ b₁✝ : CommRingCat
f✝ : b₀✝ ⟶ b₁✝
⊢ (Cat.Hom.isoMk (extendScalarsComp (Hom.hom f✝) (Hom.hom (𝟙 b₁✝)))).hom ≫
      Bicategory.whiskerLeft (extendScalars (Hom.hom f✝)).toCatHom (Cat.Hom.isoMk (extendScalarsId ↑b₁✝)).hom ≫
        (Bicategory.rightUnitor (extendScalars (Hom.hom f✝)).toCatHom).hom =
    eqToHom ⋯

Tactic:
;

Goal state after:
case refine_3
b₀✝ b₁✝ : CommRingCat
f✝ : b₀✝ ⟶ b₁✝
⊢ (Cat.Hom.isoMk (extendScalarsComp (Hom.hom f✝) (Hom.hom (𝟙 b₁✝)))).hom ≫
      Bicategory.whiskerLeft (extendScalars (Hom.hom f✝)).toCatHom (Cat.Hom.isoMk (extendScalarsId ↑b₁✝)).hom ≫
        (Bicategory.rightUnitor (extendScalars (Hom.hom f✝)).toCatHom).hom =
    eqToHom ⋯
Module: Mathlib.Algebra.Category.ModuleCat.Pseudofunctor

Goal state before:
pp: case refine_3
b₀✝ b₁✝ : CommRingCat
f✝ : b₀✝ ⟶ b₁✝
⊢ ((Cat.Hom.isoMk (extendScalarsComp (Hom.hom f✝) (Hom.hom (𝟙 b₁✝)))).hom ≫
        Bicategory.whiskerLeft (extendScalars (Hom.hom f✝)).toCatHom (Cat.Hom.isoMk (extendScalarsId ↑b₁✝)).hom ≫
          (Bicategory.rightUnitor (extendScalars (Hom.hom f✝)).toCatHom).hom).toNatTrans =
    (eqToHom ⋯).toNatTrans

Tactic:
;

Goal state after:
case refine_3
b₀✝ b₁✝ : CommRingCat
f✝ : b₀✝ ⟶ b₁✝
⊢ ((Cat.Hom.isoMk (extendScalarsComp (Hom.hom f✝) (Hom.hom (𝟙 b₁✝)))).hom ≫
        Bicategory.whiskerLeft (extendScalars (Hom.hom f✝)).toCatHom (Cat.Hom.isoMk (extendScalarsId ↑b₁✝)).hom ≫
          (Bicategory.rightUnitor (extendScalars (Hom.hom f✝)).toCatHom).hom).toNatTrans =
    (eqToHom ⋯).toNatTrans
Module: Mathlib.Algebra.Category.ModuleCat.Pseudofunctor

Goal state before:
pp: ⊢ Pseudofunctor (LocallyDiscrete CommRingCat) Cat

Tactic:
refine LocallyDiscrete.mkPseudofunctor
    (fun R ↦ Cat.of (ModuleCat.{u} R))
    (fun f ↦ (extendScalars f.hom).toCatHom)
    (fun R ↦ Cat.Hom.isoMk <| extendScalarsId R)
    (fun f g ↦ Cat.Hom.isoMk <| extendScalarsComp f.hom g.hom) ?_ ?_ ?_
  · intros; ext1; apply extendScalars_assoc'
  · intros; ext1; apply extendScalars_id_comp
  · intros; ext1; apply extendScalars_comp_id

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasCoproducts C
R : C
J : Type u'
x✝¹ : Category.{v', u'} J
K : J ⥤ Type w
c : Cocone K
hc : (K.coconeTypesEquiv.symm c).IsColimit
s : Cocone (K ⋙ sigmaConst.obj R)
j✝ j'✝ : J
g : j✝ ⟶ j'✝
x✝ : (fun X ↦ X) (K.obj j✝)
⊢ ((fun k ↦ Sigma.ι (fun x ↦ R) k ≫ s.ι.app j'✝) ∘ ⇑(ConcreteCategory.hom (K.map g))) x✝ =
    Sigma.ι (fun x ↦ R) x✝ ≫ s.ι.app j✝

Tactic:
;

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasCoproducts C
R : C
J : Type u'
x✝¹ : Category.{v', u'} J
K : J ⥤ Type w
c : Cocone K
hc : (K.coconeTypesEquiv.symm c).IsColimit
s : Cocone (K ⋙ sigmaConst.obj R)
j✝ j'✝ : J
g : j✝ ⟶ j'✝
x✝ : (fun X ↦ X) (K.obj j✝)
⊢ ((fun k ↦ Sigma.ι (fun x ↦ R) k ≫ s.ι.app j'✝) ∘ ⇑(ConcreteCategory.hom (K.map g))) x✝ =
    Sigma.ι (fun x ↦ R) x✝ ≫ s.ι.app j✝
Module: Mathlib.CategoryTheory.Limits.Preserves.SigmaConst

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
R : C
α : Type u_1
β : Type u_2
f : α → β
inst✝² : HasCoproduct fun x ↦ R
inst✝¹ : HasCoproduct fun x ↦ R
inst✝ : HasCoproduct fun x ↦ R
b✝ : α
⊢ (Sigma.ι (fun x ↦ R) b✝ ≫
      (Sigma.map' f fun x ↦ 𝟙 R) ≫
        Sigma.desc fun b ↦ if hb : b ∈ (Set.range f)ᶜ then Sigma.ι (fun x ↦ R) ⟨b, hb⟩ else 0) =
    Sigma.ι (fun x ↦ R) b✝ ≫ 0

Tactic:
;

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
R : C
α : Type u_1
β : Type u_2
f : α → β
inst✝² : HasCoproduct fun x ↦ R
inst✝¹ : HasCoproduct fun x ↦ R
inst✝ : HasCoproduct fun x ↦ R
b✝ : α
⊢ (Sigma.ι (fun x ↦ R) b✝ ≫
      (Sigma.map' f fun x ↦ 𝟙 R) ≫
        Sigma.desc fun b ↦ if hb : b ∈ (Set.range f)ᶜ then Sigma.ι (fun x ↦ R) ⟨b, hb⟩ else 0) =
    Sigma.ι (fun x ↦ R) b✝ ≫ 0
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:
;

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
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
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
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

Tactic:
;

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.Limits.Preserves.SigmaConst

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
R : C
inst✝ : HasCoproducts C
α β : Type w
f : α ⟶ β
⊢ HasCokernel (Sigma.map' ⇑(ConcreteCategory.hom f) fun x ↦ 𝟙 R)

Tactic:
;

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
R : C
inst✝ : HasCoproducts C
α β : Type w
f : α ⟶ β
⊢ HasCokernel (Sigma.map' ⇑(ConcreteCategory.hom f) fun x ↦ 𝟙 R)
Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Free

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : GrothendieckTopology C
R : Sheaf J RingCat
inst✝¹ : HasWeakSheafify J AddCommGrpCat
inst✝ : J.WEqualsLocallyBijective AddCommGrpCat
M : SheafOfModules R
I : Type u
f : I → M.sections
i : I
⊢ (fun f i ↦ M.unitHomEquiv (ιFree i ≫ f))
      ((fun s ↦ Cofan.IsColimit.desc (isColimitFreeCofan I) fun i ↦ M.unitHomEquiv.symm (s i)) f) i =
    f i

Tactic:
;

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : GrothendieckTopology C
R : Sheaf J RingCat
inst✝¹ : HasWeakSheafify J AddCommGrpCat
inst✝ : J.WEqualsLocallyBijective AddCommGrpCat
M : SheafOfModules R
I : Type u
f : I → M.sections
i : I
⊢ (fun f i ↦ M.unitHomEquiv (ιFree i ≫ f))
      ((fun s ↦ Cofan.IsColimit.desc (isColimitFreeCofan I) fun i ↦ M.unitHomEquiv.symm (s i)) f) i =
    f i
Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Free

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : GrothendieckTopology C
R : Sheaf J RingCat
inst✝¹ : HasWeakSheafify J AddCommGrpCat
inst✝ : J.WEqualsLocallyBijective AddCommGrpCat
M N : SheafOfModules R
I : Type u
s : I → M.sections
p : M ⟶ N
x✝ : I
X✝ : Cᵒᵖ
⊢ ↑(N.freeHomEquiv (M.freeHomEquiv.symm s ≫ p) x✝) X✝ =
    ↑(N.freeHomEquiv (N.freeHomEquiv.symm fun i ↦ sectionsMap p (s i)) x✝) X✝

Tactic:
;

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : GrothendieckTopology C
R : Sheaf J RingCat
inst✝¹ : HasWeakSheafify J AddCommGrpCat
inst✝ : J.WEqualsLocallyBijective AddCommGrpCat
M N : SheafOfModules R
I : Type u
s : I → M.sections
p : M ⟶ N
x✝ : I
X✝ : Cᵒᵖ
⊢ ↑(N.freeHomEquiv (M.freeHomEquiv.symm s ≫ p) x✝) X✝ =
    ↑(N.freeHomEquiv (N.freeHomEquiv.symm fun i ↦ sectionsMap p (s i)) x✝) X✝
Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Free

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J✝ : GrothendieckTopology C
R : Sheaf J✝ RingCat
inst✝¹ : HasWeakSheafify J✝ AddCommGrpCat
inst✝ : J✝.WEqualsLocallyBijective AddCommGrpCat
I J : Type u
f : I → J
⊢ freeMap f = (free J).freeHomEquiv.symm (freeSection ∘ f)

Tactic:
;

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J✝ : GrothendieckTopology C
R : Sheaf J✝ RingCat
inst✝¹ : HasWeakSheafify J✝ AddCommGrpCat
inst✝ : J✝.WEqualsLocallyBijective AddCommGrpCat
I J : Type u
f : I → J
⊢ freeMap f = (free J).freeHomEquiv.symm (freeSection ∘ f)
Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Free

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : GrothendieckTopology C
R : Sheaf J RingCat
inst✝¹ : HasWeakSheafify J AddCommGrpCat
inst✝ : J.WEqualsLocallyBijective AddCommGrpCat
I : Type u
M : SheafOfModules R
f : I → M.sections
i : I
⊢ sectionsMap (M.freeHomEquiv.symm f) (freeSection i) = f i

Tactic:
obtain ⟨f, rfl⟩ := (freeHomEquiv M).surjective f
  cat_disch

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
J : GrothendieckTopology C
R₀ : Cᵒᵖ ⥤ RingCat
R : Sheaf J RingCat
α : R₀ ⟶ R.obj
inst✝³ : Presheaf.IsLocallyInjective J α
inst✝² : Presheaf.IsLocallySurjective J α
M₀ : PresheafOfModules R₀
A : Sheaf J AddCommGrpCat
φ : M₀.presheaf ⟶ A.obj
inst✝¹ : Presheaf.IsLocallyInjective J φ
inst✝ : Presheaf.IsLocallySurjective J φ
⊢ Presheaf.IsLocallyInjective J φ

Tactic:
;

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 α
M₀ : PresheafOfModules R₀
A : Sheaf J AddCommGrpCat
φ : M₀.presheaf ⟶ A.obj
inst✝¹ : Presheaf.IsLocallyInjective J φ
inst✝ : Presheaf.IsLocallySurjective J φ
⊢ Presheaf.IsLocallyInjective J φ