mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Coalgebra.CoassocSimps

Goal state before:
pp: R : Type u_1
M : Type u_3
M' : Type u_6
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
⊢ ρ⁻¹ ∘ₗ f = f ⊗ₘ LinearMap.id ∘ₗ ρ⁻¹

Tactic:
by

Goal state after:
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
M N : Comon C
f : M.X ≅ N.X
f_counit : f.hom ≫ ε = ε
f_comul : f.hom ≫ Δ = Δ ≫ (f.hom ⊗ₘ f.hom)
this : IsComonHom f.hom
⊢ { hom := f.hom, isComonHom_hom := this } ≫ { hom := f.inv, isComonHom_hom := ⋯ } = 𝟙 M

Tactic:
by

Goal state after:
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
M N : Comon C
f : M.X ≅ N.X
f_counit : f.hom ≫ ε = ε
f_comul : f.hom ≫ Δ = Δ ≫ (f.hom ⊗ₘ f.hom)
this : IsComonHom f.hom
⊢ { hom := f.inv, isComonHom_hom := ⋯ } ≫ { hom := f.hom, isComonHom_hom := this } = 𝟙 N

Tactic:
by

Goal state after:
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 : Comon C
⊢ ε ≫ Δ = Δ ≫ (ε ⊗ₘ ε)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_3
N : Type u_4
M' : Type u_6
N' : Type u_7
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : AddCommMonoid M'
inst✝² : Module R M'
inst✝¹ : AddCommMonoid N'
inst✝ : Module R N'
f : M →ₗ[R] M'
g : N →ₗ[R] N'
⊢ β ∘ₗ f ⊗ₘ g = g ⊗ₘ f ∘ₗ β

Tactic:
by

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

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

Tactic:
by

Goal state after:
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 : Comon C
f : A ⟶ trivial C
⊢ f = { hom := ε, isComonHom_hom := ⋯ }

Tactic:
by

Goal state after:
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 : Comon C
⊢ ε.op ▷ op A.X ≫ Δ.op = (λ_ (op A.X)).hom

Tactic:
by

Goal state after:
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 : Comon C
⊢ op A.X ◁ ε.op ≫ Δ.op = (ρ_ (op A.X)).hom

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

Goal state after:
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 : Comon C
⊢ Δ.op ▷ op A.X ≫ Δ.op = (α_ (op A.X) (op A.X) (op A.X)).hom ≫ op A.X ◁ Δ.op ≫ Δ.op

Tactic:
by

Goal state after:
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
X✝ Y✝ : Comon C
f : X✝ ⟶ Y✝
⊢ η ≫ f.hom.op = η

Tactic:
by

Goal state after:
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
X✝ Y✝ : Comon C
f : X✝ ⟶ Y✝
⊢ μ ≫ f.hom.op = (f.hom.op ⊗ₘ f.hom.op) ≫ μ

Tactic:
by

Goal state after:
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 ≫ η.unop ▷ unop A.X = (λ_ (unop A.X)).inv

Tactic:
by

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

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

Tactic:
by

Goal state after:
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 ≫ unop A.X ◁ η.unop = (ρ_ (unop A.X)).inv

Tactic:
by

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

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

Tactic:
by

Goal state after:
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 ≫ unop A.X ◁ μ.unop = μ.unop ≫ μ.unop ▷ unop A.X ≫ (α_ (unop A.X) (unop A.X) (unop A.X)).hom

Tactic:
by

Goal state after:
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
X✝ Y✝ : (Mon Cᵒᵖ)ᵒᵖ
f : X✝ ⟶ Y✝
⊢ f.unop.hom.unop ≫ ε = ε

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_3
M' : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
inst✝ : Coalgebra R M
f : M →ₗ[R] M'
⊢ ε ⊗ₘ f ∘ₗ δ = LinearMap.id ⊗ₘ f ∘ₗ λ⁻¹

Tactic:
by

Goal state after:
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
X✝ Y✝ : (Mon Cᵒᵖ)ᵒᵖ
f : X✝ ⟶ Y✝
⊢ f.unop.hom.unop ≫ Δ = Δ ≫ (f.unop.hom.unop ⊗ₘ f.unop.hom.unop)

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : BraidedCategory C
A B : C
inst✝¹ : ComonObj A
inst✝ : ComonObj B
⊢ Δ = (Δ ⊗ₘ Δ) ≫ (tensorμ (op A) (op B) (op A) (op B)).unop

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : BraidedCategory C
A B : C
inst✝¹ : ComonObj A
inst✝ : ComonObj B
⊢ Δ = (Δ ⊗ₘ Δ) ≫ tensorμ A A B B

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_3
P : Type u_5
M' : Type u_6
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : AddCommMonoid P
inst✝³ : Module R P
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
inst✝ : Coalgebra R M
f : M →ₗ[R] M'
g : P →ₗ[R] M
⊢ ε ⊗ₘ f ∘ₗ δ ∘ₗ g = LinearMap.id ⊗ₘ f ∘ₗ λ⁻¹ ∘ₗ g

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_3
M' : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
inst✝ : Coalgebra R M
f : M →ₗ[R] M'
⊢ f ⊗ₘ ε ∘ₗ δ = f ⊗ₘ LinearMap.id ∘ₗ ρ⁻¹

Tactic:
by

Goal state after:
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
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : MonoidalCategory D
A : C
inst✝¹ : ComonObj A
F : C ⥤ D
inst✝ : F.OplaxMonoidal
⊢ (F.map Δ ≫ δ F A A) ≫ (F.map ε ≫ η F) ▷ F.obj A = (λ_ (F.obj A)).inv

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_3
P : Type u_5
M' : Type u_6
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : AddCommMonoid P
inst✝³ : Module R P
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
inst✝ : Coalgebra R M
f : M →ₗ[R] M'
g : P →ₗ[R] M
⊢ f ⊗ₘ ε ∘ₗ δ ∘ₗ g = f ⊗ₘ LinearMap.id ∘ₗ ρ⁻¹ ∘ₗ g

Tactic:
by

Goal state after:
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
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : MonoidalCategory D
A : C
inst✝¹ : ComonObj A
F : C ⥤ D
inst✝ : F.OplaxMonoidal
⊢ (F.map Δ ≫ δ F A A) ≫ F.obj A ◁ (F.map ε ≫ η F) = (ρ_ (F.obj A)).inv

Tactic:
by

Goal state after:
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:
by

Goal state after:
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
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : MonoidalCategory D
A : C
inst✝¹ : ComonObj A
F : C ⥤ D
inst✝ : F.OplaxMonoidal
⊢ (F.map Δ ≫ δ F A A) ≫ F.obj A ◁ (F.map Δ ≫ δ F A A) =
    (F.map Δ ≫ δ F A A) ≫ (F.map Δ ≫ δ F A A) ▷ F.obj A ≫ (α_ (F.obj A) (F.obj A) (F.obj A)).hom

Tactic:
by

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

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

Tactic:
by

Goal state after:
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
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
F : C ⥤ D
inst✝³ : F.OplaxMonoidal
X Y : C
inst✝² : ComonObj X
inst✝¹ : ComonObj Y
f : X ⟶ Y
inst✝ : IsComonHom f
⊢ F.map f ≫ ε = ε

Tactic:
by

Goal state after:
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
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
F : C ⥤ D
inst✝³ : F.OplaxMonoidal
X Y : C
inst✝² : ComonObj X
inst✝¹ : ComonObj Y
f : X ⟶ Y
inst✝ : IsComonHom f
⊢ F.map f ≫ Δ = Δ ≫ (F.map f ⊗ₘ F.map f)

Tactic:
by

Goal state after:
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
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : C ⥤ D
inst✝ : F.OplaxMonoidal
A : Comon C
⊢ { hom := F.map (𝟙 A).hom, isComonHom_hom := ⋯ } = 𝟙 { X := F.obj A.X, comon := obj.instComonObj A.X F }

Tactic:
by

Goal state after:
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
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : C ⥤ D
inst✝ : F.OplaxMonoidal
X✝ Y✝ Z✝ : Comon C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ { hom := F.map (f ≫ g).hom, isComonHom_hom := ⋯ } =
    { hom := F.map f.hom, isComonHom_hom := ⋯ } ≫ { hom := F.map g.hom, isComonHom_hom := ⋯ }

Tactic:
by

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

Goal state before:
pp: x✝¹ : Type u
x✝ : CommRingCat
⊢ Function.RightInverse (fun f ↦ ofHom (homEquiv.symm ⇑(ConcreteCategory.hom f))) fun f ↦ ↾homEquiv (Hom.hom f)

Tactic:
by

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

Goal state before:
pp: n : Type v
inst✝ : Unique n
X✝ Y✝ : CommRingCat
f : X✝ ⟶ Y✝
⊢ (coyoneda.obj (op n)).map f ≫ (RingEquiv.piUnique fun i ↦ ↑Y✝).toCommRingCatIso.hom =
    (RingEquiv.piUnique fun i ↦ ↑X✝).toCommRingCatIso.hom ≫ (𝟭 CommRingCat).map f

Tactic:
by

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

Goal state before:
pp: R : CommRingCat
X✝ Y✝ Z✝ : CommMonCat
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ Under.homMk (ofHom (MonoidAlgebra.mapDomainRingHom (↑R) (CommMonCat.Hom.hom (f ≫ g)))) ⋯ =
    Under.homMk (ofHom (MonoidAlgebra.mapDomainRingHom (↑R) (CommMonCat.Hom.hom f))) ⋯ ≫
      Under.homMk (ofHom (MonoidAlgebra.mapDomainRingHom (↑R) (CommMonCat.Hom.hom g))) ⋯

Tactic:
by

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

Goal state before:
pp: R : CommRingCat
S : Under R
⊢ (((Under.forget R ⋙ forget₂ CommRingCat CommMonCat) ⋙ R.monoidAlgebra).obj S).hom ≫
      ofHom
        (MonoidAlgebra.liftNCRingHom (Hom.hom S.hom)
          (MonoidHom.id ↑((Under.forget R ⋙ forget₂ CommRingCat CommMonCat).obj S)) ⋯) =
    ((𝟭 (Under R)).obj S).hom

Tactic:
ext; simp [MonoidAlgebra.liftNCRingHom]

Goal state after:
Module: Mathlib.GroupTheory.MonoidLocalization.Away

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
g : M →* P
hg : ∀ (y : ↥S), IsUnit (g ↑y)
x : M
F : AwayMap x N
y : M
G : AwayMap (x * y) P
⊢ G x * mk' G y ⟨x * y, ⋯⟩ = 1

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.MonoidLocalization.Away

Goal state before:
pp: M : Type u_1
inst✝⁵ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝⁴ : CommMonoid N
P : Type u_3
inst✝³ : CommMonoid P
A : Type u_4
inst✝² : AddCommMonoid A
x : A
B : Type u_5
inst✝¹ : AddCommMonoid B
F : AwayMap x B
C : Type u_6
inst✝ : AddCommMonoid C
g : A →+ C
y : A
G : AwayMap (x + y) C
⊢ G x + mk' G y ⟨x + y, ⋯⟩ = 0

Tactic:
by

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

Goal state before:
pp: R : CommRingCat
S : Under R
⊢ (((Under.forget R ⋙ forget₂ CommRingCat CommMonCat) ⋙ R.monoidAlgebra).obj S).hom ≫
      ofHom
        (MonoidAlgebra.liftNCRingHom (Hom.hom S.hom)
          (MonoidHom.id ↑((Under.forget R ⋙ forget₂ CommRingCat CommMonCat).obj S)) ⋯) =
    ((𝟭 (Under R)).obj S).hom

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.MonoidLocalization.Away

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
x : M
⊢ mk = Submonoid.LocalizationMap.mk' (monoidOf x)

Tactic:
by

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
⊢ x ^ 0 * a₀ = a₀

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : WfDvdMonoid α
x : α
hx : ¬IsUnit x
n : ℕ
d : α
h : x ^ n * (x * d) ≠ 0
hm : ∀ x_1 ∈ {a | ∃ n_1, x ^ n_1 * a = x ^ n * (x * d)}, ¬DvdNotUnit x_1 (x * d)
⊢ x ^ (n + 1) * d = x ^ n * (x * d)

Tactic:
by

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
⊢ ∃ n a, ¬x ∣ a ∧ a₀ = x ^ n * a

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : IsCancelMulZero α
inst✝ : WfDvdMonoid α
a : α
ha : ¬IsUnit a
n : ℕ
c : α
ndvd : ¬a ∣ c
hb : a ^ n * c ≠ 0
⊢ ¬a ^ (n + 1) ∣ a ^ n * c

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : IsCancelMulZero α
inst✝ : WfDvdMonoid α
a b : α
ha : ¬IsUnit a
hb : b ≠ 0
⊢ FiniteMultiplicity a b

Tactic:
by

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

Goal state before:
pp: R : CommRingCat
S T : Under R
f : S ⟶ T
⊢ ((Under.forget R ⋙ forget₂ CommRingCat CommMonCat) ⋙ R.monoidAlgebra).map f ≫
      Under.homMk
        (ofHom
          (MonoidAlgebra.liftNCRingHom (Hom.hom T.hom)
            (MonoidHom.id ↑((Under.forget R ⋙ forget₂ CommRingCat CommMonCat).obj T)) ⋯))
        ⋯ =
    Under.homMk
        (ofHom
          (MonoidAlgebra.liftNCRingHom (Hom.hom S.hom)
            (MonoidHom.id ↑((Under.forget R ⋙ forget₂ CommRingCat CommMonCat).obj S)) ⋯))
        ⋯ ≫
      (𝟭 (Under R)).map f

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.CoalgCat.ComonEquivalence

Goal state before:
pp: R : Type u
inst✝ : CommRing R
X : CoalgCat R
⊢ ModuleCat.Hom.hom
      (ModuleCat.ofHom CoalgebraStruct.comul ≫ ModuleCat.ofHom CoalgebraStruct.counit ▷ ModuleCat.of R ↑X.toModuleCat) =
    ModuleCat.Hom.hom (λ_ (ModuleCat.of R ↑X.toModuleCat)).inv

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.CoalgCat.ComonEquivalence

Goal state before:
pp: R : Type u
inst✝ : CommRing R
X : CoalgCat R
⊢ ModuleCat.Hom.hom
      (ModuleCat.ofHom CoalgebraStruct.comul ≫ ModuleCat.of R ↑X.toModuleCat ◁ ModuleCat.ofHom CoalgebraStruct.counit) =
    ModuleCat.Hom.hom (ρ_ (ModuleCat.of R ↑X.toModuleCat)).inv

Tactic:
by

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

Goal state before:
pp: R : Type u_2
inst✝² : CommMonoidWithZero R
inst✝¹ : UniqueFactorizationMonoid R
inst✝ : NormalizationMonoid R
a b : R
n : ℕ
ha : Irreducible a
hb : b ≠ 0
⊢ ↑n ≤ emultiplicity a b ↔ replicate n (normalize a) ≤ normalizedFactors b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.CoalgCat.ComonEquivalence

Goal state before:
pp: R : Type u
inst✝ : CommRing R
X : CoalgCat R
⊢ ModuleCat.Hom.hom
      (ModuleCat.ofHom CoalgebraStruct.comul ≫ ModuleCat.of R ↑X.toModuleCat ◁ ModuleCat.ofHom CoalgebraStruct.comul) =
    ModuleCat.Hom.hom
      (ModuleCat.ofHom CoalgebraStruct.comul ≫
        ModuleCat.ofHom CoalgebraStruct.comul ▷ ModuleCat.of R ↑X.toModuleCat ≫
          (α_ (ModuleCat.of R ↑X.toModuleCat) (ModuleCat.of R ↑X.toModuleCat) (ModuleCat.of R ↑X.toModuleCat)).hom)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.CoalgCat.ComonEquivalence

Goal state before:
pp: R : Type u
inst✝ : CommRing R
X✝ Y✝ : CoalgCat R
x✝ : X✝ ⟶ Y✝
⊢ (𝟭 (CoalgCat R)).map x✝ ≫ (Iso.refl ((𝟭 (CoalgCat R)).obj Y✝)).hom =
    (Iso.refl ((𝟭 (CoalgCat R)).obj X✝)).hom ≫ (toComon R ⋙ ofComon R).map x✝

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.CoalgCat.ComonEquivalence

Goal state before:
pp: R : Type u
inst✝ : CommRing R
X✝ Y✝ : Comon (ModuleCat R)
x✝ : X✝ ⟶ Y✝
⊢ (ofComon R ⋙ toComon R).map x✝ ≫ (Iso.refl ((ofComon R ⋙ toComon R).obj Y✝)).hom =
    (Iso.refl ((ofComon R ⋙ toComon R).obj X✝)).hom ≫ (𝟭 (Comon (ModuleCat R))).map x✝

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.CoalgCat.ComonEquivalence

Goal state before:
pp: R : Type u
inst✝ : CommRing R
K L : CoalgCat R
⊢ CoalgebraStruct.comul =
    ↑(TensorProduct.tensorTensorTensorComm R ↑K.toModuleCat ↑K.toModuleCat ↑L.toModuleCat ↑L.toModuleCat) ∘ₗ
      TensorProduct.map CoalgebraStruct.comul CoalgebraStruct.comul

Tactic:
by

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

Goal state before:
pp: R : Type u_2
inst✝³ : CommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
a b : R
ha : Irreducible a
hb : b ≠ 0
⊢ emultiplicity a b = ↑(count (normalize a) (normalizedFactors b))

Tactic:
by

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

Goal state before:
pp: R : Type u_2
inst✝³ : CommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
a b : R
ha : Irreducible a
hb : b ≠ 0
⊢ multiplicity a b = count (normalize a) (normalizedFactors b)

Tactic:
have := emultiplicity_eq_count_normalizedFactors ha hb

Goal state after:
R : Type u_2
inst✝³ : CommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
a b : R
ha : Irreducible a
hb : b ≠ 0
this : emultiplicity a b = ↑(count (normalize a) (normalizedFactors b))
⊢ multiplicity a b = count (normalize a) (normalizedFactors b)
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity

Goal state before:
pp: R : Type u_2
inst✝³ : CommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
a b : R
ha : Irreducible a
hb : b ≠ 0
⊢ multiplicity a b = count (normalize a) (normalizedFactors b)

Tactic:
by

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

Goal state before:
pp: case e'_3
R : Type u_2
inst✝³ : CommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
p x : R
hp : Irreducible p
hnorm : normalize p = p
n : ℕ
hle : p ^ n ∣ x
hlt : ¬p ^ (n + 1) ∣ x
hx0 : ¬x = 0
⊢ ↑n = emultiplicity p x

Tactic:
exact (emultiplicity_eq_coe.mpr ⟨hle, hlt⟩).symm

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

Goal state before:
pp: R : Type u_2
inst✝³ : CommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
p x : R
hp : Irreducible p
hnorm : normalize p = p
n : ℕ
hle : p ^ n ∣ x
hlt : ¬p ^ (n + 1) ∣ x
⊢ count p (normalizedFactors x) = n

Tactic:
by

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

Goal state before:
pp: R : CommRingCat
G : CommMonCat
⊢ R.monoidAlgebra.map ({ app := fun G ↦ CommMonCat.ofHom (MonoidAlgebra.of ↑R ↑G), naturality := ⋯ }.app G) ≫
      {
            app := fun S ↦
              Under.homMk
                (ofHom
                  (MonoidAlgebra.liftNCRingHom (Hom.hom S.hom)
                    (MonoidHom.id ↑((Under.forget R ⋙ forget₂ CommRingCat CommMonCat).obj S)) ⋯))
                ⋯,
            naturality := ⋯ }.app
        (R.monoidAlgebra.obj G) =
    𝟙 (R.monoidAlgebra.obj G)

Tactic:
by

Goal state after: