Theorem: isPreprimitive_of_large_image (Jordan/Primitive.lean)

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

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

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]
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 = ⊤

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

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

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

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

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

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

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

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)
State after:
no goals

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

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']
State after:
no goals

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

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

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

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

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
⊢ ∀ i ∈ Set.toFinset (Set.range fun g => g • B), (Set.toFinset (Set.range ⇑f ∩ i)).card ≤ 1
Tactic:
intro t ht
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 : Set β
ht : t ∈ Set.toFinset (Set.range fun g => g • B)
⊢ (Set.toFinset (Set.range ⇑f ∩ t)).card ≤ 1

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 : Set β
ht : t ∈ Set.toFinset (Set.range fun g => g • B)
⊢ (Set.toFinset (Set.range ⇑f ∩ t)).card ≤ 1
Tactic:
rw [← Set.ncard_eq_toFinset_card', ← Set.subsingleton_iff_ncard_le_one,
  Set.inter_comm, ← Set.image_preimage_eq_inter_range]
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 : Set β
ht : t ∈ Set.toFinset (Set.range fun g => g • B)
⊢ Set.Subsingleton (⇑f '' (⇑f ⁻¹' t))

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 : Set β
ht : t ∈ Set.toFinset (Set.range fun g => g • B)
⊢ Set.Subsingleton (⇑f '' (⇑f ⁻¹' t))
Tactic:
apply Set.Subsingleton.image
State after:
case hs
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 : Set β
ht : t ∈ Set.toFinset (Set.range fun g => g • B)
⊢ Set.Subsingleton (⇑f ⁻¹' t)

State before:
case hs
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 : Set β
ht : t ∈ Set.toFinset (Set.range fun g => g • B)
⊢ Set.Subsingleton (⇑f ⁻¹' t)
Tactic:
simp only [Set.mem_toFinset, Set.mem_range] at ht
State after:
case hs
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 : Set β
ht : ∃ y, y • B = t
⊢ Set.Subsingleton (⇑f ⁻¹' t)

State before:
case hs
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 : Set β
ht : ∃ y, y • B = t
⊢ Set.Subsingleton (⇑f ⁻¹' t)
Tactic:
obtain ⟨g, rfl⟩ := ht
State after:
case hs.intro
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
g : N
⊢ Set.Subsingleton (⇑f ⁻¹' (g • B))

State before:
case hs.intro
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
g : N
⊢ Set.Subsingleton (⇑f ⁻¹' (g • B))
Tactic:
apply Or.resolve_right
  (hM.has_trivial_blocks (IsBlock_preimage f (IsBlock_of_block g hB)))
State after:
case hs.intro
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
g : N
⊢ ¬⇑f ⁻¹' (g • B) = ⊤

State before:
case hs.intro
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
g : N
⊢ ¬⇑f ⁻¹' (g • B) = ⊤
Tactic:
intro h
State after:
case hs.intro
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
g : N
h : ⇑f ⁻¹' (g • B) = ⊤
⊢ False

State before:
case hs.intro
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
g : N
h : ⇑f ⁻¹' (g • B) = ⊤
⊢ False
Tactic:
apply hB_ne_top
State after:
case hs.intro
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
g : N
h : ⇑f ⁻¹' (g • B) = ⊤
⊢ B = ⊤

State before:
case hs.intro
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
g : N
h : ⇑f ⁻¹' (g • B) = ⊤
⊢ B = ⊤
Tactic:
apply is_top_of_large_block hB
State after:
case hs.intro
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
g : N
h : ⇑f ⁻¹' (g • B) = ⊤
⊢ Nat.card β < 2 * Set.ncard B

State before:
case hs.intro
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
g : N
h : ⇑f ⁻¹' (g • B) = ⊤
⊢ Nat.card β < 2 * Set.ncard B
Tactic:
rw [Nat.card_eq_fintype_card]
State after:
case hs.intro
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
g : N
h : ⇑f ⁻¹' (g • B) = ⊤
⊢ Fintype.card β < 2 * Set.ncard B

State before:
case hs.intro
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
g : N
h : ⇑f ⁻¹' (g • B) = ⊤
⊢ Fintype.card β < 2 * Set.ncard B
Tactic:
apply lt_of_lt_of_le hf'
State after:
case hs.intro
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
g : N
h : ⇑f ⁻¹' (g • B) = ⊤
⊢ 2 * Set.ncard (Set.range ⇑f) ≤ 2 * Set.ncard B

State before:
case hs.intro
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
g : N
h : ⇑f ⁻¹' (g • B) = ⊤
⊢ 2 * Set.ncard (Set.range ⇑f) ≤ 2 * Set.ncard B
Tactic:
simp only [mul_le_mul_left, Nat.succ_pos', ← smul_set_ncard_eq g B]
State after:
case hs.intro
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
g : N
h : ⇑f ⁻¹' (g • B) = ⊤
⊢ Set.ncard (Set.range ⇑f) ≤ Set.ncard (g • B)

State before:
case hs.intro
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
g : N
h : ⇑f ⁻¹' (g • B) = ⊤
⊢ Set.ncard (Set.range ⇑f) ≤ Set.ncard (g • B)
Tactic:
apply Set.ncard_le_ncard
State after:
case hs.intro.hst
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
g : N
h : ⇑f ⁻¹' (g • B) = ⊤
⊢ Set.range ⇑f ⊆ g • B

case hs.intro.ht
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
g : N
h : ⇑f ⁻¹' (g • B) = ⊤
⊢ autoParam (Set.Finite (g • B)) _auto✝

State before:
case hs.intro.hst
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
g : N
h : ⇑f ⁻¹' (g • B) = ⊤
⊢ Set.range ⇑f ⊆ g • B

case hs.intro.ht
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
g : N
h : ⇑f ⁻¹' (g • B) = ⊤
⊢ autoParam (Set.Finite (g • B)) _auto✝
Tactic:
rw [← Set.image_univ, Set.image_subset_iff, ← Set.top_eq_univ, h]
State after:
case hs.intro.ht
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
g : N
h : ⇑f ⁻¹' (g • B) = ⊤
⊢ autoParam (Set.Finite (g • B)) _auto✝

State before:
case hs.intro.ht
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
g : N
h : ⇑f ⁻¹' (g • B) = ⊤
⊢ autoParam (Set.Finite (g • B)) _auto✝
Tactic:
exact Set.toFinite (g • B)
State after:
no goals