[GOAL]
α : Type u
β : Type v
inst✝ : Semiring α
I : Ideal α
a b x y : α
hx : x ∈ I
h : y * x = 1
z : α
x✝ : z ∈ ⊤
⊢ z = z * (y * x)
[PROOFSTEP]
simp [h]
[GOAL]
α : Type u
β : Type v
inst✝ : Semiring α
I : Ideal α
a b : α
⊢ I = ⊤ → 1 ∈ I
[PROOFSTEP]
rintro rfl
[GOAL]
α : Type u
β : Type v
inst✝ : Semiring α
a b : α
⊢ 1 ∈ ⊤
[PROOFSTEP]
trivial
[GOAL]
α : Type u
β : Type v
inst✝ : Semiring α
I : Ideal α
a b : α
h : 1 ∈ I
⊢ 1 * 1 = 1
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
inst✝ : Semiring α
I : Ideal α
a b x y : α
hy : IsUnit y
⊢ y * x ∈ I ↔ x ∈ I
[PROOFSTEP]
refine' ⟨fun h => _, fun h => I.mul_mem_left y h⟩
[GOAL]
α : Type u
β : Type v
inst✝ : Semiring α
I : Ideal α
a b x y : α
hy : IsUnit y
h : y * x ∈ I
⊢ x ∈ I
[PROOFSTEP]
obtain ⟨y', hy'⟩ := hy.exists_left_inv
[GOAL]
case intro
α : Type u
β : Type v
inst✝ : Semiring α
I : Ideal α
a b x y : α
hy : IsUnit y
h : y * x ∈ I
y' : α
hy' : y' * y = 1
⊢ x ∈ I
[PROOFSTEP]
have := I.mul_mem_left y' h
[GOAL]
case intro
α : Type u
β : Type v
inst✝ : Semiring α
I : Ideal α
a b x y : α
hy : IsUnit y
h : y * x ∈ I
y' : α
hy' : y' * y = 1
this : y' * (y * x) ∈ I
⊢ x ∈ I
[PROOFSTEP]
rwa [← mul_assoc, hy', one_mul] at this 
[GOAL]
α : Type u
β : Type v
inst✝ : Semiring α
I : Ideal α
a✝ b a : α
h2 : IsUnit a
x : α
⊢ span {a * x} = span {x}
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
α : Type u
β : Type v
inst✝ : Semiring α
I : Ideal α
a✝ b a : α
h2 : IsUnit a
x : α
⊢ span {a * x} ≤ span {x}
[PROOFSTEP]
rw [span_singleton_le_iff_mem, mem_span_singleton']
[GOAL]
case a
α : Type u
β : Type v
inst✝ : Semiring α
I : Ideal α
a✝ b a : α
h2 : IsUnit a
x : α
⊢ span {x} ≤ span {a * x}
[PROOFSTEP]
rw [span_singleton_le_iff_mem, mem_span_singleton']
[GOAL]
case a
α : Type u
β : Type v
inst✝ : Semiring α
I : Ideal α
a✝ b a : α
h2 : IsUnit a
x : α
⊢ ∃ a_1, a_1 * x = a * x
case a α : Type u β : Type v inst✝ : Semiring α I : Ideal α a✝ b a : α h2 : IsUnit a x : α ⊢ ∃ a_1, a_1 * (a * x) = x
[PROOFSTEP]
exacts [⟨a, rfl⟩, ⟨_, h2.unit.inv_mul_cancel_left x⟩]
[GOAL]
α : Type u
β : Type v
inst✝ : Semiring α
I : Ideal α
a b : α
⊢ span 0 = ⊥
[PROOFSTEP]
rw [← Set.singleton_zero, span_singleton_eq_bot]
[GOAL]
α : Type u
β : Type v
inst✝ : Semiring α
I : Ideal α
a b : α
⊢ span 1 = ⊤
[PROOFSTEP]
rw [← Set.singleton_one, span_singleton_one]
[GOAL]
α : Type u
β : Type v
inst✝ : Semiring α
I : Ideal α
a b : α
s : Set α
⊢ span s = ⊤ ↔ ∃ s', ↑s' ⊆ s ∧ span ↑s' = ⊤
[PROOFSTEP]
simp_rw [eq_top_iff_one]
[GOAL]
α : Type u
β : Type v
inst✝ : Semiring α
I : Ideal α
a b : α
s : Set α
⊢ 1 ∈ span s ↔ ∃ s', ↑s' ⊆ s ∧ 1 ∈ span ↑s'
[PROOFSTEP]
exact ⟨Submodule.mem_span_finite_of_mem_span, fun ⟨s', h₁, h₂⟩ => span_mono h₁ h₂⟩
[GOAL]
α : Type u
β : Type v
inst✝¹ : Semiring α
I✝ : Ideal α
a b : α
S : Type u_1
inst✝ : CommSemiring S
x y : S
I : Ideal S
⊢ x ∈ span {y} ⊔ I ↔ ∃ a b, b ∈ I ∧ a * y + b = x
[PROOFSTEP]
rw [Submodule.mem_sup]
[GOAL]
α : Type u
β : Type v
inst✝¹ : Semiring α
I✝ : Ideal α
a b : α
S : Type u_1
inst✝ : CommSemiring S
x y : S
I : Ideal S
⊢ (∃ y_1, y_1 ∈ span {y} ∧ ∃ z, z ∈ I ∧ y_1 + z = x) ↔ ∃ a b, b ∈ I ∧ a * y + b = x
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u
β : Type v
inst✝¹ : Semiring α
I✝ : Ideal α
a b : α
S : Type u_1
inst✝ : CommSemiring S
x y : S
I : Ideal S
⊢ (∃ y_1, y_1 ∈ span {y} ∧ ∃ z, z ∈ I ∧ y_1 + z = x) → ∃ a b, b ∈ I ∧ a * y + b = x
[PROOFSTEP]
rintro ⟨ya, hya, b, hb, rfl⟩
[GOAL]
case mp.intro.intro.intro.intro
α : Type u
β : Type v
inst✝¹ : Semiring α
I✝ : Ideal α
a b✝ : α
S : Type u_1
inst✝ : CommSemiring S
y : S
I : Ideal S
ya : S
hya : ya ∈ span {y}
b : S
hb : b ∈ I
⊢ ∃ a b_1, b_1 ∈ I ∧ a * y + b_1 = ya + b
[PROOFSTEP]
obtain ⟨a, rfl⟩ := mem_span_singleton'.mp hya
[GOAL]
case mp.intro.intro.intro.intro.intro
α : Type u
β : Type v
inst✝¹ : Semiring α
I✝ : Ideal α
a✝ b✝ : α
S : Type u_1
inst✝ : CommSemiring S
y : S
I : Ideal S
b : S
hb : b ∈ I
a : S
hya : a * y ∈ span {y}
⊢ ∃ a_1 b_1, b_1 ∈ I ∧ a_1 * y + b_1 = a * y + b
[PROOFSTEP]
exact ⟨a, b, hb, rfl⟩
[GOAL]
case mpr
α : Type u
β : Type v
inst✝¹ : Semiring α
I✝ : Ideal α
a b : α
S : Type u_1
inst✝ : CommSemiring S
x y : S
I : Ideal S
⊢ (∃ a b, b ∈ I ∧ a * y + b = x) → ∃ y_1, y_1 ∈ span {y} ∧ ∃ z, z ∈ I ∧ y_1 + z = x
[PROOFSTEP]
rintro ⟨a, b, hb, rfl⟩
[GOAL]
case mpr.intro.intro.intro
α : Type u
β : Type v
inst✝¹ : Semiring α
I✝ : Ideal α
a✝ b✝ : α
S : Type u_1
inst✝ : CommSemiring S
y : S
I : Ideal S
a b : S
hb : b ∈ I
⊢ ∃ y_1, y_1 ∈ span {y} ∧ ∃ z, z ∈ I ∧ y_1 + z = a * y + b
[PROOFSTEP]
exact ⟨a * y, Ideal.mem_span_singleton'.mpr ⟨a, rfl⟩, b, hb, rfl⟩
[GOAL]
α : Type u
β : Type v
inst✝ : Semiring α
I✝ : Ideal α
a b : α
I : Ideal α
hI : IsPrime I
r : α
n : ℕ
H : r ^ n ∈ I
⊢ r ∈ I
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
α : Type u
β : Type v
inst✝ : Semiring α
I✝ : Ideal α
a b : α
I : Ideal α
hI : IsPrime I
r : α
n : ℕ
H✝ : r ^ n ∈ I
H : r ^ Nat.zero ∈ I
⊢ r ∈ I
[PROOFSTEP]
rw [pow_zero] at H 
[GOAL]
case zero
α : Type u
β : Type v
inst✝ : Semiring α
I✝ : Ideal α
a b : α
I : Ideal α
hI : IsPrime I
r : α
n : ℕ
H✝ : r ^ n ∈ I
H : 1 ∈ I
⊢ r ∈ I
[PROOFSTEP]
exact (mt (eq_top_iff_one _).2 hI.1).elim H
[GOAL]
case succ
α : Type u
β : Type v
inst✝ : Semiring α
I✝ : Ideal α
a b : α
I : Ideal α
hI : IsPrime I
r : α
n✝ : ℕ
H✝ : r ^ n✝ ∈ I
n : ℕ
ih : r ^ n ∈ I → r ∈ I
H : r ^ Nat.succ n ∈ I
⊢ r ∈ I
[PROOFSTEP]
rw [pow_succ] at H 
[GOAL]
case succ
α : Type u
β : Type v
inst✝ : Semiring α
I✝ : Ideal α
a b : α
I : Ideal α
hI : IsPrime I
r : α
n✝ : ℕ
H✝ : r ^ n✝ ∈ I
n : ℕ
ih : r ^ n ∈ I → r ∈ I
H : r * r ^ n ∈ I
⊢ r ∈ I
[PROOFSTEP]
exact Or.casesOn (hI.mem_or_mem H) id ih
[GOAL]
α : Type u
β : Type v
inst✝ : Semiring α
I✝ : Ideal α
a b : α
I : Ideal α
⊢ ¬IsPrime I ↔ I = ⊤ ∨ ∃ x _hx y _hy, x * y ∈ I
[PROOFSTEP]
simp_rw [Ideal.isPrime_iff, not_and_or, Ne.def, Classical.not_not, not_forall, not_or]
[GOAL]
α : Type u
β : Type v
inst✝ : Semiring α
I✝ : Ideal α
a b : α
I : Ideal α
⊢ (I = ⊤ ∨ ∃ x x_1 h, ¬x ∈ I ∧ ¬x_1 ∈ I) ↔ I = ⊤ ∨ ∃ x _hx y _hy, x * y ∈ I
[PROOFSTEP]
exact or_congr Iff.rfl ⟨fun ⟨x, y, hxy, hx, hy⟩ => ⟨x, hx, y, hy, hxy⟩, fun ⟨x, hx, y, hy, hxy⟩ => ⟨x, y, hxy, hx, hy⟩⟩
[GOAL]
α : Type u
β : Type v
inst✝² : Semiring α
I : Ideal α
a b : α
R : Type u_1
inst✝¹ : Ring R
inst✝ : IsDomain R
h : ⊥ = ⊤
⊢ 1 = 0
[PROOFSTEP]
rwa [Ideal.eq_top_iff_one, Submodule.mem_bot] at h 
[GOAL]
α : Type u
β : Type v
inst✝² : Semiring α
I : Ideal α
a b : α
R : Type u_1
inst✝¹ : Ring R
inst✝ : IsDomain R
x✝ y✝ : R
h : x✝ * y✝ ∈ ⊥
⊢ x✝ * y✝ = 0
[PROOFSTEP]
simpa only [Submodule.mem_bot] using h
[GOAL]
α : Type u
β : Type v
inst✝ : Semiring α
I✝ : Ideal α
a b : α
I J : Ideal α
⊢ I < J → J = ⊤ ↔ ∀ (x : α), I ≤ J → ¬x ∈ I → x ∈ J → 1 ∈ J
[PROOFSTEP]
rw [lt_iff_le_not_le]
[GOAL]
α : Type u
β : Type v
inst✝ : Semiring α
I✝ : Ideal α
a b : α
I J : Ideal α
⊢ I ≤ J ∧ ¬J ≤ I → J = ⊤ ↔ ∀ (x : α), I ≤ J → ¬x ∈ I → x ∈ J → 1 ∈ J
[PROOFSTEP]
exact
  ⟨fun H x h hx₁ hx₂ => J.eq_top_iff_one.1 <| H ⟨h, not_subset.2 ⟨_, hx₂, hx₁⟩⟩, fun H ⟨h₁, h₂⟩ =>
    let ⟨x, xJ, xI⟩ := not_subset.1 h₂
    J.eq_top_iff_one.2 <| H x h₁ xI xJ⟩
[GOAL]
α : Type u
β : Type v
inst✝ : Semiring α
I : Ideal α
a b : α
⊢ IsCoatomic (Ideal α)
[PROOFSTEP]
apply CompleteLattice.coatomic_of_top_compact
[GOAL]
case h
α : Type u
β : Type v
inst✝ : Semiring α
I : Ideal α
a b : α
⊢ CompleteLattice.IsCompactElement ⊤
[PROOFSTEP]
rw [← span_singleton_one]
[GOAL]
case h
α : Type u
β : Type v
inst✝ : Semiring α
I : Ideal α
a b : α
⊢ CompleteLattice.IsCompactElement (span {1})
[PROOFSTEP]
exact Submodule.singleton_span_isCompactElement 1
[GOAL]
α : Type u
β : Type v
inst✝ : Semiring α
I : Ideal α
a b : α
M M' : Ideal α
hM : IsMaximal M
hM' : IsMaximal M'
hne : M ≠ M'
⊢ M ⊔ M' = ⊤
[PROOFSTEP]
contrapose! hne with h
[GOAL]
α : Type u
β : Type v
inst✝ : Semiring α
I : Ideal α
a b : α
M M' : Ideal α
hM : IsMaximal M
hM' : IsMaximal M'
h : M ⊔ M' ≠ ⊤
⊢ M = M'
[PROOFSTEP]
exact hM.eq_of_le hM'.ne_top (le_sup_left.trans_eq (hM'.eq_of_le h le_sup_right).symm)
[GOAL]
α : Type u
β : Type v
inst✝¹ : Semiring α
I : Ideal α
a b : α
inst✝ : Nontrivial α
⊢ Nontrivial (Ideal α)
[PROOFSTEP]
rcases@exists_maximal α _ _ with ⟨M, hM, _⟩
[GOAL]
case intro.mk.intro
α : Type u
β : Type v
inst✝¹ : Semiring α
I : Ideal α
a b : α
inst✝ : Nontrivial α
M : Ideal α
hM : M ≠ ⊤
right✝ : ∀ (b : Ideal α), M < b → b = ⊤
⊢ Nontrivial (Ideal α)
[PROOFSTEP]
exact nontrivial_of_ne M ⊤ hM
[GOAL]
α : Type u
β : Type v
inst✝¹ : Semiring α
I : Ideal α
a b : α
R : Type u
inst✝ : Semiring R
P : Ideal R
hmax : ∀ (m : Ideal R), P < m → ¬IsMaximal m
J : Ideal R
hPJ : P < J
⊢ J = ⊤
[PROOFSTEP]
by_contra hnonmax
[GOAL]
α : Type u
β : Type v
inst✝¹ : Semiring α
I : Ideal α
a b : α
R : Type u
inst✝ : Semiring R
P : Ideal R
hmax : ∀ (m : Ideal R), P < m → ¬IsMaximal m
J : Ideal R
hPJ : P < J
hnonmax : ¬J = ⊤
⊢ False
[PROOFSTEP]
rcases exists_le_maximal J hnonmax with ⟨M, hM1, hM2⟩
[GOAL]
case intro.intro
α : Type u
β : Type v
inst✝¹ : Semiring α
I : Ideal α
a b : α
R : Type u
inst✝ : Semiring R
P : Ideal R
hmax : ∀ (m : Ideal R), P < m → ¬IsMaximal m
J : Ideal R
hPJ : P < J
hnonmax : ¬J = ⊤
M : Ideal R
hM1 : IsMaximal M
hM2 : J ≤ M
⊢ False
[PROOFSTEP]
exact hmax M (lt_of_lt_of_le hPJ hM2) hM1
[GOAL]
α : Type u
β : Type v
inst✝ : Semiring α
I : Ideal α
a b x y : α
⊢ span {x, y} = span {y, x}
[PROOFSTEP]
simp only [span_insert, sup_comm]
[GOAL]
α : Type u
β : Type v
inst✝¹ : Semiring α
I : Ideal α
a b : α
R : Type u
inst✝ : CommRing R
x y z : R
⊢ span {x + y * z, y} = span {x, y}
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u
β : Type v
inst✝¹ : Semiring α
I : Ideal α
a b : α
R : Type u
inst✝ : CommRing R
x y z x✝ : R
⊢ x✝ ∈ span {x + y * z, y} ↔ x✝ ∈ span {x, y}
[PROOFSTEP]
rw [mem_span_pair, mem_span_pair]
[GOAL]
case h
α : Type u
β : Type v
inst✝¹ : Semiring α
I : Ideal α
a b : α
R : Type u
inst✝ : CommRing R
x y z x✝ : R
⊢ (∃ a b, a * (x + y * z) + b * y = x✝) ↔ ∃ a b, a * x + b * y = x✝
[PROOFSTEP]
exact
  ⟨fun ⟨a, b, h⟩ =>
    ⟨a, b + a * z, by
      rw [← h]
      ring1⟩,
    fun ⟨a, b, h⟩ =>
    ⟨a, b - a * z, by
      rw [← h]
      ring1⟩⟩
[GOAL]
α : Type u
β : Type v
inst✝¹ : Semiring α
I : Ideal α
a✝ b✝ : α
R : Type u
inst✝ : CommRing R
x y z x✝¹ : R
x✝ : ∃ a b, a * (x + y * z) + b * y = x✝¹
a b : R
h : a * (x + y * z) + b * y = x✝¹
⊢ a * x + (b + a * z) * y = x✝¹
[PROOFSTEP]
rw [← h]
[GOAL]
α : Type u
β : Type v
inst✝¹ : Semiring α
I : Ideal α
a✝ b✝ : α
R : Type u
inst✝ : CommRing R
x y z x✝¹ : R
x✝ : ∃ a b, a * (x + y * z) + b * y = x✝¹
a b : R
h : a * (x + y * z) + b * y = x✝¹
⊢ a * x + (b + a * z) * y = a * (x + y * z) + b * y
[PROOFSTEP]
ring1
[GOAL]
α : Type u
β : Type v
inst✝¹ : Semiring α
I : Ideal α
a✝ b✝ : α
R : Type u
inst✝ : CommRing R
x y z x✝¹ : R
x✝ : ∃ a b, a * x + b * y = x✝¹
a b : R
h : a * x + b * y = x✝¹
⊢ a * (x + y * z) + (b - a * z) * y = x✝¹
[PROOFSTEP]
rw [← h]
[GOAL]
α : Type u
β : Type v
inst✝¹ : Semiring α
I : Ideal α
a✝ b✝ : α
R : Type u
inst✝ : CommRing R
x y z x✝¹ : R
x✝ : ∃ a b, a * x + b * y = x✝¹
a b : R
h : a * x + b * y = x✝¹
⊢ a * (x + y * z) + (b - a * z) * y = a * x + b * y
[PROOFSTEP]
ring1
[GOAL]
α : Type u
β : Type v
inst✝¹ : Semiring α
I : Ideal α
a b : α
R : Type u
inst✝ : CommRing R
x y z : R
⊢ span {x, y + x * z} = span {x, y}
[PROOFSTEP]
rw [span_pair_comm, span_pair_add_mul_left, span_pair_comm]
[GOAL]
α : Type u
β : Type v
inst✝ : Semiring α
I✝ : Ideal α
a b : α
I : Ideal α
hI : IsMaximal I
x : α
hx : ¬x ∈ I
⊢ ∃ y i, i ∈ I ∧ y * x + i = 1
[PROOFSTEP]
cases' isMaximal_iff.1 hI with H₁ H₂
[GOAL]
case intro
α : Type u
β : Type v
inst✝ : Semiring α
I✝ : Ideal α
a b : α
I : Ideal α
hI : IsMaximal I
x : α
hx : ¬x ∈ I
H₁ : ¬1 ∈ I
H₂ : ∀ (J : Ideal α) (x : α), I ≤ J → ¬x ∈ I → x ∈ J → 1 ∈ J
⊢ ∃ y i, i ∈ I ∧ y * x + i = 1
[PROOFSTEP]
rcases mem_span_insert.1
    (H₂ (span (insert x I)) x (Set.Subset.trans (subset_insert _ _) subset_span) hx (subset_span (mem_insert _ _))) with
  ⟨y, z, hz, hy⟩
[GOAL]
case intro.intro.intro.intro
α : Type u
β : Type v
inst✝ : Semiring α
I✝ : Ideal α
a b : α
I : Ideal α
hI : IsMaximal I
x : α
hx : ¬x ∈ I
H₁ : ¬1 ∈ I
H₂ : ∀ (J : Ideal α) (x : α), I ≤ J → ¬x ∈ I → x ∈ J → 1 ∈ J
y z : α
hz : z ∈ span ↑I
hy : 1 = y * x + z
⊢ ∃ y i, i ∈ I ∧ y * x + i = 1
[PROOFSTEP]
refine' ⟨y, z, _, hy.symm⟩
[GOAL]
case intro.intro.intro.intro
α : Type u
β : Type v
inst✝ : Semiring α
I✝ : Ideal α
a b : α
I : Ideal α
hI : IsMaximal I
x : α
hx : ¬x ∈ I
H₁ : ¬1 ∈ I
H₂ : ∀ (J : Ideal α) (x : α), I ≤ J → ¬x ∈ I → x ∈ J → 1 ∈ J
y z : α
hz : z ∈ span ↑I
hy : 1 = y * x + z
⊢ z ∈ I
[PROOFSTEP]
rwa [← span_eq I]
[GOAL]
α : Type u
β : Type v
inst✝ : Semiring α
I : Ideal α
a b : α
s : Set (Ideal α)
hs : Set.Nonempty s
hs' : IsChain (fun x x_1 => x ≤ x_1) s
H : ∀ (p : Ideal α), p ∈ s → IsPrime p
x✝ y✝ : α
e : x✝ * y✝ ∈ sInf s
hx : ¬x✝ ∈ sInf s
⊢ y✝ ∈ sInf s
[PROOFSTEP]
rw [Ideal.mem_sInf] at hx e ⊢
[GOAL]
α : Type u
β : Type v
inst✝ : Semiring α
I : Ideal α
a b : α
s : Set (Ideal α)
hs : Set.Nonempty s
hs' : IsChain (fun x x_1 => x ≤ x_1) s
H : ∀ (p : Ideal α), p ∈ s → IsPrime p
x✝ y✝ : α
e : ∀ ⦃I : Ideal α⦄, I ∈ s → x✝ * y✝ ∈ I
hx : ¬∀ ⦃I : Ideal α⦄, I ∈ s → x✝ ∈ I
⊢ ∀ ⦃I : Ideal α⦄, I ∈ s → y✝ ∈ I
[PROOFSTEP]
push_neg at hx 
[GOAL]
α : Type u
β : Type v
inst✝ : Semiring α
I : Ideal α
a b : α
s : Set (Ideal α)
hs : Set.Nonempty s
hs' : IsChain (fun x x_1 => x ≤ x_1) s
H : ∀ (p : Ideal α), p ∈ s → IsPrime p
x✝ y✝ : α
e : ∀ ⦃I : Ideal α⦄, I ∈ s → x✝ * y✝ ∈ I
hx : Exists fun ⦃I⦄ => I ∈ s ∧ ¬x✝ ∈ I
⊢ ∀ ⦃I : Ideal α⦄, I ∈ s → y✝ ∈ I
[PROOFSTEP]
obtain ⟨I, hI, hI'⟩ := hx
[GOAL]
case intro.intro
α : Type u
β : Type v
inst✝ : Semiring α
I✝ : Ideal α
a b : α
s : Set (Ideal α)
hs : Set.Nonempty s
hs' : IsChain (fun x x_1 => x ≤ x_1) s
H : ∀ (p : Ideal α), p ∈ s → IsPrime p
x✝ y✝ : α
e : ∀ ⦃I : Ideal α⦄, I ∈ s → x✝ * y✝ ∈ I
I : Ideal α
hI : I ∈ s
hI' : ¬x✝ ∈ I
⊢ ∀ ⦃I : Ideal α⦄, I ∈ s → y✝ ∈ I
[PROOFSTEP]
intro J hJ
[GOAL]
case intro.intro
α : Type u
β : Type v
inst✝ : Semiring α
I✝ : Ideal α
a b : α
s : Set (Ideal α)
hs : Set.Nonempty s
hs' : IsChain (fun x x_1 => x ≤ x_1) s
H : ∀ (p : Ideal α), p ∈ s → IsPrime p
x✝ y✝ : α
e : ∀ ⦃I : Ideal α⦄, I ∈ s → x✝ * y✝ ∈ I
I : Ideal α
hI : I ∈ s
hI' : ¬x✝ ∈ I
J : Ideal α
hJ : J ∈ s
⊢ y✝ ∈ J
[PROOFSTEP]
cases' hs'.total hI hJ with h h
[GOAL]
case intro.intro.inl
α : Type u
β : Type v
inst✝ : Semiring α
I✝ : Ideal α
a b : α
s : Set (Ideal α)
hs : Set.Nonempty s
hs' : IsChain (fun x x_1 => x ≤ x_1) s
H : ∀ (p : Ideal α), p ∈ s → IsPrime p
x✝ y✝ : α
e : ∀ ⦃I : Ideal α⦄, I ∈ s → x✝ * y✝ ∈ I
I : Ideal α
hI : I ∈ s
hI' : ¬x✝ ∈ I
J : Ideal α
hJ : J ∈ s
h : I ≤ J
⊢ y✝ ∈ J
[PROOFSTEP]
exact h (((H I hI).mem_or_mem (e hI)).resolve_left hI')
[GOAL]
case intro.intro.inr
α : Type u
β : Type v
inst✝ : Semiring α
I✝ : Ideal α
a b : α
s : Set (Ideal α)
hs : Set.Nonempty s
hs' : IsChain (fun x x_1 => x ≤ x_1) s
H : ∀ (p : Ideal α), p ∈ s → IsPrime p
x✝ y✝ : α
e : ∀ ⦃I : Ideal α⦄, I ∈ s → x✝ * y✝ ∈ I
I : Ideal α
hI : I ∈ s
hI' : ¬x✝ ∈ I
J : Ideal α
hJ : J ∈ s
h : J ≤ I
⊢ y✝ ∈ J
[PROOFSTEP]
exact ((H J hJ).mem_or_mem (e hJ)).resolve_left fun x => hI' <| h x
[GOAL]
α : Type u
β : Type v
a b : α
inst✝ : CommSemiring α
I : Ideal α
x y x✝ : α
⊢ x✝ * y = x ↔ x = y * x✝
[PROOFSTEP]
rw [eq_comm, mul_comm]
[GOAL]
α✝ : Type u
β : Type v
a b : α✝
inst✝² : CommSemiring α✝
I : Ideal α✝
α : Type u
inst✝¹ : CommRing α
inst✝ : IsDomain α
x y : α
⊢ span {x} = span {y} ↔ Associated x y
[PROOFSTEP]
rw [← dvd_dvd_iff_associated, le_antisymm_iff, and_comm]
[GOAL]
α✝ : Type u
β : Type v
a b : α✝
inst✝² : CommSemiring α✝
I : Ideal α✝
α : Type u
inst✝¹ : CommRing α
inst✝ : IsDomain α
x y : α
⊢ span {y} ≤ span {x} ∧ span {x} ≤ span {y} ↔ x ∣ y ∧ y ∣ x
[PROOFSTEP]
apply and_congr
[GOAL]
case h₁
α✝ : Type u
β : Type v
a b : α✝
inst✝² : CommSemiring α✝
I : Ideal α✝
α : Type u
inst✝¹ : CommRing α
inst✝ : IsDomain α
x y : α
⊢ span {y} ≤ span {x} ↔ x ∣ y
[PROOFSTEP]
rw [span_singleton_le_span_singleton]
[GOAL]
case h₂
α✝ : Type u
β : Type v
a b : α✝
inst✝² : CommSemiring α✝
I : Ideal α✝
α : Type u
inst✝¹ : CommRing α
inst✝ : IsDomain α
x y : α
⊢ span {x} ≤ span {y} ↔ y ∣ x
[PROOFSTEP]
rw [span_singleton_le_span_singleton]
[GOAL]
α : Type u
β : Type v
a✝ b : α
inst✝ : CommSemiring α
I : Ideal α
a : α
h2 : IsUnit a
x : α
⊢ span {x * a} = span {x}
[PROOFSTEP]
rw [mul_comm, span_singleton_mul_left_unit h2]
[GOAL]
α : Type u
β : Type v
a b : α
inst✝ : CommSemiring α
I : Ideal α
x : α
⊢ span {x} = ⊤ ↔ IsUnit x
[PROOFSTEP]
rw [isUnit_iff_dvd_one, ← span_singleton_le_span_singleton, span_singleton_one, eq_top_iff]
[GOAL]
α : Type u
β : Type v
a b : α
inst✝ : CommSemiring α
I : Ideal α
p : α
hp : p ≠ 0
⊢ IsPrime (span {p}) ↔ Prime p
[PROOFSTEP]
simp [isPrime_iff, Prime, span_singleton_eq_top, hp, mem_span_singleton]
[GOAL]
α : Type u
β : Type v
a b : α
inst✝ : CommSemiring α
I✝ I : Ideal α
H : IsMaximal I
x y : α
hxy : x * y ∈ I
hx : ¬x ∈ I
⊢ y ∈ I
[PROOFSTEP]
let J : Ideal α := Submodule.span α (insert x ↑I)
[GOAL]
α : Type u
β : Type v
a b : α
inst✝ : CommSemiring α
I✝ I : Ideal α
H : IsMaximal I
x y : α
hxy : x * y ∈ I
hx : ¬x ∈ I
J : Ideal α := Submodule.span α (insert x ↑I)
⊢ y ∈ I
[PROOFSTEP]
have IJ : I ≤ J := Set.Subset.trans (subset_insert _ _) subset_span
[GOAL]
α : Type u
β : Type v
a b : α
inst✝ : CommSemiring α
I✝ I : Ideal α
H : IsMaximal I
x y : α
hxy : x * y ∈ I
hx : ¬x ∈ I
J : Ideal α := Submodule.span α (insert x ↑I)
IJ : I ≤ J
⊢ y ∈ I
[PROOFSTEP]
have xJ : x ∈ J := Ideal.subset_span (Set.mem_insert x I)
[GOAL]
α : Type u
β : Type v
a b : α
inst✝ : CommSemiring α
I✝ I : Ideal α
H : IsMaximal I
x y : α
hxy : x * y ∈ I
hx : ¬x ∈ I
J : Ideal α := Submodule.span α (insert x ↑I)
IJ : I ≤ J
xJ : x ∈ J
⊢ y ∈ I
[PROOFSTEP]
cases' isMaximal_iff.1 H with _ oJ
[GOAL]
case intro
α : Type u
β : Type v
a b : α
inst✝ : CommSemiring α
I✝ I : Ideal α
H : IsMaximal I
x y : α
hxy : x * y ∈ I
hx : ¬x ∈ I
J : Ideal α := Submodule.span α (insert x ↑I)
IJ : I ≤ J
xJ : x ∈ J
left✝ : ¬1 ∈ I
oJ : ∀ (J : Ideal α) (x : α), I ≤ J → ¬x ∈ I → x ∈ J → 1 ∈ J
⊢ y ∈ I
[PROOFSTEP]
specialize oJ J x IJ hx xJ
[GOAL]
case intro
α : Type u
β : Type v
a b : α
inst✝ : CommSemiring α
I✝ I : Ideal α
H : IsMaximal I
x y : α
hxy : x * y ∈ I
hx : ¬x ∈ I
J : Ideal α := Submodule.span α (insert x ↑I)
IJ : I ≤ J
xJ : x ∈ J
left✝ : ¬1 ∈ I
oJ : 1 ∈ J
⊢ y ∈ I
[PROOFSTEP]
rcases Submodule.mem_span_insert.mp oJ with ⟨a, b, h, oe⟩
[GOAL]
case intro.intro.intro.intro
α : Type u
β : Type v
a✝ b✝ : α
inst✝ : CommSemiring α
I✝ I : Ideal α
H : IsMaximal I
x y : α
hxy : x * y ∈ I
hx : ¬x ∈ I
J : Ideal α := Submodule.span α (insert x ↑I)
IJ : I ≤ J
xJ : x ∈ J
left✝ : ¬1 ∈ I
oJ : 1 ∈ J
a b : α
h : b ∈ Submodule.span α ↑I
oe : 1 = a • x + b
⊢ y ∈ I
[PROOFSTEP]
obtain F : y * 1 = y * (a • x + b) := congr_arg (fun g : α => y * g) oe
[GOAL]
case intro.intro.intro.intro
α : Type u
β : Type v
a✝ b✝ : α
inst✝ : CommSemiring α
I✝ I : Ideal α
H : IsMaximal I
x y : α
hxy : x * y ∈ I
hx : ¬x ∈ I
J : Ideal α := Submodule.span α (insert x ↑I)
IJ : I ≤ J
xJ : x ∈ J
left✝ : ¬1 ∈ I
oJ : 1 ∈ J
a b : α
h : b ∈ Submodule.span α ↑I
oe : 1 = a • x + b
F : y * 1 = y * (a • x + b)
⊢ y ∈ I
[PROOFSTEP]
rw [← mul_one y, F, mul_add, mul_comm, smul_eq_mul, mul_assoc]
[GOAL]
case intro.intro.intro.intro
α : Type u
β : Type v
a✝ b✝ : α
inst✝ : CommSemiring α
I✝ I : Ideal α
H : IsMaximal I
x y : α
hxy : x * y ∈ I
hx : ¬x ∈ I
J : Ideal α := Submodule.span α (insert x ↑I)
IJ : I ≤ J
xJ : x ∈ J
left✝ : ¬1 ∈ I
oJ : 1 ∈ J
a b : α
h : b ∈ Submodule.span α ↑I
oe : 1 = a • x + b
F : y * 1 = y * (a • x + b)
⊢ a * (x * y) + y * b ∈ I
[PROOFSTEP]
refine' Submodule.add_mem I (I.mul_mem_left a hxy) (Submodule.smul_mem I y _)
[GOAL]
case intro.intro.intro.intro
α : Type u
β : Type v
a✝ b✝ : α
inst✝ : CommSemiring α
I✝ I : Ideal α
H : IsMaximal I
x y : α
hxy : x * y ∈ I
hx : ¬x ∈ I
J : Ideal α := Submodule.span α (insert x ↑I)
IJ : I ≤ J
xJ : x ∈ J
left✝ : ¬1 ∈ I
oJ : 1 ∈ J
a b : α
h : b ∈ Submodule.span α ↑I
oe : 1 = a • x + b
F : y * 1 = y * (a • x + b)
⊢ b ∈ I
[PROOFSTEP]
rwa [Submodule.span_eq] at h 
[GOAL]
α : Type u
β : Type v
a b : α
inst✝² : CommSemiring α
I : Ideal α
inst✝¹ : CommRing β
inst✝ : IsDomain β
x y : β
⊢ span {x} < span {y} ↔ DvdNotUnit y x
[PROOFSTEP]
rw [lt_iff_le_not_le, span_singleton_le_span_singleton, span_singleton_le_span_singleton, dvd_and_not_dvd_iff]
[GOAL]
α : Type u
β : Type v
a b : α
inst✝² : CommSemiring α
I : Ideal α
inst✝¹ : CommRing β
inst✝ : IsDomain β
b₁ b₂ : β
h₁ : b₁ ≠ 0
h₂ : ¬IsUnit b₂
h : span {b₁} ≤ span {b₁ * b₂}
⊢ b₁ * b₂ ∣ b₁ * 1
[PROOFSTEP]
rwa [mul_one, ← Ideal.span_singleton_le_span_singleton]
[GOAL]
α : Type u
β : Type v
a b : α
inst✝ : CommSemiring α
I : Ideal α
ha : a ∈ I
n : ℕ
hn : 0 < n
⊢ ¬0 < Nat.zero
[PROOFSTEP]
decide
[GOAL]
α : Type u
β : Type v
a b : α
inst✝ : CommSemiring α
I✝ I : Ideal α
hI : IsPrime I
x y : α
⊢ x ∈ I ∨ y ∈ I → x * y ∈ I
[PROOFSTEP]
rintro (h | h)
[GOAL]
case inl
α : Type u
β : Type v
a b : α
inst✝ : CommSemiring α
I✝ I : Ideal α
hI : IsPrime I
x y : α
h : x ∈ I
⊢ x * y ∈ I
case inr
α : Type u
β : Type v
a b : α
inst✝ : CommSemiring α
I✝ I : Ideal α
hI : IsPrime I
x y : α
h : y ∈ I
⊢ x * y ∈ I
[PROOFSTEP]
exacts [I.mul_mem_right y h, I.mul_mem_left x h]
[GOAL]
α : Type u
β : Type v
a b : α
inst✝¹ : CommSemiring α
I : Ideal α
inst✝ : DecidableEq α
s : Multiset α
n : ℕ
⊢ Multiset.sum s ^ (↑Multiset.card s * n + 1) ∈ span ↑(Multiset.toFinset (Multiset.map (fun x => x ^ (n + 1)) s))
[PROOFSTEP]
induction' s using Multiset.induction_on with a s hs
[GOAL]
case empty
α : Type u
β : Type v
a b : α
inst✝¹ : CommSemiring α
I : Ideal α
inst✝ : DecidableEq α
n : ℕ
⊢ Multiset.sum 0 ^ (↑Multiset.card 0 * n + 1) ∈ span ↑(Multiset.toFinset (Multiset.map (fun x => x ^ (n + 1)) 0))
[PROOFSTEP]
simp
[GOAL]
case cons
α : Type u
β : Type v
a✝ b : α
inst✝¹ : CommSemiring α
I : Ideal α
inst✝ : DecidableEq α
n : ℕ
a : α
s : Multiset α
hs : Multiset.sum s ^ (↑Multiset.card s * n + 1) ∈ span ↑(Multiset.toFinset (Multiset.map (fun x => x ^ (n + 1)) s))
⊢ Multiset.sum (a ::ₘ s) ^ (↑Multiset.card (a ::ₘ s) * n + 1) ∈
    span ↑(Multiset.toFinset (Multiset.map (fun x => x ^ (n + 1)) (a ::ₘ s)))
[PROOFSTEP]
simp only [Finset.coe_insert, Multiset.map_cons, Multiset.toFinset_cons, Multiset.sum_cons, Multiset.card_cons, add_pow]
[GOAL]
case cons
α : Type u
β : Type v
a✝ b : α
inst✝¹ : CommSemiring α
I : Ideal α
inst✝ : DecidableEq α
n : ℕ
a : α
s : Multiset α
hs : Multiset.sum s ^ (↑Multiset.card s * n + 1) ∈ span ↑(Multiset.toFinset (Multiset.map (fun x => x ^ (n + 1)) s))
⊢ ∑ m in Finset.range ((↑Multiset.card s + 1) * n + 1 + 1),
      a ^ m * Multiset.sum s ^ ((↑Multiset.card s + 1) * n + 1 - m) * ↑(Nat.choose ((↑Multiset.card s + 1) * n + 1) m) ∈
    span (insert (a ^ (n + 1)) ↑(Multiset.toFinset (Multiset.map (fun x => x ^ (n + 1)) s)))
[PROOFSTEP]
refine' Submodule.sum_mem _ _
[GOAL]
case cons
α : Type u
β : Type v
a✝ b : α
inst✝¹ : CommSemiring α
I : Ideal α
inst✝ : DecidableEq α
n : ℕ
a : α
s : Multiset α
hs : Multiset.sum s ^ (↑Multiset.card s * n + 1) ∈ span ↑(Multiset.toFinset (Multiset.map (fun x => x ^ (n + 1)) s))
⊢ ∀ (c : ℕ),
    c ∈ Finset.range ((↑Multiset.card s + 1) * n + 1 + 1) →
      a ^ c * Multiset.sum s ^ ((↑Multiset.card s + 1) * n + 1 - c) * ↑(Nat.choose ((↑Multiset.card s + 1) * n + 1) c) ∈
        span (insert (a ^ (n + 1)) ↑(Multiset.toFinset (Multiset.map (fun x => x ^ (n + 1)) s)))
[PROOFSTEP]
intro c _hc
[GOAL]
case cons
α : Type u
β : Type v
a✝ b : α
inst✝¹ : CommSemiring α
I : Ideal α
inst✝ : DecidableEq α
n : ℕ
a : α
s : Multiset α
hs : Multiset.sum s ^ (↑Multiset.card s * n + 1) ∈ span ↑(Multiset.toFinset (Multiset.map (fun x => x ^ (n + 1)) s))
c : ℕ
_hc : c ∈ Finset.range ((↑Multiset.card s + 1) * n + 1 + 1)
⊢ a ^ c * Multiset.sum s ^ ((↑Multiset.card s + 1) * n + 1 - c) * ↑(Nat.choose ((↑Multiset.card s + 1) * n + 1) c) ∈
    span (insert (a ^ (n + 1)) ↑(Multiset.toFinset (Multiset.map (fun x => x ^ (n + 1)) s)))
[PROOFSTEP]
rw [mem_span_insert]
[GOAL]
case cons
α : Type u
β : Type v
a✝ b : α
inst✝¹ : CommSemiring α
I : Ideal α
inst✝ : DecidableEq α
n : ℕ
a : α
s : Multiset α
hs : Multiset.sum s ^ (↑Multiset.card s * n + 1) ∈ span ↑(Multiset.toFinset (Multiset.map (fun x => x ^ (n + 1)) s))
c : ℕ
_hc : c ∈ Finset.range ((↑Multiset.card s + 1) * n + 1 + 1)
⊢ ∃ a_1 z,
    z ∈ span ↑(Multiset.toFinset (Multiset.map (fun x => x ^ (n + 1)) s)) ∧
      a ^ c * Multiset.sum s ^ ((↑Multiset.card s + 1) * n + 1 - c) * ↑(Nat.choose ((↑Multiset.card s + 1) * n + 1) c) =
        a_1 * a ^ (n + 1) + z
[PROOFSTEP]
by_cases h : n + 1 ≤ c
[GOAL]
case pos
α : Type u
β : Type v
a✝ b : α
inst✝¹ : CommSemiring α
I : Ideal α
inst✝ : DecidableEq α
n : ℕ
a : α
s : Multiset α
hs : Multiset.sum s ^ (↑Multiset.card s * n + 1) ∈ span ↑(Multiset.toFinset (Multiset.map (fun x => x ^ (n + 1)) s))
c : ℕ
_hc : c ∈ Finset.range ((↑Multiset.card s + 1) * n + 1 + 1)
h : n + 1 ≤ c
⊢ ∃ a_1 z,
    z ∈ span ↑(Multiset.toFinset (Multiset.map (fun x => x ^ (n + 1)) s)) ∧
      a ^ c * Multiset.sum s ^ ((↑Multiset.card s + 1) * n + 1 - c) * ↑(Nat.choose ((↑Multiset.card s + 1) * n + 1) c) =
        a_1 * a ^ (n + 1) + z
[PROOFSTEP]
refine'
  ⟨a ^ (c - (n + 1)) * s.sum ^ ((Multiset.card s + 1) * n + 1 - c) * ((Multiset.card s + 1) * n + 1).choose c, 0,
    Submodule.zero_mem _, _⟩
[GOAL]
case pos
α : Type u
β : Type v
a✝ b : α
inst✝¹ : CommSemiring α
I : Ideal α
inst✝ : DecidableEq α
n : ℕ
a : α
s : Multiset α
hs : Multiset.sum s ^ (↑Multiset.card s * n + 1) ∈ span ↑(Multiset.toFinset (Multiset.map (fun x => x ^ (n + 1)) s))
c : ℕ
_hc : c ∈ Finset.range ((↑Multiset.card s + 1) * n + 1 + 1)
h : n + 1 ≤ c
⊢ a ^ c * Multiset.sum s ^ ((↑Multiset.card s + 1) * n + 1 - c) * ↑(Nat.choose ((↑Multiset.card s + 1) * n + 1) c) =
    a ^ (c - (n + 1)) * Multiset.sum s ^ ((↑Multiset.card s + 1) * n + 1 - c) *
          ↑(Nat.choose ((↑Multiset.card s + 1) * n + 1) c) *
        a ^ (n + 1) +
      0
[PROOFSTEP]
rw [mul_comm _ (a ^ (n + 1))]
[GOAL]
case pos
α : Type u
β : Type v
a✝ b : α
inst✝¹ : CommSemiring α
I : Ideal α
inst✝ : DecidableEq α
n : ℕ
a : α
s : Multiset α
hs : Multiset.sum s ^ (↑Multiset.card s * n + 1) ∈ span ↑(Multiset.toFinset (Multiset.map (fun x => x ^ (n + 1)) s))
c : ℕ
_hc : c ∈ Finset.range ((↑Multiset.card s + 1) * n + 1 + 1)
h : n + 1 ≤ c
⊢ a ^ c * Multiset.sum s ^ ((↑Multiset.card s + 1) * n + 1 - c) * ↑(Nat.choose ((↑Multiset.card s + 1) * n + 1) c) =
    a ^ (n + 1) *
        (a ^ (c - (n + 1)) * Multiset.sum s ^ ((↑Multiset.card s + 1) * n + 1 - c) *
          ↑(Nat.choose ((↑Multiset.card s + 1) * n + 1) c)) +
      0
[PROOFSTEP]
simp_rw [← mul_assoc]
[GOAL]
case pos
α : Type u
β : Type v
a✝ b : α
inst✝¹ : CommSemiring α
I : Ideal α
inst✝ : DecidableEq α
n : ℕ
a : α
s : Multiset α
hs : Multiset.sum s ^ (↑Multiset.card s * n + 1) ∈ span ↑(Multiset.toFinset (Multiset.map (fun x => x ^ (n + 1)) s))
c : ℕ
_hc : c ∈ Finset.range ((↑Multiset.card s + 1) * n + 1 + 1)
h : n + 1 ≤ c
⊢ a ^ c * Multiset.sum s ^ ((↑Multiset.card s + 1) * n + 1 - c) * ↑(Nat.choose ((↑Multiset.card s + 1) * n + 1) c) =
    a ^ (n + 1) * a ^ (c - (n + 1)) * Multiset.sum s ^ ((↑Multiset.card s + 1) * n + 1 - c) *
        ↑(Nat.choose ((↑Multiset.card s + 1) * n + 1) c) +
      0
[PROOFSTEP]
rw [← pow_add, add_zero, add_tsub_cancel_of_le h]
[GOAL]
case neg
α : Type u
β : Type v
a✝ b : α
inst✝¹ : CommSemiring α
I : Ideal α
inst✝ : DecidableEq α
n : ℕ
a : α
s : Multiset α
hs : Multiset.sum s ^ (↑Multiset.card s * n + 1) ∈ span ↑(Multiset.toFinset (Multiset.map (fun x => x ^ (n + 1)) s))
c : ℕ
_hc : c ∈ Finset.range ((↑Multiset.card s + 1) * n + 1 + 1)
h : ¬n + 1 ≤ c
⊢ ∃ a_1 z,
    z ∈ span ↑(Multiset.toFinset (Multiset.map (fun x => x ^ (n + 1)) s)) ∧
      a ^ c * Multiset.sum s ^ ((↑Multiset.card s + 1) * n + 1 - c) * ↑(Nat.choose ((↑Multiset.card s + 1) * n + 1) c) =
        a_1 * a ^ (n + 1) + z
[PROOFSTEP]
use 0
[GOAL]
case h
α : Type u
β : Type v
a✝ b : α
inst✝¹ : CommSemiring α
I : Ideal α
inst✝ : DecidableEq α
n : ℕ
a : α
s : Multiset α
hs : Multiset.sum s ^ (↑Multiset.card s * n + 1) ∈ span ↑(Multiset.toFinset (Multiset.map (fun x => x ^ (n + 1)) s))
c : ℕ
_hc : c ∈ Finset.range ((↑Multiset.card s + 1) * n + 1 + 1)
h : ¬n + 1 ≤ c
⊢ ∃ z,
    z ∈ span ↑(Multiset.toFinset (Multiset.map (fun x => x ^ (n + 1)) s)) ∧
      a ^ c * Multiset.sum s ^ ((↑Multiset.card s + 1) * n + 1 - c) * ↑(Nat.choose ((↑Multiset.card s + 1) * n + 1) c) =
        0 * a ^ (n + 1) + z
[PROOFSTEP]
simp_rw [zero_mul, zero_add]
[GOAL]
case h
α : Type u
β : Type v
a✝ b : α
inst✝¹ : CommSemiring α
I : Ideal α
inst✝ : DecidableEq α
n : ℕ
a : α
s : Multiset α
hs : Multiset.sum s ^ (↑Multiset.card s * n + 1) ∈ span ↑(Multiset.toFinset (Multiset.map (fun x => x ^ (n + 1)) s))
c : ℕ
_hc : c ∈ Finset.range ((↑Multiset.card s + 1) * n + 1 + 1)
h : ¬n + 1 ≤ c
⊢ ∃ z,
    z ∈ span ↑(Multiset.toFinset (Multiset.map (fun x => x ^ (n + 1)) s)) ∧
      a ^ c * Multiset.sum s ^ ((↑Multiset.card s + 1) * n + 1 - c) * ↑(Nat.choose ((↑Multiset.card s + 1) * n + 1) c) =
        z
[PROOFSTEP]
refine' ⟨_, _, rfl⟩
[GOAL]
case h
α : Type u
β : Type v
a✝ b : α
inst✝¹ : CommSemiring α
I : Ideal α
inst✝ : DecidableEq α
n : ℕ
a : α
s : Multiset α
hs : Multiset.sum s ^ (↑Multiset.card s * n + 1) ∈ span ↑(Multiset.toFinset (Multiset.map (fun x => x ^ (n + 1)) s))
c : ℕ
_hc : c ∈ Finset.range ((↑Multiset.card s + 1) * n + 1 + 1)
h : ¬n + 1 ≤ c
⊢ a ^ c * Multiset.sum s ^ ((↑Multiset.card s + 1) * n + 1 - c) * ↑(Nat.choose ((↑Multiset.card s + 1) * n + 1) c) ∈
    span ↑(Multiset.toFinset (Multiset.map (fun x => x ^ (n + 1)) s))
[PROOFSTEP]
replace h : c ≤ n := Nat.lt_succ_iff.mp (not_le.mp h)
[GOAL]
case h
α : Type u
β : Type v
a✝ b : α
inst✝¹ : CommSemiring α
I : Ideal α
inst✝ : DecidableEq α
n : ℕ
a : α
s : Multiset α
hs : Multiset.sum s ^ (↑Multiset.card s * n + 1) ∈ span ↑(Multiset.toFinset (Multiset.map (fun x => x ^ (n + 1)) s))
c : ℕ
_hc : c ∈ Finset.range ((↑Multiset.card s + 1) * n + 1 + 1)
h : c ≤ n
⊢ a ^ c * Multiset.sum s ^ ((↑Multiset.card s + 1) * n + 1 - c) * ↑(Nat.choose ((↑Multiset.card s + 1) * n + 1) c) ∈
    span ↑(Multiset.toFinset (Multiset.map (fun x => x ^ (n + 1)) s))
[PROOFSTEP]
have : (Multiset.card s + 1) * n + 1 - c = Multiset.card s * n + 1 + (n - c) := by
  rw [add_mul, one_mul, add_assoc, add_comm n 1, ← add_assoc, add_tsub_assoc_of_le h]
[GOAL]
α : Type u
β : Type v
a✝ b : α
inst✝¹ : CommSemiring α
I : Ideal α
inst✝ : DecidableEq α
n : ℕ
a : α
s : Multiset α
hs : Multiset.sum s ^ (↑Multiset.card s * n + 1) ∈ span ↑(Multiset.toFinset (Multiset.map (fun x => x ^ (n + 1)) s))
c : ℕ
_hc : c ∈ Finset.range ((↑Multiset.card s + 1) * n + 1 + 1)
h : c ≤ n
⊢ (↑Multiset.card s + 1) * n + 1 - c = ↑Multiset.card s * n + 1 + (n - c)
[PROOFSTEP]
rw [add_mul, one_mul, add_assoc, add_comm n 1, ← add_assoc, add_tsub_assoc_of_le h]
[GOAL]
case h
α : Type u
β : Type v
a✝ b : α
inst✝¹ : CommSemiring α
I : Ideal α
inst✝ : DecidableEq α
n : ℕ
a : α
s : Multiset α
hs : Multiset.sum s ^ (↑Multiset.card s * n + 1) ∈ span ↑(Multiset.toFinset (Multiset.map (fun x => x ^ (n + 1)) s))
c : ℕ
_hc : c ∈ Finset.range ((↑Multiset.card s + 1) * n + 1 + 1)
h : c ≤ n
this : (↑Multiset.card s + 1) * n + 1 - c = ↑Multiset.card s * n + 1 + (n - c)
⊢ a ^ c * Multiset.sum s ^ ((↑Multiset.card s + 1) * n + 1 - c) * ↑(Nat.choose ((↑Multiset.card s + 1) * n + 1) c) ∈
    span ↑(Multiset.toFinset (Multiset.map (fun x => x ^ (n + 1)) s))
[PROOFSTEP]
rw [this, pow_add]
[GOAL]
case h
α : Type u
β : Type v
a✝ b : α
inst✝¹ : CommSemiring α
I : Ideal α
inst✝ : DecidableEq α
n : ℕ
a : α
s : Multiset α
hs : Multiset.sum s ^ (↑Multiset.card s * n + 1) ∈ span ↑(Multiset.toFinset (Multiset.map (fun x => x ^ (n + 1)) s))
c : ℕ
_hc : c ∈ Finset.range ((↑Multiset.card s + 1) * n + 1 + 1)
h : c ≤ n
this : (↑Multiset.card s + 1) * n + 1 - c = ↑Multiset.card s * n + 1 + (n - c)
⊢ a ^ c * (Multiset.sum s ^ (↑Multiset.card s * n + 1) * Multiset.sum s ^ (n - c)) *
      ↑(Nat.choose ((↑Multiset.card s + 1) * n + 1) c) ∈
    span ↑(Multiset.toFinset (Multiset.map (fun x => x ^ (n + 1)) s))
[PROOFSTEP]
simp_rw [mul_assoc, mul_comm (s.sum ^ (Multiset.card s * n + 1)), ← mul_assoc]
[GOAL]
case h
α : Type u
β : Type v
a✝ b : α
inst✝¹ : CommSemiring α
I : Ideal α
inst✝ : DecidableEq α
n : ℕ
a : α
s : Multiset α
hs : Multiset.sum s ^ (↑Multiset.card s * n + 1) ∈ span ↑(Multiset.toFinset (Multiset.map (fun x => x ^ (n + 1)) s))
c : ℕ
_hc : c ∈ Finset.range ((↑Multiset.card s + 1) * n + 1 + 1)
h : c ≤ n
this : (↑Multiset.card s + 1) * n + 1 - c = ↑Multiset.card s * n + 1 + (n - c)
⊢ a ^ c * Multiset.sum s ^ (n - c) * ↑(Nat.choose ((↑Multiset.card s + 1) * n + 1) c) *
      Multiset.sum s ^ (↑Multiset.card s * n + 1) ∈
    span ↑(Multiset.toFinset (Multiset.map (fun x => x ^ (n + 1)) s))
[PROOFSTEP]
exact mul_mem_left _ _ hs
[GOAL]
α : Type u
β : Type v
a b : α
inst✝ : CommSemiring α
I : Ideal α
ι : Type u_1
s : Finset ι
f : ι → α
n : ℕ
⊢ (∑ i in s, f i) ^ (Finset.card s * n + 1) ∈ span ((fun i => f i ^ (n + 1)) '' ↑s)
[PROOFSTEP]
classical simpa only [Multiset.card_map, Multiset.map_map, comp_apply, Multiset.toFinset_map, Finset.coe_image,
  Finset.val_toFinset] using pow_multiset_sum_mem_span_pow (s.1.map f) n
[GOAL]
α : Type u
β : Type v
a b : α
inst✝ : CommSemiring α
I : Ideal α
ι : Type u_1
s : Finset ι
f : ι → α
n : ℕ
⊢ (∑ i in s, f i) ^ (Finset.card s * n + 1) ∈ span ((fun i => f i ^ (n + 1)) '' ↑s)
[PROOFSTEP]
simpa only [Multiset.card_map, Multiset.map_map, comp_apply, Multiset.toFinset_map, Finset.coe_image,
  Finset.val_toFinset] using pow_multiset_sum_mem_span_pow (s.1.map f) n
[GOAL]
α : Type u
β : Type v
a b : α
inst✝ : CommSemiring α
I : Ideal α
s : Set α
hs : span s = ⊤
n : ℕ
⊢ span ((fun x => x ^ n) '' s) = ⊤
[PROOFSTEP]
rw [eq_top_iff_one]
[GOAL]
α : Type u
β : Type v
a b : α
inst✝ : CommSemiring α
I : Ideal α
s : Set α
hs : span s = ⊤
n : ℕ
⊢ 1 ∈ span ((fun x => x ^ n) '' s)
[PROOFSTEP]
cases' n with n
[GOAL]
case zero
α : Type u
β : Type v
a b : α
inst✝ : CommSemiring α
I : Ideal α
s : Set α
hs : span s = ⊤
⊢ 1 ∈ span ((fun x => x ^ Nat.zero) '' s)
[PROOFSTEP]
obtain rfl | ⟨x, hx⟩ := eq_empty_or_nonempty s
[GOAL]
case zero.inl
α : Type u
β : Type v
a b : α
inst✝ : CommSemiring α
I : Ideal α
hs : span ∅ = ⊤
⊢ 1 ∈ span ((fun x => x ^ Nat.zero) '' ∅)
[PROOFSTEP]
rw [Set.image_empty, hs]
[GOAL]
case zero.inl
α : Type u
β : Type v
a b : α
inst✝ : CommSemiring α
I : Ideal α
hs : span ∅ = ⊤
⊢ 1 ∈ ⊤
[PROOFSTEP]
trivial
[GOAL]
case zero.inr.intro
α : Type u
β : Type v
a b : α
inst✝ : CommSemiring α
I : Ideal α
s : Set α
hs : span s = ⊤
x : α
hx : x ∈ s
⊢ 1 ∈ span ((fun x => x ^ Nat.zero) '' s)
[PROOFSTEP]
exact subset_span ⟨_, hx, pow_zero _⟩
[GOAL]
case succ
α : Type u
β : Type v
a b : α
inst✝ : CommSemiring α
I : Ideal α
s : Set α
hs : span s = ⊤
n : ℕ
⊢ 1 ∈ span ((fun x => x ^ Nat.succ n) '' s)
[PROOFSTEP]
rw [eq_top_iff_one, span, Finsupp.mem_span_iff_total] at hs 
[GOAL]
case succ
α : Type u
β : Type v
a b : α
inst✝ : CommSemiring α
I : Ideal α
s : Set α
hs : ∃ l, ↑(Finsupp.total (↑s) α α Subtype.val) l = 1
n : ℕ
⊢ 1 ∈ span ((fun x => x ^ Nat.succ n) '' s)
[PROOFSTEP]
rcases hs with ⟨f, hf⟩
[GOAL]
case succ.intro
α : Type u
β : Type v
a b : α
inst✝ : CommSemiring α
I : Ideal α
s : Set α
n : ℕ
f : ↑s →₀ α
hf : ↑(Finsupp.total (↑s) α α Subtype.val) f = 1
⊢ 1 ∈ span ((fun x => x ^ Nat.succ n) '' s)
[PROOFSTEP]
have hf : (f.support.sum fun a => f a * a) = 1 := hf
[GOAL]
case succ.intro
α : Type u
β : Type v
a b : α
inst✝ : CommSemiring α
I : Ideal α
s : Set α
n : ℕ
f : ↑s →₀ α
hf✝ : ↑(Finsupp.total (↑s) α α Subtype.val) f = 1
hf : ∑ a in f.support, ↑f a * ↑a = 1
⊢ 1 ∈ span ((fun x => x ^ Nat.succ n) '' s)
[PROOFSTEP]
have := sum_pow_mem_span_pow f.support (fun a => f a * a) n
[GOAL]
case succ.intro
α : Type u
β : Type v
a b : α
inst✝ : CommSemiring α
I : Ideal α
s : Set α
n : ℕ
f : ↑s →₀ α
hf✝ : ↑(Finsupp.total (↑s) α α Subtype.val) f = 1
hf : ∑ a in f.support, ↑f a * ↑a = 1
this :
  (∑ i in f.support, ↑f i * ↑i) ^ (Finset.card f.support * n + 1) ∈
    span ((fun i => (↑f i * ↑i) ^ (n + 1)) '' ↑f.support)
⊢ 1 ∈ span ((fun x => x ^ Nat.succ n) '' s)
[PROOFSTEP]
rw [hf, one_pow] at this 
[GOAL]
case succ.intro
α : Type u
β : Type v
a b : α
inst✝ : CommSemiring α
I : Ideal α
s : Set α
n : ℕ
f : ↑s →₀ α
hf✝ : ↑(Finsupp.total (↑s) α α Subtype.val) f = 1
hf : ∑ a in f.support, ↑f a * ↑a = 1
this : 1 ∈ span ((fun i => (↑f i * ↑i) ^ (n + 1)) '' ↑f.support)
⊢ 1 ∈ span ((fun x => x ^ Nat.succ n) '' s)
[PROOFSTEP]
refine' span_le.mpr _ this
[GOAL]
case succ.intro
α : Type u
β : Type v
a b : α
inst✝ : CommSemiring α
I : Ideal α
s : Set α
n : ℕ
f : ↑s →₀ α
hf✝ : ↑(Finsupp.total (↑s) α α Subtype.val) f = 1
hf : ∑ a in f.support, ↑f a * ↑a = 1
this : 1 ∈ span ((fun i => (↑f i * ↑i) ^ (n + 1)) '' ↑f.support)
⊢ (fun i => (↑f i * ↑i) ^ (n + 1)) '' ↑f.support ⊆ ↑(span ((fun x => x ^ Nat.succ n) '' s))
[PROOFSTEP]
rintro _ hx
[GOAL]
case succ.intro
α : Type u
β : Type v
a b : α
inst✝ : CommSemiring α
I : Ideal α
s : Set α
n : ℕ
f : ↑s →₀ α
hf✝ : ↑(Finsupp.total (↑s) α α Subtype.val) f = 1
hf : ∑ a in f.support, ↑f a * ↑a = 1
this : 1 ∈ span ((fun i => (↑f i * ↑i) ^ (n + 1)) '' ↑f.support)
a✝ : α
hx : a✝ ∈ (fun i => (↑f i * ↑i) ^ (n + 1)) '' ↑f.support
⊢ a✝ ∈ ↑(span ((fun x => x ^ Nat.succ n) '' s))
[PROOFSTEP]
simp_rw [Set.mem_image] at hx 
[GOAL]
case succ.intro
α : Type u
β : Type v
a b : α
inst✝ : CommSemiring α
I : Ideal α
s : Set α
n : ℕ
f : ↑s →₀ α
hf✝ : ↑(Finsupp.total (↑s) α α Subtype.val) f = 1
hf : ∑ a in f.support, ↑f a * ↑a = 1
this : 1 ∈ span ((fun i => (↑f i * ↑i) ^ (n + 1)) '' ↑f.support)
a✝ : α
hx : ∃ x, x ∈ ↑f.support ∧ (↑f x * ↑x) ^ (n + 1) = a✝
⊢ a✝ ∈ ↑(span ((fun x => x ^ Nat.succ n) '' s))
[PROOFSTEP]
rcases hx with ⟨x, _, rfl⟩
[GOAL]
case succ.intro.intro.intro
α : Type u
β : Type v
a b : α
inst✝ : CommSemiring α
I : Ideal α
s : Set α
n : ℕ
f : ↑s →₀ α
hf✝ : ↑(Finsupp.total (↑s) α α Subtype.val) f = 1
hf : ∑ a in f.support, ↑f a * ↑a = 1
this : 1 ∈ span ((fun i => (↑f i * ↑i) ^ (n + 1)) '' ↑f.support)
x : ↑s
left✝ : x ∈ ↑f.support
⊢ (↑f x * ↑x) ^ (n + 1) ∈ ↑(span ((fun x => x ^ Nat.succ n) '' s))
[PROOFSTEP]
have : span ({(x : α) ^ (n + 1)} : Set α) ≤ span ((fun x : α => x ^ (n + 1)) '' s) :=
  by
  rw [span_le, Set.singleton_subset_iff]
  exact subset_span ⟨x, x.prop, rfl⟩
[GOAL]
α : Type u
β : Type v
a b : α
inst✝ : CommSemiring α
I : Ideal α
s : Set α
n : ℕ
f : ↑s →₀ α
hf✝ : ↑(Finsupp.total (↑s) α α Subtype.val) f = 1
hf : ∑ a in f.support, ↑f a * ↑a = 1
this : 1 ∈ span ((fun i => (↑f i * ↑i) ^ (n + 1)) '' ↑f.support)
x : ↑s
left✝ : x ∈ ↑f.support
⊢ span {↑x ^ (n + 1)} ≤ span ((fun x => x ^ (n + 1)) '' s)
[PROOFSTEP]
rw [span_le, Set.singleton_subset_iff]
[GOAL]
α : Type u
β : Type v
a b : α
inst✝ : CommSemiring α
I : Ideal α
s : Set α
n : ℕ
f : ↑s →₀ α
hf✝ : ↑(Finsupp.total (↑s) α α Subtype.val) f = 1
hf : ∑ a in f.support, ↑f a * ↑a = 1
this : 1 ∈ span ((fun i => (↑f i * ↑i) ^ (n + 1)) '' ↑f.support)
x : ↑s
left✝ : x ∈ ↑f.support
⊢ ↑x ^ (n + 1) ∈ ↑(span ((fun x => x ^ (n + 1)) '' s))
[PROOFSTEP]
exact subset_span ⟨x, x.prop, rfl⟩
[GOAL]
case succ.intro.intro.intro
α : Type u
β : Type v
a b : α
inst✝ : CommSemiring α
I : Ideal α
s : Set α
n : ℕ
f : ↑s →₀ α
hf✝ : ↑(Finsupp.total (↑s) α α Subtype.val) f = 1
hf : ∑ a in f.support, ↑f a * ↑a = 1
this✝ : 1 ∈ span ((fun i => (↑f i * ↑i) ^ (n + 1)) '' ↑f.support)
x : ↑s
left✝ : x ∈ ↑f.support
this : span {↑x ^ (n + 1)} ≤ span ((fun x => x ^ (n + 1)) '' s)
⊢ (↑f x * ↑x) ^ (n + 1) ∈ ↑(span ((fun x => x ^ Nat.succ n) '' s))
[PROOFSTEP]
refine' this _
[GOAL]
case succ.intro.intro.intro
α : Type u
β : Type v
a b : α
inst✝ : CommSemiring α
I : Ideal α
s : Set α
n : ℕ
f : ↑s →₀ α
hf✝ : ↑(Finsupp.total (↑s) α α Subtype.val) f = 1
hf : ∑ a in f.support, ↑f a * ↑a = 1
this✝ : 1 ∈ span ((fun i => (↑f i * ↑i) ^ (n + 1)) '' ↑f.support)
x : ↑s
left✝ : x ∈ ↑f.support
this : span {↑x ^ (n + 1)} ≤ span ((fun x => x ^ (n + 1)) '' s)
⊢ (↑f x * ↑x) ^ (n + 1) ∈ span {↑x ^ (n + 1)}
[PROOFSTEP]
rw [mul_pow, mem_span_singleton]
[GOAL]
case succ.intro.intro.intro
α : Type u
β : Type v
a b : α
inst✝ : CommSemiring α
I : Ideal α
s : Set α
n : ℕ
f : ↑s →₀ α
hf✝ : ↑(Finsupp.total (↑s) α α Subtype.val) f = 1
hf : ∑ a in f.support, ↑f a * ↑a = 1
this✝ : 1 ∈ span ((fun i => (↑f i * ↑i) ^ (n + 1)) '' ↑f.support)
x : ↑s
left✝ : x ∈ ↑f.support
this : span {↑x ^ (n + 1)} ≤ span ((fun x => x ^ (n + 1)) '' s)
⊢ ↑x ^ (n + 1) ∣ ↑f x ^ (n + 1) * ↑x ^ (n + 1)
[PROOFSTEP]
exact ⟨f x ^ (n + 1), mul_comm _ _⟩
[GOAL]
α : Type u
β : Type v
inst✝ : Ring α
I : Ideal α
a b x : α
⊢ span {-x} = span {x}
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u
β : Type v
inst✝ : Ring α
I : Ideal α
a b x x✝ : α
⊢ x✝ ∈ span {-x} ↔ x✝ ∈ span {x}
[PROOFSTEP]
simp only [mem_span_singleton']
[GOAL]
case h
α : Type u
β : Type v
inst✝ : Ring α
I : Ideal α
a b x x✝ : α
⊢ (∃ a, a * -x = x✝) ↔ ∃ a, a * x = x✝
[PROOFSTEP]
exact ⟨fun ⟨y, h⟩ => ⟨-y, h ▸ neg_mul_comm y x⟩, fun ⟨y, h⟩ => ⟨-y, h ▸ neg_mul_neg y x⟩⟩
[GOAL]
α : Type u
β : Type v
K : Type u
inst✝ : DivisionSemiring K
I : Ideal K
⊢ I = ⊥ ∨ I = ⊤
[PROOFSTEP]
rw [or_iff_not_imp_right]
[GOAL]
α : Type u
β : Type v
K : Type u
inst✝ : DivisionSemiring K
I : Ideal K
⊢ ¬I = ⊤ → I = ⊥
[PROOFSTEP]
change _ ≠ _ → _
[GOAL]
α : Type u
β : Type v
K : Type u
inst✝ : DivisionSemiring K
I : Ideal K
⊢ I ≠ ⊤ → I = ⊥
[PROOFSTEP]
rw [Ideal.ne_top_iff_one]
[GOAL]
α : Type u
β : Type v
K : Type u
inst✝ : DivisionSemiring K
I : Ideal K
⊢ ¬1 ∈ I → I = ⊥
[PROOFSTEP]
intro h1
[GOAL]
α : Type u
β : Type v
K : Type u
inst✝ : DivisionSemiring K
I : Ideal K
h1 : ¬1 ∈ I
⊢ I = ⊥
[PROOFSTEP]
rw [eq_bot_iff]
[GOAL]
α : Type u
β : Type v
K : Type u
inst✝ : DivisionSemiring K
I : Ideal K
h1 : ¬1 ∈ I
⊢ I ≤ ⊥
[PROOFSTEP]
intro r hr
[GOAL]
α : Type u
β : Type v
K : Type u
inst✝ : DivisionSemiring K
I : Ideal K
h1 : ¬1 ∈ I
r : K
hr : r ∈ I
⊢ r ∈ ⊥
[PROOFSTEP]
by_cases H : r = 0
[GOAL]
case pos
α : Type u
β : Type v
K : Type u
inst✝ : DivisionSemiring K
I : Ideal K
h1 : ¬1 ∈ I
r : K
hr : r ∈ I
H : r = 0
⊢ r ∈ ⊥
[PROOFSTEP]
simpa
[GOAL]
case neg
α : Type u
β : Type v
K : Type u
inst✝ : DivisionSemiring K
I : Ideal K
h1 : ¬1 ∈ I
r : K
hr : r ∈ I
H : ¬r = 0
⊢ r ∈ ⊥
[PROOFSTEP]
simpa [H, h1] using I.mul_mem_left r⁻¹ hr
[GOAL]
α : Type u
β : Type v
K : Type u
inst✝ : DivisionSemiring K
I : Ideal K
h : ⊥ = ⊤
⊢ ¬1 ∈ ⊤
[PROOFSTEP]
rw [← h]
[GOAL]
α : Type u
β : Type v
K : Type u
inst✝ : DivisionSemiring K
I : Ideal K
h : ⊥ = ⊤
⊢ ¬1 ∈ ⊥
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
R : Type u_1
inst✝ : CommRing R
I : Ideal R
a b c d : R
h1 : a - b ∈ I
h2 : c - d ∈ I
⊢ a * c - b * d ∈ I
[PROOFSTEP]
rw [show a * c - b * d = (a - b) * c + b * (c - d) by rw [sub_mul, mul_sub]; abel]
[GOAL]
α : Type u
β : Type v
R : Type u_1
inst✝ : CommRing R
I : Ideal R
a b c d : R
h1 : a - b ∈ I
h2 : c - d ∈ I
⊢ a * c - b * d = (a - b) * c + b * (c - d)
[PROOFSTEP]
rw [sub_mul, mul_sub]
[GOAL]
α : Type u
β : Type v
R : Type u_1
inst✝ : CommRing R
I : Ideal R
a b c d : R
h1 : a - b ∈ I
h2 : c - d ∈ I
⊢ a * c - b * d = a * c - b * c + (b * c - b * d)
[PROOFSTEP]
abel
[GOAL]
α : Type u
β : Type v
R : Type u_1
inst✝ : CommRing R
I : Ideal R
a b c d : R
h1 : a - b ∈ I
h2 : c - d ∈ I
⊢ a * c - b * d = a * c - b * c + (b * c - b * d)
[PROOFSTEP]
abel
[GOAL]
α : Type u
β : Type v
R : Type u_1
inst✝ : CommRing R
I : Ideal R
a b c d : R
h1 : a - b ∈ I
h2 : c - d ∈ I
⊢ (a - b) * c + b * (c - d) ∈ I
[PROOFSTEP]
exact I.add_mem (I.mul_mem_right _ h1) (I.mul_mem_left _ h2)
[GOAL]
α : Type u
β : Type v
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
hf : ¬IsField R
⊢ ∃ x _hx, ¬IsUnit x
[PROOFSTEP]
have : ¬_ := fun h => hf ⟨exists_pair_ne R, mul_comm, h⟩
[GOAL]
α : Type u
β : Type v
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
hf : ¬IsField R
this : ¬∀ {a : R}, a ≠ 0 → ∃ b, a * b = 1
⊢ ∃ x _hx, ¬IsUnit x
[PROOFSTEP]
simp_rw [isUnit_iff_exists_inv]
[GOAL]
α : Type u
β : Type v
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
hf : ¬IsField R
this : ¬∀ {a : R}, a ≠ 0 → ∃ b, a * b = 1
⊢ ∃ x h, ¬∃ b, x * b = 1
[PROOFSTEP]
push_neg at this ⊢
[GOAL]
α : Type u
β : Type v
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
hf : ¬IsField R
this : Exists fun {a} => a ≠ 0 ∧ ∀ (b : R), a * b ≠ 1
⊢ ∃ x h, ∀ (b : R), x * b ≠ 1
[PROOFSTEP]
obtain ⟨x, hx, not_unit⟩ := this
[GOAL]
case intro.intro
α : Type u
β : Type v
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
hf : ¬IsField R
x : R
hx : x ≠ 0
not_unit : ∀ (b : R), x * b ≠ 1
⊢ ∃ x h, ∀ (b : R), x * b ≠ 1
[PROOFSTEP]
exact ⟨x, hx, not_unit⟩
[GOAL]
α : Type u
β : Type v
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
⊢ ¬IsField R ↔ ∃ I, ⊥ < I ∧ I < ⊤
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u
β : Type v
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
⊢ ¬IsField R → ∃ I, ⊥ < I ∧ I < ⊤
[PROOFSTEP]
intro h
[GOAL]
case mp
α : Type u
β : Type v
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
h : ¬IsField R
⊢ ∃ I, ⊥ < I ∧ I < ⊤
[PROOFSTEP]
obtain ⟨x, nz, nu⟩ := exists_not_isUnit_of_not_isField h
[GOAL]
case mp.intro.intro
α : Type u
β : Type v
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
h : ¬IsField R
x : R
nz : x ≠ 0
nu : ¬IsUnit x
⊢ ∃ I, ⊥ < I ∧ I < ⊤
[PROOFSTEP]
use Ideal.span { x }
[GOAL]
case h
α : Type u
β : Type v
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
h : ¬IsField R
x : R
nz : x ≠ 0
nu : ¬IsUnit x
⊢ ⊥ < Ideal.span {x} ∧ Ideal.span {x} < ⊤
[PROOFSTEP]
rw [bot_lt_iff_ne_bot, lt_top_iff_ne_top]
[GOAL]
case h
α : Type u
β : Type v
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
h : ¬IsField R
x : R
nz : x ≠ 0
nu : ¬IsUnit x
⊢ Ideal.span {x} ≠ ⊥ ∧ Ideal.span {x} ≠ ⊤
[PROOFSTEP]
exact ⟨mt Ideal.span_singleton_eq_bot.mp nz, mt Ideal.span_singleton_eq_top.mp nu⟩
[GOAL]
case mpr
α : Type u
β : Type v
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
⊢ (∃ I, ⊥ < I ∧ I < ⊤) → ¬IsField R
[PROOFSTEP]
rintro ⟨I, bot_lt, lt_top⟩ hf
[GOAL]
case mpr.intro.intro
α : Type u
β : Type v
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
I : Ideal R
bot_lt : ⊥ < I
lt_top : I < ⊤
hf : IsField R
⊢ False
[PROOFSTEP]
obtain ⟨x, mem, ne_zero⟩ := SetLike.exists_of_lt bot_lt
[GOAL]
case mpr.intro.intro.intro.intro
α : Type u
β : Type v
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
I : Ideal R
bot_lt : ⊥ < I
lt_top : I < ⊤
hf : IsField R
x : R
mem : x ∈ I
ne_zero : ¬x ∈ ⊥
⊢ False
[PROOFSTEP]
rw [Submodule.mem_bot] at ne_zero 
[GOAL]
case mpr.intro.intro.intro.intro
α : Type u
β : Type v
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
I : Ideal R
bot_lt : ⊥ < I
lt_top : I < ⊤
hf : IsField R
x : R
mem : x ∈ I
ne_zero : ¬x = 0
⊢ False
[PROOFSTEP]
obtain ⟨y, hy⟩ := hf.mul_inv_cancel ne_zero
[GOAL]
case mpr.intro.intro.intro.intro.intro
α : Type u
β : Type v
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
I : Ideal R
bot_lt : ⊥ < I
lt_top : I < ⊤
hf : IsField R
x : R
mem : x ∈ I
ne_zero : ¬x = 0
y : R
hy : x * y = 1
⊢ False
[PROOFSTEP]
rw [lt_top_iff_ne_top, Ne.def, Ideal.eq_top_iff_one, ← hy] at lt_top 
[GOAL]
case mpr.intro.intro.intro.intro.intro
α : Type u
β : Type v
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
I : Ideal R
bot_lt : ⊥ < I
hf : IsField R
x : R
mem : x ∈ I
ne_zero : ¬x = 0
y : R
lt_top : ¬x * y ∈ I
hy : x * y = 1
⊢ False
[PROOFSTEP]
exact lt_top (I.mul_mem_right _ mem)
[GOAL]
α : Type u
β : Type v
R : Type u_1
inst✝ : CommSemiring R
⊢ IsField R ↔ IsSimpleOrder (Ideal R)
[PROOFSTEP]
cases subsingleton_or_nontrivial R
[GOAL]
case inl
α : Type u
β : Type v
R : Type u_1
inst✝ : CommSemiring R
h✝ : Subsingleton R
⊢ IsField R ↔ IsSimpleOrder (Ideal R)
[PROOFSTEP]
exact ⟨fun h => (not_isField_of_subsingleton _ h).elim, fun h => (false_of_nontrivial_of_subsingleton <| Ideal R).elim⟩
[GOAL]
case inr
α : Type u
β : Type v
R : Type u_1
inst✝ : CommSemiring R
h✝ : Nontrivial R
⊢ IsField R ↔ IsSimpleOrder (Ideal R)
[PROOFSTEP]
rw [← not_iff_not, Ring.not_isField_iff_exists_ideal_bot_lt_and_lt_top, ← not_iff_not]
[GOAL]
case inr
α : Type u
β : Type v
R : Type u_1
inst✝ : CommSemiring R
h✝ : Nontrivial R
⊢ (¬∃ I, ⊥ < I ∧ I < ⊤) ↔ ¬¬IsSimpleOrder (Ideal R)
[PROOFSTEP]
push_neg
[GOAL]
case inr
α : Type u
β : Type v
R : Type u_1
inst✝ : CommSemiring R
h✝ : Nontrivial R
⊢ (∀ (I : Ideal R), ⊥ < I → ¬I < ⊤) ↔ IsSimpleOrder (Ideal R)
[PROOFSTEP]
simp_rw [lt_top_iff_ne_top, bot_lt_iff_ne_bot, ← or_iff_not_imp_left, not_ne_iff]
[GOAL]
case inr
α : Type u
β : Type v
R : Type u_1
inst✝ : CommSemiring R
h✝ : Nontrivial R
⊢ (∀ (I : Ideal R), I = ⊥ ∨ I = ⊤) ↔ IsSimpleOrder (Ideal R)
[PROOFSTEP]
exact ⟨fun h => ⟨h⟩, fun h => h.2⟩
[GOAL]
α : Type u
β : Type v
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
M : Ideal R
max : Ideal.IsMaximal M
not_field : ¬IsField R
⊢ M ≠ ⊥
[PROOFSTEP]
rintro h
[GOAL]
α : Type u
β : Type v
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
M : Ideal R
max : Ideal.IsMaximal M
not_field : ¬IsField R
h : M = ⊥
⊢ False
[PROOFSTEP]
rw [h] at max 
[GOAL]
α : Type u
β : Type v
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
M : Ideal R
max : Ideal.IsMaximal ⊥
not_field : ¬IsField R
h : M = ⊥
⊢ False
[PROOFSTEP]
rcases max with ⟨⟨_h1, h2⟩⟩
[GOAL]
case mk.intro
α : Type u
β : Type v
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
M : Ideal R
not_field : ¬IsField R
h : M = ⊥
_h1 : ⊥ ≠ ⊤
h2 : ∀ (b : Ideal R), ⊥ < b → b = ⊤
⊢ False
[PROOFSTEP]
obtain ⟨I, hIbot, hItop⟩ := not_isField_iff_exists_ideal_bot_lt_and_lt_top.mp not_field
[GOAL]
case mk.intro.intro.intro
α : Type u
β : Type v
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
M : Ideal R
not_field : ¬IsField R
h : M = ⊥
_h1 : ⊥ ≠ ⊤
h2 : ∀ (b : Ideal R), ⊥ < b → b = ⊤
I : Ideal R
hIbot : ⊥ < I
hItop : I < ⊤
⊢ False
[PROOFSTEP]
exact ne_of_lt hItop (h2 I hIbot)
[GOAL]
α : Type u
β : Type v
R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
M : Ideal R
hm : IsMaximal M
non_field : ¬IsField R
⊢ ⊥ < M
[PROOFSTEP]
rcases Ring.not_isField_iff_exists_ideal_bot_lt_and_lt_top.1 non_field with ⟨I, Ibot, Itop⟩
[GOAL]
case intro.intro
α : Type u
β : Type v
R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
M : Ideal R
hm : IsMaximal M
non_field : ¬IsField R
I : Ideal R
Ibot : ⊥ < I
Itop : I < ⊤
⊢ ⊥ < M
[PROOFSTEP]
constructor
[GOAL]
case intro.intro.left
α : Type u
β : Type v
R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
M : Ideal R
hm : IsMaximal M
non_field : ¬IsField R
I : Ideal R
Ibot : ⊥ < I
Itop : I < ⊤
⊢ ↑⊥ ⊆ ↑M
[PROOFSTEP]
simp
[GOAL]
case intro.intro.right
α : Type u
β : Type v
R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
M : Ideal R
hm : IsMaximal M
non_field : ¬IsField R
I : Ideal R
Ibot : ⊥ < I
Itop : I < ⊤
⊢ ¬↑M ⊆ ↑⊥
[PROOFSTEP]
intro mle
[GOAL]
case intro.intro.right
α : Type u
β : Type v
R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
M : Ideal R
hm : IsMaximal M
non_field : ¬IsField R
I : Ideal R
Ibot : ⊥ < I
Itop : I < ⊤
mle : ↑M ⊆ ↑⊥
⊢ False
[PROOFSTEP]
apply lt_irrefl (⊤ : Ideal R)
[GOAL]
case intro.intro.right
α : Type u
β : Type v
R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
M : Ideal R
hm : IsMaximal M
non_field : ¬IsField R
I : Ideal R
Ibot : ⊥ < I
Itop : I < ⊤
mle : ↑M ⊆ ↑⊥
⊢ ⊤ < ⊤
[PROOFSTEP]
have : M = ⊥ := eq_bot_iff.mpr mle
[GOAL]
case intro.intro.right
α : Type u
β : Type v
R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
M : Ideal R
hm : IsMaximal M
non_field : ¬IsField R
I : Ideal R
Ibot : ⊥ < I
Itop : I < ⊤
mle : ↑M ⊆ ↑⊥
this : M = ⊥
⊢ ⊤ < ⊤
[PROOFSTEP]
rw [← this] at Ibot 
[GOAL]
case intro.intro.right
α : Type u
β : Type v
R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
M : Ideal R
hm : IsMaximal M
non_field : ¬IsField R
I : Ideal R
Ibot : M < I
Itop : I < ⊤
mle : ↑M ⊆ ↑⊥
this : M = ⊥
⊢ ⊤ < ⊤
[PROOFSTEP]
rwa [hm.1.2 I Ibot] at Itop 
[GOAL]
α : Type u
β : Type v
a b : α
inst✝ : CommSemiring α
h : a ∈ nonunits α
⊢ ∃ I, Ideal.IsMaximal I ∧ a ∈ I
[PROOFSTEP]
have : Ideal.span ({ a } : Set α) ≠ ⊤ := by
  intro H
  rw [Ideal.span_singleton_eq_top] at H 
  contradiction
[GOAL]
α : Type u
β : Type v
a b : α
inst✝ : CommSemiring α
h : a ∈ nonunits α
⊢ Ideal.span {a} ≠ ⊤
[PROOFSTEP]
intro H
[GOAL]
α : Type u
β : Type v
a b : α
inst✝ : CommSemiring α
h : a ∈ nonunits α
H : Ideal.span {a} = ⊤
⊢ False
[PROOFSTEP]
rw [Ideal.span_singleton_eq_top] at H 
[GOAL]
α : Type u
β : Type v
a b : α
inst✝ : CommSemiring α
h : a ∈ nonunits α
H : IsUnit a
⊢ False
[PROOFSTEP]
contradiction
[GOAL]
α : Type u
β : Type v
a b : α
inst✝ : CommSemiring α
h : a ∈ nonunits α
this : Ideal.span {a} ≠ ⊤
⊢ ∃ I, Ideal.IsMaximal I ∧ a ∈ I
[PROOFSTEP]
rcases Ideal.exists_le_maximal _ this with ⟨I, Imax, H⟩
[GOAL]
case intro.intro
α : Type u
β : Type v
a b : α
inst✝ : CommSemiring α
h : a ∈ nonunits α
this : Ideal.span {a} ≠ ⊤
I : Ideal α
Imax : Ideal.IsMaximal I
H : Ideal.span {a} ≤ I
⊢ ∃ I, Ideal.IsMaximal I ∧ a ∈ I
[PROOFSTEP]
use I, Imax
[GOAL]
case right
α : Type u
β : Type v
a b : α
inst✝ : CommSemiring α
h : a ∈ nonunits α
this : Ideal.span {a} ≠ ⊤
I : Ideal α
Imax : Ideal.IsMaximal I
H : Ideal.span {a} ≤ I
⊢ a ∈ I
[PROOFSTEP]
apply H
[GOAL]
case right.a
α : Type u
β : Type v
a b : α
inst✝ : CommSemiring α
h : a ∈ nonunits α
this : Ideal.span {a} ≠ ⊤
I : Ideal α
Imax : Ideal.IsMaximal I
H : Ideal.span {a} ≤ I
⊢ a ∈ Ideal.span {a}
[PROOFSTEP]
apply Ideal.subset_span
[GOAL]
case right.a.a
α : Type u
β : Type v
a b : α
inst✝ : CommSemiring α
h : a ∈ nonunits α
this : Ideal.span {a} ≠ ⊤
I : Ideal α
Imax : Ideal.IsMaximal I
H : Ideal.span {a} ≤ I
⊢ a ∈ {a}
[PROOFSTEP]
exact Set.mem_singleton a
