mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Ring.IsFormallyReal

Goal state before:
pp: case sq
R : Type u_1
inst✝¹ : AddMonoid R
inst✝ : Mul R
s₁ s₂ : R
h₂ : IsSumNonzeroSq s₂
a✝ : R
ha✝ : a✝ ≠ 0
⊢ IsSumNonzeroSq (a✝ * a✝ + s₂)

pp: case sq_add
R : Type u_1
inst✝¹ : AddMonoid R
inst✝ : Mul R
s₁ s₂ : R
h₂ : IsSumNonzeroSq s₂
a✝ s✝ : R
ha✝ : a✝ ≠ 0
hs✝ : IsSumNonzeroSq s✝
hs_ih✝ : IsSumNonzeroSq (s✝ + s₂)
⊢ IsSumNonzeroSq (a✝ * a✝ + s✝ + s₂)

Tactic:
<;>

Goal state after:
case sq
R : Type u_1
inst✝¹ : AddMonoid R
inst✝ : Mul R
s₁ s₂ : R
h₂ : IsSumNonzeroSq s₂
a✝ : R
ha✝ : a✝ ≠ 0
⊢ IsSumNonzeroSq (a✝ * a✝ + s₂)

case sq_add
R : Type u_1
inst✝¹ : AddMonoid R
inst✝ : Mul R
s₁ s₂ : R
h₂ : IsSumNonzeroSq s₂
a✝ s✝ : R
ha✝ : a✝ ≠ 0
hs✝ : IsSumNonzeroSq s✝
hs_ih✝ : IsSumNonzeroSq (s✝ + s₂)
⊢ IsSumNonzeroSq (a✝ * a✝ + s✝ + s₂)
Module: Mathlib.Algebra.Ring.IsFormallyReal

Goal state before:
pp: case sq
R : Type u_1
inst✝¹ : AddMonoid R
inst✝ : Mul R
s a✝ : R
ha✝ : a✝ ≠ 0
⊢ IsSumSq (a✝ * a✝)

pp: case sq_add
R : Type u_1
inst✝¹ : AddMonoid R
inst✝ : Mul R
s a✝ s✝ : R
ha✝ : a✝ ≠ 0
hs✝ : IsSumNonzeroSq s✝
hs_ih✝ : IsSumSq s✝
⊢ IsSumSq (a✝ * a✝ + s✝)

Tactic:
<;>

Goal state after:
case sq
R : Type u_1
inst✝¹ : AddMonoid R
inst✝ : Mul R
s a✝ : R
ha✝ : a✝ ≠ 0
⊢ IsSumSq (a✝ * a✝)

case sq_add
R : Type u_1
inst✝¹ : AddMonoid R
inst✝ : Mul R
s a✝ s✝ : R
ha✝ : a✝ ≠ 0
hs✝ : IsSumNonzeroSq s✝
hs_ih✝ : IsSumSq s✝
⊢ IsSumSq (a✝ * a✝ + s✝)
Module: Mathlib.Algebra.Ring.IsFormallyReal

Goal state before:
pp: R : Type u_1
inst✝¹ : AddMonoid R
inst✝ : Mul R
s : R
h : IsSumNonzeroSq s
⊢ IsSumSq s

Tactic:
induction h <;> aesop

Goal state after:
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: case h_add
R : Type u
inst₁ inst₂ : Ring R
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
⊢ HAdd.hAdd = HAdd.hAdd

pp: case h_mul
R : Type u
inst₁ inst₂ : Ring R
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
⊢ HMul.hMul = HMul.hMul

Tactic:
<;>

Goal state after:
case h_add
R : Type u
inst₁ inst₂ : Ring R
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
⊢ HAdd.hAdd = HAdd.hAdd

case h_mul
R : Type u
inst₁ inst₂ : Ring R
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
⊢ HMul.hMul = HMul.hMul
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: case h_add
R : Type u
inst₁ inst₂ : Ring R
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
h₁ : inst₁.toSemiring = inst₂.toSemiring
⊢ HAdd.hAdd = HAdd.hAdd

pp: case h_mul
R : Type u
inst₁ inst₂ : Ring R
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
h₁ : inst₁.toSemiring = inst₂.toSemiring
⊢ HMul.hMul = HMul.hMul

Tactic:
<;>

Goal state after:
case h_add
R : Type u
inst₁ inst₂ : Ring R
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
h₁ : inst₁.toSemiring = inst₂.toSemiring
⊢ HAdd.hAdd = HAdd.hAdd

case h_mul
R : Type u
inst₁ inst₂ : Ring R
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
h₁ : inst₁.toSemiring = inst₂.toSemiring
⊢ HMul.hMul = HMul.hMul
Module: Mathlib.Algebra.Ring.WithZero

Goal state before:
pp: case coe.zero
α : Type u_1
inst✝² : Mul α
inst✝¹ : Add α
inst✝ : LeftDistribClass α
c : WithZero α
a✝ : α
⊢ ↑a✝ * (0 + c) = ↑a✝ * 0 + ↑a✝ * c

pp: case coe.coe
α : Type u_1
inst✝² : Mul α
inst✝¹ : Add α
inst✝ : LeftDistribClass α
c : WithZero α
a✝¹ a✝ : α
⊢ ↑a✝¹ * (↑a✝ + c) = ↑a✝¹ * ↑a✝ + ↑a✝¹ * c

Tactic:
<;>

Goal state after:
case coe.zero
α : Type u_1
inst✝² : Mul α
inst✝¹ : Add α
inst✝ : LeftDistribClass α
c : WithZero α
a✝ : α
⊢ ↑a✝ * (0 + c) = ↑a✝ * 0 + ↑a✝ * c

case coe.coe
α : Type u_1
inst✝² : Mul α
inst✝¹ : Add α
inst✝ : LeftDistribClass α
c : WithZero α
a✝¹ a✝ : α
⊢ ↑a✝¹ * (↑a✝ + c) = ↑a✝¹ * ↑a✝ + ↑a✝¹ * c
Module: Mathlib.Algebra.Ring.WithZero

Goal state before:
pp: case coe.zero.zero
α : Type u_1
inst✝² : Mul α
inst✝¹ : Add α
inst✝ : LeftDistribClass α
a✝ : α
⊢ ↑a✝ * (0 + 0) = ↑a✝ * 0 + ↑a✝ * 0

pp: case coe.zero.coe
α : Type u_1
inst✝² : Mul α
inst✝¹ : Add α
inst✝ : LeftDistribClass α
a✝¹ a✝ : α
⊢ ↑a✝¹ * (0 + ↑a✝) = ↑a✝¹ * 0 + ↑a✝¹ * ↑a✝

pp: case coe.coe.zero
α : Type u_1
inst✝² : Mul α
inst✝¹ : Add α
inst✝ : LeftDistribClass α
a✝¹ a✝ : α
⊢ ↑a✝¹ * (↑a✝ + 0) = ↑a✝¹ * ↑a✝ + ↑a✝¹ * 0

pp: case coe.coe.coe
α : Type u_1
inst✝² : Mul α
inst✝¹ : Add α
inst✝ : LeftDistribClass α
a✝² a✝¹ a✝ : α
⊢ ↑a✝² * (↑a✝¹ + ↑a✝) = ↑a✝² * ↑a✝¹ + ↑a✝² * ↑a✝

Tactic:
<;>

Goal state after:
case coe.zero.zero
α : Type u_1
inst✝² : Mul α
inst✝¹ : Add α
inst✝ : LeftDistribClass α
a✝ : α
⊢ ↑a✝ * (0 + 0) = ↑a✝ * 0 + ↑a✝ * 0

case coe.zero.coe
α : Type u_1
inst✝² : Mul α
inst✝¹ : Add α
inst✝ : LeftDistribClass α
a✝¹ a✝ : α
⊢ ↑a✝¹ * (0 + ↑a✝) = ↑a✝¹ * 0 + ↑a✝¹ * ↑a✝

case coe.coe.zero
α : Type u_1
inst✝² : Mul α
inst✝¹ : Add α
inst✝ : LeftDistribClass α
a✝¹ a✝ : α
⊢ ↑a✝¹ * (↑a✝ + 0) = ↑a✝¹ * ↑a✝ + ↑a✝¹ * 0

case coe.coe.coe
α : Type u_1
inst✝² : Mul α
inst✝¹ : Add α
inst✝ : LeftDistribClass α
a✝² a✝¹ a✝ : α
⊢ ↑a✝² * (↑a✝¹ + ↑a✝) = ↑a✝² * ↑a✝¹ + ↑a✝² * ↑a✝
Module: Mathlib.Algebra.Ring.WithZero

Goal state before:
pp: case coe.zero
α : Type u_1
inst✝² : Mul α
inst✝¹ : Add α
inst✝ : RightDistribClass α
b : WithZero α
a✝ : α
⊢ (0 + b) * ↑a✝ = 0 * ↑a✝ + b * ↑a✝

pp: case coe.coe
α : Type u_1
inst✝² : Mul α
inst✝¹ : Add α
inst✝ : RightDistribClass α
b : WithZero α
a✝¹ a✝ : α
⊢ (↑a✝ + b) * ↑a✝¹ = ↑a✝ * ↑a✝¹ + b * ↑a✝¹

Tactic:
<;>

Goal state after:
case coe.zero
α : Type u_1
inst✝² : Mul α
inst✝¹ : Add α
inst✝ : RightDistribClass α
b : WithZero α
a✝ : α
⊢ (0 + b) * ↑a✝ = 0 * ↑a✝ + b * ↑a✝

case coe.coe
α : Type u_1
inst✝² : Mul α
inst✝¹ : Add α
inst✝ : RightDistribClass α
b : WithZero α
a✝¹ a✝ : α
⊢ (↑a✝ + b) * ↑a✝¹ = ↑a✝ * ↑a✝¹ + b * ↑a✝¹
Module: Mathlib.Algebra.Ring.WithZero

Goal state before:
pp: case coe.zero.zero
α : Type u_1
inst✝² : Mul α
inst✝¹ : Add α
inst✝ : RightDistribClass α
a✝ : α
⊢ (0 + 0) * ↑a✝ = 0 * ↑a✝ + 0 * ↑a✝

pp: case coe.zero.coe
α : Type u_1
inst✝² : Mul α
inst✝¹ : Add α
inst✝ : RightDistribClass α
a✝¹ a✝ : α
⊢ (0 + ↑a✝) * ↑a✝¹ = 0 * ↑a✝¹ + ↑a✝ * ↑a✝¹

pp: case coe.coe.zero
α : Type u_1
inst✝² : Mul α
inst✝¹ : Add α
inst✝ : RightDistribClass α
a✝¹ a✝ : α
⊢ (↑a✝ + 0) * ↑a✝¹ = ↑a✝ * ↑a✝¹ + 0 * ↑a✝¹

pp: case coe.coe.coe
α : Type u_1
inst✝² : Mul α
inst✝¹ : Add α
inst✝ : RightDistribClass α
a✝² a✝¹ a✝ : α
⊢ (↑a✝¹ + ↑a✝) * ↑a✝² = ↑a✝¹ * ↑a✝² + ↑a✝ * ↑a✝²

Tactic:
<;>

Goal state after:
case coe.zero.zero
α : Type u_1
inst✝² : Mul α
inst✝¹ : Add α
inst✝ : RightDistribClass α
a✝ : α
⊢ (0 + 0) * ↑a✝ = 0 * ↑a✝ + 0 * ↑a✝

case coe.zero.coe
α : Type u_1
inst✝² : Mul α
inst✝¹ : Add α
inst✝ : RightDistribClass α
a✝¹ a✝ : α
⊢ (0 + ↑a✝) * ↑a✝¹ = 0 * ↑a✝¹ + ↑a✝ * ↑a✝¹

case coe.coe.zero
α : Type u_1
inst✝² : Mul α
inst✝¹ : Add α
inst✝ : RightDistribClass α
a✝¹ a✝ : α
⊢ (↑a✝ + 0) * ↑a✝¹ = ↑a✝ * ↑a✝¹ + 0 * ↑a✝¹

case coe.coe.coe
α : Type u_1
inst✝² : Mul α
inst✝¹ : Add α
inst✝ : RightDistribClass α
a✝² a✝¹ a✝ : α
⊢ (↑a✝¹ + ↑a✝) * ↑a✝² = ↑a✝¹ * ↑a✝² + ↑a✝ * ↑a✝²
Module: Mathlib.Algebra.Ring.CentroidHom

Goal state before:
pp: case comm
F : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
α : Type u_5
inst✝ : NonAssocSemiring α
T : CentroidHom α
⊢ ∀ (a : α), Commute (T 1) a

pp: case left_assoc
F : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
α : Type u_5
inst✝ : NonAssocSemiring α
T : CentroidHom α
⊢ ∀ (b c : α), T 1 * (b * c) = T 1 * b * c

pp: case right_assoc
F : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
α : Type u_5
inst✝ : NonAssocSemiring α
T : CentroidHom α
⊢ ∀ (a b : α), a * b * T 1 = a * (b * T 1)

Tactic:
<;>

Goal state after:
case comm
F : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
α : Type u_5
inst✝ : NonAssocSemiring α
T : CentroidHom α
⊢ ∀ (a : α), Commute (T 1) a

case left_assoc
F : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
α : Type u_5
inst✝ : NonAssocSemiring α
T : CentroidHom α
⊢ ∀ (b c : α), T 1 * (b * c) = T 1 * b * c

case right_assoc
F : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
α : Type u_5
inst✝ : NonAssocSemiring α
T : CentroidHom α
⊢ ∀ (a b : α), a * b * T 1 = a * (b * T 1)
Module: Mathlib.Algebra.SkewMonoidAlgebra.Lift

Goal state before:
pp: k : Type u_1
G : Type u_2
H : Type u_3
inst✝ : AddCommMonoid k
f : G ≃ H
l : SkewMonoidAlgebra k G
x : H
⊢ l.coeff (f.symm x) = ((mapDomain ⇑f) l).coeff x

Tactic:
coeff_mapDomain,

Goal state after:
k : Type u_1
G : Type u_2
H : Type u_3
inst✝ : AddCommMonoid k
f : G ≃ H
l : SkewMonoidAlgebra k G
x : H
⊢ l.coeff (f.symm x) = (Finsupp.mapDomain (⇑f) l.coeff) x
Module: Mathlib.Algebra.SkewMonoidAlgebra.Support

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝³ : Monoid G
inst✝² : Semiring k
inst✝¹ : MulSemiringAction G k
f : SkewMonoidAlgebra k G
inst✝ : IsRightCancelMul G
r : k
x : G
hrx : ∀ (g : G) (y : k), y * g • r = 0 ↔ y = 0
⊢ (f * single x r).support = map (mulRightEmbedding x) f.support

Tactic:
classical
  ext a
  simp [support_mul_single_eq_image f (IsRightRegular.all x) hrx]

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

Goal state before:
pp: case pos
M : Type u_4
α : Type u_5
inst✝ : AddCommMonoid M
f : SkewMonoidAlgebra M α
a : α
b : M
x : α
hx : x = a
⊢ (f.update a b).coeff x = ((erase a) f + single a b).coeff x

pp: case neg
M : Type u_4
α : Type u_5
inst✝ : AddCommMonoid M
f : SkewMonoidAlgebra M α
a : α
b : M
x : α
hx : ¬x = a
⊢ (f.update a b).coeff x = ((erase a) f + single a b).coeff x

Tactic:
<;>

Goal state after:
case pos
M : Type u_4
α : Type u_5
inst✝ : AddCommMonoid M
f : SkewMonoidAlgebra M α
a : α
b : M
x : α
hx : x = a
⊢ (f.update a b).coeff x = ((erase a) f + single a b).coeff x

case neg
M : Type u_4
α : Type u_5
inst✝ : AddCommMonoid M
f : SkewMonoidAlgebra M α
a : α
b : M
x : α
hx : ¬x = a
⊢ (f.update a b).coeff x = ((erase a) f + single a b).coeff x
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: S : Type uS
inst✝² : CommSemiring S
A : Type uA
inst✝¹ : Semiring A
inst✝ : Algebra S A
s : A → A → Prop
this : Function.Surjective fun x ↦ { toQuot := Quot.mk (Rel s) x }
⊢ Function.Surjective ⇑(mkAlgHom S s)

Tactic:
simpa [mkAlgHom_def, mkRingHom_def]

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

Goal state before:
pp: R : Type u_1
n : ℕ
inst✝ : Semiring R
p : SkewPolynomial R
⊢ n ∈ p.support ↔ p.coeff n ≠ 0

Tactic:
by
  simp [support, coeff]

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

Goal state before:
pp: case h'
R : Type u_1
inst✝¹ : Semiring R
S : Type u_5
inst✝ : AddCommMonoid S
p : SkewPolynomial R
f : ℕ → R → S
⊢ ∀ i ∈ p.support, i ∉ ⇑toAdd '' ↑p.coeff.support → f i (p.coeff i) = 0

pp: case h
R : Type u_1
inst✝¹ : Semiring R
S : Type u_5
inst✝ : AddCommMonoid S
p : SkewPolynomial R
f : ℕ → R → S
⊢ ∀ i ∈ p.coeff.support, f (toAdd i) (p.coeff i) = f (toAdd i) (p.coeff (toAdd i))

pp: R : Type u_1
inst✝¹ : Semiring R
S : Type u_5
inst✝ : AddCommMonoid S
p : SkewPolynomial R
f : ℕ → R → S
x✝ : Multiplicative ℕ
⊢ x✝ ∈ ↑p.coeff.support → toAdd x✝ ∈ ↑p.support

Tactic:
<;>

Goal state after:
case h'
R : Type u_1
inst✝¹ : Semiring R
S : Type u_5
inst✝ : AddCommMonoid S
p : SkewPolynomial R
f : ℕ → R → S
⊢ ∀ i ∈ p.support, i ∉ ⇑toAdd '' ↑p.coeff.support → f i (p.coeff i) = 0

case h
R : Type u_1
inst✝¹ : Semiring R
S : Type u_5
inst✝ : AddCommMonoid S
p : SkewPolynomial R
f : ℕ → R → S
⊢ ∀ i ∈ p.coeff.support, f (toAdd i) (p.coeff i) = f (toAdd i) (p.coeff (toAdd i))

R : Type u_1
inst✝¹ : Semiring R
S : Type u_5
inst✝ : AddCommMonoid S
p : SkewPolynomial R
f : ℕ → R → S
x✝ : Multiplicative ℕ
⊢ x✝ ∈ ↑p.coeff.support → toAdd x✝ ∈ ↑p.support
Module: Mathlib.Algebra.SkewPolynomial.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
m n : ℕ
a b : R
⊢ (monomial m) a = (monomial n) b ↔ Finsupp.single m a = Finsupp.single n b

Tactic:
simp only [monomial_def, ← coeff_single, coeff_inj]

Goal state after:
R : Type u_1
inst✝ : Semiring R
m n : ℕ
a b : R
⊢ single (ofAdd m) a = single (ofAdd n) b ↔ single m a = single n b
Module: Mathlib.Algebra.SkewPolynomial.Basic

Goal state before:
pp: case h0
R : Type u_1
inst✝ : Semiring R
motive : SkewPolynomial R → Prop
p : SkewPolynomial R
h0 : motive 0
ha : ∀ (n : ℕ) (r : R) (q : SkewPolynomial R), n ∉ q.support → r ≠ 0 → motive q → motive ((monomial n) r + q)
⊢ motive 0

pp: case ha
R : Type u_1
inst✝ : Semiring R
motive : SkewPolynomial R → Prop
p : SkewPolynomial R
h0 : motive 0
ha : ∀ (n : ℕ) (r : R) (q : SkewPolynomial R), n ∉ q.support → r ≠ 0 → motive q → motive ((monomial n) r + q)
⊢ ∀ (a : Multiplicative ℕ) (b : R) (f : SkewMonoidAlgebra R (Multiplicative ℕ)),
    a ∉ f.support → b ≠ 0 → motive f → motive (single a b + f)

Tactic:
<;>

Goal state after:
case h0
R : Type u_1
inst✝ : Semiring R
motive : SkewPolynomial R → Prop
p : SkewPolynomial R
h0 : motive 0
ha : ∀ (n : ℕ) (r : R) (q : SkewPolynomial R), n ∉ q.support → r ≠ 0 → motive q → motive ((monomial n) r + q)
⊢ motive 0

case ha
R : Type u_1
inst✝ : Semiring R
motive : SkewPolynomial R → Prop
p : SkewPolynomial R
h0 : motive 0
ha : ∀ (n : ℕ) (r : R) (q : SkewPolynomial R), n ∉ q.support → r ≠ 0 → motive q → motive ((monomial n) r + q)
⊢ ∀ (a : Multiplicative ℕ) (b : R) (f : SkewMonoidAlgebra R (Multiplicative ℕ)),
    a ∉ f.support → b ≠ 0 → motive f → motive (single a b + f)
Module: Mathlib.Algebra.SkewPolynomial.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
motive : SkewPolynomial R → Prop
p : SkewPolynomial R
h0 : motive 0
ha : ∀ (n : ℕ) (r : R) (q : SkewPolynomial R), n ∉ q.support → r ≠ 0 → motive q → motive ((monomial n) r + q)
⊢ motive p

Tactic:
by
  apply SkewMonoidAlgebra.induction <;> aesop

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

Goal state before:
pp: case succ
R : Type u_1
inst✝¹ : Semiring R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
a : R
n : ℕ
hn : (⇑φ)^[n] a = ofAdd n • a
⊢ (⇑φ)^[n + 1] a = ofAdd (n + 1) • a

Tactic:
simp_all [MulSemiringAction.toRingHom_apply, Function.iterate_succ', -Function.iterate_succ,
      ← mul_smul, mul_comm]

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

Goal state before:
pp: case comm
α : Type u_1
inst✝¹ : NonAssocSemiring α
inst✝ : StarRing α
T : CentroidHom α
⊢ ∀ (a : α), Commute (T 1) a

pp: case left_assoc
α : Type u_1
inst✝¹ : NonAssocSemiring α
inst✝ : StarRing α
T : CentroidHom α
⊢ ∀ (b c : α), T 1 * (b * c) = T 1 * b * c

pp: case right_assoc
α : Type u_1
inst✝¹ : NonAssocSemiring α
inst✝ : StarRing α
T : CentroidHom α
⊢ ∀ (a b : α), a * b * T 1 = a * (b * T 1)

Tactic:
<;>

Goal state after:
case comm
α : Type u_1
inst✝¹ : NonAssocSemiring α
inst✝ : StarRing α
T : CentroidHom α
⊢ ∀ (a : α), Commute (T 1) a

case left_assoc
α : Type u_1
inst✝¹ : NonAssocSemiring α
inst✝ : StarRing α
T : CentroidHom α
⊢ ∀ (b c : α), T 1 * (b * c) = T 1 * b * c

case right_assoc
α : Type u_1
inst✝¹ : NonAssocSemiring α
inst✝ : StarRing α
T : CentroidHom α
⊢ ∀ (a b : α), a * b * T 1 = a * (b * T 1)
Module: Mathlib.Algebra.SkewPolynomial.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
a n : ℕ
h : a.AtLeastTwo
⊢ (OfNat.ofNat a).coeff (n + 1) = 0

Tactic:
← Nat.cast_ofNat

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
a n : ℕ
h : a.AtLeastTwo
⊢ (↑(OfNat.ofNat a)).coeff (n + 1) = 0
Module: Mathlib.Algebra.SkewPolynomial.Basic

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : Semiring R
p : SkewPolynomial R
n : ℕ
a : R
inst✝ : DecidableEq R
h✝ : a = 0
⊢ Finset.map toAdd.toEmbedding ((SkewMonoidAlgebra.support p).erase (ofAdd n)) =
    (Finset.map toAdd.toEmbedding (SkewMonoidAlgebra.support p)).erase n

pp: case neg
R : Type u_1
inst✝¹ : Semiring R
p : SkewPolynomial R
n : ℕ
a : R
inst✝ : DecidableEq R
h✝ : ¬a = 0
⊢ Finset.map toAdd.toEmbedding (insert (ofAdd n) (SkewMonoidAlgebra.support p)) =
    insert n (Finset.map toAdd.toEmbedding (SkewMonoidAlgebra.support p))

Tactic:
<;>

Goal state after:
case pos
R : Type u_1
inst✝¹ : Semiring R
p : SkewPolynomial R
n : ℕ
a : R
inst✝ : DecidableEq R
h✝ : a = 0
⊢ Finset.map toAdd.toEmbedding ((SkewMonoidAlgebra.support p).erase (ofAdd n)) =
    (Finset.map toAdd.toEmbedding (SkewMonoidAlgebra.support p)).erase n

case neg
R : Type u_1
inst✝¹ : Semiring R
p : SkewPolynomial R
n : ℕ
a : R
inst✝ : DecidableEq R
h✝ : ¬a = 0
⊢ Finset.map toAdd.toEmbedding (insert (ofAdd n) (SkewMonoidAlgebra.support p)) =
    insert n (Finset.map toAdd.toEmbedding (SkewMonoidAlgebra.support p))
Module: Mathlib.Algebra.Star.TransferInstance

Goal state before:
pp: case star
R : Type u_1
S : Type u_2
e : R ≃ S
inst✝¹ : Mul S
inst✝ : StarMul S
this✝ : Star R := ⋯
this : Mul R := ⋯
⊢ ∀ (x : R), e (star x) = star (e x)

pp: case mul
R : Type u_1
S : Type u_2
e : R ≃ S
inst✝¹ : Mul S
inst✝ : StarMul S
this✝ : Star R := ⋯
this : Mul R := ⋯
⊢ ∀ (x y : R), e (x * y) = e x * e y

Tactic:
<;>

Goal state after:
case star
R : Type u_1
S : Type u_2
e : R ≃ S
inst✝¹ : Mul S
inst✝ : StarMul S
this✝ : Star R := ⋯
this : Mul R := ⋯
⊢ ∀ (x : R), e (star x) = star (e x)

case mul
R : Type u_1
S : Type u_2
e : R ≃ S
inst✝¹ : Mul S
inst✝ : StarMul S
this✝ : Star R := ⋯
this : Mul R := ⋯
⊢ ∀ (x y : R), e (x * y) = e x * e y
Module: Mathlib.Algebra.Star.TransferInstance

Goal state before:
pp: case star
R : Type u_1
S : Type u_2
e : R ≃ S
inst✝¹ : AddMonoid S
inst✝ : StarAddMonoid S
this✝ : Star R := ⋯
this : AddMonoid R := ⋯
⊢ ∀ (x : R), e (star x) = star (e x)

pp: case add
R : Type u_1
S : Type u_2
e : R ≃ S
inst✝¹ : AddMonoid S
inst✝ : StarAddMonoid S
this✝ : Star R := ⋯
this : AddMonoid R := ⋯
⊢ ∀ (x y : R), e (x + y) = e x + e y

Tactic:
<;>

Goal state after:
case star
R : Type u_1
S : Type u_2
e : R ≃ S
inst✝¹ : AddMonoid S
inst✝ : StarAddMonoid S
this✝ : Star R := ⋯
this : AddMonoid R := ⋯
⊢ ∀ (x : R), e (star x) = star (e x)

case add
R : Type u_1
S : Type u_2
e : R ≃ S
inst✝¹ : AddMonoid S
inst✝ : StarAddMonoid S
this✝ : Star R := ⋯
this : AddMonoid R := ⋯
⊢ ∀ (x y : R), e (x + y) = e x + e y
Module: Mathlib.Algebra.Star.TransferInstance

Goal state before:
pp: case star
R : Type u_1
S : Type u_2
e : R ≃ S
inst✝¹ : NonUnitalNonAssocSemiring S
inst✝ : StarRing S
this✝ : Star R := ⋯
this : NonUnitalNonAssocSemiring R := ⋯
⊢ ∀ (x : R), e (star x) = star (e x)

pp: case add
R : Type u_1
S : Type u_2
e : R ≃ S
inst✝¹ : NonUnitalNonAssocSemiring S
inst✝ : StarRing S
this✝ : Star R := ⋯
this : NonUnitalNonAssocSemiring R := ⋯
⊢ ∀ (x y : R), e (x + y) = e x + e y

pp: case mul
R : Type u_1
S : Type u_2
e : R ≃ S
inst✝¹ : NonUnitalNonAssocSemiring S
inst✝ : StarRing S
this✝ : Star R := ⋯
this : NonUnitalNonAssocSemiring R := ⋯
⊢ ∀ (x y : R), e (x * y) = e x * e y

Tactic:
<;>

Goal state after:
case star
R : Type u_1
S : Type u_2
e : R ≃ S
inst✝¹ : NonUnitalNonAssocSemiring S
inst✝ : StarRing S
this✝ : Star R := ⋯
this : NonUnitalNonAssocSemiring R := ⋯
⊢ ∀ (x : R), e (star x) = star (e x)

case add
R : Type u_1
S : Type u_2
e : R ≃ S
inst✝¹ : NonUnitalNonAssocSemiring S
inst✝ : StarRing S
this✝ : Star R := ⋯
this : NonUnitalNonAssocSemiring R := ⋯
⊢ ∀ (x y : R), e (x + y) = e x + e y

case mul
R : Type u_1
S : Type u_2
e : R ≃ S
inst✝¹ : NonUnitalNonAssocSemiring S
inst✝ : StarRing S
this✝ : Star R := ⋯
this : NonUnitalNonAssocSemiring R := ⋯
⊢ ∀ (x y : R), e (x * y) = e x * e y
Module: Mathlib.Algebra.Star.TransferInstance

Goal state before:
pp: case star
R : Type u_1
S : Type u_2
e : R ≃ S
𝕜 : Type u_3
inst✝³ : Star 𝕜
inst✝² : Star S
inst✝¹ : SMul 𝕜 S
inst✝ : StarModule 𝕜 S
this✝ : Star R := ⋯
this : SMul 𝕜 R := ⋯
⊢ ∀ (x : R), e (star x) = star (e x)

pp: case smul
R : Type u_1
S : Type u_2
e : R ≃ S
𝕜 : Type u_3
inst✝³ : Star 𝕜
inst✝² : Star S
inst✝¹ : SMul 𝕜 S
inst✝ : StarModule 𝕜 S
this✝ : Star R := ⋯
this : SMul 𝕜 R := ⋯
⊢ ∀ (r : 𝕜) (x : R), e (r • x) = r • e x

Tactic:
<;>

Goal state after:
case star
R : Type u_1
S : Type u_2
e : R ≃ S
𝕜 : Type u_3
inst✝³ : Star 𝕜
inst✝² : Star S
inst✝¹ : SMul 𝕜 S
inst✝ : StarModule 𝕜 S
this✝ : Star R := ⋯
this : SMul 𝕜 R := ⋯
⊢ ∀ (x : R), e (star x) = star (e x)

case smul
R : Type u_1
S : Type u_2
e : R ≃ S
𝕜 : Type u_3
inst✝³ : Star 𝕜
inst✝² : Star S
inst✝¹ : SMul 𝕜 S
inst✝ : StarModule 𝕜 S
this✝ : Star R := ⋯
this : SMul 𝕜 R := ⋯
⊢ ∀ (r : 𝕜) (x : R), e (r • x) = r • e x
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: case zero
k : Type u_1
G : Type u_2
inst✝¹ : One G
inst✝ : AddMonoidWithOne k
⊢ ↑0 = single 1 ↑0

pp: case succ
k : Type u_1
G : Type u_2
inst✝¹ : One G
inst✝ : AddMonoidWithOne k
n✝ : ℕ
a✝ : ↑n✝ = single 1 ↑n✝
⊢ ↑(n✝ + 1) = single 1 ↑(n✝ + 1)

Tactic:
<;>

Goal state after:
case zero
k : Type u_1
G : Type u_2
inst✝¹ : One G
inst✝ : AddMonoidWithOne k
⊢ ↑0 = single 1 ↑0

case succ
k : Type u_1
G : Type u_2
inst✝¹ : One G
inst✝ : AddMonoidWithOne k
n✝ : ℕ
a✝ : ↑n✝ = single 1 ↑n✝
⊢ ↑(n✝ + 1) = single 1 ↑(n✝ + 1)
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: case zero
k : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid k
M : Type u_3
inst✝ : AddZeroClass M
f g : SkewMonoidAlgebra k G →+ M
h : ∀ (a : G) (b : k), f (single a b) = g (single a b)
⊢ f 0 = g 0

pp: case single
k : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid k
M : Type u_3
inst✝ : AddZeroClass M
f g : SkewMonoidAlgebra k G →+ M
h : ∀ (a : G) (b : k), f (single a b) = g (single a b)
g✝ : G
a✝ : k
⊢ f (single g✝ a✝) = g (single g✝ a✝)

pp: case add
k : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid k
M : Type u_3
inst✝ : AddZeroClass M
f g : SkewMonoidAlgebra k G →+ M
h : ∀ (a : G) (b : k), f (single a b) = g (single a b)
f✝ g✝ : SkewMonoidAlgebra k G
a✝¹ : f f✝ = g f✝
a✝ : f g✝ = g g✝
⊢ f (f✝ + g✝) = g (f✝ + g✝)

Tactic:
<;>

Goal state after:
case zero
k : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid k
M : Type u_3
inst✝ : AddZeroClass M
f g : SkewMonoidAlgebra k G →+ M
h : ∀ (a : G) (b : k), f (single a b) = g (single a b)
⊢ f 0 = g 0

case single
k : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid k
M : Type u_3
inst✝ : AddZeroClass M
f g : SkewMonoidAlgebra k G →+ M
h : ∀ (a : G) (b : k), f (single a b) = g (single a b)
g✝ : G
a✝ : k
⊢ f (single g✝ a✝) = g (single g✝ a✝)

case add
k : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid k
M : Type u_3
inst✝ : AddZeroClass M
f g : SkewMonoidAlgebra k G →+ M
h : ∀ (a : G) (b : k), f (single a b) = g (single a b)
f✝ g✝ : SkewMonoidAlgebra k G
a✝¹ : f f✝ = g f✝
a✝ : f g✝ = g g✝
⊢ f (f✝ + g✝) = g (f✝ + g✝)
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: case ofNat
k : Type u_1
G : Type u_2
inst✝¹ : AddGroupWithOne k
inst✝ : One G
a✝ : ℕ
⊢ ↑(Int.ofNat a✝) = single 1 ↑(Int.ofNat a✝)

pp: case negSucc
k : Type u_1
G : Type u_2
inst✝¹ : AddGroupWithOne k
inst✝ : One G
a✝ : ℕ
⊢ ↑(Int.negSucc a✝) = single 1 ↑(Int.negSucc a✝)

Tactic:
<;>

Goal state after:
case ofNat
k : Type u_1
G : Type u_2
inst✝¹ : AddGroupWithOne k
inst✝ : One G
a✝ : ℕ
⊢ ↑(Int.ofNat a✝) = single 1 ↑(Int.ofNat a✝)

case negSucc
k : Type u_1
G : Type u_2
inst✝¹ : AddGroupWithOne k
inst✝ : One G
a✝ : ℕ
⊢ ↑(Int.negSucc a✝) = single 1 ↑(Int.negSucc a✝)