case pos
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
h : index H = 2
a b : G
ha : a ∈ H
⊢ a * b ∈ H ↔ (a ∈ H ↔ b ∈ H)

case neg
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
h : index H = 2
a b : G
ha : ¬a ∈ H
⊢ a * b ∈ H ↔ (a ∈ H ↔ b ∈ H)
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
h : index H = 2
a b : G
⊢ a * b ∈ H ↔ (a ∈ H ↔ b ∈ H)
by_cases ha : a ∈ H
case pos
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
h : index H = 2
a b : G
ha : ¬a ∈ H
hb : b ∈ H
⊢ a * b ∈ H ↔ (a ∈ H ↔ b ∈ H)

case neg
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
h : index H = 2
a b : G
ha : ¬a ∈ H
hb : ¬b ∈ H
⊢ a * b ∈ H ↔ (a ∈ H ↔ b ∈ H)
case neg
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
h : index H = 2
a b : G
ha : ¬a ∈ H
⊢ a * b ∈ H ↔ (a ∈ H ↔ b ∈ H)
by_cases hb : b ∈ H
case neg
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
h : index H = 2
a b : G
ha : ¬a ∈ H
hb : ¬b ∈ H
⊢ a * b ∈ H
case neg
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
h : index H = 2
a b : G
ha : ¬a ∈ H
hb : ¬b ∈ H
⊢ a * b ∈ H ↔ (a ∈ H ↔ b ∈ H)
simp only [ha, hb, iff_self_iff, iff_true_iff]
case neg.intro
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
h : index H = 2
a b : G
ha : ¬a ∈ H
hb : ¬b ∈ H
c : G
hc : ∀ (b : G), Xor' (b * c ∈ H) (b ∈ H)
⊢ a * b ∈ H
case neg
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
h : index H = 2
a b : G
ha : ¬a ∈ H
hb : ¬b ∈ H
⊢ a * b ∈ H
rcases index_eq_two_iff.1 h with ⟨c, hc⟩
case neg.intro
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
h : index H = 2
a b : G
ha : ¬a ∈ H
hb : ¬b ∈ H
c : G
hc : ∀ (b : G), Xor' (b * c ∈ H) (b ∈ H)
⊢ ¬a * b * c ∈ H
case neg.intro
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
h : index H = 2
a b : G
ha : ¬a ∈ H
hb : ¬b ∈ H
c : G
hc : ∀ (b : G), Xor' (b * c ∈ H) (b ∈ H)
⊢ a * b ∈ H
refine' (hc _).or.resolve_left _
no goals
case neg.intro
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
h : index H = 2
a b : G
ha : ¬a ∈ H
hb : ¬b ∈ H
c : G
hc : ∀ (b : G), Xor' (b * c ∈ H) (b ∈ H)
⊢ ¬a * b * c ∈ H
rwa [mul_assoc, mul_mem_cancel_right ((hc _).or.resolve_right hb)]
no goals
case pos
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
h : index H = 2
a b : G
ha : a ∈ H
⊢ a * b ∈ H ↔ (a ∈ H ↔ b ∈ H)
simp only [ha, true_iff_iff, mul_mem_cancel_left ha]
no goals
case pos
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
h : index H = 2
a b : G
ha : ¬a ∈ H
hb : b ∈ H
⊢ a * b ∈ H ↔ (a ∈ H ↔ b ∈ H)
simp only [hb, iff_true_iff, mul_mem_cancel_right hb]