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

Goal state before:
pp: m : Type u_1
n : Type u_2
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
R : Type u_3
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
e₁ e₂ : n ≃ m
A : Matrix m m R
⊢ |(A.submatrix ⇑e₁ ⇑e₂).det| = |A.det|

Tactic:
have hee : e₂ = e₁.trans (e₁.symm.trans e₂) := by ext; simp
  rw [hee]
  change |((A.submatrix id (e₁.symm.trans e₂)).submatrix e₁ e₁).det| = |A.det|
  rw [Matrix.det_submatrix_equiv_self, Matrix.det_permute', abs_mul, abs_unit_intCast, one_mul]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: n : Type u_2
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
inst✝ : Nontrivial n
u v : n → R
i j : n
hij : i ≠ j
uv' : Matrix n n R := ((vecMulVec u v).updateRow i v).updateRow j v
huv' : uv'.det = 0
this : vecMulVec u v = (uv'.updateRow i (u i • uv' i)).updateRow j (u j • uv'.updateRow i (u i • uv' i) j)
⊢ (vecMulVec u v).det = 0

Tactic:
rw [this, det_updateRow_smul, updateRow_eq_self, det_updateRow_smul, updateRow_eq_self, huv',
    mul_zero, mul_zero]

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

Goal state before:
pp: case refine_1
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
x y : M F
⊢ ∀ (a b₁ b₂ : (j : J) × ↑(F.obj j)),
    (F ⋙ forget MonCat).ColimitTypeRel b₁ b₂ → colimitMulAux F a b₁ = colimitMulAux F a b₂

Tactic:
intro x y y' h
      apply colimitMulAux_eq_of_rel_right
      apply Types.FilteredColimit.rel_of_colimitTypeRel
      exact h

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

Goal state before:
pp: case refine_2
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
x y : M F
⊢ ∀ (a₁ a₂ b : (j : J) × ↑(F.obj j)),
    (F ⋙ forget MonCat).ColimitTypeRel a₁ a₂ → colimitMulAux F a₁ b = colimitMulAux F a₂ b

Tactic:
intro x x' y h
      apply colimitMulAux_eq_of_rel_left
      apply Types.FilteredColimit.rel_of_colimitTypeRel
      exact h

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K : J ⥤ C
F : C ⥤ D
inst✝ : CreatesLimit K F
c : Cone (K ⋙ F)
t : IsLimit c
j : J
⊢ (liftedLimitMapsToOriginal t).hom.hom ≫ c.π.app j = F.map ((liftLimit t).π.app j)

Tactic:
by
  rw [← liftedLimitMapsToOriginal_inv_map_π (t := t)]
  simp only [← Category.assoc, ← Cone.category_comp_hom,
    Iso.hom_inv_id, Cone.category_id_hom, Category.id_comp]

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

Goal state before:
pp: case refine_1
R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : Category.{t, v} J
F : J ⥤ ModuleCat R
inst✝ : Small.{w, max v w} ↑(F ⋙ forget (ModuleCat R)).sections
s : Cone F
⊢ ∀ (x y : ↑s.1),
    (ConcreteCategory.hom
          ((Types.Small.limitConeIsLimit (F ⋙ forget (ModuleCat R))).lift ((forget (ModuleCat R)).mapCone s)))
        (x + y) =
      (ConcreteCategory.hom
            ((Types.Small.limitConeIsLimit (F ⋙ forget (ModuleCat R))).lift ((forget (ModuleCat R)).mapCone s)))
          x +
        (ConcreteCategory.hom
            ((Types.Small.limitConeIsLimit (F ⋙ forget (ModuleCat R))).lift ((forget (ModuleCat R)).mapCone s)))
          y

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

Tactic:
· intro x y
    simp [← equivShrink_add]
    rfl

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

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

Tactic:
· intro x y
    simp [← equivShrink_add]
    rfl

Goal state after:
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:
let : G.Monoidal := transport e

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
F G : C ⥤ D
inst✝ : F.Monoidal
e : F ≅ G
this : G.Monoidal := transport e
⊢ NatTrans.IsMonoidal e.hom
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
f : J → C
X : C
j : J
⊢ (rightDistributor f X).inv ≫ biproduct.π f j ▷ X = biproduct.π (fun j ↦ f j ⊗ X) j

Tactic:
by
  classical
  cases nonempty_fintype J
  simp [rightDistributor_inv, Preadditive.sum_comp, ← comp_whiskerRight,
    biproduct.ι_π, dite_whiskerRight, comp_dite]

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
F : Jᵒᵖ ⥤ Cᵒᵖ
c : Cone F
hc : IsLimit c
s : Cocone F.unop
m : (coconeUnopOfCone c).pt ⟶ s.pt
w : ∀ (j : J), (coconeUnopOfCone c).ι.app j ≫ m = s.ι.app j
j : Jᵒᵖ
⊢ (m.op ≫ c.π.app j).unop = ((hc.lift (coneOfCoconeUnop s)).unop.op ≫ c.π.app j).unop

Tactic:
simpa only [Quiver.Hom.op_unop, IsLimit.fac] using! w (unop j)

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

Goal state before:
pp: case h₁
C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
inst✝⁷ : MonoidalCategory C
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : MonoidalCategory D
E : Type u₃
inst✝⁴ : Category.{v₃, u₃} E
inst✝³ : MonoidalCategory E
C' : Type u₁'
inst✝² : Category.{v₁', u₁'} C'
F✝ F : C ⥤ D
G : C ⥤ E
inst✝¹ : F.Monoidal
inst✝ : G.Monoidal
⊢ (ε (F.prod' G) ≫ η (F.prod' G)).1 = (𝟙 (𝟙_ (D × E))).1

Tactic:
simp only [CategoryTheory.prod_comp_fst, prod'_ε_fst, prod'_η_fst, ε_η,
        prodMonoidal_tensorUnit, prod_id]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic

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

Tactic:
by
  apply (cancel_epi (α_ X Y Z).inv).1
  apply (cancel_mono (α_ Z X Y).inv).1
  simp [hexagon_reverse]

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Composition

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
W : Set (MorphismProperty C)
h : ∀ W' ∈ W, W'.IsStableUnderComposition
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
hf : InfSet.sInf W f
hg : InfSet.sInf W g
⊢ InfSet.sInf W (f ≫ g)

Tactic:
rw [sInf_iff] at hf hg ⊢
    exact fun W' hW' ↦ (h W' hW').comp_mem _ _ (hf _ hW') (hg _ hW')

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

Goal state before:
pp: R : Type u
inst✝² : Ring R
X Y : ModuleCat R
f✝ : X ⟶ Y
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
X✝ Y✝ : ModuleCat R
f : X✝ ⟶ Y✝
hf : Mono f
⊢ Mono ((forget (ModuleCat R)).map f)

Tactic:
rw [CategoryTheory.ofHom_mono_iff_injective, ← mono_iff_injective]
      exact hf

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 : C ≌ D
inst✝² : e.functor.Monoidal
inst✝¹ : e.inverse.Monoidal
inst✝ : e.IsMonoidal
X Y : C
⊢ e.counitIso.inv.app (e.functor.obj X ⊗ e.functor.obj Y) ≫
      e.functor.map (δ e.inverse (e.functor.obj X) (e.functor.obj Y)) =
    μ e.functor X Y ≫ e.functor.map (e.unitIso.hom.app X ⊗ₘ e.unitIso.hom.app Y)

Tactic:
rw [← cancel_epi (δ e.functor _ _), Monoidal.δ_μ_assoc]
  apply e.inverse.map_injective
  simp [← cancel_epi (e.unitIso.hom.app (X ⊗ Y)), Functor.map_comp,
    unitIso_hom_app_tensor_comp_inverse_map_δ_functor_assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
inst✝³ : BraidedCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
inst✝ : BraidedCategory D
F : C ⥤ D
⊢ Function.Injective (@toMonoidal C inst✝⁵ inst✝⁴ inst✝³ D inst✝² inst✝¹ inst✝ F)

Tactic:
rintro ⟨⟩ ⟨⟩ rfl

Goal state after:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
inst✝³ : BraidedCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
inst✝ : BraidedCategory D
F : C ⥤ D
toMonoidal✝ : F.Monoidal
braided✝¹ : ∀ (X Y : C), μ F X Y ≫ F.map (β_ X Y).hom = (β_ (F.obj X) (F.obj Y)).hom ≫ μ F Y X
braided✝ : ∀ (X Y : C), μ F X Y ≫ F.map (β_ X Y).hom = (β_ (F.obj X) (F.obj Y)).hom ≫ μ F Y X
⊢ { toMonoidal := toMonoidal✝, braided := braided✝¹ } =
    { toMonoidal := { toMonoidal := toMonoidal✝, braided := braided✝¹ }.toMonoidal, braided := braided✝ }
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₁).hom ⊗ₘ (λ_ X₂).hom = tensorμ (𝟙_ C) X₁ (𝟙_ C) X₂ ≫ (λ_ (𝟙_ C)).hom ▷ (X₁ ⊗ X₂) ≫ (λ_ (X₁ ⊗ X₂)).hom

Tactic:
by
  dsimp only [tensorμ]
  have :
    (λ_ X₁).hom ⊗ₘ (λ_ X₂).hom =
      (α_ (𝟙_ C) X₁ (𝟙_ C ⊗ X₂)).hom ≫
        (𝟙_ C ◁ (α_ X₁ (𝟙_ C) X₂).inv) ≫ (λ_ ((X₁ ⊗ 𝟙_ C) ⊗ X₂)).hom ≫ ((ρ_ X₁).hom ▷ X₂) := by
    monoidal
  simp [this]

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₆
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₂
b : B
⊢ adj₃.unit.app (G₂.obj (G₁.obj (R₁.obj b))) ≫
      R₃.map (β.natTrans.app (G₁.obj (R₁.obj b))) ≫
        R₃.map (H₂.map (α.natTrans.app (R₁.obj b))) ≫ R₃.map (H₂.map (H₁.map (adj₁.counit.app b))) =
    ((adj₃.unit.app (G₂.obj (G₁.obj (R₁.obj b))) ≫
          R₃.map (L₃.map (G₂.map (adj₂.unit.app (G₁.obj (R₁.obj b))) ≫ G₂.map (R₂.map (α.natTrans.app (R₁.obj b))))) ≫
            R₃.map (L₃.map (G₂.map (R₂.map (H₁.map (adj₁.counit.app b)))))) ≫
        R₃.map (β.natTrans.app (R₂.obj (H₁.obj b)))) ≫
      R₃.map (H₂.map (adj₂.counit.app (H₁.obj b)))

Tactic:
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]

Goal state after:
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₂
b : B
⊢ adj₃.unit.app (G₂.obj (G₁.obj (R₁.obj b))) ≫
      R₃.map (β.natTrans.app (G₁.obj (R₁.obj b))) ≫
        R₃.map (H₂.map (α.natTrans.app (R₁.obj b))) ≫ R₃.map (H₂.map (H₁.map (adj₁.counit.app b))) =
    adj₃.unit.app (G₂.obj (G₁.obj (R₁.obj b))) ≫
      R₃.map
          (β.app (G₁.obj (R₁.obj b)) ≫
            (L₂ ⋙ H₂).map
              ((adj₂.unit.app (G₁.obj (R₁.obj b)) ≫ R₂.map (α.natTrans.app (R₁.obj b))) ≫
                R₂.map (H₁.map (adj₁.counit.app b)))) ≫
        R₃.map (H₂.map (adj₂.counit.app (H₁.obj b)))
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
⊢ IsUnit x ↔ IsUnit x.fst

Tactic:
by
  simp only [← nonempty_invertible_iff_isUnit, (invertibleEquivInvertibleFst x).nonempty_congr]

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

Goal state before:
pp: 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)⁻¹ = b⁻¹ * a⁻¹

Tactic:
ext
  · rw [fst_inv, fst_mul, fst_mul, mul_inv_rev, fst_inv, fst_inv]
  · simp only [snd_inv, snd_mul, fst_mul, fst_inv]
    simp only [smul_neg, smul_add]
    simp_rw [mul_inv_rev, smul_comm (_ : R), op_smul_op_smul, smul_smul, add_comm, neg_add]
    obtain ha0 | ha := eq_or_ne (fst a) 0
    · simp [ha0]
    obtain hb0 | hb := eq_or_ne (fst b) 0
    · simp [hb0]
    rw [inv_mul_cancel_right₀ ha, mul_inv_cancel_left₀ hb]

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

Goal state before:
pp: 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
x : tsze R M
hx : x.fst ≠ 0
⊢ 1 * x⁻¹⁻¹ = x * x⁻¹ * x⁻¹⁻¹

Tactic:
TrivSqZeroExt.mul_inv_cancel hx

Goal state after:
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
x : tsze R M
hx : x.fst ≠ 0
⊢ 1 * x⁻¹⁻¹ = 1 * x⁻¹⁻¹
Module: Mathlib.RingTheory.Coalgebra.Basic

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

Tactic:
ext : 1
    · rw [comp_assoc, comul_comp_inl, ← comp_assoc, rTensor_comp_map, counit_comp_inl,
        ← lTensor_comp_rTensor, comp_assoc, rTensor_counit_comp_comul, lTensor_comp_mk]
    · rw [comp_assoc, comul_comp_inr, ← comp_assoc, rTensor_comp_map, counit_comp_inr,
        ← lTensor_comp_rTensor, comp_assoc, rTensor_counit_comp_comul, lTensor_comp_mk]

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

Tactic:
simp only [Functor.comp_obj, Functor.id_obj, leftAdjointUniq, Iso.symm_hom,
    conjugateIsoEquiv_symm_apply_inv, Iso.refl_inv, NatTrans.comp_app, whiskerLeft_app,
    conjugateEquiv_symm_apply_app, NatTrans.id_app, Functor.map_id, Category.id_comp,
    Category.assoc]

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
M N O : C
inst✝² : ComonObj M
inst✝¹ : ComonObj N
inst✝ : ComonObj O
A : Mon Cᵒᵖ
⊢ μ.unop ≫ (η ▷ A.X).unop = (λ_ (unop A.X)).inv

Tactic:
← unop_comp,

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
M N O : C
inst✝² : ComonObj M
inst✝¹ : ComonObj N
inst✝ : ComonObj O
A : Mon Cᵒᵖ
⊢ (η ▷ A.X ≫ μ).unop = (λ_ (unop A.X)).inv
Module: Mathlib.CategoryTheory.Monoidal.Comon_

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
M N O : C
inst✝² : ComonObj M
inst✝¹ : ComonObj N
inst✝ : ComonObj O
A : Mon Cᵒᵖ
⊢ μ.unop ≫ (A.X ◁ η).unop = (ρ_ (unop A.X)).inv

Tactic:
← unop_comp,

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
M N O : C
inst✝² : ComonObj M
inst✝¹ : ComonObj N
inst✝ : ComonObj O
A : Mon Cᵒᵖ
⊢ (A.X ◁ η ≫ μ).unop = (ρ_ (unop A.X)).inv
Module: Mathlib.CategoryTheory.Monoidal.Comon_

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
M N O : C
inst✝² : ComonObj M
inst✝¹ : ComonObj N
inst✝ : ComonObj O
A : Mon Cᵒᵖ
⊢ μ.unop ≫ (A.X ◁ μ).unop = (μ ▷ A.X ≫ μ).unop ≫ (α_ (unop A.X) (unop A.X) (unop A.X)).hom

Tactic:
← unop_comp,

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
M N O : C
inst✝² : ComonObj M
inst✝¹ : ComonObj N
inst✝ : ComonObj O
A : Mon Cᵒᵖ
⊢ (A.X ◁ μ ≫ μ).unop = (μ ▷ A.X ≫ μ).unop ≫ (α_ (unop A.X) (unop A.X) (unop A.X)).hom
Module: Mathlib.RingTheory.Coalgebra.CoassocSimps

Goal state before:
pp: R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : Coalgebra R M
f : M →ₗ[R] N
⊢ α ∘ₗ (β ∘ₗ δ) ⊗ₘ f ∘ₗ δ = LinearMap.id ⊗ₘ (LinearMap.id ⊗ₘ f ∘ₗ β) ∘ₗ α ∘ₗ δ ⊗ₘ LinearMap.id ∘ₗ β ∘ₗ δ

Tactic:
rw [← symm_comp_map_assoc, ← LinearMap.lTensor_def, ← LinearMap.lTensor_def,
    ← LinearMap.lTensor_def, ← Coalgebra.coassoc, ← f.comp_id,
    TensorProduct.map_comp, ← LinearMap.rTensor_def]

Goal state after:
R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : Coalgebra R M
f : M →ₗ[R] N
⊢ α ∘ₗ (β ⊗ₘ f ∘ₗ LinearMap.rTensor M δ) ∘ₗ δ =
    LinearMap.lTensor M (LinearMap.lTensor M (f ∘ₗ LinearMap.id) ∘ₗ β) ∘ₗ α ∘ₗ β ∘ₗ α ∘ₗ LinearMap.rTensor M δ ∘ₗ δ
Module: Mathlib.RingTheory.TwoSidedIdeal.Operations

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
s : Set R
x : R
h : x ∈ { ringCon := sInf {s_1 | ∀ (x y : R), x - y ∈ s → s_1 x y} }
⊢ ∀ (I : TwoSidedIdeal R), s ⊆ ↑I → x ∈ I

Tactic:
I

Goal state after:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
s : Set R
x : R
h : x ∈ { ringCon := sInf {s_1 | ∀ (x y : R), x - y ∈ s → s_1 x y} }
I : TwoSidedIdeal R
⊢ s ⊆ ↑I → x ∈ I
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
S : Type u_2
inst✝ : CommSemiring S
f : R →+* S
a : R
H : ∀ (a_1 : S), ∃ b m, f b = f a ^ m * a_1
b : R
⊢ ∀ (a_1 : S), ∃ b_1 m, f b_1 = f (a * b) ^ m * a_1

Tactic:
refine fun x ↦ ?_

Goal state after:
R : Type u_1
inst✝¹ : CommSemiring R
S : Type u_2
inst✝ : CommSemiring S
f : R →+* S
a : R
H : ∀ (a_1 : S), ∃ b m, f b = f a ^ m * a_1
b : R
x : S
⊢ ∃ b_1 m, f b_1 = f (a * b) ^ m * x
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
⊢ ∃ x, ∀ (a : ↑↑s), (algebraMap R (Away ↑a)) x = f a

Tactic:
have eq a : f a * algebraMap R _ (a ^ N) = algebraMap R _ (r a) := by
    rw [map_mul, ← eq, mul_left_comm, ← map_mul, ← pow_add]

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)
⊢ ∃ x, ∀ (a : ↑↑s), (algebraMap R (Away ↑a)) x = f a
Module: Mathlib.CategoryTheory.Limits.Shapes.StrictInitial

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Quiver.IsThin C
I A : C
f : I ⟶ A
hI : IsTerminal I
⊢ IsIso f

Tactic:
CategoryTheory.isIso_iff_of_thin

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Quiver.IsThin C
I A : C
f : I ⟶ A
hI : IsTerminal I
⊢ Nonempty (A ⟶ I)
Module: Mathlib.RingTheory.Localization.BaseChange

Goal state before:
pp: R : Type u_1
inst✝¹¹ : CommSemiring R
S : Submonoid R
A : Type u_2
inst✝¹⁰ : CommSemiring A
inst✝⁹ : Algebra R A
inst✝⁸ : IsLocalization S A
M₁ : Type u_5
M₂ : Type u_6
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : Module R M₁
inst✝⁴ : Module R M₂
inst✝³ : Module A M₁
inst✝² : Module A M₂
inst✝¹ : IsScalarTower R A M₁
inst✝ : IsScalarTower R A M₂
x✝¹ : M₁
x✝ : M₂
r : R
s : ↥S
⊢ ↑s • (mk' A r s • x✝¹) ⊗ₜ[R] x✝ = ↑s • x✝¹ ⊗ₜ[R] (mk' A r s • x✝)

Tactic:
smul_tmul',

Goal state after:
R : Type u_1
inst✝¹¹ : CommSemiring R
S : Submonoid R
A : Type u_2
inst✝¹⁰ : CommSemiring A
inst✝⁹ : Algebra R A
inst✝⁸ : IsLocalization S A
M₁ : Type u_5
M₂ : Type u_6
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : Module R M₁
inst✝⁴ : Module R M₂
inst✝³ : Module A M₁
inst✝² : Module A M₂
inst✝¹ : IsScalarTower R A M₁
inst✝ : IsScalarTower R A M₂
x✝¹ : M₁
x✝ : M₂
r : R
s : ↥S
⊢ (↑s • mk' A r s • x✝¹) ⊗ₜ[R] x✝ = (↑s • x✝¹) ⊗ₜ[R] (mk' A r s • x✝)