internlm/Lean-Github huggingface dataset:
Theorem: Tutorial.hasDerivAt_pow
Proof state before:
f : ℝ → ℝ
f' a✝ : ℝ
g : ℝ → ℝ
g' a : ℝ
n : ℕ
ih : HasDerivAt (fun x => x ^ (n + 1)) ((↑n + 1) * a ^ n) a
⊢ HasDerivAt (fun x => x ^ (Nat.succ n + 1)) ((↑(Nat.succ n) + 1) * a ^ Nat.succ n) a
Tactic:
case succ n ih =>
  rw [Nat.succ_eq_add_one]
  suffices HasDerivAt (fun x => x ^ (n + 1) * x) (((n + 1) * a ^ n) * a + a ^ (n + 1) * 1) a by
    apply IsLittleO.congr_left this
    intro x
    simp
    ring
  apply ih.mul (hasDerivAt_id a)
Proof state after:
no goals
Theorem: Tutorial.hasDerivAt_pow
Proof state before:
f : ℝ → ℝ
f' a✝ : ℝ
g : ℝ → ℝ
g' a : ℝ
⊢ HasDerivAt (fun x => x ^ (Nat.zero + 1)) ((↑Nat.zero + 1) * a ^ Nat.zero) a
Tactic:
simp [hasDerivAt_iff_isLittleO_nhds_zero]
Proof state after:
no goals
Theorem: Tutorial.hasDerivAt_pow
Proof state before:
f : ℝ → ℝ
f' a✝ : ℝ
g : ℝ → ℝ
g' a : ℝ
n : ℕ
ih : HasDerivAt (fun x => x ^ (n + 1)) ((↑n + 1) * a ^ n) a
⊢ HasDerivAt (fun x => x ^ (Nat.succ n + 1)) ((↑(Nat.succ n) + 1) * a ^ Nat.succ n) a
Tactic:
rw [Nat.succ_eq_add_one]
Proof state after:
f : ℝ → ℝ
f' a✝ : ℝ
g : ℝ → ℝ
g' a : ℝ
n : ℕ
ih : HasDerivAt (fun x => x ^ (n + 1)) ((↑n + 1) * a ^ n) a
⊢ HasDerivAt (fun x => x ^ (n + 1 + 1)) ((↑(n + 1) + 1) * a ^ (n + 1)) a
Theorem: Tutorial.hasDerivAt_pow
Proof state before:
f : ℝ → ℝ
f' a✝ : ℝ
g : ℝ → ℝ
g' a : ℝ
n : ℕ
ih : HasDerivAt (fun x => x ^ (n + 1)) ((↑n + 1) * a ^ n) a
⊢ HasDerivAt (fun x => x ^ (n + 1 + 1)) ((↑(n + 1) + 1) * a ^ (n + 1)) a
Tactic:
suffices HasDerivAt (fun x => x ^ (n + 1) * x) (((n + 1) * a ^ n) * a + a ^ (n + 1) * 1) a by
  apply IsLittleO.congr_left this
  intro x
  simp
  ring
Proof state after:
f : ℝ → ℝ
f' a✝ : ℝ
g : ℝ → ℝ
g' a : ℝ
n : ℕ
ih : HasDerivAt (fun x => x ^ (n + 1)) ((↑n + 1) * a ^ n) a
⊢ HasDerivAt (fun x => x ^ (n + 1) * x) ((↑n + 1) * a ^ n * a + a ^ (n + 1) * 1) a
Theorem: Tutorial.hasDerivAt_pow
Proof state before:
f : ℝ → ℝ
f' a✝ : ℝ
g : ℝ → ℝ
g' a : ℝ
n : ℕ
ih : HasDerivAt (fun x => x ^ (n + 1)) ((↑n + 1) * a ^ n) a
⊢ HasDerivAt (fun x => x ^ (n + 1) * x) ((↑n + 1) * a ^ n * a + a ^ (n + 1) * 1) a
Tactic:
apply ih.mul (hasDerivAt_id a)
Proof state after:
no goals
Theorem: Tutorial.hasDerivAt_pow
Proof state before:
f : ℝ → ℝ
f' a✝ : ℝ
g : ℝ → ℝ
g' a : ℝ
n : ℕ
ih : HasDerivAt (fun x => x ^ (n + 1)) ((↑n + 1) * a ^ n) a
this : HasDerivAt (fun x => x ^ (n + 1) * x) ((↑n + 1) * a ^ n * a + a ^ (n + 1) * 1) a
⊢ HasDerivAt (fun x => x ^ (n + 1 + 1)) ((↑(n + 1) + 1) * a ^ (n + 1)) a
Tactic:
apply IsLittleO.congr_left this
Proof state after:
f : ℝ → ℝ
f' a✝ : ℝ
g : ℝ → ℝ
g' a : ℝ
n : ℕ
ih : HasDerivAt (fun x => x ^ (n + 1)) ((↑n + 1) * a ^ n) a
this : HasDerivAt (fun x => x ^ (n + 1) * x) ((↑n + 1) * a ^ n * a + a ^ (n + 1) * 1) a
⊢ ∀ (x : ℝ),
    (fun x => x ^ (n + 1) * x) x - (fun x => x ^ (n + 1) * x) a - (x - a) * ((↑n + 1) * a ^ n * a + a ^ (n + 1) * 1) =
      (fun x => x ^ (n + 1 + 1)) x - (fun x => x ^ (n + 1 + 1)) a - (x - a) * ((↑(n + 1) + 1) * a ^ (n + 1))
Theorem: Tutorial.hasDerivAt_pow
Proof state before:
f : ℝ → ℝ
f' a✝ : ℝ
g : ℝ → ℝ
g' a : ℝ
n : ℕ
ih : HasDerivAt (fun x => x ^ (n + 1)) ((↑n + 1) * a ^ n) a
this : HasDerivAt (fun x => x ^ (n + 1) * x) ((↑n + 1) * a ^ n * a + a ^ (n + 1) * 1) a
⊢ ∀ (x : ℝ),
    (fun x => x ^ (n + 1) * x) x - (fun x => x ^ (n + 1) * x) a - (x - a) * ((↑n + 1) * a ^ n * a + a ^ (n + 1) * 1) =
      (fun x => x ^ (n + 1 + 1)) x - (fun x => x ^ (n + 1 + 1)) a - (x - a) * ((↑(n + 1) + 1) * a ^ (n + 1))
Tactic:
intro x
Proof state after:
f : ℝ → ℝ
f' a✝ : ℝ
g : ℝ → ℝ
g' a : ℝ
n : ℕ
ih : HasDerivAt (fun x => x ^ (n + 1)) ((↑n + 1) * a ^ n) a
this : HasDerivAt (fun x => x ^ (n + 1) * x) ((↑n + 1) * a ^ n * a + a ^ (n + 1) * 1) a
x : ℝ
⊢ (fun x => x ^ (n + 1) * x) x - (fun x => x ^ (n + 1) * x) a - (x - a) * ((↑n + 1) * a ^ n * a + a ^ (n + 1) * 1) =
    (fun x => x ^ (n + 1 + 1)) x - (fun x => x ^ (n + 1 + 1)) a - (x - a) * ((↑(n + 1) + 1) * a ^ (n + 1))
Theorem: Tutorial.hasDerivAt_pow
Proof state before:
f : ℝ → ℝ
f' a✝ : ℝ
g : ℝ → ℝ
g' a : ℝ
n : ℕ
ih : HasDerivAt (fun x => x ^ (n + 1)) ((↑n + 1) * a ^ n) a
this : HasDerivAt (fun x => x ^ (n + 1) * x) ((↑n + 1) * a ^ n * a + a ^ (n + 1) * 1) a
x : ℝ
⊢ (fun x => x ^ (n + 1) * x) x - (fun x => x ^ (n + 1) * x) a - (x - a) * ((↑n + 1) * a ^ n * a + a ^ (n + 1) * 1) =
    (fun x => x ^ (n + 1 + 1)) x - (fun x => x ^ (n + 1 + 1)) a - (x - a) * ((↑(n + 1) + 1) * a ^ (n + 1))
Tactic:
simp
Proof state after:
f : ℝ → ℝ
f' a✝ : ℝ
g : ℝ → ℝ
g' a : ℝ
n : ℕ
ih : HasDerivAt (fun x => x ^ (n + 1)) ((↑n + 1) * a ^ n) a
this : HasDerivAt (fun x => x ^ (n + 1) * x) ((↑n + 1) * a ^ n * a + a ^ (n + 1) * 1) a
x : ℝ
⊢ x ^ (n + 1) * x - a ^ (n + 1) * a - (x - a) * ((↑n + 1) * a ^ n * a + a ^ (n + 1)) =
    x ^ (n + 1 + 1) - a ^ (n + 1 + 1) - (x - a) * ((↑n + 1 + 1) * a ^ (n + 1))
Theorem: Tutorial.hasDerivAt_pow
Proof state before:
f : ℝ → ℝ
f' a✝ : ℝ
g : ℝ → ℝ
g' a : ℝ
n : ℕ
ih : HasDerivAt (fun x => x ^ (n + 1)) ((↑n + 1) * a ^ n) a
this : HasDerivAt (fun x => x ^ (n + 1) * x) ((↑n + 1) * a ^ n * a + a ^ (n + 1) * 1) a
x : ℝ
⊢ x ^ (n + 1) * x - a ^ (n + 1) * a - (x - a) * ((↑n + 1) * a ^ n * a + a ^ (n + 1)) =
    x ^ (n + 1 + 1) - a ^ (n + 1 + 1) - (x - a) * ((↑n + 1 + 1) * a ^ (n + 1))
Tactic:
ring
Proof state after:
no goals
Theorem: Tutorial.abs_of_ten_inv
Proof state before:
i : ℕ
⊢ 0 < 10
Tactic:
linarith
Proof state after:
no goals
Theorem: Tutorial.«0.9999999 = 1»
Proof state before:
⊢ { cauchy := ⟦«0.9999999»⟧ } = 1
Tactic:
calc _ = Real.ofCauchy (Quotient.mk CauSeq.equiv (CauSeq.const abs 1)) := ?_
     _ = (1 : ℝ) := Real.ofCauchy_one
Proof state after:
⊢ { cauchy := ⟦«0.9999999»⟧ } = { cauchy := ⟦CauSeq.const abs 1⟧ }
Theorem: Tutorial.«0.9999999 = 1»
Proof state before:
⊢ { cauchy := ⟦«0.9999999»⟧ } = { cauchy := ⟦CauSeq.const abs 1⟧ }
Tactic:
rw [«0.9999999»]
Proof state after:
⊢ { cauchy := ⟦{ val := fun n => 1 - (10 ^ n)⁻¹, property := «0.9999999».proof_1 }⟧ } =
    { cauchy := ⟦CauSeq.const abs 1⟧ }
Theorem: Tutorial.«0.9999999 = 1»
Proof state before:
⊢ { cauchy := ⟦{ val := fun n => 1 - (10 ^ n)⁻¹, property := «0.9999999».proof_1 }⟧ } =
    { cauchy := ⟦CauSeq.const abs 1⟧ }
Tactic:
congr 1
Proof state after:
case e_cauchy

⊢ ⟦{ val := fun n => 1 - (10 ^ n)⁻¹, property := «0.9999999».proof_1 }⟧ = ⟦CauSeq.const abs 1⟧
Theorem: Tutorial.«0.9999999 = 1»
Proof state before:
case e_cauchy

⊢ ⟦{ val := fun n => 1 - (10 ^ n)⁻¹, property := «0.9999999».proof_1 }⟧ = ⟦CauSeq.const abs 1⟧
Tactic:
apply Quotient.sound
Proof state after:
case e_cauchy.a

⊢ { val := fun n => 1 - (10 ^ n)⁻¹, property := «0.9999999».proof_1 } ≈ CauSeq.const abs 1
Theorem: Tutorial.«0.9999999 = 1»
Proof state before:
case e_cauchy.a

⊢ { val := fun n => 1 - (10 ^ n)⁻¹, property := «0.9999999».proof_1 } ≈ CauSeq.const abs 1
Tactic:
intro ε ε0
Proof state after:
case e_cauchy.a
ε : ℚ
ε0 : ε > 0
⊢ ∃ i, ∀ j ≥ i, |↑({ val := fun n => 1 - (10 ^ n)⁻¹, property := «0.9999999».proof_1 } - CauSeq.const abs 1) j| < ε
Theorem: Tutorial.«0.9999999 = 1»
Proof state before:
case e_cauchy.a
ε : ℚ
ε0 : ε > 0
⊢ ∃ i, ∀ j ≥ i, |↑({ val := fun n => 1 - (10 ^ n)⁻¹, property := «0.9999999».proof_1 } - CauSeq.const abs 1) j| < ε
Tactic:
suffices ∃ i, ∀ (j : ℕ), j ≥ i → (10 ^ j : ℚ)⁻¹ < ε by simpa [abs_of_ten_inv]
Proof state after:
case e_cauchy.a
ε : ℚ
ε0 : ε > 0
⊢ ∃ i, ∀ j ≥ i, (10 ^ j)⁻¹ < ε
Theorem: Tutorial.«0.9999999 = 1»
Proof state before:
case e_cauchy.a
ε : ℚ
ε0 : ε > 0
⊢ ∃ i, ∀ j ≥ i, (10 ^ j)⁻¹ < ε
Tactic:
sorry
Proof state after:
no goals
Theorem: Tutorial.«0.9999999 = 1»
Proof state before:
ε : ℚ
ε0 : ε > 0
this : ∃ i, ∀ j ≥ i, (10 ^ j)⁻¹ < ε
⊢ ∃ i, ∀ j ≥ i, |↑({ val := fun n => 1 - (10 ^ n)⁻¹, property := «0.9999999».proof_1 } - CauSeq.const abs 1) j| < ε
Tactic:
simpa [abs_of_ten_inv]
Proof state after:
no goals
Theorem: Tutorial.hasFinSubCover_concat
Proof state before:
ι : Type
U : ι → Set ℝ
a c b : ℝ
hac : HasFinSubCover U (Icc a c)
hcb : HasFinSubCover U (Icc c b)
⊢ HasFinSubCover U (Icc a b)
Tactic:
rcases hac with ⟨ι_ac, cover_ac⟩
Proof state after:
case intro
ι : Type
U : ι → Set ℝ
a c b : ℝ
hcb : HasFinSubCover U (Icc c b)
ι_ac : Finset ι
cover_ac : Icc a c ⊆ ⋃ i ∈ ι_ac, U i
⊢ HasFinSubCover U (Icc a b)
Theorem: Tutorial.hasFinSubCover_concat
Proof state before:
case intro
ι : Type
U : ι → Set ℝ
a c b : ℝ
hcb : HasFinSubCover U (Icc c b)
ι_ac : Finset ι
cover_ac : Icc a c ⊆ ⋃ i ∈ ι_ac, U i
⊢ HasFinSubCover U (Icc a b)
Tactic:
rcases hcb with ⟨ι_cb, cover_cb⟩
Proof state after:
case intro.intro
ι : Type
U : ι → Set ℝ
a c b : ℝ
ι_ac : Finset ι
cover_ac : Icc a c ⊆ ⋃ i ∈ ι_ac, U i
ι_cb : Finset ι
cover_cb : Icc c b ⊆ ⋃ i ∈ ι_cb, U i
⊢ HasFinSubCover U (Icc a b)
Theorem: Tutorial.hasFinSubCover_concat
Proof state before:
case intro.intro
ι : Type
U : ι → Set ℝ
a c b : ℝ
ι_ac : Finset ι
cover_ac : Icc a c ⊆ ⋃ i ∈ ι_ac, U i
ι_cb : Finset ι
cover_cb : Icc c b ⊆ ⋃ i ∈ ι_cb, U i
⊢ HasFinSubCover U (Icc a b)
Tactic:
exists ι_ac ∪ ι_cb
Proof state after:
case intro.intro
ι : Type
U : ι → Set ℝ
a c b : ℝ
ι_ac : Finset ι
cover_ac : Icc a c ⊆ ⋃ i ∈ ι_ac, U i
ι_cb : Finset ι
cover_cb : Icc c b ⊆ ⋃ i ∈ ι_cb, U i
⊢ Icc a b ⊆ ⋃ i ∈ ι_ac ∪ ι_cb, U i
Theorem: Tutorial.hasFinSubCover_concat
Proof state before:
case intro.intro
ι : Type
U : ι → Set ℝ
a c b : ℝ
ι_ac : Finset ι
cover_ac : Icc a c ⊆ ⋃ i ∈ ι_ac, U i
ι_cb : Finset ι
cover_cb : Icc c b ⊆ ⋃ i ∈ ι_cb, U i
⊢ Icc a b ⊆ ⋃ i ∈ ι_ac ∪ ι_cb, U i
Tactic:
intro x hx
Proof state after:
case intro.intro
ι : Type
U : ι → Set ℝ
a c b : ℝ
ι_ac : Finset ι
cover_ac : Icc a c ⊆ ⋃ i ∈ ι_ac, U i
ι_cb : Finset ι
cover_cb : Icc c b ⊆ ⋃ i ∈ ι_cb, U i
x : ℝ
hx : x ∈ Icc a b
⊢ x ∈ ⋃ i ∈ ι_ac ∪ ι_cb, U i
Theorem: Tutorial.hasFinSubCover_concat
Proof state before:
case intro.intro
ι : Type
U : ι → Set ℝ
a c b : ℝ
ι_ac : Finset ι
cover_ac : Icc a c ⊆ ⋃ i ∈ ι_ac, U i
ι_cb : Finset ι
cover_cb : Icc c b ⊆ ⋃ i ∈ ι_cb, U i
x : ℝ
hx : x ∈ Icc a b
⊢ x ∈ ⋃ i ∈ ι_ac ∪ ι_cb, U i
Tactic:
suffices ∃ i, (i ∈ ι_ac ∨ i ∈ ι_cb) ∧ x ∈ U i by
  simpa using this
Proof state after:
case intro.intro
ι : Type
U : ι → Set ℝ
a c b : ℝ
ι_ac : Finset ι
cover_ac : Icc a c ⊆ ⋃ i ∈ ι_ac, U i
ι_cb : Finset ι
cover_cb : Icc c b ⊆ ⋃ i ∈ ι_cb, U i
x : ℝ
hx : x ∈ Icc a b
⊢ ∃ i, (i ∈ ι_ac ∨ i ∈ ι_cb) ∧ x ∈ U i
Theorem: Tutorial.hasFinSubCover_concat
Proof state before:
case intro.intro
ι : Type
U : ι → Set ℝ
a c b : ℝ
ι_ac : Finset ι
cover_ac : Icc a c ⊆ ⋃ i ∈ ι_ac, U i
ι_cb : Finset ι
cover_cb : Icc c b ⊆ ⋃ i ∈ ι_cb, U i
x : ℝ
hx : x ∈ Icc a b
⊢ ∃ i, (i ∈ ι_ac ∨ i ∈ ι_cb) ∧ x ∈ U i
Tactic:
cases le_total x c
Proof state after:
case intro.intro.inl
ι : Type
U : ι → Set ℝ
a c b : ℝ
ι_ac : Finset ι
cover_ac : Icc a c ⊆ ⋃ i ∈ ι_ac, U i
ι_cb : Finset ι
cover_cb : Icc c b ⊆ ⋃ i ∈ ι_cb, U i
x : ℝ
hx : x ∈ Icc a b
h✝ : x ≤ c
⊢ ∃ i, (i ∈ ι_ac ∨ i ∈ ι_cb) ∧ x ∈ U i

case intro.intro.inr
ι : Type
U : ι → Set ℝ
a c b : ℝ
ι_ac : Finset ι
cover_ac : Icc a c ⊆ ⋃ i ∈ ι_ac, U i
ι_cb : Finset ι
cover_cb : Icc c b ⊆ ⋃ i ∈ ι_cb, U i
x : ℝ
hx : x ∈ Icc a b
h✝ : c ≤ x
⊢ ∃ i, (i ∈ ι_ac ∨ i ∈ ι_cb) ∧ x ∈ U i
Theorem: Tutorial.hasFinSubCover_concat
Proof state before:
ι : Type
U : ι → Set ℝ
a c b : ℝ
ι_ac : Finset ι
cover_ac : Icc a c ⊆ ⋃ i ∈ ι_ac, U i
ι_cb : Finset ι
cover_cb : Icc c b ⊆ ⋃ i ∈ ι_cb, U i
x : ℝ
hx : x ∈ Icc a b
hxc : x ≤ c
⊢ ∃ i, (i ∈ ι_ac ∨ i ∈ ι_cb) ∧ x ∈ U i
Tactic:
case inl hxc =>
  obtain ⟨i, hi⟩ : ∃ i, i ∈ ι_ac ∧ x ∈ U i := by simpa using cover_ac ⟨hx.left, hxc⟩
  exact ⟨i, Or.inl hi.1, hi.2⟩
Proof state after:
no goals
Theorem: Tutorial.hasFinSubCover_concat
Proof state before:
ι : Type
U : ι → Set ℝ
a c b : ℝ
ι_ac : Finset ι
cover_ac : Icc a c ⊆ ⋃ i ∈ ι_ac, U i
ι_cb : Finset ι
cover_cb : Icc c b ⊆ ⋃ i ∈ ι_cb, U i
x : ℝ
hx : x ∈ Icc a b
hxc : c ≤ x
⊢ ∃ i, (i ∈ ι_ac ∨ i ∈ ι_cb) ∧ x ∈ U i
Tactic:
case inr hxc =>
  obtain ⟨i, hi⟩ : ∃ i, i ∈ ι_cb ∧ x ∈ U i := by simpa using cover_cb ⟨hxc, hx.right⟩
  exact ⟨i, Or.inr hi.1, hi.2⟩
Proof state after:
no goals
Theorem: Tutorial.hasFinSubCover_concat
Proof state before:
ι : Type
U : ι → Set ℝ
a c b : ℝ
ι_ac : Finset ι
cover_ac : Icc a c ⊆ ⋃ i ∈ ι_ac, U i
ι_cb : Finset ι
cover_cb : Icc c b ⊆ ⋃ i ∈ ι_cb, U i
x : ℝ
hx : x ∈ Icc a b
this : ∃ i, (i ∈ ι_ac ∨ i ∈ ι_cb) ∧ x ∈ U i
⊢ x ∈ ⋃ i ∈ ι_ac ∪ ι_cb, U i
Tactic:
simpa using this
Proof state after:
no goals
Theorem: Tutorial.hasFinSubCover_concat
Proof state before:
ι : Type
U : ι → Set ℝ
a c b : ℝ
ι_ac : Finset ι
cover_ac : Icc a c ⊆ ⋃ i ∈ ι_ac, U i
ι_cb : Finset ι
cover_cb : Icc c b ⊆ ⋃ i ∈ ι_cb, U i
x : ℝ
hx : x ∈ Icc a b
hxc : x ≤ c
⊢ ∃ i, (i ∈ ι_ac ∨ i ∈ ι_cb) ∧ x ∈ U i
Tactic:
obtain ⟨i, hi⟩ : ∃ i, i ∈ ι_ac ∧ x ∈ U i := by simpa using cover_ac ⟨hx.left, hxc⟩
Proof state after:
case intro
ι : Type
U : ι → Set ℝ
a c b : ℝ
ι_ac : Finset ι
cover_ac : Icc a c ⊆ ⋃ i ∈ ι_ac, U i
ι_cb : Finset ι
cover_cb : Icc c b ⊆ ⋃ i ∈ ι_cb, U i
x : ℝ
hx : x ∈ Icc a b
hxc : x ≤ c
i : ι
hi : i ∈ ι_ac ∧ x ∈ U i
⊢ ∃ i, (i ∈ ι_ac ∨ i ∈ ι_cb) ∧ x ∈ U i
Theorem: Tutorial.hasFinSubCover_concat
Proof state before:
case intro
ι : Type
U : ι → Set ℝ
a c b : ℝ
ι_ac : Finset ι
cover_ac : Icc a c ⊆ ⋃ i ∈ ι_ac, U i
ι_cb : Finset ι
cover_cb : Icc c b ⊆ ⋃ i ∈ ι_cb, U i
x : ℝ
hx : x ∈ Icc a b
hxc : x ≤ c
i : ι
hi : i ∈ ι_ac ∧ x ∈ U i
⊢ ∃ i, (i ∈ ι_ac ∨ i ∈ ι_cb) ∧ x ∈ U i
Tactic:
exact ⟨i, Or.inl hi.1, hi.2⟩
Proof state after:
no goals
Theorem: Tutorial.hasFinSubCover_concat
Proof state before:
ι : Type
U : ι → Set ℝ
a c b : ℝ
ι_ac : Finset ι
cover_ac : Icc a c ⊆ ⋃ i ∈ ι_ac, U i
ι_cb : Finset ι
cover_cb : Icc c b ⊆ ⋃ i ∈ ι_cb, U i
x : ℝ
hx : x ∈ Icc a b
hxc : x ≤ c
⊢ ∃ i ∈ ι_ac, x ∈ U i
Tactic:
simpa using cover_ac ⟨hx.left, hxc⟩
Proof state after:
no goals
Theorem: Tutorial.hasFinSubCover_concat
Proof state before:
ι : Type
U : ι → Set ℝ
a c b : ℝ
ι_ac : Finset ι
cover_ac : Icc a c ⊆ ⋃ i ∈ ι_ac, U i
ι_cb : Finset ι
cover_cb : Icc c b ⊆ ⋃ i ∈ ι_cb, U i
x : ℝ
hx : x ∈ Icc a b
hxc : c ≤ x
⊢ ∃ i, (i ∈ ι_ac ∨ i ∈ ι_cb) ∧ x ∈ U i
Tactic:
obtain ⟨i, hi⟩ : ∃ i, i ∈ ι_cb ∧ x ∈ U i := by simpa using cover_cb ⟨hxc, hx.right⟩
Proof state after:
case intro
ι : Type
U : ι → Set ℝ
a c b : ℝ
ι_ac : Finset ι
cover_ac : Icc a c ⊆ ⋃ i ∈ ι_ac, U i
ι_cb : Finset ι
cover_cb : Icc c b ⊆ ⋃ i ∈ ι_cb, U i
x : ℝ
hx : x ∈ Icc a b
hxc : c ≤ x
i : ι
hi : i ∈ ι_cb ∧ x ∈ U i
⊢ ∃ i, (i ∈ ι_ac ∨ i ∈ ι_cb) ∧ x ∈ U i
Theorem: Tutorial.hasFinSubCover_concat
Proof state before:
case intro
ι : Type
U : ι → Set ℝ
a c b : ℝ
ι_ac : Finset ι
cover_ac : Icc a c ⊆ ⋃ i ∈ ι_ac, U i
ι_cb : Finset ι
cover_cb : Icc c b ⊆ ⋃ i ∈ ι_cb, U i
x : ℝ
hx : x ∈ Icc a b
hxc : c ≤ x
i : ι
hi : i ∈ ι_cb ∧ x ∈ U i
⊢ ∃ i, (i ∈ ι_ac ∨ i ∈ ι_cb) ∧ x ∈ U i
Tactic:
exact ⟨i, Or.inr hi.1, hi.2⟩
Proof state after:
no goals
Theorem: Tutorial.hasFinSubCover_concat
Proof state before:
ι : Type
U : ι → Set ℝ
a c b : ℝ
ι_ac : Finset ι
cover_ac : Icc a c ⊆ ⋃ i ∈ ι_ac, U i
ι_cb : Finset ι
cover_cb : Icc c b ⊆ ⋃ i ∈ ι_cb, U i
x : ℝ
hx : x ∈ Icc a b
hxc : c ≤ x
⊢ ∃ i ∈ ι_cb, x ∈ U i
Tactic:
simpa using cover_cb ⟨hxc, hx.right⟩
Proof state after:
no goals
Theorem: Tutorial.not_HasFinSubCover_concat
Proof state before:
ι : Type
U : ι → Set ℝ
a b c : ℝ
⊢ ¬HasFinSubCover U (Icc a b) → HasFinSubCover U (Icc a c) → ¬HasFinSubCover U (Icc c b)
Tactic:
contrapose!
Proof state after:
ι : Type
U : ι → Set ℝ
a b c : ℝ
⊢ HasFinSubCover U (Icc a c) ∧ HasFinSubCover U (Icc c b) → HasFinSubCover U (Icc a b)
Theorem: Tutorial.not_HasFinSubCover_concat
Proof state before:
ι : Type
U : ι → Set ℝ
a b c : ℝ
⊢ HasFinSubCover U (Icc a c) ∧ HasFinSubCover U (Icc c b) → HasFinSubCover U (Icc a b)
Tactic:
apply (fun H ↦ hasFinSubCover_concat H.1 H.2)
Proof state after:
no goals
Theorem: Tutorial.nestedIntervalSucc_eq_or_eq
Proof state before:
ι : Type
U : ι → Set ℝ
a b : ℝ
⊢ nestedIntervalSucc U a b = (a, (a + b) / 2) ∨ nestedIntervalSucc U a b = ((a + b) / 2, b)
Tactic:
apply ite_eq_or_eq
Proof state after:
no goals
Theorem: Tutorial.nestedInterval_le
Proof state before:
ι : Type
U : ι → Set ℝ
n : ℕ
⊢ (nestedInterval U (n + 1)).1 < (nestedInterval U (n + 1)).2
Tactic:
have := nestedInterval_le n
Proof state after:
ι : Type
U : ι → Set ℝ
n : ℕ
this : (nestedInterval U n).1 < (nestedInterval U n).2
⊢ (nestedInterval U (n + 1)).1 < (nestedInterval U (n + 1)).2
Theorem: Tutorial.nestedInterval_le
Proof state before:
ι : Type
U : ι → Set ℝ
n : ℕ
this : (nestedInterval U n).1 < (nestedInterval U n).2
⊢ (nestedInterval U (n + 1)).1 < (nestedInterval U (n + 1)).2
Tactic:
cases nestedIntervalSucc_eq_or_eq U (α n) (β n) with
| inl h => rw [nestedInterval, h]; dsimp only; linarith
| inr h => rw [nestedInterval, h]; dsimp only; linarith
Proof state after:
no goals
Theorem: Tutorial.nestedInterval_le
Proof state before:
case inl
ι : Type
U : ι → Set ℝ
n : ℕ
this : (nestedInterval U n).1 < (nestedInterval U n).2
h :
  nestedIntervalSucc U (nestedInterval U n).1 (nestedInterval U n).2 =
    ((nestedInterval U n).1, ((nestedInterval U n).1 + (nestedInterval U n).2) / 2)
⊢ (nestedInterval U (n + 1)).1 < (nestedInterval U (n + 1)).2
Tactic:
rw [nestedInterval, h]
Proof state after:
case inl
ι : Type
U : ι → Set ℝ
n : ℕ
this : (nestedInterval U n).1 < (nestedInterval U n).2
h :
  nestedIntervalSucc U (nestedInterval U n).1 (nestedInterval U n).2 =
    ((nestedInterval U n).1, ((nestedInterval U n).1 + (nestedInterval U n).2) / 2)
⊢ ((nestedInterval U n).1, ((nestedInterval U n).1 + (nestedInterval U n).2) / 2).1 <
    ((nestedInterval U n).1, ((nestedInterval U n).1 + (nestedInterval U n).2) / 2).2
Theorem: Tutorial.nestedInterval_le
Proof state before:
case inl
ι : Type
U : ι → Set ℝ
n : ℕ
this : (nestedInterval U n).1 < (nestedInterval U n).2
h :
  nestedIntervalSucc U (nestedInterval U n).1 (nestedInterval U n).2 =
    ((nestedInterval U n).1, ((nestedInterval U n).1 + (nestedInterval U n).2) / 2)
⊢ ((nestedInterval U n).1, ((nestedInterval U n).1 + (nestedInterval U n).2) / 2).1 <
    ((nestedInterval U n).1, ((nestedInterval U n).1 + (nestedInterval U n).2) / 2).2
Tactic:
dsimp only
Proof state after:
case inl
ι : Type
U : ι → Set ℝ
n : ℕ
this : (nestedInterval U n).1 < (nestedInterval U n).2
h :
  nestedIntervalSucc U (nestedInterval U n).1 (nestedInterval U n).2 =
    ((nestedInterval U n).1, ((nestedInterval U n).1 + (nestedInterval U n).2) / 2)
⊢ (nestedInterval U n).1 < ((nestedInterval U n).1 + (nestedInterval U n).2) / 2
Theorem: Tutorial.nestedInterval_le
Proof state before:
case inl
ι : Type
U : ι → Set ℝ
n : ℕ
this : (nestedInterval U n).1 < (nestedInterval U n).2
h :
  nestedIntervalSucc U (nestedInterval U n).1 (nestedInterval U n).2 =
    ((nestedInterval U n).1, ((nestedInterval U n).1 + (nestedInterval U n).2) / 2)
⊢ (nestedInterval U n).1 < ((nestedInterval U n).1 + (nestedInterval U n).2) / 2
Tactic:
linarith
Proof state after:
no goals
Theorem: Tutorial.nestedInterval_le
Proof state before:
case inr
ι : Type
U : ι → Set ℝ
n : ℕ
this : (nestedInterval U n).1 < (nestedInterval U n).2
h :
  nestedIntervalSucc U (nestedInterval U n).1 (nestedInterval U n).2 =
    (((nestedInterval U n).1 + (nestedInterval U n).2) / 2, (nestedInterval U n).2)
⊢ (nestedInterval U (n + 1)).1 < (nestedInterval U (n + 1)).2
Tactic:
rw [nestedInterval, h]
Proof state after:
case inr
ι : Type
U : ι → Set ℝ
n : ℕ
this : (nestedInterval U n).1 < (nestedInterval U n).2
h :
  nestedIntervalSucc U (nestedInterval U n).1 (nestedInterval U n).2 =
    (((nestedInterval U n).1 + (nestedInterval U n).2) / 2, (nestedInterval U n).2)
⊢ (((nestedInterval U n).1 + (nestedInterval U n).2) / 2, (nestedInterval U n).2).1 <
    (((nestedInterval U n).1 + (nestedInterval U n).2) / 2, (nestedInterval U n).2).2
Theorem: Tutorial.nestedInterval_le
Proof state before:
case inr
ι : Type
U : ι → Set ℝ
n : ℕ
this : (nestedInterval U n).1 < (nestedInterval U n).2
h :
  nestedIntervalSucc U (nestedInterval U n).1 (nestedInterval U n).2 =
    (((nestedInterval U n).1 + (nestedInterval U n).2) / 2, (nestedInterval U n).2)
⊢ (((nestedInterval U n).1 + (nestedInterval U n).2) / 2, (nestedInterval U n).2).1 <
    (((nestedInterval U n).1 + (nestedInterval U n).2) / 2, (nestedInterval U n).2).2
Tactic:
dsimp only
Proof state after:
case inr
ι : Type
U : ι → Set ℝ
n : ℕ
this : (nestedInterval U n).1 < (nestedInterval U n).2
h :
  nestedIntervalSucc U (nestedInterval U n).1 (nestedInterval U n).2 =
    (((nestedInterval U n).1 + (nestedInterval U n).2) / 2, (nestedInterval U n).2)
⊢ ((nestedInterval U n).1 + (nestedInterval U n).2) / 2 < (nestedInterval U n).2
Theorem: Tutorial.nestedInterval_le
Proof state before:
case inr
ι : Type
U : ι → Set ℝ
n : ℕ
this : (nestedInterval U n).1 < (nestedInterval U n).2
h :
  nestedIntervalSucc U (nestedInterval U n).1 (nestedInterval U n).2 =
    (((nestedInterval U n).1 + (nestedInterval U n).2) / 2, (nestedInterval U n).2)
⊢ ((nestedInterval U n).1 + (nestedInterval U n).2) / 2 < (nestedInterval U n).2
Tactic:
linarith
Proof state after:
no goals
Theorem: Tutorial.nestedIntervalSeq_is_nested_succ
Proof state before:
ι : Type
U : ι → Set ℝ
n : ℕ
⊢ Icc (nestedInterval U (n + 1)).1 (nestedInterval U (n + 1)).2 ⊆ Icc (nestedInterval U n).1 (nestedInterval U n).2
Tactic:
have := nestedInterval_le U n
Proof state after:
ι : Type
U : ι → Set ℝ
n : ℕ
this : (nestedInterval U n).1 < (nestedInterval U n).2
⊢ Icc (nestedInterval U (n + 1)).1 (nestedInterval U (n + 1)).2 ⊆ Icc (nestedInterval U n).1 (nestedInterval U n).2
Theorem: Tutorial.nestedIntervalSeq_is_nested_succ
Proof state before:
ι : Type
U : ι → Set ℝ
n : ℕ
this : (nestedInterval U n).1 < (nestedInterval U n).2
⊢ Icc (nestedInterval U (n + 1)).1 (nestedInterval U (n + 1)).2 ⊆ Icc (nestedInterval U n).1 (nestedInterval U n).2
Tactic:
cases nestedIntervalSucc_eq_or_eq U (α n) (β n) with
| inl h =>
  apply Icc_subset_Icc (by rw [nestedInterval, h]) (by rw [nestedInterval, h]; dsimp only; linarith)
| inr h =>
  apply Icc_subset_Icc (by rw [nestedInterval, h]; dsimp only; linarith) (by rw [nestedInterval, h])
Proof state after:
no goals
Theorem: Tutorial.nestedIntervalSeq_is_nested_succ
Proof state before:
case inl
ι : Type
U : ι → Set ℝ
n : ℕ
this : (nestedInterval U n).1 < (nestedInterval U n).2
h :
  nestedIntervalSucc U (nestedInterval U n).1 (nestedInterval U n).2 =
    ((nestedInterval U n).1, ((nestedInterval U n).1 + (nestedInterval U n).2) / 2)
⊢ Icc (nestedInterval U (n + 1)).1 (nestedInterval U (n + 1)).2 ⊆ Icc (nestedInterval U n).1 (nestedInterval U n).2
Tactic:
apply Icc_subset_Icc (by rw [nestedInterval, h]) (by rw [nestedInterval, h]; dsimp only; linarith)
Proof state after:
no goals
Theorem: Tutorial.nestedIntervalSeq_is_nested_succ
Proof state before:
ι : Type
U : ι → Set ℝ
n : ℕ
this : (nestedInterval U n).1 < (nestedInterval U n).2
h :
  nestedIntervalSucc U (nestedInterval U n).1 (nestedInterval U n).2 =
    ((nestedInterval U n).1, ((nestedInterval U n).1 + (nestedInterval U n).2) / 2)
⊢ (nestedInterval U n).1 ≤ (nestedInterval U (n + 1)).1
Tactic:
rw [nestedInterval, h]
Proof state after:
no goals
Theorem: Tutorial.nestedIntervalSeq_is_nested_succ
Proof state before:
ι : Type
U : ι → Set ℝ
n : ℕ
this : (nestedInterval U n).1 < (nestedInterval U n).2
h :
  nestedIntervalSucc U (nestedInterval U n).1 (nestedInterval U n).2 =
    ((nestedInterval U n).1, ((nestedInterval U n).1 + (nestedInterval U n).2) / 2)
⊢ (nestedInterval U (n + 1)).2 ≤ (nestedInterval U n).2
Tactic:
rw [nestedInterval, h]
Proof state after:
ι : Type
U : ι → Set ℝ
n : ℕ
this : (nestedInterval U n).1 < (nestedInterval U n).2
h :
  nestedIntervalSucc U (nestedInterval U n).1 (nestedInterval U n).2 =
    ((nestedInterval U n).1, ((nestedInterval U n).1 + (nestedInterval U n).2) / 2)
⊢ ((nestedInterval U n).1, ((nestedInterval U n).1 + (nestedInterval U n).2) / 2).2 ≤ (nestedInterval U n).2
Theorem: Tutorial.nestedIntervalSeq_is_nested_succ
Proof state before:
ι : Type
U : ι → Set ℝ
n : ℕ
this : (nestedInterval U n).1 < (nestedInterval U n).2
h :
  nestedIntervalSucc U (nestedInterval U n).1 (nestedInterval U n).2 =
    ((nestedInterval U n).1, ((nestedInterval U n).1 + (nestedInterval U n).2) / 2)
⊢ ((nestedInterval U n).1, ((nestedInterval U n).1 + (nestedInterval U n).2) / 2).2 ≤ (nestedInterval U n).2
Tactic:
dsimp only
Proof state after:
ι : Type
U : ι → Set ℝ
n : ℕ
this : (nestedInterval U n).1 < (nestedInterval U n).2
h :
  nestedIntervalSucc U (nestedInterval U n).1 (nestedInterval U n).2 =
    ((nestedInterval U n).1, ((nestedInterval U n).1 + (nestedInterval U n).2) / 2)
⊢ ((nestedInterval U n).1 + (nestedInterval U n).2) / 2 ≤ (nestedInterval U n).2