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