-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sublist.lean
theorem sublist_replicate_iff : l <+ replicate m a ↔ ∃ n, n ≤ m ∧ l = replicate n a

Proof state:
α✝ : Type u_1
a : α✝
m n : Nat
le : n ≤ m
ih : ∀ {m : Nat}, replicate n a <+ replicate m a ↔ ∃ n_1, n_1 ≤ m ∧ replicate n a = replicate n_1 a
w : replicate n a <+ replicate m a
⊢ a :: replicate n a = replicate (n + 1) a

Tactic:
simp [replicate_succ]

Result:
no goals

Proof state:
case cons.mp
α✝ : Type u_1
a b : α✝
l : List α✝
ih : ∀ {m : Nat}, l <+ replicate m a ↔ ∃ n, n ≤ m ∧ l = replicate n a
m : Nat
w : b :: l <+ replicate m a
⊢ ∃ n, n ≤ m ∧ b :: l = replicate n a

Tactic:
cases m with
| zero => simp at w
| succ m =>
  simp [replicate_succ] at w
  cases w with
  | cons _ w =>
    obtain ⟨n, le, rfl⟩ := ih.1 (sublist_of_cons_sublist w)
    obtain rfl := (mem_replicate.1 (mem_of_cons_sublist w)).2
    exact ⟨n+1, Nat.add_le_add_right le 1, rfl⟩
  | cons₂ _ w =>
    obtain ⟨n, le, rfl⟩ := ih.1 w
    refine ⟨n+1, Nat.add_le_add_right le 1, by simp [replicate_succ]⟩

Result:
no goals

Proof state:
case cons.mp.succ
α✝ : Type u_1
a b : α✝
l : List α✝
ih : ∀ {m : Nat}, l <+ replicate m a ↔ ∃ n, n ≤ m ∧ l = replicate n a
m : Nat
w : b :: l <+ replicate (m + 1) a
⊢ ∃ n, n ≤ m + 1 ∧ b :: l = replicate n a

Tactic:
simp [replicate_succ] at w

Result:
case cons.mp.succ
α✝ : Type u_1
a b : α✝
l : List α✝
ih : ∀ {m : Nat}, l <+ replicate m a ↔ ∃ n, n ≤ m ∧ l = replicate n a
m : Nat
w : b :: l <+ a :: replicate m a
⊢ ∃ n, n ≤ m + 1 ∧ b :: l = replicate n a

Proof state:
α✝ : Type u_1
a : α✝
m : Nat
⊢ [] = replicate 0 a

Tactic:
simp

Result:
no goals

Proof state:
case cons
α✝ : Type u_1
a b : α✝
l : List α✝
ih : ∀ {m : Nat}, l <+ replicate m a ↔ ∃ n, n ≤ m ∧ l = replicate n a
m : Nat
⊢ b :: l <+ replicate m a ↔ ∃ n, n ≤ m ∧ b :: l = replicate n a

Tactic:
constructor

Result:
case cons.mp
α✝ : Type u_1
a b : α✝
l : List α✝
ih : ∀ {m : Nat}, l <+ replicate m a ↔ ∃ n, n ≤ m ∧ l = replicate n a
m : Nat
⊢ b :: l <+ replicate m a → ∃ n, n ≤ m ∧ b :: l = replicate n a

case cons.mpr
α✝ : Type u_1
a b : α✝
l : List α✝
ih : ∀ {m : Nat}, l <+ replicate m a ↔ ∃ n, n ≤ m ∧ l = replicate n a
m : Nat
⊢ (∃ n, n ≤ m ∧ b :: l = replicate n a) → b :: l <+ replicate m a

Proof state:
case nil
α✝ : Type u_1
a : α✝
m : Nat
⊢ ∃ n, n ≤ m ∧ [] = replicate n a

Tactic:
exact ⟨0, zero_le m, by simp⟩

Result:
no goals

Proof state:
case cons.mp.succ.cons.intro.intro
α✝ : Type u_1
a b : α✝
m n : Nat
le : n ≤ m
ih : ∀ {m : Nat}, replicate n a <+ replicate m a ↔ ∃ n_1, n_1 ≤ m ∧ replicate n a = replicate n_1 a
w : b :: replicate n a <+ replicate m a
⊢ ∃ n_1, n_1 ≤ m + 1 ∧ b :: replicate n a = replicate n_1 a

Tactic:
obtain rfl := (mem_replicate.1 (mem_of_cons_sublist w)).2

Result:
case cons.mp.succ.cons.intro.intro
α✝ : Type u_1
b : α✝
m n : Nat
le : n ≤ m
ih : ∀ {m : Nat}, replicate n b <+ replicate m b ↔ ∃ n_1, n_1 ≤ m ∧ replicate n b = replicate n_1 b
w : b :: replicate n b <+ replicate m b
⊢ ∃ n_1, n_1 ≤ m + 1 ∧ b :: replicate n b = replicate n_1 b

Proof state:
case cons.mpr.intro.intro
α✝ : Type u_1
a b : α✝
l : List α✝
ih : ∀ {m : Nat}, l <+ replicate m a ↔ ∃ n, n ≤ m ∧ l = replicate n a
m n : Nat
le : n ≤ m
w : b :: l = replicate n a
⊢ b :: l <+ replicate m a

Tactic:
rw [w]

Result:
case cons.mpr.intro.intro
α✝ : Type u_1
a b : α✝
l : List α✝
ih : ∀ {m : Nat}, l <+ replicate m a ↔ ∃ n, n ≤ m ∧ l = replicate n a
m n : Nat
le : n ≤ m
w : b :: l = replicate n a
⊢ replicate n a <+ replicate m a

Proof state:
case cons.mpr
α✝ : Type u_1
a b : α✝
l : List α✝
ih : ∀ {m : Nat}, l <+ replicate m a ↔ ∃ n, n ≤ m ∧ l = replicate n a
m : Nat
⊢ (∃ n, n ≤ m ∧ b :: l = replicate n a) → b :: l <+ replicate m a

Tactic:
rintro ⟨n, le, w⟩

Result:
case cons.mpr.intro.intro
α✝ : Type u_1
a b : α✝
l : List α✝
ih : ∀ {m : Nat}, l <+ replicate m a ↔ ∃ n, n ≤ m ∧ l = replicate n a
m n : Nat
le : n ≤ m
w : b :: l = replicate n a
⊢ b :: l <+ replicate m a

Proof state:
case cons.mp.zero
α✝ : Type u_1
a b : α✝
l : List α✝
ih : ∀ {m : Nat}, l <+ replicate m a ↔ ∃ n, n ≤ m ∧ l = replicate n a
w : b :: l <+ replicate 0 a
⊢ ∃ n, n ≤ 0 ∧ b :: l = replicate n a

Tactic:
simp at w

Result:
no goals

Proof state:
case cons.mp.succ.cons
α✝ : Type u_1
a b : α✝
l : List α✝
ih : ∀ {m : Nat}, l <+ replicate m a ↔ ∃ n, n ≤ m ∧ l = replicate n a
m : Nat
w : b :: l <+ replicate m a
⊢ ∃ n, n ≤ m + 1 ∧ b :: l = replicate n a

Tactic:
obtain ⟨n, le, rfl⟩ := ih.1 (sublist_of_cons_sublist w)

Result:
case cons.mp.succ.cons.intro.intro
α✝ : Type u_1
a b : α✝
m n : Nat
le : n ≤ m
ih : ∀ {m : Nat}, replicate n a <+ replicate m a ↔ ∃ n_1, n_1 ≤ m ∧ replicate n a = replicate n_1 a
w : b :: replicate n a <+ replicate m a
⊢ ∃ n_1, n_1 ≤ m + 1 ∧ b :: replicate n a = replicate n_1 a

Proof state:
case cons.mp.succ.cons₂
α✝ : Type u_1
a : α✝
l : List α✝
ih : ∀ {m : Nat}, l <+ replicate m a ↔ ∃ n, n ≤ m ∧ l = replicate n a
m : Nat
w : l <+ replicate m a
⊢ ∃ n, n ≤ m + 1 ∧ a :: l = replicate n a

Tactic:
obtain ⟨n, le, rfl⟩ := ih.1 w

Result:
case cons.mp.succ.cons₂.intro.intro
α✝ : Type u_1
a : α✝
m n : Nat
le : n ≤ m
ih : ∀ {m : Nat}, replicate n a <+ replicate m a ↔ ∃ n_1, n_1 ≤ m ∧ replicate n a = replicate n_1 a
w : replicate n a <+ replicate m a
⊢ ∃ n_1, n_1 ≤ m + 1 ∧ a :: replicate n a = replicate n_1 a

Proof state:
case cons.mp.succ.cons₂.intro.intro
α✝ : Type u_1
a : α✝
m n : Nat
le : n ≤ m
ih : ∀ {m : Nat}, replicate n a <+ replicate m a ↔ ∃ n_1, n_1 ≤ m ∧ replicate n a = replicate n_1 a
w : replicate n a <+ replicate m a
⊢ ∃ n_1, n_1 ≤ m + 1 ∧ a :: replicate n a = replicate n_1 a

Tactic:
refine ⟨n+1, Nat.add_le_add_right le 1, by simp [replicate_succ]⟩

Result:
no goals

Proof state:
case cons.mpr.intro.intro
α✝ : Type u_1
a b : α✝
l : List α✝
ih : ∀ {m : Nat}, l <+ replicate m a ↔ ∃ n, n ≤ m ∧ l = replicate n a
m n : Nat
le : n ≤ m
w : b :: l = replicate n a
⊢ replicate n a <+ replicate m a

Tactic:
exact (replicate_sublist_replicate a).2 le

Result:
no goals

Proof state:
case cons.mp
α✝ : Type u_1
a b : α✝
l : List α✝
ih : ∀ {m : Nat}, l <+ replicate m a ↔ ∃ n, n ≤ m ∧ l = replicate n a
m : Nat
⊢ b :: l <+ replicate m a → ∃ n, n ≤ m ∧ b :: l = replicate n a

Tactic:
intro w

Result:
case cons.mp
α✝ : Type u_1
a b : α✝
l : List α✝
ih : ∀ {m : Nat}, l <+ replicate m a ↔ ∃ n, n ≤ m ∧ l = replicate n a
m : Nat
w : b :: l <+ replicate m a
⊢ ∃ n, n ≤ m ∧ b :: l = replicate n a

Proof state:
case cons.mp.succ
α✝ : Type u_1
a b : α✝
l : List α✝
ih : ∀ {m : Nat}, l <+ replicate m a ↔ ∃ n, n ≤ m ∧ l = replicate n a
m : Nat
w : b :: l <+ a :: replicate m a
⊢ ∃ n, n ≤ m + 1 ∧ b :: l = replicate n a

Tactic:
cases w with
| cons _ w =>
  obtain ⟨n, le, rfl⟩ := ih.1 (sublist_of_cons_sublist w)
  obtain rfl := (mem_replicate.1 (mem_of_cons_sublist w)).2
  exact ⟨n+1, Nat.add_le_add_right le 1, rfl⟩
| cons₂ _ w =>
  obtain ⟨n, le, rfl⟩ := ih.1 w
  refine ⟨n+1, Nat.add_le_add_right le 1, by simp [replicate_succ]⟩

Result:
no goals

Proof state:
case nil
α✝ : Type u_1
a : α✝
m : Nat
⊢ [] <+ replicate m a ↔ ∃ n, n ≤ m ∧ [] = replicate n a

Tactic:
simp only [nil_sublist, true_iff]

Result:
case nil
α✝ : Type u_1
a : α✝
m : Nat
⊢ ∃ n, n ≤ m ∧ [] = replicate n a

Proof state:
case cons.mp.succ.cons.intro.intro
α✝ : Type u_1
b : α✝
m n : Nat
le : n ≤ m
ih : ∀ {m : Nat}, replicate n b <+ replicate m b ↔ ∃ n_1, n_1 ≤ m ∧ replicate n b = replicate n_1 b
w : b :: replicate n b <+ replicate m b
⊢ ∃ n_1, n_1 ≤ m + 1 ∧ b :: replicate n b = replicate n_1 b

Tactic:
exact ⟨n+1, Nat.add_le_add_right le 1, rfl⟩

Result:
no goals