Theorem: isPreprimitive_of_surjective_map (Jordan/Primitive.lean)

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

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

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

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

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

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

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

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