Theorem: Nat.exists_or_forall_not (Algdata/Init/Nat.lean)

State before:
p : Nat → Prop
inst✝ : DecidablePred p
n : Nat
⊢ (∃ i, i < n ∧ p i) ∨ ∀ (i : Nat), i < n → ¬p i
Tactic:
induction n
State after:
case zero
p : Nat → Prop
inst✝ : DecidablePred p
⊢ (∃ i, i < zero ∧ p i) ∨ ∀ (i : Nat), i < zero → ¬p i

case succ
p : Nat → Prop
inst✝ : DecidablePred p
n✝ : Nat
n_ih✝ : (∃ i, i < n✝ ∧ p i) ∨ ∀ (i : Nat), i < n✝ → ¬p i
⊢ (∃ i, i < succ n✝ ∧ p i) ∨ ∀ (i : Nat), i < succ n✝ → ¬p i

State before:
p : Nat → Prop
inst✝ : DecidablePred p
⊢ (∃ i, i < zero ∧ p i) ∨ ∀ (i : Nat), i < zero → ¬p i
Tactic:
case zero => exact Or.inr (λ _ h => by cases h)
State after:
no goals

State before:
p : Nat → Prop
inst✝ : DecidablePred p
n : Nat
h_ind : (∃ i, i < n ∧ p i) ∨ ∀ (i : Nat), i < n → ¬p i
⊢ (∃ i, i < succ n ∧ p i) ∨ ∀ (i : Nat), i < succ n → ¬p i
Tactic:
case succ n h_ind =>
  cases h_ind
  case inl hex =>
    cases hex with | intro i hi => exact Or.inl ⟨i, Nat.le.step hi.left, hi.right⟩
  case inr hall =>
    if hpn : p n
    then exact Or.inl ⟨n, n.lt_succ_self, hpn⟩
    else
      apply Or.inr
      intro i hi
      cases hi
      case refl => exact hpn
      case step hstep => exact hall i hstep
State after:
no goals

State before:
p : Nat → Prop
inst✝ : DecidablePred p
⊢ (∃ i, i < zero ∧ p i) ∨ ∀ (i : Nat), i < zero → ¬p i
Tactic:
exact Or.inr (λ _ h => by cases h)
State after:
no goals

State before:
p : Nat → Prop
inst✝ : DecidablePred p
x✝ : Nat
h : x✝ < zero
⊢ ¬p x✝
Tactic:
cases h
State after:
no goals

State before:
p : Nat → Prop
inst✝ : DecidablePred p
n : Nat
h_ind : (∃ i, i < n ∧ p i) ∨ ∀ (i : Nat), i < n → ¬p i
⊢ (∃ i, i < succ n ∧ p i) ∨ ∀ (i : Nat), i < succ n → ¬p i
Tactic:
cases h_ind
State after:
case inl
p : Nat → Prop
inst✝ : DecidablePred p
n : Nat
h✝ : ∃ i, i < n ∧ p i
⊢ (∃ i, i < succ n ∧ p i) ∨ ∀ (i : Nat), i < succ n → ¬p i

case inr
p : Nat → Prop
inst✝ : DecidablePred p
n : Nat
h✝ : ∀ (i : Nat), i < n → ¬p i
⊢ (∃ i, i < succ n ∧ p i) ∨ ∀ (i : Nat), i < succ n → ¬p i

State before:
p : Nat → Prop
inst✝ : DecidablePred p
n : Nat
hex : ∃ i, i < n ∧ p i
⊢ (∃ i, i < succ n ∧ p i) ∨ ∀ (i : Nat), i < succ n → ¬p i
Tactic:
case inl hex =>
  cases hex with | intro i hi => exact Or.inl ⟨i, Nat.le.step hi.left, hi.right⟩
State after:
no goals

State before:
p : Nat → Prop
inst✝ : DecidablePred p
n : Nat
hall : ∀ (i : Nat), i < n → ¬p i
⊢ (∃ i, i < succ n ∧ p i) ∨ ∀ (i : Nat), i < succ n → ¬p i
Tactic:
case inr hall =>
  if hpn : p n
  then exact Or.inl ⟨n, n.lt_succ_self, hpn⟩
  else
    apply Or.inr
    intro i hi
    cases hi
    case refl => exact hpn
    case step hstep => exact hall i hstep
State after:
no goals

State before:
p : Nat → Prop
inst✝ : DecidablePred p
n : Nat
hex : ∃ i, i < n ∧ p i
⊢ (∃ i, i < succ n ∧ p i) ∨ ∀ (i : Nat), i < succ n → ¬p i
Tactic:
cases hex with | intro i hi => exact Or.inl ⟨i, Nat.le.step hi.left, hi.right⟩
State after:
no goals

State before:
case intro
p : Nat → Prop
inst✝ : DecidablePred p
n i : Nat
hi : i < n ∧ p i
⊢ (∃ i, i < succ n ∧ p i) ∨ ∀ (i : Nat), i < succ n → ¬p i
Tactic:
exact Or.inl ⟨i, Nat.le.step hi.left, hi.right⟩
State after:
no goals

State before:
p : Nat → Prop
inst✝ : DecidablePred p
n : Nat
hall : ∀ (i : Nat), i < n → ¬p i
⊢ (∃ i, i < succ n ∧ p i) ∨ ∀ (i : Nat), i < succ n → ¬p i
Tactic:
if hpn : p n
then exact Or.inl ⟨n, n.lt_succ_self, hpn⟩
else
  apply Or.inr
  intro i hi
  cases hi
  case refl => exact hpn
  case step hstep => exact hall i hstep
State after:
no goals

State before:
p : Nat → Prop
inst✝ : DecidablePred p
n : Nat
hall : ∀ (i : Nat), i < n → ¬p i
hpn : p n
⊢ (∃ i, i < succ n ∧ p i) ∨ ∀ (i : Nat), i < succ n → ¬p i
Tactic:
exact Or.inl ⟨n, n.lt_succ_self, hpn⟩
State after:
no goals

State before:
p : Nat → Prop
inst✝ : DecidablePred p
n : Nat
hall : ∀ (i : Nat), i < n → ¬p i
hpn : ¬p n
⊢ (∃ i, i < succ n ∧ p i) ∨ ∀ (i : Nat), i < succ n → ¬p i
Tactic:
apply Or.inr
State after:
case h
p : Nat → Prop
inst✝ : DecidablePred p
n : Nat
hall : ∀ (i : Nat), i < n → ¬p i
hpn : ¬p n
⊢ ∀ (i : Nat), i < succ n → ¬p i

State before:
case h
p : Nat → Prop
inst✝ : DecidablePred p
n : Nat
hall : ∀ (i : Nat), i < n → ¬p i
hpn : ¬p n
⊢ ∀ (i : Nat), i < succ n → ¬p i
Tactic:
intro i hi
State after:
case h
p : Nat → Prop
inst✝ : DecidablePred p
n : Nat
hall : ∀ (i : Nat), i < n → ¬p i
hpn : ¬p n
i : Nat
hi : i < succ n
⊢ ¬p i

State before:
case h
p : Nat → Prop
inst✝ : DecidablePred p
n : Nat
hall : ∀ (i : Nat), i < n → ¬p i
hpn : ¬p n
i : Nat
hi : i < succ n
⊢ ¬p i
Tactic:
cases hi
State after:
case h.refl
p : Nat → Prop
inst✝ : DecidablePred p
n : Nat
hall : ∀ (i : Nat), i < n → ¬p i
hpn : ¬p n
⊢ ¬p n

case h.step
p : Nat → Prop
inst✝ : DecidablePred p
n : Nat
hall : ∀ (i : Nat), i < n → ¬p i
hpn : ¬p n
i : Nat
a✝ : Nat.le (succ i) n
⊢ ¬p i

State before:
p : Nat → Prop
inst✝ : DecidablePred p
n : Nat
hall : ∀ (i : Nat), i < n → ¬p i
hpn : ¬p n
⊢ ¬p n
Tactic:
case refl => exact hpn
State after:
no goals

State before:
p : Nat → Prop
inst✝ : DecidablePred p
n : Nat
hall : ∀ (i : Nat), i < n → ¬p i
hpn : ¬p n
i : Nat
hstep : Nat.le (succ i) n
⊢ ¬p i
Tactic:
case step hstep => exact hall i hstep
State after:
no goals

State before:
p : Nat → Prop
inst✝ : DecidablePred p
n : Nat
hall : ∀ (i : Nat), i < n → ¬p i
hpn : ¬p n
⊢ ¬p n
Tactic:
exact hpn
State after:
no goals

State before:
p : Nat → Prop
inst✝ : DecidablePred p
n : Nat
hall : ∀ (i : Nat), i < n → ¬p i
hpn : ¬p n
i : Nat
hstep : Nat.le (succ i) n
⊢ ¬p i
Tactic:
exact hall i hstep
State after:
no goals