-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sublist.lean
theorem isPrefix_replicate_iff {n} {a : α} {l : List α} :
    l <+: List.replicate n a ↔ l.length ≤ n ∧ l = List.replicate l.length a

Proof state:
α : Type u_1
n : Nat
a : α
l : List α
⊢ l <+: replicate n a ↔ l.length ≤ n ∧ l = replicate l.length a

Tactic:
rw [IsPrefix]

Result:
α : Type u_1
n : Nat
a : α
l : List α
⊢ (∃ t, l ++ t = replicate n a) ↔ l.length ≤ n ∧ l = replicate l.length a

Proof state:
case mpr.intro.refine_2
α : Type u_1
n : Nat
a : α
l : List α
h : l.length ≤ n
w : l = replicate l.length a
⊢ l = replicate l.length a ∧ replicate (n - l.length) a = replicate (replicate (n - l.length) a).length a

Tactic:
simpa using w

Result:
no goals

Proof state:
case mp
α : Type u_1
n : Nat
a : α
l : List α
⊢ (∃ t, l.length + t.length = n ∧ l = replicate l.length a ∧ t = replicate t.length a) →
    l.length ≤ n ∧ l = replicate l.length a

Tactic:
rintro ⟨_, rfl, _, _⟩

Result:
case mp.intro.intro.intro
α : Type u_1
a : α
l w✝ : List α
left✝ : l = replicate l.length a
right✝ : w✝ = replicate w✝.length a
⊢ l.length ≤ l.length + w✝.length ∧ l = replicate l.length a

Proof state:
case mpr.intro
α : Type u_1
n : Nat
a : α
l : List α
h : l.length ≤ n
w : l = replicate l.length a
⊢ ∃ t, l.length + t.length = n ∧ l = replicate l.length a ∧ t = replicate t.length a

Tactic:
refine ⟨replicate (n - l.length) a, ?_, ?_⟩

Result:
case mpr.intro.refine_1
α : Type u_1
n : Nat
a : α
l : List α
h : l.length ≤ n
w : l = replicate l.length a
⊢ l.length + (replicate (n - l.length) a).length = n

case mpr.intro.refine_2
α : Type u_1
n : Nat
a : α
l : List α
h : l.length ≤ n
w : l = replicate l.length a
⊢ l = replicate l.length a ∧ replicate (n - l.length) a = replicate (replicate (n - l.length) a).length a

Proof state:
case mpr
α : Type u_1
n : Nat
a : α
l : List α
⊢ l.length ≤ n ∧ l = replicate l.length a →
    ∃ t, l.length + t.length = n ∧ l = replicate l.length a ∧ t = replicate t.length a

Tactic:
rintro ⟨h, w⟩

Result:
case mpr.intro
α : Type u_1
n : Nat
a : α
l : List α
h : l.length ≤ n
w : l = replicate l.length a
⊢ ∃ t, l.length + t.length = n ∧ l = replicate l.length a ∧ t = replicate t.length a

Proof state:
α : Type u_1
n : Nat
a : α
l : List α
⊢ (∃ t, l.length + t.length = n ∧ l = replicate l.length a ∧ t = replicate t.length a) ↔
    l.length ≤ n ∧ l = replicate l.length a

Tactic:
constructor

Result:
case mp
α : Type u_1
n : Nat
a : α
l : List α
⊢ (∃ t, l.length + t.length = n ∧ l = replicate l.length a ∧ t = replicate t.length a) →
    l.length ≤ n ∧ l = replicate l.length a

case mpr
α : Type u_1
n : Nat
a : α
l : List α
⊢ l.length ≤ n ∧ l = replicate l.length a →
    ∃ t, l.length + t.length = n ∧ l = replicate l.length a ∧ t = replicate t.length a

Proof state:
case mpr.intro.refine_1
α : Type u_1
n : Nat
a : α
l : List α
h : l.length ≤ n
w : l = replicate l.length a
⊢ l.length + (replicate (n - l.length) a).length = n

Tactic:
simpa using add_sub_of_le h

Result:
no goals

Proof state:
case mp.intro.intro.intro
α : Type u_1
a : α
l w✝ : List α
left✝ : l = replicate l.length a
right✝ : w✝ = replicate w✝.length a
⊢ l.length ≤ l.length + w✝.length ∧ l = replicate l.length a

Tactic:
exact ⟨le_add_right .., ‹_›⟩

Result:
no goals

Proof state:
α : Type u_1
n : Nat
a : α
l : List α
⊢ (∃ t, l ++ t = replicate n a) ↔ l.length ≤ n ∧ l = replicate l.length a

Tactic:
simp only [append_eq_replicate_iff]

Result:
α : Type u_1
n : Nat
a : α
l : List α
⊢ (∃ t, l.length + t.length = n ∧ l = replicate l.length a ∧ t = replicate t.length a) ↔
    l.length ≤ n ∧ l = replicate l.length a