mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case inr.inl
d : ℕ
hd : d ≠ 0
h : d ∣ 0
⊢ (0 / d).factorization = factorization 0 - d.factorization

pp: case inr.inr
d n : ℕ
h : d ∣ n
hd : d ≠ 0
hn : n ≠ 0
⊢ (n / d).factorization = n.factorization - d.factorization

Tactic:
;

Goal state after:
case inr.inl
d : ℕ
hd : d ≠ 0
h : d ∣ 0
⊢ (0 / d).factorization = factorization 0 - d.factorization

case inr.inr
d n : ℕ
h : d ∣ n
hd : d ≠ 0
hn : n ≠ 0
⊢ (n / d).factorization = n.factorization - d.factorization
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
a : G
ha : IsOfFinOrder a
⊢ (↑(Finset.image (fun x ↦ a ^ x) (Finset.range (orderOf a)))).Finite

Tactic:
;

Goal state after:
G : Type u_1
inst✝ : Monoid G
a : G
ha : IsOfFinOrder a
⊢ (↑(Finset.image (fun x ↦ a ^ x) (Finset.range (orderOf a)))).Finite
Module: Mathlib.Data.Nat.Choose.Factorization

Goal state before:
pp: a b : ℕ
hb : b ≠ 0
k : ℕ
hc : b * k ≠ 0
⊢ b.factorization a ≤ (b * k).factorization a

Tactic:
;

Goal state after:
a b : ℕ
hb : b ≠ 0
k : ℕ
hc : b * k ≠ 0
⊢ b.factorization a ≤ (b * k).factorization a
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case inl
d : ℕ
hd : d ≠ 0
hdn : d ≤ d
⊢ (d / d).factorization = d.factorization - d.factorization → d ∣ d

pp: case inr
d n : ℕ
hd : d ≠ 0
hdn : d ≤ n
hd_lt_n : d < n
⊢ (n / d).factorization = n.factorization - d.factorization → d ∣ n

Tactic:
;

Goal state after:
case inl
d : ℕ
hd : d ≠ 0
hdn : d ≤ d
⊢ (d / d).factorization = d.factorization - d.factorization → d ∣ d

case inr
d n : ℕ
hd : d ≠ 0
hdn : d ≤ n
hd_lt_n : d < n
⊢ (n / d).factorization = n.factorization - d.factorization → d ∣ n
Module: Mathlib.Data.Nat.Choose.Factorization

Goal state before:
pp: case inl
p k : ℕ
p_large : 0 < p ^ 2
⊢ log p 0 ≤ 1

pp: case inr
p n k : ℕ
p_large : n < p ^ 2
hn0 : n ≠ 0
⊢ log p n ≤ 1

Tactic:
;

Goal state after:
case inl
p k : ℕ
p_large : 0 < p ^ 2
⊢ log p 0 ≤ 1

case inr
p n k : ℕ
p_large : n < p ^ 2
hn0 : n ≠ 0
⊢ log p n ≤ 1
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case inl
a b : ℕ
hb0 : b ≠ 0
hab : a ∣ b
p : ℕ
pp : ¬Prime p
⊢ p ^ a.factorization p ∣ p ^ b.factorization p

pp: case inr
a b : ℕ
hb0 : b ≠ 0
hab : a ∣ b
p : ℕ
pp : Prime p
⊢ p ^ a.factorization p ∣ p ^ b.factorization p

Tactic:
;

Goal state after:
case inl
a b : ℕ
hb0 : b ≠ 0
hab : a ∣ b
p : ℕ
pp : ¬Prime p
⊢ p ^ a.factorization p ∣ p ^ b.factorization p

case inr
a b : ℕ
hb0 : b ≠ 0
hab : a ∣ b
p : ℕ
pp : Prime p
⊢ p ^ a.factorization p ∣ p ^ b.factorization p
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case inr.inl
b : ℕ
hb0 : b ≠ 0
p : ℕ
pp : Prime p
hab : 0 ∣ b
⊢ p ^ (factorization 0) p ∣ p ^ b.factorization p

pp: case inr.inr
a b : ℕ
hb0 : b ≠ 0
hab : a ∣ b
p : ℕ
pp : Prime p
ha0 : a ≠ 0
⊢ p ^ a.factorization p ∣ p ^ b.factorization p

Tactic:
;

Goal state after:
case inr.inl
b : ℕ
hb0 : b ≠ 0
p : ℕ
pp : Prime p
hab : 0 ∣ b
⊢ p ^ (factorization 0) p ∣ p ^ b.factorization p

case inr.inr
a b : ℕ
hb0 : b ≠ 0
hab : a ∣ b
p : ℕ
pp : Prime p
ha0 : a ≠ 0
⊢ p ^ a.factorization p ∣ p ^ b.factorization p
Module: Mathlib.Data.Nat.Choose.Factorization

Goal state before:
pp: case pos
p n k : ℕ
h : n < p
hnk : n < k
⊢ (n.choose k).factorization p = 0

pp: case neg
p n k : ℕ
h : n < p
hnk : k ≤ n
⊢ (n.choose k).factorization p = 0

Tactic:
;

Goal state after:
case pos
p n k : ℕ
h : n < p
hnk : n < k
⊢ (n.choose k).factorization p = 0

case neg
p n k : ℕ
h : n < p
hnk : k ≤ n
⊢ (n.choose k).factorization p = 0
Module: Mathlib.Data.Nat.Choose.Factorization

Goal state before:
pp: case h
n k : ℕ
hkn : k ≤ n
p : ℕ
hp : p ∈ (n.choose k).factorization.support
⊢ p < n + 1

Tactic:
contrapose! hp

Goal state after:
case h
n k : ℕ
hkn : k ≤ n
p : ℕ
hp : n + 1 ≤ p
⊢ p ∉ (n.choose k).factorization.support
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case pos
n : ℕ
hn : n = 0
⊢ ∏ p ∈ n.primeFactors, p ∣ n

pp: case neg
n : ℕ
hn : ¬n = 0
⊢ ∏ p ∈ n.primeFactors, p ∣ n

Tactic:
· subst hn
    simp

Goal state after:
case neg
n : ℕ
hn : ¬n = 0
⊢ ∏ p ∈ n.primeFactors, p ∣ n
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case neg
n : ℕ
hn : ¬n = 0
⊢ ∏ p ∈ n.primeFactors, p ∣ n

Tactic:
· simpa [prod_primeFactorsList hn] using (n.primeFactorsList : Multiset ℕ).toFinset_prod_dvd_prod

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : RightCancelMonoid G
x : G
s : Set G := (fun n ↦ x ^ n) '' {n | 0 < n}
hs : s ⊆ {y | ¬IsOfFinOrder y}
h : s.Finite
⊢ IsOfFinOrder x

Tactic:
have : ¬Function.Injective fun n : ℕ => x ^ n := by
    have := Set.not_injOn_infinite_finite_image (Set.Ioi_infinite 0) h
    contrapose this
    exact Set.injOn_of_injective this

Goal state after:
G : Type u_1
inst✝ : RightCancelMonoid G
x : G
s : Set G := (fun n ↦ x ^ n) '' {n | 0 < n}
hs : s ⊆ {y | ¬IsOfFinOrder y}
h : s.Finite
this : ¬Injective fun n ↦ x ^ n
⊢ IsOfFinOrder x
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
x : G
hx : IsOfFinOrder x
n : ℕ
⊢ (finEquivPowers hx).symm ((Equiv.setCongr ⋯).symm ⟨x ^ n, ⋯⟩) = ⟨n % orderOf x, ⋯⟩

Tactic:
;

Goal state after:
G : Type u_1
inst✝ : Group G
x : G
hx : IsOfFinOrder x
n : ℕ
⊢ (finEquivPowers hx).symm ((Equiv.setCongr ⋯).symm ⟨x ^ n, ⋯⟩) = ⟨n % orderOf x, ⋯⟩
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case refine_2
G : Type u_1
inst✝² : Monoid G
n : ℕ
inst✝¹ : Fintype G
inst✝ : DecidableEq G
hn : n ≠ 0
⊢ (n.divisors.biUnion fun m ↦ {x | orderOf x = m}) = {x | x ^ n = 1}

Tactic:
;

Goal state after:
case refine_2
G : Type u_1
inst✝² : Monoid G
n : ℕ
inst✝¹ : Fintype G
inst✝ : DecidableEq G
hn : n ≠ 0
⊢ (n.divisors.biUnion fun m ↦ {x | orderOf x = m}) = {x | x ^ n = 1}
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case refine_2
G : Type u_1
inst✝² : Monoid G
n : ℕ
inst✝¹ : Fintype G
inst✝ : DecidableEq G
hn : n ≠ 0
a✝ : G
⊢ (a✝ ∈ n.divisors.biUnion fun m ↦ {x | orderOf x = m}) ↔ a✝ ∈ {x | x ^ n = 1}

Tactic:
;

Goal state after:
case refine_2
G : Type u_1
inst✝² : Monoid G
n : ℕ
inst✝¹ : Fintype G
inst✝ : DecidableEq G
hn : n ≠ 0
a✝ : G
⊢ (a✝ ∈ n.divisors.biUnion fun m ↦ {x | orderOf x = m}) ↔ a✝ ∈ {x | x ^ n = 1}
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝¹ : LeftCancelMonoid G
inst✝ : Finite G
x : G
h : ¬IsOfFinOrder x
⊢ False

Tactic:
;

Goal state after:
G : Type u_1
inst✝¹ : LeftCancelMonoid G
inst✝ : Finite G
x : G
h : ¬IsOfFinOrder x
⊢ False
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
H✝ : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝³ : LeftCancelMonoid G
inst✝² : Finite G
x y : G
n : ℕ
H : Type u_6
inst✝¹ : RightCancelMonoid H
inst✝ : Finite H
this : Finite Hᵐᵒᵖ := Finite.of_equiv H MulOpposite.opEquiv
⊢ Group H

Tactic:
letI : Group Hᵐᵒᵖ := LeftCancelMonoid.groupOfFinite (G := Hᵐᵒᵖ)

Goal state after:
G : Type u_1
H✝ : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝³ : LeftCancelMonoid G
inst✝² : Finite G
x y : G
n : ℕ
H : Type u_6
inst✝¹ : RightCancelMonoid H
inst✝ : Finite H
this✝ : Finite Hᵐᵒᵖ := Finite.of_equiv H MulOpposite.opEquiv
this : Group Hᵐᵒᵖ := LeftCancelMonoid.groupOfFinite
⊢ Group H
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
x : G
⊢ (Injective fun n ↦ x ^ n) ↔ ¬IsOfFinOrder x

Tactic:
refine ⟨?_, fun h n m hnm => ?_⟩

Goal state after:
case refine_1
G : Type u_1
inst✝ : Group G
x : G
⊢ (Injective fun n ↦ x ^ n) → ¬IsOfFinOrder x

case refine_2
G : Type u_1
inst✝ : Group G
x : G
h : ¬IsOfFinOrder x
n m : ℤ
hnm : (fun n ↦ x ^ n) n = (fun n ↦ x ^ n) m
⊢ n = m
Module: Mathlib.Algebra.CharP.Frobenius

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
p n : ℕ
inst✝ : ExpChar R p
x✝ : R
⊢ (iterateFrobenius R p n) x✝ = (frobenius R p ^ n) x✝

Tactic:
;

Goal state after:
R : Type u_1
inst✝¹ : CommSemiring R
p n : ℕ
inst✝ : ExpChar R p
x✝ : R
⊢ (iterateFrobenius R p n) x✝ = (frobenius R p ^ n) x✝
Module: Mathlib.Algebra.CharP.Frobenius

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_2
inst✝³ : CommSemiring S
f : R →* S
g : R →+* S
p m n : ℕ
inst✝² : ExpChar R p
inst✝¹ : ExpChar S p
x y : R
inst✝ : Algebra R S
r : R
s : S
⊢ (algebraMap R S) ((_root_.frobenius R p) r) * (_root_.frobenius S p) s =
    (algebraMap R S) ((_root_.frobenius R p) r) * (↑↑(_root_.frobenius S p)).toFun s

Tactic:
;

Goal state after:
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_2
inst✝³ : CommSemiring S
f : R →* S
g : R →+* S
p m n : ℕ
inst✝² : ExpChar R p
inst✝¹ : ExpChar S p
x y : R
inst✝ : Algebra R S
r : R
s : S
⊢ (algebraMap R S) ((_root_.frobenius R p) r) * (_root_.frobenius S p) s =
    (algebraMap R S) ((_root_.frobenius R p) r) * (↑↑(_root_.frobenius S p)).toFun s
Module: Mathlib.Algebra.CharP.Frobenius

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_2
inst✝³ : CommSemiring S
f✝ : R →* S
g : R →+* S
p m n : ℕ
inst✝² : ExpChar R p
inst✝¹ : ExpChar S p
x y : R
inst✝ : Algebra R S
f : R
s : S
⊢ (algebraMap R S) (f ^ p ^ n) * s ^ p ^ n = (algebraMap R S) (f ^ p ^ n) * (↑↑(_root_.iterateFrobenius S p n)).toFun s

Tactic:
;

Goal state after:
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_2
inst✝³ : CommSemiring S
f✝ : R →* S
g : R →+* S
p m n : ℕ
inst✝² : ExpChar R p
inst✝¹ : ExpChar S p
x y : R
inst✝ : Algebra R S
f : R
s : S
⊢ (algebraMap R S) (f ^ p ^ n) * s ^ p ^ n = (algebraMap R S) (f ^ p ^ n) * (↑↑(_root_.iterateFrobenius S p n)).toFun s
Module: Mathlib.Data.Nat.Multiplicity

Goal state before:
pp: p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
⊢ emultiplicity p (p ^ n) ≤ emultiplicity p ((p ^ n).choose k) + emultiplicity p k

Tactic:
;

Goal state after:
p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
⊢ emultiplicity p (p ^ n) ≤ emultiplicity p ((p ^ n).choose k) + emultiplicity p k
Module: Mathlib.Data.Nat.Multiplicity

Goal state before:
pp: h2 : _root_.Prime 2
b : Bool
n : ℕ
ih : n ≠ 0 → emultiplicity 2 n ! < ↑n
h : bit b n ≠ 0
hn : ¬n = 0
⊢ emultiplicity 2 (2 * n)! < ↑(2 * n)

Tactic:
rw [prime_two.emultiplicity_factorial_mul]

Goal state after:
h2 : _root_.Prime 2
b : Bool
n : ℕ
ih : n ≠ 0 → emultiplicity 2 n ! < ↑n
h : bit b n ≠ 0
hn : ¬n = 0
⊢ emultiplicity 2 n ! + ↑n < ↑(2 * n)
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_6
inst✝ : Group G
s : Submonoid G
hs : (↑s).Finite
x : G
hx : x ∈ s
⊢ Nat.card ↥(powers x) ≤ Nat.card ↥s

Tactic:
;

Goal state after:
G : Type u_6
inst✝ : Group G
s : Submonoid G
hs : (↑s).Finite
x : G
hx : x ∈ s
⊢ Nat.card ↥(powers x) ≤ Nat.card ↥s
Module: Mathlib.Algebra.MonoidAlgebra.Division

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : AddCommMonoid G
inst✝ : IsCancelAdd G
g a✝ : G
⊢ (0 /ᵒᶠ g).coeff a✝ = (coeff 0) a✝

Tactic:
;

Goal state after:
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : AddCommMonoid G
inst✝ : IsCancelAdd G
g a✝ : G
⊢ (0 /ᵒᶠ g).coeff a✝ = (coeff 0) a✝
Module: Mathlib.Algebra.MonoidAlgebra.Division

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : AddCommMonoid G
inst✝ : IsCancelAdd G
x : k[G]
a✝ : G
⊢ (x /ᵒᶠ 0).coeff a✝ = x.coeff a✝

Tactic:
;

Goal state after:
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : AddCommMonoid G
inst✝ : IsCancelAdd G
x : k[G]
a✝ : G
⊢ (x /ᵒᶠ 0).coeff a✝ = x.coeff a✝
Module: Mathlib.Algebra.MonoidAlgebra.Division

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : AddCommMonoid G
inst✝ : IsCancelAdd G
x y : k[G]
g a✝ : G
⊢ ((x + y) /ᵒᶠ g).coeff a✝ = (x /ᵒᶠ g + y /ᵒᶠ g).coeff a✝

Tactic:
;

Goal state after:
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : AddCommMonoid G
inst✝ : IsCancelAdd G
x y : k[G]
g a✝ : G
⊢ ((x + y) /ᵒᶠ g).coeff a✝ = (x /ᵒᶠ g + y /ᵒᶠ g).coeff a✝
Module: Mathlib.Algebra.MonoidAlgebra.Division

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : AddCommMonoid G
inst✝ : IsCancelAdd G
x : k[G]
a b a✝ : G
⊢ (x /ᵒᶠ (a + b)).coeff a✝ = (x /ᵒᶠ a /ᵒᶠ b).coeff a✝

Tactic:
;

Goal state after:
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : AddCommMonoid G
inst✝ : IsCancelAdd G
x : k[G]
a b a✝ : G
⊢ (x /ᵒᶠ (a + b)).coeff a✝ = (x /ᵒᶠ a /ᵒᶠ b).coeff a✝
Module: Mathlib.Algebra.MonoidAlgebra.Division

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : AddCommMonoid G
inst✝ : IsCancelAdd G
a : G
x : k[G]
a✝ : G
⊢ (of' k G a * x /ᵒᶠ a).coeff a✝ = x.coeff a✝

Tactic:
;

Goal state after:
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : AddCommMonoid G
inst✝ : IsCancelAdd G
a : G
x : k[G]
a✝ : G
⊢ (of' k G a * x /ᵒᶠ a).coeff a✝ = x.coeff a✝
Module: Mathlib.Algebra.MonoidAlgebra.Division

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : AddCommMonoid G
inst✝ : IsCancelAdd G
x : k[G]
a a✝ : G
⊢ (x * of' k G a /ᵒᶠ a).coeff a✝ = x.coeff a✝

Tactic:
;

Goal state after:
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : AddCommMonoid G
inst✝ : IsCancelAdd G
x : k[G]
a a✝ : G
⊢ (x * of' k G a /ᵒᶠ a).coeff a✝ = x.coeff a✝
Module: Mathlib.Algebra.Polynomial.Inductions

Goal state before:
pp: R : Type u
n : ℕ
inst✝ : Semiring R
p : R[X]
⊢ p.divX.coeff n = p.coeff (1 + n)

Tactic:
;

Goal state after:
R : Type u
n : ℕ
inst✝ : Semiring R
p : R[X]
⊢ p.divX.coeff n = p.coeff (1 + n)
Module: Mathlib.Algebra.Polynomial.Inductions

Goal state before:
pp: case ofFinsupp
R : Type u
n : ℕ
inst✝ : Semiring R
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ { toFinsupp := toFinsupp✝ }.divX.coeff n = { toFinsupp := toFinsupp✝ }.coeff (1 + n)

Tactic:
;

Goal state after:
case ofFinsupp
R : Type u
n : ℕ
inst✝ : Semiring R
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ { toFinsupp := toFinsupp✝ }.divX.coeff n = { toFinsupp := toFinsupp✝ }.coeff (1 + n)
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝² : Ring G
inst✝¹ : LinearOrder G
inst✝ : IsStrictOrderedRing G
ha₀ : 1 ≤ 0
ha : IsOfFinOrder 1
⊢ False

Tactic:
;

Goal state after:
G : Type u_1
inst✝² : Ring G
inst✝¹ : LinearOrder G
inst✝ : IsStrictOrderedRing G
ha₀ : 1 ≤ 0
ha : IsOfFinOrder 1
⊢ False
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: α : Type u_4
β : Type u_5
inst✝¹ : Monoid α
inst✝ : Monoid β
a : α
b : β
⊢ IsOfFinOrder a → IsOfFinOrder b → IsOfFinOrder (a, b)

Tactic:
by
  simpa only [← orderOf_pos_iff, Prod.orderOf] using Nat.lcm_pos

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
hp0 : p ≠ 0
this✝¹ : Nontrivial R
h : ¬p.degree ≤ 0
hXp0 : p.divX ≠ 0
this✝ : p.divX.leadingCoeff * X.leadingCoeff ≠ 0
this : (C (p.coeff 0)).degree < (p.divX * X).degree
⊢ p.divX.degree < (p.divX * X).degree

Tactic:
;

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
hp0 : p ≠ 0
this✝¹ : Nontrivial R
h : ¬p.degree ≤ 0
hXp0 : p.divX ≠ 0
this✝ : p.divX.leadingCoeff * X.leadingCoeff ≠ 0
this : (C (p.coeff 0)).degree < (p.divX * X).degree
⊢ p.divX.degree < (p.divX * X).degree
Module: Mathlib.Algebra.Polynomial.Inductions

Goal state before:
pp: R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p✝ q : R[X]
M : R[X] → Sort u_1
p : R[X]
M0 : M 0
MC : (p : R[X]) → (a : R) → p.coeff 0 = 0 → a ≠ 0 → M p → M (p + C a)
MX : (p : R[X]) → p ≠ 0 → M p → M (p * X)
this : DecidableEq R := Classical.decEq R
hp : ¬p.divX * X + C (p.coeff 0) = 0
wf : (p.divX * X + C (p.coeff 0)).divX.degree < (p.divX * X + C (p.coeff 0)).degree
hcp0 : ¬p.coeff 0 = 0
hpX0 : p.divX = 0
⊢ M 0

Tactic:
;

Goal state after:
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p✝ q : R[X]
M : R[X] → Sort u_1
p : R[X]
M0 : M 0
MC : (p : R[X]) → (a : R) → p.coeff 0 = 0 → a ≠ 0 → M p → M (p + C a)
MX : (p : R[X]) → p ≠ 0 → M p → M (p * X)
this : DecidableEq R := Classical.decEq R
hp : ¬p.divX * X + C (p.coeff 0) = 0
wf : (p.divX * X + C (p.coeff 0)).divX.degree < (p.divX * X + C (p.coeff 0)).degree
hcp0 : ¬p.coeff 0 = 0
hpX0 : p.divX = 0
⊢ M 0
Module: Mathlib.Algebra.Polynomial.Inductions

Goal state before:
pp: R : Type u
inst✝ : Semiring R
P : R[X] → Prop
p : R[X]
h0 : 0 < p.degree
hC : ∀ {a : R}, a ≠ 0 → P (C a * X)
hX : ∀ {p : R[X]}, 0 < p.degree → P p → P (p * X)
hadd : ∀ {p : R[X]} {a : R}, 0 < p.degree → P p → P (p + C a)
h : 0 < ⊥
⊢ P 0

Tactic:
;

Goal state after:
R : Type u
inst✝ : Semiring R
P : R[X] → Prop
p : R[X]
h0 : 0 < p.degree
hC : ∀ {a : R}, a ≠ 0 → P (C a * X)
hX : ∀ {p : R[X]}, 0 < p.degree → P p → P (p * X)
hadd : ∀ {p : R[X]} {a : R}, 0 < p.degree → P p → P (p + C a)
h : 0 < ⊥
⊢ P 0
Module: Mathlib.Tactic.ComputeDegree

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n : ℕ
f g : R[X]
⊢ (f + g).coeff n = f.coeff n + g.coeff n

Tactic:
;

Goal state after:
R : Type u_1
inst✝ : Semiring R
n : ℕ
f g : R[X]
⊢ (f + g).coeff n = f.coeff n + g.coeff n
Module: Mathlib.Tactic.ComputeDegree

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
n : ℕ
f g : R[X]
⊢ (f - g).coeff n = f.coeff n - g.coeff n

Tactic:
;

Goal state after:
R : Type u_1
inst✝ : Ring R
n : ℕ
f g : R[X]
⊢ (f - g).coeff n = f.coeff n - g.coeff n
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
⊢ ((expand R p) f).coeff n = if p ∣ n then f.coeff (n / p) else 0

Tactic:
by
  simp only [expand_eq_sum]
  simp_rw [coeff_sum, ← pow_mul, C_mul_X_pow_eq_monomial, coeff_monomial, sum]
  split_ifs with h
  · rw [Finset.sum_eq_single (n / p), Nat.mul_div_cancel' h, if_pos rfl]
    · intro b _ hb2
      rw [if_neg]
      intro hb3
      apply hb2
      rw [← hb3, Nat.mul_div_cancel_left b hp]
    · intro hn
      rw [notMem_support_iff.1 hn]
      split_ifs <;> rfl
  · rw [Finset.sum_eq_zero]
    intro k _
    rw [if_neg]
    exact fun hkn => h ⟨k, hkn.symm⟩

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
hp : 0 < p.degree
hmp : p.Monic
hq : q ≠ 0
zn0 : 0 ≠ 1
x✝ : p ^ (q.natDegree + 1) ∣ q
hp0 : p ≠ 0
hr : q = p ^ (q.natDegree + 1) * 0
⊢ False

Tactic:
;

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
hp : 0 < p.degree
hmp : p.Monic
hq : q ≠ 0
zn0 : 0 ≠ 1
x✝ : p ^ (q.natDegree + 1) ∣ q
hp0 : p ≠ 0
hr : q = p ^ (q.natDegree + 1) * 0
⊢ False
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
hp : 0 < p.degree
hmp : p.Monic
hq : q ≠ 0
zn0 : 0 ≠ 1
x✝ : p ^ (q.natDegree + 1) ∣ q
r : R[X]
hr : q = p ^ (q.natDegree + 1) * r
hp0 : p ≠ 0
hr0 : r ≠ 0
hpn1 : p.leadingCoeff ^ (q.natDegree + 1) = 1
hpn0' : p.leadingCoeff ^ (q.natDegree + 1) ≠ 0
hpnr0 : (p ^ (q.natDegree + 1)).leadingCoeff * r.leadingCoeff ≠ 0
⊢ ↑0 < p.degree

Tactic:
;

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
hp : 0 < p.degree
hmp : p.Monic
hq : q ≠ 0
zn0 : 0 ≠ 1
x✝ : p ^ (q.natDegree + 1) ∣ q
r : R[X]
hr : q = p ^ (q.natDegree + 1) * r
hp0 : p ≠ 0
hr0 : r ≠ 0
hpn1 : p.leadingCoeff ^ (q.natDegree + 1) = 1
hpn0' : p.leadingCoeff ^ (q.natDegree + 1) ≠ 0
hpnr0 : (p ^ (q.natDegree + 1)).leadingCoeff * r.leadingCoeff ≠ 0
⊢ ↑0 < p.degree
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a✝ b : R
n : ℕ
inst✝ : Semiring R
p✝ : R[X]
a : R
p : R[X]
⊢ ((a • p).sum fun n a ↦ C (a * ↑n) * X ^ (n - 1)) = a • p.sum fun n a ↦ C (a * ↑n) * X ^ (n - 1)

Tactic:
;

Goal state after:
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a✝ b : R
n : ℕ
inst✝ : Semiring R
p✝ : R[X]
a : R
p : R[X]
⊢ ((a • p).sum fun n a ↦ C (a * ↑n) * X ^ (n - 1)) = a • p.sum fun n a ↦ C (a * ↑n) * X ^ (n - 1)
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p.Monic
hq : q.Monic
hdvd : p ∣ q
hdeg : q.natDegree ≤ p.natDegree
⊢ q = p

Tactic:
by
  rw [eq_mul_leadingCoeff_of_monic_of_dvd_of_natDegree_le hp hdvd hdeg]
  simp [hq]

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

Goal state before:
pp: case inl
R : Type u
inst✝ : CommRing R
a b c : R
ha : IsUnit a
this : Invertible a := ha.invertible
⊢ rootMultiplicity c (comp 0 (C a * X + C b)) ≤ rootMultiplicity (a * c + b) 0

pp: case inr
R : Type u
inst✝ : CommRing R
p : R[X]
a b c : R
ha : IsUnit a
this : Invertible a := ha.invertible
hp : p ≠ 0
⊢ rootMultiplicity c (p.comp (C a * X + C b)) ≤ rootMultiplicity (a * c + b) p

Tactic:
;

Goal state after:
case inl
R : Type u
inst✝ : CommRing R
a b c : R
ha : IsUnit a
this : Invertible a := ha.invertible
⊢ rootMultiplicity c (comp 0 (C a * X + C b)) ≤ rootMultiplicity (a * c + b) 0

case inr
R : Type u
inst✝ : CommRing R
p : R[X]
a b c : R
ha : IsUnit a
this : Invertible a := ha.invertible
hp : p ≠ 0
⊢ rootMultiplicity c (p.comp (C a * X + C b)) ≤ rootMultiplicity (a * c + b) p
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
h : q.degree ≤ p.degree ∧ p ≠ 0
hq : q.Monic
hp : p.leadingCoeff ≠ 0
hq0 : q ≠ 0
⊢ q.degree ≤ p.degree

Tactic:
;

Goal state after:
R : Type u
inst✝ : Ring R
p q : R[X]
h : q.degree ≤ p.degree ∧ p ≠ 0
hq : q.Monic
hp : p.leadingCoeff ≠ 0
hq0 : q ≠ 0
⊢ q.degree ≤ p.degree
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ p.coeff (n + 1) * ↑(n + 1) = p.coeff (n + 1) * (↑n + 1)

Tactic:
;

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ p.coeff (n + 1) * ↑(n + 1) = p.coeff (n + 1) * (↑n + 1)
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: case h₂
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f : R[X]
n : ℕ
hn : f.natDegree + 1 ≤ n
⊢ 1 ≤ p

Tactic:
;

Goal state after:
case h₂
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f : R[X]
n : ℕ
hn : f.natDegree + 1 ≤ n
⊢ 1 ≤ p
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p : R[X]
this : DecidableEq R := Classical.decEq R
h : ¬Monic 0
⊢ (if h : Monic 0 then
      (if h_1 : degree 0 ≤ p.degree ∧ p ≠ 0 then
          have z := C p.leadingCoeff * X ^ (p.natDegree - natDegree 0);
          have _wf := ⋯;
          have dm := (p - 0 * z).divModByMonicAux ⋯;
          (z + dm.1, dm.2)
        else (0, p)).2
    else p) =
    p

Tactic:
;

Goal state after:
R : Type u
inst✝ : Ring R
p : R[X]
this : DecidableEq R := Classical.decEq R
h : ¬Monic 0
⊢ (if h : Monic 0 then
      (if h_1 : degree 0 ≤ p.degree ∧ p ≠ 0 then
          have z := C p.leadingCoeff * X ^ (p.natDegree - natDegree 0);
          have _wf := ⋯;
          have dm := (p - 0 * z).divModByMonicAux ⋯;
          (z + dm.1, dm.2)
        else (0, p)).2
    else p) =
    p
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p : R[X]
this : DecidableEq R := Classical.decEq R
h : ¬Monic 0
⊢ (if h : Monic 0 then
      (if h_1 : degree 0 ≤ p.degree ∧ p ≠ 0 then
          have z := C p.leadingCoeff * X ^ (p.natDegree - natDegree 0);
          have _wf := ⋯;
          have dm := (p - 0 * z).divModByMonicAux ⋯;
          (z + dm.1, dm.2)
        else (0, p)).1
    else 0) =
    0

Tactic:
;

Goal state after:
R : Type u
inst✝ : Ring R
p : R[X]
this : DecidableEq R := Classical.decEq R
h : ¬Monic 0
⊢ (if h : Monic 0 then
      (if h_1 : degree 0 ≤ p.degree ∧ p ≠ 0 then
          have z := C p.leadingCoeff * X ^ (p.natDegree - natDegree 0);
          have _wf := ⋯;
          have dm := (p - 0 * z).divModByMonicAux ⋯;
          (z + dm.1, dm.2)
        else (0, p)).1
    else 0) =
    0
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n✝ : ℕ
⊢ (contract p (f + g)).coeff n✝ = (contract p f + contract p g).coeff n✝

Tactic:
;

Goal state after:
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n✝ : ℕ
⊢ (contract p (f + g)).coeff n✝ = (contract p f + contract p g).coeff n✝