mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.MvPolynomial.Variables

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
hp : ∀ i ∈ p.vars, g i = 0
h0 : constantCoeff p = 0
d : σ →₀ ℕ
hd : d ∈ p.support
⊢ d.support.Nonempty

Tactic:
constantCoeff_eq,

Goal state after:
R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ i ∈ p.vars, g i = 0
h0 : coeff 0 p = 0
d : σ →₀ ℕ
hd : d ∈ p.support
⊢ d.support.Nonempty
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial σ R
f : σ → τ
h : Injective f
i : σ
⊢ degreeOf (f i) ((rename f) p) = degreeOf i p

Tactic:
classical
  simp only [degreeOf, degrees_rename_of_injective h, Multiset.count_map_eq_count' f p.degrees h]

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

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
hp : ∀ i ∈ p.vars, g i = 0
h0 : constantCoeff p = 0
d : σ →₀ ℕ
hd : d ∈ p.support
⊢ d.support.Nonempty

Tactic:
rw [constantCoeff_eq, coeff, ← Finsupp.notMem_support_iff] at h0

Goal state after:
R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ i ∈ p.vars, g i = 0
h0 : 0 ∉ p.coeff.support
d : σ →₀ ℕ
hd : d ∈ p.support
⊢ d.support.Nonempty
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
⊢ totalDegree 0 = 0

Tactic:
by
  rw [← C_0]; exact totalDegree_C (0 : R)

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

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
hp : ∀ i ∈ p.vars, g i = 0
h0 : ¬constantCoeff p = 0
d : σ →₀ ℕ
hd : d ∈ p.support
hd0 : d ≠ 0
⊢ d.support.Nonempty

Tactic:
constantCoeff_eq,

Goal state after:
R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ i ∈ p.vars, g i = 0
h0 : ¬coeff 0 p = 0
d : σ →₀ ℕ
hd : d ∈ p.support
hd0 : d ≠ 0
⊢ d.support.Nonempty
Module: Mathlib.Algebra.MvPolynomial.Variables

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
hp : ∀ i ∈ p.vars, g i = 0
h0 : ¬constantCoeff p = 0
d : σ →₀ ℕ
hd : d ∈ p.support
hd0 : d ≠ 0
⊢ d.support.Nonempty

Tactic:
rw [constantCoeff_eq, coeff, ← Finsupp.notMem_support_iff] at h0

Goal state after:
R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ i ∈ p.vars, g i = 0
h0 : ¬0 ∉ p.coeff.support
d : σ →₀ ℕ
hd : d ∈ p.support
hd0 : d ≠ 0
⊢ d.support.Nonempty
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: case monomial
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Unique σ
n : ℕ
d : σ →₀ ℕ
r : R
⊢ ((Polynomial.monomial ((Finsupp.single default (d default)) default)) r).coeff n =
    coeff (Finsupp.single default n) ((monomial (Finsupp.single default (d default))) r)

Tactic:
simp [Polynomial.coeff_monomial, MvPolynomial.coeff_monomial]

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

Goal state before:
pp: R : Type u
S₁ : Type v
σ : Type u_1
inst✝³ : CommSemiring R
inst✝² : IsEmpty σ
inst✝¹ : CommSemiring S₁
inst✝ : Algebra R S₁
f : σ → S₁
⊢ aeval f = (Algebra.ofId R S₁).comp ↑(isEmptyAlgEquiv R σ)

Tactic:
ext i

Goal state after:
R : Type u
S₁ : Type v
σ : Type u_1
inst✝³ : CommSemiring R
inst✝² : IsEmpty σ
inst✝¹ : CommSemiring S₁
inst✝ : Algebra R S₁
f : σ → S₁
i : σ
⊢ (aeval f) (X i) = ((Algebra.ofId R S₁).comp ↑(isEmptyAlgEquiv R σ)) (X i)
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: case inl
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
key : p = C (p.coeff 0)
⊢ p = 0 ∨ eval (q.coeff 0) p = 0 ∧ q = C (q.coeff 0)

Tactic:
rw [key, C_comp] at h
    exact Or.inl (key.trans h)

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial (Option σ) R
⊢ ((optionEquivLeft R σ) p).support = Finset.image (fun m ↦ m none) p.support

Tactic:
ext i

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial (Option σ) R
i : ℕ
⊢ i ∈ ((optionEquivLeft R σ) p).support ↔ i ∈ Finset.image (fun m ↦ m none) p.support
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: R : Type u_2
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
⊢ (p * q).reverse.leadingCoeff = p.trailingCoeff * q.trailingCoeff

Tactic:
reverse_mul_of_domain,

Goal state after:
R : Type u_2
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
⊢ (p.reverse * q.reverse).leadingCoeff = p.trailingCoeff * q.trailingCoeff
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
⊢ ((finSuccEquiv R n) f).support = Finset.image (fun m ↦ m 0) f.support

Tactic:
ext i

Goal state after:
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
⊢ i ∈ ((finSuccEquiv R n) f).support ↔ i ∈ Finset.image (fun m ↦ m 0) f.support
Module: Mathlib.Algebra.Polynomial.Monic

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

Tactic:
by
  revert ht
  refine t.induction_on ?_ ?_; · simp
  intro a t ih ht
  rw [Multiset.map_cons, Multiset.prod_cons]
  exact (ht _ (Multiset.mem_cons_self _ _)).mul (ih fun _ hi => ht _ (Multiset.mem_cons_of_mem hi))

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

Goal state before:
pp: case e'_2.e'_4
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
a : σ
p : MvPolynomial σ R
⊢ none = (Equiv.optionSubtypeNe a).symm a

Tactic:
Equiv.optionSubtypeNe_symm_apply,

Goal state after:
case e'_2.e'_4
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
a : σ
p : MvPolynomial σ R
⊢ none = if h : a = a then none else Option.some ⟨a, h⟩
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: case refine_3
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : p.Monic
hp1 : p ≠ 1
h : ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f = 1 ∨ g = 1
f g : R[X]
hfg : p = f * g
⊢ g * C f.leadingCoeff * (f * C g.leadingCoeff) = p

Tactic:
· rw [mul_mul_mul_comm, ← C_mul, ← leadingCoeff_mul, ← hfg, hp.leadingCoeff, C_1, mul_one,
      mul_comm, ← hfg]

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

Goal state before:
pp: case h
R : Type u
inst✝ : CommRing R
t : Multiset R
⊢ ∀ i ∈ t, (X - C i).Monic

Tactic:
intros
    apply monic_X_sub_C

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

Goal state before:
pp: case succ.refine_3
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
⊢ f =
    f.eraseLead +
      C (Function.extend Fin.castSucc x (fun x ↦ f.leadingCoeff) (Fin.last n)) *
        X ^ Function.extend Fin.castSucc k (fun x ↦ f.natDegree) (Fin.last n)

Tactic:
Function.extend_apply',

Goal state after:
case succ.refine_3
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
⊢ f = f.eraseLead + C f.leadingCoeff * X ^ Function.extend Fin.castSucc k (fun x ↦ f.natDegree) (Fin.last n)

case succ.refine_3.hb
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
⊢ ¬∃ a, a.castSucc = Fin.last n
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
q : R[X]
hp : h.unit⁻¹ • (p * q) = 0
n✝ : ℕ
x : ℕ × ℕ
x✝ : x ∈ antidiagonal n✝
⊢ ↑h.unit⁻¹ * (p.coeff x.1 * q.coeff x.2) = ↑h.unit⁻¹ * p.coeff x.1 * q.coeff x.2

Tactic:
rw [← mul_assoc]

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

Goal state before:
pp: case succ.refine_3
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
⊢ f = f.eraseLead + C f.leadingCoeff * X ^ Function.extend Fin.castSucc k (fun x ↦ f.natDegree) (Fin.last n)

pp: case succ.refine_3.hb
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
⊢ ¬∃ a, a.castSucc = Fin.last n

Tactic:
Function.extend_apply',

Goal state after:
case succ.refine_3
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
⊢ f = f.eraseLead + C f.leadingCoeff * X ^ f.natDegree

case succ.refine_3.hb
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
⊢ ¬∃ a, a.castSucc = Fin.last n

case succ.refine_3.hb
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
⊢ ¬∃ a, a.castSucc = Fin.last n
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
S : Type u_1
inst✝ : Semiring R
n : ℕ
f : Fin n → R
⊢ (fun p n_1 ↦ (↑p).coeff ↑n_1) ((fun f ↦ ⟨∑ i, (monomial ↑i) (f i), ⋯⟩) f) = f

Tactic:
ext i

Goal state after:
R : Type u
S : Type u_1
inst✝ : Semiring R
n : ℕ
f : Fin n → R
i : Fin n
⊢ (fun p n_1 ↦ (↑p).coeff ↑n_1) ((fun f ↦ ⟨∑ i, (monomial ↑i) (f i), ⋯⟩) f) i = f i
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
s : Set R[X]
s_fin : s.Finite
n : ℕ
h✝ : Submodule.span R s ≤ degreeLE R ↑n
⊢ Submodule.span R s ≤ degreeLT R (n + 1)

Tactic:
degreeLT_succ_eq_degreeLE

Goal state after:
R : Type u
inst✝ : Semiring R
s : Set R[X]
s_fin : s.Finite
n : ℕ
h✝ : Submodule.span R s ≤ degreeLE R ↑n
⊢ Submodule.span R s ≤ degreeLE R ↑n
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
⊢ (∑ i ∈ range n, X ^ i).comp (X + 1) = ∑ i ∈ range n, ↑(n.choose (i + 1)) * X ^ i

Tactic:
ext i

Goal state after:
R : Type u
inst✝ : Semiring R
n i : ℕ
⊢ ((∑ i ∈ range n, X ^ i).comp (X + 1)).coeff i = (∑ i ∈ range n, ↑(n.choose (i + 1)) * X ^ i).coeff i
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Ring R
p : R[X]
⊢ p.restriction.support = p.support

Tactic:
ext i

Goal state after:
R : Type u
inst✝ : Ring R
p : R[X]
i : ℕ
⊢ i ∈ p.restriction.support ↔ i ∈ p.support
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
n : ℕ
⊢ (map (algebraMap (↥(Subring.closure ↑p.coeffs)) R) p.restriction).coeff n = p.coeff n

Tactic:
rw [coeff_map, Algebra.algebraMap_ofSubsemiring_apply, coeff_restriction]

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

Goal state before:
pp: case mpr
R : Type u
inst✝ : CommSemiring R
I : Ideal R
f : R[X]
⊢ (∀ (n : ℕ), f.coeff n ∈ I) → f ∈ map C I

Tactic:
· intro hf
    rw [← sum_monomial_eq f]
    refine (I.map C : Ideal R[X]).sum_mem fun n _ => ?_
    simp only [← C_mul_X_pow_eq_monomial]
    rw [mul_comm]
    exact (I.map C : Ideal R[X]).mul_mem_left _ (mem_map_of_mem _ (hf n))

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

Goal state before:
pp: case mp
R : Type u
inst✝ : CommRing R
P : Ideal R
H : (map C P).IsPrime
this : (comap C (map C P)).IsPrime
x : R
⊢ x ∈ P → ∀ (n : ℕ), (C x).coeff n ∈ P

Tactic:
rintro h (- | n)
      · rwa [coeff_C_zero]
      · simp only [coeff_C_of_ne_zero (Nat.succ_ne_zero _), Submodule.zero_mem]

Goal state after:
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case intro
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
val✝ : Fintype ι
⊢ FiniteType R (MvPolynomial ι S)

Tactic:
refine .trans ‹_› ⟨Finset.univ.image MvPolynomial.X, ?_⟩

Goal state after:
case intro
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
val✝ : Fintype ι
⊢ adjoin S ↑(Finset.image MvPolynomial.X Finset.univ) = ⊤
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : CommRing R
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R := ⋯
hm : M ∈ Set.range I.leadingCoeffNth
N : ℕ
HN : I.leadingCoeffNth N = M
s : Finset R[X]
hs : Submodule.span R ↑s = I.degreeLE ↑N
hm2 : ∀ (k : ℕ), I.leadingCoeffNth k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ I.degreeLE ↑N → x ∈ Ideal.span ↑s
this : Submodule.span R[X] ↑s = Ideal.span ↑s
k : ℕ
ih : ∀ m < k, ∀ ⦃p : R[X]⦄, p ∈ I → p.natDegree = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : p.natDegree = k
h✝ : N < k
hp0 : p ≠ 0
h : 0 = 1
⊢ p = 0

Tactic:
ext i

Goal state after:
R : Type u
inst✝ : CommRing R
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R := ⋯.min (Set.range I.leadingCoeffNth) ⋯
hm : M ∈ Set.range I.leadingCoeffNth
N : ℕ
HN : I.leadingCoeffNth N = M
s : Finset R[X]
hs : Submodule.span R ↑s = I.degreeLE ↑N
hm2 : ∀ (k : ℕ), I.leadingCoeffNth k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ I.degreeLE ↑N → x ∈ Ideal.span ↑s
this : Submodule.span R[X] ↑s = Ideal.span ↑s
k : ℕ
ih : ∀ m < k, ∀ ⦃p : R[X]⦄, p ∈ I → p.natDegree = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : p.natDegree = k
h✝ : N < k
hp0 : p ≠ 0
h : 0 = 1
i : ℕ
⊢ p.coeff i = coeff 0 i
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case refine_3.mem
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✝ : ↥M'
x : M
j : Fin k
⊢ mj j ∈ ((↑↥A f).domRestrict N').range

Tactic:
exact ⟨⟨nj j, subset_span (by simp)⟩, hnj j⟩

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

Goal state before:
pp: case refine_1
R : Type u_1
A : Type u_2
C : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : Module R A
inst✝³ : SMulCommClass R A A
inst✝² : IsScalarTower R A A
inst✝¹ : Semiring C
inst✝ : Algebra R C
f : A →ₙₐ[R] C
S : Subalgebra R C
h : (lift f).range ≤ S
x : A
⊢ ↑f x ∈ S.toNonUnitalSubalgebra

Tactic:
exact @h (f x) ⟨x, by simp⟩

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

Goal state before:
pp: case refine_2
R : Type u_1
A : Type u_2
C : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : Module R A
inst✝³ : SMulCommClass R A A
inst✝² : IsScalarTower R A A
inst✝¹ : Semiring C
inst✝ : Algebra R C
f : A →ₙₐ[R] C
S : Subalgebra R C
h : NonUnitalAlgHom.range f ≤ S.toNonUnitalSubalgebra
x : Unitization R A
⊢ (lift f).toRingHom x ∈ S

Tactic:
induction x with

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

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : SetLike S A
hSA : NonUnitalSubsemiringClass S A
hSRA : SMulMemClass S R A
s : S
⊢ (unitization s).range = Algebra.adjoin R ↑s

Tactic:
rw [unitization, Unitization.lift_range]
  simp

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

Goal state before:
pp: F : Type u_1
R : Type u_2
S : Type u_3
A : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : Ring A
inst✝³ : Algebra R A
inst✝² : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
s : S
h : ∀ (r : R), r ≠ 0 → (algebraMap R A) r ∉ s
inst✝¹ : FunLike F (Unitization R ↥s) A
inst✝ : AlgHomClass F R (Unitization R ↥s) A
f : F
hf : ∀ (x : ↥s), f ↑x = ↑x
x : Unitization R ↥s
hx : f x = 0
⊢ x = 0

Tactic:
induction x with

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

Goal state before:
pp: 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) ⋯
x✝ : ↥s
⊢ ((Algebra.adjoin R ↑s).val.comp algHom) ↑x✝ = ↑x✝

Tactic:
by simp [algHom]

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

Goal state before:
pp: case h
R : Type u_2
inst✝¹ : CommRing R
ι : Type u_3
inst✝ : Finite ι
I : ι → Ideal R
hI : Pairwise (IsCoprime on I)
val✝ : Fintype ι
g : (i : ι) → R ⧸ I i
f : ι → R
hf : ∀ (i : ι), (Quotient.mk (I i)) (f i) = g i
e : ι → R
he : ∀ (i : ι), (Quotient.mk (I i)) (e i) = 1 ∧ ∀ (j : ι), j ≠ i → (Quotient.mk (I j)) (e i) = 0
⊢ (quotientInfToPiQuotient I) ((Quotient.mk (⨅ i, I i)) (∑ i, f i * e i)) = g

Tactic:
ext i

Goal state after:
case h
R : Type u_2
inst✝¹ : CommRing R
ι : Type u_3
inst✝ : Finite ι
I : ι → Ideal R
hI : Pairwise (IsCoprime on I)
val✝ : Fintype ι
g : (i : ι) → R ⧸ I i
f : ι → R
hf : ∀ (i : ι), (Quotient.mk (I i)) (f i) = g i
e : ι → R
he : ∀ (i : ι), (Quotient.mk (I i)) (e i) = 1 ∧ ∀ (j : ι), j ≠ i → (Quotient.mk (I j)) (e i) = 0
i : ι
⊢ (quotientInfToPiQuotient I) ((Quotient.mk (⨅ i, I i)) (∑ i, f i * e i)) i = g i
Module: Mathlib.Algebra.Algebra.Subalgebra.Unitization

Goal state before:
pp: case refine_1
R : Type u_1
A : Type u_2
C : Type u_3
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : NonUnitalSemiring A
inst✝⁹ : StarRing R
inst✝⁸ : StarRing A
inst✝⁷ : Module R A
inst✝⁶ : SMulCommClass R A A
inst✝⁵ : IsScalarTower R A A
inst✝⁴ : StarModule R A
inst✝³ : Semiring C
inst✝² : StarRing C
inst✝¹ : Algebra R C
inst✝ : StarModule R C
f : A →⋆ₙₐ[R] C
S : StarSubalgebra R C
h : (starLift f).range ≤ S
x : A
⊢ ↑(NonUnitalAlgHomClass.toNonUnitalAlgHom f) x ∈ S.toNonUnitalStarSubalgebra

Tactic:
exact @h (f x) ⟨x, by simp⟩

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

Goal state before:
pp: case refine_2
R : Type u_1
A : Type u_2
C : Type u_3
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : NonUnitalSemiring A
inst✝⁹ : StarRing R
inst✝⁸ : StarRing A
inst✝⁷ : Module R A
inst✝⁶ : SMulCommClass R A A
inst✝⁵ : IsScalarTower R A A
inst✝⁴ : StarModule R A
inst✝³ : Semiring C
inst✝² : StarRing C
inst✝¹ : Algebra R C
inst✝ : StarModule R C
f : A →⋆ₙₐ[R] C
S : StarSubalgebra R C
h : NonUnitalStarAlgHom.range f ≤ S.toNonUnitalStarSubalgebra
x : Unitization R A
⊢ (↑(starLift f)).toRingHom x ∈ S

Tactic:
induction x with

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

Goal state before:
pp: α : Type u_1
l : Finset α
h_nodup : (↑l.toList).Nodup
⊢ l.val.lists.Nodup

Tactic:
Multiset.coe_nodup

Goal state after:
α : Type u_1
l : Finset α
h_nodup : l.toList.Nodup
⊢ l.val.lists.Nodup
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: α : Type u_1
f : α → α
x : α
m : ℕ
hm : IsPeriodicPt f m x
n : ℕ
⊢ IsPeriodicPt f (n * m) x

Tactic:
simp only [mul_comm n, hm.mul_const n]

Goal state after:
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: α : Type u_1
f : α → α
x : α
n : ℕ
hf : IsPeriodicPt f n x
m : ℕ
⊢ IsFixedPt f^[n]^[m] x

Tactic:
exact hf.isFixedPt.iterate m

Goal state after:
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: case a
α : Type u_1
f : α → α
x : α
n : ℕ
h : 0 < (minimalPeriod f x).gcd n
⊢ minimalPeriod f x / (minimalPeriod f x).gcd n * (minimalPeriod f x).gcd n ∣
    minimalPeriod f^[n] x * (n / (minimalPeriod f x).gcd n) * (minimalPeriod f x).gcd n

Tactic:
Nat.div_mul_cancel (gcd_dvd_left _ _),

Goal state after:
case a
α : Type u_1
f : α → α
x : α
n : ℕ
h : 0 < (minimalPeriod f x).gcd n
⊢ minimalPeriod f x ∣ minimalPeriod f^[n] x * (n / (minimalPeriod f x).gcd n) * (minimalPeriod f x).gcd n
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
xs : List α
x d : α
h : x ∉ xs
⊢ (xs ++ [x]).nextOr x d = d

Tactic:
induction xs with
  | nil => simp
  | cons z zs IH =>
    obtain ⟨hz, hzs⟩ := not_or.mp (mt mem_cons.2 h)
    rw [cons_append, nextOr_cons_of_ne _ _ _ _ hz, IH hzs]

Goal state after:
Module: Mathlib.GroupTheory.Coset.Card

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s : Subgroup α
⊢ Nat.card (α ⧸ s) ∣ Nat.card α

Tactic:
simp [card_eq_card_quotient_mul_card_subgroup s, @dvd_mul_right ℕ]

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

Goal state before:
pp: case cons.cons
α : Type u_1
inst✝ : DecidableEq α
x hd' : α
tl : List α
hl : ∀ (hd : α) (h : x ∈ hd :: tl), (hd :: tl).prev x h ∈ hd :: tl
hd : α
h : x ∈ hd :: hd' :: tl
⊢ (hd :: hd' :: tl).prev x h ∈ hd :: hd' :: tl

Tactic:
| cons hd' tl hl =>

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
n : ℕ
hd : α
tl : List α
h : (hd :: tl).Nodup
hn✝ : n < (hd :: tl).length
hn : n < tl.length + 1
hx : (hd :: tl)[n] ∈ hd :: tl
⊢ (n + 1 + tl.length) % (tl.length + 1) = n

Tactic:
rw [add_assoc, add_comm 1, Nat.add_mod_right, Nat.mod_eq_of_lt hn]

Goal state after:
Module: Mathlib.Data.Nat.PrimeFin

Goal state before:
pp: n : ℕ
⊢ n.primeFactors = ∅ ↔ n ≤ 1

Tactic:
primeFactors_eq_empty,

Goal state after:
n : ℕ
⊢ n = 0 ∨ n = 1 ↔ n ≤ 1