mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: 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
⊢ (x * y) ^ orderOf y = 1

pp: 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 → (x * y) ^ (orderOf y / p) ≠ 1

Tactic:
<;>

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
⊢ (x * y) ^ orderOf y = 1

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 → (x * y) ^ (orderOf y / p) ≠ 1
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case hk
G : Type u_1
inst✝ : Monoid G
x : G
n p : ℕ
hp : Fact (Nat.Prime p)
hnot : ¬x ^ p ^ n = 1
hfin : x ^ p ^ (n + 1) = 1
⊢ ¬IsPeriodicPt (fun x_1 ↦ x * x_1) (p ^ n) 1

pp: case hk1
G : Type u_1
inst✝ : Monoid G
x : G
n p : ℕ
hp : Fact (Nat.Prime p)
hnot : ¬x ^ p ^ n = 1
hfin : x ^ p ^ (n + 1) = 1
⊢ IsPeriodicPt (fun x_1 ↦ x * x_1) (p ^ (n + 1)) 1

Tactic:
<;>

Goal state after:
case hk
G : Type u_1
inst✝ : Monoid G
x : G
n p : ℕ
hp : Fact (Nat.Prime p)
hnot : ¬x ^ p ^ n = 1
hfin : x ^ p ^ (n + 1) = 1
⊢ ¬IsPeriodicPt (fun x_1 ↦ x * x_1) (p ^ n) 1

case hk1
G : Type u_1
inst✝ : Monoid G
x : G
n p : ℕ
hp : Fact (Nat.Prime p)
hnot : ¬x ^ p ^ n = 1
hfin : x ^ p ^ (n + 1) = 1
⊢ IsPeriodicPt (fun x_1 ↦ x * x_1) (p ^ (n + 1)) 1
Module: Mathlib.Algebra.CharP.Lemmas

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : ℕ
hp : Nat.Prime p
x y : R
h : Commute x y
n : ℕ
⊢ ∑ m ∈ range (p ^ n + 1), x ^ m * y ^ (p ^ n - m) * ↑((p ^ n).choose m) =
    ∑ k ∈ Icc 0 (p ^ n), x ^ k * y ^ (p ^ n - k) * ↑((p ^ n).choose k)

Tactic:
← Nat.Ico_zero_eq_range,

Goal state after:
R : Type u_1
inst✝ : Semiring R
p : ℕ
hp : Nat.Prime p
x y : R
h : Commute x y
n : ℕ
⊢ ∑ m ∈ Ico 0 (p ^ n + 1), x ^ m * y ^ (p ^ n - m) * ↑((p ^ n).choose m) =
    ∑ k ∈ Icc 0 (p ^ n), x ^ k * y ^ (p ^ n - k) * ↑((p ^ n).choose k)
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : LeftCancelMonoid 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
⊢ Set.InjOn (fun n ↦ x ^ n) (Set.Ioi 0)

Tactic:
exact Set.injOn_of_injective this

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

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

Tactic:
Classical.not_not

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : ℕ
hp : Nat.Prime p
x y : R
h : Commute x y
n k : ℕ
hk✝ : k ∈ Ioo 0 (p ^ n)
hk₀ : 0 < k
hk : k < p ^ n
⊢ k ≠ 0

pp: R : Type u_1
inst✝ : Semiring R
p : ℕ
hp : Nat.Prime p
x y : R
h : Commute x y
n k : ℕ
hk✝ : k ∈ Ioo 0 (p ^ n)
hk₀ : 0 < k
hk : k < p ^ n
⊢ k ≠ p ^ n

Tactic:
<;>

Goal state after:
R : Type u_1
inst✝ : Semiring R
p : ℕ
hp : Nat.Prime p
x y : R
h : Commute x y
n k : ℕ
hk✝ : k ∈ Ioo 0 (p ^ n)
hk₀ : 0 < k
hk : k < p ^ n
⊢ k ≠ 0

R : Type u_1
inst✝ : Semiring R
p : ℕ
hp : Nat.Prime p
x y : R
h : Commute x y
n k : ℕ
hk✝ : k ∈ Ioo 0 (p ^ n)
hk₀ : 0 < k
hk : k < p ^ n
⊢ k ≠ p ^ n
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
this : Injective fun n ↦ x ^ n
⊢ Set.InjOn (fun n ↦ x ^ n) (Set.Ioi 0)

Tactic:
exact Set.injOn_of_injective this

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
this : ¬¬IsOfFinOrder x
⊢ IsOfFinOrder x

Tactic:
Classical.not_not

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 : IsOfFinOrder x
⊢ IsOfFinOrder x
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case inl
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
g : G
h : |g|ₘ = g ∧ 1 ≤ g
⊢ zpowers |g|ₘ = zpowers g

pp: case inr
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
g : G
h : |g|ₘ = g⁻¹ ∧ g < 1
⊢ zpowers |g|ₘ = zpowers g

Tactic:
<;>

Goal state after:
case inl
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
g : G
h : |g|ₘ = g ∧ 1 ≤ g
⊢ zpowers |g|ₘ = zpowers g

case inr
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
g : G
h : |g|ₘ = g⁻¹ ∧ g < 1
⊢ zpowers |g|ₘ = zpowers g
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
g : G
⊢ zpowers |g|ₘ = zpowers g

Tactic:
rcases mabs_cases g with h | h <;> simp only [h, zpowers_inv]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case inl
G : Type u_1
inst✝ : Group G
x : G
hx : ¬IsOfFinOrder x
⊢ zpowers x = zpowers x

pp: case inr
G : Type u_1
inst✝ : Group G
x : G
hx : ¬IsOfFinOrder x
⊢ zpowers x = zpowers x⁻¹

Tactic:
<;>

Goal state after:
case inl
G : Type u_1
inst✝ : Group G
x : G
hx : ¬IsOfFinOrder x
⊢ zpowers x = zpowers x

case inr
G : Type u_1
inst✝ : Group G
x : G
hx : ¬IsOfFinOrder x
⊢ zpowers x = zpowers x⁻¹
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case inl
G : Type u_1
inst✝ : Group G
x : G
hx : ¬IsOfFinOrder x
k : ℤ
h✝ : zpowers x = zpowers (x ^ k)
hx_mem : x ∈ zpowers (x ^ k)
hy_mem : x ^ k ∈ zpowers x
l : ℤ
hl : x ^ (k * l) = x ^ 1
h1 : k * l = 1
h : k = 1 ∧ l = 1
⊢ x = x ^ k ∨ x⁻¹ = x ^ k

pp: case inr
G : Type u_1
inst✝ : Group G
x : G
hx : ¬IsOfFinOrder x
k : ℤ
h✝ : zpowers x = zpowers (x ^ k)
hx_mem : x ∈ zpowers (x ^ k)
hy_mem : x ^ k ∈ zpowers x
l : ℤ
hl : x ^ (k * l) = x ^ 1
h1 : k * l = 1
h : k = -1 ∧ l = -1
⊢ x = x ^ k ∨ x⁻¹ = x ^ k

Tactic:
<;>

Goal state after:
case inl
G : Type u_1
inst✝ : Group G
x : G
hx : ¬IsOfFinOrder x
k : ℤ
h✝ : zpowers x = zpowers (x ^ k)
hx_mem : x ∈ zpowers (x ^ k)
hy_mem : x ^ k ∈ zpowers x
l : ℤ
hl : x ^ (k * l) = x ^ 1
h1 : k * l = 1
h : k = 1 ∧ l = 1
⊢ x = x ^ k ∨ x⁻¹ = x ^ k

case inr
G : Type u_1
inst✝ : Group G
x : G
hx : ¬IsOfFinOrder x
k : ℤ
h✝ : zpowers x = zpowers (x ^ k)
hx_mem : x ∈ zpowers (x ^ k)
hy_mem : x ^ k ∈ zpowers x
l : ℤ
hl : x ^ (k * l) = x ^ 1
h1 : k * l = 1
h : k = -1 ∧ l = -1
⊢ x = x ^ k ∨ x⁻¹ = x ^ k
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case zero
n b : ℕ
hn : n ≠ 0
i : ℕ
h2 : 1 ≤ i
h : i < n
pp : Prime 0
hb : n < 0 ^ b
h1 : n = 0
⊢ i < b

Tactic:
exact (hn h1).elim

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

Goal state before:
pp: case refine_1
p n k : ℕ
hp : Prime p
h : p ∣ (p ^ n).choose k
⊢ k ≠ 0

pp: case refine_2
p n k : ℕ
hp : Prime p
h : p ∣ (p ^ n).choose k
⊢ k ≠ p ^ n

Tactic:
<;>

Goal state after:
case refine_1
p n k : ℕ
hp : Prime p
h : p ∣ (p ^ n).choose k
⊢ k ≠ 0

case refine_2
p n k : ℕ
hp : Prime p
h : p ∣ (p ^ n).choose k
⊢ k ≠ p ^ n
Module: Mathlib.Data.Nat.Multiplicity

Goal state before:
pp: case refine_1
p n : ℕ
hp : Prime p
h : p ∣ (p ^ n).choose 0
⊢ False

pp: case refine_2
p n : ℕ
hp : Prime p
h : p ∣ (p ^ n).choose (p ^ n)
⊢ False

Tactic:
<;>

Goal state after:
case refine_1
p n : ℕ
hp : Prime p
h : p ∣ (p ^ n).choose 0
⊢ False

case refine_2
p n : ℕ
hp : Prime p
h : p ∣ (p ^ n).choose (p ^ n)
⊢ False
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_6
inst✝ : Group G
s : Subgroup G
x : G
hx : x ∈ s
⊢ orderOf x ∣ Nat.card ↥s

Tactic:
simpa using orderOf_dvd_natCard (⟨x, hx⟩ : s)

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

Goal state before:
pp: 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
⊢ ¬¬∃ g₂, g' = g + g₂

Tactic:
Classical.not_not

Goal state after:
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
⊢ ∃ g₂, g' = g + g₂
Module: Mathlib.Algebra.Polynomial.Inductions

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

pp: case succ
R : Type u
inst✝ : Semiring R
p : R[X]
n✝ : ℕ
⊢ (p.divX * X + C (p.coeff 0)).coeff (n✝ + 1) = p.coeff (n✝ + 1)

Tactic:
<;>

Goal state after:
case zero
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ (p.divX * X + C (p.coeff 0)).coeff 0 = p.coeff 0

case succ
R : Type u
inst✝ : Semiring R
p : R[X]
n✝ : ℕ
⊢ (p.divX * X + C (p.coeff 0)).coeff (n✝ + 1) = p.coeff (n✝ + 1)
Module: Mathlib.Algebra.Polynomial.Inductions

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

pp: case succ
R : Type u
inst✝ : Semiring R
p : R[X]
n✝ : ℕ
⊢ (X * p.divX + C (p.coeff 0)).coeff (n✝ + 1) = p.coeff (n✝ + 1)

Tactic:
<;>

Goal state after:
case zero
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ (X * p.divX + C (p.coeff 0)).coeff 0 = p.coeff 0

case succ
R : Type u
inst✝ : Semiring R
p : R[X]
n✝ : ℕ
⊢ (X * p.divX + C (p.coeff 0)).coeff (n✝ + 1) = p.coeff (n✝ + 1)
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case zero
p : ℕ
⊢ #({x ∈ Ioc 0 0 | p ∣ x}) = 0 / p

pp: case succ
p n✝ : ℕ
a✝ : #({x ∈ Ioc 0 n✝ | p ∣ x}) = n✝ / p
⊢ #({x ∈ Ioc 0 (n✝ + 1) | p ∣ x}) = (n✝ + 1) / p

Tactic:
<;>

Goal state after:
case zero
p : ℕ
⊢ #({x ∈ Ioc 0 0 | p ∣ x}) = 0 / p

case succ
p n✝ : ℕ
a✝ : #({x ∈ Ioc 0 n✝ | p ∣ x}) = n✝ / p
⊢ #({x ∈ Ioc 0 (n✝ + 1) | p ∣ x}) = (n✝ + 1) / p
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: case pos
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : p ∣ n
hn : n / p ∉ f.support
h✝ : p * (n / p) = n
⊢ 0 = 0

pp: case neg
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : p ∣ n
hn : n / p ∉ f.support
h✝ : ¬p * (n / p) = n
⊢ 0 = 0

Tactic:
<;>

Goal state after:
case pos
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : p ∣ n
hn : n / p ∉ f.support
h✝ : p * (n / p) = n
⊢ 0 = 0

case neg
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : p ∣ n
hn : n / p ∉ f.support
h✝ : ¬p * (n / p) = n
⊢ 0 = 0
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: case neg
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : ¬p ∣ n
⊢ (∑ x ∈ f.support, if p * x = n then f.coeff x else 0) = 0

Tactic:
rw [Finset.sum_eq_zero]
    intro k _
    rw [if_neg]
    exact fun hkn => h ⟨k, hkn.symm⟩

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

Goal state before:
pp: case hf
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p✝ p q : R[X]
⊢ ∀ (i : ℕ), C (0 * ↑i) * X ^ (i - 1) = 0

pp: case h_add
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p✝ p q : R[X]
⊢ ∀ (a : ℕ) (b₁ b₂ : R), C ((b₁ + b₂) * ↑a) * X ^ (a - 1) = C (b₁ * ↑a) * X ^ (a - 1) + C (b₂ * ↑a) * X ^ (a - 1)

Tactic:
<;>

Goal state after:
case hf
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p✝ p q : R[X]
⊢ ∀ (i : ℕ), C (0 * ↑i) * X ^ (i - 1) = 0

case h_add
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p✝ p q : R[X]
⊢ ∀ (a : ℕ) (b₁ b₂ : R), C ((b₁ + b₂) * ↑a) * X ^ (a - 1) = C (b₁ * ↑a) * X ^ (a - 1) + C (b₂ * ↑a) * X ^ (a - 1)
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]
⊢ (p.sum fun n a_1 ↦ C (a * a_1 * ↑n) * X ^ (n - 1)) = a • p.sum fun n a ↦ C (a * ↑n) * X ^ (n - 1)

pp: case hf
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]
⊢ ∀ (i : ℕ), C (0 * ↑i) * X ^ (i - 1) = 0

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]
⊢ (p.sum fun n a_1 ↦ C (a * a_1 * ↑n) * X ^ (n - 1)) = a • p.sum fun n a ↦ C (a * ↑n) * X ^ (n - 1)

case hf
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]
⊢ ∀ (i : ℕ), C (0 * ↑i) * X ^ (i - 1) = 0
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: case pos
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p : ℕ
f : R →+* S
q : R[X]
hp : ¬p = 0
n✝ : ℕ
h✝ : p ∣ n✝
⊢ f (q.coeff (n✝ / p)) = (map f q).coeff (n✝ / p)

pp: case neg
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p : ℕ
f : R →+* S
q : R[X]
hp : ¬p = 0
n✝ : ℕ
h✝ : ¬p ∣ n✝
⊢ f 0 = 0

Tactic:
<;>

Goal state after:
case pos
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p : ℕ
f : R →+* S
q : R[X]
hp : ¬p = 0
n✝ : ℕ
h✝ : p ∣ n✝
⊢ f (q.coeff (n✝ / p)) = (map f q).coeff (n✝ / p)

case neg
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p : ℕ
f : R →+* S
q : R[X]
hp : ¬p = 0
n✝ : ℕ
h✝ : ¬p ∣ n✝
⊢ f 0 = 0
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: case e'_2
R : Type u
inst✝ : Semiring R
n : ℕ
⊢ X ^ n = C 1 * X ^ n

pp: case e'_3
R : Type u
inst✝ : Semiring R
n : ℕ
⊢ ↑n = 1 * ↑n

Tactic:
<;>

Goal state after:
case e'_2
R : Type u
inst✝ : Semiring R
n : ℕ
⊢ X ^ n = C 1 * X ^ n

case e'_3
R : Type u
inst✝ : Semiring R
n : ℕ
⊢ ↑n = 1 * ↑n
Module: Mathlib.Algebra.Polynomial.RingDivision

Goal state before:
pp: case inl.a
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p f g : R[X]
hc : IsRelPrime (f.coeff 0 * g.coeff 0) (f.coeff 0 * g.coeff 1)
h : p = f * g
H : f.degree ≤ g.degree
hg : g.degree = 1
hf : f = C (f.coeff 0)
⊢ f.coeff 0 ∣ f.coeff 0 * g.coeff 0

pp: case inl.a
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p f g : R[X]
hc : IsRelPrime (f.coeff 0 * g.coeff 0) (f.coeff 0 * g.coeff 1)
h : p = f * g
H : f.degree ≤ g.degree
hg : g.degree = 1
hf : f = C (f.coeff 0)
⊢ f.coeff 0 ∣ f.coeff 0 * g.coeff 1

Tactic:
<;>

Goal state after:
case inl.a
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p f g : R[X]
hc : IsRelPrime (f.coeff 0 * g.coeff 0) (f.coeff 0 * g.coeff 1)
h : p = f * g
H : f.degree ≤ g.degree
hg : g.degree = 1
hf : f = C (f.coeff 0)
⊢ f.coeff 0 ∣ f.coeff 0 * g.coeff 0

case inl.a
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p f g : R[X]
hc : IsRelPrime (f.coeff 0 * g.coeff 0) (f.coeff 0 * g.coeff 1)
h : p = f * g
H : f.degree ≤ g.degree
hg : g.degree = 1
hf : f = C (f.coeff 0)
⊢ f.coeff 0 ∣ f.coeff 0 * g.coeff 1
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
hp0 : p ≠ 0
h0q : 0 < q.degree
this✝ : DecidableEq R := Classical.decEq R
hq : q.Monic
hpq : ¬p.degree < q.degree
this : Nontrivial R
⊢ (p /ₘ q).degree < p.degree

Tactic:
rw [← degree_add_divByMonic hq (not_lt.1 hpq), degree_eq_natDegree hq.ne_zero,
        degree_eq_natDegree (mt (divByMonic_eq_zero_iff hq).1 hpq)]

Goal state after:
R : Type u
inst✝ : Ring R
p q : R[X]
hp0 : p ≠ 0
h0q : 0 < q.degree
this✝ : DecidableEq R := Classical.decEq R
hq : q.Monic
hpq : ¬p.degree < q.degree
this : Nontrivial R
⊢ ↑(p /ₘ q).natDegree < ↑q.natDegree + ↑(p /ₘ q).natDegree
Module: Mathlib.Algebra.Polynomial.RingDivision

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
p : R[X]
hp : p ≠ 0
this : Decidable (∃ x, p.IsRoot x)
h : ∃ x, p.IsRoot x
x : R
hx : p.IsRoot x
hpd : 0 < p.degree
hd0 : p /ₘ (X - C x) ≠ 0
wf : (p /ₘ (X - C x)).degree < p.degree
t : Multiset R
htd : ↑t.card ≤ (p /ₘ (X - C x)).degree
htr : ∀ (a : R), count a t = rootMultiplicity a (p /ₘ (X - C x))
hdeg : (X - C x).degree ≤ p.degree
hdiv0 : p /ₘ (X - C x) ≠ 0
a : R
⊢ count a (x ::ₘ t) = rootMultiplicity a ((X - C x) * (p /ₘ (X - C x)))

Tactic:
rw [rootMultiplicity_mul (mul_ne_zero (X_sub_C_ne_zero x) hdiv0),
            rootMultiplicity_X_sub_C, ← htr a]

Goal state after:
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
p : R[X]
hp : p ≠ 0
this : Decidable (∃ x, p.IsRoot x)
h : ∃ x, p.IsRoot x
x : R
hx : p.IsRoot x
hpd : 0 < p.degree
hd0 : p /ₘ (X - C x) ≠ 0
wf : (p /ₘ (X - C x)).degree < p.degree
t : Multiset R
htd : ↑t.card ≤ (p /ₘ (X - C x)).degree
htr : ∀ (a : R), count a t = rootMultiplicity a (p /ₘ (X - C x))
hdeg : (X - C x).degree ≤ p.degree
hdiv0 : p /ₘ (X - C x) ≠ 0
a : R
⊢ count a (x ::ₘ t) = (if a = x then 1 else 0) + count a t
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: case zero
R : Type u
inst✝ : Semiring R
n : ℕ
f : R[X]
⊢ (⇑derivative)^[0] (↑n * f) = ↑n * (⇑derivative)^[0] f

pp: case succ
R : Type u
inst✝ : Semiring R
n n✝ : ℕ
a✝ : ∀ {f : R[X]}, (⇑derivative)^[n✝] (↑n * f) = ↑n * (⇑derivative)^[n✝] f
f : R[X]
⊢ (⇑derivative)^[n✝ + 1] (↑n * f) = ↑n * (⇑derivative)^[n✝ + 1] f

Tactic:
<;>

Goal state after:
case zero
R : Type u
inst✝ : Semiring R
n : ℕ
f : R[X]
⊢ (⇑derivative)^[0] (↑n * f) = ↑n * (⇑derivative)^[0] f

case succ
R : Type u
inst✝ : Semiring R
n n✝ : ℕ
a✝ : ∀ {f : R[X]}, (⇑derivative)^[n✝] (↑n * f) = ↑n * (⇑derivative)^[n✝] f
f : R[X]
⊢ (⇑derivative)^[n✝ + 1] (↑n * f) = ↑n * (⇑derivative)^[n✝ + 1] f
Module: Mathlib.Algebra.Polynomial.Eval.SMul

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
g : R →+* S
p : R[X]
x : S
s : R
A : p.natDegree < p.natDegree.succ
B : (s • p).natDegree < p.natDegree.succ
⊢ ∑ a ∈ range p.natDegree.succ, g ((s • p).coeff a) * x ^ a = g s * ∑ a ∈ range p.natDegree.succ, g (p.coeff a) * x ^ a

pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
g : R →+* S
p : R[X]
x : S
s : R
A : p.natDegree < p.natDegree.succ
B : (s • p).natDegree < p.natDegree.succ
⊢ ∀ (n : ℕ), g 0 * x ^ n = 0

pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
g : R →+* S
p : R[X]
x : S
s : R
A : p.natDegree < p.natDegree.succ
B : (s • p).natDegree < p.natDegree.succ
⊢ ∀ (n : ℕ), g 0 * x ^ n = 0

Tactic:
<;>

Goal state after:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
g : R →+* S
p : R[X]
x : S
s : R
A : p.natDegree < p.natDegree.succ
B : (s • p).natDegree < p.natDegree.succ
⊢ ∑ a ∈ range p.natDegree.succ, g ((s • p).coeff a) * x ^ a = g s * ∑ a ∈ range p.natDegree.succ, g (p.coeff a) * x ^ a

R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
g : R →+* S
p : R[X]
x : S
s : R
A : p.natDegree < p.natDegree.succ
B : (s • p).natDegree < p.natDegree.succ
⊢ ∀ (n : ℕ), g 0 * x ^ n = 0

R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
g : R →+* S
p : R[X]
x : S
s : R
A : p.natDegree < p.natDegree.succ
B : (s • p).natDegree < p.natDegree.succ
⊢ ∀ (n : ℕ), g 0 * x ^ n = 0
Module: Mathlib.Algebra.Polynomial.CancelLeads

Goal state before:
pp: case a
R : Type u_1
inst✝ : Ring R
p q : R[X]
comm : p.leadingCoeff * q.leadingCoeff = q.leadingCoeff * p.leadingCoeff
h : p.natDegree ≤ q.natDegree
hq : 0 < q.natDegree
hp : ¬p = 0
h0 : (C p.leadingCoeff * q + -(C q.leadingCoeff * X ^ (q.natDegree - p.natDegree) * p)).natDegree = q.natDegree
⊢ (C p.leadingCoeff * q + -(C q.leadingCoeff * X ^ (q.natDegree - p.natDegree) * p)).coeff
      (C p.leadingCoeff * q + -(C q.leadingCoeff * X ^ (q.natDegree - p.natDegree) * p)).natDegree =
    0

Tactic:
h0,

Goal state after:
case a
R : Type u_1
inst✝ : Ring R
p q : R[X]
comm : p.leadingCoeff * q.leadingCoeff = q.leadingCoeff * p.leadingCoeff
h : p.natDegree ≤ q.natDegree
hq : 0 < q.natDegree
hp : ¬p = 0
h0 : (C p.leadingCoeff * q + -(C q.leadingCoeff * X ^ (q.natDegree - p.natDegree) * p)).natDegree = q.natDegree
⊢ (C p.leadingCoeff * q + -(C q.leadingCoeff * X ^ (q.natDegree - p.natDegree) * p)).coeff q.natDegree = 0
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p : R[X]
⊢ p /ₘ 1 = p

Tactic:
conv_rhs => rw [← modByMonic_add_div p 1]; simp

Goal state after:
Module: Mathlib.Order.Filter.Finite

Goal state before:
pp: case mp
α : Type u
s : Set (Set α)
U : Set α
⊢ U ∈ generate s → ∃ t ⊆ s, t.Finite ∧ ⋂₀ t ⊆ U

pp: case mpr
α : Type u
s : Set (Set α)
U : Set α
⊢ (∃ t ⊆ s, t.Finite ∧ ⋂₀ t ⊆ U) → U ∈ generate s

Tactic:
<;>

Goal state after:
case mp
α : Type u
s : Set (Set α)
U : Set α
⊢ U ∈ generate s → ∃ t ⊆ s, t.Finite ∧ ⋂₀ t ⊆ U

case mpr
α : Type u
s : Set (Set α)
U : Set α
⊢ (∃ t ⊆ s, t.Finite ∧ ⋂₀ t ⊆ U) → U ∈ generate s
Module: Mathlib.Order.Filter.CountablyGenerated

Goal state before:
pp: case h.right.a
α : Type u_1
s : ℕ → Set α
⊢ ⨅ i, 𝓟 (s i) ≤ ⨅ i, 𝓟 (⋂ m, ⋂ (_ : m ≤ i), s m)

pp: case a
α : Type u_1
s : ℕ → Set α
⊢ ⨅ i, 𝓟 (⋂ m, ⋂ (_ : m ≤ i), s m) ≤ ⨅ i, 𝓟 (s i)

Tactic:
<;>

Goal state after:
case h.right.a
α : Type u_1
s : ℕ → Set α
⊢ ⨅ i, 𝓟 (s i) ≤ ⨅ i, 𝓟 (⋂ m, ⋂ (_ : m ≤ i), s m)

case a
α : Type u_1
s : ℕ → Set α
⊢ ⨅ i, 𝓟 (⋂ m, ⋂ (_ : m ≤ i), s m) ≤ ⨅ i, 𝓟 (s i)
Module: Mathlib.Order.Filter.CountablyGenerated

Goal state before:
pp: case h.right.a
α : Type u_1
s : ℕ → Set α
⊢ ∀ (i : ℕ), ⨅ i, 𝓟 (s i) ≤ 𝓟 (⋂ m, ⋂ (_ : m ≤ i), s m)

pp: case a
α : Type u_1
s : ℕ → Set α
⊢ ∀ (i : ℕ), ⨅ i, 𝓟 (⋂ m, ⋂ (_ : m ≤ i), s m) ≤ 𝓟 (s i)

Tactic:
<;>

Goal state after:
case h.right.a
α : Type u_1
s : ℕ → Set α
⊢ ∀ (i : ℕ), ⨅ i, 𝓟 (s i) ≤ 𝓟 (⋂ m, ⋂ (_ : m ≤ i), s m)

case a
α : Type u_1
s : ℕ → Set α
⊢ ∀ (i : ℕ), ⨅ i, 𝓟 (⋂ m, ⋂ (_ : m ≤ i), s m) ≤ 𝓟 (s i)
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: case e_a
R : Type u
inst✝¹ : Semiring R
inst✝ : IsAddTorsionFree R
p : R[X]
hp : ¬p.natDegree = 0
⊢ p.natDegree - 1 + 1 = p.natDegree

pp: case neg.e_a
R : Type u
inst✝¹ : Semiring R
inst✝ : IsAddTorsionFree R
p : R[X]
hp : ¬p.natDegree = 0
⊢ p.natDegree - 1 + 1 = p.natDegree

Tactic:
<;>

Goal state after:
case e_a
R : Type u
inst✝¹ : Semiring R
inst✝ : IsAddTorsionFree R
p : R[X]
hp : ¬p.natDegree = 0
⊢ p.natDegree - 1 + 1 = p.natDegree

case neg.e_a
R : Type u
inst✝¹ : Semiring R
inst✝ : IsAddTorsionFree R
p : R[X]
hp : ¬p.natDegree = 0
⊢ p.natDegree - 1 + 1 = p.natDegree