awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
f : G →* G'
⊢ Nat.card.{u_2} ↥f.range ∣ Nat.card G

Tactic:
card_dvd_of_surjective f.rangeRestrict f.rangeRestrict_surjective

Premises used: MonoidHom.rangeRestrict, Subgroup.card_dvd_of_surjective, MonoidHom.rangeRestrict_surjective
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H : Subgroup G
f : G →* G'
⊢ Nat.card.{u_2} ↥(map f H) ∣ Nat.card.{u_1} ↥H

Tactic:
card_dvd_of_surjective (f.subgroupMap H) (f.subgroupMap_surjective H)

Premises used: Subgroup.card_dvd_of_surjective, MonoidHom.subgroupMap_surjective, MonoidHom.subgroupMap
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H : Subgroup G
f : G →* G'
rw : (map f H).index = (comap f (map f H)).index * f.range.index
rw₁ : (map f H).index = (map f H).relIndex f.range * f.range.index
rw₂ rw₃ : (map f H).index = (map f H).index
⊢ (map f H).index = (H ⊔ f.ker).index * f.range.index

Tactic:
rw [← comap_map_eq, index_comap, relIndex_mul_index (H.map_le_range f)]

Premises used: Subgroup.map_le_range, Subgroup.relIndex_mul_index, Subgroup.comap_map_eq, Subgroup.index_comap
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H : Subgroup G
f : G →* G'
hf : Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := G') (⇑f : (a : G) → G')
rw : (H ⊔ f.ker).index ∣ H.index
⊢ (map f H).index ∣ H.index

Tactic:
rw [index_map, f.range_eq_top_of_surjective hf, index_top, mul_one]

Premises used: MonoidHom.range_eq_top_of_surjective, Subgroup.index_top, mul_one, Subgroup.index_map
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H : Subgroup G
f : G →* G'
hf : Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := G') (⇑f : (a : G) → G')
⊢ (H ⊔ f.ker).index ∣ H.index

Tactic:
index_dvd_of_le le_sup_left

Premises used: le_sup_left, Subgroup.index_dvd_of_le
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H : Subgroup G
f : G →* G'
hf : Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := G') (⇑f : (a : G) → G')
⊢ (H ⊔ f.ker).index ∣ H.index

Tactic:
exact index_dvd_of_le le_sup_left

Premises used: le_sup_left, Subgroup.index_dvd_of_le
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H : Subgroup G
f : G →* G'
hf : f.ker ≤ H
rw : H.index ∣ H.index * f.range.index
⊢ H.index ∣ (map f H).index

Tactic:
rw [index_map, sup_of_le_left hf]

Premises used: Subgroup.index_map, sup_of_le_left
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H : Subgroup G
f : G →* G'
hf : f.ker ≤ H
⊢ H.index ∣ H.index * f.range.index

Tactic:
apply dvd_mul_right

Premises used: dvd_mul_right
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H : Subgroup G
f : G →* G'
hf1 : Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := G') (⇑f : (a : G) → G')
hf2 : f.ker ≤ H
⊢ (map f H).index = H.index

Tactic:
Nat.dvd_antisymm (H.index_map_dvd hf1) (H.dvd_index_map hf2)

Premises used: Subgroup.dvd_index_map, Subgroup.index_map_dvd, Nat.dvd_antisymm
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
f : G →* G'
hf : Bijective.{u_1 + 1, u_2 + 1} (α := G) (β := G') (⇑f : (a : G) → G')
H : Subgroup G
rw : ⊥ ≤ H
⊢ f.ker ≤ H

Tactic:
rw [f.ker_eq_bot_iff.2 hf.1]

Premises used: Iff.mpr, And.left, MonoidHom.ker_eq_bot_iff
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
f : G →* G'
hf : Bijective.{u_1 + 1, u_2 + 1} (α := G) (β := G') (⇑f : (a : G) → G')
H : Subgroup G
⊢ ⊥ ≤ H

Tactic:
bot_le

Premises used: Set.Mem, 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 : Bijective.{u_1 + 1, u_2 + 1} (α := G) (β := G') (⇑f : (a : G) → G')
H : Subgroup G
⊢ ⊥ ≤ H

Tactic:
exact bot_le

Premises used: bot_le
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H : Subgroup G
e : G ≃* G'
⊢ index (map (↑e : G →* G') H) = H.index

Tactic:
index_map_of_bijective e.bijective H

Premises used: Subgroup.index_map_of_bijective
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H : Subgroup G
f : G →* G'
hf : Injective.{u_1 + 1, u_2 + 1} (α := G) (β := G') (⇑f : (a : G) → G')
rw : (H ⊔ f.ker).index * f.range.index = H.index * f.range.index
rw₁ : (H ⊔ ⊥).index * f.range.index = H.index * f.range.index
rw₂ rw₃ : H.index * f.range.index = H.index * f.range.index
⊢ (map f H).index = H.index * f.range.index

Tactic:
rw [H.index_map, f.ker_eq_bot_iff.mpr hf, sup_bot_eq]

Premises used: Iff.mpr, sup_bot_eq, MonoidHom.ker_eq_bot_iff, Subgroup.index_map
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
K : Subgroup ↥H
rw : K.index * H.subtype.range.index = K.index * H.index
rw₁ rw₂ : K.index * H.index = K.index * H.index
⊢ (map H.subtype K).index = K.index * H.index

Tactic:
rw [K.index_map_of_injective H.subtype_injective, H.range_subtype]

Premises used: Subgroup.subtype_injective, Subgroup.index_map_of_injective, Subgroup.range_subtype
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
⊢ H.index = Nat.card.{u_1} (G ⧸ H)

Tactic:
rfl

Premises used: Subgroup.index, rfl
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
rw : Nat.card.{u_1} ↥H * H.index = Nat.card G
rw₁ rw₂ : Nat.card G = Nat.card G
⊢ H.index * Nat.card.{u_1} ↥H = Nat.card G

Tactic:
rw [mul_comm, card_mul_index]

Premises used: mul_comm, Subgroup.card_mul_index
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
⊢ H.index ∣ Nat.card G

Tactic:
⟨Nat.card H, H.index_mul_card.symm⟩

Premises used: Subgroup.index_mul_card, Membership.mem, Subtype, Nat.card, Exists.intro, Eq.symm
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
⊢ H.relIndex K ∣ Nat.card.{u_1} ↥K

Tactic:
(H.subgroupOf K).index_dvd_card

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

Tactic:
eq_zero_of_zero_dvd (hKL ▸ relIndex_dvd_of_le_left L hHK)

Premises used: Eq.rec, Subgroup.relIndex_dvd_of_le_left, eq_zero_of_zero_dvd
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H K L : Subgroup G
hKL : K ≤ L
hHK : H.relIndex K = 0
⊢ H.relIndex L = 0

Tactic:
Finite.card_eq_zero_of_embedding (quotientSubgroupOfEmbeddingOfLE H hKL) hHK

Premises used: Finite.card_eq_zero_of_embedding, Subgroup.relIndex, Subgroup.index, Subgroup.quotientSubgroupOfEmbeddingOfLE
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
f : G →* G'
J K : Subgroup G'
hJK : J.relIndex K ≠ 0
rw : J.relIndex (map f (comap f K)) ≠ 0
⊢ (comap f J).relIndex (comap f K) ≠ 0

Tactic:
rw [relIndex_comap]

Premises used: Subgroup.relIndex_comap
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
f : G →* G'
J K : Subgroup G'
hJK : J.relIndex K ≠ 0
⊢ J.relIndex (map f (comap f K)) ≠ 0

Tactic:
fun h ↦ hJK <| relIndex_eq_zero_of_le_right (map_comap_le _ _) h

Premises used: Subgroup.map_comap_le, Subgroup.relIndex_eq_zero_of_le_right, Not
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
f : G →* G'
J K : Subgroup G'
hJK : J.relIndex K ≠ 0
⊢ J.relIndex (map f (comap f K)) ≠ 0

Tactic:
exact fun h ↦ hJK <| relIndex_eq_zero_of_le_right (map_comap_le _ _) h

Premises used: Subgroup.map_comap_le, Subgroup.relIndex_eq_zero_of_le_right
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
h : H.relIndex K = 0
⊢ H.index = 0

Tactic:
H.relIndex_top_right.symm.trans (relIndex_eq_zero_of_le_right le_top h)

Premises used: le_top, Eq.symm, Subgroup.relIndex_eq_zero_of_le_right, Subgroup.relIndex_top_right, Eq.trans
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H K L : Subgroup G
hHK : H ≤ K
hHL : H.relIndex L ≠ 0
⊢ K.relIndex L ≤ H.relIndex L

Tactic:
Nat.le_of_dvd (Nat.pos_of_ne_zero hHL) (relIndex_dvd_of_le_left L hHK)

Premises used: Subgroup.relIndex_dvd_of_le_left, Nat.pos_of_ne_zero, Nat.le_of_dvd
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H K L : Subgroup G
hKL : K ≤ L
hHL : H.relIndex L ≠ 0
⊢ H.relIndex K ≤ H.relIndex L

Tactic:
Finite.card_le_of_embedding' (quotientSubgroupOfEmbeddingOfLE H hKL) fun h => (hHL h).elim

Premises used: Finite.card_le_of_embedding', False.elim, Subgroup.relIndex, Subgroup.index, Subgroup.quotientSubgroupOfEmbeddingOfLE
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H K L : Subgroup G
hHK : H.relIndex K ≠ 0
hKL : K.relIndex L ≠ 0
⊢ H.relIndex L ≠ 0

Tactic:
fun h =>
  mul_ne_zero (mt (relIndex_eq_zero_of_le_right (show K ⊓ L ≤ K from inf_le_left)) hHK) hKL
    ((relIndex_inf_mul_relIndex H K L).trans (relIndex_eq_zero_of_le_left inf_le_left h))

Premises used: mt, Subgroup.relIndex_inf_mul_relIndex, inf_le_left, mul_ne_zero, Subgroup.relIndex_eq_zero_of_le_left, Subgroup.relIndex_eq_zero_of_le_right, Not, Eq.trans
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H K L : Subgroup G
hH : H.relIndex L ≠ 0
hK : K.relIndex L ≠ 0
⊢ H.relIndex (K ⊓ L) ≠ 0

Tactic:
replace hH : H.relIndex (K ⊓ L) ≠ 0 := mt (relIndex_eq_zero_of_le_right inf_le_right) hH
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H K L : Subgroup G
hK : K.relIndex L ≠ 0
hH : H.relIndex (K ⊓ L) ≠ 0
rw : ∀ (hK : (K ⊓ L).relIndex L ≠ 0) (hH : (H ⊓ (K ⊓ L)).relIndex (K ⊓ L) ≠ 0), (H ⊓ K ⊓ L).relIndex L ≠ 0
⊢ (H ⊓ K).relIndex L ≠ 0

Tactic:
rw [← inf_relIndex_right] at hH hK ⊢

Premises used: Subgroup.inf_relIndex_right
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H K L : Subgroup G
hK : (K ⊓ L).relIndex L ≠ 0
hH : (H ⊓ (K ⊓ L)).relIndex (K ⊓ L) ≠ 0
rw : (H ⊓ (K ⊓ L)).relIndex L ≠ 0
⊢ (H ⊓ K ⊓ L).relIndex L ≠ 0

Tactic:
rw [inf_assoc]

Premises used: inf_assoc
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H K L : Subgroup G
hK : (K ⊓ L).relIndex L ≠ 0
hH : (H ⊓ (K ⊓ L)).relIndex (K ⊓ L) ≠ 0
⊢ (H ⊓ (K ⊓ L)).relIndex L ≠ 0

Tactic:
relIndex_ne_zero_trans hH hK

Premises used: Subgroup.relIndex_ne_zero_trans
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H K L : Subgroup G
hK : (K ⊓ L).relIndex L ≠ 0
hH : (H ⊓ (K ⊓ L)).relIndex (K ⊓ L) ≠ 0
⊢ (H ⊓ (K ⊓ L)).relIndex L ≠ 0

Tactic:
exact relIndex_ne_zero_trans hH hK

Premises used: Subgroup.relIndex_ne_zero_trans
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
hH : H.index ≠ 0
hK : K.index ≠ 0
rw : ∀ (hH : H.relIndex ⊤ ≠ 0) (hK : K.relIndex ⊤ ≠ 0), (H ⊓ K).relIndex ⊤ ≠ 0
⊢ (H ⊓ K).index ≠ 0

Tactic:
rw [← relIndex_top_right] at hH hK ⊢

Premises used: Subgroup.relIndex_top_right
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
hH : H.relIndex ⊤ ≠ 0
hK : K.relIndex ⊤ ≠ 0
⊢ (H ⊓ K).relIndex ⊤ ≠ 0

Tactic:
relIndex_inf_ne_zero hH hK

Premises used: Subgroup.relIndex_inf_ne_zero
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
hH : H.relIndex ⊤ ≠ 0
hK : K.relIndex ⊤ ≠ 0
⊢ (H ⊓ K).relIndex ⊤ ≠ 0

Tactic:
exact relIndex_inf_ne_zero hH hK

Premises used: Subgroup.relIndex_inf_ne_zero
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
J K : Subgroup G
hJK : J.relIndex K ≠ 0
L : Subgroup G
rw : (comap L.subtype J).relIndex (comap L.subtype K) ≠ 0
⊢ (J ⊓ L).relIndex (K ⊓ L) ≠ 0

Tactic:
rw [← range_subtype L, inf_comm, ← map_comap_eq, inf_comm, ← map_comap_eq, ← relIndex_comap,
    comap_map_eq_self_of_injective (subtype_injective L)]

Premises used: Subgroup.map_comap_eq, Subgroup.subtype_injective, inf_comm, Subgroup.comap_map_eq_self_of_injective, Subgroup.relIndex_comap, Subgroup.range_subtype
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
J K : Subgroup G
hJK : J.relIndex K ≠ 0
L : Subgroup G
⊢ (comap L.subtype J).relIndex (comap L.subtype K) ≠ 0

Tactic:
relIndex_comap_ne_zero _ hJK

Premises used: Subgroup.relIndex_comap_ne_zero
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
J K : Subgroup G
hJK : J.relIndex K ≠ 0
L : Subgroup G
⊢ (comap L.subtype J).relIndex (comap L.subtype K) ≠ 0

Tactic:
exact relIndex_comap_ne_zero _ hJK

Premises used: Subgroup.relIndex_comap_ne_zero
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H K L : Subgroup G
pos : ∀ (h : H.relIndex L = 0), (H ⊓ K).relIndex L ≤ H.relIndex L * K.relIndex L
neg : ∀ (h : ¬H.relIndex L = 0), (H ⊓ K).relIndex L ≤ H.relIndex L * K.relIndex L
⊢ (H ⊓ K).relIndex L ≤ H.relIndex L * K.relIndex L

Tactic:
by_cases h : H.relIndex L = 0

Premises used: Subgroup.relIndex
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H K L : Subgroup G
h : H.relIndex L = 0
⊢ (H ⊓ K).relIndex L ≤ H.relIndex L * K.relIndex L

Tactic:
simp [relIndex_eq_zero_of_le_left inf_le_left h]

Premises used: inf_le_left, Subgroup.relIndex_eq_zero_of_le_left
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H K L : Subgroup G
h : ¬H.relIndex L = 0
neg : H.relIndex (K ⊓ L) * K.relIndex L ≤ H.relIndex L * K.relIndex L
⊢ (H ⊓ K).relIndex L ≤ H.relIndex L * K.relIndex L

Tactic:
rw [← inf_relIndex_right, inf_assoc, ← relIndex_mul_relIndex _ _ L inf_le_right inf_le_right,
    inf_relIndex_right, inf_relIndex_right]

Premises used: inf_le_right, Subgroup.relIndex_mul_relIndex, Subgroup.inf_relIndex_right, inf_assoc
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H K L : Subgroup G
h : ¬H.relIndex L = 0
neg neg₁ : H.relIndex L * K.relIndex L ≤ H.relIndex L * K.relIndex L
⊢ H.relIndex (K ⊓ L) * K.relIndex L ≤ H.relIndex L * K.relIndex L

Tactic:
grw [relIndex_le_of_le_right inf_le_right h]

Premises used: inf_le_right, Subgroup.relIndex_le_of_le_right
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
simp_rw : (H ⊓ K).relIndex ⊤ ≤ H.relIndex ⊤ * K.relIndex ⊤
⊢ (H ⊓ K).index ≤ H.index * K.index

Tactic:
simp_rw [← relIndex_top_right, relIndex_inf_le]

Premises used: Subgroup.relIndex_inf_le, Subgroup.relIndex_top_right
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
L : Subgroup G
ι : Type u_3
_hι : Finite ι
f : ι → Subgroup G
hf : ∀ (i : ι), (f i).relIndex L ≠ 0
⊢ relIndex (⨅ (i : ι), f i) L ≠ 0

Tactic:
haveI := Fintype.ofFinite ι
  (Finset.prod_ne_zero_iff.mpr fun i _hi => hf i) ∘
    Nat.card_pi.symm.trans ∘
      Finite.card_eq_zero_of_embedding (quotientiInfSubgroupOfEmbedding f L)

Premises used: Iff.mpr, Subgroup.quotientiInfSubgroupOfEmbedding, Function.comp, Finite.card_eq_zero_of_embedding, Finset.prod_ne_zero_iff, Nat.card_pi, Eq.symm, Not, Eq.trans
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
L : Subgroup G
ι : Type u_3
inst_1 : Fintype ι
f : ι → Subgroup G
⊢ relIndex (⨅ (i : ι), f i) L ≤ ∏ i : ι, (f i).relIndex L

Tactic:
le_of_le_of_eq
    (Finite.card_le_of_embedding' (quotientiInfSubgroupOfEmbedding f L) fun h =>
      let ⟨i, _hi, h⟩ := Finset.prod_eq_zero_iff.mp (Nat.card_pi.symm.trans h)
      relIndex_eq_zero_of_le_left (iInf_le f i) h)
    Nat.card_pi

Premises used: Subgroup.subgroupOf, iInf, le_of_le_of_eq, Finite.card_le_of_embedding', Subgroup.quotientiInfSubgroupOfEmbedding, Membership.mem, Subtype, Nat.card, HasQuotient.Quotient, Finset.prod_eq_zero_iff, Nat.card_pi, Iff.mp, _private.0.Subgroup.relIndex_iInf_le.match_1, OfNat.ofNat, Eq.symm, Eq, Subgroup.relIndex_eq_zero_of_le_left, iInf_le, Eq.trans
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
ι : Type u_3
inst_1 : Finite ι
f : ι → Subgroup G
hf : ∀ (i : ι), (f i).index ≠ 0
simp_rw : ∀ (hf : ∀ (i : ι), (f i).relIndex ⊤ ≠ 0), relIndex.{u_1} (G := G) (⨅ (i : ι), f i) ⊤ ≠ 0
⊢ index.{u_1} (G := G) (⨅ (i : ι), f i) ≠ 0

Tactic:
simp_rw [← relIndex_top_right] at hf ⊢

Premises used: Subgroup.relIndex_top_right
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
ι : Type u_3
inst_1 : Finite ι
f : ι → Subgroup G
hf : ∀ (i : ι), (f i).relIndex ⊤ ≠ 0
⊢ relIndex.{u_1} (G := G) (⨅ (i : ι), f i) ⊤ ≠ 0

Tactic:
relIndex_iInf_ne_zero hf

Premises used: Subgroup.relIndex_iInf_ne_zero
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
ι : Type u_3
inst_1 : Finite ι
f : ι → Subgroup G
hf : ∀ (i : ι), (f i).relIndex ⊤ ≠ 0
⊢ relIndex.{u_1} (G := G) (⨅ (i : ι), f i) ⊤ ≠ 0

Tactic:
exact relIndex_iInf_ne_zero hf

Premises used: Subgroup.relIndex_iInf_ne_zero
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
ι : Type u_3
inst_1 : Fintype ι
f : ι → Subgroup G
simp_rw : relIndex.{u_1} (G := G) (⨅ (i : ι), f i) ⊤ ≤ ∏ x : ι, (f x).relIndex ⊤
⊢ index.{u_1} (G := G) (⨅ (i : ι), f i) ≤ ∏ i : ι, (f i).index

Tactic:
simp_rw [← relIndex_top_right, relIndex_iInf_le]

Premises used: Subgroup.relIndex_iInf_le, Subgroup.relIndex_top_right
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
⊢ H.index = 1 ↔ H = ⊤

Tactic:
⟨fun h =>
    QuotientGroup.subgroup_eq_top_of_subsingleton H (Nat.card_eq_one_iff_unique.mp h).1,
    fun h => (congr_arg index h).trans index_top⟩

Premises used: QuotientGroup.subgroup_eq_top_of_subsingleton, Nat.card_eq_one_iff_unique, congr_arg, And.left, Subgroup.index, Iff.intro, Iff.mp, Subgroup.index_top, Eq.trans
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
⊢ H.relIndex K = 1 ↔ K ≤ H

Tactic:
index_eq_one.trans subgroupOf_eq_top

Premises used: Subgroup.subgroupOf_eq_top, Subgroup.relIndex, Iff.trans, Subgroup.index_eq_one
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
⊢ Nat.card.{u_1} ↥H = 1 ↔ H = ⊥

Tactic:
H.relIndex_bot_left ▸ relIndex_eq_one.trans le_bot_iff

Premises used: le_bot_iff, Eq.rec, Subgroup.relIndex_bot_left, Subgroup.relIndex_eq_one, Iff.trans
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
hH : H.index ∣ 2
⊢ H.index ≤ 1 ∨ H.index = Nat.succ 1

Tactic:
have := Nat.le_succ_iff.mp (Nat.le_of_dvd two_pos hH)
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
hH : H.index ∣ 2
this : H.index ≤ 1 ∨ H.index = Nat.succ 1
⊢ H.index = 0 ∨ H.index = 1 ∨ H.index = Nat.succ 1

Tactic:
rw [Nat.le_one_iff_eq_zero_or_eq_one, or_assoc] at this

Premises used: Nat.le_one_iff_eq_zero_or_eq_one, or_assoc
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
hH : H.index ∣ 2
this : H.index = 0 ∨ H.index = 1 ∨ H.index = Nat.succ 1
⊢ H.index = 1 ∨ H.index = 2

Tactic:
this.resolve_left fun h ↦ (two_ne_zero <| Nat.zero_dvd.mp (h ▸ hH)).elim

Premises used: False.elim, Nat.zero_dvd, Or.resolve_left, two_ne_zero, Iff.mp
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
hH : H.index ∣ 2
this : H.index = 0 ∨ H.index = 1 ∨ H.index = Nat.succ 1
⊢ H.index = 1 ∨ H.index = 2

Tactic:
exact this.resolve_left fun h ↦ (two_ne_zero <| Nat.zero_dvd.mp (h ▸ hH)).elim

Premises used: False.elim, Nat.zero_dvd, Or.resolve_left, two_ne_zero, Iff.mp
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
hH : H.index ∣ 2
inl : ∀ (hH : H.index = 1), ∃ (a : G), ∀ (b : G), b * a ∈ H ∨ b ∈ H
inr : ∀ (hH : H.index = 2), ∃ (a : G), ∀ (b : G), b * a ∈ H ∨ b ∈ H
⊢ ∃ (a : G), ∀ (b : G), b * a ∈ H ∨ b ∈ H

Tactic:
obtain (hH | hH) : H.index = 1 ∨ H.index = 2 := by
      -- This is just showing that 2 is prime, but we do it "longhand" to avoid making any
      -- dependence on number theory files.
      have := Nat.le_succ_iff.mp (Nat.le_of_dvd two_pos hH)
      rw [Nat.le_one_iff_eq_zero_or_eq_one, or_assoc] at this
      exact this.resolve_left fun h ↦ (two_ne_zero <| Nat.zero_dvd.mp (h ▸ hH)).elim

Premises used: Subgroup.index
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
hH_1 : H.index ∣ 2
hH : H.index = 1
⊢ ∃ (a : G), ∀ (b : G), b * a ∈ H ∨ b ∈ H

Tactic:
simp [index_eq_one.mp hH]

Premises used: Iff.mp, Subgroup.index_eq_one
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
hH_1 : H.index ∣ 2
hH : H.index = 2
⊢ ∃ (a : G), ∀ (b : G), b * a ∈ H ∨ b ∈ H

Tactic:
match index_eq_two_iff.mp hH with | ⟨a, ha⟩ => ⟨a, fun b ↦ (ha b).or⟩

Premises used: _private.0.Subgroup.index_dvd_two_iff.match_1, Exists, Subgroup.index_eq_two_iff, Xor.or, Exists.intro, Iff.mp
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
hH_1 : H.index ∣ 2
hH : H.index = 2
⊢ ∃ (a : G), ∀ (b : G), b * a ∈ H ∨ b ∈ H

Tactic:
exact match index_eq_two_iff.mp hH with | ⟨a, ha⟩ => ⟨a, fun b ↦ (ha b).or⟩
-- 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
pos : ∀ (ha' : a ∈ H), H.index ∣ 2
neg : ∀ (ha' : a ∉ H), H.index ∣ 2
⊢ H.index ∣ 2

Tactic:
by_cases ha' : a ∈ H
-- 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
ha' : a ∈ H
this : ∀ (b : G), b ∈ H
⊢ H.index ∣ 2

Tactic:
simp [(eq_top_iff' _).mpr this]

Premises used: Iff.mpr, Subgroup.eq_top_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
ha' : a ∈ H
pos : ∀ (b : G), b ∈ H
⊢ H.index ∣ 2

Tactic:
suffices ∀ b, b ∈ H by simp [(eq_top_iff' _).mpr this]
-- 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
ha' : a ∈ H
b : G
h : b * a ∈ H
⊢ b ∈ H

Tactic:
simpa using mul_mem h (inv_mem ha')

Premises used: InvMemClass.inv_mem, MulMemClass.mul_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
ha' : a ∈ H
⊢ ∀ (b : G), b ∈ H

Tactic:
exact fun b ↦ (ha b).elim (fun h ↦ by simpa using mul_mem h (inv_mem ha')) id

Premises used: id, Or.elim
-- 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
ha' : a ∉ H
⊢ H.index ∣ 2

Tactic:
dvd_of_eq (index_eq_two_iff.mpr
        ⟨a, fun b ↦ (xor_iff_or_and_not_and _ _).mpr ⟨ha b, fun h ↦ ha' ?_⟩⟩)

Premises used: Iff.mpr, HMul.hMul, Membership.mem, Subgroup.index_eq_two_iff, xor_iff_or_and_not_and, And.intro, Exists.intro, dvd_of_eq
-- 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
ha' : a ∉ H
neg : ∀ (b : G) (h : b * a ∈ H ∧ b ∈ H), a ∈ H
⊢ H.index ∣ 2

Tactic:
refine dvd_of_eq (index_eq_two_iff.mpr
        ⟨a, fun b ↦ (xor_iff_or_and_not_and _ _).mpr ⟨ha b, fun h ↦ ha' ?_⟩⟩)

Premises used: Iff.mpr, HMul.hMul, Membership.mem, Subgroup.index_eq_two_iff, xor_iff_or_and_not_and, And.intro, Exists.intro, dvd_of_eq
-- 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
ha' : a ∉ 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
rw :
  ∀ (a : G),
    (∀ (b : G), b * a ∈ H ∨ b ∈ H) ↔ ∀ (b : G), HMul.hMul (α := G) ((Equiv.inv G : (a : G) → G) a : G) b ∈ H ∨ b ∈ H
⊢ H.index ∣ 2 ↔ ∃ (a : G), ∀ (b : G), a * b ∈ H ∨ b ∈ H

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

Premises used: Equiv.inv, Subgroup.index_dvd_two_iff, Equiv.exists_congr
-- 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 : G), 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