awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Multilinear.DirectSum
Goal:
R : Type u_1
ι : Type u_2
M' : Type u_3
κ : ι → Type u_4
M : (i : ι) → κ i → Type u_5
inst : CommSemiring R
inst_1 : (i : ι) → (j : κ i) → AddCommMonoid (M i j)
inst_2 : (i : ι) → (j : κ i) → Module.{u_1, u_5} R (M i j)
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
inst_5 : DecidableEq ι
inst_6 : Finite ι
inst_7 : (i : ι) → DecidableEq (κ i)
f : MultilinearMap R (fun (i : ι) ↦ ⨁ (j : κ i), M i j) M'
p : (i : ι) → κ i
haveI :
  ∀ (this : Fintype ι),
    Eq (α := MultilinearMap.{u_1, u_2, u_5, u_3} R (fun (i : ι) ↦ M i (p i)) M')
      ((LinearEquiv.symm (fromDirectSumEquiv (κ := κ) (M := M)) :
            (a : MultilinearMap R (fun (i : ι) ↦ ⨁ (j : κ i), M i j) M') →
              (p : (i : ι) → κ i) → MultilinearMap R (fun (i : ι) ↦ M i (p i)) M')
          f p :
        MultilinearMap.{u_1, u_2, u_5, u_3} R (fun (i : ι) ↦ M i (p i)) M')
      (f.compLinearMap (M₁ := fun (i : ι) ↦ M i (p i)) (M₁' := fun (i : ι) ↦ ⨁ (j : κ i), M i j) fun (i : ι) ↦
          lof R (κ i) (M i) (p i) :
        MultilinearMap.{u_1, u_2, u_5, u_3} R (fun (i : ι) ↦ M i (p i)) M')
⊢ Eq (α := MultilinearMap.{u_1, u_2, u_5, u_3} R (fun (i : ι) ↦ M i (p i)) M')
    ((LinearEquiv.symm (fromDirectSumEquiv (κ := κ) (M := M)) :
          (a : MultilinearMap R (fun (i : ι) ↦ ⨁ (j : κ i), M i j) M') →
            (p : (i : ι) → κ i) → MultilinearMap R (fun (i : ι) ↦ M i (p i)) M')
        f p :
      MultilinearMap.{u_1, u_2, u_5, u_3} R (fun (i : ι) ↦ M i (p i)) M')
    (f.compLinearMap (M₁ := fun (i : ι) ↦ M i (p i)) (M₁' := fun (i : ι) ↦ ⨁ (j : κ i), M i j) fun (i : ι) ↦
        lof R (κ i) (M i) (p i) :
      MultilinearMap.{u_1, u_2, u_5, u_3} R (fun (i : ι) ↦ M i (p i)) M')

Tactic:
haveI : Fintype ι := Fintype.ofFinite ι
-- Module: Mathlib.LinearAlgebra.Multilinear.DirectSum
Goal:
R : Type u_1
ι : Type u_2
M' : Type u_3
κ : ι → Type u_4
M : (i : ι) → κ i → Type u_5
inst : CommSemiring R
inst_1 : (i : ι) → (j : κ i) → AddCommMonoid (M i j)
inst_2 : (i : ι) → (j : κ i) → Module.{u_1, u_5} R (M i j)
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
inst_5 : DecidableEq ι
inst_6 : Finite ι
inst_7 : (i : ι) → DecidableEq (κ i)
f : MultilinearMap R (fun (i : ι) ↦ ⨁ (j : κ i), M i j) M'
p : (i : ι) → κ i
this : Fintype ι
simp_rw :
  Eq (α := MultilinearMap.{u_1, u_2, u_5, u_3} R (fun (i : ι) ↦ M i (p i)) M')
    ((LinearEquiv.symm (fromDFinsuppEquiv κ R (M := M)) :
          (a : MultilinearMap R (fun (i : ι) ↦ ⨁ (j : κ i), M i j) M') →
            (p : (i : ι) → κ i) → MultilinearMap R (fun (i : ι) ↦ M i (p i)) M')
        f p :
      MultilinearMap.{u_1, u_2, u_5, u_3} R (fun (i : ι) ↦ M i (p i)) M')
    ((LinearEquiv.symm (fromDFinsuppEquiv κ R (M := fun (i : ι) (j : κ i) ↦ M i j)) :
          (a : MultilinearMap R (fun (i : ι) ↦ Π₀ (j : κ i), M i j) M') →
            (p : (i : ι) → κ i) → MultilinearMap R (fun (i : ι) ↦ M i (p i)) M')
        f p :
      MultilinearMap.{u_1, u_2, u_5, u_3} R (fun (i : ι) ↦ M i (p i)) M')
⊢ Eq (α := MultilinearMap.{u_1, u_2, u_5, u_3} R (fun (i : ι) ↦ M i (p i)) M')
    ((LinearEquiv.symm (fromDirectSumEquiv (κ := κ) (M := M)) :
          (a : MultilinearMap R (fun (i : ι) ↦ ⨁ (j : κ i), M i j) M') →
            (p : (i : ι) → κ i) → MultilinearMap R (fun (i : ι) ↦ M i (p i)) M')
        f p :
      MultilinearMap.{u_1, u_2, u_5, u_3} R (fun (i : ι) ↦ M i (p i)) M')
    (f.compLinearMap (M₁ := fun (i : ι) ↦ M i (p i)) (M₁' := fun (i : ι) ↦ ⨁ (j : κ i), M i j) fun (i : ι) ↦
        lof R (κ i) (M i) (p i) :
      MultilinearMap.{u_1, u_2, u_5, u_3} R (fun (i : ι) ↦ M i (p i)) M')

Tactic:
simp_rw [fromDirectSumEquiv, DirectSum.lof, ← fromDFinsuppEquiv_symm_apply]

Premises used: DirectSum.lof, MultilinearMap.fromDFinsuppEquiv_symm_apply, MultilinearMap.fromDirectSumEquiv
-- Module: Mathlib.LinearAlgebra.Multilinear.DirectSum
Goal:
R : Type u_1
ι : Type u_2
M' : Type u_3
κ : ι → Type u_4
M : (i : ι) → κ i → Type u_5
inst : CommSemiring R
inst_1 : (i : ι) → (j : κ i) → AddCommMonoid (M i j)
inst_2 : (i : ι) → (j : κ i) → Module.{u_1, u_5} R (M i j)
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
inst_5 : DecidableEq ι
inst_6 : Finite ι
inst_7 : (i : ι) → DecidableEq (κ i)
f : MultilinearMap R (fun (i : ι) ↦ ⨁ (j : κ i), M i j) M'
p : (i : ι) → κ i
this : Fintype ι
⊢ Eq (α := MultilinearMap.{u_1, u_2, u_5, u_3} R (fun (i : ι) ↦ M i (p i)) M')
    ((LinearEquiv.symm (fromDFinsuppEquiv κ R (M := M)) :
          (a : MultilinearMap R (fun (i : ι) ↦ ⨁ (j : κ i), M i j) M') →
            (p : (i : ι) → κ i) → MultilinearMap R (fun (i : ι) ↦ M i (p i)) M')
        f p :
      MultilinearMap.{u_1, u_2, u_5, u_3} R (fun (i : ι) ↦ M i (p i)) M')
    ((LinearEquiv.symm (fromDFinsuppEquiv κ R (M := M)) :
          (a : MultilinearMap R (fun (i : ι) ↦ ⨁ (j : κ i), M i j) M') →
            (p : (i : ι) → κ i) → MultilinearMap R (fun (i : ι) ↦ M i (p i)) M')
        f p :
      MultilinearMap.{u_1, u_2, u_5, u_3} R (fun (i : ι) ↦ M i (p i)) M')

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Multilinear.DirectSum
Goal:
R : Type u_1
ι : Type u_2
M' : Type u_3
κ : ι → Type u_4
M : (i : ι) → κ i → Type u_5
inst : CommSemiring R
inst_1 : (i : ι) → (j : κ i) → AddCommMonoid (M i j)
inst_2 : (i : ι) → (j : κ i) → Module.{u_1, u_5} R (M i j)
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
inst_5 : DecidableEq ι
inst_6 : Finite ι
inst_7 : (i : ι) → DecidableEq (κ i)
f : MultilinearMap R (fun (i : ι) ↦ ⨁ (j : κ i), M i j) M'
p : (i : ι) → κ i
this : Fintype ι
⊢ Eq (α := MultilinearMap.{u_1, u_2, u_5, u_3} R (fun (i : ι) ↦ M i (p i)) M')
    ((LinearEquiv.symm (fromDFinsuppEquiv κ R (M := M)) :
          (a : MultilinearMap R (fun (i : ι) ↦ ⨁ (j : κ i), M i j) M') →
            (p : (i : ι) → κ i) → MultilinearMap R (fun (i : ι) ↦ M i (p i)) M')
        f p :
      MultilinearMap.{u_1, u_2, u_5, u_3} R (fun (i : ι) ↦ M i (p i)) M')
    ((LinearEquiv.symm (fromDFinsuppEquiv κ R (M := fun (i : ι) (j : κ i) ↦ M i j)) :
          (a : MultilinearMap R (fun (i : ι) ↦ Π₀ (j : κ i), M i j) M') →
            (p : (i : ι) → κ i) → MultilinearMap R (fun (i : ι) ↦ M i (p i)) M')
        f p :
      MultilinearMap.{u_1, u_2, u_5, u_3} R (fun (i : ι) ↦ M i (p i)) M')

Tactic:
convert! rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Multilinear.FiniteDimensional
Goal:
R : Type u_2
M₂ : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M₂
inst_2 : Module R M₂
inst_3 : Module.Finite R M₂
inst_4 : Module.Free R M₂
N : Fin 0 → Type u_5
inst_5 : (i : Fin 0) → AddCommGroup (N i)
inst_6 : (i : Fin 0) → Module.{u_2, u_5} R (N i)
inst_7 : ∀ (i : Fin 0), Module.Finite.{u_2, u_5} R (N i)
inst_8 : ∀ (i : Fin 0), Module.Free.{u_2, u_5} R (N i)
⊢ IsEmpty (Fin Nat.zero)

Tactic:
haveI : IsEmpty (Fin Nat.zero) := inferInstanceAs (IsEmpty (Fin 0))
-- Module: Mathlib.LinearAlgebra.Multilinear.FiniteDimensional
Goal:
R : Type u_2
M₂ : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M₂
inst_2 : Module R M₂
inst_3 : Module.Finite R M₂
inst_4 : Module.Free R M₂
N : Fin 0 → Type u_5
inst_5 : (i : Fin 0) → AddCommGroup (N i)
inst_6 : (i : Fin 0) → Module.{u_2, u_5} R (N i)
inst_7 : ∀ (i : Fin 0), Module.Finite.{u_2, u_5} R (N i)
inst_8 : ∀ (i : Fin 0), Module.Free.{u_2, u_5} R (N i)
this : IsEmpty (Fin Nat.zero)
⊢ Module.Free R (MultilinearMap R N M₂) ∧ Module.Finite R (MultilinearMap R N M₂)

Tactic:
⟨Module.Free.of_equiv (constLinearEquivOfIsEmpty R R N M₂),
        Module.Finite.equiv (constLinearEquivOfIsEmpty R R N M₂)⟩

Premises used: MultilinearMap.constLinearEquivOfIsEmpty, And.intro, Module.Free.of_equiv, Module.Finite.equiv
-- Module: Mathlib.LinearAlgebra.Multilinear.FiniteDimensional
Goal:
R : Type u_2
M₂ : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M₂
inst_2 : Module R M₂
inst_3 : Module.Finite R M₂
inst_4 : Module.Free R M₂
N : Fin 0 → Type u_5
inst_5 : (i : Fin 0) → AddCommGroup (N i)
inst_6 : (i : Fin 0) → Module.{u_2, u_5} R (N i)
inst_7 : ∀ (i : Fin 0), Module.Finite.{u_2, u_5} R (N i)
inst_8 : ∀ (i : Fin 0), Module.Free.{u_2, u_5} R (N i)
this : IsEmpty (Fin Nat.zero)
⊢ Module.Free R (MultilinearMap R N M₂) ∧ Module.Finite R (MultilinearMap R N M₂)

Tactic:
exact
      ⟨Module.Free.of_equiv (constLinearEquivOfIsEmpty R R N M₂),
        Module.Finite.equiv (constLinearEquivOfIsEmpty R R N M₂)⟩
-- Module: Mathlib.LinearAlgebra.Multilinear.FiniteDimensional
Goal:
R : Type u_2
M₂ : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M₂
inst_2 : Module R M₂
inst_3 : Module.Finite R M₂
inst_4 : Module.Free R M₂
n : ℕ
ih :
  ∀ (N : Fin n → Type u_5) [inst_9 : (i : Fin n) → AddCommGroup (N i)]
    [inst_10 : (i : Fin n) → Module.{u_2, u_5} R (N i)] [∀ (i : Fin n), Module.Finite.{u_2, u_5} R (N i)]
    [∀ (i : Fin n), Module.Free.{u_2, u_5} R (N i)],
    Module.Free R (MultilinearMap R N M₂) ∧ Module.Finite R (MultilinearMap R N M₂)
N : Fin (n + 1) → Type u_5
inst_5 : (i : Fin (n + 1)) → AddCommGroup (N i)
inst_6 : (i : Fin (n + 1)) → Module.{u_2, u_5} R (N i)
inst_7 : ∀ (i : Fin (n + 1)), Module.Finite.{u_2, u_5} R (N i)
inst_8 : ∀ (i : Fin (n + 1)), Module.Free.{u_2, u_5} R (N i)
this :
  Module.Free R (N 0 →ₗ[R] MultilinearMap.{u_2, 0, u_5, u_3} R (fun (i : Fin n) ↦ N i.succ) M₂) ∧
    Module.Finite R (N 0 →ₗ[R] MultilinearMap.{u_2, 0, u_5, u_3} R (fun (i : Fin n) ↦ N i.succ) M₂)
⊢ Module.Free R (N 0 →ₗ[R] MultilinearMap.{u_2, 0, u_5, u_3} R (fun (i : Fin n) ↦ N i.succ) M₂)

Tactic:
cases this
-- Module: Mathlib.LinearAlgebra.Multilinear.FiniteDimensional
Goal:
R : Type u_2
M₂ : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M₂
inst_2 : Module R M₂
inst_3 : Module.Finite R M₂
inst_4 : Module.Free R M₂
n : ℕ
ih :
  ∀ (N : Fin n → Type u_5) [inst_9 : (i : Fin n) → AddCommGroup (N i)]
    [inst_10 : (i : Fin n) → Module.{u_2, u_5} R (N i)] [∀ (i : Fin n), Module.Finite.{u_2, u_5} R (N i)]
    [∀ (i : Fin n), Module.Free.{u_2, u_5} R (N i)],
    Module.Free R (MultilinearMap R N M₂) ∧ Module.Finite R (MultilinearMap R N M₂)
N : Fin (n + 1) → Type u_5
inst_5 : (i : Fin (n + 1)) → AddCommGroup (N i)
inst_6 : (i : Fin (n + 1)) → Module.{u_2, u_5} R (N i)
inst_7 : ∀ (i : Fin (n + 1)), Module.Finite.{u_2, u_5} R (N i)
inst_8 : ∀ (i : Fin (n + 1)), Module.Free.{u_2, u_5} R (N i)
this :
  Module.Free R (N 0 →ₗ[R] MultilinearMap.{u_2, 0, u_5, u_3} R (fun (i : Fin n) ↦ N i.succ) M₂) ∧
    Module.Finite R (N 0 →ₗ[R] MultilinearMap.{u_2, 0, u_5, u_3} R (fun (i : Fin n) ↦ N i.succ) M₂)
left : Module.Free R (N 0 →ₗ[R] MultilinearMap.{u_2, 0, u_5, u_3} R (fun (i : Fin n) ↦ N i.succ) M₂)
⊢ Module.Finite R (N 0 →ₗ[R] MultilinearMap.{u_2, 0, u_5, u_3} R (fun (i : Fin n) ↦ N i.succ) M₂)

Tactic:
cases this
-- Module: Mathlib.LinearAlgebra.Multilinear.FiniteDimensional
Goal:
R : Type u_2
M₂ : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M₂
inst_2 : Module R M₂
inst_3 : Module.Finite R M₂
inst_4 : Module.Free R M₂
n : ℕ
ih :
  ∀ (N : Fin n → Type u_5) [inst_9 : (i : Fin n) → AddCommGroup (N i)]
    [inst_10 : (i : Fin n) → Module.{u_2, u_5} R (N i)] [∀ (i : Fin n), Module.Finite.{u_2, u_5} R (N i)]
    [∀ (i : Fin n), Module.Free.{u_2, u_5} R (N i)],
    Module.Free R (MultilinearMap R N M₂) ∧ Module.Finite R (MultilinearMap R N M₂)
N : Fin (n + 1) → Type u_5
inst_5 : (i : Fin (n + 1)) → AddCommGroup (N i)
inst_6 : (i : Fin (n + 1)) → Module.{u_2, u_5} R (N i)
inst_7 : ∀ (i : Fin (n + 1)), Module.Finite.{u_2, u_5} R (N i)
inst_8 : ∀ (i : Fin (n + 1)), Module.Free.{u_2, u_5} R (N i)
left : Module.Free R (N 0 →ₗ[R] MultilinearMap.{u_2, 0, u_5, u_3} R (fun (i : Fin n) ↦ N i.succ) M₂)
right : Module.Finite R (N 0 →ₗ[R] MultilinearMap.{u_2, 0, u_5, u_3} R (fun (i : Fin n) ↦ N i.succ) M₂)
⊢ Module.Free R (MultilinearMap R N M₂) ∧ Module.Finite R (MultilinearMap R N M₂)

Tactic:
⟨Module.Free.of_equiv (multilinearCurryLeftEquiv R N M₂).symm,
          Module.Finite.equiv (multilinearCurryLeftEquiv R N M₂).symm⟩

Premises used: LinearEquiv.symm, multilinearCurryLeftEquiv, And.intro, Module.Free.of_equiv, Module.Finite.equiv
-- Module: Mathlib.LinearAlgebra.Multilinear.FiniteDimensional
Goal:
R : Type u_2
M₂ : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M₂
inst_2 : Module R M₂
inst_3 : Module.Finite R M₂
inst_4 : Module.Free R M₂
n : ℕ
ih :
  ∀ (N : Fin n → Type u_5) [inst_9 : (i : Fin n) → AddCommGroup (N i)]
    [inst_10 : (i : Fin n) → Module.{u_2, u_5} R (N i)] [∀ (i : Fin n), Module.Finite.{u_2, u_5} R (N i)]
    [∀ (i : Fin n), Module.Free.{u_2, u_5} R (N i)],
    Module.Free R (MultilinearMap R N M₂) ∧ Module.Finite R (MultilinearMap R N M₂)
N : Fin (n + 1) → Type u_5
inst_5 : (i : Fin (n + 1)) → AddCommGroup (N i)
inst_6 : (i : Fin (n + 1)) → Module.{u_2, u_5} R (N i)
inst_7 : ∀ (i : Fin (n + 1)), Module.Finite.{u_2, u_5} R (N i)
inst_8 : ∀ (i : Fin (n + 1)), Module.Free.{u_2, u_5} R (N i)
left : Module.Free R (N 0 →ₗ[R] MultilinearMap.{u_2, 0, u_5, u_3} R (fun (i : Fin n) ↦ N i.succ) M₂)
right : Module.Finite R (N 0 →ₗ[R] MultilinearMap.{u_2, 0, u_5, u_3} R (fun (i : Fin n) ↦ N i.succ) M₂)
⊢ Module.Free R (MultilinearMap R N M₂) ∧ Module.Finite R (MultilinearMap R N M₂)

Tactic:
exact
        ⟨Module.Free.of_equiv (multilinearCurryLeftEquiv R N M₂).symm,
          Module.Finite.equiv (multilinearCurryLeftEquiv R N M₂).symm⟩
-- Module: Mathlib.LinearAlgebra.Multilinear.FiniteDimensional
Goal:
R : Type u_2
M₂ : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M₂
inst_2 : Module R M₂
inst_3 : Module.Finite R M₂
inst_4 : Module.Free R M₂
n : ℕ
ih :
  ∀ (N : Fin n → Type u_5) [inst_9 : (i : Fin n) → AddCommGroup (N i)]
    [inst_10 : (i : Fin n) → Module.{u_2, u_5} R (N i)] [∀ (i : Fin n), Module.Finite.{u_2, u_5} R (N i)]
    [∀ (i : Fin n), Module.Free.{u_2, u_5} R (N i)],
    Module.Free R (MultilinearMap R N M₂) ∧ Module.Finite R (MultilinearMap R N M₂)
N : Fin (n + 1) → Type u_5
inst_5 : (i : Fin (n + 1)) → AddCommGroup (N i)
inst_6 : (i : Fin (n + 1)) → Module.{u_2, u_5} R (N i)
inst_7 : ∀ (i : Fin (n + 1)), Module.Finite.{u_2, u_5} R (N i)
inst_8 : ∀ (i : Fin (n + 1)), Module.Free.{u_2, u_5} R (N i)
succ :
  Module.Free R (N 0 →ₗ[R] MultilinearMap.{u_2, 0, u_5, u_3} R (fun (i : Fin n) ↦ N i.succ) M₂) ∧
    Module.Finite R (N 0 →ₗ[R] MultilinearMap.{u_2, 0, u_5, u_3} R (fun (i : Fin n) ↦ N i.succ) M₂)
⊢ Module.Free R (MultilinearMap R N M₂) ∧ Module.Finite R (MultilinearMap R N M₂)

Tactic:
suffices
      Module.Free R (N 0 →ₗ[R] MultilinearMap R (fun i : Fin n => N i.succ) M₂) ∧
        Module.Finite R (N 0 →ₗ[R] MultilinearMap R (fun i : Fin n => N i.succ) M₂) by
      cases this
      exact
        ⟨Module.Free.of_equiv (multilinearCurryLeftEquiv R N M₂).symm,
          Module.Finite.equiv (multilinearCurryLeftEquiv R N M₂).symm⟩
-- Module: Mathlib.LinearAlgebra.Multilinear.FiniteDimensional
Goal:
R : Type u_2
M₂ : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M₂
inst_2 : Module R M₂
inst_3 : Module.Finite R M₂
inst_4 : Module.Free R M₂
n : ℕ
ih :
  ∀ (N : Fin n → Type u_5) [inst_9 : (i : Fin n) → AddCommGroup (N i)]
    [inst_10 : (i : Fin n) → Module.{u_2, u_5} R (N i)] [∀ (i : Fin n), Module.Finite.{u_2, u_5} R (N i)]
    [∀ (i : Fin n), Module.Free.{u_2, u_5} R (N i)],
    Module.Free R (MultilinearMap R N M₂) ∧ Module.Finite R (MultilinearMap R N M₂)
N : Fin (n + 1) → Type u_5
inst_5 : (i : Fin (n + 1)) → AddCommGroup (N i)
inst_6 : (i : Fin (n + 1)) → Module.{u_2, u_5} R (N i)
inst_7 : ∀ (i : Fin (n + 1)), Module.Finite.{u_2, u_5} R (N i)
inst_8 : ∀ (i : Fin (n + 1)), Module.Free.{u_2, u_5} R (N i)
⊢ Module.Free R (MultilinearMap.{u_2, 0, u_5, u_3} R (fun (i : Fin n) ↦ N i.succ) M₂)

Tactic:
cases ih fun i => N i.succ

Premises used: Fin.succ
-- Module: Mathlib.LinearAlgebra.Multilinear.FiniteDimensional
Goal:
R : Type u_2
M₂ : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M₂
inst_2 : Module R M₂
inst_3 : Module.Finite R M₂
inst_4 : Module.Free R M₂
n : ℕ
ih :
  ∀ (N : Fin n → Type u_5) [inst_9 : (i : Fin n) → AddCommGroup (N i)]
    [inst_10 : (i : Fin n) → Module.{u_2, u_5} R (N i)] [∀ (i : Fin n), Module.Finite.{u_2, u_5} R (N i)]
    [∀ (i : Fin n), Module.Free.{u_2, u_5} R (N i)],
    Module.Free R (MultilinearMap R N M₂) ∧ Module.Finite R (MultilinearMap R N M₂)
N : Fin (n + 1) → Type u_5
inst_5 : (i : Fin (n + 1)) → AddCommGroup (N i)
inst_6 : (i : Fin (n + 1)) → Module.{u_2, u_5} R (N i)
inst_7 : ∀ (i : Fin (n + 1)), Module.Finite.{u_2, u_5} R (N i)
inst_8 : ∀ (i : Fin (n + 1)), Module.Free.{u_2, u_5} R (N i)
left : Module.Free R (MultilinearMap.{u_2, 0, u_5, u_3} R (fun (i : Fin n) ↦ N i.succ) M₂)
⊢ Module.Finite R (MultilinearMap.{u_2, 0, u_5, u_3} R (fun (i : Fin n) ↦ N i.succ) M₂)

Tactic:
cases ih fun i => N i.succ

Premises used: Fin.succ
-- Module: Mathlib.LinearAlgebra.Multilinear.FiniteDimensional
Goal:
R : Type u_2
M₂ : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M₂
inst_2 : Module R M₂
inst_3 : Module.Finite R M₂
inst_4 : Module.Free R M₂
n : ℕ
ih :
  ∀ (N : Fin n → Type u_5) [inst_9 : (i : Fin n) → AddCommGroup (N i)]
    [inst_10 : (i : Fin n) → Module.{u_2, u_5} R (N i)] [∀ (i : Fin n), Module.Finite.{u_2, u_5} R (N i)]
    [∀ (i : Fin n), Module.Free.{u_2, u_5} R (N i)],
    Module.Free R (MultilinearMap R N M₂) ∧ Module.Finite R (MultilinearMap R N M₂)
N : Fin (n + 1) → Type u_5
inst_5 : (i : Fin (n + 1)) → AddCommGroup (N i)
inst_6 : (i : Fin (n + 1)) → Module.{u_2, u_5} R (N i)
inst_7 : ∀ (i : Fin (n + 1)), Module.Finite.{u_2, u_5} R (N i)
inst_8 : ∀ (i : Fin (n + 1)), Module.Free.{u_2, u_5} R (N i)
left : Module.Free R (MultilinearMap.{u_2, 0, u_5, u_3} R (fun (i : Fin n) ↦ N i.succ) M₂)
right : Module.Finite R (MultilinearMap.{u_2, 0, u_5, u_3} R (fun (i : Fin n) ↦ N i.succ) M₂)
⊢ Module.Free R (N 0 →ₗ[R] MultilinearMap.{u_2, 0, u_5, u_3} R (fun (i : Fin n) ↦ N i.succ) M₂) ∧
    Module.Finite R (N 0 →ₗ[R] MultilinearMap.{u_2, 0, u_5, u_3} R (fun (i : Fin n) ↦ N i.succ) M₂)

Tactic:
⟨Module.Free.linearMap _ _ _ _, Module.Finite.linearMap _ _ _ _⟩

Premises used: Module.Free.linearMap, Module.Finite.linearMap, And.intro
-- Module: Mathlib.LinearAlgebra.Multilinear.FiniteDimensional
Goal:
R : Type u_2
M₂ : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M₂
inst_2 : Module R M₂
inst_3 : Module.Finite R M₂
inst_4 : Module.Free R M₂
n : ℕ
ih :
  ∀ (N : Fin n → Type u_5) [inst_9 : (i : Fin n) → AddCommGroup (N i)]
    [inst_10 : (i : Fin n) → Module.{u_2, u_5} R (N i)] [∀ (i : Fin n), Module.Finite.{u_2, u_5} R (N i)]
    [∀ (i : Fin n), Module.Free.{u_2, u_5} R (N i)],
    Module.Free R (MultilinearMap R N M₂) ∧ Module.Finite R (MultilinearMap R N M₂)
N : Fin (n + 1) → Type u_5
inst_5 : (i : Fin (n + 1)) → AddCommGroup (N i)
inst_6 : (i : Fin (n + 1)) → Module.{u_2, u_5} R (N i)
inst_7 : ∀ (i : Fin (n + 1)), Module.Finite.{u_2, u_5} R (N i)
inst_8 : ∀ (i : Fin (n + 1)), Module.Free.{u_2, u_5} R (N i)
left : Module.Free R (MultilinearMap.{u_2, 0, u_5, u_3} R (fun (i : Fin n) ↦ N i.succ) M₂)
right : Module.Finite R (MultilinearMap.{u_2, 0, u_5, u_3} R (fun (i : Fin n) ↦ N i.succ) M₂)
⊢ Module.Free R (N 0 →ₗ[R] MultilinearMap.{u_2, 0, u_5, u_3} R (fun (i : Fin n) ↦ N i.succ) M₂) ∧
    Module.Finite R (N 0 →ₗ[R] MultilinearMap.{u_2, 0, u_5, u_3} R (fun (i : Fin n) ↦ N i.succ) M₂)

Tactic:
exact ⟨Module.Free.linearMap _ _ _ _, Module.Finite.linearMap _ _ _ _⟩
-- Module: Mathlib.LinearAlgebra.Multilinear.FiniteDimensional
Goal:
R : Type u_2
M₂ : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M₂
inst_2 : Module R M₂
inst_3 : Module.Finite R M₂
inst_4 : Module.Free R M₂
n : ℕ
N : Fin n → Type u_5
inst_5 : (i : Fin n) → AddCommGroup (N i)
inst_6 : (i : Fin n) → Module.{u_2, u_5} R (N i)
inst_7 : ∀ (i : Fin n), Module.Finite.{u_2, u_5} R (N i)
inst_8 : ∀ (i : Fin n), Module.Free.{u_2, u_5} R (N i)
zero :
  ∀ (N : Fin 0 → Type u_5) [inst_9 : (i : Fin 0) → AddCommGroup (N i)]
    [inst_10 : (i : Fin 0) → Module.{u_2, u_5} R (N i)] [∀ (i : Fin 0), Module.Finite.{u_2, u_5} R (N i)]
    [∀ (i : Fin 0), Module.Free.{u_2, u_5} R (N i)],
    Module.Free R (MultilinearMap R N M₂) ∧ Module.Finite R (MultilinearMap R N M₂)
succ :
  ∀ (n : ℕ)
    (ih :
      ∀ (N : Fin n → Type u_5) [inst_9 : (i : Fin n) → AddCommGroup (N i)]
        [inst_10 : (i : Fin n) → Module.{u_2, u_5} R (N i)] [∀ (i : Fin n), Module.Finite.{u_2, u_5} R (N i)]
        [∀ (i : Fin n), Module.Free.{u_2, u_5} R (N i)],
        Module.Free R (MultilinearMap R N M₂) ∧ Module.Finite R (MultilinearMap R N M₂))
    (N : Fin (n + 1) → Type u_5) [inst_9 : (i : Fin (n + 1)) → AddCommGroup (N i)]
    [inst_10 : (i : Fin (n + 1)) → Module.{u_2, u_5} R (N i)] [∀ (i : Fin (n + 1)), Module.Finite.{u_2, u_5} R (N i)]
    [∀ (i : Fin (n + 1)), Module.Free.{u_2, u_5} R (N i)],
    Module.Free R (MultilinearMap R N M₂) ∧ Module.Finite R (MultilinearMap R N M₂)
⊢ Module.Free R (MultilinearMap R N M₂) ∧ Module.Finite R (MultilinearMap R N M₂)

Tactic:
induction n with
  | zero =>
    haveI : IsEmpty (Fin Nat.zero) := inferInstanceAs (IsEmpty (Fin 0))
    exact
      ⟨Module.Free.of_equiv (constLinearEquivOfIsEmpty R R N M₂),
        Module.Finite.equiv (constLinearEquivOfIsEmpty R R N M₂)⟩
  | succ n ih =>
    suffices
      Module.Free R (N 0 →ₗ[R] MultilinearMap R (fun i : Fin n => N i.succ) M₂) ∧
        Module.Finite R (N 0 →ₗ[R] MultilinearMap R (fun i : Fin n => N i.succ) M₂) by
      cases this
      exact
        ⟨Module.Free.of_equiv (multilinearCurryLeftEquiv R N M₂).symm,
          Module.Finite.equiv (multilinearCurryLeftEquiv R N M₂).symm⟩
    cases ih fun i => N i.succ
    exact ⟨Module.Free.linearMap _ _ _ _, Module.Finite.linearMap _ _ _ _⟩
-- 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)
intro : ∀ (val : Fintype ι), 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:
cases nonempty_fintype ι

Premises used: nonempty_fintype
-- 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 ι
⊢ ∀
    [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₂)

Tactic:
have := @free_and_finite_fin R M₂ _ _ _ _ _ (Fintype.card ι)
    (fun x => M₁ ((Fintype.equivFin ι).symm x))