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

Goal state before:
pp: X✝ Y✝ : Preord
a₁✝ a₂✝ : X✝ ⟶ Y✝
h : preordToCat.map a₁✝ = preordToCat.map a₂✝
x : ↑X✝
⊢ (Preord.Hom.hom a₁✝) x = (Preord.Hom.hom a₂✝) x

Tactic:
;

Goal state after:
X✝ Y✝ : Preord
a₁✝ a₂✝ : X✝ ⟶ Y✝
h : preordToCat.map a₁✝ = preordToCat.map a₂✝
x : ↑X✝
⊢ (Preord.Hom.hom a₁✝) x = (Preord.Hom.hom a₂✝) x
Module: Mathlib.Order.Category.Semilat

Goal state before:
pp: α β : SemilatSupCat
e : α.X ≃o β.X
a✝ : α.X
⊢ (ConcreteCategory.hom
        ({ toFun := ⇑e, map_sup' := ⋯, map_bot' := ⋯ } ≫ { toFun := ⇑e.symm, map_sup' := ⋯, map_bot' := ⋯ }))
      a✝ =
    (ConcreteCategory.hom (𝟙 α)) a✝

Tactic:
;

Goal state after:
α β : SemilatSupCat
e : α.X ≃o β.X
a✝ : α.X
⊢ (ConcreteCategory.hom
        ({ toFun := ⇑e, map_sup' := ⋯, map_bot' := ⋯ } ≫ { toFun := ⇑e.symm, map_sup' := ⋯, map_bot' := ⋯ }))
      a✝ =
    (ConcreteCategory.hom (𝟙 α)) a✝
Module: Mathlib.Order.Category.Semilat

Goal state before:
pp: α β : SemilatSupCat
e : α.X ≃o β.X
a✝ : β.X
⊢ (ConcreteCategory.hom
        ({ toFun := ⇑e.symm, map_sup' := ⋯, map_bot' := ⋯ } ≫ { toFun := ⇑e, map_sup' := ⋯, map_bot' := ⋯ }))
      a✝ =
    (ConcreteCategory.hom (𝟙 β)) a✝

Tactic:
;

Goal state after:
α β : SemilatSupCat
e : α.X ≃o β.X
a✝ : β.X
⊢ (ConcreteCategory.hom
        ({ toFun := ⇑e.symm, map_sup' := ⋯, map_bot' := ⋯ } ≫ { toFun := ⇑e, map_sup' := ⋯, map_bot' := ⋯ }))
      a✝ =
    (ConcreteCategory.hom (𝟙 β)) a✝
Module: Mathlib.Order.Category.Semilat

Goal state before:
pp: α β : SemilatInfCat
e : α.X ≃o β.X
a✝ : α.X
⊢ (ConcreteCategory.hom
        ({ toFun := ⇑e, map_inf' := ⋯, map_top' := ⋯ } ≫ { toFun := ⇑e.symm, map_inf' := ⋯, map_top' := ⋯ }))
      a✝ =
    (ConcreteCategory.hom (𝟙 α)) a✝

Tactic:
;

Goal state after:
α β : SemilatInfCat
e : α.X ≃o β.X
a✝ : α.X
⊢ (ConcreteCategory.hom
        ({ toFun := ⇑e, map_inf' := ⋯, map_top' := ⋯ } ≫ { toFun := ⇑e.symm, map_inf' := ⋯, map_top' := ⋯ }))
      a✝ =
    (ConcreteCategory.hom (𝟙 α)) a✝
Module: Mathlib.Order.Category.Semilat

Goal state before:
pp: α β : SemilatInfCat
e : α.X ≃o β.X
a✝ : β.X
⊢ (ConcreteCategory.hom
        ({ toFun := ⇑e.symm, map_inf' := ⋯, map_top' := ⋯ } ≫ { toFun := ⇑e, map_inf' := ⋯, map_top' := ⋯ }))
      a✝ =
    (ConcreteCategory.hom (𝟙 β)) a✝

Tactic:
;

Goal state after:
α β : SemilatInfCat
e : α.X ≃o β.X
a✝ : β.X
⊢ (ConcreteCategory.hom
        ({ toFun := ⇑e.symm, map_inf' := ⋯, map_top' := ⋯ } ≫ { toFun := ⇑e, map_inf' := ⋯, map_top' := ⋯ }))
      a✝ =
    (ConcreteCategory.hom (𝟙 β)) a✝
Module: Mathlib.Order.Category.BddOrd

Goal state before:
pp: α β : BddOrd
e : ↑α.toPartOrd ≃o ↑β.toPartOrd
a✝ : ↑α.toPartOrd
⊢ (Hom.hom (ofHom ↑e ≫ ofHom ↑e.symm)) a✝ = (Hom.hom (𝟙 α)) a✝

Tactic:
;

Goal state after:
α β : BddOrd
e : ↑α.toPartOrd ≃o ↑β.toPartOrd
a✝ : ↑α.toPartOrd
⊢ (Hom.hom (ofHom ↑e ≫ ofHom ↑e.symm)) a✝ = (Hom.hom (𝟙 α)) a✝
Module: Mathlib.Order.Category.BddOrd

Goal state before:
pp: α β : BddOrd
e : ↑α.toPartOrd ≃o ↑β.toPartOrd
a✝ : ↑β.toPartOrd
⊢ (Hom.hom (ofHom ↑e.symm ≫ ofHom ↑e)) a✝ = (Hom.hom (𝟙 β)) a✝

Tactic:
;

Goal state after:
α β : BddOrd
e : ↑α.toPartOrd ≃o ↑β.toPartOrd
a✝ : ↑β.toPartOrd
⊢ (Hom.hom (ofHom ↑e.symm ≫ ofHom ↑e)) a✝ = (Hom.hom (𝟙 β)) a✝
Module: Mathlib.Order.Category.BddLat

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

Tactic:
;

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

Goal state before:
pp: α β : 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✝

Tactic:
;

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 ↑β
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✝

Tactic:
;

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 ↑β
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✝

Tactic:
;

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.Order.Heyting.Hom

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : FunLike F α β
inst✝³ : HeytingAlgebra α
inst✝² : HeytingAlgebra β
inst✝¹ : HeytingAlgebra γ
inst✝ : HeytingAlgebra δ
g : HeytingHom α β
toFun✝ : α → β
map_sup'✝ : ∀ (a b : α), toFun✝ (a ⊔ b) = toFun✝ a ⊔ toFun✝ b
map_inf'✝ :
  ∀ (a b : α),
    { toFun := toFun✝, map_sup' := map_sup'✝ }.toFun (a ⊓ b) =
      { toFun := toFun✝, map_sup' := map_sup'✝ }.toFun a ⊓ { toFun := toFun✝, map_sup' := map_sup'✝ }.toFun b
map_bot'✝ : { toFun := toFun✝, map_sup' := map_sup'✝, map_inf' := map_inf'✝ }.toFun ⊥ = ⊥
map_himp'✝ :
  ∀ (a b : α),
    { toFun := toFun✝, map_sup' := map_sup'✝, map_inf' := map_inf'✝ }.toFun (a ⇨ b) =
      { toFun := toFun✝, map_sup' := map_sup'✝, map_inf' := map_inf'✝ }.toFun a ⇨
        { toFun := toFun✝, map_sup' := map_sup'✝, map_inf' := map_inf'✝ }.toFun b
h :
  (fun f ↦ f.toFun)
      { toFun := toFun✝, map_sup' := map_sup'✝, map_inf' := map_inf'✝, map_bot' := map_bot'✝,
        map_himp' := map_himp'✝ } =
    (fun f ↦ f.toFun) g
⊢ { toFun := toFun✝, map_sup' := map_sup'✝, map_inf' := map_inf'✝, map_bot' := map_bot'✝, map_himp' := map_himp'✝ } = g

Tactic:
;

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : FunLike F α β
inst✝³ : HeytingAlgebra α
inst✝² : HeytingAlgebra β
inst✝¹ : HeytingAlgebra γ
inst✝ : HeytingAlgebra δ
g : HeytingHom α β
toFun✝ : α → β
map_sup'✝ : ∀ (a b : α), toFun✝ (a ⊔ b) = toFun✝ a ⊔ toFun✝ b
map_inf'✝ :
  ∀ (a b : α),
    { toFun := toFun✝, map_sup' := map_sup'✝ }.toFun (a ⊓ b) =
      { toFun := toFun✝, map_sup' := map_sup'✝ }.toFun a ⊓ { toFun := toFun✝, map_sup' := map_sup'✝ }.toFun b
map_bot'✝ : { toFun := toFun✝, map_sup' := map_sup'✝, map_inf' := map_inf'✝ }.toFun ⊥ = ⊥
map_himp'✝ :
  ∀ (a b : α),
    { toFun := toFun✝, map_sup' := map_sup'✝, map_inf' := map_inf'✝ }.toFun (a ⇨ b) =
      { toFun := toFun✝, map_sup' := map_sup'✝, map_inf' := map_inf'✝ }.toFun a ⇨
        { toFun := toFun✝, map_sup' := map_sup'✝, map_inf' := map_inf'✝ }.toFun b
h :
  (fun f ↦ f.toFun)
      { toFun := toFun✝, map_sup' := map_sup'✝, map_inf' := map_inf'✝, map_bot' := map_bot'✝,
        map_himp' := map_himp'✝ } =
    (fun f ↦ f.toFun) g
⊢ { toFun := toFun✝, map_sup' := map_sup'✝, map_inf' := map_inf'✝, map_bot' := map_bot'✝, map_himp' := map_himp'✝ } = g
Module: Mathlib.Order.Heyting.Hom

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : FunLike F α β
inst✝³ : CoheytingAlgebra α
inst✝² : CoheytingAlgebra β
inst✝¹ : CoheytingAlgebra γ
inst✝ : CoheytingAlgebra δ
g : CoheytingHom α β
toFun✝ : α → β
map_sup'✝ : ∀ (a b : α), toFun✝ (a ⊔ b) = toFun✝ a ⊔ toFun✝ b
map_inf'✝ :
  ∀ (a b : α),
    { toFun := toFun✝, map_sup' := map_sup'✝ }.toFun (a ⊓ b) =
      { toFun := toFun✝, map_sup' := map_sup'✝ }.toFun a ⊓ { toFun := toFun✝, map_sup' := map_sup'✝ }.toFun b
map_top'✝ : { toFun := toFun✝, map_sup' := map_sup'✝, map_inf' := map_inf'✝ }.toFun ⊤ = ⊤
map_sdiff'✝ :
  ∀ (a b : α),
    { toFun := toFun✝, map_sup' := map_sup'✝, map_inf' := map_inf'✝ }.toFun (a \ b) =
      { toFun := toFun✝, map_sup' := map_sup'✝, map_inf' := map_inf'✝ }.toFun a \
        { toFun := toFun✝, map_sup' := map_sup'✝, map_inf' := map_inf'✝ }.toFun b
h :
  (fun f ↦ f.toFun)
      { toFun := toFun✝, map_sup' := map_sup'✝, map_inf' := map_inf'✝, map_top' := map_top'✝,
        map_sdiff' := map_sdiff'✝ } =
    (fun f ↦ f.toFun) g
⊢ { toFun := toFun✝, map_sup' := map_sup'✝, map_inf' := map_inf'✝, map_top' := map_top'✝, map_sdiff' := map_sdiff'✝ } =
    g

Tactic:
;

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : FunLike F α β
inst✝³ : CoheytingAlgebra α
inst✝² : CoheytingAlgebra β
inst✝¹ : CoheytingAlgebra γ
inst✝ : CoheytingAlgebra δ
g : CoheytingHom α β
toFun✝ : α → β
map_sup'✝ : ∀ (a b : α), toFun✝ (a ⊔ b) = toFun✝ a ⊔ toFun✝ b
map_inf'✝ :
  ∀ (a b : α),
    { toFun := toFun✝, map_sup' := map_sup'✝ }.toFun (a ⊓ b) =
      { toFun := toFun✝, map_sup' := map_sup'✝ }.toFun a ⊓ { toFun := toFun✝, map_sup' := map_sup'✝ }.toFun b
map_top'✝ : { toFun := toFun✝, map_sup' := map_sup'✝, map_inf' := map_inf'✝ }.toFun ⊤ = ⊤
map_sdiff'✝ :
  ∀ (a b : α),
    { toFun := toFun✝, map_sup' := map_sup'✝, map_inf' := map_inf'✝ }.toFun (a \ b) =
      { toFun := toFun✝, map_sup' := map_sup'✝, map_inf' := map_inf'✝ }.toFun a \
        { toFun := toFun✝, map_sup' := map_sup'✝, map_inf' := map_inf'✝ }.toFun b
h :
  (fun f ↦ f.toFun)
      { toFun := toFun✝, map_sup' := map_sup'✝, map_inf' := map_inf'✝, map_top' := map_top'✝,
        map_sdiff' := map_sdiff'✝ } =
    (fun f ↦ f.toFun) g
⊢ { toFun := toFun✝, map_sup' := map_sup'✝, map_inf' := map_inf'✝, map_top' := map_top'✝, map_sdiff' := map_sdiff'✝ } =
    g
Module: Mathlib.Order.Heyting.Hom

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : FunLike F α β
inst✝³ : BiheytingAlgebra α
inst✝² : BiheytingAlgebra β
inst✝¹ : BiheytingAlgebra γ
inst✝ : BiheytingAlgebra δ
g : BiheytingHom α β
toFun✝ : α → β
map_sup'✝ : ∀ (a b : α), toFun✝ (a ⊔ b) = toFun✝ a ⊔ toFun✝ b
map_inf'✝ :
  ∀ (a b : α),
    { toFun := toFun✝, map_sup' := map_sup'✝ }.toFun (a ⊓ b) =
      { toFun := toFun✝, map_sup' := map_sup'✝ }.toFun a ⊓ { toFun := toFun✝, map_sup' := map_sup'✝ }.toFun b
map_himp'✝ :
  ∀ (a b : α),
    { toFun := toFun✝, map_sup' := map_sup'✝, map_inf' := map_inf'✝ }.toFun (a ⇨ b) =
      { toFun := toFun✝, map_sup' := map_sup'✝, map_inf' := map_inf'✝ }.toFun a ⇨
        { toFun := toFun✝, map_sup' := map_sup'✝, map_inf' := map_inf'✝ }.toFun b
map_sdiff'✝ :
  ∀ (a b : α),
    { toFun := toFun✝, map_sup' := map_sup'✝, map_inf' := map_inf'✝ }.toFun (a \ b) =
      { toFun := toFun✝, map_sup' := map_sup'✝, map_inf' := map_inf'✝ }.toFun a \
        { toFun := toFun✝, map_sup' := map_sup'✝, map_inf' := map_inf'✝ }.toFun b
h :
  (fun f ↦ f.toFun)
      { toFun := toFun✝, map_sup' := map_sup'✝, map_inf' := map_inf'✝, map_himp' := map_himp'✝,
        map_sdiff' := map_sdiff'✝ } =
    (fun f ↦ f.toFun) g
⊢ { toFun := toFun✝, map_sup' := map_sup'✝, map_inf' := map_inf'✝, map_himp' := map_himp'✝,
      map_sdiff' := map_sdiff'✝ } =
    g

Tactic:
;

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : FunLike F α β
inst✝³ : BiheytingAlgebra α
inst✝² : BiheytingAlgebra β
inst✝¹ : BiheytingAlgebra γ
inst✝ : BiheytingAlgebra δ
g : BiheytingHom α β
toFun✝ : α → β
map_sup'✝ : ∀ (a b : α), toFun✝ (a ⊔ b) = toFun✝ a ⊔ toFun✝ b
map_inf'✝ :
  ∀ (a b : α),
    { toFun := toFun✝, map_sup' := map_sup'✝ }.toFun (a ⊓ b) =
      { toFun := toFun✝, map_sup' := map_sup'✝ }.toFun a ⊓ { toFun := toFun✝, map_sup' := map_sup'✝ }.toFun b
map_himp'✝ :
  ∀ (a b : α),
    { toFun := toFun✝, map_sup' := map_sup'✝, map_inf' := map_inf'✝ }.toFun (a ⇨ b) =
      { toFun := toFun✝, map_sup' := map_sup'✝, map_inf' := map_inf'✝ }.toFun a ⇨
        { toFun := toFun✝, map_sup' := map_sup'✝, map_inf' := map_inf'✝ }.toFun b
map_sdiff'✝ :
  ∀ (a b : α),
    { toFun := toFun✝, map_sup' := map_sup'✝, map_inf' := map_inf'✝ }.toFun (a \ b) =
      { toFun := toFun✝, map_sup' := map_sup'✝, map_inf' := map_inf'✝ }.toFun a \
        { toFun := toFun✝, map_sup' := map_sup'✝, map_inf' := map_inf'✝ }.toFun b
h :
  (fun f ↦ f.toFun)
      { toFun := toFun✝, map_sup' := map_sup'✝, map_inf' := map_inf'✝, map_himp' := map_himp'✝,
        map_sdiff' := map_sdiff'✝ } =
    (fun f ↦ f.toFun) g
⊢ { toFun := toFun✝, map_sup' := map_sup'✝, map_inf' := map_inf'✝, map_himp' := map_himp'✝,
      map_sdiff' := map_sdiff'✝ } =
    g
Module: Mathlib.Algebra.Category.BoolRing

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

Tactic:
;

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 : ↑α ≃+* ↑β
x✝ : ↑β
⊢ (Hom.hom ({ hom' := ↑e.symm } ≫ { hom' := ↑e })) x✝ = (Hom.hom (𝟙 β)) x✝

Tactic:
;

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
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✝

Tactic:
;

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

Tactic:
;

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

Tactic:
;

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

Tactic:
;

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

Tactic:
;

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'
x✝¹ : M
x✝ : N
⊢ ((AlgebraTensorModule.curry (λ ∘ₗ f ⊗ₘ g)) x✝¹) x✝ =
    ((AlgebraTensorModule.curry (g ∘ₗ λ ∘ₗ f ⊗ₘ LinearMap.id)) x✝¹) x✝

Tactic:
;

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
x✝¹ : M
x✝ : N
⊢ ((AlgebraTensorModule.curry (ρ ∘ₗ f ⊗ₘ g)) x✝¹) x✝ =
    ((AlgebraTensorModule.curry (f ∘ₗ ρ ∘ₗ LinearMap.id ⊗ₘ g)) x✝¹) x✝

Tactic:
;

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

Tactic:
;

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

Tactic:
;

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'
x✝¹ : M
x✝ : N
⊢ ((AlgebraTensorModule.curry (β ∘ₗ f ⊗ₘ g)) x✝¹) x✝ = ((AlgebraTensorModule.curry (g ⊗ₘ f ∘ₗ β)) x✝¹) x✝

Tactic:
;

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
X✝ Y✝ : Comon C
f : X✝ ⟶ Y✝
⊢ (η ≫ f.hom.op).unop = η.unop

Tactic:
;

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

Tactic:
;

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
X✝ Y✝ : Comon C
f : X✝ ⟶ Y✝
⊢ (μ ≫ f.hom.op).unop = ((f.hom.op ⊗ₘ f.hom.op) ≫ μ).unop
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ᵒᵖ
⊢ (λ_ A.X).hom.unop = (λ_ (unop A.X)).inv

Tactic:
;

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