[GOAL]
R : Type u_1
M : Type u_2
inst✝⁴ : Monoid R
inst✝³ : MulAction R M
inst✝² : MulOneClass M
inst✝¹ : IsScalarTower R M M
inst✝ : SMulCommClass R M M
a : SubMulAction R M
⊢ 1 * a = a
[PROOFSTEP]
ext x
[GOAL]
case h
R : Type u_1
M : Type u_2
inst✝⁴ : Monoid R
inst✝³ : MulAction R M
inst✝² : MulOneClass M
inst✝¹ : IsScalarTower R M M
inst✝ : SMulCommClass R M M
a : SubMulAction R M
x : M
⊢ x ∈ 1 * a ↔ x ∈ a
[PROOFSTEP]
simp only [mem_mul, mem_one, smul_mul_assoc, exists_and_left, exists_exists_eq_and, one_mul]
[GOAL]
case h
R : Type u_1
M : Type u_2
inst✝⁴ : Monoid R
inst✝³ : MulAction R M
inst✝² : MulOneClass M
inst✝¹ : IsScalarTower R M M
inst✝ : SMulCommClass R M M
a : SubMulAction R M
x : M
⊢ (∃ a_1 x_1, x_1 ∈ a ∧ a_1 • x_1 = x) ↔ x ∈ a
[PROOFSTEP]
refine' ⟨_, fun hx => ⟨1, x, hx, one_smul _ _⟩⟩
[GOAL]
case h
R : Type u_1
M : Type u_2
inst✝⁴ : Monoid R
inst✝³ : MulAction R M
inst✝² : MulOneClass M
inst✝¹ : IsScalarTower R M M
inst✝ : SMulCommClass R M M
a : SubMulAction R M
x : M
⊢ (∃ a_1 x_1, x_1 ∈ a ∧ a_1 • x_1 = x) → x ∈ a
[PROOFSTEP]
rintro ⟨r, y, hy, rfl⟩
[GOAL]
case h.intro.intro.intro
R : Type u_1
M : Type u_2
inst✝⁴ : Monoid R
inst✝³ : MulAction R M
inst✝² : MulOneClass M
inst✝¹ : IsScalarTower R M M
inst✝ : SMulCommClass R M M
a : SubMulAction R M
r : R
y : M
hy : y ∈ a
⊢ r • y ∈ a
[PROOFSTEP]
exact smul_mem _ _ hy
[GOAL]
R : Type u_1
M : Type u_2
inst✝⁴ : Monoid R
inst✝³ : MulAction R M
inst✝² : MulOneClass M
inst✝¹ : IsScalarTower R M M
inst✝ : SMulCommClass R M M
a : SubMulAction R M
⊢ a * 1 = a
[PROOFSTEP]
ext x
[GOAL]
case h
R : Type u_1
M : Type u_2
inst✝⁴ : Monoid R
inst✝³ : MulAction R M
inst✝² : MulOneClass M
inst✝¹ : IsScalarTower R M M
inst✝ : SMulCommClass R M M
a : SubMulAction R M
x : M
⊢ x ∈ a * 1 ↔ x ∈ a
[PROOFSTEP]
simp only [mem_mul, mem_one, mul_smul_comm, exists_and_left, exists_exists_eq_and, mul_one]
[GOAL]
case h
R : Type u_1
M : Type u_2
inst✝⁴ : Monoid R
inst✝³ : MulAction R M
inst✝² : MulOneClass M
inst✝¹ : IsScalarTower R M M
inst✝ : SMulCommClass R M M
a : SubMulAction R M
x : M
⊢ (∃ y, y ∈ a ∧ ∃ a, a • y = x) ↔ x ∈ a
[PROOFSTEP]
constructor
[GOAL]
case h.mp
R : Type u_1
M : Type u_2
inst✝⁴ : Monoid R
inst✝³ : MulAction R M
inst✝² : MulOneClass M
inst✝¹ : IsScalarTower R M M
inst✝ : SMulCommClass R M M
a : SubMulAction R M
x : M
⊢ (∃ y, y ∈ a ∧ ∃ a, a • y = x) → x ∈ a
[PROOFSTEP]
rintro ⟨y, hy, r, rfl⟩
[GOAL]
case h.mp.intro.intro.intro
R : Type u_1
M : Type u_2
inst✝⁴ : Monoid R
inst✝³ : MulAction R M
inst✝² : MulOneClass M
inst✝¹ : IsScalarTower R M M
inst✝ : SMulCommClass R M M
a : SubMulAction R M
y : M
hy : y ∈ a
r : R
⊢ r • y ∈ a
[PROOFSTEP]
exact smul_mem _ _ hy
[GOAL]
case h.mpr
R : Type u_1
M : Type u_2
inst✝⁴ : Monoid R
inst✝³ : MulAction R M
inst✝² : MulOneClass M
inst✝¹ : IsScalarTower R M M
inst✝ : SMulCommClass R M M
a : SubMulAction R M
x : M
⊢ x ∈ a → ∃ y, y ∈ a ∧ ∃ a, a • y = x
[PROOFSTEP]
intro hx
[GOAL]
case h.mpr
R : Type u_1
M : Type u_2
inst✝⁴ : Monoid R
inst✝³ : MulAction R M
inst✝² : MulOneClass M
inst✝¹ : IsScalarTower R M M
inst✝ : SMulCommClass R M M
a : SubMulAction R M
x : M
hx : x ∈ a
⊢ ∃ y, y ∈ a ∧ ∃ a, a • y = x
[PROOFSTEP]
exact ⟨x, hx, 1, one_smul _ _⟩
[GOAL]
R : Type u_1
M : Type u_2
inst✝⁴ : Monoid R
inst✝³ : MulAction R M
inst✝² : Monoid M
inst✝¹ : IsScalarTower R M M
inst✝ : SMulCommClass R M M
p : SubMulAction R M
x✝ : 1 ≠ 0
⊢ ↑(p ^ 1) = ↑p ^ 1
[PROOFSTEP]
rw [pow_one, pow_one]
[GOAL]
R : Type u_1
M : Type u_2
inst✝⁴ : Monoid R
inst✝³ : MulAction R M
inst✝² : Monoid M
inst✝¹ : IsScalarTower R M M
inst✝ : SMulCommClass R M M
p : SubMulAction R M
n : ℕ
x✝ : n + 2 ≠ 0
⊢ ↑(p ^ (n + 2)) = ↑p ^ (n + 2)
[PROOFSTEP]
rw [pow_succ _ (n + 1), pow_succ _ (n + 1), coe_mul, coe_pow _ n.succ_ne_zero]
[GOAL]
R : Type u_1
M : Type u_2
inst✝⁴ : Monoid R
inst✝³ : MulAction R M
inst✝² : Monoid M
inst✝¹ : IsScalarTower R M M
inst✝ : SMulCommClass R M M
p : SubMulAction R M
⊢ ↑p ^ 0 ⊆ ↑(p ^ 0)
[PROOFSTEP]
rw [pow_zero, pow_zero]
[GOAL]
R : Type u_1
M : Type u_2
inst✝⁴ : Monoid R
inst✝³ : MulAction R M
inst✝² : Monoid M
inst✝¹ : IsScalarTower R M M
inst✝ : SMulCommClass R M M
p : SubMulAction R M
⊢ 1 ⊆ ↑1
[PROOFSTEP]
exact subset_coe_one
[GOAL]
R : Type u_1
M : Type u_2
inst✝⁴ : Monoid R
inst✝³ : MulAction R M
inst✝² : Monoid M
inst✝¹ : IsScalarTower R M M
inst✝ : SMulCommClass R M M
p : SubMulAction R M
n : ℕ
⊢ ↑p ^ (n + 1) ⊆ ↑(p ^ (n + 1))
[PROOFSTEP]
rw [← Nat.succ_eq_add_one, coe_pow _ n.succ_ne_zero]
