mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Star.UnitaryStarAlgAut

Goal state before:
pp: S : Type u_1
R : Type u_2
inst✝⁴ : Semiring R
inst✝³ : StarMul R
inst✝² : SMul S R
inst✝¹ : IsScalarTower S R R
inst✝ : SMulCommClass S R R
g h : ↥(unitary R)
⊢ (let __RingEquiv := (MulSemiringAction.toRingEquiv (ConjAct Rˣ) R) (ConjAct.toConjAct (toUnits (g * h)));
    { toRingEquiv := __RingEquiv, map_star' := ⋯, map_smul' := ⋯ }) =
    (let __RingEquiv := (MulSemiringAction.toRingEquiv (ConjAct Rˣ) R) (ConjAct.toConjAct (toUnits g));
      { toRingEquiv := __RingEquiv, map_star' := ⋯, map_smul' := ⋯ }) *
      let __RingEquiv := (MulSemiringAction.toRingEquiv (ConjAct Rˣ) R) (ConjAct.toConjAct (toUnits h));
      { toRingEquiv := __RingEquiv, map_star' := ⋯, map_smul' := ⋯ }

Tactic:
ext

Goal state after:
S : Type u_1
R : Type u_2
inst✝⁴ : Semiring R
inst✝³ : StarMul R
inst✝² : SMul S R
inst✝¹ : IsScalarTower S R R
inst✝ : SMulCommClass S R R
g h : ↥(unitary R)
a✝ : R
⊢ (let __RingEquiv := (MulSemiringAction.toRingEquiv (ConjAct Rˣ) R) (ConjAct.toConjAct (toUnits (g * h)));
      { toRingEquiv := __RingEquiv, map_star' := ⋯, map_smul' := ⋯ })
      a✝ =
    ((let __RingEquiv := (MulSemiringAction.toRingEquiv (ConjAct Rˣ) R) (ConjAct.toConjAct (toUnits g));
        { toRingEquiv := __RingEquiv, map_star' := ⋯, map_smul' := ⋯ }) *
        let __RingEquiv := (MulSemiringAction.toRingEquiv (ConjAct Rˣ) R) (ConjAct.toConjAct (toUnits h));
        { toRingEquiv := __RingEquiv, map_star' := ⋯, map_smul' := ⋯ })
      a✝
Module: Mathlib.Algebra.Star.UnitaryStarAlgAut

Goal state before:
pp: S : Type u_1
R : Type u_2
inst✝⁴ : Semiring R
inst✝³ : StarMul R
inst✝² : SMul S R
inst✝¹ : IsScalarTower S R R
inst✝ : SMulCommClass S R R
u : ↥(unitary R)
⊢ ((conjStarAlgAut S R) u).symm = (conjStarAlgAut S R) (star u)

Tactic:
ext

Goal state after:
S : Type u_1
R : Type u_2
inst✝⁴ : Semiring R
inst✝³ : StarMul R
inst✝² : SMul S R
inst✝¹ : IsScalarTower S R R
inst✝ : SMulCommClass S R R
u : ↥(unitary R)
a✝ : R
⊢ ((conjStarAlgAut S R) u).symm a✝ = ((conjStarAlgAut S R) (star u)) a✝
Module: Mathlib.Algebra.Star.UnitaryStarAlgAut

Goal state before:
pp: R : Type u_3
S : Type u_4
inst✝⁸ : Ring R
inst✝⁷ : StarMul R
inst✝⁶ : CommRing S
inst✝⁵ : StarMul S
inst✝⁴ : Algebra S R
inst✝³ : StarModule S R
inst✝² : Algebra.IsCentral S R
inst✝¹ : IsCancelMulZero S
inst✝ : Module.IsTorsionFree S R
u v : ↥(unitary R)
x✝ : ∃ y, y • 1 = star ↑v * ↑u
y : S
h : y • 1 = star ↑v * ↑u
huv : ↑u = y • ↑v
hvu : ↑v = star y • ↑u
this : star y * y = 1
⊢ u = ⟨y, ⋯⟩ • v

Tactic:
ext

Goal state after:
R : Type u_3
S : Type u_4
inst✝⁸ : Ring R
inst✝⁷ : StarMul R
inst✝⁶ : CommRing S
inst✝⁵ : StarMul S
inst✝⁴ : Algebra S R
inst✝³ : StarModule S R
inst✝² : Algebra.IsCentral S R
inst✝¹ : IsCancelMulZero S
inst✝ : Module.IsTorsionFree S R
u v : ↥(unitary R)
x✝ : ∃ y, y • 1 = star ↑v * ↑u
y : S
h : y • 1 = star ↑v * ↑u
huv : ↑u = y • ↑v
hvu : ↑v = star y • ↑u
this : star y * y = 1
⊢ ↑u = ↑(⟨y, ⋯⟩ • v)
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
S : Type u_3
S₁ : Type u_4
S₂ : Type u_5
M : Type u_6
α : Type u_7
inst✝³ : Monoid G
inst✝² : AddCommMonoid M
inst✝¹ : MulAction G α
inst✝ : AddCommMonoid k
g : G
⊢ g • 0 = 0

Tactic:
ext

Goal state after:
k : Type u_1
G : Type u_2
S : Type u_3
S₁ : Type u_4
S₂ : Type u_5
M : Type u_6
α : Type u_7
inst✝³ : Monoid G
inst✝² : AddCommMonoid M
inst✝¹ : MulAction G α
inst✝ : AddCommMonoid k
g a✝ : G
⊢ (g • 0).coeff a✝ = (coeff 0) a✝
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
S : Type u_3
S₁ : Type u_4
S₂ : Type u_5
M : Type u_6
α : Type u_7
inst✝³ : Monoid G
inst✝² : AddCommMonoid M
inst✝¹ : MulAction G α
inst✝ : AddCommMonoid k
g : G
f f' : SkewMonoidAlgebra k G
⊢ g • (f + f') = g • f + g • f'

Tactic:
ext

Goal state after:
k : Type u_1
G : Type u_2
S : Type u_3
S₁ : Type u_4
S₂ : Type u_5
M : Type u_6
α : Type u_7
inst✝³ : Monoid G
inst✝² : AddCommMonoid M
inst✝¹ : MulAction G α
inst✝ : AddCommMonoid k
g : G
f f' : SkewMonoidAlgebra k G
a✝ : G
⊢ (g • (f + f')).coeff a✝ = (g • f + g • f').coeff a✝
Module: Mathlib.Algebra.Star.UnitaryStarAlgAut

Goal state before:
pp: R : Type u_3
S : Type u_4
inst✝⁸ : Ring R
inst✝⁷ : StarMul R
inst✝⁶ : CommRing S
inst✝⁵ : StarMul S
inst✝⁴ : Algebra S R
inst✝³ : StarModule S R
inst✝² : Algebra.IsCentral S R
inst✝¹ : IsCancelMulZero S
inst✝ : Module.IsTorsionFree S R
u v : ↥(unitary R)
x✝ : ∃ y, y • 1 = star ↑v * ↑u
y : S
h : y • 1 = star ↑v * ↑u
huv : ↑u = y • ↑v
hvu : ↑v = star y • ↑u
this : ↑v = 0
⊢ u = 1 • v

Tactic:
ext

Goal state after:
R : Type u_3
S : Type u_4
inst✝⁸ : Ring R
inst✝⁷ : StarMul R
inst✝⁶ : CommRing S
inst✝⁵ : StarMul S
inst✝⁴ : Algebra S R
inst✝³ : StarModule S R
inst✝² : Algebra.IsCentral S R
inst✝¹ : IsCancelMulZero S
inst✝ : Module.IsTorsionFree S R
u v : ↥(unitary R)
x✝ : ∃ y, y • 1 = star ↑v * ↑u
y : S
h : y • 1 = star ↑v * ↑u
huv : ↑u = y • ↑v
hvu : ↑v = star y • ↑u
this : ↑v = 0
⊢ ↑u = ↑(1 • v)
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: case e_g
k : Type u_1
G : Type u_2
inst✝³ : Semiring k
inst✝² : Mul G
inst✝¹ : SMulZeroClass G k
inst✝ : DecidableEq G
f g : SkewMonoidAlgebra k G
x : G
⊢ (fun a₁ b ↦ (g.sum fun a₂ b₂ ↦ single (a₁ * a₂) (b * a₁ • b₂)).coeff x) = fun a₁ b₁ ↦
    g.sum fun a₂ b₂ ↦ if a₁ * a₂ = x then b₁ * a₁ • b₂ else 0

Tactic:
ext

Goal state after:
case e_g
k : Type u_1
G : Type u_2
inst✝³ : Semiring k
inst✝² : Mul G
inst✝¹ : SMulZeroClass G k
inst✝ : DecidableEq G
f g : SkewMonoidAlgebra k G
x x✝¹ : G
x✝ : k
⊢ (g.sum fun a₂ b₂ ↦ single (x✝¹ * a₂) (x✝ * x✝¹ • b₂)).coeff x =
    g.sum fun a₂ b₂ ↦ if x✝¹ * a₂ = x then x✝ * x✝¹ • b₂ else 0
Module: Mathlib.Algebra.Star.UnitaryStarAlgAut

Goal state before:
pp: case inr
R : Type u_3
S : Type u_4
inst✝⁸ : Ring R
inst✝⁷ : StarMul R
inst✝⁶ : CommRing S
inst✝⁵ : StarMul S
inst✝⁴ : Algebra S R
inst✝³ : StarModule S R
inst✝² : Algebra.IsCentral S R
inst✝¹ : IsCancelMulZero S
inst✝ : Module.IsTorsionFree S R
u v : ↥(unitary R)
x✝ : ∃ y, y • 1 = star ↑v * ↑u
y : S
h : y • 1 = star ↑v * ↑u
huv : ↑u = y • ↑v
hvu : ↑v = star y • ↑u
this : ↑v = 0
⊢ ∃ α, u = α • v

Tactic:
· exact ⟨1, by ext; simp [this, huv] at huv ⊢⟩

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

Goal state before:
pp: case e_g.e_g
k : Type u_1
G : Type u_2
inst✝³ : Semiring k
inst✝² : Mul G
inst✝¹ : SMulZeroClass G k
inst✝ : DecidableEq G
f g : SkewMonoidAlgebra k G
x x✝¹ : G
x✝ : k
⊢ (fun a₁ b ↦ (single (x✝¹ * a₁) (x✝ * x✝¹ • b)).coeff x) = fun a₂ b₂ ↦ if x✝¹ * a₂ = x then x✝ * x✝¹ • b₂ else 0

Tactic:
ext

Goal state after:
case e_g.e_g
k : Type u_1
G : Type u_2
inst✝³ : Semiring k
inst✝² : Mul G
inst✝¹ : SMulZeroClass G k
inst✝ : DecidableEq G
f g : SkewMonoidAlgebra k G
x x✝³ : G
x✝² : k
x✝¹ : G
x✝ : k
⊢ (single (x✝³ * x✝¹) (x✝² * x✝³ • x✝)).coeff x = if x✝³ * x✝¹ = x then x✝² * x✝³ • x✝ else 0
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : SMulZeroClass G k
f g : SkewMonoidAlgebra k G
x : G
s : Finset (G × G)
hs : ∀ {p : G × G}, p ∈ s ↔ p.1 * p.2 = x
F : G × G → k := fun p ↦ if p.1 * p.2 = x then f.coeff p.1 * p.1 • g.coeff p.2 else 0
⊢ {p ∈ f.support ×ˢ g.support | p.1 * p.2 = x} = {p ∈ s | p.1 ∈ f.support ∧ p.2 ∈ g.support}

Tactic:
ext

Goal state after:
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : SMulZeroClass G k
f g : SkewMonoidAlgebra k G
x : G
s : Finset (G × G)
hs : ∀ {p : G × G}, p ∈ s ↔ p.1 * p.2 = x
F : G × G → k := fun p ↦ if p.1 * p.2 = x then f.coeff p.1 * p.1 • g.coeff p.2 else 0
a✝ : G × G
⊢ a✝ ∈ {p ∈ f.support ×ˢ g.support | p.1 * p.2 = x} ↔ a✝ ∈ {p ∈ s | p.1 ∈ f.support ∧ p.2 ∈ g.support}
Module: Mathlib.Algebra.Tropical.Basic

Goal state before:
pp: R : Type u
inst✝ : LinearOrder R
a b : Tropical (WithTop R)
⊢ a = 0 ∧ a ≤ b ∨ b = 0 ∧ b ≤ a ↔ a = 0 ∧ b = 0

Tactic:
constructor

Goal state after:
case mp
R : Type u
inst✝ : LinearOrder R
a b : Tropical (WithTop R)
⊢ a = 0 ∧ a ≤ b ∨ b = 0 ∧ b ≤ a → a = 0 ∧ b = 0

case mpr
R : Type u
inst✝ : LinearOrder R
a b : Tropical (WithTop R)
⊢ a = 0 ∧ b = 0 → a = 0 ∧ a ≤ b ∨ b = 0 ∧ b ≤ a
Module: Mathlib.Algebra.Symmetrized

Goal state before:
pp: α : Type u_1
inst✝¹ : Semiring α
inst✝ : Invertible 2
x✝ : αˢʸᵐ
⊢ 1 * x✝ = x✝

Tactic:
rw [mul_def, unsym_one, mul_one, one_mul, ← two_mul, invOf_mul_cancel_left, sym_unsym]

Goal state after:
Module: Mathlib.Algebra.Symmetrized

Goal state before:
pp: α : Type u_1
inst✝¹ : Semiring α
inst✝ : Invertible 2
x✝ : αˢʸᵐ
⊢ x✝ * 1 = x✝

Tactic:
rw [mul_def, unsym_one, mul_one, one_mul, ← two_mul, invOf_mul_cancel_left, sym_unsym]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : LinearOrder R
inst✝ : OrderTop R
s : Finset S
f : S → R
⊢ trop (s.inf f) = ∑ i ∈ s, trop (f i)

Tactic:
convert! Multiset.trop_inf (s.val.map f)

Goal state after:
case e'_3
R : Type u_1
S : Type u_2
inst✝¹ : LinearOrder R
inst✝ : OrderTop R
s : Finset S
f : S → R
⊢ ∑ i ∈ s, trop (f i) = (Multiset.map trop (Multiset.map f s.val)).sum
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)
a : G
⊢ (↑φ₁).comp (DistribMulActionHom.single a) = (↑φ₂).comp (DistribMulActionHom.single a)

Tactic:
ext

Goal state after:
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)
a : G
⊢ ((↑φ₁).comp (DistribMulActionHom.single a)) 1 = ((↑φ₂).comp (DistribMulActionHom.single a)) 1
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:
ext

Goal state after:
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
a✝ : G
⊢ ((singleOneRingHom.comp (algebraMap k A)) r * f).coeff a✝ = (f * (singleOneRingHom.comp (algebraMap k A)) r).coeff a✝
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:
ext

Goal state after:
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
a✝ : G
⊢ (r • a).coeff a✝ = ((singleOneRingHom.comp (algebraMap k A)) r * a).coeff a✝
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:
ext

Goal state after:
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)
x✝ : E
⊢ (star (star x)).ofConv x✝ = x.ofConv x✝
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:
ext

Goal state after:
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)
x✝ : E
⊢ (star (x + y)).ofConv x✝ = (star x + star y).ofConv x✝
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:
ext

Goal state after:
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)
x✝ : G
⊢ (star (toConv (f.ofConv ∘ₗ g.ofConv))).ofConv x✝ = (toConv ((star f).ofConv ∘ₗ (star g).ofConv)).ofConv x✝
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:
ext

Goal state after:
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
x✝ : E
⊢ (star (toConv id)).ofConv x✝ = (toConv id).ofConv x✝
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:
ext

Goal state after:
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 x✝ : E
⊢ (star (toConv (mulLeft R x))).ofConv x✝ = (toConv (mulRight R (star x))).ofConv x✝
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:
ext

Goal state after:
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)
x✝ : E
⊢ (star (x✝² • x✝¹)).ofConv x✝ = (star x✝² • star x✝¹).ofConv x✝
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:
ext

Goal state after:
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)
x✝¹ : E
x✝ : F
⊢ ((TensorProduct.AlgebraTensorModule.curry (star (toConv (lTensor E f.ofConv))).ofConv) x✝¹) x✝ =
    ((TensorProduct.AlgebraTensorModule.curry (toConv (lTensor E (star f).ofConv)).ofConv) x✝¹) x✝
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:
ext

Goal state after:
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)
x✝¹ : E
x✝ : G
⊢ ((TensorProduct.AlgebraTensorModule.curry (star (toConv (rTensor G f.ofConv))).ofConv) x✝¹) x✝ =
    ((TensorProduct.AlgebraTensorModule.curry (toConv (rTensor G (star f).ofConv)).ofConv) x✝¹) x✝
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:
ext

Goal state after:
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))).ofConv 1 = (toConv (toSpanSingleton S E (star a))).ofConv 1
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:
ext

Goal state after:
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
x✝ : E
⊢ (star (toConv (f.ofConv.smulRight x))).ofConv x✝ = (toConv ((star f).ofConv.smulRight (star x))).ofConv x✝
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)
⊢ toConv
      ((mul' R A ∘ₗ ↑(TensorProduct.comm R A A)) ∘ₗ
        (↑(TensorProduct.comm R A A) ∘ₗ TensorProduct.map (star g).ofConv (star f).ofConv) ∘ₗ comul) =
    toConv (mul' R A ∘ₗ TensorProduct.map (star g).ofConv (star f).ofConv ∘ₗ comul)

Tactic:
ext

Goal state after:
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)
x✝ : C
⊢ (toConv
          ((mul' R A ∘ₗ ↑(TensorProduct.comm R A A)) ∘ₗ
            (↑(TensorProduct.comm R A A) ∘ₗ TensorProduct.map (star g).ofConv (star f).ofConv) ∘ₗ comul)).ofConv
      x✝ =
    (toConv (mul' R A ∘ₗ TensorProduct.map (star g).ofConv (star f).ofConv ∘ₗ comul)).ofConv x✝
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:
ext

Goal state after:
R : Type u_1
V : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
x✝³ x✝² : VertexOperator R V
x✝¹ : ℤ
x✝ : V
⊢ (coeff (x✝³ + x✝²) (-x✝¹ - 1)) x✝ = (((fun n ↦ coeff x✝³ (-n - 1)) + fun n ↦ coeff x✝² (-n - 1)) x✝¹) x✝
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:
ext

Goal state after:
R : Type u_1
V : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
x✝³ : R
x✝² : VertexOperator R V
x✝¹ : ℤ
x✝ : V
⊢ (coeff (x✝³ • x✝²) (-x✝¹ - 1)) x✝ = (((RingHom.id R) x✝³ • fun n ↦ coeff x✝² (-n - 1)) x✝¹) x✝
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
  rw [coeff_eq_ncoeff, ncoeff_eq_zero_of_lt_order A (-n - 1) x]
  lia

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
inst✝ : Fintype n
x✝ : n
⊢ star (toConv comul) = toConv (↑(TensorProduct.comm R R R) ∘ₗ comul)

Tactic:
ext

Goal state after:
R : Type u_5
inst✝³ : CommSemiring R
inst✝² : StarRing R
n : Type u_8
inst✝¹ : DecidableEq n
inst✝ : Fintype n
x✝ : n
⊢ (star (toConv comul)).ofConv 1 = (toConv (↑(TensorProduct.comm R R R) ∘ₗ comul)).ofConv 1