Theorem: WfDvdMonoid.multiplicity_finite (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✝ : WfDvdMonoid M
x y : M
hx : ¬IsUnit x
hy : y ≠ 0
⊢ multiplicity.Finite x y
Tactic:
by_contra h
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✝ : WfDvdMonoid M
x y : M
hx : ¬IsUnit x
hy : y ≠ 0
h : ¬multiplicity.Finite x y
⊢ False

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
x y : M
hx : ¬IsUnit x
hy : y ≠ 0
h : ¬multiplicity.Finite x y
⊢ False
Tactic:
rw [multiplicity.Finite, not_exists_not] at h
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✝ : WfDvdMonoid M
x y : M
hx : ¬IsUnit x
hy : y ≠ 0
h : ∀ (x_1 : ℕ), x ^ (x_1 + 1) ∣ y
⊢ False

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
x y : M
hx : ¬IsUnit x
hy : y ≠ 0
h : ∀ (x_1 : ℕ), x ^ (x_1 + 1) ∣ y
⊢ False
Tactic:
choose f hf using h
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✝ : WfDvdMonoid M
x y : M
hx : ¬IsUnit x
hy : y ≠ 0
f : ℕ → M
hf : ∀ (x_1 : ℕ), y = x ^ (x_1 + 1) * f x_1
⊢ False

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
x y : M
hx : ¬IsUnit x
hy : y ≠ 0
f : ℕ → M
hf : ∀ (x_1 : ℕ), y = x ^ (x_1 + 1) * f x_1
⊢ False
Tactic:
obtain ⟨_, ⟨n, rfl⟩, hn⟩ :=
  (WfDvdMonoid.wellFounded_dvdNotUnit (α := M)).has_min (Set.range f) (Set.range_nonempty f)
State after:
case intro.intro.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✝ : WfDvdMonoid M
x y : M
hx : ¬IsUnit x
hy : y ≠ 0
f : ℕ → M
hf : ∀ (x_1 : ℕ), y = x ^ (x_1 + 1) * f x_1
n : ℕ
hn : ∀ x ∈ Set.range f, ¬DvdNotUnit x (f n)
⊢ False

State before:
case intro.intro.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✝ : WfDvdMonoid M
x y : M
hx : ¬IsUnit x
hy : y ≠ 0
f : ℕ → M
hf : ∀ (x_1 : ℕ), y = x ^ (x_1 + 1) * f x_1
n : ℕ
hn : ∀ x ∈ Set.range f, ¬DvdNotUnit x (f n)
⊢ False
Tactic:
apply hn _ ⟨n + 1, rfl⟩
State after:
case intro.intro.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✝ : WfDvdMonoid M
x y : M
hx : ¬IsUnit x
hy : y ≠ 0
f : ℕ → M
hf : ∀ (x_1 : ℕ), y = x ^ (x_1 + 1) * f x_1
n : ℕ
hn : ∀ x ∈ Set.range f, ¬DvdNotUnit x (f n)
⊢ DvdNotUnit (f (n + 1)) (f n)

State before:
case intro.intro.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✝ : WfDvdMonoid M
x y : M
hx : ¬IsUnit x
hy : y ≠ 0
f : ℕ → M
hf : ∀ (x_1 : ℕ), y = x ^ (x_1 + 1) * f x_1
n : ℕ
hn : ∀ x ∈ Set.range f, ¬DvdNotUnit x (f n)
⊢ DvdNotUnit (f (n + 1)) (f n)
Tactic:
constructor
State after:
case intro.intro.intro.left
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
f : ℕ → M
hf : ∀ (x_1 : ℕ), y = x ^ (x_1 + 1) * f x_1
n : ℕ
hn : ∀ x ∈ Set.range f, ¬DvdNotUnit x (f n)
⊢ f (n + 1) ≠ 0

case intro.intro.intro.right
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
f : ℕ → M
hf : ∀ (x_1 : ℕ), y = x ^ (x_1 + 1) * f x_1
n : ℕ
hn : ∀ x ∈ Set.range f, ¬DvdNotUnit x (f n)
⊢ ∃ x, ¬IsUnit x ∧ f n = f (n + 1) * x

State before:
case intro.intro.intro.left
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
f : ℕ → M
hf : ∀ (x_1 : ℕ), y = x ^ (x_1 + 1) * f x_1
n : ℕ
hn : ∀ x ∈ Set.range f, ¬DvdNotUnit x (f n)
⊢ f (n + 1) ≠ 0
Tactic:
intro e
State after:
case intro.intro.intro.left
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
f : ℕ → M
hf : ∀ (x_1 : ℕ), y = x ^ (x_1 + 1) * f x_1
n : ℕ
hn : ∀ x ∈ Set.range f, ¬DvdNotUnit x (f n)
e : f (n + 1) = 0
⊢ False

State before:
case intro.intro.intro.left
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
f : ℕ → M
hf : ∀ (x_1 : ℕ), y = x ^ (x_1 + 1) * f x_1
n : ℕ
hn : ∀ x ∈ Set.range f, ¬DvdNotUnit x (f n)
e : f (n + 1) = 0
⊢ False
Tactic:
apply hy
State after:
case intro.intro.intro.left
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
f : ℕ → M
hf : ∀ (x_1 : ℕ), y = x ^ (x_1 + 1) * f x_1
n : ℕ
hn : ∀ x ∈ Set.range f, ¬DvdNotUnit x (f n)
e : f (n + 1) = 0
⊢ y = 0

State before:
case intro.intro.intro.left
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
f : ℕ → M
hf : ∀ (x_1 : ℕ), y = x ^ (x_1 + 1) * f x_1
n : ℕ
hn : ∀ x ∈ Set.range f, ¬DvdNotUnit x (f n)
e : f (n + 1) = 0
⊢ y = 0
Tactic:
rw [hf (n + 1), e, mul_zero]
State after:
no goals

State before:
case intro.intro.intro.right
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
f : ℕ → M
hf : ∀ (x_1 : ℕ), y = x ^ (x_1 + 1) * f x_1
n : ℕ
hn : ∀ x ∈ Set.range f, ¬DvdNotUnit x (f n)
⊢ ∃ x, ¬IsUnit x ∧ f n = f (n + 1) * x
Tactic:
refine ⟨x, hx, ?_⟩
State after:
case intro.intro.intro.right
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
f : ℕ → M
hf : ∀ (x_1 : ℕ), y = x ^ (x_1 + 1) * f x_1
n : ℕ
hn : ∀ x ∈ Set.range f, ¬DvdNotUnit x (f n)
⊢ f n = f (n + 1) * x

State before:
case intro.intro.intro.right
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
f : ℕ → M
hf : ∀ (x_1 : ℕ), y = x ^ (x_1 + 1) * f x_1
n : ℕ
hn : ∀ x ∈ Set.range f, ¬DvdNotUnit x (f n)
⊢ f n = f (n + 1) * x
Tactic:
rw [mul_comm, ← (mul_right_injective₀ (a := x ^ (n + 1)) _).eq_iff]
State after:
case intro.intro.intro.right
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
f : ℕ → M
hf : ∀ (x_1 : ℕ), y = x ^ (x_1 + 1) * f x_1
n : ℕ
hn : ∀ x ∈ Set.range f, ¬DvdNotUnit x (f n)
⊢ x ^ (n + 1) * f n = x ^ (n + 1) * (x * f (n + 1))

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
f : ℕ → M
hf : ∀ (x_1 : ℕ), y = x ^ (x_1 + 1) * f x_1
n : ℕ
hn : ∀ x ∈ Set.range f, ¬DvdNotUnit x (f n)
⊢ x ^ (n + 1) ≠ 0

State before:
case intro.intro.intro.right
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
f : ℕ → M
hf : ∀ (x_1 : ℕ), y = x ^ (x_1 + 1) * f x_1
n : ℕ
hn : ∀ x ∈ Set.range f, ¬DvdNotUnit x (f n)
⊢ x ^ (n + 1) * f n = x ^ (n + 1) * (x * f (n + 1))
Tactic:
simp only [← mul_assoc, ← pow_succ, ← hf]
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✝ : WfDvdMonoid M
x y : M
hx : ¬IsUnit x
hy : y ≠ 0
f : ℕ → M
hf : ∀ (x_1 : ℕ), y = x ^ (x_1 + 1) * f x_1
n : ℕ
hn : ∀ x ∈ Set.range f, ¬DvdNotUnit x (f n)
⊢ x ^ (n + 1) ≠ 0
Tactic:
intro e
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✝ : WfDvdMonoid M
x y : M
hx : ¬IsUnit x
hy : y ≠ 0
f : ℕ → M
hf : ∀ (x_1 : ℕ), y = x ^ (x_1 + 1) * f x_1
n : ℕ
hn : ∀ x ∈ Set.range f, ¬DvdNotUnit x (f n)
e : x ^ (n + 1) = 0
⊢ False

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
x y : M
hx : ¬IsUnit x
hy : y ≠ 0
f : ℕ → M
hf : ∀ (x_1 : ℕ), y = x ^ (x_1 + 1) * f x_1
n : ℕ
hn : ∀ x ∈ Set.range f, ¬DvdNotUnit x (f n)
e : x ^ (n + 1) = 0
⊢ False
Tactic:
apply hy
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✝ : WfDvdMonoid M
x y : M
hx : ¬IsUnit x
hy : y ≠ 0
f : ℕ → M
hf : ∀ (x_1 : ℕ), y = x ^ (x_1 + 1) * f x_1
n : ℕ
hn : ∀ x ∈ Set.range f, ¬DvdNotUnit x (f n)
e : x ^ (n + 1) = 0
⊢ y = 0

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
x y : M
hx : ¬IsUnit x
hy : y ≠ 0
f : ℕ → M
hf : ∀ (x_1 : ℕ), y = x ^ (x_1 + 1) * f x_1
n : ℕ
hn : ∀ x ∈ Set.range f, ¬DvdNotUnit x (f n)
e : x ^ (n + 1) = 0
⊢ y = 0
Tactic:
rw [hf n, e, zero_mul]
State after:
no goals