case intro
S : Type ?u.74856
R : Type u_1
R₁ : Type ?u.74862
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
Q : QuadraticForm R M
x y z : M
B : BilinForm R M
h : ∀ (x y : M), ↑Q (x + y) = ↑Q x + ↑Q y + BilinForm.bilin B x y
⊢ ↑Q (x + y + z) + (↑Q x + ↑Q y + ↑Q z) = ↑Q (x + y) + ↑Q (y + z) + ↑Q (z + x)
S : Type ?u.74856
R : Type u_1
R₁ : Type ?u.74862
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
Q : QuadraticForm R M
x y z : M
⊢ ↑Q (x + y + z) + (↑Q x + ↑Q y + ↑Q z) = ↑Q (x + y) + ↑Q (y + z) + ↑Q (z + x)
obtain ⟨B, h⟩ := Q.exists_companion
case intro
S : Type ?u.74856
R : Type u_1
R₁ : Type ?u.74862
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
Q : QuadraticForm R M
x y z : M
B : BilinForm R M
h : ∀ (x y : M), ↑Q (x + y) = ↑Q x + ↑Q y + BilinForm.bilin B x y
⊢ ↑Q (x + y + z) + (↑Q x + ↑Q y + ↑Q z) = ↑Q (x + y) + ↑Q (y + z) + ↑Q (x + z)
case intro
S : Type ?u.74856
R : Type u_1
R₁ : Type ?u.74862
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
Q : QuadraticForm R M
x y z : M
B : BilinForm R M
h : ∀ (x y : M), ↑Q (x + y) = ↑Q x + ↑Q y + BilinForm.bilin B x y
⊢ ↑Q (x + y + z) + (↑Q x + ↑Q y + ↑Q z) = ↑Q (x + y) + ↑Q (y + z) + ↑Q (z + x)
rw [add_comm z x]
case intro
S : Type ?u.74856
R : Type u_1
R₁ : Type ?u.74862
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
Q : QuadraticForm R M
x y z : M
B : BilinForm R M
h : ∀ (x y : M), ↑Q (x + y) = ↑Q x + ↑Q y + BilinForm.bilin B x y
⊢ ↑Q x + ↑Q y + BilinForm.bilin B x y + ↑Q z + (BilinForm.bilin B x z + BilinForm.bilin B y z) + (↑Q x + ↑Q y + ↑Q z) =
    ↑Q x + ↑Q y + BilinForm.bilin B x y + (↑Q y + ↑Q z + BilinForm.bilin B y z) + (↑Q x + ↑Q z + BilinForm.bilin B x z)
case intro
S : Type ?u.74856
R : Type u_1
R₁ : Type ?u.74862
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
Q : QuadraticForm R M
x y z : M
B : BilinForm R M
h : ∀ (x y : M), ↑Q (x + y) = ↑Q x + ↑Q y + BilinForm.bilin B x y
⊢ ↑Q (x + y + z) + (↑Q x + ↑Q y + ↑Q z) = ↑Q (x + y) + ↑Q (y + z) + ↑Q (x + z)
simp [h]
no goals
case intro
S : Type ?u.74856
R : Type u_1
R₁ : Type ?u.74862
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
Q : QuadraticForm R M
x y z : M
B : BilinForm R M
h : ∀ (x y : M), ↑Q (x + y) = ↑Q x + ↑Q y + BilinForm.bilin B x y
⊢ ↑Q x + ↑Q y + BilinForm.bilin B x y + ↑Q z + (BilinForm.bilin B x z + BilinForm.bilin B y z) + (↑Q x + ↑Q y + ↑Q z) =
    ↑Q x + ↑Q y + BilinForm.bilin B x y + (↑Q y + ↑Q z + BilinForm.bilin B y z) + (↑Q x + ↑Q z + BilinForm.bilin B x z)
abel