-- Mathlib/GroupTheory/GroupAction/Primitive.lean
theorem isPreprimitive_congr (hφ : Function.Surjective φ) (hf : Function.Bijective f) :
    IsPreprimitive M α ↔ IsPreprimitive N β

Proof state:
case mpr
M : Type u_3
inst✝³ : Group M
α : Type u_4
inst✝² : MulAction M α
N : Type u_5
β : Type u_6
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M →* N
f : α →ₑ[⇑φ] β
hφ : Function.Surjective ⇑φ
hf : Function.Bijective ⇑f
a✝ : IsPreprimitive N β
this : IsPretransitive M α
⊢ IsPreprimitive M α

Tactic:
exact {
  isTrivialBlock_of_isBlock {B} hB := by
    rw [← Set.preimage_image_eq B hf.injective]
    exact IsTrivialBlock.preimage hf.injective
      (isTrivialBlock_of_isBlock (hB.image f hφ hf.injective)) }

Result:
no goals

Proof state:
case mp
M : Type u_3
inst✝³ : Group M
α : Type u_4
inst✝² : MulAction M α
N : Type u_5
β : Type u_6
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M →* N
f : α →ₑ[⇑φ] β
hφ : Function.Surjective ⇑φ
hf : Function.Bijective ⇑f
⊢ IsPreprimitive M α → IsPreprimitive N β

Tactic:
intro _

Result:
case mp
M : Type u_3
inst✝³ : Group M
α : Type u_4
inst✝² : MulAction M α
N : Type u_5
β : Type u_6
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M →* N
f : α →ₑ[⇑φ] β
hφ : Function.Surjective ⇑φ
hf : Function.Bijective ⇑f
a✝ : IsPreprimitive M α
⊢ IsPreprimitive N β

Proof state:
M : Type u_3
inst✝³ : Group M
α : Type u_4
inst✝² : MulAction M α
N : Type u_5
β : Type u_6
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M →* N
f : α →ₑ[⇑φ] β
hφ : Function.Surjective ⇑φ
hf : Function.Bijective ⇑f
a✝ : IsPreprimitive N β
this : IsPretransitive M α
B : Set α
hB : IsBlock M B
⊢ IsTrivialBlock (⇑f ⁻¹' (⇑f '' B))

Tactic:
exact IsTrivialBlock.preimage hf.injective
  (isTrivialBlock_of_isBlock (hB.image f hφ hf.injective))

Result:
no goals

Proof state:
case mpr
M : Type u_3
inst✝³ : Group M
α : Type u_4
inst✝² : MulAction M α
N : Type u_5
β : Type u_6
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M →* N
f : α →ₑ[⇑φ] β
hφ : Function.Surjective ⇑φ
hf : Function.Bijective ⇑f
a✝ : IsPreprimitive N β
⊢ IsPreprimitive M α

Tactic:
haveI := (isPretransitive_congr hφ hf).mpr toIsPretransitive

Result:
case mpr
M : Type u_3
inst✝³ : Group M
α : Type u_4
inst✝² : MulAction M α
N : Type u_5
β : Type u_6
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M →* N
f : α →ₑ[⇑φ] β
hφ : Function.Surjective ⇑φ
hf : Function.Bijective ⇑f
a✝ : IsPreprimitive N β
this : IsPretransitive M α
⊢ IsPreprimitive M α

Proof state:
M : Type u_3
inst✝³ : Group M
α : Type u_4
inst✝² : MulAction M α
N : Type u_5
β : Type u_6
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M →* N
f : α →ₑ[⇑φ] β
hφ : Function.Surjective ⇑φ
hf : Function.Bijective ⇑f
a✝ : IsPreprimitive N β
this : IsPretransitive M α
B : Set α
hB : IsBlock M B
⊢ IsTrivialBlock B

Tactic:
rw [← Set.preimage_image_eq B hf.injective]

Result:
M : Type u_3
inst✝³ : Group M
α : Type u_4
inst✝² : MulAction M α
N : Type u_5
β : Type u_6
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M →* N
f : α →ₑ[⇑φ] β
hφ : Function.Surjective ⇑φ
hf : Function.Bijective ⇑f
a✝ : IsPreprimitive N β
this : IsPretransitive M α
B : Set α
hB : IsBlock M B
⊢ IsTrivialBlock (⇑f ⁻¹' (⇑f '' B))

Proof state:
case mpr
M : Type u_3
inst✝³ : Group M
α : Type u_4
inst✝² : MulAction M α
N : Type u_5
β : Type u_6
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M →* N
f : α →ₑ[⇑φ] β
hφ : Function.Surjective ⇑φ
hf : Function.Bijective ⇑f
⊢ IsPreprimitive N β → IsPreprimitive M α

Tactic:
intro _

Result:
case mpr
M : Type u_3
inst✝³ : Group M
α : Type u_4
inst✝² : MulAction M α
N : Type u_5
β : Type u_6
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M →* N
f : α →ₑ[⇑φ] β
hφ : Function.Surjective ⇑φ
hf : Function.Bijective ⇑f
a✝ : IsPreprimitive N β
⊢ IsPreprimitive M α

Proof state:
case mp
M : Type u_3
inst✝³ : Group M
α : Type u_4
inst✝² : MulAction M α
N : Type u_5
β : Type u_6
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M →* N
f : α →ₑ[⇑φ] β
hφ : Function.Surjective ⇑φ
hf : Function.Bijective ⇑f
a✝ : IsPreprimitive M α
⊢ IsPreprimitive N β

Tactic:
apply IsPreprimitive.of_surjective hf.surjective

Result:
no goals

Proof state:
M : Type u_3
inst✝³ : Group M
α : Type u_4
inst✝² : MulAction M α
N : Type u_5
β : Type u_6
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M →* N
f : α →ₑ[⇑φ] β
hφ : Function.Surjective ⇑φ
hf : Function.Bijective ⇑f
⊢ IsPreprimitive M α ↔ IsPreprimitive N β

Tactic:
constructor

Result:
case mp
M : Type u_3
inst✝³ : Group M
α : Type u_4
inst✝² : MulAction M α
N : Type u_5
β : Type u_6
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_3
inst✝³ : Group M
α : Type u_4
inst✝² : MulAction M α
N : Type u_5
β : Type u_6
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M →* N
f : α →ₑ[⇑φ] β
hφ : Function.Surjective ⇑φ
hf : Function.Bijective ⇑f
⊢ IsPreprimitive N β → IsPreprimitive M α