awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv
Goal:
ι_1 : Type u_1
R_1 : Type u_2
K : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
V : Type u_8
N : Type u_9
inst : Field K
inst_1 : Invertible (α := K) 2
inst_2 : AddCommGroup V
inst_3 : Module K V
inst_4 : FiniteDimensional K V
ι : Type u_10
S : Type u_11
R : Type u_12
inst_5 : Fintype ι
inst_6 : CommSemiring R
inst_7 : Monoid S
inst_8 : DistribMulAction S R
inst_9 : SMulCommClass S R R
inst_10 : IsScalarTower S R R
w w' : ι → S
u : ι → Sˣ
h : ∀ (i : ι), w' i * HPow.hPow (β := ℕ) (↑(u i) : S) 2 = w i
x : ι → R
j : ι
hj : Membership.mem (γ := Finset ι) Finset.univ j
⊢ (w' j * (↑(HPow.hPow (β := ℕ) (u j) 2) : S)) • (x j * x j) = (w' j * HPow.hPow (β := ℕ) (↑(u j) : S) 2) • (x j * x j)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Prod
Goal:
ι : Type u_1
R : Type u_2
M₁ : Type u_3
M₂ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
P : Type u_7
Mᵢ : ι → Type u_8
Nᵢ : ι → Type u_9
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid N₁
inst_4 : AddCommMonoid N₂
inst_5 : AddCommMonoid P
inst_6 : Module R M₁
inst_7 : Module R M₂
inst_8 : Module R N₁
inst_9 : Module R N₂
inst_10 : Module R P
Q₁ : QuadraticMap R M₁ P
Q₂ : QuadraticMap R M₂ P
m₁ : M₁
⊢ Eq.{u_7 + 1} (α := P)
    ((Q₁.prod Q₂ : (a : M₁ × M₂) → P) (AddHom.toFun (LinearMap.toAddHom (LinearMap.inl R M₁ M₂)) m₁) : P)
    ((Q₁ : (a : M₁) → P) m₁ : P)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Prod
Goal:
ι : Type u_1
R : Type u_2
M₁ : Type u_3
M₂ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
P : Type u_7
Mᵢ : ι → Type u_8
Nᵢ : ι → Type u_9
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid N₁
inst_4 : AddCommMonoid N₂
inst_5 : AddCommMonoid P
inst_6 : Module R M₁
inst_7 : Module R M₂
inst_8 : Module R N₁
inst_9 : Module R N₂
inst_10 : Module R P
Q₁ : QuadraticMap R M₁ P
Q₂ : QuadraticMap R M₂ P
m₁ : M₂
⊢ Eq.{u_7 + 1} (α := P)
    ((Q₁.prod Q₂ : (a : M₁ × M₂) → P) (AddHom.toFun (LinearMap.toAddHom (LinearMap.inr R M₁ M₂)) m₁) : P)
    ((Q₂ : (a : M₂) → P) m₁ : P)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Prod
Goal:
ι : Type u_1
R : Type u_2
M₁ : Type u_3
M₂ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
P : Type u_7
Mᵢ : ι → Type u_8
Nᵢ : ι → Type u_9
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid N₁
inst_4 : AddCommMonoid N₂
inst_5 : AddCommMonoid P
inst_6 : Module R M₁
inst_7 : Module R M₂
inst_8 : Module R N₁
inst_9 : Module R N₂
inst_10 : Module R P
Q₁ : QuadraticMap R M₁ P
m₁ : M₁ × M₂
⊢ Eq.{u_7 + 1} (α := P) ((Q₁ : (a : M₁) → P) (AddHom.toFun (LinearMap.toAddHom (LinearMap.fst R M₁ M₂)) m₁) : P)
    ((Q₁.prod 0 : (a : M₁ × M₂) → P) m₁ : P)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Prod
Goal:
ι : Type u_1
R : Type u_2
M₁ : Type u_3
M₂ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
P : Type u_7
Mᵢ : ι → Type u_8
Nᵢ : ι → Type u_9
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid N₁
inst_4 : AddCommMonoid N₂
inst_5 : AddCommMonoid P
inst_6 : Module R M₁
inst_7 : Module R M₂
inst_8 : Module R N₁
inst_9 : Module R N₂
inst_10 : Module R P
Q₂ : QuadraticMap R M₂ P
m₁ : M₁ × M₂
⊢ Eq.{u_7 + 1} (α := P) ((Q₂ : (a : M₂) → P) (AddHom.toFun (LinearMap.toAddHom (LinearMap.snd R M₁ M₂)) m₁) : P)
    ((prod 0 Q₂ : (a : M₁ × M₂) → P) m₁ : P)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Prod
Goal:
R : Type u_2
M₁ : Type u_3
M₂ : Type u_4
P : Type u_7
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid P
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R P
Q₁ : QuadraticMap R M₁ P
⊢ comp (fst M₂ Q₁) (inl Q₁ 0) = id Q₁

Tactic:
ext fun _ => rfl

Premises used: QuadraticMap.Isometry.ext, rfl
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Prod
Goal:
R : Type u_2
M₁ : Type u_3
M₂ : Type u_4
P : Type u_7
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid P
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R P
Q₂ : QuadraticMap R M₂ P
⊢ comp (snd M₁ Q₂) (inr 0 Q₂) = id Q₂

Tactic:
ext fun _ => rfl

Premises used: QuadraticMap.Isometry.ext, rfl
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Prod
Goal:
R : Type u_2
M₁ : Type u_3
M₂ : Type u_4
P : Type u_7
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid P
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R P
Q₂ : QuadraticMap R M₂ P
⊢ Eq (α := Isometry.{u_2, u_3, u_4, u_7} (M₁ := M₁) 0 Q₂) (comp (snd M₁ Q₂) (inl 0 Q₂)) 0

Tactic:
ext fun _ => rfl

Premises used: QuadraticMap.Isometry.ext, rfl
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Prod
Goal:
R : Type u_2
M₁ : Type u_3
M₂ : Type u_4
P : Type u_7
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid P
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R P
Q₁ : QuadraticMap R M₁ P
⊢ Eq (α := Isometry.{u_2, u_4, u_3, u_7} (M₁ := M₂) 0 Q₁) (comp (fst M₂ Q₁) (inr Q₁ 0)) 0

Tactic:
ext fun _ => rfl

Premises used: QuadraticMap.Isometry.ext, rfl
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Prod
Goal:
R : Type u_2
M₁ : Type u_3
M₂ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
P : Type u_7
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid N₁
inst_4 : AddCommMonoid N₂
inst_5 : AddCommMonoid P
inst_6 : Module R M₁
inst_7 : Module R M₂
inst_8 : Module R N₁
inst_9 : Module R N₂
inst_10 : Module R P
Q₁ : QuadraticMap R M₁ P
Q₂ : QuadraticMap R M₂ P
Q₁' : QuadraticMap R N₁ P
Q₂' : QuadraticMap R N₂ P
e₁ : Q₁.Equivalent Q₁'
e₂ : Q₂.Equivalent Q₂'
⊢ (Q₁.prod Q₂).Equivalent (Q₁'.prod Q₂')

Tactic:
Nonempty.map2 IsometryEquiv.prod e₁ e₂

Premises used: Nonempty.map2, QuadraticMap.IsometryEquiv.prod, QuadraticMap.Equivalent
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Prod
Goal:
R : Type u_2
M₁ : Type u_3
M₂ : Type u_4
P : Type u_7
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid P
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R P
Q₁ : QuadraticMap R M₁ P
Q₂ : QuadraticMap R M₂ P
h : (Q₁.prod Q₂).Anisotropic
⊢ ∀ (a : M₁) (b : M₂),
    HAdd.hAdd (α := P) (β := P) ((Q₁ : (a : M₁) → P) a : P) ((Q₂ : (a : M₂) → P) b : P) = 0 → a = 0 ∧ b = 0

Tactic:
simp_rw [Anisotropic, prod_apply, Prod.forall, Prod.mk_eq_zero] at h

Premises used: QuadraticMap.prod_apply, QuadraticMap.Anisotropic, Prod.mk_eq_zero, Prod.forall
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Prod
Goal:
R : Type u_2
M₁ : Type u_3
M₂ : Type u_4
P : Type u_7
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid P
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R P
Q₁ : QuadraticMap R M₁ P
Q₂ : QuadraticMap R M₂ P
h :
  ∀ (a : M₁) (b : M₂),
    HAdd.hAdd (α := P) (β := P) ((Q₁ : (a : M₁) → P) a : P) ((Q₂ : (a : M₂) → P) b : P) = 0 → a = 0 ∧ b = 0
left : Q₁.Anisotropic
right : Q₂.Anisotropic
⊢ Q₁.Anisotropic ∧ Q₂.Anisotropic

Tactic:
constructor
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Prod
Goal:
R : Type u_2
M₁ : Type u_3
M₂ : Type u_4
P : Type u_7
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid P
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R P
Q₁ : QuadraticMap R M₁ P
Q₂ : QuadraticMap R M₂ P
h :
  ∀ (a : M₁) (b : M₂),
    HAdd.hAdd (α := P) (β := P) ((Q₁ : (a : M₁) → P) a : P) ((Q₂ : (a : M₂) → P) b : P) = 0 → a = 0 ∧ b = 0
x : M₁
hx : Eq.{u_7 + 1} (α := P) ((Q₁ : (a : M₁) → P) x : P) (0 : P)
⊢ x = 0

Tactic:
(h x 0 ?_).1

Premises used: And.left, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Prod
Goal:
R : Type u_2
M₁ : Type u_3
M₂ : Type u_4
P : Type u_7
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid P
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R P
Q₁ : QuadraticMap R M₁ P
Q₂ : QuadraticMap R M₂ P
h :
  ∀ (a : M₁) (b : M₂),
    HAdd.hAdd (α := P) (β := P) ((Q₁ : (a : M₁) → P) a : P) ((Q₂ : (a : M₂) → P) b : P) = 0 → a = 0 ∧ b = 0
x : M₁
hx : Eq.{u_7 + 1} (α := P) ((Q₁ : (a : M₁) → P) x : P) (0 : P)
left : HAdd.hAdd (α := P) (β := P) ((Q₁ : (a : M₁) → P) x : P) ((Q₂ : (a : M₂) → P) 0 : P) = 0
⊢ x = 0

Tactic:
refine (h x 0 ?_).1

Premises used: And.left, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Prod
Goal:
R : Type u_2
M₁ : Type u_3
M₂ : Type u_4
P : Type u_7
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid P
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R P
Q₁ : QuadraticMap R M₁ P
Q₂ : QuadraticMap R M₂ P
h :
  ∀ (a : M₁) (b : M₂),
    HAdd.hAdd (α := P) (β := P) ((Q₁ : (a : M₁) → P) a : P) ((Q₂ : (a : M₂) → P) b : P) = 0 → a = 0 ∧ b = 0
x : M₁
hx : Eq.{u_7 + 1} (α := P) ((Q₁ : (a : M₁) → P) x : P) (0 : P)
left : HAdd.hAdd (α := P) (β := P) (0 : P) ((Q₂ : (a : M₂) → P) 0 : P) = 0
left₁ : Eq.{u_7 + 1} (α := P) ((Q₂ : (a : M₂) → P) 0 : P) (0 : P)
left₂ left₃ : Eq.{u_7 + 1} (α := P) 0 0
⊢ HAdd.hAdd (α := P) (β := P) ((Q₁ : (a : M₁) → P) x : P) ((Q₂ : (a : M₂) → P) 0 : P) = 0

Tactic:
rw [hx, zero_add, map_zero]

Premises used: map_zero, zero_add
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Prod
Goal:
R : Type u_2
M₁ : Type u_3
M₂ : Type u_4
P : Type u_7
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid P
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R P
Q₁ : QuadraticMap R M₁ P
Q₂ : QuadraticMap R M₂ P
h :
  ∀ (a : M₁) (b : M₂),
    HAdd.hAdd (α := P) (β := P) ((Q₁ : (a : M₁) → P) a : P) ((Q₂ : (a : M₂) → P) b : P) = 0 → a = 0 ∧ b = 0
x : M₂
hx : Eq.{u_7 + 1} (α := P) ((Q₂ : (a : M₂) → P) x : P) (0 : P)
⊢ x = 0

Tactic:
(h 0 x ?_).2

Premises used: And.right, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Prod
Goal:
R : Type u_2
M₁ : Type u_3
M₂ : Type u_4
P : Type u_7
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid P
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R P
Q₁ : QuadraticMap R M₁ P
Q₂ : QuadraticMap R M₂ P
h :
  ∀ (a : M₁) (b : M₂),
    HAdd.hAdd (α := P) (β := P) ((Q₁ : (a : M₁) → P) a : P) ((Q₂ : (a : M₂) → P) b : P) = 0 → a = 0 ∧ b = 0
x : M₂
hx : Eq.{u_7 + 1} (α := P) ((Q₂ : (a : M₂) → P) x : P) (0 : P)
right : HAdd.hAdd (α := P) (β := P) ((Q₁ : (a : M₁) → P) 0 : P) ((Q₂ : (a : M₂) → P) x : P) = 0
⊢ x = 0

Tactic:
refine (h 0 x ?_).2

Premises used: And.right, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Prod
Goal:
R : Type u_2
M₁ : Type u_3
M₂ : Type u_4
P : Type u_7
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid P
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R P
Q₁ : QuadraticMap R M₁ P
Q₂ : QuadraticMap R M₂ P
h :
  ∀ (a : M₁) (b : M₂),
    HAdd.hAdd (α := P) (β := P) ((Q₁ : (a : M₁) → P) a : P) ((Q₂ : (a : M₂) → P) b : P) = 0 → a = 0 ∧ b = 0
x : M₂
hx : Eq.{u_7 + 1} (α := P) ((Q₂ : (a : M₂) → P) x : P) (0 : P)
right : HAdd.hAdd (α := P) (β := P) ((Q₁ : (a : M₁) → P) 0 : P) (0 : P) = 0
right₁ : Eq.{u_7 + 1} (α := P) ((Q₁ : (a : M₁) → P) 0 : P) (0 : P)
right₂ right₃ : Eq.{u_7 + 1} (α := P) 0 0
⊢ HAdd.hAdd (α := P) (β := P) ((Q₁ : (a : M₁) → P) 0 : P) ((Q₂ : (a : M₂) → P) x : P) = 0

Tactic:
rw [hx, add_zero, map_zero]

Premises used: map_zero, add_zero
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Prod
Goal:
R : Type u_2
M₁ : Type u_3
M₂ : Type u_4
P : Type u_7
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid P
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R P
inst_7 : Preorder P
inst_8 : AddLeftMono P
Q₁ : QuadraticMap R M₁ P
Q₂ : QuadraticMap R M₂ P
simp_rw :
  (∀ (a : M₁) (b : M₂), 0 ≤ HAdd.hAdd (α := P) (β := P) ((Q₁ : (a : M₁) → P) a : P) ((Q₂ : (a : M₂) → P) b : P)) ↔
    (∀ (x : M₁), LE.le.{u_7} (α := P) (0 : P) ((Q₁ : (a : M₁) → P) x : P)) ∧
      ∀ (x : M₂), LE.le.{u_7} (α := P) (0 : P) ((Q₂ : (a : M₂) → P) x : P)
⊢ (∀ (x : M₁ × M₂), LE.le.{u_7} (α := P) (0 : P) ((Q₁.prod Q₂ : (a : M₁ × M₂) → P) x : P)) ↔
    (∀ (x : M₁), LE.le.{u_7} (α := P) (0 : P) ((Q₁ : (a : M₁) → P) x : P)) ∧
      ∀ (x : M₂), LE.le.{u_7} (α := P) (0 : P) ((Q₂ : (a : M₂) → P) x : P)

Tactic:
simp_rw [Prod.forall, prod_apply]

Premises used: QuadraticMap.prod_apply, Prod.forall
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Prod
Goal:
R : Type u_2
M₁ : Type u_3
M₂ : Type u_4
P : Type u_7
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid P
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R P
inst_7 : Preorder P
inst_8 : AddLeftMono P
Q₁ : QuadraticMap R M₁ P
Q₂ : QuadraticMap R M₂ P
mp :
  (∀ (a : M₁) (b : M₂), 0 ≤ HAdd.hAdd (α := P) (β := P) ((Q₁ : (a : M₁) → P) a : P) ((Q₂ : (a : M₂) → P) b : P)) →
    (∀ (x : M₁), LE.le.{u_7} (α := P) (0 : P) ((Q₁ : (a : M₁) → P) x : P)) ∧
      ∀ (x : M₂), LE.le.{u_7} (α := P) (0 : P) ((Q₂ : (a : M₂) → P) x : P)
mpr :
  ((∀ (x : M₁), LE.le.{u_7} (α := P) (0 : P) ((Q₁ : (a : M₁) → P) x : P)) ∧
      ∀ (x : M₂), LE.le.{u_7} (α := P) (0 : P) ((Q₂ : (a : M₂) → P) x : P)) →
    ∀ (a : M₁) (b : M₂), 0 ≤ HAdd.hAdd (α := P) (β := P) ((Q₁ : (a : M₁) → P) a : P) ((Q₂ : (a : M₂) → P) b : P)
⊢ (∀ (a : M₁) (b : M₂), 0 ≤ HAdd.hAdd (α := P) (β := P) ((Q₁ : (a : M₁) → P) a : P) ((Q₂ : (a : M₂) → P) b : P)) ↔
    (∀ (x : M₁), LE.le.{u_7} (α := P) (0 : P) ((Q₁ : (a : M₁) → P) x : P)) ∧
      ∀ (x : M₂), LE.le.{u_7} (α := P) (0 : P) ((Q₂ : (a : M₂) → P) x : P)

Tactic:
constructor
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Prod
Goal:
R : Type u_2
M₁ : Type u_3
M₂ : Type u_4
P : Type u_7
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid P
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R P
inst_7 : Preorder P
inst_8 : AddLeftMono P
Q₁ : QuadraticMap R M₁ P
Q₂ : QuadraticMap R M₂ P
h : ∀ (a : M₁) (b : M₂), 0 ≤ HAdd.hAdd (α := P) (β := P) ((Q₁ : (a : M₁) → P) a : P) ((Q₂ : (a : M₂) → P) b : P)
mp : ∀ (x : M₁), LE.le.{u_7} (α := P) (0 : P) ((Q₁ : (a : M₁) → P) x : P)
mp₁ : ∀ (x : M₂), LE.le.{u_7} (α := P) (0 : P) ((Q₂ : (a : M₂) → P) x : P)
⊢ (∀ (x : M₁), LE.le.{u_7} (α := P) (0 : P) ((Q₁ : (a : M₁) → P) x : P)) ∧
    ∀ (x : M₂), LE.le.{u_7} (α := P) (0 : P) ((Q₂ : (a : M₂) → P) x : P)

Tactic:
constructor
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Prod
Goal:
R : Type u_2
M₁ : Type u_3
M₂ : Type u_4
P : Type u_7
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid P
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R P
inst_7 : Preorder P
inst_8 : AddLeftMono P
Q₁ : QuadraticMap R M₁ P
Q₂ : QuadraticMap R M₂ P
h : ∀ (a : M₁) (b : M₂), 0 ≤ HAdd.hAdd (α := P) (β := P) ((Q₁ : (a : M₁) → P) a : P) ((Q₂ : (a : M₂) → P) b : P)
x : M₁
⊢ LE.le.{u_7} (α := P) (0 : P) ((Q₁ : (a : M₁) → P) x : P)

Tactic:
simpa only [add_zero, map_zero] using h x 0

Premises used: map_zero, add_zero, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Prod
Goal:
R : Type u_2
M₁ : Type u_3
M₂ : Type u_4
P : Type u_7
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid P
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R P
inst_7 : Preorder P
inst_8 : AddLeftMono P
Q₁ : QuadraticMap R M₁ P
Q₂ : QuadraticMap R M₂ P
h : ∀ (a : M₁) (b : M₂), 0 ≤ HAdd.hAdd (α := P) (β := P) ((Q₁ : (a : M₁) → P) a : P) ((Q₂ : (a : M₂) → P) b : P)
x : M₂
⊢ LE.le.{u_7} (α := P) (0 : P) ((Q₂ : (a : M₂) → P) x : P)

Tactic:
simpa only [zero_add, map_zero] using h 0 x

Premises used: map_zero, zero_add, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Prod
Goal:
R : Type u_2
M₁ : Type u_3
M₂ : Type u_4
P : Type u_7
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid P
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R P
inst_7 : Preorder P
inst_8 : AddLeftMono P
Q₁ : QuadraticMap R M₁ P
Q₂ : QuadraticMap R M₂ P
h₁ : ∀ (x : M₁), LE.le.{u_7} (α := P) (0 : P) ((Q₁ : (a : M₁) → P) x : P)
h₂ : ∀ (x : M₂), LE.le.{u_7} (α := P) (0 : P) ((Q₂ : (a : M₂) → P) x : P)
x₁ : M₁
x₂ : M₂
⊢ 0 ≤ HAdd.hAdd (α := P) (β := P) ((Q₁ : (a : M₁) → P) x₁ : P) ((Q₂ : (a : M₂) → P) x₂ : P)

Tactic:
add_nonneg (h₁ x₁) (h₂ x₂)

Premises used: add_nonneg
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Prod
Goal:
R : Type u_2
M₁ : Type u_3
M₂ : Type u_4
P : Type u_7
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid P
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R P
inst_7 : Preorder P
inst_8 : AddLeftMono P
Q₁ : QuadraticMap R M₁ P
Q₂ : QuadraticMap R M₂ P
h₁ : ∀ (x : M₁), LE.le.{u_7} (α := P) (0 : P) ((Q₁ : (a : M₁) → P) x : P)
h₂ : ∀ (x : M₂), LE.le.{u_7} (α := P) (0 : P) ((Q₂ : (a : M₂) → P) x : P)
x₁ : M₁
x₂ : M₂
⊢ 0 ≤ HAdd.hAdd (α := P) (β := P) ((Q₁ : (a : M₁) → P) x₁ : P) ((Q₂ : (a : M₂) → P) x₂ : P)

Tactic:
exact add_nonneg (h₁ x₁) (h₂ x₂)

Premises used: add_nonneg
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Prod
Goal:
R : Type u_2
M₁ : Type u_3
M₂ : Type u_4
P : Type u_7
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid P
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R P
inst_7 : PartialOrder P
inst_8 : AddLeftMono P
Q₁ : QuadraticMap R M₁ P
Q₂ : QuadraticMap R M₂ P
simp_rw :
  ((∀ (x : M₁), LE.le.{u_7} (α := P) (0 : P) ((Q₁ : (a : M₁) → P) x : P)) ∧
        ∀ (x : M₂), LE.le.{u_7} (α := P) (0 : P) ((Q₂ : (a : M₂) → P) x : P)) ∧
      (Q₁.prod Q₂).Anisotropic ↔
    ((∀ (x : M₁), LE.le.{u_7} (α := P) (0 : P) ((Q₁ : (a : M₁) → P) x : P)) ∧ Q₁.Anisotropic) ∧
      (∀ (x : M₂), LE.le.{u_7} (α := P) (0 : P) ((Q₂ : (a : M₂) → P) x : P)) ∧ Q₂.Anisotropic
⊢ (Q₁.prod Q₂).PosDef ↔ Q₁.PosDef ∧ Q₂.PosDef

Tactic:
simp_rw [posDef_iff_nonneg, nonneg_prod_iff]

Premises used: QuadraticMap.nonneg_prod_iff, QuadraticMap.posDef_iff_nonneg
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Prod
Goal:
R : Type u_2
M₁ : Type u_3
M₂ : Type u_4
P : Type u_7
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid P
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R P
inst_7 : PartialOrder P
inst_8 : AddLeftMono P
Q₁ : QuadraticMap R M₁ P
Q₂ : QuadraticMap R M₂ P
mp :
  ((∀ (x : M₁), LE.le.{u_7} (α := P) (0 : P) ((Q₁ : (a : M₁) → P) x : P)) ∧
        ∀ (x : M₂), LE.le.{u_7} (α := P) (0 : P) ((Q₂ : (a : M₂) → P) x : P)) ∧
      (Q₁.prod Q₂).Anisotropic →
    ((∀ (x : M₁), LE.le.{u_7} (α := P) (0 : P) ((Q₁ : (a : M₁) → P) x : P)) ∧ Q₁.Anisotropic) ∧
      (∀ (x : M₂), LE.le.{u_7} (α := P) (0 : P) ((Q₂ : (a : M₂) → P) x : P)) ∧ Q₂.Anisotropic
mpr :
  ((∀ (x : M₁), LE.le.{u_7} (α := P) (0 : P) ((Q₁ : (a : M₁) → P) x : P)) ∧ Q₁.Anisotropic) ∧
      (∀ (x : M₂), LE.le.{u_7} (α := P) (0 : P) ((Q₂ : (a : M₂) → P) x : P)) ∧ Q₂.Anisotropic →
    ((∀ (x : M₁), LE.le.{u_7} (α := P) (0 : P) ((Q₁ : (a : M₁) → P) x : P)) ∧
        ∀ (x : M₂), LE.le.{u_7} (α := P) (0 : P) ((Q₂ : (a : M₂) → P) x : P)) ∧
      (Q₁.prod Q₂).Anisotropic
⊢ ((∀ (x : M₁), LE.le.{u_7} (α := P) (0 : P) ((Q₁ : (a : M₁) → P) x : P)) ∧
        ∀ (x : M₂), LE.le.{u_7} (α := P) (0 : P) ((Q₂ : (a : M₂) → P) x : P)) ∧
      (Q₁.prod Q₂).Anisotropic ↔
    ((∀ (x : M₁), LE.le.{u_7} (α := P) (0 : P) ((Q₁ : (a : M₁) → P) x : P)) ∧ Q₁.Anisotropic) ∧
      (∀ (x : M₂), LE.le.{u_7} (α := P) (0 : P) ((Q₂ : (a : M₂) → P) x : P)) ∧ Q₂.Anisotropic

Tactic:
constructor
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Prod
Goal:
R : Type u_2
M₁ : Type u_3
M₂ : Type u_4
P : Type u_7
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid P
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R P
inst_7 : PartialOrder P
inst_8 : AddLeftMono P
Q₁ : QuadraticMap R M₁ P
Q₂ : QuadraticMap R M₂ P
ha : (Q₁.prod Q₂).Anisotropic
hle₁ : ∀ (x : M₁), LE.le.{u_7} (α := P) (0 : P) ((Q₁ : (a : M₁) → P) x : P)
hle₂ : ∀ (x : M₂), LE.le.{u_7} (α := P) (0 : P) ((Q₂ : (a : M₂) → P) x : P)
⊢ Q₁.Anisotropic

Tactic:
obtain ⟨ha₁, ha₂⟩ := anisotropic_of_prod ha

Premises used: QuadraticMap.anisotropic_of_prod
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Prod
Goal:
R : Type u_2
M₁ : Type u_3
M₂ : Type u_4
P : Type u_7
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid P
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R P
inst_7 : PartialOrder P
inst_8 : AddLeftMono P
Q₁ : QuadraticMap R M₁ P
Q₂ : QuadraticMap R M₂ P
ha : (Q₁.prod Q₂).Anisotropic
hle₁ : ∀ (x : M₁), LE.le.{u_7} (α := P) (0 : P) ((Q₁ : (a : M₁) → P) x : P)
hle₂ : ∀ (x : M₂), LE.le.{u_7} (α := P) (0 : P) ((Q₂ : (a : M₂) → P) x : P)
ha₁ : Q₁.Anisotropic
⊢ Q₂.Anisotropic

Tactic:
obtain ⟨ha₁, ha₂⟩ := anisotropic_of_prod ha

Premises used: QuadraticMap.anisotropic_of_prod
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Prod
Goal:
R : Type u_2
M₁ : Type u_3
M₂ : Type u_4
P : Type u_7
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid P
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R P
inst_7 : PartialOrder P
inst_8 : AddLeftMono P
Q₁ : QuadraticMap R M₁ P
Q₂ : QuadraticMap R M₂ P
ha : (Q₁.prod Q₂).Anisotropic
hle₁ : ∀ (x : M₁), LE.le.{u_7} (α := P) (0 : P) ((Q₁ : (a : M₁) → P) x : P)
hle₂ : ∀ (x : M₂), LE.le.{u_7} (α := P) (0 : P) ((Q₂ : (a : M₂) → P) x : P)
ha₁ : Q₁.Anisotropic
ha₂ : Q₂.Anisotropic
⊢ ((∀ (x : M₁), LE.le.{u_7} (α := P) (0 : P) ((Q₁ : (a : M₁) → P) x : P)) ∧ Q₁.Anisotropic) ∧
    (∀ (x : M₂), LE.le.{u_7} (α := P) (0 : P) ((Q₂ : (a : M₂) → P) x : P)) ∧ Q₂.Anisotropic

Tactic:
⟨⟨hle₁, ha₁⟩, ⟨hle₂, ha₂⟩⟩

Premises used: And.intro
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Prod
Goal:
R : Type u_2
M₁ : Type u_3
M₂ : Type u_4
P : Type u_7
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid P
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R P
inst_7 : PartialOrder P
inst_8 : AddLeftMono P
Q₁ : QuadraticMap R M₁ P
Q₂ : QuadraticMap R M₂ P
ha : (Q₁.prod Q₂).Anisotropic
hle₁ : ∀ (x : M₁), LE.le.{u_7} (α := P) (0 : P) ((Q₁ : (a : M₁) → P) x : P)
hle₂ : ∀ (x : M₂), LE.le.{u_7} (α := P) (0 : P) ((Q₂ : (a : M₂) → P) x : P)
ha₁ : Q₁.Anisotropic
ha₂ : Q₂.Anisotropic
⊢ ((∀ (x : M₁), LE.le.{u_7} (α := P) (0 : P) ((Q₁ : (a : M₁) → P) x : P)) ∧ Q₁.Anisotropic) ∧
    (∀ (x : M₂), LE.le.{u_7} (α := P) (0 : P) ((Q₂ : (a : M₂) → P) x : P)) ∧ Q₂.Anisotropic

Tactic:
exact ⟨⟨hle₁, ha₁⟩, ⟨hle₂, ha₂⟩⟩
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Prod
Goal:
R : Type u_2
M₁ : Type u_3
M₂ : Type u_4
P : Type u_7
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid P
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R P
inst_7 : PartialOrder P
inst_8 : AddLeftMono P
Q₁ : QuadraticMap R M₁ P
Q₂ : QuadraticMap R M₂ P
hle₁ : ∀ (x : M₁), LE.le.{u_7} (α := P) (0 : P) ((Q₁ : (a : M₁) → P) x : P)
ha₁ : Q₁.Anisotropic
hle₂ : ∀ (x : M₂), LE.le.{u_7} (α := P) (0 : P) ((Q₂ : (a : M₂) → P) x : P)
ha₂ : Q₂.Anisotropic
⊢ ((∀ (x : M₁), LE.le.{u_7} (α := P) (0 : P) ((Q₁ : (a : M₁) → P) x : P)) ∧
      ∀ (x : M₂), LE.le.{u_7} (α := P) (0 : P) ((Q₂ : (a : M₂) → P) x : P)) ∧
    (Q₁.prod Q₂).Anisotropic

Tactic:
⟨⟨hle₁, hle₂⟩, ?_⟩

Premises used: And.intro
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Prod
Goal:
R : Type u_2
M₁ : Type u_3
M₂ : Type u_4
P : Type u_7
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid P
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R P
inst_7 : PartialOrder P
inst_8 : AddLeftMono P
Q₁ : QuadraticMap R M₁ P
Q₂ : QuadraticMap R M₂ P
hle₁ : ∀ (x : M₁), LE.le.{u_7} (α := P) (0 : P) ((Q₁ : (a : M₁) → P) x : P)
ha₁ : Q₁.Anisotropic
hle₂ : ∀ (x : M₂), LE.le.{u_7} (α := P) (0 : P) ((Q₂ : (a : M₂) → P) x : P)
ha₂ : Q₂.Anisotropic
mpr : (Q₁.prod Q₂).Anisotropic
⊢ ((∀ (x : M₁), LE.le.{u_7} (α := P) (0 : P) ((Q₁ : (a : M₁) → P) x : P)) ∧
      ∀ (x : M₂), LE.le.{u_7} (α := P) (0 : P) ((Q₂ : (a : M₂) → P) x : P)) ∧
    (Q₁.prod Q₂).Anisotropic

Tactic:
refine ⟨⟨hle₁, hle₂⟩, ?_⟩