mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Filtered.Basic

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
h : ∀ {J : Type w} [inst : SmallCategory J] [FinCategory J] (F : J ⥤ C), Nonempty (Cocone F)
this : Nonempty C
X Y : C
f g : X ⟶ Y
c : Cocone (ULiftHom.down ⋙ ULift.downFunctor ⋙ parallelPair f g)
⊢ ∃ Z h, f ≫ h = g ≫ h

Tactic:
refine ⟨c.pt, c.ι.app ⟨WalkingParallelPair.one⟩, ?_⟩

Goal state after:
case refine_2
C : Type u
inst✝ : Category.{v, u} C
h : ∀ {J : Type w} [inst : SmallCategory J] [FinCategory J] (F : J ⥤ C), Nonempty (Cocone F)
this : Nonempty C
X Y : C
f g : X ⟶ Y
c : Cocone (ULiftHom.down ⋙ ULift.downFunctor ⋙ parallelPair f g)
⊢ f ≫ c.ι.app { down := WalkingParallelPair.one } = g ≫ c.ι.app { down := WalkingParallelPair.one }
Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse

Goal state before:
pp: n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A B : Matrix n n R
hAB : A * B = 1
h0 : 1 + (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B) = detp 1 A * detp 1 B + detp (-1) A * detp (-1) B
h : detp 1 B • A + adjp (-1) B = detp (-1) B • A + adjp 1 B
⊢ A + (detp 1 A • adjp (-1) B + detp (-1) A • adjp 1 B) = detp 1 A • adjp 1 B + detp (-1) A • adjp (-1) B

Tactic:
replace h := congr(detp 1 A • $h + detp (-1) A • $h.symm)

Goal state after:
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A B : Matrix n n R
hAB : A * B = 1
h0 : 1 + (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B) = detp 1 A * detp 1 B + detp (-1) A * detp (-1) B
h :
  detp 1 A • (detp 1 B • A + adjp (-1) B) + detp (-1) A • (detp (-1) B • A + adjp 1 B) =
    detp 1 A • (detp (-1) B • A + adjp 1 B) + detp (-1) A • (detp 1 B • A + adjp (-1) B)
⊢ A + (detp 1 A • adjp (-1) B + detp (-1) A • adjp 1 B) = detp 1 A • adjp 1 B + detp (-1) A • adjp (-1) B
Module: Mathlib.Algebra.Category.MonCat.FilteredColimits

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
t : Cocone F
m : (colimitCocone F).pt ⟶ t.pt
h : ∀ (j : J), (colimitCocone F).ι.app j ≫ m = t.ι.app j
y : ↑(colimitCocone F).pt
⊢ (ConcreteCategory.hom m) y = (ConcreteCategory.hom (colimitDesc F t)) y

Tactic:
obtain ⟨j, y, rfl⟩ := Functor.ιColimitType_jointly_surjective _ y
    exact ConcreteCategory.congr_hom (h j) y

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✝
⊢ (shrinkYoneda.{w, v, u} ⋙ (evaluation Cᵒᵖ (Type w)).obj Y ⋙ uliftFunctor.{v, w}).map f ≫
      (Equiv.ulift.trans (shrinkYonedaObjObjEquiv.trans Equiv.ulift.symm)).toIso.hom =
    (Equiv.ulift.trans (shrinkYonedaObjObjEquiv.trans Equiv.ulift.symm)).toIso.hom ≫
      (coyoneda.obj Y ⋙ uliftFunctor.{w, v}).map f

Tactic:
by
      ext ⟨g⟩
      obtain ⟨g, rfl⟩ := shrinkYonedaObjObjEquiv.symm.surjective g
      simp [shrinkYoneda_map_app_shrinkYonedaObjObjEquiv_symm]

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✝ Y✝ : Cᵒᵖ
f : shrinkCoyoneda.{w, v, u}.obj X✝ ⟶ shrinkCoyoneda.{w, v, u}.obj Y✝
⊢ shrinkCoyoneda.{w, v, u}.map (shrinkCoyonedaObjObjEquiv (shrinkCoyonedaEquiv f)).op = f

Tactic:
by
    obtain ⟨f, rfl⟩ := shrinkCoyonedaEquiv.symm.surjective f
    cat_disch

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)).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

Tactic:
← cancel_mono ((α_ W X Y).inv ▷ Z)

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).inv ▷ Z =
    ((α_ W X (Y ⊗ Z)).inv ≫ (α_ (W ⊗ X) Y Z).inv ≫ (α_ W X Y).hom ▷ Z) ≫ (α_ W X Y).inv ▷ Z
Module: Mathlib.Algebra.Category.Ring.Limits

Goal state before:
pp: J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ RingCat
inst✝ : Small.{u, max u v} ↑(F ⋙ forget RingCat).sections
x✝ : Small.{u, max u v} ↑((F ⋙ forget₂ RingCat AddCommGrpCat) ⋙ forget AddCommGrpCat).sections :=
  forget₂AddCommGroupPreservesLimitsAux._proof_1 F
⊢ IsLimit ((forget₂ RingCat AddCommGrpCat).mapCone (limitCone F))

Tactic:
apply AddCommGrpCat.limitConeIsLimit.{v, u} _

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 : C
T : D
⊢ (δ F X Y ≫ μ F X Y) ▷ T = 𝟙 (F.obj (X ⊗ Y) ⊗ T)

Tactic:
δ_μ,

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 : C
T : D
⊢ 𝟙 (F.obj (X ⊗ Y)) ▷ T = 𝟙 (F.obj (X ⊗ Y) ⊗ T)
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 : C
T : D
⊢ T ◁ (δ F X Y ≫ μ F X Y) = 𝟙 (T ⊗ F.obj (X ⊗ Y))

Tactic:
δ_μ,

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 : C
T : D
⊢ T ◁ 𝟙 (F.obj (X ⊗ Y)) = 𝟙 (T ⊗ F.obj (X ⊗ Y))
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) Z

Tactic:
δ_μ,

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.obj ((X ⊗ Y) ⊗ Z))
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
x✝¹ x✝ : SemimoduleCat R
⊢ (x✝¹.braiding x✝).hom ≫ (x✝.braiding x✝¹).hom = 𝟙 (x✝¹ ⊗ x✝)

Tactic:
ext : 1
    apply TensorProduct.ext'
    cat_disch

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
m : (coconeLeftOpOfCone c).pt ⟶ s.pt
w : ∀ (j : Jᵒᵖ), (coconeLeftOpOfCone c).ι.app j ≫ m = s.ι.app j
⊢ m = (hc.lift (coneOfCoconeLeftOp s)).unop

Tactic:
refine Quiver.Hom.op_inj (hc.hom_ext fun j => Quiver.Hom.unop_inj ?_)
    simpa only [Quiver.Hom.op_unop, IsLimit.fac, coneOfCoconeLeftOp_π_app] using! w (op j)

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
⊢ HasWidePullbacks Cᵒᵖ ↔ HasWidePushouts C

Tactic:
refine ⟨fun h ι ↦ ?_, fun _ ↦ inferInstance⟩
  rw [← hasLimitsOfShape_opposite_opposite_iff]
  exact hasLimitsOfShape_of_equivalence (widePushoutShapeOpEquiv _).symm

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic

Goal state before:
pp: case a.a.a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ Y₁ Y₂ U₁ U₂ V₁ V₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : U₁ ⟶ V₁
g₂ : U₂ ⟶ V₂
| f₁ ≫ 𝟙 Y₁ ⊗ₘ (f₂ ⊗ₘ g₁ ⊗ₘ g₂) ≫ (α_ Y₂ V₁ V₂).inv

pp: case a.a.a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ Y₁ Y₂ U₁ U₂ V₁ V₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : U₁ ⟶ V₁
g₂ : U₂ ⟶ V₂
| 𝟙 Y₁ ⊗ₘ (β_ Y₂ V₁).hom ⊗ₘ 𝟙 V₂

pp: case a.a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ Y₁ Y₂ U₁ U₂ V₁ V₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : U₁ ⟶ V₁
g₂ : U₂ ⟶ V₂
| 𝟙 Y₁ ⊗ₘ (α_ V₁ Y₂ V₂).hom

pp: case a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ Y₁ Y₂ U₁ U₂ V₁ V₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : U₁ ⟶ V₁
g₂ : U₂ ⟶ V₂
| (α_ Y₁ V₁ (Y₂ ⊗ V₂)).inv

pp: case a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ Y₁ Y₂ U₁ U₂ V₁ V₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : U₁ ⟶ V₁
g₂ : U₂ ⟶ V₂
| (α_ X₁ X₂ (U₁ ⊗ U₂)).hom

Tactic:
comp_id f₁,

Goal state after:
case a.a.a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ Y₁ Y₂ U₁ U₂ V₁ V₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : U₁ ⟶ V₁
g₂ : U₂ ⟶ V₂
| f₁ ⊗ₘ (f₂ ⊗ₘ g₁ ⊗ₘ g₂) ≫ (α_ Y₂ V₁ V₂).inv

case a.a.a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ Y₁ Y₂ U₁ U₂ V₁ V₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : U₁ ⟶ V₁
g₂ : U₂ ⟶ V₂
| 𝟙 Y₁ ⊗ₘ (β_ Y₂ V₁).hom ⊗ₘ 𝟙 V₂

case a.a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ Y₁ Y₂ U₁ U₂ V₁ V₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : U₁ ⟶ V₁
g₂ : U₂ ⟶ V₂
| 𝟙 Y₁ ⊗ₘ (α_ V₁ Y₂ V₂).hom

case a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ Y₁ Y₂ U₁ U₂ V₁ V₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : U₁ ⟶ V₁
g₂ : U₂ ⟶ V₂
| (α_ Y₁ V₁ (Y₂ ⊗ V₂)).inv

case a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ Y₁ Y₂ U₁ U₂ V₁ V₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : U₁ ⟶ V₁
g₂ : U₂ ⟶ V₂
| (α_ X₁ X₂ (U₁ ⊗ U₂)).hom
Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic

Goal state before:
pp: case a.a.a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ Y₁ Y₂ U₁ U₂ V₁ V₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : U₁ ⟶ V₁
g₂ : U₂ ⟶ V₂
| f₁ ≫ 𝟙 Y₁ ⊗ₘ (f₂ ⊗ₘ g₁) ≫ (β_ Y₂ V₁).hom ⊗ₘ g₂ ≫ 𝟙 V₂

pp: case a.a.a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ Y₁ Y₂ U₁ U₂ V₁ V₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : U₁ ⟶ V₁
g₂ : U₂ ⟶ V₂
| 𝟙 Y₁ ⊗ₘ (α_ V₁ Y₂ V₂).hom

pp: case a.a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ Y₁ Y₂ U₁ U₂ V₁ V₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : U₁ ⟶ V₁
g₂ : U₂ ⟶ V₂
| (α_ Y₁ V₁ (Y₂ ⊗ V₂)).inv

pp: case a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ Y₁ Y₂ U₁ U₂ V₁ V₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : U₁ ⟶ V₁
g₂ : U₂ ⟶ V₂
| (α_ X₁ X₂ (U₁ ⊗ U₂)).hom

pp: case a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ Y₁ Y₂ U₁ U₂ V₁ V₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : U₁ ⟶ V₁
g₂ : U₂ ⟶ V₂
| 𝟙 X₁ ⊗ₘ (α_ X₂ U₁ U₂).inv

Tactic:
comp_id f₁,

Goal state after:
case a.a.a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ Y₁ Y₂ U₁ U₂ V₁ V₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : U₁ ⟶ V₁
g₂ : U₂ ⟶ V₂
| f₁ ⊗ₘ (f₂ ⊗ₘ g₁) ≫ (β_ Y₂ V₁).hom ⊗ₘ g₂ ≫ 𝟙 V₂

case a.a.a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ Y₁ Y₂ U₁ U₂ V₁ V₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : U₁ ⟶ V₁
g₂ : U₂ ⟶ V₂
| 𝟙 Y₁ ⊗ₘ (α_ V₁ Y₂ V₂).hom

case a.a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ Y₁ Y₂ U₁ U₂ V₁ V₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : U₁ ⟶ V₁
g₂ : U₂ ⟶ V₂
| (α_ Y₁ V₁ (Y₂ ⊗ V₂)).inv

case a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ Y₁ Y₂ U₁ U₂ V₁ V₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : U₁ ⟶ V₁
g₂ : U₂ ⟶ V₂
| (α_ X₁ X₂ (U₁ ⊗ U₂)).hom

case a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ Y₁ Y₂ U₁ U₂ V₁ V₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : U₁ ⟶ V₁
g₂ : U₂ ⟶ V₂
| 𝟙 X₁ ⊗ₘ (α_ X₂ U₁ U₂).inv
Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic

Goal state before:
pp: case a.a.a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ Y₁ Y₂ U₁ U₂ V₁ V₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : U₁ ⟶ V₁
g₂ : U₂ ⟶ V₂
| f₁ ≫ 𝟙 Y₁ ⊗ₘ ((g₁ ⊗ₘ f₂) ⊗ₘ g₂) ≫ (α_ V₁ Y₂ V₂).hom

pp: case a.a.a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ Y₁ Y₂ U₁ U₂ V₁ V₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : U₁ ⟶ V₁
g₂ : U₂ ⟶ V₂
| (α_ Y₁ V₁ (Y₂ ⊗ V₂)).inv

pp: case a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ Y₁ Y₂ U₁ U₂ V₁ V₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : U₁ ⟶ V₁
g₂ : U₂ ⟶ V₂
| (α_ X₁ X₂ (U₁ ⊗ U₂)).hom

pp: case a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ Y₁ Y₂ U₁ U₂ V₁ V₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : U₁ ⟶ V₁
g₂ : U₂ ⟶ V₂
| 𝟙 X₁ ⊗ₘ (α_ X₂ U₁ U₂).inv

pp: case a.a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ Y₁ Y₂ U₁ U₂ V₁ V₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : U₁ ⟶ V₁
g₂ : U₂ ⟶ V₂
| 𝟙 X₁ ⊗ₘ (β_ X₂ U₁).hom ⊗ₘ 𝟙 U₂

Tactic:
comp_id f₁,

Goal state after:
case a.a.a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ Y₁ Y₂ U₁ U₂ V₁ V₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : U₁ ⟶ V₁
g₂ : U₂ ⟶ V₂
| f₁ ⊗ₘ ((g₁ ⊗ₘ f₂) ⊗ₘ g₂) ≫ (α_ V₁ Y₂ V₂).hom

case a.a.a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ Y₁ Y₂ U₁ U₂ V₁ V₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : U₁ ⟶ V₁
g₂ : U₂ ⟶ V₂
| (α_ Y₁ V₁ (Y₂ ⊗ V₂)).inv

case a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ Y₁ Y₂ U₁ U₂ V₁ V₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : U₁ ⟶ V₁
g₂ : U₂ ⟶ V₂
| (α_ X₁ X₂ (U₁ ⊗ U₂)).hom

case a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ Y₁ Y₂ U₁ U₂ V₁ V₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : U₁ ⟶ V₁
g₂ : U₂ ⟶ V₂
| 𝟙 X₁ ⊗ₘ (α_ X₂ U₁ U₂).inv

case a.a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ Y₁ Y₂ U₁ U₂ V₁ V₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : U₁ ⟶ V₁
g₂ : U₂ ⟶ V₂
| 𝟙 X₁ ⊗ₘ (β_ X₂ U₁).hom ⊗ₘ 𝟙 U₂
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 G : C ⥤ D
inst✝ : F.Monoidal
i : F ≅ G
X : C
⊢ (ρ_ (G.obj X)).hom =
    G.obj X ◁ (εIso F ≪≫ i.app (𝟙_ C)).hom ≫
      ((i.symm.app X ⊗ᵢ i.symm.app (𝟙_ C)) ≪≫ μIso F X (𝟙_ C) ≪≫ i.app (X ⊗ 𝟙_ C)).hom ≫ G.map (ρ_ X).hom

Tactic:
simp only [Iso.trans_hom, εIso_hom, Iso.app_hom, ← id_tensorHom, tensorIso_hom, Iso.symm_hom,
      μIso_hom, Category.assoc, tensorHom_comp_tensorHom_assoc, Category.id_comp,
      Iso.hom_inv_id_app, Category.comp_id]

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
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F G : C ⥤ D
inst✝ : F.Monoidal
i : F ≅ G
X : C
⊢ (ρ_ (G.obj X)).hom =
    (i.inv.app X ⊗ₘ LaxMonoidal.ε F) ≫ LaxMonoidal.μ F X (𝟙_ C) ≫ i.hom.app (X ⊗ 𝟙_ C) ≫ G.map (ρ_ X).hom
Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
i : SymmetricCategory C
⊢ (fun X Y ↦ (β_ Y X).symm) = β_

Tactic:
funext X Y

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
i : SymmetricCategory C
X Y : C
⊢ (β_ Y X).symm = β_ X Y
Module: Mathlib.LinearAlgebra.TensorAlgebra.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : R
⊢ algebraMapInv ((algebraMap R (TensorAlgebra R M)) x) = x

Tactic:
by
  simp [algebraMapInv]

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

Goal state before:
pp: R' : Type u
M : Type v
inst✝⁸ : CommSemiring R'
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R' M
inst✝⁵ : Module R'ᵐᵒᵖ M
inst✝⁴ : IsCentralScalar R' M
N : Type u_3
inst✝³ : AddCommMonoid N
inst✝² : Module R' N
inst✝¹ : Module R'ᵐᵒᵖ N
inst✝ : IsCentralScalar R' N
f : M →ₗ[R'] N
r : R'
⊢ (Algebra.ofId R' (tsze R' N)) r = inl r

Tactic:
Algebra.ofId_apply,

Goal state after:
R' : Type u
M : Type v
inst✝⁸ : CommSemiring R'
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R' M
inst✝⁵ : Module R'ᵐᵒᵖ M
inst✝⁴ : IsCentralScalar R' M
N : Type u_3
inst✝³ : AddCommMonoid N
inst✝² : Module R' N
inst✝¹ : Module R'ᵐᵒᵖ N
inst✝ : IsCentralScalar R' N
f : M →ₗ[R'] N
r : R'
⊢ (algebraMap R' (tsze R' N)) r = inl r
Module: Mathlib.Algebra.Ring.BooleanRing

Goal state before:
pp: α : Type u_1
inst✝ : BooleanRing α
a b : α
⊢ a ⊔ b = b ⊔ a

Tactic:
dsimp only [(· ⊔ ·)]
  ring

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

Goal state before:
pp: α : Type u_1
inst✝ : BooleanRing α
a b c : α
⊢ a ⊔ b ⊔ c = a ⊔ (b ⊔ c)

Tactic:
dsimp only [(· ⊔ ·)]
  ring

Goal state after:
Module: Mathlib.RingTheory.Bialgebra.TensorProduct

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
D : Type u_6
inst✝¹⁴ : CommSemiring R
inst✝¹³ : CommSemiring S
inst✝¹² : Semiring A
inst✝¹¹ : Semiring B
inst✝¹⁰ : Bialgebra S A
inst✝⁹ : Bialgebra R B
inst✝⁸ : Algebra R A
inst✝⁷ : Algebra R S
inst✝⁶ : IsScalarTower R S A
inst✝⁵ : Semiring C
inst✝⁴ : Semiring D
inst✝³ : Bialgebra S C
inst✝² : Bialgebra R D
inst✝¹ : Algebra R C
inst✝ : IsScalarTower R S C
x y : A ⊗[R] R
⊢ (Coalgebra.TensorProduct.rid R S A).toFun (x * y) =
    (Coalgebra.TensorProduct.rid R S A).toFun x * (Coalgebra.TensorProduct.rid R S A).toFun y

Tactic:
by
    simp only [CoalgEquiv.toCoalgHom_eq_coe, CoalgHom.toLinearMap_eq_coe, AddHom.toFun_eq_coe,
      LinearMap.coe_toAddHom, CoalgHom.coe_toLinearMap, CoalgHom.coe_coe,
      coalgebra_rid_eq_algebra_rid_apply, map_mul]

Goal state after:
Module: Mathlib.Order.Heyting.Hom

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝² : FunLike F α β
inst✝¹ : CoheytingAlgebra α
x✝ : CoheytingAlgebra β
inst✝ : CoheytingHomClass F α β
f : F
⊢ f (⊤ \ ⊤) = ?m.32 \ ?m.32

pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝² : FunLike F α β
inst✝¹ : CoheytingAlgebra α
x✝ : CoheytingAlgebra β
inst✝ : CoheytingHomClass F α β
f : F
⊢ β

Tactic:
map_sdiff

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝² : FunLike F α β
inst✝¹ : CoheytingAlgebra α
x✝ : CoheytingAlgebra β
inst✝ : CoheytingHomClass F α β
f : F
⊢ f ⊤ \ f ⊤ = ?m.32 \ ?m.32

F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝² : FunLike F α β
inst✝¹ : CoheytingAlgebra α
x✝ : CoheytingAlgebra β
inst✝ : CoheytingHomClass F α β
f : F
⊢ β
Module: Mathlib.Order.Heyting.Hom

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : FunLike F α β
inst✝² : HeytingAlgebra α
inst✝¹ : HeytingAlgebra β
inst✝ : HeytingHomClass F α β
f : F
a b : α
⊢ f (a ⇔ b) = f a ⇔ f b

Tactic:
by simp_rw [bihimp, map_inf, map_himp]

Goal state after:
Module: Mathlib.Order.Heyting.Hom

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : FunLike F α β
inst✝² : CoheytingAlgebra α
inst✝¹ : CoheytingAlgebra β
inst✝ : CoheytingHomClass F α β
f : F
a b : α
⊢ f (a \ b) ⊔ f (b \ a) = f a \ f b ⊔ f b \ f a

Tactic:
map_sdiff

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

Goal state before:
pp: case succ.mpr
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)
b : R
hb : b ≠ 0
u : Multiset R
hu : normalizedFactors b = replicate (n + 1) (normalize a) + u
⊢ a ^ (n + 1) ∣ (replicate (n + 1) (normalize a)).prod * u.prod

Tactic:
prod_replicate

Goal state after:
case succ.mpr
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)
b : R
hb : b ≠ 0
u : Multiset R
hu : normalizedFactors b = replicate (n + 1) (normalize a) + u
⊢ a ^ (n + 1) ∣ normalize a ^ (n + 1) * u.prod
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity

Goal state before:
pp: case pos
R : Type u_2
inst✝¹ : CommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a b : R
ha : a ≠ 0
h : ∀ (p : R), Prime p → emultiplicity p a ≤ emultiplicity p b
hb : ¬b = 0
this : StrongNormalizationMonoid R := UniqueFactorizationMonoid.strongNormalizationMonoid
q : R
hq : q ∈ normalizedFactors a
hqprime : Prime q
h1 : emultiplicity q a = ↑(Multiset.count q (normalizedFactors a))
h2 : emultiplicity q b = ↑(Multiset.count q (normalizedFactors b))
⊢ Multiset.count q (normalizedFactors a) ≤ Multiset.count q (normalizedFactors b)

Tactic:
simpa [h1, h2] using h q hqprime

Goal state after:
Module: Mathlib.RingTheory.TwoSidedIdeal.Operations

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
I : TwoSidedIdeal R
h : s ⊆ ↑I
t : Set R
⊢ t * s ⊆ ↑I

Tactic:
by
  rintro - ⟨r, -, x, hx, rfl⟩
  exact mul_mem_left _ _ _ (h hx)

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
s : Set R
span_eq : Ideal.span s = ⊤
x y : R
eq : (algebraMap R ((a : ↑s) → Away ↑a)) x = (algebraMap R ((a : ↑s) → Away ↑a)) y
this : Module.eqIdeal R x y = ⊤
⊢ x = y

Tactic:
simpa [Module.eqIdeal] using (Ideal.eq_top_iff_one _).mp this

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
s : Set R
f : (a : ↑s) → Away ↑a
h : ∀ (a b : ↑s), (Away.awayToAwayRight ↑a ↑b) (f a) = (Away.awayToAwayLeft ↑b ↑a) (f b)
mem : 1 ∈ Ideal.span s
finset_eq : ∃ t, ↑t = s
span_eq : Ideal.span s = ⊤
⊢ ∃ x, ∀ (a : ↑s), (algebraMap R (Away ↑a)) x = f a

Tactic:
obtain ⟨s, rfl⟩ := finset_eq

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
s : Finset R
f : (a : ↑↑s) → Away ↑a
h : ∀ (a b : ↑↑s), (Away.awayToAwayRight ↑a ↑b) (f a) = (Away.awayToAwayLeft ↑b ↑a) (f b)
mem : 1 ∈ Ideal.span ↑s
span_eq : Ideal.span ↑s = ⊤
⊢ ∃ x, ∀ (a : ↑↑s), (algebraMap R (Away ↑a)) x = f a
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✝² : CommSemiring S
inst✝¹ : IsLocalRing S
f : R →+* S
inst✝ : IsLocalHom f
⊢ Ideal.map f (maximalIdeal R) ≤ maximalIdeal S

Tactic:
by
  rw [Ideal.map_le_iff_le_comap, IsLocalRing.maximalIdeal_comap]

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

Goal state before:
pp: case pos
R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
d : ℤ
hd : d ≤ 0
⊢ mk' B 1 (Submonoid.pow x d.natAbs) * (algebraMap R B) (x ^ (-d).natAbs) = 1

pp: case pos.hn
R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
d : ℤ
hd : d ≤ 0
⊢ 0 ≤ -d

Tactic:
Int.natAbs_neg,

Goal state after:
case pos
R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
d : ℤ
hd : d ≤ 0
⊢ mk' B 1 (Submonoid.pow x d.natAbs) * (algebraMap R B) (x ^ d.natAbs) = 1

case pos.hn
R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
d : ℤ
hd : d ≤ 0
⊢ 0 ≤ -d