awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Index
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
rw : Nat.card M ≤ Nat.card.{u_1} (G ⧸ f.ker)
⊢ (↑⊤ : Set M).ncard ≤ (↑f.range : Set M).ncard

Tactic:
rw [Subgroup.coe_top, Set.ncard_univ, ← Nat.card_coe_set_eq, SetLike.coe_sort_coe,
    ← Nat.card_congr (QuotientGroup.quotientKerEquivRange f).toEquiv]

Premises used: QuotientGroup.quotientKerEquivRange, SetLike.coe_sort_coe, Subgroup.coe_top, MulEquiv.toEquiv, Nat.card_coe_set_eq, Nat.card_congr, Set.ncard_univ
-- Module: Mathlib.GroupTheory.Index
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
⊢ Nat.card M ≤ Nat.card.{u_1} (G ⧸ f.ker)

Tactic:
Nat.le_of_mul_le_mul_left (f.ker.card_mul_index ▸ Nat.mul_le_of_le_div _ _ _ h) Nat.card_pos

Premises used: Nat.card_pos, Nat.le_of_mul_le_mul_left
-- Module: Mathlib.GroupTheory.Index
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
⊢ Nat.card M ≤ Nat.card.{u_1} (G ⧸ f.ker)

Tactic:
exact Nat.le_of_mul_le_mul_left (f.ker.card_mul_index ▸ Nat.mul_le_of_le_div _ _ _ h) Nat.card_pos

Premises used: Nat.card_pos, Nat.le_of_mul_le_mul_left
-- Module: Mathlib.GroupTheory.Index
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
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}
⊢ card.{u_1} (α := G) {g : G | (f : (a : G) → M) g = x} = card.{u_1} (α := G) {g : G | (f : (a : G) → M) g = y}

Tactic:
rcases hx with ⟨x, rfl⟩

Premises used: rfl
-- Module: Mathlib.GroupTheory.Index
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
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)}
⊢ 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 hy with ⟨y, rfl⟩

Premises used: rfl
-- Module: Mathlib.GroupTheory.Index
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
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)}
⊢ 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 mul_left_surjective x y with ⟨y, rfl⟩

Premises used: mul_left_surjective, rfl
-- Module: Mathlib.GroupTheory.Index
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
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)
| card.{u_1} (α := G) {g : G | Eq.{u_2 + 1} (α := M) ((f : (a : G) → M) g : M) ((f : (a : G) → M) x : M)}

Tactic:
rw [← map_univ_equiv (Equiv.mulRight y⁻¹), filter_map, card_map]

Premises used: Finset.card_map, Finset.map_univ_equiv, Inv.inv, Equiv.mulRight, Finset.filter_map
-- Module: Mathlib.GroupTheory.Index
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
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)}
⊢ 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:
conv_lhs =>
    rw [← map_univ_equiv (Equiv.mulRight y⁻¹), filter_map, card_map]

Premises used: Finset.card_map, Finset.map_univ_equiv, Inv.inv, Equiv.mulRight, Finset.filter_map
-- Module: Mathlib.GroupTheory.Index
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
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)
⊢ 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:
congr 2 with g
-- Module: Mathlib.GroupTheory.Index
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
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)
⊢ ((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:
simp only [Function.comp, Equiv.toEmbedding_apply, Equiv.coe_mulRight, map_mul]

Premises used: Function.comp, Equiv.toEmbedding_apply, map_mul, Equiv.coe_mulRight
-- Module: Mathlib.GroupTheory.Index
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' : (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)
⊢ 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

Premises used: Inv.inv, DFunLike.coe
-- Module: Mathlib.GroupTheory.Index
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)
e_s₃ 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)
⊢ 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:
rw [← f'.coe_toHomUnits y⁻¹, map_inv, Units.mul_inv_eq_iff_eq_mul, f'.coe_toHomUnits]

Premises used: map_inv, Units.mul_inv_eq_iff_eq_mul, MonoidHom.coe_toHomUnits, Inv.inv
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
A : Type u_2
inst : Group G
inst_1 : AddGroup A
inst_2 : DistribMulAction G A
a : G
S : AddSubgroup A
⊢ (a • S).index = S.index

Tactic:
index_map_of_bijective (MulAction.bijective _) _

Premises used: AddSubgroup.index_map_of_bijective
-- Module: Mathlib.GroupTheory.IndexNSmul
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : Free ℤ M
inst_2 : Module.Finite ℤ M
n : ℕ
⊢ index.{u_1} (G := M) (AddMonoidHom.range (G := M) (nsmulAddMonoidHom n)) =
    index (G := Fin (finrank ℤ M) → ℤ) (AddMonoidHom.range (nsmulAddMonoidHom n))

Tactic:
simpa [AddEquiv.map_range_nsmulAddMonoidHom]
        using (index_map_equiv (nsmulAddMonoidHom (α := M) n).range
                (Module.finBasis ℤ M).equivFun.toAddEquiv).symm

Premises used: AddEquiv.map_range_nsmulAddMonoidHom, AddSubgroup.index_map_equiv, AddMonoidHom.range, Module.finBasis, LinearEquiv.toAddEquiv, Int, nsmulAddMonoidHom, Eq.symm, Module.Basis.equivFun
-- Module: Mathlib.GroupTheory.IndexNSmul
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : Free ℤ M
inst_2 : Module.Finite ℤ M
n : ℕ
⊢ index (G := Fin (finrank ℤ M) → ℤ) (AddMonoidHom.range (nsmulAddMonoidHom n)) = n ^ finrank ℤ M

Tactic:
simp [index_eq_card, Nat.card_congr (addEquivPiModRangeNSMulAddMonoidHom _ n).toEquiv,
        Nat.card_fun, Int.range_nsmulAddMonoidHom,
        Nat.card_congr (Int.quotientZMultiplesNatEquivZMod n).toEquiv]

Premises used: Int.quotientZMultiplesNatEquivZMod, Int.range_nsmulAddMonoidHom, Nat.card_fun, Nat.card_congr, QuotientAddGroup.addEquivPiModRangeNSMulAddMonoidHom, AddSubgroup.index_eq_card, AddEquiv.toEquiv
-- Module: Mathlib.GroupTheory.IndexNSmul
Goal:
M : Type u_1
inst : AddCommGroup M
n : ℕ
S : AddSubgroup M
inst_1 : Free.{0, u_1} ℤ ↥((toIntSubmodule : (a : AddSubgroup M) → Submodule ℤ M) S : Submodule ℤ M)
inst_2 : Module.Finite.{0, u_1} ℤ ↥((toIntSubmodule : (a : AddSubgroup M) → Submodule ℤ M) S : Submodule ℤ M)
⊢ relIndex (map (nsmulAddMonoidHom n) S) S = n ^ finrank.{0, u_1} ℤ ↥S

Tactic:
simpa only [relIndex, addSubgroupOf_map_nsmulAddMonoidHom_eq_range]
    using index_range_nsmul S.toIntSubmodule n

Premises used: AddSubgroup.index_range_nsmul, Membership.mem, Subtype, AddSubgroup.relIndex, AddSubgroup.addSubgroupOf_map_nsmulAddMonoidHom_eq_range, AddSubgroup.toIntSubmodule, DFunLike.coe
-- Module: Mathlib.GroupTheory.IndexNSmul
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : IsTorsionFree ℤ M
n : ℕ
hn : n ≠ 0
x : M
hx : Membership.mem (γ := Submodule ℤ M) (LinearMap.ker (DistribSMul.toLinearMap ℤ M n)) x
⊢ x = 0

Tactic:
simp_all
-- Module: Mathlib.GroupTheory.IndexNSmul
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : IsTorsionFree ℤ M
n : ℕ
hn : n ≠ 0
x : M
hx : Membership.mem (γ := AddSubgroup M) (AddMonoidHom.ker (M := M) (nsmulAddMonoidHom n)) x
⊢ x = 0

Tactic:
simp_all
-- Module: Mathlib.GroupTheory.IndexNSmul
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

Tactic:
le_antisymm A.toIntSubmodule.finrank_le ?_

Premises used: le_antisymm, Submodule.finrank_le, AddSubgroup.toIntSubmodule, DFunLike.coe
-- Module: Mathlib.GroupTheory.IndexNSmul
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : Module.Finite ℤ M
inst_2 : IsTorsionFree ℤ M
A : AddSubgroup M
inst_3 : A.FiniteIndex
refine : finrank ℤ M ≤ finrank.{0, u_1} ℤ ↥A
⊢ finrank.{0, u_1} ℤ ↥A = finrank ℤ M

Tactic:
refine le_antisymm A.toIntSubmodule.finrank_le ?_

Premises used: le_antisymm, Submodule.finrank_le, AddSubgroup.toIntSubmodule, DFunLike.coe
-- Module: Mathlib.GroupTheory.IndexNSmul
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} ℤ ↥(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
-- Module: Mathlib.GroupTheory.IndexNSmul
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
rw : finrank.{0, u_1} ℤ ↥(LinearMap.range (DistribSMul.toLinearMap ℤ M A.index)) ≤ finrank.{0, u_1} ℤ ↥A
⊢ finrank ℤ M ≤ finrank.{0, u_1} ℤ ↥A

Tactic:
rw [← this]
-- Module: Mathlib.GroupTheory.IndexNSmul
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

Tactic:
Submodule.finrank_mono <| (OrderIso.symm_apply_le toIntSubmodule).mp fun m hm ↦ ?_

Premises used: Set.Mem, OrderIso.symm_apply_le, Submodule.finrank_mono, Iff.mp, AddSubgroup.toIntSubmodule
-- Module: Mathlib.GroupTheory.IndexNSmul
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
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
⊢ finrank.{0, u_1} ℤ ↥(LinearMap.range (DistribSMul.toLinearMap ℤ M A.index)) ≤ finrank.{0, u_1} ℤ ↥A

Tactic:
refine Submodule.finrank_mono <| (OrderIso.symm_apply_le toIntSubmodule).mp fun m hm ↦ ?_

Premises used: OrderIso.symm_apply_le, Submodule.finrank_mono, Iff.mp, AddSubgroup.toIntSubmodule
-- Module: Mathlib.GroupTheory.IndexNSmul
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
⊢ ∃ (x : M), A.index • x = m

Tactic:
simpa using hm
-- Module: Mathlib.GroupTheory.IndexNSmul
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
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
⊢ m ∈ A

Tactic:
obtain ⟨x, rfl⟩ : ∃ x, A.index • x = m := by simpa using hm

Premises used: AddSubgroup.index, rfl
-- Module: Mathlib.GroupTheory.IndexNSmul
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
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:
A.nsmul_index_mem x

Premises used: AddSubgroup.nsmul_index_mem
-- Module: Mathlib.GroupTheory.IndexNSmul
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
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:
exact A.nsmul_index_mem x

Premises used: AddSubgroup.nsmul_index_mem
-- Module: Mathlib.GroupTheory.IndexNSmul
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
⊢ (A.addSubgroupOf B).FiniteIndex

Tactic:
have : (A.addSubgroupOf B).FiniteIndex := IsFiniteRelIndex.to_finiteIndex_addSubgroupOf
-- Module: Mathlib.GroupTheory.IndexNSmul
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
rw : finrank.{0, u_1} ℤ ↥A = finrank.{0, u_1} ℤ ↥(A.addSubgroupOf B)
⊢ finrank.{0, u_1} ℤ ↥A = finrank.{0, u_1} ℤ ↥B

Tactic:
rw [← finrank_eq_of_finiteIndex (A.addSubgroupOf B)]

Premises used: AddSubgroup.finrank_eq_of_finiteIndex, AddSubgroup.addSubgroupOf
-- Module: Mathlib.GroupTheory.IndexNSmul
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} ℤ ↥(A.addSubgroupOf B)

Tactic:
(addSubgroupOfEquivOfLe h).symm.toIntLinearEquiv.finrank_eq

Premises used: AddEquiv.toIntLinearEquiv, Set.Mem, LinearEquiv.finrank_eq, AddSubgroup.addSubgroupOfEquivOfLe, AddEquiv.symm
-- Module: Mathlib.GroupTheory.IndexNSmul
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} ℤ ↥(A.addSubgroupOf B)

Tactic:
exact (addSubgroupOfEquivOfLe h).symm.toIntLinearEquiv.finrank_eq

Premises used: AddEquiv.toIntLinearEquiv, LinearEquiv.finrank_eq, AddSubgroup.addSubgroupOfEquivOfLe, AddEquiv.symm
-- Module: Mathlib.GroupTheory.IndexNormal
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
hH : H.index = 1
⊢ H = ⊤

Tactic:
rw [index_eq_one] at hH

Premises used: Subgroup.index_eq_one
-- Module: Mathlib.GroupTheory.IndexNormal
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
hH : H = ⊤
rw : Normal.{u_1} (G := G) ⊤
⊢ H.Normal

Tactic:
rw [hH]
-- Module: Mathlib.GroupTheory.IndexNormal
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
hH : H = ⊤
⊢ Normal.{u_1} (G := G) ⊤

Tactic:
infer_instance
-- Module: Mathlib.GroupTheory.IndexNormal
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
simp_rw₂ : g ∈ H ↔ g⁻¹ ∈ H
⊢ g * x * g⁻¹ ∈ H

Tactic:
simp_rw [mul_mem_iff_of_index_two hH, hxH, iff_true, inv_mem_iff]

Premises used: iff_true, inv_mem_iff, Subgroup.mul_mem_iff_of_index_two
-- Module: Mathlib.GroupTheory.IndexNormal
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
neg : ∀ (hG0 : ¬Nat.card G = 0), H.Normal
⊢ H.Normal

Tactic:
by_cases hG0 : Nat.card G = 0

Premises used: Nat.card
-- Module: Mathlib.GroupTheory.IndexNormal
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
hHp : H.index = (Nat.card G).minFac
hG0 : Nat.card G = 0
⊢ H.index = 2

Tactic:
rw [hG0, minFac_zero] at hHp

Premises used: Nat.minFac_zero
-- Module: Mathlib.GroupTheory.IndexNormal
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
hHp : H.index = (Nat.card G).minFac
hG0 : Nat.card G = 0
hHp₁ : H.index = 2
⊢ Nat.card G = 0

Tactic:
rw [hG0, minFac_zero] at hHp

Premises used: Nat.minFac_zero
-- Module: Mathlib.GroupTheory.IndexNormal
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
hHp : H.index = 2
hG0 : Nat.card G = 0
⊢ H.Normal

Tactic:
normal_of_index_eq_two hHp

Premises used: Subgroup.normal_of_index_eq_two
-- Module: Mathlib.GroupTheory.IndexNormal
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
hHp : H.index = 2
hG0 : Nat.card G = 0
⊢ H.Normal

Tactic:
exact normal_of_index_eq_two hHp

Premises used: Subgroup.normal_of_index_eq_two
-- Module: Mathlib.GroupTheory.IndexNormal
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
neg : ∀ (hG1 : ¬Nat.card G = 1), H.Normal
⊢ H.Normal

Tactic:
by_cases hG1 : Nat.card G = 1

Premises used: Nat.card
-- Module: Mathlib.GroupTheory.IndexNormal
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.index = 1

Tactic:
rw [hG1, minFac_one] at hHp

Premises used: Nat.minFac_one
-- Module: Mathlib.GroupTheory.IndexNormal
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
hHp₁ : H.index = 1
⊢ ¬Nat.card G = 0

Tactic:
rw [hG1, minFac_one] at hHp

Premises used: Nat.minFac_one
-- Module: Mathlib.GroupTheory.IndexNormal
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
hHp₁ : H.index = 1
hG0₁ : ¬Nat.card G = 0
⊢ Nat.card G = 1

Tactic:
rw [hG1, minFac_one] at hHp

Premises used: Nat.minFac_one
-- Module: Mathlib.GroupTheory.IndexNormal
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
hHp : H.index = 1
hG0 : ¬Nat.card G = 0
hG1 : Nat.card G = 1
⊢ H.Normal

Tactic:
normal_of_index_eq_one hHp

Premises used: Subgroup.normal_of_index_eq_one
-- Module: Mathlib.GroupTheory.IndexNormal
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
hHp : H.index = 1
hG0 : ¬Nat.card G = 0
hG1 : Nat.card G = 1
⊢ H.Normal

Tactic:
exact normal_of_index_eq_one hHp

Premises used: Subgroup.normal_of_index_eq_one
-- Module: Mathlib.GroupTheory.IndexNormal
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.normalCore.Normal

Tactic:
H.normalCore_normal

Premises used: Subgroup.normalCore_normal