mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Functor.Currying

Goal state before:
pp: case a.a
B : Type u₁
inst✝⁴ : Category.{v₁, u₁} B
C : Type u₂
inst✝³ : Category.{v₂, u₂} C
D : Type u₃
inst✝² : Category.{v₃, u₃} D
E : Type u₄
inst✝¹ : Category.{v₄, u₄} E
H : Type u₅
inst✝ : Category.{v₅, u₅} H
F : C ⥤ D ⥤ E
X✝ Y✝ Z✝ : C × D
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
| (F.map g.1).app X✝.2 ≫ (F.obj Z✝.1).map f.2

pp: case a.a
B : Type u₁
inst✝⁴ : Category.{v₁, u₁} B
C : Type u₂
inst✝³ : Category.{v₂, u₂} C
D : Type u₃
inst✝² : Category.{v₃, u₃} D
E : Type u₄
inst✝¹ : Category.{v₄, u₄} E
H : Type u₅
inst✝ : Category.{v₅, u₅} H
F : C ⥤ D ⥤ E
X✝ Y✝ Z✝ : C × D
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
| (F.obj Z✝.1).map g.2

pp: case a
B : Type u₁
inst✝⁴ : Category.{v₁, u₁} B
C : Type u₂
inst✝³ : Category.{v₂, u₂} C
D : Type u₃
inst✝² : Category.{v₃, u₃} D
E : Type u₄
inst✝¹ : Category.{v₄, u₄} E
H : Type u₅
inst✝ : Category.{v₅, u₅} H
F : C ⥤ D ⥤ E
X✝ Y✝ Z✝ : C × D
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
| (F.map f.1).app X✝.2

Tactic:
← NatTrans.naturality

Goal state after:
case a.a
B : Type u₁
inst✝⁴ : Category.{v₁, u₁} B
C : Type u₂
inst✝³ : Category.{v₂, u₂} C
D : Type u₃
inst✝² : Category.{v₃, u₃} D
E : Type u₄
inst✝¹ : Category.{v₄, u₄} E
H : Type u₅
inst✝ : Category.{v₅, u₅} H
F : C ⥤ D ⥤ E
X✝ Y✝ Z✝ : C × D
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
| (F.obj Y✝.1).map f.2 ≫ (F.map g.1).app Y✝.2

case a.a
B : Type u₁
inst✝⁴ : Category.{v₁, u₁} B
C : Type u₂
inst✝³ : Category.{v₂, u₂} C
D : Type u₃
inst✝² : Category.{v₃, u₃} D
E : Type u₄
inst✝¹ : Category.{v₄, u₄} E
H : Type u₅
inst✝ : Category.{v₅, u₅} H
F : C ⥤ D ⥤ E
X✝ Y✝ Z✝ : C × D
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
| (F.obj Z✝.1).map g.2

case a
B : Type u₁
inst✝⁴ : Category.{v₁, u₁} B
C : Type u₂
inst✝³ : Category.{v₂, u₂} C
D : Type u₃
inst✝² : Category.{v₃, u₃} D
E : Type u₄
inst✝¹ : Category.{v₄, u₄} E
H : Type u₅
inst✝ : Category.{v₅, u₅} H
F : C ⥤ D ⥤ E
X✝ Y✝ Z✝ : C × D
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
| (F.map f.1).app X✝.2
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
inst✝ : HasColimitsOfShape J C
F : J ⥤ K ⥤ C
X Y : J
f : X ⟶ Y
x : K
⊢ (F.map f).app x ≫ colimit.ι (F.flip.obj x) Y = colimit.ι (F.flip.obj x) X

Tactic:
change (F.flip.obj x).map f ≫ _ = _

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
inst✝ : HasColimitsOfShape J C
F : J ⥤ K ⥤ C
X Y : J
f : X ⟶ Y
x : K
⊢ (F.flip.obj x).map f ≫ colimit.ι (F.flip.obj x) Y = colimit.ι (F.flip.obj x) X
Module: Mathlib.CategoryTheory.Monoidal.Transport

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategoryStruct D
F : D ⥤ C
inst✝ : F.Faithful
fData : InducingFunctorData F
⊢ F.CoreMonoidal

Tactic:
letI := induced F fData

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategoryStruct D
F : D ⥤ C
inst✝ : F.Faithful
fData : InducingFunctorData F
this : MonoidalCategory D := induced F fData
⊢ F.CoreMonoidal
Module: Mathlib.CategoryTheory.Linear.LinearFunctor

Goal state before:
pp: R : Type u_1
inst✝⁷ : Semiring R
C : Type u_2
D : Type u_3
inst✝⁶ : Category.{v_1, u_2} C
inst✝⁵ : Category.{v_2, u_3} D
inst✝⁴ : Preadditive C
inst✝³ : Preadditive D
inst✝² : CategoryTheory.Linear R C
inst✝¹ : CategoryTheory.Linear R D
F G : C ⥤ D
e : F ≅ G
inst✝ : Linear R F
⊢ Linear R G

Tactic:
by
  exact
    { map_smul := fun f r => by
        simp only [← NatIso.naturality_1 e (r • f), F.map_smul, Linear.smul_comp,
          NatTrans.naturality, Linear.comp_smul, Iso.inv_hom_id_app_assoc] }

Goal state after:
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
⊢ biproduct.ι (fun j ↦ X ⊗ f j) j ≫ (leftDistributor X f).inv = X ◁ biproduct.ι f j

Tactic:
cases nonempty_fintype J
  simp [leftDistributor_inv, Preadditive.comp_sum, biproduct.ι_π_assoc, dite_comp]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
f g h : C
η : g ⟶ h
η' : g ≅ h
ih_η : η'.hom = η
⊢ (f ◁ᵢ η').hom = f ◁ η

Tactic:
simp [ih_η]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
f g h : C
η : f ⟶ g
η' : f ≅ g
ih_η : η'.hom = η
⊢ (η' ▷ᵢ h).hom = η ▷ h

Tactic:
simp [ih_η]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
f g h : C
η η' : f ⟶ g
θ θ' : g ⟶ h
ι : f ⟶ h
e_η : η = η'
e_θ : θ = θ'
e_ηθ : η' ≫ θ' = ι
⊢ η ≫ θ = ι

Tactic:
by
  simp [e_η, e_θ, e_ηθ]

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
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
F : C ⥤ D
G : C ⥤ E
inst✝¹ : F.OplaxMonoidal
inst✝ : G.OplaxMonoidal
⊢ (η (F.prod' G)).2 = η G

Tactic:
change G.map (𝟙 _) ≫ _ = _

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
F : C ⥤ D
G : C ⥤ E
inst✝¹ : F.OplaxMonoidal
inst✝ : G.OplaxMonoidal
⊢ G.map (𝟙 ((diag C).obj (𝟙_ C)).2) ≫ (η (F.prod G)).2 = η G
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
F : C ⥤ D
G : C ⥤ E
inst✝¹ : F.OplaxMonoidal
inst✝ : G.OplaxMonoidal
X Y : C
⊢ (δ (F.prod' G) X Y).2 = δ G X Y

Tactic:
change G.map (𝟙 _) ≫ _ = _

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
F : C ⥤ D
G : C ⥤ E
inst✝¹ : F.OplaxMonoidal
inst✝ : G.OplaxMonoidal
X Y : C
⊢ G.map (𝟙 ((diag C).obj (X ⊗ Y)).2) ≫ (δ (F.prod G) ((diag C).obj X) ((diag C).obj Y)).2 = δ G X Y
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
inst✝ : HasColimit F
j : J
⊢ (limitRightOpIsoOpColimit F).inv ≫ limit.π F.rightOp j = (colimit.ι F (op j)).op

Tactic:
by
  simp [limitRightOpIsoOpColimit]

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
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✝ : F.OplaxMonoidal
X Y Z : D
this :
  ∀ {X Y : D} (f : X ⟶ Y) (X' : D) {Z : D} (h : Y ⊗ X' ⟶ Z),
    F.map (G.map f) ▷ F.obj (G.obj X') ≫ (adj.counit.app Y ⊗ₘ adj.counit.app X') ≫ h =
      (adj.counit.app X ⊗ₘ adj.counit.app X') ≫ f ▷ X' ≫ h
⊢ F.map (α_ (G.obj X) (G.obj Y) (G.obj Z)).hom ≫
      δ F (G.obj X) (G.obj Y ⊗ G.obj Z) ≫
        F.obj (G.obj X) ◁ δ F (G.obj Y) (G.obj Z) ≫ (adj.counit.app X ⊗ₘ adj.counit.app Y ⊗ₘ adj.counit.app Z) =
    F.map (α_ (G.obj X) (G.obj Y) (G.obj Z)).hom ≫
      F.map (G.obj X ◁ adj.unit.app (G.obj Y ⊗ G.obj Z)) ≫
        δ F (G.obj X) (G.obj (F.obj (G.obj Y ⊗ G.obj Z))) ≫
          F.obj (G.obj X) ◁ F.map (G.map (δ F (G.obj Y) (G.obj Z))) ≫
            F.obj (G.obj X) ◁ F.map (G.map (adj.counit.app Y ⊗ₘ adj.counit.app Z)) ≫
              (adj.counit.app X ⊗ₘ adj.counit.app (Y ⊗ Z))

Tactic:
← δ_natural_right_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
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✝ : F.OplaxMonoidal
X Y Z : D
this :
  ∀ {X Y : D} (f : X ⟶ Y) (X' : D) {Z : D} (h : Y ⊗ X' ⟶ Z),
    F.map (G.map f) ▷ F.obj (G.obj X') ≫ (adj.counit.app Y ⊗ₘ adj.counit.app X') ≫ h =
      (adj.counit.app X ⊗ₘ adj.counit.app X') ≫ f ▷ X' ≫ h
⊢ F.map (α_ (G.obj X) (G.obj Y) (G.obj Z)).hom ≫
      δ F (G.obj X) (G.obj Y ⊗ G.obj Z) ≫
        F.obj (G.obj X) ◁ δ F (G.obj Y) (G.obj Z) ≫ (adj.counit.app X ⊗ₘ adj.counit.app Y ⊗ₘ adj.counit.app Z) =
    F.map (α_ (G.obj X) (G.obj Y) (G.obj Z)).hom ≫
      δ F (G.obj X) (G.obj Y ⊗ G.obj Z) ≫
        F.obj (G.obj X) ◁ F.map (adj.unit.app (G.obj Y ⊗ G.obj Z)) ≫
          F.obj (G.obj X) ◁ F.map (G.map (δ F (G.obj Y) (G.obj Z))) ≫
            F.obj (G.obj X) ◁ F.map (G.map (adj.counit.app Y ⊗ₘ adj.counit.app Z)) ≫
              (adj.counit.app X ⊗ₘ adj.counit.app (Y ⊗ Z))
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.bijective C (𝟙 X)

Tactic:
delta MorphismProperty.bijective
    convert! bijective_id
    aesop

Goal state after:
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₁ 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₁ Y₂ (V₁ ⊗ V₂)).hom ≫
        Y₁ ◁ (α_ Y₂ V₁ V₂).inv ≫ Y₁ ◁ (β_ Y₂ V₁).hom ▷ V₂ ≫ Y₁ ◁ (α_ V₁ Y₂ V₂).hom ≫ (α_ Y₁ V₁ (Y₂ ⊗ V₂)).inv =
    ((α_ X₁ X₂ (U₁ ⊗ U₂)).hom ≫
        X₁ ◁ (α_ X₂ U₁ U₂).inv ≫ X₁ ◁ (β_ X₂ U₁).hom ▷ U₂ ≫ X₁ ◁ (α_ U₁ X₂ U₂).hom ≫ (α_ X₁ U₁ (X₂ ⊗ U₂)).inv) ≫
      ((f₁ ⊗ₘ g₁) ⊗ₘ f₂ ⊗ₘ g₂)

Tactic:
simp_rw [← id_tensorHom, ← tensorHom_id]

Goal state after:
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₁ Y₂ (V₁ ⊗ V₂)).hom ≫
        (𝟙 Y₁ ⊗ₘ (α_ Y₂ V₁ V₂).inv) ≫
          (𝟙 Y₁ ⊗ₘ (β_ Y₂ V₁).hom ⊗ₘ 𝟙 V₂) ≫ (𝟙 Y₁ ⊗ₘ (α_ V₁ Y₂ V₂).hom) ≫ (α_ Y₁ V₁ (Y₂ ⊗ V₂)).inv =
    ((α_ X₁ X₂ (U₁ ⊗ U₂)).hom ≫
        (𝟙 X₁ ⊗ₘ (α_ X₂ U₁ U₂).inv) ≫
          (𝟙 X₁ ⊗ₘ (β_ X₂ U₁).hom ⊗ₘ 𝟙 U₂) ≫ (𝟙 X₁ ⊗ₘ (α_ U₁ X₂ U₂).hom) ≫ (α_ X₁ U₁ (X₂ ⊗ U₂)).inv) ≫
      ((f₁ ⊗ₘ g₁) ⊗ₘ f₂ ⊗ₘ g₂)
Module: Mathlib.CategoryTheory.Adjunction.Mates

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
D : Type u₄
E : Type u₅
F : Type u₆
inst✝⁵ : Category.{v₁, u₁} A
inst✝⁴ : Category.{v₂, u₂} B
inst✝³ : Category.{v₃, u₃} C
inst✝² : Category.{v₄, u₄} D
inst✝¹ : Category.{v₅, u₅} E
inst✝ : Category.{v₆, u₆} F
G₁ : A ⥤ C
G₂ : C ⥤ E
H₁ : B ⥤ D
H₂ : D ⥤ F
L₁ : A ⥤ B
R₁ : B ⥤ A
L₂ : C ⥤ D
R₂ : D ⥤ C
L₃ : E ⥤ F
R₃ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
α : TwoSquare G₁ L₁ L₂ H₁
β : TwoSquare G₂ L₂ L₃ H₂
b : B
⊢ adj₃.unit.app (G₂.obj (G₁.obj (R₁.obj b))) ≫
      R₃.map (β.natTrans.app (G₁.obj (R₁.obj b))) ≫
        R₃.map (H₂.map (α.natTrans.app (R₁.obj b))) ≫ R₃.map (H₂.map (H₁.map (adj₁.counit.app b))) =
    adj₃.unit.app (G₂.obj (G₁.obj (R₁.obj b))) ≫
      R₃.map
          (β.app (G₁.obj (R₁.obj b)) ≫
            (L₂ ⋙ H₂).map
              ((adj₂.unit.app (G₁.obj (R₁.obj b)) ≫ R₂.map (α.natTrans.app (R₁.obj b))) ≫
                R₂.map (H₁.map (adj₁.counit.app b)))) ≫
        R₃.map (H₂.map (adj₂.counit.app (H₁.obj b)))

Tactic:
rw [(L₂ ⋙ H₂).map_comp, R₃.map_comp, R₃.map_comp]

Goal state after:
A : Type u₁
B : Type u₂
C : Type u₃
D : Type u₄
E : Type u₅
F : Type u₆
inst✝⁵ : Category.{v₁, u₁} A
inst✝⁴ : Category.{v₂, u₂} B
inst✝³ : Category.{v₃, u₃} C
inst✝² : Category.{v₄, u₄} D
inst✝¹ : Category.{v₅, u₅} E
inst✝ : Category.{v₆, u₆} F
G₁ : A ⥤ C
G₂ : C ⥤ E
H₁ : B ⥤ D
H₂ : D ⥤ F
L₁ : A ⥤ B
R₁ : B ⥤ A
L₂ : C ⥤ D
R₂ : D ⥤ C
L₃ : E ⥤ F
R₃ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
α : TwoSquare G₁ L₁ L₂ H₁
β : TwoSquare G₂ L₂ L₃ H₂
b : B
⊢ adj₃.unit.app (G₂.obj (G₁.obj (R₁.obj b))) ≫
      R₃.map (β.natTrans.app (G₁.obj (R₁.obj b))) ≫
        R₃.map (H₂.map (α.natTrans.app (R₁.obj b))) ≫ R₃.map (H₂.map (H₁.map (adj₁.counit.app b))) =
    adj₃.unit.app (G₂.obj (G₁.obj (R₁.obj b))) ≫
      (R₃.map (β.app (G₁.obj (R₁.obj b))) ≫
          R₃.map ((L₂ ⋙ H₂).map (adj₂.unit.app (G₁.obj (R₁.obj b)) ≫ R₂.map (α.natTrans.app (R₁.obj b)))) ≫
            R₃.map ((L₂ ⋙ H₂).map (R₂.map (H₁.map (adj₁.counit.app b))))) ≫
        R₃.map (H₂.map (adj₂.counit.app (H₁.obj b)))
Module: Mathlib.CategoryTheory.Adjunction.Mates

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ L₂ L₃ : C ⥤ D
R₁ R₂ R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
α : R₁ ⟶ R₂
β : R₂ ⟶ R₃
⊢ (conjugateEquiv adj₁ adj₃) ((conjugateEquiv adj₂ adj₃).symm β ≫ (conjugateEquiv adj₁ adj₂).symm α) = α ≫ β

Tactic:
← conjugateEquiv_comp _ adj₂

Goal state after:
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ L₂ L₃ : C ⥤ D
R₁ R₂ R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
α : R₁ ⟶ R₂
β : R₂ ⟶ R₃
⊢ (conjugateEquiv adj₁ adj₂) ((conjugateEquiv adj₁ adj₂).symm α) ≫
      (conjugateEquiv adj₂ adj₃) ((conjugateEquiv adj₂ adj₃).symm β) =
    α ≫ β
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: R₁ R₂ : Type u₁
inst✝¹ : CommRing R₁
inst✝ : CommRing R₂
f₁₂ : R₁ →+* R₂
M : ModuleCat R₁
m : ↑M
⊢ (Hom.hom ((extendScalarsId R₂).hom.app ((extendScalars f₁₂).obj M)))
      ((Hom.hom ((extendScalarsComp f₁₂ (RingHom.id R₂)).hom.app M)) (1 ⊗ₜ[R₁] m)) =
    1 ⊗ₜ[R₁] m

Tactic:
erw [extendScalarsComp_hom_app_one_tmul f₁₂ (RingHom.id R₂) M m,
    extendScalarsId_hom_app_one_tmul]

Goal state after:
R₁ R₂ : Type u₁
inst✝¹ : CommRing R₁
inst✝ : CommRing R₂
f₁₂ : R₁ →+* R₂
M : ModuleCat R₁
m : ↑M
⊢ 1 ⊗ₜ[R₁] m = 1 ⊗ₜ[R₁] m
Module: Mathlib.Algebra.Ring.BooleanRing

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

Tactic:
simp only [mul_self]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Semiring A
inst✝³ : Bialgebra S A
inst✝² : Algebra R A
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R S A
⊢ (TensorProduct.rid R S A).toAlgEquiv = Algebra.TensorProduct.rid R S A

Tactic:
by
  ext x
  exact coalgebra_rid_eq_algebra_rid_apply x

Goal state after:
Module: Mathlib.RingTheory.Coalgebra.CoassocSimps

Goal state before:
pp: R : Type u_1
M : Type u_3
M' : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
inst✝ : Coalgebra R M
f : M →ₗ[R] M'
⊢ LinearMap.lTensor R f ∘ₗ LinearMap.rTensor M ε ∘ₗ δ = LinearMap.id ⊗ₘ f ∘ₗ λ⁻¹

Tactic:
Coalgebra.rTensor_counit_comp_comul

Goal state after:
R : Type u_1
M : Type u_3
M' : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
inst✝ : Coalgebra R M
f : M →ₗ[R] M'
⊢ LinearMap.lTensor R f ∘ₗ (TensorProduct.mk R R M) 1 = LinearMap.id ⊗ₘ f ∘ₗ λ⁻¹
Module: Mathlib.CategoryTheory.Monoidal.Comon_

Goal state before:
pp: C : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : MonoidalCategory C
M N O : C
inst✝⁸ : ComonObj M
inst✝⁷ : ComonObj N
inst✝⁶ : ComonObj O
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
F : C ⥤ D
inst✝³ : F.OplaxMonoidal
X Y : C
inst✝² : ComonObj X
inst✝¹ : ComonObj Y
f : X ⟶ Y
inst✝ : IsComonHom f
⊢ F.map f ≫ ε = ε

Tactic:
dsimp; rw [← F.map_comp_assoc, hom_counit]

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

Goal state before:
pp: R : Type u_1
inst✝¹⁴ : CommSemiring R
A : Type u_5
inst✝¹³ : CommSemiring A
inst✝¹² : Algebra R A
B : Type u_6
inst✝¹¹ : CommSemiring B
inst✝¹⁰ : Algebra R B
Aₚ : Type u_7
inst✝⁹ : CommSemiring Aₚ
inst✝⁸ : Algebra A Aₚ
inst✝⁷ : Algebra R Aₚ
inst✝⁶ : IsScalarTower R A Aₚ
Bₚ : Type u_8
inst✝⁵ : CommSemiring Bₚ
inst✝⁴ : Algebra B Bₚ
inst✝³ : Algebra R Bₚ
inst✝² : IsScalarTower R B Bₚ
f : A →ₐ[R] B
a : A
inst✝¹ : Away a Aₚ
inst✝ : Away (f a) Bₚ
hf : Function.Surjective ⇑f
⊢ IsLocalization (Submonoid.map f.toRingHom (Submonoid.powers a)) Bₚ

Tactic:
simp only [AlgHom.toRingHom_eq_coe, Submonoid.map_powers, RingHom.coe_coe]
    infer_instance

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

Goal state before:
pp: case refine_1
R : Type u_1
inst✝⁸ : CommSemiring R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
T : Type u_5
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra S T
inst✝³ : Algebra R T
inst✝² : IsScalarTower R S T
x y : R
inst✝¹ : Away x S
inst✝ : Away ((algebraMap R S) y) T
⊢ IsUnit ((algebraMap R T) (y * x))

Tactic:
simp only [map_mul, IsUnit.mul_iff, IsScalarTower.algebraMap_apply R S T]
    exact ⟨algebraMap_isUnit _, IsUnit.map _ (algebraMap_isUnit x)⟩

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

Goal state before:
pp: R : Type u_4
S : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
e : R
he : IsIdempotentElem e
H : RingHom.ker (algebraMap R S) = Ideal.span {1 - e}
H' : Function.Surjective ⇑(algebraMap R S)
x y : R
⊢ (algebraMap R S) x = (algebraMap R S) y ↔ e * x = e * y

Tactic:
← sub_eq_zero,

Goal state after:
R : Type u_4
S : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
e : R
he : IsIdempotentElem e
H : RingHom.ker (algebraMap R S) = Ideal.span {1 - e}
H' : Function.Surjective ⇑(algebraMap R S)
x y : R
⊢ (algebraMap R S) x - (algebraMap R S) y = 0 ↔ e * x = e * y
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: case refine_2
S : Type u_4
T : Type u_5
inst✝² : CommRing S
inst✝¹ : CommRing T
inst✝ : Algebra S T
h₁ : Function.Surjective ⇑(algebraMap S T)
r : S
hr : IsUnit ((algebraMap S T) r)
n : ℕ
hn : r ^ n • RingHom.ker (algebraMap S T) ≤ ⊥
x y : S
h : (algebraMap S T) x = (algebraMap S T) y
⊢ r ^ n * x = r ^ n * y

Tactic:
← sub_eq_zero,

Goal state after:
case refine_2
S : Type u_4
T : Type u_5
inst✝² : CommRing S
inst✝¹ : CommRing T
inst✝ : Algebra S T
h₁ : Function.Surjective ⇑(algebraMap S T)
r : S
hr : IsUnit ((algebraMap S T) r)
n : ℕ
hn : r ^ n • RingHom.ker (algebraMap S T) ≤ ⊥
x y : S
h : (algebraMap S T) x = (algebraMap S T) y
⊢ r ^ n * x - r ^ n * y = 0
Module: Mathlib.RingTheory.Jacobson.Ideal

Goal state before:
pp: case refine_1
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
f : R →+* S
hf : Function.Surjective ⇑f
h : RingHom.ker f ≤ I
this : ∀ J ∈ {J | I ≤ J ∧ J.IsMaximal}, RingHom.ker f ≤ J
⊢ sInf (map f '' {J | I ≤ J ∧ J.IsMaximal}) ≤ sInf {J | map f I ≤ J ∧ J.IsMaximal}

Tactic:
refine
      sInf_le_sInf fun J hJ =>
        ⟨comap f J, ⟨⟨le_comap_of_map_le hJ.1, ?_⟩, map_comap_of_surjective f hf J⟩⟩
    have : J.IsMaximal := hJ.right
    exact comap_isMaximal_of_surjective f hf

Goal state after:
Module: Mathlib.RingTheory.Jacobson.Ideal

Goal state before:
pp: R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Ring S
I✝ I : Ideal R
inst✝ : I.IsTwoSided
x r : R
xJ : x ∈ I.jacobson
𝔪 : Ideal R
⊢ 𝔪 ∈ {J | I ≤ J ∧ J.IsMaximal} → x * r ∈ 𝔪

Tactic:
𝔪_mem

Goal state after:
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Ring S
I✝ I : Ideal R
inst✝ : I.IsTwoSided
x r : R
xJ : x ∈ I.jacobson
𝔪 : Ideal R
𝔪_mem : 𝔪 ∈ {J | I ≤ J ∧ J.IsMaximal}
⊢ x * r ∈ 𝔪
Module: Mathlib.RingTheory.Jacobson.Ideal

Goal state before:
pp: R : Type u
inst✝ : CommRing R
x : R
hx : x ∈ ⊥.jacobson
y z : R
hz : z * y * x + z - 1 ∈ ⊥
⊢ x * y * z + z = 1

Tactic:
← sub_eq_zero,

Goal state after:
R : Type u
inst✝ : CommRing R
x : R
hx : x ∈ ⊥.jacobson
y z : R
hz : z * y * x + z - 1 ∈ ⊥
⊢ x * y * z + z - 1 = 0
Module: Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsLocalRing R
J : Ideal R
hJ : J ≠ ⊤
⊢ J ≤ maximalIdeal R

Tactic:
by
  rcases Ideal.exists_le_maximal J hJ with ⟨M, hM1, hM2⟩
  rwa [← eq_maximalIdeal hM1]

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

Goal state before:
pp: R : CommRingCat
⊢ IsIso (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away 1)))

Tactic:
by
  cases R
  exact localization_unit_isIso _

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

Goal state before:
pp: case mp
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
a : R
b : B
m d : ℤ
h : selfZPow x B m * mk' B a 1 * selfZPow x B (-d) = b
⊢ selfZPow x B m * mk' B a 1 = selfZPow x B d * b

Tactic:
have := congr_arg (fun s : B => s * selfZPow x B d) h

Goal state after:
case mp
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
a : R
b : B
m d : ℤ
h : selfZPow x B m * mk' B a 1 * selfZPow x B (-d) = b
this : selfZPow x B m * mk' B a 1 * selfZPow x B (-d) * selfZPow x B d = b * selfZPow x B d
⊢ selfZPow x B m * mk' B a 1 = selfZPow x B d * b
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
P' X' Y' Z' : C
fst' : P' ⟶ X'
snd' : P' ⟶ Y'
f' : X' ⟶ Z'
g' : Y' ⟶ Z'
e₁ : P ≅ P'
e₂ : X ≅ X'
e₃ : Y ≅ Y'
e₄ : Z ≅ Z'
commfst : fst ≫ e₂.hom = e₁.hom ≫ fst'
commsnd : snd ≫ e₃.hom = e₁.hom ≫ snd'
commf : f ≫ e₄.hom = e₂.hom ≫ f'
commg : g ≫ e₄.hom = e₃.hom ≫ g'
⊢ fst ≫ f ≫ e₄.hom = snd ≫ g ≫ e₄.hom

Tactic:
h.w_assoc

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
P' X' Y' Z' : C
fst' : P' ⟶ X'
snd' : P' ⟶ Y'
f' : X' ⟶ Z'
g' : Y' ⟶ Z'
e₁ : P ≅ P'
e₂ : X ≅ X'
e₃ : Y ≅ Y'
e₄ : Z ≅ Z'
commfst : fst ≫ e₂.hom = e₁.hom ≫ fst'
commsnd : snd ≫ e₃.hom = e₁.hom ≫ snd'
commf : f ≫ e₄.hom = e₂.hom ≫ f'
commg : g ≫ e₄.hom = e₃.hom ≫ g'
⊢ snd ≫ g ≫ e₄.hom = snd ≫ g ≫ e₄.hom
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
Z' X' Y' P' : C
f' : Z' ⟶ X'
g' : Z' ⟶ Y'
inl' : X' ⟶ P'
inr' : Y' ⟶ P'
e₁ : Z ≅ Z'
e₂ : X ≅ X'
e₃ : Y ≅ Y'
e₄ : P ≅ P'
commf : f ≫ e₂.hom = e₁.hom ≫ f'
commg : g ≫ e₃.hom = e₁.hom ≫ g'
comminl : inl ≫ e₄.hom = e₂.hom ≫ inl'
comminr : inr ≫ e₄.hom = e₃.hom ≫ inr'
⊢ f ≫ inl ≫ e₄.hom = g ≫ inr ≫ e₄.hom

Tactic:
h.w_assoc

Goal state after:
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
Z' X' Y' P' : C
f' : Z' ⟶ X'
g' : Z' ⟶ Y'
inl' : X' ⟶ P'
inr' : Y' ⟶ P'
e₁ : Z ≅ Z'
e₂ : X ≅ X'
e₃ : Y ≅ Y'
e₄ : P ≅ P'
commf : f ≫ e₂.hom = e₁.hom ≫ f'
commg : g ≫ e₃.hom = e₁.hom ≫ g'
comminl : inl ≫ e₄.hom = e₂.hom ≫ inl'
comminr : inr ≫ e₄.hom = e₃.hom ≫ inr'
⊢ g ≫ inr ≫ e₄.hom = g ≫ inr ≫ e₄.hom