awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.DirectSum (goal)
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
⊢ 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')
have 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')
Tactic: haveI : Fintype ι := Fintype.ofFinite ι
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.DirectSum (goal)
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 (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')
have 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')
Tactic: simp_rw [fromDirectSumEquiv, DirectSum.lof, ← fromDFinsuppEquiv_symm_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.FiniteDimensional (hypothesis)
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)
⊢ Module.Free R (MultilinearMap R N M₂) ∧ Module.Finite R (MultilinearMap R N M₂)
have this : IsEmpty (Fin Nat.zero)
Tactic: haveI : IsEmpty (Fin Nat.zero) := inferInstanceAs (IsEmpty (Fin 0))
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.FiniteDimensional (hypothesis)
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 (MultilinearMap R N M₂) ∧ Module.Finite R (MultilinearMap R N M₂)
have left : 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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.FiniteDimensional (hypothesis)
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.Free R (MultilinearMap R N M₂) ∧ Module.Finite R (MultilinearMap R N M₂)
have right : 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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.FiniteDimensional (goal)
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 R N M₂) ∧ Module.Finite R (MultilinearMap R N M₂)
have 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₂)
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⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.FiniteDimensional (hypothesis)
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 (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₂)
have left : 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
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.FiniteDimensional (hypothesis)
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.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₂)
have right : 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
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.FiniteDimensional (goal)
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)
⊢ Module.Free R (MultilinearMap R N M₂) ∧ Module.Finite R (MultilinearMap R N M₂)
have 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₂)
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 _ _ _ _⟩
Cleared hypotheses: n, N, inst_5, inst_6, inst_7, inst_8
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.FiniteDimensional (goal)
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₂)
⊢ Module.Free R (MultilinearMap R N M₂) ∧ Module.Finite R (MultilinearMap R N M₂)
have 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₂)
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 _ _ _ _⟩
Cleared hypotheses: n, N, inst_5, inst_6, inst_7, inst_8
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.FiniteDimensional (goal)
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₂) ∧ Module.Finite R (MultilinearMap R M₁ M₂)
have intro : ∀ (val : Fintype ι), Module.Free R (MultilinearMap R M₁ M₂) ∧ Module.Finite R (MultilinearMap R M₁ M₂)
Tactic: cases nonempty_fintype ι
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.FiniteDimensional (hypothesis)
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 ι
⊢ Module.Free R (MultilinearMap R M₁ M₂) ∧ Module.Finite R (MultilinearMap R M₁ M₂)
have 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₂)
Tactic: have := @free_and_finite_fin R M₂ _ _ _ _ _ (Fintype.card ι)
    (fun x => M₁ ((Fintype.equivFin ι).symm x))
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.FiniteDimensional (hypothesis)
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 R M₁ M₂) ∧ Module.Finite R (MultilinearMap R M₁ M₂)
have 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₂)
Tactic: obtain ⟨l, r⟩ := this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.FiniteDimensional (hypothesis)
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.Free R (MultilinearMap R M₁ M₂) ∧ Module.Finite R (MultilinearMap R M₁ M₂)
have 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₂)
Tactic: obtain ⟨l, r⟩ := this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.FiniteDimensional (goal)
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₂)
⊢ Module.Free R (MultilinearMap R M₁ M₂) ∧ Module.Finite R (MultilinearMap R M₁ M₂)
have 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₂)
Tactic: have e := domDomCongrLinearEquiv' R R M₁ M₂ (Fintype.equivFin ι)