awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Pi (goal)
Goal:
R : Type u
inst : Semiring R
ι : Type v
inst_1 : Finite ι
motive : (N : Type u) → [inst_4 : AddCommMonoid N] → [Module R N] → Prop
motive' : (N : Type (max u v)) → [inst_4 : AddCommMonoid N] → [Module R N] → Prop
equiv :
  ∀ {N : Type u} {N' : Type (max u v)} [inst_4 : AddCommMonoid N] [inst_5 : AddCommMonoid N'] [inst_6 : Module R N]
    [inst_7 : Module R N'] (a : N ≃ₗ[R] N'), motive N → motive' N'
equiv' :
  ∀ {N N' : Type (max u v)} [inst_4 : AddCommMonoid N] [inst_5 : AddCommMonoid N'] [inst_6 : Module R N]
    [inst_7 : Module R N'] (a : N ≃ₗ[R] N'), motive' N → motive' N'
unit : motive PUnit.{u + 1}
prod :
  ∀ {N : Type u} {N' : Type (max u v)} [inst_4 : AddCommMonoid N] [inst_5 : AddCommMonoid N'] [inst_6 : Module R N]
    [inst_7 : Module R N'], motive N → motive' N' → motive' (N × N')
M : ι → Type u
inst_2 : (i : ι) → AddCommMonoid (M i)
inst_3 : (i : ι) → Module R (M i)
h : ∀ (i : ι), motive (M i)
intro : ∀ (val : Fintype ι), motive' ((i : ι) → M i)
intro₁ :
  ∀ (val : Fintype ι) (M : ι → Type u) [inst_4 : (i : ι) → AddCommMonoid (M i)] [inst_5 : (i : ι) → Module R (M i)]
    (h : ∀ (i : ι), motive (M i)), motive' ((i : ι) → M i)
⊢ motive' ((i : ι) → M i)
have intro₂ : ∀ (val : Fintype ι) (α : Type v) (x : Fintype α)
  (h :
    ∀ (M : α → Type u) [inst_4 : (i : α) → AddCommMonoid (M i)] [inst_5 : (i : α) → Module R (M i)]
      (h : ∀ (i : α), motive (M i)), motive' ((i : α) → M i))
  (M : Option α → Type u) (x : (i : Option α) → AddCommMonoid (M i)) (x_1 : (i : Option α) → Module R (M i))
  (hn : ∀ (i : Option α), motive (M i)), motive' ((i : Option α) → M i)
Tactic: classical
  cases nonempty_fintype ι
  revert M
  refine Fintype.induction_empty_option
    (fun α β _ e h M _ _ hM ↦ equiv' (LinearEquiv.piCongrLeft R M e) <| h _ fun i ↦ hM _)
    (fun M _ _ _ ↦ equiv default unit) (fun α _ h M _ _ hn ↦ ?_) ι
  exact equiv' (LinearEquiv.piOptionEquivProd R).symm <| prod (hn _) (h _ fun i ↦ hn i)
Cleared hypotheses: M, inst_2, inst_3, h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Pi (goal)
Goal:
ι : Type v
inst : Finite ι
R : Type u_1
inst_1 : Ring R
motive : (N : Type u) → [inst : AddCommGroup N] → [Module R N] → Prop
motive' : (N : Type (max u v)) → [inst : AddCommGroup N] → [Module R N] → Prop
equiv :
  ∀ {N : Type u} {N' : Type (max u v)} [inst : AddCommGroup N] [inst_4 : AddCommGroup N'] [inst_5 : Module R N]
    [inst_6 : Module R N'] (a : N ≃ₗ[R] N'), motive N → motive' N'
equiv' :
  ∀ {N N' : Type (max u v)} [inst : AddCommGroup N] [inst_4 : AddCommGroup N'] [inst_5 : Module R N]
    [inst_6 : Module R N'] (a : N ≃ₗ[R] N'), motive' N → motive' N'
unit : motive PUnit.{u + 1}
prod :
  ∀ {N : Type u} {N' : Type (max u v)} [inst : AddCommGroup N] [inst_4 : AddCommGroup N'] [inst_5 : Module R N]
    [inst_6 : Module R N'], motive N → motive' N' → motive' (N × N')
M : ι → Type u
inst_2 : (i : ι) → AddCommGroup (M i)
inst_3 : (i : ι) → Module.{u_1, u} R (M i)
h : ∀ (i : ι), motive (M i)
⊢ motive' ((i : ι) → M i)
have intro : ∀ (val : Fintype ι), motive' ((i : ι) → M i)
Tactic: cases nonempty_fintype ι
-- Lean 4 proof step from Mathlib.LinearAlgebra.Pi (goal)
Goal:
ι : Type v
inst : Finite ι
R : Type u_1
inst_1 : Ring R
motive : (N : Type u) → [inst : AddCommGroup N] → [Module R N] → Prop
motive' : (N : Type (max u v)) → [inst : AddCommGroup N] → [Module R N] → Prop
equiv :
  ∀ {N : Type u} {N' : Type (max u v)} [inst : AddCommGroup N] [inst_4 : AddCommGroup N'] [inst_5 : Module R N]
    [inst_6 : Module R N'] (a : N ≃ₗ[R] N'), motive N → motive' N'
equiv' :
  ∀ {N N' : Type (max u v)} [inst : AddCommGroup N] [inst_4 : AddCommGroup N'] [inst_5 : Module R N]
    [inst_6 : Module R N'] (a : N ≃ₗ[R] N'), motive' N → motive' N'
unit : motive PUnit.{u + 1}
prod :
  ∀ {N : Type u} {N' : Type (max u v)} [inst : AddCommGroup N] [inst_4 : AddCommGroup N'] [inst_5 : Module R N]
    [inst_6 : Module R N'], motive N → motive' N' → motive' (N × N')
M : ι → Type u
inst_2 : (i : ι) → AddCommGroup (M i)
inst_3 : (i : ι) → Module.{u_1, u} R (M i)
h : ∀ (i : ι), motive (M i)
val : Fintype ι
⊢ motive' ((i : ι) → M i)
have intro : ∀ (M : ι → Type u) [inst : (i : ι) → AddCommGroup (M i)] [inst_4 : (i : ι) → Module.{u_1, u} R (M i)]
  (h : ∀ (i : ι), motive (M i)), motive' ((i : ι) → M i)
Tactic: revert M
Cleared hypotheses: M, inst_2, inst_3, h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Pi (goal)
Goal:
ι : Type v
inst : Finite ι
R : Type u_1
inst_1 : Ring R
motive : (N : Type u) → [inst : AddCommGroup N] → [Module R N] → Prop
motive' : (N : Type (max u v)) → [inst : AddCommGroup N] → [Module R N] → Prop
equiv :
  ∀ {N : Type u} {N' : Type (max u v)} [inst : AddCommGroup N] [inst_2 : AddCommGroup N'] [inst_3 : Module R N]
    [inst_4 : Module R N'] (a : N ≃ₗ[R] N'), motive N → motive' N'
equiv' :
  ∀ {N N' : Type (max u v)} [inst : AddCommGroup N] [inst_2 : AddCommGroup N'] [inst_3 : Module R N]
    [inst_4 : Module R N'] (a : N ≃ₗ[R] N'), motive' N → motive' N'
unit : motive PUnit.{u + 1}
prod :
  ∀ {N : Type u} {N' : Type (max u v)} [inst : AddCommGroup N] [inst_2 : AddCommGroup N'] [inst_3 : Module R N]
    [inst_4 : Module R N'], motive N → motive' N' → motive' (N × N')
val : Fintype ι
⊢ ∀ (M : ι → Type u) [inst : (i : ι) → AddCommGroup (M i)] [inst_2 : (i : ι) → Module.{u_1, u} R (M i)]
    (h : ∀ (i : ι), motive (M i)), motive' ((i : ι) → M i)
have intro : ∀ (α : Type v) (x : Fintype α)
  (h :
    ∀ (M : α → Type u) [inst : (i : α) → AddCommGroup (M i)] [inst_2 : (i : α) → Module.{u_1, u} R (M i)]
      (h : ∀ (i : α), motive (M i)), motive' ((i : α) → M i))
  (M : Option α → Type u) (x : (i : Option α) → AddCommGroup (M i)) (x_1 : (i : Option α) → Module.{u_1, u} R (M i))
  (hn : ∀ (i : Option α), motive (M i)), motive' ((i : Option α) → M i)
Tactic: refine Fintype.induction_empty_option
    (fun α β _ e h M _ _ hM ↦ equiv' (LinearEquiv.piCongrLeft R M e) <| h _ fun i ↦ hM _)
    (fun M _ _ _ ↦ equiv default unit) (fun α _ h M _ _ hn ↦ ?_) ι
-- Lean 4 proof step from Mathlib.LinearAlgebra.Pi (goal)
Goal:
ι : Type v
inst : Finite ι
R : Type u_1
inst_1 : Ring R
motive : (N : Type u) → [inst : AddCommGroup N] → [Module R N] → Prop
motive' : (N : Type (max u v)) → [inst : AddCommGroup N] → [Module R N] → Prop
equiv :
  ∀ {N : Type u} {N' : Type (max u v)} [inst : AddCommGroup N] [inst_4 : AddCommGroup N'] [inst_5 : Module R N]
    [inst_6 : Module R N'] (a : N ≃ₗ[R] N'), motive N → motive' N'
equiv' :
  ∀ {N N' : Type (max u v)} [inst : AddCommGroup N] [inst_4 : AddCommGroup N'] [inst_5 : Module R N]
    [inst_6 : Module R N'] (a : N ≃ₗ[R] N'), motive' N → motive' N'
unit : motive PUnit.{u + 1}
prod :
  ∀ {N : Type u} {N' : Type (max u v)} [inst : AddCommGroup N] [inst_4 : AddCommGroup N'] [inst_5 : Module R N]
    [inst_6 : Module R N'], motive N → motive' N' → motive' (N × N')
M : ι → Type u
inst_2 : (i : ι) → AddCommGroup (M i)
inst_3 : (i : ι) → Module.{u_1, u} R (M i)
h : ∀ (i : ι), motive (M i)
⊢ motive' ((i : ι) → M i)
have intro : ∀ (val : Fintype ι), motive' ((i : ι) → M i)
Tactic: classical
  cases nonempty_fintype ι
  revert M
  refine Fintype.induction_empty_option
    (fun α β _ e h M _ _ hM ↦ equiv' (LinearEquiv.piCongrLeft R M e) <| h _ fun i ↦ hM _)
    (fun M _ _ _ ↦ equiv default unit) (fun α _ h M _ _ hn ↦ ?_) ι
  exact equiv' (LinearEquiv.piOptionEquivProd R).symm <| prod (hn _) (h _ fun i ↦ hn i)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Pi (goal)
Goal:
ι : Type v
inst : Finite ι
R : Type u_1
inst_1 : Ring R
motive : (N : Type u) → [inst : AddCommGroup N] → [Module R N] → Prop
motive' : (N : Type (max u v)) → [inst : AddCommGroup N] → [Module R N] → Prop
equiv :
  ∀ {N : Type u} {N' : Type (max u v)} [inst : AddCommGroup N] [inst_4 : AddCommGroup N'] [inst_5 : Module R N]
    [inst_6 : Module R N'] (a : N ≃ₗ[R] N'), motive N → motive' N'
equiv' :
  ∀ {N N' : Type (max u v)} [inst : AddCommGroup N] [inst_4 : AddCommGroup N'] [inst_5 : Module R N]
    [inst_6 : Module R N'] (a : N ≃ₗ[R] N'), motive' N → motive' N'
unit : motive PUnit.{u + 1}
prod :
  ∀ {N : Type u} {N' : Type (max u v)} [inst : AddCommGroup N] [inst_4 : AddCommGroup N'] [inst_5 : Module R N]
    [inst_6 : Module R N'], motive N → motive' N' → motive' (N × N')
M : ι → Type u
inst_2 : (i : ι) → AddCommGroup (M i)
inst_3 : (i : ι) → Module.{u_1, u} R (M i)
h : ∀ (i : ι), motive (M i)
intro : ∀ (val : Fintype ι), motive' ((i : ι) → M i)
⊢ motive' ((i : ι) → M i)
have intro₁ : ∀ (val : Fintype ι) (M : ι → Type u) [inst : (i : ι) → AddCommGroup (M i)] [inst_4 : (i : ι) → Module.{u_1, u} R (M i)]
  (h : ∀ (i : ι), motive (M i)), motive' ((i : ι) → M i)
Tactic: classical
  cases nonempty_fintype ι
  revert M
  refine Fintype.induction_empty_option
    (fun α β _ e h M _ _ hM ↦ equiv' (LinearEquiv.piCongrLeft R M e) <| h _ fun i ↦ hM _)
    (fun M _ _ _ ↦ equiv default unit) (fun α _ h M _ _ hn ↦ ?_) ι
  exact equiv' (LinearEquiv.piOptionEquivProd R).symm <| prod (hn _) (h _ fun i ↦ hn i)
Cleared hypotheses: M, inst_2, inst_3, h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Pi (goal)
Goal:
ι : Type v
inst : Finite ι
R : Type u_1
inst_1 : Ring R
motive : (N : Type u) → [inst : AddCommGroup N] → [Module R N] → Prop
motive' : (N : Type (max u v)) → [inst : AddCommGroup N] → [Module R N] → Prop
equiv :
  ∀ {N : Type u} {N' : Type (max u v)} [inst : AddCommGroup N] [inst_4 : AddCommGroup N'] [inst_5 : Module R N]
    [inst_6 : Module R N'] (a : N ≃ₗ[R] N'), motive N → motive' N'
equiv' :
  ∀ {N N' : Type (max u v)} [inst : AddCommGroup N] [inst_4 : AddCommGroup N'] [inst_5 : Module R N]
    [inst_6 : Module R N'] (a : N ≃ₗ[R] N'), motive' N → motive' N'
unit : motive PUnit.{u + 1}
prod :
  ∀ {N : Type u} {N' : Type (max u v)} [inst : AddCommGroup N] [inst_4 : AddCommGroup N'] [inst_5 : Module R N]
    [inst_6 : Module R N'], motive N → motive' N' → motive' (N × N')
M : ι → Type u
inst_2 : (i : ι) → AddCommGroup (M i)
inst_3 : (i : ι) → Module.{u_1, u} R (M i)
h : ∀ (i : ι), motive (M i)
intro : ∀ (val : Fintype ι), motive' ((i : ι) → M i)
intro₁ :
  ∀ (val : Fintype ι) (M : ι → Type u) [inst : (i : ι) → AddCommGroup (M i)]
    [inst_4 : (i : ι) → Module.{u_1, u} R (M i)] (h : ∀ (i : ι), motive (M i)), motive' ((i : ι) → M i)
⊢ motive' ((i : ι) → M i)
have intro₂ : ∀ (val : Fintype ι) (α : Type v) (x : Fintype α)
  (h :
    ∀ (M : α → Type u) [inst : (i : α) → AddCommGroup (M i)] [inst_4 : (i : α) → Module.{u_1, u} R (M i)]
      (h : ∀ (i : α), motive (M i)), motive' ((i : α) → M i))
  (M : Option α → Type u) (x : (i : Option α) → AddCommGroup (M i)) (x_1 : (i : Option α) → Module.{u_1, u} R (M i))
  (hn : ∀ (i : Option α), motive (M i)), motive' ((i : Option α) → M i)
Tactic: classical
  cases nonempty_fintype ι
  revert M
  refine Fintype.induction_empty_option
    (fun α β _ e h M _ _ hM ↦ equiv' (LinearEquiv.piCongrLeft R M e) <| h _ fun i ↦ hM _)
    (fun M _ _ _ ↦ equiv default unit) (fun α _ h M _ _ hn ↦ ?_) ι
  exact equiv' (LinearEquiv.piOptionEquivProd R).symm <| prod (hn _) (h _ fun i ↦ hn i)
Cleared hypotheses: M, inst_2, inst_3, h
-- Lean 4 proof step from Mathlib.LinearAlgebra.PiTensorProduct.Basis (goal)
Goal:
ι : Type u_1
R : Type u_2
M : ι → Type u_3
κ : ι → Type u_4
inst : CommSemiring R
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u_2, u_3} R (M i)
inst_3 : Fintype ι
b : (i : ι) → Basis.{u_4, u_2, u_3} (κ i) R (M i)
x : (i : ι) → M i
p : (i : ι) → κ i
⊢ Eq.{u_2 + 1} (α := R)
    (((((piTensorProduct (M := M) (κ := κ) b).repr : (a : ⨂[R] (i : ι), M i) → ((i : ι) → κ i) →₀ R)
              ((tprod R (s := M) : (a : (i : ι) → M i) → ⨂[R] (i : ι), M i) x) :
            ((i : ι) → κ i) →₀ R) :
          (a : (i : ι) → κ i) → R)
        p :
      R)
    (∏ i : ι, ((((b i).repr : (a : M i) → κ i →₀ R) (x i) : Finsupp.{u_4, u_2} (κ i) R) : (a : κ i) → R) (p i) : R)
have rw : Eq.{u_2 + 1} (α := R)
  ((((Basis.repr
                (Basis.map Finsupp.basisSingleOne
                  (LinearEquiv.symm
                    (LinearEquiv.trans (re₁₂ := sorry) (re₂₁ := sorry)
                      (LinearEquiv.trans
                        (PiTensorProduct.congr (s := M) (t := fun (i : ι) ↦ Finsupp.{u_4, u_2} (κ i) R) fun (i : ι) ↦
                          (b i).repr)
                        (ofFinsuppEquiv (κ := κ) (M := fun (i : ι) ↦ R)))
                      (Finsupp.lcongr (Equiv.refl ((i : ι) → κ i))
                        (↑(constantBaseRingEquiv ι R) : (⨂[R] (x : ι), R) ≃ₗ[R] R))))) :
              (a : ⨂[R] (i : ι), M i) → ((i : ι) → κ i) →₀ R)
            ((tprod R (s := M) : (a : (i : ι) → M i) → ⨂[R] (i : ι), M i) x) :
          ((i : ι) → κ i) →₀ R) :
        (a : (i : ι) → κ i) → R)
      p :
    R)
  (∏ i : ι, ((((b i).repr : (a : M i) → κ i →₀ R) (x i) : Finsupp.{u_4, u_2} (κ i) R) : (a : κ i) → R) (p i) : R)
Tactic: rw [piTensorProduct, Subsingleton.elim (Fintype.ofFinite ι) ‹_›]
-- Lean 4 proof step from Mathlib.LinearAlgebra.PiTensorProduct.Basis (goal)
Goal:
ι : Type u_1
R : Type u_2
M : ι → Type u_3
κ : ι → Type u_4
inst : CommSemiring R
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u_2, u_3} R (M i)
inst_3 : Finite ι
b : (i : ι) → Basis.{u_4, u_2, u_3} (κ i) R (M i)
p : (i : ι) → κ i
⊢ Eq (α := ⨂[R] (i : ι), M i)
    ((piTensorProduct (M := M) (κ := κ) b : (a : (i : ι) → κ i) → ⨂[R] (i : ι), M i) p : ⨂[R] (i : ι), M i)
    (⨂ₜ[R] (i : ι), (b i : (a : κ i) → M i) (p i) : ⨂[R] (i : ι), M i)
have haveI : ∀ (this : Fintype ι),
  Eq (α := ⨂[R] (i : ι), M i)
    ((piTensorProduct (M := M) (κ := κ) b : (a : (i : ι) → κ i) → ⨂[R] (i : ι), M i) p : ⨂[R] (i : ι), M i)
    (⨂ₜ[R] (i : ι), (b i : (a : κ i) → M i) (p i) : ⨂[R] (i : ι), M i)
Tactic: haveI := Fintype.ofFinite ι
-- Lean 4 proof step from Mathlib.LinearAlgebra.PiTensorProduct.Basis (goal)
Goal:
ι : Type u_1
R : Type u_2
M : ι → Type u_3
κ : ι → Type u_4
inst : CommSemiring R
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u_2, u_3} R (M i)
inst_3 : Finite ι
b : (i : ι) → Basis.{u_4, u_2, u_3} (κ i) R (M i)
p : (i : ι) → κ i
this : Fintype ι
⊢ Eq (α := ⨂[R] (i : ι), M i)
    ((piTensorProduct (M := M) (κ := κ) b : (a : (i : ι) → κ i) → ⨂[R] (i : ι), M i) p : ⨂[R] (i : ι), M i)
    (⨂ₜ[R] (i : ι), (b i : (a : κ i) → M i) (p i) : ⨂[R] (i : ι), M i)
have refine : ∀ (q : (i : ι) → κ i),
  Eq.{u_2 + 1} (α := R)
    (((((piTensorProduct (M := M) (κ := κ) b).repr : (a : ⨂[R] (i : ι), M i) → ((i : ι) → κ i) →₀ R)
              ((piTensorProduct (M := M) (κ := κ) b : (a : (i : ι) → κ i) → ⨂[R] (i : ι), M i) p) :
            ((i : ι) → κ i) →₀ R) :
          (a : (i : ι) → κ i) → R)
        q :
      R)
    ((((piTensorProduct (M := M) (κ := κ) b).repr : (a : ⨂[R] (i : ι), M i) → ((i : ι) → κ i) →₀ R)
            (⨂ₜ[R] (i : ι), (b i : (a : κ i) → M i) (p i)) :
          (a : (i : ι) → κ i) → R)
        q :
      R)
Tactic: refine (Basis.piTensorProduct b).ext_elem (fun q ↦ ?_)
-- Lean 4 proof step from Mathlib.LinearAlgebra.PiTensorProduct.DirectSum (goal)
Goal:
R : Type u_1
ι : Type u_2
κ : ι → Type u_3
M : (i : ι) → κ i → Type u_4
inst : CommSemiring R
inst_1 : (i : ι) → (j : κ i) → AddCommMonoid (M i j)
inst_2 : (i : ι) → (j : κ i) → Module.{u_1, u_4} R (M i j)
inst_3 : Fintype ι
inst_4 : (i : ι) → DecidableEq (κ i)
p : (i : ι) → κ i
x : (i : ι) → M i (p i)
⊢ Eq (α := ⨁ (p : (i : ι) → κ i), ⨂[R] (i : ι), M i (p i))
    ((ofDirectSumEquiv (κ := κ) (M := M) :
          (a : ⨂[R] (i : ι), ⨁ (j : κ i), M i j) → ⨁ (p : (i : ι) → κ i), ⨂[R] (i : ι), M i (p i))
        ((tprod R (s := fun (i : ι) ↦ ⨁ (j : κ i), M i j) :
            (a : (i : ι) → ⨁ (j : κ i), M i j) → ⨂[R] (i : ι), ⨁ (j : κ i), M i j)
          fun (i : ι) ↦ (lof R (κ i) (M i) (p i) : (a : M i (p i)) → ⨁ (i_1 : κ i), M i i_1) (x i)) :
      ⨁ (p : (i : ι) → κ i), ⨂[R] (i : ι), M i (p i))
    (((lof R ((i : ι) → κ i) (fun (i : (i : ι) → κ i) ↦ ⨂[R] (i_1 : ι), M i_1 (i i_1)) p :
            (⨂[R] (i : ι), M i (p i)) →ₗ[R] ⨁ (i : (i : ι) → κ i), ⨂[R] (i_1 : ι), M i_1 (i i_1)) :
          (a : ⨂[R] (i : ι), M i (p i)) → ⨁ (i : (i : ι) → κ i), ⨂[R] (i_1 : ι), M i_1 (i i_1))
        ((tprod R (s := fun (i : ι) ↦ M i (p i)) : (a : (i : ι) → M i (p i)) → ⨂[R] (i : ι), M i (p i)) fun (i : ι) ↦
          x i) :
      ⨁ (i : (i : ι) → κ i), ⨂[R] (i_1 : ι), M i_1 (i i_1))
have rw : Eq (α := ⨁ (p : (i : ι) → κ i), ⨂[R] (i : ι), M i (p i))
  ((ofDFinsuppEquiv (κ := κ) (M := fun (i : ι) (j : κ i) ↦ M i j) :
        (a : ⨂[R] (i : ι), ⨁ (j : κ i), M i j) → ⨁ (p : (i : ι) → κ i), ⨂[R] (i : ι), M i (p i))
      ((tprod R (s := fun (i : ι) ↦ ⨁ (j : κ i), M i j) :
          (a : (i : ι) → ⨁ (j : κ i), M i j) → ⨂[R] (i : ι), ⨁ (j : κ i), M i j)
        fun (i : ι) ↦ (lof R (κ i) (M i) (p i) : (a : M i (p i)) → ⨁ (i_1 : κ i), M i i_1) (x i)) :
    ⨁ (p : (i : ι) → κ i), ⨂[R] (i : ι), M i (p i))
  (((lof R ((i : ι) → κ i) (fun (i : (i : ι) → κ i) ↦ ⨂[R] (i_1 : ι), M i_1 (i i_1)) p :
          (⨂[R] (i : ι), M i (p i)) →ₗ[R] ⨁ (i : (i : ι) → κ i), ⨂[R] (i_1 : ι), M i_1 (i i_1)) :
        (a : ⨂[R] (i : ι), M i (p i)) → ⨁ (i : (i : ι) → κ i), ⨂[R] (i_1 : ι), M i_1 (i i_1))
      ((tprod R (s := fun (i : ι) ↦ M i (p i)) : (a : (i : ι) → M i (p i)) → ⨂[R] (i : ι), M i (p i)) fun (i : ι) ↦
        x i) :
    ⨁ (i : (i : ι) → κ i), ⨂[R] (i_1 : ι), M i_1 (i i_1))
Tactic: classical
  rw [ofDirectSumEquiv]
  convert! ofDFinsuppEquiv_tprod_single p x
-- Lean 4 proof step from Mathlib.LinearAlgebra.PiTensorProduct.DirectSum (goal)
Goal:
R : Type u_1
ι : Type u_2
κ : ι → Type u_3
M : (i : ι) → κ i → Type u_4
inst : CommSemiring R
inst_1 : (i : ι) → (j : κ i) → AddCommMonoid (M i j)
inst_2 : (i : ι) → (j : κ i) → Module.{u_1, u_4} R (M i j)
inst_3 : Fintype ι
inst_4 : (i : ι) → DecidableEq (κ i)
p : (i : ι) → κ i
x : (i : ι) → M i (p i)
⊢ Eq (α := ⨂[R] (i : ι), ⨁ (j : κ i), M i j)
    ((LinearEquiv.symm (ofDirectSumEquiv (κ := κ) (M := M)) :
          (a : ⨁ (p : (i : ι) → κ i), ⨂[R] (i : ι), M i (p i)) → ⨂[R] (i : ι), ⨁ (j : κ i), M i j)
        (((lof R ((i : ι) → κ i) (fun (p : (i : ι) → κ i) ↦ ⨂[R] (i : ι), M i (p i)) p :
              (⨂[R] (i : ι), M i (p i)) →ₗ[R] ⨁ (i : (i : ι) → κ i), ⨂[R] (i_1 : ι), M i_1 (i i_1)) :
            (a : ⨂[R] (i : ι), M i (p i)) → ⨁ (i : (i : ι) → κ i), ⨂[R] (i_1 : ι), M i_1 (i i_1))
          ((tprod R (s := fun (i : ι) ↦ M i (p i)) : (a : (i : ι) → M i (p i)) → ⨂[R] (i : ι), M i (p i)) x)) :
      ⨂[R] (i : ι), ⨁ (j : κ i), M i j)
    ((tprod R (s := fun (i : ι) ↦ ⨁ (i_1 : κ i), M i i_1) :
          (a : (i : ι) → ⨁ (i_1 : κ i), M i i_1) → ⨂[R] (i : ι), ⨁ (i_1 : κ i), M i i_1)
        fun (i : ι) ↦ (lof R (κ i) (M i) (p i) : (a : M i (p i)) → ⨁ (i_1 : κ i), M i i_1) (x i) :
      ⨂[R] (i : ι), ⨁ (i_1 : κ i), M i i_1)
have rw : Eq (α := ⨂[R] (i : ι), ⨁ (j : κ i), M i j)
  ((LinearEquiv.symm (ofDFinsuppEquiv (κ := κ) (M := fun (i : ι) (j : κ i) ↦ M i j)) :
        (a : ⨁ (p : (i : ι) → κ i), ⨂[R] (i : ι), M i (p i)) → ⨂[R] (i : ι), ⨁ (j : κ i), M i j)
      (((lof R ((i : ι) → κ i) (fun (p : (i : ι) → κ i) ↦ ⨂[R] (i : ι), M i (p i)) p :
            (⨂[R] (i : ι), M i (p i)) →ₗ[R] ⨁ (i : (i : ι) → κ i), ⨂[R] (i_1 : ι), M i_1 (i i_1)) :
          (a : ⨂[R] (i : ι), M i (p i)) → ⨁ (i : (i : ι) → κ i), ⨂[R] (i_1 : ι), M i_1 (i i_1))
        ((tprod R (s := fun (i : ι) ↦ M i (p i)) : (a : (i : ι) → M i (p i)) → ⨂[R] (i : ι), M i (p i)) x)) :
    ⨂[R] (i : ι), ⨁ (j : κ i), M i j)
  ((tprod R (s := fun (i : ι) ↦ ⨁ (i_1 : κ i), M i i_1) :
        (a : (i : ι) → ⨁ (i_1 : κ i), M i i_1) → ⨂[R] (i : ι), ⨁ (i_1 : κ i), M i i_1)
      fun (i : ι) ↦ (lof R (κ i) (M i) (p i) : (a : M i (p i)) → ⨁ (i_1 : κ i), M i i_1) (x i) :
    ⨂[R] (i : ι), ⨁ (i_1 : κ i), M i i_1)
Tactic: classical
  rw [ofDirectSumEquiv]
  convert! ofDFinsuppEquiv_symm_single_tprod p x
-- Lean 4 proof step from Mathlib.LinearAlgebra.PiTensorProduct.DirectSum (goal)
Goal:
R : Type u_1
ι : Type u_2
κ : ι → Type u_3
M : (i : ι) → κ i → Type u_4
inst : CommSemiring R
inst_1 : (i : ι) → (j : κ i) → AddCommMonoid (M i j)
inst_2 : (i : ι) → (j : κ i) → Module.{u_1, u_4} R (M i j)
inst_3 : Finite ι
x : (i : ι) → ⨁ (j : κ i), M i j
p : (i : ι) → κ i
⊢ (((ofDirectSumEquiv (κ := κ) (M := M) :
              (a : ⨂[R] (i : ι), ⨁ (j : κ i), M i j) → ⨁ (p : (i : ι) → κ i), ⨂[R] (i : ι), M i (p i))
            ((tprod R (s := fun (i : ι) ↦ ⨁ (j : κ i), M i j) :
                (a : (i : ι) → ⨁ (j : κ i), M i j) → ⨂[R] (i : ι), ⨁ (j : κ i), M i j)
              x) :
          ⨁ (p : (i : ι) → κ i), ⨂[R] (i : ι), M i (p i)) :
        (a : (i : ι) → κ i) → ⨂[R] (i : ι), M i (a i))
      p =
    (tprod R (s := fun (i : ι) ↦ M i (p i)) : (a : (i : ι) → M i (p i)) → ⨂[R] (i : ι), M i (p i)) fun (i : ι) ↦
      (x i : (a : κ i) → M i a) (p i)
have have : ∀ (this : Fintype ι),
  (((ofDirectSumEquiv (κ := κ) (M := M) :
              (a : ⨂[R] (i : ι), ⨁ (j : κ i), M i j) → ⨁ (p : (i : ι) → κ i), ⨂[R] (i : ι), M i (p i))
            ((tprod R (s := fun (i : ι) ↦ ⨁ (j : κ i), M i j) :
                (a : (i : ι) → ⨁ (j : κ i), M i j) → ⨂[R] (i : ι), ⨁ (j : κ i), M i j)
              x) :
          ⨁ (p : (i : ι) → κ i), ⨂[R] (i : ι), M i (p i)) :
        (a : (i : ι) → κ i) → ⨂[R] (i : ι), M i (a i))
      p =
    (tprod R (s := fun (i : ι) ↦ M i (p i)) : (a : (i : ι) → M i (p i)) → ⨂[R] (i : ι), M i (p i)) fun (i : ι) ↦
      (x i : (a : κ i) → M i a) (p i)
Tactic: have : Fintype ι := Fintype.ofFinite ι
-- Lean 4 proof step from Mathlib.LinearAlgebra.PiTensorProduct.Dual (goal)
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)
    (((dualDistrib (M := M) : (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)
have rw : 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: rw [dualDistrib, Subsingleton.elim (Fintype.ofFinite ι) ‹_›]