[GOAL]
G : Type u_1
inst✝² : Group G
H : Subgroup G
inst✝¹ : IsCommutative H
inst✝ : FiniteIndex H
α β x✝ y✝ : ↑(leftTransversals ↑H)
h : diff (MonoidHom.id { x // x ∈ H }) x✝ y✝ = 1
⊢ diff (MonoidHom.id { x // x ∈ H }) y✝ x✝ = 1
[PROOFSTEP]
rw [← diff_inv, h, inv_one]
[GOAL]
G : Type u_1
inst✝² : Group G
H : Subgroup G
inst✝¹ : IsCommutative H
inst✝ : FiniteIndex H
α β x✝ y✝ z✝ : ↑(leftTransversals ↑H)
h : diff (MonoidHom.id { x // x ∈ H }) x✝ y✝ = 1
h' : diff (MonoidHom.id { x // x ∈ H }) y✝ z✝ = 1
⊢ diff (MonoidHom.id { x // x ∈ H }) x✝ z✝ = 1
[PROOFSTEP]
rw [← diff_mul_diff, h, h', one_mul]
[GOAL]
G : Type u_1
inst✝² : Group G
H : Subgroup G
inst✝¹ : IsCommutative H
inst✝ : FiniteIndex H
α β : ↑(leftTransversals ↑H)
⊢ Inhabited (QuotientDiff H)
[PROOFSTEP]
dsimp [QuotientDiff]
  -- porting note: Added `dsimp`
[GOAL]
G : Type u_1
inst✝² : Group G
H : Subgroup G
inst✝¹ : IsCommutative H
inst✝ : FiniteIndex H
α β : ↑(leftTransversals ↑H)
⊢ Inhabited
    (Quotient
      { r := fun α β => diff (MonoidHom.id { x // x ∈ H }) α β = 1,
        iseqv := (_ : Equivalence fun α β => diff (MonoidHom.id { x // x ∈ H }) α β = 1) })
[PROOFSTEP]
infer_instance
[GOAL]
G : Type u_1
inst✝² : Group G
H : Subgroup G
inst✝¹ : IsCommutative H
inst✝ : FiniteIndex H
α β : ↑(leftTransversals ↑H)
hH : Normal H
g : Gᵐᵒᵖ
⊢ diff (MonoidHom.id { x // x ∈ H }) (g • α) (g • β) =
    { val := (unop g)⁻¹ * ↑(diff (MonoidHom.id { x // x ∈ H }) α β) * unop g,
      property := (_ : (unop g)⁻¹ * ↑(diff (MonoidHom.id { x // x ∈ H }) α β) * unop g ∈ H) }
[PROOFSTEP]
letI := H.fintypeQuotientOfFiniteIndex
[GOAL]
G : Type u_1
inst✝² : Group G
H : Subgroup G
inst✝¹ : IsCommutative H
inst✝ : FiniteIndex H
α β : ↑(leftTransversals ↑H)
hH : Normal H
g : Gᵐᵒᵖ
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex H
⊢ diff (MonoidHom.id { x // x ∈ H }) (g • α) (g • β) =
    { val := (unop g)⁻¹ * ↑(diff (MonoidHom.id { x // x ∈ H }) α β) * unop g,
      property := (_ : (unop g)⁻¹ * ↑(diff (MonoidHom.id { x // x ∈ H }) α β) * unop g ∈ H) }
[PROOFSTEP]
let ϕ : H →* H :=
  { toFun := fun h =>
      ⟨g.unop⁻¹ * h * g.unop, hH.mem_comm ((congr_arg (· ∈ H) (mul_inv_cancel_left _ _)).mpr (SetLike.coe_mem _))⟩
    map_one' := by rw [Subtype.ext_iff, coe_mk, coe_one, mul_one, inv_mul_self]
    map_mul' := fun h₁ h₂ => by simp only [Subtype.ext_iff, coe_mk, coe_mul, mul_assoc, mul_inv_cancel_left] }
[GOAL]
G : Type u_1
inst✝² : Group G
H : Subgroup G
inst✝¹ : IsCommutative H
inst✝ : FiniteIndex H
α β : ↑(leftTransversals ↑H)
hH : Normal H
g : Gᵐᵒᵖ
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex H
⊢ (fun h => { val := (unop g)⁻¹ * ↑h * unop g, property := (_ : (unop g)⁻¹ * ↑h * unop g ∈ H) }) 1 = 1
[PROOFSTEP]
rw [Subtype.ext_iff, coe_mk, coe_one, mul_one, inv_mul_self]
[GOAL]
G : Type u_1
inst✝² : Group G
H : Subgroup G
inst✝¹ : IsCommutative H
inst✝ : FiniteIndex H
α β : ↑(leftTransversals ↑H)
hH : Normal H
g : Gᵐᵒᵖ
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex H
h₁ h₂ : { x // x ∈ H }
⊢ OneHom.toFun
      { toFun := fun h => { val := (unop g)⁻¹ * ↑h * unop g, property := (_ : (unop g)⁻¹ * ↑h * unop g ∈ H) },
        map_one' :=
          (_ : (fun h => { val := (unop g)⁻¹ * ↑h * unop g, property := (_ : (unop g)⁻¹ * ↑h * unop g ∈ H) }) 1 = 1) }
      (h₁ * h₂) =
    OneHom.toFun
        { toFun := fun h => { val := (unop g)⁻¹ * ↑h * unop g, property := (_ : (unop g)⁻¹ * ↑h * unop g ∈ H) },
          map_one' :=
            (_ : (fun h => { val := (unop g)⁻¹ * ↑h * unop g, property := (_ : (unop g)⁻¹ * ↑h * unop g ∈ H) }) 1 = 1) }
        h₁ *
      OneHom.toFun
        { toFun := fun h => { val := (unop g)⁻¹ * ↑h * unop g, property := (_ : (unop g)⁻¹ * ↑h * unop g ∈ H) },
          map_one' :=
            (_ : (fun h => { val := (unop g)⁻¹ * ↑h * unop g, property := (_ : (unop g)⁻¹ * ↑h * unop g ∈ H) }) 1 = 1) }
        h₂
[PROOFSTEP]
simp only [Subtype.ext_iff, coe_mk, coe_mul, mul_assoc, mul_inv_cancel_left]
[GOAL]
G : Type u_1
inst✝² : Group G
H : Subgroup G
inst✝¹ : IsCommutative H
inst✝ : FiniteIndex H
α β : ↑(leftTransversals ↑H)
hH : Normal H
g : Gᵐᵒᵖ
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex H
ϕ : { x // x ∈ H } →* { x // x ∈ H } :=
  {
    toOneHom :=
      { toFun := fun h => { val := (unop g)⁻¹ * ↑h * unop g, property := (_ : (unop g)⁻¹ * ↑h * unop g ∈ H) },
        map_one' :=
          (_ : (fun h => { val := (unop g)⁻¹ * ↑h * unop g, property := (_ : (unop g)⁻¹ * ↑h * unop g ∈ H) }) 1 = 1) },
    map_mul' :=
      (_ :
        ∀ (h₁ h₂ : { x // x ∈ H }),
          { val := (unop g)⁻¹ * ↑(h₁ * h₂) * unop g, property := (_ : (unop g)⁻¹ * ↑(h₁ * h₂) * unop g ∈ H) } =
            { val := (unop g)⁻¹ * ↑h₁ * unop g, property := (_ : (unop g)⁻¹ * ↑h₁ * unop g ∈ H) } *
              { val := (unop g)⁻¹ * ↑h₂ * unop g, property := (_ : (unop g)⁻¹ * ↑h₂ * unop g ∈ H) }) }
⊢ diff (MonoidHom.id { x // x ∈ H }) (g • α) (g • β) =
    { val := (unop g)⁻¹ * ↑(diff (MonoidHom.id { x // x ∈ H }) α β) * unop g,
      property := (_ : (unop g)⁻¹ * ↑(diff (MonoidHom.id { x // x ∈ H }) α β) * unop g ∈ H) }
[PROOFSTEP]
refine'
  Eq.trans
    (Finset.prod_bij' (fun q _ => g⁻¹ • q) (fun q _ => Finset.mem_univ _) (fun q _ => Subtype.ext _) (fun q _ => g • q)
      (fun q _ => Finset.mem_univ _) (fun q _ => smul_inv_smul g q) fun q _ => inv_smul_smul g q)
    (map_prod ϕ _ _).symm
[GOAL]
G : Type u_1
inst✝² : Group G
H : Subgroup G
inst✝¹ : IsCommutative H
inst✝ : FiniteIndex H
α β : ↑(leftTransversals ↑H)
hH : Normal H
g : Gᵐᵒᵖ
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex H
ϕ : { x // x ∈ H } →* { x // x ∈ H } :=
  {
    toOneHom :=
      { toFun := fun h => { val := (unop g)⁻¹ * ↑h * unop g, property := (_ : (unop g)⁻¹ * ↑h * unop g ∈ H) },
        map_one' :=
          (_ : (fun h => { val := (unop g)⁻¹ * ↑h * unop g, property := (_ : (unop g)⁻¹ * ↑h * unop g ∈ H) }) 1 = 1) },
    map_mul' :=
      (_ :
        ∀ (h₁ h₂ : { x // x ∈ H }),
          { val := (unop g)⁻¹ * ↑(h₁ * h₂) * unop g, property := (_ : (unop g)⁻¹ * ↑(h₁ * h₂) * unop g ∈ H) } =
            { val := (unop g)⁻¹ * ↑h₁ * unop g, property := (_ : (unop g)⁻¹ * ↑h₁ * unop g ∈ H) } *
              { val := (unop g)⁻¹ * ↑h₂ * unop g, property := (_ : (unop g)⁻¹ * ↑h₂ * unop g ∈ H) }) }
q : G ⧸ H
x✝ : q ∈ Finset.univ
⊢ ↑(↑(MonoidHom.id { x // x ∈ H })
        {
          val :=
            (↑(↑(toEquiv (_ : ↑(g • α) ∈ leftTransversals ↑H)) q))⁻¹ *
              ↑(↑(toEquiv (_ : ↑(g • β) ∈ leftTransversals ↑H)) q),
          property :=
            (_ :
              (↑(↑(toEquiv (_ : ↑(g • α) ∈ leftTransversals ↑H)) q))⁻¹ *
                  ↑(↑(toEquiv (_ : ↑(g • β) ∈ leftTransversals ↑H)) q) ∈
                H) }) =
    ↑(↑ϕ
        (↑(MonoidHom.id { x // x ∈ H })
          {
            val :=
              (↑(↑(toEquiv (_ : ↑α ∈ leftTransversals ↑H)) ((fun q x => g⁻¹ • q) q x✝)))⁻¹ *
                ↑(↑(toEquiv (_ : ↑β ∈ leftTransversals ↑H)) ((fun q x => g⁻¹ • q) q x✝)),
            property :=
              (_ :
                (↑(↑(toEquiv (_ : ↑α ∈ leftTransversals ↑H)) ((fun q x => g⁻¹ • q) q x✝)))⁻¹ *
                    ↑(↑(toEquiv (_ : ↑β ∈ leftTransversals ↑H)) ((fun q x => g⁻¹ • q) q x✝)) ∈
                  H) }))
[PROOFSTEP]
simp only [MonoidHom.id_apply, MonoidHom.coe_mk, OneHom.coe_mk, smul_apply_eq_smul_apply_inv_smul, smul_eq_mul_unop,
  mul_inv_rev, mul_assoc]
[GOAL]
G : Type u_1
inst✝³ : Group G
H : Subgroup G
inst✝² : IsCommutative H
inst✝¹ : FiniteIndex H
α✝ β✝ : ↑(leftTransversals ↑H)
inst✝ : Normal H
g : G
α β : ↑(leftTransversals ↑H)
h : Setoid.r α β
⊢ ↑(diff (MonoidHom.id { x // x ∈ H }) ((fun α => op g⁻¹ • α) α) ((fun α => op g⁻¹ • α) β)) = ↑1
[PROOFSTEP]
rwa [smul_diff_smul', coe_mk, coe_one, mul_eq_one_iff_eq_inv, mul_right_eq_self, ← coe_one, ← Subtype.ext_iff]
[GOAL]
G : Type u_1
inst✝³ : Group G
H : Subgroup G
inst✝² : IsCommutative H
inst✝¹ : FiniteIndex H
α β : ↑(leftTransversals ↑H)
inst✝ : Normal H
q : QuotientDiff H
T : ↑(leftTransversals ↑H)
⊢ (fun α => op 1⁻¹ • α) T = T
[PROOFSTEP]
rw [inv_one]
[GOAL]
G : Type u_1
inst✝³ : Group G
H : Subgroup G
inst✝² : IsCommutative H
inst✝¹ : FiniteIndex H
α β : ↑(leftTransversals ↑H)
inst✝ : Normal H
q : QuotientDiff H
T : ↑(leftTransversals ↑H)
⊢ (fun α => op 1 • α) T = T
[PROOFSTEP]
apply one_smul Gᵐᵒᵖ T
[GOAL]
G : Type u_1
inst✝³ : Group G
H : Subgroup G
inst✝² : IsCommutative H
inst✝¹ : FiniteIndex H
α β : ↑(leftTransversals ↑H)
inst✝ : Normal H
g₁ g₂ : G
q : QuotientDiff H
T : ↑(leftTransversals ↑H)
⊢ (fun α => op (g₁ * g₂)⁻¹ • α) T = (fun α => op g₁⁻¹ • α) ((fun α => op g₂⁻¹ • α) T)
[PROOFSTEP]
rw [mul_inv_rev]
[GOAL]
G : Type u_1
inst✝³ : Group G
H : Subgroup G
inst✝² : IsCommutative H
inst✝¹ : FiniteIndex H
α β : ↑(leftTransversals ↑H)
inst✝ : Normal H
g₁ g₂ : G
q : QuotientDiff H
T : ↑(leftTransversals ↑H)
⊢ (fun α => op (g₂⁻¹ * g₁⁻¹) • α) T = (fun α => op g₁⁻¹ • α) ((fun α => op g₂⁻¹ • α) T)
[PROOFSTEP]
exact mul_smul (op g₁⁻¹) (op g₂⁻¹) T
[GOAL]
G : Type u_1
inst✝³ : Group G
H : Subgroup G
inst✝² : IsCommutative H
inst✝¹ : FiniteIndex H
α β : ↑(leftTransversals ↑H)
inst✝ : Normal H
h : { x // x ∈ H }
⊢ diff (MonoidHom.id { x // x ∈ H }) α (op ↑h • β) = diff (MonoidHom.id { x // x ∈ H }) α β * h ^ index H
[PROOFSTEP]
letI := H.fintypeQuotientOfFiniteIndex
[GOAL]
G : Type u_1
inst✝³ : Group G
H : Subgroup G
inst✝² : IsCommutative H
inst✝¹ : FiniteIndex H
α β : ↑(leftTransversals ↑H)
inst✝ : Normal H
h : { x // x ∈ H }
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex H
⊢ diff (MonoidHom.id { x // x ∈ H }) α (op ↑h • β) = diff (MonoidHom.id { x // x ∈ H }) α β * h ^ index H
[PROOFSTEP]
rw [diff, diff, index_eq_card, ← Finset.card_univ, ← Finset.prod_const, ← Finset.prod_mul_distrib]
[GOAL]
G : Type u_1
inst✝³ : Group G
H : Subgroup G
inst✝² : IsCommutative H
inst✝¹ : FiniteIndex H
α β : ↑(leftTransversals ↑H)
inst✝ : Normal H
h : { x // x ∈ H }
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex H
⊢ (let α_1 := toEquiv (_ : ↑α ∈ leftTransversals ↑H);
    let β_1 := toEquiv (_ : ↑(op ↑h • β) ∈ leftTransversals ↑H);
    ∏ q : G ⧸ H,
      ↑(MonoidHom.id { x // x ∈ H })
        { val := (↑(↑α_1 q))⁻¹ * ↑(↑β_1 q),
          property :=
            (_ :
              (↑(↑(toEquiv (_ : ↑α ∈ leftTransversals ↑H)) q))⁻¹ *
                  ↑(↑(toEquiv (_ : ↑(op ↑h • β) ∈ leftTransversals ↑H)) q) ∈
                H) }) =
    ∏ x : G ⧸ H,
      ↑(MonoidHom.id { x // x ∈ H })
          { val := (↑(↑(toEquiv (_ : ↑α ∈ leftTransversals ↑H)) x))⁻¹ * ↑(↑(toEquiv (_ : ↑β ∈ leftTransversals ↑H)) x),
            property :=
              (_ :
                (↑(↑(toEquiv (_ : ↑α ∈ leftTransversals ↑H)) x))⁻¹ * ↑(↑(toEquiv (_ : ↑β ∈ leftTransversals ↑H)) x) ∈
                  H) } *
        h
[PROOFSTEP]
refine' Finset.prod_congr rfl fun q _ => _
[GOAL]
G : Type u_1
inst✝³ : Group G
H : Subgroup G
inst✝² : IsCommutative H
inst✝¹ : FiniteIndex H
α β : ↑(leftTransversals ↑H)
inst✝ : Normal H
h : { x // x ∈ H }
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex H
q : G ⧸ H
x✝ : q ∈ Finset.univ
⊢ ↑(MonoidHom.id { x // x ∈ H })
      {
        val :=
          (↑(↑(toEquiv (_ : ↑α ∈ leftTransversals ↑H)) q))⁻¹ * ↑(↑(toEquiv (_ : ↑(op ↑h • β) ∈ leftTransversals ↑H)) q),
        property :=
          (_ :
            (↑(↑(toEquiv (_ : ↑α ∈ leftTransversals ↑H)) q))⁻¹ *
                ↑(↑(toEquiv (_ : ↑(op ↑h • β) ∈ leftTransversals ↑H)) q) ∈
              H) } =
    ↑(MonoidHom.id { x // x ∈ H })
        { val := (↑(↑(toEquiv (_ : ↑α ∈ leftTransversals ↑H)) q))⁻¹ * ↑(↑(toEquiv (_ : ↑β ∈ leftTransversals ↑H)) q),
          property :=
            (_ :
              (↑(↑(toEquiv (_ : ↑α ∈ leftTransversals ↑H)) q))⁻¹ * ↑(↑(toEquiv (_ : ↑β ∈ leftTransversals ↑H)) q) ∈
                H) } *
      h
[PROOFSTEP]
simp_rw [Subtype.ext_iff, MonoidHom.id_apply, coe_mul, mul_assoc, mul_right_inj]
[GOAL]
G : Type u_1
inst✝³ : Group G
H : Subgroup G
inst✝² : IsCommutative H
inst✝¹ : FiniteIndex H
α β : ↑(leftTransversals ↑H)
inst✝ : Normal H
h : { x // x ∈ H }
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex H
q : G ⧸ H
x✝ : q ∈ Finset.univ
⊢ ↑(↑(toEquiv (_ : ↑(op ↑h • β) ∈ leftTransversals ↑H)) q) = ↑(↑(toEquiv (_ : ↑β ∈ leftTransversals ↑H)) q) * ↑h
[PROOFSTEP]
rw [smul_apply_eq_smul_apply_inv_smul, smul_eq_mul_unop, unop_op, mul_left_inj, ← Subtype.ext_iff,
  Equiv.apply_eq_iff_eq, inv_smul_eq_iff]
[GOAL]
G : Type u_1
inst✝³ : Group G
H : Subgroup G
inst✝² : IsCommutative H
inst✝¹ : FiniteIndex H
α β : ↑(leftTransversals ↑H)
inst✝ : Normal H
h : { x // x ∈ H }
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex H
q : G ⧸ H
x✝ : q ∈ Finset.univ
⊢ q = op ↑h • q
[PROOFSTEP]
exact self_eq_mul_right.mpr ((QuotientGroup.eq_one_iff _).mpr h.2)
[GOAL]
G : Type u_1
inst✝³ : Group G
H : Subgroup G
inst✝² : IsCommutative H
inst✝¹ : FiniteIndex H
α✝¹ β : ↑(leftTransversals ↑H)
inst✝ : Normal H
hH : Nat.coprime (Nat.card { x // x ∈ H }) (index H)
α✝ : QuotientDiff H
h : { x // x ∈ H }
α : ↑(leftTransversals ↑H)
hα : h • Quotient.mk'' α = Quotient.mk'' α
⊢ h ^ index H = diff (MonoidHom.id { x // x ∈ H }) (op ↑h⁻¹ • α) α
[PROOFSTEP]
rw [← diff_inv, smul_diff', diff_self, one_mul, inv_pow, inv_inv]
[GOAL]
G : Type u_1
inst✝³ : Group G
H : Subgroup G
inst✝² : IsCommutative H
inst✝¹ : FiniteIndex H
α✝¹ β✝¹ : ↑(leftTransversals ↑H)
inst✝ : Normal H
hH : Nat.coprime (Nat.card { x // x ∈ H }) (index H)
α✝ β✝ : QuotientDiff H
β α : ↑(leftTransversals ↑H)
⊢ diff (MonoidHom.id { x // x ∈ H }) β α *
      (↑(powCoprime hH).symm (diff (MonoidHom.id { x // x ∈ H }) β α))⁻¹ ^ index H =
    1
[PROOFSTEP]
rw [inv_pow, ← powCoprime_apply hH, Equiv.apply_symm_apply, mul_inv_self]
[GOAL]
G : Type u
inst✝² : Group G
inst✝¹ : Fintype G
N : Subgroup G
inst✝ : Normal N
h1 : Nat.coprime (Fintype.card { x // x ∈ N }) (index N)
h2 :
  ∀ (G' : Type u) [inst : Group G'] [inst_1 : Fintype G'],
    Fintype.card G' < Fintype.card G →
      ∀ {N' : Subgroup G'} [inst_2 : Normal N'],
        Nat.coprime (Fintype.card { x // x ∈ N' }) (index N') → ∃ H', IsComplement' N' H'
h3 : ∀ (H : Subgroup G), ¬IsComplement' N H
⊢ N ≠ ⊥
[PROOFSTEP]
rintro rfl
[GOAL]
G : Type u
inst✝² : Group G
inst✝¹ : Fintype G
h2 :
  ∀ (G' : Type u) [inst : Group G'] [inst_1 : Fintype G'],
    Fintype.card G' < Fintype.card G →
      ∀ {N' : Subgroup G'} [inst_2 : Normal N'],
        Nat.coprime (Fintype.card { x // x ∈ N' }) (index N') → ∃ H', IsComplement' N' H'
inst✝ : Normal ⊥
h1 : Nat.coprime (Fintype.card { x // x ∈ ⊥ }) (index ⊥)
h3 : ∀ (H : Subgroup G), ¬IsComplement' ⊥ H
⊢ False
[PROOFSTEP]
exact h3 ⊤ isComplement'_bot_top
[GOAL]
G : Type u
inst✝² : Group G
inst✝¹ : Fintype G
N : Subgroup G
inst✝ : Normal N
h1 : Nat.coprime (Fintype.card { x // x ∈ N }) (index N)
h2 :
  ∀ (G' : Type u) [inst : Group G'] [inst_1 : Fintype G'],
    Fintype.card G' < Fintype.card G →
      ∀ {N' : Subgroup G'} [inst_2 : Normal N'],
        Nat.coprime (Fintype.card { x // x ∈ N' }) (index N') → ∃ H', IsComplement' N' H'
h3 : ∀ (H : Subgroup G), ¬IsComplement' N H
K : Subgroup G
hK : K ⊔ N = ⊤
⊢ K = ⊤
[PROOFSTEP]
contrapose! h3
[GOAL]
G : Type u
inst✝² : Group G
inst✝¹ : Fintype G
N : Subgroup G
inst✝ : Normal N
h1 : Nat.coprime (Fintype.card { x // x ∈ N }) (index N)
h2 :
  ∀ (G' : Type u) [inst : Group G'] [inst_1 : Fintype G'],
    Fintype.card G' < Fintype.card G →
      ∀ {N' : Subgroup G'} [inst_2 : Normal N'],
        Nat.coprime (Fintype.card { x // x ∈ N' }) (index N') → ∃ H', IsComplement' N' H'
K : Subgroup G
hK : K ⊔ N = ⊤
h3 : K ≠ ⊤
⊢ ∃ H, IsComplement' N H
[PROOFSTEP]
have h4 : (N.comap K.subtype).index = N.index :=
  by
  rw [← N.relindex_top_right, ← hK]
  exact (relindex_sup_right K N).symm
[GOAL]
G : Type u
inst✝² : Group G
inst✝¹ : Fintype G
N : Subgroup G
inst✝ : Normal N
h1 : Nat.coprime (Fintype.card { x // x ∈ N }) (index N)
h2 :
  ∀ (G' : Type u) [inst : Group G'] [inst_1 : Fintype G'],
    Fintype.card G' < Fintype.card G →
      ∀ {N' : Subgroup G'} [inst_2 : Normal N'],
        Nat.coprime (Fintype.card { x // x ∈ N' }) (index N') → ∃ H', IsComplement' N' H'
K : Subgroup G
hK : K ⊔ N = ⊤
h3 : K ≠ ⊤
⊢ index (comap (Subgroup.subtype K) N) = index N
[PROOFSTEP]
rw [← N.relindex_top_right, ← hK]
[GOAL]
G : Type u
inst✝² : Group G
inst✝¹ : Fintype G
N : Subgroup G
inst✝ : Normal N
h1 : Nat.coprime (Fintype.card { x // x ∈ N }) (index N)
h2 :
  ∀ (G' : Type u) [inst : Group G'] [inst_1 : Fintype G'],
    Fintype.card G' < Fintype.card G →
      ∀ {N' : Subgroup G'} [inst_2 : Normal N'],
        Nat.coprime (Fintype.card { x // x ∈ N' }) (index N') → ∃ H', IsComplement' N' H'
K : Subgroup G
hK : K ⊔ N = ⊤
h3 : K ≠ ⊤
⊢ index (comap (Subgroup.subtype K) N) = relindex N (K ⊔ N)
[PROOFSTEP]
exact (relindex_sup_right K N).symm
[GOAL]
G : Type u
inst✝² : Group G
inst✝¹ : Fintype G
N : Subgroup G
inst✝ : Normal N
h1 : Nat.coprime (Fintype.card { x // x ∈ N }) (index N)
h2 :
  ∀ (G' : Type u) [inst : Group G'] [inst_1 : Fintype G'],
    Fintype.card G' < Fintype.card G →
      ∀ {N' : Subgroup G'} [inst_2 : Normal N'],
        Nat.coprime (Fintype.card { x // x ∈ N' }) (index N') → ∃ H', IsComplement' N' H'
K : Subgroup G
hK : K ⊔ N = ⊤
h3 : K ≠ ⊤
h4 : index (comap (Subgroup.subtype K) N) = index N
⊢ ∃ H, IsComplement' N H
[PROOFSTEP]
have h5 : Fintype.card K < Fintype.card G := by
  rw [← K.index_mul_card]
  exact lt_mul_of_one_lt_left Fintype.card_pos (one_lt_index_of_ne_top h3)
[GOAL]
G : Type u
inst✝² : Group G
inst✝¹ : Fintype G
N : Subgroup G
inst✝ : Normal N
h1 : Nat.coprime (Fintype.card { x // x ∈ N }) (index N)
h2 :
  ∀ (G' : Type u) [inst : Group G'] [inst_1 : Fintype G'],
    Fintype.card G' < Fintype.card G →
      ∀ {N' : Subgroup G'} [inst_2 : Normal N'],
        Nat.coprime (Fintype.card { x // x ∈ N' }) (index N') → ∃ H', IsComplement' N' H'
K : Subgroup G
hK : K ⊔ N = ⊤
h3 : K ≠ ⊤
h4 : index (comap (Subgroup.subtype K) N) = index N
⊢ Fintype.card { x // x ∈ K } < Fintype.card G
[PROOFSTEP]
rw [← K.index_mul_card]
[GOAL]
G : Type u
inst✝² : Group G
inst✝¹ : Fintype G
N : Subgroup G
inst✝ : Normal N
h1 : Nat.coprime (Fintype.card { x // x ∈ N }) (index N)
h2 :
  ∀ (G' : Type u) [inst : Group G'] [inst_1 : Fintype G'],
    Fintype.card G' < Fintype.card G →
      ∀ {N' : Subgroup G'} [inst_2 : Normal N'],
        Nat.coprime (Fintype.card { x // x ∈ N' }) (index N') → ∃ H', IsComplement' N' H'
K : Subgroup G
hK : K ⊔ N = ⊤
h3 : K ≠ ⊤
h4 : index (comap (Subgroup.subtype K) N) = index N
⊢ Fintype.card { x // x ∈ K } < index K * Fintype.card { x // x ∈ K }
[PROOFSTEP]
exact lt_mul_of_one_lt_left Fintype.card_pos (one_lt_index_of_ne_top h3)
[GOAL]
G : Type u
inst✝² : Group G
inst✝¹ : Fintype G
N : Subgroup G
inst✝ : Normal N
h1 : Nat.coprime (Fintype.card { x // x ∈ N }) (index N)
h2 :
  ∀ (G' : Type u) [inst : Group G'] [inst_1 : Fintype G'],
    Fintype.card G' < Fintype.card G →
      ∀ {N' : Subgroup G'} [inst_2 : Normal N'],
        Nat.coprime (Fintype.card { x // x ∈ N' }) (index N') → ∃ H', IsComplement' N' H'
K : Subgroup G
hK : K ⊔ N = ⊤
h3 : K ≠ ⊤
h4 : index (comap (Subgroup.subtype K) N) = index N
h5 : Fintype.card { x // x ∈ K } < Fintype.card G
⊢ ∃ H, IsComplement' N H
[PROOFSTEP]
have h6 : Nat.coprime (Fintype.card (N.comap K.subtype)) (N.comap K.subtype).index :=
  by
  rw [h4]
  exact h1.coprime_dvd_left (card_comap_dvd_of_injective N K.subtype Subtype.coe_injective)
[GOAL]
G : Type u
inst✝² : Group G
inst✝¹ : Fintype G
N : Subgroup G
inst✝ : Normal N
h1 : Nat.coprime (Fintype.card { x // x ∈ N }) (index N)
h2 :
  ∀ (G' : Type u) [inst : Group G'] [inst_1 : Fintype G'],
    Fintype.card G' < Fintype.card G →
      ∀ {N' : Subgroup G'} [inst_2 : Normal N'],
        Nat.coprime (Fintype.card { x // x ∈ N' }) (index N') → ∃ H', IsComplement' N' H'
K : Subgroup G
hK : K ⊔ N = ⊤
h3 : K ≠ ⊤
h4 : index (comap (Subgroup.subtype K) N) = index N
h5 : Fintype.card { x // x ∈ K } < Fintype.card G
⊢ Nat.coprime (Fintype.card { x // x ∈ comap (Subgroup.subtype K) N }) (index (comap (Subgroup.subtype K) N))
[PROOFSTEP]
rw [h4]
[GOAL]
G : Type u
inst✝² : Group G
inst✝¹ : Fintype G
N : Subgroup G
inst✝ : Normal N
h1 : Nat.coprime (Fintype.card { x // x ∈ N }) (index N)
h2 :
  ∀ (G' : Type u) [inst : Group G'] [inst_1 : Fintype G'],
    Fintype.card G' < Fintype.card G →
      ∀ {N' : Subgroup G'} [inst_2 : Normal N'],
        Nat.coprime (Fintype.card { x // x ∈ N' }) (index N') → ∃ H', IsComplement' N' H'
K : Subgroup G
hK : K ⊔ N = ⊤
h3 : K ≠ ⊤
h4 : index (comap (Subgroup.subtype K) N) = index N
h5 : Fintype.card { x // x ∈ K } < Fintype.card G
⊢ Nat.coprime (Fintype.card { x // x ∈ comap (Subgroup.subtype K) N }) (index N)
[PROOFSTEP]
exact h1.coprime_dvd_left (card_comap_dvd_of_injective N K.subtype Subtype.coe_injective)
[GOAL]
G : Type u
inst✝² : Group G
inst✝¹ : Fintype G
N : Subgroup G
inst✝ : Normal N
h1 : Nat.coprime (Fintype.card { x // x ∈ N }) (index N)
h2 :
  ∀ (G' : Type u) [inst : Group G'] [inst_1 : Fintype G'],
    Fintype.card G' < Fintype.card G →
      ∀ {N' : Subgroup G'} [inst_2 : Normal N'],
        Nat.coprime (Fintype.card { x // x ∈ N' }) (index N') → ∃ H', IsComplement' N' H'
K : Subgroup G
hK : K ⊔ N = ⊤
h3 : K ≠ ⊤
h4 : index (comap (Subgroup.subtype K) N) = index N
h5 : Fintype.card { x // x ∈ K } < Fintype.card G
h6 : Nat.coprime (Fintype.card { x // x ∈ comap (Subgroup.subtype K) N }) (index (comap (Subgroup.subtype K) N))
⊢ ∃ H, IsComplement' N H
[PROOFSTEP]
obtain ⟨H, hH⟩ := h2 K h5 h6
[GOAL]
case intro
G : Type u
inst✝² : Group G
inst✝¹ : Fintype G
N : Subgroup G
inst✝ : Normal N
h1 : Nat.coprime (Fintype.card { x // x ∈ N }) (index N)
h2 :
  ∀ (G' : Type u) [inst : Group G'] [inst_1 : Fintype G'],
    Fintype.card G' < Fintype.card G →
      ∀ {N' : Subgroup G'} [inst_2 : Normal N'],
        Nat.coprime (Fintype.card { x // x ∈ N' }) (index N') → ∃ H', IsComplement' N' H'
K : Subgroup G
hK : K ⊔ N = ⊤
h3 : K ≠ ⊤
h4 : index (comap (Subgroup.subtype K) N) = index N
h5 : Fintype.card { x // x ∈ K } < Fintype.card G
h6 : Nat.coprime (Fintype.card { x // x ∈ comap (Subgroup.subtype K) N }) (index (comap (Subgroup.subtype K) N))
H : Subgroup { x // x ∈ K }
hH : IsComplement' (comap (Subgroup.subtype K) N) H
⊢ ∃ H, IsComplement' N H
[PROOFSTEP]
replace hH : Fintype.card (H.map K.subtype) = N.index := by
  rw [← relindex_bot_left_eq_card, ← relindex_comap, MonoidHom.comap_bot, Subgroup.ker_subtype, relindex_bot_left, ←
    IsComplement'.index_eq_card (IsComplement'.symm hH), index_comap, subtype_range, ← relindex_sup_right, hK,
    relindex_top_right]
[GOAL]
G : Type u
inst✝² : Group G
inst✝¹ : Fintype G
N : Subgroup G
inst✝ : Normal N
h1 : Nat.coprime (Fintype.card { x // x ∈ N }) (index N)
h2 :
  ∀ (G' : Type u) [inst : Group G'] [inst_1 : Fintype G'],
    Fintype.card G' < Fintype.card G →
      ∀ {N' : Subgroup G'} [inst_2 : Normal N'],
        Nat.coprime (Fintype.card { x // x ∈ N' }) (index N') → ∃ H', IsComplement' N' H'
K : Subgroup G
hK : K ⊔ N = ⊤
h3 : K ≠ ⊤
h4 : index (comap (Subgroup.subtype K) N) = index N
h5 : Fintype.card { x // x ∈ K } < Fintype.card G
h6 : Nat.coprime (Fintype.card { x // x ∈ comap (Subgroup.subtype K) N }) (index (comap (Subgroup.subtype K) N))
H : Subgroup { x // x ∈ K }
hH : IsComplement' (comap (Subgroup.subtype K) N) H
⊢ Fintype.card { x // x ∈ map (Subgroup.subtype K) H } = index N
[PROOFSTEP]
rw [← relindex_bot_left_eq_card, ← relindex_comap, MonoidHom.comap_bot, Subgroup.ker_subtype, relindex_bot_left, ←
  IsComplement'.index_eq_card (IsComplement'.symm hH), index_comap, subtype_range, ← relindex_sup_right, hK,
  relindex_top_right]
[GOAL]
case intro
G : Type u
inst✝² : Group G
inst✝¹ : Fintype G
N : Subgroup G
inst✝ : Normal N
h1 : Nat.coprime (Fintype.card { x // x ∈ N }) (index N)
h2 :
  ∀ (G' : Type u) [inst : Group G'] [inst_1 : Fintype G'],
    Fintype.card G' < Fintype.card G →
      ∀ {N' : Subgroup G'} [inst_2 : Normal N'],
        Nat.coprime (Fintype.card { x // x ∈ N' }) (index N') → ∃ H', IsComplement' N' H'
K : Subgroup G
hK : K ⊔ N = ⊤
h3 : K ≠ ⊤
h4 : index (comap (Subgroup.subtype K) N) = index N
h5 : Fintype.card { x // x ∈ K } < Fintype.card G
h6 : Nat.coprime (Fintype.card { x // x ∈ comap (Subgroup.subtype K) N }) (index (comap (Subgroup.subtype K) N))
H : Subgroup { x // x ∈ K }
hH : Fintype.card { x // x ∈ map (Subgroup.subtype K) H } = index N
⊢ ∃ H, IsComplement' N H
[PROOFSTEP]
have h7 : Fintype.card N * Fintype.card (H.map K.subtype) = Fintype.card G := by rw [hH, ← N.index_mul_card, mul_comm]
[GOAL]
G : Type u
inst✝² : Group G
inst✝¹ : Fintype G
N : Subgroup G
inst✝ : Normal N
h1 : Nat.coprime (Fintype.card { x // x ∈ N }) (index N)
h2 :
  ∀ (G' : Type u) [inst : Group G'] [inst_1 : Fintype G'],
    Fintype.card G' < Fintype.card G →
      ∀ {N' : Subgroup G'} [inst_2 : Normal N'],
        Nat.coprime (Fintype.card { x // x ∈ N' }) (index N') → ∃ H', IsComplement' N' H'
K : Subgroup G
hK : K ⊔ N = ⊤
h3 : K ≠ ⊤
h4 : index (comap (Subgroup.subtype K) N) = index N
h5 : Fintype.card { x // x ∈ K } < Fintype.card G
h6 : Nat.coprime (Fintype.card { x // x ∈ comap (Subgroup.subtype K) N }) (index (comap (Subgroup.subtype K) N))
H : Subgroup { x // x ∈ K }
hH : Fintype.card { x // x ∈ map (Subgroup.subtype K) H } = index N
⊢ Fintype.card { x // x ∈ N } * Fintype.card { x // x ∈ map (Subgroup.subtype K) H } = Fintype.card G
[PROOFSTEP]
rw [hH, ← N.index_mul_card, mul_comm]
[GOAL]
case intro
G : Type u
inst✝² : Group G
inst✝¹ : Fintype G
N : Subgroup G
inst✝ : Normal N
h1 : Nat.coprime (Fintype.card { x // x ∈ N }) (index N)
h2 :
  ∀ (G' : Type u) [inst : Group G'] [inst_1 : Fintype G'],
    Fintype.card G' < Fintype.card G →
      ∀ {N' : Subgroup G'} [inst_2 : Normal N'],
        Nat.coprime (Fintype.card { x // x ∈ N' }) (index N') → ∃ H', IsComplement' N' H'
K : Subgroup G
hK : K ⊔ N = ⊤
h3 : K ≠ ⊤
h4 : index (comap (Subgroup.subtype K) N) = index N
h5 : Fintype.card { x // x ∈ K } < Fintype.card G
h6 : Nat.coprime (Fintype.card { x // x ∈ comap (Subgroup.subtype K) N }) (index (comap (Subgroup.subtype K) N))
H : Subgroup { x // x ∈ K }
hH : Fintype.card { x // x ∈ map (Subgroup.subtype K) H } = index N
h7 : Fintype.card { x // x ∈ N } * Fintype.card { x // x ∈ map (Subgroup.subtype K) H } = Fintype.card G
⊢ ∃ H, IsComplement' N H
[PROOFSTEP]
have h8 : (Fintype.card N).coprime (Fintype.card (H.map K.subtype)) := by rwa [hH]
[GOAL]
G : Type u
inst✝² : Group G
inst✝¹ : Fintype G
N : Subgroup G
inst✝ : Normal N
h1 : Nat.coprime (Fintype.card { x // x ∈ N }) (index N)
h2 :
  ∀ (G' : Type u) [inst : Group G'] [inst_1 : Fintype G'],
    Fintype.card G' < Fintype.card G →
      ∀ {N' : Subgroup G'} [inst_2 : Normal N'],
        Nat.coprime (Fintype.card { x // x ∈ N' }) (index N') → ∃ H', IsComplement' N' H'
K : Subgroup G
hK : K ⊔ N = ⊤
h3 : K ≠ ⊤
h4 : index (comap (Subgroup.subtype K) N) = index N
h5 : Fintype.card { x // x ∈ K } < Fintype.card G
h6 : Nat.coprime (Fintype.card { x // x ∈ comap (Subgroup.subtype K) N }) (index (comap (Subgroup.subtype K) N))
H : Subgroup { x // x ∈ K }
hH : Fintype.card { x // x ∈ map (Subgroup.subtype K) H } = index N
h7 : Fintype.card { x // x ∈ N } * Fintype.card { x // x ∈ map (Subgroup.subtype K) H } = Fintype.card G
⊢ Nat.coprime (Fintype.card { x // x ∈ N }) (Fintype.card { x // x ∈ map (Subgroup.subtype K) H })
[PROOFSTEP]
rwa [hH]
[GOAL]
case intro
G : Type u
inst✝² : Group G
inst✝¹ : Fintype G
N : Subgroup G
inst✝ : Normal N
h1 : Nat.coprime (Fintype.card { x // x ∈ N }) (index N)
h2 :
  ∀ (G' : Type u) [inst : Group G'] [inst_1 : Fintype G'],
    Fintype.card G' < Fintype.card G →
      ∀ {N' : Subgroup G'} [inst_2 : Normal N'],
        Nat.coprime (Fintype.card { x // x ∈ N' }) (index N') → ∃ H', IsComplement' N' H'
K : Subgroup G
hK : K ⊔ N = ⊤
h3 : K ≠ ⊤
h4 : index (comap (Subgroup.subtype K) N) = index N
h5 : Fintype.card { x // x ∈ K } < Fintype.card G
h6 : Nat.coprime (Fintype.card { x // x ∈ comap (Subgroup.subtype K) N }) (index (comap (Subgroup.subtype K) N))
H : Subgroup { x // x ∈ K }
hH : Fintype.card { x // x ∈ map (Subgroup.subtype K) H } = index N
h7 : Fintype.card { x // x ∈ N } * Fintype.card { x // x ∈ map (Subgroup.subtype K) H } = Fintype.card G
h8 : Nat.coprime (Fintype.card { x // x ∈ N }) (Fintype.card { x // x ∈ map (Subgroup.subtype K) H })
⊢ ∃ H, IsComplement' N H
[PROOFSTEP]
exact ⟨H.map K.subtype, isComplement'_of_coprime h7 h8⟩
[GOAL]
G : Type u
inst✝³ : Group G
inst✝² : Fintype G
N : Subgroup G
inst✝¹ : Normal N
h1 : Nat.coprime (Fintype.card { x // x ∈ N }) (index N)
h2 :
  ∀ (G' : Type u) [inst : Group G'] [inst_1 : Fintype G'],
    Fintype.card G' < Fintype.card G →
      ∀ {N' : Subgroup G'} [inst_2 : Normal N'],
        Nat.coprime (Fintype.card { x // x ∈ N' }) (index N') → ∃ H', IsComplement' N' H'
h3 : ∀ (H : Subgroup G), ¬IsComplement' N H
K : Subgroup G
inst✝ : Normal K
hK : K ≤ N
⊢ K = ⊥ ∨ K = N
[PROOFSTEP]
have : Function.Surjective (QuotientGroup.mk' K) := Quotient.surjective_Quotient_mk''
[GOAL]
G : Type u
inst✝³ : Group G
inst✝² : Fintype G
N : Subgroup G
inst✝¹ : Normal N
h1 : Nat.coprime (Fintype.card { x // x ∈ N }) (index N)
h2 :
  ∀ (G' : Type u) [inst : Group G'] [inst_1 : Fintype G'],
    Fintype.card G' < Fintype.card G →
      ∀ {N' : Subgroup G'} [inst_2 : Normal N'],
        Nat.coprime (Fintype.card { x // x ∈ N' }) (index N') → ∃ H', IsComplement' N' H'
h3 : ∀ (H : Subgroup G), ¬IsComplement' N H
K : Subgroup G
inst✝ : Normal K
hK : K ≤ N
this : Function.Surjective ↑(QuotientGroup.mk' K)
⊢ K = ⊥ ∨ K = N
[PROOFSTEP]
have h4 := step1 h1 h2 h3
[GOAL]
G : Type u
inst✝³ : Group G
inst✝² : Fintype G
N : Subgroup G
inst✝¹ : Normal N
h1 : Nat.coprime (Fintype.card { x // x ∈ N }) (index N)
h2 :
  ∀ (G' : Type u) [inst : Group G'] [inst_1 : Fintype G'],
    Fintype.card G' < Fintype.card G →
      ∀ {N' : Subgroup G'} [inst_2 : Normal N'],
        Nat.coprime (Fintype.card { x // x ∈ N' }) (index N') → ∃ H', IsComplement' N' H'
h3 : ∀ (H : Subgroup G), ¬IsComplement' N H
K : Subgroup G
inst✝ : Normal K
hK : K ≤ N
this : Function.Surjective ↑(QuotientGroup.mk' K)
h4 : ∀ (K : Subgroup G), K ⊔ N = ⊤ → K = ⊤
⊢ K = ⊥ ∨ K = N
[PROOFSTEP]
contrapose! h4
[GOAL]
G : Type u
inst✝³ : Group G
inst✝² : Fintype G
N : Subgroup G
inst✝¹ : Normal N
h1 : Nat.coprime (Fintype.card { x // x ∈ N }) (index N)
h2 :
  ∀ (G' : Type u) [inst : Group G'] [inst_1 : Fintype G'],
    Fintype.card G' < Fintype.card G →
      ∀ {N' : Subgroup G'} [inst_2 : Normal N'],
        Nat.coprime (Fintype.card { x // x ∈ N' }) (index N') → ∃ H', IsComplement' N' H'
h3 : ∀ (H : Subgroup G), ¬IsComplement' N H
K : Subgroup G
inst✝ : Normal K
hK : K ≤ N
this : Function.Surjective ↑(QuotientGroup.mk' K)
h4 : K ≠ ⊥ ∧ K ≠ N
⊢ ∃ K, K ⊔ N = ⊤ ∧ K ≠ ⊤
[PROOFSTEP]
have h5 : Fintype.card (G ⧸ K) < Fintype.card G :=
  by
  rw [← index_eq_card, ← K.index_mul_card]
  refine' lt_mul_of_one_lt_right (Nat.pos_of_ne_zero index_ne_zero_of_finite) (K.one_lt_card_iff_ne_bot.mpr h4.1)
[GOAL]
G : Type u
inst✝³ : Group G
inst✝² : Fintype G
N : Subgroup G
inst✝¹ : Normal N
h1 : Nat.coprime (Fintype.card { x // x ∈ N }) (index N)
h2 :
  ∀ (G' : Type u) [inst : Group G'] [inst_1 : Fintype G'],
    Fintype.card G' < Fintype.card G →
      ∀ {N' : Subgroup G'} [inst_2 : Normal N'],
        Nat.coprime (Fintype.card { x // x ∈ N' }) (index N') → ∃ H', IsComplement' N' H'
h3 : ∀ (H : Subgroup G), ¬IsComplement' N H
K : Subgroup G
inst✝ : Normal K
hK : K ≤ N
this : Function.Surjective ↑(QuotientGroup.mk' K)
h4 : K ≠ ⊥ ∧ K ≠ N
⊢ Fintype.card (G ⧸ K) < Fintype.card G
[PROOFSTEP]
rw [← index_eq_card, ← K.index_mul_card]
[GOAL]
G : Type u
inst✝³ : Group G
inst✝² : Fintype G
N : Subgroup G
inst✝¹ : Normal N
h1 : Nat.coprime (Fintype.card { x // x ∈ N }) (index N)
h2 :
  ∀ (G' : Type u) [inst : Group G'] [inst_1 : Fintype G'],
    Fintype.card G' < Fintype.card G →
      ∀ {N' : Subgroup G'} [inst_2 : Normal N'],
        Nat.coprime (Fintype.card { x // x ∈ N' }) (index N') → ∃ H', IsComplement' N' H'
h3 : ∀ (H : Subgroup G), ¬IsComplement' N H
K : Subgroup G
inst✝ : Normal K
hK : K ≤ N
this : Function.Surjective ↑(QuotientGroup.mk' K)
h4 : K ≠ ⊥ ∧ K ≠ N
⊢ index K < index K * Fintype.card { x // x ∈ K }
[PROOFSTEP]
refine' lt_mul_of_one_lt_right (Nat.pos_of_ne_zero index_ne_zero_of_finite) (K.one_lt_card_iff_ne_bot.mpr h4.1)
[GOAL]
G : Type u
inst✝³ : Group G
inst✝² : Fintype G
N : Subgroup G
inst✝¹ : Normal N
h1 : Nat.coprime (Fintype.card { x // x ∈ N }) (index N)
h2 :
  ∀ (G' : Type u) [inst : Group G'] [inst_1 : Fintype G'],
    Fintype.card G' < Fintype.card G →
      ∀ {N' : Subgroup G'} [inst_2 : Normal N'],
        Nat.coprime (Fintype.card { x // x ∈ N' }) (index N') → ∃ H', IsComplement' N' H'
h3 : ∀ (H : Subgroup G), ¬IsComplement' N H
K : Subgroup G
inst✝ : Normal K
hK : K ≤ N
this : Function.Surjective ↑(QuotientGroup.mk' K)
h4 : K ≠ ⊥ ∧ K ≠ N
h5 : Fintype.card (G ⧸ K) < Fintype.card G
⊢ ∃ K, K ⊔ N = ⊤ ∧ K ≠ ⊤
[PROOFSTEP]
have h6 : (Fintype.card (N.map (QuotientGroup.mk' K))).coprime (N.map (QuotientGroup.mk' K)).index :=
  by
  have index_map := N.index_map_eq this (by rwa [QuotientGroup.ker_mk'])
  have index_pos : 0 < N.index := Nat.pos_of_ne_zero index_ne_zero_of_finite
  rw [index_map]
  refine' h1.coprime_dvd_left _
  rw [← Nat.mul_dvd_mul_iff_left index_pos, index_mul_card, ← index_map, index_mul_card]
  exact K.card_quotient_dvd_card
[GOAL]
G : Type u
inst✝³ : Group G
inst✝² : Fintype G
N : Subgroup G
inst✝¹ : Normal N
h1 : Nat.coprime (Fintype.card { x // x ∈ N }) (index N)
h2 :
  ∀ (G' : Type u) [inst : Group G'] [inst_1 : Fintype G'],
    Fintype.card G' < Fintype.card G →
      ∀ {N' : Subgroup G'} [inst_2 : Normal N'],
        Nat.coprime (Fintype.card { x // x ∈ N' }) (index N') → ∃ H', IsComplement' N' H'
h3 : ∀ (H : Subgroup G), ¬IsComplement' N H
K : Subgroup G
inst✝ : Normal K
hK : K ≤ N
this : Function.Surjective ↑(QuotientGroup.mk' K)
h4 : K ≠ ⊥ ∧ K ≠ N
h5 : Fintype.card (G ⧸ K) < Fintype.card G
⊢ Nat.coprime (Fintype.card { x // x ∈ map (QuotientGroup.mk' K) N }) (index (map (QuotientGroup.mk' K) N))
[PROOFSTEP]
have index_map := N.index_map_eq this (by rwa [QuotientGroup.ker_mk'])
[GOAL]
G : Type u
inst✝³ : Group G
inst✝² : Fintype G
N : Subgroup G
inst✝¹ : Normal N
h1 : Nat.coprime (Fintype.card { x // x ∈ N }) (index N)
h2 :
  ∀ (G' : Type u) [inst : Group G'] [inst_1 : Fintype G'],
    Fintype.card G' < Fintype.card G →
      ∀ {N' : Subgroup G'} [inst_2 : Normal N'],
        Nat.coprime (Fintype.card { x // x ∈ N' }) (index N') → ∃ H', IsComplement' N' H'
h3 : ∀ (H : Subgroup G), ¬IsComplement' N H
K : Subgroup G
inst✝ : Normal K
hK : K ≤ N
this : Function.Surjective ↑(QuotientGroup.mk' K)
h4 : K ≠ ⊥ ∧ K ≠ N
h5 : Fintype.card (G ⧸ K) < Fintype.card G
⊢ MonoidHom.ker (QuotientGroup.mk' K) ≤ N
[PROOFSTEP]
rwa [QuotientGroup.ker_mk']
[GOAL]
G : Type u
inst✝³ : Group G
inst✝² : Fintype G
N : Subgroup G
inst✝¹ : Normal N
h1 : Nat.coprime (Fintype.card { x // x ∈ N }) (index N)
h2 :
  ∀ (G' : Type u) [inst : Group G'] [inst_1 : Fintype G'],
    Fintype.card G' < Fintype.card G →
      ∀ {N' : Subgroup G'} [inst_2 : Normal N'],
        Nat.coprime (Fintype.card { x // x ∈ N' }) (index N') → ∃ H', IsComplement' N' H'
h3 : ∀ (H : Subgroup G), ¬IsComplement' N H
K : Subgroup G
inst✝ : Normal K
hK : K ≤ N
this : Function.Surjective ↑(QuotientGroup.mk' K)
h4 : K ≠ ⊥ ∧ K ≠ N
h5 : Fintype.card (G ⧸ K) < Fintype.card G
index_map : index (map (QuotientGroup.mk' K) N) = index N
⊢ Nat.coprime (Fintype.card { x // x ∈ map (QuotientGroup.mk' K) N }) (index (map (QuotientGroup.mk' K) N))
[PROOFSTEP]
have index_pos : 0 < N.index := Nat.pos_of_ne_zero index_ne_zero_of_finite
[GOAL]
G : Type u
inst✝³ : Group G
inst✝² : Fintype G
N : Subgroup G
inst✝¹ : Normal N
h1 : Nat.coprime (Fintype.card { x // x ∈ N }) (index N)
h2 :
  ∀ (G' : Type u) [inst : Group G'] [inst_1 : Fintype G'],
    Fintype.card G' < Fintype.card G →
      ∀ {N' : Subgroup G'} [inst_2 : Normal N'],
        Nat.coprime (Fintype.card { x // x ∈ N' }) (index N') → ∃ H', IsComplement' N' H'
h3 : ∀ (H : Subgroup G), ¬IsComplement' N H
K : Subgroup G
inst✝ : Normal K
hK : K ≤ N
this : Function.Surjective ↑(QuotientGroup.mk' K)
h4 : K ≠ ⊥ ∧ K ≠ N
h5 : Fintype.card (G ⧸ K) < Fintype.card G
index_map : index (map (QuotientGroup.mk' K) N) = index N
index_pos : 0 < index N
⊢ Nat.coprime (Fintype.card { x // x ∈ map (QuotientGroup.mk' K) N }) (index (map (QuotientGroup.mk' K) N))
[PROOFSTEP]
rw [index_map]
[GOAL]
G : Type u
inst✝³ : Group G
inst✝² : Fintype G
N : Subgroup G
inst✝¹ : Normal N
h1 : Nat.coprime (Fintype.card { x // x ∈ N }) (index N)
h2 :
  ∀ (G' : Type u) [inst : Group G'] [inst_1 : Fintype G'],
    Fintype.card G' < Fintype.card G →
      ∀ {N' : Subgroup G'} [inst_2 : Normal N'],
        Nat.coprime (Fintype.card { x // x ∈ N' }) (index N') → ∃ H', IsComplement' N' H'
h3 : ∀ (H : Subgroup G), ¬IsComplement' N H
K : Subgroup G
inst✝ : Normal K
hK : K ≤ N
this : Function.Surjective ↑(QuotientGroup.mk' K)
h4 : K ≠ ⊥ ∧ K ≠ N
h5 : Fintype.card (G ⧸ K) < Fintype.card G
index_map : index (map (QuotientGroup.mk' K) N) = index N
index_pos : 0 < index N
⊢ Nat.coprime (Fintype.card { x // x ∈ map (QuotientGroup.mk' K) N }) (index N)
[PROOFSTEP]
refine' h1.coprime_dvd_left _
[GOAL]
G : Type u
inst✝³ : Group G
inst✝² : Fintype G
N : Subgroup G
inst✝¹ : Normal N
h1 : Nat.coprime (Fintype.card { x // x ∈ N }) (index N)
h2 :
  ∀ (G' : Type u) [inst : Group G'] [inst_1 : Fintype G'],
    Fintype.card G' < Fintype.card G →
      ∀ {N' : Subgroup G'} [inst_2 : Normal N'],
        Nat.coprime (Fintype.card { x // x ∈ N' }) (index N') → ∃ H', IsComplement' N' H'
h3 : ∀ (H : Subgroup G), ¬IsComplement' N H
K : Subgroup G
inst✝ : Normal K
hK : K ≤ N
this : Function.Surjective ↑(QuotientGroup.mk' K)
h4 : K ≠ ⊥ ∧ K ≠ N
h5 : Fintype.card (G ⧸ K) < Fintype.card G
index_map : index (map (QuotientGroup.mk' K) N) = index N
index_pos : 0 < index N
⊢ Fintype.card { x // x ∈ map (QuotientGroup.mk' K) N } ∣ Fintype.card { x // x ∈ N }
[PROOFSTEP]
rw [← Nat.mul_dvd_mul_iff_left index_pos, index_mul_card, ← index_map, index_mul_card]
[GOAL]
G : Type u
inst✝³ : Group G
inst✝² : Fintype G
N : Subgroup G
inst✝¹ : Normal N
h1 : Nat.coprime (Fintype.card { x // x ∈ N }) (index N)
h2 :
  ∀ (G' : Type u) [inst : Group G'] [inst_1 : Fintype G'],
    Fintype.card G' < Fintype.card G →
      ∀ {N' : Subgroup G'} [inst_2 : Normal N'],
        Nat.coprime (Fintype.card { x // x ∈ N' }) (index N') → ∃ H', IsComplement' N' H'
h3 : ∀ (H : Subgroup G), ¬IsComplement' N H
K : Subgroup G
inst✝ : Normal K
hK : K ≤ N
this : Function.Surjective ↑(QuotientGroup.mk' K)
h4 : K ≠ ⊥ ∧ K ≠ N
h5 : Fintype.card (G ⧸ K) < Fintype.card G
index_map : index (map (QuotientGroup.mk' K) N) = index N
index_pos : 0 < index N
⊢ Fintype.card (G ⧸ K) ∣ Fintype.card G
[PROOFSTEP]
exact K.card_quotient_dvd_card
[GOAL]
G : Type u
inst✝³ : Group G
inst✝² : Fintype G
N : Subgroup G
inst✝¹ : Normal N
h1 : Nat.coprime (Fintype.card { x // x ∈ N }) (index N)
h2 :
  ∀ (G' : Type u) [inst : Group G'] [inst_1 : Fintype G'],
    Fintype.card G' < Fintype.card G →
      ∀ {N' : Subgroup G'} [inst_2 : Normal N'],
        Nat.coprime (Fintype.card { x // x ∈ N' }) (index N') → ∃ H', IsComplement' N' H'
h3 : ∀ (H : Subgroup G), ¬IsComplement' N H
K : Subgroup G
inst✝ : Normal K
hK : K ≤ N
this : Function.Surjective ↑(QuotientGroup.mk' K)
h4 : K ≠ ⊥ ∧ K ≠ N
h5 : Fintype.card (G ⧸ K) < Fintype.card G
h6 : Nat.coprime (Fintype.card { x // x ∈ map (QuotientGroup.mk' K) N }) (index (map (QuotientGroup.mk' K) N))
⊢ ∃ K, K ⊔ N = ⊤ ∧ K ≠ ⊤
[PROOFSTEP]
obtain ⟨H, hH⟩ := h2 (G ⧸ K) h5 h6
[GOAL]
case intro
G : Type u
inst✝³ : Group G
inst✝² : Fintype G
N : Subgroup G
inst✝¹ : Normal N
h1 : Nat.coprime (Fintype.card { x // x ∈ N }) (index N)
h2 :
  ∀ (G' : Type u) [inst : Group G'] [inst_1 : Fintype G'],
    Fintype.card G' < Fintype.card G →
      ∀ {N' : Subgroup G'} [inst_2 : Normal N'],
        Nat.coprime (Fintype.card { x // x ∈ N' }) (index N') → ∃ H', IsComplement' N' H'
h3 : ∀ (H : Subgroup G), ¬IsComplement' N H
K : Subgroup G
inst✝ : Normal K
hK : K ≤ N
this : Function.Surjective ↑(QuotientGroup.mk' K)
h4 : K ≠ ⊥ ∧ K ≠ N
h5 : Fintype.card (G ⧸ K) < Fintype.card G
h6 : Nat.coprime (Fintype.card { x // x ∈ map (QuotientGroup.mk' K) N }) (index (map (QuotientGroup.mk' K) N))
H : Subgroup (G ⧸ K)
hH : IsComplement' (map (QuotientGroup.mk' K) N) H
⊢ ∃ K, K ⊔ N = ⊤ ∧ K ≠ ⊤
[PROOFSTEP]
refine' ⟨H.comap (QuotientGroup.mk' K), _, _⟩
[GOAL]
case intro.refine'_1
G : Type u
inst✝³ : Group G
inst✝² : Fintype G
N : Subgroup G
inst✝¹ : Normal N
h1 : Nat.coprime (Fintype.card { x // x ∈ N }) (index N)
h2 :
  ∀ (G' : Type u) [inst : Group G'] [inst_1 : Fintype G'],
    Fintype.card G' < Fintype.card G →
      ∀ {N' : Subgroup G'} [inst_2 : Normal N'],
        Nat.coprime (Fintype.card { x // x ∈ N' }) (index N') → ∃ H', IsComplement' N' H'
h3 : ∀ (H : Subgroup G), ¬IsComplement' N H
K : Subgroup G
inst✝ : Normal K
hK : K ≤ N
this : Function.Surjective ↑(QuotientGroup.mk' K)
h4 : K ≠ ⊥ ∧ K ≠ N
h5 : Fintype.card (G ⧸ K) < Fintype.card G
h6 : Nat.coprime (Fintype.card { x // x ∈ map (QuotientGroup.mk' K) N }) (index (map (QuotientGroup.mk' K) N))
H : Subgroup (G ⧸ K)
hH : IsComplement' (map (QuotientGroup.mk' K) N) H
⊢ comap (QuotientGroup.mk' K) H ⊔ N = ⊤
[PROOFSTEP]
have key : (N.map (QuotientGroup.mk' K)).comap (QuotientGroup.mk' K) = N :=
  by
  refine' comap_map_eq_self _
  rwa [QuotientGroup.ker_mk']
[GOAL]
G : Type u
inst✝³ : Group G
inst✝² : Fintype G
N : Subgroup G
inst✝¹ : Normal N
h1 : Nat.coprime (Fintype.card { x // x ∈ N }) (index N)
h2 :
  ∀ (G' : Type u) [inst : Group G'] [inst_1 : Fintype G'],
    Fintype.card G' < Fintype.card G →
      ∀ {N' : Subgroup G'} [inst_2 : Normal N'],
        Nat.coprime (Fintype.card { x // x ∈ N' }) (index N') → ∃ H', IsComplement' N' H'
h3 : ∀ (H : Subgroup G), ¬IsComplement' N H
K : Subgroup G
inst✝ : Normal K
hK : K ≤ N
this : Function.Surjective ↑(QuotientGroup.mk' K)
h4 : K ≠ ⊥ ∧ K ≠ N
h5 : Fintype.card (G ⧸ K) < Fintype.card G
h6 : Nat.coprime (Fintype.card { x // x ∈ map (QuotientGroup.mk' K) N }) (index (map (QuotientGroup.mk' K) N))
H : Subgroup (G ⧸ K)
hH : IsComplement' (map (QuotientGroup.mk' K) N) H
⊢ comap (QuotientGroup.mk' K) (map (QuotientGroup.mk' K) N) = N
[PROOFSTEP]
refine' comap_map_eq_self _
[GOAL]
G : Type u
inst✝³ : Group G
inst✝² : Fintype G
N : Subgroup G
inst✝¹ : Normal N
h1 : Nat.coprime (Fintype.card { x // x ∈ N }) (index N)
h2 :
  ∀ (G' : Type u) [inst : Group G'] [inst_1 : Fintype G'],
    Fintype.card G' < Fintype.card G →
      ∀ {N' : Subgroup G'} [inst_2 : Normal N'],
        Nat.coprime (Fintype.card { x // x ∈ N' }) (index N') → ∃ H', IsComplement' N' H'
h3 : ∀ (H : Subgroup G), ¬IsComplement' N H
K : Subgroup G
inst✝ : Normal K
hK : K ≤ N
this : Function.Surjective ↑(QuotientGroup.mk' K)
h4 : K ≠ ⊥ ∧ K ≠ N
h5 : Fintype.card (G ⧸ K) < Fintype.card G
h6 : Nat.coprime (Fintype.card { x // x ∈ map (QuotientGroup.mk' K) N }) (index (map (QuotientGroup.mk' K) N))
H : Subgroup (G ⧸ K)
hH : IsComplement' (map (QuotientGroup.mk' K) N) H
⊢ MonoidHom.ker (QuotientGroup.mk' K) ≤ N
[PROOFSTEP]
rwa [QuotientGroup.ker_mk']
[GOAL]
case intro.refine'_1
G : Type u
inst✝³ : Group G
inst✝² : Fintype G
N : Subgroup G
inst✝¹ : Normal N
h1 : Nat.coprime (Fintype.card { x // x ∈ N }) (index N)
h2 :
  ∀ (G' : Type u) [inst : Group G'] [inst_1 : Fintype G'],
    Fintype.card G' < Fintype.card G →
      ∀ {N' : Subgroup G'} [inst_2 : Normal N'],
        Nat.coprime (Fintype.card { x // x ∈ N' }) (index N') → ∃ H', IsComplement' N' H'
h3 : ∀ (H : Subgroup G), ¬IsComplement' N H
K : Subgroup G
inst✝ : Normal K
hK : K ≤ N
this : Function.Surjective ↑(QuotientGroup.mk' K)
h4 : K ≠ ⊥ ∧ K ≠ N
h5 : Fintype.card (G ⧸ K) < Fintype.card G
h6 : Nat.coprime (Fintype.card { x // x ∈ map (QuotientGroup.mk' K) N }) (index (map (QuotientGroup.mk' K) N))
H : Subgroup (G ⧸ K)
hH : IsComplement' (map (QuotientGroup.mk' K) N) H
key : comap (QuotientGroup.mk' K) (map (QuotientGroup.mk' K) N) = N
⊢ comap (QuotientGroup.mk' K) H ⊔ N = ⊤
[PROOFSTEP]
rwa [← key, comap_sup_eq, hH.symm.sup_eq_top, comap_top]
[GOAL]
case intro.refine'_2
G : Type u
inst✝³ : Group G
inst✝² : Fintype G
N : Subgroup G
inst✝¹ : Normal N
h1 : Nat.coprime (Fintype.card { x // x ∈ N }) (index N)
h2 :
  ∀ (G' : Type u) [inst : Group G'] [inst_1 : Fintype G'],
    Fintype.card G' < Fintype.card G →
      ∀ {N' : Subgroup G'} [inst_2 : Normal N'],
        Nat.coprime (Fintype.card { x // x ∈ N' }) (index N') → ∃ H', IsComplement' N' H'
h3 : ∀ (H : Subgroup G), ¬IsComplement' N H
K : Subgroup G
inst✝ : Normal K
hK : K ≤ N
this : Function.Surjective ↑(QuotientGroup.mk' K)
h4 : K ≠ ⊥ ∧ K ≠ N
h5 : Fintype.card (G ⧸ K) < Fintype.card G
h6 : Nat.coprime (Fintype.card { x // x ∈ map (QuotientGroup.mk' K) N }) (index (map (QuotientGroup.mk' K) N))
H : Subgroup (G ⧸ K)
hH : IsComplement' (map (QuotientGroup.mk' K) N) H
⊢ comap (QuotientGroup.mk' K) H ≠ ⊤
[PROOFSTEP]
rw [← comap_top (QuotientGroup.mk' K)]
[GOAL]
case intro.refine'_2
G : Type u
inst✝³ : Group G
inst✝² : Fintype G
N : Subgroup G
inst✝¹ : Normal N
h1 : Nat.coprime (Fintype.card { x // x ∈ N }) (index N)
h2 :
  ∀ (G' : Type u) [inst : Group G'] [inst_1 : Fintype G'],
    Fintype.card G' < Fintype.card G →
      ∀ {N' : Subgroup G'} [inst_2 : Normal N'],
        Nat.coprime (Fintype.card { x // x ∈ N' }) (index N') → ∃ H', IsComplement' N' H'
h3 : ∀ (H : Subgroup G), ¬IsComplement' N H
K : Subgroup G
inst✝ : Normal K
hK : K ≤ N
this : Function.Surjective ↑(QuotientGroup.mk' K)
h4 : K ≠ ⊥ ∧ K ≠ N
h5 : Fintype.card (G ⧸ K) < Fintype.card G
h6 : Nat.coprime (Fintype.card { x // x ∈ map (QuotientGroup.mk' K) N }) (index (map (QuotientGroup.mk' K) N))
H : Subgroup (G ⧸ K)
hH : IsComplement' (map (QuotientGroup.mk' K) N) H
⊢ comap (QuotientGroup.mk' K) H ≠ comap (QuotientGroup.mk' K) ⊤
[PROOFSTEP]
intro hH'
[GOAL]
case intro.refine'_2
G : Type u
inst✝³ : Group G
inst✝² : Fintype G
N : Subgroup G
inst✝¹ : Normal N
h1 : Nat.coprime (Fintype.card { x // x ∈ N }) (index N)
h2 :
  ∀ (G' : Type u) [inst : Group G'] [inst_1 : Fintype G'],
    Fintype.card G' < Fintype.card G →
      ∀ {N' : Subgroup G'} [inst_2 : Normal N'],
        Nat.coprime (Fintype.card { x // x ∈ N' }) (index N') → ∃ H', IsComplement' N' H'
h3 : ∀ (H : Subgroup G), ¬IsComplement' N H
K : Subgroup G
inst✝ : Normal K
hK : K ≤ N
this : Function.Surjective ↑(QuotientGroup.mk' K)
h4 : K ≠ ⊥ ∧ K ≠ N
h5 : Fintype.card (G ⧸ K) < Fintype.card G
h6 : Nat.coprime (Fintype.card { x // x ∈ map (QuotientGroup.mk' K) N }) (index (map (QuotientGroup.mk' K) N))
H : Subgroup (G ⧸ K)
hH : IsComplement' (map (QuotientGroup.mk' K) N) H
hH' : comap (QuotientGroup.mk' K) H = comap (QuotientGroup.mk' K) ⊤
⊢ False
[PROOFSTEP]
rw [comap_injective this hH', isComplement'_top_right, map_eq_bot_iff, QuotientGroup.ker_mk'] at hH
[GOAL]
case intro.refine'_2
G : Type u
inst✝³ : Group G
inst✝² : Fintype G
N : Subgroup G
inst✝¹ : Normal N
h1 : Nat.coprime (Fintype.card { x // x ∈ N }) (index N)
h2 :
  ∀ (G' : Type u) [inst : Group G'] [inst_1 : Fintype G'],
    Fintype.card G' < Fintype.card G →
      ∀ {N' : Subgroup G'} [inst_2 : Normal N'],
        Nat.coprime (Fintype.card { x // x ∈ N' }) (index N') → ∃ H', IsComplement' N' H'
h3 : ∀ (H : Subgroup G), ¬IsComplement' N H
K : Subgroup G
inst✝ : Normal K
hK : K ≤ N
this : Function.Surjective ↑(QuotientGroup.mk' K)
h4 : K ≠ ⊥ ∧ K ≠ N
h5 : Fintype.card (G ⧸ K) < Fintype.card G
h6 : Nat.coprime (Fintype.card { x // x ∈ map (QuotientGroup.mk' K) N }) (index (map (QuotientGroup.mk' K) N))
H : Subgroup (G ⧸ K)
hH : N ≤ K
hH' : comap (QuotientGroup.mk' K) H = comap (QuotientGroup.mk' K) ⊤
⊢ False
[PROOFSTEP]
exact h4.2 (le_antisymm hK hH)
[GOAL]
G : Type u
inst✝³ : Group G
inst✝² : Fintype G
N : Subgroup G
inst✝¹ : Normal N
h1 : Nat.coprime (Fintype.card { x // x ∈ N }) (index N)
h2 :
  ∀ (G' : Type u) [inst : Group G'] [inst_1 : Fintype G'],
    Fintype.card G' < Fintype.card G →
      ∀ {N' : Subgroup G'} [inst_2 : Normal N'],
        Nat.coprime (Fintype.card { x // x ∈ N' }) (index N') → ∃ H', IsComplement' N' H'
h3 : ∀ (H : Subgroup G), ¬IsComplement' N H
K : Subgroup { x // x ∈ N }
inst✝ : Normal (map (Subgroup.subtype N) K)
⊢ K = ⊥ ∨ K = ⊤
[PROOFSTEP]
have key := step2 h1 h2 h3 (K.map N.subtype) (map_subtype_le K)
[GOAL]
G : Type u
inst✝³ : Group G
inst✝² : Fintype G
N : Subgroup G
inst✝¹ : Normal N
h1 : Nat.coprime (Fintype.card { x // x ∈ N }) (index N)
h2 :
  ∀ (G' : Type u) [inst : Group G'] [inst_1 : Fintype G'],
    Fintype.card G' < Fintype.card G →
      ∀ {N' : Subgroup G'} [inst_2 : Normal N'],
        Nat.coprime (Fintype.card { x // x ∈ N' }) (index N') → ∃ H', IsComplement' N' H'
h3 : ∀ (H : Subgroup G), ¬IsComplement' N H
K : Subgroup { x // x ∈ N }
inst✝ : Normal (map (Subgroup.subtype N) K)
key : map (Subgroup.subtype N) K = ⊥ ∨ map (Subgroup.subtype N) K = N
⊢ K = ⊥ ∨ K = ⊤
[PROOFSTEP]
rw [← map_bot N.subtype] at key
[GOAL]
G : Type u
inst✝³ : Group G
inst✝² : Fintype G
N : Subgroup G
inst✝¹ : Normal N
h1 : Nat.coprime (Fintype.card { x // x ∈ N }) (index N)
h2 :
  ∀ (G' : Type u) [inst : Group G'] [inst_1 : Fintype G'],
    Fintype.card G' < Fintype.card G →
      ∀ {N' : Subgroup G'} [inst_2 : Normal N'],
        Nat.coprime (Fintype.card { x // x ∈ N' }) (index N') → ∃ H', IsComplement' N' H'
h3 : ∀ (H : Subgroup G), ¬IsComplement' N H
K : Subgroup { x // x ∈ N }
inst✝ : Normal (map (Subgroup.subtype N) K)
key : map (Subgroup.subtype N) K = map (Subgroup.subtype N) ⊥ ∨ map (Subgroup.subtype N) K = N
⊢ K = ⊥ ∨ K = ⊤
[PROOFSTEP]
conv at key =>
  rhs
  rhs
  rw [← N.subtype_range, N.subtype.range_eq_map]
[GOAL]
G : Type u
inst✝³ : Group G
inst✝² : Fintype G
N : Subgroup G
inst✝¹ : Normal N
h1 : Nat.coprime (Fintype.card { x // x ∈ N }) (index N)
h2 :
  ∀ (G' : Type u) [inst : Group G'] [inst_1 : Fintype G'],
    Fintype.card G' < Fintype.card G →
      ∀ {N' : Subgroup G'} [inst_2 : Normal N'],
        Nat.coprime (Fintype.card { x // x ∈ N' }) (index N') → ∃ H', IsComplement' N' H'
h3 : ∀ (H : Subgroup G), ¬IsComplement' N H
K : Subgroup { x // x ∈ N }
inst✝ : Normal (map (Subgroup.subtype N) K)
key : map (Subgroup.subtype N) K = map (Subgroup.subtype N) ⊥ ∨ map (Subgroup.subtype N) K = N
| map (Subgroup.subtype N) K = map (Subgroup.subtype N) ⊥ ∨ map (Subgroup.subtype N) K = N
[PROOFSTEP]
  rhs
  rhs
  rw [← N.subtype_range, N.subtype.range_eq_map]
[GOAL]
G : Type u
inst✝³ : Group G
inst✝² : Fintype G
N : Subgroup G
inst✝¹ : Normal N
h1 : Nat.coprime (Fintype.card { x // x ∈ N }) (index N)
h2 :
  ∀ (G' : Type u) [inst : Group G'] [inst_1 : Fintype G'],
    Fintype.card G' < Fintype.card G →
      ∀ {N' : Subgroup G'} [inst_2 : Normal N'],
        Nat.coprime (Fintype.card { x // x ∈ N' }) (index N') → ∃ H', IsComplement' N' H'
h3 : ∀ (H : Subgroup G), ¬IsComplement' N H
K : Subgroup { x // x ∈ N }
inst✝ : Normal (map (Subgroup.subtype N) K)
key : map (Subgroup.subtype N) K = map (Subgroup.subtype N) ⊥ ∨ map (Subgroup.subtype N) K = N
| map (Subgroup.subtype N) K = map (Subgroup.subtype N) ⊥ ∨ map (Subgroup.subtype N) K = N
[PROOFSTEP]
  rhs
  rhs
  rw [← N.subtype_range, N.subtype.range_eq_map]
[GOAL]
G : Type u
inst✝³ : Group G
inst✝² : Fintype G
N : Subgroup G
inst✝¹ : Normal N
h1 : Nat.coprime (Fintype.card { x // x ∈ N }) (index N)
h2 :
  ∀ (G' : Type u) [inst : Group G'] [inst_1 : Fintype G'],
    Fintype.card G' < Fintype.card G →
      ∀ {N' : Subgroup G'} [inst_2 : Normal N'],
        Nat.coprime (Fintype.card { x // x ∈ N' }) (index N') → ∃ H', IsComplement' N' H'
h3 : ∀ (H : Subgroup G), ¬IsComplement' N H
K : Subgroup { x // x ∈ N }
inst✝ : Normal (map (Subgroup.subtype N) K)
key : map (Subgroup.subtype N) K = map (Subgroup.subtype N) ⊥ ∨ map (Subgroup.subtype N) K = N
| map (Subgroup.subtype N) K = map (Subgroup.subtype N) ⊥ ∨ map (Subgroup.subtype N) K = N
[PROOFSTEP]
rhs
[GOAL]
G : Type u
inst✝³ : Group G
inst✝² : Fintype G
N : Subgroup G
inst✝¹ : Normal N
h1 : Nat.coprime (Fintype.card { x // x ∈ N }) (index N)
h2 :
  ∀ (G' : Type u) [inst : Group G'] [inst_1 : Fintype G'],
    Fintype.card G' < Fintype.card G →
      ∀ {N' : Subgroup G'} [inst_2 : Normal N'],
        Nat.coprime (Fintype.card { x // x ∈ N' }) (index N') → ∃ H', IsComplement' N' H'
h3 : ∀ (H : Subgroup G), ¬IsComplement' N H
K : Subgroup { x // x ∈ N }
inst✝ : Normal (map (Subgroup.subtype N) K)
key : map (Subgroup.subtype N) K = map (Subgroup.subtype N) ⊥ ∨ map (Subgroup.subtype N) K = N
| map (Subgroup.subtype N) K = N
[PROOFSTEP]
rhs
[GOAL]
G : Type u
inst✝³ : Group G
inst✝² : Fintype G
N : Subgroup G
inst✝¹ : Normal N
h1 : Nat.coprime (Fintype.card { x // x ∈ N }) (index N)
h2 :
  ∀ (G' : Type u) [inst : Group G'] [inst_1 : Fintype G'],
    Fintype.card G' < Fintype.card G →
      ∀ {N' : Subgroup G'} [inst_2 : Normal N'],
        Nat.coprime (Fintype.card { x // x ∈ N' }) (index N') → ∃ H', IsComplement' N' H'
h3 : ∀ (H : Subgroup G), ¬IsComplement' N H
K : Subgroup { x // x ∈ N }
inst✝ : Normal (map (Subgroup.subtype N) K)
key : map (Subgroup.subtype N) K = map (Subgroup.subtype N) ⊥ ∨ map (Subgroup.subtype N) K = N
| N
[PROOFSTEP]
rw [← N.subtype_range, N.subtype.range_eq_map]
[GOAL]
G : Type u
inst✝³ : Group G
inst✝² : Fintype G
N : Subgroup G
inst✝¹ : Normal N
h1 : Nat.coprime (Fintype.card { x // x ∈ N }) (index N)
h2 :
  ∀ (G' : Type u) [inst : Group G'] [inst_1 : Fintype G'],
    Fintype.card G' < Fintype.card G →
      ∀ {N' : Subgroup G'} [inst_2 : Normal N'],
        Nat.coprime (Fintype.card { x // x ∈ N' }) (index N') → ∃ H', IsComplement' N' H'
h3 : ∀ (H : Subgroup G), ¬IsComplement' N H
K : Subgroup { x // x ∈ N }
inst✝ : Normal (map (Subgroup.subtype N) K)
key : map (Subgroup.subtype N) K = map (Subgroup.subtype N) ⊥ ∨ map (Subgroup.subtype N) K = map (Subgroup.subtype N) ⊤
⊢ K = ⊥ ∨ K = ⊤
[PROOFSTEP]
have inj := map_injective N.subtype_injective
[GOAL]
G : Type u
inst✝³ : Group G
inst✝² : Fintype G
N : Subgroup G
inst✝¹ : Normal N
h1 : Nat.coprime (Fintype.card { x // x ∈ N }) (index N)
h2 :
  ∀ (G' : Type u) [inst : Group G'] [inst_1 : Fintype G'],
    Fintype.card G' < Fintype.card G →
      ∀ {N' : Subgroup G'} [inst_2 : Normal N'],
        Nat.coprime (Fintype.card { x // x ∈ N' }) (index N') → ∃ H', IsComplement' N' H'
h3 : ∀ (H : Subgroup G), ¬IsComplement' N H
K : Subgroup { x // x ∈ N }
inst✝ : Normal (map (Subgroup.subtype N) K)
key : map (Subgroup.subtype N) K = map (Subgroup.subtype N) ⊥ ∨ map (Subgroup.subtype N) K = map (Subgroup.subtype N) ⊤
inj : Function.Injective (map (Subgroup.subtype N))
⊢ K = ⊥ ∨ K = ⊤
[PROOFSTEP]
rwa [inj.eq_iff, inj.eq_iff] at key
[GOAL]
G : Type u
inst✝² : Group G
inst✝¹ : Fintype G
N : Subgroup G
inst✝ : Normal N
h1 : Nat.coprime (Fintype.card { x // x ∈ N }) (index N)
h2 :
  ∀ (G' : Type u) [inst : Group G'] [inst_1 : Fintype G'],
    Fintype.card G' < Fintype.card G →
      ∀ {N' : Subgroup G'} [inst_2 : Normal N'],
        Nat.coprime (Fintype.card { x // x ∈ N' }) (index N') → ∃ H', IsComplement' N' H'
h3 : ∀ (H : Subgroup G), ¬IsComplement' N H
⊢ IsPGroup (Nat.minFac (Fintype.card { x // x ∈ N })) { x // x ∈ N }
[PROOFSTEP]
haveI : Fact (Fintype.card N).minFac.Prime := ⟨step4 h1 h3⟩
[GOAL]
G : Type u
inst✝² : Group G
inst✝¹ : Fintype G
N : Subgroup G
inst✝ : Normal N
h1 : Nat.coprime (Fintype.card { x // x ∈ N }) (index N)
h2 :
  ∀ (G' : Type u) [inst : Group G'] [inst_1 : Fintype G'],
    Fintype.card G' < Fintype.card G →
      ∀ {N' : Subgroup G'} [inst_2 : Normal N'],
        Nat.coprime (Fintype.card { x // x ∈ N' }) (index N') → ∃ H', IsComplement' N' H'
h3 : ∀ (H : Subgroup G), ¬IsComplement' N H
this : Fact (Nat.Prime (Nat.minFac (Fintype.card { x // x ∈ N })))
⊢ IsPGroup (Nat.minFac (Fintype.card { x // x ∈ N })) { x // x ∈ N }
[PROOFSTEP]
refine' Sylow.nonempty.elim fun P => P.2.of_surjective P.1.subtype _
[GOAL]
G : Type u
inst✝² : Group G
inst✝¹ : Fintype G
N : Subgroup G
inst✝ : Normal N
h1 : Nat.coprime (Fintype.card { x // x ∈ N }) (index N)
h2 :
  ∀ (G' : Type u) [inst : Group G'] [inst_1 : Fintype G'],
    Fintype.card G' < Fintype.card G →
      ∀ {N' : Subgroup G'} [inst_2 : Normal N'],
        Nat.coprime (Fintype.card { x // x ∈ N' }) (index N') → ∃ H', IsComplement' N' H'
h3 : ∀ (H : Subgroup G), ¬IsComplement' N H
this : Fact (Nat.Prime (Nat.minFac (Fintype.card { x // x ∈ N })))
P : Sylow (Nat.minFac (Fintype.card { x // x ∈ N })) { x // x ∈ N }
⊢ Function.Surjective ↑(Subgroup.subtype ↑P)
[PROOFSTEP]
rw [← MonoidHom.range_top_iff_surjective, subtype_range]
[GOAL]
G : Type u
inst✝² : Group G
inst✝¹ : Fintype G
N : Subgroup G
inst✝ : Normal N
h1 : Nat.coprime (Fintype.card { x // x ∈ N }) (index N)
h2 :
  ∀ (G' : Type u) [inst : Group G'] [inst_1 : Fintype G'],
    Fintype.card G' < Fintype.card G →
      ∀ {N' : Subgroup G'} [inst_2 : Normal N'],
        Nat.coprime (Fintype.card { x // x ∈ N' }) (index N') → ∃ H', IsComplement' N' H'
h3 : ∀ (H : Subgroup G), ¬IsComplement' N H
this : Fact (Nat.Prime (Nat.minFac (Fintype.card { x // x ∈ N })))
P : Sylow (Nat.minFac (Fintype.card { x // x ∈ N })) { x // x ∈ N }
⊢ ↑P = ⊤
[PROOFSTEP]
haveI : (P.1.map N.subtype).Normal :=
  normalizer_eq_top.mp (step1 h1 h2 h3 (P.1.map N.subtype).normalizer P.normalizer_sup_eq_top)
[GOAL]
G : Type u
inst✝² : Group G
inst✝¹ : Fintype G
N : Subgroup G
inst✝ : Normal N
h1 : Nat.coprime (Fintype.card { x // x ∈ N }) (index N)
h2 :
  ∀ (G' : Type u) [inst : Group G'] [inst_1 : Fintype G'],
    Fintype.card G' < Fintype.card G →
      ∀ {N' : Subgroup G'} [inst_2 : Normal N'],
        Nat.coprime (Fintype.card { x // x ∈ N' }) (index N') → ∃ H', IsComplement' N' H'
h3 : ∀ (H : Subgroup G), ¬IsComplement' N H
this✝ : Fact (Nat.Prime (Nat.minFac (Fintype.card { x // x ∈ N })))
P : Sylow (Nat.minFac (Fintype.card { x // x ∈ N })) { x // x ∈ N }
this : Normal (map (Subgroup.subtype N) ↑P)
⊢ ↑P = ⊤
[PROOFSTEP]
exact (step3 h1 h2 h3 P.1).resolve_left (step5 h1 h3)
[GOAL]
G : Type u
inst✝² : Group G
inst✝¹ : Fintype G
N : Subgroup G
inst✝ : Normal N
h1 : Nat.coprime (Fintype.card { x // x ∈ N }) (index N)
h2 :
  ∀ (G' : Type u) [inst : Group G'] [inst_1 : Fintype G'],
    Fintype.card G' < Fintype.card G →
      ∀ {N' : Subgroup G'} [inst_2 : Normal N'],
        Nat.coprime (Fintype.card { x // x ∈ N' }) (index N') → ∃ H', IsComplement' N' H'
h3 : ∀ (H : Subgroup G), ¬IsComplement' N H
⊢ IsCommutative N
[PROOFSTEP]
haveI := N.bot_or_nontrivial.resolve_left (step0 h1 h3)
[GOAL]
G : Type u
inst✝² : Group G
inst✝¹ : Fintype G
N : Subgroup G
inst✝ : Normal N
h1 : Nat.coprime (Fintype.card { x // x ∈ N }) (index N)
h2 :
  ∀ (G' : Type u) [inst : Group G'] [inst_1 : Fintype G'],
    Fintype.card G' < Fintype.card G →
      ∀ {N' : Subgroup G'} [inst_2 : Normal N'],
        Nat.coprime (Fintype.card { x // x ∈ N' }) (index N') → ∃ H', IsComplement' N' H'
h3 : ∀ (H : Subgroup G), ¬IsComplement' N H
this : Nontrivial { x // x ∈ N }
⊢ IsCommutative N
[PROOFSTEP]
haveI : Fact (Fintype.card N).minFac.Prime := ⟨step4 h1 h3⟩
[GOAL]
G : Type u
inst✝² : Group G
inst✝¹ : Fintype G
N : Subgroup G
inst✝ : Normal N
h1 : Nat.coprime (Fintype.card { x // x ∈ N }) (index N)
h2 :
  ∀ (G' : Type u) [inst : Group G'] [inst_1 : Fintype G'],
    Fintype.card G' < Fintype.card G →
      ∀ {N' : Subgroup G'} [inst_2 : Normal N'],
        Nat.coprime (Fintype.card { x // x ∈ N' }) (index N') → ∃ H', IsComplement' N' H'
h3 : ∀ (H : Subgroup G), ¬IsComplement' N H
this✝ : Nontrivial { x // x ∈ N }
this : Fact (Nat.Prime (Nat.minFac (Fintype.card { x // x ∈ N })))
⊢ IsCommutative N
[PROOFSTEP]
exact
  ⟨⟨fun g h =>
      eq_top_iff.mp ((step3 h1 h2 h3 (center N)).resolve_left (step6 h1 h2 h3).bot_lt_center.ne') (mem_top h) g⟩⟩
[GOAL]
n : ℕ
G : Type u
inst✝² : Group G
inst✝¹ : Fintype G
hG : Fintype.card G = n
N : Subgroup G
inst✝ : Normal N
hN : Nat.coprime (Fintype.card { x // x ∈ N }) (index N)
⊢ ∃ H, IsComplement' N H
[PROOFSTEP]
revert G
[GOAL]
n : ℕ
⊢ ∀ {G : Type u} [inst : Group G] [inst_1 : Fintype G],
    Fintype.card G = n →
      ∀ {N : Subgroup G} [inst_2 : Normal N],
        Nat.coprime (Fintype.card { x // x ∈ N }) (index N) → ∃ H, IsComplement' N H
[PROOFSTEP]
apply Nat.strongInductionOn n
[GOAL]
n : ℕ
⊢ ∀ (n : ℕ),
    (∀ (m : ℕ),
        m < n →
          ∀ {G : Type u} [inst : Group G] [inst_1 : Fintype G],
            Fintype.card G = m →
              ∀ {N : Subgroup G} [inst_2 : Normal N],
                Nat.coprime (Fintype.card { x // x ∈ N }) (index N) → ∃ H, IsComplement' N H) →
      ∀ {G : Type u} [inst : Group G] [inst_1 : Fintype G],
        Fintype.card G = n →
          ∀ {N : Subgroup G} [inst_2 : Normal N],
            Nat.coprime (Fintype.card { x // x ∈ N }) (index N) → ∃ H, IsComplement' N H
[PROOFSTEP]
rintro n ih G _ _ rfl N _ hN
[GOAL]
n : ℕ
G : Type u
inst✝² : Group G
inst✝¹ : Fintype G
ih :
  ∀ (m : ℕ),
    m < Fintype.card G →
      ∀ {G : Type u} [inst : Group G] [inst_1 : Fintype G],
        Fintype.card G = m →
          ∀ {N : Subgroup G} [inst_2 : Normal N],
            Nat.coprime (Fintype.card { x // x ∈ N }) (index N) → ∃ H, IsComplement' N H
N : Subgroup G
inst✝ : Normal N
hN : Nat.coprime (Fintype.card { x // x ∈ N }) (index N)
⊢ ∃ H, IsComplement' N H
[PROOFSTEP]
refine' not_forall_not.mp fun h3 => _
[GOAL]
n : ℕ
G : Type u
inst✝² : Group G
inst✝¹ : Fintype G
ih :
  ∀ (m : ℕ),
    m < Fintype.card G →
      ∀ {G : Type u} [inst : Group G] [inst_1 : Fintype G],
        Fintype.card G = m →
          ∀ {N : Subgroup G} [inst_2 : Normal N],
            Nat.coprime (Fintype.card { x // x ∈ N }) (index N) → ∃ H, IsComplement' N H
N : Subgroup G
inst✝ : Normal N
hN : Nat.coprime (Fintype.card { x // x ∈ N }) (index N)
h3 : ∀ (x : Subgroup G), ¬IsComplement' N x
⊢ False
[PROOFSTEP]
haveI := SchurZassenhausInduction.step7 hN (fun G' _ _ hG' => by apply ih _ hG'; rfl) h3
[GOAL]
n : ℕ
G : Type u
inst✝² : Group G
inst✝¹ : Fintype G
ih :
  ∀ (m : ℕ),
    m < Fintype.card G →
      ∀ {G : Type u} [inst : Group G] [inst_1 : Fintype G],
        Fintype.card G = m →
          ∀ {N : Subgroup G} [inst_2 : Normal N],
            Nat.coprime (Fintype.card { x // x ∈ N }) (index N) → ∃ H, IsComplement' N H
N : Subgroup G
inst✝ : Normal N
hN : Nat.coprime (Fintype.card { x // x ∈ N }) (index N)
h3 : ∀ (x : Subgroup G), ¬IsComplement' N x
G' : Type u
x✝¹ : Group G'
x✝ : Fintype G'
hG' : Fintype.card G' < Fintype.card G
⊢ ∀ {N' : Subgroup G'} [inst : Normal N'],
    Nat.coprime (Fintype.card { x // x ∈ N' }) (index N') → ∃ H', IsComplement' N' H'
[PROOFSTEP]
apply ih _ hG'
[GOAL]
n : ℕ
G : Type u
inst✝² : Group G
inst✝¹ : Fintype G
ih :
  ∀ (m : ℕ),
    m < Fintype.card G →
      ∀ {G : Type u} [inst : Group G] [inst_1 : Fintype G],
        Fintype.card G = m →
          ∀ {N : Subgroup G} [inst_2 : Normal N],
            Nat.coprime (Fintype.card { x // x ∈ N }) (index N) → ∃ H, IsComplement' N H
N : Subgroup G
inst✝ : Normal N
hN : Nat.coprime (Fintype.card { x // x ∈ N }) (index N)
h3 : ∀ (x : Subgroup G), ¬IsComplement' N x
G' : Type u
x✝¹ : Group G'
x✝ : Fintype G'
hG' : Fintype.card G' < Fintype.card G
⊢ Fintype.card G' = Fintype.card G'
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
G : Type u
inst✝² : Group G
inst✝¹ : Fintype G
ih :
  ∀ (m : ℕ),
    m < Fintype.card G →
      ∀ {G : Type u} [inst : Group G] [inst_1 : Fintype G],
        Fintype.card G = m →
          ∀ {N : Subgroup G} [inst_2 : Normal N],
            Nat.coprime (Fintype.card { x // x ∈ N }) (index N) → ∃ H, IsComplement' N H
N : Subgroup G
inst✝ : Normal N
hN : Nat.coprime (Fintype.card { x // x ∈ N }) (index N)
h3 : ∀ (x : Subgroup G), ¬IsComplement' N x
this : IsCommutative N
⊢ False
[PROOFSTEP]
rw [← Nat.card_eq_fintype_card] at hN
[GOAL]
n : ℕ
G : Type u
inst✝² : Group G
inst✝¹ : Fintype G
ih :
  ∀ (m : ℕ),
    m < Fintype.card G →
      ∀ {G : Type u} [inst : Group G] [inst_1 : Fintype G],
        Fintype.card G = m →
          ∀ {N : Subgroup G} [inst_2 : Normal N],
            Nat.coprime (Fintype.card { x // x ∈ N }) (index N) → ∃ H, IsComplement' N H
N : Subgroup G
inst✝ : Normal N
hN : Nat.coprime (Nat.card { x // x ∈ N }) (index N)
h3 : ∀ (x : Subgroup G), ¬IsComplement' N x
this : IsCommutative N
⊢ False
[PROOFSTEP]
exact not_exists_of_forall_not h3 (exists_right_complement'_of_coprime_aux hN)
[GOAL]
n : ℕ
G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : Normal N
hN : Nat.coprime (Nat.card { x // x ∈ N }) (index N)
⊢ ∃ H, IsComplement' N H
[PROOFSTEP]
by_cases hN1 : Nat.card N = 0
[GOAL]
case pos
n : ℕ
G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : Normal N
hN : Nat.coprime (Nat.card { x // x ∈ N }) (index N)
hN1 : Nat.card { x // x ∈ N } = 0
⊢ ∃ H, IsComplement' N H
[PROOFSTEP]
rw [hN1, Nat.coprime_zero_left, index_eq_one] at hN
[GOAL]
case pos
n : ℕ
G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : Normal N
hN : N = ⊤
hN1 : Nat.card { x // x ∈ N } = 0
⊢ ∃ H, IsComplement' N H
[PROOFSTEP]
rw [hN]
[GOAL]
case pos
n : ℕ
G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : Normal N
hN : N = ⊤
hN1 : Nat.card { x // x ∈ N } = 0
⊢ ∃ H, IsComplement' ⊤ H
[PROOFSTEP]
exact ⟨⊥, isComplement'_top_bot⟩
[GOAL]
case neg
n : ℕ
G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : Normal N
hN : Nat.coprime (Nat.card { x // x ∈ N }) (index N)
hN1 : ¬Nat.card { x // x ∈ N } = 0
⊢ ∃ H, IsComplement' N H
[PROOFSTEP]
by_cases hN2 : N.index = 0
[GOAL]
case pos
n : ℕ
G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : Normal N
hN : Nat.coprime (Nat.card { x // x ∈ N }) (index N)
hN1 : ¬Nat.card { x // x ∈ N } = 0
hN2 : index N = 0
⊢ ∃ H, IsComplement' N H
[PROOFSTEP]
rw [hN2, Nat.coprime_zero_right] at hN
[GOAL]
case pos
n : ℕ
G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : Normal N
hN : Nat.card { x // x ∈ N } = 1
hN1 : ¬Nat.card { x // x ∈ N } = 0
hN2 : index N = 0
⊢ ∃ H, IsComplement' N H
[PROOFSTEP]
haveI := (Cardinal.toNat_eq_one_iff_unique.mp hN).1
[GOAL]
case pos
n : ℕ
G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : Normal N
hN : Nat.card { x // x ∈ N } = 1
hN1 : ¬Nat.card { x // x ∈ N } = 0
hN2 : index N = 0
this : Subsingleton { x // x ∈ N }
⊢ ∃ H, IsComplement' N H
[PROOFSTEP]
rw [N.eq_bot_of_subsingleton]
[GOAL]
case pos
n : ℕ
G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : Normal N
hN : Nat.card { x // x ∈ N } = 1
hN1 : ¬Nat.card { x // x ∈ N } = 0
hN2 : index N = 0
this : Subsingleton { x // x ∈ N }
⊢ ∃ H, IsComplement' ⊥ H
[PROOFSTEP]
exact ⟨⊤, isComplement'_bot_top⟩
[GOAL]
case neg
n : ℕ
G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : Normal N
hN : Nat.coprime (Nat.card { x // x ∈ N }) (index N)
hN1 : ¬Nat.card { x // x ∈ N } = 0
hN2 : ¬index N = 0
⊢ ∃ H, IsComplement' N H
[PROOFSTEP]
have hN3 : Nat.card G ≠ 0 := by
  rw [← N.card_mul_index]
  exact mul_ne_zero hN1 hN2
[GOAL]
n : ℕ
G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : Normal N
hN : Nat.coprime (Nat.card { x // x ∈ N }) (index N)
hN1 : ¬Nat.card { x // x ∈ N } = 0
hN2 : ¬index N = 0
⊢ Nat.card G ≠ 0
[PROOFSTEP]
rw [← N.card_mul_index]
[GOAL]
n : ℕ
G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : Normal N
hN : Nat.coprime (Nat.card { x // x ∈ N }) (index N)
hN1 : ¬Nat.card { x // x ∈ N } = 0
hN2 : ¬index N = 0
⊢ Nat.card { x // x ∈ N } * index N ≠ 0
[PROOFSTEP]
exact mul_ne_zero hN1 hN2
[GOAL]
case neg
n : ℕ
G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : Normal N
hN : Nat.coprime (Nat.card { x // x ∈ N }) (index N)
hN1 : ¬Nat.card { x // x ∈ N } = 0
hN2 : ¬index N = 0
hN3 : Nat.card G ≠ 0
⊢ ∃ H, IsComplement' N H
[PROOFSTEP]
haveI := (Cardinal.lt_aleph0_iff_fintype.mp (lt_of_not_ge (mt Cardinal.toNat_apply_of_aleph0_le hN3))).some
[GOAL]
case neg
n : ℕ
G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : Normal N
hN : Nat.coprime (Nat.card { x // x ∈ N }) (index N)
hN1 : ¬Nat.card { x // x ∈ N } = 0
hN2 : ¬index N = 0
hN3 : Nat.card G ≠ 0
this : Fintype G
⊢ ∃ H, IsComplement' N H
[PROOFSTEP]
apply exists_right_complement'_of_coprime_of_fintype
[GOAL]
case neg.hN
n : ℕ
G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : Normal N
hN : Nat.coprime (Nat.card { x // x ∈ N }) (index N)
hN1 : ¬Nat.card { x // x ∈ N } = 0
hN2 : ¬index N = 0
hN3 : Nat.card G ≠ 0
this : Fintype G
⊢ Nat.coprime (Fintype.card { x // x ∈ N }) (index N)
[PROOFSTEP]
rwa [← Nat.card_eq_fintype_card]