awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.PiTensorProduct.Dual
Goal:
ι : Type u_1
R : Type u_2
M : ι → Type u_3
inst : CommSemiring R
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u_2, u_3} R (M i)
inst_3 : Fintype ι
f : (i : ι) → Dual.{u_2, u_3} R (M i)
m : (i : ι) → M i
⊢ Eq.{u_2 + 1} (α := R)
    (((compRight R (AlgEquiv.toLinearMap (constantBaseRingEquiv ι R)) ∘ₗ
                piTensorHomMap (s := M) (t := fun (i : ι) ↦ R) :
              (a : ⨂[R] (i : ι), Dual R (M i)) → Dual R (⨂[R] (i : ι), M i))
            ((tprod R (s := fun (i : ι) ↦ Dual.{u_2, u_3} R (M i)) :
                (a : (i : ι) → Dual R (M i)) → ⨂[R] (i : ι), Dual R (M i))
              fun (i : ι) ↦ f i) :
          (a : ⨂[R] (i : ι), M i) → R)
        (⨂ₜ[R] (i : ι), m i) :
      R)
    (∏ i : ι, (f i : (a : M i) → R) (m i) : R)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.PiTensorProduct.Dual
Goal:
ι : Type u_1
R : Type u_2
κ : ι → Type u_3
M : ι → Type u_4
inst : CommRing R
inst_1 : (i : ι) → AddCommGroup (M i)
inst_2 : (i : ι) → Module.{u_2, u_4} R (M i)
inst_3 : Fintype ι
inst_4 : (i : ι) → Fintype (κ i)
b : (i : ι) → Basis.{u_3, u_2, u_4} (κ i) R (M i)
f : Dual R (⨂[R] (i : ι), M i)
simp :
  Eq (α := ⨂[R] (i : ι), Dual.{u_2, u_4} R (M i))
    (∑ x : (i : ι) → κ i,
      HSMul.hSMul (α := R) (β := ⨂[R] (i : ι), Dual.{u_2, u_4} R (M i))
        ((f : (a : ⨂[R] (i : ι), M i) → R) (⨂ₜ[R] (i : ι), (b i : (a : κ i) → M i) (x i)) : R)
        ((tprod R (s := fun (i : ι) ↦ Dual.{u_2, u_4} R (M i)) :
            (a : (i : ι) → Dual R (M i)) → ⨂[R] (i : ι), Dual R (M i))
          fun (i : ι) ↦ (b i).coord (x i)))
    (∑ x : (i : ι) → κ i,
      HSMul.hSMul (α := R) (β := ⨂[R] (i : ι), Dual.{u_2, u_4} R (M i))
        ((f : (a : ⨂[R] (i : ι), M i) → R) (⨂ₜ[R] (i : ι), (b i : (a : κ i) → M i) (x i)) : R)
        ((tprod R (s := fun (i : ι) ↦ Dual.{u_2, u_4} R (M i)) :
            (a : (i : ι) → Dual R (M i)) → ⨂[R] (i : ι), Dual R (M i))
          fun (i : ι) ↦ (b i).coord (x i)))
⊢ Eq (α := ⨂[R] (i : ι), Dual.{u_2, u_4} R (M i))
    ((dualDistribInvOfBasis (κ := κ) (M := M) b : (a : Dual R (⨂[R] (i : ι), M i)) → ⨂[R] (i : ι), Dual R (M i)) f :
      ⨂[R] (i : ι), Dual.{u_2, u_4} R (M i))
    (∑ p : (i : ι) → κ i,
        HSMul.hSMul (α := R) (β := ⨂[R] (i : ι), Dual.{u_2, u_4} R (M i))
          ((f : (a : ⨂[R] (i : ι), M i) → R) (⨂ₜ[R] (i : ι), (b i : (a : κ i) → M i) (p i)) : R)
          ((tprod R (s := fun (i : ι) ↦ Dual.{u_2, u_4} R (M i)) :
              (a : (i : ι) → Dual R (M i)) → ⨂[R] (i : ι), Dual R (M i))
            fun (i : ι) ↦ ((b i).dualBasis : (a : κ i) → Dual R (M i)) (p i)) :
      ⨂[R] (i : ι), Dual.{u_2, u_4} R (M i))

Tactic:
simp only [dualDistribInvOfBasis, Basis.coe_dualBasis, ringLmapEquivSelf_symm_apply, coe_sum,
    coe_comp, coe_smulRight, End.one_apply, Finset.sum_apply, Function.comp_apply,
    applyₗ_apply_apply]

Premises used: Module.Basis.coe_dualBasis, LinearMap.ringLmapEquivSelf_symm_apply, Finset.sum_apply, LinearMap.coe_sum, Module.End.one_apply, LinearMap.coe_comp, Function.comp_apply, LinearMap.coe_smulRight, PiTensorProduct.dualDistribInvOfBasis, LinearMap.applyₗ_apply_apply
-- Module: Mathlib.LinearAlgebra.PiTensorProduct.Dual
Goal:
ι : Type u_1
R : Type u_2
κ : ι → Type u_3
M : ι → Type u_4
inst : CommRing R
inst_1 : (i : ι) → AddCommGroup (M i)
inst_2 : (i : ι) → Module.{u_2, u_4} R (M i)
inst_3 : Fintype ι
inst_4 : (i : ι) → Fintype (κ i)
b : (i : ι) → Basis.{u_3, u_2, u_4} (κ i) R (M i)
f : Dual R (⨂[R] (i : ι), M i)
⊢ Eq (α := ⨂[R] (i : ι), Dual.{u_2, u_4} R (M i))
    (∑ x : (i : ι) → κ i,
      HSMul.hSMul (α := R) (β := ⨂[R] (i : ι), Dual.{u_2, u_4} R (M i))
        ((f : (a : ⨂[R] (i : ι), M i) → R) (⨂ₜ[R] (i : ι), (b i : (a : κ i) → M i) (x i)) : R)
        ((tprod R (s := fun (i : ι) ↦ Dual.{u_2, u_4} R (M i)) :
            (a : (i : ι) → Dual R (M i)) → ⨂[R] (i : ι), Dual R (M i))
          fun (i : ι) ↦ (b i).coord (x i)))
    (∑ x : (i : ι) → κ i,
      HSMul.hSMul (α := R) (β := ⨂[R] (i : ι), Dual.{u_2, u_4} R (M i))
        ((f : (a : ⨂[R] (i : ι), M i) → R) (⨂ₜ[R] (i : ι), (b i : (a : κ i) → M i) (x i)) : R)
        ((tprod R (s := fun (i : ι) ↦ Dual.{u_2, u_4} R (M i)) :
            (a : (i : ι) → Dual R (M i)) → ⨂[R] (i : ι), Dual R (M i))
          fun (i : ι) ↦ (b i).coord (x i)))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.PiTensorProduct.Dual
Goal:
ι : Type u_1
R : Type u_2
κ : ι → Type u_3
M : ι → Type u_4
inst : CommRing R
inst_1 : (i : ι) → AddCommGroup (M i)
inst_2 : (i : ι) → Module.{u_2, u_4} R (M i)
inst_3 : Fintype ι
inst_4 : (i : ι) → Fintype (κ i)
b : (i : ι) → Basis.{u_3, u_2, u_4} (κ i) R (M i)
f : Dual R (⨂[R] (i : ι), M i)
⊢ Eq (α := ⨂[R] (i : ι), Dual.{u_2, u_4} R (M i))
    (∑ x : (i : ι) → κ i,
      HSMul.hSMul (α := R) (β := ⨂[R] (i : ι), Dual.{u_2, u_4} R (M i))
        ((f : (a : ⨂[R] (i : ι), M i) → R) (⨂ₜ[R] (i : ι), (b i : (a : κ i) → M i) (x i)) : R)
        ((tprod R (s := fun (i : ι) ↦ Dual.{u_2, u_4} R (M i)) :
            (a : (i : ι) → Dual R (M i)) → ⨂[R] (i : ι), Dual R (M i))
          fun (i : ι) ↦ (b i).coord (x i)))
    (∑ x : (i : ι) → κ i,
      HSMul.hSMul (α := R) (β := ⨂[R] (i : ι), Dual.{u_2, u_4} R (M i))
        ((f : (a : ⨂[R] (i : ι), M i) → R) (⨂ₜ[R] (i : ι), (b i : (a : κ i) → M i) (x i)) : R)
        ((tprod R (s := fun (i : ι) ↦ Dual.{u_2, u_4} R (M i)) :
            (a : (i : ι) → Dual R (M i)) → ⨂[R] (i : ι), Dual R (M i))
          fun (i : ι) ↦ (b i).coord (x i)))

Tactic:
convert! rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.PiTensorProduct.Dual
Goal:
ι : Type u_1
R : Type u_2
κ : ι → Type u_3
M : ι → Type u_4
inst : CommRing R
inst_1 : (i : ι) → AddCommGroup (M i)
inst_2 : (i : ι) → Module.{u_2, u_4} R (M i)
inst_3 : Finite ι
inst_4 : ∀ (i : ι), Finite.{u_3 + 1} (κ i)
b : (i : ι) → Basis.{u_3, u_2, u_4} (κ i) R (M i)
haveI : ∀ (this : Fintype ι), dualDistrib (M := M) ∘ₗ dualDistribInvOfBasis (κ := κ) (M := M) b = LinearMap.id
⊢ dualDistrib (M := M) ∘ₗ dualDistribInvOfBasis (κ := κ) (M := M) b = LinearMap.id

Tactic:
haveI := Fintype.ofFinite ι
-- Module: Mathlib.LinearAlgebra.PiTensorProduct.Dual
Goal:
ι : Type u_1
R : Type u_2
κ : ι → Type u_3
M : ι → Type u_4
inst : CommRing R
inst_1 : (i : ι) → AddCommGroup (M i)
inst_2 : (i : ι) → Module.{u_2, u_4} R (M i)
inst_3 : Finite ι
inst_4 : ∀ (i : ι), Finite.{u_3 + 1} (κ i)
b : (i : ι) → Basis.{u_3, u_2, u_4} (κ i) R (M i)
this : Fintype ι
haveI :
  ∀ (this : (i : ι) → Fintype (κ i)), dualDistrib (M := M) ∘ₗ dualDistribInvOfBasis (κ := κ) (M := M) b = LinearMap.id
⊢ dualDistrib (M := M) ∘ₗ dualDistribInvOfBasis (κ := κ) (M := M) b = LinearMap.id

Tactic:
haveI := fun i => Fintype.ofFinite (κ i)
-- Module: Mathlib.LinearAlgebra.PiTensorProduct.Dual
Goal:
ι : Type u_1
R : Type u_2
κ : ι → Type u_3
M : ι → Type u_4
inst : CommRing R
inst_1 : (i : ι) → AddCommGroup (M i)
inst_2 : (i : ι) → Module.{u_2, u_4} R (M i)
inst_3 : Finite ι
inst_4 : ∀ (i : ι), Finite.{u_3 + 1} (κ i)
b : (i : ι) → Basis.{u_3, u_2, u_4} (κ i) R (M i)
this_1 : Fintype ι
this : (i : ι) → Fintype (κ i)
⊢ dualDistrib (M := M) ∘ₗ dualDistribInvOfBasis (κ := κ) (M := M) b = LinearMap.id

Tactic:
(Basis.piTensorProduct b).dualBasis.ext (fun p ↦ ?_)

Premises used: Module.Basis.dualBasis, Basis.piTensorProduct, Module.Basis.ext
-- Module: Mathlib.LinearAlgebra.PiTensorProduct.Dual
Goal:
ι : Type u_1
R : Type u_2
κ : ι → Type u_3
M : ι → Type u_4
inst : CommRing R
inst_1 : (i : ι) → AddCommGroup (M i)
inst_2 : (i : ι) → Module.{u_2, u_4} R (M i)
inst_3 : Finite ι
inst_4 : ∀ (i : ι), Finite.{u_3 + 1} (κ i)
b : (i : ι) → Basis.{u_3, u_2, u_4} (κ i) R (M i)
this_1 : Fintype ι
this : (i : ι) → Fintype (κ i)
refine :
  ∀ (p : (i : ι) → κ i),
    Eq (α := Dual R (⨂[R] (i : ι), M i))
      ((dualDistrib (M := M) ∘ₗ dualDistribInvOfBasis (κ := κ) (M := M) b :
            (a : Dual R (⨂[R] (i : ι), M i)) → Dual R (⨂[R] (i : ι), M i))
          (((Basis.piTensorProduct (M := M) (κ := κ) b).dualBasis : (a : (i : ι) → κ i) → Dual R (⨂[R] (i : ι), M i))
            p) :
        Dual R (⨂[R] (i : ι), M i))
      ((LinearMap.id : (a : Dual R (⨂[R] (i : ι), M i)) → Dual R (⨂[R] (i : ι), M i))
          (((Basis.piTensorProduct (M := M) (κ := κ) b).dualBasis : (a : (i : ι) → κ i) → Dual R (⨂[R] (i : ι), M i))
            p) :
        Dual R (⨂[R] (i : ι), M i))
⊢ dualDistrib (M := M) ∘ₗ dualDistribInvOfBasis (κ := κ) (M := M) b = LinearMap.id

Tactic:
refine (Basis.piTensorProduct b).dualBasis.ext (fun p ↦ ?_)

Premises used: Module.Basis.dualBasis, Basis.piTensorProduct, Module.Basis.ext
-- Module: Mathlib.LinearAlgebra.PiTensorProduct.Dual
Goal:
ι : Type u_1
R : Type u_2
κ : ι → Type u_3
M : ι → Type u_4
inst : CommRing R
inst_1 : (i : ι) → AddCommGroup (M i)
inst_2 : (i : ι) → Module.{u_2, u_4} R (M i)
inst_3 : Finite ι
inst_4 : ∀ (i : ι), Finite.{u_3 + 1} (κ i)
b : (i : ι) → Basis.{u_3, u_2, u_4} (κ i) R (M i)
this_1 : Fintype ι
this : (i : ι) → Fintype (κ i)
p : (i : ι) → κ i
⊢ Eq (α := Dual R (⨂[R] (i : ι), M i))
    ((dualDistrib (M := M) ∘ₗ dualDistribInvOfBasis (κ := κ) (M := M) b :
          (a : Dual R (⨂[R] (i : ι), M i)) → Dual R (⨂[R] (i : ι), M i))
        (((Basis.piTensorProduct (M := M) (κ := κ) b).dualBasis : (a : (i : ι) → κ i) → Dual R (⨂[R] (i : ι), M i)) p) :
      Dual R (⨂[R] (i : ι), M i))
    ((LinearMap.id : (a : Dual R (⨂[R] (i : ι), M i)) → Dual R (⨂[R] (i : ι), M i))
        (((Basis.piTensorProduct (M := M) (κ := κ) b).dualBasis : (a : (i : ι) → κ i) → Dual R (⨂[R] (i : ι), M i)) p) :
      Dual R (⨂[R] (i : ι), M i))

Tactic:
(Basis.piTensorProduct b).ext (fun q ↦ ?_)

Premises used: Basis.piTensorProduct, Module.Basis.ext
-- Module: Mathlib.LinearAlgebra.PiTensorProduct.Dual
Goal:
ι : Type u_1
R : Type u_2
κ : ι → Type u_3
M : ι → Type u_4
inst : CommRing R
inst_1 : (i : ι) → AddCommGroup (M i)
inst_2 : (i : ι) → Module.{u_2, u_4} R (M i)
inst_3 : Finite ι
inst_4 : ∀ (i : ι), Finite.{u_3 + 1} (κ i)
b : (i : ι) → Basis.{u_3, u_2, u_4} (κ i) R (M i)
this_1 : Fintype ι
this : (i : ι) → Fintype (κ i)
p : (i : ι) → κ i
refine :
  ∀ (q : (i : ι) → κ i),
    Eq.{u_2 + 1} (α := R)
      ((((dualDistrib (M := M) ∘ₗ dualDistribInvOfBasis (κ := κ) (M := M) b :
                  (a : Dual R (⨂[R] (i : ι), M i)) → Dual R (⨂[R] (i : ι), M i))
                (((Basis.piTensorProduct (M := M) (κ := κ) b).dualBasis :
                    (a : (i : ι) → κ i) → Dual R (⨂[R] (i : ι), M i))
                  p) :
              Dual R (⨂[R] (i : ι), M i)) :
            (a : ⨂[R] (i : ι), M i) → R)
          ((Basis.piTensorProduct (M := M) (κ := κ) b : (a : (i : ι) → κ i) → ⨂[R] (i : ι), M i) q :
            ⨂[R] (i : ι), M i) :
        R)
      ((((LinearMap.id : (a : Dual R (⨂[R] (i : ι), M i)) → Dual R (⨂[R] (i : ι), M i))
                (((Basis.piTensorProduct (M := M) (κ := κ) b).dualBasis :
                    (a : (i : ι) → κ i) → Dual R (⨂[R] (i : ι), M i))
                  p) :
              Dual R (⨂[R] (i : ι), M i)) :
            (a : ⨂[R] (i : ι), M i) → R)
          ((Basis.piTensorProduct (M := M) (κ := κ) b : (a : (i : ι) → κ i) → ⨂[R] (i : ι), M i) q :
            ⨂[R] (i : ι), M i) :
        R)
⊢ Eq (α := Dual R (⨂[R] (i : ι), M i))
    ((dualDistrib (M := M) ∘ₗ dualDistribInvOfBasis (κ := κ) (M := M) b :
          (a : Dual R (⨂[R] (i : ι), M i)) → Dual R (⨂[R] (i : ι), M i))
        (((Basis.piTensorProduct (M := M) (κ := κ) b).dualBasis : (a : (i : ι) → κ i) → Dual R (⨂[R] (i : ι), M i)) p) :
      Dual R (⨂[R] (i : ι), M i))
    ((LinearMap.id : (a : Dual R (⨂[R] (i : ι), M i)) → Dual R (⨂[R] (i : ι), M i))
        (((Basis.piTensorProduct (M := M) (κ := κ) b).dualBasis : (a : (i : ι) → κ i) → Dual R (⨂[R] (i : ι), M i)) p) :
      Dual R (⨂[R] (i : ι), M i))

Tactic:
refine (Basis.piTensorProduct b).ext (fun q ↦ ?_)

Premises used: Basis.piTensorProduct, Module.Basis.ext
-- Module: Mathlib.LinearAlgebra.PiTensorProduct.Dual
Goal:
ι : Type u_1
R : Type u_2
κ : ι → Type u_3
M : ι → Type u_4
inst : CommRing R
inst_1 : (i : ι) → AddCommGroup (M i)
inst_2 : (i : ι) → Module.{u_2, u_4} R (M i)
inst_3 : Finite ι
inst_4 : ∀ (i : ι), Finite.{u_3 + 1} (κ i)
b : (i : ι) → Basis.{u_3, u_2, u_4} (κ i) R (M i)
this_1 : Fintype ι
this : (i : ι) → Fintype (κ i)
p q : (i : ι) → κ i
⊢ Eq.{u_2 + 1} (α := R)
    ((((dualDistrib (M := M) ∘ₗ dualDistribInvOfBasis (κ := κ) (M := M) b :
                (a : Dual R (⨂[R] (i : ι), M i)) → Dual R (⨂[R] (i : ι), M i))
              (((Basis.piTensorProduct (M := M) (κ := κ) b).dualBasis :
                  (a : (i : ι) → κ i) → Dual R (⨂[R] (i : ι), M i))
                p) :
            Dual R (⨂[R] (i : ι), M i)) :
          (a : ⨂[R] (i : ι), M i) → R)
        ((Basis.piTensorProduct (M := M) (κ := κ) b : (a : (i : ι) → κ i) → ⨂[R] (i : ι), M i) q : ⨂[R] (i : ι), M i) :
      R)
    ((((LinearMap.id : (a : Dual R (⨂[R] (i : ι), M i)) → Dual R (⨂[R] (i : ι), M i))
              (((Basis.piTensorProduct (M := M) (κ := κ) b).dualBasis :
                  (a : (i : ι) → κ i) → Dual R (⨂[R] (i : ι), M i))
                p) :
            Dual R (⨂[R] (i : ι), M i)) :
          (a : ⨂[R] (i : ι), M i) → R)
        ((Basis.piTensorProduct (M := M) (κ := κ) b : (a : (i : ι) → κ i) → ⨂[R] (i : ι), M i) q : ⨂[R] (i : ι), M i) :
      R)

Tactic:
simp [Finsupp.single_apply, Fintype.prod_ite_zero, ← funext_iff]

Premises used: funext_iff, Fintype.prod_ite_zero, Finsupp.single_apply
-- Module: Mathlib.LinearAlgebra.PiTensorProduct.Dual
Goal:
ι : Type u_1
R : Type u_2
κ : ι → Type u_3
M : ι → Type u_4
inst : CommRing R
inst_1 : (i : ι) → AddCommGroup (M i)
inst_2 : (i : ι) → Module.{u_2, u_4} R (M i)
inst_3 : Finite ι
inst_4 : ∀ (i : ι), Finite.{u_3 + 1} (κ i)
b : (i : ι) → Basis.{u_3, u_2, u_4} (κ i) R (M i)
this_1 : Fintype ι
this : (i : ι) → Fintype (κ i)
refine :
  ∀ (p : (i : ι) → κ i),
    Eq (α := Dual R (⨂[R] (i : ι), M i))
      ((dualDistrib (M := M) ∘ₗ dualDistribInvOfBasis (κ := κ) (M := M) b :
            (a : Dual R (⨂[R] (i : ι), M i)) → Dual R (⨂[R] (i : ι), M i))
          (((Basis.piTensorProduct (M := M) (κ := κ) b).dualBasis : (a : (i : ι) → κ i) → Dual R (⨂[R] (i : ι), M i))
            p) :
        Dual R (⨂[R] (i : ι), M i))
      ((LinearMap.id : (a : Dual R (⨂[R] (i : ι), M i)) → Dual R (⨂[R] (i : ι), M i))
          (((Basis.piTensorProduct (M := M) (κ := κ) b).dualBasis : (a : (i : ι) → κ i) → Dual R (⨂[R] (i : ι), M i))
            p) :
        Dual R (⨂[R] (i : ι), M i))
refine₁ :
  ∀ (p q : (i : ι) → κ i),
    Eq.{u_2 + 1} (α := R)
      ((((dualDistrib (M := M) ∘ₗ dualDistribInvOfBasis (κ := κ) (M := M) b :
                  (a : Dual R (⨂[R] (i : ι), M i)) → Dual R (⨂[R] (i : ι), M i))
                (((Basis.piTensorProduct (M := M) (κ := κ) b).dualBasis :
                    (a : (i : ι) → κ i) → Dual R (⨂[R] (i : ι), M i))
                  p) :
              Dual R (⨂[R] (i : ι), M i)) :
            (a : ⨂[R] (i : ι), M i) → R)
          ((Basis.piTensorProduct (M := M) (κ := κ) b : (a : (i : ι) → κ i) → ⨂[R] (i : ι), M i) q :
            ⨂[R] (i : ι), M i) :
        R)
      ((((LinearMap.id : (a : Dual R (⨂[R] (i : ι), M i)) → Dual R (⨂[R] (i : ι), M i))
                (((Basis.piTensorProduct (M := M) (κ := κ) b).dualBasis :
                    (a : (i : ι) → κ i) → Dual R (⨂[R] (i : ι), M i))
                  p) :
              Dual R (⨂[R] (i : ι), M i)) :
            (a : ⨂[R] (i : ι), M i) → R)
          ((Basis.piTensorProduct (M := M) (κ := κ) b : (a : (i : ι) → κ i) → ⨂[R] (i : ι), M i) q :
            ⨂[R] (i : ι), M i) :
        R)
⊢ dualDistrib (M := M) ∘ₗ dualDistribInvOfBasis (κ := κ) (M := M) b = LinearMap.id

Tactic:
classical
  refine (Basis.piTensorProduct b).dualBasis.ext (fun p ↦ ?_)
  refine (Basis.piTensorProduct b).ext (fun q ↦ ?_)
  simp [Finsupp.single_apply, Fintype.prod_ite_zero, ← funext_iff]

Premises used: funext_iff, Fintype.prod_ite_zero, Finsupp.single_apply, Basis.piTensorProduct, Module.Basis.ext
-- Module: Mathlib.LinearAlgebra.PiTensorProduct.Dual
Goal:
ι : Type u_1
R : Type u_2
κ : ι → Type u_3
M : ι → Type u_4
inst : CommRing R
inst_1 : (i : ι) → AddCommGroup (M i)
inst_2 : (i : ι) → Module.{u_2, u_4} R (M i)
inst_3 : Finite ι
inst_4 : ∀ (i : ι), Finite.{u_3 + 1} (κ i)
b : (i : ι) → Basis.{u_3, u_2, u_4} (κ i) R (M i)
haveI : ∀ (this : Fintype ι), dualDistribInvOfBasis (κ := κ) (M := M) b ∘ₗ dualDistrib (M := M) = LinearMap.id
⊢ dualDistribInvOfBasis (κ := κ) (M := M) b ∘ₗ dualDistrib (M := M) = LinearMap.id

Tactic:
haveI := Fintype.ofFinite ι
-- Module: Mathlib.LinearAlgebra.PiTensorProduct.Dual
Goal:
ι : Type u_1
R : Type u_2
κ : ι → Type u_3
M : ι → Type u_4
inst : CommRing R
inst_1 : (i : ι) → AddCommGroup (M i)
inst_2 : (i : ι) → Module.{u_2, u_4} R (M i)
inst_3 : Finite ι
inst_4 : ∀ (i : ι), Finite.{u_3 + 1} (κ i)
b : (i : ι) → Basis.{u_3, u_2, u_4} (κ i) R (M i)
this : Fintype ι
haveI :
  ∀ (this : (i : ι) → Fintype (κ i)), dualDistribInvOfBasis (κ := κ) (M := M) b ∘ₗ dualDistrib (M := M) = LinearMap.id
⊢ dualDistribInvOfBasis (κ := κ) (M := M) b ∘ₗ dualDistrib (M := M) = LinearMap.id

Tactic:
haveI := fun i => Fintype.ofFinite (κ i)
-- Module: Mathlib.LinearAlgebra.PiTensorProduct.Dual
Goal:
ι : Type u_1
R : Type u_2
κ : ι → Type u_3
M : ι → Type u_4
inst : CommRing R
inst_1 : (i : ι) → AddCommGroup (M i)
inst_2 : (i : ι) → Module.{u_2, u_4} R (M i)
inst_3 : Finite ι
inst_4 : ∀ (i : ι), Finite.{u_3 + 1} (κ i)
b : (i : ι) → Basis.{u_3, u_2, u_4} (κ i) R (M i)
this_1 : Fintype ι
this : (i : ι) → Fintype (κ i)
⊢ dualDistribInvOfBasis (κ := κ) (M := M) b ∘ₗ dualDistrib (M := M) = LinearMap.id

Tactic:
(Basis.piTensorProduct (fun i => (b i).dualBasis)).ext (fun p ↦ ?_)

Premises used: Module.Basis.dualBasis, Basis.piTensorProduct, Module.Basis.ext
-- Module: Mathlib.LinearAlgebra.PiTensorProduct.Dual
Goal:
ι : Type u_1
R : Type u_2
κ : ι → Type u_3
M : ι → Type u_4
inst : CommRing R
inst_1 : (i : ι) → AddCommGroup (M i)
inst_2 : (i : ι) → Module.{u_2, u_4} R (M i)
inst_3 : Finite ι
inst_4 : ∀ (i : ι), Finite.{u_3 + 1} (κ i)
b : (i : ι) → Basis.{u_3, u_2, u_4} (κ i) R (M i)
this_1 : Fintype ι
this : (i : ι) → Fintype (κ i)
refine :
  ∀ (p : (i : ι) → κ i),
    Eq (α := ⨂[R] (i : ι), Dual.{u_2, u_4} R (M i))
      ((dualDistribInvOfBasis (κ := κ) (M := M) b ∘ₗ dualDistrib (M := M) :
            (a : ⨂[R] (i : ι), Dual R (M i)) → ⨂[R] (i : ι), Dual R (M i))
          ((Basis.piTensorProduct (M := fun (i : ι) ↦ Dual.{u_2, u_4} R (M i)) (κ := κ) fun (i : ι) ↦ (b i).dualBasis :
              (a : (i : ι) → κ i) → ⨂[R] (i : ι), Dual R (M i))
            p) :
        ⨂[R] (i : ι), Dual.{u_2, u_4} R (M i))
      ((LinearMap.id : (a : ⨂[R] (i : ι), Dual R (M i)) → ⨂[R] (i : ι), Dual R (M i))
          ((Basis.piTensorProduct (M := fun (i : ι) ↦ Dual.{u_2, u_4} R (M i)) (κ := κ) fun (i : ι) ↦ (b i).dualBasis :
              (a : (i : ι) → κ i) → ⨂[R] (i : ι), Dual R (M i))
            p) :
        ⨂[R] (i : ι), Dual.{u_2, u_4} R (M i))
⊢ dualDistribInvOfBasis (κ := κ) (M := M) b ∘ₗ dualDistrib (M := M) = LinearMap.id

Tactic:
refine (Basis.piTensorProduct (fun i => (b i).dualBasis)).ext (fun p ↦ ?_)

Premises used: Module.Basis.dualBasis, Basis.piTensorProduct, Module.Basis.ext
-- Module: Mathlib.LinearAlgebra.PiTensorProduct.Dual
Goal:
ι : Type u_1
R : Type u_2
κ : ι → Type u_3
M : ι → Type u_4
inst : CommRing R
inst_1 : (i : ι) → AddCommGroup (M i)
inst_2 : (i : ι) → Module.{u_2, u_4} R (M i)
inst_3 : Finite ι
inst_4 : ∀ (i : ι), Finite.{u_3 + 1} (κ i)
b : (i : ι) → Basis.{u_3, u_2, u_4} (κ i) R (M i)
this_1 : Fintype ι
this : (i : ι) → Fintype (κ i)
p : (i : ι) → κ i
⊢ Eq (α := ⨂[R] (i : ι), Dual.{u_2, u_4} R (M i))
    ((dualDistribInvOfBasis (κ := κ) (M := M) b ∘ₗ dualDistrib (M := M) :
          (a : ⨂[R] (i : ι), Dual R (M i)) → ⨂[R] (i : ι), Dual R (M i))
        ((Basis.piTensorProduct (M := fun (i : ι) ↦ Dual.{u_2, u_4} R (M i)) (κ := κ) fun (i : ι) ↦ (b i).dualBasis :
            (a : (i : ι) → κ i) → ⨂[R] (i : ι), Dual R (M i))
          p) :
      ⨂[R] (i : ι), Dual.{u_2, u_4} R (M i))
    ((LinearMap.id : (a : ⨂[R] (i : ι), Dual R (M i)) → ⨂[R] (i : ι), Dual R (M i))
        ((Basis.piTensorProduct (M := fun (i : ι) ↦ Dual.{u_2, u_4} R (M i)) (κ := κ) fun (i : ι) ↦ (b i).dualBasis :
            (a : (i : ι) → κ i) → ⨂[R] (i : ι), Dual R (M i))
          p) :
      ⨂[R] (i : ι), Dual.{u_2, u_4} R (M i))

Tactic:
(Basis.piTensorProduct (fun i => (b i).dualBasis)).ext_elem (fun q ↦ ?_)

Premises used: Module.Basis.ext_elem, Module.Basis.dualBasis, Basis.piTensorProduct
-- Module: Mathlib.LinearAlgebra.PiTensorProduct.Dual
Goal:
ι : Type u_1
R : Type u_2
κ : ι → Type u_3
M : ι → Type u_4
inst : CommRing R
inst_1 : (i : ι) → AddCommGroup (M i)
inst_2 : (i : ι) → Module.{u_2, u_4} R (M i)
inst_3 : Finite ι
inst_4 : ∀ (i : ι), Finite.{u_3 + 1} (κ i)
b : (i : ι) → Basis.{u_3, u_2, u_4} (κ i) R (M i)
this_1 : Fintype ι
this : (i : ι) → Fintype (κ i)
p : (i : ι) → κ i
refine :
  ∀ (q : (i : ι) → κ i),
    Eq.{u_2 + 1} (α := R)
      ((((Basis.repr
                    (Basis.piTensorProduct (M := fun (i : ι) ↦ Dual.{u_2, u_4} R (M i)) (κ := κ) fun (i : ι) ↦
                      (b i).dualBasis) :
                  (a : ⨂[R] (i : ι), Dual R (M i)) → ((i : ι) → κ i) →₀ R)
                ((dualDistribInvOfBasis (κ := κ) (M := M) b ∘ₗ dualDistrib (M := M) :
                    (a : ⨂[R] (i : ι), Dual R (M i)) → ⨂[R] (i : ι), Dual R (M i))
                  ((Basis.piTensorProduct (M := fun (i : ι) ↦ Dual.{u_2, u_4} R (M i)) (κ := κ) fun (i : ι) ↦
                        (b i).dualBasis :
                      (a : (i : ι) → κ i) → ⨂[R] (i : ι), Dual R (M i))
                    p)) :
              ((i : ι) → κ i) →₀ R) :
            (a : (i : ι) → κ i) → R)
          q :
        R)
      ((((Basis.repr
                    (Basis.piTensorProduct (M := fun (i : ι) ↦ Dual.{u_2, u_4} R (M i)) (κ := κ) fun (i : ι) ↦
                      (b i).dualBasis) :
                  (a : ⨂[R] (i : ι), Dual R (M i)) → ((i : ι) → κ i) →₀ R)
                ((LinearMap.id : (a : ⨂[R] (i : ι), Dual R (M i)) → ⨂[R] (i : ι), Dual R (M i))
                  ((Basis.piTensorProduct (M := fun (i : ι) ↦ Dual.{u_2, u_4} R (M i)) (κ := κ) fun (i : ι) ↦
                        (b i).dualBasis :
                      (a : (i : ι) → κ i) → ⨂[R] (i : ι), Dual R (M i))
                    p)) :
              ((i : ι) → κ i) →₀ R) :
            (a : (i : ι) → κ i) → R)
          q :
        R)
⊢ Eq (α := ⨂[R] (i : ι), Dual.{u_2, u_4} R (M i))
    ((dualDistribInvOfBasis (κ := κ) (M := M) b ∘ₗ dualDistrib (M := M) :
          (a : ⨂[R] (i : ι), Dual R (M i)) → ⨂[R] (i : ι), Dual R (M i))
        ((Basis.piTensorProduct (M := fun (i : ι) ↦ Dual.{u_2, u_4} R (M i)) (κ := κ) fun (i : ι) ↦ (b i).dualBasis :
            (a : (i : ι) → κ i) → ⨂[R] (i : ι), Dual R (M i))
          p) :
      ⨂[R] (i : ι), Dual.{u_2, u_4} R (M i))
    ((LinearMap.id : (a : ⨂[R] (i : ι), Dual R (M i)) → ⨂[R] (i : ι), Dual R (M i))
        ((Basis.piTensorProduct (M := fun (i : ι) ↦ Dual.{u_2, u_4} R (M i)) (κ := κ) fun (i : ι) ↦ (b i).dualBasis :
            (a : (i : ι) → κ i) → ⨂[R] (i : ι), Dual R (M i))
          p) :
      ⨂[R] (i : ι), Dual.{u_2, u_4} R (M i))

Tactic:
refine (Basis.piTensorProduct (fun i => (b i).dualBasis)).ext_elem (fun q ↦ ?_)

Premises used: Module.Basis.ext_elem, Module.Basis.dualBasis, Basis.piTensorProduct