mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.ConcreteCategory.EpiMono

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
inst✝² : HasStrongEpiMonoFactorisations C
inst✝¹ : (forget C).PreservesMonomorphisms
inst✝ : (forget C).PreservesEpimorphisms
⊢ monomorphisms C ≤ MorphismProperty.injective C

Tactic:
injective_eq_monomorphisms

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
inst✝² : HasStrongEpiMonoFactorisations C
inst✝¹ : (forget C).PreservesMonomorphisms
inst✝ : (forget C).PreservesEpimorphisms
⊢ monomorphisms C ≤ monomorphisms C
Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic

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

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

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

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

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

Tactic:
← tensorHom_comp_tensorHom,

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

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

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

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

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ : C
⊢ (λ_ (X₁ ⊗ X₂)).hom =
    (((𝟙_ C ◁ (λ_ X₁).inv ▷ X₂ ≫ 𝟙_ C ◁ (β_ (𝟙_ C) X₁).hom ▷ X₂) ≫ 𝟙_ C ◁ (α_ X₁ (𝟙_ C) X₂).hom) ≫
        (α_ (𝟙_ C) X₁ (𝟙_ C ⊗ X₂)).inv) ≫
      ((λ_ X₁).hom ⊗ₘ (λ_ X₂).hom)

Tactic:
slice_rhs 1 2 => rw [← whiskerLeft_comp, ← comp_whiskerRight,
    leftUnitor_inv_braiding]

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ : C
⊢ (λ_ (X₁ ⊗ X₂)).hom =
    ((𝟙_ C ◁ (ρ_ X₁).inv ▷ X₂ ≫ 𝟙_ C ◁ (α_ X₁ (𝟙_ C) X₂).hom) ≫ (α_ (𝟙_ C) X₁ (𝟙_ C ⊗ X₂)).inv) ≫
      ((λ_ X₁).hom ⊗ₘ (λ_ X₂).hom)
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 ^ (n.pred - i) •> x.snd <• x.fst ^ i) (List.range n)).sum = n •> x.fst ^ n.pred •> x.snd

Tactic:
← smul_comm (_ : R) (_ : Rᵐᵒᵖ),

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 ^ (n.pred - i) •> (x.snd <• x.fst ^ i)) (List.range n)).sum = n •> x.fst ^ n.pred •> x.snd
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
⊢ (mateEquiv (adj₁.comp adj₃) (adj₂.comp adj₄)) (α ≫ᵥ β) = (mateEquiv adj₃ adj₄) β ≫ₕ (mateEquiv adj₁ adj₂) α

Tactic:
by
  unfold vComp hComp mateEquiv Adjunction.comp
  ext c
  simp only [comp_obj, whiskerRight_comp, assoc, mk'_unit, whiskerLeft_comp, mk'_counit,
    whiskerRight_twice, Iso.inv_hom_id_assoc, Equiv.coe_fn_mk, comp_app, id_obj,
    rightUnitor_inv_app, Functor.whiskerLeft_app, Functor.whiskerRight_app, map_id,
    associator_inv_app, associator_hom_app, Functor.comp_map, rightUnitor_hom_app,
    leftUnitor_hom_app, comp_id, id_comp, whiskerLeft_twice, Iso.hom_inv_id_assoc]
  slice_rhs 2 4 =>
    rw [← R₂.map_comp, ← R₂.map_comp, ← assoc, ← unit_naturality (adj₄)]
  rw [R₂.map_comp, L₄.map_comp, R₄.map_comp, R₂.map_comp]
  slice_rhs 4 5 =>
    rw [← R₂.map_comp, ← R₄.map_comp, ← Functor.comp_map _ L₄, β.naturality]
  simp only [comp_obj, Functor.comp_map, map_comp, assoc]

Goal state after:
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 ^ (Nat.pred 0 - i + i) •> x.snd) (List.range 0)).sum = 0 •> x.fst ^ Nat.pred 0 •> x.snd

Tactic:
rw [Nat.pred_zero, pow_zero, List.range_zero, zero_smul, List.map_nil, List.sum_nil]

Goal state after:
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₆
X : Type u₇
Y : Type u₈
Z : 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
inst✝² : Category.{v₇, u₇} X
inst✝¹ : Category.{v₈, u₈} Y
inst✝ : Category.{v₉, u₉} Z
G₁ : A ⥤ D
H₁ : B ⥤ E
K₁ : C ⥤ F
G₂ : D ⥤ X
H₂ : E ⥤ Y
K₂ : F ⥤ Z
L₁ : A ⥤ B
R₁ : B ⥤ A
L₂ : B ⥤ C
R₂ : C ⥤ B
L₃ : D ⥤ E
R₃ : E ⥤ D
L₄ : E ⥤ F
R₄ : F ⥤ E
L₅ : X ⥤ Y
R₅ : Y ⥤ X
L₆ : Y ⥤ Z
R₆ : Z ⥤ Y
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
adj₄ : L₄ ⊣ R₄
adj₅ : L₅ ⊣ R₅
adj₆ : L₆ ⊣ R₆
α : TwoSquare G₁ L₁ L₃ H₁
β : TwoSquare H₁ L₂ L₄ K₁
γ : TwoSquare G₂ L₃ L₅ H₂
δ : TwoSquare H₂ L₄ L₆ K₂
⊢ (mateEquiv (adj₁.comp adj₂) (adj₅.comp adj₆)) ((α ≫ᵥ β) ≫ₕ γ ≫ᵥ δ) =
    ((mateEquiv adj₂ adj₄) β ≫ₕ (mateEquiv adj₁ adj₃) α) ≫ᵥ (mateEquiv adj₄ adj₆) δ ≫ₕ (mateEquiv adj₃ adj₅) γ

Tactic:
have vcomp :=
    mateEquiv_vcomp (adj₁.comp adj₂) (adj₃.comp adj₄) (adj₅.comp adj₆) (α ≫ᵥ β) (γ ≫ᵥ δ)

Goal state after:
A : Type u₁
B : Type u₂
C : Type u₃
D : Type u₄
E : Type u₅
F : Type u₆
X : Type u₇
Y : Type u₈
Z : 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
inst✝² : Category.{v₇, u₇} X
inst✝¹ : Category.{v₈, u₈} Y
inst✝ : Category.{v₉, u₉} Z
G₁ : A ⥤ D
H₁ : B ⥤ E
K₁ : C ⥤ F
G₂ : D ⥤ X
H₂ : E ⥤ Y
K₂ : F ⥤ Z
L₁ : A ⥤ B
R₁ : B ⥤ A
L₂ : B ⥤ C
R₂ : C ⥤ B
L₃ : D ⥤ E
R₃ : E ⥤ D
L₄ : E ⥤ F
R₄ : F ⥤ E
L₅ : X ⥤ Y
R₅ : Y ⥤ X
L₆ : Y ⥤ Z
R₆ : Z ⥤ Y
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
adj₄ : L₄ ⊣ R₄
adj₅ : L₅ ⊣ R₅
adj₆ : L₆ ⊣ R₆
α : TwoSquare G₁ L₁ L₃ H₁
β : TwoSquare H₁ L₂ L₄ K₁
γ : TwoSquare G₂ L₃ L₅ H₂
δ : TwoSquare H₂ L₄ L₆ K₂
vcomp :
  (mateEquiv (adj₁.comp adj₂) (adj₅.comp adj₆)) ((α ≫ᵥ β) ≫ₕ γ ≫ᵥ δ) =
    (mateEquiv (adj₁.comp adj₂) (adj₃.comp adj₄)) (α ≫ᵥ β) ≫ᵥ (mateEquiv (adj₃.comp adj₄) (adj₅.comp adj₆)) (γ ≫ᵥ δ)
⊢ (mateEquiv (adj₁.comp adj₂) (adj₅.comp adj₆)) ((α ≫ᵥ β) ≫ₕ γ ≫ᵥ δ) =
    ((mateEquiv adj₂ adj₄) β ≫ₕ (mateEquiv adj₁ adj₃) α) ≫ᵥ (mateEquiv adj₄ adj₆) δ ≫ₕ (mateEquiv adj₃ adj₅) γ
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✝ : ℕ
⊢ x.fst ^ (n✝ + 1) •> x.snd +
      (List.map (fun i ↦ x.fst ^ (n✝ - i) •> x.snd <• x.fst ^ i.succ) (List.range (n✝ + 1))).sum =
    x.fst ^ (n✝ + 1) •> x.snd +
      (List.map (fun x_1 ↦ x.fst ^ (n✝ - x_1) •> x.snd <• x.fst ^ x_1 <• x.fst) (List.range (n✝ + 1))).sum

Tactic:
← smul_comm (_ : R) (_ : Rᵐᵒᵖ),

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) •> x.snd +
      (List.map (fun i ↦ x.fst ^ (n✝ - i) •> (x.snd <• x.fst ^ i.succ)) (List.range (n✝ + 1))).sum =
    x.fst ^ (n✝ + 1) •> x.snd +
      (List.map (fun x_1 ↦ x.fst ^ (n✝ - x_1) •> (x.snd <• x.fst ^ x_1 <• x.fst)) (List.range (n✝ + 1))).sum
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: case cons
R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : AddCommMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
xs : List (tsze R M)
ih :
  xs.prod.snd =
    (List.map (fun x ↦ (List.take x.2 (List.map fst xs)).prod •> x.1.snd <• (List.drop x.2.succ (List.map fst xs)).prod)
        xs.zipIdx).sum
⊢ (x :: xs).prod.snd =
    ((List.take 0 (x.fst :: List.map fst xs)).prod •> x.snd <•
          (List.drop (Nat.succ 0) (x.fst :: List.map fst xs)).prod ::
        List.map
          (fun x_1 ↦
            (List.take (x_1.2 + 1) (x.fst :: List.map fst xs)).prod •> (id x_1.1).snd <•
              (List.drop (x_1.2 + 1).succ (x.fst :: List.map fst xs)).prod)
          xs.zipIdx).sum

Tactic:
id,

Goal state after:
case cons
R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : AddCommMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
xs : List (tsze R M)
ih :
  xs.prod.snd =
    (List.map (fun x ↦ (List.take x.2 (List.map fst xs)).prod •> x.1.snd <• (List.drop x.2.succ (List.map fst xs)).prod)
        xs.zipIdx).sum
⊢ (x :: xs).prod.snd =
    ((List.take 0 (x.fst :: List.map fst xs)).prod •> x.snd <•
          (List.drop (Nat.succ 0) (x.fst :: List.map fst xs)).prod ::
        List.map
          (fun x_1 ↦
            (List.take (x_1.2 + 1) (x.fst :: List.map fst xs)).prod •> x_1.1.snd <•
              (List.drop (x_1.2 + 1).succ (x.fst :: List.map fst xs)).prod)
          xs.zipIdx).sum
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
X : ModuleCat R
r : R
x : ↑X
m1 : Module R S := Module.compHom S f
⊢ (r • 1) ⊗ₜ[R] x = r • 1 ⊗ₜ[R] x

Tactic:
TensorProduct.smul_tmul'

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
X : ModuleCat R
r : R
x : ↑X
m1 : Module R S := Module.compHom S f
⊢ (r • 1) ⊗ₜ[R] x = (r • 1) ⊗ₜ[R] x
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 Y' : ModuleCat S
g : Y ⟶ Y'
m1 : Module R S := Module.compHom S f
m2 : Module R ↑Y := Module.compHom (↑Y) f
⊢ (restrictScalars f ⋙ extendScalars f).map g ≫ Counit.map f = Counit.map f ≫ (𝟭 (ModuleCat S)).map g

Tactic:
let m2 : Module R Y' := Module.compHom Y' f

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 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
⊢ (restrictScalars f ⋙ extendScalars f).map g ≫ Counit.map f = Counit.map f ≫ (𝟭 (ModuleCat S)).map g
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: R₁ R₂ R₃ : Type u₁
inst✝² : CommRing R₁
inst✝¹ : CommRing R₂
inst✝ : CommRing R₃
f₁₂ : R₁ →+* R₂
f₂₃ : R₂ →+* R₃
M : ModuleCat R₁
m : ↑M
⊢ (ConcreteCategory.hom ((extendScalarsComp f₁₂ f₂₃).hom.app M)) (1 ⊗ₜ[R₁] m) = 1 ⊗ₜ[R₂] (1 ⊗ₜ[R₁] m)

Tactic:
by
  rw [← extendRestrictScalarsAdj_homEquiv_apply, homEquiv_extendScalarsComp]
  rfl

Goal state after:
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' F'' : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
adj2 : F' ⊣ G
adj3 : F'' ⊣ G
x : C
⊢ (adj1.leftAdjointUniq adj2).hom.app x ≫ (adj2.leftAdjointUniq adj3).hom.app x = (adj1.leftAdjointUniq adj3).hom.app x

Tactic:
by
  rw [← leftAdjointUniq_trans adj1 adj2 adj3]
  rfl

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : Ring R₂
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
hf : Function.Bijective ⇑f
⊢ f.ker ≤ jacobson R M

Tactic:
LinearMap.ker_eq_bot.mpr hf.1,

Goal state after:
R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : Ring R₂
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
hf : Function.Bijective ⇑f
⊢ ⊥ ≤ jacobson R M
Module: Mathlib.RingTheory.TwoSidedIdeal.Operations

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
I : Ideal R
x : R
⊢ x ∈ fromIdeal I ↔ x ∈ span ↑I

Tactic:
by simp [fromIdeal]

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

Goal state before:
pp: case e'_3
R : Type u_1
inst✝² : Ring R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
ne_bot : Nontrivial ↥N
fg : Module.Finite R ↥N
⊢ Ring.jacobson R • N = Submodule.map N.subtype (Ring.jacobson R • ⊤)

pp: case e'_4
R : Type u_1
inst✝² : Ring R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
ne_bot : Nontrivial ↥N
fg : Module.Finite R ↥N
⊢ N = Submodule.map N.subtype ⊤

Tactic:
on_goal 1 => rw [map_smul'']

Goal state after:
case e'_3
R : Type u_1
inst✝² : Ring R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
ne_bot : Nontrivial ↥N
fg : Module.Finite R ↥N
⊢ Ring.jacobson R • N = Ring.jacobson R • Submodule.map N.subtype ⊤

case e'_4
R : Type u_1
inst✝² : Ring R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
ne_bot : Nontrivial ↥N
fg : Module.Finite R ↥N
⊢ N = Submodule.map N.subtype ⊤
Module: Mathlib.RingTheory.Jacobson.Ideal

Goal state before:
pp: case mp
R : Type u
inst✝ : CommRing R
I : Ideal R
hf : Function.Surjective ⇑(Quotient.mk I)
⊢ I.jacobson = I → ⊥.jacobson = ⊥

Tactic:
intro h
    replace h := congr_arg (Ideal.map (Ideal.Quotient.mk I)) h
    rw [map_jacobson_of_surjective hf (le_of_eq mk_ker)] at h
    simpa using h

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
s : Finset R
f : (a : ↑↑s) → Away ↑a
h : ∀ (a b : ↑↑s), (Away.awayToAwayRight ↑a ↑b) (f a) = (Away.awayToAwayLeft ↑b ↑a) (f b)
mem : 1 ∈ Ideal.span ↑s
span_eq : Ideal.span ↑s = ⊤
n : ↑↑s → ℕ
r✝¹ : ↑↑s → R
eq✝¹ : ∀ (a : ↑↑s), f a * (algebraMap R (Away ↑a)) ↑a ^ n a = (algebraMap R (Away ↑a)) (r✝¹ a)
N✝ : ℕ := s.attach.sup n
r✝ : ↑↑s → R := fun a ↦ ↑a ^ (N✝ - n a) * r✝¹ a
eq✝ : ∀ (a : ↑↑s), f a * (algebraMap R (Away ↑a)) (↑a ^ N✝) = (algebraMap R (Away ↑a)) (r✝ a)
N'✝ : ↑↑s → ↑↑s → ℕ
hN' : ∀ (a b : ↑↑s), (↑a * ↑b) ^ N'✝ a b * (r✝ a * ↑b ^ N✝) = (↑a * ↑b) ^ N'✝ a b * (r✝ b * ↑a ^ N✝)
N' : ℕ := (s ×ˢ s).attach.sup fun a ↦ N'✝ ⟨(↑a).1, ⋯⟩ ⟨(↑a).2, ⋯⟩
eq2✝ : ∀ (a b : ↑↑s), (↑a * ↑b) ^ N' * (r✝ a * ↑b ^ N✝) = (↑a * ↑b) ^ N' * (r✝ b * ↑a ^ N✝)
N : ℕ := N' + N✝
r : ↑↑s → R := fun a ↦ ↑a ^ N' * r✝ a
eq : ∀ (a : ↑↑s), f a * (algebraMap R (Away ↑a)) (↑a ^ N) = (algebraMap R (Away ↑a)) (r a)
eq2 : ∀ (a b : ↑↑s), r a * ↑b ^ N = r b * ↑a ^ N
c : ↑↑s → R
eq1 : ∑ i, c i • ↑i ^ N = 1
a : ↑↑s
⊢ (algebraMap R (Away ↑a)) (∑ x, c x * (r x * ↑a ^ N)) = (algebraMap R (Away ↑a)) (r a)

Tactic:
eq2 _ a,

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
s : Finset R
f : (a : ↑↑s) → Away ↑a
h : ∀ (a b : ↑↑s), (Away.awayToAwayRight ↑a ↑b) (f a) = (Away.awayToAwayLeft ↑b ↑a) (f b)
mem : 1 ∈ Ideal.span ↑s
span_eq : Ideal.span ↑s = ⊤
n : ↑↑s → ℕ
r✝¹ : ↑↑s → R
eq✝¹ : ∀ (a : ↑↑s), f a * (algebraMap R (Away ↑a)) ↑a ^ n a = (algebraMap R (Away ↑a)) (r✝¹ a)
N✝ : ℕ := s.attach.sup n
r✝ : ↑↑s → R := fun a ↦ ↑a ^ (N✝ - n a) * r✝¹ a
eq✝ : ∀ (a : ↑↑s), f a * (algebraMap R (Away ↑a)) (↑a ^ N✝) = (algebraMap R (Away ↑a)) (r✝ a)
N'✝ : ↑↑s → ↑↑s → ℕ
hN' : ∀ (a b : ↑↑s), (↑a * ↑b) ^ N'✝ a b * (r✝ a * ↑b ^ N✝) = (↑a * ↑b) ^ N'✝ a b * (r✝ b * ↑a ^ N✝)
N' : ℕ := (s ×ˢ s).attach.sup fun a ↦ N'✝ ⟨(↑a).1, ⋯⟩ ⟨(↑a).2, ⋯⟩
eq2✝ : ∀ (a b : ↑↑s), (↑a * ↑b) ^ N' * (r✝ a * ↑b ^ N✝) = (↑a * ↑b) ^ N' * (r✝ b * ↑a ^ N✝)
N : ℕ := N' + N✝
r : ↑↑s → R := fun a ↦ ↑a ^ N' * r✝ a
eq : ∀ (a : ↑↑s), f a * (algebraMap R (Away ↑a)) (↑a ^ N) = (algebraMap R (Away ↑a)) (r a)
eq2 : ∀ (a b : ↑↑s), r a * ↑b ^ N = r b * ↑a ^ N
c : ↑↑s → R
eq1 : ∑ i, c i • ↑i ^ N = 1
a : ↑↑s
⊢ (algebraMap R (Away ↑a)) (∑ x, c x * (r a * ↑x ^ N)) = (algebraMap R (Away ↑a)) (r a)
Module: Mathlib.Algebra.Module.LocalizedModule.IsLocalization

Goal state before:
pp: case refine_2
R : Type u_1
inst✝⁶ : CommSemiring R
S : Submonoid R
A : Type u_2
Aₛ : Type u_3
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : CommSemiring Aₛ
inst✝² : Algebra A Aₛ
inst✝¹ : Algebra R Aₛ
inst✝ : IsScalarTower R A Aₛ
x✝ : Aₛ
⊢ (∃ a a_1, ∃ (b : a_1 ∈ S), ⟨a_1, b⟩ • x✝ = (IsScalarTower.toAlgHom R A Aₛ).toLinearMap a) ↔
    ∃ a a_1, ∃ (_ : a_1 ∈ Algebra.algebraMapSubmonoid A S), x✝ * (algebraMap A Aₛ) a_1 = (algebraMap A Aₛ) a

Tactic:
Algebra.algebraMapSubmonoid

Goal state after:
case refine_2
R : Type u_1
inst✝⁶ : CommSemiring R
S : Submonoid R
A : Type u_2
Aₛ : Type u_3
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : CommSemiring Aₛ
inst✝² : Algebra A Aₛ
inst✝¹ : Algebra R Aₛ
inst✝ : IsScalarTower R A Aₛ
x✝ : Aₛ
⊢ (∃ a a_1, ∃ (b : a_1 ∈ S), ⟨a_1, b⟩ • x✝ = (IsScalarTower.toAlgHom R A Aₛ).toLinearMap a) ↔
    ∃ a a_1, ∃ (_ : a_1 ∈ Submonoid.map (algebraMap R A) S), x✝ * (algebraMap A Aₛ) a_1 = (algebraMap A Aₛ) a
Module: Mathlib.Algebra.Module.LocalizedModule.IsLocalization

Goal state before:
pp: case refine_3
R : Type u_1
inst✝⁶ : CommSemiring R
S : Submonoid R
A : Type u_2
Aₛ : Type u_3
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : CommSemiring Aₛ
inst✝² : Algebra A Aₛ
inst✝¹ : Algebra R Aₛ
inst✝ : IsScalarTower R A Aₛ
x✝¹ x✝ : A
⊢ ((IsScalarTower.toAlgHom R A Aₛ).toLinearMap x✝¹ = (IsScalarTower.toAlgHom R A Aₛ).toLinearMap x✝ →
      ∃ a, ∃ (b : a ∈ S), ⟨a, b⟩ • x✝¹ = ⟨a, b⟩ • x✝) ↔
    (algebraMap A Aₛ) x✝¹ = (algebraMap A Aₛ) x✝ → ∃ a, ∃ (_ : a ∈ Algebra.algebraMapSubmonoid A S), a * x✝¹ = a * x✝

Tactic:
Algebra.algebraMapSubmonoid

Goal state after:
case refine_3
R : Type u_1
inst✝⁶ : CommSemiring R
S : Submonoid R
A : Type u_2
Aₛ : Type u_3
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : CommSemiring Aₛ
inst✝² : Algebra A Aₛ
inst✝¹ : Algebra R Aₛ
inst✝ : IsScalarTower R A Aₛ
x✝¹ x✝ : A
⊢ ((IsScalarTower.toAlgHom R A Aₛ).toLinearMap x✝¹ = (IsScalarTower.toAlgHom R A Aₛ).toLinearMap x✝ →
      ∃ a, ∃ (b : a ∈ S), ⟨a, b⟩ • x✝¹ = ⟨a, b⟩ • x✝) ↔
    (algebraMap A Aₛ) x✝¹ = (algebraMap A Aₛ) x✝ → ∃ a, ∃ (_ : a ∈ Submonoid.map (algebraMap R A) S), a * x✝¹ = a * x✝
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: case a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : BraidedCategory C
M N : C
inst✝¹ : MonObj M
inst✝ : MonObj N
| (α_ M M M).hom ≫ M ◁ μ ≫ μ ⊗ₘ (α_ N N N).hom ≫ N ◁ μ ≫ μ

pp: case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : BraidedCategory C
M N : C
inst✝¹ : MonObj M
inst✝ : MonObj N
| tensorμ M N M N ▷ (M ⊗ N)

pp: case a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : BraidedCategory C
M N : C
inst✝¹ : MonObj M
inst✝ : MonObj N
| tensorμ (M ⊗ M) (N ⊗ N) M N

Tactic:
← tensorHom_comp_tensorHom,

Goal state after:
case a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : BraidedCategory C
M N : C
inst✝¹ : MonObj M
inst✝ : MonObj N
| ((α_ M M M).hom ⊗ₘ (α_ N N N).hom) ≫ (M ◁ μ ≫ μ ⊗ₘ N ◁ μ ≫ μ)

case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : BraidedCategory C
M N : C
inst✝¹ : MonObj M
inst✝ : MonObj N
| tensorμ M N M N ▷ (M ⊗ N)

case a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : BraidedCategory C
M N : C
inst✝¹ : MonObj M
inst✝ : MonObj N
| tensorμ (M ⊗ M) (N ⊗ N) M N
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
M N O X : C
inst✝² : MonObj M
inst✝¹ : MonObj N
inst✝ : MonObj O
A : Mon C
f : trivial C ⟶ A
⊢ η ≫ f.hom = η

Tactic:
IsMonHom.one_hom

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
M N O X : C
inst✝² : MonObj M
inst✝¹ : MonObj N
inst✝ : MonObj O
A : Mon C
f : trivial C ⟶ A
⊢ η = η
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: case refine_1
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'
⊢ h.cone.fst =
    e₁.hom ≫ PullbackCone.fst ((Cone.postcompose (cospanExt e₂ e₃ e₄ ⋯ ⋯).inv).obj (PullbackCone.mk fst' snd' ⋯))

Tactic:
change fst = e₁.hom ≫ fst' ≫ e₂.inv

Goal state after:
case refine_1
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 = e₁.hom ≫ fst' ≫ e₂.inv