mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse

Goal state before:
pp: n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A B : Matrix n n R
d : n → R
hAB : A * B = diagonal d
s t : ℤˣ
h : s ≠ t
i j k : n
hk : k ∈ univ
σ : Perm n
hσ : σ ∈ ofSign t ∧ σ j = k
τ : Perm n
hτ : τ ∈ ofSign s
⊢ IsAddUnit ((∏ k, A k (τ k)) * (B i k * ∏ k ∈ {j}ᶜ, B k (σ k)))

Tactic:
mem_ofSign

Goal state after:
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A B : Matrix n n R
d : n → R
hAB : A * B = diagonal d
s t : ℤˣ
h : s ≠ t
i j k : n
hk : k ∈ univ
σ : Perm n
hσ : sign σ = t ∧ σ j = k
τ : Perm n
hτ : sign τ = s
⊢ IsAddUnit ((∏ k, A k (τ k)) * (B i k * ∏ k ∈ {j}ᶜ, B k (σ k)))
Module: Mathlib.CategoryTheory.Filtered.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofiltered C
O : Finset C
H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))
S : C
f : ∀ {X : C}, X ∈ O → Nonempty (S ⟶ X)
⊢ ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f_1 : X ⟶ Y},
    ⟨X, ⟨Y, ⟨mX, ⟨mY, f_1⟩⟩⟩⟩ ∈ ∅ → (fun {X} mX ↦ ⋯.some) mX ≫ f_1 = (fun {X} mX ↦ ⋯.some) mY

Tactic:
rintro - - - - - ⟨⟩

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

Goal state before:
pp: case pos
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofiltered C
O : Finset C
H H' : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))
X Y : C
mX : X ∈ O
mY : Y ∈ O
f : X ⟶ Y
nmf : ⟨X, ⟨Y, ⟨mX, ⟨mY, f⟩⟩⟩⟩ ∉ H'
S' : C
T' : {X : C} → X ∈ O → (S' ⟶ X)
w' : ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y}, ⟨X, ⟨Y, ⟨mX, ⟨mY, f⟩⟩⟩⟩ ∈ H' → T' mX ≫ f = T' mY
X' Y' : C
mX' : X' ∈ O
mY' : Y' ∈ O
f' : X' ⟶ Y'
mf' : ⟨X', ⟨Y', ⟨mX', ⟨mY', f'⟩⟩⟩⟩ ∈ insert ⟨X, ⟨Y, ⟨mX, ⟨mY, f⟩⟩⟩⟩ H'
h : X = X' ∧ Y = Y'
⊢ eqHom (T' mX ≫ f) (T' mY) ≫ T' mX' ≫ f' = (fun {X_1} mZ ↦ eqHom (T' mX ≫ f) (T' mY) ≫ T' mZ) mY'

Tactic:
rcases h with ⟨rfl, rfl⟩
      grind [eq_condition]

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

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCat
inst✝ : IsFiltered J
j : J
x : ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).obj j
⊢ MonCat.FilteredColimits.M.mk (F ⋙ forget₂ SemiRingCat MonCat) ⟨j, x * 0⟩ =
    AddMonCat.FilteredColimits.M.mk ((F ⋙ forget₂ SemiRingCat AddCommMonCat) ⋙ forget₂ AddCommMonCat AddMonCat) ⟨j, 0⟩

Tactic:
rw [mul_zero x]

Goal state after:
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCat
inst✝ : IsFiltered J
j : J
x : ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).obj j
⊢ MonCat.FilteredColimits.M.mk (F ⋙ forget₂ SemiRingCat MonCat) ⟨j, 0⟩ =
    AddMonCat.FilteredColimits.M.mk ((F ⋙ forget₂ SemiRingCat AddCommMonCat) ⋙ forget₂ AddCommMonCat AddMonCat) ⟨j, 0⟩
Module: Mathlib.Algebra.Category.MonCat.FilteredColimits

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
x y z : M F
⊢ x * y * z = x * (y * z)

Tactic:
obtain ⟨j₁, x₁, rfl⟩ := x.mk_surjective
      obtain ⟨j₂, y₂, rfl⟩ := y.mk_surjective
      obtain ⟨j₃, z₃, rfl⟩ := z.mk_surjective
      obtain ⟨j, f₁, f₂, f₃, x, y, z, h₁, h₂, h₃⟩ :
          ∃ (j : J) (f₁ : j₁ ⟶ j) (f₂ : j₂ ⟶ j) (f₃ : j₃ ⟶ j) (x y z : F.obj j),
          F.map f₁ x₁ = x ∧ F.map f₂ y₂ = y ∧ F.map f₃ z₃ = z :=
        ⟨IsFiltered.max₃ j₁ j₂ j₃, IsFiltered.firstToMax₃ _ _ _,
          IsFiltered.secondToMax₃ _ _ _, IsFiltered.thirdToMax₃ _ _ _,
          _, _, _, rfl, rfl, rfl⟩
      simp only [← M.map_mk F f₁, ← M.map_mk F f₂, ← M.map_mk F f₃, h₁, h₂, h₃,
        colimit_mul_mk_eq', mul_assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Ulift

Goal state before:
pp: J : Type w
inst✝ : Category.{w', w} J
K : J ⥤ Type u
c : Cone K
hc : IsLimit c
s : (j : J) → (K ⋙ uliftFunctor.{v, u}).obj j
hs : s ∈ (K ⋙ uliftFunctor.{v, u}).sections
⊢ ∃! x, ∀ (j : J), (ConcreteCategory.hom ((uliftFunctor.{v, u}.mapCone c).π.app j)) x = s j

Tactic:
obtain ⟨x, hx₁, hx₂⟩ := (Types.isLimit_iff c).mp ⟨hc⟩ _ ((sectionsEquiv K).symm ⟨s, hs⟩).2

Goal state after:
J : Type w
inst✝ : Category.{w', w} J
K : J ⥤ Type u
c : Cone K
hc : IsLimit c
s : (j : J) → (K ⋙ uliftFunctor.{v, u}).obj j
hs : s ∈ (K ⋙ uliftFunctor.{v, u}).sections
x : c.pt
hx₁ : ∀ (j : J), (ConcreteCategory.hom (c.π.app j)) x = ↑((sectionsEquiv K).symm ⟨s, ⋯⟩) j
hx₂ :
  ∀ (y : c.pt), (fun x ↦ ∀ (j : J), (ConcreteCategory.hom (c.π.app j)) x = ↑((sectionsEquiv K).symm ⟨s, ⋯⟩) j) y → y = x
⊢ ∃! x, ∀ (j : J), (ConcreteCategory.hom ((uliftFunctor.{v, u}.mapCone c).π.app j)) x = s j
Module: Mathlib.Algebra.Category.ModuleCat.Limits

Goal state before:
pp: R : Type u
inst✝⁶ : Ring R
J : Type v
inst✝⁵ : Category.{t, v} J
F : J ⥤ ModuleCat R
ι : Type v
inst✝⁴ : DecidableEq ι
inst✝³ : Preorder ι
G : ι → Type v
inst✝² : (i : ι) → AddCommGroup (G i)
inst✝¹ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝ : DirectedSystem G fun i j h ↦ ⇑(f i j h)
i : ι
⊢ ↟(f i i ⋯) = 𝟙 (of R (G i))

Tactic:
by
    ext
    apply Module.DirectedSystem.map_self

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

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ GrpCat
e : forget₂ GrpCat MonCat ⋙ forget MonCat ≅ forget GrpCat := Iso.refl (forget₂ GrpCat MonCat ⋙ forget MonCat)
⊢ CreatesLimit F (forget GrpCat)

Tactic:
exact createsLimitOfNatIso e

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

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ CommGrpCat
e : forget₂ CommGrpCat GrpCat ⋙ forget GrpCat ≅ forget CommGrpCat :=
  Iso.refl (forget₂ CommGrpCat GrpCat ⋙ forget GrpCat)
⊢ CreatesLimit F (forget CommGrpCat)

Tactic:
exact createsLimitOfNatIso e

Goal state after:
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.IsEquivalence
⊢ IsIso h.counit

Tactic:
by
  have := h.isEquivalence_left_of_isEquivalence_right
  infer_instance

Goal state after:
Module: Mathlib.Algebra.Module.LinearMap.Rat

Goal state before:
pp: M : Type u_1
M₂ : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module ℚ M
inst✝¹ : AddCommGroup M₂
inst✝ : Module ℚ M₂
⊢ Injective toRatLinearMap

Tactic:
intro f g h

Goal state after:
M : Type u_1
M₂ : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module ℚ M
inst✝¹ : AddCommGroup M₂
inst✝ : Module ℚ M₂
f g : M →+ M₂
h : f.toRatLinearMap = g.toRatLinearMap
⊢ f = g
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 Z : C
f : J → C
g h : X ⟶ Y ⊗ Z ⊗ ⨁ f
w : ∀ (j : J), g ≫ Y ◁ Z ◁ biproduct.π f j = h ≫ Y ◁ Z ◁ biproduct.π f j
⊢ g = h

Tactic:
by
  apply (cancel_mono (α_ _ _ _).inv).mp
  ext
  simp [w]

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic

Goal state before:
pp: case refine_1
R : Type u
inst✝ : CommRing R
X✝ Y✝ Z✝ : ModuleCat R
x : ↑X✝
y : ↑Y✝
⊢ (((TensorProduct.mk R ↑X✝ ↑Y✝).compr₂ₛₗ (Hom.hom (X✝ ◁ 0))) x) y =
    (((TensorProduct.mk R ↑X✝ ↑Y✝).compr₂ₛₗ (Hom.hom 0)) x) y

Tactic:
simp [ModuleCat.hom_whiskerLeft]

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic

Goal state before:
pp: case refine_3
R : Type u
inst✝ : CommRing R
X✝ Y✝ Z✝ : ModuleCat R
f✝ g✝ : Y✝ ⟶ Z✝
x : ↑X✝
y : ↑Y✝
⊢ (((TensorProduct.mk R ↑X✝ ↑Y✝).compr₂ₛₗ (Hom.hom (X✝ ◁ (f✝ + g✝)))) x) y =
    (((TensorProduct.mk R ↑X✝ ↑Y✝).compr₂ₛₗ (Hom.hom (X✝ ◁ f✝ + X✝ ◁ g✝))) x) y

Tactic:
simp [ModuleCat.hom_whiskerLeft]

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic

Goal state before:
pp: case refine_1
R : Type u
inst✝ : CommRing R
X✝ Y✝ Z✝ : ModuleCat R
r✝ : R
f✝ : Y✝ ⟶ Z✝
x : ↑X✝
y : ↑Y✝
⊢ (((TensorProduct.mk R ↑X✝ ↑Y✝).compr₂ₛₗ (Hom.hom (X✝ ◁ (r✝ • f✝)))) x) y =
    (((TensorProduct.mk R ↑X✝ ↑Y✝).compr₂ₛₗ (Hom.hom (r✝ • X✝ ◁ f✝))) x) y

Tactic:
simp [ModuleCat.hom_whiskerLeft]

Goal state after:
Module: Mathlib.Tactic.CategoryTheory.Coherence.Basic

Goal state before:
pp: α : Type u_1
a b a' b' : α
ha : a = a'
hb : b = b'
h : a' = b'
⊢ a = b

Tactic:
by
  simp [h, ha, hb]

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 : D
⊢ (adj.homEquiv (G.obj X ⊗ 𝟙_ C) X).symm (ρ_ (G.obj X)).hom =
    (adj.homEquiv (G.obj X ⊗ 𝟙_ C) X).symm
      (G.obj X ◁ (adj.homEquiv (𝟙_ C) (𝟙_ D)) (η F) ≫
        (adj.homEquiv (G.obj X ⊗ G.obj (𝟙_ D)) (X ⊗ 𝟙_ D))
            (δ F (G.obj X) (G.obj (𝟙_ D)) ≫ (adj.counit.app X ⊗ₘ adj.counit.app (𝟙_ D))) ≫
          G.map (ρ_ X).hom)

Tactic:
rw [homEquiv_counit, homEquiv_unit, MonoidalCategory.whiskerLeft_comp, homEquiv_unit,
      homEquiv_counit, map_comp, map_comp, map_comp, map_comp, map_comp, map_comp,
      assoc, assoc, assoc, assoc, assoc, counit_naturality, counit_naturality_assoc,
      counit_naturality_assoc, left_triangle_components_assoc, ← δ_natural_right_assoc,
      ← δ_natural_right_assoc, tensorHom_def, assoc, ← whisker_exchange_assoc,
      ← MonoidalCategory.whiskerLeft_comp_assoc, ← MonoidalCategory.whiskerLeft_comp_assoc,
      assoc, counit_naturality, left_triangle_components_assoc, MonoidalCategory.whiskerRight_id,
      assoc, assoc, Iso.inv_hom_id, comp_id, right_unitality_hom_assoc]

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₂ Y₁ Y₂ U₁ U₂ V₁ V₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : U₁ ⟶ V₁
g₂ : U₂ ⟶ V₂
| (f₁ ⊗ₘ f₂ ⊗ₘ g₁ ⊗ₘ g₂) ≫ (𝟙 Y₁ ⊗ₘ (α_ Y₂ V₁ V₂).inv)

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₁ ⊗ₘ (β_ Y₂ V₁).hom ⊗ₘ 𝟙 V₂

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₂).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₂
| (α_ 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

Tactic:
rw [tensorHom_comp_tensorHom, comp_id f₁, ← id_comp f₁, associator_inv_naturality,
      ← 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₁ ⊗ₘ (α_ X₂ U₁ U₂).inv) ≫ (f₁ ⊗ₘ (f₂ ⊗ₘ g₁) ⊗ₘ 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₁ ⊗ₘ (β_ Y₂ V₁).hom ⊗ₘ 𝟙 V₂

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₂).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₂
| (α_ 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
Module: Mathlib.CategoryTheory.Adjunction.Mates

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

Tactic:
by
  unfold hComp vComp mateEquiv
  ext b
  simp only [comp_obj, Equiv.coe_fn_mk, whiskerRight_comp, whiskerRight_twice, assoc,
    whiskerLeft_comp, comp_app, id_obj, rightUnitor_inv_app, Functor.whiskerLeft_app,
    associator_hom_app, associator_inv_app, Functor.whiskerRight_app, map_id, Functor.comp_map,
    leftUnitor_hom_app, comp_id, id_comp, whiskerLeft_twice, Iso.hom_inv_id_assoc]
  slice_rhs 1 4 => rw [← assoc, ← assoc, ← unit_naturality (adj₃)]
  rw [L₃.map_comp, R₃.map_comp]
  slice_rhs 2 4 =>
    rw [← R₃.map_comp, ← R₃.map_comp, ← assoc, ← L₃.map_comp, ← G₂.map_comp, ← G₂.map_comp]
    rw [← Functor.comp_map G₂ L₃, β.naturality]
  rw [(L₂ ⋙ H₂).map_comp, R₃.map_comp, R₃.map_comp]
  slice_rhs 4 5 =>
    rw [← R₃.map_comp, Functor.comp_map L₂ _, ← Functor.comp_map _ L₂, ← H₂.map_comp]
    rw [adj₂.counit.naturality]
  simp only [comp_obj, Functor.comp_map, map_comp, id_obj, Functor.id_map, assoc]
  slice_rhs 4 5 =>
    rw [← R₃.map_comp, ← H₂.map_comp, ← Functor.comp_map _ L₂, adj₂.counit.naturality]
  simp only [comp_obj, id_obj, Functor.id_map, map_comp, assoc]
  slice_rhs 3 4 =>
    rw [← R₃.map_comp, ← H₂.map_comp, left_triangle_components]
  simp only [map_id, id_comp]

Goal state after:
Module: Mathlib.RingTheory.Congruence.Hom

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : NonAssocSemiring M
inst✝ : NonAssocSemiring N
c : RingCon M
g : N →+* M
⊢ c.comap g = ker (c.mk'.comp g)

Tactic:
by
  rw [ker_comp, ker_mk'_eq]

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
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ x.1 •> 0 + x.2 <• 1 = x.2

Tactic:
rw [smul_zero, zero_add, op_one, one_smul]

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
⊢ (x ^ n).snd = n •> x.fst ^ n.pred •> x.snd

Tactic:
by
  simp_rw [snd_pow_eq_sum, ← smul_comm (_ : R) (_ : Rᵐᵒᵖ), aux, smul_smul, ← pow_add]
  match n with
  | 0 => rw [Nat.pred_zero, pow_zero, List.range_zero, zero_smul, List.map_nil, List.sum_nil]
  | (Nat.succ n) =>
    simp_rw [Nat.pred_succ]
    exact (List.sum_eq_card_nsmul _ (x.fst ^ n • x.snd) (by grind)).trans
      (by rw [List.length_map, List.length_range])

Goal state after:
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
this :
  TensorProduct.lift (LinearMap.lsmul R A) ∘ₗ TensorProduct.map counit LinearMap.id ∘ₗ comul =
    TensorProduct.lift (LinearMap.lsmul R A) ∘ₗ (TensorProduct.mk R R A) 1
⊢ TensorProduct.lift (LinearMap.lsmul R A ∘ₗ counit) ∘ₗ comul = LinearMap.id

Tactic:
← LinearMap.comp_assoc,

Goal state after:
R : Type u
A : Type v
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Coalgebra R A
this :
  (TensorProduct.lift (LinearMap.lsmul R A) ∘ₗ TensorProduct.map counit LinearMap.id) ∘ₗ comul =
    TensorProduct.lift (LinearMap.lsmul R A) ∘ₗ (TensorProduct.mk R R A) 1
⊢ TensorProduct.lift (LinearMap.lsmul R A ∘ₗ counit) ∘ₗ comul = LinearMap.id
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: S : Type u_1
R R' : Type u
M : Type v
inst✝¹⁶ : CommSemiring S
inst✝¹⁵ : Semiring R
inst✝¹⁴ : CommSemiring R'
inst✝¹³ : AddCommMonoid M
inst✝¹² : Algebra S R
inst✝¹¹ : Module S M
inst✝¹⁰ : Module R M
inst✝⁹ : Module Rᵐᵒᵖ M
inst✝⁸ : SMulCommClass R Rᵐᵒᵖ M
inst✝⁷ : IsScalarTower S R M
inst✝⁶ : IsScalarTower S Rᵐᵒᵖ M
inst✝⁵ : Module R' M
inst✝⁴ : Module R'ᵐᵒᵖ M
inst✝³ : IsCentralScalar R' M
A : Type u_2
inst✝² : Semiring A
inst✝¹ : Algebra S A
inst✝ : Algebra R' A
f : R →ₐ[S] A
g : M →ₗ[S] A
hg : ∀ (x y : M), g x * g y = 0
hfg : ∀ (r : R) (x : M), g (r •> x) = f r * g x
hgf : ∀ (r : R) (x : M), g (x <• r) = g x * f r
r₁ : R
m₁ : M
r₂ : R
m₂ : M
⊢ f ((r₁ + 0) * (r₂ + 0)) + g ((r₁ + 0) •> (0 + m₂) + (op r₂ + 0) •> (0 + m₁)) =
    (f (r₁ + 0) + g (0 + m₁)) * (f (r₂ + 0) + g (0 + m₂))

Tactic:
simp only [add_zero, zero_add, add_mul, mul_add, hg]

Goal state after:
S : Type u_1
R R' : Type u
M : Type v
inst✝¹⁶ : CommSemiring S
inst✝¹⁵ : Semiring R
inst✝¹⁴ : CommSemiring R'
inst✝¹³ : AddCommMonoid M
inst✝¹² : Algebra S R
inst✝¹¹ : Module S M
inst✝¹⁰ : Module R M
inst✝⁹ : Module Rᵐᵒᵖ M
inst✝⁸ : SMulCommClass R Rᵐᵒᵖ M
inst✝⁷ : IsScalarTower S R M
inst✝⁶ : IsScalarTower S Rᵐᵒᵖ M
inst✝⁵ : Module R' M
inst✝⁴ : Module R'ᵐᵒᵖ M
inst✝³ : IsCentralScalar R' M
A : Type u_2
inst✝² : Semiring A
inst✝¹ : Algebra S A
inst✝ : Algebra R' A
f : R →ₐ[S] A
g : M →ₗ[S] A
hg : ∀ (x y : M), g x * g y = 0
hfg : ∀ (r : R) (x : M), g (r •> x) = f r * g x
hgf : ∀ (r : R) (x : M), g (x <• r) = g x * f r
r₁ : R
m₁ : M
r₂ : R
m₂ : M
⊢ f (r₁ * r₂) + g (r₁ •> m₂ + m₁ <• r₂) = f r₁ * f r₂ + g m₁ * f r₂ + f r₁ * g m₂
Module: Mathlib.RingTheory.Coalgebra.Equiv

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : Module R A
inst✝³ : Coalgebra R A
inst✝² : AddCommMonoid B
inst✝¹ : Module R B
inst✝ : CoalgebraStruct R B
f : A ≃ₗc[R] B
⊢ LinearMap.rTensor B (counit ∘ₗ ↑f.toLinearEquiv.symm) ∘ₗ
      (TensorProduct.map f.toLinearMap f.toLinearMap ∘ₗ comul) ∘ₗ ↑f.toLinearEquiv.symm =
    (TensorProduct.mk R R B) 1

Tactic:
← LinearMap.comp_assoc,

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : Module R A
inst✝³ : Coalgebra R A
inst✝² : AddCommMonoid B
inst✝¹ : Module R B
inst✝ : CoalgebraStruct R B
f : A ≃ₗc[R] B
⊢ ((LinearMap.rTensor B (counit ∘ₗ ↑f.toLinearEquiv.symm) ∘ₗ TensorProduct.map f.toLinearMap f.toLinearMap) ∘ₗ comul) ∘ₗ
      ↑f.toLinearEquiv.symm =
    (TensorProduct.mk R R B) 1
Module: Mathlib.RingTheory.Coalgebra.Equiv

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : Module R A
inst✝³ : Coalgebra R A
inst✝² : AddCommMonoid B
inst✝¹ : Module R B
inst✝ : CoalgebraStruct R B
f : A ≃ₗc[R] B
⊢ LinearMap.lTensor B (counit ∘ₗ ↑f.toLinearEquiv.symm) ∘ₗ
      (TensorProduct.map f.toLinearMap f.toLinearMap ∘ₗ comul) ∘ₗ ↑f.toLinearEquiv.symm =
    (TensorProduct.mk R B R).flip 1

Tactic:
← LinearMap.comp_assoc,

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : Module R A
inst✝³ : Coalgebra R A
inst✝² : AddCommMonoid B
inst✝¹ : Module R B
inst✝ : CoalgebraStruct R B
f : A ≃ₗc[R] B
⊢ ((LinearMap.lTensor B (counit ∘ₗ ↑f.toLinearEquiv.symm) ∘ₗ TensorProduct.map f.toLinearMap f.toLinearMap) ∘ₗ comul) ∘ₗ
      ↑f.toLinearEquiv.symm =
    (TensorProduct.mk R B R).flip 1
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: R : Type u
ι : Type v
A : ι → Type w
inst✝⁴ : DecidableEq ι
inst✝³ : CommSemiring R
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : (i : ι) → Module R (A i)
inst✝ : (i : ι) → CoalgebraStruct R (A i)
i j : ι
x✝ : A j
⊢ ((comul ∘ₗ lapply i) ∘ₗ lsingle j) x✝ = ((TensorProduct.map (lapply i) (lapply i) ∘ₗ comul) ∘ₗ lsingle j) x✝

Tactic:
have := eq_or_ne i j

Goal state after:
R : Type u
ι : Type v
A : ι → Type w
inst✝⁴ : DecidableEq ι
inst✝³ : CommSemiring R
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : (i : ι) → Module R (A i)
inst✝ : (i : ι) → CoalgebraStruct R (A i)
i j : ι
x✝ : A j
this : i = j ∨ i ≠ j
⊢ ((comul ∘ₗ lapply i) ∘ₗ lsingle j) x✝ = ((TensorProduct.map (lapply i) (lapply i) ∘ₗ comul) ∘ₗ lsingle j) x✝
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: R : Type u
ι : Type v
A : Type w
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : CoalgebraStruct R A
i j : ι
x✝ : A
⊢ ((comul ∘ₗ lapply i) ∘ₗ lsingle j) x✝ = ((TensorProduct.map (lapply i) (lapply i) ∘ₗ comul) ∘ₗ lsingle j) x✝

Tactic:
have := eq_or_ne i j

Goal state after:
R : Type u
ι : Type v
A : Type w
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : CoalgebraStruct R A
i j : ι
x✝ : A
this : i = j ∨ i ≠ j
⊢ ((comul ∘ₗ lapply i) ∘ₗ lsingle j) x✝ = ((TensorProduct.map (lapply i) (lapply i) ∘ₗ comul) ∘ₗ lsingle j) x✝
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
A : n → Type u_3
inst✝² : (i : n) → AddCommMonoid (A i)
inst✝¹ : (i : n) → Module R (A i)
inst✝ : (i : n) → CoalgebraStruct R (A i)
i j : n
x✝ : A j
⊢ ((comul ∘ₗ proj i) ∘ₗ LinearMap.single R A j) x✝ = ((map (proj i) (proj i) ∘ₗ comul) ∘ₗ LinearMap.single R A j) x✝

Tactic:
have := eq_or_ne i j

Goal state after:
R : Type u_1
n : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
A : n → Type u_3
inst✝² : (i : n) → AddCommMonoid (A i)
inst✝¹ : (i : n) → Module R (A i)
inst✝ : (i : n) → CoalgebraStruct R (A i)
i j : n
x✝ : A j
this : i = j ∨ i ≠ j
⊢ ((comul ∘ₗ proj i) ∘ₗ LinearMap.single R A j) x✝ = ((map (proj i) (proj i) ∘ₗ comul) ∘ₗ LinearMap.single R A j) x✝
Module: Mathlib.RingTheory.Coalgebra.CoassocSimps

Goal state before:
pp: R : Type u_1
M : Type u_3
N : Type u_4
P : Type u_5
M' : Type u_6
N' : Type u_7
P' : Type u_8
M₁ : Type u_11
inst✝¹⁴ : CommSemiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : Module R M
inst✝¹¹ : AddCommMonoid N
inst✝¹⁰ : Module R N
inst✝⁹ : AddCommMonoid P
inst✝⁸ : Module R P
inst✝⁷ : AddCommMonoid M'
inst✝⁶ : Module R M'
inst✝⁵ : AddCommMonoid N'
inst✝⁴ : Module R N'
inst✝³ : AddCommMonoid P'
inst✝² : Module R P'
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
f : M →ₗ[R] N
g : N →ₗ[R] P
f' : M' →ₗ[R] N'
g' : N' →ₗ[R] P'
φ : M₁ →ₗ[R] M ⊗[R] M'
⊢ g ⊗ₘ g' ∘ₗ f ⊗ₘ f' ∘ₗ φ = (g ∘ₗ f) ⊗ₘ (g' ∘ₗ f') ∘ₗ φ

Tactic:
← LinearMap.comp_assoc,

Goal state after:
R : Type u_1
M : Type u_3
N : Type u_4
P : Type u_5
M' : Type u_6
N' : Type u_7
P' : Type u_8
M₁ : Type u_11
inst✝¹⁴ : CommSemiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : Module R M
inst✝¹¹ : AddCommMonoid N
inst✝¹⁰ : Module R N
inst✝⁹ : AddCommMonoid P
inst✝⁸ : Module R P
inst✝⁷ : AddCommMonoid M'
inst✝⁶ : Module R M'
inst✝⁵ : AddCommMonoid N'
inst✝⁴ : Module R N'
inst✝³ : AddCommMonoid P'
inst✝² : Module R P'
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
f : M →ₗ[R] N
g : N →ₗ[R] P
f' : M' →ₗ[R] N'
g' : N' →ₗ[R] P'
φ : M₁ →ₗ[R] M ⊗[R] M'
⊢ (g ⊗ₘ g' ∘ₗ f ⊗ₘ f') ∘ₗ φ = (g ∘ₗ f) ⊗ₘ (g' ∘ₗ f') ∘ₗ φ