no goals
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x✝ : M × { x // x ∈ S }
m : M
s : { x // x ∈ S }
⊢ 1 • (m, s).snd • (m, s).fst = 1 • (m, s).snd • (m, s).fst
rw [one_smul]
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x✝⁴ x✝³ x✝² : M × { x // x ∈ S }
m1 : M
s1 : { x // x ∈ S }
m2 : M
s2 : { x // x ∈ S }
x✝¹ : r S M (m1, s1) (m2, s2)
m3 : M
s3 : { x // x ∈ S }
x✝ : r S M (m2, s2) (m3, s3)
u1 : { x // x ∈ S }
hu1 : u1 • (m2, s2).snd • (m1, s1).fst = u1 • (m1, s1).snd • (m2, s2).fst
u2 : { x // x ∈ S }
hu2 : u2 • (m3, s3).snd • (m2, s2).fst = u2 • (m2, s2).snd • (m3, s3).fst
⊢ (u1 * u2 * s2) • (m3, s3).snd • (m1, s1).fst = (u1 * u2 * s2) • (m1, s1).snd • (m3, s3).fst
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x✝⁴ x✝³ x✝² : M × { x // x ∈ S }
m1 : M
s1 : { x // x ∈ S }
m2 : M
s2 : { x // x ∈ S }
x✝¹ : r S M (m1, s1) (m2, s2)
m3 : M
s3 : { x // x ∈ S }
x✝ : r S M (m2, s2) (m3, s3)
u1 : { x // x ∈ S }
hu1 : u1 • (m2, s2).snd • (m1, s1).fst = u1 • (m1, s1).snd • (m2, s2).fst
u2 : { x // x ∈ S }
hu2 : u2 • (m3, s3).snd • (m2, s2).fst = u2 • (m2, s2).snd • (m3, s3).fst
⊢ r S M (m1, s1) (m3, s3)
use u1 * u2 * s2
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x✝⁴ x✝³ x✝² : M × { x // x ∈ S }
m1 : M
s1 : { x // x ∈ S }
m2 : M
s2 : { x // x ∈ S }
x✝¹ : r S M (m1, s1) (m2, s2)
m3 : M
s3 : { x // x ∈ S }
x✝ : r S M (m2, s2) (m3, s3)
u1 : { x // x ∈ S }
hu1 : u1 • (m2, s2).snd • (m1, s1).fst = u1 • (m1, s1).snd • (m2, s2).fst
u2 : { x // x ∈ S }
hu2 : u2 • (m3, s3).snd • (m2, s2).fst = u2 • (m2, s2).snd • (m3, s3).fst
hu1' : (s1 * (s3 * (u1 * u2))) • m2 = (s2 * (s3 * (u1 * u2))) • m1
hu2' : (s1 * (s2 * (u1 * u2))) • m3 = (s1 * (s3 * (u1 * u2))) • m2
⊢ (s2 * (s3 * (u1 * u2))) • m1 = (s1 * (s2 * (u1 * u2))) • m3
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x✝⁴ x✝³ x✝² : M × { x // x ∈ S }
m1 : M
s1 : { x // x ∈ S }
m2 : M
s2 : { x // x ∈ S }
x✝¹ : r S M (m1, s1) (m2, s2)
m3 : M
s3 : { x // x ∈ S }
x✝ : r S M (m2, s2) (m3, s3)
u1 : { x // x ∈ S }
hu1 : u1 • (m2, s2).snd • (m1, s1).fst = u1 • (m1, s1).snd • (m2, s2).fst
u2 : { x // x ∈ S }
hu2 : u2 • (m3, s3).snd • (m2, s2).fst = u2 • (m2, s2).snd • (m3, s3).fst
hu1' :
  (fun x x_1 => x • x_1) (u2 * s3) (u1 • (m1, s1).snd • (m2, s2).fst) =
    (fun x x_1 => x • x_1) (u2 * s3) (u1 • (m2, s2).snd • (m1, s1).fst)
hu2' :
  (fun x x_1 => x • x_1) (u1 * s1) (u2 • (m2, s2).snd • (m3, s3).fst) =
    (fun x x_1 => x • x_1) (u1 * s1) (u2 • (m3, s3).snd • (m2, s2).fst)
⊢ (u1 * u2 * s2) • (m3, s3).snd • (m1, s1).fst = (u1 * u2 * s2) • (m1, s1).snd • (m3, s3).fst
simp only [← mul_smul, smul_assoc, mul_assoc, mul_comm, mul_left_comm] at hu1' hu2'⊢
no goals
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x✝⁴ x✝³ x✝² : M × { x // x ∈ S }
m1 : M
s1 : { x // x ∈ S }
m2 : M
s2 : { x // x ∈ S }
x✝¹ : r S M (m1, s1) (m2, s2)
m3 : M
s3 : { x // x ∈ S }
x✝ : r S M (m2, s2) (m3, s3)
u1 : { x // x ∈ S }
hu1 : u1 • (m2, s2).snd • (m1, s1).fst = u1 • (m1, s1).snd • (m2, s2).fst
u2 : { x // x ∈ S }
hu2 : u2 • (m3, s3).snd • (m2, s2).fst = u2 • (m2, s2).snd • (m3, s3).fst
hu1' : (s1 * (s3 * (u1 * u2))) • m2 = (s2 * (s3 * (u1 * u2))) • m1
hu2' : (s1 * (s2 * (u1 * u2))) • m3 = (s1 * (s3 * (u1 * u2))) • m2
⊢ (s2 * (s3 * (u1 * u2))) • m1 = (s1 * (s2 * (u1 * u2))) • m3
rw [hu2', hu1']