-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem eq_replicate_or_eq_replicate_append_cons {α : Type _} (l : List α) :
    (l = []) ∨ (∃ n a, l = replicate n a ∧ 0 < n) ∨
      (∃ n a b l', l = replicate n a ++ b :: l' ∧ 0 < n ∧ a ≠ b)

Proof state:
case neg.h
α : Type u_1
x : α
n : Nat
a : α
h : 0 < n
h' : ¬x = a
⊢ ∃ n_1 a_1 b l', x :: replicate n a = replicate n_1 a_1 ++ b :: l' ∧ 0 < n_1 ∧ a_1 ≠ b

Tactic:
refine ⟨1, x, a, replicate (n - 1) a, ?_, by decide, h'⟩

Result:
case neg.h
α : Type u_1
x : α
n : Nat
a : α
h : 0 < n
h' : ¬x = a
⊢ x :: replicate n a = replicate 1 x ++ a :: replicate (n - 1) a

Proof state:
case neg
α : Type u_1
x : α
n : Nat
a b : α
l' : List α
h : 0 < n ∧ a ≠ b
h' : ¬x = a
⊢ ∃ n_1 a_1 b_1 l'_1, x :: (replicate n a ++ b :: l') = replicate n_1 a_1 ++ b_1 :: l'_1 ∧ 0 < n_1 ∧ a_1 ≠ b_1

Tactic:
refine ⟨1, x, a, replicate (n - 1) a ++ b :: l', ?_, by decide, h'⟩

Result:
case neg
α : Type u_1
x : α
n : Nat
a b : α
l' : List α
h : 0 < n ∧ a ≠ b
h' : ¬x = a
⊢ x :: (replicate n a ++ b :: l') = replicate 1 x ++ a :: (replicate (n - 1) a ++ b :: l')

Proof state:
case cons.h.inr.inr.intro.intro.intro.intro.intro.h
α : Type u_1
x : α
n : Nat
a b : α
l' : List α
h : 0 < n ∧ a ≠ b
⊢ ∃ n_1 a_1 b_1 l'_1, x :: (replicate n a ++ b :: l') = replicate n_1 a_1 ++ b_1 :: l'_1 ∧ 0 < n_1 ∧ a_1 ≠ b_1

Tactic:
by_cases h' : x = a

Result:
case pos
α : Type u_1
x : α
n : Nat
a b : α
l' : List α
h : 0 < n ∧ a ≠ b
h' : x = a
⊢ ∃ n_1 a_1 b_1 l'_1, x :: (replicate n a ++ b :: l') = replicate n_1 a_1 ++ b_1 :: l'_1 ∧ 0 < n_1 ∧ a_1 ≠ b_1

case neg
α : Type u_1
x : α
n : Nat
a b : α
l' : List α
h : 0 < n ∧ a ≠ b
h' : ¬x = a
⊢ ∃ n_1 a_1 b_1 l'_1, x :: (replicate n a ++ b :: l') = replicate n_1 a_1 ++ b_1 :: l'_1 ∧ 0 < n_1 ∧ a_1 ≠ b_1

Proof state:
α : Type u_1
x : α
n : Nat
b : α
l' : List α
h : 0 < n ∧ x ≠ b
⊢ 0 < n + 1

Tactic:
simp

Result:
no goals

Proof state:
case cons.h.inr.inr.intro.intro.intro.intro.intro
α : Type u_1
x : α
n : Nat
a b : α
l' : List α
h : 0 < n ∧ a ≠ b
⊢ (∃ n_1 a_1, x :: (replicate n a ++ b :: l') = replicate n_1 a_1 ∧ 0 < n_1) ∨
    ∃ n_1 a_1 b_1 l'_1, x :: (replicate n a ++ b :: l') = replicate n_1 a_1 ++ b_1 :: l'_1 ∧ 0 < n_1 ∧ a_1 ≠ b_1

Tactic:
right

Result:
case cons.h.inr.inr.intro.intro.intro.intro.intro.h
α : Type u_1
x : α
n : Nat
a b : α
l' : List α
h : 0 < n ∧ a ≠ b
⊢ ∃ n_1 a_1 b_1 l'_1, x :: (replicate n a ++ b :: l') = replicate n_1 a_1 ++ b_1 :: l'_1 ∧ 0 < n_1 ∧ a_1 ≠ b_1

Proof state:
α : Type u_1
x : α
⊢ 0 < 1

Tactic:
decide

Result:
no goals

Proof state:
case cons.h.inl
α : Type u_1
x : α
⊢ (∃ n a, [x] = replicate n a ∧ 0 < n) ∨ ∃ n a b l', [x] = replicate n a ++ b :: l' ∧ 0 < n ∧ a ≠ b

Tactic:
left

Result:
case cons.h.inl.h
α : Type u_1
x : α
⊢ ∃ n a, [x] = replicate n a ∧ 0 < n

Proof state:
case pos.h
α : Type u_1
x : α
n : Nat
h : 0 < n
⊢ ∃ n_1 a, x :: replicate n x = replicate n_1 a ∧ 0 < n_1

Tactic:
exact ⟨n + 1, x, rfl, by simp⟩

Result:
no goals

Proof state:
case neg.h
α : Type u_1
x : α
n : Nat
a : α
h : 0 < n
h' : ¬x = a
⊢ x :: replicate n a = replicate 1 x ++ a :: replicate (n - 1) a

Tactic:
match n with | n + 1 => simp [replicate_succ]

Result:
no goals

Proof state:
α : Type u_1
x : α
n : Nat
h : 0 < n
⊢ 0 < n + 1

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
x : α
n✝ : Nat
a : α
h' : ¬x = a
n : Nat
h : 0 < n + 1
⊢ x :: replicate (n + 1) a = replicate 1 x ++ a :: replicate (n + 1 - 1) a

Tactic:
simp [replicate_succ]

Result:
no goals

Proof state:
case cons.h
α : Type u_1
x : α
l : List α
ih : l = [] ∨ (∃ n a, l = replicate n a ∧ 0 < n) ∨ ∃ n a b l', l = replicate n a ++ b :: l' ∧ 0 < n ∧ a ≠ b
⊢ (∃ n a, x :: l = replicate n a ∧ 0 < n) ∨ ∃ n a b l', x :: l = replicate n a ++ b :: l' ∧ 0 < n ∧ a ≠ b

Tactic:
rcases ih with rfl | ⟨n, a, rfl, h⟩ | ⟨n, a, b, l', rfl, h⟩

Result:
case cons.h.inl
α : Type u_1
x : α
⊢ (∃ n a, [x] = replicate n a ∧ 0 < n) ∨ ∃ n a b l', [x] = replicate n a ++ b :: l' ∧ 0 < n ∧ a ≠ b

case cons.h.inr.inl.intro.intro.intro
α : Type u_1
x : α
n : Nat
a : α
h : 0 < n
⊢ (∃ n_1 a_1, x :: replicate n a = replicate n_1 a_1 ∧ 0 < n_1) ∨
    ∃ n_1 a_1 b l', x :: replicate n a = replicate n_1 a_1 ++ b :: l' ∧ 0 < n_1 ∧ a_1 ≠ b

case cons.h.inr.inr.intro.intro.intro.intro.intro
α : Type u_1
x : α
n : Nat
a b : α
l' : List α
h : 0 < n ∧ a ≠ b
⊢ (∃ n_1 a_1, x :: (replicate n a ++ b :: l') = replicate n_1 a_1 ∧ 0 < n_1) ∨
    ∃ n_1 a_1 b_1 l'_1, x :: (replicate n a ++ b :: l') = replicate n_1 a_1 ++ b_1 :: l'_1 ∧ 0 < n_1 ∧ a_1 ≠ b_1

Proof state:
case pos
α : Type u_1
x : α
n : Nat
a b : α
l' : List α
h : 0 < n ∧ a ≠ b
h' : x = a
⊢ ∃ n_1 a_1 b_1 l'_1, x :: (replicate n a ++ b :: l') = replicate n_1 a_1 ++ b_1 :: l'_1 ∧ 0 < n_1 ∧ a_1 ≠ b_1

Tactic:
subst h'

Result:
case pos
α : Type u_1
x : α
n : Nat
b : α
l' : List α
h : 0 < n ∧ x ≠ b
⊢ ∃ n_1 a b_1 l'_1, x :: (replicate n x ++ b :: l') = replicate n_1 a ++ b_1 :: l'_1 ∧ 0 < n_1 ∧ a ≠ b_1

Proof state:
case neg
α : Type u_1
x : α
n : Nat
a b : α
l' : List α
h : 0 < n ∧ a ≠ b
h' : ¬x = a
⊢ x :: (replicate n a ++ b :: l') = replicate 1 x ++ a :: (replicate (n - 1) a ++ b :: l')

Tactic:
match n with | n + 1 => simp [replicate_succ]

Result:
no goals

Proof state:
case pos
α : Type u_1
x : α
n : Nat
h : 0 < n
⊢ (∃ n_1 a, x :: replicate n x = replicate n_1 a ∧ 0 < n_1) ∨
    ∃ n_1 a b l', x :: replicate n x = replicate n_1 a ++ b :: l' ∧ 0 < n_1 ∧ a ≠ b

Tactic:
left

Result:
case pos.h
α : Type u_1
x : α
n : Nat
h : 0 < n
⊢ ∃ n_1 a, x :: replicate n x = replicate n_1 a ∧ 0 < n_1

Proof state:
case cons
α : Type u_1
x : α
l : List α
ih : l = [] ∨ (∃ n a, l = replicate n a ∧ 0 < n) ∨ ∃ n a b l', l = replicate n a ++ b :: l' ∧ 0 < n ∧ a ≠ b
⊢ x :: l = [] ∨ (∃ n a, x :: l = replicate n a ∧ 0 < n) ∨ ∃ n a b l', x :: l = replicate n a ++ b :: l' ∧ 0 < n ∧ a ≠ b

Tactic:
right

Result:
case cons.h
α : Type u_1
x : α
l : List α
ih : l = [] ∨ (∃ n a, l = replicate n a ∧ 0 < n) ∨ ∃ n a b l', l = replicate n a ++ b :: l' ∧ 0 < n ∧ a ≠ b
⊢ (∃ n a, x :: l = replicate n a ∧ 0 < n) ∨ ∃ n a b l', x :: l = replicate n a ++ b :: l' ∧ 0 < n ∧ a ≠ b

Proof state:
α : Type u_1
x : α
n : Nat
a : α
h : 0 < n
h' : ¬x = a
⊢ 0 < 1

Tactic:
decide

Result:
no goals

Proof state:
α : Type u_1
x : α
n : Nat
b : α
l' : List α
h : 0 < n ∧ x ≠ b
⊢ x :: (replicate n x ++ b :: l') = replicate (n + 1) x ++ b :: l'

Tactic:
simp [replicate_succ]

Result:
no goals

Proof state:
α : Type u_1
x : α
n : Nat
a b : α
l' : List α
h : 0 < n ∧ a ≠ b
h' : ¬x = a
⊢ 0 < 1

Tactic:
decide

Result:
no goals

Proof state:
case neg
α : Type u_1
x : α
n : Nat
a : α
h : 0 < n
h' : ¬x = a
⊢ (∃ n_1 a_1, x :: replicate n a = replicate n_1 a_1 ∧ 0 < n_1) ∨
    ∃ n_1 a_1 b l', x :: replicate n a = replicate n_1 a_1 ++ b :: l' ∧ 0 < n_1 ∧ a_1 ≠ b

Tactic:
right

Result:
case neg.h
α : Type u_1
x : α
n : Nat
a : α
h : 0 < n
h' : ¬x = a
⊢ ∃ n_1 a_1 b l', x :: replicate n a = replicate n_1 a_1 ++ b :: l' ∧ 0 < n_1 ∧ a_1 ≠ b

Proof state:
case cons.h.inl.h
α : Type u_1
x : α
⊢ ∃ n a, [x] = replicate n a ∧ 0 < n

Tactic:
exact ⟨1, x, rfl, by decide⟩

Result:
no goals

Proof state:
α : Type u_1
x : α
n✝ : Nat
a b : α
l' : List α
h' : ¬x = a
n : Nat
h : 0 < n + 1 ∧ a ≠ b
⊢ x :: (replicate (n + 1) a ++ b :: l') = replicate 1 x ++ a :: (replicate (n + 1 - 1) a ++ b :: l')

Tactic:
simp [replicate_succ]

Result:
no goals