Theorem: List.getSnoc?_eq_some (LeanColls/Data/List.lean)

State before:
α : Type u_1
xs : List α
x : α
c : List α
⊢ c.getSnoc? = some (xs, x) ↔ c = xs ++ [x]
Tactic:
induction c generalizing xs x <;> simp_all [getSnoc?]
State after:
case cons
α : Type u_1
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ {xs : List α} {x : α}, tail✝.getSnoc? = some (xs, x) ↔ tail✝ = xs ++ [x]
xs : List α
x : α
⊢ (match tail✝.getSnoc? with
      | none => some ([], head✝)
      | some (xs', x') => some (head✝ :: xs', x')) =
      some (xs, x) ↔
    head✝ :: tail✝ = xs ++ [x]

State before:
α : Type u_1
hd : α
tl : List α
ih : ∀ {xs : List α} {x : α}, tl.getSnoc? = some (xs, x) ↔ tl = xs ++ [x]
xs : List α
x : α
⊢ (match tl.getSnoc? with
      | none => some ([], hd)
      | some (xs', x') => some (hd :: xs', x')) =
      some (xs, x) ↔
    hd :: tl = xs ++ [x]
Tactic:
generalize ho : getSnoc? tl = o at ih
State after:
α : Type u_1
hd : α
tl xs : List α
x : α
o : Option (List α × α)
ho : tl.getSnoc? = o
ih : ∀ {xs : List α} {x : α}, o = some (xs, x) ↔ tl = xs ++ [x]
⊢ (match o with
      | none => some ([], hd)
      | some (xs', x') => some (hd :: xs', x')) =
      some (xs, x) ↔
    hd :: tl = xs ++ [x]

State before:
α : Type u_1
hd : α
tl xs : List α
x : α
o : Option (List α × α)
ho : tl.getSnoc? = o
ih : ∀ {xs : List α} {x : α}, o = some (xs, x) ↔ tl = xs ++ [x]
⊢ (match o with
      | none => some ([], hd)
      | some (xs', x') => some (hd :: xs', x')) =
      some (xs, x) ↔
    hd :: tl = xs ++ [x]
Tactic:
cases o <;> simp_all
State after:
case none
α : Type u_1
hd : α
tl xs : List α
x : α
ho : tl = []
⊢ [] = xs ∧ hd = x ↔ [hd] = xs ++ [x]

case some
α : Type u_1
hd : α
tl xs : List α
x : α
val✝ : List α × α
ho : tl.getSnoc? = some val✝
ih : ∀ {xs : List α} {x : α}, val✝ = (xs, x) ↔ tl = xs ++ [x]
⊢ hd :: val✝.1 = xs ∧ val✝.2 = x ↔ hd :: tl = xs ++ [x]

State before:
case none
α : Type u_1
hd : α
tl xs : List α
x : α
ho : tl = []
⊢ [] = xs ∧ hd = x ↔ [hd] = xs ++ [x]
Tactic:
cases xs <;> simp
State after:
no goals

State before:
case some
α : Type u_1
hd : α
tl xs : List α
x : α
val✝ : List α × α
ho : tl.getSnoc? = some val✝
ih : ∀ {xs : List α} {x : α}, val✝ = (xs, x) ↔ tl = xs ++ [x]
⊢ hd :: val✝.1 = xs ∧ val✝.2 = x ↔ hd :: tl = xs ++ [x]
Tactic:
cases xs <;> simp_all
State after:
case some.nil
α : Type u_1
hd : α
tl : List α
x : α
val✝ : List α × α
ho : tl.getSnoc? = some val✝
ih : ∀ {xs : List α} {x : α}, val✝ = (xs, x) ↔ tl = xs ++ [x]
⊢ hd = x → ¬tl = []

case some.cons
α : Type u_1
hd : α
tl : List α
x : α
val✝ : List α × α
ho : tl.getSnoc? = some val✝
ih : ∀ {xs : List α} {x : α}, val✝ = (xs, x) ↔ tl = xs ++ [x]
head✝ : α
tail✝ : List α
⊢ (hd = head✝ ∧ val✝.1 = tail✝) ∧ val✝.2 = x ↔ hd = head✝ ∧ tl = tail✝ ++ [x]

State before:
case some.nil
α : Type u_1
hd : α
tl : List α
x : α
val✝ : List α × α
ho : tl.getSnoc? = some val✝
ih : ∀ {xs : List α} {x : α}, val✝ = (xs, x) ↔ tl = xs ++ [x]
⊢ hd = x → ¬tl = []
Tactic:
rintro rfl rfl
State after:
case some.nil
α : Type u_1
hd : α
val✝ : List α × α
ho : [].getSnoc? = some val✝
ih : ∀ {xs : List α} {x : α}, val✝ = (xs, x) ↔ [] = xs ++ [x]
⊢ False

State before:
case some.nil
α : Type u_1
hd : α
val✝ : List α × α
ho : [].getSnoc? = some val✝
ih : ∀ {xs : List α} {x : α}, val✝ = (xs, x) ↔ [] = xs ++ [x]
⊢ False
Tactic:
simp_all
State after:
case some.nil
α : Type u_1
hd : α
val✝ : List α × α
ho : [].getSnoc? = some val✝
ih : ∀ {xs : List α} {x : α}, ¬val✝ = (xs, x)
⊢ False

State before:
case some.nil
α : Type u_1
hd : α
val✝ : List α × α
ho : [].getSnoc? = some val✝
ih : ∀ {xs : List α} {x : α}, ¬val✝ = (xs, x)
⊢ False
Tactic:
apply ih
State after:
case some.nil.a
α : Type u_1
hd : α
val✝ : List α × α
ho : [].getSnoc? = some val✝
ih : ∀ {xs : List α} {x : α}, ¬val✝ = (xs, x)
⊢ val✝ = (?some.nil.xs, ?some.nil.x)

case some.nil.xs
α : Type u_1
hd : α
val✝ : List α × α
ho : [].getSnoc? = some val✝
ih : ∀ {xs : List α} {x : α}, ¬val✝ = (xs, x)
⊢ List α

case some.nil.x
α : Type u_1
hd : α
val✝ : List α × α
ho : [].getSnoc? = some val✝
ih : ∀ {xs : List α} {x : α}, ¬val✝ = (xs, x)
⊢ α

State before:
case some.nil.a
α : Type u_1
hd : α
val✝ : List α × α
ho : [].getSnoc? = some val✝
ih : ∀ {xs : List α} {x : α}, ¬val✝ = (xs, x)
⊢ val✝ = (?some.nil.xs, ?some.nil.x)

case some.nil.xs
α : Type u_1
hd : α
val✝ : List α × α
ho : [].getSnoc? = some val✝
ih : ∀ {xs : List α} {x : α}, ¬val✝ = (xs, x)
⊢ List α

case some.nil.x
α : Type u_1
hd : α
val✝ : List α × α
ho : [].getSnoc? = some val✝
ih : ∀ {xs : List α} {x : α}, ¬val✝ = (xs, x)
⊢ α
Tactic:
rfl
State after:
no goals

State before:
case some.cons
α : Type u_1
hd : α
tl : List α
x : α
val✝ : List α × α
ho : tl.getSnoc? = some val✝
ih : ∀ {xs : List α} {x : α}, val✝ = (xs, x) ↔ tl = xs ++ [x]
head✝ : α
tail✝ : List α
⊢ (hd = head✝ ∧ val✝.1 = tail✝) ∧ val✝.2 = x ↔ hd = head✝ ∧ tl = tail✝ ++ [x]
Tactic:
rw [←ih]
State after:
case some.cons
α : Type u_1
hd : α
tl : List α
x : α
val✝ : List α × α
ho : tl.getSnoc? = some val✝
ih : ∀ {xs : List α} {x : α}, val✝ = (xs, x) ↔ tl = xs ++ [x]
head✝ : α
tail✝ : List α
⊢ (hd = head✝ ∧ val✝.1 = tail✝) ∧ val✝.2 = x ↔ hd = head✝ ∧ val✝ = (tail✝, x)

State before:
case some.cons
α : Type u_1
hd : α
tl : List α
x : α
val✝ : List α × α
ho : tl.getSnoc? = some val✝
ih : ∀ {xs : List α} {x : α}, val✝ = (xs, x) ↔ tl = xs ++ [x]
head✝ : α
tail✝ : List α
⊢ (hd = head✝ ∧ val✝.1 = tail✝) ∧ val✝.2 = x ↔ hd = head✝ ∧ val✝ = (tail✝, x)
Tactic:
clear ih
State after:
case some.cons
α : Type u_1
hd : α
tl : List α
x : α
val✝ : List α × α
ho : tl.getSnoc? = some val✝
head✝ : α
tail✝ : List α
⊢ (hd = head✝ ∧ val✝.1 = tail✝) ∧ val✝.2 = x ↔ hd = head✝ ∧ val✝ = (tail✝, x)

State before:
case some.cons
α : Type u_1
hd : α
tl : List α
x : α
val✝ : List α × α
ho : tl.getSnoc? = some val✝
head✝ : α
tail✝ : List α
⊢ (hd = head✝ ∧ val✝.1 = tail✝) ∧ val✝.2 = x ↔ hd = head✝ ∧ val✝ = (tail✝, x)
Tactic:
aesop
State after:
no goals