awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
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
⊢ g • a ∈ B'

Tactic:
exact hBB' <| hgB.symm ▸ (Set.smul_mem_smul_set ha)
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
B_1 : Set X
a : X
B : Set X
ha : a ∈ B
hB : IsBlock G B
⊢ LE.le (α := BlockMem G a) (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) univ ⋯)

Tactic:
simp only [Subtype.mk_le_mk, le_eq_subset, subset_univ]

Premises used: Set.le_eq_subset, Set.subset_univ, Subtype.mk_le_mk
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
B_1 : Set X
a : X
B : Set X
ha : a ∈ B
hB : IsBlock G B
simp : a ∈ B
⊢ LE.le (α := BlockMem G a) (Subtype.mk (p := fun (B : Set X) ↦ a ∈ B ∧ IsBlock G B) {a} ⋯)
    (Subtype.mk (p := fun (B : Set X) ↦ a ∈ B ∧ IsBlock G B) B ⋯)

Tactic:
simp only [Subtype.mk_le_mk, Set.le_eq_subset, Set.singleton_subset_iff]

Premises used: Set.singleton_subset_iff, Set.le_eq_subset, Subtype.mk_le_mk
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
B_1 : Set X
a : X
B : Set X
ha : a ∈ B
hB : IsBlock G B
⊢ a ∈ B

Tactic:
ha
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
B_1 : Set X
a : X
B : Set X
ha : a ∈ B
hB : IsBlock G B
⊢ a ∈ B

Tactic:
exact ha
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
a : X
⊢ Eq.{u_2 + 1} (α := Set X) (↑⊤ : Set X) univ

Tactic:
rfl

Premises used: Set.univ, setOf, rfl
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
a : X
⊢ Eq (α := Set X) (↑⊥ : Set X) {a}

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
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
rw : ∃ (x : BlockMem G a) (y : BlockMem G a), x ≠ y
⊢ Nontrivial.{u_2} (BlockMem G a)

Tactic:
rw [nontrivial_iff]

Premises used: nontrivial_iff
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
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 : Ne.{u_2 + 1} (α := BlockMem G a) ⊥ ⊤
⊢ ∃ (x : BlockMem G a) (y : BlockMem G a), x ≠ y

Tactic:
use ⊥, ⊤
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
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) ⊥ ⊤
⊢ Eq.{u_2 + 1} (α := Set X) (↑⊥ : Set X) (↑⊤ : Set X)

Tactic:
rw [← Subtype.coe_inj] at h

Premises used: Subtype.coe_inj
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
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
h₁ : ∀ (b : X) (hb : b ≠ a), False
⊢ False

Tactic:
obtain ⟨b, hb⟩ := exists_ne a

Premises used: exists_ne
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
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
h₁ : b = a
⊢ False

Tactic:
apply hb
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
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
h₁ : Membership.mem (γ := Set X) univ b
⊢ b = a

Tactic:
rw [← Set.mem_singleton_iff, h]

Premises used: Set.mem_singleton_iff
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
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
⊢ Membership.mem (γ := Set X) univ b

Tactic:
apply Set.mem_univ

Premises used: Set.mem_univ
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
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
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
⊢ Eq (α := Subgroup ↥(stabilizer G B)) (Subgroup.subgroupOf (stabilizer G x) (stabilizer G B))
    (stabilizer (↥(stabilizer G B)) x)

Tactic:
ext
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
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
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:
rfl
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
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)

Tactic:
have key : (stabilizer G x).subgroupOf (stabilizer G B) = stabilizer (stabilizer G B) x := by
    ext; rfl
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
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
rw₃ rw₄ : B.ncard = B.ncard
⊢ B.ncard = Subgroup.relIndex (stabilizer G x) (stabilizer G B)

Tactic:
rw [Subgroup.relIndex, key, index_stabilizer, hB.orbit_stabilizer_eq hx]

Premises used: MulAction.index_stabilizer, MulAction.IsBlock.orbit_stabilizer_eq, Subgroup.relIndex
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
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
obtain : ∀ (x : X) (hx : x ∈ B), B.ncard * (orbit G B).ncard = Nat.card X
⊢ B.ncard * (orbit G B).ncard = Nat.card X

Tactic:
obtain ⟨x, hx⟩ := hB_ne
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
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
rw₃ rw₄ : Nat.card X = Nat.card X
⊢ B.ncard * (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]

Premises used: Subgroup.relIndex_mul_index, MulAction.index_stabilizer_of_transitive, MulAction.IsBlock.stabilizer_le, MulAction.index_stabilizer, MulAction.IsBlock.ncard_block_eq_relIndex
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
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 ∣ Nat.card X

Tactic:
Dvd.intro _ (hB.ncard_block_mul_ncard_orbit_eq hB_ne)

Premises used: Dvd.intro, MulAction.IsBlock.ncard_block_mul_ncard_orbit_eq
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
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
inr : ∀ (hB_ne : B.Nonempty), B = Set.univ
⊢ B = Set.univ

Tactic:
rcases Set.eq_empty_or_nonempty B with rfl | hB_ne

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
inst_2 : IsPretransitive G X
hX : Finite X
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:
simp at hB'
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
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.ncard * (orbit G B).ncard = Nat.card X

Tactic:
have key := hB.ncard_block_mul_ncard_orbit_eq hB_ne
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
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' : B.ncard * (orbit G B).ncard < B.ncard * 2
hB_ne : B.Nonempty
key : B.ncard * (orbit G B).ncard = Nat.card X
rwa rwa₁ rwa₂ rwa₃ : B.Nonempty
⊢ 0 < B.ncard

Tactic:
rwa [Set.ncard_pos]

Premises used: Set.ncard_pos
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
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
⊢ (orbit G B).ncard < 2

Tactic:
rw [← key, mul_lt_mul_iff_of_pos_left (by rwa [Set.ncard_pos])] at hB'

Premises used: mul_lt_mul_iff_of_pos_left
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
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
hB'₁ : (orbit G B).ncard < 2
⊢ B.Nonempty

Tactic:
rw [← key, mul_lt_mul_iff_of_pos_left (by rwa [Set.ncard_pos])] at hB'

Premises used: mul_lt_mul_iff_of_pos_left
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
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
hB'₁ : (orbit G B).ncard < 2
hB_ne₁ : B.Nonempty
⊢ B.ncard * (orbit G B).ncard = Nat.card X

Tactic:
rw [← key, mul_lt_mul_iff_of_pos_left (by rwa [Set.ncard_pos])] at hB'

Premises used: mul_lt_mul_iff_of_pos_left
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
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
inr₁ : ∀ (hB' : LT.lt (α := ℕ) 1 2) (key : B.ncard * 1 = Nat.card X), B = Set.univ
⊢ B = Set.univ

Tactic:
interval_cases (orbit G B).ncard

Premises used: MulAction.orbit, Set.ncard
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
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
⊢ IsEmpty X

Tactic:
rw [mul_zero, eq_comm, Nat.card_eq_zero, or_iff_left hX.not_infinite] at key

Premises used: eq_comm, MulZeroClass.mul_zero, Finite.not_infinite, or_iff_left, Nat.card_eq_zero
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
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 : IsEmpty X
⊢ B = Set.univ

Tactic:
(IsEmpty.exists_iff.mp hB_ne).elim

Premises used: False.elim, IsEmpty.exists_iff, Iff.mp
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
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 : IsEmpty X
⊢ B = Set.univ

Tactic:
exact (IsEmpty.exists_iff.mp hB_ne).elim

Premises used: False.elim, IsEmpty.exists_iff, Iff.mp
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
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.ncard = ncard.{u_2} (α := X) Set.univ

Tactic:
rw [mul_one, ← Set.ncard_univ] at key

Premises used: mul_one, Set.ncard_univ
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
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
inr inr₁ : Eq.{u_2 + 1} (α := Set X) Set.univ Set.univ
⊢ B = Set.univ

Tactic:
rw [Set.eq_of_subset_of_ncard_le (Set.subset_univ B) key.ge]

Premises used: Eq.ge, Set.subset_univ, Set.eq_of_subset_of_ncard_le
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
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
this : B.ncard < 2
⊢ B.Subsingleton

Tactic:
simp_all
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
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
suffices : B.ncard < 2
⊢ B.Subsingleton

Tactic:
suffices Set.ncard B < 2 by simp_all
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
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 = ∅
inl : LT.lt (α := ℕ) 0 2
⊢ B.ncard < 2

Tactic:
rw [h, Set.ncard_empty]

Premises used: Set.ncard_empty
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
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 = ∅
⊢ LT.lt (α := ℕ) 0 2

Tactic:
simp
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
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
⊢ ¬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'

Premises used: lt_iff_not_ge, MulAction.IsBlock.ncard_block_mul_ncard_orbit_eq
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
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
hB'₁ : ¬2 * (orbit G B).ncard ≤ B.ncard * (orbit G B).ncard
⊢ B.Nonempty

Tactic:
rw [← hB.ncard_block_mul_ncard_orbit_eq h, lt_iff_not_ge] at hB'

Premises used: lt_iff_not_ge, MulAction.IsBlock.ncard_block_mul_ncard_orbit_eq
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
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
inr : ¬2 ≤ B.ncard
⊢ B.ncard < 2

Tactic:
rw [← not_le]

Premises used: not_le
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
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
⊢ ¬2 ≤ B.ncard

Tactic:
fun hb ↦ hB' (Nat.mul_le_mul_right _ hb)

Premises used: Nat.mul_le_mul_right, MulAction.orbit, Set.ncard, Not
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
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
⊢ ¬2 ≤ B.ncard

Tactic:
exact fun hb ↦ hB' (Nat.mul_le_mul_right _ hb)

Premises used: Nat.mul_le_mul_right, MulAction.orbit, Set.ncard
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
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 = ∅ ∨ 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)

Premises used: not_le, lt_iff_not_ge, Set.ncard_empty, Set.eq_empty_or_nonempty
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
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)
inr : ∀ (hfB_ne : B.Nonempty), 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)

Tactic:
rcases Set.eq_empty_or_nonempty B with hfB_e | hfB_ne

Premises used: Set.eq_empty_or_nonempty
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
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_e : B = ∅
⊢ IsBlock.{u_1, u_2} G (X := X) (⋂ (k : G), ⋂ (_ : a ∈ k • B), k • B)

Tactic:
simp [hfB_e]
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
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
k : G
hk : a ∈ k • B
⊢ B' ≤ k • B

Tactic:
Set.biInter_subset_of_mem hk

Premises used: Set.Mem, Set.biInter_subset_of_mem
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
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
k : G
hk : a ∈ k • B
⊢ B' ≤ k • B

Tactic:
exact Set.biInter_subset_of_mem hk

Premises used: Set.biInter_subset_of_mem
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
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
⊢ ∀ (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
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
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
obtain : ∀ (b : X) (hb : b ∈ B), B'.Finite
⊢ B'.Finite

Tactic:
obtain ⟨b, hb : b ∈ B⟩ := hfB_ne
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
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
obtain : ∀ (k : G) (hk : k • b = a), B'.Finite
⊢ B'.Finite

Tactic:
obtain ⟨k, hk : k • b = a⟩ := exists_smul_eq G b a

Premises used: MulAction.exists_smul_eq
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
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
k : G
hk : k • b = a
⊢ B'.Finite

Tactic:
apply Set.Finite.subset (Set.Finite.map _ hfB) (hB'₀ k ⟨b, hb, hk⟩)

Premises used: Set.Finite.subset, Set.Finite.map, And.intro, Exists.intro
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
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

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⟩)
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
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'
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
⊢ x ∈ g • B'

Tactic:
simp only [B', Set.mem_iInter, Set.mem_smul_set_iff_inv_smul_mem,
      smul_smul, ← mul_inv_rev] at hg hx ⊢

Premises used: smul_smul, Set.mem_iInter, mul_inv_rev, Set.mem_smul_set_iff_inv_smul_mem
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
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
x : X
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:
fun _ ↦ hx _ ∘ hg _

Premises used: HMul.hMul, Function.comp
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
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
x : X
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:
exact fun _ ↦ hx _ ∘ hg _

Premises used: HMul.hMul, Function.comp
-- Module: Mathlib.GroupTheory.GroupAction.Blocks
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), 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 _