Theorem: ftf_of_ge_8_le_10 (BrownCs22/Homework/Hw9.lean)

State before:
P : ℕ → Prop
n : ℕ
⊢ 8 ≤ n ∧ n ≤ 10 → from_three_five n
Tactic:
intro h
State after:
P : ℕ → Prop
n : ℕ
h : 8 ≤ n ∧ n ≤ 10
⊢ from_three_five n

State before:
P : ℕ → Prop
n : ℕ
h : 8 ≤ n ∧ n ≤ 10
⊢ from_three_five n
Tactic:
eliminate (lt_or_le n 9) with htri9 htri9
State after:
case inl
P : ℕ → Prop
n : ℕ
h : 8 ≤ n ∧ n ≤ 10
htri9 : n < 9
⊢ from_three_five n

case inr
P : ℕ → Prop
n : ℕ
h : 8 ≤ n ∧ n ≤ 10
htri9 : 9 ≤ n
⊢ from_three_five n

State before:
case inl
P : ℕ → Prop
n : ℕ
h : 8 ≤ n ∧ n ≤ 10
htri9 : n < 9
⊢ from_three_five n

case inr
P : ℕ → Prop
n : ℕ
h : 8 ≤ n ∧ n ≤ 10
htri9 : 9 ≤ n
⊢ from_three_five n
Tactic:
{
  sorry
}
State after:
case inr
P : ℕ → Prop
n : ℕ
h : 8 ≤ n ∧ n ≤ 10
htri9 : 9 ≤ n
⊢ from_three_five n

State before:
case inr
P : ℕ → Prop
n : ℕ
h : 8 ≤ n ∧ n ≤ 10
htri9 : 9 ≤ n
⊢ from_three_five n
Tactic:
{
  eliminate (lt_or_le n 10) with htri10 htri10
  {
    sorry
  }
  {
    sorry
  }
}
State after:
no goals

State before:
case inl
P : ℕ → Prop
n : ℕ
h : 8 ≤ n ∧ n ≤ 10
htri9 : n < 9
⊢ from_three_five n
Tactic:
sorry
State after:
no goals

State before:
case inr
P : ℕ → Prop
n : ℕ
h : 8 ≤ n ∧ n ≤ 10
htri9 : 9 ≤ n
⊢ from_three_five n
Tactic:
eliminate (lt_or_le n 10) with htri10 htri10
State after:
case inr.inl
P : ℕ → Prop
n : ℕ
h : 8 ≤ n ∧ n ≤ 10
htri9 : 9 ≤ n
htri10 : n < 10
⊢ from_three_five n

case inr.inr
P : ℕ → Prop
n : ℕ
h : 8 ≤ n ∧ n ≤ 10
htri9 : 9 ≤ n
htri10 : 10 ≤ n
⊢ from_three_five n

State before:
case inr.inl
P : ℕ → Prop
n : ℕ
h : 8 ≤ n ∧ n ≤ 10
htri9 : 9 ≤ n
htri10 : n < 10
⊢ from_three_five n

case inr.inr
P : ℕ → Prop
n : ℕ
h : 8 ≤ n ∧ n ≤ 10
htri9 : 9 ≤ n
htri10 : 10 ≤ n
⊢ from_three_five n
Tactic:
{
  sorry
}
State after:
case inr.inr
P : ℕ → Prop
n : ℕ
h : 8 ≤ n ∧ n ≤ 10
htri9 : 9 ≤ n
htri10 : 10 ≤ n
⊢ from_three_five n

State before:
case inr.inr
P : ℕ → Prop
n : ℕ
h : 8 ≤ n ∧ n ≤ 10
htri9 : 9 ≤ n
htri10 : 10 ≤ n
⊢ from_three_five n
Tactic:
{
  sorry
}
State after:
no goals

State before:
case inr.inl
P : ℕ → Prop
n : ℕ
h : 8 ≤ n ∧ n ≤ 10
htri9 : 9 ≤ n
htri10 : n < 10
⊢ from_three_five n
Tactic:
sorry
State after:
no goals

State before:
case inr.inr
P : ℕ → Prop
n : ℕ
h : 8 ≤ n ∧ n ≤ 10
htri9 : 9 ≤ n
htri10 : 10 ≤ n
⊢ from_three_five n
Tactic:
sorry
State after:
no goals