mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Opposites

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
⊢ HasFiniteWidePullbacks Cᵒᵖ ↔ HasFiniteWidePushouts C

Tactic:
refine ⟨fun h ↦ ⟨fun J _ ↦ ?_⟩, fun _ ↦ inferInstance⟩

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
h : HasFiniteWidePullbacks Cᵒᵖ
J : Type
x✝ : Finite J
⊢ HasColimitsOfShape (WidePushoutShape J) C
Module: Mathlib.CategoryTheory.Limits.Opposites

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
⊢ HasFiniteWidePushouts Cᵒᵖ ↔ HasFiniteWidePullbacks C

Tactic:
refine ⟨fun h ↦ ⟨fun J _ ↦ ?_⟩, fun _ ↦ inferInstance⟩

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
h : HasFiniteWidePushouts Cᵒᵖ
J : Type
x✝ : Finite J
⊢ HasLimitsOfShape (WidePullbackShape J) C
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
W X Y : C
f : W ⟶ X
g : W ⟶ Y
c : PushoutCocone f g
G : C ⥤ D
⊢ (Cocone.precompose (diagramIsoSpan (span f g ⋙ G)).symm.hom).obj (G.mapCocone c) ≅ c.map G

Tactic:
refine PushoutCocone.ext (Iso.refl _) ?_ ?_

Goal state after:
case refine_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
W X Y : C
f : W ⟶ X
g : W ⟶ Y
c : PushoutCocone f g
G : C ⥤ D
⊢ inl ((Cocone.precompose (diagramIsoSpan (span f g ⋙ G)).symm.hom).obj (G.mapCocone c)) ≫
      (Iso.refl ((Cocone.precompose (diagramIsoSpan (span f g ⋙ G)).symm.hom).obj (G.mapCocone c)).pt).hom =
    (c.map G).inl

case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
W X Y : C
f : W ⟶ X
g : W ⟶ Y
c : PushoutCocone f g
G : C ⥤ D
⊢ inr ((Cocone.precompose (diagramIsoSpan (span f g ⋙ G)).symm.hom).obj (G.mapCocone c)) ≫
      (Iso.refl ((Cocone.precompose (diagramIsoSpan (span f g ⋙ G)).symm.hom).obj (G.mapCocone c)).pt).hom =
    (c.map G).inr
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
F₁ F₂ : C ⥤ D
app : (X : C) → F₁.obj X ⟶ F₂.obj X
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
hf : F₁.map f ≫ app Y✝ = app X✝ ≫ F₂.map f
hg : F₁.map g ≫ app Z✝ = app Y✝ ≫ F₂.map g
⊢ (app X✝ ≫ F₂.map f) ≫ F₂.map g = app X✝ ≫ F₂.map f ≫ F₂.map g

Tactic:
Category.assoc

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F₁ F₂ : C ⥤ D
app : (X : C) → F₁.obj X ⟶ F₂.obj X
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
hf : F₁.map f ≫ app Y✝ = app X✝ ≫ F₂.map f
hg : F₁.map g ≫ app Z✝ = app Y✝ ≫ F₂.map g
⊢ app X✝ ≫ F₂.map f ≫ F₂.map g = app X✝ ≫ F₂.map f ≫ F₂.map g
Module: Mathlib.CategoryTheory.MorphismProperty.Composition

Goal state before:
pp: case of_comp
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
W : MorphismProperty C
X✝ Y✝ Z✝ : C
f✝ : X✝ ⟶ Y✝
x✝ y✝ z✝ : C
g' : x✝ ⟶ y✝
f : y✝ ⟶ z✝
hg' : W g'
hf : W.multiplicativeClosure' f
h_rec : ∀ (g : z✝ ⟶ Z✝), W.multiplicativeClosure' g → W.multiplicativeClosure' (f ≫ g)
g : z✝ ⟶ Z✝
hg : W.multiplicativeClosure' g
⊢ W.multiplicativeClosure' ((g' ≫ f) ≫ g)

Tactic:
Category.assoc

Goal state after:
case of_comp
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
W : MorphismProperty C
X✝ Y✝ Z✝ : C
f✝ : X✝ ⟶ Y✝
x✝ y✝ z✝ : C
g' : x✝ ⟶ y✝
f : y✝ ⟶ z✝
hg' : W g'
hf : W.multiplicativeClosure' f
h_rec : ∀ (g : z✝ ⟶ Z✝), W.multiplicativeClosure' g → W.multiplicativeClosure' (f ≫ g)
g : z✝ ⟶ Z✝
hg : W.multiplicativeClosure' g
⊢ W.multiplicativeClosure' (g' ≫ f ≫ g)
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : Cᵒᵖ
f : X ⟶ Y
g : X ⟶ Z
⊢ HasLimit (span f g).leftOp ↔ HasPushout f g

Tactic:
hasLimit_leftOp_iff_hasColimit

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : Cᵒᵖ
f : X ⟶ Y
g : X ⟶ Z
⊢ HasColimit (span f g) ↔ HasPushout f g
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✝ : C
⊢ (adj.homEquiv x✝ (𝟙_ D ⊗ F.obj x✝)) (λ_ (F.obj x✝)).inv =
    (adj.homEquiv x✝ (𝟙_ D ⊗ F.obj x✝))
      (F.map (λ_ x✝).inv ≫
        (adj.homEquiv (𝟙_ C ⊗ x✝) (F.obj (𝟙_ C) ⊗ F.obj x✝)).symm
            ((adj.unit.app (𝟙_ C) ⊗ₘ adj.unit.app x✝) ≫ μ G (F.obj (𝟙_ C)) (F.obj x✝)) ≫
          (adj.homEquiv (𝟙_ C) (𝟙_ D)).symm (ε G) ▷ F.obj x✝)

Tactic:
rw [Adjunction.homEquiv_naturality_left, Adjunction.homEquiv_naturality_right,
      Equiv.apply_symm_apply, assoc, ← μ_natural_left, ← tensorHom_id,
      tensorHom_comp_tensorHom_assoc]

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✝ : C
⊢ (adj.homEquiv x✝ (𝟙_ D ⊗ F.obj x✝)) (λ_ (F.obj x✝)).inv =
    (λ_ x✝).inv ≫
      (adj.unit.app (𝟙_ C) ≫ G.map ((adj.homEquiv (𝟙_ C) (𝟙_ D)).symm (ε G)) ⊗ₘ
          adj.unit.app x✝ ≫ 𝟙 (G.obj (F.obj x✝))) ≫
        μ G (𝟙_ D) (F.obj x✝)
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₁ ⊗ₘ g₁ ⊗ₘ f₂ ⊗ₘ g₂) ≫ (α_ Y₁ V₁ (Y₂ ⊗ V₂)).inv

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

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

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

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

Tactic:
rw [associator_inv_naturality]

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₁ U₁ (X₂ ⊗ U₂)).inv ≫ ((f₁ ⊗ₘ g₁) ⊗ₘ f₂ ⊗ₘ g₂)

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

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

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

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₁ ⊗ₘ (α_ U₁ X₂ U₂).hom
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
s t : ↑(Set.Ici c)
⊢ (∀ (x x_1 : M), (mapGen ⇑c.mk') (c.mk' x) (c.mk' x_1) → (mapGen ⇑c.mk') (c.mk' x) (c.mk' x_1)) ↔
    ∀ {x y : M}, ↑s x y → ↑t x y

Tactic:
mapGen_apply_apply_of_surjective c.mk' (c.ker_mk'_eq.trans_le s.2) c.mk'_surjective,

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
s t : ↑(Set.Ici c)
⊢ (∀ (x x_1 : M), ↑s x x_1 → (mapGen ⇑c.mk') (c.mk' x) (c.mk' x_1)) ↔ ∀ {x y : M}, ↑s x y → ↑t x y
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
⊢ x⁻¹⁻¹ = 1 * x⁻¹⁻¹

Tactic:
one_mul

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
⊢ x⁻¹⁻¹ = x⁻¹⁻¹
Module: Mathlib.Algebra.Category.CoalgCat.Basic

Goal state before:
pp: R : Type u
inst✝ : CommRing R
X Y : CoalgCat R
f : X ⟶ Y
x✝ : IsIso ((forget (CoalgCat R)).map f)
i : (forget (CoalgCat R)).obj X ≅ (forget (CoalgCat R)).obj Y := asIso ((forget (CoalgCat R)).map f)
e : ↑X.toModuleCat ≃ₗc[R] ↑Y.toModuleCat :=
  let __src := Hom.toCoalgHom f;
  let __src_1 := i.toEquiv;
  { toCoalgHom := __src, invFun := __src_1.invFun, left_inv := ⋯, right_inv := ⋯ }
⊢ IsIso f

Tactic:
exact ⟨e.toCoalgIso.isIso_hom.1⟩

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✝
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
r : R
s : ↑X
⊢ (ConcreteCategory.hom g) (1 ⊗ₜ[R] (r • s)) = (RingHom.id R) r • (ConcreteCategory.hom g) (1 ⊗ₜ[R] s)

Tactic:
by
      dsimp
      rw [RestrictScalars.smul_def, ← LinearMap.map_smul]
      erw [tmul_smul]
      congr

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

Goal state before:
pp: case refine_3.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
m1 : Module R S := Module.compHom S f
m2 : Module R ↑Y := Module.compHom (↑Y) f
s : S
⊢ (lift { toFun := fun s ↦ evalAt f s g, map_add' := ⋯, map_smul' := ⋯ }) (s • 0) =
    s • (lift { toFun := fun s ↦ evalAt f s g, map_add' := ⋯, map_smul' := ⋯ }) 0

Tactic:
rw [smul_zero, map_zero, smul_zero]

Goal state after:
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 : ModuleCat S
s : S
m1 : Module R S := Module.compHom S f
m2 : Module R ↑Y := Module.compHom (↑Y) f
⊢ (lift { toFun := fun s ↦ { toFun := fun y ↦ s • y, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯, map_smul' := ⋯ })
      (s • 0) =
    (RingHom.id S) s •
      (lift
          { toFun := fun s ↦ { toFun := fun y ↦ s • y, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯, map_smul' := ⋯ })
        0

Tactic:
rw [smul_zero, map_zero, smul_zero]

Goal state after:
Module: Mathlib.RingTheory.Coalgebra.TensorProduct

Goal state before:
pp: case e'_2.tmul.tmul
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : AddCommMonoid A
inst✝⁷ : AddCommMonoid B
inst✝⁶ : Algebra R S
inst✝⁵ : Module R A
inst✝⁴ : Module S A
inst✝³ : Module R B
inst✝² : IsScalarTower R S A
inst✝¹ : Coalgebra R B
inst✝ : Coalgebra S A
x : A
y : B
x₁ x₂ : A
y₁ y₂ : B
⊢ (counit y₁ • counit x₁) • x₂ ⊗ₜ[R] y₂ = 1 • (counit x₁ • x₂) ⊗ₜ[R] (counit y₁ • y₂)

Tactic:
tmul_smul,

Goal state after:
case e'_2.tmul.tmul
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : AddCommMonoid A
inst✝⁷ : AddCommMonoid B
inst✝⁶ : Algebra R S
inst✝⁵ : Module R A
inst✝⁴ : Module S A
inst✝³ : Module R B
inst✝² : IsScalarTower R S A
inst✝¹ : Coalgebra R B
inst✝ : Coalgebra S A
x : A
y : B
x₁ x₂ : A
y₁ y₂ : B
⊢ (counit y₁ • counit x₁) • x₂ ⊗ₜ[R] y₂ = 1 • counit y₁ • (counit x₁ • x₂) ⊗ₜ[R] y₂
Module: Mathlib.RingTheory.Coalgebra.TensorProduct

Goal state before:
pp: case e'_2.tmul.tmul
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : AddCommMonoid A
inst✝⁷ : AddCommMonoid B
inst✝⁶ : Algebra R S
inst✝⁵ : Module R A
inst✝⁴ : Module S A
inst✝³ : Module R B
inst✝² : IsScalarTower R S A
inst✝¹ : Coalgebra R B
inst✝ : Coalgebra S A
x : A
y : B
x₁ x₂ : A
y₁ y₂ : B
⊢ (counit y₂ • counit x₂) • x₁ ⊗ₜ[R] y₁ = 1 • (counit x₂ • x₁) ⊗ₜ[R] (counit y₂ • y₁)

Tactic:
tmul_smul,

Goal state after:
case e'_2.tmul.tmul
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : AddCommMonoid A
inst✝⁷ : AddCommMonoid B
inst✝⁶ : Algebra R S
inst✝⁵ : Module R A
inst✝⁴ : Module S A
inst✝³ : Module R B
inst✝² : IsScalarTower R S A
inst✝¹ : Coalgebra R B
inst✝ : Coalgebra S A
x : A
y : B
x₁ x₂ : A
y₁ y₂ : B
⊢ (counit y₂ • counit x₂) • x₁ ⊗ₜ[R] y₁ = 1 • counit y₂ • (counit x₂ • x₁) ⊗ₜ[R] y₁
Module: Mathlib.RingTheory.Coalgebra.TensorProduct

Goal state before:
pp: R✝ : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹³ : CommSemiring R✝
inst✝¹² : CommSemiring S
inst✝¹¹ : AddCommMonoid A
inst✝¹⁰ : AddCommMonoid B
inst✝⁹ : Algebra R✝ S
inst✝⁸ : Module R✝ A
inst✝⁷ : Module S A
inst✝⁶ : Module R✝ B
inst✝⁵ : IsScalarTower R✝ S A
R : Type u_5
C : Type u_6
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid C
inst✝² : Module R C
inst✝¹ : Coalgebra R C
inst✝ : IsCocomm R C
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
calc
        (μ ∘ₗ (ε ⊗ₘ ε)) ∘ₗ δ
    _ = (μ ∘ₗ ε ▷ R) ∘ₗ (C ◁ ε ∘ₗ δ) := by simp [coassoc_simps]
    _ = ε := by ext; simp

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : WfDvdMonoid α
a₀ x : α
h : a₀ ≠ 0
hx : ¬IsUnit x
⊢ 1 * a₀ = a₀

Tactic:
one_mul

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : WfDvdMonoid α
a₀ x : α
h : a₀ ≠ 0
hx : ¬IsUnit x
⊢ a₀ = a₀
Module: Mathlib.RingTheory.TwoSidedIdeal.Operations

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
z : R
⊢ z ∈ span (s ∪ s * univ ∪ univ * s ∪ univ * s * univ) ↔
    z ∈ AddSubgroup.closure (s ∪ s * univ ∪ univ * s ∪ univ * s * univ)

Tactic:
refine mem_span_iff_mem_addSubgroup_closure_absorbing ?_ ?_
    · rintro x y (((hy | ⟨y, hy, r, -, rfl⟩) | ⟨r, -, y, hy, rfl⟩) |
        ⟨-, ⟨r', -, y, hy, rfl⟩, r, -, rfl⟩)
      · exact .inl <| .inr <| ⟨x, mem_univ _, y, hy, rfl⟩
      · exact .inr <| ⟨x * y, ⟨x, mem_univ _, y, hy, rfl⟩, r, mem_univ _, mul_assoc ..⟩
      · exact .inl <| .inr <| ⟨x * r, mem_univ _, y, hy, mul_assoc ..⟩
      · refine .inr <| ⟨x * r' * y, ⟨x * r', mem_univ _, y, hy, ?_⟩, ⟨r, mem_univ _, ?_⟩⟩
        all_goals simp [mul_assoc]
    · rintro y x (((hy | ⟨y, hy, r, -, rfl⟩) | ⟨r, -, y, hy, rfl⟩) |
        ⟨-, ⟨r', -, y, hy, rfl⟩, r, -, rfl⟩)
      · exact .inl <| .inl <| .inr ⟨y, hy, x, mem_univ _, rfl⟩
      · exact .inl <| .inl <| .inr ⟨y, hy, r * x, mem_univ _, (mul_assoc ..).symm⟩
      · exact .inr <| ⟨r * y, ⟨r, mem_univ _, y, hy, rfl⟩, x, mem_univ _, rfl⟩
      · refine .inr <| ⟨r' * y, ⟨r', mem_univ _, y, hy, rfl⟩, r * x, mem_univ _, ?_⟩
        simp [mul_assoc]

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

Goal state before:
pp: case inr.inr
R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
n m : ℤ
hn : n < 0
hm : m < 0
⊢ mk' B 1 (Submonoid.pow x (n.natAbs + m.natAbs)) = mk' B (1 * 1) (Submonoid.pow x n.natAbs * Submonoid.pow x m.natAbs)

Tactic:
one_mul

Goal state after:
case inr.inr
R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
n m : ℤ
hn : n < 0
hm : m < 0
⊢ mk' B 1 (Submonoid.pow x (n.natAbs + m.natAbs)) = mk' B 1 (Submonoid.pow x n.natAbs * Submonoid.pow x m.natAbs)
Module: Mathlib.CategoryTheory.Monoidal.Mon

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

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

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

Tactic:
one_mul

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

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

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

Goal state before:
pp: case a
C : Type u₁
inst✝¹¹ : Category.{v₁, u₁} C
inst✝¹⁰ : MonoidalCategory C
M N O X✝ : C
inst✝⁹ : MonObj M
inst✝⁸ : MonObj N
inst✝⁷ : MonObj O
inst✝⁶ : BraidedCategory C
X Y Z W : C
inst✝⁵ : MonObj X
inst✝⁴ : MonObj Y
inst✝³ : MonObj Z
inst✝² : MonObj W
f : X ⟶ Y
g : Z ⟶ W
inst✝¹ : IsMonHom f
inst✝ : IsMonHom g
| η ≫ f ⊗ₘ η ≫ g

pp: case a
C : Type u₁
inst✝¹¹ : Category.{v₁, u₁} C
inst✝¹⁰ : MonoidalCategory C
M N O X✝ : C
inst✝⁹ : MonObj M
inst✝⁸ : MonObj N
inst✝⁷ : MonObj O
inst✝⁶ : BraidedCategory C
X Y Z W : C
inst✝⁵ : MonObj X
inst✝⁴ : MonObj Y
inst✝³ : MonObj Z
inst✝² : MonObj W
f : X ⟶ Y
g : Z ⟶ W
inst✝¹ : IsMonHom f
inst✝ : IsMonHom g
| (λ_ (𝟙_ C)).inv

Tactic:
one_hom,

Goal state after:
case a
C : Type u₁
inst✝¹¹ : Category.{v₁, u₁} C
inst✝¹⁰ : MonoidalCategory C
M N O X✝ : C
inst✝⁹ : MonObj M
inst✝⁸ : MonObj N
inst✝⁷ : MonObj O
inst✝⁶ : BraidedCategory C
X Y Z W : C
inst✝⁵ : MonObj X
inst✝⁴ : MonObj Y
inst✝³ : MonObj Z
inst✝² : MonObj W
f : X ⟶ Y
g : Z ⟶ W
inst✝¹ : IsMonHom f
inst✝ : IsMonHom g
| η ⊗ₘ η ≫ g

case a
C : Type u₁
inst✝¹¹ : Category.{v₁, u₁} C
inst✝¹⁰ : MonoidalCategory C
M N O X✝ : C
inst✝⁹ : MonObj M
inst✝⁸ : MonObj N
inst✝⁷ : MonObj O
inst✝⁶ : BraidedCategory C
X Y Z W : C
inst✝⁵ : MonObj X
inst✝⁴ : MonObj Y
inst✝³ : MonObj Z
inst✝² : MonObj W
f : X ⟶ Y
g : Z ⟶ W
inst✝¹ : IsMonHom f
inst✝ : IsMonHom g
| (λ_ (𝟙_ C)).inv
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X₃ Y₁ Y₂ Y₃ : C
g₁ : Y₁ ⟶ Y₂
g₂ : Y₂ ⟶ Y₃
i₃ : X₃ ⟶ Y₃
t₂ : PullbackCone g₂ i₃
i₂ : t₂.pt ⟶ Y₂
t₁ : PullbackCone g₁ i₂
hi₂ : i₂ = t₂.fst
H : IsLimit t₂
H' : IsLimit t₁
s : PullbackCone (g₁ ≫ g₂) i₃
⊢ (s.fst ≫ g₁) ≫ g₂ = s.fst ≫ g₁ ≫ g₂

Tactic:
Category.assoc

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X₃ Y₁ Y₂ Y₃ : C
g₁ : Y₁ ⟶ Y₂
g₂ : Y₂ ⟶ Y₃
i₃ : X₃ ⟶ Y₃
t₂ : PullbackCone g₂ i₃
i₂ : t₂.pt ⟶ Y₂
t₁ : PullbackCone g₁ i₂
hi₂ : i₂ = t₂.fst
H : IsLimit t₂
H' : IsLimit t₁
s : PullbackCone (g₁ ≫ g₂) i₃
⊢ s.fst ≫ g₁ ≫ g₂ = s.fst ≫ g₁ ≫ g₂
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
X₁₁ X₁₂ X₁₃ X₂₁ X₂₂ X₂₃ : C
h₁₂ : X₁₂ ⟶ X₁₃
h₂₁ : X₂₁ ⟶ X₂₂
h₂₂ : X₂₂ ⟶ X₂₃
h₁₃ : X₁₁ ⟶ X₁₃
v₁₁ : X₁₁ ⟶ X₂₁
v₁₂ : X₁₂ ⟶ X₂₂
v₁₃ : X₁₃ ⟶ X₂₃
s : IsPullback h₁₃ v₁₁ v₁₃ (h₂₁ ≫ h₂₂)
t : IsPullback h₁₂ v₁₂ v₁₃ h₂₂
⊢ v₁₁ ≫ h₂₁ ≫ h₂₂ = (v₁₁ ≫ h₂₁) ≫ h₂₂

Tactic:
Category.assoc

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
X₁₁ X₁₂ X₁₃ X₂₁ X₂₂ X₂₃ : C
h₁₂ : X₁₂ ⟶ X₁₃
h₂₁ : X₂₁ ⟶ X₂₂
h₂₂ : X₂₂ ⟶ X₂₃
h₁₃ : X₁₁ ⟶ X₁₃
v₁₁ : X₁₁ ⟶ X₂₁
v₁₂ : X₁₂ ⟶ X₂₂
v₁₃ : X₁₃ ⟶ X₂₃
s : IsPullback h₁₃ v₁₁ v₁₃ (h₂₁ ≫ h₂₂)
t : IsPullback h₁₂ v₁₂ v₁₃ h₂₂
⊢ v₁₁ ≫ h₂₁ ≫ h₂₂ = v₁₁ ≫ h₂₁ ≫ h₂₂
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_3
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
M' : Type u_4
inst✝⁴ : AddCommMonoid M'
inst✝³ : Module R M'
inst✝² : Module A M'
inst✝¹ : IsScalarTower R A M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
Q : Type (max u_3 u_4 u_2)
x✝³ : AddCommMonoid Q
x✝² : Module R Q
x✝¹ : Module A Q
x✝ : IsScalarTower R A Q
g : M →ₗ[R] Q
⊢ ∃! g', ↑R g' ∘ₗ f = g

Tactic:
obtain ⟨ℓ, rfl, h₂⟩ := IsLocalizedModule.is_universal S f g fun s ↦ by
      rw [← (Algebra.lsmul R (A := A) R Q).commutes]; exact (IsLocalization.map_units A s).map _

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_3
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
M' : Type u_4
inst✝⁴ : AddCommMonoid M'
inst✝³ : Module R M'
inst✝² : Module A M'
inst✝¹ : IsScalarTower R A M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
Q : Type (max u_3 u_4 u_2)
x✝³ : AddCommMonoid Q
x✝² : Module R Q
x✝¹ : Module A Q
x✝ : IsScalarTower R A Q
ℓ : M' →ₗ[R] Q
h₂ : ∀ (y : M' →ₗ[R] Q), (fun l ↦ l ∘ₗ f = ℓ ∘ₗ f) y → y = ℓ
⊢ ∃! g', ↑R g' ∘ₗ f = ℓ ∘ₗ f
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ X₃ Y₁ : C
f₁ : X₁ ⟶ X₂
f₂ : X₂ ⟶ X₃
i₁ : X₁ ⟶ Y₁
t₁ : PushoutCocone i₁ f₁
i₂ : X₂ ⟶ t₁.pt
t₂ : PushoutCocone «i₂» f₂
hi₂ : «i₂» = t₁.inr
H : IsColimit t₁
H' : IsColimit t₂
s : PushoutCocone i₁ (f₁ ≫ f₂)
⊢ (f₁ ≫ f₂) ≫ s.inr = f₁ ≫ f₂ ≫ s.inr

Tactic:
Category.assoc

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ X₃ Y₁ : C
f₁ : X₁ ⟶ X₂
f₂ : X₂ ⟶ X₃
i₁ : X₁ ⟶ Y₁
t₁ : PushoutCocone i₁ f₁
i₂ : X₂ ⟶ t₁.pt
t₂ : PushoutCocone «i₂» f₂
hi₂ : «i₂» = t₁.inr
H : IsColimit t₁
H' : IsColimit t₂
s : PushoutCocone i₁ (f₁ ≫ f₂)
⊢ f₁ ≫ f₂ ≫ s.inr = f₁ ≫ f₂ ≫ s.inr
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
X₁₁ X₁₂ X₂₁ X₂₂ X₃₁ X₃₂ : C
h₁₁ : X₁₁ ⟶ X₁₂
h₂₁ : X₂₁ ⟶ X₂₂
h₃₁ : X₃₁ ⟶ X₃₂
v₁₁ : X₁₁ ⟶ X₂₁
v₁₂ : X₁₂ ⟶ X₂₂
v₁₃ : X₁₂ ⟶ X₃₂
v₂₁ : X₂₁ ⟶ X₃₁
s : IsPushout h₁₁ (v₁₁ ≫ v₂₁) v₁₃ h₃₁
t : IsPushout h₁₁ v₁₁ v₁₂ h₂₁
⊢ (v₁₁ ≫ v₂₁) ≫ h₃₁ = v₁₁ ≫ v₂₁ ≫ h₃₁

Tactic:
Category.assoc

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
X₁₁ X₁₂ X₂₁ X₂₂ X₃₁ X₃₂ : C
h₁₁ : X₁₁ ⟶ X₁₂
h₂₁ : X₂₁ ⟶ X₂₂
h₃₁ : X₃₁ ⟶ X₃₂
v₁₁ : X₁₁ ⟶ X₂₁
v₁₂ : X₁₂ ⟶ X₂₂
v₁₃ : X₁₂ ⟶ X₃₂
v₂₁ : X₂₁ ⟶ X₃₁
s : IsPushout h₁₁ (v₁₁ ≫ v₂₁) v₁₃ h₃₁
t : IsPushout h₁₁ v₁₁ v₁₂ h₂₁
⊢ v₁₁ ≫ v₂₁ ≫ h₃₁ = v₁₁ ≫ v₂₁ ≫ h₃₁
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
inst✝¹ : Epi f
inst✝ : IsIso inr
sq : CommSq f g inl inr
⊢ IsColimit sq.cocone

Tactic:
by
      refine
        PushoutCocone.IsColimit.mk _ (fun s => inv inr ≫ s.inr) (fun s => ?_)
          (by simp) (by simp)
      simp only [← cancel_epi f, s.condition, sq.w_assoc, IsIso.hom_inv_id_assoc]

Goal state after: