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

Goal state before:
pp: case refine_2.refine_1
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ MonCat
inst✝ : Small.{u, max u v} ↑(F ⋙ forget MonCat).sections
c : Cone (F ⋙ forget MonCat)
t : IsLimit c
this : Small.{u, max u v} ↑(F ⋙ forget MonCat).sections
s✝ : Cone F
x y : ↑s✝.1
⊢ (ConcreteCategory.hom ((Types.Small.limitConeIsLimit (F ⋙ forget MonCat)).lift ((forget MonCat).mapCone s✝)))
      (x * y) =
    (ConcreteCategory.hom ((Types.Small.limitConeIsLimit (F ⋙ forget MonCat)).lift ((forget MonCat).mapCone s✝))) x *
      (ConcreteCategory.hom ((Types.Small.limitConeIsLimit (F ⋙ forget MonCat)).lift ((forget MonCat).mapCone s✝))) y

Tactic:
simp only [Types.Small.limitCone_pt, Functor.comp_obj, Functor.mapCone_pt,
        Types.Small.limitConeIsLimit_lift, Functor.const_obj_obj, Functor.mapCone_π_app,
        ConcreteCategory.hom_ofHom, TypeCat.Fun.coe_mk, map_mul]

Goal state after:
case refine_2.refine_1
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ MonCat
inst✝ : Small.{u, max u v} ↑(F ⋙ forget MonCat).sections
c : Cone (F ⋙ forget MonCat)
t : IsLimit c
this : Small.{u, max u v} ↑(F ⋙ forget MonCat).sections
s✝ : Cone F
x y : ↑s✝.1
⊢ (equivShrink ↑(F ⋙ forget MonCat).sections)
      ⟨fun j ↦ (ConcreteCategory.hom (s✝.π.app j)) x * (ConcreteCategory.hom (s✝.π.app j)) y, ⋯⟩ =
    (equivShrink ↑(F ⋙ forget MonCat).sections) ⟨fun j ↦ (ConcreteCategory.hom (s✝.π.app j)) x, ⋯⟩ *
      (equivShrink ↑(F ⋙ forget MonCat).sections) ⟨fun j ↦ (ConcreteCategory.hom (s✝.π.app j)) y, ⋯⟩
Module: Mathlib.CategoryTheory.Monoidal.Category

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategoryStruct C
id_tensorHom_id : ∀ (X₁ X₂ : C), 𝟙 X₁ ⊗ₘ 𝟙 X₂ = 𝟙 (X₁ ⊗ X₂)
id_tensorHom : ∀ (X : C) {Y₁ Y₂ : C} (f : Y₁ ⟶ Y₂), 𝟙 X ⊗ₘ f = X ◁ f
tensorHom_id : ∀ {X₁ X₂ : C} (f : X₁ ⟶ X₂) (Y : C), f ⊗ₘ 𝟙 Y = f ▷ Y
tensorHom_comp_tensorHom :
  ∀ {X₁ Y₁ Z₁ X₂ Y₂ Z₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (g₁ : Y₁ ⟶ Z₁) (g₂ : Y₂ ⟶ Z₂),
    (f₁ ⊗ₘ f₂) ≫ (g₁ ⊗ₘ g₂) = f₁ ≫ g₁ ⊗ₘ f₂ ≫ g₂
associator_naturality :
  ∀ {X₁ X₂ X₃ Y₁ Y₂ Y₃ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃),
    ((f₁ ⊗ₘ f₂) ⊗ₘ f₃) ≫ (α_ Y₁ Y₂ Y₃).hom = (α_ X₁ X₂ X₃).hom ≫ (f₁ ⊗ₘ f₂ ⊗ₘ f₃)
leftUnitor_naturality : ∀ {X Y : C} (f : X ⟶ Y), (𝟙 (𝟙_ C) ⊗ₘ f) ≫ (λ_ Y).hom = (λ_ X).hom ≫ f
rightUnitor_naturality : ∀ {X Y : C} (f : X ⟶ Y), (f ⊗ₘ 𝟙 (𝟙_ C)) ≫ (ρ_ Y).hom = (ρ_ X).hom ≫ f
pentagon :
  ∀ (W X Y Z : C),
    ((α_ W X Y).hom ⊗ₘ 𝟙 Z) ≫ (α_ W (X ⊗ Y) Z).hom ≫ (𝟙 W ⊗ₘ (α_ X Y Z).hom) =
      (α_ (W ⊗ X) Y Z).hom ≫ (α_ W X (Y ⊗ Z)).hom
triangle : ∀ (X Y : C), (α_ X (𝟙_ C) Y).hom ≫ (𝟙 X ⊗ₘ (λ_ Y).hom) = (ρ_ X).hom ⊗ₘ 𝟙 Y
X✝ Y✝ : C
⊢ (α_ X✝ (𝟙_ C) Y✝).hom ≫ X✝ ◁ (λ_ Y✝).hom = (ρ_ X✝).hom ▷ Y✝

Tactic:
simp [← id_tensorHom, ← tensorHom_id, triangle]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X X' : C
f : X ⟶ X'
⊢ f = (λ_ X).inv ≫ 𝟙_ C ◁ f ≫ (λ_ X').hom

Tactic:
by
  simp only [id_whiskerLeft, assoc, inv_hom_id, comp_id, inv_hom_id_assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Linear.LinearFunctor

Goal state before:
pp: case mpr
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 : C ⥤ D
h : ∀ (X : C) (r : R), F.map (r • 𝟙 X) = r • 𝟙 (F.obj X)
X Y : C
f : X ⟶ Y
r : R
this : r • f = (r • 𝟙 X) ≫ f
⊢ (r • 𝟙 (F.obj X)) ≫ F.map f = r • F.map f

Tactic:
Linear.smul_comp,

Goal state after:
case mpr
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 : C ⥤ D
h : ∀ (X : C) (r : R), F.map (r • 𝟙 X) = r • 𝟙 (F.obj X)
X Y : C
f : X ⟶ Y
r : R
this : r • f = (r • 𝟙 X) ≫ f
⊢ r • 𝟙 (F.obj X) ≫ F.map f = r • F.map f
Module: Mathlib.CategoryTheory.Monoidal.NaturalTransformation

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 G : C ⥤ D
inst✝ : F.Monoidal
e : F ≅ G
⊢ NatTrans.IsMonoidal e.hom

Tactic:
by
  let : G.Monoidal := transport e
  refine ⟨rfl, fun X Y ↦ ?_⟩
  simp [transport_μ, tensorHom_comp_tensorHom_assoc]

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
εIso : 𝟙_ D ≅ F.obj (𝟙_ C)
μIso : (X Y : C) → F.obj X ⊗ F.obj Y ≅ F.obj (X ⊗ Y)
μIso_inv_natural_left :
  ∀ {X Y : C} (f : X ⟶ Y) (X' : C), (μIso X X').inv ≫ F.map f ▷ F.obj X' = F.map (f ▷ X') ≫ (μIso Y X').inv
μIso_inv_natural_right :
  ∀ {X Y : C} (X' : C) (f : X ⟶ Y), (μIso X' X).inv ≫ F.obj X' ◁ F.map f = F.map (X' ◁ f) ≫ (μIso X' Y).inv
oplax_associativity :
  ∀ (X Y Z : C),
    (μIso (X ⊗ Y) Z).inv ≫ (μIso X Y).inv ▷ F.obj Z ≫ (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom =
      F.map (α_ X Y Z).hom ≫ (μIso X (Y ⊗ Z)).inv ≫ F.obj X ◁ (μIso Y Z).inv
oplax_left_unitality : ∀ (X : C), (λ_ (F.obj X)).inv = F.map (λ_ X).inv ≫ (μIso (𝟙_ C) X).inv ≫ εIso.inv ▷ F.obj X
oplax_right_unitality : ∀ (X : C), (ρ_ (F.obj X)).inv = F.map (ρ_ X).inv ≫ (μIso X (𝟙_ C)).inv ≫ F.obj X ◁ εIso.inv
X : C
⊢ (λ_ (F.obj X)).hom = εIso.hom ▷ F.obj X ≫ (μIso (𝟙_ C) X).hom ≫ F.map (λ_ X).hom

Tactic:
rw [← cancel_mono (λ_ (F.obj X)).inv, Iso.hom_inv_id, oplax_left_unitality]

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
εIso : 𝟙_ D ≅ F.obj (𝟙_ C)
μIso : (X Y : C) → F.obj X ⊗ F.obj Y ≅ F.obj (X ⊗ Y)
μIso_inv_natural_left :
  ∀ {X Y : C} (f : X ⟶ Y) (X' : C), (μIso X X').inv ≫ F.map f ▷ F.obj X' = F.map (f ▷ X') ≫ (μIso Y X').inv
μIso_inv_natural_right :
  ∀ {X Y : C} (X' : C) (f : X ⟶ Y), (μIso X' X).inv ≫ F.obj X' ◁ F.map f = F.map (X' ◁ f) ≫ (μIso X' Y).inv
oplax_associativity :
  ∀ (X Y Z : C),
    (μIso (X ⊗ Y) Z).inv ≫ (μIso X Y).inv ▷ F.obj Z ≫ (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom =
      F.map (α_ X Y Z).hom ≫ (μIso X (Y ⊗ Z)).inv ≫ F.obj X ◁ (μIso Y Z).inv
oplax_left_unitality : ∀ (X : C), (λ_ (F.obj X)).inv = F.map (λ_ X).inv ≫ (μIso (𝟙_ C) X).inv ≫ εIso.inv ▷ F.obj X
oplax_right_unitality : ∀ (X : C), (ρ_ (F.obj X)).inv = F.map (ρ_ X).inv ≫ (μIso X (𝟙_ C)).inv ≫ F.obj X ◁ εIso.inv
X : C
⊢ 𝟙 (𝟙_ D ⊗ F.obj X) =
    (εIso.hom ▷ F.obj X ≫ (μIso (𝟙_ C) X).hom ≫ F.map (λ_ X).hom) ≫
      F.map (λ_ X).inv ≫ (μIso (𝟙_ C) X).inv ≫ εIso.inv ▷ F.obj X
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✝ F : C ⥤ D
G : E ⥤ C'
inst✝² : MonoidalCategory C'
inst✝¹ : F.Monoidal
inst✝ : G.Monoidal
x✝¹ x✝ : C × E
⊢ μ (F.prod G) x✝¹ x✝ ≫ δ (F.prod G) x✝¹ x✝ = 𝟙 ((F.prod G).obj x✝¹ ⊗ (F.prod G).obj x✝)

Tactic:
ext <;> apply Monoidal.μ_δ

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 : E ⥤ C'
inst✝² : MonoidalCategory C'
inst✝¹ : F.Monoidal
inst✝ : G.Monoidal
x✝¹ x✝ : C × E
⊢ (δ (F.prod G) x✝¹ x✝ ≫ μ (F.prod G) x✝¹ x✝).1 = (𝟙 ((F.prod G).obj (x✝¹ ⊗ x✝))).1

Tactic:
apply Monoidal.δ_μ

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 : E ⥤ C'
inst✝² : MonoidalCategory C'
inst✝¹ : F.Monoidal
inst✝ : G.Monoidal
x✝¹ x✝ : C × E
⊢ (δ (F.prod G) x✝¹ x✝ ≫ μ (F.prod G) x✝¹ x✝).2 = (𝟙 ((F.prod G).obj (x✝¹ ⊗ x✝))).2

Tactic:
apply Monoidal.δ_μ

Goal state after:
Module: Mathlib.Algebra.Category.AlgCat.TensorAlgebra

Goal state before:
pp: R : Type u
inst✝ : CommRing R
heq :
  forget₂ (AlgCat ℤ) (ModuleCat ℤ) ⋙ forget₂ (ModuleCat ℤ) AddCommGrpCat =
    forget₂ (AlgCat ℤ) RingCat ⋙ forget₂ RingCat AddCommGrpCat
⊢ (forget₂ (AlgCat ℤ) RingCat ⋙ forget₂ RingCat AddCommGrpCat).IsRightAdjoint

Tactic:
rw [← heq]

Goal state after:
R : Type u
inst✝ : CommRing R
heq :
  forget₂ (AlgCat ℤ) (ModuleCat ℤ) ⋙ forget₂ (ModuleCat ℤ) AddCommGrpCat =
    forget₂ (AlgCat ℤ) RingCat ⋙ forget₂ RingCat AddCommGrpCat
⊢ (forget₂ (AlgCat ℤ) (ModuleCat ℤ) ⋙ forget₂ (ModuleCat ℤ) AddCommGrpCat).IsRightAdjoint
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

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

Tactic:
pow_zero,

Goal state after:
R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : AddMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
n : ℕ
h : x.snd <• x.fst = x.fst •> x.snd
⊢ (List.map (fun i ↦ x.fst ^ (0 - i + i) •> x.snd) (List.range 0)).sum = 0 •> 1 •> x.snd
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₂
α : R₁ ⟶ R₂
d : D
| L₂.map (α.app d) ≫ adj₂.counit.app d

Tactic:
← (conjugateEquiv adj₁ adj₂).right_inv α

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₂
α : R₁ ⟶ R₂
d : D
| L₂.map (((conjugateEquiv adj₁ adj₂).toFun ((conjugateEquiv adj₁ adj₂).invFun α)).app d) ≫ adj₂.counit.app d
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₂
α : R₁ ⟶ R₂
c : C
| adj₁.unit.app c ≫ α.app (L₁.obj c)

Tactic:
← (conjugateEquiv adj₁ adj₂).right_inv α

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₂
α : R₁ ⟶ R₂
c : C
| adj₁.unit.app c ≫ ((conjugateEquiv adj₁ adj₂).toFun ((conjugateEquiv adj₁ adj₂).invFun α)).app (L₁.obj c)
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

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

Tactic:
rw [fst_inv, fst_mul, fst_mul, mul_inv_rev, fst_inv, fst_inv]

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

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

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 * b)⁻¹.snd = (b⁻¹ * a⁻¹).snd

Tactic:
· rw [fst_inv, fst_mul, fst_mul, mul_inv_rev, fst_inv, fst_inv]

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
⊢ (a * b)⁻¹.snd = (b⁻¹ * a⁻¹).snd
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: case hr
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.map (counit ∘ₗ inr R A B) (inr R A B) ∘ₗ comul = (TensorProduct.mk R R (A × B)) 1 ∘ₗ inr R A B

Tactic:
counit_comp_inr,

Goal state after:
case hr
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.map counit (inr R A B) ∘ₗ comul = (TensorProduct.mk R R (A × B)) 1 ∘ₗ inr R A B
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: case hr
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.map (inr R A B) (counit ∘ₗ inr R A B) ∘ₗ comul = (TensorProduct.mk R (A × B) R).flip 1 ∘ₗ inr R A B

Tactic:
counit_comp_inr,

Goal state after:
case hr
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.map (inr R A B) counit ∘ₗ comul = (TensorProduct.mk R (A × B) R).flip 1 ∘ₗ inr R A B
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
X : ModuleCat R
Y : ModuleCat S
g : X ⟶ (restrictScalars f).obj Y
x✝ : ↑((restrictScalars f).obj (of S S))
y✝ : ↑X
⊢ (Hom.hom (ExtendRestrictScalarsAdj.HomEquiv.fromExtendScalars f g)) (x✝ ⊗ₜ[R] y✝) =
    (lift { toFun := fun s ↦ { toFun := fun y ↦ s • y, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯, map_smul' := ⋯ })
      (x✝ ⊗ₜ[R] (ConcreteCategory.hom g) y✝)

Tactic:
ExtendRestrictScalarsAdj.HomEquiv.fromExtendScalars_hom_apply

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
X : ModuleCat R
Y : ModuleCat S
g : X ⟶ (restrictScalars f).obj Y
x✝ : ↑((restrictScalars f).obj (of S S))
y✝ : ↑X
⊢ (lift { toFun := fun s ↦ ExtendRestrictScalarsAdj.HomEquiv.evalAt f s g, map_add' := ⋯, map_smul' := ⋯ })
      (x✝ ⊗ₜ[R] y✝) =
    (lift { toFun := fun s ↦ ExtendRestrictScalarsAdj.HomEquiv.evalAt f s g, map_add' := ⋯, map_smul' := ⋯ })
      (x✝ ⊗ₜ[R] y✝)
Module: Mathlib.Order.Category.Semilat

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

Tactic:
ext; exact e.apply_symm_apply _

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

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

Tactic:
ext; exact e.apply_symm_apply _

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

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

Tactic:
ext; exact e.apply_symm_apply _

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

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

Tactic:
ext; exact e.apply_symm_apply _

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

Goal state before:
pp: α β : HeytAlg
e : ↑α ≃o ↑β
⊢ ofHom { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯, map_bot' := ⋯, map_himp' := ⋯ } ≫
      ofHom { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯, map_bot' := ⋯, map_himp' := ⋯ } =
    𝟙 β

Tactic:
ext; exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Algebra.Category.BoolRing

Goal state before:
pp: α β : BoolRing
e : ↑α ≃+* ↑β
⊢ { hom' := ↑e.symm } ≫ { hom' := ↑e } = 𝟙 β

Tactic:
ext; exact e.apply_symm_apply _

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : WfDvdMonoid α
a₀ x : α
h : a₀ ≠ 0
hx : ¬IsUnit x
⊢ x ^ 0 * a₀ = a₀

Tactic:
pow_zero,

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : WfDvdMonoid α
a₀ x : α
h : a₀ ≠ 0
hx : ¬IsUnit x
⊢ 1 * a₀ = a₀
Module: Mathlib.RingTheory.Jacobson.Radical

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
h : jacobson R (M ⧸ N) = ⊥
⊢ jacobson R M ≤ N.mkQ.ker

Tactic:
← comap_bot,

Goal state after:
R : Type u_1
M : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
h : jacobson R (M ⧸ N) = ⊥
⊢ jacobson R M ≤ comap N.mkQ ⊥
Module: Mathlib.RingTheory.Jacobson.Ideal

Goal state before:
pp: case mpr
R : Type u
inst✝ : Ring R
I : Ideal R
h : ∀ x ∉ I, ∃ M, (I ≤ M ∧ M.IsMaximal) ∧ x ∉ M
x : R
hx : x ∉ I
⊢ ¬∀ ⦃I_1 : Ideal R⦄, I_1 ∈ {J | I ≤ J ∧ J.IsMaximal} → x ∈ I_1

Tactic:
push Not

Goal state after:
case mpr
R : Type u
inst✝ : Ring R
I : Ideal R
h : ∀ x ∉ I, ∃ M, (I ≤ M ∧ M.IsMaximal) ∧ x ∉ M
x : R
hx : x ∉ I
⊢ ∃ I_1 ∈ {J | I ≤ J ∧ J.IsMaximal}, x ∉ I_1
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
⊢ x = y

Tactic:
by
  suffices Module.eqIdeal R x y = ⊤ by simpa [Module.eqIdeal] using (Ideal.eq_top_iff_one _).mp this
  by_contra ne
  have ⟨r, hrs, disj⟩ := Ideal.exists_disjoint_powers_of_span_eq_top s span_eq _ ne
  let r : s := ⟨r, hrs⟩
  have ⟨⟨_, n, rfl⟩, eq⟩ := (IsLocalization.eq_iff_exists (.powers r.1) _).mp (congr_fun eq r)
  exact Set.disjoint_left.mp disj eq ⟨n, rfl⟩

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

Goal state before:
pp: case refine_1
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
hf : Function.Surjective ⇑f
K : Ideal S
⊢ comap f (sInf {J | K ≤ J ∧ J.IsMaximal}) ≤ sInf {J | comap f K ≤ J ∧ J.IsMaximal}

pp: case refine_2
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
hf : Function.Surjective ⇑f
K : Ideal S
⊢ sInf {J | comap f K ≤ J ∧ J.IsMaximal} ≤ comap f (sInf {J | K ≤ J ∧ J.IsMaximal})

Tactic:
· rw [← top_inf_eq (sInf _), ← sInf_insert, comap_sInf', sInf_eq_iInf]
    refine iInf_le_iInf_of_subset fun J hJ => ?_
    have : comap f (map f J) = J :=
      Trans.trans (comap_map_of_surjective f hf J)
        (le_antisymm (sup_le_iff.2 ⟨le_of_eq rfl, le_trans (comap_mono bot_le) hJ.left⟩)
          le_sup_left)
    rcases map_eq_top_or_isMaximal_of_surjective _ hf hJ.right with htop | hmax
    · exact ⟨⊤, Set.mem_insert ⊤ _, htop ▸ this⟩
    · exact ⟨map f J, Set.mem_insert_of_mem _ ⟨le_map_of_comap_le_of_surjective f hf hJ.1, hmax⟩,
        this⟩

Goal state after:
case refine_2
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
hf : Function.Surjective ⇑f
K : Ideal S
⊢ sInf {J | comap f K ≤ J ∧ J.IsMaximal} ≤ comap f (sInf {J | K ≤ J ∧ J.IsMaximal})
Module: Mathlib.RingTheory.Jacobson.Ideal

Goal state before:
pp: R : Type u
inst✝ : Ring R
I J : Ideal R
⊢ I ≤ J → I.jacobson ≤ J.jacobson

Tactic:
by
  intro h x hx
  rw [jacobson, mem_sInf] at hx ⊢
  exact fun K ⟨hK, hK_max⟩ => hx ⟨Trans.trans h hK, hK_max⟩

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

Goal state before:
pp: case pos
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}
r𝔪 : r ∈ 𝔪
⊢ x * r ∈ 𝔪

Tactic:
apply 𝔪.smul_mem _ r𝔪

Goal state after:
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
tfae_1_to_2 : IsLocalHom f → ⇑f '' ↑(maximalIdeal R) ⊆ ↑(maximalIdeal S)
⊢ [IsLocalHom f, ⇑f '' ↑(maximalIdeal R) ⊆ ↑(maximalIdeal S), Ideal.map f (maximalIdeal R) ≤ maximalIdeal S,
      maximalIdeal R ≤ Ideal.comap f (maximalIdeal S), Ideal.comap f (maximalIdeal S) = maximalIdeal R].TFAE

Tactic:
tfae_have 2 → 4 := Set.image_subset_iff.1

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommSemiring R
inst✝² : IsLocalRing R
inst✝¹ : CommSemiring S
inst✝ : IsLocalRing S
f : R →+* S
tfae_1_to_2 : IsLocalHom f → ⇑f '' ↑(maximalIdeal R) ⊆ ↑(maximalIdeal S)
tfae_2_to_4 : ⇑f '' ↑(maximalIdeal R) ⊆ ↑(maximalIdeal S) → maximalIdeal R ≤ Ideal.comap f (maximalIdeal S)
⊢ [IsLocalHom f, ⇑f '' ↑(maximalIdeal R) ⊆ ↑(maximalIdeal S), Ideal.map f (maximalIdeal R) ≤ maximalIdeal S,
      maximalIdeal R ≤ Ideal.comap f (maximalIdeal S), Ideal.comap f (maximalIdeal S) = maximalIdeal R].TFAE
Module: Mathlib.CategoryTheory.Limits.Shapes.StrictInitial

Goal state before:
pp: case refine_2
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
⊢ ∀ ⦃X Y : J⦄ (f : X ⟶ Y),
    (((Functor.const J).obj (F.1 i)).map f ≫
        if h : Y = i then eqToHom ⋯ else (H Y h).from (((Functor.const J).obj (F.1 i)).obj Y)) =
      (if h : X = i then eqToHom ⋯ else (H X h).from (((Functor.const J).obj (F.1 i)).obj X)) ≫ F.map f

Tactic:
intro j k f
      split_ifs with h h_1 h_1
      · cases h
        cases h_1
        obtain rfl : f = 𝟙 _ := Subsingleton.elim _ _
        simp
      · cases h
        have : IsIso (F.map f) := (H _ h_1).isIso_from _
        rw [← IsIso.comp_inv_eq]
        apply (H _ h_1).hom_ext
      · cases h_1
        apply (H _ h).hom_ext
      · apply (H _ h).hom_ext

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

Goal state before:
pp: case h
R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
a : R
b : S
b' : R
hb : (algebraMap R S) b' = b
⊢ (algebraMap R S) (a * b') = a • b

Tactic:
← hb,

Goal state after:
case h
R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
a : R
b : S
b' : R
hb : (algebraMap R S) b' = b
⊢ (algebraMap R S) (a * b') = a • (algebraMap R S) b'
Module: Mathlib.RingTheory.Localization.Integer

Goal state before:
pp: case refine_2
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
s : Finset ι
f : ι → S
this : (a : Prop) → Decidable a
i : ι
hi : i ∈ s
⊢ (algebraMap R S) ↑(∏ j ∈ s.erase i, (sec M (f j)).2) * (algebraMap R S) (sec M (f i)).1 =
    ↑(∏ i ∈ s, (sec M (f i)).2) • f i

Tactic:
sec_spec',

Goal state after:
case refine_2
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
s : Finset ι
f : ι → S
this : (a : Prop) → Decidable a
i : ι
hi : i ∈ s
⊢ (algebraMap R S) ↑(∏ j ∈ s.erase i, (sec M (f j)).2) * ((algebraMap R S) ↑(sec M (f i)).2 * f i) =
    ↑(∏ i ∈ s, (sec M (f i)).2) • f i