awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ (∃ (a_1 : R), ∃ z ∈ a, a_1 • z = x) ↔ x ∈ a

Tactic:
refine ⟨?_, fun hx => ⟨1, x, hx, one_smul _ _⟩⟩
-- 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
r : R
y : M
hy : y ∈ a
⊢ r • y ∈ a

Tactic:
smul_mem _ _ hy

Premises used: SubMulAction.smul_mem
-- 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
r : R
y : M
hy : y ∈ a
⊢ r • y ∈ a

Tactic:
exact smul_mem _ _ hy

Premises used: SubMulAction.smul_mem
-- 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 ∈ a * 1 ↔ x ∈ a
⊢ a * 1 = 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 : (∃ y ∈ a, ∃ (a : R), a • y = x) ↔ x ∈ a
⊢ x ∈ a * 1 ↔ x ∈ a

Tactic:
simp only [mem_mul, mem_one, mul_smul_comm, exists_exists_eq_and, mul_one]

Premises used: SubMulAction.mem_mul, SubMulAction.mem_one, exists_exists_eq_and, mul_smul_comm, mul_one
-- 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 : (∃ y ∈ a, ∃ (a : R), a • y = x) → x ∈ a
h₁ : x ∈ a → ∃ y ∈ a, ∃ (a : R), a • y = x
⊢ (∃ y ∈ a, ∃ (a : R), a • y = x) ↔ x ∈ a

Tactic:
constructor
-- 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
y : M
hy : y ∈ a
r : R
⊢ r • y ∈ a

Tactic:
smul_mem _ _ hy

Premises used: SubMulAction.smul_mem
-- 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
y : M
hy : y ∈ a
r : R
⊢ r • y ∈ a

Tactic:
exact smul_mem _ _ hy

Premises used: SubMulAction.smul_mem
-- 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
hx : x ∈ a
⊢ ∃ y ∈ a, ∃ (a : R), a • y = x

Tactic:
⟨x, hx, 1, one_smul _ _⟩

Premises used: one_smul, And.intro, Exists.intro, OfNat.ofNat
-- 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
hx : x ∈ a
⊢ ∃ y ∈ a, ∃ (a : R), a • y = x

Tactic:
exact ⟨x, hx, 1, one_smul _ _⟩
-- 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 : 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
rw₁ rw₂ : (↑p : Set M) = (↑p : Set M)
⊢ (↑(HPow.hPow (β := ℕ) p 1) : Set M) = HPow.hPow (β := ℕ) (↑p : Set M) 1

Tactic:
rw [pow_one, pow_one]

Premises used: pow_one
-- 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 : 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)
rw₃ rw₄ : (↑p : Set M) ^ n.succ * (↑p : Set M) = (↑p : Set M) ^ (n + 1) * (↑p : Set M)
⊢ (↑(p ^ (n + 2)) : 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]

Premises used: pow_succ, SubMulAction.coe_mul, Nat.succ_ne_zero, HAdd.hAdd, OfNat.ofNat
-- 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 : Monoid M
inst_3 : IsScalarTower R M M
inst_4 : SMulCommClass R M M
p : SubMulAction R M
⊢ 1 ⊆ (↑1 : Set M)

Tactic:
subset_coe_one

Premises used: SubMulAction.subset_coe_one
-- 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 : Monoid M
inst_3 : IsScalarTower R M M
inst_4 : SMulCommClass R M M
p : SubMulAction R M
⊢ 1 ⊆ (↑1 : Set M)

Tactic:
exact subset_coe_one

Premises used: SubMulAction.subset_coe_one
-- 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 : 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)
rw₁ rw₂ : (↑p : Set M) ^ n.succ ⊆ (↑p : Set M) ^ n.succ
⊢ (↑p : Set M) ^ (n + 1) ⊆ (↑(p ^ (n + 1)) : Set M)

Tactic:
rw [← Nat.succ_eq_add_one, coe_pow _ n.succ_ne_zero]

Premises used: Nat.succ_eq_add_one, Nat.succ_ne_zero, SubMulAction.coe_pow
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction
Goal:
S : Type u_1
M : Type u_2
N : Type u_3
α : Type u_4
inst : SetLike S α
inst_1 : SMul M N
inst_2 : SMul M α
inst_3 : Monoid N
inst_4 : MulAction N α
inst_5 : SMulMemClass S N α
inst_6 : IsScalarTower M N α
⊢ SMulMemClass S M α

Tactic:
{ smul_mem := fun m a ha => smul_one_smul N m a ▸ SMulMemClass.smul_mem _ ha }

Premises used: SMulMemClass.smul_mem, Eq.rec, smul_one_smul, HSMul.hSMul, OfNat.ofNat, SMulMemClass.mk
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction
Goal:
S : Type u'
R : Type u
M : Type v
inst : SMul R M
inst_1 : SetLike S M
hS : SMulMemClass S R M
s : S
r : R
x : ↥s
⊢ (↑(r • x) : M) = r • (↑x : M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction
Goal:
S : Type u'
R : Type u
M : Type v
inst : SMul R M
inst_1 : SetLike S M
hS : SMulMemClass S R M
s : S
r : R
x : M
hx : x ∈ s
⊢ r • Subtype.mk (p := fun (x : M) ↦ x ∈ s) x hx = Subtype.mk (p := fun (x : M) ↦ x ∈ s) (r • x) ⋯

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction
Goal:
S : Type u'
R : Type u
M : Type v
inst : SMul R M
inst_1 : SetLike S M
hS : SMulMemClass S R M
s : S
r : R
x : ↥s
⊢ r • x = Subtype.mk (p := fun (x : M) ↦ x ∈ s) (r • (↑x : M)) ⋯

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction
Goal:
R : Type u_1
M : Type u_2
S : Type u_3
inst : Monoid R
inst_1 : MulAction R M
inst_2 : SetLike S M
inst_3 : SMulMemClass S R M
N : S
x : M
h : ∀ (a : R), a • x ∈ N
⊢ x ∈ N

Tactic:
simpa using h 1

Premises used: OfNat.ofNat
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction
Goal:
S : Type u_1
R : Type u_2
M : Type u_3
inst : SetLike S M
inst_1 : SMul R M
inst_2 : SMulMemClass S R M
r : R
s : S
x : M
hx : x ∈ (↑s : Set M)
⊢ (fun (x : M) ↦ r • x) x ∈ (↑s : Set M)

Tactic:
simpa using SMulMemClass.smul_mem (r : R) hx

Premises used: SMulMemClass.smul_mem
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction
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ˣ
apply : (↑s : Set M) ⊆ (↑r : R) • (↑s : Set M)
⊢ r • (↑s : Set M) = (↑s : Set M)

Tactic:
apply subset_antisymm (smul_subset_self _ s)

Premises used: subset_antisymm, SetLike.smul_subset_self
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction
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ˣ
x : M
hx : x ∈ (↑s : Set M)
⊢ (fun (x : M) ↦ (↑r : R) • x) (r⁻¹ • x) = x

Tactic:
simp [← Units.smul_def]

Premises used: Units.smul_def
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction
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ˣ
x : M
hx : x ∈ (↑s : Set M)
⊢ x ∈ (↑r : R) • (↑s : Set M)

Tactic:
exact ⟨r⁻¹ • x, SMulMemClass.smul_mem (↑r⁻¹ : R) hx, by simp [← Units.smul_def]⟩
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction
Goal:
S : Type u'
M : Type v
N : Type u_1
α : Type u_2
inst : SetLike S α
inst_1 : SMul M N
inst_2 : SMul M α
inst_3 : Monoid N
inst_4 : MulAction N α
inst_5 : SMulMemClass S N α
inst_6 : IsScalarTower M N α
s : S
r : M
x : ↥s
⊢ (↑(r • x) : α) = r • (↑x : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction
Goal:
S : Type u'
M : Type v
N : Type u_1
α : Type u_2
inst : SetLike S α
inst_1 : SMul M N
inst_2 : SMul M α
inst_3 : Monoid N
inst_4 : MulAction N α
inst_5 : SMulMemClass S N α
inst_6 : IsScalarTower M N α
s : S
r : M
x : α
hx : x ∈ s
⊢ r • Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx = Subtype.mk (p := fun (x : α) ↦ x ∈ s) (r • x) ⋯

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction
Goal:
S : Type u'
M : Type v
N : Type u_1
α : Type u_2
inst : SetLike S α
inst_1 : SMul M N
inst_2 : SMul M α
inst_3 : Monoid N
inst_4 : MulAction N α
inst_5 : SMulMemClass S N α
inst_6 : IsScalarTower M N α
s : S
r : M
x : ↥s
⊢ r • x = Subtype.mk (p := fun (x : α) ↦ x ∈ s) (r • (↑x : α)) ⋯

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction
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
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
⊢ p = q

Tactic:
cases p
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction
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
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 }
⊢ { carrier := carrier, smul_mem' := smul_mem' : SubMulAction R M } = q

Tactic:
cases q
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction
Goal:
S : Type u'
T : Type u''
R : Type u
M : Type v
inst : SMul R M
carrier : Set M
smul_mem' : ∀ (c : R) {x : M}, x ∈ carrier → c • x ∈ carrier
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:
congr
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction
Goal:
R : Type u
M : Type v
inst : SMul R M
p : SubMulAction R M
x : M
⊢ x ∈ p.carrier ↔ x ∈ (↑p : Set M)

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction
Goal:
R : Type u
M : Type v
inst : SMul R M
p q : SubMulAction R M
h : ∀ (x : M), x ∈ p ↔ x ∈ q
⊢ p = q

Tactic:
SetLike.ext h

Premises used: SetLike.ext
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction
Goal:
R : Type u
M : Type v
inst : SMul R M
p : SubMulAction R M
s : Set M
hs : s = (↑p : Set M)
⊢ (↑(p.copy s hs) : Set M) = s

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction
Goal:
R : Type u
M : Type v
inst : SMul R M
p : SubMulAction R M
s : Set M
hs : s = (↑p : Set M)
⊢ p.copy s hs = p

Tactic:
SetLike.coe_injective hs

Premises used: SetLike.coe_injective
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction
Goal:
S : Type u'
T : Type u''
R : Type u
M : Type v
inst : SMul R M
⊢ ∀ (c : R) {x : M}, Membership.mem (γ := Set M) ∅ x → Membership.mem (γ := Set M) ∅ (c • x)

Tactic:
simp
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction
Goal:
S : Type u'
T : Type u''
R : Type u
M : Type v
inst : SMul R M
⊢ ∀ (c : R) {x : M}, Membership.mem (γ := Set M) Set.univ x → Membership.mem (γ := Set M) Set.univ (c • x)

Tactic:
simp
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction
Goal:
S : Type u'
T : Type u''
R : Type u
M : Type v
inst : SMul R M
s t : SubMulAction R M
⊢ ∀ (c : R) {x : M}, x ∈ (↑s : Set M) ∪ (↑t : Set M) → c • x ∈ (↑s : Set M) ∪ (↑t : Set M)

Tactic:
aesop
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction
Goal:
S : Type u'
T : Type u''
R : Type u
M : Type v
inst : SMul R M
s t : SubMulAction R M
⊢ ∀ (c : R) {x : M}, x ∈ (↑s : Set M) ∩ (↑t : Set M) → c • x ∈ (↑s : Set M) ∩ (↑t : Set M)

Tactic:
aesop
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction
Goal:
S_1 : Type u'
T : Type u''
R : Type u
M : Type v
inst : SMul R M
S : Set (SubMulAction R M)
⊢ ∀ (c : R) {x : M},
    Membership.mem (γ := Set M) (⋃ s ∈ S, (↑s : Set M)) x → Membership.mem (γ := Set M) (⋃ s ∈ S, (↑s : Set M)) (c • x)

Tactic:
aesop
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction
Goal:
S_1 : Type u'
T : Type u''
R : Type u
M : Type v
inst : SMul R M
S : Set (SubMulAction R M)
⊢ ∀ (c : R) {x : M},
    Membership.mem (γ := Set M) (⋂ s ∈ S, (↑s : Set M)) x → Membership.mem (γ := Set M) (⋂ s ∈ S, (↑s : Set M)) (c • x)

Tactic:
aesop
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction
Goal:
R : Type u
M : Type v
inst : SMul R M
ι : Sort u_1
p : ι → SubMulAction R M
x : M
⊢ Membership.mem (γ := Set M) (⋃ s ∈ Set.range p, (↑s : Set M)) x ↔ ∃ (i : ι), x ∈ p i

Tactic:
simp
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction
Goal:
R : Type u
M : Type v
inst : SMul R M
ι : Sort u_1
p : ι → SubMulAction R M
x : M
⊢ Membership.mem (γ := Set M) (⋂ s ∈ Set.range p, (↑s : Set M)) x ↔ ∀ (i : ι), x ∈ p i

Tactic:
simp
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction
Goal:
R : Type u
M : Type v
inst : SMul R M
p : SubMulAction R M
x : M
r : R
h : x ∈ p
⊢ r • x ∈ p

Tactic:
p.smul_mem' r h

Premises used: Set.Mem, SubMulAction.smul_mem'
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction
Goal:
R : Type u
M : Type v
inst : SMul R M
p : SubMulAction R M
r : R
x : ↥p
⊢ (↑(r • x) : M) = r • (↑x : M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction
Goal:
S : Type u'
T : Type u''
R : Type u
M : Type v
inst : SMul R M
p : SubMulAction R M
r : R
x : M
⊢ ∀ (m : R) (x : ↥p), (↑(m • x) : M) = id m • (↑x : M)

Tactic:
simp
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction
Goal:
R : Type u
M : Type v
inst : SMul R M
p : SubMulAction R M
x : ↥p
⊢ (p.subtype : (a : ↥p) → M) x = (↑x : M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction
Goal:
R : Type u
M : Type v
inst : SMul R M
p : SubMulAction R M
⊢ Injective (α := ↥p) (β := M) (⇑p.subtype : (a : ↥p) → M)

Tactic:
Subtype.coe_injective

Premises used: Subtype.coe_injective
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction
Goal:
R : Type u
M : Type v
inst : SMul R M
p : SubMulAction R M
⊢ Eq (α := (a : ↥p) → M) (⇑p.subtype : (a : ↥p) → M) (Subtype.val (p := fun (x : M) ↦ x ∈ p))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction
Goal:
R : Type u
M : Type v
inst : Monoid R
inst_1 : MulAction R M
A : Type u_1
inst_2 : SetLike A M
hA : SMulMemClass A R M
S' : A
x : ↥S'
⊢ (SMulMemClass.subtype S' : (a : ↥S') → M) x = (↑x : M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction
Goal:
R : Type u
M : Type v
inst : Monoid R
inst_1 : MulAction R M
A : Type u_1
inst_2 : SetLike A M
hA : SMulMemClass A R M
S' : A
⊢ Injective (α := ↥S') (β := M) (⇑(SMulMemClass.subtype S') : (a : ↥S') → M)

Tactic:
Subtype.coe_injective

Premises used: Subtype.coe_injective
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction
Goal:
R : Type u
M : Type v
inst : Monoid R
inst_1 : MulAction R M
A : Type u_1
inst_2 : SetLike A M
hA : SMulMemClass A R M
S' : A
⊢ Eq (α := (a : ↥S') → M) (⇑(SMulMemClass.subtype S') : (a : ↥S') → M) (Subtype.val (p := fun (x : M) ↦ x ∈ S'))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction
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
rw : HSMul.hSMul (β := R) s 1 • x ∈ p
⊢ s • x ∈ p

Tactic:
rw [← one_smul R x, ← smul_assoc]

Premises used: smul_assoc, one_smul
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction
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
⊢ HSMul.hSMul (β := R) s 1 • x ∈ p

Tactic:
p.smul_mem _ h

Premises used: SubMulAction.smul_mem
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction
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
⊢ HSMul.hSMul (β := R) s 1 • x ∈ p

Tactic:
exact p.smul_mem _ h

Premises used: SubMulAction.smul_mem
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction
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 : ↥p
⊢ (↑(s • x) : M) = s • (↑x : M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction
Goal:
R : Type u
M : Type v
inst : Monoid R
inst_1 : MulAction R M
p : SubMulAction R M
G : Type u_1
inst_2 : Group G
inst_3 : SMul G R
inst_4 : MulAction G M
inst_5 : IsScalarTower G R M
g : G
x : M
⊢ g • x ∈ p ↔ x ∈ p

Tactic:
⟨fun h => inv_smul_smul g x ▸ p.smul_of_tower_mem g⁻¹ h, p.smul_of_tower_mem g⟩

Premises used: SubMulAction.smul_of_tower_mem, Eq.rec, inv_smul_smul, Inv.inv, Iff.intro
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction
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 = MulAction.orbit R (↑m : M)

Tactic:
(Set.range_comp _ _).symm

Premises used: Set.range_comp, MulAction.orbit, Eq.symm
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction
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
rw₁ rw₂ : 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

Tactic:
rw [← val_image_orbit, Subtype.val_injective.preimage_image]

Premises used: Subtype.val_injective, SubMulAction.val_image_orbit, Function.Injective.preimage_image
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction
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)
rw₁ rw₂ : (↑x : M) ∈ MulAction.orbit R (↑m : M) ↔ (↑x : M) ∈ MulAction.orbit R (↑m : M)
⊢ x ∈ MulAction.orbit R m ↔ (↑x : M) ∈ MulAction.orbit R (↑m : M)

Tactic:
rw [← val_preimage_orbit, Set.mem_preimage]

Premises used: SubMulAction.val_preimage_orbit, Set.mem_preimage
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction
Goal:
R : Type u
M : Type v
inst : Monoid R
inst_1 : MulAction R M
p : SubMulAction R M
m : ↥p
h :
  ∀ (x : R),
    Membership.mem (γ := Submonoid R) (MulAction.stabilizerSubmonoid R m) x ↔
      Membership.mem (γ := Submonoid R) (MulAction.stabilizerSubmonoid R (↑m : M)) x
⊢ Eq (α := Submonoid R) (MulAction.stabilizerSubmonoid R m) (MulAction.stabilizerSubmonoid R (↑m : M))

Tactic:
ext
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction
Goal:
R : Type u
M : Type v
inst : Monoid R
inst_1 : MulAction R M
p : SubMulAction R M
m : ↥p
x : R
⊢ Membership.mem (γ := Submonoid R) (MulAction.stabilizerSubmonoid R m) x ↔
    Membership.mem (γ := Submonoid R) (MulAction.stabilizerSubmonoid R (↑m : M)) x

Tactic:
simp only [MulAction.mem_stabilizerSubmonoid_iff, ← SubMulAction.val_smul, SetLike.coe_eq_coe]

Premises used: SetLike.coe_eq_coe, MulAction.mem_stabilizerSubmonoid_iff, SubMulAction.val_smul
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction
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))

Tactic:
Setoid.ext_iff.2 (fun x y ↦ ?_)

Premises used: Iff.mpr, Setoid.ext_iff
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction
Goal:
R : Type u
M : Type v
inst : Group R
inst_1 : MulAction R M
p : SubMulAction R M
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
⊢ Eq (α := Setoid ↥p) (MulAction.orbitRel R ↥p)
    (Setoid.comap (Subtype.val (p := fun (x : M) ↦ x ∈ p)) (MulAction.orbitRel R M))

Tactic:
refine Setoid.ext_iff.2 (fun x y ↦ ?_)

Premises used: Iff.mpr, Setoid.ext_iff
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction
Goal:
R : Type u
M : Type v
inst : Group R
inst_1 : MulAction R M
p : SubMulAction R M
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:
mem_orbit_subMul_iff

Premises used: Set.Mem, SubMulAction.mem_orbit_subMul_iff
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction
Goal:
R : Type u
M : Type v
inst : Group R
inst_1 : MulAction R M
p : SubMulAction R M
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:
exact mem_orbit_subMul_iff

Premises used: SubMulAction.mem_orbit_subMul_iff
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction
Goal:
R : Type u
M : Type v
inst : Group R
inst_1 : MulAction R M
p : SubMulAction R M
m : ↥p
rw :
  Eq (α := Submonoid R) (Subgroup.toSubmonoid (MulAction.stabilizer R m))
    (Subgroup.toSubmonoid (MulAction.stabilizer R (↑m : M)))
⊢ Eq (α := Subgroup R) (MulAction.stabilizer R m) (MulAction.stabilizer R (↑m : M))

Tactic:
rw [← Subgroup.toSubmonoid_inj]

Premises used: Subgroup.toSubmonoid_inj
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction
Goal:
R : Type u
M : Type v
inst : Group R
inst_1 : MulAction R M
p : SubMulAction R M
m : ↥p
⊢ Eq (α := Submonoid R) (Subgroup.toSubmonoid (MulAction.stabilizer R m))
    (Subgroup.toSubmonoid (MulAction.stabilizer R (↑m : M)))

Tactic:
stabilizer_of_subMul.submonoid m

Premises used: SubMulAction.stabilizer_of_subMul.submonoid, MulAction.stabilizerSubmonoid