Theorem: isPreprimitive_of_prime (Jordan/Primitive.lean)

State before:
M : Type u_2
inst✝⁴ : Group M
α : Type u_1
inst✝³ : MulAction M α
N : Type ?u.75053
β : Type ?u.75056
inst✝² : Group N
inst✝¹ : MulAction N β
inst✝ : Fintype α
hGX : IsPretransitive M α
hp : Nat.Prime (Fintype.card α)
⊢ IsPreprimitive M α
Tactic:
apply IsPreprimitive.mk
State after:
case has_trivial_blocks'
M : Type u_2
inst✝⁴ : Group M
α : Type u_1
inst✝³ : MulAction M α
N : Type ?u.75053
β : Type ?u.75056
inst✝² : Group N
inst✝¹ : MulAction N β
inst✝ : Fintype α
hGX : IsPretransitive M α
hp : Nat.Prime (Fintype.card α)
⊢ ∀ {B : Set α}, IsBlock M B → IsTrivialBlock B

State before:
case has_trivial_blocks'
M : Type u_2
inst✝⁴ : Group M
α : Type u_1
inst✝³ : MulAction M α
N : Type ?u.75053
β : Type ?u.75056
inst✝² : Group N
inst✝¹ : MulAction N β
inst✝ : Fintype α
hGX : IsPretransitive M α
hp : Nat.Prime (Fintype.card α)
⊢ ∀ {B : Set α}, IsBlock M B → IsTrivialBlock B
Tactic:
intro B hB
State after:
case has_trivial_blocks'
M : Type u_2
inst✝⁴ : Group M
α : Type u_1
inst✝³ : MulAction M α
N : Type ?u.75053
β : Type ?u.75056
inst✝² : Group N
inst✝¹ : MulAction N β
inst✝ : Fintype α
hGX : IsPretransitive M α
hp : Nat.Prime (Fintype.card α)
B : Set α
hB : IsBlock M B
⊢ IsTrivialBlock B

State before:
case has_trivial_blocks'
M : Type u_2
inst✝⁴ : Group M
α : Type u_1
inst✝³ : MulAction M α
N : Type ?u.75053
β : Type ?u.75056
inst✝² : Group N
inst✝¹ : MulAction N β
inst✝ : Fintype α
hGX : IsPretransitive M α
hp : Nat.Prime (Fintype.card α)
B : Set α
hB : IsBlock M B
⊢ IsTrivialBlock B
Tactic:
cases' Set.subsingleton_or_nontrivial B with hB' hB'
State after:
case has_trivial_blocks'.inl
M : Type u_2
inst✝⁴ : Group M
α : Type u_1
inst✝³ : MulAction M α
N : Type ?u.75053
β : Type ?u.75056
inst✝² : Group N
inst✝¹ : MulAction N β
inst✝ : Fintype α
hGX : IsPretransitive M α
hp : Nat.Prime (Fintype.card α)
B : Set α
hB : IsBlock M B
hB' : Set.Subsingleton B
⊢ IsTrivialBlock B

case has_trivial_blocks'.inr
M : Type u_2
inst✝⁴ : Group M
α : Type u_1
inst✝³ : MulAction M α
N : Type ?u.75053
β : Type ?u.75056
inst✝² : Group N
inst✝¹ : MulAction N β
inst✝ : Fintype α
hGX : IsPretransitive M α
hp : Nat.Prime (Fintype.card α)
B : Set α
hB : IsBlock M B
hB' : Set.Nontrivial B
⊢ IsTrivialBlock B

State before:
case has_trivial_blocks'.inl
M : Type u_2
inst✝⁴ : Group M
α : Type u_1
inst✝³ : MulAction M α
N : Type ?u.75053
β : Type ?u.75056
inst✝² : Group N
inst✝¹ : MulAction N β
inst✝ : Fintype α
hGX : IsPretransitive M α
hp : Nat.Prime (Fintype.card α)
B : Set α
hB : IsBlock M B
hB' : Set.Subsingleton B
⊢ IsTrivialBlock B
Tactic:
apply Or.intro_left
State after:
case has_trivial_blocks'.inl.h
M : Type u_2
inst✝⁴ : Group M
α : Type u_1
inst✝³ : MulAction M α
N : Type ?u.75053
β : Type ?u.75056
inst✝² : Group N
inst✝¹ : MulAction N β
inst✝ : Fintype α
hGX : IsPretransitive M α
hp : Nat.Prime (Fintype.card α)
B : Set α
hB : IsBlock M B
hB' : Set.Subsingleton B
⊢ Set.Subsingleton B

State before:
case has_trivial_blocks'.inl.h
M : Type u_2
inst✝⁴ : Group M
α : Type u_1
inst✝³ : MulAction M α
N : Type ?u.75053
β : Type ?u.75056
inst✝² : Group N
inst✝¹ : MulAction N β
inst✝ : Fintype α
hGX : IsPretransitive M α
hp : Nat.Prime (Fintype.card α)
B : Set α
hB : IsBlock M B
hB' : Set.Subsingleton B
⊢ Set.Subsingleton B
Tactic:
exact hB'
State after:
no goals

State before:
case has_trivial_blocks'.inr
M : Type u_2
inst✝⁴ : Group M
α : Type u_1
inst✝³ : MulAction M α
N : Type ?u.75053
β : Type ?u.75056
inst✝² : Group N
inst✝¹ : MulAction N β
inst✝ : Fintype α
hGX : IsPretransitive M α
hp : Nat.Prime (Fintype.card α)
B : Set α
hB : IsBlock M B
hB' : Set.Nontrivial B
⊢ IsTrivialBlock B
Tactic:
apply Or.intro_right
State after:
case has_trivial_blocks'.inr.h
M : Type u_2
inst✝⁴ : Group M
α : Type u_1
inst✝³ : MulAction M α
N : Type ?u.75053
β : Type ?u.75056
inst✝² : Group N
inst✝¹ : MulAction N β
inst✝ : Fintype α
hGX : IsPretransitive M α
hp : Nat.Prime (Fintype.card α)
B : Set α
hB : IsBlock M B
hB' : Set.Nontrivial B
⊢ B = ⊤

State before:
case has_trivial_blocks'.inr.h
M : Type u_2
inst✝⁴ : Group M
α : Type u_1
inst✝³ : MulAction M α
N : Type ?u.75053
β : Type ?u.75056
inst✝² : Group N
inst✝¹ : MulAction N β
inst✝ : Fintype α
hGX : IsPretransitive M α
hp : Nat.Prime (Fintype.card α)
B : Set α
hB : IsBlock M B
hB' : Set.Nontrivial B
⊢ Set.ncard B = 1 ∨ Set.ncard B = Fintype.card α
Tactic:
rw [← Nat.dvd_prime hp]
State after:
case has_trivial_blocks'.inr.h
M : Type u_2
inst✝⁴ : Group M
α : Type u_1
inst✝³ : MulAction M α
N : Type ?u.75053
β : Type ?u.75056
inst✝² : Group N
inst✝¹ : MulAction N β
inst✝ : Fintype α
hGX : IsPretransitive M α
hp : Nat.Prime (Fintype.card α)
B : Set α
hB : IsBlock M B
hB' : Set.Nontrivial B
⊢ Set.ncard B ∣ Fintype.card α

State before:
case has_trivial_blocks'.inr.h
M : Type u_2
inst✝⁴ : Group M
α : Type u_1
inst✝³ : MulAction M α
N : Type ?u.75053
β : Type ?u.75056
inst✝² : Group N
inst✝¹ : MulAction N β
inst✝ : Fintype α
hGX : IsPretransitive M α
hp : Nat.Prime (Fintype.card α)
B : Set α
hB : IsBlock M B
hB' : Set.Nontrivial B
⊢ Set.ncard B ∣ Fintype.card α
Tactic:
simp only [← Nat.card_eq_fintype_card]
State after:
case has_trivial_blocks'.inr.h
M : Type u_2
inst✝⁴ : Group M
α : Type u_1
inst✝³ : MulAction M α
N : Type ?u.75053
β : Type ?u.75056
inst✝² : Group N
inst✝¹ : MulAction N β
inst✝ : Fintype α
hGX : IsPretransitive M α
hp : Nat.Prime (Fintype.card α)
B : Set α
hB : IsBlock M B
hB' : Set.Nontrivial B
⊢ Set.ncard B ∣ Nat.card α

State before:
case has_trivial_blocks'.inr.h
M : Type u_2
inst✝⁴ : Group M
α : Type u_1
inst✝³ : MulAction M α
N : Type ?u.75053
β : Type ?u.75056
inst✝² : Group N
inst✝¹ : MulAction N β
inst✝ : Fintype α
hGX : IsPretransitive M α
hp : Nat.Prime (Fintype.card α)
B : Set α
hB : IsBlock M B
hB' : Set.Nontrivial B
⊢ Set.ncard B ∣ Nat.card α
Tactic:
apply ncard_of_block_divides hB
State after:
case has_trivial_blocks'.inr.h
M : Type u_2
inst✝⁴ : Group M
α : Type u_1
inst✝³ : MulAction M α
N : Type ?u.75053
β : Type ?u.75056
inst✝² : Group N
inst✝¹ : MulAction N β
inst✝ : Fintype α
hGX : IsPretransitive M α
hp : Nat.Prime (Fintype.card α)
B : Set α
hB : IsBlock M B
hB' : Set.Nontrivial B
⊢ Set.Nonempty B

State before:
case has_trivial_blocks'.inr.h
M : Type u_2
inst✝⁴ : Group M
α : Type u_1
inst✝³ : MulAction M α
N : Type ?u.75053
β : Type ?u.75056
inst✝² : Group N
inst✝¹ : MulAction N β
inst✝ : Fintype α
hGX : IsPretransitive M α
hp : Nat.Prime (Fintype.card α)
B : Set α
hB : IsBlock M B
hB' : Set.Nontrivial B
⊢ Set.Nonempty B
Tactic:
exact Set.Nontrivial.nonempty hB'
State after:
no goals

State before:
M : Type u_2
inst✝⁴ : Group M
α : Type u_1
inst✝³ : MulAction M α
N : Type ?u.75053
β : Type ?u.75056
inst✝² : Group N
inst✝¹ : MulAction N β
inst✝ : Fintype α
hGX : IsPretransitive M α
hp : Nat.Prime (Fintype.card α)
B : Set α
hB : IsBlock M B
hB' : Set.Nontrivial B
this : Set.ncard B = 1 ∨ Set.ncard B = Fintype.card α
⊢ B = ⊤
Tactic:
cases' this with h h
State after:
case inl
M : Type u_2
inst✝⁴ : Group M
α : Type u_1
inst✝³ : MulAction M α
N : Type ?u.75053
β : Type ?u.75056
inst✝² : Group N
inst✝¹ : MulAction N β
inst✝ : Fintype α
hGX : IsPretransitive M α
hp : Nat.Prime (Fintype.card α)
B : Set α
hB : IsBlock M B
hB' : Set.Nontrivial B
h : Set.ncard B = 1
⊢ B = ⊤

case inr
M : Type u_2
inst✝⁴ : Group M
α : Type u_1
inst✝³ : MulAction M α
N : Type ?u.75053
β : Type ?u.75056
inst✝² : Group N
inst✝¹ : MulAction N β
inst✝ : Fintype α
hGX : IsPretransitive M α
hp : Nat.Prime (Fintype.card α)
B : Set α
hB : IsBlock M B
hB' : Set.Nontrivial B
h : Set.ncard B = Fintype.card α
⊢ B = ⊤

State before:
case inl
M : Type u_2
inst✝⁴ : Group M
α : Type u_1
inst✝³ : MulAction M α
N : Type ?u.75053
β : Type ?u.75056
inst✝² : Group N
inst✝¹ : MulAction N β
inst✝ : Fintype α
hGX : IsPretransitive M α
hp : Nat.Prime (Fintype.card α)
B : Set α
hB : IsBlock M B
hB' : Set.Nontrivial B
h : Set.ncard B = 1
⊢ B = ⊤
Tactic:
exfalso
State after:
case inl
M : Type u_2
inst✝⁴ : Group M
α : Type u_1
inst✝³ : MulAction M α
N : Type ?u.75053
β : Type ?u.75056
inst✝² : Group N
inst✝¹ : MulAction N β
inst✝ : Fintype α
hGX : IsPretransitive M α
hp : Nat.Prime (Fintype.card α)
B : Set α
hB : IsBlock M B
hB' : Set.Nontrivial B
h : Set.ncard B = 1
⊢ False

State before:
case inl
M : Type u_2
inst✝⁴ : Group M
α : Type u_1
inst✝³ : MulAction M α
N : Type ?u.75053
β : Type ?u.75056
inst✝² : Group N
inst✝¹ : MulAction N β
inst✝ : Fintype α
hGX : IsPretransitive M α
hp : Nat.Prime (Fintype.card α)
B : Set α
hB : IsBlock M B
hB' : Set.Nontrivial B
h : Set.ncard B = 1
⊢ False
Tactic:
rw [← Set.one_lt_ncard_iff_nontrivial, ← not_le] at hB'
State after:
case inl
M : Type u_2
inst✝⁴ : Group M
α : Type u_1
inst✝³ : MulAction M α
N : Type ?u.75053
β : Type ?u.75056
inst✝² : Group N
inst✝¹ : MulAction N β
inst✝ : Fintype α
hGX : IsPretransitive M α
hp : Nat.Prime (Fintype.card α)
B : Set α
hB : IsBlock M B
hB' : ¬Set.ncard B ≤ 1
h : Set.ncard B = 1
⊢ False

State before:
case inl
M : Type u_2
inst✝⁴ : Group M
α : Type u_1
inst✝³ : MulAction M α
N : Type ?u.75053
β : Type ?u.75056
inst✝² : Group N
inst✝¹ : MulAction N β
inst✝ : Fintype α
hGX : IsPretransitive M α
hp : Nat.Prime (Fintype.card α)
B : Set α
hB : IsBlock M B
hB' : ¬Set.ncard B ≤ 1
h : Set.ncard B = 1
⊢ False
Tactic:
exact hB' (le_of_eq h)
State after:
no goals

State before:
case inr
M : Type u_2
inst✝⁴ : Group M
α : Type u_1
inst✝³ : MulAction M α
N : Type ?u.75053
β : Type ?u.75056
inst✝² : Group N
inst✝¹ : MulAction N β
inst✝ : Fintype α
hGX : IsPretransitive M α
hp : Nat.Prime (Fintype.card α)
B : Set α
hB : IsBlock M B
hB' : Set.Nontrivial B
h : Set.ncard B = Fintype.card α
⊢ B = ⊤
Tactic:
rw [Set.eq_top_iff_ncard]
State after:
case inr
M : Type u_2
inst✝⁴ : Group M
α : Type u_1
inst✝³ : MulAction M α
N : Type ?u.75053
β : Type ?u.75056
inst✝² : Group N
inst✝¹ : MulAction N β
inst✝ : Fintype α
hGX : IsPretransitive M α
hp : Nat.Prime (Fintype.card α)
B : Set α
hB : IsBlock M B
hB' : Set.Nontrivial B
h : Set.ncard B = Fintype.card α
⊢ Set.ncard B = Fintype.card α

State before:
case inr
M : Type u_2
inst✝⁴ : Group M
α : Type u_1
inst✝³ : MulAction M α
N : Type ?u.75053
β : Type ?u.75056
inst✝² : Group N
inst✝¹ : MulAction N β
inst✝ : Fintype α
hGX : IsPretransitive M α
hp : Nat.Prime (Fintype.card α)
B : Set α
hB : IsBlock M B
hB' : Set.Nontrivial B
h : Set.ncard B = Fintype.card α
⊢ Set.ncard B = Fintype.card α
Tactic:
exact h
State after:
no goals