awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₂
⊢ polarBilin (R := A) (M := M₁ ⊗[R] M₂) (N := A) (Q₁.tmul Q₂) =
    HSMul.hSMul (α := A) (β := BilinMap A (M₁ ⊗[R] M₂) A) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
      (BilinForm.tmul (polarBilin.{uA, uM₁, uA} (R := A) (M := M₁) (N := A) Q₁)
        (polarBilin.{uR, uM₂, uR} (R := R) (M := M₂) (N := R) Q₂))
have simp_rw : HSMul.hSMul (α := ℕ) (β := BilinMap A (M₁ ⊗[R] M₂) A) 2
    (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₂)) =
  HSMul.hSMul (α := A) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
    (HSMul.hSMul (α := ℕ) 2
      (HSMul.hSMul (α := ℕ) (β := BilinForm A (M₁ ⊗[R] M₂)) 2
        ((BilinForm.tensorDistrib R A : (a : BilinForm A M₁ ⊗[R] BilinForm R M₂) → BilinForm A (M₁ ⊗[R] M₂))
            (((associatedHom.{uA, uA, uM₁, uA} A (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₁ ⊗ₜ[R]
              ((associatedHom.{uR, uR, uM₂, uR} R (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₂) :
          BilinForm A (M₁ ⊗[R] M₂))))
Tactic: simp_rw [← two_nsmul_associated A, ← two_nsmul_associated R, BilinForm.tmul, tmul_smul,
    ← smul_tmul', map_nsmul, associated_tmul]
-- 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₂
⊢ HSMul.hSMul (α := ℕ) (β := BilinMap A (M₁ ⊗[R] M₂) A) 2
      (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₂)) =
    HSMul.hSMul (α := A) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
      (HSMul.hSMul (α := ℕ) 2
        (HSMul.hSMul (α := ℕ) (β := BilinForm A (M₁ ⊗[R] M₂)) 2
          ((BilinForm.tensorDistrib R A : (a : BilinForm A M₁ ⊗[R] BilinForm R M₂) → BilinForm A (M₁ ⊗[R] M₂))
              (((associatedHom.{uA, uA, uM₁, uA} A (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₁ ⊗ₜ[R]
                ((associatedHom.{uR, uR, uM₂, uR} R (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₂) :
            BilinForm A (M₁ ⊗[R] M₂))))
have rw : HSMul.hSMul (α := ℕ) (β := BilinMap A (M₁ ⊗[R] M₂) A) 2
    (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₂)) =
  HSMul.hSMul (α := ℕ) 2
    (HSMul.hSMul (α := A) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
      (HSMul.hSMul (α := ℕ) (β := BilinForm A (M₁ ⊗[R] M₂)) 2
        ((BilinForm.tensorDistrib R A : (a : BilinForm A M₁ ⊗[R] BilinForm R M₂) → BilinForm A (M₁ ⊗[R] M₂))
            (((associatedHom.{uA, uA, uM₁, uA} A (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₁ ⊗ₜ[R]
              ((associatedHom.{uR, uR, uM₂, uR} R (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₂) :
          BilinForm A (M₁ ⊗[R] M₂))))
Tactic: rw [smul_comm (_ : A) (_ : ℕ), ← smul_assoc, two_smul _ (_ : A), invOf_two_add_invOf_two,
    one_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.TensorProduct (goal)
Goal:
R : Type uR
A : Type uA
M₂ : Type uM₂
inst : CommRing R
inst_1 : CommRing A
inst_2 : AddCommGroup M₂
inst_3 : Algebra R A
inst_4 : Module R M₂
inst_5 : Invertible (α := R) 2
inst_6 : Invertible (α := A) 2
Q : QuadraticForm R M₂
⊢ Eq (α := BilinMap A (A ⊗[R] M₂) A)
    (((associated (R := A) (M := A ⊗[R] M₂) (N := A) : QuadraticMap A (A ⊗[R] M₂) A →ₗ[A] BilinMap A (A ⊗[R] M₂) A) :
          (a : QuadraticMap A (A ⊗[R] M₂) A) → BilinMap A (A ⊗[R] M₂) A)
        (QuadraticForm.baseChange A Q) :
      BilinMap A (A ⊗[R] M₂) A)
    (BilinForm.baseChange A
        (((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) :
      BilinForm A (A ⊗[R] M₂))
have dsimp : Eq (α := BilinMap A (A ⊗[R] M₂) A)
  (((associated (R := A) (M := A ⊗[R] M₂) (N := A) : QuadraticMap A (A ⊗[R] M₂) A →ₗ[A] BilinMap A (A ⊗[R] M₂) A) :
        (a : QuadraticMap A (A ⊗[R] M₂) A) → BilinMap A (A ⊗[R] M₂) A)
      (QuadraticForm.tmul.{uR, uA, uA, uM₂} (A := A) (M₁ := A) QuadraticMap.sq Q) :
    BilinMap A (A ⊗[R] M₂) A)
  (BilinForm.baseChange A
      (((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) :
    BilinForm A (A ⊗[R] M₂))
Tactic: dsimp only [QuadraticForm.baseChange, LinearMap.baseChange]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.TensorProduct (goal)
Goal:
R : Type uR
A : Type uA
M₂ : Type uM₂
inst : CommRing R
inst_1 : CommRing A
inst_2 : AddCommGroup M₂
inst_3 : Algebra R A
inst_4 : Module R M₂
inst_5 : Invertible (α := R) 2
inst_6 : Invertible (α := A) 2
Q : QuadraticForm R M₂
⊢ Eq (α := BilinMap A (A ⊗[R] M₂) A)
    (((associated (R := A) (M := A ⊗[R] M₂) (N := A) : QuadraticMap A (A ⊗[R] M₂) A →ₗ[A] BilinMap A (A ⊗[R] M₂) A) :
          (a : QuadraticMap A (A ⊗[R] M₂) A) → BilinMap A (A ⊗[R] M₂) A)
        (QuadraticForm.tmul.{uR, uA, uA, uM₂} (A := A) (M₁ := A) QuadraticMap.sq Q) :
      BilinMap A (A ⊗[R] M₂) A)
    (BilinForm.baseChange A
        (((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) :
      BilinForm A (A ⊗[R] M₂))
have rw : Eq (α := BilinMap A (A ⊗[R] M₂) A)
  (BilinForm.tmul (LinearMap.mul A A)
    (((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))
  (BilinForm.baseChange A
    (((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))
Tactic: rw [associated_tmul (QuadraticMap.sq (R := A)) Q, associated_sq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.TensorProduct (goal)
Goal:
R : Type uR
A : Type uA
M₂ : Type uM₂
N₁ : Type uN₁
inst : CommRing R
inst_1 : CommRing A
inst_2 : AddCommGroup M₂
inst_3 : AddCommGroup N₁
inst_4 : Algebra R A
inst_5 : Module R N₁
inst_6 : Module A N₁
inst_7 : IsScalarTower R A N₁
inst_8 : Module R M₂
Q₁ Q₂ : QuadraticMap A (A ⊗[R] M₂) N₁
h :
  ∀ (m : M₂),
    Eq.{uN₁ + 1} (α := N₁) ((Q₁ : (a : A ⊗[R] M₂) → N₁) (1 ⊗ₜ[R] m) : N₁) ((Q₂ : (a : A ⊗[R] M₂) → N₁) (1 ⊗ₜ[R] m) : N₁)
a : A
m : M₂
⊢ Eq.{uN₁ + 1} (α := N₁) ((Q₁ : (a : A ⊗[R] M₂) → N₁) (a ⊗ₜ[R] m) : N₁) ((Q₂ : (a : A ⊗[R] M₂) → N₁) (a ⊗ₜ[R] m) : N₁)
have rw : Eq.{uN₁ + 1} (α := N₁) ((Q₁ : (a : A ⊗[R] M₂) → N₁) ((a * 1) ⊗ₜ[R] m) : N₁)
  ((Q₂ : (a : A ⊗[R] M₂) → N₁) ((a * 1) ⊗ₜ[R] m) : N₁)
Tactic: rw [← mul_one a, ← smul_eq_mul, ← smul_tmul', QuadraticMap.map_smul, QuadraticMap.map_smul, h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.TensorProduct (goal)
Goal:
R : Type uR
A : Type uA
M₂ : Type uM₂
N₁ : Type uN₁
inst : CommRing R
inst_1 : CommRing A
inst_2 : AddCommGroup M₂
inst_3 : AddCommGroup N₁
inst_4 : Algebra R A
inst_5 : Module R N₁
inst_6 : Module A N₁
inst_7 : IsScalarTower R A N₁
inst_8 : Module R M₂
Q₁ Q₂ : QuadraticMap A (A ⊗[R] M₂) N₁
h :
  ∀ (m : M₂),
    Eq.{uN₁ + 1} (α := N₁) ((Q₁ : (a : A ⊗[R] M₂) → N₁) (1 ⊗ₜ[R] m) : N₁) ((Q₂ : (a : A ⊗[R] M₂) → N₁) (1 ⊗ₜ[R] m) : N₁)
a : A
m : M₂
rw :
  Eq.{uN₁ + 1} (α := N₁) ((Q₁ : (a : A ⊗[R] M₂) → N₁) ((a * 1) ⊗ₜ[R] m) : N₁)
    ((Q₂ : (a : A ⊗[R] M₂) → N₁) ((a * 1) ⊗ₜ[R] m) : N₁)
⊢ Eq.{uN₁ + 1} (α := N₁) ((Q₁ : (a : A ⊗[R] M₂) → N₁) (a ⊗ₜ[R] m) : N₁) ((Q₂ : (a : A ⊗[R] M₂) → N₁) (a ⊗ₜ[R] m) : N₁)
have rw₁ : Eq.{uN₁ + 1} (α := N₁) ((Q₁ : (a : A ⊗[R] M₂) → N₁) (HSMul.hSMul (β := A) a 1 ⊗ₜ[R] m) : N₁)
  ((Q₂ : (a : A ⊗[R] M₂) → N₁) (HSMul.hSMul (β := A) a 1 ⊗ₜ[R] m) : N₁)
Tactic: rw [← mul_one a, ← smul_eq_mul, ← smul_tmul', QuadraticMap.map_smul, QuadraticMap.map_smul, h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.TensorProduct (goal)
Goal:
R : Type uR
A : Type uA
M₂ : Type uM₂
N₁ : Type uN₁
inst : CommRing R
inst_1 : CommRing A
inst_2 : AddCommGroup M₂
inst_3 : AddCommGroup N₁
inst_4 : Algebra R A
inst_5 : Module R N₁
inst_6 : Module A N₁
inst_7 : IsScalarTower R A N₁
inst_8 : Module R M₂
Q₁ Q₂ : QuadraticMap A (A ⊗[R] M₂) N₁
h :
  ∀ (m : M₂),
    Eq.{uN₁ + 1} (α := N₁) ((Q₁ : (a : A ⊗[R] M₂) → N₁) (1 ⊗ₜ[R] m) : N₁) ((Q₂ : (a : A ⊗[R] M₂) → N₁) (1 ⊗ₜ[R] m) : N₁)
a : A
m : M₂
rw :
  Eq.{uN₁ + 1} (α := N₁) ((Q₁ : (a : A ⊗[R] M₂) → N₁) ((a * 1) ⊗ₜ[R] m) : N₁)
    ((Q₂ : (a : A ⊗[R] M₂) → N₁) ((a * 1) ⊗ₜ[R] m) : N₁)
rw₁ :
  Eq.{uN₁ + 1} (α := N₁) ((Q₁ : (a : A ⊗[R] M₂) → N₁) (HSMul.hSMul (β := A) a 1 ⊗ₜ[R] m) : N₁)
    ((Q₂ : (a : A ⊗[R] M₂) → N₁) (HSMul.hSMul (β := A) a 1 ⊗ₜ[R] m) : N₁)
⊢ Eq.{uN₁ + 1} (α := N₁) ((Q₁ : (a : A ⊗[R] M₂) → N₁) (a ⊗ₜ[R] m) : N₁) ((Q₂ : (a : A ⊗[R] M₂) → N₁) (a ⊗ₜ[R] m) : N₁)
have rw₂ : Eq.{uN₁ + 1} (α := N₁) ((Q₁ : (a : A ⊗[R] M₂) → N₁) (HSMul.hSMul (β := A ⊗[R] M₂) a (1 ⊗ₜ[R] m)) : N₁)
  ((Q₂ : (a : A ⊗[R] M₂) → N₁) (HSMul.hSMul (β := A ⊗[R] M₂) a (1 ⊗ₜ[R] m)) : N₁)
Tactic: rw [← mul_one a, ← smul_eq_mul, ← smul_tmul', QuadraticMap.map_smul, QuadraticMap.map_smul, h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.TensorProduct (goal)
Goal:
R : Type uR
A : Type uA
M₂ : Type uM₂
N₁ : Type uN₁
inst : CommRing R
inst_1 : CommRing A
inst_2 : AddCommGroup M₂
inst_3 : AddCommGroup N₁
inst_4 : Algebra R A
inst_5 : Module R N₁
inst_6 : Module A N₁
inst_7 : IsScalarTower R A N₁
inst_8 : Module R M₂
Q₁ Q₂ : QuadraticMap A (A ⊗[R] M₂) N₁
h :
  ∀ (m : M₂),
    Eq.{uN₁ + 1} (α := N₁) ((Q₁ : (a : A ⊗[R] M₂) → N₁) (1 ⊗ₜ[R] m) : N₁) ((Q₂ : (a : A ⊗[R] M₂) → N₁) (1 ⊗ₜ[R] m) : N₁)
a : A
m : M₂
rw :
  Eq.{uN₁ + 1} (α := N₁) ((Q₁ : (a : A ⊗[R] M₂) → N₁) ((a * 1) ⊗ₜ[R] m) : N₁)
    ((Q₂ : (a : A ⊗[R] M₂) → N₁) ((a * 1) ⊗ₜ[R] m) : N₁)
rw₁ :
  Eq.{uN₁ + 1} (α := N₁) ((Q₁ : (a : A ⊗[R] M₂) → N₁) (HSMul.hSMul (β := A) a 1 ⊗ₜ[R] m) : N₁)
    ((Q₂ : (a : A ⊗[R] M₂) → N₁) (HSMul.hSMul (β := A) a 1 ⊗ₜ[R] m) : N₁)
rw₂ :
  Eq.{uN₁ + 1} (α := N₁) ((Q₁ : (a : A ⊗[R] M₂) → N₁) (HSMul.hSMul (β := A ⊗[R] M₂) a (1 ⊗ₜ[R] m)) : N₁)
    ((Q₂ : (a : A ⊗[R] M₂) → N₁) (HSMul.hSMul (β := A ⊗[R] M₂) a (1 ⊗ₜ[R] m)) : N₁)
⊢ Eq.{uN₁ + 1} (α := N₁) ((Q₁ : (a : A ⊗[R] M₂) → N₁) (a ⊗ₜ[R] m) : N₁) ((Q₂ : (a : A ⊗[R] M₂) → N₁) (a ⊗ₜ[R] m) : N₁)
have rw₃ : HSMul.hSMul (β := N₁) (a * a) ((Q₁ : (a : A ⊗[R] M₂) → N₁) (1 ⊗ₜ[R] m) : N₁) =
  (Q₂ : (a : A ⊗[R] M₂) → N₁) (HSMul.hSMul (β := A ⊗[R] M₂) a (1 ⊗ₜ[R] m))
Tactic: rw [← mul_one a, ← smul_eq_mul, ← smul_tmul', QuadraticMap.map_smul, QuadraticMap.map_smul, h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.TensorProduct (goal)
Goal:
R : Type uR
A : Type uA
M₂ : Type uM₂
N₁ : Type uN₁
inst : CommRing R
inst_1 : CommRing A
inst_2 : AddCommGroup M₂
inst_3 : AddCommGroup N₁
inst_4 : Algebra R A
inst_5 : Module R N₁
inst_6 : Module A N₁
inst_7 : IsScalarTower R A N₁
inst_8 : Module R M₂
Q₁ Q₂ : QuadraticMap A (A ⊗[R] M₂) N₁
h :
  ∀ (m : M₂),
    Eq.{uN₁ + 1} (α := N₁) ((Q₁ : (a : A ⊗[R] M₂) → N₁) (1 ⊗ₜ[R] m) : N₁) ((Q₂ : (a : A ⊗[R] M₂) → N₁) (1 ⊗ₜ[R] m) : N₁)
a : A
m : M₂
rw :
  Eq.{uN₁ + 1} (α := N₁) ((Q₁ : (a : A ⊗[R] M₂) → N₁) ((a * 1) ⊗ₜ[R] m) : N₁)
    ((Q₂ : (a : A ⊗[R] M₂) → N₁) ((a * 1) ⊗ₜ[R] m) : N₁)
rw₁ :
  Eq.{uN₁ + 1} (α := N₁) ((Q₁ : (a : A ⊗[R] M₂) → N₁) (HSMul.hSMul (β := A) a 1 ⊗ₜ[R] m) : N₁)
    ((Q₂ : (a : A ⊗[R] M₂) → N₁) (HSMul.hSMul (β := A) a 1 ⊗ₜ[R] m) : N₁)
rw₂ :
  Eq.{uN₁ + 1} (α := N₁) ((Q₁ : (a : A ⊗[R] M₂) → N₁) (HSMul.hSMul (β := A ⊗[R] M₂) a (1 ⊗ₜ[R] m)) : N₁)
    ((Q₂ : (a : A ⊗[R] M₂) → N₁) (HSMul.hSMul (β := A ⊗[R] M₂) a (1 ⊗ₜ[R] m)) : N₁)
rw₃ :
  HSMul.hSMul (β := N₁) (a * a) ((Q₁ : (a : A ⊗[R] M₂) → N₁) (1 ⊗ₜ[R] m) : N₁) =
    (Q₂ : (a : A ⊗[R] M₂) → N₁) (HSMul.hSMul (β := A ⊗[R] M₂) a (1 ⊗ₜ[R] m))
⊢ Eq.{uN₁ + 1} (α := N₁) ((Q₁ : (a : A ⊗[R] M₂) → N₁) (a ⊗ₜ[R] m) : N₁) ((Q₂ : (a : A ⊗[R] M₂) → N₁) (a ⊗ₜ[R] m) : N₁)
have rw₄ : HSMul.hSMul (β := N₁) (a * a) ((Q₁ : (a : A ⊗[R] M₂) → N₁) (1 ⊗ₜ[R] m) : N₁) =
  HSMul.hSMul (β := N₁) (a * a) ((Q₂ : (a : A ⊗[R] M₂) → N₁) (1 ⊗ₜ[R] m) : N₁)
Tactic: rw [← mul_one a, ← smul_eq_mul, ← smul_tmul', QuadraticMap.map_smul, QuadraticMap.map_smul, h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.TensorProduct (goal)
Goal:
R : Type uR
A : Type uA
M₂ : Type uM₂
N₁ : Type uN₁
inst : CommRing R
inst_1 : CommRing A
inst_2 : AddCommGroup M₂
inst_3 : AddCommGroup N₁
inst_4 : Algebra R A
inst_5 : Module R N₁
inst_6 : Module A N₁
inst_7 : IsScalarTower R A N₁
inst_8 : Module R M₂
Q₁ Q₂ : QuadraticMap A (A ⊗[R] M₂) N₁
h :
  ∀ (m : M₂),
    Eq.{uN₁ + 1} (α := N₁) ((Q₁ : (a : A ⊗[R] M₂) → N₁) (1 ⊗ₜ[R] m) : N₁) ((Q₂ : (a : A ⊗[R] M₂) → N₁) (1 ⊗ₜ[R] m) : N₁)
a : A
m : M₂
rw :
  Eq.{uN₁ + 1} (α := N₁) ((Q₁ : (a : A ⊗[R] M₂) → N₁) ((a * 1) ⊗ₜ[R] m) : N₁)
    ((Q₂ : (a : A ⊗[R] M₂) → N₁) ((a * 1) ⊗ₜ[R] m) : N₁)
rw₁ :
  Eq.{uN₁ + 1} (α := N₁) ((Q₁ : (a : A ⊗[R] M₂) → N₁) (HSMul.hSMul (β := A) a 1 ⊗ₜ[R] m) : N₁)
    ((Q₂ : (a : A ⊗[R] M₂) → N₁) (HSMul.hSMul (β := A) a 1 ⊗ₜ[R] m) : N₁)
rw₂ :
  Eq.{uN₁ + 1} (α := N₁) ((Q₁ : (a : A ⊗[R] M₂) → N₁) (HSMul.hSMul (β := A ⊗[R] M₂) a (1 ⊗ₜ[R] m)) : N₁)
    ((Q₂ : (a : A ⊗[R] M₂) → N₁) (HSMul.hSMul (β := A ⊗[R] M₂) a (1 ⊗ₜ[R] m)) : N₁)
rw₃ :
  HSMul.hSMul (β := N₁) (a * a) ((Q₁ : (a : A ⊗[R] M₂) → N₁) (1 ⊗ₜ[R] m) : N₁) =
    (Q₂ : (a : A ⊗[R] M₂) → N₁) (HSMul.hSMul (β := A ⊗[R] M₂) a (1 ⊗ₜ[R] m))
rw₄ :
  HSMul.hSMul (β := N₁) (a * a) ((Q₁ : (a : A ⊗[R] M₂) → N₁) (1 ⊗ₜ[R] m) : N₁) =
    HSMul.hSMul (β := N₁) (a * a) ((Q₂ : (a : A ⊗[R] M₂) → N₁) (1 ⊗ₜ[R] m) : N₁)
⊢ Eq.{uN₁ + 1} (α := N₁) ((Q₁ : (a : A ⊗[R] M₂) → N₁) (a ⊗ₜ[R] m) : N₁) ((Q₂ : (a : A ⊗[R] M₂) → N₁) (a ⊗ₜ[R] m) : N₁)
have rw₅ : HSMul.hSMul (β := N₁) (a * a) ((Q₂ : (a : A ⊗[R] M₂) → N₁) (1 ⊗ₜ[R] m) : N₁) =
  HSMul.hSMul (β := N₁) (a * a) ((Q₂ : (a : A ⊗[R] M₂) → N₁) (1 ⊗ₜ[R] m) : N₁)
Tactic: rw [← mul_one a, ← smul_eq_mul, ← smul_tmul', QuadraticMap.map_smul, QuadraticMap.map_smul, h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.TensorProduct (hypothesis)
Goal:
R : Type uR
A : Type uA
M₂ : Type uM₂
N₁ : Type uN₁
inst : CommRing R
inst_1 : CommRing A
inst_2 : AddCommGroup M₂
inst_3 : AddCommGroup N₁
inst_4 : Algebra R A
inst_5 : Module R N₁
inst_6 : Module A N₁
inst_7 : IsScalarTower R A N₁
inst_8 : Module R M₂
Q₁ Q₂ : QuadraticMap A (A ⊗[R] M₂) N₁
h :
  ∀ (m : M₂),
    Eq.{uN₁ + 1} (α := N₁) ((Q₁ : (a : A ⊗[R] M₂) → N₁) (1 ⊗ₜ[R] m) : N₁) ((Q₂ : (a : A ⊗[R] M₂) → N₁) (1 ⊗ₜ[R] m) : N₁)
⊢ Q₁ = Q₂
have h₁ : ∀ (a : A) (m : M₂),
  Eq.{uN₁ + 1} (α := N₁) ((Q₁ : (a : A ⊗[R] M₂) → N₁) (a ⊗ₜ[R] m) : N₁) ((Q₂ : (a : A ⊗[R] M₂) → N₁) (a ⊗ₜ[R] m) : N₁)
Tactic: replace h (a m) : Q₁ (a ⊗ₜ m) = Q₂ (a ⊗ₜ m) := by
    rw [← mul_one a, ← smul_eq_mul, ← smul_tmul', QuadraticMap.map_smul, QuadraticMap.map_smul, h]
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.TensorProduct (goal)
Goal:
R : Type uR
A : Type uA
M₂ : Type uM₂
N₁ : Type uN₁
inst : CommRing R
inst_1 : CommRing A
inst_2 : AddCommGroup M₂
inst_3 : AddCommGroup N₁
inst_4 : Algebra R A
inst_5 : Module R N₁
inst_6 : Module A N₁
inst_7 : IsScalarTower R A N₁
inst_8 : Module R M₂
Q₁ Q₂ : QuadraticMap A (A ⊗[R] M₂) N₁
h :
  ∀ (a : A) (m : M₂),
    Eq.{uN₁ + 1} (α := N₁) ((Q₁ : (a : A ⊗[R] M₂) → N₁) (a ⊗ₜ[R] m) : N₁) ((Q₂ : (a : A ⊗[R] M₂) → N₁) (a ⊗ₜ[R] m) : N₁)
⊢ Q₁ = Q₂
have H : ∀ (x : A ⊗[R] M₂), Eq.{uN₁ + 1} (α := N₁) ((Q₁ : (a : A ⊗[R] M₂) → N₁) x : N₁) ((Q₂ : (a : A ⊗[R] M₂) → N₁) x : N₁)
Tactic: ext x
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.TensorProduct (goal)
Goal:
R : Type uR
A : Type uA
M₂ : Type uM₂
N₁ : Type uN₁
inst : CommRing R
inst_1 : CommRing A
inst_2 : AddCommGroup M₂
inst_3 : AddCommGroup N₁
inst_4 : Algebra R A
inst_5 : Module R N₁
inst_6 : Module A N₁
inst_7 : IsScalarTower R A N₁
inst_8 : Module R M₂
Q₁ Q₂ : QuadraticMap A (A ⊗[R] M₂) N₁
h :
  ∀ (a : A) (m : M₂),
    Eq.{uN₁ + 1} (α := N₁) ((Q₁ : (a : A ⊗[R] M₂) → N₁) (a ⊗ₜ[R] m) : N₁) ((Q₂ : (a : A ⊗[R] M₂) → N₁) (a ⊗ₜ[R] m) : N₁)
x y : A ⊗[R] M₂
hx : Eq.{uN₁ + 1} (α := N₁) ((Q₁ : (a : A ⊗[R] M₂) → N₁) x : N₁) ((Q₂ : (a : A ⊗[R] M₂) → N₁) x : N₁)
hy : Eq.{uN₁ + 1} (α := N₁) ((Q₁ : (a : A ⊗[R] M₂) → N₁) y : N₁) ((Q₂ : (a : A ⊗[R] M₂) → N₁) y : N₁)
⊢ Eq (α := BilinMap A (A ⊗[R] M₂) N₁) (Q₁.polarBilin (R := A) (M := A ⊗[R] M₂) (N := N₁) : BilinMap A (A ⊗[R] M₂) N₁)
    (Q₂.polarBilin (R := A) (M := A ⊗[R] M₂) (N := N₁) : BilinMap A (A ⊗[R] M₂) N₁)
have a : ∀ (x x_1 : M₂),
  Eq.{uN₁ + 1} (α := N₁)
    ((((AlgebraTensorModule.curry
                  ((((AlgebraTensorModule.curry (Q₁.polarBilin (R := A) (M := A ⊗[R] M₂) (N := N₁)) :
                            A →ₗ[A] M₂ →ₗ[R] A ⊗[R] M₂ →ₗ[A] N₁) :
                          (a : A) → M₂ →ₗ[R] A ⊗[R] M₂ →ₗ[A] N₁)
                        1 :
                      (a : M₂) → A ⊗[R] M₂ →ₗ[A] N₁)
                    x) :
                A →ₗ[A] M₂ →ₗ[R] N₁) :
              (a : A) → M₂ →ₗ[R] N₁)
            1 :
          (a : M₂) → N₁)
        x_1 :
      N₁)
    ((((AlgebraTensorModule.curry
                  ((((AlgebraTensorModule.curry (Q₂.polarBilin (R := A) (M := A ⊗[R] M₂) (N := N₁)) :
                            A →ₗ[A] M₂ →ₗ[R] A ⊗[R] M₂ →ₗ[A] N₁) :
                          (a : A) → M₂ →ₗ[R] A ⊗[R] M₂ →ₗ[A] N₁)
                        1 :
                      (a : M₂) → A ⊗[R] M₂ →ₗ[A] N₁)
                    x) :
                A →ₗ[A] M₂ →ₗ[R] N₁) :
              (a : A) → M₂ →ₗ[R] N₁)
            1 :
          (a : M₂) → N₁)
        x_1 :
      N₁)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.TensorProduct (goal)
Goal:
R : Type uR
A : Type uA
M₂ : Type uM₂
N₁ : Type uN₁
inst : CommRing R
inst_1 : CommRing A
inst_2 : AddCommGroup M₂
inst_3 : AddCommGroup N₁
inst_4 : Algebra R A
inst_5 : Module R N₁
inst_6 : Module A N₁
inst_7 : IsScalarTower R A N₁
inst_8 : Module R M₂
Q₁ Q₂ : QuadraticMap A (A ⊗[R] M₂) N₁
h :
  ∀ (a : A) (m : M₂),
    Eq.{uN₁ + 1} (α := N₁) ((Q₁ : (a : A ⊗[R] M₂) → N₁) (a ⊗ₜ[R] m) : N₁) ((Q₂ : (a : A ⊗[R] M₂) → N₁) (a ⊗ₜ[R] m) : N₁)
x y : A ⊗[R] M₂
hx : Eq.{uN₁ + 1} (α := N₁) ((Q₁ : (a : A ⊗[R] M₂) → N₁) x : N₁) ((Q₂ : (a : A ⊗[R] M₂) → N₁) x : N₁)
hy : Eq.{uN₁ + 1} (α := N₁) ((Q₁ : (a : A ⊗[R] M₂) → N₁) y : N₁) ((Q₂ : (a : A ⊗[R] M₂) → N₁) y : N₁)
x_1 x_2 : M₂
⊢ Eq.{uN₁ + 1} (α := N₁)
    ((((AlgebraTensorModule.curry
                  ((((AlgebraTensorModule.curry (Q₁.polarBilin (R := A) (M := A ⊗[R] M₂) (N := N₁)) :
                            A →ₗ[A] M₂ →ₗ[R] A ⊗[R] M₂ →ₗ[A] N₁) :
                          (a : A) → M₂ →ₗ[R] A ⊗[R] M₂ →ₗ[A] N₁)
                        1 :
                      (a : M₂) → A ⊗[R] M₂ →ₗ[A] N₁)
                    x_1) :
                A →ₗ[A] M₂ →ₗ[R] N₁) :
              (a : A) → M₂ →ₗ[R] N₁)
            1 :
          (a : M₂) → N₁)
        x_2 :
      N₁)
    ((((AlgebraTensorModule.curry
                  ((((AlgebraTensorModule.curry (Q₂.polarBilin (R := A) (M := A ⊗[R] M₂) (N := N₁)) :
                            A →ₗ[A] M₂ →ₗ[R] A ⊗[R] M₂ →ₗ[A] N₁) :
                          (a : A) → M₂ →ₗ[R] A ⊗[R] M₂ →ₗ[A] N₁)
                        1 :
                      (a : M₂) → A ⊗[R] M₂ →ₗ[A] N₁)
                    x_1) :
                A →ₗ[A] M₂ →ₗ[R] N₁) :
              (a : A) → M₂ →ₗ[R] N₁)
            1 :
          (a : M₂) → N₁)
        x_2 :
      N₁)
have a : HSub.hSub (β := N₁)
    (HSub.hSub (α := N₁) (β := N₁)
      ((Q₁ : (a : A ⊗[R] M₂) → N₁) (HAdd.hAdd (α := A ⊗[R] M₂) (1 ⊗ₜ[R] x_1) (1 ⊗ₜ[R] x_2)) : N₁)
      ((Q₁ : (a : A ⊗[R] M₂) → N₁) (1 ⊗ₜ[R] x_1) : N₁))
    ((Q₁ : (a : A ⊗[R] M₂) → N₁) (1 ⊗ₜ[R] x_2) : N₁) =
  HSub.hSub (β := N₁)
    (HSub.hSub (α := N₁) (β := N₁)
      ((Q₂ : (a : A ⊗[R] M₂) → N₁) (HAdd.hAdd (α := A ⊗[R] M₂) (1 ⊗ₜ[R] x_1) (1 ⊗ₜ[R] x_2)) : N₁)
      ((Q₂ : (a : A ⊗[R] M₂) → N₁) (1 ⊗ₜ[R] x_1) : N₁))
    ((Q₂ : (a : A ⊗[R] M₂) → N₁) (1 ⊗ₜ[R] x_2) : N₁)
Tactic: dsimp [polar]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.TensorProduct (goal)
Goal:
R : Type uR
A : Type uA
M₂ : Type uM₂
N₁ : Type uN₁
inst : CommRing R
inst_1 : CommRing A
inst_2 : AddCommGroup M₂
inst_3 : AddCommGroup N₁
inst_4 : Algebra R A
inst_5 : Module R N₁
inst_6 : Module A N₁
inst_7 : IsScalarTower R A N₁
inst_8 : Module R M₂
Q₁ Q₂ : QuadraticMap A (A ⊗[R] M₂) N₁
h :
  ∀ (a : A) (m : M₂),
    Eq.{uN₁ + 1} (α := N₁) ((Q₁ : (a : A ⊗[R] M₂) → N₁) (a ⊗ₜ[R] m) : N₁) ((Q₂ : (a : A ⊗[R] M₂) → N₁) (a ⊗ₜ[R] m) : N₁)
x y : A ⊗[R] M₂
hx : Eq.{uN₁ + 1} (α := N₁) ((Q₁ : (a : A ⊗[R] M₂) → N₁) x : N₁) ((Q₂ : (a : A ⊗[R] M₂) → N₁) x : N₁)
hy : Eq.{uN₁ + 1} (α := N₁) ((Q₁ : (a : A ⊗[R] M₂) → N₁) y : N₁) ((Q₂ : (a : A ⊗[R] M₂) → N₁) y : N₁)
x_1 x_2 : M₂
⊢ HSub.hSub (β := N₁)
      (HSub.hSub (α := N₁) (β := N₁)
        ((Q₁ : (a : A ⊗[R] M₂) → N₁) (HAdd.hAdd (α := A ⊗[R] M₂) (1 ⊗ₜ[R] x_1) (1 ⊗ₜ[R] x_2)) : N₁)
        ((Q₁ : (a : A ⊗[R] M₂) → N₁) (1 ⊗ₜ[R] x_1) : N₁))
      ((Q₁ : (a : A ⊗[R] M₂) → N₁) (1 ⊗ₜ[R] x_2) : N₁) =
    HSub.hSub (β := N₁)
      (HSub.hSub (α := N₁) (β := N₁)
        ((Q₂ : (a : A ⊗[R] M₂) → N₁) (HAdd.hAdd (α := A ⊗[R] M₂) (1 ⊗ₜ[R] x_1) (1 ⊗ₜ[R] x_2)) : N₁)
        ((Q₂ : (a : A ⊗[R] M₂) → N₁) (1 ⊗ₜ[R] x_1) : N₁))
      ((Q₂ : (a : A ⊗[R] M₂) → N₁) (1 ⊗ₜ[R] x_2) : N₁)
have a : HSub.hSub (β := N₁)
    (HSub.hSub (α := N₁) (β := N₁) ((Q₁ : (a : A ⊗[R] M₂) → N₁) (1 ⊗ₜ[R] (x_1 + x_2)) : N₁)
      ((Q₁ : (a : A ⊗[R] M₂) → N₁) (1 ⊗ₜ[R] x_1) : N₁))
    ((Q₁ : (a : A ⊗[R] M₂) → N₁) (1 ⊗ₜ[R] x_2) : N₁) =
  HSub.hSub (β := N₁)
    (HSub.hSub (α := N₁) (β := N₁) ((Q₂ : (a : A ⊗[R] M₂) → N₁) (1 ⊗ₜ[R] (x_1 + x_2)) : N₁)
      ((Q₂ : (a : A ⊗[R] M₂) → N₁) (1 ⊗ₜ[R] x_1) : N₁))
    ((Q₂ : (a : A ⊗[R] M₂) → N₁) (1 ⊗ₜ[R] x_2) : N₁)
Tactic: rw [← TensorProduct.tmul_add, h, h, h]