mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Multilinear.Basic

Goal state before:
pp: R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst✝¹² : Semiring R
inst✝¹¹ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝¹⁰ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : AddCommMonoid M₃
inst✝⁷ : AddCommMonoid M'
inst✝⁶ : (i : Fin n.succ) → Module R (M i)
inst✝⁵ : (i : ι) → Module R (M₁ i)
inst✝⁴ : Module R M₂
inst✝³ : Module R M₃
inst✝² : Module R M'
f✝ f' f : MultilinearMap R M₁ M₂
P : ι → Prop
inst✝¹ : DecidablePred P
z : (i : { a // ¬P a }) → M₁ ↑i
inst✝ : DecidableEq { a // P a }
x : (i : { a // P a }) → M₁ ↑i
i : { a // P a }
a b : M₁ ↑i
⊢ (f fun j ↦ if h : P j then update x i (a + b) ⟨j, h⟩ else z ⟨j, h⟩) =
    (f fun j ↦ if h : P j then update x i a ⟨j, h⟩ else z ⟨j, h⟩) +
      f fun j ↦ if h : P j then update x i b ⟨j, h⟩ else z ⟨j, h⟩

Tactic:
repeat (rw [domDomRestrict_aux])

Goal state after:
R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst✝¹² : Semiring R
inst✝¹¹ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝¹⁰ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : AddCommMonoid M₃
inst✝⁷ : AddCommMonoid M'
inst✝⁶ : (i : Fin n.succ) → Module R (M i)
inst✝⁵ : (i : ι) → Module R (M₁ i)
inst✝⁴ : Module R M₂
inst✝³ : Module R M₃
inst✝² : Module R M'
f✝ f' f : MultilinearMap R M₁ M₂
P : ι → Prop
inst✝¹ : DecidablePred P
z : (i : { a // ¬P a }) → M₁ ↑i
inst✝ : DecidableEq { a // P a }
x : (i : { a // P a }) → M₁ ↑i
i : { a // P a }
a b : M₁ ↑i
⊢ f (update (fun j ↦ if h : P j then x ⟨j, h⟩ else z ⟨j, h⟩) (↑i) (a + b)) =
    f (update (fun j ↦ if h : P j then x ⟨j, h⟩ else z ⟨j, h⟩) (↑i) a) +
      f (update (fun j ↦ if h : P j then x ⟨j, h⟩ else z ⟨j, h⟩) (↑i) b)
Module: Mathlib.LinearAlgebra.Multilinear.Basic

Goal state before:
pp: R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst✝¹² : Semiring R
inst✝¹¹ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝¹⁰ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : AddCommMonoid M₃
inst✝⁷ : AddCommMonoid M'
inst✝⁶ : (i : Fin n.succ) → Module R (M i)
inst✝⁵ : (i : ι) → Module R (M₁ i)
inst✝⁴ : Module R M₂
inst✝³ : Module R M₃
inst✝² : Module R M'
f✝ f' f : MultilinearMap R M₁ M₂
P : ι → Prop
inst✝¹ : DecidablePred P
z✝ : (i : { a // ¬P a }) → M₁ ↑i
inst✝ : DecidableEq { a // P a }
z : (i : { a // P a }) → M₁ ↑i
i : { a // P a }
c : R
a : M₁ ↑i
⊢ (f fun j ↦ if h : P j then update z i (c • a) ⟨j, h⟩ else z✝ ⟨j, h⟩) =
    c • f fun j ↦ if h : P j then update z i a ⟨j, h⟩ else z✝ ⟨j, h⟩

Tactic:
repeat (rw [domDomRestrict_aux])

Goal state after:
R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst✝¹² : Semiring R
inst✝¹¹ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝¹⁰ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : AddCommMonoid M₃
inst✝⁷ : AddCommMonoid M'
inst✝⁶ : (i : Fin n.succ) → Module R (M i)
inst✝⁵ : (i : ι) → Module R (M₁ i)
inst✝⁴ : Module R M₂
inst✝³ : Module R M₃
inst✝² : Module R M'
f✝ f' f : MultilinearMap R M₁ M₂
P : ι → Prop
inst✝¹ : DecidablePred P
z✝ : (i : { a // ¬P a }) → M₁ ↑i
inst✝ : DecidableEq { a // P a }
z : (i : { a // P a }) → M₁ ↑i
i : { a // P a }
c : R
a : M₁ ↑i
⊢ f (update (fun j ↦ if h : P j then z ⟨j, h⟩ else z✝ ⟨j, h⟩) (↑i) (c • a)) =
    c • f (update (fun j ↦ if h : P j then z ⟨j, h⟩ else z✝ ⟨j, h⟩) (↑i) a)
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: case e'_3.refine_3
m : Type u_1
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
σ : Perm (m ⊕ n)
σ₁₂ : Perm m × Perm n
hσ₁₂ : (sumCongrHom m n) σ₁₂ = σ
⊢ σ ∈ (fun σ ↦ σ.1.sumCongr σ.2) '' ↑univ

Tactic:
use σ₁₂

Goal state after:
case h
m : Type u_1
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
σ : Perm (m ⊕ n)
σ₁₂ : Perm m × Perm n
hσ₁₂ : (sumCongrHom m n) σ₁₂ = σ
⊢ σ₁₂ ∈ ↑univ ∧ (fun σ ↦ σ.1.sumCongr σ.2) σ₁₂ = σ
Module: Mathlib.LinearAlgebra.Multilinear.Basic

Goal state before:
pp: R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁵ : CommSemiring R
inst✝⁴ : (i : ι) → AddCommMonoid (M₁ i)
inst✝³ : AddCommMonoid M₂
inst✝² : (i : ι) → Module R (M₁ i)
inst✝¹ : Module R M₂
f : MultilinearMap R M₁ M₂
inst✝ : DecidableEq ι
c : ι → R
m : (i : ι) → M₁ i
s : Finset ι
⊢ f (s.piecewise (fun i ↦ c i • m i) m) = (∏ i ∈ s, c i) • f m

Tactic:
refine s.induction_on (by simp) ?_

Goal state after:
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁵ : CommSemiring R
inst✝⁴ : (i : ι) → AddCommMonoid (M₁ i)
inst✝³ : AddCommMonoid M₂
inst✝² : (i : ι) → Module R (M₁ i)
inst✝¹ : Module R M₂
f : MultilinearMap R M₁ M₂
inst✝ : DecidableEq ι
c : ι → R
m : (i : ι) → M₁ i
s : Finset ι
⊢ ∀ (a : ι) (s : Finset ι),
    a ∉ s →
      f (s.piecewise (fun i ↦ c i • m i) m) = (∏ i ∈ s, c i) • f m →
        f ((insert a s).piecewise (fun i ↦ c i • m i) m) = (∏ i ∈ insert a s, c i) • f m
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: case refine_2
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
i✝ : Fin n.succ
x✝ : i✝ ∈ univ
i : Fin n
this : (-1) ^ ↑i = ↑↑(sign i.cycleRange)
⊢ ∑ y, sign (decomposeFin.symm (i.succ, y)) • ∏ x, A ((decomposeFin.symm (i.succ, y)) x) x =
    (-1) ^ (↑i + 1) * A i.succ 0 * (of fun i_1 j ↦ A (i.succ.succAbove i_1) j.succ).det

Tactic:
pow_succ',

Goal state after:
case refine_2
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
i✝ : Fin n.succ
x✝ : i✝ ∈ univ
i : Fin n
this : (-1) ^ ↑i = ↑↑(sign i.cycleRange)
⊢ ∑ y, sign (decomposeFin.symm (i.succ, y)) • ∏ x, A ((decomposeFin.symm (i.succ, y)) x) x =
    -1 * (-1) ^ ↑i * A i.succ 0 * (of fun i_1 j ↦ A (i.succ.succAbove i_1) j.succ).det
Module: Mathlib.LinearAlgebra.Multilinear.Basic

Goal state before:
pp: case pos.hi
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁵ : Semiring R
inst✝⁴ : (i : ι) → AddCommGroup (M₁ i)
inst✝³ : AddCommGroup M₂
inst✝² : (i : ι) → Module R (M₁ i)
inst✝¹ : Module R M₂
f : MultilinearMap R M₁ M₂
inst✝ : LinearOrder ι
a b : (i : ι) → M₁ i
k : ι
s : Finset ι
hk : ∀ x ∈ s, k < x
ih : f a - f (s.piecewise b a) = ∑ i ∈ s, f fun j ↦ if j ∈ s → j < i then a j else if i = j then a j - b j else b j
i : ι
h₁ : i = k ∨ i ∈ s → i < k
⊢ i ∉ s

Tactic:
exact fun h ↦ (hk i h).not_gt (h₁ <| .inr h)

Goal state after:
Module: Mathlib.CategoryTheory.ShrinkYoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
X X' : C
Y : Cᵒᵖ
f : unop Y ⟶ X
g : X ⟶ X'
⊢ (ConcreteCategory.hom ((shrinkYoneda.{w, v, u}.map g).app Y)) (shrinkYonedaObjObjEquiv.symm f) =
    shrinkYonedaObjObjEquiv.symm (f ≫ g)

Tactic:
simp [shrinkYoneda, shrinkYonedaObjObjEquiv]

Goal state after:
Module: Mathlib.CategoryTheory.ShrinkYoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
X X' : C
Y : Cᵒᵖ
f : (shrinkYoneda.{w, v, u}.obj X).obj Y
g : X ⟶ X'
⊢ shrinkYonedaObjObjEquiv ((ConcreteCategory.hom ((shrinkYoneda.{w, v, u}.map g).app Y)) f) =
    shrinkYonedaObjObjEquiv f ≫ g

Tactic:
simp [shrinkYoneda, shrinkYonedaObjObjEquiv]

Goal state after:
Module: Mathlib.CategoryTheory.ShrinkYoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
Y : C
X✝ Y✝ : Cᵒᵖ
f : X✝ ⟶ Y✝
g : unop X✝ ⟶ Y
⊢ (ConcreteCategory.hom
          ((shrinkCoyoneda.{w, v, u} ⋙ (evaluation C (Type w)).obj Y ⋙ uliftFunctor.{v, w}).map f ≫
            (Equiv.ulift.trans (shrinkCoyonedaObjObjEquiv.trans Equiv.ulift.symm)).toIso.hom)).toFun
      { down := shrinkCoyonedaObjObjEquiv.symm g } =
    (ConcreteCategory.hom
          ((Equiv.ulift.trans (shrinkCoyonedaObjObjEquiv.trans Equiv.ulift.symm)).toIso.hom ≫
            (yoneda.obj Y ⋙ uliftFunctor.{w, v}).map f)).toFun
      { down := shrinkCoyonedaObjObjEquiv.symm g }

Tactic:
simp [shrinkYoneda, shrinkYonedaObjObjEquiv]

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Limits

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ CommGrpCat
c : Cone (F ⋙ forget₂ CommGrpCat GrpCat)
hc : IsLimit c
this✝² : HasLimit (F ⋙ forget₂ CommGrpCat GrpCat)
this✝¹ : Small.{u, max u v} ↑(F ⋙ forget CommGrpCat).sections
this✝ : Small.{u, max u v} ↑((F ⋙ forget₂ CommGrpCat GrpCat ⋙ forget₂ GrpCat MonCat) ⋙ forget MonCat).sections
this : Small.{u, max u v} ↑((F ⋙ forget₂ CommGrpCat GrpCat) ⋙ forget GrpCat).sections
⊢ IsLimit
    ((forget₂ CommGrpCat GrpCat ⋙ forget₂ GrpCat MonCat).mapCone
      { pt := of (Types.Small.limitCone (F ⋙ forget CommGrpCat)).pt,
        π :=
          { app := fun j ↦ ofHom (MonCat.limitπMonoidHom (F ⋙ forget₂ CommGrpCat GrpCat ⋙ forget₂ GrpCat MonCat) j),
            naturality := ⋯ } })

Tactic:
by apply MonCat.HasLimits.limitConeIsLimit _

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : L.Faithful
inst✝ : L.Full
X : D
⊢ IsIso (h.counit.app X) ↔ L.essImage X

Tactic:
constructor
  · intro
    exact ⟨R.obj X, ⟨asIso (h.counit.app X)⟩⟩
  · rintro ⟨_, ⟨i⟩⟩
    rw [NatTrans.isIso_app_iff_of_iso _ i.symm]
    infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Category

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
W X Y Z : C
⊢ (α_ W X (Y ⊗ Z)).hom ≫ W ◁ (α_ X Y Z).inv ≫ (α_ W (X ⊗ Y) Z).inv = (α_ (W ⊗ X) Y Z).inv ≫ (α_ W X Y).hom ▷ Z

Tactic:
← cancel_epi (α_ W X (Y ⊗ Z)).inv,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
W X Y Z : C
⊢ (α_ W X (Y ⊗ Z)).inv ≫ (α_ W X (Y ⊗ Z)).hom ≫ W ◁ (α_ X Y Z).inv ≫ (α_ W (X ⊗ Y) Z).inv =
    (α_ W X (Y ⊗ Z)).inv ≫ (α_ (W ⊗ X) Y Z).inv ≫ (α_ W X Y).hom ▷ Z
Module: Mathlib.CategoryTheory.Monoidal.Preadditive

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Finite J
X : C
f : J → C
j : J
⊢ (leftDistributor X f).inv ≫ X ◁ biproduct.π f j = biproduct.π (fun j ↦ X ⊗ f j) j

Tactic:
cases nonempty_fintype J
  simp [leftDistributor_inv, Preadditive.sum_comp, ← whiskerLeft_comp,
    biproduct.ι_π, whiskerLeft_dite, comp_dite]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : C ⥤ D
inst✝ : F.Monoidal
X Y Z : C
⊢ F.map (α_ X Y Z).hom =
    δ F (X ⊗ Y) Z ≫ δ F X Y ▷ F.obj Z ≫ (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom ≫ F.obj X ◁ μ F Y Z ≫ μ F X (Y ⊗ Z)

Tactic:
← LaxMonoidal.associativity F,

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : C ⥤ D
inst✝ : F.Monoidal
X Y Z : C
⊢ F.map (α_ X Y Z).hom = δ F (X ⊗ Y) Z ≫ δ F X Y ▷ F.obj Z ≫ μ F X Y ▷ F.obj Z ≫ μ F (X ⊗ Y) Z ≫ F.map (α_ X Y Z).hom
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : C ⥤ D
inst✝ : F.Monoidal
X Y Z : C
⊢ F.map (α_ X Y Z).hom = δ F (X ⊗ Y) Z ≫ δ F X Y ▷ F.obj Z ≫ μ F X Y ▷ F.obj Z ≫ μ F (X ⊗ Y) Z ≫ F.map (α_ X Y Z).hom

Tactic:
whiskerRight_δ_μ_assoc,

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : C ⥤ D
inst✝ : F.Monoidal
X Y Z : C
⊢ F.map (α_ X Y Z).hom = δ F (X ⊗ Y) Z ≫ μ F (X ⊗ Y) Z ≫ F.map (α_ X Y Z).hom
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : C ⥤ D
inst✝ : F.Monoidal
X Y Z : C
⊢ 𝟙 (F.obj ((X ⊗ Y) ⊗ Z)) =
    δ F (X ⊗ Y) Z ≫
      δ F X Y ▷ F.obj Z ≫
        (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom ≫
          F.obj X ◁ μ F Y Z ≫
            μ F X (Y ⊗ Z) ≫ F.map (α_ X Y Z).inv ≫ δ F (X ⊗ Y) Z ≫ δ F X Y ▷ F.obj Z ≫ μ F X Y ▷ F.obj Z ≫ μ F (X ⊗ Y) Z

Tactic:
whiskerRight_δ_μ_assoc,

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : C ⥤ D
inst✝ : F.Monoidal
X Y Z : C
⊢ 𝟙 (F.obj ((X ⊗ Y) ⊗ Z)) =
    δ F (X ⊗ Y) Z ≫
      δ F X Y ▷ F.obj Z ≫
        (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom ≫
          F.obj X ◁ μ F Y Z ≫ μ F X (Y ⊗ Z) ≫ F.map (α_ X Y Z).inv ≫ δ F (X ⊗ Y) Z ≫ μ F (X ⊗ Y) Z
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : C ⥤ D
inst✝ : F.Monoidal
X Y Z : C
⊢ 𝟙 (F.obj ((X ⊗ Y) ⊗ Z)) = δ F (X ⊗ Y) Z ≫ δ F X Y ▷ F.obj Z ≫ μ F X Y ▷ F.obj Z ≫ μ F (X ⊗ Y) Z

Tactic:
whiskerRight_δ_μ_assoc,

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : C ⥤ D
inst✝ : F.Monoidal
X Y Z : C
⊢ 𝟙 (F.obj ((X ⊗ Y) ⊗ Z)) = δ F (X ⊗ Y) Z ≫ μ F (X ⊗ Y) Z
Module: Mathlib.Algebra.Category.Grp.ZModuleEquivalence

Goal state before:
pp: A B : ModuleCat ℤ
f : (forget₂ (ModuleCat ℤ) AddCommGrpCat).obj A ⟶ (forget₂ (ModuleCat ℤ) AddCommGrpCat).obj B
n : ℤ
x : ↑A
⊢ { toFun := ⇑(ConcreteCategory.hom f), map_add' := ⋯ }.toFun (n • x) =
    (RingHom.id ℤ) n • { toFun := ⇑(ConcreteCategory.hom f), map_add' := ⋯ }.toFun x

Tactic:
convert! AddMonoidHom.map_zsmul f.hom n x <;>
                ext <;> apply int_smul_eq_zsmul

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
inst✝ : HasPushouts C
⊢ HasPullbacks Cᵒᵖ

Tactic:
have : HasColimitsOfShape WalkingCospanᵒᵖ C :=
    hasColimitsOfShape_of_equivalence walkingCospanOpEquiv.symm

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
inst✝ : HasPushouts C
this : HasColimitsOfShape WalkingCospanᵒᵖ C
⊢ HasPullbacks Cᵒᵖ
Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y Z : C
⊢ ((β_ X (Y ⊗ Z)).hom ≫ (β_ Y Z).hom ▷ X ≫ (α_ Z Y X).hom) ≫ (α_ Z Y X).inv =
    (X ◁ (β_ Y Z).hom ≫ (α_ X Z Y).inv ≫ (β_ X Z).hom ▷ Y ≫ (α_ Z X Y).hom ≫ Z ◁ (β_ X Y).hom) ≫ (α_ Z Y X).inv

Tactic:
repeat rw [assoc]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y Z : C
⊢ (β_ X (Y ⊗ Z)).hom ≫ (β_ Y Z).hom ▷ X ≫ (α_ Z Y X).hom ≫ (α_ Z Y X).inv =
    X ◁ (β_ Y Z).hom ≫ (α_ X Z Y).inv ≫ (β_ X Z).hom ▷ Y ≫ (α_ Z X Y).hom ≫ Z ◁ (β_ X Y).hom ≫ (α_ Z Y X).inv
Module: Mathlib.CategoryTheory.MorphismProperty.Composition

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
W : MorphismProperty C
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
hf : W.multiplicativeClosure' f
hg : W.multiplicativeClosure' g
⊢ W.multiplicativeClosure' (f ≫ g)

Tactic:
by
    induction hf with
    | of _ h => exact .of_comp _ g h hg
    | id _ => rwa [Category.id_comp]
    | of_comp g' f hg' hf h_rec =>
      rw [Category.assoc]
      exact .of_comp g' (f ≫ g) hg' (h_rec g hg)

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Concrete

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type u_2
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
X : C
⊢ MorphismProperty.surjective C (𝟙 X)

Tactic:
by
    delta MorphismProperty.surjective
    convert! surjective_id
    aesop

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

Goal state before:
pp: R : Type w
inst✝² : Ring R
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ ModuleCat R
inst✝ : HasColimit (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat)
s : Cocone F
j : J
⊢ (forget₂ (ModuleCat R) AddCommGrpCat).map
      ((colimitCocone F).ι.app j ≫
        homMk
          (colimit.desc (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) ((forget₂ (ModuleCat R) AddCommGrpCat).mapCocone s))
          ⋯) =
    (forget₂ (ModuleCat R) AddCommGrpCat).map (s.ι.app j)

Tactic:
exact colimit.ι_desc ((forget₂ _ AddCommGrpCat).mapCocone s) j

Goal state after:
Module: Mathlib.Algebra.Category.BialgCat.Basic

Goal state before:
pp: R : Type u
inst✝ : CommRing R
X Y : BialgCat R
f : X ⟶ Y
x✝ : IsIso ((forget (BialgCat R)).map f)
⊢ IsIso f

Tactic:
let i := asIso ((forget (BialgCat.{v} R)).map f)
    let e : X ≃ₐc[R] Y := { f.toBialgHom, i.toEquiv with }
    exact ⟨e.toBialgIso.isIso_hom.1⟩

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

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

Tactic:
by
  apply ExtendRestrictScalarsAdj.Counit.map_apply_one_tmul

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity

Goal state before:
pp: case succ.mp
R : Type u_2
inst✝² : CommMonoidWithZero R
inst✝¹ : UniqueFactorizationMonoid R
inst✝ : NormalizationMonoid R
a : R
ha : Irreducible a
n : ℕ
ih : ∀ {b : R}, b ≠ 0 → (a ^ n ∣ b ↔ replicate n (normalize a) ≤ normalizedFactors b)
c : R
hb : ¬a ^ (n + 1) * c = 0
⊢ replicate (n + 1) (normalize a) ≤ normalizedFactors (a ^ (n + 1) * c)

Tactic:
pow_succ',

Goal state after:
case succ.mp
R : Type u_2
inst✝² : CommMonoidWithZero R
inst✝¹ : UniqueFactorizationMonoid R
inst✝ : NormalizationMonoid R
a : R
ha : Irreducible a
n : ℕ
ih : ∀ {b : R}, b ≠ 0 → (a ^ n ∣ b ↔ replicate n (normalize a) ≤ normalizedFactors b)
c : R
hb : ¬a * a ^ n * c = 0
⊢ replicate (n + 1) (normalize a) ≤ normalizedFactors (a ^ (n + 1) * c)
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity

Goal state before:
pp: case succ.mp
R : Type u_2
inst✝² : CommMonoidWithZero R
inst✝¹ : UniqueFactorizationMonoid R
inst✝ : NormalizationMonoid R
a : R
ha : Irreducible a
n : ℕ
ih : ∀ {b : R}, b ≠ 0 → (a ^ n ∣ b ↔ replicate n (normalize a) ≤ normalizedFactors b)
c : R
hb : ¬a = 0 ∧ ¬a ^ n * c = 0
⊢ replicate (n + 1) (normalize a) ≤ normalizedFactors (a ^ (n + 1) * c)

Tactic:
pow_succ',

Goal state after:
case succ.mp
R : Type u_2
inst✝² : CommMonoidWithZero R
inst✝¹ : UniqueFactorizationMonoid R
inst✝ : NormalizationMonoid R
a : R
ha : Irreducible a
n : ℕ
ih : ∀ {b : R}, b ≠ 0 → (a ^ n ∣ b ↔ replicate n (normalize a) ≤ normalizedFactors b)
c : R
hb : ¬a = 0 ∧ ¬a ^ n * c = 0
⊢ replicate (n + 1) (normalize a) ≤ normalizedFactors (a * a ^ n * c)
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity

Goal state before:
pp: R : Type u_2
inst✝³ : CommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
a b : R
ha : Irreducible a
hb : b ≠ 0
this : emultiplicity a b = ↑(count (normalize a) (normalizedFactors b))
⊢ multiplicity a b = count (normalize a) (normalizedFactors b)

Tactic:
rwa [(finiteMultiplicity_of_emultiplicity_eq_natCast this).emultiplicity_eq_multiplicity,
    ENat.natCast_inj] at this

Goal state after:
Module: Mathlib.RingTheory.LocalRing.RingHom.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : IsLocalRing R
inst✝² : Semiring S
inst✝¹ : Nontrivial S
f : R →+* S
inst✝ : IsLocalHom f
hf : Function.Surjective ⇑f
a b : R
hab : IsUnit (f a + f b)
⊢ IsUnit (f a) ∨ IsUnit (f b)

Tactic:
rw [← map_add] at hab

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : IsLocalRing R
inst✝² : Semiring S
inst✝¹ : Nontrivial S
f : R →+* S
inst✝ : IsLocalHom f
hf : Function.Surjective ⇑f
a b : R
hab : IsUnit (f (a + b))
⊢ IsUnit (f a) ∨ IsUnit (f b)
Module: Mathlib.Algebra.Module.LocalizedModule.IsLocalization

Goal state before:
pp: case refine_1
R : Type u_1
inst✝⁶ : CommSemiring R
S : Submonoid R
A : Type u_2
Aₛ : Type u_3
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : CommSemiring Aₛ
inst✝² : Algebra A Aₛ
inst✝¹ : Algebra R Aₛ
inst✝ : IsScalarTower R A Aₛ
⊢ (∀ a ∈ S, IsUnit ((algebraMap R Aₛ) a)) ↔ ∀ a ∈ Submonoid.map (algebraMap R A) S, IsUnit ((algebraMap A Aₛ) a)

Tactic:
← SetLike.mem_coe,

Goal state after:
case refine_1
R : Type u_1
inst✝⁶ : CommSemiring R
S : Submonoid R
A : Type u_2
Aₛ : Type u_3
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : CommSemiring Aₛ
inst✝² : Algebra A Aₛ
inst✝¹ : Algebra R Aₛ
inst✝ : IsScalarTower R A Aₛ
⊢ (∀ a ∈ ↑S, IsUnit ((algebraMap R Aₛ) a)) ↔ ∀ a ∈ ↑(Submonoid.map (algebraMap R A) S), IsUnit ((algebraMap A Aₛ) a)
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : BraidedCategory C
M N : C
inst✝¹ : MonObj M
inst✝ : MonObj N
⊢ (M ⊗ N) ◁ ((λ_ (𝟙_ C)).inv ≫ (η ⊗ₘ η)) ≫ tensorμ M N M N ≫ (μ ⊗ₘ μ) = (ρ_ (M ⊗ N)).hom

Tactic:
by
  simp only [whiskerLeft_comp_assoc]
  slice_lhs 2 3 => rw [tensorμ_natural_right]
  slice_lhs 3 4 => rw [tensorHom_comp_tensorHom, mul_one, mul_one]
  symm
  exact tensor_right_unitality M N

Goal state after:
Module: Mathlib.RingTheory.Localization.Module

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_3
Mₛ : Type u_4
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid Mₛ
inst✝¹ : Module R Mₛ
f : M →ₗ[R] Mₛ
inst✝ : IsLocalizedModule S f
ι : Type u_5
v : ι → M
hv : LinearIndependent R v
h : ∀ (s : ↥S), IsRegular ↑s
⊢ Set.InjOn ⇑f ↑(Finsupp.linearCombination R v).range

Tactic:
rintro _ ⟨_, r, rfl⟩ _ ⟨_, r', rfl⟩ eq

Goal state after:
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_3
Mₛ : Type u_4
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid Mₛ
inst✝¹ : Module R Mₛ
f : M →ₗ[R] Mₛ
inst✝ : IsLocalizedModule S f
ι : Type u_5
v : ι → M
hv : LinearIndependent R v
h : ∀ (s : ↥S), IsRegular ↑s
w✝¹ w✝ : ι →₀ R
eq : f ((Finsupp.linearCombination R v) w✝¹) = f ((Finsupp.linearCombination R v) w✝)
⊢ (Finsupp.linearCombination R v) w✝¹ = (Finsupp.linearCombination R v) w✝
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
h : IsPushout f g inl inr
inst : IsIso g
⊢ IsIso inl

Tactic:
have := h.hasPushout
  rw [← h.inl_isoPushout_inv]
  infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: case uniq
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPullback f f g g'
s : Fork g g'
m : s.pt ⟶ (Fork.ofι f ⋯).pt
e : m ≫ (Fork.ofι f ⋯).ι = s.ι
⊢ m = H.isLimit.lift (PullbackCone.mk s.ι s.ι ⋯)

Tactic:
apply PullbackCone.IsLimit.hom_ext H.isLimit <;> refine e.trans ?_ <;> symm

Goal state after:
case uniq.h₀
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPullback f f g g'
s : Fork g g'
m : s.pt ⟶ (Fork.ofι f ⋯).pt
e : m ≫ (Fork.ofι f ⋯).ι = s.ι
⊢ H.isLimit.lift (PullbackCone.mk s.ι s.ι ⋯) ≫ H.cone.fst = s.ι

case uniq.h₁
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPullback f f g g'
s : Fork g g'
m : s.pt ⟶ (Fork.ofι f ⋯).pt
e : m ≫ (Fork.ofι f ⋯).ι = s.ι
⊢ H.isLimit.lift (PullbackCone.mk s.ι s.ι ⋯) ≫ H.cone.snd = s.ι