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

Goal state before:
pp: R : Type u_1
A : Type u_3
B : Type u_5
inst✝³ : Semiring R
inst✝² : LinearOrder B
inst✝¹ : OrderBot B
p : R[A]
D : A → B
inst✝ : AddZeroClass A
hD : Function.Injective D
hp : p ≠ 0
a : A
ha : a ∈ p.coeff.support
he : supDegree D p = D a
⊢ Function.invFun D (D a) ∈ p.coeff.support

Tactic:
Function.leftInverse_invFun hD

Goal state after:
R : Type u_1
A : Type u_3
B : Type u_5
inst✝³ : Semiring R
inst✝² : LinearOrder B
inst✝¹ : OrderBot B
p : R[A]
D : A → B
inst✝ : AddZeroClass A
hD : Function.Injective D
hp : p ≠ 0
a : A
ha : a ∈ p.coeff.support
he : supDegree D p = D a
⊢ a ∈ p.coeff.support
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
h : p.leadingCoeff ^ n ≠ 0
this : DecidableEq R := Classical.decEq R
hp0 : ¬p = 0
hpn0 : p ^ n = 0
h1 : p.leadingCoeff ^ n ≠ 0
⊢ False

Tactic:
rw [← leadingCoeff_pow' h1, hpn0, leadingCoeff_zero] at h

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
h : 0 ≠ 0
this : DecidableEq R := Classical.decEq R
hp0 : ¬p = 0
hpn0 : p ^ n = 0
h1 : p.leadingCoeff ^ n ≠ 0
⊢ False
Module: Mathlib.Algebra.Polynomial.Degree.SmallDegree

Goal state before:
pp: R : Type u
a b c d : R
inst✝ : Semiring R
⊢ (C a * X ^ 3 + C b * X ^ 2 + C c * X + C d).degree ≤ 3

Tactic:
simpa only [add_assoc] using!
    degree_add_le_of_degree_le (degree_C_mul_X_pow_le 3 a)
      (le_trans degree_quadratic_le <| WithBot.coe_le_coe.mpr <| Nat.le_succ 2)

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
hi : (p ^ i).coeff (i * p.natDegree) = p.leadingCoeff ^ i
hp1 : p.leadingCoeff ^ i = 0
hp2 : ¬p ^ i = 0
h1 : (p ^ i).natDegree < i * p.natDegree
⊢ (p ^ i).natDegree + p.natDegree < i * p.natDegree + p.natDegree

Tactic:
by gcongr

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: case inr.inr
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder B
inst✝⁴ : OrderBot B
p q : R[A]
D : A → B
inst✝³ : AddZeroClass A
inst✝² : Add B
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hp✝ : p ≠ 0
hq✝ : q ≠ 0
ap : A
hp : supDegree D p = D ap
aq : A
hq : supDegree D q = D aq
⊢ (p * q).coeff (ap + aq) = p.coeff ap * q.coeff aq

Tactic:
exact coeff_add_of_supDegree_le hadd hD hp.le hq.le

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

Goal state before:
pp: case mp
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : Zero α
inst✝¹ : LE α
inst✝ : Std.Refl fun x1 x2 ↦ x1 ≤ x2
f : ι ↪ κ
g₁ g₂ : ι →₀ α
h' : ∀ (i : κ), (embDomain f g₁) i ≤ (embDomain f g₂) i
⊢ g₁ ≤ g₂

Tactic:
x

Goal state after:
case mp
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : Zero α
inst✝¹ : LE α
inst✝ : Std.Refl fun x1 x2 ↦ x1 ≤ x2
f : ι ↪ κ
g₁ g₂ : ι →₀ α
h' : ∀ (i : κ), (embDomain f g₁) i ≤ (embDomain f g₂) i
x : ι
⊢ g₁ x ≤ g₂ x
Module: Mathlib.Data.Finsupp.Order

Goal state before:
pp: ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
f : ι → κ
h : Function.Injective f
f1 f2 : ι →₀ α
y : κ
⊢ (mapDomain f (f1 - f2)) y = (mapDomain f f1 - mapDomain f f2) y

Tactic:
by_cases! hy : y ∉ Set.range f

Goal state after:
case pos
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
f : ι → κ
h : Function.Injective f
f1 f2 : ι →₀ α
y : κ
hy : y ∉ Set.range f
⊢ (mapDomain f (f1 - f2)) y = (mapDomain f f1 - mapDomain f f2) y

case neg
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
f : ι → κ
h : Function.Injective f
f1 f2 : ι →₀ α
y : κ
hy : y ∈ Set.range f
⊢ (mapDomain f (f1 - f2)) y = (mapDomain f f1 - mapDomain f f2) y
Module: Mathlib.Algebra.Polynomial.AlgebraMap

Goal state before:
pp: case base
R : Type u
inst✝ : CommSemiring R
P : R[X]
h : ∀ (r : R), r • P = 0 → r = 0
Q : R[X]
hQ : P * Q = 0
⊢ ∃ n, ∀ m > n, P.coeff m • Q = 0

Tactic:
use P.natDegree

Goal state after:
case h
R : Type u
inst✝ : CommSemiring R
P : R[X]
h : ∀ (r : R), r • P = 0 → r = 0
Q : R[X]
hQ : P * Q = 0
⊢ ∀ m > P.natDegree, P.coeff m • Q = 0
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: case single_add
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
motive : MvPolynomial σ R → Prop
C : ∀ (a : R), motive (MvPolynomial.C a)
mul_X : ∀ (p : MvPolynomial σ R) (n : σ), motive p → motive (p * X n)
s : σ →₀ ℕ
a : R
n : σ
⊢ ∀ (b : ℕ) (f : σ →₀ ℕ),
    n ∉ f.support → b ≠ 0 → motive ((monomial f) a) → motive ((monomial (Finsupp.single n b + f)) a)

Tactic:
e

Goal state after:
case single_add
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
motive : MvPolynomial σ R → Prop
C : ∀ (a : R), motive (MvPolynomial.C a)
mul_X : ∀ (p : MvPolynomial σ R) (n : σ), motive p → motive (p * X n)
s : σ →₀ ℕ
a : R
n : σ
e : ℕ
⊢ ∀ (f : σ →₀ ℕ), n ∉ f.support → e ≠ 0 → motive ((monomial f) a) → motive ((monomial (Finsupp.single n e + f)) a)
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
⊢ support 1 = {0}

Tactic:
by
  classical
  simp [show support (1 : MvPolynomial σ R) = if (1 : R) = 0 then ∅ else {0} from rfl]

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
m : σ →₀ ℕ
⊢ m ∈ p.support ↔ coeff m p ≠ 0

Tactic:
simp [support, coeff]

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
⊢ coeffs 1 ⊆ {1}

Tactic:
by
  classical
    rw [coeffs, Finset.image_subset_iff]
    simp_all [coeff_one]

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

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
hf : Injective f
p : MvPolynomial τ R
s : σ →₀ ℕ
⊢ coeff s ((killCompl hf) p) = coeff (Finsupp.mapDomain f s) p

Tactic:
apply p.induction_on' (P := fun p ↦ (p.killCompl hf).coeff s = p.coeff (s.mapDomain f))
  · intro u r
    rw [killCompl_monomial]
    split_ifs with h
    · simp [← (Finsupp.mapDomain_injective hf).eq_iff, u.mapDomain_comapDomain _ hf h]
    · simp? says simp only [coeff_zero, coeff_monomial, right_eq_ite_iff]
      intro rfl
      contrapose! h
      apply subset_trans <| SetLike.coe_subset_coe.mpr <| Finsupp.mapDomain_support
      simp
  · simp_intro ..

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

Goal state before:
pp: case pos
n : ℕ
M : Type u_1
inst✝ : Zero M
t : Fin (n + 1) →₀ M
a : Fin (n + 1)
c_a : a = 0
⊢ (cons (t 0) t.tail) a = t a

pp: case neg
n : ℕ
M : Type u_1
inst✝ : Zero M
t : Fin (n + 1) →₀ M
a : Fin (n + 1)
c_a : ¬a = 0
⊢ (cons (t 0) t.tail) a = t a

Tactic:
· rw [c_a, cons_zero]

Goal state after:
case neg
n : ℕ
M : Type u_1
inst✝ : Zero M
t : Fin (n + 1) →₀ M
a : Fin (n + 1)
c_a : ¬a = 0
⊢ (cons (t 0) t.tail) a = t a
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
a : R
⊢ (if a = 0 then ⊥ else sum 0 fun x e ↦ e) = 0

Tactic:
by rw [sum_zero_index, bot_eq_zero', ite_self]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
hp : p ≠ 0
⊢ p.trailingDegree = ↑n ↔ p.natTrailingDegree = n

Tactic:
by
  rw [trailingDegree_eq_natTrailingDegree hp, Nat.cast_inj]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ f.eraseLead + C f.leadingCoeff * X ^ f.natDegree = f

Tactic:
by
  rw [C_mul_X_pow_eq_monomial, eraseLead_add_monomial_natDegree_leadingCoeff]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
c : ℕ
fc : #f.support = c + 1
⊢ #f.eraseLead.support = c

Tactic:
card_support_eraseLead,

Goal state after:
R : Type u_1
inst✝ : Semiring R
f : R[X]
c : ℕ
fc : #f.support = c + 1
⊢ #f.support - 1 = c
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
⊢ ∀ b ∈ s, (f b).degree ≤ s.sup' hs (WithBot.some ∘ fun i ↦ (f i).natDegree)

Tactic:
intro b hb

Goal state after:
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
b : S
hb : b ∈ s
⊢ (f b).degree ≤ s.sup' hs (WithBot.some ∘ fun i ↦ (f i).natDegree)
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
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
⊢ ∀ b ∈ s, (WithBot.some ∘ fun i ↦ (f i).natDegree) b ≤ s.sup' hs fun i ↦ (f i).degree

Tactic:
intro b 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
b : S
hb : b ∈ s
⊢ (WithBot.some ∘ fun i ↦ (f i).natDegree) b ≤ s.sup' hs fun i ↦ (f i).degree
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ✝ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ✝ →₀ ℕ
inst✝¹ : CommSemiring R
σ : Type u_2
inst✝ : Unique σ
p✝ p q : R[X]
hp : eval₂ Polynomial.C (fun x ↦ Polynomial.X) (Polynomial.eval₂ C (X default) p) = p
hq : eval₂ Polynomial.C (fun x ↦ Polynomial.X) (Polynomial.eval₂ C (X default) q) = q
⊢ eval₂ Polynomial.C (fun x ↦ Polynomial.X) (Polynomial.eval₂ C (X default) (p + q)) = p + q

Tactic:
Polynomial.eval₂_add,

Goal state after:
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ✝ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ✝ →₀ ℕ
inst✝¹ : CommSemiring R
σ : Type u_2
inst✝ : Unique σ
p✝ p q : R[X]
hp : eval₂ Polynomial.C (fun x ↦ Polynomial.X) (Polynomial.eval₂ C (X default) p) = p
hq : eval₂ Polynomial.C (fun x ↦ Polynomial.X) (Polynomial.eval₂ C (X default) q) = q
⊢ eval₂ Polynomial.C (fun x ↦ Polynomial.X) (Polynomial.eval₂ C (X default) p + Polynomial.eval₂ C (X default) q) =
    p + q
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
⊢ ((uniqueAlgEquiv R σ) ((monomial d) r)).coeff n = coeff (Finsupp.single default n) ((monomial d) r)

Tactic:
rw [uniqueAlgEquiv_monomial, Finsupp.unique_single d]

Goal state after:
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)
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u_2
S₁ : Type u_3
S₂ : Type u_4
inst✝ : CommSemiring R
i : S₂
⊢ (commAlgEquiv R S₁ S₂) (C (X i)) = X i

Tactic:
simp [map, X, monomial]

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

Goal state before:
pp: case h_add
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
m : Option S₁ →₀ ℕ
r : R
⊢ ∀ (o : Option S₁) (m₁ m₂ : ℕ),
    (o.elim Polynomial.X fun s ↦ Polynomial.C (X s)) ^ (m₁ + m₂) =
      (o.elim Polynomial.X fun s ↦ Polynomial.C (X s)) ^ m₁ * (o.elim Polynomial.X fun s ↦ Polynomial.C (X s)) ^ m₂

Tactic:
· intros; rw [pow_add]

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

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : f = 0
⊢ f.natDegree = f.reverse.natDegree + f.natTrailingDegree

pp: case neg
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : ¬f = 0
⊢ f.natDegree = f.reverse.natDegree + f.natTrailingDegree

Tactic:
· rw [hf, reverse_zero, natDegree_zero, natTrailingDegree_zero]

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : ¬f = 0
⊢ f.natDegree = f.reverse.natDegree + f.natTrailingDegree
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
h : f ≠ 0
h₀ : ∀ {α : Type ?u.39} {β : Type ?u.41} (f : α → β), (fun x ↦ x) ∘ f = f
h₁ : ∀ {α : Type ?u.55} {β : Type ?u.57} (f : α → β), (f ∘ fun x ↦ x) = f
⊢ ((finSuccEquiv R n) f).degree = ↑(degreeOf 0 f)

Tactic:
have h' : ((finSuccEquiv R n f).support.sup fun x => x) = degreeOf 0 f := by
    rw [degreeOf_eq_sup, support_finSuccEquiv, Finset.sup_image, h₀]

Goal state after:
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
h : f ≠ 0
h₀ : ∀ {α β : Type} (f : α → β), (fun x ↦ x) ∘ f = f
h₁ : ∀ {α : Type ?u.55} {β : Type ?u.57} (f : α → β), (f ∘ fun x ↦ x) = f
h' : (((finSuccEquiv R n) f).support.sup fun x ↦ x) = degreeOf 0 f
⊢ ((finSuccEquiv R n) f).degree = ↑(degreeOf 0 f)
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: case refine_1
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
⊢ (f * g).leadingCoeff = 1

Tactic:
← hfg,

Goal state after:
case refine_1
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
⊢ p.leadingCoeff = 1
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:
rw [Equiv.optionSubtypeNe_symm_apply, dif_pos rfl]

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

Goal state before:
pp: case refine_2
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
⊢ (f * g).leadingCoeff = 1

Tactic:
← hfg,

Goal state after:
case refine_2
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
⊢ p.leadingCoeff = 1
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 * f * C (f * g).leadingCoeff = p

Tactic:
← hfg,

Goal state after:
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 * f * C p.leadingCoeff = p
Module: Mathlib.Algebra.Ring.GeomSum

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
f : ℕ → ℕ → R := fun m i ↦ (x + y) ^ i * y ^ (m - 1 - i)
n : ℕ
ih : (∑ i ∈ range n, f n i) * x + y ^ n = (x + y) ^ n
⊢ (x + y) ^ n * y ^ (1 + n - (1 + n)) = (x + y) ^ n

Tactic:
tsub_self,

Goal state after:
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
f : ℕ → ℕ → R := fun m i ↦ (x + y) ^ i * y ^ (m - 1 - i)
n : ℕ
ih : (∑ i ∈ range n, f n i) * x + y ^ n = (x + y) ^ n
⊢ (x + y) ^ n * y ^ 0 = (x + y) ^ n
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f g : R[X]
hf : f.Monic
hg : g.Monic
hp : (f * g).Monic
h : f.natDegree ≠ 0 ∧ g.natDegree ≠ 0
hl : f.natDegree ≤ g.natDegree
⊢ f.natDegree + f.natDegree ≤ f.natDegree + g.natDegree

Tactic:
by gcongr

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

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f g : R[X]
hf : f.Monic
hg : g.Monic
hp : (f * g).Monic
h : f.natDegree ≠ 0 ∧ g.natDegree ≠ 0
hl : g.natDegree ≤ f.natDegree
⊢ g.natDegree + g.natDegree ≤ f.natDegree + g.natDegree

Tactic:
by gcongr

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

Goal state before:
pp: R : Type u
S : Type v
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Nontrivial S
P : R[X]
hmo : P.Monic
f : R →+* S
⊢ (Polynomial.map f P).natDegree = P.natDegree

Tactic:
by
  refine le_antisymm natDegree_map_le (le_natDegree_of_ne_zero ?_)
  rw [coeff_map, Monic.coeff_natDegree hmo, map_one]
  exact one_ne_zero

Goal state after:
Module: Mathlib.Algebra.Ring.GeomSum

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

Tactic:
tsub_self,

Goal state after:
R : Type u_1
inst✝ : Ring R
x y : R
h : Commute x y
n : ℕ
⊢ x ^ n * y ^ 0 + ∑ i ∈ range n, x ^ i * y ^ (n - i) = x ^ n + ∑ i ∈ range n, y * (x ^ i * y ^ (n - 1 - i))
Module: Mathlib.RingTheory.Adjoin.Tower

Goal state before:
pp: A : Type w
B : Type u₁
C : Type u_1
inst✝⁶ : CommSemiring A
inst✝⁵ : CommSemiring B
inst✝⁴ : Semiring C
inst✝³ : Algebra A B
inst✝² : Algebra B C
inst✝¹ : Algebra A C
inst✝ : IsScalarTower A B C
x : Finset C
hx : Algebra.adjoin A ↑x = ⊤
y : Finset C
hy : span B ↑y = ⊤
f : C → C → B
h✝ : ∀ (x : C), Function.support (f x) ⊆ ↑y
hf : ∀ (x : C), ∑ a ∈ y, f x a • a = x
⊢ ∃ B₀, B₀.FG ∧ ⊤.FG

Tactic:
let s : Finset B := Finset.image₂ f (x ∪ y * y) y

Goal state after:
A : Type w
B : Type u₁
C : Type u_1
inst✝⁶ : CommSemiring A
inst✝⁵ : CommSemiring B
inst✝⁴ : Semiring C
inst✝³ : Algebra A B
inst✝² : Algebra B C
inst✝¹ : Algebra A C
inst✝ : IsScalarTower A B C
x : Finset C
hx : Algebra.adjoin A ↑x = ⊤
y : Finset C
hy : span B ↑y = ⊤
f : C → C → B
h✝ : ∀ (x : C), Function.support (f x) ⊆ ↑y
hf : ∀ (x : C), ∑ a ∈ y, f x a • a = x
s : Finset B := image₂ f (x ∪ y * y) y
⊢ ∃ B₀, B₀.FG ∧ ⊤.FG
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
hn : n ≠ 0
⊢ (∑ i ∈ range n, X ^ i).Monic

Tactic:
by
  nontriviality R
  apply monic_X.geom_sum _ hn
  simp only [natDegree_X, zero_lt_one]

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 • x ∈ toSubmodule (ofId (↥S') S).range

Tactic:
← tsub_add_cancel_of_le (show n i ≤ N from Finset.le_sup hi),

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 - n i + n i) • x ∈ toSubmodule (ofId (↥S') S).range
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
σ : Type v
inst✝ : CommRing R
s : Set σ
p : MvPolynomial (↑s) R
eqv : MvPolynomial (↑sᶜ) (MvPolynomial (↑s) R) ≃ₐ[R] MvPolynomial σ R :=
  (sumAlgEquiv R ↑sᶜ ↑s).symm.trans (renameEquiv R ((Equiv.sumComm ↑sᶜ ↑s).trans (Equiv.Set.sumCompl s)))
this :
  (rename Subtype.val) p =
    ((↑eqv).comp (Algebra.algHom R (MvPolynomial (↑s) R) (MvPolynomial (↑sᶜ) (MvPolynomial (↑s) R)))) p
⊢ Prime p ↔ Prime ((rename Subtype.val) p)

Tactic:
simpa [this, MulEquiv.prime_iff, Algebra.algHom] using (prime_C_iff _).symm

Goal state after:
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case mp
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
⊢ FiniteType R A → ∃ ι x f, Surjective ⇑f

Tactic:
rw [iff_quotient_freeAlgebra]

Goal state after:
case mp
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
⊢ (∃ s f, Surjective ⇑f) → ∃ ι x f, Surjective ⇑f
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 := ⋯.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
this✝ : 0 ≠ 1
this : Nontrivial R
q : R[X]
hq : q ∈ I
hdq : q.degree ≤ ↑N
hlqp : q.leadingCoeff = p.leadingCoeff
hq0 : q ≠ 0
⊢ q.leadingCoeff * (X ^ (k - q.natDegree)).leadingCoeff ≠ 0

Tactic:
Polynomial.leadingCoeff_X_pow,

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
this✝ : 0 ≠ 1
this : Nontrivial R
q : R[X]
hq : q ∈ I
hdq : q.degree ≤ ↑N
hlqp : q.leadingCoeff = p.leadingCoeff
hq0 : q ≠ 0
⊢ q.leadingCoeff * 1 ≠ 0
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹ : Monoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
f : R[M]
⊢ ∃ a, ((FreeAlgebra.lift R) fun s ↦ (of R M) ↑s) a = f

Tactic:
induction f using induction_on with
  | of m =>
    have : m ∈ closure S := hS.symm ▸ mem_top _
    refine Submonoid.closure_induction (fun m hm => ?_) ?_ ?_ this
    · exact ⟨FreeAlgebra.ι R ⟨m, hm⟩, FreeAlgebra.lift_ι_apply _ _⟩
    · exact ⟨1, map_one _⟩
    · rintro m₁ m₂ _ _ ⟨P₁, hP₁⟩ ⟨P₂, hP₂⟩
      exact
        ⟨P₁ * P₂, by
          rw [map_mul, hP₁, hP₂, of_apply, of_apply, of_apply, single_mul_single, one_mul]⟩
  | add f g ihf ihg =>
    rcases ihf with ⟨P, rfl⟩
    rcases ihg with ⟨Q, rfl⟩
    exact ⟨P + Q, map_add _ _ _⟩
  | smul r f ih =>
    rcases ih with ⟨P, rfl⟩
    exact ⟨r • P, map_smul _ _ _⟩

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

Goal state before:
pp: case a
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Subalgebra R A
⊢ toSubmodule S * toSubmodule S ≤ toSubmodule S

pp: case a
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Subalgebra R A
⊢ toSubmodule S ≤ toSubmodule S * toSubmodule S

Tactic:
· refine (mul_toSubmodule_le _ _).trans_eq ?_
    rw [sup_idem]

Goal state after:
case a
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Subalgebra R A
⊢ toSubmodule S ≤ toSubmodule S * toSubmodule S
Module: Mathlib.Algebra.CharP.Two

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R 2
x y : R
⊢ x + -y = x + y

Tactic:
neg_eq

Goal state after:
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R 2
x y : R
⊢ x + y = x + y