awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (goal)
Goal:
G : Type u_1
inst : Group G
S : Type u_3
H : Type u_4
inst_1 : Group H
inst_2 : SetLike S H
inst_3 : SubgroupClass S H
s : S
inst_4 : MulAction G H
inst_5 : IsScalarTower G Hᵐᵒᵖ H
a b : G
hab : a • (↑s : Set H) ≠ b • (↑s : Set H)
c : H
hc : c ∈ (↑s : Set H)
d : H
hd : d ∈ (↑s : Set H)
hcd : b • d = a • c
⊢ a • (↑s : Set H) = b • (↑s : Set H)
have rw : a • op c • (↑s : Set H) = b • op c • (↑s : Set H)
Tactic: rw [← op_smul_coe_set hc, ← smul_assoc, ← op_smul, ← hcd, op_smul, smul_assoc, op_smul_coe_set hc,
    op_smul_coe_set hd]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (goal)
Goal:
G : Type u_1
inst : Group G
S : Type u_3
H : Type u_4
inst_1 : Group H
inst_2 : SetLike S H
inst_3 : SubgroupClass S H
s : S
inst_4 : MulAction G H
inst_5 : IsScalarTower G Hᵐᵒᵖ H
a b : G
hab : a • (↑s : Set H) ≠ b • (↑s : Set H)
c : H
hc : c ∈ (↑s : Set H)
d : H
hd : d ∈ (↑s : Set H)
hcd : b • d = a • c
rw : a • op c • (↑s : Set H) = b • op c • (↑s : Set H)
⊢ a • (↑s : Set H) = b • (↑s : Set H)
have rw₁ : (a • op c) • (↑s : Set H) = b • op c • (↑s : Set H)
Tactic: rw [← op_smul_coe_set hc, ← smul_assoc, ← op_smul, ← hcd, op_smul, smul_assoc, op_smul_coe_set hc,
    op_smul_coe_set hd]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (goal)
Goal:
G : Type u_1
inst : Group G
S : Type u_3
H : Type u_4
inst_1 : Group H
inst_2 : SetLike S H
inst_3 : SubgroupClass S H
s : S
inst_4 : MulAction G H
inst_5 : IsScalarTower G Hᵐᵒᵖ H
a b : G
hab : a • (↑s : Set H) ≠ b • (↑s : Set H)
c : H
hc : c ∈ (↑s : Set H)
d : H
hd : d ∈ (↑s : Set H)
hcd : b • d = a • c
rw : a • op c • (↑s : Set H) = b • op c • (↑s : Set H)
rw₁ : (a • op c) • (↑s : Set H) = b • op c • (↑s : Set H)
⊢ a • (↑s : Set H) = b • (↑s : Set H)
have rw₂ : op (a • c) • (↑s : Set H) = b • op c • (↑s : Set H)
Tactic: rw [← op_smul_coe_set hc, ← smul_assoc, ← op_smul, ← hcd, op_smul, smul_assoc, op_smul_coe_set hc,
    op_smul_coe_set hd]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (goal)
Goal:
G : Type u_1
inst : Group G
S : Type u_3
H : Type u_4
inst_1 : Group H
inst_2 : SetLike S H
inst_3 : SubgroupClass S H
s : S
inst_4 : MulAction G H
inst_5 : IsScalarTower G Hᵐᵒᵖ H
a b : G
hab : a • (↑s : Set H) ≠ b • (↑s : Set H)
c : H
hc : c ∈ (↑s : Set H)
d : H
hd : d ∈ (↑s : Set H)
hcd : b • d = a • c
rw : a • op c • (↑s : Set H) = b • op c • (↑s : Set H)
rw₁ : (a • op c) • (↑s : Set H) = b • op c • (↑s : Set H)
rw₂ : op (a • c) • (↑s : Set H) = b • op c • (↑s : Set H)
⊢ a • (↑s : Set H) = b • (↑s : Set H)
have rw₃ : op (b • d) • (↑s : Set H) = b • op c • (↑s : Set H)
Tactic: rw [← op_smul_coe_set hc, ← smul_assoc, ← op_smul, ← hcd, op_smul, smul_assoc, op_smul_coe_set hc,
    op_smul_coe_set hd]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (goal)
Goal:
G : Type u_1
inst : Group G
S : Type u_3
H : Type u_4
inst_1 : Group H
inst_2 : SetLike S H
inst_3 : SubgroupClass S H
s : S
inst_4 : MulAction G H
inst_5 : IsScalarTower G Hᵐᵒᵖ H
a b : G
hab : a • (↑s : Set H) ≠ b • (↑s : Set H)
c : H
hc : c ∈ (↑s : Set H)
d : H
hd : d ∈ (↑s : Set H)
hcd : b • d = a • c
rw : a • op c • (↑s : Set H) = b • op c • (↑s : Set H)
rw₁ : (a • op c) • (↑s : Set H) = b • op c • (↑s : Set H)
rw₂ : op (a • c) • (↑s : Set H) = b • op c • (↑s : Set H)
rw₃ : op (b • d) • (↑s : Set H) = b • op c • (↑s : Set H)
⊢ a • (↑s : Set H) = b • (↑s : Set H)
have rw₄ : (b • op d) • (↑s : Set H) = b • op c • (↑s : Set H)
Tactic: rw [← op_smul_coe_set hc, ← smul_assoc, ← op_smul, ← hcd, op_smul, smul_assoc, op_smul_coe_set hc,
    op_smul_coe_set hd]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (goal)
Goal:
G : Type u_1
inst : Group G
S : Type u_3
H : Type u_4
inst_1 : Group H
inst_2 : SetLike S H
inst_3 : SubgroupClass S H
s : S
inst_4 : MulAction G H
inst_5 : IsScalarTower G Hᵐᵒᵖ H
a b : G
hab : a • (↑s : Set H) ≠ b • (↑s : Set H)
c : H
hc : c ∈ (↑s : Set H)
d : H
hd : d ∈ (↑s : Set H)
hcd : b • d = a • c
rw : a • op c • (↑s : Set H) = b • op c • (↑s : Set H)
rw₁ : (a • op c) • (↑s : Set H) = b • op c • (↑s : Set H)
rw₂ : op (a • c) • (↑s : Set H) = b • op c • (↑s : Set H)
rw₃ : op (b • d) • (↑s : Set H) = b • op c • (↑s : Set H)
rw₄ : (b • op d) • (↑s : Set H) = b • op c • (↑s : Set H)
⊢ a • (↑s : Set H) = b • (↑s : Set H)
have rw₅ : b • op d • (↑s : Set H) = b • op c • (↑s : Set H)
Tactic: rw [← op_smul_coe_set hc, ← smul_assoc, ← op_smul, ← hcd, op_smul, smul_assoc, op_smul_coe_set hc,
    op_smul_coe_set hd]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (goal)
Goal:
G : Type u_1
inst : Group G
S : Type u_3
H : Type u_4
inst_1 : Group H
inst_2 : SetLike S H
inst_3 : SubgroupClass S H
s : S
inst_4 : MulAction G H
inst_5 : IsScalarTower G Hᵐᵒᵖ H
a b : G
hab : a • (↑s : Set H) ≠ b • (↑s : Set H)
c : H
hc : c ∈ (↑s : Set H)
d : H
hd : d ∈ (↑s : Set H)
hcd : b • d = a • c
rw : a • op c • (↑s : Set H) = b • op c • (↑s : Set H)
rw₁ : (a • op c) • (↑s : Set H) = b • op c • (↑s : Set H)
rw₂ : op (a • c) • (↑s : Set H) = b • op c • (↑s : Set H)
rw₃ : op (b • d) • (↑s : Set H) = b • op c • (↑s : Set H)
rw₄ : (b • op d) • (↑s : Set H) = b • op c • (↑s : Set H)
rw₅ : b • op d • (↑s : Set H) = b • op c • (↑s : Set H)
⊢ a • (↑s : Set H) = b • (↑s : Set H)
have rw₆ : b • op d • (↑s : Set H) = b • (↑s : Set H)
Tactic: rw [← op_smul_coe_set hc, ← smul_assoc, ← op_smul, ← hcd, op_smul, smul_assoc, op_smul_coe_set hc,
    op_smul_coe_set hd]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (goal)
Goal:
G : Type u_1
inst : Group G
S : Type u_3
H : Type u_4
inst_1 : Group H
inst_2 : SetLike S H
inst_3 : SubgroupClass S H
s : S
inst_4 : MulAction G H
inst_5 : IsScalarTower G Hᵐᵒᵖ H
a b : G
hab : a • (↑s : Set H) ≠ b • (↑s : Set H)
c : H
hc : c ∈ (↑s : Set H)
d : H
hd : d ∈ (↑s : Set H)
hcd : b • d = a • c
rw : a • op c • (↑s : Set H) = b • op c • (↑s : Set H)
rw₁ : (a • op c) • (↑s : Set H) = b • op c • (↑s : Set H)
rw₂ : op (a • c) • (↑s : Set H) = b • op c • (↑s : Set H)
rw₃ : op (b • d) • (↑s : Set H) = b • op c • (↑s : Set H)
rw₄ : (b • op d) • (↑s : Set H) = b • op c • (↑s : Set H)
rw₅ : b • op d • (↑s : Set H) = b • op c • (↑s : Set H)
rw₆ : b • op d • (↑s : Set H) = b • (↑s : Set H)
⊢ a • (↑s : Set H) = b • (↑s : Set H)
have rw₇ : b • (↑s : Set H) = b • (↑s : Set H)
Tactic: rw [← op_smul_coe_set hc, ← smul_assoc, ← op_smul, ← hcd, op_smul, smul_assoc, op_smul_coe_set hc,
    op_smul_coe_set hd]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (goal)
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
H : Subgroup G
a : X
hH : stabilizer G a ≤ H
⊢ IsBlock G (orbit.{u_1, u_2} (↥H) a)
have rw : ∀ ⦃g : G⦄,
  (g • orbit.{u_1, u_2} (↥H) a ∩ orbit.{u_1, u_2} (↥H) a).Nonempty →
    g • orbit.{u_1, u_2} (↥H) a = orbit.{u_1, u_2} (↥H) a
Tactic: rw [isBlock_iff_smul_eq_of_nonempty]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (goal)
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
H : Subgroup G
a : X
hH : stabilizer G a ≤ H
g : G
h₁ h₂ : ↥H
h : Eq.{u_2 + 1} (α := X) ((fun (x : X) ↦ g • x) ((fun (m : ↥H) ↦ m • a) h₁)) ((fun (m : ↥H) ↦ m • a) h₂)
this : g ∈ H
⊢ g • orbit.{u_1, u_2} (↥H) a = orbit.{u_1, u_2} (↥H) a
have rw : (↑(Subtype.mk (p := fun (x : G) ↦ x ∈ H) g this) : G) • orbit.{u_1, u_2} (↥H) a = orbit.{u_1, u_2} (↥H) a
Tactic: rw [← Subgroup.coe_mk H g this, ← H.toSubmonoid.smul_def, smul_orbit (⟨g, this⟩ : H) a]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (goal)
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
H : Subgroup G
a : X
hH : stabilizer G a ≤ H
g : G
h₁ h₂ : ↥H
h : Eq.{u_2 + 1} (α := X) ((fun (x : X) ↦ g • x) ((fun (m : ↥H) ↦ m • a) h₁)) ((fun (m : ↥H) ↦ m • a) h₂)
this : g ∈ H
rw : (↑(Subtype.mk (p := fun (x : G) ↦ x ∈ H) g this) : G) • orbit.{u_1, u_2} (↥H) a = orbit.{u_1, u_2} (↥H) a
⊢ g • orbit.{u_1, u_2} (↥H) a = orbit.{u_1, u_2} (↥H) a
have rw₁ : Subtype.mk (p := fun (x : G) ↦ x ∈ H) g this • orbit.{u_1, u_2} (↥H) a = orbit.{u_1, u_2} (↥H) a
Tactic: rw [← Subgroup.coe_mk H g this, ← H.toSubmonoid.smul_def, smul_orbit (⟨g, this⟩ : H) a]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (goal)
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
H : Subgroup G
a : X
hH : stabilizer G a ≤ H
g : G
h₁ h₂ : ↥H
h : Eq.{u_2 + 1} (α := X) ((fun (x : X) ↦ g • x) ((fun (m : ↥H) ↦ m • a) h₁)) ((fun (m : ↥H) ↦ m • a) h₂)
this : g ∈ H
rw : (↑(Subtype.mk (p := fun (x : G) ↦ x ∈ H) g this) : G) • orbit.{u_1, u_2} (↥H) a = orbit.{u_1, u_2} (↥H) a
rw₁ : Subtype.mk (p := fun (x : G) ↦ x ∈ H) g this • orbit.{u_1, u_2} (↥H) a = orbit.{u_1, u_2} (↥H) a
⊢ g • orbit.{u_1, u_2} (↥H) a = orbit.{u_1, u_2} (↥H) a
have rw₂ : orbit.{u_1, u_2} (↥H) a = orbit.{u_1, u_2} (↥H) a
Tactic: rw [← Subgroup.coe_mk H g this, ← H.toSubmonoid.smul_def, smul_orbit (⟨g, this⟩ : H) a]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (goal)
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
H : Subgroup G
a : X
hH : stabilizer G a ≤ H
g : G
h₁ h₂ : ↥H
h : Eq.{u_2 + 1} (α := X) ((fun (x : X) ↦ g • x) ((fun (m : ↥H) ↦ m • a) h₁)) ((fun (m : ↥H) ↦ m • a) h₂)
⊢ g • orbit.{u_1, u_2} (↥H) a = orbit.{u_1, u_2} (↥H) a
have suffices : g ∈ H
Tactic: suffices g ∈ H by
    rw [← Subgroup.coe_mk H g this, ← H.toSubmonoid.smul_def, smul_orbit (⟨g, this⟩ : H) a]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (goal)
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
H : Subgroup G
a : X
hH : stabilizer G a ≤ H
g : G
h₁ h₂ : ↥H
h : Eq.{u_2 + 1} (α := X) ((fun (x : X) ↦ g • x) ((fun (m : ↥H) ↦ m • a) h₁)) ((fun (m : ↥H) ↦ m • a) h₂)
⊢ g ∈ H
have rw : (↑h₂⁻¹ : G) * g * (↑h₁ : G) ∈ H
Tactic: rw [← mul_mem_cancel_left h₂⁻¹.2, ← mul_mem_cancel_right h₁.2]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (goal)
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
H : Subgroup G
a : X
hH : stabilizer G a ≤ H
g : G
h₁ h₂ : ↥H
h : Eq.{u_2 + 1} (α := X) ((fun (x : X) ↦ g • x) ((fun (m : ↥H) ↦ m • a) h₁)) ((fun (m : ↥H) ↦ m • a) h₂)
⊢ (↑h₂⁻¹ : G) * g * (↑h₁ : G) ∈ H
have a₁ : Membership.mem (γ := Subgroup G) (stabilizer G a) ((↑h₂⁻¹ : G) * g * (↑h₁ : G))
Tactic: apply hH
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (goal)
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
B : Set X
hB : IsBlock G B
a : X
ha : a ∈ B
g : G
hg : Membership.mem (γ := Subgroup G) (stabilizer G a) g
⊢ a ∈ g • B
have rwa : g • a ∈ g • B
Tactic: rwa [← hg, smul_mem_smul_set_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (goal)
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
B : Set X
inst_2 : IsPretransitive G X
hB : IsBlock G B
a : X
ha : a ∈ B
⊢ orbit.{u_1, u_2} (↥(stabilizer G B)) a = B
have h : ∀ (x : X), x ∈ orbit.{u_1, u_2} (↥(stabilizer G B)) a ↔ x ∈ B
Tactic: ext x
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (goal)
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
B : Set X
inst_2 : IsPretransitive G X
hB : IsBlock G B
a : X
ha : a ∈ B
x : X
⊢ x ∈ orbit.{u_1, u_2} (↥(stabilizer G B)) a ↔ x ∈ B
have h : x ∈ orbit.{u_1, u_2} (↥(stabilizer G B)) a → x ∈ B
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (goal)
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
B : Set X
inst_2 : IsPretransitive G X
hB : IsBlock G B
a : X
ha : a ∈ B
x : X
h : x ∈ orbit.{u_1, u_2} (↥(stabilizer G B)) a → x ∈ B
⊢ x ∈ orbit.{u_1, u_2} (↥(stabilizer G B)) a ↔ x ∈ B
have h₁ : x ∈ B → x ∈ orbit.{u_1, u_2} (↥(stabilizer G B)) a
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (goal)
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
B : Set X
inst_2 : IsPretransitive G X
hB : IsBlock G B
a : X
ha : a ∈ B
k : G
k_mem : Membership.mem (γ := Subgroup G) (stabilizer G B) k
⊢ (fun (m : ↥(stabilizer G B)) ↦ m • a)
      (Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (stabilizer G B) x) k k_mem) ∈
    B
have h : k • a ∈ B
Tactic: simp only [Subgroup.mk_smul]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (goal)
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
B : Set X
inst_2 : IsPretransitive G X
hB : IsBlock G B
a : X
ha : a ∈ B
x : X
hx : x ∈ B
⊢ x ∈ orbit.{u_1, u_2} (↥(stabilizer G B)) a
have h : ∀ (k : G) (hx : k • a ∈ B), k • a ∈ orbit.{u_1, u_2} (↥(stabilizer G B)) a
Tactic: obtain ⟨k, rfl⟩ := exists_smul_eq G a x
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (goal)
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
a : X
H : Subgroup G
hH : stabilizer G a ≤ H
⊢ stabilizer G (orbit.{u_1, u_2} (↥H) a) = H
have h : ∀ (g : G), Membership.mem (γ := Subgroup G) (stabilizer G (orbit.{u_1, u_2} (↥H) a)) g ↔ g ∈ H
Tactic: ext g
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (goal)
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
a : X
H : Subgroup G
hH : stabilizer G a ≤ H
g : G
⊢ Membership.mem (γ := Subgroup G) (stabilizer G (orbit.{u_1, u_2} (↥H) a)) g ↔ g ∈ H
have h : Membership.mem (γ := Subgroup G) (stabilizer G (orbit.{u_1, u_2} (↥H) a)) g → g ∈ H
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (goal)
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
a : X
H : Subgroup G
hH : stabilizer G a ≤ H
g : G
h : Membership.mem (γ := Subgroup G) (stabilizer G (orbit.{u_1, u_2} (↥H) a)) g → g ∈ H
⊢ Membership.mem (γ := Subgroup G) (stabilizer G (orbit.{u_1, u_2} (↥H) a)) g ↔ g ∈ H
have h₁ : g ∈ H → Membership.mem (γ := Subgroup G) (stabilizer G (orbit.{u_1, u_2} (↥H) a)) g
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (goal)
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
a : X
H : Subgroup G
hH : stabilizer G a ≤ H
g : G
hg : Membership.mem (γ := Subgroup G) (stabilizer G (orbit.{u_1, u_2} (↥H) a)) g
⊢ g ∈ H
have h : ∀ (b : ↥H) (h : (fun (x : X) ↦ g • x) ((fun (m : ↥H) ↦ m • a) b) = a), g ∈ H
Tactic: obtain ⟨-, ⟨b, rfl⟩, h⟩ := hg.symm ▸ mem_orbit_self a
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (hypothesis)
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
a : X
H : Subgroup G
hH : stabilizer G a ≤ H
g : G
hg : Membership.mem (γ := Subgroup G) (stabilizer G (orbit.{u_1, u_2} (↥H) a)) g
b : ↥H
h : (fun (x : X) ↦ g • x) ((fun (m : ↥H) ↦ m • a) b) = a
⊢ g ∈ H
have h₁ : Membership.mem (γ := Subgroup G) (stabilizer G a) (g * (↑b : G))
Tactic: simp_rw [H.toSubmonoid.smul_def, ← mul_smul, ← mem_stabilizer_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (goal)
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
a : X
H : Subgroup G
hH : stabilizer G a ≤ H
g : G
hg : g ∈ H
⊢ Membership.mem (γ := Subgroup G) (stabilizer G (orbit.{u_1, u_2} (↥H) a)) g
have h : Subtype.mk (p := fun (x : G) ↦ x ∈ H) g hg • orbit.{u_1, u_2} (↥H) a = orbit.{u_1, u_2} (↥H) a
Tactic: rw [mem_stabilizer_iff, ← Subgroup.coe_mk H g hg, ← Submonoid.smul_def (S := H.toSubmonoid)]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (goal)
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
B_1 : Set X
htGX : IsPretransitive G X
a : X
B : Set X
ha : a ∈ B
hB : IsBlock G B
B' : Set X
ha' : a ∈ B'
hB' : IsBlock G B'
⊢ LE.le.{u_1} (α := (↑(Ici (stabilizer G a)) : Type u_1))
      (({
              toFun := fun (x : { B : Set X // a ∈ B ∧ IsBlock G B }) ↦
                match (motive := { B : Set X // a ∈ B ∧ IsBlock G B } → (↑(Ici (stabilizer G a)) : Type u_1)) x with
                | ⟨B, ⋯⟩ =>
                  Subtype.mk (p := fun (x : Subgroup G) ↦
                    Membership.mem (γ := Set (Subgroup G)) (Ici (stabilizer G a)) x) (stabilizer G B) ⋯,
              invFun := fun (x : (↑(Ici (stabilizer G a)) : Type u_1)) ↦
                match (motive := (↑(Ici (stabilizer G a)) : Type u_1) → { B : Set X // a ∈ B ∧ IsBlock G B }) x with
                | ⟨H, hH⟩ => Subtype.mk (p := fun (B : Set X) ↦ a ∈ B ∧ IsBlock G B) (orbit.{u_1, u_2} (↥H) a) ⋯,
              left_inv := ⋯, right_inv := ⋯ } :
            (a_1 : { B : Set X // a ∈ B ∧ IsBlock G B }) → (↑(Ici (stabilizer G a)) : Type u_1))
          (Subtype.mk (p := fun (B : Set X) ↦ a ∈ B ∧ IsBlock G B) B ⋯) :
        (↑(Ici (stabilizer G a)) : Type u_1))
      (({
              toFun := fun (x : { B : Set X // a ∈ B ∧ IsBlock G B }) ↦
                match (motive := { B : Set X // a ∈ B ∧ IsBlock G B } → (↑(Ici (stabilizer G a)) : Type u_1)) x with
                | ⟨B, ⋯⟩ =>
                  Subtype.mk (p := fun (x : Subgroup G) ↦
                    Membership.mem (γ := Set (Subgroup G)) (Ici (stabilizer G a)) x) (stabilizer G B) ⋯,
              invFun := fun (x : (↑(Ici (stabilizer G a)) : Type u_1)) ↦
                match (motive := (↑(Ici (stabilizer G a)) : Type u_1) → { B : Set X // a ∈ B ∧ IsBlock G B }) x with
                | ⟨H, hH⟩ => Subtype.mk (p := fun (B : Set X) ↦ a ∈ B ∧ IsBlock G B) (orbit.{u_1, u_2} (↥H) a) ⋯,
              left_inv := ⋯, right_inv := ⋯ } :
            (a_1 : { B : Set X // a ∈ B ∧ IsBlock G B }) → (↑(Ici (stabilizer G a)) : Type u_1))
          (Subtype.mk (p := fun (B : Set X) ↦ a ∈ B ∧ IsBlock G B) B' ⋯) :
        (↑(Ici (stabilizer G a)) : Type u_1)) ↔
    LE.le (α := { B : Set X // a ∈ B ∧ IsBlock G B }) (Subtype.mk (p := fun (B : Set X) ↦ a ∈ B ∧ IsBlock G B) B ⋯)
      (Subtype.mk (p := fun (B : Set X) ↦ a ∈ B ∧ IsBlock G B) B' ⋯)
have simp : LE.le (α := Subgroup G) (stabilizer G B) (stabilizer G B') ↔ B ⊆ B'
Tactic: simp only [Equiv.coe_fn_mk, Subtype.mk_le_mk, Set.le_eq_subset]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (goal)
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
B_1 : Set X
htGX : IsPretransitive G X
a : X
B : Set X
ha : a ∈ B
hB : IsBlock G B
B' : Set X
ha' : a ∈ B'
hB' : IsBlock G B'
⊢ LE.le (α := Subgroup G) (stabilizer G B) (stabilizer G B') ↔ B ⊆ B'
have mp : LE.le (α := Subgroup G) (stabilizer G B) (stabilizer G B') → B ⊆ B'
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (goal)
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
B_1 : Set X
htGX : IsPretransitive G X
a : X
B : Set X
ha : a ∈ B
hB : IsBlock G B
B' : Set X
ha' : a ∈ B'
hB' : IsBlock G B'
mp : LE.le (α := Subgroup G) (stabilizer G B) (stabilizer G B') → B ⊆ B'
⊢ LE.le (α := Subgroup G) (stabilizer G B) (stabilizer G B') ↔ B ⊆ B'
have mpr : B ⊆ B' → LE.le (α := Subgroup G) (stabilizer G B) (stabilizer G B')
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (goal)
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
B_1 : Set X
htGX : IsPretransitive G X
a : X
B : Set X
ha : a ∈ B
hB : IsBlock G B
B' : Set X
ha' : a ∈ B'
hB' : IsBlock G B'
hBB' : LE.le (α := Subgroup G) (stabilizer G B) (stabilizer G B')
b : X
hb : b ∈ B
⊢ b ∈ B'
have mp : ∀ (k : G) (hb : k • a ∈ B), k • a ∈ B'
Tactic: obtain ⟨k, rfl⟩ := htGX.exists_smul_eq a b
Cleared hypotheses: b, hb
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (goal)
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
B_1 : Set X
htGX : IsPretransitive G X
a : X
B : Set X
ha : a ∈ B
hB : IsBlock G B
B' : Set X
ha' : a ∈ B'
hB' : IsBlock G B'
hBB' : LE.le (α := Subgroup G) (stabilizer G B) (stabilizer G B')
k : G
hb : k • a ∈ B
⊢ k • a ∈ B'
have mp : Membership.mem (γ := Subgroup G) (stabilizer G B') k
Tactic: suffices k ∈ stabilizer G B' by
        exact this.symm ▸ (Set.smul_mem_smul_set ha')
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (goal)
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
B_1 : Set X
htGX : IsPretransitive G X
a : X
B : Set X
ha : a ∈ B
hB : IsBlock G B
B' : Set X
ha' : a ∈ B'
hB' : IsBlock G B'
hBB' : B ⊆ B'
g : G
hgB : Membership.mem (γ := Subgroup G) (stabilizer G B) g
⊢ Membership.mem (γ := Subgroup G) (stabilizer G B') g
have mpr : g • a ∈ B'
Tactic: apply hB'.smul_eq_of_mem ha'
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (goal)
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
B : Set X
inst_2 : Nontrivial X
a : X
⊢ Nontrivial.{u_2} (BlockMem G a)
have rw : ∃ (x : BlockMem G a) (y : BlockMem G a), x ≠ y
Tactic: rw [nontrivial_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (goal)
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
B : Set X
inst_2 : Nontrivial X
a : X
⊢ ∃ (x : BlockMem G a) (y : BlockMem G a), x ≠ y
have h : Ne.{u_2 + 1} (α := BlockMem G a) ⊥ ⊤
Tactic: use ⊥, ⊤
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (hypothesis)
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
B : Set X
inst_2 : Nontrivial X
a : X
h : Eq.{u_2 + 1} (α := BlockMem G a) ⊥ ⊤
⊢ False
have h₁ : Eq.{u_2 + 1} (α := Set X) (↑⊥ : Set X) (↑⊤ : Set X)
Tactic: rw [← Subtype.coe_inj] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (goal)
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
B : Set X
inst_2 : Nontrivial X
a : X
h : Eq (α := Set X) {a} univ
⊢ False
have h₁ : ∀ (b : X) (hb : b ≠ a), False
Tactic: obtain ⟨b, hb⟩ := exists_ne a
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (goal)
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
B : Set X
inst_2 : Nontrivial X
a : X
h : Eq (α := Set X) {a} univ
b : X
hb : b ≠ a
⊢ False
have h₁ : b = a
Tactic: apply hb
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (goal)
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
B : Set X
inst_2 : Nontrivial X
a : X
h : Eq (α := Set X) {a} univ
b : X
hb : b ≠ a
⊢ b = a
have h₁ : Membership.mem (γ := Set X) univ b
Tactic: rw [← Set.mem_singleton_iff, h]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (goal)
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
inst_2 : IsPretransitive G X
B : Set X
hB : IsBlock G B
x : X
hx : x ∈ B
⊢ Eq (α := Subgroup ↥(stabilizer G B)) (Subgroup.subgroupOf (stabilizer G x) (stabilizer G B))
    (stabilizer (↥(stabilizer G B)) x)
have h : ∀ (x_1 : ↥(stabilizer G B)),
  Membership.mem (γ := Subgroup ↥(stabilizer G B)) (Subgroup.subgroupOf (stabilizer G x) (stabilizer G B)) x_1 ↔
    Membership.mem (γ := Subgroup ↥(stabilizer G B)) (stabilizer (↥(stabilizer G B)) x) x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (hypothesis)
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
inst_2 : IsPretransitive G X
B : Set X
hB : IsBlock G B
x : X
hx : x ∈ B
⊢ B.ncard = Subgroup.relIndex (stabilizer G x) (stabilizer G B)
have key : Eq (α := Subgroup ↥(stabilizer G B)) (Subgroup.subgroupOf (stabilizer G x) (stabilizer G B))
  (stabilizer (↥(stabilizer G B)) x)
Tactic: have key : (stabilizer G x).subgroupOf (stabilizer G B) = stabilizer (stabilizer G B) x := by
    ext; rfl
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (goal)
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
inst_2 : IsPretransitive G X
B : Set X
hB : IsBlock G B
x : X
hx : x ∈ B
key :
  Eq (α := Subgroup ↥(stabilizer G B)) (Subgroup.subgroupOf (stabilizer G x) (stabilizer G B))
    (stabilizer (↥(stabilizer G B)) x)
⊢ B.ncard = Subgroup.relIndex (stabilizer G x) (stabilizer G B)
have rw : B.ncard = Subgroup.index (G := ↥(stabilizer G B)) (Subgroup.subgroupOf (stabilizer G x) (stabilizer G B))
Tactic: rw [Subgroup.relIndex, key, index_stabilizer, hB.orbit_stabilizer_eq hx]