case refine'_1
R : Type ?u.1350987
inst✝¹⁹ : Semiring R
M : Type ?u.1350993
inst✝¹⁸ : AddCommMonoid M
inst✝¹⁷ : Module R M
N : Type ?u.1351025
inst✝¹⁶ : AddCommMonoid N
inst✝¹⁵ : Module R N
P : Type ?u.1351055
inst✝¹⁴ : AddCommMonoid P
inst✝¹³ : Module R P
M' : Type ?u.1351085
inst✝¹² : AddCommGroup M'
inst✝¹¹ : Module R M'
N' : Type ?u.1351473
inst✝¹⁰ : AddCommGroup N'
inst✝⁹ : Module R N'
ι : Type ?u.1351861
ι' : Type ?u.1351864
ι'' : Type ?u.1351867
R' : Type u_1
M'' : Type u_3
M₂'' : Type u_2
N'' : Type u_4
N₂'' : Type ?u.1351882
inst✝⁸ : CommSemiring R'
inst✝⁷ : AddCommMonoid M''
inst✝⁶ : AddCommMonoid M₂''
inst✝⁵ : AddCommMonoid N''
inst✝⁴ : AddCommMonoid N₂''
inst✝³ : Module R' M''
inst✝² : Module R' M₂''
inst✝¹ : Module R' N''
inst✝ : Module R' N₂''
n : ℕ
g : M₂'' →ₗ[R'] M''
f : AlternatingMap R' M'' N'' (Fin (Nat.succ n))
m : M₂''
v : Fin n → M₂''
⊢ ↑((fun x => g) 0) (Matrix.vecCons m v 0) = Matrix.vecCons (↑g m) (fun i => ↑((fun x => g) i) (v i)) 0

case refine'_2
R : Type ?u.1350987
inst✝¹⁹ : Semiring R
M : Type ?u.1350993
inst✝¹⁸ : AddCommMonoid M
inst✝¹⁷ : Module R M
N : Type ?u.1351025
inst✝¹⁶ : AddCommMonoid N
inst✝¹⁵ : Module R N
P : Type ?u.1351055
inst✝¹⁴ : AddCommMonoid P
inst✝¹³ : Module R P
M' : Type ?u.1351085
inst✝¹² : AddCommGroup M'
inst✝¹¹ : Module R M'
N' : Type ?u.1351473
inst✝¹⁰ : AddCommGroup N'
inst✝⁹ : Module R N'
ι : Type ?u.1351861
ι' : Type ?u.1351864
ι'' : Type ?u.1351867
R' : Type u_1
M'' : Type u_3
M₂'' : Type u_2
N'' : Type u_4
N₂'' : Type ?u.1351882
inst✝⁸ : CommSemiring R'
inst✝⁷ : AddCommMonoid M''
inst✝⁶ : AddCommMonoid M₂''
inst✝⁵ : AddCommMonoid N''
inst✝⁴ : AddCommMonoid N₂''
inst✝³ : Module R' M''
inst✝² : Module R' M₂''
inst✝¹ : Module R' N''
inst✝ : Module R' N₂''
n : ℕ
g : M₂'' →ₗ[R'] M''
f : AlternatingMap R' M'' N'' (Fin (Nat.succ n))
m : M₂''
v : Fin n → M₂''
⊢ ∀ (i : Fin n),
    ↑((fun x => g) (Fin.succ i)) (Matrix.vecCons m v (Fin.succ i)) =
      Matrix.vecCons (↑g m) (fun i => ↑((fun x => g) i) (v i)) (Fin.succ i)
R : Type ?u.1350987
inst✝¹⁹ : Semiring R
M : Type ?u.1350993
inst✝¹⁸ : AddCommMonoid M
inst✝¹⁷ : Module R M
N : Type ?u.1351025
inst✝¹⁶ : AddCommMonoid N
inst✝¹⁵ : Module R N
P : Type ?u.1351055
inst✝¹⁴ : AddCommMonoid P
inst✝¹³ : Module R P
M' : Type ?u.1351085
inst✝¹² : AddCommGroup M'
inst✝¹¹ : Module R M'
N' : Type ?u.1351473
inst✝¹⁰ : AddCommGroup N'
inst✝⁹ : Module R N'
ι : Type ?u.1351861
ι' : Type ?u.1351864
ι'' : Type ?u.1351867
R' : Type u_1
M'' : Type u_3
M₂'' : Type u_2
N'' : Type u_4
N₂'' : Type ?u.1351882
inst✝⁸ : CommSemiring R'
inst✝⁷ : AddCommMonoid M''
inst✝⁶ : AddCommMonoid M₂''
inst✝⁵ : AddCommMonoid N''
inst✝⁴ : AddCommMonoid N₂''
inst✝³ : Module R' M''
inst✝² : Module R' M₂''
inst✝¹ : Module R' N''
inst✝ : Module R' N₂''
n : ℕ
g : M₂'' →ₗ[R'] M''
f : AlternatingMap R' M'' N'' (Fin (Nat.succ n))
m : M₂''
v : Fin n → M₂''
⊢ ∀ (x : Fin (Nat.succ n)),
    ↑((fun x => g) x) (Matrix.vecCons m v x) = Matrix.vecCons (↑g m) (fun i => ↑((fun x => g) i) (v i)) x
refine' Fin.cases _ _
no goals
case refine'_1
R : Type ?u.1350987
inst✝¹⁹ : Semiring R
M : Type ?u.1350993
inst✝¹⁸ : AddCommMonoid M
inst✝¹⁷ : Module R M
N : Type ?u.1351025
inst✝¹⁶ : AddCommMonoid N
inst✝¹⁵ : Module R N
P : Type ?u.1351055
inst✝¹⁴ : AddCommMonoid P
inst✝¹³ : Module R P
M' : Type ?u.1351085
inst✝¹² : AddCommGroup M'
inst✝¹¹ : Module R M'
N' : Type ?u.1351473
inst✝¹⁰ : AddCommGroup N'
inst✝⁹ : Module R N'
ι : Type ?u.1351861
ι' : Type ?u.1351864
ι'' : Type ?u.1351867
R' : Type u_1
M'' : Type u_3
M₂'' : Type u_2
N'' : Type u_4
N₂'' : Type ?u.1351882
inst✝⁸ : CommSemiring R'
inst✝⁷ : AddCommMonoid M''
inst✝⁶ : AddCommMonoid M₂''
inst✝⁵ : AddCommMonoid N''
inst✝⁴ : AddCommMonoid N₂''
inst✝³ : Module R' M''
inst✝² : Module R' M₂''
inst✝¹ : Module R' N''
inst✝ : Module R' N₂''
n : ℕ
g : M₂'' →ₗ[R'] M''
f : AlternatingMap R' M'' N'' (Fin (Nat.succ n))
m : M₂''
v : Fin n → M₂''
⊢ ↑((fun x => g) 0) (Matrix.vecCons m v 0) = Matrix.vecCons (↑g m) (fun i => ↑((fun x => g) i) (v i)) 0
rfl
no goals
case refine'_2
R : Type ?u.1350987
inst✝¹⁹ : Semiring R
M : Type ?u.1350993
inst✝¹⁸ : AddCommMonoid M
inst✝¹⁷ : Module R M
N : Type ?u.1351025
inst✝¹⁶ : AddCommMonoid N
inst✝¹⁵ : Module R N
P : Type ?u.1351055
inst✝¹⁴ : AddCommMonoid P
inst✝¹³ : Module R P
M' : Type ?u.1351085
inst✝¹² : AddCommGroup M'
inst✝¹¹ : Module R M'
N' : Type ?u.1351473
inst✝¹⁰ : AddCommGroup N'
inst✝⁹ : Module R N'
ι : Type ?u.1351861
ι' : Type ?u.1351864
ι'' : Type ?u.1351867
R' : Type u_1
M'' : Type u_3
M₂'' : Type u_2
N'' : Type u_4
N₂'' : Type ?u.1351882
inst✝⁸ : CommSemiring R'
inst✝⁷ : AddCommMonoid M''
inst✝⁶ : AddCommMonoid M₂''
inst✝⁵ : AddCommMonoid N''
inst✝⁴ : AddCommMonoid N₂''
inst✝³ : Module R' M''
inst✝² : Module R' M₂''
inst✝¹ : Module R' N''
inst✝ : Module R' N₂''
n : ℕ
g : M₂'' →ₗ[R'] M''
f : AlternatingMap R' M'' N'' (Fin (Nat.succ n))
m : M₂''
v : Fin n → M₂''
⊢ ∀ (i : Fin n),
    ↑((fun x => g) (Fin.succ i)) (Matrix.vecCons m v (Fin.succ i)) =
      Matrix.vecCons (↑g m) (fun i => ↑((fun x => g) i) (v i)) (Fin.succ i)
simp