ι : Type u_1
R✝ : Type ?u.66145
M₁ : Type ?u.66148
M₂ : Type ?u.66151
N₁ : Type ?u.66154
N₂ : Type ?u.66157
Mᵢ : ι → Type u_3
Nᵢ : ι → Type ?u.66167
inst✝¹⁵ : Semiring R✝
inst✝¹⁴ : AddCommMonoid M₁
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : AddCommMonoid N₁
inst✝¹¹ : AddCommMonoid N₂
inst✝¹⁰ : Module R✝ M₁
inst✝⁹ : Module R✝ M₂
inst✝⁸ : Module R✝ N₁
inst✝⁷ : Module R✝ N₂
inst✝⁶ : (i : ι) → AddCommMonoid (Mᵢ i)
inst✝⁵ : (i : ι) → AddCommMonoid (Nᵢ i)
inst✝⁴ : (i : ι) → Module R✝ (Mᵢ i)
inst✝³ : (i : ι) → Module R✝ (Nᵢ i)
inst✝² : Fintype ι
R : Type u_2
inst✝¹ : OrderedRing R
inst✝ : (i : ι) → Module R (Mᵢ i)
Q : (i : ι) → QuadraticForm R (Mᵢ i)
h : ∀ (x : (i : ι) → Mᵢ i), ∑ i : ι, ↑(Q i) (x i) = 0 → ∀ (a : ι), x a = 0
⊢ ∀ (i : ι), Anisotropic (Q i)
ι : Type u_1
R✝ : Type ?u.66145
M₁ : Type ?u.66148
M₂ : Type ?u.66151
N₁ : Type ?u.66154
N₂ : Type ?u.66157
Mᵢ : ι → Type u_3
Nᵢ : ι → Type ?u.66167
inst✝¹⁵ : Semiring R✝
inst✝¹⁴ : AddCommMonoid M₁
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : AddCommMonoid N₁
inst✝¹¹ : AddCommMonoid N₂
inst✝¹⁰ : Module R✝ M₁
inst✝⁹ : Module R✝ M₂
inst✝⁸ : Module R✝ N₁
inst✝⁷ : Module R✝ N₂
inst✝⁶ : (i : ι) → AddCommMonoid (Mᵢ i)
inst✝⁵ : (i : ι) → AddCommMonoid (Nᵢ i)
inst✝⁴ : (i : ι) → Module R✝ (Mᵢ i)
inst✝³ : (i : ι) → Module R✝ (Nᵢ i)
inst✝² : Fintype ι
R : Type u_2
inst✝¹ : OrderedRing R
inst✝ : (i : ι) → Module R (Mᵢ i)
Q : (i : ι) → QuadraticForm R (Mᵢ i)
h : Anisotropic (pi Q)
⊢ ∀ (i : ι), Anisotropic (Q i)
simp_rw [Anisotropic, pi_apply, Function.funext_iff, Pi.zero_apply] at h
ι : Type u_1
R✝ : Type ?u.66145
M₁ : Type ?u.66148
M₂ : Type ?u.66151
N₁ : Type ?u.66154
N₂ : Type ?u.66157
Mᵢ : ι → Type u_3
Nᵢ : ι → Type ?u.66167
inst✝¹⁵ : Semiring R✝
inst✝¹⁴ : AddCommMonoid M₁
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : AddCommMonoid N₁
inst✝¹¹ : AddCommMonoid N₂
inst✝¹⁰ : Module R✝ M₁
inst✝⁹ : Module R✝ M₂
inst✝⁸ : Module R✝ N₁
inst✝⁷ : Module R✝ N₂
inst✝⁶ : (i : ι) → AddCommMonoid (Mᵢ i)
inst✝⁵ : (i : ι) → AddCommMonoid (Nᵢ i)
inst✝⁴ : (i : ι) → Module R✝ (Mᵢ i)
inst✝³ : (i : ι) → Module R✝ (Nᵢ i)
inst✝² : Fintype ι
R : Type u_2
inst✝¹ : OrderedRing R
inst✝ : (i : ι) → Module R (Mᵢ i)
Q : (i : ι) → QuadraticForm R (Mᵢ i)
h : ∀ (x : (i : ι) → Mᵢ i), ∑ i : ι, ↑(Q i) (x i) = 0 → ∀ (a : ι), x a = 0
i : ι
x : Mᵢ i
hx : ↑(Q i) x = 0
⊢ x = 0
ι : Type u_1
R✝ : Type ?u.66145
M₁ : Type ?u.66148
M₂ : Type ?u.66151
N₁ : Type ?u.66154
N₂ : Type ?u.66157
Mᵢ : ι → Type u_3
Nᵢ : ι → Type ?u.66167
inst✝¹⁵ : Semiring R✝
inst✝¹⁴ : AddCommMonoid M₁
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : AddCommMonoid N₁
inst✝¹¹ : AddCommMonoid N₂
inst✝¹⁰ : Module R✝ M₁
inst✝⁹ : Module R✝ M₂
inst✝⁸ : Module R✝ N₁
inst✝⁷ : Module R✝ N₂
inst✝⁶ : (i : ι) → AddCommMonoid (Mᵢ i)
inst✝⁵ : (i : ι) → AddCommMonoid (Nᵢ i)
inst✝⁴ : (i : ι) → Module R✝ (Mᵢ i)
inst✝³ : (i : ι) → Module R✝ (Nᵢ i)
inst✝² : Fintype ι
R : Type u_2
inst✝¹ : OrderedRing R
inst✝ : (i : ι) → Module R (Mᵢ i)
Q : (i : ι) → QuadraticForm R (Mᵢ i)
h : ∀ (x : (i : ι) → Mᵢ i), ∑ i : ι, ↑(Q i) (x i) = 0 → ∀ (a : ι), x a = 0
⊢ ∀ (i : ι), Anisotropic (Q i)
intro i x hx
case refine_2
ι : Type u_1
R✝ : Type ?u.66145
M₁ : Type ?u.66148
M₂ : Type ?u.66151
N₁ : Type ?u.66154
N₂ : Type ?u.66157
Mᵢ : ι → Type u_3
Nᵢ : ι → Type ?u.66167
inst✝¹⁵ : Semiring R✝
inst✝¹⁴ : AddCommMonoid M₁
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : AddCommMonoid N₁
inst✝¹¹ : AddCommMonoid N₂
inst✝¹⁰ : Module R✝ M₁
inst✝⁹ : Module R✝ M₂
inst✝⁸ : Module R✝ N₁
inst✝⁷ : Module R✝ N₂
inst✝⁶ : (i : ι) → AddCommMonoid (Mᵢ i)
inst✝⁵ : (i : ι) → AddCommMonoid (Nᵢ i)
inst✝⁴ : (i : ι) → Module R✝ (Mᵢ i)
inst✝³ : (i : ι) → Module R✝ (Nᵢ i)
inst✝² : Fintype ι
R : Type u_2
inst✝¹ : OrderedRing R
inst✝ : (i : ι) → Module R (Mᵢ i)
Q : (i : ι) → QuadraticForm R (Mᵢ i)
h : ∀ (x : (i : ι) → Mᵢ i), ∑ i : ι, ↑(Q i) (x i) = 0 → ∀ (a : ι), x a = 0
i : ι
x : Mᵢ i
hx : ↑(Q i) x = 0
this : Pi.single i x i = 0
⊢ x = 0

case refine_1
ι : Type u_1
R✝ : Type ?u.66145
M₁ : Type ?u.66148
M₂ : Type ?u.66151
N₁ : Type ?u.66154
N₂ : Type ?u.66157
Mᵢ : ι → Type u_3
Nᵢ : ι → Type ?u.66167
inst✝¹⁵ : Semiring R✝
inst✝¹⁴ : AddCommMonoid M₁
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : AddCommMonoid N₁
inst✝¹¹ : AddCommMonoid N₂
inst✝¹⁰ : Module R✝ M₁
inst✝⁹ : Module R✝ M₂
inst✝⁸ : Module R✝ N₁
inst✝⁷ : Module R✝ N₂
inst✝⁶ : (i : ι) → AddCommMonoid (Mᵢ i)
inst✝⁵ : (i : ι) → AddCommMonoid (Nᵢ i)
inst✝⁴ : (i : ι) → Module R✝ (Mᵢ i)
inst✝³ : (i : ι) → Module R✝ (Nᵢ i)
inst✝² : Fintype ι
R : Type u_2
inst✝¹ : OrderedRing R
inst✝ : (i : ι) → Module R (Mᵢ i)
Q : (i : ι) → QuadraticForm R (Mᵢ i)
h : ∀ (x : (i : ι) → Mᵢ i), ∑ i : ι, ↑(Q i) (x i) = 0 → ∀ (a : ι), x a = 0
i : ι
x : Mᵢ i
hx : ↑(Q i) x = 0
⊢ ∑ i_1 : ι, ↑(Q i_1) (Pi.single i x i_1) = 0
ι : Type u_1
R✝ : Type ?u.66145
M₁ : Type ?u.66148
M₂ : Type ?u.66151
N₁ : Type ?u.66154
N₂ : Type ?u.66157
Mᵢ : ι → Type u_3
Nᵢ : ι → Type ?u.66167
inst✝¹⁵ : Semiring R✝
inst✝¹⁴ : AddCommMonoid M₁
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : AddCommMonoid N₁
inst✝¹¹ : AddCommMonoid N₂
inst✝¹⁰ : Module R✝ M₁
inst✝⁹ : Module R✝ M₂
inst✝⁸ : Module R✝ N₁
inst✝⁷ : Module R✝ N₂
inst✝⁶ : (i : ι) → AddCommMonoid (Mᵢ i)
inst✝⁵ : (i : ι) → AddCommMonoid (Nᵢ i)
inst✝⁴ : (i : ι) → Module R✝ (Mᵢ i)
inst✝³ : (i : ι) → Module R✝ (Nᵢ i)
inst✝² : Fintype ι
R : Type u_2
inst✝¹ : OrderedRing R
inst✝ : (i : ι) → Module R (Mᵢ i)
Q : (i : ι) → QuadraticForm R (Mᵢ i)
h : ∀ (x : (i : ι) → Mᵢ i), ∑ i : ι, ↑(Q i) (x i) = 0 → ∀ (a : ι), x a = 0
i : ι
x : Mᵢ i
hx : ↑(Q i) x = 0
⊢ x = 0
have := h (Pi.single i x) ?_ i
case refine_1.h
ι : Type u_1
R✝ : Type ?u.66145
M₁ : Type ?u.66148
M₂ : Type ?u.66151
N₁ : Type ?u.66154
N₂ : Type ?u.66157
Mᵢ : ι → Type u_3
Nᵢ : ι → Type ?u.66167
inst✝¹⁵ : Semiring R✝
inst✝¹⁴ : AddCommMonoid M₁
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : AddCommMonoid N₁
inst✝¹¹ : AddCommMonoid N₂
inst✝¹⁰ : Module R✝ M₁
inst✝⁹ : Module R✝ M₂
inst✝⁸ : Module R✝ N₁
inst✝⁷ : Module R✝ N₂
inst✝⁶ : (i : ι) → AddCommMonoid (Mᵢ i)
inst✝⁵ : (i : ι) → AddCommMonoid (Nᵢ i)
inst✝⁴ : (i : ι) → Module R✝ (Mᵢ i)
inst✝³ : (i : ι) → Module R✝ (Nᵢ i)
inst✝² : Fintype ι
R : Type u_2
inst✝¹ : OrderedRing R
inst✝ : (i : ι) → Module R (Mᵢ i)
Q : (i : ι) → QuadraticForm R (Mᵢ i)
h : ∀ (x : (i : ι) → Mᵢ i), ∑ i : ι, ↑(Q i) (x i) = 0 → ∀ (a : ι), x a = 0
i : ι
x : Mᵢ i
hx : ↑(Q i) x = 0
⊢ ∀ (x_1 : ι), x_1 ∈ Finset.univ → ↑(Q x_1) (Pi.single i x x_1) = 0
case refine_1
ι : Type u_1
R✝ : Type ?u.66145
M₁ : Type ?u.66148
M₂ : Type ?u.66151
N₁ : Type ?u.66154
N₂ : Type ?u.66157
Mᵢ : ι → Type u_3
Nᵢ : ι → Type ?u.66167
inst✝¹⁵ : Semiring R✝
inst✝¹⁴ : AddCommMonoid M₁
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : AddCommMonoid N₁
inst✝¹¹ : AddCommMonoid N₂
inst✝¹⁰ : Module R✝ M₁
inst✝⁹ : Module R✝ M₂
inst✝⁸ : Module R✝ N₁
inst✝⁷ : Module R✝ N₂
inst✝⁶ : (i : ι) → AddCommMonoid (Mᵢ i)
inst✝⁵ : (i : ι) → AddCommMonoid (Nᵢ i)
inst✝⁴ : (i : ι) → Module R✝ (Mᵢ i)
inst✝³ : (i : ι) → Module R✝ (Nᵢ i)
inst✝² : Fintype ι
R : Type u_2
inst✝¹ : OrderedRing R
inst✝ : (i : ι) → Module R (Mᵢ i)
Q : (i : ι) → QuadraticForm R (Mᵢ i)
h : ∀ (x : (i : ι) → Mᵢ i), ∑ i : ι, ↑(Q i) (x i) = 0 → ∀ (a : ι), x a = 0
i : ι
x : Mᵢ i
hx : ↑(Q i) x = 0
⊢ ∑ i_1 : ι, ↑(Q i_1) (Pi.single i x i_1) = 0
apply Finset.sum_eq_zero
case refine_1.h
ι : Type u_1
R✝ : Type ?u.66145
M₁ : Type ?u.66148
M₂ : Type ?u.66151
N₁ : Type ?u.66154
N₂ : Type ?u.66157
Mᵢ : ι → Type u_3
Nᵢ : ι → Type ?u.66167
inst✝¹⁵ : Semiring R✝
inst✝¹⁴ : AddCommMonoid M₁
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : AddCommMonoid N₁
inst✝¹¹ : AddCommMonoid N₂
inst✝¹⁰ : Module R✝ M₁
inst✝⁹ : Module R✝ M₂
inst✝⁸ : Module R✝ N₁
inst✝⁷ : Module R✝ N₂
inst✝⁶ : (i : ι) → AddCommMonoid (Mᵢ i)
inst✝⁵ : (i : ι) → AddCommMonoid (Nᵢ i)
inst✝⁴ : (i : ι) → Module R✝ (Mᵢ i)
inst✝³ : (i : ι) → Module R✝ (Nᵢ i)
inst✝² : Fintype ι
R : Type u_2
inst✝¹ : OrderedRing R
inst✝ : (i : ι) → Module R (Mᵢ i)
Q : (i : ι) → QuadraticForm R (Mᵢ i)
h : ∀ (x : (i : ι) → Mᵢ i), ∑ i : ι, ↑(Q i) (x i) = 0 → ∀ (a : ι), x a = 0
i : ι
x : Mᵢ i
hx : ↑(Q i) x = 0
j : ι
a✝ : j ∈ Finset.univ
⊢ ↑(Q j) (Pi.single i x j) = 0
case refine_1.h
ι : Type u_1
R✝ : Type ?u.66145
M₁ : Type ?u.66148
M₂ : Type ?u.66151
N₁ : Type ?u.66154
N₂ : Type ?u.66157
Mᵢ : ι → Type u_3
Nᵢ : ι → Type ?u.66167
inst✝¹⁵ : Semiring R✝
inst✝¹⁴ : AddCommMonoid M₁
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : AddCommMonoid N₁
inst✝¹¹ : AddCommMonoid N₂
inst✝¹⁰ : Module R✝ M₁
inst✝⁹ : Module R✝ M₂
inst✝⁸ : Module R✝ N₁
inst✝⁷ : Module R✝ N₂
inst✝⁶ : (i : ι) → AddCommMonoid (Mᵢ i)
inst✝⁵ : (i : ι) → AddCommMonoid (Nᵢ i)
inst✝⁴ : (i : ι) → Module R✝ (Mᵢ i)
inst✝³ : (i : ι) → Module R✝ (Nᵢ i)
inst✝² : Fintype ι
R : Type u_2
inst✝¹ : OrderedRing R
inst✝ : (i : ι) → Module R (Mᵢ i)
Q : (i : ι) → QuadraticForm R (Mᵢ i)
h : ∀ (x : (i : ι) → Mᵢ i), ∑ i : ι, ↑(Q i) (x i) = 0 → ∀ (a : ι), x a = 0
i : ι
x : Mᵢ i
hx : ↑(Q i) x = 0
⊢ ∀ (x_1 : ι), x_1 ∈ Finset.univ → ↑(Q x_1) (Pi.single i x x_1) = 0
intro j _
case pos
ι : Type u_1
R✝ : Type ?u.66145
M₁ : Type ?u.66148
M₂ : Type ?u.66151
N₁ : Type ?u.66154
N₂ : Type ?u.66157
Mᵢ : ι → Type u_3
Nᵢ : ι → Type ?u.66167
inst✝¹⁵ : Semiring R✝
inst✝¹⁴ : AddCommMonoid M₁
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : AddCommMonoid N₁
inst✝¹¹ : AddCommMonoid N₂
inst✝¹⁰ : Module R✝ M₁
inst✝⁹ : Module R✝ M₂
inst✝⁸ : Module R✝ N₁
inst✝⁷ : Module R✝ N₂
inst✝⁶ : (i : ι) → AddCommMonoid (Mᵢ i)
inst✝⁵ : (i : ι) → AddCommMonoid (Nᵢ i)
inst✝⁴ : (i : ι) → Module R✝ (Mᵢ i)
inst✝³ : (i : ι) → Module R✝ (Nᵢ i)
inst✝² : Fintype ι
R : Type u_2
inst✝¹ : OrderedRing R
inst✝ : (i : ι) → Module R (Mᵢ i)
Q : (i : ι) → QuadraticForm R (Mᵢ i)
h : ∀ (x : (i : ι) → Mᵢ i), ∑ i : ι, ↑(Q i) (x i) = 0 → ∀ (a : ι), x a = 0
i : ι
x : Mᵢ i
hx : ↑(Q i) x = 0
j : ι
a✝ : j ∈ Finset.univ
hji : j = i
⊢ ↑(Q j) (Pi.single i x j) = 0

case neg
ι : Type u_1
R✝ : Type ?u.66145
M₁ : Type ?u.66148
M₂ : Type ?u.66151
N₁ : Type ?u.66154
N₂ : Type ?u.66157
Mᵢ : ι → Type u_3
Nᵢ : ι → Type ?u.66167
inst✝¹⁵ : Semiring R✝
inst✝¹⁴ : AddCommMonoid M₁
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : AddCommMonoid N₁
inst✝¹¹ : AddCommMonoid N₂
inst✝¹⁰ : Module R✝ M₁
inst✝⁹ : Module R✝ M₂
inst✝⁸ : Module R✝ N₁
inst✝⁷ : Module R✝ N₂
inst✝⁶ : (i : ι) → AddCommMonoid (Mᵢ i)
inst✝⁵ : (i : ι) → AddCommMonoid (Nᵢ i)
inst✝⁴ : (i : ι) → Module R✝ (Mᵢ i)
inst✝³ : (i : ι) → Module R✝ (Nᵢ i)
inst✝² : Fintype ι
R : Type u_2
inst✝¹ : OrderedRing R
inst✝ : (i : ι) → Module R (Mᵢ i)
Q : (i : ι) → QuadraticForm R (Mᵢ i)
h : ∀ (x : (i : ι) → Mᵢ i), ∑ i : ι, ↑(Q i) (x i) = 0 → ∀ (a : ι), x a = 0
i : ι
x : Mᵢ i
hx : ↑(Q i) x = 0
j : ι
a✝ : j ∈ Finset.univ
hji : ¬j = i
⊢ ↑(Q j) (Pi.single i x j) = 0
case refine_1.h
ι : Type u_1
R✝ : Type ?u.66145
M₁ : Type ?u.66148
M₂ : Type ?u.66151
N₁ : Type ?u.66154
N₂ : Type ?u.66157
Mᵢ : ι → Type u_3
Nᵢ : ι → Type ?u.66167
inst✝¹⁵ : Semiring R✝
inst✝¹⁴ : AddCommMonoid M₁
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : AddCommMonoid N₁
inst✝¹¹ : AddCommMonoid N₂
inst✝¹⁰ : Module R✝ M₁
inst✝⁹ : Module R✝ M₂
inst✝⁸ : Module R✝ N₁
inst✝⁷ : Module R✝ N₂
inst✝⁶ : (i : ι) → AddCommMonoid (Mᵢ i)
inst✝⁵ : (i : ι) → AddCommMonoid (Nᵢ i)
inst✝⁴ : (i : ι) → Module R✝ (Mᵢ i)
inst✝³ : (i : ι) → Module R✝ (Nᵢ i)
inst✝² : Fintype ι
R : Type u_2
inst✝¹ : OrderedRing R
inst✝ : (i : ι) → Module R (Mᵢ i)
Q : (i : ι) → QuadraticForm R (Mᵢ i)
h : ∀ (x : (i : ι) → Mᵢ i), ∑ i : ι, ↑(Q i) (x i) = 0 → ∀ (a : ι), x a = 0
i : ι
x : Mᵢ i
hx : ↑(Q i) x = 0
j : ι
a✝ : j ∈ Finset.univ
⊢ ↑(Q j) (Pi.single i x j) = 0
by_cases hji : j = i
case refine_2
ι : Type u_1
R✝ : Type ?u.66145
M₁ : Type ?u.66148
M₂ : Type ?u.66151
N₁ : Type ?u.66154
N₂ : Type ?u.66157
Mᵢ : ι → Type u_3
Nᵢ : ι → Type ?u.66167
inst✝¹⁵ : Semiring R✝
inst✝¹⁴ : AddCommMonoid M₁
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : AddCommMonoid N₁
inst✝¹¹ : AddCommMonoid N₂
inst✝¹⁰ : Module R✝ M₁
inst✝⁹ : Module R✝ M₂
inst✝⁸ : Module R✝ N₁
inst✝⁷ : Module R✝ N₂
inst✝⁶ : (i : ι) → AddCommMonoid (Mᵢ i)
inst✝⁵ : (i : ι) → AddCommMonoid (Nᵢ i)
inst✝⁴ : (i : ι) → Module R✝ (Mᵢ i)
inst✝³ : (i : ι) → Module R✝ (Nᵢ i)
inst✝² : Fintype ι
R : Type u_2
inst✝¹ : OrderedRing R
inst✝ : (i : ι) → Module R (Mᵢ i)
Q : (i : ι) → QuadraticForm R (Mᵢ i)
h : ∀ (x : (i : ι) → Mᵢ i), ∑ i : ι, ↑(Q i) (x i) = 0 → ∀ (a : ι), x a = 0
i : ι
x : Mᵢ i
hx : ↑(Q i) x = 0
this : x = 0
⊢ x = 0
case refine_2
ι : Type u_1
R✝ : Type ?u.66145
M₁ : Type ?u.66148
M₂ : Type ?u.66151
N₁ : Type ?u.66154
N₂ : Type ?u.66157
Mᵢ : ι → Type u_3
Nᵢ : ι → Type ?u.66167
inst✝¹⁵ : Semiring R✝
inst✝¹⁴ : AddCommMonoid M₁
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : AddCommMonoid N₁
inst✝¹¹ : AddCommMonoid N₂
inst✝¹⁰ : Module R✝ M₁
inst✝⁹ : Module R✝ M₂
inst✝⁸ : Module R✝ N₁
inst✝⁷ : Module R✝ N₂
inst✝⁶ : (i : ι) → AddCommMonoid (Mᵢ i)
inst✝⁵ : (i : ι) → AddCommMonoid (Nᵢ i)
inst✝⁴ : (i : ι) → Module R✝ (Mᵢ i)
inst✝³ : (i : ι) → Module R✝ (Nᵢ i)
inst✝² : Fintype ι
R : Type u_2
inst✝¹ : OrderedRing R
inst✝ : (i : ι) → Module R (Mᵢ i)
Q : (i : ι) → QuadraticForm R (Mᵢ i)
h : ∀ (x : (i : ι) → Mᵢ i), ∑ i : ι, ↑(Q i) (x i) = 0 → ∀ (a : ι), x a = 0
i : ι
x : Mᵢ i
hx : ↑(Q i) x = 0
this : Pi.single i x i = 0
⊢ x = 0
rw [Pi.single_eq_same] at this
no goals
case refine_2
ι : Type u_1
R✝ : Type ?u.66145
M₁ : Type ?u.66148
M₂ : Type ?u.66151
N₁ : Type ?u.66154
N₂ : Type ?u.66157
Mᵢ : ι → Type u_3
Nᵢ : ι → Type ?u.66167
inst✝¹⁵ : Semiring R✝
inst✝¹⁴ : AddCommMonoid M₁
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : AddCommMonoid N₁
inst✝¹¹ : AddCommMonoid N₂
inst✝¹⁰ : Module R✝ M₁
inst✝⁹ : Module R✝ M₂
inst✝⁸ : Module R✝ N₁
inst✝⁷ : Module R✝ N₂
inst✝⁶ : (i : ι) → AddCommMonoid (Mᵢ i)
inst✝⁵ : (i : ι) → AddCommMonoid (Nᵢ i)
inst✝⁴ : (i : ι) → Module R✝ (Mᵢ i)
inst✝³ : (i : ι) → Module R✝ (Nᵢ i)
inst✝² : Fintype ι
R : Type u_2
inst✝¹ : OrderedRing R
inst✝ : (i : ι) → Module R (Mᵢ i)
Q : (i : ι) → QuadraticForm R (Mᵢ i)
h : ∀ (x : (i : ι) → Mᵢ i), ∑ i : ι, ↑(Q i) (x i) = 0 → ∀ (a : ι), x a = 0
i : ι
x : Mᵢ i
hx : ↑(Q i) x = 0
this : x = 0
⊢ x = 0
exact this
case pos
ι : Type u_1
R✝ : Type ?u.66145
M₁ : Type ?u.66148
M₂ : Type ?u.66151
N₁ : Type ?u.66154
N₂ : Type ?u.66157
Mᵢ : ι → Type u_3
Nᵢ : ι → Type ?u.66167
inst✝¹⁵ : Semiring R✝
inst✝¹⁴ : AddCommMonoid M₁
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : AddCommMonoid N₁
inst✝¹¹ : AddCommMonoid N₂
inst✝¹⁰ : Module R✝ M₁
inst✝⁹ : Module R✝ M₂
inst✝⁸ : Module R✝ N₁
inst✝⁷ : Module R✝ N₂
inst✝⁶ : (i : ι) → AddCommMonoid (Mᵢ i)
inst✝⁵ : (i : ι) → AddCommMonoid (Nᵢ i)
inst✝⁴ : (i : ι) → Module R✝ (Mᵢ i)
inst✝³ : (i : ι) → Module R✝ (Nᵢ i)
inst✝² : Fintype ι
R : Type u_2
inst✝¹ : OrderedRing R
inst✝ : (i : ι) → Module R (Mᵢ i)
Q : (i : ι) → QuadraticForm R (Mᵢ i)
h : ∀ (x : (i : ι) → Mᵢ i), ∑ i : ι, ↑(Q i) (x i) = 0 → ∀ (a : ι), x a = 0
j : ι
a✝ : j ∈ Finset.univ
x : Mᵢ j
hx : ↑(Q j) x = 0
⊢ ↑(Q j) (Pi.single j x j) = 0
case pos
ι : Type u_1
R✝ : Type ?u.66145
M₁ : Type ?u.66148
M₂ : Type ?u.66151
N₁ : Type ?u.66154
N₂ : Type ?u.66157
Mᵢ : ι → Type u_3
Nᵢ : ι → Type ?u.66167
inst✝¹⁵ : Semiring R✝
inst✝¹⁴ : AddCommMonoid M₁
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : AddCommMonoid N₁
inst✝¹¹ : AddCommMonoid N₂
inst✝¹⁰ : Module R✝ M₁
inst✝⁹ : Module R✝ M₂
inst✝⁸ : Module R✝ N₁
inst✝⁷ : Module R✝ N₂
inst✝⁶ : (i : ι) → AddCommMonoid (Mᵢ i)
inst✝⁵ : (i : ι) → AddCommMonoid (Nᵢ i)
inst✝⁴ : (i : ι) → Module R✝ (Mᵢ i)
inst✝³ : (i : ι) → Module R✝ (Nᵢ i)
inst✝² : Fintype ι
R : Type u_2
inst✝¹ : OrderedRing R
inst✝ : (i : ι) → Module R (Mᵢ i)
Q : (i : ι) → QuadraticForm R (Mᵢ i)
h : ∀ (x : (i : ι) → Mᵢ i), ∑ i : ι, ↑(Q i) (x i) = 0 → ∀ (a : ι), x a = 0
i : ι
x : Mᵢ i
hx : ↑(Q i) x = 0
j : ι
a✝ : j ∈ Finset.univ
hji : j = i
⊢ ↑(Q j) (Pi.single i x j) = 0
subst hji
no goals
case pos
ι : Type u_1
R✝ : Type ?u.66145
M₁ : Type ?u.66148
M₂ : Type ?u.66151
N₁ : Type ?u.66154
N₂ : Type ?u.66157
Mᵢ : ι → Type u_3
Nᵢ : ι → Type ?u.66167
inst✝¹⁵ : Semiring R✝
inst✝¹⁴ : AddCommMonoid M₁
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : AddCommMonoid N₁
inst✝¹¹ : AddCommMonoid N₂
inst✝¹⁰ : Module R✝ M₁
inst✝⁹ : Module R✝ M₂
inst✝⁸ : Module R✝ N₁
inst✝⁷ : Module R✝ N₂
inst✝⁶ : (i : ι) → AddCommMonoid (Mᵢ i)
inst✝⁵ : (i : ι) → AddCommMonoid (Nᵢ i)
inst✝⁴ : (i : ι) → Module R✝ (Mᵢ i)
inst✝³ : (i : ι) → Module R✝ (Nᵢ i)
inst✝² : Fintype ι
R : Type u_2
inst✝¹ : OrderedRing R
inst✝ : (i : ι) → Module R (Mᵢ i)
Q : (i : ι) → QuadraticForm R (Mᵢ i)
h : ∀ (x : (i : ι) → Mᵢ i), ∑ i : ι, ↑(Q i) (x i) = 0 → ∀ (a : ι), x a = 0
j : ι
a✝ : j ∈ Finset.univ
x : Mᵢ j
hx : ↑(Q j) x = 0
⊢ ↑(Q j) (Pi.single j x j) = 0
rw [Pi.single_eq_same, hx]
no goals
case neg
ι : Type u_1
R✝ : Type ?u.66145
M₁ : Type ?u.66148
M₂ : Type ?u.66151
N₁ : Type ?u.66154
N₂ : Type ?u.66157
Mᵢ : ι → Type u_3
Nᵢ : ι → Type ?u.66167
inst✝¹⁵ : Semiring R✝
inst✝¹⁴ : AddCommMonoid M₁
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : AddCommMonoid N₁
inst✝¹¹ : AddCommMonoid N₂
inst✝¹⁰ : Module R✝ M₁
inst✝⁹ : Module R✝ M₂
inst✝⁸ : Module R✝ N₁
inst✝⁷ : Module R✝ N₂
inst✝⁶ : (i : ι) → AddCommMonoid (Mᵢ i)
inst✝⁵ : (i : ι) → AddCommMonoid (Nᵢ i)
inst✝⁴ : (i : ι) → Module R✝ (Mᵢ i)
inst✝³ : (i : ι) → Module R✝ (Nᵢ i)
inst✝² : Fintype ι
R : Type u_2
inst✝¹ : OrderedRing R
inst✝ : (i : ι) → Module R (Mᵢ i)
Q : (i : ι) → QuadraticForm R (Mᵢ i)
h : ∀ (x : (i : ι) → Mᵢ i), ∑ i : ι, ↑(Q i) (x i) = 0 → ∀ (a : ι), x a = 0
i : ι
x : Mᵢ i
hx : ↑(Q i) x = 0
j : ι
a✝ : j ∈ Finset.univ
hji : ¬j = i
⊢ ↑(Q j) (Pi.single i x j) = 0
rw [Pi.single_eq_of_ne hji, map_zero]