English
If l1 ⊆ l2 and a ∈ l1.toList then a ∈ l2, by unfolding the definitions of membership and toList.
Русский
Если l1 ⊆ l2 и a ∈ l1.toList, тогда a ∈ l2, раскрывая определения членства и toList.
LaTeX
$${a} ⊆ {l1} → a ∈ l1.toList → a ∈ l2$$
Lean4
theorem trans : ∀ {l₁ l₂ l₃ : Lists α}, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃ :=
by
let trans := fun l₁ : Lists α => ∀ ⦃l₂ l₃⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
suffices PProd (∀ l₁, trans l₁) (∀ (l : Lists' α true), ∀ l' ∈ l.toList, trans l') by exact this.1
apply inductionMut
· intro a l₂ l₃ h₁ h₂
rwa [← equiv_atom.1 h₁] at h₂
· intro l₁ IH l₂ l₃ h₁ h₂
obtain - | l₂ := id h₁
· exact h₂
obtain - | l₃ := id h₂
· exact h₁
obtain ⟨hl₁, hr₁⟩ := Equiv.antisymm_iff.1 h₁
obtain ⟨hl₂, hr₂⟩ := Equiv.antisymm_iff.1 h₂
apply Equiv.antisymm_iff.2; constructor <;> apply Lists'.subset_def.2
· intro a₁ m₁
rcases Lists'.mem_of_subset' hl₁ m₁ with ⟨a₂, m₂, e₁₂⟩
rcases Lists'.mem_of_subset' hl₂ m₂ with ⟨a₃, m₃, e₂₃⟩
exact ⟨a₃, m₃, IH _ m₁ e₁₂ e₂₃⟩
· intro a₃ m₃
rcases Lists'.mem_of_subset' hr₂ m₃ with ⟨a₂, m₂, e₃₂⟩
rcases Lists'.mem_of_subset' hr₁ m₂ with ⟨a₁, m₁, e₂₁⟩
exact ⟨a₁, m₁, (IH _ m₁ e₂₁.symm e₃₂.symm).symm⟩
· rintro _ ⟨⟩
· intro a l IH₁ IH₂
simpa using ⟨IH₁, IH₂⟩
