internlm/Lean-Github huggingface dataset:
Theorem: MulAction.stabilizer.isMultiplyPreprimitive
Proof 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
Proof 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)
Theorem: MulAction.stabilizer.isMultiplyPreprimitive
Proof 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
Proof 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)
Theorem: MulAction.stabilizer.isMultiplyPreprimitive
Proof 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
Proof 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)
Theorem: MulAction.stabilizer.isMultiplyPreprimitive
Proof 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]
Proof 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)))
Theorem: MulAction.stabilizer.isMultiplyPreprimitive
Proof 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)]
Proof 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)
Theorem: MulAction.stabilizer.isMultiplyPreprimitive
Proof 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
Proof 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)
Theorem: MulAction.stabilizer.isMultiplyPreprimitive
Proof 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]
Proof 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)
Theorem: MulAction.stabilizer.isMultiplyPreprimitive
Proof 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
Proof 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)
Theorem: MulAction.stabilizer.isMultiplyPreprimitive
Proof 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
Proof 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)
Theorem: MulAction.stabilizer.isMultiplyPreprimitive
Proof 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
Proof 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))
Theorem: MulAction.stabilizer.isMultiplyPreprimitive
Proof 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⟩
Proof 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)
Theorem: MulAction.stabilizer.isMultiplyPreprimitive
Proof 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]
Proof state after:
no goals
Theorem: MulAction.stabilizer.isMultiplyPreprimitive
Proof 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]
Proof 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 ≠ ∅
Theorem: MulAction.stabilizer.isMultiplyPreprimitive
Proof 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
Proof 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
Theorem: MulAction.stabilizer.isMultiplyPreprimitive
Proof 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
Proof 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
Theorem: MulAction.stabilizer.isMultiplyPreprimitive
Proof 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
Proof 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
Theorem: MulAction.stabilizer.isMultiplyPreprimitive
Proof 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]
Proof state after:
no goals
Theorem: MulAction.stabilizer.isMultiplyPreprimitive
Proof 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
Proof 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)
Theorem: MulAction.stabilizer.isMultiplyPreprimitive
Proof 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
Proof 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
Theorem: MulAction.stabilizer.isMultiplyPreprimitive
Proof 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
Proof 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)
Theorem: MulAction.stabilizer.isMultiplyPreprimitive
Proof 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
Proof 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)