awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
Goal:
G : Type u_1
M : Type u_2
inst : Group G
inst_1 : Group M
inst_2 : Finite G
inst_3 : Finite M
f : G →* M
h : Nat.card.{u_1} ↥f.ker ≤ Nat.card G / Nat.card M
⊢ (↑⊤ : Set M).ncard ≤ (↑f.range : Set M).ncard
have rw : Nat.card M ≤ Nat.card.{u_1} (G ⧸ f.ker)
Tactic: rw [Subgroup.coe_top, Set.ncard_univ, ← Nat.card_coe_set_eq, SetLike.coe_sort_coe,
    ← Nat.card_congr (QuotientGroup.quotientKerEquivRange f).toEquiv]
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
Goal:
G : Type u_1
M : Type u_2
F : Type u_3
inst : Group G
inst_1 : Fintype G
inst_2 : Monoid M
inst_3 : DecidableEq M
inst_4 : FunLike F G M
inst_5 : MonoidHomClass F G M
f : F
x y : M
hx : Membership.mem (γ := Set M) (Set.range.{u_2, u_1 + 1} (ι := G) (⇑f : (a : G) → M)) x
hy : Membership.mem (γ := Set M) (Set.range.{u_2, u_1 + 1} (ι := G) (⇑f : (a : G) → M)) y
⊢ card.{u_1} (α := G) {g : G | (f : (a : G) → M) g = x} = card.{u_1} (α := G) {g : G | (f : (a : G) → M) g = y}
have rcases : ∀ (x : G),
  card.{u_1} (α := G) {g : G | Eq.{u_2 + 1} (α := M) ((f : (a : G) → M) g : M) ((f : (a : G) → M) x : M)} =
    card.{u_1} (α := G) {g : G | (f : (a : G) → M) g = y}
Tactic: rcases hx with ⟨x, rfl⟩
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
Goal:
G : Type u_1
M : Type u_2
F : Type u_3
inst : Group G
inst_1 : Fintype G
inst_2 : Monoid M
inst_3 : DecidableEq M
inst_4 : FunLike F G M
inst_5 : MonoidHomClass F G M
f : F
y : M
hy : Membership.mem (γ := Set M) (Set.range.{u_2, u_1 + 1} (ι := G) (⇑f : (a : G) → M)) y
x : G
⊢ card.{u_1} (α := G) {g : G | Eq.{u_2 + 1} (α := M) ((f : (a : G) → M) g : M) ((f : (a : G) → M) x : M)} =
    card.{u_1} (α := G) {g : G | (f : (a : G) → M) g = y}
have rcases : ∀ (y : G),
  card.{u_1} (α := G) {g : G | Eq.{u_2 + 1} (α := M) ((f : (a : G) → M) g : M) ((f : (a : G) → M) x : M)} =
    card.{u_1} (α := G) {g : G | Eq.{u_2 + 1} (α := M) ((f : (a : G) → M) g : M) ((f : (a : G) → M) y : M)}
Tactic: rcases hy with ⟨y, rfl⟩
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
Goal:
G : Type u_1
M : Type u_2
F : Type u_3
inst : Group G
inst_1 : Fintype G
inst_2 : Monoid M
inst_3 : DecidableEq M
inst_4 : FunLike F G M
inst_5 : MonoidHomClass F G M
f : F
x y : G
⊢ card.{u_1} (α := G) {g : G | Eq.{u_2 + 1} (α := M) ((f : (a : G) → M) g : M) ((f : (a : G) → M) x : M)} =
    card.{u_1} (α := G) {g : G | Eq.{u_2 + 1} (α := M) ((f : (a : G) → M) g : M) ((f : (a : G) → M) y : M)}
have rcases : ∀ (y : G),
  card.{u_1} (α := G) {g : G | Eq.{u_2 + 1} (α := M) ((f : (a : G) → M) g : M) ((f : (a : G) → M) x : M)} =
    card.{u_1} (α := G)
      {g : G | Eq.{u_2 + 1} (α := M) ((f : (a : G) → M) g : M) ((f : (a : G) → M) ((fun (x_1 : G) ↦ x * x_1) y) : M)}
Tactic: rcases mul_left_surjective x y with ⟨y, rfl⟩
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
Goal:
G : Type u_1
M : Type u_2
F : Type u_3
inst : Group G
inst_1 : Fintype G
inst_2 : Monoid M
inst_3 : DecidableEq M
inst_4 : FunLike F G M
inst_5 : MonoidHomClass F G M
f : F
x y : G
| card.{u_1} (α := G) {g : G | Eq.{u_2 + 1} (α := M) ((f : (a : G) → M) g : M) ((f : (a : G) → M) x : M)}
have rw : card (α := G)
  (filter
    ((fun (g : G) ↦ Eq.{u_2 + 1} (α := M) ((f : (a : G) → M) g : M) ((f : (a : G) → M) x : M)) ∘
      (⇑(Equiv.toEmbedding (Equiv.mulRight y⁻¹)) : (a : G) → G))
    univ)
Tactic: rw [← map_univ_equiv (Equiv.mulRight y⁻¹), filter_map, card_map]
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
Goal:
G : Type u_1
M : Type u_2
F : Type u_3
inst : Group G
inst_1 : Fintype G
inst_2 : Monoid M
inst_3 : DecidableEq M
inst_4 : FunLike F G M
inst_5 : MonoidHomClass F G M
f : F
x y : G
⊢ card.{u_1} (α := G) {g : G | Eq.{u_2 + 1} (α := M) ((f : (a : G) → M) g : M) ((f : (a : G) → M) x : M)} =
    card.{u_1} (α := G)
      {g : G | Eq.{u_2 + 1} (α := M) ((f : (a : G) → M) g : M) ((f : (a : G) → M) ((fun (x_1 : G) ↦ x * x_1) y) : M)}
have conv_lhs : card (α := G)
    (filter
      ((fun (g : G) ↦ Eq.{u_2 + 1} (α := M) ((f : (a : G) → M) g : M) ((f : (a : G) → M) x : M)) ∘
        (⇑(Equiv.toEmbedding (Equiv.mulRight y⁻¹)) : (a : G) → G))
      univ) =
  card.{u_1} (α := G)
    {g : G | Eq.{u_2 + 1} (α := M) ((f : (a : G) → M) g : M) ((f : (a : G) → M) ((fun (x_1 : G) ↦ x * x_1) y) : M)}
Tactic: conv_lhs =>
    rw [← map_univ_equiv (Equiv.mulRight y⁻¹), filter_map, card_map]
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
Goal:
G : Type u_1
M : Type u_2
F : Type u_3
inst : Group G
inst_1 : Fintype G
inst_2 : Monoid M
inst_3 : DecidableEq M
inst_4 : FunLike F G M
inst_5 : MonoidHomClass F G M
f : F
x y : G
⊢ card (α := G)
      (filter
        ((fun (g : G) ↦ Eq.{u_2 + 1} (α := M) ((f : (a : G) → M) g : M) ((f : (a : G) → M) x : M)) ∘
          (⇑(Equiv.toEmbedding (Equiv.mulRight y⁻¹)) : (a : G) → G))
        univ) =
    card.{u_1} (α := G)
      {g : G | Eq.{u_2 + 1} (α := M) ((f : (a : G) → M) g : M) ((f : (a : G) → M) ((fun (x_1 : G) ↦ x * x_1) y) : M)}
have e_s : ∀ (g : G),
  ((fun (g : G) ↦ Eq.{u_2 + 1} (α := M) ((f : (a : G) → M) g : M) ((f : (a : G) → M) x : M)) ∘
        (⇑(Equiv.toEmbedding (Equiv.mulRight y⁻¹)) : (a : G) → G))
      g ↔
    Eq.{u_2 + 1} (α := M) ((f : (a : G) → M) g : M) ((f : (a : G) → M) ((fun (x_1 : G) ↦ x * x_1) y) : M)
Tactic: congr 2 with g
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
Goal:
G : Type u_1
M : Type u_2
F : Type u_3
inst : Group G
inst_1 : Fintype G
inst_2 : Monoid M
inst_3 : DecidableEq M
inst_4 : FunLike F G M
inst_5 : MonoidHomClass F G M
f : F
x y g : G
⊢ ((fun (g : G) ↦ Eq.{u_2 + 1} (α := M) ((f : (a : G) → M) g : M) ((f : (a : G) → M) x : M)) ∘
        (⇑(Equiv.toEmbedding (Equiv.mulRight y⁻¹)) : (a : G) → G))
      g ↔
    Eq.{u_2 + 1} (α := M) ((f : (a : G) → M) g : M) ((f : (a : G) → M) ((fun (x_1 : G) ↦ x * x_1) y) : M)
have e_s : HMul.hMul (α := M) (β := M) ((f : (a : G) → M) g : M) ((f : (a : G) → M) y⁻¹ : M) = (f : (a : G) → M) x ↔
  (f : (a : G) → M) g = HMul.hMul (α := M) (β := M) ((f : (a : G) → M) x : M) ((f : (a : G) → M) y : M)
Tactic: simp only [Function.comp, Equiv.toEmbedding_apply, Equiv.coe_mulRight, map_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
Goal:
G : Type u_1
M : Type u_2
F : Type u_3
inst : Group G
inst_1 : Fintype G
inst_2 : Monoid M
inst_3 : DecidableEq M
inst_4 : FunLike F G M
inst_5 : MonoidHomClass F G M
f : F
x y g : G
f' : G →* M := (↑f : G →* M)
⊢ HMul.hMul (α := M) (β := M) ((f : (a : G) → M) g : M) ((f : (a : G) → M) y⁻¹ : M) = (f : (a : G) → M) x ↔
    (f : (a : G) → M) g = HMul.hMul (α := M) (β := M) ((f : (a : G) → M) x : M) ((f : (a : G) → M) y : M)
have e_s : HMul.hMul (α := M) (β := M) ((f' : (a : G) → M) g : M) ((f' : (a : G) → M) y⁻¹ : M) = (f' : (a : G) → M) x ↔
  (f' : (a : G) → M) g = HMul.hMul (α := M) (β := M) ((f' : (a : G) → M) x : M) ((f' : (a : G) → M) y : M)
Tactic: change f' g * f' y⁻¹ = f' x ↔ f' g = f' x * f' y
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
Goal:
G : Type u_1
M : Type u_2
F : Type u_3
inst : Group G
inst_1 : Fintype G
inst_2 : Monoid M
inst_3 : DecidableEq M
inst_4 : FunLike F G M
inst_5 : MonoidHomClass F G M
f : F
x y g : G
f' : G →* M := (↑f : G →* M)
⊢ HMul.hMul (α := M) (β := M) ((f' : (a : G) → M) g : M) ((f' : (a : G) → M) y⁻¹ : M) = (f' : (a : G) → M) x ↔
    (f' : (a : G) → M) g = HMul.hMul (α := M) (β := M) ((f' : (a : G) → M) x : M) ((f' : (a : G) → M) y : M)
have e_s : HMul.hMul (α := M) (β := M) ((f' : (a : G) → M) g : M) ((↑((f'.toHomUnits : (a : G) → Mˣ) y⁻¹) : M) : M) =
    (f' : (a : G) → M) x ↔
  (f' : (a : G) → M) g = HMul.hMul (α := M) (β := M) ((f' : (a : G) → M) x : M) ((f' : (a : G) → M) y : M)
Tactic: rw [← f'.coe_toHomUnits y⁻¹, map_inv, Units.mul_inv_eq_iff_eq_mul, f'.coe_toHomUnits]
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
Goal:
G : Type u_1
M : Type u_2
F : Type u_3
inst : Group G
inst_1 : Fintype G
inst_2 : Monoid M
inst_3 : DecidableEq M
inst_4 : FunLike F G M
inst_5 : MonoidHomClass F G M
f : F
x y g : G
f' : G →* M := (↑f : G →* M)
e_s :
  HMul.hMul (α := M) (β := M) ((f' : (a : G) → M) g : M) ((↑((f'.toHomUnits : (a : G) → Mˣ) y⁻¹) : M) : M) =
      (f' : (a : G) → M) x ↔
    (f' : (a : G) → M) g = HMul.hMul (α := M) (β := M) ((f' : (a : G) → M) x : M) ((f' : (a : G) → M) y : M)
⊢ HMul.hMul (α := M) (β := M) ((f' : (a : G) → M) g : M) ((f' : (a : G) → M) y⁻¹ : M) = (f' : (a : G) → M) x ↔
    (f' : (a : G) → M) g = HMul.hMul (α := M) (β := M) ((f' : (a : G) → M) x : M) ((f' : (a : G) → M) y : M)
have e_s₁ : HMul.hMul (α := M) (β := M) ((f' : (a : G) → M) g : M) ((↑((f'.toHomUnits : (a : G) → Mˣ) y)⁻¹ : M) : M) =
    (f' : (a : G) → M) x ↔
  (f' : (a : G) → M) g = HMul.hMul (α := M) (β := M) ((f' : (a : G) → M) x : M) ((f' : (a : G) → M) y : M)
Tactic: rw [← f'.coe_toHomUnits y⁻¹, map_inv, Units.mul_inv_eq_iff_eq_mul, f'.coe_toHomUnits]
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
Goal:
G : Type u_1
M : Type u_2
F : Type u_3
inst : Group G
inst_1 : Fintype G
inst_2 : Monoid M
inst_3 : DecidableEq M
inst_4 : FunLike F G M
inst_5 : MonoidHomClass F G M
f : F
x y g : G
f' : G →* M := (↑f : G →* M)
e_s :
  HMul.hMul (α := M) (β := M) ((f' : (a : G) → M) g : M) ((↑((f'.toHomUnits : (a : G) → Mˣ) y⁻¹) : M) : M) =
      (f' : (a : G) → M) x ↔
    (f' : (a : G) → M) g = HMul.hMul (α := M) (β := M) ((f' : (a : G) → M) x : M) ((f' : (a : G) → M) y : M)
e_s₁ :
  HMul.hMul (α := M) (β := M) ((f' : (a : G) → M) g : M) ((↑((f'.toHomUnits : (a : G) → Mˣ) y)⁻¹ : M) : M) =
      (f' : (a : G) → M) x ↔
    (f' : (a : G) → M) g = HMul.hMul (α := M) (β := M) ((f' : (a : G) → M) x : M) ((f' : (a : G) → M) y : M)
⊢ HMul.hMul (α := M) (β := M) ((f' : (a : G) → M) g : M) ((f' : (a : G) → M) y⁻¹ : M) = (f' : (a : G) → M) x ↔
    (f' : (a : G) → M) g = HMul.hMul (α := M) (β := M) ((f' : (a : G) → M) x : M) ((f' : (a : G) → M) y : M)
have e_s₂ : (f' : (a : G) → M) g =
    HMul.hMul (α := M) (β := M) ((f' : (a : G) → M) x : M) ((↑((f'.toHomUnits : (a : G) → Mˣ) y) : M) : M) ↔
  (f' : (a : G) → M) g = HMul.hMul (α := M) (β := M) ((f' : (a : G) → M) x : M) ((f' : (a : G) → M) y : M)
Tactic: rw [← f'.coe_toHomUnits y⁻¹, map_inv, Units.mul_inv_eq_iff_eq_mul, f'.coe_toHomUnits]
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
Goal:
G : Type u_1
M : Type u_2
F : Type u_3
inst : Group G
inst_1 : Fintype G
inst_2 : Monoid M
inst_3 : DecidableEq M
inst_4 : FunLike F G M
inst_5 : MonoidHomClass F G M
f : F
x y g : G
f' : G →* M := (↑f : G →* M)
e_s :
  HMul.hMul (α := M) (β := M) ((f' : (a : G) → M) g : M) ((↑((f'.toHomUnits : (a : G) → Mˣ) y⁻¹) : M) : M) =
      (f' : (a : G) → M) x ↔
    (f' : (a : G) → M) g = HMul.hMul (α := M) (β := M) ((f' : (a : G) → M) x : M) ((f' : (a : G) → M) y : M)
e_s₁ :
  HMul.hMul (α := M) (β := M) ((f' : (a : G) → M) g : M) ((↑((f'.toHomUnits : (a : G) → Mˣ) y)⁻¹ : M) : M) =
      (f' : (a : G) → M) x ↔
    (f' : (a : G) → M) g = HMul.hMul (α := M) (β := M) ((f' : (a : G) → M) x : M) ((f' : (a : G) → M) y : M)
e_s₂ :
  (f' : (a : G) → M) g =
      HMul.hMul (α := M) (β := M) ((f' : (a : G) → M) x : M) ((↑((f'.toHomUnits : (a : G) → Mˣ) y) : M) : M) ↔
    (f' : (a : G) → M) g = HMul.hMul (α := M) (β := M) ((f' : (a : G) → M) x : M) ((f' : (a : G) → M) y : M)
⊢ HMul.hMul (α := M) (β := M) ((f' : (a : G) → M) g : M) ((f' : (a : G) → M) y⁻¹ : M) = (f' : (a : G) → M) x ↔
    (f' : (a : G) → M) g = HMul.hMul (α := M) (β := M) ((f' : (a : G) → M) x : M) ((f' : (a : G) → M) y : M)
have e_s₃ : (f' : (a : G) → M) g = HMul.hMul (α := M) (β := M) ((f' : (a : G) → M) x : M) ((f' : (a : G) → M) y : M) ↔
  (f' : (a : G) → M) g = HMul.hMul (α := M) (β := M) ((f' : (a : G) → M) x : M) ((f' : (a : G) → M) y : M)
Tactic: rw [← f'.coe_toHomUnits y⁻¹, map_inv, Units.mul_inv_eq_iff_eq_mul, f'.coe_toHomUnits]
-- Lean 4 proof step from Mathlib.GroupTheory.IndexNSmul (goal)
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : Module.Finite ℤ M
inst_2 : IsTorsionFree ℤ M
A : AddSubgroup M
inst_3 : A.FiniteIndex
⊢ finrank.{0, u_1} ℤ ↥A = finrank ℤ M
have refine : finrank ℤ M ≤ finrank.{0, u_1} ℤ ↥A
Tactic: refine le_antisymm A.toIntSubmodule.finrank_le ?_
-- Lean 4 proof step from Mathlib.GroupTheory.IndexNSmul (hypothesis)
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : Module.Finite ℤ M
inst_2 : IsTorsionFree ℤ M
A : AddSubgroup M
inst_3 : A.FiniteIndex
⊢ finrank ℤ M ≤ finrank.{0, u_1} ℤ ↥A
have this : finrank.{0, u_1} ℤ ↥(LinearMap.range (DistribSMul.toLinearMap ℤ M A.index)) = finrank ℤ M
Tactic: have : finrank ℤ (DistribSMul.toLinearMap ℤ M A.index).range = finrank ℤ M :=
    (DistribSMul.toLinearMap ..).finrank_range_of_inj <|
      distribSMulToLinearMap_injective_of_isTorsionFree FiniteIndex.index_ne_zero
-- Lean 4 proof step from Mathlib.GroupTheory.IndexNSmul (goal)
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : Module.Finite ℤ M
inst_2 : IsTorsionFree ℤ M
A : AddSubgroup M
inst_3 : A.FiniteIndex
this : finrank.{0, u_1} ℤ ↥(LinearMap.range (DistribSMul.toLinearMap ℤ M A.index)) = finrank ℤ M
⊢ finrank ℤ M ≤ finrank.{0, u_1} ℤ ↥A
have rw : finrank.{0, u_1} ℤ ↥(LinearMap.range (DistribSMul.toLinearMap ℤ M A.index)) ≤ finrank.{0, u_1} ℤ ↥A
Tactic: rw [← this]
-- Lean 4 proof step from Mathlib.GroupTheory.IndexNSmul (goal)
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : Module.Finite ℤ M
inst_2 : IsTorsionFree ℤ M
A : AddSubgroup M
inst_3 : A.FiniteIndex
this : finrank.{0, u_1} ℤ ↥(LinearMap.range (DistribSMul.toLinearMap ℤ M A.index)) = finrank ℤ M
⊢ finrank.{0, u_1} ℤ ↥(LinearMap.range (DistribSMul.toLinearMap ℤ M A.index)) ≤ finrank.{0, u_1} ℤ ↥A
have refine : ∀ (m : M)
  (hm :
    Membership.mem (γ := AddSubgroup M)
      ((OrderIso.symm toIntSubmodule : (a : Submodule ℤ M) → AddSubgroup M)
          (LinearMap.range (DistribSMul.toLinearMap ℤ M A.index)) :
        AddSubgroup M)
      m),
  m ∈ A
Tactic: refine Submodule.finrank_mono <| (OrderIso.symm_apply_le toIntSubmodule).mp fun m hm ↦ ?_
-- Lean 4 proof step from Mathlib.GroupTheory.IndexNSmul (goal)
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : Module.Finite ℤ M
inst_2 : IsTorsionFree ℤ M
A : AddSubgroup M
inst_3 : A.FiniteIndex
this : finrank.{0, u_1} ℤ ↥(LinearMap.range (DistribSMul.toLinearMap ℤ M A.index)) = finrank ℤ M
m : M
hm :
  Membership.mem (γ := AddSubgroup M)
    ((OrderIso.symm toIntSubmodule : (a : Submodule ℤ M) → AddSubgroup M)
        (LinearMap.range (DistribSMul.toLinearMap ℤ M A.index)) :
      AddSubgroup M)
    m
⊢ m ∈ A
have obtain : ∀ (x : M)
  (hm :
    Membership.mem (γ := AddSubgroup M)
      ((OrderIso.symm toIntSubmodule : (a : Submodule ℤ M) → AddSubgroup M)
          (LinearMap.range (DistribSMul.toLinearMap ℤ M A.index)) :
        AddSubgroup M)
      (A.index • x)),
  A.index • x ∈ A
Tactic: obtain ⟨x, rfl⟩ : ∃ x, A.index • x = m := by simpa using hm
Cleared hypotheses: m, hm
-- Lean 4 proof step from Mathlib.GroupTheory.IndexNSmul (hypothesis)
Goal:
M : Type u_1
inst : AddCommGroup M
A B : AddSubgroup M
inst_1 : Module.Finite.{0, u_1} ℤ ↥B
inst_2 : IsTorsionFree.{0, u_1} ℤ ↥B
h : A ≤ B
inst_3 : A.IsFiniteRelIndex B
⊢ finrank.{0, u_1} ℤ ↥A = finrank.{0, u_1} ℤ ↥B
have this : (A.addSubgroupOf B).FiniteIndex
Tactic: have : (A.addSubgroupOf B).FiniteIndex := IsFiniteRelIndex.to_finiteIndex_addSubgroupOf
-- Lean 4 proof step from Mathlib.GroupTheory.IndexNSmul (goal)
Goal:
M : Type u_1
inst : AddCommGroup M
A B : AddSubgroup M
inst_1 : Module.Finite.{0, u_1} ℤ ↥B
inst_2 : IsTorsionFree.{0, u_1} ℤ ↥B
h : A ≤ B
inst_3 : A.IsFiniteRelIndex B
this : (A.addSubgroupOf B).FiniteIndex
⊢ finrank.{0, u_1} ℤ ↥A = finrank.{0, u_1} ℤ ↥B
have rw : finrank.{0, u_1} ℤ ↥A = finrank.{0, u_1} ℤ ↥(A.addSubgroupOf B)
Tactic: rw [← finrank_eq_of_finiteIndex (A.addSubgroupOf B)]
-- Lean 4 proof step from Mathlib.GroupTheory.IndexNormal (hypothesis)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
hH : H.index = 1
⊢ H.Normal
have hH₁ : H = ⊤
Tactic: rw [index_eq_one] at hH
Cleared hypotheses: hH
-- Lean 4 proof step from Mathlib.GroupTheory.IndexNormal (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
hH : H = ⊤
⊢ H.Normal
have rw : Normal.{u_1} (G := G) ⊤
Tactic: rw [hH]
-- Lean 4 proof step from Mathlib.GroupTheory.IndexNormal (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
hH : H.index = 2
x : G
hxH : x ∈ H
g : G
⊢ g * x * g⁻¹ ∈ H
have simp_rw : (g ∈ H ↔ x ∈ H) ↔ g⁻¹ ∈ H
Tactic: simp_rw [mul_mem_iff_of_index_two hH, hxH, iff_true, inv_mem_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.IndexNormal (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
hH : H.index = 2
x : G
hxH : x ∈ H
g : G
simp_rw : (g ∈ H ↔ x ∈ H) ↔ g⁻¹ ∈ H
⊢ g * x * g⁻¹ ∈ H
have simp_rw₁ : (g ∈ H ↔ True) ↔ g⁻¹ ∈ H
Tactic: simp_rw [mul_mem_iff_of_index_two hH, hxH, iff_true, inv_mem_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.IndexNormal (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
hH : H.index = 2
x : G
hxH : x ∈ H
g : G
simp_rw : (g ∈ H ↔ x ∈ H) ↔ g⁻¹ ∈ H
simp_rw₁ : (g ∈ H ↔ True) ↔ g⁻¹ ∈ H
⊢ g * x * g⁻¹ ∈ H
have simp_rw₂ : g ∈ H ↔ g⁻¹ ∈ H
Tactic: simp_rw [mul_mem_iff_of_index_two hH, hxH, iff_true, inv_mem_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.IndexNormal (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
hHp : H.index = (Nat.card G).minFac
⊢ H.Normal
have pos : ∀ (hG0 : Nat.card G = 0), H.Normal
Tactic: by_cases hG0 : Nat.card G = 0
-- Lean 4 proof step from Mathlib.GroupTheory.IndexNormal (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
hHp : H.index = (Nat.card G).minFac
pos : ∀ (hG0 : Nat.card G = 0), H.Normal
⊢ H.Normal
have neg : ∀ (hG0 : ¬Nat.card G = 0), H.Normal
Tactic: by_cases hG0 : Nat.card G = 0
-- Lean 4 proof step from Mathlib.GroupTheory.IndexNormal (hypothesis)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
hHp : H.index = (Nat.card G).minFac
hG0 : Nat.card G = 0
⊢ H.Normal
have hHp₁ : H.index = 2
Tactic: rw [hG0, minFac_zero] at hHp
Cleared hypotheses: hHp, hG0
-- Lean 4 proof step from Mathlib.GroupTheory.IndexNormal (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
hHp : H.index = (Nat.card G).minFac
hG0 : ¬Nat.card G = 0
⊢ H.Normal
have pos : ∀ (hG1 : Nat.card G = 1), H.Normal
Tactic: by_cases hG1 : Nat.card G = 1
-- Lean 4 proof step from Mathlib.GroupTheory.IndexNormal (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
hHp : H.index = (Nat.card G).minFac
hG0 : ¬Nat.card G = 0
pos : ∀ (hG1 : Nat.card G = 1), H.Normal
⊢ H.Normal
have neg : ∀ (hG1 : ¬Nat.card G = 1), H.Normal
Tactic: by_cases hG1 : Nat.card G = 1
-- Lean 4 proof step from Mathlib.GroupTheory.IndexNormal (hypothesis)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
hHp : H.index = (Nat.card G).minFac
hG0 : ¬Nat.card G = 0
hG1 : Nat.card G = 1
⊢ H.Normal
have hHp₁ : H.index = 1
Tactic: rw [hG1, minFac_one] at hHp
Cleared hypotheses: hHp, hG0, hG1
-- Lean 4 proof step from Mathlib.GroupTheory.IndexNormal (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
hHp : H.index = (Nat.card G).minFac
hG0 : ¬Nat.card G = 0
hG1 : ¬Nat.card G = 1
this : H.normalCore.relIndex H = 1
⊢ H.Normal
have h : H = H.normalCore
Tactic: convert! H.normalCore_normal
-- Lean 4 proof step from Mathlib.GroupTheory.IndexNormal (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
hHp : H.index = (Nat.card G).minFac
hG0 : ¬Nat.card G = 0
hG1 : ¬Nat.card G = 1
⊢ H.Normal
have neg : H.normalCore.relIndex H = 1
Tactic: suffices H.normalCore.relIndex H = 1 by
    convert! H.normalCore_normal
    exact le_antisymm (relIndex_eq_one.mp this) (normalCore_le H)
-- Lean 4 proof step from Mathlib.GroupTheory.IndexNormal (hypothesis)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
hHp : H.index = (Nat.card G).minFac
hG0 : ¬Nat.card G = 0
hG1 : ¬Nat.card G = 1
⊢ H.normalCore.relIndex H = 1
have this : Finite G
Tactic: have : Finite G := finite_of_card_ne_zero hG0
-- Lean 4 proof step from Mathlib.GroupTheory.IndexNormal (hypothesis)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
hHp : H.index = (Nat.card G).minFac
hG0 : ¬Nat.card G = 0
hG1 : ¬Nat.card G = 1
this : Finite G
⊢ H.normalCore.relIndex H = 1
have index_ne_zero : H.index ≠ 0
Tactic: have index_ne_zero : H.index ≠ 0 := index_ne_zero_of_finite
-- Lean 4 proof step from Mathlib.GroupTheory.IndexNormal (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
hHp : H.index = (Nat.card G).minFac
hG0 : ¬Nat.card G = 0
hG1 : ¬Nat.card G = 1
this : Finite G
index_ne_zero : H.index ≠ 0
⊢ H.normalCore.relIndex H = 1
have neg : H.normalCore.index = H.index
Tactic: rw [← mul_left_inj' index_ne_zero, one_mul, relIndex_mul_index H.normalCore_le]
-- Lean 4 proof step from Mathlib.GroupTheory.IndexNormal (hypothesis)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
hHp : H.index = (Nat.card G).minFac
hG0 : ¬Nat.card G = 0
hG1 : ¬Nat.card G = 1
this : Finite G
index_ne_zero : H.index ≠ 0
⊢ H.normalCore.index = H.index
have hp : Nat.Prime H.index
Tactic: have hp : Nat.Prime H.index := hHp ▸ minFac_prime hG1
-- Lean 4 proof step from Mathlib.GroupTheory.IndexNormal (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
hHp : H.index = (Nat.card G).minFac
hG0 : ¬Nat.card G = 0
hG1 : ¬Nat.card G = 1
this : Finite G
index_ne_zero : H.index ≠ 0
hp : Nat.Prime H.index
⊢ H.normalCore.index ∣ H.index !
have rw : Nat.card.{u_1} ↥(range (toPermHom G (G ⧸ H))) ∣ Nat.card.{u_1} (Equiv.Perm (G ⧸ H))
Tactic: rw [normalCore_eq_ker, index_ker, index_eq_card, ← Nat.card_perm]
-- Lean 4 proof step from Mathlib.GroupTheory.IndexNormal (hypothesis)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
hHp : H.index = (Nat.card G).minFac
hG0 : ¬Nat.card G = 0
hG1 : ¬Nat.card G = 1
this : Finite G
index_ne_zero : H.index ≠ 0
hp : Nat.Prime H.index
⊢ H.normalCore.index = H.index
have h : H.normalCore.index ∣ H.index !
Tactic: have h : H.normalCore.index ∣ H.index ! := by
    rw [normalCore_eq_ker, index_ker, index_eq_card, ← Nat.card_perm]
    exact card_subgroup_dvd_card (toPermHom G (G ⧸ H)).range
-- Lean 4 proof step from Mathlib.GroupTheory.IndexNormal (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
hHp : H.index = (Nat.card G).minFac
hG0 : ¬Nat.card G = 0
hG1 : ¬Nat.card G = 1
this : Finite G
index_ne_zero : H.index ≠ 0
hp : Nat.Prime H.index
h : H.normalCore.index ∣ H.index !
⊢ H.normalCore.index = H.index
have apply : H.normalCore.index ∣ H.index
Tactic: apply dvd_antisymm _ (index_dvd_of_le H.normalCore_le)
-- Lean 4 proof step from Mathlib.GroupTheory.IndexNormal (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
hHp : H.index = (Nat.card G).minFac
hG0 : ¬Nat.card G = 0
hG1 : ¬Nat.card G = 1
this : Finite G
index_ne_zero : H.index ≠ 0
hp : Nat.Prime H.index
h : H.normalCore.index ∣ H.index !
⊢ H.normalCore.index ∣ H.index
have rwa : H.normalCore.index.Coprime (H.index - 1)!
Tactic: rwa [← Coprime.dvd_mul_right, mul_factorial_pred hp.ne_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.IndexNormal (hypothesis)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
hHp : H.index = (Nat.card G).minFac
hG0 : ¬Nat.card G = 0
hG1 : ¬Nat.card G = 1
this : Finite G
index_ne_zero : H.index ≠ 0
hp : Nat.Prime H.index
h : H.normalCore.index ∣ H.index !
⊢ H.normalCore.index.Coprime (H.index - 1)!
have hr1 : H.normalCore.index ≠ 1
Tactic: have hr1 : H.normalCore.index ≠ 1 := fun hr1 ↦ hp.ne_one <|
    Nat.eq_one_of_dvd_one (hr1 ▸ H.normalCore.index_dvd_of_le H.normalCore_le)
-- Lean 4 proof step from Mathlib.GroupTheory.IndexNormal (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
hHp : H.index = (Nat.card G).minFac
hG0 : ¬Nat.card G = 0
hG1 : ¬Nat.card G = 1
this : Finite G
index_ne_zero : H.index ≠ 0
hp : Nat.Prime H.index
h : H.normalCore.index ∣ H.index !
hr1 : H.normalCore.index ≠ 1
⊢ H.normalCore.index.Coprime (H.index - 1)!
have rw : H.index - 1 < H.normalCore.index.minFac
Tactic: rw [Nat.coprime_factorial_iff hr1]
-- Lean 4 proof step from Mathlib.GroupTheory.IsPerfect (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
⊢ IsPerfect.{u_1} ↥H ↔ ⁅H, H⁆ = H
have rw : Eq.{u_1 + 1} (α := Subgroup ↥H) (_root_.commutator ↥H) ⊤ ↔ ⁅H, H⁆ = H
Tactic: rw [Group.isPerfect_def, ← map_subtype_inj,
    map_subtype_commutator, ← MonoidHom.range_eq_map, range_subtype]