Theorem: MulAction.remaining_transitivity (Jordan/MultipleTransitivity.lean)

State before:
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
h : IsMultiplyPretransitive M α n
hmn : n = m + Set.ncard s
⊢ IsMultiplyPretransitive (↥(fixingSubgroup M s)) (↥(SubMulAction.ofFixingSubgroup M s)) m
Tactic:
have hs : PartENat.card s = s.ncard := by
  rw [s.ncard_eq_toFinset_card, PartENat.card_eq_coe_nat_card, Set.Nat.card_coe_set_eq, PartENat.natCast_inj, s.ncard_eq_toFinset_card]
State after:
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
h : IsMultiplyPretransitive M α n
hmn : n = m + Set.ncard s
hs : PartENat.card ↑s = ↑(Set.ncard s)
⊢ IsMultiplyPretransitive (↥(fixingSubgroup M s)) (↥(SubMulAction.ofFixingSubgroup M s)) m

State before:
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
h : IsMultiplyPretransitive M α n
hmn : n = m + Set.ncard s
hs : PartENat.card ↑s = ↑(Set.ncard s)
⊢ IsMultiplyPretransitive (↥(fixingSubgroup M s)) (↥(SubMulAction.ofFixingSubgroup M s)) m
Tactic:
apply IsPretransitive.mk
State after:
case exists_smul_eq
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
h : IsMultiplyPretransitive M α n
hmn : n = m + Set.ncard s
hs : PartENat.card ↑s = ↑(Set.ncard s)
⊢ ∀ (x y : Fin m ↪ ↥(SubMulAction.ofFixingSubgroup M s)), ∃ g, g • x = y

State before:
case exists_smul_eq
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
h : IsMultiplyPretransitive M α n
hmn : n = m + Set.ncard s
hs : PartENat.card ↑s = ↑(Set.ncard s)
⊢ ∀ (x y : Fin m ↪ ↥(SubMulAction.ofFixingSubgroup M s)), ∃ g, g • x = y
Tactic:
intro x y
State after:
case exists_smul_eq
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
h : IsMultiplyPretransitive M α n
hmn : n = m + Set.ncard s
hs : PartENat.card ↑s = ↑(Set.ncard s)
x y : Fin m ↪ ↥(SubMulAction.ofFixingSubgroup M s)
⊢ ∃ g, g • x = y

State before:
case exists_smul_eq
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
h : IsMultiplyPretransitive M α n
hmn : n = m + Set.ncard s
hs : PartENat.card ↑s = ↑(Set.ncard s)
x y : Fin m ↪ ↥(SubMulAction.ofFixingSubgroup M s)
⊢ ∃ g, g • x = y
Tactic:
obtain ⟨z⟩ := equiv_fin_of_partENat_card_eq hs
State after:
case exists_smul_eq.intro
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
h : IsMultiplyPretransitive M α n
hmn : n = m + Set.ncard s
hs : PartENat.card ↑s = ↑(Set.ncard s)
x y : Fin m ↪ ↥(SubMulAction.ofFixingSubgroup M s)
z : Fin (Set.ncard s) ≃ ↑s
⊢ ∃ g, g • x = y

State before:
case exists_smul_eq.intro
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
h : IsMultiplyPretransitive M α n
hmn : n = m + Set.ncard s
hs : PartENat.card ↑s = ↑(Set.ncard s)
x y : Fin m ↪ ↥(SubMulAction.ofFixingSubgroup M s)
z : Fin (Set.ncard s) ≃ ↑s
⊢ ∃ g, g • x = y
Tactic:
obtain ⟨x', hx'1, hx'2⟩ := may_extend_with' z.toEmbedding hmn x
State after:
case exists_smul_eq.intro.intro.intro
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
h : IsMultiplyPretransitive M α n
hmn : n = m + Set.ncard s
hs : PartENat.card ↑s = ↑(Set.ncard s)
x y : Fin m ↪ ↥(SubMulAction.ofFixingSubgroup M s)
z : Fin (Set.ncard s) ≃ ↑s
x' : Fin n ↪ α
hx'1 : Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding x' = Function.Embedding.trans x (subtype sᶜ)
hx'2 :
  Function.Embedding.trans (Fin.natAddEmb m).toEmbedding
      (Function.Embedding.trans (Equiv.toEmbedding (Fin.castIso ⋯).toEquiv) x') =
    Function.Embedding.trans (Equiv.toEmbedding z) (subtype s)
⊢ ∃ g, g • x = y

State before:
case exists_smul_eq.intro.intro.intro
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
h : IsMultiplyPretransitive M α n
hmn : n = m + Set.ncard s
hs : PartENat.card ↑s = ↑(Set.ncard s)
x y : Fin m ↪ ↥(SubMulAction.ofFixingSubgroup M s)
z : Fin (Set.ncard s) ≃ ↑s
x' : Fin n ↪ α
hx'1 : Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding x' = Function.Embedding.trans x (subtype sᶜ)
hx'2 :
  Function.Embedding.trans (Fin.natAddEmb m).toEmbedding
      (Function.Embedding.trans (Equiv.toEmbedding (Fin.castIso ⋯).toEquiv) x') =
    Function.Embedding.trans (Equiv.toEmbedding z) (subtype s)
⊢ ∃ g, g • x = y
Tactic:
obtain ⟨y' : Fin n ↪ α, hy'1, hy'2⟩ := may_extend_with' z.toEmbedding hmn y
State after:
case exists_smul_eq.intro.intro.intro.intro.intro
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
h : IsMultiplyPretransitive M α n
hmn : n = m + Set.ncard s
hs : PartENat.card ↑s = ↑(Set.ncard s)
x y : Fin m ↪ ↥(SubMulAction.ofFixingSubgroup M s)
z : Fin (Set.ncard s) ≃ ↑s
x' : Fin n ↪ α
hx'1 : Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding x' = Function.Embedding.trans x (subtype sᶜ)
hx'2 :
  Function.Embedding.trans (Fin.natAddEmb m).toEmbedding
      (Function.Embedding.trans (Equiv.toEmbedding (Fin.castIso ⋯).toEquiv) x') =
    Function.Embedding.trans (Equiv.toEmbedding z) (subtype s)
y' : Fin n ↪ α
hy'1 : Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding y' = Function.Embedding.trans y (subtype sᶜ)
hy'2 :
  Function.Embedding.trans (Fin.natAddEmb m).toEmbedding
      (Function.Embedding.trans (Equiv.toEmbedding (Fin.castIso ⋯).toEquiv) y') =
    Function.Embedding.trans (Equiv.toEmbedding z) (subtype s)
⊢ ∃ g, g • x = y

State before:
case exists_smul_eq.intro.intro.intro.intro.intro
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
h : IsMultiplyPretransitive M α n
hmn : n = m + Set.ncard s
hs : PartENat.card ↑s = ↑(Set.ncard s)
x y : Fin m ↪ ↥(SubMulAction.ofFixingSubgroup M s)
z : Fin (Set.ncard s) ≃ ↑s
x' : Fin n ↪ α
hx'1 : Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding x' = Function.Embedding.trans x (subtype sᶜ)
hx'2 :
  Function.Embedding.trans (Fin.natAddEmb m).toEmbedding
      (Function.Embedding.trans (Equiv.toEmbedding (Fin.castIso ⋯).toEquiv) x') =
    Function.Embedding.trans (Equiv.toEmbedding z) (subtype s)
y' : Fin n ↪ α
hy'1 : Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding y' = Function.Embedding.trans y (subtype sᶜ)
hy'2 :
  Function.Embedding.trans (Fin.natAddEmb m).toEmbedding
      (Function.Embedding.trans (Equiv.toEmbedding (Fin.castIso ⋯).toEquiv) y') =
    Function.Embedding.trans (Equiv.toEmbedding z) (subtype s)
⊢ ∃ g, g • x = y
Tactic:
obtain ⟨g, hg⟩ := h.exists_smul_eq x' y'
State after:
case exists_smul_eq.intro.intro.intro.intro.intro.intro
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
h : IsMultiplyPretransitive M α n
hmn : n = m + Set.ncard s
hs : PartENat.card ↑s = ↑(Set.ncard s)
x y : Fin m ↪ ↥(SubMulAction.ofFixingSubgroup M s)
z : Fin (Set.ncard s) ≃ ↑s
x' : Fin n ↪ α
hx'1 : Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding x' = Function.Embedding.trans x (subtype sᶜ)
hx'2 :
  Function.Embedding.trans (Fin.natAddEmb m).toEmbedding
      (Function.Embedding.trans (Equiv.toEmbedding (Fin.castIso ⋯).toEquiv) x') =
    Function.Embedding.trans (Equiv.toEmbedding z) (subtype s)
y' : Fin n ↪ α
hy'1 : Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding y' = Function.Embedding.trans y (subtype sᶜ)
hy'2 :
  Function.Embedding.trans (Fin.natAddEmb m).toEmbedding
      (Function.Embedding.trans (Equiv.toEmbedding (Fin.castIso ⋯).toEquiv) y') =
    Function.Embedding.trans (Equiv.toEmbedding z) (subtype s)
g : M
hg : g • x' = y'
⊢ ∃ g, g • x = y

State before:
case exists_smul_eq.intro.intro.intro.intro.intro.intro
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
h : IsMultiplyPretransitive M α n
hmn : n = m + Set.ncard s
hs : PartENat.card ↑s = ↑(Set.ncard s)
x y : Fin m ↪ ↥(SubMulAction.ofFixingSubgroup M s)
z : Fin (Set.ncard s) ≃ ↑s
x' : Fin n ↪ α
hx'1 : Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding x' = Function.Embedding.trans x (subtype sᶜ)
hx'2 :
  Function.Embedding.trans (Fin.natAddEmb m).toEmbedding
      (Function.Embedding.trans (Equiv.toEmbedding (Fin.castIso ⋯).toEquiv) x') =
    Function.Embedding.trans (Equiv.toEmbedding z) (subtype s)
y' : Fin n ↪ α
hy'1 : Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding y' = Function.Embedding.trans y (subtype sᶜ)
hy'2 :
  Function.Embedding.trans (Fin.natAddEmb m).toEmbedding
      (Function.Embedding.trans (Equiv.toEmbedding (Fin.castIso ⋯).toEquiv) y') =
    Function.Embedding.trans (Equiv.toEmbedding z) (subtype s)
g : M
hg : g • x' = y'
⊢ ∃ g, g • x = y
Tactic:
suffices g ∈ fixingSubgroup M s by
  use ⟨g, this⟩
  ext i
  simp only [smul_apply, SubMulAction.val_smul_of_tower]
  have : (y i : α) = (y.trans (subtype (sᶜ)) i : α) := by
    simp only [trans_apply, Function.Embedding.coe_subtype]
    rfl
  rw [this]
  have : (x i : α) = (x.trans (subtype (sᶜ)) i : α) := by
    simp only [trans_apply, Function.Embedding.coe_subtype]
    rfl
  rw [this]
  rw [← Function.Embedding.ext_iff] at hx'1 hy'1
  simp_rw [← hy'1 i, ← hx'1 i, ← hg]
  simp only [trans_apply, smul_apply, RelEmbedding.coe_toEmbedding]
  rfl
State after:
case exists_smul_eq.intro.intro.intro.intro.intro.intro
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
h : IsMultiplyPretransitive M α n
hmn : n = m + Set.ncard s
hs : PartENat.card ↑s = ↑(Set.ncard s)
x y : Fin m ↪ ↥(SubMulAction.ofFixingSubgroup M s)
z : Fin (Set.ncard s) ≃ ↑s
x' : Fin n ↪ α
hx'1 : Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding x' = Function.Embedding.trans x (subtype sᶜ)
hx'2 :
  Function.Embedding.trans (Fin.natAddEmb m).toEmbedding
      (Function.Embedding.trans (Equiv.toEmbedding (Fin.castIso ⋯).toEquiv) x') =
    Function.Embedding.trans (Equiv.toEmbedding z) (subtype s)
y' : Fin n ↪ α
hy'1 : Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding y' = Function.Embedding.trans y (subtype sᶜ)
hy'2 :
  Function.Embedding.trans (Fin.natAddEmb m).toEmbedding
      (Function.Embedding.trans (Equiv.toEmbedding (Fin.castIso ⋯).toEquiv) y') =
    Function.Embedding.trans (Equiv.toEmbedding z) (subtype s)
g : M
hg : g • x' = y'
⊢ g ∈ fixingSubgroup M s

State before:
case exists_smul_eq.intro.intro.intro.intro.intro.intro
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
h : IsMultiplyPretransitive M α n
hmn : n = m + Set.ncard s
hs : PartENat.card ↑s = ↑(Set.ncard s)
x y : Fin m ↪ ↥(SubMulAction.ofFixingSubgroup M s)
z : Fin (Set.ncard s) ≃ ↑s
x' : Fin n ↪ α
hx'1 : Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding x' = Function.Embedding.trans x (subtype sᶜ)
hx'2 :
  Function.Embedding.trans (Fin.natAddEmb m).toEmbedding
      (Function.Embedding.trans (Equiv.toEmbedding (Fin.castIso ⋯).toEquiv) x') =
    Function.Embedding.trans (Equiv.toEmbedding z) (subtype s)
y' : Fin n ↪ α
hy'1 : Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding y' = Function.Embedding.trans y (subtype sᶜ)
hy'2 :
  Function.Embedding.trans (Fin.natAddEmb m).toEmbedding
      (Function.Embedding.trans (Equiv.toEmbedding (Fin.castIso ⋯).toEquiv) y') =
    Function.Embedding.trans (Equiv.toEmbedding z) (subtype s)
g : M
hg : g • x' = y'
⊢ g ∈ fixingSubgroup M s
Tactic:
intro a
State after:
case exists_smul_eq.intro.intro.intro.intro.intro.intro
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
h : IsMultiplyPretransitive M α n
hmn : n = m + Set.ncard s
hs : PartENat.card ↑s = ↑(Set.ncard s)
x y : Fin m ↪ ↥(SubMulAction.ofFixingSubgroup M s)
z : Fin (Set.ncard s) ≃ ↑s
x' : Fin n ↪ α
hx'1 : Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding x' = Function.Embedding.trans x (subtype sᶜ)
hx'2 :
  Function.Embedding.trans (Fin.natAddEmb m).toEmbedding
      (Function.Embedding.trans (Equiv.toEmbedding (Fin.castIso ⋯).toEquiv) x') =
    Function.Embedding.trans (Equiv.toEmbedding z) (subtype s)
y' : Fin n ↪ α
hy'1 : Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding y' = Function.Embedding.trans y (subtype sᶜ)
hy'2 :
  Function.Embedding.trans (Fin.natAddEmb m).toEmbedding
      (Function.Embedding.trans (Equiv.toEmbedding (Fin.castIso ⋯).toEquiv) y') =
    Function.Embedding.trans (Equiv.toEmbedding z) (subtype s)
g : M
hg : g • x' = y'
a : ↑s
⊢ g • ↑a = ↑a

State before:
case exists_smul_eq.intro.intro.intro.intro.intro.intro
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
h : IsMultiplyPretransitive M α n
hmn : n = m + Set.ncard s
hs : PartENat.card ↑s = ↑(Set.ncard s)
x y : Fin m ↪ ↥(SubMulAction.ofFixingSubgroup M s)
z : Fin (Set.ncard s) ≃ ↑s
x' : Fin n ↪ α
hx'1 : Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding x' = Function.Embedding.trans x (subtype sᶜ)
hx'2 :
  Function.Embedding.trans (Fin.natAddEmb m).toEmbedding
      (Function.Embedding.trans (Equiv.toEmbedding (Fin.castIso ⋯).toEquiv) x') =
    Function.Embedding.trans (Equiv.toEmbedding z) (subtype s)
y' : Fin n ↪ α
hy'1 : Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding y' = Function.Embedding.trans y (subtype sᶜ)
hy'2 :
  Function.Embedding.trans (Fin.natAddEmb m).toEmbedding
      (Function.Embedding.trans (Equiv.toEmbedding (Fin.castIso ⋯).toEquiv) y') =
    Function.Embedding.trans (Equiv.toEmbedding z) (subtype s)
g : M
hg : g • x' = y'
a : ↑s
⊢ g • ↑a = ↑a
Tactic:
have : z.toEmbedding.trans (subtype (s : Set α)) (z.symm a) = a := by
  simp only [trans_apply, Equiv.toEmbedding_apply, Equiv.apply_symm_apply,
    Function.Embedding.coe_subtype]
  rfl
State after:
case exists_smul_eq.intro.intro.intro.intro.intro.intro
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
h : IsMultiplyPretransitive M α n
hmn : n = m + Set.ncard s
hs : PartENat.card ↑s = ↑(Set.ncard s)
x y : Fin m ↪ ↥(SubMulAction.ofFixingSubgroup M s)
z : Fin (Set.ncard s) ≃ ↑s
x' : Fin n ↪ α
hx'1 : Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding x' = Function.Embedding.trans x (subtype sᶜ)
hx'2 :
  Function.Embedding.trans (Fin.natAddEmb m).toEmbedding
      (Function.Embedding.trans (Equiv.toEmbedding (Fin.castIso ⋯).toEquiv) x') =
    Function.Embedding.trans (Equiv.toEmbedding z) (subtype s)
y' : Fin n ↪ α
hy'1 : Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding y' = Function.Embedding.trans y (subtype sᶜ)
hy'2 :
  Function.Embedding.trans (Fin.natAddEmb m).toEmbedding
      (Function.Embedding.trans (Equiv.toEmbedding (Fin.castIso ⋯).toEquiv) y') =
    Function.Embedding.trans (Equiv.toEmbedding z) (subtype s)
g : M
hg : g • x' = y'
a : ↑s
this : (Function.Embedding.trans (Equiv.toEmbedding z) (subtype s)) (z.symm a) = ↑a
⊢ g • ↑a = ↑a

State before:
case exists_smul_eq.intro.intro.intro.intro.intro.intro
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
h : IsMultiplyPretransitive M α n
hmn : n = m + Set.ncard s
hs : PartENat.card ↑s = ↑(Set.ncard s)
x y : Fin m ↪ ↥(SubMulAction.ofFixingSubgroup M s)
z : Fin (Set.ncard s) ≃ ↑s
x' : Fin n ↪ α
hx'1 : Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding x' = Function.Embedding.trans x (subtype sᶜ)
hx'2 :
  Function.Embedding.trans (Fin.natAddEmb m).toEmbedding
      (Function.Embedding.trans (Equiv.toEmbedding (Fin.castIso ⋯).toEquiv) x') =
    Function.Embedding.trans (Equiv.toEmbedding z) (subtype s)
y' : Fin n ↪ α
hy'1 : Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding y' = Function.Embedding.trans y (subtype sᶜ)
hy'2 :
  Function.Embedding.trans (Fin.natAddEmb m).toEmbedding
      (Function.Embedding.trans (Equiv.toEmbedding (Fin.castIso ⋯).toEquiv) y') =
    Function.Embedding.trans (Equiv.toEmbedding z) (subtype s)
g : M
hg : g • x' = y'
a : ↑s
this : (Function.Embedding.trans (Equiv.toEmbedding z) (subtype s)) (z.symm a) = ↑a
⊢ g • ↑a = ↑a
Tactic:
simp only [← this]
State after:
case exists_smul_eq.intro.intro.intro.intro.intro.intro
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
h : IsMultiplyPretransitive M α n
hmn : n = m + Set.ncard s
hs : PartENat.card ↑s = ↑(Set.ncard s)
x y : Fin m ↪ ↥(SubMulAction.ofFixingSubgroup M s)
z : Fin (Set.ncard s) ≃ ↑s
x' : Fin n ↪ α
hx'1 : Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding x' = Function.Embedding.trans x (subtype sᶜ)
hx'2 :
  Function.Embedding.trans (Fin.natAddEmb m).toEmbedding
      (Function.Embedding.trans (Equiv.toEmbedding (Fin.castIso ⋯).toEquiv) x') =
    Function.Embedding.trans (Equiv.toEmbedding z) (subtype s)
y' : Fin n ↪ α
hy'1 : Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding y' = Function.Embedding.trans y (subtype sᶜ)
hy'2 :
  Function.Embedding.trans (Fin.natAddEmb m).toEmbedding
      (Function.Embedding.trans (Equiv.toEmbedding (Fin.castIso ⋯).toEquiv) y') =
    Function.Embedding.trans (Equiv.toEmbedding z) (subtype s)
g : M
hg : g • x' = y'
a : ↑s
this : (Function.Embedding.trans (Equiv.toEmbedding z) (subtype s)) (z.symm a) = ↑a
⊢ g • (Function.Embedding.trans (Equiv.toEmbedding z) (subtype s)) (z.symm a) =
    (Function.Embedding.trans (Equiv.toEmbedding z) (subtype s)) (z.symm a)

State before:
case exists_smul_eq.intro.intro.intro.intro.intro.intro
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
h : IsMultiplyPretransitive M α n
hmn : n = m + Set.ncard s
hs : PartENat.card ↑s = ↑(Set.ncard s)
x y : Fin m ↪ ↥(SubMulAction.ofFixingSubgroup M s)
z : Fin (Set.ncard s) ≃ ↑s
x' : Fin n ↪ α
hx'1 : Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding x' = Function.Embedding.trans x (subtype sᶜ)
hx'2 :
  Function.Embedding.trans (Fin.natAddEmb m).toEmbedding
      (Function.Embedding.trans (Equiv.toEmbedding (Fin.castIso ⋯).toEquiv) x') =
    Function.Embedding.trans (Equiv.toEmbedding z) (subtype s)
y' : Fin n ↪ α
hy'1 : Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding y' = Function.Embedding.trans y (subtype sᶜ)
hy'2 :
  Function.Embedding.trans (Fin.natAddEmb m).toEmbedding
      (Function.Embedding.trans (Equiv.toEmbedding (Fin.castIso ⋯).toEquiv) y') =
    Function.Embedding.trans (Equiv.toEmbedding z) (subtype s)
g : M
hg : g • x' = y'
a : ↑s
this : (Function.Embedding.trans (Equiv.toEmbedding z) (subtype s)) (z.symm a) = ↑a
⊢ g • (Function.Embedding.trans (Equiv.toEmbedding z) (subtype s)) (z.symm a) =
    (Function.Embedding.trans (Equiv.toEmbedding z) (subtype s)) (z.symm a)
Tactic:
conv_lhs => rw [← hx'2]
State after:
case exists_smul_eq.intro.intro.intro.intro.intro.intro
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
h : IsMultiplyPretransitive M α n
hmn : n = m + Set.ncard s
hs : PartENat.card ↑s = ↑(Set.ncard s)
x y : Fin m ↪ ↥(SubMulAction.ofFixingSubgroup M s)
z : Fin (Set.ncard s) ≃ ↑s
x' : Fin n ↪ α
hx'1 : Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding x' = Function.Embedding.trans x (subtype sᶜ)
hx'2 :
  Function.Embedding.trans (Fin.natAddEmb m).toEmbedding
      (Function.Embedding.trans (Equiv.toEmbedding (Fin.castIso ⋯).toEquiv) x') =
    Function.Embedding.trans (Equiv.toEmbedding z) (subtype s)
y' : Fin n ↪ α
hy'1 : Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding y' = Function.Embedding.trans y (subtype sᶜ)
hy'2 :
  Function.Embedding.trans (Fin.natAddEmb m).toEmbedding
      (Function.Embedding.trans (Equiv.toEmbedding (Fin.castIso ⋯).toEquiv) y') =
    Function.Embedding.trans (Equiv.toEmbedding z) (subtype s)
g : M
hg : g • x' = y'
a : ↑s
this : (Function.Embedding.trans (Equiv.toEmbedding z) (subtype s)) (z.symm a) = ↑a
⊢ g •
      (Function.Embedding.trans (Fin.natAddEmb m).toEmbedding
          (Function.Embedding.trans (Equiv.toEmbedding (Fin.castIso ⋯).toEquiv) x'))
        (z.symm a) =
    (Function.Embedding.trans (Equiv.toEmbedding z) (subtype s)) (z.symm a)

State before:
case exists_smul_eq.intro.intro.intro.intro.intro.intro
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
h : IsMultiplyPretransitive M α n
hmn : n = m + Set.ncard s
hs : PartENat.card ↑s = ↑(Set.ncard s)
x y : Fin m ↪ ↥(SubMulAction.ofFixingSubgroup M s)
z : Fin (Set.ncard s) ≃ ↑s
x' : Fin n ↪ α
hx'1 : Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding x' = Function.Embedding.trans x (subtype sᶜ)
hx'2 :
  Function.Embedding.trans (Fin.natAddEmb m).toEmbedding
      (Function.Embedding.trans (Equiv.toEmbedding (Fin.castIso ⋯).toEquiv) x') =
    Function.Embedding.trans (Equiv.toEmbedding z) (subtype s)
y' : Fin n ↪ α
hy'1 : Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding y' = Function.Embedding.trans y (subtype sᶜ)
hy'2 :
  Function.Embedding.trans (Fin.natAddEmb m).toEmbedding
      (Function.Embedding.trans (Equiv.toEmbedding (Fin.castIso ⋯).toEquiv) y') =
    Function.Embedding.trans (Equiv.toEmbedding z) (subtype s)
g : M
hg : g • x' = y'
a : ↑s
this : (Function.Embedding.trans (Equiv.toEmbedding z) (subtype s)) (z.symm a) = ↑a
⊢ g •
      (Function.Embedding.trans (Fin.natAddEmb m).toEmbedding
          (Function.Embedding.trans (Equiv.toEmbedding (Fin.castIso ⋯).toEquiv) x'))
        (z.symm a) =
    (Function.Embedding.trans (Equiv.toEmbedding z) (subtype s)) (z.symm a)
Tactic:
rw [← hy'2, ← hg]
State after:
case exists_smul_eq.intro.intro.intro.intro.intro.intro
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
h : IsMultiplyPretransitive M α n
hmn : n = m + Set.ncard s
hs : PartENat.card ↑s = ↑(Set.ncard s)
x y : Fin m ↪ ↥(SubMulAction.ofFixingSubgroup M s)
z : Fin (Set.ncard s) ≃ ↑s
x' : Fin n ↪ α
hx'1 : Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding x' = Function.Embedding.trans x (subtype sᶜ)
hx'2 :
  Function.Embedding.trans (Fin.natAddEmb m).toEmbedding
      (Function.Embedding.trans (Equiv.toEmbedding (Fin.castIso ⋯).toEquiv) x') =
    Function.Embedding.trans (Equiv.toEmbedding z) (subtype s)
y' : Fin n ↪ α
hy'1 : Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding y' = Function.Embedding.trans y (subtype sᶜ)
hy'2 :
  Function.Embedding.trans (Fin.natAddEmb m).toEmbedding
      (Function.Embedding.trans (Equiv.toEmbedding (Fin.castIso ⋯).toEquiv) y') =
    Function.Embedding.trans (Equiv.toEmbedding z) (subtype s)
g : M
hg : g • x' = y'
a : ↑s
this : (Function.Embedding.trans (Equiv.toEmbedding z) (subtype s)) (z.symm a) = ↑a
⊢ g •
      (Function.Embedding.trans (Fin.natAddEmb m).toEmbedding
          (Function.Embedding.trans (Equiv.toEmbedding (Fin.castIso ⋯).toEquiv) x'))
        (z.symm a) =
    (Function.Embedding.trans (Fin.natAddEmb m).toEmbedding
        (Function.Embedding.trans (Equiv.toEmbedding (Fin.castIso ⋯).toEquiv) (g • x')))
      (z.symm a)

State before:
case exists_smul_eq.intro.intro.intro.intro.intro.intro
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
h : IsMultiplyPretransitive M α n
hmn : n = m + Set.ncard s
hs : PartENat.card ↑s = ↑(Set.ncard s)
x y : Fin m ↪ ↥(SubMulAction.ofFixingSubgroup M s)
z : Fin (Set.ncard s) ≃ ↑s
x' : Fin n ↪ α
hx'1 : Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding x' = Function.Embedding.trans x (subtype sᶜ)
hx'2 :
  Function.Embedding.trans (Fin.natAddEmb m).toEmbedding
      (Function.Embedding.trans (Equiv.toEmbedding (Fin.castIso ⋯).toEquiv) x') =
    Function.Embedding.trans (Equiv.toEmbedding z) (subtype s)
y' : Fin n ↪ α
hy'1 : Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding y' = Function.Embedding.trans y (subtype sᶜ)
hy'2 :
  Function.Embedding.trans (Fin.natAddEmb m).toEmbedding
      (Function.Embedding.trans (Equiv.toEmbedding (Fin.castIso ⋯).toEquiv) y') =
    Function.Embedding.trans (Equiv.toEmbedding z) (subtype s)
g : M
hg : g • x' = y'
a : ↑s
this : (Function.Embedding.trans (Equiv.toEmbedding z) (subtype s)) (z.symm a) = ↑a
⊢ g •
      (Function.Embedding.trans (Fin.natAddEmb m).toEmbedding
          (Function.Embedding.trans (Equiv.toEmbedding (Fin.castIso ⋯).toEquiv) x'))
        (z.symm a) =
    (Function.Embedding.trans (Fin.natAddEmb m).toEmbedding
        (Function.Embedding.trans (Equiv.toEmbedding (Fin.castIso ⋯).toEquiv) (g • x')))
      (z.symm a)
Tactic:
simp only [trans_apply, smul_apply]
State after:
no goals

State before:
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
h : IsMultiplyPretransitive M α n
hmn : n = m + Set.ncard s
⊢ PartENat.card ↑s = ↑(Set.ncard s)
Tactic:
rw [s.ncard_eq_toFinset_card, PartENat.card_eq_coe_nat_card, Set.Nat.card_coe_set_eq, PartENat.natCast_inj, s.ncard_eq_toFinset_card]
State after:
no goals

State before:
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
h : IsMultiplyPretransitive M α n
hmn : n = m + Set.ncard s
hs : PartENat.card ↑s = ↑(Set.ncard s)
x y : Fin m ↪ ↥(SubMulAction.ofFixingSubgroup M s)
z : Fin (Set.ncard s) ≃ ↑s
x' : Fin n ↪ α
hx'1 : Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding x' = Function.Embedding.trans x (subtype sᶜ)
hx'2 :
  Function.Embedding.trans (Fin.natAddEmb m).toEmbedding
      (Function.Embedding.trans (Equiv.toEmbedding (Fin.castIso ⋯).toEquiv) x') =
    Function.Embedding.trans (Equiv.toEmbedding z) (subtype s)
y' : Fin n ↪ α
hy'1 : Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding y' = Function.Embedding.trans y (subtype sᶜ)
hy'2 :
  Function.Embedding.trans (Fin.natAddEmb m).toEmbedding
      (Function.Embedding.trans (Equiv.toEmbedding (Fin.castIso ⋯).toEquiv) y') =
    Function.Embedding.trans (Equiv.toEmbedding z) (subtype s)
g : M
hg : g • x' = y'
this : g ∈ fixingSubgroup M s
⊢ ∃ g, g • x = y
Tactic:
use ⟨g, this⟩
State after:
case h
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
h : IsMultiplyPretransitive M α n
hmn : n = m + Set.ncard s
hs : PartENat.card ↑s = ↑(Set.ncard s)
x y : Fin m ↪ ↥(SubMulAction.ofFixingSubgroup M s)
z : Fin (Set.ncard s) ≃ ↑s
x' : Fin n ↪ α
hx'1 : Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding x' = Function.Embedding.trans x (subtype sᶜ)
hx'2 :
  Function.Embedding.trans (Fin.natAddEmb m).toEmbedding
      (Function.Embedding.trans (Equiv.toEmbedding (Fin.castIso ⋯).toEquiv) x') =
    Function.Embedding.trans (Equiv.toEmbedding z) (subtype s)
y' : Fin n ↪ α
hy'1 : Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding y' = Function.Embedding.trans y (subtype sᶜ)
hy'2 :
  Function.Embedding.trans (Fin.natAddEmb m).toEmbedding
      (Function.Embedding.trans (Equiv.toEmbedding (Fin.castIso ⋯).toEquiv) y') =
    Function.Embedding.trans (Equiv.toEmbedding z) (subtype s)
g : M
hg : g • x' = y'
this : g ∈ fixingSubgroup M s
⊢ { val := g, property := this } • x = y

State before:
case h
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
h : IsMultiplyPretransitive M α n
hmn : n = m + Set.ncard s
hs : PartENat.card ↑s = ↑(Set.ncard s)
x y : Fin m ↪ ↥(SubMulAction.ofFixingSubgroup M s)
z : Fin (Set.ncard s) ≃ ↑s
x' : Fin n ↪ α
hx'1 : Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding x' = Function.Embedding.trans x (subtype sᶜ)
hx'2 :
  Function.Embedding.trans (Fin.natAddEmb m).toEmbedding
      (Function.Embedding.trans (Equiv.toEmbedding (Fin.castIso ⋯).toEquiv) x') =
    Function.Embedding.trans (Equiv.toEmbedding z) (subtype s)
y' : Fin n ↪ α
hy'1 : Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding y' = Function.Embedding.trans y (subtype sᶜ)
hy'2 :
  Function.Embedding.trans (Fin.natAddEmb m).toEmbedding
      (Function.Embedding.trans (Equiv.toEmbedding (Fin.castIso ⋯).toEquiv) y') =
    Function.Embedding.trans (Equiv.toEmbedding z) (subtype s)
g : M
hg : g • x' = y'
this : g ∈ fixingSubgroup M s
⊢ { val := g, property := this } • x = y
Tactic:
ext i
State after:
case h.h.a
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
h : IsMultiplyPretransitive M α n
hmn : n = m + Set.ncard s
hs : PartENat.card ↑s = ↑(Set.ncard s)
x y : Fin m ↪ ↥(SubMulAction.ofFixingSubgroup M s)
z : Fin (Set.ncard s) ≃ ↑s
x' : Fin n ↪ α
hx'1 : Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding x' = Function.Embedding.trans x (subtype sᶜ)
hx'2 :
  Function.Embedding.trans (Fin.natAddEmb m).toEmbedding
      (Function.Embedding.trans (Equiv.toEmbedding (Fin.castIso ⋯).toEquiv) x') =
    Function.Embedding.trans (Equiv.toEmbedding z) (subtype s)
y' : Fin n ↪ α
hy'1 : Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding y' = Function.Embedding.trans y (subtype sᶜ)
hy'2 :
  Function.Embedding.trans (Fin.natAddEmb m).toEmbedding
      (Function.Embedding.trans (Equiv.toEmbedding (Fin.castIso ⋯).toEquiv) y') =
    Function.Embedding.trans (Equiv.toEmbedding z) (subtype s)
g : M
hg : g • x' = y'
this : g ∈ fixingSubgroup M s
i : Fin m
⊢ ↑(({ val := g, property := this } • x) i) = ↑(y i)

State before:
case h.h.a
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
h : IsMultiplyPretransitive M α n
hmn : n = m + Set.ncard s
hs : PartENat.card ↑s = ↑(Set.ncard s)
x y : Fin m ↪ ↥(SubMulAction.ofFixingSubgroup M s)
z : Fin (Set.ncard s) ≃ ↑s
x' : Fin n ↪ α
hx'1 : Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding x' = Function.Embedding.trans x (subtype sᶜ)
hx'2 :
  Function.Embedding.trans (Fin.natAddEmb m).toEmbedding
      (Function.Embedding.trans (Equiv.toEmbedding (Fin.castIso ⋯).toEquiv) x') =
    Function.Embedding.trans (Equiv.toEmbedding z) (subtype s)
y' : Fin n ↪ α
hy'1 : Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding y' = Function.Embedding.trans y (subtype sᶜ)
hy'2 :
  Function.Embedding.trans (Fin.natAddEmb m).toEmbedding
      (Function.Embedding.trans (Equiv.toEmbedding (Fin.castIso ⋯).toEquiv) y') =
    Function.Embedding.trans (Equiv.toEmbedding z) (subtype s)
g : M
hg : g • x' = y'
this : g ∈ fixingSubgroup M s
i : Fin m
⊢ ↑(({ val := g, property := this } • x) i) = ↑(y i)
Tactic:
simp only [smul_apply, SubMulAction.val_smul_of_tower]
State after:
case h.h.a
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
h : IsMultiplyPretransitive M α n
hmn : n = m + Set.ncard s
hs : PartENat.card ↑s = ↑(Set.ncard s)
x y : Fin m ↪ ↥(SubMulAction.ofFixingSubgroup M s)
z : Fin (Set.ncard s) ≃ ↑s
x' : Fin n ↪ α
hx'1 : Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding x' = Function.Embedding.trans x (subtype sᶜ)
hx'2 :
  Function.Embedding.trans (Fin.natAddEmb m).toEmbedding
      (Function.Embedding.trans (Equiv.toEmbedding (Fin.castIso ⋯).toEquiv) x') =
    Function.Embedding.trans (Equiv.toEmbedding z) (subtype s)
y' : Fin n ↪ α
hy'1 : Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding y' = Function.Embedding.trans y (subtype sᶜ)
hy'2 :
  Function.Embedding.trans (Fin.natAddEmb m).toEmbedding
      (Function.Embedding.trans (Equiv.toEmbedding (Fin.castIso ⋯).toEquiv) y') =
    Function.Embedding.trans (Equiv.toEmbedding z) (subtype s)
g : M
hg : g • x' = y'
this : g ∈ fixingSubgroup M s
i : Fin m
⊢ { val := g, property := this } • ↑(x i) = ↑(y i)

State before:
case h.h.a
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
h : IsMultiplyPretransitive M α n
hmn : n = m + Set.ncard s
hs : PartENat.card ↑s = ↑(Set.ncard s)
x y : Fin m ↪ ↥(SubMulAction.ofFixingSubgroup M s)
z : Fin (Set.ncard s) ≃ ↑s
x' : Fin n ↪ α
hx'1 : Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding x' = Function.Embedding.trans x (subtype sᶜ)
hx'2 :
  Function.Embedding.trans (Fin.natAddEmb m).toEmbedding
      (Function.Embedding.trans (Equiv.toEmbedding (Fin.castIso ⋯).toEquiv) x') =
    Function.Embedding.trans (Equiv.toEmbedding z) (subtype s)
y' : Fin n ↪ α
hy'1 : Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding y' = Function.Embedding.trans y (subtype sᶜ)
hy'2 :
  Function.Embedding.trans (Fin.natAddEmb m).toEmbedding
      (Function.Embedding.trans (Equiv.toEmbedding (Fin.castIso ⋯).toEquiv) y') =
    Function.Embedding.trans (Equiv.toEmbedding z) (subtype s)
g : M
hg : g • x' = y'
this : g ∈ fixingSubgroup M s
i : Fin m
⊢ { val := g, property := this } • ↑(x i) = ↑(y i)
Tactic:
have : (y i : α) = (y.trans (subtype (sᶜ)) i : α) := by
  simp only [trans_apply, Function.Embedding.coe_subtype]
  rfl
State after:
case h.h.a
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
h : IsMultiplyPretransitive M α n
hmn : n = m + Set.ncard s
hs : PartENat.card ↑s = ↑(Set.ncard s)
x y : Fin m ↪ ↥(SubMulAction.ofFixingSubgroup M s)
z : Fin (Set.ncard s) ≃ ↑s
x' : Fin n ↪ α
hx'1 : Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding x' = Function.Embedding.trans x (subtype sᶜ)
hx'2 :
  Function.Embedding.trans (Fin.natAddEmb m).toEmbedding
      (Function.Embedding.trans (Equiv.toEmbedding (Fin.castIso ⋯).toEquiv) x') =
    Function.Embedding.trans (Equiv.toEmbedding z) (subtype s)
y' : Fin n ↪ α
hy'1 : Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding y' = Function.Embedding.trans y (subtype sᶜ)
hy'2 :
  Function.Embedding.trans (Fin.natAddEmb m).toEmbedding
      (Function.Embedding.trans (Equiv.toEmbedding (Fin.castIso ⋯).toEquiv) y') =
    Function.Embedding.trans (Equiv.toEmbedding z) (subtype s)
g : M
hg : g • x' = y'
this✝ : g ∈ fixingSubgroup M s
i : Fin m
this : ↑(y i) = (Function.Embedding.trans y (subtype sᶜ)) i
⊢ { val := g, property := this✝ } • ↑(x i) = ↑(y i)

State before:
case h.h.a
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
h : IsMultiplyPretransitive M α n
hmn : n = m + Set.ncard s
hs : PartENat.card ↑s = ↑(Set.ncard s)
x y : Fin m ↪ ↥(SubMulAction.ofFixingSubgroup M s)
z : Fin (Set.ncard s) ≃ ↑s
x' : Fin n ↪ α
hx'1 : Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding x' = Function.Embedding.trans x (subtype sᶜ)
hx'2 :
  Function.Embedding.trans (Fin.natAddEmb m).toEmbedding
      (Function.Embedding.trans (Equiv.toEmbedding (Fin.castIso ⋯).toEquiv) x') =
    Function.Embedding.trans (Equiv.toEmbedding z) (subtype s)
y' : Fin n ↪ α
hy'1 : Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding y' = Function.Embedding.trans y (subtype sᶜ)
hy'2 :
  Function.Embedding.trans (Fin.natAddEmb m).toEmbedding
      (Function.Embedding.trans (Equiv.toEmbedding (Fin.castIso ⋯).toEquiv) y') =
    Function.Embedding.trans (Equiv.toEmbedding z) (subtype s)
g : M
hg : g • x' = y'
this✝ : g ∈ fixingSubgroup M s
i : Fin m
this : ↑(y i) = (Function.Embedding.trans y (subtype sᶜ)) i
⊢ { val := g, property := this✝ } • ↑(x i) = ↑(y i)
Tactic:
rw [this]
State after:
case h.h.a
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
h : IsMultiplyPretransitive M α n
hmn : n = m + Set.ncard s
hs : PartENat.card ↑s = ↑(Set.ncard s)
x y : Fin m ↪ ↥(SubMulAction.ofFixingSubgroup M s)
z : Fin (Set.ncard s) ≃ ↑s
x' : Fin n ↪ α
hx'1 : Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding x' = Function.Embedding.trans x (subtype sᶜ)
hx'2 :
  Function.Embedding.trans (Fin.natAddEmb m).toEmbedding
      (Function.Embedding.trans (Equiv.toEmbedding (Fin.castIso ⋯).toEquiv) x') =
    Function.Embedding.trans (Equiv.toEmbedding z) (subtype s)
y' : Fin n ↪ α
hy'1 : Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding y' = Function.Embedding.trans y (subtype sᶜ)
hy'2 :
  Function.Embedding.trans (Fin.natAddEmb m).toEmbedding
      (Function.Embedding.trans (Equiv.toEmbedding (Fin.castIso ⋯).toEquiv) y') =
    Function.Embedding.trans (Equiv.toEmbedding z) (subtype s)
g : M
hg : g • x' = y'
this✝ : g ∈ fixingSubgroup M s
i : Fin m
this : ↑(y i) = (Function.Embedding.trans y (subtype sᶜ)) i
⊢ { val := g, property := this✝ } • ↑(x i) = (Function.Embedding.trans y (subtype sᶜ)) i

State before:
case h.h.a
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
h : IsMultiplyPretransitive M α n
hmn : n = m + Set.ncard s
hs : PartENat.card ↑s = ↑(Set.ncard s)
x y : Fin m ↪ ↥(SubMulAction.ofFixingSubgroup M s)
z : Fin (Set.ncard s) ≃ ↑s
x' : Fin n ↪ α
hx'1 : Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding x' = Function.Embedding.trans x (subtype sᶜ)
hx'2 :
  Function.Embedding.trans (Fin.natAddEmb m).toEmbedding
      (Function.Embedding.trans (Equiv.toEmbedding (Fin.castIso ⋯).toEquiv) x') =
    Function.Embedding.trans (Equiv.toEmbedding z) (subtype s)
y' : Fin n ↪ α
hy'1 : Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding y' = Function.Embedding.trans y (subtype sᶜ)
hy'2 :
  Function.Embedding.trans (Fin.natAddEmb m).toEmbedding
      (Function.Embedding.trans (Equiv.toEmbedding (Fin.castIso ⋯).toEquiv) y') =
    Function.Embedding.trans (Equiv.toEmbedding z) (subtype s)
g : M
hg : g • x' = y'
this✝ : g ∈ fixingSubgroup M s
i : Fin m
this : ↑(y i) = (Function.Embedding.trans y (subtype sᶜ)) i
⊢ { val := g, property := this✝ } • ↑(x i) = (Function.Embedding.trans y (subtype sᶜ)) i
Tactic:
have : (x i : α) = (x.trans (subtype (sᶜ)) i : α) := by
  simp only [trans_apply, Function.Embedding.coe_subtype]
  rfl
State after:
case h.h.a
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
h : IsMultiplyPretransitive M α n
hmn : n = m + Set.ncard s
hs : PartENat.card ↑s = ↑(Set.ncard s)
x y : Fin m ↪ ↥(SubMulAction.ofFixingSubgroup M s)
z : Fin (Set.ncard s) ≃ ↑s
x' : Fin n ↪ α
hx'1 : Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding x' = Function.Embedding.trans x (subtype sᶜ)
hx'2 :
  Function.Embedding.trans (Fin.natAddEmb m).toEmbedding
      (Function.Embedding.trans (Equiv.toEmbedding (Fin.castIso ⋯).toEquiv) x') =
    Function.Embedding.trans (Equiv.toEmbedding z) (subtype s)
y' : Fin n ↪ α
hy'1 : Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding y' = Function.Embedding.trans y (subtype sᶜ)
hy'2 :
  Function.Embedding.trans (Fin.natAddEmb m).toEmbedding
      (Function.Embedding.trans (Equiv.toEmbedding (Fin.castIso ⋯).toEquiv) y') =
    Function.Embedding.trans (Equiv.toEmbedding z) (subtype s)
g : M
hg : g • x' = y'
this✝¹ : g ∈ fixingSubgroup M s
i : Fin m
this✝ : ↑(y i) = (Function.Embedding.trans y (subtype sᶜ)) i
this : ↑(x i) = (Function.Embedding.trans x (subtype sᶜ)) i
⊢ { val := g, property := this✝¹ } • ↑(x i) = (Function.Embedding.trans y (subtype sᶜ)) i

State before:
case h.h.a
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
h : IsMultiplyPretransitive M α n
hmn : n = m + Set.ncard s
hs : PartENat.card ↑s = ↑(Set.ncard s)
x y : Fin m ↪ ↥(SubMulAction.ofFixingSubgroup M s)
z : Fin (Set.ncard s) ≃ ↑s
x' : Fin n ↪ α
hx'1 : Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding x' = Function.Embedding.trans x (subtype sᶜ)
hx'2 :
  Function.Embedding.trans (Fin.natAddEmb m).toEmbedding
      (Function.Embedding.trans (Equiv.toEmbedding (Fin.castIso ⋯).toEquiv) x') =
    Function.Embedding.trans (Equiv.toEmbedding z) (subtype s)
y' : Fin n ↪ α
hy'1 : Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding y' = Function.Embedding.trans y (subtype sᶜ)
hy'2 :
  Function.Embedding.trans (Fin.natAddEmb m).toEmbedding
      (Function.Embedding.trans (Equiv.toEmbedding (Fin.castIso ⋯).toEquiv) y') =
    Function.Embedding.trans (Equiv.toEmbedding z) (subtype s)
g : M
hg : g • x' = y'
this✝¹ : g ∈ fixingSubgroup M s
i : Fin m
this✝ : ↑(y i) = (Function.Embedding.trans y (subtype sᶜ)) i
this : ↑(x i) = (Function.Embedding.trans x (subtype sᶜ)) i
⊢ { val := g, property := this✝¹ } • ↑(x i) = (Function.Embedding.trans y (subtype sᶜ)) i
Tactic:
rw [this]
State after:
case h.h.a
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
h : IsMultiplyPretransitive M α n
hmn : n = m + Set.ncard s
hs : PartENat.card ↑s = ↑(Set.ncard s)
x y : Fin m ↪ ↥(SubMulAction.ofFixingSubgroup M s)
z : Fin (Set.ncard s) ≃ ↑s
x' : Fin n ↪ α
hx'1 : Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding x' = Function.Embedding.trans x (subtype sᶜ)
hx'2 :
  Function.Embedding.trans (Fin.natAddEmb m).toEmbedding
      (Function.Embedding.trans (Equiv.toEmbedding (Fin.castIso ⋯).toEquiv) x') =
    Function.Embedding.trans (Equiv.toEmbedding z) (subtype s)
y' : Fin n ↪ α
hy'1 : Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding y' = Function.Embedding.trans y (subtype sᶜ)
hy'2 :
  Function.Embedding.trans (Fin.natAddEmb m).toEmbedding
      (Function.Embedding.trans (Equiv.toEmbedding (Fin.castIso ⋯).toEquiv) y') =
    Function.Embedding.trans (Equiv.toEmbedding z) (subtype s)
g : M
hg : g • x' = y'
this✝¹ : g ∈ fixingSubgroup M s
i : Fin m
this✝ : ↑(y i) = (Function.Embedding.trans y (subtype sᶜ)) i
this : ↑(x i) = (Function.Embedding.trans x (subtype sᶜ)) i
⊢ { val := g, property := this✝¹ } • (Function.Embedding.trans x (subtype sᶜ)) i =
    (Function.Embedding.trans y (subtype sᶜ)) i

State before:
case h.h.a
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
h : IsMultiplyPretransitive M α n
hmn : n = m + Set.ncard s
hs : PartENat.card ↑s = ↑(Set.ncard s)
x y : Fin m ↪ ↥(SubMulAction.ofFixingSubgroup M s)
z : Fin (Set.ncard s) ≃ ↑s
x' : Fin n ↪ α
hx'1 : Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding x' = Function.Embedding.trans x (subtype sᶜ)
hx'2 :
  Function.Embedding.trans (Fin.natAddEmb m).toEmbedding
      (Function.Embedding.trans (Equiv.toEmbedding (Fin.castIso ⋯).toEquiv) x') =
    Function.Embedding.trans (Equiv.toEmbedding z) (subtype s)
y' : Fin n ↪ α
hy'1 : Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding y' = Function.Embedding.trans y (subtype sᶜ)
hy'2 :
  Function.Embedding.trans (Fin.natAddEmb m).toEmbedding
      (Function.Embedding.trans (Equiv.toEmbedding (Fin.castIso ⋯).toEquiv) y') =
    Function.Embedding.trans (Equiv.toEmbedding z) (subtype s)
g : M
hg : g • x' = y'
this✝¹ : g ∈ fixingSubgroup M s
i : Fin m
this✝ : ↑(y i) = (Function.Embedding.trans y (subtype sᶜ)) i
this : ↑(x i) = (Function.Embedding.trans x (subtype sᶜ)) i
⊢ { val := g, property := this✝¹ } • (Function.Embedding.trans x (subtype sᶜ)) i =
    (Function.Embedding.trans y (subtype sᶜ)) i
Tactic:
rw [← Function.Embedding.ext_iff] at hx'1 hy'1
State after:
case h.h.a
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
h : IsMultiplyPretransitive M α n
hmn : n = m + Set.ncard s
hs : PartENat.card ↑s = ↑(Set.ncard s)
x y : Fin m ↪ ↥(SubMulAction.ofFixingSubgroup M s)
z : Fin (Set.ncard s) ≃ ↑s
x' : Fin n ↪ α
hx'1 :
  ∀ (x_1 : Fin m),
    (Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding x') x_1 = (Function.Embedding.trans x (subtype sᶜ)) x_1
hx'2 :
  Function.Embedding.trans (Fin.natAddEmb m).toEmbedding
      (Function.Embedding.trans (Equiv.toEmbedding (Fin.castIso ⋯).toEquiv) x') =
    Function.Embedding.trans (Equiv.toEmbedding z) (subtype s)
y' : Fin n ↪ α
hy'1 :
  ∀ (x : Fin m),
    (Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding y') x = (Function.Embedding.trans y (subtype sᶜ)) x
hy'2 :
  Function.Embedding.trans (Fin.natAddEmb m).toEmbedding
      (Function.Embedding.trans (Equiv.toEmbedding (Fin.castIso ⋯).toEquiv) y') =
    Function.Embedding.trans (Equiv.toEmbedding z) (subtype s)
g : M
hg : g • x' = y'
this✝¹ : g ∈ fixingSubgroup M s
i : Fin m
this✝ : ↑(y i) = (Function.Embedding.trans y (subtype sᶜ)) i
this : ↑(x i) = (Function.Embedding.trans x (subtype sᶜ)) i
⊢ { val := g, property := this✝¹ } • (Function.Embedding.trans x (subtype sᶜ)) i =
    (Function.Embedding.trans y (subtype sᶜ)) i

State before:
case h.h.a
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
h : IsMultiplyPretransitive M α n
hmn : n = m + Set.ncard s
hs : PartENat.card ↑s = ↑(Set.ncard s)
x y : Fin m ↪ ↥(SubMulAction.ofFixingSubgroup M s)
z : Fin (Set.ncard s) ≃ ↑s
x' : Fin n ↪ α
hx'1 :
  ∀ (x_1 : Fin m),
    (Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding x') x_1 = (Function.Embedding.trans x (subtype sᶜ)) x_1
hx'2 :
  Function.Embedding.trans (Fin.natAddEmb m).toEmbedding
      (Function.Embedding.trans (Equiv.toEmbedding (Fin.castIso ⋯).toEquiv) x') =
    Function.Embedding.trans (Equiv.toEmbedding z) (subtype s)
y' : Fin n ↪ α
hy'1 :
  ∀ (x : Fin m),
    (Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding y') x = (Function.Embedding.trans y (subtype sᶜ)) x
hy'2 :
  Function.Embedding.trans (Fin.natAddEmb m).toEmbedding
      (Function.Embedding.trans (Equiv.toEmbedding (Fin.castIso ⋯).toEquiv) y') =
    Function.Embedding.trans (Equiv.toEmbedding z) (subtype s)
g : M
hg : g • x' = y'
this✝¹ : g ∈ fixingSubgroup M s
i : Fin m
this✝ : ↑(y i) = (Function.Embedding.trans y (subtype sᶜ)) i
this : ↑(x i) = (Function.Embedding.trans x (subtype sᶜ)) i
⊢ { val := g, property := this✝¹ } • (Function.Embedding.trans x (subtype sᶜ)) i =
    (Function.Embedding.trans y (subtype sᶜ)) i
Tactic:
simp_rw [← hy'1 i, ← hx'1 i, ← hg]
State after:
case h.h.a
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
h : IsMultiplyPretransitive M α n
hmn : n = m + Set.ncard s
hs : PartENat.card ↑s = ↑(Set.ncard s)
x y : Fin m ↪ ↥(SubMulAction.ofFixingSubgroup M s)
z : Fin (Set.ncard s) ≃ ↑s
x' : Fin n ↪ α
hx'1 :
  ∀ (x_1 : Fin m),
    (Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding x') x_1 = (Function.Embedding.trans x (subtype sᶜ)) x_1
hx'2 :
  Function.Embedding.trans (Fin.natAddEmb m).toEmbedding
      (Function.Embedding.trans (Equiv.toEmbedding (Fin.castIso ⋯).toEquiv) x') =
    Function.Embedding.trans (Equiv.toEmbedding z) (subtype s)
y' : Fin n ↪ α
hy'1 :
  ∀ (x : Fin m),
    (Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding y') x = (Function.Embedding.trans y (subtype sᶜ)) x
hy'2 :
  Function.Embedding.trans (Fin.natAddEmb m).toEmbedding
      (Function.Embedding.trans (Equiv.toEmbedding (Fin.castIso ⋯).toEquiv) y') =
    Function.Embedding.trans (Equiv.toEmbedding z) (subtype s)
g : M
hg : g • x' = y'
this✝¹ : g ∈ fixingSubgroup M s
i : Fin m
this✝ : ↑(y i) = (Function.Embedding.trans y (subtype sᶜ)) i
this : ↑(x i) = (Function.Embedding.trans x (subtype sᶜ)) i
⊢ { val := g, property := this✝¹ } • (Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding x') i =
    (Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding (g • x')) i

State before:
case h.h.a
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
h : IsMultiplyPretransitive M α n
hmn : n = m + Set.ncard s
hs : PartENat.card ↑s = ↑(Set.ncard s)
x y : Fin m ↪ ↥(SubMulAction.ofFixingSubgroup M s)
z : Fin (Set.ncard s) ≃ ↑s
x' : Fin n ↪ α
hx'1 :
  ∀ (x_1 : Fin m),
    (Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding x') x_1 = (Function.Embedding.trans x (subtype sᶜ)) x_1
hx'2 :
  Function.Embedding.trans (Fin.natAddEmb m).toEmbedding
      (Function.Embedding.trans (Equiv.toEmbedding (Fin.castIso ⋯).toEquiv) x') =
    Function.Embedding.trans (Equiv.toEmbedding z) (subtype s)
y' : Fin n ↪ α
hy'1 :
  ∀ (x : Fin m),
    (Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding y') x = (Function.Embedding.trans y (subtype sᶜ)) x
hy'2 :
  Function.Embedding.trans (Fin.natAddEmb m).toEmbedding
      (Function.Embedding.trans (Equiv.toEmbedding (Fin.castIso ⋯).toEquiv) y') =
    Function.Embedding.trans (Equiv.toEmbedding z) (subtype s)
g : M
hg : g • x' = y'
this✝¹ : g ∈ fixingSubgroup M s
i : Fin m
this✝ : ↑(y i) = (Function.Embedding.trans y (subtype sᶜ)) i
this : ↑(x i) = (Function.Embedding.trans x (subtype sᶜ)) i
⊢ { val := g, property := this✝¹ } • (Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding x') i =
    (Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding (g • x')) i
Tactic:
simp only [trans_apply, smul_apply, RelEmbedding.coe_toEmbedding]
State after:
case h.h.a
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
h : IsMultiplyPretransitive M α n
hmn : n = m + Set.ncard s
hs : PartENat.card ↑s = ↑(Set.ncard s)
x y : Fin m ↪ ↥(SubMulAction.ofFixingSubgroup M s)
z : Fin (Set.ncard s) ≃ ↑s
x' : Fin n ↪ α
hx'1 :
  ∀ (x_1 : Fin m),
    (Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding x') x_1 = (Function.Embedding.trans x (subtype sᶜ)) x_1
hx'2 :
  Function.Embedding.trans (Fin.natAddEmb m).toEmbedding
      (Function.Embedding.trans (Equiv.toEmbedding (Fin.castIso ⋯).toEquiv) x') =
    Function.Embedding.trans (Equiv.toEmbedding z) (subtype s)
y' : Fin n ↪ α
hy'1 :
  ∀ (x : Fin m),
    (Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding y') x = (Function.Embedding.trans y (subtype sᶜ)) x
hy'2 :
  Function.Embedding.trans (Fin.natAddEmb m).toEmbedding
      (Function.Embedding.trans (Equiv.toEmbedding (Fin.castIso ⋯).toEquiv) y') =
    Function.Embedding.trans (Equiv.toEmbedding z) (subtype s)
g : M
hg : g • x' = y'
this✝¹ : g ∈ fixingSubgroup M s
i : Fin m
this✝ : ↑(y i) = (Function.Embedding.trans y (subtype sᶜ)) i
this : ↑(x i) = (Function.Embedding.trans x (subtype sᶜ)) i
⊢ { val := g, property := this✝¹ } • x' ((Fin.castLEEmb ⋯) i) = g • x' ((Fin.castLEEmb ⋯) i)

State before:
case h.h.a
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
h : IsMultiplyPretransitive M α n
hmn : n = m + Set.ncard s
hs : PartENat.card ↑s = ↑(Set.ncard s)
x y : Fin m ↪ ↥(SubMulAction.ofFixingSubgroup M s)
z : Fin (Set.ncard s) ≃ ↑s
x' : Fin n ↪ α
hx'1 :
  ∀ (x_1 : Fin m),
    (Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding x') x_1 = (Function.Embedding.trans x (subtype sᶜ)) x_1
hx'2 :
  Function.Embedding.trans (Fin.natAddEmb m).toEmbedding
      (Function.Embedding.trans (Equiv.toEmbedding (Fin.castIso ⋯).toEquiv) x') =
    Function.Embedding.trans (Equiv.toEmbedding z) (subtype s)
y' : Fin n ↪ α
hy'1 :
  ∀ (x : Fin m),
    (Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding y') x = (Function.Embedding.trans y (subtype sᶜ)) x
hy'2 :
  Function.Embedding.trans (Fin.natAddEmb m).toEmbedding
      (Function.Embedding.trans (Equiv.toEmbedding (Fin.castIso ⋯).toEquiv) y') =
    Function.Embedding.trans (Equiv.toEmbedding z) (subtype s)
g : M
hg : g • x' = y'
this✝¹ : g ∈ fixingSubgroup M s
i : Fin m
this✝ : ↑(y i) = (Function.Embedding.trans y (subtype sᶜ)) i
this : ↑(x i) = (Function.Embedding.trans x (subtype sᶜ)) i
⊢ { val := g, property := this✝¹ } • x' ((Fin.castLEEmb ⋯) i) = g • x' ((Fin.castLEEmb ⋯) i)
Tactic:
rfl
State after:
no goals

State before:
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
h : IsMultiplyPretransitive M α n
hmn : n = m + Set.ncard s
hs : PartENat.card ↑s = ↑(Set.ncard s)
x y : Fin m ↪ ↥(SubMulAction.ofFixingSubgroup M s)
z : Fin (Set.ncard s) ≃ ↑s
x' : Fin n ↪ α
hx'1 : Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding x' = Function.Embedding.trans x (subtype sᶜ)
hx'2 :
  Function.Embedding.trans (Fin.natAddEmb m).toEmbedding
      (Function.Embedding.trans (Equiv.toEmbedding (Fin.castIso ⋯).toEquiv) x') =
    Function.Embedding.trans (Equiv.toEmbedding z) (subtype s)
y' : Fin n ↪ α
hy'1 : Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding y' = Function.Embedding.trans y (subtype sᶜ)
hy'2 :
  Function.Embedding.trans (Fin.natAddEmb m).toEmbedding
      (Function.Embedding.trans (Equiv.toEmbedding (Fin.castIso ⋯).toEquiv) y') =
    Function.Embedding.trans (Equiv.toEmbedding z) (subtype s)
g : M
hg : g • x' = y'
this : g ∈ fixingSubgroup M s
i : Fin m
⊢ ↑(y i) = (Function.Embedding.trans y (subtype sᶜ)) i
Tactic:
simp only [trans_apply, Function.Embedding.coe_subtype]
State after:
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
h : IsMultiplyPretransitive M α n
hmn : n = m + Set.ncard s
hs : PartENat.card ↑s = ↑(Set.ncard s)
x y : Fin m ↪ ↥(SubMulAction.ofFixingSubgroup M s)
z : Fin (Set.ncard s) ≃ ↑s
x' : Fin n ↪ α
hx'1 : Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding x' = Function.Embedding.trans x (subtype sᶜ)
hx'2 :
  Function.Embedding.trans (Fin.natAddEmb m).toEmbedding
      (Function.Embedding.trans (Equiv.toEmbedding (Fin.castIso ⋯).toEquiv) x') =
    Function.Embedding.trans (Equiv.toEmbedding z) (subtype s)
y' : Fin n ↪ α
hy'1 : Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding y' = Function.Embedding.trans y (subtype sᶜ)
hy'2 :
  Function.Embedding.trans (Fin.natAddEmb m).toEmbedding
      (Function.Embedding.trans (Equiv.toEmbedding (Fin.castIso ⋯).toEquiv) y') =
    Function.Embedding.trans (Equiv.toEmbedding z) (subtype s)
g : M
hg : g • x' = y'
this : g ∈ fixingSubgroup M s
i : Fin m
⊢ ↑(y i) = (subtype sᶜ) (y i)

State before:
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
h : IsMultiplyPretransitive M α n
hmn : n = m + Set.ncard s
hs : PartENat.card ↑s = ↑(Set.ncard s)
x y : Fin m ↪ ↥(SubMulAction.ofFixingSubgroup M s)
z : Fin (Set.ncard s) ≃ ↑s
x' : Fin n ↪ α
hx'1 : Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding x' = Function.Embedding.trans x (subtype sᶜ)
hx'2 :
  Function.Embedding.trans (Fin.natAddEmb m).toEmbedding
      (Function.Embedding.trans (Equiv.toEmbedding (Fin.castIso ⋯).toEquiv) x') =
    Function.Embedding.trans (Equiv.toEmbedding z) (subtype s)
y' : Fin n ↪ α
hy'1 : Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding y' = Function.Embedding.trans y (subtype sᶜ)
hy'2 :
  Function.Embedding.trans (Fin.natAddEmb m).toEmbedding
      (Function.Embedding.trans (Equiv.toEmbedding (Fin.castIso ⋯).toEquiv) y') =
    Function.Embedding.trans (Equiv.toEmbedding z) (subtype s)
g : M
hg : g • x' = y'
this : g ∈ fixingSubgroup M s
i : Fin m
⊢ ↑(y i) = (subtype sᶜ) (y i)
Tactic:
rfl
State after:
no goals

State before:
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
h : IsMultiplyPretransitive M α n
hmn : n = m + Set.ncard s
hs : PartENat.card ↑s = ↑(Set.ncard s)
x y : Fin m ↪ ↥(SubMulAction.ofFixingSubgroup M s)
z : Fin (Set.ncard s) ≃ ↑s
x' : Fin n ↪ α
hx'1 : Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding x' = Function.Embedding.trans x (subtype sᶜ)
hx'2 :
  Function.Embedding.trans (Fin.natAddEmb m).toEmbedding
      (Function.Embedding.trans (Equiv.toEmbedding (Fin.castIso ⋯).toEquiv) x') =
    Function.Embedding.trans (Equiv.toEmbedding z) (subtype s)
y' : Fin n ↪ α
hy'1 : Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding y' = Function.Embedding.trans y (subtype sᶜ)
hy'2 :
  Function.Embedding.trans (Fin.natAddEmb m).toEmbedding
      (Function.Embedding.trans (Equiv.toEmbedding (Fin.castIso ⋯).toEquiv) y') =
    Function.Embedding.trans (Equiv.toEmbedding z) (subtype s)
g : M
hg : g • x' = y'
this✝ : g ∈ fixingSubgroup M s
i : Fin m
this : ↑(y i) = (Function.Embedding.trans y (subtype sᶜ)) i
⊢ ↑(x i) = (Function.Embedding.trans x (subtype sᶜ)) i
Tactic:
simp only [trans_apply, Function.Embedding.coe_subtype]
State after:
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
h : IsMultiplyPretransitive M α n
hmn : n = m + Set.ncard s
hs : PartENat.card ↑s = ↑(Set.ncard s)
x y : Fin m ↪ ↥(SubMulAction.ofFixingSubgroup M s)
z : Fin (Set.ncard s) ≃ ↑s
x' : Fin n ↪ α
hx'1 : Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding x' = Function.Embedding.trans x (subtype sᶜ)
hx'2 :
  Function.Embedding.trans (Fin.natAddEmb m).toEmbedding
      (Function.Embedding.trans (Equiv.toEmbedding (Fin.castIso ⋯).toEquiv) x') =
    Function.Embedding.trans (Equiv.toEmbedding z) (subtype s)
y' : Fin n ↪ α
hy'1 : Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding y' = Function.Embedding.trans y (subtype sᶜ)
hy'2 :
  Function.Embedding.trans (Fin.natAddEmb m).toEmbedding
      (Function.Embedding.trans (Equiv.toEmbedding (Fin.castIso ⋯).toEquiv) y') =
    Function.Embedding.trans (Equiv.toEmbedding z) (subtype s)
g : M
hg : g • x' = y'
this✝ : g ∈ fixingSubgroup M s
i : Fin m
this : ↑(y i) = (Function.Embedding.trans y (subtype sᶜ)) i
⊢ ↑(x i) = (subtype sᶜ) (x i)

State before:
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
h : IsMultiplyPretransitive M α n
hmn : n = m + Set.ncard s
hs : PartENat.card ↑s = ↑(Set.ncard s)
x y : Fin m ↪ ↥(SubMulAction.ofFixingSubgroup M s)
z : Fin (Set.ncard s) ≃ ↑s
x' : Fin n ↪ α
hx'1 : Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding x' = Function.Embedding.trans x (subtype sᶜ)
hx'2 :
  Function.Embedding.trans (Fin.natAddEmb m).toEmbedding
      (Function.Embedding.trans (Equiv.toEmbedding (Fin.castIso ⋯).toEquiv) x') =
    Function.Embedding.trans (Equiv.toEmbedding z) (subtype s)
y' : Fin n ↪ α
hy'1 : Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding y' = Function.Embedding.trans y (subtype sᶜ)
hy'2 :
  Function.Embedding.trans (Fin.natAddEmb m).toEmbedding
      (Function.Embedding.trans (Equiv.toEmbedding (Fin.castIso ⋯).toEquiv) y') =
    Function.Embedding.trans (Equiv.toEmbedding z) (subtype s)
g : M
hg : g • x' = y'
this✝ : g ∈ fixingSubgroup M s
i : Fin m
this : ↑(y i) = (Function.Embedding.trans y (subtype sᶜ)) i
⊢ ↑(x i) = (subtype sᶜ) (x i)
Tactic:
rfl
State after:
no goals

State before:
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
h : IsMultiplyPretransitive M α n
hmn : n = m + Set.ncard s
hs : PartENat.card ↑s = ↑(Set.ncard s)
x y : Fin m ↪ ↥(SubMulAction.ofFixingSubgroup M s)
z : Fin (Set.ncard s) ≃ ↑s
x' : Fin n ↪ α
hx'1 : Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding x' = Function.Embedding.trans x (subtype sᶜ)
hx'2 :
  Function.Embedding.trans (Fin.natAddEmb m).toEmbedding
      (Function.Embedding.trans (Equiv.toEmbedding (Fin.castIso ⋯).toEquiv) x') =
    Function.Embedding.trans (Equiv.toEmbedding z) (subtype s)
y' : Fin n ↪ α
hy'1 : Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding y' = Function.Embedding.trans y (subtype sᶜ)
hy'2 :
  Function.Embedding.trans (Fin.natAddEmb m).toEmbedding
      (Function.Embedding.trans (Equiv.toEmbedding (Fin.castIso ⋯).toEquiv) y') =
    Function.Embedding.trans (Equiv.toEmbedding z) (subtype s)
g : M
hg : g • x' = y'
a : ↑s
⊢ (Function.Embedding.trans (Equiv.toEmbedding z) (subtype s)) (z.symm a) = ↑a
Tactic:
simp only [trans_apply, Equiv.toEmbedding_apply, Equiv.apply_symm_apply,
  Function.Embedding.coe_subtype]
State after:
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
h : IsMultiplyPretransitive M α n
hmn : n = m + Set.ncard s
hs : PartENat.card ↑s = ↑(Set.ncard s)
x y : Fin m ↪ ↥(SubMulAction.ofFixingSubgroup M s)
z : Fin (Set.ncard s) ≃ ↑s
x' : Fin n ↪ α
hx'1 : Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding x' = Function.Embedding.trans x (subtype sᶜ)
hx'2 :
  Function.Embedding.trans (Fin.natAddEmb m).toEmbedding
      (Function.Embedding.trans (Equiv.toEmbedding (Fin.castIso ⋯).toEquiv) x') =
    Function.Embedding.trans (Equiv.toEmbedding z) (subtype s)
y' : Fin n ↪ α
hy'1 : Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding y' = Function.Embedding.trans y (subtype sᶜ)
hy'2 :
  Function.Embedding.trans (Fin.natAddEmb m).toEmbedding
      (Function.Embedding.trans (Equiv.toEmbedding (Fin.castIso ⋯).toEquiv) y') =
    Function.Embedding.trans (Equiv.toEmbedding z) (subtype s)
g : M
hg : g • x' = y'
a : ↑s
⊢ (subtype s) a = ↑a

State before:
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
h : IsMultiplyPretransitive M α n
hmn : n = m + Set.ncard s
hs : PartENat.card ↑s = ↑(Set.ncard s)
x y : Fin m ↪ ↥(SubMulAction.ofFixingSubgroup M s)
z : Fin (Set.ncard s) ≃ ↑s
x' : Fin n ↪ α
hx'1 : Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding x' = Function.Embedding.trans x (subtype sᶜ)
hx'2 :
  Function.Embedding.trans (Fin.natAddEmb m).toEmbedding
      (Function.Embedding.trans (Equiv.toEmbedding (Fin.castIso ⋯).toEquiv) x') =
    Function.Embedding.trans (Equiv.toEmbedding z) (subtype s)
y' : Fin n ↪ α
hy'1 : Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding y' = Function.Embedding.trans y (subtype sᶜ)
hy'2 :
  Function.Embedding.trans (Fin.natAddEmb m).toEmbedding
      (Function.Embedding.trans (Equiv.toEmbedding (Fin.castIso ⋯).toEquiv) y') =
    Function.Embedding.trans (Equiv.toEmbedding z) (subtype s)
g : M
hg : g • x' = y'
a : ↑s
⊢ (subtype s) a = ↑a
Tactic:
rfl
State after:
no goals