Theorem: Rudio (Jordan/Primitive.lean)

State before:
M : Type u_1
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type ?u.94224
β : Type ?u.94227
inst✝¹ : Group N
inst✝ : MulAction N β
hpGX : IsPreprimitive M α
A : Set α
hfA : Set.Finite A
hA : Set.Nonempty A
hA' : A ≠ ⊤
a b : α
h : a ≠ b
⊢ ∃ g, a ∈ g • A ∧ b ∉ g • A
Tactic:
let B := ⋂ (g : M) (_ : a ∈ g • A), g • A
State after:
M : Type u_1
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type ?u.94224
β : Type ?u.94227
inst✝¹ : Group N
inst✝ : MulAction N β
hpGX : IsPreprimitive M α
A : Set α
hfA : Set.Finite A
hA : Set.Nonempty A
hA' : A ≠ ⊤
a b : α
h : a ≠ b
B : Set α := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
⊢ ∃ g, a ∈ g • A ∧ b ∉ g • A

State before:
M : Type u_1
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type ?u.94224
β : Type ?u.94227
inst✝¹ : Group N
inst✝ : MulAction N β
hpGX : IsPreprimitive M α
A : Set α
hfA : Set.Finite A
hA : Set.Nonempty A
hA' : A ≠ ⊤
a b : α
h : a ≠ b
B : Set α := ⋂ 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
State after:
M : Type u_1
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type ?u.94224
β : Type ?u.94227
inst✝¹ : Group N
inst✝ : MulAction N β
hpGX : IsPreprimitive M α
A : Set α
hfA : Set.Finite A
hA : Set.Nonempty A
hA' : A ≠ ⊤
a b : α
h : a ≠ b
B : Set α := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
⊢ b ∉ B

State before:
M : Type u_1
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type ?u.94224
β : Type ?u.94227
inst✝¹ : Group N
inst✝ : MulAction N β
hpGX : IsPreprimitive M α
A : Set α
hfA : Set.Finite A
hA : Set.Nonempty A
hA' : A ≠ ⊤
a b : α
h : a ≠ b
B : Set α := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
⊢ b ∉ B
Tactic:
suffices B = {a} by rw [this]; rw [Set.mem_singleton_iff]; exact Ne.symm h
State after:
M : Type u_1
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type ?u.94224
β : Type ?u.94227
inst✝¹ : Group N
inst✝ : MulAction N β
hpGX : IsPreprimitive M α
A : Set α
hfA : Set.Finite A
hA : Set.Nonempty A
hA' : A ≠ ⊤
a b : α
h : a ≠ b
B : Set α := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
⊢ B = {a}

State before:
M : Type u_1
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type ?u.94224
β : Type ?u.94227
inst✝¹ : Group N
inst✝ : MulAction N β
hpGX : IsPreprimitive M α
A : Set α
hfA : Set.Finite A
hA : Set.Nonempty A
hA' : A ≠ ⊤
a b : α
h : a ≠ b
B : Set α := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
⊢ B = {a}
Tactic:
cases' hpGX.has_trivial_blocks (IsBlock.of_subset a A hfA) with hyp hyp
State after:
case inl
M : Type u_1
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type ?u.94224
β : Type ?u.94227
inst✝¹ : Group N
inst✝ : MulAction N β
hpGX : IsPreprimitive M α
A : Set α
hfA : Set.Finite A
hA : Set.Nonempty A
hA' : A ≠ ⊤
a b : α
h : a ≠ b
B : Set α := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
hyp : Set.Subsingleton (⋂ k, ⋂ (_ : a ∈ k • A), k • A)
⊢ B = {a}

case inr
M : Type u_1
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type ?u.94224
β : Type ?u.94227
inst✝¹ : Group N
inst✝ : MulAction N β
hpGX : IsPreprimitive M α
A : Set α
hfA : Set.Finite A
hA : Set.Nonempty A
hA' : A ≠ ⊤
a b : α
h : a ≠ b
B : Set α := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
hyp : ⋂ k, ⋂ (_ : a ∈ k • A), k • A = ⊤
⊢ B = {a}

State before:
M : Type u_1
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type ?u.94224
β : Type ?u.94227
inst✝¹ : Group N
inst✝ : MulAction N β
hpGX : IsPreprimitive M α
A : Set α
hfA : Set.Finite A
hA : Set.Nonempty A
hA' : A ≠ ⊤
a b : α
h : a ≠ b
B : Set α := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
this : b ∉ B
⊢ ∃ g, a ∈ g • A ∧ b ∉ g • A
Tactic:
rw [Set.mem_iInter] at this
State after:
M : Type u_1
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type ?u.94224
β : Type ?u.94227
inst✝¹ : Group N
inst✝ : MulAction N β
hpGX : IsPreprimitive M α
A : Set α
hfA : Set.Finite A
hA : Set.Nonempty A
hA' : A ≠ ⊤
a b : α
h : a ≠ b
B : Set α := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
this : ¬∀ (i : M), b ∈ ⋂ (_ : a ∈ i • A), i • A
⊢ ∃ g, a ∈ g • A ∧ b ∉ g • A

State before:
M : Type u_1
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type ?u.94224
β : Type ?u.94227
inst✝¹ : Group N
inst✝ : MulAction N β
hpGX : IsPreprimitive M α
A : Set α
hfA : Set.Finite A
hA : Set.Nonempty A
hA' : A ≠ ⊤
a b : α
h : a ≠ b
B : Set α := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
this : ¬∀ (i : M), 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
State after:
no goals

State before:
M : Type u_1
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type ?u.94224
β : Type ?u.94227
inst✝¹ : Group N
inst✝ : MulAction N β
hpGX : IsPreprimitive M α
A : Set α
hfA : Set.Finite A
hA : Set.Nonempty A
hA' : A ≠ ⊤
a b : α
h : a ≠ b
B : Set α := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
this : B = {a}
⊢ b ∉ B
Tactic:
rw [this]
State after:
M : Type u_1
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type ?u.94224
β : Type ?u.94227
inst✝¹ : Group N
inst✝ : MulAction N β
hpGX : IsPreprimitive M α
A : Set α
hfA : Set.Finite A
hA : Set.Nonempty A
hA' : A ≠ ⊤
a b : α
h : a ≠ b
B : Set α := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
this : B = {a}
⊢ b ∉ {a}

State before:
M : Type u_1
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type ?u.94224
β : Type ?u.94227
inst✝¹ : Group N
inst✝ : MulAction N β
hpGX : IsPreprimitive M α
A : Set α
hfA : Set.Finite A
hA : Set.Nonempty A
hA' : A ≠ ⊤
a b : α
h : a ≠ b
B : Set α := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
this : B = {a}
⊢ b ∉ {a}
Tactic:
rw [Set.mem_singleton_iff]
State after:
M : Type u_1
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type ?u.94224
β : Type ?u.94227
inst✝¹ : Group N
inst✝ : MulAction N β
hpGX : IsPreprimitive M α
A : Set α
hfA : Set.Finite A
hA : Set.Nonempty A
hA' : A ≠ ⊤
a b : α
h : a ≠ b
B : Set α := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
this : B = {a}
⊢ ¬b = a

State before:
M : Type u_1
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type ?u.94224
β : Type ?u.94227
inst✝¹ : Group N
inst✝ : MulAction N β
hpGX : IsPreprimitive M α
A : Set α
hfA : Set.Finite A
hA : Set.Nonempty A
hA' : A ≠ ⊤
a b : α
h : a ≠ b
B : Set α := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
this : B = {a}
⊢ ¬b = a
Tactic:
exact Ne.symm h
State after:
no goals

State before:
case inl
M : Type u_1
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type ?u.94224
β : Type ?u.94227
inst✝¹ : Group N
inst✝ : MulAction N β
hpGX : IsPreprimitive M α
A : Set α
hfA : Set.Finite A
hA : Set.Nonempty A
hA' : A ≠ ⊤
a b : α
h : a ≠ b
B : Set α := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
hyp : Set.Subsingleton (⋂ k, ⋂ (_ : a ∈ k • A), k • A)
⊢ B = {a}
Tactic:
apply Set.Subsingleton.eq_singleton_of_mem hyp
State after:
case inl
M : Type u_1
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type ?u.94224
β : Type ?u.94227
inst✝¹ : Group N
inst✝ : MulAction N β
hpGX : IsPreprimitive M α
A : Set α
hfA : Set.Finite A
hA : Set.Nonempty A
hA' : A ≠ ⊤
a b : α
h : a ≠ b
B : Set α := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
hyp : Set.Subsingleton (⋂ k, ⋂ (_ : a ∈ k • A), k • A)
⊢ a ∈ ⋂ k, ⋂ (_ : a ∈ k • A), k • A

State before:
case inl
M : Type u_1
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type ?u.94224
β : Type ?u.94227
inst✝¹ : Group N
inst✝ : MulAction N β
hpGX : IsPreprimitive M α
A : Set α
hfA : Set.Finite A
hA : Set.Nonempty A
hA' : A ≠ ⊤
a b : α
h : a ≠ b
B : Set α := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
hyp : Set.Subsingleton (⋂ k, ⋂ (_ : a ∈ k • A), k • A)
⊢ a ∈ ⋂ k, ⋂ (_ : a ∈ k • A), k • A
Tactic:
rw [Set.mem_iInter]
State after:
case inl
M : Type u_1
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type ?u.94224
β : Type ?u.94227
inst✝¹ : Group N
inst✝ : MulAction N β
hpGX : IsPreprimitive M α
A : Set α
hfA : Set.Finite A
hA : Set.Nonempty A
hA' : A ≠ ⊤
a b : α
h : a ≠ b
B : Set α := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
hyp : Set.Subsingleton (⋂ k, ⋂ (_ : a ∈ k • A), k • A)
⊢ ∀ (i : M), a ∈ ⋂ (_ : a ∈ i • A), i • A

State before:
case inl
M : Type u_1
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type ?u.94224
β : Type ?u.94227
inst✝¹ : Group N
inst✝ : MulAction N β
hpGX : IsPreprimitive M α
A : Set α
hfA : Set.Finite A
hA : Set.Nonempty A
hA' : A ≠ ⊤
a b : α
h : a ≠ b
B : Set α := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
hyp : Set.Subsingleton (⋂ k, ⋂ (_ : a ∈ k • A), k • A)
⊢ ∀ (i : M), a ∈ ⋂ (_ : a ∈ i • A), i • A
Tactic:
intro g
State after:
case inl
M : Type u_1
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type ?u.94224
β : Type ?u.94227
inst✝¹ : Group N
inst✝ : MulAction N β
hpGX : IsPreprimitive M α
A : Set α
hfA : Set.Finite A
hA : Set.Nonempty A
hA' : A ≠ ⊤
a b : α
h : a ≠ b
B : Set α := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
hyp : Set.Subsingleton (⋂ k, ⋂ (_ : a ∈ k • A), k • A)
g : M
⊢ a ∈ ⋂ (_ : a ∈ g • A), g • A

State before:
case inl
M : Type u_1
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type ?u.94224
β : Type ?u.94227
inst✝¹ : Group N
inst✝ : MulAction N β
hpGX : IsPreprimitive M α
A : Set α
hfA : Set.Finite A
hA : Set.Nonempty A
hA' : A ≠ ⊤
a b : α
h : a ≠ b
B : Set α := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
hyp : Set.Subsingleton (⋂ k, ⋂ (_ : a ∈ k • A), k • A)
g : M
⊢ a ∈ ⋂ (_ : a ∈ g • A), g • A
Tactic:
simp only [Set.mem_iInter, imp_self]
State after:
no goals

State before:
case inr
M : Type u_1
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type ?u.94224
β : Type ?u.94227
inst✝¹ : Group N
inst✝ : MulAction N β
hpGX : IsPreprimitive M α
A : Set α
hfA : Set.Finite A
hA : Set.Nonempty A
hA' : A ≠ ⊤
a b : α
h : a ≠ b
B : Set α := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
hyp : ⋂ k, ⋂ (_ : a ∈ k • A), k • A = ⊤
⊢ B = {a}
Tactic:
change B = ⊤ at hyp
State after:
case inr
M : Type u_1
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type ?u.94224
β : Type ?u.94227
inst✝¹ : Group N
inst✝ : MulAction N β
hpGX : IsPreprimitive M α
A : Set α
hfA : Set.Finite A
hA : Set.Nonempty A
hA' : A ≠ ⊤
a b : α
h : a ≠ b
B : Set α := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
hyp : B = ⊤
⊢ B = {a}

State before:
case inr
M : Type u_1
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type ?u.94224
β : Type ?u.94227
inst✝¹ : Group N
inst✝ : MulAction N β
hpGX : IsPreprimitive M α
A : Set α
hfA : Set.Finite A
hA : Set.Nonempty A
hA' : A ≠ ⊤
a b : α
h : a ≠ b
B : Set α := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
hyp : B = ⊤
⊢ B = {a}
Tactic:
exfalso
State after:
case inr
M : Type u_1
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type ?u.94224
β : Type ?u.94227
inst✝¹ : Group N
inst✝ : MulAction N β
hpGX : IsPreprimitive M α
A : Set α
hfA : Set.Finite A
hA : Set.Nonempty A
hA' : A ≠ ⊤
a b : α
h : a ≠ b
B : Set α := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
hyp : B = ⊤
⊢ False

State before:
case inr
M : Type u_1
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type ?u.94224
β : Type ?u.94227
inst✝¹ : Group N
inst✝ : MulAction N β
hpGX : IsPreprimitive M α
A : Set α
hfA : Set.Finite A
hA : Set.Nonempty A
hA' : A ≠ ⊤
a b : α
h : a ≠ b
B : Set α := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
hyp : B = ⊤
⊢ False
Tactic:
apply hA'
State after:
case inr
M : Type u_1
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type ?u.94224
β : Type ?u.94227
inst✝¹ : Group N
inst✝ : MulAction N β
hpGX : IsPreprimitive M α
A : Set α
hfA : Set.Finite A
hA : Set.Nonempty A
hA' : A ≠ ⊤
a b : α
h : a ≠ b
B : Set α := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
hyp : B = ⊤
⊢ A = ⊤

State before:
case inr
M : Type u_1
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type ?u.94224
β : Type ?u.94227
inst✝¹ : Group N
inst✝ : MulAction N β
hpGX : IsPreprimitive M α
A : Set α
hfA : Set.Finite A
hA : Set.Nonempty A
hA' : A ≠ ⊤
a b : α
h : a ≠ b
B : Set α := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
hyp : B = ⊤
⊢ A = ⊤
Tactic:
suffices ∃ g : M, a ∈ g • A by
  obtain ⟨g, hg⟩ := this
  have : B ≤ g • A := Set.biInter_subset_of_mem hg
  rw [hyp, top_le_iff, ← eq_inv_smul_iff] at this
  rw [this, Set.top_eq_univ, Set.smul_set_univ]
State after:
case inr
M : Type u_1
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type ?u.94224
β : Type ?u.94227
inst✝¹ : Group N
inst✝ : MulAction N β
hpGX : IsPreprimitive M α
A : Set α
hfA : Set.Finite A
hA : Set.Nonempty A
hA' : A ≠ ⊤
a b : α
h : a ≠ b
B : Set α := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
hyp : B = ⊤
⊢ ∃ g, a ∈ g • A

State before:
case inr
M : Type u_1
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type ?u.94224
β : Type ?u.94227
inst✝¹ : Group N
inst✝ : MulAction N β
hpGX : IsPreprimitive M α
A : Set α
hfA : Set.Finite A
hA : Set.Nonempty A
hA' : A ≠ ⊤
a b : α
h : a ≠ b
B : Set α := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
hyp : B = ⊤
⊢ ∃ g, a ∈ g • A
Tactic:
obtain ⟨x, hx⟩ := hA
State after:
case inr.intro
M : Type u_1
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type ?u.94224
β : Type ?u.94227
inst✝¹ : Group N
inst✝ : MulAction N β
hpGX : IsPreprimitive M α
A : Set α
hfA : Set.Finite A
hA' : A ≠ ⊤
a b : α
h : a ≠ b
B : Set α := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
hyp : B = ⊤
x : α
hx : x ∈ A
⊢ ∃ g, a ∈ g • A

State before:
case inr.intro
M : Type u_1
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type ?u.94224
β : Type ?u.94227
inst✝¹ : Group N
inst✝ : MulAction N β
hpGX : IsPreprimitive M α
A : Set α
hfA : Set.Finite A
hA' : A ≠ ⊤
a b : α
h : a ≠ b
B : Set α := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
hyp : B = ⊤
x : α
hx : x ∈ A
⊢ ∃ g, a ∈ g • A
Tactic:
obtain ⟨g, hg⟩ := MulAction.exists_smul_eq M x a
State after:
case inr.intro.intro
M : Type u_1
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type ?u.94224
β : Type ?u.94227
inst✝¹ : Group N
inst✝ : MulAction N β
hpGX : IsPreprimitive M α
A : Set α
hfA : Set.Finite A
hA' : A ≠ ⊤
a b : α
h : a ≠ b
B : Set α := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
hyp : B = ⊤
x : α
hx : x ∈ A
g : M
hg : g • x = a
⊢ ∃ g, a ∈ g • A

State before:
case inr.intro.intro
M : Type u_1
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type ?u.94224
β : Type ?u.94227
inst✝¹ : Group N
inst✝ : MulAction N β
hpGX : IsPreprimitive M α
A : Set α
hfA : Set.Finite A
hA' : A ≠ ⊤
a b : α
h : a ≠ b
B : Set α := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
hyp : B = ⊤
x : α
hx : x ∈ A
g : M
hg : g • x = a
⊢ ∃ g, a ∈ g • A
Tactic:
use g
State after:
case h
M : Type u_1
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type ?u.94224
β : Type ?u.94227
inst✝¹ : Group N
inst✝ : MulAction N β
hpGX : IsPreprimitive M α
A : Set α
hfA : Set.Finite A
hA' : A ≠ ⊤
a b : α
h : a ≠ b
B : Set α := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
hyp : B = ⊤
x : α
hx : x ∈ A
g : M
hg : g • x = a
⊢ a ∈ g • A

State before:
case h
M : Type u_1
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type ?u.94224
β : Type ?u.94227
inst✝¹ : Group N
inst✝ : MulAction N β
hpGX : IsPreprimitive M α
A : Set α
hfA : Set.Finite A
hA' : A ≠ ⊤
a b : α
h : a ≠ b
B : Set α := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
hyp : B = ⊤
x : α
hx : x ∈ A
g : M
hg : g • x = a
⊢ a ∈ g • A
Tactic:
use x
State after:
no goals

State before:
M : Type u_1
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type ?u.94224
β : Type ?u.94227
inst✝¹ : Group N
inst✝ : MulAction N β
hpGX : IsPreprimitive M α
A : Set α
hfA : Set.Finite A
hA : Set.Nonempty A
hA' : A ≠ ⊤
a b : α
h : a ≠ b
B : Set α := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
hyp : B = ⊤
this : ∃ g, a ∈ g • A
⊢ A = ⊤
Tactic:
obtain ⟨g, hg⟩ := this
State after:
case intro
M : Type u_1
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type ?u.94224
β : Type ?u.94227
inst✝¹ : Group N
inst✝ : MulAction N β
hpGX : IsPreprimitive M α
A : Set α
hfA : Set.Finite A
hA : Set.Nonempty A
hA' : A ≠ ⊤
a b : α
h : a ≠ b
B : Set α := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
hyp : B = ⊤
g : M
hg : a ∈ g • A
⊢ A = ⊤

State before:
case intro
M : Type u_1
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type ?u.94224
β : Type ?u.94227
inst✝¹ : Group N
inst✝ : MulAction N β
hpGX : IsPreprimitive M α
A : Set α
hfA : Set.Finite A
hA : Set.Nonempty A
hA' : A ≠ ⊤
a b : α
h : a ≠ b
B : Set α := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
hyp : B = ⊤
g : M
hg : a ∈ g • A
⊢ A = ⊤
Tactic:
have : B ≤ g • A := Set.biInter_subset_of_mem hg
State after:
case intro
M : Type u_1
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type ?u.94224
β : Type ?u.94227
inst✝¹ : Group N
inst✝ : MulAction N β
hpGX : IsPreprimitive M α
A : Set α
hfA : Set.Finite A
hA : Set.Nonempty A
hA' : A ≠ ⊤
a b : α
h : a ≠ b
B : Set α := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
hyp : B = ⊤
g : M
hg : a ∈ g • A
this : B ≤ g • A
⊢ A = ⊤

State before:
case intro
M : Type u_1
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type ?u.94224
β : Type ?u.94227
inst✝¹ : Group N
inst✝ : MulAction N β
hpGX : IsPreprimitive M α
A : Set α
hfA : Set.Finite A
hA : Set.Nonempty A
hA' : A ≠ ⊤
a b : α
h : a ≠ b
B : Set α := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
hyp : B = ⊤
g : M
hg : a ∈ g • A
this : B ≤ g • A
⊢ A = ⊤
Tactic:
rw [hyp, top_le_iff, ← eq_inv_smul_iff] at this
State after:
case intro
M : Type u_1
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type ?u.94224
β : Type ?u.94227
inst✝¹ : Group N
inst✝ : MulAction N β
hpGX : IsPreprimitive M α
A : Set α
hfA : Set.Finite A
hA : Set.Nonempty A
hA' : A ≠ ⊤
a b : α
h : a ≠ b
B : Set α := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
hyp : B = ⊤
g : M
hg : a ∈ g • A
this : A = g⁻¹ • ⊤
⊢ A = ⊤

State before:
case intro
M : Type u_1
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type ?u.94224
β : Type ?u.94227
inst✝¹ : Group N
inst✝ : MulAction N β
hpGX : IsPreprimitive M α
A : Set α
hfA : Set.Finite A
hA : Set.Nonempty A
hA' : A ≠ ⊤
a b : α
h : a ≠ b
B : Set α := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
hyp : B = ⊤
g : M
hg : a ∈ g • A
this : A = g⁻¹ • ⊤
⊢ A = ⊤
Tactic:
rw [this, Set.top_eq_univ, Set.smul_set_univ]
State after:
no goals