internlm/Lean-Github huggingface dataset:
Theorem: MulAction.remaining_primitivity
Proof state before:
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
hs : n = m + Set.ncard s
h : IsMultiplyPreprimitive M α n
⊢ IsMultiplyPreprimitive (↥(fixingSubgroup M s)) (↥(SubMulAction.ofFixingSubgroup M s)) m
Tactic:
constructor
Proof state after:
case left
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
hs : n = m + Set.ncard s
h : IsMultiplyPreprimitive M α n
⊢ IsMultiplyPretransitive (↥(fixingSubgroup M s)) (↥(SubMulAction.ofFixingSubgroup M s)) m

case right
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
hs : n = m + Set.ncard s
h : IsMultiplyPreprimitive M α n
⊢ ∀ (s_1 : Set ↥(SubMulAction.ofFixingSubgroup M s)),
    Set.encard s_1 + 1 = ↑m →
      IsPreprimitive ↥(fixingSubgroup (↥(fixingSubgroup M s)) s_1)
        ↥(SubMulAction.ofFixingSubgroup (↥(fixingSubgroup M s)) s_1)
Theorem: MulAction.remaining_primitivity
Proof state before:
case left
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
hs : n = m + Set.ncard s
h : IsMultiplyPreprimitive M α n
⊢ IsMultiplyPretransitive (↥(fixingSubgroup M s)) (↥(SubMulAction.ofFixingSubgroup M s)) m
Tactic:
apply remaining_transitivity M α s h.left hs
Proof state after:
no goals
Theorem: MulAction.remaining_primitivity
Proof state before:
case right
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
hs : n = m + Set.ncard s
h : IsMultiplyPreprimitive M α n
⊢ ∀ (s_1 : Set ↥(SubMulAction.ofFixingSubgroup M s)),
    Set.encard s_1 + 1 = ↑m →
      IsPreprimitive ↥(fixingSubgroup (↥(fixingSubgroup M s)) s_1)
        ↥(SubMulAction.ofFixingSubgroup (↥(fixingSubgroup M s)) s_1)
Tactic:
intro t ht
Proof state after:
case right
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
hs : n = m + Set.ncard s
h : IsMultiplyPreprimitive M α n
t : Set ↥(SubMulAction.ofFixingSubgroup M s)
ht : Set.encard t + 1 = ↑m
⊢ IsPreprimitive ↥(fixingSubgroup (↥(fixingSubgroup M s)) t) ↥(SubMulAction.ofFixingSubgroup (↥(fixingSubgroup M s)) t)
Theorem: MulAction.remaining_primitivity
Proof state before:
case right
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
hs : n = m + Set.ncard s
h : IsMultiplyPreprimitive M α n
t : Set ↥(SubMulAction.ofFixingSubgroup M s)
ht : Set.encard t + 1 = ↑m
⊢ IsPreprimitive ↥(fixingSubgroup (↥(fixingSubgroup M s)) t) ↥(SubMulAction.ofFixingSubgroup (↥(fixingSubgroup M s)) t)
Tactic:
let t' : Set α := Subtype.val '' t
Proof state after:
case right
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
hs : n = m + Set.ncard s
h : IsMultiplyPreprimitive M α n
t : Set ↥(SubMulAction.ofFixingSubgroup M s)
ht : Set.encard t + 1 = ↑m
t' : Set α := Subtype.val '' t
⊢ IsPreprimitive ↥(fixingSubgroup (↥(fixingSubgroup M s)) t) ↥(SubMulAction.ofFixingSubgroup (↥(fixingSubgroup M s)) t)
Theorem: MulAction.remaining_primitivity
Proof state before:
case right
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
hs : n = m + Set.ncard s
h : IsMultiplyPreprimitive M α n
t : Set ↥(SubMulAction.ofFixingSubgroup M s)
ht : Set.encard t + 1 = ↑m
t' : Set α := Subtype.val '' t
⊢ IsPreprimitive ↥(fixingSubgroup (↥(fixingSubgroup M s)) t) ↥(SubMulAction.ofFixingSubgroup (↥(fixingSubgroup M s)) t)
Tactic:
have htt' : t = Subtype.val ⁻¹' t' := by
  apply symm
  apply Set.preimage_image_eq
  exact Subtype.coe_injective
Proof state after:
case right
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
hs : n = m + Set.ncard s
h : IsMultiplyPreprimitive M α n
t : Set ↥(SubMulAction.ofFixingSubgroup M s)
ht : Set.encard t + 1 = ↑m
t' : Set α := Subtype.val '' t
htt' : t = Subtype.val ⁻¹' t'
⊢ IsPreprimitive ↥(fixingSubgroup (↥(fixingSubgroup M s)) t) ↥(SubMulAction.ofFixingSubgroup (↥(fixingSubgroup M s)) t)
Theorem: MulAction.remaining_primitivity
Proof state before:
case right
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
hs : n = m + Set.ncard s
h : IsMultiplyPreprimitive M α n
t : Set ↥(SubMulAction.ofFixingSubgroup M s)
ht : Set.encard t + 1 = ↑m
t' : Set α := Subtype.val '' t
htt' : t = Subtype.val ⁻¹' t'
⊢ IsPreprimitive ↥(fixingSubgroup (↥(fixingSubgroup M s)) t) ↥(SubMulAction.ofFixingSubgroup (↥(fixingSubgroup M s)) t)
Tactic:
rw [htt']
Proof state after:
case right
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
hs : n = m + Set.ncard s
h : IsMultiplyPreprimitive M α n
t : Set ↥(SubMulAction.ofFixingSubgroup M s)
ht : Set.encard t + 1 = ↑m
t' : Set α := Subtype.val '' t
htt' : t = Subtype.val ⁻¹' t'
⊢ IsPreprimitive ↥(fixingSubgroup (↥(fixingSubgroup M s)) (Subtype.val ⁻¹' t'))
    ↥(SubMulAction.ofFixingSubgroup (↥(fixingSubgroup M s)) (Subtype.val ⁻¹' t'))
Theorem: MulAction.remaining_primitivity
Proof state before:
case right
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
hs : n = m + Set.ncard s
h : IsMultiplyPreprimitive M α n
t : Set ↥(SubMulAction.ofFixingSubgroup M s)
ht : Set.encard t + 1 = ↑m
t' : Set α := Subtype.val '' t
htt' : t = Subtype.val ⁻¹' t'
⊢ IsPreprimitive ↥(fixingSubgroup (↥(fixingSubgroup M s)) (Subtype.val ⁻¹' t'))
    ↥(SubMulAction.ofFixingSubgroup (↥(fixingSubgroup M s)) (Subtype.val ⁻¹' t'))
Tactic:
apply isPreprimitive_of_surjective_map
    (SubMulAction.OfFixingSubgroupUnion.map_bijective M s t').surjective
Proof state after:
case right
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
hs : n = m + Set.ncard s
h : IsMultiplyPreprimitive M α n
t : Set ↥(SubMulAction.ofFixingSubgroup M s)
ht : Set.encard t + 1 = ↑m
t' : Set α := Subtype.val '' t
htt' : t = Subtype.val ⁻¹' t'
⊢ IsPreprimitive ↥(fixingSubgroup M (s ∪ t')) ↥(SubMulAction.ofFixingSubgroup M (s ∪ t'))
Theorem: MulAction.remaining_primitivity
Proof state before:
case right
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
hs : n = m + Set.ncard s
h : IsMultiplyPreprimitive M α n
t : Set ↥(SubMulAction.ofFixingSubgroup M s)
ht : Set.encard t + 1 = ↑m
t' : Set α := Subtype.val '' t
htt' : t = Subtype.val ⁻¹' t'
⊢ IsPreprimitive ↥(fixingSubgroup M (s ∪ t')) ↥(SubMulAction.ofFixingSubgroup M (s ∪ t'))
Tactic:
apply h.right
Proof state after:
case right.x
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
hs : n = m + Set.ncard s
h : IsMultiplyPreprimitive M α n
t : Set ↥(SubMulAction.ofFixingSubgroup M s)
ht : Set.encard t + 1 = ↑m
t' : Set α := Subtype.val '' t
htt' : t = Subtype.val ⁻¹' t'
⊢ Set.encard (s ∪ t') + 1 = ↑n
Theorem: MulAction.remaining_primitivity
Proof state before:
case right.x
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
hs : n = m + Set.ncard s
h : IsMultiplyPreprimitive M α n
t : Set ↥(SubMulAction.ofFixingSubgroup M s)
ht : Set.encard t + 1 = ↑m
t' : Set α := Subtype.val '' t
htt' : t = Subtype.val ⁻¹' t'
⊢ Set.encard (s ∪ t') + 1 = ↑n
Tactic:
rw [Set.encard_union_eq _]
Proof state after:
case right.x
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
hs : n = m + Set.ncard s
h : IsMultiplyPreprimitive M α n
t : Set ↥(SubMulAction.ofFixingSubgroup M s)
ht : Set.encard t + 1 = ↑m
t' : Set α := Subtype.val '' t
htt' : t = Subtype.val ⁻¹' t'
⊢ Set.encard s + Set.encard t' + 1 = ↑n

M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
hs : n = m + Set.ncard s
h : IsMultiplyPreprimitive M α n
t : Set ↥(SubMulAction.ofFixingSubgroup M s)
ht : Set.encard t + 1 = ↑m
t' : Set α := Subtype.val '' t
htt' : t = Subtype.val ⁻¹' t'
⊢ Disjoint s t'
Theorem: MulAction.remaining_primitivity
Proof state before:
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
hs : n = m + Set.ncard s
h : IsMultiplyPreprimitive M α n
t : Set ↥(SubMulAction.ofFixingSubgroup M s)
ht : Set.encard t + 1 = ↑m
t' : Set α := Subtype.val '' t
⊢ t = Subtype.val ⁻¹' t'
Tactic:
apply symm
Proof state after:
case a
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
hs : n = m + Set.ncard s
h : IsMultiplyPreprimitive M α n
t : Set ↥(SubMulAction.ofFixingSubgroup M s)
ht : Set.encard t + 1 = ↑m
t' : Set α := Subtype.val '' t
⊢ Subtype.val ⁻¹' t' = t
Theorem: MulAction.remaining_primitivity
Proof state before:
case a
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
hs : n = m + Set.ncard s
h : IsMultiplyPreprimitive M α n
t : Set ↥(SubMulAction.ofFixingSubgroup M s)
ht : Set.encard t + 1 = ↑m
t' : Set α := Subtype.val '' t
⊢ Subtype.val ⁻¹' t' = t
Tactic:
apply Set.preimage_image_eq
Proof state after:
case a.h
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
hs : n = m + Set.ncard s
h : IsMultiplyPreprimitive M α n
t : Set ↥(SubMulAction.ofFixingSubgroup M s)
ht : Set.encard t + 1 = ↑m
t' : Set α := Subtype.val '' t
⊢ Function.Injective Subtype.val
Theorem: MulAction.remaining_primitivity
Proof state before:
case a.h
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
hs : n = m + Set.ncard s
h : IsMultiplyPreprimitive M α n
t : Set ↥(SubMulAction.ofFixingSubgroup M s)
ht : Set.encard t + 1 = ↑m
t' : Set α := Subtype.val '' t
⊢ Function.Injective Subtype.val
Tactic:
exact Subtype.coe_injective
Proof state after:
no goals
Theorem: MulAction.remaining_primitivity
Proof state before:
case right.x
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
hs : n = m + Set.ncard s
h : IsMultiplyPreprimitive M α n
t : Set ↥(SubMulAction.ofFixingSubgroup M s)
ht : Set.encard t + 1 = ↑m
t' : Set α := Subtype.val '' t
htt' : t = Subtype.val ⁻¹' t'
⊢ Set.encard s + Set.encard t' + 1 = ↑n
Tactic:
rw [Subtype.coe_injective.encard_image, add_assoc, ht, hs, add_comm, Nat.cast_add]
Proof state after:
case right.x
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
hs : n = m + Set.ncard s
h : IsMultiplyPreprimitive M α n
t : Set ↥(SubMulAction.ofFixingSubgroup M s)
ht : Set.encard t + 1 = ↑m
t' : Set α := Subtype.val '' t
htt' : t = Subtype.val ⁻¹' t'
⊢ ↑m + Set.encard s = ↑m + ↑(Set.ncard s)
Theorem: MulAction.remaining_primitivity
Proof state before:
case right.x
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
hs : n = m + Set.ncard s
h : IsMultiplyPreprimitive M α n
t : Set ↥(SubMulAction.ofFixingSubgroup M s)
ht : Set.encard t + 1 = ↑m
t' : Set α := Subtype.val '' t
htt' : t = Subtype.val ⁻¹' t'
⊢ ↑m + Set.encard s = ↑m + ↑(Set.ncard s)
Tactic:
rw [Set.Finite.cast_ncard_eq]
Proof state after:
case right.x
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
hs : n = m + Set.ncard s
h : IsMultiplyPreprimitive M α n
t : Set ↥(SubMulAction.ofFixingSubgroup M s)
ht : Set.encard t + 1 = ↑m
t' : Set α := Subtype.val '' t
htt' : t = Subtype.val ⁻¹' t'
⊢ Set.Finite s
Theorem: MulAction.remaining_primitivity
Proof state before:
case right.x
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
hs : n = m + Set.ncard s
h : IsMultiplyPreprimitive M α n
t : Set ↥(SubMulAction.ofFixingSubgroup M s)
ht : Set.encard t + 1 = ↑m
t' : Set α := Subtype.val '' t
htt' : t = Subtype.val ⁻¹' t'
⊢ Set.Finite s
Tactic:
exact Set.toFinite s
Proof state after:
no goals
Theorem: MulAction.remaining_primitivity
Proof state before:
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
hs : n = m + Set.ncard s
h : IsMultiplyPreprimitive M α n
t : Set ↥(SubMulAction.ofFixingSubgroup M s)
ht : Set.encard t + 1 = ↑m
t' : Set α := Subtype.val '' t
htt' : t = Subtype.val ⁻¹' t'
⊢ Disjoint s t'
Tactic:
rw [Set.disjoint_iff]
Proof state after:
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
hs : n = m + Set.ncard s
h : IsMultiplyPreprimitive M α n
t : Set ↥(SubMulAction.ofFixingSubgroup M s)
ht : Set.encard t + 1 = ↑m
t' : Set α := Subtype.val '' t
htt' : t = Subtype.val ⁻¹' t'
⊢ s ∩ t' ⊆ ∅
Theorem: MulAction.remaining_primitivity
Proof state before:
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
hs : n = m + Set.ncard s
h : IsMultiplyPreprimitive M α n
t : Set ↥(SubMulAction.ofFixingSubgroup M s)
ht : Set.encard t + 1 = ↑m
t' : Set α := Subtype.val '' t
htt' : t = Subtype.val ⁻¹' t'
⊢ s ∩ t' ⊆ ∅
Tactic:
intro a
Proof state after:
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
hs : n = m + Set.ncard s
h : IsMultiplyPreprimitive M α n
t : Set ↥(SubMulAction.ofFixingSubgroup M s)
ht : Set.encard t + 1 = ↑m
t' : Set α := Subtype.val '' t
htt' : t = Subtype.val ⁻¹' t'
a : α
⊢ a ∈ s ∩ t' → a ∈ ∅
Theorem: MulAction.remaining_primitivity
Proof state before:
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
hs : n = m + Set.ncard s
h : IsMultiplyPreprimitive M α n
t : Set ↥(SubMulAction.ofFixingSubgroup M s)
ht : Set.encard t + 1 = ↑m
t' : Set α := Subtype.val '' t
htt' : t = Subtype.val ⁻¹' t'
a : α
⊢ a ∈ s ∩ t' → a ∈ ∅
Tactic:
rintro ⟨hbs, ⟨b, _, rfl⟩⟩
Proof state after:
case intro.intro.intro
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
hs : n = m + Set.ncard s
h : IsMultiplyPreprimitive M α n
t : Set ↥(SubMulAction.ofFixingSubgroup M s)
ht : Set.encard t + 1 = ↑m
t' : Set α := Subtype.val '' t
htt' : t = Subtype.val ⁻¹' t'
b : ↥(SubMulAction.ofFixingSubgroup M s)
left✝ : b ∈ t
hbs : ↑b ∈ s
⊢ ↑b ∈ ∅
Theorem: MulAction.remaining_primitivity
Proof state before:
case intro.intro.intro
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
hs : n = m + Set.ncard s
h : IsMultiplyPreprimitive M α n
t : Set ↥(SubMulAction.ofFixingSubgroup M s)
ht : Set.encard t + 1 = ↑m
t' : Set α := Subtype.val '' t
htt' : t = Subtype.val ⁻¹' t'
b : ↥(SubMulAction.ofFixingSubgroup M s)
left✝ : b ∈ t
hbs : ↑b ∈ s
⊢ ↑b ∈ ∅
Tactic:
exfalso
Proof state after:
case intro.intro.intro
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
hs : n = m + Set.ncard s
h : IsMultiplyPreprimitive M α n
t : Set ↥(SubMulAction.ofFixingSubgroup M s)
ht : Set.encard t + 1 = ↑m
t' : Set α := Subtype.val '' t
htt' : t = Subtype.val ⁻¹' t'
b : ↥(SubMulAction.ofFixingSubgroup M s)
left✝ : b ∈ t
hbs : ↑b ∈ s
⊢ False
Theorem: MulAction.remaining_primitivity
Proof state before:
case intro.intro.intro
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
hs : n = m + Set.ncard s
h : IsMultiplyPreprimitive M α n
t : Set ↥(SubMulAction.ofFixingSubgroup M s)
ht : Set.encard t + 1 = ↑m
t' : Set α := Subtype.val '' t
htt' : t = Subtype.val ⁻¹' t'
b : ↥(SubMulAction.ofFixingSubgroup M s)
left✝ : b ∈ t
hbs : ↑b ∈ s
⊢ False
Tactic:
exact b.prop hbs
Proof state after:
no goals
Theorem: MulAction.isMultiplyPreprimitive_of_multiply_pretransitive_succ
Proof state before:
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hα : ↑(Nat.succ n) ≤ PartENat.card α
h : IsMultiplyPretransitive M α (Nat.succ n)
⊢ IsMultiplyPreprimitive M α n
Tactic:
cases' Nat.eq_zero_or_pos n with hn hn
Proof state after:
case inl
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hα : ↑(Nat.succ n) ≤ PartENat.card α
h : IsMultiplyPretransitive M α (Nat.succ n)
hn : n = 0
⊢ IsMultiplyPreprimitive M α n

case inr
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hα : ↑(Nat.succ n) ≤ PartENat.card α
h : IsMultiplyPretransitive M α (Nat.succ n)
hn : n > 0
⊢ IsMultiplyPreprimitive M α n
Theorem: MulAction.isMultiplyPreprimitive_of_multiply_pretransitive_succ
Proof state before:
case inr
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hα : ↑(Nat.succ n) ≤ PartENat.card α
h : IsMultiplyPretransitive M α (Nat.succ n)
hn : n > 0
⊢ IsMultiplyPreprimitive M α n
Tactic:
constructor
Proof state after:
case inr.left
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hα : ↑(Nat.succ n) ≤ PartENat.card α
h : IsMultiplyPretransitive M α (Nat.succ n)
hn : n > 0
⊢ IsMultiplyPretransitive M α n

case inr.right
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hα : ↑(Nat.succ n) ≤ PartENat.card α
h : IsMultiplyPretransitive M α (Nat.succ n)
hn : n > 0
⊢ ∀ (s : Set α), Set.encard s + 1 = ↑n → IsPreprimitive ↥(fixingSubgroup M s) ↥(SubMulAction.ofFixingSubgroup M s)
Theorem: MulAction.isMultiplyPreprimitive_of_multiply_pretransitive_succ
Proof state before:
case inr.left
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hα : ↑(Nat.succ n) ≤ PartENat.card α
h : IsMultiplyPretransitive M α (Nat.succ n)
hn : n > 0
⊢ IsMultiplyPretransitive M α n

case inr.right
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hα : ↑(Nat.succ n) ≤ PartENat.card α
h : IsMultiplyPretransitive M α (Nat.succ n)
hn : n > 0
⊢ ∀ (s : Set α), Set.encard s + 1 = ↑n → IsPreprimitive ↥(fixingSubgroup M s) ↥(SubMulAction.ofFixingSubgroup M s)
Tactic:
apply isMultiplyPretransitive_of_higher M α h
Proof state after:
case inr.left.hmn
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hα : ↑(Nat.succ n) ≤ PartENat.card α
h : IsMultiplyPretransitive M α (Nat.succ n)
hn : n > 0
⊢ n ≤ Nat.succ n

case inr.left.hα
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hα : ↑(Nat.succ n) ≤ PartENat.card α
h : IsMultiplyPretransitive M α (Nat.succ n)
hn : n > 0
⊢ ↑(Nat.succ n) ≤ PartENat.card α

case inr.right
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hα : ↑(Nat.succ n) ≤ PartENat.card α
h : IsMultiplyPretransitive M α (Nat.succ n)
hn : n > 0
⊢ ∀ (s : Set α), Set.encard s + 1 = ↑n → IsPreprimitive ↥(fixingSubgroup M s) ↥(SubMulAction.ofFixingSubgroup M s)
Theorem: MulAction.isMultiplyPreprimitive_of_multiply_pretransitive_succ
Proof state before:
case inr.left.hmn
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hα : ↑(Nat.succ n) ≤ PartENat.card α
h : IsMultiplyPretransitive M α (Nat.succ n)
hn : n > 0
⊢ n ≤ Nat.succ n

case inr.left.hα
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hα : ↑(Nat.succ n) ≤ PartENat.card α
h : IsMultiplyPretransitive M α (Nat.succ n)
hn : n > 0
⊢ ↑(Nat.succ n) ≤ PartENat.card α

case inr.right
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hα : ↑(Nat.succ n) ≤ PartENat.card α
h : IsMultiplyPretransitive M α (Nat.succ n)
hn : n > 0
⊢ ∀ (s : Set α), Set.encard s + 1 = ↑n → IsPreprimitive ↥(fixingSubgroup M s) ↥(SubMulAction.ofFixingSubgroup M s)
Tactic:
exact Nat.le_succ n
Proof state after:
case inr.left.hα
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hα : ↑(Nat.succ n) ≤ PartENat.card α
h : IsMultiplyPretransitive M α (Nat.succ n)
hn : n > 0
⊢ ↑(Nat.succ n) ≤ PartENat.card α

case inr.right
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hα : ↑(Nat.succ n) ≤ PartENat.card α
h : IsMultiplyPretransitive M α (Nat.succ n)
hn : n > 0
⊢ ∀ (s : Set α), Set.encard s + 1 = ↑n → IsPreprimitive ↥(fixingSubgroup M s) ↥(SubMulAction.ofFixingSubgroup M s)
Theorem: MulAction.isMultiplyPreprimitive_of_multiply_pretransitive_succ
Proof state before:
case inr.left.hα
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hα : ↑(Nat.succ n) ≤ PartENat.card α
h : IsMultiplyPretransitive M α (Nat.succ n)
hn : n > 0
⊢ ↑(Nat.succ n) ≤ PartENat.card α

case inr.right
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hα : ↑(Nat.succ n) ≤ PartENat.card α
h : IsMultiplyPretransitive M α (Nat.succ n)
hn : n > 0
⊢ ∀ (s : Set α), Set.encard s + 1 = ↑n → IsPreprimitive ↥(fixingSubgroup M s) ↥(SubMulAction.ofFixingSubgroup M s)
Tactic:
exact hα
Proof state after:
case inr.right
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hα : ↑(Nat.succ n) ≤ PartENat.card α
h : IsMultiplyPretransitive M α (Nat.succ n)
hn : n > 0
⊢ ∀ (s : Set α), Set.encard s + 1 = ↑n → IsPreprimitive ↥(fixingSubgroup M s) ↥(SubMulAction.ofFixingSubgroup M s)
Theorem: MulAction.isMultiplyPreprimitive_of_multiply_pretransitive_succ
Proof state before:
case inr.right
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hα : ↑(Nat.succ n) ≤ PartENat.card α
h : IsMultiplyPretransitive M α (Nat.succ n)
hn : n > 0
⊢ ∀ (s : Set α), Set.encard s + 1 = ↑n → IsPreprimitive ↥(fixingSubgroup M s) ↥(SubMulAction.ofFixingSubgroup M s)
Tactic:
obtain ⟨m, hm⟩ := Nat.exists_eq_add_of_le hn
Proof state after:
case inr.right.intro
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hα : ↑(Nat.succ n) ≤ PartENat.card α
h : IsMultiplyPretransitive M α (Nat.succ n)
hn : n > 0
m : ℕ
hm : n = Nat.succ 0 + m
⊢ ∀ (s : Set α), Set.encard s + 1 = ↑n → IsPreprimitive ↥(fixingSubgroup M s) ↥(SubMulAction.ofFixingSubgroup M s)
Theorem: MulAction.isMultiplyPreprimitive_of_multiply_pretransitive_succ
Proof state before:
case inr.right.intro
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hα : ↑(Nat.succ n) ≤ PartENat.card α
h : IsMultiplyPretransitive M α (Nat.succ n)
hn : n > 0
m : ℕ
hm : n = Nat.succ 0 + m
⊢ ∀ (s : Set α), Set.encard s + 1 = ↑n → IsPreprimitive ↥(fixingSubgroup M s) ↥(SubMulAction.ofFixingSubgroup M s)
Tactic:
rw [hm]
Proof state after:
case inr.right.intro
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hα : ↑(Nat.succ n) ≤ PartENat.card α
h : IsMultiplyPretransitive M α (Nat.succ n)
hn : n > 0
m : ℕ
hm : n = Nat.succ 0 + m
⊢ ∀ (s : Set α),
    Set.encard s + 1 = ↑(Nat.succ 0 + m) → IsPreprimitive ↥(fixingSubgroup M s) ↥(SubMulAction.ofFixingSubgroup M s)
Theorem: MulAction.isMultiplyPreprimitive_of_multiply_pretransitive_succ
Proof state before:
case inr.right.intro
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hα : ↑(Nat.succ n) ≤ PartENat.card α
h : IsMultiplyPretransitive M α (Nat.succ n)
hn : n > 0
m : ℕ
hm : n = Nat.succ 0 + m
⊢ ∀ (s : Set α),
    Set.encard s + 1 = ↑(Nat.succ 0 + m) → IsPreprimitive ↥(fixingSubgroup M s) ↥(SubMulAction.ofFixingSubgroup M s)
Tactic:
intro s hs
Proof state after:
case inr.right.intro
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hα : ↑(Nat.succ n) ≤ PartENat.card α
h : IsMultiplyPretransitive M α (Nat.succ n)
hn : n > 0
m : ℕ
hm : n = Nat.succ 0 + m
s : Set α
hs : Set.encard s + 1 = ↑(Nat.succ 0 + m)
⊢ IsPreprimitive ↥(fixingSubgroup M s) ↥(SubMulAction.ofFixingSubgroup M s)
Theorem: MulAction.isMultiplyPreprimitive_of_multiply_pretransitive_succ
Proof state before:
case inr.right.intro
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hα : ↑(Nat.succ n) ≤ PartENat.card α
h : IsMultiplyPretransitive M α (Nat.succ n)
hn : n > 0
m : ℕ
hm : n = Nat.succ 0 + m
s : Set α
hs : Set.encard s + 1 = ↑(Nat.succ 0 + m)
⊢ IsPreprimitive ↥(fixingSubgroup M s) ↥(SubMulAction.ofFixingSubgroup M s)
Tactic:
apply IsMultiplyPretransitive.isPreprimitive_of_two
Proof state after:
case inr.right.intro.h2
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hα : ↑(Nat.succ n) ≤ PartENat.card α
h : IsMultiplyPretransitive M α (Nat.succ n)
hn : n > 0
m : ℕ
hm : n = Nat.succ 0 + m
s : Set α
hs : Set.encard s + 1 = ↑(Nat.succ 0 + m)
⊢ IsMultiplyPretransitive (↥(fixingSubgroup M s)) (↥(SubMulAction.ofFixingSubgroup M s)) 2