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

Proof state:
case mp
α : Type u_1
n : Nat
a : α
l : List α
⊢ (∃ s t,
      s.length + l.length + t.length = n ∧
        (True ∧ s = replicate s.length a ∧ 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.intro.intro.intro
α : Type u_1
a : α
l w✝¹ w✝ : List α
right✝¹ : w✝ = replicate w✝.length a
left✝ : w✝¹ = replicate w✝¹.length a
right✝ : l = replicate l.length a
⊢ l.length ≤ w✝¹.length + l.length + w✝.length ∧ l = 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 [IsInfix]

Result:
α : Type u_1
n : Nat
a : α
l : List α
⊢ (∃ s t, s ++ 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
⊢ (True ∧ replicate (n - l.length) a = replicate (replicate (n - l.length) a).length a ∧ l = replicate l.length a) ∧
    [] = replicate [].length a

Tactic:
simpa using w

Result:
no goals

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

Tactic:
exact ⟨le_add_right_of_le (le_add_left ..), ‹_›⟩

Result:
no goals

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
⊢ (replicate (n - l.length) a).length + l.length + [].length = n

Tactic:
simpa using Nat.sub_add_cancel h

Result:
no goals

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

Tactic:
simp only [append_eq_replicate_iff, length_append]

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

Proof state:
case mpr
α : Type u_1
n : Nat
a : α
l : List α
⊢ l.length ≤ n ∧ l = replicate l.length a →
    ∃ s t,
      s.length + l.length + t.length = n ∧
        (True ∧ s = replicate s.length a ∧ 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
⊢ ∃ s t,
    s.length + l.length + t.length = n ∧
      (True ∧ s = replicate s.length a ∧ l = replicate l.length a) ∧ t = replicate t.length a

Proof state:
α : Type u_1
n : Nat
a : α
l : List α
⊢ (∃ s t,
      s.length + l.length + t.length = n ∧
        (True ∧ s = replicate s.length a ∧ 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 α
⊢ (∃ s t,
      s.length + l.length + t.length = n ∧
        (True ∧ s = replicate s.length a ∧ 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 →
    ∃ s t,
      s.length + l.length + t.length = n ∧
        (True ∧ s = replicate s.length a ∧ l = replicate l.length a) ∧ t = replicate t.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
⊢ ∃ s t,
    s.length + l.length + t.length = n ∧
      (True ∧ s = replicate s.length a ∧ 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
⊢ (replicate (n - l.length) a).length + l.length + [].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
⊢ (True ∧ replicate (n - l.length) a = replicate (replicate (n - l.length) a).length a ∧ l = replicate l.length a) ∧
    [] = replicate [].length a