internlm/Lean-Github huggingface dataset:
Theorem: ideal_neq_top
Proof state before:
case intro
R : Type u_1
inst✝ : Semiring R
S : Subsemigroup R
P : Ideal R
hP : ∀ (x : R), x ∉ ↑⊤ ∩ ↑S
h : P = ⊤
x : R
h₂ : x ∈ ↑S
⊢ False
Tactic:
specialize hP x
Proof state after:
case intro
R : Type u_1
inst✝ : Semiring R
S : Subsemigroup R
P : Ideal R
h : P = ⊤
x : R
h₂ : x ∈ ↑S
hP : x ∉ ↑⊤ ∩ ↑S
⊢ False
Theorem: ideal_neq_top
Proof state before:
case intro
R : Type u_1
inst✝ : Semiring R
S : Subsemigroup R
P : Ideal R
h : P = ⊤
x : R
h₂ : x ∈ ↑S
hP : x ∉ ↑⊤ ∩ ↑S
⊢ False
Tactic:
apply hP
Proof state after:
case intro
R : Type u_1
inst✝ : Semiring R
S : Subsemigroup R
P : Ideal R
h : P = ⊤
x : R
h₂ : x ∈ ↑S
hP : x ∉ ↑⊤ ∩ ↑S
⊢ x ∈ ↑⊤ ∩ ↑S
Theorem: ideal_neq_top
Proof state before:
case intro
R : Type u_1
inst✝ : Semiring R
S : Subsemigroup R
P : Ideal R
h : P = ⊤
x : R
h₂ : x ∈ ↑S
hP : x ∉ ↑⊤ ∩ ↑S
⊢ x ∈ ↑⊤ ∩ ↑S
Tactic:
exact (Set.mem_inter (Set.mem_univ x) h₂)
Proof state after:
no goals
Theorem: mem_or_mem_of_mul_mem
Proof 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
Proof 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
Theorem: mem_or_mem_of_mul_mem
Proof 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
Proof 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
Theorem: mem_or_mem_of_mul_mem
Proof 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
Proof 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
Theorem: mem_or_mem_of_mul_mem
Proof 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''
Proof 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
Theorem: mem_or_mem_of_mul_mem
Proof 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}
Proof 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
Theorem: mem_or_mem_of_mul_mem
Proof 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}
Proof 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
Theorem: mem_or_mem_of_mul_mem
Proof 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
Proof 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
Theorem: mem_or_mem_of_mul_mem
Proof 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
Proof 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
Theorem: mem_or_mem_of_mul_mem
Proof 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'⟩⟩⟩
Proof 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
Theorem: mem_or_mem_of_mul_mem
Proof 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))
Proof 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
Theorem: mem_or_mem_of_mul_mem
Proof 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'⟩
Proof state after:
no goals
Theorem: mem_or_mem_of_mul_mem
Proof 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 _)
Proof 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
Theorem: mem_or_mem_of_mul_mem
Proof 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
Proof 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
Theorem: mem_or_mem_of_mul_mem
Proof 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'
Proof 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
Theorem: mem_or_mem_of_mul_mem
Proof 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
Proof state after:
no goals
Theorem: mem_or_mem_of_mul_mem
Proof 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 _)
Proof 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
Theorem: mem_or_mem_of_mul_mem
Proof 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
Proof 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
Theorem: mem_or_mem_of_mul_mem
Proof 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''
Proof 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
Theorem: mem_or_mem_of_mul_mem
Proof 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
Proof state after:
no goals
Theorem: mem_or_mem_of_mul_mem
Proof 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]
Proof 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
Theorem: mem_or_mem_of_mul_mem
Proof 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))
Proof state after:
no goals
Theorem: Submonoid.closure_mem_of_prod_mem
Proof state before:
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
⊢ ∀ (x y : R), x * y ∈ closure {r | IsUnit r ∨ Prime r} → x ∈ closure {r | IsUnit r ∨ Prime r}
Tactic:
intros a b hab
Proof state after:
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
a b : R
hab : a * b ∈ closure {r | IsUnit r ∨ Prime r}
⊢ a ∈ closure {r | IsUnit r ∨ Prime r}
Theorem: Submonoid.closure_mem_of_prod_mem
Proof state before:
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
a b : R
hab : a * b ∈ closure {r | IsUnit r ∨ Prime r}
⊢ a ∈ closure {r | IsUnit r ∨ Prime r}
Tactic:
obtain ⟨m, hm⟩ := exists_multiset_of_mem_closure hab
Proof state after:
case intro
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
a b : R
hab : a * b ∈ closure {r | IsUnit r ∨ Prime r}
m : Multiset R
hm : ∃ (_ : ∀ y ∈ m, y ∈ {r | IsUnit r ∨ Prime r}), Multiset.prod m = a * b
⊢ a ∈ closure {r | IsUnit r ∨ Prime r}
Theorem: Submonoid.closure_mem_of_prod_mem
Proof state before:
case intro
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
a b : R
hab : a * b ∈ closure {r | IsUnit r ∨ Prime r}
m : Multiset R
hm : ∃ (_ : ∀ y ∈ m, y ∈ {r | IsUnit r ∨ Prime r}), Multiset.prod m = a * b
⊢ a ∈ closure {r | IsUnit r ∨ Prime r}
Tactic:
revert a b hm
Proof state after:
case intro
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
⊢ ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∃ (_ : ∀ y ∈ m, y ∈ {r | IsUnit r ∨ Prime r}), Multiset.prod m = a * b) → a ∈ closure {r | IsUnit r ∨ Prime r}
Theorem: Submonoid.closure_mem_of_prod_mem
Proof state before:
case intro
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
⊢ ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∃ (_ : ∀ y ∈ m, y ∈ {r | IsUnit r ∨ Prime r}), Multiset.prod m = a * b) → a ∈ closure {r | IsUnit r ∨ Prime r}
Tactic:
refine m.induction (p := fun m ↦ ∀ a b, a * b ∈ closure {r | IsUnit r ∨ Prime r} →
  (∃ (_ : ∀ y ∈ m, y ∈ {r | IsUnit r ∨ Prime r}), m.prod = a * b) →
  a ∈ closure {r | IsUnit r ∨ Prime r}) (fun _ _ _ hprod => subset_closure (Set.mem_def.2 ?_)) ?_
Proof state after:
case intro.refine_1
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
x✝² x✝¹ : R
x✝ : x✝² * x✝¹ ∈ closure {r | IsUnit r ∨ Prime r}
hprod : ∃ (_ : ∀ y ∈ 0, y ∈ {r | IsUnit r ∨ Prime r}), Multiset.prod 0 = x✝² * x✝¹
⊢ {r | IsUnit r ∨ Prime r} x✝²

case intro.refine_2
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
⊢ ∀ ⦃a : R⦄ {s : Multiset R},
    (fun m =>
          ∀ (a b : R),
            a * b ∈ closure {r | IsUnit r ∨ Prime r} →
              (∃ (_ : ∀ y ∈ m, y ∈ {r | IsUnit r ∨ Prime r}), Multiset.prod m = a * b) →
                a ∈ closure {r | IsUnit r ∨ Prime r})
        s →
      (fun m =>
          ∀ (a b : R),
            a * b ∈ closure {r | IsUnit r ∨ Prime r} →
              (∃ (_ : ∀ y ∈ m, y ∈ {r | IsUnit r ∨ Prime r}), Multiset.prod m = a * b) →
                a ∈ closure {r | IsUnit r ∨ Prime r})
        (a ::ₘ s)
Theorem: Submonoid.closure_mem_of_prod_mem
Proof state before:
case intro.refine_1
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
x✝² x✝¹ : R
x✝ : x✝² * x✝¹ ∈ closure {r | IsUnit r ∨ Prime r}
hprod : ∃ (_ : ∀ y ∈ 0, y ∈ {r | IsUnit r ∨ Prime r}), Multiset.prod 0 = x✝² * x✝¹
⊢ {r | IsUnit r ∨ Prime r} x✝²
Tactic:
left
Proof state after:
case intro.refine_1.h
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
x✝² x✝¹ : R
x✝ : x✝² * x✝¹ ∈ closure {r | IsUnit r ∨ Prime r}
hprod : ∃ (_ : ∀ y ∈ 0, y ∈ {r | IsUnit r ∨ Prime r}), Multiset.prod 0 = x✝² * x✝¹
⊢ IsUnit x✝²
Theorem: Submonoid.closure_mem_of_prod_mem
Proof state before:
case intro.refine_1.h
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
x✝² x✝¹ : R
x✝ : x✝² * x✝¹ ∈ closure {r | IsUnit r ∨ Prime r}
hprod : ∃ (_ : ∀ y ∈ 0, y ∈ {r | IsUnit r ∨ Prime r}), Multiset.prod 0 = x✝² * x✝¹
⊢ IsUnit x✝²
Tactic:
exact isUnit_of_mul_eq_one _ _ hprod.2.symm
Proof state after:
no goals
Theorem: Submonoid.closure_mem_of_prod_mem
Proof state before:
case intro.refine_2
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
⊢ ∀ ⦃a : R⦄ {s : Multiset R},
    (fun m =>
          ∀ (a b : R),
            a * b ∈ closure {r | IsUnit r ∨ Prime r} →
              (∃ (_ : ∀ y ∈ m, y ∈ {r | IsUnit r ∨ Prime r}), Multiset.prod m = a * b) →
                a ∈ closure {r | IsUnit r ∨ Prime r})
        s →
      (fun m =>
          ∀ (a b : R),
            a * b ∈ closure {r | IsUnit r ∨ Prime r} →
              (∃ (_ : ∀ y ∈ m, y ∈ {r | IsUnit r ∨ Prime r}), Multiset.prod m = a * b) →
                a ∈ closure {r | IsUnit r ∨ Prime r})
        (a ::ₘ s)
Tactic:
simp only [exists_prop, and_imp, Multiset.prod_cons, Multiset.mem_cons, forall_eq_or_imp]
Proof state after:
case intro.refine_2
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
⊢ ∀ ⦃a : R⦄ {s : Multiset R},
    (∀ (a b : R),
        a * b ∈ closure {r | IsUnit r ∨ Prime r} →
          (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}) →
      ∀ (a_2 b : R),
        a_2 * b ∈ closure {r | IsUnit r ∨ Prime r} →
          a ∈ {r | IsUnit r ∨ Prime r} →
            (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) →
              a * Multiset.prod s = a_2 * b → a_2 ∈ closure {r | IsUnit r ∨ Prime r}
Theorem: Submonoid.closure_mem_of_prod_mem
Proof state before:
case intro.refine_2
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
⊢ ∀ ⦃a : R⦄ {s : Multiset R},
    (∀ (a b : R),
        a * b ∈ closure {r | IsUnit r ∨ Prime r} →
          (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}) →
      ∀ (a_2 b : R),
        a_2 * b ∈ closure {r | IsUnit r ∨ Prime r} →
          a ∈ {r | IsUnit r ∨ Prime r} →
            (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) →
              a * Multiset.prod s = a_2 * b → a_2 ∈ closure {r | IsUnit r ∨ Prime r}
Tactic:
intros _ s hind x y _ ha hs hprod
Proof state after:
case intro.refine_2
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
a✝¹ : R
s : Multiset R
hind :
  ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}
x y : R
a✝ : x * y ∈ closure {r | IsUnit r ∨ Prime r}
ha : a✝¹ ∈ {r | IsUnit r ∨ Prime r}
hs : ∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}
hprod : a✝¹ * Multiset.prod s = x * y
⊢ x ∈ closure {r | IsUnit r ∨ Prime r}
Theorem: Submonoid.closure_mem_of_prod_mem
Proof state before:
case intro.refine_2
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
a✝¹ : R
s : Multiset R
hind :
  ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}
x y : R
a✝ : x * y ∈ closure {r | IsUnit r ∨ Prime r}
ha : a✝¹ ∈ {r | IsUnit r ∨ Prime r}
hs : ∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}
hprod : a✝¹ * Multiset.prod s = x * y
⊢ x ∈ closure {r | IsUnit r ∨ Prime r}
Tactic:
rcases ha with ha₁ | ha₂
Proof state after:
case intro.refine_2.inl
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
a✝¹ : R
s : Multiset R
hind :
  ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}
x y : R
a✝ : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}
hprod : a✝¹ * Multiset.prod s = x * y
ha₁ : IsUnit a✝¹
⊢ x ∈ closure {r | IsUnit r ∨ Prime r}

case intro.refine_2.inr
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
a✝¹ : R
s : Multiset R
hind :
  ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}
x y : R
a✝ : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}
hprod : a✝¹ * Multiset.prod s = x * y
ha₂ : Prime a✝¹
⊢ x ∈ closure {r | IsUnit r ∨ Prime r}
Theorem: Submonoid.closure_mem_of_prod_mem
Proof state before:
case intro.refine_2.inl
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
a✝¹ : R
s : Multiset R
hind :
  ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}
x y : R
a✝ : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}
hprod : a✝¹ * Multiset.prod s = x * y
ha₁ : IsUnit a✝¹
⊢ x ∈ closure {r | IsUnit r ∨ Prime r}
Tactic:
rcases ha₁.exists_right_inv with ⟨k, hk⟩
Proof state after:
case intro.refine_2.inl.intro
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
a✝¹ : R
s : Multiset R
hind :
  ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}
x y : R
a✝ : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}
hprod : a✝¹ * Multiset.prod s = x * y
ha₁ : IsUnit a✝¹
k : R
hk : a✝¹ * k = 1
⊢ x ∈ closure {r | IsUnit r ∨ Prime r}