Theorem: MulAction.stabilizer.isMultiplyPreprimitive (Jordan/MultiplePrimitivity.lean)

State before:
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
⊢ IsMultiplyPreprimitive M α (Nat.succ n) ↔
    IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
Tactic:
let h_eq := h.exists_smul_eq
State after:
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
⊢ IsMultiplyPreprimitive M α (Nat.succ n) ↔
    IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n

State before:
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
⊢ IsMultiplyPreprimitive M α (Nat.succ n) ↔
    IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
Tactic:
constructor
State after:
case mp
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
⊢ IsMultiplyPreprimitive M α (Nat.succ n) →
    IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n

case mpr
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
⊢ IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n →
    IsMultiplyPreprimitive M α (Nat.succ n)

State before:
case mp
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
⊢ IsMultiplyPreprimitive M α (Nat.succ n) →
    IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
Tactic:
intro hn
State after:
case mp
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn✝ : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn : IsMultiplyPreprimitive M α (Nat.succ n)
⊢ IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n

State before:
case mp
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn✝ : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn : IsMultiplyPreprimitive M α (Nat.succ n)
⊢ IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
Tactic:
cases' Nat.lt_or_ge n 1 with h0 h1
State after:
case mp.inl
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn✝ : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn : IsMultiplyPreprimitive M α (Nat.succ n)
h0 : n < 1
⊢ IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n

case mp.inr
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn✝ : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn : IsMultiplyPreprimitive M α (Nat.succ n)
h1 : n ≥ 1
⊢ IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n

State before:
case mp.inr
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn✝ : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn : IsMultiplyPreprimitive M α (Nat.succ n)
h1 : n ≥ 1
⊢ IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
Tactic:
constructor
State after:
case mp.inr.left
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn✝ : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn : IsMultiplyPreprimitive M α (Nat.succ n)
h1 : n ≥ 1
⊢ IsMultiplyPretransitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n

case mp.inr.right
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn✝ : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn : IsMultiplyPreprimitive M α (Nat.succ n)
h1 : n ≥ 1
⊢ ∀ (s : Set ↥(SubMulAction.ofStabilizer M a)),
    Set.encard s + 1 = ↑n →
      IsPreprimitive ↥(fixingSubgroup (↥(stabilizer M a)) s) ↥(SubMulAction.ofFixingSubgroup (↥(stabilizer M a)) s)

State before:
case mp.inr.left
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn✝ : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn : IsMultiplyPreprimitive M α (Nat.succ n)
h1 : n ≥ 1
⊢ IsMultiplyPretransitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n

case mp.inr.right
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn✝ : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn : IsMultiplyPreprimitive M α (Nat.succ n)
h1 : n ≥ 1
⊢ ∀ (s : Set ↥(SubMulAction.ofStabilizer M a)),
    Set.encard s + 1 = ↑n →
      IsPreprimitive ↥(fixingSubgroup (↥(stabilizer M a)) s) ↥(SubMulAction.ofFixingSubgroup (↥(stabilizer M a)) s)
Tactic:
exact (stabilizer.isMultiplyPretransitive M α h).mp hn.left
State after:
case mp.inr.right
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn✝ : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn : IsMultiplyPreprimitive M α (Nat.succ n)
h1 : n ≥ 1
⊢ ∀ (s : Set ↥(SubMulAction.ofStabilizer M a)),
    Set.encard s + 1 = ↑n →
      IsPreprimitive ↥(fixingSubgroup (↥(stabilizer M a)) s) ↥(SubMulAction.ofFixingSubgroup (↥(stabilizer M a)) s)

State before:
case mp.inr.right
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn✝ : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn : IsMultiplyPreprimitive M α (Nat.succ n)
h1 : n ≥ 1
⊢ ∀ (s : Set ↥(SubMulAction.ofStabilizer M a)),
    Set.encard s + 1 = ↑n →
      IsPreprimitive ↥(fixingSubgroup (↥(stabilizer M a)) s) ↥(SubMulAction.ofFixingSubgroup (↥(stabilizer M a)) s)
Tactic:
intro s hs
State after:
case mp.inr.right
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn✝ : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn : IsMultiplyPreprimitive M α (Nat.succ n)
h1 : n ≥ 1
s : Set ↥(SubMulAction.ofStabilizer M a)
hs : Set.encard s + 1 = ↑n
⊢ IsPreprimitive ↥(fixingSubgroup (↥(stabilizer M a)) s) ↥(SubMulAction.ofFixingSubgroup (↥(stabilizer M a)) s)

State before:
case mp.inr.right
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn✝ : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn : IsMultiplyPreprimitive M α (Nat.succ n)
h1 : n ≥ 1
s : Set ↥(SubMulAction.ofStabilizer M a)
hs : Set.encard s + 1 = ↑n
⊢ IsPreprimitive ↥(fixingSubgroup (↥(stabilizer M a)) s) ↥(SubMulAction.ofFixingSubgroup (↥(stabilizer M a)) s)
Tactic:
apply isPreprimitive_of_surjective_map
    (SubMulAction.equivariantMap_ofFixingSubgroup_to_ofStabilizer_bijective M a s).surjective
State after:
case mp.inr.right
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn✝ : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn : IsMultiplyPreprimitive M α (Nat.succ n)
h1 : n ≥ 1
s : Set ↥(SubMulAction.ofStabilizer M a)
hs : Set.encard s + 1 = ↑n
⊢ IsPreprimitive ↥(fixingSubgroup M (insert a (Subtype.val '' s)))
    ↥(SubMulAction.ofFixingSubgroup M (insert a (Subtype.val '' s)))

State before:
case mp.inr.right
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn✝ : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn : IsMultiplyPreprimitive M α (Nat.succ n)
h1 : n ≥ 1
s : Set ↥(SubMulAction.ofStabilizer M a)
hs : Set.encard s + 1 = ↑n
⊢ IsPreprimitive ↥(fixingSubgroup M (insert a (Subtype.val '' s)))
    ↥(SubMulAction.ofFixingSubgroup M (insert a (Subtype.val '' s)))
Tactic:
apply hn.right
State after:
case mp.inr.right.x
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn✝ : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn : IsMultiplyPreprimitive M α (Nat.succ n)
h1 : n ≥ 1
s : Set ↥(SubMulAction.ofStabilizer M a)
hs : Set.encard s + 1 = ↑n
⊢ Set.encard (insert a (Subtype.val '' s)) + 1 = ↑(Nat.succ n)

State before:
case mp.inr.right.x
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn✝ : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn : IsMultiplyPreprimitive M α (Nat.succ n)
h1 : n ≥ 1
s : Set ↥(SubMulAction.ofStabilizer M a)
hs : Set.encard s + 1 = ↑n
⊢ Set.encard (insert a (Subtype.val '' s)) + 1 = ↑(Nat.succ n)
Tactic:
rw [Set.encard_insert_of_not_mem, Subtype.coe_injective.encard_image, hs, Nat.cast_succ]
State after:
case mp.inr.right.x
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn✝ : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn : IsMultiplyPreprimitive M α (Nat.succ n)
h1 : n ≥ 1
s : Set ↥(SubMulAction.ofStabilizer M a)
hs : Set.encard s + 1 = ↑n
⊢ a ∉ Subtype.val '' s

State before:
case mp.inl
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn✝ : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn : IsMultiplyPreprimitive M α (Nat.succ n)
h0 : n < 1
⊢ IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
Tactic:
rw [Nat.lt_one_iff] at h0
State after:
case mp.inl
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn✝ : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn : IsMultiplyPreprimitive M α (Nat.succ n)
h0 : n = 0
⊢ IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n

State before:
case mp.inl
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn✝ : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn : IsMultiplyPreprimitive M α (Nat.succ n)
h0 : n = 0
⊢ IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
Tactic:
rw [h0]
State after:
case mp.inl
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn✝ : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn : IsMultiplyPreprimitive M α (Nat.succ n)
h0 : n = 0
⊢ IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) 0

State before:
case mp.inl
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn✝ : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn : IsMultiplyPreprimitive M α (Nat.succ n)
h0 : n = 0
⊢ IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) 0
Tactic:
apply isMultiplyPreprimitive_zero
State after:
no goals

State before:
case mp.inr.right.x
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn✝ : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn : IsMultiplyPreprimitive M α (Nat.succ n)
h1 : n ≥ 1
s : Set ↥(SubMulAction.ofStabilizer M a)
hs : Set.encard s + 1 = ↑n
⊢ a ∉ Subtype.val '' s
Tactic:
intro ha
State after:
case mp.inr.right.x
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn✝ : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn : IsMultiplyPreprimitive M α (Nat.succ n)
h1 : n ≥ 1
s : Set ↥(SubMulAction.ofStabilizer M a)
hs : Set.encard s + 1 = ↑n
ha : a ∈ Subtype.val '' s
⊢ False

State before:
case mp.inr.right.x
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn✝ : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn : IsMultiplyPreprimitive M α (Nat.succ n)
h1 : n ≥ 1
s : Set ↥(SubMulAction.ofStabilizer M a)
hs : Set.encard s + 1 = ↑n
ha : a ∈ Subtype.val '' s
⊢ False
Tactic:
simp only [Set.mem_image, Subtype.exists, exists_and_right, exists_eq_right] at ha
State after:
case mp.inr.right.x
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn✝ : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn : IsMultiplyPreprimitive M α (Nat.succ n)
h1 : n ≥ 1
s : Set ↥(SubMulAction.ofStabilizer M a)
hs : Set.encard s + 1 = ↑n
ha : ∃ (x : a ∈ SubMulAction.ofStabilizer M a), { val := a, property := ⋯ } ∈ s
⊢ False

State before:
case mp.inr.right.x
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn✝ : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn : IsMultiplyPreprimitive M α (Nat.succ n)
h1 : n ≥ 1
s : Set ↥(SubMulAction.ofStabilizer M a)
hs : Set.encard s + 1 = ↑n
ha : ∃ (x : a ∈ SubMulAction.ofStabilizer M a), { val := a, property := ⋯ } ∈ s
⊢ False
Tactic:
obtain ⟨b, _⟩ := ha
State after:
case mp.inr.right.x.intro
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn✝ : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn : IsMultiplyPreprimitive M α (Nat.succ n)
h1 : n ≥ 1
s : Set ↥(SubMulAction.ofStabilizer M a)
hs : Set.encard s + 1 = ↑n
b : a ∈ SubMulAction.ofStabilizer M a
h✝ : { val := a, property := ⋯ } ∈ s
⊢ False

State before:
case mp.inr.right.x.intro
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn✝ : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn : IsMultiplyPreprimitive M α (Nat.succ n)
h1 : n ≥ 1
s : Set ↥(SubMulAction.ofStabilizer M a)
hs : Set.encard s + 1 = ↑n
b : a ∈ SubMulAction.ofStabilizer M a
h✝ : { val := a, property := ⋯ } ∈ s
⊢ False
Tactic:
apply b
State after:
case mp.inr.right.x.intro
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn✝ : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn : IsMultiplyPreprimitive M α (Nat.succ n)
h1 : n ≥ 1
s : Set ↥(SubMulAction.ofStabilizer M a)
hs : Set.encard s + 1 = ↑n
b : a ∈ SubMulAction.ofStabilizer M a
h✝ : { val := a, property := ⋯ } ∈ s
⊢ a ∈ {a}

State before:
case mp.inr.right.x.intro
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn✝ : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn : IsMultiplyPreprimitive M α (Nat.succ n)
h1 : n ≥ 1
s : Set ↥(SubMulAction.ofStabilizer M a)
hs : Set.encard s + 1 = ↑n
b : a ∈ SubMulAction.ofStabilizer M a
h✝ : { val := a, property := ⋯ } ∈ s
⊢ a ∈ {a}
Tactic:
simp only [Set.mem_singleton_iff]
State after:
no goals

State before:
case mpr
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
⊢ IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n →
    IsMultiplyPreprimitive M α (Nat.succ n)
Tactic:
intro hn_0
State after:
case mpr
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
⊢ IsMultiplyPreprimitive M α (Nat.succ n)

State before:
case mpr
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
⊢ IsMultiplyPreprimitive M α (Nat.succ n)
Tactic:
constructor
State after:
case mpr.left
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
⊢ IsMultiplyPretransitive M α (Nat.succ n)

case mpr.right
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
⊢ ∀ (s : Set α),
    Set.encard s + 1 = ↑(Nat.succ n) → IsPreprimitive ↥(fixingSubgroup M s) ↥(SubMulAction.ofFixingSubgroup M s)

State before:
case mpr.left
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
⊢ IsMultiplyPretransitive M α (Nat.succ n)
Tactic:
rw [stabilizer.isMultiplyPretransitive M α h]
State after:
case mpr.left
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
⊢ IsMultiplyPretransitive (↥(stabilizer M ?m.25588)) (↥(SubMulAction.ofStabilizer M ?m.25588)) n

M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
⊢ α

State before:
case mpr.left
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
⊢ IsMultiplyPretransitive (↥(stabilizer M ?m.25588)) (↥(SubMulAction.ofStabilizer M ?m.25588)) n

M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
⊢ α
Tactic:
exact hn_0.left
State after:
no goals

State before:
case mpr.right
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
⊢ ∀ (s : Set α),
    Set.encard s + 1 = ↑(Nat.succ n) → IsPreprimitive ↥(fixingSubgroup M s) ↥(SubMulAction.ofFixingSubgroup M s)
Tactic:
suffices
  ∀ (s : Set α) (_ : s.encard + 1 = n.succ) (_ : a ∈ s),
    IsPreprimitive (fixingSubgroup M s) (SubMulAction.ofFixingSubgroup M s) by
  intro s hs
  have : ∃ b : α, b ∈ s := by
    rw [← Set.nonempty_def, Set.nonempty_iff_ne_empty]
    intro h
    apply not_lt.mpr hn
    rw [h, Set.encard_empty, zero_add, ← Nat.cast_one, Nat.cast_inj, Nat.succ_inj'] at hs
    simp only [← hs, zero_lt_one]
  obtain ⟨b, hb⟩ := this
  obtain ⟨g, hg : g • b = a⟩ := h_eq b a
  apply isPreprimitive_of_surjective_map
    (SubMulAction.conjMap_ofFixingSubgroup_bijective M (inv_smul_smul g s)).surjective
  refine' this (g • s) _ ⟨b, hb, hg⟩
  rw [smul_set_encard_eq, hs]
State after:
case mpr.right
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
⊢ ∀ (s : Set α),
    Set.encard s + 1 = ↑(Nat.succ n) → a ∈ s → IsPreprimitive ↥(fixingSubgroup M s) ↥(SubMulAction.ofFixingSubgroup M s)

State before:
case mpr.right
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
⊢ ∀ (s : Set α),
    Set.encard s + 1 = ↑(Nat.succ n) → a ∈ s → IsPreprimitive ↥(fixingSubgroup M s) ↥(SubMulAction.ofFixingSubgroup M s)
Tactic:
intro s hs has
State after:
case mpr.right
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
s : Set α
hs : Set.encard s + 1 = ↑(Nat.succ n)
has : a ∈ s
⊢ IsPreprimitive ↥(fixingSubgroup M s) ↥(SubMulAction.ofFixingSubgroup M s)

State before:
case mpr.right
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
s : Set α
hs : Set.encard s + 1 = ↑(Nat.succ n)
has : a ∈ s
⊢ IsPreprimitive ↥(fixingSubgroup M s) ↥(SubMulAction.ofFixingSubgroup M s)
Tactic:
rw [WithTop.add_one_eq_coe_succ_iff] at hs
State after:
case mpr.right
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
⊢ IsPreprimitive ↥(fixingSubgroup M s) ↥(SubMulAction.ofFixingSubgroup M s)

State before:
case mpr.right
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
⊢ IsPreprimitive ↥(fixingSubgroup M s) ↥(SubMulAction.ofFixingSubgroup M s)
Tactic:
let t : Set (SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
State after:
case mpr.right
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
⊢ IsPreprimitive ↥(fixingSubgroup M s) ↥(SubMulAction.ofFixingSubgroup M s)

State before:
case mpr.right
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
hst : s = insert a (Subtype.val '' t)
⊢ IsPreprimitive ↥(fixingSubgroup M s) ↥(SubMulAction.ofFixingSubgroup M s)
Tactic:
rw [hst]
State after:
case mpr.right
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
hst : s = insert a (Subtype.val '' t)
⊢ IsPreprimitive ↥(fixingSubgroup M (insert a (Subtype.val '' t)))
    ↥(SubMulAction.ofFixingSubgroup M (insert a (Subtype.val '' t)))

State before:
case mpr.right
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
hst : s = insert a (Subtype.val '' t)
⊢ IsPreprimitive ↥(fixingSubgroup M (insert a (Subtype.val '' t)))
    ↥(SubMulAction.ofFixingSubgroup M (insert a (Subtype.val '' t)))
Tactic:
rw [isPreprimitive_of_bijective_map_iff
    (SubMulAction.scalarMap_ofFixingSubgroupOfStabilizer_bijective M a t).surjective
    (SubMulAction.equivariantMap_ofFixingSubgroup_to_ofStabilizer_bijective M a t)]
State after:
case mpr.right
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
hst : s = insert a (Subtype.val '' t)
⊢ IsPreprimitive ↥(fixingSubgroup (↥(stabilizer M a)) t) ↥(SubMulAction.ofFixingSubgroup (↥(stabilizer M a)) t)

State before:
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
this :
  ∀ (s : Set α),
    Set.encard s + 1 = ↑(Nat.succ n) → a ∈ s → IsPreprimitive ↥(fixingSubgroup M s) ↥(SubMulAction.ofFixingSubgroup M s)
⊢ ∀ (s : Set α),
    Set.encard s + 1 = ↑(Nat.succ n) → IsPreprimitive ↥(fixingSubgroup M s) ↥(SubMulAction.ofFixingSubgroup M s)
Tactic:
intro s hs
State after:
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
this :
  ∀ (s : Set α),
    Set.encard s + 1 = ↑(Nat.succ n) → a ∈ s → IsPreprimitive ↥(fixingSubgroup M s) ↥(SubMulAction.ofFixingSubgroup M s)
s : Set α
hs : Set.encard s + 1 = ↑(Nat.succ n)
⊢ IsPreprimitive ↥(fixingSubgroup M s) ↥(SubMulAction.ofFixingSubgroup M s)

State before:
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
this :
  ∀ (s : Set α),
    Set.encard s + 1 = ↑(Nat.succ n) → a ∈ s → IsPreprimitive ↥(fixingSubgroup M s) ↥(SubMulAction.ofFixingSubgroup M s)
s : Set α
hs : Set.encard s + 1 = ↑(Nat.succ n)
⊢ IsPreprimitive ↥(fixingSubgroup M s) ↥(SubMulAction.ofFixingSubgroup M s)
Tactic:
have : ∃ b : α, b ∈ s := by
  rw [← Set.nonempty_def, Set.nonempty_iff_ne_empty]
  intro h
  apply not_lt.mpr hn
  rw [h, Set.encard_empty, zero_add, ← Nat.cast_one, Nat.cast_inj, Nat.succ_inj'] at hs
  simp only [← hs, zero_lt_one]
State after:
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
this✝ :
  ∀ (s : Set α),
    Set.encard s + 1 = ↑(Nat.succ n) → a ∈ s → IsPreprimitive ↥(fixingSubgroup M s) ↥(SubMulAction.ofFixingSubgroup M s)
s : Set α
hs : Set.encard s + 1 = ↑(Nat.succ n)
this : ∃ b, b ∈ s
⊢ IsPreprimitive ↥(fixingSubgroup M s) ↥(SubMulAction.ofFixingSubgroup M s)

State before:
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
this✝ :
  ∀ (s : Set α),
    Set.encard s + 1 = ↑(Nat.succ n) → a ∈ s → IsPreprimitive ↥(fixingSubgroup M s) ↥(SubMulAction.ofFixingSubgroup M s)
s : Set α
hs : Set.encard s + 1 = ↑(Nat.succ n)
this : ∃ b, b ∈ s
⊢ IsPreprimitive ↥(fixingSubgroup M s) ↥(SubMulAction.ofFixingSubgroup M s)
Tactic:
obtain ⟨b, hb⟩ := this
State after:
case intro
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
this :
  ∀ (s : Set α),
    Set.encard s + 1 = ↑(Nat.succ n) → a ∈ s → IsPreprimitive ↥(fixingSubgroup M s) ↥(SubMulAction.ofFixingSubgroup M s)
s : Set α
hs : Set.encard s + 1 = ↑(Nat.succ n)
b : α
hb : b ∈ s
⊢ IsPreprimitive ↥(fixingSubgroup M s) ↥(SubMulAction.ofFixingSubgroup M s)

State before:
case intro
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
this :
  ∀ (s : Set α),
    Set.encard s + 1 = ↑(Nat.succ n) → a ∈ s → IsPreprimitive ↥(fixingSubgroup M s) ↥(SubMulAction.ofFixingSubgroup M s)
s : Set α
hs : Set.encard s + 1 = ↑(Nat.succ n)
b : α
hb : b ∈ s
⊢ IsPreprimitive ↥(fixingSubgroup M s) ↥(SubMulAction.ofFixingSubgroup M s)
Tactic:
obtain ⟨g, hg : g • b = a⟩ := h_eq b a
State after:
case intro.intro
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
this :
  ∀ (s : Set α),
    Set.encard s + 1 = ↑(Nat.succ n) → a ∈ s → IsPreprimitive ↥(fixingSubgroup M s) ↥(SubMulAction.ofFixingSubgroup M s)
s : Set α
hs : Set.encard s + 1 = ↑(Nat.succ n)
b : α
hb : b ∈ s
g : M
hg : g • b = a
⊢ IsPreprimitive ↥(fixingSubgroup M s) ↥(SubMulAction.ofFixingSubgroup M s)

State before:
case intro.intro
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
this :
  ∀ (s : Set α),
    Set.encard s + 1 = ↑(Nat.succ n) → a ∈ s → IsPreprimitive ↥(fixingSubgroup M s) ↥(SubMulAction.ofFixingSubgroup M s)
s : Set α
hs : Set.encard s + 1 = ↑(Nat.succ n)
b : α
hb : b ∈ s
g : M
hg : g • b = a
⊢ IsPreprimitive ↥(fixingSubgroup M s) ↥(SubMulAction.ofFixingSubgroup M s)
Tactic:
apply isPreprimitive_of_surjective_map
  (SubMulAction.conjMap_ofFixingSubgroup_bijective M (inv_smul_smul g s)).surjective
State after:
case intro.intro
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
this :
  ∀ (s : Set α),
    Set.encard s + 1 = ↑(Nat.succ n) → a ∈ s → IsPreprimitive ↥(fixingSubgroup M s) ↥(SubMulAction.ofFixingSubgroup M s)
s : Set α
hs : Set.encard s + 1 = ↑(Nat.succ n)
b : α
hb : b ∈ s
g : M
hg : g • b = a
⊢ IsPreprimitive ↥(fixingSubgroup M (g • s)) ↥(SubMulAction.ofFixingSubgroup M (g • s))

State before:
case intro.intro
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
this :
  ∀ (s : Set α),
    Set.encard s + 1 = ↑(Nat.succ n) → a ∈ s → IsPreprimitive ↥(fixingSubgroup M s) ↥(SubMulAction.ofFixingSubgroup M s)
s : Set α
hs : Set.encard s + 1 = ↑(Nat.succ n)
b : α
hb : b ∈ s
g : M
hg : g • b = a
⊢ IsPreprimitive ↥(fixingSubgroup M (g • s)) ↥(SubMulAction.ofFixingSubgroup M (g • s))
Tactic:
refine' this (g • s) _ ⟨b, hb, hg⟩
State after:
case intro.intro
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
this :
  ∀ (s : Set α),
    Set.encard s + 1 = ↑(Nat.succ n) → a ∈ s → IsPreprimitive ↥(fixingSubgroup M s) ↥(SubMulAction.ofFixingSubgroup M s)
s : Set α
hs : Set.encard s + 1 = ↑(Nat.succ n)
b : α
hb : b ∈ s
g : M
hg : g • b = a
⊢ Set.encard (g • s) + 1 = ↑(Nat.succ n)

State before:
case intro.intro
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
this :
  ∀ (s : Set α),
    Set.encard s + 1 = ↑(Nat.succ n) → a ∈ s → IsPreprimitive ↥(fixingSubgroup M s) ↥(SubMulAction.ofFixingSubgroup M s)
s : Set α
hs : Set.encard s + 1 = ↑(Nat.succ n)
b : α
hb : b ∈ s
g : M
hg : g • b = a
⊢ Set.encard (g • s) + 1 = ↑(Nat.succ n)
Tactic:
rw [smul_set_encard_eq, hs]
State after:
no goals

State before:
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
this :
  ∀ (s : Set α),
    Set.encard s + 1 = ↑(Nat.succ n) → a ∈ s → IsPreprimitive ↥(fixingSubgroup M s) ↥(SubMulAction.ofFixingSubgroup M s)
s : Set α
hs : Set.encard s + 1 = ↑(Nat.succ n)
⊢ ∃ b, b ∈ s
Tactic:
rw [← Set.nonempty_def, Set.nonempty_iff_ne_empty]
State after:
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
this :
  ∀ (s : Set α),
    Set.encard s + 1 = ↑(Nat.succ n) → a ∈ s → IsPreprimitive ↥(fixingSubgroup M s) ↥(SubMulAction.ofFixingSubgroup M s)
s : Set α
hs : Set.encard s + 1 = ↑(Nat.succ n)
⊢ s ≠ ∅

State before:
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
this :
  ∀ (s : Set α),
    Set.encard s + 1 = ↑(Nat.succ n) → a ∈ s → IsPreprimitive ↥(fixingSubgroup M s) ↥(SubMulAction.ofFixingSubgroup M s)
s : Set α
hs : Set.encard s + 1 = ↑(Nat.succ n)
⊢ s ≠ ∅
Tactic:
intro h
State after:
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h✝ : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
this :
  ∀ (s : Set α),
    Set.encard s + 1 = ↑(Nat.succ n) → a ∈ s → IsPreprimitive ↥(fixingSubgroup M s) ↥(SubMulAction.ofFixingSubgroup M s)
s : Set α
hs : Set.encard s + 1 = ↑(Nat.succ n)
h : s = ∅
⊢ False

State before:
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h✝ : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
this :
  ∀ (s : Set α),
    Set.encard s + 1 = ↑(Nat.succ n) → a ∈ s → IsPreprimitive ↥(fixingSubgroup M s) ↥(SubMulAction.ofFixingSubgroup M s)
s : Set α
hs : Set.encard s + 1 = ↑(Nat.succ n)
h : s = ∅
⊢ False
Tactic:
apply not_lt.mpr hn
State after:
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h✝ : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
this :
  ∀ (s : Set α),
    Set.encard s + 1 = ↑(Nat.succ n) → a ∈ s → IsPreprimitive ↥(fixingSubgroup M s) ↥(SubMulAction.ofFixingSubgroup M s)
s : Set α
hs : Set.encard s + 1 = ↑(Nat.succ n)
h : s = ∅
⊢ n < 1

State before:
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h✝ : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
this :
  ∀ (s : Set α),
    Set.encard s + 1 = ↑(Nat.succ n) → a ∈ s → IsPreprimitive ↥(fixingSubgroup M s) ↥(SubMulAction.ofFixingSubgroup M s)
s : Set α
hs : Set.encard s + 1 = ↑(Nat.succ n)
h : s = ∅
⊢ n < 1
Tactic:
rw [h, Set.encard_empty, zero_add, ← Nat.cast_one, Nat.cast_inj, Nat.succ_inj'] at hs
State after:
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h✝ : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
this :
  ∀ (s : Set α),
    Set.encard s + 1 = ↑(Nat.succ n) → a ∈ s → IsPreprimitive ↥(fixingSubgroup M s) ↥(SubMulAction.ofFixingSubgroup M s)
s : Set α
hs : 0 = n
h : s = ∅
⊢ n < 1

State before:
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h✝ : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
this :
  ∀ (s : Set α),
    Set.encard s + 1 = ↑(Nat.succ n) → a ∈ s → IsPreprimitive ↥(fixingSubgroup M s) ↥(SubMulAction.ofFixingSubgroup M s)
s : Set α
hs : 0 = n
h : s = ∅
⊢ n < 1
Tactic:
simp only [← hs, zero_lt_one]
State after:
no goals

State before:
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
⊢ s = insert a (Subtype.val '' t)
Tactic:
ext x
State after:
case h
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
x : α
⊢ x ∈ s ↔ x ∈ insert a (Subtype.val '' t)

State before:
case h
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
x : α
⊢ x ∈ s ↔ x ∈ insert a (Subtype.val '' t)
Tactic:
constructor
State after:
case h.mp
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
x : α
⊢ x ∈ s → x ∈ insert a (Subtype.val '' t)

case h.mpr
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
x : α
⊢ x ∈ insert a (Subtype.val '' t) → x ∈ s

State before:
case h.mp
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
x : α
⊢ x ∈ s → x ∈ insert a (Subtype.val '' t)
Tactic:
intro hxs
State after:
case h.mp
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
x : α
hxs : x ∈ s
⊢ x ∈ insert a (Subtype.val '' t)

State before:
case h.mp
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
x : α
hxs : x ∈ s
⊢ x ∈ insert a (Subtype.val '' t)
Tactic:
by_cases hxa : x = a
State after:
case pos
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
x : α
hxs : x ∈ s
hxa : x = a
⊢ x ∈ insert a (Subtype.val '' t)

case neg
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
x : α
hxs : x ∈ s
hxa : ¬x = a
⊢ x ∈ insert a (Subtype.val '' t)

State before:
case pos
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
x : α
hxs : x ∈ s
hxa : x = a
⊢ x ∈ insert a (Subtype.val '' t)

case neg
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
x : α
hxs : x ∈ s
hxa : ¬x = a
⊢ x ∈ insert a (Subtype.val '' t)
Tactic:
rw [hxa]
State after:
case pos
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
x : α
hxs : x ∈ s
hxa : x = a
⊢ a ∈ insert a (Subtype.val '' t)

case neg
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
x : α
hxs : x ∈ s
hxa : ¬x = a
⊢ x ∈ insert a (Subtype.val '' t)

State before:
case pos
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
x : α
hxs : x ∈ s
hxa : x = a
⊢ a ∈ insert a (Subtype.val '' t)

case neg
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
x : α
hxs : x ∈ s
hxa : ¬x = a
⊢ x ∈ insert a (Subtype.val '' t)
Tactic:
apply Set.mem_insert
State after:
case neg
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
x : α
hxs : x ∈ s
hxa : ¬x = a
⊢ x ∈ insert a (Subtype.val '' t)

State before:
case neg
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
x : α
hxs : x ∈ s
hxa : ¬x = a
⊢ x ∈ insert a (Subtype.val '' t)
Tactic:
apply Set.mem_insert_of_mem
State after:
case neg.a
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
x : α
hxs : x ∈ s
hxa : ¬x = a
⊢ x ∈ Subtype.val '' t

State before:
case neg.a
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
x : α
hxs : x ∈ s
hxa : ¬x = a
⊢ x ∈ Subtype.val '' t
Tactic:
use ⟨x, ?_⟩
State after:
case h
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
x : α
hxs : x ∈ s
hxa : ¬x = a
⊢ { val := x, property := ?w } ∈ t ∧ ↑{ val := x, property := ?w } = x

case w
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
x : α
hxs : x ∈ s
hxa : ¬x = a
⊢ x ∈ SubMulAction.ofStabilizer M a

State before:
case h
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
x : α
hxs : x ∈ s
hxa : ¬x = a
⊢ { val := x, property := ?w } ∈ t ∧ ↑{ val := x, property := ?w } = x

case w
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
x : α
hxs : x ∈ s
hxa : ¬x = a
⊢ x ∈ SubMulAction.ofStabilizer M a
Tactic:
refine' And.intro _ rfl
State after:
case h
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
x : α
hxs : x ∈ s
hxa : ¬x = a
⊢ { val := x, property := ?w } ∈ t

case w
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
x : α
hxs : x ∈ s
hxa : ¬x = a
⊢ x ∈ SubMulAction.ofStabilizer M a

State before:
case w
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
x : α
hxs : x ∈ s
hxa : ¬x = a
⊢ x ∈ SubMulAction.ofStabilizer M a
Tactic:
exact hxa
State after:
no goals

State before:
case h
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
x : α
hxs : x ∈ s
hxa : ¬x = a
⊢ { val := x, property := ?w } ∈ t
Tactic:
simp only [t, Set.mem_preimage]
State after:
case h
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
x : α
hxs : x ∈ s
hxa : ¬x = a
⊢ x ∈ s

State before:
case h
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
x : α
hxs : x ∈ s
hxa : ¬x = a
⊢ x ∈ s
Tactic:
exact hxs
State after:
no goals

State before:
case h.mpr
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
x : α
⊢ x ∈ insert a (Subtype.val '' t) → x ∈ s
Tactic:
intro hxat
State after:
case h.mpr
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
x : α
hxat : x ∈ insert a (Subtype.val '' t)
⊢ x ∈ s

State before:
case h.mpr
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
x : α
hxat : x ∈ insert a (Subtype.val '' t)
⊢ x ∈ s
Tactic:
cases' Set.mem_insert_iff.mp hxat with hxa hxt
State after:
case h.mpr.inl
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
x : α
hxat : x ∈ insert a (Subtype.val '' t)
hxa : x = a
⊢ x ∈ s

case h.mpr.inr
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
x : α
hxat : x ∈ insert a (Subtype.val '' t)
hxt : x ∈ Subtype.val '' t
⊢ x ∈ s

State before:
case h.mpr.inl
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
x : α
hxat : x ∈ insert a (Subtype.val '' t)
hxa : x = a
⊢ x ∈ s

case h.mpr.inr
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
x : α
hxat : x ∈ insert a (Subtype.val '' t)
hxt : x ∈ Subtype.val '' t
⊢ x ∈ s
Tactic:
rw [hxa]
State after:
case h.mpr.inl
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
x : α
hxat : x ∈ insert a (Subtype.val '' t)
hxa : x = a
⊢ a ∈ s

case h.mpr.inr
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
x : α
hxat : x ∈ insert a (Subtype.val '' t)
hxt : x ∈ Subtype.val '' t
⊢ x ∈ s

State before:
case h.mpr.inl
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
x : α
hxat : x ∈ insert a (Subtype.val '' t)
hxa : x = a
⊢ a ∈ s

case h.mpr.inr
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
x : α
hxat : x ∈ insert a (Subtype.val '' t)
hxt : x ∈ Subtype.val '' t
⊢ x ∈ s
Tactic:
exact has
State after:
case h.mpr.inr
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
x : α
hxat : x ∈ insert a (Subtype.val '' t)
hxt : x ∈ Subtype.val '' t
⊢ x ∈ s

State before:
case h.mpr.inr
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
x : α
hxat : x ∈ insert a (Subtype.val '' t)
hxt : x ∈ Subtype.val '' t
⊢ x ∈ s
Tactic:
obtain ⟨y, hy, rfl⟩ := hxt
State after:
case h.mpr.inr.intro.intro
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
y : ↥(SubMulAction.ofStabilizer M a)
hy : y ∈ t
hxat : ↑y ∈ insert a (Subtype.val '' t)
⊢ ↑y ∈ s

State before:
case h.mpr.inr.intro.intro
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
y : ↥(SubMulAction.ofStabilizer M a)
hy : y ∈ t
hxat : ↑y ∈ insert a (Subtype.val '' t)
⊢ ↑y ∈ s
Tactic:
simpa only using hy
State after:
no goals

State before:
case mpr.right
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
hst : s = insert a (Subtype.val '' t)
⊢ IsPreprimitive ↥(fixingSubgroup (↥(stabilizer M a)) t) ↥(SubMulAction.ofFixingSubgroup (↥(stabilizer M a)) t)
Tactic:
apply hn_0.right t
State after:
case mpr.right
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
hst : s = insert a (Subtype.val '' t)
⊢ Set.encard t + 1 = ↑n

State before:
case mpr.right
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
hst : s = insert a (Subtype.val '' t)
⊢ Set.encard t + 1 = ↑n
Tactic:
rw [← hs, hst, Set.encard_insert_of_not_mem, Subtype.coe_injective.encard_image]
State after:
case mpr.right
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
hst : s = insert a (Subtype.val '' t)
⊢ a ∉ Subtype.val '' t

State before:
case mpr.right
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
hst : s = insert a (Subtype.val '' t)
⊢ a ∉ Subtype.val '' t
Tactic:
rintro ⟨x, hx⟩
State after:
case mpr.right.intro
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
hst : s = insert a (Subtype.val '' t)
x : ↥(SubMulAction.ofStabilizer M a)
hx : x ∈ t ∧ ↑x = a
⊢ False

State before:
case mpr.right.intro
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
hst : s = insert a (Subtype.val '' t)
x : ↥(SubMulAction.ofStabilizer M a)
hx : x ∈ t ∧ ↑x = a
⊢ False
Tactic:
apply x.prop
State after:
case mpr.right.intro
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
hst : s = insert a (Subtype.val '' t)
x : ↥(SubMulAction.ofStabilizer M a)
hx : x ∈ t ∧ ↑x = a
⊢ ↑x ∈ {a}

State before:
case mpr.right.intro
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
hst : s = insert a (Subtype.val '' t)
x : ↥(SubMulAction.ofStabilizer M a)
hx : x ∈ t ∧ ↑x = a
⊢ ↑x ∈ {a}
Tactic:
rw [hx.right]
State after:
case mpr.right.intro
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
hst : s = insert a (Subtype.val '' t)
x : ↥(SubMulAction.ofStabilizer M a)
hx : x ∈ t ∧ ↑x = a
⊢ a ∈ {a}

State before:
case mpr.right.intro
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : 1 ≤ n
h : IsPretransitive M α
a : α
h_eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
hn_0 : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
hst : s = insert a (Subtype.val '' t)
x : ↥(SubMulAction.ofStabilizer M a)
hx : x ∈ t ∧ ↑x = a
⊢ a ∈ {a}
Tactic:
simp only [Set.mem_singleton]
State after:
no goals