mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Multilinear.Basic

Goal state before:
pp: case neg
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁶ : Semiring R
inst✝⁵ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁴ : AddCommMonoid M₂
inst✝³ : (i : ι) → Module R (M₁ i)
inst✝² : Module R M₂
f : MultilinearMap R M₁ M₂
α : ι → Type u_1
g : (i : ι) → α i → M₁ i
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
this : (i : ι) → DecidableEq (α i) := fun i ↦ Classical.decEq (α i)
n : ℕ
IH :
  ∀ m < n,
    ∀ (A : (i : ι) → Finset (α i)),
      ∑ i, #(A i) = m → (f fun i ↦ ∑ j ∈ A i, g i j) = ∑ r ∈ piFinset A, f fun i ↦ g i (r i)
A : (i : ι) → Finset (α i)
h : ∑ i, #(A i) = n
Ai_empty : ∀ (i : ι), (A i).Nonempty
i₀ : ι
hi₀ : 1 < #(A i₀)
j₁ j₂ : α i₀
left✝ : j₁ ∈ A i₀
hj₂ : j₂ ∈ A i₀
right✝ : j₁ ≠ j₂
B : (a : ι) → Finset (α a) := update A i₀ (A i₀ \ {j₂})
C : (a : ι) → Finset (α a) := update A i₀ {j₂}
B_subset_A : ∀ (i : ι), B i ⊆ A i
C_subset_A : ∀ (i : ι), C i ⊆ A i
A_eq_BC : (fun i ↦ ∑ j ∈ A i, g i j) = update (fun i ↦ ∑ j ∈ A i, g i j) i₀ (∑ j ∈ B i₀, g i₀ j + ∑ j ∈ C i₀, g i₀ j)
Beq : update (fun i ↦ ∑ j ∈ A i, g i j) i₀ (∑ j ∈ B i₀, g i₀ j) = fun i ↦ ∑ j ∈ B i, g i j
Ceq : update (fun i ↦ ∑ j ∈ A i, g i j) i₀ (∑ j ∈ C i₀, g i₀ j) = fun i ↦ ∑ j ∈ C i, g i j
Brec : (f fun i ↦ ∑ j ∈ B i, g i j) = ∑ r ∈ piFinset B, f fun i ↦ g i (r i)
Crec : (f fun i ↦ ∑ j ∈ C i, g i j) = ∑ r ∈ piFinset C, f fun i ↦ g i (r i)
D : Disjoint (piFinset B) (piFinset C)
pi_BC : piFinset A = piFinset B ∪ piFinset C
⊢ ((∑ r ∈ piFinset B, f fun i ↦ g i (r i)) + ∑ r ∈ piFinset C, f fun i ↦ g i (r i)) =
    ∑ r ∈ piFinset B ∪ piFinset C, f fun i ↦ g i (r i)

Tactic:
← Finset.sum_union D

Goal state after:
case neg
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁶ : Semiring R
inst✝⁵ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁴ : AddCommMonoid M₂
inst✝³ : (i : ι) → Module R (M₁ i)
inst✝² : Module R M₂
f : MultilinearMap R M₁ M₂
α : ι → Type u_1
g : (i : ι) → α i → M₁ i
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
this : (i : ι) → DecidableEq (α i) := fun i ↦ Classical.decEq (α i)
n : ℕ
IH :
  ∀ m < n,
    ∀ (A : (i : ι) → Finset (α i)),
      ∑ i, #(A i) = m → (f fun i ↦ ∑ j ∈ A i, g i j) = ∑ r ∈ piFinset A, f fun i ↦ g i (r i)
A : (i : ι) → Finset (α i)
h : ∑ i, #(A i) = n
Ai_empty : ∀ (i : ι), (A i).Nonempty
i₀ : ι
hi₀ : 1 < #(A i₀)
j₁ j₂ : α i₀
left✝ : j₁ ∈ A i₀
hj₂ : j₂ ∈ A i₀
right✝ : j₁ ≠ j₂
B : (a : ι) → Finset (α a) := update A i₀ (A i₀ \ {j₂})
C : (a : ι) → Finset (α a) := update A i₀ {j₂}
B_subset_A : ∀ (i : ι), B i ⊆ A i
C_subset_A : ∀ (i : ι), C i ⊆ A i
A_eq_BC : (fun i ↦ ∑ j ∈ A i, g i j) = update (fun i ↦ ∑ j ∈ A i, g i j) i₀ (∑ j ∈ B i₀, g i₀ j + ∑ j ∈ C i₀, g i₀ j)
Beq : update (fun i ↦ ∑ j ∈ A i, g i j) i₀ (∑ j ∈ B i₀, g i₀ j) = fun i ↦ ∑ j ∈ B i, g i j
Ceq : update (fun i ↦ ∑ j ∈ A i, g i j) i₀ (∑ j ∈ C i₀, g i₀ j) = fun i ↦ ∑ j ∈ C i, g i j
Brec : (f fun i ↦ ∑ j ∈ B i, g i j) = ∑ r ∈ piFinset B, f fun i ↦ g i (r i)
Crec : (f fun i ↦ ∑ j ∈ C i, g i j) = ∑ r ∈ piFinset C, f fun i ↦ g i (r i)
D : Disjoint (piFinset B) (piFinset C)
pi_BC : piFinset A = piFinset B ∪ piFinset C
⊢ (∑ x ∈ piFinset B ∪ piFinset C, f fun i ↦ g i (x i)) = ∑ r ∈ piFinset B ∪ piFinset C, f fun i ↦ g i (r i)
Module: Mathlib.LinearAlgebra.Multilinear.Basic

Goal state before:
pp: case inr
ι : Type u_3
M₁ : ι → Type u_1
α : Type u_2
inst✝¹ : DecidableEq α
s : Set ι
inst✝ : DecidableEq { x // x ∈ s }
e : α ≃ ↑s
m : α → (i : ι) → M₁ i
a : α
z : (i : ι) → M₁ i
i : ↑s
hne : a ≠ e.symm i
⊢ update m a z (e.symm i) ↑i = update (fun j ↦ m (e.symm j) ↑j) (e a) (z ↑(e a)) i

Tactic:
rw [update_of_ne hne.symm, update_of_ne fun h ↦ (Equiv.symm_apply_apply .. ▸ h ▸ hne) rfl]

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

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
y' : (j : J) × ↑(F.obj j)
j₁ : J
y : ↑(F.obj j₁)
hyy' : Types.FilteredColimit.Rel (F ⋙ forget MonCat) ⟨j₁, y⟩ y'
j₂ : J
x : ↑(F.obj j₂)
⊢ colimitMulAux F ⟨j₂, x⟩ ⟨j₁, y⟩ = colimitMulAux F ⟨j₂, x⟩ y'

Tactic:
obtain ⟨j₃, y'⟩ := y'

Goal state after:
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
j₁ : J
y : ↑(F.obj j₁)
j₂ : J
x : ↑(F.obj j₂)
j₃ : J
y' : ↑(F.obj j₃)
hyy' : Types.FilteredColimit.Rel (F ⋙ forget MonCat) ⟨j₁, y⟩ ⟨j₃, y'⟩
⊢ colimitMulAux F ⟨j₂, x⟩ ⟨j₁, y⟩ = colimitMulAux F ⟨j₂, x⟩ ⟨j₃, y'⟩
Module: Mathlib.CategoryTheory.Limits.Types.Images

Goal state before:
pp: case step
F : ℕᵒᵖ ⥤ Type u
hF : ∀ (n : ℕ), Function.Surjective ⇑(ConcreteCategory.hom (F.map (homOfLE ⋯).op))
a : F.obj (Opposite.op 0)
n m p : ℕ
h : m.le p
ih :
  (ConcreteCategory.hom (F.map (Opposite.op { down := { down := h } })))
      ((fun x ↦
          match x with
          | Opposite.op n => preimage hF a n)
        (Opposite.op p)) =
    (fun x ↦
        match x with
        | Opposite.op n => preimage hF a n)
      (Opposite.op m)
⊢ (ConcreteCategory.hom (F.map (Opposite.op { down := { down := ⋯ } })))
      ((fun x ↦
          match x with
          | Opposite.op n => preimage hF a n)
        (Opposite.op p.succ)) =
    (fun x ↦
        match x with
        | Opposite.op n => preimage hF a n)
      (Opposite.op m)

Tactic:
rw [← ih]
    have h' : m ≤ p := h
    erw [CategoryTheory.Functor.map_comp (f := (homOfLE (Nat.le_succ p)).op) (g := (homOfLE h').op),
      comp_apply, (hF p _).choose_spec]
    rfl

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
inst✝² : Category.{w', w} J
F : J ⥤ C
inst✝¹ : PreservesLimit F G
inst✝ : HasLimit F
t : Cone F
⊢ G.map (limit.lift F t) ≫ (preservesLimitIso G F).hom = limit.lift (F ⋙ G) (G.mapCone t)

Tactic:
by
  ext
  simp [← G.map_comp]

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
inst✝² : Category.{w', w} J
F : J ⥤ C
inst✝¹ : PreservesColimit F G
inst✝ : HasColimit F
t : Cocone F
⊢ (preservesColimitIso G F).inv ≫ G.map (colimit.desc F t) = colimit.desc (F ⋙ G) (G.mapCocone t)

Tactic:
by
  ext
  simp [← G.map_comp]

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
t : Cocone F
x y : ↑(R F)
⊢ (↑(descAddMonoidHom t)).toFun (x * y) = (↑(descAddMonoidHom t)).toFun x * (↑(descAddMonoidHom t)).toFun y

Tactic:
change descAddMonoidHom t (x * y) =
          descAddMonoidHom t x * descAddMonoidHom t y
        simp [← descMonoidHom_apply_eq]

Goal state after:
Module: Mathlib.CategoryTheory.ShrinkYoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
X Y : C
f : X ⟶ Y
P : C ⥤ Type w
t : P.obj X
⊢ shrinkCoyonedaEquiv (shrinkCoyonedaEquiv.symm ((ConcreteCategory.hom (P.map f)) t)) =
    shrinkCoyonedaEquiv (shrinkCoyoneda.{w, v, u}.map f.op ≫ shrinkCoyonedaEquiv.symm t)

Tactic:
obtain ⟨t, rfl⟩ := shrinkCoyonedaEquiv.surjective t
    rw [← shrinkCoyonedaEquiv_naturality]
    simp

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

Goal state before:
pp: J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ GrpCat
inst✝ : Small.{u, max u v} ↑(F ⋙ forget GrpCat).sections
this : (forget₂ GrpCat MonCat).ReflectsIsomorphisms := reflectsIsomorphisms_forget₂ GrpCat MonCat
c' : Cone (F ⋙ forget₂ GrpCat MonCat)
t : IsLimit c'
⊢ Small.{u, max u v} ↑((F ⋙ forget₂ GrpCat MonCat) ⋙ forget MonCat).sections

Tactic:
have : HasLimit (F ⋙ forget₂ GrpCat MonCat) := ⟨_, t⟩
        apply Concrete.small_sections_of_hasLimit (F ⋙ forget₂ GrpCat MonCat)

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:
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.Limits.Preserves.Shapes.Pullbacks

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y : C
f : W ⟶ X
g : W ⟶ Y
inst✝ : PreservesColimit (span f g) G
c : Cocone (span g f)
hc : IsColimit c
⊢ IsColimit (PushoutCocone.mk ((G.mapCocone c).ι.app WalkingSpan.left) ((G.mapCocone c).ι.app WalkingSpan.right) ⋯)

Tactic:
apply PushoutCocone.isColimitOfFlip

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y : C
f : W ⟶ X
g : W ⟶ Y
inst✝ : PreservesColimit (span f g) G
c : Cocone (span g f)
hc : IsColimit c
⊢ IsColimit (PushoutCocone.mk ((G.mapCocone c).ι.app WalkingSpan.left) ((G.mapCocone c).ι.app WalkingSpan.right) ⋯).flip
Module: Mathlib.CategoryTheory.MorphismProperty.Composition

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
inst✝ : W.IsMultiplicative
⊢ W.multiplicativeClosure = W

Tactic:
apply le_antisymm _ <| le_multiplicativeClosure W

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
inst✝ : W.IsMultiplicative
⊢ W.multiplicativeClosure ≤ W
Module: Mathlib.Algebra.Category.ModuleCat.EpiMono

Goal state before:
pp: R : Type u
inst✝ : Ring R
X Y : ModuleCat R
f : X ⟶ Y
⊢ Mono f ↔ Function.Injective ⇑(ConcreteCategory.hom f)

Tactic:
by
  rw [mono_iff_ker_eq_bot, LinearMap.ker_eq_bot]

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✝ : G.LaxMonoidal
X Y Z : C
| (adj.unit.app X ▷ Y ≫ G.obj (F.obj X) ◁ adj.unit.app Y) ▷ Z ≫
    (G.obj (F.obj X) ⊗ G.obj (F.obj Y)) ◁ adj.unit.app Z ≫
      μ G (F.obj X) (F.obj Y) ▷ G.obj (F.obj Z) ≫
        μ G (F.obj X ⊗ F.obj Y) (F.obj Z) ≫ G.map (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom

Tactic:
← tensorHom_def,

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 ⥤ C
adj : F ⊣ G
inst✝ : G.LaxMonoidal
X Y Z : C
| (adj.unit.app X ⊗ₘ adj.unit.app Y) ▷ Z ≫
    (G.obj (F.obj X) ⊗ G.obj (F.obj Y)) ◁ adj.unit.app Z ≫
      μ G (F.obj X) (F.obj Y) ▷ G.obj (F.obj Z) ≫
        μ G (F.obj X ⊗ F.obj Y) (F.obj Z) ≫ G.map (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom
Module: Mathlib.Algebra.Category.ModuleCat.Colimits

Goal state before:
pp: R : Type w
inst✝² : Ring R
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ ModuleCat R
inst✝ : HasColimit (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat)
r s : R
j : J
⊢ colimit.ι (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) j ≫
      colimMap { app := fun j ↦ (F.obj j).smul (r + s), naturality := ⋯ } =
    colimit.ι (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) j ≫
      (colimMap { app := fun j ↦ (F.obj j).smul r, naturality := ⋯ } +
        colimMap { app := fun j ↦ (F.obj j).smul s, naturality := ⋯ })

Tactic:
by
    simp +instances only [Functor.comp_obj, forget₂_obj, map_add, ι_colimMap]
    rw [Preadditive.add_comp, Preadditive.comp_add]
    simp only [ι_colimMap, Functor.comp_obj, forget₂_obj]

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

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
a✝ : Π₀ (j : J), ↑(F.obj j)
⊢ a✝ ∈ {x | ∃ j j' u a, x = DFinsupp.single j' ((ConcreteCategory.hom (F.map u)) a) - DFinsupp.single j a} →
    a✝ ∈ ↑(DFinsupp.sumAddHom fun j ↦ (Quot.ι (F ⋙ uliftFunctor) j).comp AddEquiv.ulift.symm.toAddMonoidHom).ker

Tactic:
hx

Goal state after:
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
a✝ : Π₀ (j : J), ↑(F.obj j)
hx : a✝ ∈ {x | ∃ j j' u a, x = DFinsupp.single j' ((ConcreteCategory.hom (F.map u)) a) - DFinsupp.single j a}
⊢ a✝ ∈ ↑(DFinsupp.sumAddHom fun j ↦ (Quot.ι (F ⋙ uliftFunctor) j).comp AddEquiv.ulift.symm.toAddMonoidHom).ker
Module: Mathlib.Algebra.Category.Grp.Colimits

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
j j' : J
u : j ⟶ j'
a : ↑(F.obj j)
⊢ ((Quot.ι (F ⋙ uliftFunctor) j').comp AddEquiv.ulift.symm.toAddMonoidHom) ((ConcreteCategory.hom (F.map u)) a) -
      (DFinsupp.sumAddHom fun j ↦ (Quot.ι (F ⋙ uliftFunctor) j).comp AddEquiv.ulift.symm.toAddMonoidHom)
        (DFinsupp.single j a) =
    0

Tactic:
DFinsupp.sumAddHom_single

Goal state after:
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
j j' : J
u : j ⟶ j'
a : ↑(F.obj j)
⊢ ((Quot.ι (F ⋙ uliftFunctor) j').comp AddEquiv.ulift.symm.toAddMonoidHom) ((ConcreteCategory.hom (F.map u)) a) -
      ((Quot.ι (F ⋙ uliftFunctor) j).comp AddEquiv.ulift.symm.toAddMonoidHom) a =
    0
Module: Mathlib.Algebra.Category.Grp.Colimits

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
a✝ : Π₀ (j : J), ↑((F ⋙ uliftFunctor).obj j)
⊢ a✝ ∈
      {x |
        ∃ j j' u a,
          x = DFinsupp.single j' ((ConcreteCategory.hom ((F ⋙ uliftFunctor).map u)) a) - DFinsupp.single j a} →
    a✝ ∈ ↑(DFinsupp.sumAddHom fun j ↦ (Quot.ι F j).comp AddEquiv.ulift.toAddMonoidHom).ker

Tactic:
hx

Goal state after:
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
a✝ : Π₀ (j : J), ↑((F ⋙ uliftFunctor).obj j)
hx :
  a✝ ∈
    {x | ∃ j j' u a, x = DFinsupp.single j' ((ConcreteCategory.hom ((F ⋙ uliftFunctor).map u)) a) - DFinsupp.single j a}
⊢ a✝ ∈ ↑(DFinsupp.sumAddHom fun j ↦ (Quot.ι F j).comp AddEquiv.ulift.toAddMonoidHom).ker
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₂ X₃ Y₁ Y₂ Y₃ : C
⊢ tensorμ (X₁ ⊗ X₂) X₃ (Y₁ ⊗ Y₂) Y₃ ≫ tensorμ X₁ X₂ Y₁ Y₂ ▷ (X₃ ⊗ Y₃) ≫ (α_ (X₁ ⊗ Y₁) (X₂ ⊗ Y₂) (X₃ ⊗ Y₃)).hom =
    ((α_ X₁ X₂ X₃).hom ⊗ₘ (α_ Y₁ Y₂ Y₃).hom) ≫ tensorμ X₁ (X₂ ⊗ X₃) Y₁ (Y₂ ⊗ Y₃) ≫ (X₁ ⊗ Y₁) ◁ tensorμ X₂ X₃ Y₂ Y₃

Tactic:
dsimp only [tensorμ]
  calc
    _ = 𝟙 _ ⊗≫ X₁ ◁ X₂ ◁ (β_ X₃ Y₁).hom ▷ Y₂ ▷ Y₃ ⊗≫
      X₁ ◁ ((X₂ ⊗ Y₁) ◁ (β_ X₃ Y₂).hom ≫
        (β_ X₂ Y₁).hom ▷ (Y₂ ⊗ X₃)) ▷ Y₃ ⊗≫ 𝟙 _ := by
          rw [braiding_tensor_right_hom]; monoidal
    _ = _ := by rw [whisker_exchange, braiding_tensor_left_hom]; monoidal

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

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : NonAssocSemiring M
inst✝¹ : NonAssocSemiring N
inst✝ : NonAssocSemiring P
c✝ d✝ c : RingCon M
d : RingCon c.Quotient
⊢ (fun d ↦ mapGen ⇑c.mk') ((fun d ↦ ⟨d.comap c.mk', ⋯⟩) d) = d

Tactic:
ext x y

Goal state after:
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : NonAssocSemiring M
inst✝¹ : NonAssocSemiring N
inst✝ : NonAssocSemiring P
c✝ d✝ c : RingCon M
d : RingCon c.Quotient
x y : c.Quotient
⊢ ((fun d ↦ mapGen ⇑c.mk') ((fun d ↦ ⟨d.comap c.mk', ⋯⟩) d)) x y ↔ d x y
Module: Mathlib.LinearAlgebra.TensorAlgebra.Basic

Goal state before:
pp: case add
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y : TensorAlgebra R M
hx : x ∈ Algebra.adjoin R (Set.range ⇑(ι R))
hy : y ∈ Algebra.adjoin R (Set.range ⇑(ι R))
⊢ x + y ∈ Algebra.adjoin R (Set.range ⇑(ι R))

Tactic:
exact add_mem hx hy

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
x : M
⊢ (ι R) x = 0 ↔ (ι R) x = (ι R) 0

Tactic:
map_zero

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
⊢ (ι R) x = 0 ↔ (ι R) x = 0
Module: Mathlib.LinearAlgebra.TensorAlgebra.Basic

Goal state before:
pp: case refine_2
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ 0 = (algebraMap R (TensorAlgebra R M)) 0

Tactic:
map_zero

Goal state after:
case refine_2
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ 0 = 0
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
x : M
r : R
hx : x = 0 ∧ r = 0
⊢ (Algebra.linearMap R (TensorAlgebra R M)) 0 = 0

Tactic:
map_zero

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
r : R
hx : x = 0 ∧ r = 0
⊢ 0 = 0
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝⁶ : AddCommGroup M
inst✝⁵ : Semiring R
inst✝⁴ : Module Rᵐᵒᵖ M
inst✝³ : Module R M
inst✝² : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
inst✝¹ : Invertible x
inst✝ : Invertible x.fst
this : Invertible x := x.invertibleOfInvertibleFst
⊢ (⅟x).snd = -(⅟x.fst •> x.snd <• ⅟x.fst)

Tactic:
convert! congr_arg (TrivSqZeroExt.snd (R := R) (M := M)) (_ : _ = ⅟x)

Goal state after:
case convert_2
R : Type u
M : Type v
inst✝⁶ : AddCommGroup M
inst✝⁵ : Semiring R
inst✝⁴ : Module Rᵐᵒᵖ M
inst✝³ : Module R M
inst✝² : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
inst✝¹ : Invertible x
inst✝ : Invertible x.fst
this : Invertible x := x.invertibleOfInvertibleFst
⊢ ⅟x = ⅟x
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
⊢ ↑(TensorProduct.assoc R B B B) ∘ₗ LinearMap.rTensor B comul ∘ₗ comul = LinearMap.lTensor B comul ∘ₗ comul

Tactic:
simp only [← ((f : A ≃ₗ[R] B).comp_toLinearMap_symm_eq _ _).2 f.map_comp_comul,
      ← 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
⊢ (((↑(TensorProduct.assoc R B B B) ∘ₗ
            LinearMap.rTensor B ((TensorProduct.map f.toLinearMap f.toLinearMap ∘ₗ comul) ∘ₗ ↑f.toLinearEquiv.symm)) ∘ₗ
          TensorProduct.map f.toLinearMap f.toLinearMap) ∘ₗ
        comul) ∘ₗ
      ↑f.toLinearEquiv.symm =
    ((LinearMap.lTensor B ((TensorProduct.map f.toLinearMap f.toLinearMap ∘ₗ comul) ∘ₗ ↑f.toLinearEquiv.symm) ∘ₗ
          TensorProduct.map f.toLinearMap f.toLinearMap) ∘ₗ
        comul) ∘ₗ
      ↑f.toLinearEquiv.symm
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) → Coalgebra R (A i)
i✝ : n
⊢ (↑(TensorProduct.assoc R ((i : n) → A i) ((i : n) → A i) ((i : n) → A i)) ∘ₗ
        rTensor ((i : n) → A i) comul ∘ₗ comul) ∘ₗ
      LinearMap.single R A i✝ =
    (lTensor ((i : n) → A i) comul ∘ₗ comul) ∘ₗ LinearMap.single R A i✝

Tactic:
simp_rw [comp_assoc, comul_comp_single, ← comp_assoc, lTensor_comp_map, comul_comp_single,
      comp_assoc, ← comp_assoc comul, rTensor_comp_map, comul_comp_single, ← map_comp_rTensor,
      ← map_comp_lTensor, comp_assoc, ← coassoc, ← comp_assoc comul, ← comp_assoc,
      map_map_comp_assoc_eq]

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
M : ModuleCat R
N : ModuleCat S
α β : (extendScalars f).obj M ⟶ N
h : ∀ (m : ↑M), (ConcreteCategory.hom α) (1 ⊗ₜ[R] m) = (ConcreteCategory.hom β) (1 ⊗ₜ[R] m)
⊢ α = β

Tactic:
apply (restrictScalars f).map_injective

Goal state after:
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
M : ModuleCat R
N : ModuleCat S
α β : (extendScalars f).obj M ⟶ N
h : ∀ (m : ↑M), (ConcreteCategory.hom α) (1 ⊗ₜ[R] m) = (ConcreteCategory.hom β) (1 ⊗ₜ[R] m)
⊢ (restrictScalars f).map α = (restrictScalars f).map β
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: case zero
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 : (extendScalars f).obj X ⟶ Y
m1 : Module R S := Module.compHom S f
m2 : Module R ↑Y := Module.compHom (↑Y) f
⊢ 0 = (Hom.hom g) 0

Tactic:
map_zero

Goal state after:
case zero
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 : (extendScalars f).obj X ⟶ Y
m1 : Module R S := Module.compHom S f
m2 : Module R ↑Y := Module.compHom (↑Y) f
⊢ 0 = 0
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: case zero
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
⊢ 0 = (Hom.hom (Counit.map f ≫ (𝟭 (ModuleCat S)).map g)) 0

Tactic:
map_zero

Goal state after:
case zero
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
⊢ 0 = 0
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: case zero
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
⊢ 0 = (Hom.hom ((extendScalars f).map g ≫ (ExtendRestrictScalarsAdj.counit f).app Y)) 0

Tactic:
map_zero

Goal state after:
case zero
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
⊢ 0 = 0
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: R : Type u₁
inst✝ : CommRing R
M : ModuleCat R
⊢ ((extendRestrictScalarsAdj (RingHom.id R)).homEquiv M ((𝟭 (ModuleCat R)).obj M)) ((extendScalarsId R).hom.app M) =
    (restrictScalarsId R).inv.app M

Tactic:
by
  ext m
  rw [extendRestrictScalarsAdj_homEquiv_apply, ← extendScalarsId_inv_app_apply, ← comp_apply]
  simp

Goal state after: