English
A large equivalence describes when the element ⟨_, m₁⟩ lies in the list (of m₂ • w).toList at position i; it splits into cases depending on whether i matches the index of w and the nontriviality of m₁.
Русский
Большое эквивалентное утверждение описывает, когда элемент ⟨i, m₁⟩ лежит в списке (of m₂ • w).toList для позиции i; разбивается на случаи в зависимости от соответствия индекса i и ненулевого m₁.
LaTeX
$$$$ \\text{mem\_smul\_iff} : \\; \\langle i,m_1\\rangle \\in (of m_2 \\cdot w).toList \\leftrightarrow (\\langle i,m_1\\rangle \\in w.toList.tail) \\lor ... $$$$
Lean4
theorem mem_smul_iff {i j : ι} {m₁ : M i} {m₂ : M j} {w : Word M} :
⟨_, m₁⟩ ∈ (of m₂ • w).toList ↔
(¬i = j ∧ ⟨i, m₁⟩ ∈ w.toList) ∨
(m₁ ≠ 1 ∧
∃ (hij : i = j),
(⟨i, m₁⟩ ∈ w.toList.tail) ∨
(∃ m', ⟨j, m'⟩ ∈ w.toList.head? ∧ m₁ = hij ▸ (m₂ * m')) ∨ (w.fstIdx ≠ some j ∧ m₁ = hij ▸ m₂)) :=
by
rw [of_smul_def, mem_rcons_iff, mem_equivPair_tail_iff, equivPair_head, or_assoc]
by_cases hij : i = j
· subst i
simp only [not_true, ne_eq, false_and, exists_prop, true_and, false_or]
by_cases hw : ⟨j, m₁⟩ ∈ w.toList.tail
· simp [hw, show m₁ ≠ 1 from w.ne_one _ (List.mem_of_mem_tail hw)]
· simp only [hw, false_or, Option.mem_def, and_congr_right_iff]
intro hm1
split_ifs with h
· rcases h with ⟨hnil, rfl⟩
simp only [List.head?_eq_head hnil, Option.some.injEq]
constructor
· rintro rfl
exact Or.inl ⟨_, rfl, rfl⟩
· rintro (⟨_, h, rfl⟩ | hm')
· simp only [Sigma.ext_iff, heq_eq_eq, true_and] at h
subst h
rfl
· simp only [fstIdx, Option.map_eq_some_iff, Sigma.exists, exists_and_right, exists_eq_right, not_exists,
ne_eq] at hm'
exact (hm'.1 (w.toList.head hnil).2 (by rw [List.head?_eq_head])).elim
· revert h
rw [fstIdx]
cases w.toList
· simp
· simp +contextual [Sigma.ext_iff]
· rcases w with ⟨_ | _, _, _⟩ <;> simp [or_comm, hij, Ne.symm hij, eq_comm]
