internlm/Lean-Github huggingface dataset:
Theorem: MulAction.exists_extends_with_last_eq
Proof state before:
case intro
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
a : α
n : ℕ
x : Fin n ↪ ↥(SubMulAction.ofStabilizer M a)
j✝ : ↥(SubMulAction.ofStabilizer M a) ↪ α := { toFun := fun u => id ↑u, inj' := ⋯ }
u : Fin n
hu : ↑(x u) = a
⊢ False
Tactic:
apply SubMulAction.neq_of_mem_ofStabilizer M a
Proof state after:
case intro
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
a : α
n : ℕ
x : Fin n ↪ ↥(SubMulAction.ofStabilizer M a)
j✝ : ↥(SubMulAction.ofStabilizer M a) ↪ α := { toFun := fun u => id ↑u, inj' := ⋯ }
u : Fin n
hu : ↑(x u) = a
⊢ ↑?m.69556 = a

M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
a : α
n : ℕ
x : Fin n ↪ ↥(SubMulAction.ofStabilizer M a)
j✝ : ↥(SubMulAction.ofStabilizer M a) ↪ α := { toFun := fun u => id ↑u, inj' := ⋯ }
u : Fin n
hu : ↑(x u) = a
⊢ ↥(SubMulAction.ofStabilizer M a)
Theorem: MulAction.exists_extends_with_last_eq
Proof state before:
case intro
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
a : α
n : ℕ
x : Fin n ↪ ↥(SubMulAction.ofStabilizer M a)
j✝ : ↥(SubMulAction.ofStabilizer M a) ↪ α := { toFun := fun u => id ↑u, inj' := ⋯ }
u : Fin n
hu : ↑(x u) = a
⊢ ↑?m.69556 = a

M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
a : α
n : ℕ
x : Fin n ↪ ↥(SubMulAction.ofStabilizer M a)
j✝ : ↥(SubMulAction.ofStabilizer M a) ↪ α := { toFun := fun u => id ↑u, inj' := ⋯ }
u : Fin n
hu : ↑(x u) = a
⊢ ↥(SubMulAction.ofStabilizer M a)
Tactic:
exact hu
Proof state after:
no goals
Theorem: MulAction.exists_smul_of_last_eq
Proof 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
Proof 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
Theorem: MulAction.exists_smul_of_last_eq
Proof 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
Proof 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
Theorem: MulAction.exists_smul_of_last_eq
Proof 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
Proof 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
Theorem: MulAction.exists_smul_of_last_eq
Proof 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
Proof 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
Theorem: MulAction.exists_smul_of_last_eq
Proof 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] }
Proof 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
Theorem: MulAction.exists_smul_of_last_eq
Proof 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
Proof 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
Theorem: MulAction.exists_smul_of_last_eq
Proof 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⟩
Proof 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
Theorem: MulAction.exists_smul_of_last_eq
Proof 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]
Proof 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
Theorem: MulAction.exists_smul_of_last_eq
Proof 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]
Proof 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)
Theorem: MulAction.exists_smul_of_last_eq
Proof 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]
Proof 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
Theorem: MulAction.exists_smul_of_last_eq
Proof 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
Proof state after:
no goals
Theorem: MulAction.exists_smul_of_last_eq
Proof 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
Proof 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
Theorem: MulAction.exists_smul_of_last_eq
Proof 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
Proof state after:
no goals
Theorem: MulAction.exists_smul_of_last_eq
Proof 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]
Proof state after:
no goals
Theorem: MulAction.exists_smul_of_last_eq
Proof 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
Proof 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
Theorem: MulAction.exists_smul_of_last_eq
Proof 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
Proof 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
Theorem: MulAction.exists_smul_of_last_eq
Proof 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
Proof state after:
no goals
Theorem: MulAction.exists_smul_of_last_eq
Proof 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
Proof state after:
no goals
Theorem: MulAction.stabilizer.isMultiplyPretransitive'
Proof state before:
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
⊢ IsMultiplyPretransitive M α (succ n) ↔
    ∀ (a : α), IsMultiplyPretransitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
Tactic:
constructor
Proof 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)
Theorem: MulAction.stabilizer.isMultiplyPretransitive'
Proof 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
Proof 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
Theorem: MulAction.stabilizer.isMultiplyPretransitive'
Proof 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
Proof 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
Theorem: MulAction.stabilizer.isMultiplyPretransitive'
Proof 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
Proof 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
Theorem: MulAction.stabilizer.isMultiplyPretransitive'
Proof state before:
case mp.exists_smul_eq
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
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
Proof 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
Theorem: MulAction.stabilizer.isMultiplyPretransitive'
Proof state before:
case mp.exists_smul_eq
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
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
Proof state after:
case mp.exists_smul_eq.intro.intro
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
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
Theorem: MulAction.stabilizer.isMultiplyPretransitive'
Proof state before:
case mp.exists_smul_eq.intro.intro
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
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
Proof state after:
case mp.exists_smul_eq.intro.intro.intro.intro
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
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