awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Signature
Goal:
M : Type u_2
inst : AddCommGroup M
𝕜 : Type u_4
inst_1 : Field 𝕜
inst_2 : LinearOrder 𝕜
inst_3 : Module 𝕜 M
Q : QuadraticForm 𝕜 M
inst_4 : IsStrictOrderedRing 𝕜
inst_5 : FiniteDimensional 𝕜 M
have :
  ∀ (this : Invertible (α := 𝕜) 2),
    sigPos Q + sigNeg Q + Module.finrank.{u_4, u_2} 𝕜 ↥(radical (P := 𝕜) Q) = Module.finrank 𝕜 M
⊢ sigPos Q + sigNeg Q + Module.finrank.{u_4, u_2} 𝕜 ↥(radical (P := 𝕜) Q) = Module.finrank 𝕜 M

Tactic:
have : Invertible (2 : 𝕜) := invertibleOfNonzero (NeZero.ne _)
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Signature
Goal:
M : Type u_2
inst : AddCommGroup M
𝕜 : Type u_4
inst_1 : Field 𝕜
inst_2 : LinearOrder 𝕜
inst_3 : Module 𝕜 M
Q : QuadraticForm 𝕜 M
inst_4 : IsStrictOrderedRing 𝕜
inst_5 : FiniteDimensional 𝕜 M
this : Invertible (α := 𝕜) 2
obtain :
  ∀ (w : Fin (Module.finrank 𝕜 M) → 𝕜) (e : Equivalent Q (weightedSumSquares 𝕜 w)),
    sigPos Q + sigNeg Q + Module.finrank.{u_4, u_2} 𝕜 ↥(radical (P := 𝕜) Q) = Module.finrank 𝕜 M
⊢ sigPos Q + sigNeg Q + Module.finrank.{u_4, u_2} 𝕜 ↥(radical (P := 𝕜) Q) = Module.finrank 𝕜 M

Tactic:
obtain ⟨w, e⟩ := Q.equivalent_weightedSumSquares

Premises used: QuadraticForm.equivalent_weightedSumSquares
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Signature
Goal:
M : Type u_2
inst : AddCommGroup M
𝕜 : Type u_4
inst_1 : Field 𝕜
inst_2 : LinearOrder 𝕜
inst_3 : Module 𝕜 M
Q : QuadraticForm 𝕜 M
inst_4 : IsStrictOrderedRing 𝕜
inst_5 : FiniteDimensional 𝕜 M
this : Invertible (α := 𝕜) 2
w : Fin (Module.finrank 𝕜 M) → 𝕜
e : Equivalent Q (weightedSumSquares 𝕜 w)
rw :
  sigPos.{u_4, u_4} (R := 𝕜) (M := Fin (Module.finrank 𝕜 M) → 𝕜) (weightedSumSquares 𝕜 w) +
        sigNeg.{u_4, u_4} (R := 𝕜) (M := Fin (Module.finrank 𝕜 M) → 𝕜) (weightedSumSquares 𝕜 w) +
      Module.finrank 𝕜
        ↥(radical.{u_4, u_4, u_4} (R := 𝕜) (M := Fin (Module.finrank 𝕜 M) → 𝕜) (P := 𝕜) (weightedSumSquares 𝕜 w) :
            Submodule 𝕜 (Fin (Module.finrank 𝕜 M) → 𝕜)) =
    Module.finrank 𝕜 M
⊢ sigPos Q + sigNeg Q + Module.finrank.{u_4, u_2} 𝕜 ↥(radical (P := 𝕜) Q) = Module.finrank 𝕜 M

Tactic:
rw [e.sigPos_eq, e.sigNeg_eq, e.rank_radical_eq]

Premises used: QuadraticMap.Equivalent.sigPos_eq, QuadraticMap.Equivalent.sigNeg_eq, QuadraticMap.Equivalent.rank_radical_eq
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Signature
Goal:
M : Type u_2
inst : AddCommGroup M
𝕜 : Type u_4
inst_1 : Field 𝕜
inst_2 : LinearOrder 𝕜
inst_3 : Module 𝕜 M
Q : QuadraticForm 𝕜 M
inst_4 : IsStrictOrderedRing 𝕜
inst_5 : FiniteDimensional 𝕜 M
this : Invertible (α := 𝕜) 2
w : Fin (Module.finrank 𝕜 M) → 𝕜
e : Equivalent Q (weightedSumSquares 𝕜 w)
⊢ sigPos.{u_4, u_4} (R := 𝕜) (M := Fin (Module.finrank 𝕜 M) → 𝕜) (weightedSumSquares 𝕜 w) +
        sigNeg.{u_4, u_4} (R := 𝕜) (M := Fin (Module.finrank 𝕜 M) → 𝕜) (weightedSumSquares 𝕜 w) +
      Module.finrank 𝕜
        ↥(radical.{u_4, u_4, u_4} (R := 𝕜) (M := Fin (Module.finrank 𝕜 M) → 𝕜) (P := 𝕜) (weightedSumSquares 𝕜 w) :
            Submodule 𝕜 (Fin (Module.finrank 𝕜 M) → 𝕜)) =
    Nat.card (Fin (Module.finrank 𝕜 M))

Tactic:
QuadraticForm.sigPos_add_sigNeg_add_radical₁ (w := w)

Premises used: _private.0.QuadraticForm.sigPos_add_sigNeg_add_radical₁
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Signature
Goal:
M : Type u_2
inst : AddCommGroup M
𝕜 : Type u_4
inst_1 : Field 𝕜
inst_2 : LinearOrder 𝕜
inst_3 : Module 𝕜 M
Q : QuadraticForm 𝕜 M
inst_4 : IsStrictOrderedRing 𝕜
inst_5 : FiniteDimensional 𝕜 M
this : Invertible (α := 𝕜) 2
w : Fin (Module.finrank 𝕜 M) → 𝕜
e : Equivalent Q (weightedSumSquares 𝕜 w)
h : Module.finrank 𝕜 M = Nat.card (Fin (Module.finrank 𝕜 M))
⊢ sigPos.{u_4, u_4} (R := 𝕜) (M := Fin (Module.finrank 𝕜 M) → 𝕜) (weightedSumSquares 𝕜 w) +
        sigNeg.{u_4, u_4} (R := 𝕜) (M := Fin (Module.finrank 𝕜 M) → 𝕜) (weightedSumSquares 𝕜 w) +
      Module.finrank 𝕜
        ↥(radical.{u_4, u_4, u_4} (R := 𝕜) (M := Fin (Module.finrank 𝕜 M) → 𝕜) (P := 𝕜) (weightedSumSquares 𝕜 w) :
            Submodule 𝕜 (Fin (Module.finrank 𝕜 M) → 𝕜)) =
    Module.finrank 𝕜 M

Tactic:
convert! QuadraticForm.sigPos_add_sigNeg_add_radical₁ (w := w)

Premises used: _private.0.QuadraticForm.sigPos_add_sigNeg_add_radical₁
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Signature
Goal:
M : Type u_2
inst : AddCommGroup M
𝕜 : Type u_4
inst_1 : Field 𝕜
inst_2 : LinearOrder 𝕜
inst_3 : Module 𝕜 M
Q : QuadraticForm 𝕜 M
inst_4 : IsStrictOrderedRing 𝕜
inst_5 : FiniteDimensional 𝕜 M
this : Invertible (α := 𝕜) 2
w : Fin (Module.finrank 𝕜 M) → 𝕜
e : Equivalent Q (weightedSumSquares 𝕜 w)
⊢ Module.finrank 𝕜 M = Nat.card (Fin (Module.finrank 𝕜 M))

Tactic:
Eq.symm (Nat.card_fin (Module.finrank 𝕜 M))

Premises used: Eq.symm, Nat.card_fin, Module.finrank
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Signature
Goal:
M : Type u_2
inst : AddCommGroup M
𝕜 : Type u_4
inst_1 : Field 𝕜
inst_2 : LinearOrder 𝕜
inst_3 : Module 𝕜 M
Q : QuadraticForm 𝕜 M
inst_4 : IsStrictOrderedRing 𝕜
inst_5 : FiniteDimensional 𝕜 M
this : Invertible (α := 𝕜) 2
w : Fin (Module.finrank 𝕜 M) → 𝕜
e : Equivalent Q (weightedSumSquares 𝕜 w)
⊢ Module.finrank 𝕜 M = Nat.card (Fin (Module.finrank 𝕜 M))

Tactic:
exact Eq.symm (Nat.card_fin (Module.finrank 𝕜 M))

Premises used: Eq.symm, Nat.card_fin, Module.finrank
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Signature
Goal:
M : Type u_2
inst : AddCommGroup M
𝕜 : Type u_4
inst_1 : Field 𝕜
inst_2 : LinearOrder 𝕜
inst_3 : Module 𝕜 M
Q : QuadraticForm 𝕜 M
ι : Type u_5
inst_4 : Fintype ι
w : ι → 𝕜
inst_5 : IsStrictOrderedRing 𝕜
hQ : Equivalent Q (weightedSumSquares 𝕜 w)
rw : sigPos (R := 𝕜) (M := ι → 𝕜) (weightedSumSquares 𝕜 w) = Set.ncard.{u_5} (α := ι) {i : ι | 0 < w i}
⊢ sigPos Q = Set.ncard.{u_5} (α := ι) {i : ι | 0 < w i}

Tactic:
rw [hQ.sigPos_eq]

Premises used: QuadraticMap.Equivalent.sigPos_eq
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Signature
Goal:
M : Type u_2
inst : AddCommGroup M
𝕜 : Type u_4
inst_1 : Field 𝕜
inst_2 : LinearOrder 𝕜
inst_3 : Module 𝕜 M
Q : QuadraticForm 𝕜 M
ι : Type u_5
inst_4 : Fintype ι
w : ι → 𝕜
inst_5 : IsStrictOrderedRing 𝕜
hQ : Equivalent Q (weightedSumSquares 𝕜 w)
⊢ sigPos (R := 𝕜) (M := ι → 𝕜) (weightedSumSquares 𝕜 w) = Set.ncard.{u_5} (α := ι) {i : ι | 0 < w i}

Tactic:
sigPos_weightedSumSquares

Premises used: QuadraticForm.sigPos_weightedSumSquares
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Signature
Goal:
M : Type u_2
inst : AddCommGroup M
𝕜 : Type u_4
inst_1 : Field 𝕜
inst_2 : LinearOrder 𝕜
inst_3 : Module 𝕜 M
Q : QuadraticForm 𝕜 M
ι : Type u_5
inst_4 : Fintype ι
w : ι → 𝕜
inst_5 : IsStrictOrderedRing 𝕜
hQ : Equivalent Q (weightedSumSquares 𝕜 w)
⊢ sigPos (R := 𝕜) (M := ι → 𝕜) (weightedSumSquares 𝕜 w) = Set.ncard.{u_5} (α := ι) {i : ι | 0 < w i}

Tactic:
exact sigPos_weightedSumSquares

Premises used: QuadraticForm.sigPos_weightedSumSquares
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Signature
Goal:
M : Type u_2
inst : AddCommGroup M
𝕜 : Type u_4
inst_1 : Field 𝕜
inst_2 : LinearOrder 𝕜
inst_3 : Module 𝕜 M
Q : QuadraticForm 𝕜 M
ι : Type u_5
inst_4 : Fintype ι
w : ι → 𝕜
inst_5 : IsStrictOrderedRing 𝕜
hQ : Equivalent Q (weightedSumSquares 𝕜 w)
rw : sigNeg (R := 𝕜) (M := ι → 𝕜) (weightedSumSquares 𝕜 w) = Set.ncard.{u_5} (α := ι) {i : ι | w i < 0}
⊢ sigNeg Q = Set.ncard.{u_5} (α := ι) {i : ι | w i < 0}

Tactic:
rw [hQ.sigNeg_eq]

Premises used: QuadraticMap.Equivalent.sigNeg_eq
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Signature
Goal:
M : Type u_2
inst : AddCommGroup M
𝕜 : Type u_4
inst_1 : Field 𝕜
inst_2 : LinearOrder 𝕜
inst_3 : Module 𝕜 M
Q : QuadraticForm 𝕜 M
ι : Type u_5
inst_4 : Fintype ι
w : ι → 𝕜
inst_5 : IsStrictOrderedRing 𝕜
hQ : Equivalent Q (weightedSumSquares 𝕜 w)
⊢ sigNeg (R := 𝕜) (M := ι → 𝕜) (weightedSumSquares 𝕜 w) = Set.ncard.{u_5} (α := ι) {i : ι | w i < 0}

Tactic:
sigNeg_weightedSumSquares

Premises used: QuadraticForm.sigNeg_weightedSumSquares
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Signature
Goal:
M : Type u_2
inst : AddCommGroup M
𝕜 : Type u_4
inst_1 : Field 𝕜
inst_2 : LinearOrder 𝕜
inst_3 : Module 𝕜 M
Q : QuadraticForm 𝕜 M
ι : Type u_5
inst_4 : Fintype ι
w : ι → 𝕜
inst_5 : IsStrictOrderedRing 𝕜
hQ : Equivalent Q (weightedSumSquares 𝕜 w)
⊢ sigNeg (R := 𝕜) (M := ι → 𝕜) (weightedSumSquares 𝕜 w) = Set.ncard.{u_5} (α := ι) {i : ι | w i < 0}

Tactic:
exact sigNeg_weightedSumSquares

Premises used: QuadraticForm.sigNeg_weightedSumSquares
-- Module: Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries
Goal:
R : Type uR
M₁ : Type uM₁
M₂ : Type uM₂
M₃ : Type uM₃
M₄ : Type uM₄
inst : CommRing R
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : AddCommGroup M₃
inst_4 : AddCommGroup M₄
inst_5 : Module R M₁
inst_6 : Module R M₂
inst_7 : Module R M₃
inst_8 : Module R M₄
inst_9 : Invertible (α := R) 2
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
Q₄ : QuadraticForm R M₄
f : Q₁ →qᵢ Q₂
g : Q₃ →qᵢ Q₄
⊢ Q₁ = comp Q₂ f.toLinearMap

Tactic:
have h₁ : Q₁ = Q₂.comp f.toLinearMap := QuadraticMap.ext fun x => (f.map_app x).symm
-- Module: Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries
Goal:
R : Type uR
M₁ : Type uM₁
M₂ : Type uM₂
M₃ : Type uM₃
M₄ : Type uM₄
inst : CommRing R
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : AddCommGroup M₃
inst_4 : AddCommGroup M₄
inst_5 : Module R M₁
inst_6 : Module R M₂
inst_7 : Module R M₃
inst_8 : Module R M₄
inst_9 : Invertible (α := R) 2
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
Q₄ : QuadraticForm R M₄
f : Q₁ →qᵢ Q₂
g : Q₃ →qᵢ Q₄
h₁ : Q₁ = comp Q₂ f.toLinearMap
⊢ Q₃ = comp Q₄ g.toLinearMap

Tactic:
have h₃ : Q₃ = Q₄.comp g.toLinearMap := QuadraticMap.ext fun x => (g.map_app x).symm
-- Module: Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries
Goal:
R : Type uR
M₁ : Type uM₁
M₂ : Type uM₂
M₃ : Type uM₃
M₄ : Type uM₄
inst : CommRing R
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : AddCommGroup M₃
inst_4 : AddCommGroup M₄
inst_5 : Module R M₁
inst_6 : Module R M₂
inst_7 : Module R M₃
inst_8 : Module R M₄
inst_9 : Invertible (α := R) 2
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
Q₄ : QuadraticForm R M₄
f : Q₁ →qᵢ Q₂
g : Q₃ →qᵢ Q₄
h₁ : Q₁ = comp Q₂ f.toLinearMap
h₃ : Q₃ = comp Q₄ g.toLinearMap
⊢ comp (Q₂.tmul Q₄) (TensorProduct.map f.toLinearMap g.toLinearMap) = Q₁.tmul Q₃

Tactic:
(QuadraticMap.associated_rightInverse R).injective ?_

Premises used: QuadraticMap.associated_rightInverse, Function.RightInverse.injective
-- Module: Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries
Goal:
R : Type uR
M₁ : Type uM₁
M₂ : Type uM₂
M₃ : Type uM₃
M₄ : Type uM₄
inst : CommRing R
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : AddCommGroup M₃
inst_4 : AddCommGroup M₄
inst_5 : Module R M₁
inst_6 : Module R M₂
inst_7 : Module R M₃
inst_8 : Module R M₄
inst_9 : Invertible (α := R) 2
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
Q₄ : QuadraticForm R M₄
f : Q₁ →qᵢ Q₂
g : Q₃ →qᵢ Q₄
h₁ : Q₁ = comp Q₂ f.toLinearMap
h₃ : Q₃ = comp Q₄ g.toLinearMap
refine :
  Eq (α := LinearMap.BilinMap R (M₁ ⊗[R] M₃) R)
    (((associatedHom R (R := R) (M := M₁ ⊗[R] M₃) (N := R) :
            QuadraticMap R (M₁ ⊗[R] M₃) R →ₗ[R] LinearMap.BilinMap R (M₁ ⊗[R] M₃) R) :
          (a : QuadraticMap R (M₁ ⊗[R] M₃) R) → LinearMap.BilinMap R (M₁ ⊗[R] M₃) R)
        (comp (Q₂.tmul Q₄) (TensorProduct.map f.toLinearMap g.toLinearMap)) :
      LinearMap.BilinMap R (M₁ ⊗[R] M₃) R)
    (((associatedHom R (R := R) (M := M₁ ⊗[R] M₃) (N := R) :
            QuadraticMap R (M₁ ⊗[R] M₃) R →ₗ[R] LinearMap.BilinMap R (M₁ ⊗[R] M₃) R) :
          (a : QuadraticMap R (M₁ ⊗[R] M₃) R) → LinearMap.BilinMap R (M₁ ⊗[R] M₃) R)
        (Q₁.tmul Q₃) :
      LinearMap.BilinMap R (M₁ ⊗[R] M₃) R)
⊢ comp (Q₂.tmul Q₄) (TensorProduct.map f.toLinearMap g.toLinearMap) = Q₁.tmul Q₃

Tactic:
refine (QuadraticMap.associated_rightInverse R).injective ?_

Premises used: QuadraticMap.associated_rightInverse, Function.RightInverse.injective
-- Module: Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries
Goal:
R : Type uR
M₁ : Type uM₁
M₂ : Type uM₂
M₃ : Type uM₃
M₄ : Type uM₄
inst : CommRing R
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : AddCommGroup M₃
inst_4 : AddCommGroup M₄
inst_5 : Module R M₁
inst_6 : Module R M₂
inst_7 : Module R M₃
inst_8 : Module R M₄
inst_9 : Invertible (α := R) 2
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
Q₄ : QuadraticForm R M₄
f : Q₁ →qᵢ Q₂
g : Q₃ →qᵢ Q₄
h₁ : Q₁ = comp Q₂ f.toLinearMap
h₃ : Q₃ = comp Q₄ g.toLinearMap
m₁ : M₁
m₃ : M₃
m₁' : M₁
m₃' : M₃
⊢ Eq.{uR + 1} (α := R)
    (((((TensorProduct.AlgebraTensorModule.curry
                    (((((TensorProduct.AlgebraTensorModule.curry
                                  (((associatedHom R (R := R) (M := M₁ ⊗[R] M₃) (N := R) :
                                        QuadraticMap R (M₁ ⊗[R] M₃) R →ₗ[R] LinearMap.BilinMap R (M₁ ⊗[R] M₃) R) :
                                      (a : QuadraticMap R (M₁ ⊗[R] M₃) R) → LinearMap.BilinMap R (M₁ ⊗[R] M₃) R)
                                    (comp (Q₂.tmul Q₄) (TensorProduct.map f.toLinearMap g.toLinearMap))) :
                                M₁ →ₗ[R] M₃ →ₗ[R] M₁ ⊗[R] M₃ →ₗ[R] R) :
                              (a : M₁) → M₃ →ₗ[R] M₁ ⊗[R] M₃ →ₗ[R] R)
                            m₁ :
                          M₃ →ₗ[R] M₁ ⊗[R] M₃ →ₗ[R] R) :
                        (a : M₃) → M₁ ⊗[R] M₃ →ₗ[R] R)
                      m₃) :
                  M₁ →ₗ[R] M₃ →ₗ[R] R) :
                (a : M₁) → M₃ →ₗ[R] R)
              m₁' :
            M₃ →ₗ[R] R) :
          (a : M₃) → R)
        m₃' :
      R)
    (((((TensorProduct.AlgebraTensorModule.curry
                    (((((TensorProduct.AlgebraTensorModule.curry
                                  (((associatedHom R (R := R) (M := M₁ ⊗[R] M₃) (N := R) :
                                        QuadraticMap R (M₁ ⊗[R] M₃) R →ₗ[R] LinearMap.BilinMap R (M₁ ⊗[R] M₃) R) :
                                      (a : QuadraticMap R (M₁ ⊗[R] M₃) R) → LinearMap.BilinMap R (M₁ ⊗[R] M₃) R)
                                    (Q₁.tmul Q₃)) :
                                M₁ →ₗ[R] M₃ →ₗ[R] M₁ ⊗[R] M₃ →ₗ[R] R) :
                              (a : M₁) → M₃ →ₗ[R] M₁ ⊗[R] M₃ →ₗ[R] R)
                            m₁ :
                          M₃ →ₗ[R] M₁ ⊗[R] M₃ →ₗ[R] R) :
                        (a : M₃) → M₁ ⊗[R] M₃ →ₗ[R] R)
                      m₃) :
                  M₁ →ₗ[R] M₃ →ₗ[R] R) :
                (a : M₁) → M₃ →ₗ[R] R)
              m₁' :
            M₃ →ₗ[R] R) :
          (a : M₃) → R)
        m₃' :
      R)

Tactic:
simp [-associated_apply, h₁, h₃, associated_tmul]

Premises used: QuadraticMap.associated_apply, QuadraticForm.associated_tmul
-- Module: Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries
Goal:
R : Type uR
M₁ : Type uM₁
M₂ : Type uM₂
M₃ : Type uM₃
M₄ : Type uM₄
inst : CommRing R
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : AddCommGroup M₃
inst_4 : AddCommGroup M₄
inst_5 : Module R M₁
inst_6 : Module R M₂
inst_7 : Module R M₃
inst_8 : Module R M₄
inst_9 : Invertible (α := R) 2
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
Q₄ : QuadraticForm R M₄
f : Q₁ →qᵢ Q₂
g : Q₃ →qᵢ Q₄
x : M₁ ⊗[R] M₃
⊢ Eq.{uR + 1} (α := R)
    ((Q₂.tmul Q₄ : (a : M₂ ⊗[R] M₄) → R)
        ((TensorProduct.map f.toLinearMap g.toLinearMap : (a : M₁ ⊗[R] M₃) → M₂ ⊗[R] M₄) x : M₂ ⊗[R] M₄) :
      R)
    ((Q₁.tmul Q₃ : (a : M₁ ⊗[R] M₃) → R) x : R)

Tactic:
DFunLike.congr_fun (tmul_comp_tensorMap f g) x

Premises used: DFunLike.congr_fun, Quotient.liftOn', AddCon.liftOn, QuadraticForm.tmul_comp_tensorMap
-- Module: Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries
Goal:
R : Type uR
M₁ : Type uM₁
M₂ : Type uM₂
M₃ : Type uM₃
M₄ : Type uM₄
inst : CommRing R
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : AddCommGroup M₃
inst_4 : AddCommGroup M₄
inst_5 : Module R M₁
inst_6 : Module R M₂
inst_7 : Module R M₃
inst_8 : Module R M₄
inst_9 : Invertible (α := R) 2
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
Q₄ : QuadraticForm R M₄
f : Q₁ →qᵢ Q₂
g : Q₃ →qᵢ Q₄
x : M₁ ⊗[R] M₃
⊢ Eq (α := M₂ ⊗[R] M₄) ((f.tmul g : (a : M₁ ⊗[R] M₃) → M₂ ⊗[R] M₄) x : M₂ ⊗[R] M₄)
    ((TensorProduct.map f.toLinearMap g.toLinearMap : (a : M₁ ⊗[R] M₃) → M₂ ⊗[R] M₄) x : M₂ ⊗[R] M₄)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries
Goal:
R : Type uR
M₁ : Type uM₁
M₂ : Type uM₂
inst : CommRing R
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : Module R M₁
inst_4 : Module R M₂
inst_5 : Invertible (α := R) 2
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
⊢ comp (Q₂.tmul Q₁) (↑(TensorProduct.comm R M₁ M₂) : M₁ ⊗[R] M₂ →ₗ[R] M₂ ⊗[R] M₁) = Q₁.tmul Q₂

Tactic:
(QuadraticMap.associated_rightInverse R).injective ?_

Premises used: QuadraticMap.associated_rightInverse, Function.RightInverse.injective
-- Module: Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries
Goal:
R : Type uR
M₁ : Type uM₁
M₂ : Type uM₂
inst : CommRing R
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : Module R M₁
inst_4 : Module R M₂
inst_5 : Invertible (α := R) 2
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
refine :
  Eq (α := LinearMap.BilinMap R (M₁ ⊗[R] M₂) R)
    (((associatedHom R (R := R) (M := M₁ ⊗[R] M₂) (N := R) :
            QuadraticMap R (M₁ ⊗[R] M₂) R →ₗ[R] LinearMap.BilinMap R (M₁ ⊗[R] M₂) R) :
          (a : QuadraticMap R (M₁ ⊗[R] M₂) R) → LinearMap.BilinMap R (M₁ ⊗[R] M₂) R)
        (comp (Q₂.tmul Q₁) (↑(TensorProduct.comm R M₁ M₂) : M₁ ⊗[R] M₂ →ₗ[R] M₂ ⊗[R] M₁)) :
      LinearMap.BilinMap R (M₁ ⊗[R] M₂) R)
    (((associatedHom R (R := R) (M := M₁ ⊗[R] M₂) (N := R) :
            QuadraticMap R (M₁ ⊗[R] M₂) R →ₗ[R] LinearMap.BilinMap R (M₁ ⊗[R] M₂) R) :
          (a : QuadraticMap R (M₁ ⊗[R] M₂) R) → LinearMap.BilinMap R (M₁ ⊗[R] M₂) R)
        (Q₁.tmul Q₂) :
      LinearMap.BilinMap R (M₁ ⊗[R] M₂) R)
⊢ comp (Q₂.tmul Q₁) (↑(TensorProduct.comm R M₁ M₂) : M₁ ⊗[R] M₂ →ₗ[R] M₂ ⊗[R] M₁) = Q₁.tmul Q₂

Tactic:
refine (QuadraticMap.associated_rightInverse R).injective ?_

Premises used: QuadraticMap.associated_rightInverse, Function.RightInverse.injective
-- Module: Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries
Goal:
R : Type uR
M₁ : Type uM₁
M₂ : Type uM₂
inst : CommRing R
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : Module R M₁
inst_4 : Module R M₂
inst_5 : Invertible (α := R) 2
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
m₁ : M₁
m₂ : M₂
m₁' : M₁
m₂' : M₂
⊢ Eq.{uR + 1} (α := R)
    ((((LinearMap.compl₁₂
                  (LinearMap.BilinForm.tmul
                    (((associated.{uR, uM₂, uR} (R := R) (M := M₂) (N := R) :
                          QuadraticMap R M₂ R →ₗ[R] LinearMap.BilinMap R M₂ R) :
                        (a : QuadraticMap R M₂ R) → LinearMap.BilinMap R M₂ R)
                      Q₂)
                    (((associated.{uR, uM₁, uR} (R := R) (M := M₁) (N := R) :
                          QuadraticMap R M₁ R →ₗ[R] LinearMap.BilinMap R M₁ R) :
                        (a : QuadraticMap R M₁ R) → LinearMap.BilinMap R M₁ R)
                      Q₁))
                  (↑(TensorProduct.comm R M₁ M₂) : M₁ ⊗[R] M₂ →ₗ[R] M₂ ⊗[R] M₁)
                  (↑(TensorProduct.comm R M₁ M₂) : M₁ ⊗[R] M₂ →ₗ[R] M₂ ⊗[R] M₁) :
                (a : M₁ ⊗[R] M₂) → M₁ ⊗[R] M₂ →ₗ[R] R)
              (m₁ ⊗ₜ[R] m₂) :
            M₁ ⊗[R] M₂ →ₗ[R] R) :
          (a : M₁ ⊗[R] M₂) → R)
        (m₁' ⊗ₜ[R] m₂') :
      R)
    ((((LinearMap.BilinForm.tmul
                  (((associated.{uR, uM₁, uR} (R := R) (M := M₁) (N := R) :
                        QuadraticMap R M₁ R →ₗ[R] LinearMap.BilinMap R M₁ R) :
                      (a : QuadraticMap R M₁ R) → LinearMap.BilinMap R M₁ R)
                    Q₁)
                  (((associated.{uR, uM₂, uR} (R := R) (M := M₂) (N := R) :
                        QuadraticMap R M₂ R →ₗ[R] LinearMap.BilinMap R M₂ R) :
                      (a : QuadraticMap R M₂ R) → LinearMap.BilinMap R M₂ R)
                    Q₂) :
                (a : M₁ ⊗[R] M₂) → M₁ ⊗[R] M₂ →ₗ[R] R)
              (m₁ ⊗ₜ[R] m₂) :
            M₁ ⊗[R] M₂ →ₗ[R] R) :
          (a : M₁ ⊗[R] M₂) → R)
        (m₁' ⊗ₜ[R] m₂') :
      R)

Tactic:
mul_comm _ _

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, mul_comm, FreeAddMonoid.sumAux
-- Module: Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries
Goal:
R : Type uR
M₁ : Type uM₁
M₂ : Type uM₂
inst : CommRing R
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : Module R M₁
inst_4 : Module R M₂
inst_5 : Invertible (α := R) 2
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
m₁ : M₁
m₂ : M₂
m₁' : M₁
m₂' : M₂
⊢ Eq.{uR + 1} (α := R)
    ((((LinearMap.compl₁₂
                  (LinearMap.BilinForm.tmul
                    (((associated.{uR, uM₂, uR} (R := R) (M := M₂) (N := R) :
                          QuadraticMap R M₂ R →ₗ[R] LinearMap.BilinMap R M₂ R) :
                        (a : QuadraticMap R M₂ R) → LinearMap.BilinMap R M₂ R)
                      Q₂)
                    (((associated.{uR, uM₁, uR} (R := R) (M := M₁) (N := R) :
                          QuadraticMap R M₁ R →ₗ[R] LinearMap.BilinMap R M₁ R) :
                        (a : QuadraticMap R M₁ R) → LinearMap.BilinMap R M₁ R)
                      Q₁))
                  (↑(TensorProduct.comm R M₁ M₂) : M₁ ⊗[R] M₂ →ₗ[R] M₂ ⊗[R] M₁)
                  (↑(TensorProduct.comm R M₁ M₂) : M₁ ⊗[R] M₂ →ₗ[R] M₂ ⊗[R] M₁) :
                (a : M₁ ⊗[R] M₂) → M₁ ⊗[R] M₂ →ₗ[R] R)
              (m₁ ⊗ₜ[R] m₂) :
            M₁ ⊗[R] M₂ →ₗ[R] R) :
          (a : M₁ ⊗[R] M₂) → R)
        (m₁' ⊗ₜ[R] m₂') :
      R)
    ((((LinearMap.BilinForm.tmul
                  (((associated.{uR, uM₁, uR} (R := R) (M := M₁) (N := R) :
                        QuadraticMap R M₁ R →ₗ[R] LinearMap.BilinMap R M₁ R) :
                      (a : QuadraticMap R M₁ R) → LinearMap.BilinMap R M₁ R)
                    Q₁)
                  (((associated.{uR, uM₂, uR} (R := R) (M := M₂) (N := R) :
                        QuadraticMap R M₂ R →ₗ[R] LinearMap.BilinMap R M₂ R) :
                      (a : QuadraticMap R M₂ R) → LinearMap.BilinMap R M₂ R)
                    Q₂) :
                (a : M₁ ⊗[R] M₂) → M₁ ⊗[R] M₂ →ₗ[R] R)
              (m₁ ⊗ₜ[R] m₂) :
            M₁ ⊗[R] M₂ →ₗ[R] R) :
          (a : M₁ ⊗[R] M₂) → R)
        (m₁' ⊗ₜ[R] m₂') :
      R)

Tactic:
exact mul_comm _ _

Premises used: mul_comm
-- Module: Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries
Goal:
R : Type uR
M₁ : Type uM₁
M₂ : Type uM₂
inst : CommRing R
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : Module R M₁
inst_4 : Module R M₂
inst_5 : Invertible (α := R) 2
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
x : M₁ ⊗[R] M₂
⊢ Eq.{uR + 1} (α := R)
    ((Q₂.tmul Q₁ : (a : M₂ ⊗[R] M₁) → R) ((TensorProduct.comm R M₁ M₂ : (a : M₁ ⊗[R] M₂) → M₂ ⊗[R] M₁) x : M₂ ⊗[R] M₁) :
      R)
    ((Q₁.tmul Q₂ : (a : M₁ ⊗[R] M₂) → R) x : R)

Tactic:
DFunLike.congr_fun (tmul_comp_tensorComm Q₁ Q₂) x

Premises used: DFunLike.congr_fun, Quotient.liftOn', AddCon.liftOn, QuadraticForm.tmul_comp_tensorComm
-- Module: Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries
Goal:
R : Type uR
M₁ : Type uM₁
M₂ : Type uM₂
inst : CommRing R
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : Module R M₁
inst_4 : Module R M₂
inst_5 : Invertible (α := R) 2
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
x : M₁ ⊗[R] M₂
⊢ Eq (α := M₂ ⊗[R] M₁) ((Q₁.tensorComm Q₂ : (a : M₁ ⊗[R] M₂) → M₂ ⊗[R] M₁) x : M₂ ⊗[R] M₁)
    ((TensorProduct.comm R M₁ M₂ : (a : M₁ ⊗[R] M₂) → M₂ ⊗[R] M₁) x : M₂ ⊗[R] M₁)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries
Goal:
R : Type uR
M₁ : Type uM₁
M₂ : Type uM₂
inst : CommRing R
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : Module R M₁
inst_4 : Module R M₂
inst_5 : Invertible (α := R) 2
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
⊢ Eq (α := IsometryEquiv (M₁ := M₂ ⊗[R] M₁) (M₂ := M₁ ⊗[R] M₂) (Q₂.tmul Q₁) (Q₁.tmul Q₂))
    (IsometryEquiv.symm (Q₁.tensorComm Q₂)) (Q₂.tensorComm Q₁)

Tactic:
rfl

Premises used: LinearEquiv.symm, TensorProduct.comm, QuadraticMap.IsometryEquiv.symm, Quotient.liftOn', AddCon.liftOn, LinearEquiv.ofLinear, TensorProduct, QuadraticForm.tensorComm, TensorProduct.lift, rfl