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 : Matrix n n R
i j : n
h : i ≠ j
A' : Matrix n n R := A.updateRow j (A i)
s : ℤˣ
x✝¹ : n
x✝ : x✝¹ ∈ univ
⊢ (fun j ↦ A i j) x✝¹ = (fun j_1 ↦ A' j j_1) x✝¹

Tactic:
simp [A']

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
M : Matrix n n R
j : n
u v : n → R
⊢ (M.updateCol j (u + v)).det = (M.updateCol j u).det + (M.updateCol j v).det

Tactic:
rw [← det_transpose, ← updateRow_transpose, det_updateRow_add]

Goal state after:
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
M : Matrix n n R
j : n
u v : n → R
⊢ (Mᵀ.updateRow j u).det + (Mᵀ.updateRow j v).det = (M.updateCol j u).det + (M.updateCol j v).det
Module: Mathlib.CategoryTheory.Filtered.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : IsCofilteredOrEmpty C
I : Type u_1
inst✝ : Finite I
i : C
j : I → C
f : (x : I) → j x ⟶ i
this : IsCofiltered C
⊢ ∃ k fki g, ∀ (x : I), g x ≫ f x = fki

Tactic:
classical
  cases nonempty_fintype I
  obtain ⟨k, fk, hk⟩ := IsCofiltered.inf_exists (insert i (Finset.univ.image j))
    (Finset.univ.image fun x ↦ ⟨j x, i, by simp, by simp, f x⟩)
  exact ⟨k, _, _, fun x ↦ hk _ _ (Finset.mem_image_of_mem _ (Finset.mem_univ _))⟩

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.ColimitType

Goal state before:
pp: J : Type u
inst✝ : Category.{v, u} J
F : J ⥤ Type w₀
c : F.CoconeTypes
hc : c.IsColimit
j : J
x : F.obj j
⊢ ∃ j_1 x_1, c.ι j_1 x_1 = hc.equiv (F.ιColimitType j x)

Tactic:
exact ⟨j, x, rfl⟩

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Colimits

Goal state before:
pp: J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : HasColimit F
j : J
x : F.obj j
⊢ (colimitEquivColimitType F) ((hom (colimit.ι F j)) x) = Quot.mk F.ColimitTypeRel ⟨j, x⟩

Tactic:
apply (colimitEquivColimitType F).symm.injective

Goal state after:
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : HasColimit F
j : J
x : F.obj j
⊢ (colimitEquivColimitType F).symm ((colimitEquivColimitType F) ((hom (colimit.ι F j)) x)) =
    (colimitEquivColimitType F).symm (Quot.mk F.ColimitTypeRel ⟨j, x⟩)
Module: Mathlib.Algebra.Category.MonCat.FilteredColimits

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

Tactic:
obtain ⟨l, f, g, hfg⟩ := hxx'

Goal state after:
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
j₁ : J
x : ↑(F.obj j₁)
j₂ : J
y : ↑(F.obj j₂)
j₃ : J
x' : ↑(F.obj j₃)
l : J
f : ⟨j₁, x⟩.fst ⟶ l
g : ⟨j₃, x'⟩.fst ⟶ l
hfg :
  (ConcreteCategory.hom ((F ⋙ forget MonCat).map f)) ⟨j₁, x⟩.snd =
    (ConcreteCategory.hom ((F ⋙ forget MonCat).map g)) ⟨j₃, x'⟩.snd
⊢ colimitMulAux F ⟨j₁, x⟩ ⟨j₂, y⟩ = colimitMulAux F ⟨j₃, x'⟩ ⟨j₂, y⟩
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: case e'_3.refine_2
m : Type u_1
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
σ₁ : Perm m × Perm n
a✝¹ : σ₁ ∈ ↑univ
σ₂ : Perm m × Perm n
a✝ : σ₂ ∈ ↑univ
h : σ₁.1.sumCongr σ₁.2 = σ₂.1.sumCongr σ₂.2
⊢ σ₁ = σ₂

Tactic:
have h2 : ∀ x, Perm.sumCongr σ₁.fst σ₁.snd x = Perm.sumCongr σ₂.fst σ₂.snd x :=
          DFunLike.congr_fun h

Goal state after:
case e'_3.refine_2
m : Type u_1
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
σ₁ : Perm m × Perm n
a✝¹ : σ₁ ∈ ↑univ
σ₂ : Perm m × Perm n
a✝ : σ₂ ∈ ↑univ
h : σ₁.1.sumCongr σ₁.2 = σ₂.1.sumCongr σ₂.2
h2 : ∀ (x : m ⊕ n), (σ₁.1.sumCongr σ₁.2) x = (σ₂.1.sumCongr σ₂.2) x
⊢ σ₁ = σ₂
Module: Mathlib.LinearAlgebra.Multilinear.Basic

Goal state before:
pp: R : Type uR
ι : Type uι
M₂ : Type v₂
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₂
inst✝ : Fintype ι
⊢ (∏ i, 1) • 0 = 0 fun x ↦ 1

Tactic:
smul_zero,

Goal state after:
R : Type uR
ι : Type uι
M₂ : Type v₂
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₂
inst✝ : Fintype ι
⊢ 0 = 0 fun x ↦ 1
Module: Mathlib.CategoryTheory.Limits.Types.Limits

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type (max v u)
x✝¹ : Cone F
x✝ : x✝¹.pt ⟶ (limitCone F).pt
w : ∀ (j : J), x✝ ≫ (limitCone F).π.app j = x✝¹.π.app j
⊢ x✝ = ↾fun v ↦ ⟨fun j ↦ (hom (x✝¹.π.app j)) v, ⋯⟩

Tactic:
by
    ext x
    apply Subtype.ext
    funext j
    exact congr_hom (w j) x

Goal state after:
Module: Mathlib.LinearAlgebra.Multilinear.Basic

Goal state before:
pp: case neg.inl
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁵ : Semiring R
inst✝⁴ : (i : ι) → AddCommGroup (M₁ i)
inst✝³ : AddCommGroup M₂
inst✝² : (i : ι) → Module R (M₁ i)
inst✝¹ : Module R M₂
f : MultilinearMap R M₁ M₂
inst✝ : LinearOrder ι
a b v : (i : ι) → M₁ i
s : Finset ι
i : ι
hi hjs : i ∈ s
hji : ¬i < i
⊢ (if i = i then s.piecewise a v i - b i else b i) = if i = i then a i - b i else b i

pp: case neg.inr
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁵ : Semiring R
inst✝⁴ : (i : ι) → AddCommGroup (M₁ i)
inst✝³ : AddCommGroup M₂
inst✝² : (i : ι) → Module R (M₁ i)
inst✝¹ : Module R M₂
f : MultilinearMap R M₁ M₂
inst✝ : LinearOrder ι
a b v : (i : ι) → M₁ i
s : Finset ι
i : ι
hi : i ∈ s
j : ι
hjs : j ∈ s
hji : ¬j < i
hij : i ≠ j
⊢ (if i = j then s.piecewise a v j - b j else b j) = if j = i then a j - b j else b j

Tactic:
· rw [if_pos rfl, if_pos rfl, s.piecewise_eq_of_mem _ _ hi]

Goal state after:
case neg.inr
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁵ : Semiring R
inst✝⁴ : (i : ι) → AddCommGroup (M₁ i)
inst✝³ : AddCommGroup M₂
inst✝² : (i : ι) → Module R (M₁ i)
inst✝¹ : Module R M₂
f : MultilinearMap R M₁ M₂
inst✝ : LinearOrder ι
a b v : (i : ι) → M₁ i
s : Finset ι
i : ι
hi : i ∈ s
j : ι
hjs : j ∈ s
hji : ¬j < i
hij : i ≠ j
⊢ (if i = j then s.piecewise a v j - b j else b j) = if j = i then a j - b j else b j
Module: Mathlib.Algebra.Category.Ring.FilteredColimits

Goal state before:
pp: J : Type v
inst✝² : SmallCategory J
F : J ⥤ CommRingCat
inst✝¹ : IsFilteredOrEmpty J
inst✝ : ∀ (i : J), Nontrivial ↑(F.obj i)
c : Cocone F
hc : IsColimit c
⊢ Nontrivial ↑c.pt

Tactic:
cases isEmpty_or_nonempty J
  · exact ((isColimitEquivIsInitialOfIsEmpty _ _ hc).to (.of (ULift ℤ))).hom.domain_nontrivial
  have i := ‹Nonempty J›.some
  refine ⟨c.ι.app i 0, c.ι.app i 1, fun h ↦ ?_⟩
  have : IsFiltered J := ⟨⟩
  obtain ⟨k, f, e⟩ :=
    (Types.FilteredColimit.isColimit_eq_iff' (isColimitOfPreserves (forget _) hc) _ _).mp h
  exact zero_ne_one (((F.map f).hom.map_zero.symm.trans e).trans (F.map f).hom.map_one)

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 K₁ K₂ : J ⥤ C
F : C ⥤ D
h : K₁ ≅ K₂
inst✝ : CreatesLimit K₁ F
c : Cone (K₂ ⋙ F)
t : IsLimit c
t' : IsLimit ((Cone.postcompose (isoWhiskerRight h F).inv).obj c) :=
  (IsLimit.postcomposeInvEquiv (isoWhiskerRight h F) c).symm t
j : J
⊢ ((Cone.postcompose (isoWhiskerRight h F).hom).obj ((Cone.postcompose (isoWhiskerRight h F).inv).obj c)).π.app j =
    (Iso.refl
          ((Cone.postcompose (isoWhiskerRight h F).hom).obj
              ((Cone.postcompose (isoWhiskerRight h F).inv).obj c)).pt).hom ≫
      c.π.app j

Tactic:
by
                dsimp
                rw [Category.assoc, ← F.map_comp]
                simp

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

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ CommGrpCat
c : Cone (F ⋙ forget₂ CommGrpCat GrpCat)
hc : IsLimit c
this✝² : HasLimit (F ⋙ forget₂ CommGrpCat GrpCat)
this✝¹ : Small.{u, max u v} ↑(F ⋙ forget CommGrpCat).sections
this✝ : Small.{u, max u v} ↑((F ⋙ forget₂ CommGrpCat GrpCat ⋙ forget₂ GrpCat MonCat) ⋙ forget MonCat).sections
this : Small.{u, max u v} ↑((F ⋙ forget₂ CommGrpCat GrpCat) ⋙ forget GrpCat).sections
⊢ IsLimit
    ((forget₂ CommGrpCat GrpCat ⋙ forget₂ GrpCat MonCat).mapCone
      { pt := of (Types.Small.limitCone (F ⋙ forget CommGrpCat)).pt,
        π :=
          { app := fun j ↦ ofHom (MonCat.limitπMonoidHom (F ⋙ forget₂ CommGrpCat GrpCat ⋙ forget₂ GrpCat MonCat) j),
            naturality := ⋯ } })

Tactic:
apply MonCat.HasLimits.limitConeIsLimit _

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

Goal state before:
pp: J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ RingCat
inst✝ : Small.{u, max u v} ↑(F ⋙ forget RingCat).sections
this✝ : (forget₂ RingCat SemiRingCat).ReflectsIsomorphisms
this : Small.{u, max u v} ↑((F ⋙ forget₂ RingCat SemiRingCat) ⋙ forget SemiRingCat).sections
c : Cone F :=
  { pt := of (Types.Small.limitCone (F ⋙ forget RingCat)).pt,
    π := { app := fun x ↦ ofHom (SemiRingCat.limitπRingHom (F ⋙ forget₂ RingCat SemiRingCat) x), naturality := ⋯ } }
c' : Cone (F ⋙ forget₂ RingCat SemiRingCat)
t : IsLimit c'
⊢ IsLimit ((forget₂ RingCat SemiRingCat).mapCone c)

Tactic:
apply SemiRingCat.HasLimits.limitConeIsLimit _

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
f : J → C
X : C
j : J
⊢ biproduct.ι (fun j ↦ f j ⊗ X) j ≫ (rightDistributor f X).inv = biproduct.ι f j ▷ X

Tactic:
cases nonempty_fintype J
  simp [rightDistributor_inv, Preadditive.comp_sum, biproduct.ι_π_assoc,
    dite_comp]

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
W✝ W W'✝ : MorphismProperty C
W' : ?m.4
P Q : MorphismProperty C
inst✝¹ : P.HasTwoOutOfThreeProperty
inst✝ : Q.HasTwoOutOfThreeProperty
this✝ : P.HasOfPostcompProperty (P ⊓ Q)
this : P.HasOfPrecompProperty (P ⊓ Q)
⊢ (P ⊓ Q).HasTwoOutOfThreeProperty

Tactic:
have : Q.HasOfPostcompProperty (P ⊓ Q) := .of_le _ _ inf_le_right

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
W✝ W W'✝ : MorphismProperty C
W' : ?m.4
P Q : MorphismProperty C
inst✝¹ : P.HasTwoOutOfThreeProperty
inst✝ : Q.HasTwoOutOfThreeProperty
this✝¹ : P.HasOfPostcompProperty (P ⊓ Q)
this✝ : P.HasOfPrecompProperty (P ⊓ Q)
this : Q.HasOfPostcompProperty (P ⊓ Q)
⊢ (P ⊓ Q).HasTwoOutOfThreeProperty
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:
by rw [injective_eq_monomorphisms]

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 G : C ⥤ D
inst✝ : F.Monoidal
i : F ≅ G
X : C
⊢ (λ_ (G.obj X)).hom =
    (LaxMonoidal.ε F ⊗ₘ i.inv.app X) ≫ LaxMonoidal.μ F (𝟙_ C) X ≫ i.hom.app (𝟙_ C ⊗ X) ≫ G.map (λ_ X).hom

Tactic:
rw [← i.hom.naturality, ← Category.comp_id (i.inv.app X),
      ← Category.id_comp (Functor.LaxMonoidal.ε F), ← tensorHom_comp_tensorHom]

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 G : C ⥤ D
inst✝ : F.Monoidal
i : F ≅ G
X : C
⊢ (λ_ (G.obj X)).hom =
    ((𝟙 (𝟙_ D) ⊗ₘ i.inv.app X) ≫ (LaxMonoidal.ε F ⊗ₘ 𝟙 (F.obj X))) ≫
      LaxMonoidal.μ F (𝟙_ C) X ≫ F.map (λ_ X).hom ≫ i.hom.app X
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F G : C ⥤ D
inst✝ : F.Monoidal
i : F ≅ G
X : C
⊢ (ρ_ (G.obj X)).hom =
    (i.inv.app X ⊗ₘ LaxMonoidal.ε F) ≫ LaxMonoidal.μ F X (𝟙_ C) ≫ i.hom.app (X ⊗ 𝟙_ C) ≫ G.map (ρ_ X).hom

Tactic:
rw [← i.hom.naturality, ← Category.comp_id (i.inv.app X),
      ← Category.id_comp (Functor.LaxMonoidal.ε F), ← tensorHom_comp_tensorHom]

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 G : C ⥤ D
inst✝ : F.Monoidal
i : F ≅ G
X : C
⊢ (ρ_ (G.obj X)).hom =
    ((i.inv.app X ⊗ₘ 𝟙 (𝟙_ D)) ≫ (𝟙 (F.obj X) ⊗ₘ LaxMonoidal.ε F)) ≫
      LaxMonoidal.μ F X (𝟙_ C) ≫ F.map (ρ_ X).hom ≫ i.hom.app X
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 =
    ((α_ (𝟙_ C) X₁ (𝟙_ C ⊗ X₂)).hom ≫
        𝟙_ C ◁ (α_ X₁ (𝟙_ C) X₂).inv ≫
          𝟙_ C ◁ (β_ X₁ (𝟙_ C)).hom ▷ X₂ ≫ 𝟙_ C ◁ (α_ (𝟙_ C) X₁ X₂).hom ≫ (α_ (𝟙_ C) (𝟙_ C) (X₁ ⊗ X₂)).inv) ≫
      (λ_ (𝟙_ C)).hom ▷ (X₁ ⊗ X₂) ≫ (λ_ (X₁ ⊗ X₂)).hom

Tactic:
have :
    (λ_ X₁).hom ⊗ₘ (λ_ X₂).hom =
      (α_ (𝟙_ C) X₁ (𝟙_ C ⊗ X₂)).hom ≫
        (𝟙_ C ◁ (α_ X₁ (𝟙_ C) X₂).inv) ≫ (λ_ ((X₁ ⊗ 𝟙_ C) ⊗ X₂)).hom ≫ ((ρ_ X₁).hom ▷ X₂) := by
    monoidal

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ : C
this :
  (λ_ X₁).hom ⊗ₘ (λ_ X₂).hom =
    (α_ (𝟙_ C) X₁ (𝟙_ C ⊗ X₂)).hom ≫ 𝟙_ C ◁ (α_ X₁ (𝟙_ C) X₂).inv ≫ (λ_ ((X₁ ⊗ 𝟙_ C) ⊗ X₂)).hom ≫ (ρ_ X₁).hom ▷ X₂
⊢ (λ_ X₁).hom ⊗ₘ (λ_ X₂).hom =
    ((α_ (𝟙_ C) X₁ (𝟙_ C ⊗ X₂)).hom ≫
        𝟙_ C ◁ (α_ X₁ (𝟙_ C) X₂).inv ≫
          𝟙_ C ◁ (β_ X₁ (𝟙_ C)).hom ▷ X₂ ≫ 𝟙_ C ◁ (α_ (𝟙_ C) X₁ X₂).hom ≫ (α_ (𝟙_ C) (𝟙_ C) (X₁ ⊗ X₂)).inv) ≫
      (λ_ (𝟙_ C)).hom ▷ (X₁ ⊗ X₂) ≫ (λ_ (X₁ ⊗ 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
r₁ r₂ : R
⊢ 0 = r₁ •> 0 + 0 <• r₂

Tactic:
smul_zero,

Goal state after:
R : Type u
M : Type v
inst✝³ : Monoid R
inst✝² : AddMonoid M
inst✝¹ : DistribMulAction R M
inst✝ : DistribMulAction Rᵐᵒᵖ M
r₁ r₂ : R
⊢ 0 = 0 + 0 <• r₂
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : MonoidWithZero R
inst✝² : AddMonoid M
inst✝¹ : DistribMulAction R M
inst✝ : DistribMulAction Rᵐᵒᵖ M
r : R
m : M
⊢ r •> m + 0 •> 0 = r •> m

Tactic:
smul_zero,

Goal state after:
R : Type u
M : Type v
inst✝³ : MonoidWithZero R
inst✝² : AddMonoid M
inst✝¹ : DistribMulAction R M
inst✝ : DistribMulAction Rᵐᵒᵖ M
r : R
m : M
⊢ r •> m + 0 = r •> m
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : MonoidWithZero R
inst✝² : AddMonoid M
inst✝¹ : DistribMulAction R M
inst✝ : DistribMulAction Rᵐᵒᵖ M
r : R
m : M
⊢ 0 •> 0 + m <• r = m <• r

Tactic:
smul_zero,

Goal state after:
R : Type u
M : Type v
inst✝³ : MonoidWithZero R
inst✝² : AddMonoid M
inst✝¹ : DistribMulAction R M
inst✝ : DistribMulAction Rᵐᵒᵖ M
r : R
m : M
⊢ 0 + m <• r = m <• r
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
r : R
x : tsze R M
⊢ r •> x.snd + 0 <• x.fst = r •> x.snd

Tactic:
smul_zero,

Goal state after:
R : Type u
M : Type v
inst✝³ : Monoid R
inst✝² : AddMonoid M
inst✝¹ : DistribMulAction R M
inst✝ : DistribMulAction Rᵐᵒᵖ M
r : R
x : tsze R M
⊢ r •> x.snd + 0 = r •> x.snd
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 : tsze R M
r : R
⊢ x.fst •> 0 + x.snd <• r = x.snd <• r

Tactic:
smul_zero,

Goal state after:
R : Type u
M : Type v
inst✝³ : Monoid R
inst✝² : AddMonoid M
inst✝¹ : DistribMulAction R M
inst✝ : DistribMulAction Rᵐᵒᵖ M
x : tsze R M
r : R
⊢ 0 + x.snd <• r = x.snd <• r
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.2 + 0 <• x.1 = x.2

Tactic:
smul_zero,

Goal state after:
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.2 + 0 = x.2
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:
smul_zero,

Goal state after:
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)
⊢ 0 + x.2 <• 1 = x.2
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module Rᵐᵒᵖ M
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ x.1 •> 0 + 0 •> x.2 = 0

Tactic:
smul_zero,

Goal state after:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module Rᵐᵒᵖ M
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ 0 + 0 •> x.2 = 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
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
inst✝ : Invertible x
⊢ (x * ⅟x).fst = 1

Tactic:
mul_invOf_self,

Goal state after:
R : Type u
M : Type v
inst✝⁴ : AddCommGroup M
inst✝³ : Semiring R
inst✝² : Module Rᵐᵒᵖ M
inst✝¹ : Module R M
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
inst✝ : Invertible x
⊢ fst 1 = 1
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: case h2
R : Type u
M : Type v
inst✝³ : DivisionSemiring R
inst✝² : AddCommGroup M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : Module R M
r : R
⊢ -(r⁻¹ •> 0 <• r⁻¹) = 0

Tactic:
smul_zero,

Goal state after:
case h2
R : Type u
M : Type v
inst✝³ : DivisionSemiring R
inst✝² : AddCommGroup M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : Module R M
r : R
⊢ -(0 <• r⁻¹) = 0
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: case h2
R : Type u
M : Type v
inst✝³ : DivisionSemiring R
inst✝² : AddCommGroup M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : Module R M
r : R
⊢ -(0 <• r⁻¹) = 0

Tactic:
smul_zero,

Goal state after:
case h2
R : Type u
M : Type v
inst✝³ : DivisionSemiring R
inst✝² : AddCommGroup M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : Module R M
r : R
⊢ -0 = 0
Module: Mathlib.CategoryTheory.Adjunction.Mates

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
inst✝² : Category.{v₁, u₁} A
inst✝¹ : Category.{v₂, u₂} B
inst✝ : Category.{v₃, u₃} C
L₁ L₂ : B ⥤ C
R₁ R₂ : C ⥤ B
L : A ⥤ B
R : B ⥤ A
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj : L ⊣ R
τ : L₂ ⟶ L₁
X : C
h₁ :
  (R₂ ⋙ R).map (L₂.map (adj.counit.app (R₁.obj X))) ≫ (R₂ ⋙ R).map (τ.app (R₁.obj X)) =
    (R₂ ⋙ R).map (τ.app (L.obj (R.obj (R₁.obj X)))) ≫ (R₂ ⋙ R).map (L₁.map (adj.counit.app (R₁.obj X)))
h₂ :
  R.map (adj₂.unit.app (L.obj (R.obj (R₁.obj X)))) ≫ R.map (R₂.map (L₂.map (adj.counit.app (R₁.obj X)))) =
    R.map (adj.counit.app (R₁.obj X)) ≫ R.map (adj₂.unit.app (R₁.obj X))
⊢ ((conjugateEquiv (adj.comp adj₁) (adj.comp adj₂)) (L.whiskerLeft τ)).app X =
    (whiskerRight ((conjugateEquiv adj₁ adj₂) τ) R).app X

Tactic:
simp [← reassoc_of% h₁, reassoc_of% h₂]

Goal state after:
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
s : S
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ (algebraMap S R) s •> x.snd + 0 <• x.fst = x.fst •> 0 + x.snd <• (algebraMap S R) s

Tactic:
smul_zero,

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

Tactic:
smul_zero,

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