internlm/Lean-Github huggingface dataset:
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 • a = a
Tactic:
conv_lhs => rw [← hx'a]
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 • x' { val := n, isLt := ⋯ } = a
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 • x' { val := n, isLt := ⋯ } = a
Tactic:
rw [← hy'a, ← hg', smul_apply]
Proof state after:
no goals
Theorem: MulAction.stabilizer.isMultiplyPretransitive
Proof state before:
case mpr
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
a : α
⊢ IsMultiplyPretransitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n →
    IsMultiplyPretransitive M α (succ n)
Tactic:
intro hn
Proof state after:
case mpr
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
⊢ IsMultiplyPretransitive M α (succ n)
Theorem: MulAction.stabilizer.isMultiplyPretransitive
Proof state before:
case mpr
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
⊢ IsMultiplyPretransitive M α (succ n)
Tactic:
apply IsPretransitive.mk
Proof state after:
case mpr.exists_smul_eq
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 y : Fin (succ n) ↪ α), ∃ g, g • x = y
Theorem: MulAction.stabilizer.isMultiplyPretransitive
Proof state before:
case mpr.exists_smul_eq
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 y : Fin (succ n) ↪ α), ∃ g, g • x = y
Tactic:
intro x
Proof state after:
case mpr.exists_smul_eq
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) ↪ α
⊢ ∀ (y : Fin (succ n) ↪ α), ∃ g, g • x = y
Theorem: MulAction.stabilizer.isMultiplyPretransitive
Proof state before:
case mpr.exists_smul_eq
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) ↪ α
⊢ ∀ (y : Fin (succ n) ↪ α), ∃ g, g • x = y
Tactic:
obtain ⟨gx, x1, hgx, hga⟩ := exists_smul_of_last_eq M a x
Proof state after:
case mpr.exists_smul_eq.intro.intro.intro
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 (Fin.last n) = a
⊢ ∀ (y : Fin (succ n) ↪ α), ∃ g, g • x = y
Theorem: MulAction.stabilizer.isMultiplyPretransitive
Proof state before:
case mpr.exists_smul_eq.intro.intro.intro
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 (Fin.last n) = a
⊢ ∀ (y : Fin (succ n) ↪ α), ∃ g, g • x = y
Tactic:
intro y
Proof state after:
case mpr.exists_smul_eq.intro.intro.intro
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 (Fin.last n) = a
y : Fin (succ n) ↪ α
⊢ ∃ g, g • x = y
Theorem: MulAction.stabilizer.isMultiplyPretransitive
Proof state before:
case mpr.exists_smul_eq.intro.intro.intro
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 (Fin.last n) = a
y : Fin (succ n) ↪ α
⊢ ∃ g, g • x = y
Tactic:
obtain ⟨gy, y1, hgy, hgb⟩ := exists_smul_of_last_eq M a y
Proof state after:
case mpr.exists_smul_eq.intro.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 (↥(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 (Fin.last n) = 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 (Fin.last n) = a
⊢ ∃ g, g • x = y
Theorem: MulAction.stabilizer.isMultiplyPretransitive
Proof state before:
case mpr.exists_smul_eq.intro.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 (↥(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 (Fin.last n) = 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 (Fin.last n) = a
⊢ ∃ g, g • x = y
Tactic:
let hna_eq := hn.exists_smul_eq
Proof state after:
case mpr.exists_smul_eq.intro.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 (↥(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 (Fin.last n) = 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 (Fin.last n) = a
hna_eq : ∀ (x y : Fin n ↪ ↥(SubMulAction.ofStabilizer M a)), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
⊢ ∃ g, g • x = y
Theorem: MulAction.stabilizer.isMultiplyPretransitive
Proof state before:
case mpr.exists_smul_eq.intro.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 (↥(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 (Fin.last n) = 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 (Fin.last n) = a
hna_eq : ∀ (x y : Fin n ↪ ↥(SubMulAction.ofStabilizer M a)), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
⊢ ∃ g, g • x = y
Tactic:
obtain ⟨g, hg⟩ := hna_eq x1 y1
Proof state after:
case mpr.exists_smul_eq.intro.intro.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 (↥(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 (Fin.last n) = 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 (Fin.last n) = 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
⊢ ∃ g, g • x = y
Theorem: MulAction.stabilizer.isMultiplyPretransitive
Proof state before:
case mpr.exists_smul_eq.intro.intro.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 (↥(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 (Fin.last n) = 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 (Fin.last n) = 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
⊢ ∃ g, g • x = y
Tactic:
use gy⁻¹ * g * gx
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 (↥(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 (Fin.last n) = 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 (Fin.last n) = 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
⊢ (gy⁻¹ * ↑g * gx) • 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 (↥(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 (Fin.last n) = 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 (Fin.last n) = 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
⊢ (gy⁻¹ * ↑g * gx) • x = y
Tactic:
ext ⟨i, hi⟩
Proof state after:
case h.h.mk
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 (Fin.last n) = 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 (Fin.last n) = 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
⊢ ((gy⁻¹ * ↑g * gx) • x) { val := i, isLt := hi } = y { val := i, isLt := hi }
Theorem: MulAction.stabilizer.isMultiplyPretransitive
Proof state before:
case h.h.mk
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 (Fin.last n) = 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 (Fin.last n) = 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
⊢ ((gy⁻¹ * ↑g * gx) • x) { val := i, isLt := hi } = y { val := i, isLt := hi }
Tactic:
rw [mul_smul]
Proof state after:
case h.h.mk
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 (Fin.last n) = 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 (Fin.last n) = 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
⊢ ((gy⁻¹ * ↑g) • gx • x) { val := i, isLt := hi } = y { val := i, isLt := hi }
Theorem: MulAction.stabilizer.isMultiplyPretransitive
Proof state before:
case h.h.mk
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 (Fin.last n) = 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 (Fin.last n) = 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
⊢ ((gy⁻¹ * ↑g) • gx • x) { val := i, isLt := hi } = y { val := i, isLt := hi }
Tactic:
simp only [smul_apply]
Proof state after:
case h.h.mk
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 (Fin.last n) = 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 (Fin.last n) = 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
⊢ (gy⁻¹ * ↑g) • gx • x { val := i, isLt := hi } = y { val := i, isLt := hi }
Theorem: MulAction.stabilizer.isMultiplyPretransitive
Proof state before:
case h.h.mk
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 (Fin.last n) = 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 (Fin.last n) = 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
⊢ (gy⁻¹ * ↑g) • gx • x { val := i, isLt := hi } = y { val := i, isLt := hi }
Tactic:
cases' lt_or_eq_of_le (le_of_lt_succ hi) with hi' hi'
Proof state after:
case h.h.mk.inl
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 (Fin.last n) = 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 (Fin.last n) = 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
⊢ (gy⁻¹ * ↑g) • gx • x { val := i, isLt := hi } = y { val := i, isLt := hi }

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 (Fin.last n) = 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 (Fin.last n) = 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
⊢ (gy⁻¹ * ↑g) • gx • x { val := i, isLt := hi } = y { val := i, isLt := hi }