Theorem: hypothesis_zorn_lemma (Kaplanski4/Kaplanski.lean)

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
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

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
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

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⟩
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

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]
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

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
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

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₂⟩
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

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⟩
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

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₁)
State after:
no goals

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]
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

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 ⊥
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 ≤ ⊥

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]
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 ≤ ⊥

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
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

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
State after:
no goals