[GOAL]
ι : Type u_1
R : Type u_2
M₂ : Type u_3
M₁ : ι → Type u_4
inst✝⁹ : Finite ι
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : Module R M₂
inst✝⁵ : Module.Finite R M₂
inst✝⁴ : Module.Free R M₂
n : ℕ
N : Fin n → Type u_5
inst✝³ : (i : Fin n) → AddCommGroup (N i)
inst✝² : (i : Fin n) → Module R (N i)
inst✝¹ : ∀ (i : Fin n), Module.Finite R (N i)
inst✝ : ∀ (i : Fin n), Module.Free R (N i)
⊢ Module.Free R (MultilinearMap R N M₂) ∧ Module.Finite R (MultilinearMap R N M₂)
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
ι : Type u_1
R : Type u_2
M₂ : Type u_3
M₁ : ι → Type u_4
inst✝¹³ : Finite ι
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M₂
inst✝¹⁰ : Module R M₂
inst✝⁹ : Module.Finite R M₂
inst✝⁸ : Module.Free R M₂
n : ℕ
N✝ : Fin n → Type u_5
inst✝⁷ : (i : Fin n) → AddCommGroup (N✝ i)
inst✝⁶ : (i : Fin n) → Module R (N✝ i)
inst✝⁵ : ∀ (i : Fin n), Module.Finite R (N✝ i)
inst✝⁴ : ∀ (i : Fin n), Module.Free R (N✝ i)
N : Fin Nat.zero → Type u_5
inst✝³ : (i : Fin Nat.zero) → AddCommGroup (N i)
inst✝² : (i : Fin Nat.zero) → Module R (N i)
inst✝¹ : ∀ (i : Fin Nat.zero), Module.Finite R (N i)
inst✝ : ∀ (i : Fin Nat.zero), Module.Free R (N i)
⊢ Module.Free R (MultilinearMap R N M₂) ∧ Module.Finite R (MultilinearMap R N M₂)
[PROOFSTEP]
haveI : IsEmpty (Fin Nat.zero) := inferInstanceAs (IsEmpty (Fin 0))
[GOAL]
case zero
ι : Type u_1
R : Type u_2
M₂ : Type u_3
M₁ : ι → Type u_4
inst✝¹³ : Finite ι
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M₂
inst✝¹⁰ : Module R M₂
inst✝⁹ : Module.Finite R M₂
inst✝⁸ : Module.Free R M₂
n : ℕ
N✝ : Fin n → Type u_5
inst✝⁷ : (i : Fin n) → AddCommGroup (N✝ i)
inst✝⁶ : (i : Fin n) → Module R (N✝ i)
inst✝⁵ : ∀ (i : Fin n), Module.Finite R (N✝ i)
inst✝⁴ : ∀ (i : Fin n), Module.Free R (N✝ i)
N : Fin Nat.zero → Type u_5
inst✝³ : (i : Fin Nat.zero) → AddCommGroup (N i)
inst✝² : (i : Fin Nat.zero) → Module R (N i)
inst✝¹ : ∀ (i : Fin Nat.zero), Module.Finite R (N i)
inst✝ : ∀ (i : Fin Nat.zero), Module.Free R (N i)
this : IsEmpty (Fin Nat.zero)
⊢ Module.Free R (MultilinearMap R N M₂) ∧ Module.Finite R (MultilinearMap R N M₂)
[PROOFSTEP]
exact ⟨Module.Free.of_equiv (constLinearEquivOfIsEmpty R N M₂), Module.Finite.equiv (constLinearEquivOfIsEmpty R N M₂)⟩
[GOAL]
case succ
ι : Type u_1
R : Type u_2
M₂ : Type u_3
M₁ : ι → Type u_4
inst✝¹³ : Finite ι
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M₂
inst✝¹⁰ : Module R M₂
inst✝⁹ : Module.Finite R M₂
inst✝⁸ : Module.Free R M₂
n✝ : ℕ
N✝ : Fin n✝ → Type u_5
inst✝⁷ : (i : Fin n✝) → AddCommGroup (N✝ i)
inst✝⁶ : (i : Fin n✝) → Module R (N✝ i)
inst✝⁵ : ∀ (i : Fin n✝), Module.Finite R (N✝ i)
inst✝⁴ : ∀ (i : Fin n✝), Module.Free R (N✝ i)
n : ℕ
ih :
  ∀ (N : Fin n → Type u_5) [inst : (i : Fin n) → AddCommGroup (N i)] [inst_1 : (i : Fin n) → Module R (N i)]
    [inst_2 : ∀ (i : Fin n), Module.Finite R (N i)] [inst_3 : ∀ (i : Fin n), Module.Free R (N i)],
    Module.Free R (MultilinearMap R N M₂) ∧ Module.Finite R (MultilinearMap R N M₂)
N : Fin (Nat.succ n) → Type u_5
inst✝³ : (i : Fin (Nat.succ n)) → AddCommGroup (N i)
inst✝² : (i : Fin (Nat.succ n)) → Module R (N i)
inst✝¹ : ∀ (i : Fin (Nat.succ n)), Module.Finite R (N i)
inst✝ : ∀ (i : Fin (Nat.succ n)), Module.Free R (N i)
⊢ Module.Free R (MultilinearMap R N M₂) ∧ Module.Finite R (MultilinearMap R N M₂)
[PROOFSTEP]
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₂), Module.Finite.equiv (multilinearCurryLeftEquiv R N M₂)⟩
[GOAL]
ι : Type u_1
R : Type u_2
M₂ : Type u_3
M₁ : ι → Type u_4
inst✝¹³ : Finite ι
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M₂
inst✝¹⁰ : Module R M₂
inst✝⁹ : Module.Finite R M₂
inst✝⁸ : Module.Free R M₂
n✝ : ℕ
N✝ : Fin n✝ → Type u_5
inst✝⁷ : (i : Fin n✝) → AddCommGroup (N✝ i)
inst✝⁶ : (i : Fin n✝) → Module R (N✝ i)
inst✝⁵ : ∀ (i : Fin n✝), Module.Finite R (N✝ i)
inst✝⁴ : ∀ (i : Fin n✝), Module.Free R (N✝ i)
n : ℕ
ih :
  ∀ (N : Fin n → Type u_5) [inst : (i : Fin n) → AddCommGroup (N i)] [inst_1 : (i : Fin n) → Module R (N i)]
    [inst_2 : ∀ (i : Fin n), Module.Finite R (N i)] [inst_3 : ∀ (i : Fin n), Module.Free R (N i)],
    Module.Free R (MultilinearMap R N M₂) ∧ Module.Finite R (MultilinearMap R N M₂)
N : Fin (Nat.succ n) → Type u_5
inst✝³ : (i : Fin (Nat.succ n)) → AddCommGroup (N i)
inst✝² : (i : Fin (Nat.succ n)) → Module R (N i)
inst✝¹ : ∀ (i : Fin (Nat.succ n)), Module.Finite R (N i)
inst✝ : ∀ (i : Fin (Nat.succ n)), Module.Free R (N i)
this :
  Module.Free R (N 0 →ₗ[R] MultilinearMap R (fun i => N (Fin.succ i)) M₂) ∧
    Module.Finite R (N 0 →ₗ[R] MultilinearMap R (fun i => N (Fin.succ i)) M₂)
⊢ Module.Free R (MultilinearMap R N M₂) ∧ Module.Finite R (MultilinearMap R N M₂)
[PROOFSTEP]
cases this
[GOAL]
case intro
ι : Type u_1
R : Type u_2
M₂ : Type u_3
M₁ : ι → Type u_4
inst✝¹³ : Finite ι
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M₂
inst✝¹⁰ : Module R M₂
inst✝⁹ : Module.Finite R M₂
inst✝⁸ : Module.Free R M₂
n✝ : ℕ
N✝ : Fin n✝ → Type u_5
inst✝⁷ : (i : Fin n✝) → AddCommGroup (N✝ i)
inst✝⁶ : (i : Fin n✝) → Module R (N✝ i)
inst✝⁵ : ∀ (i : Fin n✝), Module.Finite R (N✝ i)
inst✝⁴ : ∀ (i : Fin n✝), Module.Free R (N✝ i)
n : ℕ
ih :
  ∀ (N : Fin n → Type u_5) [inst : (i : Fin n) → AddCommGroup (N i)] [inst_1 : (i : Fin n) → Module R (N i)]
    [inst_2 : ∀ (i : Fin n), Module.Finite R (N i)] [inst_3 : ∀ (i : Fin n), Module.Free R (N i)],
    Module.Free R (MultilinearMap R N M₂) ∧ Module.Finite R (MultilinearMap R N M₂)
N : Fin (Nat.succ n) → Type u_5
inst✝³ : (i : Fin (Nat.succ n)) → AddCommGroup (N i)
inst✝² : (i : Fin (Nat.succ n)) → Module R (N i)
inst✝¹ : ∀ (i : Fin (Nat.succ n)), Module.Finite R (N i)
inst✝ : ∀ (i : Fin (Nat.succ n)), Module.Free R (N i)
left✝ : Module.Free R (N 0 →ₗ[R] MultilinearMap R (fun i => N (Fin.succ i)) M₂)
right✝ : Module.Finite R (N 0 →ₗ[R] MultilinearMap R (fun i => N (Fin.succ i)) M₂)
⊢ Module.Free R (MultilinearMap R N M₂) ∧ Module.Finite R (MultilinearMap R N M₂)
[PROOFSTEP]
exact ⟨Module.Free.of_equiv (multilinearCurryLeftEquiv R N M₂), Module.Finite.equiv (multilinearCurryLeftEquiv R N M₂)⟩
[GOAL]
case succ
ι : Type u_1
R : Type u_2
M₂ : Type u_3
M₁ : ι → Type u_4
inst✝¹³ : Finite ι
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M₂
inst✝¹⁰ : Module R M₂
inst✝⁹ : Module.Finite R M₂
inst✝⁸ : Module.Free R M₂
n✝ : ℕ
N✝ : Fin n✝ → Type u_5
inst✝⁷ : (i : Fin n✝) → AddCommGroup (N✝ i)
inst✝⁶ : (i : Fin n✝) → Module R (N✝ i)
inst✝⁵ : ∀ (i : Fin n✝), Module.Finite R (N✝ i)
inst✝⁴ : ∀ (i : Fin n✝), Module.Free R (N✝ i)
n : ℕ
ih :
  ∀ (N : Fin n → Type u_5) [inst : (i : Fin n) → AddCommGroup (N i)] [inst_1 : (i : Fin n) → Module R (N i)]
    [inst_2 : ∀ (i : Fin n), Module.Finite R (N i)] [inst_3 : ∀ (i : Fin n), Module.Free R (N i)],
    Module.Free R (MultilinearMap R N M₂) ∧ Module.Finite R (MultilinearMap R N M₂)
N : Fin (Nat.succ n) → Type u_5
inst✝³ : (i : Fin (Nat.succ n)) → AddCommGroup (N i)
inst✝² : (i : Fin (Nat.succ n)) → Module R (N i)
inst✝¹ : ∀ (i : Fin (Nat.succ n)), Module.Finite R (N i)
inst✝ : ∀ (i : Fin (Nat.succ n)), Module.Free R (N i)
⊢ Module.Free R (N 0 →ₗ[R] MultilinearMap R (fun i => N (Fin.succ i)) M₂) ∧
    Module.Finite R (N 0 →ₗ[R] MultilinearMap R (fun i => N (Fin.succ i)) M₂)
[PROOFSTEP]
cases ih fun i => N i.succ
[GOAL]
case succ.intro
ι : Type u_1
R : Type u_2
M₂ : Type u_3
M₁ : ι → Type u_4
inst✝¹³ : Finite ι
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M₂
inst✝¹⁰ : Module R M₂
inst✝⁹ : Module.Finite R M₂
inst✝⁸ : Module.Free R M₂
n✝ : ℕ
N✝ : Fin n✝ → Type u_5
inst✝⁷ : (i : Fin n✝) → AddCommGroup (N✝ i)
inst✝⁶ : (i : Fin n✝) → Module R (N✝ i)
inst✝⁵ : ∀ (i : Fin n✝), Module.Finite R (N✝ i)
inst✝⁴ : ∀ (i : Fin n✝), Module.Free R (N✝ i)
n : ℕ
ih :
  ∀ (N : Fin n → Type u_5) [inst : (i : Fin n) → AddCommGroup (N i)] [inst_1 : (i : Fin n) → Module R (N i)]
    [inst_2 : ∀ (i : Fin n), Module.Finite R (N i)] [inst_3 : ∀ (i : Fin n), Module.Free R (N i)],
    Module.Free R (MultilinearMap R N M₂) ∧ Module.Finite R (MultilinearMap R N M₂)
N : Fin (Nat.succ n) → Type u_5
inst✝³ : (i : Fin (Nat.succ n)) → AddCommGroup (N i)
inst✝² : (i : Fin (Nat.succ n)) → Module R (N i)
inst✝¹ : ∀ (i : Fin (Nat.succ n)), Module.Finite R (N i)
inst✝ : ∀ (i : Fin (Nat.succ n)), Module.Free R (N i)
left✝ : Module.Free R (MultilinearMap R (fun i => N (Fin.succ i)) M₂)
right✝ : Module.Finite R (MultilinearMap R (fun i => N (Fin.succ i)) M₂)
⊢ Module.Free R (N 0 →ₗ[R] MultilinearMap R (fun i => N (Fin.succ i)) M₂) ∧
    Module.Finite R (N 0 →ₗ[R] MultilinearMap R (fun i => N (Fin.succ i)) M₂)
[PROOFSTEP]
exact ⟨Module.Free.linearMap _ _ _, Module.Finite.linearMap _ _⟩
[GOAL]
ι : Type u_1
R : Type u_2
M₂ : Type u_3
M₁ : ι → Type u_4
inst✝⁹ : Finite ι
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : Module R M₂
inst✝⁵ : Module.Finite R M₂
inst✝⁴ : Module.Free R M₂
inst✝³ : (i : ι) → AddCommGroup (M₁ i)
inst✝² : (i : ι) → Module R (M₁ i)
inst✝¹ : ∀ (i : ι), Module.Finite R (M₁ i)
inst✝ : ∀ (i : ι), Module.Free R (M₁ i)
⊢ Module.Free R (MultilinearMap R M₁ M₂) ∧ Module.Finite R (MultilinearMap R M₁ M₂)
[PROOFSTEP]
cases nonempty_fintype ι
[GOAL]
case intro
ι : Type u_1
R : Type u_2
M₂ : Type u_3
M₁ : ι → Type u_4
inst✝⁹ : Finite ι
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : Module R M₂
inst✝⁵ : Module.Finite R M₂
inst✝⁴ : Module.Free R M₂
inst✝³ : (i : ι) → AddCommGroup (M₁ i)
inst✝² : (i : ι) → Module R (M₁ i)
inst✝¹ : ∀ (i : ι), Module.Finite R (M₁ i)
inst✝ : ∀ (i : ι), Module.Free R (M₁ i)
val✝ : Fintype ι
⊢ Module.Free R (MultilinearMap R M₁ M₂) ∧ Module.Finite R (MultilinearMap R M₁ M₂)
[PROOFSTEP]
have := @free_and_finite_fin R M₂ _ _ _ _ _ (Fintype.card ι) (fun x => M₁ ((Fintype.equivFin ι).symm x))
[GOAL]
case intro
ι : Type u_1
R : Type u_2
M₂ : Type u_3
M₁ : ι → Type u_4
inst✝⁹ : Finite ι
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : Module R M₂
inst✝⁵ : Module.Finite R M₂
inst✝⁴ : Module.Free R M₂
inst✝³ : (i : ι) → AddCommGroup (M₁ i)
inst✝² : (i : ι) → Module R (M₁ i)
inst✝¹ : ∀ (i : ι), Module.Finite R (M₁ i)
inst✝ : ∀ (i : ι), Module.Free R (M₁ i)
val✝ : Fintype ι
this :
  ∀ [inst : (i : Fin (Fintype.card ι)) → AddCommGroup (M₁ (↑(Fintype.equivFin ι).symm i))]
    [inst_1 : (i : Fin (Fintype.card ι)) → Module R (M₁ (↑(Fintype.equivFin ι).symm i))]
    [inst_2 : ∀ (i : Fin (Fintype.card ι)), Module.Finite R (M₁ (↑(Fintype.equivFin ι).symm i))]
    [inst_3 : ∀ (i : Fin (Fintype.card ι)), Module.Free R (M₁ (↑(Fintype.equivFin ι).symm i))],
    Module.Free R (MultilinearMap R (fun x => M₁ (↑(Fintype.equivFin ι).symm x)) M₂) ∧
      Module.Finite R (MultilinearMap R (fun x => M₁ (↑(Fintype.equivFin ι).symm x)) M₂)
⊢ Module.Free R (MultilinearMap R M₁ M₂) ∧ Module.Finite R (MultilinearMap R M₁ M₂)
[PROOFSTEP]
cases' this with l r
[GOAL]
case intro.intro
ι : Type u_1
R : Type u_2
M₂ : Type u_3
M₁ : ι → Type u_4
inst✝⁹ : Finite ι
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : Module R M₂
inst✝⁵ : Module.Finite R M₂
inst✝⁴ : Module.Free R M₂
inst✝³ : (i : ι) → AddCommGroup (M₁ i)
inst✝² : (i : ι) → Module R (M₁ i)
inst✝¹ : ∀ (i : ι), Module.Finite R (M₁ i)
inst✝ : ∀ (i : ι), Module.Free R (M₁ i)
val✝ : Fintype ι
this :
  ∀ [inst : (i : Fin (Fintype.card ι)) → AddCommGroup (M₁ (↑(Fintype.equivFin ι).symm i))]
    [inst_1 : (i : Fin (Fintype.card ι)) → Module R (M₁ (↑(Fintype.equivFin ι).symm i))]
    [inst_2 : ∀ (i : Fin (Fintype.card ι)), Module.Finite R (M₁ (↑(Fintype.equivFin ι).symm i))]
    [inst_3 : ∀ (i : Fin (Fintype.card ι)), Module.Free R (M₁ (↑(Fintype.equivFin ι).symm i))],
    Module.Free R (MultilinearMap R (fun x => M₁ (↑(Fintype.equivFin ι).symm x)) M₂) ∧
      Module.Finite R (MultilinearMap R (fun x => M₁ (↑(Fintype.equivFin ι).symm x)) M₂)
l : Module.Free R (MultilinearMap R (fun x => M₁ (↑(Fintype.equivFin ι).symm x)) M₂)
r : Module.Finite R (MultilinearMap R (fun x => M₁ (↑(Fintype.equivFin ι).symm x)) M₂)
⊢ Module.Free R (MultilinearMap R M₁ M₂) ∧ Module.Finite R (MultilinearMap R M₁ M₂)
[PROOFSTEP]
have e := domDomCongrLinearEquiv' R M₁ M₂ (Fintype.equivFin ι)
[GOAL]
case intro.intro
ι : Type u_1
R : Type u_2
M₂ : Type u_3
M₁ : ι → Type u_4
inst✝⁹ : Finite ι
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : Module R M₂
inst✝⁵ : Module.Finite R M₂
inst✝⁴ : Module.Free R M₂
inst✝³ : (i : ι) → AddCommGroup (M₁ i)
inst✝² : (i : ι) → Module R (M₁ i)
inst✝¹ : ∀ (i : ι), Module.Finite R (M₁ i)
inst✝ : ∀ (i : ι), Module.Free R (M₁ i)
val✝ : Fintype ι
this :
  ∀ [inst : (i : Fin (Fintype.card ι)) → AddCommGroup (M₁ (↑(Fintype.equivFin ι).symm i))]
    [inst_1 : (i : Fin (Fintype.card ι)) → Module R (M₁ (↑(Fintype.equivFin ι).symm i))]
    [inst_2 : ∀ (i : Fin (Fintype.card ι)), Module.Finite R (M₁ (↑(Fintype.equivFin ι).symm i))]
    [inst_3 : ∀ (i : Fin (Fintype.card ι)), Module.Free R (M₁ (↑(Fintype.equivFin ι).symm i))],
    Module.Free R (MultilinearMap R (fun x => M₁ (↑(Fintype.equivFin ι).symm x)) M₂) ∧
      Module.Finite R (MultilinearMap R (fun x => M₁ (↑(Fintype.equivFin ι).symm x)) M₂)
l : Module.Free R (MultilinearMap R (fun x => M₁ (↑(Fintype.equivFin ι).symm x)) M₂)
r : Module.Finite R (MultilinearMap R (fun x => M₁ (↑(Fintype.equivFin ι).symm x)) M₂)
e : MultilinearMap R M₁ M₂ ≃ₗ[R] MultilinearMap R (fun i => M₁ (↑(Fintype.equivFin ι).symm i)) M₂
⊢ Module.Free R (MultilinearMap R M₁ M₂) ∧ Module.Finite R (MultilinearMap R M₁ M₂)
[PROOFSTEP]
exact ⟨Module.Free.of_equiv e.symm, Module.Finite.equiv e.symm⟩
