awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv
Goal:
R : Type u_2
M₁ : Type u_5
M₂ : Type u_6
N : Type u_9
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid N
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R N
Q₁ : QuadraticMap R M₁ N
Q₂ : QuadraticMap R M₂ N
f : Q₁.IsometryEquiv Q₂
⊢ f.symm = f.symm.toLinearEquiv

Tactic:
rfl

Premises used: LinearEquiv.symm, rfl
-- Module: Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv
Goal:
R : Type u_2
M : Type u_4
N : Type u_9
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
Q : QuadraticMap R M N
⊢ Q.Equivalent Q

Tactic:
⟨IsometryEquiv.refl Q⟩

Premises used: Nonempty.intro, QuadraticMap.IsometryEquiv.refl, QuadraticMap.Equivalent
-- Module: Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv
Goal:
R : Type u_2
M₁ : Type u_5
M₂ : Type u_6
N : Type u_9
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid N
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R N
Q₁ : QuadraticMap R M₁ N
Q₂ : QuadraticMap R M₂ N
h : Q₁.Equivalent Q₂
⊢ Q₂.Equivalent Q₁

Tactic:
h.elim fun f => ⟨f.symm⟩

Premises used: QuadraticMap.IsometryEquiv.symm, Nonempty.elim, Nonempty.intro
-- Module: Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv
Goal:
R : Type u_2
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N : Type u_9
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M₃
inst_4 : AddCommMonoid N
inst_5 : Module R M₁
inst_6 : Module R M₂
inst_7 : Module R M₃
inst_8 : Module R N
Q₁ : QuadraticMap R M₁ N
Q₂ : QuadraticMap R M₂ N
Q₃ : QuadraticMap R M₃ N
h : Q₁.Equivalent Q₂
h' : Q₂.Equivalent Q₃
⊢ Q₁.Equivalent Q₃

Tactic:
h'.elim <| h.elim fun f g => ⟨f.trans g⟩

Premises used: Nonempty.elim, Nonempty.intro, QuadraticMap.IsometryEquiv.trans
-- Module: Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv
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
f : M₁ ≃ₗ[R] M
m : M
⊢ Eq.{u_9 + 1} (α := N) ((Q.comp (↑f : M₁ →ₗ[R] M) : (a : M₁) → N) ((↑f.symm : M →ₗ[R] M₁).toFun m) : N)
    ((Q : (a : M) → N) m : N)

Tactic:
simp only [comp_apply, LinearEquiv.coe_coe, LinearEquiv.toFun_eq_coe,
        f.apply_symm_apply]

Premises used: QuadraticMap.comp_apply, LinearEquiv.apply_symm_apply, LinearEquiv.toFun_eq_coe, LinearEquiv.coe_coe
-- Module: Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv
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
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)
⊢ 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))

Tactic:
refine ⟨iso, fun m => ?_⟩
-- Module: Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv
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)
    ((basisRepr Q v : (a : Fin (finrank K V) → K) → K)
        ((iso : (a : V) → Fin (finrank K V) → K) m : Fin (finrank K V) → K) :
      K)
    ((Q : (a : V) → K) m : K)

Tactic:
iso.map_app m

Premises used: QuadraticMap.IsometryEquiv.map_app
-- Module: Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv
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
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
⊢ 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:
convert! iso.map_app m

Premises used: QuadraticMap.IsometryEquiv.map_app
-- Module: Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv
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
h 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))
⊢ (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:
rw [basisRepr_eq_of_iIsOrtho _ _ hv₁]

Premises used: QuadraticMap.basisRepr_eq_of_iIsOrtho
-- Module: Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv
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
⊢ ∃ (w : Fin (finrank K V) → K), Equivalent Q (weightedSumSquares K w)

Tactic:
let ⟨v, hv₁⟩ := exists_orthogonal_basis (associated_isSymm _ Q)
  ⟨_, ⟨Q.isometryEquivWeightedSumSquares v hv₁⟩⟩

Premises used: Exists, _private.0.QuadraticForm.equivalent_weightedSumSquares.match_1, LinearMap.BilinForm.exists_orthogonal_basis, QuadraticForm.isometryEquivWeightedSumSquares, Nonempty.intro, QuadraticMap.weightedSumSquares, QuadraticForm.associated_isSymm, Exists.intro, DFunLike.coe, QuadraticMap.Equivalent
-- Module: Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv
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)
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)
⊢ ∃ (w : Fin (finrank K V) → Kˣ), Equivalent Q (weightedSumSquares K w)

Tactic:
obtain ⟨v, hv₁⟩ := exists_orthogonal_basis (associated_isSymm K Q)

Premises used: LinearMap.BilinForm.exists_orthogonal_basis, QuadraticForm.associated_isSymm
-- Module: Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv
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)
⊢ ∀ (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
-- Module: Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv
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)
⊢ ∀ (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₂

Premises used: QuadraticMap.associated_eq_self_apply, LinearMap.IsOrtho
-- Module: Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv
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)),
    ¬Eq.{u_3 + 1} (α := K) ((Q : (a : V) → K) ((v : (a : Fin (finrank K V)) → V) i : V) : K) (0 : K)
⊢ ∃ (w : Fin (finrank K V) → Kˣ), Equivalent Q (weightedSumSquares K w)

Tactic:
⟨fun i => Units.mk0 _ (hv₂ i), ⟨Q.isometryEquivWeightedSumSquares v hv₁⟩⟩

Premises used: QuadraticForm.isometryEquivWeightedSumSquares, Nonempty.intro, Units.mk0, Exists.intro, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv
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)),
    ¬Eq.{u_3 + 1} (α := K) ((Q : (a : V) → K) ((v : (a : Fin (finrank K V)) → V) i : V) : K) (0 : K)
⊢ ∃ (w : Fin (finrank K V) → Kˣ), Equivalent Q (weightedSumSquares K w)

Tactic:
exact ⟨fun i => Units.mk0 _ (hv₂ i), ⟨Q.isometryEquivWeightedSumSquares v hv₁⟩⟩
-- 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
h : w = w'
⊢ ∀ (m : ι → R),
    Eq.{u_12 + 1} (α := R)
      ((weightedSumSquares R w' : (a : ι → R) → R)
          (AddHom.toFun (LinearMap.toAddHom (↑(LinearEquiv.refl R (ι → R)) : (ι → R) →ₗ[R] ι → R)) m) :
        R)
      ((weightedSumSquares R w : (a : ι → R) → R) m : R)

Tactic:
simp [h]
-- 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 y : ι → R
⊢ u • (x + y) = u • x + u • y

Tactic:
simp
-- 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
v : R
x : ι → R
h₁ : ∀ (i : ι), (u • v • x) i = HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) v : R) (u • x) i
⊢ u • v • x = HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) v : R) (u • x)

Tactic:
ext i
-- 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
v : R
x : ι → R
i : ι
⊢ (u • v • x) i = HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) v : R) (u • x) i

Tactic:
simp only [Pi.smul_apply', Pi.smul_apply, RingHom.id_apply, smul_comm]

Premises used: RingHom.id_apply, Pi.smul_apply', SMulCommClass.smul_comm, Pi.smul_apply
-- 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
⊢ (fun (x : ι → R) ↦ u⁻¹ • x) ((fun (x : ι → R) ↦ u • x) x) = x

Tactic:
simp
-- 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
⊢ (fun (x : ι → R) ↦ u • x) ((fun (x : ι → R) ↦ u⁻¹ • x) x) = x

Tactic:
simp
-- 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
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))
⊢ Eq.{u_12 + 1} (α := R) ((weightedSumSquares R w' : (a : ι → R) → R) (u • x) : R)
    ((weightedSumSquares R w : (a : ι → R) → R) x : R)

Tactic:
simp only [weightedSumSquares_apply, Pi.smul_apply']

Premises used: Pi.smul_apply', QuadraticMap.weightedSumSquares_apply
-- 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
⊢ 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:
Finset.sum_congr rfl fun j hj => ?_

Premises used: Finset.sum_congr, rfl
-- 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
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)
⊢ 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:
refine Finset.sum_congr rfl fun j hj => ?_

Premises used: Finset.sum_congr, rfl
-- 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
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)
⊢ w' j • (u j • x j * u j • x j) = w j • (x j * x j)

Tactic:
rw [smul_mul_smul, Units.smul_def, smul_smul, ← pow_two, ← h]

Premises used: pow_two, smul_mul_smul, smul_smul, Units.smul_def