awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.BilinearForm.Properties
Goal:
V : Type u_5
K : Type u_6
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
ι : Type u_9
inst_3 : DecidableEq ι
inst_4 : Finite ι
B : BilinForm K V
hB : B.Nondegenerate
b : Basis ι K V
i j : ι
a :
  Eq.{u_6 + 1} (α := K) (if j = i then 1 else 0 : K)
    ((((B : (a : V) → V →ₗ[K] K) ((b : (a : ι) → V) i) : V →ₗ[K] K) : (a : V) → K)
        ((B.flip.dualBasis ⋯ b : (a : ι) → V) j : V) :
      K)
a₁ :
  Eq.{u_6 + 1} (α := K) (if j = i then 1 else 0 : K)
    ((((((flipHom : (a : BilinForm K V) → BilinForm K V) B : BilinForm K V) : (a : V) → V →ₗ[K] K)
              ((B.flip.dualBasis ⋯ b : (a : ι) → V) j) :
            V →ₗ[K] K) :
          (a : V) → K)
        ((b : (a : ι) → V) i : V) :
      K)
a₂ : Eq.{u_6 + 1} (α := K) (if j = i then 1 else 0) (if i = j then 1 else 0)
⊢ Eq.{u_6 + 1} (α := K)
    ((((B : (a : V) → V →ₗ[K] K) ((B.dualBasis hB (B.flip.dualBasis ⋯ b) : (a : ι) → V) i) : V →ₗ[K] K) : (a : V) → K)
        ((B.flip.dualBasis ⋯ b : (a : ι) → V) j : V) :
      K)
    ((((B : (a : V) → V →ₗ[K] K) ((b : (a : ι) → V) i) : V →ₗ[K] K) : (a : V) → K)
        ((B.flip.dualBasis ⋯ b : (a : ι) → V) j : V) :
      K)

Tactic:
simp_rw [apply_dualBasis_left, ← B.flip_apply, apply_dualBasis_left, @eq_comm _ i j]

Premises used: LinearMap.BilinForm.apply_dualBasis_left, eq_comm, LinearMap.BilinForm.flip_apply
-- Module: Mathlib.LinearAlgebra.BilinearForm.Properties
Goal:
V : Type u_5
K : Type u_6
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
ι : Type u_9
inst_3 : DecidableEq ι
inst_4 : Finite ι
B : BilinForm K V
hB : B.Nondegenerate
b : Basis ι K V
⊢ B.flip.dualBasis ⋯ (B.dualBasis hB b) = b

Tactic:
dualBasis_dualBasis_flip hB.flip b

Premises used: LinearMap.mk₂'ₛₗ, LinearMap.BilinForm.Nondegenerate.flip, LinearMap.flip, LinearMap.BilinForm.dualBasis_dualBasis_flip
-- Module: Mathlib.LinearAlgebra.BilinearForm.Properties
Goal:
V : Type u_5
K : Type u_6
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
ι : Type u_9
inst_3 : DecidableEq ι
inst_4 : Finite ι
B : BilinForm K V
hB : B.Nondegenerate
hB' : B.IsSymm
b : Basis ι K V
⊢ B.flip.dualBasis ⋯ (B.flip.flip.dualBasis ⋯ b) = b

Tactic:
dualBasis_dualBasis_flip hB.flip b

Premises used: LinearMap.BilinForm.Nondegenerate.flip, LinearMap.BilinForm.dualBasis_dualBasis_flip
-- Module: Mathlib.LinearAlgebra.BilinearForm.Properties
Goal:
V : Type u_5
K : Type u_6
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
ι : Type u_9
inst_3 : DecidableEq ι
inst_4 : Finite ι
B : BilinForm K V
hB : B.Nondegenerate
hB' : B.IsSymm
b : Basis ι K V
h : B = B.flip
⊢ B.dualBasis hB (B.dualBasis hB b) = b

Tactic:
convert! dualBasis_dualBasis_flip hB.flip b

Premises used: LinearMap.BilinForm.Nondegenerate.flip, LinearMap.BilinForm.dualBasis_dualBasis_flip
-- Module: Mathlib.LinearAlgebra.BilinearForm.Properties
Goal:
V : Type u_5
K : Type u_6
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
ι : Type u_9
inst_3 : DecidableEq ι
inst_4 : Finite ι
B : BilinForm K V
hB : B.Nondegenerate
hB' : B.IsSymm
b : Basis ι K V
h : B.flip = B
h₁ h₂ h₃ h₄ : B.IsSymm
⊢ B = B.flip

Tactic:
rwa [eq_comm, ← isSymm_iff_flip]

Premises used: LinearMap.BilinForm.isSymm_iff_flip, eq_comm
-- Module: Mathlib.LinearAlgebra.BilinearForm.Properties
Goal:
V : Type u_5
K : Type u_6
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
ι : Type u_9
inst_3 : DecidableEq ι
inst_4 : Finite ι
B : BilinForm K V
hB : B.Nondegenerate
hB' : B.IsSymm
⊢ Function.Involutive (α := Basis ι K V) (B.dualBasis hB)

Tactic:
fun b ↦ dualBasis_dualBasis hB hB' b

Premises used: LinearMap.BilinForm.dualBasis_dualBasis, Function.Involutive
-- Module: Mathlib.LinearAlgebra.BilinearForm.Properties
Goal:
V : Type u_5
K : Type u_6
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
ι : Type u_9
inst_3 : DecidableEq ι
inst_4 : Finite ι
B : BilinForm K V
hB : B.Nondegenerate
hB' : B.IsSymm
⊢ Function.Injective (α := Basis ι K V) (B.dualBasis hB)

Tactic:
(B.dualBasis_involutive hB hB').injective

Premises used: Function.Involutive.injective, LinearMap.BilinForm.dualBasis_involutive
-- Module: Mathlib.LinearAlgebra.BilinearForm.Properties
Goal:
V : Type u_5
K : Type u_6
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
ι : Type u_9
inst_3 : DecidableEq ι
inst_4 : Finite ι
B : BilinForm K V
hB : B.Nondegenerate
b : Basis ι K V
v : ι → V
h : (⇑(B.dualBasis hB b) : (a : ι) → V) = v
x x_1 : ι
rw :
  Eq.{u_6 + 1} (α := K)
    ((((B : (a : V) → V →ₗ[K] K) ((B.dualBasis hB b : (a : ι) → V) x) : V →ₗ[K] K) : (a : V) → K)
        ((b : (a : ι) → V) x_1 : V) :
      K)
    (if x_1 = x then 1 else 0 : K)
rw₁ rw₂ : Eq.{u_6 + 1} (α := K) (if x_1 = x then 1 else 0) (if x_1 = x then 1 else 0)
⊢ Eq.{u_6 + 1} (α := K) ((((B : (a : V) → V →ₗ[K] K) (v x) : V →ₗ[K] K) : (a : V) → K) ((b : (a : ι) → V) x_1 : V) : K)
    (if x_1 = x then 1 else 0 : K)

Tactic:
rw [← h, apply_dualBasis_left]

Premises used: LinearMap.BilinForm.apply_dualBasis_left
-- Module: Mathlib.LinearAlgebra.BilinearForm.Properties
Goal:
V : Type u_5
K : Type u_6
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
ι : Type u_9
inst_3 : DecidableEq ι
inst_4 : Finite ι
B : BilinForm K V
hB : B.Nondegenerate
b : Basis ι K V
v : ι → V
h :
  ∀ (i j : ι),
    Eq.{u_6 + 1} (α := K) ((((B : (a : V) → V →ₗ[K] K) (v i) : V →ₗ[K] K) : (a : V) → K) ((b : (a : ι) → V) j : V) : K)
      (if j = i then 1 else 0 : K)
x x_1 : ι
rw :
  Eq.{u_6 + 1} (α := K)
    ((((B : (a : V) → V →ₗ[K] K) ((B.dualBasis hB b : (a : ι) → V) x) : V →ₗ[K] K) : (a : V) → K)
        ((b : (a : ι) → V) x_1 : V) :
      K)
    (((((B.dualBasis hB b).repr : (a : V) → ι →₀ K) (v x) : ι →₀ K) : (a : ι) → K) x_1 : K)
rw₁ :
  Eq.{u_6 + 1} (α := K)
    ((((B : (a : V) → V →ₗ[K] K) ((B.dualBasis hB b : (a : ι) → V) x) : V →ₗ[K] K) : (a : V) → K)
        ((b : (a : ι) → V) x_1 : V) :
      K)
    ((((B : (a : V) → V →ₗ[K] K) (v x) : V →ₗ[K] K) : (a : V) → K) ((b : (a : ι) → V) x_1 : V) : K)
rw₂ :
  Eq.{u_6 + 1} (α := K) (if x_1 = x then 1 else 0 : K)
    ((((B : (a : V) → V →ₗ[K] K) (v x) : V →ₗ[K] K) : (a : V) → K) ((b : (a : ι) → V) x_1 : V) : K)
rw₃ rw₄ : Eq.{u_6 + 1} (α := K) (if x_1 = x then 1 else 0) (if x_1 = x then 1 else 0)
⊢ Eq.{u_6 + 1} (α := K)
    (((((B.dualBasis hB b).repr : (a : V) → ι →₀ K) ((B.dualBasis hB b : (a : ι) → V) x) : ι →₀ K) : (a : ι) → K) x_1 :
      K)
    (((((B.dualBasis hB b).repr : (a : V) → ι →₀ K) (v x) : ι →₀ K) : (a : ι) → K) x_1 : K)

Tactic:
rw [dualBasis_repr_apply, dualBasis_repr_apply, apply_dualBasis_left, h]

Premises used: LinearMap.BilinForm.apply_dualBasis_left, LinearMap.BilinForm.dualBasis_repr_apply
-- Module: Mathlib.LinearAlgebra.BilinearForm.Properties
Goal:
V : Type u_5
K : Type u_6
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
B₁ B₂ : BilinForm K V
b₂ : B₂.Nondegenerate
v : V
rw :
  Eq (α := V →ₗ[K] K)
    ((B₂ : (a : V) → V →ₗ[K] K) (((↑(B₂.toDual b₂).symm : Dual K V →ₗ[K] V) ∘ₗ B₁ : (a : V) → V) v) : V →ₗ[K] K)
    ((B₁ : (a : V) → V →ₗ[K] K) v : V →ₗ[K] K)
⊢ Eq (α := V →ₗ[K] K) ((B₂ : (a : V) → V →ₗ[K] K) ((B₁.symmCompOfNondegenerate B₂ b₂ : (a : V) → V) v) : V →ₗ[K] K)
    ((B₁ : (a : V) → V →ₗ[K] K) v : V →ₗ[K] K)

Tactic:
rw [symmCompOfNondegenerate]

Premises used: LinearMap.BilinForm.symmCompOfNondegenerate
-- Module: Mathlib.LinearAlgebra.BilinearForm.Properties
Goal:
V : Type u_5
K : Type u_6
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
B₁ B₂ : BilinForm K V
b₂ : B₂.Nondegenerate
v : V
simp :
  Eq (α := V →ₗ[K] K)
    ((B₂ : (a : V) → V →ₗ[K] K) (((B₂.toDual b₂).symm : (a : Dual K V) → V) ((B₁ : (a : V) → Dual K V) v : Dual K V)) :
      V →ₗ[K] K)
    ((B₁ : (a : V) → V →ₗ[K] K) v : V →ₗ[K] K)
⊢ Eq (α := V →ₗ[K] K)
    ((B₂ : (a : V) → V →ₗ[K] K) (((↑(B₂.toDual b₂).symm : Dual K V →ₗ[K] V) ∘ₗ B₁ : (a : V) → V) v) : V →ₗ[K] K)
    ((B₁ : (a : V) → V →ₗ[K] K) v : V →ₗ[K] K)

Tactic:
simp only [coe_comp, LinearEquiv.coe_coe, Function.comp_apply]

Premises used: LinearMap.coe_comp, Function.comp_apply, LinearEquiv.coe_coe
-- Module: Mathlib.LinearAlgebra.BilinearForm.Properties
Goal:
V : Type u_5
K : Type u_6
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
B₁ B₂ : BilinForm K V
b₂ : B₂.Nondegenerate
v : V
erw erw₁ : Eq (α := V →ₗ[K] K) ((B₁ : (a : V) → Dual K V) v : Dual K V) ((B₁ : (a : V) → V →ₗ[K] K) v : V →ₗ[K] K)
⊢ Eq (α := V →ₗ[K] K)
    ((B₂ : (a : V) → V →ₗ[K] K) (((B₂.toDual b₂).symm : (a : Dual K V) → V) ((B₁ : (a : V) → Dual K V) v : Dual K V)) :
      V →ₗ[K] K)
    ((B₁ : (a : V) → V →ₗ[K] K) v : V →ₗ[K] K)

Tactic:
erw [LinearEquiv.apply_symm_apply (B₂.toDual b₂)]

Premises used: LinearMap.BilinForm.toDual, LinearEquiv.apply_symm_apply
-- Module: Mathlib.LinearAlgebra.BilinearForm.Properties
Goal:
V : Type u_5
K : Type u_6
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
B₁ B₂ : BilinForm K V
b₂ : B₂.Nondegenerate
v w : V
rw : ((((B₁ : (a : V) → V →ₗ[K] K) w : V →ₗ[K] K) : (a : V) → K) v : K)
| ((((B₂ : (a : V) → V →ₗ[K] K) ((B₁.symmCompOfNondegenerate B₂ b₂ : (a : V) → V) w) : V →ₗ[K] K) : (a : V) → K) v : K)

Tactic:
rw [comp_symmCompOfNondegenerate_apply]

Premises used: LinearMap.BilinForm.comp_symmCompOfNondegenerate_apply
-- Module: Mathlib.LinearAlgebra.BilinearForm.Properties
Goal:
V : Type u_5
K : Type u_6
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
B₁ B₂ : BilinForm K V
b₂ : B₂.Nondegenerate
v w : V
conv_lhs :
  Eq.{u_6 + 1} (α := K)
    ((((B₂ : (a : V) → V →ₗ[K] K) ((B₁.symmCompOfNondegenerate B₂ b₂ : (a : V) → V) w) : V →ₗ[K] K) : (a : V) → K) v :
      K)
    ((((B₁ : (a : V) → V →ₗ[K] K) w : V →ₗ[K] K) : (a : V) → K) v : K)
conv_lhs₁ :
  Eq.{u_6 + 1} (α := K) ((((B₁ : (a : V) → V →ₗ[K] K) w : V →ₗ[K] K) : (a : V) → K) v : K)
    ((((B₁ : (a : V) → V →ₗ[K] K) w : V →ₗ[K] K) : (a : V) → K) v : K)
⊢ Eq.{u_6 + 1} (α := K)
    ((((B₂ : (a : V) → V →ₗ[K] K) ((B₁.symmCompOfNondegenerate B₂ b₂ : (a : V) → V) w) : V →ₗ[K] K) : (a : V) → K) v :
      K)
    ((((B₁ : (a : V) → V →ₗ[K] K) w : V →ₗ[K] K) : (a : V) → K) v : K)

Tactic:
conv_lhs => rw [comp_symmCompOfNondegenerate_apply]

Premises used: LinearMap.BilinForm.comp_symmCompOfNondegenerate_apply
-- Module: Mathlib.LinearAlgebra.BilinearForm.Properties
Goal:
V : Type u_5
K : Type u_6
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
B : BilinForm K V
b : B.Nondegenerate
φ : V →ₗ[K] V
⊢ IsAdjointPair B B (⇑(B.leftAdjointOfNondegenerate b φ) : (a : V) → V) (⇑φ : (a : V) → V)

Tactic:
fun x y =>
  (B.compRight φ).symmCompOfNondegenerate_left_apply b y x

Premises used: LinearMap.BilinForm.symmCompOfNondegenerate_left_apply, LinearMap.IsAdjointPair, LinearMap.BilinForm.compRight
-- Module: Mathlib.LinearAlgebra.BilinearForm.Properties
Goal:
V : Type u_5
K : Type u_6
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
B : BilinForm K V
b : B.Nondegenerate
ψ φ : V →ₗ[K] V
⊢ IsAdjointPair B B (⇑ψ : (a : V) → V) (⇑φ : (a : V) → V) ↔ ψ = B.leftAdjointOfNondegenerate b φ

Tactic:
⟨fun h =>
    B.isAdjointPair_unique_of_nondegenerate b φ ψ _ h
      (isAdjointPairLeftAdjointOfNondegenerate _ _ _),
    fun h => h.symm ▸ isAdjointPairLeftAdjointOfNondegenerate _ _ _⟩

Premises used: LinearMap.BilinForm.isAdjointPair_unique_of_nondegenerate, Eq.rec, Iff.intro, Eq.symm, LinearMap.BilinForm.isAdjointPairLeftAdjointOfNondegenerate, LinearMap.BilinForm.leftAdjointOfNondegenerate
-- Module: Mathlib.LinearAlgebra.BilinearForm.TensorProduct
Goal:
R : Type uR
A : Type uA
M₁ : Type uM₁
M₂ : Type uM₂
N₁ : Type uN₁
N₂ : Type uN₂
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : AddCommMonoid M₁
inst_3 : AddCommMonoid M₂
inst_4 : AddCommMonoid N₁
inst_5 : AddCommMonoid 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 : SMulCommClass R A N₁
inst_14 : IsScalarTower R A N₁
inst_15 : Module R M₂
inst_16 : Module R N₂
B₁ : BilinMap A M₁ N₁
B₂ : BilinMap R M₂ N₂
m₁ : M₁
m₂ : M₂
m₁' : M₁
m₂' : M₂
⊢ Eq (α := N₁ ⊗[R] N₂)
    (((((((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₂))
                    (B₁ ⊗ₜ[R] B₂) :
                  BilinMap A (M₁ ⊗[R] M₂) (N₁ ⊗[R] N₂)) :
                (a : M₁ ⊗[R] M₂) → M₁ ⊗[R] M₂ →ₗ[A] N₁ ⊗[R] N₂)
              (m₁ ⊗ₜ[R] m₂) :
            M₁ ⊗[R] M₂ →ₗ[A] N₁ ⊗[R] N₂) :
          (a : M₁ ⊗[R] M₂) → N₁ ⊗[R] N₂)
        (m₁' ⊗ₜ[R] m₂') :
      N₁ ⊗[R] N₂)
    ((((B₁ : (a : M₁) → M₁ →ₗ[A] N₁) m₁ : M₁ →ₗ[A] N₁) : (a : M₁) → N₁) m₁' ⊗ₜ[R]
        (((B₂ : (a : M₂) → M₂ →ₗ[R] N₂) m₂ : M₂ →ₗ[R] N₂) : (a : M₂) → N₂) m₂' :
      N₁ ⊗[R] N₂)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, TensorProduct.tmul, AddCon.toQuotient, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.LinearAlgebra.BilinearForm.TensorProduct
Goal:
R : Type uR
A : Type uA
M₁ : Type uM₁
M₂ : Type uM₂
N₁ : Type uN₁
N₂ : Type uN₂
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : AddCommMonoid M₁
inst_3 : AddCommMonoid M₂
inst_4 : AddCommMonoid N₁
inst_5 : AddCommMonoid 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 : SMulCommClass R A N₁
inst_14 : IsScalarTower R A N₁
inst_15 : Module R M₂
inst_16 : Module R N₂
B₁ : BilinMap A M₁ N₁
B₂ : BilinMap R M₂ N₂
hB₁ :
  ∀ (x y : M₁),
    Eq.{uN₁ + 1} (α := N₁) ((((B₁ : (a : M₁) → M₁ →ₗ[A] N₁) x : M₁ →ₗ[A] N₁) : (a : M₁) → N₁) y : N₁)
      ((((B₁ : (a : M₁) → M₁ →ₗ[A] N₁) y : M₁ →ₗ[A] N₁) : (a : M₁) → N₁) x : N₁)
hB₂ :
  ∀ (x y : M₂),
    Eq.{uN₂ + 1} (α := N₂) ((((B₂ : (a : M₂) → M₂ →ₗ[R] N₂) x : M₂ →ₗ[R] N₂) : (a : M₂) → N₂) y : N₂)
      ((((B₂ : (a : M₂) → M₂ →ₗ[R] N₂) y : M₂ →ₗ[R] N₂) : (a : M₂) → N₂) x : N₂)
x y : M₁ ⊗[R] M₂
revert :
  ∀ (x y : M₁ ⊗[R] M₂),
    Eq (α := N₁ ⊗[R] N₂)
      ((((B₁.tmul B₂ : (a : M₁ ⊗[R] M₂) → M₁ ⊗[R] M₂ →ₗ[A] N₁ ⊗[R] N₂) x : M₁ ⊗[R] M₂ →ₗ[A] N₁ ⊗[R] N₂) :
            (a : M₁ ⊗[R] M₂) → N₁ ⊗[R] N₂)
          y :
        N₁ ⊗[R] N₂)
      ((((B₁.tmul B₂ : (a : M₁ ⊗[R] M₂) → M₁ ⊗[R] M₂ →ₗ[A] N₁ ⊗[R] N₂) y : M₁ ⊗[R] M₂ →ₗ[A] N₁ ⊗[R] N₂) :
            (a : M₁ ⊗[R] M₂) → N₁ ⊗[R] N₂)
          x :
        N₁ ⊗[R] N₂)
⊢ Eq (α := N₁ ⊗[R] N₂)
    ((((B₁.tmul B₂ : (a : M₁ ⊗[R] M₂) → M₁ ⊗[R] M₂ →ₗ[A] N₁ ⊗[R] N₂) x : M₁ ⊗[R] M₂ →ₗ[A] N₁ ⊗[R] N₂) :
          (a : M₁ ⊗[R] M₂) → N₁ ⊗[R] N₂)
        y :
      N₁ ⊗[R] N₂)
    ((((B₁.tmul B₂ : (a : M₁ ⊗[R] M₂) → M₁ ⊗[R] M₂ →ₗ[A] N₁ ⊗[R] N₂) y : M₁ ⊗[R] M₂ →ₗ[A] N₁ ⊗[R] N₂) :
          (a : M₁ ⊗[R] M₂) → N₁ ⊗[R] N₂)
        x :
      N₁ ⊗[R] N₂)

Tactic:
revert x y
-- Module: Mathlib.LinearAlgebra.BilinearForm.TensorProduct
Goal:
R : Type uR
A : Type uA
M₁ : Type uM₁
M₂ : Type uM₂
N₁ : Type uN₁
N₂ : Type uN₂
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : AddCommMonoid M₁
inst_3 : AddCommMonoid M₂
inst_4 : AddCommMonoid N₁
inst_5 : AddCommMonoid 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 : SMulCommClass R A N₁
inst_14 : IsScalarTower R A N₁
inst_15 : Module R M₂
inst_16 : Module R N₂
B₁ : BilinMap A M₁ N₁
B₂ : BilinMap R M₂ N₂
hB₁ :
  ∀ (x y : M₁),
    Eq.{uN₁ + 1} (α := N₁) ((((B₁ : (a : M₁) → M₁ →ₗ[A] N₁) x : M₁ →ₗ[A] N₁) : (a : M₁) → N₁) y : N₁)
      ((((B₁ : (a : M₁) → M₁ →ₗ[A] N₁) y : M₁ →ₗ[A] N₁) : (a : M₁) → N₁) x : N₁)
hB₂ :
  ∀ (x y : M₂),
    Eq.{uN₂ + 1} (α := N₂) ((((B₂ : (a : M₂) → M₂ →ₗ[R] N₂) x : M₂ →ₗ[R] N₂) : (a : M₂) → N₂) y : N₂)
      ((((B₂ : (a : M₂) → M₂ →ₗ[R] N₂) y : M₂ →ₗ[R] N₂) : (a : M₂) → N₂) x : N₂)
rw : Eq (α := BilinMap A (M₁ ⊗[R] M₂) (N₁ ⊗[R] N₂)) (B₁.tmul B₂) (flip (B₁.tmul B₂))
⊢ ∀ (x y : M₁ ⊗[R] M₂),
    Eq (α := N₁ ⊗[R] N₂)
      ((((B₁.tmul B₂ : (a : M₁ ⊗[R] M₂) → M₁ ⊗[R] M₂ →ₗ[A] N₁ ⊗[R] N₂) x : M₁ ⊗[R] M₂ →ₗ[A] N₁ ⊗[R] N₂) :
            (a : M₁ ⊗[R] M₂) → N₁ ⊗[R] N₂)
          y :
        N₁ ⊗[R] N₂)
      ((((B₁.tmul B₂ : (a : M₁ ⊗[R] M₂) → M₁ ⊗[R] M₂ →ₗ[A] N₁ ⊗[R] N₂) y : M₁ ⊗[R] M₂ →ₗ[A] N₁ ⊗[R] N₂) :
            (a : M₁ ⊗[R] M₂) → N₁ ⊗[R] N₂)
          x :
        N₁ ⊗[R] N₂)

Tactic:
rw [isSymm_iff_eq_flip]

Premises used: LinearMap.BilinMap.isSymm_iff_eq_flip
-- Module: Mathlib.LinearAlgebra.BilinearForm.TensorProduct
Goal:
R : Type uR
A : Type uA
M₁ : Type uM₁
M₂ : Type uM₂
N₁ : Type uN₁
N₂ : Type uN₂
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : AddCommMonoid M₁
inst_3 : AddCommMonoid M₂
inst_4 : AddCommMonoid N₁
inst_5 : AddCommMonoid 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 : SMulCommClass R A N₁
inst_14 : IsScalarTower R A N₁
inst_15 : Module R M₂
inst_16 : Module R N₂
B₁ : BilinMap A M₁ N₁
B₂ : BilinMap R M₂ N₂
hB₁ :
  ∀ (x y : M₁),
    Eq.{uN₁ + 1} (α := N₁) ((((B₁ : (a : M₁) → M₁ →ₗ[A] N₁) x : M₁ →ₗ[A] N₁) : (a : M₁) → N₁) y : N₁)
      ((((B₁ : (a : M₁) → M₁ →ₗ[A] N₁) y : M₁ →ₗ[A] N₁) : (a : M₁) → N₁) x : N₁)
hB₂ :
  ∀ (x y : M₂),
    Eq.{uN₂ + 1} (α := N₂) ((((B₂ : (a : M₂) → M₂ →ₗ[R] N₂) x : M₂ →ₗ[R] N₂) : (a : M₂) → N₂) y : N₂)
      ((((B₂ : (a : M₂) → M₂ →ₗ[R] N₂) y : M₂ →ₗ[R] N₂) : (a : M₂) → N₂) x : N₂)
⊢ Eq (α := BilinMap A (M₁ ⊗[R] M₂) (N₁ ⊗[R] N₂)) (B₁.tmul B₂) (flip (B₁.tmul B₂))

Tactic:
aesop
-- Module: Mathlib.LinearAlgebra.BilinearForm.TensorProduct
Goal:
R : Type uR
A : Type uA
M₂ : Type uM₂
N₂ : Type uN₂
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid N₂
inst_4 : Algebra R A
inst_5 : Module R M₂
inst_6 : Module R N₂
B₂ : BilinMap R M₂ N₂
a : A
m₂ : M₂
a' : A
m₂' : M₂
⊢ Eq (α := A ⊗[R] N₂)
    ((((BilinMap.baseChange A B₂ : (a : A ⊗[R] M₂) → A ⊗[R] M₂ →ₗ[A] A ⊗[R] N₂) (a ⊗ₜ[R] m₂) :
            A ⊗[R] M₂ →ₗ[A] A ⊗[R] N₂) :
          (a : A ⊗[R] M₂) → A ⊗[R] N₂)
        (a' ⊗ₜ[R] m₂') :
      A ⊗[R] N₂)
    ((a * a') ⊗ₜ[R] (((B₂ : (a : M₂) → M₂ →ₗ[R] N₂) m₂ : M₂ →ₗ[R] N₂) : (a : M₂) → N₂) m₂' : A ⊗[R] N₂)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, TensorProduct.tmul, AddCon.toQuotient, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.LinearAlgebra.BilinearForm.TensorProduct
Goal:
R : Type uR
A : Type uA
M₂ : Type uM₂
N₂ : Type uN₂
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid N₂
inst_4 : Algebra R A
inst_5 : Module R M₂
inst_6 : Module R N₂
B₂ : BilinMap R M₂ N₂
hB₂ :
  ∀ (x y : M₂),
    Eq.{uN₂ + 1} (α := N₂) ((((B₂ : (a : M₂) → M₂ →ₗ[R] N₂) x : M₂ →ₗ[R] N₂) : (a : M₂) → N₂) y : N₂)
      ((((B₂ : (a : M₂) → M₂ →ₗ[R] N₂) y : M₂ →ₗ[R] N₂) : (a : M₂) → N₂) x : N₂)
x y : A ⊗[R] M₂
⊢ Eq (α := A ⊗[R] N₂)
    ((((BilinMap.baseChange A B₂ : (a : A ⊗[R] M₂) → A ⊗[R] M₂ →ₗ[A] A ⊗[R] N₂) x : A ⊗[R] M₂ →ₗ[A] A ⊗[R] N₂) :
          (a : A ⊗[R] M₂) → A ⊗[R] N₂)
        y :
      A ⊗[R] N₂)
    ((((BilinMap.baseChange A B₂ : (a : A ⊗[R] M₂) → A ⊗[R] M₂ →ₗ[A] A ⊗[R] N₂) y : A ⊗[R] M₂ →ₗ[A] A ⊗[R] N₂) :
          (a : A ⊗[R] M₂) → A ⊗[R] N₂)
        x :
      A ⊗[R] N₂)

Tactic:
tmul_isSymm mul_comm hB₂ x y

Premises used: LinearMap.BilinMap.tmul_isSymm
-- Module: Mathlib.LinearAlgebra.BilinearForm.TensorProduct
Goal:
R : Type uR
A : Type uA
M₁ : Type uM₁
M₂ : Type uM₂
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : AddCommMonoid M₁
inst_3 : AddCommMonoid 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₂
B₁ : BilinForm A M₁
B₂ : BilinForm R M₂
m₁ : M₁
m₂ : M₂
m₁' : M₁
m₂' : M₂
⊢ (((((tensorDistrib R A : (a : BilinForm A M₁ ⊗[R] BilinForm R M₂) → BilinForm A (M₁ ⊗[R] M₂)) (B₁ ⊗ₜ[R] B₂) :
                BilinForm A (M₁ ⊗[R] M₂)) :
              (a : M₁ ⊗[R] M₂) → M₁ ⊗[R] M₂ →ₗ[A] A)
            (m₁ ⊗ₜ[R] m₂) :
          M₁ ⊗[R] M₂ →ₗ[A] A) :
        (a : M₁ ⊗[R] M₂) → A)
      (m₁' ⊗ₜ[R] m₂') =
    HSMul.hSMul.{uR, uA, uA} (α := R) (β := A) ((((B₂ : (a : M₂) → M₂ →ₗ[R] R) m₂ : M₂ →ₗ[R] R) : (a : M₂) → R) m₂' : R)
      ((((B₁ : (a : M₁) → M₁ →ₗ[A] A) m₁ : M₁ →ₗ[A] A) : (a : M₁) → A) m₁' : A)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.LinearAlgebra.BilinearForm.TensorProduct
Goal:
R : Type uR
A : Type uA
M₁ : Type uM₁
M₂ : Type uM₂
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : AddCommMonoid M₁
inst_3 : AddCommMonoid 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₂
B₁ : BilinForm A M₁
B₂ : BilinForm R M₂
hB₁ : IsSymm B₁
hB₂ : IsSymm B₂
rw : Eq (α := BilinForm A (M₁ ⊗[R] M₂)) (B₁.tmul B₂) (LinearMap.flip (B₁.tmul B₂))
⊢ IsSymm (M := M₁ ⊗[R] M₂) (B₁.tmul B₂)

Tactic:
rw [LinearMap.isSymm_iff_eq_flip]

Premises used: LinearMap.isSymm_iff_eq_flip
-- Module: Mathlib.LinearAlgebra.BilinearForm.TensorProduct
Goal:
R : Type uR
A : Type uA
M₁ : Type uM₁
M₂ : Type uM₂
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : AddCommMonoid M₁
inst_3 : AddCommMonoid 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₂
B₁ : BilinForm A M₁
B₂ : BilinForm R M₂
hB₁ : IsSymm B₁
hB₂ : IsSymm B₂
a :
  ∀ (x₁ : M₁) (x₂ : M₂) (y₁ : M₁) (y₂ : M₂),
    Eq.{uA + 1} (α := A)
      (((((AlgebraTensorModule.curry
                      (((((AlgebraTensorModule.curry (B₁.tmul B₂) : M₁ →ₗ[A] M₂ →ₗ[R] M₁ ⊗[R] M₂ →ₗ[A] A) :
                                (a : M₁) → M₂ →ₗ[R] M₁ ⊗[R] M₂ →ₗ[A] A)
                              x₁ :
                            M₂ →ₗ[R] M₁ ⊗[R] M₂ →ₗ[A] A) :
                          (a : M₂) → M₁ ⊗[R] M₂ →ₗ[A] A)
                        x₂) :
                    M₁ →ₗ[A] M₂ →ₗ[R] A) :
                  (a : M₁) → M₂ →ₗ[R] A)
                y₁ :
              M₂ →ₗ[R] A) :
            (a : M₂) → A)
          y₂ :
        A)
      (((((AlgebraTensorModule.curry
                      (((((AlgebraTensorModule.curry (LinearMap.flip (B₁.tmul B₂)) :
                                  M₁ →ₗ[A] M₂ →ₗ[R] M₁ ⊗[R] M₂ →ₗ[A] A) :
                                (a : M₁) → M₂ →ₗ[R] M₁ ⊗[R] M₂ →ₗ[A] A)
                              x₁ :
                            M₂ →ₗ[R] M₁ ⊗[R] M₂ →ₗ[A] A) :
                          (a : M₂) → M₁ ⊗[R] M₂ →ₗ[A] A)
                        x₂) :
                    M₁ →ₗ[A] M₂ →ₗ[R] A) :
                  (a : M₁) → M₂ →ₗ[R] A)
                y₁ :
              M₂ →ₗ[R] A) :
            (a : M₂) → A)
          y₂ :
        A)
⊢ Eq (α := BilinForm A (M₁ ⊗[R] M₂)) (B₁.tmul B₂) (LinearMap.flip (B₁.tmul B₂))

Tactic:
ext x₁ x₂ y₁ y₂