internlm/Lean-Github huggingface dataset:
Theorem: Tutorial.HasFinSubCover_of_Icc
Proof state before:
case intro.intro.intro.intro.intro
ι : Type
U : ι → Set ℝ
hU : ∀ (i : ι), IsOpen (U i)
cover : Icc 0 1 ⊆ ⋃ i, U i
H : ¬HasFinSubCover U (Icc 0 1)
c : ℝ := CauSeq.lim (nestedIntervalCauSeq U)
i : ι
hU' : c ∈ U i
ε : ℝ
ε0 : ε > 0
hε : Metric.ball c ε ⊆ U i
n : ℕ
hn : (ε / 2)⁻¹ < 2 ^ n
⊢ Icc (nestedInterval U n).1 (nestedInterval U n).2 ⊆ U i
Tactic:
suffices ∀ x, x ∈ I(n) → |x - c| < ε by
  sorry
Proof state after:
case intro.intro.intro.intro.intro
ι : Type
U : ι → Set ℝ
hU : ∀ (i : ι), IsOpen (U i)
cover : Icc 0 1 ⊆ ⋃ i, U i
H : ¬HasFinSubCover U (Icc 0 1)
c : ℝ := CauSeq.lim (nestedIntervalCauSeq U)
i : ι
hU' : c ∈ U i
ε : ℝ
ε0 : ε > 0
hε : Metric.ball c ε ⊆ U i
n : ℕ
hn : (ε / 2)⁻¹ < 2 ^ n
⊢ ∀ x ∈ Icc (nestedInterval U n).1 (nestedInterval U n).2, |x - c| < ε
Theorem: Tutorial.HasFinSubCover_of_Icc
Proof state before:
case intro.intro.intro.intro.intro
ι : Type
U : ι → Set ℝ
hU : ∀ (i : ι), IsOpen (U i)
cover : Icc 0 1 ⊆ ⋃ i, U i
H : ¬HasFinSubCover U (Icc 0 1)
c : ℝ := CauSeq.lim (nestedIntervalCauSeq U)
i : ι
hU' : c ∈ U i
ε : ℝ
ε0 : ε > 0
hε : Metric.ball c ε ⊆ U i
n : ℕ
hn : (ε / 2)⁻¹ < 2 ^ n
⊢ ∀ x ∈ Icc (nestedInterval U n).1 (nestedInterval U n).2, |x - c| < ε
Tactic:
sorry
Proof state after:
no goals
Theorem: Tutorial.HasFinSubCover_of_Icc
Proof state before:
ι : Type
U : ι → Set ℝ
hU : ∀ (i : ι), IsOpen (U i)
cover : Icc 0 1 ⊆ ⋃ i, U i
H : ¬HasFinSubCover U (Icc 0 1)
c : ℝ := CauSeq.lim (nestedIntervalCauSeq U)
i : ι
hU' : c ∈ U i
ε : ℝ
ε0 : ε > 0
hε : Metric.ball c ε ⊆ U i
⊢ ∃ n, (ε / 2)⁻¹ < 2 ^ n
Tactic:
sorry
Proof state after:
no goals
Theorem: Tutorial.HasFinSubCover_of_Icc
Proof state before:
ι : Type
U : ι → Set ℝ
hU : ∀ (i : ι), IsOpen (U i)
cover : Icc 0 1 ⊆ ⋃ i, U i
H : ¬HasFinSubCover U (Icc 0 1)
c : ℝ := CauSeq.lim (nestedIntervalCauSeq U)
i : ι
hU' : c ∈ U i
ε : ℝ
ε0 : ε > 0
hε : Metric.ball c ε ⊆ U i
n : ℕ
hn : (ε / 2)⁻¹ < 2 ^ n
this : HasFinSubCover U (Icc (nestedInterval U n).1 (nestedInterval U n).2)
⊢ False
Tactic:
sorry
Proof state after:
no goals
Theorem: Tutorial.HasFinSubCover_of_Icc
Proof state before:
ι : Type
U : ι → Set ℝ
hU : ∀ (i : ι), IsOpen (U i)
cover : Icc 0 1 ⊆ ⋃ i, U i
H : ¬HasFinSubCover U (Icc 0 1)
c : ℝ := CauSeq.lim (nestedIntervalCauSeq U)
i : ι
hU' : c ∈ U i
ε : ℝ
ε0 : ε > 0
hε : Metric.ball c ε ⊆ U i
n : ℕ
hn : (ε / 2)⁻¹ < 2 ^ n
this : Icc (nestedInterval U n).1 (nestedInterval U n).2 ⊆ U i
⊢ HasFinSubCover U (Icc (nestedInterval U n).1 (nestedInterval U n).2)
Tactic:
sorry
Proof state after:
no goals
Theorem: Tutorial.HasFinSubCover_of_Icc
Proof state before:
ι : Type
U : ι → Set ℝ
hU : ∀ (i : ι), IsOpen (U i)
cover : Icc 0 1 ⊆ ⋃ i, U i
H : ¬HasFinSubCover U (Icc 0 1)
c : ℝ := CauSeq.lim (nestedIntervalCauSeq U)
i : ι
hU' : c ∈ U i
ε : ℝ
ε0 : ε > 0
hε : Metric.ball c ε ⊆ U i
n : ℕ
hn : (ε / 2)⁻¹ < 2 ^ n
this : ∀ x ∈ Icc (nestedInterval U n).1 (nestedInterval U n).2, |x - c| < ε
⊢ Icc (nestedInterval U n).1 (nestedInterval U n).2 ⊆ U i
Tactic:
sorry
Proof state after:
no goals
Theorem: Tutorial.Injective.comp
Proof state before:
X Y Z : Type
f : X → Y
g : Y → Z
hfinj : Injective f
hginj : Injective g
⊢ Injective (g ∘ f)
Tactic:
rw [Injective]
Proof state after:
X Y Z : Type
f : X → Y
g : Y → Z
hfinj : Injective f
hginj : Injective g
⊢ ∀ {x₁ x₂ : X}, (g ∘ f) x₁ = (g ∘ f) x₂ → x₁ = x₂
Theorem: Tutorial.Injective.comp
Proof state before:
X Y Z : Type
f : X → Y
g : Y → Z
hfinj : Injective f
hginj : Injective g
⊢ ∀ {x₁ x₂ : X}, (g ∘ f) x₁ = (g ∘ f) x₂ → x₁ = x₂
Tactic:
intro x₁ x₂ hgf
Proof state after:
X Y Z : Type
f : X → Y
g : Y → Z
hfinj : Injective f
hginj : Injective g
x₁ x₂ : X
hgf : (g ∘ f) x₁ = (g ∘ f) x₂
⊢ x₁ = x₂
Theorem: Tutorial.Injective.comp
Proof state before:
X Y Z : Type
f : X → Y
g : Y → Z
hfinj : Injective f
hginj : Injective g
x₁ x₂ : X
hgf : (g ∘ f) x₁ = (g ∘ f) x₂
⊢ x₁ = x₂
Tactic:
have hf := hginj hgf
Proof state after:
X Y Z : Type
f : X → Y
g : Y → Z
hfinj : Injective f
hginj : Injective g
x₁ x₂ : X
hgf : (g ∘ f) x₁ = (g ∘ f) x₂
hf : f x₁ = f x₂
⊢ x₁ = x₂
Theorem: Tutorial.Injective.comp
Proof state before:
X Y Z : Type
f : X → Y
g : Y → Z
hfinj : Injective f
hginj : Injective g
x₁ x₂ : X
hgf : (g ∘ f) x₁ = (g ∘ f) x₂
hf : f x₁ = f x₂
⊢ x₁ = x₂
Tactic:
sorry
Proof state after:
no goals
Theorem: Tutorial.Injective.of_comp
Proof state before:
X Y Z : Type
f : X → Y
g : Y → Z
hgfinj : Injective (g ∘ f)
⊢ Injective f
Tactic:
rw [Injective]
Proof state after:
X Y Z : Type
f : X → Y
g : Y → Z
hgfinj : Injective (g ∘ f)
⊢ ∀ {x₁ x₂ : X}, f x₁ = f x₂ → x₁ = x₂
Theorem: Tutorial.Injective.of_comp
Proof state before:
X Y Z : Type
f : X → Y
g : Y → Z
hgfinj : Injective (g ∘ f)
⊢ ∀ {x₁ x₂ : X}, f x₁ = f x₂ → x₁ = x₂
Tactic:
intro x₁ x₂ hf
Proof state after:
X Y Z : Type
f : X → Y
g : Y → Z
hgfinj : Injective (g ∘ f)
x₁ x₂ : X
hf : f x₁ = f x₂
⊢ x₁ = x₂
Theorem: Tutorial.Injective.of_comp
Proof state before:
X Y Z : Type
f : X → Y
g : Y → Z
hgfinj : Injective (g ∘ f)
x₁ x₂ : X
hf : f x₁ = f x₂
⊢ x₁ = x₂
Tactic:
have h : g (f x₁) = g (f x₂) := by
  sorry
Proof state after:
X Y Z : Type
f : X → Y
g : Y → Z
hgfinj : Injective (g ∘ f)
x₁ x₂ : X
hf : f x₁ = f x₂
h : g (f x₁) = g (f x₂)
⊢ x₁ = x₂
Theorem: Tutorial.Injective.of_comp
Proof state before:
X Y Z : Type
f : X → Y
g : Y → Z
hgfinj : Injective (g ∘ f)
x₁ x₂ : X
hf : f x₁ = f x₂
h : g (f x₁) = g (f x₂)
⊢ x₁ = x₂
Tactic:
sorry
Proof state after:
no goals
Theorem: Tutorial.Injective.of_comp
Proof state before:
X Y Z : Type
f : X → Y
g : Y → Z
hgfinj : Injective (g ∘ f)
x₁ x₂ : X
hf : f x₁ = f x₂
⊢ g (f x₁) = g (f x₂)
Tactic:
sorry
Proof state after:
no goals
Theorem: Tutorial.Surjective.comp
Proof state before:
X Y Z : Type
f : X → Y
g : Y → Z
hfsurj : Surjective f
hgsurj : Surjective g
⊢ Surjective (g ∘ f)
Tactic:
rw [Surjective]
Proof state after:
X Y Z : Type
f : X → Y
g : Y → Z
hfsurj : Surjective f
hgsurj : Surjective g
⊢ ∀ (y : Z), ∃ x, (g ∘ f) x = y
Theorem: Tutorial.Surjective.comp
Proof state before:
X Y Z : Type
f : X → Y
g : Y → Z
hfsurj : Surjective f
hgsurj : Surjective g
⊢ ∀ (y : Z), ∃ x, (g ∘ f) x = y
Tactic:
intro z
Proof state after:
X Y Z : Type
f : X → Y
g : Y → Z
hfsurj : Surjective f
hgsurj : Surjective g
z : Z
⊢ ∃ x, (g ∘ f) x = z
Theorem: Tutorial.Surjective.comp
Proof state before:
X Y Z : Type
f : X → Y
g : Y → Z
hfsurj : Surjective f
hgsurj : Surjective g
z : Z
⊢ ∃ x, (g ∘ f) x = z
Tactic:
have ⟨y, hy⟩ := hgsurj z
Proof state after:
X Y Z : Type
f : X → Y
g : Y → Z
hfsurj : Surjective f
hgsurj : Surjective g
z : Z
y : Y
hy : g y = z
⊢ ∃ x, (g ∘ f) x = z
Theorem: Tutorial.Surjective.comp
Proof state before:
X Y Z : Type
f : X → Y
g : Y → Z
hfsurj : Surjective f
hgsurj : Surjective g
z : Z
y : Y
hy : g y = z
⊢ ∃ x, (g ∘ f) x = z
Tactic:
sorry
Proof state after:
no goals
Theorem: Tutorial.Surjective.of_comp
Proof state before:
X Y Z : Type
f : X → Y
g : Y → Z
h : Surjective (g ∘ f)
⊢ Surjective g
Tactic:
sorry
Proof state after:
no goals
Theorem: Tutorial.Subgroup.mem_comm
Proof state before:
G : Type
inst✝¹ : Group G
N : Subgroup G
inst✝ : Normal N
a b : G
hab : a * b ∈ N
⊢ b * a ∈ N
Tactic:
sorry
Proof state after:
no goals
Theorem: Tutorial.mem_of_eq_one
Proof state before:
G : Type
inst✝¹ : Group G
N : Subgroup G
inst✝ : Subgroup.Normal N
a : G
⊢ LeftQuotient.mk a = 1 ↔ a ∈ N
Tactic:
sorry
Proof state after:
no goals
Theorem: Tutorial.GroupHom.rangeKerLift_injective
Proof state before:
G H : Type
inst✝¹ : Group G
inst✝ : Group H
f : G →* H
⊢ Function.Injective ⇑(rangeKerLift f)
Tactic:
sorry
Proof state after:
no goals
Theorem: Tutorial.GroupHom.rangeKerLift_surjective
Proof state before:
G H : Type
inst✝¹ : Group G
inst✝ : Group H
f : G →* H
y : H
hy : y ∈ range f
⊢ ∃ a, (rangeKerLift f) a = { val := y, property := hy }
Tactic:
sorry
Proof state after:
no goals
Theorem: Tutorial.«0.9999999 = 1»
Proof state before:
case e_cauchy.a
ε : ℚ
ε0 : ε > 0
⊢ ∃ i, ∀ j ≥ i, (10 ^ j)⁻¹ < ε
Tactic:
have ⟨n, hn⟩ : ∃ n : ℕ, ε⁻¹ < 10 ^ n := pow_unbounded_of_one_lt ε⁻¹ rfl
Proof state after:
case e_cauchy.a
ε : ℚ
ε0 : ε > 0
n : ℕ
hn : ε⁻¹ < 10 ^ n
⊢ ∃ i, ∀ j ≥ i, (10 ^ j)⁻¹ < ε
Theorem: Tutorial.«0.9999999 = 1»
Proof state before:
case e_cauchy.a
ε : ℚ
ε0 : ε > 0
n : ℕ
hn : ε⁻¹ < 10 ^ n
⊢ ∃ i, ∀ j ≥ i, (10 ^ j)⁻¹ < ε
Tactic:
have : (10 ^ n : ℚ)⁻¹ < ε := inv_lt_of_inv_lt ε0 hn
Proof state after:
case e_cauchy.a
ε : ℚ
ε0 : ε > 0
n : ℕ
hn : ε⁻¹ < 10 ^ n
this : (10 ^ n)⁻¹ < ε
⊢ ∃ i, ∀ j ≥ i, (10 ^ j)⁻¹ < ε
Theorem: Tutorial.«0.9999999 = 1»
Proof state before:
case e_cauchy.a
ε : ℚ
ε0 : ε > 0
n : ℕ
hn : ε⁻¹ < 10 ^ n
this : (10 ^ n)⁻¹ < ε
⊢ ∃ i, ∀ j ≥ i, (10 ^ j)⁻¹ < ε
Tactic:
exists n
Proof state after:
case e_cauchy.a
ε : ℚ
ε0 : ε > 0
n : ℕ
hn : ε⁻¹ < 10 ^ n
this : (10 ^ n)⁻¹ < ε
⊢ ∀ j ≥ n, (10 ^ j)⁻¹ < ε
Theorem: Tutorial.«0.9999999 = 1»
Proof state before:
case e_cauchy.a
ε : ℚ
ε0 : ε > 0
n : ℕ
hn : ε⁻¹ < 10 ^ n
this : (10 ^ n)⁻¹ < ε
⊢ ∀ j ≥ n, (10 ^ j)⁻¹ < ε
Tactic:
intro h hj
Proof state after:
case e_cauchy.a
ε : ℚ
ε0 : ε > 0
n : ℕ
hn : ε⁻¹ < 10 ^ n
this : (10 ^ n)⁻¹ < ε
h : ℕ
hj : h ≥ n
⊢ (10 ^ h)⁻¹ < ε
Theorem: Tutorial.«0.9999999 = 1»
Proof state before:
case e_cauchy.a
ε : ℚ
ε0 : ε > 0
n : ℕ
hn : ε⁻¹ < 10 ^ n
this : (10 ^ n)⁻¹ < ε
h : ℕ
hj : h ≥ n
⊢ (10 ^ h)⁻¹ < ε
Tactic:
calc (10 ^ h : ℚ )⁻¹ ≤ (10 ^ n : ℚ)⁻¹ := inv_pow_le_inv_pow_of_le (by linarith) hj
  _ < ε := this
Proof state after:
no goals
Theorem: Tutorial.«0.9999999 = 1»
Proof state before:
ε : ℚ
ε0 : ε > 0
n : ℕ
hn : ε⁻¹ < 10 ^ n
this : (10 ^ n)⁻¹ < ε
h : ℕ
hj : h ≥ n
⊢ 1 ≤ 10
Tactic:
linarith
Proof state after:
no goals
Theorem: Tutorial.HasFinSubCover_of_Icc
Proof state before:
case intro.intro.intro.intro.intro
ι : Type
U : ι → Set ℝ
hU : ∀ (i : ι), IsOpen (U i)
cover : Icc 0 1 ⊆ ⋃ i, U i
H : ¬HasFinSubCover U (Icc 0 1)
c : ℝ := CauSeq.lim (nestedIntervalCauSeq U)
i : ι
hU' : c ∈ U i
ε : ℝ
ε0 : ε > 0
hε : Metric.ball c ε ⊆ U i
⊢ False
Tactic:
have ⟨n, hn⟩ : ∃ n : ℕ, (ε / 2)⁻¹ < 2 ^ n := by
  apply pow_unbounded_of_one_lt (ε / 2)⁻¹ (by linarith)
Proof state after:
case intro.intro.intro.intro.intro
ι : Type
U : ι → Set ℝ
hU : ∀ (i : ι), IsOpen (U i)
cover : Icc 0 1 ⊆ ⋃ i, U i
H : ¬HasFinSubCover U (Icc 0 1)
c : ℝ := CauSeq.lim (nestedIntervalCauSeq U)
i : ι
hU' : c ∈ U i
ε : ℝ
ε0 : ε > 0
hε : Metric.ball c ε ⊆ U i
n : ℕ
hn : (ε / 2)⁻¹ < 2 ^ n
⊢ False
Theorem: Tutorial.HasFinSubCover_of_Icc
Proof state before:
case intro.intro.intro.intro.intro
ι : Type
U : ι → Set ℝ
hU : ∀ (i : ι), IsOpen (U i)
cover : Icc 0 1 ⊆ ⋃ i, U i
H : ¬HasFinSubCover U (Icc 0 1)
c : ℝ := CauSeq.lim (nestedIntervalCauSeq U)
i : ι
hU' : c ∈ U i
ε : ℝ
ε0 : ε > 0
hε : Metric.ball c ε ⊆ U i
n : ℕ
hn : (ε / 2)⁻¹ < 2 ^ n
⊢ False
Tactic:
suffices HasFinSubCover U I(n) by
  apply nestedInterval_not_HasFinSubCover H n this
Proof state after:
case intro.intro.intro.intro.intro
ι : Type
U : ι → Set ℝ
hU : ∀ (i : ι), IsOpen (U i)
cover : Icc 0 1 ⊆ ⋃ i, U i
H : ¬HasFinSubCover U (Icc 0 1)
c : ℝ := CauSeq.lim (nestedIntervalCauSeq U)
i : ι
hU' : c ∈ U i
ε : ℝ
ε0 : ε > 0
hε : Metric.ball c ε ⊆ U i
n : ℕ
hn : (ε / 2)⁻¹ < 2 ^ n
⊢ HasFinSubCover U (Icc (nestedInterval U n).1 (nestedInterval U n).2)
Theorem: Tutorial.HasFinSubCover_of_Icc
Proof state before:
case intro.intro.intro.intro.intro
ι : Type
U : ι → Set ℝ
hU : ∀ (i : ι), IsOpen (U i)
cover : Icc 0 1 ⊆ ⋃ i, U i
H : ¬HasFinSubCover U (Icc 0 1)
c : ℝ := CauSeq.lim (nestedIntervalCauSeq U)
i : ι
hU' : c ∈ U i
ε : ℝ
ε0 : ε > 0
hε : Metric.ball c ε ⊆ U i
n : ℕ
hn : (ε / 2)⁻¹ < 2 ^ n
⊢ HasFinSubCover U (Icc (nestedInterval U n).1 (nestedInterval U n).2)
Tactic:
suffices I(n) ⊆ U i by
  exists {i}
  simpa using this
Proof state after:
case intro.intro.intro.intro.intro
ι : Type
U : ι → Set ℝ
hU : ∀ (i : ι), IsOpen (U i)
cover : Icc 0 1 ⊆ ⋃ i, U i
H : ¬HasFinSubCover U (Icc 0 1)
c : ℝ := CauSeq.lim (nestedIntervalCauSeq U)
i : ι
hU' : c ∈ U i
ε : ℝ
ε0 : ε > 0
hε : Metric.ball c ε ⊆ U i
n : ℕ
hn : (ε / 2)⁻¹ < 2 ^ n
⊢ Icc (nestedInterval U n).1 (nestedInterval U n).2 ⊆ U i
Theorem: Tutorial.HasFinSubCover_of_Icc
Proof state before:
case intro.intro.intro.intro.intro
ι : Type
U : ι → Set ℝ
hU : ∀ (i : ι), IsOpen (U i)
cover : Icc 0 1 ⊆ ⋃ i, U i
H : ¬HasFinSubCover U (Icc 0 1)
c : ℝ := CauSeq.lim (nestedIntervalCauSeq U)
i : ι
hU' : c ∈ U i
ε : ℝ
ε0 : ε > 0
hε : Metric.ball c ε ⊆ U i
n : ℕ
hn : (ε / 2)⁻¹ < 2 ^ n
⊢ Icc (nestedInterval U n).1 (nestedInterval U n).2 ⊆ U i
Tactic:
suffices ∀ x, x ∈ I(n) → |x - c| < ε by
  intro x hx
  apply hε (this x hx)
Proof state after:
case intro.intro.intro.intro.intro
ι : Type
U : ι → Set ℝ
hU : ∀ (i : ι), IsOpen (U i)
cover : Icc 0 1 ⊆ ⋃ i, U i
H : ¬HasFinSubCover U (Icc 0 1)
c : ℝ := CauSeq.lim (nestedIntervalCauSeq U)
i : ι
hU' : c ∈ U i
ε : ℝ
ε0 : ε > 0
hε : Metric.ball c ε ⊆ U i
n : ℕ
hn : (ε / 2)⁻¹ < 2 ^ n
⊢ ∀ x ∈ Icc (nestedInterval U n).1 (nestedInterval U n).2, |x - c| < ε
Theorem: Tutorial.HasFinSubCover_of_Icc
Proof state before:
case intro.intro.intro.intro.intro
ι : Type
U : ι → Set ℝ
hU : ∀ (i : ι), IsOpen (U i)
cover : Icc 0 1 ⊆ ⋃ i, U i
H : ¬HasFinSubCover U (Icc 0 1)
c : ℝ := CauSeq.lim (nestedIntervalCauSeq U)
i : ι
hU' : c ∈ U i
ε : ℝ
ε0 : ε > 0
hε : Metric.ball c ε ⊆ U i
n : ℕ
hn : (ε / 2)⁻¹ < 2 ^ n
⊢ ∀ x ∈ Icc (nestedInterval U n).1 (nestedInterval U n).2, |x - c| < ε
Tactic:
intro x hx
Proof state after:
case intro.intro.intro.intro.intro
ι : Type
U : ι → Set ℝ
hU : ∀ (i : ι), IsOpen (U i)
cover : Icc 0 1 ⊆ ⋃ i, U i
H : ¬HasFinSubCover U (Icc 0 1)
c : ℝ := CauSeq.lim (nestedIntervalCauSeq U)
i : ι
hU' : c ∈ U i
ε : ℝ
ε0 : ε > 0
hε : Metric.ball c ε ⊆ U i
n : ℕ
hn : (ε / 2)⁻¹ < 2 ^ n
x : ℝ
hx : x ∈ Icc (nestedInterval U n).1 (nestedInterval U n).2
⊢ |x - c| < ε
Theorem: Tutorial.HasFinSubCover_of_Icc
Proof state before:
case intro.intro.intro.intro.intro
ι : Type
U : ι → Set ℝ
hU : ∀ (i : ι), IsOpen (U i)
cover : Icc 0 1 ⊆ ⋃ i, U i
H : ¬HasFinSubCover U (Icc 0 1)
c : ℝ := CauSeq.lim (nestedIntervalCauSeq U)
i : ι
hU' : c ∈ U i
ε : ℝ
ε0 : ε > 0
hε : Metric.ball c ε ⊆ U i
n : ℕ
hn : (ε / 2)⁻¹ < 2 ^ n
x : ℝ
hx : x ∈ Icc (nestedInterval U n).1 (nestedInterval U n).2
⊢ |x - c| < ε
Tactic:
have hba : β n - α n = (2 ^ n : ℝ)⁻¹ := nestedInterval_len U n
Proof state after:
case intro.intro.intro.intro.intro
ι : Type
U : ι → Set ℝ
hU : ∀ (i : ι), IsOpen (U i)
cover : Icc 0 1 ⊆ ⋃ i, U i
H : ¬HasFinSubCover U (Icc 0 1)
c : ℝ := CauSeq.lim (nestedIntervalCauSeq U)
i : ι
hU' : c ∈ U i
ε : ℝ
ε0 : ε > 0
hε : Metric.ball c ε ⊆ U i
n : ℕ
hn : (ε / 2)⁻¹ < 2 ^ n
x : ℝ
hx : x ∈ Icc (nestedInterval U n).1 (nestedInterval U n).2
hba : (nestedInterval U n).2 - (nestedInterval U n).1 = (2 ^ n)⁻¹
⊢ |x - c| < ε
Theorem: Tutorial.HasFinSubCover_of_Icc
Proof state before:
case intro.intro.intro.intro.intro
ι : Type
U : ι → Set ℝ
hU : ∀ (i : ι), IsOpen (U i)
cover : Icc 0 1 ⊆ ⋃ i, U i
H : ¬HasFinSubCover U (Icc 0 1)
c : ℝ := CauSeq.lim (nestedIntervalCauSeq U)
i : ι
hU' : c ∈ U i
ε : ℝ
ε0 : ε > 0
hε : Metric.ball c ε ⊆ U i
n : ℕ
hn : (ε / 2)⁻¹ < 2 ^ n
x : ℝ
hx : x ∈ Icc (nestedInterval U n).1 (nestedInterval U n).2
hba : (nestedInterval U n).2 - (nestedInterval U n).1 = (2 ^ n)⁻¹
⊢ |x - c| < ε
Tactic:
have hn := inv_lt_of_inv_lt (by linarith) hn
Proof state after:
case intro.intro.intro.intro.intro
ι : Type
U : ι → Set ℝ
hU : ∀ (i : ι), IsOpen (U i)
cover : Icc 0 1 ⊆ ⋃ i, U i
H : ¬HasFinSubCover U (Icc 0 1)
c : ℝ := CauSeq.lim (nestedIntervalCauSeq U)
i : ι
hU' : c ∈ U i
ε : ℝ
ε0 : ε > 0
hε : Metric.ball c ε ⊆ U i
n : ℕ
hn✝ : (ε / 2)⁻¹ < 2 ^ n
x : ℝ
hx : x ∈ Icc (nestedInterval U n).1 (nestedInterval U n).2
hba : (nestedInterval U n).2 - (nestedInterval U n).1 = (2 ^ n)⁻¹
hn : (2 ^ n)⁻¹ < ε / 2
⊢ |x - c| < ε
Theorem: Tutorial.HasFinSubCover_of_Icc
Proof state before:
case intro.intro.intro.intro.intro
ι : Type
U : ι → Set ℝ
hU : ∀ (i : ι), IsOpen (U i)
cover : Icc 0 1 ⊆ ⋃ i, U i
H : ¬HasFinSubCover U (Icc 0 1)
c : ℝ := CauSeq.lim (nestedIntervalCauSeq U)
i : ι
hU' : c ∈ U i
ε : ℝ
ε0 : ε > 0
hε : Metric.ball c ε ⊆ U i
n : ℕ
hn✝ : (ε / 2)⁻¹ < 2 ^ n
x : ℝ
hx : x ∈ Icc (nestedInterval U n).1 (nestedInterval U n).2
hba : (nestedInterval U n).2 - (nestedInterval U n).1 = (2 ^ n)⁻¹
hn : (2 ^ n)⁻¹ < ε / 2
⊢ |x - c| < ε
Tactic:
have hc : α n ≤ c ∧ c ≤ β n := nestedIntervalLim_mem U n
Proof state after:
case intro.intro.intro.intro.intro
ι : Type
U : ι → Set ℝ
hU : ∀ (i : ι), IsOpen (U i)
cover : Icc 0 1 ⊆ ⋃ i, U i
H : ¬HasFinSubCover U (Icc 0 1)
c : ℝ := CauSeq.lim (nestedIntervalCauSeq U)
i : ι
hU' : c ∈ U i
ε : ℝ
ε0 : ε > 0
hε : Metric.ball c ε ⊆ U i
n : ℕ
hn✝ : (ε / 2)⁻¹ < 2 ^ n
x : ℝ
hx : x ∈ Icc (nestedInterval U n).1 (nestedInterval U n).2
hba : (nestedInterval U n).2 - (nestedInterval U n).1 = (2 ^ n)⁻¹
hn : (2 ^ n)⁻¹ < ε / 2
hc : (nestedInterval U n).1 ≤ c ∧ c ≤ (nestedInterval U n).2
⊢ |x - c| < ε
Theorem: Tutorial.HasFinSubCover_of_Icc
Proof state before:
case intro.intro.intro.intro.intro
ι : Type
U : ι → Set ℝ
hU : ∀ (i : ι), IsOpen (U i)
cover : Icc 0 1 ⊆ ⋃ i, U i
H : ¬HasFinSubCover U (Icc 0 1)
c : ℝ := CauSeq.lim (nestedIntervalCauSeq U)
i : ι
hU' : c ∈ U i
ε : ℝ
ε0 : ε > 0
hε : Metric.ball c ε ⊆ U i
n : ℕ
hn✝ : (ε / 2)⁻¹ < 2 ^ n
x : ℝ
hx : x ∈ Icc (nestedInterval U n).1 (nestedInterval U n).2
hba : (nestedInterval U n).2 - (nestedInterval U n).1 = (2 ^ n)⁻¹
hn : (2 ^ n)⁻¹ < ε / 2
hc : (nestedInterval U n).1 ≤ c ∧ c ≤ (nestedInterval U n).2
⊢ |x - c| < ε
Tactic:
have hx : α n ≤ x ∧ x ≤ β n := hx
Proof state after:
case intro.intro.intro.intro.intro
ι : Type
U : ι → Set ℝ
hU : ∀ (i : ι), IsOpen (U i)
cover : Icc 0 1 ⊆ ⋃ i, U i
H : ¬HasFinSubCover U (Icc 0 1)
c : ℝ := CauSeq.lim (nestedIntervalCauSeq U)
i : ι
hU' : c ∈ U i
ε : ℝ
ε0 : ε > 0
hε : Metric.ball c ε ⊆ U i
n : ℕ
hn✝ : (ε / 2)⁻¹ < 2 ^ n
x : ℝ
hx✝ : x ∈ Icc (nestedInterval U n).1 (nestedInterval U n).2
hba : (nestedInterval U n).2 - (nestedInterval U n).1 = (2 ^ n)⁻¹
hn : (2 ^ n)⁻¹ < ε / 2
hc : (nestedInterval U n).1 ≤ c ∧ c ≤ (nestedInterval U n).2
hx : (nestedInterval U n).1 ≤ x ∧ x ≤ (nestedInterval U n).2
⊢ |x - c| < ε
Theorem: Tutorial.HasFinSubCover_of_Icc
Proof state before:
case intro.intro.intro.intro.intro
ι : Type
U : ι → Set ℝ
hU : ∀ (i : ι), IsOpen (U i)
cover : Icc 0 1 ⊆ ⋃ i, U i
H : ¬HasFinSubCover U (Icc 0 1)
c : ℝ := CauSeq.lim (nestedIntervalCauSeq U)
i : ι
hU' : c ∈ U i
ε : ℝ
ε0 : ε > 0
hε : Metric.ball c ε ⊆ U i
n : ℕ
hn✝ : (ε / 2)⁻¹ < 2 ^ n
x : ℝ
hx✝ : x ∈ Icc (nestedInterval U n).1 (nestedInterval U n).2
hba : (nestedInterval U n).2 - (nestedInterval U n).1 = (2 ^ n)⁻¹
hn : (2 ^ n)⁻¹ < ε / 2
hc : (nestedInterval U n).1 ≤ c ∧ c ≤ (nestedInterval U n).2
hx : (nestedInterval U n).1 ≤ x ∧ x ≤ (nestedInterval U n).2
⊢ |x - c| < ε
Tactic:
calc |x - c|
  _ = |(x - α n) - (c - α n)| := by simp
  _ ≤ |x - α n| + |c - α n| := by apply abs_sub
  _ = (x - α n) + (c - α n) := by
    apply congrArg₂ <;> rw [abs_eq_self] <;> linarith
  _ < ε / 2 + ε / 2 := by linarith
  _ = ε := by ring
Proof state after:
no goals
Theorem: Tutorial.HasFinSubCover_of_Icc
Proof state before:
ι : Type
U : ι → Set ℝ
hU : ∀ (i : ι), IsOpen (U i)
cover : Icc 0 1 ⊆ ⋃ i, U i
H : ¬HasFinSubCover U (Icc 0 1)
c : ℝ := CauSeq.lim (nestedIntervalCauSeq U)
i : ι
hU' : c ∈ U i
ε : ℝ
ε0 : ε > 0
hε : Metric.ball c ε ⊆ U i
⊢ ∃ n, (ε / 2)⁻¹ < 2 ^ n
Tactic:
apply pow_unbounded_of_one_lt (ε / 2)⁻¹ (by linarith)
Proof state after:
no goals
Theorem: Tutorial.HasFinSubCover_of_Icc
Proof state before:
ι : Type
U : ι → Set ℝ
hU : ∀ (i : ι), IsOpen (U i)
cover : Icc 0 1 ⊆ ⋃ i, U i
H : ¬HasFinSubCover U (Icc 0 1)
c : ℝ := CauSeq.lim (nestedIntervalCauSeq U)
i : ι
hU' : c ∈ U i
ε : ℝ
ε0 : ε > 0
hε : Metric.ball c ε ⊆ U i
⊢ 1 < 2
Tactic:
linarith
Proof state after:
no goals
Theorem: Tutorial.HasFinSubCover_of_Icc
Proof state before:
ι : Type
U : ι → Set ℝ
hU : ∀ (i : ι), IsOpen (U i)
cover : Icc 0 1 ⊆ ⋃ i, U i
H : ¬HasFinSubCover U (Icc 0 1)
c : ℝ := CauSeq.lim (nestedIntervalCauSeq U)
i : ι
hU' : c ∈ U i
ε : ℝ
ε0 : ε > 0
hε : Metric.ball c ε ⊆ U i
n : ℕ
hn : (ε / 2)⁻¹ < 2 ^ n
this : HasFinSubCover U (Icc (nestedInterval U n).1 (nestedInterval U n).2)
⊢ False
Tactic:
apply nestedInterval_not_HasFinSubCover H n this
Proof state after:
no goals
Theorem: Tutorial.HasFinSubCover_of_Icc
Proof state before:
ι : Type
U : ι → Set ℝ
hU : ∀ (i : ι), IsOpen (U i)
cover : Icc 0 1 ⊆ ⋃ i, U i
H : ¬HasFinSubCover U (Icc 0 1)
c : ℝ := CauSeq.lim (nestedIntervalCauSeq U)
i : ι
hU' : c ∈ U i
ε : ℝ
ε0 : ε > 0
hε : Metric.ball c ε ⊆ U i
n : ℕ
hn : (ε / 2)⁻¹ < 2 ^ n
this : Icc (nestedInterval U n).1 (nestedInterval U n).2 ⊆ U i
⊢ HasFinSubCover U (Icc (nestedInterval U n).1 (nestedInterval U n).2)
Tactic:
exists {i}
Proof state after:
ι : Type
U : ι → Set ℝ
hU : ∀ (i : ι), IsOpen (U i)
cover : Icc 0 1 ⊆ ⋃ i, U i
H : ¬HasFinSubCover U (Icc 0 1)
c : ℝ := CauSeq.lim (nestedIntervalCauSeq U)
i : ι
hU' : c ∈ U i
ε : ℝ
ε0 : ε > 0
hε : Metric.ball c ε ⊆ U i
n : ℕ
hn : (ε / 2)⁻¹ < 2 ^ n
this : Icc (nestedInterval U n).1 (nestedInterval U n).2 ⊆ U i
⊢ Icc (nestedInterval U n).1 (nestedInterval U n).2 ⊆ ⋃ i_1 ∈ {i}, U i_1
Theorem: Tutorial.HasFinSubCover_of_Icc
Proof state before:
ι : Type
U : ι → Set ℝ
hU : ∀ (i : ι), IsOpen (U i)
cover : Icc 0 1 ⊆ ⋃ i, U i
H : ¬HasFinSubCover U (Icc 0 1)
c : ℝ := CauSeq.lim (nestedIntervalCauSeq U)
i : ι
hU' : c ∈ U i
ε : ℝ
ε0 : ε > 0
hε : Metric.ball c ε ⊆ U i
n : ℕ
hn : (ε / 2)⁻¹ < 2 ^ n
this : Icc (nestedInterval U n).1 (nestedInterval U n).2 ⊆ U i
⊢ Icc (nestedInterval U n).1 (nestedInterval U n).2 ⊆ ⋃ i_1 ∈ {i}, U i_1
Tactic:
simpa using this
Proof state after:
no goals
Theorem: Tutorial.HasFinSubCover_of_Icc
Proof state before:
ι : Type
U : ι → Set ℝ
hU : ∀ (i : ι), IsOpen (U i)
cover : Icc 0 1 ⊆ ⋃ i, U i
H : ¬HasFinSubCover U (Icc 0 1)
c : ℝ := CauSeq.lim (nestedIntervalCauSeq U)
i : ι
hU' : c ∈ U i
ε : ℝ
ε0 : ε > 0
hε : Metric.ball c ε ⊆ U i
n : ℕ
hn : (ε / 2)⁻¹ < 2 ^ n
this : ∀ x ∈ Icc (nestedInterval U n).1 (nestedInterval U n).2, |x - c| < ε
⊢ Icc (nestedInterval U n).1 (nestedInterval U n).2 ⊆ U i
Tactic:
intro x hx
Proof state after:
ι : Type
U : ι → Set ℝ
hU : ∀ (i : ι), IsOpen (U i)
cover : Icc 0 1 ⊆ ⋃ i, U i
H : ¬HasFinSubCover U (Icc 0 1)
c : ℝ := CauSeq.lim (nestedIntervalCauSeq U)
i : ι
hU' : c ∈ U i
ε : ℝ
ε0 : ε > 0
hε : Metric.ball c ε ⊆ U i
n : ℕ
hn : (ε / 2)⁻¹ < 2 ^ n
this : ∀ x ∈ Icc (nestedInterval U n).1 (nestedInterval U n).2, |x - c| < ε
x : ℝ
hx : x ∈ Icc (nestedInterval U n).1 (nestedInterval U n).2
⊢ x ∈ U i
Theorem: Tutorial.HasFinSubCover_of_Icc
Proof state before:
ι : Type
U : ι → Set ℝ
hU : ∀ (i : ι), IsOpen (U i)
cover : Icc 0 1 ⊆ ⋃ i, U i
H : ¬HasFinSubCover U (Icc 0 1)
c : ℝ := CauSeq.lim (nestedIntervalCauSeq U)
i : ι
hU' : c ∈ U i
ε : ℝ
ε0 : ε > 0
hε : Metric.ball c ε ⊆ U i
n : ℕ
hn : (ε / 2)⁻¹ < 2 ^ n
this : ∀ x ∈ Icc (nestedInterval U n).1 (nestedInterval U n).2, |x - c| < ε
x : ℝ
hx : x ∈ Icc (nestedInterval U n).1 (nestedInterval U n).2
⊢ x ∈ U i
Tactic:
apply hε (this x hx)
Proof state after:
no goals
Theorem: Tutorial.HasFinSubCover_of_Icc
Proof state before:
ι : Type
U : ι → Set ℝ
hU : ∀ (i : ι), IsOpen (U i)
cover : Icc 0 1 ⊆ ⋃ i, U i
H : ¬HasFinSubCover U (Icc 0 1)
c : ℝ := CauSeq.lim (nestedIntervalCauSeq U)
i : ι
hU' : c ∈ U i
ε : ℝ
ε0 : ε > 0
hε : Metric.ball c ε ⊆ U i
n : ℕ
hn : (ε / 2)⁻¹ < 2 ^ n
x : ℝ
hx : x ∈ Icc (nestedInterval U n).1 (nestedInterval U n).2
hba : (nestedInterval U n).2 - (nestedInterval U n).1 = (2 ^ n)⁻¹
⊢ 0 < ε / 2
Tactic:
linarith
Proof state after:
no goals
Theorem: Tutorial.HasFinSubCover_of_Icc
Proof state before:
ι : Type
U : ι → Set ℝ
hU : ∀ (i : ι), IsOpen (U i)
cover : Icc 0 1 ⊆ ⋃ i, U i
H : ¬HasFinSubCover U (Icc 0 1)
c : ℝ := CauSeq.lim (nestedIntervalCauSeq U)
i : ι
hU' : c ∈ U i
ε : ℝ
ε0 : ε > 0
hε : Metric.ball c ε ⊆ U i
n : ℕ
hn✝ : (ε / 2)⁻¹ < 2 ^ n
x : ℝ
hx✝ : x ∈ Icc (nestedInterval U n).1 (nestedInterval U n).2
hba : (nestedInterval U n).2 - (nestedInterval U n).1 = (2 ^ n)⁻¹
hn : (2 ^ n)⁻¹ < ε / 2
hc : (nestedInterval U n).1 ≤ c ∧ c ≤ (nestedInterval U n).2
hx : (nestedInterval U n).1 ≤ x ∧ x ≤ (nestedInterval U n).2
⊢ |x - c| = |x - (nestedInterval U n).1 - (c - (nestedInterval U n).1)|
Tactic:
simp
Proof state after:
no goals