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

State before:
d a b : ℕ
inst✝ : NeZero d
⊢ ∃ I, feasible d I ∧ mem a b I
Tactic:
obtain ⟨n, rfl⟩ := Nat.exists_eq_succ_of_ne_zero (NeZero.ne d)
State after:
case intro
a b n : ℕ
inst✝ : NeZero (Nat.succ n)
⊢ ∃ I, feasible (Nat.succ n) I ∧ mem a b I

State before:
case intro
a b n : ℕ
inst✝ : NeZero (Nat.succ n)
⊢ ∃ I, feasible (Nat.succ n) I ∧ mem a b I
Tactic:
induction' n with n ih
State after:
case intro.zero
a b n : ℕ
inst✝ : NeZero (Nat.succ n)
⊢ ∃ I, feasible (Nat.succ Nat.zero) I ∧ mem a b I

case intro.succ
a b n✝ : ℕ
inst✝ : NeZero (Nat.succ n✝)
n : ℕ
ih : ∃ I, feasible (Nat.succ n) I ∧ mem a b I
⊢ ∃ I, feasible (Nat.succ (Nat.succ n)) I ∧ mem a b I

State before:
case intro.zero
a b n : ℕ
inst✝ : NeZero (Nat.succ n)
⊢ ∃ I, feasible (Nat.succ Nat.zero) I ∧ mem a b I
Tactic:
exact ⟨base, feasible_base, mem_base _ _⟩
State after:
no goals

State before:
case intro.succ
a b n✝ : ℕ
inst✝ : NeZero (Nat.succ n✝)
n : ℕ
ih : ∃ I, feasible (Nat.succ n) I ∧ mem a b I
⊢ ∃ I, feasible (Nat.succ (Nat.succ n)) I ∧ mem a b I
Tactic:
obtain ⟨I', hf, hm⟩ := ih
State after:
case intro.succ.intro.intro
a b n✝ : ℕ
inst✝ : NeZero (Nat.succ n✝)
n : ℕ
I' : BasicInterval
hf : feasible (Nat.succ n) I'
hm : mem a b I'
⊢ ∃ I, feasible (Nat.succ (Nat.succ n)) I ∧ mem a b I

State before:
case intro.succ.intro.intro.inl
a b n✝ : ℕ
inst✝ : NeZero (Nat.succ n✝)
n : ℕ
I' : BasicInterval
hf : feasible (Nat.succ n) I'
hm : mem a b I'
h : feasible (Nat.succ (Nat.succ n)) I'
⊢ ∃ I, feasible (Nat.succ (Nat.succ n)) I ∧ mem a b I
Tactic:
exact ⟨I', h, hm⟩
State after:
no goals

State before:
case intro.succ.intro.intro.inr
a b n✝ : ℕ
inst✝ : NeZero (Nat.succ n✝)
n : ℕ
I' : BasicInterval
hf : feasible (Nat.succ n) I'
hm : mem a b I'
h : feasible (Nat.succ (Nat.succ n)) (left I') ∧ feasible (Nat.succ (Nat.succ n)) (right I')
⊢ ∃ I, feasible (Nat.succ (Nat.succ n)) I ∧ mem a b I
Tactic:
rcases mem_left_or_mem_right I' hm with hm | hm
State after:
case intro.succ.intro.intro.inr.inl
a b n✝ : ℕ
inst✝ : NeZero (Nat.succ n✝)
n : ℕ
I' : BasicInterval
hf : feasible (Nat.succ n) I'
hm✝ : mem a b I'
h : feasible (Nat.succ (Nat.succ n)) (left I') ∧ feasible (Nat.succ (Nat.succ n)) (right I')
hm : mem a b (left I')
⊢ ∃ I, feasible (Nat.succ (Nat.succ n)) I ∧ mem a b I

case intro.succ.intro.intro.inr.inr
a b n✝ : ℕ
inst✝ : NeZero (Nat.succ n✝)
n : ℕ
I' : BasicInterval
hf : feasible (Nat.succ n) I'
hm✝ : mem a b I'
h : feasible (Nat.succ (Nat.succ n)) (left I') ∧ feasible (Nat.succ (Nat.succ n)) (right I')
hm : mem a b (right I')
⊢ ∃ I, feasible (Nat.succ (Nat.succ n)) I ∧ mem a b I

State before:
case intro.succ.intro.intro.inr.inl
a b n✝ : ℕ
inst✝ : NeZero (Nat.succ n✝)
n : ℕ
I' : BasicInterval
hf : feasible (Nat.succ n) I'
hm✝ : mem a b I'
h : feasible (Nat.succ (Nat.succ n)) (left I') ∧ feasible (Nat.succ (Nat.succ n)) (right I')
hm : mem a b (left I')
⊢ ∃ I, feasible (Nat.succ (Nat.succ n)) I ∧ mem a b I
Tactic:
exact ⟨I'.left, h.1, hm⟩
State after:
no goals

State before:
case intro.succ.intro.intro.inr.inr
a b n✝ : ℕ
inst✝ : NeZero (Nat.succ n✝)
n : ℕ
I' : BasicInterval
hf : feasible (Nat.succ n) I'
hm✝ : mem a b I'
h : feasible (Nat.succ (Nat.succ n)) (left I') ∧ feasible (Nat.succ (Nat.succ n)) (right I')
hm : mem a b (right I')
⊢ ∃ I, feasible (Nat.succ (Nat.succ n)) I ∧ mem a b I
Tactic:
exact ⟨I'.right, h.2, hm⟩
State after:
no goals