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
rw : (subgroupOf ⊥ H).index = Nat.card.{u_1} ↥H
⊢ relIndex ⊥ H = Nat.card.{u_1} ↥H
have rw₁ : index.{u_1} (G := ↥H) ⊥ = Nat.card.{u_1} ↥H
Tactic: rw [relIndex, bot_subgroupOf, index_bot]
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
rw : (subgroupOf ⊥ H).index = Nat.card.{u_1} ↥H
rw₁ : index.{u_1} (G := ↥H) ⊥ = Nat.card.{u_1} ↥H
⊢ relIndex ⊥ H = Nat.card.{u_1} ↥H
have rw₂ : Nat.card.{u_1} ↥H = Nat.card.{u_1} ↥H
Tactic: rw [relIndex, bot_subgroupOf, index_bot]
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
⊢ H.relIndex ⊥ = 1
have rw : index (G := ↥⊥) (H.subgroupOf ⊥) = 1
Tactic: rw [relIndex, subgroupOf_bot_eq_top, index_top]
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
rw : index (G := ↥⊥) (H.subgroupOf ⊥) = 1
⊢ H.relIndex ⊥ = 1
have rw₁ : index.{u_1} (G := ↥⊥) ⊤ = 1
Tactic: rw [relIndex, subgroupOf_bot_eq_top, index_top]
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
rw : index (G := ↥⊥) (H.subgroupOf ⊥) = 1
rw₁ : index.{u_1} (G := ↥⊥) ⊤ = 1
⊢ H.relIndex ⊥ = 1
have rw₂ : Eq (α := ℕ) 1 1
Tactic: rw [relIndex, subgroupOf_bot_eq_top, index_top]
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
⊢ H.relIndex H = 1
have rw : (H.subgroupOf H).index = 1
Tactic: rw [relIndex, subgroupOf_self, index_top]
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
rw : (H.subgroupOf H).index = 1
⊢ H.relIndex H = 1
have rw₁ : index.{u_1} (G := ↥H) ⊤ = 1
Tactic: rw [relIndex, subgroupOf_self, index_top]
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
rw : (H.subgroupOf H).index = 1
rw₁ : index.{u_1} (G := ↥H) ⊤ = 1
⊢ H.relIndex H = 1
have rw₂ : Eq (α := ℕ) 1 1
Tactic: rw [relIndex, subgroupOf_self, index_top]
-- 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'
⊢ f.ker.index = Nat.card.{u_2} ↥f.range
have rw : (comap f ⊥).index = Nat.card.{u_2} ↥f.range
Tactic: rw [← MonoidHom.comap_bot, index_comap, relIndex_bot_left]
-- 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 : (comap f ⊥).index = Nat.card.{u_2} ↥f.range
⊢ f.ker.index = Nat.card.{u_2} ↥f.range
have rw₁ : relIndex ⊥ f.range = Nat.card.{u_2} ↥f.range
Tactic: rw [← MonoidHom.comap_bot, index_comap, relIndex_bot_left]
-- 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 : (comap f ⊥).index = Nat.card.{u_2} ↥f.range
rw₁ : relIndex ⊥ f.range = Nat.card.{u_2} ↥f.range
⊢ f.ker.index = Nat.card.{u_2} ↥f.range
have rw₂ : Nat.card.{u_2} ↥f.range = Nat.card.{u_2} ↥f.range
Tactic: rw [← MonoidHom.comap_bot, index_comap, relIndex_bot_left]
-- 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'
K : Subgroup G
f : G →* G'
⊢ f.ker.relIndex K = Nat.card.{u_2} ↥(map f K)
have rw : (comap f ⊥).relIndex K = Nat.card.{u_2} ↥(map f K)
Tactic: rw [← MonoidHom.comap_bot, relIndex_comap, relIndex_bot_left]
-- 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'
K : Subgroup G
f : G →* G'
rw : (comap f ⊥).relIndex K = Nat.card.{u_2} ↥(map f K)
⊢ f.ker.relIndex K = Nat.card.{u_2} ↥(map f K)
have rw₁ : relIndex ⊥ (map f K) = Nat.card.{u_2} ↥(map f K)
Tactic: rw [← MonoidHom.comap_bot, relIndex_comap, relIndex_bot_left]
-- 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'
K : Subgroup G
f : G →* G'
rw : (comap f ⊥).relIndex K = Nat.card.{u_2} ↥(map f K)
rw₁ : relIndex ⊥ (map f K) = Nat.card.{u_2} ↥(map f K)
⊢ f.ker.relIndex K = Nat.card.{u_2} ↥(map f K)
have rw₂ : Nat.card.{u_2} ↥(map f K) = Nat.card.{u_2} ↥(map f K)
Tactic: rw [← MonoidHom.comap_bot, relIndex_comap, relIndex_bot_left]
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
⊢ Nat.card.{u_1} ↥H * H.index = Nat.card G
have rw : relIndex ⊥ H * H.index = index.{u_1} (G := G) ⊥
Tactic: rw [← relIndex_bot_left, ← index_bot]
-- 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'
hf : Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := G') (⇑f : (a : G) → G')
⊢ Nat.card G' ∣ Nat.card G
have rw : Nat.card.{u_1} (G ⧸ f.ker) ∣ Nat.card G
Tactic: rw [← Nat.card_congr (QuotientGroup.quotientKerEquivOfSurjective f hf).toEquiv]
-- 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
f : G →* G'
⊢ (map f H).index = (H ⊔ f.ker).index * f.range.index
have rw : (map f H).index = (comap f (map f H)).index * f.range.index
Tactic: rw [← comap_map_eq, index_comap, relIndex_mul_index (H.map_le_range f)]
-- 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
f : G →* G'
rw : (map f H).index = (comap f (map f H)).index * f.range.index
⊢ (map f H).index = (H ⊔ f.ker).index * f.range.index
have rw₁ : (map f H).index = (map f H).relIndex f.range * f.range.index
Tactic: rw [← comap_map_eq, index_comap, relIndex_mul_index (H.map_le_range f)]
-- 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
f : G →* G'
rw : (map f H).index = (comap f (map f H)).index * f.range.index
rw₁ : (map f H).index = (map f H).relIndex f.range * f.range.index
⊢ (map f H).index = (H ⊔ f.ker).index * f.range.index
have rw₂ : (map f H).index = (map f H).index
Tactic: rw [← comap_map_eq, index_comap, relIndex_mul_index (H.map_le_range f)]
-- 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
f : G →* G'
hf : Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := G') (⇑f : (a : G) → G')
⊢ (map f H).index ∣ H.index
have rw : (H ⊔ f.ker).index ∣ H.index
Tactic: rw [index_map, f.range_eq_top_of_surjective hf, index_top, mul_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 : Subgroup G
f : G →* G'
hf : f.ker ≤ H
⊢ H.index ∣ (map f H).index
have rw : H.index ∣ H.index * f.range.index
Tactic: rw [index_map, sup_of_le_left hf]
-- 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'
hf : Bijective.{u_1 + 1, u_2 + 1} (α := G) (β := G') (⇑f : (a : G) → G')
H : Subgroup G
⊢ f.ker ≤ H
have rw : ⊥ ≤ H
Tactic: rw [f.ker_eq_bot_iff.2 hf.1]
-- 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
f : G →* G'
hf : Injective.{u_1 + 1, u_2 + 1} (α := G) (β := G') (⇑f : (a : G) → G')
⊢ (map f H).index = H.index * f.range.index
have rw : (H ⊔ f.ker).index * f.range.index = H.index * f.range.index
Tactic: rw [H.index_map, f.ker_eq_bot_iff.mpr hf, sup_bot_eq]
-- 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
f : G →* G'
hf : Injective.{u_1 + 1, u_2 + 1} (α := G) (β := G') (⇑f : (a : G) → G')
rw : (H ⊔ f.ker).index * f.range.index = H.index * f.range.index
⊢ (map f H).index = H.index * f.range.index
have rw₁ : (H ⊔ ⊥).index * f.range.index = H.index * f.range.index
Tactic: rw [H.index_map, f.ker_eq_bot_iff.mpr hf, sup_bot_eq]
-- 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
f : G →* G'
hf : Injective.{u_1 + 1, u_2 + 1} (α := G) (β := G') (⇑f : (a : G) → G')
rw : (H ⊔ f.ker).index * f.range.index = H.index * f.range.index
rw₁ : (H ⊔ ⊥).index * f.range.index = H.index * f.range.index
⊢ (map f H).index = H.index * f.range.index
have rw₂ : H.index * f.range.index = H.index * f.range.index
Tactic: rw [H.index_map, f.ker_eq_bot_iff.mpr hf, sup_bot_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
K : Subgroup ↥H
⊢ (map H.subtype K).index = K.index * H.index
have rw : K.index * H.subtype.range.index = K.index * H.index
Tactic: rw [K.index_map_of_injective H.subtype_injective, H.range_subtype]
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
K : Subgroup ↥H
rw : K.index * H.subtype.range.index = K.index * H.index
⊢ (map H.subtype K).index = K.index * H.index
have rw₁ : K.index * H.index = K.index * H.index
Tactic: rw [K.index_map_of_injective H.subtype_injective, H.range_subtype]
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
⊢ H.index * Nat.card.{u_1} ↥H = Nat.card G
have rw : Nat.card.{u_1} ↥H * H.index = Nat.card G
Tactic: rw [mul_comm, card_mul_index]
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
rw : Nat.card.{u_1} ↥H * H.index = Nat.card G
⊢ H.index * Nat.card.{u_1} ↥H = Nat.card G
have rw₁ : Nat.card G = Nat.card G
Tactic: rw [mul_comm, card_mul_index]
-- 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'
J K : Subgroup G'
hJK : J.relIndex K ≠ 0
⊢ (comap f J).relIndex (comap f K) ≠ 0
have rw : J.relIndex (map f (comap f K)) ≠ 0
Tactic: rw [relIndex_comap]
-- Lean 4 proof step from Mathlib.GroupTheory.Index (hypothesis)
Goal:
G : Type u_1
inst : Group G
H K L : Subgroup G
hH : H.relIndex L ≠ 0
hK : K.relIndex L ≠ 0
⊢ (H ⊓ K).relIndex L ≠ 0
have hH₁ : H.relIndex (K ⊓ L) ≠ 0
Tactic: replace hH : H.relIndex (K ⊓ L) ≠ 0 := mt (relIndex_eq_zero_of_le_right inf_le_right) hH
Cleared hypotheses: hH
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
Goal:
G : Type u_1
inst : Group G
H K L : Subgroup G
hK : K.relIndex L ≠ 0
hH : H.relIndex (K ⊓ L) ≠ 0
⊢ (H ⊓ K).relIndex L ≠ 0
have rw : ∀ (hK : (K ⊓ L).relIndex L ≠ 0) (hH : (H ⊓ (K ⊓ L)).relIndex (K ⊓ L) ≠ 0), (H ⊓ K ⊓ L).relIndex L ≠ 0
Tactic: rw [← inf_relIndex_right] at hH hK ⊢
Cleared hypotheses: hK, hH
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
Goal:
G : Type u_1
inst : Group G
H K L : Subgroup G
hK : (K ⊓ L).relIndex L ≠ 0
hH : (H ⊓ (K ⊓ L)).relIndex (K ⊓ L) ≠ 0
⊢ (H ⊓ K ⊓ L).relIndex L ≠ 0
have rw : (H ⊓ (K ⊓ L)).relIndex L ≠ 0
Tactic: rw [inf_assoc]
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
hH : H.index ≠ 0
hK : K.index ≠ 0
⊢ (H ⊓ K).index ≠ 0
have rw : ∀ (hH : H.relIndex ⊤ ≠ 0) (hK : K.relIndex ⊤ ≠ 0), (H ⊓ K).relIndex ⊤ ≠ 0
Tactic: rw [← relIndex_top_right] at hH hK ⊢
Cleared hypotheses: hH, hK
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
Goal:
G : Type u_1
inst : Group G
J K : Subgroup G
hJK : J.relIndex K ≠ 0
L : Subgroup G
⊢ (J ⊓ L).relIndex (K ⊓ L) ≠ 0
have rw : (comap L.subtype J).relIndex (comap L.subtype K) ≠ 0
Tactic: rw [← range_subtype L, inf_comm, ← map_comap_eq, inf_comm, ← map_comap_eq, ← relIndex_comap,
    comap_map_eq_self_of_injective (subtype_injective L)]
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
Goal:
G : Type u_1
inst : Group G
H K L : Subgroup G
⊢ (H ⊓ K).relIndex L ≤ H.relIndex L * K.relIndex L
have pos : ∀ (h : H.relIndex L = 0), (H ⊓ K).relIndex L ≤ H.relIndex L * K.relIndex L
Tactic: by_cases h : H.relIndex L = 0
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
Goal:
G : Type u_1
inst : Group G
H K L : Subgroup G
pos : ∀ (h : H.relIndex L = 0), (H ⊓ K).relIndex L ≤ H.relIndex L * K.relIndex L
⊢ (H ⊓ K).relIndex L ≤ H.relIndex L * K.relIndex L
have neg : ∀ (h : ¬H.relIndex L = 0), (H ⊓ K).relIndex L ≤ H.relIndex L * K.relIndex L
Tactic: by_cases h : H.relIndex L = 0
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
Goal:
G : Type u_1
inst : Group G
H K L : Subgroup G
h : ¬H.relIndex L = 0
⊢ (H ⊓ K).relIndex L ≤ H.relIndex L * K.relIndex L
have neg : H.relIndex (K ⊓ L) * K.relIndex L ≤ H.relIndex L * K.relIndex L
Tactic: rw [← inf_relIndex_right, inf_assoc, ← relIndex_mul_relIndex _ _ L inf_le_right inf_le_right,
    inf_relIndex_right, inf_relIndex_right]
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
Goal:
G : Type u_1
inst : Group G
H K L : Subgroup G
h : ¬H.relIndex L = 0
⊢ H.relIndex (K ⊓ L) * K.relIndex L ≤ H.relIndex L * K.relIndex L
have neg : H.relIndex L * K.relIndex L ≤ H.relIndex L * K.relIndex L
Tactic: grw [relIndex_le_of_le_right inf_le_right h]
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
⊢ (H ⊓ K).index ≤ H.index * K.index
have simp_rw : (H ⊓ K).relIndex ⊤ ≤ H.relIndex ⊤ * K.relIndex ⊤
Tactic: simp_rw [← relIndex_top_right, relIndex_inf_le]
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
Goal:
G : Type u_1
inst : Group G
ι : Type u_3
inst_1 : Finite ι
f : ι → Subgroup G
hf : ∀ (i : ι), (f i).index ≠ 0
⊢ index.{u_1} (G := G) (⨅ (i : ι), f i) ≠ 0
have simp_rw : ∀ (hf : ∀ (i : ι), (f i).relIndex ⊤ ≠ 0), relIndex.{u_1} (G := G) (⨅ (i : ι), f i) ⊤ ≠ 0
Tactic: simp_rw [← relIndex_top_right] at hf ⊢
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
Goal:
G : Type u_1
inst : Group G
ι : Type u_3
inst_1 : Fintype ι
f : ι → Subgroup G
⊢ index.{u_1} (G := G) (⨅ (i : ι), f i) ≤ ∏ i : ι, (f i).index
have simp_rw : relIndex.{u_1} (G := G) (⨅ (i : ι), f i) ⊤ ≤ ∏ x : ι, (f x).relIndex ⊤
Tactic: simp_rw [← relIndex_top_right, relIndex_iInf_le]
-- Lean 4 proof step from Mathlib.GroupTheory.Index (hypothesis)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
hH : H.index ∣ 2
⊢ H.index = 1 ∨ H.index = 2
have this : H.index ≤ 1 ∨ H.index = Nat.succ 1
Tactic: have := Nat.le_succ_iff.mp (Nat.le_of_dvd two_pos hH)
-- Lean 4 proof step from Mathlib.GroupTheory.Index (hypothesis)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
hH : H.index ∣ 2
this : H.index ≤ 1 ∨ H.index = Nat.succ 1
⊢ H.index = 1 ∨ H.index = 2
have this₁ : H.index = 0 ∨ H.index = 1 ∨ H.index = Nat.succ 1
Tactic: rw [Nat.le_one_iff_eq_zero_or_eq_one, or_assoc] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
hH : H.index ∣ 2
⊢ ∃ (a : G), ∀ (b : G), b * a ∈ H ∨ b ∈ H
have inl : ∀ (hH : H.index = 1), ∃ (a : G), ∀ (b : G), b * a ∈ H ∨ b ∈ H
Tactic: obtain (hH | hH) : H.index = 1 ∨ H.index = 2 := by
      -- This is just showing that 2 is prime, but we do it "longhand" to avoid making any
      -- dependence on number theory files.
      have := Nat.le_succ_iff.mp (Nat.le_of_dvd two_pos hH)
      rw [Nat.le_one_iff_eq_zero_or_eq_one, or_assoc] at this
      exact this.resolve_left fun h ↦ (two_ne_zero <| Nat.zero_dvd.mp (h ▸ hH)).elim
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
hH : H.index ∣ 2
inl : ∀ (hH : H.index = 1), ∃ (a : G), ∀ (b : G), b * a ∈ H ∨ b ∈ H
⊢ ∃ (a : G), ∀ (b : G), b * a ∈ H ∨ b ∈ H
have inr : ∀ (hH : H.index = 2), ∃ (a : G), ∀ (b : G), b * a ∈ H ∨ b ∈ H
Tactic: obtain (hH | hH) : H.index = 1 ∨ H.index = 2 := by
      -- This is just showing that 2 is prime, but we do it "longhand" to avoid making any
      -- dependence on number theory files.
      have := Nat.le_succ_iff.mp (Nat.le_of_dvd two_pos hH)
      rw [Nat.le_one_iff_eq_zero_or_eq_one, or_assoc] at this
      exact this.resolve_left fun h ↦ (two_ne_zero <| Nat.zero_dvd.mp (h ▸ hH)).elim
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
a : G
ha : ∀ (b : G), b * a ∈ H ∨ b ∈ H
⊢ H.index ∣ 2
have pos : ∀ (ha' : a ∈ H), H.index ∣ 2
Tactic: by_cases ha' : a ∈ H
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
a : G
ha : ∀ (b : G), b * a ∈ H ∨ b ∈ H
pos : ∀ (ha' : a ∈ H), H.index ∣ 2
⊢ H.index ∣ 2
have neg : ∀ (ha' : a ∉ H), H.index ∣ 2
Tactic: by_cases ha' : a ∈ H
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
a : G
ha : ∀ (b : G), b * a ∈ H ∨ b ∈ H
ha' : a ∈ H
⊢ H.index ∣ 2
have pos : ∀ (b : G), b ∈ H
Tactic: suffices ∀ b, b ∈ H by simp [(eq_top_iff' _).mpr this]
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
a : G
ha : ∀ (b : G), b * a ∈ H ∨ b ∈ H
ha' : a ∉ H
⊢ H.index ∣ 2
have neg : ∀ (b : G) (h : b * a ∈ H ∧ b ∈ H), a ∈ H
Tactic: refine dvd_of_eq (index_eq_two_iff.mpr
        ⟨a, fun b ↦ (xor_iff_or_and_not_and _ _).mpr ⟨ha b, fun h ↦ ha' ?_⟩⟩)
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
⊢ H.index ∣ 2 ↔ ∃ (a : G), ∀ (b : G), a * b ∈ H ∨ b ∈ H
have rw : ∀ (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: rw [index_dvd_two_iff, (Equiv.inv G).exists_congr]
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup 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
have 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)
Tactic: refine fun a ↦ (Equiv.inv G).forall_congr fun b ↦ ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
hH : Finite.{u_1 + 1} (G ⧸ H)
⊢ H.index ≠ 0
have intro : ∀ (val : Fintype (G ⧸ H)), H.index ≠ 0
Tactic: cases nonempty_fintype (G ⧸ H)
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
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
⊢ Finite.{u_3 + 1} (MulAction.orbitRel.Quotient.{u_1, u_3} (↥H) X)
have have : ∀ (this : Fintype (G ⧸ H)), Finite.{u_3 + 1} (MulAction.orbitRel.Quotient.{u_1, u_3} (↥H) X)
Tactic: have := fintypeOfIndexNeZero hi
-- Lean 4 proof step from Mathlib.GroupTheory.Index (hypothesis)
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
⊢ Finite.{u_3 + 1} (MulAction.orbitRel.Quotient.{u_1, u_3} (↥H) X)
have this : Subsingleton.{u_3 + 1} (MulAction.orbitRel.Quotient G X)
Tactic: have := (MulAction.pretransitive_iff_subsingleton_quotient G X).1 inferInstance
-- 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
this : ∃ (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
have 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
Tactic: rcases this with ⟨n₁, n₂, hlt, hle, he⟩
Cleared hypotheses: this
-- 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₂ : ℕ
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
have refine : a ^ (n₂ - n₁) ∈ H
Tactic: refine ⟨n₂ - n₁, by lia, by lia, ?_⟩
-- 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
n₁ n₂ : ℕ
hlt : n₁ < n₂
hle : n₂ ≤ H.index
he : Eq (α := G ⧸ H) (↑(a ^ n₂) : G ⧸ H) (↑(a ^ n₁) : G ⧸ H)
⊢ a ^ (n₂ - n₁) ∈ H
have he₁ : a ^ HAdd.hAdd (α := ℤ) (↑n₂ : ℤ) (-(↑n₁ : ℤ)) ∈ H
Tactic: rw [eq_comm, QuotientGroup.eq, ← zpow_natCast, ← zpow_natCast, ← zpow_neg, ← zpow_add,
        add_comm] at he
Cleared hypotheses: 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₁ n₂ : ℕ
hlt : n₁ < n₂
hle : n₂ ≤ H.index
he : a ^ HAdd.hAdd (α := ℤ) (↑n₂ : ℤ) (-(↑n₁ : ℤ)) ∈ H
⊢ a ^ (n₂ - n₁) ∈ H
have rw : HPow.hPow (β := ℤ) a (↑(n₂ - n₁) : ℤ) ∈ H
Tactic: rw [← zpow_natCast]
-- 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₂ : ℕ
hlt : n₁ < n₂
hle : n₂ ≤ H.index
he : a ^ HAdd.hAdd (α := ℤ) (↑n₂ : ℤ) (-(↑n₁ : ℤ)) ∈ H
⊢ HPow.hPow (β := ℤ) a (↑(n₂ - n₁) : ℤ) ∈ H
have h₁ : (↑(n₂ - n₁) : ℤ) = HAdd.hAdd (α := ℤ) (↑n₂ : ℤ) (-(↑n₁ : ℤ))
Tactic: convert! 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 : ℕ), 0 < n ∧ n ≤ H.index ∧ a ^ n ∈ H
have suffices : ∃ (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 ∧ ((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
-- 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
this :
  ∃ (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)
have 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)
Tactic: rcases this with ⟨n₁, n₂, hne, hle₁, hle₂, he⟩
Cleared hypotheses: this
-- 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₂ : ℕ
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)
have inl : ∀ (hlt : n₁ < n₂), ∃ (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
-- 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₂ : ℕ
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)
⊢ ∃ (n₁ : ℕ) (n₂ : ℕ), n₁ < n₂ ∧ n₂ ≤ H.index ∧ Eq (α := G ⧸ H) (↑(a ^ n₂) : G ⧸ H) (↑(a ^ n₁) : G ⧸ H)
have inr : ∀ (hlt : n₂ < n₁), ∃ (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
-- 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 ∧ Eq (α := G ⧸ H) (↑(a ^ n₂) : G ⧸ H) (↑(a ^ n₁) : G ⧸ H)
have suffices : ∃ (n₁ : ℕ) (n₂ : ℕ), n₁ ≠ n₂ ∧ n₁ ≤ H.index ∧ 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⟩