internlm/Lean-Github huggingface dataset:
Theorem: WfDvdMonoid.multiplicity_finite_iff
Proof state before:
case mp
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁴ : Field K
inst✝³ : CharZero K
inst✝² : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
M : Type u_2
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : WfDvdMonoid M
x y : M
⊢ IsUnit x ∨ y = 0 → ¬multiplicity.Finite x y
Tactic:
rintro (hx|hy)
Proof state after:
case mp.inl
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁴ : Field K
inst✝³ : CharZero K
inst✝² : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
M : Type u_2
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : WfDvdMonoid M
x y : M
hx : IsUnit x
⊢ ¬multiplicity.Finite x y

case mp.inr
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁴ : Field K
inst✝³ : CharZero K
inst✝² : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
M : Type u_2
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : WfDvdMonoid M
x y : M
hy : y = 0
⊢ ¬multiplicity.Finite x y
Theorem: WfDvdMonoid.multiplicity_finite_iff
Proof state before:
case mp.inl
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁴ : Field K
inst✝³ : CharZero K
inst✝² : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
M : Type u_2
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : WfDvdMonoid M
x y : M
hx : IsUnit x
⊢ ¬multiplicity.Finite x y
Tactic:
exact fun ⟨n, hn⟩ ↦ hn (hx.pow _).dvd
Proof state after:
no goals
Theorem: WfDvdMonoid.multiplicity_finite_iff
Proof state before:
case mp.inr
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁴ : Field K
inst✝³ : CharZero K
inst✝² : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
M : Type u_2
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : WfDvdMonoid M
x y : M
hy : y = 0
⊢ ¬multiplicity.Finite x y
Tactic:
simp [hy]
Proof state after:
no goals
Theorem: WfDvdMonoid.multiplicity_finite_iff
Proof state before:
case mpr
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁴ : Field K
inst✝³ : CharZero K
inst✝² : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
M : Type u_2
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : WfDvdMonoid M
x y : M
⊢ ¬IsUnit x ∧ y ≠ 0 → multiplicity.Finite x y
Tactic:
intro ⟨hx, hy⟩
Proof state after:
case mpr
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁴ : Field K
inst✝³ : CharZero K
inst✝² : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
M : Type u_2
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : WfDvdMonoid M
x y : M
hx : ¬IsUnit x
hy : y ≠ 0
⊢ multiplicity.Finite x y
Theorem: WfDvdMonoid.multiplicity_finite_iff
Proof state before:
case mpr
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁴ : Field K
inst✝³ : CharZero K
inst✝² : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
M : Type u_2
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : WfDvdMonoid M
x y : M
hx : ¬IsUnit x
hy : y ≠ 0
⊢ multiplicity.Finite x y
Tactic:
exact WfDvdMonoid.multiplicity_finite hx hy
Proof state after:
no goals
Theorem: WfDvdMonoid.multiplicity_eq_top_iff
Proof state before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁵ : Field K
inst✝⁴ : CharZero K
inst✝³ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
M : Type u_2
inst✝² : CancelCommMonoidWithZero M
inst✝¹ : WfDvdMonoid M
inst✝ : DecidableRel fun a b => a ∣ b
x y : M
⊢ multiplicity x y = ⊤ ↔ IsUnit x ∨ y = 0
Tactic:
rw [multiplicity.eq_top_iff_not_finite, WfDvdMonoid.multiplicity_finite_iff, or_iff_not_and_not]
Proof state after:
no goals
Theorem: dvd_iff_multiplicity_le
Proof state before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁵ : Field K
inst✝⁴ : CharZero K
inst✝³ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
M : Type u_2
inst✝² : CancelCommMonoidWithZero M
inst✝¹ : DecidableRel fun a b => a ∣ b
inst✝ : UniqueFactorizationMonoid M
a b : M
ha : a ≠ 0
⊢ a ∣ b ↔ ∀ (p : M), Prime p → multiplicity p a ≤ multiplicity p b
Tactic:
constructor
Proof state after:
case mp
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁵ : Field K
inst✝⁴ : CharZero K
inst✝³ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
M : Type u_2
inst✝² : CancelCommMonoidWithZero M
inst✝¹ : DecidableRel fun a b => a ∣ b
inst✝ : UniqueFactorizationMonoid M
a b : M
ha : a ≠ 0
⊢ a ∣ b → ∀ (p : M), Prime p → multiplicity p a ≤ multiplicity p b

case mpr
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁵ : Field K
inst✝⁴ : CharZero K
inst✝³ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
M : Type u_2
inst✝² : CancelCommMonoidWithZero M
inst✝¹ : DecidableRel fun a b => a ∣ b
inst✝ : UniqueFactorizationMonoid M
a b : M
ha : a ≠ 0
⊢ (∀ (p : M), Prime p → multiplicity p a ≤ multiplicity p b) → a ∣ b
Theorem: dvd_iff_multiplicity_le
Proof state before:
case mp
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁵ : Field K
inst✝⁴ : CharZero K
inst✝³ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
M : Type u_2
inst✝² : CancelCommMonoidWithZero M
inst✝¹ : DecidableRel fun a b => a ∣ b
inst✝ : UniqueFactorizationMonoid M
a b : M
ha : a ≠ 0
⊢ a ∣ b → ∀ (p : M), Prime p → multiplicity p a ≤ multiplicity p b
Tactic:
intro hab p _
Proof state after:
case mp
K : Type u_1
p✝ : ℕ+
hpri : Fact p✝.Prime
inst✝⁵ : Field K
inst✝⁴ : CharZero K
inst✝³ : IsCyclotomicExtension {p✝} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p✝
M : Type u_2
inst✝² : CancelCommMonoidWithZero M
inst✝¹ : DecidableRel fun a b => a ∣ b
inst✝ : UniqueFactorizationMonoid M
a b : M
ha : a ≠ 0
hab : a ∣ b
p : M
a✝ : Prime p
⊢ multiplicity p a ≤ multiplicity p b
Theorem: dvd_iff_multiplicity_le
Proof state before:
case mp
K : Type u_1
p✝ : ℕ+
hpri : Fact p✝.Prime
inst✝⁵ : Field K
inst✝⁴ : CharZero K
inst✝³ : IsCyclotomicExtension {p✝} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p✝
M : Type u_2
inst✝² : CancelCommMonoidWithZero M
inst✝¹ : DecidableRel fun a b => a ∣ b
inst✝ : UniqueFactorizationMonoid M
a b : M
ha : a ≠ 0
hab : a ∣ b
p : M
a✝ : Prime p
⊢ multiplicity p a ≤ multiplicity p b
Tactic:
exact multiplicity.multiplicity_le_multiplicity_of_dvd_right hab
Proof state after:
no goals
Theorem: dvd_iff_multiplicity_le
Proof state before:
case mpr
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁵ : Field K
inst✝⁴ : CharZero K
inst✝³ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
M : Type u_2
inst✝² : CancelCommMonoidWithZero M
inst✝¹ : DecidableRel fun a b => a ∣ b
inst✝ : UniqueFactorizationMonoid M
a b : M
ha : a ≠ 0
⊢ (∀ (p : M), Prime p → multiplicity p a ≤ multiplicity p b) → a ∣ b
Tactic:
intro H
Proof state after:
case mpr
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁵ : Field K
inst✝⁴ : CharZero K
inst✝³ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
M : Type u_2
inst✝² : CancelCommMonoidWithZero M
inst✝¹ : DecidableRel fun a b => a ∣ b
inst✝ : UniqueFactorizationMonoid M
a b : M
ha : a ≠ 0
H : ∀ (p : M), Prime p → multiplicity p a ≤ multiplicity p b
⊢ a ∣ b
Theorem: dvd_iff_multiplicity_le
Proof state before:
case mpr
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁵ : Field K
inst✝⁴ : CharZero K
inst✝³ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
M : Type u_2
inst✝² : CancelCommMonoidWithZero M
inst✝¹ : DecidableRel fun a b => a ∣ b
inst✝ : UniqueFactorizationMonoid M
a b : M
ha : a ≠ 0
H : ∀ (p : M), Prime p → multiplicity p a ≤ multiplicity p b
⊢ a ∣ b
Tactic:
by_cases hb : b = 0
Proof state after:
case pos
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁵ : Field K
inst✝⁴ : CharZero K
inst✝³ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
M : Type u_2
inst✝² : CancelCommMonoidWithZero M
inst✝¹ : DecidableRel fun a b => a ∣ b
inst✝ : UniqueFactorizationMonoid M
a b : M
ha : a ≠ 0
H : ∀ (p : M), Prime p → multiplicity p a ≤ multiplicity p b
hb : b = 0
⊢ a ∣ b

case neg
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁵ : Field K
inst✝⁴ : CharZero K
inst✝³ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
M : Type u_2
inst✝² : CancelCommMonoidWithZero M
inst✝¹ : DecidableRel fun a b => a ∣ b
inst✝ : UniqueFactorizationMonoid M
a b : M
ha : a ≠ 0
H : ∀ (p : M), Prime p → multiplicity p a ≤ multiplicity p b
hb : ¬b = 0
⊢ a ∣ b
Theorem: dvd_iff_multiplicity_le
Proof state before:
case neg
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁵ : Field K
inst✝⁴ : CharZero K
inst✝³ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
M : Type u_2
inst✝² : CancelCommMonoidWithZero M
inst✝¹ : DecidableRel fun a b => a ∣ b
inst✝ : UniqueFactorizationMonoid M
a b : M
ha : a ≠ 0
H : ∀ (p : M), Prime p → multiplicity p a ≤ multiplicity p b
hb : ¬b = 0
⊢ a ∣ b
Tactic:
induction' a using WfDvdMonoid.induction_on_irreducible with u hu a q _ hq IH
Proof state after:
case neg.h0
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁵ : Field K
inst✝⁴ : CharZero K
inst✝³ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
M : Type u_2
inst✝² : CancelCommMonoidWithZero M
inst✝¹ : DecidableRel fun a b => a ∣ b
inst✝ : UniqueFactorizationMonoid M
b : M
hb : ¬b = 0
ha : 0 ≠ 0
H : ∀ (p : M), Prime p → multiplicity p 0 ≤ multiplicity p b
⊢ 0 ∣ b

case neg.hu
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁵ : Field K
inst✝⁴ : CharZero K
inst✝³ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
M : Type u_2
inst✝² : CancelCommMonoidWithZero M
inst✝¹ : DecidableRel fun a b => a ∣ b
inst✝ : UniqueFactorizationMonoid M
b : M
hb : ¬b = 0
u : M
hu : IsUnit u
ha : u ≠ 0
H : ∀ (p : M), Prime p → multiplicity p u ≤ multiplicity p b
⊢ u ∣ b

case neg.hi
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁵ : Field K
inst✝⁴ : CharZero K
inst✝³ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
M : Type u_2
inst✝² : CancelCommMonoidWithZero M
inst✝¹ : DecidableRel fun a b => a ∣ b
inst✝ : UniqueFactorizationMonoid M
b : M
hb : ¬b = 0
a q : M
a✝ : a ≠ 0
hq : Irreducible q
IH : a ≠ 0 → (∀ (p : M), Prime p → multiplicity p a ≤ multiplicity p b) → a ∣ b
ha : q * a ≠ 0
H : ∀ (p : M), Prime p → multiplicity p (q * a) ≤ multiplicity p b
⊢ q * a ∣ b
Theorem: dvd_iff_multiplicity_le
Proof state before:
case pos
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁵ : Field K
inst✝⁴ : CharZero K
inst✝³ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
M : Type u_2
inst✝² : CancelCommMonoidWithZero M
inst✝¹ : DecidableRel fun a b => a ∣ b
inst✝ : UniqueFactorizationMonoid M
a b : M
ha : a ≠ 0
H : ∀ (p : M), Prime p → multiplicity p a ≤ multiplicity p b
hb : b = 0
⊢ a ∣ b
Tactic:
exact hb ▸ dvd_zero a
Proof state after:
no goals
Theorem: dvd_iff_multiplicity_le
Proof state before:
case neg.h0
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁵ : Field K
inst✝⁴ : CharZero K
inst✝³ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
M : Type u_2
inst✝² : CancelCommMonoidWithZero M
inst✝¹ : DecidableRel fun a b => a ∣ b
inst✝ : UniqueFactorizationMonoid M
b : M
hb : ¬b = 0
ha : 0 ≠ 0
H : ∀ (p : M), Prime p → multiplicity p 0 ≤ multiplicity p b
⊢ 0 ∣ b
Tactic:
exact (ha rfl).elim
Proof state after:
no goals
Theorem: dvd_iff_multiplicity_le
Proof state before:
case neg.hu
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁵ : Field K
inst✝⁴ : CharZero K
inst✝³ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
M : Type u_2
inst✝² : CancelCommMonoidWithZero M
inst✝¹ : DecidableRel fun a b => a ∣ b
inst✝ : UniqueFactorizationMonoid M
b : M
hb : ¬b = 0
u : M
hu : IsUnit u
ha : u ≠ 0
H : ∀ (p : M), Prime p → multiplicity p u ≤ multiplicity p b
⊢ u ∣ b
Tactic:
exact hu.dvd
Proof state after:
no goals
Theorem: dvd_iff_multiplicity_le
Proof state before:
case neg.hi
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁵ : Field K
inst✝⁴ : CharZero K
inst✝³ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
M : Type u_2
inst✝² : CancelCommMonoidWithZero M
inst✝¹ : DecidableRel fun a b => a ∣ b
inst✝ : UniqueFactorizationMonoid M
b : M
hb : ¬b = 0
a q : M
a✝ : a ≠ 0
hq : Irreducible q
IH : a ≠ 0 → (∀ (p : M), Prime p → multiplicity p a ≤ multiplicity p b) → a ∣ b
ha : q * a ≠ 0
H : ∀ (p : M), Prime p → multiplicity p (q * a) ≤ multiplicity p b
⊢ q * a ∣ b
Tactic:
simp only [ne_eq, mul_eq_zero, not_or] at ha
Proof state after:
case neg.hi
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁵ : Field K
inst✝⁴ : CharZero K
inst✝³ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
M : Type u_2
inst✝² : CancelCommMonoidWithZero M
inst✝¹ : DecidableRel fun a b => a ∣ b
inst✝ : UniqueFactorizationMonoid M
b : M
hb : ¬b = 0
a q : M
a✝ : a ≠ 0
hq : Irreducible q
IH : a ≠ 0 → (∀ (p : M), Prime p → multiplicity p a ≤ multiplicity p b) → a ∣ b
H : ∀ (p : M), Prime p → multiplicity p (q * a) ≤ multiplicity p b
ha : ¬q = 0 ∧ ¬a = 0
⊢ q * a ∣ b
Theorem: dvd_iff_multiplicity_le
Proof state before:
case neg.hi
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁵ : Field K
inst✝⁴ : CharZero K
inst✝³ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
M : Type u_2
inst✝² : CancelCommMonoidWithZero M
inst✝¹ : DecidableRel fun a b => a ∣ b
inst✝ : UniqueFactorizationMonoid M
b : M
hb : ¬b = 0
a q : M
a✝ : a ≠ 0
hq : Irreducible q
IH : a ≠ 0 → (∀ (p : M), Prime p → multiplicity p a ≤ multiplicity p b) → a ∣ b
H : ∀ (p : M), Prime p → multiplicity p (q * a) ≤ multiplicity p b
ha : ¬q = 0 ∧ ¬a = 0
⊢ q * a ∣ b
Tactic:
rw [UniqueFactorizationMonoid.irreducible_iff_prime] at hq
Proof state after:
case neg.hi
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁵ : Field K
inst✝⁴ : CharZero K
inst✝³ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
M : Type u_2
inst✝² : CancelCommMonoidWithZero M
inst✝¹ : DecidableRel fun a b => a ∣ b
inst✝ : UniqueFactorizationMonoid M
b : M
hb : ¬b = 0
a q : M
a✝ : a ≠ 0
hq : Prime q
IH : a ≠ 0 → (∀ (p : M), Prime p → multiplicity p a ≤ multiplicity p b) → a ∣ b
H : ∀ (p : M), Prime p → multiplicity p (q * a) ≤ multiplicity p b
ha : ¬q = 0 ∧ ¬a = 0
⊢ q * a ∣ b
Theorem: dvd_iff_multiplicity_le
Proof state before:
case neg.hi
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁵ : Field K
inst✝⁴ : CharZero K
inst✝³ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
M : Type u_2
inst✝² : CancelCommMonoidWithZero M
inst✝¹ : DecidableRel fun a b => a ∣ b
inst✝ : UniqueFactorizationMonoid M
b : M
hb : ¬b = 0
a q : M
a✝ : a ≠ 0
hq : Prime q
IH : a ≠ 0 → (∀ (p : M), Prime p → multiplicity p a ≤ multiplicity p b) → a ∣ b
H : ∀ (p : M), Prime p → multiplicity p (q * a) ≤ multiplicity p b
ha : ¬q = 0 ∧ ¬a = 0
⊢ q * a ∣ b
Tactic:
obtain ⟨c, rfl⟩ : a ∣ b := by
  refine' IH ha.2 (fun p hp ↦ (le_trans ?_ (H p hp)))
  rw [multiplicity.mul hp]
  exact le_add_self
Proof state after:
case neg.hi.intro
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁵ : Field K
inst✝⁴ : CharZero K
inst✝³ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
M : Type u_2
inst✝² : CancelCommMonoidWithZero M
inst✝¹ : DecidableRel fun a b => a ∣ b
inst✝ : UniqueFactorizationMonoid M
a q : M
a✝ : a ≠ 0
hq : Prime q
ha : ¬q = 0 ∧ ¬a = 0
c : M
hb : ¬a * c = 0
IH : a ≠ 0 → (∀ (p : M), Prime p → multiplicity p a ≤ multiplicity p (a * c)) → a ∣ a * c
H : ∀ (p : M), Prime p → multiplicity p (q * a) ≤ multiplicity p (a * c)
⊢ q * a ∣ a * c
Theorem: dvd_iff_multiplicity_le
Proof state before:
case neg.hi.intro
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁵ : Field K
inst✝⁴ : CharZero K
inst✝³ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
M : Type u_2
inst✝² : CancelCommMonoidWithZero M
inst✝¹ : DecidableRel fun a b => a ∣ b
inst✝ : UniqueFactorizationMonoid M
a q : M
a✝ : a ≠ 0
hq : Prime q
ha : ¬q = 0 ∧ ¬a = 0
c : M
hb : ¬a * c = 0
IH : a ≠ 0 → (∀ (p : M), Prime p → multiplicity p a ≤ multiplicity p (a * c)) → a ∣ a * c
H : ∀ (p : M), Prime p → multiplicity p (q * a) ≤ multiplicity p (a * c)
⊢ q * a ∣ a * c
Tactic:
rw [mul_comm]
Proof state after:
case neg.hi.intro
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁵ : Field K
inst✝⁴ : CharZero K
inst✝³ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
M : Type u_2
inst✝² : CancelCommMonoidWithZero M
inst✝¹ : DecidableRel fun a b => a ∣ b
inst✝ : UniqueFactorizationMonoid M
a q : M
a✝ : a ≠ 0
hq : Prime q
ha : ¬q = 0 ∧ ¬a = 0
c : M
hb : ¬a * c = 0
IH : a ≠ 0 → (∀ (p : M), Prime p → multiplicity p a ≤ multiplicity p (a * c)) → a ∣ a * c
H : ∀ (p : M), Prime p → multiplicity p (q * a) ≤ multiplicity p (a * c)
⊢ a * q ∣ a * c
Theorem: dvd_iff_multiplicity_le
Proof state before:
case neg.hi.intro
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁵ : Field K
inst✝⁴ : CharZero K
inst✝³ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
M : Type u_2
inst✝² : CancelCommMonoidWithZero M
inst✝¹ : DecidableRel fun a b => a ∣ b
inst✝ : UniqueFactorizationMonoid M
a q : M
a✝ : a ≠ 0
hq : Prime q
ha : ¬q = 0 ∧ ¬a = 0
c : M
hb : ¬a * c = 0
IH : a ≠ 0 → (∀ (p : M), Prime p → multiplicity p a ≤ multiplicity p (a * c)) → a ∣ a * c
H : ∀ (p : M), Prime p → multiplicity p (q * a) ≤ multiplicity p (a * c)
⊢ a * q ∣ a * c
Tactic:
simp only [ne_eq, mul_eq_zero, not_or] at hb
Proof state after:
case neg.hi.intro
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁵ : Field K
inst✝⁴ : CharZero K
inst✝³ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
M : Type u_2
inst✝² : CancelCommMonoidWithZero M
inst✝¹ : DecidableRel fun a b => a ∣ b
inst✝ : UniqueFactorizationMonoid M
a q : M
a✝ : a ≠ 0
hq : Prime q
ha : ¬q = 0 ∧ ¬a = 0
c : M
IH : a ≠ 0 → (∀ (p : M), Prime p → multiplicity p a ≤ multiplicity p (a * c)) → a ∣ a * c
H : ∀ (p : M), Prime p → multiplicity p (q * a) ≤ multiplicity p (a * c)
hb : ¬a = 0 ∧ ¬c = 0
⊢ a * q ∣ a * c
Theorem: dvd_iff_multiplicity_le
Proof state before:
case neg.hi.intro
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁵ : Field K
inst✝⁴ : CharZero K
inst✝³ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
M : Type u_2
inst✝² : CancelCommMonoidWithZero M
inst✝¹ : DecidableRel fun a b => a ∣ b
inst✝ : UniqueFactorizationMonoid M
a q : M
a✝ : a ≠ 0
hq : Prime q
ha : ¬q = 0 ∧ ¬a = 0
c : M
IH : a ≠ 0 → (∀ (p : M), Prime p → multiplicity p a ≤ multiplicity p (a * c)) → a ∣ a * c
H : ∀ (p : M), Prime p → multiplicity p (q * a) ≤ multiplicity p (a * c)
hb : ¬a = 0 ∧ ¬c = 0
⊢ a * q ∣ a * c
Tactic:
have := H q hq
Proof state after:
case neg.hi.intro
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁵ : Field K
inst✝⁴ : CharZero K
inst✝³ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
M : Type u_2
inst✝² : CancelCommMonoidWithZero M
inst✝¹ : DecidableRel fun a b => a ∣ b
inst✝ : UniqueFactorizationMonoid M
a q : M
a✝ : a ≠ 0
hq : Prime q
ha : ¬q = 0 ∧ ¬a = 0
c : M
IH : a ≠ 0 → (∀ (p : M), Prime p → multiplicity p a ≤ multiplicity p (a * c)) → a ∣ a * c
H : ∀ (p : M), Prime p → multiplicity p (q * a) ≤ multiplicity p (a * c)
hb : ¬a = 0 ∧ ¬c = 0
this : multiplicity q (q * a) ≤ multiplicity q (a * c)
⊢ a * q ∣ a * c
Theorem: dvd_iff_multiplicity_le
Proof state before:
case neg.hi.intro
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁵ : Field K
inst✝⁴ : CharZero K
inst✝³ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
M : Type u_2
inst✝² : CancelCommMonoidWithZero M
inst✝¹ : DecidableRel fun a b => a ∣ b
inst✝ : UniqueFactorizationMonoid M
a q : M
a✝ : a ≠ 0
hq : Prime q
ha : ¬q = 0 ∧ ¬a = 0
c : M
IH : a ≠ 0 → (∀ (p : M), Prime p → multiplicity p a ≤ multiplicity p (a * c)) → a ∣ a * c
H : ∀ (p : M), Prime p → multiplicity p (q * a) ≤ multiplicity p (a * c)
hb : ¬a = 0 ∧ ¬c = 0
this : multiplicity q (q * a) ≤ multiplicity q (a * c)
⊢ a * q ∣ a * c
Tactic:
rw [multiplicity.mul hq, multiplicity.mul hq, add_comm,
  ← PartENat.natCast_get (multiplicity.finite_iff_dom.mp
    (WfDvdMonoid.multiplicity_finite hq.not_unit ha.2)),
  ← PartENat.natCast_get (multiplicity.finite_iff_dom.mp
    (WfDvdMonoid.multiplicity_finite hq.not_unit hb.2)),
  ← PartENat.natCast_get (multiplicity.finite_iff_dom.mp
    (WfDvdMonoid.multiplicity_finite hq.not_unit ha.1)),
  ← Nat.cast_add, ← Nat.cast_add, PartENat.coe_le_coe,
  multiplicity.get_multiplicity_self, add_le_add_iff_left,
  ← PartENat.coe_le_coe, PartENat.natCast_get, ← multiplicity.pow_dvd_iff_le_multiplicity,
  pow_one] at this
Proof state after:
case neg.hi.intro
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁵ : Field K
inst✝⁴ : CharZero K
inst✝³ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
M : Type u_2
inst✝² : CancelCommMonoidWithZero M
inst✝¹ : DecidableRel fun a b => a ∣ b
inst✝ : UniqueFactorizationMonoid M
a q : M
a✝ : a ≠ 0
hq : Prime q
ha : ¬q = 0 ∧ ¬a = 0
c : M
IH : a ≠ 0 → (∀ (p : M), Prime p → multiplicity p a ≤ multiplicity p (a * c)) → a ∣ a * c
H : ∀ (p : M), Prime p → multiplicity p (q * a) ≤ multiplicity p (a * c)
hb : ¬a = 0 ∧ ¬c = 0
this : q ∣ c
⊢ a * q ∣ a * c
Theorem: dvd_iff_multiplicity_le
Proof state before:
case neg.hi.intro
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁵ : Field K
inst✝⁴ : CharZero K
inst✝³ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
M : Type u_2
inst✝² : CancelCommMonoidWithZero M
inst✝¹ : DecidableRel fun a b => a ∣ b
inst✝ : UniqueFactorizationMonoid M
a q : M
a✝ : a ≠ 0
hq : Prime q
ha : ¬q = 0 ∧ ¬a = 0
c : M
IH : a ≠ 0 → (∀ (p : M), Prime p → multiplicity p a ≤ multiplicity p (a * c)) → a ∣ a * c
H : ∀ (p : M), Prime p → multiplicity p (q * a) ≤ multiplicity p (a * c)
hb : ¬a = 0 ∧ ¬c = 0
this : q ∣ c
⊢ a * q ∣ a * c
Tactic:
exact mul_dvd_mul_left _ this
Proof state after:
no goals
Theorem: dvd_iff_multiplicity_le
Proof state before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁵ : Field K
inst✝⁴ : CharZero K
inst✝³ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
M : Type u_2
inst✝² : CancelCommMonoidWithZero M
inst✝¹ : DecidableRel fun a b => a ∣ b
inst✝ : UniqueFactorizationMonoid M
b : M
hb : ¬b = 0
a q : M
a✝ : a ≠ 0
hq : Prime q
IH : a ≠ 0 → (∀ (p : M), Prime p → multiplicity p a ≤ multiplicity p b) → a ∣ b
H : ∀ (p : M), Prime p → multiplicity p (q * a) ≤ multiplicity p b
ha : ¬q = 0 ∧ ¬a = 0
⊢ a ∣ b
Tactic:
refine' IH ha.2 (fun p hp ↦ (le_trans ?_ (H p hp)))
Proof state after:
K : Type u_1
p✝ : ℕ+
hpri : Fact p✝.Prime
inst✝⁵ : Field K
inst✝⁴ : CharZero K
inst✝³ : IsCyclotomicExtension {p✝} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p✝
M : Type u_2
inst✝² : CancelCommMonoidWithZero M
inst✝¹ : DecidableRel fun a b => a ∣ b
inst✝ : UniqueFactorizationMonoid M
b : M
hb : ¬b = 0
a q : M
a✝ : a ≠ 0
hq : Prime q
IH : a ≠ 0 → (∀ (p : M), Prime p → multiplicity p a ≤ multiplicity p b) → a ∣ b
H : ∀ (p : M), Prime p → multiplicity p (q * a) ≤ multiplicity p b
ha : ¬q = 0 ∧ ¬a = 0
p : M
hp : Prime p
⊢ multiplicity p a ≤ multiplicity p (q * a)
Theorem: dvd_iff_multiplicity_le
Proof state before:
K : Type u_1
p✝ : ℕ+
hpri : Fact p✝.Prime
inst✝⁵ : Field K
inst✝⁴ : CharZero K
inst✝³ : IsCyclotomicExtension {p✝} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p✝
M : Type u_2
inst✝² : CancelCommMonoidWithZero M
inst✝¹ : DecidableRel fun a b => a ∣ b
inst✝ : UniqueFactorizationMonoid M
b : M
hb : ¬b = 0
a q : M
a✝ : a ≠ 0
hq : Prime q
IH : a ≠ 0 → (∀ (p : M), Prime p → multiplicity p a ≤ multiplicity p b) → a ∣ b
H : ∀ (p : M), Prime p → multiplicity p (q * a) ≤ multiplicity p b
ha : ¬q = 0 ∧ ¬a = 0
p : M
hp : Prime p
⊢ multiplicity p a ≤ multiplicity p (q * a)
Tactic:
rw [multiplicity.mul hp]
Proof state after:
K : Type u_1
p✝ : ℕ+
hpri : Fact p✝.Prime
inst✝⁵ : Field K
inst✝⁴ : CharZero K
inst✝³ : IsCyclotomicExtension {p✝} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p✝
M : Type u_2
inst✝² : CancelCommMonoidWithZero M
inst✝¹ : DecidableRel fun a b => a ∣ b
inst✝ : UniqueFactorizationMonoid M
b : M
hb : ¬b = 0
a q : M
a✝ : a ≠ 0
hq : Prime q
IH : a ≠ 0 → (∀ (p : M), Prime p → multiplicity p a ≤ multiplicity p b) → a ∣ b
H : ∀ (p : M), Prime p → multiplicity p (q * a) ≤ multiplicity p b
ha : ¬q = 0 ∧ ¬a = 0
p : M
hp : Prime p
⊢ multiplicity p a ≤ multiplicity p q + multiplicity p a
Theorem: dvd_iff_multiplicity_le
Proof state before:
K : Type u_1
p✝ : ℕ+
hpri : Fact p✝.Prime
inst✝⁵ : Field K
inst✝⁴ : CharZero K
inst✝³ : IsCyclotomicExtension {p✝} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p✝
M : Type u_2
inst✝² : CancelCommMonoidWithZero M
inst✝¹ : DecidableRel fun a b => a ∣ b
inst✝ : UniqueFactorizationMonoid M
b : M
hb : ¬b = 0
a q : M
a✝ : a ≠ 0
hq : Prime q
IH : a ≠ 0 → (∀ (p : M), Prime p → multiplicity p a ≤ multiplicity p b) → a ∣ b
H : ∀ (p : M), Prime p → multiplicity p (q * a) ≤ multiplicity p b
ha : ¬q = 0 ∧ ¬a = 0
p : M
hp : Prime p
⊢ multiplicity p a ≤ multiplicity p q + multiplicity p a
Tactic:
exact le_add_self
Proof state after:
no goals