Theorem: mem_or_mem_of_mul_mem (Kaplanski4/Kaplanski.lean)

State before:
R : Type u_1
inst✝ : CommSemiring R
P : Ideal R
S : Subsemigroup R
x y : R
hP : P ∈ Kaplansky.set S
hmax : ∀ I ∈ Kaplansky.set S, P ≤ I → I = P
⊢ x * y ∈ P → x ∈ P ∨ y ∈ P
Tactic:
intro hxy
State after:
R : Type u_1
inst✝ : CommSemiring R
P : Ideal R
S : Subsemigroup R
x y : R
hP : P ∈ Kaplansky.set S
hmax : ∀ I ∈ Kaplansky.set S, P ≤ I → I = P
hxy : x * y ∈ P
⊢ x ∈ P ∨ y ∈ P

State before:
R : Type u_1
inst✝ : CommSemiring R
P : Ideal R
S : Subsemigroup R
x y : R
hP : P ∈ Kaplansky.set S
hmax : ∀ I ∈ Kaplansky.set S, P ≤ I → I = P
hxy : x * y ∈ P
⊢ x ∈ P ∨ y ∈ P
Tactic:
by_contra h
State after:
R : Type u_1
inst✝ : CommSemiring R
P : Ideal R
S : Subsemigroup R
x y : R
hP : P ∈ Kaplansky.set S
hmax : ∀ I ∈ Kaplansky.set S, P ≤ I → I = P
hxy : x * y ∈ P
h : ¬(x ∈ P ∨ y ∈ P)
⊢ False

State before:
R : Type u_1
inst✝ : CommSemiring R
P : Ideal R
S : Subsemigroup R
x y : R
hP : P ∈ Kaplansky.set S
hmax : ∀ I ∈ Kaplansky.set S, P ≤ I → I = P
hxy : x * y ∈ P
h : ¬(x ∈ P ∨ y ∈ P)
⊢ False
Tactic:
push_neg at h
State after:
R : Type u_1
inst✝ : CommSemiring R
P : Ideal R
S : Subsemigroup R
x y : R
hP : P ∈ Kaplansky.set S
hmax : ∀ I ∈ Kaplansky.set S, P ≤ I → I = P
hxy : x * y ∈ P
h : x ∉ P ∧ y ∉ P
⊢ False

State before:
R : Type u_1
inst✝ : CommSemiring R
P : Ideal R
S : Subsemigroup R
x y : R
hP : P ∈ Kaplansky.set S
hmax : ∀ I ∈ Kaplansky.set S, P ≤ I → I = P
hxy : x * y ∈ P
h : x ∉ P ∧ y ∉ P
⊢ False
Tactic:
cases' h with h' h''
State after:
case intro
R : Type u_1
inst✝ : CommSemiring R
P : Ideal R
S : Subsemigroup R
x y : R
hP : P ∈ Kaplansky.set S
hmax : ∀ I ∈ Kaplansky.set S, P ≤ I → I = P
hxy : x * y ∈ P
h' : x ∉ P
h'' : y ∉ P
⊢ False

State before:
case intro
R : Type u_1
inst✝ : CommSemiring R
P : Ideal R
S : Subsemigroup R
x y : R
hP : P ∈ Kaplansky.set S
hmax : ∀ I ∈ Kaplansky.set S, P ≤ I → I = P
hxy : x * y ∈ P
h' : x ∉ P
h'' : y ∉ P
⊢ False
Tactic:
let I := P ⊔ Ideal.span {x}
State after:
case intro
R : Type u_1
inst✝ : CommSemiring R
P : Ideal R
S : Subsemigroup R
x y : R
hP : P ∈ Kaplansky.set S
hmax : ∀ I ∈ Kaplansky.set S, P ≤ I → I = P
hxy : x * y ∈ P
h' : x ∉ P
h'' : y ∉ P
I : Ideal R := P ⊔ Ideal.span {x}
⊢ False

State before:
case intro
R : Type u_1
inst✝ : CommSemiring R
P : Ideal R
S : Subsemigroup R
x y : R
hP : P ∈ Kaplansky.set S
hmax : ∀ I ∈ Kaplansky.set S, P ≤ I → I = P
hxy : x * y ∈ P
h' : x ∉ P
h'' : y ∉ P
I : Ideal R := P ⊔ Ideal.span {x}
⊢ False
Tactic:
let J := P ⊔ Ideal.span {y}
State after:
case intro
R : Type u_1
inst✝ : CommSemiring R
P : Ideal R
S : Subsemigroup R
x y : R
hP : P ∈ Kaplansky.set S
hmax : ∀ I ∈ Kaplansky.set S, P ≤ I → I = P
hxy : x * y ∈ P
h' : x ∉ P
h'' : y ∉ P
I : Ideal R := P ⊔ Ideal.span {x}
J : Ideal R := P ⊔ Ideal.span {y}
⊢ False

State before:
case intro
R : Type u_1
inst✝ : CommSemiring R
P : Ideal R
S : Subsemigroup R
x y : R
hP : P ∈ Kaplansky.set S
hmax : ∀ I ∈ Kaplansky.set S, P ≤ I → I = P
hxy : x * y ∈ P
h' : x ∉ P
h'' : y ∉ P
I : Ideal R := P ⊔ Ideal.span {x}
J : Ideal R := P ⊔ Ideal.span {y}
⊢ False
Tactic:
have h₁ : ∃ x : R, x ∈ (I : Set R) ∩ S := by
  refine' exists_mem_inter hmax (lt_of_le_of_ne' le_sup_left _)
  intro hI
  rw [← hI, ← I.span_singleton_le_iff_mem] at h'
  exact h' le_sup_right
State after:
case intro
R : Type u_1
inst✝ : CommSemiring R
P : Ideal R
S : Subsemigroup R
x y : R
hP : P ∈ Kaplansky.set S
hmax : ∀ I ∈ Kaplansky.set S, P ≤ I → I = P
hxy : x * y ∈ P
h' : x ∉ P
h'' : y ∉ P
I : Ideal R := P ⊔ Ideal.span {x}
J : Ideal R := P ⊔ Ideal.span {y}
h₁ : ∃ x, x ∈ ↑I ∩ ↑S
⊢ False

State before:
case intro
R : Type u_1
inst✝ : CommSemiring R
P : Ideal R
S : Subsemigroup R
x y : R
hP : P ∈ Kaplansky.set S
hmax : ∀ I ∈ Kaplansky.set S, P ≤ I → I = P
hxy : x * y ∈ P
h' : x ∉ P
h'' : y ∉ P
I : Ideal R := P ⊔ Ideal.span {x}
J : Ideal R := P ⊔ Ideal.span {y}
h₁ : ∃ x, x ∈ ↑I ∩ ↑S
⊢ False
Tactic:
have h₂ : ∃ x : R, x ∈ (J : Set R) ∩ S := by
  refine' exists_mem_inter hmax (lt_of_le_of_ne' le_sup_left _)
  intro hJ
  rw [← hJ, ← J.span_singleton_le_iff_mem] at h''
  exact h'' le_sup_right
State after:
case intro
R : Type u_1
inst✝ : CommSemiring R
P : Ideal R
S : Subsemigroup R
x y : R
hP : P ∈ Kaplansky.set S
hmax : ∀ I ∈ Kaplansky.set S, P ≤ I → I = P
hxy : x * y ∈ P
h' : x ∉ P
h'' : y ∉ P
I : Ideal R := P ⊔ Ideal.span {x}
J : Ideal R := P ⊔ Ideal.span {y}
h₁ : ∃ x, x ∈ ↑I ∩ ↑S
h₂ : ∃ x, x ∈ ↑J ∩ ↑S
⊢ False

State before:
case intro
R : Type u_1
inst✝ : CommSemiring R
P : Ideal R
S : Subsemigroup R
x y : R
hP : P ∈ Kaplansky.set S
hmax : ∀ I ∈ Kaplansky.set S, P ≤ I → I = P
hxy : x * y ∈ P
h' : x ∉ P
h'' : y ∉ P
I : Ideal R := P ⊔ Ideal.span {x}
J : Ideal R := P ⊔ Ideal.span {y}
h₁ : ∃ x, x ∈ ↑I ∩ ↑S
h₂ : ∃ x, x ∈ ↑J ∩ ↑S
⊢ False
Tactic:
rcases h₁, h₂ with ⟨⟨s, ⟨hs, hs'⟩⟩, ⟨t, ⟨ht, ht'⟩⟩⟩
State after:
case intro.intro.intro.intro.intro
R : Type u_1
inst✝ : CommSemiring R
P : Ideal R
S : Subsemigroup R
x y : R
hP : P ∈ Kaplansky.set S
hmax : ∀ I ∈ Kaplansky.set S, P ≤ I → I = P
hxy : x * y ∈ P
h' : x ∉ P
h'' : y ∉ P
I : Ideal R := P ⊔ Ideal.span {x}
J : Ideal R := P ⊔ Ideal.span {y}
s : R
hs : s ∈ ↑I
hs' : s ∈ ↑S
t : R
ht : t ∈ ↑J
ht' : t ∈ ↑S
⊢ False

State before:
case intro.intro.intro.intro.intro
R : Type u_1
inst✝ : CommSemiring R
P : Ideal R
S : Subsemigroup R
x y : R
hP : P ∈ Kaplansky.set S
hmax : ∀ I ∈ Kaplansky.set S, P ≤ I → I = P
hxy : x * y ∈ P
h' : x ∉ P
h'' : y ∉ P
I : Ideal R := P ⊔ Ideal.span {x}
J : Ideal R := P ⊔ Ideal.span {y}
s : R
hs : s ∈ ↑I
hs' : s ∈ ↑S
t : R
ht : t ∈ ↑J
ht' : t ∈ ↑S
⊢ False
Tactic:
have h₃ : I * J ≤ P := by
  rw [Ideal.mul_sup, Ideal.sup_mul, Ideal.sup_mul, Ideal.span_singleton_mul_span_singleton]
  exact
    sup_le (sup_le Ideal.mul_le_right Ideal.mul_le_left)
      (sup_le Ideal.mul_le_right (P.span_singleton_le_iff_mem.2 hxy))
State after:
case intro.intro.intro.intro.intro
R : Type u_1
inst✝ : CommSemiring R
P : Ideal R
S : Subsemigroup R
x y : R
hP : P ∈ Kaplansky.set S
hmax : ∀ I ∈ Kaplansky.set S, P ≤ I → I = P
hxy : x * y ∈ P
h' : x ∉ P
h'' : y ∉ P
I : Ideal R := P ⊔ Ideal.span {x}
J : Ideal R := P ⊔ Ideal.span {y}
s : R
hs : s ∈ ↑I
hs' : s ∈ ↑S
t : R
ht : t ∈ ↑J
ht' : t ∈ ↑S
h₃ : I * J ≤ P
⊢ False

State before:
case intro.intro.intro.intro.intro
R : Type u_1
inst✝ : CommSemiring R
P : Ideal R
S : Subsemigroup R
x y : R
hP : P ∈ Kaplansky.set S
hmax : ∀ I ∈ Kaplansky.set S, P ≤ I → I = P
hxy : x * y ∈ P
h' : x ∉ P
h'' : y ∉ P
I : Ideal R := P ⊔ Ideal.span {x}
J : Ideal R := P ⊔ Ideal.span {y}
s : R
hs : s ∈ ↑I
hs' : s ∈ ↑S
t : R
ht : t ∈ ↑J
ht' : t ∈ ↑S
h₃ : I * J ≤ P
⊢ False
Tactic:
exact
  Set.eq_empty_iff_forall_not_mem.1 hP (s * t) ⟨h₃ (Ideal.mul_mem_mul hs ht), S.mul_mem hs' ht'⟩
State after:
no goals

State before:
R : Type u_1
inst✝ : CommSemiring R
P : Ideal R
S : Subsemigroup R
x y : R
hP : P ∈ Kaplansky.set S
hmax : ∀ I ∈ Kaplansky.set S, P ≤ I → I = P
hxy : x * y ∈ P
h' : x ∉ P
h'' : y ∉ P
I : Ideal R := P ⊔ Ideal.span {x}
J : Ideal R := P ⊔ Ideal.span {y}
⊢ ∃ x, x ∈ ↑I ∩ ↑S
Tactic:
refine' exists_mem_inter hmax (lt_of_le_of_ne' le_sup_left _)
State after:
R : Type u_1
inst✝ : CommSemiring R
P : Ideal R
S : Subsemigroup R
x y : R
hP : P ∈ Kaplansky.set S
hmax : ∀ I ∈ Kaplansky.set S, P ≤ I → I = P
hxy : x * y ∈ P
h' : x ∉ P
h'' : y ∉ P
I : Ideal R := P ⊔ Ideal.span {x}
J : Ideal R := P ⊔ Ideal.span {y}
⊢ I ≠ P

State before:
R : Type u_1
inst✝ : CommSemiring R
P : Ideal R
S : Subsemigroup R
x y : R
hP : P ∈ Kaplansky.set S
hmax : ∀ I ∈ Kaplansky.set S, P ≤ I → I = P
hxy : x * y ∈ P
h' : x ∉ P
h'' : y ∉ P
I : Ideal R := P ⊔ Ideal.span {x}
J : Ideal R := P ⊔ Ideal.span {y}
⊢ I ≠ P
Tactic:
intro hI
State after:
R : Type u_1
inst✝ : CommSemiring R
P : Ideal R
S : Subsemigroup R
x y : R
hP : P ∈ Kaplansky.set S
hmax : ∀ I ∈ Kaplansky.set S, P ≤ I → I = P
hxy : x * y ∈ P
h' : x ∉ P
h'' : y ∉ P
I : Ideal R := P ⊔ Ideal.span {x}
J : Ideal R := P ⊔ Ideal.span {y}
hI : I = P
⊢ False

State before:
R : Type u_1
inst✝ : CommSemiring R
P : Ideal R
S : Subsemigroup R
x y : R
hP : P ∈ Kaplansky.set S
hmax : ∀ I ∈ Kaplansky.set S, P ≤ I → I = P
hxy : x * y ∈ P
h' : x ∉ P
h'' : y ∉ P
I : Ideal R := P ⊔ Ideal.span {x}
J : Ideal R := P ⊔ Ideal.span {y}
hI : I = P
⊢ False
Tactic:
rw [← hI, ← I.span_singleton_le_iff_mem] at h'
State after:
R : Type u_1
inst✝ : CommSemiring R
P : Ideal R
S : Subsemigroup R
x y : R
hP : P ∈ Kaplansky.set S
hmax : ∀ I ∈ Kaplansky.set S, P ≤ I → I = P
hxy : x * y ∈ P
h'' : y ∉ P
I : Ideal R := P ⊔ Ideal.span {x}
h' : ¬Ideal.span {x} ≤ I
J : Ideal R := P ⊔ Ideal.span {y}
hI : I = P
⊢ False

State before:
R : Type u_1
inst✝ : CommSemiring R
P : Ideal R
S : Subsemigroup R
x y : R
hP : P ∈ Kaplansky.set S
hmax : ∀ I ∈ Kaplansky.set S, P ≤ I → I = P
hxy : x * y ∈ P
h'' : y ∉ P
I : Ideal R := P ⊔ Ideal.span {x}
h' : ¬Ideal.span {x} ≤ I
J : Ideal R := P ⊔ Ideal.span {y}
hI : I = P
⊢ False
Tactic:
exact h' le_sup_right
State after:
no goals

State before:
R : Type u_1
inst✝ : CommSemiring R
P : Ideal R
S : Subsemigroup R
x y : R
hP : P ∈ Kaplansky.set S
hmax : ∀ I ∈ Kaplansky.set S, P ≤ I → I = P
hxy : x * y ∈ P
h' : x ∉ P
h'' : y ∉ P
I : Ideal R := P ⊔ Ideal.span {x}
J : Ideal R := P ⊔ Ideal.span {y}
h₁ : ∃ x, x ∈ ↑I ∩ ↑S
⊢ ∃ x, x ∈ ↑J ∩ ↑S
Tactic:
refine' exists_mem_inter hmax (lt_of_le_of_ne' le_sup_left _)
State after:
R : Type u_1
inst✝ : CommSemiring R
P : Ideal R
S : Subsemigroup R
x y : R
hP : P ∈ Kaplansky.set S
hmax : ∀ I ∈ Kaplansky.set S, P ≤ I → I = P
hxy : x * y ∈ P
h' : x ∉ P
h'' : y ∉ P
I : Ideal R := P ⊔ Ideal.span {x}
J : Ideal R := P ⊔ Ideal.span {y}
h₁ : ∃ x, x ∈ ↑I ∩ ↑S
⊢ J ≠ P

State before:
R : Type u_1
inst✝ : CommSemiring R
P : Ideal R
S : Subsemigroup R
x y : R
hP : P ∈ Kaplansky.set S
hmax : ∀ I ∈ Kaplansky.set S, P ≤ I → I = P
hxy : x * y ∈ P
h' : x ∉ P
h'' : y ∉ P
I : Ideal R := P ⊔ Ideal.span {x}
J : Ideal R := P ⊔ Ideal.span {y}
h₁ : ∃ x, x ∈ ↑I ∩ ↑S
⊢ J ≠ P
Tactic:
intro hJ
State after:
R : Type u_1
inst✝ : CommSemiring R
P : Ideal R
S : Subsemigroup R
x y : R
hP : P ∈ Kaplansky.set S
hmax : ∀ I ∈ Kaplansky.set S, P ≤ I → I = P
hxy : x * y ∈ P
h' : x ∉ P
h'' : y ∉ P
I : Ideal R := P ⊔ Ideal.span {x}
J : Ideal R := P ⊔ Ideal.span {y}
h₁ : ∃ x, x ∈ ↑I ∩ ↑S
hJ : J = P
⊢ False

State before:
R : Type u_1
inst✝ : CommSemiring R
P : Ideal R
S : Subsemigroup R
x y : R
hP : P ∈ Kaplansky.set S
hmax : ∀ I ∈ Kaplansky.set S, P ≤ I → I = P
hxy : x * y ∈ P
h' : x ∉ P
h'' : y ∉ P
I : Ideal R := P ⊔ Ideal.span {x}
J : Ideal R := P ⊔ Ideal.span {y}
h₁ : ∃ x, x ∈ ↑I ∩ ↑S
hJ : J = P
⊢ False
Tactic:
rw [← hJ, ← J.span_singleton_le_iff_mem] at h''
State after:
R : Type u_1
inst✝ : CommSemiring R
P : Ideal R
S : Subsemigroup R
x y : R
hP : P ∈ Kaplansky.set S
hmax : ∀ I ∈ Kaplansky.set S, P ≤ I → I = P
hxy : x * y ∈ P
h' : x ∉ P
I : Ideal R := P ⊔ Ideal.span {x}
J : Ideal R := P ⊔ Ideal.span {y}
h'' : ¬Ideal.span {y} ≤ J
h₁ : ∃ x, x ∈ ↑I ∩ ↑S
hJ : J = P
⊢ False

State before:
R : Type u_1
inst✝ : CommSemiring R
P : Ideal R
S : Subsemigroup R
x y : R
hP : P ∈ Kaplansky.set S
hmax : ∀ I ∈ Kaplansky.set S, P ≤ I → I = P
hxy : x * y ∈ P
h' : x ∉ P
I : Ideal R := P ⊔ Ideal.span {x}
J : Ideal R := P ⊔ Ideal.span {y}
h'' : ¬Ideal.span {y} ≤ J
h₁ : ∃ x, x ∈ ↑I ∩ ↑S
hJ : J = P
⊢ False
Tactic:
exact h'' le_sup_right
State after:
no goals

State before:
R : Type u_1
inst✝ : CommSemiring R
P : Ideal R
S : Subsemigroup R
x y : R
hP : P ∈ Kaplansky.set S
hmax : ∀ I ∈ Kaplansky.set S, P ≤ I → I = P
hxy : x * y ∈ P
h' : x ∉ P
h'' : y ∉ P
I : Ideal R := P ⊔ Ideal.span {x}
J : Ideal R := P ⊔ Ideal.span {y}
s : R
hs : s ∈ ↑I
hs' : s ∈ ↑S
t : R
ht : t ∈ ↑J
ht' : t ∈ ↑S
⊢ I * J ≤ P
Tactic:
rw [Ideal.mul_sup, Ideal.sup_mul, Ideal.sup_mul, Ideal.span_singleton_mul_span_singleton]
State after:
R : Type u_1
inst✝ : CommSemiring R
P : Ideal R
S : Subsemigroup R
x y : R
hP : P ∈ Kaplansky.set S
hmax : ∀ I ∈ Kaplansky.set S, P ≤ I → I = P
hxy : x * y ∈ P
h' : x ∉ P
h'' : y ∉ P
I : Ideal R := P ⊔ Ideal.span {x}
J : Ideal R := P ⊔ Ideal.span {y}
s : R
hs : s ∈ ↑I
hs' : s ∈ ↑S
t : R
ht : t ∈ ↑J
ht' : t ∈ ↑S
⊢ P * P ⊔ Ideal.span {x} * P ⊔ (P * Ideal.span {y} ⊔ Ideal.span {x * y}) ≤ P

State before:
R : Type u_1
inst✝ : CommSemiring R
P : Ideal R
S : Subsemigroup R
x y : R
hP : P ∈ Kaplansky.set S
hmax : ∀ I ∈ Kaplansky.set S, P ≤ I → I = P
hxy : x * y ∈ P
h' : x ∉ P
h'' : y ∉ P
I : Ideal R := P ⊔ Ideal.span {x}
J : Ideal R := P ⊔ Ideal.span {y}
s : R
hs : s ∈ ↑I
hs' : s ∈ ↑S
t : R
ht : t ∈ ↑J
ht' : t ∈ ↑S
⊢ P * P ⊔ Ideal.span {x} * P ⊔ (P * Ideal.span {y} ⊔ Ideal.span {x * y}) ≤ P
Tactic:
exact
  sup_le (sup_le Ideal.mul_le_right Ideal.mul_le_left)
    (sup_le Ideal.mul_le_right (P.span_singleton_le_iff_mem.2 hxy))
State after:
no goals