ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
N : Type ?u.490383
inst✝ : Monoid N
i j : ι
w : NeWord M i j
⊢ { fst := i, snd := head w } ∈ List.head? (toList w)
ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
N : Type ?u.490383
inst✝ : Monoid N
i j : ι
w : NeWord M i j
⊢ List.head? (toList w) = some { fst := i, snd := head w }
rw [← Option.mem_def]
case singleton
ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
N : Type ?u.490383
inst✝ : Monoid N
i j i✝ : ι
x✝ : M i✝
a✝ : x✝ ≠ 1
⊢ { fst := i✝, snd := head (singleton x✝ a✝) } ∈ List.head? (toList (singleton x✝ a✝))

case append
ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
N : Type ?u.490383
inst✝ : Monoid N
i j i✝ j✝ k✝ l✝ : ι
_w₁✝ : NeWord M i✝ j✝
_hne✝ : j✝ ≠ k✝
_w₂✝ : NeWord M k✝ l✝
_w₁_ih✝ : { fst := i✝, snd := head _w₁✝ } ∈ List.head? (toList _w₁✝)
_w₂_ih✝ : { fst := k✝, snd := head _w₂✝ } ∈ List.head? (toList _w₂✝)
⊢ { fst := i✝, snd := head (append _w₁✝ _hne✝ _w₂✝) } ∈ List.head? (toList (append _w₁✝ _hne✝ _w₂✝))
ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
N : Type ?u.490383
inst✝ : Monoid N
i j : ι
w : NeWord M i j
⊢ { fst := i, snd := head w } ∈ List.head? (toList w)
induction w
case singleton
ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
N : Type ?u.490383
inst✝ : Monoid N
i j i✝ : ι
x✝ : M i✝
a✝ : x✝ ≠ 1
⊢ List.head? (toList (singleton x✝ a✝)) = some { fst := i✝, snd := head (singleton x✝ a✝) }
case singleton
ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
N : Type ?u.490383
inst✝ : Monoid N
i j i✝ : ι
x✝ : M i✝
a✝ : x✝ ≠ 1
⊢ { fst := i✝, snd := head (singleton x✝ a✝) } ∈ List.head? (toList (singleton x✝ a✝))
rw [Option.mem_def]
no goals
case singleton
ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
N : Type ?u.490383
inst✝ : Monoid N
i j i✝ : ι
x✝ : M i✝
a✝ : x✝ ≠ 1
⊢ List.head? (toList (singleton x✝ a✝)) = some { fst := i✝, snd := head (singleton x✝ a✝) }
rfl
no goals
case append
ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
N : Type ?u.490383
inst✝ : Monoid N
i j i✝ j✝ k✝ l✝ : ι
_w₁✝ : NeWord M i✝ j✝
_hne✝ : j✝ ≠ k✝
_w₂✝ : NeWord M k✝ l✝
_w₁_ih✝ : { fst := i✝, snd := head _w₁✝ } ∈ List.head? (toList _w₁✝)
_w₂_ih✝ : { fst := k✝, snd := head _w₂✝ } ∈ List.head? (toList _w₂✝)
⊢ { fst := i✝, snd := head (append _w₁✝ _hne✝ _w₂✝) } ∈ List.head? (toList (append _w₁✝ _hne✝ _w₂✝))
exact List.head?_append (by assumption)
no goals
ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
N : Type ?u.490383
inst✝ : Monoid N
i j i✝ j✝ k✝ l✝ : ι
_w₁✝ : NeWord M i✝ j✝
_hne✝ : j✝ ≠ k✝
_w₂✝ : NeWord M k✝ l✝
_w₁_ih✝ : { fst := i✝, snd := head _w₁✝ } ∈ List.head? (toList _w₁✝)
_w₂_ih✝ : { fst := k✝, snd := head _w₂✝ } ∈ List.head? (toList _w₂✝)
⊢ { fst := i✝, snd := head (append _w₁✝ _hne✝ _w₂✝) } ∈ List.head? (toList _w₁✝)
assumption