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
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)
rw : B.ncard = Subgroup.index (G := ↥(stabilizer G B)) (Subgroup.subgroupOf (stabilizer G x) (stabilizer G B))
⊢ B.ncard = Subgroup.relIndex (stabilizer G x) (stabilizer G B)
have rw₁ : B.ncard = Subgroup.index.{u_1} (G := ↥(stabilizer G B)) (stabilizer (↥(stabilizer G B)) x)
Tactic: rw [Subgroup.relIndex, key, index_stabilizer, hB.orbit_stabilizer_eq 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
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)
rw : B.ncard = Subgroup.index (G := ↥(stabilizer G B)) (Subgroup.subgroupOf (stabilizer G x) (stabilizer G B))
rw₁ : B.ncard = Subgroup.index.{u_1} (G := ↥(stabilizer G B)) (stabilizer (↥(stabilizer G B)) x)
⊢ B.ncard = Subgroup.relIndex (stabilizer G x) (stabilizer G B)
have rw₂ : B.ncard = (orbit.{u_1, u_2} (↥(stabilizer G B)) x).ncard
Tactic: rw [Subgroup.relIndex, key, index_stabilizer, hB.orbit_stabilizer_eq 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
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)
rw : B.ncard = Subgroup.index (G := ↥(stabilizer G B)) (Subgroup.subgroupOf (stabilizer G x) (stabilizer G B))
rw₁ : B.ncard = Subgroup.index.{u_1} (G := ↥(stabilizer G B)) (stabilizer (↥(stabilizer G B)) x)
rw₂ : B.ncard = (orbit.{u_1, u_2} (↥(stabilizer G B)) x).ncard
⊢ B.ncard = Subgroup.relIndex (stabilizer G x) (stabilizer G B)
have rw₃ : B.ncard = B.ncard
Tactic: rw [Subgroup.relIndex, key, index_stabilizer, hB.orbit_stabilizer_eq 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
inst_2 : IsPretransitive G X
B : Set X
hB : IsBlock G B
hB_ne : B.Nonempty
⊢ B.ncard * (orbit G B).ncard = Nat.card X
have obtain : ∀ (x : X) (hx : x ∈ B), B.ncard * (orbit G B).ncard = Nat.card X
Tactic: obtain ⟨x, hx⟩ := hB_ne
Cleared hypotheses: hB_ne
-- 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
⊢ B.ncard * (orbit G B).ncard = Nat.card X
have rw : Subgroup.relIndex (stabilizer G x) (stabilizer G B) * (orbit G B).ncard = Nat.card X
Tactic: rw [ncard_block_eq_relIndex hB hx, ← index_stabilizer,
      Subgroup.relIndex_mul_index (hB.stabilizer_le hx), index_stabilizer_of_transitive]
-- 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
rw : Subgroup.relIndex (stabilizer G x) (stabilizer G B) * (orbit G B).ncard = Nat.card X
⊢ B.ncard * (orbit G B).ncard = Nat.card X
have rw₁ : Subgroup.relIndex (stabilizer G x) (stabilizer G B) * Subgroup.index (stabilizer G B) = Nat.card X
Tactic: rw [ncard_block_eq_relIndex hB hx, ← index_stabilizer,
      Subgroup.relIndex_mul_index (hB.stabilizer_le hx), index_stabilizer_of_transitive]
-- 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
rw : Subgroup.relIndex (stabilizer G x) (stabilizer G B) * (orbit G B).ncard = Nat.card X
rw₁ : Subgroup.relIndex (stabilizer G x) (stabilizer G B) * Subgroup.index (stabilizer G B) = Nat.card X
⊢ B.ncard * (orbit G B).ncard = Nat.card X
have rw₂ : Subgroup.index (stabilizer G x) = Nat.card X
Tactic: rw [ncard_block_eq_relIndex hB hx, ← index_stabilizer,
      Subgroup.relIndex_mul_index (hB.stabilizer_le hx), index_stabilizer_of_transitive]
-- 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
rw : Subgroup.relIndex (stabilizer G x) (stabilizer G B) * (orbit G B).ncard = Nat.card X
rw₁ : Subgroup.relIndex (stabilizer G x) (stabilizer G B) * Subgroup.index (stabilizer G B) = Nat.card X
rw₂ : Subgroup.index (stabilizer G x) = Nat.card X
⊢ B.ncard * (orbit G B).ncard = Nat.card X
have rw₃ : Nat.card X = Nat.card X
Tactic: rw [ncard_block_eq_relIndex hB hx, ← index_stabilizer,
      Subgroup.relIndex_mul_index (hB.stabilizer_le hx), index_stabilizer_of_transitive]
-- 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
hX : Finite X
hB : IsBlock G B
hB' : Nat.card X < B.ncard * 2
⊢ B = Set.univ
have inl : ∀ (hB : IsBlock.{u_1, u_2} G (X := X) ∅) (hB' : Nat.card X < ncard.{u_2} (α := X) ∅ * 2),
  Eq.{u_2 + 1} (α := Set X) ∅ Set.univ
Tactic: rcases Set.eq_empty_or_nonempty B with rfl | hB_ne
Cleared hypotheses: B, hB, 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
inst_2 : IsPretransitive G X
B : Set X
hX : Finite X
hB : IsBlock G B
hB' : Nat.card X < B.ncard * 2
inl :
  ∀ (hB : IsBlock.{u_1, u_2} G (X := X) ∅) (hB' : Nat.card X < ncard.{u_2} (α := X) ∅ * 2),
    Eq.{u_2 + 1} (α := Set X) ∅ Set.univ
⊢ B = Set.univ
have inr : ∀ (hB_ne : B.Nonempty), B = Set.univ
Tactic: rcases Set.eq_empty_or_nonempty B with rfl | hB_ne
-- 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
hX : Finite X
hB : IsBlock G B
hB' : Nat.card X < B.ncard * 2
hB_ne : B.Nonempty
⊢ B = Set.univ
have key : B.ncard * (orbit G B).ncard = Nat.card X
Tactic: have key := hB.ncard_block_mul_ncard_orbit_eq hB_ne
-- 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
hX : Finite X
hB : IsBlock G B
hB' : Nat.card X < B.ncard * 2
hB_ne : B.Nonempty
key : B.ncard * (orbit G B).ncard = Nat.card X
⊢ B = Set.univ
have hB'₁ : (orbit G B).ncard < 2
Tactic: rw [← key, mul_lt_mul_iff_of_pos_left (by rwa [Set.ncard_pos])] at hB'
Cleared hypotheses: hB', hB_ne, key
-- 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
hX : Finite X
hB : IsBlock G B
hB' : (orbit G B).ncard < 2
hB_ne : B.Nonempty
key : B.ncard * (orbit G B).ncard = Nat.card X
⊢ B = Set.univ
have inr : ∀ (hB' : LT.lt (α := ℕ) 0 2) (key : B.ncard * 0 = Nat.card X), B = Set.univ
Tactic: interval_cases (orbit G B).ncard
Cleared hypotheses: hB', key
-- 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
hX : Finite X
hB : IsBlock G B
hB' : (orbit G B).ncard < 2
hB_ne : B.Nonempty
key : B.ncard * (orbit G B).ncard = Nat.card X
inr : ∀ (hB' : LT.lt (α := ℕ) 0 2) (key : B.ncard * 0 = Nat.card X), B = Set.univ
⊢ B = Set.univ
have inr₁ : ∀ (hB' : LT.lt (α := ℕ) 1 2) (key : B.ncard * 1 = Nat.card X), B = Set.univ
Tactic: interval_cases (orbit G B).ncard
Cleared hypotheses: hB', key
-- 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
hX : Finite X
hB : IsBlock G B
hB_ne : B.Nonempty
hB' : LT.lt (α := ℕ) 0 2
key : B.ncard * 0 = Nat.card X
⊢ B = Set.univ
have key₁ : IsEmpty X
Tactic: rw [mul_zero, eq_comm, Nat.card_eq_zero, or_iff_left hX.not_infinite] at key
Cleared hypotheses: key
-- 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
hX : Finite X
hB : IsBlock G B
hB_ne : B.Nonempty
hB' : LT.lt (α := ℕ) 1 2
key : B.ncard * 1 = Nat.card X
⊢ B = Set.univ
have key₁ : B.ncard = ncard.{u_2} (α := X) Set.univ
Tactic: rw [mul_one, ← Set.ncard_univ] at key
Cleared hypotheses: key
-- 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
hX : Finite X
hB : IsBlock G B
hB_ne : B.Nonempty
hB' : LT.lt (α := ℕ) 1 2
key : B.ncard = ncard.{u_2} (α := X) Set.univ
⊢ B = Set.univ
have inr : Eq.{u_2 + 1} (α := Set X) Set.univ Set.univ
Tactic: rw [Set.eq_of_subset_of_ncard_le (Set.subset_univ B) key.ge]
-- 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
inst_3 : Finite X
hB : IsBlock G B
hB' : Nat.card X < 2 * (orbit G B).ncard
⊢ B.Subsingleton
have suffices : B.ncard < 2
Tactic: suffices Set.ncard B < 2 by simp_all
-- 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
inst_3 : Finite X
hB : IsBlock G B
hB' : Nat.card X < 2 * (orbit G B).ncard
h : B = ∅
⊢ B.ncard < 2
have inl : LT.lt (α := ℕ) 0 2
Tactic: rw [h, Set.ncard_empty]
-- 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
inst_3 : Finite X
hB : IsBlock G B
hB' : Nat.card X < 2 * (orbit G B).ncard
h : B.Nonempty
⊢ B.ncard < 2
have hB'₁ : ¬2 * (orbit G B).ncard ≤ B.ncard * (orbit G B).ncard
Tactic: rw [← hB.ncard_block_mul_ncard_orbit_eq h, lt_iff_not_ge] at hB'
Cleared hypotheses: hB', 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
inst_3 : Finite X
hB : IsBlock G B
hB' : ¬2 * (orbit G B).ncard ≤ B.ncard * (orbit G B).ncard
h : B.Nonempty
⊢ B.ncard < 2
have inr : ¬2 ≤ B.ncard
Tactic: rw [← not_le]
-- 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
inst_3 : Finite X
hB : IsBlock G B
hB' : Nat.card X < 2 * (orbit G B).ncard
⊢ B.ncard < 2
have x : B = ∅ ∨ B.Nonempty
Tactic: cases Set.eq_empty_or_nonempty B with
  | inl h => rw [h, Set.ncard_empty]; simp
  | inr h =>
    rw [← hB.ncard_block_mul_ncard_orbit_eq h, lt_iff_not_ge] at hB'
    rw [← not_le]
    exact fun hb ↦ hB' (Nat.mul_le_mul_right _ 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
inst_2 : IsPretransitive G X
B : Set X
a : X
hfB : B.Finite
B' : Set X := ⋂ (k : G), ⋂ (_ : a ∈ k • B), k • B
⊢ IsBlock.{u_1, u_2} G (X := X) (⋂ (k : G), ⋂ (_ : a ∈ k • B), k • B)
have inl : ∀ (hfB_e : B = ∅), IsBlock.{u_1, u_2} G (X := X) (⋂ (k : G), ⋂ (_ : a ∈ k • B), k • B)
Tactic: rcases Set.eq_empty_or_nonempty B with hfB_e | hfB_ne
-- 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
a : X
hfB : B.Finite
B' : Set X := ⋂ (k : G), ⋂ (_ : a ∈ k • B), k • B
inl : ∀ (hfB_e : B = ∅), IsBlock.{u_1, u_2} G (X := X) (⋂ (k : G), ⋂ (_ : a ∈ k • B), k • B)
⊢ IsBlock.{u_1, u_2} G (X := X) (⋂ (k : G), ⋂ (_ : a ∈ k • B), k • B)
have inr : ∀ (hfB_ne : B.Nonempty), IsBlock.{u_1, u_2} G (X := X) (⋂ (k : G), ⋂ (_ : a ∈ k • B), k • B)
Tactic: rcases Set.eq_empty_or_nonempty B with hfB_e | hfB_ne
-- 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
a : X
hfB : B.Finite
B' : Set X := ⋂ (k : G), ⋂ (_ : a ∈ k • B), k • B
hfB_ne : B.Nonempty
⊢ IsBlock.{u_1, u_2} G (X := X) (⋂ (k : G), ⋂ (_ : a ∈ k • B), k • B)
have hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
Tactic: have hB'₀ : ∀ (k : G) (_ : a ∈ k • B), B' ≤ k • B := by
    intro k hk
    exact Set.biInter_subset_of_mem hk
-- 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
a : X
hfB : B.Finite
B' : Set X := ⋂ (k : G), ⋂ (_ : a ∈ k • B), k • B
hfB_ne : B.Nonempty
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
⊢ B'.Finite
have obtain : ∀ (b : X) (hb : b ∈ B), B'.Finite
Tactic: obtain ⟨b, hb : b ∈ B⟩ := hfB_ne
Cleared hypotheses: hfB_ne
-- 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
a : X
hfB : B.Finite
B' : Set X := ⋂ (k : G), ⋂ (_ : a ∈ k • B), k • B
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
b : X
hb : b ∈ B
⊢ B'.Finite
have obtain : ∀ (k : G) (hk : k • b = a), B'.Finite
Tactic: obtain ⟨k, hk : k • b = a⟩ := exists_smul_eq G b 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
inst_2 : IsPretransitive G X
B : Set X
a : X
hfB : B.Finite
B' : Set X := ⋂ (k : G), ⋂ (_ : a ∈ k • B), k • B
hfB_ne : B.Nonempty
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
⊢ IsBlock.{u_1, u_2} G (X := X) (⋂ (k : G), ⋂ (_ : a ∈ k • B), k • B)
have hfB' : B'.Finite
Tactic: have hfB' : B'.Finite := by
    obtain ⟨b, hb : b ∈ B⟩ := hfB_ne
    obtain ⟨k, hk : k • b = a⟩ := exists_smul_eq G b a
    apply Set.Finite.subset (Set.Finite.map _ hfB) (hB'₀ k ⟨b, hb, hk⟩)
-- 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
a : X
hfB : B.Finite
B' : Set X := ⋂ (k : G), ⋂ (_ : a ∈ k • B), k • B
hfB_ne : B.Nonempty
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
hfB' : B'.Finite
g : G
hg : a ∈ g • B'
x : X
hx : x ∈ B'
⊢ x ∈ g • B'
have simp : ∀ (hg : ∀ (i : G) (i_1 : i⁻¹ • a ∈ B), (g * i)⁻¹ • a ∈ B) (hx : ∀ (i : G) (i_1 : i⁻¹ • a ∈ B), i⁻¹ • x ∈ B) (i : G)
  (i_1 : i⁻¹ • a ∈ B), (g * i)⁻¹ • x ∈ B
Tactic: simp only [B', Set.mem_iInter, Set.mem_smul_set_iff_inv_smul_mem,
      smul_smul, ← mul_inv_rev] at hg hx ⊢
Cleared hypotheses: hg, hx
-- 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
a : X
hfB : B.Finite
B' : Set X := ⋂ (k : G), ⋂ (_ : a ∈ k • B), k • B
hfB_ne : B.Nonempty
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
hfB' : B'.Finite
⊢ IsBlock.{u_1, u_2} G (X := X) (⋂ (k : G), ⋂ (_ : a ∈ k • B), k • B)
have hag : ∀ (g : G), a ∈ g • B' → B' ≤ g • B'
Tactic: have hag : ∀ g : G, a ∈ g • B' → B' ≤ g • B' := by
    intro g hg x hx
    -- a = g • b; b ∈ B'; a ∈ k • B → b ∈ k • B
    simp only [B', Set.mem_iInter, Set.mem_smul_set_iff_inv_smul_mem,
      smul_smul, ← mul_inv_rev] at hg hx ⊢
    exact fun _ ↦ hx _ ∘ hg _
-- 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
a : X
hfB : B.Finite
B' : Set X := ⋂ (k : G), ⋂ (_ : a ∈ k • B), k • B
hfB_ne : B.Nonempty
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
hfB' : B'.Finite
hag : ∀ (g : G), a ∈ g • B' → B' ≤ g • B'
g : G
hg : a ∈ g • B'
⊢ B' = g • B'
have rw : B' ⊆ g • B'
Tactic: rw [eq_comm, ← mem_stabilizer_iff, mem_stabilizer_set_iff_subset_smul_set hfB']
-- 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
a : X
hfB : B.Finite
B' : Set X := ⋂ (k : G), ⋂ (_ : a ∈ k • B), k • B
hfB_ne : B.Nonempty
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
hfB' : B'.Finite
hag : ∀ (g : G), a ∈ g • B' → B' ≤ g • B'
⊢ IsBlock.{u_1, u_2} G (X := X) (⋂ (k : G), ⋂ (_ : a ∈ k • B), k • B)
have hag' : ∀ (g : G) (hg : a ∈ g • B'), B' = g • B'
Tactic: have hag' (g : G) (hg : a ∈ g • B') : B' = g • B' := by
    rw [eq_comm, ← mem_stabilizer_iff, mem_stabilizer_set_iff_subset_smul_set hfB']
    exact hag g hg
-- 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
a : X
hfB : B.Finite
B' : Set X := ⋂ (k : G), ⋂ (_ : a ∈ k • B), k • B
hfB_ne : B.Nonempty
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
hfB' : B'.Finite
hag : ∀ (g : G), a ∈ g • B' → B' ≤ g • B'
hag' : ∀ (g : G) (hg : a ∈ g • B'), B' = g • B'
⊢ IsBlock.{u_1, u_2} G (X := X) (⋂ (k : G), ⋂ (_ : a ∈ k • B), k • B)
have inr : ∀ ⦃g : G⦄,
  (HSMul.hSMul (β := Set X) g (⋂ (k : G), ⋂ (_ : a ∈ k • B), k • B) ∩ ⋂ (k : G), ⋂ (_ : a ∈ k • B), k • B).Nonempty →
    HSMul.hSMul (β := Set X) g (⋂ (k : G), ⋂ (_ : a ∈ k • B), k • B) = ⋂ (k : G), ⋂ (_ : a ∈ k • B), k • B
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
inst_2 : IsPretransitive G X
B : Set X
a : X
hfB : B.Finite
B' : Set X := ⋂ (k : G), ⋂ (_ : a ∈ k • B), k • B
hfB_ne : B.Nonempty
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
hfB' : B'.Finite
hag : ∀ (g : G), a ∈ g • B' → B' ≤ g • B'
hag' : ∀ (g : G) (hg : a ∈ g • B'), B' = g • B'
g : G
b : X
hb' : b ∈ g • B'
hb : b ∈ B'
⊢ HSMul.hSMul (β := Set X) g (⋂ (k : G), ⋂ (_ : a ∈ k • B), k • B) = ⋂ (k : G), ⋂ (_ : a ∈ k • B), k • B
have inr : ∀ (k : G) (hk : k • a = b),
  HSMul.hSMul (β := Set X) g (⋂ (k : G), ⋂ (_ : a ∈ k • B), k • B) = ⋂ (k : G), ⋂ (_ : a ∈ k • B), k • B
Tactic: obtain ⟨k : G, hk : k • a = b⟩ := exists_smul_eq G a b
-- 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
a : X
hfB : B.Finite
B' : Set X := ⋂ (k : G), ⋂ (_ : a ∈ k • B), k • B
hfB_ne : B.Nonempty
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
hfB' : B'.Finite
hag : ∀ (g : G), a ∈ g • B' → B' ≤ g • B'
hag' : ∀ (g : G) (hg : a ∈ g • B'), B' = g • B'
g : G
b : X
hb' : b ∈ g • B'
hb : b ∈ B'
k : G
hk : k • a = b
⊢ a ∈ k⁻¹ • B'
have refine : (fun (x : X) ↦ k⁻¹ • x) b = a
Tactic: refine ⟨b, hb, ?_⟩
-- 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
a : X
hfB : B.Finite
B' : Set X := ⋂ (k : G), ⋂ (_ : a ∈ k • B), k • B
hfB_ne : B.Nonempty
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
hfB' : B'.Finite
hag : ∀ (g : G), a ∈ g • B' → B' ≤ g • B'
hag' : ∀ (g : G) (hg : a ∈ g • B'), B' = g • B'
g : G
b : X
hb' : b ∈ g • B'
hb : b ∈ B'
k : G
hk : k • a = b
⊢ HSMul.hSMul (β := Set X) g (⋂ (k : G), ⋂ (_ : a ∈ k • B), k • B) = ⋂ (k : G), ⋂ (_ : a ∈ k • B), k • B
have hak : a ∈ k⁻¹ • B'
Tactic: have hak : a ∈ k⁻¹ • B' := by
    refine ⟨b, hb, ?_⟩
    simp only [← hk, inv_smul_smul]
-- 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
a : X
hfB : B.Finite
B' : Set X := ⋂ (k : G), ⋂ (_ : a ∈ k • B), k • B
hfB_ne : B.Nonempty
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
hfB' : B'.Finite
hag : ∀ (g : G), a ∈ g • B' → B' ≤ g • B'
hag' : ∀ (g : G) (hg : a ∈ g • B'), B' = g • B'
g : G
b : X
hb' : b ∈ g • B'
hb : b ∈ B'
k : G
hk : k • a = b
hak : a ∈ k⁻¹ • B'
⊢ HSMul.hSMul (β := Set X) g (⋂ (k : G), ⋂ (_ : a ∈ k • B), k • B) = ⋂ (k : G), ⋂ (_ : a ∈ k • B), k • B
have hagk : a ∈ (k⁻¹ * g) • B'
Tactic: have hagk : a ∈ (k⁻¹ * g) • B' := by
    rw [mul_smul, Set.mem_smul_set_iff_inv_smul_mem, inv_inv, hk]
    exact hb'
-- 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
a : X
hfB : B.Finite
B' : Set X := ⋂ (k : G), ⋂ (_ : a ∈ k • B), k • B
hfB_ne : B.Nonempty
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
hfB' : B'.Finite
hag : ∀ (g : G), a ∈ g • B' → B' ≤ g • B'
hag' : ∀ (g : G) (hg : a ∈ g • B'), B' = g • B'
g : G
b : X
hb' : b ∈ g • B'
hb : b ∈ B'
k : G
hk : k • a = b
hak : a ∈ k⁻¹ • B'
hagk : a ∈ (k⁻¹ * g) • B'
⊢ HSMul.hSMul (β := Set X) g (⋂ (k : G), ⋂ (_ : a ∈ k • B), k • B) = ⋂ (k : G), ⋂ (_ : a ∈ k • B), k • B
have hkB' : B' = k⁻¹ • B'
Tactic: have hkB' : B' = k⁻¹ • B' := hag' k⁻¹ hak
-- 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
a : X
hfB : B.Finite
B' : Set X := ⋂ (k : G), ⋂ (_ : a ∈ k • B), k • B
hfB_ne : B.Nonempty
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
hfB' : B'.Finite
hag : ∀ (g : G), a ∈ g • B' → B' ≤ g • B'
hag' : ∀ (g : G) (hg : a ∈ g • B'), B' = g • B'
g : G
b : X
hb' : b ∈ g • B'
hb : b ∈ B'
k : G
hk : k • a = b
hak : a ∈ k⁻¹ • B'
hagk : a ∈ (k⁻¹ * g) • B'
hkB' : B' = k⁻¹ • B'
⊢ HSMul.hSMul (β := Set X) g (⋂ (k : G), ⋂ (_ : a ∈ k • B), k • B) = ⋂ (k : G), ⋂ (_ : a ∈ k • B), k • B
have hgkB' : B' = (k⁻¹ * g) • B'
Tactic: have hgkB' : B' = (k⁻¹ * g) • B' := hag' (k⁻¹ * g) hagk
-- 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
a : X
hfB : B.Finite
B' : Set X := ⋂ (k : G), ⋂ (_ : a ∈ k • B), k • B
hfB_ne : B.Nonempty
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
hfB' : B'.Finite
hag : ∀ (g : G), a ∈ g • B' → B' ≤ g • B'
hag' : ∀ (g : G) (hg : a ∈ g • B'), B' = g • B'
g : G
b : X
hb' : b ∈ g • B'
hb : b ∈ B'
k : G
hk : k • a = b
hak : a ∈ k⁻¹ • B'
hagk : a ∈ (k⁻¹ * g) • B'
hkB' : B' = k⁻¹ • B'
hgkB' : B' = (k⁻¹ * g) • B'
⊢ HSMul.hSMul (β := Set X) g (⋂ (k : G), ⋂ (_ : a ∈ k • B), k • B) = ⋂ (k : G), ⋂ (_ : a ∈ k • B), k • B
have hgkB'₁ : B' = k⁻¹ • g • B'
Tactic: rw [mul_smul] at hgkB'
Cleared hypotheses: hgkB'
-- 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
a : X
hfB : B.Finite
B' : Set X := ⋂ (k : G), ⋂ (_ : a ∈ k • B), k • B
hfB_ne : B.Nonempty
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
hfB' : B'.Finite
hag : ∀ (g : G), a ∈ g • B' → B' ≤ g • B'
hag' : ∀ (g : G) (hg : a ∈ g • B'), B' = g • B'
g : G
b : X
hb' : b ∈ g • B'
hb : b ∈ B'
k : G
hk : k • a = b
hak : a ∈ k⁻¹ • B'
hagk : a ∈ (k⁻¹ * g) • B'
hkB' : B' = k⁻¹ • B'
hgkB' : B' = k⁻¹ • g • B'
⊢ HSMul.hSMul (β := Set X) g (⋂ (k : G), ⋂ (_ : a ∈ k • B), k • B) = ⋂ (k : G), ⋂ (_ : a ∈ k • B), k • B
have hkB'₁ : k • B' = B'
Tactic: rw [← smul_eq_iff_eq_inv_smul] at hkB' hgkB'
Cleared hypotheses: hkB', hgkB'