mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.DFinsupp.Lex

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : LinearOrder ι
inst✝ : (i : ι) → PartialOrder (α i)
a b : Π₀ (i : ι), α i
h : a ≤ b
hne : ¬toLex a = toLex b
⊢ toLex a < toLex b

Tactic:
exact ⟨Finset.min' _ (nonempty_neLocus_iff.2 hne),
    fun j hj ↦ notMem_neLocus.1 fun h ↦ (Finset.min'_le _ _ h).not_gt hj,
    (h _).lt_of_ne (mem_neLocus.1 <| Finset.min'_mem _ _)⟩

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

Goal state before:
pp: R : Type u
σ : Type u_1
r : R
inst✝ : CommSemiring R
⊢ (C r).vars = ∅

Tactic:
rw [vars_def, degrees_C, Multiset.toFinset_zero]

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
i : σ
e : ℕ
r : R
he : e ≠ 0
hr : r ≠ 0
⊢ ((monomial (Finsupp.single i e)) r).vars = {i}

Tactic:
by
  rw [vars_monomial hr, Finsupp.support_single _ he]

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finsupp.Fin

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : Zero M
inst✝ : AddCommMonoid N
n : ℕ
σ : Fin n →₀ M
i : M
f : Fin (n + 1) → M → N
h : ∀ (x : Fin (n + 1)), f x 0 = 0
⊢ (cons i σ).sum f = f 0 i + σ.sum (Fin.tail f)

Tactic:
sum_fintype _ _ (fun _ => by apply h),

Goal state after:
M : Type u_1
N : Type u_2
inst✝¹ : Zero M
inst✝ : AddCommMonoid N
n : ℕ
σ : Fin n →₀ M
i : M
f : Fin (n + 1) → M → N
h : ∀ (x : Fin (n + 1)), f x 0 = 0
⊢ ∑ i_1, f i_1 ((cons i σ) i_1) = f 0 i + σ.sum (Fin.tail f)
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s : σ →₀ ℕ
c : R
hc : c ≠ 0
⊢ ((monomial s) c).totalDegree = s.sum fun x e ↦ e

Tactic:
classical simp [totalDegree, support_monomial, if_neg hc]

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

Goal state before:
pp: case succ
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
hf : p.natDegree ≤ n + 1
hn : p.coeff (n + 1) = 0
h : p.natDegree = n.succ
⊢ False

Tactic:
rw [← Nat.succ_eq_add_one, ← h, coeff_natDegree, leadingCoeff_eq_zero] at hn

Goal state after:
case succ
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
hf : p.natDegree ≤ n + 1
hn : p = 0
h : p.natDegree = n.succ
⊢ False
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
this : DecidableEq R := Classical.decEq R
h0 : ¬p.comp q = 0
n : ℕ
hn : n ∈ p.support
⊢ ↑(C (p.coeff n)).natDegree + n • q.degree ≤ ↑(C (p.coeff n)).natDegree + n • ↑q.natDegree

Tactic:
by grw [degree_le_natDegree]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
h : p.coeff 0 ≠ 0
⊢ p.coeff p.natTrailingDegree = p.coeff 0

Tactic:
(natTrailingDegree_eq_zero.mpr <| .inr h)

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
h : p.coeff 0 ≠ 0
⊢ p.coeff 0 = p.coeff 0
Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree

Goal state before:
pp: R : Type u
a : R
inst✝ : Semiring R
n : ℕ
ha : a ≠ 0
⊢ (C a * X ^ n).trailingDegree = ↑n

Tactic:
rw [C_mul_X_pow_eq_monomial, trailingDegree_monomial ha]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
i j : ℕ
h₁ : (i, j) ∈ antidiagonal (p.natTrailingDegree + q.natTrailingDegree)
h₂ : (i, j) ≠ (p.natTrailingDegree, q.natTrailingDegree)
⊢ p.coeff (i, j).1 * q.coeff (i, j).2 = 0

Tactic:
mem_antidiagonal

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
i j : ℕ
h₁ : (i, j).1 + (i, j).2 = p.natTrailingDegree + q.natTrailingDegree
h₂ : (i, j) ≠ (p.natTrailingDegree, q.natTrailingDegree)
⊢ p.coeff (i, j).1 * q.coeff (i, j).2 = 0
Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.trailingCoeff * q.trailingCoeff ≠ 0
hp : p ≠ 0
⊢ (p * q).trailingDegree = p.trailingDegree + q.trailingDegree

Tactic:
have hq : q ≠ 0 := fun hq => h (by rw [hq, trailingCoeff_zero, mul_zero])

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.trailingCoeff * q.trailingCoeff ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ (p * q).trailingDegree = p.trailingDegree + q.trailingDegree
Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.trailingCoeff * q.trailingCoeff ≠ 0
hp : p ≠ 0
⊢ (p * q).natTrailingDegree = p.natTrailingDegree + q.natTrailingDegree

Tactic:
have hq : q ≠ 0 := fun hq => h (by rw [hq, trailingCoeff_zero, mul_zero])

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.trailingCoeff * q.trailingCoeff ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ (p * q).natTrailingDegree = p.natTrailingDegree + q.natTrailingDegree
Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ∞
h : p.trailingDegree < n
h₀ : p = 0
⊢ n ≤ p.trailingDegree

Tactic:
by simp [h₀]

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

Goal state before:
pp: case pos.refine_1
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
s : Finset S
h : {i | i ∈ s ∧ f i ≠ 0}.Pairwise (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : s.Nonempty
⊢ (s.sup' hs fun i ↦ (f i).degree) ≤ s.sup' hs (WithBot.some ∘ fun i ↦ (f i).natDegree)

pp: case pos.refine_2
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
s : Finset S
h : {i | i ∈ s ∧ f i ≠ 0}.Pairwise (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : s.Nonempty
⊢ s.sup' hs (WithBot.some ∘ fun i ↦ (f i).natDegree) ≤ s.sup' hs fun i ↦ (f i).degree

Tactic:
· rw [Finset.sup'_le_iff]
        intro b hb
        by_cases hb' : f b = 0
        · simpa [hb'] using! hs
        rw [degree_eq_natDegree hb', Nat.cast_withBot]
        exact Finset.le_sup' (fun i : S => (natDegree (f i) : WithBot ℕ)) hb

Goal state after:
case pos.refine_2
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
s : Finset S
h : {i | i ∈ s ∧ f i ≠ 0}.Pairwise (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : s.Nonempty
⊢ s.sup' hs (WithBot.some ∘ fun i ↦ (f i).natDegree) ≤ s.sup' hs fun i ↦ (f i).degree
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 * 0) = reflect N f * 0

Tactic:
mul_zero,

Goal state after:
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) 0 = reflect N f * 0
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) 0 = reflect N f * 0

Tactic:
mul_zero,

Goal state after:
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) 0 = 0
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
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.eraseLead + C g.leadingCoeff * X ^ g.natDegree)) =
    reflect N f * reflect O (g.eraseLead + C g.leadingCoeff * X ^ g.natDegree)

Tactic:
mul_add,

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.eraseLead + f * (C g.leadingCoeff * X ^ g.natDegree)) =
    reflect N f * reflect O (g.eraseLead + C g.leadingCoeff * X ^ g.natDegree)
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
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.eraseLead) + reflect (N + O) (f * (C g.leadingCoeff * X ^ g.natDegree)) =
    reflect N f * (reflect O g.eraseLead + reflect O (C g.leadingCoeff * X ^ g.natDegree))

Tactic:
mul_add,

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.eraseLead) + reflect (N + O) (f * (C g.leadingCoeff * X ^ g.natDegree)) =
    reflect N f * reflect O g.eraseLead + reflect N f * reflect O (C g.leadingCoeff * X ^ g.natDegree)
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: case neg
R : Type u_2
inst✝² : Ring R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
x : R
P : R[X]
hx : x ≠ 0
h : P.nextCoeff = 0
hp : ¬P = 0
he : ¬P.eraseLead = 0
⊢ ((X - C x) * P).eraseLead.eraseLead = (X - C x) * P.eraseLead

Tactic:
have h₁ : ((X - C x) * P).natDegree = P.natDegree + 1 := by
    rw [natDegree_mul (X_sub_C_ne_zero x) hp, natDegree_X_sub_C, add_comm]

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
hf : Function.Injective ⇑f
p : R[X]
⊢ (map f p).degree = p.degree

Tactic:
simp [hf, map_ne_zero_iff, ne_or_eq]

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

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

Tactic:
mul_zero,

Goal state after:
case neg.inl.succ
R : Type u_2
inst✝² : Ring R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
x : R
P : R[X]
hx : x ≠ 0
h : P.nextCoeff = 0
hp : ¬P = 0
he : ¬P.eraseLead = 0
h₁ : ((X - C x) * P).natDegree = P.natDegree + 1
dP : ℕ
hdP : P.natDegree = dP + 2
h₂ : ((X - C x) * P).nextCoeff ≠ 0
n : ℕ
hn : n < P.natDegree
hd₁ : n < ((X - C x) * P).eraseLead.natDegree
n✝ : ℕ
hn₂ : n = n✝ + 1
⊢ 0 - 0 = 0
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
h : p.comp q = 0
⊢ p = 0 ∨ eval (q.coeff 0) p = 0 ∧ q = C (q.coeff 0)

Tactic:
have key : p.natDegree = 0 ∨ q.natDegree = 0 := by
    rw [← mul_eq_zero, ← natDegree_comp, h, natDegree_zero]

Goal state after:
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
h : p.comp q = 0
key : p.natDegree = 0 ∨ q.natDegree = 0
⊢ p = 0 ∨ eval (q.coeff 0) p = 0 ∧ q = C (q.coeff 0)
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial (Option σ) R
m : ℕ
d : σ →₀ ℕ
⊢ coeff d (((optionEquivLeft R σ) p).coeff m) = coeff (optionElim m d) p

Tactic:
rw [← optionEquivLeft_coeff_some_coeff_none]
  congr <;> simp

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

Goal state before:
pp: case pos
R : Type u_2
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
f g : R[X]
f0 : ¬f = 0
g0 : g = 0
⊢ (f * 0).reverse = f.reverse * reverse 0

Tactic:
mul_zero,

Goal state after:
case pos
R : Type u_2
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
f g : R[X]
f0 : ¬f = 0
g0 : g = 0
⊢ reverse 0 = f.reverse * reverse 0
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: case refine_2
R : Type u
ι : Type y
inst✝ : CommSemiring R
t✝ : Multiset ι
f : ι → R[X]
a : ι
t : Multiset ι
ih : (∀ i ∈ t, (f i).Monic) → (Multiset.map f t).prod.Monic
ht : ∀ i ∈ a ::ₘ t, (f i).Monic
⊢ (f a * (Multiset.map f t).prod).Monic

Tactic:
exact (ht _ (Multiset.mem_cons_self _ _)).mul (ih fun _ hi => ht _ (Multiset.mem_cons_of_mem hi))

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

Goal state before:
pp: case refine_1
R : Type u
ι : Type y
inst✝ : CommSemiring R
t : Multiset ι
f : ι → R[X]
⊢ (C 1).nextCoeff = 0

Tactic:
rw [nextCoeff_C_eq_zero]

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

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
n : ℕ
hn : ∀ {f : R[X]}, #f.support = n → ∃ k x, ∃ (_ : StrictMono k) (_ : ∀ (i : Fin n), x i ≠ 0), f = ∑ i, C (x i) * X ^ k i
f : R[X]
h : #f.support = n + 1
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf : f.eraseLead = ∑ i, C (x i) * X ^ k i
H : ¬∃ k, k.castSucc = Fin.last n
i j : Fin n
hij : i.castSucc < j.castSucc
⊢ i < j

Tactic:
← Fin.castSucc_lt_castSucc_iff

Goal state after:
case pos
R : Type u_1
inst✝ : Semiring R
n : ℕ
hn : ∀ {f : R[X]}, #f.support = n → ∃ k x, ∃ (_ : StrictMono k) (_ : ∀ (i : Fin n), x i ≠ 0), f = ∑ i, C (x i) * X ^ k i
f : R[X]
h : #f.support = n + 1
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf : f.eraseLead = ∑ i, C (x i) * X ^ k i
H : ¬∃ k, k.castSucc = Fin.last n
i j : Fin n
hij : i.castSucc < j.castSucc
⊢ i.castSucc < j.castSucc
Module: Mathlib.Algebra.Ring.GeomSum

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
x : R
n : ℕ
this : -((∑ i ∈ range n, x ^ i) * (x - 1)) = 1 - x ^ n
⊢ (∑ i ∈ range n, x ^ i) * (1 - x) = 1 - x ^ n

Tactic:
← mul_neg,

Goal state after:
R : Type u_1
inst✝ : Ring R
x : R
n : ℕ
this : (∑ i ∈ range n, x ^ i) * -(x - 1) = 1 - x ^ n
⊢ (∑ i ∈ range n, x ^ i) * (1 - x) = 1 - x ^ n
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: case mp
R : Type u
inst✝ : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
q : R[X]
⊢ q * p = 0 → q = 0

Tactic:
intro hp
    replace hp := congr_arg (· * C ↑h.unit⁻¹) hp
    simp only [zero_mul] at hp
    rwa [mul_assoc, Monic.mul_left_eq_zero_iff] at hp
    refine monic_mul_C_of_leadingCoeff_mul_eq_one ?_
    simp

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

Goal state before:
pp: 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)
x : A
hx : x ∈ p
y : A
hy : y ∈ q
⊢ x ∈ Subalgebra.toSubmodule (adjoin R s)

Tactic:
rw [← hp']

Goal state after:
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)
x : A
hx : x ∈ p
y : A
hy : y ∈ q
⊢ x ∈ span R p
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case pos
R : Type u
inst✝ : Semiring R
s : Set R[X]
p : R[X]
hs : s.Nonempty
hp : p ∈ Submodule.span R s
h : ∀ p' ∈ s, p'.degree < degree 0
hp_zero : p = 0
⊢ False

Tactic:
degree_zero

Goal state after:
case pos
R : Type u
inst✝ : Semiring R
s : Set R[X]
p : R[X]
hs : s.Nonempty
hp : p ∈ Submodule.span R s
h : ∀ p' ∈ s, p'.degree < ⊥
hp_zero : p = 0
⊢ False
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : #f.support = 3
⊢ ∃ k m n,
    ∃ (_ : k < m) (_ : m < n),
      ∃ x y z, ∃ (_ : x ≠ 0) (_ : y ≠ 0) (_ : z ≠ 0), f = C x * X ^ k + C y * X ^ m + C z * X ^ n

pp: case refine_2
R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ (∃ k m n,
      ∃ (_ : k < m) (_ : m < n),
        ∃ x y z, ∃ (_ : x ≠ 0) (_ : y ≠ 0) (_ : z ≠ 0), f = C x * X ^ k + C y * X ^ m + C z * X ^ n) →
    #f.support = 3

Tactic:
· obtain ⟨k, x, hk, hx, rfl⟩ := card_support_eq.mp h
    refine
      ⟨k 0, k 1, k 2, hk Nat.zero_lt_one, hk (Nat.lt_succ_self 1), x 0, x 1, x 2, hx 0, hx 1, hx 2,
        ?_⟩
    rw [Fin.sum_univ_castSucc, Fin.sum_univ_castSucc, Fin.sum_univ_one]
    rfl

Goal state after:
case refine_2
R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ (∃ k m n,
      ∃ (_ : k < m) (_ : m < n),
        ∃ x y z, ∃ (_ : x ≠ 0) (_ : y ≠ 0) (_ : z ≠ 0), f = C x * X ^ k + C y * X ^ m + C z * X ^ n) →
    #f.support = 3
Module: Mathlib.RingTheory.Adjoin.Tower

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁶ : CommSemiring C
inst✝⁵ : CommSemiring D
inst✝⁴ : CommSemiring E
inst✝³ : Algebra C D
inst✝² : Algebra C E
inst✝¹ : Algebra D E
inst✝ : IsScalarTower C D E
S : Set E
this : Set.range ⇑(algebraMap D E) = Set.range ⇑(algebraMap (↥(Subalgebra.map (IsScalarTower.toAlgHom C D E) ⊤)) E)
⊢ Subalgebra.restrictScalars C (adjoin D S) =
    Subalgebra.restrictScalars C (adjoin (↥(Subalgebra.map (IsScalarTower.toAlgHom C D E) ⊤)) S)

Tactic:
ext x
    change x ∈ Subsemiring.closure (_ ∪ S) ↔ x ∈ Subsemiring.closure (_ ∪ S)
    rw [this]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
s : Set R[X]
s_fin : s.Finite
⊢ ∃ n, Submodule.span R s ≤ degreeLE R ↑n

Tactic:
by_cases s_emp : s.Nonempty

Goal state after:
case pos
R : Type u
inst✝ : Semiring R
s : Set R[X]
s_fin : s.Finite
s_emp : s.Nonempty
⊢ ∃ n, Submodule.span R s ≤ degreeLE R ↑n

case neg
R : Type u
inst✝ : Semiring R
s : Set R[X]
s_fin : s.Finite
s_emp : ¬s.Nonempty
⊢ ∃ n, Submodule.span R s ≤ degreeLE R ↑n
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Ring R
i : ℕ
⊢ (if i = 0 then 1 else 0) = ↑(if i = 0 then 1 else 0)

Tactic:
split_ifs <;> rfl

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
S' : Subalgebra R S
ι : Type u_3
ι' : Finset ι
s l : ι → S
e : ∑ i ∈ ι', l i * s i = 1
hs : ∀ (i : ι), s i ∈ S'
hl : ∀ (i : ι), l i ∈ S'
x : S
n : ι → ℕ
hn : ∀ (i : ι), s i ^ n i • x ∈ S'
s' : ι → ↥S' := fun x ↦ ⟨s x, ⋯⟩
l' : ι → ↥S' := fun x ↦ ⟨l x, ⋯⟩
e' : ∑ i ∈ ι', l' i * s' i = 1
this : Ideal.span (s' '' ↑ι') = ⊤
N : ℕ := ι'.sup n
hN : Ideal.span ((fun x ↦ x ^ N) '' s' '' ↑ι') = ⊤
i : ι
hi : i ∈ ↑ι'
⊢ s' i ^ (N - n i) • s' i ^ n i • x ∈ toSubmodule (ofId (↥S') S).range

Tactic:
refine Submodule.smul_mem _ (⟨_, pow_mem (hs i) _⟩ : S') ?_

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
S' : Subalgebra R S
ι : Type u_3
ι' : Finset ι
s l : ι → S
e : ∑ i ∈ ι', l i * s i = 1
hs : ∀ (i : ι), s i ∈ S'
hl : ∀ (i : ι), l i ∈ S'
x : S
n : ι → ℕ
hn : ∀ (i : ι), s i ^ n i • x ∈ S'
s' : ι → ↥S' := fun x ↦ ⟨s x, ⋯⟩
l' : ι → ↥S' := fun x ↦ ⟨l x, ⋯⟩
e' : ∑ i ∈ ι', l' i * s' i = 1
this : Ideal.span (s' '' ↑ι') = ⊤
N : ℕ := ι'.sup n
hN : Ideal.span ((fun x ↦ x ^ N) '' s' '' ↑ι') = ⊤
i : ι
hi : i ∈ ↑ι'
⊢ s' i ^ n i • x ∈ toSubmodule (ofId (↥S') S).range
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹ : AddMonoid M
inst✝ : CommRing R
h : AddMonoid.FG M
⊢ FiniteType R R[M]

Tactic:
obtain ⟨S, hS⟩ := h.fg_top
  exact .of_surjective
      (FreeAlgebra.lift R fun s : (S : Set M) => of' R M ↑s)
      (freeAlgebra_lift_of_surjective_of_closure hS)

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

Goal state before:
pp: n a b : ℤ
h : a ≡ b [ZMOD n]
⊢ a ≡ 0 [ZMOD n] ↔ b ≡ 0 [ZMOD n]

Tactic:
exact ⟨fun ha ↦ h.symm.trans ha, h.trans⟩

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

Goal state before:
pp: case refine_1
R : Type u_1
S : Type u_2
A : Type u_3
inst✝³ : Field R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
s : S
h1 : 1 ∉ s
algHom : Unitization R ↥s →ₐ[R] ↥(Algebra.adjoin R ↑s) := (unitization s).codRestrict (Algebra.adjoin R ↑s) ⋯
⊢ Function.Injective ⇑algHom

Tactic:
have := AlgHomClass.unitization_injective s h1
        ((Subalgebra.val _).comp algHom) fun _ ↦ by simp [algHom]
      rw [AlgHom.coe_comp] at this
      exact this.of_comp

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

Goal state before:
pp: case cons
α : Type u_1
t : α
ts : List α
r : List (List α)
l : List α
L : List (List α)
ih :
  foldr (fun y r ↦ (permutationsAux2 t ts r y id).snd) r L =
    flatMap (fun y ↦ (permutationsAux2 t ts [] y id).snd) L ++ r
⊢ (permutationsAux2 t ts (flatMap (fun y ↦ (permutationsAux2 t ts [] y id).snd) L ++ r) l id).snd =
    (permutationsAux2 t ts [] l id).snd ++ (flatMap (fun y ↦ (permutationsAux2 t ts [] y id).snd) L ++ r)

Tactic:
permutationsAux2_append

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

Goal state before:
pp: case succ.refine_2.e_b
α : Type u_1
n : ℕ
IH : ∀ (ts : List α), ts.length < n → ts.permutations ~ ts.permutations'
ts✝ : List α
h✝ : ts✝.length < n + 1
ts : List α
t : α
x✝¹ : ts.length < n + 1 → ts.permutations ~ ts.permutations'
h : ts.length < n
IH₂ : ts.reverse.permutations ~ ts.permutations'
x✝ : List α
⊢ (permutationsAux2 t [] [] x✝ id).snd ++ [x✝ ++ [t]] = (permutationsAux2 t [] [x✝ ++ [t]] x✝ id).snd

Tactic:
permutationsAux2_append

Goal state after:
case succ.refine_2.e_b
α : Type u_1
n : ℕ
IH : ∀ (ts : List α), ts.length < n → ts.permutations ~ ts.permutations'
ts✝ : List α
h✝ : ts✝.length < n + 1
ts : List α
t : α
x✝¹ : ts.length < n + 1 → ts.permutations ~ ts.permutations'
h : ts.length < n
IH₂ : ts.reverse.permutations ~ ts.permutations'
x✝ : List α
⊢ (permutationsAux2 t [] [x✝ ++ [t]] x✝ id).snd = (permutationsAux2 t [] [x✝ ++ [t]] x✝ id).snd
Module: Mathlib.GroupTheory.GroupAction.Basic

Goal state before:
pp: case h
G : Type u_1
α : Type u_2
β : Type u_3
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : MulAction G β
a : α
g h : G
⊢ ↑((h * g⁻¹) • ⟨(fun m ↦ m • a) g, ⋯⟩) = ↑⟨(fun m ↦ m • a) h, ⋯⟩

Tactic:
simp [mul_smul]

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Basic

Goal state before:
pp: case h
G : Type u_1
α : Type u_2
β : Type u_3
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : MulAction G β
a✝ : α
g : G
yh : (fun m ↦ m • a✝) g ∈ orbitRel.Quotient.orbit (Quotient.mk'' a✝)
h : G
zh : (fun m ↦ m • a✝) h ∈ orbitRel.Quotient.orbit (Quotient.mk'' a✝)
⊢ ↑((h * g⁻¹) • ⟨(fun m ↦ m • a✝) g, yh⟩) = ↑⟨(fun m ↦ m • a✝) h, zh⟩

Tactic:
simp [mul_smul]

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
l m : List α
a : α
_H : ∀ (hl : m ≠ []), Chain r ↑m ↔ IsChain r (m.getLast hl :: m)
hl✝ : m ++ [a] ≠ []
⊢ Chain r ↑(m ++ [a]) ↔ IsChain r ((m ++ [a]).getLast hl✝ :: (m ++ [a]))

Tactic:
← coe_cons_eq_coe_append,

Goal state after:
α : Type u_1
r : α → α → Prop
l m : List α
a : α
_H : ∀ (hl : m ≠ []), Chain r ↑m ↔ IsChain r (m.getLast hl :: m)
hl✝ : m ++ [a] ≠ []
⊢ Chain r ↑(a :: m) ↔ IsChain r ((m ++ [a]).getLast hl✝ :: (m ++ [a]))