Theorem: MulAction.stabilizer.isMultiplyPretransitive' (Jordan/MultipleTransitivity.lean)

State before:
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
⊢ IsMultiplyPretransitive M α (succ n) ↔
    ∀ (a : α), IsMultiplyPretransitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
Tactic:
constructor
State after:
case mp
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
⊢ IsMultiplyPretransitive M α (succ n) →
    ∀ (a : α), IsMultiplyPretransitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n

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)

State before:
case mp
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
⊢ IsMultiplyPretransitive M α (succ n) →
    ∀ (a : α), IsMultiplyPretransitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
Tactic:
intro hn a
State after:
case mp
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
hn : IsMultiplyPretransitive M α (succ n)
a : α
⊢ IsMultiplyPretransitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n

State before:
case mp
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
hn : IsMultiplyPretransitive M α (succ n)
a : α
⊢ IsMultiplyPretransitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
Tactic:
let hn_eq := hn.exists_smul_eq
State after:
case mp
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
hn : IsMultiplyPretransitive M α (succ n)
a : α
hn_eq : ∀ (x y : Fin (succ n) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
⊢ IsMultiplyPretransitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n

State before:
case mp
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
hn : IsMultiplyPretransitive M α (succ n)
a : α
hn_eq : ∀ (x y : Fin (succ n) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
⊢ IsMultiplyPretransitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
Tactic:
apply IsPretransitive.mk
State after:
case mp.exists_smul_eq
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
hn : IsMultiplyPretransitive M α (succ n)
a : α
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

State before:
case mp.exists_smul_eq
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
hn : IsMultiplyPretransitive M α (succ n)
a : α
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:
intro x y
State after:
case mp.exists_smul_eq
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
hn : IsMultiplyPretransitive M α (succ n)
a : α
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

State before:
case mp.exists_smul_eq
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
hn : IsMultiplyPretransitive M α (succ n)
a : α
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
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 : ℕ
hn : IsMultiplyPretransitive M α (succ n)
a : α
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

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 : ℕ
hn : IsMultiplyPretransitive M α (succ n)
a : α
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
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 : ℕ
hn : IsMultiplyPretransitive M α (succ n)
a : α
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

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 : ℕ
hn : IsMultiplyPretransitive M α (succ n)
a : α
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'
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 : ℕ
hn : IsMultiplyPretransitive M α (succ n)
a : α
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

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 : ℕ
hn : IsMultiplyPretransitive M α (succ n)
a : α
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]
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 : ℕ
hn : IsMultiplyPretransitive M α (succ n)
a : α
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

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 : ℕ
hn : IsMultiplyPretransitive M α (succ n)
a : α
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⟩
State after:
case h
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
hn : IsMultiplyPretransitive M α (succ n)
a : α
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

State before:
case h
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
hn : IsMultiplyPretransitive M α (succ n)
a : α
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⟩
State after:
case h.h.mk.a
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
hn : IsMultiplyPretransitive M α (succ n)
a : α
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 })

State before:
case h.h.mk.a
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
hn : IsMultiplyPretransitive M α (succ n)
a : α
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]
State after:
case h.h.mk.a
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
hn : IsMultiplyPretransitive M α (succ n)
a : α
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 })

State before:
case h.h.mk.a
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
hn : IsMultiplyPretransitive M α (succ n)
a : α
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'
State after:
case h.h.mk.a
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
hn : IsMultiplyPretransitive M α (succ n)
a : α
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 })

State before:
case h.h.mk.a
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
hn : IsMultiplyPretransitive M α (succ n)
a : α
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⟩
State after:
case h.h.mk.a
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
hn : IsMultiplyPretransitive M α (succ n)
a : α
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 })

State before:
case h.h.mk.a
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
hn : IsMultiplyPretransitive M α (succ n)
a : α
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⟩
State after:
case h.h.mk.a
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
hn : IsMultiplyPretransitive M α (succ n)
a : α
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 })

State before:
case h.h.mk.a
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
hn : IsMultiplyPretransitive M α (succ n)
a : α
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'
State after:
case h.h.mk.a
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
hn : IsMultiplyPretransitive M α (succ n)
a : α
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 })

State before:
case h.h.mk.a
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
hn : IsMultiplyPretransitive M α (succ n)
a : α
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']
State after:
case h.h.mk.a
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
hn : IsMultiplyPretransitive M α (succ n)
a : α
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 })

State before:
case h.h.mk.a
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
hn : IsMultiplyPretransitive M α (succ n)
a : α
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
State after:
no goals

State before:
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
hn : IsMultiplyPretransitive M α (succ n)
a : α
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]
State after:
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
hn : IsMultiplyPretransitive M α (succ n)
a : α
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

State before:
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
hn : IsMultiplyPretransitive M α (succ n)
a : α
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]
State after:
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
hn : IsMultiplyPretransitive M α (succ n)
a : α
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

State before:
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
hn : IsMultiplyPretransitive M α (succ n)
a : α
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]
State after:
no goals

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
State after:
case mpr
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
hn : ∀ (a : α), IsMultiplyPretransitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
⊢ IsMultiplyPretransitive M α (succ n)

State before:
case mpr
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
hn : ∀ (a : α), IsMultiplyPretransitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
⊢ IsMultiplyPretransitive M α (succ n)
Tactic:
apply IsPretransitive.mk
State after:
case mpr.exists_smul_eq
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
hn : ∀ (a : α), IsMultiplyPretransitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
⊢ ∀ (x y : Fin (succ n) ↪ α), ∃ g, g • x = y

State before:
case mpr.exists_smul_eq
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
hn : ∀ (a : α), IsMultiplyPretransitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
⊢ ∀ (x y : Fin (succ n) ↪ α), ∃ g, g • x = y
Tactic:
intro x
State after:
case mpr.exists_smul_eq
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
hn : ∀ (a : α), IsMultiplyPretransitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
x : Fin (succ n) ↪ α
⊢ ∀ (y : Fin (succ n) ↪ α), ∃ g, g • x = y

State before:
case mpr.exists_smul_eq
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
hn : ∀ (a : α), IsMultiplyPretransitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
x : Fin (succ n) ↪ α
⊢ ∀ (y : Fin (succ n) ↪ α), ∃ g, g • x = y
Tactic:
let a := x ⟨n, lt_add_one n⟩
State after:
case mpr.exists_smul_eq
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
hn : ∀ (a : α), IsMultiplyPretransitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
x : Fin (succ n) ↪ α
a : α := x { val := n, isLt := ⋯ }
⊢ ∀ (y : Fin (succ n) ↪ α), ∃ g, g • x = y

State before:
case mpr.exists_smul_eq
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
hn : ∀ (a : α), IsMultiplyPretransitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
x : Fin (succ n) ↪ α
a : α := x { val := n, isLt := ⋯ }
⊢ ∀ (y : Fin (succ n) ↪ α), ∃ g, g • x = y
Tactic:
obtain ⟨gx, x1, hgx, hga⟩ := exists_smul_of_last_eq M a x
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 : ℕ
hn : ∀ (a : α), IsMultiplyPretransitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
x : Fin (succ n) ↪ α
a : α := x { val := n, isLt := ⋯ }
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

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 : ℕ
hn : ∀ (a : α), IsMultiplyPretransitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
x : Fin (succ n) ↪ α
a : α := x { val := n, isLt := ⋯ }
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
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 : ℕ
hn : ∀ (a : α), IsMultiplyPretransitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
x : Fin (succ n) ↪ α
a : α := x { val := n, isLt := ⋯ }
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

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 : ℕ
hn : ∀ (a : α), IsMultiplyPretransitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
x : Fin (succ n) ↪ α
a : α := x { val := n, isLt := ⋯ }
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
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 : ℕ
hn : ∀ (a : α), IsMultiplyPretransitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
x : Fin (succ n) ↪ α
a : α := x { val := n, isLt := ⋯ }
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

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 : ℕ
hn : ∀ (a : α), IsMultiplyPretransitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
x : Fin (succ n) ↪ α
a : α := x { val := n, isLt := ⋯ }
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 a).exists_smul_eq
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 : ℕ
hn : ∀ (a : α), IsMultiplyPretransitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
x : Fin (succ n) ↪ α
a : α := x { val := n, isLt := ⋯ }
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

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 : ℕ
hn : ∀ (a : α), IsMultiplyPretransitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
x : Fin (succ n) ↪ α
a : α := x { val := n, isLt := ⋯ }
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
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 : ℕ
hn : ∀ (a : α), IsMultiplyPretransitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
x : Fin (succ n) ↪ α
a : α := x { val := n, isLt := ⋯ }
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

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 : ℕ
hn : ∀ (a : α), IsMultiplyPretransitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
x : Fin (succ n) ↪ α
a : α := x { val := n, isLt := ⋯ }
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
State after:
case h
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
hn : ∀ (a : α), IsMultiplyPretransitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
x : Fin (succ n) ↪ α
a : α := x { val := n, isLt := ⋯ }
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

State before:
case h
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
hn : ∀ (a : α), IsMultiplyPretransitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
x : Fin (succ n) ↪ α
a : α := x { val := n, isLt := ⋯ }
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⟩
State after:
case h.h.mk
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
hn : ∀ (a : α), IsMultiplyPretransitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
x : Fin (succ n) ↪ α
a : α := x { val := n, isLt := ⋯ }
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 }

State before:
case h.h.mk
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
hn : ∀ (a : α), IsMultiplyPretransitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
x : Fin (succ n) ↪ α
a : α := x { val := n, isLt := ⋯ }
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]
State after:
case h.h.mk
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
hn : ∀ (a : α), IsMultiplyPretransitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
x : Fin (succ n) ↪ α
a : α := x { val := n, isLt := ⋯ }
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 }

State before:
case h.h.mk
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
hn : ∀ (a : α), IsMultiplyPretransitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
x : Fin (succ n) ↪ α
a : α := x { val := n, isLt := ⋯ }
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]
State after:
case h.h.mk
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
hn : ∀ (a : α), IsMultiplyPretransitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
x : Fin (succ n) ↪ α
a : α := x { val := n, isLt := ⋯ }
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 }

State before:
case h.h.mk
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
hn : ∀ (a : α), IsMultiplyPretransitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
x : Fin (succ n) ↪ α
a : α := x { val := n, isLt := ⋯ }
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'
State after:
case h.h.mk.inl
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
hn : ∀ (a : α), IsMultiplyPretransitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
x : Fin (succ n) ↪ α
a : α := x { val := n, isLt := ⋯ }
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 : ℕ
hn : ∀ (a : α), IsMultiplyPretransitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
x : Fin (succ n) ↪ α
a : α := x { val := n, isLt := ⋯ }
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 }

State before:
case h.h.mk.inl
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
hn : ∀ (a : α), IsMultiplyPretransitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
x : Fin (succ n) ↪ α
a : α := x { val := n, isLt := ⋯ }
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 }
Tactic:
rw [← Function.Embedding.ext_iff] at hgx hgy hg
State after:
case h.h.mk.inl
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
hn : ∀ (a : α), IsMultiplyPretransitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
x : Fin (succ n) ↪ α
a : α := x { val := n, isLt := ⋯ }
gx : M
x1 : Fin n ↪ ↥(SubMulAction.ofStabilizer M a)
hgx :
  ∀ (x_1 : Fin n),
    (Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding (gx • x)) x_1 =
      (Function.Embedding.trans x1 (subtype fun x => x ∈ SubMulAction.ofStabilizer M a)) x_1
hga : gx • x (Fin.last n) = a
y : Fin (succ n) ↪ α
gy : M
y1 : Fin n ↪ ↥(SubMulAction.ofStabilizer M a)
hgy :
  ∀ (x : Fin n),
    (Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding (gy • y)) x =
      (Function.Embedding.trans y1 (subtype fun x => x ∈ SubMulAction.ofStabilizer M a)) x
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 : ∀ (x : Fin n), (g • x1) x = y1 x
i : ℕ
hi : i < succ n
hi' : i < n
⊢ (gy⁻¹ * ↑g) • gx • x { val := i, isLt := hi } = y { val := i, isLt := hi }

State before:
case h.h.mk.inl
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
hn : ∀ (a : α), IsMultiplyPretransitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
x : Fin (succ n) ↪ α
a : α := x { val := n, isLt := ⋯ }
gx : M
x1 : Fin n ↪ ↥(SubMulAction.ofStabilizer M a)
hgx :
  ∀ (x_1 : Fin n),
    (Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding (gx • x)) x_1 =
      (Function.Embedding.trans x1 (subtype fun x => x ∈ SubMulAction.ofStabilizer M a)) x_1
hga : gx • x (Fin.last n) = a
y : Fin (succ n) ↪ α
gy : M
y1 : Fin n ↪ ↥(SubMulAction.ofStabilizer M a)
hgy :
  ∀ (x : Fin n),
    (Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding (gy • y)) x =
      (Function.Embedding.trans y1 (subtype fun x => x ∈ SubMulAction.ofStabilizer M a)) x
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 : ∀ (x : Fin n), (g • x1) x = y1 x
i : ℕ
hi : i < succ n
hi' : i < n
⊢ (gy⁻¹ * ↑g) • gx • x { val := i, isLt := hi } = y { val := i, isLt := hi }
Tactic:
specialize hgx ⟨i, hi'⟩
State after:
case h.h.mk.inl
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
hn : ∀ (a : α), IsMultiplyPretransitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
x : Fin (succ n) ↪ α
a : α := x { val := n, isLt := ⋯ }
gx : M
x1 : Fin n ↪ ↥(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 :
  ∀ (x : Fin n),
    (Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding (gy • y)) x =
      (Function.Embedding.trans y1 (subtype fun x => x ∈ SubMulAction.ofStabilizer M a)) x
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 : ∀ (x : Fin n), (g • x1) x = y1 x
i : ℕ
hi : i < succ n
hi' : i < n
hgx :
  (Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding (gx • x)) { val := i, isLt := hi' } =
    (Function.Embedding.trans x1 (subtype fun x => x ∈ SubMulAction.ofStabilizer M a)) { val := i, isLt := hi' }
⊢ (gy⁻¹ * ↑g) • gx • x { val := i, isLt := hi } = y { val := i, isLt := hi }

State before:
case h.h.mk.inl
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
hn : ∀ (a : α), IsMultiplyPretransitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
x : Fin (succ n) ↪ α
a : α := x { val := n, isLt := ⋯ }
gx : M
x1 : Fin n ↪ ↥(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 :
  ∀ (x : Fin n),
    (Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding (gy • y)) x =
      (Function.Embedding.trans y1 (subtype fun x => x ∈ SubMulAction.ofStabilizer M a)) x
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 : ∀ (x : Fin n), (g • x1) x = y1 x
i : ℕ
hi : i < succ n
hi' : i < n
hgx :
  (Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding (gx • x)) { val := i, isLt := hi' } =
    (Function.Embedding.trans x1 (subtype fun x => x ∈ SubMulAction.ofStabilizer M a)) { val := i, isLt := hi' }
⊢ (gy⁻¹ * ↑g) • gx • x { val := i, isLt := hi } = y { val := i, isLt := hi }
Tactic:
specialize hgy ⟨i, hi'⟩
State after:
case h.h.mk.inl
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
hn : ∀ (a : α), IsMultiplyPretransitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
x : Fin (succ n) ↪ α
a : α := x { val := n, isLt := ⋯ }
gx : M
x1 : Fin n ↪ ↥(SubMulAction.ofStabilizer M a)
hga : gx • x (Fin.last n) = a
y : Fin (succ n) ↪ α
gy : M
y1 : Fin n ↪ ↥(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 : ∀ (x : Fin n), (g • x1) x = y1 x
i : ℕ
hi : i < succ n
hi' : i < n
hgx :
  (Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding (gx • x)) { val := i, isLt := hi' } =
    (Function.Embedding.trans x1 (subtype fun x => x ∈ SubMulAction.ofStabilizer M a)) { val := i, isLt := hi' }
hgy :
  (Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding (gy • y)) { val := i, isLt := hi' } =
    (Function.Embedding.trans y1 (subtype fun x => x ∈ SubMulAction.ofStabilizer M a)) { val := i, isLt := hi' }
⊢ (gy⁻¹ * ↑g) • gx • x { val := i, isLt := hi } = y { val := i, isLt := hi }

State before:
case h.h.mk.inl
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
hn : ∀ (a : α), IsMultiplyPretransitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
x : Fin (succ n) ↪ α
a : α := x { val := n, isLt := ⋯ }
gx : M
x1 : Fin n ↪ ↥(SubMulAction.ofStabilizer M a)
hga : gx • x (Fin.last n) = a
y : Fin (succ n) ↪ α
gy : M
y1 : Fin n ↪ ↥(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 : ∀ (x : Fin n), (g • x1) x = y1 x
i : ℕ
hi : i < succ n
hi' : i < n
hgx :
  (Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding (gx • x)) { val := i, isLt := hi' } =
    (Function.Embedding.trans x1 (subtype fun x => x ∈ SubMulAction.ofStabilizer M a)) { val := i, isLt := hi' }
hgy :
  (Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding (gy • y)) { val := i, isLt := hi' } =
    (Function.Embedding.trans y1 (subtype fun x => x ∈ SubMulAction.ofStabilizer M a)) { val := i, isLt := hi' }
⊢ (gy⁻¹ * ↑g) • gx • x { val := i, isLt := hi } = y { val := i, isLt := hi }
Tactic:
specialize hg ⟨i, hi'⟩
State after:
case h.h.mk.inl
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
hn : ∀ (a : α), IsMultiplyPretransitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
x : Fin (succ n) ↪ α
a : α := x { val := n, isLt := ⋯ }
gx : M
x1 : Fin n ↪ ↥(SubMulAction.ofStabilizer M a)
hga : gx • x (Fin.last n) = a
y : Fin (succ n) ↪ α
gy : M
y1 : Fin n ↪ ↥(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)
i : ℕ
hi : i < succ n
hi' : i < n
hgx :
  (Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding (gx • x)) { val := i, isLt := hi' } =
    (Function.Embedding.trans x1 (subtype fun x => x ∈ SubMulAction.ofStabilizer M a)) { val := i, isLt := hi' }
hgy :
  (Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding (gy • y)) { val := i, isLt := hi' } =
    (Function.Embedding.trans y1 (subtype fun x => x ∈ SubMulAction.ofStabilizer M a)) { val := i, isLt := hi' }
hg : (g • x1) { val := i, isLt := hi' } = y1 { val := i, isLt := hi' }
⊢ (gy⁻¹ * ↑g) • gx • x { val := i, isLt := hi } = y { val := i, isLt := hi }

State before:
case h.h.mk.inl
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
hn : ∀ (a : α), IsMultiplyPretransitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
x : Fin (succ n) ↪ α
a : α := x { val := n, isLt := ⋯ }
gx : M
x1 : Fin n ↪ ↥(SubMulAction.ofStabilizer M a)
hga : gx • x (Fin.last n) = a
y : Fin (succ n) ↪ α
gy : M
y1 : Fin n ↪ ↥(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)
i : ℕ
hi : i < succ n
hi' : i < n
hgx :
  (Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding (gx • x)) { val := i, isLt := hi' } =
    (Function.Embedding.trans x1 (subtype fun x => x ∈ SubMulAction.ofStabilizer M a)) { val := i, isLt := hi' }
hgy :
  (Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding (gy • y)) { val := i, isLt := hi' } =
    (Function.Embedding.trans y1 (subtype fun x => x ∈ SubMulAction.ofStabilizer M a)) { val := i, isLt := hi' }
hg : (g • x1) { val := i, isLt := hi' } = y1 { val := i, isLt := hi' }
⊢ (gy⁻¹ * ↑g) • gx • x { val := i, isLt := hi } = y { val := i, isLt := hi }
Tactic:
simp only [Fin.castLEEmb_toEmbedding, trans_apply, coeFn_mk, Fin.castLE_mk,
  smul_apply, zero_eq, coe_subtype] at hgx hgy hg
State after:
case h.h.mk.inl
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
hn : ∀ (a : α), IsMultiplyPretransitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
x : Fin (succ n) ↪ α
a : α := x { val := n, isLt := ⋯ }
gx : M
x1 : Fin n ↪ ↥(SubMulAction.ofStabilizer M a)
hga : gx • x (Fin.last n) = a
y : Fin (succ n) ↪ α
gy : M
y1 : Fin n ↪ ↥(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)
i : ℕ
hi : i < succ n
hi' : i < n
hgx : gx • x { val := i, isLt := ⋯ } = ↑(x1 { val := i, isLt := hi' })
hgy : gy • y { val := i, isLt := ⋯ } = ↑(y1 { val := i, isLt := hi' })
hg : g • x1 { val := i, isLt := hi' } = y1 { val := i, isLt := hi' }
⊢ (gy⁻¹ * ↑g) • gx • x { val := i, isLt := hi } = y { val := i, isLt := hi }

State before:
case h.h.mk.inl
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
hn : ∀ (a : α), IsMultiplyPretransitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
x : Fin (succ n) ↪ α
a : α := x { val := n, isLt := ⋯ }
gx : M
x1 : Fin n ↪ ↥(SubMulAction.ofStabilizer M a)
hga : gx • x (Fin.last n) = a
y : Fin (succ n) ↪ α
gy : M
y1 : Fin n ↪ ↥(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)
i : ℕ
hi : i < succ n
hi' : i < n
hgx : gx • x { val := i, isLt := ⋯ } = ↑(x1 { val := i, isLt := hi' })
hgy : gy • y { val := i, isLt := ⋯ } = ↑(y1 { val := i, isLt := hi' })
hg : g • x1 { val := i, isLt := hi' } = y1 { val := i, isLt := hi' }
⊢ (gy⁻¹ * ↑g) • gx • x { val := i, isLt := hi } = y { val := i, isLt := hi }
Tactic:
rw [hgx, mul_smul, inv_smul_eq_iff, hgy, ← hg]
State after:
case h.h.mk.inl
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
hn : ∀ (a : α), IsMultiplyPretransitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
x : Fin (succ n) ↪ α
a : α := x { val := n, isLt := ⋯ }
gx : M
x1 : Fin n ↪ ↥(SubMulAction.ofStabilizer M a)
hga : gx • x (Fin.last n) = a
y : Fin (succ n) ↪ α
gy : M
y1 : Fin n ↪ ↥(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)
i : ℕ
hi : i < succ n
hi' : i < n
hgx : gx • x { val := i, isLt := ⋯ } = ↑(x1 { val := i, isLt := hi' })
hgy : gy • y { val := i, isLt := ⋯ } = ↑(y1 { val := i, isLt := hi' })
hg : g • x1 { val := i, isLt := hi' } = y1 { val := i, isLt := hi' }
⊢ ↑g • ↑(x1 { val := i, isLt := hi' }) = ↑(g • x1 { val := i, isLt := hi' })

State before:
case h.h.mk.inl
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
hn : ∀ (a : α), IsMultiplyPretransitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
x : Fin (succ n) ↪ α
a : α := x { val := n, isLt := ⋯ }
gx : M
x1 : Fin n ↪ ↥(SubMulAction.ofStabilizer M a)
hga : gx • x (Fin.last n) = a
y : Fin (succ n) ↪ α
gy : M
y1 : Fin n ↪ ↥(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)
i : ℕ
hi : i < succ n
hi' : i < n
hgx : gx • x { val := i, isLt := ⋯ } = ↑(x1 { val := i, isLt := hi' })
hgy : gy • y { val := i, isLt := ⋯ } = ↑(y1 { val := i, isLt := hi' })
hg : g • x1 { val := i, isLt := hi' } = y1 { val := i, isLt := hi' }
⊢ ↑g • ↑(x1 { val := i, isLt := hi' }) = ↑(g • x1 { val := i, isLt := hi' })
Tactic:
rfl
State after:
no goals

State before:
case h.h.mk.inr
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
hn : ∀ (a : α), IsMultiplyPretransitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
x : Fin (succ n) ↪ α
a : α := x { val := n, isLt := ⋯ }
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 }
Tactic:
simp only [hi']
State after:
case h.h.mk.inr
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
hn : ∀ (a : α), IsMultiplyPretransitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
x : Fin (succ n) ↪ α
a : α := x { val := n, isLt := ⋯ }
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 := n, isLt := ⋯ } = y { val := n, isLt := ⋯ }

State before:
case h.h.mk.inr
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
hn : ∀ (a : α), IsMultiplyPretransitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
x : Fin (succ n) ↪ α
a : α := x { val := n, isLt := ⋯ }
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 := n, isLt := ⋯ } = y { val := n, isLt := ⋯ }
Tactic:
dsimp [Fin.last] at  hga hgb
State after:
case h.h.mk.inr
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
hn : ∀ (a : α), IsMultiplyPretransitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
x : Fin (succ n) ↪ α
a : α := x { val := n, isLt := ⋯ }
gx : M
x1 : Fin n ↪ ↥(SubMulAction.ofStabilizer M a)
hgx :
  Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding (gx • x) =
    Function.Embedding.trans x1 (subtype fun x => x ∈ SubMulAction.ofStabilizer M a)
hga : gx • x { val := n, isLt := ⋯ } = a
y : Fin (succ n) ↪ α
gy : M
y1 : Fin n ↪ ↥(SubMulAction.ofStabilizer M a)
hgy :
  Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding (gy • y) =
    Function.Embedding.trans y1 (subtype fun x => x ∈ SubMulAction.ofStabilizer M a)
hgb : gy • y { val := n, isLt := ⋯ } = a
hna_eq : ∀ (x y : Fin n ↪ ↥(SubMulAction.ofStabilizer M a)), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
g : ↥(stabilizer M a)
hg : g • x1 = y1
i : ℕ
hi : i < succ n
hi' : i = n
⊢ (gy⁻¹ * ↑g) • gx • x { val := n, isLt := ⋯ } = y { val := n, isLt := ⋯ }

State before:
case h.h.mk.inr
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
hn : ∀ (a : α), IsMultiplyPretransitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
x : Fin (succ n) ↪ α
a : α := x { val := n, isLt := ⋯ }
gx : M
x1 : Fin n ↪ ↥(SubMulAction.ofStabilizer M a)
hgx :
  Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding (gx • x) =
    Function.Embedding.trans x1 (subtype fun x => x ∈ SubMulAction.ofStabilizer M a)
hga : gx • x { val := n, isLt := ⋯ } = a
y : Fin (succ n) ↪ α
gy : M
y1 : Fin n ↪ ↥(SubMulAction.ofStabilizer M a)
hgy :
  Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding (gy • y) =
    Function.Embedding.trans y1 (subtype fun x => x ∈ SubMulAction.ofStabilizer M a)
hgb : gy • y { val := n, isLt := ⋯ } = a
hna_eq : ∀ (x y : Fin n ↪ ↥(SubMulAction.ofStabilizer M a)), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
g : ↥(stabilizer M a)
hg : g • x1 = y1
i : ℕ
hi : i < succ n
hi' : i = n
⊢ (gy⁻¹ * ↑g) • gx • x { val := n, isLt := ⋯ } = y { val := n, isLt := ⋯ }
Tactic:
rw [hga, mul_smul, inv_smul_eq_iff, hgb]
State after:
case h.h.mk.inr
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
hn : ∀ (a : α), IsMultiplyPretransitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
x : Fin (succ n) ↪ α
a : α := x { val := n, isLt := ⋯ }
gx : M
x1 : Fin n ↪ ↥(SubMulAction.ofStabilizer M a)
hgx :
  Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding (gx • x) =
    Function.Embedding.trans x1 (subtype fun x => x ∈ SubMulAction.ofStabilizer M a)
hga : gx • x { val := n, isLt := ⋯ } = a
y : Fin (succ n) ↪ α
gy : M
y1 : Fin n ↪ ↥(SubMulAction.ofStabilizer M a)
hgy :
  Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding (gy • y) =
    Function.Embedding.trans y1 (subtype fun x => x ∈ SubMulAction.ofStabilizer M a)
hgb : gy • y { val := n, isLt := ⋯ } = a
hna_eq : ∀ (x y : Fin n ↪ ↥(SubMulAction.ofStabilizer M a)), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
g : ↥(stabilizer M a)
hg : g • x1 = y1
i : ℕ
hi : i < succ n
hi' : i = n
⊢ ↑g • a = a

State before:
case h.h.mk.inr
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
hn : ∀ (a : α), IsMultiplyPretransitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
x : Fin (succ n) ↪ α
a : α := x { val := n, isLt := ⋯ }
gx : M
x1 : Fin n ↪ ↥(SubMulAction.ofStabilizer M a)
hgx :
  Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding (gx • x) =
    Function.Embedding.trans x1 (subtype fun x => x ∈ SubMulAction.ofStabilizer M a)
hga : gx • x { val := n, isLt := ⋯ } = a
y : Fin (succ n) ↪ α
gy : M
y1 : Fin n ↪ ↥(SubMulAction.ofStabilizer M a)
hgy :
  Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding (gy • y) =
    Function.Embedding.trans y1 (subtype fun x => x ∈ SubMulAction.ofStabilizer M a)
hgb : gy • y { val := n, isLt := ⋯ } = a
hna_eq : ∀ (x y : Fin n ↪ ↥(SubMulAction.ofStabilizer M a)), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
g : ↥(stabilizer M a)
hg : g • x1 = y1
i : ℕ
hi : i < succ n
hi' : i = n
⊢ ↑g • a = a
Tactic:
rw [← mem_stabilizer_iff]
State after:
case h.h.mk.inr
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
hn : ∀ (a : α), IsMultiplyPretransitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
x : Fin (succ n) ↪ α
a : α := x { val := n, isLt := ⋯ }
gx : M
x1 : Fin n ↪ ↥(SubMulAction.ofStabilizer M a)
hgx :
  Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding (gx • x) =
    Function.Embedding.trans x1 (subtype fun x => x ∈ SubMulAction.ofStabilizer M a)
hga : gx • x { val := n, isLt := ⋯ } = a
y : Fin (succ n) ↪ α
gy : M
y1 : Fin n ↪ ↥(SubMulAction.ofStabilizer M a)
hgy :
  Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding (gy • y) =
    Function.Embedding.trans y1 (subtype fun x => x ∈ SubMulAction.ofStabilizer M a)
hgb : gy • y { val := n, isLt := ⋯ } = a
hna_eq : ∀ (x y : Fin n ↪ ↥(SubMulAction.ofStabilizer M a)), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
g : ↥(stabilizer M a)
hg : g • x1 = y1
i : ℕ
hi : i < succ n
hi' : i = n
⊢ ↑g ∈ stabilizer M a

State before:
case h.h.mk.inr
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
hn : ∀ (a : α), IsMultiplyPretransitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
x : Fin (succ n) ↪ α
a : α := x { val := n, isLt := ⋯ }
gx : M
x1 : Fin n ↪ ↥(SubMulAction.ofStabilizer M a)
hgx :
  Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding (gx • x) =
    Function.Embedding.trans x1 (subtype fun x => x ∈ SubMulAction.ofStabilizer M a)
hga : gx • x { val := n, isLt := ⋯ } = a
y : Fin (succ n) ↪ α
gy : M
y1 : Fin n ↪ ↥(SubMulAction.ofStabilizer M a)
hgy :
  Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding (gy • y) =
    Function.Embedding.trans y1 (subtype fun x => x ∈ SubMulAction.ofStabilizer M a)
hgb : gy • y { val := n, isLt := ⋯ } = a
hna_eq : ∀ (x y : Fin n ↪ ↥(SubMulAction.ofStabilizer M a)), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
g : ↥(stabilizer M a)
hg : g • x1 = y1
i : ℕ
hi : i < succ n
hi' : i = n
⊢ ↑g ∈ stabilizer M a
Tactic:
exact SetLike.coe_mem g
State after:
no goals