-- Mathlib/GroupTheory/GroupAction/Primitive.lean
theorem exists_mem_smul_and_not_mem_smul [IsPreprimitive G X]
    {A : Set X} (hfA : A.Finite) (hA : A.Nonempty) (hA' : A ≠ .univ) {a b : X} (h : a ≠ b) :
    ∃ g : G, a ∈ g • A ∧ b ∉ g • A

Proof state:
G : Type u_1
X : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G X
inst✝ : IsPreprimitive G X
A : Set X
hfA : A.Finite
hA : A.Nonempty
hA' : A ≠ Set.univ
a b : X
h : a ≠ b
B : Set X := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
hyp : B = ⊤
this : ∃ g, a ∈ g • A
⊢ A = Set.univ

Tactic:
obtain ⟨g, hg⟩ := this

Result:
case intro
G : Type u_1
X : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G X
inst✝ : IsPreprimitive G X
A : Set X
hfA : A.Finite
hA : A.Nonempty
hA' : A ≠ Set.univ
a b : X
h : a ≠ b
B : Set X := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
hyp : B = ⊤
g : G
hg : a ∈ g • A
⊢ A = Set.univ

Proof state:
case inl
G : Type u_1
X : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G X
inst✝ : IsPreprimitive G X
A : Set X
hfA : A.Finite
hA : A.Nonempty
hA' : A ≠ Set.univ
a b : X
h : a ≠ b
B : Set X := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
hyp : (⋂ k, ⋂ (_ : a ∈ k • A), k • A).Subsingleton
⊢ a ∈ ⋂ k, ⋂ (_ : a ∈ k • A), k • A

Tactic:
rw [Set.mem_iInter]

Result:
case inl
G : Type u_1
X : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G X
inst✝ : IsPreprimitive G X
A : Set X
hfA : A.Finite
hA : A.Nonempty
hA' : A ≠ Set.univ
a b : X
h : a ≠ b
B : Set X := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
hyp : (⋂ k, ⋂ (_ : a ∈ k • A), k • A).Subsingleton
⊢ ∀ (i : G), a ∈ ⋂ (_ : a ∈ i • A), i • A

Proof state:
G : Type u_1
X : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G X
inst✝ : IsPreprimitive G X
A : Set X
hfA : A.Finite
hA : A.Nonempty
hA' : A ≠ Set.univ
a b : X
h : a ≠ b
B : Set X := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
this : b ∉ B
⊢ ∃ g, a ∈ g • A ∧ b ∉ g • A

Tactic:
rw [Set.mem_iInter] at this

Result:
G : Type u_1
X : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G X
inst✝ : IsPreprimitive G X
A : Set X
hfA : A.Finite
hA : A.Nonempty
hA' : A ≠ Set.univ
a b : X
h : a ≠ b
B : Set X := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
this : ¬∀ (i : G), b ∈ ⋂ (_ : a ∈ i • A), i • A
⊢ ∃ g, a ∈ g • A ∧ b ∉ g • A

Proof state:
case intro
G : Type u_1
X : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G X
inst✝ : IsPreprimitive G X
A : Set X
hfA : A.Finite
hA : A.Nonempty
hA' : A ≠ Set.univ
a b : X
h : a ≠ b
B : Set X := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
hyp : B = ⊤
g : G
hg : a ∈ g • A
this : B ≤ g • A
⊢ A = Set.univ

Tactic:
rw [hyp, top_le_iff, ← eq_inv_smul_iff] at this

Result:
case intro
G : Type u_1
X : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G X
inst✝ : IsPreprimitive G X
A : Set X
hfA : A.Finite
hA : A.Nonempty
hA' : A ≠ Set.univ
a b : X
h : a ≠ b
B : Set X := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
hyp : B = ⊤
g : G
hg : a ∈ g • A
this : A = g⁻¹ • ⊤
⊢ A = Set.univ

Proof state:
G : Type u_1
X : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G X
inst✝ : IsPreprimitive G X
A : Set X
hfA : A.Finite
hA : A.Nonempty
hA' : A ≠ Set.univ
a b : X
h : a ≠ b
B : Set X := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
⊢ ∃ g, a ∈ g • A ∧ b ∉ g • A

Tactic:
suffices b ∉ B by
  rw [Set.mem_iInter] at this
  simpa only [Set.mem_iInter, not_forall, exists_prop] using this

Result:
G : Type u_1
X : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G X
inst✝ : IsPreprimitive G X
A : Set X
hfA : A.Finite
hA : A.Nonempty
hA' : A ≠ Set.univ
a b : X
h : a ≠ b
B : Set X := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
⊢ b ∉ B

Proof state:
case inr
G : Type u_1
X : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G X
inst✝ : IsPreprimitive G X
A : Set X
hfA : A.Finite
hA : A.Nonempty
hA' : A ≠ Set.univ
a b : X
h : a ≠ b
B : Set X := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
hyp : B = ⊤
⊢ ∃ g, a ∈ g • A

Tactic:
obtain ⟨x, hx⟩ := hA

Result:
case inr.intro
G : Type u_1
X : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G X
inst✝ : IsPreprimitive G X
A : Set X
hfA : A.Finite
hA' : A ≠ Set.univ
a b : X
h : a ≠ b
B : Set X := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
hyp : B = ⊤
x : X
hx : x ∈ A
⊢ ∃ g, a ∈ g • A

Proof state:
case inr
G : Type u_1
X : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G X
inst✝ : IsPreprimitive G X
A : Set X
hfA : A.Finite
hA : A.Nonempty
hA' : A ≠ Set.univ
a b : X
h : a ≠ b
B : Set X := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
hyp : ⋂ k, ⋂ (_ : a ∈ k • A), k • A = Set.univ
⊢ B = {a}

Tactic:
change B = ⊤ at hyp

Result:
case inr
G : Type u_1
X : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G X
inst✝ : IsPreprimitive G X
A : Set X
hfA : A.Finite
hA : A.Nonempty
hA' : A ≠ Set.univ
a b : X
h : a ≠ b
B : Set X := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
hyp : B = ⊤
⊢ B = {a}

Proof state:
case inl
G : Type u_1
X : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G X
inst✝ : IsPreprimitive G X
A : Set X
hfA : A.Finite
hA : A.Nonempty
hA' : A ≠ Set.univ
a b : X
h : a ≠ b
B : Set X := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
hyp : (⋂ k, ⋂ (_ : a ∈ k • A), k • A).Subsingleton
⊢ B = {a}

Tactic:
apply Set.Subsingleton.eq_singleton_of_mem hyp

Result:
case inl
G : Type u_1
X : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G X
inst✝ : IsPreprimitive G X
A : Set X
hfA : A.Finite
hA : A.Nonempty
hA' : A ≠ Set.univ
a b : X
h : a ≠ b
B : Set X := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
hyp : (⋂ k, ⋂ (_ : a ∈ k • A), k • A).Subsingleton
⊢ a ∈ ⋂ k, ⋂ (_ : a ∈ k • A), k • A

Proof state:
G : Type u_1
X : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G X
inst✝ : IsPreprimitive G X
A : Set X
hfA : A.Finite
hA : A.Nonempty
hA' : A ≠ Set.univ
a b : X
h : a ≠ b
B : Set X := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
this : ¬∀ (i : G), b ∈ ⋂ (_ : a ∈ i • A), i • A
⊢ ∃ g, a ∈ g • A ∧ b ∉ g • A

Tactic:
simpa only [Set.mem_iInter, not_forall, exists_prop] using this

Result:
no goals

Proof state:
G : Type u_1
X : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G X
inst✝ : IsPreprimitive G X
A : Set X
hfA : A.Finite
hA : A.Nonempty
hA' : A ≠ Set.univ
a b : X
h : a ≠ b
B : Set X := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
⊢ b ∉ B

Tactic:
suffices B = {a} by rw [this]; rw [Set.mem_singleton_iff]; exact Ne.symm h

Result:
G : Type u_1
X : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G X
inst✝ : IsPreprimitive G X
A : Set X
hfA : A.Finite
hA : A.Nonempty
hA' : A ≠ Set.univ
a b : X
h : a ≠ b
B : Set X := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
⊢ B = {a}