no goals
α : Type u_1
β : Type ?u.29777
l l₁ l₂ l₃ : List α
a b : α
m n : ℕ
s : List α
this : s = [] ↔ s <+: []
⊢ s ∈ inits [] ↔ s <+: []
simpa only [inits, mem_singleton]
no goals
α : Type u_1
β : Type ?u.29777
l l₁ l₂ l₃ : List α
a✝ b : α
m n : ℕ
s : List α
a : α
t : List α
this : (s = [] ∨ ∃ l, l ∈ inits t ∧ a :: l = s) ↔ s <+: a :: t
⊢ s ∈ inits (a :: t) ↔ s <+: a :: t
simpa
α : Type u_1
β : Type ?u.29777
l l₁ l₂ l₃ : List α
a✝ b : α
m n : ℕ
s✝¹ : List α
a : α
t : List α
o : s✝¹ = [] ∨ ∃ l, l ∈ inits t ∧ a :: l = s✝¹
s✝ r : List α
hr : r ∈ inits t
hs : a :: r = s✝
s : List α
ht : r ++ s = t
⊢ s✝ <+: a :: t
α : Type u_1
β : Type ?u.29777
l l₁ l₂ l₃ : List α
a✝ b : α
m n : ℕ
s✝ : List α
a : α
t : List α
o : s✝ = [] ∨ ∃ l, l ∈ inits t ∧ a :: l = s✝
s r : List α
hr : r ∈ inits t
hs : a :: r = s
⊢ s <+: a :: t
let ⟨s, ht⟩ := (mem_inits _ _).1 hr
α : Type u_1
β : Type ?u.29777
l l₁ l₂ l₃ : List α
a✝ b : α
m n : ℕ
s✝¹ : List α
a : α
t : List α
o : s✝¹ = [] ∨ ∃ l, l ∈ inits t ∧ a :: l = s✝¹
s✝ r : List α
hr : r ∈ inits t
hs : a :: r = s✝
s : List α
ht : r ++ s = t
⊢ a :: r <+: a :: (r ++ s)
α : Type u_1
β : Type ?u.29777
l l₁ l₂ l₃ : List α
a✝ b : α
m n : ℕ
s✝¹ : List α
a : α
t : List α
o : s✝¹ = [] ∨ ∃ l, l ∈ inits t ∧ a :: l = s✝¹
s✝ r : List α
hr : r ∈ inits t
hs : a :: r = s✝
s : List α
ht : r ++ s = t
⊢ s✝ <+: a :: t
rw [← hs, ← ht]
no goals
α : Type u_1
β : Type ?u.29777
l l₁ l₂ l₃ : List α
a✝ b : α
m n : ℕ
s✝¹ : List α
a : α
t : List α
o : s✝¹ = [] ∨ ∃ l, l ∈ inits t ∧ a :: l = s✝¹
s✝ r : List α
hr : r ∈ inits t
hs : a :: r = s✝
s : List α
ht : r ++ s = t
⊢ a :: r <+: a :: (r ++ s)
exact ⟨s, rfl⟩
α : Type u_1
β : Type ?u.29777
l l₁ l₂ l₃ : List α
a✝ b✝ : α
m n : ℕ
s✝ : List α
a : α
t : List α
mi : s✝ <+: a :: t
b : α
s r : List α
hr : b :: s ++ r = a :: t
ba : b = a
st : s ++ r = t
⊢ ∃ l, l ∈ inits t ∧ a :: l = a :: s
α : Type u_1
β : Type ?u.29777
l l₁ l₂ l₃ : List α
a✝ b✝ : α
m n : ℕ
s✝ : List α
a : α
t : List α
mi : s✝ <+: a :: t
b : α
s r : List α
hr : b :: s ++ r = a :: t
ba : b = a
st : s ++ r = t
⊢ ∃ l, l ∈ inits t ∧ a :: l = b :: s
rw [ba]
no goals
α : Type u_1
β : Type ?u.29777
l l₁ l₂ l₃ : List α
a✝ b✝ : α
m n : ℕ
s✝ : List α
a : α
t : List α
mi : s✝ <+: a :: t
b : α
s r : List α
hr : b :: s ++ r = a :: t
ba : b = a
st : s ++ r = t
⊢ ∃ l, l ∈ inits t ∧ a :: l = a :: s
exact ⟨_, (mem_inits _ _).2 ⟨_, st⟩, rfl⟩