English
For g, g1 ∈ G, a ∈ A, and s ∈ S, the value indToCoindAux A g a (s · g1) equals A.ρ(s) applied to indToCoindAux A g a g1, establishing a compatibility with S-action.
Русский
Для g, g1 ∈ G, a ∈ A и s ∈ S значение indToCoindAux A g a (s · g1) равно A.ρ(s) применённому к indToCoindAux A g a g1, устанавливая совместимость с действием S.
LaTeX
$$$indToCoindAux A g a (s \cdot g1) = A.ρ s (indToCoindAux A g a g1)$$$
Lean4
@[simp]
theorem indToCoindAux_mul_snd (g g₁ : G) (a : A) (s : S) :
indToCoindAux A g a (s * g₁) = A.ρ s (indToCoindAux A g a g₁) :=
by
rcases em ((QuotientGroup.rightRel S).r g₁ g) with ⟨s₁, rfl⟩ | h
· simp only [indToCoindAux, LinearMap.pi_apply]
rw [dif_pos ⟨s * s₁, mul_assoc ..⟩, dif_pos ⟨s₁, rfl⟩]
simp [S.1.smul_def, mul_assoc, ← S.1.mul_def]
· rw [indToCoindAux_of_not_rel _ _ _ h, indToCoindAux_of_not_rel, map_zero]
exact mt (fun ⟨s₁, hs₁⟩ => ⟨s⁻¹ * s₁, by simp_all [S.1.smul_def, mul_assoc]⟩) h
