Can we avoid nesting when using by_cases?

Stream: new members

[Nathan]

Can we avoid nesting when using by_cases?

example (n : ℕ) : n > 0 := by
  by_cases (n > 100)
  · sorry
  · by_cases (n > 70)
    · sorry
    · by_cases (n > 50)
      · sorry
      · by_cases (n > 30)
        · sorry
        · sorry

[Ruben Van de Velde]

Nathan said:

Can we avoid nesting when using by_cases?

example (n : ℕ) : n > 0 := by
  by_cases (n > 100)
  · sorry
  by_cases (n > 70)
  · sorry
  by_cases (n > 50)
  · sorry
  by_cases (n > 30)
  · sorry
  sorry

[Kevin Buzzard]

import Mathlib

example (n : ℕ) : n > 0 := by
  obtain h | h | h | h | h : (n > 100) ∨ (n > 70 ∧ n ≤ 100) ∨ (n > 50 ∧ n ≤ 70) ∨ (n > 30 ∧ n ≤ 50) ∨ (n ≤ 30):= by omega
  · sorry
  · sorry
  · sorry
  · sorry
  · sorry

[Nathan]

thanks :pray: these look interesting