awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer (goal)
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))
⊢ Eq.{u_2 + 1} (α := α) ((fun (x : α) ↦ g • x) x) ((fun (x : α) ↦ g • x) y)
have 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)
Tactic: rwa [← SetLike.coe_eq_coe, conjMap_apply] at hxy
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer (goal)
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)
⊢ Eq.{u_2 + 1} (α := α) ((fun (x : α) ↦ g • x) x) ((fun (x : α) ↦ g • x) y)
have 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)
Tactic: rwa [← SetLike.coe_eq_coe, conjMap_apply] at hxy
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer (goal)
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)
⊢ 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) → α)
have simp : ∀ (x_1 : Fin n), ¬(↑((x : (a_1 : Fin n) → ↥(ofStabilizer G a)) x_1) : α) = a
Tactic: simp only [Set.mem_range, trans_apply, Function.Embedding.subtype_apply, not_exists]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer (goal)
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) (y : Fin n ↪ ↥(ofStabilizer G a)), g • x = ofStabilizer.snoc y
have 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
Tactic: obtain ⟨g, hgx⟩ := exists_smul_eq G (x (Fin.last n)) a
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer (goal)
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 : α)
have simp : ¬Eq (α := α) ((Fin.Embedding.init (g • x) : (a : Fin n) → α) i : α) ((g • x : (a : Fin (n + 1)) → α) (Fin.last n) : α)
Tactic: simp only [mem_ofStabilizer_iff,
      Nat.succ_eq_add_one, ← hgx, ← smul_apply, ne_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer (goal)
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 + 1)) → α) (Fin.last n) : α)
have suffices : Eq (α := α) ((Fin.Embedding.init (g • x) : (a : Fin n) → α) i : α) ((g • x : (a : Fin n.succ) → α) i.castSucc : α)
Tactic: suffices Fin.Embedding.init (g • x) i = (g • x) i.castSucc by
      simp [this]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer (hypothesis)
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
⊢ ∃ (g : G) (y : Fin n ↪ ↥(ofStabilizer G a)), g • x = ofStabilizer.snoc y
have 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 : α)
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]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer (goal)
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 : α)
⊢ ∃ (g : G) (y : Fin n ↪ ↥(ofStabilizer G a)), g • x = ofStabilizer.snoc y
have h : g • x = ofStabilizer.snoc (codRestrict (↑(ofStabilizer G a) : Set α) (Fin.Embedding.init (g • x)) H)
Tactic: use g, (Fin.Embedding.init (g • x)).codRestrict (ofStabilizer G a) H
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer (goal)
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 : α)
⊢ g • x = ofStabilizer.snoc (codRestrict (↑(ofStabilizer G a) : Set α) (Fin.Embedding.init (g • x)) H)
have 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 :
      α)
Tactic: ext i
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer (goal)
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
⊢ 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 :
      α)
have 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 :
      α)
Tactic: rcases Fin.eq_castSucc_or_eq_last i with ⟨i, rfl⟩ | ⟨rfl⟩
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer (goal)
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 :
        α)
⊢ 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 :
      α)
have 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) :
    α)
Tactic: rcases Fin.eq_castSucc_or_eq_last i with ⟨i, rfl⟩ | ⟨rfl⟩
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer (goal)
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 : α) ∈ s
have h : s = g • s
Tactic: convert! Set.smul_mem_smul_set x.prop
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer (hypothesis)
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
s : Set α
⊢ Eq (α := Subgroup G) (stabilizer G sᶜ) (stabilizer G s)
have this : ∀ (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]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer (goal)
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)
have refine : Eq (α := Subgroup G) (stabilizer G sᶜᶜ) (stabilizer G s)
Tactic: refine le_antisymm (le_of_le_of_eq (this _) ?_) (this _)
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer (goal)
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)
have rw : Eq (α := Subgroup G) (stabilizer G s) (stabilizer G s)
Tactic: rw [compl_compl]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.Pointwise (goal)
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
⊢ 1 * a = a
have h : ∀ (x : M), x ∈ 1 * a ↔ x ∈ a
Tactic: ext x
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.Pointwise (goal)
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
⊢ x ∈ 1 * a ↔ x ∈ a
have h : (∃ (a_1 : R), ∃ z ∈ a, a_1 • z = x) ↔ x ∈ a
Tactic: simp only [mem_mul, mem_one, smul_mul_assoc, exists_exists_eq_and, one_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.Pointwise (goal)
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
have h : (∃ (a_1 : R), ∃ z ∈ a, a_1 • z = x) → x ∈ a
Tactic: refine ⟨?_, fun hx => ⟨1, x, hx, one_smul _ _⟩⟩
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.Pointwise (goal)
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
⊢ a * 1 = a
have h : ∀ (x : M), x ∈ a * 1 ↔ x ∈ a
Tactic: ext x
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.Pointwise (goal)
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
⊢ x ∈ a * 1 ↔ x ∈ a
have h : (∃ y ∈ a, ∃ (a : R), a • y = x) ↔ x ∈ a
Tactic: simp only [mem_mul, mem_one, mul_smul_comm, exists_exists_eq_and, mul_one]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.Pointwise (goal)
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
⊢ (∃ y ∈ a, ∃ (a : R), a • y = x) ↔ x ∈ a
have h : (∃ y ∈ a, ∃ (a : R), a • y = x) → x ∈ a
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.Pointwise (goal)
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 : (∃ y ∈ a, ∃ (a : R), a • y = x) → x ∈ a
⊢ (∃ y ∈ a, ∃ (a : R), a • y = x) ↔ x ∈ a
have h₁ : x ∈ a → ∃ y ∈ a, ∃ (a : R), a • y = x
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.Pointwise (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Monoid R
inst_1 : MulAction R M
inst_2 : Monoid M
inst_3 : IsScalarTower R M M
inst_4 : SMulCommClass R M M
p : SubMulAction R M
h : Ne (α := ℕ) 1 0
⊢ (↑(HPow.hPow (β := ℕ) p 1) : Set M) = HPow.hPow (β := ℕ) (↑p : Set M) 1
have rw : (↑p : Set M) = HPow.hPow (β := ℕ) (↑p : Set M) 1
Tactic: rw [pow_one, pow_one]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.Pointwise (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Monoid R
inst_1 : MulAction R M
inst_2 : Monoid M
inst_3 : IsScalarTower R M M
inst_4 : SMulCommClass R M M
p : SubMulAction R M
h : Ne (α := ℕ) 1 0
rw : (↑p : Set M) = HPow.hPow (β := ℕ) (↑p : Set M) 1
⊢ (↑(HPow.hPow (β := ℕ) p 1) : Set M) = HPow.hPow (β := ℕ) (↑p : Set M) 1
have rw₁ : (↑p : Set M) = (↑p : Set M)
Tactic: rw [pow_one, pow_one]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.Pointwise (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Monoid R
inst_1 : MulAction R M
inst_2 : Monoid M
inst_3 : IsScalarTower R M M
inst_4 : SMulCommClass R M M
p : SubMulAction R M
n : ℕ
h : n + 2 ≠ 0
⊢ (↑(p ^ (n + 2)) : Set M) = (↑p : Set M) ^ (n + 2)
have rw : (↑(p ^ (n + 1) * p) : Set M) = (↑p : Set M) ^ (n + 2)
Tactic: rw [pow_succ _ (n + 1), pow_succ _ (n + 1), coe_mul, coe_pow _ n.succ_ne_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.Pointwise (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Monoid R
inst_1 : MulAction R M
inst_2 : Monoid M
inst_3 : IsScalarTower R M M
inst_4 : SMulCommClass R M M
p : SubMulAction R M
n : ℕ
h : n + 2 ≠ 0
rw : (↑(p ^ (n + 1) * p) : Set M) = (↑p : Set M) ^ (n + 2)
⊢ (↑(p ^ (n + 2)) : Set M) = (↑p : Set M) ^ (n + 2)
have rw₁ : (↑(p ^ (n + 1) * p) : Set M) = (↑p : Set M) ^ (n + 1) * (↑p : Set M)
Tactic: rw [pow_succ _ (n + 1), pow_succ _ (n + 1), coe_mul, coe_pow _ n.succ_ne_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.Pointwise (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Monoid R
inst_1 : MulAction R M
inst_2 : Monoid M
inst_3 : IsScalarTower R M M
inst_4 : SMulCommClass R M M
p : SubMulAction R M
n : ℕ
h : n + 2 ≠ 0
rw : (↑(p ^ (n + 1) * p) : Set M) = (↑p : Set M) ^ (n + 2)
rw₁ : (↑(p ^ (n + 1) * p) : Set M) = (↑p : Set M) ^ (n + 1) * (↑p : Set M)
⊢ (↑(p ^ (n + 2)) : Set M) = (↑p : Set M) ^ (n + 2)
have rw₂ : (↑(p ^ (n + 1)) : Set M) * (↑p : Set M) = (↑p : Set M) ^ (n + 1) * (↑p : Set M)
Tactic: rw [pow_succ _ (n + 1), pow_succ _ (n + 1), coe_mul, coe_pow _ n.succ_ne_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.Pointwise (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Monoid R
inst_1 : MulAction R M
inst_2 : Monoid M
inst_3 : IsScalarTower R M M
inst_4 : SMulCommClass R M M
p : SubMulAction R M
n : ℕ
h : n + 2 ≠ 0
rw : (↑(p ^ (n + 1) * p) : Set M) = (↑p : Set M) ^ (n + 2)
rw₁ : (↑(p ^ (n + 1) * p) : Set M) = (↑p : Set M) ^ (n + 1) * (↑p : Set M)
rw₂ : (↑(p ^ (n + 1)) : Set M) * (↑p : Set M) = (↑p : Set M) ^ (n + 1) * (↑p : Set M)
⊢ (↑(p ^ (n + 2)) : Set M) = (↑p : Set M) ^ (n + 2)
have rw₃ : (↑p : Set M) ^ n.succ * (↑p : Set M) = (↑p : Set M) ^ (n + 1) * (↑p : Set M)
Tactic: rw [pow_succ _ (n + 1), pow_succ _ (n + 1), coe_mul, coe_pow _ n.succ_ne_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.Pointwise (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Monoid R
inst_1 : MulAction R M
inst_2 : Monoid M
inst_3 : IsScalarTower R M M
inst_4 : SMulCommClass R M M
p : SubMulAction R M
n : ℕ
rw : (↑p : Set M) ^ n.succ ⊆ (↑(p ^ n.succ) : Set M)
⊢ (↑p : Set M) ^ (n + 1) ⊆ (↑(p ^ (n + 1)) : Set M)
have rw₁ : (↑p : Set M) ^ n.succ ⊆ (↑p : Set M) ^ n.succ
Tactic: rw [← Nat.succ_eq_add_one, coe_pow _ n.succ_ne_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction (goal)
Goal:
S : Type u_1
R : Type u_2
M : Type u_3
inst : SetLike S M
inst_1 : Monoid R
inst_2 : MulAction R M
inst_3 : SMulMemClass S R M
s : S
r : Rˣ
⊢ r • (↑s : Set M) = (↑s : Set M)
have apply : (↑s : Set M) ⊆ (↑r : R) • (↑s : Set M)
Tactic: apply subset_antisymm (smul_subset_self _ s)
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction (goal)
Goal:
S : Type u'
T : Type u''
R : Type u
M : Type v
inst : SMul R M
p q : SubMulAction R M
h : p.carrier = q.carrier
⊢ p = q
have mk : ∀ (carrier : Set M) (smul_mem' : ∀ (c : R) {x : M}, x ∈ carrier → c • x ∈ carrier)
  (h : { carrier := carrier, smul_mem' := smul_mem' : SubMulAction R M }.carrier = q.carrier),
  { carrier := carrier, smul_mem' := smul_mem' : SubMulAction R M } = q
Tactic: cases p
Cleared hypotheses: p, h
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction (goal)
Goal:
S : Type u'
T : Type u''
R : Type u
M : Type v
inst : SMul R M
q : SubMulAction R M
carrier : Set M
smul_mem' : ∀ (c : R) {x : M}, x ∈ carrier → c • x ∈ carrier
h : { carrier := carrier, smul_mem' := smul_mem' : SubMulAction R M }.carrier = q.carrier
⊢ { carrier := carrier, smul_mem' := smul_mem' : SubMulAction R M } = q
have mk : ∀ (carrier_1 : Set M) (smul_mem'_1 : ∀ (c : R) {x : M}, x ∈ carrier_1 → c • x ∈ carrier_1)
  (h :
    { carrier := carrier, smul_mem' := smul_mem' : SubMulAction R M }.carrier =
      { carrier := carrier_1, smul_mem' := smul_mem'_1 : SubMulAction R M }.carrier),
  { carrier := carrier, smul_mem' := smul_mem' : SubMulAction R M } = { carrier := carrier_1, smul_mem' := smul_mem'_1 }
Tactic: cases q
Cleared hypotheses: q, h
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction (goal)
Goal:
S : Type u'
R : Type u
M : Type v
inst : Monoid R
inst_1 : MulAction R M
inst_2 : SMul S R
inst_3 : SMul S M
inst_4 : IsScalarTower S R M
p : SubMulAction R M
s : S
x : M
h : x ∈ p
⊢ s • x ∈ p
have rw : HSMul.hSMul (β := R) s 1 • x ∈ p
Tactic: rw [← one_smul R x, ← smul_assoc]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction (goal)
Goal:
R : Type u
M : Type v
inst : Monoid R
inst_1 : MulAction R M
p : SubMulAction R M
m : ↥p
⊢ Subtype.val (p := fun (x : M) ↦ x ∈ p) ⁻¹' MulAction.orbit R (↑m : M) = MulAction.orbit R m
have rw : Subtype.val (p := fun (x : M) ↦ x ∈ p) ⁻¹' Subtype.val (p := fun (x : M) ↦ x ∈ p) '' MulAction.orbit R m =
  MulAction.orbit R m
Tactic: rw [← val_image_orbit, Subtype.val_injective.preimage_image]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction (goal)
Goal:
R : Type u
M : Type v
inst : Monoid R
inst_1 : MulAction R M
p : SubMulAction R M
m : ↥p
rw :
  Subtype.val (p := fun (x : M) ↦ x ∈ p) ⁻¹' Subtype.val (p := fun (x : M) ↦ x ∈ p) '' MulAction.orbit R m =
    MulAction.orbit R m
⊢ Subtype.val (p := fun (x : M) ↦ x ∈ p) ⁻¹' MulAction.orbit R (↑m : M) = MulAction.orbit R m
have rw₁ : MulAction.orbit R m = MulAction.orbit R m
Tactic: rw [← val_image_orbit, Subtype.val_injective.preimage_image]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction (goal)
Goal:
R : Type u
M : Type v
inst : Monoid R
inst_1 : MulAction R M
p : SubMulAction R M
x m : ↥p
⊢ x ∈ MulAction.orbit R m ↔ (↑x : M) ∈ MulAction.orbit R (↑m : M)
have rw : Membership.mem (γ := Set ↥p) (Subtype.val (p := fun (x : M) ↦ x ∈ p) ⁻¹' MulAction.orbit R (↑m : M)) x ↔
  (↑x : M) ∈ MulAction.orbit R (↑m : M)
Tactic: rw [← val_preimage_orbit, Set.mem_preimage]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction (goal)
Goal:
R : Type u
M : Type v
inst : Monoid R
inst_1 : MulAction R M
p : SubMulAction R M
x m : ↥p
rw :
  Membership.mem (γ := Set ↥p) (Subtype.val (p := fun (x : M) ↦ x ∈ p) ⁻¹' MulAction.orbit R (↑m : M)) x ↔
    (↑x : M) ∈ MulAction.orbit R (↑m : M)
⊢ x ∈ MulAction.orbit R m ↔ (↑x : M) ∈ MulAction.orbit R (↑m : M)
have rw₁ : (↑x : M) ∈ MulAction.orbit R (↑m : M) ↔ (↑x : M) ∈ MulAction.orbit R (↑m : M)
Tactic: rw [← val_preimage_orbit, Set.mem_preimage]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction (goal)
Goal:
R : Type u
M : Type v
inst : Monoid R
inst_1 : MulAction R M
p : SubMulAction R M
m : ↥p
⊢ Eq (α := Submonoid R) (MulAction.stabilizerSubmonoid R m) (MulAction.stabilizerSubmonoid R (↑m : M))
have h : ∀ (x : R),
  Membership.mem (γ := Submonoid R) (MulAction.stabilizerSubmonoid R m) x ↔
    Membership.mem (γ := Submonoid R) (MulAction.stabilizerSubmonoid R (↑m : M)) x
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction (goal)
Goal:
R : Type u
M : Type v
inst : Group R
inst_1 : MulAction R M
p : SubMulAction R M
⊢ Eq (α := Setoid ↥p) (MulAction.orbitRel R ↥p)
    (Setoid.comap (Subtype.val (p := fun (x : M) ↦ x ∈ p)) (MulAction.orbitRel R M))
have refine : ∀ (x y : ↥p),
  (MulAction.orbitRel R ↥p : ↥p → ↥p → Prop) x y ↔
    (Setoid.comap Subtype.val (MulAction.orbitRel R M) : ↥p → ↥p → Prop) x y
Tactic: refine Setoid.ext_iff.2 (fun x y ↦ ?_)