awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.SchurZassenhaus (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : IsMulCommutative.{u_1} ↥H
inst_2 : H.FiniteIndex
α β : H.LeftTransversal
inst_3 : H.Normal
h : ↥H
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex
⊢ Eq.{u_1 + 1} (α := ↥H)
    (∏ q : G ⧸ H,
      (MonoidHom.id ↥H : (a : ↥H) → ↥H)
        (Subtype.mk (p := fun (x : G) ↦ x ∈ H)
          (HMul.hMul (α := G)
            (↑((⋯.leftQuotientEquiv (S := (↑α : Set G)) : (a : G ⧸ H) → (↑(↑α : Set G) : Type u_1)) q) : G)⁻¹
            (↑((⋯.leftQuotientEquiv (S := (↑(op (↑h : G) • β) : Set G)) :
                    (a : G ⧸ H) → (↑(↑(op (↑h : G) • β) : Set G) : Type u_1))
                  q) :
              G))
          ⋯))
    (∏ x : G ⧸ H,
      HMul.hMul (α := ↥H)
        ((MonoidHom.id ↥H : (a : ↥H) → ↥H)
            (Subtype.mk (p := fun (x : G) ↦ x ∈ H)
              (HMul.hMul (α := G)
                (↑((⋯.leftQuotientEquiv (S := (↑α : Set G)) : (a : G ⧸ H) → (↑(↑α : Set G) : Type u_1)) x) : G)⁻¹
                (↑((⋯.leftQuotientEquiv (S := (↑β : Set G)) : (a : G ⧸ H) → (↑(↑β : Set G) : Type u_1)) x) : G))
              ⋯) :
          ↥H)
        h)
have refine : ∀ (q : G ⧸ H),
  Membership.mem (γ := Finset (G ⧸ H)) Finset.univ q →
    (MonoidHom.id ↥H : (a : ↥H) → ↥H)
        (Subtype.mk (p := fun (x : G) ↦ x ∈ H)
          (HMul.hMul (α := G)
            (↑((sorry.leftQuotientEquiv (S := (↑α : Set G)) : (a : G ⧸ H) → (↑(↑α : Set G) : Type u_1)) q) : G)⁻¹
            (↑((sorry.leftQuotientEquiv (S := (↑(op (↑h : G) • β) : Set G)) :
                    (a : G ⧸ H) → (↑(↑(op (↑h : G) • β) : Set G) : Type u_1))
                  q) :
              G))
          sorry) =
      HMul.hMul (α := ↥H)
        ((MonoidHom.id ↥H : (a : ↥H) → ↥H)
            (Subtype.mk (p := fun (x : G) ↦ x ∈ H)
              (HMul.hMul (α := G)
                (↑((sorry.leftQuotientEquiv (S := (↑α : Set G)) : (a : G ⧸ H) → (↑(↑α : Set G) : Type u_1)) q) : G)⁻¹
                (↑((sorry.leftQuotientEquiv (S := (↑β : Set G)) : (a : G ⧸ H) → (↑(↑β : Set G) : Type u_1)) q) : G))
              sorry) :
          ↥H)
        h
Tactic: refine Finset.prod_congr rfl fun q _ => ?_
-- Lean 4 proof step from Mathlib.GroupTheory.SchurZassenhaus (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : IsMulCommutative.{u_1} ↥H
inst_2 : H.FiniteIndex
α β : H.LeftTransversal
inst_3 : H.Normal
h : ↥H
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex
q : G ⧸ H
h_1 : Membership.mem (γ := Finset (G ⧸ H)) Finset.univ q
⊢ (MonoidHom.id ↥H : (a : ↥H) → ↥H)
      (Subtype.mk (p := fun (x : G) ↦ x ∈ H)
        (HMul.hMul (α := G)
          (↑((⋯.leftQuotientEquiv (S := (↑α : Set G)) : (a : G ⧸ H) → (↑(↑α : Set G) : Type u_1)) q) : G)⁻¹
          (↑((⋯.leftQuotientEquiv (S := (↑(op (↑h : G) • β) : Set G)) :
                  (a : G ⧸ H) → (↑(↑(op (↑h : G) • β) : Set G) : Type u_1))
                q) :
            G))
        ⋯) =
    HMul.hMul (α := ↥H)
      ((MonoidHom.id ↥H : (a : ↥H) → ↥H)
          (Subtype.mk (p := fun (x : G) ↦ x ∈ H)
            (HMul.hMul (α := G)
              (↑((⋯.leftQuotientEquiv (S := (↑α : Set G)) : (a : G ⧸ H) → (↑(↑α : Set G) : Type u_1)) q) : G)⁻¹
              (↑((⋯.leftQuotientEquiv (S := (↑β : Set G)) : (a : G ⧸ H) → (↑(↑β : Set G) : Type u_1)) q) : G))
            ⋯) :
        ↥H)
      h
have simp_rw : (↑((sorry.leftQuotientEquiv (S := (↑(op (↑h : G) • β) : Set G)) : (a : G ⧸ H) → (↑(↑(op (↑h : G) • β) : Set G) : Type u_1))
        q) :
    G) =
  (↑((sorry.leftQuotientEquiv (S := (↑β : Set G)) : (a : G ⧸ H) → (↑(↑β : Set G) : Type u_1)) q) : G) * (↑h : G)
Tactic: simp_rw [Subtype.ext_iff, MonoidHom.id_apply, coe_mul, mul_assoc, mul_right_inj]
-- Lean 4 proof step from Mathlib.GroupTheory.SchurZassenhaus (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : IsMulCommutative.{u_1} ↥H
inst_2 : H.FiniteIndex
α β : H.LeftTransversal
inst_3 : H.Normal
h : ↥H
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex
q : G ⧸ H
h_1 : Membership.mem (γ := Finset (G ⧸ H)) Finset.univ q
⊢ (↑((⋯.leftQuotientEquiv (S := (↑(op (↑h : G) • β) : Set G)) :
            (a : G ⧸ H) → (↑(↑(op (↑h : G) • β) : Set G) : Type u_1))
          q) :
      G) =
    (↑((⋯.leftQuotientEquiv (S := (↑β : Set G)) : (a : G ⧸ H) → (↑(↑β : Set G) : Type u_1)) q) : G) * (↑h : G)
have rw : q = op (↑h : G) • q
Tactic: rw [smul_apply_eq_smul_apply_inv_smul, smul_eq_mul_unop, MulOpposite.unop_op, mul_left_inj,
    ← Subtype.ext_iff, Equiv.apply_eq_iff_eq, inv_smul_eq_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.SchurZassenhaus (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : IsMulCommutative.{u_1} ↥H
inst_2 : H.FiniteIndex
inst_3 : H.Normal
hH : (Nat.card.{u_1} ↥H).Coprime H.index
α_1 : H.QuotientDiff
h : ↥H
α : H.LeftTransversal
hα : HSMul.hSMul (β := H.QuotientDiff) h (Quotient.mk'' α) = Quotient.mk'' α
⊢ h ^ H.index = diff (MonoidHom.id ↥H) (op (↑h⁻¹ : G) • α) α
have rw : h ^ H.index = (diff (MonoidHom.id ↥H) α (op (↑h⁻¹ : G) • α))⁻¹
Tactic: rw [← diff_inv, smul_diff', diff_self, one_mul, inv_pow, inv_inv]
-- Lean 4 proof step from Mathlib.GroupTheory.SchurZassenhaus (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : IsMulCommutative.{u_1} ↥H
inst_2 : H.FiniteIndex
inst_3 : H.Normal
hH : (Nat.card.{u_1} ↥H).Coprime H.index
α_1 : H.QuotientDiff
h : ↥H
α : H.LeftTransversal
hα : HSMul.hSMul (β := H.QuotientDiff) h (Quotient.mk'' α) = Quotient.mk'' α
rw : h ^ H.index = (diff (MonoidHom.id ↥H) α (op (↑h⁻¹ : G) • α))⁻¹
⊢ h ^ H.index = diff (MonoidHom.id ↥H) (op (↑h⁻¹ : G) • α) α
have rw₁ : h ^ H.index = (diff (MonoidHom.id ↥H) α α * h⁻¹ ^ H.index)⁻¹
Tactic: rw [← diff_inv, smul_diff', diff_self, one_mul, inv_pow, inv_inv]
-- Lean 4 proof step from Mathlib.GroupTheory.SchurZassenhaus (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : IsMulCommutative.{u_1} ↥H
inst_2 : H.FiniteIndex
inst_3 : H.Normal
hH : (Nat.card.{u_1} ↥H).Coprime H.index
α_1 : H.QuotientDiff
h : ↥H
α : H.LeftTransversal
hα : HSMul.hSMul (β := H.QuotientDiff) h (Quotient.mk'' α) = Quotient.mk'' α
rw : h ^ H.index = (diff (MonoidHom.id ↥H) α (op (↑h⁻¹ : G) • α))⁻¹
rw₁ : h ^ H.index = (diff (MonoidHom.id ↥H) α α * h⁻¹ ^ H.index)⁻¹
⊢ h ^ H.index = diff (MonoidHom.id ↥H) (op (↑h⁻¹ : G) • α) α
have rw₂ : h ^ H.index = (1 * h⁻¹ ^ H.index)⁻¹
Tactic: rw [← diff_inv, smul_diff', diff_self, one_mul, inv_pow, inv_inv]
-- Lean 4 proof step from Mathlib.GroupTheory.SchurZassenhaus (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : IsMulCommutative.{u_1} ↥H
inst_2 : H.FiniteIndex
inst_3 : H.Normal
hH : (Nat.card.{u_1} ↥H).Coprime H.index
α_1 : H.QuotientDiff
h : ↥H
α : H.LeftTransversal
hα : HSMul.hSMul (β := H.QuotientDiff) h (Quotient.mk'' α) = Quotient.mk'' α
rw : h ^ H.index = (diff (MonoidHom.id ↥H) α (op (↑h⁻¹ : G) • α))⁻¹
rw₁ : h ^ H.index = (diff (MonoidHom.id ↥H) α α * h⁻¹ ^ H.index)⁻¹
rw₂ : h ^ H.index = (1 * h⁻¹ ^ H.index)⁻¹
⊢ h ^ H.index = diff (MonoidHom.id ↥H) (op (↑h⁻¹ : G) • α) α
have rw₃ : h ^ H.index = (h⁻¹ ^ H.index)⁻¹
Tactic: rw [← diff_inv, smul_diff', diff_self, one_mul, inv_pow, inv_inv]
-- Lean 4 proof step from Mathlib.GroupTheory.SchurZassenhaus (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : IsMulCommutative.{u_1} ↥H
inst_2 : H.FiniteIndex
inst_3 : H.Normal
hH : (Nat.card.{u_1} ↥H).Coprime H.index
α_1 : H.QuotientDiff
h : ↥H
α : H.LeftTransversal
hα : HSMul.hSMul (β := H.QuotientDiff) h (Quotient.mk'' α) = Quotient.mk'' α
rw : h ^ H.index = (diff (MonoidHom.id ↥H) α (op (↑h⁻¹ : G) • α))⁻¹
rw₁ : h ^ H.index = (diff (MonoidHom.id ↥H) α α * h⁻¹ ^ H.index)⁻¹
rw₂ : h ^ H.index = (1 * h⁻¹ ^ H.index)⁻¹
rw₃ : h ^ H.index = (h⁻¹ ^ H.index)⁻¹
⊢ h ^ H.index = diff (MonoidHom.id ↥H) (op (↑h⁻¹ : G) • α) α
have rw₄ : h ^ H.index = (h ^ H.index)⁻¹⁻¹
Tactic: rw [← diff_inv, smul_diff', diff_self, one_mul, inv_pow, inv_inv]
-- Lean 4 proof step from Mathlib.GroupTheory.SchurZassenhaus (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : IsMulCommutative.{u_1} ↥H
inst_2 : H.FiniteIndex
inst_3 : H.Normal
hH : (Nat.card.{u_1} ↥H).Coprime H.index
α_1 : H.QuotientDiff
h : ↥H
α : H.LeftTransversal
hα : HSMul.hSMul (β := H.QuotientDiff) h (Quotient.mk'' α) = Quotient.mk'' α
rw : h ^ H.index = (diff (MonoidHom.id ↥H) α (op (↑h⁻¹ : G) • α))⁻¹
rw₁ : h ^ H.index = (diff (MonoidHom.id ↥H) α α * h⁻¹ ^ H.index)⁻¹
rw₂ : h ^ H.index = (1 * h⁻¹ ^ H.index)⁻¹
rw₃ : h ^ H.index = (h⁻¹ ^ H.index)⁻¹
rw₄ : h ^ H.index = (h ^ H.index)⁻¹⁻¹
⊢ h ^ H.index = diff (MonoidHom.id ↥H) (op (↑h⁻¹ : G) • α) α
have rw₅ : h ^ H.index = h ^ H.index
Tactic: rw [← diff_inv, smul_diff', diff_self, one_mul, inv_pow, inv_inv]
-- Lean 4 proof step from Mathlib.GroupTheory.SchurZassenhaus (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : IsMulCommutative.{u_1} ↥H
inst_2 : H.FiniteIndex
inst_3 : H.Normal
hH : (Nat.card.{u_1} ↥H).Coprime H.index
α_1 β_1 : H.QuotientDiff
β α : H.LeftTransversal
⊢ diff (MonoidHom.id ↥H) β α *
      HPow.hPow (α := ↥H) (((powCoprime hH).symm : (a : ↥H) → ↥H) (diff (MonoidHom.id ↥H) β α))⁻¹ H.index =
    1
have rw : diff (MonoidHom.id ↥H) β α *
    (HPow.hPow (α := ↥H) (((powCoprime hH).symm : (a : ↥H) → ↥H) (diff (MonoidHom.id ↥H) β α)) H.index)⁻¹ =
  1
Tactic: rw [inv_pow, ← powCoprime_apply hH, Equiv.apply_symm_apply, mul_inv_cancel]
-- Lean 4 proof step from Mathlib.GroupTheory.SchurZassenhaus (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : IsMulCommutative.{u_1} ↥H
inst_2 : H.FiniteIndex
inst_3 : H.Normal
hH : (Nat.card.{u_1} ↥H).Coprime H.index
α_1 β_1 : H.QuotientDiff
β α : H.LeftTransversal
rw :
  diff (MonoidHom.id ↥H) β α *
      (HPow.hPow (α := ↥H) (((powCoprime hH).symm : (a : ↥H) → ↥H) (diff (MonoidHom.id ↥H) β α)) H.index)⁻¹ =
    1
⊢ diff (MonoidHom.id ↥H) β α *
      HPow.hPow (α := ↥H) (((powCoprime hH).symm : (a : ↥H) → ↥H) (diff (MonoidHom.id ↥H) β α))⁻¹ H.index =
    1
have rw₁ : HMul.hMul (α := ↥H) (β := ↥H) (diff (MonoidHom.id ↥H) β α : ↥H)
    (((powCoprime hH : (a : ↥H) → ↥H) (((powCoprime hH).symm : (a : ↥H) → ↥H) (diff (MonoidHom.id ↥H) β α)))⁻¹ : ↥H) =
  1
Tactic: rw [inv_pow, ← powCoprime_apply hH, Equiv.apply_symm_apply, mul_inv_cancel]
-- Lean 4 proof step from Mathlib.GroupTheory.SchurZassenhaus (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : IsMulCommutative.{u_1} ↥H
inst_2 : H.FiniteIndex
inst_3 : H.Normal
hH : (Nat.card.{u_1} ↥H).Coprime H.index
α_1 β_1 : H.QuotientDiff
β α : H.LeftTransversal
rw :
  diff (MonoidHom.id ↥H) β α *
      (HPow.hPow (α := ↥H) (((powCoprime hH).symm : (a : ↥H) → ↥H) (diff (MonoidHom.id ↥H) β α)) H.index)⁻¹ =
    1
rw₁ :
  HMul.hMul (α := ↥H) (β := ↥H) (diff (MonoidHom.id ↥H) β α : ↥H)
      (((powCoprime hH : (a : ↥H) → ↥H) (((powCoprime hH).symm : (a : ↥H) → ↥H) (diff (MonoidHom.id ↥H) β α)))⁻¹ : ↥H) =
    1
⊢ diff (MonoidHom.id ↥H) β α *
      HPow.hPow (α := ↥H) (((powCoprime hH).symm : (a : ↥H) → ↥H) (diff (MonoidHom.id ↥H) β α))⁻¹ H.index =
    1
have rw₂ : HMul.hMul (α := ↥H) (diff (MonoidHom.id ↥H) β α) (diff (MonoidHom.id ↥H) β α)⁻¹ = 1
Tactic: rw [inv_pow, ← powCoprime_apply hH, Equiv.apply_symm_apply, mul_inv_cancel]
-- Lean 4 proof step from Mathlib.GroupTheory.SchurZassenhaus (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : IsMulCommutative.{u_1} ↥H
inst_2 : H.FiniteIndex
inst_3 : H.Normal
hH : (Nat.card.{u_1} ↥H).Coprime H.index
α_1 β_1 : H.QuotientDiff
β α : H.LeftTransversal
rw :
  diff (MonoidHom.id ↥H) β α *
      (HPow.hPow (α := ↥H) (((powCoprime hH).symm : (a : ↥H) → ↥H) (diff (MonoidHom.id ↥H) β α)) H.index)⁻¹ =
    1
rw₁ :
  HMul.hMul (α := ↥H) (β := ↥H) (diff (MonoidHom.id ↥H) β α : ↥H)
      (((powCoprime hH : (a : ↥H) → ↥H) (((powCoprime hH).symm : (a : ↥H) → ↥H) (diff (MonoidHom.id ↥H) β α)))⁻¹ : ↥H) =
    1
rw₂ : HMul.hMul (α := ↥H) (diff (MonoidHom.id ↥H) β α) (diff (MonoidHom.id ↥H) β α)⁻¹ = 1
⊢ diff (MonoidHom.id ↥H) β α *
      HPow.hPow (α := ↥H) (((powCoprime hH).symm : (a : ↥H) → ↥H) (diff (MonoidHom.id ↥H) β α))⁻¹ H.index =
    1
have rw₃ : Eq.{u_1 + 1} (α := ↥H) 1 1
Tactic: rw [inv_pow, ← powCoprime_apply hH, Equiv.apply_symm_apply, mul_inv_cancel]
-- Lean 4 proof step from Mathlib.GroupTheory.SchurZassenhaus (goal)
Goal:
G : Type u
inst : Group G
N : Subgroup G
inst_1 : N.Normal
h1 : (Nat.card.{u} ↥N).Coprime N.index
h2 :
  ∀ (G' : Type u) [inst : Group G'] [Finite G'],
    Nat.card G' < Nat.card G →
      ∀ {N' : Subgroup G'} [N'.Normal], (Nat.card.{u} ↥N').Coprime N'.index → ∃ (H' : Subgroup G'), N'.IsComplement' H'
h3 : ∀ (H : Subgroup G), ¬N.IsComplement' H
inst_2 : Finite G
K : Subgroup G
hK : K ⊔ N = ⊤
⊢ K = ⊤
have contrapose! : ∀ (h3 : K ≠ ⊤), ∃ (H : Subgroup G), N.IsComplement' H
Tactic: contrapose! h3
Cleared hypotheses: h3
-- Lean 4 proof step from Mathlib.GroupTheory.SchurZassenhaus (goal)
Goal:
G : Type u
inst : Group G
N : Subgroup G
inst_1 : N.Normal
h1 : (Nat.card.{u} ↥N).Coprime N.index
h2 :
  ∀ (G' : Type u) [inst : Group G'] [Finite G'],
    Nat.card G' < Nat.card G →
      ∀ {N' : Subgroup G'} [N'.Normal], (Nat.card.{u} ↥N').Coprime N'.index → ∃ (H' : Subgroup G'), N'.IsComplement' H'
inst_2 : Finite G
K : Subgroup G
hK : K ⊔ N = ⊤
h3 : K ≠ ⊤
⊢ (comap K.subtype N).index = N.index
have rw : (comap K.subtype N).index = N.relIndex (K ⊔ N)
Tactic: rw [← N.relIndex_top_right, ← hK]
-- Lean 4 proof step from Mathlib.GroupTheory.SchurZassenhaus (hypothesis)
Goal:
G : Type u
inst : Group G
N : Subgroup G
inst_1 : N.Normal
h1 : (Nat.card.{u} ↥N).Coprime N.index
h2 :
  ∀ (G' : Type u) [inst : Group G'] [Finite G'],
    Nat.card G' < Nat.card G →
      ∀ {N' : Subgroup G'} [N'.Normal], (Nat.card.{u} ↥N').Coprime N'.index → ∃ (H' : Subgroup G'), N'.IsComplement' H'
inst_2 : Finite G
K : Subgroup G
hK : K ⊔ N = ⊤
h3 : K ≠ ⊤
⊢ ∃ (H : Subgroup G), N.IsComplement' H
have h4 : (comap K.subtype N).index = N.index
Tactic: have h4 : (N.comap K.subtype).index = N.index := by
    rw [← N.relIndex_top_right, ← hK]
    exact (relIndex_sup_right K N).symm
-- Lean 4 proof step from Mathlib.GroupTheory.SchurZassenhaus (goal)
Goal:
G : Type u
inst : Group G
N : Subgroup G
inst_1 : N.Normal
h1 : (Nat.card.{u} ↥N).Coprime N.index
h2 :
  ∀ (G' : Type u) [inst : Group G'] [Finite G'],
    Nat.card G' < Nat.card G →
      ∀ {N' : Subgroup G'} [N'.Normal], (Nat.card.{u} ↥N').Coprime N'.index → ∃ (H' : Subgroup G'), N'.IsComplement' H'
inst_2 : Finite G
K : Subgroup G
hK : K ⊔ N = ⊤
h3 : K ≠ ⊤
h4 : (comap K.subtype N).index = N.index
⊢ Nat.card.{u} ↥K < Nat.card G
have rw : Nat.card.{u} ↥K < K.index * Nat.card.{u} ↥K
Tactic: rw [← K.index_mul_card]
-- Lean 4 proof step from Mathlib.GroupTheory.SchurZassenhaus (hypothesis)
Goal:
G : Type u
inst : Group G
N : Subgroup G
inst_1 : N.Normal
h1 : (Nat.card.{u} ↥N).Coprime N.index
h2 :
  ∀ (G' : Type u) [inst : Group G'] [Finite G'],
    Nat.card G' < Nat.card G →
      ∀ {N' : Subgroup G'} [N'.Normal], (Nat.card.{u} ↥N').Coprime N'.index → ∃ (H' : Subgroup G'), N'.IsComplement' H'
inst_2 : Finite G
K : Subgroup G
hK : K ⊔ N = ⊤
h3 : K ≠ ⊤
h4 : (comap K.subtype N).index = N.index
⊢ ∃ (H : Subgroup G), N.IsComplement' H
have h5 : Nat.card.{u} ↥K < Nat.card G
Tactic: have h5 : Nat.card K < Nat.card G := by
    rw [← K.index_mul_card]
    exact lt_mul_of_one_lt_left Nat.card_pos (one_lt_index_of_ne_top h3)
-- Lean 4 proof step from Mathlib.GroupTheory.SchurZassenhaus (goal)
Goal:
G : Type u
inst : Group G
N : Subgroup G
inst_1 : N.Normal
h1 : (Nat.card.{u} ↥N).Coprime N.index
h2 :
  ∀ (G' : Type u) [inst : Group G'] [Finite G'],
    Nat.card G' < Nat.card G →
      ∀ {N' : Subgroup G'} [N'.Normal], (Nat.card.{u} ↥N').Coprime N'.index → ∃ (H' : Subgroup G'), N'.IsComplement' H'
inst_2 : Finite G
K : Subgroup G
hK : K ⊔ N = ⊤
h3 : K ≠ ⊤
h4 : (comap K.subtype N).index = N.index
h5 : Nat.card.{u} ↥K < Nat.card G
⊢ (Nat.card.{u} ↥(comap K.subtype N)).Coprime (comap K.subtype N).index
have rw : (Nat.card.{u} ↥(comap K.subtype N)).Coprime N.index
Tactic: rw [h4]
-- Lean 4 proof step from Mathlib.GroupTheory.SchurZassenhaus (hypothesis)
Goal:
G : Type u
inst : Group G
N : Subgroup G
inst_1 : N.Normal
h1 : (Nat.card.{u} ↥N).Coprime N.index
h2 :
  ∀ (G' : Type u) [inst : Group G'] [Finite G'],
    Nat.card G' < Nat.card G →
      ∀ {N' : Subgroup G'} [N'.Normal], (Nat.card.{u} ↥N').Coprime N'.index → ∃ (H' : Subgroup G'), N'.IsComplement' H'
inst_2 : Finite G
K : Subgroup G
hK : K ⊔ N = ⊤
h3 : K ≠ ⊤
h4 : (comap K.subtype N).index = N.index
h5 : Nat.card.{u} ↥K < Nat.card G
⊢ ∃ (H : Subgroup G), N.IsComplement' H
have h6 : (Nat.card.{u} ↥(comap K.subtype N)).Coprime (comap K.subtype N).index
Tactic: have h6 : Nat.Coprime (Nat.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)
-- Lean 4 proof step from Mathlib.GroupTheory.SchurZassenhaus (goal)
Goal:
G : Type u
inst : Group G
N : Subgroup G
inst_1 : N.Normal
h1 : (Nat.card.{u} ↥N).Coprime N.index
h2 :
  ∀ (G' : Type u) [inst : Group G'] [Finite G'],
    Nat.card G' < Nat.card G →
      ∀ {N' : Subgroup G'} [N'.Normal], (Nat.card.{u} ↥N').Coprime N'.index → ∃ (H' : Subgroup G'), N'.IsComplement' H'
inst_2 : Finite G
K : Subgroup G
hK : K ⊔ N = ⊤
h3 : K ≠ ⊤
h4 : (comap K.subtype N).index = N.index
h5 : Nat.card.{u} ↥K < Nat.card G
h6 : (Nat.card.{u} ↥(comap K.subtype N)).Coprime (comap K.subtype N).index
⊢ ∃ (H : Subgroup G), N.IsComplement' H
have obtain : ∀ (H : Subgroup ↥K) (hH : (comap K.subtype N).IsComplement' H), ∃ (H : Subgroup G), N.IsComplement' H
Tactic: obtain ⟨H, hH⟩ := h2 K h5 h6
-- Lean 4 proof step from Mathlib.GroupTheory.SchurZassenhaus (goal)
Goal:
G : Type u
inst : Group G
N : Subgroup G
inst_1 : N.Normal
h1 : (Nat.card.{u} ↥N).Coprime N.index
h2 :
  ∀ (G' : Type u) [inst : Group G'] [Finite G'],
    Nat.card G' < Nat.card G →
      ∀ {N' : Subgroup G'} [N'.Normal], (Nat.card.{u} ↥N').Coprime N'.index → ∃ (H' : Subgroup G'), N'.IsComplement' H'
inst_2 : Finite G
K : Subgroup G
hK : K ⊔ N = ⊤
h3 : K ≠ ⊤
h4 : (comap K.subtype N).index = N.index
h5 : Nat.card.{u} ↥K < Nat.card G
h6 : (Nat.card.{u} ↥(comap K.subtype N)).Coprime (comap K.subtype N).index
H : Subgroup ↥K
hH : (comap K.subtype N).IsComplement' H
⊢ Nat.card.{u} ↥(map K.subtype H) = N.index
have rw : relIndex ⊥ (map K.subtype H) = N.index
Tactic: rw [← relIndex_bot_left, ← relIndex_comap, MonoidHom.comap_bot, Subgroup.ker_subtype,
      relIndex_bot_left, ← IsComplement'.index_eq_card (IsComplement'.symm hH), index_comap,
      range_subtype, ← relIndex_sup_right, hK, relIndex_top_right]
-- Lean 4 proof step from Mathlib.GroupTheory.SchurZassenhaus (goal)
Goal:
G : Type u
inst : Group G
N : Subgroup G
inst_1 : N.Normal
h1 : (Nat.card.{u} ↥N).Coprime N.index
h2 :
  ∀ (G' : Type u) [inst : Group G'] [Finite G'],
    Nat.card G' < Nat.card G →
      ∀ {N' : Subgroup G'} [N'.Normal], (Nat.card.{u} ↥N').Coprime N'.index → ∃ (H' : Subgroup G'), N'.IsComplement' H'
inst_2 : Finite G
K : Subgroup G
hK : K ⊔ N = ⊤
h3 : K ≠ ⊤
h4 : (comap K.subtype N).index = N.index
h5 : Nat.card.{u} ↥K < Nat.card G
h6 : (Nat.card.{u} ↥(comap K.subtype N)).Coprime (comap K.subtype N).index
H : Subgroup ↥K
hH : (comap K.subtype N).IsComplement' H
rw : relIndex ⊥ (map K.subtype H) = N.index
⊢ Nat.card.{u} ↥(map K.subtype H) = N.index
have rw₁ : (comap K.subtype ⊥).relIndex H = N.index
Tactic: rw [← relIndex_bot_left, ← relIndex_comap, MonoidHom.comap_bot, Subgroup.ker_subtype,
      relIndex_bot_left, ← IsComplement'.index_eq_card (IsComplement'.symm hH), index_comap,
      range_subtype, ← relIndex_sup_right, hK, relIndex_top_right]
-- Lean 4 proof step from Mathlib.GroupTheory.SchurZassenhaus (goal)
Goal:
G : Type u
inst : Group G
N : Subgroup G
inst_1 : N.Normal
h1 : (Nat.card.{u} ↥N).Coprime N.index
h2 :
  ∀ (G' : Type u) [inst : Group G'] [Finite G'],
    Nat.card G' < Nat.card G →
      ∀ {N' : Subgroup G'} [N'.Normal], (Nat.card.{u} ↥N').Coprime N'.index → ∃ (H' : Subgroup G'), N'.IsComplement' H'
inst_2 : Finite G
K : Subgroup G
hK : K ⊔ N = ⊤
h3 : K ≠ ⊤
h4 : (comap K.subtype N).index = N.index
h5 : Nat.card.{u} ↥K < Nat.card G
h6 : (Nat.card.{u} ↥(comap K.subtype N)).Coprime (comap K.subtype N).index
H : Subgroup ↥K
hH : (comap K.subtype N).IsComplement' H
rw : relIndex ⊥ (map K.subtype H) = N.index
rw₁ : (comap K.subtype ⊥).relIndex H = N.index
⊢ Nat.card.{u} ↥(map K.subtype H) = N.index
have rw₂ : K.subtype.ker.relIndex H = N.index
Tactic: rw [← relIndex_bot_left, ← relIndex_comap, MonoidHom.comap_bot, Subgroup.ker_subtype,
      relIndex_bot_left, ← IsComplement'.index_eq_card (IsComplement'.symm hH), index_comap,
      range_subtype, ← relIndex_sup_right, hK, relIndex_top_right]
-- Lean 4 proof step from Mathlib.GroupTheory.SchurZassenhaus (goal)
Goal:
G : Type u
inst : Group G
N : Subgroup G
inst_1 : N.Normal
h1 : (Nat.card.{u} ↥N).Coprime N.index
h2 :
  ∀ (G' : Type u) [inst : Group G'] [Finite G'],
    Nat.card G' < Nat.card G →
      ∀ {N' : Subgroup G'} [N'.Normal], (Nat.card.{u} ↥N').Coprime N'.index → ∃ (H' : Subgroup G'), N'.IsComplement' H'
inst_2 : Finite G
K : Subgroup G
hK : K ⊔ N = ⊤
h3 : K ≠ ⊤
h4 : (comap K.subtype N).index = N.index
h5 : Nat.card.{u} ↥K < Nat.card G
h6 : (Nat.card.{u} ↥(comap K.subtype N)).Coprime (comap K.subtype N).index
H : Subgroup ↥K
hH : (comap K.subtype N).IsComplement' H
rw : relIndex ⊥ (map K.subtype H) = N.index
rw₁ : (comap K.subtype ⊥).relIndex H = N.index
rw₂ : K.subtype.ker.relIndex H = N.index
⊢ Nat.card.{u} ↥(map K.subtype H) = N.index
have rw₃ : relIndex ⊥ H = N.index
Tactic: rw [← relIndex_bot_left, ← relIndex_comap, MonoidHom.comap_bot, Subgroup.ker_subtype,
      relIndex_bot_left, ← IsComplement'.index_eq_card (IsComplement'.symm hH), index_comap,
      range_subtype, ← relIndex_sup_right, hK, relIndex_top_right]
-- Lean 4 proof step from Mathlib.GroupTheory.SchurZassenhaus (goal)
Goal:
G : Type u
inst : Group G
N : Subgroup G
inst_1 : N.Normal
h1 : (Nat.card.{u} ↥N).Coprime N.index
h2 :
  ∀ (G' : Type u) [inst : Group G'] [Finite G'],
    Nat.card G' < Nat.card G →
      ∀ {N' : Subgroup G'} [N'.Normal], (Nat.card.{u} ↥N').Coprime N'.index → ∃ (H' : Subgroup G'), N'.IsComplement' H'
inst_2 : Finite G
K : Subgroup G
hK : K ⊔ N = ⊤
h3 : K ≠ ⊤
h4 : (comap K.subtype N).index = N.index
h5 : Nat.card.{u} ↥K < Nat.card G
h6 : (Nat.card.{u} ↥(comap K.subtype N)).Coprime (comap K.subtype N).index
H : Subgroup ↥K
hH : (comap K.subtype N).IsComplement' H
rw : relIndex ⊥ (map K.subtype H) = N.index
rw₁ : (comap K.subtype ⊥).relIndex H = N.index
rw₂ : K.subtype.ker.relIndex H = N.index
rw₃ : relIndex ⊥ H = N.index
⊢ Nat.card.{u} ↥(map K.subtype H) = N.index
have rw₄ : Nat.card.{u} ↥H = N.index
Tactic: rw [← relIndex_bot_left, ← relIndex_comap, MonoidHom.comap_bot, Subgroup.ker_subtype,
      relIndex_bot_left, ← IsComplement'.index_eq_card (IsComplement'.symm hH), index_comap,
      range_subtype, ← relIndex_sup_right, hK, relIndex_top_right]
-- Lean 4 proof step from Mathlib.GroupTheory.SchurZassenhaus (goal)
Goal:
G : Type u
inst : Group G
N : Subgroup G
inst_1 : N.Normal
h1 : (Nat.card.{u} ↥N).Coprime N.index
h2 :
  ∀ (G' : Type u) [inst : Group G'] [Finite G'],
    Nat.card G' < Nat.card G →
      ∀ {N' : Subgroup G'} [N'.Normal], (Nat.card.{u} ↥N').Coprime N'.index → ∃ (H' : Subgroup G'), N'.IsComplement' H'
inst_2 : Finite G
K : Subgroup G
hK : K ⊔ N = ⊤
h3 : K ≠ ⊤
h4 : (comap K.subtype N).index = N.index
h5 : Nat.card.{u} ↥K < Nat.card G
h6 : (Nat.card.{u} ↥(comap K.subtype N)).Coprime (comap K.subtype N).index
H : Subgroup ↥K
hH : (comap K.subtype N).IsComplement' H
rw : relIndex ⊥ (map K.subtype H) = N.index
rw₁ : (comap K.subtype ⊥).relIndex H = N.index
rw₂ : K.subtype.ker.relIndex H = N.index
rw₃ : relIndex ⊥ H = N.index
rw₄ : Nat.card.{u} ↥H = N.index
rw₅ : (comap K.subtype N).index = N.index
⊢ Nat.card.{u} ↥(map K.subtype H) = N.index
have rw₆ : N.relIndex K.subtype.range = N.index
Tactic: rw [← relIndex_bot_left, ← relIndex_comap, MonoidHom.comap_bot, Subgroup.ker_subtype,
      relIndex_bot_left, ← IsComplement'.index_eq_card (IsComplement'.symm hH), index_comap,
      range_subtype, ← relIndex_sup_right, hK, relIndex_top_right]