FormalConjectures.OEIS.«4290»

/-
Copyright 2026 The Formal Conjectures Authors.

Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at

    https://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/

import FormalConjecturesUtil

Least positive multiple of $n$ in base 10 with digits 0 and 1

Least positive multiple of $n$ that when written in base 10 uses only 0's and 1's.

References:

A004290

namespace OeisA4290

Least positive multiple of $n$ using only 0's and 1's in base 10.

noncomputable def a (n : ℕ) : ℕ :=
  sInf { m : ℕ | 0 < m ∧ n ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1 }



@[category test, AMS 11]
theorem a_0 : a 0 = 0 := by⊢ a 0 = 0
  dsimp [a]⊢ sInf {m | 0 < m ∧ 0 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 0
  have h_empty : { m : ℕ | 0 < m ∧ 0 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1 } = ∅ := by⊢ a 0 = 0h_empty:{m | 0 < m ∧ 0 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = ∅⊢ sInf {m | 0 < m ∧ 0 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 0
    ext mm:ℕ⊢ m ∈ {m | 0 < m ∧ 0 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} ↔ m ∈ ∅h_empty:{m | 0 < m ∧ 0 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = ∅⊢ sInf {m | 0 < m ∧ 0 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 0
    simp only [Set.mem_ofPred_eq, Set.mem_empty_iff_false, iff_false, not_and]m:ℕ⊢ 0 < m → 0 ∣ m → ¬∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1h_empty:{m | 0 < m ∧ 0 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = ∅⊢ sInf {m | 0 < m ∧ 0 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 0
    intro hm h0dvdm:ℕhm:0 < mh0dvd:0 ∣ m⊢ ¬∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1h_empty:{m | 0 < m ∧ 0 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = ∅⊢ sInf {m | 0 < m ∧ 0 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 0
    have hm0 : m = 0 := Nat.eq_zero_of_zero_dvd h0dvdm:ℕhm:0 < mh0dvd:0 ∣ mhm0:m = 0⊢ ¬∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1h_empty:{m | 0 < m ∧ 0 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = ∅⊢ sInf {m | 0 < m ∧ 0 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 0
    omegah_empty:{m | 0 < m ∧ 0 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = ∅⊢ sInf {m | 0 < m ∧ 0 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 0h_empty:{m | 0 < m ∧ 0 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = ∅⊢ sInf {m | 0 < m ∧ 0 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 0
  rw [h_empty,h_empty:{m | 0 < m ∧ 0 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = ∅⊢ sInf ∅ = 0All goals completed! 🐙 Nat.sInf_emptyh_empty:{m | 0 < m ∧ 0 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = ∅⊢ 0 = 0All goals completed! 🐙]All goals completed! 🐙



@[category test, AMS 11]
theorem a_1 : a 1 = 1 := by⊢ a 1 = 1
  dsimp [a]⊢ sInf {m | 0 < m ∧ 1 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 1
  have h_least : IsLeast { m : ℕ | 0 < m ∧ 1 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1 } 1 := by⊢ a 1 = 1h_least:IsLeast {m | 0 < m ∧ 1 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 1⊢ sInf {m | 0 < m ∧ 1 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 1
    refine ⟨⟨by⊢ 0 < 1h_least:IsLeast {m | 0 < m ∧ 1 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 1⊢ sInf {m | 0 < m ∧ 1 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 1 decideAll goals completed! 🐙h_least:IsLeast {m | 0 < m ∧ 1 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 1⊢ sInf {m | 0 < m ∧ 1 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 1, dvd_rfl, ?_⟩, fun m hm ↦ hm.1⟩
    intro d hdd:ℕhd:d ∈ Nat.digits 10 1⊢ d = 0 ∨ d = 1h_least:IsLeast {m | 0 < m ∧ 1 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 1⊢ sInf {m | 0 < m ∧ 1 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 1
    rw [Nat.digits_def' (byd:ℕhd:d ∈ Nat.digits 10 1⊢ 1 < 10d:ℕhd:d ∈ [1 % 10]⊢ d = 0 ∨ d = 1h_least:IsLeast {m | 0 < m ∧ 1 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 1⊢ sInf {m | 0 < m ∧ 1 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 1 decideAll goals completed! 🐙d:ℕhd:d ∈ [1 % 10]⊢ d = 0 ∨ d = 1h_least:IsLeast {m | 0 < m ∧ 1 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 1⊢ sInf {m | 0 < m ∧ 1 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 1) (byd:ℕhd:d ∈ Nat.digits 10 1⊢ 0 < 1d:ℕhd:d ∈ [1 % 10]⊢ d = 0 ∨ d = 1h_least:IsLeast {m | 0 < m ∧ 1 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 1⊢ sInf {m | 0 < m ∧ 1 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 1 decideAll goals completed! 🐙d:ℕhd:d ∈ [1 % 10]⊢ d = 0 ∨ d = 1h_least:IsLeast {m | 0 < m ∧ 1 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 1⊢ sInf {m | 0 < m ∧ 1 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 1), show (1 / 10 : ℕ) = 0 by⊢ a 1 = 1d:ℕhd:d ∈ [1 % 10]⊢ d = 0 ∨ d = 1h_least:IsLeast {m | 0 < m ∧ 1 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 1⊢ sInf {m | 0 < m ∧ 1 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 1 rflAll goals completed! 🐙d:ℕhd:d ∈ [1 % 10]⊢ d = 0 ∨ d = 1h_least:IsLeast {m | 0 < m ∧ 1 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 1⊢ sInf {m | 0 < m ∧ 1 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 1,
      Nat.digits_zerod:ℕhd:d ∈ [1 % 10]⊢ d = 0 ∨ d = 1d:ℕhd:d ∈ [1 % 10]⊢ d = 0 ∨ d = 1h_least:IsLeast {m | 0 < m ∧ 1 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 1⊢ sInf {m | 0 < m ∧ 1 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 1] at hdd:ℕhd:d ∈ [1 % 10]⊢ d = 0 ∨ d = 1h_least:IsLeast {m | 0 < m ∧ 1 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 1⊢ sInf {m | 0 < m ∧ 1 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 1
    simp only [show 1 % 10 = 1 by rfl, List.mem_singleton] at hdd:ℕhd:d = 1⊢ d = 0 ∨ d = 1h_least:IsLeast {m | 0 < m ∧ 1 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 1⊢ sInf {m | 0 < m ∧ 1 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 1
    subst hd⊢ 1 = 0 ∨ 1 = 1h_least:IsLeast {m | 0 < m ∧ 1 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 1⊢ sInf {m | 0 < m ∧ 1 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 1
    exact Or.inr rflh_least:IsLeast {m | 0 < m ∧ 1 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 1⊢ sInf {m | 0 < m ∧ 1 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 1h_least:IsLeast {m | 0 < m ∧ 1 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 1⊢ sInf {m | 0 < m ∧ 1 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 1
  exact h_least.csInf_eqAll goals completed! 🐙



@[category test, AMS 11]
theorem a_2 : a 2 = 10 := by⊢ a 2 = 10
  dsimp [a]⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10
  have h_least : IsLeast { m : ℕ | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1 } 10 := by⊢ a 2 = 10h_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10
    refine ⟨⟨by⊢ 0 < 10h_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10 decideAll goals completed! 🐙h_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10, by⊢ 2 ∣ 10h_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10 decideAll goals completed! 🐙h_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10, ?_⟩, ?_⟩
    ·refine_1⊢ ∀ d ∈ Nat.digits 10 10, d = 0 ∨ d = 1h_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10 intro d hdrefine_1d:ℕhd:d ∈ Nat.digits 10 10⊢ d = 0 ∨ d = 1h_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10
      have h10 : (10 : ℕ) = 10 ^ 1 * 1 := by⊢ a 2 = 10refine_1d:ℕhd:d ∈ Nat.digits 10 10h10:10 = 10 ^ 1 * 1⊢ d = 0 ∨ d = 1h_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10 rflrefine_1d:ℕhd:d ∈ Nat.digits 10 10h10:10 = 10 ^ 1 * 1⊢ d = 0 ∨ d = 1h_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10refine_1d:ℕhd:d ∈ Nat.digits 10 10h10:10 = 10 ^ 1 * 1⊢ d = 0 ∨ d = 1h_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10
      nth_rw 2 [h10refine_1d:ℕhd:d ∈ Nat.digits 10 (10 ^ 1 * 1)h10:10 = 10 ^ 1 * 1⊢ d = 0 ∨ d = 1h_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10]refine_1d:ℕhd:d ∈ Nat.digits 10 (10 ^ 1 * 1)h10:10 = 10 ^ 1 * 1⊢ d = 0 ∨ d = 1h_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10 at hd
      rw [Nat.digits_base_pow_mul (b := 10) (k := 1) (m := 1) (byd:ℕhd:d ∈ Nat.digits 10 (10 ^ 1 * 1)h10:10 = 10 ^ 1 * 1⊢ 1 < 10refine_1d:ℕhd:d ∈ List.replicate 1 0 ++ [1]h10:10 = 10 ^ 1 * 1⊢ d = 0 ∨ d = 1h_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10 decideAll goals completed! 🐙refine_1d:ℕhd:d ∈ List.replicate 1 0 ++ [1]h10:10 = 10 ^ 1 * 1⊢ d = 0 ∨ d = 1h_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10) (byd:ℕhd:d ∈ Nat.digits 10 (10 ^ 1 * 1)h10:10 = 10 ^ 1 * 1⊢ 0 < 1refine_1d:ℕhd:d ∈ List.replicate 1 0 ++ [1]h10:10 = 10 ^ 1 * 1⊢ d = 0 ∨ d = 1h_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10 decideAll goals completed! 🐙refine_1d:ℕhd:d ∈ List.replicate 1 0 ++ [1]h10:10 = 10 ^ 1 * 1⊢ d = 0 ∨ d = 1h_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10),
          Nat.digits_of_lt 10 1 (byd:ℕhd:d ∈ List.replicate 1 0 ++ Nat.digits 10 1h10:10 = 10 ^ 1 * 1⊢ 1 ≠ 0refine_1d:ℕhd:d ∈ List.replicate 1 0 ++ [1]h10:10 = 10 ^ 1 * 1⊢ d = 0 ∨ d = 1h_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10 decideAll goals completed! 🐙refine_1d:ℕhd:d ∈ List.replicate 1 0 ++ [1]h10:10 = 10 ^ 1 * 1⊢ d = 0 ∨ d = 1h_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10) (byd:ℕhd:d ∈ List.replicate 1 0 ++ Nat.digits 10 1h10:10 = 10 ^ 1 * 1⊢ 1 < 10refine_1d:ℕhd:d ∈ List.replicate 1 0 ++ [1]h10:10 = 10 ^ 1 * 1⊢ d = 0 ∨ d = 1h_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10 decideAll goals completed! 🐙refine_1d:ℕhd:d ∈ List.replicate 1 0 ++ [1]h10:10 = 10 ^ 1 * 1⊢ d = 0 ∨ d = 1h_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10)] at hdrefine_1d:ℕhd:d ∈ List.replicate 1 0 ++ [1]h10:10 = 10 ^ 1 * 1⊢ d = 0 ∨ d = 1h_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10
      simp only [List.replicate_one, List.singleton_append, List.mem_cons,
        List.not_mem_nil, or_false] at hdrefine_1d:ℕh10:10 = 10 ^ 1 * 1hd:d = 0 ∨ d = 1⊢ d = 0 ∨ d = 1h_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10
      exact hdAll goals completed! 🐙h_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10
    ·refine_2⊢ 10 ∈ lowerBounds {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}h_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10 intro m hmrefine_2m:ℕhm:m ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}⊢ 10 ≤ mh_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10
      by_contra! hltrefine_2m:ℕhm:m ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:m < 10⊢ Falseh_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10
      have hm_pos : 0 < m := hm.1refine_2m:ℕhm:m ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:m < 10hm_pos:0 < m⊢ Falseh_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10
      have h2dvd : 2 ∣ m := hm.2.1refine_2m:ℕhm:m ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:m < 10hm_pos:0 < mh2dvd:2 ∣ m⊢ Falseh_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10
      have hd : ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1 := hm.2.2refine_2m:ℕhm:m ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:m < 10hm_pos:0 < mh2dvd:2 ∣ mhd:∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1⊢ Falseh_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10
      interval_cases mrefine_2.«1»m:ℕhm:1 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:1 < 10hm_pos:0 < 1h2dvd:2 ∣ 1hd:∀ d ∈ Nat.digits 10 1, d = 0 ∨ d = 1⊢ Falserefine_2.«2»m:ℕhm:2 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:2 < 10hm_pos:0 < 2h2dvd:2 ∣ 2hd:∀ d ∈ Nat.digits 10 2, d = 0 ∨ d = 1⊢ Falserefine_2.«3»m:ℕhm:3 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:3 < 10hm_pos:0 < 3h2dvd:2 ∣ 3hd:∀ d ∈ Nat.digits 10 3, d = 0 ∨ d = 1⊢ Falserefine_2.«4»m:ℕhm:4 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:4 < 10hm_pos:0 < 4h2dvd:2 ∣ 4hd:∀ d ∈ Nat.digits 10 4, d = 0 ∨ d = 1⊢ Falserefine_2.«5»m:ℕhm:5 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:5 < 10hm_pos:0 < 5h2dvd:2 ∣ 5hd:∀ d ∈ Nat.digits 10 5, d = 0 ∨ d = 1⊢ Falserefine_2.«6»m:ℕhm:6 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:6 < 10hm_pos:0 < 6h2dvd:2 ∣ 6hd:∀ d ∈ Nat.digits 10 6, d = 0 ∨ d = 1⊢ Falserefine_2.«7»m:ℕhm:7 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:7 < 10hm_pos:0 < 7h2dvd:2 ∣ 7hd:∀ d ∈ Nat.digits 10 7, d = 0 ∨ d = 1⊢ Falserefine_2.«8»m:ℕhm:8 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:8 < 10hm_pos:0 < 8h2dvd:2 ∣ 8hd:∀ d ∈ Nat.digits 10 8, d = 0 ∨ d = 1⊢ Falserefine_2.«9»m:ℕhm:9 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:9 < 10hm_pos:0 < 9h2dvd:2 ∣ 9hd:∀ d ∈ Nat.digits 10 9, d = 0 ∨ d = 1⊢ Falseh_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10
      ·refine_2.«1»m:ℕhm:1 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:1 < 10hm_pos:0 < 1h2dvd:2 ∣ 1hd:∀ d ∈ Nat.digits 10 1, d = 0 ∨ d = 1⊢ Falseh_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10 revert h2dvdrefine_2.«1»m:ℕhm:1 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:1 < 10hm_pos:0 < 1hd:∀ d ∈ Nat.digits 10 1, d = 0 ∨ d = 1⊢ 2 ∣ 1 → Falseh_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10; decideAll goals completed! 🐙h_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10
      ·refine_2.«2»m:ℕhm:2 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:2 < 10hm_pos:0 < 2h2dvd:2 ∣ 2hd:∀ d ∈ Nat.digits 10 2, d = 0 ∨ d = 1⊢ Falseh_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10 have hm_d : Nat.digits 10 2 = [2] := Nat.digits_of_lt 10 2 (bym:ℕhm:2 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:2 < 10hm_pos:0 < 2h2dvd:2 ∣ 2hd:∀ d ∈ Nat.digits 10 2, d = 0 ∨ d = 1⊢ 2 ≠ 0refine_2.«2»m:ℕhm:2 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:2 < 10hm_pos:0 < 2h2dvd:2 ∣ 2hd:∀ d ∈ Nat.digits 10 2, d = 0 ∨ d = 1hm_d:Nat.digits 10 2 = [2]⊢ Falseh_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10 decideAll goals completed! 🐙refine_2.«2»m:ℕhm:2 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:2 < 10hm_pos:0 < 2h2dvd:2 ∣ 2hd:∀ d ∈ Nat.digits 10 2, d = 0 ∨ d = 1hm_d:Nat.digits 10 2 = [2]⊢ Falseh_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10) (bym:ℕhm:2 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:2 < 10hm_pos:0 < 2h2dvd:2 ∣ 2hd:∀ d ∈ Nat.digits 10 2, d = 0 ∨ d = 1⊢ 2 < 10refine_2.«2»m:ℕhm:2 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:2 < 10hm_pos:0 < 2h2dvd:2 ∣ 2hd:∀ d ∈ Nat.digits 10 2, d = 0 ∨ d = 1hm_d:Nat.digits 10 2 = [2]⊢ Falseh_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10 decideAll goals completed! 🐙refine_2.«2»m:ℕhm:2 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:2 < 10hm_pos:0 < 2h2dvd:2 ∣ 2hd:∀ d ∈ Nat.digits 10 2, d = 0 ∨ d = 1hm_d:Nat.digits 10 2 = [2]⊢ Falseh_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10)refine_2.«2»m:ℕhm:2 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:2 < 10hm_pos:0 < 2h2dvd:2 ∣ 2hd:∀ d ∈ Nat.digits 10 2, d = 0 ∨ d = 1hm_d:Nat.digits 10 2 = [2]⊢ Falseh_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10
        have h_mem : 2 ∈ Nat.digits 10 2 := by⊢ a 2 = 10refine_2.«2»m:ℕhm:2 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:2 < 10hm_pos:0 < 2h2dvd:2 ∣ 2hd:∀ d ∈ Nat.digits 10 2, d = 0 ∨ d = 1hm_d:Nat.digits 10 2 = [2]h_mem:2 ∈ Nat.digits 10 2⊢ Falseh_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10 rw [hm_dm:ℕhm:2 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:2 < 10hm_pos:0 < 2h2dvd:2 ∣ 2hd:∀ d ∈ Nat.digits 10 2, d = 0 ∨ d = 1hm_d:Nat.digits 10 2 = [2]⊢ 2 ∈ [2]m:ℕhm:2 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:2 < 10hm_pos:0 < 2h2dvd:2 ∣ 2hd:∀ d ∈ Nat.digits 10 2, d = 0 ∨ d = 1hm_d:Nat.digits 10 2 = [2]⊢ 2 ∈ [2]refine_2.«2»m:ℕhm:2 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:2 < 10hm_pos:0 < 2h2dvd:2 ∣ 2hd:∀ d ∈ Nat.digits 10 2, d = 0 ∨ d = 1hm_d:Nat.digits 10 2 = [2]h_mem:2 ∈ Nat.digits 10 2⊢ Falseh_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10]m:ℕhm:2 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:2 < 10hm_pos:0 < 2h2dvd:2 ∣ 2hd:∀ d ∈ Nat.digits 10 2, d = 0 ∨ d = 1hm_d:Nat.digits 10 2 = [2]⊢ 2 ∈ [2]refine_2.«2»m:ℕhm:2 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:2 < 10hm_pos:0 < 2h2dvd:2 ∣ 2hd:∀ d ∈ Nat.digits 10 2, d = 0 ∨ d = 1hm_d:Nat.digits 10 2 = [2]h_mem:2 ∈ Nat.digits 10 2⊢ Falseh_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10; exact List.Mem.head []refine_2.«2»m:ℕhm:2 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:2 < 10hm_pos:0 < 2h2dvd:2 ∣ 2hd:∀ d ∈ Nat.digits 10 2, d = 0 ∨ d = 1hm_d:Nat.digits 10 2 = [2]h_mem:2 ∈ Nat.digits 10 2⊢ Falseh_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10refine_2.«2»m:ℕhm:2 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:2 < 10hm_pos:0 < 2h2dvd:2 ∣ 2hd:∀ d ∈ Nat.digits 10 2, d = 0 ∨ d = 1hm_d:Nat.digits 10 2 = [2]h_mem:2 ∈ Nat.digits 10 2⊢ Falseh_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10
        have := hd 2 h_memrefine_2.«2»m:ℕhm:2 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:2 < 10hm_pos:0 < 2h2dvd:2 ∣ 2hd:∀ d ∈ Nat.digits 10 2, d = 0 ∨ d = 1hm_d:Nat.digits 10 2 = [2]h_mem:2 ∈ Nat.digits 10 2this:2 = 0 ∨ 2 = 1⊢ Falseh_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10; omegaAll goals completed! 🐙h_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10
      ·refine_2.«3»m:ℕhm:3 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:3 < 10hm_pos:0 < 3h2dvd:2 ∣ 3hd:∀ d ∈ Nat.digits 10 3, d = 0 ∨ d = 1⊢ Falseh_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10 have hm_d : Nat.digits 10 3 = [3] := Nat.digits_of_lt 10 3 (bym:ℕhm:3 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:3 < 10hm_pos:0 < 3h2dvd:2 ∣ 3hd:∀ d ∈ Nat.digits 10 3, d = 0 ∨ d = 1⊢ 3 ≠ 0refine_2.«3»m:ℕhm:3 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:3 < 10hm_pos:0 < 3h2dvd:2 ∣ 3hd:∀ d ∈ Nat.digits 10 3, d = 0 ∨ d = 1hm_d:Nat.digits 10 3 = [3]⊢ Falseh_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10 decideAll goals completed! 🐙refine_2.«3»m:ℕhm:3 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:3 < 10hm_pos:0 < 3h2dvd:2 ∣ 3hd:∀ d ∈ Nat.digits 10 3, d = 0 ∨ d = 1hm_d:Nat.digits 10 3 = [3]⊢ Falseh_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10) (bym:ℕhm:3 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:3 < 10hm_pos:0 < 3h2dvd:2 ∣ 3hd:∀ d ∈ Nat.digits 10 3, d = 0 ∨ d = 1⊢ 3 < 10refine_2.«3»m:ℕhm:3 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:3 < 10hm_pos:0 < 3h2dvd:2 ∣ 3hd:∀ d ∈ Nat.digits 10 3, d = 0 ∨ d = 1hm_d:Nat.digits 10 3 = [3]⊢ Falseh_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10 decideAll goals completed! 🐙refine_2.«3»m:ℕhm:3 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:3 < 10hm_pos:0 < 3h2dvd:2 ∣ 3hd:∀ d ∈ Nat.digits 10 3, d = 0 ∨ d = 1hm_d:Nat.digits 10 3 = [3]⊢ Falseh_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10)refine_2.«3»m:ℕhm:3 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:3 < 10hm_pos:0 < 3h2dvd:2 ∣ 3hd:∀ d ∈ Nat.digits 10 3, d = 0 ∨ d = 1hm_d:Nat.digits 10 3 = [3]⊢ Falseh_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10
        have h_mem : 3 ∈ Nat.digits 10 3 := by⊢ a 2 = 10refine_2.«3»m:ℕhm:3 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:3 < 10hm_pos:0 < 3h2dvd:2 ∣ 3hd:∀ d ∈ Nat.digits 10 3, d = 0 ∨ d = 1hm_d:Nat.digits 10 3 = [3]h_mem:3 ∈ Nat.digits 10 3⊢ Falseh_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10 rw [hm_dm:ℕhm:3 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:3 < 10hm_pos:0 < 3h2dvd:2 ∣ 3hd:∀ d ∈ Nat.digits 10 3, d = 0 ∨ d = 1hm_d:Nat.digits 10 3 = [3]⊢ 3 ∈ [3]m:ℕhm:3 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:3 < 10hm_pos:0 < 3h2dvd:2 ∣ 3hd:∀ d ∈ Nat.digits 10 3, d = 0 ∨ d = 1hm_d:Nat.digits 10 3 = [3]⊢ 3 ∈ [3]refine_2.«3»m:ℕhm:3 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:3 < 10hm_pos:0 < 3h2dvd:2 ∣ 3hd:∀ d ∈ Nat.digits 10 3, d = 0 ∨ d = 1hm_d:Nat.digits 10 3 = [3]h_mem:3 ∈ Nat.digits 10 3⊢ Falseh_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10]m:ℕhm:3 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:3 < 10hm_pos:0 < 3h2dvd:2 ∣ 3hd:∀ d ∈ Nat.digits 10 3, d = 0 ∨ d = 1hm_d:Nat.digits 10 3 = [3]⊢ 3 ∈ [3]refine_2.«3»m:ℕhm:3 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:3 < 10hm_pos:0 < 3h2dvd:2 ∣ 3hd:∀ d ∈ Nat.digits 10 3, d = 0 ∨ d = 1hm_d:Nat.digits 10 3 = [3]h_mem:3 ∈ Nat.digits 10 3⊢ Falseh_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10; exact List.Mem.head []refine_2.«3»m:ℕhm:3 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:3 < 10hm_pos:0 < 3h2dvd:2 ∣ 3hd:∀ d ∈ Nat.digits 10 3, d = 0 ∨ d = 1hm_d:Nat.digits 10 3 = [3]h_mem:3 ∈ Nat.digits 10 3⊢ Falseh_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10refine_2.«3»m:ℕhm:3 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:3 < 10hm_pos:0 < 3h2dvd:2 ∣ 3hd:∀ d ∈ Nat.digits 10 3, d = 0 ∨ d = 1hm_d:Nat.digits 10 3 = [3]h_mem:3 ∈ Nat.digits 10 3⊢ Falseh_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10
        have := hd 3 h_memrefine_2.«3»m:ℕhm:3 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:3 < 10hm_pos:0 < 3h2dvd:2 ∣ 3hd:∀ d ∈ Nat.digits 10 3, d = 0 ∨ d = 1hm_d:Nat.digits 10 3 = [3]h_mem:3 ∈ Nat.digits 10 3this:3 = 0 ∨ 3 = 1⊢ Falseh_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10; omegaAll goals completed! 🐙h_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10
      ·refine_2.«4»m:ℕhm:4 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:4 < 10hm_pos:0 < 4h2dvd:2 ∣ 4hd:∀ d ∈ Nat.digits 10 4, d = 0 ∨ d = 1⊢ Falseh_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10 have hm_d : Nat.digits 10 4 = [4] := Nat.digits_of_lt 10 4 (bym:ℕhm:4 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:4 < 10hm_pos:0 < 4h2dvd:2 ∣ 4hd:∀ d ∈ Nat.digits 10 4, d = 0 ∨ d = 1⊢ 4 ≠ 0refine_2.«4»m:ℕhm:4 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:4 < 10hm_pos:0 < 4h2dvd:2 ∣ 4hd:∀ d ∈ Nat.digits 10 4, d = 0 ∨ d = 1hm_d:Nat.digits 10 4 = [4]⊢ Falseh_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10 decideAll goals completed! 🐙refine_2.«4»m:ℕhm:4 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:4 < 10hm_pos:0 < 4h2dvd:2 ∣ 4hd:∀ d ∈ Nat.digits 10 4, d = 0 ∨ d = 1hm_d:Nat.digits 10 4 = [4]⊢ Falseh_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10) (bym:ℕhm:4 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:4 < 10hm_pos:0 < 4h2dvd:2 ∣ 4hd:∀ d ∈ Nat.digits 10 4, d = 0 ∨ d = 1⊢ 4 < 10refine_2.«4»m:ℕhm:4 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:4 < 10hm_pos:0 < 4h2dvd:2 ∣ 4hd:∀ d ∈ Nat.digits 10 4, d = 0 ∨ d = 1hm_d:Nat.digits 10 4 = [4]⊢ Falseh_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10 decideAll goals completed! 🐙refine_2.«4»m:ℕhm:4 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:4 < 10hm_pos:0 < 4h2dvd:2 ∣ 4hd:∀ d ∈ Nat.digits 10 4, d = 0 ∨ d = 1hm_d:Nat.digits 10 4 = [4]⊢ Falseh_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10)refine_2.«4»m:ℕhm:4 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:4 < 10hm_pos:0 < 4h2dvd:2 ∣ 4hd:∀ d ∈ Nat.digits 10 4, d = 0 ∨ d = 1hm_d:Nat.digits 10 4 = [4]⊢ Falseh_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10
        have h_mem : 4 ∈ Nat.digits 10 4 := by⊢ a 2 = 10refine_2.«4»m:ℕhm:4 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:4 < 10hm_pos:0 < 4h2dvd:2 ∣ 4hd:∀ d ∈ Nat.digits 10 4, d = 0 ∨ d = 1hm_d:Nat.digits 10 4 = [4]h_mem:4 ∈ Nat.digits 10 4⊢ Falseh_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10 rw [hm_dm:ℕhm:4 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:4 < 10hm_pos:0 < 4h2dvd:2 ∣ 4hd:∀ d ∈ Nat.digits 10 4, d = 0 ∨ d = 1hm_d:Nat.digits 10 4 = [4]⊢ 4 ∈ [4]m:ℕhm:4 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:4 < 10hm_pos:0 < 4h2dvd:2 ∣ 4hd:∀ d ∈ Nat.digits 10 4, d = 0 ∨ d = 1hm_d:Nat.digits 10 4 = [4]⊢ 4 ∈ [4]refine_2.«4»m:ℕhm:4 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:4 < 10hm_pos:0 < 4h2dvd:2 ∣ 4hd:∀ d ∈ Nat.digits 10 4, d = 0 ∨ d = 1hm_d:Nat.digits 10 4 = [4]h_mem:4 ∈ Nat.digits 10 4⊢ Falseh_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10]m:ℕhm:4 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:4 < 10hm_pos:0 < 4h2dvd:2 ∣ 4hd:∀ d ∈ Nat.digits 10 4, d = 0 ∨ d = 1hm_d:Nat.digits 10 4 = [4]⊢ 4 ∈ [4]refine_2.«4»m:ℕhm:4 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:4 < 10hm_pos:0 < 4h2dvd:2 ∣ 4hd:∀ d ∈ Nat.digits 10 4, d = 0 ∨ d = 1hm_d:Nat.digits 10 4 = [4]h_mem:4 ∈ Nat.digits 10 4⊢ Falseh_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10; exact List.Mem.head []refine_2.«4»m:ℕhm:4 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:4 < 10hm_pos:0 < 4h2dvd:2 ∣ 4hd:∀ d ∈ Nat.digits 10 4, d = 0 ∨ d = 1hm_d:Nat.digits 10 4 = [4]h_mem:4 ∈ Nat.digits 10 4⊢ Falseh_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10refine_2.«4»m:ℕhm:4 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:4 < 10hm_pos:0 < 4h2dvd:2 ∣ 4hd:∀ d ∈ Nat.digits 10 4, d = 0 ∨ d = 1hm_d:Nat.digits 10 4 = [4]h_mem:4 ∈ Nat.digits 10 4⊢ Falseh_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10
        have := hd 4 h_memrefine_2.«4»m:ℕhm:4 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:4 < 10hm_pos:0 < 4h2dvd:2 ∣ 4hd:∀ d ∈ Nat.digits 10 4, d = 0 ∨ d = 1hm_d:Nat.digits 10 4 = [4]h_mem:4 ∈ Nat.digits 10 4this:4 = 0 ∨ 4 = 1⊢ Falseh_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10; omegaAll goals completed! 🐙h_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10
      ·refine_2.«5»m:ℕhm:5 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:5 < 10hm_pos:0 < 5h2dvd:2 ∣ 5hd:∀ d ∈ Nat.digits 10 5, d = 0 ∨ d = 1⊢ Falseh_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10 have hm_d : Nat.digits 10 5 = [5] := Nat.digits_of_lt 10 5 (bym:ℕhm:5 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:5 < 10hm_pos:0 < 5h2dvd:2 ∣ 5hd:∀ d ∈ Nat.digits 10 5, d = 0 ∨ d = 1⊢ 5 ≠ 0refine_2.«5»m:ℕhm:5 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:5 < 10hm_pos:0 < 5h2dvd:2 ∣ 5hd:∀ d ∈ Nat.digits 10 5, d = 0 ∨ d = 1hm_d:Nat.digits 10 5 = [5]⊢ Falseh_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10 decideAll goals completed! 🐙refine_2.«5»m:ℕhm:5 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:5 < 10hm_pos:0 < 5h2dvd:2 ∣ 5hd:∀ d ∈ Nat.digits 10 5, d = 0 ∨ d = 1hm_d:Nat.digits 10 5 = [5]⊢ Falseh_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10) (bym:ℕhm:5 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:5 < 10hm_pos:0 < 5h2dvd:2 ∣ 5hd:∀ d ∈ Nat.digits 10 5, d = 0 ∨ d = 1⊢ 5 < 10refine_2.«5»m:ℕhm:5 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:5 < 10hm_pos:0 < 5h2dvd:2 ∣ 5hd:∀ d ∈ Nat.digits 10 5, d = 0 ∨ d = 1hm_d:Nat.digits 10 5 = [5]⊢ Falseh_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10 decideAll goals completed! 🐙refine_2.«5»m:ℕhm:5 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:5 < 10hm_pos:0 < 5h2dvd:2 ∣ 5hd:∀ d ∈ Nat.digits 10 5, d = 0 ∨ d = 1hm_d:Nat.digits 10 5 = [5]⊢ Falseh_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10)refine_2.«5»m:ℕhm:5 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:5 < 10hm_pos:0 < 5h2dvd:2 ∣ 5hd:∀ d ∈ Nat.digits 10 5, d = 0 ∨ d = 1hm_d:Nat.digits 10 5 = [5]⊢ Falseh_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10
        have h_mem : 5 ∈ Nat.digits 10 5 := by⊢ a 2 = 10refine_2.«5»m:ℕhm:5 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:5 < 10hm_pos:0 < 5h2dvd:2 ∣ 5hd:∀ d ∈ Nat.digits 10 5, d = 0 ∨ d = 1hm_d:Nat.digits 10 5 = [5]h_mem:5 ∈ Nat.digits 10 5⊢ Falseh_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10 rw [hm_dm:ℕhm:5 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:5 < 10hm_pos:0 < 5h2dvd:2 ∣ 5hd:∀ d ∈ Nat.digits 10 5, d = 0 ∨ d = 1hm_d:Nat.digits 10 5 = [5]⊢ 5 ∈ [5]m:ℕhm:5 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:5 < 10hm_pos:0 < 5h2dvd:2 ∣ 5hd:∀ d ∈ Nat.digits 10 5, d = 0 ∨ d = 1hm_d:Nat.digits 10 5 = [5]⊢ 5 ∈ [5]refine_2.«5»m:ℕhm:5 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:5 < 10hm_pos:0 < 5h2dvd:2 ∣ 5hd:∀ d ∈ Nat.digits 10 5, d = 0 ∨ d = 1hm_d:Nat.digits 10 5 = [5]h_mem:5 ∈ Nat.digits 10 5⊢ Falseh_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10]m:ℕhm:5 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:5 < 10hm_pos:0 < 5h2dvd:2 ∣ 5hd:∀ d ∈ Nat.digits 10 5, d = 0 ∨ d = 1hm_d:Nat.digits 10 5 = [5]⊢ 5 ∈ [5]refine_2.«5»m:ℕhm:5 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:5 < 10hm_pos:0 < 5h2dvd:2 ∣ 5hd:∀ d ∈ Nat.digits 10 5, d = 0 ∨ d = 1hm_d:Nat.digits 10 5 = [5]h_mem:5 ∈ Nat.digits 10 5⊢ Falseh_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10; exact List.Mem.head []refine_2.«5»m:ℕhm:5 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:5 < 10hm_pos:0 < 5h2dvd:2 ∣ 5hd:∀ d ∈ Nat.digits 10 5, d = 0 ∨ d = 1hm_d:Nat.digits 10 5 = [5]h_mem:5 ∈ Nat.digits 10 5⊢ Falseh_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10refine_2.«5»m:ℕhm:5 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:5 < 10hm_pos:0 < 5h2dvd:2 ∣ 5hd:∀ d ∈ Nat.digits 10 5, d = 0 ∨ d = 1hm_d:Nat.digits 10 5 = [5]h_mem:5 ∈ Nat.digits 10 5⊢ Falseh_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10
        have := hd 5 h_memrefine_2.«5»m:ℕhm:5 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:5 < 10hm_pos:0 < 5h2dvd:2 ∣ 5hd:∀ d ∈ Nat.digits 10 5, d = 0 ∨ d = 1hm_d:Nat.digits 10 5 = [5]h_mem:5 ∈ Nat.digits 10 5this:5 = 0 ∨ 5 = 1⊢ Falseh_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10; omegaAll goals completed! 🐙h_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10
      ·refine_2.«6»m:ℕhm:6 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:6 < 10hm_pos:0 < 6h2dvd:2 ∣ 6hd:∀ d ∈ Nat.digits 10 6, d = 0 ∨ d = 1⊢ Falseh_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10 have hm_d : Nat.digits 10 6 = [6] := Nat.digits_of_lt 10 6 (bym:ℕhm:6 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:6 < 10hm_pos:0 < 6h2dvd:2 ∣ 6hd:∀ d ∈ Nat.digits 10 6, d = 0 ∨ d = 1⊢ 6 ≠ 0refine_2.«6»m:ℕhm:6 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:6 < 10hm_pos:0 < 6h2dvd:2 ∣ 6hd:∀ d ∈ Nat.digits 10 6, d = 0 ∨ d = 1hm_d:Nat.digits 10 6 = [6]⊢ Falseh_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10 decideAll goals completed! 🐙refine_2.«6»m:ℕhm:6 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:6 < 10hm_pos:0 < 6h2dvd:2 ∣ 6hd:∀ d ∈ Nat.digits 10 6, d = 0 ∨ d = 1hm_d:Nat.digits 10 6 = [6]⊢ Falseh_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10) (bym:ℕhm:6 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:6 < 10hm_pos:0 < 6h2dvd:2 ∣ 6hd:∀ d ∈ Nat.digits 10 6, d = 0 ∨ d = 1⊢ 6 < 10refine_2.«6»m:ℕhm:6 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:6 < 10hm_pos:0 < 6h2dvd:2 ∣ 6hd:∀ d ∈ Nat.digits 10 6, d = 0 ∨ d = 1hm_d:Nat.digits 10 6 = [6]⊢ Falseh_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10 decideAll goals completed! 🐙refine_2.«6»m:ℕhm:6 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:6 < 10hm_pos:0 < 6h2dvd:2 ∣ 6hd:∀ d ∈ Nat.digits 10 6, d = 0 ∨ d = 1hm_d:Nat.digits 10 6 = [6]⊢ Falseh_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10)refine_2.«6»m:ℕhm:6 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:6 < 10hm_pos:0 < 6h2dvd:2 ∣ 6hd:∀ d ∈ Nat.digits 10 6, d = 0 ∨ d = 1hm_d:Nat.digits 10 6 = [6]⊢ Falseh_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10
        have h_mem : 6 ∈ Nat.digits 10 6 := by⊢ a 2 = 10refine_2.«6»m:ℕhm:6 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:6 < 10hm_pos:0 < 6h2dvd:2 ∣ 6hd:∀ d ∈ Nat.digits 10 6, d = 0 ∨ d = 1hm_d:Nat.digits 10 6 = [6]h_mem:6 ∈ Nat.digits 10 6⊢ Falseh_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10 rw [hm_dm:ℕhm:6 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:6 < 10hm_pos:0 < 6h2dvd:2 ∣ 6hd:∀ d ∈ Nat.digits 10 6, d = 0 ∨ d = 1hm_d:Nat.digits 10 6 = [6]⊢ 6 ∈ [6]m:ℕhm:6 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:6 < 10hm_pos:0 < 6h2dvd:2 ∣ 6hd:∀ d ∈ Nat.digits 10 6, d = 0 ∨ d = 1hm_d:Nat.digits 10 6 = [6]⊢ 6 ∈ [6]refine_2.«6»m:ℕhm:6 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:6 < 10hm_pos:0 < 6h2dvd:2 ∣ 6hd:∀ d ∈ Nat.digits 10 6, d = 0 ∨ d = 1hm_d:Nat.digits 10 6 = [6]h_mem:6 ∈ Nat.digits 10 6⊢ Falseh_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10]m:ℕhm:6 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:6 < 10hm_pos:0 < 6h2dvd:2 ∣ 6hd:∀ d ∈ Nat.digits 10 6, d = 0 ∨ d = 1hm_d:Nat.digits 10 6 = [6]⊢ 6 ∈ [6]refine_2.«6»m:ℕhm:6 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:6 < 10hm_pos:0 < 6h2dvd:2 ∣ 6hd:∀ d ∈ Nat.digits 10 6, d = 0 ∨ d = 1hm_d:Nat.digits 10 6 = [6]h_mem:6 ∈ Nat.digits 10 6⊢ Falseh_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10; exact List.Mem.head []refine_2.«6»m:ℕhm:6 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:6 < 10hm_pos:0 < 6h2dvd:2 ∣ 6hd:∀ d ∈ Nat.digits 10 6, d = 0 ∨ d = 1hm_d:Nat.digits 10 6 = [6]h_mem:6 ∈ Nat.digits 10 6⊢ Falseh_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10refine_2.«6»m:ℕhm:6 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:6 < 10hm_pos:0 < 6h2dvd:2 ∣ 6hd:∀ d ∈ Nat.digits 10 6, d = 0 ∨ d = 1hm_d:Nat.digits 10 6 = [6]h_mem:6 ∈ Nat.digits 10 6⊢ Falseh_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10
        have := hd 6 h_memrefine_2.«6»m:ℕhm:6 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:6 < 10hm_pos:0 < 6h2dvd:2 ∣ 6hd:∀ d ∈ Nat.digits 10 6, d = 0 ∨ d = 1hm_d:Nat.digits 10 6 = [6]h_mem:6 ∈ Nat.digits 10 6this:6 = 0 ∨ 6 = 1⊢ Falseh_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10; omegaAll goals completed! 🐙h_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10
      ·refine_2.«7»m:ℕhm:7 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:7 < 10hm_pos:0 < 7h2dvd:2 ∣ 7hd:∀ d ∈ Nat.digits 10 7, d = 0 ∨ d = 1⊢ Falseh_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10 have hm_d : Nat.digits 10 7 = [7] := Nat.digits_of_lt 10 7 (bym:ℕhm:7 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:7 < 10hm_pos:0 < 7h2dvd:2 ∣ 7hd:∀ d ∈ Nat.digits 10 7, d = 0 ∨ d = 1⊢ 7 ≠ 0refine_2.«7»m:ℕhm:7 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:7 < 10hm_pos:0 < 7h2dvd:2 ∣ 7hd:∀ d ∈ Nat.digits 10 7, d = 0 ∨ d = 1hm_d:Nat.digits 10 7 = [7]⊢ Falseh_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10 decideAll goals completed! 🐙refine_2.«7»m:ℕhm:7 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:7 < 10hm_pos:0 < 7h2dvd:2 ∣ 7hd:∀ d ∈ Nat.digits 10 7, d = 0 ∨ d = 1hm_d:Nat.digits 10 7 = [7]⊢ Falseh_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10) (bym:ℕhm:7 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:7 < 10hm_pos:0 < 7h2dvd:2 ∣ 7hd:∀ d ∈ Nat.digits 10 7, d = 0 ∨ d = 1⊢ 7 < 10refine_2.«7»m:ℕhm:7 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:7 < 10hm_pos:0 < 7h2dvd:2 ∣ 7hd:∀ d ∈ Nat.digits 10 7, d = 0 ∨ d = 1hm_d:Nat.digits 10 7 = [7]⊢ Falseh_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10 decideAll goals completed! 🐙refine_2.«7»m:ℕhm:7 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:7 < 10hm_pos:0 < 7h2dvd:2 ∣ 7hd:∀ d ∈ Nat.digits 10 7, d = 0 ∨ d = 1hm_d:Nat.digits 10 7 = [7]⊢ Falseh_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10)refine_2.«7»m:ℕhm:7 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:7 < 10hm_pos:0 < 7h2dvd:2 ∣ 7hd:∀ d ∈ Nat.digits 10 7, d = 0 ∨ d = 1hm_d:Nat.digits 10 7 = [7]⊢ Falseh_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10
        have h_mem : 7 ∈ Nat.digits 10 7 := by⊢ a 2 = 10refine_2.«7»m:ℕhm:7 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:7 < 10hm_pos:0 < 7h2dvd:2 ∣ 7hd:∀ d ∈ Nat.digits 10 7, d = 0 ∨ d = 1hm_d:Nat.digits 10 7 = [7]h_mem:7 ∈ Nat.digits 10 7⊢ Falseh_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10 rw [hm_dm:ℕhm:7 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:7 < 10hm_pos:0 < 7h2dvd:2 ∣ 7hd:∀ d ∈ Nat.digits 10 7, d = 0 ∨ d = 1hm_d:Nat.digits 10 7 = [7]⊢ 7 ∈ [7]m:ℕhm:7 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:7 < 10hm_pos:0 < 7h2dvd:2 ∣ 7hd:∀ d ∈ Nat.digits 10 7, d = 0 ∨ d = 1hm_d:Nat.digits 10 7 = [7]⊢ 7 ∈ [7]refine_2.«7»m:ℕhm:7 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:7 < 10hm_pos:0 < 7h2dvd:2 ∣ 7hd:∀ d ∈ Nat.digits 10 7, d = 0 ∨ d = 1hm_d:Nat.digits 10 7 = [7]h_mem:7 ∈ Nat.digits 10 7⊢ Falseh_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10]m:ℕhm:7 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:7 < 10hm_pos:0 < 7h2dvd:2 ∣ 7hd:∀ d ∈ Nat.digits 10 7, d = 0 ∨ d = 1hm_d:Nat.digits 10 7 = [7]⊢ 7 ∈ [7]refine_2.«7»m:ℕhm:7 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:7 < 10hm_pos:0 < 7h2dvd:2 ∣ 7hd:∀ d ∈ Nat.digits 10 7, d = 0 ∨ d = 1hm_d:Nat.digits 10 7 = [7]h_mem:7 ∈ Nat.digits 10 7⊢ Falseh_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10; exact List.Mem.head []refine_2.«7»m:ℕhm:7 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:7 < 10hm_pos:0 < 7h2dvd:2 ∣ 7hd:∀ d ∈ Nat.digits 10 7, d = 0 ∨ d = 1hm_d:Nat.digits 10 7 = [7]h_mem:7 ∈ Nat.digits 10 7⊢ Falseh_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10refine_2.«7»m:ℕhm:7 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:7 < 10hm_pos:0 < 7h2dvd:2 ∣ 7hd:∀ d ∈ Nat.digits 10 7, d = 0 ∨ d = 1hm_d:Nat.digits 10 7 = [7]h_mem:7 ∈ Nat.digits 10 7⊢ Falseh_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10
        have := hd 7 h_memrefine_2.«7»m:ℕhm:7 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:7 < 10hm_pos:0 < 7h2dvd:2 ∣ 7hd:∀ d ∈ Nat.digits 10 7, d = 0 ∨ d = 1hm_d:Nat.digits 10 7 = [7]h_mem:7 ∈ Nat.digits 10 7this:7 = 0 ∨ 7 = 1⊢ Falseh_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10; omegaAll goals completed! 🐙h_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10
      ·refine_2.«8»m:ℕhm:8 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:8 < 10hm_pos:0 < 8h2dvd:2 ∣ 8hd:∀ d ∈ Nat.digits 10 8, d = 0 ∨ d = 1⊢ Falseh_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10 have hm_d : Nat.digits 10 8 = [8] := Nat.digits_of_lt 10 8 (bym:ℕhm:8 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:8 < 10hm_pos:0 < 8h2dvd:2 ∣ 8hd:∀ d ∈ Nat.digits 10 8, d = 0 ∨ d = 1⊢ 8 ≠ 0refine_2.«8»m:ℕhm:8 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:8 < 10hm_pos:0 < 8h2dvd:2 ∣ 8hd:∀ d ∈ Nat.digits 10 8, d = 0 ∨ d = 1hm_d:Nat.digits 10 8 = [8]⊢ Falseh_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10 decideAll goals completed! 🐙refine_2.«8»m:ℕhm:8 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:8 < 10hm_pos:0 < 8h2dvd:2 ∣ 8hd:∀ d ∈ Nat.digits 10 8, d = 0 ∨ d = 1hm_d:Nat.digits 10 8 = [8]⊢ Falseh_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10) (bym:ℕhm:8 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:8 < 10hm_pos:0 < 8h2dvd:2 ∣ 8hd:∀ d ∈ Nat.digits 10 8, d = 0 ∨ d = 1⊢ 8 < 10refine_2.«8»m:ℕhm:8 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:8 < 10hm_pos:0 < 8h2dvd:2 ∣ 8hd:∀ d ∈ Nat.digits 10 8, d = 0 ∨ d = 1hm_d:Nat.digits 10 8 = [8]⊢ Falseh_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10 decideAll goals completed! 🐙refine_2.«8»m:ℕhm:8 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:8 < 10hm_pos:0 < 8h2dvd:2 ∣ 8hd:∀ d ∈ Nat.digits 10 8, d = 0 ∨ d = 1hm_d:Nat.digits 10 8 = [8]⊢ Falseh_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10)refine_2.«8»m:ℕhm:8 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:8 < 10hm_pos:0 < 8h2dvd:2 ∣ 8hd:∀ d ∈ Nat.digits 10 8, d = 0 ∨ d = 1hm_d:Nat.digits 10 8 = [8]⊢ Falseh_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10
        have h_mem : 8 ∈ Nat.digits 10 8 := by⊢ a 2 = 10refine_2.«8»m:ℕhm:8 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:8 < 10hm_pos:0 < 8h2dvd:2 ∣ 8hd:∀ d ∈ Nat.digits 10 8, d = 0 ∨ d = 1hm_d:Nat.digits 10 8 = [8]h_mem:8 ∈ Nat.digits 10 8⊢ Falseh_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10 rw [hm_dm:ℕhm:8 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:8 < 10hm_pos:0 < 8h2dvd:2 ∣ 8hd:∀ d ∈ Nat.digits 10 8, d = 0 ∨ d = 1hm_d:Nat.digits 10 8 = [8]⊢ 8 ∈ [8]m:ℕhm:8 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:8 < 10hm_pos:0 < 8h2dvd:2 ∣ 8hd:∀ d ∈ Nat.digits 10 8, d = 0 ∨ d = 1hm_d:Nat.digits 10 8 = [8]⊢ 8 ∈ [8]refine_2.«8»m:ℕhm:8 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:8 < 10hm_pos:0 < 8h2dvd:2 ∣ 8hd:∀ d ∈ Nat.digits 10 8, d = 0 ∨ d = 1hm_d:Nat.digits 10 8 = [8]h_mem:8 ∈ Nat.digits 10 8⊢ Falseh_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10]m:ℕhm:8 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:8 < 10hm_pos:0 < 8h2dvd:2 ∣ 8hd:∀ d ∈ Nat.digits 10 8, d = 0 ∨ d = 1hm_d:Nat.digits 10 8 = [8]⊢ 8 ∈ [8]refine_2.«8»m:ℕhm:8 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:8 < 10hm_pos:0 < 8h2dvd:2 ∣ 8hd:∀ d ∈ Nat.digits 10 8, d = 0 ∨ d = 1hm_d:Nat.digits 10 8 = [8]h_mem:8 ∈ Nat.digits 10 8⊢ Falseh_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10; exact List.Mem.head []refine_2.«8»m:ℕhm:8 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:8 < 10hm_pos:0 < 8h2dvd:2 ∣ 8hd:∀ d ∈ Nat.digits 10 8, d = 0 ∨ d = 1hm_d:Nat.digits 10 8 = [8]h_mem:8 ∈ Nat.digits 10 8⊢ Falseh_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10refine_2.«8»m:ℕhm:8 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:8 < 10hm_pos:0 < 8h2dvd:2 ∣ 8hd:∀ d ∈ Nat.digits 10 8, d = 0 ∨ d = 1hm_d:Nat.digits 10 8 = [8]h_mem:8 ∈ Nat.digits 10 8⊢ Falseh_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10
        have := hd 8 h_memrefine_2.«8»m:ℕhm:8 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:8 < 10hm_pos:0 < 8h2dvd:2 ∣ 8hd:∀ d ∈ Nat.digits 10 8, d = 0 ∨ d = 1hm_d:Nat.digits 10 8 = [8]h_mem:8 ∈ Nat.digits 10 8this:8 = 0 ∨ 8 = 1⊢ Falseh_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10; omegaAll goals completed! 🐙h_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10
      ·refine_2.«9»m:ℕhm:9 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:9 < 10hm_pos:0 < 9h2dvd:2 ∣ 9hd:∀ d ∈ Nat.digits 10 9, d = 0 ∨ d = 1⊢ Falseh_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10 have hm_d : Nat.digits 10 9 = [9] := Nat.digits_of_lt 10 9 (bym:ℕhm:9 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:9 < 10hm_pos:0 < 9h2dvd:2 ∣ 9hd:∀ d ∈ Nat.digits 10 9, d = 0 ∨ d = 1⊢ 9 ≠ 0refine_2.«9»m:ℕhm:9 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:9 < 10hm_pos:0 < 9h2dvd:2 ∣ 9hd:∀ d ∈ Nat.digits 10 9, d = 0 ∨ d = 1hm_d:Nat.digits 10 9 = [9]⊢ Falseh_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10 decideAll goals completed! 🐙refine_2.«9»m:ℕhm:9 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:9 < 10hm_pos:0 < 9h2dvd:2 ∣ 9hd:∀ d ∈ Nat.digits 10 9, d = 0 ∨ d = 1hm_d:Nat.digits 10 9 = [9]⊢ Falseh_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10) (bym:ℕhm:9 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:9 < 10hm_pos:0 < 9h2dvd:2 ∣ 9hd:∀ d ∈ Nat.digits 10 9, d = 0 ∨ d = 1⊢ 9 < 10refine_2.«9»m:ℕhm:9 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:9 < 10hm_pos:0 < 9h2dvd:2 ∣ 9hd:∀ d ∈ Nat.digits 10 9, d = 0 ∨ d = 1hm_d:Nat.digits 10 9 = [9]⊢ Falseh_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10 decideAll goals completed! 🐙refine_2.«9»m:ℕhm:9 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:9 < 10hm_pos:0 < 9h2dvd:2 ∣ 9hd:∀ d ∈ Nat.digits 10 9, d = 0 ∨ d = 1hm_d:Nat.digits 10 9 = [9]⊢ Falseh_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10)refine_2.«9»m:ℕhm:9 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:9 < 10hm_pos:0 < 9h2dvd:2 ∣ 9hd:∀ d ∈ Nat.digits 10 9, d = 0 ∨ d = 1hm_d:Nat.digits 10 9 = [9]⊢ Falseh_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10
        have h_mem : 9 ∈ Nat.digits 10 9 := by⊢ a 2 = 10refine_2.«9»m:ℕhm:9 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:9 < 10hm_pos:0 < 9h2dvd:2 ∣ 9hd:∀ d ∈ Nat.digits 10 9, d = 0 ∨ d = 1hm_d:Nat.digits 10 9 = [9]h_mem:9 ∈ Nat.digits 10 9⊢ Falseh_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10 rw [hm_dm:ℕhm:9 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:9 < 10hm_pos:0 < 9h2dvd:2 ∣ 9hd:∀ d ∈ Nat.digits 10 9, d = 0 ∨ d = 1hm_d:Nat.digits 10 9 = [9]⊢ 9 ∈ [9]m:ℕhm:9 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:9 < 10hm_pos:0 < 9h2dvd:2 ∣ 9hd:∀ d ∈ Nat.digits 10 9, d = 0 ∨ d = 1hm_d:Nat.digits 10 9 = [9]⊢ 9 ∈ [9]refine_2.«9»m:ℕhm:9 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:9 < 10hm_pos:0 < 9h2dvd:2 ∣ 9hd:∀ d ∈ Nat.digits 10 9, d = 0 ∨ d = 1hm_d:Nat.digits 10 9 = [9]h_mem:9 ∈ Nat.digits 10 9⊢ Falseh_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10]m:ℕhm:9 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:9 < 10hm_pos:0 < 9h2dvd:2 ∣ 9hd:∀ d ∈ Nat.digits 10 9, d = 0 ∨ d = 1hm_d:Nat.digits 10 9 = [9]⊢ 9 ∈ [9]refine_2.«9»m:ℕhm:9 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:9 < 10hm_pos:0 < 9h2dvd:2 ∣ 9hd:∀ d ∈ Nat.digits 10 9, d = 0 ∨ d = 1hm_d:Nat.digits 10 9 = [9]h_mem:9 ∈ Nat.digits 10 9⊢ Falseh_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10; exact List.Mem.head []refine_2.«9»m:ℕhm:9 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:9 < 10hm_pos:0 < 9h2dvd:2 ∣ 9hd:∀ d ∈ Nat.digits 10 9, d = 0 ∨ d = 1hm_d:Nat.digits 10 9 = [9]h_mem:9 ∈ Nat.digits 10 9⊢ Falseh_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10refine_2.«9»m:ℕhm:9 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:9 < 10hm_pos:0 < 9h2dvd:2 ∣ 9hd:∀ d ∈ Nat.digits 10 9, d = 0 ∨ d = 1hm_d:Nat.digits 10 9 = [9]h_mem:9 ∈ Nat.digits 10 9⊢ Falseh_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10
        have := hd 9 h_memrefine_2.«9»m:ℕhm:9 ∈ {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1}hlt:9 < 10hm_pos:0 < 9h2dvd:2 ∣ 9hd:∀ d ∈ Nat.digits 10 9, d = 0 ∨ d = 1hm_d:Nat.digits 10 9 = [9]h_mem:9 ∈ Nat.digits 10 9this:9 = 0 ∨ 9 = 1⊢ Falseh_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10; omegah_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10h_least:IsLeast {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} 10⊢ sInf {m | 0 < m ∧ 2 ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10
  exact h_least.csInf_eqAll goals completed! 🐙

$a(10^k) = 10^k$ for all $k$.


@[category textbook, AMS 11]
theorem a_ten_pow (k : ℕ) : a (10 ^ k) = 10 ^ k := byk:ℕ⊢ a (10 ^ k) = 10 ^ k
  dsimp [a]k:ℕ⊢ sInf {m | 0 < m ∧ 10 ^ k ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10 ^ k
  have h_least : IsLeast { m : ℕ | 0 < m ∧ 10 ^ k ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1 } (10 ^ k) := byk:ℕ⊢ a (10 ^ k) = 10 ^ kk:ℕh_least:IsLeast {m | 0 < m ∧ 10 ^ k ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} (10 ^ k)⊢ sInf {m | 0 < m ∧ 10 ^ k ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10 ^ k
    refine ⟨⟨Nat.pow_pos (byk:ℕ⊢ 0 < 10k:ℕh_least:IsLeast {m | 0 < m ∧ 10 ^ k ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} (10 ^ k)⊢ sInf {m | 0 < m ∧ 10 ^ k ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10 ^ k decideAll goals completed! 🐙k:ℕh_least:IsLeast {m | 0 < m ∧ 10 ^ k ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} (10 ^ k)⊢ sInf {m | 0 < m ∧ 10 ^ k ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10 ^ k), dvd_rfl, ?_⟩, fun m hm ↦ Nat.le_of_dvd hm.1 hm.2.1⟩
    intro d hdk:ℕd:ℕhd:d ∈ Nat.digits 10 (10 ^ k)⊢ d = 0 ∨ d = 1k:ℕh_least:IsLeast {m | 0 < m ∧ 10 ^ k ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} (10 ^ k)⊢ sInf {m | 0 < m ∧ 10 ^ k ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10 ^ k
    have h10k : 10 ^ k = 10 ^ k * 1 := byk:ℕ⊢ a (10 ^ k) = 10 ^ kk:ℕd:ℕhd:d ∈ Nat.digits 10 (10 ^ k)h10k:10 ^ k = 10 ^ k * 1⊢ d = 0 ∨ d = 1k:ℕh_least:IsLeast {m | 0 < m ∧ 10 ^ k ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} (10 ^ k)⊢ sInf {m | 0 < m ∧ 10 ^ k ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10 ^ k rw [mul_onek:ℕd:ℕhd:d ∈ Nat.digits 10 (10 ^ k)⊢ 10 ^ k = 10 ^ kk:ℕd:ℕhd:d ∈ Nat.digits 10 (10 ^ k)h10k:10 ^ k = 10 ^ k * 1⊢ d = 0 ∨ d = 1k:ℕh_least:IsLeast {m | 0 < m ∧ 10 ^ k ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} (10 ^ k)⊢ sInf {m | 0 < m ∧ 10 ^ k ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10 ^ k]k:ℕd:ℕhd:d ∈ Nat.digits 10 (10 ^ k)h10k:10 ^ k = 10 ^ k * 1⊢ d = 0 ∨ d = 1k:ℕh_least:IsLeast {m | 0 < m ∧ 10 ^ k ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} (10 ^ k)⊢ sInf {m | 0 < m ∧ 10 ^ k ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10 ^ kk:ℕd:ℕhd:d ∈ Nat.digits 10 (10 ^ k)h10k:10 ^ k = 10 ^ k * 1⊢ d = 0 ∨ d = 1k:ℕh_least:IsLeast {m | 0 < m ∧ 10 ^ k ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} (10 ^ k)⊢ sInf {m | 0 < m ∧ 10 ^ k ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10 ^ k
    rw [h10k,k:ℕd:ℕhd:d ∈ Nat.digits 10 (10 ^ k * 1)h10k:10 ^ k = 10 ^ k * 1⊢ d = 0 ∨ d = 1k:ℕd:ℕhd:d ∈ List.replicate k 0 ++ [1]h10k:10 ^ k = 10 ^ k * 1⊢ d = 0 ∨ d = 1k:ℕh_least:IsLeast {m | 0 < m ∧ 10 ^ k ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} (10 ^ k)⊢ sInf {m | 0 < m ∧ 10 ^ k ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10 ^ k Nat.digits_base_pow_mul (b := 10) (k := k) (m := 1) (byk:ℕd:ℕhd:d ∈ Nat.digits 10 (10 ^ k * 1)h10k:10 ^ k = 10 ^ k * 1⊢ 1 < 10k:ℕd:ℕhd:d ∈ List.replicate k 0 ++ [1]h10k:10 ^ k = 10 ^ k * 1⊢ d = 0 ∨ d = 1k:ℕh_least:IsLeast {m | 0 < m ∧ 10 ^ k ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} (10 ^ k)⊢ sInf {m | 0 < m ∧ 10 ^ k ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10 ^ k decideAll goals completed! 🐙k:ℕd:ℕhd:d ∈ List.replicate k 0 ++ [1]h10k:10 ^ k = 10 ^ k * 1⊢ d = 0 ∨ d = 1k:ℕh_least:IsLeast {m | 0 < m ∧ 10 ^ k ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} (10 ^ k)⊢ sInf {m | 0 < m ∧ 10 ^ k ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10 ^ k) (byk:ℕd:ℕhd:d ∈ Nat.digits 10 (10 ^ k * 1)h10k:10 ^ k = 10 ^ k * 1⊢ 0 < 1k:ℕd:ℕhd:d ∈ List.replicate k 0 ++ [1]h10k:10 ^ k = 10 ^ k * 1⊢ d = 0 ∨ d = 1k:ℕh_least:IsLeast {m | 0 < m ∧ 10 ^ k ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} (10 ^ k)⊢ sInf {m | 0 < m ∧ 10 ^ k ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10 ^ k decideAll goals completed! 🐙k:ℕd:ℕhd:d ∈ List.replicate k 0 ++ [1]h10k:10 ^ k = 10 ^ k * 1⊢ d = 0 ∨ d = 1k:ℕh_least:IsLeast {m | 0 < m ∧ 10 ^ k ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} (10 ^ k)⊢ sInf {m | 0 < m ∧ 10 ^ k ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10 ^ k),
        Nat.digits_of_lt 10 1 (byk:ℕd:ℕhd:d ∈ List.replicate k 0 ++ Nat.digits 10 1h10k:10 ^ k = 10 ^ k * 1⊢ 1 ≠ 0k:ℕd:ℕhd:d ∈ List.replicate k 0 ++ [1]h10k:10 ^ k = 10 ^ k * 1⊢ d = 0 ∨ d = 1k:ℕh_least:IsLeast {m | 0 < m ∧ 10 ^ k ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} (10 ^ k)⊢ sInf {m | 0 < m ∧ 10 ^ k ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10 ^ k decideAll goals completed! 🐙k:ℕd:ℕhd:d ∈ List.replicate k 0 ++ [1]h10k:10 ^ k = 10 ^ k * 1⊢ d = 0 ∨ d = 1k:ℕh_least:IsLeast {m | 0 < m ∧ 10 ^ k ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} (10 ^ k)⊢ sInf {m | 0 < m ∧ 10 ^ k ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10 ^ k) (byk:ℕd:ℕhd:d ∈ List.replicate k 0 ++ Nat.digits 10 1h10k:10 ^ k = 10 ^ k * 1⊢ 1 < 10k:ℕd:ℕhd:d ∈ List.replicate k 0 ++ [1]h10k:10 ^ k = 10 ^ k * 1⊢ d = 0 ∨ d = 1k:ℕh_least:IsLeast {m | 0 < m ∧ 10 ^ k ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} (10 ^ k)⊢ sInf {m | 0 < m ∧ 10 ^ k ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10 ^ k decideAll goals completed! 🐙k:ℕd:ℕhd:d ∈ List.replicate k 0 ++ [1]h10k:10 ^ k = 10 ^ k * 1⊢ d = 0 ∨ d = 1k:ℕh_least:IsLeast {m | 0 < m ∧ 10 ^ k ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} (10 ^ k)⊢ sInf {m | 0 < m ∧ 10 ^ k ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10 ^ k)] at hdk:ℕd:ℕhd:d ∈ List.replicate k 0 ++ [1]h10k:10 ^ k = 10 ^ k * 1⊢ d = 0 ∨ d = 1k:ℕh_least:IsLeast {m | 0 < m ∧ 10 ^ k ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} (10 ^ k)⊢ sInf {m | 0 < m ∧ 10 ^ k ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10 ^ k
    simp only [List.mem_append, List.mem_replicate, List.mem_singleton] at hdk:ℕd:ℕh10k:10 ^ k = 10 ^ k * 1hd:k ≠ 0 ∧ d = 0 ∨ d = 1⊢ d = 0 ∨ d = 1k:ℕh_least:IsLeast {m | 0 < m ∧ 10 ^ k ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} (10 ^ k)⊢ sInf {m | 0 < m ∧ 10 ^ k ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10 ^ k
    rcases hd with ⟨-, rfl⟩ | rflinlk:ℕh10k:10 ^ k = 10 ^ k * 1⊢ 0 = 0 ∨ 0 = 1inrk:ℕh10k:10 ^ k = 10 ^ k * 1⊢ 1 = 0 ∨ 1 = 1k:ℕh_least:IsLeast {m | 0 < m ∧ 10 ^ k ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} (10 ^ k)⊢ sInf {m | 0 < m ∧ 10 ^ k ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10 ^ k
    ·inlk:ℕh10k:10 ^ k = 10 ^ k * 1⊢ 0 = 0 ∨ 0 = 1k:ℕh_least:IsLeast {m | 0 < m ∧ 10 ^ k ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} (10 ^ k)⊢ sInf {m | 0 < m ∧ 10 ^ k ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10 ^ k exact Or.inl rflAll goals completed! 🐙k:ℕh_least:IsLeast {m | 0 < m ∧ 10 ^ k ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} (10 ^ k)⊢ sInf {m | 0 < m ∧ 10 ^ k ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10 ^ k
    ·inrk:ℕh10k:10 ^ k = 10 ^ k * 1⊢ 1 = 0 ∨ 1 = 1k:ℕh_least:IsLeast {m | 0 < m ∧ 10 ^ k ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} (10 ^ k)⊢ sInf {m | 0 < m ∧ 10 ^ k ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10 ^ k exact Or.inr rflk:ℕh_least:IsLeast {m | 0 < m ∧ 10 ^ k ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} (10 ^ k)⊢ sInf {m | 0 < m ∧ 10 ^ k ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10 ^ kk:ℕh_least:IsLeast {m | 0 < m ∧ 10 ^ k ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} (10 ^ k)⊢ sInf {m | 0 < m ∧ 10 ^ k ∣ m ∧ ∀ d ∈ Nat.digits 10 m, d = 0 ∨ d = 1} = 10 ^ k
  exact h_least.csInf_eqAll goals completed! 🐙

It is known that $a(10^k - 1) = (10^{9k} - 1) / 9$ for all $k$. Is $a(n) < a(10^k - 1)$ for all $n < 10^k - 1$?

David Radcliffe, Aug 01 2025

@[category research open, AMS 11]
theorem conjecture (k : ℕ) :
    ∀ n < 10 ^ k - 1, a n < a (10 ^ k - 1) := byk:ℕ⊢ ∀ n < 10 ^ k - 1, OeisA4290.a n < OeisA4290.a (10 ^ k - 1)
  sorryAll goals completed! 🐙

end OeisA4290