mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Derivation.MapCoeffs

Goal state before:
pp: case add
R : Type u_1
A : Type u_2
M : Type u_3
inst✝¹² : CommRing R
inst✝¹¹ : CommRing A
inst✝¹⁰ : Algebra R A
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module A M
inst✝⁷ : Module R M
d : Derivation R A M
B : Type u_4
M' : Type u_5
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R B
inst✝⁴ : Algebra A B
inst✝³ : AddCommGroup M'
inst✝² : Module B M'
inst✝¹ : Module R M'
inst✝ : Module A M'
d' : Derivation R B M'
f : M →ₗ[A] M'
h : ∀ (a : A), f (d a) = d' ((algebraMap A B) a)
x : B
p✝ q✝ : A[X]
a✝¹ :
  d' ((aeval x) p✝) =
    (PolynomialModule.eval x) ((PolynomialModule.map B f) (d.mapCoeffs p✝)) + (aeval x) (derivative p✝) • d' x
a✝ :
  d' ((aeval x) q✝) =
    (PolynomialModule.eval x) ((PolynomialModule.map B f) (d.mapCoeffs q✝)) + (aeval x) (derivative q✝) • d' x
⊢ d' ((aeval x) (p✝ + q✝)) =
    (PolynomialModule.eval x) ((PolynomialModule.map B f) (d.mapCoeffs (p✝ + q✝))) +
      (aeval x) (derivative (p✝ + q✝)) • d' x

Tactic:
| add =>

Goal state after:
Module: Mathlib.Algebra.Polynomial.Bivariate

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
⊢ R[X][Y] ≃ₐ[R] R[X][Y]

Tactic:
apply AlgEquiv.ofAlgHom (aevalAeval (Y : R[X][Y]) (C X)) (aevalAeval (Y : R[X][Y]) (C X))
    <;> (ext n m <;> simp)

Goal state after:
Module: Mathlib.Algebra.Polynomial.Bivariate

Goal state before:
pp: case add
R : Type u_1
inst✝ : CommSemiring R
p✝ q✝ : R[X]
a✝¹ : swap (map C p✝) = C p✝
a✝ : swap (map C q✝) = C q✝
⊢ swap (map C (p✝ + q✝)) = C (p✝ + q✝)

Tactic:
| add =>

Goal state after:
Module: Mathlib.Algebra.Polynomial.Bivariate

Goal state before:
pp: case add
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
x y : A
p✝ q✝ : R[X][Y]
a✝¹ : (aevalAeval x y) (swap p✝) = (aevalAeval y x) p✝
a✝ : (aevalAeval x y) (swap q✝) = (aevalAeval y x) q✝
⊢ (aevalAeval x y) (swap (p✝ + q✝)) = (aevalAeval y x) (p✝ + q✝)

Tactic:
| add =>

Goal state after:
Module: Mathlib.Algebra.Polynomial.Bivariate

Goal state before:
pp: case add
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
x : A
p✝ q✝ : R[X][Y]
a✝¹ : (aeval (C x)) p✝ = (mapAlgHom (aeval x)) (swap p✝)
a✝ : (aeval (C x)) q✝ = (mapAlgHom (aeval x)) (swap q✝)
⊢ (aeval (C x)) (p✝ + q✝) = (mapAlgHom (aeval x)) (swap (p✝ + q✝))

Tactic:
| add =>

Goal state after:
Module: Mathlib.Algebra.Order.Module.HahnEmbedding

Goal state before:
pp: K : Type u_1
inst✝¹¹ : DivisionRing K
inst✝¹⁰ : LinearOrder K
inst✝⁹ : IsOrderedRing K
inst✝⁸ : Archimedean K
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : LinearOrder M
inst✝⁵ : IsOrderedAddMonoid M
inst✝⁴ : Module K M
inst✝³ : IsOrderedModule K M
R : Type u_3
inst✝² : AddCommGroup R
inst✝¹ : LinearOrder R
inst✝ : Module K R
seed : Seed K M R
c✝ : Set (Partial seed)
hnonempty : c✝.Nonempty
hc : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) c✝
x : ↥(sSupFun hc).domain
c : FiniteArchimedeanClass M
hx : ↑x ∈ sSup (LinearPMap.domain '' (fun x ↦ ↑x) '' c✝)
f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧
hmem : f ∈ (fun x ↦ ↑x) '' c✝
hf : ↑x ∈ f.domain
f' : Partial seed
hmem' : f' ∈ c✝
hf' : ↑f' = f
h : toLex ((truncLTLinearMap K c) (ofLex (↑f ⟨↑x, hf⟩))) ∈ f.toFun.range
⊢ toLex ((truncLTLinearMap K c) (ofLex (↑(sSupFun hc) x))) ∈ (sSupFun hc).toFun.range

Tactic:
simp_rw [LinearMap.mem_range, LinearPMap.toFun_eq_coe] at ⊢ h

Goal state after:
K : Type u_1
inst✝¹¹ : DivisionRing K
inst✝¹⁰ : LinearOrder K
inst✝⁹ : IsOrderedRing K
inst✝⁸ : Archimedean K
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : LinearOrder M
inst✝⁵ : IsOrderedAddMonoid M
inst✝⁴ : Module K M
inst✝³ : IsOrderedModule K M
R : Type u_3
inst✝² : AddCommGroup R
inst✝¹ : LinearOrder R
inst✝ : Module K R
seed : Seed K M R
c✝ : Set (Partial seed)
hnonempty : c✝.Nonempty
hc : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) c✝
x : ↥(sSupFun hc).domain
c : FiniteArchimedeanClass M
hx : ↑x ∈ sSup (LinearPMap.domain '' (fun x ↦ ↑x) '' c✝)
f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧
hmem : f ∈ (fun x ↦ ↑x) '' c✝
hf : ↑x ∈ f.domain
f' : Partial seed
hmem' : f' ∈ c✝
hf' : ↑f' = f
h : ∃ y, ↑f y = toLex ((truncLTLinearMap K c) (ofLex (↑f ⟨↑x, hf⟩)))
⊢ ∃ y, ↑(sSupFun hc) y = toLex ((truncLTLinearMap K c) (ofLex (↑(sSupFun hc) x)))
Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p q : R[X]
n : ℕ
hp : p.IsMonicOfDegree n
hq : q.natDegree < n
⊢ (p + q).IsMonicOfDegree n

Tactic:
rcases subsingleton_or_nontrivial R with H | H
  · simpa using hp
  refine (isMonicOfDegree_iff ..).mpr ⟨?_, ?_⟩
  · exact natDegree_add_le_of_degree_le hp.natDegree_eq.le hq.le
  · rw [coeff_add_eq_left_of_lt hq]
    exact ((isMonicOfDegree_iff p n).mp hp).2

Goal state after:
Module: Mathlib.Algebra.Polynomial.DenomsClearable

Goal state before:
pp: R : Type u_1
K : Type u_2
inst✝¹ : Semiring R
inst✝ : CommSemiring K
i : R →+* K
b : R
bi : K
N : ℕ
a : R
bu : bi * i b = 1
n : ℕ
r : R
nN : n ≤ N
⊢ i (r * a ^ n * b ^ (N - n)) = i b ^ N * (eval (i a * bi) (C (i r)) * eval (i a * bi) (X ^ n))

Tactic:
eval_pow,

Goal state after:
R : Type u_1
K : Type u_2
inst✝¹ : Semiring R
inst✝ : CommSemiring K
i : R →+* K
b : R
bi : K
N : ℕ
a : R
bu : bi * i b = 1
n : ℕ
r : R
nN : n ≤ N
⊢ i (r * a ^ n * b ^ (N - n)) = i b ^ N * (eval (i a * bi) (C (i r)) * eval (i a * bi) X ^ n)
Module: Mathlib.Algebra.Polynomial.Mirror

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
n : ℕ
a : R
ha : ¬a = 0
⊢ reflect (if a = 0 then 0 else n) ((monomial n) a) * X ^ ((monomial n) a).natTrailingDegree = (monomial n) a

Tactic:
if_neg ha,

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
n : ℕ
a : R
ha : ¬a = 0
⊢ reflect n ((monomial n) a) * X ^ ((monomial n) a).natTrailingDegree = (monomial n) a
Module: Mathlib.Data.List.Destutter

Goal state before:
pp: α : Type u_1
l : List α
R : α → α → Prop
inst✝ : DecidableRel R
a : α
h : destutter' R a l = a :: l
⊢ IsChain R (destutter' R a l)

Tactic:
exact l.isChain_destutter' R a

Goal state after:
Module: Mathlib.Algebra.Polynomial.PartialFractions

Goal state before:
pp: case succ.snoc.snoc
R : Type u_1
inst✝ : CommRing R
g : R[X]
hg : g.Monic
n : ℕ
ih :
  ∀ {q₁ q₂ : R[X]} {r₁ r₂ : Fin n → R[X]},
    (∀ (i : Fin n), (r₁ i).degree < g.degree) →
      (∀ (i : Fin n), (r₂ i).degree < g.degree) →
        q₁ * g ^ n + ∑ i, r₁ i * g ^ ↑i = q₂ * g ^ n + ∑ i, r₂ i * g ^ ↑i → q₁ = q₂ ∧ r₁ = r₂
q₁ q₂ : R[X]
rs₁ : Fin n → R[X]
r₁ : R[X]
hr₁ : ∀ (i : Fin (n + 1)), (Fin.snoc rs₁ r₁ i).degree < g.degree
rs₂ : Fin n → R[X]
r₂ : R[X]
hr₂ : ∀ (i : Fin (n + 1)), (Fin.snoc rs₂ r₂ i).degree < g.degree
hf : q₁ * g ^ (n + 1) + ∑ i, Fin.snoc rs₁ r₁ i * g ^ ↑i = q₂ * g ^ (n + 1) + ∑ i, Fin.snoc rs₂ r₂ i * g ^ ↑i
⊢ q₁ = q₂ ∧ Fin.snoc rs₁ r₁ = Fin.snoc rs₂ r₂

Tactic:
simp only [Fin.sum_univ_castSucc, Fin.snoc_castSucc,
      Fin.val_castSucc, Fin.snoc_last, Fin.val_last] at hf

Goal state after:
case succ.snoc.snoc
R : Type u_1
inst✝ : CommRing R
g : R[X]
hg : g.Monic
n : ℕ
ih :
  ∀ {q₁ q₂ : R[X]} {r₁ r₂ : Fin n → R[X]},
    (∀ (i : Fin n), (r₁ i).degree < g.degree) →
      (∀ (i : Fin n), (r₂ i).degree < g.degree) →
        q₁ * g ^ n + ∑ i, r₁ i * g ^ ↑i = q₂ * g ^ n + ∑ i, r₂ i * g ^ ↑i → q₁ = q₂ ∧ r₁ = r₂
q₁ q₂ : R[X]
rs₁ : Fin n → R[X]
r₁ : R[X]
hr₁ : ∀ (i : Fin (n + 1)), (Fin.snoc rs₁ r₁ i).degree < g.degree
rs₂ : Fin n → R[X]
r₂ : R[X]
hr₂ : ∀ (i : Fin (n + 1)), (Fin.snoc rs₂ r₂ i).degree < g.degree
hf : q₁ * g ^ (n + 1) + (∑ x, rs₁ x * g ^ ↑x + r₁ * g ^ n) = q₂ * g ^ (n + 1) + (∑ x, rs₂ x * g ^ ↑x + r₂ * g ^ n)
⊢ q₁ = q₂ ∧ Fin.snoc rs₁ r₁ = Fin.snoc rs₂ r₂
Module: Mathlib.Algebra.Polynomial.Smeval

Goal state before:
pp: R : Type u_3
inst✝³ : Semiring R
S : Type u_4
inst✝² : Semiring S
inst✝¹ : Module R S
inst✝ : IsScalarTower R S S
p : R[X]
x : S
⊢ eval₂ RingHom.smulOneHom x p = p.smeval x

Tactic:
rw [smeval_eq_sum, eval₂_eq_sum]

Goal state after:
R : Type u_3
inst✝³ : Semiring R
S : Type u_4
inst✝² : Semiring S
inst✝¹ : Module R S
inst✝ : IsScalarTower R S S
p : R[X]
x : S
⊢ (p.sum fun e a ↦ RingHom.smulOneHom a * x ^ e) = p.sum (smul_pow x)
Module: Mathlib.Algebra.Polynomial.Smeval

Goal state before:
pp: R : Type u_3
inst✝ : Semiring R
r : R
x✝ : R[X]
⊢ (leval r) x✝ = x✝.smeval r

Tactic:
simpa using eval_eq_smeval _ _

Goal state after:
Module: Mathlib.Algebra.Polynomial.SpecificDegree

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
hp : Monic 1
hp2 : 2 ≤ natDegree 1
hp3 : natDegree 1 ≤ 3
hp0 : 1 ≠ 0
⊢ False

Tactic:
natDegree_one

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
hp : Monic 1
hp2 : 2 ≤ 0
hp3 : natDegree 1 ≤ 3
hp0 : 1 ≠ 0
⊢ False
Module: Mathlib.Algebra.Polynomial.SpecificDegree

Goal state before:
pp: case pos
K : Type u_1
inst✝ : Field K
p : K[X]
hdeg : 1 ≤ p.natDegree ∧ p.natDegree ≤ 3
hnot : ∀ (x : K), ¬p.IsRoot x
hdeg2 : 2 ≤ p.natDegree
⊢ ∀ (x : K), x ∉ p.roots

Tactic:
simp_all

Goal state after:
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
hu : u ≠ 0
⊢ (trinomial k m n u v w).natTrailingDegree = k

Tactic:
refine
    natTrailingDegree_eq_of_trailingDegree_eq_some
      ((Finset.le_inf fun i h => ?_).antisymm <|
          trailingDegree_le_of_ne_zero <| by rwa [trinomial_trailing_coeff' hkm hmn]).symm
  replace h := support_trinomial_subset k m n u v w h
  rw [mem_insert, mem_insert, mem_singleton] at h
  rcases h with (rfl | rfl | rfl)
  · exact le_rfl
  · exact WithTop.coe_le_coe.mpr hkm.le
  · exact WithTop.coe_le_coe.mpr (hkm.trans hmn).le

Goal state after:
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
hw : w ≠ 0
⊢ (trinomial k m n u v w).leadingCoeff = w

Tactic:
by
  rw [leadingCoeff, trinomial_natDegree hkm hmn hw, trinomial_leading_coeff' hkm hmn]

Goal state after:
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: case refine_1
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
⊢ ((trinomial k m n ↑u ↑v ↑w).sum fun x x_1 ↦ x_1 ^ 2) = 3

Tactic:
sum_def,

Goal state after:
case refine_1
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
⊢ ∑ n_1 ∈ (trinomial k m n ↑u ↑v ↑w).support, (trinomial k m n ↑u ↑v ↑w).coeff n_1 ^ 2 = 3
Module: Mathlib.Algebra.Polynomial.RuleOfSigns

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : Semiring R
inst✝ : LinearOrder R
P : R[X]
h : SignType.sign P.leadingCoeff = SignType.sign P.nextCoeff
hpz : P = 0
⊢ P.eraseLead.signVariations = P.signVariations

Tactic:
simp_all

Goal state after:
Module: Mathlib.Algebra.Polynomial.RuleOfSigns

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : LinearOrder R
P : R[X]
h : SignType.sign P.leadingCoeff = SignType.sign P.nextCoeff
hpz : ¬P = 0
a✝ : P.nextCoeff = 0
⊢ False

Tactic:
simp_all

Goal state after:
Module: Mathlib.Algebra.Polynomial.RuleOfSigns

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : Semiring R
inst✝ : LinearOrder R
P : R[X]
h : P ≠ 0
hpz : P = 0
⊢ P.signVariations =
    P.eraseLead.signVariations + if SignType.sign P.leadingCoeff = -SignType.sign P.eraseLead.leadingCoeff then 1 else 0

Tactic:
simp_all

Goal state after:
Module: Mathlib.Algebra.Polynomial.RuleOfSigns

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : LinearOrder R
P : R[X]
h : P ≠ 0
hpz : ¬P = 0
⊢ SignType.sign P.leadingCoeff ≠ 0

Tactic:
simp_all

Goal state after:
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: case refine_2
p : ℤ[X]
hp : (p.sum fun x x_1 ↦ x_1 ^ 2) = 3
key : ∀ k ∈ p.support, p.coeff k ^ 2 = 1
⊢ #p.support = 3

Tactic:
sum_def,

Goal state after:
case refine_2
p : ℤ[X]
hp : ∑ n ∈ p.support, p.coeff n ^ 2 = 3
key : ∀ k ∈ p.support, p.coeff k ^ 2 = 1
⊢ #p.support = 3
Module: Mathlib.Algebra.Polynomial.PartialFractions

Goal state before:
pp: case cons
R : Type u_1
inst✝¹ : CommRing R
ι : Type u_2
inst✝ : DecidableEq ι
g : ι → R[X]
i j : ι
s : Finset ι
hj : j ∉ s
ih : ∀ (hi : i ∉ s), ((↑(Finset.cons i s hi)).Pairwise fun i j ↦ IsCoprime (g i) (g j)) → IsCoprime (g i) (∏ i ∈ s, g i)
hi : i ∉ Finset.cons j s hj
hgg : (↑(Finset.cons i (Finset.cons j s hj) hi)).Pairwise fun i j ↦ IsCoprime (g i) (g j)
⊢ IsCoprime (g i) (∏ i ∈ Finset.cons j s hj, g i)

Tactic:
rw [Finset.prod_cons, IsCoprime.mul_right_iff]
        refine ⟨hgg (by simp) (by simp) fun hij => hi (by simp [hij]), ih ?_ ?_⟩
        · exact mt Finset.mem_cons_of_mem hi
        · exact hgg.mono (SetLike.coe_mono (Finset.cons_subset_cons.2 (Finset.subset_cons hj)))

Goal state after:
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: case inr
p q : ℤ[X]
k m m' n : ℕ
hkm : k < m
hmn : m < n
hkm' : k < m'
hmn' : m' < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
h : p * p.mirror = q.mirror.mirror.mirror * q.mirror.mirror
hq : q.mirror = trinomial k (n - m' + k) n ↑u ↑v ↑w
hmul : ↑w * ↑u = ↑u * ↑w
⊢ q = p ∨ q = p.mirror

Tactic:
q.mirror.mirror_mirror

Goal state after:
case inr
p q : ℤ[X]
k m m' n : ℕ
hkm : k < m
hmn : m < n
hkm' : k < m'
hmn' : m' < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
h : p * p.mirror = q.mirror * q.mirror.mirror
hq : q.mirror = trinomial k (n - m' + k) n ↑u ↑v ↑w
hmul : ↑w * ↑u = ↑u * ↑w
⊢ q = p ∨ q = p.mirror
Module: Mathlib.Algebra.QuadraticAlgebra.Defs

Goal state before:
pp: R : Type u_1
a b : R
inst✝¹ : Zero R
inst✝ : One R
r : R
⊢ QuadraticAlgebra.C r = 1 ↔ r = 1

Tactic:
by
  rw [← C_one, C_inj]

Goal state after:
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: R : Type u_1
inst✝¹ : Rack R
G : Type u_2
inst✝ : Group G
f : R →◃ Quandle.Conj G
⊢ ⟦unit⟧.liftOn (mapAux f) ⋯ = 1

Tactic:
simp only [Quotient.lift_mk, mapAux]

Goal state after:
Module: Mathlib.Algebra.QuaternionBasis

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
x y : ℍ[R,c₁,c₂,c₃]
⊢ q.lift (x + y) = q.lift x + q.lift y

Tactic:
simp only [lift, re_add, map_add, imI_add, add_smul, imJ_add, imK_add]

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
x y : ℍ[R,c₁,c₂,c₃]
⊢ (algebraMap R A) x.re + (algebraMap R A) y.re + (x.imI • q.i + y.imI • q.i) + (x.imJ • q.j + y.imJ • q.j) +
      (x.imK • q.k + y.imK • q.k) =
    (algebraMap R A) x.re + x.imI • q.i + x.imJ • q.j + x.imK • q.k +
      ((algebraMap R A) y.re + y.imI • q.i + y.imJ • q.j + y.imK • q.k)
Module: Mathlib.Algebra.Ring.IsFormallyReal

Goal state before:
pp: case sq_add.inl
R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
s✝ s : R
hs✝ : IsSumSq s
ih : s ≠ 0 → IsSumNonzeroSq s
hs : 0 * 0 + s ≠ 0
⊢ IsSumNonzeroSq (0 * 0 + s)

Tactic:
simp_all

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:
simp_all

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:
rw [add_comm a b, add_comm a c]
  exact Rel.add_left h

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
f : SkewMonoidAlgebra k G
v : V
hv : v ∈ ↑W
⊢ f.sum single • v ∈ ↑W

Tactic:
sum_def,

Goal state after:
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
f : SkewMonoidAlgebra k G
v : V
hv : v ∈ ↑W
⊢ f.coeff.sum single • v ∈ ↑W
Module: Mathlib.Algebra.RingQuot

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

Tactic:
| trans =>

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:
| trans =>

Goal state after:
Module: Mathlib.Algebra.RingQuot

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

Tactic:
| add =>

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:
rintro ⟨⟨⟩⟩ ⟨⟨⟩⟩

Goal state after:
case mk.mk
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
toQuot✝¹ : Quot (Rel r)
a✝¹ : R
toQuot✝ : Quot (Rel r)
a✝ : R
⊢ { toQuot := Quot.mk (Rel r) a✝¹ } + { toQuot := Quot.mk (Rel r) a✝ } =
    { toQuot := Quot.mk (Rel r) a✝ } + { toQuot := Quot.mk (Rel r) 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
R : Type uR
inst✝ : Ring R
r : R → R → Prop
⊢ ∀ (a b : RingQuot r), a - b = a + -b

Tactic:
rintro ⟨⟨⟩⟩ ⟨⟨⟩⟩

Goal state after:
case mk.mk
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
toQuot✝¹ : Quot (Rel r)
a✝¹ : R
toQuot✝ : Quot (Rel r)
a✝ : R
⊢ { toQuot := Quot.mk (Rel r) a✝¹ } - { toQuot := Quot.mk (Rel r) a✝ } =
    { toQuot := Quot.mk (Rel r) a✝¹ } + -{ toQuot := Quot.mk (Rel r) 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
R : Type uR
inst✝ : CommSemiring R
r : R → R → Prop
⊢ ∀ (a b : RingQuot r), a * b = b * a

Tactic:
rintro ⟨⟨⟩⟩ ⟨⟨⟩⟩

Goal state after:
case mk.mk
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
toQuot✝¹ : Quot (Rel r)
a✝¹ : R
toQuot✝ : Quot (Rel r)
a✝ : R
⊢ { toQuot := Quot.mk (Rel r) a✝¹ } * { toQuot := Quot.mk (Rel r) a✝ } =
    { toQuot := Quot.mk (Rel r) a✝ } * { toQuot := Quot.mk (Rel r) 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
R : Type uR
inst✝ : CommSemiring R
r : R → R → Prop
⊢ ∀ (a b : RingQuot r), a * b = b * a

Tactic:
by
    rintro ⟨⟨⟩⟩ ⟨⟨⟩⟩
    simp [mul_quot, mul_comm]

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

Goal state before:
pp: R : Type u
inst✝⁶ : Ring R
inst✝⁵ : PartialOrder R
inst✝⁴ : StarRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : IsOrderedModule ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x
P : R := (√2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (√2)⁻¹ • (A₁ - A₀) + B₁
⊢ √2 ^ 3 • 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ =
    ((√2)⁻¹ * 2⁻¹) • 1 + ((√2)⁻¹ * 2⁻¹) • (A₀ * A₁) - 2⁻¹ • (B₀ * A₁) +
          (((√2)⁻¹ * 2⁻¹) • (A₁ * A₀) + ((√2)⁻¹ * 2⁻¹) • 1 - 2⁻¹ • (B₀ * A₀)) -
        (2⁻¹ • (A₁ * B₀) + 2⁻¹ • (A₀ * B₀) - (√2)⁻¹ • 1) +
      (((√2)⁻¹ * 2⁻¹) • 1 - ((√2)⁻¹ * 2⁻¹) • (A₀ * A₁) + 2⁻¹ • (B₁ * A₁) -
          (((√2)⁻¹ * 2⁻¹) • (A₁ * A₀) - ((√2)⁻¹ * 2⁻¹) • 1 + 2⁻¹ • (B₁ * A₀)) +
        (2⁻¹ • (A₁ * B₁) - 2⁻¹ • (A₀ * B₁) + (√2)⁻¹ • 1))

Tactic:
simp only [← T.A₀B₀_commutes, ← T.A₀B₁_commutes, ← T.A₁B₀_commutes, ← T.A₁B₁_commutes]

Goal state after:
R : Type u
inst✝⁶ : Ring R
inst✝⁵ : PartialOrder R
inst✝⁴ : StarRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : IsOrderedModule ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x
P : R := (√2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (√2)⁻¹ • (A₁ - A₀) + B₁
⊢ √2 ^ 3 • 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ =
    ((√2)⁻¹ * 2⁻¹) • 1 + ((√2)⁻¹ * 2⁻¹) • (A₀ * A₁) - 2⁻¹ • (A₁ * B₀) +
          (((√2)⁻¹ * 2⁻¹) • (A₁ * A₀) + ((√2)⁻¹ * 2⁻¹) • 1 - 2⁻¹ • (A₀ * B₀)) -
        (2⁻¹ • (A₁ * B₀) + 2⁻¹ • (A₀ * B₀) - (√2)⁻¹ • 1) +
      (((√2)⁻¹ * 2⁻¹) • 1 - ((√2)⁻¹ * 2⁻¹) • (A₀ * A₁) + 2⁻¹ • (A₁ * B₁) -
          (((√2)⁻¹ * 2⁻¹) • (A₁ * A₀) - ((√2)⁻¹ * 2⁻¹) • 1 + 2⁻¹ • (A₀ * B₁)) +
        (2⁻¹ • (A₁ * B₁) - 2⁻¹ • (A₀ * B₁) + (√2)⁻¹ • 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:
by
  rw [← Nat.cast_ofNat]
  simp [-Nat.cast_ofNat]

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
⊢ (monomial n) (-a) + (monomial n) a = 0

Tactic:
← monomial_add,

Goal state after:
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
⊢ (monomial n) (-a + a) = 0
Module: Mathlib.Algebra.Star.RingQuot

Goal state before:
pp: R✝ : Type u
inst✝³ : Semiring R✝
r✝ : R✝ → R✝ → Prop
inst✝² : StarRing R✝
R : Type u
inst✝¹ : Semiring R
inst✝ : StarRing R
r : R → R → Prop
hr : ∀ (a b : R), r a b → r (star a) (star b)
⊢ ∀ (r_1 s : RingQuot r), star' r hr (r_1 * s) = star' r hr s * star' r hr r_1

Tactic:
rintro ⟨⟨⟩⟩ ⟨⟨⟩⟩

Goal state after:
case mk.mk
R✝ : Type u
inst✝³ : Semiring R✝
r✝ : R✝ → R✝ → Prop
inst✝² : StarRing R✝
R : Type u
inst✝¹ : Semiring R
inst✝ : StarRing R
r : R → R → Prop
hr : ∀ (a b : R), r a b → r (star a) (star b)
toQuot✝¹ : Quot (Rel r)
a✝¹ : R
toQuot✝ : Quot (Rel r)
a✝ : R
⊢ star' r hr ({ toQuot := Quot.mk (Rel r) a✝¹ } * { toQuot := Quot.mk (Rel r) a✝ }) =
    star' r hr { toQuot := Quot.mk (Rel r) a✝ } * star' r hr { toQuot := Quot.mk (Rel r) a✝¹ }
Module: Mathlib.Algebra.Star.RingQuot

Goal state before:
pp: R✝ : Type u
inst✝³ : Semiring R✝
r✝ : R✝ → R✝ → Prop
inst✝² : StarRing R✝
R : Type u
inst✝¹ : Semiring R
inst✝ : StarRing R
r : R → R → Prop
hr : ∀ (a b : R), r a b → r (star a) (star b)
⊢ ∀ (r_1 s : RingQuot r), star' r hr (r_1 + s) = star' r hr r_1 + star' r hr s

Tactic:
rintro ⟨⟨⟩⟩ ⟨⟨⟩⟩

Goal state after:
case mk.mk
R✝ : Type u
inst✝³ : Semiring R✝
r✝ : R✝ → R✝ → Prop
inst✝² : StarRing R✝
R : Type u
inst✝¹ : Semiring R
inst✝ : StarRing R
r : R → R → Prop
hr : ∀ (a b : R), r a b → r (star a) (star b)
toQuot✝¹ : Quot (Rel r)
a✝¹ : R
toQuot✝ : Quot (Rel r)
a✝ : R
⊢ star' r hr ({ toQuot := Quot.mk (Rel r) a✝¹ } + { toQuot := Quot.mk (Rel r) a✝ }) =
    star' r hr { toQuot := Quot.mk (Rel r) a✝¹ } + star' r hr { toQuot := Quot.mk (Rel r) a✝ }
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

Tactic:
simp_all

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

Goal state before:
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:
simp_all

Goal state after: