awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
g : G
a b : α
hg : b = g • a
left :
  Function.Injective (α := ↥(ofStabilizer G a)) (β := ↥(ofStabilizer G b))
    (⇑(conjMap hg) : (a : ↥(ofStabilizer G a)) → ↥(ofStabilizer G b))
right :
  Function.Surjective (α := ↥(ofStabilizer G a)) (β := ↥(ofStabilizer G b))
    (⇑(conjMap hg) : (a : ↥(ofStabilizer G a)) → ↥(ofStabilizer G b))
⊢ Function.Bijective (α := ↥(ofStabilizer G a)) (β := ↥(ofStabilizer G b))
    (⇑(conjMap hg) : (a : ↥(ofStabilizer G a)) → ↥(ofStabilizer G b))

Tactic:
constructor
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
g : G
a b : α
hg : b = g • a
x : α
hx : Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x
y : α
hy : Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) y
hxy :
  Eq (α := ↥(ofStabilizer G b))
    ((conjMap hg : (a : ↥(ofStabilizer G a)) → ↥(ofStabilizer G b))
        (Subtype.mk (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) x hx) :
      ↥(ofStabilizer G b))
    ((conjMap hg : (a : ↥(ofStabilizer G a)) → ↥(ofStabilizer G b))
        (Subtype.mk (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) y hy) :
      ↥(ofStabilizer G b))
left : x = y
⊢ Subtype.mk (p := fun (x : α) ↦
      Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) x hx =
    Subtype.mk (p := fun (x : α) ↦
      Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) y hy

Tactic:
simp only [Subtype.mk_eq_mk]

Premises used: Subtype.mk_eq_mk
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
g : G
a b : α
hg : b = g • a
x : α
hx : Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x
y : α
hy : Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) y
hxy :
  Eq (α := ↥(ofStabilizer G b))
    ((conjMap hg : (a : ↥(ofStabilizer G a)) → ↥(ofStabilizer G b))
        (Subtype.mk (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) x hx) :
      ↥(ofStabilizer G b))
    ((conjMap hg : (a : ↥(ofStabilizer G a)) → ↥(ofStabilizer G b))
        (Subtype.mk (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) y hy) :
      ↥(ofStabilizer G b))
left : Eq.{u_2 + 1} (α := α) ((fun (x : α) ↦ g • x) x) ((fun (x : α) ↦ g • x) y)
⊢ x = y

Tactic:
apply (MulAction.injective g)

Premises used: MulAction.injective
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
g : G
a b : α
hg : b = g • a
x : α
hx : Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x
y : α
hy : Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) y
hxy :
  Eq (α := ↥(ofStabilizer G b))
    ((conjMap hg : (a : ↥(ofStabilizer G a)) → ↥(ofStabilizer G b))
        (Subtype.mk (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) x hx) :
      ↥(ofStabilizer G b))
    ((conjMap hg : (a : ↥(ofStabilizer G a)) → ↥(ofStabilizer G b))
        (Subtype.mk (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) y hy) :
      ↥(ofStabilizer G b))
left :
  ∀
    (hxy :
      Eq.{u_2 + 1} (α := α)
        (↑((conjMap hg : (a : ↥(ofStabilizer G a)) → ↥(ofStabilizer G b))
              (Subtype.mk (p := fun (x : α) ↦
                Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) x hx)) :
          α)
        (↑((conjMap hg : (a : ↥(ofStabilizer G a)) → ↥(ofStabilizer G b))
              (Subtype.mk (p := fun (x : α) ↦
                Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) y hy)) :
          α)),
    Eq.{u_2 + 1} (α := α) ((fun (x : α) ↦ g • x) x) ((fun (x : α) ↦ g • x) y)
left₁ left₂ left₃ left₄ :
  ∀
    (hxy :
      g •
          (↑(Subtype.mk (p := fun (x : α) ↦
                Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) x hx) :
            α) =
        (↑((conjMap hg : (a : ↥(ofStabilizer G a)) → ↥(ofStabilizer G b))
              (Subtype.mk (p := fun (x : α) ↦
                Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) y hy)) :
          α)),
    Eq.{u_2 + 1} (α := α) ((fun (x : α) ↦ g • x) x) ((fun (x : α) ↦ g • x) y)
⊢ Eq.{u_2 + 1} (α := α) ((fun (x : α) ↦ g • x) x) ((fun (x : α) ↦ g • x) y)

Tactic:
rwa [← SetLike.coe_eq_coe, conjMap_apply] at hxy

Premises used: SetLike.coe_eq_coe, SubMulAction.ofStabilizer.conjMap_apply
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
g : G
a b : α
hg : b = g • a
x : ↥(ofStabilizer G b)
⊢ ∃ (a_1 : ↥(ofStabilizer G a)), (conjMap hg : (a : ↥(ofStabilizer G a)) → ↥(ofStabilizer G b)) a_1 = x

Tactic:
⟨conjMap _ x, inv_conjMap_comp_apply _ x⟩

Premises used: SubMulAction.ofStabilizer.conjMap, SubMulAction.ofStabilizer.inv_conjMap_comp_apply, Exists.intro, DFunLike.coe
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
g : G
a b : α
hg : b = g • a
x : ↥(ofStabilizer G b)
⊢ ∃ (a_1 : ↥(ofStabilizer G a)), (conjMap hg : (a : ↥(ofStabilizer G a)) → ↥(ofStabilizer G b)) a_1 = x

Tactic:
exact ⟨conjMap _ x, inv_conjMap_comp_apply _ x⟩
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
g h k : G
a b c : α
hg : b = g • a
hh : c = h • b
hk : c = k • a
n : ℕ
x : Fin n ↪ ↥(ofStabilizer G a)
simp : ∀ (x_1 : Fin n), ¬(↑((x : (a_1 : Fin n) → ↥(ofStabilizer G a)) x_1) : α) = a
⊢ a ∉
    Set.range (ι := Fin n)
      (⇑(x.trans
            (subtype fun (x : α) ↦
              Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x)) :
        (a : Fin n) → α)

Tactic:
simp only [Set.mem_range, trans_apply, Function.Embedding.subtype_apply, not_exists]

Premises used: Set.mem_range, not_exists, Function.Embedding.trans_apply, Function.Embedding.subtype_apply
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
g h k : G
a b c : α
hg : b = g • a
hh : c = h • b
hk : c = k • a
n : ℕ
x : Fin n ↪ ↥(ofStabilizer G a)
⊢ ∀ (x_1 : Fin n), ¬(↑((x : (a_1 : Fin n) → ↥(ofStabilizer G a)) x_1) : α) = a

Tactic:
fun i ↦ (x i).prop

Premises used: Set.Mem, setOf, Subtype.prop, Set.singleton, DFunLike.coe, Not
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
g h k : G
a b c : α
hg : b = g • a
hh : c = h • b
hk : c = k • a
n : ℕ
x : Fin n ↪ ↥(ofStabilizer G a)
⊢ ∀ (x_1 : Fin n), ¬(↑((x : (a_1 : Fin n) → ↥(ofStabilizer G a)) x_1) : α) = a

Tactic:
exact fun i ↦ (x i).prop

Premises used: Subtype.prop, DFunLike.coe
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
a : α
n : ℕ
x : Fin n ↪ ↥(ofStabilizer G a)
i : Fin n
⊢ Eq (α := α) ((snoc x : (a : Fin n.succ) → α) i.castSucc : α)
    ((↑((x : (a_1 : Fin n) → ↥(ofStabilizer G a)) i) : α) : α)

Tactic:
simp [snoc]

Premises used: SubMulAction.ofStabilizer.snoc
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
a : α
n : ℕ
x : Fin n ↪ ↥(ofStabilizer G a)
⊢ (snoc x : (a : Fin n.succ) → α) (Fin.last n) = a

Tactic:
simp [snoc]

Premises used: SubMulAction.ofStabilizer.snoc
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
inst_2 : IsPretransitive G α
n : ℕ
a : α
x : Fin n.succ ↪ α
obtain :
  ∀ (g : G) (hgx : HSMul.hSMul (β := α) g ((x : (a : Fin n.succ) → α) (Fin.last n) : α) = a),
    ∃ (g : G) (y : Fin n ↪ ↥(ofStabilizer G a)), g • x = ofStabilizer.snoc y
⊢ ∃ (g : G) (y : Fin n ↪ ↥(ofStabilizer G a)), g • x = ofStabilizer.snoc y

Tactic:
obtain ⟨g, hgx⟩ := exists_smul_eq G (x (Fin.last n)) a

Premises used: Fin.last, MulAction.exists_smul_eq, DFunLike.coe
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
inst_2 : IsPretransitive G α
n : ℕ
a : α
x : Fin n.succ ↪ α
g : G
hgx : HSMul.hSMul (β := α) g ((x : (a : Fin n.succ) → α) (Fin.last n) : α) = a
i : Fin n
simp :
  ¬Eq (α := α) ((Fin.Embedding.init (g • x) : (a : Fin n) → α) i : α) ((g • x : (a : Fin (n + 1)) → α) (Fin.last n) : α)
⊢ Membership.mem (α := α) (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a)
    ((Fin.Embedding.init (g • x) : (a : Fin n) → α) i : α)

Tactic:
simp only [mem_ofStabilizer_iff,
      Nat.succ_eq_add_one, ← hgx, ← smul_apply, ne_eq]

Premises used: Function.Embedding.smul_apply, Nat.succ_eq_add_one, ne_eq, SubMulAction.mem_ofStabilizer_iff
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
inst_2 : IsPretransitive G α
n : ℕ
a : α
x : Fin n.succ ↪ α
g : G
hgx : HSMul.hSMul (β := α) g ((x : (a : Fin n.succ) → α) (Fin.last n) : α) = a
i : Fin n
this :
  Eq (α := α) ((Fin.Embedding.init (g • x) : (a : Fin n) → α) i : α) ((g • x : (a : Fin n.succ) → α) i.castSucc : α)
⊢ ¬Eq (α := α) ((Fin.Embedding.init (g • x) : (a : Fin n) → α) i : α) ((g • x : (a : Fin (n + 1)) → α) (Fin.last n) : α)

Tactic:
simp [this]
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
inst_2 : IsPretransitive G α
n : ℕ
a : α
x : Fin n.succ ↪ α
g : G
hgx : HSMul.hSMul (β := α) g ((x : (a : Fin n.succ) → α) (Fin.last n) : α) = a
i : Fin n
suffices :
  Eq (α := α) ((Fin.Embedding.init (g • x) : (a : Fin n) → α) i : α) ((g • x : (a : Fin n.succ) → α) i.castSucc : α)
⊢ ¬Eq (α := α) ((Fin.Embedding.init (g • x) : (a : Fin n) → α) i : α) ((g • x : (a : Fin (n + 1)) → α) (Fin.last n) : α)

Tactic:
suffices Fin.Embedding.init (g • x) i = (g • x) i.castSucc by
      simp [this]
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
inst_2 : IsPretransitive G α
n : ℕ
a : α
x : Fin n.succ ↪ α
g : G
hgx : HSMul.hSMul (β := α) g ((x : (a : Fin n.succ) → α) (Fin.last n) : α) = a
i : Fin n
⊢ Eq (α := α) ((Fin.Embedding.init (g • x) : (a : Fin n) → α) i : α) ((g • x : (a : Fin n.succ) → α) i.castSucc : α)

Tactic:
simp [Fin.Embedding.init, Fin.init_def]

Premises used: Fin.init_def, Fin.Embedding.init
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
inst_2 : IsPretransitive G α
n : ℕ
a : α
x : Fin n.succ ↪ α
g : G
hgx : HSMul.hSMul (β := α) g ((x : (a : Fin n.succ) → α) (Fin.last n) : α) = a
⊢ ∀ (i : Fin n),
    Membership.mem (α := α) (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a)
      ((Fin.Embedding.init (g • x) : (a : Fin n) → α) i : α)

Tactic:
have H : ∀ i, Fin.Embedding.init (g • x) i ∈ ofStabilizer G a := fun i ↦ by
    simp only [mem_ofStabilizer_iff,
      Nat.succ_eq_add_one, ← hgx, ← smul_apply, ne_eq]
    suffices Fin.Embedding.init (g • x) i = (g • x) i.castSucc by
      simp [this]
    simp [Fin.Embedding.init, Fin.init_def]
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
inst_2 : IsPretransitive G α
n : ℕ
a : α
x : Fin n.succ ↪ α
g : G
hgx : HSMul.hSMul (β := α) g ((x : (a : Fin n.succ) → α) (Fin.last n) : α) = a
H :
  ∀ (i : Fin n),
    Membership.mem (α := α) (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a)
      ((Fin.Embedding.init (g • x) : (a : Fin n) → α) i : α)
h : g • x = ofStabilizer.snoc (codRestrict (↑(ofStabilizer G a) : Set α) (Fin.Embedding.init (g • x)) H)
⊢ ∃ (g : G) (y : Fin n ↪ ↥(ofStabilizer G a)), g • x = ofStabilizer.snoc y

Tactic:
use g, (Fin.Embedding.init (g • x)).codRestrict (ofStabilizer G a) H

Premises used: Function.Embedding.codRestrict, Fin.Embedding.init, HSMul.hSMul
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
inst_2 : IsPretransitive G α
n : ℕ
a : α
x : Fin n.succ ↪ α
g : G
hgx : HSMul.hSMul (β := α) g ((x : (a : Fin n.succ) → α) (Fin.last n) : α) = a
H :
  ∀ (i : Fin n),
    Membership.mem (α := α) (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a)
      ((Fin.Embedding.init (g • x) : (a : Fin n) → α) i : α)
h :
  ∀ (i : Fin n.succ),
    Eq (α := α) ((g • x : (a : Fin n.succ) → α) i : α)
      ((ofStabilizer.snoc (codRestrict (↑(ofStabilizer G a) : Set α) (Fin.Embedding.init (g • x)) H) :
            (a : Fin n.succ) → α)
          i :
        α)
⊢ g • x = ofStabilizer.snoc (codRestrict (↑(ofStabilizer G a) : Set α) (Fin.Embedding.init (g • x)) H)

Tactic:
ext i
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
inst_2 : IsPretransitive G α
n : ℕ
a : α
x : Fin n.succ ↪ α
g : G
hgx : HSMul.hSMul (β := α) g ((x : (a : Fin n.succ) → α) (Fin.last n) : α) = a
H :
  ∀ (i : Fin n),
    Membership.mem (α := α) (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a)
      ((Fin.Embedding.init (g • x) : (a : Fin n) → α) i : α)
i : Fin n.succ
h :
  ∀ (i : Fin n),
    Eq (α := α) ((g • x : (a : Fin n.succ) → α) i.castSucc : α)
      ((ofStabilizer.snoc (codRestrict (↑(ofStabilizer G a) : Set α) (Fin.Embedding.init (g • x)) H) :
            (a : Fin n.succ) → α)
          i.castSucc :
        α)
h₁ :
  Eq (α := α) ((g • x : (a : Fin n.succ) → α) (Fin.last n) : α)
    ((ofStabilizer.snoc (codRestrict (↑(ofStabilizer G a) : Set α) (Fin.Embedding.init (g • x)) H) :
          (a : Fin n.succ) → α)
        (Fin.last n) :
      α)
⊢ Eq (α := α) ((g • x : (a : Fin n.succ) → α) i : α)
    ((ofStabilizer.snoc (codRestrict (↑(ofStabilizer G a) : Set α) (Fin.Embedding.init (g • x)) H) :
          (a : Fin n.succ) → α)
        i :
      α)

Tactic:
rcases Fin.eq_castSucc_or_eq_last i with ⟨i, rfl⟩ | ⟨rfl⟩

Premises used: Fin.eq_castSucc_or_eq_last, rfl
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
inst_2 : IsPretransitive G α
n : ℕ
a : α
x : Fin n.succ ↪ α
g : G
hgx : HSMul.hSMul (β := α) g ((x : (a : Fin n.succ) → α) (Fin.last n) : α) = a
H :
  ∀ (i : Fin n),
    Membership.mem (α := α) (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a)
      ((Fin.Embedding.init (g • x) : (a : Fin n) → α) i : α)
i : Fin n
⊢ Eq (α := α) ((g • x : (a : Fin n.succ) → α) i.castSucc : α)
    ((ofStabilizer.snoc (codRestrict (↑(ofStabilizer G a) : Set α) (Fin.Embedding.init (g • x)) H) :
          (a : Fin n.succ) → α)
        i.castSucc :
      α)

Tactic:
simpa [ofStabilizer.snoc] using
      Subtype.ext_iff.mp <| Function.Embedding.codRestrict_apply _ _ H i

Premises used: SubMulAction.ofStabilizer.snoc, Subtype.ext_iff, Iff.mp, Function.Embedding.codRestrict_apply
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
inst_2 : IsPretransitive G α
n : ℕ
a : α
x : Fin n.succ ↪ α
g : G
hgx : HSMul.hSMul (β := α) g ((x : (a : Fin n.succ) → α) (Fin.last n) : α) = a
H :
  ∀ (i : Fin n),
    Membership.mem (α := α) (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a)
      ((Fin.Embedding.init (g • x) : (a : Fin n) → α) i : α)
⊢ Eq (α := α) ((g • x : (a : Fin n.succ) → α) (Fin.last n) : α)
    ((ofStabilizer.snoc (codRestrict (↑(ofStabilizer G a) : Set α) (Fin.Embedding.init (g • x)) H) :
          (a : Fin n.succ) → α)
        (Fin.last n) :
      α)

Tactic:
simpa only [smul_apply, ofStabilizer.snoc, Fin.Embedding.snoc_last]

Premises used: Function.Embedding.smul_apply, Fin.Embedding.snoc_last, SubMulAction.ofStabilizer.snoc
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
s : Set α
g : ↥(stabilizer G s)
x : (↑s : Type u_2)
⊢ g • (↑x : α) ∈ g • s

Tactic:
Set.smul_mem_smul_set x.prop

Premises used: Subtype.prop, Set.smul_mem_smul_set
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
s : Set α
g : ↥(stabilizer G s)
x : (↑s : Type u_2)
h : s = g • s
⊢ g • (↑x : α) ∈ s

Tactic:
convert! Set.smul_mem_smul_set x.prop

Premises used: Subtype.prop, Set.smul_mem_smul_set
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
s : Set α
g : ↥(stabilizer G s)
x : (↑s : Type u_2)
⊢ s = g • s

Tactic:
(mem_stabilizer_iff.mp g.prop).symm

Premises used: Subtype.prop, Iff.mp, MulAction.mem_stabilizer_iff, Eq.symm
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
s : Set α
g : ↥(stabilizer G s)
x : (↑s : Type u_2)
⊢ s = g • s

Tactic:
exact (mem_stabilizer_iff.mp g.prop).symm

Premises used: Subtype.prop, Iff.mp, MulAction.mem_stabilizer_iff, Eq.symm
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
s : Set α
g : ↥(stabilizer G s)
x : (↑s : Type u_2)
⊢ (↑(g • x) : α) = (↑g : G) • (↑x : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
s : Set α
g k : ↥(stabilizer G s)
x : (↑s : Type u_2)
⊢ (g * k) • x = g • k • x

Tactic:
simp only [← Subtype.coe_inj, SMul.smul_stabilizer_def, Subgroup.coe_mul, mul_smul]

Premises used: Subtype.coe_inj, Subgroup.coe_mul, SMul.smul_stabilizer_def, SemigroupAction.mul_smul
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
s : Set α
x : (↑s : Type u_2)
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := ↥(stabilizer G s)) 1 x = x

Tactic:
simp only [← Subtype.coe_inj, SMul.smul_stabilizer_def, OneMemClass.coe_one, one_smul]

Premises used: OneMemClass.coe_one, Subtype.coe_inj, one_smul, SMul.smul_stabilizer_def
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
⊢ Eq (α := Subgroup G) (stabilizer.{u_1, u_2} G (α := Set α) ∅) ⊤

Tactic:
aesop
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
⊢ Eq (α := Subgroup G) (stabilizer.{u_1, u_2} G (α := Set α) univ) ⊤

Tactic:
aesop
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
s_1 s : Set α
g : G
h : Membership.mem (γ := Subgroup G) (stabilizer G s) g
⊢ Membership.mem (γ := Subgroup G) (stabilizer G sᶜ) g

Tactic:
simp [Set.smul_set_compl, mem_stabilizer_iff.1 h]

Premises used: Set.smul_set_compl, Iff.mp, MulAction.mem_stabilizer_iff
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
s : Set α
⊢ ∀ (s : Set α), LE.le (α := Subgroup G) (stabilizer G s) (stabilizer G sᶜ)

Tactic:
have (s : Set α) : stabilizer G s ≤ stabilizer G (sᶜ) := by
    intro g h
    simp [Set.smul_set_compl, mem_stabilizer_iff.1 h]
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
s : Set α
this : ∀ (s : Set α), LE.le (α := Subgroup G) (stabilizer G s) (stabilizer G sᶜ)
⊢ Eq (α := Subgroup G) (stabilizer G sᶜ) (stabilizer G s)

Tactic:
le_antisymm (le_of_le_of_eq (this _) ?_) (this _)

Premises used: le_of_le_of_eq, le_antisymm
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
s : Set α
this : ∀ (s : Set α), LE.le (α := Subgroup G) (stabilizer G s) (stabilizer G sᶜ)
refine : Eq (α := Subgroup G) (stabilizer G sᶜᶜ) (stabilizer G s)
⊢ Eq (α := Subgroup G) (stabilizer G sᶜ) (stabilizer G s)

Tactic:
refine le_antisymm (le_of_le_of_eq (this _) ?_) (this _)

Premises used: le_of_le_of_eq, le_antisymm
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
s : Set α
this : ∀ (s : Set α), LE.le (α := Subgroup G) (stabilizer G s) (stabilizer G sᶜ)
rw rw₁ : Eq (α := Subgroup G) (stabilizer G s) (stabilizer G s)
⊢ Eq (α := Subgroup G) (stabilizer G sᶜᶜ) (stabilizer G s)

Tactic:
rw [compl_compl]

Premises used: compl_compl
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Pointwise
Goal:
R : Type u_1
M : Type u_2
inst : Monoid R
inst_1 : MulAction R M
inst_2 : One M
⊢ (↑1 : Set M) = Set.range fun (r : R) ↦ HSMul.hSMul (β := M) r 1

Tactic:
rfl

Premises used: setOf, Set.range, rfl
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Pointwise
Goal:
R : Type u_1
M : Type u_2
inst : Monoid R
inst_1 : MulAction R M
inst_2 : One M
x : M
⊢ Membership.mem (γ := SubMulAction R M) 1 x ↔ ∃ (r : R), HSMul.hSMul (β := M) r 1 = x

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.range
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Pointwise
Goal:
R : Type u_1
M : Type u_2
inst : Monoid R
inst_1 : MulAction R M
inst_2 : One M
⊢ 1 ⊆ (↑1 : Set M)

Tactic:
fun _ hx =>
  ⟨1, (one_smul _ _).trans hx.symm⟩

Premises used: Set.Mem, setOf, Set.Subset, one_smul, Exists.intro, Set.range, OfNat.ofNat, Eq.symm, Eq.trans
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Pointwise
Goal:
R : Type u_1
M : Type u_2
inst : Monoid R
inst_1 : MulAction R M
inst_2 : Mul M
inst_3 : IsScalarTower R M M
p q : SubMulAction R M
⊢ (↑(p * q) : Set M) = (↑p : Set M) * (↑q : Set M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Pointwise
Goal:
R : Type u_1
M : Type u_2
inst : Monoid R
inst_1 : MulAction R M
inst_2 : Mul M
inst_3 : IsScalarTower R M M
p q : SubMulAction R M
x : M
⊢ x ∈ p * q ↔ ∃ y ∈ p, ∃ z ∈ q, y * z = x

Tactic:
Set.mem_mul

Premises used: Set.Mem, Set.mem_mul
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Pointwise
Goal:
R : Type u_1
M : Type u_2
inst : Monoid R
inst_1 : MulAction R M
inst_2 : MulOneClass M
inst_3 : IsScalarTower R M M
inst_4 : SMulCommClass R M M
a : SubMulAction R M
h : ∀ (x : M), x ∈ 1 * a ↔ x ∈ a
⊢ 1 * a = a

Tactic:
ext x
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Pointwise
Goal:
R : Type u_1
M : Type u_2
inst : Monoid R
inst_1 : MulAction R M
inst_2 : MulOneClass M
inst_3 : IsScalarTower R M M
inst_4 : SMulCommClass R M M
a : SubMulAction R M
x : M
h : (∃ (a_1 : R), ∃ z ∈ a, a_1 • z = x) ↔ x ∈ a
⊢ x ∈ 1 * a ↔ x ∈ a

Tactic:
simp only [mem_mul, mem_one, smul_mul_assoc, exists_exists_eq_and, one_mul]

Premises used: SubMulAction.mem_mul, smul_mul_assoc, SubMulAction.mem_one, exists_exists_eq_and, one_mul
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Pointwise
Goal:
R : Type u_1
M : Type u_2
inst : Monoid R
inst_1 : MulAction R M
inst_2 : MulOneClass M
inst_3 : IsScalarTower R M M
inst_4 : SMulCommClass R M M
a : SubMulAction R M
x : M
⊢ (∃ (a_1 : R), ∃ z ∈ a, a_1 • z = x) ↔ x ∈ a

Tactic:
⟨?_, fun hx => ⟨1, x, hx, one_smul _ _⟩⟩

Premises used: one_smul, And.intro, Iff.intro, Exists.intro, OfNat.ofNat