-- Mathlib/GroupTheory/GroupAction/Blocks.lean
theorem of_subset (a : X) (hfB : B.Finite) :
    IsBlock G (⋂ (k : G) (_ : a ∈ k • B), k • B)

Proof state:
case inr.intro.intro.intro
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
B : Set X
a : X
hfB : B.Finite
B' : Set X := ⋂ k, ⋂ (_ : 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), 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'
⊢ g • ⋂ k, ⋂ (_ : a ∈ k • B), k • B = ⋂ k, ⋂ (_ : a ∈ k • B), k • B

Tactic:
rw [← smul_eq_iff_eq_inv_smul] at hkB' hgkB'

Result:
case inr.intro.intro.intro
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
B : Set X
a : X
hfB : B.Finite
B' : Set X := ⋂ k, ⋂ (_ : 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), 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' : k • B' = B'
hgkB' : k • B' = g • B'
⊢ g • ⋂ k, ⋂ (_ : a ∈ k • B), k • B = ⋂ k, ⋂ (_ : a ∈ k • B), k • B

Proof state:
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
B : Set X
a : X
hfB : B.Finite
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
⊢ IsBlock G (⋂ k, ⋂ (_ : a ∈ k • B), k • B)

Tactic:
rcases Set.eq_empty_or_nonempty B with hfB_e | hfB_ne

Result:
case inl
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
B : Set X
a : X
hfB : B.Finite
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_e : B = ∅
⊢ IsBlock G (⋂ k, ⋂ (_ : a ∈ k • B), k • B)

case inr
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
B : Set X
a : X
hfB : B.Finite
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : B.Nonempty
⊢ IsBlock G (⋂ k, ⋂ (_ : a ∈ k • B), k • B)

Proof state:
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
B : Set X
a : X
hfB : B.Finite
B' : Set X := ⋂ k, ⋂ (_ : 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⁻¹ • a ∈ B → (g * i)⁻¹ • a ∈ B
hx : ∀ (i : G), i⁻¹ • a ∈ B → i⁻¹ • x ∈ B
⊢ ∀ (i : G), i⁻¹ • a ∈ B → (g * i)⁻¹ • x ∈ B

Tactic:
exact fun _ ↦ hx _ ∘ hg _

Result:
no goals

Proof state:
case inr
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
B : Set X
a : X
hfB : B.Finite
B' : Set X := ⋂ k, ⋂ (_ : 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), a ∈ g • B' → B' = g • B'
⊢ IsBlock G (⋂ k, ⋂ (_ : a ∈ k • B), k • B)

Tactic:
rw [isBlock_iff_smul_eq_of_nonempty]

Result:
case inr
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
B : Set X
a : X
hfB : B.Finite
B' : Set X := ⋂ k, ⋂ (_ : 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), a ∈ g • B' → B' = g • B'
⊢ ∀ ⦃g : G⦄,
    ((g • ⋂ k, ⋂ (_ : a ∈ k • B), k • B) ∩ ⋂ k, ⋂ (_ : a ∈ k • B), k • B).Nonempty →
      g • ⋂ k, ⋂ (_ : a ∈ k • B), k • B = ⋂ k, ⋂ (_ : a ∈ k • B), k • B

Proof state:
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
B : Set X
a : X
hfB : B.Finite
B' : Set X := ⋂ k, ⋂ (_ : 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

Result:
no goals

Proof state:
case inr
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
B : Set X
a : X
hfB : B.Finite
B' : Set X := ⋂ k, ⋂ (_ : 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), a ∈ g • B' → B' = g • B'
⊢ ∀ ⦃g : G⦄,
    ((g • ⋂ k, ⋂ (_ : a ∈ k • B), k • B) ∩ ⋂ k, ⋂ (_ : a ∈ k • B), k • B).Nonempty →
      g • ⋂ k, ⋂ (_ : a ∈ k • B), k • B = ⋂ k, ⋂ (_ : a ∈ k • B), k • B

Tactic:
rintro g ⟨b : X, hb' : b ∈ g • B', hb : b ∈ B'⟩

Result:
case inr.intro.intro
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
B : Set X
a : X
hfB : B.Finite
B' : Set X := ⋂ k, ⋂ (_ : 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), a ∈ g • B' → B' = g • B'
g : G
b : X
hb' : b ∈ g • B'
hb : b ∈ B'
⊢ g • ⋂ k, ⋂ (_ : a ∈ k • B), k • B = ⋂ k, ⋂ (_ : a ∈ k • B), k • B

Proof state:
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
B : Set X
a : X
hfB : B.Finite
B' : Set X := ⋂ k, ⋂ (_ : 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'

Tactic:
rw [eq_comm, ← mem_stabilizer_iff, mem_stabilizer_set_iff_subset_smul_set hfB']

Result:
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
B : Set X
a : X
hfB : B.Finite
B' : Set X := ⋂ k, ⋂ (_ : 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'

Proof state:
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
B : Set X
a : X
hfB : B.Finite
B' : Set X := ⋂ k, ⋂ (_ : 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), 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'
⊢ b ∈ g • B'

Tactic:
exact hb'

Result:
no goals

Proof state:
case inr
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
B : Set X
a : X
hfB : B.Finite
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : B.Nonempty
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
hfB' : B'.Finite
⊢ IsBlock G (⋂ k, ⋂ (_ : a ∈ k • B), k • B)

Tactic:
have hag : ∀ g : G, a ∈ g • B' → B' ≤ g • B' :=  by
  intro g hg x hx
  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 _

Result:
case inr
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
B : Set X
a : X
hfB : B.Finite
B' : Set X := ⋂ k, ⋂ (_ : 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 G (⋂ k, ⋂ (_ : a ∈ k • B), k • B)

Proof state:
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
B : Set X
a : X
hfB : B.Finite
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : B.Nonempty
⊢ ∀ (k : G), a ∈ k • B → B' ≤ k • B

Tactic:
intro k hk

Result:
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
B : Set X
a : X
hfB : B.Finite
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : B.Nonempty
k : G
hk : a ∈ k • B
⊢ B' ≤ k • B