G : Type u_1
inst✝ : Group G
H K L : Subgroup G
⊢ (∃ x, ¬x ∈ H ∧ ∀ (x_1 : G), ¬x_1 ∈ H → x_1⁻¹ * x ∈ H) ↔ ∃ a, ∀ (b : G), b * a ∈ H ↔ ¬b ∈ H
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
⊢ index H = 2 ↔ ∃ a, ∀ (b : G), Xor' (b * a ∈ H) (b ∈ H)
simp only [index, Nat.card_eq_two_iff' ((1 : G) : G ⧸ H), ExistsUnique, inv_mem_iff,
  QuotientGroup.exists_mk, QuotientGroup.forall_mk, Ne.def, QuotientGroup.eq, mul_one,
  xor_iff_iff_not]
case refine'_1
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
a : G
ha : ¬a ∈ H ∧ ∀ (x : G), ¬x ∈ H → x⁻¹ * a ∈ H
b : G
hba : b * a ∈ H
hb : b ∈ H
⊢ False

case refine'_2
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
a : G
ha : ¬a ∈ H ∧ ∀ (x : G), ¬x ∈ H → x⁻¹ * a ∈ H
b : G
hb : ¬b ∈ H
⊢ b * a ∈ H

case refine'_3
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
a : G
ha : ∀ (b : G), b * a ∈ H ↔ ¬b ∈ H
⊢ ¬a ∈ H

case refine'_4
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
a : G
ha : ∀ (b : G), b * a ∈ H ↔ ¬b ∈ H
b : G
hb : ¬b ∈ H
⊢ b⁻¹ * a ∈ H
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
⊢ (∃ x, ¬x ∈ H ∧ ∀ (x_1 : G), ¬x_1 ∈ H → x_1⁻¹ * x ∈ H) ↔ ∃ a, ∀ (b : G), b * a ∈ H ↔ ¬b ∈ H
refine'
  exists_congr fun a => ⟨fun ha b => ⟨fun hba hb => _, fun hb => _⟩, fun ha => ⟨_, fun b hb => _⟩⟩
no goals
case refine'_1
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
a : G
ha : ¬a ∈ H ∧ ∀ (x : G), ¬x ∈ H → x⁻¹ * a ∈ H
b : G
hba : b * a ∈ H
hb : b ∈ H
⊢ False
exact ha.1 ((mul_mem_cancel_left hb).1 hba)
no goals
case refine'_2
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
a : G
ha : ¬a ∈ H ∧ ∀ (x : G), ¬x ∈ H → x⁻¹ * a ∈ H
b : G
hb : ¬b ∈ H
⊢ b * a ∈ H
exact inv_inv b ▸ ha.2 _ (mt (inv_mem_iff (x := b)).1 hb)
case refine'_3
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
a : G
ha : ∀ (b : G), b * a ∈ H ↔ ¬b ∈ H
⊢ 1 ∈ H
case refine'_3
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
a : G
ha : ∀ (b : G), b * a ∈ H ↔ ¬b ∈ H
⊢ ¬a ∈ H
rw [← inv_mem_iff (x := a), ← ha, inv_mul_self]
no goals
case refine'_3
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
a : G
ha : ∀ (b : G), b * a ∈ H ↔ ¬b ∈ H
⊢ 1 ∈ H
exact one_mem _
no goals
case refine'_4
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
a : G
ha : ∀ (b : G), b * a ∈ H ↔ ¬b ∈ H
b : G
hb : ¬b ∈ H
⊢ b⁻¹ * a ∈ H
rwa [ha, inv_mem_iff (x := b)]