Theorem: MulAction.isMultiplyPreprimitive_of_bijective_map (Jordan/MultiplePrimitivity.lean)

State before:
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
h : IsMultiplyPreprimitive M α n
⊢ IsMultiplyPreprimitive N β n
Tactic:
constructor
State after:
case left
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
h : IsMultiplyPreprimitive M α n
⊢ IsMultiplyPretransitive N β n

case right
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
h : IsMultiplyPreprimitive M α n
⊢ ∀ (s : Set β), Set.encard s + 1 = ↑n → IsPreprimitive ↥(fixingSubgroup N s) ↥(SubMulAction.ofFixingSubgroup N s)

State before:
case left
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
h : IsMultiplyPreprimitive M α n
⊢ IsMultiplyPretransitive N β n

case right
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
h : IsMultiplyPreprimitive M α n
⊢ ∀ (s : Set β), Set.encard s + 1 = ↑n → IsPreprimitive ↥(fixingSubgroup N s) ↥(SubMulAction.ofFixingSubgroup N s)
Tactic:
apply isMultiplyPretransitive_of_surjective_map hf.surjective h.left
State after:
case right
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
h : IsMultiplyPreprimitive M α n
⊢ ∀ (s : Set β), Set.encard s + 1 = ↑n → IsPreprimitive ↥(fixingSubgroup N s) ↥(SubMulAction.ofFixingSubgroup N s)

State before:
case right
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
h : IsMultiplyPreprimitive M α n
⊢ ∀ (s : Set β), Set.encard s + 1 = ↑n → IsPreprimitive ↥(fixingSubgroup N s) ↥(SubMulAction.ofFixingSubgroup N s)
Tactic:
intro t ht
State after:
case right
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
h : IsMultiplyPreprimitive M α n
t : Set β
ht : Set.encard t + 1 = ↑n
⊢ IsPreprimitive ↥(fixingSubgroup N t) ↥(SubMulAction.ofFixingSubgroup N t)

State before:
case right
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
h : IsMultiplyPreprimitive M α n
t : Set β
ht : Set.encard t + 1 = ↑n
⊢ IsPreprimitive ↥(fixingSubgroup N t) ↥(SubMulAction.ofFixingSubgroup N t)
Tactic:
let s := f ⁻¹' t
State after:
case right
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
h : IsMultiplyPreprimitive M α n
t : Set β
ht : Set.encard t + 1 = ↑n
s : Set α := ⇑f ⁻¹' t
⊢ IsPreprimitive ↥(fixingSubgroup N t) ↥(SubMulAction.ofFixingSubgroup N t)

State before:
case right
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
h : IsMultiplyPreprimitive M α n
t : Set β
ht : Set.encard t + 1 = ↑n
s : Set α := ⇑f ⁻¹' t
⊢ IsPreprimitive ↥(fixingSubgroup N t) ↥(SubMulAction.ofFixingSubgroup N t)
Tactic:
have hs' : f '' s = t := Set.image_preimage_eq t hf.surjective
State after:
case right
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
h : IsMultiplyPreprimitive M α n
t : Set β
ht : Set.encard t + 1 = ↑n
s : Set α := ⇑f ⁻¹' t
hs' : ⇑f '' s = t
⊢ IsPreprimitive ↥(fixingSubgroup N t) ↥(SubMulAction.ofFixingSubgroup N t)

State before:
case right
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
h : IsMultiplyPreprimitive M α n
t : Set β
ht : Set.encard t + 1 = ↑n
s : Set α := ⇑f ⁻¹' t
hs' : ⇑f '' s = t
⊢ IsPreprimitive ↥(fixingSubgroup N t) ↥(SubMulAction.ofFixingSubgroup N t)
Tactic:
let φ' : fixingSubgroup M s → fixingSubgroup N t := fun ⟨m, hm⟩ =>
  ⟨φ m, fun ⟨y, hy⟩ => by
    rw [← hs', Set.mem_image_iff_bex] at hy
    obtain ⟨x, hx, hx'⟩ := hy
    simp only [Subtype.coe_mk]
    rw [← hx', ← map_smulₛₗ]
    apply congr_arg
    rw [mem_fixingSubgroup_iff] at hm
    exact hm x hx⟩
State after:
case right
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
h : IsMultiplyPreprimitive M α n
t : Set β
ht : Set.encard t + 1 = ↑n
s : Set α := ⇑f ⁻¹' t
hs' : ⇑f '' s = t
φ' : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun x =>
    match x with
    | { val := m, property := hm } => { val := φ m, property := ⋯ }
⊢ IsPreprimitive ↥(fixingSubgroup N t) ↥(SubMulAction.ofFixingSubgroup N t)

State before:
case right
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
h : IsMultiplyPreprimitive M α n
t : Set β
ht : Set.encard t + 1 = ↑n
s : Set α := ⇑f ⁻¹' t
hs' : ⇑f '' s = t
φ' : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun x =>
    match x with
    | { val := m, property := hm } => { val := φ m, property := ⋯ }
⊢ IsPreprimitive ↥(fixingSubgroup N t) ↥(SubMulAction.ofFixingSubgroup N t)
Tactic:
let f' : SubMulAction.ofFixingSubgroup M s →ₑ[φ'] SubMulAction.ofFixingSubgroup N t :=
  { toFun := fun ⟨x, hx⟩ => ⟨f.toFun x, fun h => hx (Set.mem_preimage.mp h)⟩
    map_smul' := fun ⟨m, hm⟩ ⟨x, hx⟩ =>
      by
      rw [← SetLike.coe_eq_coe]
      exact f.map_smul' m x }
State after:
case right
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
h : IsMultiplyPreprimitive M α n
t : Set β
ht : Set.encard t + 1 = ↑n
s : Set α := ⇑f ⁻¹' t
hs' : ⇑f '' s = t
φ' : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun x =>
    match x with
    | { val := m, property := hm } => { val := φ m, property := ⋯ }
f' : ↥(SubMulAction.ofFixingSubgroup M s) →ₑ[φ'] ↥(SubMulAction.ofFixingSubgroup N t) :=
  {
    toFun := fun x =>
      match x with
      | { val := x, property := hx } => { val := f.toFun x, property := ⋯ },
    map_smul' := ⋯ }
⊢ IsPreprimitive ↥(fixingSubgroup N t) ↥(SubMulAction.ofFixingSubgroup N t)

State before:
case right
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
h : IsMultiplyPreprimitive M α n
t : Set β
ht : Set.encard t + 1 = ↑n
s : Set α := ⇑f ⁻¹' t
hs' : ⇑f '' s = t
φ' : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun x =>
    match x with
    | { val := m, property := hm } => { val := φ m, property := ⋯ }
f' : ↥(SubMulAction.ofFixingSubgroup M s) →ₑ[φ'] ↥(SubMulAction.ofFixingSubgroup N t) :=
  {
    toFun := fun x =>
      match x with
      | { val := x, property := hx } => { val := f.toFun x, property := ⋯ },
    map_smul' := ⋯ }
hf' : Function.Surjective ⇑f'
⊢ IsPreprimitive ↥(fixingSubgroup N t) ↥(SubMulAction.ofFixingSubgroup N t)
Tactic:
refine isPreprimitive_of_surjective_map hf' (h.right s ?_)
State after:
case right
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
h : IsMultiplyPreprimitive M α n
t : Set β
ht : Set.encard t + 1 = ↑n
s : Set α := ⇑f ⁻¹' t
hs' : ⇑f '' s = t
φ' : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun x =>
    match x with
    | { val := m, property := hm } => { val := φ m, property := ⋯ }
f' : ↥(SubMulAction.ofFixingSubgroup M s) →ₑ[φ'] ↥(SubMulAction.ofFixingSubgroup N t) :=
  {
    toFun := fun x =>
      match x with
      | { val := x, property := hx } => { val := f.toFun x, property := ⋯ },
    map_smul' := ⋯ }
hf' : Function.Surjective ⇑f'
⊢ Set.encard s + 1 = ↑n

State before:
case right
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
h : IsMultiplyPreprimitive M α n
t : Set β
ht : Set.encard t + 1 = ↑n
s : Set α := ⇑f ⁻¹' t
hs' : ⇑f '' s = t
φ' : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun x =>
    match x with
    | { val := m, property := hm } => { val := φ m, property := ⋯ }
f' : ↥(SubMulAction.ofFixingSubgroup M s) →ₑ[φ'] ↥(SubMulAction.ofFixingSubgroup N t) :=
  {
    toFun := fun x =>
      match x with
      | { val := x, property := hx } => { val := f.toFun x, property := ⋯ },
    map_smul' := ⋯ }
hf' : Function.Surjective ⇑f'
⊢ Set.encard s + 1 = ↑n
Tactic:
rw [← ht, ← hs', hf.injective.encard_image]
State after:
no goals

State before:
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
h : IsMultiplyPreprimitive M α n
t : Set β
ht : Set.encard t + 1 = ↑n
s : Set α := ⇑f ⁻¹' t
hs' : ⇑f '' s = t
x✝¹ : ↥(fixingSubgroup M s)
m : M
hm : m ∈ fixingSubgroup M s
x✝ : ↑t
y : β
hy : y ∈ t
⊢ φ m • ↑{ val := y, property := hy } = ↑{ val := y, property := hy }
Tactic:
rw [← hs', Set.mem_image_iff_bex] at hy
State after:
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
h : IsMultiplyPreprimitive M α n
t : Set β
ht : Set.encard t + 1 = ↑n
s : Set α := ⇑f ⁻¹' t
hs' : ⇑f '' s = t
x✝¹ : ↥(fixingSubgroup M s)
m : M
hm : m ∈ fixingSubgroup M s
x✝ : ↑t
y : β
hy✝ : y ∈ t
hy : ∃ x, ∃ (_ : x ∈ s), f x = y
⊢ φ m • ↑{ val := y, property := hy✝ } = ↑{ val := y, property := hy✝ }

State before:
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
h : IsMultiplyPreprimitive M α n
t : Set β
ht : Set.encard t + 1 = ↑n
s : Set α := ⇑f ⁻¹' t
hs' : ⇑f '' s = t
x✝¹ : ↥(fixingSubgroup M s)
m : M
hm : m ∈ fixingSubgroup M s
x✝ : ↑t
y : β
hy✝ : y ∈ t
hy : ∃ x, ∃ (_ : x ∈ s), f x = y
⊢ φ m • ↑{ val := y, property := hy✝ } = ↑{ val := y, property := hy✝ }
Tactic:
obtain ⟨x, hx, hx'⟩ := hy
State after:
case intro.intro
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
h : IsMultiplyPreprimitive M α n
t : Set β
ht : Set.encard t + 1 = ↑n
s : Set α := ⇑f ⁻¹' t
hs' : ⇑f '' s = t
x✝¹ : ↥(fixingSubgroup M s)
m : M
hm : m ∈ fixingSubgroup M s
x✝ : ↑t
y : β
hy : y ∈ t
x : α
hx : x ∈ s
hx' : f x = y
⊢ φ m • ↑{ val := y, property := hy } = ↑{ val := y, property := hy }

State before:
case intro.intro
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
h : IsMultiplyPreprimitive M α n
t : Set β
ht : Set.encard t + 1 = ↑n
s : Set α := ⇑f ⁻¹' t
hs' : ⇑f '' s = t
x✝¹ : ↥(fixingSubgroup M s)
m : M
hm : m ∈ fixingSubgroup M s
x✝ : ↑t
y : β
hy : y ∈ t
x : α
hx : x ∈ s
hx' : f x = y
⊢ φ m • ↑{ val := y, property := hy } = ↑{ val := y, property := hy }
Tactic:
simp only [Subtype.coe_mk]
State after:
case intro.intro
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
h : IsMultiplyPreprimitive M α n
t : Set β
ht : Set.encard t + 1 = ↑n
s : Set α := ⇑f ⁻¹' t
hs' : ⇑f '' s = t
x✝¹ : ↥(fixingSubgroup M s)
m : M
hm : m ∈ fixingSubgroup M s
x✝ : ↑t
y : β
hy : y ∈ t
x : α
hx : x ∈ s
hx' : f x = y
⊢ φ m • y = y

State before:
case intro.intro
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
h : IsMultiplyPreprimitive M α n
t : Set β
ht : Set.encard t + 1 = ↑n
s : Set α := ⇑f ⁻¹' t
hs' : ⇑f '' s = t
x✝¹ : ↥(fixingSubgroup M s)
m : M
hm : m ∈ fixingSubgroup M s
x✝ : ↑t
y : β
hy : y ∈ t
x : α
hx : x ∈ s
hx' : f x = y
⊢ φ m • y = y
Tactic:
rw [← hx', ← map_smulₛₗ]
State after:
case intro.intro
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
h : IsMultiplyPreprimitive M α n
t : Set β
ht : Set.encard t + 1 = ↑n
s : Set α := ⇑f ⁻¹' t
hs' : ⇑f '' s = t
x✝¹ : ↥(fixingSubgroup M s)
m : M
hm : m ∈ fixingSubgroup M s
x✝ : ↑t
y : β
hy : y ∈ t
x : α
hx : x ∈ s
hx' : f x = y
⊢ f (m • x) = f x

State before:
case intro.intro
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
h : IsMultiplyPreprimitive M α n
t : Set β
ht : Set.encard t + 1 = ↑n
s : Set α := ⇑f ⁻¹' t
hs' : ⇑f '' s = t
x✝¹ : ↥(fixingSubgroup M s)
m : M
hm : m ∈ fixingSubgroup M s
x✝ : ↑t
y : β
hy : y ∈ t
x : α
hx : x ∈ s
hx' : f x = y
⊢ f (m • x) = f x
Tactic:
apply congr_arg
State after:
case intro.intro.h
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
h : IsMultiplyPreprimitive M α n
t : Set β
ht : Set.encard t + 1 = ↑n
s : Set α := ⇑f ⁻¹' t
hs' : ⇑f '' s = t
x✝¹ : ↥(fixingSubgroup M s)
m : M
hm : m ∈ fixingSubgroup M s
x✝ : ↑t
y : β
hy : y ∈ t
x : α
hx : x ∈ s
hx' : f x = y
⊢ m • x = x

State before:
case intro.intro.h
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
h : IsMultiplyPreprimitive M α n
t : Set β
ht : Set.encard t + 1 = ↑n
s : Set α := ⇑f ⁻¹' t
hs' : ⇑f '' s = t
x✝¹ : ↥(fixingSubgroup M s)
m : M
hm : m ∈ fixingSubgroup M s
x✝ : ↑t
y : β
hy : y ∈ t
x : α
hx : x ∈ s
hx' : f x = y
⊢ m • x = x
Tactic:
rw [mem_fixingSubgroup_iff] at hm
State after:
case intro.intro.h
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
h : IsMultiplyPreprimitive M α n
t : Set β
ht : Set.encard t + 1 = ↑n
s : Set α := ⇑f ⁻¹' t
hs' : ⇑f '' s = t
x✝¹ : ↥(fixingSubgroup M s)
m : M
hm : ∀ y ∈ s, m • y = y
x✝ : ↑t
y : β
hy : y ∈ t
x : α
hx : x ∈ s
hx' : f x = y
⊢ m • x = x

State before:
case intro.intro.h
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
h : IsMultiplyPreprimitive M α n
t : Set β
ht : Set.encard t + 1 = ↑n
s : Set α := ⇑f ⁻¹' t
hs' : ⇑f '' s = t
x✝¹ : ↥(fixingSubgroup M s)
m : M
hm : ∀ y ∈ s, m • y = y
x✝ : ↑t
y : β
hy : y ∈ t
x : α
hx : x ∈ s
hx' : f x = y
⊢ m • x = x
Tactic:
exact hm x hx
State after:
no goals

State before:
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
h : IsMultiplyPreprimitive M α n
t : Set β
ht : Set.encard t + 1 = ↑n
s : Set α := ⇑f ⁻¹' t
hs' : ⇑f '' s = t
φ' : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun x =>
    match x with
    | { val := m, property := hm } => { val := φ m, property := ⋯ }
x✝¹ : ↥(fixingSubgroup M s)
x✝ : ↥(SubMulAction.ofFixingSubgroup M s)
m : M
hm : m ∈ fixingSubgroup M s
x : α
hx : x ∈ SubMulAction.ofFixingSubgroup M s
⊢ (fun x =>
        match x with
        | { val := x, property := hx } => { val := f.toFun x, property := ⋯ })
      ({ val := m, property := hm } • { val := x, property := hx }) =
    φ' { val := m, property := hm } •
      (fun x =>
          match x with
          | { val := x, property := hx } => { val := f.toFun x, property := ⋯ })
        { val := x, property := hx }
Tactic:
rw [← SetLike.coe_eq_coe]
State after:
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
h : IsMultiplyPreprimitive M α n
t : Set β
ht : Set.encard t + 1 = ↑n
s : Set α := ⇑f ⁻¹' t
hs' : ⇑f '' s = t
φ' : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun x =>
    match x with
    | { val := m, property := hm } => { val := φ m, property := ⋯ }
x✝¹ : ↥(fixingSubgroup M s)
x✝ : ↥(SubMulAction.ofFixingSubgroup M s)
m : M
hm : m ∈ fixingSubgroup M s
x : α
hx : x ∈ SubMulAction.ofFixingSubgroup M s
⊢ ↑((fun x =>
          match x with
          | { val := x, property := hx } => { val := f.toFun x, property := ⋯ })
        ({ val := m, property := hm } • { val := x, property := hx })) =
    ↑(φ' { val := m, property := hm } •
        (fun x =>
            match x with
            | { val := x, property := hx } => { val := f.toFun x, property := ⋯ })
          { val := x, property := hx })

State before:
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
h : IsMultiplyPreprimitive M α n
t : Set β
ht : Set.encard t + 1 = ↑n
s : Set α := ⇑f ⁻¹' t
hs' : ⇑f '' s = t
φ' : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun x =>
    match x with
    | { val := m, property := hm } => { val := φ m, property := ⋯ }
x✝¹ : ↥(fixingSubgroup M s)
x✝ : ↥(SubMulAction.ofFixingSubgroup M s)
m : M
hm : m ∈ fixingSubgroup M s
x : α
hx : x ∈ SubMulAction.ofFixingSubgroup M s
⊢ ↑((fun x =>
          match x with
          | { val := x, property := hx } => { val := f.toFun x, property := ⋯ })
        ({ val := m, property := hm } • { val := x, property := hx })) =
    ↑(φ' { val := m, property := hm } •
        (fun x =>
            match x with
            | { val := x, property := hx } => { val := f.toFun x, property := ⋯ })
          { val := x, property := hx })
Tactic:
exact f.map_smul' m x
State after:
no goals

State before:
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
h : IsMultiplyPreprimitive M α n
t : Set β
ht : Set.encard t + 1 = ↑n
s : Set α := ⇑f ⁻¹' t
hs' : ⇑f '' s = t
φ' : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun x =>
    match x with
    | { val := m, property := hm } => { val := φ m, property := ⋯ }
f' : ↥(SubMulAction.ofFixingSubgroup M s) →ₑ[φ'] ↥(SubMulAction.ofFixingSubgroup N t) :=
  {
    toFun := fun x =>
      match x with
      | { val := x, property := hx } => { val := f.toFun x, property := ⋯ },
    map_smul' := ⋯ }
⊢ Function.Surjective ⇑f'
Tactic:
rintro ⟨y, hy⟩
State after:
case mk
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
h : IsMultiplyPreprimitive M α n
t : Set β
ht : Set.encard t + 1 = ↑n
s : Set α := ⇑f ⁻¹' t
hs' : ⇑f '' s = t
φ' : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun x =>
    match x with
    | { val := m, property := hm } => { val := φ m, property := ⋯ }
f' : ↥(SubMulAction.ofFixingSubgroup M s) →ₑ[φ'] ↥(SubMulAction.ofFixingSubgroup N t) :=
  {
    toFun := fun x =>
      match x with
      | { val := x, property := hx } => { val := f.toFun x, property := ⋯ },
    map_smul' := ⋯ }
y : β
hy : y ∈ SubMulAction.ofFixingSubgroup N t
⊢ ∃ a, f' a = { val := y, property := hy }

State before:
case mk
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
h : IsMultiplyPreprimitive M α n
t : Set β
ht : Set.encard t + 1 = ↑n
s : Set α := ⇑f ⁻¹' t
hs' : ⇑f '' s = t
φ' : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun x =>
    match x with
    | { val := m, property := hm } => { val := φ m, property := ⋯ }
f' : ↥(SubMulAction.ofFixingSubgroup M s) →ₑ[φ'] ↥(SubMulAction.ofFixingSubgroup N t) :=
  {
    toFun := fun x =>
      match x with
      | { val := x, property := hx } => { val := f.toFun x, property := ⋯ },
    map_smul' := ⋯ }
y : β
hy : y ∈ SubMulAction.ofFixingSubgroup N t
⊢ ∃ a, f' a = { val := y, property := hy }
Tactic:
obtain ⟨x, hx⟩ := hf.right y
State after:
case mk.intro
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
h : IsMultiplyPreprimitive M α n
t : Set β
ht : Set.encard t + 1 = ↑n
s : Set α := ⇑f ⁻¹' t
hs' : ⇑f '' s = t
φ' : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun x =>
    match x with
    | { val := m, property := hm } => { val := φ m, property := ⋯ }
f' : ↥(SubMulAction.ofFixingSubgroup M s) →ₑ[φ'] ↥(SubMulAction.ofFixingSubgroup N t) :=
  {
    toFun := fun x =>
      match x with
      | { val := x, property := hx } => { val := f.toFun x, property := ⋯ },
    map_smul' := ⋯ }
y : β
hy : y ∈ SubMulAction.ofFixingSubgroup N t
x : α
hx : f x = y
⊢ ∃ a, f' a = { val := y, property := hy }

State before:
case mk.intro
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
h : IsMultiplyPreprimitive M α n
t : Set β
ht : Set.encard t + 1 = ↑n
s : Set α := ⇑f ⁻¹' t
hs' : ⇑f '' s = t
φ' : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun x =>
    match x with
    | { val := m, property := hm } => { val := φ m, property := ⋯ }
f' : ↥(SubMulAction.ofFixingSubgroup M s) →ₑ[φ'] ↥(SubMulAction.ofFixingSubgroup N t) :=
  {
    toFun := fun x =>
      match x with
      | { val := x, property := hx } => { val := f.toFun x, property := ⋯ },
    map_smul' := ⋯ }
y : β
hy : y ∈ SubMulAction.ofFixingSubgroup N t
x : α
hx : f x = y
⊢ ∃ a, f' a = { val := y, property := hy }
Tactic:
use ⟨x, ?_⟩
State after:
case h
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
h : IsMultiplyPreprimitive M α n
t : Set β
ht : Set.encard t + 1 = ↑n
s : Set α := ⇑f ⁻¹' t
hs' : ⇑f '' s = t
φ' : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun x =>
    match x with
    | { val := m, property := hm } => { val := φ m, property := ⋯ }
f' : ↥(SubMulAction.ofFixingSubgroup M s) →ₑ[φ'] ↥(SubMulAction.ofFixingSubgroup N t) :=
  {
    toFun := fun x =>
      match x with
      | { val := x, property := hx } => { val := f.toFun x, property := ⋯ },
    map_smul' := ⋯ }
y : β
hy : y ∈ SubMulAction.ofFixingSubgroup N t
x : α
hx : f x = y
⊢ f' { val := x, property := ?w } = { val := y, property := hy }

case w
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
h : IsMultiplyPreprimitive M α n
t : Set β
ht : Set.encard t + 1 = ↑n
s : Set α := ⇑f ⁻¹' t
hs' : ⇑f '' s = t
φ' : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun x =>
    match x with
    | { val := m, property := hm } => { val := φ m, property := ⋯ }
f' : ↥(SubMulAction.ofFixingSubgroup M s) →ₑ[φ'] ↥(SubMulAction.ofFixingSubgroup N t) :=
  {
    toFun := fun x =>
      match x with
      | { val := x, property := hx } => { val := f.toFun x, property := ⋯ },
    map_smul' := ⋯ }
y : β
hy : y ∈ SubMulAction.ofFixingSubgroup N t
x : α
hx : f x = y
⊢ x ∈ SubMulAction.ofFixingSubgroup M s

State before:
case h
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
h : IsMultiplyPreprimitive M α n
t : Set β
ht : Set.encard t + 1 = ↑n
s : Set α := ⇑f ⁻¹' t
hs' : ⇑f '' s = t
φ' : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun x =>
    match x with
    | { val := m, property := hm } => { val := φ m, property := ⋯ }
f' : ↥(SubMulAction.ofFixingSubgroup M s) →ₑ[φ'] ↥(SubMulAction.ofFixingSubgroup N t) :=
  {
    toFun := fun x =>
      match x with
      | { val := x, property := hx } => { val := f.toFun x, property := ⋯ },
    map_smul' := ⋯ }
y : β
hy : y ∈ SubMulAction.ofFixingSubgroup N t
x : α
hx : f x = y
⊢ f' { val := x, property := ?w } = { val := y, property := hy }
Tactic:
simp only [f']
State after:
case h
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
h : IsMultiplyPreprimitive M α n
t : Set β
ht : Set.encard t + 1 = ↑n
s : Set α := ⇑f ⁻¹' t
hs' : ⇑f '' s = t
φ' : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun x =>
    match x with
    | { val := m, property := hm } => { val := φ m, property := ⋯ }
f' : ↥(SubMulAction.ofFixingSubgroup M s) →ₑ[φ'] ↥(SubMulAction.ofFixingSubgroup N t) :=
  {
    toFun := fun x =>
      match x with
      | { val := x, property := hx } => { val := f.toFun x, property := ⋯ },
    map_smul' := ⋯ }
y : β
hy : y ∈ SubMulAction.ofFixingSubgroup N t
x : α
hx : f x = y
⊢ { toFun := fun x => { val := f.toFun ↑x, property := ⋯ }, map_smul' := ⋯ } { val := x, property := ?w } =
    { val := y, property := hy }

State before:
case h
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
h : IsMultiplyPreprimitive M α n
t : Set β
ht : Set.encard t + 1 = ↑n
s : Set α := ⇑f ⁻¹' t
hs' : ⇑f '' s = t
φ' : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun x =>
    match x with
    | { val := m, property := hm } => { val := φ m, property := ⋯ }
f' : ↥(SubMulAction.ofFixingSubgroup M s) →ₑ[φ'] ↥(SubMulAction.ofFixingSubgroup N t) :=
  {
    toFun := fun x =>
      match x with
      | { val := x, property := hx } => { val := f.toFun x, property := ⋯ },
    map_smul' := ⋯ }
y : β
hy : y ∈ SubMulAction.ofFixingSubgroup N t
x : α
hx : f x = y
⊢ { toFun := fun x => { val := f.toFun ↑x, property := ⋯ }, map_smul' := ⋯ } { val := x, property := ?w } =
    { val := y, property := hy }
Tactic:
apply Subtype.coe_injective
State after:
case h.a
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
h : IsMultiplyPreprimitive M α n
t : Set β
ht : Set.encard t + 1 = ↑n
s : Set α := ⇑f ⁻¹' t
hs' : ⇑f '' s = t
φ' : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun x =>
    match x with
    | { val := m, property := hm } => { val := φ m, property := ⋯ }
f' : ↥(SubMulAction.ofFixingSubgroup M s) →ₑ[φ'] ↥(SubMulAction.ofFixingSubgroup N t) :=
  {
    toFun := fun x =>
      match x with
      | { val := x, property := hx } => { val := f.toFun x, property := ⋯ },
    map_smul' := ⋯ }
y : β
hy : y ∈ SubMulAction.ofFixingSubgroup N t
x : α
hx : f x = y
⊢ (fun a => ↑a)
      ({ toFun := fun x => { val := f.toFun ↑x, property := ⋯ }, map_smul' := ⋯ } { val := x, property := ?w }) =
    (fun a => ↑a) { val := y, property := hy }

State before:
case h.a
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
h : IsMultiplyPreprimitive M α n
t : Set β
ht : Set.encard t + 1 = ↑n
s : Set α := ⇑f ⁻¹' t
hs' : ⇑f '' s = t
φ' : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun x =>
    match x with
    | { val := m, property := hm } => { val := φ m, property := ⋯ }
f' : ↥(SubMulAction.ofFixingSubgroup M s) →ₑ[φ'] ↥(SubMulAction.ofFixingSubgroup N t) :=
  {
    toFun := fun x =>
      match x with
      | { val := x, property := hx } => { val := f.toFun x, property := ⋯ },
    map_smul' := ⋯ }
y : β
hy : y ∈ SubMulAction.ofFixingSubgroup N t
x : α
hx : f x = y
⊢ (fun a => ↑a)
      ({ toFun := fun x => { val := f.toFun ↑x, property := ⋯ }, map_smul' := ⋯ } { val := x, property := ?w }) =
    (fun a => ↑a) { val := y, property := hy }
Tactic:
exact hx
State after:
no goals

State before:
case w
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
h : IsMultiplyPreprimitive M α n
t : Set β
ht : Set.encard t + 1 = ↑n
s : Set α := ⇑f ⁻¹' t
hs' : ⇑f '' s = t
φ' : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun x =>
    match x with
    | { val := m, property := hm } => { val := φ m, property := ⋯ }
f' : ↥(SubMulAction.ofFixingSubgroup M s) →ₑ[φ'] ↥(SubMulAction.ofFixingSubgroup N t) :=
  {
    toFun := fun x =>
      match x with
      | { val := x, property := hx } => { val := f.toFun x, property := ⋯ },
    map_smul' := ⋯ }
y : β
hy : y ∈ SubMulAction.ofFixingSubgroup N t
x : α
hx : f x = y
⊢ x ∈ SubMulAction.ofFixingSubgroup M s
Tactic:
intro h
State after:
case w
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
h✝ : IsMultiplyPreprimitive M α n
t : Set β
ht : Set.encard t + 1 = ↑n
s : Set α := ⇑f ⁻¹' t
hs' : ⇑f '' s = t
φ' : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun x =>
    match x with
    | { val := m, property := hm } => { val := φ m, property := ⋯ }
f' : ↥(SubMulAction.ofFixingSubgroup M s) →ₑ[φ'] ↥(SubMulAction.ofFixingSubgroup N t) :=
  {
    toFun := fun x =>
      match x with
      | { val := x, property := hx } => { val := f.toFun x, property := ⋯ },
    map_smul' := ⋯ }
y : β
hy : y ∈ SubMulAction.ofFixingSubgroup N t
x : α
hx : f x = y
h : x ∈ s
⊢ False

State before:
case w
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
h✝ : IsMultiplyPreprimitive M α n
t : Set β
ht : Set.encard t + 1 = ↑n
s : Set α := ⇑f ⁻¹' t
hs' : ⇑f '' s = t
φ' : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun x =>
    match x with
    | { val := m, property := hm } => { val := φ m, property := ⋯ }
f' : ↥(SubMulAction.ofFixingSubgroup M s) →ₑ[φ'] ↥(SubMulAction.ofFixingSubgroup N t) :=
  {
    toFun := fun x =>
      match x with
      | { val := x, property := hx } => { val := f.toFun x, property := ⋯ },
    map_smul' := ⋯ }
y : β
hy : y ∈ SubMulAction.ofFixingSubgroup N t
x : α
hx : f x = y
h : x ∈ s
⊢ False
Tactic:
apply hy
State after:
case w
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
h✝ : IsMultiplyPreprimitive M α n
t : Set β
ht : Set.encard t + 1 = ↑n
s : Set α := ⇑f ⁻¹' t
hs' : ⇑f '' s = t
φ' : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun x =>
    match x with
    | { val := m, property := hm } => { val := φ m, property := ⋯ }
f' : ↥(SubMulAction.ofFixingSubgroup M s) →ₑ[φ'] ↥(SubMulAction.ofFixingSubgroup N t) :=
  {
    toFun := fun x =>
      match x with
      | { val := x, property := hx } => { val := f.toFun x, property := ⋯ },
    map_smul' := ⋯ }
y : β
hy : y ∈ SubMulAction.ofFixingSubgroup N t
x : α
hx : f x = y
h : x ∈ s
⊢ y ∈ t

State before:
case w
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
h✝ : IsMultiplyPreprimitive M α n
t : Set β
ht : Set.encard t + 1 = ↑n
s : Set α := ⇑f ⁻¹' t
hs' : ⇑f '' s = t
φ' : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun x =>
    match x with
    | { val := m, property := hm } => { val := φ m, property := ⋯ }
f' : ↥(SubMulAction.ofFixingSubgroup M s) →ₑ[φ'] ↥(SubMulAction.ofFixingSubgroup N t) :=
  {
    toFun := fun x =>
      match x with
      | { val := x, property := hx } => { val := f.toFun x, property := ⋯ },
    map_smul' := ⋯ }
y : β
hy : y ∈ SubMulAction.ofFixingSubgroup N t
x : α
hx : f x = y
h : x ∈ s
⊢ y ∈ t
Tactic:
rw [← hs']
State after:
case w
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
h✝ : IsMultiplyPreprimitive M α n
t : Set β
ht : Set.encard t + 1 = ↑n
s : Set α := ⇑f ⁻¹' t
hs' : ⇑f '' s = t
φ' : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun x =>
    match x with
    | { val := m, property := hm } => { val := φ m, property := ⋯ }
f' : ↥(SubMulAction.ofFixingSubgroup M s) →ₑ[φ'] ↥(SubMulAction.ofFixingSubgroup N t) :=
  {
    toFun := fun x =>
      match x with
      | { val := x, property := hx } => { val := f.toFun x, property := ⋯ },
    map_smul' := ⋯ }
y : β
hy : y ∈ SubMulAction.ofFixingSubgroup N t
x : α
hx : f x = y
h : x ∈ s
⊢ y ∈ ⇑f '' s

State before:
case w
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
h✝ : IsMultiplyPreprimitive M α n
t : Set β
ht : Set.encard t + 1 = ↑n
s : Set α := ⇑f ⁻¹' t
hs' : ⇑f '' s = t
φ' : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun x =>
    match x with
    | { val := m, property := hm } => { val := φ m, property := ⋯ }
f' : ↥(SubMulAction.ofFixingSubgroup M s) →ₑ[φ'] ↥(SubMulAction.ofFixingSubgroup N t) :=
  {
    toFun := fun x =>
      match x with
      | { val := x, property := hx } => { val := f.toFun x, property := ⋯ },
    map_smul' := ⋯ }
y : β
hy : y ∈ SubMulAction.ofFixingSubgroup N t
x : α
hx : f x = y
h : x ∈ s
⊢ y ∈ ⇑f '' s
Tactic:
exact ⟨x, h, hx⟩
State after:
no goals