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

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

Tactic:
;

Goal state after:
α : Type u_1
inst✝¹ : Mul α
inst✝ : HasDistribNeg α
x✝¹ x✝ : Set α
⊢ (fun x ↦ -x) '' x✝¹ * x✝ = (fun x ↦ -x) '' (x✝¹ * x✝)
Module: Mathlib.Algebra.Ring.Pointwise.Set

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

Tactic:
;

Goal state after:
α : Type u_1
inst✝¹ : Mul α
inst✝ : HasDistribNeg α
x✝¹ x✝ : Set α
⊢ x✝¹ * (fun x ↦ -x) '' x✝ = (fun x ↦ -x) '' (x✝¹ * x✝)
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
toNonUnitalNonAssocSemiring✝¹ : NonUnitalNonAssocSemiring R
mul_comm✝¹ : ∀ (a b : R), a * b = b * a
toNonUnitalNonAssocSemiring✝ : NonUnitalNonAssocSemiring R
mul_comm✝ : ∀ (a b : R), a * b = b * a
a✝ :
  { toNonUnitalNonAssocSemiring := toNonUnitalNonAssocSemiring✝¹, mul_comm := mul_comm✝¹ }.toNonUnitalNonAssocSemiring =
    { toNonUnitalNonAssocSemiring := toNonUnitalNonAssocSemiring✝, mul_comm := mul_comm✝ }.toNonUnitalNonAssocSemiring
⊢ { toNonUnitalNonAssocSemiring := toNonUnitalNonAssocSemiring✝¹, mul_comm := mul_comm✝¹ } =
    { toNonUnitalNonAssocSemiring := toNonUnitalNonAssocSemiring✝, mul_comm := mul_comm✝ }

Tactic:
;

Goal state after:
R : Type u
toNonUnitalNonAssocSemiring✝¹ : NonUnitalNonAssocSemiring R
mul_comm✝¹ : ∀ (a b : R), a * b = b * a
toNonUnitalNonAssocSemiring✝ : NonUnitalNonAssocSemiring R
mul_comm✝ : ∀ (a b : R), a * b = b * a
a✝ :
  { toNonUnitalNonAssocSemiring := toNonUnitalNonAssocSemiring✝¹, mul_comm := mul_comm✝¹ }.toNonUnitalNonAssocSemiring =
    { toNonUnitalNonAssocSemiring := toNonUnitalNonAssocSemiring✝, mul_comm := mul_comm✝ }.toNonUnitalNonAssocSemiring
⊢ { toNonUnitalNonAssocSemiring := toNonUnitalNonAssocSemiring✝¹, mul_comm := mul_comm✝¹ } =
    { toNonUnitalNonAssocSemiring := toNonUnitalNonAssocSemiring✝, mul_comm := mul_comm✝ }
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
toNonUnitalSemiring✝¹ : NonUnitalSemiring R
mul_comm✝¹ : ∀ (a b : R), a * b = b * a
toNonUnitalSemiring✝ : NonUnitalSemiring R
mul_comm✝ : ∀ (a b : R), a * b = b * a
a✝ :
  { toNonUnitalSemiring := toNonUnitalSemiring✝¹, mul_comm := mul_comm✝¹ }.toNonUnitalSemiring =
    { toNonUnitalSemiring := toNonUnitalSemiring✝, mul_comm := mul_comm✝ }.toNonUnitalSemiring
⊢ { toNonUnitalSemiring := toNonUnitalSemiring✝¹, mul_comm := mul_comm✝¹ } =
    { toNonUnitalSemiring := toNonUnitalSemiring✝, mul_comm := mul_comm✝ }

Tactic:
;

Goal state after:
R : Type u
toNonUnitalSemiring✝¹ : NonUnitalSemiring R
mul_comm✝¹ : ∀ (a b : R), a * b = b * a
toNonUnitalSemiring✝ : NonUnitalSemiring R
mul_comm✝ : ∀ (a b : R), a * b = b * a
a✝ :
  { toNonUnitalSemiring := toNonUnitalSemiring✝¹, mul_comm := mul_comm✝¹ }.toNonUnitalSemiring =
    { toNonUnitalSemiring := toNonUnitalSemiring✝, mul_comm := mul_comm✝ }.toNonUnitalSemiring
⊢ { toNonUnitalSemiring := toNonUnitalSemiring✝¹, mul_comm := mul_comm✝¹ } =
    { toNonUnitalSemiring := toNonUnitalSemiring✝, mul_comm := mul_comm✝ }
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
toNonUnitalNonAssocRing✝¹ : NonUnitalNonAssocRing R
mul_comm✝¹ : ∀ (a b : R), a * b = b * a
toNonUnitalNonAssocRing✝ : NonUnitalNonAssocRing R
mul_comm✝ : ∀ (a b : R), a * b = b * a
a✝ :
  { toNonUnitalNonAssocRing := toNonUnitalNonAssocRing✝¹, mul_comm := mul_comm✝¹ }.toNonUnitalNonAssocRing =
    { toNonUnitalNonAssocRing := toNonUnitalNonAssocRing✝, mul_comm := mul_comm✝ }.toNonUnitalNonAssocRing
⊢ { toNonUnitalNonAssocRing := toNonUnitalNonAssocRing✝¹, mul_comm := mul_comm✝¹ } =
    { toNonUnitalNonAssocRing := toNonUnitalNonAssocRing✝, mul_comm := mul_comm✝ }

Tactic:
;

Goal state after:
R : Type u
toNonUnitalNonAssocRing✝¹ : NonUnitalNonAssocRing R
mul_comm✝¹ : ∀ (a b : R), a * b = b * a
toNonUnitalNonAssocRing✝ : NonUnitalNonAssocRing R
mul_comm✝ : ∀ (a b : R), a * b = b * a
a✝ :
  { toNonUnitalNonAssocRing := toNonUnitalNonAssocRing✝¹, mul_comm := mul_comm✝¹ }.toNonUnitalNonAssocRing =
    { toNonUnitalNonAssocRing := toNonUnitalNonAssocRing✝, mul_comm := mul_comm✝ }.toNonUnitalNonAssocRing
⊢ { toNonUnitalNonAssocRing := toNonUnitalNonAssocRing✝¹, mul_comm := mul_comm✝¹ } =
    { toNonUnitalNonAssocRing := toNonUnitalNonAssocRing✝, mul_comm := mul_comm✝ }
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
toNonUnitalRing✝¹ : NonUnitalRing R
mul_comm✝¹ : ∀ (a b : R), a * b = b * a
toNonUnitalRing✝ : NonUnitalRing R
mul_comm✝ : ∀ (a b : R), a * b = b * a
a✝ :
  { toNonUnitalRing := toNonUnitalRing✝¹, mul_comm := mul_comm✝¹ }.toNonUnitalRing =
    { toNonUnitalRing := toNonUnitalRing✝, mul_comm := mul_comm✝ }.toNonUnitalRing
⊢ { toNonUnitalRing := toNonUnitalRing✝¹, mul_comm := mul_comm✝¹ } =
    { toNonUnitalRing := toNonUnitalRing✝, mul_comm := mul_comm✝ }

Tactic:
;

Goal state after:
R : Type u
toNonUnitalRing✝¹ : NonUnitalRing R
mul_comm✝¹ : ∀ (a b : R), a * b = b * a
toNonUnitalRing✝ : NonUnitalRing R
mul_comm✝ : ∀ (a b : R), a * b = b * a
a✝ :
  { toNonUnitalRing := toNonUnitalRing✝¹, mul_comm := mul_comm✝¹ }.toNonUnitalRing =
    { toNonUnitalRing := toNonUnitalRing✝, mul_comm := mul_comm✝ }.toNonUnitalRing
⊢ { toNonUnitalRing := toNonUnitalRing✝¹, mul_comm := mul_comm✝¹ } =
    { toNonUnitalRing := toNonUnitalRing✝, mul_comm := mul_comm✝ }
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
toSemiring✝¹ : Semiring R
mul_comm✝¹ : ∀ (a b : R), a * b = b * a
toSemiring✝ : Semiring R
mul_comm✝ : ∀ (a b : R), a * b = b * a
a✝ :
  { toSemiring := toSemiring✝¹, mul_comm := mul_comm✝¹ }.toSemiring =
    { toSemiring := toSemiring✝, mul_comm := mul_comm✝ }.toSemiring
⊢ { toSemiring := toSemiring✝¹, mul_comm := mul_comm✝¹ } = { toSemiring := toSemiring✝, mul_comm := mul_comm✝ }

Tactic:
;

Goal state after:
R : Type u
toSemiring✝¹ : Semiring R
mul_comm✝¹ : ∀ (a b : R), a * b = b * a
toSemiring✝ : Semiring R
mul_comm✝ : ∀ (a b : R), a * b = b * a
a✝ :
  { toSemiring := toSemiring✝¹, mul_comm := mul_comm✝¹ }.toSemiring =
    { toSemiring := toSemiring✝, mul_comm := mul_comm✝ }.toSemiring
⊢ { toSemiring := toSemiring✝¹, mul_comm := mul_comm✝¹ } = { toSemiring := toSemiring✝, mul_comm := mul_comm✝ }
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
toRing✝¹ : Ring R
mul_comm✝¹ : ∀ (a b : R), a * b = b * a
toRing✝ : Ring R
mul_comm✝ : ∀ (a b : R), a * b = b * a
a✝ : { toRing := toRing✝¹, mul_comm := mul_comm✝¹ }.toRing = { toRing := toRing✝, mul_comm := mul_comm✝ }.toRing
⊢ { toRing := toRing✝¹, mul_comm := mul_comm✝¹ } = { toRing := toRing✝, mul_comm := mul_comm✝ }

Tactic:
;

Goal state after:
R : Type u
toRing✝¹ : Ring R
mul_comm✝¹ : ∀ (a b : R), a * b = b * a
toRing✝ : Ring R
mul_comm✝ : ∀ (a b : R), a * b = b * a
a✝ : { toRing := toRing✝¹, mul_comm := mul_comm✝¹ }.toRing = { toRing := toRing✝, mul_comm := mul_comm✝ }.toRing
⊢ { toRing := toRing✝¹, mul_comm := mul_comm✝¹ } = { toRing := toRing✝, mul_comm := mul_comm✝ }
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:
;

Goal state after:
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
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:
;

Goal state after:
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
Module: Mathlib.Algebra.Ring.WithZero

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

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

Tactic:
;

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

case coe
α : Type u_1
inst✝² : Mul α
inst✝¹ : Add α
inst✝ : LeftDistribClass α
b c : WithZero α
a✝ : α
⊢ ↑a✝ * (b + c) = ↑a✝ * b + ↑a✝ * c
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 = (algebraMap K L) (P.coeff n) * x ^ n

Tactic:
;

Goal state after:
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 = (algebraMap K L) (P.coeff n) * x ^ n
Module: Mathlib.Algebra.Ring.WithZero

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

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

Tactic:
;

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

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

Goal state before:
pp: case refine_2
α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
T : AddMonoid.End α
h : ∀ g ∈ Set.range ⇑L ∪ Set.range ⇑R, g * T = T * g
⊢ T ∈ (toEndRingHom α).rangeS

Tactic:
refine ⟨⟨T, fun a b ↦ ?_, fun a b ↦ ?_⟩, rfl⟩

Goal state after:
case refine_2.refine_1
α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
T : AddMonoid.End α
h : ∀ g ∈ Set.range ⇑L ∪ Set.range ⇑R, g * T = T * g
a b : α
⊢ (↑T).toFun (a * b) = a * (↑T).toFun b

case refine_2.refine_2
α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
T : AddMonoid.End α
h : ∀ g ∈ Set.range ⇑L ∪ Set.range ⇑R, g * T = T * g
a b : α
⊢ (↑T).toFun (a * b) = (↑T).toFun a * b
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 α)
a : α
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
;

Goal state after:
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 α)
a : α
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.Algebra.SkewMonoidAlgebra.Lift

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝ : AddCommMonoid k
G' : Type u_4
G'' : Type u_5
f : G ≃ G'
g : G' ≃ G''
l : SkewMonoidAlgebra k G
x : G''
⊢ (equivMapDomain (f.trans g) l).coeff x = (equivMapDomain g (equivMapDomain f l)).coeff x

Tactic:
;

Goal state after:
k : Type u_1
G : Type u_2
inst✝ : AddCommMonoid k
G' : Type u_4
G'' : Type u_5
f : G ≃ G'
g : G' ≃ G''
l : SkewMonoidAlgebra k G
x : G''
⊢ (equivMapDomain (f.trans g) l).coeff x = (equivMapDomain g (equivMapDomain f l)).coeff x
Module: Mathlib.Algebra.SkewMonoidAlgebra.Lift

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝ : AddCommMonoid k
l : SkewMonoidAlgebra k G
x : G
⊢ (equivMapDomain (Equiv.refl G) l).coeff x = l.coeff x

Tactic:
;

Goal state after:
k : Type u_1
G : Type u_2
inst✝ : AddCommMonoid k
l : SkewMonoidAlgebra k G
x : G
⊢ (equivMapDomain (Equiv.refl G) l).coeff x = l.coeff x
Module: Mathlib.Algebra.SkewMonoidAlgebra.Single

Goal state before:
pp: M : Type u_4
α : Type u_5
inst✝¹ : AddCommMonoid M
a : α
f : SkewMonoidAlgebra M α
inst✝ : DecidableEq α
a✝ : α
⊢ a✝ ∈ ((erase a) f).support ↔ a✝ ∈ f.support.erase a

Tactic:
;

Goal state after:
M : Type u_4
α : Type u_5
inst✝¹ : AddCommMonoid M
a : α
f : SkewMonoidAlgebra M α
inst✝ : DecidableEq α
a✝ : α
⊢ a✝ ∈ ((erase a) f).support ↔ a✝ ∈ f.support.erase a
Module: Mathlib.Algebra.SkewMonoidAlgebra.Single

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

Tactic:
;

Goal state after:
M : Type u_4
α : Type u_5
inst✝ : AddCommMonoid M
a : α
f : SkewMonoidAlgebra M α
a✝ : α
⊢ (single a (f.coeff a) + (erase a) f).coeff a✝ = f.coeff a✝
Module: Mathlib.Algebra.SkewMonoidAlgebra.Single

Goal state before:
pp: M : Type u_4
α : Type u_5
inst✝ : AddCommMonoid M
f : SkewMonoidAlgebra M α
a a✝ : α
⊢ (f.update a (f.coeff a)).coeff a✝ = f.coeff a✝

Tactic:
;

Goal state after:
M : Type u_4
α : Type u_5
inst✝ : AddCommMonoid M
f : SkewMonoidAlgebra M α
a a✝ : α
⊢ (f.update a (f.coeff a)).coeff a✝ = f.coeff a✝
Module: Mathlib.Algebra.SkewMonoidAlgebra.Single

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

Tactic:
;

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

Goal state before:
pp: R : Type uR
inst✝³ : Semiring R
S : Type uS
inst✝² : CommSemiring S
T : Type uT
A : Type uA
inst✝¹ : Semiring A
inst✝ : Algebra S A
r✝ r : R → R → Prop
⊢ ∀ (x : RingQuot r), 0 • x = 0

Tactic:
by
    rintro ⟨⟨⟩⟩
    simp only [smul_quot, zero_smul, zero_quot]

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

Goal state before:
pp: M : Type u_4
α : Type u_5
inst✝ : AddCommMonoid M
f : SkewMonoidAlgebra M α
a a✝ : α
⊢ (f.update a 0).coeff a✝ = ((erase a) f).coeff a✝

Tactic:
;

Goal state after:
M : Type u_4
α : Type u_5
inst✝ : AddCommMonoid M
f : SkewMonoidAlgebra M α
a a✝ : α
⊢ (f.update a 0).coeff a✝ = ((erase a) f).coeff a✝
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: R : Type uR
inst✝⁴ : Semiring R
S : Type uS
inst✝³ : CommSemiring S
T : Type uT
A : Type uA
inst✝² : Semiring A
inst✝¹ : Algebra S A
r : R → R → Prop
inst✝ : Semiring T
s : A → A → Prop
x✝ : S
⊢ (↑↑(mkRingHom s)).toFun ((algebraMap S A) x✝) = (algebraMap S (RingQuot s)) x✝

Tactic:
simp [mkRingHom_def]

Goal state after:
R : Type uR
inst✝⁴ : Semiring R
S : Type uS
inst✝³ : CommSemiring S
T : Type uT
A : Type uA
inst✝² : Semiring A
inst✝¹ : Algebra S A
r : R → R → Prop
inst✝ : Semiring T
s : A → A → Prop
x✝ : S
⊢ { toQuot := Quot.mk (Rel s) ((algebraMap S A) x✝) } = (algebraMap S (RingQuot s)) x✝
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: R : Type uR
inst✝⁴ : Semiring R
S : Type uS
inst✝³ : CommSemiring S
T : Type uT
A : Type uA
inst✝² : Semiring A
inst✝¹ : Algebra S A
r : R → R → Prop
inst✝ : Semiring T
s : A → A → Prop
x✝ : S
⊢ { toQuot := Quot.mk (Rel s) ((algebraMap S A) x✝) } = (algebraMap S (RingQuot s)) x✝

Tactic:
;

Goal state after:
R : Type uR
inst✝⁴ : Semiring R
S : Type uS
inst✝³ : CommSemiring S
T : Type uT
A : Type uA
inst✝² : Semiring A
inst✝¹ : Algebra S A
r : R → R → Prop
inst✝ : Semiring T
s : A → A → Prop
x✝ : S
⊢ { toQuot := Quot.mk (Rel s) ((algebraMap S A) x✝) } = (algebraMap S (RingQuot s)) x✝
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: R : Type uR
inst✝⁶ : Semiring R
S : Type uS
inst✝⁵ : CommSemiring S
T : Type uT
A : Type uA
inst✝⁴ : Semiring A
inst✝³ : Algebra S A
r : R → R → Prop
inst✝² : Semiring T
B : Type u₄
inst✝¹ : Semiring B
inst✝ : Algebra S B
s : A → A → Prop
f : A →ₐ[S] B
h : ∀ ⦃x y : A⦄, s x y → f x = f y
⊢ ∀ (r : S), Quot.lift ⇑f ⋯ ((algebraMap S (RingQuot s)) r).toQuot = (algebraMap S B) r

Tactic:
by
    rintro x
    simp [← one_quot, smul_quot, Algebra.algebraMap_eq_smul_one]

Goal state after:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: R : Type uR
inst✝⁶ : Semiring R
S : Type uS
inst✝⁵ : CommSemiring S
T : Type uT
A : Type uA
inst✝⁴ : Semiring A
inst✝³ : Algebra S A
r : R → R → Prop
inst✝² : Semiring T
B : Type u₄
inst✝¹ : Semiring B
inst✝ : Algebra S B
f : A ≃ₐ[S] B
rel : A → A → Prop
x y : B
h : (rel on ⇑f.symm) x y
⊢ rel (↑↑f.symm x) (↑↑f.symm y)

Tactic:
;

Goal state after:
R : Type uR
inst✝⁶ : Semiring R
S : Type uS
inst✝⁵ : CommSemiring S
T : Type uT
A : Type uA
inst✝⁴ : Semiring A
inst✝³ : Algebra S A
r : R → R → Prop
inst✝² : Semiring T
B : Type u₄
inst✝¹ : Semiring B
inst✝ : Algebra S B
f : A ≃ₐ[S] B
rel : A → A → Prop
x y : B
h : (rel on ⇑f.symm) x y
⊢ rel (↑↑f.symm x) (↑↑f.symm y)
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: R : Type uR
inst✝⁶ : Semiring R
S : Type uS
inst✝⁵ : CommSemiring S
T : Type uT
A : Type uA
inst✝⁴ : Semiring A
inst✝³ : Algebra S A
r : R → R → Prop
inst✝² : Semiring T
B : Type u₄
inst✝¹ : Semiring B
inst✝ : Algebra S B
f : A ≃ₐ[S] B
rel : A → A → Prop
b : B
⊢ ((((liftAlgHom S) ⟨(mkAlgHom S (rel on ⇑f.symm)).comp ↑f, ⋯⟩).comp
            ((liftAlgHom S) ⟨(mkAlgHom S rel).comp ↑f.symm, ⋯⟩)).comp
        (mkAlgHom S (rel on ⇑f.symm)))
      b =
    ((AlgHom.id S (RingQuot (rel on ⇑f.symm))).comp (mkAlgHom S (rel on ⇑f.symm))) b

Tactic:
;

Goal state after:
R : Type uR
inst✝⁶ : Semiring R
S : Type uS
inst✝⁵ : CommSemiring S
T : Type uT
A : Type uA
inst✝⁴ : Semiring A
inst✝³ : Algebra S A
r : R → R → Prop
inst✝² : Semiring T
B : Type u₄
inst✝¹ : Semiring B
inst✝ : Algebra S B
f : A ≃ₐ[S] B
rel : A → A → Prop
b : B
⊢ ((((liftAlgHom S) ⟨(mkAlgHom S (rel on ⇑f.symm)).comp ↑f, ⋯⟩).comp
            ((liftAlgHom S) ⟨(mkAlgHom S rel).comp ↑f.symm, ⋯⟩)).comp
        (mkAlgHom S (rel on ⇑f.symm)))
      b =
    ((AlgHom.id S (RingQuot (rel on ⇑f.symm))).comp (mkAlgHom S (rel on ⇑f.symm))) b
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: R : Type uR
inst✝⁶ : Semiring R
S : Type uS
inst✝⁵ : CommSemiring S
T : Type uT
A : Type uA
inst✝⁴ : Semiring A
inst✝³ : Algebra S A
r : R → R → Prop
inst✝² : Semiring T
B : Type u₄
inst✝¹ : Semiring B
inst✝ : Algebra S B
f : A ≃ₐ[S] B
rel : A → A → Prop
a : A
⊢ ((((liftAlgHom S) ⟨(mkAlgHom S rel).comp ↑f.symm, ⋯⟩).comp
            ((liftAlgHom S) ⟨(mkAlgHom S (rel on ⇑f.symm)).comp ↑f, ⋯⟩)).comp
        (mkAlgHom S rel))
      a =
    ((AlgHom.id S (RingQuot rel)).comp (mkAlgHom S rel)) a

Tactic:
;

Goal state after:
R : Type uR
inst✝⁶ : Semiring R
S : Type uS
inst✝⁵ : CommSemiring S
T : Type uT
A : Type uA
inst✝⁴ : Semiring A
inst✝³ : Algebra S A
r : R → R → Prop
inst✝² : Semiring T
B : Type u₄
inst✝¹ : Semiring B
inst✝ : Algebra S B
f : A ≃ₐ[S] B
rel : A → A → Prop
a : A
⊢ ((((liftAlgHom S) ⟨(mkAlgHom S rel).comp ↑f.symm, ⋯⟩).comp
            ((liftAlgHom S) ⟨(mkAlgHom S (rel on ⇑f.symm)).comp ↑f, ⋯⟩)).comp
        (mkAlgHom S rel))
      a =
    ((AlgHom.id S (RingQuot rel)).comp (mkAlgHom S rel)) a
Module: Mathlib.Algebra.Star.NonUnitalSubsemiring

Goal state before:
pp: case mk
A : Type v
B : Type w
C : Type w'
R : Type v
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : Star R
q : NonUnitalStarSubsemiring R
toNonUnitalSubsemiring✝ : NonUnitalSubsemiring R
star_mem'✝ : ∀ {a : R}, a ∈ toNonUnitalSubsemiring✝.carrier → star a ∈ toNonUnitalSubsemiring✝.carrier
h : (fun {s} ↦ s.carrier) = fun {s} ↦ s.carrier
⊢ { toNonUnitalSubsemiring := toNonUnitalSubsemiring✝, star_mem' := star_mem'✝ } = q

Tactic:
;

Goal state after:
case mk
A : Type v
B : Type w
C : Type w'
R : Type v
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : Star R
q : NonUnitalStarSubsemiring R
toNonUnitalSubsemiring✝ : NonUnitalSubsemiring R
star_mem'✝ : ∀ {a : R}, a ∈ toNonUnitalSubsemiring✝.carrier → star a ∈ toNonUnitalSubsemiring✝.carrier
h : (fun {s} ↦ s.carrier) = fun {s} ↦ s.carrier
⊢ { toNonUnitalSubsemiring := toNonUnitalSubsemiring✝, star_mem' := star_mem'✝ } = q
Module: Mathlib.Algebra.Star.NonUnitalSubsemiring

Goal state before:
pp: case mk.mk
A : Type v
B : Type w
C : Type w'
R : Type v
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : Star R
toNonUnitalSubsemiring✝¹ : NonUnitalSubsemiring R
star_mem'✝¹ : ∀ {a : R}, a ∈ toNonUnitalSubsemiring✝¹.carrier → star a ∈ toNonUnitalSubsemiring✝¹.carrier
toNonUnitalSubsemiring✝ : NonUnitalSubsemiring R
star_mem'✝ : ∀ {a : R}, a ∈ toNonUnitalSubsemiring✝.carrier → star a ∈ toNonUnitalSubsemiring✝.carrier
h : (fun {s} ↦ s.carrier) = fun {s} ↦ s.carrier
⊢ { toNonUnitalSubsemiring := toNonUnitalSubsemiring✝¹, star_mem' := star_mem'✝¹ } =
    { toNonUnitalSubsemiring := toNonUnitalSubsemiring✝, star_mem' := star_mem'✝ }

Tactic:
;

Goal state after:
case mk.mk
A : Type v
B : Type w
C : Type w'
R : Type v
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : Star R
toNonUnitalSubsemiring✝¹ : NonUnitalSubsemiring R
star_mem'✝¹ : ∀ {a : R}, a ∈ toNonUnitalSubsemiring✝¹.carrier → star a ∈ toNonUnitalSubsemiring✝¹.carrier
toNonUnitalSubsemiring✝ : NonUnitalSubsemiring R
star_mem'✝ : ∀ {a : R}, a ∈ toNonUnitalSubsemiring✝.carrier → star a ∈ toNonUnitalSubsemiring✝.carrier
h : (fun {s} ↦ s.carrier) = fun {s} ↦ s.carrier
⊢ { toNonUnitalSubsemiring := toNonUnitalSubsemiring✝¹, star_mem' := star_mem'✝¹ } =
    { toNonUnitalSubsemiring := toNonUnitalSubsemiring✝, star_mem' := star_mem'✝ }
Module: Mathlib.Algebra.Star.NonUnitalSubsemiring

Goal state before:
pp: case mk.mk
A : Type v
B : Type w
C : Type w'
R : Type v
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : Star R
toNonUnitalSubsemiring✝¹ : NonUnitalSubsemiring R
star_mem'✝¹ : ∀ {a : R}, a ∈ toNonUnitalSubsemiring✝¹.carrier → star a ∈ toNonUnitalSubsemiring✝¹.carrier
toNonUnitalSubsemiring✝ : NonUnitalSubsemiring R
star_mem'✝ : ∀ {a : R}, a ∈ toNonUnitalSubsemiring✝.carrier → star a ∈ toNonUnitalSubsemiring✝.carrier
h : (fun {s} ↦ s.carrier) = fun {s} ↦ s.carrier
⊢ toNonUnitalSubsemiring✝¹ = toNonUnitalSubsemiring✝

Tactic:
;

Goal state after:
case mk.mk
A : Type v
B : Type w
C : Type w'
R : Type v
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : Star R
toNonUnitalSubsemiring✝¹ : NonUnitalSubsemiring R
star_mem'✝¹ : ∀ {a : R}, a ∈ toNonUnitalSubsemiring✝¹.carrier → star a ∈ toNonUnitalSubsemiring✝¹.carrier
toNonUnitalSubsemiring✝ : NonUnitalSubsemiring R
star_mem'✝ : ∀ {a : R}, a ∈ toNonUnitalSubsemiring✝.carrier → star a ∈ toNonUnitalSubsemiring✝.carrier
h : (fun {s} ↦ s.carrier) = fun {s} ↦ s.carrier
⊢ toNonUnitalSubsemiring✝¹ = toNonUnitalSubsemiring✝