no goals
R : Type u
ι : Type u'
n : ℕ
M : Fin (Nat.succ n) → Type v
M₁ : ι → Type v₁
M₂ : Type v₂
M₃ : Type v₃
M' : Type v'
inst✝¹⁴ : Semiring R
inst✝¹³ : (i : Fin (Nat.succ n)) → AddCommMonoid (M i)
inst✝¹² : (i : ι) → AddCommMonoid (M₁ i)
inst✝¹¹ : AddCommMonoid M₂
inst✝¹⁰ : AddCommMonoid M₃
inst✝⁹ : AddCommMonoid M'
inst✝⁸ : (i : Fin (Nat.succ n)) → Module R (M i)
inst✝⁷ : (i : ι) → Module R (M₁ i)
inst✝⁶ : Module R M₂
inst✝⁵ : Module R M₃
inst✝⁴ : Module R M'
f✝ f' : MultilinearMap R M₁ M₂
M₁' : ι → Type u_1
inst✝³ : (i : ι) → AddCommMonoid (M₁' i)
inst✝² : (i : ι) → Module R (M₁' i)
M₁'' : ι → Type ?u.177120
inst✝¹ : (i : ι) → AddCommMonoid (M₁'' i)
inst✝ : (i : ι) → Module R (M₁'' i)
f : (i : ι) → M₁ i →ₗ[R] M₁' i
hf : ∀ (i : ι), Surjective ↑(f i)
g₁ g₂ : MultilinearMap R M₁' M₂
h : (fun g => compLinearMap g f) g₁ = (fun g => compLinearMap g f) g₂
x : (i : ι) → M₁' i
⊢ ↑g₁ x = ↑g₂ x
simpa [fun i => surjInv_eq (hf i)] using ext_iff.mp h fun i => surjInv (hf i) (x i)