Theorem: List.getLast_intercalate (One.lean)

State before:
α : Type ?u.383648
delim : List α
a : α
l : List (List α)
h₂ : intercalate delim l ≠ []
not_nil : getLast? l ≠ some []
⊢ l ≠ []
Tactic:
intro contr
State after:
α : Type ?u.383648
delim : List α
a : α
l : List (List α)
h₂ : intercalate delim l ≠ []
not_nil : getLast? l ≠ some []
contr : l = []
⊢ False

State before:
α : Type ?u.383648
delim : List α
a : α
l : List (List α)
h₂ : intercalate delim l ≠ []
not_nil : getLast? l ≠ some []
contr : l = []
⊢ False
Tactic:
apply h₂
State after:
α : Type ?u.383648
delim : List α
a : α
l : List (List α)
h₂ : intercalate delim l ≠ []
not_nil : getLast? l ≠ some []
contr : l = []
⊢ intercalate delim l = []

State before:
α : Type ?u.383648
delim : List α
a : α
l : List (List α)
h₂ : intercalate delim l ≠ []
not_nil : getLast? l ≠ some []
contr : l = []
⊢ intercalate delim l = []
Tactic:
rw [contr]
State after:
α : Type ?u.383648
delim : List α
a : α
l : List (List α)
h₂ : intercalate delim l ≠ []
not_nil : getLast? l ≠ some []
contr : l = []
⊢ intercalate delim [] = []

State before:
α : Type ?u.383648
delim : List α
a : α
l : List (List α)
h₂ : intercalate delim l ≠ []
not_nil : getLast? l ≠ some []
contr : l = []
⊢ intercalate delim [] = []
Tactic:
simp only [intercalate._eq_1, join]
State after:
no goals

State before:
α : Type ?u.383648
delim : List α
a : α
l : List (List α)
h₂ : intercalate delim l ≠ []
not_nil : getLast? l ≠ some []
⊢ getLast l (_ : l = [] → False) ≠ []
Tactic:
intro contr
State after:
α : Type ?u.383648
delim : List α
a : α
l : List (List α)
h₂ : intercalate delim l ≠ []
not_nil : getLast? l ≠ some []
contr : getLast l (_ : l = [] → False) = []
⊢ False

State before:
α : Type ?u.383648
delim : List α
a : α
l : List (List α)
h₂ : intercalate delim l ≠ []
not_nil : getLast? l ≠ some []
contr : getLast l (_ : l = [] → False) = []
⊢ False
Tactic:
apply not_nil
State after:
α : Type ?u.383648
delim : List α
a : α
l : List (List α)
h₂ : intercalate delim l ≠ []
not_nil : getLast? l ≠ some []
contr : getLast l (_ : l = [] → False) = []
⊢ getLast? l = some []

State before:
α : Type ?u.383648
delim : List α
a : α
l : List (List α)
h₂ : intercalate delim l ≠ []
not_nil : getLast? l ≠ some []
contr : getLast l (_ : l = [] → False) = []
⊢ getLast? l = some []
Tactic:
rw[←contr]
State after:
α : Type ?u.383648
delim : List α
a : α
l : List (List α)
h₂ : intercalate delim l ≠ []
not_nil : getLast? l ≠ some []
contr : getLast l (_ : l = [] → False) = []
⊢ getLast? l = some (getLast l (_ : l = [] → False))

State before:
α : Type ?u.383648
delim : List α
a : α
l : List (List α)
h₂ : intercalate delim l ≠ []
not_nil : getLast? l ≠ some []
contr : getLast l (_ : l = [] → False) = []
⊢ getLast? l = some (getLast l (_ : l = [] → False))
Tactic:
apply List.getLast?_eq_getLast
State after:
no goals

State before:
α : Type u_1
delim : List α
a : α
l : List (List α)
h₂ : intercalate delim l ≠ []
not_nil : getLast? l ≠ some []
⊢ getLast (intercalate delim l) h₂ =
    getLast (getLast l (_ : l = [] → False)) (_ : getLast l (_ : l = [] → False) = [] → False)
Tactic:
match l with
| [] => simp only [intercalate._eq_1, join, ne_eq, not_true] at h₂
| [a] =>
  simp [intercalate]
| [a,b] =>
  simp [intercalate]
  simp [← intercalate._eq_1]
  simp only [← append_assoc]
  rw [getLast_append']
| head::mid::mid₂::tail =>
  simp [intercalate]
  simp [← intercalate._eq_1]
  simp only [← append_assoc]
  rw [getLast_append', getLast_intercalate (mid₂::tail)]
  . intro contr
    apply not_nil
    rw [List.getLast?_eq_getLast]
    simp only [ne_eq, not_false_iff, getLast_cons, Option.some.injEq]
    generalize_proofs hp
    apply List.intercalate_eq_nil contr (getLast (mid₂ :: tail) hp)
    apply List.getLast_mem
    simp only [ne_eq, not_false_iff]
  . intro contr
    apply not_nil
    simp only [getLast?_cons_cons, contr]
  . exact a
State after:
no goals

State before:
α : Type u_1
delim : List α
a : α
l : List (List α)
h₂ : intercalate delim [] ≠ []
not_nil : getLast? [] ≠ some []
⊢ getLast (intercalate delim []) h₂ =
    getLast (getLast [] (_ : [] = [] → False)) (_ : getLast [] (_ : [] = [] → False) = [] → False)
Tactic:
simp only [intercalate._eq_1, join, ne_eq, not_true] at h₂
State after:
no goals

State before:
α : Type u_1
delim : List α
a✝ : α
l : List (List α)
a : List α
h₂ : intercalate delim [a] ≠ []
not_nil : getLast? [a] ≠ some []
⊢ getLast (intercalate delim [a]) h₂ =
    getLast (getLast [a] (_ : [a] = [] → False)) (_ : getLast [a] (_ : [a] = [] → False) = [] → False)
Tactic:
simp [intercalate]
State after:
no goals

State before:
α : Type u_1
delim : List α
a✝ : α
l : List (List α)
a b : List α
h₂ : intercalate delim [a, b] ≠ []
not_nil : getLast? [a, b] ≠ some []
⊢ getLast (intercalate delim [a, b]) h₂ =
    getLast (getLast [a, b] (_ : [a, b] = [] → False)) (_ : getLast [a, b] (_ : [a, b] = [] → False) = [] → False)
Tactic:
simp [intercalate]
State after:
α : Type u_1
delim : List α
a✝ : α
l : List (List α)
a b : List α
h₂ : intercalate delim [a, b] ≠ []
not_nil : getLast? [a, b] ≠ some []
⊢ getLast (a ++ (delim ++ b)) (_ : a ++ (delim ++ b) ≠ []) = getLast b (_ : b ≠ [])

State before:
α : Type u_1
delim : List α
a✝ : α
l : List (List α)
a b : List α
h₂ : intercalate delim [a, b] ≠ []
not_nil : getLast? [a, b] ≠ some []
⊢ getLast (a ++ (delim ++ b)) (_ : a ++ (delim ++ b) ≠ []) = getLast b (_ : b ≠ [])
Tactic:
simp only [← append_assoc]
State after:
α : Type u_1
delim : List α
a✝ : α
l : List (List α)
a b : List α
h₂ : intercalate delim [a, b] ≠ []
not_nil : getLast? [a, b] ≠ some []
⊢ getLast (a ++ delim ++ b) (_ : a ++ delim ++ b ≠ []) = getLast b (_ : b ≠ [])

State before:
α : Type u_1
delim : List α
a✝ : α
l : List (List α)
a b : List α
h₂ : intercalate delim [a, b] ≠ []
not_nil : getLast? [a, b] ≠ some []
⊢ getLast (a ++ delim ++ b) (_ : a ++ delim ++ b ≠ []) = getLast b (_ : b ≠ [])
Tactic:
rw [getLast_append']
State after:
no goals

State before:
α : Type u_1
delim : List α
a : α
l : List (List α)
head mid mid₂ : List α
tail : List (List α)
h₂ : intercalate delim (head :: mid :: mid₂ :: tail) ≠ []
not_nil : getLast? (head :: mid :: mid₂ :: tail) ≠ some []
⊢ getLast (intercalate delim (head :: mid :: mid₂ :: tail)) h₂ =
    getLast (getLast (head :: mid :: mid₂ :: tail) (_ : head :: mid :: mid₂ :: tail = [] → False))
      (_ : getLast (head :: mid :: mid₂ :: tail) (_ : head :: mid :: mid₂ :: tail = [] → False) = [] → False)
Tactic:
simp [intercalate]
State after:
α : Type u_1
delim : List α
a : α
l : List (List α)
head mid mid₂ : List α
tail : List (List α)
h₂ : intercalate delim (head :: mid :: mid₂ :: tail) ≠ []
not_nil : getLast? (head :: mid :: mid₂ :: tail) ≠ some []
⊢ getLast (head ++ (delim ++ (mid ++ (delim ++ join (intersperse delim (mid₂ :: tail))))))
      (_ : head ++ (delim ++ (mid ++ (delim ++ join (intersperse delim (mid₂ :: tail))))) ≠ []) =
    getLast (getLast (mid₂ :: tail) (_ : ¬mid₂ :: tail = [])) (_ : getLast (mid₂ :: tail) (_ : ¬mid₂ :: tail = []) ≠ [])

State before:
α : Type u_1
delim : List α
a : α
l : List (List α)
head mid mid₂ : List α
tail : List (List α)
h₂ : intercalate delim (head :: mid :: mid₂ :: tail) ≠ []
not_nil : getLast? (head :: mid :: mid₂ :: tail) ≠ some []
⊢ getLast (head ++ (delim ++ (mid ++ (delim ++ join (intersperse delim (mid₂ :: tail))))))
      (_ : head ++ (delim ++ (mid ++ (delim ++ join (intersperse delim (mid₂ :: tail))))) ≠ []) =
    getLast (getLast (mid₂ :: tail) (_ : ¬mid₂ :: tail = [])) (_ : getLast (mid₂ :: tail) (_ : ¬mid₂ :: tail = []) ≠ [])
Tactic:
simp [← intercalate._eq_1]
State after:
α : Type u_1
delim : List α
a : α
l : List (List α)
head mid mid₂ : List α
tail : List (List α)
h₂ : intercalate delim (head :: mid :: mid₂ :: tail) ≠ []
not_nil : getLast? (head :: mid :: mid₂ :: tail) ≠ some []
⊢ getLast (head ++ (delim ++ (mid ++ (delim ++ intercalate delim (mid₂ :: tail)))))
      (_ : head ++ (delim ++ (mid ++ (delim ++ intercalate delim (mid₂ :: tail)))) ≠ []) =
    getLast (getLast (mid₂ :: tail) (_ : ¬mid₂ :: tail = [])) (_ : getLast (mid₂ :: tail) (_ : ¬mid₂ :: tail = []) ≠ [])

State before:
α : Type u_1
delim : List α
a : α
l : List (List α)
head mid mid₂ : List α
tail : List (List α)
h₂ : intercalate delim (head :: mid :: mid₂ :: tail) ≠ []
not_nil : getLast? (head :: mid :: mid₂ :: tail) ≠ some []
⊢ getLast (head ++ (delim ++ (mid ++ (delim ++ intercalate delim (mid₂ :: tail)))))
      (_ : head ++ (delim ++ (mid ++ (delim ++ intercalate delim (mid₂ :: tail)))) ≠ []) =
    getLast (getLast (mid₂ :: tail) (_ : ¬mid₂ :: tail = [])) (_ : getLast (mid₂ :: tail) (_ : ¬mid₂ :: tail = []) ≠ [])
Tactic:
simp only [← append_assoc]
State after:
α : Type u_1
delim : List α
a : α
l : List (List α)
head mid mid₂ : List α
tail : List (List α)
h₂ : intercalate delim (head :: mid :: mid₂ :: tail) ≠ []
not_nil : getLast? (head :: mid :: mid₂ :: tail) ≠ some []
⊢ getLast (head ++ delim ++ mid ++ delim ++ intercalate delim (mid₂ :: tail))
      (_ : head ++ delim ++ mid ++ delim ++ intercalate delim (mid₂ :: tail) ≠ []) =
    getLast (getLast (mid₂ :: tail) (_ : ¬mid₂ :: tail = [])) (_ : getLast (mid₂ :: tail) (_ : ¬mid₂ :: tail = []) ≠ [])

State before:
α : Type u_1
delim : List α
a : α
l : List (List α)
head mid mid₂ : List α
tail : List (List α)
h₂ : intercalate delim (head :: mid :: mid₂ :: tail) ≠ []
not_nil : getLast? (head :: mid :: mid₂ :: tail) ≠ some []
⊢ getLast (head ++ delim ++ mid ++ delim ++ intercalate delim (mid₂ :: tail))
      (_ : head ++ delim ++ mid ++ delim ++ intercalate delim (mid₂ :: tail) ≠ []) =
    getLast (getLast (mid₂ :: tail) (_ : ¬mid₂ :: tail = [])) (_ : getLast (mid₂ :: tail) (_ : ¬mid₂ :: tail = []) ≠ [])
Tactic:
rw [getLast_append', getLast_intercalate (mid₂::tail)]
State after:
case h₂
α : Type u_1
delim : List α
a : α
l : List (List α)
head mid mid₂ : List α
tail : List (List α)
h₂ : intercalate delim (head :: mid :: mid₂ :: tail) ≠ []
not_nil : getLast? (head :: mid :: mid₂ :: tail) ≠ some []
⊢ intercalate delim (mid₂ :: tail) ≠ []

case not_nil
α : Type u_1
delim : List α
a : α
l : List (List α)
head mid mid₂ : List α
tail : List (List α)
h₂ : intercalate delim (head :: mid :: mid₂ :: tail) ≠ []
not_nil : getLast? (head :: mid :: mid₂ :: tail) ≠ some []
⊢ getLast? (mid₂ :: tail) ≠ some []

α : Type u_1
delim : List α
a : α
l : List (List α)
head mid mid₂ : List α
tail : List (List α)
h₂ : intercalate delim (head :: mid :: mid₂ :: tail) ≠ []
not_nil : getLast? (head :: mid :: mid₂ :: tail) ≠ some []
⊢ α

State before:
case h₂
α : Type u_1
delim : List α
a : α
l : List (List α)
head mid mid₂ : List α
tail : List (List α)
h₂ : intercalate delim (head :: mid :: mid₂ :: tail) ≠ []
not_nil : getLast? (head :: mid :: mid₂ :: tail) ≠ some []
⊢ intercalate delim (mid₂ :: tail) ≠ []

case not_nil
α : Type u_1
delim : List α
a : α
l : List (List α)
head mid mid₂ : List α
tail : List (List α)
h₂ : intercalate delim (head :: mid :: mid₂ :: tail) ≠ []
not_nil : getLast? (head :: mid :: mid₂ :: tail) ≠ some []
⊢ getLast? (mid₂ :: tail) ≠ some []

α : Type u_1
delim : List α
a : α
l : List (List α)
head mid mid₂ : List α
tail : List (List α)
h₂ : intercalate delim (head :: mid :: mid₂ :: tail) ≠ []
not_nil : getLast? (head :: mid :: mid₂ :: tail) ≠ some []
⊢ α
Tactic:
. intro contr
  apply not_nil
  rw [List.getLast?_eq_getLast]
  simp only [ne_eq, not_false_iff, getLast_cons, Option.some.injEq]
  generalize_proofs hp
  apply List.intercalate_eq_nil contr (getLast (mid₂ :: tail) hp)
  apply List.getLast_mem
  simp only [ne_eq, not_false_iff]
State after:
case not_nil
α : Type u_1
delim : List α
a : α
l : List (List α)
head mid mid₂ : List α
tail : List (List α)
h₂ : intercalate delim (head :: mid :: mid₂ :: tail) ≠ []
not_nil : getLast? (head :: mid :: mid₂ :: tail) ≠ some []
⊢ getLast? (mid₂ :: tail) ≠ some []

α : Type u_1
delim : List α
a : α
l : List (List α)
head mid mid₂ : List α
tail : List (List α)
h₂ : intercalate delim (head :: mid :: mid₂ :: tail) ≠ []
not_nil : getLast? (head :: mid :: mid₂ :: tail) ≠ some []
⊢ α

State before:
case not_nil
α : Type u_1
delim : List α
a : α
l : List (List α)
head mid mid₂ : List α
tail : List (List α)
h₂ : intercalate delim (head :: mid :: mid₂ :: tail) ≠ []
not_nil : getLast? (head :: mid :: mid₂ :: tail) ≠ some []
⊢ getLast? (mid₂ :: tail) ≠ some []

α : Type u_1
delim : List α
a : α
l : List (List α)
head mid mid₂ : List α
tail : List (List α)
h₂ : intercalate delim (head :: mid :: mid₂ :: tail) ≠ []
not_nil : getLast? (head :: mid :: mid₂ :: tail) ≠ some []
⊢ α
Tactic:
. intro contr
  apply not_nil
  simp only [getLast?_cons_cons, contr]
State after:
α : Type u_1
delim : List α
a : α
l : List (List α)
head mid mid₂ : List α
tail : List (List α)
h₂ : intercalate delim (head :: mid :: mid₂ :: tail) ≠ []
not_nil : getLast? (head :: mid :: mid₂ :: tail) ≠ some []
⊢ α

State before:
α : Type u_1
delim : List α
a : α
l : List (List α)
head mid mid₂ : List α
tail : List (List α)
h₂ : intercalate delim (head :: mid :: mid₂ :: tail) ≠ []
not_nil : getLast? (head :: mid :: mid₂ :: tail) ≠ some []
⊢ α
Tactic:
. exact a
State after:
no goals