internlm/Lean-Github huggingface dataset:
Theorem: exercise6_2
Proof state before:
ι : Type u_1
L : Filter ι
s : ι → Set ℝ
t : Set ℝ
f : ℝ → ℝ
ha : ∀ (x : ℝ), f x ≠ 0
⊢ (∀ (x : ℝ), ∀ᶠ (i : ι) in L, x ∈ s i ↔ x ∈ t) ↔
    ∀ (x : ℝ), Tendsto (fun i => indicator (s i) f x) L (𝓝 (indicator t f x))
Tactic:
sorry
Proof state after:
no goals
Theorem: exercise6_3
Proof state before:
α : Type u_1
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
f : α → α
hf : Continuous f
h2f : Injective f
a b x : α
hab : a ≤ b
h2ab : f a < f b
hx : a ≤ x
⊢ f a ≤ f x
Tactic:
sorry
Proof state after:
no goals
Theorem: exercise6_4
Proof state before:
α : Type u_1
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
f : α → α
hf : Continuous f
h2f : Injective f
a b : α
hab : a ≤ b
h2ab : f a < f b
⊢ StrictMonoOn f (Ici a)
Tactic:
sorry
Proof state after:
no goals
Theorem: exercise6_5
Proof state before:
α : Type u_1
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
f : ℝ → ℝ
hf : Continuous f
h2f : Injective f
⊢ StrictMono f ∨ StrictAnti f
Tactic:
have h3f : ∀ {a b : ℝ} (hab : a ≤ b) (h2ab : f a < f b), StrictMonoOn f (Iic b)
Proof state after:
case h3f
α : Type u_1
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
f : ℝ → ℝ
hf : Continuous f
h2f : Injective f
⊢ ∀ {a b : ℝ}, a ≤ b → f a < f b → StrictMonoOn f (Iic b)

α : Type u_1
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
f : ℝ → ℝ
hf : Continuous f
h2f : Injective f
h3f : ∀ {a b : ℝ}, a ≤ b → f a < f b → StrictMonoOn f (Iic b)
⊢ StrictMono f ∨ StrictAnti f
Theorem: exercise6_5
Proof state before:
α : Type u_1
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
f : ℝ → ℝ
hf : Continuous f
h2f : Injective f
h3f : ∀ {a b : ℝ}, a ≤ b → f a < f b → StrictMonoOn f (Iic b)
⊢ StrictMono f ∨ StrictAnti f
Tactic:
sorry
Proof state after:
no goals
Theorem: exercise6_5
Proof state before:
case h3f
α : Type u_1
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
f : ℝ → ℝ
hf : Continuous f
h2f : Injective f
⊢ ∀ {a b : ℝ}, a ≤ b → f a < f b → StrictMonoOn f (Iic b)
Tactic:
intro a b hab h2ab
Proof state after:
case h3f
α : Type u_1
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
f : ℝ → ℝ
hf : Continuous f
h2f : Injective f
a b : ℝ
hab : a ≤ b
h2ab : f a < f b
⊢ StrictMonoOn f (Iic b)
Theorem: exercise6_5
Proof state before:
case h3f
α : Type u_1
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
f : ℝ → ℝ
hf : Continuous f
h2f : Injective f
a b : ℝ
hab : a ≤ b
h2ab : f a < f b
⊢ StrictMonoOn f (Iic b)
Tactic:
have := exercise6_4 (OrderDual ℝ) hf h2f hab h2ab
Proof state after:
case h3f
α : Type u_1
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
f : ℝ → ℝ
hf : Continuous f
h2f : Injective f
a b : ℝ
hab : a ≤ b
h2ab : f a < f b
this : StrictMonoOn f (Ici b)
⊢ StrictMonoOn f (Iic b)
Theorem: exercise6_5
Proof state before:
case h3f
α : Type u_1
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
f : ℝ → ℝ
hf : Continuous f
h2f : Injective f
a b : ℝ
hab : a ≤ b
h2ab : f a < f b
this : StrictMonoOn f (Ici b)
⊢ StrictMonoOn f (Iic b)
Tactic:
convert this using 0
Proof state after:
case a
α : Type u_1
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
f : ℝ → ℝ
hf : Continuous f
h2f : Injective f
a b : ℝ
hab : a ≤ b
h2ab : f a < f b
this : StrictMonoOn f (Ici b)
⊢ StrictMonoOn f (Iic b) ↔ StrictMonoOn f (Ici b)
Theorem: exercise6_5
Proof state before:
case a
α : Type u_1
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
f : ℝ → ℝ
hf : Continuous f
h2f : Injective f
a b : ℝ
hab : a ≤ b
h2ab : f a < f b
this : StrictMonoOn f (Ici b)
⊢ StrictMonoOn f (Iic b) ↔ StrictMonoOn f (Ici b)
Tactic:
exact strict_mono_on_dual_iff.symm
Proof state after:
no goals
Theorem: exercise6_6
Proof state before:
α : Type u_1
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
⊢ ¬DifferentiableAt ℝ (fun x => |x|) 0
Tactic:
intro h
Proof state after:
α : Type u_1
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
h : DifferentiableAt ℝ (fun x => |x|) 0
⊢ False
Theorem: exercise6_6
Proof state before:
α : Type u_1
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
h : DifferentiableAt ℝ (fun x => |x|) 0
⊢ False
Tactic:
have h1 : HasDerivWithinAt (fun x : ℝ ↦ |x|) 1 (Ici 0) 0
Proof state after:
case h1
α : Type u_1
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
h : DifferentiableAt ℝ (fun x => |x|) 0
⊢ HasDerivWithinAt (fun x => |x|) 1 (Ici 0) 0

α : Type u_1
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
h : DifferentiableAt ℝ (fun x => |x|) 0
h1 : HasDerivWithinAt (fun x => |x|) 1 (Ici 0) 0
⊢ False
Theorem: exercise6_6
Proof state before:
α : Type u_1
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
h : DifferentiableAt ℝ (fun x => |x|) 0
h1 : HasDerivWithinAt (fun x => |x|) 1 (Ici 0) 0
⊢ False
Tactic:
have h2 : HasDerivWithinAt (fun x : ℝ ↦ |x|) (-1) (Iic 0) 0
Proof state after:
case h2
α : Type u_1
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
h : DifferentiableAt ℝ (fun x => |x|) 0
h1 : HasDerivWithinAt (fun x => |x|) 1 (Ici 0) 0
⊢ HasDerivWithinAt (fun x => |x|) (-1) (Iic 0) 0

α : Type u_1
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
h : DifferentiableAt ℝ (fun x => |x|) 0
h1 : HasDerivWithinAt (fun x => |x|) 1 (Ici 0) 0
h2 : HasDerivWithinAt (fun x => |x|) (-1) (Iic 0) 0
⊢ False
Theorem: exercise6_6
Proof state before:
α : Type u_1
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
h : DifferentiableAt ℝ (fun x => |x|) 0
h1 : HasDerivWithinAt (fun x => |x|) 1 (Ici 0) 0
h2 : HasDerivWithinAt (fun x => |x|) (-1) (Iic 0) 0
⊢ False
Tactic:
have h3 : UniqueDiffWithinAt ℝ (Ici (0 : ℝ)) 0 := by
  sorry
Proof state after:
α : Type u_1
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
h : DifferentiableAt ℝ (fun x => |x|) 0
h1 : HasDerivWithinAt (fun x => |x|) 1 (Ici 0) 0
h2 : HasDerivWithinAt (fun x => |x|) (-1) (Iic 0) 0
h3 : UniqueDiffWithinAt ℝ (Ici 0) 0
⊢ False
Theorem: exercise6_6
Proof state before:
α : Type u_1
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
h : DifferentiableAt ℝ (fun x => |x|) 0
h1 : HasDerivWithinAt (fun x => |x|) 1 (Ici 0) 0
h2 : HasDerivWithinAt (fun x => |x|) (-1) (Iic 0) 0
h3 : UniqueDiffWithinAt ℝ (Ici 0) 0
⊢ False
Tactic:
have h4 : UniqueDiffWithinAt ℝ (Iic (0 : ℝ)) 0 := by
  sorry
Proof state after:
α : Type u_1
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
h : DifferentiableAt ℝ (fun x => |x|) 0
h1 : HasDerivWithinAt (fun x => |x|) 1 (Ici 0) 0
h2 : HasDerivWithinAt (fun x => |x|) (-1) (Iic 0) 0
h3 : UniqueDiffWithinAt ℝ (Ici 0) 0
h4 : UniqueDiffWithinAt ℝ (Iic 0) 0
⊢ False
Theorem: exercise6_6
Proof state before:
α : Type u_1
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
h : DifferentiableAt ℝ (fun x => |x|) 0
h1 : HasDerivWithinAt (fun x => |x|) 1 (Ici 0) 0
h2 : HasDerivWithinAt (fun x => |x|) (-1) (Iic 0) 0
h3 : UniqueDiffWithinAt ℝ (Ici 0) 0
h4 : UniqueDiffWithinAt ℝ (Iic 0) 0
⊢ False
Tactic:
sorry
Proof state after:
no goals
Theorem: exercise6_6
Proof state before:
case h1
α : Type u_1
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
h : DifferentiableAt ℝ (fun x => |x|) 0
⊢ HasDerivWithinAt (fun x => |x|) 1 (Ici 0) 0
Tactic:
sorry
Proof state after:
no goals
Theorem: exercise6_6
Proof state before:
case h2
α : Type u_1
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
h : DifferentiableAt ℝ (fun x => |x|) 0
h1 : HasDerivWithinAt (fun x => |x|) 1 (Ici 0) 0
⊢ HasDerivWithinAt (fun x => |x|) (-1) (Iic 0) 0
Tactic:
sorry
Proof state after:
no goals
Theorem: exercise6_6
Proof state before:
α : Type u_1
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
h : DifferentiableAt ℝ (fun x => |x|) 0
h1 : HasDerivWithinAt (fun x => |x|) 1 (Ici 0) 0
h2 : HasDerivWithinAt (fun x => |x|) (-1) (Iic 0) 0
⊢ UniqueDiffWithinAt ℝ (Ici 0) 0
Tactic:
sorry
Proof state after:
no goals
Theorem: exercise6_6
Proof state before:
α : Type u_1
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
h : DifferentiableAt ℝ (fun x => |x|) 0
h1 : HasDerivWithinAt (fun x => |x|) 1 (Ici 0) 0
h2 : HasDerivWithinAt (fun x => |x|) (-1) (Iic 0) 0
h3 : UniqueDiffWithinAt ℝ (Ici 0) 0
⊢ UniqueDiffWithinAt ℝ (Iic 0) 0
Tactic:
sorry
Proof state after:
no goals
Theorem: fac_pos
Proof state before:
n : ℕ
⊢ 0 < fac n
Tactic:
induction n
Proof state after:
case zero

⊢ 0 < fac 0

case succ
n✝ : ℕ
a✝ : 0 < fac n✝
⊢ 0 < fac (n✝ + 1)
Theorem: fac_pos
Proof state before:
⊢ 0 < fac 0
Tactic:
case zero =>
  rw [fac]
  norm_num
Proof state after:
no goals
Theorem: fac_pos
Proof state before:
k : ℕ
ih : 0 < fac k
⊢ 0 < fac (k + 1)
Tactic:
case succ k ih =>
  rw [fac]
  positivity
Proof state after:
no goals
Theorem: fac_pos
Proof state before:
⊢ 0 < fac 0
Tactic:
rw [fac]
Proof state after:
⊢ 0 < 1
Theorem: fac_pos
Proof state before:
⊢ 0 < 1
Tactic:
norm_num
Proof state after:
no goals
Theorem: fac_pos
Proof state before:
k : ℕ
ih : 0 < fac k
⊢ 0 < fac (k + 1)
Tactic:
rw [fac]
Proof state after:
k : ℕ
ih : 0 < fac k
⊢ 0 < (k + 1) * fac k
Theorem: fac_pos
Proof state before:
k : ℕ
ih : 0 < fac k
⊢ 0 < (k + 1) * fac k
Tactic:
positivity
Proof state after:
no goals
Theorem: pow_two_le_fac
Proof state before:
n : ℕ
⊢ 2 ^ n ≤ fac (n + 1)
Tactic:
induction n
Proof state after:
case zero

⊢ 2 ^ 0 ≤ fac (0 + 1)

case succ
n✝ : ℕ
a✝ : 2 ^ n✝ ≤ fac (n✝ + 1)
⊢ 2 ^ (n✝ + 1) ≤ fac (n✝ + 1 + 1)
Theorem: pow_two_le_fac
Proof state before:
⊢ 2 ^ 0 ≤ fac (0 + 1)
Tactic:
case zero =>
  norm_num
Proof state after:
no goals
Theorem: pow_two_le_fac
Proof state before:
k : ℕ
ih : 2 ^ k ≤ fac (k + 1)
⊢ 2 ^ (k + 1) ≤ fac (k + 1 + 1)
Tactic:
case succ k ih =>
  rw [fac, pow_add, mul_comm]
  gcongr
  linarith
Proof state after:
no goals
Theorem: pow_two_le_fac
Proof state before:
⊢ 2 ^ 0 ≤ fac (0 + 1)
Tactic:
norm_num
Proof state after:
no goals
Theorem: pow_two_le_fac
Proof state before:
k : ℕ
ih : 2 ^ k ≤ fac (k + 1)
⊢ 2 ^ (k + 1) ≤ fac (k + 1 + 1)
Tactic:
rw [fac, pow_add, mul_comm]
Proof state after:
k : ℕ
ih : 2 ^ k ≤ fac (k + 1)
⊢ 2 ^ 1 * 2 ^ k ≤ (k + 1 + 1) * fac (k + 1)
Theorem: pow_two_le_fac
Proof state before:
k : ℕ
ih : 2 ^ k ≤ fac (k + 1)
⊢ 2 ^ 1 * 2 ^ k ≤ (k + 1 + 1) * fac (k + 1)
Tactic:
gcongr
Proof state after:
case h₁
k : ℕ
ih : 2 ^ k ≤ fac (k + 1)
⊢ 2 ^ 1 ≤ k + 1 + 1
Theorem: pow_two_le_fac
Proof state before:
case h₁
k : ℕ
ih : 2 ^ k ≤ fac (k + 1)
⊢ 2 ^ 1 ≤ k + 1 + 1
Tactic:
linarith
Proof state after:
no goals
Theorem: sum_id
Proof state before:
n : ℕ
⊢ ∑ i in Finset.range (n + 1), i = n * (n + 1) / 2
Tactic:
symm
Proof state after:
n : ℕ
⊢ n * (n + 1) / 2 = ∑ i in Finset.range (n + 1), i
Theorem: sum_id
Proof state before:
n : ℕ
⊢ n * (n + 1) / 2 = ∑ i in Finset.range (n + 1), i
Tactic:
rw [Nat.div_eq_of_eq_mul_left]
Proof state after:
case H1
n : ℕ
⊢ 0 < 2

case H2
n : ℕ
⊢ n * (n + 1) = (∑ i in Finset.range (n + 1), i) * 2
Theorem: sum_id
Proof state before:
case H1
n : ℕ
⊢ 0 < 2

case H2
n : ℕ
⊢ n * (n + 1) = (∑ i in Finset.range (n + 1), i) * 2
Tactic:
norm_num
Proof state after:
case H2
n : ℕ
⊢ n * (n + 1) = (∑ i in Finset.range (n + 1), i) * 2
Theorem: sum_id
Proof state before:
case H2
n : ℕ
⊢ n * (n + 1) = (∑ i in Finset.range (n + 1), i) * 2
Tactic:
symm
Proof state after:
case H2
n : ℕ
⊢ (∑ i in Finset.range (n + 1), i) * 2 = n * (n + 1)
Theorem: sum_id
Proof state before:
case H2
n : ℕ
⊢ (∑ i in Finset.range (n + 1), i) * 2 = n * (n + 1)
Tactic:
induction n
Proof state after:
case H2.zero

⊢ (∑ i in Finset.range (0 + 1), i) * 2 = 0 * (0 + 1)

case H2.succ
n✝ : ℕ
a✝ : (∑ i in Finset.range (n✝ + 1), i) * 2 = n✝ * (n✝ + 1)
⊢ (∑ i in Finset.range (n✝ + 1 + 1), i) * 2 = (n✝ + 1) * (n✝ + 1 + 1)
Theorem: sum_id
Proof state before:
⊢ (∑ i in Finset.range (0 + 1), i) * 2 = 0 * (0 + 1)
Tactic:
case zero => simp
Proof state after:
no goals
Theorem: sum_id
Proof state before:
k : ℕ
ih : (∑ i in Finset.range (k + 1), i) * 2 = k * (k + 1)
⊢ (∑ i in Finset.range (k + 1 + 1), i) * 2 = (k + 1) * (k + 1 + 1)
Tactic:
case succ k ih =>
  rw [sum_range_succ, add_mul, ih]
  ring
Proof state after:
no goals
Theorem: sum_id
Proof state before:
⊢ (∑ i in Finset.range (0 + 1), i) * 2 = 0 * (0 + 1)
Tactic:
simp
Proof state after:
no goals
Theorem: sum_id
Proof state before:
k : ℕ
ih : (∑ i in Finset.range (k + 1), i) * 2 = k * (k + 1)
⊢ (∑ i in Finset.range (k + 1 + 1), i) * 2 = (k + 1) * (k + 1 + 1)
Tactic:
rw [sum_range_succ, add_mul, ih]
Proof state after:
k : ℕ
ih : (∑ i in Finset.range (k + 1), i) * 2 = k * (k + 1)
⊢ k * (k + 1) + (k + 1) * 2 = (k + 1) * (k + 1 + 1)
Theorem: sum_id
Proof state before:
k : ℕ
ih : (∑ i in Finset.range (k + 1), i) * 2 = k * (k + 1)
⊢ k * (k + 1) + (k + 1) * 2 = (k + 1) * (k + 1 + 1)
Tactic:
ring
Proof state after:
no goals
Theorem: ϕ_sub_ψ_ne_zero
Proof state before:
n : ℕ
⊢ ϕ - ψ ≠ 0
Tactic:
simp [ϕ, ψ, sub_eq_zero]
Proof state after:
n : ℕ
⊢ ¬1 + sqrt 5 = 1 - sqrt 5
Theorem: ϕ_sub_ψ_ne_zero
Proof state before:
n : ℕ
⊢ ¬1 + sqrt 5 = 1 - sqrt 5
Tactic:
simp [sub_eq_add_neg]
Proof state after:
n : ℕ
⊢ 0 < 5
Theorem: ϕ_sub_ψ_ne_zero
Proof state before:
n : ℕ
⊢ 0 < 5
Tactic:
norm_num
Proof state after:
no goals
Theorem: ϕ_sq
Proof state before:
n : ℕ
⊢ ϕ ^ 2 = ϕ + 1
Tactic:
simp [ϕ, add_sq]
Proof state after:
n : ℕ
⊢ (1 + 2 * sqrt 5 + sqrt 5 ^ 2) / 2 ^ 2 = (1 + sqrt 5) / 2 + 1
Theorem: ϕ_sq
Proof state before:
n : ℕ
⊢ (1 + 2 * sqrt 5 + sqrt 5 ^ 2) / 2 ^ 2 = (1 + sqrt 5) / 2 + 1
Tactic:
field_simp
Proof state after:
n : ℕ
⊢ (1 + 2 * sqrt 5 + 5) * 2 = (1 + sqrt 5 + 2) * 2 ^ 2
Theorem: ϕ_sq
Proof state before:
n : ℕ
⊢ (1 + 2 * sqrt 5 + 5) * 2 = (1 + sqrt 5 + 2) * 2 ^ 2
Tactic:
ring
Proof state after:
no goals
Theorem: ψ_sq
Proof state before:
n : ℕ
⊢ ψ ^ 2 = ψ + 1
Tactic:
simp [ψ, sub_sq]
Proof state after:
n : ℕ
⊢ (1 - 2 * sqrt 5 + sqrt 5 ^ 2) / 2 ^ 2 = (1 - sqrt 5) / 2 + 1
Theorem: ψ_sq
Proof state before:
n : ℕ
⊢ (1 - 2 * sqrt 5 + sqrt 5 ^ 2) / 2 ^ 2 = (1 - sqrt 5) / 2 + 1
Tactic:
field_simp
Proof state after:
n : ℕ
⊢ (1 - 2 * sqrt 5 + 5) * 2 = (1 - sqrt 5 + 2) * 2 ^ 2
Theorem: ψ_sq
Proof state before:
n : ℕ
⊢ (1 - 2 * sqrt 5 + 5) * 2 = (1 - sqrt 5 + 2) * 2 ^ 2
Tactic:
ring
Proof state after:
no goals
Theorem: coe_fib_eq
Proof state before:
n✝ n : ℕ
⊢ ↑(fib n) = (ϕ ^ n - ψ ^ n) / (ϕ - ψ)
Tactic:
induction n using Nat.two_step_induction
Proof state after:
case zero
n : ℕ
⊢ ↑(fib 0) = (ϕ ^ 0 - ψ ^ 0) / (ϕ - ψ)

case one
n : ℕ
⊢ ↑(fib 1) = (ϕ ^ 1 - ψ ^ 1) / (ϕ - ψ)

case step
n k✝ : ℕ
IH0✝ : ↑(fib k✝) = (ϕ ^ k✝ - ψ ^ k✝) / (ϕ - ψ)
IH1✝ : ↑(fib (k✝ + 1)) = (ϕ ^ (k✝ + 1) - ψ ^ (k✝ + 1)) / (ϕ - ψ)
⊢ ↑(fib (k✝ + 2)) = (ϕ ^ (k✝ + 2) - ψ ^ (k✝ + 2)) / (ϕ - ψ)
Theorem: coe_fib_eq
Proof state before:
n : ℕ
⊢ ↑(fib 0) = (ϕ ^ 0 - ψ ^ 0) / (ϕ - ψ)
Tactic:
case zero => simp
Proof state after:
no goals
Theorem: coe_fib_eq
Proof state before:
n : ℕ
⊢ ↑(fib 1) = (ϕ ^ 1 - ψ ^ 1) / (ϕ - ψ)
Tactic:
case one => simp
Proof state after:
no goals
Theorem: coe_fib_eq
Proof state before:
n k : ℕ
ih1 : ↑(fib k) = (ϕ ^ k - ψ ^ k) / (ϕ - ψ)
ih2 : ↑(fib (k + 1)) = (ϕ ^ (k + 1) - ψ ^ (k + 1)) / (ϕ - ψ)
⊢ ↑(fib (k + 2)) = (ϕ ^ (k + 2) - ψ ^ (k + 2)) / (ϕ - ψ)
Tactic:
case step k ih1 ih2 =>
  simp [fib, ih1, ih2]
  field_simp
  simp [pow_add]
  ring
Proof state after:
no goals
Theorem: coe_fib_eq
Proof state before:
n : ℕ
⊢ ↑(fib 0) = (ϕ ^ 0 - ψ ^ 0) / (ϕ - ψ)
Tactic:
simp
Proof state after:
no goals
Theorem: coe_fib_eq
Proof state before:
n : ℕ
⊢ ↑(fib 1) = (ϕ ^ 1 - ψ ^ 1) / (ϕ - ψ)
Tactic:
simp
Proof state after:
no goals
Theorem: coe_fib_eq
Proof state before:
n k : ℕ
ih1 : ↑(fib k) = (ϕ ^ k - ψ ^ k) / (ϕ - ψ)
ih2 : ↑(fib (k + 1)) = (ϕ ^ (k + 1) - ψ ^ (k + 1)) / (ϕ - ψ)
⊢ ↑(fib (k + 2)) = (ϕ ^ (k + 2) - ψ ^ (k + 2)) / (ϕ - ψ)
Tactic:
simp [fib, ih1, ih2]
Proof state after:
n k : ℕ
ih1 : ↑(fib k) = (ϕ ^ k - ψ ^ k) / (ϕ - ψ)
ih2 : ↑(fib (k + 1)) = (ϕ ^ (k + 1) - ψ ^ (k + 1)) / (ϕ - ψ)
⊢ (ϕ ^ (k + 1) - ψ ^ (k + 1)) / (ϕ - ψ) + (ϕ ^ k - ψ ^ k) / (ϕ - ψ) = (ϕ ^ (k + 2) - ψ ^ (k + 2)) / (ϕ - ψ)
Theorem: coe_fib_eq
Proof state before:
n k : ℕ
ih1 : ↑(fib k) = (ϕ ^ k - ψ ^ k) / (ϕ - ψ)
ih2 : ↑(fib (k + 1)) = (ϕ ^ (k + 1) - ψ ^ (k + 1)) / (ϕ - ψ)
⊢ (ϕ ^ (k + 1) - ψ ^ (k + 1)) / (ϕ - ψ) + (ϕ ^ k - ψ ^ k) / (ϕ - ψ) = (ϕ ^ (k + 2) - ψ ^ (k + 2)) / (ϕ - ψ)
Tactic:
field_simp
Proof state after:
n k : ℕ
ih1 : ↑(fib k) = (ϕ ^ k - ψ ^ k) / (ϕ - ψ)
ih2 : ↑(fib (k + 1)) = (ϕ ^ (k + 1) - ψ ^ (k + 1)) / (ϕ - ψ)
⊢ ϕ ^ (k + 1) - ψ ^ (k + 1) + (ϕ ^ k - ψ ^ k) = ϕ ^ (k + 2) - ψ ^ (k + 2)
Theorem: coe_fib_eq
Proof state before:
n k : ℕ
ih1 : ↑(fib k) = (ϕ ^ k - ψ ^ k) / (ϕ - ψ)
ih2 : ↑(fib (k + 1)) = (ϕ ^ (k + 1) - ψ ^ (k + 1)) / (ϕ - ψ)
⊢ ϕ ^ (k + 1) - ψ ^ (k + 1) + (ϕ ^ k - ψ ^ k) = ϕ ^ (k + 2) - ψ ^ (k + 2)
Tactic:
simp [pow_add]
Proof state after:
n k : ℕ
ih1 : ↑(fib k) = (ϕ ^ k - ψ ^ k) / (ϕ - ψ)
ih2 : ↑(fib (k + 1)) = (ϕ ^ (k + 1) - ψ ^ (k + 1)) / (ϕ - ψ)
⊢ ϕ ^ k * ϕ - ψ ^ k * ψ + (ϕ ^ k - ψ ^ k) = ϕ ^ k * (ϕ + 1) - ψ ^ k * (ψ + 1)
Theorem: coe_fib_eq
Proof state before:
n k : ℕ
ih1 : ↑(fib k) = (ϕ ^ k - ψ ^ k) / (ϕ - ψ)
ih2 : ↑(fib (k + 1)) = (ϕ ^ (k + 1) - ψ ^ (k + 1)) / (ϕ - ψ)
⊢ ϕ ^ k * ϕ - ψ ^ k * ψ + (ϕ ^ k - ψ ^ k) = ϕ ^ k * (ϕ + 1) - ψ ^ k * (ψ + 1)
Tactic:
ring
Proof state after:
no goals
Theorem: fac_dvd_fac
Proof state before:
n✝ n m : ℕ
h : n ≤ m
⊢ fac n ∣ fac m
Tactic:
sorry
Proof state after:
no goals
Theorem: le_generateFrom_iff_subset_isOpen
Proof state before:
n : ℕ
α : Type u_1
t : TopologicalSpace α
g : Set (Set α)
h : g ⊆ {s | IsOpen s}
⊢ {s | IsOpen s} ⊆ {s | IsOpen s}
Tactic:
intro s hs
Proof state after:
n : ℕ
α : Type u_1
t : TopologicalSpace α
g : Set (Set α)
h : g ⊆ {s | IsOpen s}
s : Set α
hs : s ∈ {s | IsOpen s}
⊢ s ∈ {s | IsOpen s}
Theorem: le_generateFrom_iff_subset_isOpen
Proof state before:
n : ℕ
α : Type u_1
t : TopologicalSpace α
g : Set (Set α)
h : g ⊆ {s | IsOpen s}
s : Set α
hs : s ∈ {s | IsOpen s}
⊢ s ∈ {s | IsOpen s}
Tactic:
simp
Proof state after:
n : ℕ
α : Type u_1
t : TopologicalSpace α
g : Set (Set α)
h : g ⊆ {s | IsOpen s}
s : Set α
hs : s ∈ {s | IsOpen s}
⊢ IsOpen s
Theorem: le_generateFrom_iff_subset_isOpen
Proof state before:
n : ℕ
α : Type u_1
t : TopologicalSpace α
g : Set (Set α)
h : g ⊆ {s | IsOpen s}
s : Set α
hs : s ∈ {s | IsOpen s}
⊢ IsOpen s
Tactic:
simp at hs
Proof state after:
n : ℕ
α : Type u_1
t : TopologicalSpace α
g : Set (Set α)
h : g ⊆ {s | IsOpen s}
s : Set α
hs : IsOpen s
⊢ IsOpen s
Theorem: le_generateFrom_iff_subset_isOpen
Proof state before:
n : ℕ
α : Type u_1
t : TopologicalSpace α
g : Set (Set α)
h : g ⊆ {s | IsOpen s}
s : Set α
hs : IsOpen s
⊢ IsOpen s
Tactic:
induction hs
Proof state after:
case basic
n : ℕ
α : Type u_1
t : TopologicalSpace α
g : Set (Set α)
h : g ⊆ {s | IsOpen s}
s s✝ : Set α
a✝ : s✝ ∈ g
⊢ IsOpen s✝

case univ
n : ℕ
α : Type u_1
t : TopologicalSpace α
g : Set (Set α)
h : g ⊆ {s | IsOpen s}
s : Set α
⊢ IsOpen Set.univ

case inter
n : ℕ
α : Type u_1
t : TopologicalSpace α
g : Set (Set α)
h : g ⊆ {s | IsOpen s}
s s✝ t✝ : Set α
a✝¹ : GenerateOpen g s✝
a✝ : GenerateOpen g t✝
a_ih✝¹ : IsOpen s✝
a_ih✝ : IsOpen t✝
⊢ IsOpen (s✝ ∩ t✝)

case sUnion
n : ℕ
α : Type u_1
t : TopologicalSpace α
g : Set (Set α)
h : g ⊆ {s | IsOpen s}
s : Set α
S✝ : Set (Set α)
a✝ : ∀ s ∈ S✝, GenerateOpen g s
a_ih✝ : ∀ s ∈ S✝, IsOpen s
⊢ IsOpen (⋃₀ S✝)
Theorem: le_generateFrom_iff_subset_isOpen
Proof state before:
n : ℕ
α : Type u_1
t : TopologicalSpace α
g : Set (Set α)
h : g ⊆ {s | IsOpen s}
s✝ s : Set α
hs : s ∈ g
⊢ IsOpen s
Tactic:
case basic s hs =>
  apply h
  exact hs
Proof state after:
no goals
Theorem: le_generateFrom_iff_subset_isOpen
Proof state before:
n : ℕ
α : Type u_1
t : TopologicalSpace α
g : Set (Set α)
h : g ⊆ {s | IsOpen s}
s : Set α
⊢ IsOpen Set.univ
Tactic:
case univ =>
  simp
Proof state after:
no goals
Theorem: le_generateFrom_iff_subset_isOpen
Proof state before:
n : ℕ
α : Type u_1
t : TopologicalSpace α
g : Set (Set α)
h : g ⊆ {s | IsOpen s}
s✝ s s' : Set α
a✝¹ : GenerateOpen g s
a✝ : GenerateOpen g s'
ihs : IsOpen s
ihs' : IsOpen s'
⊢ IsOpen (s ∩ s')
Tactic:
case inter s s' _ _ ihs ihs' =>
  apply IsOpen.inter
  exact ihs
  exact ihs'
Proof state after:
no goals
Theorem: le_generateFrom_iff_subset_isOpen
Proof state before:
n : ℕ
α : Type u_1
t : TopologicalSpace α
g : Set (Set α)
h : g ⊆ {s | IsOpen s}
s : Set α
S : Set (Set α)
a✝ : ∀ s ∈ S, GenerateOpen g s
hS : ∀ s ∈ S, IsOpen s
⊢ IsOpen (⋃₀ S)
Tactic:
case sUnion S _ hS =>
  apply isOpen_sUnion
  exact hS
Proof state after:
no goals
Theorem: le_generateFrom_iff_subset_isOpen
Proof state before:
n : ℕ
α : Type u_1
t : TopologicalSpace α
g : Set (Set α)
h : g ⊆ {s | IsOpen s}
s✝ s : Set α
hs : s ∈ g
⊢ IsOpen s
Tactic:
apply h
Proof state after:
case a
n : ℕ
α : Type u_1
t : TopologicalSpace α
g : Set (Set α)
h : g ⊆ {s | IsOpen s}
s✝ s : Set α
hs : s ∈ g
⊢ s ∈ g
Theorem: le_generateFrom_iff_subset_isOpen
Proof state before:
case a
n : ℕ
α : Type u_1
t : TopologicalSpace α
g : Set (Set α)
h : g ⊆ {s | IsOpen s}
s✝ s : Set α
hs : s ∈ g
⊢ s ∈ g
Tactic:
exact hs
Proof state after:
no goals
Theorem: le_generateFrom_iff_subset_isOpen
Proof state before:
n : ℕ
α : Type u_1
t : TopologicalSpace α
g : Set (Set α)
h : g ⊆ {s | IsOpen s}
s : Set α
⊢ IsOpen Set.univ
Tactic:
simp
Proof state after:
no goals
Theorem: le_generateFrom_iff_subset_isOpen
Proof state before:
n : ℕ
α : Type u_1
t : TopologicalSpace α
g : Set (Set α)
h : g ⊆ {s | IsOpen s}
s✝ s s' : Set α
a✝¹ : GenerateOpen g s
a✝ : GenerateOpen g s'
ihs : IsOpen s
ihs' : IsOpen s'
⊢ IsOpen (s ∩ s')
Tactic:
apply IsOpen.inter
Proof state after:
case h₁
n : ℕ
α : Type u_1
t : TopologicalSpace α
g : Set (Set α)
h : g ⊆ {s | IsOpen s}
s✝ s s' : Set α
a✝¹ : GenerateOpen g s
a✝ : GenerateOpen g s'
ihs : IsOpen s
ihs' : IsOpen s'
⊢ IsOpen s

case h₂
n : ℕ
α : Type u_1
t : TopologicalSpace α
g : Set (Set α)
h : g ⊆ {s | IsOpen s}
s✝ s s' : Set α
a✝¹ : GenerateOpen g s
a✝ : GenerateOpen g s'
ihs : IsOpen s
ihs' : IsOpen s'
⊢ IsOpen s'
Theorem: le_generateFrom_iff_subset_isOpen
Proof state before:
case h₁
n : ℕ
α : Type u_1
t : TopologicalSpace α
g : Set (Set α)
h : g ⊆ {s | IsOpen s}
s✝ s s' : Set α
a✝¹ : GenerateOpen g s
a✝ : GenerateOpen g s'
ihs : IsOpen s
ihs' : IsOpen s'
⊢ IsOpen s

case h₂
n : ℕ
α : Type u_1
t : TopologicalSpace α
g : Set (Set α)
h : g ⊆ {s | IsOpen s}
s✝ s s' : Set α
a✝¹ : GenerateOpen g s
a✝ : GenerateOpen g s'
ihs : IsOpen s
ihs' : IsOpen s'
⊢ IsOpen s'
Tactic:
exact ihs
Proof state after:
case h₂
n : ℕ
α : Type u_1
t : TopologicalSpace α
g : Set (Set α)
h : g ⊆ {s | IsOpen s}
s✝ s s' : Set α
a✝¹ : GenerateOpen g s
a✝ : GenerateOpen g s'
ihs : IsOpen s
ihs' : IsOpen s'
⊢ IsOpen s'