Theorem: AltChoose_zero_of_k_gt_n (BrownCs22/Homework/Hw8.lean)

State before:
⊢ ∀ (n k : ℕ), n < k → (n A k) = 0
Tactic:
basic_induction
State after:
case a

⊢ ∀ (k : ℕ), 0 < k → (0 A k) = 0

case a

⊢ ∀ (n : ℕ), (∀ (k : ℕ), n < k → (n A k) = 0) → ∀ (k : ℕ), n + 1 < k → (n + 1 A k) = 0

State before:
case a

⊢ ∀ (k : ℕ), 0 < k → (0 A k) = 0

case a

⊢ ∀ (n : ℕ), (∀ (k : ℕ), n < k → (n A k) = 0) → ∀ (k : ℕ), n + 1 < k → (n + 1 A k) = 0
Tactic:
{
  sorry
}
State after:
case a

⊢ ∀ (n : ℕ), (∀ (k : ℕ), n < k → (n A k) = 0) → ∀ (k : ℕ), n + 1 < k → (n + 1 A k) = 0

State before:
case a

⊢ ∀ (n : ℕ), (∀ (k : ℕ), n < k → (n A k) = 0) → ∀ (k : ℕ), n + 1 < k → (n + 1 A k) = 0
Tactic:
{
  intro n 
  intro ih 
  sorry
}
State after:
no goals

State before:
case a

⊢ ∀ (k : ℕ), 0 < k → (0 A k) = 0
Tactic:
sorry
State after:
no goals

State before:
case a

⊢ ∀ (n : ℕ), (∀ (k : ℕ), n < k → (n A k) = 0) → ∀ (k : ℕ), n + 1 < k → (n + 1 A k) = 0
Tactic:
intro n
State after:
case a
n : ℕ
⊢ (∀ (k : ℕ), n < k → (n A k) = 0) → ∀ (k : ℕ), n + 1 < k → (n + 1 A k) = 0

State before:
case a
n : ℕ
⊢ (∀ (k : ℕ), n < k → (n A k) = 0) → ∀ (k : ℕ), n + 1 < k → (n + 1 A k) = 0
Tactic:
intro ih
State after:
case a
n : ℕ
ih : ∀ (k : ℕ), n < k → (n A k) = 0
⊢ ∀ (k : ℕ), n + 1 < k → (n + 1 A k) = 0

State before:
case a
n : ℕ
ih : ∀ (k : ℕ), n < k → (n A k) = 0
⊢ ∀ (k : ℕ), n + 1 < k → (n + 1 A k) = 0
Tactic:
sorry
State after:
no goals