[GOAL]
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
x✝¹ x✝ : R
s : { x // x ∈ ⊥ }
h : ↑s * x✝¹ = ↑s * x✝
⊢ x✝¹ * ↑s = x✝ * ↑s
[PROOFSTEP]
rcases s with ⟨s, hs⟩
[GOAL]
case mk
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
x✝¹ x✝ s : R
hs : s ∈ ⊥
h : ↑{ val := s, property := hs } * x✝¹ = ↑{ val := s, property := hs } * x✝
⊢ x✝¹ * ↑{ val := s, property := hs } = x✝ * ↑{ val := s, property := hs }
[PROOFSTEP]
rw [Submonoid.mem_bot] at hs 
[GOAL]
case mk
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
x✝¹ x✝ s : R
hs✝ : s ∈ ⊥
hs : s = 1
h : ↑{ val := s, property := hs✝ } * x✝¹ = ↑{ val := s, property := hs✝ } * x✝
⊢ x✝¹ * ↑{ val := s, property := hs✝ } = x✝ * ↑{ val := s, property := hs✝ }
[PROOFSTEP]
subst hs
[GOAL]
case mk
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
x✝¹ x✝ : R
hs : 1 ∈ ⊥
h : ↑{ val := 1, property := hs } * x✝¹ = ↑{ val := 1, property := hs } * x✝
⊢ x✝¹ * ↑{ val := 1, property := hs } = x✝ * ↑{ val := 1, property := hs }
[PROOFSTEP]
rw [one_mul, one_mul] at h 
[GOAL]
case mk
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
x✝¹ x✝ : R
hs : 1 ∈ ⊥
h : x✝¹ = x✝
⊢ x✝¹ * ↑{ val := 1, property := hs } = x✝ * ↑{ val := 1, property := hs }
[PROOFSTEP]
subst h
[GOAL]
case mk
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
x✝ : R
hs : 1 ∈ ⊥
⊢ x✝ * ↑{ val := 1, property := hs } = x✝ * ↑{ val := 1, property := hs }
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
x✝ : R
s : { x // x ∈ ⊥ }
⊢ x✝ * ↑((fun x s => s) x✝ s) = ↑s * (fun r x => r) x✝ s
[PROOFSTEP]
rcases s with ⟨s, hs⟩
[GOAL]
case mk
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
x✝ s : R
hs : s ∈ ⊥
⊢ x✝ * ↑((fun x s => s) x✝ { val := s, property := hs }) =
    ↑{ val := s, property := hs } * (fun r x => r) x✝ { val := s, property := hs }
[PROOFSTEP]
rw [Submonoid.mem_bot] at hs 
[GOAL]
case mk
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
x✝ s : R
hs✝ : s ∈ ⊥
hs : s = 1
⊢ x✝ * ↑((fun x s => s) x✝ { val := s, property := hs✝ }) =
    ↑{ val := s, property := hs✝ } * (fun r x => r) x✝ { val := s, property := hs✝ }
[PROOFSTEP]
simp [hs]
[GOAL]
R✝ : Type u_1
inst✝² : Monoid R✝
S✝ : Submonoid R✝
inst✝¹ : OreSet S✝
R : Type ?u.7831
inst✝ : CommMonoid R
S : Submonoid R
m n : R
s : { x // x ∈ S }
h : ↑s * m = ↑s * n
⊢ m * ↑s = n * ↑s
[PROOFSTEP]
rw [mul_comm n s, mul_comm m s, h]
[GOAL]
R✝ : Type u_1
inst✝² : Monoid R✝
S✝ : Submonoid R✝
inst✝¹ : OreSet S✝
R : Type ?u.7831
inst✝ : CommMonoid R
S : Submonoid R
r : R
s : { x // x ∈ S }
⊢ r * ↑((fun x s => s) r s) = ↑s * (fun r x => r) r s
[PROOFSTEP]
rw [mul_comm]
