case mp
R : Type u_1
R₁ : Type u_2
R₂ : Type ?u.197485
R₃ : Type ?u.197488
M : Type ?u.197491
M₁ : Type u_3
M₂ : Type ?u.197497
Mₗ₁ : Type ?u.197500
Mₗ₁' : Type ?u.197503
Mₗ₂ : Type ?u.197506
Mₗ₂' : Type ?u.197509
K : Type ?u.197512
K₁ : Type ?u.197515
K₂ : Type ?u.197518
V : Type ?u.197521
V₁ : Type ?u.197524
V₂ : Type ?u.197527
n : Type ?u.197530
inst✝⁵ : CommRing R
inst✝⁴ : CommSemiring R₁
inst✝³ : AddCommMonoid M₁
inst✝² : Module R₁ M₁
I₁ I₂ I : R₁ →+* R
B✝ : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
B : M₁ →ₛₗ[I] M₁ →ₛₗ[I] R
h : IsAlt B
⊢ B = -flip B

case mpr
R : Type u_1
R₁ : Type u_2
R₂ : Type ?u.197485
R₃ : Type ?u.197488
M : Type ?u.197491
M₁ : Type u_3
M₂ : Type ?u.197497
Mₗ₁ : Type ?u.197500
Mₗ₁' : Type ?u.197503
Mₗ₂ : Type ?u.197506
Mₗ₂' : Type ?u.197509
K : Type ?u.197512
K₁ : Type ?u.197515
K₂ : Type ?u.197518
V : Type ?u.197521
V₁ : Type ?u.197524
V₂ : Type ?u.197527
n : Type ?u.197530
inst✝⁵ : CommRing R
inst✝⁴ : CommSemiring R₁
inst✝³ : AddCommMonoid M₁
inst✝² : Module R₁ M₁
I₁ I₂ I : R₁ →+* R
B✝ : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
B : M₁ →ₛₗ[I] M₁ →ₛₗ[I] R
h : B = -flip B
⊢ IsAlt B
R : Type u_1
R₁ : Type u_2
R₂ : Type ?u.197485
R₃ : Type ?u.197488
M : Type ?u.197491
M₁ : Type u_3
M₂ : Type ?u.197497
Mₗ₁ : Type ?u.197500
Mₗ₁' : Type ?u.197503
Mₗ₂ : Type ?u.197506
Mₗ₂' : Type ?u.197509
K : Type ?u.197512
K₁ : Type ?u.197515
K₂ : Type ?u.197518
V : Type ?u.197521
V₁ : Type ?u.197524
V₂ : Type ?u.197527
n : Type ?u.197530
inst✝⁵ : CommRing R
inst✝⁴ : CommSemiring R₁
inst✝³ : AddCommMonoid M₁
inst✝² : Module R₁ M₁
I₁ I₂ I : R₁ →+* R
B✝ : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
B : M₁ →ₛₗ[I] M₁ →ₛₗ[I] R
⊢ IsAlt B ↔ B = -flip B
constructor <;> intro h
case mpr
R : Type u_1
R₁ : Type u_2
R₂ : Type ?u.197485
R₃ : Type ?u.197488
M : Type ?u.197491
M₁ : Type u_3
M₂ : Type ?u.197497
Mₗ₁ : Type ?u.197500
Mₗ₁' : Type ?u.197503
Mₗ₂ : Type ?u.197506
Mₗ₂' : Type ?u.197509
K : Type ?u.197512
K₁ : Type ?u.197515
K₂ : Type ?u.197518
V : Type ?u.197521
V₁ : Type ?u.197524
V₂ : Type ?u.197527
n : Type ?u.197530
inst✝⁵ : CommRing R
inst✝⁴ : CommSemiring R₁
inst✝³ : AddCommMonoid M₁
inst✝² : Module R₁ M₁
I₁ I₂ I : R₁ →+* R
B✝ : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
B : M₁ →ₛₗ[I] M₁ →ₛₗ[I] R
h : B = -flip B
x : M₁
⊢ ↑(↑B x) x = 0
case mpr
R : Type u_1
R₁ : Type u_2
R₂ : Type ?u.197485
R₃ : Type ?u.197488
M : Type ?u.197491
M₁ : Type u_3
M₂ : Type ?u.197497
Mₗ₁ : Type ?u.197500
Mₗ₁' : Type ?u.197503
Mₗ₂ : Type ?u.197506
Mₗ₂' : Type ?u.197509
K : Type ?u.197512
K₁ : Type ?u.197515
K₂ : Type ?u.197518
V : Type ?u.197521
V₁ : Type ?u.197524
V₂ : Type ?u.197527
n : Type ?u.197530
inst✝⁵ : CommRing R
inst✝⁴ : CommSemiring R₁
inst✝³ : AddCommMonoid M₁
inst✝² : Module R₁ M₁
I₁ I₂ I : R₁ →+* R
B✝ : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
B : M₁ →ₛₗ[I] M₁ →ₛₗ[I] R
h : B = -flip B
⊢ IsAlt B
intro x
case mpr
R : Type u_1
R₁ : Type u_2
R₂ : Type ?u.197485
R₃ : Type ?u.197488
M : Type ?u.197491
M₁ : Type u_3
M₂ : Type ?u.197497
Mₗ₁ : Type ?u.197500
Mₗ₁' : Type ?u.197503
Mₗ₂ : Type ?u.197506
Mₗ₂' : Type ?u.197509
K : Type ?u.197512
K₁ : Type ?u.197515
K₂ : Type ?u.197518
V : Type ?u.197521
V₁ : Type ?u.197524
V₂ : Type ?u.197527
n : Type ?u.197530
inst✝⁵ : CommRing R
inst✝⁴ : CommSemiring R₁
inst✝³ : AddCommMonoid M₁
inst✝² : Module R₁ M₁
I₁ I₂ I : R₁ →+* R
B✝ : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
B : M₁ →ₛₗ[I] M₁ →ₛₗ[I] R
h : B = -flip B
x : M₁
h' : ↑(↑B x) x = ↑(↑(-flip B) x) x := congr_fun₂ h x x
⊢ ↑(↑B x) x = 0
case mpr
R : Type u_1
R₁ : Type u_2
R₂ : Type ?u.197485
R₃ : Type ?u.197488
M : Type ?u.197491
M₁ : Type u_3
M₂ : Type ?u.197497
Mₗ₁ : Type ?u.197500
Mₗ₁' : Type ?u.197503
Mₗ₂ : Type ?u.197506
Mₗ₂' : Type ?u.197509
K : Type ?u.197512
K₁ : Type ?u.197515
K₂ : Type ?u.197518
V : Type ?u.197521
V₁ : Type ?u.197524
V₂ : Type ?u.197527
n : Type ?u.197530
inst✝⁵ : CommRing R
inst✝⁴ : CommSemiring R₁
inst✝³ : AddCommMonoid M₁
inst✝² : Module R₁ M₁
I₁ I₂ I : R₁ →+* R
B✝ : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
B : M₁ →ₛₗ[I] M₁ →ₛₗ[I] R
h : B = -flip B
x : M₁
⊢ ↑(↑B x) x = 0
let h' := congr_fun₂ h x x
case mpr
R : Type u_1
R₁ : Type u_2
R₂ : Type ?u.197485
R₃ : Type ?u.197488
M : Type ?u.197491
M₁ : Type u_3
M₂ : Type ?u.197497
Mₗ₁ : Type ?u.197500
Mₗ₁' : Type ?u.197503
Mₗ₂ : Type ?u.197506
Mₗ₂' : Type ?u.197509
K : Type ?u.197512
K₁ : Type ?u.197515
K₂ : Type ?u.197518
V : Type ?u.197521
V₁ : Type ?u.197524
V₂ : Type ?u.197527
n : Type ?u.197530
inst✝⁵ : CommRing R
inst✝⁴ : CommSemiring R₁
inst✝³ : AddCommMonoid M₁
inst✝² : Module R₁ M₁
I₁ I₂ I : R₁ →+* R
B✝ : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
B : M₁ →ₛₗ[I] M₁ →ₛₗ[I] R
h : B = -flip B
x : M₁
h' : ↑(↑B x) x + ↑(↑B x) x = 0
⊢ ↑(↑B x) x = 0
case mpr
R : Type u_1
R₁ : Type u_2
R₂ : Type ?u.197485
R₃ : Type ?u.197488
M : Type ?u.197491
M₁ : Type u_3
M₂ : Type ?u.197497
Mₗ₁ : Type ?u.197500
Mₗ₁' : Type ?u.197503
Mₗ₂ : Type ?u.197506
Mₗ₂' : Type ?u.197509
K : Type ?u.197512
K₁ : Type ?u.197515
K₂ : Type ?u.197518
V : Type ?u.197521
V₁ : Type ?u.197524
V₂ : Type ?u.197527
n : Type ?u.197530
inst✝⁵ : CommRing R
inst✝⁴ : CommSemiring R₁
inst✝³ : AddCommMonoid M₁
inst✝² : Module R₁ M₁
I₁ I₂ I : R₁ →+* R
B✝ : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
B : M₁ →ₛₗ[I] M₁ →ₛₗ[I] R
h : B = -flip B
x : M₁
h' : ↑(↑B x) x = ↑(↑(-flip B) x) x := congr_fun₂ h x x
⊢ ↑(↑B x) x = 0
simp only [neg_apply, flip_apply, ← add_eq_zero_iff_eq_neg] at h'
no goals
case mpr
R : Type u_1
R₁ : Type u_2
R₂ : Type ?u.197485
R₃ : Type ?u.197488
M : Type ?u.197491
M₁ : Type u_3
M₂ : Type ?u.197497
Mₗ₁ : Type ?u.197500
Mₗ₁' : Type ?u.197503
Mₗ₂ : Type ?u.197506
Mₗ₂' : Type ?u.197509
K : Type ?u.197512
K₁ : Type ?u.197515
K₂ : Type ?u.197518
V : Type ?u.197521
V₁ : Type ?u.197524
V₂ : Type ?u.197527
n : Type ?u.197530
inst✝⁵ : CommRing R
inst✝⁴ : CommSemiring R₁
inst✝³ : AddCommMonoid M₁
inst✝² : Module R₁ M₁
I₁ I₂ I : R₁ →+* R
B✝ : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
B : M₁ →ₛₗ[I] M₁ →ₛₗ[I] R
h : B = -flip B
x : M₁
h' : ↑(↑B x) x + ↑(↑B x) x = 0
⊢ ↑(↑B x) x = 0
exact add_self_eq_zero.mp h'
case mp.h.h
R : Type u_1
R₁ : Type u_2
R₂ : Type ?u.197485
R₃ : Type ?u.197488
M : Type ?u.197491
M₁ : Type u_3
M₂ : Type ?u.197497
Mₗ₁ : Type ?u.197500
Mₗ₁' : Type ?u.197503
Mₗ₂ : Type ?u.197506
Mₗ₂' : Type ?u.197509
K : Type ?u.197512
K₁ : Type ?u.197515
K₂ : Type ?u.197518
V : Type ?u.197521
V₁ : Type ?u.197524
V₂ : Type ?u.197527
n : Type ?u.197530
inst✝⁵ : CommRing R
inst✝⁴ : CommSemiring R₁
inst✝³ : AddCommMonoid M₁
inst✝² : Module R₁ M₁
I₁ I₂ I : R₁ →+* R
B✝ : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
B : M₁ →ₛₗ[I] M₁ →ₛₗ[I] R
h : IsAlt B
x✝¹ x✝ : M₁
⊢ ↑(↑B x✝¹) x✝ = ↑(↑(-flip B) x✝¹) x✝
case mp
R : Type u_1
R₁ : Type u_2
R₂ : Type ?u.197485
R₃ : Type ?u.197488
M : Type ?u.197491
M₁ : Type u_3
M₂ : Type ?u.197497
Mₗ₁ : Type ?u.197500
Mₗ₁' : Type ?u.197503
Mₗ₂ : Type ?u.197506
Mₗ₂' : Type ?u.197509
K : Type ?u.197512
K₁ : Type ?u.197515
K₂ : Type ?u.197518
V : Type ?u.197521
V₁ : Type ?u.197524
V₂ : Type ?u.197527
n : Type ?u.197530
inst✝⁵ : CommRing R
inst✝⁴ : CommSemiring R₁
inst✝³ : AddCommMonoid M₁
inst✝² : Module R₁ M₁
I₁ I₂ I : R₁ →+* R
B✝ : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
B : M₁ →ₛₗ[I] M₁ →ₛₗ[I] R
h : IsAlt B
⊢ B = -flip B
ext
case mp.h.h
R : Type u_1
R₁ : Type u_2
R₂ : Type ?u.197485
R₃ : Type ?u.197488
M : Type ?u.197491
M₁ : Type u_3
M₂ : Type ?u.197497
Mₗ₁ : Type ?u.197500
Mₗ₁' : Type ?u.197503
Mₗ₂ : Type ?u.197506
Mₗ₂' : Type ?u.197509
K : Type ?u.197512
K₁ : Type ?u.197515
K₂ : Type ?u.197518
V : Type ?u.197521
V₁ : Type ?u.197524
V₂ : Type ?u.197527
n : Type ?u.197530
inst✝⁵ : CommRing R
inst✝⁴ : CommSemiring R₁
inst✝³ : AddCommMonoid M₁
inst✝² : Module R₁ M₁
I₁ I₂ I : R₁ →+* R
B✝ : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
B : M₁ →ₛₗ[I] M₁ →ₛₗ[I] R
h : IsAlt B
x✝¹ x✝ : M₁
⊢ ↑(↑B x✝¹) x✝ = -↑(↑B x✝) x✝¹
case mp.h.h
R : Type u_1
R₁ : Type u_2
R₂ : Type ?u.197485
R₃ : Type ?u.197488
M : Type ?u.197491
M₁ : Type u_3
M₂ : Type ?u.197497
Mₗ₁ : Type ?u.197500
Mₗ₁' : Type ?u.197503
Mₗ₂ : Type ?u.197506
Mₗ₂' : Type ?u.197509
K : Type ?u.197512
K₁ : Type ?u.197515
K₂ : Type ?u.197518
V : Type ?u.197521
V₁ : Type ?u.197524
V₂ : Type ?u.197527
n : Type ?u.197530
inst✝⁵ : CommRing R
inst✝⁴ : CommSemiring R₁
inst✝³ : AddCommMonoid M₁
inst✝² : Module R₁ M₁
I₁ I₂ I : R₁ →+* R
B✝ : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
B : M₁ →ₛₗ[I] M₁ →ₛₗ[I] R
h : IsAlt B
x✝¹ x✝ : M₁
⊢ ↑(↑B x✝¹) x✝ = ↑(↑(-flip B) x✝¹) x✝
simp_rw [neg_apply, flip_apply]
no goals
case mp.h.h
R : Type u_1
R₁ : Type u_2
R₂ : Type ?u.197485
R₃ : Type ?u.197488
M : Type ?u.197491
M₁ : Type u_3
M₂ : Type ?u.197497
Mₗ₁ : Type ?u.197500
Mₗ₁' : Type ?u.197503
Mₗ₂ : Type ?u.197506
Mₗ₂' : Type ?u.197509
K : Type ?u.197512
K₁ : Type ?u.197515
K₂ : Type ?u.197518
V : Type ?u.197521
V₁ : Type ?u.197524
V₂ : Type ?u.197527
n : Type ?u.197530
inst✝⁵ : CommRing R
inst✝⁴ : CommSemiring R₁
inst✝³ : AddCommMonoid M₁
inst✝² : Module R₁ M₁
I₁ I₂ I : R₁ →+* R
B✝ : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
B : M₁ →ₛₗ[I] M₁ →ₛₗ[I] R
h : IsAlt B
x✝¹ x✝ : M₁
⊢ ↑(↑B x✝¹) x✝ = -↑(↑B x✝) x✝¹
exact (h.neg _ _).symm