mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Heyting.Hom

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : CoheytingAlgebra α
inst✝¹ : CoheytingAlgebra β
inst✝ : CoheytingAlgebra γ
f₁ f₂ : CoheytingHom α β
g : CoheytingHom β γ
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ g (f₁ a) = g (f₂ a)

Tactic:
by

Goal state after:
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 δ
f g : BiheytingHom α β
h : (fun f ↦ f.toFun) f = (fun f ↦ f.toFun) g
⊢ f = g

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.BoolRing

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

Tactic:
by

Goal state after:
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 δ
f : BiheytingHom α β
f' : α → β
h : f' = ⇑f
⊢ ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.BoolRing

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

Tactic:
by

Goal state after:
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 δ
f : BiheytingHom α β
f' : α → β
h : f' = ⇑f
⊢ ∀ (a b : α), f' (a ⊓ b) = f' a ⊓ f' b

Tactic:
by

Goal state after:
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 δ
f : BiheytingHom α β
f' : α → β
h : f' = ⇑f
⊢ ∀ (a b : α), f' (a ⇨ b) = f' a ⇨ f' b

Tactic:
by

Goal state after:
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 δ
f : BiheytingHom α β
f' : α → β
h : f' = ⇑f
⊢ ∀ (a b : α), f' (a \ b) = f' a \ f' b

Tactic:
by

Goal state after:
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 δ
f : BiheytingHom β γ
g : BiheytingHom α β
a b : α
⊢ (⇑f ∘ ⇑g) (a ⇨ b) = (⇑f ∘ ⇑g) a ⇨ (⇑f ∘ ⇑g) b

Tactic:
by

Goal state after:
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 δ
f : BiheytingHom β γ
g : BiheytingHom α β
a b : α
⊢ (⇑f ∘ ⇑g) (a \ b) = (⇑f ∘ ⇑g) a \ (⇑f ∘ ⇑g) b

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Braided.Opposite

Goal state before:
pp: C : Type u_2
inst✝² : Category.{v_2, u_2} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y W Z : Cᵒᵖ
⊢ (tensorμ X W Y Z).unop = tensorμ (unop X) (unop Y) (unop W) (unop Z)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Braided.Opposite

Goal state before:
pp: C : Type u_2
inst✝² : Category.{v_2, u_2} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y W Z : C
⊢ (tensorμ X W Y Z).op = tensorμ (op X) (op Y) (op W) (op Z)

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : MonoidalCategory C
X Y : C
⊢ (α_ (𝟙_ C) X Y).hom ≫ (λ_ (X ⊗ Y)).hom = (λ_ X).hom ⊗ₘ 𝟙 Y

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : MonoidalCategory C
X Y : C
⊢ (λ_ (X ⊗ Y)).hom = (α_ (𝟙_ C) X Y).inv ≫ ((λ_ X).hom ⊗ₘ 𝟙 Y)

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : MonoidalCategory C
X Y : C
⊢ (λ_ (X ⊗ Y)).inv = ((λ_ X).inv ⊗ₘ 𝟙 Y) ≫ (α_ (𝟙_ C) X Y).hom

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : MonoidalCategory C
X Y : C
⊢ 𝟙 X ⊗ₘ (ρ_ Y).inv = (ρ_ (X ⊗ Y)).inv ≫ (α_ X Y (𝟙_ C)).hom

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : MonoidalCategory C
X Y : C
⊢ (λ_ X).inv ⊗ₘ 𝟙 Y = (λ_ (X ⊗ Y)).inv ≫ (α_ (𝟙_ C) X Y).inv

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : MonoidalCategory C
W X Y Z : C
⊢ (α_ W (X ⊗ Y) Z).inv ≫ ((α_ W X Y).inv ⊗ₘ 𝟙 Z) ≫ (α_ (W ⊗ X) Y Z).hom = (𝟙 W ⊗ₘ (α_ X Y Z).hom) ≫ (α_ W X (Y ⊗ Z)).inv

Tactic:
by

Goal state after:
Module: Mathlib.Order.Heyting.Hom

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : BiheytingAlgebra α
inst✝¹ : BiheytingAlgebra β
inst✝ : BiheytingAlgebra γ
f₁ f₂ : BiheytingHom α β
g : BiheytingHom β γ
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ g (f₁ a) = g (f₂ a)

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : MonoidalCategory C
⊢ (λ_ (𝟙_ C)).hom = (ρ_ (𝟙_ C)).hom

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : MonoidalCategory C
⊢ (λ_ (𝟙_ C)).inv = (ρ_ (𝟙_ C)).inv

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : MonoidalCategory C
W X Y Z : C
⊢ (α_ W X (Y ⊗ Z)).hom ≫ (𝟙 W ⊗ₘ (α_ X Y Z).inv) = (α_ (W ⊗ X) Y Z).inv ≫ ((α_ W X Y).hom ⊗ₘ 𝟙 Z) ≫ (α_ W (X ⊗ Y) Z).hom

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : MonoidalCategory C
W X Y Z : C
⊢ (α_ (W ⊗ X) Y Z).inv ≫ ((α_ W X Y).hom ⊗ₘ 𝟙 Z) = (α_ W X (Y ⊗ Z)).hom ≫ (𝟙 W ⊗ₘ (α_ X Y Z).inv) ≫ (α_ W (X ⊗ Y) Z).inv

Tactic:
by

Goal state after:
Module: Mathlib.Order.Category.BoolAlg

Goal state before:
pp: X : BoolAlg
x : ↑X
⊢ (ConcreteCategory.hom (𝟙 X)) x = x

Tactic:
by

Goal state after:
Module: Mathlib.Order.Category.BoolAlg

Goal state before:
pp: X Y Z : BoolAlg
f : X ⟶ Y
g : Y ⟶ Z
x : ↑X
⊢ (ConcreteCategory.hom (f ≫ g)) x = (ConcreteCategory.hom g) ((ConcreteCategory.hom f) x)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Category.BoolAlg

Goal state before:
pp: X Y : BoolAlg
e : X ≅ Y
x : ↑X
⊢ (ConcreteCategory.hom e.inv) ((ConcreteCategory.hom e.hom) x) = x

Tactic:
by

Goal state after:
Module: Mathlib.Order.Category.BoolAlg

Goal state before:
pp: X Y : BoolAlg
e : X ≅ Y
s : ↑Y
⊢ (ConcreteCategory.hom e.hom) ((ConcreteCategory.hom e.inv) s) = s

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
P' : Type u_8
M₁ : Type u_11
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'
inst✝³ : AddCommMonoid P'
inst✝² : Module R P'
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
f : M →ₗ[R] N
g : N →ₗ[R] P
f' : M' →ₗ[R] N'
g' : N' →ₗ[R] P'
φ : M₁ →ₗ[R] M ⊗[R] M'
⊢ g ⊗ₘ g' ∘ₗ f ⊗ₘ f' ∘ₗ φ = (g ∘ₗ f) ⊗ₘ (g' ∘ₗ f') ∘ₗ φ

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_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₂ ⊗[R] M₃
⊢ f₁ ⊗ₘ (f₂ ⊗ₘ f₃) ∘ₗ α ∘ₗ f = α ∘ₗ (f₁ ⊗ₘ f₂) ⊗ₘ f₃ ∘ₗ f

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_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₂ ⊗[R] M₃)
⊢ (f₁ ⊗ₘ f₂) ⊗ₘ f₃ ∘ₗ α⁻¹ ∘ₗ f = α⁻¹ ∘ₗ f₁ ⊗ₘ (f₂ ⊗ₘ f₃) ∘ₗ f

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_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:
by

Goal state after:
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 : M →ₗ[R] M ⊗[R] M₃
⊢ α ∘ₗ (f₁ ⊗ₘ f₂ ∘ₗ f₁₂) ⊗ₘ f₃ ∘ₗ f = f₁ ⊗ₘ (f₂ ⊗ₘ f₃) ∘ₗ α ∘ₗ f₁₂ ⊗ₘ LinearMap.id ∘ₗ f

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_11
M₂ : Type u_12
M₃ : Type u_13
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✝³ : Module R M₁
inst✝² : Module R M₂
inst✝¹ : Module R M₃
inst✝ : Module R N₃
f₃ : M₃ →ₗ[R] N₃
f₁₂ : M →ₗ[R] M₁ ⊗[R] M₂
⊢ α ∘ₗ f₁₂ ⊗ₘ f₃ = LinearMap.id ⊗ₘ (LinearMap.id ⊗ₘ f₃) ∘ₗ α ∘ₗ 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
P : Type u_5
M₁ : Type u_11
M₂ : Type u_12
M₃ : Type u_13
N₃ : Type u_16
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
inst✝⁹ : AddCommMonoid P
inst✝⁸ : Module R P
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : AddCommMonoid M₃
inst✝⁴ : AddCommMonoid N₃
inst✝³ : Module R M₁
inst✝² : Module R M₂
inst✝¹ : Module R M₃
inst✝ : Module R N₃
f₃ : M₃ →ₗ[R] N₃
f₁₂ : M →ₗ[R] M₁ ⊗[R] M₂
f : P →ₗ[R] M ⊗[R] M₃
⊢ α ∘ₗ f₁₂ ⊗ₘ f₃ ∘ₗ f = LinearMap.id ⊗ₘ (LinearMap.id ⊗ₘ f₃) ∘ₗ α ∘ₗ f₁₂ ⊗ₘ LinearMap.id ∘ₗ f

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_11
M₂ : Type u_12
M₃ : Type u_13
N₁ : Type u_14
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : AddCommMonoid M₃
inst✝⁴ : AddCommMonoid N₁
inst✝³ : Module R M₁
inst✝² : Module R M₂
inst✝¹ : Module R M₃
inst✝ : Module R N₁
f₁ : M₁ →ₗ[R] N₁
f₂₃ : M →ₗ[R] M₂ ⊗[R] M₃
⊢ α⁻¹ ∘ₗ f₁ ⊗ₘ f₂₃ = (f₁ ⊗ₘ LinearMap.id) ⊗ₘ LinearMap.id ∘ₗ α⁻¹ ∘ₗ LinearMap.id ⊗ₘ f₂₃

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_11
M₂ : Type u_12
M₃ : Type u_13
N₁ : Type u_14
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
inst✝⁹ : AddCommMonoid P
inst✝⁸ : Module R P
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : AddCommMonoid M₃
inst✝⁴ : AddCommMonoid N₁
inst✝³ : Module R M₁
inst✝² : Module R M₂
inst✝¹ : Module R M₃
inst✝ : Module R N₁
f₁ : M₁ →ₗ[R] N₁
f₂₃ : M →ₗ[R] M₂ ⊗[R] M₃
f : P →ₗ[R] M₁ ⊗[R] M
⊢ α⁻¹ ∘ₗ f₁ ⊗ₘ f₂₃ ∘ₗ f = (f₁ ⊗ₘ LinearMap.id) ⊗ₘ LinearMap.id ∘ₗ α⁻¹ ∘ₗ LinearMap.id ⊗ₘ f₂₃ ∘ₗ f

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_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:
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_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 N
inst✝¹² : Module R N
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 : N →ₗ[R] M₁ ⊗[R] M
⊢ α⁻¹ ∘ₗ f₁ ⊗ₘ (f₂ ⊗ₘ f₃ ∘ₗ f₂₃) ∘ₗ f = (f₁ ⊗ₘ f₂) ⊗ₘ f₃ ∘ₗ α⁻¹ ∘ₗ LinearMap.id ⊗ₘ f₂₃ ∘ₗ 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
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:
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
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'
f : M →ₗ[R] M'
g : P →ₗ[R] M ⊗[R] N
⊢ α⁻¹ ∘ₗ f ⊗ₘ λ⁻¹ ∘ₗ g = (f ⊗ₘ LinearMap.id ∘ₗ ρ⁻¹) ⊗ₘ LinearMap.id ∘ₗ g

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'
f : M →ₗ[R] M'
⊢ α⁻¹ ∘ₗ f ⊗ₘ ρ⁻¹ = (f ⊗ₘ LinearMap.id) ⊗ₘ 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
P : Type u_5
M' : Type u_6
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'
f : M →ₗ[R] M'
g : P →ₗ[R] M ⊗[R] N
⊢ α⁻¹ ∘ₗ f ⊗ₘ ρ⁻¹ ∘ₗ g = (f ⊗ₘ LinearMap.id) ⊗ₘ LinearMap.id ∘ₗ ρ⁻¹ ∘ₗ g

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
⊢ α ∘ₗ ρ⁻¹ = 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
P : Type u_5
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : P →ₗ[R] M ⊗[R] N
⊢ α ∘ₗ ρ⁻¹ ∘ₗ f = LinearMap.id ⊗ₘ ρ⁻¹ ∘ₗ 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
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:
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
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 N'
inst✝ : Module R N'
f : N →ₗ[R] N'
g : P →ₗ[R] M ⊗[R] N
⊢ α ∘ₗ λ⁻¹ ⊗ₘ f ∘ₗ g = LinearMap.id ⊗ₘ (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
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:
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
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 N'
inst✝ : Module R N'
f : N →ₗ[R] N'
g : P →ₗ[R] M ⊗[R] N
⊢ α ∘ₗ ρ⁻¹ ⊗ₘ f ∘ₗ g = LinearMap.id ⊗ₘ (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
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:
by

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

Goal state before:
pp: C✝ : Type u₁
inst✝³ : Category.{v₁, u₁} C✝
inst✝² : MonoidalCategory C✝
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
⊢ (λ_ (𝟙_ C)).inv ≫ 𝟙 (𝟙_ C) ▷ 𝟙_ C = (λ_ (𝟙_ C)).inv

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✝
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
⊢ (λ_ (𝟙_ C)).inv ≫ 𝟙_ C ◁ 𝟙 (𝟙_ C) = (ρ_ (𝟙_ C)).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
P : Type u_5
M' : Type u_6
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'
f : M →ₗ[R] R
g : N →ₗ[R] M'
h : P →ₗ[R] M ⊗[R] N
⊢ λ ∘ₗ f ⊗ₘ g ∘ₗ h = g ∘ₗ λ ∘ₗ 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✝
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
⊢ (λ_ (𝟙_ C)).inv ≫ 𝟙_ C ◁ (λ_ (𝟙_ C)).inv = (λ_ (𝟙_ C)).inv ≫ (λ_ (𝟙_ C)).inv ▷ 𝟙_ C ≫ (α_ (𝟙_ C) (𝟙_ C) (𝟙_ C)).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
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:
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
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'
f : M →ₗ[R] M'
g : N →ₗ[R] R
h : P →ₗ[R] M ⊗[R] N
⊢ ρ ∘ₗ f ⊗ₘ g ∘ₗ h = f ∘ₗ ρ ∘ₗ LinearMap.id ⊗ₘ g ∘ₗ 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
f : M ≅ N
inst✝ : IsComonHom f.hom
⊢ f.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'
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
f : M ≅ N
inst✝ : IsComonHom f.hom
⊢ f.inv ≫ Δ = Δ ≫ (f.inv ⊗ₘ f.inv)

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 : C
inst✝ : ComonObj M
Z : C
f : M ⟶ Z
⊢ Δ ≫ (ε ⊗ₘ f) = f ≫ (λ_ Z).inv

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 : C
inst✝ : ComonObj M
Z : C
f : M ⟶ Z
⊢ Δ ≫ (f ⊗ₘ ε) = f ≫ (ρ_ Z).inv

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
X : C
inst✝ : ComonObj X
⊢ Δ ≫ Δ ▷ X = Δ ≫ X ◁ Δ ≫ (α_ X X X).inv

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✝ B✝ : Comon C
f : A✝ ⟶ B✝
e : IsIso ((forget C).map f)
⊢ f ≫ { hom := inv f.hom, isComonHom_hom := ⋯ } = 𝟙 A✝ ∧ { hom := inv f.hom, isComonHom_hom := ⋯ } ≫ f = 𝟙 B✝

Tactic:
by

Goal state after: