mathlib-initiative/mathlib-tactics huggingface dataset:
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✝
k : Type u_6
A : Type u_7
inst✝⁹ : CommSemiring k
inst✝⁸ : Semiring A
inst✝⁷ : Algebra k A
H : Type u_8
F : Type u_9
inst✝⁶ : Monoid H
inst✝⁵ : FunLike F G H
inst✝⁴ : MonoidHomClass F G H
inst✝³ : MulSemiringAction G A
inst✝² : MulSemiringAction H A
inst✝¹ : SMulCommClass G k A
inst✝ : SMulCommClass H k A
f : F
hf : ∀ (a : G) (x : A), a • x = f a • x
⊢ ∀ (r : k),
    (↑↑(mapDomainRingHom hf)).toFun ((algebraMap k (SkewMonoidAlgebra A G)) r) =
      (algebraMap k (SkewMonoidAlgebra A H)) 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✝ : AddCommMonoid k
f : G ≃ H
l : SkewMonoidAlgebra k G
⊢ equivMapDomain f l = (mapDomain ⇑f) l

Tactic:
by

Goal state after:
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
⊢ equivMapDomain (f.trans g) l = equivMapDomain g (equivMapDomain f l)

Tactic:
by

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

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

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✝ : AddCommMonoid k
f : G ≃ H
a : G
b : k
⊢ equivMapDomain f (single a b) = single (f a) b

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
A : Type u_4
inst✝ : AddCommMonoid A
e : G ≃ H
v : SkewMonoidAlgebra A G
⊢ equivMapDomain e.symm (equivMapDomain e v) = v

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
A : Type u_4
inst✝ : AddCommMonoid A
e : G ≃ H
v : SkewMonoidAlgebra A H
⊢ equivMapDomain e (equivMapDomain e.symm v) = v

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
A : Type u_4
inst✝ : AddCommMonoid A
e : G ≃ H
a b : SkewMonoidAlgebra A G
⊢ equivMapDomain e (a + b) = equivMapDomain e a + equivMapDomain e b

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
A : Type u_4
inst✝² : Semiring k
inst✝¹ : AddCommMonoid A
inst✝ : Module k A
e : G ≃ H
⊢ ∀ (c : k) (x : SkewMonoidAlgebra A G), (domCongr e) (c • x) = c • (domCongr e) x

Tactic:
by

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

Goal state before:
pp: k : Type u_1
G : Type u_2
A : Type u_4
inst✝⁵ : Monoid G
inst✝⁴ : Semiring A
inst✝³ : CommSemiring k
inst✝² : Algebra k A
inst✝¹ : MulSemiringAction G A
inst✝ : SMulCommClass G k A
⊢ domCongrAlg k A ⋯ = AlgEquiv.refl

Tactic:
by

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

Goal state before:
pp: k : Type u_1
G : Type u_2
H : Type u_3
M : Type u_4
α : Type u_5
inst✝ : AddCommMonoid M
a a' : α
b : M
f : SkewMonoidAlgebra M α
⊢ { coeff := Finsupp.erase a (coeff 0) } = 0

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
A : Type u_4
inst✝⁸ : Monoid G
inst✝⁷ : Monoid H
inst✝⁶ : Semiring A
inst✝⁵ : CommSemiring k
inst✝⁴ : Algebra k A
inst✝³ : MulSemiringAction G A
inst✝² : MulSemiringAction H A
inst✝¹ : SMulCommClass G k A
inst✝ : SMulCommClass H k A
e : G ≃* H
he : ∀ (a : G) (x : A), a • x = e a • x
a : H
x : A
⊢ a • x = e.symm a • x

Tactic:
by

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

Goal state before:
pp: k : Type u_1
G : Type u_2
H : Type u_3
M : Type u_4
α : Type u_5
inst✝ : AddCommMonoid M
a a' : α
b : M
f : SkewMonoidAlgebra M α
⊢ ∀ (x y : SkewMonoidAlgebra M α),
    { coeff := Finsupp.erase a (x + y).coeff } =
      { coeff := Finsupp.erase a x.coeff } + { coeff := Finsupp.erase a y.coeff }

Tactic:
by

Goal state after:
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 α
⊢ ((erase a) f).support = f.support.erase a

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: M : Type u_4
α : Type u_5
inst✝ : AddCommMonoid M
a : α
b : M
⊢ (erase a) (single a b) = 0

Tactic:
by

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

Goal state before:
pp: M : Type u_4
α : Type u_5
inst✝ : AddCommMonoid M
a : α
f : SkewMonoidAlgebra M α
⊢ single a (f.coeff a) + (erase a) 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✝⁶ : Semiring k
inst✝⁵ : Monoid G
inst✝⁴ : MulSemiringAction G k
V : Type u_4
inst✝³ : AddCommMonoid V
inst✝² : Module k V
inst✝¹ : Module (SkewMonoidAlgebra k G) V
inst✝ : IsScalarTower k (SkewMonoidAlgebra k G) V
W : Submodule k V
h : ∀ (g : G), ∀ v ∈ W, (of k G) g • v ∈ W
⊢ ∀ (c : SkewMonoidAlgebra k G) {x : V}, x ∈ ↑W → c • x ∈ ↑W

Tactic:
by

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
a b c d : R
hab : Relation.EqvGen (Rel r) a b
hcd : Relation.EqvGen (Rel r) c d
⊢ Relation.EqvGen (Rel r) (a * c) (b * d)

Tactic:
by

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

Goal state before:
pp: M : Type u_4
α : Type u_5
inst✝ : AddCommMonoid M
p : SkewMonoidAlgebra M α → Prop
f✝ : SkewMonoidAlgebra M α
h0 : p 0
ha : ∀ (a : α) (b : M) (f : SkewMonoidAlgebra M α), a ∉ f.support → b ≠ 0 → p f → p (single a b + f)
s : Finset α
f : SkewMonoidAlgebra M α
hf : f.support = ∅
⊢ p f

Tactic:
by

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

Goal state before:
pp: M : Type u_4
α : Type u_5
inst✝ : AddCommMonoid M
p : SkewMonoidAlgebra M α → Prop
f✝ : SkewMonoidAlgebra M α
h0 : p 0
ha : ∀ (a : α) (b : M) (f : SkewMonoidAlgebra M α), a ∉ f.support → b ≠ 0 → p f → p (single a b + f)
s✝ : Finset α
a : α
s : Finset α
has : a ∉ s
ih : ∀ (f : SkewMonoidAlgebra M α), f.support = s → p f
f : SkewMonoidAlgebra M α
hf : f.support = Finset.cons a s has
this : p (single a (f.coeff a) + (erase a) f)
⊢ p f

Tactic:
by

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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : AddCommMonoid k
k' : Type u_3
G' : Type u_4
inst✝¹ : DecidableEq G'
inst✝ : AddCommMonoid k'
f : SkewMonoidAlgebra k G
g : G → k → SkewMonoidAlgebra k' G'
⊢ (f.sum g).support ⊆ f.support.biUnion fun a ↦ (g a (f.coeff a)).support

Tactic:
by

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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝ : AddCommGroup k
p : SkewMonoidAlgebra k G
⊢ (-p).support = p.support

Tactic:
by

Goal state after:
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✝ : DecidableEq G
r : k
a : G
⊢ image₂ (fun x1 x2 ↦ x1 * x2) {a} f.support ⊆ image (fun x ↦ a * x) f.support

Tactic:
by

Goal state after:
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✝ : DecidableEq G
r : k
a : G
⊢ image₂ (fun x1 x2 ↦ x1 * x2) f.support {a} ⊆ image (fun x ↦ x * a) f.support

Tactic:
by

Goal state after:
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✝ : DecidableEq G
r : k
x : G
lx : IsLeftRegular x
hrx : ∀ (y : k), r * x • y = 0 ↔ y = 0
y : G
hy : y ∈ image (fun x_1 ↦ x * x_1) f.support
⊢ ∃ a ∈ f.support, x * a = y

Tactic:
by

Goal state after:
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✝ : DecidableEq G
r : k
x : G
lx : IsLeftRegular x
hrx : ∀ (y : k), r * x • y = 0 ↔ y = 0
⊢ (single x r * f).support = image (fun x_1 ↦ x * x_1) f.support

Tactic:
by

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
a b c d : R
hab : Relation.EqvGen (Rel r) a b
hcd : Relation.EqvGen (Rel r) c d
⊢ Relation.EqvGen (Rel r) (a + c) (b + d)

Tactic:
by

Goal state after:
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✝ : DecidableEq G
r : k
x : G
rx : IsRightRegular x
hrx : ∀ (g : G) (y : k), y * g • r = 0 ↔ y = 0
y : G
hy : y ∈ image (fun x_1 ↦ x_1 * x) f.support
⊢ ∃ a ∈ f.support, a * x = y

Tactic:
by

Goal state after:
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✝ : DecidableEq G
r : k
x : G
rx : IsRightRegular x
hrx : ∀ (g : G) (y : k), y * g • r = 0 ↔ y = 0
⊢ (f * single x r).support = image (fun x_1 ↦ x_1 * x) f.support

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: case mpr.trans
R : Type uR
inst✝ : Semiring R
r : R → R → Prop
x₁ x₂ x✝ y✝ z✝ : R
a✝¹ : RingConGen.Rel r x✝ y✝
a✝ : RingConGen.Rel r y✝ z✝
a_ih✝¹ : Relation.EqvGen (Rel r) x✝ y✝
a_ih✝ : Relation.EqvGen (Rel r) y✝ z✝
⊢ Relation.EqvGen (Rel r) x✝ z✝

Tactic:
exact (RingQuot.ringCon r).trans ‹_› ‹_›

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

Goal state after:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: R : Type uR
inst✝ : Semiring R
r : R → R → Prop
⊢ Relation.EqvGen (Rel r) = RingConGen.Rel r

Tactic:
by

Goal state after:
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✝ : IsLeftCancelMul G
r : k
x : G
hrx : ∀ (y : k), r * x • y = 0 ↔ y = 0
⊢ (single x r * f).support = map (mulLeftEmbedding x) f.support

Tactic:
by

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
x✝ : RingQuot r
n : ℕ
a✝ : Quot (Rel r)
a b : R
h : Rel r a b
⊢ Quot.mk (Rel r) (a ^ n) = Quot.mk (Rel r) (b ^ n)

Tactic:
by

Goal state after:
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
⊢ f ∈ Submodule.span k (⇑(of k G) '' ↑f.support)

Tactic:
by

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✝⁴ : CommSemiring T
inst✝³ : SMul S T
inst✝² : Algebra S R
inst✝¹ : Algebra T R
inst✝ : IsScalarTower S T R
s : S
t : T
x✝ : RingQuot r
a : Quot (Rel r)
a' : R
⊢ (s • t) • { toQuot := Quot.mk (Rel r) a' } = s • t • { toQuot := Quot.mk (Rel r) a' }

Tactic:
by

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

Goal state before:
pp: M : Type u_4
α : Type u_5
inst✝ : AddCommMonoid M
p : SkewMonoidAlgebra M α → Prop
f✝ : SkewMonoidAlgebra M α
h0 : p 0
ha : ∀ (a : α) (b : M) (f : SkewMonoidAlgebra M α), a ∉ f.support → b ≠ 0 → p f → p (single a b + f)
s✝ : Finset α
a : α
s : Finset α
has : a ∉ s
ih : ∀ (f : SkewMonoidAlgebra M α), f.support = s → p f
f : SkewMonoidAlgebra M α
hf : f.support = Finset.cons a s has
⊢ p f

Tactic:
by

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✝³ : CommSemiring T
inst✝² : Algebra S R
inst✝¹ : Algebra T R
inst✝ : SMulCommClass S T R
s : S
t : T
x✝ : RingQuot r
a : Quot (Rel r)
a' : R
⊢ s • t • { toQuot := Quot.mk (Rel r) a' } = t • s • { toQuot := Quot.mk (Rel r) a' }

Tactic:
by

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 : α
⊢ f.update a (f.coeff a) = f

Tactic:
by

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

Goal state before:
pp: M : Type u_4
α : Type u_5
inst✝ : AddCommMonoid M
a : α
b : M
⊢ update 0 a b = single a b

Tactic:
by

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 : α
b : M
inst✝¹ : DecidableEq α
inst✝ : DecidableEq M
⊢ (f.update a b).support = if b = 0 then f.support.erase a else insert a f.support

Tactic:
by

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' : α
b : M
inst✝ : DecidableEq α
⊢ (f.update a b).coeff a' = if a' = a then b else f.coeff a'

Tactic:
by

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 → R → Prop
⊢ ∀ (a b c : RingQuot r), a + b + c = a + (b + c)

Tactic:
by

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 : α
b : M
⊢ (f.update a b).coeff a = b

Tactic:
by

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' : α
b : M
h : a' ≠ a
⊢ (f.update a b).coeff a' = f.coeff a'

Tactic:
by

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 → R → Prop
⊢ ∀ (a : RingQuot r), 0 + a = a

Tactic:
by

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 → R → Prop
⊢ ∀ (a : RingQuot r), a + 0 = a

Tactic:
by

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 : α
b : M
⊢ f.update a b = (erase a) f + single a b

Tactic:
by

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 → R → Prop
⊢ ∀ (x : RingQuot r), 0 • x = 0

Tactic:
by

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 : α
⊢ f.update a 0 = (erase a) f

Tactic:
by

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 → R → Prop
⊢ ∀ (n : ℕ) (x : RingQuot r), (n + 1) • x = n • x + x

Tactic:
by

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 → R → Prop
⊢ ∀ (a b : RingQuot r), a + b = b + a

Tactic:
by

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 → R → Prop
⊢ ∀ (a b c : RingQuot r), a * b * c = a * (b * c)

Tactic:
by

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 → R → Prop
⊢ ∀ (a : RingQuot r), 1 * a = a

Tactic:
rintro ⟨⟨⟩⟩
    simp only [mul_quot, ← one_quot, one_mul]

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 → R → Prop
⊢ ∀ (a : RingQuot r), 1 * a = a

Tactic:
by

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 → R → Prop
⊢ ∀ (a : RingQuot r), a * 1 = a

Tactic:
by

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 → R → Prop
⊢ ∀ (x : RingQuot r), x ^ 0 = 1

Tactic:
by

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 → R → Prop
⊢ ∀ (n : ℕ) (x : RingQuot r), x ^ (n + 1) = x ^ n * x

Tactic:
by

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 → R → Prop
⊢ ∀ (a : RingQuot r), 0 * a = 0

Tactic:
by

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 → R → Prop
⊢ ∀ (a : RingQuot r), a * 0 = 0

Tactic:
by

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 → R → Prop
⊢ ∀ (a b c : RingQuot r), a * (b + c) = a * b + a * c

Tactic:
by

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 → R → Prop
⊢ ∀ (a b c : RingQuot r), (a + b) * c = a * c + b * c

Tactic:
by

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 → R → Prop
⊢ ↑0 = 0

Tactic:
by

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 → R → Prop
⊢ ∀ (n : ℕ), ↑(n + 1) = ↑n + 1

Tactic:
by

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
R : Type uR
inst✝ : Ring R
r : R → R → Prop
⊢ ∀ (a b : RingQuot r), a - b = a + -b

Tactic:
by

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
R : Type uR
inst✝ : Ring R
r : R → R → Prop
⊢ ∀ (a : RingQuot r), 0 • a = 0

Tactic:
by

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
R : Type uR
inst✝ : Ring R
r : R → R → Prop
⊢ ∀ (n : ℕ) (a : RingQuot r), ↑n.succ • a = ↑n • a + a

Tactic:
by

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
R : Type uR
inst✝ : Ring R
r : R → R → Prop
⊢ ∀ (n : ℕ) (a : RingQuot r), Int.negSucc n • a = -(↑n.succ • a)

Tactic:
by

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
R : Type uR
inst✝ : Ring R
r : R → R → Prop
⊢ ∀ (a : RingQuot r), -a + a = 0

Tactic:
by

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
R : Type uR
inst✝ : Ring R
r : R → R → Prop
n : ℕ
⊢ Quot.mk (Rel r) ↑↑n = Quot.mk (Rel r) ↑n

Tactic:
by

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
R : Type uR
inst✝ : Ring R
r : R → R → Prop
n : ℕ
⊢ Quot.mk (Rel r) ↑(Int.negSucc n) = ((instNeg r).1 ↑(n + 1)).toQuot

Tactic:
by

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
R : Type uR
inst✝ : CommSemiring R
r : R → R → Prop
⊢ ∀ (a b : RingQuot r), a * b = b * a

Tactic:
by

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✝ : Algebra S R
r : R → R → Prop
⊢ { toQuot := Quot.mk (Rel r) ((algebraMap S R) 1) } = 1

Tactic:
by

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✝ : Algebra S R
r : R → R → Prop
⊢ ∀ (x y : S),
    { toQuot := Quot.mk (Rel r) ((algebraMap S R) (x * y)) } =
      { toQuot := Quot.mk (Rel r) ((algebraMap S R) x) } * { toQuot := Quot.mk (Rel r) ((algebraMap S R) y) }

Tactic:
by

Goal state after: