internlm/Lean-Github huggingface dataset:
Theorem: MulAction.stabilizer.isMultiplyPretransitive'
Proof 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'⟩
Proof state after:
case h.h.mk.inl
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
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 }
Theorem: MulAction.stabilizer.isMultiplyPretransitive'
Proof 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'⟩
Proof state after:
case h.h.mk.inl
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
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 }
Theorem: MulAction.stabilizer.isMultiplyPretransitive'
Proof 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
Proof state after:
case h.h.mk.inl
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
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 }
Theorem: MulAction.stabilizer.isMultiplyPretransitive'
Proof 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]
Proof state after:
case h.h.mk.inl
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
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' })
Theorem: MulAction.stabilizer.isMultiplyPretransitive'
Proof 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
Proof state after:
no goals
Theorem: MulAction.stabilizer.isMultiplyPretransitive'
Proof 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']
Proof 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 := ⋯ }
Theorem: MulAction.stabilizer.isMultiplyPretransitive'
Proof 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
Proof 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 := ⋯ }
Theorem: MulAction.stabilizer.isMultiplyPretransitive'
Proof 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]
Proof 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
Theorem: MulAction.stabilizer.isMultiplyPretransitive'
Proof 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]
Proof 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
Theorem: MulAction.stabilizer.isMultiplyPretransitive'
Proof 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
Proof state after:
no goals
Theorem: MulAction.stabilizer.isMultiplyPretransitive
Proof state before:
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
a : α
⊢ IsMultiplyPretransitive M α (succ n) ↔
    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 : ℕ
a : α
⊢ IsMultiplyPretransitive M α (succ n) →
    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 : ℕ
a : α
⊢ IsMultiplyPretransitive M α (succ n) →
    IsMultiplyPretransitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
Tactic:
intro hn
Proof state after:
case mp
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
a : α
hn : IsMultiplyPretransitive M α (succ n)
⊢ 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 : ℕ
a : α
hn : IsMultiplyPretransitive M α (succ n)
⊢ 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 : ℕ
a : α
hn : IsMultiplyPretransitive M α (succ n)
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 : ℕ
a : α
hn : IsMultiplyPretransitive M α (succ n)
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 : ℕ
a : α
hn : IsMultiplyPretransitive M α (succ n)
hn_eq : ∀ (x y : Fin (succ n) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
⊢ ∀ (x y : Fin n ↪ ↥(SubMulAction.ofStabilizer M a)), ∃ g, g • x = y
Theorem: MulAction.stabilizer.isMultiplyPretransitive
Proof state before:
case mp.exists_smul_eq
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
hα' : IsPretransitive M α
n : ℕ
a : α
hn : IsMultiplyPretransitive M α (succ n)
hn_eq : ∀ (x y : Fin (succ n) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
⊢ ∀ (x y : Fin n ↪ ↥(SubMulAction.ofStabilizer M a)), ∃ g, g • x = y
Tactic:
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 : ℕ
a : α
hn : IsMultiplyPretransitive M α (succ n)
hn_eq : ∀ (x y : Fin (succ n) ↪ α), ∃ g, g • x = y := IsPretransitive.exists_smul_eq
x y : Fin n ↪ ↥(SubMulAction.ofStabilizer M a)
⊢ ∃ g, g • x = y