awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
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
z : M ⊗[R] N
x : Dual R N
y : Dual R M
⊢ Eq.{u_1 + 1} (α := R)
    ((((dualDistrib R N M : (a : Dual R N ⊗[R] Dual R M) → Dual R (N ⊗[R] M)) (x ⊗ₜ[R] y) : Dual R (N ⊗[R] M)) :
          (a : N ⊗[R] M) → R)
        ((TensorProduct.comm R M N : (a : M ⊗[R] N) → N ⊗[R] M) z : 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 ⊗ₜ[R] y)) :
            Dual R (M ⊗[R] N)) :
          (a : M ⊗[R] N) → R)
        z :
      R)
have tmul : Eq.{u_1 + 1} (α := R)
  ((((dualDistrib R N M : (a : Dual R N ⊗[R] Dual R M) → Dual R (N ⊗[R] M)) (x ⊗ₜ[R] 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 ⊗ₜ[R] y)) :
          Dual R (M ⊗[R] N)) :
        (a : M ⊗[R] N) → R)
      0 :
    R)
Tactic: induction z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
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
z : M ⊗[R] N
x : Dual R N
y : Dual R M
tmul :
  Eq.{u_1 + 1} (α := R)
    ((((dualDistrib R N M : (a : Dual R N ⊗[R] Dual R M) → Dual R (N ⊗[R] M)) (x ⊗ₜ[R] 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 ⊗ₜ[R] 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 ⊗ₜ[R] y) : Dual R (N ⊗[R] M)) :
          (a : N ⊗[R] M) → R)
        ((TensorProduct.comm R M N : (a : M ⊗[R] N) → N ⊗[R] M) z : 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 ⊗ₜ[R] y)) :
            Dual R (M ⊗[R] N)) :
          (a : M ⊗[R] N) → R)
        z :
      R)
have tmul₁ : ∀ (x_1 : M) (y_1 : N),
  Eq.{u_1 + 1} (α := R)
    ((((dualDistrib R N M : (a : Dual R N ⊗[R] Dual R M) → Dual R (N ⊗[R] M)) (x ⊗ₜ[R] 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 ⊗ₜ[R] y)) :
            Dual R (M ⊗[R] N)) :
          (a : M ⊗[R] N) → R)
        (x_1 ⊗ₜ[R] y_1) :
      R)
Tactic: induction z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
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
⊢ dualDistrib R M N ∘ₗ dualDistribInvOfBasis b c = LinearMap.id
have 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))
Tactic: apply (b.tensorProduct c).dualBasis.ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
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 : κ
⊢ 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))
have 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)
Tactic: apply (b.tensorProduct c).ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
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' : κ
⊢ 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)
have 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)
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
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' : κ
⊢ ∑ 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)
have 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)
Tactic: rw [Finset.sum_eq_single i, Finset.sum_eq_single j]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
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)
⊢ ∑ 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)
have 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
Tactic: rw [Finset.sum_eq_single i, Finset.sum_eq_single j]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
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
⊢ ∑ 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)
have 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: rw [Finset.sum_eq_single i, Finset.sum_eq_single j]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
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
⊢ ∑ 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)
have 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
Tactic: rw [Finset.sum_eq_single i, Finset.sum_eq_single j]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
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
⊢ ∑ 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)
have 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: rw [Finset.sum_eq_single i, Finset.sum_eq_single j]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
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
⊢ dualDistribInvOfBasis b c ∘ₗ dualDistrib R M N = LinearMap.id
have 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)
Tactic: apply (b.dualBasis.tensorProduct c.dualBasis).ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
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 : κ
⊢ 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, j)) :
      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, j)) :
      Dual R M ⊗[R] Dual R N)
have simp : Eq (α := Dual R M ⊗[R] Dual R N)
  (∑ x : ι,
    ∑ x_1 : κ,
      HSMul.hSMul (β := Dual R M ⊗[R] Dual R N)
        (HMul.hMul (α := R) (β := R) ((Finsupp.single x 1 : (a : ι) → R) i : R)
          ((Finsupp.single x_1 1 : (a : κ) → R) j : R))
        (b.coord x ⊗ₜ[R] c.coord x_1))
  (b.coord i ⊗ₜ[R] c.coord j)
Tactic: simp only [Basis.tensorProduct_apply, Basis.coe_dualBasis, coe_comp, Function.comp_apply,
    dualDistribInvOfBasis_apply, dualDistrib_apply, Basis.coord_apply, Basis.repr_self,
    id_coe, id_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
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 : κ
⊢ Eq (α := Dual R M ⊗[R] Dual R N)
    (∑ x : ι,
      ∑ x_1 : κ,
        HSMul.hSMul (β := Dual R M ⊗[R] Dual R N)
          (HMul.hMul (α := R) (β := R) ((Finsupp.single x 1 : (a : ι) → R) i : R)
            ((Finsupp.single x_1 1 : (a : κ) → R) j : R))
          (b.coord x ⊗ₜ[R] c.coord x_1))
    (b.coord i ⊗ₜ[R] c.coord j)
have rw : HSMul.hSMul (β := Dual R M ⊗[R] Dual R N)
    (HMul.hMul (α := R) (β := R) ((Finsupp.single i 1 : (a : ι) → R) i : R) ((Finsupp.single j 1 : (a : κ) → R) j : R))
    (b.coord i ⊗ₜ[R] c.coord j) =
  b.coord i ⊗ₜ[R] c.coord j
Tactic: rw [Finset.sum_eq_single i, Finset.sum_eq_single j]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
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 : κ
rw :
  HSMul.hSMul (β := Dual R M ⊗[R] Dual R N)
      (HMul.hMul (α := R) (β := R) ((Finsupp.single i 1 : (a : ι) → R) i : R)
        ((Finsupp.single j 1 : (a : κ) → R) j : R))
      (b.coord i ⊗ₜ[R] c.coord j) =
    b.coord i ⊗ₜ[R] c.coord j
⊢ Eq (α := Dual R M ⊗[R] Dual R N)
    (∑ x : ι,
      ∑ x_1 : κ,
        HSMul.hSMul (β := Dual R M ⊗[R] Dual R N)
          (HMul.hMul (α := R) (β := R) ((Finsupp.single x 1 : (a : ι) → R) i : R)
            ((Finsupp.single x_1 1 : (a : κ) → R) j : R))
          (b.coord x ⊗ₜ[R] c.coord x_1))
    (b.coord i ⊗ₜ[R] c.coord j)
have h₀ : ∀ (b_1 : κ),
  Membership.mem (γ := Finset κ) Finset.univ b_1 →
    b_1 ≠ j →
      HSMul.hSMul (β := Dual R M ⊗[R] Dual R N)
          (HMul.hMul (α := R) (β := R) ((Finsupp.single i 1 : (a : ι) → R) i : R)
            ((Finsupp.single b_1 1 : (a : κ) → R) j : R))
          (b.coord i ⊗ₜ[R] c.coord b_1) =
        0
Tactic: rw [Finset.sum_eq_single i, Finset.sum_eq_single j]