-- Mathlib/LinearAlgebra/ExteriorAlgebra/OfAlternating.lean
theorem liftAlternating_apply_ιMulti {n : ℕ} (f : ∀ i, M [⋀^Fin i]→ₗ[R] N)
    (v : Fin n → M) : liftAlternating (R := R) (M := M) (N := N) f (ιMulti R n v) = f n v

Proof state:
case succ
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
n : ℕ
ih :
  ∀ (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (v : Fin n → M),
    (liftAlternating f) (List.ofFn fun i => (ι R) (v i)).prod = (f n) v
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
v : Fin (n + 1) → M
⊢ (f n.succ) (Matrix.vecCons (v 0) fun i => v i.succ) = (f (n + 1)) v

Tactic:
congr

Result:
case succ.h.e_6.h
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
n : ℕ
ih :
  ∀ (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (v : Fin n → M),
    (liftAlternating f) (List.ofFn fun i => (ι R) (v i)).prod = (f n) v
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
v : Fin (n + 1) → M
⊢ (Matrix.vecCons (v 0) fun i => v i.succ) = v

Proof state:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
n : ℕ
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
v : Fin n → M
⊢ (liftAlternating f) ((ιMulti R n) v) = (f n) v

Tactic:
rw [ιMulti_apply]

Result:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
n : ℕ
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
v : Fin n → M
⊢ (liftAlternating f) (List.ofFn fun i => (ι R) (v i)).prod = (f n) v

Proof state:
case succ.h.e_6.h
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
n : ℕ
ih :
  ∀ (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (v : Fin n → M),
    (liftAlternating f) (List.ofFn fun i => (ι R) (v i)).prod = (f n) v
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
v : Fin (n + 1) → M
⊢ (Matrix.vecCons (v 0) fun i => v i.succ) = v

Tactic:
exact Matrix.cons_head_tail _

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
n : ℕ
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
v : Fin n → M
⊢ (liftAlternating f) (List.ofFn fun i => (ι R) (v i)).prod = (f n) v

Tactic:
induction n generalizing f with
| zero => rw [List.ofFn_zero, List.prod_nil, liftAlternating_one, Subsingleton.elim 0 v]
| succ n ih =>
  rw [List.ofFn_succ, List.prod_cons, liftAlternating_ι_mul, ih,
    AlternatingMap.curryLeft_apply_apply]
  congr
  exact Matrix.cons_head_tail _

Result:
no goals

Proof state:
case zero
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
v : Fin 0 → M
⊢ (liftAlternating f) (List.ofFn fun i => (ι R) (v i)).prod = (f 0) v

Tactic:
rw [List.ofFn_zero, List.prod_nil, liftAlternating_one, Subsingleton.elim 0 v]

Result:
no goals

Proof state:
case succ
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
n : ℕ
ih :
  ∀ (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (v : Fin n → M),
    (liftAlternating f) (List.ofFn fun i => (ι R) (v i)).prod = (f n) v
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
v : Fin (n + 1) → M
⊢ (liftAlternating f) (List.ofFn fun i => (ι R) (v i)).prod = (f (n + 1)) v

Tactic:
rw [List.ofFn_succ, List.prod_cons, liftAlternating_ι_mul, ih,
  AlternatingMap.curryLeft_apply_apply]

Result:
case succ
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
n : ℕ
ih :
  ∀ (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (v : Fin n → M),
    (liftAlternating f) (List.ofFn fun i => (ι R) (v i)).prod = (f n) v
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
v : Fin (n + 1) → M
⊢ (f n.succ) (Matrix.vecCons (v 0) fun i => v i.succ) = (f (n + 1)) v