[GOAL]
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
t : Finset ι
h : Finset.Nonempty t
I : ι → Ideal R
⊢ ⨆ (i : ι) (_ : i ∈ t), ⨅ (j : ι) (_ : j ∈ t) (_ : j ≠ i), I j = ⊤ ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
[PROOFSTEP]
haveI : DecidableEq ι := Classical.decEq ι
[GOAL]
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
t : Finset ι
h : Finset.Nonempty t
I : ι → Ideal R
this : DecidableEq ι
⊢ ⨆ (i : ι) (_ : i ∈ t), ⨅ (j : ι) (_ : j ∈ t) (_ : j ≠ i), I j = ⊤ ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
[PROOFSTEP]
rw [eq_top_iff_one, Submodule.mem_iSup_finset_iff_exists_sum]
[GOAL]
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
t : Finset ι
h : Finset.Nonempty t
I : ι → Ideal R
this : DecidableEq ι
⊢ (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
[PROOFSTEP]
refine' h.cons_induction _ _
[GOAL]
case refine'_1
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
t : Finset ι
h : Finset.Nonempty t
I : ι → Ideal R
this : DecidableEq ι
⊢ ∀ (a : ι), (∃ μ, (Finset.sum {a} fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑{a} fun i j => I i ⊔ I j = ⊤
[PROOFSTEP]
clear t h
[GOAL]
case refine'_2
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
t : Finset ι
h : Finset.Nonempty t
I : ι → Ideal R
this : DecidableEq ι
⊢ ∀ ⦃a : ι⦄ (s : Finset ι) (h : ¬a ∈ s),
    Finset.Nonempty s →
      ((∃ μ, (Finset.sum s fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑s fun i j => I i ⊔ I j = ⊤) →
        ((∃ μ, (Finset.sum (Finset.cons a s h) fun i => ↑(μ i)) = 1) ↔
          Set.Pairwise ↑(Finset.cons a s h) fun i j => I i ⊔ I j = ⊤)
[PROOFSTEP]
clear t h
[GOAL]
case refine'_1
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
⊢ ∀ (a : ι), (∃ μ, (Finset.sum {a} fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑{a} fun i j => I i ⊔ I j = ⊤
[PROOFSTEP]
simp only [Finset.sum_singleton, Finset.coe_singleton, Set.pairwise_singleton, iff_true_iff]
[GOAL]
case refine'_1
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
⊢ ∀ (a : ι), ∃ μ, ↑(μ a) = 1
[PROOFSTEP]
refine' fun a => ⟨fun i => if h : i = a then ⟨1, _⟩ else 0, _⟩
[GOAL]
case refine'_1.refine'_1
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a i : ι
h : i = a
⊢ 1 ∈ ⨅ (j : ι) (_ : j ∈ {a}) (_ : j ≠ i), I j
[PROOFSTEP]
simp [h]
[GOAL]
case refine'_1.refine'_2
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
⊢ ↑((fun i => if h : i = a then { val := 1, property := (_ : 1 ∈ ⨅ (x : ι) (_ : x ∈ {a}) (_ : x ≠ i), I x) } else 0)
        a) =
    1
[PROOFSTEP]
simp only [dif_pos, dif_ctx_congr, Submodule.coe_mk, eq_self_iff_true]
[GOAL]
case refine'_2
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
⊢ ∀ ⦃a : ι⦄ (s : Finset ι) (h : ¬a ∈ s),
    Finset.Nonempty s →
      ((∃ μ, (Finset.sum s fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑s fun i j => I i ⊔ I j = ⊤) →
        ((∃ μ, (Finset.sum (Finset.cons a s h) fun i => ↑(μ i)) = 1) ↔
          Set.Pairwise ↑(Finset.cons a s h) fun i j => I i ⊔ I j = ⊤)
[PROOFSTEP]
intro a t hat h ih
[GOAL]
case refine'_2
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
⊢ (∃ μ, (Finset.sum (Finset.cons a t hat) fun i => ↑(μ i)) = 1) ↔
    Set.Pairwise ↑(Finset.cons a t hat) fun i j => I i ⊔ I j = ⊤
[PROOFSTEP]
rw [Finset.coe_cons, Set.pairwise_insert_of_symmetric fun i j (h : I i ⊔ I j = ⊤) => sup_comm.trans h]
[GOAL]
case refine'_2
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
⊢ (∃ μ, (Finset.sum (Finset.cons a t hat) fun i => ↑(μ i)) = 1) ↔
    (Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤) ∧ ∀ (b : ι), b ∈ ↑t → a ≠ b → I a ⊔ I b = ⊤
[PROOFSTEP]
constructor
[GOAL]
case refine'_2.mp
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
⊢ (∃ μ, (Finset.sum (Finset.cons a t hat) fun i => ↑(μ i)) = 1) →
    (Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤) ∧ ∀ (b : ι), b ∈ ↑t → a ≠ b → I a ⊔ I b = ⊤
[PROOFSTEP]
rintro ⟨μ, hμ⟩
[GOAL]
case refine'_2.mp.intro
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ i), I j }
hμ : (Finset.sum (Finset.cons a t hat) fun i => ↑(μ i)) = 1
⊢ (Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤) ∧ ∀ (b : ι), b ∈ ↑t → a ≠ b → I a ⊔ I b = ⊤
[PROOFSTEP]
rw [Finset.sum_cons] at hμ
[GOAL]
case refine'_2.mp.intro
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ i), I j }
hμ : (↑(μ a) + Finset.sum t fun x => ↑(μ x)) = 1
⊢ (Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤) ∧ ∀ (b : ι), b ∈ ↑t → a ≠ b → I a ⊔ I b = ⊤
[PROOFSTEP]
refine ⟨ih.mp ⟨Pi.single h.choose ⟨μ a, ?a1⟩ + fun i => ⟨μ i, ?a2⟩, ?a3⟩, fun b hb ab => ?a4⟩
[GOAL]
case a3
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ i), I j }
hμ : (↑(μ a) + Finset.sum t fun x => ↑(μ x)) = 1
⊢ (Finset.sum t fun i => ↑((Pi.single (Exists.choose h) { val := ↑(μ a), property := ?a1 } + fun i => ?m.8605 i) i)) = 1
case a4
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ i), I j }
hμ : (↑(μ a) + Finset.sum t fun x => ↑(μ x)) = 1
b : ι
hb : b ∈ ↑t
ab : a ≠ b
⊢ I a ⊔ I b = ⊤
case a1
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ i), I j }
hμ : (↑(μ a) + Finset.sum t fun x => ↑(μ x)) = 1
⊢ ↑(μ a) ∈ ⨅ (j : ι) (_ : j ∈ t) (_ : j ≠ Exists.choose h), I j
case a2
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ i), I j }
hμ : (↑(μ a) + Finset.sum t fun x => ↑(μ x)) = 1
i : ι
⊢ ↑(μ i) ∈ ⨅ (j : ι) (_ : j ∈ t) (_ : j ≠ i), I j
[PROOFSTEP]
case a1 =>
  have := Submodule.coe_mem (μ a)
  rw [mem_iInf] at this ⊢
    --for some reason `simp only [mem_iInf]` times out
  intro i
  specialize this i
  rw [mem_iInf, mem_iInf] at this ⊢
  intro hi _
  apply this (Finset.subset_cons _ hi)
  rintro rfl
  exact hat hi
[GOAL]
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ i), I j }
hμ : (↑(μ a) + Finset.sum t fun x => ↑(μ x)) = 1
⊢ ↑(μ a) ∈ ⨅ (j : ι) (_ : j ∈ t) (_ : j ≠ Exists.choose h), I j
[PROOFSTEP]
case a1 =>
  have := Submodule.coe_mem (μ a)
  rw [mem_iInf] at this ⊢
    --for some reason `simp only [mem_iInf]` times out
  intro i
  specialize this i
  rw [mem_iInf, mem_iInf] at this ⊢
  intro hi _
  apply this (Finset.subset_cons _ hi)
  rintro rfl
  exact hat hi
[GOAL]
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ i), I j }
hμ : (↑(μ a) + Finset.sum t fun x => ↑(μ x)) = 1
⊢ ↑(μ a) ∈ ⨅ (j : ι) (_ : j ∈ t) (_ : j ≠ Exists.choose h), I j
[PROOFSTEP]
have := Submodule.coe_mem (μ a)
[GOAL]
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝ : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ i), I j }
hμ : (↑(μ a) + Finset.sum t fun x => ↑(μ x)) = 1
this : ↑(μ a) ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ a), I j
⊢ ↑(μ a) ∈ ⨅ (j : ι) (_ : j ∈ t) (_ : j ≠ Exists.choose h), I j
[PROOFSTEP]
rw [mem_iInf] at this ⊢
  --for some reason `simp only [mem_iInf]` times out
[GOAL]
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝ : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ i), I j }
hμ : (↑(μ a) + Finset.sum t fun x => ↑(μ x)) = 1
this : ∀ (i : ι), ↑(μ a) ∈ ⨅ (_ : i ∈ Finset.cons a t hat) (_ : i ≠ a), I i
⊢ ∀ (i : ι), ↑(μ a) ∈ ⨅ (_ : i ∈ t) (_ : i ≠ Exists.choose h), I i
[PROOFSTEP]
intro i
[GOAL]
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝ : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ i), I j }
hμ : (↑(μ a) + Finset.sum t fun x => ↑(μ x)) = 1
this : ∀ (i : ι), ↑(μ a) ∈ ⨅ (_ : i ∈ Finset.cons a t hat) (_ : i ≠ a), I i
i : ι
⊢ ↑(μ a) ∈ ⨅ (_ : i ∈ t) (_ : i ≠ Exists.choose h), I i
[PROOFSTEP]
specialize this i
[GOAL]
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝ : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ i), I j }
hμ : (↑(μ a) + Finset.sum t fun x => ↑(μ x)) = 1
i : ι
this : ↑(μ a) ∈ ⨅ (_ : i ∈ Finset.cons a t hat) (_ : i ≠ a), I i
⊢ ↑(μ a) ∈ ⨅ (_ : i ∈ t) (_ : i ≠ Exists.choose h), I i
[PROOFSTEP]
rw [mem_iInf, mem_iInf] at this ⊢
[GOAL]
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝ : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ i), I j }
hμ : (↑(μ a) + Finset.sum t fun x => ↑(μ x)) = 1
i : ι
this : i ∈ Finset.cons a t hat → i ≠ a → ↑(μ a) ∈ I i
⊢ i ∈ t → i ≠ Exists.choose h → ↑(μ a) ∈ I i
[PROOFSTEP]
intro hi _
[GOAL]
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝ : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ i), I j }
hμ : (↑(μ a) + Finset.sum t fun x => ↑(μ x)) = 1
i : ι
this : i ∈ Finset.cons a t hat → i ≠ a → ↑(μ a) ∈ I i
hi : i ∈ t
i✝ : i ≠ Exists.choose h
⊢ ↑(μ a) ∈ I i
[PROOFSTEP]
apply this (Finset.subset_cons _ hi)
[GOAL]
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝ : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ i), I j }
hμ : (↑(μ a) + Finset.sum t fun x => ↑(μ x)) = 1
i : ι
this : i ∈ Finset.cons a t hat → i ≠ a → ↑(μ a) ∈ I i
hi : i ∈ t
i✝ : i ≠ Exists.choose h
⊢ i ≠ a
[PROOFSTEP]
rintro rfl
[GOAL]
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝ : DecidableEq ι
t : Finset ι
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
i : ι
hi : i ∈ t
i✝ : i ≠ Exists.choose h
hat : ¬i ∈ t
μ : (i_1 : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons i t hat) (_ : j ≠ i_1), I j }
hμ : (↑(μ i) + Finset.sum t fun x => ↑(μ x)) = 1
this : i ∈ Finset.cons i t hat → i ≠ i → ↑(μ i) ∈ I i
⊢ False
[PROOFSTEP]
exact hat hi
[GOAL]
case a3
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ i), I j }
hμ : (↑(μ a) + Finset.sum t fun x => ↑(μ x)) = 1
⊢ (Finset.sum t fun i =>
      ↑((Pi.single (Exists.choose h)
              { val := ↑(μ a), property := (_ : ↑(μ a) ∈ ⨅ (j : ι) (_ : j ∈ t) (_ : j ≠ Exists.choose h), I j) } +
            fun i => ?m.8605 i)
          i)) =
    1
case a4
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ i), I j }
hμ : (↑(μ a) + Finset.sum t fun x => ↑(μ x)) = 1
b : ι
hb : b ∈ ↑t
ab : a ≠ b
⊢ I a ⊔ I b = ⊤
case a2
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ i), I j }
hμ : (↑(μ a) + Finset.sum t fun x => ↑(μ x)) = 1
i : ι
⊢ ↑(μ i) ∈ ⨅ (j : ι) (_ : j ∈ t) (_ : j ≠ i), I j
[PROOFSTEP]
case a2 =>
  have := Submodule.coe_mem (μ i)
  simp only [mem_iInf] at this ⊢
  intro j hj ij
  exact this _ (Finset.subset_cons _ hj) ij
[GOAL]
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ i), I j }
hμ : (↑(μ a) + Finset.sum t fun x => ↑(μ x)) = 1
i : ι
⊢ ↑(μ i) ∈ ⨅ (j : ι) (_ : j ∈ t) (_ : j ≠ i), I j
[PROOFSTEP]
case a2 =>
  have := Submodule.coe_mem (μ i)
  simp only [mem_iInf] at this ⊢
  intro j hj ij
  exact this _ (Finset.subset_cons _ hj) ij
[GOAL]
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ i), I j }
hμ : (↑(μ a) + Finset.sum t fun x => ↑(μ x)) = 1
i : ι
⊢ ↑(μ i) ∈ ⨅ (j : ι) (_ : j ∈ t) (_ : j ≠ i), I j
[PROOFSTEP]
have := Submodule.coe_mem (μ i)
[GOAL]
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝ : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ i), I j }
hμ : (↑(μ a) + Finset.sum t fun x => ↑(μ x)) = 1
i : ι
this : ↑(μ i) ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ i), I j
⊢ ↑(μ i) ∈ ⨅ (j : ι) (_ : j ∈ t) (_ : j ≠ i), I j
[PROOFSTEP]
simp only [mem_iInf] at this ⊢
[GOAL]
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝ : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ i), I j }
hμ : (↑(μ a) + Finset.sum t fun x => ↑(μ x)) = 1
i : ι
this : ∀ (i_1 : ι), i_1 ∈ Finset.cons a t hat → i_1 ≠ i → ↑(μ i) ∈ I i_1
⊢ ∀ (i_1 : ι), i_1 ∈ t → i_1 ≠ i → ↑(μ i) ∈ I i_1
[PROOFSTEP]
intro j hj ij
[GOAL]
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝ : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ i), I j }
hμ : (↑(μ a) + Finset.sum t fun x => ↑(μ x)) = 1
i : ι
this : ∀ (i_1 : ι), i_1 ∈ Finset.cons a t hat → i_1 ≠ i → ↑(μ i) ∈ I i_1
j : ι
hj : j ∈ t
ij : j ≠ i
⊢ ↑(μ i) ∈ I j
[PROOFSTEP]
exact this _ (Finset.subset_cons _ hj) ij
[GOAL]
case a3
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ i), I j }
hμ : (↑(μ a) + Finset.sum t fun x => ↑(μ x)) = 1
⊢ (Finset.sum t fun i =>
      ↑((Pi.single (Exists.choose h)
              { val := ↑(μ a), property := (_ : ↑(μ a) ∈ ⨅ (j : ι) (_ : j ∈ t) (_ : j ≠ Exists.choose h), I j) } +
            fun i => { val := ↑(μ i), property := (_ : ↑(μ i) ∈ ⨅ (j : ι) (_ : j ∈ t) (_ : j ≠ i), I j) })
          i)) =
    1
case a4
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ i), I j }
hμ : (↑(μ a) + Finset.sum t fun x => ↑(μ x)) = 1
b : ι
hb : b ∈ ↑t
ab : a ≠ b
⊢ I a ⊔ I b = ⊤
[PROOFSTEP]
case a3 =>
  rw [← @if_pos _ _ h.choose_spec R (μ a) 0, ← Finset.sum_pi_single', ← Finset.sum_add_distrib] at hμ
  convert hμ
  rename_i i _
  rw [Pi.add_apply, Submodule.coe_add, Submodule.coe_mk]
  by_cases hi : i = h.choose
  · rw [hi, Pi.single_eq_same, Pi.single_eq_same, Submodule.coe_mk]
  · rw [Pi.single_eq_of_ne hi, Pi.single_eq_of_ne hi, Submodule.coe_zero]
[GOAL]
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ i), I j }
hμ : (↑(μ a) + Finset.sum t fun x => ↑(μ x)) = 1
⊢ (Finset.sum t fun i =>
      ↑((Pi.single (Exists.choose h)
              { val := ↑(μ a), property := (_ : ↑(μ a) ∈ ⨅ (j : ι) (_ : j ∈ t) (_ : j ≠ Exists.choose h), I j) } +
            fun i => { val := ↑(μ i), property := (_ : ↑(μ i) ∈ ⨅ (j : ι) (_ : j ∈ t) (_ : j ≠ i), I j) })
          i)) =
    1
[PROOFSTEP]
case a3 =>
  rw [← @if_pos _ _ h.choose_spec R (μ a) 0, ← Finset.sum_pi_single', ← Finset.sum_add_distrib] at hμ
  convert hμ
  rename_i i _
  rw [Pi.add_apply, Submodule.coe_add, Submodule.coe_mk]
  by_cases hi : i = h.choose
  · rw [hi, Pi.single_eq_same, Pi.single_eq_same, Submodule.coe_mk]
  · rw [Pi.single_eq_of_ne hi, Pi.single_eq_of_ne hi, Submodule.coe_zero]
[GOAL]
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ i), I j }
hμ : (↑(μ a) + Finset.sum t fun x => ↑(μ x)) = 1
⊢ (Finset.sum t fun i =>
      ↑((Pi.single (Exists.choose h)
              { val := ↑(μ a), property := (_ : ↑(μ a) ∈ ⨅ (j : ι) (_ : j ∈ t) (_ : j ≠ Exists.choose h), I j) } +
            fun i => { val := ↑(μ i), property := (_ : ↑(μ i) ∈ ⨅ (j : ι) (_ : j ∈ t) (_ : j ≠ i), I j) })
          i)) =
    1
[PROOFSTEP]
rw [← @if_pos _ _ h.choose_spec R (μ a) 0, ← Finset.sum_pi_single', ← Finset.sum_add_distrib] at hμ
[GOAL]
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ i), I j }
hμ✝ : (↑(μ a) + Finset.sum t fun x => ↑(μ x)) = 1
hμ : (Finset.sum t fun x => Pi.single (Exists.choose h) (↑(μ a)) x + ↑(μ x)) = 1
⊢ (Finset.sum t fun i =>
      ↑((Pi.single (Exists.choose h)
              { val := ↑(μ a), property := (_ : ↑(μ a) ∈ ⨅ (j : ι) (_ : j ∈ t) (_ : j ≠ Exists.choose h), I j) } +
            fun i => { val := ↑(μ i), property := (_ : ↑(μ i) ∈ ⨅ (j : ι) (_ : j ∈ t) (_ : j ≠ i), I j) })
          i)) =
    1
[PROOFSTEP]
convert hμ
[GOAL]
case h.e'_2.a
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ i), I j }
hμ✝ : (↑(μ a) + Finset.sum t fun x => ↑(μ x)) = 1
hμ : (Finset.sum t fun x => Pi.single (Exists.choose h) (↑(μ a)) x + ↑(μ x)) = 1
x✝ : ι
a✝ : x✝ ∈ t
⊢ ↑((Pi.single (Exists.choose h)
            { val := ↑(μ a), property := (_ : ↑(μ a) ∈ ⨅ (j : ι) (_ : j ∈ t) (_ : j ≠ Exists.choose h), I j) } +
          fun i => { val := ↑(μ i), property := (_ : ↑(μ i) ∈ ⨅ (j : ι) (_ : j ∈ t) (_ : j ≠ i), I j) })
        x✝) =
    Pi.single (Exists.choose h) (↑(μ a)) x✝ + ↑(μ x✝)
[PROOFSTEP]
rename_i i _
[GOAL]
case h.e'_2.a
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ i), I j }
hμ✝ : (↑(μ a) + Finset.sum t fun x => ↑(μ x)) = 1
hμ : (Finset.sum t fun x => Pi.single (Exists.choose h) (↑(μ a)) x + ↑(μ x)) = 1
i : ι
a✝ : i ∈ t
⊢ ↑((Pi.single (Exists.choose h)
            { val := ↑(μ a), property := (_ : ↑(μ a) ∈ ⨅ (j : ι) (_ : j ∈ t) (_ : j ≠ Exists.choose h), I j) } +
          fun i => { val := ↑(μ i), property := (_ : ↑(μ i) ∈ ⨅ (j : ι) (_ : j ∈ t) (_ : j ≠ i), I j) })
        i) =
    Pi.single (Exists.choose h) (↑(μ a)) i + ↑(μ i)
[PROOFSTEP]
rw [Pi.add_apply, Submodule.coe_add, Submodule.coe_mk]
[GOAL]
case h.e'_2.a
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ i), I j }
hμ✝ : (↑(μ a) + Finset.sum t fun x => ↑(μ x)) = 1
hμ : (Finset.sum t fun x => Pi.single (Exists.choose h) (↑(μ a)) x + ↑(μ x)) = 1
i : ι
a✝ : i ∈ t
⊢ ↑(Pi.single (Exists.choose h)
          { val := ↑(μ a), property := (_ : ↑(μ a) ∈ ⨅ (j : ι) (_ : j ∈ t) (_ : j ≠ Exists.choose h), I j) } i) +
      ↑{ val := ↑(μ i), property := (_ : ↑(μ i) ∈ ⨅ (j : ι) (_ : j ∈ t) (_ : j ≠ i), I j) } =
    Pi.single (Exists.choose h) (↑(μ a)) i + ↑(μ i)
[PROOFSTEP]
by_cases hi : i = h.choose
[GOAL]
case pos
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ i), I j }
hμ✝ : (↑(μ a) + Finset.sum t fun x => ↑(μ x)) = 1
hμ : (Finset.sum t fun x => Pi.single (Exists.choose h) (↑(μ a)) x + ↑(μ x)) = 1
i : ι
a✝ : i ∈ t
hi : i = Exists.choose h
⊢ ↑(Pi.single (Exists.choose h)
          { val := ↑(μ a), property := (_ : ↑(μ a) ∈ ⨅ (j : ι) (_ : j ∈ t) (_ : j ≠ Exists.choose h), I j) } i) +
      ↑{ val := ↑(μ i), property := (_ : ↑(μ i) ∈ ⨅ (j : ι) (_ : j ∈ t) (_ : j ≠ i), I j) } =
    Pi.single (Exists.choose h) (↑(μ a)) i + ↑(μ i)
[PROOFSTEP]
rw [hi, Pi.single_eq_same, Pi.single_eq_same, Submodule.coe_mk]
[GOAL]
case neg
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ i), I j }
hμ✝ : (↑(μ a) + Finset.sum t fun x => ↑(μ x)) = 1
hμ : (Finset.sum t fun x => Pi.single (Exists.choose h) (↑(μ a)) x + ↑(μ x)) = 1
i : ι
a✝ : i ∈ t
hi : ¬i = Exists.choose h
⊢ ↑(Pi.single (Exists.choose h)
          { val := ↑(μ a), property := (_ : ↑(μ a) ∈ ⨅ (j : ι) (_ : j ∈ t) (_ : j ≠ Exists.choose h), I j) } i) +
      ↑{ val := ↑(μ i), property := (_ : ↑(μ i) ∈ ⨅ (j : ι) (_ : j ∈ t) (_ : j ≠ i), I j) } =
    Pi.single (Exists.choose h) (↑(μ a)) i + ↑(μ i)
[PROOFSTEP]
rw [Pi.single_eq_of_ne hi, Pi.single_eq_of_ne hi, Submodule.coe_zero]
[GOAL]
case a4
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ i), I j }
hμ : (↑(μ a) + Finset.sum t fun x => ↑(μ x)) = 1
b : ι
hb : b ∈ ↑t
ab : a ≠ b
⊢ I a ⊔ I b = ⊤
[PROOFSTEP]
case a4 =>
  rw [eq_top_iff_one, Submodule.mem_sup]
  rw [add_comm] at hμ
  refine' ⟨_, _, _, _, hμ⟩
  · refine' sum_mem _ fun x hx => _
    have := Submodule.coe_mem (μ x)
    simp only [mem_iInf] at this
    apply this _ (Finset.mem_cons_self _ _)
    rintro rfl
    exact hat hx
  · have := Submodule.coe_mem (μ a)
    simp only [mem_iInf] at this
    exact this _ (Finset.subset_cons _ hb) ab.symm
[GOAL]
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ i), I j }
hμ : (↑(μ a) + Finset.sum t fun x => ↑(μ x)) = 1
b : ι
hb : b ∈ ↑t
ab : a ≠ b
⊢ I a ⊔ I b = ⊤
[PROOFSTEP]
case a4 =>
  rw [eq_top_iff_one, Submodule.mem_sup]
  rw [add_comm] at hμ
  refine' ⟨_, _, _, _, hμ⟩
  · refine' sum_mem _ fun x hx => _
    have := Submodule.coe_mem (μ x)
    simp only [mem_iInf] at this
    apply this _ (Finset.mem_cons_self _ _)
    rintro rfl
    exact hat hx
  · have := Submodule.coe_mem (μ a)
    simp only [mem_iInf] at this
    exact this _ (Finset.subset_cons _ hb) ab.symm
[GOAL]
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ i), I j }
hμ : (↑(μ a) + Finset.sum t fun x => ↑(μ x)) = 1
b : ι
hb : b ∈ ↑t
ab : a ≠ b
⊢ I a ⊔ I b = ⊤
[PROOFSTEP]
rw [eq_top_iff_one, Submodule.mem_sup]
[GOAL]
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ i), I j }
hμ : (↑(μ a) + Finset.sum t fun x => ↑(μ x)) = 1
b : ι
hb : b ∈ ↑t
ab : a ≠ b
⊢ ∃ y, y ∈ I a ∧ ∃ z, z ∈ I b ∧ y + z = 1
[PROOFSTEP]
rw [add_comm] at hμ
[GOAL]
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ i), I j }
hμ : (Finset.sum t fun x => ↑(μ x)) + ↑(μ a) = 1
b : ι
hb : b ∈ ↑t
ab : a ≠ b
⊢ ∃ y, y ∈ I a ∧ ∃ z, z ∈ I b ∧ y + z = 1
[PROOFSTEP]
refine' ⟨_, _, _, _, hμ⟩
[GOAL]
case refine'_1
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ i), I j }
hμ : (Finset.sum t fun x => ↑(μ x)) + ↑(μ a) = 1
b : ι
hb : b ∈ ↑t
ab : a ≠ b
⊢ (Finset.sum t fun x => ↑(μ x)) ∈ I a
[PROOFSTEP]
refine' sum_mem _ fun x hx => _
[GOAL]
case refine'_1
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ i), I j }
hμ : (Finset.sum t fun x => ↑(μ x)) + ↑(μ a) = 1
b : ι
hb : b ∈ ↑t
ab : a ≠ b
x : ι
hx : x ∈ t
⊢ ↑(μ x) ∈ I a
[PROOFSTEP]
have := Submodule.coe_mem (μ x)
[GOAL]
case refine'_1
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝ : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ i), I j }
hμ : (Finset.sum t fun x => ↑(μ x)) + ↑(μ a) = 1
b : ι
hb : b ∈ ↑t
ab : a ≠ b
x : ι
hx : x ∈ t
this : ↑(μ x) ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ x), I j
⊢ ↑(μ x) ∈ I a
[PROOFSTEP]
simp only [mem_iInf] at this
[GOAL]
case refine'_1
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝ : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ i), I j }
hμ : (Finset.sum t fun x => ↑(μ x)) + ↑(μ a) = 1
b : ι
hb : b ∈ ↑t
ab : a ≠ b
x : ι
hx : x ∈ t
this : ∀ (i : ι), i ∈ Finset.cons a t hat → i ≠ x → ↑(μ x) ∈ I i
⊢ ↑(μ x) ∈ I a
[PROOFSTEP]
apply this _ (Finset.mem_cons_self _ _)
[GOAL]
case refine'_1
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝ : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ i), I j }
hμ : (Finset.sum t fun x => ↑(μ x)) + ↑(μ a) = 1
b : ι
hb : b ∈ ↑t
ab : a ≠ b
x : ι
hx : x ∈ t
this : ∀ (i : ι), i ∈ Finset.cons a t hat → i ≠ x → ↑(μ x) ∈ I i
⊢ a ≠ x
[PROOFSTEP]
rintro rfl
[GOAL]
case refine'_1
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝ : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ i), I j }
hμ : (Finset.sum t fun x => ↑(μ x)) + ↑(μ a) = 1
b : ι
hb : b ∈ ↑t
ab : a ≠ b
hx : a ∈ t
this : ∀ (i : ι), i ∈ Finset.cons a t hat → i ≠ a → ↑(μ a) ∈ I i
⊢ False
[PROOFSTEP]
exact hat hx
[GOAL]
case refine'_2
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ i), I j }
hμ : (Finset.sum t fun x => ↑(μ x)) + ↑(μ a) = 1
b : ι
hb : b ∈ ↑t
ab : a ≠ b
⊢ ↑(μ a) ∈ I b
[PROOFSTEP]
have := Submodule.coe_mem (μ a)
[GOAL]
case refine'_2
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝ : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ i), I j }
hμ : (Finset.sum t fun x => ↑(μ x)) + ↑(μ a) = 1
b : ι
hb : b ∈ ↑t
ab : a ≠ b
this : ↑(μ a) ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ a), I j
⊢ ↑(μ a) ∈ I b
[PROOFSTEP]
simp only [mem_iInf] at this
[GOAL]
case refine'_2
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝ : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ i), I j }
hμ : (Finset.sum t fun x => ↑(μ x)) + ↑(μ a) = 1
b : ι
hb : b ∈ ↑t
ab : a ≠ b
this : ∀ (i : ι), i ∈ Finset.cons a t hat → i ≠ a → ↑(μ a) ∈ I i
⊢ ↑(μ a) ∈ I b
[PROOFSTEP]
exact this _ (Finset.subset_cons _ hb) ab.symm
[GOAL]
case refine'_2.mpr
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
⊢ ((Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤) ∧ ∀ (b : ι), b ∈ ↑t → a ≠ b → I a ⊔ I b = ⊤) →
    ∃ μ, (Finset.sum (Finset.cons a t hat) fun i => ↑(μ i)) = 1
[PROOFSTEP]
rintro ⟨hs, Hb⟩
[GOAL]
case refine'_2.mpr.intro
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
hs : Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
Hb : ∀ (b : ι), b ∈ ↑t → a ≠ b → I a ⊔ I b = ⊤
⊢ ∃ μ, (Finset.sum (Finset.cons a t hat) fun i => ↑(μ i)) = 1
[PROOFSTEP]
obtain ⟨μ, hμ⟩ := ih.mpr hs
[GOAL]
case refine'_2.mpr.intro.intro
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
hs : Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
Hb : ∀ (b : ι), b ∈ ↑t → a ≠ b → I a ⊔ I b = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ t) (_ : j ≠ i), I j }
hμ : (Finset.sum t fun i => ↑(μ i)) = 1
⊢ ∃ μ, (Finset.sum (Finset.cons a t hat) fun i => ↑(μ i)) = 1
[PROOFSTEP]
have := sup_iInf_eq_top fun b hb => Hb b hb (ne_of_mem_of_not_mem hb hat).symm
[GOAL]
case refine'_2.mpr.intro.intro
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝ : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
hs : Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
Hb : ∀ (b : ι), b ∈ ↑t → a ≠ b → I a ⊔ I b = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ t) (_ : j ≠ i), I j }
hμ : (Finset.sum t fun i => ↑(μ i)) = 1
this : I a ⊔ ⨅ (i : ι) (_ : i ∈ t), I i = ⊤
⊢ ∃ μ, (Finset.sum (Finset.cons a t hat) fun i => ↑(μ i)) = 1
[PROOFSTEP]
rw [eq_top_iff_one, Submodule.mem_sup] at this
[GOAL]
case refine'_2.mpr.intro.intro
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝ : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
hs : Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
Hb : ∀ (b : ι), b ∈ ↑t → a ≠ b → I a ⊔ I b = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ t) (_ : j ≠ i), I j }
hμ : (Finset.sum t fun i => ↑(μ i)) = 1
this : ∃ y, y ∈ I a ∧ ∃ z, z ∈ ⨅ (i : ι) (_ : i ∈ t), I i ∧ y + z = 1
⊢ ∃ μ, (Finset.sum (Finset.cons a t hat) fun i => ↑(μ i)) = 1
[PROOFSTEP]
obtain ⟨u, hu, v, hv, huv⟩ := this
[GOAL]
case refine'_2.mpr.intro.intro.intro.intro.intro.intro
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
hs : Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
Hb : ∀ (b : ι), b ∈ ↑t → a ≠ b → I a ⊔ I b = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ t) (_ : j ≠ i), I j }
hμ : (Finset.sum t fun i => ↑(μ i)) = 1
u : R
hu : u ∈ I a
v : R
hv : v ∈ ⨅ (i : ι) (_ : i ∈ t), I i
huv : u + v = 1
⊢ ∃ μ, (Finset.sum (Finset.cons a t hat) fun i => ↑(μ i)) = 1
[PROOFSTEP]
refine' ⟨fun i => if hi : i = a then ⟨v, _⟩ else ⟨u * μ i, _⟩, _⟩
[GOAL]
case refine'_2.mpr.intro.intro.intro.intro.intro.intro.refine'_1
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
hs : Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
Hb : ∀ (b : ι), b ∈ ↑t → a ≠ b → I a ⊔ I b = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ t) (_ : j ≠ i), I j }
hμ : (Finset.sum t fun i => ↑(μ i)) = 1
u : R
hu : u ∈ I a
v : R
hv : v ∈ ⨅ (i : ι) (_ : i ∈ t), I i
huv : u + v = 1
i : ι
hi : i = a
⊢ v ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ i), I j
[PROOFSTEP]
simp only [mem_iInf] at hv ⊢
[GOAL]
case refine'_2.mpr.intro.intro.intro.intro.intro.intro.refine'_1
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
hs : Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
Hb : ∀ (b : ι), b ∈ ↑t → a ≠ b → I a ⊔ I b = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ t) (_ : j ≠ i), I j }
hμ : (Finset.sum t fun i => ↑(μ i)) = 1
u : R
hu : u ∈ I a
v : R
huv : u + v = 1
i : ι
hi : i = a
hv : ∀ (i : ι), i ∈ t → v ∈ I i
⊢ ∀ (i_1 : ι), i_1 ∈ Finset.cons a t hat → i_1 ≠ i → v ∈ I i_1
[PROOFSTEP]
intro j hj ij
[GOAL]
case refine'_2.mpr.intro.intro.intro.intro.intro.intro.refine'_1
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
hs : Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
Hb : ∀ (b : ι), b ∈ ↑t → a ≠ b → I a ⊔ I b = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ t) (_ : j ≠ i), I j }
hμ : (Finset.sum t fun i => ↑(μ i)) = 1
u : R
hu : u ∈ I a
v : R
huv : u + v = 1
i : ι
hi : i = a
hv : ∀ (i : ι), i ∈ t → v ∈ I i
j : ι
hj : j ∈ Finset.cons a t hat
ij : j ≠ i
⊢ v ∈ I j
[PROOFSTEP]
rw [Finset.mem_cons, ← hi] at hj
[GOAL]
case refine'_2.mpr.intro.intro.intro.intro.intro.intro.refine'_1
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
hs : Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
Hb : ∀ (b : ι), b ∈ ↑t → a ≠ b → I a ⊔ I b = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ t) (_ : j ≠ i), I j }
hμ : (Finset.sum t fun i => ↑(μ i)) = 1
u : R
hu : u ∈ I a
v : R
huv : u + v = 1
i : ι
hi : i = a
hv : ∀ (i : ι), i ∈ t → v ∈ I i
j : ι
hj : j = i ∨ j ∈ t
ij : j ≠ i
⊢ v ∈ I j
[PROOFSTEP]
exact hv _ (hj.resolve_left ij)
[GOAL]
case refine'_2.mpr.intro.intro.intro.intro.intro.intro.refine'_2
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
hs : Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
Hb : ∀ (b : ι), b ∈ ↑t → a ≠ b → I a ⊔ I b = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ t) (_ : j ≠ i), I j }
hμ : (Finset.sum t fun i => ↑(μ i)) = 1
u : R
hu : u ∈ I a
v : R
hv : v ∈ ⨅ (i : ι) (_ : i ∈ t), I i
huv : u + v = 1
i : ι
hi : ¬i = a
⊢ u * ↑(μ i) ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ i), I j
[PROOFSTEP]
have := Submodule.coe_mem (μ i)
[GOAL]
case refine'_2.mpr.intro.intro.intro.intro.intro.intro.refine'_2
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝ : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
hs : Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
Hb : ∀ (b : ι), b ∈ ↑t → a ≠ b → I a ⊔ I b = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ t) (_ : j ≠ i), I j }
hμ : (Finset.sum t fun i => ↑(μ i)) = 1
u : R
hu : u ∈ I a
v : R
hv : v ∈ ⨅ (i : ι) (_ : i ∈ t), I i
huv : u + v = 1
i : ι
hi : ¬i = a
this : ↑(μ i) ∈ ⨅ (j : ι) (_ : j ∈ t) (_ : j ≠ i), I j
⊢ u * ↑(μ i) ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ i), I j
[PROOFSTEP]
simp only [mem_iInf] at this ⊢
[GOAL]
case refine'_2.mpr.intro.intro.intro.intro.intro.intro.refine'_2
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝ : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
hs : Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
Hb : ∀ (b : ι), b ∈ ↑t → a ≠ b → I a ⊔ I b = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ t) (_ : j ≠ i), I j }
hμ : (Finset.sum t fun i => ↑(μ i)) = 1
u : R
hu : u ∈ I a
v : R
hv : v ∈ ⨅ (i : ι) (_ : i ∈ t), I i
huv : u + v = 1
i : ι
hi : ¬i = a
this : ∀ (i_1 : ι), i_1 ∈ t → i_1 ≠ i → ↑(μ i) ∈ I i_1
⊢ ∀ (i_1 : ι), i_1 ∈ Finset.cons a t hat → i_1 ≠ i → u * ↑(μ i) ∈ I i_1
[PROOFSTEP]
intro j hj ij
[GOAL]
case refine'_2.mpr.intro.intro.intro.intro.intro.intro.refine'_2
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝ : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
hs : Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
Hb : ∀ (b : ι), b ∈ ↑t → a ≠ b → I a ⊔ I b = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ t) (_ : j ≠ i), I j }
hμ : (Finset.sum t fun i => ↑(μ i)) = 1
u : R
hu : u ∈ I a
v : R
hv : v ∈ ⨅ (i : ι) (_ : i ∈ t), I i
huv : u + v = 1
i : ι
hi : ¬i = a
this : ∀ (i_1 : ι), i_1 ∈ t → i_1 ≠ i → ↑(μ i) ∈ I i_1
j : ι
hj : j ∈ Finset.cons a t hat
ij : j ≠ i
⊢ u * ↑(μ i) ∈ I j
[PROOFSTEP]
rcases Finset.mem_cons.mp hj with (rfl | hj)
[GOAL]
case refine'_2.mpr.intro.intro.intro.intro.intro.intro.refine'_2.inl
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝ : DecidableEq ι
t : Finset ι
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
hs : Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ t) (_ : j ≠ i), I j }
hμ : (Finset.sum t fun i => ↑(μ i)) = 1
u v : R
hv : v ∈ ⨅ (i : ι) (_ : i ∈ t), I i
huv : u + v = 1
i : ι
this : ∀ (i_1 : ι), i_1 ∈ t → i_1 ≠ i → ↑(μ i) ∈ I i_1
j : ι
ij : j ≠ i
hat : ¬j ∈ t
Hb : ∀ (b : ι), b ∈ ↑t → j ≠ b → I j ⊔ I b = ⊤
hu : u ∈ I j
hi : ¬i = j
hj : j ∈ Finset.cons j t hat
⊢ u * ↑(μ i) ∈ I j
[PROOFSTEP]
exact mul_mem_right _ _ hu
[GOAL]
case refine'_2.mpr.intro.intro.intro.intro.intro.intro.refine'_2.inr
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝ : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
hs : Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
Hb : ∀ (b : ι), b ∈ ↑t → a ≠ b → I a ⊔ I b = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ t) (_ : j ≠ i), I j }
hμ : (Finset.sum t fun i => ↑(μ i)) = 1
u : R
hu : u ∈ I a
v : R
hv : v ∈ ⨅ (i : ι) (_ : i ∈ t), I i
huv : u + v = 1
i : ι
hi : ¬i = a
this : ∀ (i_1 : ι), i_1 ∈ t → i_1 ≠ i → ↑(μ i) ∈ I i_1
j : ι
hj✝ : j ∈ Finset.cons a t hat
ij : j ≠ i
hj : j ∈ t
⊢ u * ↑(μ i) ∈ I j
[PROOFSTEP]
exact mul_mem_left _ _ (this _ hj ij)
[GOAL]
case refine'_2.mpr.intro.intro.intro.intro.intro.intro.refine'_3
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
hs : Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
Hb : ∀ (b : ι), b ∈ ↑t → a ≠ b → I a ⊔ I b = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ t) (_ : j ≠ i), I j }
hμ : (Finset.sum t fun i => ↑(μ i)) = 1
u : R
hu : u ∈ I a
v : R
hv : v ∈ ⨅ (i : ι) (_ : i ∈ t), I i
huv : u + v = 1
⊢ (Finset.sum (Finset.cons a t hat) fun i =>
      ↑((fun i =>
            if hi : i = a then
              { val := v, property := (_ : v ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ i), I j) }
            else
              { val := u * ↑(μ i),
                property := (_ : u * ↑(μ i) ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ i), I j) })
          i)) =
    1
[PROOFSTEP]
dsimp only
[GOAL]
case refine'_2.mpr.intro.intro.intro.intro.intro.intro.refine'_3
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
hs : Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
Hb : ∀ (b : ι), b ∈ ↑t → a ≠ b → I a ⊔ I b = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ t) (_ : j ≠ i), I j }
hμ : (Finset.sum t fun i => ↑(μ i)) = 1
u : R
hu : u ∈ I a
v : R
hv : v ∈ ⨅ (i : ι) (_ : i ∈ t), I i
huv : u + v = 1
⊢ (Finset.sum (Finset.cons a t hat) fun i =>
      ↑(if hi : i = a then { val := v, property := (_ : v ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ i), I j) }
        else
          { val := u * ↑(μ i),
            property := (_ : u * ↑(μ i) ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ i), I j) })) =
    1
[PROOFSTEP]
rw [Finset.sum_cons, dif_pos rfl, add_comm]
[GOAL]
case refine'_2.mpr.intro.intro.intro.intro.intro.intro.refine'_3
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
hs : Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
Hb : ∀ (b : ι), b ∈ ↑t → a ≠ b → I a ⊔ I b = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ t) (_ : j ≠ i), I j }
hμ : (Finset.sum t fun i => ↑(μ i)) = 1
u : R
hu : u ∈ I a
v : R
hv : v ∈ ⨅ (i : ι) (_ : i ∈ t), I i
huv : u + v = 1
⊢ (Finset.sum t fun x =>
        ↑(if hi : x = a then
            { val := v, property := (_ : v ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ x), I j) }
          else
            { val := u * ↑(μ x),
              property := (_ : u * ↑(μ x) ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ x), I j) })) +
      ↑{ val := v, property := (_ : v ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ a), I j) } =
    1
[PROOFSTEP]
rw [← mul_one u] at huv
[GOAL]
case refine'_2.mpr.intro.intro.intro.intro.intro.intro.refine'_3
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
hs : Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
Hb : ∀ (b : ι), b ∈ ↑t → a ≠ b → I a ⊔ I b = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ t) (_ : j ≠ i), I j }
hμ : (Finset.sum t fun i => ↑(μ i)) = 1
u : R
hu : u ∈ I a
v : R
hv : v ∈ ⨅ (i : ι) (_ : i ∈ t), I i
huv : u * 1 + v = 1
⊢ (Finset.sum t fun x =>
        ↑(if hi : x = a then
            { val := v, property := (_ : v ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ x), I j) }
          else
            { val := u * ↑(μ x),
              property := (_ : u * ↑(μ x) ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ x), I j) })) +
      ↑{ val := v, property := (_ : v ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ a), I j) } =
    1
[PROOFSTEP]
rw [← huv, ← hμ, Finset.mul_sum]
[GOAL]
case refine'_2.mpr.intro.intro.intro.intro.intro.intro.refine'_3
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
hs : Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
Hb : ∀ (b : ι), b ∈ ↑t → a ≠ b → I a ⊔ I b = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ t) (_ : j ≠ i), I j }
hμ : (Finset.sum t fun i => ↑(μ i)) = 1
u : R
hu : u ∈ I a
v : R
hv : v ∈ ⨅ (i : ι) (_ : i ∈ t), I i
huv : u * 1 + v = 1
⊢ (Finset.sum t fun x =>
        ↑(if hi : x = a then
            { val := v, property := (_ : v ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ x), I j) }
          else
            { val := u * ↑(μ x),
              property := (_ : u * ↑(μ x) ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ x), I j) })) +
      ↑{ val := v, property := (_ : v ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ a), I j) } =
    (Finset.sum t fun x => u * ↑(μ x)) + v
[PROOFSTEP]
congr 1
[GOAL]
case refine'_2.mpr.intro.intro.intro.intro.intro.intro.refine'_3.e_a
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
hs : Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
Hb : ∀ (b : ι), b ∈ ↑t → a ≠ b → I a ⊔ I b = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ t) (_ : j ≠ i), I j }
hμ : (Finset.sum t fun i => ↑(μ i)) = 1
u : R
hu : u ∈ I a
v : R
hv : v ∈ ⨅ (i : ι) (_ : i ∈ t), I i
huv : u * 1 + v = 1
⊢ (Finset.sum t fun x =>
      ↑(if hi : x = a then { val := v, property := (_ : v ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ x), I j) }
        else
          { val := u * ↑(μ x),
            property := (_ : u * ↑(μ x) ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ x), I j) })) =
    Finset.sum t fun x => u * ↑(μ x)
[PROOFSTEP]
apply Finset.sum_congr rfl
[GOAL]
case refine'_2.mpr.intro.intro.intro.intro.intro.intro.refine'_3.e_a
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
hs : Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
Hb : ∀ (b : ι), b ∈ ↑t → a ≠ b → I a ⊔ I b = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ t) (_ : j ≠ i), I j }
hμ : (Finset.sum t fun i => ↑(μ i)) = 1
u : R
hu : u ∈ I a
v : R
hv : v ∈ ⨅ (i : ι) (_ : i ∈ t), I i
huv : u * 1 + v = 1
⊢ ∀ (x : ι),
    x ∈ t →
      ↑(if hi : x = a then { val := v, property := (_ : v ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ x), I j) }
          else
            { val := u * ↑(μ x),
              property := (_ : u * ↑(μ x) ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ x), I j) }) =
        u * ↑(μ x)
[PROOFSTEP]
intro j hj
[GOAL]
case refine'_2.mpr.intro.intro.intro.intro.intro.intro.refine'_3.e_a
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
hs : Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
Hb : ∀ (b : ι), b ∈ ↑t → a ≠ b → I a ⊔ I b = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ t) (_ : j ≠ i), I j }
hμ : (Finset.sum t fun i => ↑(μ i)) = 1
u : R
hu : u ∈ I a
v : R
hv : v ∈ ⨅ (i : ι) (_ : i ∈ t), I i
huv : u * 1 + v = 1
j : ι
hj : j ∈ t
⊢ ↑(if hi : j = a then
        { val := v, property := (_ : v ∈ ⨅ (j_1 : ι) (_ : j_1 ∈ Finset.cons a t hat) (_ : j_1 ≠ j), I j_1) }
      else
        { val := u * ↑(μ j),
          property := (_ : u * ↑(μ j) ∈ ⨅ (j_1 : ι) (_ : j_1 ∈ Finset.cons a t hat) (_ : j_1 ≠ j), I j_1) }) =
    u * ↑(μ j)
[PROOFSTEP]
rw [dif_neg]
[GOAL]
case refine'_2.mpr.intro.intro.intro.intro.intro.intro.refine'_3.e_a.hnc
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
hs : Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
Hb : ∀ (b : ι), b ∈ ↑t → a ≠ b → I a ⊔ I b = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ t) (_ : j ≠ i), I j }
hμ : (Finset.sum t fun i => ↑(μ i)) = 1
u : R
hu : u ∈ I a
v : R
hv : v ∈ ⨅ (i : ι) (_ : i ∈ t), I i
huv : u * 1 + v = 1
j : ι
hj : j ∈ t
⊢ ¬j = a
[PROOFSTEP]
rintro rfl
[GOAL]
case refine'_2.mpr.intro.intro.intro.intro.intro.intro.refine'_3.e_a.hnc
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
t : Finset ι
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
hs : Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ t) (_ : j ≠ i), I j }
hμ : (Finset.sum t fun i => ↑(μ i)) = 1
u v : R
hv : v ∈ ⨅ (i : ι) (_ : i ∈ t), I i
huv : u * 1 + v = 1
j : ι
hj : j ∈ t
hat : ¬j ∈ t
Hb : ∀ (b : ι), b ∈ ↑t → j ≠ b → I j ⊔ I b = ⊤
hu : u ∈ I j
⊢ False
[PROOFSTEP]
exact hat hj


[GOAL]
n : ℕ
K : Type u_1
inst✝ : CommRing K
μ : K
h : IsPrimitiveRoot μ n
hpos : 0 < n
⊢ IsIntegral ℤ μ
[PROOFSTEP]
use X ^ n - 1
[GOAL]
case h
n : ℕ
K : Type u_1
inst✝ : CommRing K
μ : K
h : IsPrimitiveRoot μ n
hpos : 0 < n
⊢ Monic (X ^ n - 1) ∧ eval₂ (algebraMap ℤ K) μ (X ^ n - 1) = 0
[PROOFSTEP]
constructor
[GOAL]
case h.left
n : ℕ
K : Type u_1
inst✝ : CommRing K
μ : K
h : IsPrimitiveRoot μ n
hpos : 0 < n
⊢ Monic (X ^ n - 1)
[PROOFSTEP]
exact monic_X_pow_sub_C 1 (ne_of_lt hpos).symm
[GOAL]
case h.right
n : ℕ
K : Type u_1
inst✝ : CommRing K
μ : K
h : IsPrimitiveRoot μ n
hpos : 0 < n
⊢ eval₂ (algebraMap ℤ K) μ (X ^ n - 1) = 0
[PROOFSTEP]
simp only [((IsPrimitiveRoot.iff_def μ n).mp h).left, eval₂_one, eval₂_X_pow, eval₂_sub, sub_self]
[GOAL]
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
⊢ minpoly ℤ μ ∣ X ^ n - 1
[PROOFSTEP]
rcases n.eq_zero_or_pos with (rfl | h0)
[GOAL]
case inl
K : Type u_1
inst✝² : CommRing K
μ : K
inst✝¹ : IsDomain K
inst✝ : CharZero K
h : IsPrimitiveRoot μ 0
⊢ minpoly ℤ μ ∣ X ^ 0 - 1
[PROOFSTEP]
simp
[GOAL]
case inr
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
h0 : n > 0
⊢ minpoly ℤ μ ∣ X ^ n - 1
[PROOFSTEP]
apply minpoly.isIntegrallyClosed_dvd (isIntegral h h0)
[GOAL]
case inr
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
h0 : n > 0
⊢ ↑(Polynomial.aeval μ) (X ^ n - 1) = 0
[PROOFSTEP]
simp only [((IsPrimitiveRoot.iff_def μ n).mp h).left, aeval_X_pow, eq_intCast, Int.cast_one, aeval_one, AlgHom.map_sub,
  sub_self]
[GOAL]
n : ℕ
K : Type u_1
inst✝³ : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝² : IsDomain K
inst✝¹ : CharZero K
p : ℕ
inst✝ : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
⊢ Separable (map (Int.castRingHom (ZMod p)) (minpoly ℤ μ))
[PROOFSTEP]
have hdvd : map (Int.castRingHom (ZMod p)) (minpoly ℤ μ) ∣ X ^ n - 1 :=
  by
  convert RingHom.map_dvd (mapRingHom (Int.castRingHom (ZMod p))) (minpoly_dvd_x_pow_sub_one h)
  simp only [map_sub, map_pow, coe_mapRingHom, map_X, map_one]
[GOAL]
n : ℕ
K : Type u_1
inst✝³ : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝² : IsDomain K
inst✝¹ : CharZero K
p : ℕ
inst✝ : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
⊢ map (Int.castRingHom (ZMod p)) (minpoly ℤ μ) ∣ X ^ n - 1
[PROOFSTEP]
convert RingHom.map_dvd (mapRingHom (Int.castRingHom (ZMod p))) (minpoly_dvd_x_pow_sub_one h)
[GOAL]
case h.e'_4
n : ℕ
K : Type u_1
inst✝³ : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝² : IsDomain K
inst✝¹ : CharZero K
p : ℕ
inst✝ : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
⊢ X ^ n - 1 = ↑(mapRingHom (Int.castRingHom (ZMod p))) (X ^ n - 1)
[PROOFSTEP]
simp only [map_sub, map_pow, coe_mapRingHom, map_X, map_one]
[GOAL]
n : ℕ
K : Type u_1
inst✝³ : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝² : IsDomain K
inst✝¹ : CharZero K
p : ℕ
inst✝ : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hdvd : map (Int.castRingHom (ZMod p)) (minpoly ℤ μ) ∣ X ^ n - 1
⊢ Separable (map (Int.castRingHom (ZMod p)) (minpoly ℤ μ))
[PROOFSTEP]
refine' Separable.of_dvd (separable_X_pow_sub_C 1 _ one_ne_zero) hdvd
[GOAL]
n : ℕ
K : Type u_1
inst✝³ : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝² : IsDomain K
inst✝¹ : CharZero K
p : ℕ
inst✝ : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hdvd : map (Int.castRingHom (ZMod p)) (minpoly ℤ μ) ∣ X ^ n - 1
⊢ ↑n ≠ 0
[PROOFSTEP]
by_contra hzero
[GOAL]
n : ℕ
K : Type u_1
inst✝³ : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝² : IsDomain K
inst✝¹ : CharZero K
p : ℕ
inst✝ : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hdvd : map (Int.castRingHom (ZMod p)) (minpoly ℤ μ) ∣ X ^ n - 1
hzero : ↑n = 0
⊢ False
[PROOFSTEP]
exact hdiv ((ZMod.nat_cast_zmod_eq_zero_iff_dvd n p).1 hzero)
[GOAL]
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hdiv : ¬p ∣ n
⊢ minpoly ℤ μ ∣ ↑(expand ℤ p) (minpoly ℤ (μ ^ p))
[PROOFSTEP]
rcases n.eq_zero_or_pos with (rfl | hpos)
[GOAL]
case inl
K : Type u_1
inst✝² : CommRing K
μ : K
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
h : IsPrimitiveRoot μ 0
hdiv : ¬p ∣ 0
⊢ minpoly ℤ μ ∣ ↑(expand ℤ p) (minpoly ℤ (μ ^ p))
[PROOFSTEP]
simp_all
[GOAL]
case inr
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hdiv : ¬p ∣ n
hpos : n > 0
⊢ minpoly ℤ μ ∣ ↑(expand ℤ p) (minpoly ℤ (μ ^ p))
[PROOFSTEP]
letI : IsIntegrallyClosed ℤ := GCDMonoid.toIsIntegrallyClosed
[GOAL]
case inr
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hdiv : ¬p ∣ n
hpos : n > 0
this : IsIntegrallyClosed ℤ := GCDMonoid.toIsIntegrallyClosed
⊢ minpoly ℤ μ ∣ ↑(expand ℤ p) (minpoly ℤ (μ ^ p))
[PROOFSTEP]
refine' minpoly.isIntegrallyClosed_dvd (h.isIntegral hpos) _
[GOAL]
case inr
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hdiv : ¬p ∣ n
hpos : n > 0
this : IsIntegrallyClosed ℤ := GCDMonoid.toIsIntegrallyClosed
⊢ ↑(Polynomial.aeval μ) (↑(expand ℤ p) (minpoly ℤ (μ ^ p))) = 0
[PROOFSTEP]
rw [aeval_def, coe_expand, ← comp, eval₂_eq_eval_map, map_comp, Polynomial.map_pow, map_X, eval_comp, eval_pow, eval_X,
  ← eval₂_eq_eval_map, ← aeval_def]
[GOAL]
case inr
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hdiv : ¬p ∣ n
hpos : n > 0
this : IsIntegrallyClosed ℤ := GCDMonoid.toIsIntegrallyClosed
⊢ ↑(Polynomial.aeval (μ ^ p)) (minpoly ℤ (μ ^ p)) = 0
[PROOFSTEP]
exact minpoly.aeval _ _
[GOAL]
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
⊢ map (Int.castRingHom (ZMod p)) (minpoly ℤ μ) ∣ map (Int.castRingHom (ZMod p)) (minpoly ℤ (μ ^ p)) ^ p
[PROOFSTEP]
set Q := minpoly ℤ (μ ^ p)
[GOAL]
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
Q : ℤ[X] := minpoly ℤ (μ ^ p)
⊢ map (Int.castRingHom (ZMod p)) (minpoly ℤ μ) ∣ map (Int.castRingHom (ZMod p)) Q ^ p
[PROOFSTEP]
have hfrob : map (Int.castRingHom (ZMod p)) Q ^ p = map (Int.castRingHom (ZMod p)) (expand ℤ p Q) := by
  rw [← ZMod.expand_card, map_expand]
[GOAL]
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
Q : ℤ[X] := minpoly ℤ (μ ^ p)
⊢ map (Int.castRingHom (ZMod p)) Q ^ p = map (Int.castRingHom (ZMod p)) (↑(expand ℤ p) Q)
[PROOFSTEP]
rw [← ZMod.expand_card, map_expand]
[GOAL]
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hfrob : map (Int.castRingHom (ZMod p)) Q ^ p = map (Int.castRingHom (ZMod p)) (↑(expand ℤ p) Q)
⊢ map (Int.castRingHom (ZMod p)) (minpoly ℤ μ) ∣ map (Int.castRingHom (ZMod p)) Q ^ p
[PROOFSTEP]
rw [hfrob]
[GOAL]
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hfrob : map (Int.castRingHom (ZMod p)) Q ^ p = map (Int.castRingHom (ZMod p)) (↑(expand ℤ p) Q)
⊢ map (Int.castRingHom (ZMod p)) (minpoly ℤ μ) ∣ map (Int.castRingHom (ZMod p)) (↑(expand ℤ p) Q)
[PROOFSTEP]
apply RingHom.map_dvd (mapRingHom (Int.castRingHom (ZMod p)))
[GOAL]
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hfrob : map (Int.castRingHom (ZMod p)) Q ^ p = map (Int.castRingHom (ZMod p)) (↑(expand ℤ p) Q)
⊢ minpoly ℤ μ ∣ ↑(expand ℤ p) Q
[PROOFSTEP]
exact minpoly_dvd_expand h hdiv
[GOAL]
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
⊢ minpoly ℤ μ = minpoly ℤ (μ ^ p)
[PROOFSTEP]
classical
by_cases hn : n = 0
· simp_all
have hpos := Nat.pos_of_ne_zero hn
by_contra hdiff
set P := minpoly ℤ μ
set Q := minpoly ℤ (μ ^ p)
have Pmonic : P.Monic := minpoly.monic (h.isIntegral hpos)
have Qmonic : Q.Monic := minpoly.monic ((h.pow_of_prime hprime.1 hdiv).isIntegral hpos)
have Pirr : Irreducible P := minpoly.irreducible (h.isIntegral hpos)
have Qirr : Irreducible Q := minpoly.irreducible ((h.pow_of_prime hprime.1 hdiv).isIntegral hpos)
have PQprim : IsPrimitive (P * Q) := Pmonic.isPrimitive.mul Qmonic.isPrimitive
have prod : P * Q ∣ X ^ n - 1 :=
  by
  rw [IsPrimitive.Int.dvd_iff_map_cast_dvd_map_cast (P * Q) (X ^ n - 1) PQprim
      (monic_X_pow_sub_C (1 : ℤ) (ne_of_gt hpos)).isPrimitive,
    Polynomial.map_mul]
  refine' IsCoprime.mul_dvd _ _ _
  · have aux := IsPrimitive.Int.irreducible_iff_irreducible_map_cast Pmonic.isPrimitive
    refine' (dvd_or_coprime _ _ (aux.1 Pirr)).resolve_left _
    rw [map_dvd_map (Int.castRingHom ℚ) Int.cast_injective Pmonic]
    intro hdiv
    refine' hdiff (eq_of_monic_of_associated Pmonic Qmonic _)
    exact associated_of_dvd_dvd hdiv (Pirr.dvd_symm Qirr hdiv)
  · apply (map_dvd_map (Int.castRingHom ℚ) Int.cast_injective Pmonic).2
    exact minpoly_dvd_x_pow_sub_one h
  · apply (map_dvd_map (Int.castRingHom ℚ) Int.cast_injective Qmonic).2
    exact minpoly_dvd_x_pow_sub_one (pow_of_prime h hprime.1 hdiv)
replace prod := RingHom.map_dvd (mapRingHom (Int.castRingHom (ZMod p))) prod
rw [coe_mapRingHom, Polynomial.map_mul, Polynomial.map_sub, Polynomial.map_one, Polynomial.map_pow, map_X] at prod
obtain ⟨R, hR⟩ := minpoly_dvd_mod_p h hdiv
rw [hR, ← mul_assoc, ← Polynomial.map_mul, ← sq, Polynomial.map_pow] at prod
have habs : map (Int.castRingHom (ZMod p)) P ^ 2 ∣ map (Int.castRingHom (ZMod p)) P ^ 2 * R := by use R
replace habs :=
  lt_of_lt_of_le (PartENat.coe_lt_coe.2 one_lt_two) (multiplicity.le_multiplicity_of_pow_dvd (dvd_trans habs prod))
have hfree : Squarefree (X ^ n - 1 : (ZMod p)[X]) :=
  (separable_X_pow_sub_C 1 (fun h => hdiv <| (ZMod.nat_cast_zmod_eq_zero_iff_dvd n p).1 h) one_ne_zero).squarefree
cases' (multiplicity.squarefree_iff_multiplicity_le_one (X ^ n - 1)).1 hfree (map (Int.castRingHom (ZMod p)) P) with hle
  hunit
· rw [Nat.cast_one] at habs ; exact hle.not_lt habs
· replace hunit := degree_eq_zero_of_isUnit hunit
  rw [degree_map_eq_of_leadingCoeff_ne_zero (Int.castRingHom (ZMod p)) _] at hunit
  · exact (minpoly.degree_pos (isIntegral h hpos)).ne' hunit
  simp only [Pmonic, eq_intCast, Monic.leadingCoeff, Int.cast_one, Ne.def, not_false_iff, one_ne_zero]
[GOAL]
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
⊢ minpoly ℤ μ = minpoly ℤ (μ ^ p)
[PROOFSTEP]
by_cases hn : n = 0
[GOAL]
case pos
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hn : n = 0
⊢ minpoly ℤ μ = minpoly ℤ (μ ^ p)
[PROOFSTEP]
simp_all
[GOAL]
case neg
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hn : ¬n = 0
⊢ minpoly ℤ μ = minpoly ℤ (μ ^ p)
[PROOFSTEP]
have hpos := Nat.pos_of_ne_zero hn
[GOAL]
case neg
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hn : ¬n = 0
hpos : 0 < n
⊢ minpoly ℤ μ = minpoly ℤ (μ ^ p)
[PROOFSTEP]
by_contra hdiff
[GOAL]
case neg
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hn : ¬n = 0
hpos : 0 < n
hdiff : ¬minpoly ℤ μ = minpoly ℤ (μ ^ p)
⊢ False
[PROOFSTEP]
set P := minpoly ℤ μ
[GOAL]
case neg
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hn : ¬n = 0
hpos : 0 < n
P : ℤ[X] := minpoly ℤ μ
hdiff : ¬P = minpoly ℤ (μ ^ p)
⊢ False
[PROOFSTEP]
set Q := minpoly ℤ (μ ^ p)
[GOAL]
case neg
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hn : ¬n = 0
hpos : 0 < n
P : ℤ[X] := minpoly ℤ μ
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hdiff : ¬P = Q
⊢ False
[PROOFSTEP]
have Pmonic : P.Monic := minpoly.monic (h.isIntegral hpos)
[GOAL]
case neg
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hn : ¬n = 0
hpos : 0 < n
P : ℤ[X] := minpoly ℤ μ
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hdiff : ¬P = Q
Pmonic : Monic P
⊢ False
[PROOFSTEP]
have Qmonic : Q.Monic := minpoly.monic ((h.pow_of_prime hprime.1 hdiv).isIntegral hpos)
[GOAL]
case neg
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hn : ¬n = 0
hpos : 0 < n
P : ℤ[X] := minpoly ℤ μ
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hdiff : ¬P = Q
Pmonic : Monic P
Qmonic : Monic Q
⊢ False
[PROOFSTEP]
have Pirr : Irreducible P := minpoly.irreducible (h.isIntegral hpos)
[GOAL]
case neg
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hn : ¬n = 0
hpos : 0 < n
P : ℤ[X] := minpoly ℤ μ
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hdiff : ¬P = Q
Pmonic : Monic P
Qmonic : Monic Q
Pirr : Irreducible P
⊢ False
[PROOFSTEP]
have Qirr : Irreducible Q := minpoly.irreducible ((h.pow_of_prime hprime.1 hdiv).isIntegral hpos)
[GOAL]
case neg
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hn : ¬n = 0
hpos : 0 < n
P : ℤ[X] := minpoly ℤ μ
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hdiff : ¬P = Q
Pmonic : Monic P
Qmonic : Monic Q
Pirr : Irreducible P
Qirr : Irreducible Q
⊢ False
[PROOFSTEP]
have PQprim : IsPrimitive (P * Q) := Pmonic.isPrimitive.mul Qmonic.isPrimitive
[GOAL]
case neg
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hn : ¬n = 0
hpos : 0 < n
P : ℤ[X] := minpoly ℤ μ
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hdiff : ¬P = Q
Pmonic : Monic P
Qmonic : Monic Q
Pirr : Irreducible P
Qirr : Irreducible Q
PQprim : IsPrimitive (P * Q)
⊢ False
[PROOFSTEP]
have prod : P * Q ∣ X ^ n - 1 :=
  by
  rw [IsPrimitive.Int.dvd_iff_map_cast_dvd_map_cast (P * Q) (X ^ n - 1) PQprim
      (monic_X_pow_sub_C (1 : ℤ) (ne_of_gt hpos)).isPrimitive,
    Polynomial.map_mul]
  refine' IsCoprime.mul_dvd _ _ _
  · have aux := IsPrimitive.Int.irreducible_iff_irreducible_map_cast Pmonic.isPrimitive
    refine' (dvd_or_coprime _ _ (aux.1 Pirr)).resolve_left _
    rw [map_dvd_map (Int.castRingHom ℚ) Int.cast_injective Pmonic]
    intro hdiv
    refine' hdiff (eq_of_monic_of_associated Pmonic Qmonic _)
    exact associated_of_dvd_dvd hdiv (Pirr.dvd_symm Qirr hdiv)
  · apply (map_dvd_map (Int.castRingHom ℚ) Int.cast_injective Pmonic).2
    exact minpoly_dvd_x_pow_sub_one h
  · apply (map_dvd_map (Int.castRingHom ℚ) Int.cast_injective Qmonic).2
    exact minpoly_dvd_x_pow_sub_one (pow_of_prime h hprime.1 hdiv)
[GOAL]
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hn : ¬n = 0
hpos : 0 < n
P : ℤ[X] := minpoly ℤ μ
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hdiff : ¬P = Q
Pmonic : Monic P
Qmonic : Monic Q
Pirr : Irreducible P
Qirr : Irreducible Q
PQprim : IsPrimitive (P * Q)
⊢ P * Q ∣ X ^ n - 1
[PROOFSTEP]
rw [IsPrimitive.Int.dvd_iff_map_cast_dvd_map_cast (P * Q) (X ^ n - 1) PQprim
    (monic_X_pow_sub_C (1 : ℤ) (ne_of_gt hpos)).isPrimitive,
  Polynomial.map_mul]
[GOAL]
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hn : ¬n = 0
hpos : 0 < n
P : ℤ[X] := minpoly ℤ μ
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hdiff : ¬P = Q
Pmonic : Monic P
Qmonic : Monic Q
Pirr : Irreducible P
Qirr : Irreducible Q
PQprim : IsPrimitive (P * Q)
⊢ map (Int.castRingHom ℚ) P * map (Int.castRingHom ℚ) Q ∣ map (Int.castRingHom ℚ) (X ^ n - 1)
[PROOFSTEP]
refine' IsCoprime.mul_dvd _ _ _
[GOAL]
case refine'_1
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hn : ¬n = 0
hpos : 0 < n
P : ℤ[X] := minpoly ℤ μ
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hdiff : ¬P = Q
Pmonic : Monic P
Qmonic : Monic Q
Pirr : Irreducible P
Qirr : Irreducible Q
PQprim : IsPrimitive (P * Q)
⊢ IsCoprime (map (Int.castRingHom ℚ) P) (map (Int.castRingHom ℚ) Q)
[PROOFSTEP]
have aux := IsPrimitive.Int.irreducible_iff_irreducible_map_cast Pmonic.isPrimitive
[GOAL]
case refine'_1
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hn : ¬n = 0
hpos : 0 < n
P : ℤ[X] := minpoly ℤ μ
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hdiff : ¬P = Q
Pmonic : Monic P
Qmonic : Monic Q
Pirr : Irreducible P
Qirr : Irreducible Q
PQprim : IsPrimitive (P * Q)
aux : Irreducible P ↔ Irreducible (map (Int.castRingHom ℚ) P)
⊢ IsCoprime (map (Int.castRingHom ℚ) P) (map (Int.castRingHom ℚ) Q)
[PROOFSTEP]
refine' (dvd_or_coprime _ _ (aux.1 Pirr)).resolve_left _
[GOAL]
case refine'_1
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hn : ¬n = 0
hpos : 0 < n
P : ℤ[X] := minpoly ℤ μ
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hdiff : ¬P = Q
Pmonic : Monic P
Qmonic : Monic Q
Pirr : Irreducible P
Qirr : Irreducible Q
PQprim : IsPrimitive (P * Q)
aux : Irreducible P ↔ Irreducible (map (Int.castRingHom ℚ) P)
⊢ ¬map (Int.castRingHom ℚ) P ∣ map (Int.castRingHom ℚ) Q
[PROOFSTEP]
rw [map_dvd_map (Int.castRingHom ℚ) Int.cast_injective Pmonic]
[GOAL]
case refine'_1
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hn : ¬n = 0
hpos : 0 < n
P : ℤ[X] := minpoly ℤ μ
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hdiff : ¬P = Q
Pmonic : Monic P
Qmonic : Monic Q
Pirr : Irreducible P
Qirr : Irreducible Q
PQprim : IsPrimitive (P * Q)
aux : Irreducible P ↔ Irreducible (map (Int.castRingHom ℚ) P)
⊢ ¬P ∣ Q
[PROOFSTEP]
intro hdiv
[GOAL]
case refine'_1
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv✝ : ¬p ∣ n
hn : ¬n = 0
hpos : 0 < n
P : ℤ[X] := minpoly ℤ μ
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hdiff : ¬P = Q
Pmonic : Monic P
Qmonic : Monic Q
Pirr : Irreducible P
Qirr : Irreducible Q
PQprim : IsPrimitive (P * Q)
aux : Irreducible P ↔ Irreducible (map (Int.castRingHom ℚ) P)
hdiv : P ∣ Q
⊢ False
[PROOFSTEP]
refine' hdiff (eq_of_monic_of_associated Pmonic Qmonic _)
[GOAL]
case refine'_1
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv✝ : ¬p ∣ n
hn : ¬n = 0
hpos : 0 < n
P : ℤ[X] := minpoly ℤ μ
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hdiff : ¬P = Q
Pmonic : Monic P
Qmonic : Monic Q
Pirr : Irreducible P
Qirr : Irreducible Q
PQprim : IsPrimitive (P * Q)
aux : Irreducible P ↔ Irreducible (map (Int.castRingHom ℚ) P)
hdiv : P ∣ Q
⊢ Associated P Q
[PROOFSTEP]
exact associated_of_dvd_dvd hdiv (Pirr.dvd_symm Qirr hdiv)
[GOAL]
case refine'_2
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hn : ¬n = 0
hpos : 0 < n
P : ℤ[X] := minpoly ℤ μ
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hdiff : ¬P = Q
Pmonic : Monic P
Qmonic : Monic Q
Pirr : Irreducible P
Qirr : Irreducible Q
PQprim : IsPrimitive (P * Q)
⊢ map (Int.castRingHom ℚ) P ∣ map (Int.castRingHom ℚ) (X ^ n - 1)
[PROOFSTEP]
apply (map_dvd_map (Int.castRingHom ℚ) Int.cast_injective Pmonic).2
[GOAL]
case refine'_2
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hn : ¬n = 0
hpos : 0 < n
P : ℤ[X] := minpoly ℤ μ
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hdiff : ¬P = Q
Pmonic : Monic P
Qmonic : Monic Q
Pirr : Irreducible P
Qirr : Irreducible Q
PQprim : IsPrimitive (P * Q)
⊢ P ∣ X ^ n - 1
[PROOFSTEP]
exact minpoly_dvd_x_pow_sub_one h
[GOAL]
case refine'_3
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hn : ¬n = 0
hpos : 0 < n
P : ℤ[X] := minpoly ℤ μ
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hdiff : ¬P = Q
Pmonic : Monic P
Qmonic : Monic Q
Pirr : Irreducible P
Qirr : Irreducible Q
PQprim : IsPrimitive (P * Q)
⊢ map (Int.castRingHom ℚ) Q ∣ map (Int.castRingHom ℚ) (X ^ n - 1)
[PROOFSTEP]
apply (map_dvd_map (Int.castRingHom ℚ) Int.cast_injective Qmonic).2
[GOAL]
case refine'_3
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hn : ¬n = 0
hpos : 0 < n
P : ℤ[X] := minpoly ℤ μ
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hdiff : ¬P = Q
Pmonic : Monic P
Qmonic : Monic Q
Pirr : Irreducible P
Qirr : Irreducible Q
PQprim : IsPrimitive (P * Q)
⊢ Q ∣ X ^ n - 1
[PROOFSTEP]
exact minpoly_dvd_x_pow_sub_one (pow_of_prime h hprime.1 hdiv)
[GOAL]
case neg
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hn : ¬n = 0
hpos : 0 < n
P : ℤ[X] := minpoly ℤ μ
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hdiff : ¬P = Q
Pmonic : Monic P
Qmonic : Monic Q
Pirr : Irreducible P
Qirr : Irreducible Q
PQprim : IsPrimitive (P * Q)
prod : P * Q ∣ X ^ n - 1
⊢ False
[PROOFSTEP]
replace prod := RingHom.map_dvd (mapRingHom (Int.castRingHom (ZMod p))) prod
[GOAL]
case neg
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hn : ¬n = 0
hpos : 0 < n
P : ℤ[X] := minpoly ℤ μ
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hdiff : ¬P = Q
Pmonic : Monic P
Qmonic : Monic Q
Pirr : Irreducible P
Qirr : Irreducible Q
PQprim : IsPrimitive (P * Q)
prod : ↑(mapRingHom (Int.castRingHom (ZMod p))) (P * Q) ∣ ↑(mapRingHom (Int.castRingHom (ZMod p))) (X ^ n - 1)
⊢ False
[PROOFSTEP]
rw [coe_mapRingHom, Polynomial.map_mul, Polynomial.map_sub, Polynomial.map_one, Polynomial.map_pow, map_X] at prod
[GOAL]
case neg
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hn : ¬n = 0
hpos : 0 < n
P : ℤ[X] := minpoly ℤ μ
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hdiff : ¬P = Q
Pmonic : Monic P
Qmonic : Monic Q
Pirr : Irreducible P
Qirr : Irreducible Q
PQprim : IsPrimitive (P * Q)
prod : map (Int.castRingHom (ZMod p)) P * map (Int.castRingHom (ZMod p)) Q ∣ X ^ n - 1
⊢ False
[PROOFSTEP]
obtain ⟨R, hR⟩ := minpoly_dvd_mod_p h hdiv
[GOAL]
case neg.intro
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hn : ¬n = 0
hpos : 0 < n
P : ℤ[X] := minpoly ℤ μ
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hdiff : ¬P = Q
Pmonic : Monic P
Qmonic : Monic Q
Pirr : Irreducible P
Qirr : Irreducible Q
PQprim : IsPrimitive (P * Q)
prod : map (Int.castRingHom (ZMod p)) P * map (Int.castRingHom (ZMod p)) Q ∣ X ^ n - 1
R : (ZMod p)[X]
hR : map (Int.castRingHom (ZMod p)) (minpoly ℤ (μ ^ p)) = map (Int.castRingHom (ZMod p)) (minpoly ℤ μ) * R
⊢ False
[PROOFSTEP]
rw [hR, ← mul_assoc, ← Polynomial.map_mul, ← sq, Polynomial.map_pow] at prod
[GOAL]
case neg.intro
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hn : ¬n = 0
hpos : 0 < n
P : ℤ[X] := minpoly ℤ μ
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hdiff : ¬P = Q
Pmonic : Monic P
Qmonic : Monic Q
Pirr : Irreducible P
Qirr : Irreducible Q
PQprim : IsPrimitive (P * Q)
R : (ZMod p)[X]
prod : map (Int.castRingHom (ZMod p)) P ^ 2 * R ∣ X ^ n - 1
hR : map (Int.castRingHom (ZMod p)) (minpoly ℤ (μ ^ p)) = map (Int.castRingHom (ZMod p)) (minpoly ℤ μ) * R
⊢ False
[PROOFSTEP]
have habs : map (Int.castRingHom (ZMod p)) P ^ 2 ∣ map (Int.castRingHom (ZMod p)) P ^ 2 * R := by use R
[GOAL]
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hn : ¬n = 0
hpos : 0 < n
P : ℤ[X] := minpoly ℤ μ
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hdiff : ¬P = Q
Pmonic : Monic P
Qmonic : Monic Q
Pirr : Irreducible P
Qirr : Irreducible Q
PQprim : IsPrimitive (P * Q)
R : (ZMod p)[X]
prod : map (Int.castRingHom (ZMod p)) P ^ 2 * R ∣ X ^ n - 1
hR : map (Int.castRingHom (ZMod p)) (minpoly ℤ (μ ^ p)) = map (Int.castRingHom (ZMod p)) (minpoly ℤ μ) * R
⊢ map (Int.castRingHom (ZMod p)) P ^ 2 ∣ map (Int.castRingHom (ZMod p)) P ^ 2 * R
[PROOFSTEP]
use R
[GOAL]
case neg.intro
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hn : ¬n = 0
hpos : 0 < n
P : ℤ[X] := minpoly ℤ μ
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hdiff : ¬P = Q
Pmonic : Monic P
Qmonic : Monic Q
Pirr : Irreducible P
Qirr : Irreducible Q
PQprim : IsPrimitive (P * Q)
R : (ZMod p)[X]
prod : map (Int.castRingHom (ZMod p)) P ^ 2 * R ∣ X ^ n - 1
hR : map (Int.castRingHom (ZMod p)) (minpoly ℤ (μ ^ p)) = map (Int.castRingHom (ZMod p)) (minpoly ℤ μ) * R
habs : map (Int.castRingHom (ZMod p)) P ^ 2 ∣ map (Int.castRingHom (ZMod p)) P ^ 2 * R
⊢ False
[PROOFSTEP]
replace habs :=
  lt_of_lt_of_le (PartENat.coe_lt_coe.2 one_lt_two) (multiplicity.le_multiplicity_of_pow_dvd (dvd_trans habs prod))
[GOAL]
case neg.intro
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hn : ¬n = 0
hpos : 0 < n
P : ℤ[X] := minpoly ℤ μ
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hdiff : ¬P = Q
Pmonic : Monic P
Qmonic : Monic Q
Pirr : Irreducible P
Qirr : Irreducible Q
PQprim : IsPrimitive (P * Q)
R : (ZMod p)[X]
prod : map (Int.castRingHom (ZMod p)) P ^ 2 * R ∣ X ^ n - 1
hR : map (Int.castRingHom (ZMod p)) (minpoly ℤ (μ ^ p)) = map (Int.castRingHom (ZMod p)) (minpoly ℤ μ) * R
habs : ↑1 < multiplicity (map (Int.castRingHom (ZMod p)) P) (X ^ n - 1)
⊢ False
[PROOFSTEP]
have hfree : Squarefree (X ^ n - 1 : (ZMod p)[X]) :=
  (separable_X_pow_sub_C 1 (fun h => hdiv <| (ZMod.nat_cast_zmod_eq_zero_iff_dvd n p).1 h) one_ne_zero).squarefree
[GOAL]
case neg.intro
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hn : ¬n = 0
hpos : 0 < n
P : ℤ[X] := minpoly ℤ μ
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hdiff : ¬P = Q
Pmonic : Monic P
Qmonic : Monic Q
Pirr : Irreducible P
Qirr : Irreducible Q
PQprim : IsPrimitive (P * Q)
R : (ZMod p)[X]
prod : map (Int.castRingHom (ZMod p)) P ^ 2 * R ∣ X ^ n - 1
hR : map (Int.castRingHom (ZMod p)) (minpoly ℤ (μ ^ p)) = map (Int.castRingHom (ZMod p)) (minpoly ℤ μ) * R
habs : ↑1 < multiplicity (map (Int.castRingHom (ZMod p)) P) (X ^ n - 1)
hfree : Squarefree (X ^ n - 1)
⊢ False
[PROOFSTEP]
cases' (multiplicity.squarefree_iff_multiplicity_le_one (X ^ n - 1)).1 hfree (map (Int.castRingHom (ZMod p)) P) with hle
  hunit
[GOAL]
case neg.intro.inl
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hn : ¬n = 0
hpos : 0 < n
P : ℤ[X] := minpoly ℤ μ
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hdiff : ¬P = Q
Pmonic : Monic P
Qmonic : Monic Q
Pirr : Irreducible P
Qirr : Irreducible Q
PQprim : IsPrimitive (P * Q)
R : (ZMod p)[X]
prod : map (Int.castRingHom (ZMod p)) P ^ 2 * R ∣ X ^ n - 1
hR : map (Int.castRingHom (ZMod p)) (minpoly ℤ (μ ^ p)) = map (Int.castRingHom (ZMod p)) (minpoly ℤ μ) * R
habs : ↑1 < multiplicity (map (Int.castRingHom (ZMod p)) P) (X ^ n - 1)
hfree : Squarefree (X ^ n - 1)
hle : multiplicity (map (Int.castRingHom (ZMod p)) P) (X ^ n - 1) ≤ 1
⊢ False
[PROOFSTEP]
rw [Nat.cast_one] at habs
[GOAL]
case neg.intro.inl
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hn : ¬n = 0
hpos : 0 < n
P : ℤ[X] := minpoly ℤ μ
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hdiff : ¬P = Q
Pmonic : Monic P
Qmonic : Monic Q
Pirr : Irreducible P
Qirr : Irreducible Q
PQprim : IsPrimitive (P * Q)
R : (ZMod p)[X]
prod : map (Int.castRingHom (ZMod p)) P ^ 2 * R ∣ X ^ n - 1
hR : map (Int.castRingHom (ZMod p)) (minpoly ℤ (μ ^ p)) = map (Int.castRingHom (ZMod p)) (minpoly ℤ μ) * R
habs : 1 < multiplicity (map (Int.castRingHom (ZMod p)) P) (X ^ n - 1)
hfree : Squarefree (X ^ n - 1)
hle : multiplicity (map (Int.castRingHom (ZMod p)) P) (X ^ n - 1) ≤ 1
⊢ False
[PROOFSTEP]
exact hle.not_lt habs
[GOAL]
case neg.intro.inr
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hn : ¬n = 0
hpos : 0 < n
P : ℤ[X] := minpoly ℤ μ
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hdiff : ¬P = Q
Pmonic : Monic P
Qmonic : Monic Q
Pirr : Irreducible P
Qirr : Irreducible Q
PQprim : IsPrimitive (P * Q)
R : (ZMod p)[X]
prod : map (Int.castRingHom (ZMod p)) P ^ 2 * R ∣ X ^ n - 1
hR : map (Int.castRingHom (ZMod p)) (minpoly ℤ (μ ^ p)) = map (Int.castRingHom (ZMod p)) (minpoly ℤ μ) * R
habs : ↑1 < multiplicity (map (Int.castRingHom (ZMod p)) P) (X ^ n - 1)
hfree : Squarefree (X ^ n - 1)
hunit : IsUnit (map (Int.castRingHom (ZMod p)) P)
⊢ False
[PROOFSTEP]
replace hunit := degree_eq_zero_of_isUnit hunit
[GOAL]
case neg.intro.inr
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hn : ¬n = 0
hpos : 0 < n
P : ℤ[X] := minpoly ℤ μ
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hdiff : ¬P = Q
Pmonic : Monic P
Qmonic : Monic Q
Pirr : Irreducible P
Qirr : Irreducible Q
PQprim : IsPrimitive (P * Q)
R : (ZMod p)[X]
prod : map (Int.castRingHom (ZMod p)) P ^ 2 * R ∣ X ^ n - 1
hR : map (Int.castRingHom (ZMod p)) (minpoly ℤ (μ ^ p)) = map (Int.castRingHom (ZMod p)) (minpoly ℤ μ) * R
habs : ↑1 < multiplicity (map (Int.castRingHom (ZMod p)) P) (X ^ n - 1)
hfree : Squarefree (X ^ n - 1)
hunit : degree (map (Int.castRingHom (ZMod p)) P) = 0
⊢ False
[PROOFSTEP]
rw [degree_map_eq_of_leadingCoeff_ne_zero (Int.castRingHom (ZMod p)) _] at hunit
[GOAL]
case neg.intro.inr
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hn : ¬n = 0
hpos : 0 < n
P : ℤ[X] := minpoly ℤ μ
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hdiff : ¬P = Q
Pmonic : Monic P
Qmonic : Monic Q
Pirr : Irreducible P
Qirr : Irreducible Q
PQprim : IsPrimitive (P * Q)
R : (ZMod p)[X]
prod : map (Int.castRingHom (ZMod p)) P ^ 2 * R ∣ X ^ n - 1
hR : map (Int.castRingHom (ZMod p)) (minpoly ℤ (μ ^ p)) = map (Int.castRingHom (ZMod p)) (minpoly ℤ μ) * R
habs : ↑1 < multiplicity (map (Int.castRingHom (ZMod p)) P) (X ^ n - 1)
hfree : Squarefree (X ^ n - 1)
hunit : degree P = 0
⊢ False
[PROOFSTEP]
exact (minpoly.degree_pos (isIntegral h hpos)).ne' hunit
[GOAL]
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hn : ¬n = 0
hpos : 0 < n
P : ℤ[X] := minpoly ℤ μ
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hdiff : ¬P = Q
Pmonic : Monic P
Qmonic : Monic Q
Pirr : Irreducible P
Qirr : Irreducible Q
PQprim : IsPrimitive (P * Q)
R : (ZMod p)[X]
prod : map (Int.castRingHom (ZMod p)) P ^ 2 * R ∣ X ^ n - 1
hR : map (Int.castRingHom (ZMod p)) (minpoly ℤ (μ ^ p)) = map (Int.castRingHom (ZMod p)) (minpoly ℤ μ) * R
habs : ↑1 < multiplicity (map (Int.castRingHom (ZMod p)) P) (X ^ n - 1)
hfree : Squarefree (X ^ n - 1)
hunit : degree (map (Int.castRingHom (ZMod p)) P) = 0
⊢ ↑(Int.castRingHom (ZMod p)) (leadingCoeff P) ≠ 0
[PROOFSTEP]
simp only [Pmonic, eq_intCast, Monic.leadingCoeff, Int.cast_one, Ne.def, not_false_iff, one_ne_zero]
[GOAL]
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
m : ℕ
hcop : Nat.coprime m n
⊢ minpoly ℤ μ = minpoly ℤ (μ ^ m)
[PROOFSTEP]
revert n hcop
[GOAL]
K : Type u_1
inst✝² : CommRing K
μ : K
inst✝¹ : IsDomain K
inst✝ : CharZero K
m : ℕ
⊢ ∀ {n : ℕ}, IsPrimitiveRoot μ n → Nat.coprime m n → minpoly ℤ μ = minpoly ℤ (μ ^ m)
[PROOFSTEP]
refine' UniqueFactorizationMonoid.induction_on_prime m _ _ _
[GOAL]
case refine'_1
K : Type u_1
inst✝² : CommRing K
μ : K
inst✝¹ : IsDomain K
inst✝ : CharZero K
m n✝ : ℕ
⊢ IsPrimitiveRoot μ n✝ → Nat.coprime 0 n✝ → minpoly ℤ μ = minpoly ℤ (μ ^ 0)
[PROOFSTEP]
intro h hn
[GOAL]
case refine'_1
K : Type u_1
inst✝² : CommRing K
μ : K
inst✝¹ : IsDomain K
inst✝ : CharZero K
m n✝ : ℕ
h : IsPrimitiveRoot μ n✝
hn : Nat.coprime 0 n✝
⊢ minpoly ℤ μ = minpoly ℤ (μ ^ 0)
[PROOFSTEP]
congr
[GOAL]
case refine'_1.e_x
K : Type u_1
inst✝² : CommRing K
μ : K
inst✝¹ : IsDomain K
inst✝ : CharZero K
m n✝ : ℕ
h : IsPrimitiveRoot μ n✝
hn : Nat.coprime 0 n✝
⊢ μ = μ ^ 0
[PROOFSTEP]
simpa [(Nat.coprime_zero_left _).mp hn] using h
[GOAL]
case refine'_2
K : Type u_1
inst✝² : CommRing K
μ : K
inst✝¹ : IsDomain K
inst✝ : CharZero K
m n✝ : ℕ
⊢ ∀ (x : ℕ), IsUnit x → IsPrimitiveRoot μ n✝ → Nat.coprime x n✝ → minpoly ℤ μ = minpoly ℤ (μ ^ x)
[PROOFSTEP]
intro u hunit _ _
[GOAL]
case refine'_2
K : Type u_1
inst✝² : CommRing K
μ : K
inst✝¹ : IsDomain K
inst✝ : CharZero K
m n✝ u : ℕ
hunit : IsUnit u
h✝ : IsPrimitiveRoot μ n✝
hcop✝ : Nat.coprime u n✝
⊢ minpoly ℤ μ = minpoly ℤ (μ ^ u)
[PROOFSTEP]
congr
[GOAL]
case refine'_2.e_x
K : Type u_1
inst✝² : CommRing K
μ : K
inst✝¹ : IsDomain K
inst✝ : CharZero K
m n✝ u : ℕ
hunit : IsUnit u
h✝ : IsPrimitiveRoot μ n✝
hcop✝ : Nat.coprime u n✝
⊢ μ = μ ^ u
[PROOFSTEP]
simp [Nat.isUnit_iff.mp hunit]
[GOAL]
case refine'_3
K : Type u_1
inst✝² : CommRing K
μ : K
inst✝¹ : IsDomain K
inst✝ : CharZero K
m n✝ : ℕ
⊢ ∀ (a p : ℕ),
    a ≠ 0 →
      Prime p →
        (IsPrimitiveRoot μ n✝ → Nat.coprime a n✝ → minpoly ℤ μ = minpoly ℤ (μ ^ a)) →
          IsPrimitiveRoot μ n✝ → Nat.coprime (p * a) n✝ → minpoly ℤ μ = minpoly ℤ (μ ^ (p * a))
[PROOFSTEP]
intro a p _ hprime
[GOAL]
case refine'_3
K : Type u_1
inst✝² : CommRing K
μ : K
inst✝¹ : IsDomain K
inst✝ : CharZero K
m n✝ a p : ℕ
a✝ : a ≠ 0
hprime : Prime p
⊢ (IsPrimitiveRoot μ n✝ → Nat.coprime a n✝ → minpoly ℤ μ = minpoly ℤ (μ ^ a)) →
    IsPrimitiveRoot μ n✝ → Nat.coprime (p * a) n✝ → minpoly ℤ μ = minpoly ℤ (μ ^ (p * a))
[PROOFSTEP]
intro hind h hcop
[GOAL]
case refine'_3
K : Type u_1
inst✝² : CommRing K
μ : K
inst✝¹ : IsDomain K
inst✝ : CharZero K
m n✝ a p : ℕ
a✝ : a ≠ 0
hprime : Prime p
hind : IsPrimitiveRoot μ n✝ → Nat.coprime a n✝ → minpoly ℤ μ = minpoly ℤ (μ ^ a)
h : IsPrimitiveRoot μ n✝
hcop : Nat.coprime (p * a) n✝
⊢ minpoly ℤ μ = minpoly ℤ (μ ^ (p * a))
[PROOFSTEP]
rw [hind h (Nat.coprime.coprime_mul_left hcop)]
[GOAL]
case refine'_3
K : Type u_1
inst✝² : CommRing K
μ : K
inst✝¹ : IsDomain K
inst✝ : CharZero K
m n✝ a p : ℕ
a✝ : a ≠ 0
hprime : Prime p
hind : IsPrimitiveRoot μ n✝ → Nat.coprime a n✝ → minpoly ℤ μ = minpoly ℤ (μ ^ a)
h : IsPrimitiveRoot μ n✝
hcop : Nat.coprime (p * a) n✝
⊢ minpoly ℤ (μ ^ a) = minpoly ℤ (μ ^ (p * a))
[PROOFSTEP]
clear hind
[GOAL]
case refine'_3
K : Type u_1
inst✝² : CommRing K
μ : K
inst✝¹ : IsDomain K
inst✝ : CharZero K
m n✝ a p : ℕ
a✝ : a ≠ 0
hprime : Prime p
h : IsPrimitiveRoot μ n✝
hcop : Nat.coprime (p * a) n✝
⊢ minpoly ℤ (μ ^ a) = minpoly ℤ (μ ^ (p * a))
[PROOFSTEP]
replace hprime := hprime.nat_prime
[GOAL]
case refine'_3
K : Type u_1
inst✝² : CommRing K
μ : K
inst✝¹ : IsDomain K
inst✝ : CharZero K
m n✝ a p : ℕ
a✝ : a ≠ 0
h : IsPrimitiveRoot μ n✝
hcop : Nat.coprime (p * a) n✝
hprime : Nat.Prime p
⊢ minpoly ℤ (μ ^ a) = minpoly ℤ (μ ^ (p * a))
[PROOFSTEP]
have hdiv := (Nat.Prime.coprime_iff_not_dvd hprime).1 (Nat.coprime.coprime_mul_right hcop)
[GOAL]
case refine'_3
K : Type u_1
inst✝² : CommRing K
μ : K
inst✝¹ : IsDomain K
inst✝ : CharZero K
m n✝ a p : ℕ
a✝ : a ≠ 0
h : IsPrimitiveRoot μ n✝
hcop : Nat.coprime (p * a) n✝
hprime : Nat.Prime p
hdiv : ¬p ∣ n✝
⊢ minpoly ℤ (μ ^ a) = minpoly ℤ (μ ^ (p * a))
[PROOFSTEP]
haveI := Fact.mk hprime
[GOAL]
case refine'_3
K : Type u_1
inst✝² : CommRing K
μ : K
inst✝¹ : IsDomain K
inst✝ : CharZero K
m n✝ a p : ℕ
a✝ : a ≠ 0
h : IsPrimitiveRoot μ n✝
hcop : Nat.coprime (p * a) n✝
hprime : Nat.Prime p
hdiv : ¬p ∣ n✝
this : Fact (Nat.Prime p)
⊢ minpoly ℤ (μ ^ a) = minpoly ℤ (μ ^ (p * a))
[PROOFSTEP]
rw [minpoly_eq_pow (h.pow_of_coprime a (Nat.coprime.coprime_mul_left hcop)) hdiv]
[GOAL]
case refine'_3
K : Type u_1
inst✝² : CommRing K
μ : K
inst✝¹ : IsDomain K
inst✝ : CharZero K
m n✝ a p : ℕ
a✝ : a ≠ 0
h : IsPrimitiveRoot μ n✝
hcop : Nat.coprime (p * a) n✝
hprime : Nat.Prime p
hdiv : ¬p ∣ n✝
this : Fact (Nat.Prime p)
⊢ minpoly ℤ ((μ ^ a) ^ p) = minpoly ℤ (μ ^ (p * a))
[PROOFSTEP]
congr 1
[GOAL]
case refine'_3.e_x
K : Type u_1
inst✝² : CommRing K
μ : K
inst✝¹ : IsDomain K
inst✝ : CharZero K
m n✝ a p : ℕ
a✝ : a ≠ 0
h : IsPrimitiveRoot μ n✝
hcop : Nat.coprime (p * a) n✝
hprime : Nat.Prime p
hdiv : ¬p ∣ n✝
this : Fact (Nat.Prime p)
⊢ (μ ^ a) ^ p = μ ^ (p * a)
[PROOFSTEP]
ring
[GOAL]
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
m : ℕ
hcop : Nat.coprime m n
⊢ IsRoot (map (Int.castRingHom K) (minpoly ℤ μ)) (μ ^ m)
[PROOFSTEP]
simp only [minpoly_eq_pow_coprime h hcop, IsRoot.def, eval_map]
[GOAL]
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
m : ℕ
hcop : Nat.coprime m n
⊢ eval₂ (Int.castRingHom K) (μ ^ m) (minpoly ℤ (μ ^ m)) = 0
[PROOFSTEP]
exact minpoly.aeval ℤ (μ ^ m)
[GOAL]
n : ℕ
K : Type u_1
inst✝³ : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝² : IsDomain K
inst✝¹ : CharZero K
inst✝ : DecidableEq K
⊢ primitiveRoots n K ⊆ Multiset.toFinset (roots (map (Int.castRingHom K) (minpoly ℤ μ)))
[PROOFSTEP]
by_cases hn : n = 0
[GOAL]
case pos
n : ℕ
K : Type u_1
inst✝³ : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝² : IsDomain K
inst✝¹ : CharZero K
inst✝ : DecidableEq K
hn : n = 0
⊢ primitiveRoots n K ⊆ Multiset.toFinset (roots (map (Int.castRingHom K) (minpoly ℤ μ)))
[PROOFSTEP]
simp_all
[GOAL]
case neg
n : ℕ
K : Type u_1
inst✝³ : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝² : IsDomain K
inst✝¹ : CharZero K
inst✝ : DecidableEq K
hn : ¬n = 0
⊢ primitiveRoots n K ⊆ Multiset.toFinset (roots (map (Int.castRingHom K) (minpoly ℤ μ)))
[PROOFSTEP]
have hpos := Nat.pos_of_ne_zero hn
[GOAL]
case neg
n : ℕ
K : Type u_1
inst✝³ : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝² : IsDomain K
inst✝¹ : CharZero K
inst✝ : DecidableEq K
hn : ¬n = 0
hpos : 0 < n
⊢ primitiveRoots n K ⊆ Multiset.toFinset (roots (map (Int.castRingHom K) (minpoly ℤ μ)))
[PROOFSTEP]
intro x hx
[GOAL]
case neg
n : ℕ
K : Type u_1
inst✝³ : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝² : IsDomain K
inst✝¹ : CharZero K
inst✝ : DecidableEq K
hn : ¬n = 0
hpos : 0 < n
x : K
hx : x ∈ primitiveRoots n K
⊢ x ∈ Multiset.toFinset (roots (map (Int.castRingHom K) (minpoly ℤ μ)))
[PROOFSTEP]
obtain ⟨m, _, hcop, rfl⟩ := (isPrimitiveRoot_iff h hpos).1 ((mem_primitiveRoots hpos).1 hx)
[GOAL]
case neg.intro.intro.intro
n : ℕ
K : Type u_1
inst✝³ : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝² : IsDomain K
inst✝¹ : CharZero K
inst✝ : DecidableEq K
hn : ¬n = 0
hpos : 0 < n
m : ℕ
left✝ : m < n
hcop : Nat.coprime m n
hx : μ ^ m ∈ primitiveRoots n K
⊢ μ ^ m ∈ Multiset.toFinset (roots (map (Int.castRingHom K) (minpoly ℤ μ)))
[PROOFSTEP]
simp only [Multiset.mem_toFinset, mem_roots]
[GOAL]
case neg.intro.intro.intro
n : ℕ
K : Type u_1
inst✝³ : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝² : IsDomain K
inst✝¹ : CharZero K
inst✝ : DecidableEq K
hn : ¬n = 0
hpos : 0 < n
m : ℕ
left✝ : m < n
hcop : Nat.coprime m n
hx : μ ^ m ∈ primitiveRoots n K
⊢ μ ^ m ∈ roots (map (Int.castRingHom K) (minpoly ℤ μ))
[PROOFSTEP]
convert pow_isRoot_minpoly h hcop
[GOAL]
case a
n : ℕ
K : Type u_1
inst✝³ : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝² : IsDomain K
inst✝¹ : CharZero K
inst✝ : DecidableEq K
hn : ¬n = 0
hpos : 0 < n
m : ℕ
left✝ : m < n
hcop : Nat.coprime m n
hx : μ ^ m ∈ primitiveRoots n K
⊢ μ ^ m ∈ roots (map (Int.castRingHom K) (minpoly ℤ μ)) ↔ IsRoot (map (Int.castRingHom K) (minpoly ℤ μ)) (μ ^ m)
[PROOFSTEP]
rw [← mem_roots]
[GOAL]
case a
n : ℕ
K : Type u_1
inst✝³ : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝² : IsDomain K
inst✝¹ : CharZero K
inst✝ : DecidableEq K
hn : ¬n = 0
hpos : 0 < n
m : ℕ
left✝ : m < n
hcop : Nat.coprime m n
hx : μ ^ m ∈ primitiveRoots n K
⊢ map (Int.castRingHom K) (minpoly ℤ μ) ≠ 0
[PROOFSTEP]
exact map_monic_ne_zero <| minpoly.monic <| isIntegral h hpos
[GOAL]
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
⊢ Nat.totient n ≤ natDegree (minpoly ℤ μ)
[PROOFSTEP]
classical
let P : ℤ[X] := minpoly ℤ μ
let P_K : K[X] := map (Int.castRingHom K) P
calc
  n.totient = (primitiveRoots n K).card := h.card_primitiveRoots.symm
  _ ≤ P_K.roots.toFinset.card := (Finset.card_le_of_subset (is_roots_of_minpoly h))
  _ ≤ Multiset.card P_K.roots := (Multiset.toFinset_card_le _)
  _ ≤ P_K.natDegree := (card_roots' _)
  _ ≤ P.natDegree := natDegree_map_le _ _
[GOAL]
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
⊢ Nat.totient n ≤ natDegree (minpoly ℤ μ)
[PROOFSTEP]
let P : ℤ[X] := minpoly ℤ μ
[GOAL]
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
P : ℤ[X] := minpoly ℤ μ
⊢ Nat.totient n ≤ natDegree (minpoly ℤ μ)
[PROOFSTEP]
let P_K : K[X] := map (Int.castRingHom K) P
[GOAL]
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
P : ℤ[X] := minpoly ℤ μ
P_K : K[X] := map (Int.castRingHom K) P
⊢ Nat.totient n ≤ natDegree (minpoly ℤ μ)
[PROOFSTEP]
calc
  n.totient = (primitiveRoots n K).card := h.card_primitiveRoots.symm
  _ ≤ P_K.roots.toFinset.card := (Finset.card_le_of_subset (is_roots_of_minpoly h))
  _ ≤ Multiset.card P_K.roots := (Multiset.toFinset_card_le _)
  _ ≤ P_K.natDegree := (card_roots' _)
  _ ≤ P.natDegree := natDegree_map_le _ _