Theorem: HTPI.exists_cons_of_length_eq_succ (HTPILib/Chap7.lean)

State before:
A : Type
l : List A
n : ℕ
h : List.length l = n + 1
⊢ ∃ a L, l = a :: L ∧ List.length L = n
Tactic:
have h1 : ¬l.length = 0 := by linarith
State after:
A : Type
l : List A
n : ℕ
h : List.length l = n + 1
h1 : ¬List.length l = 0
⊢ ∃ a L, l = a :: L ∧ List.length L = n

State before:
A : Type
l : List A
n : ℕ
h : List.length l = n + 1
h1 : ¬List.length l = 0
⊢ ∃ a L, l = a :: L ∧ List.length L = n
Tactic:
rewrite [List.length_eq_zero] at h1
State after:
A : Type
l : List A
n : ℕ
h : List.length l = n + 1
h1 : ¬l = []
⊢ ∃ a L, l = a :: L ∧ List.length L = n

State before:
A : Type
l : List A
n : ℕ
h : List.length l = n + 1
h1 : ¬l = []
⊢ ∃ a L, l = a :: L ∧ List.length L = n
Tactic:
obtain (a : A) (h2 : ∃ (L : List A), l = a :: L) from
  List.exists_cons_of_ne_nil h1
State after:
A : Type
l : List A
n : ℕ
h : List.length l = n + 1
h1 : ¬l = []
a : A
h2 : ∃ L, l = a :: L
⊢ ∃ a L, l = a :: L ∧ List.length L = n

State before:
A : Type
l : List A
n : ℕ
h : List.length l = n + 1
h1 : ¬l = []
a : A
h2 : ∃ L, l = a :: L
⊢ ∃ a L, l = a :: L ∧ List.length L = n
Tactic:
obtain (L : List A) (h3 : l = a :: L) from h2
State after:
A : Type
l : List A
n : ℕ
h : List.length l = n + 1
h1 : ¬l = []
a : A
h2 : ∃ L, l = a :: L
L : List A
h3 : l = a :: L
⊢ ∃ a L, l = a :: L ∧ List.length L = n

State before:
A : Type
l : List A
n : ℕ
h : List.length l = n + 1
h1 : ¬l = []
a : A
h2 : ∃ L, l = a :: L
L : List A
h3 : l = a :: L
⊢ ∃ a L, l = a :: L ∧ List.length L = n
Tactic:
apply Exists.intro a
State after:
A : Type
l : List A
n : ℕ
h : List.length l = n + 1
h1 : ¬l = []
a : A
h2 : ∃ L, l = a :: L
L : List A
h3 : l = a :: L
⊢ ∃ L, l = a :: L ∧ List.length L = n

State before:
A : Type
l : List A
n : ℕ
h : List.length l = n + 1
h1 : ¬l = []
a : A
h2 : ∃ L, l = a :: L
L : List A
h3 : l = a :: L
⊢ ∃ L, l = a :: L ∧ List.length L = n
Tactic:
apply Exists.intro L
State after:
A : Type
l : List A
n : ℕ
h : List.length l = n + 1
h1 : ¬l = []
a : A
h2 : ∃ L, l = a :: L
L : List A
h3 : l = a :: L
⊢ l = a :: L ∧ List.length L = n

State before:
A : Type
l : List A
n : ℕ
h : List.length l = n + 1
h1 : ¬l = []
a : A
h2 : ∃ L, l = a :: L
L : List A
h3 : l = a :: L
⊢ l = a :: L ∧ List.length L = n
Tactic:
apply And.intro h3
State after:
A : Type
l : List A
n : ℕ
h : List.length l = n + 1
h1 : ¬l = []
a : A
h2 : ∃ L, l = a :: L
L : List A
h3 : l = a :: L
⊢ List.length L = n

State before:
A : Type
l : List A
n : ℕ
h : List.length l = n + 1
h1 : ¬l = []
a : A
h2 : ∃ L, l = a :: L
L : List A
h3 : l = a :: L
⊢ List.length L = n
Tactic:
have h4 : (a :: L).length = L.length + 1 := List.length_cons a L
State after:
A : Type
l : List A
n : ℕ
h : List.length l = n + 1
h1 : ¬l = []
a : A
h2 : ∃ L, l = a :: L
L : List A
h3 : l = a :: L
h4 : List.length (a :: L) = List.length L + 1
⊢ List.length L = n

State before:
A : Type
l : List A
n : ℕ
h : List.length l = n + 1
h1 : ¬l = []
a : A
h2 : ∃ L, l = a :: L
L : List A
h3 : l = a :: L
h4 : List.length (a :: L) = List.length L + 1
⊢ List.length L = n
Tactic:
rewrite [←h3, h] at h4
State after:
A : Type
l : List A
n : ℕ
h : List.length l = n + 1
h1 : ¬l = []
a : A
h2 : ∃ L, l = a :: L
L : List A
h3 : l = a :: L
h4 : n + 1 = List.length L + 1
⊢ List.length L = n

State before:
A : Type
l : List A
n : ℕ
h : List.length l = n + 1
h1 : ¬l = []
a : A
h2 : ∃ L, l = a :: L
L : List A
h3 : l = a :: L
h4 : n + 1 = List.length L + 1
⊢ List.length L = n
Tactic:
show L.length = n from (Nat.add_right_cancel h4).symm
State after:
no goals

State before:
A : Type
l : List A
n : ℕ
h : List.length l = n + 1
⊢ ¬List.length l = 0
Tactic:
linarith
State after:
no goals