internlm/Lean-Github huggingface dataset:
Theorem: isPreprimitive_of_prime
Proof 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
Proof 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 = ⊤
Theorem: isPreprimitive_of_prime
Proof 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]
Proof 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 α
Theorem: isPreprimitive_of_prime
Proof 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]
Proof 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 α
Theorem: isPreprimitive_of_prime
Proof 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
Proof 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
Theorem: isPreprimitive_of_prime
Proof 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'
Proof state after:
no goals
Theorem: isPreprimitive_of_prime
Proof 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
Proof 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 = ⊤
Theorem: isPreprimitive_of_prime
Proof 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
Proof 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
Theorem: isPreprimitive_of_prime
Proof 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'
Proof 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
Theorem: isPreprimitive_of_prime
Proof 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)
Proof state after:
no goals
Theorem: isPreprimitive_of_prime
Proof 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]
Proof 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 α
Theorem: isPreprimitive_of_prime
Proof 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
Proof state after:
no goals
Theorem: isPreprimitive_of_large_image
Proof state before:
M : Type u_4
inst✝⁴ : Group M
α : Type u_3
inst✝³ : MulAction M α
N : Type u_2
β : Type u_1
inst✝² : Group N
inst✝¹ : MulAction N β
inst✝ : Fintype β
htβ : IsPretransitive N β
φ : M → N
f : α →ₑ[φ] β
hM : IsPreprimitive M α
hf' : Fintype.card β < 2 * Set.ncard (Set.range ⇑f)
⊢ IsPreprimitive N β
Tactic:
apply IsPreprimitive.mk
Proof state after:
case has_trivial_blocks'
M : Type u_4
inst✝⁴ : Group M
α : Type u_3
inst✝³ : MulAction M α
N : Type u_2
β : Type u_1
inst✝² : Group N
inst✝¹ : MulAction N β
inst✝ : Fintype β
htβ : IsPretransitive N β
φ : M → N
f : α →ₑ[φ] β
hM : IsPreprimitive M α
hf' : Fintype.card β < 2 * Set.ncard (Set.range ⇑f)
⊢ ∀ {B : Set β}, IsBlock N B → IsTrivialBlock B
Theorem: isPreprimitive_of_large_image
Proof state before:
case has_trivial_blocks'
M : Type u_4
inst✝⁴ : Group M
α : Type u_3
inst✝³ : MulAction M α
N : Type u_2
β : Type u_1
inst✝² : Group N
inst✝¹ : MulAction N β
inst✝ : Fintype β
htβ : IsPretransitive N β
φ : M → N
f : α →ₑ[φ] β
hM : IsPreprimitive M α
hf' : Fintype.card β < 2 * Set.ncard (Set.range ⇑f)
⊢ ∀ {B : Set β}, IsBlock N B → IsTrivialBlock B
Tactic:
intro B hB
Proof state after:
case has_trivial_blocks'
M : Type u_4
inst✝⁴ : Group M
α : Type u_3
inst✝³ : MulAction M α
N : Type u_2
β : Type u_1
inst✝² : Group N
inst✝¹ : MulAction N β
inst✝ : Fintype β
htβ : IsPretransitive N β
φ : M → N
f : α →ₑ[φ] β
hM : IsPreprimitive M α
hf' : Fintype.card β < 2 * Set.ncard (Set.range ⇑f)
B : Set β
hB : IsBlock N B
⊢ IsTrivialBlock B
Theorem: isPreprimitive_of_large_image
Proof state before:
case has_trivial_blocks'
M : Type u_4
inst✝⁴ : Group M
α : Type u_3
inst✝³ : MulAction M α
N : Type u_2
β : Type u_1
inst✝² : Group N
inst✝¹ : MulAction N β
inst✝ : Fintype β
htβ : IsPretransitive N β
φ : M → N
f : α →ₑ[φ] β
hM : IsPreprimitive M α
hf' : Fintype.card β < 2 * Set.ncard (Set.range ⇑f)
B : Set β
hB : IsBlock N B
⊢ IsTrivialBlock B
Tactic:
dsimp only [IsTrivialBlock]
Proof state after:
case has_trivial_blocks'
M : Type u_4
inst✝⁴ : Group M
α : Type u_3
inst✝³ : MulAction M α
N : Type u_2
β : Type u_1
inst✝² : Group N
inst✝¹ : MulAction N β
inst✝ : Fintype β
htβ : IsPretransitive N β
φ : M → N
f : α →ₑ[φ] β
hM : IsPreprimitive M α
hf' : Fintype.card β < 2 * Set.ncard (Set.range ⇑f)
B : Set β
hB : IsBlock N B
⊢ Set.Subsingleton B ∨ B = ⊤
Theorem: isPreprimitive_of_large_image
Proof state before:
case has_trivial_blocks'
M : Type u_4
inst✝⁴ : Group M
α : Type u_3
inst✝³ : MulAction M α
N : Type u_2
β : Type u_1
inst✝² : Group N
inst✝¹ : MulAction N β
inst✝ : Fintype β
htβ : IsPretransitive N β
φ : M → N
f : α →ₑ[φ] β
hM : IsPreprimitive M α
hf' : Fintype.card β < 2 * Set.ncard (Set.range ⇑f)
B : Set β
hB : IsBlock N B
⊢ Set.Subsingleton B ∨ B = ⊤
Tactic:
rw [or_iff_not_imp_right]
Proof state after:
case has_trivial_blocks'
M : Type u_4
inst✝⁴ : Group M
α : Type u_3
inst✝³ : MulAction M α
N : Type u_2
β : Type u_1
inst✝² : Group N
inst✝¹ : MulAction N β
inst✝ : Fintype β
htβ : IsPretransitive N β
φ : M → N
f : α →ₑ[φ] β
hM : IsPreprimitive M α
hf' : Fintype.card β < 2 * Set.ncard (Set.range ⇑f)
B : Set β
hB : IsBlock N B
⊢ ¬B = ⊤ → Set.Subsingleton B
Theorem: isPreprimitive_of_large_image
Proof state before:
case has_trivial_blocks'
M : Type u_4
inst✝⁴ : Group M
α : Type u_3
inst✝³ : MulAction M α
N : Type u_2
β : Type u_1
inst✝² : Group N
inst✝¹ : MulAction N β
inst✝ : Fintype β
htβ : IsPretransitive N β
φ : M → N
f : α →ₑ[φ] β
hM : IsPreprimitive M α
hf' : Fintype.card β < 2 * Set.ncard (Set.range ⇑f)
B : Set β
hB : IsBlock N B
⊢ ¬B = ⊤ → Set.Subsingleton B
Tactic:
intro hB_ne_top
Proof state after:
case has_trivial_blocks'
M : Type u_4
inst✝⁴ : Group M
α : Type u_3
inst✝³ : MulAction M α
N : Type u_2
β : Type u_1
inst✝² : Group N
inst✝¹ : MulAction N β
inst✝ : Fintype β
htβ : IsPretransitive N β
φ : M → N
f : α →ₑ[φ] β
hM : IsPreprimitive M α
hf' : Fintype.card β < 2 * Set.ncard (Set.range ⇑f)
B : Set β
hB : IsBlock N B
hB_ne_top : ¬B = ⊤
⊢ Set.Subsingleton B
Theorem: isPreprimitive_of_large_image
Proof state before:
case has_trivial_blocks'
M : Type u_4
inst✝⁴ : Group M
α : Type u_3
inst✝³ : MulAction M α
N : Type u_2
β : Type u_1
inst✝² : Group N
inst✝¹ : MulAction N β
inst✝ : Fintype β
htβ : IsPretransitive N β
φ : M → N
f : α →ₑ[φ] β
hM : IsPreprimitive M α
hf' : Fintype.card β < 2 * Set.ncard (Set.range ⇑f)
B : Set β
hB : IsBlock N B
hB_ne_top : ¬B = ⊤
⊢ Set.Subsingleton B
Tactic:
rw [Set.subsingleton_iff_ncard_le_one, ← Nat.lt_succ]
Proof state after:
case has_trivial_blocks'
M : Type u_4
inst✝⁴ : Group M
α : Type u_3
inst✝³ : MulAction M α
N : Type u_2
β : Type u_1
inst✝² : Group N
inst✝¹ : MulAction N β
inst✝ : Fintype β
htβ : IsPretransitive N β
φ : M → N
f : α →ₑ[φ] β
hM : IsPreprimitive M α
hf' : Fintype.card β < 2 * Set.ncard (Set.range ⇑f)
B : Set β
hB : IsBlock N B
hB_ne_top : ¬B = ⊤
⊢ Set.ncard B < Nat.succ 1
Theorem: isPreprimitive_of_large_image
Proof state before:
case has_trivial_blocks'
M : Type u_4
inst✝⁴ : Group M
α : Type u_3
inst✝³ : MulAction M α
N : Type u_2
β : Type u_1
inst✝² : Group N
inst✝¹ : MulAction N β
inst✝ : Fintype β
htβ : IsPretransitive N β
φ : M → N
f : α →ₑ[φ] β
hM : IsPreprimitive M α
hf' : Fintype.card β < 2 * Set.ncard (Set.range ⇑f)
B : Set β
hB : IsBlock N B
hB_ne_top : ¬B = ⊤
⊢ Set.ncard B < Nat.succ 1
Tactic:
cases' Set.eq_empty_or_nonempty B with hBe hB_ne
Proof state after:
case has_trivial_blocks'.inl
M : Type u_4
inst✝⁴ : Group M
α : Type u_3
inst✝³ : MulAction M α
N : Type u_2
β : Type u_1
inst✝² : Group N
inst✝¹ : MulAction N β
inst✝ : Fintype β
htβ : IsPretransitive N β
φ : M → N
f : α →ₑ[φ] β
hM : IsPreprimitive M α
hf' : Fintype.card β < 2 * Set.ncard (Set.range ⇑f)
B : Set β
hB : IsBlock N B
hB_ne_top : ¬B = ⊤
hBe : B = ∅
⊢ Set.ncard B < Nat.succ 1

case has_trivial_blocks'.inr
M : Type u_4
inst✝⁴ : Group M
α : Type u_3
inst✝³ : MulAction M α
N : Type u_2
β : Type u_1
inst✝² : Group N
inst✝¹ : MulAction N β
inst✝ : Fintype β
htβ : IsPretransitive N β
φ : M → N
f : α →ₑ[φ] β
hM : IsPreprimitive M α
hf' : Fintype.card β < 2 * Set.ncard (Set.range ⇑f)
B : Set β
hB : IsBlock N B
hB_ne_top : ¬B = ⊤
hB_ne : Set.Nonempty B
⊢ Set.ncard B < Nat.succ 1
Theorem: isPreprimitive_of_large_image
Proof state before:
case has_trivial_blocks'.inr
M : Type u_4
inst✝⁴ : Group M
α : Type u_3
inst✝³ : MulAction M α
N : Type u_2
β : Type u_1
inst✝² : Group N
inst✝¹ : MulAction N β
inst✝ : Fintype β
htβ : IsPretransitive N β
φ : M → N
f : α →ₑ[φ] β
hM : IsPreprimitive M α
hf' : Fintype.card β < 2 * Set.ncard (Set.range ⇑f)
B : Set β
hB : IsBlock N B
hB_ne_top : ¬B = ⊤
hB_ne : Set.Nonempty B
⊢ Set.ncard B < Nat.succ 1
Tactic:
apply lt_of_mul_lt_mul_right (lt_of_le_of_lt _ hf') (Nat.zero_le _)
Proof state after:
M : Type u_4
inst✝⁴ : Group M
α : Type u_3
inst✝³ : MulAction M α
N : Type u_2
β : Type u_1
inst✝² : Group N
inst✝¹ : MulAction N β
inst✝ : Fintype β
htβ : IsPretransitive N β
φ : M → N
f : α →ₑ[φ] β
hM : IsPreprimitive M α
hf' : Fintype.card β < 2 * Set.ncard (Set.range ⇑f)
B : Set β
hB : IsBlock N B
hB_ne_top : ¬B = ⊤
hB_ne : Set.Nonempty B
⊢ Set.ncard B * Set.ncard (Set.range ⇑f) ≤ Fintype.card β
Theorem: isPreprimitive_of_large_image
Proof state before:
M : Type u_4
inst✝⁴ : Group M
α : Type u_3
inst✝³ : MulAction M α
N : Type u_2
β : Type u_1
inst✝² : Group N
inst✝¹ : MulAction N β
inst✝ : Fintype β
htβ : IsPretransitive N β
φ : M → N
f : α →ₑ[φ] β
hM : IsPreprimitive M α
hf' : Fintype.card β < 2 * Set.ncard (Set.range ⇑f)
B : Set β
hB : IsBlock N B
hB_ne_top : ¬B = ⊤
hB_ne : Set.Nonempty B
⊢ Set.ncard B * Set.ncard (Set.range ⇑f) ≤ Fintype.card β
Tactic:
simp only [← Nat.card_eq_fintype_card, ← ncard_block_mul_ncard_orbit_eq hB hB_ne]
Proof state after:
M : Type u_4
inst✝⁴ : Group M
α : Type u_3
inst✝³ : MulAction M α
N : Type u_2
β : Type u_1
inst✝² : Group N
inst✝¹ : MulAction N β
inst✝ : Fintype β
htβ : IsPretransitive N β
φ : M → N
f : α →ₑ[φ] β
hM : IsPreprimitive M α
hf' : Fintype.card β < 2 * Set.ncard (Set.range ⇑f)
B : Set β
hB : IsBlock N B
hB_ne_top : ¬B = ⊤
hB_ne : Set.Nonempty B
⊢ Set.ncard B * Set.ncard (Set.range ⇑f) ≤ Set.ncard B * Set.ncard (Set.range fun g => g • B)
Theorem: isPreprimitive_of_large_image
Proof state before:
M : Type u_4
inst✝⁴ : Group M
α : Type u_3
inst✝³ : MulAction M α
N : Type u_2
β : Type u_1
inst✝² : Group N
inst✝¹ : MulAction N β
inst✝ : Fintype β
htβ : IsPretransitive N β
φ : M → N
f : α →ₑ[φ] β
hM : IsPreprimitive M α
hf' : Fintype.card β < 2 * Set.ncard (Set.range ⇑f)
B : Set β
hB : IsBlock N B
hB_ne_top : ¬B = ⊤
hB_ne : Set.Nonempty B
⊢ Set.ncard B * Set.ncard (Set.range ⇑f) ≤ Set.ncard B * Set.ncard (Set.range fun g => g • B)
Tactic:
apply Nat.mul_le_mul_left _
Proof state after:
M : Type u_4
inst✝⁴ : Group M
α : Type u_3
inst✝³ : MulAction M α
N : Type u_2
β : Type u_1
inst✝² : Group N
inst✝¹ : MulAction N β
inst✝ : Fintype β
htβ : IsPretransitive N β
φ : M → N
f : α →ₑ[φ] β
hM : IsPreprimitive M α
hf' : Fintype.card β < 2 * Set.ncard (Set.range ⇑f)
B : Set β
hB : IsBlock N B
hB_ne_top : ¬B = ⊤
hB_ne : Set.Nonempty B
⊢ Set.ncard (Set.range ⇑f) ≤ Set.ncard (Set.range fun g => g • B)
Theorem: isPreprimitive_of_large_image
Proof state before:
M : Type u_4
inst✝⁴ : Group M
α : Type u_3
inst✝³ : MulAction M α
N : Type u_2
β : Type u_1
inst✝² : Group N
inst✝¹ : MulAction N β
inst✝ : Fintype β
htβ : IsPretransitive N β
φ : M → N
f : α →ₑ[φ] β
hM : IsPreprimitive M α
hf' : Fintype.card β < 2 * Set.ncard (Set.range ⇑f)
B : Set β
hB : IsBlock N B
hB_ne_top : ¬B = ⊤
hB_ne : Set.Nonempty B
⊢ Set.ncard (Set.range ⇑f) ≤ Set.ncard (Set.range fun g => g • B)
Tactic:
classical
simp only [Set.ncard_eq_toFinset_card']
rw [Setoid.IsPartition.card_set_eq_sum_parts (Set.range f)
    (IsBlockSystem.of_block hB hB_ne).left]
rw [Finset.card_eq_sum_ones]
refine' Finset.sum_le_sum _
intro t ht
rw [← Set.ncard_eq_toFinset_card', ← Set.subsingleton_iff_ncard_le_one,
  Set.inter_comm, ← Set.image_preimage_eq_inter_range]
apply Set.Subsingleton.image
simp only [Set.mem_toFinset, Set.mem_range] at ht
obtain ⟨g, rfl⟩ := ht
apply Or.resolve_right
  (hM.has_trivial_blocks (IsBlock_preimage f (IsBlock_of_block g hB)))
intro h
apply hB_ne_top
apply is_top_of_large_block hB
rw [Nat.card_eq_fintype_card]
apply lt_of_lt_of_le hf'
simp only [mul_le_mul_left, Nat.succ_pos', ← smul_set_ncard_eq g B]
apply Set.ncard_le_ncard
rw [← Set.image_univ, Set.image_subset_iff, ← Set.top_eq_univ, h]
exact Set.toFinite (g • B)
Proof state after:
no goals
Theorem: isPreprimitive_of_large_image
Proof state before:
case has_trivial_blocks'.inl
M : Type u_4
inst✝⁴ : Group M
α : Type u_3
inst✝³ : MulAction M α
N : Type u_2
β : Type u_1
inst✝² : Group N
inst✝¹ : MulAction N β
inst✝ : Fintype β
htβ : IsPretransitive N β
φ : M → N
f : α →ₑ[φ] β
hM : IsPreprimitive M α
hf' : Fintype.card β < 2 * Set.ncard (Set.range ⇑f)
B : Set β
hB : IsBlock N B
hB_ne_top : ¬B = ⊤
hBe : B = ∅
⊢ Set.ncard B < Nat.succ 1
Tactic:
rw [hBe]
Proof state after:
case has_trivial_blocks'.inl
M : Type u_4
inst✝⁴ : Group M
α : Type u_3
inst✝³ : MulAction M α
N : Type u_2
β : Type u_1
inst✝² : Group N
inst✝¹ : MulAction N β
inst✝ : Fintype β
htβ : IsPretransitive N β
φ : M → N
f : α →ₑ[φ] β
hM : IsPreprimitive M α
hf' : Fintype.card β < 2 * Set.ncard (Set.range ⇑f)
B : Set β
hB : IsBlock N B
hB_ne_top : ¬B = ⊤
hBe : B = ∅
⊢ Set.ncard ∅ < Nat.succ 1
Theorem: isPreprimitive_of_large_image
Proof state before:
case has_trivial_blocks'.inl
M : Type u_4
inst✝⁴ : Group M
α : Type u_3
inst✝³ : MulAction M α
N : Type u_2
β : Type u_1
inst✝² : Group N
inst✝¹ : MulAction N β
inst✝ : Fintype β
htβ : IsPretransitive N β
φ : M → N
f : α →ₑ[φ] β
hM : IsPreprimitive M α
hf' : Fintype.card β < 2 * Set.ncard (Set.range ⇑f)
B : Set β
hB : IsBlock N B
hB_ne_top : ¬B = ⊤
hBe : B = ∅
⊢ Set.ncard ∅ < Nat.succ 1
Tactic:
simp only [Set.ncard_empty, Nat.succ_pos']
Proof state after:
no goals
Theorem: isPreprimitive_of_large_image
Proof state before:
M : Type u_4
inst✝⁴ : Group M
α : Type u_3
inst✝³ : MulAction M α
N : Type u_2
β : Type u_1
inst✝² : Group N
inst✝¹ : MulAction N β
inst✝ : Fintype β
htβ : IsPretransitive N β
φ : M → N
f : α →ₑ[φ] β
hM : IsPreprimitive M α
hf' : Fintype.card β < 2 * Set.ncard (Set.range ⇑f)
B : Set β
hB : IsBlock N B
hB_ne_top : ¬B = ⊤
hB_ne : Set.Nonempty B
⊢ Set.ncard (Set.range ⇑f) ≤ Set.ncard (Set.range fun g => g • B)
Tactic:
simp only [Set.ncard_eq_toFinset_card']
Proof state after:
M : Type u_4
inst✝⁴ : Group M
α : Type u_3
inst✝³ : MulAction M α
N : Type u_2
β : Type u_1
inst✝² : Group N
inst✝¹ : MulAction N β
inst✝ : Fintype β
htβ : IsPretransitive N β
φ : M → N
f : α →ₑ[φ] β
hM : IsPreprimitive M α
hf' : Fintype.card β < 2 * Set.ncard (Set.range ⇑f)
B : Set β
hB : IsBlock N B
hB_ne_top : ¬B = ⊤
hB_ne : Set.Nonempty B
⊢ (Set.toFinset (Set.range ⇑f)).card ≤ (Set.toFinset (Set.range fun g => g • B)).card
Theorem: isPreprimitive_of_large_image
Proof state before:
M : Type u_4
inst✝⁴ : Group M
α : Type u_3
inst✝³ : MulAction M α
N : Type u_2
β : Type u_1
inst✝² : Group N
inst✝¹ : MulAction N β
inst✝ : Fintype β
htβ : IsPretransitive N β
φ : M → N
f : α →ₑ[φ] β
hM : IsPreprimitive M α
hf' : Fintype.card β < 2 * Set.ncard (Set.range ⇑f)
B : Set β
hB : IsBlock N B
hB_ne_top : ¬B = ⊤
hB_ne : Set.Nonempty B
⊢ (Set.toFinset (Set.range ⇑f)).card ≤ (Set.toFinset (Set.range fun g => g • B)).card
Tactic:
rw [Setoid.IsPartition.card_set_eq_sum_parts (Set.range f)
    (IsBlockSystem.of_block hB hB_ne).left]
Proof state after:
M : Type u_4
inst✝⁴ : Group M
α : Type u_3
inst✝³ : MulAction M α
N : Type u_2
β : Type u_1
inst✝² : Group N
inst✝¹ : MulAction N β
inst✝ : Fintype β
htβ : IsPretransitive N β
φ : M → N
f : α →ₑ[φ] β
hM : IsPreprimitive M α
hf' : Fintype.card β < 2 * Set.ncard (Set.range ⇑f)
B : Set β
hB : IsBlock N B
hB_ne_top : ¬B = ⊤
hB_ne : Set.Nonempty B
⊢ ∑ t in Set.toFinset (Set.range fun g => g • B), (Set.toFinset (Set.range ⇑f ∩ t)).card ≤
    (Set.toFinset (Set.range fun g => g • B)).card
Theorem: isPreprimitive_of_large_image
Proof state before:
M : Type u_4
inst✝⁴ : Group M
α : Type u_3
inst✝³ : MulAction M α
N : Type u_2
β : Type u_1
inst✝² : Group N
inst✝¹ : MulAction N β
inst✝ : Fintype β
htβ : IsPretransitive N β
φ : M → N
f : α →ₑ[φ] β
hM : IsPreprimitive M α
hf' : Fintype.card β < 2 * Set.ncard (Set.range ⇑f)
B : Set β
hB : IsBlock N B
hB_ne_top : ¬B = ⊤
hB_ne : Set.Nonempty B
⊢ ∑ t in Set.toFinset (Set.range fun g => g • B), (Set.toFinset (Set.range ⇑f ∩ t)).card ≤
    (Set.toFinset (Set.range fun g => g • B)).card
Tactic:
rw [Finset.card_eq_sum_ones]
Proof state after:
M : Type u_4
inst✝⁴ : Group M
α : Type u_3
inst✝³ : MulAction M α
N : Type u_2
β : Type u_1
inst✝² : Group N
inst✝¹ : MulAction N β
inst✝ : Fintype β
htβ : IsPretransitive N β
φ : M → N
f : α →ₑ[φ] β
hM : IsPreprimitive M α
hf' : Fintype.card β < 2 * Set.ncard (Set.range ⇑f)
B : Set β
hB : IsBlock N B
hB_ne_top : ¬B = ⊤
hB_ne : Set.Nonempty B
⊢ ∑ t in Set.toFinset (Set.range fun g => g • B), (Set.toFinset (Set.range ⇑f ∩ t)).card ≤
    ∑ x in Set.toFinset (Set.range fun g => g • B), 1
Theorem: isPreprimitive_of_large_image
Proof state before:
M : Type u_4
inst✝⁴ : Group M
α : Type u_3
inst✝³ : MulAction M α
N : Type u_2
β : Type u_1
inst✝² : Group N
inst✝¹ : MulAction N β
inst✝ : Fintype β
htβ : IsPretransitive N β
φ : M → N
f : α →ₑ[φ] β
hM : IsPreprimitive M α
hf' : Fintype.card β < 2 * Set.ncard (Set.range ⇑f)
B : Set β
hB : IsBlock N B
hB_ne_top : ¬B = ⊤
hB_ne : Set.Nonempty B
⊢ ∑ t in Set.toFinset (Set.range fun g => g • B), (Set.toFinset (Set.range ⇑f ∩ t)).card ≤
    ∑ x in Set.toFinset (Set.range fun g => g • B), 1
Tactic:
refine' Finset.sum_le_sum _
Proof state after:
M : Type u_4
inst✝⁴ : Group M
α : Type u_3
inst✝³ : MulAction M α
N : Type u_2
β : Type u_1
inst✝² : Group N
inst✝¹ : MulAction N β
inst✝ : Fintype β
htβ : IsPretransitive N β
φ : M → N
f : α →ₑ[φ] β
hM : IsPreprimitive M α
hf' : Fintype.card β < 2 * Set.ncard (Set.range ⇑f)
B : Set β
hB : IsBlock N B
hB_ne_top : ¬B = ⊤
hB_ne : Set.Nonempty B
⊢ ∀ i ∈ Set.toFinset (Set.range fun g => g • B), (Set.toFinset (Set.range ⇑f ∩ i)).card ≤ 1