internlm/Lean-Github huggingface dataset:
Theorem: isTrivialBlock_of_surjective_map
Proof state before:
M : Type u_4
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type u_3
β : Type u_1
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Surjective ⇑f
B : Set α
hB : IsTrivialBlock B
⊢ IsTrivialBlock (⇑f '' B)
Tactic:
cases' hB with hB hB
Proof state after:
case inl
M : Type u_4
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type u_3
β : Type u_1
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Surjective ⇑f
B : Set α
hB : Set.Subsingleton B
⊢ IsTrivialBlock (⇑f '' B)

case inr
M : Type u_4
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type u_3
β : Type u_1
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Surjective ⇑f
B : Set α
hB : B = ⊤
⊢ IsTrivialBlock (⇑f '' B)
Theorem: isTrivialBlock_of_surjective_map
Proof state before:
case inl
M : Type u_4
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type u_3
β : Type u_1
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Surjective ⇑f
B : Set α
hB : Set.Subsingleton B
⊢ IsTrivialBlock (⇑f '' B)
Tactic:
apply Or.intro_left
Proof state after:
case inl.h
M : Type u_4
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type u_3
β : Type u_1
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Surjective ⇑f
B : Set α
hB : Set.Subsingleton B
⊢ Set.Subsingleton (⇑f '' B)
Theorem: isTrivialBlock_of_surjective_map
Proof state before:
case inl.h
M : Type u_4
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type u_3
β : Type u_1
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Surjective ⇑f
B : Set α
hB : Set.Subsingleton B
⊢ Set.Subsingleton (⇑f '' B)
Tactic:
apply Set.Subsingleton.image hB
Proof state after:
no goals
Theorem: isTrivialBlock_of_surjective_map
Proof state before:
case inr
M : Type u_4
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type u_3
β : Type u_1
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Surjective ⇑f
B : Set α
hB : B = ⊤
⊢ IsTrivialBlock (⇑f '' B)
Tactic:
apply Or.intro_right
Proof state after:
case inr.h
M : Type u_4
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type u_3
β : Type u_1
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Surjective ⇑f
B : Set α
hB : B = ⊤
⊢ ⇑f '' B = ⊤
Theorem: isTrivialBlock_of_surjective_map
Proof state before:
case inr.h
M : Type u_4
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type u_3
β : Type u_1
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Surjective ⇑f
B : Set α
hB : B = ⊤
⊢ ⇑f '' B = ⊤
Tactic:
rw [hB]
Proof state after:
case inr.h
M : Type u_4
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type u_3
β : Type u_1
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Surjective ⇑f
B : Set α
hB : B = ⊤
⊢ ⇑f '' ⊤ = ⊤
Theorem: isTrivialBlock_of_surjective_map
Proof state before:
case inr.h
M : Type u_4
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type u_3
β : Type u_1
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Surjective ⇑f
B : Set α
hB : B = ⊤
⊢ ⇑f '' ⊤ = ⊤
Tactic:
simp only [Set.top_eq_univ, Set.image_univ, Set.range_iff_surjective]
Proof state after:
case inr.h
M : Type u_4
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type u_3
β : Type u_1
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Surjective ⇑f
B : Set α
hB : B = ⊤
⊢ Function.Surjective ⇑f
Theorem: isTrivialBlock_of_surjective_map
Proof state before:
case inr.h
M : Type u_4
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type u_3
β : Type u_1
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Surjective ⇑f
B : Set α
hB : B = ⊤
⊢ Function.Surjective ⇑f
Tactic:
exact hf
Proof state after:
no goals
Theorem: isTrivialBlock_of_injective_map
Proof state before:
M : Type u_4
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type u_3
β : Type u_1
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Injective ⇑f
B : Set β
hB : IsTrivialBlock B
⊢ IsTrivialBlock (⇑f ⁻¹' B)
Tactic:
cases' hB with hB hB
Proof state after:
case inl
M : Type u_4
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type u_3
β : Type u_1
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Injective ⇑f
B : Set β
hB : Set.Subsingleton B
⊢ IsTrivialBlock (⇑f ⁻¹' B)

case inr
M : Type u_4
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type u_3
β : Type u_1
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Injective ⇑f
B : Set β
hB : B = ⊤
⊢ IsTrivialBlock (⇑f ⁻¹' B)
Theorem: isTrivialBlock_of_injective_map
Proof state before:
case inl
M : Type u_4
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type u_3
β : Type u_1
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Injective ⇑f
B : Set β
hB : Set.Subsingleton B
⊢ IsTrivialBlock (⇑f ⁻¹' B)

case inr
M : Type u_4
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type u_3
β : Type u_1
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Injective ⇑f
B : Set β
hB : B = ⊤
⊢ IsTrivialBlock (⇑f ⁻¹' B)
Tactic:
apply Or.intro_left
Proof state after:
case inl.h
M : Type u_4
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type u_3
β : Type u_1
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Injective ⇑f
B : Set β
hB : Set.Subsingleton B
⊢ Set.Subsingleton (⇑f ⁻¹' B)

case inr
M : Type u_4
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type u_3
β : Type u_1
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Injective ⇑f
B : Set β
hB : B = ⊤
⊢ IsTrivialBlock (⇑f ⁻¹' B)
Theorem: isTrivialBlock_of_injective_map
Proof state before:
case inl.h
M : Type u_4
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type u_3
β : Type u_1
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Injective ⇑f
B : Set β
hB : Set.Subsingleton B
⊢ Set.Subsingleton (⇑f ⁻¹' B)

case inr
M : Type u_4
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type u_3
β : Type u_1
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Injective ⇑f
B : Set β
hB : B = ⊤
⊢ IsTrivialBlock (⇑f ⁻¹' B)
Tactic:
exact Set.Subsingleton.preimage hB hf
Proof state after:
case inr
M : Type u_4
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type u_3
β : Type u_1
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Injective ⇑f
B : Set β
hB : B = ⊤
⊢ IsTrivialBlock (⇑f ⁻¹' B)
Theorem: isTrivialBlock_of_injective_map
Proof state before:
case inr
M : Type u_4
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type u_3
β : Type u_1
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Injective ⇑f
B : Set β
hB : B = ⊤
⊢ IsTrivialBlock (⇑f ⁻¹' B)
Tactic:
apply Or.intro_right
Proof state after:
case inr.h
M : Type u_4
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type u_3
β : Type u_1
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Injective ⇑f
B : Set β
hB : B = ⊤
⊢ ⇑f ⁻¹' B = ⊤
Theorem: isTrivialBlock_of_injective_map
Proof state before:
case inr.h
M : Type u_4
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type u_3
β : Type u_1
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Injective ⇑f
B : Set β
hB : B = ⊤
⊢ ⇑f ⁻¹' B = ⊤
Tactic:
simp only [hB, Set.top_eq_univ]
Proof state after:
case inr.h
M : Type u_4
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type u_3
β : Type u_1
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Injective ⇑f
B : Set β
hB : B = ⊤
⊢ ⇑f ⁻¹' Set.univ = Set.univ
Theorem: isTrivialBlock_of_injective_map
Proof state before:
case inr.h
M : Type u_4
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type u_3
β : Type u_1
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Injective ⇑f
B : Set β
hB : B = ⊤
⊢ ⇑f ⁻¹' Set.univ = Set.univ
Tactic:
apply Set.preimage_univ
Proof state after:
no goals
Theorem: isPreprimitive_of_surjective_map
Proof state before:
M : Type u_4
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type u_3
β : Type u_1
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Surjective ⇑f
h : IsPreprimitive M α
⊢ IsPreprimitive N β
Tactic:
have : IsPretransitive N β := isPretransitive.of_surjective_map hf h.toIsPretransitive
Proof state after:
M : Type u_4
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type u_3
β : Type u_1
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Surjective ⇑f
h : IsPreprimitive M α
this : IsPretransitive N β
⊢ IsPreprimitive N β
Theorem: isPreprimitive_of_surjective_map
Proof state before:
M : Type u_4
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type u_3
β : Type u_1
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Surjective ⇑f
h : IsPreprimitive M α
this : IsPretransitive N β
⊢ IsPreprimitive N β
Tactic:
apply IsPreprimitive.mk
Proof state after:
case has_trivial_blocks'
M : Type u_4
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type u_3
β : Type u_1
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Surjective ⇑f
h : IsPreprimitive M α
this : IsPretransitive N β
⊢ ∀ {B : Set β}, IsBlock N B → IsTrivialBlock B
Theorem: isPreprimitive_of_surjective_map
Proof state before:
case has_trivial_blocks'
M : Type u_4
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type u_3
β : Type u_1
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Surjective ⇑f
h : IsPreprimitive M α
this : IsPretransitive N β
⊢ ∀ {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_2
inst✝² : MulAction M α
N : Type u_3
β : Type u_1
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Surjective ⇑f
h : IsPreprimitive M α
this : IsPretransitive N β
B : Set β
hB : IsBlock N B
⊢ IsTrivialBlock B
Theorem: isPreprimitive_of_surjective_map
Proof state before:
case has_trivial_blocks'
M : Type u_4
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type u_3
β : Type u_1
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Surjective ⇑f
h : IsPreprimitive M α
this : IsPretransitive N β
B : Set β
hB : IsBlock N B
⊢ IsTrivialBlock B
Tactic:
rw [← Set.image_preimage_eq B hf]
Proof state after:
case has_trivial_blocks'
M : Type u_4
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type u_3
β : Type u_1
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Surjective ⇑f
h : IsPreprimitive M α
this : IsPretransitive N β
B : Set β
hB : IsBlock N B
⊢ IsTrivialBlock (⇑f '' (⇑f ⁻¹' B))
Theorem: isPreprimitive_of_surjective_map
Proof state before:
case has_trivial_blocks'
M : Type u_4
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type u_3
β : Type u_1
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Surjective ⇑f
h : IsPreprimitive M α
this : IsPretransitive N β
B : Set β
hB : IsBlock N B
⊢ IsTrivialBlock (⇑f '' (⇑f ⁻¹' B))
Tactic:
apply isTrivialBlock_of_surjective_map hf
Proof state after:
case has_trivial_blocks'
M : Type u_4
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type u_3
β : Type u_1
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Surjective ⇑f
h : IsPreprimitive M α
this : IsPretransitive N β
B : Set β
hB : IsBlock N B
⊢ IsTrivialBlock (⇑f ⁻¹' B)
Theorem: isPreprimitive_of_surjective_map
Proof state before:
case has_trivial_blocks'
M : Type u_4
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type u_3
β : Type u_1
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Surjective ⇑f
h : IsPreprimitive M α
this : IsPretransitive N β
B : Set β
hB : IsBlock N B
⊢ IsTrivialBlock (⇑f ⁻¹' B)
Tactic:
apply h.has_trivial_blocks
Proof state after:
case has_trivial_blocks'
M : Type u_4
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type u_3
β : Type u_1
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Surjective ⇑f
h : IsPreprimitive M α
this : IsPretransitive N β
B : Set β
hB : IsBlock N B
⊢ IsBlock M (⇑f ⁻¹' B)
Theorem: isPreprimitive_of_surjective_map
Proof state before:
case has_trivial_blocks'
M : Type u_4
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type u_3
β : Type u_1
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Surjective ⇑f
h : IsPreprimitive M α
this : IsPretransitive N β
B : Set β
hB : IsBlock N B
⊢ IsBlock M (⇑f ⁻¹' B)
Tactic:
apply IsBlock_preimage
Proof state after:
case has_trivial_blocks'.hB
M : Type u_4
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type u_3
β : Type u_1
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Surjective ⇑f
h : IsPreprimitive M α
this : IsPretransitive N β
B : Set β
hB : IsBlock N B
⊢ IsBlock N B
Theorem: isPreprimitive_of_surjective_map
Proof state before:
case has_trivial_blocks'.hB
M : Type u_4
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type u_3
β : Type u_1
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Surjective ⇑f
h : IsPreprimitive M α
this : IsPretransitive N β
B : Set β
hB : IsBlock N B
⊢ IsBlock N B
Tactic:
exact hB
Proof state after:
no goals
Theorem: isPreprimitive_of_bijective_map_iff
Proof state before:
M : Type u_4
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type u_3
β : Type u_1
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hφ : Function.Surjective φ
hf : Function.Bijective ⇑f
⊢ IsPreprimitive M α ↔ IsPreprimitive N β
Tactic:
constructor
Proof state after:
case mp
M : Type u_4
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type u_3
β : Type u_1
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hφ : Function.Surjective φ
hf : Function.Bijective ⇑f
⊢ IsPreprimitive M α → IsPreprimitive N β

case mpr
M : Type u_4
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type u_3
β : Type u_1
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hφ : Function.Surjective φ
hf : Function.Bijective ⇑f
⊢ IsPreprimitive N β → IsPreprimitive M α
Theorem: isPreprimitive_of_bijective_map_iff
Proof state before:
case mp
M : Type u_4
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type u_3
β : Type u_1
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hφ : Function.Surjective φ
hf : Function.Bijective ⇑f
⊢ IsPreprimitive M α → IsPreprimitive N β

case mpr
M : Type u_4
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type u_3
β : Type u_1
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hφ : Function.Surjective φ
hf : Function.Bijective ⇑f
⊢ IsPreprimitive N β → IsPreprimitive M α
Tactic:
apply isPreprimitive_of_surjective_map hf.surjective
Proof state after:
case mpr
M : Type u_4
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type u_3
β : Type u_1
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hφ : Function.Surjective φ
hf : Function.Bijective ⇑f
⊢ IsPreprimitive N β → IsPreprimitive M α
Theorem: isPreprimitive_of_bijective_map_iff
Proof state before:
case mpr
M : Type u_4
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type u_3
β : Type u_1
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hφ : Function.Surjective φ
hf : Function.Bijective ⇑f
⊢ IsPreprimitive N β → IsPreprimitive M α
Tactic:
intro hN
Proof state after:
case mpr
M : Type u_4
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type u_3
β : Type u_1
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hφ : Function.Surjective φ
hf : Function.Bijective ⇑f
hN : IsPreprimitive N β
⊢ IsPreprimitive M α
Theorem: isPreprimitive_of_bijective_map_iff
Proof state before:
case mpr
M : Type u_4
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type u_3
β : Type u_1
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hφ : Function.Surjective φ
hf : Function.Bijective ⇑f
hN : IsPreprimitive N β
⊢ IsPreprimitive M α
Tactic:
haveI := (isPretransitive.of_bijective_map_iff hφ hf).mpr hN.toIsPretransitive
Proof state after:
case mpr
M : Type u_4
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type u_3
β : Type u_1
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hφ : Function.Surjective φ
hf : Function.Bijective ⇑f
hN : IsPreprimitive N β
this : IsPretransitive M α
⊢ IsPreprimitive M α
Theorem: isPreprimitive_of_bijective_map_iff
Proof state before:
case mpr
M : Type u_4
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type u_3
β : Type u_1
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hφ : Function.Surjective φ
hf : Function.Bijective ⇑f
hN : IsPreprimitive N β
this : IsPretransitive M α
⊢ IsPreprimitive M α
Tactic:
apply IsPreprimitive.mk
Proof state after:
case mpr.has_trivial_blocks'
M : Type u_4
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type u_3
β : Type u_1
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hφ : Function.Surjective φ
hf : Function.Bijective ⇑f
hN : IsPreprimitive N β
this : IsPretransitive M α
⊢ ∀ {B : Set α}, IsBlock M B → IsTrivialBlock B
Theorem: isPreprimitive_of_bijective_map_iff
Proof state before:
case mpr.has_trivial_blocks'
M : Type u_4
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type u_3
β : Type u_1
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hφ : Function.Surjective φ
hf : Function.Bijective ⇑f
hN : IsPreprimitive N β
this : IsPretransitive M α
⊢ ∀ {B : Set α}, IsBlock M B → IsTrivialBlock B
Tactic:
intro B hB
Proof state after:
case mpr.has_trivial_blocks'
M : Type u_4
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type u_3
β : Type u_1
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hφ : Function.Surjective φ
hf : Function.Bijective ⇑f
hN : IsPreprimitive N β
this : IsPretransitive M α
B : Set α
hB : IsBlock M B
⊢ IsTrivialBlock B
Theorem: isPreprimitive_of_bijective_map_iff
Proof state before:
case mpr.has_trivial_blocks'
M : Type u_4
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type u_3
β : Type u_1
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hφ : Function.Surjective φ
hf : Function.Bijective ⇑f
hN : IsPreprimitive N β
this : IsPretransitive M α
B : Set α
hB : IsBlock M B
⊢ IsTrivialBlock B
Tactic:
rw [← Set.preimage_image_eq B hf.injective]
Proof state after:
case mpr.has_trivial_blocks'
M : Type u_4
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type u_3
β : Type u_1
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hφ : Function.Surjective φ
hf : Function.Bijective ⇑f
hN : IsPreprimitive N β
this : IsPretransitive M α
B : Set α
hB : IsBlock M B
⊢ IsTrivialBlock (⇑f ⁻¹' (⇑f '' B))
Theorem: isPreprimitive_of_bijective_map_iff
Proof state before:
case mpr.has_trivial_blocks'
M : Type u_4
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type u_3
β : Type u_1
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hφ : Function.Surjective φ
hf : Function.Bijective ⇑f
hN : IsPreprimitive N β
this : IsPretransitive M α
B : Set α
hB : IsBlock M B
⊢ IsTrivialBlock (⇑f ⁻¹' (⇑f '' B))
Tactic:
apply isTrivialBlock_of_injective_map hf.injective
Proof state after:
case mpr.has_trivial_blocks'
M : Type u_4
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type u_3
β : Type u_1
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hφ : Function.Surjective φ
hf : Function.Bijective ⇑f
hN : IsPreprimitive N β
this : IsPretransitive M α
B : Set α
hB : IsBlock M B
⊢ IsTrivialBlock (⇑f '' B)
Theorem: isPreprimitive_of_bijective_map_iff
Proof state before:
case mpr.has_trivial_blocks'
M : Type u_4
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type u_3
β : Type u_1
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hφ : Function.Surjective φ
hf : Function.Bijective ⇑f
hN : IsPreprimitive N β
this : IsPretransitive M α
B : Set α
hB : IsBlock M B
⊢ IsTrivialBlock (⇑f '' B)
Tactic:
apply hN.has_trivial_blocks
Proof state after:
case mpr.has_trivial_blocks'
M : Type u_4
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type u_3
β : Type u_1
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hφ : Function.Surjective φ
hf : Function.Bijective ⇑f
hN : IsPreprimitive N β
this : IsPretransitive M α
B : Set α
hB : IsBlock M B
⊢ IsBlock N (⇑f '' B)
Theorem: isPreprimitive_of_bijective_map_iff
Proof state before:
case mpr.has_trivial_blocks'
M : Type u_4
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type u_3
β : Type u_1
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hφ : Function.Surjective φ
hf : Function.Bijective ⇑f
hN : IsPreprimitive N β
this : IsPretransitive M α
B : Set α
hB : IsBlock M B
⊢ IsBlock N (⇑f '' B)
Tactic:
apply IsBlock_image f hφ hf.injective
Proof state after:
case mpr.has_trivial_blocks'
M : Type u_4
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type u_3
β : Type u_1
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hφ : Function.Surjective φ
hf : Function.Bijective ⇑f
hN : IsPreprimitive N β
this : IsPretransitive M α
B : Set α
hB : IsBlock M B
⊢ IsBlock M B
Theorem: isPreprimitive_of_bijective_map_iff
Proof state before:
case mpr.has_trivial_blocks'
M : Type u_4
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type u_3
β : Type u_1
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hφ : Function.Surjective φ
hf : Function.Bijective ⇑f
hN : IsPreprimitive N β
this : IsPretransitive M α
B : Set α
hB : IsBlock M B
⊢ IsBlock M B
Tactic:
exact hB
Proof state after:
no goals
Theorem: isPreprimitive_of_bijective_map_iff'
Proof state before:
M : Type u_4
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type u_3
β : Type u_1
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hφ : Function.Surjective φ
hf : Function.Bijective ⇑f
⊢ IsPreprimitive M α ↔ IsPreprimitive N β
Tactic:
constructor
Proof state after:
case mp
M : Type u_4
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type u_3
β : Type u_1
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hφ : Function.Surjective φ
hf : Function.Bijective ⇑f
⊢ IsPreprimitive M α → IsPreprimitive N β

case mpr
M : Type u_4
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type u_3
β : Type u_1
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hφ : Function.Surjective φ
hf : Function.Bijective ⇑f
⊢ IsPreprimitive N β → IsPreprimitive M α
Theorem: isPreprimitive_of_bijective_map_iff'
Proof state before:
case mp
M : Type u_4
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type u_3
β : Type u_1
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hφ : Function.Surjective φ
hf : Function.Bijective ⇑f
⊢ IsPreprimitive M α → IsPreprimitive N β

case mpr
M : Type u_4
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type u_3
β : Type u_1
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hφ : Function.Surjective φ
hf : Function.Bijective ⇑f
⊢ IsPreprimitive N β → IsPreprimitive M α
Tactic:
apply isPreprimitive_of_surjective_map hf.surjective
Proof state after:
case mpr
M : Type u_4
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type u_3
β : Type u_1
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hφ : Function.Surjective φ
hf : Function.Bijective ⇑f
⊢ IsPreprimitive N β → IsPreprimitive M α