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

Goal state before:
pp: α : Type u_3
β : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid N
inst✝ : AddCommMonoid P
f : SkewMonoidAlgebra M α
g : α → M → SkewMonoidAlgebra N β
h : β → N → P
h_zero : ∀ (a : β), h a 0 = 0
h_add : ∀ (a : β) (b₁ b₂ : N), h a (b₁ + b₂) = h a b₁ + h a b₂
⊢ (f.coeff.sum fun a b ↦ (g a b).coeff.sum h) = f.sum fun a b ↦ (g a b).sum h

Tactic:
]

Goal state after:
α : Type u_3
β : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid N
inst✝ : AddCommMonoid P
f : SkewMonoidAlgebra M α
g : α → M → SkewMonoidAlgebra N β
h : β → N → P
h_zero : ∀ (a : β), h a 0 = 0
h_add : ∀ (a : β) (b₁ b₂ : N), h a (b₁ + b₂) = h a b₁ + h a b₂
⊢ (f.coeff.sum fun a b ↦ (g a b).coeff.sum h) = f.sum fun a b ↦ (g a b).sum h
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝ : AddCommMonoid k
p : SkewMonoidAlgebra k G → Prop
f : SkewMonoidAlgebra k G
zero : p 0
single : ∀ (g : G) (a : k), p (SkewMonoidAlgebra.single g a)
add : ∀ (f g : SkewMonoidAlgebra k G), p f → p g → p (f + g)
⊢ p (∑ a ∈ f.support, SkewMonoidAlgebra.single a (f.coeff a))

Tactic:
]

Goal state after:
k : Type u_1
G : Type u_2
inst✝ : AddCommMonoid k
p : SkewMonoidAlgebra k G → Prop
f : SkewMonoidAlgebra k G
zero : p 0
single : ∀ (g : G) (a : k), p (SkewMonoidAlgebra.single g a)
add : ∀ (f g : SkewMonoidAlgebra k G), p f → p g → p (f + g)
⊢ p (∑ a ∈ f.support, SkewMonoidAlgebra.single a (f.coeff a))
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝⁵ : Mul G
R : Type u_3
inst✝⁴ : Semiring R
inst✝³ : NonAssocSemiring k
inst✝² : SMul G k
g_hom : Type u_4
inst✝¹ : FunLike g_hom G R
inst✝ : MulHomClass g_hom G R
f : k →+* R
g : g_hom
a b : SkewMonoidAlgebra k G
h_comm : ∀ {x y : G}, y ∈ a.support → f (y • b.coeff x) * g y = g y * f (b.coeff x)
y : G
hy : y ∈ a.support
x : G
_hx : x ∈ b.support
⊢ f (a.coeff y) * (g y * (f (b.coeff x) * g x)) = f (a.coeff y) * (g y * (f (b.coeff x) * g x))

Tactic:
]

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

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

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

Tactic:
]

Goal state after:
case single
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Monoid G
inst✝ : MulSemiringAction G k
g : G
a : k
⊢ ((single g a).sum fun a₂ b₂ ↦ single (1 * a₂) (1 * 1 • b₂)) = single g a

case single
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Monoid G
inst✝ : MulSemiringAction G k
g : G
a : k
⊢ ((single g a).sum fun a₂ b₂ ↦ single (1 * a₂) (0 * 1 • b₂)) = 0
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

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

pp: case single
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Monoid G
inst✝ : MulSemiringAction G k
g : G
a : k
⊢ single (g * 1) (a * g • 0) = 0

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

Tactic:
]

Goal state after:
case single
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Monoid G
inst✝ : MulSemiringAction G k
g : G
a : k
⊢ single (g * 1) (a * g • 1) = single g a

case single
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Monoid G
inst✝ : MulSemiringAction G k
g : G
a : k
⊢ single (g * 1) (a * g • 0) = 0

case single
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Monoid G
inst✝ : MulSemiringAction G k
g : G
a : k
⊢ ((single 1 1).sum fun a₂ b₂ ↦ single (g * a₂) (0 * g • b₂)) = 0
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : CommMonoid G
inst✝¹ : MulSemiringAction G k
inst✝ : SMulCommClass G k k
a b : SkewMonoidAlgebra k G
g : G
r : k
⊢ (algebraMap k k) r = (algebraMap k k) r

Tactic:
]

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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : CommMonoid G
inst✝¹ : MulSemiringAction G k
inst✝ : SMulCommClass G k k
a b : SkewMonoidAlgebra k G
hgk : ∀ (g : G) (r : k), g • r = r
⊢ (b.coeff.sum fun x' v' ↦ a.coeff.sum fun x v ↦ single (x * x') (v * v')) =
    b.coeff.sum fun a₁ b₁ ↦ a.coeff.sum fun a₂ b₂ ↦ single (a₁ * a₂) (b₁ * b₂)

Tactic:
]

Goal state after:
k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : CommMonoid G
inst✝¹ : MulSemiringAction G k
inst✝ : SMulCommClass G k k
a b : SkewMonoidAlgebra k G
hgk : ∀ (g : G) (r : k), g • r = r
⊢ (b.coeff.sum fun x' v' ↦ a.coeff.sum fun x v ↦ single (x * x') (v * v')) =
    b.coeff.sum fun a₁ b₁ ↦ a.coeff.sum fun a₂ b₂ ↦ single (a₁ * a₂) (b₁ * b₂)
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : CommMonoid G
inst✝¹ : MulSemiringAction G k
inst✝ : SMulCommClass G k k
a b : SkewMonoidAlgebra k G
hgk : ∀ (g : G) (r : k), g • r = r
x : G
x✝¹ : x ∈ b.coeff.support
y : G
x✝ : y ∈ a.coeff.support
⊢ single (x * y) (b.coeff x * a.coeff y) = single (x * y) (b.coeff x * a.coeff y)

Tactic:
]

Goal state after:
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
hvy : 1 • ↑v = (star y * y) • ↑v
⊢ ∃ α, u = α • v

Tactic:
]

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
hvy : 1 • ↑v = (star y * y) • ↑v
⊢ ∃ α, u = α • v
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
hvy : star y * y = 1 ∨ ↑v = 0
⊢ ∃ α, u = α • v

Tactic:
]

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
hvy : star y * y = 1 ∨ ↑v = 0
⊢ ∃ α, u = α • 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 α
g g' : G
f : SkewMonoidAlgebra M α
⊢ (mapDomain fun x ↦ g • x) ((mapDomain fun x ↦ g' • x) f) = (mapDomain fun x ↦ g • x) ((mapDomain fun x ↦ g' • x) f)

Tactic:
]

Goal state after:
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 α
f : SkewMonoidAlgebra M α
⊢ f = f

Tactic:
]

Goal state after:
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
inst✝ : DecidableEq G
f g : SkewMonoidAlgebra k G
x : G
⊢ (f.sum fun a₁ b ↦ (g.sum fun a₂ b₂ ↦ single (a₁ * a₂) (b * a₁ • b₂)).coeff x) =
    f.sum fun a₁ b₁ ↦ g.sum fun a₂ b₂ ↦ if a₁ * a₂ = x then b₁ * a₁ • b₂ else 0

Tactic:
]

Goal state after:
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
⊢ (f.sum fun a₁ b ↦ (g.sum fun a₂ b₂ ↦ single (a₁ * a₂) (b * a₁ • b₂)).coeff x) =
    f.sum fun a₁ b₁ ↦ g.sum fun a₂ b₂ ↦ if a₁ * a₂ = x then b₁ * a₁ • b₂ else 0
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 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

Tactic:
]

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.Symmetrized

Goal state before:
pp: α : Type u_1
inst✝³ : Mul α
inst✝² : AddMonoidWithOne α
inst✝¹ : Invertible 2
a : α
inst✝ : Invertible a
⊢ 1 = 1

Tactic:
]

Goal state after:
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
⊢ ∑ a₁ ∈ f.support, ∑ a₂ ∈ g.support, F (a₁, a₂) = ∑ x ∈ f.support, ∑ y ∈ g.support, F (x, y)

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.TrivSqZeroExt.Ideal

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
r : R
m : M
hr : r = 0
⊢ (0, m) = inr (snd (0, m))

Tactic:
]

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
r : R
m : M
hr : r = 0
⊢ (0, m) = inr (snd (0, m))
Module: Mathlib.Algebra.TrivSqZeroExt.Ideal

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
r : R
m : M
hrm : (r, m) = inr (snd (r, m))
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.TrivSqZeroExt.Ideal

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
x : TrivSqZeroExt R M
hx : x = inr x.snd
y : TrivSqZeroExt R M
hy : y = inr y.snd
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: R : Type u
inst✝ : LinearOrder R
x y : Tropical R
⊢ untrop x ≤ untrop y ↔ untrop x ≤ untrop y

Tactic:
]

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

Goal state before:
pp: R : Type u
inst✝ : LinearOrder R
x y : Tropical R
⊢ untrop y ≤ untrop x ↔ untrop y ≤ untrop x

Tactic:
]

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

Goal state before:
pp: R : Type u
inst✝ : LinearOrder R
x y z : Tropical R
⊢ min (untrop x) (untrop y) = untrop z ↔ x = z ∧ x ≤ y ∨ y = z ∧ y ≤ x

Tactic:
]

Goal state after:
R : Type u
inst✝ : LinearOrder R
x y z : Tropical R
⊢ min (untrop x) (untrop y) = untrop z ↔ x = z ∧ x ≤ y ∨ y = z ∧ y ≤ x
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:
]

Goal state after:
R : Type u
inst✝ : LinearOrder R
a b : Tropical (WithTop R)
⊢ a = 0 ∧ a ≤ b ∨ b = 0 ∧ b ≤ a ↔ a = 0 ∧ b = 0
Module: Mathlib.Algebra.Symmetrized

Goal state before:
pp: α : Type u_1
inst✝¹ : Semiring α
inst✝ : Invertible 2
a b c : αˢʸᵐ
⊢ sym (⅟2 * (unsym a * (unsym b + unsym c) + (unsym b * unsym a + unsym c * unsym a))) =
    sym (⅟2 * (unsym a * unsym b + unsym b * unsym a + (unsym a * unsym c + unsym c * unsym a)))

Tactic:
]

Goal state after:
α : Type u_1
inst✝¹ : Semiring α
inst✝ : Invertible 2
a b c : αˢʸᵐ
⊢ sym (⅟2 * (unsym a * (unsym b + unsym c) + (unsym b * unsym a + unsym c * unsym a))) =
    sym (⅟2 * (unsym a * unsym b + unsym b * unsym a + (unsym a * unsym c + unsym c * unsym a)))
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
this : ({p | p.1 * p.2 = x} ∩ Function.support fun p ↦ f.coeff p.1 * p.1 • g.coeff p.2).Finite
⊢ (f * g).coeff x = ∑ i ∈ this.toFinset, f.coeff i.1 * i.1 • g.coeff i.2

Tactic:
]

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
this : ({p | p.1 * p.2 = x} ∩ Function.support fun p ↦ f.coeff p.1 * p.1 • g.coeff p.2).Finite
⊢ (f * g).coeff x = ∑ i ∈ this.toFinset, f.coeff i.1 * i.1 • g.coeff i.2
Module: Mathlib.Algebra.Symmetrized

Goal state before:
pp: case e_6.e_a
α : Type u_1
inst✝¹ : Semiring α
inst✝ : Invertible 2
a b c : αˢʸᵐ
⊢ unsym a * unsym b + unsym a * unsym c + (unsym b * unsym a + unsym c * unsym a) =
    unsym a * unsym b + unsym b * unsym a + (unsym a * unsym c + unsym c * unsym a)

Tactic:
]

Goal state after:
case e_6.e_a
α : Type u_1
inst✝¹ : Semiring α
inst✝ : Invertible 2
a b c : αˢʸᵐ
⊢ unsym a * unsym b + unsym a * unsym c + (unsym b * unsym a + unsym c * unsym a) =
    unsym a * unsym b + unsym b * unsym a + (unsym a * unsym c + unsym c * unsym a)
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
this : ({p | p.1 * p.2 = x} ∩ Function.support fun p ↦ f.coeff p.1 * p.1 • g.coeff p.2).Finite
s : Finset (G × G) := this.toFinset
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₁ ∈ f.support, ∑ a₂ ∈ g.support, F (a₁, a₂) = ∑ x ∈ f.support, ∑ y ∈ g.support, F (x, y)

Tactic:
]

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

Goal state before:
pp: case inl
R : Type u
inst✝ : LinearOrder R
x y z : Tropical R
h : y ≤ z
hx : x ≤ y
⊢ x ≤ x

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Symmetrized

Goal state before:
pp: α : Type u_1
inst✝¹ : Semiring α
inst✝ : Invertible 2
a b c : αˢʸᵐ
⊢ sym (⅟2 * (unsym a * unsym c + unsym b * unsym c + unsym c * (unsym a + unsym b))) =
    sym (⅟2 * (unsym a * unsym c + unsym c * unsym a + (unsym b * unsym c + unsym c * unsym b)))

Tactic:
]

Goal state after:
α : Type u_1
inst✝¹ : Semiring α
inst✝ : Invertible 2
a b c : αˢʸᵐ
⊢ sym (⅟2 * (unsym a * unsym c + unsym b * unsym c + unsym c * (unsym a + unsym b))) =
    sym (⅟2 * (unsym a * unsym c + unsym c * unsym a + (unsym b * unsym c + unsym c * unsym b)))
Module: Mathlib.Algebra.Tropical.Basic

Goal state before:
pp: case inr
R : Type u
inst✝ : LinearOrder R
x y z : Tropical R
h : y ≤ z
hy : y ≤ x
⊢ y ≤ x + z

Tactic:
]

Goal state after:
case inr
R : Type u
inst✝ : LinearOrder R
x y z : Tropical R
h : y ≤ z
hy : y ≤ x
⊢ y ≤ x + z
Module: Mathlib.Algebra.Symmetrized

Goal state before:
pp: case e_6.e_a
α : Type u_1
inst✝¹ : Semiring α
inst✝ : Invertible 2
a b c : αˢʸᵐ
⊢ unsym a * unsym c + unsym b * unsym c + (unsym c * unsym a + unsym c * unsym b) =
    unsym a * unsym c + unsym c * unsym a + (unsym b * unsym c + unsym c * unsym b)

Tactic:
]

Goal state after:
case e_6.e_a
α : Type u_1
inst✝¹ : Semiring α
inst✝ : Invertible 2
a b c : αˢʸᵐ
⊢ unsym a * unsym c + unsym b * unsym c + (unsym c * unsym a + unsym c * unsym b) =
    unsym a * unsym c + unsym c * unsym a + (unsym b * unsym c + unsym c * unsym b)
Module: Mathlib.Algebra.Tropical.Basic

Goal state before:
pp: case inr.inl
R : Type u
inst✝ : LinearOrder R
x y z : Tropical R
h : y ≤ z
hy : y ≤ x
hx : x ≤ z
⊢ y ≤ x

Tactic:
]

Goal state after:
case inr.inl
R : Type u
inst✝ : LinearOrder R
x y z : Tropical R
h : y ≤ z
hy : y ≤ x
hx : x ≤ z
⊢ y ≤ x
Module: Mathlib.Algebra.Tropical.Basic

Goal state before:
pp: case inr.inr
R : Type u
inst✝ : LinearOrder R
x y z : Tropical R
h : y ≤ z
hy : y ≤ x
hx : z ≤ x
⊢ y ≤ z

Tactic:
]

Goal state after:
case inr.inr
R : Type u
inst✝ : LinearOrder R
x y z : Tropical R
h : y ≤ z
hy : y ≤ x
hx : z ≤ x
⊢ y ≤ z
Module: Mathlib.Algebra.Symmetrized

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

Tactic:
]

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

Goal state before:
pp: case inl
R : Type u
inst✝³ : LinearOrder R
inst✝² : AddMonoid R
inst✝¹ : AddLeftMono R
inst✝ : AddRightMono R
x y : Tropical R
n : ℕ
h : x ≤ y
⊢ x ^ n = x ^ n

Tactic:
]

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

Goal state before:
pp: case inr
R : Type u
inst✝³ : LinearOrder R
inst✝² : AddMonoid R
inst✝¹ : AddLeftMono R
inst✝ : AddRightMono R
x y : Tropical R
n : ℕ
h : y ≤ x
⊢ y ^ n = y ^ n

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Symmetrized

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

Tactic:
]

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

Goal state before:
pp: case succ
R : Type u_1
inst✝¹ : LinearOrder R
inst✝ : OrderTop R
x : Tropical R
n : ℕ
IH : (n + 1) • x = x
⊢ x = x

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Symmetrized

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

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Symmetrized

Goal state before:
pp: α : Type u_1
inst✝¹ : Semiring α
inst✝ : Invertible 2
a : α
⊢ sym (a * a) = sym (a * a)

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Symmetrized

Goal state before:
pp: α : Type u_1
inst✝⁴ : Mul α
inst✝³ : AddCommSemigroup α
inst✝² : One α
inst✝¹ : OfNat α 2
inst✝ : Invertible 2
a b : αˢʸᵐ
⊢ sym (⅟2 * (unsym b * unsym a + unsym a * unsym b)) = sym (⅟2 * (unsym b * unsym a + unsym a * unsym b))

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Symmetrized

Goal state before:
pp: α : Type u_1
inst✝¹ : Ring α
inst✝ : Invertible 2
a✝ b : αˢʸᵐ
a : α
this : Commute 2 a
⊢ ?m.16 a

Tactic:
]

Goal state after:
α : Type u_1
inst✝¹ : Ring α
inst✝ : Invertible 2
a✝ b : αˢʸᵐ
a : α
this : Commute 2 a
⊢ ?m.16 a
Module: Mathlib.Algebra.Tropical.BigOperators

Goal state before:
pp: case inr
R : Type u_1
S : Type u_2
inst✝ : ConditionallyCompleteLinearOrder R
s : Finset S
f : S → WithTop R
h : s.Nonempty
⊢ ∑ i ∈ s, trop (f i) = ∑ i ∈ s, trop (f i)

Tactic:
]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : ConditionallyCompleteLinearOrder R
inst✝ : Fintype S
f : S → WithTop R
⊢ ∑ i, trop (f i) = ∑ i, trop (f i)

Tactic:
]

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

Goal state before:
pp: case inr
R : Type u_1
S : Type u_2
inst✝ : ConditionallyCompleteLinearOrder R
s : Finset S
f : S → Tropical (WithTop R)
h : s.Nonempty
⊢ s.inf (untrop ∘ f) = s.inf (untrop ∘ f)

Tactic:
]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : ConditionallyCompleteLinearOrder R
inst✝ : Fintype S
f : S → Tropical (WithTop R)
⊢ sInf ((fun x ↦ untrop (f x)) '' ↑univ) = sInf ((fun i ↦ untrop (f i)) '' ↑univ)

Tactic:
]

Goal state after:
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
r : k
g g' : G
x : SkewMonoidAlgebra k G
h : ¬∃ d, g' = g * d
⊢ (x.sum fun a₂ b₂ ↦ if g * a₂ = g' then r * g • b₂ else 0) = 0

pp: k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : SMulZeroClass G k
r : k
g g' : G
x : SkewMonoidAlgebra k G
h : ¬∃ d, g' = g * d
⊢ (x.sum fun a₂ b₂ ↦ if g * a₂ = g' then 0 * g • b₂ else 0) = 0

Tactic:
]

Goal state after:
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : SMulZeroClass G k
r : k
g g' : G
x : SkewMonoidAlgebra k G
h : ¬∃ d, g' = g * d
⊢ (x.sum fun a₂ b₂ ↦ if g * a₂ = g' then r * g • b₂ else 0) = 0

k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : SMulZeroClass G k
r : k
g g' : G
x : SkewMonoidAlgebra k G
h : ¬∃ d, g' = g * d
⊢ (x.sum fun a₂ b₂ ↦ if g * a₂ = g' then 0 * g • b₂ else 0) = 0
Module: Mathlib.Algebra.Symmetrized

Goal state before:
pp: case calc_1
α : Type u_1
inst✝¹ : Ring α
inst✝ : Invertible 2
a b : αˢʸᵐ
commute_half_left : ∀ (a : α), ⅟2 * a = a * ⅟2
⊢ sym
      (⅟2 * ⅟2 *
        (unsym a * unsym b * unsym (a * a) + unsym b * unsym a * unsym (a * a) + unsym (a * a) * unsym a * unsym b +
          unsym (a * a) * unsym b * unsym a)) =
    sym
      (⅟2 * ⅟2 *
        (unsym a * unsym b * unsym (a * a) + unsym b * unsym a * unsym (a * a) + unsym (a * a) * unsym a * unsym b +
          unsym (a * a) * unsym b * unsym a))

Tactic:
]

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 : SkewMonoidAlgebra k G
r : k
x a : G
⊢ a = x ↔ a = x

Tactic:
]

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 * g).coeff x

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Symmetrized

Goal state before:
pp: case calc_2
α : Type u_1
inst✝¹ : Ring α
inst✝ : Invertible 2
a b : αˢʸᵐ
commute_half_left : ∀ (a : α), ⅟2 * a = a * ⅟2
⊢ ⅟2 * ⅟2 *
      (unsym a * unsym b * unsym (a * a) + unsym b * unsym a * unsym (a * a) + unsym (a * a) * unsym a * unsym b +
        unsym (a * a) * unsym b * unsym a) =
    ⅟2 * ⅟2 *
      (unsym a * (unsym b * unsym (a * a) + unsym (a * a) * unsym b) +
        (unsym b * unsym (a * a) + unsym (a * a) * unsym b) * unsym a)

Tactic:
]

Goal state after:
case calc_2
α : Type u_1
inst✝¹ : Ring α
inst✝ : Invertible 2
a b : αˢʸᵐ
commute_half_left : ∀ (a : α), ⅟2 * a = a * ⅟2
⊢ ⅟2 * ⅟2 *
      (unsym a * unsym b * unsym (a * a) + unsym b * unsym a * unsym (a * a) + unsym (a * a) * unsym a * unsym b +
        unsym (a * a) * unsym b * unsym a) =
    ⅟2 * ⅟2 *
      (unsym a * (unsym b * unsym (a * a) + unsym (a * a) * unsym b) +
        (unsym b * unsym (a * a) + unsym (a * a) * unsym b) * unsym a)
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
⊢ g (single 1 b) * g (single a 1) = g (single 1 b) * g (single a 1)

Tactic:
]

Goal state after: