internlm/Lean-Github huggingface dataset:
Theorem: push_le_push
Proof state before:
case mp
A B : Finset ℕ
AB : ∀ ⦃x : ℕ⦄, x ∈ insert 0 (Finset.image (fun n => n + 1) A) → x ∈ insert 0 (Finset.image (fun n => n + 1) B)
x : ℕ
xA : x ∈ A
h : x + 1 ∈ insert 0 (Finset.image (fun n => n + 1) A)
⊢ x ∈ B
Tactic:
specialize AB h
Proof state after:
case mp
A B : Finset ℕ
x : ℕ
xA : x ∈ A
h : x + 1 ∈ insert 0 (Finset.image (fun n => n + 1) A)
AB : x + 1 ∈ insert 0 (Finset.image (fun n => n + 1) B)
⊢ x ∈ B
Theorem: push_le_push
Proof state before:
case mp
A B : Finset ℕ
x : ℕ
xA : x ∈ A
h : x + 1 ∈ insert 0 (Finset.image (fun n => n + 1) A)
AB : x + 1 ∈ insert 0 (Finset.image (fun n => n + 1) B)
⊢ x ∈ B
Tactic:
simp at AB
Proof state after:
case mp
A B : Finset ℕ
x : ℕ
xA : x ∈ A
h : x + 1 ∈ insert 0 (Finset.image (fun n => n + 1) A)
AB : x ∈ B
⊢ x ∈ B
Theorem: push_le_push
Proof state before:
case mp
A B : Finset ℕ
x : ℕ
xA : x ∈ A
h : x + 1 ∈ insert 0 (Finset.image (fun n => n + 1) A)
AB : x ∈ B
⊢ x ∈ B
Tactic:
assumption
Proof state after:
no goals
Theorem: push_le_push
Proof state before:
A B : Finset ℕ
AB : ∀ ⦃x : ℕ⦄, x ∈ insert 0 (Finset.image (fun n => n + 1) A) → x ∈ insert 0 (Finset.image (fun n => n + 1) B)
x : ℕ
xA : x ∈ A
⊢ x + 1 ∈ insert 0 (Finset.image (fun n => n + 1) A)
Tactic:
simpa
Proof state after:
no goals
Theorem: push_le_push
Proof state before:
case mpr
A B : Finset ℕ
⊢ A ⊆ B → insert 0 (Finset.image (fun n => n + 1) A) ⊆ insert 0 (Finset.image (fun n => n + 1) B)
Tactic:
intro AB
Proof state after:
case mpr
A B : Finset ℕ
AB : A ⊆ B
⊢ insert 0 (Finset.image (fun n => n + 1) A) ⊆ insert 0 (Finset.image (fun n => n + 1) B)
Theorem: push_le_push
Proof state before:
case mpr
A B : Finset ℕ
AB : A ⊆ B
⊢ insert 0 (Finset.image (fun n => n + 1) A) ⊆ insert 0 (Finset.image (fun n => n + 1) B)
Tactic:
apply Finset.insert_subset_insert
Proof state after:
case mpr.h
A B : Finset ℕ
AB : A ⊆ B
⊢ Finset.image (fun n => n + 1) A ⊆ Finset.image (fun n => n + 1) B
Theorem: push_le_push
Proof state before:
case mpr.h
A B : Finset ℕ
AB : A ⊆ B
⊢ Finset.image (fun n => n + 1) A ⊆ Finset.image (fun n => n + 1) B
Tactic:
apply Finset.image_mono
Proof state after:
case mpr.h.a
A B : Finset ℕ
AB : A ⊆ B
⊢ A ≤ B
Theorem: push_le_push
Proof state before:
case mpr.h.a
A B : Finset ℕ
AB : A ⊆ B
⊢ A ≤ B
Tactic:
assumption
Proof state after:
no goals
Theorem: push_sum
Proof state before:
X : Type
inst✝ : AddCommGroup X
a : X
f : ℕ → X
N : Finset ℕ
⊢ a + N.sum f = (push N).sum (cons a f)
Tactic:
rw [push]
Proof state after:
X : Type
inst✝ : AddCommGroup X
a : X
f : ℕ → X
N : Finset ℕ
⊢ a + N.sum f = (insert 0 (Finset.image (fun n => n + 1) N)).sum (cons a f)
Theorem: push_sum
Proof state before:
X : Type
inst✝ : AddCommGroup X
a : X
f : ℕ → X
N : Finset ℕ
⊢ a + N.sum f = (insert 0 (Finset.image (fun n => n + 1) N)).sum (cons a f)
Tactic:
simp
Proof state after:
X : Type
inst✝ : AddCommGroup X
a : X
f : ℕ → X
N : Finset ℕ
⊢ a + N.sum f = cons a f 0 + N.sum fun x => cons a f (x + 1)
Theorem: push_sum
Proof state before:
X : Type
inst✝ : AddCommGroup X
a : X
f : ℕ → X
N : Finset ℕ
⊢ a + N.sum f = cons a f 0 + N.sum fun x => cons a f (x + 1)
Tactic:
rfl
Proof state after:
no goals
Theorem: push_prod
Proof state before:
a : ℂ
f : ℕ → ℂ
N : Finset ℕ
⊢ a * N.prod f = (push N).prod (cons a f)
Tactic:
rw [push]
Proof state after:
a : ℂ
f : ℕ → ℂ
N : Finset ℕ
⊢ a * N.prod f = (insert 0 (Finset.image (fun n => n + 1) N)).prod (cons a f)
Theorem: push_prod
Proof state before:
a : ℂ
f : ℕ → ℂ
N : Finset ℕ
⊢ a * N.prod f = (insert 0 (Finset.image (fun n => n + 1) N)).prod (cons a f)
Tactic:
simp
Proof state after:
a : ℂ
f : ℕ → ℂ
N : Finset ℕ
⊢ a * N.prod f = cons a f 0 * N.prod fun x => cons a f (x + 1)
Theorem: push_prod
Proof state before:
a : ℂ
f : ℕ → ℂ
N : Finset ℕ
⊢ a * N.prod f = cons a f 0 * N.prod fun x => cons a f (x + 1)
Tactic:
rfl
Proof state after:
no goals
Theorem: push_range
Proof state before:
⊢ Set.range push = {N | 0 ∈ N}
Tactic:
rw [Set.range]
Proof state after:
⊢ {x | ∃ y, push y = x} = {N | 0 ∈ N}
Theorem: push_range
Proof state before:
⊢ {x | ∃ y, push y = x} = {N | 0 ∈ N}
Tactic:
apply Set.ext
Proof state after:
case h

⊢ ∀ (x : Finset ℕ), x ∈ {x | ∃ y, push y = x} ↔ x ∈ {N | 0 ∈ N}
Theorem: push_range
Proof state before:
case h

⊢ ∀ (x : Finset ℕ), x ∈ {x | ∃ y, push y = x} ↔ x ∈ {N | 0 ∈ N}
Tactic:
simp
Proof state after:
case h

⊢ ∀ (x : Finset ℕ), (∃ y, push y = x) ↔ 0 ∈ x
Theorem: push_range
Proof state before:
case h

⊢ ∀ (x : Finset ℕ), (∃ y, push y = x) ↔ 0 ∈ x
Tactic:
intro N
Proof state after:
case h
N : Finset ℕ
⊢ (∃ y, push y = N) ↔ 0 ∈ N
Theorem: push_range
Proof state before:
case h
N : Finset ℕ
⊢ (∃ y, push y = N) ↔ 0 ∈ N
Tactic:
constructor
Proof state after:
case h.mp
N : Finset ℕ
⊢ (∃ y, push y = N) → 0 ∈ N

case h.mpr
N : Finset ℕ
⊢ 0 ∈ N → ∃ y, push y = N
Theorem: push_range
Proof state before:
case h.mp
N : Finset ℕ
⊢ (∃ y, push y = N) → 0 ∈ N
Tactic:
intro h
Proof state after:
case h.mp
N : Finset ℕ
h : ∃ y, push y = N
⊢ 0 ∈ N
Theorem: push_range
Proof state before:
case h.mp
N : Finset ℕ
h : ∃ y, push y = N
⊢ 0 ∈ N
Tactic:
rcases h with ⟨M, H⟩
Proof state after:
case h.mp.intro
N M : Finset ℕ
H : push M = N
⊢ 0 ∈ N
Theorem: push_range
Proof state before:
case h.mp.intro
N M : Finset ℕ
H : push M = N
⊢ 0 ∈ N
Tactic:
rw [push] at H
Proof state after:
case h.mp.intro
N M : Finset ℕ
H : insert 0 (Finset.image (fun n => n + 1) M) = N
⊢ 0 ∈ N
Theorem: push_range
Proof state before:
case h.mp.intro
N M : Finset ℕ
H : insert 0 (Finset.image (fun n => n + 1) M) = N
⊢ 0 ∈ N
Tactic:
rw [← H]
Proof state after:
case h.mp.intro
N M : Finset ℕ
H : insert 0 (Finset.image (fun n => n + 1) M) = N
⊢ 0 ∈ insert 0 (Finset.image (fun n => n + 1) M)
Theorem: push_range
Proof state before:
case h.mp.intro
N M : Finset ℕ
H : insert 0 (Finset.image (fun n => n + 1) M) = N
⊢ 0 ∈ insert 0 (Finset.image (fun n => n + 1) M)
Tactic:
exact Finset.mem_insert_self 0 _
Proof state after:
no goals
Theorem: push_range
Proof state before:
case h.mpr
N : Finset ℕ
⊢ 0 ∈ N → ∃ y, push y = N
Tactic:
intro N0
Proof state after:
case h.mpr
N : Finset ℕ
N0 : 0 ∈ N
⊢ ∃ y, push y = N
Theorem: push_range
Proof state before:
case h.mpr
N : Finset ℕ
N0 : 0 ∈ N
⊢ ∃ y, push y = N
Tactic:
exists pop N
Proof state after:
case h.mpr
N : Finset ℕ
N0 : 0 ∈ N
⊢ push (pop N) = N
Theorem: push_range
Proof state before:
case h.mpr
N : Finset ℕ
N0 : 0 ∈ N
⊢ push (pop N) = N
Tactic:
rw [push_pop]
Proof state after:
case h.mpr
N : Finset ℕ
N0 : 0 ∈ N
⊢ insert 0 N = N
Theorem: push_range
Proof state before:
case h.mpr
N : Finset ℕ
N0 : 0 ∈ N
⊢ insert 0 N = N
Tactic:
exact Finset.insert_eq_of_mem N0
Proof state after:
no goals
Theorem: push_comap_atTop
Proof state before:
⊢ Filter.comap push atTop = atTop
Tactic:
apply Filter.comap_embedding_atTop
Proof state after:
case hm

⊢ ∀ (b₁ b₂ : Finset ℕ), push b₁ ≤ push b₂ ↔ b₁ ≤ b₂

case hu

⊢ ∀ (c : Finset ℕ), ∃ b, c ≤ push b
Theorem: push_comap_atTop
Proof state before:
case hm

⊢ ∀ (b₁ b₂ : Finset ℕ), push b₁ ≤ push b₂ ↔ b₁ ≤ b₂

case hu

⊢ ∀ (c : Finset ℕ), ∃ b, c ≤ push b
Tactic:
exact @push_le_push
Proof state after:
case hu

⊢ ∀ (c : Finset ℕ), ∃ b, c ≤ push b
Theorem: push_comap_atTop
Proof state before:
case hu

⊢ ∀ (c : Finset ℕ), ∃ b, c ≤ push b
Tactic:
intro N
Proof state after:
case hu
N : Finset ℕ
⊢ ∃ b, N ≤ push b
Theorem: push_comap_atTop
Proof state before:
case hu
N : Finset ℕ
⊢ ∃ b, N ≤ push b
Tactic:
exists pop N
Proof state after:
case hu
N : Finset ℕ
⊢ N ≤ push (pop N)
Theorem: push_comap_atTop
Proof state before:
case hu
N : Finset ℕ
⊢ N ≤ push (pop N)
Tactic:
rw [push_pop]
Proof state after:
case hu
N : Finset ℕ
⊢ N ≤ insert 0 N
Theorem: push_comap_atTop
Proof state before:
case hu
N : Finset ℕ
⊢ N ≤ insert 0 N
Tactic:
simp
Proof state after:
no goals
Theorem: tendsto_comp_push
Proof state before:
A : Type
f : Finset ℕ → A
l : Filter A
⊢ Filter.Tendsto (f ∘ push) atTop l ↔ Filter.Tendsto f atTop l
Tactic:
nth_rw 1 [← push_comap_atTop]
Proof state after:
A : Type
f : Finset ℕ → A
l : Filter A
⊢ Filter.Tendsto (f ∘ push) (Filter.comap push atTop) l ↔ Filter.Tendsto f atTop l
Theorem: tendsto_comp_push
Proof state before:
A : Type
f : Finset ℕ → A
l : Filter A
⊢ Filter.Tendsto (f ∘ push) (Filter.comap push atTop) l ↔ Filter.Tendsto f atTop l
Tactic:
apply Filter.tendsto_comap'_iff
Proof state after:
case h
A : Type
f : Finset ℕ → A
l : Filter A
⊢ Set.range push ∈ atTop
Theorem: tendsto_comp_push
Proof state before:
case h
A : Type
f : Finset ℕ → A
l : Filter A
⊢ Set.range push ∈ atTop
Tactic:
rw [push_range]
Proof state after:
case h
A : Type
f : Finset ℕ → A
l : Filter A
⊢ {N | 0 ∈ N} ∈ atTop
Theorem: tendsto_comp_push
Proof state before:
case h
A : Type
f : Finset ℕ → A
l : Filter A
⊢ {N | 0 ∈ N} ∈ atTop
Tactic:
have h : {N : Finset ℕ | 0 ∈ N} = {N : Finset ℕ | {0} ≤ N} := by simp
Proof state after:
case h
A : Type
f : Finset ℕ → A
l : Filter A
h : {N | 0 ∈ N} = {N | {0} ≤ N}
⊢ {N | 0 ∈ N} ∈ atTop
Theorem: tendsto_comp_push
Proof state before:
case h
A : Type
f : Finset ℕ → A
l : Filter A
h : {N | 0 ∈ N} = {N | {0} ≤ N}
⊢ {N | 0 ∈ N} ∈ atTop
Tactic:
rw [h]
Proof state after:
case h
A : Type
f : Finset ℕ → A
l : Filter A
h : {N | 0 ∈ N} = {N | {0} ≤ N}
⊢ {N | {0} ≤ N} ∈ atTop
Theorem: tendsto_comp_push
Proof state before:
case h
A : Type
f : Finset ℕ → A
l : Filter A
h : {N | 0 ∈ N} = {N | {0} ≤ N}
⊢ {N | {0} ≤ N} ∈ atTop
Tactic:
exact Filter.mem_atTop _
Proof state after:
no goals
Theorem: tendsto_comp_push
Proof state before:
A : Type
f : Finset ℕ → A
l : Filter A
⊢ {N | 0 ∈ N} = {N | {0} ≤ N}
Tactic:
simp
Proof state after:
no goals
Theorem: finset_complex_abs_sum_le
Proof state before:
N : Finset ℕ
f : ℕ → ℂ
⊢ Complex.abs (N.sum fun n => f n) ≤ N.sum fun n => Complex.abs (f n)
Tactic:
induction' N using Finset.induction with n N Nn h
Proof state after:
case empty
f : ℕ → ℂ
⊢ Complex.abs (∅.sum fun n => f n) ≤ ∅.sum fun n => Complex.abs (f n)

case insert
f : ℕ → ℂ
n : ℕ
N : Finset ℕ
Nn : n ∉ N
h : Complex.abs (N.sum fun n => f n) ≤ N.sum fun n => Complex.abs (f n)
⊢ Complex.abs ((insert n N).sum fun n => f n) ≤ (insert n N).sum fun n => Complex.abs (f n)
Theorem: finset_complex_abs_sum_le
Proof state before:
case empty
f : ℕ → ℂ
⊢ Complex.abs (∅.sum fun n => f n) ≤ ∅.sum fun n => Complex.abs (f n)
Tactic:
simp
Proof state after:
no goals
Theorem: finset_complex_abs_sum_le
Proof state before:
case insert
f : ℕ → ℂ
n : ℕ
N : Finset ℕ
Nn : n ∉ N
h : Complex.abs (N.sum fun n => f n) ≤ N.sum fun n => Complex.abs (f n)
⊢ Complex.abs ((insert n N).sum fun n => f n) ≤ (insert n N).sum fun n => Complex.abs (f n)
Tactic:
rw [Finset.sum_insert Nn]
Proof state after:
case insert
f : ℕ → ℂ
n : ℕ
N : Finset ℕ
Nn : n ∉ N
h : Complex.abs (N.sum fun n => f n) ≤ N.sum fun n => Complex.abs (f n)
⊢ Complex.abs (f n + N.sum fun x => f x) ≤ (insert n N).sum fun n => Complex.abs (f n)
Theorem: finset_complex_abs_sum_le
Proof state before:
case insert
f : ℕ → ℂ
n : ℕ
N : Finset ℕ
Nn : n ∉ N
h : Complex.abs (N.sum fun n => f n) ≤ N.sum fun n => Complex.abs (f n)
⊢ Complex.abs (f n + N.sum fun x => f x) ≤ (insert n N).sum fun n => Complex.abs (f n)
Tactic:
rw [Finset.sum_insert Nn]
Proof state after:
case insert
f : ℕ → ℂ
n : ℕ
N : Finset ℕ
Nn : n ∉ N
h : Complex.abs (N.sum fun n => f n) ≤ N.sum fun n => Complex.abs (f n)
⊢ Complex.abs (f n + N.sum fun x => f x) ≤ Complex.abs (f n) + N.sum fun x => Complex.abs (f x)
Theorem: finset_complex_abs_sum_le
Proof state before:
case insert
f : ℕ → ℂ
n : ℕ
N : Finset ℕ
Nn : n ∉ N
h : Complex.abs (N.sum fun n => f n) ≤ N.sum fun n => Complex.abs (f n)
⊢ Complex.abs (f n + N.sum fun x => f x) ≤ Complex.abs (f n) + N.sum fun x => Complex.abs (f x)
Tactic:
trans abs (f n) + abs (N.sum fun n ↦ f n)
Proof state after:
f : ℕ → ℂ
n : ℕ
N : Finset ℕ
Nn : n ∉ N
h : Complex.abs (N.sum fun n => f n) ≤ N.sum fun n => Complex.abs (f n)
⊢ Complex.abs (f n + N.sum fun x => f x) ≤ Complex.abs (f n) + Complex.abs (N.sum fun n => f n)

f : ℕ → ℂ
n : ℕ
N : Finset ℕ
Nn : n ∉ N
h : Complex.abs (N.sum fun n => f n) ≤ N.sum fun n => Complex.abs (f n)
⊢ Complex.abs (f n) + Complex.abs (N.sum fun n => f n) ≤ Complex.abs (f n) + N.sum fun x => Complex.abs (f x)
Theorem: finset_complex_abs_sum_le
Proof state before:
f : ℕ → ℂ
n : ℕ
N : Finset ℕ
Nn : n ∉ N
h : Complex.abs (N.sum fun n => f n) ≤ N.sum fun n => Complex.abs (f n)
⊢ Complex.abs (f n + N.sum fun x => f x) ≤ Complex.abs (f n) + Complex.abs (N.sum fun n => f n)
Tactic:
exact Complex.abs.add_le _ _
Proof state after:
no goals
Theorem: finset_complex_abs_sum_le
Proof state before:
f : ℕ → ℂ
n : ℕ
N : Finset ℕ
Nn : n ∉ N
h : Complex.abs (N.sum fun n => f n) ≤ N.sum fun n => Complex.abs (f n)
⊢ Complex.abs (f n) + Complex.abs (N.sum fun n => f n) ≤ Complex.abs (f n) + N.sum fun x => Complex.abs (f x)
Tactic:
apply add_le_add_left
Proof state after:
case bc
f : ℕ → ℂ
n : ℕ
N : Finset ℕ
Nn : n ∉ N
h : Complex.abs (N.sum fun n => f n) ≤ N.sum fun n => Complex.abs (f n)
⊢ Complex.abs (N.sum fun n => f n) ≤ N.sum fun x => Complex.abs (f x)
Theorem: finset_complex_abs_sum_le
Proof state before:
case bc
f : ℕ → ℂ
n : ℕ
N : Finset ℕ
Nn : n ∉ N
h : Complex.abs (N.sum fun n => f n) ≤ N.sum fun n => Complex.abs (f n)
⊢ Complex.abs (N.sum fun n => f n) ≤ N.sum fun x => Complex.abs (f x)
Tactic:
assumption
Proof state after:
no goals
Theorem: subset_union_sdiff
Proof state before:
A B : Finset ℕ
⊢ B ⊆ A ∪ B \ A
Tactic:
rw [Finset.subset_iff]
Proof state after:
A B : Finset ℕ
⊢ ∀ ⦃x : ℕ⦄, x ∈ B → x ∈ A ∪ B \ A
Theorem: subset_union_sdiff
Proof state before:
A B : Finset ℕ
⊢ ∀ ⦃x : ℕ⦄, x ∈ B → x ∈ A ∪ B \ A
Tactic:
intro x Bx
Proof state after:
A B : Finset ℕ
x : ℕ
Bx : x ∈ B
⊢ x ∈ A ∪ B \ A
Theorem: subset_union_sdiff
Proof state before:
A B : Finset ℕ
x : ℕ
Bx : x ∈ B
⊢ x ∈ A ∪ B \ A
Tactic:
rw [Finset.mem_union, Finset.mem_sdiff]
Proof state after:
A B : Finset ℕ
x : ℕ
Bx : x ∈ B
⊢ x ∈ A ∨ x ∈ B ∧ x ∉ A
Theorem: subset_union_sdiff
Proof state before:
A B : Finset ℕ
x : ℕ
Bx : x ∈ B
⊢ x ∈ A ∨ x ∈ B ∧ x ∉ A
Tactic:
by_cases Ax : x ∈ A
Proof state after:
case pos
A B : Finset ℕ
x : ℕ
Bx : x ∈ B
Ax : x ∈ A
⊢ x ∈ A ∨ x ∈ B ∧ x ∉ A

case neg
A B : Finset ℕ
x : ℕ
Bx : x ∈ B
Ax : x ∉ A
⊢ x ∈ A ∨ x ∈ B ∧ x ∉ A
Theorem: subset_union_sdiff
Proof state before:
case pos
A B : Finset ℕ
x : ℕ
Bx : x ∈ B
Ax : x ∈ A
⊢ x ∈ A ∨ x ∈ B ∧ x ∉ A
Tactic:
left
Proof state after:
case pos.h
A B : Finset ℕ
x : ℕ
Bx : x ∈ B
Ax : x ∈ A
⊢ x ∈ A
Theorem: subset_union_sdiff
Proof state before:
case pos.h
A B : Finset ℕ
x : ℕ
Bx : x ∈ B
Ax : x ∈ A
⊢ x ∈ A
Tactic:
exact Ax
Proof state after:
no goals
Theorem: subset_union_sdiff
Proof state before:
case neg
A B : Finset ℕ
x : ℕ
Bx : x ∈ B
Ax : x ∉ A
⊢ x ∈ A ∨ x ∈ B ∧ x ∉ A
Tactic:
right
Proof state after:
case neg.h
A B : Finset ℕ
x : ℕ
Bx : x ∈ B
Ax : x ∉ A
⊢ x ∈ B ∧ x ∉ A
Theorem: subset_union_sdiff
Proof state before:
case neg.h
A B : Finset ℕ
x : ℕ
Bx : x ∈ B
Ax : x ∉ A
⊢ x ∈ B ∧ x ∉ A
Tactic:
exact ⟨Bx, Ax⟩
Proof state after:
no goals
Theorem: closure_inter_subset_compl
Proof state before:
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s u v : Set X
vo : IsOpen v
d : Disjoint u v
⊢ closure (s ∩ u) ⊆ vᶜ
Tactic:
rw [← vo.isClosed_compl.closure_eq]
Proof state after:
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s u v : Set X
vo : IsOpen v
d : Disjoint u v
⊢ closure (s ∩ u) ⊆ closure vᶜ
Theorem: closure_inter_subset_compl
Proof state before:
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s u v : Set X
vo : IsOpen v
d : Disjoint u v
⊢ closure (s ∩ u) ⊆ closure vᶜ
Tactic:
apply closure_mono
Proof state after:
case h
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s u v : Set X
vo : IsOpen v
d : Disjoint u v
⊢ s ∩ u ⊆ vᶜ
Theorem: closure_inter_subset_compl
Proof state before:
case h
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s u v : Set X
vo : IsOpen v
d : Disjoint u v
⊢ s ∩ u ⊆ vᶜ
Tactic:
exact _root_.trans (inter_subset_right _ _) (Disjoint.subset_compl_left d.symm)
Proof state after:
no goals
Theorem: isClosed_closed_inter
Proof state before:
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s u v : Set X
sc : IsClosed s
vo : IsOpen v
d : Disjoint u v
suv : s ⊆ u ∪ v
⊢ IsClosed (s ∩ u)
Tactic:
rw [←closure_subset_iff_isClosed, ←diff_eq_empty]
Proof state after:
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s u v : Set X
sc : IsClosed s
vo : IsOpen v
d : Disjoint u v
suv : s ⊆ u ∪ v
⊢ closure (s ∩ u) \ (s ∩ u) = ∅
Theorem: isClosed_closed_inter
Proof state before:
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s u v : Set X
sc : IsClosed s
vo : IsOpen v
d : Disjoint u v
suv : s ⊆ u ∪ v
⊢ closure (s ∩ u) \ (s ∩ u) = ∅
Tactic:
by_contra h
Proof state after:
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s u v : Set X
sc : IsClosed s
vo : IsOpen v
d : Disjoint u v
suv : s ⊆ u ∪ v
h : ¬closure (s ∩ u) \ (s ∩ u) = ∅
⊢ False
Theorem: isClosed_closed_inter
Proof state before:
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s u v : Set X
sc : IsClosed s
vo : IsOpen v
d : Disjoint u v
suv : s ⊆ u ∪ v
h : ¬closure (s ∩ u) \ (s ∩ u) = ∅
⊢ False
Tactic:
simp only [← ne_eq, ← nonempty_iff_ne_empty] at h
Proof state after:
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s u v : Set X
sc : IsClosed s
vo : IsOpen v
d : Disjoint u v
suv : s ⊆ u ∪ v
h : (closure (s ∩ u) \ (s ∩ u)).Nonempty
⊢ False
Theorem: isClosed_closed_inter
Proof state before:
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s u v : Set X
sc : IsClosed s
vo : IsOpen v
d : Disjoint u v
suv : s ⊆ u ∪ v
h : (closure (s ∩ u) \ (s ∩ u)).Nonempty
⊢ False
Tactic:
rcases h with ⟨x, h⟩
Proof state after:
case intro
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s u v : Set X
sc : IsClosed s
vo : IsOpen v
d : Disjoint u v
suv : s ⊆ u ∪ v
x : X
h : x ∈ closure (s ∩ u) \ (s ∩ u)
⊢ False
Theorem: isClosed_closed_inter
Proof state before:
case intro
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s u v : Set X
sc : IsClosed s
vo : IsOpen v
d : Disjoint u v
suv : s ⊆ u ∪ v
x : X
h : x ∈ closure (s ∩ u) \ (s ∩ u)
⊢ False
Tactic:
simp only [mem_diff, mem_inter_iff, not_and] at h
Proof state after:
case intro
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s u v : Set X
sc : IsClosed s
vo : IsOpen v
d : Disjoint u v
suv : s ⊆ u ∪ v
x : X
h : x ∈ closure (s ∩ u) ∧ (x ∈ s → x ∉ u)
⊢ False
Theorem: isClosed_closed_inter
Proof state before:
case intro
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s u v : Set X
sc : IsClosed s
vo : IsOpen v
d : Disjoint u v
suv : s ⊆ u ∪ v
x : X
h : x ∈ closure (s ∩ u) ∧ (x ∈ s → x ∉ u)
⊢ False
Tactic:
have sus : closure (s ∩ u) ⊆ s := by
  nth_rw 2 [← sc.closure_eq]; apply closure_mono; apply inter_subset_left
Proof state after:
case intro
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s u v : Set X
sc : IsClosed s
vo : IsOpen v
d : Disjoint u v
suv : s ⊆ u ∪ v
x : X
h : x ∈ closure (s ∩ u) ∧ (x ∈ s → x ∉ u)
sus : closure (s ∩ u) ⊆ s
⊢ False
Theorem: isClosed_closed_inter
Proof state before:
case intro
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s u v : Set X
sc : IsClosed s
vo : IsOpen v
d : Disjoint u v
suv : s ⊆ u ∪ v
x : X
h : x ∈ closure (s ∩ u) ∧ (x ∈ s → x ∉ u)
sus : closure (s ∩ u) ⊆ s
⊢ False
Tactic:
have xs := sus h.1
Proof state after:
case intro
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s u v : Set X
sc : IsClosed s
vo : IsOpen v
d : Disjoint u v
suv : s ⊆ u ∪ v
x : X
h : x ∈ closure (s ∩ u) ∧ (x ∈ s → x ∉ u)
sus : closure (s ∩ u) ⊆ s
xs : x ∈ s
⊢ False
Theorem: isClosed_closed_inter
Proof state before:
case intro
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s u v : Set X
sc : IsClosed s
vo : IsOpen v
d : Disjoint u v
suv : s ⊆ u ∪ v
x : X
h : x ∈ closure (s ∩ u) ∧ (x ∈ s → x ∉ u)
sus : closure (s ∩ u) ⊆ s
xs : x ∈ s
⊢ False
Tactic:
have m := not_or.mpr ⟨h.2 xs, not_mem_of_mem_compl (closure_inter_subset_compl vo d h.1)⟩
Proof state after:
case intro
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s u v : Set X
sc : IsClosed s
vo : IsOpen v
d : Disjoint u v
suv : s ⊆ u ∪ v
x : X
h : x ∈ closure (s ∩ u) ∧ (x ∈ s → x ∉ u)
sus : closure (s ∩ u) ⊆ s
xs : x ∈ s
m : ¬(x ∈ u ∨ x ∈ v)
⊢ False
Theorem: isClosed_closed_inter
Proof state before:
case intro
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s u v : Set X
sc : IsClosed s
vo : IsOpen v
d : Disjoint u v
suv : s ⊆ u ∪ v
x : X
h : x ∈ closure (s ∩ u) ∧ (x ∈ s → x ∉ u)
sus : closure (s ∩ u) ⊆ s
xs : x ∈ s
m : ¬(x ∈ u ∨ x ∈ v)
⊢ False
Tactic:
rw [← mem_union _ _ _] at m
Proof state after:
case intro
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s u v : Set X
sc : IsClosed s
vo : IsOpen v
d : Disjoint u v
suv : s ⊆ u ∪ v
x : X
h : x ∈ closure (s ∩ u) ∧ (x ∈ s → x ∉ u)
sus : closure (s ∩ u) ⊆ s
xs : x ∈ s
m : x ∉ u ∪ v
⊢ False
Theorem: isClosed_closed_inter
Proof state before:
case intro
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s u v : Set X
sc : IsClosed s
vo : IsOpen v
d : Disjoint u v
suv : s ⊆ u ∪ v
x : X
h : x ∈ closure (s ∩ u) ∧ (x ∈ s → x ∉ u)
sus : closure (s ∩ u) ⊆ s
xs : x ∈ s
m : x ∉ u ∪ v
⊢ False
Tactic:
exact not_mem_subset suv m xs
Proof state after:
no goals