R : Type ?u.957968
M : Type ?u.957971
inst✝¹⁸ : Semiring R
inst✝¹⁷ : AddCommMonoid M
inst✝¹⁶ : Module R M
R₁ : Type u_1
M₁ : Type u_2
inst✝¹⁵ : Ring R₁
inst✝¹⁴ : AddCommGroup M₁
inst✝¹³ : Module R₁ M₁
R₂ : Type ?u.958619
M₂ : Type ?u.958622
inst✝¹² : CommSemiring R₂
inst✝¹¹ : AddCommMonoid M₂
inst✝¹⁰ : Module R₂ M₂
R₃ : Type ?u.958809
M₃ : Type ?u.958812
inst✝⁹ : CommRing R₃
inst✝⁸ : AddCommGroup M₃
inst✝⁷ : Module R₃ M₃
V : Type ?u.959400
K : Type ?u.959403
inst✝⁶ : Field K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
B : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
M₂' : Type ?u.960617
M₂'' : Type ?u.960620
inst✝³ : AddCommMonoid M₂'
inst✝² : AddCommMonoid M₂''
inst✝¹ : Module R₂ M₂'
inst✝ : Module R₂ M₂''
H : IsAlt B₁
x y : M₁
H1 : bilin B₁ (x + y) (x + y) = 0
⊢ -bilin B₁ x y = bilin B₁ y x
R : Type ?u.957968
M : Type ?u.957971
inst✝¹⁸ : Semiring R
inst✝¹⁷ : AddCommMonoid M
inst✝¹⁶ : Module R M
R₁ : Type u_1
M₁ : Type u_2
inst✝¹⁵ : Ring R₁
inst✝¹⁴ : AddCommGroup M₁
inst✝¹³ : Module R₁ M₁
R₂ : Type ?u.958619
M₂ : Type ?u.958622
inst✝¹² : CommSemiring R₂
inst✝¹¹ : AddCommMonoid M₂
inst✝¹⁰ : Module R₂ M₂
R₃ : Type ?u.958809
M₃ : Type ?u.958812
inst✝⁹ : CommRing R₃
inst✝⁸ : AddCommGroup M₃
inst✝⁷ : Module R₃ M₃
V : Type ?u.959400
K : Type ?u.959403
inst✝⁶ : Field K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
B : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
M₂' : Type ?u.960617
M₂'' : Type ?u.960620
inst✝³ : AddCommMonoid M₂'
inst✝² : AddCommMonoid M₂''
inst✝¹ : Module R₂ M₂'
inst✝ : Module R₂ M₂''
H : IsAlt B₁
x y : M₁
⊢ -bilin B₁ x y = bilin B₁ y x
have H1 : B₁ (x + y) (x + y) = 0 := self_eq_zero H (x + y)
R : Type ?u.957968
M : Type ?u.957971
inst✝¹⁸ : Semiring R
inst✝¹⁷ : AddCommMonoid M
inst✝¹⁶ : Module R M
R₁ : Type u_1
M₁ : Type u_2
inst✝¹⁵ : Ring R₁
inst✝¹⁴ : AddCommGroup M₁
inst✝¹³ : Module R₁ M₁
R₂ : Type ?u.958619
M₂ : Type ?u.958622
inst✝¹² : CommSemiring R₂
inst✝¹¹ : AddCommMonoid M₂
inst✝¹⁰ : Module R₂ M₂
R₃ : Type ?u.958809
M₃ : Type ?u.958812
inst✝⁹ : CommRing R₃
inst✝⁸ : AddCommGroup M₃
inst✝⁷ : Module R₃ M₃
V : Type ?u.959400
K : Type ?u.959403
inst✝⁶ : Field K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
B : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
M₂' : Type ?u.960617
M₂'' : Type ?u.960620
inst✝³ : AddCommMonoid M₂'
inst✝² : AddCommMonoid M₂''
inst✝¹ : Module R₂ M₂'
inst✝ : Module R₂ M₂''
H : IsAlt B₁
x y : M₁
H1 : -bilin B₁ x y = bilin B₁ y x
⊢ -bilin B₁ x y = bilin B₁ y x
R : Type ?u.957968
M : Type ?u.957971
inst✝¹⁸ : Semiring R
inst✝¹⁷ : AddCommMonoid M
inst✝¹⁶ : Module R M
R₁ : Type u_1
M₁ : Type u_2
inst✝¹⁵ : Ring R₁
inst✝¹⁴ : AddCommGroup M₁
inst✝¹³ : Module R₁ M₁
R₂ : Type ?u.958619
M₂ : Type ?u.958622
inst✝¹² : CommSemiring R₂
inst✝¹¹ : AddCommMonoid M₂
inst✝¹⁰ : Module R₂ M₂
R₃ : Type ?u.958809
M₃ : Type ?u.958812
inst✝⁹ : CommRing R₃
inst✝⁸ : AddCommGroup M₃
inst✝⁷ : Module R₃ M₃
V : Type ?u.959400
K : Type ?u.959403
inst✝⁶ : Field K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
B : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
M₂' : Type ?u.960617
M₂'' : Type ?u.960620
inst✝³ : AddCommMonoid M₂'
inst✝² : AddCommMonoid M₂''
inst✝¹ : Module R₂ M₂'
inst✝ : Module R₂ M₂''
H : IsAlt B₁
x y : M₁
H1 : bilin B₁ (x + y) (x + y) = 0
⊢ -bilin B₁ x y = bilin B₁ y x
rw [add_left, add_right, add_right, self_eq_zero H, self_eq_zero H, zero_add, add_zero,
  add_eq_zero_iff_neg_eq] at H1
no goals
R : Type ?u.957968
M : Type ?u.957971
inst✝¹⁸ : Semiring R
inst✝¹⁷ : AddCommMonoid M
inst✝¹⁶ : Module R M
R₁ : Type u_1
M₁ : Type u_2
inst✝¹⁵ : Ring R₁
inst✝¹⁴ : AddCommGroup M₁
inst✝¹³ : Module R₁ M₁
R₂ : Type ?u.958619
M₂ : Type ?u.958622
inst✝¹² : CommSemiring R₂
inst✝¹¹ : AddCommMonoid M₂
inst✝¹⁰ : Module R₂ M₂
R₃ : Type ?u.958809
M₃ : Type ?u.958812
inst✝⁹ : CommRing R₃
inst✝⁸ : AddCommGroup M₃
inst✝⁷ : Module R₃ M₃
V : Type ?u.959400
K : Type ?u.959403
inst✝⁶ : Field K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
B : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
M₂' : Type ?u.960617
M₂'' : Type ?u.960620
inst✝³ : AddCommMonoid M₂'
inst✝² : AddCommMonoid M₂''
inst✝¹ : Module R₂ M₂'
inst✝ : Module R₂ M₂''
H : IsAlt B₁
x y : M₁
H1 : -bilin B₁ x y = bilin B₁ y x
⊢ -bilin B₁ x y = bilin B₁ y x
exact H1