internlm/Lean-Github huggingface dataset:
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 (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]
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 (Fin.natAddEmb m).toEmbedding
        (Function.Embedding.trans (Equiv.toEmbedding (Fin.castIso ⋯).toEquiv) (g • x')))
      (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 (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]
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
⊢ 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]
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
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⟩
Proof 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
Theorem: MulAction.remaining_transitivity
Proof 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
Proof 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)
Theorem: MulAction.remaining_transitivity
Proof 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]
Proof 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)
Theorem: MulAction.remaining_transitivity
Proof 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
Proof 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)
Theorem: MulAction.remaining_transitivity
Proof 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]
Proof 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
Theorem: MulAction.remaining_transitivity
Proof 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
Proof 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
Theorem: MulAction.remaining_transitivity
Proof 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]
Proof 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
Theorem: MulAction.remaining_transitivity
Proof 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
Proof 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