awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries
Goal:
R : Type uR
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 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R M₃
inst_7 : Invertible (α := R) 2
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
⊢ comp (Q₁.tmul (Q₂.tmul Q₃)) (↑(TensorProduct.assoc R M₁ M₂ M₃) : M₁ ⊗[R] M₂ ⊗[R] M₃ →ₗ[R] M₁ ⊗[R] (M₂ ⊗[R] M₃)) =
    QuadraticForm.tmul (Q₁.tmul Q₂) 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₃
inst : CommRing R
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : AddCommGroup M₃
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R M₃
inst_7 : Invertible (α := R) 2
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
refine :
  Eq (α := LinearMap.BilinMap R (M₁ ⊗[R] M₂ ⊗[R] M₃) R)
    (((associatedHom R (R := R) (M := M₁ ⊗[R] M₂ ⊗[R] M₃) (N := R) :
            QuadraticMap R (M₁ ⊗[R] M₂ ⊗[R] M₃) R →ₗ[R] LinearMap.BilinMap R (M₁ ⊗[R] M₂ ⊗[R] M₃) R) :
          (a : QuadraticMap R (M₁ ⊗[R] M₂ ⊗[R] M₃) R) → LinearMap.BilinMap R (M₁ ⊗[R] M₂ ⊗[R] M₃) R)
        (comp (Q₁.tmul (Q₂.tmul Q₃))
          (↑(TensorProduct.assoc R M₁ M₂ M₃) : M₁ ⊗[R] M₂ ⊗[R] M₃ →ₗ[R] M₁ ⊗[R] (M₂ ⊗[R] M₃))) :
      LinearMap.BilinMap R (M₁ ⊗[R] M₂ ⊗[R] M₃) R)
    (((associatedHom R (R := R) (M := M₁ ⊗[R] M₂ ⊗[R] M₃) (N := R) :
            QuadraticMap R (M₁ ⊗[R] M₂ ⊗[R] M₃) R →ₗ[R] LinearMap.BilinMap R (M₁ ⊗[R] M₂ ⊗[R] M₃) R) :
          (a : QuadraticMap R (M₁ ⊗[R] M₂ ⊗[R] M₃) R) → LinearMap.BilinMap R (M₁ ⊗[R] M₂ ⊗[R] M₃) R)
        (QuadraticForm.tmul (Q₁.tmul Q₂) Q₃) :
      LinearMap.BilinMap R (M₁ ⊗[R] M₂ ⊗[R] M₃) R)
⊢ comp (Q₁.tmul (Q₂.tmul Q₃)) (↑(TensorProduct.assoc R M₁ M₂ M₃) : M₁ ⊗[R] M₂ ⊗[R] M₃ →ₗ[R] M₁ ⊗[R] (M₂ ⊗[R] M₃)) =
    QuadraticForm.tmul (Q₁.tmul Q₂) 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₃
inst : CommRing R
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : AddCommGroup M₃
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R M₃
inst_7 : Invertible (α := R) 2
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
m₁ : M₁
m₂ : 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₁)
                    (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.assoc R M₁ M₂ M₃) : M₁ ⊗[R] M₂ ⊗[R] M₃ →ₗ[R] M₁ ⊗[R] (M₂ ⊗[R] M₃))
                  (↑(TensorProduct.assoc R M₁ M₂ M₃) : M₁ ⊗[R] M₂ ⊗[R] M₃ →ₗ[R] M₁ ⊗[R] (M₂ ⊗[R] M₃)) :
                (a : M₁ ⊗[R] M₂ ⊗[R] M₃) → M₁ ⊗[R] M₂ ⊗[R] M₃ →ₗ[R] R)
              (m₁ ⊗ₜ[R] m₂ ⊗ₜ[R] m₁') :
            M₁ ⊗[R] M₂ ⊗[R] M₃ →ₗ[R] R) :
          (a : M₁ ⊗[R] M₂ ⊗[R] M₃) → R)
        (m₂' ⊗ₜ[R] m₁'' ⊗ₜ[R] m₂'') :
      R)
    ((((LinearMap.BilinForm.tmul
                  (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₂))
                  (((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₂ ⊗[R] M₃) → M₁ ⊗[R] M₂ ⊗[R] M₃ →ₗ[R] R)
              (m₁ ⊗ₜ[R] m₂ ⊗ₜ[R] m₁') :
            M₁ ⊗[R] M₂ ⊗[R] M₃ →ₗ[R] R) :
          (a : M₁ ⊗[R] M₂ ⊗[R] M₃) → R)
        (m₂' ⊗ₜ[R] m₁'' ⊗ₜ[R] m₂'') :
      R)

Tactic:
mul_assoc _ _ _

Premises used: Quotient.liftOn', AddCon.liftOn, mul_assoc, List.foldl, FreeAddMonoid.sumAux
-- Module: Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries
Goal:
R : Type uR
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 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R M₃
inst_7 : Invertible (α := R) 2
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
m₁ : M₁
m₂ : 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₁)
                    (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.assoc R M₁ M₂ M₃) : M₁ ⊗[R] M₂ ⊗[R] M₃ →ₗ[R] M₁ ⊗[R] (M₂ ⊗[R] M₃))
                  (↑(TensorProduct.assoc R M₁ M₂ M₃) : M₁ ⊗[R] M₂ ⊗[R] M₃ →ₗ[R] M₁ ⊗[R] (M₂ ⊗[R] M₃)) :
                (a : M₁ ⊗[R] M₂ ⊗[R] M₃) → M₁ ⊗[R] M₂ ⊗[R] M₃ →ₗ[R] R)
              (m₁ ⊗ₜ[R] m₂ ⊗ₜ[R] m₁') :
            M₁ ⊗[R] M₂ ⊗[R] M₃ →ₗ[R] R) :
          (a : M₁ ⊗[R] M₂ ⊗[R] M₃) → R)
        (m₂' ⊗ₜ[R] m₁'' ⊗ₜ[R] m₂'') :
      R)
    ((((LinearMap.BilinForm.tmul
                  (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₂))
                  (((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₂ ⊗[R] M₃) → M₁ ⊗[R] M₂ ⊗[R] M₃ →ₗ[R] R)
              (m₁ ⊗ₜ[R] m₂ ⊗ₜ[R] m₁') :
            M₁ ⊗[R] M₂ ⊗[R] M₃ →ₗ[R] R) :
          (a : M₁ ⊗[R] M₂ ⊗[R] M₃) → R)
        (m₂' ⊗ₜ[R] m₁'' ⊗ₜ[R] m₂'') :
      R)

Tactic:
exact mul_assoc _ _ _

Premises used: mul_assoc
-- Module: Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries
Goal:
R : Type uR
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 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R M₃
inst_7 : Invertible (α := R) 2
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
x : M₁ ⊗[R] M₂ ⊗[R] M₃
⊢ Eq.{uR + 1} (α := R)
    ((Q₁.tmul (Q₂.tmul Q₃) : (a : M₁ ⊗[R] (M₂ ⊗[R] M₃)) → R)
        ((TensorProduct.assoc R M₁ M₂ M₃ : (a : M₁ ⊗[R] M₂ ⊗[R] M₃) → M₁ ⊗[R] (M₂ ⊗[R] M₃)) x : M₁ ⊗[R] (M₂ ⊗[R] M₃)) :
      R)
    ((QuadraticForm.tmul (Q₁.tmul Q₂) Q₃ : (a : M₁ ⊗[R] M₂ ⊗[R] M₃) → R) x : R)

Tactic:
DFunLike.congr_fun (tmul_comp_tensorAssoc Q₁ Q₂ Q₃) x

Premises used: DFunLike.congr_fun, Quotient.liftOn', AddCon.liftOn, QuadraticForm.tmul_comp_tensorAssoc
-- Module: Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries
Goal:
R : Type uR
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 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R M₃
inst_7 : Invertible (α := R) 2
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
x : M₁ ⊗[R] M₂ ⊗[R] M₃
⊢ Eq (α := M₁ ⊗[R] (M₂ ⊗[R] M₃))
    ((Q₁.tensorAssoc Q₂ Q₃ : (a : M₁ ⊗[R] M₂ ⊗[R] M₃) → M₁ ⊗[R] (M₂ ⊗[R] M₃)) x : M₁ ⊗[R] (M₂ ⊗[R] M₃))
    ((TensorProduct.assoc R M₁ M₂ M₃ : (a : M₁ ⊗[R] M₂ ⊗[R] M₃) → M₁ ⊗[R] (M₂ ⊗[R] M₃)) x : M₁ ⊗[R] (M₂ ⊗[R] M₃))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries
Goal:
R : Type uR
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 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R M₃
inst_7 : Invertible (α := R) 2
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
x : M₁ ⊗[R] (M₂ ⊗[R] M₃)
⊢ Eq (α := M₁ ⊗[R] M₂ ⊗[R] M₃)
    ((IsometryEquiv.symm (Q₁.tensorAssoc Q₂ Q₃) : (a : M₁ ⊗[R] (M₂ ⊗[R] M₃)) → M₁ ⊗[R] M₂ ⊗[R] M₃) x :
      M₁ ⊗[R] M₂ ⊗[R] M₃)
    ((LinearEquiv.symm (TensorProduct.assoc R M₁ M₂ M₃) : (a : M₁ ⊗[R] (M₂ ⊗[R] M₃)) → M₁ ⊗[R] M₂ ⊗[R] M₃) x :
      M₁ ⊗[R] M₂ ⊗[R] M₃)

Tactic:
rfl

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

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₁
inst : CommRing R
inst_1 : AddCommGroup M₁
inst_2 : Module R M₁
inst_3 : Invertible (α := R) 2
Q₁ : QuadraticForm R M₁
refine :
  Eq (α := LinearMap.BilinMap R (M₁ ⊗[R] R) R)
    (((associatedHom R (R := R) (M := M₁ ⊗[R] R) (N := R) :
            QuadraticMap R (M₁ ⊗[R] R) R →ₗ[R] LinearMap.BilinMap R (M₁ ⊗[R] R) R) :
          (a : QuadraticMap R (M₁ ⊗[R] R) R) → LinearMap.BilinMap R (M₁ ⊗[R] R) R)
        (comp Q₁ (↑(TensorProduct.rid R M₁) : M₁ ⊗[R] R →ₗ[R] M₁)) :
      LinearMap.BilinMap R (M₁ ⊗[R] R) R)
    (((associatedHom R (R := R) (M := M₁ ⊗[R] R) (N := R) :
            QuadraticMap R (M₁ ⊗[R] R) R →ₗ[R] LinearMap.BilinMap R (M₁ ⊗[R] R) R) :
          (a : QuadraticMap R (M₁ ⊗[R] R) R) → LinearMap.BilinMap R (M₁ ⊗[R] R) R)
        (Q₁.tmul (R := R) (M₂ := R) QuadraticMap.sq) :
      LinearMap.BilinMap R (M₁ ⊗[R] R) R)
⊢ comp Q₁ (↑(TensorProduct.rid R M₁) : M₁ ⊗[R] R →ₗ[R] M₁) = Q₁.tmul (R := R) (M₂ := R) QuadraticMap.sq

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₁
inst : CommRing R
inst_1 : AddCommGroup M₁
inst_2 : Module R M₁
inst_3 : Invertible (α := R) 2
Q₁ : QuadraticForm R M₁
a :
  ∀ (m₁ m₁' : M₁),
    Eq.{uR + 1} (α := R)
      (((((TensorProduct.AlgebraTensorModule.curry
                      (((((TensorProduct.AlgebraTensorModule.curry
                                    (((associatedHom R (R := R) (M := M₁ ⊗[R] R) (N := R) :
                                          QuadraticMap R (M₁ ⊗[R] R) R →ₗ[R] LinearMap.BilinMap R (M₁ ⊗[R] R) R) :
                                        (a : QuadraticMap R (M₁ ⊗[R] R) R) → LinearMap.BilinMap R (M₁ ⊗[R] R) R)
                                      (comp Q₁ (↑(TensorProduct.rid R M₁) : M₁ ⊗[R] R →ₗ[R] M₁))) :
                                  M₁ →ₗ[R] R →ₗ[R] M₁ ⊗[R] R →ₗ[R] R) :
                                (a : M₁) → R →ₗ[R] M₁ ⊗[R] R →ₗ[R] R)
                              m₁ :
                            R →ₗ[R] M₁ ⊗[R] R →ₗ[R] R) :
                          (a : R) → M₁ ⊗[R] R →ₗ[R] R)
                        1) :
                    M₁ →ₗ[R] R →ₗ[R] R) :
                  (a : M₁) → R →ₗ[R] R)
                m₁' :
              R →ₗ[R] R) :
            (a : R) → R)
          1 :
        R)
      (((((TensorProduct.AlgebraTensorModule.curry
                      (((((TensorProduct.AlgebraTensorModule.curry
                                    (((associatedHom R (R := R) (M := M₁ ⊗[R] R) (N := R) :
                                          QuadraticMap R (M₁ ⊗[R] R) R →ₗ[R] LinearMap.BilinMap R (M₁ ⊗[R] R) R) :
                                        (a : QuadraticMap R (M₁ ⊗[R] R) R) → LinearMap.BilinMap R (M₁ ⊗[R] R) R)
                                      (Q₁.tmul (R := R) (M₂ := R) QuadraticMap.sq)) :
                                  M₁ →ₗ[R] R →ₗ[R] M₁ ⊗[R] R →ₗ[R] R) :
                                (a : M₁) → R →ₗ[R] M₁ ⊗[R] R →ₗ[R] R)
                              m₁ :
                            R →ₗ[R] M₁ ⊗[R] R →ₗ[R] R) :
                          (a : R) → M₁ ⊗[R] R →ₗ[R] R)
                        1) :
                    M₁ →ₗ[R] R →ₗ[R] R) :
                  (a : M₁) → R →ₗ[R] R)
                m₁' :
              R →ₗ[R] R) :
            (a : R) → R)
          1 :
        R)
⊢ Eq (α := LinearMap.BilinMap R (M₁ ⊗[R] R) R)
    (((associatedHom R (R := R) (M := M₁ ⊗[R] R) (N := R) :
            QuadraticMap R (M₁ ⊗[R] R) R →ₗ[R] LinearMap.BilinMap R (M₁ ⊗[R] R) R) :
          (a : QuadraticMap R (M₁ ⊗[R] R) R) → LinearMap.BilinMap R (M₁ ⊗[R] R) R)
        (comp Q₁ (↑(TensorProduct.rid R M₁) : M₁ ⊗[R] R →ₗ[R] M₁)) :
      LinearMap.BilinMap R (M₁ ⊗[R] R) R)
    (((associatedHom R (R := R) (M := M₁ ⊗[R] R) (N := R) :
            QuadraticMap R (M₁ ⊗[R] R) R →ₗ[R] LinearMap.BilinMap R (M₁ ⊗[R] R) R) :
          (a : QuadraticMap R (M₁ ⊗[R] R) R) → LinearMap.BilinMap R (M₁ ⊗[R] R) R)
        (Q₁.tmul (R := R) (M₂ := R) QuadraticMap.sq) :
      LinearMap.BilinMap R (M₁ ⊗[R] R) R)

Tactic:
ext m₁ m₁'
-- Module: Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries
Goal:
R : Type uR
M₁ : Type uM₁
inst : CommRing R
inst_1 : AddCommGroup M₁
inst_2 : Module R M₁
inst_3 : Invertible (α := R) 2
Q₁ : QuadraticForm R M₁
m₁ m₁' : M₁
a :
  Eq.{uR + 1} (α := R)
    ((((LinearMap.compl₁₂
                  (((associatedHom.{uR, uR, uM₁, uR} R (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.rid R M₁) : M₁ ⊗[R] R →ₗ[R] M₁) (↑(TensorProduct.rid R M₁) : M₁ ⊗[R] R →ₗ[R] M₁) :
                (a : M₁ ⊗[R] R) → M₁ ⊗[R] R →ₗ[R] R)
              (m₁ ⊗ₜ[R] 1) :
            M₁ ⊗[R] R →ₗ[R] R) :
          (a : M₁ ⊗[R] R) → R)
        (m₁' ⊗ₜ[R] 1) :
      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, uR, uR} (R := R) (M := R) (N := R) :
                        QuadraticMap R R R →ₗ[R] LinearMap.BilinMap R R R) :
                      (a : QuadraticMap R R R) → LinearMap.BilinMap R R R)
                    QuadraticMap.sq) :
                (a : M₁ ⊗[R] R) → M₁ ⊗[R] R →ₗ[R] R)
              (m₁ ⊗ₜ[R] 1) :
            M₁ ⊗[R] R →ₗ[R] R) :
          (a : M₁ ⊗[R] R) → R)
        (m₁' ⊗ₜ[R] 1) :
      R)
⊢ Eq.{uR + 1} (α := R)
    (((((((associatedHom R (R := R) (M := M₁ ⊗[R] R) (N := R) :
                        QuadraticMap R (M₁ ⊗[R] R) R →ₗ[R] LinearMap.BilinMap R (M₁ ⊗[R] R) R) :
                      (a : QuadraticMap R (M₁ ⊗[R] R) R) → LinearMap.BilinMap R (M₁ ⊗[R] R) R)
                    (comp Q₁ (↑(TensorProduct.rid R M₁) : M₁ ⊗[R] R →ₗ[R] M₁)) :
                  LinearMap.BilinMap R (M₁ ⊗[R] R) R) :
                (a : M₁ ⊗[R] R) → M₁ ⊗[R] R →ₗ[R] R)
              (m₁ ⊗ₜ[R] 1) :
            M₁ ⊗[R] R →ₗ[R] R) :
          (a : M₁ ⊗[R] R) → R)
        (m₁' ⊗ₜ[R] 1) :
      R)
    (((((((associatedHom R (R := R) (M := M₁ ⊗[R] R) (N := R) :
                        QuadraticMap R (M₁ ⊗[R] R) R →ₗ[R] LinearMap.BilinMap R (M₁ ⊗[R] R) R) :
                      (a : QuadraticMap R (M₁ ⊗[R] R) R) → LinearMap.BilinMap R (M₁ ⊗[R] R) R)
                    (Q₁.tmul (R := R) (M₂ := R) QuadraticMap.sq) :
                  LinearMap.BilinMap R (M₁ ⊗[R] R) R) :
                (a : M₁ ⊗[R] R) → M₁ ⊗[R] R →ₗ[R] R)
              (m₁ ⊗ₜ[R] 1) :
            M₁ ⊗[R] R →ₗ[R] R) :
          (a : M₁ ⊗[R] R) → R)
        (m₁' ⊗ₜ[R] 1) :
      R)

Tactic:
simp only [associated_tmul, QuadraticMap.associated_comp]

Premises used: QuadraticMap.associated_comp, QuadraticForm.associated_tmul
-- Module: Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries
Goal:
R : Type uR
M₁ : Type uM₁
inst : CommRing R
inst_1 : AddCommGroup M₁
inst_2 : Module R M₁
inst_3 : Invertible (α := R) 2
Q₁ : QuadraticForm R M₁
m₁ m₁' : M₁
⊢ Eq.{uR + 1} (α := R)
    ((((LinearMap.compl₁₂
                  (((associatedHom.{uR, uR, uM₁, uR} R (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.rid R M₁) : M₁ ⊗[R] R →ₗ[R] M₁) (↑(TensorProduct.rid R M₁) : M₁ ⊗[R] R →ₗ[R] M₁) :
                (a : M₁ ⊗[R] R) → M₁ ⊗[R] R →ₗ[R] R)
              (m₁ ⊗ₜ[R] 1) :
            M₁ ⊗[R] R →ₗ[R] R) :
          (a : M₁ ⊗[R] R) → R)
        (m₁' ⊗ₜ[R] 1) :
      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, uR, uR} (R := R) (M := R) (N := R) :
                        QuadraticMap R R R →ₗ[R] LinearMap.BilinMap R R R) :
                      (a : QuadraticMap R R R) → LinearMap.BilinMap R R R)
                    QuadraticMap.sq) :
                (a : M₁ ⊗[R] R) → M₁ ⊗[R] R →ₗ[R] R)
              (m₁ ⊗ₜ[R] 1) :
            M₁ ⊗[R] R →ₗ[R] R) :
          (a : M₁ ⊗[R] R) → R)
        (m₁' ⊗ₜ[R] 1) :
      R)

Tactic:
simp [-associated_apply, one_mul]

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

Tactic:
DFunLike.congr_fun (comp_tensorRId_eq Q₁) x

Premises used: DFunLike.congr_fun, QuadraticForm.comp_tensorRId_eq
-- Module: Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries
Goal:
R : Type uR
M₁ : Type uM₁
inst : CommRing R
inst_1 : AddCommGroup M₁
inst_2 : Module R M₁
inst_3 : Invertible (α := R) 2
Q₁ : QuadraticForm R M₁
x : M₁ ⊗[R] R
⊢ Eq.{uM₁ + 1} (α := M₁) ((Q₁.tensorRId : (a : M₁ ⊗[R] R) → M₁) x : M₁)
    ((TensorProduct.rid R M₁ : (a : M₁ ⊗[R] R) → M₁) x : M₁)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries
Goal:
R : Type uR
M₁ : Type uM₁
inst : CommRing R
inst_1 : AddCommGroup M₁
inst_2 : Module R M₁
inst_3 : Invertible (α := R) 2
Q₁ : QuadraticForm R M₁
x : M₁
⊢ Eq (α := M₁ ⊗[R] R) ((IsometryEquiv.symm Q₁.tensorRId : (a : M₁) → M₁ ⊗[R] R) x : M₁ ⊗[R] R)
    ((LinearEquiv.symm (TensorProduct.rid R M₁) : (a : M₁) → M₁ ⊗[R] R) x : M₁ ⊗[R] R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries
Goal:
R : Type uR
M₂ : Type uM₂
inst : CommRing R
inst_1 : AddCommGroup M₂
inst_2 : Module R M₂
inst_3 : Invertible (α := R) 2
Q₂ : QuadraticForm R M₂
h :
  ∀ (m : M₂),
    Eq.{uR + 1} (α := R)
      ((comp Q₂ (↑(TensorProduct.lid R M₂) : R ⊗[R] M₂ →ₗ[R] M₂) : (a : R ⊗[R] M₂) → R) (1 ⊗ₜ[R] m) : R)
      (((QuadraticForm.tmul (A := R) (M₁ := R) QuadraticMap.sq Q₂ : QuadraticForm R (R ⊗[R] M₂)) : (a : R ⊗[R] M₂) → R)
          (1 ⊗ₜ[R] m) :
        R)
⊢ comp Q₂ (↑(TensorProduct.lid R M₂) : R ⊗[R] M₂ →ₗ[R] M₂) = QuadraticForm.tmul (A := R) (M₁ := R) QuadraticMap.sq Q₂

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries
Goal:
R : Type uR
M₂ : Type uM₂
inst : CommRing R
inst_1 : AddCommGroup M₂
inst_2 : Module R M₂
inst_3 : Invertible (α := R) 2
Q₂ : QuadraticForm R M₂
m : M₂
⊢ Eq.{uR + 1} (α := R)
    ((comp Q₂ (↑(TensorProduct.lid R M₂) : R ⊗[R] M₂ →ₗ[R] M₂) : (a : R ⊗[R] M₂) → R) (1 ⊗ₜ[R] m) : R)
    (((QuadraticForm.tmul (A := R) (M₁ := R) QuadraticMap.sq Q₂ : QuadraticForm R (R ⊗[R] M₂)) : (a : R ⊗[R] M₂) → R)
        (1 ⊗ₜ[R] m) :
      R)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries
Goal:
R : Type uR
M₂ : Type uM₂
inst : CommRing R
inst_1 : AddCommGroup M₂
inst_2 : Module R M₂
inst_3 : Invertible (α := R) 2
Q₂ : QuadraticForm R M₂
x : R ⊗[R] M₂
⊢ Eq.{uR + 1} (α := R) ((Q₂ : (a : M₂) → R) ((TensorProduct.lid R M₂ : (a : R ⊗[R] M₂) → M₂) x : M₂) : R)
    (((QuadraticForm.tmul (A := R) (M₁ := R) QuadraticMap.sq Q₂ : QuadraticForm R (R ⊗[R] M₂)) : (a : R ⊗[R] M₂) → R)
        x :
      R)

Tactic:
DFunLike.congr_fun (comp_tensorLId_eq Q₂) x

Premises used: DFunLike.congr_fun, QuadraticForm.comp_tensorLId_eq
-- Module: Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries
Goal:
R : Type uR
M₂ : Type uM₂
inst : CommRing R
inst_1 : AddCommGroup M₂
inst_2 : Module R M₂
inst_3 : Invertible (α := R) 2
Q₂ : QuadraticForm R M₂
x : R ⊗[R] M₂
⊢ Eq.{uM₂ + 1} (α := M₂) ((Q₂.tensorLId : (a : R ⊗[R] M₂) → M₂) x : M₂)
    ((TensorProduct.lid R M₂ : (a : R ⊗[R] M₂) → M₂) x : M₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries
Goal:
R : Type uR
M₂ : Type uM₂
inst : CommRing R
inst_1 : AddCommGroup M₂
inst_2 : Module R M₂
inst_3 : Invertible (α := R) 2
Q₂ : QuadraticForm R M₂
x : M₂
⊢ Eq (α := R ⊗[R] M₂) ((IsometryEquiv.symm Q₂.tensorLId : (a : M₂) → R ⊗[R] M₂) x : R ⊗[R] M₂)
    ((LinearEquiv.symm (TensorProduct.lid R M₂) : (a : M₂) → R ⊗[R] M₂) x : R ⊗[R] M₂)

Tactic:
rfl

Premises used: rfl