mathlib-initiative/mathlib-tactics huggingface dataset:
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.Full
inst✝ : L.Faithful
this :
  L.whiskerLeft h.counit = (L.associator R L).inv ≫ whiskerRight (inv h.unit) L ≫ L.leftUnitor.hom ≫ L.rightUnitor.inv
⊢ IsIso (L.whiskerLeft h.counit)

Tactic:
rw [this]

Goal state after:
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.Full
inst✝ : L.Faithful
this :
  L.whiskerLeft h.counit = (L.associator R L).inv ≫ whiskerRight (inv h.unit) L ≫ L.leftUnitor.hom ≫ L.rightUnitor.inv
⊢ IsIso ((L.associator R L).inv ≫ whiskerRight (inv h.unit) L ≫ L.leftUnitor.hom ≫ L.rightUnitor.inv)
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.Full
inst✝ : L.Faithful
this :
  whiskerRight h.counit R = (R.associator L R).hom ≫ inv (R.whiskerLeft h.unit) ≫ R.rightUnitor.hom ≫ R.leftUnitor.inv
⊢ IsIso (whiskerRight h.counit R)

Tactic:
rw [this]

Goal state after:
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.Full
inst✝ : L.Faithful
this :
  whiskerRight h.counit R = (R.associator L R).hom ≫ inv (R.whiskerLeft h.unit) ≫ R.rightUnitor.hom ≫ R.leftUnitor.inv
⊢ IsIso ((R.associator L R).hom ≫ inv (R.whiskerLeft h.unit) ≫ R.rightUnitor.hom ≫ R.leftUnitor.inv)
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✝¹ : R.Full
inst✝ : R.Faithful
this :
  R.whiskerLeft h.unit = (R.rightUnitor.hom ≫ R.leftUnitor.inv) ≫ inv ((R.associator L R).inv ≫ whiskerRight h.counit R)
⊢ IsIso (R.whiskerLeft h.unit)

Tactic:
rw [this]

Goal state after:
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✝¹ : R.Full
inst✝ : R.Faithful
this :
  R.whiskerLeft h.unit = (R.rightUnitor.hom ≫ R.leftUnitor.inv) ≫ inv ((R.associator L R).inv ≫ whiskerRight h.counit R)
⊢ IsIso ((R.rightUnitor.hom ≫ R.leftUnitor.inv) ≫ inv ((R.associator L R).inv ≫ whiskerRight h.counit R))
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✝¹ : R.Full
inst✝ : R.Faithful
this :
  whiskerRight h.unit L = (L.leftUnitor.hom ≫ L.rightUnitor.inv) ≫ inv ((L.associator R L).hom ≫ L.whiskerLeft h.counit)
⊢ IsIso (whiskerRight h.unit L)

Tactic:
rw [this]

Goal state after:
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✝¹ : R.Full
inst✝ : R.Faithful
this :
  whiskerRight h.unit L = (L.leftUnitor.hom ≫ L.rightUnitor.inv) ≫ inv ((L.associator R L).hom ≫ L.whiskerLeft h.counit)
⊢ IsIso ((L.leftUnitor.hom ≫ L.rightUnitor.inv) ≫ inv ((L.associator R L).hom ≫ L.whiskerLeft h.counit))
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✝ : Fintype J
f : J → C
X : C
⊢ (rightDistributor f X).hom = ∑ j, biproduct.π f j ▷ X ≫ biproduct.ι (fun j ↦ f j ⊗ X) j

Tactic:
by
  classical
  ext
  dsimp [rightDistributor, Functor.mapBiproduct, Functor.mapBicone]
  erw [biproduct.lift_π]
  simp only [Preadditive.sum_comp, Category.assoc, biproduct.ι_π, comp_dite, comp_zero,
    Finset.sum_dite_eq', Finset.mem_univ, eqToHom_refl, Category.comp_id, ite_true]

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 : D
f : X ⟶ Y
X' : D
this : F.map (G.map f) ▷ F.obj (G.obj X') ≫ ?m.200 = (adj.counit.app X ⊗ₘ adj.counit.app X') ≫ ?m.237
⊢ adj.unit.app (G.obj X ⊗ G.obj X') ≫
      G.map (δ F (G.obj X) (G.obj X') ≫ F.map (G.map f) ▷ F.obj (G.obj X') ≫ (adj.counit.app Y ⊗ₘ adj.counit.app X')) =
    adj.unit.app (G.obj X ⊗ G.obj X') ≫
      G.map (δ F (G.obj X) (G.obj X') ≫ (adj.counit.app X ⊗ₘ adj.counit.app X') ≫ f ▷ X')

Tactic:
rw [this]

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' X : D
g : X' ⟶ Y'
this : F.obj (G.obj X) ◁ F.map (G.map g) ≫ ?m.305 = (adj.counit.app X ⊗ₘ adj.counit.app X') ≫ ?m.342
⊢ adj.unit.app (G.obj X ⊗ G.obj X') ≫
      G.map (δ F (G.obj X) (G.obj X') ≫ F.obj (G.obj X) ◁ F.map (G.map g) ≫ (adj.counit.app X ⊗ₘ adj.counit.app Y')) =
    adj.unit.app (G.obj X ⊗ G.obj X') ≫
      G.map (δ F (G.obj X) (G.obj X') ≫ (adj.counit.app X ⊗ₘ adj.counit.app X') ≫ X ◁ g)

Tactic:
rw [this]

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 : C
⊢ 𝟙_ C ◁ (β_ (𝟙_ C) X).hom ≫
      (α_ (𝟙_ C) X (𝟙_ C)).inv ≫
        (β_ (𝟙_ C) X).hom ▷ 𝟙_ C ≫ (β_ (𝟙_ C) X).inv ▷ 𝟙_ C ≫ (α_ (𝟙_ C) X (𝟙_ C)).hom ≫ 𝟙_ C ◁ (ρ_ X).hom =
    (α_ (𝟙_ C) (𝟙_ C) X).inv ≫
      (β_ (𝟙_ C ⊗ 𝟙_ C) X).hom ≫
        (α_ X (𝟙_ C) (𝟙_ C)).inv ≫ (β_ (𝟙_ C) X).inv ▷ 𝟙_ C ≫ (α_ (𝟙_ C) X (𝟙_ C)).hom ≫ 𝟙_ C ◁ (ρ_ X).hom

Tactic:
slice_lhs 1 3 => rw [← hexagon_reverse]

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
⊢ ((((α_ (𝟙_ C) (𝟙_ C) X).inv ≫ (β_ (𝟙_ C ⊗ 𝟙_ C) X).hom ≫ (α_ X (𝟙_ C) (𝟙_ C)).inv) ≫ (β_ (𝟙_ C) X).inv ▷ 𝟙_ C) ≫
        (α_ (𝟙_ C) X (𝟙_ C)).hom) ≫
      𝟙_ C ◁ (ρ_ X).hom =
    (α_ (𝟙_ C) (𝟙_ C) X).inv ≫
      (β_ (𝟙_ C ⊗ 𝟙_ C) X).hom ≫
        (α_ X (𝟙_ C) (𝟙_ C)).inv ≫ (β_ (𝟙_ C) X).inv ▷ 𝟙_ C ≫ (α_ (𝟙_ C) X (𝟙_ C)).hom ≫ 𝟙_ C ◁ (ρ_ X).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
G : D ⥤ C
adj : F ⊣ G
inst✝² : F.Monoidal
inst✝¹ : G.Monoidal
inst✝ : adj.IsMonoidal
⊢ ε G ≫ G.map (ε F) = adj.unit.app (𝟙_ C)

Tactic:
simp [← adj.unit_app_unit_comp_map_η]

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₂ : C
this :
  (λ_ (𝟙_ C)).inv ▷ (X₁ ⊗ X₂) ≫ (α_ (𝟙_ C) (𝟙_ C) (X₁ ⊗ X₂)).hom ≫ 𝟙_ C ◁ (α_ (𝟙_ C) X₁ X₂).inv =
    𝟙_ C ◁ (λ_ X₁).inv ▷ X₂
| (λ_ (𝟙_ C)).inv ▷ (X₁ ⊗ X₂) ≫ (α_ (𝟙_ C) (𝟙_ C) (X₁ ⊗ X₂)).hom ≫ 𝟙_ C ◁ (α_ (𝟙_ C) X₁ X₂).inv

pp: case a.a.a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ : C
this :
  (λ_ (𝟙_ C)).inv ▷ (X₁ ⊗ X₂) ≫ (α_ (𝟙_ C) (𝟙_ C) (X₁ ⊗ X₂)).hom ≫ 𝟙_ C ◁ (α_ (𝟙_ C) X₁ X₂).inv =
    𝟙_ C ◁ (λ_ X₁).inv ▷ X₂
| 𝟙_ C ◁ (β_ (𝟙_ C) X₁).hom ▷ X₂

pp: case a.a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ : C
this :
  (λ_ (𝟙_ C)).inv ▷ (X₁ ⊗ X₂) ≫ (α_ (𝟙_ C) (𝟙_ C) (X₁ ⊗ X₂)).hom ≫ 𝟙_ C ◁ (α_ (𝟙_ C) X₁ X₂).inv =
    𝟙_ C ◁ (λ_ X₁).inv ▷ X₂
| 𝟙_ C ◁ (α_ X₁ (𝟙_ C) X₂).hom

pp: case a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ : C
this :
  (λ_ (𝟙_ C)).inv ▷ (X₁ ⊗ X₂) ≫ (α_ (𝟙_ C) (𝟙_ C) (X₁ ⊗ X₂)).hom ≫ 𝟙_ C ◁ (α_ (𝟙_ C) X₁ X₂).inv =
    𝟙_ C ◁ (λ_ X₁).inv ▷ X₂
| (α_ (𝟙_ C) X₁ (𝟙_ C ⊗ X₂)).inv

pp: case a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ : C
this :
  (λ_ (𝟙_ C)).inv ▷ (X₁ ⊗ X₂) ≫ (α_ (𝟙_ C) (𝟙_ C) (X₁ ⊗ X₂)).hom ≫ 𝟙_ C ◁ (α_ (𝟙_ C) X₁ X₂).inv =
    𝟙_ C ◁ (λ_ X₁).inv ▷ X₂
| (λ_ X₁).hom ⊗ₘ (λ_ X₂).hom

Tactic:
rw [this]

Goal state after:
case a.a.a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ : C
this :
  (λ_ (𝟙_ C)).inv ▷ (X₁ ⊗ X₂) ≫ (α_ (𝟙_ C) (𝟙_ C) (X₁ ⊗ X₂)).hom ≫ 𝟙_ C ◁ (α_ (𝟙_ C) X₁ X₂).inv =
    𝟙_ C ◁ (λ_ X₁).inv ▷ X₂
| 𝟙_ C ◁ (λ_ X₁).inv ▷ X₂

case a.a.a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ : C
this :
  (λ_ (𝟙_ C)).inv ▷ (X₁ ⊗ X₂) ≫ (α_ (𝟙_ C) (𝟙_ C) (X₁ ⊗ X₂)).hom ≫ 𝟙_ C ◁ (α_ (𝟙_ C) X₁ X₂).inv =
    𝟙_ C ◁ (λ_ X₁).inv ▷ X₂
| 𝟙_ C ◁ (β_ (𝟙_ C) X₁).hom ▷ X₂

case a.a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ : C
this :
  (λ_ (𝟙_ C)).inv ▷ (X₁ ⊗ X₂) ≫ (α_ (𝟙_ C) (𝟙_ C) (X₁ ⊗ X₂)).hom ≫ 𝟙_ C ◁ (α_ (𝟙_ C) X₁ X₂).inv =
    𝟙_ C ◁ (λ_ X₁).inv ▷ X₂
| 𝟙_ C ◁ (α_ X₁ (𝟙_ C) X₂).hom

case a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ : C
this :
  (λ_ (𝟙_ C)).inv ▷ (X₁ ⊗ X₂) ≫ (α_ (𝟙_ C) (𝟙_ C) (X₁ ⊗ X₂)).hom ≫ 𝟙_ C ◁ (α_ (𝟙_ C) X₁ X₂).inv =
    𝟙_ C ◁ (λ_ X₁).inv ▷ X₂
| (α_ (𝟙_ C) X₁ (𝟙_ C ⊗ X₂)).inv

case a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ : C
this :
  (λ_ (𝟙_ C)).inv ▷ (X₁ ⊗ X₂) ≫ (α_ (𝟙_ C) (𝟙_ C) (X₁ ⊗ X₂)).hom ≫ 𝟙_ C ◁ (α_ (𝟙_ C) X₁ X₂).inv =
    𝟙_ C ◁ (λ_ X₁).inv ▷ X₂
| (λ_ X₁).hom ⊗ₘ (λ_ X₂).hom
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
x : Quot F
| x

Tactic:
rw [← AddMonoidHom.id_apply _ x]

Goal state after:
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
x : Quot F
| (AddMonoidHom.id (Quot F)) 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
x : Quot (F ⋙ uliftFunctor)
| x

Tactic:
rw [← AddMonoidHom.id_apply _ x]

Goal state after:
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
x : Quot (F ⋙ uliftFunctor)
| (AddMonoidHom.id (Quot (F ⋙ uliftFunctor))) x
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₂ : C
this :
  (ρ_ X₁).hom ⊗ₘ (ρ_ X₂).hom =
    (α_ X₁ (𝟙_ C) (X₂ ⊗ 𝟙_ C)).hom ≫ X₁ ◁ (α_ (𝟙_ C) X₂ (𝟙_ C)).inv ≫ X₁ ◁ (ρ_ (𝟙_ C ⊗ X₂)).hom ≫ X₁ ◁ (λ_ X₂).hom
⊢ (ρ_ X₁).hom ⊗ₘ (ρ_ X₂).hom =
    ((α_ X₁ (𝟙_ C) (X₂ ⊗ 𝟙_ C)).hom ≫
        X₁ ◁ (α_ (𝟙_ C) X₂ (𝟙_ C)).inv ≫
          X₁ ◁ (β_ (𝟙_ C) X₂).hom ▷ 𝟙_ C ≫ X₁ ◁ (α_ X₂ (𝟙_ C) (𝟙_ C)).hom ≫ (α_ X₁ X₂ (𝟙_ C ⊗ 𝟙_ C)).inv) ≫
      (X₁ ⊗ X₂) ◁ (λ_ (𝟙_ C)).hom ≫ (ρ_ (X₁ ⊗ X₂)).hom

Tactic:
rw [this]

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ : C
this :
  (ρ_ X₁).hom ⊗ₘ (ρ_ X₂).hom =
    (α_ X₁ (𝟙_ C) (X₂ ⊗ 𝟙_ C)).hom ≫ X₁ ◁ (α_ (𝟙_ C) X₂ (𝟙_ C)).inv ≫ X₁ ◁ (ρ_ (𝟙_ C ⊗ X₂)).hom ≫ X₁ ◁ (λ_ X₂).hom
⊢ (α_ X₁ (𝟙_ C) (X₂ ⊗ 𝟙_ C)).hom ≫ X₁ ◁ (α_ (𝟙_ C) X₂ (𝟙_ C)).inv ≫ X₁ ◁ (ρ_ (𝟙_ C ⊗ X₂)).hom ≫ X₁ ◁ (λ_ X₂).hom =
    ((α_ X₁ (𝟙_ C) (X₂ ⊗ 𝟙_ C)).hom ≫
        X₁ ◁ (α_ (𝟙_ C) X₂ (𝟙_ C)).inv ≫
          X₁ ◁ (β_ (𝟙_ C) X₂).hom ▷ 𝟙_ C ≫ X₁ ◁ (α_ X₂ (𝟙_ C) (𝟙_ C)).hom ≫ (α_ X₁ X₂ (𝟙_ C ⊗ 𝟙_ C)).inv) ≫
      (X₁ ⊗ X₂) ◁ (λ_ (𝟙_ C)).hom ≫ (ρ_ (X₁ ⊗ X₂)).hom
Module: Mathlib.RingTheory.Congruence.Hom

Goal state before:
pp: M : Type u_1
P : Type u_3
inst✝¹ : NonAssocSemiring M
inst✝ : NonAssocSemiring P
c : RingCon M
f : M →+* P
h : c ≤ ker f
⊢ Bijective ⇑(c.lift f h) ↔ c = ker f ∧ Surjective ⇑f

Tactic:
unfold Function.Bijective

Goal state after:
M : Type u_1
P : Type u_3
inst✝¹ : NonAssocSemiring M
inst✝ : NonAssocSemiring P
c : RingCon M
f : M →+* P
h : c ≤ ker f
⊢ Injective ⇑(c.lift f h) ∧ Surjective ⇑(c.lift f h) ↔ c = ker f ∧ Surjective ⇑f
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
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : M →ₗ[R] A
x y : FreeAlgebra R M
h : Rel R M x y
⊢ (RingCon.ker ((FreeAlgebra.lift R) ⇑f).toRingHom) x y

Tactic:
induction h <;>
          simp [Algebra.smul_def, FreeAlgebra.lift_ι_apply,
            map_mul, AlgHom.commutes, map_add, RingCon.ker]

Goal state after:
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
C : TensorAlgebra R M → Prop
algebraMap : ∀ (r : R), C ((Algebra.algebraMap R (TensorAlgebra R M)) r)
ι : ∀ (x : M), C ((TensorAlgebra.ι R) x)
mul : ∀ (a b : TensorAlgebra R M), C a → C b → C (a * b)
add : ∀ (a b : TensorAlgebra R M), C a → C b → C (a + b)
a : TensorAlgebra R M
s : Subalgebra R (TensorAlgebra R M) :=
  { carrier := {a | C a}, mul_mem' := mul, one_mem' := ⋯, add_mem' := add, zero_mem' := ⋯,
    algebraMap_mem' := algebraMap }
of : M →ₗ[R] ↥s := LinearMap.codRestrict (Subalgebra.toSubmodule s) (TensorAlgebra.ι R) ι
of_apply : ∀ {x : M}, ↑(of x) = (TensorAlgebra.ι R) x
⊢ C a

Tactic:
have of_id : AlgHom.id R (TensorAlgebra R M) = s.val.comp (lift R of) := by
    ext
    simp [of_apply]

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
C : TensorAlgebra R M → Prop
algebraMap : ∀ (r : R), C ((Algebra.algebraMap R (TensorAlgebra R M)) r)
ι : ∀ (x : M), C ((TensorAlgebra.ι R) x)
mul : ∀ (a b : TensorAlgebra R M), C a → C b → C (a * b)
add : ∀ (a b : TensorAlgebra R M), C a → C b → C (a + b)
a : TensorAlgebra R M
s : Subalgebra R (TensorAlgebra R M) :=
  { carrier := {a | C a}, mul_mem' := mul, one_mem' := ⋯, add_mem' := add, zero_mem' := ⋯,
    algebraMap_mem' := algebraMap }
of : M →ₗ[R] ↥s := LinearMap.codRestrict (Subalgebra.toSubmodule s) (TensorAlgebra.ι R) ι
of_apply : ∀ {x : M}, ↑(of x) = (TensorAlgebra.ι R) x
of_id : AlgHom.id R (TensorAlgebra R M) = s.val.comp ((lift R) of)
⊢ C a
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 ⥤ D
H : B ⥤ E
K : C ⥤ F
L₁ : A ⥤ B
R₁ : B ⥤ A
L₂ : D ⥤ E
R₂ : E ⥤ D
L₃ : B ⥤ C
R₃ : C ⥤ B
L₄ : E ⥤ F
R₄ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
adj₄ : L₄ ⊣ R₄
α : TwoSquare G L₁ L₂ H
β : TwoSquare H L₃ L₄ K
c : C
⊢ adj₂.unit.app (G.obj (R₁.obj (R₃.obj c))) ≫
      R₂.map (adj₄.unit.app (L₂.obj (G.obj (R₁.obj (R₃.obj c))))) ≫
        R₂.map (R₄.map (L₄.map (α.natTrans.app (R₁.obj (R₃.obj c))))) ≫
          R₂.map (R₄.map (β.natTrans.app (L₁.obj (R₁.obj (R₃.obj c))))) ≫
            R₂.map (R₄.map (K.map (L₃.map (adj₁.counit.app (R₃.obj c))))) ≫
              R₂.map (R₄.map (K.map (adj₃.counit.app c))) =
    adj₂.unit.app (G.obj (R₁.obj (R₃.obj c))) ≫
      ((R₂.map (adj₄.unit.app (L₂.obj (G.obj (R₁.obj (R₃.obj c))))) ≫
            R₂.map (R₄.map (L₄.map (α.natTrans.app (R₁.obj (R₃.obj c))))) ≫
              R₂.map (R₄.map (L₄.map (H.map (adj₁.counit.app (R₃.obj c)))))) ≫
          R₂.map (R₄.map (β.natTrans.app (R₃.obj c)))) ≫
        R₂.map (R₄.map (K.map (adj₃.counit.app c)))

Tactic:
slice_rhs 4 5 =>
    rw [← R₂.map_comp, ← R₄.map_comp, ← Functor.comp_map _ L₄, β.naturality]

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 ⥤ D
H : B ⥤ E
K : C ⥤ F
L₁ : A ⥤ B
R₁ : B ⥤ A
L₂ : D ⥤ E
R₂ : E ⥤ D
L₃ : B ⥤ C
R₃ : C ⥤ B
L₄ : E ⥤ F
R₄ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
adj₄ : L₄ ⊣ R₄
α : TwoSquare G L₁ L₂ H
β : TwoSquare H L₃ L₄ K
c : C
⊢ adj₂.unit.app (G.obj (R₁.obj (R₃.obj c))) ≫
      R₂.map (adj₄.unit.app (L₂.obj (G.obj (R₁.obj (R₃.obj c))))) ≫
        R₂.map (R₄.map (L₄.map (α.natTrans.app (R₁.obj (R₃.obj c))))) ≫
          R₂.map (R₄.map (β.natTrans.app (L₁.obj (R₁.obj (R₃.obj c))))) ≫
            R₂.map (R₄.map (K.map (L₃.map (adj₁.counit.app (R₃.obj c))))) ≫
              R₂.map (R₄.map (K.map (adj₃.counit.app c))) =
    adj₂.unit.app (G.obj (R₁.obj (R₃.obj c))) ≫
      R₂.map (adj₄.unit.app (L₂.obj (G.obj (R₁.obj (R₃.obj c))))) ≫
        R₂.map (R₄.map (L₄.map (α.natTrans.app (R₁.obj (R₃.obj c))))) ≫
          R₂.map (R₄.map (β.app (L₁.obj (R₁.obj (R₃.obj c))) ≫ (L₃ ⋙ K).map (adj₁.counit.app (R₃.obj c)))) ≫
            R₂.map (R₄.map (K.map (adj₃.counit.app c)))
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₂ : C ⥤ D
R₁ R₂ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : L₂ ⟶ L₁
c : C
this :
  adj₁.unit.app c ≫
      𝟙 (R₁.obj (L₁.obj c)) ≫
        adj₂.unit.app (R₁.obj (L₁.obj c)) ≫
          𝟙 (R₂.obj (L₂.obj (R₁.obj (L₁.obj c)))) ≫
            𝟙 (R₂.obj (L₂.obj (R₁.obj (L₁.obj c)))) ≫
              R₂.map (𝟙 (L₂.obj (R₁.obj (L₁.obj c))) ≫ α.app (R₁.obj (L₁.obj c)) ≫ 𝟙 (L₁.obj (R₁.obj (L₁.obj c)))) ≫
                𝟙 (R₂.obj (L₁.obj (R₁.obj (L₁.obj c)))) ≫
                  𝟙 (R₂.obj (L₁.obj (R₁.obj (L₁.obj c)))) ≫
                    R₂.map (adj₁.counit.app (L₁.obj c)) ≫ 𝟙 (R₂.obj (L₁.obj c)) =
    adj₂.unit.app c ≫ R₂.map (𝟙 (L₂.obj c) ≫ α.app c ≫ 𝟙 (L₁.obj c))
⊢ adj₁.unit.app c ≫
      𝟙 (R₁.obj (L₁.obj c)) ≫
        adj₂.unit.app (R₁.obj (L₁.obj c)) ≫
          𝟙 (R₂.obj (L₂.obj (R₁.obj (L₁.obj c)))) ≫
            𝟙 (R₂.obj (L₂.obj (R₁.obj (L₁.obj c)))) ≫
              R₂.map (𝟙 (L₂.obj (R₁.obj (L₁.obj c))) ≫ α.app (R₁.obj (L₁.obj c)) ≫ 𝟙 (L₁.obj (R₁.obj (L₁.obj c)))) ≫
                𝟙 (R₂.obj (L₁.obj (R₁.obj (L₁.obj c)))) ≫
                  𝟙 (R₂.obj (L₁.obj (R₁.obj (L₁.obj c)))) ≫
                    R₂.map (adj₁.counit.app (L₁.obj c)) ≫ 𝟙 (R₂.obj (L₁.obj c)) =
    adj₂.unit.app c ≫ R₂.map (α.app c)

Tactic:
rw [this]

Goal state after:
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ L₂ : C ⥤ D
R₁ R₂ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : L₂ ⟶ L₁
c : C
this :
  adj₁.unit.app c ≫
      𝟙 (R₁.obj (L₁.obj c)) ≫
        adj₂.unit.app (R₁.obj (L₁.obj c)) ≫
          𝟙 (R₂.obj (L₂.obj (R₁.obj (L₁.obj c)))) ≫
            𝟙 (R₂.obj (L₂.obj (R₁.obj (L₁.obj c)))) ≫
              R₂.map (𝟙 (L₂.obj (R₁.obj (L₁.obj c))) ≫ α.app (R₁.obj (L₁.obj c)) ≫ 𝟙 (L₁.obj (R₁.obj (L₁.obj c)))) ≫
                𝟙 (R₂.obj (L₁.obj (R₁.obj (L₁.obj c)))) ≫
                  𝟙 (R₂.obj (L₁.obj (R₁.obj (L₁.obj c)))) ≫
                    R₂.map (adj₁.counit.app (L₁.obj c)) ≫ 𝟙 (R₂.obj (L₁.obj c)) =
    adj₂.unit.app c ≫ R₂.map (𝟙 (L₂.obj c) ≫ α.app c ≫ 𝟙 (L₁.obj c))
⊢ adj₂.unit.app c ≫ R₂.map (𝟙 (L₂.obj c) ≫ α.app c ≫ 𝟙 (L₁.obj c)) = adj₂.unit.app c ≫ R₂.map (α.app c)
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: R : Type u
A : Type v
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Coalgebra R A
a : A
⊢ (TensorProduct.assoc R A A A).symm ((LinearMap.lTensor A comul) (comul a)) = (LinearMap.rTensor A comul) (comul a)

Tactic:
(TensorProduct.assoc R A A A).symm_apply_eq,

Goal state after:
R : Type u
A : Type v
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Coalgebra R A
a : A
⊢ (LinearMap.lTensor A comul) (comul a) = (TensorProduct.assoc R A A A) ((LinearMap.rTensor A comul) (comul a))
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: case h2
R : Type u
M : Type v
inst✝⁴ : DivisionSemiring R
inst✝³ : AddCommGroup M
inst✝² : Module Rᵐᵒᵖ M
inst✝¹ : Module R M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
a b : tsze R M
⊢ -((a.fst * b.fst)⁻¹ •> a.fst •> b.snd <• (a.fst * b.fst)⁻¹ +
        (a.fst * b.fst)⁻¹ •> (a.snd <• b.fst) <• (a.fst * b.fst)⁻¹) =
    -(b.fst⁻¹ •> (a.fst⁻¹ •> a.snd <• a.fst⁻¹)) + -(b.fst⁻¹ •> b.snd <• b.fst⁻¹ <• a.fst⁻¹)

Tactic:
simp_rw [mul_inv_rev, smul_comm (_ : R), op_smul_op_smul, smul_smul, add_comm, neg_add]

Goal state after:
case h2
R : Type u
M : Type v
inst✝⁴ : DivisionSemiring R
inst✝³ : AddCommGroup M
inst✝² : Module Rᵐᵒᵖ M
inst✝¹ : Module R M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
a b : tsze R M
⊢ -((b.fst⁻¹ * a.fst⁻¹) •> a.snd <• (b.fst * (b.fst⁻¹ * a.fst⁻¹))) +
      -((b.fst⁻¹ * a.fst⁻¹ * a.fst) •> b.snd <• (b.fst⁻¹ * a.fst⁻¹)) =
    -((b.fst⁻¹ * a.fst⁻¹) •> a.snd <• a.fst⁻¹) + -(b.fst⁻¹ •> b.snd <• (b.fst⁻¹ * a.fst⁻¹))
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : Module R A
inst✝² : Module R B
inst✝¹ : Coalgebra R A
inst✝ : Coalgebra R B
⊢ ↑(TensorProduct.assoc R (A × B) (A × B) (A × B)) ∘ₗ rTensor (A × B) comul ∘ₗ comul = lTensor (A × B) comul ∘ₗ comul

Tactic:
dsimp +instances only [instCoalgebraStruct]

Goal state after:
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : Module R A
inst✝² : Module R B
inst✝¹ : Coalgebra R A
inst✝ : Coalgebra R B
⊢ ↑(TensorProduct.assoc R (A × B) (A × B) (A × B)) ∘ₗ
      rTensor (A × B)
          ((TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul).coprod
            (TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul)) ∘ₗ
        (TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul).coprod
          (TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul) =
    lTensor (A × B)
        ((TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul).coprod
          (TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul)) ∘ₗ
      (TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul).coprod (TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul)
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✝
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
Y : ModuleCat S
m1 : Module R S := Module.compHom S f
m2 : Module R ↑Y := Module.compHom (↑Y) f
s₁ s₂ : S
⊢ { toFun := fun y ↦ (s₁ + s₂) • y, map_add' := ⋯, map_smul' := ⋯ } =
    { toFun := fun y ↦ s₁ • y, map_add' := ⋯, map_smul' := ⋯ } +
      { toFun := fun y ↦ s₂ • y, map_add' := ⋯, map_smul' := ⋯ }

Tactic:
by
          ext y
          change (s₁ + s₂) • y = s₁ • y + s₂ • y
          rw [add_smul]

Goal state after:
Module: Mathlib.Order.Category.Semilat

Goal state before:
pp: α β : SemilatSupCat
e : α.X ≃o β.X
⊢ { toFun := ⇑e, map_sup' := ⋯, map_bot' := ⋯ } ≫ { toFun := ⇑e.symm, map_sup' := ⋯, map_bot' := ⋯ } = 𝟙 α

Tactic:
by ext; exact e.symm_apply_apply _

Goal state after:
Module: Mathlib.Order.Category.Semilat

Goal state before:
pp: α β : SemilatInfCat
e : α.X ≃o β.X
⊢ { toFun := ⇑e, map_inf' := ⋯, map_top' := ⋯ } ≫ { toFun := ⇑e.symm, map_inf' := ⋯, map_top' := ⋯ } = 𝟙 α

Tactic:
by ext; exact e.symm_apply_apply _

Goal state after:
Module: Mathlib.Order.Category.BddOrd

Goal state before:
pp: α β : BddOrd
e : ↑α.toPartOrd ≃o ↑β.toPartOrd
⊢ ofHom ↑e ≫ ofHom ↑e.symm = 𝟙 α

Tactic:
by ext; exact e.symm_apply_apply _

Goal state after:
Module: Mathlib.Order.Category.BddLat

Goal state before:
pp: α β : BddLat
e : ↑α.toLat ≃o ↑β.toLat
⊢ ofHom
        (let __src := { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯ };
        { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ }) ≫
      ofHom
        (let __src := { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯ };
        { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ }) =
    𝟙 α

Tactic:
by ext; exact e.symm_apply_apply _

Goal state after: