Theorem: UpperLowerContinuous.real_induction (Compfiles/UpperLowerContinuous.lean)

State before:
S : Set ℝ
h1 : ∀ x ∈ S, ∃ y, x < y ∧ Set.Ico x y ⊆ S
h2 : ∀ (x y : ℝ), x < y → Set.Ico x y ⊆ S → y ∈ S
z : ℝ
hz : z ∈ S
⊢ Set.Ici z ⊆ S
Tactic:
by_contra H
State after:
S : Set ℝ
h1 : ∀ x ∈ S, ∃ y, x < y ∧ Set.Ico x y ⊆ S
h2 : ∀ (x y : ℝ), x < y → Set.Ico x y ⊆ S → y ∈ S
z : ℝ
hz : z ∈ S
H : ¬Set.Ici z ⊆ S
⊢ False

State before:
S : Set ℝ
h1 : ∀ x ∈ S, ∃ y, x < y ∧ Set.Ico x y ⊆ S
h2 : ∀ (x y : ℝ), x < y → Set.Ico x y ⊆ S → y ∈ S
z : ℝ
hz : z ∈ S
H : ¬Set.Ici z ⊆ S
⊢ False
Tactic:
rw[Set.subset_def] at H
State after:
S : Set ℝ
h1 : ∀ x ∈ S, ∃ y, x < y ∧ Set.Ico x y ⊆ S
h2 : ∀ (x y : ℝ), x < y → Set.Ico x y ⊆ S → y ∈ S
z : ℝ
hz : z ∈ S
H : ¬∀ x ∈ Set.Ici z, x ∈ S
⊢ False

State before:
S : Set ℝ
h1 : ∀ x ∈ S, ∃ y, x < y ∧ Set.Ico x y ⊆ S
h2 : ∀ (x y : ℝ), x < y → Set.Ico x y ⊆ S → y ∈ S
z : ℝ
hz : z ∈ S
H : ¬∀ x ∈ Set.Ici z, x ∈ S
⊢ False
Tactic:
push_neg at H
State after:
S : Set ℝ
h1 : ∀ x ∈ S, ∃ y, x < y ∧ Set.Ico x y ⊆ S
h2 : ∀ (x y : ℝ), x < y → Set.Ico x y ⊆ S → y ∈ S
z : ℝ
hz : z ∈ S
H : ∃ x ∈ Set.Ici z, x ∉ S
⊢ False

State before:
S : Set ℝ
h1 : ∀ x ∈ S, ∃ y, x < y ∧ Set.Ico x y ⊆ S
h2 : ∀ (x y : ℝ), x < y → Set.Ico x y ⊆ S → y ∈ S
z : ℝ
hz : z ∈ S
H : ∃ x ∈ Set.Ici z, x ∉ S
⊢ False
Tactic:
obtain ⟨w₁, hw₁, hw₁'⟩ := H
State after:
case intro.intro
S : Set ℝ
h1 : ∀ x ∈ S, ∃ y, x < y ∧ Set.Ico x y ⊆ S
h2 : ∀ (x y : ℝ), x < y → Set.Ico x y ⊆ S → y ∈ S
z : ℝ
hz : z ∈ S
w₁ : ℝ
hw₁ : w₁ ∈ Set.Ici z
hw₁' : w₁ ∉ S
⊢ False

State before:
case intro.intro
S : Set ℝ
h1 : ∀ x ∈ S, ∃ y, x < y ∧ Set.Ico x y ⊆ S
h2 : ∀ (x y : ℝ), x < y → Set.Ico x y ⊆ S → y ∈ S
z : ℝ
hz : z ∈ S
w₁ : ℝ
hw₁ : w₁ ∈ Set.Ici z
hw₁' : w₁ ∉ S
⊢ False
Tactic:
let W : Set ℝ := {w | z ≤ w ∧ w ∉ S}
State after:
case intro.intro
S : Set ℝ
h1 : ∀ x ∈ S, ∃ y, x < y ∧ Set.Ico x y ⊆ S
h2 : ∀ (x y : ℝ), x < y → Set.Ico x y ⊆ S → y ∈ S
z : ℝ
hz : z ∈ S
w₁ : ℝ
hw₁ : w₁ ∈ Set.Ici z
hw₁' : w₁ ∉ S
W : Set ℝ := {w | z ≤ w ∧ w ∉ S}
⊢ False

State before:
case intro.intro
S : Set ℝ
h1 : ∀ x ∈ S, ∃ y, x < y ∧ Set.Ico x y ⊆ S
h2 : ∀ (x y : ℝ), x < y → Set.Ico x y ⊆ S → y ∈ S
z : ℝ
hz : z ∈ S
w₁ : ℝ
hw₁ : w₁ ∈ Set.Ici z
hw₁' : w₁ ∉ S
W : Set ℝ := {w | z ≤ w ∧ w ∉ S}
⊢ False
Tactic:
let w₀ := sInf W
State after:
case intro.intro
S : Set ℝ
h1 : ∀ x ∈ S, ∃ y, x < y ∧ Set.Ico x y ⊆ S
h2 : ∀ (x y : ℝ), x < y → Set.Ico x y ⊆ S → y ∈ S
z : ℝ
hz : z ∈ S
w₁ : ℝ
hw₁ : w₁ ∈ Set.Ici z
hw₁' : w₁ ∉ S
W : Set ℝ := {w | z ≤ w ∧ w ∉ S}
w₀ : ℝ := sInf W
⊢ False

State before:
case intro.intro
S : Set ℝ
h1 : ∀ x ∈ S, ∃ y, x < y ∧ Set.Ico x y ⊆ S
h2 : ∀ (x y : ℝ), x < y → Set.Ico x y ⊆ S → y ∈ S
z : ℝ
hz : z ∈ S
w₁ : ℝ
hw₁ : w₁ ∈ Set.Ici z
hw₁' : w₁ ∉ S
W : Set ℝ := {w | z ≤ w ∧ w ∉ S}
w₀ : ℝ := sInf W
⊢ False
Tactic:
have hwne : Set.Nonempty W := ⟨w₁, hw₁, hw₁'⟩
State after:
case intro.intro
S : Set ℝ
h1 : ∀ x ∈ S, ∃ y, x < y ∧ Set.Ico x y ⊆ S
h2 : ∀ (x y : ℝ), x < y → Set.Ico x y ⊆ S → y ∈ S
z : ℝ
hz : z ∈ S
w₁ : ℝ
hw₁ : w₁ ∈ Set.Ici z
hw₁' : w₁ ∉ S
W : Set ℝ := {w | z ≤ w ∧ w ∉ S}
w₀ : ℝ := sInf W
hwne : W.Nonempty
⊢ False

State before:
case intro.intro
S : Set ℝ
h1 : ∀ x ∈ S, ∃ y, x < y ∧ Set.Ico x y ⊆ S
h2 : ∀ (x y : ℝ), x < y → Set.Ico x y ⊆ S → y ∈ S
z : ℝ
hz : z ∈ S
w₁ : ℝ
hw₁ : w₁ ∈ Set.Ici z
hw₁' : w₁ ∉ S
W : Set ℝ := {w | z ≤ w ∧ w ∉ S}
w₀ : ℝ := sInf W
hwne : W.Nonempty
⊢ False
Tactic:
have h6 : z ∈ lowerBounds W := fun _ ha ↦ ha.1
State after:
case intro.intro
S : Set ℝ
h1 : ∀ x ∈ S, ∃ y, x < y ∧ Set.Ico x y ⊆ S
h2 : ∀ (x y : ℝ), x < y → Set.Ico x y ⊆ S → y ∈ S
z : ℝ
hz : z ∈ S
w₁ : ℝ
hw₁ : w₁ ∈ Set.Ici z
hw₁' : w₁ ∉ S
W : Set ℝ := {w | z ≤ w ∧ w ∉ S}
w₀ : ℝ := sInf W
hwne : W.Nonempty
h6 : z ∈ lowerBounds W
⊢ False

State before:
case intro.intro
S : Set ℝ
h1 : ∀ x ∈ S, ∃ y, x < y ∧ Set.Ico x y ⊆ S
h2 : ∀ (x y : ℝ), x < y → Set.Ico x y ⊆ S → y ∈ S
z : ℝ
hz : z ∈ S
w₁ : ℝ
hw₁ : w₁ ∈ Set.Ici z
hw₁' : w₁ ∉ S
W : Set ℝ := {w | z ≤ w ∧ w ∉ S}
w₀ : ℝ := sInf W
hwne : W.Nonempty
h6 : z ∈ lowerBounds W
⊢ False
Tactic:
have hwbb : BddBelow W := Set.nonempty_of_mem h6
State after:
case intro.intro
S : Set ℝ
h1 : ∀ x ∈ S, ∃ y, x < y ∧ Set.Ico x y ⊆ S
h2 : ∀ (x y : ℝ), x < y → Set.Ico x y ⊆ S → y ∈ S
z : ℝ
hz : z ∈ S
w₁ : ℝ
hw₁ : w₁ ∈ Set.Ici z
hw₁' : w₁ ∉ S
W : Set ℝ := {w | z ≤ w ∧ w ∉ S}
w₀ : ℝ := sInf W
hwne : W.Nonempty
h6 : z ∈ lowerBounds W
hwbb : BddBelow W
⊢ False

State before:
case intro.intro
S : Set ℝ
h1 : ∀ x ∈ S, ∃ y, x < y ∧ Set.Ico x y ⊆ S
h2 : ∀ (x y : ℝ), x < y → Set.Ico x y ⊆ S → y ∈ S
z : ℝ
hz : z ∈ S
w₁ : ℝ
hw₁ : w₁ ∈ Set.Ici z
hw₁' : w₁ ∉ S
W : Set ℝ := {w | z ≤ w ∧ w ∉ S}
w₀ : ℝ := sInf W
hwne : W.Nonempty
h6 : z ∈ lowerBounds W
hwbb : BddBelow W
⊢ False
Tactic:
have h7: Set.Ico z w₀ ⊆ S := by
  intro s₁ hs
  by_contra H
  exact (not_le.mpr hs.2) (csInf_le hwbb ⟨hs.1, H⟩)
State after:
case intro.intro
S : Set ℝ
h1 : ∀ x ∈ S, ∃ y, x < y ∧ Set.Ico x y ⊆ S
h2 : ∀ (x y : ℝ), x < y → Set.Ico x y ⊆ S → y ∈ S
z : ℝ
hz : z ∈ S
w₁ : ℝ
hw₁ : w₁ ∈ Set.Ici z
hw₁' : w₁ ∉ S
W : Set ℝ := {w | z ≤ w ∧ w ∉ S}
w₀ : ℝ := sInf W
hwne : W.Nonempty
h6 : z ∈ lowerBounds W
hwbb : BddBelow W
h7 : Set.Ico z w₀ ⊆ S
⊢ False

State before:
case intro.intro
S : Set ℝ
h1 : ∀ x ∈ S, ∃ y, x < y ∧ Set.Ico x y ⊆ S
h2 : ∀ (x y : ℝ), x < y → Set.Ico x y ⊆ S → y ∈ S
z : ℝ
hz : z ∈ S
w₁ : ℝ
hw₁ : w₁ ∈ Set.Ici z
hw₁' : w₁ ∉ S
W : Set ℝ := {w | z ≤ w ∧ w ∉ S}
w₀ : ℝ := sInf W
hwne : W.Nonempty
h6 : z ∈ lowerBounds W
hwbb : BddBelow W
h7 : Set.Ico z w₀ ⊆ S
⊢ False
Tactic:
have h9 : ∀ w ∈ W, z ≤ w := fun w h ↦ h.1
State after:
case intro.intro
S : Set ℝ
h1 : ∀ x ∈ S, ∃ y, x < y ∧ Set.Ico x y ⊆ S
h2 : ∀ (x y : ℝ), x < y → Set.Ico x y ⊆ S → y ∈ S
z : ℝ
hz : z ∈ S
w₁ : ℝ
hw₁ : w₁ ∈ Set.Ici z
hw₁' : w₁ ∉ S
W : Set ℝ := {w | z ≤ w ∧ w ∉ S}
w₀ : ℝ := sInf W
hwne : W.Nonempty
h6 : z ∈ lowerBounds W
hwbb : BddBelow W
h7 : Set.Ico z w₀ ⊆ S
h9 : ∀ w ∈ W, z ≤ w
⊢ False

State before:
case intro.intro
S : Set ℝ
h1 : ∀ x ∈ S, ∃ y, x < y ∧ Set.Ico x y ⊆ S
h2 : ∀ (x y : ℝ), x < y → Set.Ico x y ⊆ S → y ∈ S
z : ℝ
hz : z ∈ S
w₁ : ℝ
hw₁ : w₁ ∈ Set.Ici z
hw₁' : w₁ ∉ S
W : Set ℝ := {w | z ≤ w ∧ w ∉ S}
w₀ : ℝ := sInf W
hwne : W.Nonempty
h6 : z ∈ lowerBounds W
hwbb : BddBelow W
h7 : Set.Ico z w₀ ⊆ S
h9 : ∀ w ∈ W, z ≤ w
⊢ False
Tactic:
have h10 : z ≤ w₀ := le_csInf hwne h9
State after:
case intro.intro
S : Set ℝ
h1 : ∀ x ∈ S, ∃ y, x < y ∧ Set.Ico x y ⊆ S
h2 : ∀ (x y : ℝ), x < y → Set.Ico x y ⊆ S → y ∈ S
z : ℝ
hz : z ∈ S
w₁ : ℝ
hw₁ : w₁ ∈ Set.Ici z
hw₁' : w₁ ∉ S
W : Set ℝ := {w | z ≤ w ∧ w ∉ S}
w₀ : ℝ := sInf W
hwne : W.Nonempty
h6 : z ∈ lowerBounds W
hwbb : BddBelow W
h7 : Set.Ico z w₀ ⊆ S
h9 : ∀ w ∈ W, z ≤ w
h10 : z ≤ w₀
⊢ False

State before:
case intro.intro
S : Set ℝ
h1 : ∀ x ∈ S, ∃ y, x < y ∧ Set.Ico x y ⊆ S
h2 : ∀ (x y : ℝ), x < y → Set.Ico x y ⊆ S → y ∈ S
z : ℝ
hz : z ∈ S
w₁ : ℝ
hw₁ : w₁ ∈ Set.Ici z
hw₁' : w₁ ∉ S
W : Set ℝ := {w | z ≤ w ∧ w ∉ S}
w₀ : ℝ := sInf W
hwne : W.Nonempty
h6 : z ∈ lowerBounds W
hwbb : BddBelow W
h7 : Set.Ico z w₀ ⊆ S
h9 : ∀ w ∈ W, z ≤ w
h10 : z ≤ w₀
⊢ False
Tactic:
have h13 := Real.is_glb_sInf W hwne hwbb
State after:
case intro.intro
S : Set ℝ
h1 : ∀ x ∈ S, ∃ y, x < y ∧ Set.Ico x y ⊆ S
h2 : ∀ (x y : ℝ), x < y → Set.Ico x y ⊆ S → y ∈ S
z : ℝ
hz : z ∈ S
w₁ : ℝ
hw₁ : w₁ ∈ Set.Ici z
hw₁' : w₁ ∉ S
W : Set ℝ := {w | z ≤ w ∧ w ∉ S}
w₀ : ℝ := sInf W
hwne : W.Nonempty
h6 : z ∈ lowerBounds W
hwbb : BddBelow W
h7 : Set.Ico z w₀ ⊆ S
h9 : ∀ w ∈ W, z ≤ w
h10 : z ≤ w₀
h13 : IsGLB W (sInf W)
⊢ False

State before:
case intro.intro
S : Set ℝ
h1 : ∀ x ∈ S, ∃ y, x < y ∧ Set.Ico x y ⊆ S
h2 : ∀ (x y : ℝ), x < y → Set.Ico x y ⊆ S → y ∈ S
z : ℝ
hz : z ∈ S
w₁ : ℝ
hw₁ : w₁ ∈ Set.Ici z
hw₁' : w₁ ∉ S
W : Set ℝ := {w | z ≤ w ∧ w ∉ S}
w₀ : ℝ := sInf W
hwne : W.Nonempty
h6 : z ∈ lowerBounds W
hwbb : BddBelow W
h7 : Set.Ico z w₀ ⊆ S
h9 : ∀ w ∈ W, z ≤ w
h10 : z ≤ w₀
h13 : IsGLB W (sInf W)
⊢ False
Tactic:
have h11 : z ≠ w₀ := by
  by_contra H
  obtain ⟨y, hy1, hy2⟩ := h1 z hz
  rw[H] at hy1 h6
  have h12 : y ∈ lowerBounds W := by
    intro a ha;
    by_contra H'; push_neg at H'
    exact ha.2 (hy2 ⟨h9 a ha, H'⟩)
  exact (not_le.mpr hy1) ((isGLB_iff_le_iff.mp h13 y).mpr h12)
State after:
case intro.intro
S : Set ℝ
h1 : ∀ x ∈ S, ∃ y, x < y ∧ Set.Ico x y ⊆ S
h2 : ∀ (x y : ℝ), x < y → Set.Ico x y ⊆ S → y ∈ S
z : ℝ
hz : z ∈ S
w₁ : ℝ
hw₁ : w₁ ∈ Set.Ici z
hw₁' : w₁ ∉ S
W : Set ℝ := {w | z ≤ w ∧ w ∉ S}
w₀ : ℝ := sInf W
hwne : W.Nonempty
h6 : z ∈ lowerBounds W
hwbb : BddBelow W
h7 : Set.Ico z w₀ ⊆ S
h9 : ∀ w ∈ W, z ≤ w
h10 : z ≤ w₀
h13 : IsGLB W (sInf W)
h11 : z ≠ w₀
⊢ False

State before:
case intro.intro
S : Set ℝ
h1 : ∀ x ∈ S, ∃ y, x < y ∧ Set.Ico x y ⊆ S
h2 : ∀ (x y : ℝ), x < y → Set.Ico x y ⊆ S → y ∈ S
z : ℝ
hz : z ∈ S
w₁ : ℝ
hw₁ : w₁ ∈ Set.Ici z
hw₁' : w₁ ∉ S
W : Set ℝ := {w | z ≤ w ∧ w ∉ S}
w₀ : ℝ := sInf W
hwne : W.Nonempty
h6 : z ∈ lowerBounds W
hwbb : BddBelow W
h7 : Set.Ico z w₀ ⊆ S
h9 : ∀ w ∈ W, z ≤ w
h10 : z ≤ w₀
h13 : IsGLB W (sInf W)
h11 : z ≠ w₀
⊢ False
Tactic:
have h15: z < w₀ := Ne.lt_of_le h11 h10
State after:
case intro.intro
S : Set ℝ
h1 : ∀ x ∈ S, ∃ y, x < y ∧ Set.Ico x y ⊆ S
h2 : ∀ (x y : ℝ), x < y → Set.Ico x y ⊆ S → y ∈ S
z : ℝ
hz : z ∈ S
w₁ : ℝ
hw₁ : w₁ ∈ Set.Ici z
hw₁' : w₁ ∉ S
W : Set ℝ := {w | z ≤ w ∧ w ∉ S}
w₀ : ℝ := sInf W
hwne : W.Nonempty
h6 : z ∈ lowerBounds W
hwbb : BddBelow W
h7 : Set.Ico z w₀ ⊆ S
h9 : ∀ w ∈ W, z ≤ w
h10 : z ≤ w₀
h13 : IsGLB W (sInf W)
h11 : z ≠ w₀
h15 : z < w₀
⊢ False

State before:
case intro.intro
S : Set ℝ
h1 : ∀ x ∈ S, ∃ y, x < y ∧ Set.Ico x y ⊆ S
h2 : ∀ (x y : ℝ), x < y → Set.Ico x y ⊆ S → y ∈ S
z : ℝ
hz : z ∈ S
w₁ : ℝ
hw₁ : w₁ ∈ Set.Ici z
hw₁' : w₁ ∉ S
W : Set ℝ := {w | z ≤ w ∧ w ∉ S}
w₀ : ℝ := sInf W
hwne : W.Nonempty
h6 : z ∈ lowerBounds W
hwbb : BddBelow W
h7 : Set.Ico z w₀ ⊆ S
h9 : ∀ w ∈ W, z ≤ w
h10 : z ≤ w₀
h13 : IsGLB W (sInf W)
h11 : z ≠ w₀
h15 : z < w₀
⊢ False
Tactic:
have h8 := h2 z w₀ h15 h7
State after:
case intro.intro
S : Set ℝ
h1 : ∀ x ∈ S, ∃ y, x < y ∧ Set.Ico x y ⊆ S
h2 : ∀ (x y : ℝ), x < y → Set.Ico x y ⊆ S → y ∈ S
z : ℝ
hz : z ∈ S
w₁ : ℝ
hw₁ : w₁ ∈ Set.Ici z
hw₁' : w₁ ∉ S
W : Set ℝ := {w | z ≤ w ∧ w ∉ S}
w₀ : ℝ := sInf W
hwne : W.Nonempty
h6 : z ∈ lowerBounds W
hwbb : BddBelow W
h7 : Set.Ico z w₀ ⊆ S
h9 : ∀ w ∈ W, z ≤ w
h10 : z ≤ w₀
h13 : IsGLB W (sInf W)
h11 : z ≠ w₀
h15 : z < w₀
h8 : w₀ ∈ S
⊢ False

State before:
case intro.intro
S : Set ℝ
h1 : ∀ x ∈ S, ∃ y, x < y ∧ Set.Ico x y ⊆ S
h2 : ∀ (x y : ℝ), x < y → Set.Ico x y ⊆ S → y ∈ S
z : ℝ
hz : z ∈ S
w₁ : ℝ
hw₁ : w₁ ∈ Set.Ici z
hw₁' : w₁ ∉ S
W : Set ℝ := {w | z ≤ w ∧ w ∉ S}
w₀ : ℝ := sInf W
hwne : W.Nonempty
h6 : z ∈ lowerBounds W
hwbb : BddBelow W
h7 : Set.Ico z w₀ ⊆ S
h9 : ∀ w ∈ W, z ≤ w
h10 : z ≤ w₀
h13 : IsGLB W (sInf W)
h11 : z ≠ w₀
h15 : z < w₀
h8 : w₀ ∈ S
⊢ False
Tactic:
obtain ⟨y, hwy, hy⟩ := h1 w₀ h8
State after:
case intro.intro.intro.intro
S : Set ℝ
h1 : ∀ x ∈ S, ∃ y, x < y ∧ Set.Ico x y ⊆ S
h2 : ∀ (x y : ℝ), x < y → Set.Ico x y ⊆ S → y ∈ S
z : ℝ
hz : z ∈ S
w₁ : ℝ
hw₁ : w₁ ∈ Set.Ici z
hw₁' : w₁ ∉ S
W : Set ℝ := {w | z ≤ w ∧ w ∉ S}
w₀ : ℝ := sInf W
hwne : W.Nonempty
h6 : z ∈ lowerBounds W
hwbb : BddBelow W
h7 : Set.Ico z w₀ ⊆ S
h9 : ∀ w ∈ W, z ≤ w
h10 : z ≤ w₀
h13 : IsGLB W (sInf W)
h11 : z ≠ w₀
h15 : z < w₀
h8 : w₀ ∈ S
y : ℝ
hwy : w₀ < y
hy : Set.Ico w₀ y ⊆ S
⊢ False

State before:
case intro.intro.intro.intro
S : Set ℝ
h1 : ∀ x ∈ S, ∃ y, x < y ∧ Set.Ico x y ⊆ S
h2 : ∀ (x y : ℝ), x < y → Set.Ico x y ⊆ S → y ∈ S
z : ℝ
hz : z ∈ S
w₁ : ℝ
hw₁ : w₁ ∈ Set.Ici z
hw₁' : w₁ ∉ S
W : Set ℝ := {w | z ≤ w ∧ w ∉ S}
w₀ : ℝ := sInf W
hwne : W.Nonempty
h6 : z ∈ lowerBounds W
hwbb : BddBelow W
h7 : Set.Ico z w₀ ⊆ S
h9 : ∀ w ∈ W, z ≤ w
h10 : z ≤ w₀
h13 : IsGLB W (sInf W)
h11 : z ≠ w₀
h15 : z < w₀
h8 : w₀ ∈ S
y : ℝ
hwy : w₀ < y
hy : Set.Ico w₀ y ⊆ S
h12 : y ∈ lowerBounds W
⊢ False
Tactic:
exact (not_le.mpr hwy) ((isGLB_iff_le_iff.mp h13 y).mpr h12)
State after:
no goals

State before:
S : Set ℝ
h1 : ∀ x ∈ S, ∃ y, x < y ∧ Set.Ico x y ⊆ S
h2 : ∀ (x y : ℝ), x < y → Set.Ico x y ⊆ S → y ∈ S
z : ℝ
hz : z ∈ S
w₁ : ℝ
hw₁ : w₁ ∈ Set.Ici z
hw₁' : w₁ ∉ S
W : Set ℝ := {w | z ≤ w ∧ w ∉ S}
w₀ : ℝ := sInf W
hwne : W.Nonempty
h6 : z ∈ lowerBounds W
hwbb : BddBelow W
⊢ Set.Ico z w₀ ⊆ S
Tactic:
intro s₁ hs
State after:
S : Set ℝ
h1 : ∀ x ∈ S, ∃ y, x < y ∧ Set.Ico x y ⊆ S
h2 : ∀ (x y : ℝ), x < y → Set.Ico x y ⊆ S → y ∈ S
z : ℝ
hz : z ∈ S
w₁ : ℝ
hw₁ : w₁ ∈ Set.Ici z
hw₁' : w₁ ∉ S
W : Set ℝ := {w | z ≤ w ∧ w ∉ S}
w₀ : ℝ := sInf W
hwne : W.Nonempty
h6 : z ∈ lowerBounds W
hwbb : BddBelow W
s₁ : ℝ
hs : s₁ ∈ Set.Ico z w₀
⊢ s₁ ∈ S

State before:
S : Set ℝ
h1 : ∀ x ∈ S, ∃ y, x < y ∧ Set.Ico x y ⊆ S
h2 : ∀ (x y : ℝ), x < y → Set.Ico x y ⊆ S → y ∈ S
z : ℝ
hz : z ∈ S
w₁ : ℝ
hw₁ : w₁ ∈ Set.Ici z
hw₁' : w₁ ∉ S
W : Set ℝ := {w | z ≤ w ∧ w ∉ S}
w₀ : ℝ := sInf W
hwne : W.Nonempty
h6 : z ∈ lowerBounds W
hwbb : BddBelow W
s₁ : ℝ
hs : s₁ ∈ Set.Ico z w₀
⊢ s₁ ∈ S
Tactic:
by_contra H
State after:
S : Set ℝ
h1 : ∀ x ∈ S, ∃ y, x < y ∧ Set.Ico x y ⊆ S
h2 : ∀ (x y : ℝ), x < y → Set.Ico x y ⊆ S → y ∈ S
z : ℝ
hz : z ∈ S
w₁ : ℝ
hw₁ : w₁ ∈ Set.Ici z
hw₁' : w₁ ∉ S
W : Set ℝ := {w | z ≤ w ∧ w ∉ S}
w₀ : ℝ := sInf W
hwne : W.Nonempty
h6 : z ∈ lowerBounds W
hwbb : BddBelow W
s₁ : ℝ
hs : s₁ ∈ Set.Ico z w₀
H : s₁ ∉ S
⊢ False

State before:
S : Set ℝ
h1 : ∀ x ∈ S, ∃ y, x < y ∧ Set.Ico x y ⊆ S
h2 : ∀ (x y : ℝ), x < y → Set.Ico x y ⊆ S → y ∈ S
z : ℝ
hz : z ∈ S
w₁ : ℝ
hw₁ : w₁ ∈ Set.Ici z
hw₁' : w₁ ∉ S
W : Set ℝ := {w | z ≤ w ∧ w ∉ S}
w₀ : ℝ := sInf W
hwne : W.Nonempty
h6 : z ∈ lowerBounds W
hwbb : BddBelow W
s₁ : ℝ
hs : s₁ ∈ Set.Ico z w₀
H : s₁ ∉ S
⊢ False
Tactic:
exact (not_le.mpr hs.2) (csInf_le hwbb ⟨hs.1, H⟩)
State after:
no goals

State before:
S : Set ℝ
h1 : ∀ x ∈ S, ∃ y, x < y ∧ Set.Ico x y ⊆ S
h2 : ∀ (x y : ℝ), x < y → Set.Ico x y ⊆ S → y ∈ S
z : ℝ
hz : z ∈ S
w₁ : ℝ
hw₁ : w₁ ∈ Set.Ici z
hw₁' : w₁ ∉ S
W : Set ℝ := {w | z ≤ w ∧ w ∉ S}
w₀ : ℝ := sInf W
hwne : W.Nonempty
h6 : z ∈ lowerBounds W
hwbb : BddBelow W
h7 : Set.Ico z w₀ ⊆ S
h9 : ∀ w ∈ W, z ≤ w
h10 : z ≤ w₀
h13 : IsGLB W (sInf W)
⊢ z ≠ w₀
Tactic:
by_contra H
State after:
S : Set ℝ
h1 : ∀ x ∈ S, ∃ y, x < y ∧ Set.Ico x y ⊆ S
h2 : ∀ (x y : ℝ), x < y → Set.Ico x y ⊆ S → y ∈ S
z : ℝ
hz : z ∈ S
w₁ : ℝ
hw₁ : w₁ ∈ Set.Ici z
hw₁' : w₁ ∉ S
W : Set ℝ := {w | z ≤ w ∧ w ∉ S}
w₀ : ℝ := sInf W
hwne : W.Nonempty
h6 : z ∈ lowerBounds W
hwbb : BddBelow W
h7 : Set.Ico z w₀ ⊆ S
h9 : ∀ w ∈ W, z ≤ w
h10 : z ≤ w₀
h13 : IsGLB W (sInf W)
H : z = w₀
⊢ False

State before:
S : Set ℝ
h1 : ∀ x ∈ S, ∃ y, x < y ∧ Set.Ico x y ⊆ S
h2 : ∀ (x y : ℝ), x < y → Set.Ico x y ⊆ S → y ∈ S
z : ℝ
hz : z ∈ S
w₁ : ℝ
hw₁ : w₁ ∈ Set.Ici z
hw₁' : w₁ ∉ S
W : Set ℝ := {w | z ≤ w ∧ w ∉ S}
w₀ : ℝ := sInf W
hwne : W.Nonempty
h6 : z ∈ lowerBounds W
hwbb : BddBelow W
h7 : Set.Ico z w₀ ⊆ S
h9 : ∀ w ∈ W, z ≤ w
h10 : z ≤ w₀
h13 : IsGLB W (sInf W)
H : z = w₀
⊢ False
Tactic:
obtain ⟨y, hy1, hy2⟩ := h1 z hz
State after:
case intro.intro
S : Set ℝ
h1 : ∀ x ∈ S, ∃ y, x < y ∧ Set.Ico x y ⊆ S
h2 : ∀ (x y : ℝ), x < y → Set.Ico x y ⊆ S → y ∈ S
z : ℝ
hz : z ∈ S
w₁ : ℝ
hw₁ : w₁ ∈ Set.Ici z
hw₁' : w₁ ∉ S
W : Set ℝ := {w | z ≤ w ∧ w ∉ S}
w₀ : ℝ := sInf W
hwne : W.Nonempty
h6 : z ∈ lowerBounds W
hwbb : BddBelow W
h7 : Set.Ico z w₀ ⊆ S
h9 : ∀ w ∈ W, z ≤ w
h10 : z ≤ w₀
h13 : IsGLB W (sInf W)
H : z = w₀
y : ℝ
hy1 : z < y
hy2 : Set.Ico z y ⊆ S
⊢ False

State before:
case intro.intro
S : Set ℝ
h1 : ∀ x ∈ S, ∃ y, x < y ∧ Set.Ico x y ⊆ S
h2 : ∀ (x y : ℝ), x < y → Set.Ico x y ⊆ S → y ∈ S
z : ℝ
hz : z ∈ S
w₁ : ℝ
hw₁ : w₁ ∈ Set.Ici z
hw₁' : w₁ ∉ S
W : Set ℝ := {w | z ≤ w ∧ w ∉ S}
w₀ : ℝ := sInf W
hwne : W.Nonempty
h6 : z ∈ lowerBounds W
hwbb : BddBelow W
h7 : Set.Ico z w₀ ⊆ S
h9 : ∀ w ∈ W, z ≤ w
h10 : z ≤ w₀
h13 : IsGLB W (sInf W)
H : z = w₀
y : ℝ
hy1 : z < y
hy2 : Set.Ico z y ⊆ S
⊢ False
Tactic:
rw[H] at hy1 h6
State after:
case intro.intro
S : Set ℝ
h1 : ∀ x ∈ S, ∃ y, x < y ∧ Set.Ico x y ⊆ S
h2 : ∀ (x y : ℝ), x < y → Set.Ico x y ⊆ S → y ∈ S
z : ℝ
hz : z ∈ S
w₁ : ℝ
hw₁ : w₁ ∈ Set.Ici z
hw₁' : w₁ ∉ S
W : Set ℝ := {w | z ≤ w ∧ w ∉ S}
w₀ : ℝ := sInf W
hwne : W.Nonempty
h6 : w₀ ∈ lowerBounds W
hwbb : BddBelow W
h7 : Set.Ico z w₀ ⊆ S
h9 : ∀ w ∈ W, z ≤ w
h10 : z ≤ w₀
h13 : IsGLB W (sInf W)
H : z = w₀
y : ℝ
hy1 : w₀ < y
hy2 : Set.Ico z y ⊆ S
⊢ False

State before:
case intro.intro
S : Set ℝ
h1 : ∀ x ∈ S, ∃ y, x < y ∧ Set.Ico x y ⊆ S
h2 : ∀ (x y : ℝ), x < y → Set.Ico x y ⊆ S → y ∈ S
z : ℝ
hz : z ∈ S
w₁ : ℝ
hw₁ : w₁ ∈ Set.Ici z
hw₁' : w₁ ∉ S
W : Set ℝ := {w | z ≤ w ∧ w ∉ S}
w₀ : ℝ := sInf W
hwne : W.Nonempty
h6 : w₀ ∈ lowerBounds W
hwbb : BddBelow W
h7 : Set.Ico z w₀ ⊆ S
h9 : ∀ w ∈ W, z ≤ w
h10 : z ≤ w₀
h13 : IsGLB W (sInf W)
H : z = w₀
y : ℝ
hy1 : w₀ < y
hy2 : Set.Ico z y ⊆ S
⊢ False
Tactic:
have h12 : y ∈ lowerBounds W := by
  intro a ha;
  by_contra H'; push_neg at H'
  exact ha.2 (hy2 ⟨h9 a ha, H'⟩)
State after:
case intro.intro
S : Set ℝ
h1 : ∀ x ∈ S, ∃ y, x < y ∧ Set.Ico x y ⊆ S
h2 : ∀ (x y : ℝ), x < y → Set.Ico x y ⊆ S → y ∈ S
z : ℝ
hz : z ∈ S
w₁ : ℝ
hw₁ : w₁ ∈ Set.Ici z
hw₁' : w₁ ∉ S
W : Set ℝ := {w | z ≤ w ∧ w ∉ S}
w₀ : ℝ := sInf W
hwne : W.Nonempty
h6 : w₀ ∈ lowerBounds W
hwbb : BddBelow W
h7 : Set.Ico z w₀ ⊆ S
h9 : ∀ w ∈ W, z ≤ w
h10 : z ≤ w₀
h13 : IsGLB W (sInf W)
H : z = w₀
y : ℝ
hy1 : w₀ < y
hy2 : Set.Ico z y ⊆ S
h12 : y ∈ lowerBounds W
⊢ False

State before:
case intro.intro
S : Set ℝ
h1 : ∀ x ∈ S, ∃ y, x < y ∧ Set.Ico x y ⊆ S
h2 : ∀ (x y : ℝ), x < y → Set.Ico x y ⊆ S → y ∈ S
z : ℝ
hz : z ∈ S
w₁ : ℝ
hw₁ : w₁ ∈ Set.Ici z
hw₁' : w₁ ∉ S
W : Set ℝ := {w | z ≤ w ∧ w ∉ S}
w₀ : ℝ := sInf W
hwne : W.Nonempty
h6 : w₀ ∈ lowerBounds W
hwbb : BddBelow W
h7 : Set.Ico z w₀ ⊆ S
h9 : ∀ w ∈ W, z ≤ w
h10 : z ≤ w₀
h13 : IsGLB W (sInf W)
H : z = w₀
y : ℝ
hy1 : w₀ < y
hy2 : Set.Ico z y ⊆ S
h12 : y ∈ lowerBounds W
⊢ False
Tactic:
exact (not_le.mpr hy1) ((isGLB_iff_le_iff.mp h13 y).mpr h12)
State after:
no goals

State before:
S : Set ℝ
h1 : ∀ x ∈ S, ∃ y, x < y ∧ Set.Ico x y ⊆ S
h2 : ∀ (x y : ℝ), x < y → Set.Ico x y ⊆ S → y ∈ S
z : ℝ
hz : z ∈ S
w₁ : ℝ
hw₁ : w₁ ∈ Set.Ici z
hw₁' : w₁ ∉ S
W : Set ℝ := {w | z ≤ w ∧ w ∉ S}
w₀ : ℝ := sInf W
hwne : W.Nonempty
h6 : w₀ ∈ lowerBounds W
hwbb : BddBelow W
h7 : Set.Ico z w₀ ⊆ S
h9 : ∀ w ∈ W, z ≤ w
h10 : z ≤ w₀
h13 : IsGLB W (sInf W)
H : z = w₀
y : ℝ
hy1 : w₀ < y
hy2 : Set.Ico z y ⊆ S
⊢ y ∈ lowerBounds W
Tactic:
intro a ha
State after:
S : Set ℝ
h1 : ∀ x ∈ S, ∃ y, x < y ∧ Set.Ico x y ⊆ S
h2 : ∀ (x y : ℝ), x < y → Set.Ico x y ⊆ S → y ∈ S
z : ℝ
hz : z ∈ S
w₁ : ℝ
hw₁ : w₁ ∈ Set.Ici z
hw₁' : w₁ ∉ S
W : Set ℝ := {w | z ≤ w ∧ w ∉ S}
w₀ : ℝ := sInf W
hwne : W.Nonempty
h6 : w₀ ∈ lowerBounds W
hwbb : BddBelow W
h7 : Set.Ico z w₀ ⊆ S
h9 : ∀ w ∈ W, z ≤ w
h10 : z ≤ w₀
h13 : IsGLB W (sInf W)
H : z = w₀
y : ℝ
hy1 : w₀ < y
hy2 : Set.Ico z y ⊆ S
a : ℝ
ha : a ∈ W
⊢ y ≤ a

State before:
S : Set ℝ
h1 : ∀ x ∈ S, ∃ y, x < y ∧ Set.Ico x y ⊆ S
h2 : ∀ (x y : ℝ), x < y → Set.Ico x y ⊆ S → y ∈ S
z : ℝ
hz : z ∈ S
w₁ : ℝ
hw₁ : w₁ ∈ Set.Ici z
hw₁' : w₁ ∉ S
W : Set ℝ := {w | z ≤ w ∧ w ∉ S}
w₀ : ℝ := sInf W
hwne : W.Nonempty
h6 : w₀ ∈ lowerBounds W
hwbb : BddBelow W
h7 : Set.Ico z w₀ ⊆ S
h9 : ∀ w ∈ W, z ≤ w
h10 : z ≤ w₀
h13 : IsGLB W (sInf W)
H : z = w₀
y : ℝ
hy1 : w₀ < y
hy2 : Set.Ico z y ⊆ S
a : ℝ
ha : a ∈ W
⊢ y ≤ a
Tactic:
by_contra H'
State after:
S : Set ℝ
h1 : ∀ x ∈ S, ∃ y, x < y ∧ Set.Ico x y ⊆ S
h2 : ∀ (x y : ℝ), x < y → Set.Ico x y ⊆ S → y ∈ S
z : ℝ
hz : z ∈ S
w₁ : ℝ
hw₁ : w₁ ∈ Set.Ici z
hw₁' : w₁ ∉ S
W : Set ℝ := {w | z ≤ w ∧ w ∉ S}
w₀ : ℝ := sInf W
hwne : W.Nonempty
h6 : w₀ ∈ lowerBounds W
hwbb : BddBelow W
h7 : Set.Ico z w₀ ⊆ S
h9 : ∀ w ∈ W, z ≤ w
h10 : z ≤ w₀
h13 : IsGLB W (sInf W)
H : z = w₀
y : ℝ
hy1 : w₀ < y
hy2 : Set.Ico z y ⊆ S
a : ℝ
ha : a ∈ W
H' : ¬y ≤ a
⊢ False

State before:
S : Set ℝ
h1 : ∀ x ∈ S, ∃ y, x < y ∧ Set.Ico x y ⊆ S
h2 : ∀ (x y : ℝ), x < y → Set.Ico x y ⊆ S → y ∈ S
z : ℝ
hz : z ∈ S
w₁ : ℝ
hw₁ : w₁ ∈ Set.Ici z
hw₁' : w₁ ∉ S
W : Set ℝ := {w | z ≤ w ∧ w ∉ S}
w₀ : ℝ := sInf W
hwne : W.Nonempty
h6 : w₀ ∈ lowerBounds W
hwbb : BddBelow W
h7 : Set.Ico z w₀ ⊆ S
h9 : ∀ w ∈ W, z ≤ w
h10 : z ≤ w₀
h13 : IsGLB W (sInf W)
H : z = w₀
y : ℝ
hy1 : w₀ < y
hy2 : Set.Ico z y ⊆ S
a : ℝ
ha : a ∈ W
H' : ¬y ≤ a
⊢ False
Tactic:
push_neg at H'
State after:
S : Set ℝ
h1 : ∀ x ∈ S, ∃ y, x < y ∧ Set.Ico x y ⊆ S
h2 : ∀ (x y : ℝ), x < y → Set.Ico x y ⊆ S → y ∈ S
z : ℝ
hz : z ∈ S
w₁ : ℝ
hw₁ : w₁ ∈ Set.Ici z
hw₁' : w₁ ∉ S
W : Set ℝ := {w | z ≤ w ∧ w ∉ S}
w₀ : ℝ := sInf W
hwne : W.Nonempty
h6 : w₀ ∈ lowerBounds W
hwbb : BddBelow W
h7 : Set.Ico z w₀ ⊆ S
h9 : ∀ w ∈ W, z ≤ w
h10 : z ≤ w₀
h13 : IsGLB W (sInf W)
H : z = w₀
y : ℝ
hy1 : w₀ < y
hy2 : Set.Ico z y ⊆ S
a : ℝ
ha : a ∈ W
H' : a < y
⊢ False

State before:
S : Set ℝ
h1 : ∀ x ∈ S, ∃ y, x < y ∧ Set.Ico x y ⊆ S
h2 : ∀ (x y : ℝ), x < y → Set.Ico x y ⊆ S → y ∈ S
z : ℝ
hz : z ∈ S
w₁ : ℝ
hw₁ : w₁ ∈ Set.Ici z
hw₁' : w₁ ∉ S
W : Set ℝ := {w | z ≤ w ∧ w ∉ S}
w₀ : ℝ := sInf W
hwne : W.Nonempty
h6 : w₀ ∈ lowerBounds W
hwbb : BddBelow W
h7 : Set.Ico z w₀ ⊆ S
h9 : ∀ w ∈ W, z ≤ w
h10 : z ≤ w₀
h13 : IsGLB W (sInf W)
H : z = w₀
y : ℝ
hy1 : w₀ < y
hy2 : Set.Ico z y ⊆ S
a : ℝ
ha : a ∈ W
H' : a < y
⊢ False
Tactic:
exact ha.2 (hy2 ⟨h9 a ha, H'⟩)
State after:
no goals

State before:
S : Set ℝ
h1 : ∀ x ∈ S, ∃ y, x < y ∧ Set.Ico x y ⊆ S
h2 : ∀ (x y : ℝ), x < y → Set.Ico x y ⊆ S → y ∈ S
z : ℝ
hz : z ∈ S
w₁ : ℝ
hw₁ : w₁ ∈ Set.Ici z
hw₁' : w₁ ∉ S
W : Set ℝ := {w | z ≤ w ∧ w ∉ S}
w₀ : ℝ := sInf W
hwne : W.Nonempty
h6 : z ∈ lowerBounds W
hwbb : BddBelow W
h7 : Set.Ico z w₀ ⊆ S
h9 : ∀ w ∈ W, z ≤ w
h10 : z ≤ w₀
h13 : IsGLB W (sInf W)
h11 : z ≠ w₀
h15 : z < w₀
h8 : w₀ ∈ S
y : ℝ
hwy : w₀ < y
hy : Set.Ico w₀ y ⊆ S
⊢ y ∈ lowerBounds W
Tactic:
intro a ha
State after:
S : Set ℝ
h1 : ∀ x ∈ S, ∃ y, x < y ∧ Set.Ico x y ⊆ S
h2 : ∀ (x y : ℝ), x < y → Set.Ico x y ⊆ S → y ∈ S
z : ℝ
hz : z ∈ S
w₁ : ℝ
hw₁ : w₁ ∈ Set.Ici z
hw₁' : w₁ ∉ S
W : Set ℝ := {w | z ≤ w ∧ w ∉ S}
w₀ : ℝ := sInf W
hwne : W.Nonempty
h6 : z ∈ lowerBounds W
hwbb : BddBelow W
h7 : Set.Ico z w₀ ⊆ S
h9 : ∀ w ∈ W, z ≤ w
h10 : z ≤ w₀
h13 : IsGLB W (sInf W)
h11 : z ≠ w₀
h15 : z < w₀
h8 : w₀ ∈ S
y : ℝ
hwy : w₀ < y
hy : Set.Ico w₀ y ⊆ S
a : ℝ
ha : a ∈ W
⊢ y ≤ a

State before:
S : Set ℝ
h1 : ∀ x ∈ S, ∃ y, x < y ∧ Set.Ico x y ⊆ S
h2 : ∀ (x y : ℝ), x < y → Set.Ico x y ⊆ S → y ∈ S
z : ℝ
hz : z ∈ S
w₁ : ℝ
hw₁ : w₁ ∈ Set.Ici z
hw₁' : w₁ ∉ S
W : Set ℝ := {w | z ≤ w ∧ w ∉ S}
w₀ : ℝ := sInf W
hwne : W.Nonempty
h6 : z ∈ lowerBounds W
hwbb : BddBelow W
h7 : Set.Ico z w₀ ⊆ S
h9 : ∀ w ∈ W, z ≤ w
h10 : z ≤ w₀
h13 : IsGLB W (sInf W)
h11 : z ≠ w₀
h15 : z < w₀
h8 : w₀ ∈ S
y : ℝ
hwy : w₀ < y
hy : Set.Ico w₀ y ⊆ S
a : ℝ
ha : a ∈ W
⊢ y ≤ a
Tactic:
by_contra H'
State after:
S : Set ℝ
h1 : ∀ x ∈ S, ∃ y, x < y ∧ Set.Ico x y ⊆ S
h2 : ∀ (x y : ℝ), x < y → Set.Ico x y ⊆ S → y ∈ S
z : ℝ
hz : z ∈ S
w₁ : ℝ
hw₁ : w₁ ∈ Set.Ici z
hw₁' : w₁ ∉ S
W : Set ℝ := {w | z ≤ w ∧ w ∉ S}
w₀ : ℝ := sInf W
hwne : W.Nonempty
h6 : z ∈ lowerBounds W
hwbb : BddBelow W
h7 : Set.Ico z w₀ ⊆ S
h9 : ∀ w ∈ W, z ≤ w
h10 : z ≤ w₀
h13 : IsGLB W (sInf W)
h11 : z ≠ w₀
h15 : z < w₀
h8 : w₀ ∈ S
y : ℝ
hwy : w₀ < y
hy : Set.Ico w₀ y ⊆ S
a : ℝ
ha : a ∈ W
H' : ¬y ≤ a
⊢ False

State before:
S : Set ℝ
h1 : ∀ x ∈ S, ∃ y, x < y ∧ Set.Ico x y ⊆ S
h2 : ∀ (x y : ℝ), x < y → Set.Ico x y ⊆ S → y ∈ S
z : ℝ
hz : z ∈ S
w₁ : ℝ
hw₁ : w₁ ∈ Set.Ici z
hw₁' : w₁ ∉ S
W : Set ℝ := {w | z ≤ w ∧ w ∉ S}
w₀ : ℝ := sInf W
hwne : W.Nonempty
h6 : z ∈ lowerBounds W
hwbb : BddBelow W
h7 : Set.Ico z w₀ ⊆ S
h9 : ∀ w ∈ W, z ≤ w
h10 : z ≤ w₀
h13 : IsGLB W (sInf W)
h11 : z ≠ w₀
h15 : z < w₀
h8 : w₀ ∈ S
y : ℝ
hwy : w₀ < y
hy : Set.Ico w₀ y ⊆ S
a : ℝ
ha : a ∈ W
H' : ¬y ≤ a
⊢ False
Tactic:
push_neg at H'
State after:
S : Set ℝ
h1 : ∀ x ∈ S, ∃ y, x < y ∧ Set.Ico x y ⊆ S
h2 : ∀ (x y : ℝ), x < y → Set.Ico x y ⊆ S → y ∈ S
z : ℝ
hz : z ∈ S
w₁ : ℝ
hw₁ : w₁ ∈ Set.Ici z
hw₁' : w₁ ∉ S
W : Set ℝ := {w | z ≤ w ∧ w ∉ S}
w₀ : ℝ := sInf W
hwne : W.Nonempty
h6 : z ∈ lowerBounds W
hwbb : BddBelow W
h7 : Set.Ico z w₀ ⊆ S
h9 : ∀ w ∈ W, z ≤ w
h10 : z ≤ w₀
h13 : IsGLB W (sInf W)
h11 : z ≠ w₀
h15 : z < w₀
h8 : w₀ ∈ S
y : ℝ
hwy : w₀ < y
hy : Set.Ico w₀ y ⊆ S
a : ℝ
ha : a ∈ W
H' : a < y
⊢ False

State before:
S : Set ℝ
h1 : ∀ x ∈ S, ∃ y, x < y ∧ Set.Ico x y ⊆ S
h2 : ∀ (x y : ℝ), x < y → Set.Ico x y ⊆ S → y ∈ S
z : ℝ
hz : z ∈ S
w₁ : ℝ
hw₁ : w₁ ∈ Set.Ici z
hw₁' : w₁ ∉ S
W : Set ℝ := {w | z ≤ w ∧ w ∉ S}
w₀ : ℝ := sInf W
hwne : W.Nonempty
h6 : z ∈ lowerBounds W
hwbb : BddBelow W
h7 : Set.Ico z w₀ ⊆ S
h9 : ∀ w ∈ W, z ≤ w
h10 : z ≤ w₀
h13 : IsGLB W (sInf W)
h11 : z ≠ w₀
h15 : z < w₀
h8 : w₀ ∈ S
y : ℝ
hwy : w₀ < y
hy : Set.Ico w₀ y ⊆ S
a : ℝ
ha : a ∈ W
H' : a < y
⊢ False
Tactic:
apply ha.2
State after:
S : Set ℝ
h1 : ∀ x ∈ S, ∃ y, x < y ∧ Set.Ico x y ⊆ S
h2 : ∀ (x y : ℝ), x < y → Set.Ico x y ⊆ S → y ∈ S
z : ℝ
hz : z ∈ S
w₁ : ℝ
hw₁ : w₁ ∈ Set.Ici z
hw₁' : w₁ ∉ S
W : Set ℝ := {w | z ≤ w ∧ w ∉ S}
w₀ : ℝ := sInf W
hwne : W.Nonempty
h6 : z ∈ lowerBounds W
hwbb : BddBelow W
h7 : Set.Ico z w₀ ⊆ S
h9 : ∀ w ∈ W, z ≤ w
h10 : z ≤ w₀
h13 : IsGLB W (sInf W)
h11 : z ≠ w₀
h15 : z < w₀
h8 : w₀ ∈ S
y : ℝ
hwy : w₀ < y
hy : Set.Ico w₀ y ⊆ S
a : ℝ
ha : a ∈ W
H' : a < y
⊢ a ∈ S

State before:
S : Set ℝ
h1 : ∀ x ∈ S, ∃ y, x < y ∧ Set.Ico x y ⊆ S
h2 : ∀ (x y : ℝ), x < y → Set.Ico x y ⊆ S → y ∈ S
z : ℝ
hz : z ∈ S
w₁ : ℝ
hw₁ : w₁ ∈ Set.Ici z
hw₁' : w₁ ∉ S
W : Set ℝ := {w | z ≤ w ∧ w ∉ S}
w₀ : ℝ := sInf W
hwne : W.Nonempty
h6 : z ∈ lowerBounds W
hwbb : BddBelow W
h7 : Set.Ico z w₀ ⊆ S
h9 : ∀ w ∈ W, z ≤ w
h10 : z ≤ w₀
h13 : IsGLB W (sInf W)
h11 : z ≠ w₀
h15 : z < w₀
h8 : w₀ ∈ S
y : ℝ
hwy : w₀ < y
hy : Set.Ico w₀ y ⊆ S
a : ℝ
ha : a ∈ W
H' : a < y
⊢ a ∈ S
Tactic:
obtain hlt | hle := lt_or_le a w₀
State after:
case inl
S : Set ℝ
h1 : ∀ x ∈ S, ∃ y, x < y ∧ Set.Ico x y ⊆ S
h2 : ∀ (x y : ℝ), x < y → Set.Ico x y ⊆ S → y ∈ S
z : ℝ
hz : z ∈ S
w₁ : ℝ
hw₁ : w₁ ∈ Set.Ici z
hw₁' : w₁ ∉ S
W : Set ℝ := {w | z ≤ w ∧ w ∉ S}
w₀ : ℝ := sInf W
hwne : W.Nonempty
h6 : z ∈ lowerBounds W
hwbb : BddBelow W
h7 : Set.Ico z w₀ ⊆ S
h9 : ∀ w ∈ W, z ≤ w
h10 : z ≤ w₀
h13 : IsGLB W (sInf W)
h11 : z ≠ w₀
h15 : z < w₀
h8 : w₀ ∈ S
y : ℝ
hwy : w₀ < y
hy : Set.Ico w₀ y ⊆ S
a : ℝ
ha : a ∈ W
H' : a < y
hlt : a < w₀
⊢ a ∈ S

case inr
S : Set ℝ
h1 : ∀ x ∈ S, ∃ y, x < y ∧ Set.Ico x y ⊆ S
h2 : ∀ (x y : ℝ), x < y → Set.Ico x y ⊆ S → y ∈ S
z : ℝ
hz : z ∈ S
w₁ : ℝ
hw₁ : w₁ ∈ Set.Ici z
hw₁' : w₁ ∉ S
W : Set ℝ := {w | z ≤ w ∧ w ∉ S}
w₀ : ℝ := sInf W
hwne : W.Nonempty
h6 : z ∈ lowerBounds W
hwbb : BddBelow W
h7 : Set.Ico z w₀ ⊆ S
h9 : ∀ w ∈ W, z ≤ w
h10 : z ≤ w₀
h13 : IsGLB W (sInf W)
h11 : z ≠ w₀
h15 : z < w₀
h8 : w₀ ∈ S
y : ℝ
hwy : w₀ < y
hy : Set.Ico w₀ y ⊆ S
a : ℝ
ha : a ∈ W
H' : a < y
hle : w₀ ≤ a
⊢ a ∈ S

State before:
case inl
S : Set ℝ
h1 : ∀ x ∈ S, ∃ y, x < y ∧ Set.Ico x y ⊆ S
h2 : ∀ (x y : ℝ), x < y → Set.Ico x y ⊆ S → y ∈ S
z : ℝ
hz : z ∈ S
w₁ : ℝ
hw₁ : w₁ ∈ Set.Ici z
hw₁' : w₁ ∉ S
W : Set ℝ := {w | z ≤ w ∧ w ∉ S}
w₀ : ℝ := sInf W
hwne : W.Nonempty
h6 : z ∈ lowerBounds W
hwbb : BddBelow W
h7 : Set.Ico z w₀ ⊆ S
h9 : ∀ w ∈ W, z ≤ w
h10 : z ≤ w₀
h13 : IsGLB W (sInf W)
h11 : z ≠ w₀
h15 : z < w₀
h8 : w₀ ∈ S
y : ℝ
hwy : w₀ < y
hy : Set.Ico w₀ y ⊆ S
a : ℝ
ha : a ∈ W
H' : a < y
hlt : a < w₀
⊢ a ∈ S
Tactic:
exact h7 ⟨ha.1, hlt⟩
State after:
no goals

State before:
case inr
S : Set ℝ
h1 : ∀ x ∈ S, ∃ y, x < y ∧ Set.Ico x y ⊆ S
h2 : ∀ (x y : ℝ), x < y → Set.Ico x y ⊆ S → y ∈ S
z : ℝ
hz : z ∈ S
w₁ : ℝ
hw₁ : w₁ ∈ Set.Ici z
hw₁' : w₁ ∉ S
W : Set ℝ := {w | z ≤ w ∧ w ∉ S}
w₀ : ℝ := sInf W
hwne : W.Nonempty
h6 : z ∈ lowerBounds W
hwbb : BddBelow W
h7 : Set.Ico z w₀ ⊆ S
h9 : ∀ w ∈ W, z ≤ w
h10 : z ≤ w₀
h13 : IsGLB W (sInf W)
h11 : z ≠ w₀
h15 : z < w₀
h8 : w₀ ∈ S
y : ℝ
hwy : w₀ < y
hy : Set.Ico w₀ y ⊆ S
a : ℝ
ha : a ∈ W
H' : a < y
hle : w₀ ≤ a
⊢ a ∈ S
Tactic:
exact hy ⟨hle, H'⟩
State after:
no goals