internlm/Lean-Github huggingface dataset:
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
⊢ ∀ i ∈ Set.toFinset (Set.range fun g => g • B), (Set.toFinset (Set.range ⇑f ∩ i)).card ≤ 1
Tactic:
intro t ht
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 : Set β
ht : t ∈ Set.toFinset (Set.range fun g => g • B)
⊢ (Set.toFinset (Set.range ⇑f ∩ t)).card ≤ 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 : 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]
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 : Set β
ht : t ∈ Set.toFinset (Set.range fun g => g • B)
⊢ Set.Subsingleton (⇑f '' (⇑f ⁻¹' t))
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 : Set β
ht : t ∈ Set.toFinset (Set.range fun g => g • B)
⊢ Set.Subsingleton (⇑f '' (⇑f ⁻¹' t))
Tactic:
apply Set.Subsingleton.image
Proof 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)
Theorem: isPreprimitive_of_large_image
Proof 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
Proof 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)
Theorem: isPreprimitive_of_large_image
Proof 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
Proof 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))
Theorem: isPreprimitive_of_large_image
Proof 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)))
Proof 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) = ⊤
Theorem: isPreprimitive_of_large_image
Proof 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
Proof 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
Theorem: isPreprimitive_of_large_image
Proof 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
Proof 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 = ⊤
Theorem: isPreprimitive_of_large_image
Proof 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
Proof 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
Theorem: isPreprimitive_of_large_image
Proof 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]
Proof 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
Theorem: isPreprimitive_of_large_image
Proof 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'
Proof 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
Theorem: isPreprimitive_of_large_image
Proof 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]
Proof 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)
Theorem: isPreprimitive_of_large_image
Proof 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
Proof 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✝
Theorem: isPreprimitive_of_large_image
Proof 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]
Proof 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✝
Theorem: isPreprimitive_of_large_image
Proof 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)
Proof state after:
no goals
Theorem: Rudio
Proof state before:
M : Type u_1
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type ?u.94224
β : Type ?u.94227
inst✝¹ : Group N
inst✝ : MulAction N β
hpGX : IsPreprimitive M α
A : Set α
hfA : Set.Finite A
hA : Set.Nonempty A
hA' : A ≠ ⊤
a b : α
h : a ≠ b
⊢ ∃ g, a ∈ g • A ∧ b ∉ g • A
Tactic:
let B := ⋂ (g : M) (_ : a ∈ g • A), g • A
Proof state after:
M : Type u_1
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type ?u.94224
β : Type ?u.94227
inst✝¹ : Group N
inst✝ : MulAction N β
hpGX : IsPreprimitive M α
A : Set α
hfA : Set.Finite A
hA : Set.Nonempty A
hA' : A ≠ ⊤
a b : α
h : a ≠ b
B : Set α := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
⊢ ∃ g, a ∈ g • A ∧ b ∉ g • A
Theorem: Rudio
Proof state before:
M : Type u_1
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type ?u.94224
β : Type ?u.94227
inst✝¹ : Group N
inst✝ : MulAction N β
hpGX : IsPreprimitive M α
A : Set α
hfA : Set.Finite A
hA : Set.Nonempty A
hA' : A ≠ ⊤
a b : α
h : a ≠ b
B : Set α := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
⊢ ∃ g, a ∈ g • A ∧ b ∉ g • A
Tactic:
suffices b ∉ B by
  rw [Set.mem_iInter] at this
  simpa only [Set.mem_iInter, not_forall, exists_prop] using this
Proof state after:
M : Type u_1
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type ?u.94224
β : Type ?u.94227
inst✝¹ : Group N
inst✝ : MulAction N β
hpGX : IsPreprimitive M α
A : Set α
hfA : Set.Finite A
hA : Set.Nonempty A
hA' : A ≠ ⊤
a b : α
h : a ≠ b
B : Set α := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
⊢ b ∉ B
Theorem: Rudio
Proof state before:
M : Type u_1
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type ?u.94224
β : Type ?u.94227
inst✝¹ : Group N
inst✝ : MulAction N β
hpGX : IsPreprimitive M α
A : Set α
hfA : Set.Finite A
hA : Set.Nonempty A
hA' : A ≠ ⊤
a b : α
h : a ≠ b
B : Set α := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
⊢ b ∉ B
Tactic:
suffices B = {a} by rw [this]; rw [Set.mem_singleton_iff]; exact Ne.symm h
Proof state after:
M : Type u_1
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type ?u.94224
β : Type ?u.94227
inst✝¹ : Group N
inst✝ : MulAction N β
hpGX : IsPreprimitive M α
A : Set α
hfA : Set.Finite A
hA : Set.Nonempty A
hA' : A ≠ ⊤
a b : α
h : a ≠ b
B : Set α := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
⊢ B = {a}
Theorem: Rudio
Proof state before:
M : Type u_1
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type ?u.94224
β : Type ?u.94227
inst✝¹ : Group N
inst✝ : MulAction N β
hpGX : IsPreprimitive M α
A : Set α
hfA : Set.Finite A
hA : Set.Nonempty A
hA' : A ≠ ⊤
a b : α
h : a ≠ b
B : Set α := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
⊢ B = {a}
Tactic:
cases' hpGX.has_trivial_blocks (IsBlock.of_subset a A hfA) with hyp hyp
Proof state after:
case inl
M : Type u_1
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type ?u.94224
β : Type ?u.94227
inst✝¹ : Group N
inst✝ : MulAction N β
hpGX : IsPreprimitive M α
A : Set α
hfA : Set.Finite A
hA : Set.Nonempty A
hA' : A ≠ ⊤
a b : α
h : a ≠ b
B : Set α := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
hyp : Set.Subsingleton (⋂ k, ⋂ (_ : a ∈ k • A), k • A)
⊢ B = {a}

case inr
M : Type u_1
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type ?u.94224
β : Type ?u.94227
inst✝¹ : Group N
inst✝ : MulAction N β
hpGX : IsPreprimitive M α
A : Set α
hfA : Set.Finite A
hA : Set.Nonempty A
hA' : A ≠ ⊤
a b : α
h : a ≠ b
B : Set α := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
hyp : ⋂ k, ⋂ (_ : a ∈ k • A), k • A = ⊤
⊢ B = {a}
Theorem: Rudio
Proof state before:
M : Type u_1
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type ?u.94224
β : Type ?u.94227
inst✝¹ : Group N
inst✝ : MulAction N β
hpGX : IsPreprimitive M α
A : Set α
hfA : Set.Finite A
hA : Set.Nonempty A
hA' : A ≠ ⊤
a b : α
h : a ≠ b
B : Set α := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
this : b ∉ B
⊢ ∃ g, a ∈ g • A ∧ b ∉ g • A
Tactic:
rw [Set.mem_iInter] at this
Proof state after:
M : Type u_1
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type ?u.94224
β : Type ?u.94227
inst✝¹ : Group N
inst✝ : MulAction N β
hpGX : IsPreprimitive M α
A : Set α
hfA : Set.Finite A
hA : Set.Nonempty A
hA' : A ≠ ⊤
a b : α
h : a ≠ b
B : Set α := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
this : ¬∀ (i : M), b ∈ ⋂ (_ : a ∈ i • A), i • A
⊢ ∃ g, a ∈ g • A ∧ b ∉ g • A
Theorem: Rudio
Proof state before:
M : Type u_1
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type ?u.94224
β : Type ?u.94227
inst✝¹ : Group N
inst✝ : MulAction N β
hpGX : IsPreprimitive M α
A : Set α
hfA : Set.Finite A
hA : Set.Nonempty A
hA' : A ≠ ⊤
a b : α
h : a ≠ b
B : Set α := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
this : ¬∀ (i : M), b ∈ ⋂ (_ : a ∈ i • A), i • A
⊢ ∃ g, a ∈ g • A ∧ b ∉ g • A
Tactic:
simpa only [Set.mem_iInter, not_forall, exists_prop] using this
Proof state after:
no goals
Theorem: Rudio
Proof state before:
M : Type u_1
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type ?u.94224
β : Type ?u.94227
inst✝¹ : Group N
inst✝ : MulAction N β
hpGX : IsPreprimitive M α
A : Set α
hfA : Set.Finite A
hA : Set.Nonempty A
hA' : A ≠ ⊤
a b : α
h : a ≠ b
B : Set α := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
this : B = {a}
⊢ b ∉ B
Tactic:
rw [this]
Proof state after:
M : Type u_1
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type ?u.94224
β : Type ?u.94227
inst✝¹ : Group N
inst✝ : MulAction N β
hpGX : IsPreprimitive M α
A : Set α
hfA : Set.Finite A
hA : Set.Nonempty A
hA' : A ≠ ⊤
a b : α
h : a ≠ b
B : Set α := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
this : B = {a}
⊢ b ∉ {a}
Theorem: Rudio
Proof state before:
M : Type u_1
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type ?u.94224
β : Type ?u.94227
inst✝¹ : Group N
inst✝ : MulAction N β
hpGX : IsPreprimitive M α
A : Set α
hfA : Set.Finite A
hA : Set.Nonempty A
hA' : A ≠ ⊤
a b : α
h : a ≠ b
B : Set α := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
this : B = {a}
⊢ b ∉ {a}
Tactic:
rw [Set.mem_singleton_iff]
Proof state after:
M : Type u_1
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type ?u.94224
β : Type ?u.94227
inst✝¹ : Group N
inst✝ : MulAction N β
hpGX : IsPreprimitive M α
A : Set α
hfA : Set.Finite A
hA : Set.Nonempty A
hA' : A ≠ ⊤
a b : α
h : a ≠ b
B : Set α := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
this : B = {a}
⊢ ¬b = a
Theorem: Rudio
Proof state before:
M : Type u_1
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type ?u.94224
β : Type ?u.94227
inst✝¹ : Group N
inst✝ : MulAction N β
hpGX : IsPreprimitive M α
A : Set α
hfA : Set.Finite A
hA : Set.Nonempty A
hA' : A ≠ ⊤
a b : α
h : a ≠ b
B : Set α := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
this : B = {a}
⊢ ¬b = a
Tactic:
exact Ne.symm h
Proof state after:
no goals
Theorem: Rudio
Proof state before:
case inl
M : Type u_1
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type ?u.94224
β : Type ?u.94227
inst✝¹ : Group N
inst✝ : MulAction N β
hpGX : IsPreprimitive M α
A : Set α
hfA : Set.Finite A
hA : Set.Nonempty A
hA' : A ≠ ⊤
a b : α
h : a ≠ b
B : Set α := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
hyp : Set.Subsingleton (⋂ k, ⋂ (_ : a ∈ k • A), k • A)
⊢ B = {a}
Tactic:
apply Set.Subsingleton.eq_singleton_of_mem hyp
Proof state after:
case inl
M : Type u_1
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type ?u.94224
β : Type ?u.94227
inst✝¹ : Group N
inst✝ : MulAction N β
hpGX : IsPreprimitive M α
A : Set α
hfA : Set.Finite A
hA : Set.Nonempty A
hA' : A ≠ ⊤
a b : α
h : a ≠ b
B : Set α := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
hyp : Set.Subsingleton (⋂ k, ⋂ (_ : a ∈ k • A), k • A)
⊢ a ∈ ⋂ k, ⋂ (_ : a ∈ k • A), k • A
Theorem: Rudio
Proof state before:
case inl
M : Type u_1
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type ?u.94224
β : Type ?u.94227
inst✝¹ : Group N
inst✝ : MulAction N β
hpGX : IsPreprimitive M α
A : Set α
hfA : Set.Finite A
hA : Set.Nonempty A
hA' : A ≠ ⊤
a b : α
h : a ≠ b
B : Set α := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
hyp : Set.Subsingleton (⋂ k, ⋂ (_ : a ∈ k • A), k • A)
⊢ a ∈ ⋂ k, ⋂ (_ : a ∈ k • A), k • A
Tactic:
rw [Set.mem_iInter]
Proof state after:
case inl
M : Type u_1
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type ?u.94224
β : Type ?u.94227
inst✝¹ : Group N
inst✝ : MulAction N β
hpGX : IsPreprimitive M α
A : Set α
hfA : Set.Finite A
hA : Set.Nonempty A
hA' : A ≠ ⊤
a b : α
h : a ≠ b
B : Set α := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
hyp : Set.Subsingleton (⋂ k, ⋂ (_ : a ∈ k • A), k • A)
⊢ ∀ (i : M), a ∈ ⋂ (_ : a ∈ i • A), i • A
Theorem: Rudio
Proof state before:
case inl
M : Type u_1
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type ?u.94224
β : Type ?u.94227
inst✝¹ : Group N
inst✝ : MulAction N β
hpGX : IsPreprimitive M α
A : Set α
hfA : Set.Finite A
hA : Set.Nonempty A
hA' : A ≠ ⊤
a b : α
h : a ≠ b
B : Set α := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
hyp : Set.Subsingleton (⋂ k, ⋂ (_ : a ∈ k • A), k • A)
⊢ ∀ (i : M), a ∈ ⋂ (_ : a ∈ i • A), i • A
Tactic:
intro g
Proof state after:
case inl
M : Type u_1
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type ?u.94224
β : Type ?u.94227
inst✝¹ : Group N
inst✝ : MulAction N β
hpGX : IsPreprimitive M α
A : Set α
hfA : Set.Finite A
hA : Set.Nonempty A
hA' : A ≠ ⊤
a b : α
h : a ≠ b
B : Set α := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
hyp : Set.Subsingleton (⋂ k, ⋂ (_ : a ∈ k • A), k • A)
g : M
⊢ a ∈ ⋂ (_ : a ∈ g • A), g • A