mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Category.BddLat

Goal state before:
pp: α β : BddLat
e : ↑α.toLat ≃o ↑β.toLat
⊢ ofHom
        (let __src := { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯ };
        { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ }) ≫
      ofHom
        (let __src := { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯ };
        { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ }) =
    𝟙 β

Tactic:
ext

Goal state after:
α β : BddLat
e : ↑α.toLat ≃o ↑β.toLat
a✝ : ↑β.toLat
⊢ (Hom.hom
        (ofHom
            (let __src := { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯ };
            { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ }) ≫
          ofHom
            (let __src := { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯ };
            { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ })))
      a✝ =
    (Hom.hom (𝟙 β)) a✝
Module: Mathlib.Order.Category.HeytAlg

Goal state before:
pp: α β : HeytAlg
e : ↑α ≃o ↑β
⊢ ofHom { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯, map_bot' := ⋯, map_himp' := ⋯ } ≫
      ofHom { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯, map_bot' := ⋯, map_himp' := ⋯ } =
    𝟙 α

Tactic:
ext

Goal state after:
α β : HeytAlg
e : ↑α ≃o ↑β
a✝ : ↑α
⊢ (Hom.hom
        (ofHom { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯, map_bot' := ⋯, map_himp' := ⋯ } ≫
          ofHom { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯, map_bot' := ⋯, map_himp' := ⋯ }))
      a✝ =
    (Hom.hom (𝟙 α)) a✝
Module: Mathlib.Order.Category.HeytAlg

Goal state before:
pp: α β : HeytAlg
e : ↑α ≃o ↑β
⊢ ofHom { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯, map_bot' := ⋯, map_himp' := ⋯ } ≫
      ofHom { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯, map_bot' := ⋯, map_himp' := ⋯ } =
    𝟙 β

Tactic:
ext

Goal state after:
α β : HeytAlg
e : ↑α ≃o ↑β
a✝ : ↑β
⊢ (Hom.hom
        (ofHom { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯, map_bot' := ⋯, map_himp' := ⋯ } ≫
          ofHom { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯, map_bot' := ⋯, map_himp' := ⋯ }))
      a✝ =
    (Hom.hom (𝟙 β)) a✝
Module: Mathlib.Algebra.Category.BoolRing

Goal state before:
pp: α β : BoolRing
e : ↑α ≃+* ↑β
⊢ { hom' := ↑e } ≫ { hom' := ↑e.symm } = 𝟙 α

Tactic:
ext

Goal state after:
α β : BoolRing
e : ↑α ≃+* ↑β
x✝ : ↑α
⊢ (Hom.hom ({ hom' := ↑e } ≫ { hom' := ↑e.symm })) x✝ = (Hom.hom (𝟙 α)) x✝
Module: Mathlib.Algebra.Category.BoolRing

Goal state before:
pp: α β : BoolRing
e : ↑α ≃+* ↑β
⊢ { hom' := ↑e.symm } ≫ { hom' := ↑e } = 𝟙 β

Tactic:
ext

Goal state after:
α β : BoolRing
e : ↑α ≃+* ↑β
x✝ : ↑β
⊢ (Hom.hom ({ hom' := ↑e.symm } ≫ { hom' := ↑e })) x✝ = (Hom.hom (𝟙 β)) x✝
Module: Mathlib.RingTheory.Coalgebra.CoassocSimps

Goal state before:
pp: R : Type u_1
M : Type u_3
M₁ : Type u_11
M₂ : Type u_12
M₃ : Type u_13
N₁ : Type u_14
N₂ : Type u_15
N₃ : Type u_16
inst✝¹⁴ : CommSemiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : Module R M
inst✝¹¹ : AddCommMonoid M₁
inst✝¹⁰ : AddCommMonoid M₂
inst✝⁹ : AddCommMonoid M₃
inst✝⁸ : AddCommMonoid N₁
inst✝⁷ : AddCommMonoid N₂
inst✝⁶ : AddCommMonoid N₃
inst✝⁵ : Module R M₁
inst✝⁴ : Module R M₂
inst✝³ : Module R M₃
inst✝² : Module R N₁
inst✝¹ : Module R N₂
inst✝ : Module R N₃
f₁ : M₁ →ₗ[R] N₁
f₂ : M₂ →ₗ[R] N₂
f₃ : M₃ →ₗ[R] N₃
f₁₂ : M →ₗ[R] M₁ ⊗[R] M₂
⊢ α ∘ₗ (f₁ ⊗ₘ f₂ ∘ₗ f₁₂) ⊗ₘ f₃ = (α ∘ₗ (f₁ ⊗ₘ f₂) ⊗ₘ f₃) ∘ₗ f₁₂ ⊗ₘ LinearMap.id

Tactic:
ext

Goal state after:
R : Type u_1
M : Type u_3
M₁ : Type u_11
M₂ : Type u_12
M₃ : Type u_13
N₁ : Type u_14
N₂ : Type u_15
N₃ : Type u_16
inst✝¹⁴ : CommSemiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : Module R M
inst✝¹¹ : AddCommMonoid M₁
inst✝¹⁰ : AddCommMonoid M₂
inst✝⁹ : AddCommMonoid M₃
inst✝⁸ : AddCommMonoid N₁
inst✝⁷ : AddCommMonoid N₂
inst✝⁶ : AddCommMonoid N₃
inst✝⁵ : Module R M₁
inst✝⁴ : Module R M₂
inst✝³ : Module R M₃
inst✝² : Module R N₁
inst✝¹ : Module R N₂
inst✝ : Module R N₃
f₁ : M₁ →ₗ[R] N₁
f₂ : M₂ →ₗ[R] N₂
f₃ : M₃ →ₗ[R] N₃
f₁₂ : M →ₗ[R] M₁ ⊗[R] M₂
x✝¹ : M
x✝ : M₃
⊢ ((AlgebraTensorModule.curry (α ∘ₗ (f₁ ⊗ₘ f₂ ∘ₗ f₁₂) ⊗ₘ f₃)) x✝¹) x✝ =
    ((AlgebraTensorModule.curry ((α ∘ₗ (f₁ ⊗ₘ f₂) ⊗ₘ f₃) ∘ₗ f₁₂ ⊗ₘ LinearMap.id)) x✝¹) x✝
Module: Mathlib.RingTheory.Coalgebra.CoassocSimps

Goal state before:
pp: R : Type u_1
M : Type u_3
M₁ : Type u_11
M₂ : Type u_12
M₃ : Type u_13
N₁ : Type u_14
N₂ : Type u_15
N₃ : Type u_16
inst✝¹⁴ : CommSemiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : Module R M
inst✝¹¹ : AddCommMonoid M₁
inst✝¹⁰ : AddCommMonoid M₂
inst✝⁹ : AddCommMonoid M₃
inst✝⁸ : AddCommMonoid N₁
inst✝⁷ : AddCommMonoid N₂
inst✝⁶ : AddCommMonoid N₃
inst✝⁵ : Module R M₁
inst✝⁴ : Module R M₂
inst✝³ : Module R M₃
inst✝² : Module R N₁
inst✝¹ : Module R N₂
inst✝ : Module R N₃
f₁ : M₁ →ₗ[R] N₁
f₂ : M₂ →ₗ[R] N₂
f₃ : M₃ →ₗ[R] N₃
f₂₃ : M →ₗ[R] M₂ ⊗[R] M₃
⊢ α⁻¹ ∘ₗ f₁ ⊗ₘ (f₂ ⊗ₘ f₃ ∘ₗ f₂₃) = (α⁻¹ ∘ₗ f₁ ⊗ₘ (f₂ ⊗ₘ f₃)) ∘ₗ LinearMap.id ⊗ₘ f₂₃

Tactic:
ext

Goal state after:
R : Type u_1
M : Type u_3
M₁ : Type u_11
M₂ : Type u_12
M₃ : Type u_13
N₁ : Type u_14
N₂ : Type u_15
N₃ : Type u_16
inst✝¹⁴ : CommSemiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : Module R M
inst✝¹¹ : AddCommMonoid M₁
inst✝¹⁰ : AddCommMonoid M₂
inst✝⁹ : AddCommMonoid M₃
inst✝⁸ : AddCommMonoid N₁
inst✝⁷ : AddCommMonoid N₂
inst✝⁶ : AddCommMonoid N₃
inst✝⁵ : Module R M₁
inst✝⁴ : Module R M₂
inst✝³ : Module R M₃
inst✝² : Module R N₁
inst✝¹ : Module R N₂
inst✝ : Module R N₃
f₁ : M₁ →ₗ[R] N₁
f₂ : M₂ →ₗ[R] N₂
f₃ : M₃ →ₗ[R] N₃
f₂₃ : M →ₗ[R] M₂ ⊗[R] M₃
x✝¹ : M₁
x✝ : M
⊢ ((AlgebraTensorModule.curry (α⁻¹ ∘ₗ f₁ ⊗ₘ (f₂ ⊗ₘ f₃ ∘ₗ f₂₃))) x✝¹) x✝ =
    ((AlgebraTensorModule.curry ((α⁻¹ ∘ₗ f₁ ⊗ₘ (f₂ ⊗ₘ f₃)) ∘ₗ LinearMap.id ⊗ₘ f₂₃)) x✝¹) x✝
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'
f : M →ₗ[R] M'
⊢ α⁻¹ ∘ₗ f ⊗ₘ λ⁻¹ = (f ⊗ₘ LinearMap.id ∘ₗ ρ⁻¹) ⊗ₘ LinearMap.id

Tactic:
ext

Goal state after:
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'
f : M →ₗ[R] M'
x✝¹ : M
x✝ : N
⊢ ((AlgebraTensorModule.curry (α⁻¹ ∘ₗ f ⊗ₘ λ⁻¹)) x✝¹) x✝ =
    ((AlgebraTensorModule.curry ((f ⊗ₘ LinearMap.id ∘ₗ ρ⁻¹) ⊗ₘ LinearMap.id)) x✝¹) x✝
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'
f : M →ₗ[R] M'
⊢ α⁻¹ ∘ₗ f ⊗ₘ ρ⁻¹ = (f ⊗ₘ LinearMap.id) ⊗ₘ LinearMap.id ∘ₗ ρ⁻¹

Tactic:
ext

Goal state after:
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'
f : M →ₗ[R] M'
x✝¹ : M
x✝ : N
⊢ ((AlgebraTensorModule.curry (α⁻¹ ∘ₗ f ⊗ₘ ρ⁻¹)) x✝¹) x✝ =
    ((AlgebraTensorModule.curry ((f ⊗ₘ LinearMap.id) ⊗ₘ LinearMap.id ∘ₗ ρ⁻¹)) x✝¹) x✝
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
⊢ α ∘ₗ ρ⁻¹ = LinearMap.id ⊗ₘ ρ⁻¹

Tactic:
ext

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
x✝¹ : M
x✝ : N
⊢ ((AlgebraTensorModule.curry (α ∘ₗ ρ⁻¹)) x✝¹) x✝ = ((AlgebraTensorModule.curry (LinearMap.id ⊗ₘ ρ⁻¹)) x✝¹) x✝
Module: Mathlib.RingTheory.Coalgebra.CoassocSimps

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

Tactic:
ext

Goal state after:
R : Type u_1
M : Type u_3
N : Type u_4
N' : Type u_7
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid N'
inst✝ : Module R N'
f : N →ₗ[R] N'
x✝¹ : M
x✝ : N
⊢ ((AlgebraTensorModule.curry (α ∘ₗ λ⁻¹ ⊗ₘ f)) x✝¹) x✝ =
    ((AlgebraTensorModule.curry (LinearMap.id ⊗ₘ (LinearMap.id ⊗ₘ f) ∘ₗ λ⁻¹)) x✝¹) x✝
Module: Mathlib.RingTheory.Coalgebra.CoassocSimps

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

Tactic:
ext

Goal state after:
R : Type u_1
M : Type u_3
N : Type u_4
N' : Type u_7
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid N'
inst✝ : Module R N'
f : N →ₗ[R] N'
x✝¹ : M
x✝ : N
⊢ ((AlgebraTensorModule.curry (α ∘ₗ ρ⁻¹ ⊗ₘ f)) x✝¹) x✝ =
    ((AlgebraTensorModule.curry (LinearMap.id ⊗ₘ (LinearMap.id ⊗ₘ f ∘ₗ λ⁻¹))) x✝¹) x✝
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'
f : M →ₗ[R] R
g : N →ₗ[R] M'
⊢ λ ∘ₗ f ⊗ₘ g = g ∘ₗ λ ∘ₗ f ⊗ₘ LinearMap.id

Tactic:
ext

Goal state after:
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'
f : M →ₗ[R] R
g : N →ₗ[R] M'
x✝¹ : M
x✝ : N
⊢ ((AlgebraTensorModule.curry (λ ∘ₗ f ⊗ₘ g)) x✝¹) x✝ =
    ((AlgebraTensorModule.curry (g ∘ₗ λ ∘ₗ f ⊗ₘ LinearMap.id)) x✝¹) x✝
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'
f : M →ₗ[R] M'
g : N →ₗ[R] R
⊢ ρ ∘ₗ f ⊗ₘ g = f ∘ₗ ρ ∘ₗ LinearMap.id ⊗ₘ g

Tactic:
ext

Goal state after:
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'
f : M →ₗ[R] M'
g : N →ₗ[R] R
x✝¹ : M
x✝ : N
⊢ ((AlgebraTensorModule.curry (ρ ∘ₗ f ⊗ₘ g)) x✝¹) x✝ =
    ((AlgebraTensorModule.curry (f ∘ₗ ρ ∘ₗ LinearMap.id ⊗ₘ g)) x✝¹) x✝
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 = LinearMap.id ⊗ₘ f ∘ₗ λ⁻¹

Tactic:
ext

Goal state after:
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'
x✝ : M
⊢ (λ⁻¹ ∘ₗ f) x✝ = (LinearMap.id ⊗ₘ f ∘ₗ λ⁻¹) x✝
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:
ext

Goal state after:
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'
x✝ : M
⊢ (ρ⁻¹ ∘ₗ f) x✝ = (f ⊗ₘ LinearMap.id ∘ₗ ρ⁻¹) x✝
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:
ext

Goal state after:
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'
x✝¹ : M
x✝ : N
⊢ ((AlgebraTensorModule.curry (β ∘ₗ f ⊗ₘ g)) x✝¹) x✝ = ((AlgebraTensorModule.curry (g ⊗ₘ f ∘ₗ β)) x✝¹) 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 : Comon C
f : A ⟶ trivial C
⊢ f = { hom := ε, isComonHom_hom := ⋯ }

Tactic:
ext

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 : Comon C
f : A ⟶ trivial C
⊢ f.hom = { hom := ε, isComonHom_hom := ⋯ }.hom
Module: Mathlib.RingTheory.Coalgebra.CoassocSimps

Goal state before:
pp: case e_f.e_f
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.lTensor M (LinearMap.lTensor M (f ∘ₗ LinearMap.id) ∘ₗ β) ∘ₗ α) ∘ₗ β) ∘ₗ α

Tactic:
ext

Goal state after:
case e_f.e_f
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
x✝² x✝¹ x✝ : M
⊢ (((AlgebraTensorModule.curry (AlgebraTensorModule.curry (α ∘ₗ β ⊗ₘ f))) x✝²) x✝¹) x✝ =
    (((AlgebraTensorModule.curry
            (AlgebraTensorModule.curry
              (((LinearMap.lTensor M (LinearMap.lTensor M (f ∘ₗ LinearMap.id) ∘ₗ β) ∘ₗ α) ∘ₗ β) ∘ₗ α)))
          x✝²)
        x✝¹)
      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
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:
ext

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
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 := ⋯ }.hom = (𝟙 { X := F.obj A.X, comon := obj.instComonObj A.X F }).hom
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:
ext

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
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 =
    ({ hom := F.map f.hom, isComonHom_hom := ⋯ } ≫ { hom := F.map g.hom, isComonHom_hom := ⋯ }).hom
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:
ext

Goal state after:
n : Type v
inst✝ : Unique n
X✝ Y✝ : CommRingCat
f : X✝ ⟶ Y✝
x✝ : ↑((coyoneda.obj (op n)).obj X✝)
⊢ (Hom.hom ((coyoneda.obj (op n)).map f ≫ (RingEquiv.piUnique fun i ↦ ↑Y✝).toCommRingCatIso.hom)) x✝ =
    (Hom.hom ((RingEquiv.piUnique fun i ↦ ↑X✝).toCommRingCatIso.hom ≫ (𝟭 CommRingCat).map f)) x✝
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

Goal state after:
R : CommRingCat
S : Under R
x✝ : ↑R
⊢ (Hom.hom
        ((((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)) ⋯)))
      x✝ =
    (Hom.hom ((𝟭 (Under R)).obj S).hom) x✝
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity

Goal state before:
pp: case succ
R : Type u_2
inst✝² : CommMonoidWithZero R
inst✝¹ : UniqueFactorizationMonoid R
inst✝ : NormalizationMonoid R
a : R
ha : Irreducible a
n : ℕ
ih : ∀ {b : R}, b ≠ 0 → (a ^ n ∣ b ↔ replicate n (normalize a) ≤ normalizedFactors b)
b : R
hb : b ≠ 0
⊢ a ^ (n + 1) ∣ b ↔ replicate (n + 1) (normalize a) ≤ normalizedFactors b

Tactic:
constructor

Goal state after:
case succ.mp
R : Type u_2
inst✝² : CommMonoidWithZero R
inst✝¹ : UniqueFactorizationMonoid R
inst✝ : NormalizationMonoid R
a : R
ha : Irreducible a
n : ℕ
ih : ∀ {b : R}, b ≠ 0 → (a ^ n ∣ b ↔ replicate n (normalize a) ≤ normalizedFactors b)
b : R
hb : b ≠ 0
⊢ a ^ (n + 1) ∣ b → replicate (n + 1) (normalize a) ≤ normalizedFactors b

case succ.mpr
R : Type u_2
inst✝² : CommMonoidWithZero R
inst✝¹ : UniqueFactorizationMonoid R
inst✝ : NormalizationMonoid R
a : R
ha : Irreducible a
n : ℕ
ih : ∀ {b : R}, b ≠ 0 → (a ^ n ∣ b ↔ replicate n (normalize a) ≤ normalizedFactors b)
b : R
hb : b ≠ 0
⊢ replicate (n + 1) (normalize a) ≤ normalizedFactors b → a ^ (n + 1) ∣ b
Module: Mathlib.Algebra.Category.Ring.Adjunctions

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

Tactic:
ext

Goal state after:
R : CommRingCat
S : Under R
x✝ : ↑((forget₂ CommRingCat CommMonCat).obj S.right)
⊢ (CommMonCat.Hom.hom
        (CommMonCat.ofHom (MonoidAlgebra.of ↑R ↑S.right) ≫
          CommMonCat.ofHom ↑(MonoidAlgebra.liftNCRingHom (Hom.hom S.hom) (MonoidHom.id ↑S.right) ⋯)))
      x✝ =
    (CommMonCat.Hom.hom (𝟙 ((forget₂ CommRingCat CommMonCat).obj S.right))) x✝
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
x : R
hx : x ≠ 0
⊢ (normalizedFactors x).prod ~ᵤ x

Tactic:
exact prod_normalizedFactors hx

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

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
M : Type u
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Coalgebra R M
⊢ (TensorProduct.mk R
          ↑(Opposite.unop
              (Opposite.unop
                  ((Comon.Comon_EquivMon_OpOp (ModuleCat R)).symm.inverse.obj
                    ((comonEquivalence R).symm.inverse.obj (𝟙_ (CoalgCat R))))).X)
          ↑(Opposite.unop
              (Opposite.unop
                  ((Comon.Comon_EquivMon_OpOp (ModuleCat R)).symm.inverse.obj
                    ((comonEquivalence R).symm.inverse.obj (of R M)))).X)).compr₂ₛₗ
      (λ_ (of R M)).hom.toCoalgHom'.toLinearMap =
    (TensorProduct.mk R
          ↑(Opposite.unop
              (Opposite.unop
                  ((Comon.Comon_EquivMon_OpOp (ModuleCat R)).symm.inverse.obj
                    ((comonEquivalence R).symm.inverse.obj (𝟙_ (CoalgCat R))))).X)
          ↑(Opposite.unop
              (Opposite.unop
                  ((Comon.Comon_EquivMon_OpOp (ModuleCat R)).symm.inverse.obj
                    ((comonEquivalence R).symm.inverse.obj (of R M)))).X)).compr₂ₛₗ
      ↑(TensorProduct.lid R M)

Tactic:
ext

Goal state after:
R : Type u
inst✝³ : CommRing R
M : Type u
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Coalgebra R M
x✝ :
  ↑(Opposite.unop
      (Opposite.unop
          ((Comon.Comon_EquivMon_OpOp (ModuleCat R)).symm.inverse.obj
            ((comonEquivalence R).symm.inverse.obj (of R M)))).X)
⊢ (((TensorProduct.mk R
              ↑(Opposite.unop
                  (Opposite.unop
                      ((Comon.Comon_EquivMon_OpOp (ModuleCat R)).symm.inverse.obj
                        ((comonEquivalence R).symm.inverse.obj (𝟙_ (CoalgCat R))))).X)
              ↑(Opposite.unop
                  (Opposite.unop
                      ((Comon.Comon_EquivMon_OpOp (ModuleCat R)).symm.inverse.obj
                        ((comonEquivalence R).symm.inverse.obj (of R M)))).X)).compr₂ₛₗ
          (λ_ (of R M)).hom.toCoalgHom'.toLinearMap)
        1)
      x✝ =
    (((TensorProduct.mk R
              ↑(Opposite.unop
                  (Opposite.unop
                      ((Comon.Comon_EquivMon_OpOp (ModuleCat R)).symm.inverse.obj
                        ((comonEquivalence R).symm.inverse.obj (𝟙_ (CoalgCat R))))).X)
              ↑(Opposite.unop
                  (Opposite.unop
                      ((Comon.Comon_EquivMon_OpOp (ModuleCat R)).symm.inverse.obj
                        ((comonEquivalence R).symm.inverse.obj (of R M)))).X)).compr₂ₛₗ
          ↑(TensorProduct.lid R M))
        1)
      x✝