Let G be an infinite group and let H be a subgroup s.t. |H| < |G|. Then |G/H| = |G|.

quotient_group_cardinality.lean

import group_theory.quotient_group
import set_theory.ordinal

-- https://math.stackexchange.com/a/370073/783124

namespace cardinal

open quotient_group

variables {α : Type*} [group α] {s : set α} [is_subgroup s]

lemma omega_le_or_omega_le_of_omega_le_mul {a b : cardinal} :
  omega ≤ a * b → omega ≤ a ∨ omega ≤ b :=
by { rw ←not_imp_not, push_neg, exact λ ⟨ha, hb⟩, mul_lt_omega ha hb }

@[to_additive mk_add_subgroup_ne_zero]
lemma mk_subgroup_ne_zero (s : set α) [is_subgroup s] : mk s ≠ 0 :=
ne_zero_iff_nonempty.mpr ⟨⟨1, is_submonoid.one_mem⟩⟩

@[to_additive mk_quotient_add_group_ne_zero]
lemma mk_quotient_group_ne_zero (s : set α) [is_subgroup s] :
  mk (quotient s) ≠ 0 :=
ne_zero_iff_nonempty.mpr (nonempty.intro (quotient.mk' 1))

lemma mk_group_eq_mk_quotient_mul_mk_subgroup :
  mk α = mk (quotient s) * mk s :=
begin
  rw [mul_def, cardinal.eq],
  exact ⟨is_subgroup.group_equiv_quotient_times_subgroup _⟩
end

lemma mk_quotient_group (h : omega ≤ mk α) (hs : mk s < mk α) :
  mk α = mk (quotient s) :=
begin
  rw @mk_group_eq_mk_quotient_mul_mk_subgroup _ _ s _,
  have hs : mk s ≤ mk (quotient s),
  { by_contra this,
    have : mk s * mk (quotient s) < mk α,
    from mul_lt_of_lt h hs (lt.trans (not_le.mp this) hs),
    rw [mul_comm, @mk_group_eq_mk_quotient_mul_mk_subgroup _ _ s _] at this,
    exact (and_not_self _).mp this },
  have h : omega ≤ mk (quotient s) * mk s,
  by rwa ←mk_group_eq_mk_quotient_mul_mk_subgroup,
  cases omega_le_or_omega_le_of_omega_le_mul h with h h,
  { have : mk s ≠ 0, from mk_subgroup_ne_zero _,
    rw mul_eq_max_of_omega_le_left h this,
    exact sup_eq_left.mpr hs },
  { have : mk (quotient s) ≠ 0, by apply mk_quotient_group_ne_zero,
    rw [mul_comm, mul_eq_max_of_omega_le_left h this],
    exact sup_eq_right.mpr hs }
end

variables {β : Type*} [add_group β] {t : set β} [is_add_subgroup t]

open quotient_add_group

-- Unfortunately `to_additive` does not work here.
lemma mk_add_group_eq_mk_quotient_mul_mk_subgroup :
  mk β = mk (quotient t) * mk t :=
begin
  rw [mul_def, cardinal.eq],
  exact ⟨is_add_subgroup.group_equiv_quotient_times_subgroup _⟩
end

attribute [to_additive mk_add_group_eq_mk_quotient_mul_mk_subgroup] mk_group_eq_mk_quotient_mul_mk_subgroup

lemma mk_quotient_add_group (h : omega ≤ mk β) (hs : mk t < mk β) :
  mk β = mk (quotient t) :=
begin
  rw @mk_add_group_eq_mk_quotient_mul_mk_subgroup _ _ t _,
  have hs : mk t ≤ mk (quotient t),
  { by_contra this,
    have : mk t * mk (quotient t) < mk β,
    from mul_lt_of_lt h hs (lt.trans (not_le.mp this) hs),
    rw [mul_comm, @mk_add_group_eq_mk_quotient_mul_mk_subgroup _ _ t _] at this,
    exact (and_not_self _).mp this },
  have h : omega ≤ mk (quotient t) * mk t,
  by rwa ←mk_add_group_eq_mk_quotient_mul_mk_subgroup,
  cases omega_le_or_omega_le_of_omega_le_mul h with h h,
  { have : mk t ≠ 0, from mk_add_subgroup_ne_zero _,
    rw mul_eq_max_of_omega_le_left h this,
    exact sup_eq_left.mpr hs },
  { have : mk (quotient t) ≠ 0, by apply mk_quotient_add_group_ne_zero,
    rw [mul_comm, mul_eq_max_of_omega_le_left h this],
    exact sup_eq_right.mpr hs }
end

attribute [to_additive mk_quotient_add_group] mk_quotient_group

end cardinal