mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: b n : ℕ
IH : ∀ m ≤ n, ∀ (i : ℕ), ((b + 2).digits m)[i]?.getD 0 = m / (b + 2) ^ i % (b + 2)
⊢ b + 2 ≠ 1

Tactic:
by grind

Goal state after:
Module: Mathlib.NumberTheory.Padics.PadicVal.Defs

Goal state before:
pp: case inl
n : ℕ
⊢ (emultiplicity 1 n).toNat = padicValNat 1 n

pp: case inr
p n : ℕ
hp : p ≠ 1
⊢ (emultiplicity p n).toNat = padicValNat p n

Tactic:
· simp

Goal state after:
case inr
p n : ℕ
hp : p ≠ 1
⊢ (emultiplicity p n).toNat = padicValNat p n
Module: Mathlib.NumberTheory.Padics.PadicVal.Defs

Goal state before:
pp: case inr.inl
p : ℕ
hp : p ≠ 1
⊢ (emultiplicity p 0).toNat = padicValNat p 0

pp: case inr.inr
p n : ℕ
hp : p ≠ 1
hn : n ≠ 0
⊢ (emultiplicity p n).toNat = padicValNat p n

Tactic:
· simp

Goal state after:
case inr.inr
p n : ℕ
hp : p ≠ 1
hn : n ≠ 0
⊢ (emultiplicity p n).toNat = padicValNat p n
Module: Mathlib.NumberTheory.Padics.PadicVal.Defs

Goal state before:
pp: case inl
p : ℕ
⊢ padicValNat p 0 = 0 ↔ p = 1 ∨ 0 = 0 ∨ ¬p ∣ 0

pp: case inr
p n : ℕ
hn₀ : n ≠ 0
⊢ padicValNat p n = 0 ↔ p = 1 ∨ n = 0 ∨ ¬p ∣ n

Tactic:
· simp

Goal state after:
case inr
p n : ℕ
hn₀ : n ≠ 0
⊢ padicValNat p n = 0 ↔ p = 1 ∨ n = 0 ∨ ¬p ∣ n
Module: Mathlib.NumberTheory.Padics.PadicVal.Defs

Goal state before:
pp: case inr.inl
n : ℕ
hn₀ : n ≠ 0
⊢ padicValNat 1 n = 0 ↔ 1 = 1 ∨ n = 0 ∨ ¬1 ∣ n

pp: case inr.inr
p n : ℕ
hn₀ : n ≠ 0
hp₁ : p ≠ 1
⊢ padicValNat p n = 0 ↔ p = 1 ∨ n = 0 ∨ ¬p ∣ n

Tactic:
· simp

Goal state after:
case inr.inr
p n : ℕ
hn₀ : n ≠ 0
hp₁ : p ≠ 1
⊢ padicValNat p n = 0 ↔ p = 1 ∨ n = 0 ∨ ¬p ∣ n
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: case inl
n b : ℕ
hb : 1 < b
l i : ℕ
hi : i ∈ b.digits n
⊢ i < b

Tactic:
exact digits_lt_base hb hi

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case inl
G : Type u_1
inst✝ : Monoid G
a : G
⊢ IsOfFinOrder (a ^ 0) ↔ IsOfFinOrder a ∨ 0 = 0

pp: case inr
G : Type u_1
inst✝ : Monoid G
a : G
n : ℕ
hn : n ≠ 0
⊢ IsOfFinOrder (a ^ n) ↔ IsOfFinOrder a ∨ n = 0

Tactic:
· simp

Goal state after:
case inr
G : Type u_1
inst✝ : Monoid G
a : G
n : ℕ
hn : n ≠ 0
⊢ IsOfFinOrder (a ^ n) ↔ IsOfFinOrder a ∨ n = 0
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case h₂
α : Type u_1
inst✝ : Ring α
p a b : α
h : ↑(multiplicity p b) < emultiplicity p a
this : FiniteMultiplicity p b
⊢ p ^ multiplicity p b ∣ b

Tactic:
· simp

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
h : 0 < n
⊢ (if h : 1 ∈ periodicPts fun x_1 ↦ x * x_1 then Nat.find h else 0) = n ↔
    IsPeriodicPt (fun x_1 ↦ x * x_1) n 1 ∧ ∀ m < n, 0 < m → ¬IsPeriodicPt (fun x_1 ↦ x * x_1) m 1

Tactic:
split_ifs with h1

Goal state after:
case pos
G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
h : 0 < n
h1 : 1 ∈ periodicPts fun x_1 ↦ x * x_1
⊢ Nat.find h1 = n ↔ IsPeriodicPt (fun x_1 ↦ x * x_1) n 1 ∧ ∀ m < n, 0 < m → ¬IsPeriodicPt (fun x_1 ↦ x * x_1) m 1

case neg
G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
h : 0 < n
h1 : 1 ∉ periodicPts fun x_1 ↦ x * x_1
⊢ 0 = n ↔ IsPeriodicPt (fun x_1 ↦ x * x_1) n 1 ∧ ∀ m < n, 0 < m → ¬IsPeriodicPt (fun x_1 ↦ x * x_1) m 1
Module: Mathlib.Data.Nat.Factorization.Defs

Goal state before:
pp: case refine_1
α : Type u_1
S : Finset α
g : α → ℕ
hS : ∀ x ∈ S, g x ≠ 0
⊢ (∅.prod g).factorization = ∑ x ∈ ∅, (g x).factorization

pp: case refine_2
α : Type u_1
S : Finset α
g : α → ℕ
hS : ∀ x ∈ S, g x ≠ 0
⊢ ∀ (a : α) (s : Finset α),
    a ∈ S →
      s ⊆ S →
        a ∉ s →
          (s.prod g).factorization = ∑ x ∈ s, (g x).factorization →
            ((insert a s).prod g).factorization = ∑ x ∈ insert a s, (g x).factorization

Tactic:
· simp

Goal state after:
case refine_2
α : Type u_1
S : Finset α
g : α → ℕ
hS : ∀ x ∈ S, g x ≠ 0
⊢ ∀ (a : α) (s : Finset α),
    a ∈ S →
      s ⊆ S →
        a ∉ s →
          (s.prod g).factorization = ∑ x ∈ s, (g x).factorization →
            ((insert a s).prod g).factorization = ∑ x ∈ insert a s, (g x).factorization
Module: Mathlib.Data.Nat.Factorization.Defs

Goal state before:
pp: case succ.inl
k : ℕ
ih : (0 ^ k).factorization = k • factorization 0
⊢ (0 ^ (k + 1)).factorization = (k + 1) • factorization 0

pp: case succ.inr
n k : ℕ
ih : (n ^ k).factorization = k • n.factorization
hn : n ≠ 0
⊢ (n ^ (k + 1)).factorization = (k + 1) • n.factorization

Tactic:
· simp

Goal state after:
case succ.inr
n k : ℕ
ih : (n ^ k).factorization = k • n.factorization
hn : n ≠ 0
⊢ (n ^ (k + 1)).factorization = (k + 1) • n.factorization
Module: Mathlib.Data.Nat.Factorization.Defs

Goal state before:
pp: case inl
f : ℕ →₀ ℕ
hf : f ≤ factorization 0
⊢ (f.prod fun x1 x2 ↦ x1 ^ x2) ∣ 0

pp: case inr
n : ℕ
f : ℕ →₀ ℕ
hf : f ≤ n.factorization
hn : n ≠ 0
⊢ (f.prod fun x1 x2 ↦ x1 ^ x2) ∣ n

Tactic:
· simp

Goal state after:
case inr
n : ℕ
f : ℕ →₀ ℕ
hf : f ≤ n.factorization
hn : n ≠ 0
⊢ (f.prod fun x1 x2 ↦ x1 ^ x2) ∣ n
Module: Mathlib.Data.Nat.Choose.Factorization

Goal state before:
pp: n p : ℕ
hp : Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
h2 : p * n + 1 ≤ p * (n + 1)
⊢ (p * (n + 1))!.factorization p = (p * n)!.factorization p + (n + 1).factorization p + 1

Tactic:
have h3 : p * n + 1 ≤ p * (n + 1) + 1 := by lia

Goal state after:
n p : ℕ
hp : Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
h2 : p * n + 1 ≤ p * (n + 1)
h3 : p * n + 1 ≤ p * (n + 1) + 1
⊢ (p * (n + 1))!.factorization p = (p * n)!.factorization p + (n + 1).factorization p + 1
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case inl
b : ℕ
hb : b ≠ 0
⊢ factorization 0 ≤ (0 * b).factorization

pp: case inr
a b : ℕ
hb : b ≠ 0
ha : a ≠ 0
⊢ a.factorization ≤ (a * b).factorization

Tactic:
· simp

Goal state after:
case inr
a b : ℕ
hb : b ≠ 0
ha : a ≠ 0
⊢ a.factorization ≤ (a * b).factorization
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x y : G
h : Commute x y
hy : IsOfFinOrder y
hdvd : ∀ (p : ℕ), Nat.Prime p → p ∣ orderOf x → p * orderOf x ∣ orderOf y
hoy : 0 < orderOf y
hxy : orderOf x ∣ orderOf y
⊢ orderOf (x * y) = orderOf y

Tactic:
apply orderOf_eq_of_pow_and_pow_div_prime hoy <;> simp only [Ne, ← orderOf_dvd_iff_pow_eq_one]

Goal state after:
case hx
G : Type u_1
inst✝ : Monoid G
x y : G
h : Commute x y
hy : IsOfFinOrder y
hdvd : ∀ (p : ℕ), Nat.Prime p → p ∣ orderOf x → p * orderOf x ∣ orderOf y
hoy : 0 < orderOf y
hxy : orderOf x ∣ orderOf y
⊢ orderOf (x * y) ∣ orderOf y

case hd
G : Type u_1
inst✝ : Monoid G
x y : G
h : Commute x y
hy : IsOfFinOrder y
hdvd : ∀ (p : ℕ), Nat.Prime p → p ∣ orderOf x → p * orderOf x ∣ orderOf y
hoy : 0 < orderOf y
hxy : orderOf x ∣ orderOf y
⊢ ∀ (p : ℕ), Nat.Prime p → p ∣ orderOf y → ¬orderOf (x * y) ∣ orderOf y / p
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:
· simp

Goal state after:
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: p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
⊢ ((p ^ n).choose k).factorization p = ((p ^ n).choose k).factorization p + k.factorization p - k.factorization p

Tactic:
rw [Nat.add_sub_cancel_right]

Goal state after:
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:
· simp

Goal state after:
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 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:
· simp

Goal state after:
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.GroupTheory.OrderOfElement

Goal state before:
pp: case neg.hg
R : Type u_6
inst✝¹ : Ring R
inst✝ : Nontrivial R
h : ¬ringChar R = 2
⊢ (-1) ^ 2 = 1

pp: case hg1
R : Type u_6
inst✝¹ : Ring R
inst✝ : Nontrivial R
h : ¬ringChar R = 2
⊢ -1 ≠ 1

Tactic:
· simp

Goal state after:
case hg1
R : Type u_6
inst✝¹ : Ring R
inst✝ : Nontrivial R
h : ¬ringChar R = 2
⊢ -1 ≠ 1
Module: Mathlib.Data.Nat.Factorization.Basic

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

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

Tactic:
· simp

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

Goal state before:
pp: case inr.inr.inr.inl
a b : ℕ
hab : a ∣ b
hb0 : b ≠ 0
ha0 : a ≠ 0
q : ℕ
pp : Prime q
ha : a / q ^ a.factorization q ≠ 0
hb : b / q ^ b.factorization q ≠ 0
⊢ (Finsupp.erase q a.factorization) q ≤ (Finsupp.erase q b.factorization) q

pp: case inr.inr.inr.inr
a b : ℕ
hab : a ∣ b
p : ℕ
pp : Prime p
hb0 : b ≠ 0
ha0 : a ≠ 0
ha : a / p ^ a.factorization p ≠ 0
hb : b / p ^ b.factorization p ≠ 0
q : ℕ
hqp : q ≠ p
⊢ (Finsupp.erase p a.factorization) q ≤ (Finsupp.erase p b.factorization) q

Tactic:
· simp

Goal state after:
case inr.inr.inr.inr
a b : ℕ
hab : a ∣ b
p : ℕ
pp : Prime p
hb0 : b ≠ 0
ha0 : a ≠ 0
ha : a / p ^ a.factorization p ≠ 0
hb : b / p ^ b.factorization p ≠ 0
q : ℕ
hqp : q ≠ p
⊢ (Finsupp.erase p a.factorization) q ≤ (Finsupp.erase p b.factorization) q
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case inl
a : ℕ
h : ∀ (p : ℕ), a / p ^ a.factorization p ∣ 0 / p ^ (factorization 0) p
⊢ a ∣ 0

pp: case inr
a b : ℕ
h : ∀ (p : ℕ), a / p ^ a.factorization p ∣ b / p ^ b.factorization p
hb0 : b ≠ 0
⊢ a ∣ b

Tactic:
· simp

Goal state after:
case inr
a b : ℕ
h : ∀ (p : ℕ), a / p ^ a.factorization p ∣ b / p ^ b.factorization p
hb0 : b ≠ 0
⊢ a ∣ b
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case inl
d : ℕ
⊢ d ∣ 0 ↔ ∀ (p k : ℕ), Prime p → p ^ k ∣ d → p ^ k ∣ 0

pp: case inr
n d : ℕ
hn : n ≠ 0
⊢ d ∣ n ↔ ∀ (p k : ℕ), Prime p → p ^ k ∣ d → p ^ k ∣ n

Tactic:
· simp

Goal state after:
case inr
n d : ℕ
hn : n ≠ 0
⊢ d ∣ n ↔ ∀ (p k : ℕ), Prime p → p ^ k ∣ d → p ^ k ∣ n
Module: Mathlib.Data.Nat.Multiplicity

Goal state before:
pp: n p : ℕ
hp : Prime p
hp' : _root_.Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
h2 : p * n + 1 ≤ p * (n + 1)
⊢ emultiplicity p (p * (n + 1))! = emultiplicity p (p * n)! + emultiplicity p (n + 1) + 1

Tactic:
have h3 : p * n + 1 ≤ p * (n + 1) + 1 := by lia

Goal state after:
n p : ℕ
hp : Prime p
hp' : _root_.Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
h2 : p * n + 1 ≤ p * (n + 1)
h3 : p * n + 1 ≤ p * (n + 1) + 1
⊢ emultiplicity p (p * (n + 1))! = emultiplicity p (p * n)! + emultiplicity p (n + 1) + 1
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
x : G
⊢ orderOf x⁻¹ = orderOf x

Tactic:
simp [orderOf_eq_orderOf_iff]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case inl
G : Type u_1
inst✝¹ : CommGroup G
inst✝ : IsMulTorsionFree G
⊢ orderOf 1 ≤ 1

pp: case inr
G : Type u_1
inst✝¹ : CommGroup G
inst✝ : IsMulTorsionFree G
g : G
ha : g ≠ 1
⊢ orderOf g ≤ 1

Tactic:
· simp

Goal state after:
case inr
G : Type u_1
inst✝¹ : CommGroup G
inst✝ : IsMulTorsionFree G
g : G
ha : g ≠ 1
⊢ orderOf g ≤ 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
⊢ #(n.divisors.biUnion fun m ↦ {x | orderOf x = m}) = #{x | x ^ n = 1}

Tactic:
congr; ext; simp [hn, orderOf_dvd_iff_pow_eq_one]

Goal state after:
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case inl
β : Type u_1
inst✝ : CommMonoid β
n : ℕ
f : ℕ → β
⊢ (gcd 0 n).primeFactors.prod f * (0 * n).primeFactors.prod f = (primeFactors 0).prod f * n.primeFactors.prod f

pp: case inr
β : Type u_1
inst✝ : CommMonoid β
m n : ℕ
f : ℕ → β
hm₀ : m ≠ 0
⊢ (m.gcd n).primeFactors.prod f * (m * n).primeFactors.prod f = m.primeFactors.prod f * n.primeFactors.prod f

Tactic:
· simp

Goal state after:
case inr
β : Type u_1
inst✝ : CommMonoid β
m n : ℕ
f : ℕ → β
hm₀ : m ≠ 0
⊢ (m.gcd n).primeFactors.prod f * (m * n).primeFactors.prod f = m.primeFactors.prod f * n.primeFactors.prod f
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case inr.inl
β : Type u_1
inst✝ : CommMonoid β
m : ℕ
f : ℕ → β
hm₀ : m ≠ 0
⊢ (m.gcd 0).primeFactors.prod f * (m * 0).primeFactors.prod f = m.primeFactors.prod f * (primeFactors 0).prod f

pp: case inr.inr
β : Type u_1
inst✝ : CommMonoid β
m n : ℕ
f : ℕ → β
hm₀ : m ≠ 0
hn₀ : n ≠ 0
⊢ (m.gcd n).primeFactors.prod f * (m * n).primeFactors.prod f = m.primeFactors.prod f * n.primeFactors.prod f

Tactic:
· simp

Goal state after:
case inr.inr
β : Type u_1
inst✝ : CommMonoid β
m n : ℕ
f : ℕ → β
hm₀ : m ≠ 0
hn₀ : n ≠ 0
⊢ (m.gcd n).primeFactors.prod f * (m * n).primeFactors.prod f = m.primeFactors.prod f * n.primeFactors.prod f
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case inl
p : ℕ
pp : Prime p
⊢ Icc 1 ((factorization 0) p) = {i ∈ Ico 1 0 | p ^ i ∣ 0}

pp: case inr
n p : ℕ
pp : Prime p
hn : n ≠ 0
⊢ Icc 1 (n.factorization p) = {i ∈ Ico 1 n | p ^ i ∣ n}

Tactic:
· simp

Goal state after:
case inr
n p : ℕ
pp : Prime p
hn : n ≠ 0
⊢ Icc 1 (n.factorization p) = {i ∈ Ico 1 n | p ^ i ∣ n}
Module: Mathlib.Data.Nat.Multiplicity

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

Tactic:
rw [Nat.add_sub_cancel_right]

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

Goal state before:
pp: case inr
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCommMonoid G
x : k[G]
g g' : G
h : ¬∃ d, g' = g + d
⊢ (x * single g 1 %ᵒᶠ g).coeff g' = 0

Tactic:
· rw [coeff_modOf_of_not_exists_add _ _ _ h, coeff_mul_single_of_forall_add_ne]
    simpa [eq_comm, add_comm] using h

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

Goal state before:
pp: case inl
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : AddCommMonoid G
inst✝ : IsCancelAdd G
x : k[G]
g d : G
⊢ (single g 1 * (x /ᵒᶠ g)).coeff (g + d) + (x %ᵒᶠ g).coeff (g + d) = x.coeff (g + d)

Tactic:
rw [coeff_modOf_self_add, add_zero, coeff_single_mul_add, one_mul, coeff_divOf]

Goal state after:
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: n : ℕ
p1 p2 : ↥n.primeFactors
hp : p1 ≠ p2
⊢ (↑p1).Coprime ↑p2

Tactic:
refine (Nat.coprime_primes ?_ ?_).mpr <| Subtype.coe_ne_coe.mpr hp

Goal state after:
case refine_1
n : ℕ
p1 p2 : ↥n.primeFactors
hp : p1 ≠ p2
⊢ Prime ↑p1

case refine_2
n : ℕ
p1 p2 : ↥n.primeFactors
hp : p1 ≠ p2
⊢ Prime ↑p2
Module: Mathlib.Algebra.Polynomial.Inductions

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
h : p = C (p.coeff 0)
⊢ p.divX = 0

Tactic:
by rw [h, divX_C]

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

Goal state before:
pp: case zero
R : Type u
inst✝ : Semiring R
⊢ (X ^ 0).divX = if 0 = 0 then 0 else X ^ (0 - 1)

pp: case succ
R : Type u
inst✝ : Semiring R
n✝ : ℕ
⊢ (X ^ (n✝ + 1)).divX = if n✝ + 1 = 0 then 0 else X ^ (n✝ + 1 - 1)

Tactic:
· simp

Goal state after:
case succ
R : Type u
inst✝ : Semiring R
n✝ : ℕ
⊢ (X ^ (n✝ + 1)).divX = if n✝ + 1 = 0 then 0 else X ^ (n✝ + 1 - 1)
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case inr.inl
G : Type u_1
inst✝² : Ring G
inst✝¹ : LinearOrder G
inst✝ : IsStrictOrderedRing G
h : |1| = 1
⊢ orderOf 1 ≤ 2

pp: case inr.inr
G : Type u_1
inst✝² : Ring G
inst✝¹ : LinearOrder G
inst✝ : IsStrictOrderedRing G
h : |(-1)| = 1
⊢ orderOf (-1) ≤ 2

Tactic:
· simp

Goal state after:
case inr.inr
G : Type u_1
inst✝² : Ring G
inst✝¹ : LinearOrder G
inst✝ : IsStrictOrderedRing G
h : |(-1)| = 1
⊢ orderOf (-1) ≤ 2
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case mp
R : Type u_6
inst✝¹ : NonAssocRing R
p : ℕ
inst✝ : Fintype R
hn : card R = p
hR : ∀ i < p, ↑i = 0 → i = 0
n : ℕ
H : ↑p = 0
h : ↑(n % p + p * (n / p)) = 0
⊢ p ∣ n

Tactic:
Nat.cast_add,

Goal state after:
case mp
R : Type u_6
inst✝¹ : NonAssocRing R
p : ℕ
inst✝ : Fintype R
hn : card R = p
hR : ∀ i < p, ↑i = 0 → i = 0
n : ℕ
H : ↑p = 0
h : ↑(n % p) + ↑(p * (n / p)) = 0
⊢ p ∣ n
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case mpr
R : Type u_6
inst✝¹ : NonAssocRing R
p : ℕ
inst✝ : Fintype R
hn : card R = p
hR : ∀ i < p, ↑i = 0 → i = 0
n : ℕ
H : ↑p = 0
⊢ p ∣ n → ↑n = 0

Tactic:
rintro ⟨n, rfl⟩

Goal state after:
case mpr
R : Type u_6
inst✝¹ : NonAssocRing R
p : ℕ
inst✝ : Fintype R
hn : card R = p
hR : ∀ i < p, ↑i = 0 → i = 0
H : ↑p = 0
n : ℕ
⊢ ↑(p * n) = 0
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: case inl
R : Type u
inst✝ : CommSemiring R
p : ℕ
f : R[X]
hp : p = 0
⊢ ((expand R p) f).natDegree = f.natDegree * p

Tactic:
hp,

Goal state after:
case inl
R : Type u
inst✝ : CommSemiring R
p : ℕ
f : R[X]
hp : p = 0
⊢ ((expand R 0) f).natDegree = f.natDegree * 0
Module: Mathlib.Algebra.Polynomial.RingDivision

Goal state before:
pp: case pos
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
hp : p = 0
⊢ (p * q).trailingDegree = p.trailingDegree + q.trailingDegree

Tactic:
hp,

Goal state after:
case pos
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
hp : p = 0
⊢ (0 * q).trailingDegree = trailingDegree 0 + q.trailingDegree
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: case inl
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
hdeg : (p * 0).natDegree ≤ p.natDegree
⊢ p * 0 = p * C (p * 0).leadingCoeff

pp: case inr
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
r : R[X]
hdeg : (p * r).natDegree ≤ p.natDegree
hr : r ≠ 0
⊢ p * r = p * C (p * r).leadingCoeff

Tactic:
· simp

Goal state after:
case inr
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
r : R[X]
hdeg : (p * r).natDegree ≤ p.natDegree
hr : r ≠ 0
⊢ p * r = p * C (p * r).leadingCoeff
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:
· simp

Goal state after:
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.Derivative

Goal state before:
pp: R : Type u
inst✝ : Semiring R
a : R
n : ℕ
⊢ (monomial n) (a * ↑(n + 1)) = (monomial n) (a * (↑n + 1))

Tactic:
Nat.cast_add,

Goal state after:
R : Type u
inst✝ : Semiring R
a : R
n : ℕ
⊢ (monomial n) (a * (↑n + ↑1)) = (monomial n) (a * (↑n + 1))
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:
rw [dif_neg h]

Goal state after:
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:
rw [dif_neg h]

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

Goal state before:
pp: case hp
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b : R
ha : a ≠ 0
hab : IsRelPrime a b
⊢ (C a * X + C b).degree = 1

pp: case hc
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b : R
ha : a ≠ 0
hab : IsRelPrime a b
⊢ IsRelPrime ((C a * X + C b).coeff 0) ((C a * X + C b).coeff 1)

Tactic:
· compute_degree!

Goal state after:
case hc
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b : R
ha : a ≠ 0
hab : IsRelPrime a b
⊢ IsRelPrime ((C a * X + C b).coeff 0) ((C a * X + C b).coeff 1)
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: case monomial.monomial.succ.succ
R : Type u
inst✝ : Semiring R
a b : R
m n : ℕ
⊢ (monomial (m + 1 + (n + 1) - 1)) (a * (b * ↑(m + 1))) + (monomial (m + 1 + (n + 1) - 1)) (a * (b * ↑(n + 1))) =
    (monomial (m + 1 - 1 + (n + 1))) (a * (b * ↑(m + 1))) + (monomial (m + 1 + (n + 1 - 1))) (a * (b * ↑(n + 1)))

Tactic:
| succ n =>

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

Goal state before:
pp: case inl
R : Type u
inst✝¹ : CommRing R
p n : ℕ
inst✝ : ExpChar R p
r : R
⊢ rootMultiplicity r ((expand R (p ^ n)) 0) = p ^ n * rootMultiplicity (r ^ p ^ n) 0

pp: case inr
R : Type u
inst✝¹ : CommRing R
p n : ℕ
inst✝ : ExpChar R p
f : R[X]
r : R
h0 : f ≠ 0
⊢ rootMultiplicity r ((expand R (p ^ n)) f) = p ^ n * rootMultiplicity (r ^ p ^ n) f

Tactic:
· simp

Goal state after:
case inr
R : Type u
inst✝¹ : CommRing R
p n : ℕ
inst✝ : ExpChar R p
f : R[X]
r : R
h0 : f ≠ 0
⊢ rootMultiplicity r ((expand R (p ^ n)) f) = p ^ n * rootMultiplicity (r ^ p ^ n) f
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
f g q r : R[X]
hg : g.Monic
h : r + g * q = f ∧ r.degree < g.degree
a✝ : Nontrivial R
h₁ : r - f %ₘ g = -g * (q - f /ₘ g)
h₂ : (r - f %ₘ g).degree = (g * (q - f /ₘ g)).degree
h₄ : (r - f %ₘ g).degree < g.degree
hqf : ¬q - f /ₘ g = 0
⊢ g.degree ≤ g.degree + (q - f /ₘ g).degree

Tactic:
by
            rw [degree_eq_natDegree hg.ne_zero, degree_eq_natDegree hqf]
            norm_cast
            exact Nat.le_add_right _ _

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
k : ℕ
⊢ (⇑derivative)^[k] (map f p) = map f ((⇑derivative)^[k] p)

Tactic:
induction k generalizing p with
  | zero => simp
  | succ k ih =>
    simp only [ih, Function.iterate_succ, Polynomial.derivative_map, Function.comp_apply]

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
f g q r : R[X]
hg : g.Monic
h : r + g * q = f ∧ r.degree < g.degree
a✝ : Nontrivial R
h₁ : r - f %ₘ g = -g * (q - f /ₘ g)
h₂ : (r - f %ₘ g).degree = (g * (q - f /ₘ g)).degree
h₄ : (r - f %ₘ g).degree < g.degree
hqf : ¬q - f /ₘ g = 0
⊢ g.degree + (q - f /ₘ g).degree = (r - f %ₘ g).degree

Tactic:
by rw [h₂, degree_mul']; simpa [Monic.def.1 hg]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Multiset A
x : A
hx : x ∈ s
p : R[X]
hp : (mapAlg R A) p = (Multiset.map (fun x ↦ X - C x) s).prod
⊢ (aeval x) ((mapAlg R A) p) = 0

Tactic:
hp,

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Multiset A
x : A
hx : x ∈ s
p : R[X]
hp : (mapAlg R A) p = (Multiset.map (fun x ↦ X - C x) s).prod
⊢ (aeval x) (Multiset.map (fun x ↦ X - C x) s).prod = 0