Theorem: dvd_iff_multiplicity_le (FltRegular/CaseII/AuxLemmas.lean)

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

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 _
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

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
State after:
no goals

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

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

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

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
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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

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

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

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]
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

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

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

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

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
State after:
no goals

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)))
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)

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]
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

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
State after:
no goals