Theorem: pow_dvd_pow_iff_dvd (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✝ : UniqueFactorizationMonoid M
a b : M
x : ℕ
h' : x ≠ 0
⊢ a ^ x ∣ b ^ x ↔ a ∣ b
Tactic:
by_cases ha : a = 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✝ : UniqueFactorizationMonoid M
a b : M
x : ℕ
h' : x ≠ 0
ha : a = 0
⊢ a ^ x ∣ b ^ x ↔ 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✝ : UniqueFactorizationMonoid M
a b : M
x : ℕ
h' : x ≠ 0
ha : ¬a = 0
⊢ a ^ x ∣ b ^ x ↔ 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✝ : UniqueFactorizationMonoid M
a b : M
x : ℕ
h' : x ≠ 0
ha : ¬a = 0
⊢ a ^ x ∣ b ^ x ↔ a ∣ b
Tactic:
have ha' : a ^ x ≠ 0 := (pow_ne_zero_iff h').mpr ha
State after:
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✝ : UniqueFactorizationMonoid M
a b : M
x : ℕ
h' : x ≠ 0
ha : ¬a = 0
ha' : a ^ x ≠ 0
⊢ a ^ x ∣ b ^ x ↔ 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✝ : UniqueFactorizationMonoid M
a b : M
x : ℕ
h' : x ≠ 0
ha : ¬a = 0
ha' : a ^ x ≠ 0
⊢ a ^ x ∣ b ^ x ↔ a ∣ b
Tactic:
rw [dvd_iff_multiplicity_le ha, dvd_iff_multiplicity_le ha']
State after:
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✝ : UniqueFactorizationMonoid M
a b : M
x : ℕ
h' : x ≠ 0
ha : ¬a = 0
ha' : a ^ x ≠ 0
⊢ (∀ (p : M), Prime p → multiplicity p (a ^ x) ≤ multiplicity p (b ^ x)) ↔
    ∀ (p : M), Prime p → multiplicity p a ≤ multiplicity p 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✝ : UniqueFactorizationMonoid M
a b : M
x : ℕ
h' : x ≠ 0
ha : ¬a = 0
ha' : a ^ x ≠ 0
⊢ (∀ (p : M), Prime p → multiplicity p (a ^ x) ≤ multiplicity p (b ^ x)) ↔
    ∀ (p : M), Prime p → multiplicity p a ≤ multiplicity p b
Tactic:
refine forall₂_congr (fun p hp ↦ ?_)
State after:
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✝ : UniqueFactorizationMonoid M
a b : M
x : ℕ
h' : x ≠ 0
ha : ¬a = 0
ha' : a ^ x ≠ 0
p : M
hp : Prime p
⊢ multiplicity p (a ^ x) ≤ multiplicity p (b ^ x) ↔ multiplicity p a ≤ multiplicity p 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✝ : UniqueFactorizationMonoid M
a b : M
x : ℕ
h' : x ≠ 0
ha : ¬a = 0
ha' : a ^ x ≠ 0
p : M
hp : Prime p
⊢ multiplicity p (a ^ x) ≤ multiplicity p (b ^ x) ↔ multiplicity p a ≤ multiplicity p b
Tactic:
simp_rw [multiplicity.pow hp, ← PartENat.withTopEquiv_le]
State after:
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✝ : UniqueFactorizationMonoid M
a b : M
x : ℕ
h' : x ≠ 0
ha : ¬a = 0
ha' : a ^ x ≠ 0
p : M
hp : Prime p
⊢ PartENat.withTopEquiv (x • multiplicity p a) ≤ PartENat.withTopEquiv (x • multiplicity p b) ↔
    PartENat.withTopEquiv (multiplicity p a) ≤ PartENat.withTopEquiv (multiplicity p 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✝ : UniqueFactorizationMonoid M
a b : M
x : ℕ
h' : x ≠ 0
ha : ¬a = 0
ha' : a ^ x ≠ 0
p : M
hp : Prime p
⊢ PartENat.withTopEquiv (x • multiplicity p a) ≤ PartENat.withTopEquiv (x • multiplicity p b) ↔
    PartENat.withTopEquiv (multiplicity p a) ≤ PartENat.withTopEquiv (multiplicity p b)
Tactic:
show PartENat.withTopAddEquiv _ ≤ PartENat.withTopAddEquiv _ ↔ _
State after:
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✝ : UniqueFactorizationMonoid M
a b : M
x : ℕ
h' : x ≠ 0
ha : ¬a = 0
ha' : a ^ x ≠ 0
p : M
hp : Prime p
⊢ PartENat.withTopAddEquiv (x • multiplicity p a) ≤ PartENat.withTopAddEquiv (x • multiplicity p b) ↔
    PartENat.withTopEquiv (multiplicity p a) ≤ PartENat.withTopEquiv (multiplicity p 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✝ : UniqueFactorizationMonoid M
a b : M
x : ℕ
h' : x ≠ 0
ha : ¬a = 0
ha' : a ^ x ≠ 0
p : M
hp : Prime p
⊢ PartENat.withTopAddEquiv (x • multiplicity p a) ≤ PartENat.withTopAddEquiv (x • multiplicity p b) ↔
    PartENat.withTopEquiv (multiplicity p a) ≤ PartENat.withTopEquiv (multiplicity p b)
Tactic:
simp_rw [map_nsmul]
State after:
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✝ : UniqueFactorizationMonoid M
a b : M
x : ℕ
h' : x ≠ 0
ha : ¬a = 0
ha' : a ^ x ≠ 0
p : M
hp : Prime p
⊢ x • PartENat.withTopAddEquiv (multiplicity p a) ≤ x • PartENat.withTopAddEquiv (multiplicity p b) ↔
    PartENat.withTopEquiv (multiplicity p a) ≤ PartENat.withTopEquiv (multiplicity p 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✝ : UniqueFactorizationMonoid M
a b : M
x : ℕ
h' : x ≠ 0
ha : ¬a = 0
ha' : a ^ x ≠ 0
p : M
hp : Prime p
⊢ x • PartENat.withTopAddEquiv (multiplicity p a) ≤ x • PartENat.withTopAddEquiv (multiplicity p b) ↔
    PartENat.withTopEquiv (multiplicity p a) ≤ PartENat.withTopEquiv (multiplicity p b)
Tactic:
rw [ENat.nsmul_mono h']
State after:
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✝ : UniqueFactorizationMonoid M
a b : M
x : ℕ
h' : x ≠ 0
ha : ¬a = 0
ha' : a ^ x ≠ 0
p : M
hp : Prime p
⊢ PartENat.withTopAddEquiv (multiplicity p a) ≤ PartENat.withTopAddEquiv (multiplicity p b) ↔
    PartENat.withTopEquiv (multiplicity p a) ≤ PartENat.withTopEquiv (multiplicity p 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✝ : UniqueFactorizationMonoid M
a b : M
x : ℕ
h' : x ≠ 0
ha : ¬a = 0
ha' : a ^ x ≠ 0
p : M
hp : Prime p
⊢ PartENat.withTopAddEquiv (multiplicity p a) ≤ PartENat.withTopAddEquiv (multiplicity p b) ↔
    PartENat.withTopEquiv (multiplicity p a) ≤ PartENat.withTopEquiv (multiplicity p b)
Tactic:
rfl
State after:
no goals

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✝ : UniqueFactorizationMonoid M
a b : M
x : ℕ
h' : x ≠ 0
ha : a = 0
⊢ a ^ x ∣ b ^ x ↔ a ∣ b
Tactic:
rw [ha, zero_pow h', zero_dvd_iff, zero_dvd_iff, pow_eq_zero_iff h']
State after:
no goals