internlm/Lean-Github huggingface dataset:
Theorem: Subsemigroup.submonoid.powers_absorbing
Proof state before:
M : Type ?u.8793
N : Type ?u.8796
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
hp : Prime p
⊢ ProdProperty (Submonoid.powers p).toSubsemigroup
Tactic:
rintro x y hxy
Proof state after:
M : Type ?u.8793
N : Type ?u.8796
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
hp : Prime p
x y : R
hxy : x * y ∈ (Submonoid.powers p).toSubsemigroup
⊢ (∃ z ∈ (Submonoid.powers p).toSubsemigroup, Associated x z) ∧
    ∃ z ∈ (Submonoid.powers p).toSubsemigroup, Associated y z
Theorem: Subsemigroup.submonoid.powers_absorbing
Proof state before:
M : Type ?u.8793
N : Type ?u.8796
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
hp : Prime p
x y : R
hxy : x * y ∈ (Submonoid.powers p).toSubsemigroup
⊢ (∃ z ∈ (Submonoid.powers p).toSubsemigroup, Associated x z) ∧
    ∃ z ∈ (Submonoid.powers p).toSubsemigroup, Associated y z
Tactic:
cases' ((Submonoid.mem_powers_iff _ _).1 hxy) with m hm
Proof state after:
case intro
M : Type ?u.8793
N : Type ?u.8796
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
hp : Prime p
x y : R
hxy : x * y ∈ (Submonoid.powers p).toSubsemigroup
m : ℕ
hm : p ^ m = x * y
⊢ (∃ z ∈ (Submonoid.powers p).toSubsemigroup, Associated x z) ∧
    ∃ z ∈ (Submonoid.powers p).toSubsemigroup, Associated y z
Theorem: Subsemigroup.submonoid.powers_absorbing
Proof state before:
case intro
M : Type ?u.8793
N : Type ?u.8796
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
hp : Prime p
x y : R
hxy : x * y ∈ (Submonoid.powers p).toSubsemigroup
m : ℕ
hm : p ^ m = x * y
⊢ (∃ z ∈ (Submonoid.powers p).toSubsemigroup, Associated x z) ∧
    ∃ z ∈ (Submonoid.powers p).toSubsemigroup, Associated y z
Tactic:
rw [← one_mul (p^m)] at hm
Proof state after:
case intro
M : Type ?u.8793
N : Type ?u.8796
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
hp : Prime p
x y : R
hxy : x * y ∈ (Submonoid.powers p).toSubsemigroup
m : ℕ
hm : 1 * p ^ m = x * y
⊢ (∃ z ∈ (Submonoid.powers p).toSubsemigroup, Associated x z) ∧
    ∃ z ∈ (Submonoid.powers p).toSubsemigroup, Associated y z
Theorem: Subsemigroup.submonoid.powers_absorbing
Proof state before:
case intro
M : Type ?u.8793
N : Type ?u.8796
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
hp : Prime p
x y : R
hxy : x * y ∈ (Submonoid.powers p).toSubsemigroup
m : ℕ
hm : 1 * p ^ m = x * y
⊢ (∃ z ∈ (Submonoid.powers p).toSubsemigroup, Associated x z) ∧
    ∃ z ∈ (Submonoid.powers p).toSubsemigroup, Associated y z
Tactic:
rcases (mul_eq_mul_prime_pow hp hm.symm) with ⟨i, j, _, _, ⟨_, hbc, hx, hy⟩⟩
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro
M : Type ?u.8793
N : Type ?u.8796
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
hp : Prime p
x y : R
hxy : x * y ∈ (Submonoid.powers p).toSubsemigroup
m : ℕ
hm : 1 * p ^ m = x * y
i j : ℕ
w✝¹ w✝ : R
left✝ : i + j = m
hbc : 1 = w✝¹ * w✝
hx : x = w✝¹ * p ^ i
hy : y = w✝ * p ^ j
⊢ (∃ z ∈ (Submonoid.powers p).toSubsemigroup, Associated x z) ∧
    ∃ z ∈ (Submonoid.powers p).toSubsemigroup, Associated y z
Theorem: Subsemigroup.submonoid.powers_absorbing
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro
M : Type ?u.8793
N : Type ?u.8796
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
hp : Prime p
x y : R
hxy : x * y ∈ (Submonoid.powers p).toSubsemigroup
m : ℕ
hm : 1 * p ^ m = x * y
i j : ℕ
w✝¹ w✝ : R
left✝ : i + j = m
hbc : 1 = w✝¹ * w✝
hx : x = w✝¹ * p ^ i
hy : y = w✝ * p ^ j
⊢ (∃ z ∈ (Submonoid.powers p).toSubsemigroup, Associated x z) ∧
    ∃ z ∈ (Submonoid.powers p).toSubsemigroup, Associated y z
Tactic:
rw [hx, hy]
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro
M : Type ?u.8793
N : Type ?u.8796
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
hp : Prime p
x y : R
hxy : x * y ∈ (Submonoid.powers p).toSubsemigroup
m : ℕ
hm : 1 * p ^ m = x * y
i j : ℕ
w✝¹ w✝ : R
left✝ : i + j = m
hbc : 1 = w✝¹ * w✝
hx : x = w✝¹ * p ^ i
hy : y = w✝ * p ^ j
⊢ (∃ z ∈ (Submonoid.powers p).toSubsemigroup, Associated (w✝¹ * p ^ i) z) ∧
    ∃ z ∈ (Submonoid.powers p).toSubsemigroup, Associated (w✝ * p ^ j) z
Theorem: Subsemigroup.submonoid.powers_absorbing
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro
M : Type ?u.8793
N : Type ?u.8796
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
hp : Prime p
x y : R
hxy : x * y ∈ (Submonoid.powers p).toSubsemigroup
m : ℕ
hm : 1 * p ^ m = x * y
i j : ℕ
w✝¹ w✝ : R
left✝ : i + j = m
hbc : 1 = w✝¹ * w✝
hx : x = w✝¹ * p ^ i
hy : y = w✝ * p ^ j
⊢ (∃ z ∈ (Submonoid.powers p).toSubsemigroup, Associated (w✝¹ * p ^ i) z) ∧
    ∃ z ∈ (Submonoid.powers p).toSubsemigroup, Associated (w✝ * p ^ j) z
Tactic:
refine' ⟨⟨p^i, (Submonoid.mem_powers_iff _ _).2 ⟨i, rfl⟩,
  (associated_isUnit_mul_left_iff (isUnit_of_mul_eq_one _ _ hbc.symm)).2 (Associated.refl (p^i))⟩,
    p^j, (Submonoid.mem_powers_iff _ _).2 ⟨j, rfl⟩, _⟩
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro
M : Type ?u.8793
N : Type ?u.8796
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
hp : Prime p
x y : R
hxy : x * y ∈ (Submonoid.powers p).toSubsemigroup
m : ℕ
hm : 1 * p ^ m = x * y
i j : ℕ
w✝¹ w✝ : R
left✝ : i + j = m
hbc : 1 = w✝¹ * w✝
hx : x = w✝¹ * p ^ i
hy : y = w✝ * p ^ j
⊢ Associated (w✝ * p ^ j) (p ^ j)
Theorem: Subsemigroup.submonoid.powers_absorbing
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro
M : Type ?u.8793
N : Type ?u.8796
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
hp : Prime p
x y : R
hxy : x * y ∈ (Submonoid.powers p).toSubsemigroup
m : ℕ
hm : 1 * p ^ m = x * y
i j : ℕ
w✝¹ w✝ : R
left✝ : i + j = m
hbc : 1 = w✝¹ * w✝
hx : x = w✝¹ * p ^ i
hy : y = w✝ * p ^ j
⊢ Associated (w✝ * p ^ j) (p ^ j)
Tactic:
rw [mul_comm] at hbc
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro
M : Type ?u.8793
N : Type ?u.8796
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
hp : Prime p
x y : R
hxy : x * y ∈ (Submonoid.powers p).toSubsemigroup
m : ℕ
hm : 1 * p ^ m = x * y
i j : ℕ
w✝¹ w✝ : R
left✝ : i + j = m
hbc : 1 = w✝ * w✝¹
hx : x = w✝¹ * p ^ i
hy : y = w✝ * p ^ j
⊢ Associated (w✝ * p ^ j) (p ^ j)
Theorem: Subsemigroup.submonoid.powers_absorbing
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro
M : Type ?u.8793
N : Type ?u.8796
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
hp : Prime p
x y : R
hxy : x * y ∈ (Submonoid.powers p).toSubsemigroup
m : ℕ
hm : 1 * p ^ m = x * y
i j : ℕ
w✝¹ w✝ : R
left✝ : i + j = m
hbc : 1 = w✝ * w✝¹
hx : x = w✝¹ * p ^ i
hy : y = w✝ * p ^ j
⊢ Associated (w✝ * p ^ j) (p ^ j)
Tactic:
exact (associated_isUnit_mul_left_iff (isUnit_of_mul_eq_one _ _ hbc.symm)).2
  (Associated.refl (p^j))
Proof state after:
no goals
Theorem: Subsemigroup.prodProperty_iff_of_comm
Proof state before:
M : Type u_1
N : Type ?u.11134
inst✝ : CommMonoid M
S : Subsemigroup M
h : ∀ (x y : M), x * y ∈ S → ∃ z ∈ S, Associated x z
x y : M
hxy : x * y ∈ S
⊢ y * x ∈ S
Tactic:
rwa [mul_comm] at hxy
Proof state after:
no goals
Theorem: Submonoid.bot_prodProperty
Proof state before:
M : Type u_1
N : Type ?u.12181
inst✝ : CommMonoid M
x✝¹ x✝ : M
hxy : x✝¹ * x✝ ∈ ⊥.toSubsemigroup
⊢ x✝ * ?m.13325 x✝¹ x✝ hxy = 1
Tactic:
rwa [mul_comm] at hxy
Proof state after:
no goals
Theorem: Submonoid.fst_prodProperty
Proof state before:
M : Type u_1
N : Type u_2
inst✝¹ : Monoid M
inst✝ : Monoid N
s : Submonoid M
t : Submonoid N
⊢ Subsemigroup.ProdProperty (prod s t).toSubsemigroup → Subsemigroup.ProdProperty s.toSubsemigroup
Tactic:
rintro h x y hxy
Proof state after:
M : Type u_1
N : Type u_2
inst✝¹ : Monoid M
inst✝ : Monoid N
s : Submonoid M
t : Submonoid N
h : Subsemigroup.ProdProperty (prod s t).toSubsemigroup
x y : M
hxy : x * y ∈ s.toSubsemigroup
⊢ (∃ z ∈ s.toSubsemigroup, Associated x z) ∧ ∃ z ∈ s.toSubsemigroup, Associated y z
Theorem: Submonoid.fst_prodProperty
Proof state before:
M : Type u_1
N : Type u_2
inst✝¹ : Monoid M
inst✝ : Monoid N
s : Submonoid M
t : Submonoid N
h : Subsemigroup.ProdProperty (prod s t).toSubsemigroup
x y : M
hxy : x * y ∈ s.toSubsemigroup
⊢ (∃ z ∈ s.toSubsemigroup, Associated x z) ∧ ∃ z ∈ s.toSubsemigroup, Associated y z
Tactic:
specialize h (x, 1) (y, 1)
Proof state after:
M : Type u_1
N : Type u_2
inst✝¹ : Monoid M
inst✝ : Monoid N
s : Submonoid M
t : Submonoid N
x y : M
hxy : x * y ∈ s.toSubsemigroup
h :
  (x, 1) * (y, 1) ∈ (prod s t).toSubsemigroup →
    (∃ z ∈ (prod s t).toSubsemigroup, Associated (x, 1) z) ∧ ∃ z ∈ (prod s t).toSubsemigroup, Associated (y, 1) z
⊢ (∃ z ∈ s.toSubsemigroup, Associated x z) ∧ ∃ z ∈ s.toSubsemigroup, Associated y z
Theorem: Submonoid.fst_prodProperty
Proof state before:
M : Type u_1
N : Type u_2
inst✝¹ : Monoid M
inst✝ : Monoid N
s : Submonoid M
t : Submonoid N
x y : M
hxy : x * y ∈ s.toSubsemigroup
h :
  (x, 1) * (y, 1) ∈ (prod s t).toSubsemigroup →
    (∃ z ∈ (prod s t).toSubsemigroup, Associated (x, 1) z) ∧ ∃ z ∈ (prod s t).toSubsemigroup, Associated (y, 1) z
⊢ (∃ z ∈ s.toSubsemigroup, Associated x z) ∧ ∃ z ∈ s.toSubsemigroup, Associated y z
Tactic:
rw [Prod.mk_one_mul_mk_one] at h
Proof state after:
M : Type u_1
N : Type u_2
inst✝¹ : Monoid M
inst✝ : Monoid N
s : Submonoid M
t : Submonoid N
x y : M
hxy : x * y ∈ s.toSubsemigroup
h :
  (x * y, 1) ∈ (prod s t).toSubsemigroup →
    (∃ z ∈ (prod s t).toSubsemigroup, Associated (x, 1) z) ∧ ∃ z ∈ (prod s t).toSubsemigroup, Associated (y, 1) z
⊢ (∃ z ∈ s.toSubsemigroup, Associated x z) ∧ ∃ z ∈ s.toSubsemigroup, Associated y z
Theorem: Submonoid.fst_prodProperty
Proof state before:
M : Type u_1
N : Type u_2
inst✝¹ : Monoid M
inst✝ : Monoid N
s : Submonoid M
t : Submonoid N
x y : M
hxy : x * y ∈ s.toSubsemigroup
h :
  (x * y, 1) ∈ (prod s t).toSubsemigroup →
    (∃ z ∈ (prod s t).toSubsemigroup, Associated (x, 1) z) ∧ ∃ z ∈ (prod s t).toSubsemigroup, Associated (y, 1) z
⊢ (∃ z ∈ s.toSubsemigroup, Associated x z) ∧ ∃ z ∈ s.toSubsemigroup, Associated y z
Tactic:
obtain ⟨⟨a, ha, ha₂⟩, b, hb, hb₂⟩ := h (Submonoid.mem_prod.2 ⟨hxy, t.one_mem⟩)
Proof state after:
case intro.intro.intro.intro.intro
M : Type u_1
N : Type u_2
inst✝¹ : Monoid M
inst✝ : Monoid N
s : Submonoid M
t : Submonoid N
x y : M
hxy : x * y ∈ s.toSubsemigroup
h :
  (x * y, 1) ∈ (prod s t).toSubsemigroup →
    (∃ z ∈ (prod s t).toSubsemigroup, Associated (x, 1) z) ∧ ∃ z ∈ (prod s t).toSubsemigroup, Associated (y, 1) z
a : M × N
ha : a ∈ (prod s t).toSubsemigroup
ha₂ : Associated (x, 1) a
b : M × N
hb : b ∈ (prod s t).toSubsemigroup
hb₂ : Associated (y, 1) b
⊢ (∃ z ∈ s.toSubsemigroup, Associated x z) ∧ ∃ z ∈ s.toSubsemigroup, Associated y z
Theorem: Submonoid.fst_prodProperty
Proof state before:
case intro.intro.intro.intro.intro
M : Type u_1
N : Type u_2
inst✝¹ : Monoid M
inst✝ : Monoid N
s : Submonoid M
t : Submonoid N
x y : M
hxy : x * y ∈ s.toSubsemigroup
h :
  (x * y, 1) ∈ (prod s t).toSubsemigroup →
    (∃ z ∈ (prod s t).toSubsemigroup, Associated (x, 1) z) ∧ ∃ z ∈ (prod s t).toSubsemigroup, Associated (y, 1) z
a : M × N
ha : a ∈ (prod s t).toSubsemigroup
ha₂ : Associated (x, 1) a
b : M × N
hb : b ∈ (prod s t).toSubsemigroup
hb₂ : Associated (y, 1) b
⊢ (∃ z ∈ s.toSubsemigroup, Associated x z) ∧ ∃ z ∈ s.toSubsemigroup, Associated y z
Tactic:
exact ⟨⟨a.1, (Submonoid.mem_prod.1 ha).1, (Subsemigroup.Prod.associated_iff.1 ha₂).1⟩, b.1,
  (Submonoid.mem_prod.1 hb).1, (Subsemigroup.Prod.associated_iff.1 hb₂).1⟩
Proof state after:
no goals
Theorem: Submonoid.snd_prodProperty
Proof state before:
M : Type u_1
N : Type u_2
inst✝¹ : Monoid M
inst✝ : Monoid N
s : Submonoid M
t : Submonoid N
⊢ Subsemigroup.ProdProperty (prod s t).toSubsemigroup → Subsemigroup.ProdProperty t.toSubsemigroup
Tactic:
rintro h x y hxy
Proof state after:
M : Type u_1
N : Type u_2
inst✝¹ : Monoid M
inst✝ : Monoid N
s : Submonoid M
t : Submonoid N
h : Subsemigroup.ProdProperty (prod s t).toSubsemigroup
x y : N
hxy : x * y ∈ t.toSubsemigroup
⊢ (∃ z ∈ t.toSubsemigroup, Associated x z) ∧ ∃ z ∈ t.toSubsemigroup, Associated y z
Theorem: Submonoid.snd_prodProperty
Proof state before:
M : Type u_1
N : Type u_2
inst✝¹ : Monoid M
inst✝ : Monoid N
s : Submonoid M
t : Submonoid N
h : Subsemigroup.ProdProperty (prod s t).toSubsemigroup
x y : N
hxy : x * y ∈ t.toSubsemigroup
⊢ (∃ z ∈ t.toSubsemigroup, Associated x z) ∧ ∃ z ∈ t.toSubsemigroup, Associated y z
Tactic:
specialize h (1, x) (1, y)
Proof state after:
M : Type u_1
N : Type u_2
inst✝¹ : Monoid M
inst✝ : Monoid N
s : Submonoid M
t : Submonoid N
x y : N
hxy : x * y ∈ t.toSubsemigroup
h :
  (1, x) * (1, y) ∈ (prod s t).toSubsemigroup →
    (∃ z ∈ (prod s t).toSubsemigroup, Associated (1, x) z) ∧ ∃ z ∈ (prod s t).toSubsemigroup, Associated (1, y) z
⊢ (∃ z ∈ t.toSubsemigroup, Associated x z) ∧ ∃ z ∈ t.toSubsemigroup, Associated y z
Theorem: Submonoid.snd_prodProperty
Proof state before:
M : Type u_1
N : Type u_2
inst✝¹ : Monoid M
inst✝ : Monoid N
s : Submonoid M
t : Submonoid N
x y : N
hxy : x * y ∈ t.toSubsemigroup
h :
  (1, x) * (1, y) ∈ (prod s t).toSubsemigroup →
    (∃ z ∈ (prod s t).toSubsemigroup, Associated (1, x) z) ∧ ∃ z ∈ (prod s t).toSubsemigroup, Associated (1, y) z
⊢ (∃ z ∈ t.toSubsemigroup, Associated x z) ∧ ∃ z ∈ t.toSubsemigroup, Associated y z
Tactic:
rw [Prod.one_mk_mul_one_mk] at h
Proof state after:
M : Type u_1
N : Type u_2
inst✝¹ : Monoid M
inst✝ : Monoid N
s : Submonoid M
t : Submonoid N
x y : N
hxy : x * y ∈ t.toSubsemigroup
h :
  (1, x * y) ∈ (prod s t).toSubsemigroup →
    (∃ z ∈ (prod s t).toSubsemigroup, Associated (1, x) z) ∧ ∃ z ∈ (prod s t).toSubsemigroup, Associated (1, y) z
⊢ (∃ z ∈ t.toSubsemigroup, Associated x z) ∧ ∃ z ∈ t.toSubsemigroup, Associated y z
Theorem: Submonoid.snd_prodProperty
Proof state before:
M : Type u_1
N : Type u_2
inst✝¹ : Monoid M
inst✝ : Monoid N
s : Submonoid M
t : Submonoid N
x y : N
hxy : x * y ∈ t.toSubsemigroup
h :
  (1, x * y) ∈ (prod s t).toSubsemigroup →
    (∃ z ∈ (prod s t).toSubsemigroup, Associated (1, x) z) ∧ ∃ z ∈ (prod s t).toSubsemigroup, Associated (1, y) z
⊢ (∃ z ∈ t.toSubsemigroup, Associated x z) ∧ ∃ z ∈ t.toSubsemigroup, Associated y z
Tactic:
obtain ⟨⟨a, ha, ha₂⟩, b, hb, hb₂⟩ := h (Submonoid.mem_prod.2 ⟨s.one_mem, hxy⟩)
Proof state after:
case intro.intro.intro.intro.intro
M : Type u_1
N : Type u_2
inst✝¹ : Monoid M
inst✝ : Monoid N
s : Submonoid M
t : Submonoid N
x y : N
hxy : x * y ∈ t.toSubsemigroup
h :
  (1, x * y) ∈ (prod s t).toSubsemigroup →
    (∃ z ∈ (prod s t).toSubsemigroup, Associated (1, x) z) ∧ ∃ z ∈ (prod s t).toSubsemigroup, Associated (1, y) z
a : M × N
ha : a ∈ (prod s t).toSubsemigroup
ha₂ : Associated (1, x) a
b : M × N
hb : b ∈ (prod s t).toSubsemigroup
hb₂ : Associated (1, y) b
⊢ (∃ z ∈ t.toSubsemigroup, Associated x z) ∧ ∃ z ∈ t.toSubsemigroup, Associated y z
Theorem: Submonoid.snd_prodProperty
Proof state before:
case intro.intro.intro.intro.intro
M : Type u_1
N : Type u_2
inst✝¹ : Monoid M
inst✝ : Monoid N
s : Submonoid M
t : Submonoid N
x y : N
hxy : x * y ∈ t.toSubsemigroup
h :
  (1, x * y) ∈ (prod s t).toSubsemigroup →
    (∃ z ∈ (prod s t).toSubsemigroup, Associated (1, x) z) ∧ ∃ z ∈ (prod s t).toSubsemigroup, Associated (1, y) z
a : M × N
ha : a ∈ (prod s t).toSubsemigroup
ha₂ : Associated (1, x) a
b : M × N
hb : b ∈ (prod s t).toSubsemigroup
hb₂ : Associated (1, y) b
⊢ (∃ z ∈ t.toSubsemigroup, Associated x z) ∧ ∃ z ∈ t.toSubsemigroup, Associated y z
Tactic:
exact ⟨⟨a.2, (Submonoid.mem_prod.1 ha).2, (Subsemigroup.Prod.associated_iff.1 ha₂).2⟩, b.2,
  (Submonoid.mem_prod.1 hb).2, (Subsemigroup.Prod.associated_iff.1 hb₂).2⟩
Proof state after:
no goals
Theorem: hypothesis_zorn_lemma
Proof state before:
R : Type u_1
inst✝ : Semiring R
S : Subsemigroup R
hS : 0 ∉ S
C : Set (Ideal R)
hC : C ⊆ Kaplansky.set S
hC₂ : IsChain (fun x x_1 => x ≤ x_1) C
⊢ ∃ P ∈ Kaplansky.set S, ∀ J ∈ C, J ≤ P
Tactic:
by_cases h : C.Nonempty
Proof state after:
case pos
R : Type u_1
inst✝ : Semiring R
S : Subsemigroup R
hS : 0 ∉ S
C : Set (Ideal R)
hC : C ⊆ Kaplansky.set S
hC₂ : IsChain (fun x x_1 => x ≤ x_1) C
h : Set.Nonempty C
⊢ ∃ P ∈ Kaplansky.set S, ∀ J ∈ C, J ≤ P

case neg
R : Type u_1
inst✝ : Semiring R
S : Subsemigroup R
hS : 0 ∉ S
C : Set (Ideal R)
hC : C ⊆ Kaplansky.set S
hC₂ : IsChain (fun x x_1 => x ≤ x_1) C
h : ¬Set.Nonempty C
⊢ ∃ P ∈ Kaplansky.set S, ∀ J ∈ C, J ≤ P
Theorem: hypothesis_zorn_lemma
Proof state before:
case pos
R : Type u_1
inst✝ : Semiring R
S : Subsemigroup R
hS : 0 ∉ S
C : Set (Ideal R)
hC : C ⊆ Kaplansky.set S
hC₂ : IsChain (fun x x_1 => x ≤ x_1) C
h : Set.Nonempty C
⊢ ∃ P ∈ Kaplansky.set S, ∀ J ∈ C, J ≤ P
Tactic:
cases' (Set.nonempty_def.1 h) with I hI
Proof state after:
case pos.intro
R : Type u_1
inst✝ : Semiring R
S : Subsemigroup R
hS : 0 ∉ S
C : Set (Ideal R)
hC : C ⊆ Kaplansky.set S
hC₂ : IsChain (fun x x_1 => x ≤ x_1) C
h : Set.Nonempty C
I : Ideal R
hI : I ∈ C
⊢ ∃ P ∈ Kaplansky.set S, ∀ J ∈ C, J ≤ P
Theorem: hypothesis_zorn_lemma
Proof state before:
case pos.intro
R : Type u_1
inst✝ : Semiring R
S : Subsemigroup R
hS : 0 ∉ S
C : Set (Ideal R)
hC : C ⊆ Kaplansky.set S
hC₂ : IsChain (fun x x_1 => x ≤ x_1) C
h : Set.Nonempty C
I : Ideal R
hI : I ∈ C
⊢ ∃ P ∈ Kaplansky.set S, ∀ J ∈ C, J ≤ P
Tactic:
refine' ⟨sSup C, _, fun z hz => le_sSup hz⟩
Proof state after:
case pos.intro
R : Type u_1
inst✝ : Semiring R
S : Subsemigroup R
hS : 0 ∉ S
C : Set (Ideal R)
hC : C ⊆ Kaplansky.set S
hC₂ : IsChain (fun x x_1 => x ≤ x_1) C
h : Set.Nonempty C
I : Ideal R
hI : I ∈ C
⊢ sSup C ∈ Kaplansky.set S
Theorem: hypothesis_zorn_lemma
Proof state before:
case pos.intro
R : Type u_1
inst✝ : Semiring R
S : Subsemigroup R
hS : 0 ∉ S
C : Set (Ideal R)
hC : C ⊆ Kaplansky.set S
hC₂ : IsChain (fun x x_1 => x ≤ x_1) C
h : Set.Nonempty C
I : Ideal R
hI : I ∈ C
⊢ sSup C ∈ Kaplansky.set S
Tactic:
rw [Kaplansky.set_def, Set.eq_empty_iff_forall_not_mem]
Proof state after:
case pos.intro
R : Type u_1
inst✝ : Semiring R
S : Subsemigroup R
hS : 0 ∉ S
C : Set (Ideal R)
hC : C ⊆ Kaplansky.set S
hC₂ : IsChain (fun x x_1 => x ≤ x_1) C
h : Set.Nonempty C
I : Ideal R
hI : I ∈ C
⊢ ∀ (x : R), x ∉ ↑(sSup C) ∩ ↑S
Theorem: hypothesis_zorn_lemma
Proof state before:
case pos.intro
R : Type u_1
inst✝ : Semiring R
S : Subsemigroup R
hS : 0 ∉ S
C : Set (Ideal R)
hC : C ⊆ Kaplansky.set S
hC₂ : IsChain (fun x x_1 => x ≤ x_1) C
h : Set.Nonempty C
I : Ideal R
hI : I ∈ C
⊢ ∀ (x : R), x ∉ ↑(sSup C) ∩ ↑S
Tactic:
rintro x hx
Proof state after:
case pos.intro
R : Type u_1
inst✝ : Semiring R
S : Subsemigroup R
hS : 0 ∉ S
C : Set (Ideal R)
hC : C ⊆ Kaplansky.set S
hC₂ : IsChain (fun x x_1 => x ≤ x_1) C
h : Set.Nonempty C
I : Ideal R
hI : I ∈ C
x : R
hx : x ∈ ↑(sSup C) ∩ ↑S
⊢ False
Theorem: hypothesis_zorn_lemma
Proof state before:
case pos.intro
R : Type u_1
inst✝ : Semiring R
S : Subsemigroup R
hS : 0 ∉ S
C : Set (Ideal R)
hC : C ⊆ Kaplansky.set S
hC₂ : IsChain (fun x x_1 => x ≤ x_1) C
h : Set.Nonempty C
I : Ideal R
hI : I ∈ C
x : R
hx : x ∈ ↑(sSup C) ∩ ↑S
⊢ False
Tactic:
rcases (Submodule.mem_sSup_of_directed ⟨_, hI⟩ hC₂.directedOn).1 hx.1 with ⟨J, hJ₁, hJ₂⟩
Proof state after:
case pos.intro.intro.intro
R : Type u_1
inst✝ : Semiring R
S : Subsemigroup R
hS : 0 ∉ S
C : Set (Ideal R)
hC : C ⊆ Kaplansky.set S
hC₂ : IsChain (fun x x_1 => x ≤ x_1) C
h : Set.Nonempty C
I : Ideal R
hI : I ∈ C
x : R
hx : x ∈ ↑(sSup C) ∩ ↑S
J : Submodule R R
hJ₁ : J ∈ C
hJ₂ : x ∈ J
⊢ False
Theorem: hypothesis_zorn_lemma
Proof state before:
case pos.intro.intro.intro
R : Type u_1
inst✝ : Semiring R
S : Subsemigroup R
hS : 0 ∉ S
C : Set (Ideal R)
hC : C ⊆ Kaplansky.set S
hC₂ : IsChain (fun x x_1 => x ≤ x_1) C
h : Set.Nonempty C
I : Ideal R
hI : I ∈ C
x : R
hx : x ∈ ↑(sSup C) ∩ ↑S
J : Submodule R R
hJ₁ : J ∈ C
hJ₂ : x ∈ J
⊢ False
Tactic:
have hx₂ : (J : Set R) ∩ S ≠ ∅ := Set.nonempty_iff_ne_empty.1 ⟨x, hJ₂, hx.2⟩
Proof state after:
case pos.intro.intro.intro
R : Type u_1
inst✝ : Semiring R
S : Subsemigroup R
hS : 0 ∉ S
C : Set (Ideal R)
hC : C ⊆ Kaplansky.set S
hC₂ : IsChain (fun x x_1 => x ≤ x_1) C
h : Set.Nonempty C
I : Ideal R
hI : I ∈ C
x : R
hx : x ∈ ↑(sSup C) ∩ ↑S
J : Submodule R R
hJ₁ : J ∈ C
hJ₂ : x ∈ J
hx₂ : ↑J ∩ ↑S ≠ ∅
⊢ False
Theorem: hypothesis_zorn_lemma
Proof state before:
case pos.intro.intro.intro
R : Type u_1
inst✝ : Semiring R
S : Subsemigroup R
hS : 0 ∉ S
C : Set (Ideal R)
hC : C ⊆ Kaplansky.set S
hC₂ : IsChain (fun x x_1 => x ≤ x_1) C
h : Set.Nonempty C
I : Ideal R
hI : I ∈ C
x : R
hx : x ∈ ↑(sSup C) ∩ ↑S
J : Submodule R R
hJ₁ : J ∈ C
hJ₂ : x ∈ J
hx₂ : ↑J ∩ ↑S ≠ ∅
⊢ False
Tactic:
exact hx₂ (hC hJ₁)
Proof state after:
no goals
Theorem: hypothesis_zorn_lemma
Proof state before:
case neg
R : Type u_1
inst✝ : Semiring R
S : Subsemigroup R
hS : 0 ∉ S
C : Set (Ideal R)
hC : C ⊆ Kaplansky.set S
hC₂ : IsChain (fun x x_1 => x ≤ x_1) C
h : ¬Set.Nonempty C
⊢ ∃ P ∈ Kaplansky.set S, ∀ J ∈ C, J ≤ P
Tactic:
rw [Set.not_nonempty_iff_eq_empty.1 h]
Proof state after:
case neg
R : Type u_1
inst✝ : Semiring R
S : Subsemigroup R
hS : 0 ∉ S
C : Set (Ideal R)
hC : C ⊆ Kaplansky.set S
hC₂ : IsChain (fun x x_1 => x ≤ x_1) C
h : ¬Set.Nonempty C
⊢ ∃ P ∈ Kaplansky.set S, ∀ J ∈ ∅, J ≤ P
Theorem: hypothesis_zorn_lemma
Proof state before:
case neg
R : Type u_1
inst✝ : Semiring R
S : Subsemigroup R
hS : 0 ∉ S
C : Set (Ideal R)
hC : C ⊆ Kaplansky.set S
hC₂ : IsChain (fun x x_1 => x ≤ x_1) C
h : ¬Set.Nonempty C
⊢ ∃ P ∈ Kaplansky.set S, ∀ J ∈ ∅, J ≤ P
Tactic:
use ⊥
Proof state after:
case h
R : Type u_1
inst✝ : Semiring R
S : Subsemigroup R
hS : 0 ∉ S
C : Set (Ideal R)
hC : C ⊆ Kaplansky.set S
hC₂ : IsChain (fun x x_1 => x ≤ x_1) C
h : ¬Set.Nonempty C
⊢ ⊥ ∈ Kaplansky.set S ∧ ∀ J ∈ ∅, J ≤ ⊥
Theorem: hypothesis_zorn_lemma
Proof state before:
case h
R : Type u_1
inst✝ : Semiring R
S : Subsemigroup R
hS : 0 ∉ S
C : Set (Ideal R)
hC : C ⊆ Kaplansky.set S
hC₂ : IsChain (fun x x_1 => x ≤ x_1) C
h : ¬Set.Nonempty C
⊢ ⊥ ∈ Kaplansky.set S ∧ ∀ J ∈ ∅, J ≤ ⊥
Tactic:
rw [Kaplansky.set_def, Set.eq_empty_iff_forall_not_mem]
Proof state after:
case h
R : Type u_1
inst✝ : Semiring R
S : Subsemigroup R
hS : 0 ∉ S
C : Set (Ideal R)
hC : C ⊆ Kaplansky.set S
hC₂ : IsChain (fun x x_1 => x ≤ x_1) C
h : ¬Set.Nonempty C
⊢ (∀ (x : R), x ∉ ↑⊥ ∩ ↑S) ∧ ∀ J ∈ ∅, J ≤ ⊥
Theorem: hypothesis_zorn_lemma
Proof state before:
case h
R : Type u_1
inst✝ : Semiring R
S : Subsemigroup R
hS : 0 ∉ S
C : Set (Ideal R)
hC : C ⊆ Kaplansky.set S
hC₂ : IsChain (fun x x_1 => x ≤ x_1) C
h : ¬Set.Nonempty C
⊢ (∀ (x : R), x ∉ ↑⊥ ∩ ↑S) ∧ ∀ J ∈ ∅, J ≤ ⊥
Tactic:
simp
Proof state after:
case h
R : Type u_1
inst✝ : Semiring R
S : Subsemigroup R
hS : 0 ∉ S
C : Set (Ideal R)
hC : C ⊆ Kaplansky.set S
hC₂ : IsChain (fun x x_1 => x ≤ x_1) C
h : ¬Set.Nonempty C
⊢ 0 ∉ S
Theorem: hypothesis_zorn_lemma
Proof state before:
case h
R : Type u_1
inst✝ : Semiring R
S : Subsemigroup R
hS : 0 ∉ S
C : Set (Ideal R)
hC : C ⊆ Kaplansky.set S
hC₂ : IsChain (fun x x_1 => x ≤ x_1) C
h : ¬Set.Nonempty C
⊢ 0 ∉ S
Tactic:
exact hS
Proof state after:
no goals
Theorem: ideal_neq_top
Proof state before:
R : Type u_1
inst✝ : Semiring R
S : Subsemigroup R
hS : Set.Nonempty ↑S
P : Ideal R
hP : P ∈ Kaplansky.set S
⊢ P ≠ ⊤
Tactic:
intro h
Proof state after:
R : Type u_1
inst✝ : Semiring R
S : Subsemigroup R
hS : Set.Nonempty ↑S
P : Ideal R
hP : P ∈ Kaplansky.set S
h : P = ⊤
⊢ False
Theorem: ideal_neq_top
Proof state before:
R : Type u_1
inst✝ : Semiring R
S : Subsemigroup R
hS : Set.Nonempty ↑S
P : Ideal R
hP : P ∈ Kaplansky.set S
h : P = ⊤
⊢ False
Tactic:
rw [Kaplansky.set, h, Set.mem_setOf, Set.eq_empty_iff_forall_not_mem] at hP
Proof state after:
R : Type u_1
inst✝ : Semiring R
S : Subsemigroup R
hS : Set.Nonempty ↑S
P : Ideal R
hP : ∀ (x : R), x ∉ ↑⊤ ∩ ↑S
h : P = ⊤
⊢ False
Theorem: ideal_neq_top
Proof state before:
R : Type u_1
inst✝ : Semiring R
S : Subsemigroup R
hS : Set.Nonempty ↑S
P : Ideal R
hP : ∀ (x : R), x ∉ ↑⊤ ∩ ↑S
h : P = ⊤
⊢ False
Tactic:
rw [Set.nonempty_def] at hS
Proof state after:
R : Type u_1
inst✝ : Semiring R
S : Subsemigroup R
hS : ∃ x, x ∈ ↑S
P : Ideal R
hP : ∀ (x : R), x ∉ ↑⊤ ∩ ↑S
h : P = ⊤
⊢ False
Theorem: ideal_neq_top
Proof state before:
R : Type u_1
inst✝ : Semiring R
S : Subsemigroup R
hS : ∃ x, x ∈ ↑S
P : Ideal R
hP : ∀ (x : R), x ∉ ↑⊤ ∩ ↑S
h : P = ⊤
⊢ False
Tactic:
cases' hS with x h₂
Proof state after:
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