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

Goal state before:
pp: case refine_4
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
R : Type v
inst✝² : CommRing R
o : Type u_3
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := {σ | ∀ (x : n × o), (σ x).2 = x.2}
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (σ x).2 = x.2
⊢ ∀ a ∈ univ,
    ∏ x, ↑↑(sign (a x ⋯)) * ∏ x_1, M x ((a x ⋯) x_1) x_1 =
      ↑↑(sign (prodCongrLeft fun k ↦ a k ⋯)) * ∏ i, blockDiagonal M ((prodCongrLeft fun k ↦ a k ⋯) i) i

Tactic:
· intro σ _
      rw [Finset.prod_mul_distrib, ← Finset.univ_product_univ, Finset.prod_product_right]
      simp only [sign_prodCongrLeft, Units.coe_prod, Int.cast_prod, blockDiagonal_apply_eq,
        prodCongrLeft_apply]

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

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCat
inst✝ : IsFiltered J
j₁ : J
x : ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).obj j₁
j₂ : J
y : ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).obj j₂
j₃ : J
z : ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).obj j₃
k : J := IsFiltered.max₃ j₁ j₂ j₃
f : j₁ ⟶ IsFiltered.max₃ j₁ j₂ j₃ := IsFiltered.firstToMax₃ j₁ j₂ j₃
g : j₂ ⟶ IsFiltered.max₃ j₁ j₂ j₃ := IsFiltered.secondToMax₃ j₁ j₂ j₃
h : j₃ ⟶ IsFiltered.max₃ j₁ j₂ j₃ := IsFiltered.thirdToMax₃ j₁ j₂ j₃
⊢ Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel ⟨j₁, x⟩ *
      (Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel ⟨j₂, y⟩ +
        Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel ⟨j₃, z⟩) =
    Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel ⟨j₁, x⟩ *
        Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel ⟨j₂, y⟩ +
      Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel ⟨j₁, x⟩ *
        Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel ⟨j₃, z⟩

Tactic:
colimit_add_mk_eq _ ⟨j₂, _⟩ ⟨j₃, _⟩ k g h,

Goal state after:
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCat
inst✝ : IsFiltered J
j₁ : J
x : ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).obj j₁
j₂ : J
y : ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).obj j₂
j₃ : J
z : ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).obj j₃
k : J := IsFiltered.max₃ j₁ j₂ j₃
f : j₁ ⟶ IsFiltered.max₃ j₁ j₂ j₃ := IsFiltered.firstToMax₃ j₁ j₂ j₃
g : j₂ ⟶ IsFiltered.max₃ j₁ j₂ j₃ := IsFiltered.secondToMax₃ j₁ j₂ j₃
h : j₃ ⟶ IsFiltered.max₃ j₁ j₂ j₃ := IsFiltered.thirdToMax₃ j₁ j₂ j₃
⊢ Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel ⟨j₁, x⟩ *
      AddMonCat.FilteredColimits.M.mk ((F ⋙ forget₂ SemiRingCat AddCommMonCat) ⋙ forget₂ AddCommMonCat AddMonCat)
        ⟨k,
          (ConcreteCategory.hom (((F ⋙ forget₂ SemiRingCat AddCommMonCat) ⋙ forget₂ AddCommMonCat AddMonCat).map g))
              ⟨j₂, y⟩.snd +
            (ConcreteCategory.hom (((F ⋙ forget₂ SemiRingCat AddCommMonCat) ⋙ forget₂ AddCommMonCat AddMonCat).map h))
              ⟨j₃, z⟩.snd⟩ =
    Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel ⟨j₁, x⟩ *
        Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel ⟨j₂, y⟩ +
      Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel ⟨j₁, x⟩ *
        Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel ⟨j₃, z⟩
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
⊢ Aᵀ.det = ∑ j, (-1) ^ ↑j * A 0 j * (A.submatrix Fin.succ j.succAbove).det

Tactic:
det_succ_column_zero

Goal state after:
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
⊢ ∑ i, (-1) ^ ↑i * Aᵀ i 0 * (Aᵀ.submatrix i.succAbove Fin.succ).det =
    ∑ j, (-1) ^ ↑j * A 0 j * (A.submatrix Fin.succ j.succAbove).det
Module: Mathlib.CategoryTheory.Limits.Preserves.Limits

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
inst✝⁵ : Category.{w', w} J
F : J ⥤ C
inst✝⁴ : PreservesColimit F G
inst✝³ : HasColimit F
inst✝² : PreservesColimitsOfShape J G
inst✝¹ : HasColimitsOfShape J D
inst✝ : HasColimitsOfShape J C
X✝ Y✝ : J ⥤ C
f : X✝ ⟶ Y✝
⊢ (preservesColimitIso G X✝).inv ≫ (colim ⋙ G).map f =
    ((Functor.whiskeringRight J C D).obj G ⋙ colim).map f ≫ (preservesColimitIso G Y✝).inv

Tactic:
apply colimit.hom_ext

Goal state after:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
inst✝⁵ : Category.{w', w} J
F : J ⥤ C
inst✝⁴ : PreservesColimit F G
inst✝³ : HasColimit F
inst✝² : PreservesColimitsOfShape J G
inst✝¹ : HasColimitsOfShape J D
inst✝ : HasColimitsOfShape J C
X✝ Y✝ : J ⥤ C
f : X✝ ⟶ Y✝
⊢ ∀ (j : J),
    colimit.ι (((Functor.whiskeringRight J C D).obj G).obj X✝) j ≫ (preservesColimitIso G X✝).inv ≫ (colim ⋙ G).map f =
      colimit.ι (((Functor.whiskeringRight J C D).obj G).obj X✝) j ≫
        ((Functor.whiskeringRight J C D).obj G ⋙ colim).map f ≫ (preservesColimitIso G Y✝).inv
Module: Mathlib.CategoryTheory.Limits.Creates

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K : J ⥤ C
F G : C ⥤ D
h : F ≅ G
inst✝ : CreatesColimit K F
c : Cocone (K ⋙ G)
t : IsColimit c
⊢ G.mapCocone (liftColimit ((IsColimit.precomposeHomEquiv (K.isoWhiskerLeft h) c).symm t)) ≅ c

Tactic:
refine (IsColimit.mapCoconeEquiv h ?_).uniqueUpToIso t

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K : J ⥤ C
F G : C ⥤ D
h : F ≅ G
inst✝ : CreatesColimit K F
c : Cocone (K ⋙ G)
t : IsColimit c
⊢ IsColimit (F.mapCocone (liftColimit ((IsColimit.precomposeHomEquiv (K.isoWhiskerLeft h) c).symm t)))
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
inst✝ : HasColimitsOfShape J C
F : J ⥤ K ⥤ C
j : J
k : K
⊢ colimit.ι (F ⋙ (evaluation K C).obj k) j ≫ (colimitObjIsoColimitCompEvaluation F k).inv = (colimit.ι F j).app k

Tactic:
by
  dsimp [colimitObjIsoColimitCompEvaluation]
  simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
inst✝ : HasColimitsOfShape J C
F : J ⥤ K ⥤ C
i j : K
f : i ⟶ j
⊢ (colimitObjIsoColimitCompEvaluation F i).inv ≫ (colimit F).map f =
    colimMap (F.whiskerLeft ((evaluation K C).map f)) ≫ (colimitObjIsoColimitCompEvaluation F j).inv

Tactic:
colimitObjIsoColimitCompEvaluation_inv_colimit_map

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
inst✝ : HasColimitsOfShape J C
F : J ⥤ K ⥤ C
i j : K
f : i ⟶ j
⊢ colimMap (F.whiskerLeft ((evaluation K C).map f)) ≫ (colimitObjIsoColimitCompEvaluation F j).inv =
    colimMap (F.whiskerLeft ((evaluation K C).map f)) ≫ (colimitObjIsoColimitCompEvaluation F j).inv
Module: Mathlib.Algebra.Category.Grp.Limits

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

Tactic:
by apply IsLimit.uniqueUpToIso (MonCat.HasLimits.limitConeIsLimit.{v, u} _) t

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
hc : IsLimit c
⊢ Small.{u, max u v} ↑((F ⋙ forget₂ CommGrpCat GrpCat) ⋙ forget GrpCat).sections

Tactic:
change Small.{u} (F ⋙ forget CommGrpCat).sections

Goal state after:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ CommGrpCat
c : Cone F
hc : IsLimit c
⊢ Small.{u, max u v} ↑(F ⋙ forget CommGrpCat).sections
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
f : X ⟶ Y
g : Y ⟶ Z
⊢ W ◁ (f ≫ g) = W ◁ f ≫ W ◁ g

Tactic:
simp [← id_tensorHom]

Goal state after:
Module: Mathlib.Tactic.CategoryTheory.Monoidal.Normalize

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
f f' g g' h i : C
α : f ≅ g
η : g ⟶ h
ηs : h ⟶ i
β : f' ≅ g'
η₁ : g ⊗ g' ⟶ h ⊗ g'
ηs₁ : h ⊗ g' ⟶ i ⊗ g'
η₂ : g ⊗ g' ⟶ i ⊗ g'
η₃ : f ⊗ f' ⟶ i ⊗ g'
e_η₁ : ((Iso.refl g).hom ≫ η ≫ (Iso.refl h).hom) ▷ g' = η₁
e_ηs₁ : ηs ▷ g' = ηs₁
e_η₂ : η₁ ≫ ηs₁ = η₂
e_η₃ : (α ⊗ᵢ β).hom ≫ η₂ = η₃
⊢ α.hom ≫ η ≫ ηs ⊗ₘ β.hom = η₃

Tactic:
by
  simp_all [MonoidalCategory.tensorHom_def']

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
F : J ⥤ Cᵒᵖ
c : Cone F
hc : IsLimit c
s : Cocone F.leftOp
j : Jᵒᵖ
⊢ ((coconeLeftOpOfCone c).ι.app j ≫ (hc.lift (coneOfCoconeLeftOp s)).unop).op = (s.ι.app j).op

Tactic:
by
      simp only [coconeLeftOpOfCone_ι_app, op_comp, Quiver.Hom.op_unop, IsLimit.fac,
        coneOfCoconeLeftOp_π_app, op_unop]

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
⊢ HasLimitsOfShape J Cᵒᵖ ↔ HasColimitsOfShape Jᵒᵖ C

Tactic:
refine ⟨fun _ ↦ ?_, fun _ ↦ inferInstance⟩
  have : HasLimitsOfShape Jᵒᵖᵒᵖ Cᵒᵖ := hasLimitsOfShape_of_equivalence (opOpEquivalence J).symm
  exact hasColimitsOfShape_of_hasLimitsOfShape_op

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.EpiMono

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : ReflectsColimit (span f f) F
inst✝ : Epi (F.map f)
⊢ Epi f

Tactic:
have := PushoutCocone.isColimitMkIdId (F.map f)
  simp_rw [← F.map_id] at this
  apply
    PushoutCocone.epi_of_isColimitMkIdId _
      (isColimitOfIsColimitPushoutCoconeMap F _ this)

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✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
hf : MorphismProperty.surjective C f
hg : MorphismProperty.surjective C g
⊢ MorphismProperty.surjective C (f ≫ g)

Tactic:
delta MorphismProperty.surjective
    rw [hom_comp]
    exact hg.comp hf

Goal state after:
Module: Mathlib.CategoryTheory.ConcreteCategory.EpiMono

Goal state before:
pp: C✝ : Type u
inst✝¹⁰ : Category.{v, u} C✝
FC✝ : C✝ → C✝ → Type u_1
CC✝ : C✝ → Type w
inst✝⁹ : (X Y : C✝) → FunLike (FC✝ X Y) (CC✝ X) (CC✝ Y)
inst✝⁸ : ConcreteCategory C✝ FC✝
C : Type u
D : Type u'
inst✝⁷ : Category.{v, u} C
inst✝⁶ : Category.{v', u'} D
FC : C → C → Type u_2
CC : C → Type w
inst✝⁵ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁴ : ConcreteCategory C FC
FD : D → D → Type u_3
CD : D → Type w
inst✝³ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝² : ConcreteCategory D FD
inst✝¹ : HasForget₂ C D
inst✝ : (forget C).PreservesMonomorphisms
⊢ (forget₂ C D ⋙ forget D).PreservesMonomorphisms

Tactic:
simp only [HasForget₂.forget_comp]

Goal state after:
C✝ : Type u
inst✝¹⁰ : Category.{v, u} C✝
FC✝ : C✝ → C✝ → Type u_1
CC✝ : C✝ → Type w
inst✝⁹ : (X Y : C✝) → FunLike (FC✝ X Y) (CC✝ X) (CC✝ Y)
inst✝⁸ : ConcreteCategory C✝ FC✝
C : Type u
D : Type u'
inst✝⁷ : Category.{v, u} C
inst✝⁶ : Category.{v', u'} D
FC : C → C → Type u_2
CC : C → Type w
inst✝⁵ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁴ : ConcreteCategory C FC
FD : D → D → Type u_3
CD : D → Type w
inst✝³ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝² : ConcreteCategory D FD
inst✝¹ : HasForget₂ C D
inst✝ : (forget C).PreservesMonomorphisms
⊢ (forget C).PreservesMonomorphisms
Module: Mathlib.CategoryTheory.ConcreteCategory.EpiMono

Goal state before:
pp: C✝ : Type u
inst✝¹⁰ : Category.{v, u} C✝
FC✝ : C✝ → C✝ → Type u_1
CC✝ : C✝ → Type w
inst✝⁹ : (X Y : C✝) → FunLike (FC✝ X Y) (CC✝ X) (CC✝ Y)
inst✝⁸ : ConcreteCategory C✝ FC✝
C : Type u
D : Type u'
inst✝⁷ : Category.{v, u} C
inst✝⁶ : Category.{v', u'} D
FC : C → C → Type u_2
CC : C → Type w
inst✝⁵ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁴ : ConcreteCategory C FC
FD : D → D → Type u_3
CD : D → Type w
inst✝³ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝² : ConcreteCategory D FD
inst✝¹ : HasForget₂ C D
inst✝ : (forget C).PreservesEpimorphisms
⊢ (forget₂ C D ⋙ forget D).PreservesEpimorphisms

Tactic:
simp only [HasForget₂.forget_comp]

Goal state after:
C✝ : Type u
inst✝¹⁰ : Category.{v, u} C✝
FC✝ : C✝ → C✝ → Type u_1
CC✝ : C✝ → Type w
inst✝⁹ : (X Y : C✝) → FunLike (FC✝ X Y) (CC✝ X) (CC✝ Y)
inst✝⁸ : ConcreteCategory C✝ FC✝
C : Type u
D : Type u'
inst✝⁷ : Category.{v, u} C
inst✝⁶ : Category.{v', u'} D
FC : C → C → Type u_2
CC : C → Type w
inst✝⁵ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁴ : ConcreteCategory C FC
FD : D → D → Type u_3
CD : D → Type w
inst✝³ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝² : ConcreteCategory D FD
inst✝¹ : HasForget₂ C D
inst✝ : (forget C).PreservesEpimorphisms
⊢ (forget C).PreservesEpimorphisms
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
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : G.LaxMonoidal
X✝ Y✝ x✝¹ : C
x✝ : X✝ ⟶ Y✝
⊢ (adj.homEquiv (x✝¹ ⊗ X✝) (F.obj x✝¹ ⊗ F.obj Y✝)).symm
      ((adj.unit.app x✝¹ ⊗ₘ adj.unit.app X✝) ≫ G.obj (F.obj x✝¹) ◁ G.map (F.map x✝) ≫ μ G (F.obj x✝¹) (F.obj Y✝)) =
    (adj.homEquiv (x✝¹ ⊗ X✝) (F.obj x✝¹ ⊗ F.obj Y✝)).symm
      (x✝¹ ◁ x✝ ≫ (adj.unit.app x✝¹ ⊗ₘ adj.unit.app Y✝) ≫ μ G (F.obj x✝¹) (F.obj Y✝))

Tactic:
simp [← id_tensorHom]

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

Goal state before:
pp: case ε
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : MonoidalCategory C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : MonoidalCategory D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
inst✝¹ : MonoidalCategory E
C' : Type u₁'
inst✝ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
x✝ : G.LaxMonoidal
⊢ ε G = ε G

pp: case μ
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : MonoidalCategory C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : MonoidalCategory D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
inst✝¹ : MonoidalCategory E
C' : Type u₁'
inst✝ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
x✝² : G.LaxMonoidal
x✝¹ x✝ : D
⊢ μ G x✝¹ x✝ = μ G x✝¹ x✝

Tactic:
· simp

Goal state after:
case μ
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : MonoidalCategory C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : MonoidalCategory D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
inst✝¹ : MonoidalCategory E
C' : Type u₁'
inst✝ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
x✝² : G.LaxMonoidal
x✝¹ x✝ : D
⊢ μ G x✝¹ x✝ = μ G x✝¹ x✝
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: case η
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : MonoidalCategory C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : MonoidalCategory D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
inst✝¹ : MonoidalCategory E
C' : Type u₁'
inst✝ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
x✝ : F.OplaxMonoidal
⊢ η F = η F

pp: case δ
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : MonoidalCategory C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : MonoidalCategory D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
inst✝¹ : MonoidalCategory E
C' : Type u₁'
inst✝ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
x✝² : F.OplaxMonoidal
x✝¹ x✝ : C
⊢ δ F x✝¹ x✝ = δ F x✝¹ x✝

Tactic:
· simp

Goal state after:
case δ
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : MonoidalCategory C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : MonoidalCategory D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
inst✝¹ : MonoidalCategory E
C' : Type u₁'
inst✝ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
x✝² : F.OplaxMonoidal
x✝¹ x✝ : C
⊢ δ F x✝¹ x✝ = δ F x✝¹ x✝
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
r : R
⊢ colimit.desc (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) ((forget₂ (ModuleCat R) AddCommGrpCat).mapCocone s) ≫
      s.pt.smul r =
    (colimitCocone F).pt.smul r ≫
      colimit.desc (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) ((forget₂ (ModuleCat R) AddCommGrpCat).mapCocone s)

Tactic:
apply colimit.hom_ext

Goal state after:
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
r : R
⊢ ∀ (j : J),
    colimit.ι (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) j ≫
        colimit.desc (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) ((forget₂ (ModuleCat R) AddCommGrpCat).mapCocone s) ≫
          s.pt.smul r =
      colimit.ι (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) j ≫
        (colimitCocone F).pt.smul r ≫
          colimit.desc (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) ((forget₂ (ModuleCat R) AddCommGrpCat).mapCocone s)
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
m : (colimitCocone F).pt ⟶ s.pt
hm : ∀ (j : J), (colimitCocone F).ι.app j ≫ m = s.ι.app j
⊢ (forget₂ (ModuleCat R) AddCommGrpCat).map m =
    (forget₂ (ModuleCat R) AddCommGrpCat).map
      (homMk
        (colimit.desc (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) ((forget₂ (ModuleCat R) AddCommGrpCat).mapCocone s)) ⋯)

Tactic:
apply colimit.hom_ext

Goal state after:
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
m : (colimitCocone F).pt ⟶ s.pt
hm : ∀ (j : J), (colimitCocone F).ι.app j ≫ m = s.ι.app j
⊢ ∀ (j : J),
    colimit.ι (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) j ≫ (forget₂ (ModuleCat R) AddCommGrpCat).map m =
      colimit.ι (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) j ≫
        (forget₂ (ModuleCat R) AddCommGrpCat).map
          (homMk
            (colimit.desc (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) ((forget₂ (ModuleCat R) AddCommGrpCat).mapCocone s))
            ⋯)
Module: Mathlib.Algebra.Category.Grp.Colimits

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
h : Function.Bijective ⇑(Quot.desc F c)
s : Cocone F
j : J
x : ↑(F.obj j)
⊢ (Quot.desc F s) ((AddEquiv.ofBijective (Quot.desc F c) h).symm ((Quot.desc F c) ((Quot.ι F j) x))) =
    (Hom.hom (s.ι.app j)) x

Tactic:
← AddEquiv.ofBijective_apply _ h,

Goal state after:
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
h : Function.Bijective ⇑(Quot.desc F c)
s : Cocone F
j : J
x : ↑(F.obj j)
⊢ (Quot.desc F s)
      ((AddEquiv.ofBijective (Quot.desc F c) h).symm ((AddEquiv.ofBijective (Quot.desc F c) h) ((Quot.ι F j) x))) =
    (Hom.hom (s.ι.app j)) x
Module: Mathlib.Algebra.Category.Grp.Colimits

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
h : Function.Bijective ⇑(Quot.desc F c)
s : Cocone F
m : c.pt ⟶ s.pt
hm : ∀ (j : J), c.ι.app j ≫ m = s.ι.app j
x : Quot F
⊢ (Hom.hom m) ((Quot.desc F c) x) = (Quot.desc F s) ((AddEquiv.ofBijective (Quot.desc F c) h).symm ((Quot.desc F c) x))

Tactic:
← AddEquiv.ofBijective_apply _ h,

Goal state after:
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
h : Function.Bijective ⇑(Quot.desc F c)
s : Cocone F
m : c.pt ⟶ s.pt
hm : ∀ (j : J), c.ι.app j ≫ m = s.ι.app j
x : Quot F
⊢ (Hom.hom m) ((AddEquiv.ofBijective (Quot.desc F c) h) x) =
    (Quot.desc F s) ((AddEquiv.ofBijective (Quot.desc F c) h).symm ((AddEquiv.ofBijective (Quot.desc F c) h) x))
Module: Mathlib.CategoryTheory.Adjunction.Mates

Goal state before:
pp: C : Type u₁
D : Type u₂
E : Type u₃
F : Type u₄
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} E
inst✝ : Category.{v₄, u₄} F
G : C ⥤ E
H : D ⥤ F
L₁ : C ⥤ D
R₁ : D ⥤ C
L₂ : E ⥤ F
R₂ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : TwoSquare R₁ H G R₂
d : D
⊢ L₂.map (((mateEquiv adj₁ adj₂).toFun ((mateEquiv adj₁ adj₂).invFun α)).app d) ≫ adj₂.counit.app (H.obj d) =
    ((mateEquiv adj₁ adj₂).symm α).app (R₁.obj d) ≫ H.map (adj₁.counit.app d)

Tactic:
exact (mateEquiv_counit adj₁ adj₂ ((mateEquiv adj₁ adj₂).symm α) d)

Goal state after:
Module: Mathlib.RingTheory.Congruence.Hom

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : NonAssocSemiring M
inst✝¹ : NonAssocSemiring N
inst✝ : NonAssocSemiring P
f : M →+* N
g : N →+* P
x y : M
⊢ (ker (g.comp f)) x y ↔ ((ker g).comap f) x y

Tactic:
simp [ker_apply, comap_rel]

Goal state after:
Module: Mathlib.RingTheory.Congruence.Hom

Goal state before:
pp: case refl
M : Type u_1
N : Type u_2
inst✝¹ : NonAssocSemiring M
inst✝ : NonAssocSemiring N
c : RingCon M
f : M →+* N
h : ker f ≤ c
hf : Surjective ⇑f
this : Equivalence (Relation.Map ⇑c.toSetoid ⇑f ⇑f)
i✝¹ i✝ x : N
⊢ Relation.Map (⇑c) (⇑f) (⇑f) x x

Tactic:
| refl x =>

Goal state after:
Module: Mathlib.RingTheory.Congruence.Hom

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : NonAssocSemiring M
inst✝ : NonAssocSemiring N
c : RingCon M
f : M →+* N
h : ker f ≤ c
hf : Surjective ⇑f
x y : M
⊢ c x y → ∃ a b, c a b ∧ f a = f x ∧ f b = f y

Tactic:
by grind

Goal state after:
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : AddMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
n✝ : ℕ
h : x.snd <• x.fst = x.fst •> x.snd
n : ℕ
⊢ ∀ x_1 ∈ List.map (fun i ↦ x.fst ^ (n - i + i) •> x.snd) (List.range n.succ), x_1 = x.fst ^ n •> x.snd

Tactic:
by grind

Goal state after:
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝⁴ : AddCommGroup M
inst✝³ : Semiring R
inst✝² : Module Rᵐᵒᵖ M
inst✝¹ : Module R M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
r : R
⊢ IsUnit (inl r).fst ↔ IsUnit r

Tactic:
fst_inl

Goal state after:
R : Type u
M : Type v
inst✝⁴ : AddCommGroup M
inst✝³ : Semiring R
inst✝² : Module Rᵐᵒᵖ M
inst✝¹ : Module R M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
r : R
⊢ IsUnit r ↔ IsUnit r
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: case h1
R : Type u
M : Type v
inst✝³ : DivisionSemiring R
inst✝² : AddCommGroup M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : Module R M
r : R
⊢ r⁻¹ = (inl r⁻¹).fst

Tactic:
fst_inl

Goal state after:
case h1
R : Type u
M : Type v
inst✝³ : DivisionSemiring R
inst✝² : AddCommGroup M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : Module R M
r : R
⊢ r⁻¹ = r⁻¹