awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv (goal)
Goal:
ι : Type u_1
R : 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 : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₁
inst_3 : AddCommMonoid M₂
inst_4 : AddCommMonoid M₃
inst_5 : AddCommMonoid N
inst_6 : Module R M
inst_7 : Module R M₁
inst_8 : Module R M₂
inst_9 : Module R M₃
inst_10 : Module R N
Q₁ : QuadraticMap R M₁ N
Q₂ : QuadraticMap R M₂ N
Q₃ : QuadraticMap R M₃ N
f : Q₁.IsometryEquiv Q₂
m : M₂
⊢ Eq.{u_9 + 1} (α := N) ((Q₂ : (a : M₂) → N) ((f : (a : M₁) → M₂) ((↑f.symm : M₂ →ₗ[R] M₁).toFun m) : M₂) : N)
    ((Q₂ : (a : M₂) → N) m : N)
have h : (f : (a : M₁) → M₂) ((↑f.symm : M₂ →ₗ[R] M₁).toFun m) = m
Tactic: congr
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv (goal)
Goal:
ι : Type u_1
R : 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 : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₁
inst_3 : AddCommMonoid M₂
inst_4 : AddCommMonoid M₃
inst_5 : AddCommMonoid N
inst_6 : Module R M
inst_7 : Module R M₁
inst_8 : Module R M₂
inst_9 : Module R M₃
inst_10 : Module R N
Q₁ : QuadraticMap R M₁ N
Q₂ : QuadraticMap R M₂ N
Q₃ : QuadraticMap R M₃ N
f : Q₁.IsometryEquiv Q₂
g : Q₂.IsometryEquiv Q₃
m : M₁
⊢ Eq.{u_9 + 1} (α := N) ((Q₃ : (a : M₃) → N) ((↑(f.toLinearEquiv ≪≫ₗ g.toLinearEquiv) : M₁ →ₗ[R] M₃).toFun m) : N)
    ((Q₁ : (a : M₁) → N) m : N)
have rw : Eq.{u_9 + 1} (α := N) ((Q₃ : (a : M₃) → N) ((↑(f.toLinearEquiv ≪≫ₗ g.toLinearEquiv) : M₁ →ₗ[R] M₃).toFun m) : N)
  ((Q₃ : (a : M₃) → N) ((g : (a : M₂) → M₃) ((f : (a : M₁) → M₂) m : M₂) : M₃) : N)
Tactic: rw [← f.map_app, ← g.map_app]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv (goal)
Goal:
ι : Type u_1
R : 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
Q : QuadraticForm K V
v : Basis (Fin (finrank K V)) K V
hv₁ :
  LinearMap.IsOrthoᵢ.{u_3, u_3, u_3, u_8, 0} (R := K) (R₁ := K) (M := K) (M₁ := V) (n := Fin (finrank K V)) (I₁ :=
    RingHom.id K) (I₁' := RingHom.id K)
    (((associated.{u_3, u_8, u_3} (R := K) (M := V) (N := K) : QuadraticMap K V K →ₗ[K] LinearMap.BilinMap K V K) :
        (a : QuadraticMap K V K) → LinearMap.BilinMap K V K)
      Q)
    (⇑v : (a : Fin (finrank K V)) → V)
iso : IsometryEquiv Q (basisRepr Q v) := isometryEquivBasisRepr Q v
⊢ IsometryEquiv (M₂ := Fin (finrank K V) → K) Q
    (weightedSumSquares (S := K) K fun (i : Fin (finrank K V)) ↦
      (Q : (a : V) → K) ((v : (a : Fin (finrank K V)) → V) i : V))
have refine : ∀ (m : V),
  Eq (α := K)
    ((weightedSumSquares (S := K) K fun (i : Fin (finrank K V)) ↦
            (Q : (a : V) → K) ((v : (a : Fin (finrank K V)) → V) i : V) :
          (a : Fin (finrank K V) → K) → K)
        ((↑iso.toLinearEquiv : V →ₗ[K] Fin (finrank K V) → K).toFun m) :
      K)
    ((Q : (a : V) → K) m : K)
Tactic: refine ⟨iso, fun m => ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv (goal)
Goal:
ι : Type u_1
R : 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
Q : QuadraticForm K V
v : Basis (Fin (finrank K V)) K V
hv₁ :
  LinearMap.IsOrthoᵢ.{u_3, u_3, u_3, u_8, 0} (R := K) (R₁ := K) (M := K) (M₁ := V) (n := Fin (finrank K V)) (I₁ :=
    RingHom.id K) (I₁' := RingHom.id K)
    (((associated.{u_3, u_8, u_3} (R := K) (M := V) (N := K) : QuadraticMap K V K →ₗ[K] LinearMap.BilinMap K V K) :
        (a : QuadraticMap K V K) → LinearMap.BilinMap K V K)
      Q)
    (⇑v : (a : Fin (finrank K V)) → V)
iso : IsometryEquiv Q (basisRepr Q v) := isometryEquivBasisRepr Q v
m : V
⊢ Eq (α := K)
    ((weightedSumSquares (S := K) K fun (i : Fin (finrank K V)) ↦
            (Q : (a : V) → K) ((v : (a : Fin (finrank K V)) → V) i : V) :
          (a : Fin (finrank K V) → K) → K)
        ((↑iso.toLinearEquiv : V →ₗ[K] Fin (finrank K V) → K).toFun m) :
      K)
    ((Q : (a : V) → K) m : K)
have h : (weightedSumSquares (S := K) K fun (i : Fin (finrank K V)) ↦
    (Q : (a : V) → K) ((v : (a : Fin (finrank K V)) → V) i : V)) =
  basisRepr Q v
Tactic: convert! iso.map_app m
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv (goal)
Goal:
ι : Type u_1
R : 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
Q : QuadraticForm K V
v : Basis (Fin (finrank K V)) K V
hv₁ :
  LinearMap.IsOrthoᵢ.{u_3, u_3, u_3, u_8, 0} (R := K) (R₁ := K) (M := K) (M₁ := V) (n := Fin (finrank K V)) (I₁ :=
    RingHom.id K) (I₁' := RingHom.id K)
    (((associated.{u_3, u_8, u_3} (R := K) (M := V) (N := K) : QuadraticMap K V K →ₗ[K] LinearMap.BilinMap K V K) :
        (a : QuadraticMap K V K) → LinearMap.BilinMap K V K)
      Q)
    (⇑v : (a : Fin (finrank K V)) → V)
iso : IsometryEquiv Q (basisRepr Q v) := isometryEquivBasisRepr Q v
m : V
⊢ (weightedSumSquares (S := K) K fun (i : Fin (finrank K V)) ↦
      (Q : (a : V) → K) ((v : (a : Fin (finrank K V)) → V) i : V)) =
    basisRepr Q v
have h : Eq (α := QuadraticMap K (Fin (finrank K V) → K) K)
  (weightedSumSquares (S := K) K fun (i : Fin (finrank K V)) ↦
    (Q : (a : V) → K) ((v : (a : Fin (finrank K V)) → V) i : V))
  (weightedSumSquares (S := K) K fun (i : Fin (finrank K V)) ↦
    (Q : (a : V) → K) ((v : (a : Fin (finrank K V)) → V) i : V))
Tactic: rw [basisRepr_eq_of_iIsOrtho _ _ hv₁]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv (goal)
Goal:
K : Type u_3
V : Type u_8
inst : Field K
inst_1 : Invertible (α := K) 2
inst_2 : AddCommGroup V
inst_3 : Module K V
inst_4 : FiniteDimensional K V
Q : QuadraticForm K V
hQ :
  LinearMap.SeparatingLeft.{u_3, u_3, u_3, u_3, u_8, u_8} (R := K) (R₁ := K) (R₂ := K) (M := K) (M₁ := V) (M₂ := V)
    (I₁ := RingHom.id K) (I₂ := RingHom.id K)
    (((associated.{u_3, u_8, u_3} (R := K) (M := V) (N := K) : QuadraticMap K V K →ₗ[K] LinearMap.BilinMap K V K) :
        (a : QuadraticMap K V K) → LinearMap.BilinMap K V K)
      Q)
⊢ ∃ (w : Fin (finrank K V) → Kˣ), Equivalent Q (weightedSumSquares K w)
have obtain : ∀ (v : Basis (Fin (finrank K V)) K V)
  (hv₁ :
    LinearMap.IsOrthoᵢ.{u_3, u_3, u_3, u_8, 0} (R := K) (R₁ := K) (M := K) (M₁ := V) (n := Fin (finrank K V)) (I₁ :=
      RingHom.id K) (I₁' := RingHom.id K)
      (((associatedHom.{u_3, u_3, u_8, u_3} K (R := K) (M := V) (N := K) :
            QuadraticMap K V K →ₗ[K] LinearMap.BilinMap K V K) :
          (a : QuadraticMap K V K) → LinearMap.BilinMap K V K)
        Q)
      (⇑v : (a : Fin (finrank K V)) → V)),
  ∃ (w : Fin (finrank K V) → Kˣ), Equivalent Q (weightedSumSquares K w)
Tactic: obtain ⟨v, hv₁⟩ := exists_orthogonal_basis (associated_isSymm K Q)
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv (hypothesis)
Goal:
K : Type u_3
V : Type u_8
inst : Field K
inst_1 : Invertible (α := K) 2
inst_2 : AddCommGroup V
inst_3 : Module K V
inst_4 : FiniteDimensional K V
Q : QuadraticForm K V
hQ :
  LinearMap.SeparatingLeft.{u_3, u_3, u_3, u_3, u_8, u_8} (R := K) (R₁ := K) (R₂ := K) (M := K) (M₁ := V) (M₂ := V)
    (I₁ := RingHom.id K) (I₂ := RingHom.id K)
    (((associated.{u_3, u_8, u_3} (R := K) (M := V) (N := K) : QuadraticMap K V K →ₗ[K] LinearMap.BilinMap K V K) :
        (a : QuadraticMap K V K) → LinearMap.BilinMap K V K)
      Q)
v : Basis (Fin (finrank K V)) K V
hv₁ :
  LinearMap.IsOrthoᵢ.{u_3, u_3, u_3, u_8, 0} (R := K) (R₁ := K) (M := K) (M₁ := V) (n := Fin (finrank K V)) (I₁ :=
    RingHom.id K) (I₁' := RingHom.id K)
    (((associatedHom.{u_3, u_3, u_8, u_3} K (R := K) (M := V) (N := K) :
          QuadraticMap K V K →ₗ[K] LinearMap.BilinMap K V K) :
        (a : QuadraticMap K V K) → LinearMap.BilinMap K V K)
      Q)
    (⇑v : (a : Fin (finrank K V)) → V)
⊢ ∃ (w : Fin (finrank K V) → Kˣ), Equivalent Q (weightedSumSquares K w)
have hv₂ : ∀ (i : Fin (finrank K V)),
  ¬LinearMap.IsOrtho.{u_3, u_3, u_3, u_3, u_8, u_8} (R := K) (R₁ := K) (R₂ := K) (M := K) (M₁ := V) (M₂ := V) (I₁ :=
      RingHom.id K) (I₂ := RingHom.id K)
      (((associatedHom.{u_3, u_3, u_8, u_3} K (R := K) (M := V) (N := K) :
              QuadraticMap K V K →ₗ[K] LinearMap.BilinMap K V K) :
            (a : QuadraticMap K V K) → LinearMap.BilinMap K V K)
          Q :
        LinearMap.BilinMap K V K)
      ((v : (a : Fin (finrank K V)) → V) i : V) ((v : (a : Fin (finrank K V)) → V) i : V)
Tactic: have hv₂ := hv₁.not_isOrtho_basis_self_of_separatingLeft hQ
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv (hypothesis)
Goal:
K : Type u_3
V : Type u_8
inst : Field K
inst_1 : Invertible (α := K) 2
inst_2 : AddCommGroup V
inst_3 : Module K V
inst_4 : FiniteDimensional K V
Q : QuadraticForm K V
hQ :
  LinearMap.SeparatingLeft.{u_3, u_3, u_3, u_3, u_8, u_8} (R := K) (R₁ := K) (R₂ := K) (M := K) (M₁ := V) (M₂ := V)
    (I₁ := RingHom.id K) (I₂ := RingHom.id K)
    (((associated.{u_3, u_8, u_3} (R := K) (M := V) (N := K) : QuadraticMap K V K →ₗ[K] LinearMap.BilinMap K V K) :
        (a : QuadraticMap K V K) → LinearMap.BilinMap K V K)
      Q)
v : Basis (Fin (finrank K V)) K V
hv₁ :
  LinearMap.IsOrthoᵢ.{u_3, u_3, u_3, u_8, 0} (R := K) (R₁ := K) (M := K) (M₁ := V) (n := Fin (finrank K V)) (I₁ :=
    RingHom.id K) (I₁' := RingHom.id K)
    (((associatedHom.{u_3, u_3, u_8, u_3} K (R := K) (M := V) (N := K) :
          QuadraticMap K V K →ₗ[K] LinearMap.BilinMap K V K) :
        (a : QuadraticMap K V K) → LinearMap.BilinMap K V K)
      Q)
    (⇑v : (a : Fin (finrank K V)) → V)
hv₂ :
  ∀ (i : Fin (finrank K V)),
    ¬LinearMap.IsOrtho.{u_3, u_3, u_3, u_3, u_8, u_8} (R := K) (R₁ := K) (R₂ := K) (M := K) (M₁ := V) (M₂ := V) (I₁ :=
        RingHom.id K) (I₂ := RingHom.id K)
        (((associatedHom.{u_3, u_3, u_8, u_3} K (R := K) (M := V) (N := K) :
                QuadraticMap K V K →ₗ[K] LinearMap.BilinMap K V K) :
              (a : QuadraticMap K V K) → LinearMap.BilinMap K V K)
            Q :
          LinearMap.BilinMap K V K)
        ((v : (a : Fin (finrank K V)) → V) i : V) ((v : (a : Fin (finrank K V)) → V) i : V)
⊢ ∃ (w : Fin (finrank K V) → Kˣ), Equivalent Q (weightedSumSquares K w)
have hv₃ : ∀ (i : Fin (finrank K V)),
  ¬Eq.{u_3 + 1} (α := K) ((Q : (a : V) → K) ((v : (a : Fin (finrank K V)) → V) i : V) : K) (0 : K)
Tactic: simp_rw [LinearMap.IsOrtho, associated_eq_self_apply] at hv₂
Cleared hypotheses: hv₂
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv (goal)
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
v : R
x : ι → R
⊢ u • v • x = HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) v : R) (u • x)
have h₁ : ∀ (i : ι), (u • v • x) i = HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) v : R) (u • x) i
Tactic: ext i
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv (goal)
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
⊢ Eq.{u_12 + 1} (α := R) ((weightedSumSquares R w' : (a : ι → R) → R) (u • x) : R)
    ((weightedSumSquares R w : (a : ι → R) → R) x : R)
have simp : Eq.{u_12 + 1} (α := R) (∑ x_1 : ι, w' x_1 • (u x_1 • x x_1 * u x_1 • x x_1)) (∑ i : ι, w i • (x i * x i))
Tactic: simp only [weightedSumSquares_apply, Pi.smul_apply']
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv (goal)
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
⊢ Eq.{u_12 + 1} (α := R) (∑ x_1 : ι, w' x_1 • (u x_1 • x x_1 * u x_1 • x x_1)) (∑ i : ι, w i • (x i * x i))
have refine : ∀ (j : ι) (hj : Membership.mem (γ := Finset ι) Finset.univ j), w' j • (u j • x j * u j • x j) = w j • (x j * x j)
Tactic: refine Finset.sum_congr rfl fun j hj => ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv (goal)
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 • (u j • x j * u j • x j) = w j • (x j * x j)
have rw : (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: rw [smul_mul_smul, Units.smul_def, smul_smul, ← pow_two, ← h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Prod (hypothesis)
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
⊢ Q₁.Anisotropic ∧ Q₂.Anisotropic
have 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
Tactic: simp_rw [Anisotropic, prod_apply, Prod.forall, Prod.mk_eq_zero] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Prod (goal)
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
⊢ Q₁.Anisotropic ∧ Q₂.Anisotropic
have left : Q₁.Anisotropic
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Prod (goal)
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
⊢ Q₁.Anisotropic ∧ Q₂.Anisotropic
have right : Q₂.Anisotropic
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Prod (goal)
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
have left : HAdd.hAdd (α := P) (β := P) ((Q₁ : (a : M₁) → P) x : P) ((Q₂ : (a : M₂) → P) 0 : P) = 0
Tactic: refine (h x 0 ?_).1
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Prod (goal)
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)
⊢ HAdd.hAdd (α := P) (β := P) ((Q₁ : (a : M₁) → P) x : P) ((Q₂ : (a : M₂) → P) 0 : P) = 0
have left : HAdd.hAdd (α := P) (β := P) (0 : P) ((Q₂ : (a : M₂) → P) 0 : P) = 0
Tactic: rw [hx, zero_add, map_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Prod (goal)
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
⊢ HAdd.hAdd (α := P) (β := P) ((Q₁ : (a : M₁) → P) x : P) ((Q₂ : (a : M₂) → P) 0 : P) = 0
have left₁ : Eq.{u_7 + 1} (α := P) ((Q₂ : (a : M₂) → P) 0 : P) (0 : P)
Tactic: rw [hx, zero_add, map_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Prod (goal)
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)
⊢ HAdd.hAdd (α := P) (β := P) ((Q₁ : (a : M₁) → P) x : P) ((Q₂ : (a : M₂) → P) 0 : P) = 0
have left₂ : Eq.{u_7 + 1} (α := P) 0 0
Tactic: rw [hx, zero_add, map_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Prod (goal)
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
have right : HAdd.hAdd (α := P) (β := P) ((Q₁ : (a : M₁) → P) 0 : P) ((Q₂ : (a : M₂) → P) x : P) = 0
Tactic: refine (h 0 x ?_).2
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Prod (goal)
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)
⊢ HAdd.hAdd (α := P) (β := P) ((Q₁ : (a : M₁) → P) 0 : P) ((Q₂ : (a : M₂) → P) x : P) = 0
have right : HAdd.hAdd (α := P) (β := P) ((Q₁ : (a : M₁) → P) 0 : P) (0 : P) = 0
Tactic: rw [hx, add_zero, map_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Prod (goal)
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
⊢ HAdd.hAdd (α := P) (β := P) ((Q₁ : (a : M₁) → P) 0 : P) ((Q₂ : (a : M₂) → P) x : P) = 0
have right₁ : Eq.{u_7 + 1} (α := P) ((Q₁ : (a : M₁) → P) 0 : P) (0 : P)
Tactic: rw [hx, add_zero, map_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Prod (goal)
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)
⊢ HAdd.hAdd (α := P) (β := P) ((Q₁ : (a : M₁) → P) 0 : P) ((Q₂ : (a : M₂) → P) x : P) = 0
have right₂ : Eq.{u_7 + 1} (α := P) 0 0
Tactic: rw [hx, add_zero, map_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Prod (goal)
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
⊢ (∀ (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)
have 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)
Tactic: simp_rw [Prod.forall, prod_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Prod (goal)
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
⊢ (∀ (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)
have 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)
Tactic: constructor