ι : Type ?u.47407
R✝ : Type ?u.47410
M₁ : Type u_2
M₂ : Type u_3
N₁ : Type ?u.47419
N₂ : Type ?u.47422
Mᵢ : ι → Type ?u.47427
Nᵢ : ι → Type ?u.47432
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)
R : Type u_1
inst✝² : OrderedRing R
inst✝¹ : Module R M₁
inst✝ : Module R M₂
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
⊢ ((∀ (x : M₁), 0 ≤ ↑Q₁ x) ∧ ∀ (x : M₂), 0 ≤ ↑Q₂ x) ∧ Anisotropic (prod Q₁ Q₂) ↔
    ((∀ (x : M₁), 0 ≤ ↑Q₁ x) ∧ Anisotropic Q₁) ∧ (∀ (x : M₂), 0 ≤ ↑Q₂ x) ∧ Anisotropic Q₂
ι : Type ?u.47407
R✝ : Type ?u.47410
M₁ : Type u_2
M₂ : Type u_3
N₁ : Type ?u.47419
N₂ : Type ?u.47422
Mᵢ : ι → Type ?u.47427
Nᵢ : ι → Type ?u.47432
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)
R : Type u_1
inst✝² : OrderedRing R
inst✝¹ : Module R M₁
inst✝ : Module R M₂
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
⊢ PosDef (prod Q₁ Q₂) ↔ PosDef Q₁ ∧ PosDef Q₂
simp_rw [posDef_iff_nonneg, nonneg_prod_iff]
case mp
ι : Type ?u.47407
R✝ : Type ?u.47410
M₁ : Type u_2
M₂ : Type u_3
N₁ : Type ?u.47419
N₂ : Type ?u.47422
Mᵢ : ι → Type ?u.47427
Nᵢ : ι → Type ?u.47432
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)
R : Type u_1
inst✝² : OrderedRing R
inst✝¹ : Module R M₁
inst✝ : Module R M₂
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
⊢ ((∀ (x : M₁), 0 ≤ ↑Q₁ x) ∧ ∀ (x : M₂), 0 ≤ ↑Q₂ x) ∧ Anisotropic (prod Q₁ Q₂) →
    ((∀ (x : M₁), 0 ≤ ↑Q₁ x) ∧ Anisotropic Q₁) ∧ (∀ (x : M₂), 0 ≤ ↑Q₂ x) ∧ Anisotropic Q₂

case mpr
ι : Type ?u.47407
R✝ : Type ?u.47410
M₁ : Type u_2
M₂ : Type u_3
N₁ : Type ?u.47419
N₂ : Type ?u.47422
Mᵢ : ι → Type ?u.47427
Nᵢ : ι → Type ?u.47432
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)
R : Type u_1
inst✝² : OrderedRing R
inst✝¹ : Module R M₁
inst✝ : Module R M₂
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
⊢ ((∀ (x : M₁), 0 ≤ ↑Q₁ x) ∧ Anisotropic Q₁) ∧ (∀ (x : M₂), 0 ≤ ↑Q₂ x) ∧ Anisotropic Q₂ →
    ((∀ (x : M₁), 0 ≤ ↑Q₁ x) ∧ ∀ (x : M₂), 0 ≤ ↑Q₂ x) ∧ Anisotropic (prod Q₁ Q₂)
ι : Type ?u.47407
R✝ : Type ?u.47410
M₁ : Type u_2
M₂ : Type u_3
N₁ : Type ?u.47419
N₂ : Type ?u.47422
Mᵢ : ι → Type ?u.47427
Nᵢ : ι → Type ?u.47432
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)
R : Type u_1
inst✝² : OrderedRing R
inst✝¹ : Module R M₁
inst✝ : Module R M₂
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
⊢ ((∀ (x : M₁), 0 ≤ ↑Q₁ x) ∧ ∀ (x : M₂), 0 ≤ ↑Q₂ x) ∧ Anisotropic (prod Q₁ Q₂) ↔
    ((∀ (x : M₁), 0 ≤ ↑Q₁ x) ∧ Anisotropic Q₁) ∧ (∀ (x : M₂), 0 ≤ ↑Q₂ x) ∧ Anisotropic Q₂
constructor
case mp.intro.intro
ι : Type ?u.47407
R✝ : Type ?u.47410
M₁ : Type u_2
M₂ : Type u_3
N₁ : Type ?u.47419
N₂ : Type ?u.47422
Mᵢ : ι → Type ?u.47427
Nᵢ : ι → Type ?u.47432
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)
R : Type u_1
inst✝² : OrderedRing R
inst✝¹ : Module R M₁
inst✝ : Module R M₂
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
ha : Anisotropic (prod Q₁ Q₂)
hle₁ : ∀ (x : M₁), 0 ≤ ↑Q₁ x
hle₂ : ∀ (x : M₂), 0 ≤ ↑Q₂ x
⊢ ((∀ (x : M₁), 0 ≤ ↑Q₁ x) ∧ Anisotropic Q₁) ∧ (∀ (x : M₂), 0 ≤ ↑Q₂ x) ∧ Anisotropic Q₂
case mp
ι : Type ?u.47407
R✝ : Type ?u.47410
M₁ : Type u_2
M₂ : Type u_3
N₁ : Type ?u.47419
N₂ : Type ?u.47422
Mᵢ : ι → Type ?u.47427
Nᵢ : ι → Type ?u.47432
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)
R : Type u_1
inst✝² : OrderedRing R
inst✝¹ : Module R M₁
inst✝ : Module R M₂
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
⊢ ((∀ (x : M₁), 0 ≤ ↑Q₁ x) ∧ ∀ (x : M₂), 0 ≤ ↑Q₂ x) ∧ Anisotropic (prod Q₁ Q₂) →
    ((∀ (x : M₁), 0 ≤ ↑Q₁ x) ∧ Anisotropic Q₁) ∧ (∀ (x : M₂), 0 ≤ ↑Q₂ x) ∧ Anisotropic Q₂
rintro ⟨⟨hle₁, hle₂⟩, ha⟩
case mp.intro.intro.intro
ι : Type ?u.47407
R✝ : Type ?u.47410
M₁ : Type u_2
M₂ : Type u_3
N₁ : Type ?u.47419
N₂ : Type ?u.47422
Mᵢ : ι → Type ?u.47427
Nᵢ : ι → Type ?u.47432
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)
R : Type u_1
inst✝² : OrderedRing R
inst✝¹ : Module R M₁
inst✝ : Module R M₂
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
ha : Anisotropic (prod Q₁ Q₂)
hle₁ : ∀ (x : M₁), 0 ≤ ↑Q₁ x
hle₂ : ∀ (x : M₂), 0 ≤ ↑Q₂ x
ha₁ : Anisotropic Q₁
ha₂ : Anisotropic Q₂
⊢ ((∀ (x : M₁), 0 ≤ ↑Q₁ x) ∧ Anisotropic Q₁) ∧ (∀ (x : M₂), 0 ≤ ↑Q₂ x) ∧ Anisotropic Q₂
case mp.intro.intro
ι : Type ?u.47407
R✝ : Type ?u.47410
M₁ : Type u_2
M₂ : Type u_3
N₁ : Type ?u.47419
N₂ : Type ?u.47422
Mᵢ : ι → Type ?u.47427
Nᵢ : ι → Type ?u.47432
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)
R : Type u_1
inst✝² : OrderedRing R
inst✝¹ : Module R M₁
inst✝ : Module R M₂
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
ha : Anisotropic (prod Q₁ Q₂)
hle₁ : ∀ (x : M₁), 0 ≤ ↑Q₁ x
hle₂ : ∀ (x : M₂), 0 ≤ ↑Q₂ x
⊢ ((∀ (x : M₁), 0 ≤ ↑Q₁ x) ∧ Anisotropic Q₁) ∧ (∀ (x : M₂), 0 ≤ ↑Q₂ x) ∧ Anisotropic Q₂
obtain ⟨ha₁, ha₂⟩ := anisotropic_of_prod ha
no goals
case mp.intro.intro.intro
ι : Type ?u.47407
R✝ : Type ?u.47410
M₁ : Type u_2
M₂ : Type u_3
N₁ : Type ?u.47419
N₂ : Type ?u.47422
Mᵢ : ι → Type ?u.47427
Nᵢ : ι → Type ?u.47432
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)
R : Type u_1
inst✝² : OrderedRing R
inst✝¹ : Module R M₁
inst✝ : Module R M₂
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
ha : Anisotropic (prod Q₁ Q₂)
hle₁ : ∀ (x : M₁), 0 ≤ ↑Q₁ x
hle₂ : ∀ (x : M₂), 0 ≤ ↑Q₂ x
ha₁ : Anisotropic Q₁
ha₂ : Anisotropic Q₂
⊢ ((∀ (x : M₁), 0 ≤ ↑Q₁ x) ∧ Anisotropic Q₁) ∧ (∀ (x : M₂), 0 ≤ ↑Q₂ x) ∧ Anisotropic Q₂
refine' ⟨⟨hle₁, ha₁⟩, ⟨hle₂, ha₂⟩⟩
case mpr.intro.intro.intro
ι : Type ?u.47407
R✝ : Type ?u.47410
M₁ : Type u_2
M₂ : Type u_3
N₁ : Type ?u.47419
N₂ : Type ?u.47422
Mᵢ : ι → Type ?u.47427
Nᵢ : ι → Type ?u.47432
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)
R : Type u_1
inst✝² : OrderedRing R
inst✝¹ : Module R M₁
inst✝ : Module R M₂
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
hle₁ : ∀ (x : M₁), 0 ≤ ↑Q₁ x
ha₁ : Anisotropic Q₁
hle₂ : ∀ (x : M₂), 0 ≤ ↑Q₂ x
ha₂ : Anisotropic Q₂
⊢ ((∀ (x : M₁), 0 ≤ ↑Q₁ x) ∧ ∀ (x : M₂), 0 ≤ ↑Q₂ x) ∧ Anisotropic (prod Q₁ Q₂)
case mpr
ι : Type ?u.47407
R✝ : Type ?u.47410
M₁ : Type u_2
M₂ : Type u_3
N₁ : Type ?u.47419
N₂ : Type ?u.47422
Mᵢ : ι → Type ?u.47427
Nᵢ : ι → Type ?u.47432
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)
R : Type u_1
inst✝² : OrderedRing R
inst✝¹ : Module R M₁
inst✝ : Module R M₂
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
⊢ ((∀ (x : M₁), 0 ≤ ↑Q₁ x) ∧ Anisotropic Q₁) ∧ (∀ (x : M₂), 0 ≤ ↑Q₂ x) ∧ Anisotropic Q₂ →
    ((∀ (x : M₁), 0 ≤ ↑Q₁ x) ∧ ∀ (x : M₂), 0 ≤ ↑Q₂ x) ∧ Anisotropic (prod Q₁ Q₂)
rintro ⟨⟨hle₁, ha₁⟩, ⟨hle₂, ha₂⟩⟩
case mpr.intro.intro.intro
ι : Type ?u.47407
R✝ : Type ?u.47410
M₁ : Type u_2
M₂ : Type u_3
N₁ : Type ?u.47419
N₂ : Type ?u.47422
Mᵢ : ι → Type ?u.47427
Nᵢ : ι → Type ?u.47432
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)
R : Type u_1
inst✝² : OrderedRing R
inst✝¹ : Module R M₁
inst✝ : Module R M₂
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
hle₁ : ∀ (x : M₁), 0 ≤ ↑Q₁ x
ha₁ : Anisotropic Q₁
hle₂ : ∀ (x : M₂), 0 ≤ ↑Q₂ x
ha₂ : Anisotropic Q₂
⊢ Anisotropic (prod Q₁ Q₂)
case mpr.intro.intro.intro
ι : Type ?u.47407
R✝ : Type ?u.47410
M₁ : Type u_2
M₂ : Type u_3
N₁ : Type ?u.47419
N₂ : Type ?u.47422
Mᵢ : ι → Type ?u.47427
Nᵢ : ι → Type ?u.47432
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)
R : Type u_1
inst✝² : OrderedRing R
inst✝¹ : Module R M₁
inst✝ : Module R M₂
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
hle₁ : ∀ (x : M₁), 0 ≤ ↑Q₁ x
ha₁ : Anisotropic Q₁
hle₂ : ∀ (x : M₂), 0 ≤ ↑Q₂ x
ha₂ : Anisotropic Q₂
⊢ ((∀ (x : M₁), 0 ≤ ↑Q₁ x) ∧ ∀ (x : M₂), 0 ≤ ↑Q₂ x) ∧ Anisotropic (prod Q₁ Q₂)
refine' ⟨⟨hle₁, hle₂⟩, _⟩
case mpr.intro.intro.intro.mk
ι : Type ?u.47407
R✝ : Type ?u.47410
M₁ : Type u_2
M₂ : Type u_3
N₁ : Type ?u.47419
N₂ : Type ?u.47422
Mᵢ : ι → Type ?u.47427
Nᵢ : ι → Type ?u.47432
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)
R : Type u_1
inst✝² : OrderedRing R
inst✝¹ : Module R M₁
inst✝ : Module R M₂
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
hle₁ : ∀ (x : M₁), 0 ≤ ↑Q₁ x
ha₁ : Anisotropic Q₁
hle₂ : ∀ (x : M₂), 0 ≤ ↑Q₂ x
ha₂ : Anisotropic Q₂
x₁ : M₁
x₂ : M₂
hx : ↑Q₁ x₁ + ↑Q₂ x₂ = 0
⊢ (x₁, x₂) = 0
case mpr.intro.intro.intro
ι : Type ?u.47407
R✝ : Type ?u.47410
M₁ : Type u_2
M₂ : Type u_3
N₁ : Type ?u.47419
N₂ : Type ?u.47422
Mᵢ : ι → Type ?u.47427
Nᵢ : ι → Type ?u.47432
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)
R : Type u_1
inst✝² : OrderedRing R
inst✝¹ : Module R M₁
inst✝ : Module R M₂
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
hle₁ : ∀ (x : M₁), 0 ≤ ↑Q₁ x
ha₁ : Anisotropic Q₁
hle₂ : ∀ (x : M₂), 0 ≤ ↑Q₂ x
ha₂ : Anisotropic Q₂
⊢ Anisotropic (prod Q₁ Q₂)
rintro ⟨x₁, x₂⟩ (hx : Q₁ x₁ + Q₂ x₂ = 0)
case mpr.intro.intro.intro.mk
ι : Type ?u.47407
R✝ : Type ?u.47410
M₁ : Type u_2
M₂ : Type u_3
N₁ : Type ?u.47419
N₂ : Type ?u.47422
Mᵢ : ι → Type ?u.47427
Nᵢ : ι → Type ?u.47432
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)
R : Type u_1
inst✝² : OrderedRing R
inst✝¹ : Module R M₁
inst✝ : Module R M₂
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
hle₁ : ∀ (x : M₁), 0 ≤ ↑Q₁ x
ha₁ : Anisotropic Q₁
hle₂ : ∀ (x : M₂), 0 ≤ ↑Q₂ x
ha₂ : Anisotropic Q₂
x₁ : M₁
x₂ : M₂
hx : x₁ = 0 ∧ x₂ = 0
⊢ (x₁, x₂) = 0
case mpr.intro.intro.intro.mk
ι : Type ?u.47407
R✝ : Type ?u.47410
M₁ : Type u_2
M₂ : Type u_3
N₁ : Type ?u.47419
N₂ : Type ?u.47422
Mᵢ : ι → Type ?u.47427
Nᵢ : ι → Type ?u.47432
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)
R : Type u_1
inst✝² : OrderedRing R
inst✝¹ : Module R M₁
inst✝ : Module R M₂
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
hle₁ : ∀ (x : M₁), 0 ≤ ↑Q₁ x
ha₁ : Anisotropic Q₁
hle₂ : ∀ (x : M₂), 0 ≤ ↑Q₂ x
ha₂ : Anisotropic Q₂
x₁ : M₁
x₂ : M₂
hx : ↑Q₁ x₁ + ↑Q₂ x₂ = 0
⊢ (x₁, x₂) = 0
rw [add_eq_zero_iff' (hle₁ x₁) (hle₂ x₂), ha₁.eq_zero_iff, ha₂.eq_zero_iff] at hx
no goals
case mpr.intro.intro.intro.mk
ι : Type ?u.47407
R✝ : Type ?u.47410
M₁ : Type u_2
M₂ : Type u_3
N₁ : Type ?u.47419
N₂ : Type ?u.47422
Mᵢ : ι → Type ?u.47427
Nᵢ : ι → Type ?u.47432
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)
R : Type u_1
inst✝² : OrderedRing R
inst✝¹ : Module R M₁
inst✝ : Module R M₂
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
hle₁ : ∀ (x : M₁), 0 ≤ ↑Q₁ x
ha₁ : Anisotropic Q₁
hle₂ : ∀ (x : M₂), 0 ≤ ↑Q₂ x
ha₂ : Anisotropic Q₂
x₁ : M₁
x₂ : M₂
hx : x₁ = 0 ∧ x₂ = 0
⊢ (x₁, x₂) = 0
rwa [Prod.mk_eq_zero]