mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Shift.Adjunction

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝³ : AddGroup A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
a : A
inst✝ : F.CommShift A
Y : D
h : -a + a = 0
⊢ (iso adj a).inv.app Y =
    adj.unit.app ((shiftFunctor C a).obj (G.obj Y)) ≫
      G.map ((shiftFunctorCompIsoId D (-a) a h).inv.app (F.obj ((shiftFunctor C a).obj (G.obj Y)))) ≫
        G.map ((shiftFunctor D a).map ((shiftFunctor D (-a)).map ((Functor.commShiftIso F a).hom.app (G.obj Y)))) ≫
          G.map ((shiftFunctor D a).map ((shiftFunctorCompIsoId D a (-a) ⋯).hom.app (F.obj (G.obj Y)))) ≫
            G.map ((shiftFunctor D a).map (adj.counit.app Y))

Tactic:
simp only [iso, iso', shiftEquiv', Equiv.toFun_as_coe, conjugateIsoEquiv_apply_inv,
    conjugateEquiv_apply_app, Functor.comp_obj, comp_unit_app, Functor.id_obj,
    Equivalence.toAdjunction_unit, Equivalence.Equivalence_mk'_unit, Iso.symm_hom, Functor.comp_map,
    comp_counit_app, Equivalence.toAdjunction_counit, Equivalence.Equivalence_mk'_counit,
    Functor.map_shiftFunctorCompIsoId_hom_app, assoc, Functor.map_comp]

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝³ : AddGroup A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
a : A
inst✝ : F.CommShift A
Y : D
h : -a + a = 0
⊢ adj.unit.app ((shiftFunctor C a).obj (G.obj Y)) ≫
      G.map ((shiftFunctorCompIsoId D (-a) a ⋯).inv.app (F.obj ((shiftFunctor C a).obj (G.obj Y)))) ≫
        G.map ((shiftFunctor D a).map ((Functor.commShiftIso F (-a)).inv.app ((shiftFunctor C a).obj (G.obj Y)))) ≫
          G.map ((shiftFunctor D a).map ((Functor.commShiftIso F (-a)).hom.app ((shiftFunctor C a).obj (G.obj Y)))) ≫
            G.map ((shiftFunctor D a).map ((shiftFunctor D (-a)).map ((Functor.commShiftIso F a).hom.app (G.obj Y)))) ≫
              G.map ((shiftFunctor D a).map ((shiftFunctorCompIsoId D a (-a) ⋯).hom.app (F.obj (G.obj Y)))) ≫
                G.map ((shiftFunctor D a).map (adj.counit.app Y)) =
    adj.unit.app ((shiftFunctor C a).obj (G.obj Y)) ≫
      G.map ((shiftFunctorCompIsoId D (-a) a h).inv.app (F.obj ((shiftFunctor C a).obj (G.obj Y)))) ≫
        G.map ((shiftFunctor D a).map ((shiftFunctor D (-a)).map ((Functor.commShiftIso F a).hom.app (G.obj Y)))) ≫
          G.map ((shiftFunctor D a).map ((shiftFunctorCompIsoId D a (-a) ⋯).hom.app (F.obj (G.obj Y)))) ≫
            G.map ((shiftFunctor D a).map (adj.counit.app Y))
Module: Mathlib.CategoryTheory.Shift.ShiftedHomOpposite

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasShift C ℤ
X Y : C
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
n a : ℤ
x y : Opposite.op ((shiftFunctor C a).obj Y) ⟶ (shiftFunctor Cᵒᵖ n).obj (Opposite.op X)
a' : ℤ
h : n + a = a'
⊢ (opEquiv n).symm (x + y) ≫ (shiftFunctorAdd' C a n a' ⋯).inv.app Y =
    (opEquiv n).symm x ≫ (shiftFunctorAdd' C a n a' ⋯).inv.app Y +
      (opEquiv n).symm y ≫ (shiftFunctorAdd' C a n a' ⋯).inv.app Y

Tactic:
opEquiv_symm_add,

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasShift C ℤ
X Y : C
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
n a : ℤ
x y : Opposite.op ((shiftFunctor C a).obj Y) ⟶ (shiftFunctor Cᵒᵖ n).obj (Opposite.op X)
a' : ℤ
h : n + a = a'
⊢ ((opEquiv n).symm x + (opEquiv n).symm y) ≫ (shiftFunctorAdd' C a n a' ⋯).inv.app Y =
    (opEquiv n).symm x ≫ (shiftFunctorAdd' C a n a' ⋯).inv.app Y +
      (opEquiv n).symm y ≫ (shiftFunctorAdd' C a n a' ⋯).inv.app Y
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Triangle

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
T₁ T₂ : (Triangle C)ᵒᵖ
f : T₁ ⟶ T₂
⊢ ((𝟭 (Triangle C)ᵒᵖ).map f ≫
        ((Triangle.mk ((functor C).obj T₂).mor₂.unop ((functor C).obj T₂).mor₁.unop
                  (((opShiftFunctorEquivalence C 1).unitIso.inv.app ((functor C).obj T₂).obj₁).unop ≫
                    (shiftFunctor C 1).map ((functor C).obj T₂).mor₃.unop)).isoMk
              (Opposite.unop T₂)
              (Iso.refl
                (Triangle.mk ((functor C).obj T₂).mor₂.unop ((functor C).obj T₂).mor₁.unop
                    (((opShiftFunctorEquivalence C 1).unitIso.inv.app ((functor C).obj T₂).obj₁).unop ≫
                      (shiftFunctor C 1).map ((functor C).obj T₂).mor₃.unop)).obj₁)
              (Iso.refl
                (Triangle.mk ((functor C).obj T₂).mor₂.unop ((functor C).obj T₂).mor₁.unop
                    (((opShiftFunctorEquivalence C 1).unitIso.inv.app ((functor C).obj T₂).obj₁).unop ≫
                      (shiftFunctor C 1).map ((functor C).obj T₂).mor₃.unop)).obj₂)
              (Iso.refl
                (Triangle.mk ((functor C).obj T₂).mor₂.unop ((functor C).obj T₂).mor₁.unop
                    (((opShiftFunctorEquivalence C 1).unitIso.inv.app ((functor C).obj T₂).obj₁).unop ≫
                      (shiftFunctor C 1).map ((functor C).obj T₂).mor₃.unop)).obj₃)
              ⋯ ⋯ ⋯).op.hom).unop =
    (((Triangle.mk ((functor C).obj T₁).mor₂.unop ((functor C).obj T₁).mor₁.unop
                  (((opShiftFunctorEquivalence C 1).unitIso.inv.app ((functor C).obj T₁).obj₁).unop ≫
                    (shiftFunctor C 1).map ((functor C).obj T₁).mor₃.unop)).isoMk
              (Opposite.unop T₁)
              (Iso.refl
                (Triangle.mk ((functor C).obj T₁).mor₂.unop ((functor C).obj T₁).mor₁.unop
                    (((opShiftFunctorEquivalence C 1).unitIso.inv.app ((functor C).obj T₁).obj₁).unop ≫
                      (shiftFunctor C 1).map ((functor C).obj T₁).mor₃.unop)).obj₁)
              (Iso.refl
                (Triangle.mk ((functor C).obj T₁).mor₂.unop ((functor C).obj T₁).mor₁.unop
                    (((opShiftFunctorEquivalence C 1).unitIso.inv.app ((functor C).obj T₁).obj₁).unop ≫
                      (shiftFunctor C 1).map ((functor C).obj T₁).mor₃.unop)).obj₂)
              (Iso.refl
                (Triangle.mk ((functor C).obj T₁).mor₂.unop ((functor C).obj T₁).mor₁.unop
                    (((opShiftFunctorEquivalence C 1).unitIso.inv.app ((functor C).obj T₁).obj₁).unop ≫
                      (shiftFunctor C 1).map ((functor C).obj T₁).mor₃.unop)).obj₃)
              ⋯ ⋯ ⋯).op.hom ≫
        (functor C ⋙ inverse C).map f).unop

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Triangle

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
⊢ ∀ {X Y : Triangle Cᵒᵖ} (f : X ⟶ Y),
    (inverse C ⋙ functor C).map f ≫
        (((inverse C ⋙ functor C).obj Y).isoMk ((𝟭 (Triangle Cᵒᵖ)).obj Y)
            (Iso.refl ((inverse C ⋙ functor C).obj Y).obj₁) (Iso.refl ((inverse C ⋙ functor C).obj Y).obj₂)
            (Iso.refl ((inverse C ⋙ functor C).obj Y).obj₃) ⋯ ⋯ ⋯).hom =
      (((inverse C ⋙ functor C).obj X).isoMk ((𝟭 (Triangle Cᵒᵖ)).obj X) (Iso.refl ((inverse C ⋙ functor C).obj X).obj₁)
            (Iso.refl ((inverse C ⋙ functor C).obj X).obj₂) (Iso.refl ((inverse C ⋙ functor C).obj X).obj₃) ⋯ ⋯ ⋯).hom ≫
        (𝟭 (Triangle Cᵒᵖ)).map f

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Center.Linear

Goal state before:
pp: R : Type w
inst✝³ : Ring R
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : Linear R C
⊢ { app := fun X ↦ 1 • 𝟙 X, naturality := ⋯ } = 1

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Center.Linear

Goal state before:
pp: R : Type w
inst✝³ : Ring R
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : Linear R C
a b : R
X : C
⊢ CatCenter.app { app := fun X ↦ (a * b) • 𝟙 X, naturality := ⋯ } X =
    CatCenter.app { app := fun X ↦ a • 𝟙 X, naturality := ⋯ } X ≫
      CatCenter.app { app := fun X ↦ b • 𝟙 X, naturality := ⋯ } X

Tactic:
rw [Linear.smul_comp, Linear.comp_smul, smul_smul]

Goal state after:
R : Type w
inst✝³ : Ring R
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : Linear R C
a b : R
X : C
⊢ CatCenter.app { app := fun X ↦ (a * b) • 𝟙 X, naturality := ⋯ } X = (a * b) • 𝟙 X ≫ 𝟙 X
Module: Mathlib.CategoryTheory.Center.Linear

Goal state before:
pp: R : Type w
inst✝³ : Ring R
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : Linear R C
⊢ { app := fun X ↦ 0 • 𝟙 X, naturality := ⋯ } = 0

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
S : ShortComplex C
hS : S.ShortExact
inst✝ : HasDerivedCategory C
X : C
n₀ : ℕ
x : Ext X S.X₃ n₀
n₁ : ℕ
h : n₀ + 1 = n₁
⊢ (ConcreteCategory.hom
        ((preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).homologySequenceδ hS.singleTriangle ↑n₀ ↑n₁ ⋯))
      x.hom =
    (x.comp hS.extClass h).hom

Tactic:
rw [Pretriangulated.preadditiveCoyoneda_homologySequenceδ_apply,
    comp_hom, hS.extClass_hom, ShiftedHom.comp]
  rfl

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Ext.Basic

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : Small.{v, u} R
M N : ModuleCat R
r : R
mem_ann : r ∈ Module.annihilator R ↑N
n : ℕ
h : ↑(AddCommGrpCat.of (Ext N M n))
⊢ r • 𝟙 N = 0

Tactic:
simp [← ModuleCat.lsmul_eq_smul_id, Module.mem_annihilator_iff_lsmul_eq_zero.mp mem_ann]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Nondegenerate

Goal state before:
pp: ι : Type u_1
κ : Type u_2
R : Type u_3
M : Type u_4
inst✝⁴ : Fintype ι
inst✝³ : Finite κ
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
hv : ∀ (g : ι → R), ∑ i, g i • v i = 0 → ∀ (i : ι), g i = 0
A : Matrix κ ι R
hA : A.Nondegenerate
this : Fintype κ
w : κ → R
hw : ∑ x, (∑ i, w i • A i x) • v x = 0
⊢ w = 0

Tactic:
replace hv : w ᵥ* A = 0 := funext <| hv _ hw

Goal state after:
ι : Type u_1
κ : Type u_2
R : Type u_3
M : Type u_4
inst✝⁴ : Fintype ι
inst✝³ : Finite κ
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
A : Matrix κ ι R
hA : A.Nondegenerate
this : Fintype κ
w : κ → R
hw : ∑ x, (∑ i, w i • A i x) • v x = 0
hv : w ᵥ* A = 0
⊢ w = 0
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs

Goal state before:
pp: n : Type u
R : Type v
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
inst✝³ : CommRing R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Fact (Even (Fintype.card n))
g : ↥(GLPos n R)
⊢ 0 < (-1) ^ Fintype.card n * (↑↑g).det

Tactic:
(Fact.out (p := Even <| Fintype.card n)).neg_one_pow,

Goal state after:
n : Type u
R : Type v
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
inst✝³ : CommRing R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Fact (Even (Fintype.card n))
g : ↥(GLPos n R)
⊢ 0 < 1 * (↑↑g).det
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
i : n
A : ↥(center (SpecialLinearGroup n R))
⊢ (fun a ↦ ⟨⟨a • 1, ⋯⟩, ⋯⟩) ((fun A ↦ rootsOfUnity.mkOfPowEq (↑↑A i i) ⋯) A) = A

Tactic:
by
    refine SetCoe.ext <| SetCoe.ext ?_
    obtain ⟨r, _, hr⟩ := mem_center_iff.mp A.property
    simpa [← hr, Submonoid.smul_def, Units.smul_def] using! smul_one_eq_diagonal r

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: case refine_1
ι : Type u_1
F : Type u_2
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : CommRing F
i j : ι
hij : i ≠ j
b : F
h : transvection hij b ∈ Subgroup.center (SpecialLinearGroup ι F)
⊢ b = 0

pp: case refine_2
ι : Type u_1
F : Type u_2
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : CommRing F
i j : ι
hij : i ≠ j
b : F
hb : b = 0
⊢ transvection hij b ∈ Subgroup.center (SpecialLinearGroup ι F)

Tactic:
· obtain ⟨r, _, hr⟩ := mem_center_iff.1 h
    simpa [transvection_coe, hij] using congr($hr i j).symm

Goal state after:
case refine_2
ι : Type u_1
F : Type u_2
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : CommRing F
i j : ι
hij : i ≠ j
b : F
hb : b = 0
⊢ transvection hij b ∈ Subgroup.center (SpecialLinearGroup ι F)
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: ⊢ !![0, -1; 1, 0].det = 1

Tactic:
simp [Matrix.det_fin_two_of]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: ⊢ !![1, 1; 0, 1].det = 1

Tactic:
simp [Matrix.det_fin_two_of]

Goal state after:
Module: Mathlib.Algebra.DirectSum.Ring

Goal state before:
pp: ι : Type u_1
inst✝⁴ : DecidableEq ι
A : ι → Type u_2
R : Type u_3
inst✝³ : (i : ι) → AddCommMonoid (A i)
inst✝² : AddMonoid ι
inst✝¹ : GSemiring A
inst✝ : Semiring R
f : (i : ι) → A i →+ R
hone : (f 0) GradedMonoid.GOne.one = 1
hmul : ∀ {i j : ι} (ai : A i) (aj : A j), (f (i + j)) (GradedMonoid.GMul.mul ai aj) = (f i) ai * (f j) aj
⊢ (toAddMonoid f) 1 = 1

Tactic:
by
      change (toAddMonoid f) (of _ 0 _) = 1
      rw [toAddMonoid_of]
      exact hone

Goal state after:
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Fold

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticForm R M
f : M →ₗ[R] CliffordAlgebra Q × N →ₗ[R] N
hf : ∀ (m : M) (x : CliffordAlgebra Q) (fx : N), (f m) ((ι Q) m * x, (f m) (x, fx)) = Q m • fx
v : M
x_fx : CliffordAlgebra Q × N
⊢ ((foldr'Aux Q f) v) (((foldr'Aux Q f) v) x_fx) = Q v • x_fx

Tactic:
simp only [foldr'Aux_apply_apply]
  rw [← mul_assoc, ι_sq_scalar, ← Algebra.smul_def, hf, Prod.smul_mk]

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.FilteredColimits

Goal state before:
pp: R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCat R
j : J
⊢ 0 = M.mk F ⟨j, 0⟩

Tactic:
by
  apply AddMonCat.FilteredColimits.colimit_zero_eq

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.LeftResolution

Goal state before:
pp: R : Type u
inst✝ : Ring R
X : Type u
M N : ModuleCat R
f : (free R).obj X ⟶ N
p : M ⟶ N
hp : Function.Surjective ⇑(ConcreteCategory.hom p)
s : ↑N → ↑M
hs : Function.RightInverse s ⇑(ConcreteCategory.hom p)
⊢ freeDesc (↾fun x ↦ s ((ConcreteCategory.hom f) (freeMk x))) ≫ p = f

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.Algebra.Module.LocalizedModule.Exact

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
S : Submonoid R
M₀ : Type u_2
inst✝⁵ : AddCommMonoid M₀
inst✝⁴ : Module R M₀
M₁ : Type u_3
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
M₂ : Type u_4
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
g : M₀ →ₗ[R] M₁
h : M₁ →ₗ[R] M₂
ex : Exact ⇑g ⇑h
y : LocalizedModule S M₁
x✝ : y ∈ Set.range ⇑((IsLocalizedModule.map S (mkLinearMap S M₀) (mkLinearMap S M₁)) g)
x : LocalizedModule S M₀
hx : ((IsLocalizedModule.map S (mkLinearMap S M₀) (mkLinearMap S M₁)) g) x = y
⊢ ((IsLocalizedModule.map S (mkLinearMap S M₁) (mkLinearMap S M₂)) h) y = 0

Tactic:
revert hx
      refine induction_on (fun m s hx ↦ ?_) x
      rw [← hx, map_LocalizedModules, map_LocalizedModules, (ex (g m)).2 ⟨m, rfl⟩, zero_mk]

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'App (RingCat.Hom.hom (R.map (𝟙 X))) ⋯ (colimit (F ⋙ evaluation R X))).inv

Tactic:
ι_colimMap_assoc,

Goal state after:
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
⊢ (F.whiskerLeft (restriction R (𝟙 X))).app j ≫
      colimit.ι (F ⋙ evaluation R X ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (𝟙 X)))) j ≫
        (preservesColimitIso (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (𝟙 X)))) (F ⋙ evaluation R X)).inv =
    colimit.ι (F ⋙ evaluation R X) j ≫
      (ModuleCat.restrictScalarsId'App (RingCat.Hom.hom (R.map (𝟙 X))) ⋯ (colimit (F ⋙ evaluation R X))).inv
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'App (RingCat.Hom.hom (R.map f)) (RingCat.Hom.hom (R.map g))
              (RingCat.Hom.hom (R.map (f ≫ g))) ⋯ (colimit (F ⋙ evaluation R Z))).inv

Tactic:
ι_colimMap_assoc,

Goal state after:
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
⊢ (F.whiskerLeft (restriction R (f ≫ g))).app j ≫
      colimit.ι (F ⋙ evaluation R Z ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (f ≫ g)))) j ≫
        (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'App (RingCat.Hom.hom (R.map f)) (RingCat.Hom.hom (R.map g))
              (RingCat.Hom.hom (R.map (f ≫ g))) ⋯ (colimit (F ⋙ evaluation R Z))).inv
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 (lift (𝟙 A) f ≫ (zeroMul t).hom)

Tactic:
exact mono_comp _ _

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
x✝ : J
⊢ { app := fun x ↦ snd (X.obj x) (Y.obj x), naturality := ⋯ }.app 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))
              X ▷
            Y ≫
          (λ_ Y).hom).app
      x✝

Tactic:
simp only [Monoidal.tensorObj_obj, snd_def, asEmptyCone_pt, NatTrans.comp_app,
      Monoidal.tensorUnit_obj, Monoidal.whiskerRight_app, Monoidal.leftUnitor_hom_app,
      Iso.cancel_iso_hom_right]

Goal state after:
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
x✝ : J
⊢ isTerminalTensorUnit.from (X.obj x✝) ▷ Y.obj x✝ =
    (IsTerminal.from
            (evaluationJointlyReflectsLimits (asEmptyCone (𝟙_ (J ⥤ C))) fun x ↦
              isLimitChangeEmptyCone C isTerminalTensorUnit
                (((evaluation J C).obj x).mapCone (asEmptyCone (𝟙_ (J ⥤ C)))) (Iso.refl (𝟙_ C)))
            X).app
        x✝ ▷
      Y.obj x✝
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Generator

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
R : Cᵒᵖ ⥤ RingCat
M N : PresheafOfModules R
f₁ f₂ : M ⟶ N
h : ∀ (G : PresheafOfModules R), freeYoneda R G → ∀ (h : G ⟶ M), h ≫ f₁ = h ≫ f₂
X : C
m : ↑(M.obj (Opposite.op X))
⊢ (ModuleCat.Hom.hom (f₁.app (Opposite.op X))) m = (ModuleCat.Hom.hom (f₂.app (Opposite.op X))) m

Tactic:
obtain ⟨g, rfl⟩ := freeYonedaEquiv.surjective m

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
R : Cᵒᵖ ⥤ RingCat
M N : PresheafOfModules R
f₁ f₂ : M ⟶ N
h : ∀ (G : PresheafOfModules R), freeYoneda R G → ∀ (h : G ⟶ M), h ≫ f₁ = h ≫ f₂
X : C
g : (free R).obj (yoneda.obj X) ⟶ M
⊢ (ModuleCat.Hom.hom (f₁.app (Opposite.op X))) (freeYonedaEquiv g) =
    (ModuleCat.Hom.hom (f₂.app (Opposite.op X))) (freeYonedaEquiv g)
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
X Y : F.PartialRightAdjointSource
f : X ⟶ Y
⊢ F.partialRightAdjointHomEquiv (F.partialRightAdjointMap f) =
    F.partialRightAdjointHomEquiv (𝟙 (F.partialRightAdjointObj X)) ≫ f.hom

Tactic:
simp [partialRightAdjointMap]

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

Goal state before:
pp: C₀ : Type u_1
C₁ : Type u_2
inst✝¹ : Category.{v_1, u_1} C₀
inst✝ : Category.{v_2, u_2} C₁
F₀₀' : C₀ ⥤ C₀
F₀'₁ : C₀ ⥤ C₁
G₀'₀ : C₀ ⥤ C₀
G₁₀' : C₁ ⥤ C₀
adj₀₀' : F₀₀' ⊣ G₀'₀
adj₀'₁ : F₀'₁ ⊣ G₁₀'
e₀'₀ : G₀'₀ ≅ 𝟭 C₀
X₀ : C₀
⊢ (adj₀₀'.leftAdjointCompIso adj₀'₁ adj₀'₁ (G₁₀'.isoWhiskerLeft e₀'₀ ≪≫ G₁₀'.rightUnitor)).hom.app X₀ =
    (isoWhiskerRight (adj₀₀'.leftAdjointIdIso e₀'₀) F₀'₁ ≪≫ F₀'₁.leftUnitor).hom.app X₀

Tactic:
have h₁ := congr_map F₀'₁ (adj₀₀'.counit.naturality (adj₀'₁.unit.app X₀))

Goal state after:
C₀ : Type u_1
C₁ : Type u_2
inst✝¹ : Category.{v_1, u_1} C₀
inst✝ : Category.{v_2, u_2} C₁
F₀₀' : C₀ ⥤ C₀
F₀'₁ : C₀ ⥤ C₁
G₀'₀ : C₀ ⥤ C₀
G₁₀' : C₁ ⥤ C₀
adj₀₀' : F₀₀' ⊣ G₀'₀
adj₀'₁ : F₀'₁ ⊣ G₁₀'
e₀'₀ : G₀'₀ ≅ 𝟭 C₀
X₀ : C₀
h₁ :
  F₀'₁.map ((G₀'₀ ⋙ F₀₀').map (adj₀'₁.unit.app X₀) ≫ adj₀₀'.counit.app ((F₀'₁ ⋙ G₁₀').obj X₀)) =
    F₀'₁.map (adj₀₀'.counit.app ((𝟭 C₀).obj X₀) ≫ (𝟭 C₀).map (adj₀'₁.unit.app X₀))
⊢ (adj₀₀'.leftAdjointCompIso adj₀'₁ adj₀'₁ (G₁₀'.isoWhiskerLeft e₀'₀ ≪≫ G₁₀'.rightUnitor)).hom.app X₀ =
    (isoWhiskerRight (adj₀₀'.leftAdjointIdIso e₀'₀) F₀'₁ ≪≫ F₀'₁.leftUnitor).hom.app X₀
Module: Mathlib.CategoryTheory.Sites.Precoverage

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : Precoverage C
inst✝ : J.IsStableUnderBaseChange
ι : Type w
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hR : Presieve.ofArrows X f ∈ J.coverings S
Y : C
g✝ : Y ⟶ S
P : ι → C
p₁ : (i : ι) → P i ⟶ Y
p₂ : (i : ι) → P i ⟶ X i
h : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g✝ (f i)
a : ↑(Presieve.ofArrows X f).uncurry ⊕ ↑(Presieve.ofArrows P p₁).uncurry → ι :=
  fun i ↦ Sum.elim (fun i ↦ Presieve.ofArrows.idx ⋯) (fun i ↦ Presieve.ofArrows.idx ⋯) i
Z : C
g : Z ⟶ Y
hg : Presieve.ofArrows P p₁ g
⊢ Z = (P ∘ a) (Sum.inr ⟨⟨Z, g⟩, hg⟩)

Tactic:
by cat_disch

Goal state after: