-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem replicateRecOn {α : Type _} {p : List α → Prop} (m : List α)
    (h0 : p []) (hr : ∀ a n, 0 < n → p (replicate n a))
    (hi : ∀ a b n l, a ≠ b → 0 < n → p (b :: l) → p (replicate n a ++ b :: l)) : p m

Proof state:
α : Type u_1
p : List α → Prop
m : List α
h0 : p []
hr : ∀ (a : α) (n : Nat), 0 < n → p (replicate n a)
hi : ∀ (a b : α) (n : Nat) (l : List α), a ≠ b → 0 < n → p (b :: l) → p (replicate n a ++ b :: l)
n : Nat
a b : α
l' : List α
w : m = replicate n a ++ b :: l'
hn : 0 < n
h : a ≠ b
⊢ (b :: l').length < m.length

Tactic:
simpa [w] using Nat.lt_add_of_pos_left hn

Result:
no goals

Proof state:
case inr.inr.intro.intro.intro.intro.intro.intro
α : Type u_1
p : List α → Prop
m : List α
h0 : p []
hr : ∀ (a : α) (n : Nat), 0 < n → p (replicate n a)
hi : ∀ (a b : α) (n : Nat) (l : List α), a ≠ b → 0 < n → p (b :: l) → p (replicate n a ++ b :: l)
n : Nat
a b : α
l' : List α
w : m = replicate n a ++ b :: l'
hn : 0 < n
h : a ≠ b
this : (b :: l').length < m.length
⊢ p m

Tactic:
subst w

Result:
case inr.inr.intro.intro.intro.intro.intro.intro
α : Type u_1
p : List α → Prop
h0 : p []
hr : ∀ (a : α) (n : Nat), 0 < n → p (replicate n a)
hi : ∀ (a b : α) (n : Nat) (l : List α), a ≠ b → 0 < n → p (b :: l) → p (replicate n a ++ b :: l)
n : Nat
a b : α
l' : List α
hn : 0 < n
h : a ≠ b
this : (b :: l').length < (replicate n a ++ b :: l').length
⊢ p (replicate n a ++ b :: l')

Proof state:
case inr.inr.intro.intro.intro.intro.intro.intro
α : Type u_1
p : List α → Prop
h0 : p []
hr : ∀ (a : α) (n : Nat), 0 < n → p (replicate n a)
hi : ∀ (a b : α) (n : Nat) (l : List α), a ≠ b → 0 < n → p (b :: l) → p (replicate n a ++ b :: l)
n : Nat
a b : α
l' : List α
hn : 0 < n
h : a ≠ b
this : (b :: l').length < (replicate n a ++ b :: l').length
⊢ p (replicate n a ++ b :: l')

Tactic:
exact hi _ _ _ _ h hn (replicateRecOn (b :: l') h0 hr hi)

Result:
no goals

Proof state:
α : Type u_1
p : List α → Prop
m : List α
h0 : p []
hr : ∀ (a : α) (n : Nat), 0 < n → p (replicate n a)
hi : ∀ (a b : α) (n : Nat) (l : List α), a ≠ b → 0 < n → p (b :: l) → p (replicate n a ++ b :: l)
⊢ p m

Tactic:
rcases eq_replicate_or_eq_replicate_append_cons m with
  rfl | ⟨n, a, rfl, hn⟩ | ⟨n, a, b, l', w, hn, h⟩

Result:
case inl
α : Type u_1
p : List α → Prop
h0 : p []
hr : ∀ (a : α) (n : Nat), 0 < n → p (replicate n a)
hi : ∀ (a b : α) (n : Nat) (l : List α), a ≠ b → 0 < n → p (b :: l) → p (replicate n a ++ b :: l)
⊢ p []

case inr.inl.intro.intro.intro
α : Type u_1
p : List α → Prop
h0 : p []
hr : ∀ (a : α) (n : Nat), 0 < n → p (replicate n a)
hi : ∀ (a b : α) (n : Nat) (l : List α), a ≠ b → 0 < n → p (b :: l) → p (replicate n a ++ b :: l)
n : Nat
a : α
hn : 0 < n
⊢ p (replicate n a)

case inr.inr.intro.intro.intro.intro.intro.intro
α : Type u_1
p : List α → Prop
m : List α
h0 : p []
hr : ∀ (a : α) (n : Nat), 0 < n → p (replicate n a)
hi : ∀ (a b : α) (n : Nat) (l : List α), a ≠ b → 0 < n → p (b :: l) → p (replicate n a ++ b :: l)
n : Nat
a b : α
l' : List α
w : m = replicate n a ++ b :: l'
hn : 0 < n
h : a ≠ b
⊢ p m

Proof state:
case inl
α : Type u_1
p : List α → Prop
h0 : p []
hr : ∀ (a : α) (n : Nat), 0 < n → p (replicate n a)
hi : ∀ (a b : α) (n : Nat) (l : List α), a ≠ b → 0 < n → p (b :: l) → p (replicate n a ++ b :: l)
⊢ p []

Tactic:
exact h0

Result:
no goals

Proof state:
case inr.inl.intro.intro.intro
α : Type u_1
p : List α → Prop
h0 : p []
hr : ∀ (a : α) (n : Nat), 0 < n → p (replicate n a)
hi : ∀ (a b : α) (n : Nat) (l : List α), a ≠ b → 0 < n → p (b :: l) → p (replicate n a ++ b :: l)
n : Nat
a : α
hn : 0 < n
⊢ p (replicate n a)

Tactic:
exact hr _ _ hn

Result:
no goals

Proof state:
case inr.inr.intro.intro.intro.intro.intro.intro
α : Type u_1
p : List α → Prop
m : List α
h0 : p []
hr : ∀ (a : α) (n : Nat), 0 < n → p (replicate n a)
hi : ∀ (a b : α) (n : Nat) (l : List α), a ≠ b → 0 < n → p (b :: l) → p (replicate n a ++ b :: l)
n : Nat
a b : α
l' : List α
w : m = replicate n a ++ b :: l'
hn : 0 < n
h : a ≠ b
⊢ p m

Tactic:
have : (b :: l').length < m.length := by
  simpa [w] using Nat.lt_add_of_pos_left hn

Result:
case inr.inr.intro.intro.intro.intro.intro.intro
α : Type u_1
p : List α → Prop
m : List α
h0 : p []
hr : ∀ (a : α) (n : Nat), 0 < n → p (replicate n a)
hi : ∀ (a b : α) (n : Nat) (l : List α), a ≠ b → 0 < n → p (b :: l) → p (replicate n a ++ b :: l)
n : Nat
a b : α
l' : List α
w : m = replicate n a ++ b :: l'
hn : 0 < n
h : a ≠ b
this : (b :: l').length < m.length
⊢ p m