mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Category.ModuleCat.Limits

Goal state before:
pp: case refine_2
R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : Category.{t, v} J
F : J ⥤ ModuleCat R
inst✝ : Small.{w, max v w} ↑(F ⋙ forget (ModuleCat R)).sections
s : Cone F
⊢ ∀ (m : R) (x : ↑s.1),
    {
            toFun :=
              ⇑(ConcreteCategory.hom
                  ((Types.Small.limitConeIsLimit (F ⋙ forget (ModuleCat R))).lift ((forget (ModuleCat R)).mapCone s))),
            map_add' := ⋯ }.toFun
        (m • x) =
      (RingHom.id R) m •
        {
              toFun :=
                ⇑(ConcreteCategory.hom
                    ((Types.Small.limitConeIsLimit (F ⋙ forget (ModuleCat R))).lift
                      ((forget (ModuleCat R)).mapCone s))),
              map_add' := ⋯ }.toFun
          x

Tactic:
· intro r x
    simp [← equivShrink_smul]
    rfl

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

Goal state before:
pp: case refine_2
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ SemiRingCat
inst✝ : Small.{u, max u v} ↑(F ⋙ forget SemiRingCat).sections
s : Cone F
⊢ ∀ (x y : ↑s.1),
    EquivLike.coe (equivShrink ↑(F ⋙ forget SemiRingCat).sections)
        ⟨fun j ↦ (ConcreteCategory.hom (((forget SemiRingCat).mapCone s).π.app j)) (x * y), ⋯⟩ =
      EquivLike.coe (equivShrink ↑(F ⋙ forget SemiRingCat).sections)
          ⟨fun j ↦ (ConcreteCategory.hom (((forget SemiRingCat).mapCone s).π.app j)) x, ⋯⟩ *
        EquivLike.coe (equivShrink ↑(F ⋙ forget SemiRingCat).sections)
          ⟨fun j ↦ (ConcreteCategory.hom (((forget SemiRingCat).mapCone s).π.app j)) y, ⋯⟩

Tactic:
intro x y
    simp [← equivShrink_mul]
    rfl

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 Y : C
f : J → C
⊢ ((asIso (𝟙 X) ⊗ᵢ leftDistributor Y f) ≪≫ leftDistributor X fun j ↦ Y ⊗ f j) =
    (α_ X Y (⨁ f)).symm ≪≫ leftDistributor (X ⊗ Y) f ≪≫ biproduct.mapIso fun x ↦ α_ X Y (f x)

Tactic:
by
  classical
  cases nonempty_fintype J
  ext
  simp only [Category.comp_id, Category.assoc, eqToHom_refl, Iso.trans_hom, Iso.symm_hom,
    asIso_hom, comp_zero, comp_dite, Preadditive.sum_comp, Preadditive.comp_sum, tensor_sum,
    id_tensor_comp, tensorIso_hom, leftDistributor_hom, biproduct.mapIso_hom, biproduct.ι_map,
    biproduct.ι_π, Finset.sum_dite_irrel, Finset.sum_dite_eq', Finset.sum_const_zero]
  simp_rw [← id_tensorHom]
  simp only [← id_tensor_comp, biproduct.ι_π]
  simp only [id_tensor_comp, tensor_dite, comp_dite]
  simp

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 ⥤ E
inst✝¹ : F.OplaxMonoidal
inst✝ : G.OplaxMonoidal
X✝ Y✝ x✝¹ : C
x✝ : X✝ ⟶ Y✝
⊢ G.map (δ F x✝¹ X✝) ≫ δ G (F.obj x✝¹) (F.obj X✝) ≫ G.obj (F.obj x✝¹) ◁ G.map (F.map x✝) =
    G.map (F.map (x✝¹ ◁ x✝)) ≫ G.map (δ F x✝¹ Y✝) ≫ δ G (F.obj x✝¹) (F.obj Y✝)

Tactic:
δ_natural_right,

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 ⥤ E
inst✝¹ : F.OplaxMonoidal
inst✝ : G.OplaxMonoidal
X✝ Y✝ x✝¹ : C
x✝ : X✝ ⟶ Y✝
⊢ G.map (δ F x✝¹ X✝) ≫ G.map (F.obj x✝¹ ◁ F.map x✝) ≫ δ G (F.obj x✝¹) (F.obj Y✝) =
    G.map (F.map (x✝¹ ◁ x✝)) ≫ G.map (δ F x✝¹ Y✝) ≫ δ G (F.obj x✝¹) (F.obj Y✝)
Module: Mathlib.Tactic.CategoryTheory.Monoidal.PureCoherence

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
f g f' : C
η θ : f ≅ g
η_f : 𝟙_ C ⊗ f ≅ f'
η_g : 𝟙_ C ⊗ g ≅ f'
h_η : 𝟙_ C ◁ η ≪≫ η_g = η_f
h_θ : 𝟙_ C ◁ θ ≪≫ η_g = η_f
⊢ η.hom = (λ_ f).inv ≫ η_f.hom ≫ η_g.inv ≫ (λ_ g).hom

Tactic:
by
      simp [← reassoc_of% (congrArg Iso.hom h_η)]

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 ⥤ E
inst✝¹ : F.OplaxMonoidal
inst✝ : G.OplaxMonoidal
X✝ Y✝ x✝¹ : C
x✝ : X✝ ⟶ Y✝
⊢ G.map (δ F x✝¹ X✝ ≫ F.obj x✝¹ ◁ F.map x✝) ≫ δ G (F.obj x✝¹) (F.obj Y✝) =
    G.map (F.map (x✝¹ ◁ x✝)) ≫ G.map (δ F x✝¹ Y✝) ≫ δ G (F.obj x✝¹) (F.obj Y✝)

Tactic:
δ_natural_right,

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 ⥤ E
inst✝¹ : F.OplaxMonoidal
inst✝ : G.OplaxMonoidal
X✝ Y✝ x✝¹ : C
x✝ : X✝ ⟶ Y✝
⊢ G.map (F.map (x✝¹ ◁ x✝) ≫ δ F x✝¹ Y✝) ≫ δ G (F.obj x✝¹) (F.obj Y✝) =
    G.map (F.map (x✝¹ ◁ x✝)) ≫ G.map (δ F x✝¹ Y✝) ≫ δ G (F.obj x✝¹) (F.obj 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
T : D
⊢ ε F ▷ T ≫ η F ▷ T = 𝟙 (𝟙_ D ⊗ T)

Tactic:
by
  rw [← MonoidalCategory.comp_whiskerRight, ε_η, id_whiskerRight]

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.leftOp
hc : IsLimit c
s : Cocone F
m : (coconeOfConeLeftOp c).pt ⟶ s.pt
w : ∀ (j : J), (coconeOfConeLeftOp c).ι.app j ≫ m = s.ι.app j
j : Jᵒᵖ
⊢ (m.unop ≫ c.π.app j).op = ((hc.lift (coneLeftOpOfCocone s)).op.unop ≫ c.π.app j).op

Tactic:
simpa only [Quiver.Hom.unop_op, IsLimit.fac, coconeOfConeLeftOp_ι_app] using! w (unop j)

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

Goal state before:
pp: case h₁
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✝ F : C ⥤ D
G : C ⥤ E
inst✝¹ : F.Monoidal
inst✝ : G.Monoidal
x✝¹ x✝ : C
⊢ (μ (F.prod' G) x✝¹ x✝ ≫ δ (F.prod' G) x✝¹ x✝).1 = (𝟙 ((F.prod' G).obj x✝¹ ⊗ (F.prod' G).obj x✝)).1

Tactic:
simp only [CategoryTheory.prod_comp_fst, prod'_μ_fst, prod'_δ_fst, μ_δ,
        prod'_obj, prodMonoidal_tensorObj, prod_id]

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

Goal state before:
pp: case refine_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
W X Y : C
f : W ⟶ X
g : W ⟶ Y
c : PushoutCocone f g
G : C ⥤ D
⊢ inl ((Cocone.precompose (diagramIsoSpan (span f g ⋙ G)).symm.hom).obj (G.mapCocone c)) ≫
      (Iso.refl ((Cocone.precompose (diagramIsoSpan (span f g ⋙ G)).symm.hom).obj (G.mapCocone c)).pt).hom =
    (c.map G).inl

pp: case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
W X Y : C
f : W ⟶ X
g : W ⟶ Y
c : PushoutCocone f g
G : C ⥤ D
⊢ inr ((Cocone.precompose (diagramIsoSpan (span f g ⋙ G)).symm.hom).obj (G.mapCocone c)) ≫
      (Iso.refl ((Cocone.precompose (diagramIsoSpan (span f g ⋙ G)).symm.hom).obj (G.mapCocone c)).pt).hom =
    (c.map G).inr

Tactic:
· dsimp only [inl]
        simp

Goal state after:
case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
W X Y : C
f : W ⟶ X
g : W ⟶ Y
c : PushoutCocone f g
G : C ⥤ D
⊢ inr ((Cocone.precompose (diagramIsoSpan (span f g ⋙ G)).symm.hom).obj (G.mapCocone c)) ≫
      (Iso.refl ((Cocone.precompose (diagramIsoSpan (span f g ⋙ G)).symm.hom).obj (G.mapCocone c)).pt).hom =
    (c.map G).inr
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✝¹ : PreservesLimit (cospan f f) F
inst✝ : Mono f
⊢ Mono (F.map f)

Tactic:
by
  have := isLimitPullbackConeMapOfIsLimit F _ (PullbackCone.isLimitMkIdId f)
  simp_rw [F.map_id] at this
  apply PullbackCone.mono_of_isLimitMkIdId _ 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).inv ≫ (ρ_ (𝟙_ C)).hom ▷ X = 𝟙_ C ◁ (λ_ X).hom

Tactic:
rw [triangle_assoc_comp_right]

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'
e : C ≌ D
inst✝² : e.functor.Monoidal
inst✝¹ : e.inverse.Monoidal
inst✝ : e.IsMonoidal
⊢ ε e.symm.inverse = e.symm.toAdjunction.unit.app (𝟙_ D) ≫ e.symm.inverse.map (η e.symm.functor)

Tactic:
simp only [toAdjunction]
    dsimp [symm]
    rw [counitIso_inv_app_comp_functor_map_η_inverse]

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) ι
⊢ C a

Tactic:
have of_apply {x : M} : of x = (TensorAlgebra.ι R) x := by rfl

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
⊢ C a
Module: Mathlib.LinearAlgebra.TensorAlgebra.Basic

Goal state before:
pp: case algebraMap
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r✝ : R
⊢ (algebraMap R (TensorAlgebra R M)) r✝ ∈ Algebra.adjoin R (Set.range ⇑(ι R))

Tactic:
exact algebraMap_mem _ _

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

Goal state before:
pp: case succ
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 : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
n✝ : ℕ
⊢ (List.map (fun i ↦ x.fst ^ (n✝ + 1 - i) •> x.snd <• x.fst ^ i) (List.range (n✝ + 1 + 1))).sum =
    (x ^ (n✝ + 1)).fst •> x.snd +
      (List.map (fun i ↦ x.fst ^ ((n✝ + 1).pred - i) •> x.snd <• x.fst ^ i) (List.range (n✝ + 1))).sum <• x.fst

Tactic:
List.sum_range_succ'

Goal state after:
case succ
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 : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
n✝ : ℕ
⊢ x.fst ^ (n✝ + 1 - 0) •> x.snd <• x.fst ^ 0 +
      (List.map (fun i ↦ x.fst ^ (n✝ + 1 - i.succ) •> x.snd <• x.fst ^ i.succ) (List.range (n✝ + 1))).sum =
    (x ^ (n✝ + 1)).fst •> x.snd +
      (List.map (fun i ↦ x.fst ^ ((n✝ + 1).pred - i) •> x.snd <• x.fst ^ i) (List.range (n✝ + 1))).sum <• x.fst
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✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
X : ModuleCat R
Y : ModuleCat S
g : (restrictScalars f).obj Y ⟶ X
y : ↑Y
s1 s2 : S
⊢ (ConcreteCategory.hom g) ((s1 + s2) • y) = (ConcreteCategory.hom g) (s1 • y) + (ConcreteCategory.hom g) (s2 • y)

Tactic:
by simp [add_smul]

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

Goal state before:
pp: R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
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
r : R
s : S
y : ↑Y
⊢ (f r • s) • y = f r • s • y

Tactic:
smul_eq_mul,

Goal state after:
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
r : R
s : S
y : ↑Y
⊢ (f r * s) • y = f r • s • y
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: case tmul
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 Y' : ModuleCat S
g : Y ⟶ Y'
m1 : Module R S := Module.compHom S f
m2✝ : Module R ↑Y := Module.compHom (↑Y) f
m2 : Module R ↑Y' := Module.compHom (↑Y') f
s'✝ : ↑((restrictScalars f).obj (of S S))
y : ↑((restrictScalars f).obj Y)
s' : S := s'✝
⊢ ({ toFun := fun s ↦ { toFun := fun y ↦ s • y, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯ } s').toAddHom
      ((ConcreteCategory.hom g) y) =
    (Hom.hom g) ((Hom.hom (Counit.map f)) (s' ⊗ₜ[R] y))

Tactic:
change s' • g y = g (s' • y)

Goal state after:
case tmul
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 Y' : ModuleCat S
g : Y ⟶ Y'
m1 : Module R S := Module.compHom S f
m2✝ : Module R ↑Y := Module.compHom (↑Y) f
m2 : Module R ↑Y' := Module.compHom (↑Y') f
s'✝ : ↑((restrictScalars f).obj (of S S))
y : ↑((restrictScalars f).obj Y)
s' : S := s'✝
⊢ s' • (ConcreteCategory.hom g) y = (ConcreteCategory.hom g) (s' • y)
Module: Mathlib.CategoryTheory.Adjunction.Unique

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
F F' : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
adj2 : F' ⊣ G
x : C
⊢ (adj1.unit ≫ whiskerRight (adj1.leftAdjointUniq adj2).hom G).app x = adj2.unit.app x

Tactic:
rw [NatTrans.comp_app, ← homEquiv_leftAdjointUniq_hom_app adj1 adj2]

Goal state after:
C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
F F' : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
adj2 : F' ⊣ G
x : C
⊢ adj1.unit.app x ≫ (whiskerRight (adj1.leftAdjointUniq adj2).hom G).app x =
    (adj1.homEquiv x (F'.obj x)) ((adj1.leftAdjointUniq adj2).hom.app x)
Module: Mathlib.CategoryTheory.Adjunction.Unique

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
F : C ⥤ D
G G' : D ⥤ C
adj1 : F ⊣ G
adj2 : F ⊣ G'
x : C
⊢ adj1.unit.app x ≫ adj2.unit.app (G.obj (F.obj x)) ≫ G'.map (adj1.counit.app (F.obj x)) = adj2.unit.app x

Tactic:
← adj2.unit_naturality_assoc,

Goal state after:
C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
F : C ⥤ D
G G' : D ⥤ C
adj1 : F ⊣ G
adj2 : F ⊣ G'
x : C
⊢ adj2.unit.app x ≫ G'.map (F.map (adj1.unit.app x)) ≫ G'.map (adj1.counit.app (F.obj x)) = adj2.unit.app x
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
r r' : R
h : Associated r r'
inst✝ : Away r S
⊢ Away r' S

Tactic:
obtain ⟨u, rfl⟩ := h

Goal state after:
R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
r : R
inst✝ : Away r S
u : Rˣ
⊢ Away (r * ↑u) S
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommSemiring R
P : Type u_3
inst✝⁶ : CommSemiring P
Q : Type u_4
inst✝⁵ : CommSemiring Q
inst✝⁴ : Algebra P Q
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra R S
f : R →+* P
r : R
inst✝¹ : Away r S
inst✝ : Away (f r) Q
H : ∀ (a : R), f a = 0 → ∃ n, r ^ n * a = 0
a : R
n : ℕ
ha : f r ^ n * f a = 0
m : ℕ
hm : r ^ m * (r ^ n * a) = 0
⊢ r ^ (m + n) * a = 0

Tactic:
by simp [pow_add, mul_assoc, *]

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
I : Ideal R
r : R
h : r - 1 ∈ I.jacobson
⊢ ∃ s, s * r - 1 ∈ I

Tactic:
convert! exists_mul_add_sub_mem_of_mem_jacobson _ h
  simp

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
r : R
h : r - 1 ∈ ⊥.jacobson
s : R
hs : s * r - 1 ∈ ⊥
⊢ IsUnit r

Tactic:
rw [mem_bot, sub_eq_zero, mul_comm] at hs

Goal state after:
R : Type u
inst✝ : CommRing R
r : R
h : r - 1 ∈ ⊥.jacobson
s : R
hs : r * s = 1
⊢ IsUnit r
Module: Mathlib.RingTheory.LocalRing.RingHom.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
hf : Function.Surjective ⇑f
h : IsLocalHom f
⊢ Function.Surjective ⇑(Units.map ↑f)

Tactic:
intro a
  obtain ⟨b, hb⟩ := hf (a : S)
  use (isUnit_of_map_unit f b (by rw [hb]; exact Units.isUnit _)).unit
  ext
  exact hb

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

Goal state before:
pp: case intro
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
ι : Type u_4
inst✝ : Finite ι
f : ι → S
val✝ : Fintype ι
⊢ ∃ b, ∀ (i : ι), IsInteger R (↑b • f i)

Tactic:
obtain ⟨b, hb⟩ := exist_integer_multiples M Finset.univ f

Goal state after:
case intro
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
ι : Type u_4
inst✝ : Finite ι
f : ι → S
val✝ : Fintype ι
b : ↥M
hb : ∀ i ∈ Finset.univ, IsInteger R (↑b • f i)
⊢ ∃ b, ∀ (i : ι), IsInteger R (↑b • f i)
Module: Mathlib.CategoryTheory.Monoidal.Mon

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

Tactic:
simp only [comp_whiskerRight_assoc]
  slice_lhs 2 3 => rw [tensorμ_natural_left]
  slice_lhs 3 4 => rw [tensorHom_comp_tensorHom, one_mul, one_mul]
  symm
  exact tensor_left_unitality M N

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

Goal state before:
pp: R : Type u_1
Rₛ : Type u_2
inst✝¹⁰ : CommSemiring R
S : Submonoid R
inst✝⁹ : CommSemiring Rₛ
inst✝⁸ : Algebra R Rₛ
inst✝⁷ : IsLocalization S Rₛ
M : Type u_3
Mₛ : Type u_4
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : AddCommMonoid Mₛ
inst✝³ : Module R Mₛ
inst✝² : Module Rₛ Mₛ
inst✝¹ : IsScalarTower R Rₛ Mₛ
f : M →ₗ[R] Mₛ
inst✝ : IsLocalizedModule S f
v : Set M
hv : span R v = ⊤
x : Mₛ
x✝ : x ∈ ⊤
m : M
s : ↥S
h : (algebraMap R Rₛ) ↑(m, s).2 • x = f (m, s).1
⊢ x ∈ span Rₛ (⇑f '' v)

Tactic:
← Units.smul_isUnit (IsLocalization.map_units Rₛ s),

Goal state after:
R : Type u_1
Rₛ : Type u_2
inst✝¹⁰ : CommSemiring R
S : Submonoid R
inst✝⁹ : CommSemiring Rₛ
inst✝⁸ : Algebra R Rₛ
inst✝⁷ : IsLocalization S Rₛ
M : Type u_3
Mₛ : Type u_4
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : AddCommMonoid Mₛ
inst✝³ : Module R Mₛ
inst✝² : Module Rₛ Mₛ
inst✝¹ : IsScalarTower R Rₛ Mₛ
f : M →ₗ[R] Mₛ
inst✝ : IsLocalizedModule S f
v : Set M
hv : span R v = ⊤
x : Mₛ
x✝ : x ∈ ⊤
m : M
s : ↥S
h : ⋯.unit • x = f (m, s).1
⊢ x ∈ span Rₛ (⇑f '' v)
Module: Mathlib.RingTheory.Localization.BaseChange

Goal state before:
pp: R : Type u_7
S : Type u_8
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
A : Type u_9
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
M : Submonoid R
inst✝ : IsLocalization M A
s : S
x : R
y : ↥M
⊢ mk' A x y ⊗ₜ[R] s = mk' (A ⊗[R] S) ((algebraMap R S) x * s) ⟨(algebraMap R S) ↑y, ⋯⟩

Tactic:
simp [IsLocalization.eq_mk'_iff_mul_eq, map_mul,
    RingHom.algebraMap_toAlgebra]

Goal state after:
Module: Mathlib.Control.Bifunctor

Goal state before:
pp: case id_bimap
F : Type u₀ → Type u₁ → Type u₂
inst✝⁵ : Bifunctor F
G : Type u_1 → Type u₀
H : Type u_2 → Type u₁
inst✝⁴ : Functor G
inst✝³ : Functor H
inst✝² : LawfulFunctor G
inst✝¹ : LawfulFunctor H
inst✝ : LawfulBifunctor F
α✝ : Type u_1
β✝ : Type u_2
x✝ : bicompl F G H α✝ β✝
⊢ bimap id id x✝ = x✝

Tactic:
simp [bimap, map_id, map_comp_map, functor_norm]

Goal state after:
Module: Mathlib.Control.Bifunctor

Goal state before:
pp: case bimap_bimap
F : Type u₀ → Type u₁ → Type u₂
inst✝⁵ : Bifunctor F
G : Type u_1 → Type u₀
H : Type u_2 → Type u₁
inst✝⁴ : Functor G
inst✝³ : Functor H
inst✝² : LawfulFunctor G
inst✝¹ : LawfulFunctor H
inst✝ : LawfulBifunctor F
α₀✝ α₁✝ α₂✝ : Type u_1
β₀✝ β₁✝ β₂✝ : Type u_2
f✝ : α₀✝ → α₁✝
f'✝ : α₁✝ → α₂✝
g✝ : β₀✝ → β₁✝
g'✝ : β₁✝ → β₂✝
x✝ : bicompl F G H α₀✝ β₀✝
⊢ bimap f'✝ g'✝ (bimap f✝ g✝ x✝) = bimap (f'✝ ∘ f✝) (g'✝ ∘ g✝) x✝

Tactic:
simp [bimap, map_id, map_comp_map, functor_norm]

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

Goal state before:
pp: R : Type u
inst✝⁸ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
T : Type u_1
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
inst✝³ : IsLocalization S T
T' : Type u_2
inst✝² : CommSemiring T'
inst✝¹ : Algebra R T'
inst✝ : IsLocalization S T'
x : T
p✝ : LocalizedModule S M
a : R × ↥S := IsLocalization.sec S x
p p' : M × ↥S
s : ↥S
h : s • p'.2 • p.1 = s • p.2 • p'.1
⊢ s • (a.2 * p'.2) • a.1 • p.1 = a.2 • a.1 • s • p'.2 • p.1

Tactic:
by
            simp_rw [Submonoid.smul_def, Submonoid.coe_mul, ← mul_smul]; ring_nf

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Basic

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
T✝ : Monad C
G : Comonad C
F : C ⥤ C
T : Monad C
i : T.toFunctor ≅ F
X : C
⊢ F.map (((i.inv ◫ i.inv) ≫ T.μ ≫ i.hom).app X) ≫ ((i.inv ◫ i.inv) ≫ T.μ ≫ i.hom).app X =
    ((i.inv ◫ i.inv) ≫ T.μ ≫ i.hom).app (F.obj X) ≫ ((i.inv ◫ i.inv) ≫ T.μ ≫ i.hom).app X

Tactic:
simp only [comp_obj, NatTrans.comp_app, NatTrans.hcomp_app, Category.assoc, Functor.map_comp,
      NatTrans.naturality_assoc, hom_inv_id_app_assoc, NatIso.cancel_natIso_inv_left]
    slice_lhs 4 5 => rw [← T.map_comp]
    simp only [hom_inv_id_app, Functor.map_id, id_comp]
    slice_lhs 1 2 => rw [← T.map_comp]
    simp only [Functor.map_comp, Category.assoc]
    congr 1
    simp only [← Category.assoc, NatIso.cancel_natIso_hom_right]
    rw [← T.μ.naturality]
    simp [T.assoc X]

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Basic

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
T✝ : Monad C
G : Comonad C
F : C ⥤ C
T : Monad C
i : T.toFunctor ≅ F
X : C
⊢ (T.η ≫ i.hom).app (F.obj X) ≫ ((i.inv ◫ i.inv) ≫ T.μ ≫ i.hom).app X = 𝟙 ((𝟭 C).obj (F.obj X))

Tactic:
simp only [Functor.id_obj, NatTrans.comp_app, comp_obj, NatTrans.hcomp_app, Category.assoc,
      hom_inv_id_app_assoc]
    slice_lhs 1 2 => rw [← T.η.naturality (i.inv.app X), ]
    simp

Goal state after: