Theorem: verus_lemma_induction_helper (VerusLeanStd/GeneralInternals.lean)

State before:
n : ℤ
f : ℤ → Bool
x : ℤ
h1 : n > 0
h2 : ∀ (i : ℤ), 0 ≤ i ∧ i < n → f i = true
h3 : ∀ (i : ℤ), i ≥ 0 ∧ f i = true → f (i + n) = true
h4 : ∀ (i : ℤ), i < n ∧ f i = true → f (i - n) = true
⊢ f x = true
Tactic:
by_cases h0 : x ≥ 0
State after:
case pos
n : ℤ
f : ℤ → Bool
x : ℤ
h1 : n > 0
h2 : ∀ (i : ℤ), 0 ≤ i ∧ i < n → f i = true
h3 : ∀ (i : ℤ), i ≥ 0 ∧ f i = true → f (i + n) = true
h4 : ∀ (i : ℤ), i < n ∧ f i = true → f (i - n) = true
h0 : x ≥ 0
⊢ f x = true

case neg
n : ℤ
f : ℤ → Bool
x : ℤ
h1 : n > 0
h2 : ∀ (i : ℤ), 0 ≤ i ∧ i < n → f i = true
h3 : ∀ (i : ℤ), i ≥ 0 ∧ f i = true → f (i + n) = true
h4 : ∀ (i : ℤ), i < n ∧ f i = true → f (i - n) = true
h0 : ¬x ≥ 0
⊢ f x = true

State before:
case pos
n : ℤ
f : ℤ → Bool
x : ℤ
h1 : n > 0
h2 : ∀ (i : ℤ), 0 ≤ i ∧ i < n → f i = true
h3 : ∀ (i : ℤ), i ≥ 0 ∧ f i = true → f (i + n) = true
h4 : ∀ (i : ℤ), i < n ∧ f i = true → f (i - n) = true
h0 : x ≥ 0
⊢ f x = true

case neg
n : ℤ
f : ℤ → Bool
x : ℤ
h1 : n > 0
h2 : ∀ (i : ℤ), 0 ≤ i ∧ i < n → f i = true
h3 : ∀ (i : ℤ), i ≥ 0 ∧ f i = true → f (i + n) = true
h4 : ∀ (i : ℤ), i < n ∧ f i = true → f (i - n) = true
h0 : ¬x ≥ 0
⊢ f x = true
Tactic:
. exact verus_lemma_induction_helper_pos n f x h0 h1 h2 h3 h4
State after:
case neg
n : ℤ
f : ℤ → Bool
x : ℤ
h1 : n > 0
h2 : ∀ (i : ℤ), 0 ≤ i ∧ i < n → f i = true
h3 : ∀ (i : ℤ), i ≥ 0 ∧ f i = true → f (i + n) = true
h4 : ∀ (i : ℤ), i < n ∧ f i = true → f (i - n) = true
h0 : ¬x ≥ 0
⊢ f x = true

State before:
case neg
n : ℤ
f : ℤ → Bool
x : ℤ
h1 : n > 0
h2 : ∀ (i : ℤ), 0 ≤ i ∧ i < n → f i = true
h3 : ∀ (i : ℤ), i ≥ 0 ∧ f i = true → f (i + n) = true
h4 : ∀ (i : ℤ), i < n ∧ f i = true → f (i - n) = true
h0 : ¬x ≥ 0
⊢ f x = true
Tactic:
. simp only [ge_iff_le, not_le] at h0
  exact verus_lemma_induction_helper_neg n f x h0 h1 h2 h3 h4
State after:
no goals

State before:
case pos
n : ℤ
f : ℤ → Bool
x : ℤ
h1 : n > 0
h2 : ∀ (i : ℤ), 0 ≤ i ∧ i < n → f i = true
h3 : ∀ (i : ℤ), i ≥ 0 ∧ f i = true → f (i + n) = true
h4 : ∀ (i : ℤ), i < n ∧ f i = true → f (i - n) = true
h0 : x ≥ 0
⊢ f x = true
Tactic:
exact verus_lemma_induction_helper_pos n f x h0 h1 h2 h3 h4
State after:
no goals

State before:
case neg
n : ℤ
f : ℤ → Bool
x : ℤ
h1 : n > 0
h2 : ∀ (i : ℤ), 0 ≤ i ∧ i < n → f i = true
h3 : ∀ (i : ℤ), i ≥ 0 ∧ f i = true → f (i + n) = true
h4 : ∀ (i : ℤ), i < n ∧ f i = true → f (i - n) = true
h0 : ¬x ≥ 0
⊢ f x = true
Tactic:
simp only [ge_iff_le, not_le] at h0
State after:
case neg
n : ℤ
f : ℤ → Bool
x : ℤ
h1 : n > 0
h2 : ∀ (i : ℤ), 0 ≤ i ∧ i < n → f i = true
h3 : ∀ (i : ℤ), i ≥ 0 ∧ f i = true → f (i + n) = true
h4 : ∀ (i : ℤ), i < n ∧ f i = true → f (i - n) = true
h0 : x < 0
⊢ f x = true

State before:
case neg
n : ℤ
f : ℤ → Bool
x : ℤ
h1 : n > 0
h2 : ∀ (i : ℤ), 0 ≤ i ∧ i < n → f i = true
h3 : ∀ (i : ℤ), i ≥ 0 ∧ f i = true → f (i + n) = true
h4 : ∀ (i : ℤ), i < n ∧ f i = true → f (i - n) = true
h0 : x < 0
⊢ f x = true
Tactic:
exact verus_lemma_induction_helper_neg n f x h0 h1 h2 h3 h4
State after:
no goals