case singleton
ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
N : Type ?u.485949
inst✝ : Monoid N
i j i✝ : ι
x✝ : M i✝
a✝ : x✝ ≠ 1
⊢ toList (singleton x✝ a✝) ≠ []

case append
ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
N : Type ?u.485949
inst✝ : Monoid N
i j i✝ j✝ k✝ l✝ : ι
_w₁✝ : NeWord M i✝ j✝
_hne✝ : j✝ ≠ k✝
_w₂✝ : NeWord M k✝ l✝
_w₁_ih✝ : toList _w₁✝ ≠ []
_w₂_ih✝ : toList _w₂✝ ≠ []
⊢ toList (append _w₁✝ _hne✝ _w₂✝) ≠ []
ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
N : Type ?u.485949
inst✝ : Monoid N
i j : ι
w : NeWord M i j
⊢ toList w ≠ []
induction w
no goals
case singleton
ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
N : Type ?u.485949
inst✝ : Monoid N
i j i✝ : ι
x✝ : M i✝
a✝ : x✝ ≠ 1
⊢ toList (singleton x✝ a✝) ≠ []
rintro ⟨rfl⟩
case append.a
ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
N : Type ?u.485949
inst✝ : Monoid N
i j i✝ j✝ k✝ l✝ : ι
_w₁✝ : NeWord M i✝ j✝
_hne✝ : j✝ ≠ k✝
_w₂✝ : NeWord M k✝ l✝
_w₁_ih✝ : toList _w₁✝ ≠ []
_w₂_ih✝ : toList _w₂✝ ≠ []
⊢ toList _w₁✝ ≠ []
case append
ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
N : Type ?u.485949
inst✝ : Monoid N
i j i✝ j✝ k✝ l✝ : ι
_w₁✝ : NeWord M i✝ j✝
_hne✝ : j✝ ≠ k✝
_w₂✝ : NeWord M k✝ l✝
_w₁_ih✝ : toList _w₁✝ ≠ []
_w₂_ih✝ : toList _w₂✝ ≠ []
⊢ toList (append _w₁✝ _hne✝ _w₂✝) ≠ []
apply List.append_ne_nil_of_ne_nil_left
no goals
case append.a
ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
N : Type ?u.485949
inst✝ : Monoid N
i j i✝ j✝ k✝ l✝ : ι
_w₁✝ : NeWord M i✝ j✝
_hne✝ : j✝ ≠ k✝
_w₂✝ : NeWord M k✝ l✝
_w₁_ih✝ : toList _w₁✝ ≠ []
_w₂_ih✝ : toList _w₂✝ ≠ []
⊢ toList _w₁✝ ≠ []
assumption