internlm/Lean-Github huggingface dataset:
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 :
  ∀ (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]
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 (Fin.castLEEmb ⋯).toEmbedding x') i =
    (Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding (g • x')) 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 :
  ∀ (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]
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✝¹ } • x' ((Fin.castLEEmb ⋯) i) = g • x' ((Fin.castLEEmb ⋯) 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 :
  ∀ (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
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
i : Fin m
⊢ ↑(y i) = (Function.Embedding.trans y (subtype sᶜ)) i
Tactic:
simp only [trans_apply, Function.Embedding.coe_subtype]
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)
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)
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
i : Fin m
⊢ ↑(y i) = (subtype sᶜ) (y i)
Tactic:
rfl
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
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]
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)
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)
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
i : Fin m
this : ↑(y i) = (Function.Embedding.trans y (subtype sᶜ)) i
⊢ ↑(x i) = (subtype sᶜ) (x i)
Tactic:
rfl
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'
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]
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)
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
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'
a : ↑s
⊢ (subtype s) a = ↑a
Tactic:
rfl
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 : m + Set.ncard s ≤ n
hn : ↑n ≤ PartENat.card α
⊢ IsMultiplyPretransitive (↥(fixingSubgroup M s)) (↥(SubMulAction.ofFixingSubgroup M s)) m
Tactic:
apply remaining_transitivity
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 : m + Set.ncard s ≤ n
hn : ↑n ≤ PartENat.card α
⊢ IsMultiplyPretransitive M α ?n

case hmn
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 : m + Set.ncard s ≤ n
hn : ↑n ≤ PartENat.card α
⊢ ?n = m + Set.ncard s

case n
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 : m + Set.ncard s ≤ n
hn : ↑n ≤ PartENat.card α
⊢ ℕ
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 : m + Set.ncard s ≤ n
hn : ↑n ≤ PartENat.card α
⊢ IsMultiplyPretransitive M α ?n

case hmn
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 : m + Set.ncard s ≤ n
hn : ↑n ≤ PartENat.card α
⊢ ?n = m + Set.ncard s

case n
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 : m + Set.ncard s ≤ n
hn : ↑n ≤ PartENat.card α
⊢ ℕ
Tactic:
exact isMultiplyPretransitive_of_higher M α h hmn hn
Proof state after:
case hmn
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 : m + Set.ncard s ≤ n
hn : ↑n ≤ PartENat.card α
⊢ m + Set.ncard s = m + Set.ncard s
Theorem: MulAction.remaining_transitivity'
Proof state before:
case hmn
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 : m + Set.ncard s ≤ n
hn : ↑n ≤ PartENat.card α
⊢ m + Set.ncard s = m + Set.ncard s
Tactic:
rfl
Proof state after:
no goals
Theorem: Set.ncard_le_fintype_card
Proof state before:
M : Type ?u.179009
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
s : Set α
⊢ Set.ncard s ≤ Fintype.card α
Tactic:
rw [← Nat.card_eq_fintype_card, ← Set.ncard_univ]
Proof state after:
M : Type ?u.179009
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
s : Set α
⊢ Set.ncard s ≤ Set.ncard Set.univ
Theorem: Set.ncard_le_fintype_card
Proof state before:
M : Type ?u.179009
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
s : Set α
⊢ Set.ncard s ≤ Set.ncard Set.univ
Tactic:
exact Set.ncard_le_ncard s.subset_univ
Proof state after:
no goals
Theorem: MulAction.IsMultiplyPretransitive.index_of_fixing_subgroup_aux
Proof state before:
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
k : ℕ
hmk : IsMultiplyPretransitive M α k
s : Set α
hs : Set.ncard s = k
⊢ Subgroup.index (fixingSubgroup M s) * (Fintype.card α - Set.ncard s)! = (Fintype.card α)!
Tactic:
revert M α
Proof state after:
k : ℕ
⊢ ∀ (M : Type u_2) (α : Type u_1) [inst : Group M] [inst_1 : MulAction M α] [inst_2 : Fintype α],
    IsMultiplyPretransitive M α k →
      ∀ {s : Set α},
        Set.ncard s = k → Subgroup.index (fixingSubgroup M s) * (Fintype.card α - Set.ncard s)! = (Fintype.card α)!
Theorem: MulAction.IsMultiplyPretransitive.index_of_fixing_subgroup_aux
Proof state before:
k : ℕ
⊢ ∀ (M : Type u_2) (α : Type u_1) [inst : Group M] [inst_1 : MulAction M α] [inst_2 : Fintype α],
    IsMultiplyPretransitive M α k →
      ∀ {s : Set α},
        Set.ncard s = k → Subgroup.index (fixingSubgroup M s) * (Fintype.card α - Set.ncard s)! = (Fintype.card α)!
Tactic:
induction' k with k hrec
Proof state after:
case zero

⊢ ∀ (M : Type u_2) (α : Type u_1) [inst : Group M] [inst_1 : MulAction M α] [inst_2 : Fintype α],
    IsMultiplyPretransitive M α zero →
      ∀ {s : Set α},
        Set.ncard s = zero → Subgroup.index (fixingSubgroup M s) * (Fintype.card α - Set.ncard s)! = (Fintype.card α)!

case succ
k : ℕ
hrec :
  ∀ (M : Type u_2) (α : Type u_1) [inst : Group M] [inst_1 : MulAction M α] [inst_2 : Fintype α],
    IsMultiplyPretransitive M α k →
      ∀ {s : Set α},
        Set.ncard s = k → Subgroup.index (fixingSubgroup M s) * (Fintype.card α - Set.ncard s)! = (Fintype.card α)!
⊢ ∀ (M : Type u_2) (α : Type u_1) [inst : Group M] [inst_1 : MulAction M α] [inst_2 : Fintype α],
    IsMultiplyPretransitive M α (succ k) →
      ∀ {s : Set α},
        Set.ncard s = succ k → Subgroup.index (fixingSubgroup M s) * (Fintype.card α - Set.ncard s)! = (Fintype.card α)!
Theorem: MulAction.IsMultiplyPretransitive.index_of_fixing_subgroup_aux
Proof state before:
case succ
k : ℕ
hrec :
  ∀ (M : Type u_2) (α : Type u_1) [inst : Group M] [inst_1 : MulAction M α] [inst_2 : Fintype α],
    IsMultiplyPretransitive M α k →
      ∀ {s : Set α},
        Set.ncard s = k → Subgroup.index (fixingSubgroup M s) * (Fintype.card α - Set.ncard s)! = (Fintype.card α)!
⊢ ∀ (M : Type u_2) (α : Type u_1) [inst : Group M] [inst_1 : MulAction M α] [inst_2 : Fintype α],
    IsMultiplyPretransitive M α (succ k) →
      ∀ {s : Set α},
        Set.ncard s = succ k → Subgroup.index (fixingSubgroup M s) * (Fintype.card α - Set.ncard s)! = (Fintype.card α)!
Tactic:
intro M α _ _ _ hmk s hs
Proof state after:
case succ
k : ℕ
hrec :
  ∀ (M : Type u_2) (α : Type u_1) [inst : Group M] [inst_1 : MulAction M α] [inst_2 : Fintype α],
    IsMultiplyPretransitive M α k →
      ∀ {s : Set α},
        Set.ncard s = k → Subgroup.index (fixingSubgroup M s) * (Fintype.card α - Set.ncard s)! = (Fintype.card α)!
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
hmk : IsMultiplyPretransitive M α (succ k)
s : Set α
hs : Set.ncard s = succ k
⊢ Subgroup.index (fixingSubgroup M s) * (Fintype.card α - Set.ncard s)! = (Fintype.card α)!