awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
refine :
  ∀ (a b : G),
    b * a ∈ H ∨ b ∈ H ↔
      HMul.hMul (α := G) (β := G) ((Equiv.inv G : (a : G) → G) a : G) ((Equiv.inv G : (a : G) → G) b : G) ∈ H ∨
        Membership.mem (α := G) H ((Equiv.inv G : (a : G) → G) b : G)
⊢ ∀ (a : G),
    (∀ (b : G), b * a ∈ H ∨ b ∈ H) ↔ ∀ (b : G), HMul.hMul (α := G) ((Equiv.inv G : (a : G) → G) a : G) b ∈ H ∨ b ∈ H

Tactic:
refine fun a ↦ (Equiv.inv G).forall_congr fun b ↦ ?_

Premises used: Equiv.inv, Equiv.forall_congr
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
a b : G
⊢ b * a ∈ H ∨ b ∈ H ↔
    HMul.hMul (α := G) (β := G) ((Equiv.inv G : (a : G) → G) a : G) ((Equiv.inv G : (a : G) → G) b : G) ∈ H ∨
      Membership.mem (α := G) H ((Equiv.inv G : (a : G) → G) b : G)

Tactic:
simp only [Equiv.inv_apply, inv_mem_iff, ← mul_inv_rev]

Premises used: inv_mem_iff, Equiv.inv_apply, mul_inv_rev
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
⊢ H.relIndex K ∣ 2 ↔ ∃ a ∈ K, ∀ b ∈ K, b * a ∈ H ∨ b ∈ H

Tactic:
simp [Subgroup.relIndex, Subgroup.index_dvd_two_iff, mem_subgroupOf]

Premises used: Subgroup.index_dvd_two_iff, Subgroup.relIndex, Subgroup.mem_subgroupOf
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
⊢ H.relIndex K ∣ 2 ↔ ∃ a ∈ K, ∀ b ∈ K, a * b ∈ H ∨ b ∈ H

Tactic:
simp [Subgroup.relIndex, Subgroup.index_dvd_two_iff', mem_subgroupOf]

Premises used: Subgroup.index_dvd_two_iff', Subgroup.relIndex, Subgroup.mem_subgroupOf
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
h : (Nat.card.{u_1} ↥H).Coprime (Nat.card.{u_1} ↥K)
⊢ H ⊓ K = ⊥

Tactic:
card_eq_one.1 <| Nat.eq_one_of_dvd_coprimes h
    (card_dvd_of_le inf_le_left) (card_dvd_of_le inf_le_right)

Premises used: Subgroup.card_eq_one, Nat.eq_one_of_dvd_coprimes, inf_le_right, Subgroup.card_dvd_of_le, Iff.mp, inf_le_left
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
hH : Finite.{u_1 + 1} (G ⧸ H)
intro : ∀ (val : Fintype (G ⧸ H)), H.index ≠ 0
⊢ H.index ≠ 0

Tactic:
cases nonempty_fintype (G ⧸ H)

Premises used: HasQuotient.Quotient, nonempty_fintype
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
hH : Finite.{u_1 + 1} (G ⧸ H)
val : Fintype (G ⧸ H)
⊢ Nat.card.{u_1} (G ⧸ H) ≠ 0

Tactic:
Nat.card_pos.ne'

Premises used: Nat.card_pos, LT.lt.ne'
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
hH : Finite.{u_1 + 1} (G ⧸ H)
val : Fintype (G ⧸ H)
⊢ Nat.card.{u_1} (G ⧸ H) ≠ 0

Tactic:
exact Nat.card_pos.ne'

Premises used: Nat.card_pos, LT.lt.ne'
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
⊢ H.index = 0 ↔ Infinite.{u_1 + 1} (G ⧸ H)

Tactic:
simp [index_eq_card, Nat.card_eq_zero]

Premises used: Subgroup.index_eq_card, Nat.card_eq_zero
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
⊢ H.index ≠ 0 ↔ Finite.{u_1 + 1} (G ⧸ H)

Tactic:
simp [index_eq_zero_iff_infinite]

Premises used: Subgroup.index_eq_zero_iff_infinite
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : Finite.{u_1 + 1} (G ⧸ H)
hH : H ≠ ⊤
⊢ 1 < H.index

Tactic:
Nat.one_lt_iff_ne_zero_and_ne_one.mpr ⟨index_ne_zero_of_finite, mt index_eq_one.mp hH⟩

Premises used: Iff.mpr, Subgroup.index_ne_zero_of_finite, mt, And.intro, Nat.one_lt_iff_ne_zero_and_ne_one, Iff.mp, Subgroup.index_eq_one
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
X : Type u_3
inst_1 : MulAction G X
inst_2 : Finite.{u_3 + 1} (MulAction.orbitRel.Quotient G X)
hi : H.index ≠ 0
have : ∀ (this : Fintype (G ⧸ H)), Finite.{u_3 + 1} (MulAction.orbitRel.Quotient.{u_1, u_3} (↥H) X)
⊢ Finite.{u_3 + 1} (MulAction.orbitRel.Quotient.{u_1, u_3} (↥H) X)

Tactic:
have := fintypeOfIndexNeZero hi
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
X : Type u_3
inst_1 : MulAction G X
inst_2 : Finite.{u_3 + 1} (MulAction.orbitRel.Quotient G X)
hi : H.index ≠ 0
this : Fintype (G ⧸ H)
⊢ Finite.{u_3 + 1} (MulAction.orbitRel.Quotient.{u_1, u_3} (↥H) X)

Tactic:
MulAction.finite_quotient_of_finite_quotient_of_finite_quotient

Premises used: MulAction.finite_quotient_of_finite_quotient_of_finite_quotient
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
X : Type u_3
inst_1 : MulAction G X
inst_2 : Finite.{u_3 + 1} (MulAction.orbitRel.Quotient G X)
hi : H.index ≠ 0
this : Fintype (G ⧸ H)
⊢ Finite.{u_3 + 1} (MulAction.orbitRel.Quotient.{u_1, u_3} (↥H) X)

Tactic:
exact MulAction.finite_quotient_of_finite_quotient_of_finite_quotient

Premises used: MulAction.finite_quotient_of_finite_quotient_of_finite_quotient
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
X : Type u_3
inst_1 : MulAction G X
inst_2 : MulAction.IsPretransitive G X
hi : H.index ≠ 0
⊢ Subsingleton.{u_3 + 1} (MulAction.orbitRel.Quotient G X)

Tactic:
have := (MulAction.pretransitive_iff_subsingleton_quotient G X).1 inferInstance
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
X : Type u_3
inst_1 : MulAction G X
inst_2 : MulAction.IsPretransitive G X
hi : H.index ≠ 0
this : Subsingleton.{u_3 + 1} (MulAction.orbitRel.Quotient G X)
⊢ Finite.{u_3 + 1} (MulAction.orbitRel.Quotient.{u_1, u_3} (↥H) X)

Tactic:
finite_quotient_of_finite_quotient_of_index_ne_zero hi

Premises used: Subgroup.finite_quotient_of_finite_quotient_of_index_ne_zero
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
X : Type u_3
inst_1 : MulAction G X
inst_2 : MulAction.IsPretransitive G X
hi : H.index ≠ 0
this : Subsingleton.{u_3 + 1} (MulAction.orbitRel.Quotient G X)
⊢ Finite.{u_3 + 1} (MulAction.orbitRel.Quotient.{u_1, u_3} (↥H) X)

Tactic:
exact finite_quotient_of_finite_quotient_of_index_ne_zero hi

Premises used: Subgroup.finite_quotient_of_finite_quotient_of_index_ne_zero
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
this : ∃ (n₁ : ℕ) (n₂ : ℕ), n₁ < n₂ ∧ n₂ ≤ H.index ∧ Eq (α := G ⧸ H) (↑(a ^ n₂) : G ⧸ H) (↑(a ^ n₁) : G ⧸ H)
rcases :
  ∀ (n₁ n₂ : ℕ) (hlt : n₁ < n₂) (hle : n₂ ≤ H.index) (he : Eq (α := G ⧸ H) (↑(a ^ n₂) : G ⧸ H) (↑(a ^ n₁) : G ⧸ H)),
    ∃ (n : ℕ), 0 < n ∧ n ≤ H.index ∧ a ^ n ∈ H
⊢ ∃ (n : ℕ), 0 < n ∧ n ≤ H.index ∧ a ^ n ∈ H

Tactic:
rcases this with ⟨n₁, n₂, hlt, hle, he⟩
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
n₁ n₂ : ℕ
hlt : n₁ < n₂
hle : n₂ ≤ H.index
he : Eq (α := G ⧸ H) (↑(a ^ n₂) : G ⧸ H) (↑(a ^ n₁) : G ⧸ H)
⊢ 0 < n₂ - n₁

Tactic:
lia
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
n₁ n₂ : ℕ
hlt : n₁ < n₂
hle : n₂ ≤ H.index
he : Eq (α := G ⧸ H) (↑(a ^ n₂) : G ⧸ H) (↑(a ^ n₁) : G ⧸ H)
⊢ n₂ - n₁ ≤ H.index

Tactic:
lia
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
n₁ n₂ : ℕ
hlt : n₁ < n₂
hle : n₂ ≤ H.index
he : Eq (α := G ⧸ H) (↑(a ^ n₂) : G ⧸ H) (↑(a ^ n₁) : G ⧸ H)
refine : a ^ (n₂ - n₁) ∈ H
⊢ ∃ (n : ℕ), 0 < n ∧ n ≤ H.index ∧ a ^ n ∈ H

Tactic:
refine ⟨n₂ - n₁, by lia, by lia, ?_⟩
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
n₁ n₂ : ℕ
hlt : n₁ < n₂
hle : n₂ ≤ H.index
he : Eq (α := G ⧸ H) (↑(a ^ n₂) : G ⧸ H) (↑(a ^ n₁) : G ⧸ H)
⊢ a ^ HAdd.hAdd (α := ℤ) (↑n₂ : ℤ) (-(↑n₁ : ℤ)) ∈ H

Tactic:
rw [eq_comm, QuotientGroup.eq, ← zpow_natCast, ← zpow_natCast, ← zpow_neg, ← zpow_add,
        add_comm] at he

Premises used: zpow_natCast, zpow_add, QuotientGroup.eq, eq_comm, add_comm, zpow_neg
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
n₁ n₂ : ℕ
hlt : n₁ < n₂
hle : n₂ ≤ H.index
he : a ^ HAdd.hAdd (α := ℤ) (↑n₂ : ℤ) (-(↑n₁ : ℤ)) ∈ H
rw : HPow.hPow (β := ℤ) a (↑(n₂ - n₁) : ℤ) ∈ H
⊢ a ^ (n₂ - n₁) ∈ H

Tactic:
rw [← zpow_natCast]

Premises used: zpow_natCast
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
n₁ n₂ : ℕ
hlt : n₁ < n₂
hle : n₂ ≤ H.index
he : a ^ HAdd.hAdd (α := ℤ) (↑n₂ : ℤ) (-(↑n₁ : ℤ)) ∈ H
⊢ a ^ HAdd.hAdd (α := ℤ) (↑n₂ : ℤ) (-(↑n₁ : ℤ)) ∈ H

Tactic:
he
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
n₁ n₂ : ℕ
hlt : n₁ < n₂
hle : n₂ ≤ H.index
he : a ^ HAdd.hAdd (α := ℤ) (↑n₂ : ℤ) (-(↑n₁ : ℤ)) ∈ H
h₁ : (↑(n₂ - n₁) : ℤ) = HAdd.hAdd (α := ℤ) (↑n₂ : ℤ) (-(↑n₁ : ℤ))
⊢ HPow.hPow (β := ℤ) a (↑(n₂ - n₁) : ℤ) ∈ H

Tactic:
convert! he
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
n₁ n₂ : ℕ
hlt : n₁ < n₂
hle : n₂ ≤ H.index
he : a ^ HAdd.hAdd (α := ℤ) (↑n₂ : ℤ) (-(↑n₁ : ℤ)) ∈ H
⊢ (↑(n₂ - n₁) : ℤ) = HAdd.hAdd (α := ℤ) (↑n₂ : ℤ) (-(↑n₁ : ℤ))

Tactic:
lia
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
suffices : ∃ (n₁ : ℕ) (n₂ : ℕ), n₁ < n₂ ∧ n₂ ≤ H.index ∧ Eq (α := G ⧸ H) (↑(a ^ n₂) : G ⧸ H) (↑(a ^ n₁) : G ⧸ H)
⊢ ∃ (n : ℕ), 0 < n ∧ n ≤ H.index ∧ a ^ n ∈ H

Tactic:
suffices ∃ n₁ n₂, n₁ < n₂ ∧ n₂ ≤ H.index ∧ ((a ^ n₂ : G) : G ⧸ H) = ((a ^ n₁ : G) : G ⧸ H) by
    rcases this with ⟨n₁, n₂, hlt, hle, he⟩
    refine ⟨n₂ - n₁, by lia, by lia, ?_⟩
    rw [eq_comm, QuotientGroup.eq, ← zpow_natCast, ← zpow_natCast, ← zpow_neg, ← zpow_add,
        add_comm] at he
    rw [← zpow_natCast]
    convert! he
    lia
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
this :
  ∃ (n₁ : ℕ) (n₂ : ℕ), n₁ ≠ n₂ ∧ n₁ ≤ H.index ∧ n₂ ≤ H.index ∧ Eq (α := G ⧸ H) (↑(a ^ n₂) : G ⧸ H) (↑(a ^ n₁) : G ⧸ H)
rcases :
  ∀ (n₁ n₂ : ℕ) (hne : n₁ ≠ n₂) (hle₁ : n₁ ≤ H.index) (hle₂ : n₂ ≤ H.index)
    (he : Eq (α := G ⧸ H) (↑(a ^ n₂) : G ⧸ H) (↑(a ^ n₁) : G ⧸ H)),
    ∃ (n₁ : ℕ) (n₂ : ℕ), n₁ < n₂ ∧ n₂ ≤ H.index ∧ Eq (α := G ⧸ H) (↑(a ^ n₂) : G ⧸ H) (↑(a ^ n₁) : G ⧸ H)
⊢ ∃ (n₁ : ℕ) (n₂ : ℕ), n₁ < n₂ ∧ n₂ ≤ H.index ∧ Eq (α := G ⧸ H) (↑(a ^ n₂) : G ⧸ H) (↑(a ^ n₁) : G ⧸ H)

Tactic:
rcases this with ⟨n₁, n₂, hne, hle₁, hle₂, he⟩
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
n₁ n₂ : ℕ
hne : n₁ ≠ n₂
hle₁ : n₁ ≤ H.index
hle₂ : n₂ ≤ H.index
he : Eq (α := G ⧸ H) (↑(a ^ n₂) : G ⧸ H) (↑(a ^ n₁) : G ⧸ H)
inl :
  ∀ (hlt : n₁ < n₂),
    ∃ (n₁ : ℕ) (n₂ : ℕ), n₁ < n₂ ∧ n₂ ≤ H.index ∧ Eq (α := G ⧸ H) (↑(a ^ n₂) : G ⧸ H) (↑(a ^ n₁) : G ⧸ H)
inr :
  ∀ (hlt : n₂ < n₁),
    ∃ (n₁ : ℕ) (n₂ : ℕ), n₁ < n₂ ∧ n₂ ≤ H.index ∧ Eq (α := G ⧸ H) (↑(a ^ n₂) : G ⧸ H) (↑(a ^ n₁) : G ⧸ H)
⊢ ∃ (n₁ : ℕ) (n₂ : ℕ), n₁ < n₂ ∧ n₂ ≤ H.index ∧ Eq (α := G ⧸ H) (↑(a ^ n₂) : G ⧸ H) (↑(a ^ n₁) : G ⧸ H)

Tactic:
rcases hne.lt_or_gt with hlt | hlt

Premises used: Ne.lt_or_gt
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
n₁ n₂ : ℕ
hne : n₁ ≠ n₂
hle₁ : n₁ ≤ H.index
hle₂ : n₂ ≤ H.index
he : Eq (α := G ⧸ H) (↑(a ^ n₂) : G ⧸ H) (↑(a ^ n₁) : G ⧸ H)
hlt : n₁ < n₂
⊢ ∃ (n₁ : ℕ) (n₂ : ℕ), n₁ < n₂ ∧ n₂ ≤ H.index ∧ Eq (α := G ⧸ H) (↑(a ^ n₂) : G ⧸ H) (↑(a ^ n₁) : G ⧸ H)

Tactic:
⟨n₁, n₂, hlt, hle₂, he⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
n₁ n₂ : ℕ
hne : n₁ ≠ n₂
hle₁ : n₁ ≤ H.index
hle₂ : n₂ ≤ H.index
he : Eq (α := G ⧸ H) (↑(a ^ n₂) : G ⧸ H) (↑(a ^ n₁) : G ⧸ H)
hlt : n₁ < n₂
⊢ ∃ (n₁ : ℕ) (n₂ : ℕ), n₁ < n₂ ∧ n₂ ≤ H.index ∧ Eq (α := G ⧸ H) (↑(a ^ n₂) : G ⧸ H) (↑(a ^ n₁) : G ⧸ H)

Tactic:
exact ⟨n₁, n₂, hlt, hle₂, he⟩
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
n₁ n₂ : ℕ
hne : n₁ ≠ n₂
hle₁ : n₁ ≤ H.index
hle₂ : n₂ ≤ H.index
he : Eq (α := G ⧸ H) (↑(a ^ n₂) : G ⧸ H) (↑(a ^ n₁) : G ⧸ H)
hlt : n₂ < n₁
⊢ ∃ (n₁ : ℕ) (n₂ : ℕ), n₁ < n₂ ∧ n₂ ≤ H.index ∧ Eq (α := G ⧸ H) (↑(a ^ n₂) : G ⧸ H) (↑(a ^ n₁) : G ⧸ H)

Tactic:
⟨n₂, n₁, hlt, hle₁, he.symm⟩

Premises used: And.intro, Exists.intro, Eq.symm
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
n₁ n₂ : ℕ
hne : n₁ ≠ n₂
hle₁ : n₁ ≤ H.index
hle₂ : n₂ ≤ H.index
he : Eq (α := G ⧸ H) (↑(a ^ n₂) : G ⧸ H) (↑(a ^ n₁) : G ⧸ H)
hlt : n₂ < n₁
⊢ ∃ (n₁ : ℕ) (n₂ : ℕ), n₁ < n₂ ∧ n₂ ≤ H.index ∧ Eq (α := G ⧸ H) (↑(a ^ n₂) : G ⧸ H) (↑(a ^ n₁) : G ⧸ H)

Tactic:
exact ⟨n₂, n₁, hlt, hle₁, he.symm⟩
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
suffices :
  ∃ (n₁ : ℕ) (n₂ : ℕ), n₁ ≠ n₂ ∧ n₁ ≤ H.index ∧ n₂ ≤ H.index ∧ Eq (α := G ⧸ H) (↑(a ^ n₂) : G ⧸ H) (↑(a ^ n₁) : G ⧸ H)
⊢ ∃ (n₁ : ℕ) (n₂ : ℕ), n₁ < n₂ ∧ n₂ ≤ H.index ∧ Eq (α := G ⧸ H) (↑(a ^ n₂) : G ⧸ H) (↑(a ^ n₁) : G ⧸ H)

Tactic:
suffices ∃ n₁ n₂, n₁ ≠ n₂ ∧ n₁ ≤ H.index ∧ n₂ ≤ H.index ∧
      ((a ^ n₂ : G) : G ⧸ H) = ((a ^ n₁ : G) : G ⧸ H) by
    rcases this with ⟨n₁, n₂, hne, hle₁, hle₂, he⟩
    rcases hne.lt_or_gt with hlt | hlt
    · exact ⟨n₁, n₂, hlt, hle₂, he⟩
    · exact ⟨n₂, n₁, hlt, hle₁, he.symm⟩
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
by_contra :
  ∀
    (hc :
      ¬∃ (n₁ : ℕ) (n₂ : ℕ),
          n₁ ≠ n₂ ∧ n₁ ≤ H.index ∧ n₂ ≤ H.index ∧ Eq (α := G ⧸ H) (↑(a ^ n₂) : G ⧸ H) (↑(a ^ n₁) : G ⧸ H)),
    False
⊢ ∃ (n₁ : ℕ) (n₂ : ℕ), n₁ ≠ n₂ ∧ n₁ ≤ H.index ∧ n₂ ≤ H.index ∧ Eq (α := G ⧸ H) (↑(a ^ n₂) : G ⧸ H) (↑(a ^ n₁) : G ⧸ H)

Tactic:
by_contra hc
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
hc :
  ¬∃ (n₁ : ℕ) (n₂ : ℕ), n₁ ≠ n₂ ∧ n₁ ≤ H.index ∧ n₂ ≤ H.index ∧ Eq (α := G ⧸ H) (↑(a ^ n₂) : G ⧸ H) (↑(a ^ n₁) : G ⧸ H)
⊢ ∀ (x x_1 : ℕ), ¬(x ≠ x_1 ∧ x ≤ H.index ∧ x_1 ≤ H.index ∧ Eq (α := G ⧸ H) (↑(a ^ x_1) : G ⧸ H) (↑(a ^ x) : G ⧸ H))

Tactic:
simp_rw [not_exists] at hc

Premises used: not_exists
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
hc : ∀ (x x_1 : ℕ), ¬(x ≠ x_1 ∧ x ≤ H.index ∧ x_1 ≤ H.index ∧ Eq (α := G ⧸ H) (↑(a ^ x_1) : G ⧸ H) (↑(a ^ x) : G ⧸ H))
f : (↑(Set.Icc 0 H.index) : Type) → G ⧸ H := fun (n : (↑(Set.Icc 0 H.index) : Type)) ↦ (↑(a ^ (↑n : ℕ)) : G ⧸ H)
n₁ : ℕ
h₁ : 0 ≤ n₁
hle₁ : n₁ ≤ H.index
n₂ : ℕ
h₂ : 0 ≤ n₂
hle₂ : n₂ ≤ H.index
he :
  f (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Set.Icc 0 H.index) n₁ ⋯) =
    f (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Set.Icc 0 H.index) n₂ ⋯)
⊢ ¬(n₁ ≠ n₂ ∧ n₁ ≤ H.index ∧ n₂ ≤ H.index ∧ Eq (α := G ⧸ H) (↑(a ^ n₂) : G ⧸ H) (↑(a ^ n₁) : G ⧸ H))

Tactic:
have hc' := hc n₁ n₂
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
hc : ∀ (x x_1 : ℕ), ¬(x ≠ x_1 ∧ x ≤ H.index ∧ x_1 ≤ H.index ∧ Eq (α := G ⧸ H) (↑(a ^ x_1) : G ⧸ H) (↑(a ^ x) : G ⧸ H))
f : (↑(Set.Icc 0 H.index) : Type) → G ⧸ H := fun (n : (↑(Set.Icc 0 H.index) : Type)) ↦ (↑(a ^ (↑n : ℕ)) : G ⧸ H)
n₁ : ℕ
h₁ : 0 ≤ n₁
hle₁ : n₁ ≤ H.index
n₂ : ℕ
h₂ : 0 ≤ n₂
hle₂ : n₂ ≤ H.index
he : Eq (α := G ⧸ H) (↑(a ^ n₁) : G ⧸ H) (↑(a ^ n₂) : G ⧸ H)
hc' : ¬(n₁ ≠ n₂ ∧ n₁ ≤ H.index ∧ n₂ ≤ H.index ∧ Eq (α := G ⧸ H) (↑(a ^ n₂) : G ⧸ H) (↑(a ^ n₁) : G ⧸ H))
⊢ Eq (α := (↑(Set.Icc 0 H.index) : Type)) (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Set.Icc 0 H.index) n₁ ⋯)
    (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Set.Icc 0 H.index) n₂ ⋯)

Tactic:
simpa [hle₁, hle₂, he] using hc'
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
hc : ∀ (x x_1 : ℕ), ¬(x ≠ x_1 ∧ x ≤ H.index ∧ x_1 ≤ H.index ∧ Eq (α := G ⧸ H) (↑(a ^ x_1) : G ⧸ H) (↑(a ^ x) : G ⧸ H))
f : (↑(Set.Icc 0 H.index) : Type) → G ⧸ H := fun (n : (↑(Set.Icc 0 H.index) : Type)) ↦ (↑(a ^ (↑n : ℕ)) : G ⧸ H)
⊢ Injective f

Tactic:
have hf : Function.Injective f := by
    rintro ⟨n₁, h₁, hle₁⟩ ⟨n₂, h₂, hle₂⟩ he
    have hc' := hc n₁ n₂
    dsimp only [f] at he
    simpa [hle₁, hle₂, he] using hc'
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
hc : ∀ (x x_1 : ℕ), ¬(x ≠ x_1 ∧ x ≤ H.index ∧ x_1 ≤ H.index ∧ Eq (α := G ⧸ H) (↑(a ^ x_1) : G ⧸ H) (↑(a ^ x) : G ⧸ H))
f : (↑(Set.Icc 0 H.index) : Type) → G ⧸ H := fun (n : (↑(Set.Icc 0 H.index) : Type)) ↦ (↑(a ^ (↑n : ℕ)) : G ⧸ H)
hf : Injective f
⊢ Finite.{u_1 + 1} (G ⧸ H)

Tactic:
have := (fintypeOfIndexNeZero h).finite
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
hc : ∀ (x x_1 : ℕ), ¬(x ≠ x_1 ∧ x ≤ H.index ∧ x_1 ≤ H.index ∧ Eq (α := G ⧸ H) (↑(a ^ x_1) : G ⧸ H) (↑(a ^ x) : G ⧸ H))
f : (↑(Set.Icc 0 H.index) : Type) → G ⧸ H := fun (n : (↑(Set.Icc 0 H.index) : Type)) ↦ (↑(a ^ (↑n : ℕ)) : G ⧸ H)
hf : Injective f
this : Finite.{u_1 + 1} (G ⧸ H)
⊢ Nat.card (↑(Set.Icc 0 H.index) : Type) ≤ Nat.card.{u_1} (G ⧸ H)

Tactic:
have hcard := Nat.card_le_card_of_injective f hf
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
hc : ∀ (x x_1 : ℕ), ¬(x ≠ x_1 ∧ x ≤ H.index ∧ x_1 ≤ H.index ∧ Eq (α := G ⧸ H) (↑(a ^ x_1) : G ⧸ H) (↑(a ^ x) : G ⧸ H))
f : (↑(Set.Icc 0 H.index) : Type) → G ⧸ H := fun (n : (↑(Set.Icc 0 H.index) : Type)) ↦ (↑(a ^ (↑n : ℕ)) : G ⧸ H)
hf : Injective f
this : Finite.{u_1 + 1} (G ⧸ H)
hcard : Nat.card (↑(Set.Icc 0 H.index) : Type) ≤ Nat.card.{u_1} (G ⧸ H)
⊢ False

Tactic:
simp [← index_eq_card] at hcard

Premises used: Subgroup.index_eq_card
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
h : H.relIndex K ≠ 0
a : G
ha : a ∈ K
rcases :
  ∀ (n : ℕ) (hlt : 0 < n) (hle : n ≤ (H.subgroupOf K).index)
    (he : Subtype.mk (p := fun (x : G) ↦ x ∈ K) a ha ^ n ∈ H.subgroupOf K),
    ∃ (n : ℕ), 0 < n ∧ n ≤ H.relIndex K ∧ a ^ n ∈ H ⊓ K
⊢ ∃ (n : ℕ), 0 < n ∧ n ≤ H.relIndex K ∧ a ^ n ∈ H ⊓ K

Tactic:
rcases exists_pow_mem_of_index_ne_zero h ⟨a, ha⟩ with ⟨n, hlt, hle, he⟩

Premises used: Subtype.mk, Subgroup.exists_pow_mem_of_index_ne_zero
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
h : H.relIndex K ≠ 0
a : G
ha : a ∈ K
n : ℕ
hlt : 0 < n
hle : n ≤ (H.subgroupOf K).index
he : Subtype.mk (p := fun (x : G) ↦ x ∈ K) a ha ^ n ∈ H.subgroupOf K
⊢ ∃ (n : ℕ), 0 < n ∧ n ≤ H.relIndex K ∧ a ^ n ∈ H ⊓ K

Tactic:
⟨n, hlt, hle, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
h : H.relIndex K ≠ 0
a : G
ha : a ∈ K
n : ℕ
hlt : 0 < n
hle : n ≤ (H.subgroupOf K).index
he : Subtype.mk (p := fun (x : G) ↦ x ∈ K) a ha ^ n ∈ H.subgroupOf K
refine : a ^ n ∈ H ⊓ K
⊢ ∃ (n : ℕ), 0 < n ∧ n ≤ H.relIndex K ∧ a ^ n ∈ H ⊓ K

Tactic:
refine ⟨n, hlt, hle, ?_⟩
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
h : H.relIndex K ≠ 0
a : G
ha : a ∈ K
n : ℕ
hlt : 0 < n
hle : n ≤ (H.subgroupOf K).index
he : Subtype.mk (p := fun (x : G) ↦ x ∈ K) a ha ^ n ∈ H.subgroupOf K
⊢ a ^ n ∈ H ⊓ K

Tactic:
simpa [pow_mem ha, mem_subgroupOf] using he

Premises used: pow_mem, Subgroup.mem_subgroupOf
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
n : ℕ
hn : ∀ (m : ℕ), 0 < m → m ≤ H.index → m ∣ n
rcases : ∀ (m : ℕ) (hlt : 0 < m) (hle : m ≤ H.index) (he : a ^ m ∈ H), a ^ n ∈ H
⊢ a ^ n ∈ H

Tactic:
rcases exists_pow_mem_of_index_ne_zero h a with ⟨m, hlt, hle, he⟩

Premises used: Subgroup.exists_pow_mem_of_index_ne_zero
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
n : ℕ
hn : ∀ (m : ℕ), 0 < m → m ≤ H.index → m ∣ n
m : ℕ
hlt : 0 < m
hle : m ≤ H.index
he : a ^ m ∈ H
rcases : ∀ (k : ℕ) (hn : ∀ (m_1 : ℕ), 0 < m_1 → m_1 ≤ H.index → m_1 ∣ m * k), a ^ (m * k) ∈ H
⊢ a ^ n ∈ H

Tactic:
rcases hn m hlt hle with ⟨k, rfl⟩

Premises used: rfl
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
m : ℕ
hlt : 0 < m
hle : m ≤ H.index
he : a ^ m ∈ H
k : ℕ
hn : ∀ (m_1 : ℕ), 0 < m_1 → m_1 ≤ H.index → m_1 ∣ m * k
rw : (a ^ m) ^ k ∈ H
⊢ a ^ (m * k) ∈ H

Tactic:
rw [pow_mul]

Premises used: pow_mul
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
m : ℕ
hlt : 0 < m
hle : m ≤ H.index
he : a ^ m ∈ H
k : ℕ
hn : ∀ (m_1 : ℕ), 0 < m_1 → m_1 ≤ H.index → m_1 ∣ m * k
⊢ (a ^ m) ^ k ∈ H

Tactic:
pow_mem he _

Premises used: pow_mem
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
m : ℕ
hlt : 0 < m
hle : m ≤ H.index
he : a ^ m ∈ H
k : ℕ
hn : ∀ (m_1 : ℕ), 0 < m_1 → m_1 ≤ H.index → m_1 ∣ m * k
⊢ (a ^ m) ^ k ∈ H

Tactic:
exact pow_mem he _

Premises used: pow_mem
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
h : H.relIndex K ≠ 0
a : G
ha : a ∈ K
n : ℕ
hn : ∀ (m : ℕ), 0 < m → m ≤ H.relIndex K → m ∣ n
⊢ Subtype.mk (p := fun (x : G) ↦ x ∈ K) a ha ^ n ∈ H.subgroupOf K

Tactic:
pow_mem_of_index_ne_zero_of_dvd h ⟨a, ha⟩ hn

Premises used: Subgroup.pow_mem_of_index_ne_zero_of_dvd, Subtype.mk
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
h : H.relIndex K ≠ 0
a : G
ha : a ∈ K
n : ℕ
hn : ∀ (m : ℕ), 0 < m → m ≤ H.relIndex K → m ∣ n
a₁ : a ^ n ∈ H ⊓ K ↔ Subtype.mk (p := fun (x : G) ↦ x ∈ K) a ha ^ n ∈ H.subgroupOf K
⊢ a ^ n ∈ H ⊓ K

Tactic:
convert! pow_mem_of_index_ne_zero_of_dvd h ⟨a, ha⟩ hn

Premises used: Subgroup.pow_mem_of_index_ne_zero_of_dvd, Subtype.mk
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
h : H.relIndex K ≠ 0
a : G
ha : a ∈ K
n : ℕ
hn : ∀ (m : ℕ), 0 < m → m ≤ H.relIndex K → m ∣ n
⊢ a ^ n ∈ H ⊓ K ↔ Subtype.mk (p := fun (x : G) ↦ x ∈ K) a ha ^ n ∈ H.subgroupOf K

Tactic:
simp [pow_mem ha, mem_subgroupOf]

Premises used: pow_mem, Subgroup.mem_subgroupOf
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H : Subgroup G
K : Subgroup G'
simp_rw : Nat.card ((G × G') ⧸ H.prod K) = Nat.card (Prod.{u_1, u_2} (G ⧸ H) (G' ⧸ K))
⊢ (H.prod K).index = H.index * K.index

Tactic:
simp_rw [index, ← Nat.card_prod]

Premises used: Subgroup.index, Nat.card_prod
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H : Subgroup G
K : Subgroup G'
⊢ Nat.card ((G × G') ⧸ H.prod K) = Nat.card (Prod.{u_1, u_2} (G ⧸ H) (G' ⧸ K))

Tactic:
Nat.card_congr (QuotientGroup.prodEquiv H K)

Premises used: QuotientGroup.prodEquiv, Nat.card_congr
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H : Subgroup G
K : Subgroup G'
⊢ Nat.card ((G × G') ⧸ H.prod K) = Nat.card (Prod.{u_1, u_2} (G ⧸ H) (G' ⧸ K))

Tactic:
exact Nat.card_congr (QuotientGroup.prodEquiv H K)

Premises used: QuotientGroup.prodEquiv, Nat.card_congr
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
ι : Type u_3
inst_1 : Fintype ι
H : ι → Subgroup G
simp_rw : Nat.card (((i : ι) → G) ⧸ pi (f := fun (i : ι) ↦ G) Set.univ H) = Nat.card ((a : ι) → G ⧸ H a)
⊢ (pi (f := fun (i : ι) ↦ G) Set.univ H).index = ∏ i : ι, (H i).index

Tactic:
simp_rw [index, ← Nat.card_pi]

Premises used: Nat.card_pi, Subgroup.index
-- Module: Mathlib.GroupTheory.Index
Goal:
G : Type u_1
inst : Group G
ι : Type u_3
inst_1 : Fintype ι
H : ι → Subgroup G
⊢ Nat.card (((i : ι) → G) ⧸ pi (f := fun (i : ι) ↦ G) Set.univ H) = Nat.card ((a : ι) → G ⧸ H a)

Tactic:
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