internlm/Lean-Github huggingface dataset:
Theorem: MulAction.stabilizer.isMultiplyPretransitive
Proof state before:
case mp.exists_smul_eq
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
a : α
hn : IsMultiplyPretransitive M α (succ n)
hn_eq : ∀ (x y : Fin (succ n) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x y : Fin n ↪ ↥(SubMulAction.ofStabilizer M a)
⊢ ∃ g, g • x = y
Tactic:
obtain ⟨x', hx', hx'a⟩ := exists_extends_with_last_eq M a x
Proof state after:
case mp.exists_smul_eq.intro.intro
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
a : α
hn : IsMultiplyPretransitive M α (succ n)
hn_eq : ∀ (x y : Fin (succ n) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x y : Fin n ↪ ↥(SubMulAction.ofStabilizer M a)
x' : Fin (succ n) ↪ α
hx' :
  Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding x' =
    Function.Embedding.trans x { toFun := fun u => id ↑u, inj' := ⋯ }
hx'a : x' { val := n, isLt := ⋯ } = a
⊢ ∃ g, g • x = y
Theorem: MulAction.stabilizer.isMultiplyPretransitive
Proof state before:
case mp.exists_smul_eq.intro.intro
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
a : α
hn : IsMultiplyPretransitive M α (succ n)
hn_eq : ∀ (x y : Fin (succ n) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x y : Fin n ↪ ↥(SubMulAction.ofStabilizer M a)
x' : Fin (succ n) ↪ α
hx' :
  Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding x' =
    Function.Embedding.trans x { toFun := fun u => id ↑u, inj' := ⋯ }
hx'a : x' { val := n, isLt := ⋯ } = a
⊢ ∃ g, g • x = y
Tactic:
obtain ⟨y', hy', hy'a⟩ := exists_extends_with_last_eq M a y
Proof state after:
case mp.exists_smul_eq.intro.intro.intro.intro
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
a : α
hn : IsMultiplyPretransitive M α (succ n)
hn_eq : ∀ (x y : Fin (succ n) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x y : Fin n ↪ ↥(SubMulAction.ofStabilizer M a)
x' : Fin (succ n) ↪ α
hx' :
  Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding x' =
    Function.Embedding.trans x { toFun := fun u => id ↑u, inj' := ⋯ }
hx'a : x' { val := n, isLt := ⋯ } = a
y' : Fin (succ n) ↪ α
hy' :
  Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding y' =
    Function.Embedding.trans y { toFun := fun u => id ↑u, inj' := ⋯ }
hy'a : y' { val := n, isLt := ⋯ } = a
⊢ ∃ g, g • x = y
Theorem: MulAction.stabilizer.isMultiplyPretransitive
Proof state before:
case mp.exists_smul_eq.intro.intro.intro.intro
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
a : α
hn : IsMultiplyPretransitive M α (succ n)
hn_eq : ∀ (x y : Fin (succ n) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x y : Fin n ↪ ↥(SubMulAction.ofStabilizer M a)
x' : Fin (succ n) ↪ α
hx' :
  Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding x' =
    Function.Embedding.trans x { toFun := fun u => id ↑u, inj' := ⋯ }
hx'a : x' { val := n, isLt := ⋯ } = a
y' : Fin (succ n) ↪ α
hy' :
  Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding y' =
    Function.Embedding.trans y { toFun := fun u => id ↑u, inj' := ⋯ }
hy'a : y' { val := n, isLt := ⋯ } = a
⊢ ∃ g, g • x = y
Tactic:
obtain ⟨g, hg'⟩ := hn_eq x' y'
Proof state after:
case mp.exists_smul_eq.intro.intro.intro.intro.intro
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
a : α
hn : IsMultiplyPretransitive M α (succ n)
hn_eq : ∀ (x y : Fin (succ n) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x y : Fin n ↪ ↥(SubMulAction.ofStabilizer M a)
x' : Fin (succ n) ↪ α
hx' :
  Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding x' =
    Function.Embedding.trans x { toFun := fun u => id ↑u, inj' := ⋯ }
hx'a : x' { val := n, isLt := ⋯ } = a
y' : Fin (succ n) ↪ α
hy' :
  Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding y' =
    Function.Embedding.trans y { toFun := fun u => id ↑u, inj' := ⋯ }
hy'a : y' { val := n, isLt := ⋯ } = a
g : M
hg' : g • x' = y'
⊢ ∃ g, g • x = y
Theorem: MulAction.stabilizer.isMultiplyPretransitive
Proof state before:
case mp.exists_smul_eq.intro.intro.intro.intro.intro
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
a : α
hn : IsMultiplyPretransitive M α (succ n)
hn_eq : ∀ (x y : Fin (succ n) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x y : Fin n ↪ ↥(SubMulAction.ofStabilizer M a)
x' : Fin (succ n) ↪ α
hx' :
  Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding x' =
    Function.Embedding.trans x { toFun := fun u => id ↑u, inj' := ⋯ }
hx'a : x' { val := n, isLt := ⋯ } = a
y' : Fin (succ n) ↪ α
hy' :
  Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding y' =
    Function.Embedding.trans y { toFun := fun u => id ↑u, inj' := ⋯ }
hy'a : y' { val := n, isLt := ⋯ } = a
g : M
hg' : g • x' = y'
⊢ ∃ g, g • x = y
Tactic:
have hg : g ∈ stabilizer M a := by
  rw [mem_stabilizer_iff]
  conv_lhs => rw [← hx'a]
  rw [← hy'a, ← hg', smul_apply]
Proof state after:
case mp.exists_smul_eq.intro.intro.intro.intro.intro
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
a : α
hn : IsMultiplyPretransitive M α (succ n)
hn_eq : ∀ (x y : Fin (succ n) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x y : Fin n ↪ ↥(SubMulAction.ofStabilizer M a)
x' : Fin (succ n) ↪ α
hx' :
  Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding x' =
    Function.Embedding.trans x { toFun := fun u => id ↑u, inj' := ⋯ }
hx'a : x' { val := n, isLt := ⋯ } = a
y' : Fin (succ n) ↪ α
hy' :
  Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding y' =
    Function.Embedding.trans y { toFun := fun u => id ↑u, inj' := ⋯ }
hy'a : y' { val := n, isLt := ⋯ } = a
g : M
hg' : g • x' = y'
hg : g ∈ stabilizer M a
⊢ ∃ g, g • x = y
Theorem: MulAction.stabilizer.isMultiplyPretransitive
Proof state before:
case mp.exists_smul_eq.intro.intro.intro.intro.intro
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
a : α
hn : IsMultiplyPretransitive M α (succ n)
hn_eq : ∀ (x y : Fin (succ n) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x y : Fin n ↪ ↥(SubMulAction.ofStabilizer M a)
x' : Fin (succ n) ↪ α
hx' :
  Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding x' =
    Function.Embedding.trans x { toFun := fun u => id ↑u, inj' := ⋯ }
hx'a : x' { val := n, isLt := ⋯ } = a
y' : Fin (succ n) ↪ α
hy' :
  Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding y' =
    Function.Embedding.trans y { toFun := fun u => id ↑u, inj' := ⋯ }
hy'a : y' { val := n, isLt := ⋯ } = a
g : M
hg' : g • x' = y'
hg : g ∈ stabilizer M a
⊢ ∃ g, g • x = y
Tactic:
use ⟨g, hg⟩
Proof state after:
case h
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
a : α
hn : IsMultiplyPretransitive M α (succ n)
hn_eq : ∀ (x y : Fin (succ n) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x y : Fin n ↪ ↥(SubMulAction.ofStabilizer M a)
x' : Fin (succ n) ↪ α
hx' :
  Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding x' =
    Function.Embedding.trans x { toFun := fun u => id ↑u, inj' := ⋯ }
hx'a : x' { val := n, isLt := ⋯ } = a
y' : Fin (succ n) ↪ α
hy' :
  Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding y' =
    Function.Embedding.trans y { toFun := fun u => id ↑u, inj' := ⋯ }
hy'a : y' { val := n, isLt := ⋯ } = a
g : M
hg' : g • x' = y'
hg : g ∈ stabilizer M a
⊢ { val := g, property := hg } • x = y
Theorem: MulAction.stabilizer.isMultiplyPretransitive
Proof state before:
case h
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
a : α
hn : IsMultiplyPretransitive M α (succ n)
hn_eq : ∀ (x y : Fin (succ n) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x y : Fin n ↪ ↥(SubMulAction.ofStabilizer M a)
x' : Fin (succ n) ↪ α
hx' :
  Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding x' =
    Function.Embedding.trans x { toFun := fun u => id ↑u, inj' := ⋯ }
hx'a : x' { val := n, isLt := ⋯ } = a
y' : Fin (succ n) ↪ α
hy' :
  Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding y' =
    Function.Embedding.trans y { toFun := fun u => id ↑u, inj' := ⋯ }
hy'a : y' { val := n, isLt := ⋯ } = a
g : M
hg' : g • x' = y'
hg : g ∈ stabilizer M a
⊢ { val := g, property := hg } • x = y
Tactic:
ext ⟨i, hi⟩
Proof state after:
case h.h.mk.a
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
a : α
hn : IsMultiplyPretransitive M α (succ n)
hn_eq : ∀ (x y : Fin (succ n) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x y : Fin n ↪ ↥(SubMulAction.ofStabilizer M a)
x' : Fin (succ n) ↪ α
hx' :
  Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding x' =
    Function.Embedding.trans x { toFun := fun u => id ↑u, inj' := ⋯ }
hx'a : x' { val := n, isLt := ⋯ } = a
y' : Fin (succ n) ↪ α
hy' :
  Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding y' =
    Function.Embedding.trans y { toFun := fun u => id ↑u, inj' := ⋯ }
hy'a : y' { val := n, isLt := ⋯ } = a
g : M
hg' : g • x' = y'
hg : g ∈ stabilizer M a
i : ℕ
hi : i < n
⊢ ↑(({ val := g, property := hg } • x) { val := i, isLt := hi }) = ↑(y { val := i, isLt := hi })
Theorem: MulAction.stabilizer.isMultiplyPretransitive
Proof state before:
case h.h.mk.a
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
a : α
hn : IsMultiplyPretransitive M α (succ n)
hn_eq : ∀ (x y : Fin (succ n) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x y : Fin n ↪ ↥(SubMulAction.ofStabilizer M a)
x' : Fin (succ n) ↪ α
hx' :
  Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding x' =
    Function.Embedding.trans x { toFun := fun u => id ↑u, inj' := ⋯ }
hx'a : x' { val := n, isLt := ⋯ } = a
y' : Fin (succ n) ↪ α
hy' :
  Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding y' =
    Function.Embedding.trans y { toFun := fun u => id ↑u, inj' := ⋯ }
hy'a : y' { val := n, isLt := ⋯ } = a
g : M
hg' : g • x' = y'
hg : g ∈ stabilizer M a
i : ℕ
hi : i < n
⊢ ↑(({ val := g, property := hg } • x) { val := i, isLt := hi }) = ↑(y { val := i, isLt := hi })
Tactic:
simp only [smul_apply, SubMulAction.val_smul_of_tower]
Proof state after:
case h.h.mk.a
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
a : α
hn : IsMultiplyPretransitive M α (succ n)
hn_eq : ∀ (x y : Fin (succ n) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x y : Fin n ↪ ↥(SubMulAction.ofStabilizer M a)
x' : Fin (succ n) ↪ α
hx' :
  Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding x' =
    Function.Embedding.trans x { toFun := fun u => id ↑u, inj' := ⋯ }
hx'a : x' { val := n, isLt := ⋯ } = a
y' : Fin (succ n) ↪ α
hy' :
  Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding y' =
    Function.Embedding.trans y { toFun := fun u => id ↑u, inj' := ⋯ }
hy'a : y' { val := n, isLt := ⋯ } = a
g : M
hg' : g • x' = y'
hg : g ∈ stabilizer M a
i : ℕ
hi : i < n
⊢ { val := g, property := hg } • ↑(x { val := i, isLt := hi }) = ↑(y { val := i, isLt := hi })
Theorem: MulAction.stabilizer.isMultiplyPretransitive
Proof state before:
case h.h.mk.a
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
a : α
hn : IsMultiplyPretransitive M α (succ n)
hn_eq : ∀ (x y : Fin (succ n) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x y : Fin n ↪ ↥(SubMulAction.ofStabilizer M a)
x' : Fin (succ n) ↪ α
hx' :
  Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding x' =
    Function.Embedding.trans x { toFun := fun u => id ↑u, inj' := ⋯ }
hx'a : x' { val := n, isLt := ⋯ } = a
y' : Fin (succ n) ↪ α
hy' :
  Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding y' =
    Function.Embedding.trans y { toFun := fun u => id ↑u, inj' := ⋯ }
hy'a : y' { val := n, isLt := ⋯ } = a
g : M
hg' : g • x' = y'
hg : g ∈ stabilizer M a
i : ℕ
hi : i < n
⊢ { val := g, property := hg } • ↑(x { val := i, isLt := hi }) = ↑(y { val := i, isLt := hi })
Tactic:
rw [← Function.Embedding.ext_iff] at hx' hy'
Proof state after:
case h.h.mk.a
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
a : α
hn : IsMultiplyPretransitive M α (succ n)
hn_eq : ∀ (x y : Fin (succ n) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x y : Fin n ↪ ↥(SubMulAction.ofStabilizer M a)
x' : Fin (succ n) ↪ α
hx' :
  ∀ (x_1 : Fin n),
    (Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding x') x_1 =
      (Function.Embedding.trans x { toFun := fun u => id ↑u, inj' := ⋯ }) x_1
hx'a : x' { val := n, isLt := ⋯ } = a
y' : Fin (succ n) ↪ α
hy' :
  ∀ (x : Fin n),
    (Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding y') x =
      (Function.Embedding.trans y { toFun := fun u => id ↑u, inj' := ⋯ }) x
hy'a : y' { val := n, isLt := ⋯ } = a
g : M
hg' : g • x' = y'
hg : g ∈ stabilizer M a
i : ℕ
hi : i < n
⊢ { val := g, property := hg } • ↑(x { val := i, isLt := hi }) = ↑(y { val := i, isLt := hi })
Theorem: MulAction.stabilizer.isMultiplyPretransitive
Proof state before:
case h.h.mk.a
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
a : α
hn : IsMultiplyPretransitive M α (succ n)
hn_eq : ∀ (x y : Fin (succ n) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x y : Fin n ↪ ↥(SubMulAction.ofStabilizer M a)
x' : Fin (succ n) ↪ α
hx' :
  ∀ (x_1 : Fin n),
    (Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding x') x_1 =
      (Function.Embedding.trans x { toFun := fun u => id ↑u, inj' := ⋯ }) x_1
hx'a : x' { val := n, isLt := ⋯ } = a
y' : Fin (succ n) ↪ α
hy' :
  ∀ (x : Fin n),
    (Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding y') x =
      (Function.Embedding.trans y { toFun := fun u => id ↑u, inj' := ⋯ }) x
hy'a : y' { val := n, isLt := ⋯ } = a
g : M
hg' : g • x' = y'
hg : g ∈ stabilizer M a
i : ℕ
hi : i < n
⊢ { val := g, property := hg } • ↑(x { val := i, isLt := hi }) = ↑(y { val := i, isLt := hi })
Tactic:
specialize hx' ⟨i, hi⟩
Proof state after:
case h.h.mk.a
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
a : α
hn : IsMultiplyPretransitive M α (succ n)
hn_eq : ∀ (x y : Fin (succ n) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x y : Fin n ↪ ↥(SubMulAction.ofStabilizer M a)
x' : Fin (succ n) ↪ α
hx'a : x' { val := n, isLt := ⋯ } = a
y' : Fin (succ n) ↪ α
hy' :
  ∀ (x : Fin n),
    (Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding y') x =
      (Function.Embedding.trans y { toFun := fun u => id ↑u, inj' := ⋯ }) x
hy'a : y' { val := n, isLt := ⋯ } = a
g : M
hg' : g • x' = y'
hg : g ∈ stabilizer M a
i : ℕ
hi : i < n
hx' :
  (Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding x') { val := i, isLt := hi } =
    (Function.Embedding.trans x { toFun := fun u => id ↑u, inj' := ⋯ }) { val := i, isLt := hi }
⊢ { val := g, property := hg } • ↑(x { val := i, isLt := hi }) = ↑(y { val := i, isLt := hi })
Theorem: MulAction.stabilizer.isMultiplyPretransitive
Proof state before:
case h.h.mk.a
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
a : α
hn : IsMultiplyPretransitive M α (succ n)
hn_eq : ∀ (x y : Fin (succ n) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x y : Fin n ↪ ↥(SubMulAction.ofStabilizer M a)
x' : Fin (succ n) ↪ α
hx'a : x' { val := n, isLt := ⋯ } = a
y' : Fin (succ n) ↪ α
hy' :
  ∀ (x : Fin n),
    (Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding y') x =
      (Function.Embedding.trans y { toFun := fun u => id ↑u, inj' := ⋯ }) x
hy'a : y' { val := n, isLt := ⋯ } = a
g : M
hg' : g • x' = y'
hg : g ∈ stabilizer M a
i : ℕ
hi : i < n
hx' :
  (Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding x') { val := i, isLt := hi } =
    (Function.Embedding.trans x { toFun := fun u => id ↑u, inj' := ⋯ }) { val := i, isLt := hi }
⊢ { val := g, property := hg } • ↑(x { val := i, isLt := hi }) = ↑(y { val := i, isLt := hi })
Tactic:
specialize hy' ⟨i, hi⟩
Proof state after:
case h.h.mk.a
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
a : α
hn : IsMultiplyPretransitive M α (succ n)
hn_eq : ∀ (x y : Fin (succ n) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x y : Fin n ↪ ↥(SubMulAction.ofStabilizer M a)
x' : Fin (succ n) ↪ α
hx'a : x' { val := n, isLt := ⋯ } = a
y' : Fin (succ n) ↪ α
hy'a : y' { val := n, isLt := ⋯ } = a
g : M
hg' : g • x' = y'
hg : g ∈ stabilizer M a
i : ℕ
hi : i < n
hx' :
  (Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding x') { val := i, isLt := hi } =
    (Function.Embedding.trans x { toFun := fun u => id ↑u, inj' := ⋯ }) { val := i, isLt := hi }
hy' :
  (Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding y') { val := i, isLt := hi } =
    (Function.Embedding.trans y { toFun := fun u => id ↑u, inj' := ⋯ }) { val := i, isLt := hi }
⊢ { val := g, property := hg } • ↑(x { val := i, isLt := hi }) = ↑(y { val := i, isLt := hi })
Theorem: MulAction.stabilizer.isMultiplyPretransitive
Proof state before:
case h.h.mk.a
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
a : α
hn : IsMultiplyPretransitive M α (succ n)
hn_eq : ∀ (x y : Fin (succ n) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x y : Fin n ↪ ↥(SubMulAction.ofStabilizer M a)
x' : Fin (succ n) ↪ α
hx'a : x' { val := n, isLt := ⋯ } = a
y' : Fin (succ n) ↪ α
hy'a : y' { val := n, isLt := ⋯ } = a
g : M
hg' : g • x' = y'
hg : g ∈ stabilizer M a
i : ℕ
hi : i < n
hx' :
  (Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding x') { val := i, isLt := hi } =
    (Function.Embedding.trans x { toFun := fun u => id ↑u, inj' := ⋯ }) { val := i, isLt := hi }
hy' :
  (Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding y') { val := i, isLt := hi } =
    (Function.Embedding.trans y { toFun := fun u => id ↑u, inj' := ⋯ }) { val := i, isLt := hi }
⊢ { val := g, property := hg } • ↑(x { val := i, isLt := hi }) = ↑(y { val := i, isLt := hi })
Tactic:
simp only [trans_apply, RelEmbedding.coe_toEmbedding, Fin.castLE_mk, id.def, coeFn_mk] at hx' hy'
Proof state after:
case h.h.mk.a
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
a : α
hn : IsMultiplyPretransitive M α (succ n)
hn_eq : ∀ (x y : Fin (succ n) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x y : Fin n ↪ ↥(SubMulAction.ofStabilizer M a)
x' : Fin (succ n) ↪ α
hx'a : x' { val := n, isLt := ⋯ } = a
y' : Fin (succ n) ↪ α
hy'a : y' { val := n, isLt := ⋯ } = a
g : M
hg' : g • x' = y'
hg : g ∈ stabilizer M a
i : ℕ
hi : i < n
hx' : x' ((Fin.castLEEmb ⋯) { val := i, isLt := hi }) = ↑(x { val := i, isLt := hi })
hy' : y' ((Fin.castLEEmb ⋯) { val := i, isLt := hi }) = ↑(y { val := i, isLt := hi })
⊢ { val := g, property := hg } • ↑(x { val := i, isLt := hi }) = ↑(y { val := i, isLt := hi })
Theorem: MulAction.stabilizer.isMultiplyPretransitive
Proof state before:
case h.h.mk.a
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
a : α
hn : IsMultiplyPretransitive M α (succ n)
hn_eq : ∀ (x y : Fin (succ n) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x y : Fin n ↪ ↥(SubMulAction.ofStabilizer M a)
x' : Fin (succ n) ↪ α
hx'a : x' { val := n, isLt := ⋯ } = a
y' : Fin (succ n) ↪ α
hy'a : y' { val := n, isLt := ⋯ } = a
g : M
hg' : g • x' = y'
hg : g ∈ stabilizer M a
i : ℕ
hi : i < n
hx' : x' ((Fin.castLEEmb ⋯) { val := i, isLt := hi }) = ↑(x { val := i, isLt := hi })
hy' : y' ((Fin.castLEEmb ⋯) { val := i, isLt := hi }) = ↑(y { val := i, isLt := hi })
⊢ { val := g, property := hg } • ↑(x { val := i, isLt := hi }) = ↑(y { val := i, isLt := hi })
Tactic:
rw [← hx', ← hy', ← hg']
Proof state after:
case h.h.mk.a
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
a : α
hn : IsMultiplyPretransitive M α (succ n)
hn_eq : ∀ (x y : Fin (succ n) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x y : Fin n ↪ ↥(SubMulAction.ofStabilizer M a)
x' : Fin (succ n) ↪ α
hx'a : x' { val := n, isLt := ⋯ } = a
y' : Fin (succ n) ↪ α
hy'a : y' { val := n, isLt := ⋯ } = a
g : M
hg' : g • x' = y'
hg : g ∈ stabilizer M a
i : ℕ
hi : i < n
hx' : x' ((Fin.castLEEmb ⋯) { val := i, isLt := hi }) = ↑(x { val := i, isLt := hi })
hy' : y' ((Fin.castLEEmb ⋯) { val := i, isLt := hi }) = ↑(y { val := i, isLt := hi })
⊢ { val := g, property := hg } • x' ((Fin.castLEEmb ⋯) { val := i, isLt := hi }) =
    (g • x') ((Fin.castLEEmb ⋯) { val := i, isLt := hi })
Theorem: MulAction.stabilizer.isMultiplyPretransitive
Proof state before:
case h.h.mk.a
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
a : α
hn : IsMultiplyPretransitive M α (succ n)
hn_eq : ∀ (x y : Fin (succ n) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x y : Fin n ↪ ↥(SubMulAction.ofStabilizer M a)
x' : Fin (succ n) ↪ α
hx'a : x' { val := n, isLt := ⋯ } = a
y' : Fin (succ n) ↪ α
hy'a : y' { val := n, isLt := ⋯ } = a
g : M
hg' : g • x' = y'
hg : g ∈ stabilizer M a
i : ℕ
hi : i < n
hx' : x' ((Fin.castLEEmb ⋯) { val := i, isLt := hi }) = ↑(x { val := i, isLt := hi })
hy' : y' ((Fin.castLEEmb ⋯) { val := i, isLt := hi }) = ↑(y { val := i, isLt := hi })
⊢ { val := g, property := hg } • x' ((Fin.castLEEmb ⋯) { val := i, isLt := hi }) =
    (g • x') ((Fin.castLEEmb ⋯) { val := i, isLt := hi })
Tactic:
rfl
Proof state after:
no goals
Theorem: MulAction.stabilizer.isMultiplyPretransitive
Proof state before:
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
a : α
hn : IsMultiplyPretransitive M α (succ n)
hn_eq : ∀ (x y : Fin (succ n) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x y : Fin n ↪ ↥(SubMulAction.ofStabilizer M a)
x' : Fin (succ n) ↪ α
hx' :
  Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding x' =
    Function.Embedding.trans x { toFun := fun u => id ↑u, inj' := ⋯ }
hx'a : x' { val := n, isLt := ⋯ } = a
y' : Fin (succ n) ↪ α
hy' :
  Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding y' =
    Function.Embedding.trans y { toFun := fun u => id ↑u, inj' := ⋯ }
hy'a : y' { val := n, isLt := ⋯ } = a
g : M
hg' : g • x' = y'
⊢ g ∈ stabilizer M a
Tactic:
rw [mem_stabilizer_iff]
Proof state after:
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
a : α
hn : IsMultiplyPretransitive M α (succ n)
hn_eq : ∀ (x y : Fin (succ n) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x y : Fin n ↪ ↥(SubMulAction.ofStabilizer M a)
x' : Fin (succ n) ↪ α
hx' :
  Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding x' =
    Function.Embedding.trans x { toFun := fun u => id ↑u, inj' := ⋯ }
hx'a : x' { val := n, isLt := ⋯ } = a
y' : Fin (succ n) ↪ α
hy' :
  Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding y' =
    Function.Embedding.trans y { toFun := fun u => id ↑u, inj' := ⋯ }
hy'a : y' { val := n, isLt := ⋯ } = a
g : M
hg' : g • x' = y'
⊢ g • a = a