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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Monoid G
inst✝ : MulSemiringAction G k
f : SkewMonoidAlgebra k G
r : k
x : G
⊢ (single 1 r * f).coeff x = r * f.coeff x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Group G
inst✝ : MulSemiringAction G k
f g : SkewMonoidAlgebra k G
x : G
⊢ (f * g).coeff x = f.sum fun a b ↦ (single a b * g).coeff x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Group G
inst✝ : MulSemiringAction G k
f g : SkewMonoidAlgebra k G
x : G
⊢ (f.sum fun a b ↦ (single a b * g).coeff x) = f.sum fun a b ↦ b * a • g.coeff (a⁻¹ * x)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Group G
inst✝ : MulSemiringAction G k
f g : SkewMonoidAlgebra k G
x : G
⊢ (f * g).coeff x = g.sum fun a b ↦ (f * single a b).coeff x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Group G
inst✝ : MulSemiringAction G k
f g : SkewMonoidAlgebra k G
x : G
⊢ (g.sum fun a b ↦ (f * single a b).coeff x) = g.sum fun a b ↦ f.coeff (x * a⁻¹) * (x * a⁻¹) • b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Monoid G
inst✝ : MulSemiringAction G k
a₁ a₂ : G
b₁ b₂ : k
⊢ ((single a₂ b₂).sum fun a₂ b₂ ↦ single (a₁ * a₂) (0 * a₁ • b₂)) = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Monoid G
inst✝ : MulSemiringAction G k
a₁ a₂ : G
b₁ b₂ : k
⊢ single (a₁ * a₂) (b₁ * a₁ • 0) = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Monoid G
inst✝ : MulSemiringAction G k
x y : k
⊢ (↑(singleAddHom 1)).toFun (x * y) = (↑(singleAddHom 1)).toFun x * (↑(singleAddHom 1)).toFun y

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Monoid G
inst✝ : MulSemiringAction G k
f g : SkewMonoidAlgebra k G →+* k
h₁ : ∀ (b : k), f (single 1 b) = g (single 1 b)
h_of : ∀ (a : G), f (single a 1) = g (single a 1)
a : G
b₁ b₂ : k
⊢ single 1 b₁ * single a b₂ = single a (b₁ * b₂)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Monoid G
inst✝ : MulSemiringAction G k
f g : SkewMonoidAlgebra k G →+* k
h₁ : ∀ (b : k), f (single 1 b) = g (single 1 b)
h_of : ∀ (a : G), f (single a 1) = g (single a 1)
this : ∀ {a : G} {b₁ b₂ : k}, single 1 b₁ * single a b₂ = single a (b₁ * b₂)
a : G
b : k
⊢ ((fun f ↦ ↑f) f) (single a b) = ((fun f ↦ ↑f) g) (single a b)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: α : Type u_3
α₂ : Type u_4
β : Type u_5
F : Type u_6
inst✝⁴ : Semiring β
inst✝³ : Monoid α
inst✝² : Monoid α₂
inst✝¹ : FunLike F α α₂
inst✝ : MonoidHomClass F α α₂
f : F
⊢ (mapDomain ⇑f) 1 = 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: α : Type u_3
α₂ : Type u_4
β : Type u_5
F : Type u_6
inst✝⁶ : Semiring β
inst✝⁵ : Monoid α
inst✝⁴ : Monoid α₂
inst✝³ : FunLike F α α₂
inst✝² : MulSemiringAction α β
inst✝¹ : MulSemiringAction α₂ β
inst✝ : MulHomClass F α α₂
f : F
x y : SkewMonoidAlgebra β α
hf : ∀ (a : α) (x : β), a • x = f a • x
⊢ ∀ (b : α₂), (((mapDomain ⇑f) y).sum fun a₂ b₂ ↦ single (b * a₂) (0 * b • b₂)) = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: α : Type u_3
α₂ : Type u_4
β : Type u_5
F : Type u_6
inst✝⁶ : Semiring β
inst✝⁵ : Monoid α
inst✝⁴ : Monoid α₂
inst✝³ : FunLike F α α₂
inst✝² : MulSemiringAction α β
inst✝¹ : MulSemiringAction α₂ β
inst✝ : MulHomClass F α α₂
f : F
x y : SkewMonoidAlgebra β α
hf : ∀ (a : α) (x : β), a • x = f a • x
⊢ ∀ (b : α₂) (m₁ m₂ : β),
    (((mapDomain ⇑f) y).sum fun a₂ b₂ ↦ single (b * a₂) ((m₁ + m₂) * b • b₂)) =
      (((mapDomain ⇑f) y).sum fun a₂ b₂ ↦ single (b * a₂) (m₁ * b • b₂)) +
        ((mapDomain ⇑f) y).sum fun a₂ b₂ ↦ single (b * a₂) (m₂ * b • b₂)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: α : Type u_3
α₂ : Type u_4
β : Type u_5
F : Type u_6
inst✝⁶ : Semiring β
inst✝⁵ : Monoid α
inst✝⁴ : Monoid α₂
inst✝³ : FunLike F α α₂
inst✝² : MulSemiringAction α β
inst✝¹ : MulSemiringAction α₂ β
inst✝ : MulHomClass F α α₂
f : F
x y : SkewMonoidAlgebra β α
hf : ∀ (a : α) (x : β), a • x = f a • x
a : α
b : β
c : α₂
⊢ ∀ (b_1 : α₂), single (f a * b_1) (b * f a • 0) = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: α : Type u_3
α₂ : Type u_4
β : Type u_5
F : Type u_6
inst✝⁶ : Semiring β
inst✝⁵ : Monoid α
inst✝⁴ : Monoid α₂
inst✝³ : FunLike F α α₂
inst✝² : MulSemiringAction α β
inst✝¹ : MulSemiringAction α₂ β
inst✝ : MulHomClass F α α₂
f : F
x y : SkewMonoidAlgebra β α
hf : ∀ (a : α) (x : β), a • x = f a • x
a : α
b : β
c : α₂
⊢ ∀ (b_1 : α₂) (m₁ m₂ : β),
    single (f a * b_1) (b * f a • (m₁ + m₂)) = single (f a * b_1) (b * f a • m₁) + single (f a * b_1) (b * f a • m₂)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: α : Type u_3
α₂ : Type u_4
β : Type u_5
F : Type u_6
inst✝⁶ : Semiring β
inst✝⁵ : Monoid α
inst✝⁴ : Monoid α₂
inst✝³ : FunLike F α α₂
inst✝² : MulSemiringAction α β
inst✝¹ : MulSemiringAction α₂ β
inst✝ : MulHomClass F α α₂
f : F
x y : SkewMonoidAlgebra β α
hf : ∀ (a : α) (x : β), a • x = f a • x
⊢ (x.sum fun a b ↦ y.sum fun a₂ b₂ ↦ (mapDomain ⇑f) (single (a * a₂) (b * a • b₂))) =
    ((mapDomain ⇑f) x).sum fun a₁ b₁ ↦ ((mapDomain ⇑f) y).sum fun a₂ b₂ ↦ single (a₁ * a₂) (b₁ * a₁ • b₂)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: α : Type u_3
α₂ : Type u_4
β : Type u_5
F : Type u_6
inst✝⁶ : Semiring β
inst✝⁵ : Monoid α
inst✝⁴ : Monoid α₂
inst✝³ : FunLike F α α₂
inst✝² : MulSemiringAction α β
inst✝¹ : MulSemiringAction α₂ β
inst✝ : MulHomClass F α α₂
f : F
x y : SkewMonoidAlgebra β α
hf : ∀ (a : α) (x : β), a • x = f a • x
⊢ (mapDomain ⇑f) (x * y) = (mapDomain ⇑f) x * (mapDomain ⇑f) y

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Monoid G
inst✝ : MulSemiringAction G k
a b : G
⊢ single (a * b) 1 = single a 1 * single b 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Monoid G
inst✝ : MulSemiringAction G k
a : G
⊢ (of k G) a = single a 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Monoid G
inst✝ : MulSemiringAction G k
g : G
r : k
⊢ r • (of k G) g = single g r

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝³ : Semiring k
inst✝² : Monoid G
inst✝¹ : MulSemiringAction G k
inst✝ : Nontrivial k
a b : G
h : (of k G) a = (of k G) b
⊢ a = b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : MulOneClass G
R : Type u_3
inst✝ : Semiring R
f : k →+* R
g : G →* R
c : k
φ : SkewMonoidAlgebra k G
this : (liftNC ↑f ⇑g).comp ((smulAddHom k (SkewMonoidAlgebra k G)) c) = (AddMonoidHom.mulLeft (f c)).comp (liftNC ↑f ⇑g)
⊢ (liftNC ↑f ⇑g) (c • φ) = f c * (liftNC ↑f ⇑g) φ

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : MulOneClass G
R : Type u_3
inst✝ : Semiring R
f : k →+* R
g : G →* R
c : k
φ : SkewMonoidAlgebra k G
⊢ (liftNC ↑f ⇑g) (c • φ) = f c * (liftNC ↑f ⇑g) φ

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝³ : Semiring k
inst✝² : Monoid G
inst✝¹ : MulSemiringAction G k
inst✝ : IsScalarTower k k k
t : k
a b : SkewMonoidAlgebra k G
⊢ (t • a) • b = t • a • b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: k✝ : Type u_1
G : Type u_2
R : Type u_3
M : Type u_4
N : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid N
inst✝ : DistribMulAction R M
α : Type u_6
a : α
k : R
m : M
⊢ (↑(singleAddHom a)).toFun (k • m) = (MonoidHom.id R) k • (↑(singleAddHom a)).toFun m

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
A : Type u_6
inst✝⁴ : NonUnitalNonAssocSemiring A
inst✝³ : Monoid G
inst✝² : Semiring k
inst✝¹ : MulSemiringAction G k
inst✝ : DistribMulAction k A
φ₁ φ₂ : SkewMonoidAlgebra k G →ₙₐ[k] A
h : ∀ (x : G), φ₁ (single x 1) = φ₂ (single x 1)
⊢ φ₁ = φ₂

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝⁵ : Monoid G
inst✝⁴ : CommSemiring k
A : Type u_3
inst✝³ : Semiring A
inst✝² : Algebra k A
inst✝¹ : MulSemiringAction G A
inst✝ : SMulCommClass G k A
r : k
f : SkewMonoidAlgebra A G
⊢ (singleOneRingHom.comp (algebraMap k A)) r * f = f * (singleOneRingHom.comp (algebraMap k A)) r

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝⁵ : Monoid G
inst✝⁴ : CommSemiring k
A : Type u_3
inst✝³ : Semiring A
inst✝² : Algebra k A
inst✝¹ : MulSemiringAction G A
inst✝ : SMulCommClass G k A
r : k
a : SkewMonoidAlgebra A G
⊢ r • a = (singleOneRingHom.comp (algebraMap k A)) r * a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝³ : Monoid G
inst✝² : CommSemiring k
inst✝¹ : MulSemiringAction G k
inst✝ : SMulCommClass G k k
a : G
b : k
⊢ single a b = (algebraMap k (SkewMonoidAlgebra k G)) b * (of k G) a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝⁵ : Monoid G
inst✝⁴ : CommSemiring k
A : Type u_3
inst✝³ : Semiring A
inst✝² : Algebra k A
a : G
b : k
inst✝¹ : MulSemiringAction G A
inst✝ : SMulCommClass G k A
⊢ single a ((algebraMap k A) b) = (algebraMap k (SkewMonoidAlgebra A G)) b * (of A G) a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Star.LinearMap

Goal state before:
pp: R : Type u_1
E : Type u_2
F : Type u_3
inst✝⁹ : Semiring R
inst✝⁸ : InvolutiveStar R
inst✝⁷ : AddCommMonoid E
inst✝⁶ : Module R E
inst✝⁵ : StarAddMonoid E
inst✝⁴ : StarModule R E
inst✝³ : AddCommMonoid F
inst✝² : Module R F
inst✝¹ : StarAddMonoid F
inst✝ : StarModule R F
f : WithConv (E →ₗ[R] F)
⊢ ∀ (x y : E), star (f.ofConv (star (x + y))) = star (f.ofConv (star x)) + star (f.ofConv (star y))

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Star.LinearMap

Goal state before:
pp: R : Type u_1
E : Type u_2
F : Type u_3
inst✝⁹ : Semiring R
inst✝⁸ : InvolutiveStar R
inst✝⁷ : AddCommMonoid E
inst✝⁶ : Module R E
inst✝⁵ : StarAddMonoid E
inst✝⁴ : StarModule R E
inst✝³ : AddCommMonoid F
inst✝² : Module R F
inst✝¹ : StarAddMonoid F
inst✝ : StarModule R F
f : WithConv (E →ₗ[R] F)
⊢ ∀ (m : R) (x : E), star (f.ofConv (star (m • x))) = (RingHom.id R) m • star (f.ofConv (star x))

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Star.LinearMap

Goal state before:
pp: R : Type u_1
E : Type u_2
F : Type u_3
inst✝⁹ : Semiring R
inst✝⁸ : InvolutiveStar R
inst✝⁷ : AddCommMonoid E
inst✝⁶ : Module R E
inst✝⁵ : StarAddMonoid E
inst✝⁴ : StarModule R E
inst✝³ : AddCommMonoid F
inst✝² : Module R F
inst✝¹ : StarAddMonoid F
inst✝ : StarModule R F
x : WithConv (E →ₗ[R] F)
⊢ star (star x) = x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Star.LinearMap

Goal state before:
pp: R : Type u_1
E : Type u_2
F : Type u_3
inst✝⁹ : Semiring R
inst✝⁸ : InvolutiveStar R
inst✝⁷ : AddCommMonoid E
inst✝⁶ : Module R E
inst✝⁵ : StarAddMonoid E
inst✝⁴ : StarModule R E
inst✝³ : AddCommMonoid F
inst✝² : Module R F
inst✝¹ : StarAddMonoid F
inst✝ : StarModule R F
x y : WithConv (E →ₗ[R] F)
⊢ star (x + y) = star x + star y

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Star.LinearMap

Goal state before:
pp: R : Type u_1
E : Type u_2
F : Type u_3
inst✝⁹ : Semiring R
inst✝⁸ : InvolutiveStar R
inst✝⁷ : AddCommMonoid E
inst✝⁶ : Module R E
inst✝⁵ : StarAddMonoid E
inst✝⁴ : StarModule R E
inst✝³ : AddCommMonoid F
inst✝² : Module R F
inst✝¹ : StarAddMonoid F
inst✝ : StarModule R F
f : WithConv (E →ₗ[R] F)
⊢ IsSelfAdjoint f ↔ ∀ (x : E), f.ofConv (star x) = star (f.ofConv x)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Star.LinearMap

Goal state before:
pp: R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹³ : Semiring R
inst✝¹² : InvolutiveStar R
inst✝¹¹ : AddCommMonoid E
inst✝¹⁰ : Module R E
inst✝⁹ : StarAddMonoid E
inst✝⁸ : StarModule R E
inst✝⁷ : AddCommMonoid F
inst✝⁶ : Module R F
inst✝⁵ : StarAddMonoid F
inst✝⁴ : StarModule R F
G : Type u_4
inst✝³ : AddCommMonoid G
inst✝² : Module R G
inst✝¹ : StarAddMonoid G
inst✝ : StarModule R G
f : WithConv (E →ₗ[R] F)
g : WithConv (G →ₗ[R] E)
⊢ star (toConv (f.ofConv ∘ₗ g.ofConv)) = toConv ((star f).ofConv ∘ₗ (star g).ofConv)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Star.LinearMap

Goal state before:
pp: R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹³ : Semiring R
inst✝¹² : InvolutiveStar R
inst✝¹¹ : AddCommMonoid E
inst✝¹⁰ : Module R E
inst✝⁹ : StarAddMonoid E
inst✝⁸ : StarModule R E
inst✝⁷ : AddCommMonoid F
inst✝⁶ : Module R F
inst✝⁵ : StarAddMonoid F
inst✝⁴ : StarModule R F
G : Type u_4
inst✝³ : AddCommMonoid G
inst✝² : Module R G
inst✝¹ : StarAddMonoid G
inst✝ : StarModule R G
f : E →ₗ[R] F
g : G →ₗ[R] E
⊢ star (toConv (f ∘ₗ g)) = toConv ((star (toConv f)).ofConv ∘ₗ (star (toConv g)).ofConv)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Star.LinearMap

Goal state before:
pp: R : Type u_1
E : Type u_2
inst✝⁵ : Semiring R
inst✝⁴ : InvolutiveStar R
inst✝³ : AddCommMonoid E
inst✝² : Module R E
inst✝¹ : StarAddMonoid E
inst✝ : StarModule R E
⊢ star (toConv id) = toConv id

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Star.LinearMap

Goal state before:
pp: R : Type u_1
E : Type u_2
F : Type u_3
inst✝⁹ : Semiring R
inst✝⁸ : InvolutiveStar R
inst✝⁷ : AddCommMonoid E
inst✝⁶ : Module R E
inst✝⁵ : StarAddMonoid E
inst✝⁴ : StarModule R E
inst✝³ : AddCommMonoid F
inst✝² : Module R F
inst✝¹ : StarAddMonoid F
inst✝ : StarModule R F
⊢ star 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Star.LinearMap

Goal state before:
pp: R : Type u_1
inst✝⁷ : Semiring R
inst✝⁶ : InvolutiveStar R
E : Type u_6
inst✝⁵ : NonUnitalNonAssocSemiring E
inst✝⁴ : StarRing E
inst✝³ : Module R E
inst✝² : StarModule R E
inst✝¹ : SMulCommClass R E E
inst✝ : IsScalarTower R E E
x : E
⊢ star (toConv (mulLeft R x)) = toConv (mulRight R (star x))

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Star.LinearMap

Goal state before:
pp: R : Type u_1
inst✝⁷ : Semiring R
inst✝⁶ : InvolutiveStar R
E : Type u_6
inst✝⁵ : NonUnitalNonAssocSemiring E
inst✝⁴ : StarRing E
inst✝³ : Module R E
inst✝² : StarModule R E
inst✝¹ : SMulCommClass R E E
inst✝ : IsScalarTower R E E
x : E
⊢ star (toConv (mulRight R x)) = toConv (mulLeft R (star x))

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Star.LinearMap

Goal state before:
pp: R' : Type u_5
E : Type u_6
inst✝⁷ : CommSemiring R'
inst✝⁶ : StarRing R'
inst✝⁵ : NonUnitalNonAssocSemiring E
inst✝⁴ : StarRing E
inst✝³ : Module R' E
inst✝² : StarModule R' E
inst✝¹ : SMulCommClass R' E E
inst✝ : IsScalarTower R' E E
x✝¹ x✝ : E
⊢ (star (toConv (mul' R' E))).ofConv (x✝¹ ⊗ₜ[R'] x✝) =
    (toConv (mul' R' E ∘ₗ ↑(TensorProduct.comm R' E E))).ofConv (x✝¹ ⊗ₜ[R'] x✝)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Star.LinearMap

Goal state before:
pp: R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹⁴ : Semiring R
inst✝¹³ : InvolutiveStar R
inst✝¹² : AddCommMonoid E
inst✝¹¹ : Module R E
inst✝¹⁰ : StarAddMonoid E
inst✝⁹ : StarModule R E
inst✝⁸ : AddCommMonoid F
inst✝⁷ : Module R F
inst✝⁶ : StarAddMonoid F
inst✝⁵ : StarModule R F
G : Type u_4
inst✝⁴ : AddCommMonoid G
inst✝³ : Module R G
inst✝² : StarAddMonoid G
inst✝¹ : StarModule R G
inst✝ : SMulCommClass R R F
x✝¹ : R
x✝ : WithConv (E →ₗ[R] F)
⊢ star (x✝¹ • x✝) = star x✝¹ • star x✝

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Star.LinearMap

Goal state before:
pp: R : Type u_5
E : Type u_6
F : Type u_7
G : Type u_8
H : Type u_9
inst✝¹⁷ : CommSemiring R
inst✝¹⁶ : StarRing R
inst✝¹⁵ : AddCommMonoid E
inst✝¹⁴ : StarAddMonoid E
inst✝¹³ : Module R E
inst✝¹² : StarModule R E
inst✝¹¹ : AddCommMonoid F
inst✝¹⁰ : StarAddMonoid F
inst✝⁹ : Module R F
inst✝⁸ : StarModule R F
inst✝⁷ : AddCommMonoid G
inst✝⁶ : StarAddMonoid G
inst✝⁵ : Module R G
inst✝⁴ : StarModule R G
inst✝³ : AddCommMonoid H
inst✝² : StarAddMonoid H
inst✝¹ : Module R H
inst✝ : StarModule R H
f : WithConv (E →ₗ[R] F)
g : WithConv (G →ₗ[R] H)
x✝¹ : E
x✝ : G
⊢ (star (toConv (TensorProduct.map f.ofConv g.ofConv))).ofConv (x✝¹ ⊗ₜ[R] x✝) =
    (toConv (TensorProduct.map (star f).ofConv (star g).ofConv)).ofConv (x✝¹ ⊗ₜ[R] x✝)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Symmetrized

Goal state before:
pp: α : Type u_1
inst✝¹ : Ring α
inst✝ : Invertible 2
a b : αˢʸᵐ
⊢ a * b * (a * a) = a * (b * (a * a))

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Star.LinearMap

Goal state before:
pp: R : Type u_5
E : Type u_6
F : Type u_7
G : Type u_8
H : Type u_9
inst✝¹⁷ : CommSemiring R
inst✝¹⁶ : StarRing R
inst✝¹⁵ : AddCommMonoid E
inst✝¹⁴ : StarAddMonoid E
inst✝¹³ : Module R E
inst✝¹² : StarModule R E
inst✝¹¹ : AddCommMonoid F
inst✝¹⁰ : StarAddMonoid F
inst✝⁹ : Module R F
inst✝⁸ : StarModule R F
inst✝⁷ : AddCommMonoid G
inst✝⁶ : StarAddMonoid G
inst✝⁵ : Module R G
inst✝⁴ : StarModule R G
inst✝³ : AddCommMonoid H
inst✝² : StarAddMonoid H
inst✝¹ : Module R H
inst✝ : StarModule R H
f : WithConv (E →ₗ[R] F)
g : WithConv (G →ₗ[R] H)
x : TensorProduct R E G
⊢ star ((TensorProduct.map f.ofConv g.ofConv) x) = (TensorProduct.map (star f).ofConv (star g).ofConv) (star x)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Star.LinearMap

Goal state before:
pp: R : Type u_5
E : Type u_6
F : Type u_7
G : Type u_8
inst✝¹³ : CommSemiring R
inst✝¹² : StarRing R
inst✝¹¹ : AddCommMonoid E
inst✝¹⁰ : StarAddMonoid E
inst✝⁹ : Module R E
inst✝⁸ : StarModule R E
inst✝⁷ : AddCommMonoid F
inst✝⁶ : StarAddMonoid F
inst✝⁵ : Module R F
inst✝⁴ : StarModule R F
inst✝³ : AddCommMonoid G
inst✝² : StarAddMonoid G
inst✝¹ : Module R G
inst✝ : StarModule R G
f : WithConv (F →ₗ[R] G)
⊢ star (toConv (lTensor E f.ofConv)) = toConv (lTensor E (star f).ofConv)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Star.LinearMap

Goal state before:
pp: R : Type u_5
E : Type u_6
F : Type u_7
G : Type u_8
inst✝¹³ : CommSemiring R
inst✝¹² : StarRing R
inst✝¹¹ : AddCommMonoid E
inst✝¹⁰ : StarAddMonoid E
inst✝⁹ : Module R E
inst✝⁸ : StarModule R E
inst✝⁷ : AddCommMonoid F
inst✝⁶ : StarAddMonoid F
inst✝⁵ : Module R F
inst✝⁴ : StarModule R F
inst✝³ : AddCommMonoid G
inst✝² : StarAddMonoid G
inst✝¹ : Module R G
inst✝ : StarModule R G
f : WithConv (E →ₗ[R] F)
⊢ star (toConv (rTensor G f.ofConv)) = toConv (rTensor G (star f).ofConv)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Star.LinearMap

Goal state before:
pp: E : Type u_2
inst✝⁶ : AddCommMonoid E
inst✝⁵ : StarAddMonoid E
S : Type u_5
inst✝⁴ : Semiring S
inst✝³ : StarAddMonoid S
inst✝² : StarModule S S
inst✝¹ : Module S E
inst✝ : StarModule S E
a : E
⊢ star (toConv (toSpanSingleton S E a)) = toConv (toSpanSingleton S E (star a))

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Star.LinearMap

Goal state before:
pp: E : Type u_2
F : Type u_3
inst✝¹⁰ : AddCommMonoid E
inst✝⁹ : StarAddMonoid E
inst✝⁸ : AddCommMonoid F
inst✝⁷ : StarAddMonoid F
S : Type u_5
inst✝⁶ : Semiring S
inst✝⁵ : StarAddMonoid S
inst✝⁴ : StarModule S S
inst✝³ : Module S E
inst✝² : StarModule S E
inst✝¹ : Module S F
inst✝ : StarModule S F
f : WithConv (E →ₗ[S] S)
x : F
⊢ star (toConv (f.ofConv.smulRight x)) = toConv ((star f).ofConv.smulRight (star x))

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Star.LinearMap

Goal state before:
pp: R : Type u_5
A : Type u_6
C : Type u_7
inst✝¹² : CommSemiring R
inst✝¹¹ : StarRing R
inst✝¹⁰ : NonUnitalNonAssocSemiring A
inst✝⁹ : Module R A
inst✝⁸ : SMulCommClass R A A
inst✝⁷ : IsScalarTower R A A
inst✝⁶ : StarRing A
inst✝⁵ : StarModule R A
inst✝⁴ : AddCommMonoid C
inst✝³ : Module R C
inst✝² : StarAddMonoid C
inst✝¹ : StarModule R C
inst✝ : CoalgebraStruct R C
h : star (toConv comul) = toConv (↑(TensorProduct.comm R C C) ∘ₗ comul)
f g : WithConv (C →ₗ[R] A)
⊢ star (f * g) = star g * star f

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Star.LinearMap

Goal state before:
pp: R : Type u_5
inst✝⁶ : CommSemiring R
inst✝⁵ : StarRing R
n : Type u_8
inst✝⁴ : DecidableEq n
B : n → Type u_9
inst✝³ : (i : n) → AddCommMonoid (B i)
inst✝² : (i : n) → Module R (B i)
inst✝¹ : (i : n) → StarAddMonoid (B i)
inst✝ : ∀ (i : n), StarModule R (B i)
i : n
⊢ star (toConv (single R B i)) = toConv (single R B i)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Star.LinearMap

Goal state before:
pp: R : Type u_5
inst✝⁸ : CommSemiring R
inst✝⁷ : StarRing R
n : Type u_8
inst✝⁶ : DecidableEq n
B : n → Type u_9
inst✝⁵ : (i : n) → AddCommMonoid (B i)
inst✝⁴ : (i : n) → Module R (B i)
inst✝³ : (i : n) → StarAddMonoid (B i)
inst✝² : ∀ (i : n), StarModule R (B i)
inst✝¹ : Fintype n
inst✝ : (i : n) → CoalgebraStruct R (B i)
h : ∀ (i : n), star (toConv comul) = toConv (↑(TensorProduct.comm R (B i) (B i)) ∘ₗ comul)
i : n
x : B i
⊢ ?m.178

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Vertex.VertexOperator

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
x✝¹ x✝ : VertexOperator R V
⊢ (fun n ↦ coeff (x✝¹ + x✝) (-n - 1)) = (fun n ↦ coeff x✝¹ (-n - 1)) + fun n ↦ coeff x✝ (-n - 1)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Vertex.VertexOperator

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
x✝¹ : R
x✝ : VertexOperator R V
⊢ (fun n ↦ coeff (x✝¹ • x✝) (-n - 1)) = (RingHom.id R) x✝¹ • fun n ↦ coeff x✝ (-n - 1)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Vertex.VertexOperator

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
A : VertexOperator R V
n : ℤ
⊢ coeff A n = ncoeff A (-n - 1)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Vertex.VertexOperator

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
A : VertexOperator R V
n : ℤ
x : V
h : -n - 1 < ((HahnModule.of R).symm (A x)).order
⊢ (ncoeff A n) x = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Vertex.VertexOperator

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
A : VertexOperator R V
n : ℤ
x : V
h : n < ((HahnModule.of R).symm (A x)).order
⊢ (coeff A n) x = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Vertex.VertexOperator

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
f : ℤ → Module.End R V
hf : ∀ (x : V), BddBelow (Function.support fun y ↦ (f y) x)
x : V
n : ℤ
⊢ ((HahnModule.of R).symm ((of_coeff f hf) x)).coeff n = (f n) x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Tropical.Lattice

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝ : ConditionallyCompleteLinearOrder R
⊢ ∀ (s : Set (Tropical R)), ¬BddAbove s → sSup s = sSup ∅

Tactic:
by

Goal state after: