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

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
s : R
hs : s ≠ 0
h : IsSumSq s
⊢ IsSumNonzeroSq s

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : AddMonoid R
inst✝ : Mul R
x : R
hx : x ∈ {x | ∃ x_1, x_1 ≠ 0 ∧ x_1 * x_1 = x}
⊢ x ∈ ↑(sumNonzeroSq R)

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : AddMonoid R
inst✝ : Mul R
⊢ closure {x | ∃ x_1, x_1 ≠ 0 ∧ x_1 * x_1 = x} = sumNonzeroSq R

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : AddCommMonoid R
inst✝ : Mul R
hz : ∀ {a : R}, a * a = 0 → a = 0
ha : ∀ {s₁ s₂ : R}, IsSumSq s₁ → IsSumSq s₂ → s₁ + s₂ = 0 → s₁ = 0
this : ∀ (x : R), IsSumNonzeroSq x → x ≠ 0
⊢ ¬IsSumNonzeroSq 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : AddCommMonoid R
inst✝ : Mul R
hz : ∀ {a : R}, a * a = 0 → a = 0
ha : ∀ {s₁ s₂ : R}, IsSumSq s₁ → IsSumSq s₂ → s₁ + s₂ = 0 → s₁ = 0
⊢ ¬IsSumNonzeroSq 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Pointwise.Set

Goal state before:
pp: α : Type u_1
inst✝¹ : Mul α
inst✝ : HasDistribNeg α
x✝¹ x✝ : Set α
⊢ -x✝¹ * x✝ = -(x✝¹ * x✝)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Pointwise.Set

Goal state before:
pp: α : Type u_1
inst✝¹ : Mul α
inst✝ : HasDistribNeg α
x✝¹ x✝ : Set α
⊢ x✝¹ * -x✝ = -(x✝¹ * x✝)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
h : ∀ {s a : R}, IsSumSq s → a * a + s = 0 → a = 0
this : ∀ (x : R), IsSumNonzeroSq x → x ≠ 0
⊢ ¬IsSumNonzeroSq 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
h : ∀ {s a : R}, IsSumSq s → a * a + s = 0 → a = 0
x a✝ : R
ha : a✝ ≠ 0
hc : a✝ * a✝ = 0
⊢ a✝ * a✝ + 0 = 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
h : ∀ {s a : R}, IsSumSq s → a * a + s = 0 → a = 0
⊢ ¬IsSumNonzeroSq 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : IsFormallyReal R
⊢ 1 < 2

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : IsFormallyReal R
x : R
hx : x ^ 2 = 0
hc : x ≠ 0
⊢ IsSumNonzeroSq 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : IsFormallyReal R
⊢ IsReduced R

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : IsFormallyReal R
s₁ s₂ : R
hs₁ : IsSumSq s₁
hs₂ : IsSumSq s₂
h : s₁ + s₂ = 0
h₁ : s₁ ≠ 0
hc : s₂ = 0
⊢ False

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : IsFormallyReal R
s₁ s₂ : R
hs₁ : IsSumSq s₁
hs₂ : IsSumSq s₂
h : s₁ + s₂ = 0
⊢ s₁ = 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : IsFormallyReal R
s₁ s₂ : R
hs₁ : IsSumSq s₁
hs₂ : IsSumSq s₂
h : s₁ + s₂ = 0
⊢ s₂ = 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : NonUnitalNonAssocRing R
inst✝ : IsFormallyReal R
s : R
h₁ : IsSumSq s
h₂ : IsSumSq (-s)
⊢ s + -s = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Semireal.Defs

Goal state before:
pp: R : Type u_1
inst✝³ : AddGroup R
inst✝² : One R
inst✝¹ : Mul R
inst✝ : IsSemireal R
x✝ : IsSumSq (-1)
⊢ False

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Semireal.Defs

Goal state before:
pp: R : Type u_1
inst✝² : AddGroup R
inst✝¹ : One R
inst✝ : Mul R
h : ¬IsSumSq (-1)
⊢ ∀ {s : R}, IsSumSq s → 1 + s ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Semireal.Defs

Goal state before:
pp: R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : IsSemireal R
n : ℕ
hn : 1 + ↑n = 0
⊢ IsSumSq ↑n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Semireal.Defs

Goal state before:
pp: R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : IsSemireal R
n : ℕ
hn : ↑n = 0
⊢ n = 0

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: R : Type u
⊢ Function.Injective (@toNonUnitalRing R)

Tactic:
by

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

Goal state before:
pp: R : Type u
⊢ Function.Injective (@toNonAssocRing R)

Tactic:
by

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

Goal state before:
pp: R : Type u
⊢ Function.Injective (@toSemiring R)

Tactic:
by

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

Goal state before:
pp: R : Type u
⊢ Function.Injective (@toRing R)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M✝ : Type u_2
inst✝ : NonUnitalNonAssocRing R
M N : AddSubgroup R
x✝ : R
h : x✝ ∈ (M.toAddSubmonoid * N.toAddSubmonoid).carrier
m : R
hm : m ∈ M.toAddSubmonoid
n : R
hn : n ∈ N.toAddSubmonoid
⊢ -(m * n) ∈ (M.toAddSubmonoid * N.toAddSubmonoid).carrier

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M✝ : Type u_2
inst✝ : NonUnitalNonAssocRing R
M N : AddSubgroup R
x✝ : R
h : x✝ ∈ (M.toAddSubmonoid * N.toAddSubmonoid).carrier
r₁ r₂ : R
h₁ : -r₁ ∈ (M.toAddSubmonoid * N.toAddSubmonoid).carrier
h₂ : -r₂ ∈ (M.toAddSubmonoid * N.toAddSubmonoid).carrier
⊢ -(r₁ + r₂) ∈ (M.toAddSubmonoid * N.toAddSubmonoid).carrier

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : AddSubgroup M
⊢ 0 • s = ⊥

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Subring.IntPolynomial

Goal state before:
pp: K : Type u_1
inst✝ : Field K
R : Subring K
P : K[X]
hP : ∀ (n : ℕ), P.coeff n ∈ R
n : ℕ
⊢ n ∈ P.support ↔ ⟨P.coeff n, ⋯⟩ ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Subring.IntPolynomial

Goal state before:
pp: K : Type u_1
inst✝ : Field K
R : Subring K
P : K[X]
hP : ∀ (n : ℕ), P.coeff n ∈ R
⊢ (int R P hP).Monic ↔ P.Monic

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Subring.IntPolynomial

Goal state before:
pp: K : Type u_1
inst✝² : Field K
R : Subring K
P : K[X]
hP : ∀ (n : ℕ), P.coeff n ∈ R
L : Type u_2
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
n : ℕ
x✝ : n ∈ Finset.range (P.natDegree + 1)
⊢ (algebraMap (↥R) L) ((int R P hP).coeff n) * x ^ n = P.coeff n • x ^ n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Subring.IntPolynomial

Goal state before:
pp: K : Type u_1
inst✝² : Field K
R : Subring K
P : K[X]
hP : ∀ (n : ℕ), P.coeff n ∈ R
L : Type u_2
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
⊢ eval₂ (algebraMap (↥R) L) x (int R P hP) = (aeval x) P

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : Mul α
inst✝¹ : Add α
inst✝ : LeftDistribClass α
a b c : WithZero α
⊢ a * (b + c) = a * b + a * c

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : Mul α
inst✝¹ : Add α
inst✝ : RightDistribClass α
a b c : WithZero α
⊢ (a + b) * c = a * c + b * c

Tactic:
by

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

Goal state before:
pp: F : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
f g : CentroidHom α
h : (fun f ↦ (↑f.toAddMonoidHom).toFun) f = (fun f ↦ (↑f.toAddMonoidHom).toFun) g
⊢ f = g

Tactic:
by

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

Goal state before:
pp: F : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
f : CentroidHom α
f' : α → α
h : f' = ⇑f
a b : α
⊢ f' (a * b) = a * f' b

Tactic:
by

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

Goal state before:
pp: F : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
f : CentroidHom α
f' : α → α
h : f' = ⇑f
a b : α
⊢ f' (a * b) = f' a * b

Tactic:
by

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

Goal state before:
pp: α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
g f₁ f₂ : CentroidHom α
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ g (f₁ a) = g (f₂ a)

Tactic:
by

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

Goal state before:
pp: F : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
f g : CentroidHom α
a b : α
⊢ (↑(↑f + ↑g)).toFun (a * b) = a * (↑(↑f + ↑g)).toFun b

Tactic:
by

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

Goal state before:
pp: F : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
f g : CentroidHom α
a b : α
⊢ (↑(↑f + ↑g)).toFun (a * b) = (↑(↑f + ↑g)).toFun a * b

Tactic:
by

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

Goal state before:
pp: F : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
α : Type u_5
inst✝¹² : NonUnitalNonAssocSemiring α
inst✝¹¹ : Monoid M
inst✝¹⁰ : Monoid N
inst✝⁹ : Semiring R
inst✝⁸ : DistribMulAction M α
inst✝⁷ : SMulCommClass M α α
inst✝⁶ : IsScalarTower M α α
inst✝⁵ : DistribMulAction N α
inst✝⁴ : SMulCommClass N α α
inst✝³ : IsScalarTower N α α
inst✝² : Module R α
inst✝¹ : SMulCommClass R α α
inst✝ : IsScalarTower R α α
n : M
f : CentroidHom α
a b : α
⊢ (↑(n • ↑f)).toFun (a * b) = a * (↑(n • ↑f)).toFun b

Tactic:
by

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

Goal state before:
pp: F : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
α : Type u_5
inst✝¹² : NonUnitalNonAssocSemiring α
inst✝¹¹ : Monoid M
inst✝¹⁰ : Monoid N
inst✝⁹ : Semiring R
inst✝⁸ : DistribMulAction M α
inst✝⁷ : SMulCommClass M α α
inst✝⁶ : IsScalarTower M α α
inst✝⁵ : DistribMulAction N α
inst✝⁴ : SMulCommClass N α α
inst✝³ : IsScalarTower N α α
inst✝² : Module R α
inst✝¹ : SMulCommClass R α α
inst✝ : IsScalarTower R α α
n : M
f : CentroidHom α
a b : α
⊢ (↑(n • ↑f)).toFun (a * b) = (↑(n • ↑f)).toFun a * b

Tactic:
by

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

Goal state before:
pp: F : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
α : Type u_5
inst✝¹² : NonUnitalNonAssocSemiring α
inst✝¹¹ : Monoid M
inst✝¹⁰ : Monoid N
inst✝⁹ : Semiring R
inst✝⁸ : DistribMulAction M α
inst✝⁷ : SMulCommClass M α α
inst✝⁶ : IsScalarTower M α α
inst✝⁵ : DistribMulAction N α
inst✝⁴ : SMulCommClass N α α
inst✝³ : IsScalarTower N α α
inst✝² : Module R α
inst✝¹ : SMulCommClass R α α
inst✝ : IsScalarTower R α α
f : CentroidHom α
n : ℕ
a b : α
⊢ (↑(f.toEnd ^ n)).toFun (a * b) = a * (↑(f.toEnd ^ n)).toFun b

Tactic:
by

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

Goal state before:
pp: F : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
α : Type u_5
inst✝¹² : NonUnitalNonAssocSemiring α
inst✝¹¹ : Monoid M
inst✝¹⁰ : Monoid N
inst✝⁹ : Semiring R
inst✝⁸ : DistribMulAction M α
inst✝⁷ : SMulCommClass M α α
inst✝⁶ : IsScalarTower M α α
inst✝⁵ : DistribMulAction N α
inst✝⁴ : SMulCommClass N α α
inst✝³ : IsScalarTower N α α
inst✝² : Module R α
inst✝¹ : SMulCommClass R α α
inst✝ : IsScalarTower R α α
f : CentroidHom α
n : ℕ
a b : α
⊢ (↑(f.toEnd ^ n)).toFun (a * b) = (↑(f.toEnd ^ n)).toFun a * b

Tactic:
by

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

Goal state before:
pp: α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
T S : CentroidHom α
a b : α
⊢ (⇑T ∘ ⇑S) (a * b) = (⇑S ∘ ⇑T) (a * b)

Tactic:
by

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

Goal state before:
pp: α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
⊢ (toEndRingHom α).rangeS = Subsemiring.centralizer (Set.range ⇑L ∪ Set.range ⇑R)

Tactic:
by

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

Goal state before:
pp: F : Type u_1
M : Type u_2
N : Type u_3
R✝ : Type u_4
α : Type u_5
inst✝¹⁶ : NonUnitalNonAssocSemiring α
inst✝¹⁵ : Monoid M
inst✝¹⁴ : Monoid N
inst✝¹³ : Semiring R✝
inst✝¹² : DistribMulAction M α
inst✝¹¹ : SMulCommClass M α α
inst✝¹⁰ : IsScalarTower M α α
inst✝⁹ : DistribMulAction N α
inst✝⁸ : SMulCommClass N α α
inst✝⁷ : IsScalarTower N α α
inst✝⁶ : Module R✝ α
inst✝⁵ : SMulCommClass R✝ α α
inst✝⁴ : IsScalarTower R✝ α α
R : Type u_6
inst✝³ : CommSemiring «R»
inst✝² : Module «R» α
inst✝¹ : SMulCommClass «R» α α
inst✝ : IsScalarTower «R» α α
z : ↥(NonUnitalSubsemiring.center α)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
by

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

Goal state before:
pp: F : Type u_1
M : Type u_2
N : Type u_3
R✝ : Type u_4
α : Type u_5
inst✝¹⁶ : NonUnitalNonAssocSemiring α
inst✝¹⁵ : Monoid M
inst✝¹⁴ : Monoid N
inst✝¹³ : Semiring R✝
inst✝¹² : DistribMulAction M α
inst✝¹¹ : SMulCommClass M α α
inst✝¹⁰ : IsScalarTower M α α
inst✝⁹ : DistribMulAction N α
inst✝⁸ : SMulCommClass N α α
inst✝⁷ : IsScalarTower N α α
inst✝⁶ : Module R✝ α
inst✝⁵ : SMulCommClass R✝ α α
inst✝⁴ : IsScalarTower R✝ α α
R : Type u_6
inst✝³ : CommSemiring «R»
inst✝² : Module «R» α
inst✝¹ : SMulCommClass «R» α α
inst✝ : IsScalarTower «R» α α
z₁ z₂ : ↥(NonUnitalSubsemiring.center α)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
by

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

Goal state before:
pp: F : Type u_1
M : Type u_2
N : Type u_3
R✝ : Type u_4
α : Type u_5
inst✝¹⁶ : NonUnitalNonAssocSemiring α
inst✝¹⁵ : Monoid M
inst✝¹⁴ : Monoid N
inst✝¹³ : Semiring R✝
inst✝¹² : DistribMulAction M α
inst✝¹¹ : SMulCommClass M α α
inst✝¹⁰ : IsScalarTower M α α
inst✝⁹ : DistribMulAction N α
inst✝⁸ : SMulCommClass N α α
inst✝⁷ : IsScalarTower N α α
inst✝⁶ : Module R✝ α
inst✝⁵ : SMulCommClass R✝ α α
inst✝⁴ : IsScalarTower R✝ α α
R : Type u_6
inst✝³ : CommSemiring «R»
inst✝² : Module «R» α
inst✝¹ : SMulCommClass «R» α α
inst✝ : IsScalarTower «R» α α
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
by

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

Goal state before:
pp: F : Type u_1
M : Type u_2
N : Type u_3
R✝ : Type u_4
α : Type u_5
inst✝¹⁶ : NonUnitalNonAssocSemiring α
inst✝¹⁵ : Monoid M
inst✝¹⁴ : Monoid N
inst✝¹³ : Semiring R✝
inst✝¹² : DistribMulAction M α
inst✝¹¹ : SMulCommClass M α α
inst✝¹⁰ : IsScalarTower M α α
inst✝⁹ : DistribMulAction N α
inst✝⁸ : SMulCommClass N α α
inst✝⁷ : IsScalarTower N α α
inst✝⁶ : Module R✝ α
inst✝⁵ : SMulCommClass R✝ α α
inst✝⁴ : IsScalarTower R✝ α α
R : Type u_6
inst✝³ : CommSemiring «R»
inst✝² : Module «R» α
inst✝¹ : SMulCommClass «R» α α
inst✝ : IsScalarTower «R» α α
x✝¹ x✝ : ↥(NonUnitalSubsemiring.center α)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
by

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

Goal state before:
pp: F : Type u_1
M : Type u_2
N : Type u_3
R✝ : Type u_4
α : Type u_5
inst✝¹⁶ : NonUnitalNonAssocSemiring α
inst✝¹⁵ : Monoid M
inst✝¹⁴ : Monoid N
inst✝¹³ : Semiring R✝
inst✝¹² : DistribMulAction M α
inst✝¹¹ : SMulCommClass M α α
inst✝¹⁰ : IsScalarTower M α α
inst✝⁹ : DistribMulAction N α
inst✝⁸ : SMulCommClass N α α
inst✝⁷ : IsScalarTower N α α
inst✝⁶ : Module R✝ α
inst✝⁵ : SMulCommClass R✝ α α
inst✝⁴ : IsScalarTower R✝ α α
R : Type u_6
inst✝³ : CommSemiring «R»
inst✝² : Module «R» α
inst✝¹ : SMulCommClass «R» α α
inst✝ : IsScalarTower «R» α α
f g : ↥(Subsemiring.center (CentroidHom α))
h : (fun f ↦ (↑(↑f).toAddMonoidHom).toFun) f = (fun f ↦ (↑(↑f).toAddMonoidHom).toFun) g
⊢ f = g

Tactic:
by

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

Goal state before:
pp: α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
a : α
⊢ a ∈ NonUnitalSubsemiring.center α ↔ R a = L a ∧ L a ∈ (toEndRingHom α).rangeS

Tactic:
by

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

Goal state before:
pp: α : Type u_5
inst✝ : NonUnitalNonAssocCommSemiring α
a : α
⊢ a ∈ NonUnitalSubsemiring.center α ↔ ∀ (b : α), Commute (L b) (L a)

Tactic:
by

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

Goal state before:
pp: F : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
α : Type u_5
inst✝ : NonAssocSemiring α
T : CentroidHom α
⊢ T 1 ∈ Subsemiring.center α

Tactic:
by

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

Goal state before:
pp: F : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
α : Type u_5
inst✝ : NonAssocSemiring α
z : ↥(Subsemiring.center α)
⊢ ↑((fun T ↦ ⟨T 1, ⋯⟩) (centerToCentroid.toFun z)) = ↑z

Tactic:
by

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

Goal state before:
pp: F : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
α : Type u_5
inst✝ : NonAssocSemiring α
T : CentroidHom α
x✝ : α
⊢ (centerToCentroid.toFun ((fun T ↦ ⟨T 1, ⋯⟩) T)) x✝ = T x✝

Tactic:
by

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

Goal state before:
pp: F : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
α : Type u_5
inst✝ : NonUnitalNonAssocRing α
f : CentroidHom α
a b : α
⊢ (↑(-↑f)).toFun (a * b) = a * (↑(-↑f)).toFun b

Tactic:
by

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

Goal state before:
pp: F : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
α : Type u_5
inst✝ : NonUnitalNonAssocRing α
f : CentroidHom α
a b : α
⊢ (↑(-↑f)).toFun (a * b) = (↑(-↑f)).toFun a * b

Tactic:
by

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

Goal state before:
pp: F : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
α : Type u_5
inst✝ : NonUnitalNonAssocRing α
f g : CentroidHom α
a b : α
⊢ (↑(↑f - ↑g)).toFun (a * b) = a * (↑(↑f - ↑g)).toFun b

Tactic:
by

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

Goal state before:
pp: F : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
α : Type u_5
inst✝ : NonUnitalNonAssocRing α
f g : CentroidHom α
a b : α
⊢ (↑(↑f - ↑g)).toFun (a * b) = (↑(↑f - ↑g)).toFun a * b

Tactic:
by

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

Goal state before:
pp: F : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
α : Type u_5
inst✝ : NonUnitalRing α
h : ∀ (a b : α), (∀ (r : α), a * r * b = 0) → a = 0 ∨ b = 0
f g : CentroidHom α
⊢ f * g = g * f

Tactic:
by

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

Goal state before:
pp: k : Type u_1
G : Type u_2
H : Type u_3
inst✝⁸ : CommSemiring k
inst✝⁷ : Monoid G
inst✝⁶ : Monoid H
A : Type u_4
B : Type u_5
inst✝⁵ : Semiring A
inst✝⁴ : Algebra k A
inst✝³ : Semiring B
inst✝² : Algebra k B
inst✝¹ : MulSemiringAction G A
inst✝ : SMulCommClass G k A
f : A →ₐ[k] B
g : G →* B
h_comm : ∀ {x : A} {y : G}, f (y • x) * g y = g y * f x
⊢ ∀ (r : k), (↑↑(liftNCRingHom (↑f) g ⋯)).toFun ((algebraMap k (SkewMonoidAlgebra A G)) r) = (algebraMap k B) r

Tactic:
by

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

Goal state before:
pp: k : Type u_1
G : Type u_2
H : Type u_3
inst✝⁸ : CommSemiring k
inst✝⁷ : Monoid G
inst✝⁶ : Monoid H
A : Type u_4
B : Type u_5
inst✝⁵ : Semiring A
inst✝⁴ : Algebra k A
inst✝³ : Semiring B
inst✝² : Algebra k B
inst✝¹ : MulSemiringAction G k
inst✝ : SMulCommClass G k k
F : G →* A
⊢ SkewMonoidAlgebra k G →ₐ[k] A

Tactic:
by

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

Goal state before:
pp: k : Type u_1
G : Type u_2
H : Type u_3
inst✝⁸ : CommSemiring k
inst✝⁷ : Monoid G
inst✝⁶ : Monoid H
A : Type u_4
B : Type u_5
inst✝⁵ : Semiring A
inst✝⁴ : Algebra k A
inst✝³ : Semiring B
inst✝² : Algebra k B
inst✝¹ : MulSemiringAction G k
inst✝ : SMulCommClass G k k
f : G →* A
⊢ (fun f ↦ (↑f).comp (of k G)) ((fun F ↦ liftNCAlgHom (Algebra.ofId k A) F ⋯) f) = f

Tactic:
by

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

Goal state before:
pp: k : Type u_1
G : Type u_2
H : Type u_3
inst✝⁸ : CommSemiring k
inst✝⁷ : Monoid G
inst✝⁶ : Monoid H
A : Type u_4
B : Type u_5
inst✝⁵ : Semiring A
inst✝⁴ : Algebra k A
inst✝³ : Semiring B
inst✝² : Algebra k B
inst✝¹ : MulSemiringAction G k
inst✝ : SMulCommClass G k k
F : SkewMonoidAlgebra k G →ₐ[k] A
⊢ (fun F ↦ liftNCAlgHom (Algebra.ofId k A) F ⋯) ((fun f ↦ (↑f).comp (of k G)) F) = F

Tactic:
by

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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝⁵ : CommSemiring k
inst✝⁴ : Monoid G
A : Type u_4
inst✝³ : Semiring A
inst✝² : Algebra k A
inst✝¹ : MulSemiringAction G k
inst✝ : SMulCommClass G k k
F : G →* A
f : SkewMonoidAlgebra k G
⊢ ((lift k G A) F) f = f.sum fun a b ↦ b • F a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: R : Type uR
inst✝ : Semiring R
r : R → R → Prop
a b c : R
h : Rel r b c
⊢ Rel r (a + b) (a + c)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: R : Type uR
inst✝ : Ring R
r : R → R → Prop
a b : R
h : Rel r a b
⊢ Rel r (-a) (-b)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: R : Type uR
inst✝ : Ring R
r : R → R → Prop
a b c : R
h : Rel r a b
⊢ Rel r (a - c) (b - c)

Tactic:
by

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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝⁵ : CommSemiring k
inst✝⁴ : Monoid G
A : Type u_4
inst✝³ : Semiring A
inst✝² : Algebra k A
inst✝¹ : MulSemiringAction G k
inst✝ : SMulCommClass G k k
F : G →* A
x : G
⊢ ((lift k G A) F) ((of k G) x) = F x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: R : Type uR
inst✝ : Ring R
r : R → R → Prop
a b c : R
h : Rel r b c
⊢ Rel r (a - b) (a - c)

Tactic:
by

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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝⁵ : CommSemiring k
inst✝⁴ : Monoid G
A : Type u_4
inst✝³ : Semiring A
inst✝² : Algebra k A
inst✝¹ : MulSemiringAction G k
inst✝ : SMulCommClass G k k
F : G →* A
a : G
b : k
⊢ ((lift k G A) F) (single a b) = b • F a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: S : Type uS
inst✝² : CommSemiring S
A : Type uA
inst✝¹ : Semiring A
inst✝ : Algebra S A
r : A → A → Prop
k : S
a b : A
h : Rel r a b
⊢ Rel r (k • a) (k • b)

Tactic:
by

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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝⁵ : CommSemiring k
inst✝⁴ : Monoid G
A : Type u_4
inst✝³ : Semiring A
inst✝² : Algebra k A
inst✝¹ : MulSemiringAction G k
inst✝ : SMulCommClass G k k
F : SkewMonoidAlgebra k G →ₐ[k] A
f : SkewMonoidAlgebra k G
⊢ F f = f.sum fun a b ↦ b • F (single a 1)

Tactic:
by

Goal state after: