mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case isTrue
α : Type u_1
inst✝ : Monoid α
a b : α
m : ℕ
nh : a ^ m ∣ b
h✝ : FiniteMultiplicity a b
hm : ↑(Nat.find h✝) < ↑m
⊢ False

pp: case isFalse
α : Type u_1
inst✝ : Monoid α
a b : α
m : ℕ
nh : a ^ m ∣ b
h✝ : ¬FiniteMultiplicity a b
hm : ⊤ < ↑m
⊢ False

Tactic:
·

Goal state after:
case isTrue
α : Type u_1
inst✝ : Monoid α
a b : α
m : ℕ
nh : a ^ m ∣ b
h✝ : FiniteMultiplicity a b
hm : ↑(Nat.find h✝) < ↑m
⊢ False
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case isFalse
α : Type u_1
inst✝ : Monoid α
a b : α
m : ℕ
nh : a ^ m ∣ b
h✝ : ¬FiniteMultiplicity a b
hm : ⊤ < ↑m
⊢ False

Tactic:
·

Goal state after:
case isFalse
α : Type u_1
inst✝ : Monoid α
a b : α
m : ℕ
nh : a ^ m ∣ b
h✝ : ¬FiniteMultiplicity a b
hm : ⊤ < ↑m
⊢ False
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case mp
α : Type u_1
inst✝ : Monoid α
a b : α
n : ℕ
⊢ emultiplicity a b = ↑n → a ^ n ∣ b ∧ ¬a ^ (n + 1) ∣ b

pp: case mpr
α : Type u_1
inst✝ : Monoid α
a b : α
n : ℕ
⊢ a ^ n ∣ b ∧ ¬a ^ (n + 1) ∣ b → emultiplicity a b = ↑n

Tactic:
·

Goal state after:
case mp
α : Type u_1
inst✝ : Monoid α
a b : α
n : ℕ
⊢ emultiplicity a b = ↑n → a ^ n ∣ b ∧ ¬a ^ (n + 1) ∣ b
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case mp.left
α : Type u_1
inst✝ : Monoid α
a b : α
n : ℕ
h : emultiplicity a b = ↑n
⊢ a ^ n ∣ b

pp: case mp.right
α : Type u_1
inst✝ : Monoid α
a b : α
n : ℕ
h : emultiplicity a b = ↑n
⊢ ¬a ^ (n + 1) ∣ b

Tactic:
·

Goal state after:
case mp.left
α : Type u_1
inst✝ : Monoid α
a b : α
n : ℕ
h : emultiplicity a b = ↑n
⊢ a ^ n ∣ b
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case mp.right
α : Type u_1
inst✝ : Monoid α
a b : α
n : ℕ
h : emultiplicity a b = ↑n
⊢ ¬a ^ (n + 1) ∣ b

Tactic:
·

Goal state after:
case mp.right
α : Type u_1
inst✝ : Monoid α
a b : α
n : ℕ
h : emultiplicity a b = ↑n
⊢ ¬a ^ (n + 1) ∣ b
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case mpr
α : Type u_1
inst✝ : Monoid α
a b : α
n : ℕ
⊢ a ^ n ∣ b ∧ ¬a ^ (n + 1) ∣ b → emultiplicity a b = ↑n

Tactic:
·

Goal state after:
case mpr
α : Type u_1
inst✝ : Monoid α
a b : α
n : ℕ
⊢ a ^ n ∣ b ∧ ¬a ^ (n + 1) ∣ b → emultiplicity a b = ↑n
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case pos
α : Type u_1
inst✝ : Monoid α
a b : α
hf : FiniteMultiplicity a b
⊢ emultiplicity a b = 0 ↔ ¬a ∣ b

pp: case neg
α : Type u_1
inst✝ : Monoid α
a b : α
hf : ¬FiniteMultiplicity a b
⊢ emultiplicity a b = 0 ↔ ¬a ∣ b

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝ : Monoid α
a b : α
hf : FiniteMultiplicity a b
⊢ emultiplicity a b = 0 ↔ ¬a ∣ b
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case neg
α : Type u_1
inst✝ : Monoid α
a b : α
hf : ¬FiniteMultiplicity a b
⊢ emultiplicity a b = 0 ↔ ¬a ∣ b

Tactic:
·

Goal state after:
case neg
α : Type u_1
inst✝ : Monoid α
a b : α
hf : ¬FiniteMultiplicity a b
⊢ emultiplicity a b = 0 ↔ ¬a ∣ b
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
hfin : FiniteMultiplicity a b
c k : α
hc : b = a ^ (multiplicity a b + 1) * k
hk : c = a * k
h₁ : a ^ (multiplicity a b + 1) ∣ b
⊢ False

Tactic:
exact (hfin.multiplicity_eq_iff.1 (by simp)).2 h₁

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
inst✝¹ : Monoid α
inst✝ : Monoid β
a b : α
c d : β
⊢ emultiplicity a b ≤ emultiplicity c d → ∀ (n : ℕ), a ^ n ∣ b → c ^ n ∣ d

pp: case mpr
α : Type u_1
β : Type u_2
inst✝¹ : Monoid α
inst✝ : Monoid β
a b : α
c d : β
⊢ (∀ (n : ℕ), a ^ n ∣ b → c ^ n ∣ d) → emultiplicity a b ≤ emultiplicity c d

Tactic:
·

Goal state after:
case mp
α : Type u_1
β : Type u_2
inst✝¹ : Monoid α
inst✝ : Monoid β
a b : α
c d : β
⊢ emultiplicity a b ≤ emultiplicity c d → ∀ (n : ℕ), a ^ n ∣ b → c ^ n ∣ d
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case pos
b f n e : ℕ
ih : (b.toDigitsCore f (n / b) []).length ≤ e + 1
h_e_pos : 0 < e + 1 + 1
hlt : n < b ^ (e + 1 + 1)
h✝ : n / b = 0
⊢ [(n % b).digitChar].length ≤ e + 1 + 1

pp: case neg
b f n e : ℕ
ih : (b.toDigitsCore f (n / b) []).length ≤ e + 1
h_e_pos : 0 < e + 1 + 1
hlt : n < b ^ (e + 1 + 1)
h✝ : ¬n / b = 0
⊢ (b.toDigitsCore f (n / b) [(n % b).digitChar]).length ≤ e + 1 + 1

Tactic:
·

Goal state after:
case pos
b f n e : ℕ
ih : (b.toDigitsCore f (n / b) []).length ≤ e + 1
h_e_pos : 0 < e + 1 + 1
hlt : n < b ^ (e + 1 + 1)
h✝ : n / b = 0
⊢ [(n % b).digitChar].length ≤ e + 1 + 1
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case neg
b f n e : ℕ
ih : (b.toDigitsCore f (n / b) []).length ≤ e + 1
h_e_pos : 0 < e + 1 + 1
hlt : n < b ^ (e + 1 + 1)
h✝ : ¬n / b = 0
⊢ (b.toDigitsCore f (n / b) [(n % b).digitChar]).length ≤ e + 1 + 1

Tactic:
·

Goal state after:
case neg
b f n e : ℕ
ih : (b.toDigitsCore f (n / b) []).length ≤ e + 1
h_e_pos : 0 < e + 1 + 1
hlt : n < b ^ (e + 1 + 1)
h✝ : ¬n / b = 0
⊢ (b.toDigitsCore f (n / b) [(n % b).digitChar]).length ≤ e + 1 + 1
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case inl
G : Type u_6
inst✝ : DivisionMonoid G
x : G
x✝ : ∃ n, n ≠ 0 ∧ x ^ n = 1
n : ℤ
hn : n ≠ 0
hn' : x ^ n = 1
h : n = ↑n.natAbs
⊢ x ^ n.natAbs = 1

pp: case inr
G : Type u_6
inst✝ : DivisionMonoid G
x : G
x✝ : ∃ n, n ≠ 0 ∧ x ^ n = 1
n : ℤ
hn : n ≠ 0
hn' : x ^ n = 1
h : n = -↑n.natAbs
⊢ x ^ n.natAbs = 1

Tactic:
·

Goal state after:
case inl
G : Type u_6
inst✝ : DivisionMonoid G
x : G
x✝ : ∃ n, n ≠ 0 ∧ x ^ n = 1
n : ℤ
hn : n ≠ 0
hn' : x ^ n = 1
h : n = ↑n.natAbs
⊢ x ^ n.natAbs = 1
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case inr
G : Type u_6
inst✝ : DivisionMonoid G
x : G
x✝ : ∃ n, n ≠ 0 ∧ x ^ n = 1
n : ℤ
hn : n ≠ 0
hn' : x ^ n = 1
h : n = -↑n.natAbs
⊢ x ^ n.natAbs = 1

Tactic:
·

Goal state after:
case inr
G : Type u_6
inst✝ : DivisionMonoid G
x : G
x✝ : ∃ n, n ≠ 0 ∧ x ^ n = 1
n : ℤ
hn : n ≠ 0
hn' : x ^ n = 1
h : n = -↑n.natAbs
⊢ x ^ n.natAbs = 1
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
inst✝¹ : Monoid α
inst✝ : Monoid β
a b : α
c d : β
⊢ (∀ (n : ℕ), a ^ n ∣ b → c ^ n ∣ d) → emultiplicity a b ≤ emultiplicity c d

Tactic:
·

Goal state after:
case mpr
α : Type u_1
β : Type u_2
inst✝¹ : Monoid α
inst✝ : Monoid β
a b : α
c d : β
⊢ (∀ (n : ℕ), a ^ n ∣ b → c ^ n ∣ d) → emultiplicity a b ≤ emultiplicity c d
Module: Mathlib.Data.Nat.Digits.Lemmas

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

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

Tactic:
·

Goal state after:
case ind.zero
b n : ℕ
IH : ∀ m ≤ n, ∀ (i : ℕ), ((b + 2).digits m)[i]?.getD 0 = m / (b + 2) ^ i % (b + 2)
⊢ ((b + 2).digits n.succ)[0]?.getD 0 = n.succ / (b + 2) ^ 0 % (b + 2)
Module: Mathlib.Data.Nat.Digits.Lemmas

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

Tactic:
·

Goal state after:
case ind.succ
b n : ℕ
IH : ∀ m ≤ n, ∀ (i : ℕ), ((b + 2).digits m)[i]?.getD 0 = m / (b + 2) ^ i % (b + 2)
i : ℕ
⊢ ((b + 2).digits n.succ)[i + 1]?.getD 0 = n.succ / (b + 2) ^ (i + 1) % (b + 2)
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:
·

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

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

Tactic:
·

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

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

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

Tactic:
·

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

Goal state after:
case inl
p : ℕ
⊢ padicValNat p 0 = 0 ↔ p = 1 ∨ 0 = 0 ∨ ¬p ∣ 0
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:
·

Goal state after:
case inr.inl
n : ℕ
hn₀ : n ≠ 0
⊢ padicValNat 1 n = 0 ↔ 1 = 1 ∨ n = 0 ∨ ¬1 ∣ n
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:
·

Goal state after:
case inl
G : Type u_1
inst✝ : Monoid G
a : G
⊢ IsOfFinOrder (a ^ 0) ↔ IsOfFinOrder a ∨ 0 = 0
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

pp: case inr
n b : ℕ
hb : 1 < b
l : ℕ
left✝ : l - (b.digits n).length ≠ 0
⊢ 0 < b

Tactic:
·

Goal state after:
case inl
n b : ℕ
hb : 1 < b
l i : ℕ
hi : i ∈ b.digits n
⊢ i < b
Module: Mathlib.GroupTheory.OrderOfElement

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

Tactic:
·

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.Data.Nat.Digits.Lemmas

Goal state before:
pp: case inr
n b : ℕ
hb : 1 < b
l : ℕ
left✝ : l - (b.digits n).length ≠ 0
⊢ 0 < b

Tactic:
·

Goal state after:
case inr
n b : ℕ
hb : 1 < b
l : ℕ
left✝ : l - (b.digits n).length ≠ 0
⊢ 0 < b
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝¹ : Monoid G
a : G
inst✝ : IsMulTorsionFree G
ha : a ≠ 1
n : ℕ
hn : 0 < n
han : a ^ n = 1
⊢ False

Tactic:
exact ha <| pow_left_injective hn.ne' <| by simpa using han

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

Goal state before:
pp: case inl
p : ℕ
⊢ count p (primeFactorsList 0) = (factorization 0) p

pp: case inr
n p : ℕ
hn0 : n > 0
⊢ count p n.primeFactorsList = n.factorization p

Tactic:
·

Goal state after:
case inl
p : ℕ
⊢ count p (primeFactorsList 0) = (factorization 0) p
Module: Mathlib.Data.Nat.Factorization.Defs

Goal state before:
pp: case inr.a
n p : ℕ
hn0 : n > 0
pp : Prime p
⊢ count p n.primeFactorsList ≤ padicValNat p n

pp: case a
n p : ℕ
hn0 : n > 0
pp : Prime p
⊢ padicValNat p n ≤ count p n.primeFactorsList

Tactic:
·

Goal state after:
case inr.a
n p : ℕ
hn0 : n > 0
pp : Prime p
⊢ count p n.primeFactorsList ≤ padicValNat p n
Module: Mathlib.Data.Nat.Factorization.Defs

Goal state before:
pp: case a
n p : ℕ
hn0 : n > 0
pp : Prime p
⊢ padicValNat p n ≤ count p n.primeFactorsList

Tactic:
·

Goal state after:
case a
n p : ℕ
hn0 : n > 0
pp : Prime p
⊢ padicValNat p n ≤ count p n.primeFactorsList
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: a b✝ : ℕ
hb : ¬b✝ = 0
b : ℕ
h : ∀ (n : ℕ), (b + 2) ^ n ∣ b✝
ha : b + 2 ≠ 0
ha1 : b + 2 ≠ 1
x✝ : b + 2 ≤ 1
⊢ False

Tactic:
by lia

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case top
α : Type u_1
inst✝ : Semiring α
p a b : α
hm : min (emultiplicity p a) (emultiplicity p b) = ⊤
⊢ ⊤ ≤ emultiplicity p (a + b)

pp: case coe
α : Type u_1
inst✝ : Semiring α
p a b : α
a✝ : ℕ
hm : min (emultiplicity p a) (emultiplicity p b) = ↑a✝
⊢ ↑a✝ ≤ emultiplicity p (a + b)

Tactic:
·

Goal state after:
case top
α : Type u_1
inst✝ : Semiring α
p a b : α
hm : min (emultiplicity p a) (emultiplicity p b) = ⊤
⊢ ⊤ ≤ emultiplicity p (a + b)
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case coe
α : Type u_1
inst✝ : Semiring α
p a b : α
a✝ : ℕ
hm : min (emultiplicity p a) (emultiplicity p b) = ↑a✝
⊢ ↑a✝ ≤ emultiplicity p (a + b)

Tactic:
·

Goal state after:
case coe
α : Type u_1
inst✝ : Semiring α
p a b : α
a✝ : ℕ
hm : min (emultiplicity p a) (emultiplicity p b) = ↑a✝
⊢ ↑a✝ ≤ emultiplicity p (a + b)
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: case refine_1
b : ℕ
hb : 1 < b
l : ℕ
L : List ℕ
hL : L ∈ {L | L.length = l ∧ ∀ x ∈ L, x < b}
⊢ (b.digitsAppend l (ofDigits b L)).length = l

pp: case refine_2
b : ℕ
hb : 1 < b
l : ℕ
L : List ℕ
hL : L ∈ {L | L.length = l ∧ ∀ x ∈ L, x < b}
⊢ ∀ x ∈ b.digitsAppend l (ofDigits b L), x < b

Tactic:
·

Goal state after:
case refine_1
b : ℕ
hb : 1 < b
l : ℕ
L : List ℕ
hL : L ∈ {L | L.length = l ∧ ∀ x ∈ L, x < b}
⊢ (b.digitsAppend l (ofDigits b L)).length = l
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: case refine_2
b : ℕ
hb : 1 < b
l : ℕ
L : List ℕ
hL : L ∈ {L | L.length = l ∧ ∀ x ∈ L, x < b}
⊢ ∀ x ∈ b.digitsAppend l (ofDigits b L), x < b

Tactic:
·

Goal state after:
case refine_2
b : ℕ
hb : 1 < b
l : ℕ
L : List ℕ
hL : L ∈ {L | L.length = l ∧ ∀ x ∈ L, x < b}
⊢ ∀ x ∈ b.digitsAppend l (ofDigits b L), x < b
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case inl
a : ℕ
b : ℤ
h : b = ↑b.natAbs
⊢ emultiplicity a b.natAbs = emultiplicity ↑a ↑b.natAbs

pp: case inr
a : ℕ
b : ℤ
h : b = -↑b.natAbs
⊢ emultiplicity a b.natAbs = emultiplicity (↑a) (-↑b.natAbs)

Tactic:
·

Goal state after:
case inl
a : ℕ
b : ℤ
h : b = ↑b.natAbs
⊢ emultiplicity a b.natAbs = emultiplicity ↑a ↑b.natAbs
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case inr
a : ℕ
b : ℤ
h : b = -↑b.natAbs
⊢ emultiplicity a b.natAbs = emultiplicity (↑a) (-↑b.natAbs)

Tactic:
·

Goal state after:
case inr
a : ℕ
b : ℤ
h : b = -↑b.natAbs
⊢ emultiplicity a b.natAbs = emultiplicity (↑a) (-↑b.natAbs)
Module: Mathlib.RingTheory.Multiplicity

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

pp: case hsucc
α : Type u_1
inst✝ : Ring α
p a b : α
h : ↑(multiplicity p b) < emultiplicity p a
this : FiniteMultiplicity p b
⊢ ¬p ^ (multiplicity p b + 1) ∣ a + b

Tactic:
·

Goal state after:
case hk
α : Type u_1
inst✝ : Ring α
p a b : α
h : ↑(multiplicity p b) < emultiplicity p a
this : FiniteMultiplicity p b
⊢ p ^ multiplicity p b ∣ a + b
Module: Mathlib.RingTheory.Multiplicity

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

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

Goal state after:
case hk.h₁
α : Type u_1
inst✝ : Ring α
p a b : α
h : ↑(multiplicity p b) < emultiplicity p a
this : FiniteMultiplicity p b
⊢ p ^ multiplicity p b ∣ a
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:
·

Goal state after:
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
Module: Mathlib.RingTheory.Multiplicity

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

Tactic:
·

Goal state after:
case hsucc
α : Type u_1
inst✝ : Ring α
p a b : α
h : ↑(multiplicity p b) < emultiplicity p a
this : FiniteMultiplicity p b
⊢ ¬p ^ (multiplicity p b + 1) ∣ a + b
Module: Mathlib.RingTheory.Multiplicity

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

pp: case hsucc
α : Type u_1
inst✝ : Ring α
p a b : α
h : ↑(multiplicity p b) < emultiplicity p a
this : FiniteMultiplicity p b
⊢ p ^ (multiplicity p b + 1) ∣ a

Tactic:
·

Goal state after:
case hsucc
α : Type u_1
inst✝ : Ring α
p a b : α
h : ↑(multiplicity p b) < emultiplicity p a
this : FiniteMultiplicity p b
⊢ ¬p ^ (multiplicity p b + 1) ∣ b
Module: Mathlib.Data.Nat.Factorization.Defs

Goal state before:
pp: case refine_1
d n : ℕ
hd : d ≠ 0
hn : n ≠ 0
hdn : d.factorization ≤ n.factorization
⊢ d ∣ n

pp: case refine_2
d n : ℕ
hd : d ≠ 0
hn : n ≠ 0
x✝ : d ∣ n
c : ℕ
h : n = d * c
⊢ d.factorization ≤ n.factorization

Tactic:
·

Goal state after:
case refine_1
d n : ℕ
hd : d ≠ 0
hn : n ≠ 0
hdn : d.factorization ≤ n.factorization
⊢ d ∣ n
Module: Mathlib.Data.Nat.Factorization.Defs

Goal state before:
pp: case refine_2
d n : ℕ
hd : d ≠ 0
hn : n ≠ 0
x✝ : d ∣ n
c : ℕ
h : n = d * c
⊢ d.factorization ≤ n.factorization

Tactic:
·

Goal state after:
case refine_2
d n : ℕ
hd : d ≠ 0
hn : n ≠ 0
x✝ : d ∣ n
c : ℕ
h : n = d * c
⊢ d.factorization ≤ n.factorization
Module: Mathlib.GroupTheory.OrderOfElement

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

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

Tactic:
·

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

Goal state after:
case refine_1
α : Type u_1
S : Finset α
g : α → ℕ
hS : ∀ x ∈ S, g x ≠ 0
⊢ (∅.prod g).factorization = ∑ x ∈ ∅, (g x).factorization
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: case refine_1
b : ℕ
hb : 1 < b
l d : ℕ
hd : d < b
L : List ℕ
hL : L ∈ fixedLengthDigits hb l
⊢ (d :: L).length = l + 1

pp: case refine_2
b : ℕ
hb : 1 < b
l d : ℕ
hd : d < b
L : List ℕ
hL : L ∈ fixedLengthDigits hb l
⊢ ∀ x ∈ d :: L, x < b

Tactic:
·

Goal state after:
case refine_1
b : ℕ
hb : 1 < b
l d : ℕ
hd : d < b
L : List ℕ
hL : L ∈ fixedLengthDigits hb l
⊢ (d :: L).length = l + 1
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: case refine_2
b : ℕ
hb : 1 < b
l d : ℕ
hd : d < b
L : List ℕ
hL : L ∈ fixedLengthDigits hb l
⊢ ∀ x ∈ d :: L, x < b

Tactic:
·

Goal state after:
case refine_2
b : ℕ
hb : 1 < b
l d : ℕ
hd : d < b
L : List ℕ
hL : L ∈ fixedLengthDigits hb l
⊢ ∀ x ∈ d :: L, x < b
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case inl
α : Type u_1
inst✝ : Ring α
p a b : α
h : emultiplicity p a ≠ emultiplicity p b
hab : emultiplicity p a < emultiplicity p b
⊢ emultiplicity p (a + b) = min (emultiplicity p a) (emultiplicity p b)

pp: case inr.inl
α : Type u_1
inst✝ : Ring α
p a b : α
h : emultiplicity p a ≠ emultiplicity p b
h✝ : emultiplicity p a = emultiplicity p b
⊢ emultiplicity p (a + b) = min (emultiplicity p a) (emultiplicity p b)

pp: case inr.inr
α : Type u_1
inst✝ : Ring α
p a b : α
h : emultiplicity p a ≠ emultiplicity p b
hab : emultiplicity p b < emultiplicity p a
⊢ emultiplicity p (a + b) = min (emultiplicity p a) (emultiplicity p b)

Tactic:
·

Goal state after:
case inl
α : Type u_1
inst✝ : Ring α
p a b : α
h : emultiplicity p a ≠ emultiplicity p b
hab : emultiplicity p a < emultiplicity p b
⊢ emultiplicity p (a + b) = min (emultiplicity p a) (emultiplicity p b)
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: case refine_2.inl
b : ℕ
hb : 1 < b
l : ℕ
L : List ℕ
hL : L ∈ fixedLengthDigits hb l
x : ℕ
hd : x < b
hx : x ∈ x :: L
⊢ x < b

pp: case refine_2.inr
b : ℕ
hb : 1 < b
l d : ℕ
hd : d < b
L : List ℕ
hL : L ∈ fixedLengthDigits hb l
x : ℕ
hx✝ : x ∈ d :: L
hx : x ∈ L
⊢ x < b

Tactic:
·

Goal state after:
case refine_2.inl
b : ℕ
hb : 1 < b
l : ℕ
L : List ℕ
hL : L ∈ fixedLengthDigits hb l
x : ℕ
hd : x < b
hx : x ∈ x :: L
⊢ x < b
Module: Mathlib.Data.Nat.Factorization.Defs

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

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.Digits.Lemmas

Goal state before:
pp: case refine_2.inr
b : ℕ
hb : 1 < b
l d : ℕ
hd : d < b
L : List ℕ
hL : L ∈ fixedLengthDigits hb l
x : ℕ
hx✝ : x ∈ d :: L
hx : x ∈ L
⊢ x < b

Tactic:
·

Goal state after:
case refine_2.inr
b : ℕ
hb : 1 < b
l d : ℕ
hd : d < b
L : List ℕ
hL : L ∈ fixedLengthDigits hb l
x : ℕ
hx✝ : x ∈ d :: L
hx : x ∈ L
⊢ x < b
Module: Mathlib.GroupTheory.OrderOfElement

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

Tactic:
·

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

Goal state before:
pp: case inr.inl
α : Type u_1
inst✝ : Ring α
p a b : α
h : emultiplicity p a ≠ emultiplicity p b
h✝ : emultiplicity p a = emultiplicity p b
⊢ emultiplicity p (a + b) = min (emultiplicity p a) (emultiplicity p b)

pp: case inr.inr
α : Type u_1
inst✝ : Ring α
p a b : α
h : emultiplicity p a ≠ emultiplicity p b
hab : emultiplicity p b < emultiplicity p a
⊢ emultiplicity p (a + b) = min (emultiplicity p a) (emultiplicity p b)

Tactic:
·

Goal state after:
case inr.inl
α : Type u_1
inst✝ : Ring α
p a b : α
h : emultiplicity p a ≠ emultiplicity p b
h✝ : emultiplicity p a = emultiplicity p b
⊢ emultiplicity p (a + b) = min (emultiplicity p a) (emultiplicity p b)
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case inr.inr
α : Type u_1
inst✝ : Ring α
p a b : α
h : emultiplicity p a ≠ emultiplicity p b
hab : emultiplicity p b < emultiplicity p a
⊢ emultiplicity p (a + b) = min (emultiplicity p a) (emultiplicity p b)

Tactic:
·

Goal state after:
case inr.inr
α : Type u_1
inst✝ : Ring α
p a b : α
h : emultiplicity p a ≠ emultiplicity p b
hab : emultiplicity p b < emultiplicity p a
⊢ emultiplicity p (a + b) = min (emultiplicity p a) (emultiplicity p b)