awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Signature (goal)
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 Q + sigNeg Q + Module.finrank.{u_4, u_2} 𝕜 ↥(radical (P := 𝕜) Q) = Module.finrank 𝕜 M
have 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
Tactic: rw [e.sigPos_eq, e.sigNeg_eq, e.rank_radical_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Signature (goal)
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) → 𝕜)) =
    Module.finrank 𝕜 M
have h : Module.finrank 𝕜 M = Nat.card (Fin (Module.finrank 𝕜 M))
Tactic: convert! QuadraticForm.sigPos_add_sigNeg_add_radical₁ (w := w)
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Signature (goal)
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 Q = Set.ncard.{u_5} (α := ι) {i : ι | 0 < w i}
have rw : sigPos (R := 𝕜) (M := ι → 𝕜) (weightedSumSquares 𝕜 w) = Set.ncard.{u_5} (α := ι) {i : ι | 0 < w i}
Tactic: rw [hQ.sigPos_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Signature (goal)
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 Q = Set.ncard.{u_5} (α := ι) {i : ι | w i < 0}
have rw : sigNeg (R := 𝕜) (M := ι → 𝕜) (weightedSumSquares 𝕜 w) = Set.ncard.{u_5} (α := ι) {i : ι | w i < 0}
Tactic: rw [hQ.sigNeg_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries (hypothesis)
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₄
⊢ comp (Q₂.tmul Q₄) (TensorProduct.map f.toLinearMap g.toLinearMap) = Q₁.tmul Q₃
have h₁ : Q₁ = comp Q₂ f.toLinearMap
Tactic: have h₁ : Q₁ = Q₂.comp f.toLinearMap := QuadraticMap.ext fun x => (f.map_app x).symm
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries (hypothesis)
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
⊢ comp (Q₂.tmul Q₄) (TensorProduct.map f.toLinearMap g.toLinearMap) = Q₁.tmul Q₃
have h₃ : Q₃ = comp Q₄ g.toLinearMap
Tactic: have h₃ : Q₃ = Q₄.comp g.toLinearMap := QuadraticMap.ext fun x => (g.map_app x).symm
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries (goal)
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₃
have 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)
Tactic: refine (QuadraticMap.associated_rightInverse R).injective ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries (goal)
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₂
have 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)
Tactic: refine (QuadraticMap.associated_rightInverse R).injective ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries (goal)
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 (α := 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)
have a : ∀ (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.comm R M₁ M₂) : M₁ ⊗[R] M₂ →ₗ[R] M₂ ⊗[R] M₁))) :
                                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: ext m₁ m₂ m₁' m₂'
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries (goal)
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₃
have 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)
Tactic: refine (QuadraticMap.associated_rightInverse R).injective ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries (goal)
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
have 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)
Tactic: refine (QuadraticMap.associated_rightInverse R).injective ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries (goal)
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₁
⊢ 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)
have 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)
Tactic: ext m₁ m₁'
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries (goal)
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)
    (((((((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)
have 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)
Tactic: simp only [associated_tmul, QuadraticMap.associated_comp]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries (goal)
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.lid R M₂) : R ⊗[R] M₂ →ₗ[R] M₂) = QuadraticForm.tmul (A := R) (M₁ := R) QuadraticMap.sq Q₂
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.TensorProduct (hypothesis)
Goal:
R : Type uR
A : Type uA
M₁ : Type uM₁
M₂ : Type uM₂
N₁ : Type uN₁
N₂ : Type uN₂
inst : CommRing R
inst_1 : CommRing A
inst_2 : AddCommGroup M₁
inst_3 : AddCommGroup M₂
inst_4 : AddCommGroup N₁
inst_5 : AddCommGroup N₂
inst_6 : Algebra R A
inst_7 : Module R M₁
inst_8 : Module A M₁
inst_9 : Module R N₁
inst_10 : Module A N₁
inst_11 : SMulCommClass R A M₁
inst_12 : IsScalarTower R A M₁
inst_13 : IsScalarTower R A N₁
inst_14 : Module R M₂
inst_15 : Module R N₂
inst_16 : Invertible (α := R) 2
inst_17 : Invertible (α := A) 2
Q₁ : QuadraticMap A M₁ N₁
Q₂ : QuadraticMap R M₂ N₂
this : Invertible (α := A) 2 :=
  Invertible.copy (r := (algebraMap R A : (a : R) → A) 2) (Invertible.map (algebraMap R A) 2) 2 ⋯
⊢ Eq (α := BilinMap A (M₁ ⊗[R] M₂) (N₁ ⊗[R] N₂))
    ((associated : (a : QuadraticMap A (M₁ ⊗[R] M₂) (N₁ ⊗[R] N₂)) → BilinMap A (M₁ ⊗[R] M₂) (N₁ ⊗[R] N₂))
        (((tensorDistrib R A :
              QuadraticMap A M₁ N₁ ⊗[R] QuadraticMap R M₂ N₂ →ₗ[A] QuadraticMap A (M₁ ⊗[R] M₂) (N₁ ⊗[R] N₂)) :
            (a : QuadraticMap A M₁ N₁ ⊗[R] QuadraticMap R M₂ N₂) → QuadraticMap A (M₁ ⊗[R] M₂) (N₁ ⊗[R] N₂))
          (Q₁ ⊗ₜ[R] Q₂)) :
      BilinMap A (M₁ ⊗[R] M₂) (N₁ ⊗[R] N₂))
    (((BilinMap.tensorDistrib R A : BilinMap A M₁ N₁ ⊗[R] BilinMap R M₂ N₂ →ₗ[A] BilinMap A (M₁ ⊗[R] M₂) (N₁ ⊗[R] N₂)) :
          (a : BilinMap A M₁ N₁ ⊗[R] BilinMap R M₂ N₂) → BilinMap A (M₁ ⊗[R] M₂) (N₁ ⊗[R] N₂))
        ((associated : (a : QuadraticMap A M₁ N₁) → BilinMap A M₁ N₁) Q₁ ⊗ₜ[R]
          (associated : (a : QuadraticMap R M₂ N₂) → BilinMap R M₂ N₂) Q₂) :
      BilinMap A (M₁ ⊗[R] M₂) (N₁ ⊗[R] N₂))
have this₁ : Subsingleton.{uA + 1} (Invertible (α := A) 2)
Tactic: have : Subsingleton (Invertible (2 : A)) := inferInstance
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.TensorProduct (goal)
Goal:
R : Type uR
A : Type uA
M₁ : Type uM₁
M₂ : Type uM₂
inst : CommRing R
inst_1 : CommRing A
inst_2 : AddCommGroup M₁
inst_3 : AddCommGroup M₂
inst_4 : Algebra R A
inst_5 : Module R M₁
inst_6 : Module A M₁
inst_7 : SMulCommClass R A M₁
inst_8 : IsScalarTower R A M₁
inst_9 : Module R M₂
inst_10 : Invertible (α := R) 2
inst_11 : Invertible (α := A) 2
Q₁ : QuadraticForm A M₁
Q₂ : QuadraticForm R M₂
⊢ Eq (α := BilinMap A (M₁ ⊗[R] M₂) A)
    (((associated (R := A) (M := M₁ ⊗[R] M₂) (N := A) : QuadraticMap A (M₁ ⊗[R] M₂) A →ₗ[A] BilinMap A (M₁ ⊗[R] M₂) A) :
          (a : QuadraticMap A (M₁ ⊗[R] M₂) A) → BilinMap A (M₁ ⊗[R] M₂) A)
        (Q₁.tmul Q₂) :
      BilinMap A (M₁ ⊗[R] M₂) A)
    (BilinForm.tmul
        (((associated.{uA, uM₁, uA} (R := A) (M := M₁) (N := A) : QuadraticMap A M₁ A →ₗ[A] BilinMap A M₁ A) :
            (a : QuadraticMap A M₁ A) → BilinMap A M₁ A)
          Q₁)
        (((associated.{uR, uM₂, uR} (R := R) (M := M₂) (N := R) : QuadraticMap R M₂ R →ₗ[R] BilinMap R M₂ R) :
            (a : QuadraticMap R M₂ R) → BilinMap R M₂ R)
          Q₂) :
      BilinMap A (M₁ ⊗[R] M₂) A)
have rw : Eq (α := BilinMap A (M₁ ⊗[R] M₂) A)
  (((associated (R := A) (M := M₁ ⊗[R] M₂) (N := A) : QuadraticMap A (M₁ ⊗[R] M₂) A →ₗ[A] BilinMap A (M₁ ⊗[R] M₂) A) :
        (a : QuadraticMap A (M₁ ⊗[R] M₂) A) → BilinMap A (M₁ ⊗[R] M₂) A)
      (Q₁.tmul Q₂) :
    BilinMap A (M₁ ⊗[R] M₂) A)
  ((((↑(LinearEquiv.congrRight₂ (AlgebraTensorModule.rid R A A)) :
            BilinMap A (M₁ ⊗[R] M₂) (A ⊗[R] R) →ₗ[A] BilinMap A (M₁ ⊗[R] M₂) A) :
          BilinMap A (M₁ ⊗[R] M₂) (A ⊗[R] R) →ₗ[A] BilinMap A (M₁ ⊗[R] M₂) A) :
        (a : BilinMap A (M₁ ⊗[R] M₂) (A ⊗[R] R)) → BilinForm A (M₁ ⊗[R] M₂))
      ((associated : (a : QuadraticMap A (M₁ ⊗[R] M₂) (A ⊗[R] R)) → BilinMap A (M₁ ⊗[R] M₂) (A ⊗[R] R))
        (QuadraticMap.tmul.{uR, uA, uM₁, uM₂, uA, uR} (R := R) (A := A) (M₁ := M₁) (M₂ := M₂) (N₁ := A) (N₂ := R) Q₁
          Q₂)) :
    BilinForm A (M₁ ⊗[R] M₂))
Tactic: rw [BilinForm.tmul, BilinForm.tensorDistrib, LinearMap.comp_apply, ← BilinMap.tmul,
    ← QuadraticMap.associated_tmul Q₁ Q₂]