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

State before:
n : ℕ
⊢ (n C 1) = n
Tactic:
have hnzp : n = 0 ∨ ∃ n0, n = n0 + 1 := eq_zero_or_exists_succ n
State after:
n : ℕ
hnzp : n = 0 ∨ ∃ n0, n = n0 + 1
⊢ (n C 1) = n

State before:
n : ℕ
hnzp : n = 0 ∨ ∃ n0, n = n0 + 1
⊢ (n C 1) = n
Tactic:
eliminate hnzp with h h
State after:
case inl
n : ℕ
h : n = 0
⊢ (n C 1) = n

case inr
n : ℕ
h : ∃ n0, n = n0 + 1
⊢ (n C 1) = n

State before:
case inl
n : ℕ
h : n = 0
⊢ (n C 1) = n

case inr
n : ℕ
h : ∃ n0, n = n0 + 1
⊢ (n C 1) = n
Tactic:
{simp [h]}
State after:
case inr
n : ℕ
h : ∃ n0, n = n0 + 1
⊢ (n C 1) = n

State before:
case inr
n : ℕ
h : ∃ n0, n = n0 + 1
⊢ (n C 1) = n
Tactic:
{
  eliminate h with n0 h
  have : n ≠ 0 := by linarith 
  simp [Choose]
  rewrite [h, Nat.factorial_succ]
  simp
  rewrite [Nat.mul_div_cancel]
  {linarith}
  {apply Nat.factorial_pos}
}
State after:
no goals

State before:
case inl
n : ℕ
h : n = 0
⊢ (n C 1) = n
Tactic:
simp [h]
State after:
no goals

State before:
case inr
n : ℕ
h : ∃ n0, n = n0 + 1
⊢ (n C 1) = n
Tactic:
eliminate h with n0 h
State after:
case inr.intro
n n0 : ℕ
h : n = n0 + 1
⊢ (n C 1) = n

State before:
case inr.intro
n n0 : ℕ
h : n = n0 + 1
⊢ (n C 1) = n
Tactic:
have : n ≠ 0 := by linarith
State after:
case inr.intro
n n0 : ℕ
h : n = n0 + 1
this : n ≠ 0
⊢ (n C 1) = n

State before:
case inr.intro
n n0 : ℕ
h : n = n0 + 1
this : n ≠ 0
⊢ (n C 1) = n
Tactic:
simp [Choose]
State after:
case inr.intro
n n0 : ℕ
h : n = n0 + 1
this : n ≠ 0
⊢ n¡ / (n - 1)¡ = n

State before:
case inr.intro
n n0 : ℕ
h : n = n0 + 1
this : n ≠ 0
⊢ n¡ / (n - 1)¡ = n
Tactic:
rewrite [h, Nat.factorial_succ]
State after:
case inr.intro
n n0 : ℕ
h : n = n0 + 1
this : n ≠ 0
⊢ (n0 + 1) * n0¡ / (n0 + 1 - 1)¡ = n0 + 1

State before:
case inr.intro
n n0 : ℕ
h : n = n0 + 1
this : n ≠ 0
⊢ (n0 + 1) * n0¡ / (n0 + 1 - 1)¡ = n0 + 1
Tactic:
simp
State after:
case inr.intro
n n0 : ℕ
h : n = n0 + 1
this : n ≠ 0
⊢ (n0 + 1) * n0¡ / n0¡ = n0 + 1

State before:
case inr.intro
n n0 : ℕ
h : n = n0 + 1
this : n ≠ 0
⊢ (n0 + 1) * n0¡ / n0¡ = n0 + 1
Tactic:
rewrite [Nat.mul_div_cancel]
State after:
case inr.intro
n n0 : ℕ
h : n = n0 + 1
this : n ≠ 0
⊢ n0 + 1 = n0 + 1

case inr.intro.H
n n0 : ℕ
h : n = n0 + 1
this : n ≠ 0
⊢ 0 < n0¡

State before:
case inr.intro
n n0 : ℕ
h : n = n0 + 1
this : n ≠ 0
⊢ n0 + 1 = n0 + 1

case inr.intro.H
n n0 : ℕ
h : n = n0 + 1
this : n ≠ 0
⊢ 0 < n0¡
Tactic:
{linarith}
State after:
case inr.intro.H
n n0 : ℕ
h : n = n0 + 1
this : n ≠ 0
⊢ 0 < n0¡

State before:
case inr.intro.H
n n0 : ℕ
h : n = n0 + 1
this : n ≠ 0
⊢ 0 < n0¡
Tactic:
{apply Nat.factorial_pos}
State after:
no goals

State before:
n n0 : ℕ
h : n = n0 + 1
⊢ n ≠ 0
Tactic:
linarith
State after:
no goals

State before:
case inr.intro
n n0 : ℕ
h : n = n0 + 1
this : n ≠ 0
⊢ n0 + 1 = n0 + 1
Tactic:
linarith
State after:
no goals

State before:
case inr.intro.H
n n0 : ℕ
h : n = n0 + 1
this : n ≠ 0
⊢ 0 < n0¡
Tactic:
apply Nat.factorial_pos
State after:
no goals