mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: case h1
R : Type u
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Semiring R
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : Module R M
x : tsze R M
r : R
h : x.fst * r = 1
⊢ (x * (inl r + inr (-(r •> (x.snd <• r))))).fst = fst 1

pp: case h2
R : Type u
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Semiring R
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : Module R M
x : tsze R M
r : R
h : x.fst * r = 1
⊢ (x * (inl r + inr (-(r •> (x.snd <• r))))).snd = snd 1

Tactic:
<;>

Goal state after:
case h1
R : Type u
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Semiring R
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : Module R M
x : tsze R M
r : R
h : x.fst * r = 1
⊢ (x * (inl r + inr (-(r •> (x.snd <• r))))).fst = fst 1

case h2
R : Type u
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Semiring R
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : Module R M
x : tsze R M
r : R
h : x.fst * r = 1
⊢ (x * (inl r + inr (-(r •> (x.snd <• r))))).snd = snd 1
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: case h1
R : Type u
M : Type v
inst✝⁵ : AddCommGroup M
inst✝⁴ : Semiring R
inst✝³ : Module Rᵐᵒᵖ M
inst✝² : Module R M
inst✝¹ : SMulCommClass R Rᵐᵒᵖ M
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
inst✝ : Invertible x.fst
⊢ fst (⅟x.fst, -(⅟x.fst •> x.snd <• ⅟x.fst)) = (inl ⅟x.fst + inr (-(⅟x.fst •> x.snd <• ⅟x.fst))).fst

pp: case h2
R : Type u
M : Type v
inst✝⁵ : AddCommGroup M
inst✝⁴ : Semiring R
inst✝³ : Module Rᵐᵒᵖ M
inst✝² : Module R M
inst✝¹ : SMulCommClass R Rᵐᵒᵖ M
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
inst✝ : Invertible x.fst
⊢ snd (⅟x.fst, -(⅟x.fst •> x.snd <• ⅟x.fst)) = (inl ⅟x.fst + inr (-(⅟x.fst •> x.snd <• ⅟x.fst))).snd

Tactic:
<;>

Goal state after:
case h1
R : Type u
M : Type v
inst✝⁵ : AddCommGroup M
inst✝⁴ : Semiring R
inst✝³ : Module Rᵐᵒᵖ M
inst✝² : Module R M
inst✝¹ : SMulCommClass R Rᵐᵒᵖ M
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
inst✝ : Invertible x.fst
⊢ fst (⅟x.fst, -(⅟x.fst •> x.snd <• ⅟x.fst)) = (inl ⅟x.fst + inr (-(⅟x.fst •> x.snd <• ⅟x.fst))).fst

case h2
R : Type u
M : Type v
inst✝⁵ : AddCommGroup M
inst✝⁴ : Semiring R
inst✝³ : Module Rᵐᵒᵖ M
inst✝² : Module R M
inst✝¹ : SMulCommClass R Rᵐᵒᵖ M
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
inst✝ : Invertible x.fst
⊢ snd (⅟x.fst, -(⅟x.fst •> x.snd <• ⅟x.fst)) = (inl ⅟x.fst + inr (-(⅟x.fst •> x.snd <• ⅟x.fst))).snd
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: case h1
R : Type u
M : Type v
inst✝⁵ : AddCommGroup M
inst✝⁴ : Semiring R
inst✝³ : Module Rᵐᵒᵖ M
inst✝² : Module R M
inst✝¹ : SMulCommClass R Rᵐᵒᵖ M
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
inst✝ : Invertible x.fst
⊢ fst (⅟x.fst, -(⅟x.fst •> x.snd <• ⅟x.fst)) = (inl ⅟x.fst + inr (-(⅟x.fst •> (x.snd <• ⅟x.fst)))).fst

pp: case h2
R : Type u
M : Type v
inst✝⁵ : AddCommGroup M
inst✝⁴ : Semiring R
inst✝³ : Module Rᵐᵒᵖ M
inst✝² : Module R M
inst✝¹ : SMulCommClass R Rᵐᵒᵖ M
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
inst✝ : Invertible x.fst
⊢ snd (⅟x.fst, -(⅟x.fst •> x.snd <• ⅟x.fst)) = (inl ⅟x.fst + inr (-(⅟x.fst •> (x.snd <• ⅟x.fst)))).snd

Tactic:
<;>

Goal state after:
case h1
R : Type u
M : Type v
inst✝⁵ : AddCommGroup M
inst✝⁴ : Semiring R
inst✝³ : Module Rᵐᵒᵖ M
inst✝² : Module R M
inst✝¹ : SMulCommClass R Rᵐᵒᵖ M
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
inst✝ : Invertible x.fst
⊢ fst (⅟x.fst, -(⅟x.fst •> x.snd <• ⅟x.fst)) = (inl ⅟x.fst + inr (-(⅟x.fst •> (x.snd <• ⅟x.fst)))).fst

case h2
R : Type u
M : Type v
inst✝⁵ : AddCommGroup M
inst✝⁴ : Semiring R
inst✝³ : Module Rᵐᵒᵖ M
inst✝² : Module R M
inst✝¹ : SMulCommClass R Rᵐᵒᵖ M
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
inst✝ : Invertible x.fst
⊢ snd (⅟x.fst, -(⅟x.fst •> x.snd <• ⅟x.fst)) = (inl ⅟x.fst + inr (-(⅟x.fst •> (x.snd <• ⅟x.fst)))).snd
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: case h1
R : Type u
M : Type v
inst✝³ : DivisionSemiring R
inst✝² : AddCommGroup M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : Module R M
x : tsze R M
hx : x.fst ≠ 0
⊢ x⁻¹.fst = (inl x.fst⁻¹ + inr (-(x.fst⁻¹ •> x.snd <• x.fst⁻¹))).fst

pp: case h2
R : Type u
M : Type v
inst✝³ : DivisionSemiring R
inst✝² : AddCommGroup M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : Module R M
x : tsze R M
hx : x.fst ≠ 0
⊢ x⁻¹.snd = (inl x.fst⁻¹ + inr (-(x.fst⁻¹ •> x.snd <• x.fst⁻¹))).snd

Tactic:
<;>

Goal state after:
case h1
R : Type u
M : Type v
inst✝³ : DivisionSemiring R
inst✝² : AddCommGroup M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : Module R M
x : tsze R M
hx : x.fst ≠ 0
⊢ x⁻¹.fst = (inl x.fst⁻¹ + inr (-(x.fst⁻¹ •> x.snd <• x.fst⁻¹))).fst

case h2
R : Type u
M : Type v
inst✝³ : DivisionSemiring R
inst✝² : AddCommGroup M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : Module R M
x : tsze R M
hx : x.fst ≠ 0
⊢ x⁻¹.snd = (inl x.fst⁻¹ + inr (-(x.fst⁻¹ •> x.snd <• x.fst⁻¹))).snd
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: case h1
R : Type u
M : Type v
inst✝⁵ : DivisionSemiring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module Rᵐᵒᵖ M
inst✝² : Module R M
inst✝¹ : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
inst✝ : Invertible x
this : Invertible x.fst := ⋯
⊢ (⅟x).fst = x⁻¹.fst

pp: case h2
R : Type u
M : Type v
inst✝⁵ : DivisionSemiring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module Rᵐᵒᵖ M
inst✝² : Module R M
inst✝¹ : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
inst✝ : Invertible x
this : Invertible x.fst := ⋯
⊢ (⅟x).snd = x⁻¹.snd

Tactic:
<;>

Goal state after:
case h1
R : Type u
M : Type v
inst✝⁵ : DivisionSemiring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module Rᵐᵒᵖ M
inst✝² : Module R M
inst✝¹ : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
inst✝ : Invertible x
this : Invertible x.fst := ⋯
⊢ (⅟x).fst = x⁻¹.fst

case h2
R : Type u
M : Type v
inst✝⁵ : DivisionSemiring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module Rᵐᵒᵖ M
inst✝² : Module R M
inst✝¹ : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
inst✝ : Invertible x
this : Invertible x.fst := ⋯
⊢ (⅟x).snd = x⁻¹.snd
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: case h1
R : Type u
M : Type v
inst✝³ : DivisionRing R
inst✝² : AddCommGroup M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : Module R M
x : tsze R M
⊢ (-x)⁻¹.fst = (-x⁻¹).fst

pp: case h2
R : Type u
M : Type v
inst✝³ : DivisionRing R
inst✝² : AddCommGroup M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : Module R M
x : tsze R M
⊢ (-x)⁻¹.snd = (-x⁻¹).snd

Tactic:
<;>

Goal state after:
case h1
R : Type u
M : Type v
inst✝³ : DivisionRing R
inst✝² : AddCommGroup M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : Module R M
x : tsze R M
⊢ (-x)⁻¹.fst = (-x⁻¹).fst

case h2
R : Type u
M : Type v
inst✝³ : DivisionRing R
inst✝² : AddCommGroup M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : Module R M
x : tsze R M
⊢ (-x)⁻¹.snd = (-x⁻¹).snd
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: case hl
R : Type u
A : Type v
B : Type w
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid A
inst✝⁶ : AddCommMonoid B
inst✝⁵ : Module R A
inst✝⁴ : Module R B
inst✝³ : Coalgebra R A
inst✝² : Coalgebra R B
inst✝¹ : IsCocomm R A
inst✝ : IsCocomm R B
x✝ : A
⊢ ((↑(TensorProduct.comm R (A × B) (A × B)) ∘ₗ comul) ∘ₗ inl R A B) x✝ = (comul ∘ₗ inl R A B) x✝

pp: case hr
R : Type u
A : Type v
B : Type w
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid A
inst✝⁶ : AddCommMonoid B
inst✝⁵ : Module R A
inst✝⁴ : Module R B
inst✝³ : Coalgebra R A
inst✝² : Coalgebra R B
inst✝¹ : IsCocomm R A
inst✝ : IsCocomm R B
x✝ : B
⊢ ((↑(TensorProduct.comm R (A × B) (A × B)) ∘ₗ comul) ∘ₗ inr R A B) x✝ = (comul ∘ₗ inr R A B) x✝

Tactic:
<;>

Goal state after:
case hl
R : Type u
A : Type v
B : Type w
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid A
inst✝⁶ : AddCommMonoid B
inst✝⁵ : Module R A
inst✝⁴ : Module R B
inst✝³ : Coalgebra R A
inst✝² : Coalgebra R B
inst✝¹ : IsCocomm R A
inst✝ : IsCocomm R B
x✝ : A
⊢ ((↑(TensorProduct.comm R (A × B) (A × B)) ∘ₗ comul) ∘ₗ inl R A B) x✝ = (comul ∘ₗ inl R A B) x✝

case hr
R : Type u
A : Type v
B : Type w
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid A
inst✝⁶ : AddCommMonoid B
inst✝⁵ : Module R A
inst✝⁴ : Module R B
inst✝³ : Coalgebra R A
inst✝² : Coalgebra R B
inst✝¹ : IsCocomm R A
inst✝ : IsCocomm R B
x✝ : B
⊢ ((↑(TensorProduct.comm R (A × B) (A × B)) ∘ₗ comul) ∘ₗ inr R A B) x✝ = (comul ∘ₗ inr R A B) x✝
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
Y : ModuleCat S
m1 : Module R S := Module.compHom S f
m2 : Module R ↑Y := Module.compHom (↑Y) f
s : S
r : R
y : ↑Y
⊢ s • r • y = (RingHom.id R) r • s • y

Tactic:
change s • f r • y = f r • s • y

Goal state after:
R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
Y : ModuleCat S
m1 : Module R S := Module.compHom S f
m2 : Module R ↑Y := Module.compHom (↑Y) f
s : S
r : R
y : ↑Y
⊢ s • f r • y = f r • s • y
Module: Mathlib.CategoryTheory.Category.Pointed

Goal state before:
pp: case none
X'✝ X✝ : Type ?u.36
Y✝ : Pointed
f : X'✝ ⟶ X✝
g : X✝ ⟶ (forget Pointed).obj Y✝
⊢ ({ toFun := fun f ↦ ↾(f.toFun ∘ some),
              invFun := fun f ↦ { toFun := fun o ↦ Option.elim o Y✝.point ⇑(ConcreteCategory.hom f), map_point := ⋯ },
              left_inv := ⋯, right_inv := ⋯ }.symm
          (f ≫ g)).toFun
      none =
    (typeToPointed.map f ≫
          { toFun := fun f ↦ ↾(f.toFun ∘ some),
                invFun := fun f ↦ { toFun := fun o ↦ Option.elim o Y✝.point ⇑(ConcreteCategory.hom f), map_point := ⋯ },
                left_inv := ⋯, right_inv := ⋯ }.symm
            g).toFun
      none

pp: case some
X'✝ X✝ : Type ?u.36
Y✝ : Pointed
f : X'✝ ⟶ X✝
g : X✝ ⟶ (forget Pointed).obj Y✝
val✝ : X'✝
⊢ ({ toFun := fun f ↦ ↾(f.toFun ∘ some),
              invFun := fun f ↦ { toFun := fun o ↦ Option.elim o Y✝.point ⇑(ConcreteCategory.hom f), map_point := ⋯ },
              left_inv := ⋯, right_inv := ⋯ }.symm
          (f ≫ g)).toFun
      (some val✝) =
    (typeToPointed.map f ≫
          { toFun := fun f ↦ ↾(f.toFun ∘ some),
                invFun := fun f ↦ { toFun := fun o ↦ Option.elim o Y✝.point ⇑(ConcreteCategory.hom f), map_point := ⋯ },
                left_inv := ⋯, right_inv := ⋯ }.symm
            g).toFun
      (some val✝)

Tactic:
<;>

Goal state after:
case none
X'✝ X✝ : Type ?u.36
Y✝ : Pointed
f : X'✝ ⟶ X✝
g : X✝ ⟶ (forget Pointed).obj Y✝
⊢ ({ toFun := fun f ↦ ↾(f.toFun ∘ some),
              invFun := fun f ↦ { toFun := fun o ↦ Option.elim o Y✝.point ⇑(ConcreteCategory.hom f), map_point := ⋯ },
              left_inv := ⋯, right_inv := ⋯ }.symm
          (f ≫ g)).toFun
      none =
    (typeToPointed.map f ≫
          { toFun := fun f ↦ ↾(f.toFun ∘ some),
                invFun := fun f ↦ { toFun := fun o ↦ Option.elim o Y✝.point ⇑(ConcreteCategory.hom f), map_point := ⋯ },
                left_inv := ⋯, right_inv := ⋯ }.symm
            g).toFun
      none

case some
X'✝ X✝ : Type ?u.36
Y✝ : Pointed
f : X'✝ ⟶ X✝
g : X✝ ⟶ (forget Pointed).obj Y✝
val✝ : X'✝
⊢ ({ toFun := fun f ↦ ↾(f.toFun ∘ some),
              invFun := fun f ↦ { toFun := fun o ↦ Option.elim o Y✝.point ⇑(ConcreteCategory.hom f), map_point := ⋯ },
              left_inv := ⋯, right_inv := ⋯ }.symm
          (f ≫ g)).toFun
      (some val✝) =
    (typeToPointed.map f ≫
          { toFun := fun f ↦ ↾(f.toFun ∘ some),
                invFun := fun f ↦ { toFun := fun o ↦ Option.elim o Y✝.point ⇑(ConcreteCategory.hom f), map_point := ⋯ },
                left_inv := ⋯, right_inv := ⋯ }.symm
            g).toFun
      (some val✝)
Module: Mathlib.Algebra.Ring.BooleanRing

Goal state before:
pp: case false
α : Type u_1
β : Type u_2
γ : Type u_3
⊢ false * 0 = 0

pp: case true
α : Type u_1
β : Type u_2
γ : Type u_3
⊢ true * 0 = 0

Tactic:
<;>

Goal state after:
case false
α : Type u_1
β : Type u_2
γ : Type u_3
⊢ false * 0 = 0

case true
α : Type u_1
β : Type u_2
γ : Type u_3
⊢ true * 0 = 0
Module: Mathlib.RingTheory.Bialgebra.TensorProduct

Goal state before:
pp: case ha
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
D : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Bialgebra R A
inst✝ : Bialgebra R B
x✝ : A
⊢ (((counitAlgHom R (B ⊗[R] A)).comp ↑(Algebra.TensorProduct.comm R A B)).comp Algebra.TensorProduct.includeLeft) x✝ =
    ((counitAlgHom R (A ⊗[R] B)).comp Algebra.TensorProduct.includeLeft) x✝

pp: case hb
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
D : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Bialgebra R A
inst✝ : Bialgebra R B
x✝ : B
⊢ ((AlgHom.restrictScalars R ((counitAlgHom R (B ⊗[R] A)).comp ↑(Algebra.TensorProduct.comm R A B))).comp
        Algebra.TensorProduct.includeRight)
      x✝ =
    ((AlgHom.restrictScalars R (counitAlgHom R (A ⊗[R] B))).comp Algebra.TensorProduct.includeRight) x✝

Tactic:
<;>

Goal state after:
case ha
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
D : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Bialgebra R A
inst✝ : Bialgebra R B
x✝ : A
⊢ (((counitAlgHom R (B ⊗[R] A)).comp ↑(Algebra.TensorProduct.comm R A B)).comp Algebra.TensorProduct.includeLeft) x✝ =
    ((counitAlgHom R (A ⊗[R] B)).comp Algebra.TensorProduct.includeLeft) x✝

case hb
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
D : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Bialgebra R A
inst✝ : Bialgebra R B
x✝ : B
⊢ ((AlgHom.restrictScalars R ((counitAlgHom R (B ⊗[R] A)).comp ↑(Algebra.TensorProduct.comm R A B))).comp
        Algebra.TensorProduct.includeRight)
      x✝ =
    ((AlgHom.restrictScalars R (counitAlgHom R (A ⊗[R] B))).comp Algebra.TensorProduct.includeRight) x✝
Module: Mathlib.RingTheory.Bialgebra.TensorProduct

Goal state before:
pp: case ha
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
D : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Bialgebra R A
inst✝ : Bialgebra R B
a : A
⊢ (((Algebra.TensorProduct.map ↑(Algebra.TensorProduct.comm R A B) ↑(Algebra.TensorProduct.comm R A B)).comp
            (comulAlgHom R (A ⊗[R] B))).comp
        Algebra.TensorProduct.includeLeft)
      a =
    (((comulAlgHom R (B ⊗[R] A)).comp ↑(Algebra.TensorProduct.comm R A B)).comp Algebra.TensorProduct.includeLeft) a

pp: case hb
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
D : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Bialgebra R A
inst✝ : Bialgebra R B
a : B
⊢ ((AlgHom.restrictScalars R
            ((Algebra.TensorProduct.map ↑(Algebra.TensorProduct.comm R A B) ↑(Algebra.TensorProduct.comm R A B)).comp
              (comulAlgHom R (A ⊗[R] B)))).comp
        Algebra.TensorProduct.includeRight)
      a =
    ((AlgHom.restrictScalars R ((comulAlgHom R (B ⊗[R] A)).comp ↑(Algebra.TensorProduct.comm R A B))).comp
        Algebra.TensorProduct.includeRight)
      a

Tactic:
<;>

Goal state after:
case ha
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
D : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Bialgebra R A
inst✝ : Bialgebra R B
a : A
⊢ (((Algebra.TensorProduct.map ↑(Algebra.TensorProduct.comm R A B) ↑(Algebra.TensorProduct.comm R A B)).comp
            (comulAlgHom R (A ⊗[R] B))).comp
        Algebra.TensorProduct.includeLeft)
      a =
    (((comulAlgHom R (B ⊗[R] A)).comp ↑(Algebra.TensorProduct.comm R A B)).comp Algebra.TensorProduct.includeLeft) a

case hb
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
D : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Bialgebra R A
inst✝ : Bialgebra R B
a : B
⊢ ((AlgHom.restrictScalars R
            ((Algebra.TensorProduct.map ↑(Algebra.TensorProduct.comm R A B) ↑(Algebra.TensorProduct.comm R A B)).comp
              (comulAlgHom R (A ⊗[R] B)))).comp
        Algebra.TensorProduct.includeRight)
      a =
    ((AlgHom.restrictScalars R ((comulAlgHom R (B ⊗[R] A)).comp ↑(Algebra.TensorProduct.comm R A B))).comp
        Algebra.TensorProduct.includeRight)
      a
Module: Mathlib.CategoryTheory.Category.Bipointed

Goal state before:
pp: case none
X'✝ X✝ : Pointed
Y✝ : Bipointed
f : X'✝ ⟶ X✝
g : X✝ ⟶ bipointedToPointedFst.obj Y✝
⊢ ({ toFun := fun f ↦ { toFun := f.toFun ∘ some, map_point := ⋯ },
              invFun := fun f ↦ { toFun := fun o ↦ Option.elim o Y✝.toProd.2 f.toFun, map_fst := ⋯, map_snd := ⋯ },
              left_inv := ⋯, right_inv := ⋯ }.symm
          (f ≫ g)).toFun
      none =
    (pointedToBipointedFst.map f ≫
          { toFun := fun f ↦ { toFun := f.toFun ∘ some, map_point := ⋯ },
                invFun := fun f ↦ { toFun := fun o ↦ Option.elim o Y✝.toProd.2 f.toFun, map_fst := ⋯, map_snd := ⋯ },
                left_inv := ⋯, right_inv := ⋯ }.symm
            g).toFun
      none

pp: case some
X'✝ X✝ : Pointed
Y✝ : Bipointed
f : X'✝ ⟶ X✝
g : X✝ ⟶ bipointedToPointedFst.obj Y✝
val✝ : X'✝.X
⊢ ({ toFun := fun f ↦ { toFun := f.toFun ∘ some, map_point := ⋯ },
              invFun := fun f ↦ { toFun := fun o ↦ Option.elim o Y✝.toProd.2 f.toFun, map_fst := ⋯, map_snd := ⋯ },
              left_inv := ⋯, right_inv := ⋯ }.symm
          (f ≫ g)).toFun
      (some val✝) =
    (pointedToBipointedFst.map f ≫
          { toFun := fun f ↦ { toFun := f.toFun ∘ some, map_point := ⋯ },
                invFun := fun f ↦ { toFun := fun o ↦ Option.elim o Y✝.toProd.2 f.toFun, map_fst := ⋯, map_snd := ⋯ },
                left_inv := ⋯, right_inv := ⋯ }.symm
            g).toFun
      (some val✝)

Tactic:
<;>

Goal state after:
case none
X'✝ X✝ : Pointed
Y✝ : Bipointed
f : X'✝ ⟶ X✝
g : X✝ ⟶ bipointedToPointedFst.obj Y✝
⊢ ({ toFun := fun f ↦ { toFun := f.toFun ∘ some, map_point := ⋯ },
              invFun := fun f ↦ { toFun := fun o ↦ Option.elim o Y✝.toProd.2 f.toFun, map_fst := ⋯, map_snd := ⋯ },
              left_inv := ⋯, right_inv := ⋯ }.symm
          (f ≫ g)).toFun
      none =
    (pointedToBipointedFst.map f ≫
          { toFun := fun f ↦ { toFun := f.toFun ∘ some, map_point := ⋯ },
                invFun := fun f ↦ { toFun := fun o ↦ Option.elim o Y✝.toProd.2 f.toFun, map_fst := ⋯, map_snd := ⋯ },
                left_inv := ⋯, right_inv := ⋯ }.symm
            g).toFun
      none

case some
X'✝ X✝ : Pointed
Y✝ : Bipointed
f : X'✝ ⟶ X✝
g : X✝ ⟶ bipointedToPointedFst.obj Y✝
val✝ : X'✝.X
⊢ ({ toFun := fun f ↦ { toFun := f.toFun ∘ some, map_point := ⋯ },
              invFun := fun f ↦ { toFun := fun o ↦ Option.elim o Y✝.toProd.2 f.toFun, map_fst := ⋯, map_snd := ⋯ },
              left_inv := ⋯, right_inv := ⋯ }.symm
          (f ≫ g)).toFun
      (some val✝) =
    (pointedToBipointedFst.map f ≫
          { toFun := fun f ↦ { toFun := f.toFun ∘ some, map_point := ⋯ },
                invFun := fun f ↦ { toFun := fun o ↦ Option.elim o Y✝.toProd.2 f.toFun, map_fst := ⋯, map_snd := ⋯ },
                left_inv := ⋯, right_inv := ⋯ }.symm
            g).toFun
      (some val✝)
Module: Mathlib.CategoryTheory.Category.Bipointed

Goal state before:
pp: case none
X'✝ X✝ : Pointed
Y✝ : Bipointed
f : X'✝ ⟶ X✝
g : X✝ ⟶ bipointedToPointedSnd.obj Y✝
⊢ ({ toFun := fun f ↦ { toFun := f.toFun ∘ some, map_point := ⋯ },
              invFun := fun f ↦ { toFun := fun o ↦ Option.elim o Y✝.toProd.1 f.toFun, map_fst := ⋯, map_snd := ⋯ },
              left_inv := ⋯, right_inv := ⋯ }.symm
          (f ≫ g)).toFun
      none =
    (pointedToBipointedSnd.map f ≫
          { toFun := fun f ↦ { toFun := f.toFun ∘ some, map_point := ⋯ },
                invFun := fun f ↦ { toFun := fun o ↦ Option.elim o Y✝.toProd.1 f.toFun, map_fst := ⋯, map_snd := ⋯ },
                left_inv := ⋯, right_inv := ⋯ }.symm
            g).toFun
      none

pp: case some
X'✝ X✝ : Pointed
Y✝ : Bipointed
f : X'✝ ⟶ X✝
g : X✝ ⟶ bipointedToPointedSnd.obj Y✝
val✝ : X'✝.X
⊢ ({ toFun := fun f ↦ { toFun := f.toFun ∘ some, map_point := ⋯ },
              invFun := fun f ↦ { toFun := fun o ↦ Option.elim o Y✝.toProd.1 f.toFun, map_fst := ⋯, map_snd := ⋯ },
              left_inv := ⋯, right_inv := ⋯ }.symm
          (f ≫ g)).toFun
      (some val✝) =
    (pointedToBipointedSnd.map f ≫
          { toFun := fun f ↦ { toFun := f.toFun ∘ some, map_point := ⋯ },
                invFun := fun f ↦ { toFun := fun o ↦ Option.elim o Y✝.toProd.1 f.toFun, map_fst := ⋯, map_snd := ⋯ },
                left_inv := ⋯, right_inv := ⋯ }.symm
            g).toFun
      (some val✝)

Tactic:
<;>

Goal state after:
case none
X'✝ X✝ : Pointed
Y✝ : Bipointed
f : X'✝ ⟶ X✝
g : X✝ ⟶ bipointedToPointedSnd.obj Y✝
⊢ ({ toFun := fun f ↦ { toFun := f.toFun ∘ some, map_point := ⋯ },
              invFun := fun f ↦ { toFun := fun o ↦ Option.elim o Y✝.toProd.1 f.toFun, map_fst := ⋯, map_snd := ⋯ },
              left_inv := ⋯, right_inv := ⋯ }.symm
          (f ≫ g)).toFun
      none =
    (pointedToBipointedSnd.map f ≫
          { toFun := fun f ↦ { toFun := f.toFun ∘ some, map_point := ⋯ },
                invFun := fun f ↦ { toFun := fun o ↦ Option.elim o Y✝.toProd.1 f.toFun, map_fst := ⋯, map_snd := ⋯ },
                left_inv := ⋯, right_inv := ⋯ }.symm
            g).toFun
      none

case some
X'✝ X✝ : Pointed
Y✝ : Bipointed
f : X'✝ ⟶ X✝
g : X✝ ⟶ bipointedToPointedSnd.obj Y✝
val✝ : X'✝.X
⊢ ({ toFun := fun f ↦ { toFun := f.toFun ∘ some, map_point := ⋯ },
              invFun := fun f ↦ { toFun := fun o ↦ Option.elim o Y✝.toProd.1 f.toFun, map_fst := ⋯, map_snd := ⋯ },
              left_inv := ⋯, right_inv := ⋯ }.symm
          (f ≫ g)).toFun
      (some val✝) =
    (pointedToBipointedSnd.map f ≫
          { toFun := fun f ↦ { toFun := f.toFun ∘ some, map_point := ⋯ },
                invFun := fun f ↦ { toFun := fun o ↦ Option.elim o Y✝.toProd.1 f.toFun, map_fst := ⋯, map_snd := ⋯ },
                left_inv := ⋯, right_inv := ⋯ }.symm
            g).toFun
      (some val✝)
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:
rw [← op_whiskerLeft, ← op_comp, comul_counit]

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
⊢ (ρ_ A.X).inv.op = (ρ_ (op A.X)).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
A : Mon Cᵒᵖ
⊢ μ.unop ≫ unop A.X ◁ η.unop = (ρ_ (unop A.X)).inv

Tactic:
by rw [← unop_whiskerLeft, ← unop_comp, MonObj.mul_one]; rfl

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:
simp_rw [← LinearMap.comp_assoc]

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