mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
inst✝ : Semiring R
r : R
i : ℕ
a✝ : Nontrivial R
⊢ ((X + C r) ^ i).leadingCoeff = 1

Tactic:
rw [leadingCoeff_pow'] <;> simp

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
S : Type u_1
inst✝ : Semiring S
f g : R[X] →+* S
h₁ : ∀ (a : R), f (C a) = g (C a)
h₂ : f X = g X
⊢ f = g

Tactic:
by
  set f' := f.comp (toFinsuppIso R).symm.toRingHom with hf'
  set g' := g.comp (toFinsuppIso R).symm.toRingHom with hg'
  have A : f' = g' := by
    ext
    · simp [f', g', h₁, RingEquiv.toRingHom_eq_coe]
    simpa using! h₂
  have B : f = f'.comp (toFinsuppIso R) := by
    rw [hf', RingHom.comp_assoc]
    ext x
    simp only [RingEquiv.toRingHom_eq_coe, RingEquiv.symm_apply_apply, Function.comp_apply,
      RingHom.coe_comp, RingEquiv.coe_toRingHom]
  have C' : g = g'.comp (toFinsuppIso R) := by
    rw [hg', RingHom.comp_assoc]
    ext x
    simp only [RingEquiv.toRingHom_eq_coe, RingEquiv.symm_apply_apply, Function.comp_apply,
      RingHom.coe_comp, RingEquiv.coe_toRingHom]
  rw [B, C', A]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Eval.Degree

Goal state before:
pp: case hf
R : Type u
S : Type v
inst✝² : Semiring R
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
hf : IsUnit f.leadingCoeff
H : IsUnit (map φ f)
dz : (map φ f).degree = 0
⊢ φ f.leadingCoeff ≠ 0

Tactic:
intro h
    have u : IsUnit (φ f.leadingCoeff) := IsUnit.map φ hf
    rw [h] at u
    simp at u

Goal state after:
Module: Mathlib.Data.Finsupp.Order

Goal state before:
pp: ι : Type u_1
α : Type u_3
β : Type u_4
inst✝⁵ : Zero α
inst✝⁴ : Preorder α
inst✝³ : AddCommMonoid β
inst✝² : Preorder β
inst✝¹ : IsOrderedAddMonoid β
inst✝ : DecidableEq ι
f₁ f₂ : ι →₀ α
h : ι → α → β
hf : f₁ ≤ f₂
hh : ∀ i ∈ f₁.support ∪ f₂.support, Monotone (h i)
hh₀ : ∀ i ∈ f₁.support ∪ f₂.support, h i 0 = 0
⊢ f₁.sum h ≤ f₂.sum h

Tactic:
rw [sum_of_support_subset _ Finset.subset_union_left _ hh₀,
    sum_of_support_subset _ Finset.subset_union_right _ hh₀]
  gcongr with i hi
  exact hh _ hi <| hf _

Goal state after:
Module: Mathlib.Data.Finsupp.Order

Goal state before:
pp: α : Type u_5
M : Type u_6
N : Type u_7
inst✝³ : Zero M
inst✝² : AddCommMonoid N
inst✝¹ : PartialOrder N
inst✝ : IsOrderedAddMonoid N
f : α →₀ M
g : M → N
hg : g 0 = 0
h : 0 ≤ fun x ↦ g x
a : α
⊢ ((single a (f a)).sum fun x m ↦ g m) ≤ f.sum fun x m ↦ g m

Tactic:
apply single_le_sum _ (fun _ m ↦ h m)

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p : R[X]
n : ℕ
hp : p.coeff n ∈ R⁰
r : R
hr : r • p = 0
⊢ r * p.coeff n = 0

Tactic:
simpa using congr(coeff $hr n)

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
g : σ → S₁
r : R
P : MvPolynomial σ R
⊢ (eval₂Hom f g) (r • P) = f r • (eval₂Hom f g) P

Tactic:
simp [smul_eq_C_mul]

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
g : σ → S₁
p : MvPolynomial σ R
⊢ eval₂ f g p = (eval g) ((map f) p)

Tactic:
by
  simp [eval₂, eval]; simp [map, MvPolynomial, Finsupp.sum_mapRange_index, mapRingHom]

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.CommRing

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommRing R
i : σ
p q : MvPolynomial σ R
⊢ degreeOf i (p - q) ≤ max (degreeOf i p) (degreeOf i q)

Tactic:
by
  simpa only [sub_eq_add_neg, degreeOf_neg] using degreeOf_add_le i p (-q)

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.CommRing

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommRing R
a b : MvPolynomial σ R
⊢ (a - b).totalDegree = (a + -b).totalDegree

Tactic:
rw [sub_eq_add_neg]

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: R : Type u
S₂ : Type w
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₂
f : R →+* S₂
g : σ → S₂
φ : MvPolynomial σ R
h : ∀ (d : σ →₀ ℕ), coeff d φ ≠ 0 → ∃ i ∈ d.support, g i = 0
⊢ (eval₂Hom f g) φ = 0

Tactic:
rw [φ.as_sum, map_sum]

Goal state after:
R : Type u
S₂ : Type w
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₂
f : R →+* S₂
g : σ → S₂
φ : MvPolynomial σ R
h : ∀ (d : σ →₀ ℕ), coeff d φ ≠ 0 → ∃ i ∈ d.support, g i = 0
⊢ ∑ x ∈ φ.support, (eval₂Hom f g) ((monomial x) (coeff x φ)) = 0
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
i : σ
h : degreeOf i q < degreeOf i p
this : p.support.Nonempty
s : σ →₀ ℕ
hs1 : s ∈ p.support
hs2 : degreeOf i p = s i
⊢ degreeOf i p ≤ s i

Tactic:
hs2

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
i : σ
h : degreeOf i q < degreeOf i p
this : p.support.Nonempty
s : σ →₀ ℕ
hs1 : s ∈ p.support
hs2 : degreeOf i p = s i
⊢ s i ≤ s i
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
i : σ
this : p.support.Nonempty
s : σ →₀ ℕ
hs1 : s ∈ p.support
hs2 : degreeOf i p = s i
h : s ∈ q.support
⊢ degreeOf i p ≤ degreeOf i q

Tactic:
hs2

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
i : σ
this : p.support.Nonempty
s : σ →₀ ℕ
hs1 : s ∈ p.support
hs2 : degreeOf i p = s i
h : s ∈ q.support
⊢ s i ≤ degreeOf i q
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
a : ℕ
h : a ∈ f.eraseLead.support
⊢ a < f.natDegree

Tactic:
by
  rw [eraseLead_support, mem_erase] at h
  exact (le_natDegree_of_mem_supp a h.2).lt_of_ne h.1

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

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
p q : R[X]
pq : p.degree < q.degree
n : ℕ
nd : n = q.natDegree
⊢ (p + q).eraseLead.coeff n = (p + q.eraseLead).coeff n

Tactic:
rw [nd, eraseLead_coeff, if_pos (natDegree_add_eq_right_of_degree_lt pq).symm]
    simpa using (coeff_eq_zero_of_degree_lt (lt_of_lt_of_le pq degree_le_natDegree)).symm

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

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
N O : ℕ
f : R[X]
Cf : #f.support ≤ Nat.succ 0
Nf : f.natDegree ≤ N
cg : ℕ
hcg : ∀ (g : R[X]), #g.support ≤ cg.succ → g.natDegree ≤ O → reflect (N + O) (f * g) = reflect N f * reflect O g
g : R[X]
Cg : #g.support ≤ (cg + 1).succ
Og : g.natDegree ≤ O
g0 : g = 0
⊢ reflect (N + O) (f * g) = reflect N f * reflect O g

pp: case neg
R : Type u_1
inst✝ : Semiring R
N O : ℕ
f : R[X]
Cf : #f.support ≤ Nat.succ 0
Nf : f.natDegree ≤ N
cg : ℕ
hcg : ∀ (g : R[X]), #g.support ≤ cg.succ → g.natDegree ≤ O → reflect (N + O) (f * g) = reflect N f * reflect O g
g : R[X]
Cg : #g.support ≤ (cg + 1).succ
Og : g.natDegree ≤ O
g0 : ¬g = 0
⊢ reflect (N + O) (f * g) = reflect N f * reflect O g

Tactic:
· rw [g0, reflect_zero, mul_zero, mul_zero, reflect_zero]

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
N O : ℕ
f : R[X]
Cf : #f.support ≤ Nat.succ 0
Nf : f.natDegree ≤ N
cg : ℕ
hcg : ∀ (g : R[X]), #g.support ≤ cg.succ → g.natDegree ≤ O → reflect (N + O) (f * g) = reflect N f * reflect O g
g : R[X]
Cg : #g.support ≤ (cg + 1).succ
Og : g.natDegree ≤ O
g0 : ¬g = 0
⊢ reflect (N + O) (f * g) = reflect N f * reflect O g
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.nextCoeff ≠ 0
this : 0 < f.natDegree
⊢ f.eraseLead.coeff f.eraseLead.natDegree = f.nextCoeff

Tactic:
nextCoeff,

Goal state after:
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.nextCoeff ≠ 0
this : 0 < f.natDegree
⊢ f.eraseLead.coeff f.eraseLead.natDegree = if f.natDegree = 0 then 0 else f.coeff (f.natDegree - 1)
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: R : Type u_2
inst✝² : Ring R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
x : R
P : R[X]
hx : x ≠ 0
hp : ¬P = 0
he : ¬P.eraseLead = 0
h₁ : ((X - C x) * P).natDegree = P.natDegree + 1
dP : ℕ
hdP : P.natDegree = dP + 2
h : P.coeff (dP + 1) = 0
⊢ ((X - C x) * P).nextCoeff ≠ 0

Tactic:
nextCoeff,

Goal state after:
R : Type u_2
inst✝² : Ring R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
x : R
P : R[X]
hx : x ≠ 0
hp : ¬P = 0
he : ¬P.eraseLead = 0
h₁ : ((X - C x) * P).natDegree = P.natDegree + 1
dP : ℕ
hdP : P.natDegree = dP + 2
h : P.coeff (dP + 1) = 0
⊢ (if ((X - C x) * P).natDegree = 0 then 0 else ((X - C x) * P).coeff (((X - C x) * P).natDegree - 1)) ≠ 0
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: case inl
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
q : R[X]
hq : 0 < q.degree
⊢ (comp 0 q).degree = degree 0 * q.degree

Tactic:
rw [zero_comp, degree_zero, WithBot.bot_mul']
    simp [hq.ne']

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

Goal state before:
pp: case succ.zero
R : Type u_1
inst✝ : Semiring R
motive : R[X] → Prop
N : ℕ
zero : motive 0
C_mul_pow : ∀ (n : ℕ) (r : R), r ≠ 0 → n ≤ N → motive (C r * X ^ n)
add : ∀ (f g : R[X]), f.natDegree < g.natDegree → g.natDegree ≤ N → motive f → motive g → motive (f + g)
f : R[X]
df : f.natDegree ≤ N
hc : ∀ (f : R[X]), f.natDegree ≤ N → #f.support = 0 → motive f
hf : #f.support = 0 + 1
⊢ f.leadingCoeff ≠ 0

Tactic:
rw [leadingCoeff_ne_zero, Ne, ← card_support_eq_zero, hf]
        exact zero_ne_one.symm

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: case neg
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
p : MvPolynomial (Option S₁) R
i : ℕ
hi : i ≤ p.totalDegree
hpi : ¬((optionEquivLeft R S₁) p).coeff i = 0
σ : S₁ →₀ ℕ
hσ : σ ∈ (((optionEquivLeft R S₁) p).coeff i).support
⊢ (i + σ.sum fun x e ↦ e) ≤ p.totalDegree

Tactic:
refine le_trans ?_ (Finset.le_sup (b := σ.embDomain .some + .single .none i) ?_)

Goal state after:
case neg.refine_1
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
p : MvPolynomial (Option S₁) R
i : ℕ
hi : i ≤ p.totalDegree
hpi : ¬((optionEquivLeft R S₁) p).coeff i = 0
σ : S₁ →₀ ℕ
hσ : σ ∈ (((optionEquivLeft R S₁) p).coeff i).support
⊢ (i + σ.sum fun x e ↦ e) ≤ (embDomain Embedding.some σ + Finsupp.single none i).sum fun x e ↦ e

case neg.refine_2
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
p : MvPolynomial (Option S₁) R
i : ℕ
hi : i ≤ p.totalDegree
hpi : ¬((optionEquivLeft R S₁) p).coeff i = 0
σ : S₁ →₀ ℕ
hσ : σ ∈ (((optionEquivLeft R S₁) p).coeff i).support
⊢ embDomain Embedding.some σ + Finsupp.single none i ∈ p.support
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: case neg
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
p : MvPolynomial (Option S₁) R
i : ℕ
hpi : ¬((optionEquivLeft R S₁) p).coeff i = 0
σ : S₁ →₀ ℕ
hσ : σ ∈ (((optionEquivLeft R S₁) p).coeff i).support
⊢ (σ.sum fun x e ↦ e) ≤ p.totalDegree

Tactic:
refine le_trans ?_ (Finset.le_sup (b := σ.embDomain .some + .single .none i) ?_)

Goal state after:
case neg.refine_1
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
p : MvPolynomial (Option S₁) R
i : ℕ
hpi : ¬((optionEquivLeft R S₁) p).coeff i = 0
σ : S₁ →₀ ℕ
hσ : σ ∈ (((optionEquivLeft R S₁) p).coeff i).support
⊢ (σ.sum fun x e ↦ e) ≤ (embDomain Embedding.some σ + Finsupp.single none i).sum fun x e ↦ e

case neg.refine_2
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
p : MvPolynomial (Option S₁) R
i : ℕ
hpi : ¬((optionEquivLeft R S₁) p).coeff i = 0
σ : S₁ →₀ ℕ
hσ : σ ∈ (((optionEquivLeft R S₁) p).coeff i).support
⊢ embDomain Embedding.some σ + Finsupp.single none i ∈ p.support
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: case hC
R : Type u
inst✝ : CommSemiring R
n : ℕ
i : R
⊢ ((↑(finSuccEquiv R n)).comp C) i =
    ((eval₂Hom (Polynomial.C.comp C) fun i ↦ Fin.cases Polynomial.X (fun k ↦ Polynomial.C (X k)) i).comp C) i

pp: case hX
R : Type u
inst✝ : CommSemiring R
n : ℕ
i : Fin (n + 1)
n✝ : ℕ
⊢ (↑(finSuccEquiv R n) (X i)).coeff n✝ =
    ((eval₂Hom (Polynomial.C.comp C) fun i ↦ Fin.cases Polynomial.X (fun k ↦ Polynomial.C (X k)) i) (X i)).coeff n✝

Tactic:
· simp only [finSuccEquiv, optionEquivLeft_apply, aeval_C, AlgEquiv.coe_trans, RingHom.coe_coe,
      coe_eval₂Hom, comp_apply, renameEquiv_apply, eval₂_C, RingHom.coe_comp, rename_C]
    rfl

Goal state after:
case hX
R : Type u
inst✝ : CommSemiring R
n : ℕ
i : Fin (n + 1)
n✝ : ℕ
⊢ (↑(finSuccEquiv R n) (X i)).coeff n✝ =
    ((eval₂Hom (Polynomial.C.comp C) fun i ↦ Fin.cases Polynomial.X (fun k ↦ Polynomial.C (X k)) i) (X i)).coeff n✝
Module: Mathlib.Algebra.Polynomial.BigOperators

Goal state before:
pp: case hadd
S : Type u_1
inst✝ : Semiring S
l : List S[X]
⊢ ∀ (x y : S[X]), (x + y).natDegree ≤ max x.natDegree y.natDegree

Tactic:
exact natDegree_add_le

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

Goal state before:
pp: case cons
S : Type u_1
inst✝ : Semiring S
n : WithBot ℕ
hd : S[X]
tl : List S[X]
ih : (∀ p ∈ tl, p.degree ≤ n) → tl.sum.degree ≤ n
hl : ∀ p ∈ hd :: tl, p.degree ≤ n
⊢ (hd :: tl).sum.degree ≤ n

Tactic:
simp only [List.mem_cons, forall_eq_or_imp] at hl
    rcases hl with ⟨hhd, htl⟩
    rw [List.sum_cons]
    exact le_trans (degree_add_le hd tl.sum) (max_le hhd (ih htl))

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: case mp
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin (n + 1) →₀ ℕ
⊢ (∃ x, ¬coeff (cons i x) f = 0 ∧ cons i x = m) → coeff m f ≠ 0 ∧ m 0 = i

pp: case mpr
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin (n + 1) →₀ ℕ
⊢ coeff m f ≠ 0 ∧ m 0 = i → ∃ x, ¬coeff (cons i x) f = 0 ∧ cons i x = m

Tactic:
· grind [cons_zero]

Goal state after:
case mpr
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin (n + 1) →₀ ℕ
⊢ coeff m f ≠ 0 ∧ m 0 = i → ∃ x, ¬coeff (cons i x) f = 0 ∧ cons i x = m
Module: Mathlib.Algebra.Polynomial.BigOperators

Goal state before:
pp: R : Type u
inst✝ : CommRing R
t : Multiset R
ht : 0 < t.card
a✝ : Nontrivial R
⊢ (Multiset.map (fun x ↦ X - C x) t).prod.coeff (t.card - 1) = (Multiset.map (fun x ↦ X - C x) t).prod.nextCoeff

Tactic:
nextCoeff,

Goal state after:
R : Type u
inst✝ : CommRing R
t : Multiset R
ht : 0 < t.card
a✝ : Nontrivial R
⊢ (Multiset.map (fun x ↦ X - C x) t).prod.coeff (t.card - 1) =
    if (Multiset.map (fun x ↦ X - C x) t).prod.natDegree = 0 then 0
    else (Multiset.map (fun x ↦ X - C x) t).prod.coeff ((Multiset.map (fun x ↦ X - C x) t).prod.natDegree - 1)
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
hp : p.Monic
hpq : q.degree < p.degree
⊢ (p - q).Monic

Tactic:
rw [sub_eq_add_neg]

Goal state after:
R : Type u
inst✝ : Ring R
p q : R[X]
hp : p.Monic
hpq : q.degree < p.degree
⊢ (p + -q).Monic
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.leadingCoeff = -1
hpq : p.degree < q.degree
this : (-q).coeff (-q).natDegree = 1
⊢ (p - q).Monic

Tactic:
rw [sub_eq_add_neg]

Goal state after:
R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.leadingCoeff = -1
hpq : p.degree < q.degree
this : (-q).coeff (-q).natDegree = 1
⊢ (p + -q).Monic
Module: Mathlib.Algebra.Ring.GeomSum

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Ring R
r : R
p a b : ℕ
h : a ∣ b
hp₀ : ¬p = 0
hp : ∀ (c : ℕ), 1 ≤ p ^ c
⊢ ↑p ^ a - 1 ∣ ↑p ^ b - 1

Tactic:
exact dvd_pow_sub_one_of_dvd h

Goal state after:
Module: Mathlib.RingTheory.Adjoin.FG

Goal state before:
pp: case refine_2
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : (Subalgebra.toSubmodule (adjoin R s)).FG
h2 : (Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)).FG
p : Set A
hp : p.Finite
hp' : span R p = Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : q.Finite
hq' : span (↥(adjoin R s)) q = Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)
l : A →₀ ↥(adjoin R s)
hlq : l ∈ Finsupp.supported (↥(adjoin R s)) (↥(adjoin R s)) q
this :
  ∀ [inst : Semiring ↥(adjoin R s)] [inst_1 : AddCommMonoid A] [inst_2 : Module (↥(adjoin R s)) A] {v : A → A}
    (l : A →₀ ↥(adjoin R s)), (Finsupp.linearCombination (↥(adjoin R s)) v) l = l.sum fun i a ↦ a • v i
z : A
⊢ z ∈ l.support → l z • _root_.id z ∈ span R (p * q)

Tactic:
hz

Goal state after:
case refine_2
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : (Subalgebra.toSubmodule (adjoin R s)).FG
h2 : (Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)).FG
p : Set A
hp : p.Finite
hp' : span R p = Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : q.Finite
hq' : span (↥(adjoin R s)) q = Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)
l : A →₀ ↥(adjoin R s)
hlq : l ∈ Finsupp.supported (↥(adjoin R s)) (↥(adjoin R s)) q
this :
  ∀ [inst : Semiring ↥(adjoin R s)] [inst_1 : AddCommMonoid A] [inst_2 : Module (↥(adjoin R s)) A] {v : A → A}
    (l : A →₀ ↥(adjoin R s)), (Finsupp.linearCombination (↥(adjoin R s)) v) l = l.sum fun i a ↦ a • v i
z : A
hz : z ∈ l.support
⊢ l z • _root_.id z ∈ span R (p * q)
Module: Mathlib.RingTheory.Adjoin.Tower

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Semiring A
inst✝³ : Algebra R S
inst✝² : Algebra S A
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R S A
s : Finset S
hs : adjoin R ↑s = ⊤
t : Finset A
ht : adjoin S ↑t = ⊤
⊢ adjoin R ↑(Finset.image (⇑(algebraMap S A)) s ∪ t) = ⊤

Tactic:
Finset.coe_union,

Goal state after:
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Semiring A
inst✝³ : Algebra R S
inst✝² : Algebra S A
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R S A
s : Finset S
hs : adjoin R ↑s = ⊤
t : Finset A
ht : adjoin S ↑t = ⊤
⊢ adjoin R (↑(Finset.image (⇑(algebraMap S A)) s) ∪ ↑t) = ⊤
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
ι : Type u_2
s : Finset ι
f : ι → R[X]
I : Ideal R
n : ι → ℕ
h : ∀ i ∈ s, ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)
k : ℕ
⊢ (s.prod f).coeff k ∈ I ^ (s.sum n - k)

Tactic:
classical
    induction s using Finset.induction generalizing k with
    | empty =>
      rw [sum_empty, prod_empty, coeff_one, zero_tsub, pow_zero, Ideal.one_eq_top]
      exact Submodule.mem_top
    | insert a s ha hs =>
      rw [sum_insert ha, prod_insert ha, coeff_mul]
      apply sum_mem
      rintro ⟨i, j⟩ e
      obtain rfl : i + j = k := mem_antidiagonal.mp e
      apply Ideal.pow_le_pow_right add_tsub_add_le_tsub_add_tsub
      rw [pow_add]
      exact Ideal.mul_mem_mul (by grind) (by grind)

Goal state after:
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: R : Type uR
S : Type uS
A : Type uA
B : Type uB
M : Type uM
N : Type uN
inst✝¹² : CommSemiring R
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Semiring A
inst✝⁹ : Semiring B
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R A
inst✝⁶ : Algebra R B
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
ι : Type u_1
inst✝¹ : Finite ι
inst✝ : FiniteType R S
⊢ FiniteType R (MvPolynomial ι S)

Tactic:
classical
  cases nonempty_fintype ι
  refine .trans ‹_› ⟨Finset.univ.image MvPolynomial.X, ?_⟩
  rw [Finset.coe_image, Finset.coe_univ, Set.image_univ]
  exact MvPolynomial.adjoin_range_X

Goal state after:
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: R : Type uR
S : Type uS
A : Type uA
B : Type uB
M : Type uM
N : Type uN
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra R B
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
hA : FiniteType R A
hB : FiniteType R B
⊢ ⊤.FG

Tactic:
by rw [← Subalgebra.prod_top]; exact hA.1.prod hB.1

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Pointwise

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Subalgebra R A
y : A
hy : y ∈ toSubmodule S
z : A
⊢ z ∈ toSubmodule T → y * z ∈ toSubmodule (S ⊔ T)

Tactic:
hz

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Subalgebra R A
y : A
hy : y ∈ toSubmodule S
z : A
hz : z ∈ toSubmodule T
⊢ y * z ∈ toSubmodule (S ⊔ T)
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
p q : R[X]
v : M
hv : v ∈ ((aeval f) (p * q)).ker
p' q' : R[X]
hpq' : p' * p + q' * q = 1
⊢ ((aeval f) (p' * (q * p))) v = ((aeval f) (p' * (p * q))) v

Tactic:
mul_comm q p

Goal state after:
R : Type u
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
p q : R[X]
v : M
hv : v ∈ ((aeval f) (p * q)).ker
p' q' : R[X]
hpq' : p' * p + q' * q = 1
⊢ ((aeval f) (p' * (p * q))) v = ((aeval f) (p' * (p * q))) v
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
M : Type u_1
x✝² : AddCommMonoid M
x✝¹ : Module R M
x✝ : Module.Finite R M
N : Submodule R M
f : ↥N →ₗ[R] M
hf : Surjective ⇑f
this✝² : AddCommGroup M := addCommMonoidToAddCommGroup R
this✝¹ : AddCommGroup ↥N := addCommMonoidToAddCommGroup R
i : ↥N →ₗ[R] M := N.subtype
hi : Function.Injective ⇑i := injective_subtype N
n : ↥N
hn : f n = 0
k : ℕ
mj : Fin k → M
hmj : Surjective ⇑((Module.piEquiv (Fin k) R M) mj)
b : Fin k → R
hb : ((Module.piEquiv (Fin k) R M) mj) b = i n
nj : Fin k → ↥N
hnj : ∀ (j : Fin k), f (nj j) = mj j
c : Fin k → Fin k → R
hc : ∀ (j : Fin k), ((Module.piEquiv (Fin k) R M) mj) (c j) = i (nj j)
A : Subring R := Subring.closure (Set.range b ∪ Set.range (Function.uncurry c))
N' : Submodule ↥A ↥N := span (↥A) ({n} ∪ Set.range nj)
M' : Submodule (↥A) M := span (↥A) (Set.range mj)
this✝ : IsNoetherianRing ↥A
this : Module.Finite ↥A ↥M'
x : ↥N
j : Fin k
⊢ f (nj j) ∈ Set.range mj

Tactic:
by simp [hnj]

Goal state after:
Module: Mathlib.Data.Int.ModEq

Goal state before:
pp: case succ
n a b : ℤ
h : a ≡ b [ZMOD n]
d : ℕ
hd : a ^ d ≡ b ^ d [ZMOD n]
⊢ a ^ d * a ≡ b ^ d * b [ZMOD n]

Tactic:
exact hd.mul h

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: R : Type u
S : Type v
F : Type w
inst✝² : Ring R
inst✝¹ : Semiring S
ι : Type u_1
I : ι → Ideal R
inst✝ : ∀ (i : ι), (I i).IsTwoSided
⊢ ∀ a ∈ ⨅ i, I i, (RingHom.pi fun i ↦ Quotient.mk (I i)) a = 0

Tactic:
simp [← RingHom.mem_ker, ker_Pi_Quotient_mk]

Goal state after:
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case cons
α : Type u_1
inst✝ : DecidableEq α
x d d' y : α
ys : List α
IH : x ∈ ys.dropLast → ys.nextOr x d = ys.nextOr x d'
x_mem : x ∈ (y :: ys).dropLast
⊢ (y :: ys).nextOr x d = (y :: ys).nextOr x d'

Tactic:
rcases ys with - | ⟨z, zs⟩

Goal state after:
case cons.nil
α : Type u_1
inst✝ : DecidableEq α
x d d' y : α
IH : x ∈ [].dropLast → [].nextOr x d = [].nextOr x d'
x_mem : x ∈ [y].dropLast
⊢ [y].nextOr x d = [y].nextOr x d'

case cons.cons
α : Type u_1
inst✝ : DecidableEq α
x d d' y z : α
zs : List α
IH : x ∈ (z :: zs).dropLast → (z :: zs).nextOr x d = (z :: zs).nextOr x d'
x_mem : x ∈ (y :: z :: zs).dropLast
⊢ (y :: z :: zs).nextOr x d = (y :: z :: zs).nextOr x d'
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case cons
α : Type u_1
inst✝ : DecidableEq α
x d y : α
ys : List α
IH : ys.nextOr x d ≠ d → x ∈ ys
h : (y :: ys).nextOr x d ≠ d
⊢ x ∈ y :: ys

Tactic:
rcases ys with - | ⟨z, zs⟩

Goal state after:
case cons.nil
α : Type u_1
inst✝ : DecidableEq α
x d y : α
IH : [].nextOr x d ≠ d → x ∈ []
h : [y].nextOr x d ≠ d
⊢ x ∈ [y]

case cons.cons
α : Type u_1
inst✝ : DecidableEq α
x d y z : α
zs : List α
IH : (z :: zs).nextOr x d ≠ d → x ∈ z :: zs
h : (y :: z :: zs).nextOr x d ≠ d
⊢ x ∈ y :: z :: zs