awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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_2 + 1, u_1 + 1} (α := G') (β := G) (⇑f : (a : G') → G)
key :
  ∀ (x y : G'),
    (QuotientGroup.leftRel (comap f H) : G' → G' → Prop) x y ↔
      (QuotientGroup.leftRel H : G → G → Prop) ((f : (a : G') → G) x : G) ((f : (a : G') → G) y : G)
x : G
⊢ ∃ (a : G' ⧸ comap f H), Eq (α := G ⧸ H) (Quotient.map' (⇑f : (a : G') → G) ⋯ a) (Quotient.mk'' x)
have refine_2 : ∀ (y : G') (hy : (f : (a : G') → G) y = x),
  ∃ (a : G' ⧸ comap f H), Eq (α := G ⧸ H) (Quotient.map' (⇑f : (a : G') → G) sorry a) (Quotient.mk'' x)
Tactic: obtain ⟨y, hy⟩ := hf x
-- 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
K : Subgroup G'
⊢ (comap f H).relIndex K = H.relIndex (map f K)
have rw : ((comap f H).subgroupOf K).index = H.relIndex (map f K)
Tactic: rw [relIndex, subgroupOf, comap_comap, index_comap, ← f.map_range, K.range_subtype]
-- 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
K : Subgroup G'
rw : ((comap f H).subgroupOf K).index = H.relIndex (map f K)
⊢ (comap f H).relIndex K = H.relIndex (map f K)
have rw₁ : (comap K.subtype (comap f H)).index = H.relIndex (map f K)
Tactic: rw [relIndex, subgroupOf, comap_comap, index_comap, ← f.map_range, K.range_subtype]
-- 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
K : Subgroup G'
rw : ((comap f H).subgroupOf K).index = H.relIndex (map f K)
rw₁ : (comap K.subtype (comap f H)).index = H.relIndex (map f K)
⊢ (comap f H).relIndex K = H.relIndex (map f K)
have rw₂ : (comap (f.comp K.subtype) H).index = H.relIndex (map f K)
Tactic: rw [relIndex, subgroupOf, comap_comap, index_comap, ← f.map_range, K.range_subtype]
-- 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
K : Subgroup G'
rw : ((comap f H).subgroupOf K).index = H.relIndex (map f K)
rw₁ : (comap K.subtype (comap f H)).index = H.relIndex (map f K)
rw₂ : (comap (f.comp K.subtype) H).index = H.relIndex (map f K)
⊢ (comap f H).relIndex K = H.relIndex (map f K)
have rw₃ : H.relIndex (f.comp K.subtype).range = H.relIndex (map f K)
Tactic: rw [relIndex, subgroupOf, comap_comap, index_comap, ← f.map_range, K.range_subtype]
-- 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
K : Subgroup G'
rw : ((comap f H).subgroupOf K).index = H.relIndex (map f K)
rw₁ : (comap K.subtype (comap f H)).index = H.relIndex (map f K)
rw₂ : (comap (f.comp K.subtype) H).index = H.relIndex (map f K)
rw₃ : H.relIndex (f.comp K.subtype).range = H.relIndex (map f K)
⊢ (comap f H).relIndex K = H.relIndex (map f K)
have rw₄ : H.relIndex (map f K.subtype.range) = H.relIndex (map f K)
Tactic: rw [relIndex, subgroupOf, comap_comap, index_comap, ← f.map_range, K.range_subtype]
-- 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
K : Subgroup G'
rw : ((comap f H).subgroupOf K).index = H.relIndex (map f K)
rw₁ : (comap K.subtype (comap f H)).index = H.relIndex (map f K)
rw₂ : (comap (f.comp K.subtype) H).index = H.relIndex (map f K)
rw₃ : H.relIndex (f.comp K.subtype).range = H.relIndex (map f K)
rw₄ : H.relIndex (map f K.subtype.range) = H.relIndex (map f K)
⊢ (comap f H).relIndex K = H.relIndex (map f K)
have rw₅ : H.relIndex (map f K) = H.relIndex (map f K)
Tactic: rw [relIndex, subgroupOf, comap_comap, index_comap, ← f.map_range, K.range_subtype]
-- 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'
H K : Subgroup G
hf : Injective.{u_1 + 1, u_2 + 1} (α := G) (β := G') (⇑f : (a : G) → G')
⊢ (map f H).relIndex (map f K) = H.relIndex K
have rw : (comap f (map f H)).relIndex K = H.relIndex K
Tactic: rw [← Subgroup.relIndex_comap, Subgroup.comap_map_eq_self_of_injective 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'
H K : Subgroup G
hf : Injective.{u_1 + 1, u_2 + 1} (α := G) (β := G') (⇑f : (a : G) → G')
rw : (comap f (map f H)).relIndex K = H.relIndex K
⊢ (map f H).relIndex (map f K) = H.relIndex K
have rw₁ : H.relIndex K = H.relIndex K
Tactic: rw [← Subgroup.relIndex_comap, Subgroup.comap_map_eq_self_of_injective 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'
H K : Subgroup G
⊢ (map f H).relIndex (map f K) = (H ⊔ f.ker).relIndex (K ⊔ f.ker)
have rw : (map f H).relIndex (map f K) = (comap f (map f H)).relIndex (K ⊔ f.ker)
Tactic: rw [← comap_map_eq, ← comap_map_eq, relIndex_comap, (gc_map_comap f).l_u_l_eq_l]
-- 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'
H K : Subgroup G
rw : (map f H).relIndex (map f K) = (comap f (map f H)).relIndex (K ⊔ f.ker)
⊢ (map f H).relIndex (map f K) = (H ⊔ f.ker).relIndex (K ⊔ f.ker)
have rw₁ : (map f H).relIndex (map f K) = (comap f (map f H)).relIndex (comap f (map f K))
Tactic: rw [← comap_map_eq, ← comap_map_eq, relIndex_comap, (gc_map_comap f).l_u_l_eq_l]
-- 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'
H K : Subgroup G
rw : (map f H).relIndex (map f K) = (comap f (map f H)).relIndex (K ⊔ f.ker)
rw₁ : (map f H).relIndex (map f K) = (comap f (map f H)).relIndex (comap f (map f K))
⊢ (map f H).relIndex (map f K) = (H ⊔ f.ker).relIndex (K ⊔ f.ker)
have rw₂ : (map f H).relIndex (map f K) = (map f H).relIndex (map f (comap f (map f K)))
Tactic: rw [← comap_map_eq, ← comap_map_eq, relIndex_comap, (gc_map_comap f).l_u_l_eq_l]
-- 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'
H K : Subgroup G
rw : (map f H).relIndex (map f K) = (comap f (map f H)).relIndex (K ⊔ f.ker)
rw₁ : (map f H).relIndex (map f K) = (comap f (map f H)).relIndex (comap f (map f K))
rw₂ : (map f H).relIndex (map f K) = (map f H).relIndex (map f (comap f (map f K)))
⊢ (map f H).relIndex (map f K) = (H ⊔ f.ker).relIndex (K ⊔ f.ker)
have rw₃ : (map f H).relIndex (map f K) = (map f H).relIndex (map f K)
Tactic: rw [← comap_map_eq, ← comap_map_eq, relIndex_comap, (gc_map_comap f).l_u_l_eq_l]
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
h : H ≤ K
⊢ H.relIndex K * K.index = H.index
have rw : K.index * H.relIndex K = H.index
Tactic: rw [mul_comm]
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
h : H ≤ K
⊢ K.index * H.relIndex K = H.index
have simp_rw : K.index * (H.subgroupOf K).index = H.index
Tactic: simp_rw [relIndex, index, ← Nat.card_prod, Nat.card_congr <| quotientEquivProdOfLE h]
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
h : H ≤ K
simp_rw : K.index * (H.subgroupOf K).index = H.index
⊢ K.index * H.relIndex K = H.index
have simp_rw₁ : Nat.card.{u_1} (G ⧸ K) * Nat.card.{u_1} (↥K ⧸ H.subgroupOf K) = Nat.card.{u_1} (G ⧸ H)
Tactic: simp_rw [relIndex, index, ← Nat.card_prod, Nat.card_congr <| quotientEquivProdOfLE h]
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
h : H ≤ K
simp_rw : K.index * (H.subgroupOf K).index = H.index
simp_rw₁ : Nat.card.{u_1} (G ⧸ K) * Nat.card.{u_1} (↥K ⧸ H.subgroupOf K) = Nat.card.{u_1} (G ⧸ H)
⊢ K.index * H.relIndex K = H.index
have simp_rw₂ : Nat.card.{u_1} ((G ⧸ K) × ↥K ⧸ H.subgroupOf K) = Nat.card.{u_1} (G ⧸ H)
Tactic: simp_rw [relIndex, index, ← Nat.card_prod, Nat.card_congr <| quotientEquivProdOfLE h]
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
Goal:
G : Type u_1
inst : Group G
H K L : Subgroup G
hHK : H ≤ K
hKL : K ≤ L
⊢ H.relIndex K * K.relIndex L = H.relIndex L
have rw : (H.subgroupOf L).relIndex (K.subgroupOf L) * K.relIndex L = H.relIndex L
Tactic: rw [← relIndex_subgroupOf hKL]
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
⊢ (H ⊓ K).relIndex K = H.relIndex K
have rw : ((H ⊓ K).subgroupOf K).index = H.relIndex K
Tactic: rw [relIndex, relIndex, inf_subgroupOf_right]
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
rw : ((H ⊓ K).subgroupOf K).index = H.relIndex K
⊢ (H ⊓ K).relIndex K = H.relIndex K
have rw₁ : ((H ⊓ K).subgroupOf K).index = (H.subgroupOf K).index
Tactic: rw [relIndex, relIndex, inf_subgroupOf_right]
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
rw : ((H ⊓ K).subgroupOf K).index = H.relIndex K
rw₁ : ((H ⊓ K).subgroupOf K).index = (H.subgroupOf K).index
⊢ (H ⊓ K).relIndex K = H.relIndex K
have rw₂ : (H.subgroupOf K).index = (H.subgroupOf K).index
Tactic: rw [relIndex, relIndex, inf_subgroupOf_right]
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
⊢ (H ⊓ K).relIndex H = K.relIndex H
have rw : (K ⊓ H).relIndex H = K.relIndex H
Tactic: rw [inf_comm, inf_relIndex_right]
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
rw : (K ⊓ H).relIndex H = K.relIndex H
⊢ (H ⊓ K).relIndex H = K.relIndex H
have rw₁ : K.relIndex H = K.relIndex H
Tactic: rw [inf_comm, 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.relIndex (K ⊓ L) * K.relIndex L = (H ⊓ K).relIndex L
have rw : (H ⊓ (K ⊓ L)).relIndex (K ⊓ L) * K.relIndex L = (H ⊓ K).relIndex L
Tactic: rw [← inf_relIndex_right H (K ⊓ L), ← inf_relIndex_right K L, ← inf_relIndex_right (H ⊓ K) L,
    inf_assoc, relIndex_mul_relIndex (H ⊓ (K ⊓ L)) (K ⊓ L) L inf_le_right inf_le_right]
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
Goal:
G : Type u_1
inst : Group G
H K L : Subgroup G
rw : (H ⊓ (K ⊓ L)).relIndex (K ⊓ L) * K.relIndex L = (H ⊓ K).relIndex L
⊢ H.relIndex (K ⊓ L) * K.relIndex L = (H ⊓ K).relIndex L
have rw₁ : (H ⊓ (K ⊓ L)).relIndex (K ⊓ L) * (K ⊓ L).relIndex L = (H ⊓ K).relIndex L
Tactic: rw [← inf_relIndex_right H (K ⊓ L), ← inf_relIndex_right K L, ← inf_relIndex_right (H ⊓ K) L,
    inf_assoc, relIndex_mul_relIndex (H ⊓ (K ⊓ L)) (K ⊓ L) L inf_le_right inf_le_right]
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
Goal:
G : Type u_1
inst : Group G
H K L : Subgroup G
rw : (H ⊓ (K ⊓ L)).relIndex (K ⊓ L) * K.relIndex L = (H ⊓ K).relIndex L
rw₁ : (H ⊓ (K ⊓ L)).relIndex (K ⊓ L) * (K ⊓ L).relIndex L = (H ⊓ K).relIndex L
⊢ H.relIndex (K ⊓ L) * K.relIndex L = (H ⊓ K).relIndex L
have rw₂ : (H ⊓ (K ⊓ L)).relIndex (K ⊓ L) * (K ⊓ L).relIndex L = (H ⊓ K ⊓ L).relIndex L
Tactic: rw [← inf_relIndex_right H (K ⊓ L), ← inf_relIndex_right K L, ← inf_relIndex_right (H ⊓ K) L,
    inf_assoc, relIndex_mul_relIndex (H ⊓ (K ⊓ L)) (K ⊓ L) L inf_le_right inf_le_right]
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
Goal:
G : Type u_1
inst : Group G
H K L : Subgroup G
rw : (H ⊓ (K ⊓ L)).relIndex (K ⊓ L) * K.relIndex L = (H ⊓ K).relIndex L
rw₁ : (H ⊓ (K ⊓ L)).relIndex (K ⊓ L) * (K ⊓ L).relIndex L = (H ⊓ K).relIndex L
rw₂ : (H ⊓ (K ⊓ L)).relIndex (K ⊓ L) * (K ⊓ L).relIndex L = (H ⊓ K ⊓ L).relIndex L
⊢ H.relIndex (K ⊓ L) * K.relIndex L = (H ⊓ K).relIndex L
have rw₃ : (H ⊓ (K ⊓ L)).relIndex (K ⊓ L) * (K ⊓ L).relIndex L = (H ⊓ (K ⊓ L)).relIndex L
Tactic: rw [← inf_relIndex_right H (K ⊓ L), ← inf_relIndex_right K L, ← inf_relIndex_right (H ⊓ K) L,
    inf_assoc, relIndex_mul_relIndex (H ⊓ (K ⊓ L)) (K ⊓ L) L inf_le_right inf_le_right]
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
Goal:
G : Type u_1
inst : Group G
H K L : Subgroup G
rw : (H ⊓ (K ⊓ L)).relIndex (K ⊓ L) * K.relIndex L = (H ⊓ K).relIndex L
rw₁ : (H ⊓ (K ⊓ L)).relIndex (K ⊓ L) * (K ⊓ L).relIndex L = (H ⊓ K).relIndex L
rw₂ : (H ⊓ (K ⊓ L)).relIndex (K ⊓ L) * (K ⊓ L).relIndex L = (H ⊓ K ⊓ L).relIndex L
rw₃ : (H ⊓ (K ⊓ L)).relIndex (K ⊓ L) * (K ⊓ L).relIndex L = (H ⊓ (K ⊓ L)).relIndex L
⊢ H.relIndex (K ⊓ L) * K.relIndex L = (H ⊓ K).relIndex L
have rw₄ : (H ⊓ (K ⊓ L)).relIndex L = (H ⊓ (K ⊓ L)).relIndex L
Tactic: rw [← inf_relIndex_right H (K ⊓ L), ← inf_relIndex_right K L, ← inf_relIndex_right (H ⊓ K) L,
    inf_assoc, relIndex_mul_relIndex (H ⊓ (K ⊓ L)) (K ⊓ L) L inf_le_right inf_le_right]
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
inst_1 : K.Normal
⊢ K.relIndex (K ⊔ H) = K.relIndex H
have rw : K.relIndex (H ⊔ K) = K.relIndex H
Tactic: rw [sup_comm, relIndex_sup_right]
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
inst_1 : K.Normal
rw : K.relIndex (H ⊔ K) = K.relIndex H
⊢ K.relIndex (K ⊔ H) = K.relIndex H
have rw₁ : K.relIndex H = K.relIndex H
Tactic: rw [sup_comm, relIndex_sup_right]
-- 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), Xor (b * a ∈ H) (b ∈ H)
have simp : (∃ x ∉ H, ∀ x_1 ∉ H, x_1⁻¹ * x ∈ H) ↔ ∃ (a : G), ∀ (b : G), b * a ∈ H ↔ b ∉ H
Tactic: simp only [index, Nat.card_eq_two_iff' ((1 : G) : G ⧸ H), ExistsUnique, inv_mem_iff,
    QuotientGroup.exists_mk, QuotientGroup.forall_mk, Ne, QuotientGroup.eq, mul_one,
    xor_iff_iff_not]
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
⊢ (∃ x ∉ H, ∀ x_1 ∉ H, x_1⁻¹ * x ∈ H) ↔ ∃ (a : G), ∀ (b : G), b * a ∈ H ↔ b ∉ H
have refine_1 : ∀ (a : G) (ha : a ∉ H ∧ ∀ x ∉ H, x⁻¹ * a ∈ H) (b : G) (hba : b * a ∈ H) (hb : b ∈ H), False
Tactic: refine exists_congr fun a =>
    ⟨fun ha b => ⟨fun hba hb => ?_, fun hb => ?_⟩, fun ha => ⟨?_, fun b hb => ?_⟩⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
refine_1 : ∀ (a : G) (ha : a ∉ H ∧ ∀ x ∉ H, x⁻¹ * a ∈ H) (b : G) (hba : b * a ∈ H) (hb : b ∈ H), False
⊢ (∃ x ∉ H, ∀ x_1 ∉ H, x_1⁻¹ * x ∈ H) ↔ ∃ (a : G), ∀ (b : G), b * a ∈ H ↔ b ∉ H
have refine_2 : ∀ (a : G) (ha : a ∉ H ∧ ∀ x ∉ H, x⁻¹ * a ∈ H) (b : G) (hb : b ∉ H), b * a ∈ H
Tactic: refine exists_congr fun a =>
    ⟨fun ha b => ⟨fun hba hb => ?_, fun hb => ?_⟩, fun ha => ⟨?_, fun b hb => ?_⟩⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
refine_1 : ∀ (a : G) (ha : a ∉ H ∧ ∀ x ∉ H, x⁻¹ * a ∈ H) (b : G) (hba : b * a ∈ H) (hb : b ∈ H), False
refine_2 : ∀ (a : G) (ha : a ∉ H ∧ ∀ x ∉ H, x⁻¹ * a ∈ H) (b : G) (hb : b ∉ H), b * a ∈ H
⊢ (∃ x ∉ H, ∀ x_1 ∉ H, x_1⁻¹ * x ∈ H) ↔ ∃ (a : G), ∀ (b : G), b * a ∈ H ↔ b ∉ H
have refine_3 : ∀ (a : G) (ha : ∀ (b : G), b * a ∈ H ↔ b ∉ H), a ∉ H
Tactic: refine exists_congr fun a =>
    ⟨fun ha b => ⟨fun hba hb => ?_, fun hb => ?_⟩, fun ha => ⟨?_, fun b hb => ?_⟩⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
refine_1 : ∀ (a : G) (ha : a ∉ H ∧ ∀ x ∉ H, x⁻¹ * a ∈ H) (b : G) (hba : b * a ∈ H) (hb : b ∈ H), False
refine_2 : ∀ (a : G) (ha : a ∉ H ∧ ∀ x ∉ H, x⁻¹ * a ∈ H) (b : G) (hb : b ∉ H), b * a ∈ H
refine_3 : ∀ (a : G) (ha : ∀ (b : G), b * a ∈ H ↔ b ∉ H), a ∉ H
⊢ (∃ x ∉ H, ∀ x_1 ∉ H, x_1⁻¹ * x ∈ H) ↔ ∃ (a : G), ∀ (b : G), b * a ∈ H ↔ b ∉ H
have refine_4 : ∀ (a : G) (ha : ∀ (b : G), b * a ∈ H ↔ b ∉ H) (b : G) (hb : b ∉ H), b⁻¹ * a ∈ H
Tactic: refine exists_congr fun a =>
    ⟨fun ha b => ⟨fun hba hb => ?_, fun hb => ?_⟩, fun ha => ⟨?_, fun b hb => ?_⟩⟩
-- 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
⊢ a ∉ H
have refine_3 : 1 ∈ H
Tactic: rw [← inv_mem_iff (x := a), ← ha, inv_mul_cancel]
-- 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
b : G
hb : b ∉ H
⊢ b⁻¹ * a ∈ H
have refine_4 : b⁻¹ ∉ H
Tactic: rwa [ha, inv_mem_iff (x := b)]
-- 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), Xor (a * b ∈ H) (b ∈ H)
have rw : ∀ (a : G),
  (∀ (b : G), Xor (b * a ∈ H) (b ∈ H)) ↔
    ∀ (b : G), Xor (HMul.hMul (α := G) ((Equiv.inv G : (a : G) → G) a : G) b ∈ H) (b ∈ H)
Tactic: rw [index_eq_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), Xor (b * a ∈ H) (b ∈ H)) ↔
      ∀ (b : G), Xor (HMul.hMul (α := G) ((Equiv.inv G : (a : G) → G) a : G) b ∈ H) (b ∈ H)
have refine : ∀ (a b : G),
  Xor (b * a ∈ H) (b ∈ H) ↔
    Xor (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
⊢ H.index = 2 ↔ ∃ a ∉ H, ∀ (b : G), b * a ∈ H ∨ b ∈ H
have simp : (∃ (a : G), ∀ (b : G), (b * a ∈ H ∨ b ∈ H) ∧ ¬(b * a ∈ H ∧ b ∈ H)) ↔ ∃ a ∉ H, ∀ (b : G), b * a ∈ H ∨ b ∈ H
Tactic: simp only [index_eq_two_iff, xor_iff_or_and_not_and]
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
⊢ H.index = 2 ↔ ∃ a ∉ H, ∀ (b : G), a * b ∈ H ∨ b ∈ H
have simp : (∃ (a : G), ∀ (b : G), (a * b ∈ H ∨ b ∈ H) ∧ ¬(a * b ∈ H ∧ b ∈ H)) ↔ ∃ a ∉ H, ∀ (b : G), a * b ∈ H ∨ b ∈ H
Tactic: simp only [index_eq_two_iff', xor_iff_or_and_not_and]
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
⊢ H.relIndex K = 2 ↔ ∃ a ∈ K, a ∉ H ∧ ∀ b ∈ K, b * a ∈ H ∨ b ∈ H
have rw : (∃ a ∉ H.subgroupOf K, ∀ (b : ↥K), b * a ∈ H.subgroupOf K ∨ b ∈ H.subgroupOf K) ↔
  ∃ a ∈ K, a ∉ H ∧ ∀ b ∈ K, b * a ∈ H ∨ b ∈ H
Tactic: rw [Subgroup.relIndex, Subgroup.index_eq_two_iff_exists_notMem_and]
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
⊢ (∃ a ∉ H.subgroupOf K, ∀ (b : ↥K), b * a ∈ H.subgroupOf K ∨ b ∈ H.subgroupOf K) ↔
    ∃ a ∈ K, a ∉ H ∧ ∀ b ∈ K, b * a ∈ H ∨ b ∈ H
have simp : (∃ a ∉ H, a ∈ K ∧ ∀ (a_1 : G) (b : a_1 ∈ K), a_1 * a ∈ H ∨ a_1 ∈ H) ↔ ∃ a ∈ K, a ∉ H ∧ ∀ b ∈ K, b * a ∈ H ∨ b ∈ H
Tactic: simp only [mem_subgroupOf, coe_mul, Subtype.forall, Subtype.exists, exists_and_left, exists_prop]
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
⊢ (∃ a ∉ H, a ∈ K ∧ ∀ (a_1 : G) (b : a_1 ∈ K), a_1 * a ∈ H ∨ a_1 ∈ H) ↔ ∃ a ∈ K, a ∉ H ∧ ∀ b ∈ K, b * a ∈ H ∨ b ∈ H
have refine : ∀ (g : G), (g ∉ H ∧ g ∈ K ∧ ∀ (a : G) (b : a ∈ K), a * g ∈ H ∨ a ∈ H) ↔ g ∈ K ∧ g ∉ H ∧ ∀ b ∈ K, b * g ∈ H ∨ b ∈ H
Tactic: refine exists_congr fun g ↦ ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
⊢ H.relIndex K = 2 ↔ ∃ a ∈ K, a ∉ H ∧ ∀ b ∈ K, a * b ∈ H ∨ b ∈ H
have rw : (∃ a ∉ H.subgroupOf K, ∀ (b : ↥K), a * b ∈ H.subgroupOf K ∨ b ∈ H.subgroupOf K) ↔
  ∃ a ∈ K, a ∉ H ∧ ∀ b ∈ K, a * b ∈ H ∨ b ∈ H
Tactic: rw [Subgroup.relIndex, Subgroup.index_eq_two_iff_exists_notMem_and']
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
⊢ (∃ a ∉ H.subgroupOf K, ∀ (b : ↥K), a * b ∈ H.subgroupOf K ∨ b ∈ H.subgroupOf K) ↔
    ∃ a ∈ K, a ∉ H ∧ ∀ b ∈ K, a * b ∈ H ∨ b ∈ H
have simp : (∃ a ∉ H, a ∈ K ∧ ∀ (a_1 : G) (b : a_1 ∈ K), a * a_1 ∈ H ∨ a_1 ∈ H) ↔ ∃ a ∈ K, a ∉ H ∧ ∀ b ∈ K, a * b ∈ H ∨ b ∈ H
Tactic: simp only [mem_subgroupOf, coe_mul, Subtype.forall, Subtype.exists, exists_and_left, exists_prop]
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
⊢ (∃ a ∉ H, a ∈ K ∧ ∀ (a_1 : G) (b : a_1 ∈ K), a * a_1 ∈ H ∨ a_1 ∈ H) ↔ ∃ a ∈ K, a ∉ H ∧ ∀ b ∈ K, a * b ∈ H ∨ b ∈ H
have refine : ∀ (g : G), (g ∉ H ∧ g ∈ K ∧ ∀ (a : G) (b : a ∈ K), g * a ∈ H ∨ a ∈ H) ↔ g ∈ K ∧ g ∉ H ∧ ∀ b ∈ K, g * b ∈ H ∨ b ∈ H
Tactic: refine exists_congr fun g ↦ ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
h : H.index = 2
a b : G
⊢ a * b ∈ H ↔ (a ∈ H ↔ b ∈ H)
have pos : ∀ (ha : a ∈ H), a * b ∈ H ↔ (a ∈ H ↔ b ∈ H)
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
h : H.index = 2
a b : G
pos : ∀ (ha : a ∈ H), a * b ∈ H ↔ (a ∈ H ↔ b ∈ H)
⊢ a * b ∈ H ↔ (a ∈ H ↔ b ∈ H)
have neg : ∀ (ha : a ∉ H), a * b ∈ H ↔ (a ∈ H ↔ b ∈ H)
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
h : H.index = 2
a b : G
ha : a ∉ H
⊢ a * b ∈ H ↔ (a ∈ H ↔ b ∈ H)
have pos : ∀ (hb : b ∈ H), a * b ∈ H ↔ (a ∈ H ↔ b ∈ H)
Tactic: by_cases hb : b ∈ H
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
h : H.index = 2
a b : G
ha : a ∉ H
pos : ∀ (hb : b ∈ H), a * b ∈ H ↔ (a ∈ H ↔ b ∈ H)
⊢ a * b ∈ H ↔ (a ∈ H ↔ b ∈ H)
have neg : ∀ (hb : b ∉ H), a * b ∈ H ↔ (a ∈ H ↔ b ∈ H)
Tactic: by_cases hb : b ∈ H
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
h : H.index = 2
a b : G
ha : a ∉ H
hb : b ∉ H
⊢ a * b ∈ H ↔ (a ∈ H ↔ b ∈ H)
have neg : a * b ∈ H
Tactic: simp only [ha, hb, iff_true]
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
h : H.index = 2
a b : G
ha : a ∉ H
hb : b ∉ H
⊢ a * b ∈ H
have neg : ∀ (c : G) (hc : ∀ (b : G), Xor (b * c ∈ H) (b ∈ H)), a * b ∈ H
Tactic: rcases index_eq_two_iff.1 h with ⟨c, hc⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
h : H.index = 2
a b : G
ha : a ∉ H
hb : b ∉ H
c : G
hc : ∀ (b : G), Xor (b * c ∈ H) (b ∈ H)
⊢ a * b ∈ H
have neg : a * b * c ∉ H
Tactic: refine (hc _).or.resolve_left ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
h : H.index = 2
a b : G
ha : a ∉ H
hb : b ∉ H
c : G
hc : ∀ (b : G), Xor (b * c ∈ H) (b ∈ H)
⊢ a * b * c ∉ H
have neg : a * (b * c) ∉ H
Tactic: rwa [mul_assoc, mul_mem_cancel_right ((hc _).or.resolve_right hb)]
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
h : H.index = 2
a : G
⊢ a * a ∈ H
have rw : a ∈ H ↔ a ∈ H
Tactic: rw [mul_mem_iff_of_index_two h]
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
⊢ H.relIndex ⊤ = H.index
have rw : H.relIndex ⊤ = H.relIndex ⊤ * index.{u_1} (G := G) ⊤
Tactic: rw [← relIndex_mul_index (show H ≤ ⊤ from le_top), index_top, mul_one]
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
rw : H.relIndex ⊤ = H.relIndex ⊤ * index.{u_1} (G := G) ⊤
⊢ H.relIndex ⊤ = H.index
have rw₁ : H.relIndex ⊤ = H.relIndex ⊤ * 1
Tactic: rw [← relIndex_mul_index (show H ≤ ⊤ from le_top), index_top, mul_one]
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
rw : H.relIndex ⊤ = H.relIndex ⊤ * index.{u_1} (G := G) ⊤
rw₁ : H.relIndex ⊤ = H.relIndex ⊤ * 1
⊢ H.relIndex ⊤ = H.index
have rw₂ : H.relIndex ⊤ = H.relIndex ⊤
Tactic: rw [← relIndex_mul_index (show H ≤ ⊤ from le_top), index_top, mul_one]
-- Lean 4 proof step from Mathlib.GroupTheory.Index (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
⊢ relIndex ⊥ H = Nat.card.{u_1} ↥H
have rw : (subgroupOf ⊥ H).index = Nat.card.{u_1} ↥H
Tactic: rw [relIndex, bot_subgroupOf, index_bot]