Theorem: isPreprimitive_of_bijective_map_iff (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 : α →ₑ[φ] β
hφ : Function.Surjective φ
hf : Function.Bijective ⇑f
⊢ IsPreprimitive M α ↔ IsPreprimitive N β
Tactic:
constructor
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 α

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

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

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

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

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

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

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

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

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

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