[GOAL]
G : Type u_1
inst✝¹ : Group G
H K L : Subgroup G
G' : Type u_2
inst✝ : Group G'
f : G' →* G
hf : Function.Surjective ↑f
⊢ index (comap f H) = index H
[PROOFSTEP]
letI := QuotientGroup.leftRel H
[GOAL]
G : Type u_1
inst✝¹ : Group G
H K L : Subgroup G
G' : Type u_2
inst✝ : Group G'
f : G' →* G
hf : Function.Surjective ↑f
this : Setoid G := QuotientGroup.leftRel H
⊢ index (comap f H) = index H
[PROOFSTEP]
letI := QuotientGroup.leftRel (H.comap f)
[GOAL]
G : Type u_1
inst✝¹ : Group G
H K L : Subgroup G
G' : Type u_2
inst✝ : Group G'
f : G' →* G
hf : Function.Surjective ↑f
this✝ : Setoid G := QuotientGroup.leftRel H
this : Setoid G' := QuotientGroup.leftRel (comap f H)
⊢ index (comap f H) = index H
[PROOFSTEP]
have key : ∀ x y : G', Setoid.r x y ↔ Setoid.r (f x) (f y) :=
  by
  simp only [QuotientGroup.leftRel_apply]
  exact fun x y => iff_of_eq (congr_arg (· ∈ H) (by rw [f.map_mul, f.map_inv]))
[GOAL]
G : Type u_1
inst✝¹ : Group G
H K L : Subgroup G
G' : Type u_2
inst✝ : Group G'
f : G' →* G
hf : Function.Surjective ↑f
this✝ : Setoid G := QuotientGroup.leftRel H
this : Setoid G' := QuotientGroup.leftRel (comap f H)
⊢ ∀ (x y : G'), Setoid.r x y ↔ Setoid.r (↑f x) (↑f y)
[PROOFSTEP]
simp only [QuotientGroup.leftRel_apply]
[GOAL]
G : Type u_1
inst✝¹ : Group G
H K L : Subgroup G
G' : Type u_2
inst✝ : Group G'
f : G' →* G
hf : Function.Surjective ↑f
this✝ : Setoid G := QuotientGroup.leftRel H
this : Setoid G' := QuotientGroup.leftRel (comap f H)
⊢ ∀ (x y : G'), x⁻¹ * y ∈ comap f H ↔ (↑f x)⁻¹ * ↑f y ∈ H
[PROOFSTEP]
exact fun x y => iff_of_eq (congr_arg (· ∈ H) (by rw [f.map_mul, f.map_inv]))
[GOAL]
G : Type u_1
inst✝¹ : Group G
H K L : Subgroup G
G' : Type u_2
inst✝ : Group G'
f : G' →* G
hf : Function.Surjective ↑f
this✝ : Setoid G := QuotientGroup.leftRel H
this : Setoid G' := QuotientGroup.leftRel (comap f H)
x y : G'
⊢ ↑f (x⁻¹ * y) = (↑f x)⁻¹ * ↑f y
[PROOFSTEP]
rw [f.map_mul, f.map_inv]
[GOAL]
G : Type u_1
inst✝¹ : Group G
H K L : Subgroup G
G' : Type u_2
inst✝ : Group G'
f : G' →* G
hf : Function.Surjective ↑f
this✝ : Setoid G := QuotientGroup.leftRel H
this : Setoid G' := QuotientGroup.leftRel (comap f H)
key : ∀ (x y : G'), Setoid.r x y ↔ Setoid.r (↑f x) (↑f y)
⊢ index (comap f H) = index H
[PROOFSTEP]
refine' Cardinal.toNat_congr (Equiv.ofBijective (Quotient.map' f fun x y => (key x y).mp) ⟨_, _⟩)
[GOAL]
case refine'_1
G : Type u_1
inst✝¹ : Group G
H K L : Subgroup G
G' : Type u_2
inst✝ : Group G'
f : G' →* G
hf : Function.Surjective ↑f
this✝ : Setoid G := QuotientGroup.leftRel H
this : Setoid G' := QuotientGroup.leftRel (comap f H)
key : ∀ (x y : G'), Setoid.r x y ↔ Setoid.r (↑f x) (↑f y)
⊢ Function.Injective (Quotient.map' ↑f (_ : ∀ (x y : G'), Setoid.r x y → Setoid.r (↑f x) (↑f y)))
[PROOFSTEP]
simp_rw [← Quotient.eq''] at key 
[GOAL]
case refine'_1
G : Type u_1
inst✝¹ : Group G
H K L : Subgroup G
G' : Type u_2
inst✝ : Group G'
f : G' →* G
hf : Function.Surjective ↑f
this✝ : Setoid G := QuotientGroup.leftRel H
this : Setoid G' := QuotientGroup.leftRel (comap f H)
key✝ : ∀ (x y : G'), Setoid.r x y ↔ Setoid.r (↑f x) (↑f y)
key : ∀ (x y : G'), Quotient.mk'' x = Quotient.mk'' y ↔ Quotient.mk'' (↑f x) = Quotient.mk'' (↑f y)
⊢ Function.Injective (Quotient.map' ↑f (_ : ∀ (x y : G'), Setoid.r x y → Setoid.r (↑f x) (↑f y)))
[PROOFSTEP]
refine' Quotient.ind' fun x => _
[GOAL]
case refine'_1
G : Type u_1
inst✝¹ : Group G
H K L : Subgroup G
G' : Type u_2
inst✝ : Group G'
f : G' →* G
hf : Function.Surjective ↑f
this✝ : Setoid G := QuotientGroup.leftRel H
this : Setoid G' := QuotientGroup.leftRel (comap f H)
key✝ : ∀ (x y : G'), Setoid.r x y ↔ Setoid.r (↑f x) (↑f y)
key : ∀ (x y : G'), Quotient.mk'' x = Quotient.mk'' y ↔ Quotient.mk'' (↑f x) = Quotient.mk'' (↑f y)
x : G'
⊢ ∀ ⦃a₂ : G' ⧸ comap f H⦄,
    Quotient.map' ↑f (_ : ∀ (x y : G'), Setoid.r x y → Setoid.r (↑f x) (↑f y)) (Quotient.mk'' x) =
        Quotient.map' ↑f (_ : ∀ (x y : G'), Setoid.r x y → Setoid.r (↑f x) (↑f y)) a₂ →
      Quotient.mk'' x = a₂
[PROOFSTEP]
refine' Quotient.ind' fun y => _
[GOAL]
case refine'_1
G : Type u_1
inst✝¹ : Group G
H K L : Subgroup G
G' : Type u_2
inst✝ : Group G'
f : G' →* G
hf : Function.Surjective ↑f
this✝ : Setoid G := QuotientGroup.leftRel H
this : Setoid G' := QuotientGroup.leftRel (comap f H)
key✝ : ∀ (x y : G'), Setoid.r x y ↔ Setoid.r (↑f x) (↑f y)
key : ∀ (x y : G'), Quotient.mk'' x = Quotient.mk'' y ↔ Quotient.mk'' (↑f x) = Quotient.mk'' (↑f y)
x y : G'
⊢ Quotient.map' ↑f (_ : ∀ (x y : G'), Setoid.r x y → Setoid.r (↑f x) (↑f y)) (Quotient.mk'' x) =
      Quotient.map' ↑f (_ : ∀ (x y : G'), Setoid.r x y → Setoid.r (↑f x) (↑f y)) (Quotient.mk'' y) →
    Quotient.mk'' x = Quotient.mk'' y
[PROOFSTEP]
exact (key x y).mpr
[GOAL]
case refine'_2
G : Type u_1
inst✝¹ : Group G
H K L : Subgroup G
G' : Type u_2
inst✝ : Group G'
f : G' →* G
hf : Function.Surjective ↑f
this✝ : Setoid G := QuotientGroup.leftRel H
this : Setoid G' := QuotientGroup.leftRel (comap f H)
key : ∀ (x y : G'), Setoid.r x y ↔ Setoid.r (↑f x) (↑f y)
⊢ Function.Surjective (Quotient.map' ↑f (_ : ∀ (x y : G'), Setoid.r x y → Setoid.r (↑f x) (↑f y)))
[PROOFSTEP]
refine' Quotient.ind' fun x => _
[GOAL]
case refine'_2
G : Type u_1
inst✝¹ : Group G
H K L : Subgroup G
G' : Type u_2
inst✝ : Group G'
f : G' →* G
hf : Function.Surjective ↑f
this✝ : Setoid G := QuotientGroup.leftRel H
this : Setoid G' := QuotientGroup.leftRel (comap f H)
key : ∀ (x y : G'), Setoid.r x y ↔ Setoid.r (↑f x) (↑f y)
x : G
⊢ ∃ a, Quotient.map' ↑f (_ : ∀ (x y : G'), Setoid.r x y → Setoid.r (↑f x) (↑f y)) a = Quotient.mk'' x
[PROOFSTEP]
obtain ⟨y, hy⟩ := hf x
[GOAL]
case refine'_2.intro
G : Type u_1
inst✝¹ : Group G
H K L : Subgroup G
G' : Type u_2
inst✝ : Group G'
f : G' →* G
hf : Function.Surjective ↑f
this✝ : Setoid G := QuotientGroup.leftRel H
this : Setoid G' := QuotientGroup.leftRel (comap f H)
key : ∀ (x y : G'), Setoid.r x y ↔ Setoid.r (↑f x) (↑f y)
x : G
y : G'
hy : ↑f y = x
⊢ ∃ a, Quotient.map' ↑f (_ : ∀ (x y : G'), Setoid.r x y → Setoid.r (↑f x) (↑f y)) a = Quotient.mk'' x
[PROOFSTEP]
exact ⟨y, (Quotient.map'_mk'' f _ y).trans (congr_arg Quotient.mk'' hy)⟩
[GOAL]
G : Type u_1
inst✝¹ : Group G
H K L : Subgroup G
G' : Type u_2
inst✝ : Group G'
f : G' →* G
⊢ comap f H = comap (MonoidHom.rangeRestrict f) (subgroupOf H (MonoidHom.range f))
[PROOFSTEP]
rfl
[GOAL]
G : Type u_1
inst✝¹ : Group G
H K✝ L : Subgroup G
G' : Type u_2
inst✝ : Group G'
f : G' →* G
K : Subgroup G'
⊢ relindex (comap f H) K = relindex H (map f K)
[PROOFSTEP]
rw [relindex, subgroupOf, comap_comap, index_comap, ← f.map_range, K.subtype_range]
[GOAL]
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
hHK : H ≤ K
hKL : K ≤ L
⊢ relindex H K * relindex K L = relindex H L
[PROOFSTEP]
rw [← relindex_subgroupOf hKL]
[GOAL]
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
hHK : H ≤ K
hKL : K ≤ L
⊢ relindex (subgroupOf H L) (subgroupOf K L) * relindex K L = relindex H L
[PROOFSTEP]
exact relindex_mul_index fun x hx => hHK hx
[GOAL]
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
⊢ relindex (H ⊓ K) K = relindex H K
[PROOFSTEP]
rw [relindex, relindex, inf_subgroupOf_right]
[GOAL]
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
⊢ relindex (H ⊓ K) H = relindex K H
[PROOFSTEP]
rw [inf_comm, inf_relindex_right]
[GOAL]
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
⊢ relindex H (K ⊓ L) * relindex K L = relindex (H ⊓ K) L
[PROOFSTEP]
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]
[GOAL]
G : Type u_1
inst✝¹ : Group G
H K L : Subgroup G
inst✝ : Normal K
⊢ relindex K (K ⊔ H) = relindex K H
[PROOFSTEP]
rw [sup_comm, relindex_sup_right]
[GOAL]
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
⊢ index H = 2 ↔ ∃ a, ∀ (b : G), Xor' (b * a ∈ H) (b ∈ H)
[PROOFSTEP]
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]
[GOAL]
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
[PROOFSTEP]
refine' exists_congr fun a => ⟨fun ha b => ⟨fun hba hb => _, fun hb => _⟩, fun ha => ⟨_, fun b hb => _⟩⟩
[GOAL]
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
[PROOFSTEP]
exact ha.1 ((mul_mem_cancel_left hb).1 hba)
[GOAL]
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
[PROOFSTEP]
exact inv_inv b ▸ ha.2 _ (mt (inv_mem_iff (x := b)).1 hb)
[GOAL]
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
[PROOFSTEP]
rw [← inv_mem_iff (x := a), ← ha, inv_mul_self]
[GOAL]
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
[PROOFSTEP]
exact one_mem _
[GOAL]
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
[PROOFSTEP]
rwa [ha, inv_mem_iff (x := b)]
[GOAL]
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)
[PROOFSTEP]
by_cases ha : a ∈ H
[GOAL]
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)
[PROOFSTEP]
simp only [ha, true_iff_iff, mul_mem_cancel_left ha]
[GOAL]
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)
[PROOFSTEP]
by_cases hb : b ∈ H
[GOAL]
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)
[PROOFSTEP]
simp only [hb, iff_true_iff, mul_mem_cancel_right hb]
[GOAL]
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)
[PROOFSTEP]
simp only [ha, hb, iff_self_iff, iff_true_iff]
[GOAL]
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
[PROOFSTEP]
rcases index_eq_two_iff.1 h with ⟨c, hc⟩
[GOAL]
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
[PROOFSTEP]
refine' (hc _).or.resolve_left _
[GOAL]
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
[PROOFSTEP]
rwa [mul_assoc, mul_mem_cancel_right ((hc _).or.resolve_right hb)]
[GOAL]
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
h : index H = 2
a : G
⊢ a * a ∈ H
[PROOFSTEP]
rw [mul_mem_iff_of_index_two h]
[GOAL]
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
⊢ relindex H ⊤ = index H
[PROOFSTEP]
rw [← relindex_mul_index (show H ≤ ⊤ from le_top), index_top, mul_one]
[GOAL]
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
⊢ relindex ⊥ H = Nat.card { x // x ∈ H }
[PROOFSTEP]
rw [relindex, bot_subgroupOf, index_bot]
[GOAL]
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
⊢ relindex H ⊥ = 1
[PROOFSTEP]
rw [relindex, subgroupOf_bot_eq_top, index_top]
[GOAL]
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
⊢ relindex H H = 1
[PROOFSTEP]
rw [relindex, subgroupOf_self, index_top]
[GOAL]
G : Type u_1
inst✝¹ : Group G
H✝ K L : Subgroup G
H : Type u_2
inst✝ : Group H
f : G →* H
⊢ index (MonoidHom.ker f) = Nat.card ↑(Set.range ↑f)
[PROOFSTEP]
rw [← MonoidHom.comap_bot, index_comap, relindex_bot_left]
[GOAL]
G : Type u_1
inst✝¹ : Group G
H✝ K L : Subgroup G
H : Type u_2
inst✝ : Group H
f : G →* H
⊢ Nat.card { x // x ∈ MonoidHom.range f } = Nat.card ↑(Set.range ↑f)
[PROOFSTEP]
rfl
[GOAL]
G : Type u_1
inst✝¹ : Group G
H✝ K✝ L : Subgroup G
H : Type u_2
inst✝ : Group H
f : G →* H
K : Subgroup G
⊢ relindex (MonoidHom.ker f) K = Nat.card ↑(↑f '' ↑K)
[PROOFSTEP]
rw [← MonoidHom.comap_bot, relindex_comap, relindex_bot_left]
[GOAL]
G : Type u_1
inst✝¹ : Group G
H✝ K✝ L : Subgroup G
H : Type u_2
inst✝ : Group H
f : G →* H
K : Subgroup G
⊢ Nat.card { x // x ∈ map f K } = Nat.card ↑(↑f '' ↑K)
[PROOFSTEP]
rfl
[GOAL]
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
⊢ Nat.card { x // x ∈ H } * index H = Nat.card G
[PROOFSTEP]
rw [← relindex_bot_left, ← index_bot]
[GOAL]
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
⊢ relindex ⊥ H * index H = index ⊥
[PROOFSTEP]
exact relindex_mul_index bot_le
[GOAL]
G✝ : Type u_1
inst✝² : Group G✝
H✝ K L : Subgroup G✝
G : Type u_2
H : Type u_3
inst✝¹ : Group G
inst✝ : Group H
f : G →* H
hf : Function.Injective ↑f
⊢ Nat.card G ∣ Nat.card H
[PROOFSTEP]
rw [Nat.card_congr (MonoidHom.ofInjective hf).toEquiv]
[GOAL]
G✝ : Type u_1
inst✝² : Group G✝
H✝ K L : Subgroup G✝
G : Type u_2
H : Type u_3
inst✝¹ : Group G
inst✝ : Group H
f : G →* H
hf : Function.Injective ↑f
⊢ Nat.card { x // x ∈ MonoidHom.range f } ∣ Nat.card H
[PROOFSTEP]
exact Dvd.intro f.range.index f.range.card_mul_index
[GOAL]
G✝ : Type u_1
inst✝² : Group G✝
H✝ K L : Subgroup G✝
G : Type u_2
H : Type u_3
inst✝¹ : Group G
inst✝ : Group H
f : G →* H
hf : Function.Surjective ↑f
⊢ Nat.card H ∣ Nat.card G
[PROOFSTEP]
rw [← Nat.card_congr (QuotientGroup.quotientKerEquivOfSurjective f hf).toEquiv]
[GOAL]
G✝ : Type u_1
inst✝² : Group G✝
H✝ K L : Subgroup G✝
G : Type u_2
H : Type u_3
inst✝¹ : Group G
inst✝ : Group H
f : G →* H
hf : Function.Surjective ↑f
⊢ Nat.card (G ⧸ MonoidHom.ker f) ∣ Nat.card G
[PROOFSTEP]
exact Dvd.intro_left (Nat.card f.ker) f.ker.card_mul_index
[GOAL]
G✝ : Type u_1
inst✝⁴ : Group G✝
H✝ K L : Subgroup G✝
G : Type u_2
H : Type u_3
inst✝³ : Group G
inst✝² : Group H
inst✝¹ : Fintype G
inst✝ : Fintype H
f : G →* H
hf : Function.Surjective ↑f
⊢ Fintype.card H ∣ Fintype.card G
[PROOFSTEP]
simp only [← Nat.card_eq_fintype_card, nat_card_dvd_of_surjective f hf]
[GOAL]
G : Type u_1
inst✝¹ : Group G
H K L : Subgroup G
G' : Type u_2
inst✝ : Group G'
f : G →* G'
⊢ index (map f H) = index (H ⊔ MonoidHom.ker f) * index (MonoidHom.range f)
[PROOFSTEP]
rw [← comap_map_eq, index_comap, relindex_mul_index (H.map_le_range f)]
[GOAL]
G : Type u_1
inst✝¹ : Group G
H K L : Subgroup G
G' : Type u_2
inst✝ : Group G'
f : G →* G'
hf : Function.Surjective ↑f
⊢ index (map f H) ∣ index H
[PROOFSTEP]
rw [index_map, f.range_top_of_surjective hf, index_top, mul_one]
[GOAL]
G : Type u_1
inst✝¹ : Group G
H K L : Subgroup G
G' : Type u_2
inst✝ : Group G'
f : G →* G'
hf : Function.Surjective ↑f
⊢ index (H ⊔ MonoidHom.ker f) ∣ index H
[PROOFSTEP]
exact index_dvd_of_le le_sup_left
[GOAL]
G : Type u_1
inst✝¹ : Group G
H K L : Subgroup G
G' : Type u_2
inst✝ : Group G'
f : G →* G'
hf : MonoidHom.ker f ≤ H
⊢ index H ∣ index (map f H)
[PROOFSTEP]
rw [index_map, sup_of_le_left hf]
[GOAL]
G : Type u_1
inst✝¹ : Group G
H K L : Subgroup G
G' : Type u_2
inst✝ : Group G'
f : G →* G'
hf : MonoidHom.ker f ≤ H
⊢ index H ∣ index H * index (MonoidHom.range f)
[PROOFSTEP]
apply dvd_mul_right
[GOAL]
G : Type u_1
inst✝¹ : Group G
H K L : Subgroup G
inst✝ : Fintype G
hH : Fintype { x // x ∈ H }
⊢ index H * Fintype.card { x // x ∈ H } = Fintype.card G
[PROOFSTEP]
rw [← relindex_bot_left_eq_card, ← index_bot_eq_card, mul_comm]
[GOAL]
G : Type u_1
inst✝¹ : Group G
H K L : Subgroup G
inst✝ : Fintype G
hH : Fintype { x // x ∈ H }
⊢ relindex ⊥ H * index H = index ⊥
[PROOFSTEP]
exact relindex_mul_index bot_le
[GOAL]
G : Type u_1
inst✝¹ : Group G
H K L : Subgroup G
inst✝ : Fintype G
⊢ index H ∣ Fintype.card G
[PROOFSTEP]
classical exact ⟨Fintype.card H, H.index_mul_card.symm⟩
[GOAL]
G : Type u_1
inst✝¹ : Group G
H K L : Subgroup G
inst✝ : Fintype G
⊢ index H ∣ Fintype.card G
[PROOFSTEP]
exact ⟨Fintype.card H, H.index_mul_card.symm⟩
[GOAL]
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
hH : relindex H L ≠ 0
hK : relindex K L ≠ 0
⊢ relindex (H ⊓ K) L ≠ 0
[PROOFSTEP]
replace hH : H.relindex (K ⊓ L) ≠ 0 := mt (relindex_eq_zero_of_le_right inf_le_right) hH
[GOAL]
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
hK : relindex K L ≠ 0
hH : relindex H (K ⊓ L) ≠ 0
⊢ relindex (H ⊓ K) L ≠ 0
[PROOFSTEP]
rw [← inf_relindex_right] at hH hK ⊢
[GOAL]
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
hK : relindex (K ⊓ L) L ≠ 0
hH : relindex (H ⊓ (K ⊓ L)) (K ⊓ L) ≠ 0
⊢ relindex (H ⊓ K ⊓ L) L ≠ 0
[PROOFSTEP]
rw [inf_assoc]
[GOAL]
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
hK : relindex (K ⊓ L) L ≠ 0
hH : relindex (H ⊓ (K ⊓ L)) (K ⊓ L) ≠ 0
⊢ relindex (H ⊓ (K ⊓ L)) L ≠ 0
[PROOFSTEP]
exact relindex_ne_zero_trans hH hK
[GOAL]
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
hH : index H ≠ 0
hK : index K ≠ 0
⊢ index (H ⊓ K) ≠ 0
[PROOFSTEP]
rw [← relindex_top_right] at hH hK ⊢
[GOAL]
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
hH : relindex H ⊤ ≠ 0
hK : relindex K ⊤ ≠ 0
⊢ relindex (H ⊓ K) ⊤ ≠ 0
[PROOFSTEP]
exact relindex_inf_ne_zero hH hK
[GOAL]
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
⊢ relindex (H ⊓ K) L ≤ relindex H L * relindex K L
[PROOFSTEP]
by_cases h : H.relindex L = 0
[GOAL]
case pos
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
h : relindex H L = 0
⊢ relindex (H ⊓ K) L ≤ relindex H L * relindex K L
[PROOFSTEP]
exact (le_of_eq (relindex_eq_zero_of_le_left inf_le_left h)).trans (zero_le _)
[GOAL]
case neg
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
h : ¬relindex H L = 0
⊢ relindex (H ⊓ K) L ≤ relindex H L * relindex K L
[PROOFSTEP]
rw [← inf_relindex_right, inf_assoc, ← relindex_mul_relindex _ _ L inf_le_right inf_le_right, inf_relindex_right,
  inf_relindex_right]
[GOAL]
case neg
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
h : ¬relindex H L = 0
⊢ relindex H (K ⊓ L) * relindex K L ≤ relindex H L * relindex K L
[PROOFSTEP]
exact mul_le_mul_right' (relindex_le_of_le_right inf_le_right h) (K.relindex L)
[GOAL]
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
⊢ index (H ⊓ K) ≤ index H * index K
[PROOFSTEP]
simp_rw [← relindex_top_right, relindex_inf_le]
[GOAL]
G : Type u_1
inst✝¹ : Group G
H K L : Subgroup G
ι : Type u_2
inst✝ : Finite ι
f : ι → Subgroup G
hf : ∀ (i : ι), index (f i) ≠ 0
⊢ index (⨅ (i : ι), f i) ≠ 0
[PROOFSTEP]
simp_rw [← relindex_top_right] at hf ⊢
[GOAL]
G : Type u_1
inst✝¹ : Group G
H K L : Subgroup G
ι : Type u_2
inst✝ : Finite ι
f : ι → Subgroup G
hf : ∀ (i : ι), relindex (f i) ⊤ ≠ 0
⊢ relindex (⨅ (i : ι), f i) ⊤ ≠ 0
[PROOFSTEP]
exact relindex_iInf_ne_zero hf
[GOAL]
G : Type u_1
inst✝¹ : Group G
H K L : Subgroup G
ι : Type u_2
inst✝ : Fintype ι
f : ι → Subgroup G
⊢ index (⨅ (i : ι), f i) ≤ ∏ i : ι, index (f i)
[PROOFSTEP]
simp_rw [← relindex_top_right, relindex_iInf_le]
[GOAL]
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
hH : Finite (G ⧸ H)
⊢ index H ≠ 0
[PROOFSTEP]
cases nonempty_fintype (G ⧸ H)
[GOAL]
case intro
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
hH : Finite (G ⧸ H)
val✝ : Fintype (G ⧸ H)
⊢ index H ≠ 0
[PROOFSTEP]
rw [index_eq_card]
[GOAL]
case intro
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
hH : Finite (G ⧸ H)
val✝ : Fintype (G ⧸ H)
⊢ Fintype.card (G ⧸ H) ≠ 0
[PROOFSTEP]
exact Fintype.card_ne_zero
[GOAL]
G : Type u_1
inst✝¹ : Group G
H K L : Subgroup G
inst✝ : FiniteIndex H
⊢ FiniteIndex (normalCore H)
[PROOFSTEP]
rw [normalCore_eq_ker]
[GOAL]
G : Type u_1
inst✝¹ : Group G
H K L : Subgroup G
inst✝ : FiniteIndex H
⊢ FiniteIndex (MonoidHom.ker (MulAction.toPermHom G (G ⧸ H)))
[PROOFSTEP]
infer_instance
[GOAL]
G : Type u_1
inst✝² : Group G
H K L : Subgroup G
inst✝¹ : Finite ↑(commutatorSet G)
inst✝ : Group.FG G
⊢ FiniteIndex (center G)
[PROOFSTEP]
obtain ⟨S, -, hS⟩ := Group.rank_spec G
[GOAL]
case intro.intro
G : Type u_1
inst✝² : Group G
H K L : Subgroup G
inst✝¹ : Finite ↑(commutatorSet G)
inst✝ : Group.FG G
S : Finset G
hS : closure ↑S = ⊤
⊢ FiniteIndex (center G)
[PROOFSTEP]
exact ⟨mt (Finite.card_eq_zero_of_embedding (quotientCenterEmbedding hS)) Finite.card_pos.ne'⟩
[GOAL]
G : Type u_1
inst✝² : Group G
H K L : Subgroup G
inst✝¹ : Finite ↑(commutatorSet G)
inst✝ : Group.FG G
⊢ index (center G) ≤ Nat.card ↑(commutatorSet G) ^ Group.rank G
[PROOFSTEP]
obtain ⟨S, hS1, hS2⟩ := Group.rank_spec G
[GOAL]
case intro.intro
G : Type u_1
inst✝² : Group G
H K L : Subgroup G
inst✝¹ : Finite ↑(commutatorSet G)
inst✝ : Group.FG G
S : Finset G
hS1 : Finset.card S = Group.rank G
hS2 : closure ↑S = ⊤
⊢ index (center G) ≤ Nat.card ↑(commutatorSet G) ^ Group.rank G
[PROOFSTEP]
rw [← hS1, ← Fintype.card_coe, ← Nat.card_eq_fintype_card, ← Finset.coe_sort_coe, ← Nat.card_fun]
[GOAL]
case intro.intro
G : Type u_1
inst✝² : Group G
H K L : Subgroup G
inst✝¹ : Finite ↑(commutatorSet G)
inst✝ : Group.FG G
S : Finset G
hS1 : Finset.card S = Group.rank G
hS2 : closure ↑S = ⊤
⊢ index (center G) ≤ Nat.card (↑↑S → ↑(commutatorSet G))
[PROOFSTEP]
exact Finite.card_le_of_embedding (quotientCenterEmbedding hS2)
