mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Homology.LeftResolution.Basic

Goal state before:
pp: A : Type u_1
C : Type u_2
inst✝⁶ : Category.{v_1, u_2} C
inst✝⁵ : Category.{v_2, u_1} A
ι : C ⥤ A
Λ : LeftResolution ι
X Y : A
inst✝⁴ : ι.Full
inst✝³ : ι.Faithful
inst✝² : HasZeroMorphisms C
inst✝¹ : Abelian A
inst✝ : Λ.F.PreservesZeroMorphisms
⊢ Λ.chainComplexMap 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.ExteriorPower.Basic

Goal state before:
pp: R : Type u
inst✝⁶ : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
N' : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup N'
inst✝ : Module R N'
h : ∀ (m : M), (fun x ↦ m) = update (fun x ↦ 0) 0 m
m₁ m₂ : M
⊢ ((ιMulti R 1) fun x ↦ m₁ + m₂) = ((ιMulti R 1) fun x ↦ m₁) + (ιMulti R 1) fun x ↦ m₂

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.ExteriorPower.Basic

Goal state before:
pp: R : Type u
inst✝⁶ : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
N' : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup N'
inst✝ : Module R N'
h : ∀ (m : M), (fun x ↦ m) = update (fun x ↦ 0) 0 m
r : R
m : M
⊢ ((ιMulti R 1) fun x ↦ r • m) = (RingHom.id R) r • (ιMulti R 1) fun x ↦ m

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.ExteriorPower.Basic

Goal state before:
pp: R : Type u
inst✝⁶ : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
N' : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup N'
inst✝ : Module R N'
⊢ M →ₗ[R] ↥(⋀[R]^1 M)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.ExteriorPower.Basic

Goal state before:
pp: R : Type u
inst✝⁶ : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
N' : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup N'
inst✝ : Module R N'
⊢ (alternatingMapLinearEquiv ((AlternatingMap.ofSubsingleton R M M 0) LinearMap.id) ∘ₗ
      have h := ⋯;
      { toFun := fun m ↦ (ιMulti R 1) fun x ↦ m, map_add' := ⋯, map_smul' := ⋯ }) =
    LinearMap.id

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.ExteriorPower.Basic

Goal state before:
pp: R : Type u
inst✝⁶ : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
N' : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup N'
inst✝ : Module R N'
⊢ (have h := ⋯;
      { toFun := fun m ↦ (ιMulti R 1) fun x ↦ m, map_add' := ⋯, map_smul' := ⋯ }) ∘ₗ
      alternatingMapLinearEquiv ((AlternatingMap.ofSubsingleton R M M 0) LinearMap.id) =
    LinearMap.id

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.ExteriorPower.Basic

Goal state before:
pp: R : Type u
inst✝² : CommRing R
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : Fin 1 → M
⊢ (oneEquiv R M) ((ιMulti R 1) f) = f 0

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.ExteriorPower.Basic

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
M : Type u_1
N : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
⊢ ↑(oneEquiv R N) ∘ₗ map 1 f = f ∘ₗ ↑(oneEquiv R M)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.LeftResolution.Basic

Goal state before:
pp: A : Type u_1
C : Type u_2
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Category.{v_2, u_1} A
ι : C ⥤ A
Λ : LeftResolution ι
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
inst✝³ : ι.Full
inst✝² : ι.Faithful
inst✝¹ : HasZeroMorphisms C
inst✝ : Abelian A
⊢ Λ.chainComplexMap (f ≫ g) = Λ.chainComplexMap f ≫ Λ.chainComplexMap g

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
F : J ⥤ PresheafOfModules R
inst✝ : ∀ (X : Cᵒᵖ), Small.{v, max u₂ v} ↑((F ⋙ evaluation R X) ⋙ forget (ModuleCat ↑(R.obj X))).sections
c : Cone F
hc : (X : Cᵒᵖ) → IsLimit ((evaluation R X).mapCone c)
s : Cone F
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ s.pt.map f ≫ (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map ((hc Y).lift ((evaluation R Y).mapCone s)) =
    (hc X).lift ((evaluation R X).mapCone s) ≫ c.pt.map f

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
F : J ⥤ PresheafOfModules R
inst✝ : ∀ (X : Cᵒᵖ), Small.{v, max u₂ v} ↑((F ⋙ evaluation R X) ⋙ forget (ModuleCat ↑(R.obj X))).sections
c : Cone F
hc : (X : Cᵒᵖ) → IsLimit ((evaluation R X).mapCone c)
s : Cone F
j : J
⊢ { app := fun X ↦ (hc X).lift ((evaluation R X).mapCone s), naturality := ⋯ } ≫ c.π.app j = s.π.app j

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
F : J ⥤ PresheafOfModules R
inst✝ : ∀ (X : Cᵒᵖ), Small.{v, max u₂ v} ↑((F ⋙ evaluation R X) ⋙ forget (ModuleCat ↑(R.obj X))).sections
c : Cone F
hc : (X : Cᵒᵖ) → IsLimit ((evaluation R X).mapCone c)
s : Cone F
m : s.pt ⟶ c.pt
hm : ∀ (j : J), m ≫ c.π.app j = s.π.app j
⊢ m = { app := fun X ↦ (hc X).lift ((evaluation R X).mapCone s), naturality := ⋯ }

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
F : J ⥤ PresheafOfModules R
inst✝ : ∀ (X : Cᵒᵖ), Small.{v, max u₂ v} ↑((F ⋙ evaluation R X) ⋙ forget (ModuleCat ↑(R.obj X))).sections
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ HasLimit (F ⋙ evaluation R Y ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f)))

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
F : J ⥤ PresheafOfModules R
inst✝ : ∀ (X : Cᵒᵖ), Small.{v, max u₂ v} ↑((F ⋙ evaluation R X) ⋙ forget (ModuleCat ↑(R.obj X))).sections
X : Cᵒᵖ
⊢ limMap (F.whiskerLeft (restriction R (𝟙 X))) ≫
      (preservesLimitIso (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (𝟙 X)))) (F ⋙ evaluation R X)).inv =
    (ModuleCat.restrictScalarsId' (RingCat.Hom.hom (R.map (𝟙 X))) ⋯).inv.app (limit (F ⋙ evaluation R X))

Tactic:
by

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

Goal state before:
pp: C : Type u'
inst✝ : Category.{v', u'} C
R R' : Cᵒᵖ ⥤ RingCat
M' : PresheafOfModules R'
α : R ⟶ R'
X Y : Cᵒᵖ
f : X ⟶ Y
r : ↑(R.obj X)
x : ↑((ModuleCat.restrictScalars (RingCat.Hom.hom (α.app X))).obj (M'.obj X))
⊢ (ConcreteCategory.hom (R'.map f)) ((ConcreteCategory.hom (α.app X)) r) • (ConcreteCategory.hom (M'.map f)) x =
    (RingHom.id ↑(R.obj X)) r • (ConcreteCategory.hom (M'.map f)) x

Tactic:
by

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

Goal state before:
pp: C : Type u'
inst✝ : Category.{v', u'} C
R R' : Cᵒᵖ ⥤ RingCat
α : R ⟶ R'
X✝ Y✝ : PresheafOfModules R'
φ' : X✝ ⟶ Y✝
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ (X✝.restrictScalarsObj α).map f ≫
      (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map
        ((ModuleCat.restrictScalars (RingCat.Hom.hom (α.app Y))).map (φ'.app Y)) =
    (ModuleCat.restrictScalars (RingCat.Hom.hom (α.app X))).map (φ'.app X) ≫ (Y✝.restrictScalarsObj α).map f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Discrete.StructuredArrow

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
T : Type w
F : C ⥤ Discrete T
t : T
inst✝ : Subsingleton T
X : C
⊢ { as := t } = F.obj X

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Discrete.StructuredArrow

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
T : Type w
F : C ⥤ Discrete T
t : T
inst✝ : Subsingleton T
X : C
⊢ F.obj X = { as := t }

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Final.Connected

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
T : Type w
inst✝ : Unique T
F : C ⥤ Discrete T
⊢ IsConnected C ↔ F.Final

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Final.Connected

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
T : Type w
inst✝ : Unique T
F : C ⥤ Discrete T
⊢ IsConnected C ↔ F.Initial

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Final.Connected

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
T : Type w
inst✝¹ : Unique T
F : C ⥤ Discrete T
inst✝ : IsConnected C
⊢ F.Final

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Final.Connected

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
T : Type w
inst✝¹ : Unique T
F : C ⥤ Discrete T
inst✝ : IsConnected C
⊢ F.Initial

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
F : J ⥤ PresheafOfModules R
inst✝ :
  ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y),
    PreservesColimit (F ⋙ evaluation R Y) (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f)))
c : Cocone F
hc : (X : Cᵒᵖ) → IsColimit ((evaluation R X).mapCocone c)
s : Cocone F
X Y : Cᵒᵖ
f : X ⟶ Y
j : J
⊢ ((evaluation R X).mapCocone c).ι.app j ≫
      c.pt.map f ≫
        (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map ((hc Y).desc ((evaluation R Y).mapCocone s)) =
    ((evaluation R X).mapCocone c).ι.app j ≫ (hc X).desc ((evaluation R X).mapCocone s) ≫ s.pt.map f

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
F : J ⥤ PresheafOfModules R
inst✝ : ∀ (X : Cᵒᵖ), Small.{v, max u₂ v} ↑((F ⋙ evaluation R X) ⋙ forget (ModuleCat ↑(R.obj X))).sections
X Y Z : Cᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
⊢ limMap (F.whiskerLeft (restriction R (f ≫ g))) ≫
      (preservesLimitIso (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (f ≫ g)))) (F ⋙ evaluation R Z)).inv =
    (limMap (F.whiskerLeft (restriction R f)) ≫
        (preservesLimitIso (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))) (F ⋙ evaluation R Y)).inv) ≫
      (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map
          (limMap (F.whiskerLeft (restriction R g)) ≫
            (preservesLimitIso (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map g))) (F ⋙ evaluation R Z)).inv) ≫
        (ModuleCat.restrictScalarsComp' (RingCat.Hom.hom (R.map f)) (RingCat.Hom.hom (R.map g))
                (RingCat.Hom.hom (R.map (f ≫ g))) ⋯).inv.app
          (limit (F ⋙ evaluation R Z))

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
F : J ⥤ PresheafOfModules R
inst✝ :
  ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y),
    PreservesColimit (F ⋙ evaluation R Y) (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f)))
c : Cocone F
hc : (X : Cᵒᵖ) → IsColimit ((evaluation R X).mapCocone c)
s : Cocone F
j : J
⊢ c.ι.app j ≫ { app := fun X ↦ (hc X).desc ((evaluation R X).mapCocone s), naturality := ⋯ } = s.ι.app j

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
F : J ⥤ PresheafOfModules R
inst✝ : ∀ (X : Cᵒᵖ), Small.{v, max u₂ v} ↑((F ⋙ evaluation R X) ⋙ forget (ModuleCat ↑(R.obj X))).sections
j : J
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ (((Functor.const J).obj (limitPresheafOfModules F)).obj j).map f ≫
      (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map (limit.π (F ⋙ evaluation R Y) j) =
    limit.π (F ⋙ evaluation R X) j ≫ (F.obj j).map f

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
F : J ⥤ PresheafOfModules R
inst✝ : ∀ (X : Cᵒᵖ), Small.{v, max u₂ v} ↑((F ⋙ evaluation R X) ⋙ forget (ModuleCat ↑(R.obj X))).sections
j j' : J
f : j ⟶ j'
⊢ ((Functor.const J).obj (limitPresheafOfModules F)).map f ≫
      { app := fun X ↦ limit.π (F ⋙ evaluation R X) j', naturality := ⋯ } =
    { app := fun X ↦ limit.π (F ⋙ evaluation R X) j, naturality := ⋯ } ≫ F.map f

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
F : J ⥤ PresheafOfModules R
inst✝ :
  ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y),
    PreservesColimit (F ⋙ evaluation R Y) (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f)))
c : Cocone F
hc : (X : Cᵒᵖ) → IsColimit ((evaluation R X).mapCocone c)
s : Cocone F
m : c.pt ⟶ s.pt
hm : ∀ (j : J), c.ι.app j ≫ m = s.ι.app j
⊢ m = { app := fun X ↦ (hc X).desc ((evaluation R X).mapCocone s), naturality := ⋯ }

Tactic:
by

Goal state after:
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
⊢ (λ_ ((extendScalars f).obj M)).inv =
    (extendScalars f).map (λ_ M).inv ≫
      (AlgebraTensorModule.distribBaseChange R S ↑(𝟙_ (ModuleCat R)) ↑M).symm.toModuleIso.inv ≫
        (AlgebraTensorModule.rid R S S).symm.toModuleIso.inv ▷ (extendScalars f).obj M

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
J : Type u₂
inst✝² : Category.{v₂, u₂} J
F : J ⥤ PresheafOfModules R
inst✝¹ :
  ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y),
    PreservesColimit (F ⋙ evaluation R Y) (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f)))
inst✝ : ∀ (X : Cᵒᵖ), HasColimit (F ⋙ evaluation R X)
X : Cᵒᵖ
j : J
⊢ colimit.ι (F ⋙ evaluation R X) j ≫
      colimMap (F.whiskerLeft (restriction R (𝟙 X))) ≫
        (preservesColimitIso (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (𝟙 X)))) (F ⋙ evaluation R X)).inv =
    colimit.ι (F ⋙ evaluation R X) j ≫
      (ModuleCat.restrictScalarsId' (RingCat.Hom.hom (R.map (𝟙 X))) ⋯).inv.app (colimit (F ⋙ evaluation R X))

Tactic:
by

Goal state after:
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
⊢ (ρ_ ((extendScalars f).obj M)).inv =
    (extendScalars f).map (ρ_ M).inv ≫
      (AlgebraTensorModule.distribBaseChange R S ↑M ↑(𝟙_ (ModuleCat R))).symm.toModuleIso.inv ≫
        (extendScalars f).obj M ◁ (AlgebraTensorModule.rid R S S).symm.toModuleIso.inv

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Adjunction

Goal state before:
pp: R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
r : R
⊢ (ConcreteCategory.hom (ε (restrictScalars f))) r = f r

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Adjunction

Goal state before:
pp: R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
M₁ M₂ : ModuleCat S
m₁ : ↑M₁
m₂ : ↑M₂
⊢ (ConcreteCategory.hom (μ (restrictScalars f) M₁ M₂)) (m₁ ⊗ₜ[R] m₂) = m₁ ⊗ₜ[S] m₂

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Closed.Cartesian

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
X X' Y Y' Z A B : C
inst✝ : Closed A
I : C
t : IsInitial I
⊢ snd A I = uncurry (t.to (A ⟹ I))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Closed.Cartesian

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
X X' Y Y' Z A B : C
inst✝ : Closed A
I : C
t : IsInitial I
⊢ snd A I ≫ t.to (A ⊗ I) = 𝟙 (A ⊗ I)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Closed.Cartesian

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : CartesianMonoidalCategory C
X X' Y Y' Z A B : C
inst✝² : Closed A
inst✝¹ : BraidedCategory C
I : C
t : IsInitial I
inst✝ : MonoidalClosed C
⊢ default ≫ curry ((mulZero t).hom ≫ t.to B) = 𝟙 (I ⟹ B)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Closed.Cartesian

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
A : C
inst✝ : Closed A
I : C
t : IsInitial I
f : A ⟶ I
⊢ Mono f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Closed.Cartesian

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
A : C
inst✝ : Closed A
I : C
t : IsInitial I
f : A ⟶ I
⊢ IsIso f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Closed.Cartesian

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
I B : C
t : IsInitial I
inst✝ : MonoidalClosed C
Z✝ : C
g h : Z✝ ⟶ I
x✝ : g ≫ t.to B = h ≫ t.to B
⊢ g = h

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory

Goal state before:
pp: J : Type u_1
C : Type u_2
D : Type u_3
E : Type u_4
inst✝⁵ : Category.{v_1, u_1} J
inst✝⁴ : Category.{v_2, u_2} C
inst✝³ : Category.{v_3, u_3} D
inst✝² : Category.{v_4, u_4} E
inst✝¹ : CartesianMonoidalCategory C
inst✝ : CartesianMonoidalCategory E
X Y : J ⥤ C
⊢ { app := fun x ↦ fst (X.obj x) (Y.obj x), naturality := ⋯ } =
    X ◁
        IsTerminal.from
          (evaluationJointlyReflectsLimits (asEmptyCone (𝟙_ (J ⥤ C))) fun x ↦
            isLimitChangeEmptyCone C isTerminalTensorUnit (((evaluation J C).obj x).mapCone (asEmptyCone (𝟙_ (J ⥤ C))))
              (Iso.refl (asEmptyCone (𝟙_ C)).pt))
          Y ≫
      (ρ_ X).hom

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
J : Type u₂
inst✝² : Category.{v₂, u₂} J
F : J ⥤ PresheafOfModules R
inst✝¹ :
  ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y),
    PreservesColimit (F ⋙ evaluation R Y) (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f)))
inst✝ : ∀ (X : Cᵒᵖ), HasColimit (F ⋙ evaluation R X)
X Y Z : Cᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
j : J
⊢ colimit.ι (F ⋙ evaluation R X) j ≫
      colimMap (F.whiskerLeft (restriction R (f ≫ g))) ≫
        (preservesColimitIso (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (f ≫ g)))) (F ⋙ evaluation R Z)).inv =
    colimit.ι (F ⋙ evaluation R X) j ≫
      (colimMap (F.whiskerLeft (restriction R f)) ≫
          (preservesColimitIso (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))) (F ⋙ evaluation R Y)).inv) ≫
        (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map
            (colimMap (F.whiskerLeft (restriction R g)) ≫
              (preservesColimitIso (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map g))) (F ⋙ evaluation R Z)).inv) ≫
          (ModuleCat.restrictScalarsComp' (RingCat.Hom.hom (R.map f)) (RingCat.Hom.hom (R.map g))
                  (RingCat.Hom.hom (R.map (f ≫ g))) ⋯).inv.app
            (colimit (F ⋙ evaluation R Z))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory

Goal state before:
pp: J : Type u_1
C : Type u_2
D : Type u_3
E : Type u_4
inst✝⁵ : Category.{v_1, u_1} J
inst✝⁴ : Category.{v_2, u_2} C
inst✝³ : Category.{v_3, u_3} D
inst✝² : Category.{v_4, u_4} E
inst✝¹ : CartesianMonoidalCategory C
inst✝ : CartesianMonoidalCategory E
X Y : J ⥤ C
⊢ { app := fun x ↦ snd (X.obj x) (Y.obj x), naturality := ⋯ } =
    IsTerminal.from
          (evaluationJointlyReflectsLimits (asEmptyCone (𝟙_ (J ⥤ C))) fun x ↦
            isLimitChangeEmptyCone C isTerminalTensorUnit (((evaluation J C).obj x).mapCone (asEmptyCone (𝟙_ (J ⥤ C))))
              (Iso.refl (asEmptyCone (𝟙_ C)).pt))
          X ▷
        Y ≫
      (λ_ Y).hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory

Goal state before:
pp: J : Type u_1
C : Type u_2
D : Type u_3
E : Type u_4
inst✝⁵ : Category.{v_1, u_1} J
inst✝⁴ : Category.{v_2, u_2} C
inst✝³ : Category.{v_3, u_3} D
inst✝² : Category.{v_4, u_4} E
inst✝¹ : CartesianMonoidalCategory C
inst✝ : CartesianMonoidalCategory E
X Y : J ⥤ C
j : J
⊢ (pair X Y ⋙ (evaluation J C).obj j).obj { as := WalkingPair.left } ≅
    (pair (X.obj j) (Y.obj j)).obj { as := WalkingPair.left }

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory

Goal state before:
pp: J : Type u_1
C : Type u_2
D : Type u_3
E : Type u_4
inst✝⁵ : Category.{v_1, u_1} J
inst✝⁴ : Category.{v_2, u_2} C
inst✝³ : Category.{v_3, u_3} D
inst✝² : Category.{v_4, u_4} E
inst✝¹ : CartesianMonoidalCategory C
inst✝ : CartesianMonoidalCategory E
X Y : J ⥤ C
j : J
⊢ (pair X Y ⋙ (evaluation J C).obj j).obj { as := WalkingPair.right } ≅
    (pair (X.obj j) (Y.obj j)).obj { as := WalkingPair.right }

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
J : Type u₂
inst✝² : Category.{v₂, u₂} J
F : J ⥤ PresheafOfModules R
inst✝¹ :
  ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y),
    PreservesColimit (F ⋙ evaluation R Y) (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f)))
inst✝ : ∀ (X : Cᵒᵖ), HasColimit (F ⋙ evaluation R X)
j : J
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ (F.obj j).map f ≫ (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map (colimit.ι (F ⋙ evaluation R Y) j) =
    colimit.ι (F ⋙ evaluation R X) j ≫ (((Functor.const J).obj (colimitPresheafOfModules F)).obj j).map f

Tactic:
by

Goal state after:
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 F' G' : C ⥤ D
α : F ⟶ G
β : F' ⟶ G'
X Y : C
f : X ⟶ Y
⊢ (tensorObj F F').map f ≫ (α.app Y ⊗ₘ β.app Y) = (α.app X ⊗ₘ β.app X) ≫ (tensorObj G G').map f

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
J : Type u₂
inst✝² : Category.{v₂, u₂} J
F : J ⥤ PresheafOfModules R
inst✝¹ :
  ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y),
    PreservesColimit (F ⋙ evaluation R Y) (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f)))
inst✝ : ∀ (X : Cᵒᵖ), HasColimit (F ⋙ evaluation R X)
X Y : J
f : X ⟶ Y
⊢ F.map f ≫ { app := fun X ↦ colimit.ι (F ⋙ evaluation R X) Y, naturality := ⋯ } =
    { app := fun X_1 ↦ colimit.ι (F ⋙ evaluation R X_1) X, naturality := ⋯ } ≫
      ((Functor.const J).obj (colimitPresheafOfModules F)).map f

Tactic:
by

Goal state after:
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 F' G' : C ⥤ D
α : F✝ ⟶ G
β✝ : F' ⟶ G'
F : C ⥤ D
β : F' ⟶ G'
X Y : C
f : X ⟶ Y
⊢ (tensorObj F F').map f ≫ F.obj Y ◁ β.app Y = F.obj X ◁ β.app X ≫ (tensorObj F G').map f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory

Goal state before:
pp: J : Type u_1
C : Type u_2
D : Type u_3
E : Type u_4
inst✝⁵ : Category.{v_1, u_1} J
inst✝⁴ : Category.{v_2, u_2} C
inst✝³ : Category.{v_3, u_3} D
inst✝² : Category.{v_4, u_4} E
inst✝¹ : CartesianMonoidalCategory C
inst✝ : CartesianMonoidalCategory E
X Y : J ⥤ C
j : J
⊢ ∀ (j_1 : Discrete WalkingPair),
    (BinaryFan.mk (fst (X.obj j) (Y.obj j)) (snd (X.obj j) (Y.obj j))).π.app j_1 =
      (Iso.refl (BinaryFan.mk (fst (X.obj j) (Y.obj j)) (snd (X.obj j) (Y.obj j))).pt).hom ≫
        ((Cone.postcompose
                    (mapPairIso (Iso.refl ((pair X Y ⋙ (evaluation J C).obj j).obj { as := WalkingPair.left }))
                        (Iso.refl ((pair X Y ⋙ (evaluation J C).obj j).obj { as := WalkingPair.right }))).hom).obj
                (((evaluation J C).obj j).mapCone
                  (BinaryFan.mk { app := fun x ↦ fst (X.obj x) (Y.obj x), naturality := ⋯ }
                    { app := fun x ↦ snd (X.obj x) (Y.obj x), naturality := ⋯ }))).π.app
          j_1

Tactic:
by

Goal state after: