awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Multilinear.FiniteDimensional
Goal:
ι : Type u_1
R : Type u_2
M₂ : Type u_3
M₁ : ι → Type u_4
inst : Finite ι
inst_1 : CommRing R
inst_2 : AddCommGroup M₂
inst_3 : Module R M₂
inst_4 : Module.Finite R M₂
inst_5 : Module.Free R M₂
inst_6 : (i : ι) → AddCommGroup (M₁ i)
inst_7 : (i : ι) → Module.{u_2, u_4} R (M₁ i)
inst_8 : ∀ (i : ι), Module.Finite.{u_2, u_4} R (M₁ i)
inst_9 : ∀ (i : ι), Module.Free.{u_2, u_4} R (M₁ i)
val : Fintype ι
this :
  ∀
    [inst :
      (i : Fin (Fintype.card ι)) →
        AddCommGroup (M₁ ((Equiv.symm (Fintype.equivFin ι) : (a : Fin (Fintype.card ι)) → ι) i))]
    [inst_10 :
      (i : Fin (Fintype.card ι)) →
        Module.{u_2, u_4} R (M₁ ((Equiv.symm (Fintype.equivFin ι) : (a : Fin (Fintype.card ι)) → ι) i))]
    [∀ (i : Fin (Fintype.card ι)),
        Module.Finite.{u_2, u_4} R (M₁ ((Equiv.symm (Fintype.equivFin ι) : (a : Fin (Fintype.card ι)) → ι) i))]
    [∀ (i : Fin (Fintype.card ι)),
        Module.Free.{u_2, u_4} R (M₁ ((Equiv.symm (Fintype.equivFin ι) : (a : Fin (Fintype.card ι)) → ι) i))],
    Module.Free R
        (MultilinearMap.{u_2, 0, u_4, u_3} R
          (fun (x : Fin (Fintype.card ι)) ↦ M₁ ((Equiv.symm (Fintype.equivFin ι) : (a : Fin (Fintype.card ι)) → ι) x))
          M₂) ∧
      Module.Finite R
        (MultilinearMap.{u_2, 0, u_4, u_3} R
          (fun (x : Fin (Fintype.card ι)) ↦ M₁ ((Equiv.symm (Fintype.equivFin ι) : (a : Fin (Fintype.card ι)) → ι) x))
          M₂)
⊢ Module.Free R
    (MultilinearMap.{u_2, 0, u_4, u_3} R
      (fun (x : Fin (Fintype.card ι)) ↦ M₁ ((Equiv.symm (Fintype.equivFin ι) : (a : Fin (Fintype.card ι)) → ι) x)) M₂)

Tactic:
obtain ⟨l, r⟩ := this
-- Module: Mathlib.LinearAlgebra.Multilinear.FiniteDimensional
Goal:
ι : Type u_1
R : Type u_2
M₂ : Type u_3
M₁ : ι → Type u_4
inst : Finite ι
inst_1 : CommRing R
inst_2 : AddCommGroup M₂
inst_3 : Module R M₂
inst_4 : Module.Finite R M₂
inst_5 : Module.Free R M₂
inst_6 : (i : ι) → AddCommGroup (M₁ i)
inst_7 : (i : ι) → Module.{u_2, u_4} R (M₁ i)
inst_8 : ∀ (i : ι), Module.Finite.{u_2, u_4} R (M₁ i)
inst_9 : ∀ (i : ι), Module.Free.{u_2, u_4} R (M₁ i)
val : Fintype ι
this :
  ∀
    [inst :
      (i : Fin (Fintype.card ι)) →
        AddCommGroup (M₁ ((Equiv.symm (Fintype.equivFin ι) : (a : Fin (Fintype.card ι)) → ι) i))]
    [inst_10 :
      (i : Fin (Fintype.card ι)) →
        Module.{u_2, u_4} R (M₁ ((Equiv.symm (Fintype.equivFin ι) : (a : Fin (Fintype.card ι)) → ι) i))]
    [∀ (i : Fin (Fintype.card ι)),
        Module.Finite.{u_2, u_4} R (M₁ ((Equiv.symm (Fintype.equivFin ι) : (a : Fin (Fintype.card ι)) → ι) i))]
    [∀ (i : Fin (Fintype.card ι)),
        Module.Free.{u_2, u_4} R (M₁ ((Equiv.symm (Fintype.equivFin ι) : (a : Fin (Fintype.card ι)) → ι) i))],
    Module.Free R
        (MultilinearMap.{u_2, 0, u_4, u_3} R
          (fun (x : Fin (Fintype.card ι)) ↦ M₁ ((Equiv.symm (Fintype.equivFin ι) : (a : Fin (Fintype.card ι)) → ι) x))
          M₂) ∧
      Module.Finite R
        (MultilinearMap.{u_2, 0, u_4, u_3} R
          (fun (x : Fin (Fintype.card ι)) ↦ M₁ ((Equiv.symm (Fintype.equivFin ι) : (a : Fin (Fintype.card ι)) → ι) x))
          M₂)
l :
  Module.Free R
    (MultilinearMap.{u_2, 0, u_4, u_3} R
      (fun (x : Fin (Fintype.card ι)) ↦ M₁ ((Equiv.symm (Fintype.equivFin ι) : (a : Fin (Fintype.card ι)) → ι) x)) M₂)
⊢ Module.Finite R
    (MultilinearMap.{u_2, 0, u_4, u_3} R
      (fun (x : Fin (Fintype.card ι)) ↦ M₁ ((Equiv.symm (Fintype.equivFin ι) : (a : Fin (Fintype.card ι)) → ι) x)) M₂)

Tactic:
obtain ⟨l, r⟩ := this
-- Module: Mathlib.LinearAlgebra.Multilinear.FiniteDimensional
Goal:
ι : Type u_1
R : Type u_2
M₂ : Type u_3
M₁ : ι → Type u_4
inst : Finite ι
inst_1 : CommRing R
inst_2 : AddCommGroup M₂
inst_3 : Module R M₂
inst_4 : Module.Finite R M₂
inst_5 : Module.Free R M₂
inst_6 : (i : ι) → AddCommGroup (M₁ i)
inst_7 : (i : ι) → Module.{u_2, u_4} R (M₁ i)
inst_8 : ∀ (i : ι), Module.Finite.{u_2, u_4} R (M₁ i)
inst_9 : ∀ (i : ι), Module.Free.{u_2, u_4} R (M₁ i)
val : Fintype ι
this :
  ∀
    [inst :
      (i : Fin (Fintype.card ι)) →
        AddCommGroup (M₁ ((Equiv.symm (Fintype.equivFin ι) : (a : Fin (Fintype.card ι)) → ι) i))]
    [inst_10 :
      (i : Fin (Fintype.card ι)) →
        Module.{u_2, u_4} R (M₁ ((Equiv.symm (Fintype.equivFin ι) : (a : Fin (Fintype.card ι)) → ι) i))]
    [∀ (i : Fin (Fintype.card ι)),
        Module.Finite.{u_2, u_4} R (M₁ ((Equiv.symm (Fintype.equivFin ι) : (a : Fin (Fintype.card ι)) → ι) i))]
    [∀ (i : Fin (Fintype.card ι)),
        Module.Free.{u_2, u_4} R (M₁ ((Equiv.symm (Fintype.equivFin ι) : (a : Fin (Fintype.card ι)) → ι) i))],
    Module.Free R
        (MultilinearMap.{u_2, 0, u_4, u_3} R
          (fun (x : Fin (Fintype.card ι)) ↦ M₁ ((Equiv.symm (Fintype.equivFin ι) : (a : Fin (Fintype.card ι)) → ι) x))
          M₂) ∧
      Module.Finite R
        (MultilinearMap.{u_2, 0, u_4, u_3} R
          (fun (x : Fin (Fintype.card ι)) ↦ M₁ ((Equiv.symm (Fintype.equivFin ι) : (a : Fin (Fintype.card ι)) → ι) x))
          M₂)
l :
  Module.Free R
    (MultilinearMap.{u_2, 0, u_4, u_3} R
      (fun (x : Fin (Fintype.card ι)) ↦ M₁ ((Equiv.symm (Fintype.equivFin ι) : (a : Fin (Fintype.card ι)) → ι) x)) M₂)
r :
  Module.Finite R
    (MultilinearMap.{u_2, 0, u_4, u_3} R
      (fun (x : Fin (Fintype.card ι)) ↦ M₁ ((Equiv.symm (Fintype.equivFin ι) : (a : Fin (Fintype.card ι)) → ι) x)) M₂)
intro :
  ∀
    (e :
      MultilinearMap R M₁ M₂ ≃ₗ[R]
        MultilinearMap.{u_2, 0, u_4, u_3} R
          (fun (i : Fin (Fintype.card ι)) ↦ M₁ ((Equiv.symm (Fintype.equivFin ι) : (a : Fin (Fintype.card ι)) → ι) i))
          M₂),
    Module.Free R (MultilinearMap R M₁ M₂) ∧ Module.Finite R (MultilinearMap R M₁ M₂)
⊢ Module.Free R (MultilinearMap R M₁ M₂) ∧ Module.Finite R (MultilinearMap R M₁ M₂)

Tactic:
have e := domDomCongrLinearEquiv' R R M₁ M₂ (Fintype.equivFin ι)
-- Module: Mathlib.LinearAlgebra.Multilinear.FiniteDimensional
Goal:
ι : Type u_1
R : Type u_2
M₂ : Type u_3
M₁ : ι → Type u_4
inst : Finite ι
inst_1 : CommRing R
inst_2 : AddCommGroup M₂
inst_3 : Module R M₂
inst_4 : Module.Finite R M₂
inst_5 : Module.Free R M₂
inst_6 : (i : ι) → AddCommGroup (M₁ i)
inst_7 : (i : ι) → Module.{u_2, u_4} R (M₁ i)
inst_8 : ∀ (i : ι), Module.Finite.{u_2, u_4} R (M₁ i)
inst_9 : ∀ (i : ι), Module.Free.{u_2, u_4} R (M₁ i)
val : Fintype ι
this :
  ∀
    [inst :
      (i : Fin (Fintype.card ι)) →
        AddCommGroup (M₁ ((Equiv.symm (Fintype.equivFin ι) : (a : Fin (Fintype.card ι)) → ι) i))]
    [inst_10 :
      (i : Fin (Fintype.card ι)) →
        Module.{u_2, u_4} R (M₁ ((Equiv.symm (Fintype.equivFin ι) : (a : Fin (Fintype.card ι)) → ι) i))]
    [∀ (i : Fin (Fintype.card ι)),
        Module.Finite.{u_2, u_4} R (M₁ ((Equiv.symm (Fintype.equivFin ι) : (a : Fin (Fintype.card ι)) → ι) i))]
    [∀ (i : Fin (Fintype.card ι)),
        Module.Free.{u_2, u_4} R (M₁ ((Equiv.symm (Fintype.equivFin ι) : (a : Fin (Fintype.card ι)) → ι) i))],
    Module.Free R
        (MultilinearMap.{u_2, 0, u_4, u_3} R
          (fun (x : Fin (Fintype.card ι)) ↦ M₁ ((Equiv.symm (Fintype.equivFin ι) : (a : Fin (Fintype.card ι)) → ι) x))
          M₂) ∧
      Module.Finite R
        (MultilinearMap.{u_2, 0, u_4, u_3} R
          (fun (x : Fin (Fintype.card ι)) ↦ M₁ ((Equiv.symm (Fintype.equivFin ι) : (a : Fin (Fintype.card ι)) → ι) x))
          M₂)
l :
  Module.Free R
    (MultilinearMap.{u_2, 0, u_4, u_3} R
      (fun (x : Fin (Fintype.card ι)) ↦ M₁ ((Equiv.symm (Fintype.equivFin ι) : (a : Fin (Fintype.card ι)) → ι) x)) M₂)
r :
  Module.Finite R
    (MultilinearMap.{u_2, 0, u_4, u_3} R
      (fun (x : Fin (Fintype.card ι)) ↦ M₁ ((Equiv.symm (Fintype.equivFin ι) : (a : Fin (Fintype.card ι)) → ι) x)) M₂)
e :
  MultilinearMap R M₁ M₂ ≃ₗ[R]
    MultilinearMap.{u_2, 0, u_4, u_3} R
      (fun (i : Fin (Fintype.card ι)) ↦ M₁ ((Equiv.symm (Fintype.equivFin ι) : (a : Fin (Fintype.card ι)) → ι) i)) M₂
⊢ Module.Free R (MultilinearMap R M₁ M₂) ∧ Module.Finite R (MultilinearMap R M₁ M₂)

Tactic:
⟨Module.Free.of_equiv e.symm, Module.Finite.equiv e.symm⟩

Premises used: LinearEquiv.symm, And.intro, Module.Free.of_equiv, Module.Finite.equiv
-- Module: Mathlib.LinearAlgebra.Multilinear.FiniteDimensional
Goal:
ι : Type u_1
R : Type u_2
M₂ : Type u_3
M₁ : ι → Type u_4
inst : Finite ι
inst_1 : CommRing R
inst_2 : AddCommGroup M₂
inst_3 : Module R M₂
inst_4 : Module.Finite R M₂
inst_5 : Module.Free R M₂
inst_6 : (i : ι) → AddCommGroup (M₁ i)
inst_7 : (i : ι) → Module.{u_2, u_4} R (M₁ i)
inst_8 : ∀ (i : ι), Module.Finite.{u_2, u_4} R (M₁ i)
inst_9 : ∀ (i : ι), Module.Free.{u_2, u_4} R (M₁ i)
val : Fintype ι
this :
  ∀
    [inst :
      (i : Fin (Fintype.card ι)) →
        AddCommGroup (M₁ ((Equiv.symm (Fintype.equivFin ι) : (a : Fin (Fintype.card ι)) → ι) i))]
    [inst_10 :
      (i : Fin (Fintype.card ι)) →
        Module.{u_2, u_4} R (M₁ ((Equiv.symm (Fintype.equivFin ι) : (a : Fin (Fintype.card ι)) → ι) i))]
    [∀ (i : Fin (Fintype.card ι)),
        Module.Finite.{u_2, u_4} R (M₁ ((Equiv.symm (Fintype.equivFin ι) : (a : Fin (Fintype.card ι)) → ι) i))]
    [∀ (i : Fin (Fintype.card ι)),
        Module.Free.{u_2, u_4} R (M₁ ((Equiv.symm (Fintype.equivFin ι) : (a : Fin (Fintype.card ι)) → ι) i))],
    Module.Free R
        (MultilinearMap.{u_2, 0, u_4, u_3} R
          (fun (x : Fin (Fintype.card ι)) ↦ M₁ ((Equiv.symm (Fintype.equivFin ι) : (a : Fin (Fintype.card ι)) → ι) x))
          M₂) ∧
      Module.Finite R
        (MultilinearMap.{u_2, 0, u_4, u_3} R
          (fun (x : Fin (Fintype.card ι)) ↦ M₁ ((Equiv.symm (Fintype.equivFin ι) : (a : Fin (Fintype.card ι)) → ι) x))
          M₂)
l :
  Module.Free R
    (MultilinearMap.{u_2, 0, u_4, u_3} R
      (fun (x : Fin (Fintype.card ι)) ↦ M₁ ((Equiv.symm (Fintype.equivFin ι) : (a : Fin (Fintype.card ι)) → ι) x)) M₂)
r :
  Module.Finite R
    (MultilinearMap.{u_2, 0, u_4, u_3} R
      (fun (x : Fin (Fintype.card ι)) ↦ M₁ ((Equiv.symm (Fintype.equivFin ι) : (a : Fin (Fintype.card ι)) → ι) x)) M₂)
e :
  MultilinearMap R M₁ M₂ ≃ₗ[R]
    MultilinearMap.{u_2, 0, u_4, u_3} R
      (fun (i : Fin (Fintype.card ι)) ↦ M₁ ((Equiv.symm (Fintype.equivFin ι) : (a : Fin (Fintype.card ι)) → ι) i)) M₂
⊢ Module.Free R (MultilinearMap R M₁ M₂) ∧ Module.Finite R (MultilinearMap R M₁ M₂)

Tactic:
exact ⟨Module.Free.of_equiv e.symm, Module.Finite.equiv e.symm⟩
-- Module: Mathlib.LinearAlgebra.Multilinear.FiniteDimensional
Goal:
ι : Type u_1
R : Type u_2
M₂ : Type u_3
M₁ : ι → Type u_4
inst : Finite ι
inst_1 : CommRing R
inst_2 : AddCommGroup M₂
inst_3 : Module R M₂
inst_4 : Module.Finite R M₂
inst_5 : Module.Free R M₂
inst_6 : (i : ι) → AddCommGroup (M₁ i)
inst_7 : (i : ι) → Module.{u_2, u_4} R (M₁ i)
inst_8 : ∀ (i : ι), Module.Finite.{u_2, u_4} R (M₁ i)
inst_9 : ∀ (i : ι), Module.Free.{u_2, u_4} R (M₁ i)
⊢ Module.Finite R (MultilinearMap R M₁ M₂)

Tactic:
free_and_finite.2

Premises used: And.right, _private.0.MultilinearMap.free_and_finite
-- Module: Mathlib.LinearAlgebra.Multilinear.FiniteDimensional
Goal:
ι : Type u_1
R : Type u_2
M₂ : Type u_3
M₁ : ι → Type u_4
inst : Finite ι
inst_1 : CommRing R
inst_2 : AddCommGroup M₂
inst_3 : Module R M₂
inst_4 : Module.Finite R M₂
inst_5 : Module.Free R M₂
inst_6 : (i : ι) → AddCommGroup (M₁ i)
inst_7 : (i : ι) → Module.{u_2, u_4} R (M₁ i)
inst_8 : ∀ (i : ι), Module.Finite.{u_2, u_4} R (M₁ i)
inst_9 : ∀ (i : ι), Module.Free.{u_2, u_4} R (M₁ i)
⊢ Module.Free R (MultilinearMap R M₁ M₂)

Tactic:
free_and_finite.1

Premises used: And.left, _private.0.MultilinearMap.free_and_finite
-- Module: Mathlib.LinearAlgebra.Multilinear.Finsupp
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
κ : ι → Type u_4
inst : DecidableEq ι
inst_1 : Fintype ι
inst_2 : CommSemiring R
inst_3 : DecidableEq R
inst_4 : DecidableEq ι'
inst_5 : (i : ι) → Fintype (κ i)
inst_6 : (i : ι) → DecidableEq (κ i)
f : ((i : ι) → κ i) × ι' →₀ R
⊢ Eq (α := MultilinearMap R (fun (i : ι) ↦ Finsupp.{u_4, u_3} (κ i) R) (ι' →₀ R))
    ((freeFinsuppEquiv (κ := κ) : (a : ((i : ι) → κ i) × ι' →₀ R) → MultilinearMap R (fun (i : ι) ↦ κ i →₀ R) (ι' →₀ R))
        f :
      MultilinearMap R (fun (i : ι) ↦ Finsupp.{u_4, u_3} (κ i) R) (ι' →₀ R))
    ((LinearEquiv.multilinearMapCongrLeft (M₁ := fun (x : ι) ↦ Finsupp.{u_4, u_3} (κ x) R) (M₁' := fun (x : ι) ↦
            Π₀ (x : κ x), R) fun (x : ι) ↦ finsuppLequivDFinsupp R :
          (a : MultilinearMap R (fun (x : ι) ↦ Π₀ (x : κ x), R) (ι' →₀ R)) →
            MultilinearMap R (fun (x : ι) ↦ κ x →₀ R) (ι' →₀ R))
        ((LinearEquiv.symm
              (LinearEquiv.multilinearMapCongrRight R (M₁ := fun (x : ι) ↦ Π₀ (x : κ x), R) (finsuppLequivDFinsupp R)) :
            (a : MultilinearMap R (fun (x : ι) ↦ Π₀ (x : κ x), R) (Π₀ (x : ι'), R)) →
              MultilinearMap R (fun (x : ι) ↦ Π₀ (x : κ x), R) (ι' →₀ R))
          ((freeDFinsuppEquiv (κ := κ) :
              (a : Π₀ (x : ((i : ι) → κ i) × ι'), R) →
                MultilinearMap R (fun (i : ι) ↦ Π₀ (x : κ i), R) (Π₀ (x : ι'), R))
            ((finsuppLequivDFinsupp R : (a : ((i : ι) → κ i) × ι' →₀ R) → Π₀ (x : ((i : ι) → κ i) × ι'), R) f))) :
      MultilinearMap R (fun (x : ι) ↦ Finsupp.{u_4, u_3} (κ x) R) (ι' →₀ R))

Tactic:
rfl

Premises used: MultilinearMap.compLinearMap, rfl
-- Module: Mathlib.LinearAlgebra.Multilinear.Finsupp
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
κ : ι → Type u_4
inst : DecidableEq ι
inst_1 : Fintype ι
inst_2 : CommSemiring R
inst_3 : DecidableEq R
inst_4 : DecidableEq ι'
inst_5 : (i : ι) → Fintype (κ i)
inst_6 : (i : ι) → DecidableEq (κ i)
p : ((i : ι) → κ i) × ι'
r : R
x : (i : ι) → Finsupp.{u_4, u_3} (κ i) R
⊢ (((freeFinsuppEquiv (κ := κ) : (a : ((i : ι) → κ i) × ι' →₀ R) → MultilinearMap R (fun (i : ι) ↦ κ i →₀ R) (ι' →₀ R))
            (Finsupp.single p r) :
          MultilinearMap R (fun (i : ι) ↦ Finsupp.{u_4, u_3} (κ i) R) (ι' →₀ R)) :
        (a : (i : ι) → κ i →₀ R) → ι' →₀ R)
      x =
    HSMul.hSMul (β := ι' →₀ R) r (Finsupp.single p.2 (∏ i : ι, (x i : (a : κ i) → R) (p.1 i)))

Tactic:
simp [freeFinsuppEquiv_def]

Premises used: MultilinearMap.freeFinsuppEquiv_def
-- Module: Mathlib.LinearAlgebra.Multilinear.Finsupp
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
κ : ι → Type u_4
inst : DecidableEq ι
inst_1 : Fintype ι
inst_2 : CommSemiring R
inst_3 : DecidableEq R
inst_4 : DecidableEq ι'
inst_5 : (i : ι) → Fintype (κ i)
inst_6 : (i : ι) → DecidableEq (κ i)
inst_7 : Fintype ι'
x : (i : ι) → Finsupp.{u_4, u_3} (κ i) R
⊢ Eq (α := ι' →₀ R)
    (((freeFinsuppEquiv (κ := κ) :
              (a : ((i : ι) → κ i) × ι' →₀ R) → MultilinearMap R (fun (i : ι) ↦ κ i →₀ R) (ι' →₀ R))
            0 :
          (a : (i : ι) → κ i →₀ R) → ι' →₀ R)
        x :
      ι' →₀ R)
    (∑ p : ((i : ι) → κ i) × ι',
        HSMul.hSMul (α := R) (β := ι' →₀ R) ((0 : (a : ((i : ι) → κ i) × ι') → R) p : R)
          (Finsupp.single p.2 (∏ i : ι, (x i : (a : κ i) → R) (p.1 i))) :
      ι' →₀ R)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Multilinear.Finsupp
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
κ : ι → Type u_4
inst : DecidableEq ι
inst_1 : Fintype ι
inst_2 : CommSemiring R
inst_3 : DecidableEq R
inst_4 : DecidableEq ι'
inst_5 : (i : ι) → Fintype (κ i)
inst_6 : (i : ι) → DecidableEq (κ i)
inst_7 : Fintype ι'
x : (i : ι) → Finsupp.{u_4, u_3} (κ i) R
f g : ((i : ι) → κ i) × ι' →₀ R
hf :
  Eq (α := ι' →₀ R)
    ((((freeFinsuppEquiv (κ := κ) :
                (a : ((i : ι) → κ i) × ι' →₀ R) → MultilinearMap R (fun (i : ι) ↦ κ i →₀ R) (ι' →₀ R))
              f :
            MultilinearMap R (fun (i : ι) ↦ Finsupp.{u_4, u_3} (κ i) R) (ι' →₀ R)) :
          (a : (i : ι) → κ i →₀ R) → ι' →₀ R)
        x :
      ι' →₀ R)
    (∑ p : ((i : ι) → κ i) × ι',
        HSMul.hSMul (α := R) (β := ι' →₀ R) ((f : (a : ((i : ι) → κ i) × ι') → R) p : R)
          (Finsupp.single p.2 (∏ i : ι, (x i : (a : κ i) → R) (p.1 i))) :
      ι' →₀ R)
hg :
  Eq (α := ι' →₀ R)
    ((((freeFinsuppEquiv (κ := κ) :
                (a : ((i : ι) → κ i) × ι' →₀ R) → MultilinearMap R (fun (i : ι) ↦ κ i →₀ R) (ι' →₀ R))
              g :
            MultilinearMap R (fun (i : ι) ↦ Finsupp.{u_4, u_3} (κ i) R) (ι' →₀ R)) :
          (a : (i : ι) → κ i →₀ R) → ι' →₀ R)
        x :
      ι' →₀ R)
    (∑ p : ((i : ι) → κ i) × ι',
        HSMul.hSMul (α := R) (β := ι' →₀ R) ((g : (a : ((i : ι) → κ i) × ι') → R) p : R)
          (Finsupp.single p.2 (∏ i : ι, (x i : (a : κ i) → R) (p.1 i))) :
      ι' →₀ R)
⊢ Eq (α := ι' →₀ R)
    ((((freeFinsuppEquiv (κ := κ) :
                (a : ((i : ι) → κ i) × ι' →₀ R) → MultilinearMap R (fun (i : ι) ↦ κ i →₀ R) (ι' →₀ R))
              (f + g) :
            MultilinearMap R (fun (i : ι) ↦ Finsupp.{u_4, u_3} (κ i) R) (ι' →₀ R)) :
          (a : (i : ι) → κ i →₀ R) → ι' →₀ R)
        x :
      ι' →₀ R)
    (∑ p : ((i : ι) → κ i) × ι',
        HSMul.hSMul (α := R) (β := ι' →₀ R) ((f + g : (a : ((i : ι) → κ i) × ι') → R) p : R)
          (Finsupp.single p.2 (∏ i : ι, (x i : (a : κ i) → R) (p.1 i))) :
      ι' →₀ R)

Tactic:
simp [hf, hg, add_mul, Finset.sum_add_distrib]

Premises used: add_mul, Finset.sum_add_distrib
-- Module: Mathlib.LinearAlgebra.Multilinear.Finsupp
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
κ : ι → Type u_4
inst : DecidableEq ι
inst_1 : Fintype ι
inst_2 : CommSemiring R
inst_3 : DecidableEq R
inst_4 : DecidableEq ι'
inst_5 : (i : ι) → Fintype (κ i)
inst_6 : (i : ι) → DecidableEq (κ i)
inst_7 : Fintype ι'
x : (i : ι) → Finsupp.{u_4, u_3} (κ i) R
p : ((i : ι) → κ i) × ι'
r : R
⊢ Eq (α := ι' →₀ R)
    ((((freeFinsuppEquiv (κ := κ) :
                (a : ((i : ι) → κ i) × ι' →₀ R) → MultilinearMap R (fun (i : ι) ↦ κ i →₀ R) (ι' →₀ R))
              (Finsupp.single p r) :
            MultilinearMap R (fun (i : ι) ↦ Finsupp.{u_4, u_3} (κ i) R) (ι' →₀ R)) :
          (a : (i : ι) → κ i →₀ R) → ι' →₀ R)
        x :
      ι' →₀ R)
    (∑ p_1 : ((i : ι) → κ i) × ι',
        HSMul.hSMul (α := R) (β := ι' →₀ R) ((Finsupp.single p r : (a : ((i : ι) → κ i) × ι') → R) p_1 : R)
          (Finsupp.single p_1.2 (∏ i : ι, (x i : (a : κ i) → R) (p_1.1 i))) :
      ι' →₀ R)

Tactic:
simp [Finsupp.single_apply]

Premises used: Finsupp.single_apply
-- Module: Mathlib.LinearAlgebra.Multilinear.Pi
Goal:
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : Type uN
inst : Semiring R
inst_1 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst_2 : AddCommMonoid N
inst_3 : (i : ι) → (k : κ i) → Module.{uR, uM} R (M i k)
inst_4 : Module R N
inst_5 : Finite ι
inst_6 : ∀ (i : ι), Finite.{uκ + 1} (κ i)
inst_7 : (i : ι) → DecidableEq (κ i)
f g : MultilinearMap R (fun (i : ι) ↦ (j : κ i) → M i j) N
h :
  ∀ (p : (i : ι) → κ i),
    Eq (α := MultilinearMap.{uR, uι, uM, uN} R (fun (i : ι) ↦ M i (p i)) N)
      (f.compLinearMap (M₁ := fun (i : ι) ↦ M i (p i)) (M₁' := fun (i : ι) ↦ (j : κ i) → M i j) fun (i : ι) ↦
        LinearMap.single R (M i) (p i))
      (g.compLinearMap (M₁ := fun (i : ι) ↦ M i (p i)) (M₁' := fun (i : ι) ↦ (j : κ i) → M i j) fun (i : ι) ↦
        LinearMap.single R (M i) (p i))
H :
  ∀ (x : (i : ι) → (j : κ i) → M i j),
    Eq.{uN + 1} (α := N) ((f : (a : (i : ι) → (j : κ i) → M i j) → N) x : N)
      ((g : (a : (i : ι) → (j : κ i) → M i j) → N) x : N)
⊢ f = g

Tactic:
ext x
-- Module: Mathlib.LinearAlgebra.Multilinear.Pi
Goal:
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : Type uN
inst : Semiring R
inst_1 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst_2 : AddCommMonoid N
inst_3 : (i : ι) → (k : κ i) → Module.{uR, uM} R (M i k)
inst_4 : Module R N
inst_5 : Finite ι
inst_6 : ∀ (i : ι), Finite.{uκ + 1} (κ i)
inst_7 : (i : ι) → DecidableEq (κ i)
f g : MultilinearMap R (fun (i : ι) ↦ (j : κ i) → M i j) N
h :
  ∀ (p : (i : ι) → κ i),
    Eq (α := MultilinearMap.{uR, uι, uM, uN} R (fun (i : ι) ↦ M i (p i)) N)
      (f.compLinearMap (M₁ := fun (i : ι) ↦ M i (p i)) (M₁' := fun (i : ι) ↦ (j : κ i) → M i j) fun (i : ι) ↦
        LinearMap.single R (M i) (p i))
      (g.compLinearMap (M₁ := fun (i : ι) ↦ M i (p i)) (M₁' := fun (i : ι) ↦ (j : κ i) → M i j) fun (i : ι) ↦
        LinearMap.single R (M i) (p i))
x : (i : ι) → (j : κ i) → M i j
H :
  Eq.{uN + 1} (α := N) ((f : (a : (i : ι) → (j : κ i) → M i j) → N) fun (i : ι) ↦ x i : N)
    ((g : (a : (i : ι) → (j : κ i) → M i j) → N) fun (i : ι) ↦ x i : N)
⊢ Eq.{uN + 1} (α := N) ((f : (a : (i : ι) → (j : κ i) → M i j) → N) x : N)
    ((g : (a : (i : ι) → (j : κ i) → M i j) → N) x : N)

Tactic:
change f (fun i ↦ x i) = g (fun i ↦ x i)

Premises used: DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Multilinear.Pi
Goal:
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : Type uN
inst : Semiring R
inst_1 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst_2 : AddCommMonoid N
inst_3 : (i : ι) → (k : κ i) → Module.{uR, uM} R (M i k)
inst_4 : Module R N
inst_5 : Finite ι
inst_6 : ∀ (i : ι), Finite.{uκ + 1} (κ i)
inst_7 : (i : ι) → DecidableEq (κ i)
f g : MultilinearMap R (fun (i : ι) ↦ (j : κ i) → M i j) N
h :
  ∀ (p : (i : ι) → κ i),
    Eq (α := MultilinearMap.{uR, uι, uM, uN} R (fun (i : ι) ↦ M i (p i)) N)
      (f.compLinearMap (M₁ := fun (i : ι) ↦ M i (p i)) (M₁' := fun (i : ι) ↦ (j : κ i) → M i j) fun (i : ι) ↦
        LinearMap.single R (M i) (p i))
      (g.compLinearMap (M₁ := fun (i : ι) ↦ M i (p i)) (M₁' := fun (i : ι) ↦ (j : κ i) → M i j) fun (i : ι) ↦
        LinearMap.single R (M i) (p i))
x : (i : ι) → (j : κ i) → M i j
H :
  ∀ (i : Fintype ι),
    Eq.{uN + 1} (α := N) ((f : (a : (i : ι) → (j : κ i) → M i j) → N) fun (i : ι) ↦ x i : N)
      ((g : (a : (i : ι) → (j : κ i) → M i j) → N) fun (i : ι) ↦ x i : N)
⊢ Eq.{uN + 1} (α := N) ((f : (a : (i : ι) → (j : κ i) → M i j) → N) fun (i : ι) ↦ x i : N)
    ((g : (a : (i : ι) → (j : κ i) → M i j) → N) fun (i : ι) ↦ x i : N)

Tactic:
obtain ⟨i⟩ := nonempty_fintype ι

Premises used: nonempty_fintype
-- Module: Mathlib.LinearAlgebra.Multilinear.Pi
Goal:
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : Type uN
inst : Semiring R
inst_1 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst_2 : AddCommMonoid N
inst_3 : (i : ι) → (k : κ i) → Module.{uR, uM} R (M i k)
inst_4 : Module R N
inst_5 : Finite ι
inst_6 : ∀ (i : ι), Finite.{uκ + 1} (κ i)
inst_7 : (i : ι) → DecidableEq (κ i)
f g : MultilinearMap R (fun (i : ι) ↦ (j : κ i) → M i j) N
h :
  ∀ (p : (i : ι) → κ i),
    Eq (α := MultilinearMap.{uR, uι, uM, uN} R (fun (i : ι) ↦ M i (p i)) N)
      (f.compLinearMap (M₁ := fun (i : ι) ↦ M i (p i)) (M₁' := fun (i : ι) ↦ (j : κ i) → M i j) fun (i : ι) ↦
        LinearMap.single R (M i) (p i))
      (g.compLinearMap (M₁ := fun (i : ι) ↦ M i (p i)) (M₁' := fun (i : ι) ↦ (j : κ i) → M i j) fun (i : ι) ↦
        LinearMap.single R (M i) (p i))
x : (i : ι) → (j : κ i) → M i j
i : Fintype ι
H :
  ∀ (this : (i : ι) → Fintype (κ i)),
    Eq.{uN + 1} (α := N) ((f : (a : (i : ι) → (j : κ i) → M i j) → N) fun (i : ι) ↦ x i : N)
      ((g : (a : (i : ι) → (j : κ i) → M i j) → N) fun (i : ι) ↦ x i : N)
⊢ Eq.{uN + 1} (α := N) ((f : (a : (i : ι) → (j : κ i) → M i j) → N) fun (i : ι) ↦ x i : N)
    ((g : (a : (i : ι) → (j : κ i) → M i j) → N) fun (i : ι) ↦ x i : N)

Tactic:
have (i : _) := (nonempty_fintype (κ i)).some
-- Module: Mathlib.LinearAlgebra.Multilinear.Pi
Goal:
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : Type uN
inst : Semiring R
inst_1 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst_2 : AddCommMonoid N
inst_3 : (i : ι) → (k : κ i) → Module.{uR, uM} R (M i k)
inst_4 : Module R N
inst_5 : Finite ι
inst_6 : ∀ (i : ι), Finite.{uκ + 1} (κ i)
inst_7 : (i : ι) → DecidableEq (κ i)
f g : MultilinearMap R (fun (i : ι) ↦ (j : κ i) → M i j) N
h :
  ∀ (p : (i : ι) → κ i),
    Eq (α := MultilinearMap.{uR, uι, uM, uN} R (fun (i : ι) ↦ M i (p i)) N)
      (f.compLinearMap (M₁ := fun (i : ι) ↦ M i (p i)) (M₁' := fun (i : ι) ↦ (j : κ i) → M i j) fun (i : ι) ↦
        LinearMap.single R (M i) (p i))
      (g.compLinearMap (M₁ := fun (i : ι) ↦ M i (p i)) (M₁' := fun (i : ι) ↦ (j : κ i) → M i j) fun (i : ι) ↦
        LinearMap.single R (M i) (p i))
x : (i : ι) → (j : κ i) → M i j
i : Fintype ι
this : (i : ι) → Fintype (κ i)
H :
  ∀ (this : DecidableEq ι),
    Eq.{uN + 1} (α := N) ((f : (a : (i : ι) → (j : κ i) → M i j) → N) fun (i : ι) ↦ x i : N)
      ((g : (a : (i : ι) → (j : κ i) → M i j) → N) fun (i : ι) ↦ x i : N)
⊢ Eq.{uN + 1} (α := N) ((f : (a : (i : ι) → (j : κ i) → M i j) → N) fun (i : ι) ↦ x i : N)
    ((g : (a : (i : ι) → (j : κ i) → M i j) → N) fun (i : ι) ↦ x i : N)

Tactic:
have := Classical.decEq ι