Theorem: MulAction.exists_smul_of_last_eq (Jordan/MultipleTransitivity.lean)

State before:
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
a : α
x : Fin (succ n) ↪ α
⊢ ∃ g x1,
    Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding (g • x) =
        Function.Embedding.trans x1 (subtype fun x => x ∈ SubMulAction.ofStabilizer M a) ∧
      g • x (Fin.last n) = a
Tactic:
let hα'eq := hα'.exists_smul_eq
State after:
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
a : α
x : Fin (succ n) ↪ α
hα'eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
⊢ ∃ g x1,
    Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding (g • x) =
        Function.Embedding.trans x1 (subtype fun x => x ∈ SubMulAction.ofStabilizer M a) ∧
      g • x (Fin.last n) = a

State before:
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
a : α
x : Fin (succ n) ↪ α
hα'eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
⊢ ∃ g x1,
    Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding (g • x) =
        Function.Embedding.trans x1 (subtype fun x => x ∈ SubMulAction.ofStabilizer M a) ∧
      g • x (Fin.last n) = a
Tactic:
obtain ⟨g, hgx⟩ := hα'eq (x (Fin.last n)) a
State after:
case intro
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
a : α
x : Fin (succ n) ↪ α
hα'eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
g : M
hgx : g • x (Fin.last n) = a
⊢ ∃ g x1,
    Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding (g • x) =
        Function.Embedding.trans x1 (subtype fun x => x ∈ SubMulAction.ofStabilizer M a) ∧
      g • x (Fin.last n) = a

State before:
case intro
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
a : α
x : Fin (succ n) ↪ α
hα'eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
g : M
hgx : g • x (Fin.last n) = a
⊢ ∃ g x1,
    Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding (g • x) =
        Function.Embedding.trans x1 (subtype fun x => x ∈ SubMulAction.ofStabilizer M a) ∧
      g • x (Fin.last n) = a
Tactic:
use g
State after:
case h
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
a : α
x : Fin (succ n) ↪ α
hα'eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
g : M
hgx : g • x (Fin.last n) = a
⊢ ∃ x1,
    Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding (g • x) =
        Function.Embedding.trans x1 (subtype fun x => x ∈ SubMulAction.ofStabilizer M a) ∧
      g • x (Fin.last n) = a

State before:
case h
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
a : α
x : Fin (succ n) ↪ α
hα'eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
g : M
hgx : g • x (Fin.last n) = a
⊢ ∃ x1,
    Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding (g • x) =
        Function.Embedding.trans x1 (subtype fun x => x ∈ SubMulAction.ofStabilizer M a) ∧
      g • x (Fin.last n) = a
Tactic:
have zgx : ∀ (i : Fin n), g • x (Fin.castSucc i) ∈ SubMulAction.ofStabilizer M a := by
  rintro ⟨i, hi⟩
  rw [SubMulAction.mem_ofStabilizer_iff]
  rw [← hgx]
  simp only [Fin.castSucc_mk, ne_eq, smul_left_cancel_iff, EmbeddingLike.apply_eq_iff_eq, Fin.mk.injEq]
  exact Fin.ne_of_lt hi
State after:
case h
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
a : α
x : Fin (succ n) ↪ α
hα'eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
g : M
hgx : g • x (Fin.last n) = a
zgx : ∀ (i : Fin n), g • x (Fin.castSucc i) ∈ SubMulAction.ofStabilizer M a
⊢ ∃ x1,
    Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding (g • x) =
        Function.Embedding.trans x1 (subtype fun x => x ∈ SubMulAction.ofStabilizer M a) ∧
      g • x (Fin.last n) = a

State before:
case h
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
a : α
x : Fin (succ n) ↪ α
hα'eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
g : M
hgx : g • x (Fin.last n) = a
zgx : ∀ (i : Fin n), g • x (Fin.castSucc i) ∈ SubMulAction.ofStabilizer M a
⊢ ∃ x1,
    Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding (g • x) =
        Function.Embedding.trans x1 (subtype fun x => x ∈ SubMulAction.ofStabilizer M a) ∧
      g • x (Fin.last n) = a
Tactic:
use {
  toFun := fun i => ⟨g • x i, (by
    simp
    exact zgx i)⟩
  inj' := fun i j ↦ by
    simp only [Fin.coe_eq_castSucc, Subtype.mk.injEq, smul_left_cancel_iff,
      EmbeddingLike.apply_eq_iff_eq, Fin.castSucc_inj, imp_self] }
State after:
case h
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
a : α
x : Fin (succ n) ↪ α
hα'eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
g : M
hgx : g • x (Fin.last n) = a
zgx : ∀ (i : Fin n), g • x (Fin.castSucc i) ∈ SubMulAction.ofStabilizer M a
⊢ Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding (g • x) =
      Function.Embedding.trans { toFun := fun i => { val := g • x ↑↑i, property := ⋯ }, inj' := ⋯ }
        (subtype fun x => x ∈ SubMulAction.ofStabilizer M a) ∧
    g • x (Fin.last n) = a

State before:
case h
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
a : α
x : Fin (succ n) ↪ α
hα'eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
g : M
hgx : g • x (Fin.last n) = a
zgx : ∀ (i : Fin n), g • x (Fin.castSucc i) ∈ SubMulAction.ofStabilizer M a
⊢ Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding (g • x) =
      Function.Embedding.trans { toFun := fun i => { val := g • x ↑↑i, property := ⋯ }, inj' := ⋯ }
        (subtype fun x => x ∈ SubMulAction.ofStabilizer M a) ∧
    g • x (Fin.last n) = a
Tactic:
constructor
State after:
case h.left
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
a : α
x : Fin (succ n) ↪ α
hα'eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
g : M
hgx : g • x (Fin.last n) = a
zgx : ∀ (i : Fin n), g • x (Fin.castSucc i) ∈ SubMulAction.ofStabilizer M a
⊢ Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding (g • x) =
    Function.Embedding.trans { toFun := fun i => { val := g • x ↑↑i, property := ⋯ }, inj' := ⋯ }
      (subtype fun x => x ∈ SubMulAction.ofStabilizer M a)

case h.right
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
a : α
x : Fin (succ n) ↪ α
hα'eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
g : M
hgx : g • x (Fin.last n) = a
zgx : ∀ (i : Fin n), g • x (Fin.castSucc i) ∈ SubMulAction.ofStabilizer M a
⊢ g • x (Fin.last n) = a

State before:
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
a : α
x : Fin (succ n) ↪ α
hα'eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
g : M
hgx : g • x (Fin.last n) = a
⊢ ∀ (i : Fin n), g • x (Fin.castSucc i) ∈ SubMulAction.ofStabilizer M a
Tactic:
rintro ⟨i, hi⟩
State after:
case mk
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
a : α
x : Fin (succ n) ↪ α
hα'eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
g : M
hgx : g • x (Fin.last n) = a
i : ℕ
hi : i < n
⊢ g • x (Fin.castSucc { val := i, isLt := hi }) ∈ SubMulAction.ofStabilizer M a

State before:
case mk
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
a : α
x : Fin (succ n) ↪ α
hα'eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
g : M
hgx : g • x (Fin.last n) = a
i : ℕ
hi : i < n
⊢ g • x (Fin.castSucc { val := i, isLt := hi }) ∈ SubMulAction.ofStabilizer M a
Tactic:
rw [SubMulAction.mem_ofStabilizer_iff]
State after:
case mk
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
a : α
x : Fin (succ n) ↪ α
hα'eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
g : M
hgx : g • x (Fin.last n) = a
i : ℕ
hi : i < n
⊢ g • x (Fin.castSucc { val := i, isLt := hi }) ≠ a

State before:
case mk
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
a : α
x : Fin (succ n) ↪ α
hα'eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
g : M
hgx : g • x (Fin.last n) = a
i : ℕ
hi : i < n
⊢ g • x (Fin.castSucc { val := i, isLt := hi }) ≠ a
Tactic:
rw [← hgx]
State after:
case mk
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
a : α
x : Fin (succ n) ↪ α
hα'eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
g : M
hgx : g • x (Fin.last n) = a
i : ℕ
hi : i < n
⊢ g • x (Fin.castSucc { val := i, isLt := hi }) ≠ g • x (Fin.last n)

State before:
case mk
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
a : α
x : Fin (succ n) ↪ α
hα'eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
g : M
hgx : g • x (Fin.last n) = a
i : ℕ
hi : i < n
⊢ g • x (Fin.castSucc { val := i, isLt := hi }) ≠ g • x (Fin.last n)
Tactic:
simp only [Fin.castSucc_mk, ne_eq, smul_left_cancel_iff, EmbeddingLike.apply_eq_iff_eq, Fin.mk.injEq]
State after:
case mk
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
a : α
x : Fin (succ n) ↪ α
hα'eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
g : M
hgx : g • x (Fin.last n) = a
i : ℕ
hi : i < n
⊢ ¬{ val := i, isLt := ⋯ } = Fin.last n

State before:
case mk
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
a : α
x : Fin (succ n) ↪ α
hα'eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
g : M
hgx : g • x (Fin.last n) = a
i : ℕ
hi : i < n
⊢ ¬{ val := i, isLt := ⋯ } = Fin.last n
Tactic:
exact Fin.ne_of_lt hi
State after:
no goals

State before:
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
a : α
x : Fin (succ n) ↪ α
hα'eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
g : M
hgx : g • x (Fin.last n) = a
zgx : ∀ (i : Fin n), g • x (Fin.castSucc i) ∈ SubMulAction.ofStabilizer M a
i : Fin n
⊢ g • x ↑↑i ∈ SubMulAction.ofStabilizer M a
Tactic:
simp
State after:
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
a : α
x : Fin (succ n) ↪ α
hα'eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
g : M
hgx : g • x (Fin.last n) = a
zgx : ∀ (i : Fin n), g • x (Fin.castSucc i) ∈ SubMulAction.ofStabilizer M a
i : Fin n
⊢ g • x (Fin.castSucc i) ∈ SubMulAction.ofStabilizer M a

State before:
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
a : α
x : Fin (succ n) ↪ α
hα'eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
g : M
hgx : g • x (Fin.last n) = a
zgx : ∀ (i : Fin n), g • x (Fin.castSucc i) ∈ SubMulAction.ofStabilizer M a
i : Fin n
⊢ g • x (Fin.castSucc i) ∈ SubMulAction.ofStabilizer M a
Tactic:
exact zgx i
State after:
no goals

State before:
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
a : α
x : Fin (succ n) ↪ α
hα'eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
g : M
hgx : g • x (Fin.last n) = a
zgx : ∀ (i : Fin n), g • x (Fin.castSucc i) ∈ SubMulAction.ofStabilizer M a
i j : Fin n
⊢ (fun i => { val := g • x ↑↑i, property := ⋯ }) i = (fun i => { val := g • x ↑↑i, property := ⋯ }) j → i = j
Tactic:
simp only [Fin.coe_eq_castSucc, Subtype.mk.injEq, smul_left_cancel_iff,
  EmbeddingLike.apply_eq_iff_eq, Fin.castSucc_inj, imp_self]
State after:
no goals

State before:
case h.left
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
a : α
x : Fin (succ n) ↪ α
hα'eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
g : M
hgx : g • x (Fin.last n) = a
zgx : ∀ (i : Fin n), g • x (Fin.castSucc i) ∈ SubMulAction.ofStabilizer M a
⊢ Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding (g • x) =
    Function.Embedding.trans { toFun := fun i => { val := g • x ↑↑i, property := ⋯ }, inj' := ⋯ }
      (subtype fun x => x ∈ SubMulAction.ofStabilizer M a)
Tactic:
ext i
State after:
case h.left.h
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
a : α
x : Fin (succ n) ↪ α
hα'eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
g : M
hgx : g • x (Fin.last n) = a
zgx : ∀ (i : Fin n), g • x (Fin.castSucc i) ∈ SubMulAction.ofStabilizer M a
i : Fin n
⊢ (Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding (g • x)) i =
    (Function.Embedding.trans { toFun := fun i => { val := g • x ↑↑i, property := ⋯ }, inj' := ⋯ }
        (subtype fun x => x ∈ SubMulAction.ofStabilizer M a))
      i

State before:
case h.left.h
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
a : α
x : Fin (succ n) ↪ α
hα'eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
g : M
hgx : g • x (Fin.last n) = a
zgx : ∀ (i : Fin n), g • x (Fin.castSucc i) ∈ SubMulAction.ofStabilizer M a
i : Fin n
⊢ (Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding (g • x)) i =
    (Function.Embedding.trans { toFun := fun i => { val := g • x ↑↑i, property := ⋯ }, inj' := ⋯ }
        (subtype fun x => x ∈ SubMulAction.ofStabilizer M a))
      i
Tactic:
simp
State after:
case h.left.h
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
a : α
x : Fin (succ n) ↪ α
hα'eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
g : M
hgx : g • x (Fin.last n) = a
zgx : ∀ (i : Fin n), g • x (Fin.castSucc i) ∈ SubMulAction.ofStabilizer M a
i : Fin n
⊢ Fin.castLE ⋯ i = Fin.castSucc i

State before:
case h.left.h
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
a : α
x : Fin (succ n) ↪ α
hα'eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
g : M
hgx : g • x (Fin.last n) = a
zgx : ∀ (i : Fin n), g • x (Fin.castSucc i) ∈ SubMulAction.ofStabilizer M a
i : Fin n
⊢ Fin.castLE ⋯ i = Fin.castSucc i
Tactic:
rfl
State after:
no goals

State before:
case h.right
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
a : α
x : Fin (succ n) ↪ α
hα'eq : ∀ (x y : α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
g : M
hgx : g • x (Fin.last n) = a
zgx : ∀ (i : Fin n), g • x (Fin.castSucc i) ∈ SubMulAction.ofStabilizer M a
⊢ g • x (Fin.last n) = a
Tactic:
exact hgx
State after:
no goals