ι : Type u_1
R✝ : Type ?u.83936
M₁ : Type ?u.83939
M₂ : Type ?u.83942
N₁ : Type ?u.83945
N₂ : Type ?u.83948
Mᵢ : ι → Type u_3
Nᵢ : ι → Type ?u.83958
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)
⊢ (∀ (i : ι) (x : Mᵢ i), 0 ≤ ↑(Q i) x) ∧ Anisotropic (pi Q) ↔
    ∀ (i : ι), (∀ (x : Mᵢ i), 0 ≤ ↑(Q i) x) ∧ Anisotropic (Q i)
ι : Type u_1
R✝ : Type ?u.83936
M₁ : Type ?u.83939
M₂ : Type ?u.83942
N₁ : Type ?u.83945
N₂ : Type ?u.83948
Mᵢ : ι → Type u_3
Nᵢ : ι → Type ?u.83958
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)
⊢ PosDef (pi Q) ↔ ∀ (i : ι), PosDef (Q i)
simp_rw [posDef_iff_nonneg, nonneg_pi_iff]
case mp
ι : Type u_1
R✝ : Type ?u.83936
M₁ : Type ?u.83939
M₂ : Type ?u.83942
N₁ : Type ?u.83945
N₂ : Type ?u.83948
Mᵢ : ι → Type u_3
Nᵢ : ι → Type ?u.83958
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)
⊢ (∀ (i : ι) (x : Mᵢ i), 0 ≤ ↑(Q i) x) ∧ Anisotropic (pi Q) →
    ∀ (i : ι), (∀ (x : Mᵢ i), 0 ≤ ↑(Q i) x) ∧ Anisotropic (Q i)

case mpr
ι : Type u_1
R✝ : Type ?u.83936
M₁ : Type ?u.83939
M₂ : Type ?u.83942
N₁ : Type ?u.83945
N₂ : Type ?u.83948
Mᵢ : ι → Type u_3
Nᵢ : ι → Type ?u.83958
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)
⊢ (∀ (i : ι), (∀ (x : Mᵢ i), 0 ≤ ↑(Q i) x) ∧ Anisotropic (Q i)) →
    (∀ (i : ι) (x : Mᵢ i), 0 ≤ ↑(Q i) x) ∧ Anisotropic (pi Q)
ι : Type u_1
R✝ : Type ?u.83936
M₁ : Type ?u.83939
M₂ : Type ?u.83942
N₁ : Type ?u.83945
N₂ : Type ?u.83948
Mᵢ : ι → Type u_3
Nᵢ : ι → Type ?u.83958
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)
⊢ (∀ (i : ι) (x : Mᵢ i), 0 ≤ ↑(Q i) x) ∧ Anisotropic (pi Q) ↔
    ∀ (i : ι), (∀ (x : Mᵢ i), 0 ≤ ↑(Q i) x) ∧ Anisotropic (Q i)
constructor
case mp.intro
ι : Type u_1
R✝ : Type ?u.83936
M₁ : Type ?u.83939
M₂ : Type ?u.83942
N₁ : Type ?u.83945
N₂ : Type ?u.83948
Mᵢ : ι → Type u_3
Nᵢ : ι → Type ?u.83958
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)
hle : ∀ (i : ι) (x : Mᵢ i), 0 ≤ ↑(Q i) x
ha : Anisotropic (pi Q)
⊢ ∀ (i : ι), (∀ (x : Mᵢ i), 0 ≤ ↑(Q i) x) ∧ Anisotropic (Q i)
case mp
ι : Type u_1
R✝ : Type ?u.83936
M₁ : Type ?u.83939
M₂ : Type ?u.83942
N₁ : Type ?u.83945
N₂ : Type ?u.83948
Mᵢ : ι → Type u_3
Nᵢ : ι → Type ?u.83958
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)
⊢ (∀ (i : ι) (x : Mᵢ i), 0 ≤ ↑(Q i) x) ∧ Anisotropic (pi Q) →
    ∀ (i : ι), (∀ (x : Mᵢ i), 0 ≤ ↑(Q i) x) ∧ Anisotropic (Q i)
rintro ⟨hle, ha⟩
case mp.intro
ι : Type u_1
R✝ : Type ?u.83936
M₁ : Type ?u.83939
M₂ : Type ?u.83942
N₁ : Type ?u.83945
N₂ : Type ?u.83948
Mᵢ : ι → Type u_3
Nᵢ : ι → Type ?u.83958
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)
hle : ∀ (i : ι) (x : Mᵢ i), 0 ≤ ↑(Q i) x
ha : Anisotropic (pi Q)
i : ι
⊢ (∀ (x : Mᵢ i), 0 ≤ ↑(Q i) x) ∧ Anisotropic (Q i)
case mp.intro
ι : Type u_1
R✝ : Type ?u.83936
M₁ : Type ?u.83939
M₂ : Type ?u.83942
N₁ : Type ?u.83945
N₂ : Type ?u.83948
Mᵢ : ι → Type u_3
Nᵢ : ι → Type ?u.83958
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)
hle : ∀ (i : ι) (x : Mᵢ i), 0 ≤ ↑(Q i) x
ha : Anisotropic (pi Q)
⊢ ∀ (i : ι), (∀ (x : Mᵢ i), 0 ≤ ↑(Q i) x) ∧ Anisotropic (Q i)
intro i
no goals
case mp.intro
ι : Type u_1
R✝ : Type ?u.83936
M₁ : Type ?u.83939
M₂ : Type ?u.83942
N₁ : Type ?u.83945
N₂ : Type ?u.83948
Mᵢ : ι → Type u_3
Nᵢ : ι → Type ?u.83958
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)
hle : ∀ (i : ι) (x : Mᵢ i), 0 ≤ ↑(Q i) x
ha : Anisotropic (pi Q)
i : ι
⊢ (∀ (x : Mᵢ i), 0 ≤ ↑(Q i) x) ∧ Anisotropic (Q i)
exact ⟨hle i, anisotropic_of_pi ha i⟩
case mpr
ι : Type u_1
R✝ : Type ?u.83936
M₁ : Type ?u.83939
M₂ : Type ?u.83942
N₁ : Type ?u.83945
N₂ : Type ?u.83948
Mᵢ : ι → Type u_3
Nᵢ : ι → Type ?u.83958
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 : ∀ (i : ι), (∀ (x : Mᵢ i), 0 ≤ ↑(Q i) x) ∧ Anisotropic (Q i)
⊢ (∀ (i : ι) (x : Mᵢ i), 0 ≤ ↑(Q i) x) ∧ Anisotropic (pi Q)
case mpr
ι : Type u_1
R✝ : Type ?u.83936
M₁ : Type ?u.83939
M₂ : Type ?u.83942
N₁ : Type ?u.83945
N₂ : Type ?u.83948
Mᵢ : ι → Type u_3
Nᵢ : ι → Type ?u.83958
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)
⊢ (∀ (i : ι), (∀ (x : Mᵢ i), 0 ≤ ↑(Q i) x) ∧ Anisotropic (Q i)) →
    (∀ (i : ι) (x : Mᵢ i), 0 ≤ ↑(Q i) x) ∧ Anisotropic (pi Q)
intro h
case mpr
ι : Type u_1
R✝ : Type ?u.83936
M₁ : Type ?u.83939
M₂ : Type ?u.83942
N₁ : Type ?u.83945
N₂ : Type ?u.83948
Mᵢ : ι → Type u_3
Nᵢ : ι → Type ?u.83958
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 : ∀ (i : ι), (∀ (x : Mᵢ i), 0 ≤ ↑(Q i) x) ∧ Anisotropic (Q i)
x : (i : ι) → Mᵢ i
hx : ↑(pi Q) x = 0
i : ι
⊢ ↑(Q i) (x i) = 0
case mpr
ι : Type u_1
R✝ : Type ?u.83936
M₁ : Type ?u.83939
M₂ : Type ?u.83942
N₁ : Type ?u.83945
N₂ : Type ?u.83948
Mᵢ : ι → Type u_3
Nᵢ : ι → Type ?u.83958
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 : ∀ (i : ι), (∀ (x : Mᵢ i), 0 ≤ ↑(Q i) x) ∧ Anisotropic (Q i)
⊢ (∀ (i : ι) (x : Mᵢ i), 0 ≤ ↑(Q i) x) ∧ Anisotropic (pi Q)
refine' ⟨fun i => (h i).1, fun x hx => funext fun i => (h i).2 _ _⟩
case mpr
ι : Type u_1
R✝ : Type ?u.83936
M₁ : Type ?u.83939
M₂ : Type ?u.83942
N₁ : Type ?u.83945
N₂ : Type ?u.83948
Mᵢ : ι → Type u_3
Nᵢ : ι → Type ?u.83958
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 : ∀ (i : ι), (∀ (x : Mᵢ i), 0 ≤ ↑(Q i) x) ∧ Anisotropic (Q i)
x : (i : ι) → Mᵢ i
hx : ∀ (i : ι), i ∈ Finset.univ → ↑(Q i) (x i) = 0
i : ι
⊢ ↑(Q i) (x i) = 0

ι : Type u_1
R✝ : Type ?u.83936
M₁ : Type ?u.83939
M₂ : Type ?u.83942
N₁ : Type ?u.83945
N₂ : Type ?u.83948
Mᵢ : ι → Type u_3
Nᵢ : ι → Type ?u.83958
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 : ∀ (i : ι), (∀ (x : Mᵢ i), 0 ≤ ↑(Q i) x) ∧ Anisotropic (Q i)
x : (i : ι) → Mᵢ i
hx : ∑ i : ι, ↑(Q i) (x i) = 0
i j : ι
x✝ : j ∈ Finset.univ
⊢ 0 ≤ ↑(Q j) (x j)
case mpr
ι : Type u_1
R✝ : Type ?u.83936
M₁ : Type ?u.83939
M₂ : Type ?u.83942
N₁ : Type ?u.83945
N₂ : Type ?u.83948
Mᵢ : ι → Type u_3
Nᵢ : ι → Type ?u.83958
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 : ∀ (i : ι), (∀ (x : Mᵢ i), 0 ≤ ↑(Q i) x) ∧ Anisotropic (Q i)
x : (i : ι) → Mᵢ i
hx : ↑(pi Q) x = 0
i : ι
⊢ ↑(Q i) (x i) = 0
rw [pi_apply, Finset.sum_eq_zero_iff_of_nonneg fun j _ => ?_] at hx
no goals
ι : Type u_1
R✝ : Type ?u.83936
M₁ : Type ?u.83939
M₂ : Type ?u.83942
N₁ : Type ?u.83945
N₂ : Type ?u.83948
Mᵢ : ι → Type u_3
Nᵢ : ι → Type ?u.83958
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 : ∀ (i : ι), (∀ (x : Mᵢ i), 0 ≤ ↑(Q i) x) ∧ Anisotropic (Q i)
x : (i : ι) → Mᵢ i
hx : ∑ i : ι, ↑(Q i) (x i) = 0
i j : ι
x✝ : j ∈ Finset.univ
⊢ 0 ≤ ↑(Q j) (x j)
exact (h j).1 _
no goals
case mpr
ι : Type u_1
R✝ : Type ?u.83936
M₁ : Type ?u.83939
M₂ : Type ?u.83942
N₁ : Type ?u.83945
N₂ : Type ?u.83948
Mᵢ : ι → Type u_3
Nᵢ : ι → Type ?u.83958
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 : ∀ (i : ι), (∀ (x : Mᵢ i), 0 ≤ ↑(Q i) x) ∧ Anisotropic (Q i)
x : (i : ι) → Mᵢ i
hx : ∀ (i : ι), i ∈ Finset.univ → ↑(Q i) (x i) = 0
i : ι
⊢ ↑(Q i) (x i) = 0
exact hx _ (Finset.mem_univ _)