internlm/Lean-Github huggingface dataset:
Theorem: caseStrongRecOnOddPrimes
Proof state before:
case ind.inl.inr.intro
p : ℕ → Prop
zero : p 0
two : p 2
not_prime : ∀ (n : ℕ), ¬Nat.Prime (Nat.succ n) → (∀ (x : ℕ), x ≤ n → p x) → p (Nat.succ n)
odd_prime : ∀ (n : ℕ), Nat.Prime (Nat.succ (2 * n)) → (∀ (x : ℕ), x ≤ 2 * n → p x) → p (Nat.succ (2 * n))
k : ℕ
h_ind : ∀ (m : ℕ), m ≤ k → p m
hk_prime : Nat.Prime (Nat.succ k)
m : ℕ
hm : k = 2 * m
⊢ p (Nat.succ k)
Tactic:
simp [hm] at *
Proof state after:
case ind.inl.inr.intro
p : ℕ → Prop
zero : p 0
two : p 2
not_prime : ∀ (n : ℕ), ¬Nat.Prime (Nat.succ n) → (∀ (x : ℕ), x ≤ n → p x) → p (Nat.succ n)
odd_prime : ∀ (n : ℕ), Nat.Prime (Nat.succ (2 * n)) → (∀ (x : ℕ), x ≤ 2 * n → p x) → p (Nat.succ (2 * n))
k m : ℕ
h_ind : ∀ (m_1 : ℕ), m_1 ≤ 2 * m → p m_1
hk_prime : Nat.Prime (Nat.succ (2 * m))
hm : True
⊢ p (Nat.succ (2 * m))
Theorem: caseStrongRecOnOddPrimes
Proof state before:
case ind.inl.inr.intro
p : ℕ → Prop
zero : p 0
two : p 2
not_prime : ∀ (n : ℕ), ¬Nat.Prime (Nat.succ n) → (∀ (x : ℕ), x ≤ n → p x) → p (Nat.succ n)
odd_prime : ∀ (n : ℕ), Nat.Prime (Nat.succ (2 * n)) → (∀ (x : ℕ), x ≤ 2 * n → p x) → p (Nat.succ (2 * n))
k m : ℕ
h_ind : ∀ (m_1 : ℕ), m_1 ≤ 2 * m → p m_1
hk_prime : Nat.Prime (Nat.succ (2 * m))
hm : True
⊢ p (Nat.succ (2 * m))
Tactic:
apply odd_prime _ hk_prime h_ind
Proof state after:
no goals
Theorem: prodPrimesLePowFour
Proof state before:
n : ℕ
⊢ prodPrimes n ≤ 4 ^ Nat.pred n
Tactic:
induction n using caseStrongRecOnOddPrimes with
| zero => simp
| two => simp
| not_prime n hp hi =>
  specialize hi n
  simp at hi
  cases n with
  | zero => simp
  | succ n =>
    simp only [Nat.pred_succ] at *
    simp [prodPrimes]
    rw [primesSuccEqPrimesSelf hp, Nat.add_one]
    rw [← prodPrimes, Nat.add_one]
    apply le_trans hi
    simp [pow_succ]
| odd_prime n hp hi =>
  simp
  conv => rhs; rw [two_mul, pow_add]
  specialize hi n.succ _
  . cases n with
    | zero => contradiction  | succ n => linarith
  simp at hi
  rw [prodPrimesSplit (by linarith : n.succ ≤ (2*n).succ)]
  apply Nat.mul_le_mul hi
  apply le_trans _ chooseHalfLePowFour
  exact prodPrimesIocLeChoose
Proof state after:
no goals
Theorem: prodPrimesLePowFour
Proof state before:
case zero

⊢ prodPrimes 0 ≤ 4 ^ Nat.pred 0
Tactic:
simp
Proof state after:
no goals
Theorem: prodPrimesLePowFour
Proof state before:
case two

⊢ prodPrimes 2 ≤ 4 ^ Nat.pred 2
Tactic:
simp
Proof state after:
no goals
Theorem: prodPrimesLePowFour
Proof state before:
case not_prime
n : ℕ
hp : ¬Nat.Prime (Nat.succ n)
hi : ∀ (x : ℕ), x ≤ n → prodPrimes x ≤ 4 ^ Nat.pred x
⊢ prodPrimes (Nat.succ n) ≤ 4 ^ Nat.pred (Nat.succ n)
Tactic:
specialize hi n
Proof state after:
case not_prime
n : ℕ
hp : ¬Nat.Prime (Nat.succ n)
hi : n ≤ n → prodPrimes n ≤ 4 ^ Nat.pred n
⊢ prodPrimes (Nat.succ n) ≤ 4 ^ Nat.pred (Nat.succ n)
Theorem: prodPrimesLePowFour
Proof state before:
case not_prime
n : ℕ
hp : ¬Nat.Prime (Nat.succ n)
hi : n ≤ n → prodPrimes n ≤ 4 ^ Nat.pred n
⊢ prodPrimes (Nat.succ n) ≤ 4 ^ Nat.pred (Nat.succ n)
Tactic:
simp at hi
Proof state after:
case not_prime
n : ℕ
hp : ¬Nat.Prime (Nat.succ n)
hi : prodPrimes n ≤ 4 ^ Nat.pred n
⊢ prodPrimes (Nat.succ n) ≤ 4 ^ Nat.pred (Nat.succ n)
Theorem: prodPrimesLePowFour
Proof state before:
case not_prime
n : ℕ
hp : ¬Nat.Prime (Nat.succ n)
hi : prodPrimes n ≤ 4 ^ Nat.pred n
⊢ prodPrimes (Nat.succ n) ≤ 4 ^ Nat.pred (Nat.succ n)
Tactic:
cases n with
| zero => simp
| succ n =>
  simp only [Nat.pred_succ] at *
  simp [prodPrimes]
  rw [primesSuccEqPrimesSelf hp, Nat.add_one]
  rw [← prodPrimes, Nat.add_one]
  apply le_trans hi
  simp [pow_succ]
Proof state after:
no goals
Theorem: prodPrimesLePowFour
Proof state before:
case not_prime.zero
hp : ¬Nat.Prime (Nat.succ Nat.zero)
hi : prodPrimes Nat.zero ≤ 4 ^ Nat.pred Nat.zero
⊢ prodPrimes (Nat.succ Nat.zero) ≤ 4 ^ Nat.pred (Nat.succ Nat.zero)
Tactic:
simp
Proof state after:
no goals
Theorem: prodPrimesLePowFour
Proof state before:
case not_prime.succ
n : ℕ
hp : ¬Nat.Prime (Nat.succ (Nat.succ n))
hi : prodPrimes (Nat.succ n) ≤ 4 ^ Nat.pred (Nat.succ n)
⊢ prodPrimes (Nat.succ (Nat.succ n)) ≤ 4 ^ Nat.pred (Nat.succ (Nat.succ n))
Tactic:
simp only [Nat.pred_succ] at *
Proof state after:
case not_prime.succ
n : ℕ
hp : ¬Nat.Prime (Nat.succ (Nat.succ n))
hi : prodPrimes (Nat.succ n) ≤ 4 ^ n
⊢ prodPrimes (Nat.succ (Nat.succ n)) ≤ 4 ^ (n + 1)
Theorem: prodPrimesLePowFour
Proof state before:
case not_prime.succ
n : ℕ
hp : ¬Nat.Prime (Nat.succ (Nat.succ n))
hi : prodPrimes (Nat.succ n) ≤ 4 ^ n
⊢ prodPrimes (Nat.succ (Nat.succ n)) ≤ 4 ^ (n + 1)
Tactic:
simp [prodPrimes]
Proof state after:
case not_prime.succ
n : ℕ
hp : ¬Nat.Prime (Nat.succ (Nat.succ n))
hi : prodPrimes (Nat.succ n) ≤ 4 ^ n
⊢ ∏ p in primes (Finset.range (Nat.succ (Nat.succ (Nat.succ n)))), p ≤ 4 ^ (n + 1)
Theorem: prodPrimesLePowFour
Proof state before:
case not_prime.succ
n : ℕ
hp : ¬Nat.Prime (Nat.succ (Nat.succ n))
hi : prodPrimes (Nat.succ n) ≤ 4 ^ n
⊢ ∏ p in primes (Finset.range (Nat.succ (Nat.succ (Nat.succ n)))), p ≤ 4 ^ (n + 1)
Tactic:
rw [primesSuccEqPrimesSelf hp, Nat.add_one]
Proof state after:
case not_prime.succ
n : ℕ
hp : ¬Nat.Prime (Nat.succ (Nat.succ n))
hi : prodPrimes (Nat.succ n) ≤ 4 ^ n
⊢ ∏ p in primes (Finset.range (Nat.succ (Nat.succ n))), p ≤ 4 ^ Nat.succ n
Theorem: prodPrimesLePowFour
Proof state before:
case not_prime.succ
n : ℕ
hp : ¬Nat.Prime (Nat.succ (Nat.succ n))
hi : prodPrimes (Nat.succ n) ≤ 4 ^ n
⊢ ∏ p in primes (Finset.range (Nat.succ (Nat.succ n))), p ≤ 4 ^ Nat.succ n
Tactic:
rw [← prodPrimes, Nat.add_one]
Proof state after:
case not_prime.succ
n : ℕ
hp : ¬Nat.Prime (Nat.succ (Nat.succ n))
hi : prodPrimes (Nat.succ n) ≤ 4 ^ n
⊢ prodPrimes (Nat.succ n) ≤ 4 ^ Nat.succ n
Theorem: prodPrimesLePowFour
Proof state before:
case not_prime.succ
n : ℕ
hp : ¬Nat.Prime (Nat.succ (Nat.succ n))
hi : prodPrimes (Nat.succ n) ≤ 4 ^ n
⊢ prodPrimes (Nat.succ n) ≤ 4 ^ Nat.succ n
Tactic:
apply le_trans hi
Proof state after:
case not_prime.succ
n : ℕ
hp : ¬Nat.Prime (Nat.succ (Nat.succ n))
hi : prodPrimes (Nat.succ n) ≤ 4 ^ n
⊢ 4 ^ n ≤ 4 ^ Nat.succ n
Theorem: prodPrimesLePowFour
Proof state before:
case not_prime.succ
n : ℕ
hp : ¬Nat.Prime (Nat.succ (Nat.succ n))
hi : prodPrimes (Nat.succ n) ≤ 4 ^ n
⊢ 4 ^ n ≤ 4 ^ Nat.succ n
Tactic:
simp [pow_succ]
Proof state after:
no goals
Theorem: prodPrimesLePowFour
Proof state before:
case odd_prime
n : ℕ
hp : Nat.Prime (Nat.succ (2 * n))
hi : ∀ (x : ℕ), x ≤ 2 * n → prodPrimes x ≤ 4 ^ Nat.pred x
⊢ prodPrimes (Nat.succ (2 * n)) ≤ 4 ^ Nat.pred (Nat.succ (2 * n))
Tactic:
simp
Proof state after:
case odd_prime
n : ℕ
hp : Nat.Prime (Nat.succ (2 * n))
hi : ∀ (x : ℕ), x ≤ 2 * n → prodPrimes x ≤ 4 ^ Nat.pred x
⊢ prodPrimes (Nat.succ (2 * n)) ≤ 4 ^ (2 * n)
Theorem: prodPrimesLePowFour
Proof state before:
case odd_prime
n : ℕ
hp : Nat.Prime (Nat.succ (2 * n))
hi : ∀ (x : ℕ), x ≤ 2 * n → prodPrimes x ≤ 4 ^ Nat.pred x
⊢ prodPrimes (Nat.succ (2 * n)) ≤ 4 ^ (2 * n)
Tactic:
conv => rhs; rw [two_mul, pow_add]
Proof state after:
case odd_prime
n : ℕ
hp : Nat.Prime (Nat.succ (2 * n))
hi : ∀ (x : ℕ), x ≤ 2 * n → prodPrimes x ≤ 4 ^ Nat.pred x
⊢ prodPrimes (Nat.succ (2 * n)) ≤ 4 ^ n * 4 ^ n
Theorem: prodPrimesLePowFour
Proof state before:
case odd_prime
n : ℕ
hp : Nat.Prime (Nat.succ (2 * n))
hi : ∀ (x : ℕ), x ≤ 2 * n → prodPrimes x ≤ 4 ^ Nat.pred x
⊢ prodPrimes (Nat.succ (2 * n)) ≤ 4 ^ n * 4 ^ n
Tactic:
specialize hi n.succ _
Proof state after:
case odd_prime
n : ℕ
hp : Nat.Prime (Nat.succ (2 * n))
hi : ∀ (x : ℕ), x ≤ 2 * n → prodPrimes x ≤ 4 ^ Nat.pred x
⊢ Nat.succ n ≤ 2 * n

case odd_prime
n : ℕ
hp : Nat.Prime (Nat.succ (2 * n))
hi : prodPrimes (Nat.succ n) ≤ 4 ^ Nat.pred (Nat.succ n)
⊢ prodPrimes (Nat.succ (2 * n)) ≤ 4 ^ n * 4 ^ n
Theorem: prodPrimesLePowFour
Proof state before:
case odd_prime
n : ℕ
hp : Nat.Prime (Nat.succ (2 * n))
hi : ∀ (x : ℕ), x ≤ 2 * n → prodPrimes x ≤ 4 ^ Nat.pred x
⊢ Nat.succ n ≤ 2 * n

case odd_prime
n : ℕ
hp : Nat.Prime (Nat.succ (2 * n))
hi : prodPrimes (Nat.succ n) ≤ 4 ^ Nat.pred (Nat.succ n)
⊢ prodPrimes (Nat.succ (2 * n)) ≤ 4 ^ n * 4 ^ n
Tactic:
. cases n with
  | zero => contradiction  | succ n => linarith
Proof state after:
case odd_prime
n : ℕ
hp : Nat.Prime (Nat.succ (2 * n))
hi : prodPrimes (Nat.succ n) ≤ 4 ^ Nat.pred (Nat.succ n)
⊢ prodPrimes (Nat.succ (2 * n)) ≤ 4 ^ n * 4 ^ n
Theorem: prodPrimesLePowFour
Proof state before:
case odd_prime
n : ℕ
hp : Nat.Prime (Nat.succ (2 * n))
hi : prodPrimes (Nat.succ n) ≤ 4 ^ Nat.pred (Nat.succ n)
⊢ prodPrimes (Nat.succ (2 * n)) ≤ 4 ^ n * 4 ^ n
Tactic:
simp at hi
Proof state after:
case odd_prime
n : ℕ
hp : Nat.Prime (Nat.succ (2 * n))
hi : prodPrimes (Nat.succ n) ≤ 4 ^ n
⊢ prodPrimes (Nat.succ (2 * n)) ≤ 4 ^ n * 4 ^ n
Theorem: prodPrimesLePowFour
Proof state before:
case odd_prime
n : ℕ
hp : Nat.Prime (Nat.succ (2 * n))
hi : prodPrimes (Nat.succ n) ≤ 4 ^ n
⊢ prodPrimes (Nat.succ (2 * n)) ≤ 4 ^ n * 4 ^ n
Tactic:
rw [prodPrimesSplit (by linarith : n.succ ≤ (2*n).succ)]
Proof state after:
case odd_prime
n : ℕ
hp : Nat.Prime (Nat.succ (2 * n))
hi : prodPrimes (Nat.succ n) ≤ 4 ^ n
⊢ prodPrimes (Nat.succ n) * ∏ p in primes (Finset.Ioc (Nat.succ n) (Nat.succ (2 * n))), p ≤ 4 ^ n * 4 ^ n
Theorem: prodPrimesLePowFour
Proof state before:
case odd_prime
n : ℕ
hp : Nat.Prime (Nat.succ (2 * n))
hi : prodPrimes (Nat.succ n) ≤ 4 ^ n
⊢ prodPrimes (Nat.succ n) * ∏ p in primes (Finset.Ioc (Nat.succ n) (Nat.succ (2 * n))), p ≤ 4 ^ n * 4 ^ n
Tactic:
apply Nat.mul_le_mul hi
Proof state after:
case odd_prime
n : ℕ
hp : Nat.Prime (Nat.succ (2 * n))
hi : prodPrimes (Nat.succ n) ≤ 4 ^ n
⊢ ∏ p in primes (Finset.Ioc (Nat.succ n) (Nat.succ (2 * n))), p ≤ 4 ^ n
Theorem: prodPrimesLePowFour
Proof state before:
case odd_prime
n : ℕ
hp : Nat.Prime (Nat.succ (2 * n))
hi : prodPrimes (Nat.succ n) ≤ 4 ^ n
⊢ ∏ p in primes (Finset.Ioc (Nat.succ n) (Nat.succ (2 * n))), p ≤ 4 ^ n
Tactic:
apply le_trans _ chooseHalfLePowFour
Proof state after:
n : ℕ
hp : Nat.Prime (Nat.succ (2 * n))
hi : prodPrimes (Nat.succ n) ≤ 4 ^ n
⊢ ∏ p in primes (Finset.Ioc (Nat.succ n) (Nat.succ (2 * n))), p ≤ Nat.choose (2 * n + 1) n
Theorem: prodPrimesLePowFour
Proof state before:
n : ℕ
hp : Nat.Prime (Nat.succ (2 * n))
hi : prodPrimes (Nat.succ n) ≤ 4 ^ n
⊢ ∏ p in primes (Finset.Ioc (Nat.succ n) (Nat.succ (2 * n))), p ≤ Nat.choose (2 * n + 1) n
Tactic:
exact prodPrimesIocLeChoose
Proof state after:
no goals
Theorem: prodPrimesLePowFour
Proof state before:
case odd_prime
n : ℕ
hp : Nat.Prime (Nat.succ (2 * n))
hi : ∀ (x : ℕ), x ≤ 2 * n → prodPrimes x ≤ 4 ^ Nat.pred x
⊢ Nat.succ n ≤ 2 * n
Tactic:
cases n with
| zero => contradiction  | succ n => linarith
Proof state after:
no goals
Theorem: prodPrimesLePowFour
Proof state before:
case odd_prime.zero
hp : Nat.Prime (Nat.succ (2 * Nat.zero))
hi : ∀ (x : ℕ), x ≤ 2 * Nat.zero → prodPrimes x ≤ 4 ^ Nat.pred x
⊢ Nat.succ Nat.zero ≤ 2 * Nat.zero
Tactic:
contradiction
Proof state after:
no goals
Theorem: prodPrimesLePowFour
Proof state before:
case odd_prime.succ
n : ℕ
hp : Nat.Prime (Nat.succ (2 * Nat.succ n))
hi : ∀ (x : ℕ), x ≤ 2 * Nat.succ n → prodPrimes x ≤ 4 ^ Nat.pred x
⊢ Nat.succ (Nat.succ n) ≤ 2 * Nat.succ n
Tactic:
linarith
Proof state after:
no goals
Theorem: prodPrimesLePowFour
Proof state before:
n : ℕ
hp : Nat.Prime (Nat.succ (2 * n))
hi : prodPrimes (Nat.succ n) ≤ 4 ^ n
⊢ Nat.succ n ≤ Nat.succ (2 * n)
Tactic:
linarith
Proof state after:
no goals
Theorem: prodPrimesRealLePowFour
Proof state before:
x : ℝ
hx : 1 ≤ x
⊢ ↑(prodPrimes ⌊x⌋₊) ≤ ↑(4 ^ (⌊x⌋₊ - 1))
Tactic:
norm_cast
Proof state after:
x : ℝ
hx : 1 ≤ x
⊢ prodPrimes ⌊x⌋₊ ≤ 4 ^ (⌊x⌋₊ - 1)
Theorem: prodPrimesRealLePowFour
Proof state before:
x : ℝ
hx : 1 ≤ x
⊢ prodPrimes ⌊x⌋₊ ≤ 4 ^ (⌊x⌋₊ - 1)
Tactic:
apply prodPrimesLePowFour
Proof state after:
no goals
Theorem: prodPrimesRealLePowFour
Proof state before:
x : ℝ
hx : 1 ≤ x
⊢ ↑(4 ^ (⌊x⌋₊ - 1)) = 4 ^ ↑(⌊x⌋₊ - 1)
Tactic:
norm_cast
Proof state after:
no goals
Theorem: prodPrimesRealLePowFour
Proof state before:
x : ℝ
hx : 1 ≤ x
⊢ 4 ^ ↑(⌊x⌋₊ - 1) ≤ 4 ^ (x - 1)
Tactic:
rw [Real.rpow_le_rpow_left_iff (by norm_num)]
Proof state after:
x : ℝ
hx : 1 ≤ x
⊢ ↑(⌊x⌋₊ - 1) ≤ x - 1
Theorem: prodPrimesRealLePowFour
Proof state before:
x : ℝ
hx : 1 ≤ x
⊢ ↑(⌊x⌋₊ - 1) ≤ x - 1
Tactic:
rw [← Nat.floor_sub_one]
Proof state after:
x : ℝ
hx : 1 ≤ x
⊢ ↑⌊x - 1⌋₊ ≤ x - 1
Theorem: prodPrimesRealLePowFour
Proof state before:
x : ℝ
hx : 1 ≤ x
⊢ ↑⌊x - 1⌋₊ ≤ x - 1
Tactic:
apply Nat.floor_le
Proof state after:
case ha
x : ℝ
hx : 1 ≤ x
⊢ 0 ≤ x - 1
Theorem: prodPrimesRealLePowFour
Proof state before:
case ha
x : ℝ
hx : 1 ≤ x
⊢ 0 ≤ x - 1
Tactic:
linarith
Proof state after:
no goals
Theorem: prodPrimesRealLePowFour
Proof state before:
x : ℝ
hx : 1 ≤ x
⊢ 1 < 4
Tactic:
norm_num
Proof state after:
no goals
Theorem: allPrimeNums
Proof state before:
⊢ List.All₂ Nat.Prime nums
Tactic:
simp (config := {decide := false}) [nums]
Proof state after:
⊢ Nat.Prime 2 ∧
    Nat.Prime 3 ∧
      Nat.Prime 5 ∧
        Nat.Prime 7 ∧
          Nat.Prime 13 ∧
            Nat.Prime 23 ∧
              Nat.Prime 43 ∧
                Nat.Prime 83 ∧
                  Nat.Prime 163 ∧ Nat.Prime 317 ∧ Nat.Prime 631 ∧ Nat.Prime 1259 ∧ Nat.Prime 2503 ∧ Nat.Prime 4001
Theorem: allPrimeNums
Proof state before:
⊢ Nat.Prime 2 ∧
    Nat.Prime 3 ∧
      Nat.Prime 5 ∧
        Nat.Prime 7 ∧
          Nat.Prime 13 ∧
            Nat.Prime 23 ∧
              Nat.Prime 43 ∧
                Nat.Prime 83 ∧
                  Nat.Prime 163 ∧ Nat.Prime 317 ∧ Nat.Prime 631 ∧ Nat.Prime 1259 ∧ Nat.Prime 2503 ∧ Nat.Prime 4001
Tactic:
norm_num1
Proof state after:
⊢ True ∧ True ∧ True ∧ True ∧ True ∧ True ∧ True ∧ True ∧ True ∧ True ∧ True ∧ True ∧ True ∧ True
Theorem: allPrimeNums
Proof state before:
⊢ True ∧ True ∧ True ∧ True ∧ True ∧ True ∧ True ∧ True ∧ True ∧ True ∧ True ∧ True ∧ True ∧ True
Tactic:
simp
Proof state after:
no goals
Theorem: existsOfSlowMono
Proof state before:
a b : ℕ
l : List ℕ
hl_mono : List.Chain (fun u v => u < v) a l
hl_slow : List.Chain (fun u v => v ≤ 2 * u) a l
hl_cons : l ≠ []
hb : b < List.getLast l hl_cons
⊢ ∀ (n : ℕ), n ∈ Set.Icc a b → ∃ lᵢ, lᵢ ∈ l ∧ lᵢ ∈ Set.Ioc n (2 * n)
Tactic:
cases l with
| nil => contradiction
| cons x l =>
  induction l generalizing a x with
  | nil =>
    intro n hn
    simp at *
    apply And.intro <;> linarith
  | cons y l h =>
    rw [List.chain_cons] at hl_mono
    rw [List.chain_cons] at hl_slow
    simp at hb
    specialize @h x y hl_mono.right hl_slow.right (List.cons_ne_nil y l) hb
    intro n hn
    specialize h n
    have : ∀ lᵢ, lᵢ ∈ x :: y :: l ↔ lᵢ = x ∨ lᵢ ∈ y :: l := by simp
    simp_rw [this]
    simp only [or_and_right]
    rw [exists_or]
    cases le_or_lt x n with
    | inl hx =>
      apply Or.inr
      simp only [Set.mem_Ico] at *
      specialize h (And.intro hx hn.right)
      exact h
    | inr hx =>
      apply Or.inl
      simp at *
      apply And.intro <;> linarith
Proof state after:
no goals
Theorem: existsOfSlowMono
Proof state before:
case nil
a b : ℕ
hl_mono : List.Chain (fun u v => u < v) a []
hl_slow : List.Chain (fun u v => v ≤ 2 * u) a []
hl_cons : [] ≠ []
hb : b < List.getLast [] hl_cons
⊢ ∀ (n : ℕ), n ∈ Set.Icc a b → ∃ lᵢ, lᵢ ∈ [] ∧ lᵢ ∈ Set.Ioc n (2 * n)
Tactic:
contradiction
Proof state after:
no goals
Theorem: existsOfSlowMono
Proof state before:
case cons
a b x : ℕ
l : List ℕ
hl_mono : List.Chain (fun u v => u < v) a (x :: l)
hl_slow : List.Chain (fun u v => v ≤ 2 * u) a (x :: l)
hl_cons : x :: l ≠ []
hb : b < List.getLast (x :: l) hl_cons
⊢ ∀ (n : ℕ), n ∈ Set.Icc a b → ∃ lᵢ, lᵢ ∈ x :: l ∧ lᵢ ∈ Set.Ioc n (2 * n)
Tactic:
induction l generalizing a x with
| nil =>
  intro n hn
  simp at *
  apply And.intro <;> linarith
| cons y l h =>
  rw [List.chain_cons] at hl_mono
  rw [List.chain_cons] at hl_slow
  simp at hb
  specialize @h x y hl_mono.right hl_slow.right (List.cons_ne_nil y l) hb
  intro n hn
  specialize h n
  have : ∀ lᵢ, lᵢ ∈ x :: y :: l ↔ lᵢ = x ∨ lᵢ ∈ y :: l := by simp
  simp_rw [this]
  simp only [or_and_right]
  rw [exists_or]
  cases le_or_lt x n with
  | inl hx =>
    apply Or.inr
    simp only [Set.mem_Ico] at *
    specialize h (And.intro hx hn.right)
    exact h
  | inr hx =>
    apply Or.inl
    simp at *
    apply And.intro <;> linarith
Proof state after:
no goals
Theorem: existsOfSlowMono
Proof state before:
case cons.nil
b a x : ℕ
hl_mono : List.Chain (fun u v => u < v) a [x]
hl_slow : List.Chain (fun u v => v ≤ 2 * u) a [x]
hl_cons : [x] ≠ []
hb : b < List.getLast [x] hl_cons
⊢ ∀ (n : ℕ), n ∈ Set.Icc a b → ∃ lᵢ, lᵢ ∈ [x] ∧ lᵢ ∈ Set.Ioc n (2 * n)
Tactic:
intro n hn
Proof state after:
case cons.nil
b a x : ℕ
hl_mono : List.Chain (fun u v => u < v) a [x]
hl_slow : List.Chain (fun u v => v ≤ 2 * u) a [x]
hl_cons : [x] ≠ []
hb : b < List.getLast [x] hl_cons
n : ℕ
hn : n ∈ Set.Icc a b
⊢ ∃ lᵢ, lᵢ ∈ [x] ∧ lᵢ ∈ Set.Ioc n (2 * n)
Theorem: existsOfSlowMono
Proof state before:
case cons.nil
b a x : ℕ
hl_mono : List.Chain (fun u v => u < v) a [x]
hl_slow : List.Chain (fun u v => v ≤ 2 * u) a [x]
hl_cons : [x] ≠ []
hb : b < List.getLast [x] hl_cons
n : ℕ
hn : n ∈ Set.Icc a b
⊢ ∃ lᵢ, lᵢ ∈ [x] ∧ lᵢ ∈ Set.Ioc n (2 * n)
Tactic:
simp at *
Proof state after:
case cons.nil
b a x : ℕ
hl_cons : [x] ≠ []
hb : b < x
n : ℕ
hl_mono : a < x
hl_slow : x ≤ 2 * a
hn : a ≤ n ∧ n ≤ b
⊢ n < x ∧ x ≤ 2 * n
Theorem: existsOfSlowMono
Proof state before:
case cons.nil
b a x : ℕ
hl_cons : [x] ≠ []
hb : b < x
n : ℕ
hl_mono : a < x
hl_slow : x ≤ 2 * a
hn : a ≤ n ∧ n ≤ b
⊢ n < x ∧ x ≤ 2 * n
Tactic:
apply And.intro <;> linarith
Proof state after:
no goals
Theorem: existsOfSlowMono
Proof state before:
case cons.cons
b y : ℕ
l : List ℕ
h :
  ∀ {a : ℕ} (x : ℕ),
    List.Chain (fun u v => u < v) a (x :: l) →
      List.Chain (fun u v => v ≤ 2 * u) a (x :: l) →
        ∀ (hl_cons : x :: l ≠ []),
          b < List.getLast (x :: l) hl_cons → ∀ (n : ℕ), n ∈ Set.Icc a b → ∃ lᵢ, lᵢ ∈ x :: l ∧ lᵢ ∈ Set.Ioc n (2 * n)
a x : ℕ
hl_mono : List.Chain (fun u v => u < v) a (x :: y :: l)
hl_slow : List.Chain (fun u v => v ≤ 2 * u) a (x :: y :: l)
hl_cons : x :: y :: l ≠ []
hb : b < List.getLast (x :: y :: l) hl_cons
⊢ ∀ (n : ℕ), n ∈ Set.Icc a b → ∃ lᵢ, lᵢ ∈ x :: y :: l ∧ lᵢ ∈ Set.Ioc n (2 * n)
Tactic:
rw [List.chain_cons] at hl_mono
Proof state after:
case cons.cons
b y : ℕ
l : List ℕ
h :
  ∀ {a : ℕ} (x : ℕ),
    List.Chain (fun u v => u < v) a (x :: l) →
      List.Chain (fun u v => v ≤ 2 * u) a (x :: l) →
        ∀ (hl_cons : x :: l ≠ []),
          b < List.getLast (x :: l) hl_cons → ∀ (n : ℕ), n ∈ Set.Icc a b → ∃ lᵢ, lᵢ ∈ x :: l ∧ lᵢ ∈ Set.Ioc n (2 * n)
a x : ℕ
hl_mono : a < x ∧ List.Chain (fun u v => u < v) x (y :: l)
hl_slow : List.Chain (fun u v => v ≤ 2 * u) a (x :: y :: l)
hl_cons : x :: y :: l ≠ []
hb : b < List.getLast (x :: y :: l) hl_cons
⊢ ∀ (n : ℕ), n ∈ Set.Icc a b → ∃ lᵢ, lᵢ ∈ x :: y :: l ∧ lᵢ ∈ Set.Ioc n (2 * n)
Theorem: existsOfSlowMono
Proof state before:
case cons.cons
b y : ℕ
l : List ℕ
h :
  ∀ {a : ℕ} (x : ℕ),
    List.Chain (fun u v => u < v) a (x :: l) →
      List.Chain (fun u v => v ≤ 2 * u) a (x :: l) →
        ∀ (hl_cons : x :: l ≠ []),
          b < List.getLast (x :: l) hl_cons → ∀ (n : ℕ), n ∈ Set.Icc a b → ∃ lᵢ, lᵢ ∈ x :: l ∧ lᵢ ∈ Set.Ioc n (2 * n)
a x : ℕ
hl_mono : a < x ∧ List.Chain (fun u v => u < v) x (y :: l)
hl_slow : List.Chain (fun u v => v ≤ 2 * u) a (x :: y :: l)
hl_cons : x :: y :: l ≠ []
hb : b < List.getLast (x :: y :: l) hl_cons
⊢ ∀ (n : ℕ), n ∈ Set.Icc a b → ∃ lᵢ, lᵢ ∈ x :: y :: l ∧ lᵢ ∈ Set.Ioc n (2 * n)
Tactic:
rw [List.chain_cons] at hl_slow
Proof state after:
case cons.cons
b y : ℕ
l : List ℕ
h :
  ∀ {a : ℕ} (x : ℕ),
    List.Chain (fun u v => u < v) a (x :: l) →
      List.Chain (fun u v => v ≤ 2 * u) a (x :: l) →
        ∀ (hl_cons : x :: l ≠ []),
          b < List.getLast (x :: l) hl_cons → ∀ (n : ℕ), n ∈ Set.Icc a b → ∃ lᵢ, lᵢ ∈ x :: l ∧ lᵢ ∈ Set.Ioc n (2 * n)
a x : ℕ
hl_mono : a < x ∧ List.Chain (fun u v => u < v) x (y :: l)
hl_slow : x ≤ 2 * a ∧ List.Chain (fun u v => v ≤ 2 * u) x (y :: l)
hl_cons : x :: y :: l ≠ []
hb : b < List.getLast (x :: y :: l) hl_cons
⊢ ∀ (n : ℕ), n ∈ Set.Icc a b → ∃ lᵢ, lᵢ ∈ x :: y :: l ∧ lᵢ ∈ Set.Ioc n (2 * n)
Theorem: existsOfSlowMono
Proof state before:
case cons.cons
b y : ℕ
l : List ℕ
h :
  ∀ {a : ℕ} (x : ℕ),
    List.Chain (fun u v => u < v) a (x :: l) →
      List.Chain (fun u v => v ≤ 2 * u) a (x :: l) →
        ∀ (hl_cons : x :: l ≠ []),
          b < List.getLast (x :: l) hl_cons → ∀ (n : ℕ), n ∈ Set.Icc a b → ∃ lᵢ, lᵢ ∈ x :: l ∧ lᵢ ∈ Set.Ioc n (2 * n)
a x : ℕ
hl_mono : a < x ∧ List.Chain (fun u v => u < v) x (y :: l)
hl_slow : x ≤ 2 * a ∧ List.Chain (fun u v => v ≤ 2 * u) x (y :: l)
hl_cons : x :: y :: l ≠ []
hb : b < List.getLast (x :: y :: l) hl_cons
⊢ ∀ (n : ℕ), n ∈ Set.Icc a b → ∃ lᵢ, lᵢ ∈ x :: y :: l ∧ lᵢ ∈ Set.Ioc n (2 * n)
Tactic:
simp at hb
Proof state after:
case cons.cons
b y : ℕ
l : List ℕ
h :
  ∀ {a : ℕ} (x : ℕ),
    List.Chain (fun u v => u < v) a (x :: l) →
      List.Chain (fun u v => v ≤ 2 * u) a (x :: l) →
        ∀ (hl_cons : x :: l ≠ []),
          b < List.getLast (x :: l) hl_cons → ∀ (n : ℕ), n ∈ Set.Icc a b → ∃ lᵢ, lᵢ ∈ x :: l ∧ lᵢ ∈ Set.Ioc n (2 * n)
a x : ℕ
hl_mono : a < x ∧ List.Chain (fun u v => u < v) x (y :: l)
hl_slow : x ≤ 2 * a ∧ List.Chain (fun u v => v ≤ 2 * u) x (y :: l)
hl_cons : x :: y :: l ≠ []
hb : b < List.getLast (y :: l) (_ : ¬y :: l = [])
⊢ ∀ (n : ℕ), n ∈ Set.Icc a b → ∃ lᵢ, lᵢ ∈ x :: y :: l ∧ lᵢ ∈ Set.Ioc n (2 * n)
Theorem: existsOfSlowMono
Proof state before:
case cons.cons
b y : ℕ
l : List ℕ
h :
  ∀ {a : ℕ} (x : ℕ),
    List.Chain (fun u v => u < v) a (x :: l) →
      List.Chain (fun u v => v ≤ 2 * u) a (x :: l) →
        ∀ (hl_cons : x :: l ≠ []),
          b < List.getLast (x :: l) hl_cons → ∀ (n : ℕ), n ∈ Set.Icc a b → ∃ lᵢ, lᵢ ∈ x :: l ∧ lᵢ ∈ Set.Ioc n (2 * n)
a x : ℕ
hl_mono : a < x ∧ List.Chain (fun u v => u < v) x (y :: l)
hl_slow : x ≤ 2 * a ∧ List.Chain (fun u v => v ≤ 2 * u) x (y :: l)
hl_cons : x :: y :: l ≠ []
hb : b < List.getLast (y :: l) (_ : ¬y :: l = [])
⊢ ∀ (n : ℕ), n ∈ Set.Icc a b → ∃ lᵢ, lᵢ ∈ x :: y :: l ∧ lᵢ ∈ Set.Ioc n (2 * n)
Tactic:
specialize @h x y hl_mono.right hl_slow.right (List.cons_ne_nil y l) hb
Proof state after:
case cons.cons
b y : ℕ
l : List ℕ
a x : ℕ
hl_mono : a < x ∧ List.Chain (fun u v => u < v) x (y :: l)
hl_slow : x ≤ 2 * a ∧ List.Chain (fun u v => v ≤ 2 * u) x (y :: l)
hl_cons : x :: y :: l ≠ []
hb : b < List.getLast (y :: l) (_ : ¬y :: l = [])
h : ∀ (n : ℕ), n ∈ Set.Icc x b → ∃ lᵢ, lᵢ ∈ y :: l ∧ lᵢ ∈ Set.Ioc n (2 * n)
⊢ ∀ (n : ℕ), n ∈ Set.Icc a b → ∃ lᵢ, lᵢ ∈ x :: y :: l ∧ lᵢ ∈ Set.Ioc n (2 * n)
Theorem: existsOfSlowMono
Proof state before:
case cons.cons
b y : ℕ
l : List ℕ
a x : ℕ
hl_mono : a < x ∧ List.Chain (fun u v => u < v) x (y :: l)
hl_slow : x ≤ 2 * a ∧ List.Chain (fun u v => v ≤ 2 * u) x (y :: l)
hl_cons : x :: y :: l ≠ []
hb : b < List.getLast (y :: l) (_ : ¬y :: l = [])
h : ∀ (n : ℕ), n ∈ Set.Icc x b → ∃ lᵢ, lᵢ ∈ y :: l ∧ lᵢ ∈ Set.Ioc n (2 * n)
⊢ ∀ (n : ℕ), n ∈ Set.Icc a b → ∃ lᵢ, lᵢ ∈ x :: y :: l ∧ lᵢ ∈ Set.Ioc n (2 * n)
Tactic:
intro n hn
Proof state after:
case cons.cons
b y : ℕ
l : List ℕ
a x : ℕ
hl_mono : a < x ∧ List.Chain (fun u v => u < v) x (y :: l)
hl_slow : x ≤ 2 * a ∧ List.Chain (fun u v => v ≤ 2 * u) x (y :: l)
hl_cons : x :: y :: l ≠ []
hb : b < List.getLast (y :: l) (_ : ¬y :: l = [])
h : ∀ (n : ℕ), n ∈ Set.Icc x b → ∃ lᵢ, lᵢ ∈ y :: l ∧ lᵢ ∈ Set.Ioc n (2 * n)
n : ℕ
hn : n ∈ Set.Icc a b
⊢ ∃ lᵢ, lᵢ ∈ x :: y :: l ∧ lᵢ ∈ Set.Ioc n (2 * n)
Theorem: existsOfSlowMono
Proof state before:
case cons.cons
b y : ℕ
l : List ℕ
a x : ℕ
hl_mono : a < x ∧ List.Chain (fun u v => u < v) x (y :: l)
hl_slow : x ≤ 2 * a ∧ List.Chain (fun u v => v ≤ 2 * u) x (y :: l)
hl_cons : x :: y :: l ≠ []
hb : b < List.getLast (y :: l) (_ : ¬y :: l = [])
h : ∀ (n : ℕ), n ∈ Set.Icc x b → ∃ lᵢ, lᵢ ∈ y :: l ∧ lᵢ ∈ Set.Ioc n (2 * n)
n : ℕ
hn : n ∈ Set.Icc a b
⊢ ∃ lᵢ, lᵢ ∈ x :: y :: l ∧ lᵢ ∈ Set.Ioc n (2 * n)
Tactic:
specialize h n
Proof state after:
case cons.cons
b y : ℕ
l : List ℕ
a x : ℕ
hl_mono : a < x ∧ List.Chain (fun u v => u < v) x (y :: l)
hl_slow : x ≤ 2 * a ∧ List.Chain (fun u v => v ≤ 2 * u) x (y :: l)
hl_cons : x :: y :: l ≠ []
hb : b < List.getLast (y :: l) (_ : ¬y :: l = [])
n : ℕ
hn : n ∈ Set.Icc a b
h : n ∈ Set.Icc x b → ∃ lᵢ, lᵢ ∈ y :: l ∧ lᵢ ∈ Set.Ioc n (2 * n)
⊢ ∃ lᵢ, lᵢ ∈ x :: y :: l ∧ lᵢ ∈ Set.Ioc n (2 * n)