Theorem: Weight.BasicInterval.feasible_left_or_right (Weights/BasicInterval.lean)

State before:
d : ℕ
I : BasicInterval
h : feasible d I
⊢ feasible (Nat.succ d) I ∨ feasible (Nat.succ d) (left I) ∧ feasible (Nat.succ d) (right I)
Tactic:
by_cases h' : I.feasible d.succ
State after:
case pos
d : ℕ
I : BasicInterval
h : feasible d I
h' : feasible (Nat.succ d) I
⊢ feasible (Nat.succ d) I ∨ feasible (Nat.succ d) (left I) ∧ feasible (Nat.succ d) (right I)

case neg
d : ℕ
I : BasicInterval
h : feasible d I
h' : ¬feasible (Nat.succ d) I
⊢ feasible (Nat.succ d) I ∨ feasible (Nat.succ d) (left I) ∧ feasible (Nat.succ d) (right I)

State before:
case pos
d : ℕ
I : BasicInterval
h : feasible d I
h' : feasible (Nat.succ d) I
⊢ feasible (Nat.succ d) I ∨ feasible (Nat.succ d) (left I) ∧ feasible (Nat.succ d) (right I)
Tactic:
exact Or.inl h'
State after:
no goals

State before:
case neg
d : ℕ
I : BasicInterval
h : feasible d I
h' : ¬feasible (Nat.succ d) I
⊢ feasible (Nat.succ d) I ∨ feasible (Nat.succ d) (left I) ∧ feasible (Nat.succ d) (right I)
Tactic:
simp only [feasible] at h h' ⊢
State after:
case neg
d : ℕ
I : BasicInterval
h : I.a₁ + I.b₁ ≤ d ∧ I.a₂ + I.b₂ ≤ d ∧ d < I.a₁ + I.a₂ + I.b₁ + I.b₂
h' : ¬(I.a₁ + I.b₁ ≤ Nat.succ d ∧ I.a₂ + I.b₂ ≤ Nat.succ d ∧ Nat.succ d < I.a₁ + I.a₂ + I.b₁ + I.b₂)
⊢ I.a₁ + I.b₁ ≤ Nat.succ d ∧ I.a₂ + I.b₂ ≤ Nat.succ d ∧ Nat.succ d < I.a₁ + I.a₂ + I.b₁ + I.b₂ ∨
    ((left I).a₁ + (left I).b₁ ≤ Nat.succ d ∧
        (left I).a₂ + (left I).b₂ ≤ Nat.succ d ∧ Nat.succ d < (left I).a₁ + (left I).a₂ + (left I).b₁ + (left I).b₂) ∧
      (right I).a₁ + (right I).b₁ ≤ Nat.succ d ∧
        (right I).a₂ + (right I).b₂ ≤ Nat.succ d ∧
          Nat.succ d < (right I).a₁ + (right I).a₂ + (right I).b₁ + (right I).b₂

State before:
case neg
d : ℕ
I : BasicInterval
h : I.a₁ + I.b₁ ≤ d ∧ I.a₂ + I.b₂ ≤ d ∧ d < I.a₁ + I.a₂ + I.b₁ + I.b₂
h' : ¬(I.a₁ + I.b₁ ≤ Nat.succ d ∧ I.a₂ + I.b₂ ≤ Nat.succ d ∧ Nat.succ d < I.a₁ + I.a₂ + I.b₁ + I.b₂)
⊢ I.a₁ + I.b₁ ≤ Nat.succ d ∧ I.a₂ + I.b₂ ≤ Nat.succ d ∧ Nat.succ d < I.a₁ + I.a₂ + I.b₁ + I.b₂ ∨
    ((left I).a₁ + (left I).b₁ ≤ Nat.succ d ∧
        (left I).a₂ + (left I).b₂ ≤ Nat.succ d ∧ Nat.succ d < (left I).a₁ + (left I).a₂ + (left I).b₁ + (left I).b₂) ∧
      (right I).a₁ + (right I).b₁ ≤ Nat.succ d ∧
        (right I).a₂ + (right I).b₂ ≤ Nat.succ d ∧
          Nat.succ d < (right I).a₁ + (right I).a₂ + (right I).b₁ + (right I).b₂
Tactic:
simp only [not_and_or, not_le, not_lt] at h'
State after:
case neg
d : ℕ
I : BasicInterval
h : I.a₁ + I.b₁ ≤ d ∧ I.a₂ + I.b₂ ≤ d ∧ d < I.a₁ + I.a₂ + I.b₁ + I.b₂
h' : Nat.succ d < I.a₁ + I.b₁ ∨ Nat.succ d < I.a₂ + I.b₂ ∨ I.a₁ + I.a₂ + I.b₁ + I.b₂ ≤ Nat.succ d
⊢ I.a₁ + I.b₁ ≤ Nat.succ d ∧ I.a₂ + I.b₂ ≤ Nat.succ d ∧ Nat.succ d < I.a₁ + I.a₂ + I.b₁ + I.b₂ ∨
    ((left I).a₁ + (left I).b₁ ≤ Nat.succ d ∧
        (left I).a₂ + (left I).b₂ ≤ Nat.succ d ∧ Nat.succ d < (left I).a₁ + (left I).a₂ + (left I).b₁ + (left I).b₂) ∧
      (right I).a₁ + (right I).b₁ ≤ Nat.succ d ∧
        (right I).a₂ + (right I).b₂ ≤ Nat.succ d ∧
          Nat.succ d < (right I).a₁ + (right I).a₂ + (right I).b₁ + (right I).b₂

State before:
case neg
d : ℕ
I : BasicInterval
h : I.a₁ + I.b₁ ≤ d ∧ I.a₂ + I.b₂ ≤ d ∧ d < I.a₁ + I.a₂ + I.b₁ + I.b₂
h' : Nat.succ d < I.a₁ + I.b₁ ∨ Nat.succ d < I.a₂ + I.b₂ ∨ I.a₁ + I.a₂ + I.b₁ + I.b₂ ≤ Nat.succ d
⊢ I.a₁ + I.b₁ ≤ Nat.succ d ∧ I.a₂ + I.b₂ ≤ Nat.succ d ∧ Nat.succ d < I.a₁ + I.a₂ + I.b₁ + I.b₂ ∨
    ((left I).a₁ + (left I).b₁ ≤ Nat.succ d ∧
        (left I).a₂ + (left I).b₂ ≤ Nat.succ d ∧ Nat.succ d < (left I).a₁ + (left I).a₂ + (left I).b₁ + (left I).b₂) ∧
      (right I).a₁ + (right I).b₁ ≤ Nat.succ d ∧
        (right I).a₂ + (right I).b₂ ≤ Nat.succ d ∧
          Nat.succ d < (right I).a₁ + (right I).a₂ + (right I).b₁ + (right I).b₂
Tactic:
rcases h' with _ | _ | _ <;> try exfalso; linarith
State after:
case neg.inr.inr
d : ℕ
I : BasicInterval
h : I.a₁ + I.b₁ ≤ d ∧ I.a₂ + I.b₂ ≤ d ∧ d < I.a₁ + I.a₂ + I.b₁ + I.b₂
h✝ : I.a₁ + I.a₂ + I.b₁ + I.b₂ ≤ Nat.succ d
⊢ I.a₁ + I.b₁ ≤ Nat.succ d ∧ I.a₂ + I.b₂ ≤ Nat.succ d ∧ Nat.succ d < I.a₁ + I.a₂ + I.b₁ + I.b₂ ∨
    ((left I).a₁ + (left I).b₁ ≤ Nat.succ d ∧
        (left I).a₂ + (left I).b₂ ≤ Nat.succ d ∧ Nat.succ d < (left I).a₁ + (left I).a₂ + (left I).b₁ + (left I).b₂) ∧
      (right I).a₁ + (right I).b₁ ≤ Nat.succ d ∧
        (right I).a₂ + (right I).b₂ ≤ Nat.succ d ∧
          Nat.succ d < (right I).a₁ + (right I).a₂ + (right I).b₁ + (right I).b₂

State before:
case neg.inr.inr
d : ℕ
I : BasicInterval
h : I.a₁ + I.b₁ ≤ d ∧ I.a₂ + I.b₂ ≤ d ∧ d < I.a₁ + I.a₂ + I.b₁ + I.b₂
h✝ : I.a₁ + I.a₂ + I.b₁ + I.b₂ ≤ Nat.succ d
⊢ I.a₁ + I.b₁ ≤ Nat.succ d ∧ I.a₂ + I.b₂ ≤ Nat.succ d ∧ Nat.succ d < I.a₁ + I.a₂ + I.b₁ + I.b₂ ∨
    ((left I).a₁ + (left I).b₁ ≤ Nat.succ d ∧
        (left I).a₂ + (left I).b₂ ≤ Nat.succ d ∧ Nat.succ d < (left I).a₁ + (left I).a₂ + (left I).b₁ + (left I).b₂) ∧
      (right I).a₁ + (right I).b₁ ≤ Nat.succ d ∧
        (right I).a₂ + (right I).b₂ ≤ Nat.succ d ∧
          Nat.succ d < (right I).a₁ + (right I).a₂ + (right I).b₁ + (right I).b₂
Tactic:
refine Or.inr ⟨⟨?_, ?_, ?_⟩, ⟨?_, ?_, ?_⟩⟩ <;> simp <;> linarith
State after:
no goals

State before:
case neg.inr.inr
d : ℕ
I : BasicInterval
h : I.a₁ + I.b₁ ≤ d ∧ I.a₂ + I.b₂ ≤ d ∧ d < I.a₁ + I.a₂ + I.b₁ + I.b₂
h✝ : I.a₁ + I.a₂ + I.b₁ + I.b₂ ≤ Nat.succ d
⊢ I.a₁ + I.b₁ ≤ Nat.succ d ∧ I.a₂ + I.b₂ ≤ Nat.succ d ∧ Nat.succ d < I.a₁ + I.a₂ + I.b₁ + I.b₂ ∨
    ((left I).a₁ + (left I).b₁ ≤ Nat.succ d ∧
        (left I).a₂ + (left I).b₂ ≤ Nat.succ d ∧ Nat.succ d < (left I).a₁ + (left I).a₂ + (left I).b₁ + (left I).b₂) ∧
      (right I).a₁ + (right I).b₁ ≤ Nat.succ d ∧
        (right I).a₂ + (right I).b₂ ≤ Nat.succ d ∧
          Nat.succ d < (right I).a₁ + (right I).a₂ + (right I).b₁ + (right I).b₂
Tactic:
exfalso
State after:
case neg.inr.inr
d : ℕ
I : BasicInterval
h : I.a₁ + I.b₁ ≤ d ∧ I.a₂ + I.b₂ ≤ d ∧ d < I.a₁ + I.a₂ + I.b₁ + I.b₂
h✝ : I.a₁ + I.a₂ + I.b₁ + I.b₂ ≤ Nat.succ d
⊢ False

State before:
case neg.inr.inl
d : ℕ
I : BasicInterval
h : I.a₁ + I.b₁ ≤ d ∧ I.a₂ + I.b₂ ≤ d ∧ d < I.a₁ + I.a₂ + I.b₁ + I.b₂
h✝ : Nat.succ d < I.a₂ + I.b₂
⊢ False
Tactic:
linarith
State after:
no goals