ι : Type ?u.43590
R✝ : Type ?u.43593
M₁ : Type u_2
M₂ : Type u_3
N₁ : Type ?u.43602
N₂ : Type ?u.43605
Mᵢ : ι → Type ?u.43610
Nᵢ : ι → Type ?u.43615
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₂
⊢ (∀ (a : M₁) (b : M₂), 0 ≤ ↑Q₁ a + ↑Q₂ b) ↔ (∀ (x : M₁), 0 ≤ ↑Q₁ x) ∧ ∀ (x : M₂), 0 ≤ ↑Q₂ x
ι : Type ?u.43590
R✝ : Type ?u.43593
M₁ : Type u_2
M₂ : Type u_3
N₁ : Type ?u.43602
N₂ : Type ?u.43605
Mᵢ : ι → Type ?u.43610
Nᵢ : ι → Type ?u.43615
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₁ × M₂), 0 ≤ ↑(prod Q₁ Q₂) x) ↔ (∀ (x : M₁), 0 ≤ ↑Q₁ x) ∧ ∀ (x : M₂), 0 ≤ ↑Q₂ x
simp_rw [Prod.forall, prod_apply]
case mp
ι : Type ?u.43590
R✝ : Type ?u.43593
M₁ : Type u_2
M₂ : Type u_3
N₁ : Type ?u.43602
N₂ : Type ?u.43605
Mᵢ : ι → Type ?u.43610
Nᵢ : ι → Type ?u.43615
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₂
⊢ (∀ (a : M₁) (b : M₂), 0 ≤ ↑Q₁ a + ↑Q₂ b) → (∀ (x : M₁), 0 ≤ ↑Q₁ x) ∧ ∀ (x : M₂), 0 ≤ ↑Q₂ x

case mpr
ι : Type ?u.43590
R✝ : Type ?u.43593
M₁ : Type u_2
M₂ : Type u_3
N₁ : Type ?u.43602
N₂ : Type ?u.43605
Mᵢ : ι → Type ?u.43610
Nᵢ : ι → Type ?u.43615
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) → ∀ (a : M₁) (b : M₂), 0 ≤ ↑Q₁ a + ↑Q₂ b
ι : Type ?u.43590
R✝ : Type ?u.43593
M₁ : Type u_2
M₂ : Type u_3
N₁ : Type ?u.43602
N₂ : Type ?u.43605
Mᵢ : ι → Type ?u.43610
Nᵢ : ι → Type ?u.43615
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₂
⊢ (∀ (a : M₁) (b : M₂), 0 ≤ ↑Q₁ a + ↑Q₂ b) ↔ (∀ (x : M₁), 0 ≤ ↑Q₁ x) ∧ ∀ (x : M₂), 0 ≤ ↑Q₂ x
constructor
case mp
ι : Type ?u.43590
R✝ : Type ?u.43593
M₁ : Type u_2
M₂ : Type u_3
N₁ : Type ?u.43602
N₂ : Type ?u.43605
Mᵢ : ι → Type ?u.43610
Nᵢ : ι → Type ?u.43615
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₂
h : ∀ (a : M₁) (b : M₂), 0 ≤ ↑Q₁ a + ↑Q₂ b
⊢ (∀ (x : M₁), 0 ≤ ↑Q₁ x) ∧ ∀ (x : M₂), 0 ≤ ↑Q₂ x
case mp
ι : Type ?u.43590
R✝ : Type ?u.43593
M₁ : Type u_2
M₂ : Type u_3
N₁ : Type ?u.43602
N₂ : Type ?u.43605
Mᵢ : ι → Type ?u.43610
Nᵢ : ι → Type ?u.43615
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₂
⊢ (∀ (a : M₁) (b : M₂), 0 ≤ ↑Q₁ a + ↑Q₂ b) → (∀ (x : M₁), 0 ≤ ↑Q₁ x) ∧ ∀ (x : M₂), 0 ≤ ↑Q₂ x
intro h
case mp.left
ι : Type ?u.43590
R✝ : Type ?u.43593
M₁ : Type u_2
M₂ : Type u_3
N₁ : Type ?u.43602
N₂ : Type ?u.43605
Mᵢ : ι → Type ?u.43610
Nᵢ : ι → Type ?u.43615
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₂
h : ∀ (a : M₁) (b : M₂), 0 ≤ ↑Q₁ a + ↑Q₂ b
⊢ ∀ (x : M₁), 0 ≤ ↑Q₁ x

case mp.right
ι : Type ?u.43590
R✝ : Type ?u.43593
M₁ : Type u_2
M₂ : Type u_3
N₁ : Type ?u.43602
N₂ : Type ?u.43605
Mᵢ : ι → Type ?u.43610
Nᵢ : ι → Type ?u.43615
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₂
h : ∀ (a : M₁) (b : M₂), 0 ≤ ↑Q₁ a + ↑Q₂ b
⊢ ∀ (x : M₂), 0 ≤ ↑Q₂ x
case mp
ι : Type ?u.43590
R✝ : Type ?u.43593
M₁ : Type u_2
M₂ : Type u_3
N₁ : Type ?u.43602
N₂ : Type ?u.43605
Mᵢ : ι → Type ?u.43610
Nᵢ : ι → Type ?u.43615
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₂
h : ∀ (a : M₁) (b : M₂), 0 ≤ ↑Q₁ a + ↑Q₂ b
⊢ (∀ (x : M₁), 0 ≤ ↑Q₁ x) ∧ ∀ (x : M₂), 0 ≤ ↑Q₂ x
constructor
case mp.left
ι : Type ?u.43590
R✝ : Type ?u.43593
M₁ : Type u_2
M₂ : Type u_3
N₁ : Type ?u.43602
N₂ : Type ?u.43605
Mᵢ : ι → Type ?u.43610
Nᵢ : ι → Type ?u.43615
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₂
h : ∀ (a : M₁) (b : M₂), 0 ≤ ↑Q₁ a + ↑Q₂ b
x : M₁
⊢ 0 ≤ ↑Q₁ x
case mp.left
ι : Type ?u.43590
R✝ : Type ?u.43593
M₁ : Type u_2
M₂ : Type u_3
N₁ : Type ?u.43602
N₂ : Type ?u.43605
Mᵢ : ι → Type ?u.43610
Nᵢ : ι → Type ?u.43615
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₂
h : ∀ (a : M₁) (b : M₂), 0 ≤ ↑Q₁ a + ↑Q₂ b
⊢ ∀ (x : M₁), 0 ≤ ↑Q₁ x
intro x
no goals
case mp.left
ι : Type ?u.43590
R✝ : Type ?u.43593
M₁ : Type u_2
M₂ : Type u_3
N₁ : Type ?u.43602
N₂ : Type ?u.43605
Mᵢ : ι → Type ?u.43610
Nᵢ : ι → Type ?u.43615
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₂
h : ∀ (a : M₁) (b : M₂), 0 ≤ ↑Q₁ a + ↑Q₂ b
x : M₁
⊢ 0 ≤ ↑Q₁ x
simpa only [add_zero, map_zero] using h x 0
case mp.right
ι : Type ?u.43590
R✝ : Type ?u.43593
M₁ : Type u_2
M₂ : Type u_3
N₁ : Type ?u.43602
N₂ : Type ?u.43605
Mᵢ : ι → Type ?u.43610
Nᵢ : ι → Type ?u.43615
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₂
h : ∀ (a : M₁) (b : M₂), 0 ≤ ↑Q₁ a + ↑Q₂ b
x : M₂
⊢ 0 ≤ ↑Q₂ x
case mp.right
ι : Type ?u.43590
R✝ : Type ?u.43593
M₁ : Type u_2
M₂ : Type u_3
N₁ : Type ?u.43602
N₂ : Type ?u.43605
Mᵢ : ι → Type ?u.43610
Nᵢ : ι → Type ?u.43615
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₂
h : ∀ (a : M₁) (b : M₂), 0 ≤ ↑Q₁ a + ↑Q₂ b
⊢ ∀ (x : M₂), 0 ≤ ↑Q₂ x
intro x
no goals
case mp.right
ι : Type ?u.43590
R✝ : Type ?u.43593
M₁ : Type u_2
M₂ : Type u_3
N₁ : Type ?u.43602
N₂ : Type ?u.43605
Mᵢ : ι → Type ?u.43610
Nᵢ : ι → Type ?u.43615
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₂
h : ∀ (a : M₁) (b : M₂), 0 ≤ ↑Q₁ a + ↑Q₂ b
x : M₂
⊢ 0 ≤ ↑Q₂ x
simpa only [zero_add, map_zero] using h 0 x
case mpr.intro
ι : Type ?u.43590
R✝ : Type ?u.43593
M₁ : Type u_2
M₂ : Type u_3
N₁ : Type ?u.43602
N₂ : Type ?u.43605
Mᵢ : ι → Type ?u.43610
Nᵢ : ι → Type ?u.43615
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₂
h₁ : ∀ (x : M₁), 0 ≤ ↑Q₁ x
h₂ : ∀ (x : M₂), 0 ≤ ↑Q₂ x
x₁ : M₁
x₂ : M₂
⊢ 0 ≤ ↑Q₁ x₁ + ↑Q₂ x₂
case mpr
ι : Type ?u.43590
R✝ : Type ?u.43593
M₁ : Type u_2
M₂ : Type u_3
N₁ : Type ?u.43602
N₂ : Type ?u.43605
Mᵢ : ι → Type ?u.43610
Nᵢ : ι → Type ?u.43615
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) → ∀ (a : M₁) (b : M₂), 0 ≤ ↑Q₁ a + ↑Q₂ b
rintro ⟨h₁, h₂⟩ x₁ x₂
no goals
case mpr.intro
ι : Type ?u.43590
R✝ : Type ?u.43593
M₁ : Type u_2
M₂ : Type u_3
N₁ : Type ?u.43602
N₂ : Type ?u.43605
Mᵢ : ι → Type ?u.43610
Nᵢ : ι → Type ?u.43615
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₂
h₁ : ∀ (x : M₁), 0 ≤ ↑Q₁ x
h₂ : ∀ (x : M₂), 0 ≤ ↑Q₂ x
x₁ : M₁
x₂ : M₂
⊢ 0 ≤ ↑Q₁ x₁ + ↑Q₂ x₂
exact add_nonneg (h₁ x₁) (h₂ x₂)