R : Type u_1
inst✝¹⁰ : CommSemiring R
M : Type u_2
N : Type u_3
P : Type ?u.1367541
Q : Type ?u.1367544
S : Type ?u.1367547
inst✝⁹ : AddCommGroup M
inst✝⁸ : AddCommGroup N
inst✝⁷ : AddCommGroup P
inst✝⁶ : AddCommGroup Q
inst✝⁵ : AddCommGroup S
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R P
inst✝¹ : Module R Q
inst✝ : Module R S
x : M ⊗[R] N
⊢ -0 = 0
R : Type u_1
inst✝¹⁰ : CommSemiring R
M : Type u_2
N : Type u_3
P : Type ?u.1367541
Q : Type ?u.1367544
S : Type ?u.1367547
inst✝⁹ : AddCommGroup M
inst✝⁸ : AddCommGroup N
inst✝⁷ : AddCommGroup P
inst✝⁶ : AddCommGroup Q
inst✝⁵ : AddCommGroup S
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R P
inst✝¹ : Module R Q
inst✝ : Module R S
x : M ⊗[R] N
⊢ -0 + 0 = 0
rw [add_zero]
no goals
R : Type u_1
inst✝¹⁰ : CommSemiring R
M : Type u_2
N : Type u_3
P : Type ?u.1367541
Q : Type ?u.1367544
S : Type ?u.1367547
inst✝⁹ : AddCommGroup M
inst✝⁸ : AddCommGroup N
inst✝⁷ : AddCommGroup P
inst✝⁶ : AddCommGroup Q
inst✝⁵ : AddCommGroup S
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R P
inst✝¹ : Module R Q
inst✝ : Module R S
x : M ⊗[R] N
⊢ -0 = 0
apply (Neg.aux R).map_zero
case h.e'_3
R : Type u_1
inst✝¹⁰ : CommSemiring R
M : Type u_2
N : Type u_3
P : Type ?u.1367541
Q : Type ?u.1367544
S : Type ?u.1367547
inst✝⁹ : AddCommGroup M
inst✝⁸ : AddCommGroup N
inst✝⁷ : AddCommGroup P
inst✝⁶ : AddCommGroup Q
inst✝⁵ : AddCommGroup S
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R P
inst✝¹ : Module R Q
inst✝ : Module R S
x✝ : M ⊗[R] N
x : M
y : N
⊢ 0 = (-x + x) ⊗ₜ[R] y
R : Type u_1
inst✝¹⁰ : CommSemiring R
M : Type u_2
N : Type u_3
P : Type ?u.1367541
Q : Type ?u.1367544
S : Type ?u.1367547
inst✝⁹ : AddCommGroup M
inst✝⁸ : AddCommGroup N
inst✝⁷ : AddCommGroup P
inst✝⁶ : AddCommGroup Q
inst✝⁵ : AddCommGroup S
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R P
inst✝¹ : Module R Q
inst✝ : Module R S
x✝ : M ⊗[R] N
x : M
y : N
⊢ -x ⊗ₜ[R] y + x ⊗ₜ[R] y = 0
convert (add_tmul (R := R) (-x) x y).symm
no goals
case h.e'_3
R : Type u_1
inst✝¹⁰ : CommSemiring R
M : Type u_2
N : Type u_3
P : Type ?u.1367541
Q : Type ?u.1367544
S : Type ?u.1367547
inst✝⁹ : AddCommGroup M
inst✝⁸ : AddCommGroup N
inst✝⁷ : AddCommGroup P
inst✝⁶ : AddCommGroup Q
inst✝⁵ : AddCommGroup S
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R P
inst✝¹ : Module R Q
inst✝ : Module R S
x✝ : M ⊗[R] N
x : M
y : N
⊢ 0 = (-x + x) ⊗ₜ[R] y
rw [add_left_neg, zero_tmul]
R : Type u_1
inst✝¹⁰ : CommSemiring R
M : Type u_2
N : Type u_3
P : Type ?u.1367541
Q : Type ?u.1367544
S : Type ?u.1367547
inst✝⁹ : AddCommGroup M
inst✝⁸ : AddCommGroup N
inst✝⁷ : AddCommGroup P
inst✝⁶ : AddCommGroup Q
inst✝⁵ : AddCommGroup S
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R P
inst✝¹ : Module R Q
inst✝ : Module R S
x✝ x y : M ⊗[R] N
hx : -x + x = 0
hy : -y + y = 0
this : -x + x + (-y + y) = 0
⊢ -(x + y) + (x + y) = 0

case this
R : Type u_1
inst✝¹⁰ : CommSemiring R
M : Type u_2
N : Type u_3
P : Type ?u.1367541
Q : Type ?u.1367544
S : Type ?u.1367547
inst✝⁹ : AddCommGroup M
inst✝⁸ : AddCommGroup N
inst✝⁷ : AddCommGroup P
inst✝⁶ : AddCommGroup Q
inst✝⁵ : AddCommGroup S
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R P
inst✝¹ : Module R Q
inst✝ : Module R S
x✝ x y : M ⊗[R] N
hx : -x + x = 0
hy : -y + y = 0
⊢ -x + x + (-y + y) = 0
R : Type u_1
inst✝¹⁰ : CommSemiring R
M : Type u_2
N : Type u_3
P : Type ?u.1367541
Q : Type ?u.1367544
S : Type ?u.1367547
inst✝⁹ : AddCommGroup M
inst✝⁸ : AddCommGroup N
inst✝⁷ : AddCommGroup P
inst✝⁶ : AddCommGroup Q
inst✝⁵ : AddCommGroup S
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R P
inst✝¹ : Module R Q
inst✝ : Module R S
x✝ x y : M ⊗[R] N
hx : -x + x = 0
hy : -y + y = 0
⊢ -(x + y) + (x + y) = 0
suffices : -x + x + (-y + y) = 0
no goals
case this
R : Type u_1
inst✝¹⁰ : CommSemiring R
M : Type u_2
N : Type u_3
P : Type ?u.1367541
Q : Type ?u.1367544
S : Type ?u.1367547
inst✝⁹ : AddCommGroup M
inst✝⁸ : AddCommGroup N
inst✝⁷ : AddCommGroup P
inst✝⁶ : AddCommGroup Q
inst✝⁵ : AddCommGroup S
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R P
inst✝¹ : Module R Q
inst✝ : Module R S
x✝ x y : M ⊗[R] N
hx : -x + x = 0
hy : -y + y = 0
⊢ -x + x + (-y + y) = 0
rw [hx, hy, add_zero]
R : Type u_1
inst✝¹⁰ : CommSemiring R
M : Type u_2
N : Type u_3
P : Type ?u.1367541
Q : Type ?u.1367544
S : Type ?u.1367547
inst✝⁹ : AddCommGroup M
inst✝⁸ : AddCommGroup N
inst✝⁷ : AddCommGroup P
inst✝⁶ : AddCommGroup Q
inst✝⁵ : AddCommGroup S
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R P
inst✝¹ : Module R Q
inst✝ : Module R S
x✝ x y : M ⊗[R] N
hx : -x + x = 0
hy : -y + y = 0
this : -x + x + (-y + y) = 0
⊢ -(x + y) + (x + y) = -x + x + (-y + y)
R : Type u_1
inst✝¹⁰ : CommSemiring R
M : Type u_2
N : Type u_3
P : Type ?u.1367541
Q : Type ?u.1367544
S : Type ?u.1367547
inst✝⁹ : AddCommGroup M
inst✝⁸ : AddCommGroup N
inst✝⁷ : AddCommGroup P
inst✝⁶ : AddCommGroup Q
inst✝⁵ : AddCommGroup S
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R P
inst✝¹ : Module R Q
inst✝ : Module R S
x✝ x y : M ⊗[R] N
hx : -x + x = 0
hy : -y + y = 0
this : -x + x + (-y + y) = 0
⊢ -(x + y) + (x + y) = 0
rw [← this]
R : Type u_1
inst✝¹⁰ : CommSemiring R
M : Type u_2
N : Type u_3
P : Type ?u.1367541
Q : Type ?u.1367544
S : Type ?u.1367547
inst✝⁹ : AddCommGroup M
inst✝⁸ : AddCommGroup N
inst✝⁷ : AddCommGroup P
inst✝⁶ : AddCommGroup Q
inst✝⁵ : AddCommGroup S
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R P
inst✝¹ : Module R Q
inst✝ : Module R S
x✝ x y : M ⊗[R] N
hx : -x + x = 0
hy : -y + y = 0
this : -x + x + (-y + y) = 0
⊢ { neg := ↑(AddCon.lift (addConGen (Eqv R M N)) (Neg.aux R) (_ : addConGen (Eqv R M N) ≤ AddCon.ker (Neg.aux R))) }.1
        (x + y) +
      (x + y) =
    { neg := ↑(AddCon.lift (addConGen (Eqv R M N)) (Neg.aux R) (_ : addConGen (Eqv R M N) ≤ AddCon.ker (Neg.aux R))) }.1
          x +
        x +
      ({
              neg :=
                ↑(AddCon.lift (addConGen (Eqv R M N)) (Neg.aux R)
                    (_ : addConGen (Eqv R M N) ≤ AddCon.ker (Neg.aux R))) }.1
          y +
        y)
R : Type u_1
inst✝¹⁰ : CommSemiring R
M : Type u_2
N : Type u_3
P : Type ?u.1367541
Q : Type ?u.1367544
S : Type ?u.1367547
inst✝⁹ : AddCommGroup M
inst✝⁸ : AddCommGroup N
inst✝⁷ : AddCommGroup P
inst✝⁶ : AddCommGroup Q
inst✝⁵ : AddCommGroup S
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R P
inst✝¹ : Module R Q
inst✝ : Module R S
x✝ x y : M ⊗[R] N
hx : -x + x = 0
hy : -y + y = 0
this : -x + x + (-y + y) = 0
⊢ -(x + y) + (x + y) = -x + x + (-y + y)
unfold Neg.neg neg
R : Type u_1
inst✝¹⁰ : CommSemiring R
M : Type u_2
N : Type u_3
P : Type ?u.1367541
Q : Type ?u.1367544
S : Type ?u.1367547
inst✝⁹ : AddCommGroup M
inst✝⁸ : AddCommGroup N
inst✝⁷ : AddCommGroup P
inst✝⁶ : AddCommGroup Q
inst✝⁵ : AddCommGroup S
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R P
inst✝¹ : Module R Q
inst✝ : Module R S
x✝ x y : M ⊗[R] N
hx : -x + x = 0
hy : -y + y = 0
this : -x + x + (-y + y) = 0
⊢ ↑(AddCon.lift (addConGen (Eqv R M N)) (Neg.aux R) (_ : addConGen (Eqv R M N) ≤ AddCon.ker (Neg.aux R))) (x + y) +
      (x + y) =
    ↑(AddCon.lift (addConGen (Eqv R M N)) (Neg.aux R) (_ : addConGen (Eqv R M N) ≤ AddCon.ker (Neg.aux R))) x + x +
      (↑(AddCon.lift (addConGen (Eqv R M N)) (Neg.aux R) (_ : addConGen (Eqv R M N) ≤ AddCon.ker (Neg.aux R))) y + y)
R : Type u_1
inst✝¹⁰ : CommSemiring R
M : Type u_2
N : Type u_3
P : Type ?u.1367541
Q : Type ?u.1367544
S : Type ?u.1367547
inst✝⁹ : AddCommGroup M
inst✝⁸ : AddCommGroup N
inst✝⁷ : AddCommGroup P
inst✝⁶ : AddCommGroup Q
inst✝⁵ : AddCommGroup S
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R P
inst✝¹ : Module R Q
inst✝ : Module R S
x✝ x y : M ⊗[R] N
hx : -x + x = 0
hy : -y + y = 0
this : -x + x + (-y + y) = 0
⊢ { neg := ↑(AddCon.lift (addConGen (Eqv R M N)) (Neg.aux R) (_ : addConGen (Eqv R M N) ≤ AddCon.ker (Neg.aux R))) }.1
        (x + y) +
      (x + y) =
    { neg := ↑(AddCon.lift (addConGen (Eqv R M N)) (Neg.aux R) (_ : addConGen (Eqv R M N) ≤ AddCon.ker (Neg.aux R))) }.1
          x +
        x +
      ({
              neg :=
                ↑(AddCon.lift (addConGen (Eqv R M N)) (Neg.aux R)
                    (_ : addConGen (Eqv R M N) ≤ AddCon.ker (Neg.aux R))) }.1
          y +
        y)
simp only
R : Type u_1
inst✝¹⁰ : CommSemiring R
M : Type u_2
N : Type u_3
P : Type ?u.1367541
Q : Type ?u.1367544
S : Type ?u.1367547
inst✝⁹ : AddCommGroup M
inst✝⁸ : AddCommGroup N
inst✝⁷ : AddCommGroup P
inst✝⁶ : AddCommGroup Q
inst✝⁵ : AddCommGroup S
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R P
inst✝¹ : Module R Q
inst✝ : Module R S
x✝ x y : M ⊗[R] N
hx : -x + x = 0
hy : -y + y = 0
this : -x + x + (-y + y) = 0
⊢ ↑(AddCon.lift (addConGen (Eqv R M N)) (Neg.aux R) (_ : addConGen (Eqv R M N) ≤ AddCon.ker (Neg.aux R))) x +
        ↑(AddCon.lift (addConGen (Eqv R M N)) (Neg.aux R) (_ : addConGen (Eqv R M N) ≤ AddCon.ker (Neg.aux R))) y +
      (x + y) =
    ↑(AddCon.lift (addConGen (Eqv R M N)) (Neg.aux R) (_ : addConGen (Eqv R M N) ≤ AddCon.ker (Neg.aux R))) x + x +
      (↑(AddCon.lift (addConGen (Eqv R M N)) (Neg.aux R) (_ : addConGen (Eqv R M N) ≤ AddCon.ker (Neg.aux R))) y + y)
R : Type u_1
inst✝¹⁰ : CommSemiring R
M : Type u_2
N : Type u_3
P : Type ?u.1367541
Q : Type ?u.1367544
S : Type ?u.1367547
inst✝⁹ : AddCommGroup M
inst✝⁸ : AddCommGroup N
inst✝⁷ : AddCommGroup P
inst✝⁶ : AddCommGroup Q
inst✝⁵ : AddCommGroup S
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R P
inst✝¹ : Module R Q
inst✝ : Module R S
x✝ x y : M ⊗[R] N
hx : -x + x = 0
hy : -y + y = 0
this : -x + x + (-y + y) = 0
⊢ ↑(AddCon.lift (addConGen (Eqv R M N)) (Neg.aux R) (_ : addConGen (Eqv R M N) ≤ AddCon.ker (Neg.aux R))) (x + y) +
      (x + y) =
    ↑(AddCon.lift (addConGen (Eqv R M N)) (Neg.aux R) (_ : addConGen (Eqv R M N) ≤ AddCon.ker (Neg.aux R))) x + x +
      (↑(AddCon.lift (addConGen (Eqv R M N)) (Neg.aux R) (_ : addConGen (Eqv R M N) ≤ AddCon.ker (Neg.aux R))) y + y)
rw [AddMonoidHom.map_add]
no goals
R : Type u_1
inst✝¹⁰ : CommSemiring R
M : Type u_2
N : Type u_3
P : Type ?u.1367541
Q : Type ?u.1367544
S : Type ?u.1367547
inst✝⁹ : AddCommGroup M
inst✝⁸ : AddCommGroup N
inst✝⁷ : AddCommGroup P
inst✝⁶ : AddCommGroup Q
inst✝⁵ : AddCommGroup S
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R P
inst✝¹ : Module R Q
inst✝ : Module R S
x✝ x y : M ⊗[R] N
hx : -x + x = 0
hy : -y + y = 0
this : -x + x + (-y + y) = 0
⊢ ↑(AddCon.lift (addConGen (Eqv R M N)) (Neg.aux R) (_ : addConGen (Eqv R M N) ≤ AddCon.ker (Neg.aux R))) x +
        ↑(AddCon.lift (addConGen (Eqv R M N)) (Neg.aux R) (_ : addConGen (Eqv R M N) ≤ AddCon.ker (Neg.aux R))) y +
      (x + y) =
    ↑(AddCon.lift (addConGen (Eqv R M N)) (Neg.aux R) (_ : addConGen (Eqv R M N) ≤ AddCon.ker (Neg.aux R))) x + x +
      (↑(AddCon.lift (addConGen (Eqv R M N)) (Neg.aux R) (_ : addConGen (Eqv R M N) ≤ AddCon.ker (Neg.aux R))) y + y)
abel