Subgroup_card_mul.lean

import Mathlib.tactic
import Mathlib.GroupTheory.Complement

open Classical
open scoped Pointwise

lemma Subgroup.card_not_eq [Group G] [Fintype G] (H : Subgroup G) :
  Fintype.card ↑H ≠ 0
:= by
  intro F
  rw [Fintype.card_eq_zero_iff] at F
  apply F.false
  use 1; apply one_mem

def QuotientGroup.eq_class_of [Group G] (H : Subgroup G) (s : G) : Set G :=
  {x : G | (⟦s⟧ : G ⧸ H) = ⟦x⟧ }

lemma QuotientGroup.decompose [Group G] (H : Subgroup G)
  (S : Set G) (HS : S ∈ Subgroup.leftTransversals H) :
  ⊤ = ⋃ (s : S),(QuotientGroup.eq_class_of H s)
:= by
  ext h; simp
  unfold eq_class_of; simp
  have Hs := Subgroup.mem_leftTransversals_iff_existsUnique_quotient_mk''_eq.mp HS ⟦h⟧
  obtain ⟨s, Hs, _⟩ := Hs
  use s; simp
  change ⟦↑s⟧ = ⟦h⟧ at Hs
  apply Quotient.exact' Hs

lemma Subgroup.card_subgroupOf_comm [Group G] (H K : Subgroup G) :
  Nat.card (H.subgroupOf K) = Nat.card (K.subgroupOf H)
:= by
  apply Nat.card_congr
  refine {
    toFun := by
      rintro ⟨⟨k, Hk⟩, HK⟩
      apply Subgroup.mem_subgroupOf.mp at HK; simp at HK
      use ⟨k, HK⟩
      apply Subgroup.mem_subgroupOf.mpr; simp
      assumption
    invFun := by
      rintro ⟨⟨h, Hh⟩, HH⟩
      apply Subgroup.mem_subgroupOf.mp at HH; simp at HH
      use ⟨h, HH⟩
      apply Subgroup.mem_subgroupOf.mpr; simp
      assumption
    left_inv := by intro x; simp
    right_inv := by intro x; simp
  }

lemma Subgroup.coarc_subgroupOf_eq_card_inf [Group G] (H K : Subgroup G) :
  Nat.card (H.subgroupOf K) = Nat.card ((H ⊓ K : Subgroup G))
:= by
  apply Nat.card_congr
  refine {
    toFun := by
      rintro ⟨⟨k, Hk⟩, HK⟩
      apply Subgroup.mem_subgroupOf.mp at HK; simp at HK
      use k; constructor<;> simp<;> assumption
    invFun := by
      rintro ⟨x, Hx, Kx⟩; simp at *
      use ⟨x, Kx⟩
      apply Subgroup.mem_subgroupOf.mpr; simp
      assumption
    left_inv := by intro x; simp
    right_inv := by rintro ⟨x, Hx, Hk⟩; simp
  }



lemma Subgroup.card_mul [Group G] [Fintype G] (H K : Subgroup G) :
  Nat.card ↑((H : Set G) * K) = (Nat.card H * Nat.card K) / (Nat.card ↥(H ⊓ K))
:= by

  apply Nat.eq_div_of_mul_eq_left
  · rw [<- Fintype.card_eq_nat_card]
    apply Subgroup.card_not_eq (H ⊓ K)
  ·
    obtain ⟨S, HS, _⟩ := (Subgroup.exists_left_transversal (K.subgroupOf H) 1)
    have ES := Subgroup.card_left_transversal HS
    have Smk := (Subgroup.mem_leftTransversals_iff_existsUnique_quotient_mk''_eq.mp HS)
    have E0 := QuotientGroup.decompose _ _ HS




    have EH :  (↑H : Set G) = (Subtype.val '' ((⋃ (s : ↑S), QuotientGroup.eq_class_of (K.subgroupOf H) ↑s) )) := by
      rw [<- E0]; ext x; simp


    have HK :
      (↑H : Set G) * (↑K : Set G) =
      ⋃₀ {X | ∃ s ∈ S, X = ({↑s} : Set G) *(↑K : Set G)}
      := by
      conv => arg 1; arg 1; rw [EH]
      ext x; simp
      rw [Set.mem_mul]; simp
      unfold QuotientGroup.eq_class_of; simp
      constructor<;> intro Hx
      · obtain ⟨h, ⟨Hh, s, Hs, Ss, E⟩, ⟨k, Kk, Hx⟩⟩ := Hx
        rw [<- Hx]
        unfold HasEquiv.Equiv instHasEquivOfSetoid at E; simp at E
        apply QuotientGroup.leftRel_apply.mp at E
        rw [Subgroup.mem_subgroupOf] at E; simp at E

        use ((fun x => s⁻¹ * x) ⁻¹' (↑K : Set G) : Set G); simp
        constructor
        · use s
          constructor
          · use Hs
          · simp
        · rw [<- mul_assoc]
          apply mul_mem<;> assumption
      · obtain ⟨X, ⟨s, ⟨Hs, Ss⟩, HX⟩, Xt⟩ := Hx
        have : x ∈ (fun x => s⁻¹ * x) ⁻¹' ↑K := by
          rw [<- HX]; assumption
        simp at this
        use s
        constructor
        · use Hs
          use s
          use Hs
          constructor; assumption
          unfold HasEquiv.Equiv instHasEquivOfSetoid; simp
          apply QuotientGroup.leftRel_apply.mpr; simp
          apply one_mem
        · use (s⁻¹ * x)
          constructor; assumption
          rw [<- mul_assoc]; simp


    rw [<- Subgroup.card_mul_index (K.subgroupOf H)]
    conv => arg 2; rw [mul_assoc, mul_comm, Subgroup.card_subgroupOf_comm, Subgroup.coarc_subgroupOf_eq_card_inf]
    simp; left
    rw [Fintype.card_eq_nat_card, Fintype.card_eq_nat_card]
    rw [<- ES, <- Nat.card_prod]
    rw [HK]
    apply Nat.card_congr

    refine {
      toFun := by
        rintro ⟨x,Hx⟩
        simp at Hx
        let Y := Hx.choose
        have HY := Hx.choose_spec.1
        have XY : x ∈ Y := Hx.choose_spec.2
        let s := HY.choose
        have Hs1 : ∃ (Hs : s ∈ H), ⟨s, Hs⟩ ∈ S := HY.choose_spec.1
        have Hs : s ∈ H := Hs1.choose
        have Ss : ⟨s, Hs⟩ ∈ S := Hs1.choose_spec
        have EY : Y = (fun x => s⁻¹ * x) ⁻¹' ↑K := HY.choose_spec.2
        rw [EY] at XY
        simp at XY
        constructor
        · use ⟨s, Hs⟩
        · use s⁻¹ * x
      invFun := by
        intro ⟨⟨⟨s, Hs⟩, Ss⟩, ⟨k, Hk⟩⟩
        use s * k; simp
        use (((fun x => s⁻¹ * x) ⁻¹' ↑K) : Set G); simp
        constructor<;> [skip; exact Hk]
        use s; constructor
        · use Hs
        · simp
      left_inv := by intro x; simp
      right_inv := by
        rintro ⟨⟨⟨s, Hs⟩, Ss⟩, ⟨k, Hk⟩⟩


        have Hx : ↑s * k ∈ {X | ∃ s ∈ S, X = ({↑s} : Set G) * ↑K}.sUnion := by
          simp
          use {s} * K
          constructor
          · use s
            constructor
            · use Hs
            · ext x; simp
          · simp; assumption

        conv => arg 1; arg 1; simp; change ⟨s * k, Hx⟩
        simp at Hx
        let Y := Hx.choose
        have HY := Hx.choose_spec.1
        have XY : (s * k) ∈ Y := Hx.choose_spec.2
        let s' := HY.choose
        have Hs1 : ∃ (Hs' : s' ∈ H), ⟨s', Hs'⟩ ∈ S := HY.choose_spec.1
        have Hs' : s' ∈ H := Hs1.choose
        have Ss' : ⟨s', Hs'⟩ ∈ S := Hs1.choose_spec
        have EY : Y = (fun x => s'⁻¹ * x) ⁻¹' ↑K := HY.choose_spec.2
        rw [EY] at XY
        simp at XY
        simp
        change s' = s ∧ s'⁻¹ * (s  * k) = k
        obtain ⟨⟨⟨s'', Hs''⟩, Ss''⟩, Hs1, Hs2⟩ := Smk ⟦⟨s, Hs⟩⟧
        suffices : s' = s
        rw [this]; constructor; simp; rw [<- mul_assoc]; simp
        have E1 := Hs2 ⟨⟨s, Hs⟩, Ss⟩ rfl; simp at E1
        rw [E1]
        have : (⟦⟨s', Hs'⟩⟧ : H ⧸ (K.subgroupOf H)) = ⟦⟨s, Hs⟩⟧ := by
          apply Quotient.sound'
          apply QuotientGroup.leftRel_apply.mpr
          rw [Subgroup.mem_subgroupOf]; simp
          rw [<- mul_assoc] at XY
          apply inv_mem at Hk
          apply (mul_mem XY) at Hk
          rw [mul_assoc (s'⁻¹ * s)] at Hk; simp at Hk
          assumption
        have E2 := Hs2 ⟨⟨s', Hs'⟩, Ss'⟩ this; simp at E2
        rw [E2]
    }