awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.PiTensorProduct.Dual (goal)
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))
    ((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))
have 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)))
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.PiTensorProduct.Dual (goal)
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)
⊢ dualDistrib (M := M) ∘ₗ dualDistribInvOfBasis (κ := κ) (M := M) b = LinearMap.id
have haveI : ∀ (this : Fintype ι), dualDistrib (M := M) ∘ₗ dualDistribInvOfBasis (κ := κ) (M := M) b = LinearMap.id
Tactic: haveI := Fintype.ofFinite ι
-- Lean 4 proof step from Mathlib.LinearAlgebra.PiTensorProduct.Dual (goal)
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 ι
⊢ dualDistrib (M := M) ∘ₗ dualDistribInvOfBasis (κ := κ) (M := M) b = LinearMap.id
have haveI : ∀ (this : (i : ι) → Fintype (κ i)), dualDistrib (M := M) ∘ₗ dualDistribInvOfBasis (κ := κ) (M := M) b = LinearMap.id
Tactic: haveI := fun i => Fintype.ofFinite (κ i)
-- Lean 4 proof step from Mathlib.LinearAlgebra.PiTensorProduct.Dual (goal)
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
have 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))
Tactic: refine (Basis.piTensorProduct b).dualBasis.ext (fun p ↦ ?_)
-- Lean 4 proof step from Mathlib.LinearAlgebra.PiTensorProduct.Dual (goal)
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))
have 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)
Tactic: refine (Basis.piTensorProduct b).ext (fun q ↦ ?_)
-- Lean 4 proof step from Mathlib.LinearAlgebra.PiTensorProduct.Dual (goal)
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
have 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))
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.PiTensorProduct.Dual (goal)
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
have 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)
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.PiTensorProduct.Dual (goal)
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)
⊢ dualDistribInvOfBasis (κ := κ) (M := M) b ∘ₗ dualDistrib (M := M) = LinearMap.id
have haveI : ∀ (this : Fintype ι), dualDistribInvOfBasis (κ := κ) (M := M) b ∘ₗ dualDistrib (M := M) = LinearMap.id
Tactic: haveI := Fintype.ofFinite ι
-- Lean 4 proof step from Mathlib.LinearAlgebra.PiTensorProduct.Dual (goal)
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 ι
⊢ dualDistribInvOfBasis (κ := κ) (M := M) b ∘ₗ dualDistrib (M := M) = LinearMap.id
have haveI : ∀ (this : (i : ι) → Fintype (κ i)), dualDistribInvOfBasis (κ := κ) (M := M) b ∘ₗ dualDistrib (M := M) = LinearMap.id
Tactic: haveI := fun i => Fintype.ofFinite (κ i)
-- Lean 4 proof step from Mathlib.LinearAlgebra.PiTensorProduct.Dual (goal)
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
have 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))
Tactic: refine (Basis.piTensorProduct (fun i => (b i).dualBasis)).ext (fun p ↦ ?_)
-- Lean 4 proof step from Mathlib.LinearAlgebra.PiTensorProduct.Dual (goal)
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))
have 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)
Tactic: refine (Basis.piTensorProduct (fun i => (b i).dualBasis)).ext_elem (fun q ↦ ?_)
-- Lean 4 proof step from Mathlib.LinearAlgebra.PiTensorProduct.Dual (goal)
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
have 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))
Tactic: classical
  refine (Basis.piTensorProduct (fun i => (b i).dualBasis)).ext (fun p ↦ ?_)
  refine (Basis.piTensorProduct (fun i => (b i).dualBasis)).ext_elem (fun q ↦ ?_)
  simp [Finsupp.single_apply, Fintype.prod_ite_zero, ← funext_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.PiTensorProduct.Dual (goal)
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
have refine₁ : ∀ (p 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)
Tactic: classical
  refine (Basis.piTensorProduct (fun i => (b i).dualBasis)).ext (fun p ↦ ?_)
  refine (Basis.piTensorProduct (fun i => (b i).dualBasis)).ext_elem (fun q ↦ ?_)
  simp [Finsupp.single_apply, Fintype.prod_ite_zero, ← funext_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.PiTensorProduct (goal)
Goal:
ι : Type u_1
R : Type u_4
inst : CommSemiring R
R₁ : Type u_5
s : ι → Type u_7
inst_1 : (i : ι) → AddCommMonoid (s i)
inst_2 : (i : ι) → Module.{u_4, u_7} R (s i)
inst_3 : DecidableEq ι
z : R
f : (i : ι) → s i
i : ι
r : R₁
inst_4 : SMul R₁ R
inst_5 : IsScalarTower R₁ R R
inst_6 : SMul.{u_5, u_7} R₁ (s i)
inst_7 : IsScalarTower.{u_5, u_4, u_7} R₁ R (s i)
⊢ r • z = HSMul.hSMul (β := R) r 1 * z
have rw : r • z = r • (1 * z)
Tactic: rw [smul_mul_assoc, one_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.PiTensorProduct (goal)
Goal:
ι : Type u_1
R : Type u_4
inst : CommSemiring R
R₁ : Type u_5
s : ι → Type u_7
inst_1 : (i : ι) → AddCommMonoid (s i)
inst_2 : (i : ι) → Module.{u_4, u_7} R (s i)
inst_3 : DecidableEq ι
z : R
f : (i : ι) → s i
i : ι
r : R₁
inst_4 : SMul R₁ R
inst_5 : IsScalarTower R₁ R R
inst_6 : SMul.{u_5, u_7} R₁ (s i)
inst_7 : IsScalarTower.{u_5, u_4, u_7} R₁ R (s i)
rw : r • z = r • (1 * z)
⊢ r • z = HSMul.hSMul (β := R) r 1 * z
have rw₁ : r • z = r • z
Tactic: rw [smul_mul_assoc, one_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.PiTensorProduct (hypothesis)
Goal:
ι : Type u_1
R : Type u_4
inst : CommSemiring R
R₁ : Type u_5
s : ι → Type u_7
inst_1 : (i : ι) → AddCommMonoid (s i)
inst_2 : (i : ι) → Module.{u_4, u_7} R (s i)
inst_3 : DecidableEq ι
z : R
f : (i : ι) → s i
i : ι
r : R₁
inst_4 : SMul R₁ R
inst_5 : IsScalarTower R₁ R R
inst_6 : SMul.{u_5, u_7} R₁ (s i)
inst_7 : IsScalarTower.{u_5, u_4, u_7} R₁ R (s i)
⊢ Eq (α := ⨂[R] (i : ι), s i) (tprodCoeff R (s := s) z (update (β := s) f i (r • f i)))
    (tprodCoeff R (s := s) (r • z) f)
have h₁ : r • z = HSMul.hSMul (β := R) r 1 * z
Tactic: have h₁ : r • z = r • (1 : R) * z := by rw [smul_mul_assoc, one_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.PiTensorProduct (hypothesis)
Goal:
ι : Type u_1
R : Type u_4
inst : CommSemiring R
R₁ : Type u_5
s : ι → Type u_7
inst_1 : (i : ι) → AddCommMonoid (s i)
inst_2 : (i : ι) → Module.{u_4, u_7} R (s i)
inst_3 : DecidableEq ι
z : R
f : (i : ι) → s i
i : ι
r : R₁
inst_4 : SMul R₁ R
inst_5 : IsScalarTower R₁ R R
inst_6 : SMul.{u_5, u_7} R₁ (s i)
inst_7 : IsScalarTower.{u_5, u_4, u_7} R₁ R (s i)
h₁ : r • z = HSMul.hSMul (β := R) r 1 * z
⊢ Eq (α := ⨂[R] (i : ι), s i) (tprodCoeff R (s := s) z (update (β := s) f i (r • f i)))
    (tprodCoeff R (s := s) (r • z) f)
have h₂ : r • f i = HSMul.hSMul (β := R) r 1 • f i
Tactic: have h₂ : r • f i = (r • (1 : R)) • f i := (smul_one_smul _ _ _).symm
-- Lean 4 proof step from Mathlib.LinearAlgebra.PiTensorProduct (goal)
Goal:
ι : Type u_1
R : Type u_4
inst : CommSemiring R
R₁ : Type u_5
s : ι → Type u_7
inst_1 : (i : ι) → AddCommMonoid (s i)
inst_2 : (i : ι) → Module.{u_4, u_7} R (s i)
inst_3 : DecidableEq ι
z : R
f : (i : ι) → s i
i : ι
r : R₁
inst_4 : SMul R₁ R
inst_5 : IsScalarTower R₁ R R
inst_6 : SMul.{u_5, u_7} R₁ (s i)
inst_7 : IsScalarTower.{u_5, u_4, u_7} R₁ R (s i)
h₁ : r • z = HSMul.hSMul (β := R) r 1 * z
h₂ : r • f i = HSMul.hSMul (β := R) r 1 • f i
⊢ Eq (α := ⨂[R] (i : ι), s i) (tprodCoeff R (s := s) z (update (β := s) f i (r • f i)))
    (tprodCoeff R (s := s) (r • z) f)
have rw : Eq (α := ⨂[R] (i : ι), s i) (tprodCoeff R (s := s) z (update (β := s) f i (HSMul.hSMul (β := R) r 1 • f i)))
  (tprodCoeff R (s := s) (HSMul.hSMul (β := R) r 1 * z) f)
Tactic: rw [h₁, h₂]