awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
⊢ ∃ (n₁ : ℕ) (n₂ : ℕ), n₁ ≠ n₂ ∧ n₁ ≤ H.index ∧ n₂ ≤ H.index ∧ Eq (α := G ⧸ H) (↑(a ^ n₂) : G ⧸ H) (↑(a ^ n₁) : G ⧸ H)
have 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
Tactic: by_contra hc
-- Lean 4 proof step from Mathlib.GroupTheory.Index (hypothesis)
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)
⊢ False
have 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))
Tactic: simp_rw [not_exists] at hc
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.GroupTheory.Index (hypothesis)
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₂ ⋯)
⊢ 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₂ ⋯)
have hc' : ¬(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₂
-- Lean 4 proof step from Mathlib.GroupTheory.Index (hypothesis)
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)
⊢ False
have hf : 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'
-- Lean 4 proof step from Mathlib.GroupTheory.Index (hypothesis)
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
⊢ False
have this : Finite.{u_1 + 1} (G ⧸ H)
Tactic: have := (fintypeOfIndexNeZero h).finite
-- Lean 4 proof step from Mathlib.GroupTheory.Index (hypothesis)
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)
⊢ False
have hcard : 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
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
h : H.relIndex K ≠ 0
a : G
ha : a ∈ K
⊢ ∃ (n : ℕ), 0 < n ∧ n ≤ H.relIndex K ∧ a ^ n ∈ H ⊓ K
have 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
Tactic: rcases exists_pow_mem_of_index_ne_zero h ⟨a, ha⟩ with ⟨n, hlt, hle, he⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
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
have refine : a ^ n ∈ H ⊓ K
Tactic: refine ⟨n, hlt, hle, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
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
⊢ a ^ n ∈ H
have rcases : ∀ (m : ℕ) (hlt : 0 < m) (hle : m ≤ H.index) (he : a ^ m ∈ H), a ^ n ∈ H
Tactic: rcases exists_pow_mem_of_index_ne_zero h a with ⟨m, hlt, hle, he⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
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
⊢ a ^ n ∈ H
have rcases : ∀ (k : ℕ) (hn : ∀ (m_1 : ℕ), 0 < m_1 → m_1 ≤ H.index → m_1 ∣ m * k), a ^ (m * k) ∈ H
Tactic: rcases hn m hlt hle with ⟨k, rfl⟩
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
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
have rw : (a ^ m) ^ k ∈ H
Tactic: rw [pow_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
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
have a₁ : a ^ n ∈ H ⊓ K ↔ Subtype.mk (p := fun (x : G) ↦ x ∈ K) a ha ^ n ∈ H.subgroupOf K
Tactic: convert! pow_mem_of_index_ne_zero_of_dvd h ⟨a, ha⟩ hn
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H : Subgroup G
K : Subgroup G'
⊢ (H.prod K).index = H.index * K.index
have simp_rw : Nat.card ((G × G') ⧸ H.prod K) = Nat.card (Prod.{u_1, u_2} (G ⧸ H) (G' ⧸ K))
Tactic: simp_rw [index, ← Nat.card_prod]
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
Goal:
G : Type u_1
inst : Group G
ι : Type u_3
inst_1 : Fintype ι
H : ι → Subgroup G
⊢ (pi (f := fun (i : ι) ↦ G) Set.univ H).index = ∏ i : ι, (H i).index
have simp_rw : Nat.card (((i : ι) → G) ⧸ pi (f := fun (i : ι) ↦ G) Set.univ H) = Nat.card ((a : ι) → G ⧸ H a)
Tactic: simp_rw [index, ← Nat.card_pi]
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
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)
have 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
Tactic: refine Nat.card_congr
    ((Quotient.congrRight (fun x y ↦ ?_)).trans (Setoid.piQuotientEquiv _).symm)
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
Goal:
G : Type u_1
inst : Group G
ι : Type u_3
inst_1 : Fintype ι
H : ι → Subgroup G
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
have rw : (piSetoid : ((i : ι) → G) → ((i : ι) → G) → Prop) x y ↔ (piSetoid : ((i : ι) → G) → ((i : ι) → G) → Prop) x y
Tactic: rw [QuotientGroup.leftRel_pi]
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
⊢ H.IsFiniteRelIndex K ↔ (H.subgroupOf K).FiniteIndex
have rw : H.relIndex K ≠ 0 ↔ (H.subgroupOf K).FiniteIndex
Tactic: rw [isFiniteRelIndex_iff_relIndex_ne_zero, finiteIndex_iff, relIndex]
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
rw : H.relIndex K ≠ 0 ↔ (H.subgroupOf K).FiniteIndex
⊢ H.IsFiniteRelIndex K ↔ (H.subgroupOf K).FiniteIndex
have rw₁ : H.relIndex K ≠ 0 ↔ (H.subgroupOf K).index ≠ 0
Tactic: rw [isFiniteRelIndex_iff_relIndex_ne_zero, finiteIndex_iff, relIndex]
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
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
⊢ H.IsFiniteRelIndex K ↔ (H.subgroupOf K).FiniteIndex
have rw₂ : (H.subgroupOf K).index ≠ 0 ↔ (H.subgroupOf K).index ≠ 0
Tactic: rw [isFiniteRelIndex_iff_relIndex_ne_zero, finiteIndex_iff, relIndex]
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
⊢ H.IsFiniteRelIndex ⊤ ↔ H.FiniteIndex
have rw : H.IsFiniteRelIndex ⊤ ↔ H.index ≠ 0
Tactic: rw [finiteIndex_iff, isFiniteRelIndex_iff_relIndex_ne_zero, relIndex_top_right]
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
rw : H.IsFiniteRelIndex ⊤ ↔ H.index ≠ 0
⊢ H.IsFiniteRelIndex ⊤ ↔ H.FiniteIndex
have rw₁ : H.relIndex ⊤ ≠ 0 ↔ H.index ≠ 0
Tactic: rw [finiteIndex_iff, isFiniteRelIndex_iff_relIndex_ne_zero, relIndex_top_right]
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
rw : H.IsFiniteRelIndex ⊤ ↔ H.index ≠ 0
rw₁ : H.relIndex ⊤ ≠ 0 ↔ H.index ≠ 0
⊢ H.IsFiniteRelIndex ⊤ ↔ H.FiniteIndex
have rw₂ : H.index ≠ 0 ↔ H.index ≠ 0
Tactic: rw [finiteIndex_iff, isFiniteRelIndex_iff_relIndex_ne_zero, relIndex_top_right]
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
f : G →* G'
⊢ Finite G ↔ Finite.{u_1 + 1} ↥f.ker ∧ Finite.{u_2 + 1} ↥f.range
have rw : Finite.{u_1 + 1} ↥f.ker ∧ f.ker.FiniteIndex ↔ 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]
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
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
⊢ Finite G ↔ Finite.{u_1 + 1} ↥f.ker ∧ Finite.{u_2 + 1} ↥f.range
have rw₁ : Finite.{u_1 + 1} ↥f.ker ∧ f.ker.FiniteIndex ↔ Finite.{u_1 + 1} ↥f.ker ∧ Finite.{u_1 + 1} (G ⧸ f.ker)
Tactic: rw [finite_iff_finite_and_finiteIndex f.ker, ← (QuotientGroup.quotientKerEquivRange f).finite_iff,
    finiteIndex_iff_finite_quotient]
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
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)
⊢ Finite G ↔ Finite.{u_1 + 1} ↥f.ker ∧ Finite.{u_2 + 1} ↥f.range
have 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)
Tactic: rw [finite_iff_finite_and_finiteIndex f.ker, ← (QuotientGroup.quotientKerEquivRange f).finite_iff,
    finiteIndex_iff_finite_quotient]
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
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) (⨅ i ∈ s, f i)
have rw : FiniteIndex.{u_1} (G := G) (⨅ (x : Subtype (Membership.mem s)), f (↑x : ι))
Tactic: rw [iInf_subtype']
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
Goal:
G : Type u_1
inst : Group G
H K L : Subgroup G
inst_1 : H.IsFiniteRelIndex L
h : H ≤ K
⊢ K.IsFiniteRelIndex L
have rw : (H.subgroupOf L).FiniteIndex → ∀ (h : H ≤ K), (K.subgroupOf L).FiniteIndex
Tactic: rw [isFiniteRelIndex_iff_finiteIndex] at *
Cleared hypotheses: inst_1, h
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
Goal:
G : Type u_1
inst : Group G
H K L : Subgroup G
h : K ≤ L
inst_1 : H.IsFiniteRelIndex L
⊢ H.IsFiniteRelIndex K
have rw : H.relIndex K ≠ 0
Tactic: rw [isFiniteRelIndex_iff_relIndex_ne_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.Index (hypothesis)
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
h : H.FiniteIndex
⊢ H.IsFiniteRelIndex K
have h₁ : H.IsFiniteRelIndex ⊤
Tactic: rw [← isFiniteRelIndex_top_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.Index (hypothesis)
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
h : H < K
inst_1 : H.FiniteIndex
⊢ K.index < H.index
have h0 : K.index ≠ 0
Tactic: have h0 : K.index ≠ 0 := (finiteIndex_of_le h.le).index_ne_zero
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
h : H < K
inst_1 : H.FiniteIndex
h0 : K.index ≠ 0
⊢ K.index < H.index
have apply : K.index ≠ H.index
Tactic: apply lt_of_le_of_ne (index_antitone h.le)
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
h : H < K
inst_1 : H.FiniteIndex
h0 : K.index ≠ 0
⊢ K.index ≠ H.index
have rw : ¬K ≤ H
Tactic: rw [← relIndex_mul_index h.le, Ne, eq_comm, mul_eq_right₀ h0, relIndex_eq_one]
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
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
⊢ H.normalCore.FiniteIndex
have rw : FiniteIndex (MonoidHom.ker (M := Equiv.Perm (G ⧸ H)) (MulAction.toPermHom G (G ⧸ H)))
Tactic: rw [normalCore_eq_ker]
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
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
⊢ H.normalCore.FiniteIndex
have 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)
Tactic: rw [← AddSubgroup.finiteIndex_toSubgroup_iff] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
Goal:
G : Type u_1
inst : Group G
f : G →* G
hf : f.ker.FiniteIndex
⊢ f.range.index = Nat.card.{u_1} ↥f.ker
have rw : f.range.index * f.ker.index = Nat.card.{u_1} ↥f.ker * f.ker.index
Tactic: rw [← mul_left_inj' hf.index_ne_zero, card_mul_index, index_ker, index_mul_card]
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
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
⊢ f.range.index = Nat.card.{u_1} ↥f.ker
have rw₁ : f.range.index * f.ker.index = Nat.card G
Tactic: rw [← mul_left_inj' hf.index_ne_zero, card_mul_index, index_ker, index_mul_card]
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
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
⊢ f.range.index = Nat.card.{u_1} ↥f.ker
have rw₂ : f.range.index * Nat.card.{u_1} ↥f.range = Nat.card G
Tactic: rw [← mul_left_inj' hf.index_ne_zero, card_mul_index, index_ker, index_mul_card]
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
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
⊢ f.range.index = Nat.card.{u_1} ↥f.ker
have rw₃ : Nat.card G = Nat.card G
Tactic: rw [← mul_left_inj' hf.index_ne_zero, card_mul_index, index_ker, index_mul_card]
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
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
⊢ (h • J).relIndex (h • K) = J.relIndex K
have 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
Tactic: rw [pointwise_smul_def K, ← relIndex_comap, pointwise_smul_def,
    comap_map_eq_self_of_injective (by intro a b; simp)]
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
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
⊢ (h • J).relIndex (h • K) = J.relIndex K
have 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
Tactic: rw [pointwise_smul_def K, ← relIndex_comap, pointwise_smul_def,
    comap_map_eq_self_of_injective (by intro a b; simp)]
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
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
⊢ (h • J).relIndex (h • K) = J.relIndex K
have 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
Tactic: rw [pointwise_smul_def K, ← relIndex_comap, pointwise_smul_def,
    comap_map_eq_self_of_injective (by intro a b; simp)]
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
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
⊢ (h • J).relIndex (h • K) = J.relIndex K
have rw₃ : J.relIndex 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)]
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
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
⊢ (h • J).relIndex (h • K) = J.relIndex K
have 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
Tactic: rw [pointwise_smul_def K, ← relIndex_comap, pointwise_smul_def,
    comap_map_eq_self_of_injective (by intro a b; simp)]
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
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
⊢ (h • J).relIndex (h • K) = J.relIndex K
have 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
Tactic: rw [pointwise_smul_def K, ← relIndex_comap, pointwise_smul_def,
    comap_map_eq_self_of_injective (by intro a b; simp)]
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
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
⊢ (h • J).relIndex (h • K) = J.relIndex K
have 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
Tactic: rw [pointwise_smul_def K, ← relIndex_comap, pointwise_smul_def,
    comap_map_eq_self_of_injective (by intro a b; simp)]
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
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
⊢ (h • J).relIndex (h • K) = J.relIndex K
have rw₃ : J.relIndex 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)]
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
x : X
inst_2 : IsPretransitive G X
⊢ Subgroup.index (stabilizer G x) = Nat.card X
have rw : (orbit G x).ncard = Nat.card X
Tactic: rw [index_stabilizer, orbit_eq_univ, Set.ncard_univ]
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
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
⊢ Subgroup.index (stabilizer G x) = Nat.card X
have rw₁ : Set.ncard.{u_2} (α := X) Set.univ = Nat.card X
Tactic: rw [index_stabilizer, orbit_eq_univ, Set.ncard_univ]
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
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
⊢ Subgroup.index (stabilizer G x) = Nat.card X
have rw₂ : Nat.card X = Nat.card X
Tactic: rw [index_stabilizer, orbit_eq_univ, Set.ncard_univ]
-- 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
⊢ Function.Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := M) (⇑f : (a : G) → M)
have refine : (↑⊤ : Set M).ncard ≤ (↑f.range : Set M).ncard
Tactic: refine range_eq_top.1 <| SetLike.ext' <| Set.eq_of_subset_of_ncard_le (Set.subset_univ _) ?_