internlm/Lean-Github huggingface dataset:
Theorem: UpperLowerContinuous.real_induction
Proof 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
Proof 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
Theorem: UpperLowerContinuous.real_induction
Proof 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
Proof 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
Theorem: UpperLowerContinuous.real_induction
Proof 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}
Proof 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
Theorem: UpperLowerContinuous.real_induction
Proof 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
Proof 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
Theorem: UpperLowerContinuous.real_induction
Proof 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₁'⟩
Proof 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
Theorem: UpperLowerContinuous.real_induction
Proof 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
Proof 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
Theorem: UpperLowerContinuous.real_induction
Proof 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
Proof 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
Theorem: UpperLowerContinuous.real_induction
Proof 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⟩)
Proof 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
Theorem: UpperLowerContinuous.real_induction
Proof 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
Proof 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
Theorem: UpperLowerContinuous.real_induction
Proof 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
Proof 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
Theorem: UpperLowerContinuous.real_induction
Proof 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
Proof 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
Theorem: UpperLowerContinuous.real_induction
Proof 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)
Proof 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
Theorem: UpperLowerContinuous.real_induction
Proof 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
Proof 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
Theorem: UpperLowerContinuous.real_induction
Proof 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
Proof 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
Theorem: UpperLowerContinuous.real_induction
Proof 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
Proof 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
Theorem: UpperLowerContinuous.real_induction
Proof 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)
Proof state after:
no goals
Theorem: UpperLowerContinuous.real_induction
Proof 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
Proof 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
Theorem: UpperLowerContinuous.real_induction
Proof 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
Proof 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
Theorem: UpperLowerContinuous.real_induction
Proof 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⟩)
Proof state after:
no goals
Theorem: UpperLowerContinuous.real_induction
Proof 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
Proof 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
Theorem: UpperLowerContinuous.real_induction
Proof 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
Proof 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
Theorem: UpperLowerContinuous.real_induction
Proof 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
Proof 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
Theorem: UpperLowerContinuous.real_induction
Proof 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'⟩)
Proof 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
Theorem: UpperLowerContinuous.real_induction
Proof 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)
Proof state after:
no goals
Theorem: UpperLowerContinuous.real_induction
Proof 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
Proof 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
Theorem: UpperLowerContinuous.real_induction
Proof 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'
Proof 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
Theorem: UpperLowerContinuous.real_induction
Proof 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'
Proof 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
Theorem: UpperLowerContinuous.real_induction
Proof 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'⟩)
Proof state after:
no goals
Theorem: UpperLowerContinuous.real_induction
Proof 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
Proof 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
Theorem: UpperLowerContinuous.real_induction
Proof 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'
Proof 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