mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete

Goal state before:
pp: B : Type u_1
C : Type u_2
inst✝² : Bicategory B
inst✝¹ : IsLocallyDiscrete B
inst✝ : Bicategory C
obj : B → C
map : {b b' : B} → (b ⟶ b') → (obj b ⟶ obj b')
mapId : (b : B) → map (𝟙 b) ⟶ 𝟙 (obj b)
mapComp : {b₀ b₁ b₂ : B} → (f : b₀ ⟶ b₁) → (g : b₁ ⟶ b₂) → map (f ≫ g) ⟶ map f ≫ map g
map₂_associator :
  autoParam
    (∀ {b₀ b₁ b₂ b₃ : B} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (h : b₂ ⟶ b₃),
      eqToHom ⋯ ≫ mapComp f (g ≫ h) ≫ map f ◁ mapComp g h =
        mapComp (f ≫ g) h ≫ mapComp f g ▷ map h ≫ (α_ (map f) (map g) (map h)).hom)
    oplaxFunctorOfIsLocallyDiscrete._auto_1
b₀ b₁ : B
f : b₀ ⟶ b₁
⊢ map (𝟙 b₀ ≫ f) = map f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete

Goal state before:
pp: B : Type u_1
C : Type u_2
inst✝² : Bicategory B
inst✝¹ : IsLocallyDiscrete B
inst✝ : Bicategory C
obj : B → C
map : {b b' : B} → (b ⟶ b') → (obj b ⟶ obj b')
mapId : (b : B) → map (𝟙 b) ⟶ 𝟙 (obj b)
mapComp : {b₀ b₁ b₂ : B} → (f : b₀ ⟶ b₁) → (g : b₁ ⟶ b₂) → map (f ≫ g) ⟶ map f ≫ map g
map₂_associator :
  autoParam
    (∀ {b₀ b₁ b₂ b₃ : B} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (h : b₂ ⟶ b₃),
      eqToHom ⋯ ≫ mapComp f (g ≫ h) ≫ map f ◁ mapComp g h =
        mapComp (f ≫ g) h ≫ mapComp f g ▷ map h ≫ (α_ (map f) (map g) (map h)).hom)
    oplaxFunctorOfIsLocallyDiscrete._auto_1
map₂_left_unitor :
  autoParam (∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁), mapComp (𝟙 b₀) f ≫ mapId b₀ ▷ map f ≫ (λ_ (map f)).hom = eqToHom ⋯)
    oplaxFunctorOfIsLocallyDiscrete._auto_3
b₀ b₁ : B
f : b₀ ⟶ b₁
⊢ map (f ≫ 𝟙 b₁) = map f

Tactic:
by

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 φ
X : Cᵒᵖ
m : ↑(A.obj.obj X)
Y : C
f : Y ⟶ Opposite.unop X
m₀ : ToType (M₀.presheaf.obj (Opposite.op Y))
hm₀ : (ConcreteCategory.hom (φ.app (Opposite.op Y))) m₀ = (ConcreteCategory.hom (A.obj.map f.op)) m
⊢ (ConcreteCategory.hom (α.app (Opposite.op Y))) 0 = (ConcreteCategory.hom (R.obj.map f.op)) 0

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete

Goal state before:
pp: B : Type u_1
C : Type u_2
inst✝² : Bicategory B
inst✝¹ : IsLocallyDiscrete B
inst✝ : Bicategory C
obj : B → C
map : {b b' : B} → (b ⟶ b') → (obj b ⟶ obj b')
mapId : (b : B) → map (𝟙 b) ⟶ 𝟙 (obj b)
mapComp : {b₀ b₁ b₂ : B} → (f : b₀ ⟶ b₁) → (g : b₁ ⟶ b₂) → map (f ≫ g) ⟶ map f ≫ map g
map₂_associator :
  ∀ {b₀ b₁ b₂ b₃ : B} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (h : b₂ ⟶ b₃),
    eqToHom ⋯ ≫ mapComp f (g ≫ h) ≫ map f ◁ mapComp g h =
      mapComp (f ≫ g) h ≫ mapComp f g ▷ map h ≫ (α_ (map f) (map g) (map h)).hom
map₂_left_unitor : ∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁), mapComp (𝟙 b₀) f ≫ mapId b₀ ▷ map f ≫ (λ_ (map f)).hom = eqToHom ⋯
map₂_right_unitor : ∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁), mapComp f (𝟙 b₁) ≫ map f ◁ mapId b₁ ≫ (ρ_ (map f)).hom = eqToHom ⋯
a✝ b✝ : B
f✝ g✝ : a✝ ⟶ b✝
φ : f✝ ⟶ g✝
⊢ map f✝ = map g✝

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete

Goal state before:
pp: B : Type u_1
C : Type u_2
inst✝² : Bicategory B
inst✝¹ : IsLocallyDiscrete B
inst✝ : Bicategory C
obj : B → C
map : {b b' : B} → (b ⟶ b') → (obj b ⟶ obj b')
mapId : (b : B) → map (𝟙 b) ⟶ 𝟙 (obj b)
mapComp : {b₀ b₁ b₂ : B} → (f : b₀ ⟶ b₁) → (g : b₁ ⟶ b₂) → map (f ≫ g) ⟶ map f ≫ map g
map₂_associator :
  ∀ {b₀ b₁ b₂ b₃ : B} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (h : b₂ ⟶ b₃),
    eqToHom ⋯ ≫ mapComp f (g ≫ h) ≫ map f ◁ mapComp g h =
      mapComp (f ≫ g) h ≫ mapComp f g ▷ map h ≫ (α_ (map f) (map g) (map h)).hom
map₂_left_unitor : ∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁), mapComp (𝟙 b₀) f ≫ mapId b₀ ▷ map f ≫ (λ_ (map f)).hom = eqToHom ⋯
map₂_right_unitor : ∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁), mapComp f (𝟙 b₁) ≫ map f ◁ mapId b₁ ≫ (ρ_ (map f)).hom = eqToHom ⋯
a✝ b✝ c✝ : B
f✝ f'✝ : a✝ ⟶ b✝
η : f✝ ⟶ f'✝
⊢ ∀ (g : b✝ ⟶ c✝), eqToHom ⋯ ≫ mapComp f'✝ g = mapComp f✝ g ≫ eqToHom ⋯ ▷ map g

Tactic:
by

Goal state after:
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
s : Cofork (Sigma.map' f fun x ↦ 𝟙 R) 0
⊢ (Cofork.π (sigmaConstCokernelCofork R f) ≫
      Sigma.desc fun x ↦
        match x with
        | ⟨b, property⟩ => Sigma.ι (fun x ↦ R) b ≫ s.π) =
    s.π

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete

Goal state before:
pp: B : Type u_1
C : Type u_2
inst✝² : Bicategory B
inst✝¹ : IsLocallyDiscrete B
inst✝ : Bicategory C
obj : B → C
map : {b b' : B} → (b ⟶ b') → (obj b ⟶ obj b')
mapId : (b : B) → map (𝟙 b) ⟶ 𝟙 (obj b)
mapComp : {b₀ b₁ b₂ : B} → (f : b₀ ⟶ b₁) → (g : b₁ ⟶ b₂) → map (f ≫ g) ⟶ map f ≫ map g
map₂_associator :
  ∀ {b₀ b₁ b₂ b₃ : B} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (h : b₂ ⟶ b₃),
    eqToHom ⋯ ≫ mapComp f (g ≫ h) ≫ map f ◁ mapComp g h =
      mapComp (f ≫ g) h ≫ mapComp f g ▷ map h ≫ (α_ (map f) (map g) (map h)).hom
map₂_left_unitor : ∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁), mapComp (𝟙 b₀) f ≫ mapId b₀ ▷ map f ≫ (λ_ (map f)).hom = eqToHom ⋯
map₂_right_unitor : ∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁), mapComp f (𝟙 b₁) ≫ map f ◁ mapId b₁ ≫ (ρ_ (map f)).hom = eqToHom ⋯
a✝ b✝ c✝ : B
x✝² : a✝ ⟶ b✝
x✝¹ x✝ : b✝ ⟶ c✝
η : x✝¹ ⟶ x✝
⊢ eqToHom ⋯ ≫ mapComp x✝² x✝ = mapComp x✝² x✝¹ ≫ map x✝² ◁ eqToHom ⋯

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete

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
x✝ : LocallyDiscrete C
X : C
⊢ (match 𝟙 { as := X } with
    | { as := f } => (F.map f).toLoc) =
    𝟙
      (match { as := X } with
      | { as := X } => { as := F.obj X })

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete

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
b₀✝ b₁✝ b₂✝ : LocallyDiscrete C
x✝¹ : b₀✝ ⟶ b₁✝
x✝ : b₁✝ ⟶ b₂✝
f : b₀✝.as ⟶ b₁✝.as
g : b₁✝.as ⟶ b₂✝.as
⊢ (match { as := f } ≫ { as := g } with
    | { as := f } => (F.map f).toLoc) =
    (match { as := f } with
      | { as := f } => (F.map f).toLoc) ≫
      match { as := g } with
      | { as := f } => (F.map f).toLoc

Tactic:
by

Goal state after:
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
x✝ : LocallyDiscrete I
X : I
⊢ (match 𝟙 { as := X } with
    | { as := f } => F.map f) =
    𝟙
      (match { as := X } with
      | { as := X } => F.obj X)

Tactic:
by

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 φ
X : Cᵒᵖ
m : ↑(A.obj.obj X)
⊢ smul α φ 0 m = 0

Tactic:
by

Goal state after:
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₀✝ ⟶ b₁✝
g : b₁✝ ⟶ b₂✝
⊢ (match f ≫ g with
    | { as := f } => F.map f) =
    (match f with
      | { as := f } => F.map f) ≫
      match g with
      | { as := f } => F.map f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete

Goal state before:
pp: B₀ : Type u_1
C : Type u_2
inst✝¹ : Category.{v_1, u_1} B₀
inst✝ : Bicategory C
obj : B₀ → C
map : {b b' : B₀} → (b ⟶ b') → (obj b ⟶ obj b')
mapId : (b : B₀) → map (𝟙 b) ≅ 𝟙 (obj b)
mapComp : {b₀ b₁ b₂ : B₀} → (f : b₀ ⟶ b₁) → (g : b₁ ⟶ b₂) → map (f ≫ g) ≅ map f ≫ map g
b₀ b₁ b₂ b₃ : B₀
f : b₀ ⟶ b₁
g : b₁ ⟶ b₂
h : b₂ ⟶ b₃
⊢ map ((f ≫ g) ≫ h) = map (f ≫ g ≫ h)

Tactic:
by

Goal state after:
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
s : Cofork (Sigma.map' f fun x ↦ 𝟙 R) 0
m : (sigmaConstCokernelCofork R f).pt ⟶ s.pt
hm : Cofork.π (sigmaConstCokernelCofork R f) ≫ m = s.π
⊢ m =
    Sigma.desc fun x ↦
      match x with
      | ⟨b, property⟩ => Sigma.ι (fun x ↦ R) b ≫ s.π

Tactic:
by

Goal state after:
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 ((sigmaConst.obj R).map f)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete

Goal state before:
pp: B₀ : Type u_1
C : Type u_2
inst✝¹ : Category.{v_1, u_1} B₀
inst✝ : Bicategory C
obj : B₀ → C
map : {b b' : B₀} → (b ⟶ b') → (obj b ⟶ obj b')
mapId : (b : B₀) → map (𝟙 b) ≅ 𝟙 (obj b)
mapComp : {b₀ b₁ b₂ : B₀} → (f : b₀ ⟶ b₁) → (g : b₁ ⟶ b₂) → map (f ≫ g) ≅ map f ≫ map g
map₂_associator :
  autoParam
    (∀ {b₀ b₁ b₂ b₃ : B₀} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (h : b₂ ⟶ b₃),
      (mapComp (f ≫ g) h).hom ≫
          (mapComp f g).hom ▷ map h ≫
            (α_ (map f) (map g) (map h)).hom ≫ map f ◁ (mapComp g h).inv ≫ (mapComp f (g ≫ h)).inv =
        eqToHom ⋯)
    mkPseudofunctor._auto_1
b₀ b₁ : B₀
f : b₀ ⟶ b₁
⊢ map (𝟙 b₀ ≫ f) = map f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete

Goal state before:
pp: B₀ : Type u_1
C : Type u_2
inst✝¹ : Category.{v_1, u_1} B₀
inst✝ : Bicategory C
obj : B₀ → C
map : {b b' : B₀} → (b ⟶ b') → (obj b ⟶ obj b')
mapId : (b : B₀) → map (𝟙 b) ≅ 𝟙 (obj b)
mapComp : {b₀ b₁ b₂ : B₀} → (f : b₀ ⟶ b₁) → (g : b₁ ⟶ b₂) → map (f ≫ g) ≅ map f ≫ map g
map₂_associator :
  autoParam
    (∀ {b₀ b₁ b₂ b₃ : B₀} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (h : b₂ ⟶ b₃),
      (mapComp (f ≫ g) h).hom ≫
          (mapComp f g).hom ▷ map h ≫
            (α_ (map f) (map g) (map h)).hom ≫ map f ◁ (mapComp g h).inv ≫ (mapComp f (g ≫ h)).inv =
        eqToHom ⋯)
    mkPseudofunctor._auto_1
map₂_left_unitor :
  autoParam
    (∀ {b₀ b₁ : B₀} (f : b₀ ⟶ b₁), (mapComp (𝟙 b₀) f).hom ≫ (mapId b₀).hom ▷ map f ≫ (λ_ (map f)).hom = eqToHom ⋯)
    mkPseudofunctor._auto_3
b₀ b₁ : B₀
f : b₀ ⟶ b₁
⊢ map (f ≫ 𝟙 b₁) = map f

Tactic:
by

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 φ
X : Cᵒᵖ
r : ↑(R.obj.obj X)
Y : C
f : Y ⟶ Opposite.unop X
r₀ : ToType (R₀.obj (Opposite.op Y))
hr₀ : (ConcreteCategory.hom (α.app (Opposite.op Y))) r₀ = (ConcreteCategory.hom (R.obj.map f.op)) r
⊢ (ConcreteCategory.hom (φ.app (Opposite.op Y))) 0 = (ConcreteCategory.hom (A.obj.map f.op)) 0

Tactic:
by

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

Goal state before:
pp: J : Type u₁
inst✝ : Fintype J
j : Bicone J
⊢ j ∈ [Bicone.left, Bicone.right].toFinset ∪ Finset.image Bicone.diagram Fintype.elems

Tactic:
by

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

Goal state before:
pp: J : Type u₁
inst✝ : Category.{v₁, u₁} J
j k : Bicone J
f g : BiconeHom J j k
⊢ Decidable (f = g)

Tactic:
by

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 φ
X : Cᵒᵖ
r : ↑(R.obj.obj X)
⊢ smul α φ r 0 = 0

Tactic:
by

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

Goal state before:
pp: J : Type u₁
inst✝ : Category.{v₁, u₁} J
X✝ Y✝ Z✝ : Bicone J
f : BiconeHom J X✝ Y✝
g : BiconeHom J Y✝ Z✝
⊢ BiconeHom J X✝ Z✝

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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 φ
X : Cᵒᵖ
r : ↑(R.obj.obj X)
m m' : ↑(A.obj.obj X)
S : Sieve (Opposite.unop X) := Presheaf.imageSieve α r ⊓ Presheaf.imageSieve φ m ⊓ Presheaf.imageSieve φ m'
⊢ S ∈ J (Opposite.unop X)

Tactic:
by

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

Goal state before:
pp: J : Type u₁
inst✝ : Category.{v₁, u₁} J
W✝ X✝ Y✝ Z✝ : Bicone J
f : W✝ ⟶ X✝
g : X✝ ⟶ Y✝
h : Y✝ ⟶ Z✝
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h

Tactic:
by

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

Goal state before:
pp: J : Type v₁
inst✝¹ : SmallCategory J
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : J ⥤ C
c₁ c₂ : Cone F
X✝ Y✝ : Bicone J
f : X✝ ⟶ Y✝
⊢ (Bicone.casesOn X✝ c₁.pt c₂.pt fun j ↦ F.obj j) ⟶ Bicone.casesOn Y✝ c₁.pt c₂.pt fun j ↦ F.obj j

Tactic:
by

Goal state after:
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
s : free I ⟶ M
i : I
⊢ (freeCofan I).inj i ≫
      (fun s ↦ Cofan.IsColimit.desc (isColimitFreeCofan I) fun i ↦ M.unitHomEquiv.symm (s i))
        ((fun f i ↦ M.unitHomEquiv (ιFree i ≫ f)) s) =
    (freeCofan I).inj i ≫ s

Tactic:
by

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 φ
X : Cᵒᵖ
r : ↑(R.obj.obj X)
m m' : ↑(A.obj.obj X)
S : Sieve (Opposite.unop X) := Presheaf.imageSieve α r ⊓ Presheaf.imageSieve φ m ⊓ Presheaf.imageSieve φ m'
hS : S ∈ J (Opposite.unop X)
Y : C
f : Y ⟶ Opposite.unop X
r₀ : ToType (R₀.obj (Opposite.op Y))
hr₀ : (ConcreteCategory.hom (α.app (Opposite.op Y))) r₀ = (ConcreteCategory.hom (R.obj.map f.op)) r
m₀ : ↑(M₀.obj (Opposite.op Y))
hm₀ : (ConcreteCategory.hom (φ.app (Opposite.op Y))) m₀ = (ConcreteCategory.hom (A.obj.map f.op)) m
m₀' : ↑(M₀.obj (Opposite.op Y))
hm₀' : (ConcreteCategory.hom (φ.app (Opposite.op Y))) m₀' = (ConcreteCategory.hom (A.obj.map f.op)) m'
⊢ (ConcreteCategory.hom (φ.app (Opposite.op Y))) (m₀ + m₀') = (ConcreteCategory.hom (A.obj.map f.op)) (m + m')

Tactic:
by

Goal state after:
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
⊢ (fun f i ↦ M.unitHomEquiv (ιFree i ≫ f))
      ((fun s ↦ Cofan.IsColimit.desc (isColimitFreeCofan I) fun i ↦ M.unitHomEquiv.symm (s i)) f) =
    f

Tactic:
by

Goal state after:
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
⊢ N.freeHomEquiv (M.freeHomEquiv.symm s ≫ p) = N.freeHomEquiv (N.freeHomEquiv.symm fun i ↦ sectionsMap p (s i))

Tactic:
by

Goal state after:
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 : free I ⟶ M
i : I
⊢ M.unitHomEquiv.symm (M.freeHomEquiv f i) = ιFree i ≫ f

Tactic:
by

Goal state after:
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
⊢ (free J).freeHomEquiv.symm ((free J).freeHomEquiv (freeMap f)) = (free J).freeHomEquiv.symm (freeSection ∘ f)

Tactic:
by

Goal state after:
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
i : I
⊢ sectionsMap (freeMap f) (freeSection i) = freeSection (f i)

Tactic:
by

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

Goal state after:
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
i : I
⊢ ιFree i ≫ freeMap f = ιFree (f i)

Tactic:
by

Goal state after:
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
⊢ coprod.inl ≫ (freeSumIso I J).hom = freeMap Sum.inl

Tactic:
by

Goal state after:
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
⊢ coprod.inr ≫ (freeSumIso I J).hom = freeMap Sum.inr

Tactic:
by

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 φ
X : Cᵒᵖ
r : ↑(R.obj.obj X)
m m' : ↑(A.obj.obj X)
⊢ smul α φ r (m + m') = smul α φ r m + smul α φ r m'

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : PreservesFiniteCoproducts F
n : ℕ
⊢ PreservesLimitsOfShape (Discrete (Fin n)) F.op

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ Dᵒᵖ
inst✝ : PreservesFiniteCoproducts F
x✝ : ℕ
⊢ PreservesLimitsOfShape (Discrete (Fin x✝)) F.leftOp

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : Cᵒᵖ ⥤ D
inst✝ : PreservesFiniteCoproducts F
x✝ : ℕ
⊢ PreservesLimitsOfShape (Discrete (Fin x✝)) F.rightOp

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : Cᵒᵖ ⥤ Dᵒᵖ
inst✝ : PreservesFiniteCoproducts F
x✝ : ℕ
⊢ PreservesLimitsOfShape (Discrete (Fin x✝)) F.unop

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : PreservesFiniteProducts F
x✝ : ℕ
⊢ PreservesColimitsOfShape (Discrete (Fin x✝)) F.op

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ Dᵒᵖ
inst✝ : PreservesFiniteProducts F
x✝ : ℕ
⊢ PreservesColimitsOfShape (Discrete (Fin x✝)) F.leftOp

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : Cᵒᵖ ⥤ D
inst✝ : PreservesFiniteProducts F
x✝ : ℕ
⊢ PreservesColimitsOfShape (Discrete (Fin x✝)) F.rightOp

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : Cᵒᵖ ⥤ Dᵒᵖ
inst✝ : PreservesFiniteProducts F
x✝ : ℕ
⊢ PreservesColimitsOfShape (Discrete (Fin x✝)) F.unop

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : ReflectsFiniteCoproducts F
n : ℕ
⊢ ReflectsLimitsOfShape (Discrete (Fin n)) F.op

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ Dᵒᵖ
inst✝ : ReflectsFiniteCoproducts F
x✝ : ℕ
⊢ ReflectsLimitsOfShape (Discrete (Fin x✝)) F.leftOp

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : Cᵒᵖ ⥤ D
inst✝ : ReflectsFiniteCoproducts F
x✝ : ℕ
⊢ ReflectsLimitsOfShape (Discrete (Fin x✝)) F.rightOp

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : Cᵒᵖ ⥤ Dᵒᵖ
inst✝ : ReflectsFiniteCoproducts F
x✝ : ℕ
⊢ ReflectsLimitsOfShape (Discrete (Fin x✝)) F.unop

Tactic:
by

Goal state after: