Theorem: MulAction.isMultiplyPreprimitive_of_multiply_pretransitive_succ (Jordan/MultiplePrimitivity.lean)

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
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

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
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)

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
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)

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
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)

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α
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)

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
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)

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]
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)

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
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)

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
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

State before:
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
Tactic:
rw [add_comm _ m, Nat.cast_add, ← Nat.cast_one, WithTop.add_eq_add_iff] at hs
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 = ↑m
⊢ IsMultiplyPretransitive (↥(fixingSubgroup M s)) (↥(SubMulAction.ofFixingSubgroup M s)) 2

State before:
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 = ↑m
⊢ IsMultiplyPretransitive (↥(fixingSubgroup M s)) (↥(SubMulAction.ofFixingSubgroup M s)) 2
Tactic:
have : Finite s := by rw [Set.finite_coe_iff]; exact Set.finite_of_encard_eq_coe hs
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 = ↑m
this : Finite ↑s
⊢ IsMultiplyPretransitive (↥(fixingSubgroup M s)) (↥(SubMulAction.ofFixingSubgroup M s)) 2

State before:
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 = ↑m
this : Finite ↑s
⊢ IsMultiplyPretransitive (↥(fixingSubgroup M s)) (↥(SubMulAction.ofFixingSubgroup M s)) 2
Tactic:
apply remaining_transitivity M α s h
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 = ↑m
this : Finite ↑s
⊢ Nat.succ n = 2 + Set.ncard s

State before:
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 = ↑m
this : Finite ↑s
⊢ Nat.succ n = 2 + Set.ncard s
Tactic:
unfold Set.ncard
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 = ↑m
this : Finite ↑s
⊢ Nat.succ n = 2 + ENat.toNat (Set.encard s)

State before:
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 = ↑m
this : Finite ↑s
⊢ Nat.succ n = 2 + ENat.toNat (Set.encard s)
Tactic:
rw [hs, hm, ENat.toNat_coe, ← Nat.succ_add]
State after:
no goals

State before:
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
Tactic:
rw [hn]
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 α 0

State before:
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 α 0
Tactic:
apply isMultiplyPreprimitive_zero
State after:
no goals

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)
hn : n > 0
m : ℕ
hm : n = Nat.succ 0 + m
s : Set α
hs : Set.encard s = ↑m
⊢ Finite ↑s
Tactic:
rw [Set.finite_coe_iff]
State after:
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 = ↑m
⊢ Set.Finite s

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)
hn : n > 0
m : ℕ
hm : n = Nat.succ 0 + m
s : Set α
hs : Set.encard s = ↑m
⊢ Set.Finite s
Tactic:
exact Set.finite_of_encard_eq_coe hs
State after:
no goals