awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
x y : Dual R N ⊗[R] Dual R M
h :
  Eq.{u_1 + 1} (α := R)
    ((((dualDistrib R N M : (a : Dual R N ⊗[R] Dual R M) → Dual R (N ⊗[R] M)) x : Dual R (N ⊗[R] M)) :
          (a : N ⊗[R] M) → R)
        ((TensorProduct.comm R M N : (a : M ⊗[R] N) → N ⊗[R] M) 0) :
      R)
    ((((dualDistrib R M N : (a : Dual R M ⊗[R] Dual R N) → Dual R (M ⊗[R] N))
              ((TensorProduct.comm R (Dual R N) (Dual R M) : (a : Dual R N ⊗[R] Dual R M) → Dual R M ⊗[R] Dual R N) x) :
            Dual R (M ⊗[R] N)) :
          (a : M ⊗[R] N) → R)
        0 :
      R)
h_1 :
  Eq.{u_1 + 1} (α := R)
    ((((dualDistrib R N M : (a : Dual R N ⊗[R] Dual R M) → Dual R (N ⊗[R] M)) y : Dual R (N ⊗[R] M)) :
          (a : N ⊗[R] M) → R)
        ((TensorProduct.comm R M N : (a : M ⊗[R] N) → N ⊗[R] M) 0) :
      R)
    ((((dualDistrib R M N : (a : Dual R M ⊗[R] Dual R N) → Dual R (M ⊗[R] N))
              ((TensorProduct.comm R (Dual R N) (Dual R M) : (a : Dual R N ⊗[R] Dual R M) → Dual R M ⊗[R] Dual R N) y) :
            Dual R (M ⊗[R] N)) :
          (a : M ⊗[R] N) → R)
        0 :
      R)
⊢ Eq.{u_1 + 1} (α := R)
    ((((dualDistrib R N M : (a : Dual R N ⊗[R] Dual R M) → Dual R (N ⊗[R] M)) (x + y) : Dual R (N ⊗[R] M)) :
          (a : N ⊗[R] M) → R)
        ((TensorProduct.comm R M N : (a : M ⊗[R] N) → N ⊗[R] M) 0) :
      R)
    ((((dualDistrib R M N : (a : Dual R M ⊗[R] Dual R N) → Dual R (M ⊗[R] N))
              ((TensorProduct.comm R (Dual R N) (Dual R M) : (a : Dual R N ⊗[R] Dual R M) → Dual R M ⊗[R] Dual R N)
                (x + y)) :
            Dual R (M ⊗[R] N)) :
          (a : M ⊗[R] N) → R)
        0 :
      R)

Tactic:
simp_all [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
x y : Dual R N ⊗[R] Dual R M
x_1 : M
y_1 : N
h :
  Eq.{u_1 + 1} (α := R)
    ((((dualDistrib R N M : (a : Dual R N ⊗[R] Dual R M) → Dual R (N ⊗[R] M)) x : Dual R (N ⊗[R] M)) :
          (a : N ⊗[R] M) → R)
        ((TensorProduct.comm R M N : (a : M ⊗[R] N) → N ⊗[R] M) (x_1 ⊗ₜ[R] y_1) : N ⊗[R] M) :
      R)
    ((((dualDistrib R M N : (a : Dual R M ⊗[R] Dual R N) → Dual R (M ⊗[R] N))
              ((TensorProduct.comm R (Dual R N) (Dual R M) : (a : Dual R N ⊗[R] Dual R M) → Dual R M ⊗[R] Dual R N) x) :
            Dual R (M ⊗[R] N)) :
          (a : M ⊗[R] N) → R)
        (x_1 ⊗ₜ[R] y_1) :
      R)
h_1 :
  Eq.{u_1 + 1} (α := R)
    ((((dualDistrib R N M : (a : Dual R N ⊗[R] Dual R M) → Dual R (N ⊗[R] M)) y : Dual R (N ⊗[R] M)) :
          (a : N ⊗[R] M) → R)
        ((TensorProduct.comm R M N : (a : M ⊗[R] N) → N ⊗[R] M) (x_1 ⊗ₜ[R] y_1) : N ⊗[R] M) :
      R)
    ((((dualDistrib R M N : (a : Dual R M ⊗[R] Dual R N) → Dual R (M ⊗[R] N))
              ((TensorProduct.comm R (Dual R N) (Dual R M) : (a : Dual R N ⊗[R] Dual R M) → Dual R M ⊗[R] Dual R N) y) :
            Dual R (M ⊗[R] N)) :
          (a : M ⊗[R] N) → R)
        (x_1 ⊗ₜ[R] y_1) :
      R)
⊢ Eq.{u_1 + 1} (α := R)
    ((((dualDistrib R N M : (a : Dual R N ⊗[R] Dual R M) → Dual R (N ⊗[R] M)) (x + y) : Dual R (N ⊗[R] M)) :
          (a : N ⊗[R] M) → R)
        ((TensorProduct.comm R M N : (a : M ⊗[R] N) → N ⊗[R] M) (x_1 ⊗ₜ[R] y_1) : N ⊗[R] M) :
      R)
    ((((dualDistrib R M N : (a : Dual R M ⊗[R] Dual R N) → Dual R (M ⊗[R] N))
              ((TensorProduct.comm R (Dual R N) (Dual R M) : (a : Dual R N ⊗[R] Dual R M) → Dual R M ⊗[R] Dual R N)
                (x + y)) :
            Dual R (M ⊗[R] N)) :
          (a : M ⊗[R] N) → R)
        (x_1 ⊗ₜ[R] y_1) :
      R)

Tactic:
simp_all [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid N
inst_5 : Module R M
inst_6 : Module A M
inst_7 : Module R N
inst_8 : IsScalarTower R A M
f : Dual A M
g : Dual R N
m : M
n : N
⊢ ((((dualDistrib R A M N : Dual A M ⊗[R] Dual R N →ₗ[A] Dual A (M ⊗[R] N)) :
              (a : Dual A M ⊗[R] Dual R N) → Dual A (M ⊗[R] N))
            (f ⊗ₜ[R] g) :
          Dual A (M ⊗[R] N)) :
        (a : M ⊗[R] N) → A)
      (m ⊗ₜ[R] n) =
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := A) ((g : (a : N) → R) n : R) ((f : (a : M) → A) m : A)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst : DecidableEq ι
inst_1 : DecidableEq κ
inst_2 : Fintype ι
inst_3 : Fintype κ
inst_4 : CommSemiring R
inst_5 : AddCommMonoid M
inst_6 : AddCommMonoid N
inst_7 : Module R M
inst_8 : Module R N
b : Basis ι R M
c : Basis κ R N
f : Dual R (M ⊗[R] N)
⊢ Eq (α := Dual R M ⊗[R] Dual R N)
    ((dualDistribInvOfBasis b c : (a : Dual R (M ⊗[R] N)) → Dual R M ⊗[R] Dual R N) f : Dual R M ⊗[R] Dual R N)
    (∑ i : ι,
        ∑ j : κ,
          HSMul.hSMul (α := R) (β := Dual R M ⊗[R] Dual R N)
            ((f : (a : M ⊗[R] N) → R) ((b : (a : ι) → M) i ⊗ₜ[R] (c : (a : κ) → N) j : M ⊗[R] N) : R)
            ((b.dualBasis : (a : ι) → Dual R M) i ⊗ₜ[R] (c.dualBasis : (a : κ) → Dual R N) j : Dual R M ⊗[R] Dual R N) :
      Dual R M ⊗[R] Dual R N)

Tactic:
simp [dualDistribInvOfBasis]

Premises used: TensorProduct.dualDistribInvOfBasis
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst : DecidableEq ι
inst_1 : DecidableEq κ
inst_2 : Fintype ι
inst_3 : Fintype κ
inst_4 : CommSemiring R
inst_5 : AddCommMonoid M
inst_6 : AddCommMonoid N
inst_7 : Module R M
inst_8 : Module R N
b : Basis ι R M
c : Basis κ R N
apply :
  ∀ (i : ι × κ),
    Eq (α := Dual R (M ⊗[R] N))
      ((dualDistrib R M N ∘ₗ dualDistribInvOfBasis b c : (a : Dual R (M ⊗[R] N)) → Dual R (M ⊗[R] N))
          (((Basis.dualBasis (b.tensorProduct c) : Basis (ι × κ) R (Dual R (M ⊗[R] N))) :
              (a : ι × κ) → Dual R (M ⊗[R] N))
            i) :
        Dual R (M ⊗[R] N))
      ((LinearMap.id : (a : Dual R (M ⊗[R] N)) → Dual R (M ⊗[R] N))
          (((Basis.dualBasis (b.tensorProduct c) : Basis (ι × κ) R (Dual R (M ⊗[R] N))) :
              (a : ι × κ) → Dual R (M ⊗[R] N))
            i) :
        Dual R (M ⊗[R] N))
⊢ dualDistrib R M N ∘ₗ dualDistribInvOfBasis b c = LinearMap.id

Tactic:
apply (b.tensorProduct c).dualBasis.ext

Premises used: Module.Basis.dualBasis, Module.Basis.tensorProduct, Module.Basis.ext
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst : DecidableEq ι
inst_1 : DecidableEq κ
inst_2 : Fintype ι
inst_3 : Fintype κ
inst_4 : CommSemiring R
inst_5 : AddCommMonoid M
inst_6 : AddCommMonoid N
inst_7 : Module R M
inst_8 : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
apply :
  ∀ (i_1 : ι × κ),
    Eq.{u_1 + 1} (α := R)
      ((((dualDistrib R M N ∘ₗ dualDistribInvOfBasis b c : (a : Dual R (M ⊗[R] N)) → Dual R (M ⊗[R] N))
                (((Basis.dualBasis (b.tensorProduct c) : Basis (ι × κ) R (Dual R (M ⊗[R] N))) :
                    (a : ι × κ) → Dual R (M ⊗[R] N))
                  (i, j)) :
              Dual R (M ⊗[R] N)) :
            (a : M ⊗[R] N) → R)
          (((b.tensorProduct c : Basis (ι × κ) R (M ⊗[R] N)) : (a : ι × κ) → M ⊗[R] N) i_1 : M ⊗[R] N) :
        R)
      ((((LinearMap.id : (a : Dual R (M ⊗[R] N)) → Dual R (M ⊗[R] N))
                (((Basis.dualBasis (b.tensorProduct c) : Basis (ι × κ) R (Dual R (M ⊗[R] N))) :
                    (a : ι × κ) → Dual R (M ⊗[R] N))
                  (i, j)) :
              Dual R (M ⊗[R] N)) :
            (a : M ⊗[R] N) → R)
          (((b.tensorProduct c : Basis (ι × κ) R (M ⊗[R] N)) : (a : ι × κ) → M ⊗[R] N) i_1 : M ⊗[R] N) :
        R)
⊢ Eq (α := Dual R (M ⊗[R] N))
    ((dualDistrib R M N ∘ₗ dualDistribInvOfBasis b c : (a : Dual R (M ⊗[R] N)) → Dual R (M ⊗[R] N))
        (((Basis.dualBasis (b.tensorProduct c) : Basis (ι × κ) R (Dual R (M ⊗[R] N))) : (a : ι × κ) → Dual R (M ⊗[R] N))
          (i, j)) :
      Dual R (M ⊗[R] N))
    ((LinearMap.id : (a : Dual R (M ⊗[R] N)) → Dual R (M ⊗[R] N))
        (((Basis.dualBasis (b.tensorProduct c) : Basis (ι × κ) R (Dual R (M ⊗[R] N))) : (a : ι × κ) → Dual R (M ⊗[R] N))
          (i, j)) :
      Dual R (M ⊗[R] N))

Tactic:
apply (b.tensorProduct c).ext

Premises used: Module.Basis.tensorProduct, Module.Basis.ext
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst : DecidableEq ι
inst_1 : DecidableEq κ
inst_2 : Fintype ι
inst_3 : Fintype κ
inst_4 : CommSemiring R
inst_5 : AddCommMonoid M
inst_6 : AddCommMonoid N
inst_7 : Module R M
inst_8 : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
i' : ι
j' : κ
simp :
  ∑ x : ι,
      ∑ x_1 : κ,
        HMul.hMul (α := R) (β := R) ((Finsupp.single x_1 1 : (a : κ) → R) j : R)
            ((Finsupp.single x 1 : (a : ι) → R) i : R) *
          HMul.hMul (α := R) (β := R) ((Finsupp.single i' 1 : (a : ι) → R) x : R)
            ((Finsupp.single j' 1 : (a : κ) → R) x_1 : R) =
    HMul.hMul (α := R) (β := R) ((Finsupp.single j' 1 : (a : κ) → R) j : R) ((Finsupp.single i' 1 : (a : ι) → R) i : R)
⊢ Eq.{u_1 + 1} (α := R)
    ((((dualDistrib R M N ∘ₗ dualDistribInvOfBasis b c : (a : Dual R (M ⊗[R] N)) → Dual R (M ⊗[R] N))
              (((Basis.dualBasis (b.tensorProduct c) : Basis (ι × κ) R (Dual R (M ⊗[R] N))) :
                  (a : ι × κ) → Dual R (M ⊗[R] N))
                (i, j)) :
            Dual R (M ⊗[R] N)) :
          (a : M ⊗[R] N) → R)
        (((b.tensorProduct c : Basis (ι × κ) R (M ⊗[R] N)) : (a : ι × κ) → M ⊗[R] N) (i', j') : M ⊗[R] N) :
      R)
    ((((LinearMap.id : (a : Dual R (M ⊗[R] N)) → Dual R (M ⊗[R] N))
              (((Basis.dualBasis (b.tensorProduct c) : Basis (ι × κ) R (Dual R (M ⊗[R] N))) :
                  (a : ι × κ) → Dual R (M ⊗[R] N))
                (i, j)) :
            Dual R (M ⊗[R] N)) :
          (a : M ⊗[R] N) → R)
        (((b.tensorProduct c : Basis (ι × κ) R (M ⊗[R] N)) : (a : ι × κ) → M ⊗[R] N) (i', j') : M ⊗[R] N) :
      R)

Tactic:
simp only [dualDistrib, Basis.coe_dualBasis, coe_comp, Function.comp_apply,
    dualDistribInvOfBasis_apply, Basis.coord_apply, Basis.tensorProduct_repr_tmul_apply,
    Basis.repr_self, _root_.map_sum, map_smul, homTensorHomMap_apply, compRight_apply,
    Basis.tensorProduct_apply, LinearMap.coe_sum, Finset.sum_apply, smul_apply, LinearEquiv.coe_coe,
    map_tmul, lid_tmul, smul_eq_mul, id_coe, id_eq]

Premises used: Module.Basis.tensorProduct_apply, LinearMap.compRight_apply, Module.Basis.coe_dualBasis, LinearMap.smul_apply, LinearMap.id_coe, Finset.sum_apply, TensorProduct.dualDistrib, TensorProduct.lid_tmul, LinearMap.coe_sum, map_sum, LinearMap.coe_comp, TensorProduct.dualDistribInvOfBasis_apply, TensorProduct.map_tmul, TensorProduct.homTensorHomMap_apply, Function.comp_apply, smul_eq_mul, Module.Basis.tensorProduct_repr_tmul_apply, Module.Basis.coord_apply, Module.Basis.repr_self, LinearEquiv.coe_coe, map_smul, id_eq
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst : DecidableEq ι
inst_1 : DecidableEq κ
inst_2 : Fintype ι
inst_3 : Fintype κ
inst_4 : CommSemiring R
inst_5 : AddCommMonoid M
inst_6 : AddCommMonoid N
inst_7 : Module R M
inst_8 : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
i' : ι
j' : κ
rw :
  HMul.hMul (α := R) (β := R) ((Finsupp.single j 1 : (a : κ) → R) j : R) ((Finsupp.single i 1 : (a : ι) → R) i : R) *
      HMul.hMul (α := R) (β := R) ((Finsupp.single i' 1 : (a : ι) → R) i : R)
        ((Finsupp.single j' 1 : (a : κ) → R) j : R) =
    HMul.hMul (α := R) (β := R) ((Finsupp.single j' 1 : (a : κ) → R) j : R) ((Finsupp.single i' 1 : (a : ι) → R) i : R)
h₀ :
  ∀ (b : κ),
    Membership.mem (γ := Finset κ) Finset.univ b →
      b ≠ j →
        HMul.hMul (α := R) (β := R) ((Finsupp.single b 1 : (a : κ) → R) j : R)
              ((Finsupp.single i 1 : (a : ι) → R) i : R) *
            HMul.hMul (α := R) (β := R) ((Finsupp.single i' 1 : (a : ι) → R) i : R)
              ((Finsupp.single j' 1 : (a : κ) → R) b : R) =
          0
h₁ :
  j ∉ Finset.univ →
    HMul.hMul (α := R) (β := R) ((Finsupp.single j 1 : (a : κ) → R) j : R) ((Finsupp.single i 1 : (a : ι) → R) i : R) *
        HMul.hMul (α := R) (β := R) ((Finsupp.single i' 1 : (a : ι) → R) i : R)
          ((Finsupp.single j' 1 : (a : κ) → R) j : R) =
      0
h₂ :
  ∀ (b : ι),
    Membership.mem (γ := Finset ι) Finset.univ b →
      b ≠ i →
        Eq.{u_1 + 1} (α := R)
          (∑ x : κ,
            HMul.hMul (α := R) (β := R) ((Finsupp.single x 1 : (a : κ) → R) j : R)
                ((Finsupp.single b 1 : (a : ι) → R) i : R) *
              HMul.hMul (α := R) (β := R) ((Finsupp.single i' 1 : (a : ι) → R) b : R)
                ((Finsupp.single j' 1 : (a : κ) → R) x : R))
          0
h₃ :
  i ∉ Finset.univ →
    Eq.{u_1 + 1} (α := R)
      (∑ x : κ,
        HMul.hMul (α := R) (β := R) ((Finsupp.single x 1 : (a : κ) → R) j : R)
            ((Finsupp.single i 1 : (a : ι) → R) i : R) *
          HMul.hMul (α := R) (β := R) ((Finsupp.single i' 1 : (a : ι) → R) i : R)
            ((Finsupp.single j' 1 : (a : κ) → R) x : R))
      0
⊢ ∑ x : ι,
      ∑ x_1 : κ,
        HMul.hMul (α := R) (β := R) ((Finsupp.single x_1 1 : (a : κ) → R) j : R)
            ((Finsupp.single x 1 : (a : ι) → R) i : R) *
          HMul.hMul (α := R) (β := R) ((Finsupp.single i' 1 : (a : ι) → R) x : R)
            ((Finsupp.single j' 1 : (a : κ) → R) x_1 : R) =
    HMul.hMul (α := R) (β := R) ((Finsupp.single j' 1 : (a : κ) → R) j : R) ((Finsupp.single i' 1 : (a : ι) → R) i : R)

Tactic:
rw [Finset.sum_eq_single i, Finset.sum_eq_single j]

Premises used: Finset.sum_eq_single
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst : DecidableEq ι
inst_1 : DecidableEq κ
inst_2 : Fintype ι
inst_3 : Fintype κ
inst_4 : CommSemiring R
inst_5 : AddCommMonoid M
inst_6 : AddCommMonoid N
inst_7 : Module R M
inst_8 : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
i' : ι
j' : κ
⊢ HMul.hMul (α := R) (β := R) ((Finsupp.single j 1 : (a : κ) → R) j : R) ((Finsupp.single i 1 : (a : ι) → R) i : R) *
      HMul.hMul (α := R) (β := R) ((Finsupp.single i' 1 : (a : ι) → R) i : R)
        ((Finsupp.single j' 1 : (a : κ) → R) j : R) =
    HMul.hMul (α := R) (β := R) ((Finsupp.single j' 1 : (a : κ) → R) j : R) ((Finsupp.single i' 1 : (a : ι) → R) i : R)

Tactic:
simpa using mul_comm _ _

Premises used: mul_comm
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst : DecidableEq ι
inst_1 : DecidableEq κ
inst_2 : Fintype ι
inst_3 : Fintype κ
inst_4 : CommSemiring R
inst_5 : AddCommMonoid M
inst_6 : AddCommMonoid N
inst_7 : Module R M
inst_8 : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
i' : ι
j' b_1 : κ
h : Membership.mem (γ := Finset κ) Finset.univ b_1
h_1 : b_1 ≠ j
⊢ HMul.hMul (α := R) (β := R) ((Finsupp.single b_1 1 : (a : κ) → R) j : R) ((Finsupp.single i 1 : (a : ι) → R) i : R) *
      HMul.hMul (α := R) (β := R) ((Finsupp.single i' 1 : (a : ι) → R) i : R)
        ((Finsupp.single j' 1 : (a : κ) → R) b_1 : R) =
    0

Tactic:
simp [*] at *
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst : DecidableEq ι
inst_1 : DecidableEq κ
inst_2 : Fintype ι
inst_3 : Fintype κ
inst_4 : CommSemiring R
inst_5 : AddCommMonoid M
inst_6 : AddCommMonoid N
inst_7 : Module R M
inst_8 : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
i' : ι
j' : κ
h₀ h₁ :
  ∀ (b : κ),
    Membership.mem (γ := Finset κ) Finset.univ b →
      b ≠ j →
        HMul.hMul (α := R) (β := R) ((Finsupp.single b 1 : (a : κ) → R) j : R)
              ((Finsupp.single i 1 : (a : ι) → R) i : R) *
            HMul.hMul (α := R) (β := R) ((Finsupp.single i' 1 : (a : ι) → R) i : R)
              ((Finsupp.single j' 1 : (a : κ) → R) b : R) =
          0
⊢ ∀ (b : κ),
    Membership.mem (γ := Finset κ) Finset.univ b →
      b ≠ j →
        HMul.hMul (α := R) (β := R) ((Finsupp.single b 1 : (a : κ) → R) j : R)
              ((Finsupp.single i 1 : (a : ι) → R) i : R) *
            HMul.hMul (α := R) (β := R) ((Finsupp.single i' 1 : (a : ι) → R) i : R)
              ((Finsupp.single j' 1 : (a : κ) → R) b : R) =
          0

Tactic:
{ intros; simp [*] at * }
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst : DecidableEq ι
inst_1 : DecidableEq κ
inst_2 : Fintype ι
inst_3 : Fintype κ
inst_4 : CommSemiring R
inst_5 : AddCommMonoid M
inst_6 : AddCommMonoid N
inst_7 : Module R M
inst_8 : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
i' : ι
j' : κ
h : j ∉ Finset.univ
⊢ HMul.hMul (α := R) (β := R) ((Finsupp.single j 1 : (a : κ) → R) j : R) ((Finsupp.single i 1 : (a : ι) → R) i : R) *
      HMul.hMul (α := R) (β := R) ((Finsupp.single i' 1 : (a : ι) → R) i : R)
        ((Finsupp.single j' 1 : (a : κ) → R) j : R) =
    0

Tactic:
simp [*] at *
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst : DecidableEq ι
inst_1 : DecidableEq κ
inst_2 : Fintype ι
inst_3 : Fintype κ
inst_4 : CommSemiring R
inst_5 : AddCommMonoid M
inst_6 : AddCommMonoid N
inst_7 : Module R M
inst_8 : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
i' : ι
j' : κ
h₁ h₂ :
  j ∉ Finset.univ →
    HMul.hMul (α := R) (β := R) ((Finsupp.single j 1 : (a : κ) → R) j : R) ((Finsupp.single i 1 : (a : ι) → R) i : R) *
        HMul.hMul (α := R) (β := R) ((Finsupp.single i' 1 : (a : ι) → R) i : R)
          ((Finsupp.single j' 1 : (a : κ) → R) j : R) =
      0
⊢ j ∉ Finset.univ →
    HMul.hMul (α := R) (β := R) ((Finsupp.single j 1 : (a : κ) → R) j : R) ((Finsupp.single i 1 : (a : ι) → R) i : R) *
        HMul.hMul (α := R) (β := R) ((Finsupp.single i' 1 : (a : ι) → R) i : R)
          ((Finsupp.single j' 1 : (a : κ) → R) j : R) =
      0

Tactic:
{ intros; simp [*] at * }
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst : DecidableEq ι
inst_1 : DecidableEq κ
inst_2 : Fintype ι
inst_3 : Fintype κ
inst_4 : CommSemiring R
inst_5 : AddCommMonoid M
inst_6 : AddCommMonoid N
inst_7 : Module R M
inst_8 : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
i' : ι
j' : κ
b_1 : ι
h : Membership.mem (γ := Finset ι) Finset.univ b_1
h_1 : b_1 ≠ i
⊢ Eq.{u_1 + 1} (α := R)
    (∑ x : κ,
      HMul.hMul (α := R) (β := R) ((Finsupp.single x 1 : (a : κ) → R) j : R)
          ((Finsupp.single b_1 1 : (a : ι) → R) i : R) *
        HMul.hMul (α := R) (β := R) ((Finsupp.single i' 1 : (a : ι) → R) b_1 : R)
          ((Finsupp.single j' 1 : (a : κ) → R) x : R))
    0

Tactic:
simp [*] at *
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst : DecidableEq ι
inst_1 : DecidableEq κ
inst_2 : Fintype ι
inst_3 : Fintype κ
inst_4 : CommSemiring R
inst_5 : AddCommMonoid M
inst_6 : AddCommMonoid N
inst_7 : Module R M
inst_8 : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
i' : ι
j' : κ
h₀ h₁ :
  ∀ (b : ι),
    Membership.mem (γ := Finset ι) Finset.univ b →
      b ≠ i →
        Eq.{u_1 + 1} (α := R)
          (∑ x : κ,
            HMul.hMul (α := R) (β := R) ((Finsupp.single x 1 : (a : κ) → R) j : R)
                ((Finsupp.single b 1 : (a : ι) → R) i : R) *
              HMul.hMul (α := R) (β := R) ((Finsupp.single i' 1 : (a : ι) → R) b : R)
                ((Finsupp.single j' 1 : (a : κ) → R) x : R))
          0
⊢ ∀ (b : ι),
    Membership.mem (γ := Finset ι) Finset.univ b →
      b ≠ i →
        Eq.{u_1 + 1} (α := R)
          (∑ x : κ,
            HMul.hMul (α := R) (β := R) ((Finsupp.single x 1 : (a : κ) → R) j : R)
                ((Finsupp.single b 1 : (a : ι) → R) i : R) *
              HMul.hMul (α := R) (β := R) ((Finsupp.single i' 1 : (a : ι) → R) b : R)
                ((Finsupp.single j' 1 : (a : κ) → R) x : R))
          0

Tactic:
{ intros; simp [*] at * }
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst : DecidableEq ι
inst_1 : DecidableEq κ
inst_2 : Fintype ι
inst_3 : Fintype κ
inst_4 : CommSemiring R
inst_5 : AddCommMonoid M
inst_6 : AddCommMonoid N
inst_7 : Module R M
inst_8 : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
i' : ι
j' : κ
h : i ∉ Finset.univ
⊢ Eq.{u_1 + 1} (α := R)
    (∑ x : κ,
      HMul.hMul (α := R) (β := R) ((Finsupp.single x 1 : (a : κ) → R) j : R)
          ((Finsupp.single i 1 : (a : ι) → R) i : R) *
        HMul.hMul (α := R) (β := R) ((Finsupp.single i' 1 : (a : ι) → R) i : R)
          ((Finsupp.single j' 1 : (a : κ) → R) x : R))
    0

Tactic:
simp [*] at *
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst : DecidableEq ι
inst_1 : DecidableEq κ
inst_2 : Fintype ι
inst_3 : Fintype κ
inst_4 : CommSemiring R
inst_5 : AddCommMonoid M
inst_6 : AddCommMonoid N
inst_7 : Module R M
inst_8 : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
i' : ι
j' : κ
h₁ h₂ :
  i ∉ Finset.univ →
    Eq.{u_1 + 1} (α := R)
      (∑ x : κ,
        HMul.hMul (α := R) (β := R) ((Finsupp.single x 1 : (a : κ) → R) j : R)
            ((Finsupp.single i 1 : (a : ι) → R) i : R) *
          HMul.hMul (α := R) (β := R) ((Finsupp.single i' 1 : (a : ι) → R) i : R)
            ((Finsupp.single j' 1 : (a : κ) → R) x : R))
      0
⊢ i ∉ Finset.univ →
    Eq.{u_1 + 1} (α := R)
      (∑ x : κ,
        HMul.hMul (α := R) (β := R) ((Finsupp.single x 1 : (a : κ) → R) j : R)
            ((Finsupp.single i 1 : (a : ι) → R) i : R) *
          HMul.hMul (α := R) (β := R) ((Finsupp.single i' 1 : (a : ι) → R) i : R)
            ((Finsupp.single j' 1 : (a : κ) → R) x : R))
      0

Tactic:
{ intros; simp [*] at * }
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst : DecidableEq ι
inst_1 : DecidableEq κ
inst_2 : Fintype ι
inst_3 : Fintype κ
inst_4 : CommSemiring R
inst_5 : AddCommMonoid M
inst_6 : AddCommMonoid N
inst_7 : Module R M
inst_8 : Module R N
b : Basis ι R M
c : Basis κ R N
apply :
  ∀ (i : ι × κ),
    Eq (α := Dual R M ⊗[R] Dual R N)
      ((dualDistribInvOfBasis b c ∘ₗ dualDistrib R M N : (a : Dual R M ⊗[R] Dual R N) → Dual R M ⊗[R] Dual R N)
          (((b.dualBasis.tensorProduct c.dualBasis : Basis (ι × κ) R (Dual R M ⊗[R] Dual R N)) :
              (a : ι × κ) → Dual R M ⊗[R] Dual R N)
            i) :
        Dual R M ⊗[R] Dual R N)
      ((LinearMap.id : (a : Dual R M ⊗[R] Dual R N) → Dual R M ⊗[R] Dual R N)
          (((b.dualBasis.tensorProduct c.dualBasis : Basis (ι × κ) R (Dual R M ⊗[R] Dual R N)) :
              (a : ι × κ) → Dual R M ⊗[R] Dual R N)
            i) :
        Dual R M ⊗[R] Dual R N)
⊢ dualDistribInvOfBasis b c ∘ₗ dualDistrib R M N = LinearMap.id

Tactic:
apply (b.dualBasis.tensorProduct c.dualBasis).ext

Premises used: Module.Basis.dualBasis, Module.Basis.tensorProduct, Module.Basis.ext