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

State before:
P : ℕ → Prop
n : ℕ
⊢ 3 ≤ n → from_three_five (n - 3) → from_three_five n
Tactic:
intro h_3_le_n hftf
State after:
P : ℕ → Prop
n : ℕ
h_3_le_n : 3 ≤ n
hftf : from_three_five (n - 3)
⊢ from_three_five n

State before:
P : ℕ → Prop
n : ℕ
h_3_le_n : 3 ≤ n
hftf : from_three_five (n - 3)
⊢ from_three_five n
Tactic:
have : (n-3) + 3 = n := by {
  sorry
}
State after:
P : ℕ → Prop
n : ℕ
h_3_le_n : 3 ≤ n
hftf : from_three_five (n - 3)
this : n - 3 + 3 = n
⊢ from_three_five n

State before:
P : ℕ → Prop
n : ℕ
h_3_le_n : 3 ≤ n
hftf : from_three_five (n - 3)
this : n - 3 + 3 = n
⊢ from_three_five n
Tactic:
sorry
State after:
no goals

State before:
P : ℕ → Prop
n : ℕ
h_3_le_n : 3 ≤ n
hftf : from_three_five (n - 3)
⊢ n - 3 + 3 = n
Tactic:
sorry
State after:
no goals