awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H K L : Subgroup G
hHK : H ≤ K
hKL : K ≤ L
rw : (H.subgroupOf L).relIndex (K.subgroupOf L) * K.relIndex L = H.relIndex L
⊢ H.relIndex K * K.relIndex L = H.relIndex L

Tactic:
rw [← relIndex_subgroupOf hKL]

Premises used: Subgroup.relIndex_subgroupOf
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H K L : Subgroup G
hHK : H ≤ K
hKL : K ≤ L
⊢ (H.subgroupOf L).relIndex (K.subgroupOf L) * K.relIndex L = H.relIndex L

Tactic:
relIndex_mul_index fun x hx => hHK hx

Premises used: Subgroup.relIndex_mul_index, Subgroup.relIndex
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H K L : Subgroup G
hHK : H ≤ K
hKL : K ≤ L
⊢ (H.subgroupOf L).relIndex (K.subgroupOf L) * K.relIndex L = H.relIndex L

Tactic:
exact relIndex_mul_index fun x hx => hHK hx

Premises used: Subgroup.relIndex_mul_index
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
rw : ((H ⊓ K).subgroupOf K).index = H.relIndex K
rw₁ : ((H ⊓ K).subgroupOf K).index = (H.subgroupOf K).index
rw₂ rw₃ : (H.subgroupOf K).index = (H.subgroupOf K).index
⊢ (H ⊓ K).relIndex K = H.relIndex K

Tactic:
rw [relIndex, relIndex, inf_subgroupOf_right]

Premises used: Subgroup.inf_subgroupOf_right, Subgroup.relIndex
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
rw : (K ⊓ H).relIndex H = K.relIndex H
rw₁ rw₂ : K.relIndex H = K.relIndex H
⊢ (H ⊓ K).relIndex H = K.relIndex H

Tactic:
rw [inf_comm, inf_relIndex_right]

Premises used: Subgroup.inf_relIndex_right, inf_comm
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H K L : Subgroup G
rw : (H ⊓ (K ⊓ L)).relIndex (K ⊓ L) * K.relIndex L = (H ⊓ K).relIndex L
rw₁ : (H ⊓ (K ⊓ L)).relIndex (K ⊓ L) * (K ⊓ L).relIndex L = (H ⊓ K).relIndex L
rw₂ : (H ⊓ (K ⊓ L)).relIndex (K ⊓ L) * (K ⊓ L).relIndex L = (H ⊓ K ⊓ L).relIndex L
rw₃ : (H ⊓ (K ⊓ L)).relIndex (K ⊓ L) * (K ⊓ L).relIndex L = (H ⊓ (K ⊓ L)).relIndex L
rw₄ rw₅ : (H ⊓ (K ⊓ L)).relIndex L = (H ⊓ (K ⊓ L)).relIndex L
⊢ H.relIndex (K ⊓ L) * K.relIndex L = (H ⊓ K).relIndex L

Tactic:
rw [← inf_relIndex_right H (K ⊓ L), ← inf_relIndex_right K L, ← inf_relIndex_right (H ⊓ K) L,
    inf_assoc, relIndex_mul_relIndex (H ⊓ (K ⊓ L)) (K ⊓ L) L inf_le_right inf_le_right]

Premises used: inf_le_right, Subgroup.relIndex_mul_relIndex, Subgroup.inf_relIndex_right, inf_assoc, Min.min
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
inst_1 : K.Normal
⊢ K.relIndex (H ⊔ K) = K.relIndex H

Tactic:
Nat.card_congr (QuotientGroup.quotientInfEquivProdNormalQuotient H K).toEquiv.symm

Premises used: MulEquiv.toEquiv, Subgroup.relIndex, Nat.card_congr, Subgroup.index, Equiv.symm, QuotientGroup.quotientInfEquivProdNormalQuotient
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
inst_1 : K.Normal
rw : K.relIndex (H ⊔ K) = K.relIndex H
rw₁ rw₂ : K.relIndex H = K.relIndex H
⊢ K.relIndex (K ⊔ H) = K.relIndex H

Tactic:
rw [sup_comm, relIndex_sup_right]

Premises used: Subgroup.relIndex_sup_right, sup_comm
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
inst_1 : H.Normal
⊢ H.relIndex K ∣ H.index

Tactic:
relIndex_sup_right K H ▸ relIndex_dvd_index_of_le le_sup_right

Premises used: Subgroup.relIndex_dvd_index_of_le, Eq.rec, le_sup_right, Subgroup.relIndex_sup_right
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H K L : Subgroup G
hHK : H ≤ K
⊢ K.relIndex L ∣ H.relIndex L

Tactic:
inf_of_le_left hHK ▸ dvd_of_mul_left_eq _ (relIndex_inf_mul_relIndex _ _ _)

Premises used: inf_of_le_left, dvd_of_mul_left_eq, Eq.rec, Subgroup.relIndex_inf_mul_relIndex
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
simp : (∃ x ∉ H, ∀ x_1 ∉ H, x_1⁻¹ * x ∈ H) ↔ ∃ (a : G), ∀ (b : G), b * a ∈ H ↔ b ∉ H
⊢ H.index = 2 ↔ ∃ (a : G), ∀ (b : G), Xor (b * a ∈ H) (b ∈ H)

Tactic:
simp only [index, Nat.card_eq_two_iff' ((1 : G) : G ⧸ H), ExistsUnique, inv_mem_iff,
    QuotientGroup.exists_mk, QuotientGroup.forall_mk, Ne, QuotientGroup.eq, mul_one,
    xor_iff_iff_not]

Premises used: QuotientGroup.mk, Nat.card_eq_two_iff', QuotientGroup.eq, inv_mem_iff, Ne, xor_iff_iff_not, ExistsUnique, Subgroup.index, mul_one, OfNat.ofNat, QuotientGroup.exists_mk, QuotientGroup.forall_mk
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
⊢ (∃ x ∉ H, ∀ x_1 ∉ H, x_1⁻¹ * x ∈ H) ↔ ∃ (a : G), ∀ (b : G), b * a ∈ H ↔ b ∉ H

Tactic:
exists_congr fun a =>
    ⟨fun ha b => ⟨fun hba hb => ?_, fun hb => ?_⟩, fun ha => ⟨?_, fun b hb => ?_⟩⟩

Premises used: exists_congr, And.intro, Iff.intro
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
refine_1 : ∀ (a : G) (ha : a ∉ H ∧ ∀ x ∉ H, x⁻¹ * a ∈ H) (b : G) (hba : b * a ∈ H) (hb : b ∈ H), False
refine_2 : ∀ (a : G) (ha : a ∉ H ∧ ∀ x ∉ H, x⁻¹ * a ∈ H) (b : G) (hb : b ∉ H), b * a ∈ H
refine_3 : ∀ (a : G) (ha : ∀ (b : G), b * a ∈ H ↔ b ∉ H), a ∉ H
refine_4 : ∀ (a : G) (ha : ∀ (b : G), b * a ∈ H ↔ b ∉ H) (b : G) (hb : b ∉ H), b⁻¹ * a ∈ H
⊢ (∃ x ∉ H, ∀ x_1 ∉ H, x_1⁻¹ * x ∈ H) ↔ ∃ (a : G), ∀ (b : G), b * a ∈ H ↔ b ∉ H

Tactic:
refine exists_congr fun a =>
    ⟨fun ha b => ⟨fun hba hb => ?_, fun hb => ?_⟩, fun ha => ⟨?_, fun b hb => ?_⟩⟩

Premises used: exists_congr, Iff.intro
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
a : G
ha : a ∉ H ∧ ∀ x ∉ H, x⁻¹ * a ∈ H
b : G
hba : b * a ∈ H
hb : b ∈ H
⊢ False

Tactic:
ha.1 ((mul_mem_cancel_left hb).1 hba)

Premises used: And.left, Iff.mp, mul_mem_cancel_left
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
a : G
ha : a ∉ H ∧ ∀ x ∉ H, x⁻¹ * a ∈ H
b : G
hba : b * a ∈ H
hb : b ∈ H
⊢ False

Tactic:
exact ha.1 ((mul_mem_cancel_left hb).1 hba)

Premises used: And.left, Iff.mp, mul_mem_cancel_left
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
a : G
ha : a ∉ H ∧ ∀ x ∉ H, x⁻¹ * a ∈ H
b : G
hb : b ∉ H
⊢ b * a ∈ H

Tactic:
inv_inv b ▸ ha.2 _ (mt (inv_mem_iff (x := b)).1 hb)

Premises used: mt, Eq.rec, inv_mem_iff, And.right, inv_inv, Iff.mp
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
a : G
ha : a ∉ H ∧ ∀ x ∉ H, x⁻¹ * a ∈ H
b : G
hb : b ∉ H
⊢ b * a ∈ H

Tactic:
exact inv_inv b ▸ ha.2 _ (mt (inv_mem_iff (x := b)).1 hb)
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
a : G
ha : ∀ (b : G), b * a ∈ H ↔ b ∉ H
refine_3 : 1 ∈ H
⊢ a ∉ H

Tactic:
rw [← inv_mem_iff (x := a), ← ha, inv_mul_cancel]

Premises used: inv_mul_cancel, inv_mem_iff
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
a : G
ha : ∀ (b : G), b * a ∈ H ↔ b ∉ H
⊢ 1 ∈ H

Tactic:
one_mem _

Premises used: OneMemClass.one_mem
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
a : G
ha : ∀ (b : G), b * a ∈ H ↔ b ∉ H
⊢ 1 ∈ H

Tactic:
exact one_mem _

Premises used: OneMemClass.one_mem
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
a : G
ha : ∀ (b : G), b * a ∈ H ↔ b ∉ H
b : G
hb : b ∉ H
refine_4 : b⁻¹ ∉ H
refine_4₁ refine_4₂ refine_4₃ refine_4₄ : b ∉ H
⊢ b⁻¹ * a ∈ H

Tactic:
rwa [ha, inv_mem_iff (x := b)]

Premises used: inv_mem_iff
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
rw :
  ∀ (a : G),
    (∀ (b : G), Xor (b * a ∈ H) (b ∈ H)) ↔
      ∀ (b : G), Xor (HMul.hMul (α := G) ((Equiv.inv G : (a : G) → G) a : G) b ∈ H) (b ∈ H)
⊢ H.index = 2 ↔ ∃ (a : G), ∀ (b : G), Xor (a * b ∈ H) (b ∈ H)

Tactic:
rw [index_eq_two_iff, (Equiv.inv G).exists_congr]

Premises used: Equiv.inv, Subgroup.index_eq_two_iff, Equiv.exists_congr
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
⊢ ∀ (a : G),
    (∀ (b : G), Xor (b * a ∈ H) (b ∈ H)) ↔
      ∀ (b : G), Xor (HMul.hMul (α := G) ((Equiv.inv G : (a : G) → G) a : G) b ∈ H) (b ∈ H)

Tactic:
fun a ↦ (Equiv.inv G).forall_congr fun b ↦ ?_

Premises used: Equiv.inv, Equiv.forall_congr
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
refine :
  ∀ (a b : G),
    Xor (b * a ∈ H) (b ∈ H) ↔
      Xor (HMul.hMul (α := G) (β := G) ((Equiv.inv G : (a : G) → G) a : G) ((Equiv.inv G : (a : G) → G) b : G) ∈ H)
        (Membership.mem (α := G) H ((Equiv.inv G : (a : G) → G) b : G))
⊢ ∀ (a : G),
    (∀ (b : G), Xor (b * a ∈ H) (b ∈ H)) ↔
      ∀ (b : G), Xor (HMul.hMul (α := G) ((Equiv.inv G : (a : G) → G) a : G) b ∈ H) (b ∈ H)

Tactic:
refine fun a ↦ (Equiv.inv G).forall_congr fun b ↦ ?_

Premises used: Equiv.inv, Equiv.forall_congr
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
a b : G
⊢ Xor (b * a ∈ H) (b ∈ H) ↔
    Xor (HMul.hMul (α := G) (β := G) ((Equiv.inv G : (a : G) → G) a : G) ((Equiv.inv G : (a : G) → G) b : G) ∈ H)
      (Membership.mem (α := G) H ((Equiv.inv G : (a : G) → G) b : G))

Tactic:
simp only [Equiv.inv_apply, inv_mem_iff, ← mul_inv_rev]

Premises used: inv_mem_iff, Equiv.inv_apply, mul_inv_rev
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
simp : (∃ (a : G), ∀ (b : G), (b * a ∈ H ∨ b ∈ H) ∧ ¬(b * a ∈ H ∧ b ∈ H)) ↔ ∃ a ∉ H, ∀ (b : G), b * a ∈ H ∨ b ∈ H
⊢ H.index = 2 ↔ ∃ a ∉ H, ∀ (b : G), b * a ∈ H ∨ b ∈ H

Tactic:
simp only [index_eq_two_iff, xor_iff_or_and_not_and]

Premises used: Subgroup.index_eq_two_iff, xor_iff_or_and_not_and
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
a : G
h : a ∉ H ∧ ∀ (b : G), b * a ∈ H ∨ b ∈ H
b : G
h' : b * a ∈ H ∧ b ∈ H
⊢ a ∈ H

Tactic:
simpa using mul_mem (inv_mem h'.2) h'.1

Premises used: InvMemClass.inv_mem, And.right, And.left, MulMemClass.mul_mem
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
⊢ (∃ (a : G), ∀ (b : G), (b * a ∈ H ∨ b ∈ H) ∧ ¬(b * a ∈ H ∧ b ∈ H)) ↔ ∃ a ∉ H, ∀ (b : G), b * a ∈ H ∨ b ∈ H

Tactic:
exact exists_congr fun a ↦ ⟨fun h ↦ ⟨fun ha ↦ ((h a)).2 ⟨mul_mem ha ha, ha⟩, fun b ↦ (h b).1⟩,
    fun h b ↦ ⟨h.2 b, fun h' ↦ h.1 (by simpa using mul_mem (inv_mem h'.2) h'.1)⟩⟩

Premises used: exists_congr, Iff.intro
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
simp : (∃ (a : G), ∀ (b : G), (a * b ∈ H ∨ b ∈ H) ∧ ¬(a * b ∈ H ∧ b ∈ H)) ↔ ∃ a ∉ H, ∀ (b : G), a * b ∈ H ∨ b ∈ H
⊢ H.index = 2 ↔ ∃ a ∉ H, ∀ (b : G), a * b ∈ H ∨ b ∈ H

Tactic:
simp only [index_eq_two_iff', xor_iff_or_and_not_and]

Premises used: xor_iff_or_and_not_and, Subgroup.index_eq_two_iff'
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
a : G
h : a ∉ H ∧ ∀ (b : G), a * b ∈ H ∨ b ∈ H
b : G
h' : a * b ∈ H ∧ b ∈ H
⊢ a ∈ H

Tactic:
simpa using mul_mem h'.1 (inv_mem h'.2)

Premises used: InvMemClass.inv_mem, And.right, And.left, MulMemClass.mul_mem
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
⊢ (∃ (a : G), ∀ (b : G), (a * b ∈ H ∨ b ∈ H) ∧ ¬(a * b ∈ H ∧ b ∈ H)) ↔ ∃ a ∉ H, ∀ (b : G), a * b ∈ H ∨ b ∈ H

Tactic:
exact exists_congr fun a ↦ ⟨fun h ↦ ⟨fun ha ↦ ((h a)).2 ⟨mul_mem ha ha, ha⟩, fun b ↦ (h b).1⟩,
    fun h b ↦ ⟨h.2 b, fun h' ↦ h.1 (by simpa using mul_mem h'.1 (inv_mem h'.2))⟩⟩

Premises used: exists_congr, Iff.intro
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
⊢ H.relIndex K = 2 ↔ ∃ a ∈ K, ∀ b ∈ K, Xor (b * a ∈ H) (b ∈ H)

Tactic:
simp [Subgroup.relIndex, Subgroup.index_eq_two_iff, mem_subgroupOf]

Premises used: Subgroup.index_eq_two_iff, Subgroup.relIndex, Subgroup.mem_subgroupOf
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
⊢ H.relIndex K = 2 ↔ ∃ a ∈ K, ∀ b ∈ K, Xor (a * b ∈ H) (b ∈ H)

Tactic:
simp [Subgroup.relIndex, Subgroup.index_eq_two_iff', mem_subgroupOf]

Premises used: Subgroup.relIndex, Subgroup.index_eq_two_iff', Subgroup.mem_subgroupOf
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
rw :
  (∃ a ∉ H.subgroupOf K, ∀ (b : ↥K), b * a ∈ H.subgroupOf K ∨ b ∈ H.subgroupOf K) ↔
    ∃ a ∈ K, a ∉ H ∧ ∀ b ∈ K, b * a ∈ H ∨ b ∈ H
⊢ H.relIndex K = 2 ↔ ∃ a ∈ K, a ∉ H ∧ ∀ b ∈ K, b * a ∈ H ∨ b ∈ H

Tactic:
rw [Subgroup.relIndex, Subgroup.index_eq_two_iff_exists_notMem_and]

Premises used: Subgroup.relIndex, Subgroup.index_eq_two_iff_exists_notMem_and
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
simp : (∃ a ∉ H, a ∈ K ∧ ∀ (a_1 : G) (b : a_1 ∈ K), a_1 * a ∈ H ∨ a_1 ∈ H) ↔ ∃ a ∈ K, a ∉ H ∧ ∀ b ∈ K, b * a ∈ H ∨ b ∈ H
⊢ (∃ a ∉ H.subgroupOf K, ∀ (b : ↥K), b * a ∈ H.subgroupOf K ∨ b ∈ H.subgroupOf K) ↔
    ∃ a ∈ K, a ∉ H ∧ ∀ b ∈ K, b * a ∈ H ∨ b ∈ H

Tactic:
simp only [mem_subgroupOf, coe_mul, Subtype.forall, Subtype.exists, exists_and_left, exists_prop]

Premises used: Subtype.exists, exists_and_left, Subtype.forall, exists_prop, Subgroup.coe_mul, Subgroup.mem_subgroupOf
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
⊢ (∃ a ∉ H, a ∈ K ∧ ∀ (a_1 : G) (b : a_1 ∈ K), a_1 * a ∈ H ∨ a_1 ∈ H) ↔ ∃ a ∈ K, a ∉ H ∧ ∀ b ∈ K, b * a ∈ H ∨ b ∈ H

Tactic:
exists_congr fun g ↦ ?_

Premises used: exists_congr
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
refine :
  ∀ (g : G), (g ∉ H ∧ g ∈ K ∧ ∀ (a : G) (b : a ∈ K), a * g ∈ H ∨ a ∈ H) ↔ g ∈ K ∧ g ∉ H ∧ ∀ b ∈ K, b * g ∈ H ∨ b ∈ H
⊢ (∃ a ∉ H, a ∈ K ∧ ∀ (a_1 : G) (b : a_1 ∈ K), a_1 * a ∈ H ∨ a_1 ∈ H) ↔ ∃ a ∈ K, a ∉ H ∧ ∀ b ∈ K, b * a ∈ H ∨ b ∈ H

Tactic:
refine exists_congr fun g ↦ ?_

Premises used: exists_congr
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
g : G
⊢ (g ∉ H ∧ g ∈ K ∧ ∀ (a : G) (b : a ∈ K), a * g ∈ H ∨ a ∈ H) ↔ g ∈ K ∧ g ∉ H ∧ ∀ b ∈ K, b * g ∈ H ∨ b ∈ H

Tactic:
simp only [and_left_comm]

Premises used: and_left_comm
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
rw :
  (∃ a ∉ H.subgroupOf K, ∀ (b : ↥K), a * b ∈ H.subgroupOf K ∨ b ∈ H.subgroupOf K) ↔
    ∃ a ∈ K, a ∉ H ∧ ∀ b ∈ K, a * b ∈ H ∨ b ∈ H
⊢ H.relIndex K = 2 ↔ ∃ a ∈ K, a ∉ H ∧ ∀ b ∈ K, a * b ∈ H ∨ b ∈ H

Tactic:
rw [Subgroup.relIndex, Subgroup.index_eq_two_iff_exists_notMem_and']

Premises used: Subgroup.relIndex, Subgroup.index_eq_two_iff_exists_notMem_and'
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
simp : (∃ a ∉ H, a ∈ K ∧ ∀ (a_1 : G) (b : a_1 ∈ K), a * a_1 ∈ H ∨ a_1 ∈ H) ↔ ∃ a ∈ K, a ∉ H ∧ ∀ b ∈ K, a * b ∈ H ∨ b ∈ H
⊢ (∃ a ∉ H.subgroupOf K, ∀ (b : ↥K), a * b ∈ H.subgroupOf K ∨ b ∈ H.subgroupOf K) ↔
    ∃ a ∈ K, a ∉ H ∧ ∀ b ∈ K, a * b ∈ H ∨ b ∈ H

Tactic:
simp only [mem_subgroupOf, coe_mul, Subtype.forall, Subtype.exists, exists_and_left, exists_prop]

Premises used: Subtype.exists, exists_and_left, Subtype.forall, exists_prop, Subgroup.coe_mul, Subgroup.mem_subgroupOf
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
⊢ (∃ a ∉ H, a ∈ K ∧ ∀ (a_1 : G) (b : a_1 ∈ K), a * a_1 ∈ H ∨ a_1 ∈ H) ↔ ∃ a ∈ K, a ∉ H ∧ ∀ b ∈ K, a * b ∈ H ∨ b ∈ H

Tactic:
exists_congr fun g ↦ ?_

Premises used: exists_congr
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
refine :
  ∀ (g : G), (g ∉ H ∧ g ∈ K ∧ ∀ (a : G) (b : a ∈ K), g * a ∈ H ∨ a ∈ H) ↔ g ∈ K ∧ g ∉ H ∧ ∀ b ∈ K, g * b ∈ H ∨ b ∈ H
⊢ (∃ a ∉ H, a ∈ K ∧ ∀ (a_1 : G) (b : a_1 ∈ K), a * a_1 ∈ H ∨ a_1 ∈ H) ↔ ∃ a ∈ K, a ∉ H ∧ ∀ b ∈ K, a * b ∈ H ∨ b ∈ H

Tactic:
refine exists_congr fun g ↦ ?_

Premises used: exists_congr
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
g : G
⊢ (g ∉ H ∧ g ∈ K ∧ ∀ (a : G) (b : a ∈ K), g * a ∈ H ∨ a ∈ H) ↔ g ∈ K ∧ g ∉ H ∧ ∀ b ∈ K, g * b ∈ H ∨ b ∈ H

Tactic:
simp only [and_left_comm]

Premises used: and_left_comm
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
h : H.index = 2
a b : G
pos : ∀ (ha : a ∈ H), a * b ∈ H ↔ (a ∈ H ↔ b ∈ H)
neg : ∀ (ha : a ∉ H), a * b ∈ H ↔ (a ∈ H ↔ b ∈ H)
⊢ a * b ∈ H ↔ (a ∈ H ↔ b ∈ H)

Tactic:
by_cases ha : a ∈ H
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
h : H.index = 2
a b : G
ha : a ∈ H
⊢ a * b ∈ H ↔ (a ∈ H ↔ b ∈ H)

Tactic:
simp only [ha, true_iff, mul_mem_cancel_left ha]

Premises used: true_iff, mul_mem_cancel_left
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
h : H.index = 2
a b : G
ha : a ∉ H
pos : ∀ (hb : b ∈ H), a * b ∈ H ↔ (a ∈ H ↔ b ∈ H)
neg : ∀ (hb : b ∉ H), a * b ∈ H ↔ (a ∈ H ↔ b ∈ H)
⊢ a * b ∈ H ↔ (a ∈ H ↔ b ∈ H)

Tactic:
by_cases hb : b ∈ H
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
h : H.index = 2
a b : G
ha : a ∉ H
hb : b ∈ H
⊢ a * b ∈ H ↔ (a ∈ H ↔ b ∈ H)

Tactic:
simp only [hb, iff_true, mul_mem_cancel_right hb]

Premises used: iff_true, mul_mem_cancel_right
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
h : H.index = 2
a b : G
ha : a ∉ H
hb : b ∉ H
neg : a * b ∈ H
⊢ a * b ∈ H ↔ (a ∈ H ↔ b ∈ H)

Tactic:
simp only [ha, hb, iff_true]

Premises used: iff_true
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
h : H.index = 2
a b : G
ha : a ∉ H
hb : b ∉ H
neg : ∀ (c : G) (hc : ∀ (b : G), Xor (b * c ∈ H) (b ∈ H)), a * b ∈ H
⊢ a * b ∈ H

Tactic:
rcases index_eq_two_iff.1 h with ⟨c, hc⟩

Premises used: Subgroup.index_eq_two_iff, Iff.mp
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
h : H.index = 2
a b : G
ha : a ∉ H
hb : b ∉ H
c : G
hc : ∀ (b : G), Xor (b * c ∈ H) (b ∈ H)
⊢ a * b ∈ H

Tactic:
(hc _).or.resolve_left ?_

Premises used: Or.resolve_left, Xor.or
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
h : H.index = 2
a b : G
ha : a ∉ H
hb : b ∉ H
c : G
hc : ∀ (b : G), Xor (b * c ∈ H) (b ∈ H)
neg : a * b * c ∉ H
⊢ a * b ∈ H

Tactic:
refine (hc _).or.resolve_left ?_

Premises used: Or.resolve_left, Xor.or
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
h : H.index = 2
a b : G
ha : a ∉ H
hb : b ∉ H
c : G
hc : ∀ (b : G), Xor (b * c ∈ H) (b ∈ H)
neg : a * (b * c) ∉ H
neg₁ neg₂ neg₃ neg₄ : a ∉ H
⊢ a * b * c ∉ H

Tactic:
rwa [mul_assoc, mul_mem_cancel_right ((hc _).or.resolve_right hb)]

Premises used: mul_assoc, Xor.or, Or.resolve_right, mul_mem_cancel_right
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
h : H.index = 2
a : G
rw rw₁ : a ∈ H ↔ a ∈ H
⊢ a * a ∈ H

Tactic:
rw [mul_mem_iff_of_index_two h]

Premises used: Subgroup.mul_mem_iff_of_index_two
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
h : H.index = 2
a : G
⊢ HPow.hPow (β := ℕ) a 2 ∈ H

Tactic:
(pow_two a).symm ▸ mul_self_mem_of_index_two h a

Premises used: pow_two, Eq.rec, Subgroup.mul_self_mem_of_index_two, Eq.symm
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
⊢ index.{u_1} (G := G) ⊤ = 1

Tactic:
Nat.card_eq_one_iff_unique.mpr ⟨QuotientGroup.subsingleton_quotient_top, ⟨1⟩⟩

Premises used: Iff.mpr, Nonempty.intro, Nat.card_eq_one_iff_unique, QuotientGroup.subsingleton_quotient_top, And.intro, Subgroup.index, OfNat.ofNat
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
⊢ index.{u_1} (G := G) ⊥ = Nat.card G

Tactic:
Nat.card_congr QuotientGroup.quotientBot.toEquiv

Premises used: MulEquiv.toEquiv, Nat.card_congr, Subgroup.index, QuotientGroup.quotientBot
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
⊢ relIndex ⊤ H = 1

Tactic:
index_top

Premises used: Subgroup.subgroupOf, Set.Mem, Set.univ, setOf, Subgroup.relIndex, Set.preimage, Subgroup.index_top, Subgroup.comap
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
rw : H.relIndex ⊤ = H.relIndex ⊤ * index.{u_1} (G := G) ⊤
rw₁ : H.relIndex ⊤ = H.relIndex ⊤ * 1
rw₂ rw₃ : H.relIndex ⊤ = H.relIndex ⊤
⊢ H.relIndex ⊤ = H.index

Tactic:
rw [← relIndex_mul_index (show H ≤ ⊤ from le_top), index_top, mul_one]

Premises used: Subgroup.relIndex_mul_index, le_top, Subgroup.index_top, mul_one
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
rw : (subgroupOf ⊥ H).index = Nat.card.{u_1} ↥H
rw₁ : index.{u_1} (G := ↥H) ⊥ = Nat.card.{u_1} ↥H
rw₂ rw₃ : Nat.card.{u_1} ↥H = Nat.card.{u_1} ↥H
⊢ relIndex ⊥ H = Nat.card.{u_1} ↥H

Tactic:
rw [relIndex, bot_subgroupOf, index_bot]

Premises used: Subgroup.relIndex, Subgroup.index_bot, Subgroup.bot_subgroupOf
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
rw : index (G := ↥⊥) (H.subgroupOf ⊥) = 1
rw₁ : index.{u_1} (G := ↥⊥) ⊤ = 1
rw₂ rw₃ : Eq (α := ℕ) 1 1
⊢ H.relIndex ⊥ = 1

Tactic:
rw [relIndex, subgroupOf_bot_eq_top, index_top]

Premises used: Subgroup.relIndex, Subgroup.index_top, Subgroup.subgroupOf_bot_eq_top
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
rw : (H.subgroupOf H).index = 1
rw₁ : index.{u_1} (G := ↥H) ⊤ = 1
rw₂ rw₃ : Eq (α := ℕ) 1 1
⊢ H.relIndex H = 1

Tactic:
rw [relIndex, subgroupOf_self, index_top]

Premises used: Subgroup.subgroupOf_self, Subgroup.relIndex, Subgroup.index_top
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
f : G →* G'
rw : (comap f ⊥).index = Nat.card.{u_2} ↥f.range
rw₁ : relIndex ⊥ f.range = Nat.card.{u_2} ↥f.range
rw₂ rw₃ : Nat.card.{u_2} ↥f.range = Nat.card.{u_2} ↥f.range
⊢ f.ker.index = Nat.card.{u_2} ↥f.range

Tactic:
rw [← MonoidHom.comap_bot, index_comap, relIndex_bot_left]

Premises used: MonoidHom.comap_bot, Subgroup.relIndex_bot_left, Subgroup.index_comap
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
K : Subgroup G
f : G →* G'
rw : (comap f ⊥).relIndex K = Nat.card.{u_2} ↥(map f K)
rw₁ : relIndex ⊥ (map f K) = Nat.card.{u_2} ↥(map f K)
rw₂ rw₃ : Nat.card.{u_2} ↥(map f K) = Nat.card.{u_2} ↥(map f K)
⊢ f.ker.relIndex K = Nat.card.{u_2} ↥(map f K)

Tactic:
rw [← MonoidHom.comap_bot, relIndex_comap, relIndex_bot_left]

Premises used: MonoidHom.comap_bot, Subgroup.relIndex_bot_left, Subgroup.relIndex_comap
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
rw : relIndex ⊥ H * H.index = index.{u_1} (G := G) ⊥
⊢ Nat.card.{u_1} ↥H * H.index = Nat.card G

Tactic:
rw [← relIndex_bot_left, ← index_bot]

Premises used: Subgroup.relIndex_bot_left, Subgroup.index_bot
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
⊢ relIndex ⊥ H * H.index = index.{u_1} (G := G) ⊥

Tactic:
relIndex_mul_index bot_le

Premises used: Subgroup.relIndex_mul_index, bot_le
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
⊢ relIndex ⊥ H * H.index = index.{u_1} (G := G) ⊥

Tactic:
exact relIndex_mul_index bot_le

Premises used: Subgroup.relIndex_mul_index, bot_le
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
f : G →* G'
hf : Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := G') (⇑f : (a : G) → G')
rw : Nat.card.{u_1} (G ⧸ f.ker) ∣ Nat.card G
⊢ Nat.card G' ∣ Nat.card G

Tactic:
rw [← Nat.card_congr (QuotientGroup.quotientKerEquivOfSurjective f hf).toEquiv]

Premises used: MulEquiv.toEquiv, Nat.card_congr, QuotientGroup.quotientKerEquivOfSurjective
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
f : G →* G'
hf : Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := G') (⇑f : (a : G) → G')
⊢ Nat.card.{u_1} (G ⧸ f.ker) ∣ Nat.card G

Tactic:
Dvd.intro_left (Nat.card f.ker) f.ker.card_mul_index

Premises used: Membership.mem, Subtype, Nat.card, Dvd.intro_left, MonoidHom.ker, Subgroup.card_mul_index
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
f : G →* G'
hf : Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := G') (⇑f : (a : G) → G')
⊢ Nat.card.{u_1} (G ⧸ f.ker) ∣ Nat.card G

Tactic:
exact Dvd.intro_left (Nat.card f.ker) f.ker.card_mul_index

Premises used: Membership.mem, Subtype, Nat.card, Dvd.intro_left, MonoidHom.ker, Subgroup.card_mul_index