internlm/Lean-Github huggingface dataset:
Theorem: MulAction.isPreprimitive_iff_is_one_preprimitive
Proof state before:
case mpr.intro
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
left✝ : IsMultiplyPretransitive M α 1
h1' : ∀ (s : Set α), Set.encard s + 1 = ↑1 → IsPreprimitive ↥(fixingSubgroup M s) ↥(SubMulAction.ofFixingSubgroup M s)
⊢ IsPreprimitive M α
Tactic:
apply isPreprimitive_of_surjective_map
  (Function.Bijective.surjective
      (SubMulAction.ofFixingSubgroupEmpty_equivariantMap_bijective M α))
Proof state after:
case mpr.intro
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
left✝ : IsMultiplyPretransitive M α 1
h1' : ∀ (s : Set α), Set.encard s + 1 = ↑1 → IsPreprimitive ↥(fixingSubgroup M s) ↥(SubMulAction.ofFixingSubgroup M s)
⊢ IsPreprimitive ↥(fixingSubgroup M ∅) ↥(SubMulAction.ofFixingSubgroup M ∅)
Theorem: MulAction.isPreprimitive_iff_is_one_preprimitive
Proof state before:
case mpr.intro
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
left✝ : IsMultiplyPretransitive M α 1
h1' : ∀ (s : Set α), Set.encard s + 1 = ↑1 → IsPreprimitive ↥(fixingSubgroup M s) ↥(SubMulAction.ofFixingSubgroup M s)
⊢ IsPreprimitive ↥(fixingSubgroup M ∅) ↥(SubMulAction.ofFixingSubgroup M ∅)
Tactic:
apply h1'
Proof state after:
case mpr.intro.x
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
left✝ : IsMultiplyPretransitive M α 1
h1' : ∀ (s : Set α), Set.encard s + 1 = ↑1 → IsPreprimitive ↥(fixingSubgroup M s) ↥(SubMulAction.ofFixingSubgroup M s)
⊢ Set.encard ∅ + 1 = ↑1
Theorem: MulAction.isPreprimitive_iff_is_one_preprimitive
Proof state before:
case mpr.intro.x
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
left✝ : IsMultiplyPretransitive M α 1
h1' : ∀ (s : Set α), Set.encard s + 1 = ↑1 → IsPreprimitive ↥(fixingSubgroup M s) ↥(SubMulAction.ofFixingSubgroup M s)
⊢ Set.encard ∅ + 1 = ↑1
Tactic:
simp only [Set.encard_empty, zero_add, Nat.cast_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 : α
⊢ IsMultiplyPreprimitive M α (Nat.succ n) ↔
    IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
Tactic:
let h_eq := h.exists_smul_eq
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
⊢ IsMultiplyPreprimitive M α (Nat.succ n) ↔
    IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
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
⊢ IsMultiplyPreprimitive M α (Nat.succ n) ↔
    IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
Tactic:
constructor
Proof 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)
Theorem: MulAction.stabilizer.isMultiplyPreprimitive
Proof 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
Proof 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
Theorem: MulAction.stabilizer.isMultiplyPreprimitive
Proof 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
Proof 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
Theorem: MulAction.stabilizer.isMultiplyPreprimitive
Proof 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
Proof 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)
Theorem: MulAction.stabilizer.isMultiplyPreprimitive
Proof 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
Proof 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)
Theorem: MulAction.stabilizer.isMultiplyPreprimitive
Proof 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
Proof 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)
Theorem: MulAction.stabilizer.isMultiplyPreprimitive
Proof 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
Proof 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)))
Theorem: MulAction.stabilizer.isMultiplyPreprimitive
Proof 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
Proof 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)
Theorem: MulAction.stabilizer.isMultiplyPreprimitive
Proof 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]
Proof 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
Theorem: MulAction.stabilizer.isMultiplyPreprimitive
Proof 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
Proof 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
Theorem: MulAction.stabilizer.isMultiplyPreprimitive
Proof 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]
Proof 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
Theorem: MulAction.stabilizer.isMultiplyPreprimitive
Proof 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
Proof state after:
no goals
Theorem: MulAction.stabilizer.isMultiplyPreprimitive
Proof 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
Proof 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
Theorem: MulAction.stabilizer.isMultiplyPreprimitive
Proof 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
Proof 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
Theorem: MulAction.stabilizer.isMultiplyPreprimitive
Proof 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
Proof 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
Theorem: MulAction.stabilizer.isMultiplyPreprimitive
Proof 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
Proof 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}
Theorem: MulAction.stabilizer.isMultiplyPreprimitive
Proof 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]
Proof state after:
no goals
Theorem: MulAction.stabilizer.isMultiplyPreprimitive
Proof 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
Proof 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)
Theorem: MulAction.stabilizer.isMultiplyPreprimitive
Proof 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
Proof 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)
Theorem: MulAction.stabilizer.isMultiplyPreprimitive
Proof 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]
Proof 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
⊢ α
Theorem: MulAction.stabilizer.isMultiplyPreprimitive
Proof 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
Proof state after:
no goals
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) → 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]
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 α),
    Set.encard s + 1 = ↑(Nat.succ n) → a ∈ s → IsPreprimitive ↥(fixingSubgroup M s) ↥(SubMulAction.ofFixingSubgroup M s)