English
If H has index 2 in G, then for all a,b ∈ G, ab ∈ H is equivalent to (a ∈ H) ↔ (b ∈ H).
Русский
Если подгруппа H имеет индекс 2 в группе G, то для всех a, b ∈ G выполнено ab ∈ H тогда и только тогда, когда (a ∈ H) ↔ (b ∈ H).
LaTeX
$$$ [G: H] = 2 \implies \forall a,b \in G,\ ab \in H \iff (a \in H) \iff (b \in H). $$$
Lean4
@[to_additive]
theorem mul_mem_iff_of_index_two (h : H.index = 2) {a b : G} : a * b ∈ H ↔ (a ∈ H ↔ b ∈ H) :=
by
by_cases ha : a ∈ H; · simp only [ha, true_iff, mul_mem_cancel_left ha]
by_cases hb : b ∈ H; · simp only [hb, iff_true, mul_mem_cancel_right hb]
simp only [ha, hb, iff_true]
rcases index_eq_two_iff.1 h with ⟨c, hc⟩
refine (hc _).or.resolve_left ?_
rwa [mul_assoc, mul_mem_cancel_right ((hc _).or.resolve_right hb)]
