awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
ι : Type u_3
inst_1 : Fintype ι
H : ι → Subgroup G
refine :
  ∀ (x y : (i : ι) → G),
    (QuotientGroup.leftRel (pi Set.univ H) : ((i : ι) → G) → ((i : ι) → G) → Prop) x y ↔
      (piSetoid : ((i : ι) → G) → ((i : ι) → G) → Prop) x y
⊢ Nat.card (((i : ι) → G) ⧸ pi (f := fun (i : ι) ↦ G) Set.univ H) = Nat.card ((a : ι) → G ⧸ H a)

Tactic:
refine Nat.card_congr
    ((Quotient.congrRight (fun x y ↦ ?_)).trans (Setoid.piQuotientEquiv _).symm)

Premises used: Setoid.piQuotientEquiv, Equiv.trans, Quotient.congrRight, Nat.card_congr, Equiv.symm
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
ι : Type u_3
inst_1 : Fintype ι
H : ι → Subgroup G
x y : (i : ι) → G
rw rw₁ : (piSetoid : ((i : ι) → G) → ((i : ι) → G) → Prop) x y ↔ (piSetoid : ((i : ι) → G) → ((i : ι) → G) → Prop) x y
⊢ (QuotientGroup.leftRel (pi Set.univ H) : ((i : ι) → G) → ((i : ι) → G) → Prop) x y ↔
    (piSetoid : ((i : ι) → G) → ((i : ι) → G) → Prop) x y

Tactic:
rw [QuotientGroup.leftRel_pi]

Premises used: QuotientGroup.leftRel_pi
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
⊢ AddSubgroup.index.{u_1} (G := Additive G) ((toAddSubgroup : (a : Subgroup G) → AddSubgroup (Additive G)) H) = H.index

Tactic:
rfl

Premises used: Set.Mem, Additive, MulOpposite, setOf, MulAction.orbitRel, MulAction.orbit, Set.preimage, Subgroup.index, AddOpposite.unop, MulOpposite.unop, rfl
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_3
inst : AddGroup G
H : AddSubgroup G
⊢ index.{u_3} (G := Multiplicative G) ((AddSubgroup.toSubgroup : (a : AddSubgroup G) → Subgroup (Multiplicative G)) H) =
    H.index

Tactic:
rfl

Premises used: AddAction.orbit, AddSubgroup.index, Set.Mem, setOf, AddOpposite, Multiplicative, Set.preimage, AddOpposite.unop, MulOpposite.unop, AddAction.orbitRel, rfl
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
⊢ AddSubgroup.relIndex.{u_1} (G := Additive G) ((toAddSubgroup : (a : Subgroup G) → AddSubgroup (Additive G)) H)
      ((toAddSubgroup : (a : Subgroup G) → AddSubgroup (Additive G)) K) =
    H.relIndex K

Tactic:
rfl

Premises used: Set.Mem, Additive, MulOpposite, setOf, MulAction.orbitRel, Subgroup.relIndex, MulAction.orbit, Set.preimage, Subgroup.index, MulOpposite.unop, rfl
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_3
inst : AddGroup G
H K : AddSubgroup G
⊢ relIndex.{u_3} (G := Multiplicative G)
      ((AddSubgroup.toSubgroup : (a : AddSubgroup G) → Subgroup (Multiplicative G)) H)
      ((AddSubgroup.toSubgroup : (a : AddSubgroup G) → Subgroup (Multiplicative G)) K) =
    H.relIndex K

Tactic:
rfl

Premises used: AddAction.orbit, AddSubgroup.index, Set.Mem, setOf, AddOpposite, Multiplicative, AddSubgroup.relIndex, Set.preimage, AddOpposite.unop, AddAction.orbitRel, rfl
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
inst_1 : H.IsFiniteRelIndex K
⊢ H.relIndex K ≠ 0

Tactic:
IsFiniteRelIndex.relIndex_ne_zero

Premises used: Subgroup.IsFiniteRelIndex.relIndex_ne_zero
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
⊢ H.IsFiniteRelIndex K ↔ H.relIndex K ≠ 0

Tactic:
⟨fun _ ↦ relIndex_ne_zero, IsFiniteRelIndex.mk⟩

Premises used: Subgroup.relIndex_ne_zero, Iff.intro, Subgroup.IsFiniteRelIndex.mk
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
⊢ H.FiniteIndex ↔ H.index ≠ 0

Tactic:
⟨fun h ↦ h.index_ne_zero, fun h ↦ ⟨h⟩⟩

Premises used: Subgroup.FiniteIndex.index_ne_zero, Iff.intro, Subgroup.FiniteIndex.mk
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
rw : H.relIndex K ≠ 0 ↔ (H.subgroupOf K).FiniteIndex
rw₁ : H.relIndex K ≠ 0 ↔ (H.subgroupOf K).index ≠ 0
rw₂ rw₃ : (H.subgroupOf K).index ≠ 0 ↔ (H.subgroupOf K).index ≠ 0
⊢ H.IsFiniteRelIndex K ↔ (H.subgroupOf K).FiniteIndex

Tactic:
rw [isFiniteRelIndex_iff_relIndex_ne_zero, finiteIndex_iff, relIndex]

Premises used: Subgroup.isFiniteRelIndex_iff_relIndex_ne_zero, Subgroup.relIndex, Subgroup.finiteIndex_iff
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
⊢ ¬H.FiniteIndex ↔ H.index = 0

Tactic:
simp [finiteIndex_iff]

Premises used: Subgroup.finiteIndex_iff
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
⊢ AddSubgroup.FiniteIndex.{u_1} (G := Additive G) ((toAddSubgroup : (a : Subgroup G) → AddSubgroup (Additive G)) H) ↔
    H.FiniteIndex

Tactic:
simp [finiteIndex_iff, AddSubgroup.finiteIndex_iff]

Premises used: AddSubgroup.finiteIndex_iff, Subgroup.finiteIndex_iff
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_3
inst : AddGroup G
H : AddSubgroup G
⊢ FiniteIndex.{u_3} (G := Multiplicative G)
      ((AddSubgroup.toSubgroup : (a : AddSubgroup G) → Subgroup (Multiplicative G)) H) ↔
    H.FiniteIndex

Tactic:
simp [finiteIndex_iff, AddSubgroup.finiteIndex_iff]

Premises used: AddSubgroup.finiteIndex_iff, Subgroup.finiteIndex_iff
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
rw : H.IsFiniteRelIndex ⊤ ↔ H.index ≠ 0
rw₁ : H.relIndex ⊤ ≠ 0 ↔ H.index ≠ 0
rw₂ rw₃ : H.index ≠ 0 ↔ H.index ≠ 0
⊢ H.IsFiniteRelIndex ⊤ ↔ H.FiniteIndex

Tactic:
rw [finiteIndex_iff, isFiniteRelIndex_iff_relIndex_ne_zero, relIndex_top_right]

Premises used: Subgroup.isFiniteRelIndex_iff_relIndex_ne_zero, Subgroup.finiteIndex_iff, Subgroup.relIndex_top_right
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H K L : Subgroup G
f : G →* G'
inst_2 : H.FiniteIndex
⊢ Finite.{u_1 + 1} (G ⧸ H)

Tactic:
fintypeQuotientOfFiniteIndex.finite

Premises used: Fintype.finite, Subgroup.fintypeQuotientOfFiniteIndex
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : Finite.{u_1 + 1} (G ⧸ H)
⊢ H.FiniteIndex

Tactic:
⟨index_ne_zero_of_finite⟩

Premises used: Subgroup.index_ne_zero_of_finite, Subgroup.FiniteIndex.mk
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
⊢ H.FiniteIndex ↔ Finite.{u_1 + 1} (G ⧸ H)

Tactic:
⟨fun _ ↦ inferInstance, fun _ ↦ finiteIndex_of_finite_quotient⟩

Premises used: inferInstance, Iff.intro, Subgroup.finiteIndex_of_finite_quotient
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H K L : Subgroup G
f : G →* G'
inst_2 : Finite G
⊢ H.FiniteIndex

Tactic:
finiteIndex_of_finite_quotient

Premises used: Subgroup.finiteIndex_of_finite_quotient
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H K L : Subgroup G
f : G →* G'
inst_2 : H.FiniteIndex
inst_3 : K.FiniteIndex
⊢ (H.prod K).FiniteIndex

Tactic:
simp_all [finiteIndex_iff]

Premises used: Subgroup.finiteIndex_iff
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
f : G →* G'
rw : Finite.{u_1 + 1} ↥f.ker ∧ f.ker.FiniteIndex ↔ Finite.{u_1 + 1} ↥f.ker ∧ Finite.{u_2 + 1} ↥f.range
rw₁ : Finite.{u_1 + 1} ↥f.ker ∧ f.ker.FiniteIndex ↔ Finite.{u_1 + 1} ↥f.ker ∧ Finite.{u_1 + 1} (G ⧸ f.ker)
rw₂ rw₃ :
  Finite.{u_1 + 1} ↥f.ker ∧ Finite.{u_1 + 1} (G ⧸ f.ker) ↔ Finite.{u_1 + 1} ↥f.ker ∧ Finite.{u_1 + 1} (G ⧸ f.ker)
⊢ Finite G ↔ Finite.{u_1 + 1} ↥f.ker ∧ Finite.{u_2 + 1} ↥f.range

Tactic:
rw [finite_iff_finite_and_finiteIndex f.ker, ← (QuotientGroup.quotientKerEquivRange f).finite_iff,
    finiteIndex_iff_finite_quotient]

Premises used: QuotientGroup.quotientKerEquivRange, Equiv.finite_iff, Subgroup.finite_iff_finite_and_finiteIndex, MulEquiv.toEquiv, MonoidHom.ker, Subgroup.finiteIndex_iff_finite_quotient
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H K L : Subgroup G
f : G →* G'
⊢ FiniteIndex.{u_1} (G := G) ⊤

Tactic:
⟨ne_of_eq_of_ne index_top one_ne_zero⟩

Premises used: ne_of_eq_of_ne, Subgroup.FiniteIndex.mk, Subgroup.index_top, one_ne_zero
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H K L : Subgroup G
f : G →* G'
inst_2 : H.FiniteIndex
inst_3 : K.FiniteIndex
⊢ (H ⊓ K).FiniteIndex

Tactic:
⟨index_inf_ne_zero FiniteIndex.index_ne_zero FiniteIndex.index_ne_zero⟩

Premises used: Subgroup.FiniteIndex.index_ne_zero, Subgroup.index_inf_ne_zero, Subgroup.FiniteIndex.mk
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
ι : Type u_3
inst_1 : Finite ι
f : ι → Subgroup G
hf : ∀ (i : ι), (f i).FiniteIndex
⊢ FiniteIndex.{u_1} (G := G) (⨅ (i : ι), f i)

Tactic:
⟨index_iInf_ne_zero fun i => (hf i).index_ne_zero⟩

Premises used: Subgroup.FiniteIndex.index_ne_zero, Subgroup.FiniteIndex.mk, Subgroup.index_iInf_ne_zero
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
ι : Type u_3
s : Finset ι
f : ι → Subgroup G
hs : ∀ i ∈ s, (f i).FiniteIndex
rw : FiniteIndex.{u_1} (G := G) (⨅ (x : Subtype (Membership.mem s)), f (↑x : ι))
⊢ FiniteIndex.{u_1} (G := G) (⨅ i ∈ s, f i)

Tactic:
rw [iInf_subtype']

Premises used: iInf_subtype'
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
ι : Type u_3
s : Finset ι
f : ι → Subgroup G
hs : ∀ i ∈ s, (f i).FiniteIndex
⊢ FiniteIndex.{u_1} (G := G) (⨅ (x : Subtype (Membership.mem s)), f (↑x : ι))

Tactic:
finiteIndex_iInf fun ⟨i, hi⟩ => hs i hi

Premises used: Subgroup.finiteIndex_iInf, Subgroup.FiniteIndex, _private.0.Subgroup.finiteIndex_iInf'.match_1, Subtype.val
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
ι : Type u_3
s : Finset ι
f : ι → Subgroup G
hs : ∀ i ∈ s, (f i).FiniteIndex
⊢ FiniteIndex.{u_1} (G := G) (⨅ (x : Subtype (Membership.mem s)), f (↑x : ι))

Tactic:
exact finiteIndex_iInf fun ⟨i, hi⟩ => hs i hi

Premises used: Subgroup.finiteIndex_iInf
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H_1 K_1 L : Subgroup G
f : G →* G'
H K : Subgroup G
inst_2 : H.FiniteIndex
⊢ (H.subgroupOf K).FiniteIndex

Tactic:
⟨fun h => H.index_ne_zero_of_finite <| H.index_eq_zero_of_relIndex_eq_zero h⟩

Premises used: Subgroup.index_ne_zero_of_finite, Subgroup.FiniteIndex.mk, Subgroup.index_eq_zero_of_relIndex_eq_zero
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
inst_1 : H.FiniteIndex
h : H ≤ K
⊢ K.FiniteIndex

Tactic:
⟨ne_zero_of_dvd_ne_zero FiniteIndex.index_ne_zero (index_dvd_of_le h)⟩

Premises used: Subgroup.FiniteIndex.index_ne_zero, Subgroup.FiniteIndex.mk, Subgroup.index_dvd_of_le, ne_zero_of_dvd_ne_zero
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H K L : Subgroup G
inst_1 : H.IsFiniteRelIndex L
h : H ≤ K
rw : (H.subgroupOf L).FiniteIndex → ∀ (h : H ≤ K), (K.subgroupOf L).FiniteIndex
⊢ K.IsFiniteRelIndex L

Tactic:
rw [isFiniteRelIndex_iff_finiteIndex] at *

Premises used: Subgroup.isFiniteRelIndex_iff_finiteIndex
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H K L : Subgroup G
inst_1 : (H.subgroupOf L).FiniteIndex
h : H ≤ K
⊢ (K.subgroupOf L).FiniteIndex

Tactic:
finiteIndex_of_le <| subgroupOf_mono L h

Premises used: Subgroup.subgroupOf_mono, Subgroup.finiteIndex_of_le
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H K L : Subgroup G
inst_1 : (H.subgroupOf L).FiniteIndex
h : H ≤ K
⊢ (K.subgroupOf L).FiniteIndex

Tactic:
exact finiteIndex_of_le <| subgroupOf_mono L h

Premises used: Subgroup.subgroupOf_mono, Subgroup.finiteIndex_of_le
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H K L : Subgroup G
h : K ≤ L
inst_1 : H.IsFiniteRelIndex L
rw : H.relIndex K ≠ 0
⊢ H.IsFiniteRelIndex K

Tactic:
rw [isFiniteRelIndex_iff_relIndex_ne_zero]

Premises used: Subgroup.isFiniteRelIndex_iff_relIndex_ne_zero
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H K L : Subgroup G
h : K ≤ L
inst_1 : H.IsFiniteRelIndex L
⊢ H.relIndex K ≠ 0

Tactic:
mt (relIndex_eq_zero_of_le_right h) relIndex_ne_zero

Premises used: mt, Subgroup.relIndex_ne_zero, Subgroup.relIndex_eq_zero_of_le_right
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H K L : Subgroup G
h : K ≤ L
inst_1 : H.IsFiniteRelIndex L
⊢ H.relIndex K ≠ 0

Tactic:
exact mt (relIndex_eq_zero_of_le_right h) relIndex_ne_zero

Premises used: mt, Subgroup.relIndex_ne_zero, Subgroup.relIndex_eq_zero_of_le_right
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
h : H.FiniteIndex
⊢ H.IsFiniteRelIndex ⊤

Tactic:
rw [← isFiniteRelIndex_top_iff] at h

Premises used: Subgroup.isFiniteRelIndex_top_iff
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
h : H.IsFiniteRelIndex ⊤
⊢ H.IsFiniteRelIndex K

Tactic:
isFiniteRelIndex_of_le_right _ le_top

Premises used: le_top, Subgroup.isFiniteRelIndex_of_le_right
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
h : H.IsFiniteRelIndex ⊤
⊢ H.IsFiniteRelIndex K

Tactic:
exact isFiniteRelIndex_of_le_right _ le_top

Premises used: le_top, Subgroup.isFiniteRelIndex_of_le_right
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
h : H ≤ K
inst_1 : H.FiniteIndex
⊢ K.index ≤ H.index

Tactic:
Nat.le_of_dvd (Nat.zero_lt_of_ne_zero FiniteIndex.index_ne_zero) (index_dvd_of_le h)

Premises used: Subgroup.FiniteIndex.index_ne_zero, Nat.zero_lt_of_ne_zero, Subgroup.index_dvd_of_le, Nat.le_of_dvd
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
h : H < K
inst_1 : H.FiniteIndex
⊢ K.index ≠ 0

Tactic:
have h0 : K.index ≠ 0 := (finiteIndex_of_le h.le).index_ne_zero
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
h : H < K
inst_1 : H.FiniteIndex
h0 : K.index ≠ 0
apply : K.index ≠ H.index
⊢ K.index < H.index

Tactic:
apply lt_of_le_of_ne (index_antitone h.le)

Premises used: LT.lt.le, Subgroup.index_antitone, lt_of_le_of_ne
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
h : H < K
inst_1 : H.FiniteIndex
h0 : K.index ≠ 0
rw : ¬K ≤ H
⊢ K.index ≠ H.index

Tactic:
rw [← relIndex_mul_index h.le, Ne, eq_comm, mul_eq_right₀ h0, relIndex_eq_one]

Premises used: Subgroup.relIndex_mul_index, LT.lt.le, Ne, mul_eq_right₀, eq_comm, Subgroup.relIndex_eq_one
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
h : H < K
inst_1 : H.FiniteIndex
h0 : K.index ≠ 0
⊢ ¬K ≤ H

Tactic:
h.not_ge

Premises used: LT.lt.not_ge
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
h : H < K
inst_1 : H.FiniteIndex
h0 : K.index ≠ 0
⊢ ¬K ≤ H

Tactic:
exact h.not_ge

Premises used: LT.lt.not_ge
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
G'_1 : Type u_2
inst : Group G
inst_1 : Group G'_1
H K L : Subgroup G
f_1 : G →* G'_1
G' : Type u_3
inst_2 : Group G'
f : G →* G'
inst_3 : Finite.{u_3 + 1} ↥f.range
⊢ f.ker.FiniteIndex

Tactic:
@finiteIndex_of_finite_quotient G _ f.ker
    (Finite.of_equiv f.range (QuotientGroup.quotientKerEquivRange f).symm)

Premises used: Subgroup.finiteIndex_of_finite_quotient
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H K L : Subgroup G
f : G →* G'
inst_2 : H.FiniteIndex
rw : FiniteIndex (MonoidHom.ker (M := Equiv.Perm (G ⧸ H)) (MulAction.toPermHom G (G ⧸ H)))
⊢ H.normalCore.FiniteIndex

Tactic:
rw [normalCore_eq_ker]

Premises used: Subgroup.normalCore_eq_ker
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H K L : Subgroup G
f : G →* G'
inst_2 : H.FiniteIndex
⊢ FiniteIndex (MonoidHom.ker (M := Equiv.Perm (G ⧸ H)) (MulAction.toPermHom G (G ⧸ H)))

Tactic:
infer_instance
-- Module: Mathlib.GroupTheory.Index
Goal:
G_1 : Type u_1
G' : Type u_2
inst : Group G_1
inst_1 : Group G'
H_1 K L : Subgroup G_1
f : G_1 →* G'
G : Type u_3
inst_2 : AddGroup G
H : AddSubgroup G
h : H.FiniteIndex
rw :
  ∀
    (h :
      FiniteIndex.{u_3} (G := Multiplicative G)
        ((AddSubgroup.toSubgroup : (a : AddSubgroup G) → Subgroup (Multiplicative G)) H)),
    FiniteIndex.{u_3} (G := Multiplicative G)
      ((AddSubgroup.toSubgroup : (a : AddSubgroup G) → Subgroup (Multiplicative G)) H.normalCore)
⊢ H.normalCore.FiniteIndex

Tactic:
rw [← AddSubgroup.finiteIndex_toSubgroup_iff] at h ⊢

Premises used: AddSubgroup.finiteIndex_toSubgroup_iff
-- Module: Mathlib.GroupTheory.Index
Goal:
G_1 : Type u_1
G' : Type u_2
inst : Group G_1
inst_1 : Group G'
H_1 K L : Subgroup G_1
f : G_1 →* G'
G : Type u_3
inst_2 : AddGroup G
H : AddSubgroup G
h :
  FiniteIndex.{u_3} (G := Multiplicative G)
    ((AddSubgroup.toSubgroup : (a : AddSubgroup G) → Subgroup (Multiplicative G)) H)
⊢ FiniteIndex.{u_3} (G := Multiplicative G)
    ((AddSubgroup.toSubgroup : (a : AddSubgroup G) → Subgroup (Multiplicative G)) H.normalCore)

Tactic:
H.toSubgroup.finiteIndex_normalCore

Premises used: Set.Mem, setOf, Multiplicative, AddSubgroup.toSubgroup, Set.preimage, Subgroup.normalCore, DFunLike.coe, Subgroup.finiteIndex_normalCore
-- Module: Mathlib.GroupTheory.Index
Goal:
G_1 : Type u_1
G' : Type u_2
inst : Group G_1
inst_1 : Group G'
H_1 K L : Subgroup G_1
f : G_1 →* G'
G : Type u_3
inst_2 : AddGroup G
H : AddSubgroup G
h :
  FiniteIndex.{u_3} (G := Multiplicative G)
    ((AddSubgroup.toSubgroup : (a : AddSubgroup G) → Subgroup (Multiplicative G)) H)
⊢ FiniteIndex.{u_3} (G := Multiplicative G)
    ((AddSubgroup.toSubgroup : (a : AddSubgroup G) → Subgroup (Multiplicative G)) H.normalCore)

Tactic:
exact H.toSubgroup.finiteIndex_normalCore

Premises used: AddSubgroup.toSubgroup, DFunLike.coe, Subgroup.finiteIndex_normalCore
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
f : G →* G
hf : f.ker.FiniteIndex
rw : f.range.index * f.ker.index = Nat.card.{u_1} ↥f.ker * f.ker.index
rw₁ : f.range.index * f.ker.index = Nat.card G
rw₂ : f.range.index * Nat.card.{u_1} ↥f.range = Nat.card G
rw₃ rw₄ : Nat.card G = Nat.card G
⊢ f.range.index = Nat.card.{u_1} ↥f.ker

Tactic:
rw [← mul_left_inj' hf.index_ne_zero, card_mul_index, index_ker, index_mul_card]

Premises used: Subgroup.index_ker, Subgroup.index_mul_card, Subgroup.FiniteIndex.index_ne_zero, mul_left_inj', Subgroup.card_mul_index
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
H : Type u_2
inst : Group H
h : H
inst_1 : Group G
inst_2 : MulDistribMulAction H G
J K : Subgroup G
a b : G
⊢ Eq (α := G)
      (((((MulDistribMulAction.toMonoidEnd H G : MonoidHom.{u_2, u_1} H (Monoid.End G)) : (a : H) → Monoid.End G) h :
              Monoid.End G) :
            (a : G) → G)
          a :
        G)
      (((((MulDistribMulAction.toMonoidEnd H G : MonoidHom.{u_2, u_1} H (Monoid.End G)) : (a : H) → Monoid.End G) h :
              Monoid.End G) :
            (a : G) → G)
          b :
        G) →
    a = b

Tactic:
simp
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
H : Type u_2
inst : Group H
h : H
inst_1 : Group G
inst_2 : MulDistribMulAction H G
J K : Subgroup G
rw :
  (h • J).relIndex
      (map (((MulDistribMulAction.toMonoidEnd H G : MonoidHom.{u_2, u_1} H (Monoid.End G)) : (a : H) → Monoid.End G) h)
        K) =
    J.relIndex K
rw₁ :
  relIndex
      (comap
        (((MulDistribMulAction.toMonoidEnd H G : MonoidHom.{u_2, u_1} H (Monoid.End G)) : (a : H) → Monoid.End G) h)
        (h • J))
      K =
    J.relIndex K
rw₂ :
  relIndex
      (comap (N := G)
        (((MulDistribMulAction.toMonoidEnd H G : MonoidHom.{u_2, u_1} H (Monoid.End G)) : (a : H) → Monoid.End G) h)
        (map
          (((MulDistribMulAction.toMonoidEnd H G : MonoidHom.{u_2, u_1} H (Monoid.End G)) : (a : H) → Monoid.End G) h)
          J))
      K =
    J.relIndex K
rw₃ rw₄ : J.relIndex K = J.relIndex K
⊢ (h • J).relIndex (h • K) = J.relIndex K

Tactic:
rw [pointwise_smul_def K, ← relIndex_comap, pointwise_smul_def,
    comap_map_eq_self_of_injective (by intro a b; simp)]

Premises used: Subgroup.pointwise_smul_def, Subgroup.comap_map_eq_self_of_injective, Subgroup.relIndex_comap
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
H : Type u_2
inst : Group H
h : H
inst_1 : AddGroup G
inst_2 : DistribMulAction H G
J K : AddSubgroup G
a b : G
⊢ Eq (α := G)
      (((((DistribMulAction.toAddMonoidEnd H G : MonoidHom.{u_2, u_1} H (AddMonoid.End G)) : (a : H) → AddMonoid.End G)
                h :
              AddMonoid.End G) :
            (a : G) → G)
          a :
        G)
      (((((DistribMulAction.toAddMonoidEnd H G : MonoidHom.{u_2, u_1} H (AddMonoid.End G)) : (a : H) → AddMonoid.End G)
                h :
              AddMonoid.End G) :
            (a : G) → G)
          b :
        G) →
    a = b

Tactic:
simp
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
H : Type u_2
inst : Group H
h : H
inst_1 : AddGroup G
inst_2 : DistribMulAction H G
J K : AddSubgroup G
rw :
  (h • J).relIndex
      (map
        (((DistribMulAction.toAddMonoidEnd H G : MonoidHom.{u_2, u_1} H (AddMonoid.End G)) : (a : H) → AddMonoid.End G)
          h)
        K) =
    J.relIndex K
rw₁ :
  relIndex
      (comap
        (((DistribMulAction.toAddMonoidEnd H G : MonoidHom.{u_2, u_1} H (AddMonoid.End G)) : (a : H) → AddMonoid.End G)
          h)
        (h • J))
      K =
    J.relIndex K
rw₂ :
  relIndex
      (comap (N := G)
        (((DistribMulAction.toAddMonoidEnd H G : MonoidHom.{u_2, u_1} H (AddMonoid.End G)) : (a : H) → AddMonoid.End G)
          h)
        (map
          (((DistribMulAction.toAddMonoidEnd H G : MonoidHom.{u_2, u_1} H (AddMonoid.End G)) :
              (a : H) → AddMonoid.End G)
            h)
          J))
      K =
    J.relIndex K
rw₃ rw₄ : J.relIndex K = J.relIndex K
⊢ (h • J).relIndex (h • K) = J.relIndex K

Tactic:
rw [pointwise_smul_def K, ← relIndex_comap, pointwise_smul_def,
    comap_map_eq_self_of_injective (by intro a b; simp)]

Premises used: AddSubgroup.relIndex_comap, AddSubgroup.pointwise_smul_def, AddSubgroup.comap_map_eq_self_of_injective
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
x : X
⊢ Subgroup.index (stabilizer G x) = (orbit G x).ncard

Tactic:
(Nat.card_congr (MulAction.orbitEquivQuotientStabilizer G x)).symm.trans
    (Nat.card_coe_set_eq (orbit G x))

Premises used: MulAction.orbitEquivQuotientStabilizer, Nat.card_coe_set_eq, MulAction.orbit, Nat.card_congr, Subgroup.index, Eq.symm, Eq.trans
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
x : X
inst_2 : IsPretransitive G X
rw : (orbit G x).ncard = Nat.card X
rw₁ : Set.ncard.{u_2} (α := X) Set.univ = Nat.card X
rw₂ rw₃ : Nat.card X = Nat.card X
⊢ Subgroup.index (stabilizer G x) = Nat.card X

Tactic:
rw [index_stabilizer, orbit_eq_univ, Set.ncard_univ]

Premises used: MulAction.index_stabilizer, MulAction.orbit_eq_univ, 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
⊢ Function.Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := M) (⇑f : (a : G) → M)

Tactic:
range_eq_top.1 <| SetLike.ext' <| Set.eq_of_subset_of_ncard_le (Set.subset_univ _) ?_

Premises used: Set.subset_univ, SetLike.ext', MonoidHom.range_eq_top, Iff.mp, Set.eq_of_subset_of_ncard_le
-- 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
refine : (↑⊤ : Set M).ncard ≤ (↑f.range : Set M).ncard
⊢ Function.Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := M) (⇑f : (a : G) → M)

Tactic:
refine range_eq_top.1 <| SetLike.ext' <| Set.eq_of_subset_of_ncard_le (Set.subset_univ _) ?_

Premises used: Set.subset_univ, SetLike.ext', MonoidHom.range_eq_top, Iff.mp, Set.eq_of_subset_of_ncard_le