internlm/Lean-Github huggingface dataset:
Theorem: MulAction.stabilizer.isMultiplyPretransitive
Proof state before:
case h.h.mk.inr
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
a : α
hn : IsMultiplyPretransitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
x : Fin (succ n) ↪ α
gx : M
x1 : Fin n ↪ ↥(SubMulAction.ofStabilizer M a)
hgx :
  Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding (gx • x) =
    Function.Embedding.trans x1 (subtype fun x => x ∈ SubMulAction.ofStabilizer M a)
hga : gx • x { val := n, isLt := ⋯ } = a
y : Fin (succ n) ↪ α
gy : M
y1 : Fin n ↪ ↥(SubMulAction.ofStabilizer M a)
hgy :
  Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding (gy • y) =
    Function.Embedding.trans y1 (subtype fun x => x ∈ SubMulAction.ofStabilizer M a)
hgb : gy • y { val := n, isLt := ⋯ } = a
hna_eq : ∀ (x y : Fin n ↪ ↥(SubMulAction.ofStabilizer M a)), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
g : ↥(stabilizer M a)
hg : g • x1 = y1
i : ℕ
hi : i < succ n
hi' : i = n
⊢ ↑g • a = a
Tactic:
rw [← mem_stabilizer_iff]
Proof state after:
case h.h.mk.inr
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
a : α
hn : IsMultiplyPretransitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
x : Fin (succ n) ↪ α
gx : M
x1 : Fin n ↪ ↥(SubMulAction.ofStabilizer M a)
hgx :
  Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding (gx • x) =
    Function.Embedding.trans x1 (subtype fun x => x ∈ SubMulAction.ofStabilizer M a)
hga : gx • x { val := n, isLt := ⋯ } = a
y : Fin (succ n) ↪ α
gy : M
y1 : Fin n ↪ ↥(SubMulAction.ofStabilizer M a)
hgy :
  Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding (gy • y) =
    Function.Embedding.trans y1 (subtype fun x => x ∈ SubMulAction.ofStabilizer M a)
hgb : gy • y { val := n, isLt := ⋯ } = a
hna_eq : ∀ (x y : Fin n ↪ ↥(SubMulAction.ofStabilizer M a)), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
g : ↥(stabilizer M a)
hg : g • x1 = y1
i : ℕ
hi : i < succ n
hi' : i = n
⊢ ↑g ∈ stabilizer M a
Theorem: MulAction.stabilizer.isMultiplyPretransitive
Proof state before:
case h.h.mk.inr
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
a : α
hn : IsMultiplyPretransitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
x : Fin (succ n) ↪ α
gx : M
x1 : Fin n ↪ ↥(SubMulAction.ofStabilizer M a)
hgx :
  Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding (gx • x) =
    Function.Embedding.trans x1 (subtype fun x => x ∈ SubMulAction.ofStabilizer M a)
hga : gx • x { val := n, isLt := ⋯ } = a
y : Fin (succ n) ↪ α
gy : M
y1 : Fin n ↪ ↥(SubMulAction.ofStabilizer M a)
hgy :
  Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding (gy • y) =
    Function.Embedding.trans y1 (subtype fun x => x ∈ SubMulAction.ofStabilizer M a)
hgb : gy • y { val := n, isLt := ⋯ } = a
hna_eq : ∀ (x y : Fin n ↪ ↥(SubMulAction.ofStabilizer M a)), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
g : ↥(stabilizer M a)
hg : g • x1 = y1
i : ℕ
hi : i < succ n
hi' : i = n
⊢ ↑g ∈ stabilizer M a
Tactic:
exact SetLike.coe_mem g
Proof state after:
no goals
Theorem: MulAction.remaining_transitivity
Proof 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]
Proof 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
Theorem: MulAction.remaining_transitivity
Proof 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
Proof 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
Theorem: MulAction.remaining_transitivity
Proof 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
Proof 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
Theorem: MulAction.remaining_transitivity
Proof 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
Proof 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
Theorem: MulAction.remaining_transitivity
Proof 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
Proof 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
Theorem: MulAction.remaining_transitivity
Proof 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
Proof 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
Theorem: MulAction.remaining_transitivity
Proof 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'
Proof 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
Theorem: MulAction.remaining_transitivity
Proof 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
Proof 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
Theorem: MulAction.remaining_transitivity
Proof 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
Proof 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
Theorem: MulAction.remaining_transitivity
Proof 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
Proof 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
Theorem: MulAction.remaining_transitivity
Proof 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]
Proof 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)
Theorem: MulAction.remaining_transitivity
Proof 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]
Proof 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)