mathlib-initiative/mathlib-tactics huggingface dataset:
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:
·

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

Goal state after:
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
Module: Mathlib.Data.Nat.Factorization.Basic

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

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.GroupTheory.OrderOfElement

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

pp: 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

Tactic:
·

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

Goal state before:
pp: p n k b : ℕ
hp : Prime p
hkn : k ≤ n
hnb : log p n < b
this : n - k + k = n
⊢ n = n - k + k

pp: p n k b : ℕ
hp : Prime p
hkn : k ≤ n
hnb : log p n < b
this : n - k + k = n
⊢ log p (n - k + k) < b

Tactic:
·

Goal state after:
p n k b : ℕ
hp : Prime p
hkn : k ≤ n
hnb : log p n < b
this : n - k + k = n
⊢ n = n - k + k
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:
·

Goal state after:
case inl
p : ℕ
pp : Prime p
⊢ Icc 1 ((factorization 0) p) = {i ∈ Ico 1 0 | p ^ i ∣ 0}
Module: Mathlib.Algebra.CharP.Frobenius

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

Tactic:
by
  rw [iterateFrobenius_def, pow_zero, pow_one]

Goal state after:
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 : 0 ^ i ∣ n
⊢ i < b

pp: case succ
n b : ℕ
hn : n ≠ 0
i : ℕ
h2 : 1 ≤ i
h : i < n
p : ℕ
pp : Prime (p + 1)
hb : n < (p + 1) ^ b
h1 : (p + 1) ^ i ∣ n
⊢ i < b

Tactic:
·

Goal state after:
case zero
n b : ℕ
hn : n ≠ 0
i : ℕ
h2 : 1 ≤ i
h : i < n
pp : Prime 0
hb : n < 0 ^ b
h1 : 0 ^ i ∣ n
⊢ i < b
Module: Mathlib.Data.Nat.Factorization.Basic

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

Tactic:
by lia

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

Goal state before:
pp: p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
hdisj : Disjoint ({i ∈ Ico 1 n.succ | p ^ i ≤ k % p ^ i + (p ^ n - k) % p ^ i}) ({i ∈ Ico 1 n.succ | p ^ i ∣ k})
⊢ #({x ∈ Ico 1 n.succ | p ^ x ≤ k % p ^ x + (p ^ n - k) % p ^ x ∨ p ^ x ∣ k}) ≤ n

Tactic:
have filter_le_Ico := (Ico 1 n.succ).card_filter_le
        fun x => p ^ x ≤ k % p ^ x + (p ^ n - k) % p ^ x ∨ p ^ x ∣ k

Goal state after:
p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
hdisj : Disjoint ({i ∈ Ico 1 n.succ | p ^ i ≤ k % p ^ i + (p ^ n - k) % p ^ i}) ({i ∈ Ico 1 n.succ | p ^ i ∣ k})
filter_le_Ico : #({x ∈ Ico 1 n.succ | p ^ x ≤ k % p ^ x + (p ^ n - k) % p ^ x ∨ p ^ x ∣ k}) ≤ #(Ico 1 n.succ)
⊢ #({x ∈ Ico 1 n.succ | p ^ x ≤ k % p ^ x + (p ^ n - k) % p ^ x ∨ p ^ x ∣ k}) ≤ n
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case succ
n b : ℕ
hn : n ≠ 0
i : ℕ
h2 : 1 ≤ i
h : i < n
p : ℕ
pp : Prime (p + 1)
hb : n < (p + 1) ^ b
h1 : (p + 1) ^ i ∣ n
⊢ i < b

Tactic:
·

Goal state after:
case succ
n b : ℕ
hn : n ≠ 0
i : ℕ
h2 : 1 ≤ i
h : i < n
p : ℕ
pp : Prime (p + 1)
hb : n < (p + 1) ^ b
h1 : (p + 1) ^ i ∣ n
⊢ i < b
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: b m n : ℕ
hm : Prime m
hn : 0 < n
hb : n < m ^ b
⊢ n ≠ 0

Tactic:
by lia

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

Goal state before:
pp: case inl
p n k : ℕ
hp : Prime p
hk : k ≠ 0
hkp✝ : k ≠ p ^ n
hkp : p ^ n < k
⊢ p ∣ (p ^ n).choose k

pp: case inr
p n k : ℕ
hp : Prime p
hk : k ≠ 0
hkp✝ : k ≠ p ^ n
hkp : k < p ^ n
⊢ p ∣ (p ^ n).choose k

Tactic:
·

Goal state after:
case inl
p n k : ℕ
hp : Prime p
hk : k ≠ 0
hkp✝ : k ≠ p ^ n
hkp : p ^ n < k
⊢ p ∣ (p ^ n).choose k
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case mp
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ a = b → ∀ (p : ℕ), Prime p → padicValNat p a = padicValNat p b

pp: case mpr
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ (∀ (p : ℕ), Prime p → padicValNat p a = padicValNat p b) → a = b

Tactic:
·

Goal state after:
case mp
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ a = b → ∀ (p : ℕ), Prime p → padicValNat p a = padicValNat p b
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case mp
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ a = b → ∀ (p : ℕ), Prime p → padicValNat p a = padicValNat p b

pp: case mpr
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ (∀ (p : ℕ), Prime p → padicValNat p a = padicValNat p b) → a = b

Tactic:
· rintro rfl
    simp

Goal state after:
case mpr
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ (∀ (p : ℕ), Prime p → padicValNat p a = padicValNat p b) → a = b
Module: Mathlib.Data.Nat.Multiplicity

Goal state before:
pp: case refine_1
h2 : _root_.Prime 2
⊢ 0 ≠ 0 → emultiplicity 2 0! < ↑0

pp: case refine_2
h2 : _root_.Prime 2
⊢ ∀ (b : Bool) (n : ℕ), (n ≠ 0 → emultiplicity 2 n ! < ↑n) → bit b n ≠ 0 → emultiplicity 2 (bit b n)! < ↑(bit b n)

Tactic:
·

Goal state after:
case refine_1
h2 : _root_.Prime 2
⊢ 0 ≠ 0 → emultiplicity 2 0! < ↑0
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case mpr
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ (∀ (p : ℕ), Prime p → padicValNat p a = padicValNat p b) → a = b

Tactic:
·

Goal state after:
case mpr
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ (∀ (p : ℕ), Prime p → padicValNat p a = padicValNat p b) → a = b
Module: Mathlib.Data.Nat.Multiplicity

Goal state before:
pp: case refine_2
h2 : _root_.Prime 2
⊢ ∀ (b : Bool) (n : ℕ), (n ≠ 0 → emultiplicity 2 n ! < ↑n) → bit b n ≠ 0 → emultiplicity 2 (bit b n)! < ↑(bit b n)

Tactic:
·

Goal state after:
case refine_2
h2 : _root_.Prime 2
⊢ ∀ (b : Bool) (n : ℕ), (n ≠ 0 → emultiplicity 2 n ! < ↑n) → bit b n ≠ 0 → emultiplicity 2 (bit b n)! < ↑(bit b n)
Module: Mathlib.Data.Nat.Multiplicity

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

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

Tactic:
·

Goal state after:
case pos
h2 : _root_.Prime 2
b : Bool
n : ℕ
ih : n ≠ 0 → emultiplicity 2 n ! < ↑n
h : bit b n ≠ 0
hn : n = 0
⊢ emultiplicity 2 (bit b n)! < ↑(bit b n)
Module: Mathlib.Data.Nat.Multiplicity

Goal state before:
pp: case pos
h2 : _root_.Prime 2
b : Bool
ih : 0 ≠ 0 → emultiplicity 2 0! < ↑0
h : b = true
⊢ 0 < ↑1

pp: case pos
h2 : _root_.Prime 2
b : Bool
ih : 0 ≠ 0 → emultiplicity 2 0! < ↑0
h : b = true
⊢ Prime 2

Tactic:
·

Goal state after:
case pos
h2 : _root_.Prime 2
b : Bool
ih : 0 ≠ 0 → emultiplicity 2 0! < ↑0
h : b = true
⊢ 0 < ↑1
Module: Mathlib.Data.Nat.Multiplicity

Goal state before:
pp: case pos
h2 : _root_.Prime 2
b : Bool
ih : 0 ≠ 0 → emultiplicity 2 0! < ↑0
h : b = true
⊢ Prime 2

Tactic:
·

Goal state after:
case pos
h2 : _root_.Prime 2
b : Bool
ih : 0 ≠ 0 → emultiplicity 2 0! < ↑0
h : b = true
⊢ Prime 2
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case pos
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
h : ∀ (p : ℕ), Prime p → padicValNat p a = padicValNat p b
p : ℕ
pp : Prime p
⊢ a.factorization p = b.factorization p

pp: case neg
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
h : ∀ (p : ℕ), Prime p → padicValNat p a = padicValNat p b
p : ℕ
pp : ¬Prime p
⊢ a.factorization p = b.factorization p

Tactic:
·

Goal state after:
case pos
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
h : ∀ (p : ℕ), Prime p → padicValNat p a = padicValNat p b
p : ℕ
pp : Prime p
⊢ a.factorization p = b.factorization p
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case neg
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
h : ∀ (p : ℕ), Prime p → padicValNat p a = padicValNat p b
p : ℕ
pp : ¬Prime p
⊢ a.factorization p = b.factorization p

Tactic:
·

Goal state after:
case neg
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
h : ∀ (p : ℕ), Prime p → padicValNat p a = padicValNat p b
p : ℕ
pp : ¬Prime p
⊢ a.factorization p = b.factorization p
Module: Mathlib.Data.Nat.Multiplicity

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

pp: case neg.true
h2 : _root_.Prime 2
n : ℕ
ih : n ≠ 0 → emultiplicity 2 n ! < ↑n
hn : ¬n = 0
this : emultiplicity 2 (2 * n)! < ↑(2 * n)
h : bit true n ≠ 0
⊢ emultiplicity 2 (bit true n)! < ↑(bit true n)

Tactic:
·

Goal state after:
case neg.false
h2 : _root_.Prime 2
n : ℕ
ih : n ≠ 0 → emultiplicity 2 n ! < ↑n
hn : ¬n = 0
this : emultiplicity 2 (2 * n)! < ↑(2 * n)
h : bit false n ≠ 0
⊢ emultiplicity 2 (bit false n)! < ↑(bit false n)
Module: Mathlib.Data.Nat.Multiplicity

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

Tactic:
·

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

Goal state before:
pp: case inl
G : Type u_6
inst✝ : Group G
x : G
h : Fintype G
⊢ orderOf x ∣ Nat.card G

pp: case inr
G : Type u_6
inst✝ : Group G
x : G
h : Infinite G
⊢ orderOf x ∣ Nat.card G

Tactic:
·

Goal state after:
case inl
G : Type u_6
inst✝ : Group G
x : G
h : Fintype G
⊢ orderOf x ∣ Nat.card G
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case inr
G : Type u_6
inst✝ : Group G
x : G
h : Infinite G
⊢ orderOf x ∣ Nat.card G

Tactic:
·

Goal state after:
case inr
G : Type u_6
inst✝ : Group G
x : G
h : Infinite G
⊢ orderOf x ∣ Nat.card G
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case h
n : ℕ
hn : n ≠ 0
m : ℕ
pr : n < m
⊢ n.factorization.support ⊆ {p ∈ Finset.range m | Prime p}

pp: case hg
n : ℕ
hn : n ≠ 0
m : ℕ
pr : n < m
⊢ ∀ x ∈ {p ∈ Finset.range m | Prime p} \ n.factorization.support, x ^ padicValNat x n = 1

pp: case hfg
n : ℕ
hn : n ≠ 0
m : ℕ
pr : n < m
⊢ ∀ x ∈ n.factorization.support, (fun x1 x2 ↦ x1 ^ x2) x (n.factorization x) = x ^ padicValNat x n

Tactic:
·

Goal state after:
case h
n : ℕ
hn : n ≠ 0
m : ℕ
pr : n < m
⊢ n.factorization.support ⊆ {p ∈ Finset.range m | Prime p}
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case hg
n : ℕ
hn : n ≠ 0
m : ℕ
pr : n < m
⊢ ∀ x ∈ {p ∈ Finset.range m | Prime p} \ n.factorization.support, x ^ padicValNat x n = 1

pp: case hfg
n : ℕ
hn : n ≠ 0
m : ℕ
pr : n < m
⊢ ∀ x ∈ n.factorization.support, (fun x1 x2 ↦ x1 ^ x2) x (n.factorization x) = x ^ padicValNat x n

Tactic:
·

Goal state after:
case hg
n : ℕ
hn : n ≠ 0
m : ℕ
pr : n < m
⊢ ∀ x ∈ {p ∈ Finset.range m | Prime p} \ n.factorization.support, x ^ padicValNat x n = 1
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
g : G
x : k[G]
d : G
⊢ (single g 1 * x %ᵒᶠ g).coeff (g + d) = 0

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

Tactic:
·

Goal state after:
case inl
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCommMonoid G
g : G
x : k[G]
d : G
⊢ (single g 1 * x %ᵒᶠ g).coeff (g + d) = 0
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
g : G
x : k[G]
g' : G
h : ¬∃ d, g' = g + d
⊢ (single g 1 * x %ᵒᶠ g).coeff g' = 0

Tactic:
·

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

Goal state before:
pp: case hfg
n : ℕ
hn : n ≠ 0
m : ℕ
pr : n < m
⊢ ∀ x ∈ n.factorization.support, (fun x1 x2 ↦ x1 ^ x2) x (n.factorization x) = x ^ padicValNat x n

Tactic:
·

Goal state after:
case hfg
n : ℕ
hn : n ≠ 0
m : ℕ
pr : n < m
⊢ ∀ x ∈ n.factorization.support, (fun x1 x2 ↦ x1 ^ x2) x (n.factorization x) = x ^ padicValNat x n
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
x : k[G]
g d : G
⊢ (x * single g 1 %ᵒᶠ g).coeff (g + d) = 0

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:
·

Goal state after:
case inl
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCommMonoid G
x : k[G]
g d : G
⊢ (x * single g 1 %ᵒᶠ g).coeff (g + d) = 0
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:
·

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

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

Tactic:
·

Goal state after:
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)
Module: Mathlib.Data.Nat.Factorization.Basic

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

pp: case refine_2
n : ℕ
p1 p2 : ↥n.primeFactors
hp : p1 ≠ p2
⊢ Prime ↑p2

Tactic:
·

Goal state after:
case refine_1
n : ℕ
p1 p2 : ↥n.primeFactors
hp : p1 ≠ p2
⊢ Prime ↑p1
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
inst✝ : IsCancelAdd G
x : k[G]
g g' : G
h : ¬∃ d, g' = g + d
⊢ (single g 1 * (x /ᵒᶠ g)).coeff g' + (x %ᵒᶠ g).coeff g' = x.coeff g'

Tactic:
·

Goal state after:
case inr
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : AddCommMonoid G
inst✝ : IsCancelAdd G
x : k[G]
g g' : G
h : ¬∃ d, g' = g + d
⊢ (single g 1 * (x /ᵒᶠ g)).coeff g' + (x %ᵒᶠ g).coeff g' = x.coeff g'
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case refine_2
n : ℕ
p1 p2 : ↥n.primeFactors
hp : p1 ≠ p2
⊢ Prime ↑p2

Tactic:
·

Goal state after:
case refine_2
n : ℕ
p1 p2 : ↥n.primeFactors
hp : p1 ≠ p2
⊢ Prime ↑p2
Module: Mathlib.Algebra.MonoidAlgebra.Division

Goal state before:
pp: case mp
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : AddCommMonoid G
inst✝ : IsCancelAdd G
x : k[G]
g : G
⊢ of' k G g ∣ x → x %ᵒᶠ g = 0

pp: case mpr
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : AddCommMonoid G
inst✝ : IsCancelAdd G
x : k[G]
g : G
⊢ x %ᵒᶠ g = 0 → of' k G g ∣ x

Tactic:
·

Goal state after:
case mp
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : AddCommMonoid G
inst✝ : IsCancelAdd G
x : k[G]
g : G
⊢ of' k G g ∣ x → x %ᵒᶠ g = 0
Module: Mathlib.Algebra.MonoidAlgebra.Division

Goal state before:
pp: case mpr
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : AddCommMonoid G
inst✝ : IsCancelAdd G
x : k[G]
g : G
⊢ x %ᵒᶠ g = 0 → of' k G g ∣ x

Tactic:
·

Goal state after:
case mpr
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : AddCommMonoid G
inst✝ : IsCancelAdd G
x : k[G]
g : G
⊢ x %ᵒᶠ g = 0 → of' k G g ∣ x
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case refine_1
n k : ℕ
hn : n ≠ 0
hk : k ≠ 0
h : n ∣ k ^ n
⊢ n.primeFactors ⊆ k.primeFactors

pp: case refine_2
n k : ℕ
hn : n ≠ 0
hk : k ≠ 0
h : n.primeFactors ⊆ k.primeFactors
⊢ n ∣ k ^ n

Tactic:
·

Goal state after:
case refine_1
n k : ℕ
hn : n ≠ 0
hk : k ≠ 0
h : n ∣ k ^ n
⊢ n.primeFactors ⊆ k.primeFactors
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case refine_2
n k : ℕ
hn : n ≠ 0
hk : k ≠ 0
h : n.primeFactors ⊆ k.primeFactors
⊢ n ∣ k ^ n

Tactic:
·

Goal state after:
case refine_2
n k : ℕ
hn : n ≠ 0
hk : k ≠ 0
h : n.primeFactors ⊆ k.primeFactors
⊢ n ∣ k ^ n
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case inl
n k : ℕ
hn : n ≠ 0
hk : k ≠ 0
x✝ : ∃ m, n ∣ k ^ m
h : n ∣ k ^ 0
⊢ n.primeFactors ⊆ k.primeFactors

pp: case inr
n k : ℕ
hn : n ≠ 0
hk : k ≠ 0
x✝ : ∃ m, n ∣ k ^ m
m : ℕ
h : n ∣ k ^ m
hm : m ≠ 0
⊢ n.primeFactors ⊆ k.primeFactors

Tactic:
·

Goal state after:
case inl
n k : ℕ
hn : n ≠ 0
hk : k ≠ 0
x✝ : ∃ m, n ∣ k ^ m
h : n ∣ k ^ 0
⊢ n.primeFactors ⊆ k.primeFactors
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:
·

Goal state after:
case zero
R : Type u
inst✝ : Semiring R
⊢ (X ^ 0).divX = if 0 = 0 then 0 else X ^ (0 - 1)
Module: Mathlib.Algebra.Polynomial.Inductions

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

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.Algebra.Polynomial.Inductions

Goal state before:
pp: case φ_k
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ ∀ (f : R[X]), f.natDegree < 1 → divX_hom f = 0

pp: case φ_mon
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ ∀ (n : ℕ) (c : R), c ≠ 0 → (divX_hom ((monomial n) c)).natDegree = n - 1

Tactic:
·

Goal state after:
case φ_k
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ ∀ (f : R[X]), f.natDegree < 1 → divX_hom f = 0
Module: Mathlib.Algebra.Polynomial.Inductions

Goal state before:
pp: case φ_mon
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ ∀ (n : ℕ) (c : R), c ≠ 0 → (divX_hom ((monomial n) c)).natDegree = n - 1

Tactic:
·

Goal state after:
case φ_mon
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ ∀ (n : ℕ) (c : R), c ≠ 0 → (divX_hom ((monomial n) c)).natDegree = n - 1
Module: Mathlib.Algebra.Polynomial.Inductions

Goal state before:
pp: case pos
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
c : R
c0 : c ≠ 0
n0 : n = 0
⊢ (C c * 0).natDegree = n - 1

pp: case neg
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
c : R
c0 : c ≠ 0
n0 : ¬n = 0
⊢ (C c * X ^ (n - 1)).natDegree = n - 1

Tactic:
·

Goal state after:
case pos
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
c : R
c0 : c ≠ 0
n0 : n = 0
⊢ (C c * 0).natDegree = n - 1
Module: Mathlib.Algebra.Polynomial.Inductions

Goal state before:
pp: case neg
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
c : R
c0 : c ≠ 0
n0 : ¬n = 0
⊢ (C c * X ^ (n - 1)).natDegree = n - 1

Tactic:
·

Goal state after:
case neg
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
c : R
c0 : c ≠ 0
n0 : ¬n = 0
⊢ (C c * X ^ (n - 1)).natDegree = n - 1
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case pos
n N : ℕ
ih : #({k ∈ Finset.range N.succ | k ≠ 0 ∧ n ∣ k}) = N / n
h : n ∣ N.succ
⊢ #(if N + 1 ≠ 0 ∧ n ∣ N + 1 then insert (N + 1) ({k ∈ Finset.range (N + 1) | k ≠ 0 ∧ n ∣ k})
      else {k ∈ Finset.range (N + 1) | k ≠ 0 ∧ n ∣ k}) =
    (N + 1) / n

pp: case neg
n N : ℕ
ih : #({k ∈ Finset.range N.succ | k ≠ 0 ∧ n ∣ k}) = N / n
h : ¬n ∣ N.succ
⊢ #(if N + 1 ≠ 0 ∧ n ∣ N + 1 then insert (N + 1) ({k ∈ Finset.range (N + 1) | k ≠ 0 ∧ n ∣ k})
      else {k ∈ Finset.range (N + 1) | k ≠ 0 ∧ n ∣ k}) =
    (N + 1) / n

Tactic:
·

Goal state after:
case pos
n N : ℕ
ih : #({k ∈ Finset.range N.succ | k ≠ 0 ∧ n ∣ k}) = N / n
h : n ∣ N.succ
⊢ #(if N + 1 ≠ 0 ∧ n ∣ N + 1 then insert (N + 1) ({k ∈ Finset.range (N + 1) | k ≠ 0 ∧ n ∣ k})
      else {k ∈ Finset.range (N + 1) | k ≠ 0 ∧ n ∣ k}) =
    (N + 1) / n
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case neg
n N : ℕ
ih : #({k ∈ Finset.range N.succ | k ≠ 0 ∧ n ∣ k}) = N / n
h : ¬n ∣ N.succ
⊢ #(if N + 1 ≠ 0 ∧ n ∣ N + 1 then insert (N + 1) ({k ∈ Finset.range (N + 1) | k ≠ 0 ∧ n ∣ k})
      else {k ∈ Finset.range (N + 1) | k ≠ 0 ∧ n ∣ k}) =
    (N + 1) / n

Tactic:
·

Goal state after:
case neg
n N : ℕ
ih : #({k ∈ Finset.range N.succ | k ≠ 0 ∧ n ∣ k}) = N / n
h : ¬n ∣ N.succ
⊢ #(if N + 1 ≠ 0 ∧ n ∣ N + 1 then insert (N + 1) ({k ∈ Finset.range (N + 1) | k ≠ 0 ∧ n ∣ k})
      else {k ∈ Finset.range (N + 1) | k ≠ 0 ∧ n ∣ k}) =
    (N + 1) / n
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case pos
a b m n : ℕ
hmn : m.Coprime n
h : a ^ m = b ^ n
ha0 : a = 0
⊢ ∃ c, a = c ^ n ∧ b = c ^ m

pp: case neg
a b m n : ℕ
hmn : m.Coprime n
h : a ^ m = b ^ n
ha0 : ¬a = 0
⊢ ∃ c, a = c ^ n ∧ b = c ^ m

Tactic:
·

Goal state after:
case pos
a b m n : ℕ
hmn : m.Coprime n
h : a ^ m = b ^ n
ha0 : a = 0
⊢ ∃ c, a = c ^ n ∧ b = c ^ m
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case pos
a b m n : ℕ
hmn : m.Coprime n
h : b ^ n = a ^ m
ha0 : a = 0
hm0 : m = 0
⊢ ∃ c, a = c ^ n ∧ b = c ^ m

pp: case neg
a b m n : ℕ
hmn : m.Coprime n
h : b ^ n = a ^ m
ha0 : a = 0
hm0 : ¬m = 0
⊢ ∃ c, a = c ^ n ∧ b = c ^ m

Tactic:
·

Goal state after:
case pos
a b m n : ℕ
hmn : m.Coprime n
h : b ^ n = a ^ m
ha0 : a = 0
hm0 : m = 0
⊢ ∃ c, a = c ^ n ∧ b = c ^ m
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case neg
a b m n : ℕ
hmn : m.Coprime n
h : b ^ n = a ^ m
ha0 : a = 0
hm0 : ¬m = 0
⊢ ∃ c, a = c ^ n ∧ b = c ^ m

Tactic:
·

Goal state after:
case neg
a b m n : ℕ
hmn : m.Coprime n
h : b ^ n = a ^ m
ha0 : a = 0
hm0 : ¬m = 0
⊢ ∃ c, a = c ^ n ∧ b = c ^ m
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case pos
a b m n : ℕ
hmn : m.Coprime n
h : a ^ m = b ^ n
ha0 : ¬a = 0
hn0 : n = 0
⊢ ∃ c, a = c ^ n ∧ b = c ^ m

pp: case neg
a b m n : ℕ
hmn : m.Coprime n
h : a ^ m = b ^ n
ha0 : ¬a = 0
hn0 : ¬n = 0
⊢ ∃ c, a = c ^ n ∧ b = c ^ m

Tactic:
·

Goal state after:
case pos
a b m n : ℕ
hmn : m.Coprime n
h : a ^ m = b ^ n
ha0 : ¬a = 0
hn0 : n = 0
⊢ ∃ c, a = c ^ n ∧ b = c ^ m